Activating the printing of the debug information for supported architecture.

4 files changed, 48 insertions, 17 deletions

diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 510dbc64..05b55a10 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -88,6 +88,8 @@ module Printer(Target:TARGET) =
       | Gfun (Internal code) -> print_function oc name code
       | Gfun (External ef) ->   ()
       | Gvar v -> print_var oc name v
+
+    module DebugPrinter = DwarfPrinter (Target)
             
   end
 
@@ -102,6 +104,8 @@ let print_program oc p db =
   PrintAnnot.close_filenames ();
   if !Clflags.option_g && Configuration.advanced_debug then
     begin
-      let module DebugPrinter = DwarfPrinter(Target) in
-      ()
+      match db with
+      | None -> ()
+      | Some db ->
+          Printer.DebugPrinter.print_debug oc db
     end
diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml
index b7f417f6..206061b6 100644
--- a/debug/CtoDwarf.ml
+++ b/debug/CtoDwarf.ml
@@ -111,7 +111,7 @@ let rec type_to_dwarf (typ: typ): int * dw_entry list =
             Some ret,et) in
           let prototyped,children,others =
             (match args with 
-            | None ->
+            | None -> 
                 let u = {
                   unspecified_parameter_file_loc = None;
                   unspecified_parameter_artificial = None;
@@ -182,3 +182,21 @@ let rec type_to_dwarf (typ: typ): int * dw_entry list =
     Hashtbl.add type_table typ_string id;
     id,entries
         
+let rec globdecl_to_dwarf decl =
+  match decl.gdesc with
+  | Gtypedef (n,t) -> let i,t = type_to_dwarf t in
+    Hashtbl.add defined_types_table n.name i;
+    t
+  | Gpragma _ 
+  | _ ->  []
+
+let program_to_dwarf prog name =
+  Hashtbl.reset type_table;
+  Hashtbl.reset defined_types_table;
+  reset_id ();
+  let defs = List.concat (List.map globdecl_to_dwarf 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
index 0b175563..6010ac20 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -25,6 +25,7 @@ module DwarfPrinter(Target: TARGET) :
 
     open Target
 
+      
     let string_of_byte value =
       sprintf "	.byte		%s\n" (if value then "0x1" else "0x0")
 
@@ -328,11 +329,15 @@ module DwarfPrinter(Target: TARGET) :
       ()
 
     let print_ref oc r =
-      print_label oc (entry_to_label 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_label oc (entry_to_label at.array_type)
+      print_ref oc at.array_type
 
     let print_bound_value oc = function
       | BoundConst bc -> print_uleb128 oc bc
@@ -358,12 +363,12 @@ module DwarfPrinter(Target: TARGET) :
 
     let print_compilation_unit oc tag =
       print_string oc (Sys.getcwd ());
-      print_label oc (get_start_addr ());
-      print_label oc (get_end_addr ());
+      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_label oc (get_stmt_list_addr ())
+      print_addr oc (get_stmt_list_addr ())
 
     let print_const_type oc ct =
       print_ref oc ct.const_type
@@ -461,7 +466,7 @@ module DwarfPrinter(Target: TARGET) :
 
     let  print_entry oc entry =
       entry_iter_sib (fun sib entry ->
-        print_ref oc entry.id;
+        print_label oc (entry_to_label entry.id);
         let has_sib = match sib with
         | None -> false
         | Some _ -> true in
@@ -512,7 +517,7 @@ module DwarfPrinter(Target: TARGET) :
       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 *)
-      fprintf oc "	.4byte		%a\n" label !abbrev_start_addr; (* Offset into the abbreviation *)
+      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;
diff --git a/driver/Driver.ml b/driver/Driver.ml
index f14b2671..80a5891c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -129,6 +129,9 @@ let parse_c_file sourcename ifile =
     Cprint.program (Format.formatter_of_out_channel oc) ast;
     close_out oc
   end;
+  let debug = if !option_g && Configuration.advanced_debug then
+    Some (program_to_dwarf ast sourcename) 
+  else None in
   (* Conversion to Csyntax *)
   let csyntax =
     match Timing.time "CompCert C generation" C2C.convertProgram ast with
@@ -142,7 +145,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 *)
 
@@ -158,7 +161,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)
@@ -182,13 +185,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 None;
+  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 *)
 
@@ -266,7 +270,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;
       ""
@@ -293,7 +297,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