aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile3
-rw-r--r--Makefile.extr2
-rw-r--r--arm/TargetPrinter.ml12
-rw-r--r--backend/PrintAnnot.ml8
-rw-r--r--backend/PrintAsm.ml54
-rw-r--r--backend/PrintAsm.mli4
-rw-r--r--backend/PrintAsmaux.ml8
-rw-r--r--checklink/Check.ml4
-rw-r--r--common/Sections.ml2
-rw-r--r--common/Sections.mli2
-rwxr-xr-xconfigure5
-rw-r--r--cparser/Cutil.mli2
-rw-r--r--cparser/Parse.ml21
-rw-r--r--cparser/Parse.mli2
-rw-r--r--debug/CtoDwarf.ml392
-rw-r--r--debug/DwarfPrinter.ml502
-rw-r--r--debug/DwarfTypes.mli271
-rw-r--r--debug/DwarfUtil.ml126
-rw-r--r--driver/Configuration.ml6
-rw-r--r--driver/Driver.ml25
-rw-r--r--ia32/TargetPrinter.ml13
-rw-r--r--powerpc/TargetPrinter.ml72
22 files changed, 1494 insertions, 42 deletions
diff --git a/Makefile b/Makefile
index 6fd8d2a6..44381d7e 100644
--- a/Makefile
+++ b/Makefile
@@ -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
diff --git a/configure b/configure
index f9591c0b..60ea1be7 100755
--- a/configure
+++ b/configure
@@ -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 () =
generated by cgit (git 2.34.1) at 2024-07-03 18:19:25 +0000