Filled in missing functions for debug information on ia32.

Like for arm and ppc the functions for section names and start and
end addresses of compilation units are defined and the print_annot
function is moved to Asmexpandaux.ml.

5 files changed, 91 insertions, 87 deletions

diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index b5bbc664..990f207d 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -407,38 +407,17 @@ let float_reg_to_dwarf = function
    | FR8 -> 72  | FR9 -> 73  | FR10 -> 74 | FR11 -> 75
    | FR12 -> 76 | FR13 -> 77 | FR14 -> 78 | FR15 -> 79
 
-let preg_to_dwarf_int = function
+let preg_to_dwarf = 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;
     if !Clflags.option_g then
-      expand_debug id translate_annot expand_instruction fn.fn_code
+      expand_debug id 13 preg_to_dwarf expand_instruction fn.fn_code
     else
       List.iter expand_instruction fn.fn_code;
     Errors.OK (get_current_function ())
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 5c3ac381..25be9be3 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -63,9 +63,30 @@ let expand_scope id lbl 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 translate_annot sp preg_to_dwarf annot = 
+  let rec aux = function
+    | BA x -> Some (sp,BA (preg_to_dwarf x))
+    | BA_int _
+    | BA_long _
+    | BA_float _
+    | BA_single _
+    | BA_loadglobal _
+    | BA_addrglobal _
+    | BA_loadstack _ -> None
+    | BA_addrstack ofs -> Some (sp,BA_addrstack ofs)
+    | BA_splitlong (hi,lo) -> 
+        begin
+          match (aux hi,aux lo) with
+          | Some (_,hi) ,Some (_,lo) -> Some (sp,BA_splitlong (hi,lo))
+          | _,_ -> None
+        end in
+  (match annot with
+  | [] -> None
+  | a::_ -> aux a)
     
 
-let expand_debug id annot simple l =
+let expand_debug id sp preg simple l =
   let get_lbl = function
     | None -> 
         let lbl = new_label () in
@@ -85,7 +106,7 @@ let expand_debug id annot simple l =
               aux  lbl scopes rest
           | 3 ->
              begin 
-               match annot args with
+               match translate_annot sp preg args with
                | Some a ->
                    let lbl = get_lbl lbl in
                    Debug.start_live_range (id,txt) lbl a;
@@ -98,7 +119,7 @@ let expand_debug id annot simple l =
               aux (Some lbl) scopes rest
           | 5 ->
               begin
-                match annot args with
+                match translate_annot sp preg args with
                 | Some a->
                     Debug.stack_variable (id,txt) a;
                     aux lbl scopes rest
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index baf0523e..4f02e633 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -387,36 +387,46 @@ let expand_instruction instr =
      end
   | _ -> emit instr
        
-let expand_function fn =
-  try
-    set_current_function fn;
-    List.iter expand_instruction fn.fn_code;
-    Errors.OK (get_current_function ())
-  with Error s ->
-    Errors.Error (Errors.msg (coqstring_of_camlstring s))
+let int_reg_to_dwarf = function
+  | EAX -> 0
+  | EBX -> 3
+  | ECX -> 1
+  | EDX -> 2
+  | ESI -> 6
+  | EDI -> 7
+  | EBP -> 5
+  | ESP -> 4
 
-let expand_fundef = function
-  | Internal f ->
-      begin match expand_function f with
-      | Errors.OK tf -> Errors.OK (Internal tf)
-      | Errors.Error msg -> Errors.Error msg
-      end
-  | External ef ->
-      Errors.OK (External ef)
+let float_reg_to_dwarf = function
+  | XMM0 -> 21
+  | XMM1 -> 22
+  | XMM2 -> 23
+  | XMM3 -> 24
+  | XMM4 -> 25
+  | XMM5 -> 26
+  | XMM6 -> 27
+  | XMM7 -> 28
 
-let expand_program (p: Asm.program) : Asm.program Errors.res =
-  AST.transform_partial_program expand_fundef p
-let expand_function fn =
+let preg_to_dwarf = function
+   | IR r -> int_reg_to_dwarf r
+   | FR r -> float_reg_to_dwarf r
+   | _ -> assert false
+
+
+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 4 preg_to_dwarf 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
@@ -424,4 +434,4 @@ let expand_fundef = function
       Errors.OK (External ef)
 
 let expand_program (p: Asm.program) : Asm.program Errors.res =
