aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--arm/Asmexpand.ml25
-rw-r--r--backend/Asmexpandaux.ml27
-rw-r--r--ia32/Asmexpand.ml54
-rw-r--r--ia32/TargetPrinter.ml47
-rw-r--r--powerpc/Asmexpand.ml25
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 ())