Merge branch 'dwarf' of /local/schommer/trunk/build/compcert.ppc/compcert into dwarf

Author: bschommer

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)"; \
          echo "struct_passing_style=$(STRUCT_PASSING)"; \
          echo "struct_return_style=$(STRUCT_RETURN)"; \
          version=`cat VERSION`; \

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
 

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 () = 

backend/PrintAnnot.ml

@@ -21,6 +21,13 @@ open AST
 open Memdata
 open Asm
 
+(** 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
+
+
 (** Line number annotations *)
 
 let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t
@@ -66,21 +73,21 @@ 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
         Hashtbl.find filename_info file
       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

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,15 +109,37 @@ 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 ();
   PrintAnnot.print_version_and_options oc Target.comment;
   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

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

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 *)

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 =

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

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

configure

@@ -19,6 +19,7 @@ toolprefix=''
 target=''
 has_runtime_lib=true
 build_checklink=true
+advanced_debug=false
 
 usage='Usage: ./configure [options] target
 
@@ -113,7 +114,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
@@ -357,6 +359,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'

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. *)
 

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

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