Filled in the rest of the funciton needed for thte debug info under arm.

The name_of_section function no returns the correct name for the
debug sections, the prologue and epilogue directives are added and
the labels for the live ranges are introduced in the Asmexpand pass.

8 files changed, 84 insertions, 24 deletions

diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index da08bf7c..b5bbc664 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -395,17 +395,59 @@ let expand_instruction instr =
   | _ ->
      emit instr
 
-let expand_function fn =
+let int_reg_to_dwarf = function
+   | IR0 -> 0  | IR1 -> 1  | IR2 -> 2  | IR3 -> 3
+   | IR4 -> 4  | IR5 -> 5  | IR6 -> 6  | IR7 -> 7
+   | IR8 -> 8  | IR9 -> 9  | IR10 -> 10 | IR11 -> 11
+   | IR12 -> 12 | IR13 -> 13 | IR14 -> 14
+
+let float_reg_to_dwarf = function
+   | FR0 -> 64  | FR1 -> 65  | FR2 -> 66  | FR3 -> 67
+   | FR4 -> 68  | FR5 -> 69  | FR6 -> 70  | FR7 -> 71
+   | FR8 -> 72  | FR9 -> 73  | FR10 -> 74 | FR11 -> 75
+   | FR12 -> 76 | FR13 -> 77 | FR14 -> 78 | FR15 -> 79
+
+let preg_to_dwarf_int = function
+   | IR r -> int_reg_to_dwarf r
+   | FR r -> float_reg_to_dwarf r
+   | _ -> assert false
+
+let translate_annot annot = 
+  let rec aux = function
+    | BA x -> Some (13,BA (preg_to_dwarf_int x))
+    | BA_int _
+    | BA_long _
+    | BA_float _
+    | BA_single _
+    | BA_loadglobal _
+    | BA_addrglobal _
+    | BA_loadstack _ -> None
+    | BA_addrstack ofs -> Some (13,BA_addrstack ofs)
+    | BA_splitlong (hi,lo) -> 
+        begin
+          match (aux hi,aux lo) with
+          | Some (_,hi) ,Some (_,lo) -> Some (13,BA_splitlong (hi,lo))
+          | _,_ -> None
+        end in
+  (match annot with
+  | [] -> None
+  | a::_ -> aux a)
+
+
+let expand_function id fn =
   try
     set_current_function fn;
-    List.iter expand_instruction fn.fn_code;
+    if !Clflags.option_g then
+      expand_debug id translate_annot expand_instruction fn.fn_code
+    else
+      List.iter expand_instruction fn.fn_code;
     Errors.OK (get_current_function ())
   with Error s ->
     Errors.Error (Errors.msg (coqstring_of_camlstring s))
 
-let expand_fundef _ = function
+let expand_fundef id = function
   | Internal f ->
-      begin match expand_function f with
+      begin match expand_function id f with
       | Errors.OK tf -> Errors.OK (Internal tf)
       | Errors.Error msg -> Errors.Error msg
       end
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index fc11f649..2e676090 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -153,9 +153,11 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | 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 _
-      | Section_debug_loc
-      | Section_debug_abbrev -> "" (* Dummy value *)
+      | Section_debug_info _ -> ".section	.debug_info,\"\",%progbits"
+      | Section_debug_loc -> ".section	.debug_loc,\"\",%progbits"
+      | Section_debug_abbrev -> ".section	.debug_abbrev,\"\",%progbits"
+      | Section_debug_line _ -> ".section	.debug_line,\"\",%progbits"
+
             
     let section oc sec =
       fprintf oc "	%s\n" (name_of_section sec)
@@ -896,9 +898,25 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
         | _ -> "armv7");
       fprintf oc "	.fpu	%s\n"
         (if Opt.vfpv3 then "vfpv3-d16" else "vfpv2");
-      fprintf oc "	.%s\n" (if !Clflags.option_mthumb then "thumb" else "arm")
+      fprintf oc "	.%s\n" (if !Clflags.option_mthumb then "thumb" else "arm");
+      if !Clflags.option_g then begin
+        section oc Section_text;
+        let low_pc = new_label () in
+        Debug.add_compilation_section_start ".text" low_pc;
+        fprintf oc "%a:\n" elf_label low_pc;
+        fprintf oc "	.cfi_sections	.debug_frame\n"
+      end
+
+
+    let print_epilogue oc = 
+      if !Clflags.option_g then begin
+        let high_pc = new_label () in
+        Debug.add_compilation_section_end ".text" high_pc;
+        Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
+        section oc Section_text;
+        fprintf oc "%a:\n" elf_label high_pc
+        end
 
-    let print_epilogue oc = ()
 
     let default_falignment = 4
     
diff --git a/common/Sections.ml b/common/Sections.ml
index be0f415e..cc8b0758 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -30,6 +30,7 @@ type section_name =
   | Section_debug_info of string
   | Section_debug_abbrev
   | Section_debug_loc
