aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/Asmexpand.ml50
-rw-r--r--arm/TargetPrinter.ml28
-rw-r--r--common/Sections.ml1
-rw-r--r--common/Sections.mli1
-rw-r--r--debug/DwarfPrinter.ml2
-rw-r--r--ia32/TargetPrinter.ml5
-rw-r--r--powerpc/Asmexpand.ml12
-rw-r--r--powerpc/TargetPrinter.ml9
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
generated by cgit (git 2.34.1) at 2024-06-26 18:23:02 +0000