From 0ffd562ae1941e37471ac0c2b8f93bed1de26441 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 9 Oct 2015 11:06:24 +0200 Subject: Filled in the rest of the funciton needed for thte debug info under arm. The name_of_section function no returns the correct name for the debug sections, the prologue and epilogue directives are added and the labels for the live ranges are introduced in the Asmexpand pass. --- arm/TargetPrinter.ml | 28 +++++++++++++++++++++++----- 1 file changed, 23 insertions(+), 5 deletions(-) (limited to 'arm/TargetPrinter.ml') 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 -- cgit From 7a6bb90048db7a254e959b1e3c308bac5fe6c418 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 11 Oct 2015 17:43:59 +0200 Subject: Use Coq strings instead of idents to name external and builtin functions. The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables. --- arm/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 2e676090..04226900 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -777,7 +777,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = begin match ef with | EF_annot(txt, targs) -> fprintf oc "%s annotation: " comment; - print_annot_text preg "sp" oc (extern_atom txt) args; + print_annot_text preg "sp" oc (camlstring_of_coqstring txt) args; 0 | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg "sp" oc @@ -785,7 +785,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = 0 | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - print_inline_asm preg oc (extern_atom txt) sg args res; + print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment; 5 (* hoping this is an upper bound... *) | _ -> -- cgit From 16315711d815580afa77f93424cc49c7362ab5b8 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 13 Oct 2015 14:57:31 +0200 Subject: Implement the usage of the debug_str section for the gcc backend. GCC prints all string larger than 3 characters in the debug_str section which reduces the size of the debug information since entries containing the same string now map to the same string in the debug_str sections. Bug 17392. --- arm/TargetPrinter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 2e676090..b988f10f 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -157,7 +157,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Section_debug_loc -> ".section .debug_loc,\"\",%progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",%progbits" | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" - + | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" let section oc sec = fprintf oc " %s\n" (name_of_section sec) -- cgit From 60ab550a952c3d9719b2a91ec90c9b58769f6717 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:07:48 +0200 Subject: bug 17392: remove trailing whitespace in source files --- arm/TargetPrinter.ml | 94 ++++++++++++++++++++++++++-------------------------- 1 file changed, 47 insertions(+), 47 deletions(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index b988f10f..4961f897 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -40,13 +40,13 @@ module type PRINTER_OPTIONS = module Target (Opt: PRINTER_OPTIONS) : TARGET = struct (* Code generation options. *) - + let literals_in_code = ref true (* to be turned into a proper option *) - + (* Basic printing functions *) - + let print_label oc lbl = elf_label oc (transl_label lbl) - + let comment = "@" let symbol = elf_symbol @@ -61,34 +61,34 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | IR4 -> "r4" | IR5 -> "r5" | IR6 -> "r6" | IR7 -> "r7" | IR8 -> "r8" | IR9 -> "r9" | IR10 -> "r10" | IR11 -> "r11" | IR12 -> "r12" | IR13 -> "sp" | IR14 -> "lr" - + let float_reg_name = function | FR0 -> "d0" | FR1 -> "d1" | FR2 -> "d2" | FR3 -> "d3" | FR4 -> "d4" | FR5 -> "d5" | FR6 -> "d6" | FR7 -> "d7" | FR8 -> "d8" | FR9 -> "d9" | FR10 -> "d10" | FR11 -> "d11" | FR12 -> "d12" | FR13 -> "d13" | FR14 -> "d14" | FR15 -> "d15" - + let single_float_reg_index = function | FR0 -> 0 | FR1 -> 2 | FR2 -> 4 | FR3 -> 6 | FR4 -> 8 | FR5 -> 10 | FR6 -> 12 | FR7 -> 14 | FR8 -> 16 | FR9 -> 18 | FR10 -> 20 | FR11 -> 22 | FR12 -> 24 | FR13 -> 26 | FR14 -> 28 | FR15 -> 30 - + let single_float_reg_name = function | FR0 -> "s0" | FR1 -> "s2" | FR2 -> "s4" | FR3 -> "s6" | FR4 -> "s8" | FR5 -> "s10" | FR6 -> "s12" | FR7 -> "s14" | FR8 -> "s16" | FR9 -> "s18" | FR10 -> "s20" | FR11 -> "s22" | FR12 -> "s24" | FR13 -> "s26" | FR14 -> "s28" | FR15 -> "s30" - + let ireg oc r = output_string oc (int_reg_name r) let freg oc r = output_string oc (float_reg_name r) let freg_single oc r = output_string oc (single_float_reg_name r) - + let preg oc = function | IR r -> ireg oc r | FR r -> freg oc r | _ -> assert false - + let condition_name = function | TCeq -> "eq" | TCne -> "ne" @@ -102,7 +102,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | TClt -> "lt" | TCgt -> "gt" | TCle -> "le" - + let neg_condition_name = function | TCeq -> "ne" | TCne -> "eq" @@ -116,7 +116,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | TClt -> "ge" | TCgt -> "le" | TCle -> "gt" - + (* In Thumb2 mode, some arithmetic instructions have shorter encodings if they carry the "S" flag (update condition flags): add (but not sp + imm) @@ -158,27 +158,27 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Section_debug_abbrev -> ".section .debug_abbrev,\"\",%progbits" | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" - + let section oc sec = fprintf oc " %s\n" (name_of_section sec) - + (* Record current code position and latest position at which to emit float and symbol constants. *) - + let currpos = ref 0 let size_constants = ref 0 let max_pos_constants = ref max_int - + let distance_to_emit_constants () = if !literals_in_code then !max_pos_constants - (!currpos + !size_constants) else max_int - + (* Associate labels to floating-point constants and to symbols *) - + let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t) let float32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t) - + let label_float bf = try Hashtbl.find float_labels bf @@ -188,7 +188,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = size_constants := !size_constants + 8; max_pos_constants := min !max_pos_constants (!currpos + 1024); lbl' - + let label_float32 bf = try Hashtbl.find float32_labels bf @@ -198,10 +198,10 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = size_constants := !size_constants + 4; max_pos_constants := min !max_pos_constants (!currpos + 1024); lbl' - + let symbol_labels = (Hashtbl.create 39 : (ident * Integers.Int.int, int) Hashtbl.t) - + let label_symbol id ofs = try Hashtbl.find symbol_labels (id, ofs) @@ -211,14 +211,14 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = size_constants := !size_constants + 4; max_pos_constants := min !max_pos_constants (!currpos + 4096); lbl' - + let reset_constants () = Hashtbl.clear float_labels; Hashtbl.clear float32_labels; Hashtbl.clear symbol_labels; size_constants := 0; max_pos_constants := max_int - + let emit_constants oc = fprintf oc " .balign 4\n"; Hashtbl.iter @@ -238,9 +238,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = lbl symbol_offset (id, ofs)) symbol_labels; reset_constants () - + (* Generate code to load the address of id + ofs in register r *) - + let loadsymbol oc r id ofs = if !Clflags.option_mthumb then begin fprintf oc " movw %a, #:lower16:%a\n" @@ -249,13 +249,13 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = ireg r symbol_offset (id, ofs); 2 end else begin let lbl = label_symbol id ofs in - fprintf oc " ldr %a, .L%d @ %a\n" + fprintf oc " ldr %a, .L%d @ %a\n" ireg r lbl symbol_offset (id, ofs); 1 end - + (* Emit instruction sequences that set or offset a register by a constant. *) (* No S suffix because they are applied to SP most of the time. *) - + let movimm oc dst n = match Asmgen.decompose_int n with | [] -> assert false @@ -265,7 +265,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (fun n -> fprintf oc " orr %s, %s, #%a\n" dst dst coqint n) tl; List.length l - + let addimm oc dst src n = match Asmgen.decompose_int n with | [] -> assert false @@ -275,7 +275,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (fun n -> fprintf oc " add %s, %s, #%a\n" dst dst coqint n) tl; List.length l - + let subimm oc dst src n = match Asmgen.decompose_int n with | [] -> assert false @@ -285,27 +285,27 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (fun n -> fprintf oc " sub %s, %s, #%a\n" dst dst coqint n) tl; List.length l - + (* Recognition of float constants appropriate for VMOV. a normalized binary floating point encoding with 1 sign bit, 4 bits of fraction and a 3-bit exponent *) - + let is_immediate_float64 bits = let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant - + let is_immediate_float32 bits = let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in let mant = Int32.logand bits 0x7F_FFFFl in exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant - + (* Emit .file / .loc debugging directives *) - + let print_file_line oc file line = print_file_line oc comment file line - + let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) @@ -456,7 +456,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = match Opt.float_abi with | Soft -> (FixupEABI.fixup_arguments, FixupEABI.fixup_result) | Hard -> (FixupHF.fixup_arguments, FixupHF.fixup_result) - + (* Printing of instructions *) let shift_op oc = function @@ -494,7 +494,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " b %a\n" symbol id; n + 1 | Pbreg(r, sg) -> - let n = + let n = if r = IR14 then fixup_result oc Outgoing sg else fixup_arguments oc Outgoing sg in @@ -886,7 +886,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " .space %s\n" (Z.to_string n) | Init_addrof(symb, ofs) -> fprintf oc " .word %a\n" symbol_offset (symb, ofs) - + let print_prologue oc = fprintf oc " .syntax unified\n"; fprintf oc " .arch %s\n" @@ -908,7 +908,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = end - let print_epilogue oc = + let print_epilogue oc = if !Clflags.option_g then begin let high_pc = new_label () in Debug.add_compilation_section_end ".text" high_pc; @@ -919,22 +919,22 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let default_falignment = 4 - + let label = elf_label - + let new_label = new_label end -let sel_target () = +let sel_target () = let module S : PRINTER_OPTIONS = struct - + let vfpv3 = Configuration.model >= "armv7" - + let float_abi = match Configuration.abi with | "eabi" -> Soft | "hardfloat" -> Hard | _ -> assert false - + let hardware_idiv = match Configuration.model with | "armv7r" | "armv7m" -> !Clflags.option_mthumb -- cgit From 44845982f412810b0c18067987f2780ef6245fbb Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 15 Oct 2015 09:10:22 +0200 Subject: Use section type also for other targets. Bug 17392. --- arm/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 4961f897..3bffe59b 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -902,7 +902,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = if !Clflags.option_g then begin section oc Section_text; let low_pc = new_label () in - Debug.add_compilation_section_start ".text" low_pc; + Debug.add_compilation_section_start Section_text low_pc; fprintf oc "%a:\n" elf_label low_pc; fprintf oc " .cfi_sections .debug_frame\n" end @@ -911,7 +911,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = 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.add_compilation_section_end Section_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 -- cgit From 1e52bb2001964d87086cea00d0cb779e270b99ce Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 15 Oct 2015 13:15:28 +0200 Subject: First step to implemente address ranges for the gnu backend. In contrast to the dcc, the gcc uses address ranges to express non-contiguous range of addresses. As a first step we set the start and end addresses for the different address ranges for the compilation unit by using the start and end addresses of functions. Bug 17392. --- arm/TargetPrinter.ml | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 3bffe59b..151326bb 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -901,21 +901,15 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = 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 Section_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 Section_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 + end let default_falignment = 4 -- cgit From 24b4159b6a29328c529e0e59405e03ea192aa99e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Oct 2015 13:06:09 +0200 Subject: Implemented the usage of DW_AT_ranges for non-contiguous address ranges. The gcc produces DW_AT_ranges for non-contiguous address ranges, like compilation units containing functions which are placed in different ELF-sections or lexical scopes that are split up. With this commit CompCert also uses this DWARF v3 feature for gnu backend based targets. In order to ensure backward compability a flag is added which avoids this and produces debug info in DWARF v2 format. Bug 17392. --- arm/TargetPrinter.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 151326bb..9f435cee 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -157,6 +157,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Section_debug_loc -> ".section .debug_loc,\"\",%progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",%progbits" | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" + | Section_debug_line -> ".section .debug_ranges,\"\",%progbits" | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" let section oc sec = -- cgit From 32ab0017ba80baafd03230960beaf3e256637369 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Oct 2015 13:14:15 +0200 Subject: Fixed typos in the arm and ia32 section printing. Bug 17392 --- arm/TargetPrinter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 9f435cee..3b920ce0 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -157,7 +157,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Section_debug_loc -> ".section .debug_loc,\"\",%progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",%progbits" | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" - | Section_debug_line -> ".section .debug_ranges,\"\",%progbits" + | Section_debug_ranges -> ".section .debug_ranges,\"\",%progbits" | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" let section oc sec = -- cgit From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- arm/TargetPrinter.ml | 94 ++++++++++++++++++++++++++-------------------------- 1 file changed, 47 insertions(+), 47 deletions(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 04226900..a938725a 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -40,13 +40,13 @@ module type PRINTER_OPTIONS = module Target (Opt: PRINTER_OPTIONS) : TARGET = struct (* Code generation options. *) - + let literals_in_code = ref true (* to be turned into a proper option *) - + (* Basic printing functions *) - + let print_label oc lbl = elf_label oc (transl_label lbl) - + let comment = "@" let symbol = elf_symbol @@ -61,34 +61,34 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | IR4 -> "r4" | IR5 -> "r5" | IR6 -> "r6" | IR7 -> "r7" | IR8 -> "r8" | IR9 -> "r9" | IR10 -> "r10" | IR11 -> "r11" | IR12 -> "r12" | IR13 -> "sp" | IR14 -> "lr" - + let float_reg_name = function | FR0 -> "d0" | FR1 -> "d1" | FR2 -> "d2" | FR3 -> "d3" | FR4 -> "d4" | FR5 -> "d5" | FR6 -> "d6" | FR7 -> "d7" | FR8 -> "d8" | FR9 -> "d9" | FR10 -> "d10" | FR11 -> "d11" | FR12 -> "d12" | FR13 -> "d13" | FR14 -> "d14" | FR15 -> "d15" - + let single_float_reg_index = function | FR0 -> 0 | FR1 -> 2 | FR2 -> 4 | FR3 -> 6 | FR4 -> 8 | FR5 -> 10 | FR6 -> 12 | FR7 -> 14 | FR8 -> 16 | FR9 -> 18 | FR10 -> 20 | FR11 -> 22 | FR12 -> 24 | FR13 -> 26 | FR14 -> 28 | FR15 -> 30 - + let single_float_reg_name = function | FR0 -> "s0" | FR1 -> "s2" | FR2 -> "s4" | FR3 -> "s6" | FR4 -> "s8" | FR5 -> "s10" | FR6 -> "s12" | FR7 -> "s14" | FR8 -> "s16" | FR9 -> "s18" | FR10 -> "s20" | FR11 -> "s22" | FR12 -> "s24" | FR13 -> "s26" | FR14 -> "s28" | FR15 -> "s30" - + let ireg oc r = output_string oc (int_reg_name r) let freg oc r = output_string oc (float_reg_name r) let freg_single oc r = output_string oc (single_float_reg_name r) - + let preg oc = function | IR r -> ireg oc r | FR r -> freg oc r | _ -> assert false - + let condition_name = function | TCeq -> "eq" | TCne -> "ne" @@ -102,7 +102,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | TClt -> "lt" | TCgt -> "gt" | TCle -> "le" - + let neg_condition_name = function | TCeq -> "ne" | TCne -> "eq" @@ -116,7 +116,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | TClt -> "ge" | TCgt -> "le" | TCle -> "gt" - + (* In Thumb2 mode, some arithmetic instructions have shorter encodings if they carry the "S" flag (update condition flags): add (but not sp + imm) @@ -158,27 +158,27 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | 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) - + (* Record current code position and latest position at which to emit float and symbol constants. *) - + let currpos = ref 0 let size_constants = ref 0 let max_pos_constants = ref max_int - + let distance_to_emit_constants () = if !literals_in_code then !max_pos_constants - (!currpos + !size_constants) else max_int - + (* Associate labels to floating-point constants and to symbols *) - + let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t) let float32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t) - + let label_float bf = try Hashtbl.find float_labels bf @@ -188,7 +188,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = size_constants := !size_constants + 8; max_pos_constants := min !max_pos_constants (!currpos + 1024); lbl' - + let label_float32 bf = try Hashtbl.find float32_labels bf @@ -198,10 +198,10 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = size_constants := !size_constants + 4; max_pos_constants := min !max_pos_constants (!currpos + 1024); lbl' - + let symbol_labels = (Hashtbl.create 39 : (ident * Integers.Int.int, int) Hashtbl.t) - + let label_symbol id ofs = try Hashtbl.find symbol_labels (id, ofs) @@ -211,14 +211,14 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = size_constants := !size_constants + 4; max_pos_constants := min !max_pos_constants (!currpos + 4096); lbl' - + let reset_constants () = Hashtbl.clear float_labels; Hashtbl.clear float32_labels; Hashtbl.clear symbol_labels; size_constants := 0; max_pos_constants := max_int - + let emit_constants oc = fprintf oc " .balign 4\n"; Hashtbl.iter @@ -238,9 +238,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = lbl symbol_offset (id, ofs)) symbol_labels; reset_constants () - + (* Generate code to load the address of id + ofs in register r *) - + let loadsymbol oc r id ofs = if !Clflags.option_mthumb then begin fprintf oc " movw %a, #:lower16:%a\n" @@ -249,13 +249,13 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = ireg r symbol_offset (id, ofs); 2 end else begin let lbl = label_symbol id ofs in - fprintf oc " ldr %a, .L%d @ %a\n" + fprintf oc " ldr %a, .L%d @ %a\n" ireg r lbl symbol_offset (id, ofs); 1 end - + (* Emit instruction sequences that set or offset a register by a constant. *) (* No S suffix because they are applied to SP most of the time. *) - + let movimm oc dst n = match Asmgen.decompose_int n with | [] -> assert false @@ -265,7 +265,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (fun n -> fprintf oc " orr %s, %s, #%a\n" dst dst coqint n) tl; List.length l - + let addimm oc dst src n = match Asmgen.decompose_int n with | [] -> assert false @@ -275,7 +275,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (fun n -> fprintf oc " add %s, %s, #%a\n" dst dst coqint n) tl; List.length l - + let subimm oc dst src n = match Asmgen.decompose_int n with | [] -> assert false @@ -285,27 +285,27 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (fun n -> fprintf oc " sub %s, %s, #%a\n" dst dst coqint n) tl; List.length l - + (* Recognition of float constants appropriate for VMOV. a normalized binary floating point encoding with 1 sign bit, 4 bits of fraction and a 3-bit exponent *) - + let is_immediate_float64 bits = let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant - + let is_immediate_float32 bits = let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in let mant = Int32.logand bits 0x7F_FFFFl in exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant - + (* Emit .file / .loc debugging directives *) - + let print_file_line oc file line = print_file_line oc comment file line - + let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) @@ -456,7 +456,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = match Opt.float_abi with | Soft -> (FixupEABI.fixup_arguments, FixupEABI.fixup_result) | Hard -> (FixupHF.fixup_arguments, FixupHF.fixup_result) - + (* Printing of instructions *) let shift_op oc = function @@ -494,7 +494,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " b %a\n" symbol id; n + 1 | Pbreg(r, sg) -> - let n = + let n = if r = IR14 then fixup_result oc Outgoing sg else fixup_arguments oc Outgoing sg in @@ -886,7 +886,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " .space %s\n" (Z.to_string n) | Init_addrof(symb, ofs) -> fprintf oc " .word %a\n" symbol_offset (symb, ofs) - + let print_prologue oc = fprintf oc " .syntax unified\n"; fprintf oc " .arch %s\n" @@ -908,7 +908,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = end - let print_epilogue oc = + let print_epilogue oc = if !Clflags.option_g then begin let high_pc = new_label () in Debug.add_compilation_section_end ".text" high_pc; @@ -919,22 +919,22 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let default_falignment = 4 - + let label = elf_label - + let new_label = new_label end -let sel_target () = +let sel_target () = let module S : PRINTER_OPTIONS = struct - + let vfpv3 = Configuration.model >= "armv7" - + let float_abi = match Configuration.abi with | "eabi" -> Soft | "hardfloat" -> Hard | _ -> assert false - + let hardware_idiv = match Configuration.model with | "armv7r" | "armv7m" -> !Clflags.option_mthumb -- cgit