diff options
-rw-r--r-- | arm/Asmexpand.ml | 50 | ||||
-rw-r--r-- | arm/TargetPrinter.ml | 28 | ||||
-rw-r--r-- | common/Sections.ml | 1 | ||||
-rw-r--r-- | common/Sections.mli | 1 | ||||
-rw-r--r-- | debug/DwarfPrinter.ml | 2 | ||||
-rw-r--r-- | ia32/TargetPrinter.ml | 5 | ||||
-rw-r--r-- | powerpc/Asmexpand.ml | 12 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 9 |
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 |