From 8d2e4a51d56b7f4d3673a5132edd1adb37a14295 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 21 Aug 2015 15:21:36 +0200 Subject: Added symbol functions for printing of the location for global variables. --- cfrontend/C2C.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index b919c1d4..f1c8ec8e 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1038,7 +1038,9 @@ let convertFundef loc env fd = let params = List.map (fun (id, ty) -> - (intern_string id.name, convertTyp env ty)) + let id' = intern_string id.name in + add_stamp id.stamp id'; + (id', convertTyp env ty)) fd.fd_params in let vars = List.map @@ -1047,7 +1049,9 @@ let convertFundef loc env fd = unsupported "'static' or 'extern' local variable"; if init <> None then unsupported "initialized local variable"; - (intern_string id.name, convertTyp env ty)) + let id' = intern_string id.name in + add_stamp id.stamp id'; + (id', convertTyp env ty)) fd.fd_locals in let body' = convertStmt loc env fd.fd_body in let id' = intern_string fd.fd_name.name in @@ -1075,6 +1079,7 @@ let convertFundecl env (sto, id, ty, optinit) = | Tfunction(args, res, cconv) -> (args, res, cconv) | _ -> assert false in let id' = intern_string id.name in + add_stamp id.stamp id'; let sg = signature_of_type args res cconv in let ef = if id.name = "malloc" then EF_malloc else @@ -1116,6 +1121,7 @@ let convertInitializer env ty i = let convertGlobvar loc env (sto, id, ty, optinit) = let id' = intern_string id.name in + add_stamp id.stamp id'; let ty' = convertTyp env ty in let sz = Ctypes.sizeof !comp_env ty' in let al = Ctypes.alignof !comp_env ty' in -- cgit From 98cddc7ba45b34fbd71d9a80c27a8e5ec6b311b0 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 16 Sep 2015 19:43:35 +0200 Subject: Move more functionality in the new interface. Added functions to add more information to the debuging interface, like the struct layout with offsets, bitifiled layout and removed the no longer needed mapping from stamp to atom. --- cfrontend/C2C.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 1a6abb6e..e31da76b 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -524,6 +524,11 @@ let convertField env f = (intern_string f.fld_name, convertTyp env f.fld_typ) let convertCompositedef env su id attr members = + let t = match su with C.Struct -> + let layout = Cutil.struct_layout env members in + List.iter (fun (a,b) -> Debug.set_member_offset id a b) layout; + TStruct (id,attr) | C.Union -> TUnion (id,attr) in + Debug.set_composite_size id su (Cutil.sizeof env t); Composite(intern_string id.name, begin match su with C.Struct -> Struct | C.Union -> Union end, List.map (convertField env) members, @@ -1039,7 +1044,6 @@ let convertFundef loc env fd = List.map (fun (id, ty) -> let id' = intern_string id.name in - add_stamp id.stamp id'; (id', convertTyp env ty)) fd.fd_params in let vars = @@ -1050,7 +1054,6 @@ let convertFundef loc env fd = if init <> None then unsupported "initialized local variable"; let id' = intern_string id.name in - add_stamp id.stamp id'; (id', convertTyp env ty)) fd.fd_locals in let body' = convertStmt loc env fd.fd_body in @@ -1079,7 +1082,7 @@ let convertFundecl env (sto, id, ty, optinit) = | Tfunction(args, res, cconv) -> (args, res, cconv) | _ -> assert false in let id' = intern_string id.name in - add_stamp id.stamp id'; + Debug.atom_function id id'; let sg = signature_of_type args res cconv in let ef = if id.name = "malloc" then EF_malloc else @@ -1121,7 +1124,7 @@ let convertInitializer env ty i = let convertGlobvar loc env (sto, id, ty, optinit) = let id' = intern_string id.name in - add_stamp id.stamp id'; + Debug.atom_global_variable id id'; let ty' = convertTyp env ty in let sz = Ctypes.sizeof !comp_env ty' in let al = Ctypes.alignof !comp_env ty' in -- cgit From c8a0b76c6b9c3eb004a7fccdd2ad15cc8615ef93 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 17 Sep 2015 18:19:37 +0200 Subject: First version with computation of dwarf info from debug info. Introduced a new dwarf generation from the information collected in the DebugInformation and removed the old CtODwarf translation. --- cfrontend/C2C.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index e31da76b..4ed1ded3 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1058,6 +1058,7 @@ let convertFundef loc env fd = fd.fd_locals in let body' = convertStmt loc env fd.fd_body in let id' = intern_string fd.fd_name.name in + Debug.atom_function fd.fd_name id'; Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; a_alignment = None; @@ -1082,7 +1083,6 @@ let convertFundecl env (sto, id, ty, optinit) = | Tfunction(args, res, cconv) -> (args, res, cconv) | _ -> assert false in let id' = intern_string id.name in - Debug.atom_function id id'; let sg = signature_of_type args res cconv in let ef = if id.name = "malloc" then EF_malloc else -- cgit From 31aceeb1be64d529432f35bbea16ebafc3a21df0 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 18 Sep 2015 16:42:05 +0200 Subject: Started implementing the scope for the Debug Informations. Scopes will be handled by a stack of all open scopes. This stack then can also be used to generate the debug directives to track the scopes through the rest of the passes. --- cfrontend/C2C.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 4ed1ded3..b7012ef9 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1054,6 +1054,7 @@ let convertFundef loc env fd = if init <> None then unsupported "initialized local variable"; let id' = intern_string id.name in + Debug.atom_local_variable id id'; (id', convertTyp env ty)) fd.fd_locals in let body' = convertStmt loc env fd.fd_body in -- cgit From db0a62a01bbf90617701b68917319767159bf039 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 18 Sep 2015 17:07:29 +0200 Subject: Ctypes.composite_of_def: make sure it computes within Coq. (Suggested by A. Appel.) --- cfrontend/Ctypes.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index a555f792..1f55da7f 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -802,13 +802,13 @@ Program Definition composite_of_def Next Obligation. apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos. apply align_le; apply alignof_composite_pos. -Qed. +Defined. Next Obligation. apply align_attr_two_p. apply alignof_composite_two_p. -Qed. +Defined. Next Obligation. apply align_divides. apply alignof_composite_pos. -Qed. +Defined. (** The composite environment for a program is obtained by entering its composite definitions in sequence. The definitions are assumed -- cgit From 9147350fdb47f3471ce6d9202b7c996f79ffab2d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 20 Sep 2015 15:23:38 +0200 Subject: Experiment: track the scopes of local variables via __builtin_debug. C2C: the code that insert debug builtins with the line numbers is now in Unblock. Handle calls to __builtin_debug. Unblock: generate __builtin_debug(1) for line numbers, carrying the list of active scopes as extra arguments. Generate __builtin_debug(6) for local variable declarations, carrying the corresponding scope number as extra argument. Constprop: avoid duplicating debug arguments that are constants already. PrintAsmaux: show this extra debug info as comments. --- cfrontend/C2C.ml | 74 +++++++++++++++++++++++++++----------------------------- 1 file changed, 36 insertions(+), 38 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 5cd5997d..f5e550f3 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -741,6 +741,22 @@ let rec convertExpr env e = | C.ECompound(ty1, ie) -> unsupported "compound literals"; ezero + | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) -> + let (kind, args1) = + match args with + | {edesc = C.EConst(CInt(n,_,_))} :: args1 -> (n, args1) + | _ -> error "ill_formed __builtin_debug"; (0L, args) in + let (text, args2) = + match args1 with + | {edesc = C.EConst(CStr(txt))} :: args2 -> (txt, args2) + | {edesc = C.EVar id} :: args2 -> (id.name, args2) + | _ -> error "ill_formed __builtin_debug"; ("", args1) in + let targs2 = convertTypArgs env [] args2 in + Ebuiltin( + EF_debug(P.of_int64 kind, intern_string text, + typlist_of_typelist targs2), + targs2, convertExprList env args2, convertTyp env e.etyp) + | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) -> begin match args with | {edesc = C.EConst(CStr txt)} :: args1 -> @@ -922,16 +938,6 @@ let rec contains_case s = (** Annotations for line numbers *) -let add_lineno prev_loc this_loc s = - if !Clflags.option_g && prev_loc <> this_loc && this_loc <> Cutil.no_loc - then begin - let txt = sprintf "#line:%s:%d" (fst this_loc) (snd this_loc) in - Ssequence(Sdo(Ebuiltin(EF_debug(P.one, intern_string txt, []), - Tnil, Enil, Tvoid)), - s) - end else - s - (** Statements *) let swrap = function @@ -939,36 +945,31 @@ let swrap = function | Errors.Error msg -> error ("retyping error: " ^ string_of_errmsg msg); Sskip -let rec convertStmt ploc env s = +let rec convertStmt env s = updateLoc s.sloc; match s.sdesc with | C.Sskip -> Sskip | C.Sdo e -> - add_lineno ploc s.sloc (swrap (Ctyping.sdo (convertExpr env e))) + swrap (Ctyping.sdo (convertExpr env e)) | C.Sseq(s1, s2) -> - let s1' = convertStmt ploc env s1 in - let s2' = convertStmt s1.sloc env s2 in + let s1' = convertStmt env s1 in + let s2' = convertStmt env s2 in Ssequence(s1', s2') | C.Sif(e, s1, s2) -> let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.sifthenelse te - (convertStmt s.sloc env s1) (convertStmt s.sloc env s2))) + swrap (Ctyping.sifthenelse te (convertStmt env s1) (convertStmt env s2)) | C.Swhile(e, s1) -> let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.swhile te (convertStmt s.sloc env s1))) + swrap (Ctyping.swhile te (convertStmt env s1)) | C.Sdowhile(s1, e) -> let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.sdowhile te (convertStmt s.sloc env s1))) + swrap (Ctyping.sdowhile te (convertStmt env s1)) | C.Sfor(s1, e, s2, s3) -> let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.sfor - (convertStmt s.sloc env s1) te - (convertStmt s.sloc env s2) (convertStmt s.sloc env s3))) + swrap (Ctyping.sfor + (convertStmt env s1) te + (convertStmt env s2) (convertStmt env s3)) | C.Sbreak -> Sbreak | C.Scontinue -> @@ -981,22 +982,20 @@ let rec convertStmt ploc env s = contains_case init end; let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.sswitch te - (convertSwitch s.sloc env (is_longlong env e.etyp) cases))) + swrap (Ctyping.sswitch te + (convertSwitch env (is_longlong env e.etyp) cases)) | C.Slabeled(C.Slabel lbl, s1) -> - add_lineno ploc s.sloc - (Slabel(intern_string lbl, convertStmt s.sloc env s1)) + Slabel(intern_string lbl, convertStmt env s1) | C.Slabeled(C.Scase _, _) -> unsupported "'case' outside of 'switch'"; Sskip | C.Slabeled(C.Sdefault, _) -> unsupported "'default' outside of 'switch'"; Sskip | C.Sgoto lbl -> - add_lineno ploc s.sloc (Sgoto(intern_string lbl)) + Sgoto(intern_string lbl) | C.Sreturn None -> - add_lineno ploc s.sloc (Sreturn None) + Sreturn None | C.Sreturn(Some e) -> - add_lineno ploc s.sloc (Sreturn(Some(convertExpr env e))) + Sreturn(Some(convertExpr env e)) | C.Sblock _ -> unsupported "nested blocks"; Sskip | C.Sdecl _ -> @@ -1004,10 +1003,9 @@ let rec convertStmt ploc env s = | C.Sasm(attrs, txt, outputs, inputs, clobber) -> if not !Clflags.option_finline_asm then unsupported "inline 'asm' statement (consider adding option -finline-asm)"; - add_lineno ploc s.sloc - (Sdo (convertAsm s.sloc env txt outputs inputs clobber)) + Sdo (convertAsm s.sloc env txt outputs inputs clobber) -and convertSwitch ploc env is_64 = function +and convertSwitch env is_64 = function | [] -> LSnil | (lbl, s) :: rem -> @@ -1024,7 +1022,7 @@ and convertSwitch ploc env is_64 = function then Z.of_uint64 v else Z.of_uint32 (Int64.to_int32 v)) in - LScons(lbl', convertStmt ploc env s, convertSwitch s.sloc env is_64 rem) + LScons(lbl', convertStmt env s, convertSwitch env is_64 rem) (** Function definitions *) @@ -1049,7 +1047,7 @@ let convertFundef loc env fd = unsupported "initialized local variable"; (intern_string id.name, convertTyp env ty)) fd.fd_locals in - let body' = convertStmt loc env fd.fd_body in + let body' = convertStmt env fd.fd_body in let id' = intern_string fd.fd_name.name in Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; -- cgit From 5492b5b55afa68e3d628da07ff583a0cac79b7e3 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 28 Sep 2015 13:36:53 +0200 Subject: Added location for the formal parameters and move the end of all scopes before the last statement. --- cfrontend/C2C.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index dd55e60f..332665f4 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1042,6 +1042,7 @@ let convertFundef loc env fd = List.map (fun (id, ty) -> let id' = intern_string id.name in + Debug.atom_parameter fd.fd_name id id'; (id', convertTyp env ty)) fd.fd_params in let vars = -- cgit From ee76d81e0e7d8a76cd31bf0d01a532d248dca45a Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 30 Sep 2015 12:43:49 +0200 Subject: Fixed minor issue with parameters that get put on the stack, made the code more robust and added indentation for convertCompositeDef --- cfrontend/C2C.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 332665f4..bd281374 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -524,10 +524,12 @@ let convertField env f = (intern_string f.fld_name, convertTyp env f.fld_typ) let convertCompositedef env su id attr members = - let t = match su with C.Struct -> - let layout = Cutil.struct_layout env members in - List.iter (fun (a,b) -> Debug.set_member_offset id a b) layout; - TStruct (id,attr) | C.Union -> TUnion (id,attr) in + let t = match su with + | C.Struct -> + let layout = Cutil.struct_layout env members in + List.iter (fun (a,b) -> Debug.set_member_offset id a b) layout; + TStruct (id,attr) + | C.Union -> TUnion (id,attr) in Debug.set_composite_size id su (Cutil.sizeof env t); Composite(intern_string id.name, begin match su with C.Struct -> Struct | C.Union -> Union end, -- cgit