diff options
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/Asmexpand.ml | 50 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 28 |
2 files changed, 69 insertions, 9 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 |