diff options
33 files changed, 2257 insertions, 909 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index f7f0d313..86f9f973 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -152,7 +152,8 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Section_user(s, wr, ex) -> sprintf ".section \"%s\",\"a%s%s\",%%progbits" s (if wr then "w" else "") (if ex then "x" else "") - | Section_debug_info + | Section_debug_info _ + | Section_debug_loc | Section_debug_abbrev -> "" (* Dummy value *) let section oc sec = @@ -905,9 +906,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let get_end_addr () = -1 (* Dummy constant *) let get_stmt_list_addr () = -1 (* Dummy constant *) - - module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs (* Dummy Abbrev types *) + let get_debug_start_addr () = -1 (* Dummy constant *) + let label = elf_label let new_label = new_label diff --git a/backend/Constprop.v b/backend/Constprop.v index cd844d30..8f4cb76d 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -144,9 +144,9 @@ Fixpoint debug_strength_reduction (ae: AE.t) (al: list (builtin_arg reg)) := | a :: al => let a' := builtin_arg_reduction ae a in let al' := a :: debug_strength_reduction ae al in - match a' with - | BA_int _ | BA_long _ | BA_float _ | BA_single _ => a' :: al' - | _ => al' + match a, a' with + | BA _, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => a' :: al' + | _, _ => al' end end. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index d9005f5e..eafefed5 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -243,7 +243,11 @@ Proof. induction 2; simpl. - exists (@nil val); constructor. - destruct IHlist_forall2 as (vl' & A). - destruct (builtin_arg_reduction ae a1); repeat (eauto; econstructor). + assert (eval_builtin_args ge (fun r => rs#r) sp m + (a1 :: debug_strength_reduction ae al) (b1 :: vl')) + by (constructor; eauto). + destruct a1; try (econstructor; eassumption). + destruct (builtin_arg_reduction ae (BA x)); repeat (eauto; econstructor). Qed. Lemma builtin_strength_reduction_correct: diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index f3c80f3e..a152e3c2 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -24,14 +24,11 @@ open TargetPrinter module Printer(Target:TARGET) = struct - let addr_mapping: (string, (int * int)) Hashtbl.t = Hashtbl.create 7 - let get_fun_addr name = - let name = extern_atom name in - let start_addr = new_label () - and end_addr = new_label () in - Hashtbl.add addr_mapping name (start_addr,end_addr); - start_addr,end_addr + let s = Target.new_label () + and e = Target.new_label () in + Debug.add_fun_addr name (e,s); + s,e let print_debug_label oc l = if !Clflags.option_g && Configuration.advanced_debug then @@ -39,7 +36,6 @@ module Printer(Target:TARGET) = else () - let print_location oc loc = if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc) @@ -67,7 +63,9 @@ module Printer(Target:TARGET) = print_debug_label oc e; Target.print_fun_info oc name; Target.emit_constants oc lit; - Target.print_jumptable oc jmptbl + Target.print_jumptable oc jmptbl; + if !Clflags.option_g then + Hashtbl.iter (fun p i -> Debug.add_label name p i) current_function_labels let print_init_data oc name id = if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0 @@ -102,8 +100,7 @@ module Printer(Target:TARGET) = let sz = match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in Target.print_comm_symb oc sz name align - - + let print_globdef oc (name,gdef) = match gdef with | Gfun (Internal code) -> print_function oc name code @@ -113,18 +110,13 @@ module Printer(Target:TARGET) = module DwarfTarget: DwarfTypes.DWARF_TARGET = struct let label = Target.label - let name_of_section = Target.name_of_section + let section = Target.section let print_file_loc = Target.print_file_loc - let get_start_addr = Target.get_start_addr - let get_end_addr = Target.get_end_addr - let get_stmt_list_addr = Target.get_stmt_list_addr let name_of_section = Target.name_of_section - let get_fun_addr s = try Some (Hashtbl.find addr_mapping s) with Not_found -> None + let symbol = Target.symbol end - module DebugPrinter = DwarfPrinter (DwarfTarget) (Target.DwarfAbbrevs) - - + module DebugPrinter = DwarfPrinter (DwarfTarget) end let print_program oc p db = @@ -138,7 +130,14 @@ let print_program oc p db = close_filenames (); if !Clflags.option_g && Configuration.advanced_debug then begin - match db with + let atom_to_s s = + let s = C2C.atom_sections s in + match s with + | [] -> Target.name_of_section Section_text + | (Section_user (n,_,_))::_ -> n + | a::_ -> + Target.name_of_section a in + match Debug.generate_debug_info atom_to_s (Target.name_of_section Section_text) with | None -> () | Some db -> Printer.DebugPrinter.print_debug oc db diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 67e53aea..1c3b47b5 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -48,10 +48,10 @@ module type TARGET = val get_start_addr: unit -> int val get_end_addr: unit -> int val get_stmt_list_addr: unit -> int + val get_debug_start_addr: unit -> int val new_label: unit -> int val label: out_channel -> int -> unit val print_file_loc: out_channel -> file_loc -> unit - module DwarfAbbrevs: DWARF_ABBREVS end (* On-the-fly label renaming *) @@ -140,12 +140,6 @@ let coqint oc n = fprintf oc "%ld" (camlint_of_coqint n) (* Printing annotations in asm syntax *) -(** All files used in the debug entries *) -module StringSet = Set.Make(String) -let all_files : StringSet.t ref = ref StringSet.empty -let add_file file = - all_files := StringSet.add file !all_files - let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t = Hashtbl.create 7 @@ -283,6 +277,9 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args = | 5 -> (* local variable preallocated in stack *) fprintf oc "%s debug: %s resides at%a\n" comment txt print_debug_args args + | 6 -> (* scope annotations *) + fprintf oc "%s debug: current scopes%a\n" + comment print_debug_args args; | _ -> () diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 5cd5997d..bd281374 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -524,6 +524,13 @@ 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, @@ -741,6 +748,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 +945,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 +952,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 +989,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 +1010,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 +1029,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 *) @@ -1038,7 +1043,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 + Debug.atom_parameter fd.fd_name id id'; + (id', convertTyp env ty)) fd.fd_params in let vars = List.map @@ -1047,10 +1054,13 @@ 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 + Debug.atom_local_variable id id'; + (id', 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 + Debug.atom_function fd.fd_name id'; Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; a_alignment = None; @@ -1116,6 +1126,7 @@ let convertInitializer env ty i = let convertGlobvar loc env (sto, id, ty, optinit) = let id' = intern_string id.name in + 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 diff --git a/common/Sections.ml b/common/Sections.ml index c0c95848..be0f415e 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -27,8 +27,9 @@ type section_name = | Section_literal | Section_jumptable | Section_user of string * bool (*writable*) * bool (*executable*) - | Section_debug_info + | Section_debug_info of string | Section_debug_abbrev + | Section_debug_loc type access_mode = | Access_default diff --git a/common/Sections.mli b/common/Sections.mli index e878b9e5..cf6f13b8 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -26,8 +26,9 @@ type section_name = | Section_literal | Section_jumptable | Section_user of string * bool (*writable*) * bool (*executable*) - | Section_debug_info + | Section_debug_info of string | Section_debug_abbrev + | Section_debug_loc type access_mode = | Access_default diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index fbf57082..d064f4b1 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -134,6 +134,7 @@ let rec transf_struct_members env id count = function if !config.bitfields_msb_first then sizeof_ikind carrier_ikind * 8 - pos - sz else pos in + Debug.set_bitfield_offset id name pos carrier (sizeof_ikind carrier_ikind); Hashtbl.add bitfield_table (id, name) {bf_carrier = carrier; bf_carrier_typ = carrier_typ; diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 4ceaa016..1af5af1e 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -20,6 +20,8 @@ open C let print_idents_in_full = ref false +let print_debug_idents = ref false + let print_line_numbers = ref false let location pp (file, lineno) = @@ -27,7 +29,9 @@ let location pp (file, lineno) = fprintf pp "# %d \"%s\"@ " lineno file let ident pp i = - if !print_idents_in_full + if !print_debug_idents + then fprintf pp "$%d" i.stamp + else if !print_idents_in_full then fprintf pp "%s$%d" i.name i.stamp else fprintf pp "%s" i.name diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli index d63e341c..349b5f9a 100644 --- a/cparser/Cprint.mli +++ b/cparser/Cprint.mli @@ -15,6 +15,7 @@ val print_idents_in_full : bool ref val print_line_numbers : bool ref +val print_debug_idents : bool ref val location : Format.formatter -> C.location -> unit val attributes : Format.formatter -> C.attributes -> unit diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index a3c05c34..90bbfe5a 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -427,7 +427,6 @@ let sizeof_union env members = We lay out fields consecutively, inserting padding to preserve their alignment. Not done here but in composite_info_decl: rounding size to alignment. *) - let sizeof_struct env members = let rec sizeof_rec ofs = function | [] -> @@ -449,6 +448,26 @@ let sizeof_struct env members = end in sizeof_rec 0 members +(* Simplified version to compute offsets on structs without bitfields *) +let struct_layout env members = + let rec struct_layout_rec mem ofs = function + | [] -> + mem + | [ { fld_typ = TArray(_, None, _) } as m ] -> + (* C99: ty[] allowed as last field *) + begin match alignof env m.fld_typ with + | Some a -> ( m.fld_name,align ofs a)::mem + | None -> [] + end + | m :: rem -> + match alignof env m.fld_typ, sizeof env m.fld_typ with + | Some a, Some s -> + let offset = align ofs a in + struct_layout_rec ((m.fld_name,offset)::mem) (offset + s) rem + | _, _ -> [] + in struct_layout_rec [] 0 members + + (* Determine whether a type is incomplete *) let incomplete_type env t = diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index b1f77944..b9879339 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -105,6 +105,8 @@ val composite_info_decl: Env.t -> struct_or_union -> attributes -> Env.composite_info val composite_info_def: Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info +val struct_layout: + Env.t -> field list -> (string * int) list (* Type classification functions *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 820f90f5..33c4822d 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -56,9 +56,11 @@ let elab_loc l = (l.filename, l.lineno) let top_declarations = ref ([] : globdecl list) -let emit_elab loc td = +let emit_elab ?(enter:bool=true) env loc td = let loc = elab_loc loc in - top_declarations := { gdesc = td; gloc = loc } :: !top_declarations + let dec ={ gdesc = td; gloc = loc } in + if enter then Debug.insert_global_declaration env dec; + top_declarations := dec :: !top_declarations let reset() = top_declarations := [] @@ -730,7 +732,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = (* finishing the definition of an incomplete struct or union *) let (ci', env') = elab_struct_or_union_info kind loc env members attrs in (* Emit a global definition for it *) - emit_elab loc (Gcompositedef(kind, tag', attrs, ci'.ci_members)); + emit_elab env' loc (Gcompositedef(kind, tag', attrs, ci'.ci_members)); (* Replace infos but keep same ident *) (tag', Env.add_composite env' tag' ci') | Some(tag', {ci_sizeof = Some _}), Some _ @@ -745,7 +747,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = (* enter it with a new name *) let (tag', env') = Env.enter_composite env tag ci in (* emit it *) - emit_elab loc (Gcompositedecl(kind, tag', attrs)); + emit_elab env' loc (Gcompositedecl(kind, tag', attrs)); (tag', env') | _, Some members -> (* definition of a complete struct or union *) @@ -753,12 +755,12 @@ and elab_struct_or_union only kind loc tag optmembers attrs env = (* enter it, incomplete, with a new name *) let (tag', env') = Env.enter_composite env tag ci1 in (* emit a declaration so that inner structs and unions can refer to it *) - emit_elab loc (Gcompositedecl(kind, tag', attrs)); + emit_elab env' loc (Gcompositedecl(kind, tag', attrs)); (* elaborate the members *) let (ci2, env'') = elab_struct_or_union_info kind loc env' members attrs in (* emit a definition *) - emit_elab loc (Gcompositedef(kind, tag', attrs, ci2.ci_members)); + emit_elab env'' loc (Gcompositedef(kind, tag', attrs, ci2.ci_members)); (* Replace infos but keep same ident *) (tag', Env.add_composite env'' tag' ci2) @@ -809,7 +811,7 @@ and elab_enum only loc tag optmembers attrs env = let (dcls, env') = elab_members env 0L members in let info = { ei_members = dcls; ei_attr = attrs } in let (tag', env'') = Env.enter_enum env' tag info in - emit_elab loc (Genumdef(tag', attrs, dcls)); + emit_elab env' loc (Genumdef(tag', attrs, dcls)); (tag', env'') (* Elaboration of a naked type, e.g. in a cast *) @@ -1312,7 +1314,7 @@ let elab_expr loc env a = let ty = TFun(TInt(IInt, []), None, false, []) in (* Emit an extern declaration for it *) let id = Env.fresh_ident n in - emit_elab loc (Gdecl(Storage_extern, id, ty, None)); + emit_elab env loc (Gdecl(Storage_extern, id, ty, None)); { edesc = EVar id; etyp = ty } | _ -> elab a1 in let bl = List.map elab al in @@ -1789,7 +1791,7 @@ let enter_typedefs loc env sto dl = if redef Env.lookup_ident env s then error loc "redefinition of identifier '%s' as different kind of symbol" s; let (id, env') = Env.enter_typedef env s ty in - emit_elab loc (Gtypedef(id, ty)); + emit_elab env loc (Gtypedef(id, ty)); env') env dl let enter_or_refine_ident local loc env s sto ty = @@ -1865,7 +1867,7 @@ let enter_decdefs local loc env sto dl = ((sto', id, ty', init') :: decls, env2) else begin (* Global definition *) - emit_elab loc (Gdecl(sto', id, ty', init')); + emit_elab env2 loc (Gdecl(sto', id, ty', init')); (decls, env2) end in let (decls, env') = List.fold_left enter_decdef ([], env) dl in @@ -1899,7 +1901,7 @@ let elab_fundef env spec name body loc = let (func_ty, func_init) = __func__type_and_init s in let (func_id, _, env3,func_ty) = enter_or_refine_ident true loc env2 "__func__" Storage_static func_ty in - emit_elab loc (Gdecl(Storage_static, func_id, func_ty, Some func_init)); + emit_elab ~enter:false env3 loc (Gdecl(Storage_static, func_id, func_ty, Some func_init)); (* Elaborate function body *) let body' = !elab_funbody_f ty_ret env3 body in (* Special treatment of the "main" function *) @@ -1925,7 +1927,7 @@ let elab_fundef env spec name body loc = fd_vararg = vararg; fd_locals = []; fd_body = body'' } in - emit_elab loc (Gfundef fn); + emit_elab env1 loc (Gfundef fn); env1 let elab_kr_fundef env spec name params defs body loc = @@ -1997,7 +1999,7 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition) (* pragma *) | PRAGMA(s, loc) -> - emit_elab loc (Gpragma s); + emit_elab env loc (Gpragma s); ([], env) and elab_definitions local env = function @@ -2224,7 +2226,9 @@ and elab_block_body env ctx sl = | DEFINITION def :: sl1 -> let (dcl, env') = elab_definition true env def in let loc = elab_loc (get_definitionloc def) in - List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl + List.map (fun ((sto,id,ty,_) as d) -> + Debug.insert_local_declaration sto id ty loc; + {sdesc = Sdecl d; sloc = loc}) dcl @ elab_block_body env' ctx sl1 | s :: sl1 -> let s' = elab_stmt env ctx s in diff --git a/cparser/Parse.ml b/cparser/Parse.ml index c9564c08..2be3a612 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -24,12 +24,7 @@ let transform_program t p name = (run_pass Unblock.program 'b' (run_pass Bitfields.program 'f' p)))) in - let debug = - if !Clflags.option_g && Configuration.advanced_debug then - Some (CtoDwarf.program_to_dwarf p p1 name) - else - None in - (Rename.program p1 (Filename.chop_suffix name ".c")),debug + (Rename.program p1 (Filename.chop_suffix name ".c")) let parse_transformations s = let t = ref CharSet.empty in @@ -46,7 +41,7 @@ let parse_transformations s = let preprocessed_file transfs name sourcefile = Cerrors.reset(); let ic = open_in sourcefile in - let p,d = + let p = try let t = parse_transformations transfs in let lb = Lexer.init name ic in @@ -65,6 +60,6 @@ let preprocessed_file transfs name sourcefile = Timing.time2 "Emulations" transform_program t p1 name with | Cerrors.Abort -> - [],None in + [] in close_in ic; - if Cerrors.check_errors() then None,None else Some p,d + if Cerrors.check_errors() then None else Some p diff --git a/cparser/Parse.mli b/cparser/Parse.mli index ac8feb70..58c3cfb9 100644 --- a/cparser/Parse.mli +++ b/cparser/Parse.mli @@ -15,7 +15,7 @@ (* Entry point for the library: parse, elaborate, and transform *) -val preprocessed_file: string -> string -> string -> C.program option * DwarfTypes.dw_entry option +val preprocessed_file: string -> string -> string -> C.program option (* first arg: desired transformations second arg: source file name before preprocessing diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 91f50552..c6646b5c 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -177,16 +177,89 @@ and expand_init islocal env i = in expand i +(* Insertion of debug annotation, for -g mode *) + +let debug_id = Env.fresh_ident "__builtin_debug" +let debug_ty = + TFun(TVoid [], Some [Env.fresh_ident "kind", TInt(IInt, [])], true, []) + +let debug_annot kind args = + { sloc = no_loc; + sdesc = Sdo { + etyp = TVoid []; + edesc = ECall({edesc = EVar debug_id; etyp = debug_ty}, + intconst kind IInt :: args) + } + } + +let string_const str = + let c = CStr str in { edesc = EConst c; etyp = type_of_constant c } + +let integer_const n = + intconst (Int64.of_int n) IInt + +(* Line number annotation: + __builtin_debug(1, "#line:filename:lineno") *) +(* TODO: consider + __builtin_debug(1, "filename", lineno) + instead. *) + +let debug_lineno (filename, lineno) = + debug_annot 1L + [string_const (Printf.sprintf "#line:%s:%d" filename lineno)] + +(* Scope annotation: + __builtin_debug(6, "", scope1, scope2, ..., scopeN) +*) + +let empty_string = string_const "" + +let curr_fun_id = ref 0 + +let debug_var_decl ctx id = + Debug.add_lvar_scope !curr_fun_id id (List.hd ctx) + +let debug_scope ctx = + debug_annot 6L (empty_string :: List.rev_map integer_const ctx) + +(* Add line number debug annotation if the line number changes. + Add scope debug annotation regardless. *) + + +let add_lineno ctx prev_loc this_loc s = + if !Clflags.option_g then + sseq no_loc (debug_scope ctx) + (if this_loc <> prev_loc && this_loc <> no_loc + then sseq no_loc (debug_lineno this_loc) s + else s) + else s + +(* Generate fresh scope identifiers, for blocks that contain at least + one declaration *) + +let block_contains_decl sl = + List.exists + (function {sdesc = Sdecl _} -> true | _ -> false) + sl + +let next_scope_id = ref 0 + +let new_scope_id () = + incr next_scope_id; !next_scope_id + (* Process a block-scoped variable declaration. The variable is entered in [local_variables]. The initializer, if any, is converted into assignments and prepended to [k]. *) -let process_decl loc env (sto, id, ty, optinit) k = +let process_decl loc env ctx (sto, id, ty, optinit) k = let ty' = remove_const env ty in local_variables := (sto, id, ty', None) :: !local_variables; + debug_var_decl ctx id; + (* TODO: register the fact that id is declared in scope ctx *) match optinit with - | None -> k + | None -> + k | Some init -> let init' = expand_init true env init in let l = local_initializer env { edesc = EVar id; etyp = ty' } init' [] in @@ -194,57 +267,90 @@ let process_decl loc env (sto, id, ty, optinit) k = (* Simplification of blocks within a statement *) -let rec unblock_stmt env s = +let rec unblock_stmt env ctx ploc s = match s.sdesc with | Sskip -> s | Sdo e -> - {s with sdesc = Sdo(expand_expr true env e)} + add_lineno ctx ploc s.sloc + {s with sdesc = Sdo(expand_expr true env e)} | Sseq(s1, s2) -> - {s with sdesc = Sseq(unblock_stmt env s1, unblock_stmt env s2)} + {s with sdesc = Sseq(unblock_stmt env ctx ploc s1, + unblock_stmt env ctx s1.sloc s2)} | Sif(e, s1, s2) -> - {s with sdesc = Sif(expand_expr true env e, - unblock_stmt env s1, unblock_stmt env s2)} + add_lineno ctx ploc s.sloc + {s with sdesc = Sif(expand_expr true env e, + unblock_stmt env ctx s.sloc s1, + unblock_stmt env ctx s.sloc s2)} | Swhile(e, s1) -> - {s with sdesc = Swhile(expand_expr true env e, unblock_stmt env s1)} + add_lineno ctx ploc s.sloc + {s with sdesc = Swhile(expand_expr true env e, + unblock_stmt env ctx s.sloc s1)} | Sdowhile(s1, e) -> - {s with sdesc = Sdowhile(unblock_stmt env s1, expand_expr true env e)} + add_lineno ctx ploc s.sloc + {s with sdesc = Sdowhile(unblock_stmt env ctx s.sloc s1, + expand_expr true env e)} | Sfor(s1, e, s2, s3) -> - {s with sdesc = Sfor(unblock_stmt env s1, - expand_expr true env e, - unblock_stmt env s2, - unblock_stmt env s3)} + add_lineno ctx ploc s.sloc + {s with sdesc = Sfor(unblock_stmt env ctx s.sloc s1, + expand_expr true env e, + unblock_stmt env ctx s.sloc s2, + unblock_stmt env ctx s.sloc s3)} | Sbreak -> s | Scontinue -> s | Sswitch(e, s1) -> - {s with sdesc = Sswitch(expand_expr true env e, unblock_stmt env s1)} + add_lineno ctx ploc s.sloc + {s with sdesc = Sswitch(expand_expr true env e, + unblock_stmt env ctx s.sloc s1)} | Slabeled(lbl, s1) -> - {s with sdesc = Slabeled(lbl, unblock_stmt env s1)} - | Sgoto lbl -> s - | Sreturn None -> s + add_lineno ctx ploc s.sloc + {s with sdesc = Slabeled(lbl, unblock_stmt env ctx s.sloc s1)} + | Sgoto lbl -> + add_lineno ctx ploc s.sloc s + | Sreturn None -> + add_lineno ctx ploc s.sloc s | Sreturn (Some e) -> - {s with sdesc = Sreturn(Some (expand_expr true env e))} - | Sblock sl -> unblock_block env sl - | Sdecl d -> assert false + add_lineno ctx ploc s.sloc + {s with sdesc = Sreturn(Some (expand_expr true env e))} + | Sblock sl -> + let ctx' = + if block_contains_decl sl + then + let id = new_scope_id () in + (match ctx with + | [] -> Debug.enter_function_scope !curr_fun_id id + | a::_ -> Debug.enter_scope !curr_fun_id a id); + id:: ctx + else ctx in + unblock_block env ctx' ploc sl + | Sdecl d -> + assert false | Sasm(attr, template, outputs, inputs, clob) -> let expand_asm_operand (lbl, cstr, e) = (lbl, cstr, expand_expr true env e) in - {s with sdesc = Sasm(attr, template, - List.map expand_asm_operand outputs, - List.map expand_asm_operand inputs, clob)} + add_lineno ctx ploc s.sloc + {s with sdesc = Sasm(attr, template, + List.map expand_asm_operand outputs, + List.map expand_asm_operand inputs, clob)} -and unblock_block env = function +and unblock_block env ctx ploc = function | [] -> sskip | {sdesc = Sdecl d; sloc = loc} :: sl -> - process_decl loc env d (unblock_block env sl) + add_lineno ctx ploc loc + (process_decl loc env ctx d + (unblock_block env ctx loc sl)) | s :: sl -> - sseq s.sloc (unblock_stmt env s) (unblock_block env sl) + sseq s.sloc (unblock_stmt env ctx ploc s) + (unblock_block env ctx s.sloc sl) (* Simplification of blocks and compound literals within a function *) let unblock_fundef env f = local_variables := []; - let body = unblock_stmt env f.fd_body in + next_scope_id := 0; + curr_fun_id:= f.fd_name.stamp; + (* TODO: register the parameters as being declared in function scope *) + let body = unblock_stmt env [] no_loc f.fd_body in let decls = !local_variables in local_variables := []; { f with fd_locals = f.fd_locals @ decls; fd_body = body } @@ -299,4 +405,5 @@ let rec unblock_glob env accu = function (* Entry point *) let program p = + {gloc = no_loc; gdesc = Gdecl(Storage_extern, debug_id, debug_ty, None)} :: unblock_glob (Builtins.environment()) [] p diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml deleted file mode 100644 index c2085eb0..00000000 --- a/debug/CtoDwarf.ml +++ /dev/null @@ -1,543 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) -(* *) -(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) -(* is distributed under the terms of the INRIA Non-Commercial *) -(* License Agreement. *) -(* *) -(* *********************************************************************) - -open Builtins -open C -open Cprint -open Cutil -open C2C -open DwarfTypes -open DwarfUtil -open Env -open Set - -(* Functions to translate a C Ast into Dwarf 2 debugging information *) - - -(* Hashtable from type name to entry id *) -let type_table: (string, int) Hashtbl.t = Hashtbl.create 7 - -(* Hashtable for typedefname to entry id *) -let typedef_table: (string, int) Hashtbl.t = Hashtbl.create 7 - -(* Hashtable from composite table to entry id *) -let composite_types_table: (int, int) Hashtbl.t = Hashtbl.create 7 - -(* Hashtable from id of a defined composite types to minimal type info *) -let composite_declarations: (int, (struct_or_union * string * location)) Hashtbl.t = Hashtbl.create 7 - -module IntSet = Set.Make(struct type t = int let compare = compare end) - -(* Set of all declared composite_types *) -let composite_defined: IntSet.t ref = ref IntSet.empty - -(* Get the type id of a composite_type *) -let get_composite_type (name: int): int = - try - Hashtbl.find composite_types_table name - with Not_found -> - let id = next_id () in - Hashtbl.add composite_types_table name id; - id - -(* Translate a C.typ to a string needed for hashing *) -let typ_to_string (ty: typ) = - let buf = Buffer.create 7 in - let chan = Format.formatter_of_buffer buf in - typ chan ty; - Format.pp_print_flush chan (); - Buffer.contents buf - -let rec mmap f env = function - | [] -> ([],env) - | hd :: tl -> - let (hd',env1) = f env hd in - let (tl', env2) = mmap f env1 tl in - (hd' :: tl', env2) - - -(* Helper functions for the attributes *) - -let strip_attributes typ = - let strip = List.filter (fun a -> a = AConst || a = AVolatile) in - match typ with - | TVoid at -> TVoid (strip at) - | TInt (k,at) -> TInt (k,strip at) - | TFloat (k,at) -> TFloat(k,strip at) - | TPtr (t,at) -> TPtr(t,strip at) - | TArray (t,s,at) -> TArray(t,s,strip at) - | TFun (t,arg,v,at) -> TFun(t,arg,v,strip at) - | TNamed (n,at) -> TNamed(n,strip at) - | TStruct (n,at) -> TStruct(n,strip at) - | TUnion (n,at) -> TUnion(n,strip at) - | TEnum (n,at) -> TEnum(n,strip at) - - -let strip_last_attribute typ = - let rec hd_opt l = match l with - [] -> None,[] - | AConst::rest -> Some AConst,rest - | AVolatile::rest -> Some AVolatile,rest - | _::rest -> hd_opt rest in - match typ with - | TVoid at -> let l,r = hd_opt at in - l,TVoid r - | TInt (k,at) -> let l,r = hd_opt at in - l,TInt (k,r) - | TFloat (k,at) -> let l,r = hd_opt at in - l,TFloat (k,r) - | TPtr (t,at) -> let l,r = hd_opt at in - l,TPtr(t,r) - | TArray (t,s,at) -> let l,r = hd_opt at in - l,TArray(t,s,r) - | TFun (t,arg,v,at) -> let l,r = hd_opt at in - l,TFun(t,arg,v,r) - | TNamed (n,at) -> let l,r = hd_opt at in - l,TNamed(n,r) - | TStruct (n,at) -> let l,r = hd_opt at in - l,TStruct(n,r) - | TUnion (n,at) -> let l,r = hd_opt at in - l,TUnion(n,r) - | TEnum (n,at) -> let l,r = hd_opt at in - l,TEnum(n,r) - -(* Dwarf tag for the void type*) -let rec void_dwarf_tag = - let void = { - base_type_byte_size = 0; - base_type_encoding = None; - base_type_name = "void"; - } in - DW_TAG_base_type void - -(* Generate a dwarf tag for the given integer type *) -and int_to_dwarf_tag k = - let encoding = - (match k with - | IBool -> DW_ATE_boolean - | IChar -> - if !Machine.config.Machine.char_signed then - DW_ATE_signed_char - else - DW_ATE_unsigned_char - | ILong | ILongLong | IShort | ISChar -> DW_ATE_signed_char - | _ -> DW_ATE_unsigned)in - let int = { - base_type_byte_size = sizeof_ikind k; - base_type_encoding = Some encoding; - base_type_name = typ_to_string (TInt (k,[]));} in - DW_TAG_base_type int - -(* Generate a dwarf tag for the given floating point type *) -and float_to_dwarf_tag k = - let byte_size = sizeof_fkind k in - let float = { - base_type_byte_size = byte_size; - base_type_encoding = Some DW_ATE_float; - base_type_name = typ_to_string (TFloat (k,[])); - } in - DW_TAG_base_type float - -(* Generate a dwarf tag for the given function type *) -and fun_to_dwarf_tag rt args = - let ret,et = (match rt with - | TVoid _ -> None,[] - | _ -> let ret,et = type_to_dwarf rt in - Some ret,et) in - let prototyped,children,others = - (match args with - | None -> - let u = { - unspecified_parameter_file_loc = None; - unspecified_parameter_artificial = None; - } in - let u = new_entry (DW_TAG_unspecified_parameter u) in - false,[u],[] - | Some [] -> true,[],[] - | Some l -> - let c,e = mmap (fun acc (_,t) -> - let t,e = type_to_dwarf t in - let fp = - { - formal_parameter_file_loc = None; - formal_parameter_artificial = None; - formal_parameter_location = None; - formal_parameter_name = None; - formal_parameter_segment = None; - formal_parameter_type = t; - formal_parameter_variable_parameter = None; - } in - let entry = new_entry (DW_TAG_formal_parameter fp) in - entry,(e@acc)) [] l in - true,c,e) in - let s = { - subroutine_type = ret; - subroutine_prototyped = prototyped; - } in - let s = new_entry (DW_TAG_subroutine_type s) in - let s = add_children s children in - s.id,((s::others)@et) - -(* Generate a dwarf tag for the given array type *) -and array_to_dwarf_tag child size = - let append_opt a b = - match a with - | None -> b - | Some a -> a::b in - let size_to_subrange s = - match s with - | None -> None - | Some i -> - let i = Int64.to_int (Int64.sub i Int64.one) in - let s = - { - subrange_type = None; - subrange_upper_bound = Some (BoundConst i); - } in - Some (new_entry (DW_TAG_subrange_type s)) in - let rec aux t = - (match t with - | TArray (child,size,_) -> - let sub = size_to_subrange size in - let t,c,e = aux child in - t,append_opt sub c,e - | _ -> let t,e = type_to_dwarf t in - t,[],e) in - let t,children,e = aux child in - let sub = size_to_subrange size in - let children = List.rev (append_opt sub children) in - let arr = { - array_type_file_loc = None; - array_type = t; - } in - let arr = new_entry (DW_TAG_array_type arr) in - let arr = add_children arr children in - arr.id,(arr::e) - -(* Translate a typ without attributes to a dwarf_tag *) -and type_to_dwarf_entry typ typ_string= - let id,entries = - (match typ with - | TVoid _ -> - let e = new_entry void_dwarf_tag in - e.id,[e] - | TInt (k,_) -> - let e = new_entry (int_to_dwarf_tag k) in - e.id,[e] - | TFloat (k,_) -> - let e = new_entry (float_to_dwarf_tag k) in - e.id,[e] - | TPtr (t,_) -> - let t,e = type_to_dwarf t in - let pointer = {pointer_type = t;} in - let t = new_entry (DW_TAG_pointer_type pointer) in - t.id,t::e - | TFun (rt,args,_,_) -> fun_to_dwarf_tag rt args - | TStruct (i,_) - | TUnion (i,_) - | TEnum (i,_) -> - let t = get_composite_type i.stamp in - t,[] - | TNamed (i,at) -> - let t = Hashtbl.find typedef_table i.name in - t,[] - | TArray (child,size,_) -> array_to_dwarf_tag child size) - in - Hashtbl.add type_table typ_string id; - id,entries - -(* Tranlate type with attributes to their corresponding dwarf represenation *) -and attr_type_to_dwarf typ typ_string = - let l,t = strip_last_attribute typ in - match l with - | Some AConst -> let id,t = type_to_dwarf t in - let const_tag = DW_TAG_const_type ({const_type = id;}) in - let const_entry = new_entry const_tag in - let id = const_entry.id in - Hashtbl.add type_table typ_string id; - id,const_entry::t - | Some AVolatile -> let id,t = type_to_dwarf t in - let volatile_tag = DW_TAG_volatile_type ({volatile_type = id;}) in - let volatile_entry = new_entry volatile_tag in - let id = volatile_entry.id in - Hashtbl.add type_table typ_string id; - id,volatile_entry::t - | Some (ARestrict|AAlignas _| Attr(_,_)) -> type_to_dwarf t (* This should not happen *) - | None -> type_to_dwarf_entry typ typ_string - -(* Translate a given type to its dwarf representation *) -and type_to_dwarf (typ: typ): int * dw_entry list = - match typ with - | TStruct (i,_) - | TUnion (i,_) - | TEnum (i,_) -> - let t = get_composite_type i.stamp in - t,[] - | _ -> - let typ = strip_attributes typ in - let typ_string = typ_to_string typ in - try - Hashtbl.find type_table typ_string,[] - with Not_found -> - attr_type_to_dwarf typ typ_string - -(* Translate a typedef to its corresponding dwarf representation *) -let typedef_to_dwarf gloc (name,t) = - let i,t = type_to_dwarf t in - let td = { - typedef_file_loc = gloc; - typedef_name = name; - typedef_type = i; - } in - let td = new_entry (DW_TAG_typedef td) in - Hashtbl.add typedef_table name td.id; - td::t - -(* Translate a global var to its corresponding dwarf representation *) -let glob_var_to_dwarf (s,n,t,_) gloc = - let i,t = type_to_dwarf t in - let ext = (match s with - | Storage_static -> false - | _ -> true) in - let decl = { - variable_file_loc = (Some gloc); - variable_declaration = None; - variable_external = Some ext; - variable_location = None; - variable_name = n.name; - variable_segment = None; - variable_type = i; - } in - let decl = new_entry (DW_TAG_variable decl) in - t,decl - -(* Translate a function definition to its corresponding dwarf representation *) -let fundef_to_dwarf f gloc = - let ret,e = (match f.fd_ret with - | TVoid _ -> None,[] - | _ -> let i,t = type_to_dwarf f.fd_ret in - Some i,t) in - let ext = (match f.fd_storage with - | Storage_static -> false - | _ -> true) in - let fdef = { - subprogram_file_loc = (Some gloc); - subprogram_external = Some ext; - subprogram_frame_base = None; - subprogram_name = f.fd_name.name; - subprogram_prototyped = true; - subprogram_type = ret; - } in - let fp,e = mmap (fun acc (p,t) -> - let t,e = type_to_dwarf t in - let fp = - { - formal_parameter_file_loc = None; - formal_parameter_artificial = None; - formal_parameter_location = None; - formal_parameter_name = (Some p.name); - formal_parameter_segment = None; - formal_parameter_type = t; - formal_parameter_variable_parameter = None; - } in - let entry = new_entry (DW_TAG_formal_parameter fp) in - entry,(e@acc)) e f.fd_params in - let fdef = new_entry (DW_TAG_subprogram fdef) in - let fdef = add_children fdef fp in - e,fdef - -(* Translate a enum definition to its corresponding dwarf representation *) -let enum_to_dwarf (n,at,e) gloc = - let enumerator_to_dwarf (i,c,_)= - let tag = - { - enumerator_file_loc = None; - enumerator_value = Int64.to_int c; - enumerator_name = i.name; - } in - new_entry (DW_TAG_enumerator tag) in - let bs = sizeof_ikind enum_ikind in - let enum = { - enumeration_file_loc = Some gloc; - enumeration_byte_size = bs; - enumeration_declaration = None; - enumeration_name = if n.name <> "" then Some n.name else None; - } in - let id = get_composite_type n.stamp in - let child = List.map enumerator_to_dwarf e in - let enum = - { - tag = DW_TAG_enumeration_type enum; - children = child; - id = id; - } in - [enum] - -(* Translate a struct definition to its corresponding dwarf representation *) -let struct_to_dwarf (n,at,m) env gloc = - let info = Env.find_struct env n in - let tag =DW_TAG_structure_type { - structure_file_loc = Some gloc; - structure_byte_size = info.ci_sizeof; - structure_declaration = None; - structure_name = if n.name <> "" then Some n.name else None; - } in - let id = get_composite_type n.stamp in - let rec pack acc bcc l m = - match m with - | [] -> acc,bcc,[] - | m::ms as ml -> - (match m.fld_bitfield with - | None -> acc,bcc,ml - | Some n -> - if n = 0 then - acc,bcc,ms (* bit width 0 means end of pack *) - else if l + n > 8 * !Machine.config.Machine.sizeof_int then - acc,bcc,ml (* doesn't fit in current word *) - else - let t,e = type_to_dwarf m.fld_typ in - let um = { - member_file_loc = None; - member_byte_size = Some !Machine.config.Machine.sizeof_int; - member_bit_offset = Some l; - member_bit_size = Some n; - member_data_member_location = None; - member_declaration = None; - member_name = if m.fld_name <> "" then Some m.fld_name else None; - member_type = t; - } in - pack ((new_entry (DW_TAG_member um))::acc) (e@bcc) (l + n) ms) - and translate acc bcc m = - match m with - [] -> acc,bcc - | m::ms as ml -> - (match m.fld_bitfield with - | None -> - let t,e = type_to_dwarf m.fld_typ in - let um = { - member_file_loc = None; - member_byte_size = None; - member_bit_offset = None; - member_bit_size = None; - member_data_member_location = None; - member_declaration = None; - member_name = if m.fld_name <> "" then Some m.fld_name else None; - member_type = t; - } in - translate ((new_entry (DW_TAG_member um))::acc) (e@bcc) ms - | Some _ -> let acc,bcc,rest = pack acc bcc 0 ml in - translate acc bcc rest) - in - let children,e = translate [] [] m in - let children,e = List.rev children,e in - let sou = { - tag = tag; - children = children; - id = id;} in - e@[sou] - -(* Translate a union definition to its corresponding dwarf representation *) -let union_to_dwarf (n,at,m) env gloc = - let info = Env.find_union env n in - let tag = DW_TAG_union_type { - union_file_loc = Some gloc; - union_byte_size = info.ci_sizeof; - union_declaration = None; - union_name = if n.name <> "" then Some n.name else None; - } in - let id = get_composite_type n.stamp in - let children,e = mmap - (fun acc f -> - let t,e = type_to_dwarf f.fld_typ in - let um = { - member_file_loc = None; - member_byte_size = None; - member_bit_offset = None; - member_bit_size = None; - member_data_member_location = None; - member_declaration = None; - member_name = if f.fld_name <> "" then Some f.fld_name else None; - member_type = t; - } in - new_entry (DW_TAG_member um),e@acc)[] m in - let sou = { - tag = tag; - children = children; - id = id;} in - e@[sou] - -(* Translate global declarations to there dwarf representation *) -let globdecl_to_dwarf env (typs,decls) decl = - PrintAsmaux.add_file (fst decl.gloc); - match decl.gdesc with - | Gtypedef (n,t) -> let ret = typedef_to_dwarf (Some decl.gloc) (n.name,t) in - typs@ret,decls - | Gdecl d -> let t,d = glob_var_to_dwarf d decl.gloc in - typs@t,d::decls - | Gfundef f -> let t,d = fundef_to_dwarf f decl.gloc in - typs@t,d::decls - | Genumdef (n,at,e) -> - composite_defined:= IntSet.add n.stamp !composite_defined; - let ret = enum_to_dwarf (n,at,e) decl.gloc in - typs@ret,decls - | Gcompositedef (Struct,n,at,m) -> - composite_defined:= IntSet.add n.stamp !composite_defined; - let ret = struct_to_dwarf (n,at,m) env decl.gloc in - typs@ret,decls - | Gcompositedef (Union,n,at,m) -> - composite_defined:= IntSet.add n.stamp !composite_defined; - let ret = union_to_dwarf (n,at,m) env decl.gloc in - typs@ret,decls - | Gcompositedecl (sou,i,_) -> Hashtbl.add composite_declarations i.stamp (sou,i.name,decl.gloc); - typs,decls - | Gpragma _ -> typs,decls - -let forward_declaration_to_dwarf sou name loc stamp = - let id = get_composite_type stamp in - let tag = match sou with - | Struct -> - DW_TAG_structure_type{ - structure_file_loc = Some loc; - structure_byte_size = None; - structure_declaration = Some true; - structure_name = if name <> "" then Some name else None; - } - | Union -> - DW_TAG_union_type { - union_file_loc = Some loc; - union_byte_size = None; - union_declaration = Some true; - union_name = if name <> "" then Some name else None; - } in - {tag = tag; children = []; id = id} - - -(* Compute the dwarf representations of global declarations. The second program argument is the - program after the bitfield and packed struct transformation *) -let program_to_dwarf prog prog1 name = - Hashtbl.reset type_table; - Hashtbl.reset composite_types_table; - Hashtbl.reset typedef_table; - let prog = cleanupGlobals (prog) in - let env = translEnv Env.empty prog1 in - reset_id (); - let typs = List.map (typedef_to_dwarf None) C2C.builtins.typedefs in - let typs = List.concat typs in - let typs,defs = List.fold_left (globdecl_to_dwarf env) (typs,[]) prog in - let typs = Hashtbl.fold (fun i (sou,name,loc) typs -> if not (IntSet.mem i !composite_defined) then - (forward_declaration_to_dwarf sou name loc i)::typs else typs) composite_declarations typs in - let defs = typs @ defs in - let cp = { - compile_unit_name = name; - } in - let cp = new_entry (DW_TAG_compile_unit cp) in - add_children cp defs diff --git a/debug/Debug.ml b/debug/Debug.ml new file mode 100644 index 00000000..1d3b260e --- /dev/null +++ b/debug/Debug.ml @@ -0,0 +1,108 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open AST +open BinNums +open C +open Camlcoq +open Dwarfgen +open DwarfTypes + +(* Interface for generating and printing debug information *) + +(* Record used for stroring references to the actual implementation functions *) +type implem = + { + mutable init: string -> unit; + mutable atom_function: ident -> atom -> unit; + mutable atom_global_variable: ident -> atom -> unit; + mutable set_composite_size: ident -> struct_or_union -> int option -> unit; + mutable set_member_offset: ident -> string -> int -> unit; + mutable set_bitfield_offset: ident -> string -> int -> string -> int -> unit; + mutable insert_global_declaration: Env.t -> globdecl -> unit; + mutable add_fun_addr: atom -> (int * int) -> unit; + mutable generate_debug_info: (atom -> string) -> string -> debug_entries option; + mutable all_files_iter: (string -> unit) -> unit; + mutable insert_local_declaration: storage -> ident -> typ -> location -> unit; + mutable atom_local_variable: ident -> atom -> unit; + mutable enter_scope: int -> int -> int -> unit; + mutable enter_function_scope: int -> int -> unit; + mutable add_lvar_scope: int -> ident -> int -> unit; + mutable open_scope: atom -> int -> positive -> unit; + mutable close_scope: atom -> int -> positive -> unit; + mutable start_live_range: atom -> positive -> int * int builtin_arg -> unit; + mutable end_live_range: atom -> positive -> unit; + mutable stack_variable: atom -> int * int builtin_arg -> unit; + mutable function_end: atom -> positive -> unit; + mutable add_label: atom -> positive -> int -> unit; + mutable atom_parameter: ident -> ident -> atom -> unit; + mutable add_compilation_section_start: string ->(int * int * int * string) -> unit; + mutable compute_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit; + mutable exists_section: string -> bool; + } + +let implem = + { + init = (fun _ -> ()); + atom_function = (fun _ _ -> ()); + atom_global_variable = (fun _ _ -> ()); + set_composite_size = (fun _ _ _ -> ()); + set_member_offset = (fun _ _ _ -> ()); + set_bitfield_offset = (fun _ _ _ _ _ -> ()); + insert_global_declaration = (fun _ _ -> ()); + add_fun_addr = (fun _ _ -> ()); + generate_debug_info = (fun _ _ -> None); + all_files_iter = (fun _ -> ()); + insert_local_declaration = (fun _ _ _ _ -> ()); + atom_local_variable = (fun _ _ -> ()); + enter_scope = (fun _ _ _ -> ()); + enter_function_scope = (fun _ _ -> ()); + add_lvar_scope = (fun _ _ _ -> ()); + open_scope = (fun _ _ _ -> ()); + close_scope = (fun _ _ _ -> ()); + start_live_range = (fun _ _ _ -> ()); + end_live_range = (fun _ _ -> ()); + stack_variable = (fun _ _ -> ()); + function_end = (fun _ _ -> ()); + add_label = (fun _ _ _ -> ()); + atom_parameter = (fun _ _ _ -> ()); + add_compilation_section_start = (fun _ _ -> ()); + compute_file_enum = (fun _ _ _ -> ()); + exists_section = (fun _ -> true); +} + +let init_compile_unit name = implem.init name +let atom_function id atom = implem.atom_function id atom +let atom_global_variable id atom = implem.atom_global_variable id atom +let set_composite_size id sou size = implem.set_composite_size id sou size +let set_member_offset id field off = implem.set_member_offset id field off +let set_bitfield_offset id field off underlying size = implem.set_bitfield_offset id field off underlying size +let insert_global_declaration env dec = implem.insert_global_declaration env dec +let add_fun_addr atom addr = implem.add_fun_addr atom addr +let generate_debug_info fun_s var_s = implem.generate_debug_info fun_s var_s +let all_files_iter f = implem.all_files_iter f +let insert_local_declaration sto id ty loc = implem.insert_local_declaration sto id ty loc +let atom_local_variable id atom = implem.atom_local_variable id atom +let enter_scope p_id id = implem.enter_scope p_id id +let enter_function_scope fun_id sc_id = implem.enter_function_scope fun_id sc_id +let add_lvar_scope fun_id var_id s_id = implem.add_lvar_scope fun_id var_id s_id +let open_scope atom id lbl = implem.open_scope atom id lbl +let close_scope atom id lbl = implem.close_scope atom id lbl +let start_live_range atom lbl loc = implem.start_live_range atom lbl loc +let end_live_range atom lbl = implem.end_live_range atom lbl +let stack_variable atom loc = implem.stack_variable atom loc +let function_end atom loc = implem.function_end atom loc +let add_label atom p lbl = implem.add_label atom p lbl +let atom_parameter fid pid atom = implem.atom_parameter fid pid atom +let add_compilation_section_start sec addr = implem.add_compilation_section_start sec addr +let exists_section sec = implem.exists_section sec +let compute_file_enum end_l entry_l line_e = implem.compute_file_enum end_l entry_l line_e diff --git a/debug/Debug.mli b/debug/Debug.mli new file mode 100644 index 00000000..166a6759 --- /dev/null +++ b/debug/Debug.mli @@ -0,0 +1,78 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open AST +open C +open Camlcoq +open DwarfTypes +open BinNums + + +(* Record used for stroring references to the actual implementation functions *) +type implem = + { + mutable init: string -> unit; + mutable atom_function: ident -> atom -> unit; + mutable atom_global_variable: ident -> atom -> unit; + mutable set_composite_size: ident -> struct_or_union -> int option -> unit; + mutable set_member_offset: ident -> string -> int -> unit; + mutable set_bitfield_offset: ident -> string -> int -> string -> int -> unit; + mutable insert_global_declaration: Env.t -> globdecl -> unit; + mutable add_fun_addr: atom -> (int * int) -> unit; + mutable generate_debug_info: (atom -> string) -> string -> debug_entries option; + mutable all_files_iter: (string -> unit) -> unit; + mutable insert_local_declaration: storage -> ident -> typ -> location -> unit; + mutable atom_local_variable: ident -> atom -> unit; + mutable enter_scope: int -> int -> int -> unit; + mutable enter_function_scope: int -> int -> unit; + mutable add_lvar_scope: int -> ident -> int -> unit; + mutable open_scope: atom -> int -> positive -> unit; + mutable close_scope: atom -> int -> positive -> unit; + mutable start_live_range: atom -> positive -> int * int builtin_arg -> unit; + mutable end_live_range: atom -> positive -> unit; + mutable stack_variable: atom -> int * int builtin_arg -> unit; + mutable function_end: atom -> positive -> unit; + mutable add_label: atom -> positive -> int -> unit; + mutable atom_parameter: ident -> ident -> atom -> unit; + mutable add_compilation_section_start: string -> (int * int * int * string) -> unit; + mutable compute_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit; + mutable exists_section: string -> bool; + } + +val implem: implem + +val init_compile_unit: string -> unit +val atom_function: ident -> atom -> unit +val atom_global_variable: ident -> atom -> unit +val set_composite_size: ident -> struct_or_union -> int option -> unit +val set_member_offset: ident -> string -> int -> unit +val set_bitfield_offset: ident -> string -> int -> string -> int -> unit +val insert_global_declaration: Env.t -> globdecl -> unit +val add_fun_addr: atom -> (int * int) -> unit +val all_files_iter: (string -> unit) -> unit +val insert_local_declaration: storage -> ident -> typ -> location -> unit +val atom_local_variable: ident -> atom -> unit +val enter_scope: int -> int -> int -> unit +val enter_function_scope: int -> int -> unit +val add_lvar_scope: int -> ident -> int -> unit +val open_scope: atom -> int -> positive -> unit +val close_scope: atom -> int -> positive -> unit +val start_live_range: atom -> positive -> (int * int builtin_arg) -> unit +val end_live_range: atom -> positive -> unit +val stack_variable: atom -> int * int builtin_arg -> unit +val function_end: atom -> positive -> unit +val add_label: atom -> positive -> int -> unit +val generate_debug_info: (atom -> string) -> string -> debug_entries option +val atom_parameter: ident -> ident -> atom -> unit +val add_compilation_section_start: string -> (int * int * int * string) -> unit +val compute_file_enum: (string -> int) -> (string-> int) -> (unit -> unit) -> unit +val exists_section: string -> bool diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml new file mode 100644 index 00000000..382845a4 --- /dev/null +++ b/debug/DebugInformation.ml @@ -0,0 +1,821 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open AST +open BinNums +open C +open Camlcoq +open Cutil + +(* This implements an interface for the collection of debugging + information. *) + +(* Simple id generator *) +let id = ref 0 + +let next_id () = + let nid = !id in + incr id; nid + +let reset_id () = + id := 0 + +(* Auximilary functions *) +let list_replace c f l = + List.map (fun a -> if c a then f a else a) l + +(* The name of the current compilation unit *) +let file_name: string ref = ref "" + +(** All files used in the debug entries *) +module StringSet = Set.Make(String) +let all_files : StringSet.t ref = ref StringSet.empty +let add_file file = + all_files := StringSet.add file !all_files + +(* Types for the information of type info *) +type composite_field = + { + cfd_name: string; + cfd_typ: int; + cfd_bit_size: int option; + cfd_bit_offset: int option; + cfd_byte_offset: int option; + cfd_byte_size: int option; + cfd_bitfield: string option; + } + +type composite_type = + { + ct_name: string; + ct_sou: struct_or_union; + ct_file_loc: location option; + ct_members: composite_field list; + ct_sizeof: int option; + ct_declaration: bool; + } + +type ptr_type = { + pts: int + } + +type const_type = { + cst_type: int + } + +type volatile_type = { + vol_type: int + } + + +type array_type = { + arr_type: int; + arr_size: int64 option list; + } + +type typedef = { + typedef_file_loc: location option; + typedef_name: string; + typ: int option; + } + +type enumerator = { + enumerator_name: string; + enumerator_const: int64; + } + +type enum_type = { + enum_name: string; + enum_byte_size: int option; + enum_file_loc: location option; + enum_enumerators: enumerator list; + } + +type int_type = { + int_kind: ikind; + } + +type float_type = { + float_kind: fkind; + } + +type parameter_type = { + param_type: int; + param_name: string; + } + +type function_type = { + fun_return_type: int option; + fun_prototyped: bool; + fun_params: parameter_type list; + } + +type debug_types = + | IntegerType of int_type + | FloatType of float_type + | PointerType of ptr_type + | ArrayType of array_type + | CompositeType of composite_type + | EnumType of enum_type + | FunctionType of function_type + | Typedef of typedef + | ConstType of const_type + | VolatileType of volatile_type + | Void + +(* All types encountered *) +let types: (int,debug_types) Hashtbl.t = Hashtbl.create 7 + +(* Lookup table for types *) +let lookup_types: (string, int) Hashtbl.t = Hashtbl.create 7 + +(* Translate a C.typ to a string needed for hashing *) +let typ_to_string (ty: typ) = + let buf = Buffer.create 7 in + let chan = Format.formatter_of_buffer buf in + Cprint.print_debug_idents := true; + Cprint.typ chan ty; + Cprint.print_debug_idents := false; + Format.pp_print_flush chan (); + Buffer.contents buf + +(* Helper functions for the attributes *) +let strip_attributes typ = + let strip = List.filter (fun a -> a = AConst || a = AVolatile) in + match typ with + | TVoid at -> TVoid (strip at) + | TInt (k,at) -> TInt (k,strip at) + | TFloat (k,at) -> TFloat(k,strip at) + | TPtr (t,at) -> TPtr(t,strip at) + | TArray (t,s,at) -> TArray(t,s,strip at) + | TFun (t,arg,v,at) -> TFun(t,arg,v,strip at) + | TNamed (n,at) -> TNamed(n,strip at) + | TStruct (n,at) -> TStruct(n,strip at) + | TUnion (n,at) -> TUnion(n,strip at) + | TEnum (n,at) -> TEnum(n,strip at) + +let strip_last_attribute typ = + let rec hd_opt l = match l with + [] -> None,[] + | AConst::rest -> Some AConst,rest + | AVolatile::rest -> Some AVolatile,rest + | _::rest -> hd_opt rest in + match typ with + | TVoid at -> let l,r = hd_opt at in + l,TVoid r + | TInt (k,at) -> let l,r = hd_opt at in + l,TInt (k,r) + | TFloat (k,at) -> let l,r = hd_opt at in + l,TFloat (k,r) + | TPtr (t,at) -> let l,r = hd_opt at in + l,TPtr(t,r) + | TArray (t,s,at) -> let l,r = hd_opt at in + l,TArray(t,s,r) + | TFun (t,arg,v,at) -> let l,r = hd_opt at in + l,TFun(t,arg,v,r) + | TNamed (n,at) -> let l,r = hd_opt at in + l,TNamed(n,r) + | TStruct (n,at) -> let l,r = hd_opt at in + l,TStruct(n,r) + | TUnion (n,at) -> let l,r = hd_opt at in + l,TUnion(n,r) + | TEnum (n,at) -> let l,r = hd_opt at in + l,TEnum(n,r) + +(* Does the type already exist? *) +let exist_type (ty: typ) = + (* We are only interrested in Const and Volatile *) + let ty = strip_attributes ty in + Hashtbl.mem lookup_types (typ_to_string ty) + +(* Find the type id to an type *) +let find_type (ty: typ) = + (* We are only interrested in Const and Volatile *) + let ty = strip_attributes ty in + Hashtbl.find lookup_types (typ_to_string ty) + +(* Add type and information *) +let insert_type (ty: typ) = + let insert d_ty ty = + let id = next_id () + and name = typ_to_string ty in + Hashtbl.add types id d_ty; + Hashtbl.add lookup_types name id; + id in + (* We are only interrested in Const and Volatile *) + let ty = strip_attributes ty in + let rec typ_aux ty = + try find_type ty with + | Not_found -> + let d_ty = + match ty with + | TVoid _ -> Void + | TInt (k,_) -> + IntegerType ({int_kind = k }) + | TFloat (k,_) -> + FloatType ({float_kind = k}) + | TPtr (t,_) -> + let id = attr_aux t in + PointerType ({pts = id}) + | TArray (t,s,_) -> + let rec size acc t = (match t with + | TArray (child,s,_) -> + size (s::acc) child + | _ -> t,List.rev acc) in + let t,s = size [s] t in + let id = attr_aux t in + let arr = { + arr_type = id; + arr_size= s; + } in + ArrayType arr + | TFun (t,param,va,_) -> + let param,prot = (match param with + | None -> [],false + | Some p -> List.map (fun (i,t) -> let t = attr_aux t in + { + param_type = t; + param_name = i.name; + }) p,true) in + let ret = (match t with + | TVoid _ -> None + | _ -> Some (attr_aux t)) in + let ftype = { + fun_return_type = ret; + fun_prototyped = prot; + fun_params = param; + } in + FunctionType ftype + | TNamed (id,_) -> + let typ = try + let _,t = + List.find (fun a -> fst a = id.name) CBuiltins.builtins.Builtins.typedefs in + Some (attr_aux t) + with Not_found -> None in + let t = { + typedef_file_loc = None; + typedef_name = id.name; + typ = typ; + } in + Typedef t + | TStruct (id,_) -> + let str = + { + ct_name = id.name; + ct_sou = Struct; + ct_file_loc = None; + ct_members = []; + ct_declaration = false; + ct_sizeof = None; + } in + CompositeType str + | TUnion (id,_) -> + let union = + { + ct_name = id.name; + ct_sou = Union; + ct_file_loc = None; + ct_members = []; + ct_declaration = false; + ct_sizeof = None; + } in + CompositeType union + | TEnum (id,_) -> + let enum = + { + enum_name = id.name; + enum_byte_size = None; + enum_file_loc = None; + enum_enumerators = []; + } in + EnumType enum in + insert d_ty ty + and attr_aux ty = + try + find_type ty + with + Not_found -> + match strip_last_attribute ty with + | Some AConst,t -> + let id = attr_aux t in + let const = { cst_type = id} in + insert (ConstType const) ty + | Some AVolatile,t -> + let id = attr_aux t in + let volatile = {vol_type = id} in + insert (VolatileType volatile) ty + | Some (ARestrict|AAlignas _| Attr(_,_)),t -> + attr_aux t + | None,t -> typ_aux t + in + attr_aux ty + +(* Replace the composite information *) +let replace_composite id f = + let str = Hashtbl.find types id in + match str with + | CompositeType comp -> let comp' = f comp in + if comp <> comp' then Hashtbl.replace types id (CompositeType comp') + | _ -> assert false (* This should never happen *) + +(* Replace the enum information *) +let replace_enum id f = + let str = Hashtbl.find types id in + match str with + | EnumType comp -> let comp' = f comp in + if comp <> comp' then Hashtbl.replace types id (EnumType comp') + | _ -> assert false (* This should never happen *) + +(* Replace the typdef information *) +let replace_typedef id f = + let typdef = Hashtbl.find types id in + match typdef with + | Typedef typ -> let typ' = f typ in + if typ <> typ' then Hashtbl.replace types id (Typedef typ') + | _ -> assert false (* This should never happen *) + +(* Types for global definitions *) + +(* Information for a global variable *) +type global_variable_information = { + gvar_name: string; + gvar_atom: atom option; + gvar_file_loc: location; + gvar_declaration: bool; + gvar_external: bool; + gvar_type: int; + } + +type parameter_information = + { + parameter_name: string; + parameter_ident: int; + parameter_atom: atom option; + parameter_type: int; +} + +type function_information = { + fun_name: string; + fun_atom: atom option; + fun_file_loc: location; + fun_external: bool; + fun_return_type: int option; (* Again the special case of void functions *) + fun_vararg: bool; + fun_parameter: parameter_information list; + fun_low_pc: int option; + fun_high_pc: int option; + fun_scope: int option; + } + +type definition_type = + | GlobalVariable of global_variable_information + | Function of function_information + + +(* All global definitions encountered *) +let definitions: (int,definition_type) Hashtbl.t = Hashtbl.create 7 + +(* Mapping from stamp to debug id *) +let stamp_to_definition: (int,int) Hashtbl.t = Hashtbl.create 7 + +(* Mapping from name to debug id *) +let name_to_definition: (string,int) Hashtbl.t = Hashtbl.create 7 + +(* Mapping from atom to debug id *) +let atom_to_definition: (atom, int) Hashtbl.t = Hashtbl.create 7 + +let find_gvar_stamp id = + let id = (Hashtbl.find stamp_to_definition id) in + let var = Hashtbl.find definitions id in + match var with + | GlobalVariable var -> id,var + | _ -> assert false + +let find_fun_stamp id = + let id = (Hashtbl.find stamp_to_definition id) in + let f = Hashtbl.find definitions id in + match f with + | Function f -> id,f + | _ -> assert false + +let find_fun_atom id = + let id = (Hashtbl.find atom_to_definition id) in + let f = Hashtbl.find definitions id in + match f with + | Function f -> id,f + | _ -> assert false + +let replace_var id var = + let var = GlobalVariable var in + Hashtbl.replace definitions id var + +let replace_fun id f = + let f = Function f in + Hashtbl.replace definitions id f + + +(* Information for local variables *) +type local_variable_information = { + lvar_name: string; + lvar_atom: atom option; + lvar_file_loc:location; + lvar_type: int; + lvar_static: bool; (* Static variable are mapped to symbols *) + } + +type scope_information = + { + scope_variables: int list; (* Variable and Scope ids *) + } + +type local_information = + | LocalVariable of local_variable_information + | Scope of scope_information + +(* All local variables *) +let local_variables: (int, local_information) Hashtbl.t = Hashtbl.create 7 + +(* Mapping from stampt to the debug id of the local variable *) +let stamp_to_local: (int,int) Hashtbl.t = Hashtbl.create 7 + +(* Mapping form atom to the debug id of the local variable *) +let atom_to_local: (atom, int) Hashtbl.t = Hashtbl.create 7 + +(* Map from scope id + function id to debug id *) +let scope_to_local: (int * int,int) Hashtbl.t = Hashtbl.create 7 + +(* Map from scope id + function atom to debug id *) +let atom_to_scope: (atom * int, int) Hashtbl.t = Hashtbl.create 7 + +let find_lvar_stamp id = + let id = (Hashtbl.find stamp_to_local id) in + let v = Hashtbl.find local_variables id in + match v with + | LocalVariable v -> id,v + | _ -> assert false + +let replace_lvar id var = + let var = LocalVariable var in + Hashtbl.replace local_variables id var + +let find_scope_id fid id = + let id = Hashtbl.find scope_to_local (fid,id) in + let v = Hashtbl.find local_variables id in + match v with + | Scope v -> id,v + | _ -> assert false + +let replace_scope id var = + let var = Scope var in + Hashtbl.replace local_variables id var + +let gen_comp_typ sou id at = + if sou = Struct then + TStruct (id,at) + else + TUnion (id,at) + +let insert_global_declaration env dec= + add_file (fst dec.gloc); + let insert d_dec stamp = + let id = next_id () in + Hashtbl.add definitions id d_dec; + Hashtbl.add stamp_to_definition stamp id + in + match dec.gdesc with + | Gdecl (sto,id,ty,init) -> + if not (is_function_type env ty) then begin + if not (Hashtbl.mem stamp_to_definition id.stamp) then begin + let at_decl,ext = (match sto with + | Storage_extern -> init = None,true + | Storage_static -> false,false + | _ -> false,true) in + let ty = insert_type ty in + let decl = { + gvar_name = id.name; + gvar_atom = None; + gvar_file_loc = dec.gloc; + gvar_declaration = at_decl; + gvar_external = ext; + gvar_type = ty; + } in + insert (GlobalVariable decl) id.stamp + end else if init <> None || sto <> Storage_extern then begin (* It is a definition *) + let id,var = find_gvar_stamp id.stamp in + replace_var id ({var with gvar_declaration = false;}) + end + end else if not (Hashtbl.mem name_to_definition id.name) then begin + (* Implict declarations need special handling *) + let id' = next_id () in + Hashtbl.add stamp_to_definition id.stamp id'; + Hashtbl.add name_to_definition id.name id' + end + | Gfundef f -> + let ret = (match f.fd_ret with + | TVoid _ -> None + | _ -> Some (insert_type f.fd_ret)) in + let ext = (match f.fd_storage with + | Storage_static -> false + | _ -> true) in + let params = List.map (fun (p,ty) -> + let ty = insert_type ty in + { + parameter_name = p.name; + parameter_ident = p.stamp; + parameter_atom = None; + parameter_type = ty; + }) f.fd_params in + let fd = + { + fun_name = f.fd_name.name; + fun_atom = None; + fun_file_loc = dec.gloc; + fun_external = ext; + fun_return_type = ret; + fun_vararg = f.fd_vararg; + fun_parameter = params; + fun_low_pc = None; + fun_high_pc = None; + fun_scope = None; + } in + begin try + let id' = Hashtbl.find name_to_definition f.fd_name.name in + Hashtbl.add stamp_to_definition f.fd_name.stamp id'; + Hashtbl.add definitions id' (Function fd) + with Not_found -> + insert (Function fd) f.fd_name.stamp + end + | Gcompositedecl (sou,id,at) -> + ignore (insert_type (gen_comp_typ sou id at)); + let id = find_type (gen_comp_typ sou id []) in + replace_composite id (fun comp -> if comp.ct_file_loc = None then + {comp with ct_file_loc = Some (dec.gloc);} + else comp) + | Gcompositedef (sou,id,at,fi) -> + ignore (insert_type (gen_comp_typ sou id at)); + let id = find_type (gen_comp_typ sou id []) in + let fi = List.filter (fun f -> f.fld_name <> "") fi in (* Fields without names need no info *) + let fields = List.map (fun f -> + { + cfd_name = f.fld_name; + cfd_typ = insert_type f.fld_typ; + cfd_bit_size = f.fld_bitfield; + cfd_bit_offset = None; + cfd_byte_offset = None; + cfd_byte_size = None; + cfd_bitfield = None; + }) fi in + replace_composite id (fun comp -> + let loc = if comp.ct_file_loc = None then Some dec.gloc else comp.ct_file_loc in + {comp with ct_file_loc = loc; ct_members = fields; ct_declaration = true;}) + | Gtypedef (id,t) -> + let id = insert_type (TNamed (id,[])) in + let tid = insert_type t in + replace_typedef id (fun typ -> {typ with typedef_file_loc = Some dec.gloc; typ = Some tid;}); + | Genumdef (n,at,e) -> + ignore(insert_type (TEnum (n,at))); + let id = find_type (TEnum (n,[])) in + let enumerator = List.map (fun (i,c,_) -> + { + enumerator_name = i.name; + enumerator_const = c; + }) e in + replace_enum id (fun en -> + {en with enum_file_loc = Some dec.gloc; enum_enumerators = enumerator;}) + | Gpragma _ -> () + +let set_member_offset str field offset = + let id = find_type (TStruct (str,[])) in + replace_composite id (fun comp -> + let name f = f.cfd_name = field || match f.cfd_bitfield with Some n -> n = field | _ -> false in + let members = list_replace name (fun a -> {a with cfd_byte_offset = Some offset;}) comp.ct_members in + {comp with ct_members = members;}) + +let set_composite_size comp sou size = + let id = find_type (gen_comp_typ sou comp []) in + replace_composite id (fun comp -> {comp with ct_sizeof = size;}) + +let set_bitfield_offset str field offset underlying size = + let id = find_type (TStruct (str,[])) in + replace_composite id (fun comp -> + let name f = f.cfd_name = field in + let members = list_replace name (fun a -> + {a with cfd_bit_offset = Some offset; cfd_bitfield = Some underlying; cfd_byte_size = Some size}) + comp.ct_members in + {comp with ct_members = members;}) + +let atom_global_variable id atom = + try + let id,var = find_gvar_stamp id.stamp in + replace_var id ({var with gvar_atom = Some atom;}); + Hashtbl.add atom_to_definition atom id + with Not_found -> () + +let atom_function id atom = + try + let id',f = find_fun_stamp id.stamp in + replace_fun id' ({f with fun_atom = Some atom;}); + Hashtbl.add atom_to_definition atom id'; + Hashtbl.iter (fun (fid,sid) tid -> if fid = id.stamp then + Hashtbl.add atom_to_scope (atom,sid) tid) scope_to_local + with Not_found -> () + +let atom_parameter fid id atom = + try + let fid',f = find_fun_stamp fid.stamp in + let name p = p.parameter_ident = id.stamp in + let params = list_replace name (fun p -> {p with parameter_atom = Some atom;}) f.fun_parameter in + replace_fun fid' ({f with fun_parameter = params;}) + with Not_found -> () + +let add_fun_addr atom (high,low) = + try + let id,f = find_fun_atom atom in + replace_fun id ({f with fun_high_pc = Some high; fun_low_pc = Some low;}) + with Not_found -> () + +let atom_local_variable id atom = + try + let id,var = find_lvar_stamp id.stamp in + replace_lvar id ({var with lvar_atom = Some atom;}); + Hashtbl.add atom_to_local atom id + with Not_found -> () + +let add_lvar_scope f_id var_id s_id = + try + let s_id',scope = find_scope_id f_id s_id in + let var_id,_ = find_lvar_stamp var_id.stamp in + replace_scope s_id' ({scope_variables = var_id::scope.scope_variables;}) + with Not_found -> () + +let insert_local_declaration sto id ty loc = + let ty = insert_type ty in + let var = { + lvar_name = id.name; + lvar_atom = None; + lvar_file_loc = loc; + lvar_type = ty; + lvar_static = sto = Storage_static; + } in + let id' = next_id () in + Hashtbl.add local_variables id' (LocalVariable var); + Hashtbl.add stamp_to_local id.stamp id' + +let new_scope f_id sc_id = + let scope = {scope_variables = [];} in + let id = next_id () in + Hashtbl.add local_variables id (Scope scope); + Hashtbl.add scope_to_local (f_id,sc_id) id; + id + +let enter_function_scope fun_id sc_id = + try + let id = new_scope fun_id sc_id in + let fun_id,f = find_fun_stamp fun_id in + replace_fun fun_id ({f with fun_scope = Some id}) + with Not_found -> () + +let enter_scope f_id p_id id = + try + let id' = new_scope f_id id in + let p_id',scope = find_scope_id f_id p_id in + replace_scope p_id' ({scope_variables = id'::scope.scope_variables;}) + with Not_found -> () + + +type scope_range = + { + start_addr: positive option; + end_addr: positive option; + } + +type var_range = + { + range_start: positive option; + range_end: positive option; + var_loc: int * int builtin_arg; + } + +type var_location = + | RangeLoc of var_range list + | FunctionLoc of int * int builtin_arg (* Stack allocated variables *) + +let var_locations: (atom,var_location) Hashtbl.t = Hashtbl.create 7 + +let scope_ranges: (int,scope_range list) Hashtbl.t = Hashtbl.create 7 + +let label_translation: (atom * positive, int) Hashtbl.t = Hashtbl.create 7 + +let add_label atom p i = + Hashtbl.add label_translation (atom,p) i + +(* Auxiliary data structures and functions *) +module IntSet = Set.Make(struct + type t = int + let compare (x:int) (y:int) = compare x y +end) + +let open_scopes: IntSet.t ref = ref IntSet.empty +let open_vars: atom list ref = ref [] + +let open_scope atom s_id lbl = + try + let s_id = Hashtbl.find atom_to_scope (atom,s_id) in + let old_r = try Hashtbl.find scope_ranges s_id with Not_found -> [] in + let n_scop = { start_addr = Some lbl; end_addr = None;} in + open_scopes := IntSet.add s_id !open_scopes; + Hashtbl.replace scope_ranges s_id (n_scop::old_r) + with Not_found -> () + +let close_scope atom s_id lbl = + try + let s_id = Hashtbl.find atom_to_scope (atom,s_id) in + let old_r = try Hashtbl.find scope_ranges s_id with Not_found -> [] in + let last_r,rest = + begin + match old_r with + | a::rest -> a,rest + | _ -> assert false (* We must have an opening scope *) + end in + let new_r = ({last_r with end_addr = Some lbl;})::rest in + open_scopes := IntSet.remove s_id !open_scopes; + Hashtbl.replace scope_ranges s_id new_r + with Not_found -> () + +let start_live_range atom lbl loc = + let old_r = begin try Hashtbl.find var_locations atom with Not_found -> (RangeLoc []) end in + match old_r with + | RangeLoc old_r -> + let n_r = { range_start = Some lbl; range_end = None; var_loc = loc } in + open_vars := atom::!open_vars; + Hashtbl.replace var_locations atom (RangeLoc (n_r::old_r)) + | _ -> () (* Parameter that is passed as variable *) + +let end_live_range atom lbl = + try + let old_r = Hashtbl.find var_locations atom in + match old_r with + | RangeLoc (n_r::old_r) -> + if n_r.range_end = None then (* We can skip non open locations *) + let n_r = {n_r with range_end = Some lbl} in + Hashtbl.replace var_locations atom (RangeLoc (n_r::old_r)) + | _ -> () + with Not_found -> () + +let stack_variable atom (sp,loc) = + Hashtbl.add var_locations atom (FunctionLoc (sp,loc)) + +let function_end atom loc = + IntSet.iter (fun id -> close_scope atom id loc) !open_scopes; + open_scopes := IntSet.empty; + List.iter (fun atom -> end_live_range atom loc) !open_vars; + open_vars:= [] + +let compilation_section_start: (string,int * int * int * string) Hashtbl.t = Hashtbl.create 7 +let compilation_section_end: (string,int) Hashtbl.t = Hashtbl.create 7 + +let add_compilation_section_start sec addr = + Hashtbl.add compilation_section_start sec addr + +let add_compilation_section_end sec addr = + Hashtbl.add compilation_section_end sec addr + +let exists_section sec = + Hashtbl.mem compilation_section_start sec + +let filenum: (string * string,int) Hashtbl.t = Hashtbl.create 7 + +let compute_file_enum end_label entry_label line_end = + Hashtbl.iter (fun sec (_,_,_,secname) -> + Hashtbl.add compilation_section_end sec (end_label secname); + StringSet.iter (fun file -> + let lbl = entry_label file in + Hashtbl.add filenum (sec,file) lbl) !all_files; + line_end ()) compilation_section_start + +let init name = + id := 0; + file_name := name; + Hashtbl.reset types; + Hashtbl.reset lookup_types; + Hashtbl.reset definitions; + Hashtbl.reset stamp_to_definition; + Hashtbl.reset name_to_definition; + Hashtbl.reset atom_to_definition; + Hashtbl.reset local_variables; + Hashtbl.reset stamp_to_local; + Hashtbl.reset atom_to_local; + Hashtbl.reset scope_to_local; + Hashtbl.reset compilation_section_start; + Hashtbl.reset compilation_section_end; + Hashtbl.reset filenum; + all_files := StringSet.empty diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml new file mode 100644 index 00000000..6a50b020 --- /dev/null +++ b/debug/DebugInit.ml @@ -0,0 +1,80 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open AST +open BinNums +open C +open Camlcoq +open Dwarfgen +open DwarfTypes +open Debug + +let init_debug () = + implem.init <- DebugInformation.init; + implem.atom_function <- DebugInformation.atom_function; + implem.atom_global_variable <- DebugInformation.atom_global_variable; + implem.set_composite_size <- DebugInformation.set_composite_size; + implem.set_member_offset <- DebugInformation.set_member_offset; + implem.set_bitfield_offset <- DebugInformation.set_bitfield_offset; + implem.insert_global_declaration <- DebugInformation.insert_global_declaration; + implem.add_fun_addr <- DebugInformation.add_fun_addr; + implem.generate_debug_info <- (fun a b -> Some (Dwarfgen.gen_debug_info a b)); + implem.all_files_iter <- (fun f -> DebugInformation.StringSet.iter f !DebugInformation.all_files); + implem.insert_local_declaration <- DebugInformation.insert_local_declaration; + implem.atom_local_variable <- DebugInformation.atom_local_variable; + implem.enter_scope <- DebugInformation.enter_scope; + implem.enter_function_scope <- DebugInformation.enter_function_scope; + implem.add_lvar_scope <- DebugInformation.add_lvar_scope; + implem.open_scope <- DebugInformation.open_scope; + implem.close_scope <- DebugInformation.close_scope; + implem.start_live_range <- DebugInformation.start_live_range; + implem.end_live_range <- DebugInformation.end_live_range; + implem.stack_variable <- DebugInformation.stack_variable; + implem.function_end <- DebugInformation.function_end; + implem.add_label <- DebugInformation.add_label; + implem.atom_parameter <- DebugInformation.atom_parameter; + implem.add_compilation_section_start <- DebugInformation.add_compilation_section_start; + implem.compute_file_enum <- DebugInformation.compute_file_enum; + implem.exists_section <- DebugInformation.exists_section + +let init_none () = + implem.init <- (fun _ -> ()); + implem.atom_function <- (fun _ _ -> ()); + implem.atom_global_variable <- (fun _ _ -> ()); + implem.set_composite_size <- (fun _ _ _ -> ()); + implem.set_member_offset <- (fun _ _ _ -> ()); + implem.set_bitfield_offset <- (fun _ _ _ _ _ -> ()); + implem.insert_global_declaration <- (fun _ _ -> ()); + implem.add_fun_addr <- (fun _ _ -> ()); + implem.generate_debug_info <- (fun _ _ -> None); + implem.all_files_iter <- (fun _ -> ()); + implem.insert_local_declaration <- (fun _ _ _ _ -> ()); + implem.atom_local_variable <- (fun _ _ -> ()); + implem.enter_scope <- (fun _ _ _ -> ()); + implem.enter_function_scope <- (fun _ _ -> ()); + implem.add_lvar_scope <- (fun _ _ _ -> ()); + implem.open_scope <- (fun _ _ _ -> ()); + implem.close_scope <- (fun _ _ _ -> ()); + implem.start_live_range <- (fun _ _ _ -> ()); + implem.end_live_range <- (fun _ _ -> ()); + implem.stack_variable <- (fun _ _ -> ()); + implem.function_end <- (fun _ _ -> ()); + implem.add_label <- (fun _ _ _ -> ()); + implem.atom_parameter <- (fun _ _ _ -> ()); + implem.add_compilation_section_start <- (fun _ _ -> ()); + implem.exists_section <- (fun _ -> true) + +let init () = + if !Clflags.option_g && Configuration.advanced_debug then + init_debug () + else + init_none () diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index 15843eb9..a95c71a1 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -19,14 +19,13 @@ open PrintAsmaux open Sections (* The printer is parameterized over target specific functions and a set of dwarf type constants *) -module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): +module DwarfPrinter(Target: DWARF_TARGET): sig - val print_debug: out_channel -> dw_entry -> unit + val print_debug: out_channel -> debug_entries -> unit end = struct open Target - open DwarfAbbrevs (* Byte value to string *) let string_of_byte value = @@ -36,6 +35,10 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let print_label oc lbl = fprintf oc "%a:\n" label lbl + (* Print a positive label *) + let print_plabel oc lbl = + print_label oc (transl_label lbl) + (* Helper functions for abbreviation printing *) let add_byte buf value = Buffer.add_string buf (string_of_byte value) @@ -64,18 +67,15 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let add_low_pc = add_abbr_entry (0x11,low_pc_type_abbr) - let add_fun_pc sp buf = - match get_fun_addr sp.subprogram_name with - | None ->() - | Some (a,b) -> add_high_pc buf; add_low_pc buf - let add_declaration = add_abbr_entry (0x3c,declaration_type_abbr) let add_location loc buf = match loc with | None -> () - | Some (LocConst _) -> add_abbr_entry (0x2,location_const_type_abbr) buf - | Some (LocBlock _) -> add_abbr_entry (0x2,location_block_type_abbr) buf + | Some (LocRef _) -> add_abbr_entry (0x2,location_ref_type_abbr) buf + | Some (LocList _ ) + | Some (LocSymbol _) + | Some (LocSimple _) -> add_abbr_entry (0x2,location_block_type_abbr) buf (* Dwarf entity to string function *) let abbrev_string_of_entity entity has_sibling = @@ -105,8 +105,8 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): | DW_TAG_compile_unit e -> prologue 0x11; add_abbr_entry (0x1b,comp_dir_type_abbr) buf; - add_high_pc buf; add_low_pc buf; + add_high_pc buf; add_abbr_entry (0x13,language_type_abbr) buf; add_name buf; add_abbr_entry (0x25,producer_type_abbr) buf; @@ -129,32 +129,31 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): prologue 0x5; add_attr_some e.formal_parameter_file_loc add_file_loc; add_attr_some e.formal_parameter_artificial (add_abbr_entry (0x34,artificial_type_abbr)); - add_location e.formal_parameter_location buf; add_attr_some e.formal_parameter_name add_name; - add_location e.formal_parameter_segment buf; add_type buf; - add_attr_some e.formal_parameter_variable_parameter (add_abbr_entry (0x4b,variable_parameter_type_abbr)) + add_attr_some e.formal_parameter_variable_parameter (add_abbr_entry (0x4b,variable_parameter_type_abbr)); + add_location e.formal_parameter_location buf | DW_TAG_label _ -> prologue 0xa; add_low_pc buf; add_name buf; - | DW_TAG_lexical_block _ -> + | DW_TAG_lexical_block a -> prologue 0xb; - add_high_pc buf; - add_low_pc buf + add_attr_some a.lexical_block_high_pc add_high_pc; + add_attr_some a.lexical_block_low_pc add_low_pc | DW_TAG_member e -> prologue 0xd; add_attr_some e.member_file_loc add_file_loc; - add_attr_some e.member_byte_size add_member_size; - add_attr_some e.member_bit_offset (add_abbr_entry (0xd,bit_offset_type_abbr)); - add_attr_some e.member_bit_size (add_abbr_entry (0xc,bit_size_type_abbr)); + add_attr_some e.member_byte_size add_byte_size; + add_attr_some e.member_bit_offset (add_abbr_entry (0xc,bit_offset_type_abbr)); + add_attr_some e.member_bit_size (add_abbr_entry (0xd,bit_size_type_abbr)); + add_attr_some e.member_declaration add_declaration; + add_attr_some e.member_name add_name; + add_type buf; (match e.member_data_member_location with | None -> () | Some (DataLocBlock __) -> add_abbr_entry (0x38,data_location_block_type_abbr) buf - | Some (DataLocRef _) -> add_abbr_entry (0x38,data_location_ref_type_abbr) buf); - add_attr_some e.member_declaration add_declaration; - add_attr_some e.member_name add_name; - add_type buf + | Some (DataLocRef _) -> add_abbr_entry (0x38,data_location_ref_type_abbr) buf) | DW_TAG_pointer_type _ -> prologue 0xf; add_type buf @@ -166,9 +165,10 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): add_attr_some e.structure_name add_name | DW_TAG_subprogram e -> prologue 0x2e; - add_attr_some e.subprogram_file_loc add_file_loc; + add_file_loc buf; add_attr_some e.subprogram_external (add_abbr_entry (0x3f,external_type_abbr)); - add_fun_pc e buf; + add_attr_some e.subprogram_high_pc add_high_pc; + add_attr_some e.subprogram_low_pc add_low_pc; add_name buf; add_abbr_entry (0x27,prototyped_type_abbr) buf; add_attr_some e.subprogram_type add_type; @@ -200,12 +200,11 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): add_attr_some e.unspecified_parameter_artificial (add_abbr_entry (0x34,artificial_type_abbr)) | DW_TAG_variable e -> prologue 0x34; - add_attr_some e.variable_file_loc add_file_loc; + add_file_loc buf; add_attr_some e.variable_declaration add_declaration; add_attr_some e.variable_external (add_abbr_entry (0x3f,external_type_abbr)); add_location e.variable_location buf; add_name buf; - add_location e.variable_segment buf; add_type buf | DW_TAG_volatile_type _ -> prologue 0x35; @@ -246,7 +245,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let print_abbrev oc = let abbrevs = Hashtbl.fold (fun s i acc -> (s,i)::acc) abbrev_mapping [] in let abbrevs = List.sort (fun (_,a) (_,b) -> Pervasives.compare a b) abbrevs in - fprintf oc " .section %s\n" (name_of_section Section_debug_abbrev); + section oc Section_debug_abbrev; let lbl = new_label () in abbrev_start_addr := lbl; print_label oc lbl; @@ -276,9 +275,6 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): | None -> () | Some o -> f oc o - let print_file_loc oc f = - print_opt_value oc f print_file_loc - let print_flag oc b = output_string oc (string_of_byte b) @@ -294,16 +290,74 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let print_byte oc b = fprintf oc " .byte 0x%X\n" b - let print_loc oc loc = - () - - let print_data_location oc dl = - () + let print_2byte oc b = + fprintf oc " .2byte 0x%X\n" b let print_ref oc r = let ref = entry_to_label r in fprintf oc " .4byte %a\n" label ref + let print_file_loc oc = function + | Some (file,col) -> + fprintf oc " .4byte %a\n" label file; + print_uleb128 oc col + | None -> () + + let print_loc_expr oc = function + | DW_OP_bregx (a,b) -> + print_byte oc dw_op_bregx; + print_uleb128 oc a; + fprintf oc " .sleb128 %ld\n" b + | DW_OP_plus_uconst i -> + print_byte oc dw_op_plus_uconst; + print_uleb128 oc i + | DW_OP_piece i -> + print_byte oc dw_op_piece; + print_uleb128 oc i + | DW_OP_reg i -> + if i < 32 then + print_byte oc (dw_op_reg0 + i) + else begin + print_byte oc dw_op_regx; + print_uleb128 oc i + end + + let print_loc oc loc = + match loc with + | LocSymbol s -> + print_sleb128 oc 5; + print_byte oc dw_op_addr; + fprintf oc " .4byte %a\n" symbol s + | LocSimple e -> + print_sleb128 oc (size_of_loc_expr e); + print_loc_expr oc e + | LocList e -> + let size = List.fold_left (fun acc a -> acc + size_of_loc_expr a) 0 e in + print_sleb128 oc size; + List.iter (print_loc_expr oc) e + | LocRef f -> print_ref oc f + + let print_list_loc oc = function + | LocSymbol s -> + print_2byte oc 5; + print_byte oc dw_op_addr; + fprintf oc " .4byte %a\n" symbol s + | LocSimple e -> + print_2byte oc (size_of_loc_expr e); + print_loc_expr oc e + | LocList e -> + let size = List.fold_left (fun acc a -> acc + size_of_loc_expr a) 0 e in + print_2byte oc size; + List.iter (print_loc_expr oc) e + | LocRef f -> print_ref oc f + + let print_data_location oc dl = + match dl with + | DataLocBlock e -> + print_sleb128 oc (size_of_loc_expr e); + print_loc_expr oc e + | _ -> () + let print_addr oc a = fprintf oc " .4byte %a\n" label a @@ -336,12 +390,12 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let print_compilation_unit oc tag = let prod_name = sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:%s" Version.version Configuration.arch in print_string oc (Sys.getcwd ()); - print_addr oc (get_end_addr ()); - print_addr oc (get_start_addr ()); + print_addr oc tag.compile_unit_low_pc; + print_addr oc tag.compile_unit_high_pc; print_uleb128 oc 1; print_string oc tag.compile_unit_name; print_string oc prod_name; - print_addr oc (get_stmt_list_addr ()) + print_addr oc tag.compile_unit_stmt_list let print_const_type oc ct = print_ref oc ct.const_type @@ -360,29 +414,30 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let print_formal_parameter oc fp = print_file_loc oc fp.formal_parameter_file_loc; print_opt_value oc fp.formal_parameter_artificial print_flag; - print_opt_value oc fp.formal_parameter_location print_loc; print_opt_value oc fp.formal_parameter_name print_string; - print_opt_value oc fp.formal_parameter_segment print_loc; print_ref oc fp.formal_parameter_type; - print_opt_value oc fp.formal_parameter_variable_parameter print_flag + print_opt_value oc fp.formal_parameter_variable_parameter print_flag; + print_opt_value oc fp.formal_parameter_location print_loc let print_tag_label oc tl = print_ref oc tl.label_low_pc; print_string oc tl.label_name + let print_lexical_block oc lb = - print_ref oc lb.lexical_block_high_pc; - print_ref oc lb.lexical_block_low_pc + print_opt_value oc lb.lexical_block_high_pc print_addr; + print_opt_value oc lb.lexical_block_low_pc print_addr let print_member oc mb = print_file_loc oc mb.member_file_loc; print_opt_value oc mb.member_byte_size print_byte; print_opt_value oc mb.member_bit_offset print_byte; print_opt_value oc mb.member_bit_size print_byte; - print_opt_value oc mb.member_data_member_location print_data_location; print_opt_value oc mb.member_declaration print_flag; print_opt_value oc mb.member_name print_string; - print_ref oc mb.member_type + print_ref oc mb.member_type; + print_opt_value oc mb.member_data_member_location print_data_location + let print_pointer oc pt = print_ref oc pt.pointer_type @@ -398,11 +453,10 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): fprintf oc " .4byte %a\n" label s let print_subprogram oc sp = - let addr = get_fun_addr sp.subprogram_name in - print_file_loc oc sp.subprogram_file_loc; + print_file_loc oc (Some sp.subprogram_file_loc); print_opt_value oc sp.subprogram_external print_flag; - print_opt_value oc sp.subprogram_frame_base print_loc; - print_opt_value oc addr print_subprogram_addr; + print_opt_value oc sp.subprogram_high_pc print_addr; + print_opt_value oc sp.subprogram_low_pc print_addr; print_string oc sp.subprogram_name; print_flag oc sp.subprogram_prototyped; print_opt_value oc sp.subprogram_type print_ref @@ -431,12 +485,11 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_opt_value oc up.unspecified_parameter_artificial print_flag let print_variable oc var = - print_file_loc oc var.variable_file_loc; + print_file_loc oc (Some var.variable_file_loc); print_opt_value oc var.variable_declaration print_flag; print_opt_value oc var.variable_external print_flag; print_opt_value oc var.variable_location print_loc; print_string oc var.variable_name; - print_opt_value oc var.variable_segment print_loc; print_ref oc var.variable_type let print_volatile_type oc vt = @@ -482,16 +535,15 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_sleb128 oc 0) entry (* Print the debug abbrev section *) - let print_debug_abbrev oc entry = - compute_abbrev entry; + let print_debug_abbrev oc entries = + List.iter (fun (_,_,e,_) -> compute_abbrev e) entries; print_abbrev oc (* Print the debug info section *) - let print_debug_info oc entry = - let debug_start = new_label () in - debug_start_addr:= debug_start; - fprintf oc" .section %s\n" (name_of_section Section_debug_info); - print_label oc debug_start; + let print_debug_info oc sec start entry = + debug_start_addr:= start; + section oc (Section_debug_info sec); + print_label oc start; let debug_length_start = new_label () (* Address used for length calculation *) and debug_end = new_label () in fprintf oc " .4byte %a-%a\n" label debug_end label debug_length_start; @@ -503,10 +555,24 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_sleb128 oc 0; print_label oc debug_end (* End of the debug section *) + let print_location_entry oc c_low l = + print_label oc (entry_to_label l.loc_id); + List.iter (fun (b,e,loc) -> + fprintf oc " .4byte %a-%a\n" label b label c_low; + fprintf oc " .4byte %a-%a\n" label e label c_low; + print_list_loc oc loc) l.loc; + fprintf oc " .4byte 0\n"; + fprintf oc " .4byte 0\n" + + let print_location_list oc (c_low,l) = + List.iter (print_location_entry oc c_low) l (* Print the debug info and abbrev section *) - let print_debug oc entry = - print_debug_abbrev oc entry; - print_debug_info oc entry + let print_debug oc entries = + print_debug_abbrev oc entries; + List.iter (fun (s,d,e,_) -> print_debug_info oc s d e) entries; + section oc Section_debug_loc; + List.iter (fun (_,_,_,l) -> print_location_list oc l) entries + end diff --git a/debug/DwarfPrinter.mli b/debug/DwarfPrinter.mli index 9e0e6693..e1e10601 100644 --- a/debug/DwarfPrinter.mli +++ b/debug/DwarfPrinter.mli @@ -12,7 +12,7 @@ open DwarfTypes -module DwarfPrinter: functor (Target: DWARF_TARGET) -> functor (DwarfAbbrevs: DWARF_ABBREVS) -> +module DwarfPrinter: functor (Target: DWARF_TARGET) -> sig - val print_debug: out_channel -> dw_entry -> unit + val print_debug: out_channel -> debug_entries -> unit end diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli index eaf07e1e..906b7cba 100644 --- a/debug/DwarfTypes.mli +++ b/debug/DwarfTypes.mli @@ -12,6 +12,8 @@ (* Types used for writing dwarf debug information *) +open BinNums +open Camlcoq open Sections (* Basic types for the value of attributes *) @@ -36,12 +38,20 @@ type address = int type block = string -type location_value = - | LocConst of constant - | LocBlock of block +type location_expression = + | DW_OP_plus_uconst of constant + | DW_OP_bregx of int * int32 + | DW_OP_piece of int + | DW_OP_reg of int +type location_value = + | LocSymbol of atom + | LocRef of address + | LocSimple of location_expression + | LocList of location_expression list + type data_location_value = - | DataLocBlock of block + | DataLocBlock of location_expression | DataLocRef of reference type bound_value = @@ -50,7 +60,7 @@ type bound_value = (* Types representing the attribute information per tag value *) -type file_loc = string * constant +type file_loc = int * constant type dw_tag_array_type = { @@ -67,7 +77,10 @@ type dw_tag_base_type = type dw_tag_compile_unit = { - compile_unit_name: string; + compile_unit_name: string; + compile_unit_low_pc: int; + compile_unit_high_pc: int; + compile_unit_stmt_list: int; } type dw_tag_const_type = @@ -94,11 +107,10 @@ type dw_tag_formal_parameter = { formal_parameter_file_loc: file_loc option; formal_parameter_artificial: flag option; - formal_parameter_location: location_value option; formal_parameter_name: string option; - formal_parameter_segment: location_value option; formal_parameter_type: reference; formal_parameter_variable_parameter: flag option; + formal_parameter_location: location_value option; } type dw_tag_label = @@ -109,8 +121,8 @@ type dw_tag_label = type dw_tag_lexical_block = { - lexical_block_high_pc: address; - lexical_block_low_pc: address; + lexical_block_high_pc: address option; + lexical_block_low_pc: address option; } type dw_tag_member = @@ -140,12 +152,13 @@ type dw_tag_structure_type = type dw_tag_subprogram = { - subprogram_file_loc: file_loc option; - subprogram_external: flag option; - subprogram_frame_base: location_value option; + subprogram_file_loc: file_loc; + subprogram_external: flag option; subprogram_name: string; subprogram_prototyped: flag; - subprogram_type: reference option; + subprogram_type: reference option; + subprogram_high_pc: reference option; + subprogram_low_pc: reference option; } type dw_tag_subrange_type = @@ -183,13 +196,12 @@ type dw_tag_unspecified_parameter = type dw_tag_variable = { - variable_file_loc: file_loc option; + variable_file_loc: file_loc; variable_declaration: flag option; variable_external: flag option; - variable_location: location_value option; variable_name: string; - variable_segment: location_value option; variable_type: reference; + variable_location: location_value option; } type dw_tag_volatile_type = @@ -228,46 +240,21 @@ type dw_entry = id: reference; } -(* Module type for a matching from type to dwarf encoding *) -module type DWARF_ABBREVS = - sig - val sibling_type_abbr: int - val file_loc_type_abbr: int * int - val type_abbr: int - val name_type_abbr: int - val encoding_type_abbr: int - val byte_size_type_abbr: int - val member_size_abbr: int - val high_pc_type_abbr: int - val low_pc_type_abbr: int - val stmt_list_type_abbr: int - val declaration_type_abbr: int - val external_type_abbr: int - val prototyped_type_abbr: int - val bit_offset_type_abbr: int - val comp_dir_type_abbr: int - val language_type_abbr: int - val producer_type_abbr: int - val value_type_abbr: int - val artificial_type_abbr: int - val variable_parameter_type_abbr: int - val bit_size_type_abbr: int - val location_const_type_abbr: int - val location_block_type_abbr: int - val data_location_block_type_abbr: int - val data_location_ref_type_abbr: int - val bound_const_type_abbr: int - val bound_ref_type_abbr: int - end +(* The type for the location list. *) +type location_entry = + { + loc: (int * int * location_value) list; + loc_id: reference; + } +type dw_locations = int * location_entry list + +type debug_entries = (string * int * dw_entry * dw_locations) list (* The target specific functions for printing the debug information *) module type DWARF_TARGET= sig val label: out_channel -> int -> unit val print_file_loc: out_channel -> file_loc -> unit - val get_start_addr: unit -> int - val get_end_addr: unit -> int - val get_stmt_list_addr: unit -> int - val name_of_section: section_name -> string - val get_fun_addr: string -> (int * int) option + val section: out_channel -> section_name -> unit + val symbol: out_channel -> atom -> unit end diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml index f47c2b58..16e446ee 100644 --- a/debug/DwarfUtil.ml +++ b/debug/DwarfUtil.ml @@ -14,18 +14,8 @@ open DwarfTypes -let id = ref 0 - -let next_id () = - let nid = !id in - incr id; nid - -let reset_id () = - id := 0 - (* Generate a new entry from a given tag *) -let new_entry tag = - let id = next_id () in +let new_entry id tag = { tag = tag; children = []; @@ -86,34 +76,67 @@ let dw_form_ref8 = 0x14 let dw_ref_udata = 0x15 let dw_ref_indirect = 0x16 +(* Operation encoding *) +let dw_op_addr = 0x3 +let dw_op_plus_uconst = 0x23 +let dw_op_reg0 = 0x50 +let dw_op_regx = 0x90 +let dw_op_bregx = 0x92 +let dw_op_piece = 0x93 + + (* Default corresponding encoding for the different abbreviations *) -module DefaultAbbrevs = - struct - let sibling_type_abbr = dw_form_ref4 - let file_loc_type_abbr = dw_form_data4,dw_form_udata - let type_abbr = dw_form_ref_addr - let name_type_abbr = dw_form_string - let encoding_type_abbr = dw_form_data1 - let byte_size_type_abbr = dw_form_data1 - let member_size_abbr = dw_form_udata - let high_pc_type_abbr = dw_form_addr - let low_pc_type_abbr = dw_form_addr - let stmt_list_type_abbr = dw_form_data4 - let declaration_type_abbr = dw_form_flag - let external_type_abbr = dw_form_flag - let prototyped_type_abbr = dw_form_flag - let bit_offset_type_abbr = dw_form_data1 - let comp_dir_type_abbr = dw_form_string - let language_type_abbr = dw_form_udata - let producer_type_abbr = dw_form_string - let value_type_abbr = dw_form_sdata - let artificial_type_abbr = dw_form_flag - let variable_parameter_type_abbr = dw_form_flag - let bit_size_type_abbr = dw_form_data1 - let location_const_type_abbr = dw_form_data4 - let location_block_type_abbr = dw_form_block - let data_location_block_type_abbr = dw_form_block - let data_location_ref_type_abbr = dw_form_ref4 - let bound_const_type_abbr = dw_form_udata - let bound_ref_type_abbr=dw_form_ref4 - end +let sibling_type_abbr = dw_form_ref4 +let file_loc_type_abbr = dw_form_data4,dw_form_udata +let type_abbr = dw_form_ref_addr +let name_type_abbr = dw_form_string +let encoding_type_abbr = dw_form_data1 +let byte_size_type_abbr = dw_form_data1 +let member_size_abbr = dw_form_udata +let high_pc_type_abbr = dw_form_addr +let low_pc_type_abbr = dw_form_addr +let stmt_list_type_abbr = dw_form_data4 +let declaration_type_abbr = dw_form_flag +let external_type_abbr = dw_form_flag +let prototyped_type_abbr = dw_form_flag +let bit_offset_type_abbr = dw_form_data1 +let comp_dir_type_abbr = dw_form_string +let language_type_abbr = dw_form_udata +let producer_type_abbr = dw_form_string +let value_type_abbr = dw_form_sdata +let artificial_type_abbr = dw_form_flag +let variable_parameter_type_abbr = dw_form_flag +let bit_size_type_abbr = dw_form_data1 +let location_ref_type_abbr = dw_form_data4 +let location_block_type_abbr = dw_form_block +let data_location_block_type_abbr = dw_form_block +let data_location_ref_type_abbr = dw_form_ref4 +let bound_const_type_abbr = dw_form_udata +let bound_ref_type_abbr=dw_form_ref4 + +(* Sizeof functions for the encoding of uleb128 and sleb128 *) +let sizeof_uleb128 value = + let size = ref 1 in + let value = ref (value lsr 7) in + while !value <> 0 do + value := !value lsr 7; + incr size; + done; + !size + +let sizeof_sleb128 value = + let size = ref 1 in + let byte = ref (value land 0x7f) in + let value = ref (value lsr 7) in + while not ((!value = 0 && (!byte land 0x40) = 0) || (!value = -1 && ((!byte land 0x40) <> 0))) do + byte := !value land 0x7f; + value := !value lsr 7; + incr size; + done; + !size + +let size_of_loc_expr = function + | DW_OP_bregx (a,b) -> 1 + (sizeof_uleb128 a) + (sizeof_sleb128 (Int32.to_int b)) + | DW_OP_plus_uconst a + | DW_OP_piece a -> 1 + (sizeof_uleb128 a) + | DW_OP_reg i -> if i < 32 then 1 else 2 diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml new file mode 100644 index 00000000..3239ceb6 --- /dev/null +++ b/debug/Dwarfgen.ml @@ -0,0 +1,444 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open AST +open C +open Camlcoq +open Cutil +open DebugInformation +open DwarfTypes +open DwarfUtil +(* Generate the dwarf DIE's from the information collected in DebugInformation *) + +(* Helper function to get values that must be set. *) +let get_opt_val = function + | Some a -> a + | None -> assert false + +(* Auxiliary data structures and functions *) +module IntSet = Set.Make(struct + type t = int + let compare (x:int) (y:int) = compare x y +end) + +let rec mmap f env = function + | [] -> ([],env) + | hd :: tl -> + let (hd',env1) = f env hd in + let (tl', env2) = mmap f env1 tl in + (hd' :: tl', env2) + +(* Functions to translate the basetypes. *) +let int_type_to_entry id i = + let encoding = + (match i.int_kind with + | IBool -> DW_ATE_boolean + | IChar -> + if !Machine.config.Machine.char_signed then + DW_ATE_signed_char + else + DW_ATE_unsigned_char + | IInt | ILong | ILongLong | IShort | ISChar -> DW_ATE_signed + | _ -> DW_ATE_unsigned)in + let int = { + base_type_byte_size = sizeof_ikind i.int_kind; + base_type_encoding = Some encoding; + base_type_name = typ_to_string (TInt (i.int_kind,[]));} in + new_entry id (DW_TAG_base_type int) + +let float_type_to_entry id f = + let byte_size = sizeof_fkind f.float_kind in + let float = { + base_type_byte_size = byte_size; + base_type_encoding = Some DW_ATE_float; + base_type_name = typ_to_string (TFloat (f.float_kind,[])); + } in + new_entry id (DW_TAG_base_type float) + +let void_to_entry id = + let void = { + base_type_byte_size = 0; + base_type_encoding = None; + base_type_name = "void"; + } in + new_entry id (DW_TAG_base_type void) + +let translate_file_loc sec (f,l) = + Hashtbl.find filenum (sec,f),l + +let translate_file_loc_opt sec = function + | None -> None + | Some (f,l) -> + try + Some (translate_file_loc sec (f,l)) + with Not_found -> None + +let typedef_to_entry sec id t = + let i = get_opt_val t.typ in + let td = { + typedef_file_loc = translate_file_loc_opt sec t.typedef_file_loc; + typedef_name = t.typedef_name; + typedef_type = i; + } in + new_entry id (DW_TAG_typedef td) + +let pointer_to_entry id p = + let p = {pointer_type = p.pts} in + new_entry id (DW_TAG_pointer_type p) + +let array_to_entry id arr = + let arr_tag = { + array_type_file_loc = None; + array_type = arr.arr_type; + } in + let arr_entry = new_entry id (DW_TAG_array_type arr_tag) in + let children = List.map (fun a -> + let r = match a with + | None -> None + | Some i -> + let bound = Int64.to_int (Int64.sub i Int64.one) in + Some (BoundConst bound) in + let s = { + subrange_type = None; + subrange_upper_bound = r; + } in + new_entry (next_id ()) (DW_TAG_subrange_type s)) arr.arr_size in + add_children arr_entry children + +let const_to_entry id c = + new_entry id (DW_TAG_const_type ({const_type = c.cst_type})) + +let volatile_to_entry id v = + new_entry id (DW_TAG_volatile_type ({volatile_type = v.vol_type})) + +let enum_to_entry sec id e = + let enumerator_to_entry e = + let tag = + { + enumerator_file_loc = None; + enumerator_value = Int64.to_int (e.enumerator_const); + enumerator_name = e.enumerator_name; + } in + new_entry (next_id ()) (DW_TAG_enumerator tag) in + let bs = sizeof_ikind enum_ikind in + let enum = { + enumeration_file_loc = translate_file_loc_opt sec e.enum_file_loc; + enumeration_byte_size = bs; + enumeration_declaration = Some false; + enumeration_name = Some e.enum_name; + } in + let enum = new_entry id (DW_TAG_enumeration_type enum) in + let child = List.map enumerator_to_entry e.enum_enumerators in + add_children enum child + +let fun_type_to_entry id f = + let children = if f.fun_prototyped then + let u = { + unspecified_parameter_file_loc = None; + unspecified_parameter_artificial = None; + } in + [new_entry (next_id ()) (DW_TAG_unspecified_parameter u)] + else + List.map (fun p -> + let fp = { + formal_parameter_file_loc = None; + formal_parameter_artificial = None; + formal_parameter_name = if p.param_name <> "" then Some p.param_name else None; + formal_parameter_type = p.param_type; + formal_parameter_variable_parameter = None; + formal_parameter_location = None; + } in + new_entry (next_id ()) (DW_TAG_formal_parameter fp)) f.fun_params; + in + let s = { + subroutine_type = f.fun_return_type; + subroutine_prototyped = f.fun_prototyped + } in + let s = new_entry id (DW_TAG_subroutine_type s) in + add_children s children + +let member_to_entry mem = + let mem = { + member_file_loc = None; + member_byte_size = mem.cfd_byte_size; + member_bit_offset = mem.cfd_bit_offset; + member_bit_size = mem.cfd_bit_size; + member_data_member_location = + (match mem.cfd_byte_offset with + | None -> None + | Some s -> Some (DataLocBlock (DW_OP_plus_uconst s))); + member_declaration = None; + member_name = Some (mem.cfd_name); + member_type = mem.cfd_typ; + } in + new_entry (next_id ()) (DW_TAG_member mem) + +let struct_to_entry sec id s = + let tag = { + structure_file_loc = translate_file_loc_opt sec s.ct_file_loc; + structure_byte_size = s.ct_sizeof; + structure_declaration = Some s.ct_declaration; + structure_name = if s.ct_name <> "" then Some s.ct_name else None; + } in + let entry = new_entry id (DW_TAG_structure_type tag) in + let child = List.map member_to_entry s.ct_members in + add_children entry child + +let union_to_entry sec id s = + let tag = { + union_file_loc = translate_file_loc_opt sec s.ct_file_loc; + union_byte_size = s.ct_sizeof; + union_declaration = Some s.ct_declaration; + union_name = if s.ct_name <> "" then Some s.ct_name else None; + } in + let entry = new_entry id (DW_TAG_union_type tag) in + let child = List.map member_to_entry s.ct_members in + add_children entry child + +let composite_to_entry sec id s = + match s.ct_sou with + | Struct -> struct_to_entry sec id s + | Union -> union_to_entry sec id s + +let infotype_to_entry sec id = function + | IntegerType i -> int_type_to_entry id i + | FloatType f -> float_type_to_entry id f + | PointerType p -> pointer_to_entry id p + | ArrayType arr -> array_to_entry id arr + | CompositeType c -> composite_to_entry sec id c + | EnumType e -> enum_to_entry sec id e + | FunctionType f -> fun_type_to_entry id f + | Typedef t -> typedef_to_entry sec id t + | ConstType c -> const_to_entry id c + | VolatileType v -> volatile_to_entry id v + | Void -> void_to_entry id + +let needs_types id d = + let add_type id d = + if not (IntSet.mem id d) then + IntSet.add id d,true + else + d,false in + let t = Hashtbl.find types id in + match t with + | IntegerType _ + | FloatType _ + | Void + | EnumType _ -> d,false + | Typedef t -> + add_type (get_opt_val t.typ) d + | PointerType p -> + add_type p.pts d + | ArrayType arr -> + add_type arr.arr_type d + | ConstType c -> + add_type c.cst_type d + | VolatileType v -> + add_type v.vol_type d + | FunctionType f -> + let d,c = match f.fun_return_type with + | Some t -> add_type t d + | None -> d,false in + List.fold_left (fun (d,c) p -> + let d,c' = add_type p.param_type d in + d,c||c') (d,c) f.fun_params + | CompositeType c -> + List.fold_left (fun (d,c) f -> + let d,c' = add_type f.cfd_typ d in + d,c||c') (d,false) c.ct_members + +let gen_types sec needed = + let rec aux d = + let d,c = IntSet.fold (fun id (d,c) -> + let d,c' = needs_types id d in + d,c||c') d (d,false) in + if c then + aux d + else + d in + let typs = aux needed in + List.rev (Hashtbl.fold (fun id t acc -> + if IntSet.mem id typs then + (infotype_to_entry sec id t)::acc + else + acc) types []) + +let global_variable_to_entry sec acc id v = + let var = { + variable_file_loc = translate_file_loc sec v.gvar_file_loc; + variable_declaration = Some v.gvar_declaration; + variable_external = Some v.gvar_external; + variable_name = v.gvar_name; + variable_type = v.gvar_type; + variable_location = match v.gvar_atom with Some a -> Some (LocSymbol a) | None -> None; + } in + new_entry id (DW_TAG_variable var),IntSet.add v.gvar_type acc + +let gen_splitlong op_hi op_lo = + let op_piece = DW_OP_piece 4 in + op_piece::op_hi@(op_piece::op_lo) + +let translate_function_loc a = function + | BA_addrstack (ofs) -> + let ofs = camlint_of_coqint ofs in + Some (LocSimple (DW_OP_bregx (a,ofs))),[] + | BA_splitlong (BA_addrstack hi,BA_addrstack lo)-> + let hi = camlint_of_coqint hi + and lo = camlint_of_coqint lo in + if lo = Int32.add hi 4l then + Some (LocSimple (DW_OP_bregx (a,hi))),[] + else + let op_hi = [DW_OP_bregx (a,hi)] + and op_lo = [DW_OP_bregx (a,lo)] in + Some (LocList (gen_splitlong op_hi op_lo)),[] + | _ -> None,[] + +let range_entry_loc (sp,l) = + let rec aux = function + | BA i -> [DW_OP_reg i] + | BA_addrstack ofs -> + let ofs = camlint_of_coqint ofs in + [DW_OP_bregx (sp,ofs)] + | BA_splitlong (hi,lo) -> + let hi = aux hi + and lo = aux lo in + gen_splitlong hi lo + | _ -> assert false in + match aux l with + | [] -> assert false + | [a] -> LocSimple a + | a::rest -> LocList (a::rest) + +let location_entry f_id atom = + try + begin + match (Hashtbl.find var_locations atom) with + | FunctionLoc (a,r) -> + translate_function_loc a r + | RangeLoc l -> + let l = List.map (fun i -> + let hi = get_opt_val i.range_start + and lo = get_opt_val i.range_end in + let hi = Hashtbl.find label_translation (f_id,hi) + and lo = Hashtbl.find label_translation (f_id,lo) in + hi,lo,range_entry_loc i.var_loc) l in + let id = next_id () in + Some (LocRef id),[{loc = l;loc_id = id;}] + end + with Not_found -> None,[] + +let function_parameter_to_entry f_id (acc,bcc) p = + let loc,loc_list = location_entry f_id (get_opt_val p.parameter_atom) in + let p = { + formal_parameter_file_loc = None; + formal_parameter_artificial = None; + formal_parameter_name = Some p.parameter_name; + formal_parameter_type = p.parameter_type; + formal_parameter_variable_parameter = None; + formal_parameter_location = loc; + } in + new_entry (next_id ()) (DW_TAG_formal_parameter p),(IntSet.add p.formal_parameter_type acc,loc_list@bcc) + +let rec local_variable_to_entry sec f_id (acc,bcc) v id = + let loc,loc_list = location_entry f_id (get_opt_val v.lvar_atom) in + let var = { + variable_file_loc = translate_file_loc sec v.lvar_file_loc; + variable_declaration = None; + variable_external = None; + variable_name = v.lvar_name; + variable_type = v.lvar_type; + variable_location = loc; + } in + new_entry id (DW_TAG_variable var),(IntSet.add v.lvar_type acc,loc_list@bcc) + +and scope_to_entry sec f_id acc sc id = + let l_pc,h_pc = try + let r = Hashtbl.find scope_ranges id in + let lbl l = match l with + | Some l -> Some (Hashtbl.find label_translation (f_id,l)) + | None -> None in + begin + match r with + | [] -> None,None + | [a] -> lbl a.start_addr, lbl a.end_addr + | a::rest -> lbl (List.hd (List.rev rest)).start_addr,lbl a.end_addr + end + with Not_found -> None,None in + let scope = { + lexical_block_high_pc = h_pc; + lexical_block_low_pc = l_pc; + } in + let vars,acc = mmap (local_to_entry sec f_id) acc sc.scope_variables in + let entry = new_entry id (DW_TAG_lexical_block scope) in + add_children entry vars,acc + +and local_to_entry sec f_id acc id = + match Hashtbl.find local_variables id with + | LocalVariable v -> local_variable_to_entry sec f_id acc v id + | Scope v -> scope_to_entry sec f_id acc v id + +let fun_scope_to_entries sec f_id acc id = + match id with + | None -> [],acc + | Some id -> + let sc = Hashtbl.find local_variables id in + (match sc with + | Scope sc ->mmap (local_to_entry sec f_id) acc sc.scope_variables + | _ -> assert false) + +let function_to_entry sec (acc,bcc) id f = + let f_tag = { + subprogram_file_loc = translate_file_loc sec f.fun_file_loc; + subprogram_external = Some f.fun_external; + subprogram_name = f.fun_name; + subprogram_prototyped = true; + subprogram_type = f.fun_return_type; + subprogram_high_pc = f.fun_high_pc; + subprogram_low_pc = f.fun_low_pc; + } in + let f_id = get_opt_val f.fun_atom in + let acc = match f.fun_return_type with Some s -> IntSet.add s acc | None -> acc in + let f_entry = new_entry id (DW_TAG_subprogram f_tag) in + let params,(acc,bcc) = mmap (function_parameter_to_entry f_id) (acc,bcc) f.fun_parameter in + let vars,(acc,bcc) = fun_scope_to_entries sec f_id (acc,bcc) f.fun_scope in + add_children f_entry (params@vars),(acc,bcc) + +let definition_to_entry sec (acc,bcc) id t = + match t with + | GlobalVariable g -> let e,acc = global_variable_to_entry sec acc id g in + e,(acc,bcc) + | Function f -> function_to_entry sec (acc,bcc) id f + +module StringMap = Map.Make(String) + +let gen_debug_info sec_name var_section : debug_entries = + let defs = Hashtbl.fold (fun id t acc -> + let s = match t with + | GlobalVariable _ -> var_section + | Function f -> sec_name (get_opt_val f.fun_atom) in + let old = try StringMap.find s acc with Not_found -> [] in + StringMap.add s ((id,t)::old) acc) definitions StringMap.empty in + StringMap.fold (fun s defs acc -> + let defs,(ty,locs) = List.fold_left (fun (acc,bcc) (id,t) -> + let t,bcc = definition_to_entry s bcc id t in + t::acc,bcc) ([],(IntSet.empty,[])) defs in + let line_start,low_pc,debug_start,_ = Hashtbl.find compilation_section_start s + and high_pc = Hashtbl.find compilation_section_end s in + let cp = { + compile_unit_name = !file_name; + compile_unit_low_pc = low_pc; + compile_unit_high_pc = high_pc; + compile_unit_stmt_list = line_start; + } in + let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in + let cp = add_children cp ((gen_types s ty) @ defs) in + (s,debug_start,cp,(low_pc,locs))::acc) defs [] diff --git a/driver/Driver.ml b/driver/Driver.ml index f53de821..9b1a6e70 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -108,6 +108,7 @@ let preprocess ifile ofile = (* From preprocessed C to Csyntax *) let parse_c_file sourcename ifile = + Debug.init_compile_unit sourcename; Sections.initialize(); (* Simplification options *) let simplifs = @@ -117,10 +118,10 @@ let parse_c_file sourcename ifile = ^ (if !option_fpacked_structs then "p" else "") in (* Parsing and production of a simplified C AST *) - let ast,debug = + let ast = match Parse.preprocessed_file simplifs sourcename ifile with - | None,_ -> exit 2 - | Some p,d -> p,d in + | None -> exit 2 + | Some p -> p in (* Save C AST if requested *) if !option_dparse then begin let ofile = output_filename sourcename ".c" ".parsed.c" in @@ -141,7 +142,7 @@ let parse_c_file sourcename ifile = PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; close_out oc end; - csyntax,debug + csyntax,None (* Dump Asm code in binary format for the validator *) @@ -682,6 +683,7 @@ let _ = Builtins.set C2C.builtins; CPragmas.initialize(); parse_cmdline cmdline_actions; + DebugInit.init (); (* Initialize the debug functions *) let nolink = !option_c || !option_S || !option_E || !option_interp in if nolink && !option_o <> None && !num_source_files >= 2 then begin eprintf "Ambiguous '-o' option (multiple source files)\n"; diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 439dd2b0..51169d86 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -101,7 +101,8 @@ module Cygwin_System : SYSTEM = | Section_user(s, wr, ex) -> sprintf ".section \"%s\", \"%s\"\n" s (if ex then "xr" else if wr then "d" else "dr") - | Section_debug_info + | Section_debug_info _ + | Section_debug_loc | Section_debug_abbrev -> "" (* Dummy value *) let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -150,7 +151,8 @@ module ELF_System : SYSTEM = | Section_user(s, wr, ex) -> sprintf ".section \"%s\",\"a%s%s\",@progbits" s (if wr then "w" else "") (if ex then "x" else "") - | Section_debug_info + | Section_debug_info _ + | Section_debug_loc | Section_debug_abbrev -> "" (* Dummy value *) let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -202,7 +204,8 @@ module MacOS_System : SYSTEM = sprintf ".section \"%s\", %s, %s" (if wr then "__DATA" else "__TEXT") s (if ex then "regular, pure_instructions" else "regular") - | Section_debug_info + | Section_debug_info _ + | Section_debug_loc | Section_debug_abbrev -> "" (* Dummy value *) let stack_alignment = 16 (* mandatory *) @@ -770,7 +773,7 @@ module Target(System: SYSTEM):TARGET = let get_stmt_list_addr () = -1 (* Dummy constant *) - module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs (* Dummy Abbrev types *) + let get_debug_start_addr () = -1 (* Dummy constant *) let label = label diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 68c095f0..c50b3230 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -295,8 +295,7 @@ let intern_string s = next_atom := Pos.succ !next_atom; Hashtbl.add atom_of_string s a; Hashtbl.add string_of_atom a s; - a - + a let extern_atom a = try Hashtbl.find string_of_atom a diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index a7e66701..5764aa8f 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -330,8 +330,9 @@ let p_section oc = function | Section_literal -> fprintf oc "{\"Section Name\":\"Literal\"}" | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}" | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":%s,\"Writable\":%B,\"Executable\":%B}" s w e - | Section_debug_info - | Section_debug_abbrev -> () (* There should be no info in the debug sections *) + | Section_debug_info _ + | Section_debug_abbrev + | Section_debug_loc -> () (* There should be no info in the debug sections *) let p_int_opt oc = function | None -> fprintf oc "0" diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index fc0fc44e..5a365123 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -563,7 +563,7 @@ let num_crbit = function | CRbit_3 -> 3 | CRbit_6 -> 6 -let expand_instruction instr = +let expand_instruction_simple instr = match instr with | Pallocframe(sz, ofs,retofs) -> let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in @@ -637,22 +637,160 @@ let expand_instruction instr = | _ -> emit instr -let expand_function fn = +(* Translate to the integer identifier of the register as + the EABI specifies *) + +let int_reg_to_dwarf = function + | GPR0 -> 0 | GPR1 -> 1 | GPR2 -> 2 | GPR3 -> 3 + | GPR4 -> 4 | GPR5 -> 5 | GPR6 -> 6 | GPR7 -> 7 + | GPR8 -> 8 | GPR9 -> 9 | GPR10 -> 10 | GPR11 -> 11 + | GPR12 -> 12 | GPR13 -> 13 | GPR14 -> 14 | GPR15 -> 15 + | GPR16 -> 16 | GPR17 -> 17 | GPR18 -> 18 | GPR19 -> 19 + | GPR20 -> 20 | GPR21 -> 21 | GPR22 -> 22 | GPR23 -> 23 + | GPR24 -> 24 | GPR25 -> 25 | GPR26 -> 26 | GPR27 -> 27 + | GPR28 -> 28 | GPR29 -> 29 | GPR30 -> 30 | GPR31 -> 31 + +let float_reg_to_dwarf = function + | FPR0 -> 32 | FPR1 -> 33 | FPR2 -> 34 | FPR3 -> 35 + | FPR4 -> 36 | FPR5 -> 37 | FPR6 -> 38 | FPR7 -> 39 + | FPR8 -> 40 | FPR9 -> 41 | FPR10 -> 42 | FPR11 -> 43 + | FPR12 -> 44 | FPR13 -> 45 | FPR14 -> 46 | FPR15 -> 47 + | FPR16 -> 48 | FPR17 -> 49 | FPR18 -> 50 | FPR19 -> 51 + | FPR20 -> 52 | FPR21 -> 53 | FPR22 -> 54| FPR23 -> 55 + | FPR24 -> 56 | FPR25 -> 57 | FPR26 -> 58 | FPR27 -> 59 + | FPR28 -> 60 | FPR29 -> 61 | FPR30 -> 62 | FPR31 -> 63 + +let preg_to_dwarf_int = function + | IR r -> int_reg_to_dwarf r + | FR r -> float_reg_to_dwarf r + | _ -> assert false + + +let translate_annot annot = + let rec aux = function + | BA x -> Some (BA (preg_to_dwarf_int x)) + | BA_int _ + | BA_long _ + | BA_float _ + | BA_single _ + | BA_loadglobal _ + | BA_addrglobal _ + | BA_loadstack _ -> None + | BA_addrstack ofs -> Some (BA_addrstack ofs) + | BA_splitlong (hi,lo) -> + begin + match (aux hi,aux lo) with + | Some hi ,Some lo -> Some (BA_splitlong (hi,lo)) + | _,_ -> None + end in + (match annot with + | [] -> None + | a::_ -> aux a) + +let expand_scope id lbl oldscopes newscopes = + let opening = List.filter (fun a -> not (List.mem a oldscopes)) newscopes + and closing = List.filter (fun a -> not (List.mem a newscopes)) oldscopes in + List.iter (fun i -> Debug.open_scope id i lbl) opening; + List.iter (fun i -> Debug.close_scope id i lbl) closing + +let expand_instruction id l = + let get_lbl = function + | None -> + let lbl = new_label () in + emit (Plabel lbl); + lbl + | Some lbl -> lbl in + let rec aux lbl scopes = function + | [] -> let lbl = get_lbl lbl in + Debug.function_end id lbl + | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest -> + let kind = (P.to_int kind) in + emit i; + begin + match kind with + | 1-> + aux lbl scopes rest + | 2 -> + aux lbl scopes rest + | 3 -> + begin + match translate_annot args with + | Some a -> + let lbl = get_lbl lbl in + Debug.start_live_range txt lbl (1,a); + aux (Some lbl) scopes rest + | None -> aux lbl scopes rest + end + | 4 -> + let lbl = get_lbl lbl in + Debug.end_live_range txt lbl; + aux (Some lbl) scopes rest + | 5 -> + begin + match translate_annot args with + | Some a-> + Debug.stack_variable txt (1,a); + aux lbl scopes rest + | _ -> aux lbl scopes rest + end + | 6 -> + let lbl = get_lbl lbl in + let scopes' = List.map (function BA_int x -> Int32.to_int (camlint_of_coqint x) | _ -> assert false) args in + expand_scope id lbl scopes scopes'; + aux (Some lbl) scopes' rest + | _ -> + aux None scopes rest + end + | i::rest -> expand_instruction_simple i; aux None scopes rest in + (* We need to move all closing debug annotations before the last real statement *) + let rec move_debug acc = function + | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest -> + move_debug (i::acc) rest (* Move the debug annotations forward *) + | b::rest -> List.rev (b::(List.rev acc)@rest) (* We found the first non debug location *) + | [] -> List.rev acc (* This actually can never happen *) in + aux None [] (move_debug [] (List.rev l)) + + +let expand_function id fn = try set_current_function fn; - List.iter expand_instruction fn.fn_code; + if !Clflags.option_g then + expand_instruction id fn.fn_code + else + List.iter expand_instruction_simple fn.fn_code; Errors.OK (get_current_function ()) with Error s -> Errors.Error (Errors.msg (coqstring_of_camlstring s)) -let expand_fundef = function +let expand_fundef id = function | Internal f -> - begin match expand_function f with + begin match expand_function id f with | Errors.OK tf -> Errors.OK (Internal tf) | Errors.Error msg -> Errors.Error msg end | External ef -> Errors.OK (External ef) +let rec transform_partial_prog transfun p = + match p with + | [] -> Errors.OK [] + | (id,Gvar v)::l -> + (match transform_partial_prog transfun l with + | Errors.OK x -> Errors.OK ((id,Gvar v)::x) + | Errors.Error msg -> Errors.Error msg) + | (id,Gfun f)::l -> + (match transfun id f with + | Errors.OK tf -> + (match transform_partial_prog transfun l with + | Errors.OK x -> Errors.OK ((id,Gfun tf)::x) + | Errors.Error msg -> Errors.Error msg) + | Errors.Error msg -> + Errors.Error ((Errors.MSG (coqstring_of_camlstring "In function"))::((Errors.CTX + id) :: (Errors.MSG (coqstring_of_camlstring ": ") :: msg)))) + let expand_program (p: Asm.program) : Asm.program Errors.res = - AST.transform_partial_program expand_fundef p + match transform_partial_prog expand_fundef p.prog_defs with + | Errors.OK x-> + Errors.OK { prog_defs = x; prog_public = p.prog_public; prog_main = + p.prog_main } + | Errors.Error msg -> Errors.Error msg diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index eca7a1b8..3c73f22d 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -78,6 +78,8 @@ let end_addr = ref (-1) let stmt_list_addr = ref (-1) +let debug_start_addr = ref (-1) + let label = elf_label module Linux_System : SYSTEM = @@ -129,9 +131,10 @@ module Linux_System : SYSTEM = | Section_user(s, wr, ex) -> sprintf ".section \"%s\",\"a%s%s\",@progbits" s (if wr then "w" else "") (if ex then "x" else "") - | Section_debug_info -> ".debug_info,\"\",@progbits" + | Section_debug_info _ -> ".debug_info,\"\",@progbits" | Section_debug_abbrev -> ".debug_abbrev,\"\",@progbits" - + | Section_debug_loc -> ".debug_loc,\"\",@progbits" + let section oc sec = let name = name_of_section sec in assert (name <> "COMM"); @@ -207,14 +210,20 @@ module Diab_System : SYSTEM = | true, false -> 'd' (* data *) | false, true -> 'c' (* text *) | false, false -> 'r') (* const *) - | Section_debug_info -> ".debug_info,,n" - | Section_debug_abbrev -> ".debug_abbrev,,n" + | Section_debug_info s -> sprintf ".section .debug_info%s,,n" (if s <> ".text" then s else "") + | Section_debug_abbrev -> ".section .debug_abbrev,,n" + | Section_debug_loc -> ".section .debug_loc,,n" let section oc sec = let name = name_of_section sec in assert (name <> "COMM"); - fprintf oc " %s\n" name - + match sec with + | Section_debug_info s -> + fprintf oc " %s\n" name; + if s <> ".text" then + fprintf oc " .sectionlink .debug_info\n" + | _ -> + fprintf oc " %s\n" name let print_file_line oc file line = print_file_line_d2 oc comment file line @@ -229,65 +238,51 @@ module Diab_System : SYSTEM = let cfi_rel_offset oc reg ofs = () let print_prologue oc = - fprintf oc " .xopt align-fill-text=0x60000000\n"; - if !Clflags.option_g then - begin - fprintf oc " .text\n"; - fprintf oc " .section .debug_line,,n\n"; - let label_line_start = new_label () in - stmt_list_addr := label_line_start; - fprintf oc "%a:\n" label label_line_start; - fprintf oc " .text\n"; - let label_start = new_label () in - start_addr := label_start; - fprintf oc "%a:\n" label label_start; - fprintf oc " .d2_line_start .debug_line\n"; - end - - let filenum : (string,int) Hashtbl.t = Hashtbl.create 7 - - let additional_debug_sections: StringSet.t ref = ref StringSet.empty - + fprintf oc " .xopt align-fill-text=0x60000000\n" let print_epilogue oc = - if !Clflags.option_g then - begin - fprintf oc "\n"; - let label_end = new_label () in - end_addr := label_end; - fprintf oc "%a:\n" label label_end; - fprintf oc " .text\n"; - StringSet.iter (fun file -> - let label = new_label () in - Hashtbl.add filenum file label; - fprintf oc ".L%d: .d2filenum \"%s\"\n" label file) !all_files; - fprintf oc " .d2_line_end\n"; - StringSet.iter (fun s -> - fprintf oc " %s\n" s; - fprintf oc " .d2_line_end\n") !additional_debug_sections - end + let end_label sec = + fprintf oc "\n"; + fprintf oc " %s\n" sec; + let label_end = new_label () in + fprintf oc "%a:\n" label label_end; + label_end + and entry_label f = + let label = new_label () in + fprintf oc ".L%d: .d2filenum \"%s\"\n" label f; + label + and end_line () = fprintf oc " .d2_line_end\n" in + Debug.compute_file_enum end_label entry_label end_line let print_file_loc oc (file,col) = - fprintf oc " .4byte %a\n" label (Hashtbl.find filenum file); + fprintf oc " .4byte 1\n";(* label (Hashtbl.find filenum file);*) fprintf oc " .uleb128 %d\n" col let debug_section oc sec = - if !Clflags.option_g && Configuration.advanced_debug then - match sec with - | Section_user (name,_,_) -> - let sec_name = name_of_section sec in - if not (StringSet.mem sec_name !additional_debug_sections) then - begin - let name = ".debug_line"^name in - additional_debug_sections := StringSet.add sec_name !additional_debug_sections; - fprintf oc " .section %s,,n\n" name; - fprintf oc " .sectionlink .debug_line\n"; - section oc sec; - fprintf oc " .d2_line_start %s\n" name - end - | _ -> () (* Only the case of a user section is interresting *) - else - () + match sec with + | Section_debug_abbrev + | Section_debug_info _ + | Section_debug_loc -> () + | sec -> + let name = match sec with + | Section_user (name,_,_) -> name + | _ -> name_of_section sec in + if not (Debug.exists_section name) then + let line_start = new_label () + and low_pc = new_label () + and debug_info = new_label () in + Debug.add_compilation_section_start name (line_start,low_pc,debug_info,name_of_section sec); + let line_name = ".debug_line" ^(if name <> ".text" then name else "") in + fprintf oc " .section %s,,n\n" line_name; + if name <> ".text" then + fprintf oc " .sectionlink .debug_line\n"; + fprintf oc "%a:\n" label line_start; + section oc sec; + fprintf oc "%a:\n" label low_pc; + fprintf oc " .0byte %a\n" label debug_info; + fprintf oc " .d2_line_start %s\n" line_name + else + () end @@ -855,14 +850,13 @@ module Target (System : SYSTEM):TARGET = let get_stmt_list_addr () = !stmt_list_addr - module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs + let get_debug_start_addr () = !debug_start_addr let new_label = new_label let section oc sec = section oc sec; debug_section oc sec - end let sel_target () = |