From 929ea48c136e4c07900e3f23995582f5f88f4f6d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 23 Dec 2020 17:52:18 +0100 Subject: AArch64: wrong function alignment The alignment was 2 bytes (like for ARM) but should be 4 bytes. It was ignored by the GNU assembler, but the LLVM assembler warns. --- aarch64/TargetPrinter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64/TargetPrinter.ml') diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 78b9eb2a..5631f47e 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -587,7 +587,7 @@ module Target : TARGET = section oc Section_text; end - let default_falignment = 2 + let default_falignment = 4 let cfi_startproc oc = () let cfi_endproc oc = () -- cgit From d851af2536a093d9ff257df55a3a67a0f381a6b6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 23 Dec 2020 18:45:51 +0100 Subject: AArch64: clarify the printing of extending-register arithmetic operations The extended register is now printed as an X register if the extension mode is UXTX, and as a W register otherwise. --- aarch64/TargetPrinter.ml | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'aarch64/TargetPrinter.ml') diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 5631f47e..a46b548c 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -217,15 +217,15 @@ module Target : TARGET = | SOasr n -> fprintf oc ", asr #%a" coqint n | SOror n -> fprintf oc ", ror #%a" coqint n -(* Print a sign- or zero-extended operand *) - let extendop oc = function - | EOsxtb n -> fprintf oc ", sxtb #%a" coqint n - | EOsxth n -> fprintf oc ", sxth #%a" coqint n - | EOsxtw n -> fprintf oc ", sxtw #%a" coqint n - | EOuxtb n -> fprintf oc ", uxtb #%a" coqint n - | EOuxth n -> fprintf oc ", uxth #%a" coqint n - | EOuxtw n -> fprintf oc ", uxtw #%a" coqint n - | EOuxtx n -> fprintf oc ", uxtx #%a" coqint n +(* Print a sign- or zero-extended register operand *) + let regextend oc = function + | (r, EOsxtb n) -> fprintf oc "%a, sxtb #%a" wreg r coqint n + | (r, EOsxth n) -> fprintf oc "%a, sxth #%a" wreg r coqint n + | (r, EOsxtw n) -> fprintf oc "%a, sxtw #%a" wreg r coqint n + | (r, EOuxtb n) -> fprintf oc "%a, uxtb #%a" wreg r coqint n + | (r, EOuxth n) -> fprintf oc "%a, uxth #%a" wreg r coqint n + | (r, EOuxtw n) -> fprintf oc "%a, uxtw #%a" wreg r coqint n + | (r, EOuxtx n) -> fprintf oc "%a, uxtx #%a" xreg r coqint n (* Printing of instructions *) let print_instruction oc = function @@ -335,13 +335,13 @@ module Target : TARGET = fprintf oc " cmn %a, %a%a\n" ireg0 (sz, r1) ireg (sz, r2) shiftop s (* Integer arithmetic, extending register *) | Paddext(rd, r1, r2, x) -> - fprintf oc " add %a, %a, %a%a\n" xregsp rd xregsp r1 wreg r2 extendop x + fprintf oc " add %a, %a, %a\n" xregsp rd xregsp r1 regextend (r2, x) | Psubext(rd, r1, r2, x) -> - fprintf oc " sub %a, %a, %a%a\n" xregsp rd xregsp r1 wreg r2 extendop x + fprintf oc " sub %a, %a, %a\n" xregsp rd xregsp r1 regextend (r2, x) | Pcmpext(r1, r2, x) -> - fprintf oc " cmp %a, %a%a\n" xreg r1 wreg r2 extendop x + fprintf oc " cmp %a, %a\n" xreg r1 regextend (r2, x) | Pcmnext(r1, r2, x) -> - fprintf oc " cmn %a, %a%a\n" xreg r1 wreg r2 extendop x + fprintf oc " cmn %a, %a\n" xreg r1 regextend (r2, x) (* Logical, shifted register *) | Pand(sz, rd, r1, r2, s) -> fprintf oc " and %a, %a, %a%a\n" ireg (sz, rd) ireg0 (sz, r1) ireg (sz, r2) shiftop s -- cgit From c50680bb86564fe61db61e6140a418ccc7d36677 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 23 Dec 2020 15:54:51 +0100 Subject: AArch64: macOS port This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors. --- aarch64/TargetPrinter.ml | 332 +++++++++++++++++++++++++++++++---------------- 1 file changed, 223 insertions(+), 109 deletions(-) (limited to 'aarch64/TargetPrinter.ml') diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index a46b548c..1c1ff018 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -36,100 +36,128 @@ let is_immediate_float32 bits = let mant = Int32.logand bits 0x7F_FFFFl in exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant -(* Module containing the printing functions *) +(* Naming and printing registers *) + +let intsz oc (sz, n) = + match sz with X -> coqint64 oc n | W -> coqint oc n + +let xreg_name = function + | X0 -> "x0" | X1 -> "x1" | X2 -> "x2" | X3 -> "x3" + | X4 -> "x4" | X5 -> "x5" | X6 -> "x6" | X7 -> "x7" + | X8 -> "x8" | X9 -> "x9" | X10 -> "x10" | X11 -> "x11" + | X12 -> "x12" | X13 -> "x13" | X14 -> "x14" | X15 -> "x15" + | X16 -> "x16" | X17 -> "x17" | X18 -> "x18" | X19 -> "x19" + | X20 -> "x20" | X21 -> "x21" | X22 -> "x22" | X23 -> "x23" + | X24 -> "x24" | X25 -> "x25" | X26 -> "x26" | X27 -> "x27" + | X28 -> "x28" | X29 -> "x29" | X30 -> "x30" + +let wreg_name = function + | X0 -> "w0" | X1 -> "w1" | X2 -> "w2" | X3 -> "w3" + | X4 -> "w4" | X5 -> "w5" | X6 -> "w6" | X7 -> "w7" + | X8 -> "w8" | X9 -> "w9" | X10 -> "w10" | X11 -> "w11" + | X12 -> "w12" | X13 -> "w13" | X14 -> "w14" | X15 -> "w15" + | X16 -> "w16" | X17 -> "w17" | X18 -> "w18" | X19 -> "w19" + | X20 -> "w20" | X21 -> "w21" | X22 -> "w22" | X23 -> "w23" + | X24 -> "w24" | X25 -> "w25" | X26 -> "w26" | X27 -> "w27" + | X28 -> "w28" | X29 -> "w29" | X30 -> "w30" + +let xreg0_name = function RR0 r -> xreg_name r | XZR -> "xzr" +let wreg0_name = function RR0 r -> wreg_name r | XZR -> "wzr" + +let xregsp_name = function RR1 r -> xreg_name r | XSP -> "sp" +let wregsp_name = function RR1 r -> wreg_name r | XSP -> "wsp" + +let dreg_name = function +| D0 -> "d0" | D1 -> "d1" | D2 -> "d2" | D3 -> "d3" +| D4 -> "d4" | D5 -> "d5" | D6 -> "d6" | D7 -> "d7" +| D8 -> "d8" | D9 -> "d9" | D10 -> "d10" | D11 -> "d11" +| D12 -> "d12" | D13 -> "d13" | D14 -> "d14" | D15 -> "d15" +| D16 -> "d16" | D17 -> "d17" | D18 -> "d18" | D19 -> "d19" +| D20 -> "d20" | D21 -> "d21" | D22 -> "d22" | D23 -> "d23" +| D24 -> "d24" | D25 -> "d25" | D26 -> "d26" | D27 -> "d27" +| D28 -> "d28" | D29 -> "d29" | D30 -> "d30" | D31 -> "d31" + +let sreg_name = function +| D0 -> "s0" | D1 -> "s1" | D2 -> "s2" | D3 -> "s3" +| D4 -> "s4" | D5 -> "s5" | D6 -> "s6" | D7 -> "s7" +| D8 -> "s8" | D9 -> "s9" | D10 -> "s10" | D11 -> "s11" +| D12 -> "s12" | D13 -> "s13" | D14 -> "s14" | D15 -> "s15" +| D16 -> "s16" | D17 -> "s17" | D18 -> "s18" | D19 -> "s19" +| D20 -> "s20" | D21 -> "s21" | D22 -> "s22" | D23 -> "s23" +| D24 -> "s24" | D25 -> "s25" | D26 -> "s26" | D27 -> "s27" +| D28 -> "s28" | D29 -> "s29" | D30 -> "s30" | D31 -> "s31" + +let xreg oc r = output_string oc (xreg_name r) +let wreg oc r = output_string oc (wreg_name r) +let ireg oc (sz, r) = + output_string oc (match sz with X -> xreg_name r | W -> wreg_name r) + +let xreg0 oc r = output_string oc (xreg0_name r) +let wreg0 oc r = output_string oc (wreg0_name r) +let ireg0 oc (sz, r) = + output_string oc (match sz with X -> xreg0_name r | W -> wreg0_name r) + +let xregsp oc r = output_string oc (xregsp_name r) +let iregsp oc (sz, r) = + output_string oc (match sz with X -> xregsp_name r | W -> wregsp_name r) + +let dreg oc r = output_string oc (dreg_name r) +let sreg oc r = output_string oc (sreg_name r) +let freg oc (sz, r) = + output_string oc (match sz with D -> dreg_name r | S -> sreg_name r) + +let preg_asm oc ty = function + | IR r -> if ty = Tint then wreg oc r else xreg oc r + | FR r -> if ty = Tsingle then sreg oc r else dreg oc r + | _ -> assert false + +let preg_annot = function + | IR r -> xreg_name r + | FR r -> dreg_name r + | _ -> assert false + +(* Base-2 log of a Caml integer *) +let rec log2 n = + assert (n > 0); + if n = 1 then 0 else 1 + log2 (n lsr 1) + +(* System dependent printer functions *) + +module type SYSTEM = + sig + val comment: string + val raw_symbol: out_channel -> string -> unit + val symbol: out_channel -> P.t -> unit + val symbol_offset_high: out_channel -> P.t * Z.t -> unit + val symbol_offset_low: out_channel -> P.t * Z.t -> unit + val label: out_channel -> int -> unit + val label_high: out_channel -> int -> unit + val label_low: out_channel -> int -> unit + val load_symbol_address: out_channel -> ireg -> P.t -> unit + val name_of_section: section_name -> string + val print_fun_info: out_channel -> P.t -> unit + val print_var_info: out_channel -> P.t -> unit + val print_comm_decl: out_channel -> P.t -> Z.t -> int -> unit + val print_lcomm_decl: out_channel -> P.t -> Z.t -> int -> unit + end -module Target : TARGET = +module ELF_System : SYSTEM = struct - -(* Basic printing functions *) - let comment = "//" + let raw_symbol = output_string + let symbol = elf_symbol + let symbol_offset_high = elf_symbol_offset + let symbol_offset_low oc id_ofs = + fprintf oc "#:lo12:%a" elf_symbol_offset id_ofs - let symbol = elf_symbol - let symbol_offset = elf_symbol_offset - let label = elf_label + let label = elf_label + let label_high = elf_label + let label_low oc lbl = + fprintf oc "#:lo12:%a" elf_label lbl - let print_label oc lbl = label oc (transl_label lbl) - - let intsz oc (sz, n) = - match sz with X -> coqint64 oc n | W -> coqint oc n - - let xreg_name = function - | X0 -> "x0" | X1 -> "x1" | X2 -> "x2" | X3 -> "x3" - | X4 -> "x4" | X5 -> "x5" | X6 -> "x6" | X7 -> "x7" - | X8 -> "x8" | X9 -> "x9" | X10 -> "x10" | X11 -> "x11" - | X12 -> "x12" | X13 -> "x13" | X14 -> "x14" | X15 -> "x15" - | X16 -> "x16" | X17 -> "x17" | X18 -> "x18" | X19 -> "x19" - | X20 -> "x20" | X21 -> "x21" | X22 -> "x22" | X23 -> "x23" - | X24 -> "x24" | X25 -> "x25" | X26 -> "x26" | X27 -> "x27" - | X28 -> "x28" | X29 -> "x29" | X30 -> "x30" - - let wreg_name = function - | X0 -> "w0" | X1 -> "w1" | X2 -> "w2" | X3 -> "w3" - | X4 -> "w4" | X5 -> "w5" | X6 -> "w6" | X7 -> "w7" - | X8 -> "w8" | X9 -> "w9" | X10 -> "w10" | X11 -> "w11" - | X12 -> "w12" | X13 -> "w13" | X14 -> "w14" | X15 -> "w15" - | X16 -> "w16" | X17 -> "w17" | X18 -> "w18" | X19 -> "w19" - | X20 -> "w20" | X21 -> "w21" | X22 -> "w22" | X23 -> "w23" - | X24 -> "w24" | X25 -> "w25" | X26 -> "w26" | X27 -> "w27" - | X28 -> "w28" | X29 -> "w29" | X30 -> "w30" - - let xreg0_name = function RR0 r -> xreg_name r | XZR -> "xzr" - let wreg0_name = function RR0 r -> wreg_name r | XZR -> "wzr" - - let xregsp_name = function RR1 r -> xreg_name r | XSP -> "sp" - let wregsp_name = function RR1 r -> wreg_name r | XSP -> "wsp" - - let dreg_name = function - | D0 -> "d0" | D1 -> "d1" | D2 -> "d2" | D3 -> "d3" - | D4 -> "d4" | D5 -> "d5" | D6 -> "d6" | D7 -> "d7" - | D8 -> "d8" | D9 -> "d9" | D10 -> "d10" | D11 -> "d11" - | D12 -> "d12" | D13 -> "d13" | D14 -> "d14" | D15 -> "d15" - | D16 -> "d16" | D17 -> "d17" | D18 -> "d18" | D19 -> "d19" - | D20 -> "d20" | D21 -> "d21" | D22 -> "d22" | D23 -> "d23" - | D24 -> "d24" | D25 -> "d25" | D26 -> "d26" | D27 -> "d27" - | D28 -> "d28" | D29 -> "d29" | D30 -> "d30" | D31 -> "d31" - - let sreg_name = function - | D0 -> "s0" | D1 -> "s1" | D2 -> "s2" | D3 -> "s3" - | D4 -> "s4" | D5 -> "s5" | D6 -> "s6" | D7 -> "s7" - | D8 -> "s8" | D9 -> "s9" | D10 -> "s10" | D11 -> "s11" - | D12 -> "s12" | D13 -> "s13" | D14 -> "s14" | D15 -> "s15" - | D16 -> "s16" | D17 -> "s17" | D18 -> "s18" | D19 -> "s19" - | D20 -> "s20" | D21 -> "s21" | D22 -> "s22" | D23 -> "s23" - | D24 -> "s24" | D25 -> "s25" | D26 -> "s26" | D27 -> "s27" - | D28 -> "s28" | D29 -> "s29" | D30 -> "s30" | D31 -> "s31" - - let xreg oc r = output_string oc (xreg_name r) - let wreg oc r = output_string oc (wreg_name r) - let ireg oc (sz, r) = - output_string oc (match sz with X -> xreg_name r | W -> wreg_name r) - - let xreg0 oc r = output_string oc (xreg0_name r) - let wreg0 oc r = output_string oc (wreg0_name r) - let ireg0 oc (sz, r) = - output_string oc (match sz with X -> xreg0_name r | W -> wreg0_name r) - - let xregsp oc r = output_string oc (xregsp_name r) - let iregsp oc (sz, r) = - output_string oc (match sz with X -> xregsp_name r | W -> wregsp_name r) - - let dreg oc r = output_string oc (dreg_name r) - let sreg oc r = output_string oc (sreg_name r) - let freg oc (sz, r) = - output_string oc (match sz with D -> dreg_name r | S -> sreg_name r) - - let preg_asm oc ty = function - | IR r -> if ty = Tint then wreg oc r else xreg oc r - | FR r -> if ty = Tsingle then sreg oc r else dreg oc r - | _ -> assert false - - let preg_annot = function - | IR r -> xreg_name r - | FR r -> dreg_name r - | _ -> assert false - -(* Names of sections *) + let load_symbol_address oc rd id = + fprintf oc " adrp %a, :got:%a\n" xreg rd symbol id; + fprintf oc " ldr %a, [%a, #:got_lo12:%a]\n" xreg rd xreg rd symbol id let name_of_section = function | Section_text -> ".text" @@ -151,6 +179,94 @@ module Target : TARGET = s (if wr then "w" else "") (if ex then "x" else "") | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",@note" + let print_fun_info = elf_print_fun_info + let print_var_info = elf_print_var_info + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al + + let print_lcomm_decl oc name sz al = + fprintf oc " .local %a\n" symbol name; + print_comm_decl oc name sz al + + end + +module MacOS_System : SYSTEM = + struct + let comment = ";" + + let raw_symbol oc s = + fprintf oc "_%s" s + + let symbol oc symb = + raw_symbol oc (extern_atom symb) + + let symbol_offset_gen kind oc (id, ofs) = + fprintf oc "%a@%s" symbol id kind; + let ofs = camlint64_of_ptrofs ofs in + if ofs <> 0L then fprintf oc " + %Ld" ofs + + let symbol_offset_high = symbol_offset_gen "PAGE" + let symbol_offset_low = symbol_offset_gen "PAGEOFF" + + let label oc lbl = + fprintf oc "L%d" lbl + + let label_high oc lbl = + fprintf oc "%a@PAGE" label lbl + let label_low oc lbl = + fprintf oc "%a@PAGEOFF" label lbl + + let load_symbol_address oc rd id = + fprintf oc " adrp %a, %a@GOTPAGE\n" xreg rd symbol id; + fprintf oc " ldr %a, [%a, %a@GOTPAGEOFF]\n" xreg rd xreg rd symbol id + + let name_of_section = function + | Section_text -> ".text" + | Section_data i | Section_small_data i -> + if i || (not !Clflags.option_fcommon) then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i || (not !Clflags.option_fcommon) then ".const" else "COMM" + | Section_string -> ".const" + | Section_literal -> ".const" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\", %s, %s" + (if wr then "__DATA" else "__TEXT") s + (if ex then "regular, pure_instructions" else "regular") + | 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_str -> ".section __DWARF,__debug_str,regular,debug" + | Section_debug_ranges -> ".section __DWARF,__debug_ranges,regular,debug" + | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" + | Section_ais_annotation -> assert false (* Not supported under MacOS *) + + let print_fun_info _ _ = () + let print_var_info _ _ = () + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" + symbol name (Z.to_string sz) (log2 al) + + let print_lcomm_decl oc name sz al = + fprintf oc " .lcomm %a, %s, %d\n" + symbol name (Z.to_string sz) (log2 al) + + end + +(* Module containing the printing functions *) + +module Target(System: SYSTEM): TARGET = + struct + include System + +(* Basic printing functions *) + + let print_label oc lbl = label oc (transl_label lbl) + +(* Names of sections *) + let section oc sec = fprintf oc " %s\n" (name_of_section sec) @@ -206,7 +322,7 @@ module Target : TARGET = | ADlsl(base, r, n) -> fprintf oc "[%a, %a, lsl #%a]" xregsp base xreg r coqint n | ADsxt(base, r, n) -> fprintf oc "[%a, %a, sxtw #%a]" xregsp base wreg r coqint n | ADuxt(base, r, n) -> fprintf oc "[%a, %a, uxtw #%a]" xregsp base wreg r coqint n - | ADadr(base, id, ofs) -> fprintf oc "[%a, #:lo12:%a]" xregsp base symbol_offset (id, ofs) + | ADadr(base, id, ofs) -> fprintf oc "[%a, %a]" xregsp base symbol_offset_low (id, ofs) | ADpostincr(base, n) -> fprintf oc "[%a], #%a" xregsp base coqint64 n (* Print a shifted operand *) @@ -312,9 +428,9 @@ module Target : TARGET = fprintf oc " movk %a, #%d, lsl #%d\n" ireg (sz, rd) (Z.to_int n) (Z.to_int pos) (* PC-relative addressing *) | Padrp(rd, id, ofs) -> - fprintf oc " adrp %a, %a\n" xreg rd symbol_offset (id, ofs) + fprintf oc " adrp %a, %a\n" xreg rd symbol_offset_high (id, ofs) | Paddadr(rd, r1, id, ofs) -> - fprintf oc " add %a, %a, #:lo12:%a\n" xreg rd xreg r1 symbol_offset (id, ofs) + fprintf oc " add %a, %a, %a\n" xreg rd xreg r1 symbol_offset_low (id, ofs) (* Bit-field operations *) | Psbfiz(sz, rd, r1, r, s) -> fprintf oc " sbfiz %a, %a, %a, %d\n" ireg (sz, rd) ireg (sz, r1) coqint r (Z.to_int s) @@ -413,8 +529,8 @@ module Target : TARGET = fprintf oc " fmov %a, #%.7f\n" dreg rd (Int64.float_of_bits d) else begin let lbl = label_literal64 d in - fprintf oc " adrp x16, %a\n" label lbl; - fprintf oc " ldr %a, [x16, #:lo12:%a] %s %.18g\n" dreg rd label lbl comment (Int64.float_of_bits d) + fprintf oc " adrp x16, %a\n" label_high lbl; + fprintf oc " ldr %a, [x16, %a] %s %.18g\n" dreg rd label_low lbl comment (Int64.float_of_bits d) end | Pfmovimms(rd, f) -> let d = camlint_of_coqint (Floats.Float32.to_bits f) in @@ -422,8 +538,8 @@ module Target : TARGET = fprintf oc " fmov %a, #%.7f\n" sreg rd (Int32.float_of_bits d) else begin let lbl = label_literal32 d in - fprintf oc " adrp x16, %a\n" label lbl; - fprintf oc " ldr %a, [x16, #:lo12:%a] %s %.18g\n" sreg rd label lbl comment (Int32.float_of_bits d) + fprintf oc " adrp x16, %a\n" label_high lbl; + fprintf oc " ldr %a, [x16, %a] %s %.18g\n" sreg rd label_low lbl comment (Int32.float_of_bits d) end | Pfmovi(D, rd, r1) -> fprintf oc " fmov %a, %a\n" dreg rd xreg0 r1 @@ -490,8 +606,7 @@ module Target : TARGET = | Plabel lbl -> fprintf oc "%a:\n" print_label lbl | Ploadsymbol(rd, id) -> - fprintf oc " adrp %a, :got:%a\n" xreg rd symbol id; - fprintf oc " ldr %a, [%a, #:got_lo12:%a]\n" xreg rd xreg rd symbol id + load_symbol_address oc rd id | Pcvtsw2x(rd, r1) -> fprintf oc " sxtw %a, %a\n" xreg rd wreg r1 | Pcvtuw2x(rd, r1) -> @@ -554,19 +669,12 @@ module Target : TARGET = jumptables := [] end - let print_fun_info = elf_print_fun_info - let print_optional_fun_info _ = () - let print_var_info = elf_print_var_info - let print_comm_symb oc sz name align = - if C2C.atom_is_static name then - fprintf oc " .local %a\n" symbol name; - fprintf oc " .comm %a, %s, %d\n" - symbol name - (Z.to_string sz) - align + if C2C.atom_is_static name + then print_lcomm_decl oc name sz align + else print_comm_decl oc name sz align let print_instructions oc fn = current_function_sig := fn.fn_sig; @@ -595,4 +703,10 @@ module Target : TARGET = end let sel_target () = - (module Target:TARGET) + let module S = + (val (match Configuration.system with + | "linux" -> (module ELF_System : SYSTEM) + | "macosx" -> (module MacOS_System : SYSTEM) + | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")) + : SYSTEM) in + (module Target(S) : TARGET) -- cgit From 4925303d4f8c011fbb40157cbf44e51a68f7aa2d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 26 Dec 2020 18:54:14 +0100 Subject: AArch64 / macOS: use __DATA,__CONST section instead of .const (temporary fix) The .const section cannot contain absolute references to symbols, as these may need relocation and therefore must be writable. This should be fixed more generally by distinguishing between initialization data that contains absolute references to symbols and initialization data that does not. --- aarch64/TargetPrinter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64/TargetPrinter.ml') diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 1c1ff018..6e7b3fba 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -226,7 +226,7 @@ module MacOS_System : SYSTEM = | Section_data i | Section_small_data i -> if i || (not !Clflags.option_fcommon) then ".data" else "COMM" | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".const" else "COMM" + if i || (not !Clflags.option_fcommon) then ".section __DATA,__CONST" else "COMM" | Section_string -> ".const" | Section_literal -> ".const" | Section_jumptable -> ".text" -- cgit From ab62e1bed37d2efe4d2a9e0139839bae21b1cdd9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 18 Jan 2021 19:56:44 +0100 Subject: "macosx" is now called "macos" The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos". --- aarch64/TargetPrinter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64/TargetPrinter.ml') diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 6e7b3fba..800348a7 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -706,7 +706,7 @@ let sel_target () = let module S = (val (match Configuration.system with | "linux" -> (module ELF_System : SYSTEM) - | "macosx" -> (module MacOS_System : SYSTEM) + | "macos" -> (module MacOS_System : SYSTEM) | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")) : SYSTEM) in (module Target(S) : TARGET) -- cgit From 30feb31c6d6e9235acad42ec5d09d14f3919cc36 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 30 Dec 2020 11:41:10 +0100 Subject: Introduce and use PrintAsmaux.variable_section This is a generalization of the previous PrintAsmaux.common_section function that - handles initialized variables in addition to uninitialized variables; - can be used for Section_const, not just for Section_data. --- aarch64/TargetPrinter.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'aarch64/TargetPrinter.ml') diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 800348a7..e31abf71 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -162,9 +162,9 @@ module ELF_System : SYSTEM = let name_of_section = function | Section_text -> ".text" | Section_data i | Section_small_data i -> - if i then ".data" else common_section () + variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" + variable_section ~sec:".section .rodata" i | Section_string -> ".section .rodata" | Section_literal -> ".section .rodata" | Section_jumptable -> ".section .rodata" @@ -224,9 +224,9 @@ module MacOS_System : SYSTEM = let name_of_section = function | Section_text -> ".text" | Section_data i | Section_small_data i -> - if i || (not !Clflags.option_fcommon) then ".data" else "COMM" + variable_section ~sec:".data" i | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section __DATA,__CONST" else "COMM" + variable_section ~sec:".section __DATA,__CONST" i | Section_string -> ".const" | Section_literal -> ".const" | Section_jumptable -> ".text" -- cgit From ed89275cb820bb7ab283c51e461d852d1c8bec63 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 30 Dec 2020 11:00:22 +0100 Subject: Section handling: finer control of variable initialization Distinguish between: - uninitialized variables, which can go in COMM if supported - variables initialized with fixed, numeric quantities, which can go in a readonly section if "const" - variables initialized with symbol addresses which may need relocation, which cannot go in a readonly section even if "const", but can go in a special "const_data" section. Also: on macOS, use ".const" instead of ".literal8" for literals, as not all literals have size 8. --- aarch64/TargetPrinter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64/TargetPrinter.ml') diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index e31abf71..a9d47bdd 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -226,7 +226,7 @@ module MacOS_System : SYSTEM = | Section_data i | Section_small_data i -> variable_section ~sec:".data" i | Section_const i | Section_small_const i -> - variable_section ~sec:".section __DATA,__CONST" i + variable_section ~sec:".const" ~reloc:".const_data" i | Section_string -> ".const" | Section_literal -> ".const" | Section_jumptable -> ".text" -- cgit