aboutsummaryrefslogtreecommitdiffstats
path: root/debug
diff options
context:
space:
mode:
Diffstat (limited to 'debug')
-rw-r--r--debug/CtoDwarf.ml543
-rw-r--r--debug/Debug.ml103
-rw-r--r--debug/Debug.mli32
-rw-r--r--debug/DebugInformation.ml670
-rw-r--r--debug/DwarfPrinter.ml61
-rw-r--r--debug/DwarfTypes.mli29
-rw-r--r--debug/DwarfUtil.ml12
-rw-r--r--debug/Dwarfgen.ml259
8 files changed, 1114 insertions, 595 deletions
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..10b4e68f
--- /dev/null
+++ b/debug/Debug.ml
@@ -0,0 +1,103 @@
+(* *********************************************************************)
+(* *)
+(* 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 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: unit -> dw_entry option;
+ mutable all_files_iter: (string -> unit) -> unit;
+ mutable insert_local_declaration: int -> storage -> ident -> typ -> location -> unit;
+ mutable atom_local_variable: ident -> atom -> unit;
+ mutable enter_scope: int -> int -> unit;
+ mutable enter_function_scope: ident -> int -> unit;
+ }
+
+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 _ _ -> ());
+}
+
+let init () =
+ if !Clflags.option_g then begin
+ 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 () -> Some (Dwarfgen.gen_debug_info ()));
+ 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;
+ end else begin
+ 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 _ _ -> ());
+ end
+
+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 () = implem.generate_debug_info ()
+let all_files_iter f = implem.all_files_iter f
+let insert_local_declaration scope sto id ty loc = implem.insert_local_declaration scope 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
diff --git a/debug/Debug.mli b/debug/Debug.mli
new file mode 100644
index 00000000..087f073f
--- /dev/null
+++ b/debug/Debug.mli
@@ -0,0 +1,32 @@
+(* *********************************************************************)
+(* *)
+(* 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 Camlcoq
+open DwarfTypes
+
+
+val init: unit -> unit
+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 generate_debug_info: unit -> dw_entry option
+val all_files_iter: (string -> unit) -> unit
+val insert_local_declaration: int -> storage -> ident -> typ -> location -> unit
+val atom_local_variable: ident -> atom -> unit
+val enter_scope: int -> int -> unit
+val enter_function_scope: ident -> int -> unit
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
new file mode 100644
index 00000000..a85f2081
--- /dev/null
+++ b/debug/DebugInformation.ml
@@ -0,0 +1,670 @@
+(* *********************************************************************)
+(* *)
+(* 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 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
+
+(* 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
+ let old = !Cprint.print_idents_in_full in
+ Cprint.print_idents_in_full := true;
+ Cprint.typ chan ty;
+ Cprint.print_idents_in_full := old;
+ 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 t = {
+ typedef_file_loc = None;
+ typedef_name = id.name;
+ typ = None;
+ } 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_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 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 to debug id *)
+let scope_to_local: (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 id =
+ let id = (Hashtbl.find scope_to_local 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
+ | 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_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
+ insert (Function fd) f.fd_name.stamp
+ | 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.map (fun a -> if name a then
+ {a with cfd_byte_offset = Some offset;}
+ else a) 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.map (fun a -> if name a then
+ {a with cfd_bit_offset = Some offset; cfd_bitfield = Some underlying; cfd_byte_size = Some size}
+ else
+ a) 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
+ 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 var_id s_id =
+ try
+ let s_id',scope = find_scope_id s_id in
+ replace_scope s_id' ({scope_variables = var_id::scope.scope_variables;})
+ with Not_found -> ()
+
+let insert_local_declaration scope sto id ty loc =
+ let ty = find_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';
+ add_lvar_scope id' scope
+
+let new_scope sc_id =
+ let scope = {scope_variables = [];} in
+ let id = next_id () in
+ Hashtbl.add local_variables id (Scope scope);
+ Hashtbl.add scope_to_local sc_id id;
+ id
+
+let enter_function_scope fun_id sc_id =
+ try
+ let id = new_scope sc_id in
+ let fun_id,f = find_fun_stamp fun_id.stamp in
+ replace_fun id ({f with fun_scope = Some id})
+ with Not_found -> ()
+
+let enter_scope p_id id =
+ try
+ let id' = new_scope id in
+ let p_id',scope = find_scope_id p_id in
+ replace_scope p_id' ({scope_variables = id'::scope.scope_variables;})
+ with Not_found -> ()
+
+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 atom_to_definition;
+ Hashtbl.reset local_variables;
+ Hashtbl.reset stamp_to_local;
+ Hashtbl.reset atom_to_local;
+ Hashtbl.reset scope_to_local;
+
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index 15843eb9..5e58e365 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -64,16 +64,12 @@ 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 (LocSymbol _) ->add_abbr_entry (0x2,location_block_type_abbr) buf
| Some (LocConst _) -> add_abbr_entry (0x2,location_const_type_abbr) buf
| Some (LocBlock _) -> add_abbr_entry (0x2,location_block_type_abbr) buf
@@ -129,9 +125,7 @@ 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))
| DW_TAG_label _ ->
@@ -145,16 +139,16 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
| 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 +160,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 +195,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;
@@ -295,10 +289,20 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
fprintf oc " .byte 0x%X\n" b
let print_loc oc loc =
- ()
+ match loc with
+ | LocSymbol s ->
+ fprintf oc " .sleb128 5\n";
+ fprintf oc " .byte 3\n";
+ fprintf oc " .4byte %a\n" symbol s
+ | _ -> ()
let print_data_location oc dl =
- ()
+ match dl with
+ | DataLocBlock [DW_OP_plus_uconst i] ->
+ fprintf oc " .sleb128 2\n";
+ fprintf oc " .byte 0x23\n";
+ fprintf oc " .byte %d\n" i
+ | _ -> ()
let print_ref oc r =
let ref = entry_to_label r in
@@ -360,9 +364,7 @@ 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
@@ -379,10 +381,11 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
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 +401,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 +433,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 =
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index eaf07e1e..b5be3121 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -13,6 +13,7 @@
(* Types used for writing dwarf debug information *)
open Sections
+open Camlcoq
(* Basic types for the value of attributes *)
@@ -36,12 +37,18 @@ type address = int
type block = string
+type location_expression =
+ | DW_OP_plus_uconst of constant
+ | DW_OP
+
+
type location_value =
+ | LocSymbol of atom
| LocConst of constant
| LocBlock of block
type data_location_value =
- | DataLocBlock of block
+ | DataLocBlock of location_expression list
| DataLocRef of reference
type bound_value =
@@ -94,9 +101,7 @@ 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;
}
@@ -140,12 +145,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 +189,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 =
@@ -269,5 +274,7 @@ module type DWARF_TARGET=
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 get_location: int -> location_value option
+ val get_frame_base: int -> location_value option
+ val symbol: out_channel -> atom -> unit
end
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml
index f47c2b58..4cd838b6 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 = [];
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
new file mode 100644
index 00000000..bb0ab5f2
--- /dev/null
+++ b/debug/Dwarfgen.ml
@@ -0,0 +1,259 @@
+(* *********************************************************************)
+(* *)
+(* 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 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
+
+(* 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 typedef_to_entry id t =
+ let i = get_opt_val t.typ in
+ let td = {
+ typedef_file_loc = 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 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 = 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;
+ } 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 = Some (DataLocBlock [DW_OP_plus_uconst (get_opt_val mem.cfd_byte_offset)]);
+ 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 id s =
+ let tag = {
+ structure_file_loc = 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 id s =
+ let tag = {
+ union_file_loc = 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 id s =
+ match s.ct_sou with
+ | Struct -> struct_to_entry id s
+ | Union -> union_to_entry id s
+
+let infotype_to_entry 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 id c
+ | EnumType e -> enum_to_entry id e
+ | FunctionType f -> fun_type_to_entry id f
+ | Typedef t -> typedef_to_entry id t
+ | ConstType c -> const_to_entry id c
+ | VolatileType v -> volatile_to_entry id v
+ | Void -> void_to_entry id
+
+let gen_types () =
+ List.rev (Hashtbl.fold (fun id t acc -> (infotype_to_entry id t)::acc) types [])
+
+let global_variable_to_entry id v =
+ let var = {
+ variable_file_loc = 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)
+
+let function_parameter_to_entry p =
+ 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;
+ } in
+ new_entry (next_id ()) (DW_TAG_formal_parameter p)
+
+let local_variable_to_entry v id =
+ let var = {
+ variable_file_loc = v.lvar_file_loc;
+ variable_declaration = None;
+ variable_external = None;
+ variable_name = v.lvar_name;
+ variable_type = v.lvar_type;
+ variable_location = None;
+ } in
+ new_entry id (DW_TAG_variable var)
+
+let function_to_entry id f =
+ let f_tag = {
+ subprogram_file_loc = 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_entry = new_entry id (DW_TAG_subprogram f_tag) in
+ let params = List.map function_parameter_to_entry f.fun_parameter in
+(* let vars = List.map local_variable_to_entry f.fun_locals in*)
+ add_children f_entry params
+
+let definition_to_entry id t =
+ match t with
+ | GlobalVariable g -> global_variable_to_entry id g
+ | Function f -> function_to_entry id f
+
+let gen_defs () =
+ List.rev (Hashtbl.fold (fun id t acc -> (definition_to_entry id t)::acc) definitions [])
+
+let gen_debug_info () =
+ let cp = {
+ compile_unit_name = !file_name;
+ } in
+ let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in
+ add_children cp ((gen_types ()) @ (gen_defs ()))
generated by cgit (git 2.34.1) at 2024-06-02 15:01:56 +0000