-  AST.transform_partial_program expand_fundef p
+  AST.transform_partial_ident_program expand_fundef p
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 371be558..95de40ca 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -102,10 +102,10 @@ module Cygwin_System : SYSTEM =
       | Section_user(s, wr, ex) ->
           sprintf ".section	\"%s\", \"%s\"\n"
             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 *)
+      | Section_debug_info _ -> ".section	.debug_info,\"dr\""
+      | Section_debug_loc ->  ".section	.debug_loc,\"dr\""
+      | Section_debug_line _ -> ".section	.debug_line,\"dr\""
+      | Section_debug_abbrev -> ".section	.debug_abbrev,\"dr\"" (* Dummy value *)
 
     let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
 
@@ -153,10 +153,10 @@ module ELF_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 _
-      | Section_debug_loc 
-      | Section_debug_line _
-      | Section_debug_abbrev -> "" (* Dummy value *)
+      | Section_debug_info _ -> ".section	.debug_info,\"\",@progbits"
+      | Section_debug_loc -> ".section	.debug_loc,\"\",@progbits"
+      | Section_debug_line _ -> ".section	.debug_line,\"\",@progbits"
+      | Section_debug_abbrev -> ".section	.debug_abbrev,\"\",@progbits"
             
     let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
                     
@@ -207,10 +207,11 @@ module MacOS_System : SYSTEM =
           sprintf ".section	\"%s\", %s, %s"
             (if wr then "__DATA" else "__TEXT") s
             (if ex then "regular, pure_instructions" else "regular")
-      | Section_debug_info _
-      | Section_debug_loc
-      | Section_debug_line _
-      | Section_debug_abbrev -> "" (* Dummy value *)
+      | Section_debug_info _ ->	".section	__DWARF,__debug_info,regular,debug"
+      | Section_debug_loc  -> ".section	__DWARF,__debug_loc,regular,debug"
+      | Section_debug_line _ -> ".section	__DWARF,__debug_line,regular,debug"
+      | Section_debug_abbrev -> ".section	__DWARF,__debug_abbrev,regular,debug" (* Dummy value *)
+    
     
     let stack_alignment =  16 (* mandatory *)
          
@@ -748,9 +749,16 @@ module Target(System: SYSTEM):TARGET =
         
     let print_var_info = print_var_info
 
-    let print_prologue _ = 
-      need_masks := false
-    
+    let print_prologue oc = 
+      need_masks := false;
+      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 !need_masks then begin
         section oc (Section_const true);
@@ -765,7 +773,14 @@ module Target(System: SYSTEM):TARGET =
         fprintf oc "%a:	.long   0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n"
           raw_symbol "__abss_mask"
       end;
-      System.print_epilogue oc
+      System.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 comment = comment
 
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index fb569a00..00234f9b 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -660,38 +660,17 @@ let float_reg_to_dwarf = function
    | FPR24 -> 56 | FPR25 -> 57 | FPR26 -> 58 | FPR27 -> 59
    | FPR28 -> 60 | FPR29 -> 61 | FPR30 -> 62 | FPR31 -> 63
 
-let preg_to_dwarf_int = function
+let preg_to_dwarf = 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 (1,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 (1,BA_addrstack ofs)
-    | BA_splitlong (hi,lo) -> 
-        begin
-          match (aux hi,aux lo) with
-          | Some (_,hi) ,Some (_,lo) -> Some (1,BA_splitlong (hi,lo))
-          | _,_ -> None
-        end in
-  (match annot with
-  | [] -> None
-  | a::_ -> aux a)
-
 let expand_function id fn =
   try
     set_current_function fn;
     if !Clflags.option_g then
-      expand_debug id translate_annot expand_instruction fn.fn_code
+      expand_debug id 2 preg_to_dwarf expand_instruction fn.fn_code
     else
       List.iter expand_instruction fn.fn_code;
     Errors.OK (get_current_function ())