+  | Section_debug_line of string
 
 type access_mode =
   | Access_default
diff --git a/common/Sections.mli b/common/Sections.mli
index cf6f13b8..7a8c8225 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -29,6 +29,7 @@ type section_name =
   | Section_debug_info of string
   | Section_debug_abbrev
   | Section_debug_loc
+  | Section_debug_line of string
 
 type access_mode =
   | Access_default
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index 2a54fa6a..1bd54470 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -627,7 +627,7 @@ module DwarfPrinter(Target: DWARF_TARGET):
       print_abbrev oc;
       section oc Section_debug_loc;
       print_location_list oc loc;
-      fprintf oc "	.section	.debug_line,\"\",@progbits\n";
+      section oc (Section_debug_line "");
       print_label oc line_start
 
     (* Print the debug info and abbrev section *)
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 19b4b10a..371be558 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -104,6 +104,7 @@ module Cygwin_System : SYSTEM =
             s (if ex then "xr" else if wr then "d" else "dr")
       | Section_debug_info _
       | Section_debug_loc
+      | Section_debug_line _
       | Section_debug_abbrev -> "" (* Dummy value *)
 
     let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
@@ -153,7 +154,8 @@ module ELF_System : SYSTEM =
           sprintf ".section	\"%s\",\"a%s%s\",@progbits"
             s (if wr then "w" else "") (if ex then "x" else "")
       | Section_debug_info _
-      | Section_debug_loc
+      | Section_debug_loc 
+      | Section_debug_line _
       | Section_debug_abbrev -> "" (* Dummy value *)
             
     let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
@@ -207,6 +209,7 @@ module MacOS_System : SYSTEM =
             (if ex then "regular, pure_instructions" else "regular")
       | Section_debug_info _
       | Section_debug_loc
+      | Section_debug_line _
       | Section_debug_abbrev -> "" (* Dummy value *)
     
     let stack_alignment =  16 (* mandatory *)
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index bf7e4c3e..fb569a00 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -563,7 +563,7 @@ let num_crbit = function
   | CRbit_3 -> 3
   | CRbit_6 -> 6
 
-let expand_instruction_simple instr =
+let expand_instruction instr =
   match instr with
   | Pallocframe(sz, ofs,retofs) ->
       let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in
@@ -687,19 +687,13 @@ let translate_annot annot =
   | [] -> None
   | a::_ -> aux a)
 
-let expand_scope id lbl oldscopes newscopes =
-  let opening = List.filter (fun a -> not (List.mem a oldscopes)) newscopes
-  and closing = List.filter (fun a -> not (List.mem a newscopes)) oldscopes in
-  List.iter (fun i -> Debug.open_scope id i lbl) opening;
-  List.iter (fun i -> Debug.close_scope id i lbl) closing
-    
 let expand_function id fn =
   try
     set_current_function fn;
     if !Clflags.option_g then
-      expand_debug id translate_annot expand_instruction_simple fn.fn_code
+      expand_debug id translate_annot expand_instruction fn.fn_code
     else
-      List.iter expand_instruction_simple fn.fn_code;
+      List.iter expand_instruction fn.fn_code;
     Errors.OK (get_current_function ())
   with Error s ->
     Errors.Error (Errors.msg (coqstring_of_camlstring s))
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 530e269d..0f0ed357 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -126,7 +126,9 @@ module Linux_System : SYSTEM =
       | Section_debug_info _ -> ".section	.debug_info,\"\",@progbits"
       | Section_debug_abbrev -> ".section	.debug_abbrev,\"\",@progbits"
       | Section_debug_loc -> ".section	.debug_loc,\"\",@progbits"
-            
+      | Section_debug_line _ ->  ".section	.debug_line,\"\",@progbits\n"
+
+
     let section oc sec =
       let name = name_of_section sec in
       assert (name <> "COMM");
@@ -146,9 +148,7 @@ module Linux_System : SYSTEM =
     let cfi_rel_offset = cfi_rel_offset
 
     let print_prologue oc = 
-      if !Clflags.option_g then
-        begin
-      (* TODO print file *)
+      if !Clflags.option_g then  begin
           section oc Section_text;
           let low_pc = new_label () in
           Debug.add_compilation_section_start ".text" low_pc;
@@ -220,6 +220,7 @@ module Diab_System : SYSTEM =
       | Section_debug_info s -> sprintf ".section	.debug_info%s,,n" (if s <> ".text" then s else "")
       | Section_debug_abbrev -> ".section	.debug_abbrev,,n"
       | Section_debug_loc -> ".section	.debug_loc,,n"
+      | Section_debug_line s -> sprintf ".section	.debug_line.%s,,n\n" s;
 
     let section oc sec =
       let name = name_of_section sec in