diff options
-rw-r--r-- | Makefile | 3 | ||||
-rw-r--r-- | Makefile.extr | 2 | ||||
-rw-r--r-- | arm/TargetPrinter.ml | 12 | ||||
-rw-r--r-- | backend/PrintAnnot.ml | 8 | ||||
-rw-r--r-- | backend/PrintAsm.ml | 54 | ||||
-rw-r--r-- | backend/PrintAsm.mli | 4 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 8 | ||||
-rw-r--r-- | checklink/Check.ml | 4 | ||||
-rw-r--r-- | common/Sections.ml | 2 | ||||
-rw-r--r-- | common/Sections.mli | 2 | ||||
-rwxr-xr-x | configure | 5 | ||||
-rw-r--r-- | cparser/Cutil.mli | 2 | ||||
-rw-r--r-- | cparser/Parse.ml | 21 | ||||
-rw-r--r-- | cparser/Parse.mli | 2 | ||||
-rw-r--r-- | debug/CtoDwarf.ml | 392 | ||||
-rw-r--r-- | debug/DwarfPrinter.ml | 502 | ||||
-rw-r--r-- | debug/DwarfTypes.mli | 271 | ||||
-rw-r--r-- | debug/DwarfUtil.ml | 126 | ||||
-rw-r--r-- | driver/Configuration.ml | 6 | ||||
-rw-r--r-- | driver/Driver.ml | 25 | ||||
-rw-r--r-- | ia32/TargetPrinter.ml | 13 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 72 |
22 files changed, 1494 insertions, 42 deletions
@@ -15,7 +15,7 @@ include Makefile.config -DIRS=lib common $(ARCH) backend cfrontend driver \ +DIRS=lib common $(ARCH) backend cfrontend driver debug\ flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight \ cparser cparser/validator @@ -203,6 +203,7 @@ compcert.ini: Makefile.config VERSION echo "system=$(SYSTEM)"; \ echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \ echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \ + echo "advanced_debug=$(ADVANCED_DEBUG)"; \ version=`cat VERSION`; \ echo version=$$version) \ > compcert.ini diff --git a/Makefile.extr b/Makefile.extr index fed2d78f..4e17e904 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -21,7 +21,7 @@ include Makefile.config DIRS=extraction \ lib common $(ARCH) backend cfrontend cparser driver \ - exportclight + exportclight debug # Directories containing Caml code that must be preprocessed by Camlp4 diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 9e45019e..b37683d3 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -1127,6 +1127,18 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let print_epilogue oc = () let default_falignment = 4 + + let get_start_addr () = -1 (* Dummy constant *) + + let get_end_addr () = -1 (* Dummy constant *) + + let get_stmt_list_addr () = -1 (* Dummy constant *) + + module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs (* Dummy Abbrev types *) + + let label = print_label + + let new_label = new_label end let sel_target () = diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml index 54174b9f..26f96370 100644 --- a/backend/PrintAnnot.ml +++ b/backend/PrintAnnot.ml @@ -66,10 +66,10 @@ let print_file_line oc pref file line = | Some fb -> Printlines.copy oc pref fb line line end -(* Add file and line debug location, using DWARF1 directives in the style +(* Add file and line debug location, using DWARF2 directives in the style of Diab C 5 *) -let print_file_line_d1 oc pref file line = +let print_file_line_d2 oc pref file line = if !Clflags.option_g && file <> "" then begin let (_, filebuf) = try @@ -77,10 +77,10 @@ let print_file_line_d1 oc pref file line = with Not_found -> enter_filename file in if file <> !last_file then begin - fprintf oc " .d1file %S\n" file; + fprintf oc " .d2file %S\n" file; last_file := file end; - fprintf oc " .d1line %d\n" line; + fprintf oc " .d2line %d\n" line; match filebuf with | None -> () | Some fb -> Printlines.copy oc pref fb line line diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index a6883339..11854ace 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -15,6 +15,7 @@ open AST open Asm open Camlcoq open Datatypes +open DwarfPrinter open PrintAsmaux open Printf open Sections @@ -23,6 +24,22 @@ 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 print_debug_label oc l = + if !Clflags.option_g && Configuration.advanced_debug then + fprintf oc "%a:\n" Target.label l + else + () + + let print_location oc loc = if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc) @@ -37,16 +54,21 @@ module Printer(Target:TARGET) = if not (C2C.atom_is_static name) then fprintf oc " .globl %a\n" Target.symbol name; Target.print_optional_fun_info oc; + let s,e = if !Clflags.option_g && Configuration.advanced_debug then + get_fun_addr name + else + -1,-1 in + print_debug_label oc s; fprintf oc "%a:\n" Target.symbol name; print_location oc (C2C.atom_location name); Target.cfi_startproc oc; Target.print_instructions oc fn; Target.cfi_endproc oc; + print_debug_label oc e; Target.print_fun_info oc name; Target.emit_constants oc lit; Target.print_jumptable oc jmptbl - - + let print_init_data oc name id = if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0 && List.for_all (function Init_int8 _ -> true | _ -> false) id @@ -87,10 +109,25 @@ module Printer(Target:TARGET) = | Gfun (Internal code) -> print_function oc name code | Gfun (External ef) -> () | Gvar v -> print_var oc name v - + + module DwarfTarget: DwarfTypes.DWARF_TARGET = + struct + let label = Target.label + let name_of_section = Target.name_of_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 = Hashtbl.find addr_mapping s + end + + module DebugPrinter = DwarfPrinter (DwarfTarget) (Target.DwarfAbbrevs) + + end -let print_program oc p = +let print_program oc p db = let module Target = (val (sel_target ()):TARGET) in let module Printer = Printer(Target) in PrintAnnot.reset_filenames (); @@ -98,4 +135,11 @@ let print_program oc p = Target.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; Target.print_epilogue oc; - PrintAnnot.close_filenames () + PrintAnnot.close_filenames (); + if !Clflags.option_g && Configuration.advanced_debug then + begin + match db with + | None -> () + | Some db -> + Printer.DebugPrinter.print_debug oc db + end diff --git a/backend/PrintAsm.mli b/backend/PrintAsm.mli index eb63f1be..0b2869b0 100644 --- a/backend/PrintAsm.mli +++ b/backend/PrintAsm.mli @@ -11,6 +11,4 @@ (* *) (* *********************************************************************) -open PrintAsmaux - -val print_program: out_channel -> Asm.program -> unit +val print_program: out_channel -> Asm.program -> DwarfTypes.dw_entry option -> unit diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 64db2cb0..8bc961ef 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -14,6 +14,7 @@ open AST open Asm open Camlcoq +open DwarfTypes open Datatypes open Printf open Sections @@ -43,6 +44,13 @@ module type TARGET = val comment: string val symbol: out_channel -> P.t -> unit val default_falignment: int + val get_start_addr: unit -> int + val get_end_addr: unit -> int + val get_stmt_list_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 *) diff --git a/checklink/Check.ml b/checklink/Check.ml index db0159c4..4924744c 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -75,6 +75,8 @@ let name_of_section_Linux: section_name -> string = function | Section_literal -> ".rodata.cst8" | Section_jumptable -> ".text" | Section_user(s, wr, ex) -> s +| Section_debug_info -> ".debug_info" +| Section_debug_abbrev -> ".debug_abbrev" (** Adapted from CompCert *) let name_of_section_Diab: section_name -> string = function @@ -87,6 +89,8 @@ let name_of_section_Diab: section_name -> string = function | Section_literal -> ".text" | Section_jumptable -> ".text" | Section_user(s, wr, ex) -> s +| Section_debug_info -> ".debug_info" +| Section_debug_abbrev -> ".debug_abbrev" (** Taken from CompCert *) let name_of_section: section_name -> string = diff --git a/common/Sections.ml b/common/Sections.ml index c6d4c4c2..c0c95848 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -27,6 +27,8 @@ type section_name = | Section_literal | Section_jumptable | Section_user of string * bool (*writable*) * bool (*executable*) + | Section_debug_info + | Section_debug_abbrev type access_mode = | Access_default diff --git a/common/Sections.mli b/common/Sections.mli index 38b99db0..e878b9e5 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -26,6 +26,8 @@ type section_name = | Section_literal | Section_jumptable | Section_user of string * bool (*writable*) * bool (*executable*) + | Section_debug_info + | Section_debug_abbrev type access_mode = | Access_default @@ -19,6 +19,7 @@ toolprefix='' target='' has_runtime_lib=true build_checklink=true +advanced_debug=false usage='Usage: ./configure [options] target @@ -104,7 +105,8 @@ case "$target" in asm_supports_cfi=false clinker="${toolprefix}dcc" libmath="-lm" - cchecklink=${build_checklink};; + cchecklink=${build_checklink} + advanced_debug=true;; arm*-*) arch="arm" case "$target" in @@ -336,6 +338,7 @@ LIBMATH=$libmath HAS_RUNTIME_LIB=$has_runtime_lib CCHECKLINK=$cchecklink ASM_SUPPORTS_CFI=$asm_supports_cfi +ADVANCED_DEBUG=$advanced_debug EOF else cat >> Makefile.config <<'EOF' diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index b90dc897..06c66b41 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -94,6 +94,8 @@ val incomplete_type : Env.t -> typ -> bool declared but not defined struct or union, or array type without a size. *) val sizeof_ikind: ikind -> int (* Return the size of the given integer kind. *) +val sizeof_fkind: fkind -> int + (* Return the size of the given float kind. *) val is_signed_ikind: ikind -> bool (* Return true if the given integer kind is signed, false if unsigned. *) diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 59b04e7a..645465c3 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -17,14 +17,19 @@ module CharSet = Set.Make(struct type t = char let compare = compare end) -let transform_program t p = +let transform_program t p name = let run_pass pass flag p = if CharSet.mem flag t then pass p else p in - Rename.program - (run_pass StructReturn.program 's' + let p1 = (run_pass StructReturn.program 's' (run_pass PackedStructs.program 'p' (run_pass Bitfields.program 'f' (run_pass Unblock.program 'b' - p)))) + 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),debug let parse_transformations s = let t = ref CharSet.empty in @@ -41,7 +46,7 @@ let parse_transformations s = let preprocessed_file transfs name sourcefile = Cerrors.reset(); let ic = open_in sourcefile in - let p = + let p,d = try let t = parse_transformations transfs in let lb = Lexer.init name ic in @@ -57,9 +62,9 @@ let preprocessed_file transfs name sourcefile = | Parser.Parser.Inter.Timeout_pr -> assert false | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) in let p1 = Timing.time "Elaboration" Elab.elab_file ast in - Timing.time2 "Emulations" transform_program t p1 + Timing.time2 "Emulations" transform_program t p1 name with | Cerrors.Abort -> - [] in + [],None in close_in ic; - if Cerrors.check_errors() then None else Some p + if Cerrors.check_errors() then None,None else Some p,d diff --git a/cparser/Parse.mli b/cparser/Parse.mli index 58c3cfb9..ac8feb70 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 +val preprocessed_file: string -> string -> string -> C.program option * DwarfTypes.dw_entry option (* first arg: desired transformations second arg: source file name before preprocessing diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml new file mode 100644 index 00000000..481221dd --- /dev/null +++ b/debug/CtoDwarf.ml @@ -0,0 +1,392 @@ +(* *********************************************************************) +(* *) +(* 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 C +open Cprint +open Cutil +open C2C +open DwarfTypes +open DwarfUtil +open Env + +(* 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: (string, int) Hashtbl.t = Hashtbl.create 7 + +let get_composite_type (name: string): int = + try + Hashtbl.find composite_types_table name + with Not_found -> + let id = next_id () in + Hashtbl.add composite_types_table name id; + id + + +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) + +let attr_to_dw attr_list id entries = + List.fold_left (fun (id,entry) attr -> + match attr with + | AConst -> let const_tag = DW_TAG_const_type ({const_type = id;}) in + let const_entry = new_entry const_tag in + const_entry.id,const_entry::entry + | AVolatile -> let volatile_tag = DW_TAG_volatile_type ({volatile_type = id;}) in + let volatile_entry = new_entry volatile_tag in + volatile_entry.id,volatile_entry::entry + | ARestrict + | AAlignas _ + | Attr _ -> id,entry) (id,entries) (List.rev attr_list) +let attr_to_dw_tag attr_list tag = + let entry = new_entry tag in + attr_to_dw attr_list entry.id [entry] + + +let rec type_to_dwarf (typ: typ): int * dw_entry list = + let typ_string = typ_to_string typ in + try + Hashtbl.find type_table typ_string,[] + with Not_found -> + let id,entries = + match typ with + | TVoid at -> let void = { + base_type_byte_size = 0; + base_type_encoding = None; + base_type_name = "void"; + } in + attr_to_dw_tag at (DW_TAG_base_type void) + | TInt (k,at) -> + 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_string;} in + attr_to_dw_tag at (DW_TAG_base_type int) + | TFloat (k,at) -> + 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_string; + } in + attr_to_dw_tag at (DW_TAG_base_type float) + | TPtr (t,at) -> + let t,e = type_to_dwarf t in + let pointer = {pointer_type = t;} in + let t,e2 = attr_to_dw_tag at (DW_TAG_pointer_type pointer) in + t,e2@e + | TFun (rt,args,_,at) -> + let ret,et = (match rt with + | TVoid _ -> None,[] (* Void return *) + | _ -> 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 + attr_to_dw at s.id ((s::others)@et) + | TStruct (i,at) + | TUnion (i,at) + | TEnum (i,at) -> + let t = get_composite_type i.name in + attr_to_dw at t [] + | TNamed (i,at) -> + let t = Hashtbl.find typedef_table i.name in + attr_to_dw at t [] + | TArray (child,size,at) -> + let size_to_subrange s = + let b = (match s with + | None -> None + | Some i -> + let i = Int64.to_int i in + Some (BoundConst i)) in + let s = { + subrange_type = None; + subrange_upper_bound = b; + } in + 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,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 (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 + attr_to_dw at arr.id (arr::e) + in + Hashtbl.add type_table typ_string id; + id,entries + +let rec globdecl_to_dwarf env decl = + match decl.gdesc with + | Gtypedef (n,t) -> + let i,t = type_to_dwarf t in + Hashtbl.add typedef_table n.name i; + let td = { + typedef_file_loc = Some (decl.gloc); + typedef_name = n.name; + typedef_type = i; + } in + let td = new_entry (DW_TAG_typedef td) in + td::t + | Gdecl (s,n,t,_) -> + let i,t = type_to_dwarf t in + let at_decl = (match s with + | Storage_extern -> true + | _ -> false) in + let ext = (match s with + | Storage_static -> false + | _ -> true) in + let decl = { + variable_file_loc = (Some decl.gloc); + variable_declaration = Some at_decl; + 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 + decl::t + | Gfundef f -> + 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 decl.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 + fdef::e + | Genumdef (n,at,e) -> + let bs = sizeof_ikind enum_ikind in + let enum = { + enumeration_file_loc = Some decl.gloc; + enumeration_byte_size = bs; + enumeration_declaration = Some false; + enumeration_name = n.name; + } in + let id = get_composite_type n.name in + let child = List.map (fun (i,c,_) -> + new_entry (DW_TAG_enumerator ( + { + enumerator_file_loc = None; + enumerator_value = Int64.to_int c; + enumerator_name = i.name; + }))) e in + let enum = + { + tag = DW_TAG_enumeration_type enum; + children = child; + id = id;} in + [enum] + | Gcompositedef (sou,n,at,m) -> + let tag = (match sou with + | Struct -> + let info = Env.find_struct env n in + DW_TAG_structure_type { + structure_file_loc = Some decl.gloc; + structure_byte_size = info.ci_sizeof; + structure_declaration = Some false; + structure_name = n.name; + } + | Union -> + let info = Env.find_union env n in + DW_TAG_union_type { + union_file_loc = Some decl.gloc; + union_byte_size = info.ci_sizeof; + union_declaration = Some false; + union_name = n.name; + }) in + let id = get_composite_type n.name in + let children,e = + (match sou with + | Struct -> + (* This is the same layout used in Cutil *) + 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 = m.fld_name; + 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 = m.fld_name; + 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 + List.rev children,e + | Union -> 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 = f.fld_name; + member_type = t; + } in + new_entry (DW_TAG_member um),e@acc)[] m) in + let sou = { + tag = tag; + children = children; + id = id;} in + sou::e + | Gcompositedecl _ + | Gpragma _ -> [] + +let add_size prog debug = + let env = translEnv Env.empty prog in + entry_map (function + | DW_TAG_structure_type s -> + let _,info = Env.lookup_struct env s.structure_name in + DW_TAG_structure_type {s with structure_byte_size = info.ci_sizeof;} + | DW_TAG_union_type u -> + let _,info = Env.lookup_union env u.union_name in + DW_TAG_union_type {u with union_byte_size = info.ci_sizeof;} + | e -> e) debug + +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 defs = List.concat (List.map (globdecl_to_dwarf env) prog) 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/DwarfPrinter.ml b/debug/DwarfPrinter.ml new file mode 100644 index 00000000..dec3279e --- /dev/null +++ b/debug/DwarfPrinter.ml @@ -0,0 +1,502 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Printer for the Dwarf 2 debug information in ASM *) + +open DwarfTypes +open DwarfUtil +open Printf +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): + sig + val print_debug: out_channel -> dw_entry -> unit + end = + struct + + open Target + open DwarfAbbrevs + + (* Byte value to string *) + let string_of_byte value = + sprintf " .byte %s\n" (if value then "0x1" else "0x0") + + (* Print a label *) + let print_label oc lbl = + fprintf oc "%a:\n" label lbl + + (* Helper functions for abbreviation printing *) + let add_byte buf value = + Buffer.add_string buf (string_of_byte value) + + let add_abbr_uleb v buf = + Buffer.add_string buf (Printf.sprintf " .uleb128 %d\n" v) + + let add_abbr_entry (v1,v2) buf = + add_abbr_uleb v1 buf; + add_abbr_uleb v2 buf + + let add_file_loc buf = + let file,line = file_loc_type_abbr in + add_abbr_entry (0x3a,file) buf; + add_abbr_entry (0x3b,line) buf + + let add_type = add_abbr_entry (0x49,type_abbr) + + let add_name = add_abbr_entry (0x3,name_type_abbr) + + let add_byte_size = add_abbr_entry (0xb,byte_size_type_abbr) + + let add_high_pc = add_abbr_entry (0x12,high_pc_type_abbr) + + let add_low_pc = add_abbr_entry (0x11,low_pc_type_abbr) + + 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 + + (* Dwarf entity to string function *) + let abbrev_string_of_entity entity has_sibling = + let buf = Buffer.create 12 in + let add_attr_some v f = + match v with + | None -> () + | Some _ -> f buf in + let prologue id = + let has_child = match entity.children with + | [] -> false + | _ -> true in + add_abbr_uleb id buf; + add_byte buf has_child; + if has_sibling then add_abbr_entry (0x1,sibling_type_abbr) buf; + in + (match entity.tag with + | DW_TAG_array_type e -> + prologue 0x1; + add_attr_some e.array_type_file_loc add_file_loc; + add_type buf + | DW_TAG_base_type b -> + prologue 0x24; + add_byte_size buf; + add_attr_some b.base_type_encoding (add_abbr_entry (0x3e,encoding_type_abbr)); + add_name buf + | 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_abbr_entry (0x13,language_type_abbr) buf; + add_name buf; + add_abbr_entry (0x25,producer_type_abbr) buf; + add_abbr_entry (0x10,stmt_list_type_abbr) buf; + | DW_TAG_const_type _ -> + prologue 0x26; + add_type buf + | DW_TAG_enumeration_type e -> + prologue 0x4; + add_attr_some e.enumeration_file_loc add_file_loc; + add_byte_size buf; + add_attr_some e.enumeration_declaration add_declaration; + add_name buf + | DW_TAG_enumerator e -> + prologue 0x28; + add_attr_some e.enumerator_file_loc add_file_loc; + add_abbr_entry (0x1c,value_type_abbr) buf; + add_name buf + | DW_TAG_formal_parameter e -> + prologue 0x34; + 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)) + | DW_TAG_label _ -> + prologue 0xa; + add_low_pc buf; + add_name buf; + | DW_TAG_lexical_block _ -> + prologue 0xb; + add_high_pc buf; + add_low_pc buf + | DW_TAG_member e -> + prologue 0xd; + add_attr_some e.member_file_loc add_file_loc; + add_attr_some e.member_byte_size add_byte_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)); + (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_name buf; + add_type buf + | DW_TAG_pointer_type _ -> + prologue 0xf; + add_type buf + | DW_TAG_structure_type e -> + prologue 0x13; + add_attr_some e.structure_file_loc add_file_loc; + add_attr_some e.structure_byte_size add_byte_size; + add_attr_some e.structure_declaration add_declaration; + add_name buf + | DW_TAG_subprogram e -> + prologue 0x2e; + add_attr_some e.subprogram_file_loc add_file_loc; + add_attr_some e.subprogram_external (add_abbr_entry (0x3f,external_type_abbr)); + add_high_pc buf; + add_low_pc buf; + add_name buf; + add_abbr_entry (0x27,prototyped_type_abbr) buf; + add_attr_some e.subprogram_type add_type; + | DW_TAG_subrange_type e -> + prologue 0x21; + add_attr_some e.subrange_type add_type; + (match e.subrange_upper_bound with + | None -> () + | Some (BoundConst _) -> add_abbr_entry (0x2f,bound_const_type_abbr) buf + | Some (BoundRef _) -> add_abbr_entry (0x2f,bound_ref_type_abbr) buf) + | DW_TAG_subroutine_type e -> + prologue 0x15; + add_attr_some e.subroutine_type add_type; + add_abbr_entry (0x27,prototyped_type_abbr) buf + | DW_TAG_typedef e -> + prologue 0x16; + add_attr_some e.typedef_file_loc add_file_loc; + add_name buf; + add_type buf + | DW_TAG_union_type e -> + prologue 0x17; + add_attr_some e.union_file_loc add_file_loc; + add_attr_some e.union_byte_size add_byte_size; + add_attr_some e.union_declaration add_declaration; + add_name buf + | DW_TAG_unspecified_parameter e -> + prologue 0x18; + add_attr_some e.unspecified_parameter_file_loc add_file_loc; + 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_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; + add_type buf); + Buffer.contents buf + + let abbrev_start_addr = ref (-1) + + let curr_abbrev = ref 1 + + (* Function to get unique abbreviation ids *) + let next_abbrev () = + let abbrev = !curr_abbrev in + incr curr_abbrev;abbrev + + (* Mapping from abbreviation string to abbrevaiton id *) + let abbrev_mapping: (string,int) Hashtbl.t = Hashtbl.create 7 + + (* Look up the id of the abbreviation and add it if it is missing *) + let get_abbrev entity has_sibling = + let abbrev_string = abbrev_string_of_entity entity has_sibling in + (try + Hashtbl.find abbrev_mapping abbrev_string + with Not_found -> + let id = next_abbrev () in + Hashtbl.add abbrev_mapping abbrev_string id; + id) + + (* Compute the abbreviations of an entry and its children *) + let compute_abbrev entry = + entry_iter_sib (fun sib entry -> + let has_sib = match sib with + | None -> false + | Some _ -> true in + ignore (get_abbrev entry has_sib)) (fun _ -> ()) entry + + (* Print the debug_abbrev section using the previous computed abbreviations*) + 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); + let lbl = new_label () in + abbrev_start_addr := lbl; + print_label oc lbl; + List.iter (fun (s,id) -> + fprintf oc " .uleb128 %d\n" id; + output_string oc s; + fprintf oc " .uleb128 0\n"; + fprintf oc " .uleb128 0\n") abbrevs; + fprintf oc " .sleb128 0\n" + + let debug_start_addr = ref (-1) + + let entry_labels: (int,int) Hashtbl.t = Hashtbl.create 7 + + (* Translate the ids to address labels *) + let entry_to_label id = + try + Hashtbl.find entry_labels id + with Not_found -> + let label = new_label () in + Hashtbl.add entry_labels id label; + label + + (* Helper functions for debug printing *) + let print_opt_value oc o f = + match o with + | 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) + + let print_string oc s = + fprintf oc " .asciz \"%s\"\n" s + + let print_uleb128 oc d = + fprintf oc " .uleb128 %d\n" d + + let print_sleb128 oc d = + fprintf oc " .sleb128 %d\n" d + + 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_ref oc r = + let ref = entry_to_label r in + fprintf oc " .4byte %a\n" label ref + + let print_addr oc a = + fprintf oc " .4byte %a\n" label a + + let print_array_type oc at = + print_file_loc oc at.array_type_file_loc; + print_ref oc at.array_type + + let print_bound_value oc = function + | BoundConst bc -> print_uleb128 oc bc + | BoundRef br -> print_ref oc br + + let print_base_type oc bt = + print_byte oc bt.base_type_byte_size; + (match bt.base_type_encoding with + | Some e -> + let encoding = match e with + | DW_ATE_address -> 0x1 + | DW_ATE_boolean -> 0x2 + | DW_ATE_complex_float -> 0x3 + | DW_ATE_float -> 0x4 + | DW_ATE_signed -> 0x5 + | DW_ATE_signed_char -> 0x6 + | DW_ATE_unsigned -> 0x7 + | DW_ATE_unsigned_char -> 0x8 + in + print_byte oc encoding; + | None -> ()); + print_string oc bt.base_type_name + + let print_compilation_unit oc tag = + print_string oc (Sys.getcwd ()); + print_addr oc (get_start_addr ()); + print_addr oc (get_end_addr ()); + print_uleb128 oc 1; + print_string oc tag.compile_unit_name; + print_string oc ("CompCert "^Configuration.version); + print_addr oc (get_stmt_list_addr ()) + + let print_const_type oc ct = + print_ref oc ct.const_type + + let print_enumeration_type oc et = + print_file_loc oc et.enumeration_file_loc; + print_uleb128 oc et.enumeration_byte_size; + print_opt_value oc et.enumeration_declaration print_flag; + print_string oc et.enumeration_name + + let print_enumerator oc en = + print_file_loc oc en.enumerator_file_loc; + print_sleb128 oc en.enumerator_value; + print_string oc en.enumerator_name + + 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 + + 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 + + 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_string oc mb.member_name; + print_ref oc mb.member_type + + let print_pointer oc pt = + print_ref oc pt.pointer_type + + let print_structure oc st = + print_file_loc oc st.structure_file_loc; + print_opt_value oc st.structure_byte_size print_uleb128; + print_opt_value oc st.structure_declaration print_flag; + print_string oc st.structure_name + + let print_subprogram oc sp = + let s,e = get_fun_addr sp.subprogram_name in + print_file_loc oc sp.subprogram_file_loc; + print_opt_value oc sp.subprogram_external print_flag; + print_opt_value oc sp.subprogram_frame_base print_loc; + fprintf oc " .4byte %a\n" label s; + fprintf oc " .4byte %a\n" label e; + print_string oc sp.subprogram_name; + print_flag oc sp.subprogram_prototyped; + print_opt_value oc sp.subprogram_type print_ref + + let print_subrange oc sr = + print_opt_value oc sr.subrange_type print_ref; + print_opt_value oc sr.subrange_upper_bound print_bound_value + + let print_subroutine oc st = + print_opt_value oc st.subroutine_type print_ref; + print_flag oc st.subroutine_prototyped + + let print_typedef oc td = + print_file_loc oc td.typedef_file_loc; + print_string oc td.typedef_name; + print_ref oc td.typedef_type + + let print_union_type oc ut = + print_file_loc oc ut.union_file_loc; + print_opt_value oc ut.union_byte_size print_uleb128; + print_opt_value oc ut.union_declaration print_flag; + print_string oc ut.union_name + + let print_unspecified_parameter oc up = + print_file_loc oc up.unspecified_parameter_file_loc; + print_opt_value oc up.unspecified_parameter_artificial print_flag + + let print_variable oc var = + print_file_loc oc 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 = + print_ref oc vt.volatile_type + + (* Print an debug entry *) + let print_entry oc entry = + entry_iter_sib (fun sib entry -> + print_label oc (entry_to_label entry.id); + let has_sib = match sib with + | None -> false + | Some _ -> true in + let id = get_abbrev entry has_sib in + print_sleb128 oc id; + (match sib with + | None -> () + | Some s -> let lbl = entry_to_label s in + fprintf oc " .4byte %a-%a\n" label lbl label !debug_start_addr); + begin + match entry.tag with + | DW_TAG_array_type arr_type -> print_array_type oc arr_type + | DW_TAG_compile_unit comp -> print_compilation_unit oc comp + | DW_TAG_base_type bt -> print_base_type oc bt + | DW_TAG_const_type ct -> print_const_type oc ct + | DW_TAG_enumeration_type et -> print_enumeration_type oc et + | DW_TAG_enumerator et -> print_enumerator oc et + | DW_TAG_formal_parameter fp -> print_formal_parameter oc fp + | DW_TAG_label lb -> print_tag_label oc lb + | DW_TAG_lexical_block lb -> print_lexical_block oc lb + | DW_TAG_member mb -> print_member oc mb + | DW_TAG_pointer_type pt -> print_pointer oc pt + | DW_TAG_structure_type st -> print_structure oc st + | DW_TAG_subprogram sb -> print_subprogram oc sb + | DW_TAG_subrange_type sb -> print_subrange oc sb + | DW_TAG_subroutine_type st -> print_subroutine oc st + | DW_TAG_typedef tp -> print_typedef oc tp + | DW_TAG_union_type ut -> print_union_type oc ut + | DW_TAG_unspecified_parameter up -> print_unspecified_parameter oc up + | DW_TAG_variable var -> print_variable oc var + | DW_TAG_volatile_type vt -> print_volatile_type oc vt + end) (fun e -> + if e.children <> [] then + print_sleb128 oc 0) entry + + (* Print the debug abbrev section *) + let print_debug_abbrev oc entry = + compute_abbrev entry; + 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 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; + print_label oc debug_length_start; + fprintf oc " .2byte 0x2\n"; (* Dwarf version *) + print_addr oc !abbrev_start_addr; (* Offset into the abbreviation *) + print_byte oc !Machine.config.Machine.sizeof_ptr; (* Sizeof pointer type *) + print_entry oc entry; + print_sleb128 oc 0; + print_label oc debug_end (* End of the debug section *) + + + (* Print the debug info and abbrev section *) + let print_debug oc entry = + print_debug_abbrev oc entry; + print_debug_info oc entry + + end diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli new file mode 100644 index 00000000..d4fb0df9 --- /dev/null +++ b/debug/DwarfTypes.mli @@ -0,0 +1,271 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Types used for writing dwarf debug information *) + +open Sections + +(* Basic types for the value of attributes *) + +type constant = int + +type flag = bool + +type reference = int + +type encoding = + | DW_ATE_address + | DW_ATE_boolean + | DW_ATE_complex_float + | DW_ATE_float + | DW_ATE_signed + | DW_ATE_signed_char + | DW_ATE_unsigned + | DW_ATE_unsigned_char + +type address = int + +type block = string + +type location_value = + | LocConst of constant + | LocBlock of block + +type data_location_value = + | DataLocBlock of block + | DataLocRef of reference + +type bound_value = + | BoundConst of constant + | BoundRef of reference + +(* Types representing the attribute information per tag value *) + +type file_loc = string * constant + +type dw_tag_array_type = + { + array_type_file_loc: file_loc option; + array_type: reference; + } + +type dw_tag_base_type = + { + base_type_byte_size: constant; + base_type_encoding: encoding option; + base_type_name: string; + } + +type dw_tag_compile_unit = + { + compile_unit_name: string; + } + +type dw_tag_const_type = + { + const_type: reference; + } + +type dw_tag_enumeration_type = + { + enumeration_file_loc: file_loc option; + enumeration_byte_size: constant; + enumeration_declaration: flag option; + enumeration_name: string; + } + +type dw_tag_enumerator = + { + enumerator_file_loc: file_loc option; + enumerator_value: constant; + enumerator_name: string; + } + +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; + } + +type dw_tag_label = + { + label_low_pc: address; + label_name: string; + } + +type dw_tag_lexical_block = + { + lexical_block_high_pc: address; + lexical_block_low_pc: address; + } + +type dw_tag_member = + { + member_file_loc: file_loc option; + member_byte_size: constant option; + member_bit_offset: constant option; + member_bit_size: constant option; + member_data_member_location: data_location_value option; + member_declaration: flag option; + member_name: string; + member_type: reference; + } + +type dw_tag_pointer_type = + { + pointer_type: reference; + } + +type dw_tag_structure_type = + { + structure_file_loc: file_loc option; + structure_byte_size: constant option; + structure_declaration: flag option; + structure_name: string; + } + +type dw_tag_subprogram = + { + subprogram_file_loc: file_loc option; + subprogram_external: flag option; + subprogram_frame_base: location_value option; + subprogram_name: string; + subprogram_prototyped: flag; + subprogram_type: reference option; + } + +type dw_tag_subrange_type = + { + subrange_type: reference option; + subrange_upper_bound: bound_value option; + } + +type dw_tag_subroutine_type = + { + subroutine_type: reference option; + subroutine_prototyped: flag; + } + +type dw_tag_typedef = + { + typedef_file_loc: file_loc option; + typedef_name: string; + typedef_type: reference; + } + +type dw_tag_union_type = + { + union_file_loc: file_loc option; + union_byte_size: constant option; + union_declaration: flag option; + union_name: string; + } + +type dw_tag_unspecified_parameter = + { + unspecified_parameter_file_loc: file_loc option; + unspecified_parameter_artificial: flag option; + } + +type dw_tag_variable = + { + variable_file_loc: file_loc option; + variable_declaration: flag option; + variable_external: flag option; + variable_location: location_value option; + variable_name: string; + variable_segment: location_value option; + variable_type: reference; + } + +type dw_tag_volatile_type = + { + volatile_type: reference; + } + +type dw_tag = + | DW_TAG_array_type of dw_tag_array_type + | DW_TAG_base_type of dw_tag_base_type + | DW_TAG_compile_unit of dw_tag_compile_unit + | DW_TAG_const_type of dw_tag_const_type + | DW_TAG_enumeration_type of dw_tag_enumeration_type + | DW_TAG_enumerator of dw_tag_enumerator + | DW_TAG_formal_parameter of dw_tag_formal_parameter + | DW_TAG_label of dw_tag_label + | DW_TAG_lexical_block of dw_tag_lexical_block + | DW_TAG_member of dw_tag_member + | DW_TAG_pointer_type of dw_tag_pointer_type + | DW_TAG_structure_type of dw_tag_structure_type + | DW_TAG_subprogram of dw_tag_subprogram + | DW_TAG_subrange_type of dw_tag_subrange_type + | DW_TAG_subroutine_type of dw_tag_subroutine_type + | DW_TAG_typedef of dw_tag_typedef + | DW_TAG_union_type of dw_tag_union_type + | DW_TAG_unspecified_parameter of dw_tag_unspecified_parameter + | DW_TAG_variable of dw_tag_variable + | DW_TAG_volatile_type of dw_tag_volatile_type + +(* The type of the entries. *) + +type dw_entry = + { + tag: dw_tag; + children: dw_entry list; + id: reference; + } + + +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 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 + +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 + end diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml new file mode 100644 index 00000000..fe4a0f7b --- /dev/null +++ b/debug/DwarfUtil.ml @@ -0,0 +1,126 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Utility functions for the dwarf debuging type *) + +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 + { + tag = tag; + children = []; + id = id; + } + +(* Add an entry as child to another entry *) +let add_child entry child = + {entry with children = child::entry.children;} + + +(* Add entries as children to another entry *) +let add_children entry children = + {entry with children = entry.children@children;} + + +let list_iter_with_next f list = + let rec aux = (function + | [] -> () + | [a] -> f None a + | a::b::rest -> f (Some b.id) a; aux (b::rest)) in + aux list + +(* Iter over the tree and pass the sibling id *) +let entry_iter_sib f g entry = + let rec aux sib entry = + f sib entry; + list_iter_with_next aux entry.children; + g entry in + aux None entry + + +(* Fold over the tree in prefix order *) +let rec entry_fold f acc entry = + let acc = f acc entry.tag in + List.fold_left (entry_fold f) acc entry.children + +let rec entry_map f entry = + let t = f entry.tag in + let children = List.map (entry_map f) entry.children in + { + entry with + tag = t; + children = children; + } + +(* Attribute form encoding *) +let dw_form_addr = 0x01 +let dw_form_block2 = 0x03 +let dw_form_block4 = 0x04 +let dw_form_data2 = 0x05 +let dw_form_data4 = 0x06 +let dw_form_data8 = 0x07 +let dw_form_string = 0x08 +let dw_form_block = 0x09 +let dw_form_block1 = 0x0a +let dw_form_data1 = 0x0b +let dw_form_flag = 0x0c +let dw_form_sdata = 0x0d +let dw_form_strp = 0x0e +let dw_form_udata = 0x0f +let dw_form_ref_addr = 0x10 +let dw_form_ref1 = 0x11 +let dw_form_ref2 = 0x12 +let dw_form_ref4 = 0x13 +let dw_form_ref8 = 0x14 +let dw_ref_udata = 0x15 +let dw_ref_indirect = 0x16 + +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 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 diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 0012dc0c..48c31767 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -93,4 +93,10 @@ let asm_supports_cfi = | "false" -> false | v -> bad_config "asm_supports_cfi" [v] +let advanced_debug = + match get_config_string "advanced_debug" with + | "true" -> true + | "false" -> false + | v -> bad_config "advanced_debug" [v] + let version = get_config_string "version" diff --git a/driver/Driver.ml b/driver/Driver.ml index d22dd77c..1191982d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -117,17 +117,17 @@ let parse_c_file sourcename ifile = ^ (if !option_fpacked_structs then "p" else "") in (* Parsing and production of a simplified C AST *) - let ast = + let ast,debug = match Parse.preprocessed_file simplifs sourcename ifile with - | None -> exit 2 - | Some p -> p in + | None,_ -> exit 2 + | Some p,d -> p,d in (* Save C AST if requested *) if !option_dparse then begin let ofile = output_filename sourcename ".c" ".parsed.c" in let oc = open_out ofile in Cprint.program (Format.formatter_of_out_channel oc) ast; close_out oc - end; + end; (* Conversion to Csyntax *) let csyntax = match Timing.time "CompCert C generation" C2C.convertProgram ast with @@ -141,7 +141,7 @@ let parse_c_file sourcename ifile = PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; close_out oc end; - csyntax + csyntax,debug (* Dump Asm code in binary format for the validator *) @@ -157,7 +157,7 @@ let dump_asm asm destfile = (* From CompCert C AST to asm *) -let compile_c_ast sourcename csyntax ofile = +let compile_c_ast sourcename csyntax ofile debug = (* Prepare to dump Clight, RTL, etc, if requested *) let set_dest dst opt ext = dst := if !opt then Some (output_filename sourcename ".c" ext) @@ -181,13 +181,14 @@ let compile_c_ast sourcename csyntax ofile = dump_asm asm (output_filename sourcename ".c" ".sdump"); (* Print Asm in text form *) let oc = open_out ofile in - PrintAsm.print_program oc asm; + PrintAsm.print_program oc asm debug; close_out oc (* From C source to asm *) let compile_c_file sourcename ifile ofile = - compile_c_ast sourcename (parse_c_file sourcename ifile) ofile + let ast,debug = parse_c_file sourcename ifile in + compile_c_ast sourcename ast ofile debug (* From Cminor to asm *) @@ -212,7 +213,7 @@ let compile_cminor_file ifile ofile = exit 2 | Errors.OK p -> let oc = open_out ofile in - PrintAsm.print_program oc p; + PrintAsm.print_program oc p None; close_out oc with Parsing.Parse_error -> eprintf "File %s, character %d: Syntax error\n" @@ -265,7 +266,7 @@ let process_c_file sourcename = let preproname = Filename.temp_file "compcert" ".i" in preprocess sourcename preproname; if !option_interp then begin - let csyntax = parse_c_file sourcename preproname in + let csyntax,_ = parse_c_file sourcename preproname in safe_remove preproname; Interp.execute csyntax; "" @@ -292,7 +293,7 @@ let process_c_file sourcename = let process_i_file sourcename = if !option_interp then begin - let csyntax = parse_c_file sourcename sourcename in + let csyntax,_ = parse_c_file sourcename sourcename in Interp.execute csyntax; "" end else if !option_S then begin @@ -509,7 +510,7 @@ let cmdline_actions = Exact "-fall", Self (fun _ -> set_all language_support_options); Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) - Exact "-g", Self (fun s -> option_g := true; push_linker_arg s); + Exact "-g", Self (fun s -> option_g := true); (* Code generation options -- more below *) Exact "-O0", Self (fun _ -> unset_all optimization_options); Exact "-O", Self (fun _ -> set_all optimization_options); diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 888a7e72..d2d8440f 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -972,6 +972,19 @@ module Target(System: SYSTEM):TARGET = let comment = comment let default_falignment = 16 + + let get_start_addr () = -1 (* Dummy constant *) + + let get_end_addr () = -1 (* Dummy constant *) + + let get_stmt_list_addr () = -1 (* Dummy constant *) + + module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs (* Dummy Abbrev types *) + + let label = label + + let new_label = new_label + end let sel_target () = diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 70aec6c0..50a00b9e 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -38,6 +38,8 @@ module type SYSTEM = val cfi_adjust: out_channel -> int32 -> unit val cfi_rel_offset: out_channel -> string -> int32 -> unit val print_prologue: out_channel -> unit + val print_epilogue: out_channel -> unit + val print_file_loc: out_channel -> DwarfTypes.file_loc -> unit end let symbol = elf_symbol @@ -68,6 +70,14 @@ let float_reg_name = function | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27" | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31" +let start_addr = ref (-1) + +let end_addr = ref (-1) + +let stmt_list_addr = ref (-1) + +let label = elf_label + module Linux_System : SYSTEM = struct @@ -117,6 +127,9 @@ 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_abbrev -> ".debug_abbrev,\"\",@progbits" + let print_file_line oc file line = PrintAnnot.print_file_line oc comment file line @@ -131,6 +144,10 @@ module Linux_System : SYSTEM = let cfi_rel_offset = cfi_rel_offset let print_prologue oc = () + + let print_epilogue oc = () + + let print_file_loc _ _ = () end @@ -182,9 +199,11 @@ 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" let print_file_line oc file line = - PrintAnnot.print_file_line_d1 oc comment file line + PrintAnnot.print_file_line_d2 oc comment file line (* Emit .cfi directives *) let cfi_startproc oc = () @@ -198,8 +217,40 @@ module Diab_System : SYSTEM = let print_prologue oc = fprintf oc " .xopt align-fill-text=0x60000000\n"; if !Clflags.option_g then - fprintf oc " .xopt asm-debug-on\n" - + 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 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"; + Hashtbl.iter (fun file _ -> + let label = new_label () in + Hashtbl.add filenum file label; + fprintf oc ".L%d: .d2filenum \"%s\"\n" label file) PrintAnnot.filename_info; + fprintf oc " .d2_line_end\n" + end + + let print_file_loc oc (file,col) = + fprintf oc " .4byte %a\n" label (Hashtbl.find filenum file); + fprintf oc " .uleb128 %d\n" col + end module Target (System : SYSTEM):TARGET = @@ -212,7 +263,7 @@ module Target (System : SYSTEM):TARGET = let raw_symbol oc s = fprintf oc "%s" s - let label = elf_label + let label = label let label_low oc lbl = fprintf oc ".L%d@l" lbl @@ -726,8 +777,6 @@ module Target (System : SYSTEM):TARGET = let print_align oc align = fprintf oc " .balign %d\n" align - let print_epilogue _ = () - let print_jumptable oc jmptbl = let print_jumptable oc (lbl, tbl) = fprintf oc "%a:" label lbl; @@ -742,6 +791,17 @@ module Target (System : SYSTEM):TARGET = end let default_falignment = 4 + + let get_start_addr () = !start_addr + + let get_end_addr () = !end_addr + + let get_stmt_list_addr () = !stmt_list_addr + + module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs + + let new_label = new_label + end let sel_target () = |