diff options
| -rw-r--r-- | arm/PrintAsm.ml | 1236 | ||||
| -rw-r--r-- | arm/PrintAsm.mli | 13 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 1143 | ||||
| -rw-r--r-- | backend/PrintAsm.ml | 101 | ||||
| -rw-r--r-- | backend/PrintAsm.mli (renamed from powerpc/PrintAsm.mli) | 3 | ||||
| -rw-r--r-- | backend/PrintAsmaux.ml | 134 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 4 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 1067 | ||||
| -rw-r--r-- | ia32/PrintAsm.mli | 13 | ||||
| -rw-r--r-- | ia32/TargetPrinter.ml | 993 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 849 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 753 |
12 files changed, 3130 insertions, 3179 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml deleted file mode 100644 index 7f511912..00000000 --- a/arm/PrintAsm.ml +++ /dev/null @@ -1,1236 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Printing ARM assembly code in asm syntax *) - -open Printf -open Datatypes -open Camlcoq -open Sections -open AST -open Memdata -open Asm - -(* Type for the ABI versions *) -type float_abi_type = - | Hard - | Soft - -(* Module type for the options *) -module type PRINTER_OPTIONS = - sig - val float_abi: float_abi_type - val vfpv3: bool - val hardware_idiv: bool - val cfi_startproc: out_channel -> unit - val cfi_endproc: out_channel -> unit - val cfi_adjust: out_channel -> int32 -> unit - val cfi_rel_offset: out_channel -> string -> int32 -> unit - end - -(* Module containing the printing functions *) - -module AsmPrinter (Opt: PRINTER_OPTIONS) = - (struct -(* Code generation options. *) - -let literals_in_code = ref true (* to be turned into a proper option *) - -(* On-the-fly label renaming *) - -let next_label = ref 100 - -let new_label() = - let lbl = !next_label in incr next_label; lbl - -let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t) - -let label_for_label lbl = - try - Hashtbl.find current_function_labels lbl - with Not_found -> - let lbl' = new_label() in - Hashtbl.add current_function_labels lbl lbl'; - lbl' - -(* Basic printing functions *) - -let print_symb oc symb = - fprintf oc "%s" (extern_atom symb) - -let print_label oc lbl = - fprintf oc ".L%d" (label_for_label lbl) - -let coqint oc n = - fprintf oc "%ld" (camlint_of_coqint n) - -let comment = "@" - -let print_symb_ofs oc (symb, ofs) = - print_symb oc symb; - let ofs = camlint_of_coqint ofs in - if ofs <> 0l then fprintf oc " + %ld" ofs - -let int_reg_name = function - | IR0 -> "r0" | IR1 -> "r1" | IR2 -> "r2" | IR3 -> "r3" - | 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" - | TChs -> "hs" - | TClo -> "lo" - | TCmi -> "mi" - | TCpl -> "pl" - | TChi -> "hi" - | TCls -> "ls" - | TCge -> "ge" - | TClt -> "lt" - | TCgt -> "gt" - | TCle -> "le" - -let neg_condition_name = function - | TCeq -> "ne" - | TCne -> "eq" - | TChs -> "lo" - | TClo -> "hs" - | TCmi -> "pl" - | TCpl -> "mi" - | TChi -> "ls" - | TCls -> "hi" - | TCge -> "lt" - | 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) - and - asr - bic - eor - lsl - lsr - mov - mvn - orr - rsb - sub (but not sp - imm) - The proof of Asmgen shows that CompCert-generated code behaves the - same whether flags are updated or not by those instructions. The - following printing function adds a "S" suffix if we are in Thumb2 - mode. *) - -let thumbS oc = - if !Clflags.option_mthumb then output_char oc 's' - -(* Names of sections *) - -let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else "COMM" - | Section_const i | Section_small_const i -> - if i then ".section .rodata" else "COMM" - | Section_string -> ".section .rodata" - | Section_literal -> ".text" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\",\"a%s%s\",%%progbits" - s (if wr then "w" else "") (if ex then "x" else "") - -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 - with Not_found -> - let lbl' = new_label() in - Hashtbl.add float_labels bf lbl'; - 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 - with Not_found -> - let lbl' = new_label() in - Hashtbl.add float32_labels bf lbl'; - 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) - with Not_found -> - let lbl' = new_label() in - Hashtbl.add symbol_labels (id, ofs) lbl'; - 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 - (fun bf lbl -> - (* Little-endian floats *) - let bfhi = Int64.shift_right_logical bf 32 - and bflo = Int64.logand bf 0xFFFF_FFFFL in - fprintf oc ".L%d: .word 0x%Lx, 0x%Lx\n" lbl bflo bfhi) - float_labels; - Hashtbl.iter - (fun bf lbl -> - fprintf oc ".L%d: .word 0x%lx\n" lbl bf) - float32_labels; - Hashtbl.iter - (fun (id, ofs) lbl -> - fprintf oc ".L%d: .word %a\n" - lbl print_symb_ofs (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" - ireg r print_symb_ofs (id, ofs); - fprintf oc " movt %a, #:upper16:%a\n" - ireg r print_symb_ofs (id, ofs); 2 - end else begin - let lbl = label_symbol id ofs in - fprintf oc " ldr %a, .L%d @ %a\n" - ireg r lbl print_symb_ofs (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 - | hd::tl as l -> - fprintf oc " mov %s, #%a\n" dst coqint hd; - List.iter - (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 - | hd::tl as l -> - fprintf oc " add %s, %s, #%a\n" dst src coqint hd; - List.iter - (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 - | hd::tl as l -> - fprintf oc " sub %s, %s, #%a\n" dst src coqint hd; - List.iter - (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 = - PrintAnnot.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) - -(* Built-ins. They come in two flavors: - - annotation statements: take their arguments in registers or stack - locations; generate no code; - - inlined by the compiler: take their arguments in arbitrary - registers. -*) - -(* Handling of annotations *) - -let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" - -let print_annot_stmt oc txt targs args = - if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) - (int_of_string (Str.matched_group 2 txt)) - end else begin - fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "sp" oc txt targs args - end - -let print_annot_val oc txt args res = - fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_val preg oc txt args; - match args, res with - | [IR src], [IR dst] -> - if dst = src then 0 else (fprintf oc " mov %a, %a\n" ireg dst ireg src; 1) - | [FR src], [FR dst] -> - if dst = src then 0 else (fprintf oc " vmov.f64 %a, %a\n" freg dst freg src; 1) - | _, _ -> assert false - -(* Handling of memcpy *) - -(* The ARM has strict alignment constraints for 2 and 4 byte accesses. - 8-byte accesses must be 4-aligned. *) - -let print_builtin_memcpy_small oc sz al src dst = - let rec copy ofs sz ninstr = - if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin - fprintf oc " vldr %a, [%a, #%d]\n" freg FR7 ireg src ofs; - fprintf oc " vstr %a, [%a, #%d]\n" freg FR7 ireg dst ofs; - copy (ofs + 8) (sz - 8) (ninstr + 2) - end else if sz >= 4 && al >= 4 then begin - fprintf oc " ldr %a, [%a, #%d]\n" ireg IR14 ireg src ofs; - fprintf oc " str %a, [%a, #%d]\n" ireg IR14 ireg dst ofs; - copy (ofs + 4) (sz - 4) (ninstr + 2) - end else if sz >= 2 && al >= 2 then begin - fprintf oc " ldrh %a, [%a, #%d]\n" ireg IR14 ireg src ofs; - fprintf oc " strh %a, [%a, #%d]\n" ireg IR14 ireg dst ofs; - copy (ofs + 2) (sz - 2) (ninstr + 2) - end else if sz >= 1 then begin - fprintf oc " ldrb %a, [%a, #%d]\n" ireg IR14 ireg src ofs; - fprintf oc " strb %a, [%a, #%d]\n" ireg IR14 ireg dst ofs; - copy (ofs + 1) (sz - 1) (ninstr + 2) - end else - ninstr in - copy 0 sz 0 - -let print_builtin_memcpy_big oc sz al src dst = - assert (sz >= al); - assert (sz mod al = 0); - assert (src = IR2); - assert (dst = IR3); - let (load, store, chunksize) = - if al >= 4 then ("ldr", "str", 4) - else if al = 2 then ("ldrh", "strh", 2) - else ("ldrb", "strb", 1) in - let n = movimm oc "r14" (coqint_of_camlint (Int32.of_int (sz / chunksize))) in - let lbl = new_label() in - fprintf oc ".L%d: %s %a, [%a], #%d\n" lbl load ireg IR12 ireg src chunksize; - fprintf oc " subs %a, %a, #1\n" ireg IR14 ireg IR14; - fprintf oc " %s %a, [%a], #%d\n" store ireg IR12 ireg dst chunksize; - fprintf oc " bne .L%d\n" lbl; - n + 4 - -let print_builtin_memcpy oc sz al args = - let (dst, src) = - match args with [IR d; IR s] -> (d, s) | _ -> assert false in - fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n" - comment sz al; - let n = - if sz <= 32 - then print_builtin_memcpy_small oc sz al src dst - else print_builtin_memcpy_big oc sz al src dst in - fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment; n - -(* Handling of volatile reads and writes *) - -let print_builtin_vload_common oc chunk args res = - match chunk, args, res with - | Mint8unsigned, [IR addr], [IR res] -> - fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint8signed, [IR addr], [IR res] -> - fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint16unsigned, [IR addr], [IR res] -> - fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint16signed, [IR addr], [IR res] -> - fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint32, [IR addr], [IR res] -> - fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint64, [IR addr], [IR res1; IR res2] -> - if addr <> res2 then begin - fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr; - fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr - end else begin - fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr; - fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr - end; 2 - | Mfloat32, [IR addr], [FR res] -> - fprintf oc " vldr %a, [%a, #0]\n" freg_single res ireg addr; 1 - | Mfloat64, [IR addr], [FR res] -> - fprintf oc " vldr %a, [%a, #0]\n" freg res ireg addr; 1 - | _ -> - assert false - -let print_builtin_vload oc chunk args res = - fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; - let n = print_builtin_vload_common oc chunk args res in - fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n - -let print_builtin_vload_global oc chunk id ofs args res = - fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; - let n1 = loadsymbol oc IR14 id ofs in - let n2 = print_builtin_vload_common oc chunk [IR IR14] res in - fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n1 + n2 - -let print_builtin_vstore_common oc chunk args = - match chunk, args with - | (Mint8signed | Mint8unsigned), [IR addr; IR src] -> - fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1 - | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> - fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1 - | Mint32, [IR addr; IR src] -> - fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1 - | Mint64, [IR addr; IR src1; IR src2] -> - fprintf oc " str %a, [%a, #0]\n" ireg src2 ireg addr; - fprintf oc " str %a, [%a, #4]\n" ireg src1 ireg addr; 2 - | Mfloat32, [IR addr; FR src] -> - fprintf oc " vstr %a, [%a, #0]\n" freg_single src ireg addr; 1 - | Mfloat64, [IR addr; FR src] -> - fprintf oc " vstr %a, [%a, #0]\n" freg src ireg addr; 1 - | _ -> - assert false - -let print_builtin_vstore oc chunk args = - fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; - let n = print_builtin_vstore_common oc chunk args in - fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n - -let print_builtin_vstore_global oc chunk id ofs args = - fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; - let n1 = loadsymbol oc IR14 id ofs in - let n2 = print_builtin_vstore_common oc chunk (IR IR14 :: args) in - fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n1 + n2 - -(* Handling of varargs *) - -let current_function_stacksize = ref 0l -let current_function_sig = - ref { sig_args = []; sig_res = None; sig_cc = cc_default } - -let align n a = (n + a - 1) land (-a) - -let rec next_arg_location ir ofs = function - | [] -> - Int32.of_int (ir * 4 + ofs) - | (Tint | Tsingle | Tany32) :: l -> - if ir < 4 - then next_arg_location (ir + 1) ofs l - else next_arg_location ir (ofs + 4) l - | (Tfloat | Tlong | Tany64) :: l -> - if ir < 3 - then next_arg_location (align ir 2 + 2) ofs l - else next_arg_location ir (align ofs 8 + 8) l - -let print_builtin_va_start oc r = - if not (!current_function_sig).sig_cc.cc_vararg then - invalid_arg "Fatal error: va_start used in non-vararg function"; - let ofs = - Int32.add - (next_arg_location 0 0 (!current_function_sig).sig_args) - !current_function_stacksize in - let n = addimm oc "r14" "sp" (coqint_of_camlint ofs) in - fprintf oc " str r14, [%a, #0]\n" ireg r; - n + 1 - -(* Auxiliary for 64-bit integer arithmetic built-ins. They expand to - two instructions, one computing the low 32 bits of the result, - followed by another computing the high 32 bits. In cases where - the first instruction would overwrite arguments to the second - instruction, we must go through IR14 to hold the low 32 bits of the result. -*) - -let print_int64_arith oc conflict rl fn = - if conflict then begin - let n = fn IR14 in - fprintf oc " mov%t %a, %a\n" thumbS ireg rl ireg IR14; - n + 1 - end else - fn rl - -(* Handling of compiler-inlined builtins *) - -let print_builtin_inline oc name args res = - fprintf oc "%s begin %s\n" comment name; - let n = match name, args, res with - (* Integer arithmetic *) - | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] -> - fprintf oc " rev %a, %a\n" ireg res ireg a1; 1 - | "__builtin_bswap16", [IR a1], [IR res] -> - fprintf oc " rev16 %a, %a\n" ireg res ireg a1; 1 - | "__builtin_clz", [IR a1], [IR res] -> - fprintf oc " clz %a, %a\n" ireg res ireg a1; 1 - (* Float arithmetic *) - | "__builtin_fabs", [FR a1], [FR res] -> - fprintf oc " vabs.f64 %a, %a\n" freg res freg a1; 1 - | "__builtin_fsqrt", [FR a1], [FR res] -> - fprintf oc " vsqrt.f64 %a, %a\n" freg res freg a1; 1 - (* 64-bit integer arithmetic *) - | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> - print_int64_arith oc (rl = ah) rl (fun rl -> - fprintf oc " rsbs %a, %a, #0\n" ireg rl ireg al; - (* No "rsc" instruction in Thumb2. Emulate based on - rsc a, b, #0 == a <- AddWithCarry(~b, 0, carry) - == mvn a, b; adc a, a, #0 *) - if !Clflags.option_mthumb then begin - fprintf oc " mvn %a, %a\n" ireg rh ireg ah; - fprintf oc " adc %a, %a, #0\n" ireg rh ireg rh; 3 - end else begin - fprintf oc " rsc %a, %a, #0\n" ireg rh ireg ah; 2 - end) - | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - print_int64_arith oc (rl = ah || rl = bh) rl (fun rl -> - fprintf oc " adds %a, %a, %a\n" ireg rl ireg al ireg bl; - fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2) - | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - print_int64_arith oc (rl = ah || rl = bh) rl (fun rl -> - fprintf oc " subs %a, %a, %a\n" ireg rl ireg al ireg bl; - fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2) - | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> - fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1 - (* Memory accesses *) - | "__builtin_read16_reversed", [IR a1], [IR res] -> - fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg a1; - fprintf oc " rev16 %a, %a\n" ireg res ireg res; 2 - | "__builtin_read32_reversed", [IR a1], [IR res] -> - fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg a1; - fprintf oc " rev %a, %a\n" ireg res ireg res; 2 - | "__builtin_write16_reversed", [IR a1; IR a2], _ -> - fprintf oc " rev16 %a, %a\n" ireg IR14 ireg a2; - fprintf oc " strh %a, [%a, #0]\n" ireg IR14 ireg a1; 2 - | "__builtin_write32_reversed", [IR a1; IR a2], _ -> - fprintf oc " rev %a, %a\n" ireg IR14 ireg a2; - fprintf oc " str %a, [%a, #0]\n" ireg IR14 ireg a1; 2 - (* Synchronization *) - | "__builtin_membar", [], _ -> - 0 - | "__builtin_dmb", [], _ -> - fprintf oc " dmb\n"; 1 - | "__builtin_dsb", [], _ -> - fprintf oc " dsb\n"; 1 - | "__builtin_isb", [], _ -> - fprintf oc " isb\n"; 1 - - (* Vararg stuff *) - | "__builtin_va_start", [IR a], _ -> - print_builtin_va_start oc a - (* Catch-all *) - | _ -> - invalid_arg ("unrecognized builtin " ^ name) - in - fprintf oc "%s end %s\n" comment name; - n - -(* Fixing up calling conventions *) - -type direction = Incoming | Outgoing - -module FixupEABI = struct - - let ireg_param = function - | 0 -> IR0 | 1 -> IR1 | 2 -> IR2 | 3 -> IR3 | _ -> assert false - - let freg_param = function - | 0 -> FR0 | 1 -> FR1 | 2 -> FR2 | 3 -> FR3 | _ -> assert false - - let fixup_double oc dir f i1 i2 = - match dir with - | Incoming -> (* f <- (i1, i2) *) - fprintf oc " vmov %a, %a, %a\n" freg f ireg i1 ireg i2 - | Outgoing -> (* (i1, i2) <- f *) - fprintf oc " vmov %a, %a, %a\n" ireg i1 ireg i2 freg f - - let fixup_single oc dir f i = - match dir with - | Incoming -> (* f <- i *) - fprintf oc " vmov %a, %a\n" freg_single f ireg i - | Outgoing -> (* i <- f *) - fprintf oc " vmov %a, %a\n" ireg i freg_single f - - let fixup_conventions oc dir tyl = - let rec fixup i tyl = - if i >= 4 then 0 else - match tyl with - | [] -> 0 - | (Tint | Tany32) :: tyl' -> - fixup (i+1) tyl' - | Tlong :: tyl' -> - fixup (((i + 1) land (-2)) + 2) tyl' - | (Tfloat | Tany64) :: tyl' -> - let i = (i + 1) land (-2) in - if i >= 4 then 0 else begin - fixup_double oc dir (freg_param i) (ireg_param i) (ireg_param (i+1)); - 1 + fixup (i+2) tyl' - end - | Tsingle :: tyl' -> - fixup_single oc dir (freg_param i) (ireg_param i); - 1 + fixup (i+1) tyl' - in fixup 0 tyl - - let fixup_arguments oc dir sg = - fixup_conventions oc dir sg.sig_args - - let fixup_result oc dir sg = - fixup_conventions oc dir (proj_sig_res sg :: []) - -end - -module FixupHF = struct - - type fsize = Single | Double - - let rec find_single used pos = - if pos >= Array.length used then pos - else if used.(pos) then find_single used (pos + 1) - else begin used.(pos) <- true; pos end - - let rec find_double used pos = - if pos + 1 >= Array.length used then pos - else if used.(pos) || used.(pos + 1) then find_double used (pos + 2) - else begin used.(pos) <- true; used.(pos + 1) <- true; pos / 2 end - - let rec fixup_actions used fr tyl = - match tyl with - | [] -> [] - | (Tint | Tlong | Tany32) :: tyl' -> fixup_actions used fr tyl' - | (Tfloat | Tany64) :: tyl' -> - if fr >= 8 then [] else begin - let dr = find_double used 0 in - assert (dr < 8); - (fr, Double, dr) :: fixup_actions used (fr + 1) tyl' - end - | Tsingle :: tyl' -> - if fr >= 8 then [] else begin - let sr = find_single used 0 in - assert (sr < 16); - (fr, Single, sr) :: fixup_actions used (fr + 1) tyl' - end - - let rec fixup_outgoing oc = function - | [] -> 0 - | (fr, Double, dr) :: act -> - if fr = dr then fixup_outgoing oc act else begin - fprintf oc " vmov.f64 d%d, d%d\n" dr fr; - 1 + fixup_outgoing oc act - end - | (fr, Single, sr) :: act -> - fprintf oc " vmov.f32 s%d, s%d\n" sr (2*fr); - 1 + fixup_outgoing oc act - - let rec fixup_incoming oc = function - | [] -> 0 - | (fr, Double, dr) :: act -> - let n = fixup_incoming oc act in - if fr = dr then n else begin - fprintf oc " vmov.f64 d%d, d%d\n" fr dr; - 1 + n - end - | (fr, Single, sr) :: act -> - let n = fixup_incoming oc act in - if fr = sr then n else begin - fprintf oc " vmov.f32 s%d, s%d\n" (2*fr) sr; - 1 + n - end - - let fixup_arguments oc dir sg = - if sg.sig_cc.cc_vararg then - FixupEABI.fixup_arguments oc dir sg - else begin - let act = fixup_actions (Array.make 16 false) 0 sg.sig_args in - match dir with - | Outgoing -> fixup_outgoing oc act - | Incoming -> fixup_incoming oc act - end - - let fixup_result oc dir sg = - if sg.sig_cc.cc_vararg then - FixupEABI.fixup_result oc dir sg - else - 0 -end - -let (fixup_arguments, fixup_result) = - 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 - | SOimm n -> fprintf oc "#%a" coqint n - | SOreg r -> ireg oc r - | SOlsl(r, n) -> fprintf oc "%a, lsl #%a" ireg r coqint n - | SOlsr(r, n) -> fprintf oc "%a, lsr #%a" ireg r coqint n - | SOasr(r, n) -> fprintf oc "%a, asr #%a" ireg r coqint n - | SOror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n - -let print_instruction oc = function - (* Core instructions *) - | Padd(r1, r2, so) -> - fprintf oc " add%s %a, %a, %a\n" - (if !Clflags.option_mthumb && r2 <> IR14 then "s" else "") - ireg r1 ireg r2 shift_op so; 1 - | Pand(r1, r2, so) -> - fprintf oc " and%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 - | Pasr(r1, r2, r3) -> - fprintf oc " asr%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 ireg r3; 1 - | Pb lbl -> - fprintf oc " b %a\n" print_label lbl; 1 - | Pbc(bit, lbl) -> - fprintf oc " b%s %a\n" (condition_name bit) print_label lbl; 1 - | Pbsymb(id, sg) -> - let n = fixup_arguments oc Outgoing sg in - fprintf oc " b %a\n" print_symb id; - n + 1 - | Pbreg(r, sg) -> - let n = - if r = IR14 - then fixup_result oc Outgoing sg - else fixup_arguments oc Outgoing sg in - fprintf oc " bx %a\n" ireg r; - n + 1 - | Pblsymb(id, sg) -> - let n1 = fixup_arguments oc Outgoing sg in - fprintf oc " bl %a\n" print_symb id; - let n2 = fixup_result oc Incoming sg in - n1 + 1 + n2 - | Pblreg(r, sg) -> - let n1 = fixup_arguments oc Outgoing sg in - fprintf oc " blx %a\n" ireg r; - let n2 = fixup_result oc Incoming sg in - n1 + 1 + n2 - | Pbic(r1, r2, so) -> - fprintf oc " bic%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 - | Pcmp(r1, so) -> - fprintf oc " cmp %a, %a\n" ireg r1 shift_op so; 1 - | Peor(r1, r2, so) -> - fprintf oc " eor%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 - | Pldr(r1, r2, sa) | Pldr_a(r1, r2, sa) -> - fprintf oc " ldr %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 - | Pldrb(r1, r2, sa) -> - fprintf oc " ldrb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 - | Pldrh(r1, r2, sa) -> - fprintf oc " ldrh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 - | Pldrsb(r1, r2, sa) -> - fprintf oc " ldrsb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 - | Pldrsh(r1, r2, sa) -> - fprintf oc " ldrsh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 - | Plsl(r1, r2, r3) -> - fprintf oc " lsl%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 ireg r3; 1 - | Plsr(r1, r2, r3) -> - fprintf oc " lsr%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 ireg r3; 1 - | Pmla(r1, r2, r3, r4) -> - fprintf oc " mla %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 - | Pmov(r1, so) -> - fprintf oc " mov%t %a, %a\n" thumbS ireg r1 shift_op so; 1 - | Pmovw(r1, n) -> - fprintf oc " movw %a, #%a\n" ireg r1 coqint n; 1 - | Pmovt(r1, n) -> - fprintf oc " movt %a, #%a\n" ireg r1 coqint n; 1 - | Pmul(r1, r2, r3) -> - fprintf oc " mul %a, %a, %a\n" ireg r1 ireg r2 ireg r3; 1 - | Pmvn(r1, so) -> - fprintf oc " mvn%t %a, %a\n" thumbS ireg r1 shift_op so; 1 - | Porr(r1, r2, so) -> - fprintf oc " orr%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 - | Prsb(r1, r2, so) -> - fprintf oc " rsb%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 - | Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) -> - fprintf oc " str %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; - begin match r1, r2, sa with - | IR14, IR13, SOimm n -> Opt.cfi_rel_offset oc "lr" (camlint_of_coqint n) - | _ -> () - end; - 1 - | Pstrb(r1, r2, sa) -> - fprintf oc " strb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 - | Pstrh(r1, r2, sa) -> - fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 - | Psdiv -> - if Opt.hardware_idiv then begin - fprintf oc " sdiv r0, r0, r1\n"; 1 - end else begin - fprintf oc " bl __aeabi_idiv\n"; 1 - end - | Psbfx(r1, r2, lsb, sz) -> - fprintf oc " sbfx %a, %a, #%a, #%a\n" ireg r1 ireg r2 coqint lsb coqint sz; 1 - | Psmull(r1, r2, r3, r4) -> - fprintf oc " smull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 - | Psub(r1, r2, so) -> - fprintf oc " sub%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 - | Pudiv -> - if Opt.hardware_idiv then begin - fprintf oc " udiv r0, r0, r1\n"; 1 - end else begin - fprintf oc " bl __aeabi_uidiv\n"; 1 - end - | Pumull(r1, r2, r3, r4) -> - fprintf oc " umull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 - (* Floating-point VFD instructions *) - | Pfcpyd(r1, r2) -> - fprintf oc " vmov.f64 %a, %a\n" freg r1 freg r2; 1 - | Pfabsd(r1, r2) -> - fprintf oc " vabs.f64 %a, %a\n" freg r1 freg r2; 1 - | Pfnegd(r1, r2) -> - fprintf oc " vneg.f64 %a, %a\n" freg r1 freg r2; 1 - | Pfaddd(r1, r2, r3) -> - fprintf oc " vadd.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 - | Pfdivd(r1, r2, r3) -> - fprintf oc " vdiv.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 - | Pfmuld(r1, r2, r3) -> - fprintf oc " vmul.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 - | Pfsubd(r1, r2, r3) -> - fprintf oc " vsub.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 - | Pflid(r1, f) -> - let f = camlint64_of_coqint(Floats.Float.to_bits f) in - if Opt.vfpv3 && is_immediate_float64 f then begin - fprintf oc " vmov.f64 %a, #%F\n" - freg r1 (Int64.float_of_bits f); 1 - (* immediate floats have at most 4 bits of fraction, so they - should print exactly with OCaml's F decimal format. *) - end else if !literals_in_code then begin - let lbl = label_float f in - fprintf oc " vldr %a, .L%d @ %.12g\n" - freg r1 lbl (Int64.float_of_bits f); 1 - end else begin - let lbl = label_float f in - fprintf oc " movw r14, #:lower16:.L%d\n" lbl; - fprintf oc " movt r14, #:upper16:.L%d\n" lbl; - fprintf oc " vldr %a, [r14, #0] @ %.12g\n" - freg r1 (Int64.float_of_bits f); 3 - end - | Pfcmpd(r1, r2) -> - fprintf oc " vcmp.f64 %a, %a\n" freg r1 freg r2; - fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2 - | Pfcmpzd(r1) -> - fprintf oc " vcmp.f64 %a, #0\n" freg r1; - fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2 - | Pfsitod(r1, r2) -> - fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2; - fprintf oc " vcvt.f64.s32 %a, %a\n" freg r1 freg_single r1; 2 - | Pfuitod(r1, r2) -> - fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2; - fprintf oc " vcvt.f64.u32 %a, %a\n" freg r1 freg_single r1; 2 - | Pftosizd(r1, r2) -> - fprintf oc " vcvt.s32.f64 %a, %a\n" freg_single FR6 freg r2; - fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6; 2 - | Pftouizd(r1, r2) -> - fprintf oc " vcvt.u32.f64 %a, %a\n" freg_single FR6 freg r2; - fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6; 2 - | Pfabss(r1, r2) -> - fprintf oc " vabs.f32 %a, %a\n" freg_single r1 freg_single r2; 1 - | Pfnegs(r1, r2) -> - fprintf oc " vneg.f32 %a, %a\n" freg_single r1 freg_single r2; 1 - | Pfadds(r1, r2, r3) -> - fprintf oc " vadd.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 - | Pfdivs(r1, r2, r3) -> - fprintf oc " vdiv.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 - | Pfmuls(r1, r2, r3) -> - fprintf oc " vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 - | Pfsubs(r1, r2, r3) -> - fprintf oc " vsub.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 - | Pflis(r1, f) -> - let f = camlint_of_coqint(Floats.Float32.to_bits f) in - if Opt.vfpv3 && is_immediate_float32 f then begin - fprintf oc " vmov.f32 %a, #%F\n" - freg_single r1 (Int32.float_of_bits f); 1 - (* immediate floats have at most 4 bits of fraction, so they - should print exactly with OCaml's F decimal format. *) - end else if !literals_in_code then begin - let lbl = label_float32 f in - fprintf oc " vldr %a, .L%d @ %.12g\n" - freg_single r1 lbl (Int32.float_of_bits f); 1 - end else begin - fprintf oc " movw r14, #%ld\n" (Int32.logand f 0xFFFFl); - fprintf oc " movt r14, #%ld\n" (Int32.shift_right_logical f 16); - fprintf oc " vmov %a, r14 @ %.12g\n" - freg_single r1 (Int32.float_of_bits f); 3 - end - | Pfcmps(r1, r2) -> - fprintf oc " vcmp.f32 %a, %a\n" freg_single r1 freg_single r2; - fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2 - | Pfcmpzs(r1) -> - fprintf oc " vcmp.f32 %a, #0\n" freg_single r1; - fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2 - | Pfsitos(r1, r2) -> - fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2; - fprintf oc " vcvt.f32.s32 %a, %a\n" freg_single r1 freg_single r1; 2 - | Pfuitos(r1, r2) -> - fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2; - fprintf oc " vcvt.f32.u32 %a, %a\n" freg_single r1 freg_single r1; 2 - | Pftosizs(r1, r2) -> - fprintf oc " vcvt.s32.f32 %a, %a\n" freg_single FR6 freg_single r2; - fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6; 2 - | Pftouizs(r1, r2) -> - fprintf oc " vcvt.u32.f32 %a, %a\n" freg_single FR6 freg_single r2; - fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6; 2 - | Pfcvtsd(r1, r2) -> - fprintf oc " vcvt.f32.f64 %a, %a\n" freg_single r1 freg r2; 1 - | Pfcvtds(r1, r2) -> - fprintf oc " vcvt.f64.f32 %a, %a\n" freg r1 freg_single r2; 1 - | Pfldd(r1, r2, n) | Pfldd_a(r1, r2, n) -> - fprintf oc " vldr %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1 - | Pflds(r1, r2, n) -> - fprintf oc " vldr %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1 - | Pfstd(r1, r2, n) | Pfstd_a(r1, r2, n) -> - fprintf oc " vstr %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1 - | Pfsts(r1, r2, n) -> - fprintf oc " vstr %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1 - (* Pseudo-instructions *) - | Pallocframe(sz, ofs) -> - fprintf oc " mov r12, sp\n"; - if (!current_function_sig).sig_cc.cc_vararg then begin - fprintf oc " push {r0, r1, r2, r3}\n"; - Opt.cfi_adjust oc 16l - end; - let sz' = camlint_of_coqint sz in - let ninstr = subimm oc "sp" "sp" sz in - Opt.cfi_adjust oc sz'; - fprintf oc " str r12, [sp, #%a]\n" coqint ofs; - current_function_stacksize := sz'; - ninstr + (if (!current_function_sig).sig_cc.cc_vararg then 3 else 2) - | Pfreeframe(sz, ofs) -> - let sz = - if (!current_function_sig).sig_cc.cc_vararg - then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz)) - else sz in - if Asmgen.is_immed_arith sz - then fprintf oc " add sp, sp, #%a\n" coqint sz - else fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; 1 - | Plabel lbl -> - fprintf oc "%a:\n" print_label lbl; 0 - | Ploadsymbol(r1, id, ofs) -> - loadsymbol oc r1 id ofs - | Pmovite(cond, r1, ifso, ifnot) -> - fprintf oc " ite %s\n" (condition_name cond); - fprintf oc " mov%s %a, %a\n" - (condition_name cond) ireg r1 shift_op ifso; - fprintf oc " mov%s %a, %a\n" - (neg_condition_name cond) ireg r1 shift_op ifnot; 2 - | Pbtbl(r, tbl) -> - if !Clflags.option_mthumb then begin - let lbl = new_label() in - fprintf oc " adr r14, .L%d\n" lbl; - fprintf oc " add r14, r14, %a, lsl #2\n" ireg r; - fprintf oc " mov pc, r14\n"; - fprintf oc ".L%d:\n" lbl; - List.iter - (fun l -> fprintf oc " b.w %a\n" print_label l) - tbl; - 3 + List.length tbl - end else begin - fprintf oc " add pc, pc, %a, lsl #2\n" ireg r; - fprintf oc " nop\n"; - List.iter - (fun l -> fprintf oc " b %a\n" print_label l) - tbl; - 2 + List.length tbl - end - | Pbuiltin(ef, args, res) -> - begin match ef with - | EF_builtin(name, sg) -> - print_builtin_inline oc (extern_atom name) args res - | EF_vload chunk -> - print_builtin_vload oc chunk args res - | EF_vstore chunk -> - print_builtin_vstore oc chunk args - | EF_vload_global(chunk, id, ofs) -> - print_builtin_vload_global oc chunk id ofs args res - | EF_vstore_global(chunk, id, ofs) -> - print_builtin_vstore_global oc chunk id ofs args - | EF_memcpy(sz, al) -> - print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz)) - (Int32.to_int (camlint_of_coqint al)) args - | EF_annot_val(txt, targ) -> - print_annot_val oc (extern_atom txt) args res - | EF_inline_asm txt -> - fprintf oc "%s begin inline assembly\n" comment; - fprintf oc " %s\n" (extern_atom txt); - fprintf oc "%s end inline assembly\n" comment; - 5 (* hoping this is an upper bound... *) - | _ -> - assert false - end - | Pannot(ef, args) -> - begin match ef with - | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) targs args; 0 - | _ -> - assert false - end - -let no_fallthrough = function - | Pb _ -> true - | Pbsymb _ -> true - | Pbreg _ -> true - | _ -> false - -let rec print_instructions oc instrs = - match instrs with - | [] -> () - | i :: il -> - let n = print_instruction oc i in - currpos := !currpos + n * 4; - let d = distance_to_emit_constants() in - if d < 256 && no_fallthrough i then - emit_constants oc - else if d < 16 then begin - let lbl = new_label() in - fprintf oc " b .L%d\n" lbl; - emit_constants oc; - fprintf oc ".L%d:\n" lbl - end; - print_instructions oc il - -let print_function oc name fn = - Hashtbl.clear current_function_labels; - reset_constants(); - current_function_sig := fn.fn_sig; - currpos := 0; - let (text, lit) = - match C2C.atom_sections name with - | t :: l :: _ -> (t, l) - | _ -> (Section_text, Section_literal) in - section oc text; - let alignment = - match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in - fprintf oc " .balign %d\n" alignment; - if not (C2C.atom_is_static name) then - fprintf oc " .global %a\n" print_symb name; - if !Clflags.option_mthumb then - fprintf oc " .thumb_func\n"; - fprintf oc "%a:\n" print_symb name; - print_location oc (C2C.atom_location name); - Opt.cfi_startproc oc; - ignore (fixup_arguments oc Incoming fn.fn_sig); - print_instructions oc fn.fn_code; - if !literals_in_code then emit_constants oc; - Opt.cfi_endproc oc; - fprintf oc " .type %a, %%function\n" print_symb name; - fprintf oc " .size %a, . - %a\n" print_symb name print_symb name; - if not !literals_in_code && !size_constants > 0 then begin - section oc lit; - emit_constants oc - end - -(* Data *) - -let print_init oc = function - | Init_int8 n -> - fprintf oc " .byte %ld\n" (camlint_of_coqint n) - | Init_int16 n -> - fprintf oc " .short %ld\n" (camlint_of_coqint n) - | Init_int32 n -> - fprintf oc " .word %ld\n" (camlint_of_coqint n) - | Init_int64 n -> - fprintf oc " .quad %Ld\n" (camlint64_of_coqint n) - | Init_float32 n -> - fprintf oc " .word 0x%lx %s %.15g \n" (camlint_of_coqint (Floats.Float32.to_bits n)) - comment (camlfloat_of_coqfloat n) - | Init_float64 n -> - fprintf oc " .quad %Ld %s %.18g\n" (camlint64_of_coqint (Floats.Float.to_bits n)) - comment (camlfloat_of_coqfloat n) - | Init_space n -> - if Z.gt n Z.zero then - fprintf oc " .space %s\n" (Z.to_string n) - | Init_addrof(symb, ofs) -> - fprintf oc " .word %a\n" print_symb_ofs (symb, ofs) - -let print_init_data oc name id = - if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0 - && List.for_all (function Init_int8 _ -> true | _ -> false) id - then - fprintf oc " .ascii \"%s\"\n" (PrintCsyntax.string_of_init id) - else - List.iter (print_init oc) id - -let print_var oc name v = - match v.gvar_init with - | [] -> () - | _ -> - let sec = - match C2C.atom_sections name with - | [s] -> s - | _ -> Section_data true - and align = - match C2C.atom_alignof name with - | Some a -> a - | None -> 8 (* 8-alignment is a safe default *) - in - let name_sec = - name_of_section sec in - if name_sec <> "COMM" then begin - fprintf oc " %s\n" name_sec; - fprintf oc " .balign %d\n" align; - if not (C2C.atom_is_static name) then - fprintf oc " .global %a\n" print_symb name; - fprintf oc "%a:\n" print_symb name; - print_init_data oc name v.gvar_init; - fprintf oc " .type %a, %%object\n" print_symb name; - fprintf oc " .size %a, . - %a\n" print_symb name print_symb name - end else begin - let sz = - match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in - if C2C.atom_is_static name then - fprintf oc " .local %a\n" print_symb name; - fprintf oc " .comm %a, %s, %d\n" - print_symb name - (Z.to_string sz) - align - end - -let print_globdef oc (name, gdef) = - match gdef with - | Gfun(Internal f) -> print_function oc name f - | Gfun(External ef) -> () - | Gvar v -> print_var oc name v - - end) - -let print_program oc p = - let module Opt : 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 - | _ -> false - - - (* Emit .cfi directives *) - let cfi_startproc = - if Configuration.asm_supports_cfi then - (fun oc -> fprintf oc " .cfi_startproc\n") - else - (fun _ -> ()) - - let cfi_endproc = - if Configuration.asm_supports_cfi then - (fun oc ->fprintf oc " .cfi_endproc\n") - else - (fun _ -> ()) - - let cfi_adjust = - if Configuration.asm_supports_cfi then - (fun oc delta -> fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta) - else - (fun _ _ -> ()) - - let cfi_rel_offset = - if Configuration.asm_supports_cfi then - (fun oc reg ofs -> fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs) - else - (fun _ _ _ -> ()) - - end in - let module Printer = AsmPrinter(Opt) in - PrintAnnot.reset_filenames(); - PrintAnnot.print_version_and_options oc Printer.comment; - fprintf oc " .syntax unified\n"; - fprintf oc " .arch %s\n" - (match Configuration.model with - | "armv6" -> "armv6" - | "armv7a" -> "armv7-a" - | "armv7r" -> "armv7-r" - | "armv7m" -> "armv7-m" - | _ -> "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"); - List.iter (Printer.print_globdef oc) p.prog_defs; - PrintAnnot.close_filenames() - diff --git a/arm/PrintAsm.mli b/arm/PrintAsm.mli deleted file mode 100644 index aefe3a0a..00000000 --- a/arm/PrintAsm.mli +++ /dev/null @@ -1,13 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -val print_program: out_channel -> Asm.program -> unit diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml new file mode 100644 index 00000000..62dd2bc2 --- /dev/null +++ b/arm/TargetPrinter.ml @@ -0,0 +1,1143 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Printing ARM assembly code in asm syntax *) + +open Printf +open Datatypes +open Camlcoq +open Sections +open AST +open Memdata +open Asm +open PrintAsmaux + +(* Type for the ABI versions *) +type float_abi_type = + | Hard + | Soft + +(* Module type for the options *) +module type PRINTER_OPTIONS = + sig + val float_abi: float_abi_type + val vfpv3: bool + val hardware_idiv: bool + end + +(* Module containing the printing functions *) + +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 + + let symbol_offset oc (symb, ofs) = + symbol oc symb; + let ofs = camlint_of_coqint ofs in + if ofs <> 0l then fprintf oc " + %ld" ofs + + let int_reg_name = function + | IR0 -> "r0" | IR1 -> "r1" | IR2 -> "r2" | IR3 -> "r3" + | 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" + | TChs -> "hs" + | TClo -> "lo" + | TCmi -> "mi" + | TCpl -> "pl" + | TChi -> "hi" + | TCls -> "ls" + | TCge -> "ge" + | TClt -> "lt" + | TCgt -> "gt" + | TCle -> "le" + + let neg_condition_name = function + | TCeq -> "ne" + | TCne -> "eq" + | TChs -> "lo" + | TClo -> "hs" + | TCmi -> "pl" + | TCpl -> "mi" + | TChi -> "ls" + | TCls -> "hi" + | TCge -> "lt" + | 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) + and + asr + bic + eor + lsl + lsr + mov + mvn + orr + rsb + sub (but not sp - imm) + The proof of Asmgen shows that CompCert-generated code behaves the + same whether flags are updated or not by those instructions. The + following printing function adds a "S" suffix if we are in Thumb2 + mode. *) + + let thumbS oc = + if !Clflags.option_mthumb then output_char oc 's' + +(* Names of sections *) + + let name_of_section = function + | Section_text -> ".text" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".section .rodata" else "COMM" + | Section_string -> ".section .rodata" + | Section_literal -> ".text" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\",\"a%s%s\",%%progbits" + s (if wr then "w" else "") (if ex then "x" else "") + + 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 + with Not_found -> + let lbl' = new_label() in + Hashtbl.add float_labels bf lbl'; + 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 + with Not_found -> + let lbl' = new_label() in + Hashtbl.add float32_labels bf lbl'; + 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) + with Not_found -> + let lbl' = new_label() in + Hashtbl.add symbol_labels (id, ofs) lbl'; + 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 + (fun bf lbl -> + (* Little-endian floats *) + let bfhi = Int64.shift_right_logical bf 32 + and bflo = Int64.logand bf 0xFFFF_FFFFL in + fprintf oc ".L%d: .word 0x%Lx, 0x%Lx\n" lbl bflo bfhi) + float_labels; + Hashtbl.iter + (fun bf lbl -> + fprintf oc ".L%d: .word 0x%lx\n" lbl bf) + float32_labels; + Hashtbl.iter + (fun (id, ofs) lbl -> + fprintf oc ".L%d: .word %a\n" + 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" + ireg r symbol_offset (id, ofs); + fprintf oc " movt %a, #:upper16:%a\n" + 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" + 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 + | hd::tl as l -> + fprintf oc " mov %s, #%a\n" dst coqint hd; + List.iter + (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 + | hd::tl as l -> + fprintf oc " add %s, %s, #%a\n" dst src coqint hd; + List.iter + (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 + | hd::tl as l -> + fprintf oc " sub %s, %s, #%a\n" dst src coqint hd; + List.iter + (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 = + PrintAnnot.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) + +(* Built-ins. They come in two flavors: + - annotation statements: take their arguments in registers or stack + locations; generate no code; + - inlined by the compiler: take their arguments in arbitrary + registers. +*) + +(* Handling of annotations *) + + let print_annot_stmt oc txt targs args = + if Str.string_match re_file_line txt 0 then begin + print_file_line oc (Str.matched_group 1 txt) + (int_of_string (Str.matched_group 2 txt)) + end else begin + fprintf oc "%s annotation: " comment; + PrintAnnot.print_annot_stmt preg "sp" oc txt targs args + end + + let print_annot_val oc txt args res = + fprintf oc "%s annotation: " comment; + PrintAnnot.print_annot_val preg oc txt args; + match args, res with + | [IR src], [IR dst] -> + if dst = src then 0 else (fprintf oc " mov %a, %a\n" ireg dst ireg src; 1) + | [FR src], [FR dst] -> + if dst = src then 0 else (fprintf oc " vmov.f64 %a, %a\n" freg dst freg src; 1) + | _, _ -> assert false + +(* Handling of memcpy *) + +(* The ARM has strict alignment constraints for 2 and 4 byte accesses. + 8-byte accesses must be 4-aligned. *) + + let print_builtin_memcpy_small oc sz al src dst = + let rec copy ofs sz ninstr = + if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin + fprintf oc " vldr %a, [%a, #%d]\n" freg FR7 ireg src ofs; + fprintf oc " vstr %a, [%a, #%d]\n" freg FR7 ireg dst ofs; + copy (ofs + 8) (sz - 8) (ninstr + 2) + end else if sz >= 4 && al >= 4 then begin + fprintf oc " ldr %a, [%a, #%d]\n" ireg IR14 ireg src ofs; + fprintf oc " str %a, [%a, #%d]\n" ireg IR14 ireg dst ofs; + copy (ofs + 4) (sz - 4) (ninstr + 2) + end else if sz >= 2 && al >= 2 then begin + fprintf oc " ldrh %a, [%a, #%d]\n" ireg IR14 ireg src ofs; + fprintf oc " strh %a, [%a, #%d]\n" ireg IR14 ireg dst ofs; + copy (ofs + 2) (sz - 2) (ninstr + 2) + end else if sz >= 1 then begin + fprintf oc " ldrb %a, [%a, #%d]\n" ireg IR14 ireg src ofs; + fprintf oc " strb %a, [%a, #%d]\n" ireg IR14 ireg dst ofs; + copy (ofs + 1) (sz - 1) (ninstr + 2) + end else + ninstr in + copy 0 sz 0 + + let print_builtin_memcpy_big oc sz al src dst = + assert (sz >= al); + assert (sz mod al = 0); + assert (src = IR2); + assert (dst = IR3); + let (load, store, chunksize) = + if al >= 4 then ("ldr", "str", 4) + else if al = 2 then ("ldrh", "strh", 2) + else ("ldrb", "strb", 1) in + let n = movimm oc "r14" (coqint_of_camlint (Int32.of_int (sz / chunksize))) in + let lbl = new_label() in + fprintf oc ".L%d: %s %a, [%a], #%d\n" lbl load ireg IR12 ireg src chunksize; + fprintf oc " subs %a, %a, #1\n" ireg IR14 ireg IR14; + fprintf oc " %s %a, [%a], #%d\n" store ireg IR12 ireg dst chunksize; + fprintf oc " bne .L%d\n" lbl; + n + 4 + + let print_builtin_memcpy oc sz al args = + let (dst, src) = + match args with [IR d; IR s] -> (d, s) | _ -> assert false in + fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n" + comment sz al; + let n = + if sz <= 32 + then print_builtin_memcpy_small oc sz al src dst + else print_builtin_memcpy_big oc sz al src dst in + fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment; n + +(* Handling of volatile reads and writes *) + + let print_builtin_vload_common oc chunk args res = + match chunk, args, res with + | Mint8unsigned, [IR addr], [IR res] -> + fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint8signed, [IR addr], [IR res] -> + fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint16unsigned, [IR addr], [IR res] -> + fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint16signed, [IR addr], [IR res] -> + fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint32, [IR addr], [IR res] -> + fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint64, [IR addr], [IR res1; IR res2] -> + if addr <> res2 then begin + fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr; + fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr + end else begin + fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr; + fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr + end; 2 + | Mfloat32, [IR addr], [FR res] -> + fprintf oc " vldr %a, [%a, #0]\n" freg_single res ireg addr; 1 + | Mfloat64, [IR addr], [FR res] -> + fprintf oc " vldr %a, [%a, #0]\n" freg res ireg addr; 1 + | _ -> + assert false + + let print_builtin_vload oc chunk args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + let n = print_builtin_vload_common oc chunk args res in + fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n + + let print_builtin_vload_global oc chunk id ofs args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + let n1 = loadsymbol oc IR14 id ofs in + let n2 = print_builtin_vload_common oc chunk [IR IR14] res in + fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n1 + n2 + + let print_builtin_vstore_common oc chunk args = + match chunk, args with + | (Mint8signed | Mint8unsigned), [IR addr; IR src] -> + fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1 + | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> + fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1 + | Mint32, [IR addr; IR src] -> + fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1 + | Mint64, [IR addr; IR src1; IR src2] -> + fprintf oc " str %a, [%a, #0]\n" ireg src2 ireg addr; + fprintf oc " str %a, [%a, #4]\n" ireg src1 ireg addr; 2 + | Mfloat32, [IR addr; FR src] -> + fprintf oc " vstr %a, [%a, #0]\n" freg_single src ireg addr; 1 + | Mfloat64, [IR addr; FR src] -> + fprintf oc " vstr %a, [%a, #0]\n" freg src ireg addr; 1 + | _ -> + assert false + + let print_builtin_vstore oc chunk args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + let n = print_builtin_vstore_common oc chunk args in + fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n + + let print_builtin_vstore_global oc chunk id ofs args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + let n1 = loadsymbol oc IR14 id ofs in + let n2 = print_builtin_vstore_common oc chunk (IR IR14 :: args) in + fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n1 + n2 + +(* Handling of varargs *) + + let align n a = (n + a - 1) land (-a) + + let rec next_arg_location ir ofs = function + | [] -> + Int32.of_int (ir * 4 + ofs) + | (Tint | Tsingle | Tany32) :: l -> + if ir < 4 + then next_arg_location (ir + 1) ofs l + else next_arg_location ir (ofs + 4) l + | (Tfloat | Tlong | Tany64) :: l -> + if ir < 3 + then next_arg_location (align ir 2 + 2) ofs l + else next_arg_location ir (align ofs 8 + 8) l + + let print_builtin_va_start oc r = + if not (!current_function_sig).sig_cc.cc_vararg then + invalid_arg "Fatal error: va_start used in non-vararg function"; + let ofs = + Int32.add + (next_arg_location 0 0 (!current_function_sig).sig_args) + !current_function_stacksize in + let n = addimm oc "r14" "sp" (coqint_of_camlint ofs) in + fprintf oc " str r14, [%a, #0]\n" ireg r; + n + 1 + +(* Auxiliary for 64-bit integer arithmetic built-ins. They expand to + two instructions, one computing the low 32 bits of the result, + followed by another computing the high 32 bits. In cases where + the first instruction would overwrite arguments to the second + instruction, we must go through IR14 to hold the low 32 bits of the result. + *) + + let print_int64_arith oc conflict rl fn = + if conflict then begin + let n = fn IR14 in + fprintf oc " mov%t %a, %a\n" thumbS ireg rl ireg IR14; + n + 1 + end else + fn rl + +(* Handling of compiler-inlined builtins *) + + let print_builtin_inline oc name args res = + fprintf oc "%s begin %s\n" comment name; + let n = match name, args, res with + (* Integer arithmetic *) + | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] -> + fprintf oc " rev %a, %a\n" ireg res ireg a1; 1 + | "__builtin_bswap16", [IR a1], [IR res] -> + fprintf oc " rev16 %a, %a\n" ireg res ireg a1; 1 + | "__builtin_clz", [IR a1], [IR res] -> + fprintf oc " clz %a, %a\n" ireg res ireg a1; 1 + (* Float arithmetic *) + | "__builtin_fabs", [FR a1], [FR res] -> + fprintf oc " vabs.f64 %a, %a\n" freg res freg a1; 1 + | "__builtin_fsqrt", [FR a1], [FR res] -> + fprintf oc " vsqrt.f64 %a, %a\n" freg res freg a1; 1 + (* 64-bit integer arithmetic *) + | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> + print_int64_arith oc (rl = ah) rl (fun rl -> + fprintf oc " rsbs %a, %a, #0\n" ireg rl ireg al; + (* No "rsc" instruction in Thumb2. Emulate based on + rsc a, b, #0 == a <- AddWithCarry(~b, 0, carry) + == mvn a, b; adc a, a, #0 *) + if !Clflags.option_mthumb then begin + fprintf oc " mvn %a, %a\n" ireg rh ireg ah; + fprintf oc " adc %a, %a, #0\n" ireg rh ireg rh; 3 + end else begin + fprintf oc " rsc %a, %a, #0\n" ireg rh ireg ah; 2 + end) + | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + print_int64_arith oc (rl = ah || rl = bh) rl (fun rl -> + fprintf oc " adds %a, %a, %a\n" ireg rl ireg al ireg bl; + fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2) + | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + print_int64_arith oc (rl = ah || rl = bh) rl (fun rl -> + fprintf oc " subs %a, %a, %a\n" ireg rl ireg al ireg bl; + fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2) + | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> + fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1 + (* Memory accesses *) + | "__builtin_read16_reversed", [IR a1], [IR res] -> + fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg a1; + fprintf oc " rev16 %a, %a\n" ireg res ireg res; 2 + | "__builtin_read32_reversed", [IR a1], [IR res] -> + fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg a1; + fprintf oc " rev %a, %a\n" ireg res ireg res; 2 + | "__builtin_write16_reversed", [IR a1; IR a2], _ -> + fprintf oc " rev16 %a, %a\n" ireg IR14 ireg a2; + fprintf oc " strh %a, [%a, #0]\n" ireg IR14 ireg a1; 2 + | "__builtin_write32_reversed", [IR a1; IR a2], _ -> + fprintf oc " rev %a, %a\n" ireg IR14 ireg a2; + fprintf oc " str %a, [%a, #0]\n" ireg IR14 ireg a1; 2 + (* Synchronization *) + | "__builtin_membar", [], _ -> + 0 + | "__builtin_dmb", [], _ -> + fprintf oc " dmb\n"; 1 + | "__builtin_dsb", [], _ -> + fprintf oc " dsb\n"; 1 + | "__builtin_isb", [], _ -> + fprintf oc " isb\n"; 1 + + (* Vararg stuff *) + | "__builtin_va_start", [IR a], _ -> + print_builtin_va_start oc a + (* Catch-all *) + | _ -> + invalid_arg ("unrecognized builtin " ^ name) + in + fprintf oc "%s end %s\n" comment name; + n + +(* Fixing up calling conventions *) + + type direction = Incoming | Outgoing + + module FixupEABI = struct + + let ireg_param = function + | 0 -> IR0 | 1 -> IR1 | 2 -> IR2 | 3 -> IR3 | _ -> assert false + + let freg_param = function + | 0 -> FR0 | 1 -> FR1 | 2 -> FR2 | 3 -> FR3 | _ -> assert false + + let fixup_double oc dir f i1 i2 = + match dir with + | Incoming -> (* f <- (i1, i2) *) + fprintf oc " vmov %a, %a, %a\n" freg f ireg i1 ireg i2 + | Outgoing -> (* (i1, i2) <- f *) + fprintf oc " vmov %a, %a, %a\n" ireg i1 ireg i2 freg f + + let fixup_single oc dir f i = + match dir with + | Incoming -> (* f <- i *) + fprintf oc " vmov %a, %a\n" freg_single f ireg i + | Outgoing -> (* i <- f *) + fprintf oc " vmov %a, %a\n" ireg i freg_single f + + let fixup_conventions oc dir tyl = + let rec fixup i tyl = + if i >= 4 then 0 else + match tyl with + | [] -> 0 + | (Tint | Tany32) :: tyl' -> + fixup (i+1) tyl' + | Tlong :: tyl' -> + fixup (((i + 1) land (-2)) + 2) tyl' + | (Tfloat | Tany64) :: tyl' -> + let i = (i + 1) land (-2) in + if i >= 4 then 0 else begin + fixup_double oc dir (freg_param i) (ireg_param i) (ireg_param (i+1)); + 1 + fixup (i+2) tyl' + end + | Tsingle :: tyl' -> + fixup_single oc dir (freg_param i) (ireg_param i); + 1 + fixup (i+1) tyl' + in fixup 0 tyl + + let fixup_arguments oc dir sg = + fixup_conventions oc dir sg.sig_args + + let fixup_result oc dir sg = + fixup_conventions oc dir (proj_sig_res sg :: []) + + end + + module FixupHF = struct + + type fsize = Single | Double + + let rec find_single used pos = + if pos >= Array.length used then pos + else if used.(pos) then find_single used (pos + 1) + else begin used.(pos) <- true; pos end + + let rec find_double used pos = + if pos + 1 >= Array.length used then pos + else if used.(pos) || used.(pos + 1) then find_double used (pos + 2) + else begin used.(pos) <- true; used.(pos + 1) <- true; pos / 2 end + + let rec fixup_actions used fr tyl = + match tyl with + | [] -> [] + | (Tint | Tlong | Tany32) :: tyl' -> fixup_actions used fr tyl' + | (Tfloat | Tany64) :: tyl' -> + if fr >= 8 then [] else begin + let dr = find_double used 0 in + assert (dr < 8); + (fr, Double, dr) :: fixup_actions used (fr + 1) tyl' + end + | Tsingle :: tyl' -> + if fr >= 8 then [] else begin + let sr = find_single used 0 in + assert (sr < 16); + (fr, Single, sr) :: fixup_actions used (fr + 1) tyl' + end + + let rec fixup_outgoing oc = function + | [] -> 0 + | (fr, Double, dr) :: act -> + if fr = dr then fixup_outgoing oc act else begin + fprintf oc " vmov.f64 d%d, d%d\n" dr fr; + 1 + fixup_outgoing oc act + end + | (fr, Single, sr) :: act -> + fprintf oc " vmov.f32 s%d, s%d\n" sr (2*fr); + 1 + fixup_outgoing oc act + + let rec fixup_incoming oc = function + | [] -> 0 + | (fr, Double, dr) :: act -> + let n = fixup_incoming oc act in + if fr = dr then n else begin + fprintf oc " vmov.f64 d%d, d%d\n" fr dr; + 1 + n + end + | (fr, Single, sr) :: act -> + let n = fixup_incoming oc act in + if fr = sr then n else begin + fprintf oc " vmov.f32 s%d, s%d\n" (2*fr) sr; + 1 + n + end + + let fixup_arguments oc dir sg = + if sg.sig_cc.cc_vararg then + FixupEABI.fixup_arguments oc dir sg + else begin + let act = fixup_actions (Array.make 16 false) 0 sg.sig_args in + match dir with + | Outgoing -> fixup_outgoing oc act + | Incoming -> fixup_incoming oc act + end + + let fixup_result oc dir sg = + if sg.sig_cc.cc_vararg then + FixupEABI.fixup_result oc dir sg + else + 0 + end + + let (fixup_arguments, fixup_result) = + 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 + | SOimm n -> fprintf oc "#%a" coqint n + | SOreg r -> ireg oc r + | SOlsl(r, n) -> fprintf oc "%a, lsl #%a" ireg r coqint n + | SOlsr(r, n) -> fprintf oc "%a, lsr #%a" ireg r coqint n + | SOasr(r, n) -> fprintf oc "%a, asr #%a" ireg r coqint n + | SOror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n + + let print_instruction oc = function + (* Core instructions *) + | Padd(r1, r2, so) -> + fprintf oc " add%s %a, %a, %a\n" + (if !Clflags.option_mthumb && r2 <> IR14 then "s" else "") + ireg r1 ireg r2 shift_op so; 1 + | Pand(r1, r2, so) -> + fprintf oc " and%t %a, %a, %a\n" + thumbS ireg r1 ireg r2 shift_op so; 1 + | Pasr(r1, r2, r3) -> + fprintf oc " asr%t %a, %a, %a\n" + thumbS ireg r1 ireg r2 ireg r3; 1 + | Pb lbl -> + fprintf oc " b %a\n" print_label lbl; 1 + | Pbc(bit, lbl) -> + fprintf oc " b%s %a\n" (condition_name bit) print_label lbl; 1 + | Pbsymb(id, sg) -> + let n = fixup_arguments oc Outgoing sg in + fprintf oc " b %a\n" symbol id; + n + 1 + | Pbreg(r, sg) -> + let n = + if r = IR14 + then fixup_result oc Outgoing sg + else fixup_arguments oc Outgoing sg in + fprintf oc " bx %a\n" ireg r; + n + 1 + | Pblsymb(id, sg) -> + let n1 = fixup_arguments oc Outgoing sg in + fprintf oc " bl %a\n" symbol id; + let n2 = fixup_result oc Incoming sg in + n1 + 1 + n2 + | Pblreg(r, sg) -> + let n1 = fixup_arguments oc Outgoing sg in + fprintf oc " blx %a\n" ireg r; + let n2 = fixup_result oc Incoming sg in + n1 + 1 + n2 + | Pbic(r1, r2, so) -> + fprintf oc " bic%t %a, %a, %a\n" + thumbS ireg r1 ireg r2 shift_op so; 1 + | Pcmp(r1, so) -> + fprintf oc " cmp %a, %a\n" ireg r1 shift_op so; 1 + | Peor(r1, r2, so) -> + fprintf oc " eor%t %a, %a, %a\n" + thumbS ireg r1 ireg r2 shift_op so; 1 + | Pldr(r1, r2, sa) | Pldr_a(r1, r2, sa) -> + fprintf oc " ldr %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + | Pldrb(r1, r2, sa) -> + fprintf oc " ldrb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + | Pldrh(r1, r2, sa) -> + fprintf oc " ldrh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + | Pldrsb(r1, r2, sa) -> + fprintf oc " ldrsb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + | Pldrsh(r1, r2, sa) -> + fprintf oc " ldrsh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + | Plsl(r1, r2, r3) -> + fprintf oc " lsl%t %a, %a, %a\n" + thumbS ireg r1 ireg r2 ireg r3; 1 + | Plsr(r1, r2, r3) -> + fprintf oc " lsr%t %a, %a, %a\n" + thumbS ireg r1 ireg r2 ireg r3; 1 + | Pmla(r1, r2, r3, r4) -> + fprintf oc " mla %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 + | Pmov(r1, so) -> + fprintf oc " mov%t %a, %a\n" thumbS ireg r1 shift_op so; 1 + | Pmovw(r1, n) -> + fprintf oc " movw %a, #%a\n" ireg r1 coqint n; 1 + | Pmovt(r1, n) -> + fprintf oc " movt %a, #%a\n" ireg r1 coqint n; 1 + | Pmul(r1, r2, r3) -> + fprintf oc " mul %a, %a, %a\n" ireg r1 ireg r2 ireg r3; 1 + | Pmvn(r1, so) -> + fprintf oc " mvn%t %a, %a\n" thumbS ireg r1 shift_op so; 1 + | Porr(r1, r2, so) -> + fprintf oc " orr%t %a, %a, %a\n" + thumbS ireg r1 ireg r2 shift_op so; 1 + | Prsb(r1, r2, so) -> + fprintf oc " rsb%t %a, %a, %a\n" + thumbS ireg r1 ireg r2 shift_op so; 1 + | Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) -> + fprintf oc " str %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; + begin match r1, r2, sa with + | IR14, IR13, SOimm n -> cfi_rel_offset oc "lr" (camlint_of_coqint n) + | _ -> () + end; + 1 + | Pstrb(r1, r2, sa) -> + fprintf oc " strb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + | Pstrh(r1, r2, sa) -> + fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + | Psdiv -> + if Opt.hardware_idiv then begin + fprintf oc " sdiv r0, r0, r1\n"; 1 + end else begin + fprintf oc " bl __aeabi_idiv\n"; 1 + end + | Psbfx(r1, r2, lsb, sz) -> + fprintf oc " sbfx %a, %a, #%a, #%a\n" ireg r1 ireg r2 coqint lsb coqint sz; 1 + | Psmull(r1, r2, r3, r4) -> + fprintf oc " smull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 + | Psub(r1, r2, so) -> + fprintf oc " sub%t %a, %a, %a\n" + thumbS ireg r1 ireg r2 shift_op so; 1 + | Pudiv -> + if Opt.hardware_idiv then begin + fprintf oc " udiv r0, r0, r1\n"; 1 + end else begin + fprintf oc " bl __aeabi_uidiv\n"; 1 + end + | Pumull(r1, r2, r3, r4) -> + fprintf oc " umull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 + (* Floating-point VFD instructions *) + | Pfcpyd(r1, r2) -> + fprintf oc " vmov.f64 %a, %a\n" freg r1 freg r2; 1 + | Pfabsd(r1, r2) -> + fprintf oc " vabs.f64 %a, %a\n" freg r1 freg r2; 1 + | Pfnegd(r1, r2) -> + fprintf oc " vneg.f64 %a, %a\n" freg r1 freg r2; 1 + | Pfaddd(r1, r2, r3) -> + fprintf oc " vadd.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 + | Pfdivd(r1, r2, r3) -> + fprintf oc " vdiv.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 + | Pfmuld(r1, r2, r3) -> + fprintf oc " vmul.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 + | Pfsubd(r1, r2, r3) -> + fprintf oc " vsub.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 + | Pflid(r1, f) -> + let f = camlint64_of_coqint(Floats.Float.to_bits f) in + if Opt.vfpv3 && is_immediate_float64 f then begin + fprintf oc " vmov.f64 %a, #%F\n" + freg r1 (Int64.float_of_bits f); 1 + (* immediate floats have at most 4 bits of fraction, so they + should print exactly with OCaml's F decimal format. *) + end else if !literals_in_code then begin + let lbl = label_float f in + fprintf oc " vldr %a, .L%d @ %.12g\n" + freg r1 lbl (Int64.float_of_bits f); 1 + end else begin + let lbl = label_float f in + fprintf oc " movw r14, #:lower16:.L%d\n" lbl; + fprintf oc " movt r14, #:upper16:.L%d\n" lbl; + fprintf oc " vldr %a, [r14, #0] @ %.12g\n" + freg r1 (Int64.float_of_bits f); 3 + end + | Pfcmpd(r1, r2) -> + fprintf oc " vcmp.f64 %a, %a\n" freg r1 freg r2; + fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2 + | Pfcmpzd(r1) -> + fprintf oc " vcmp.f64 %a, #0\n" freg r1; + fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2 + | Pfsitod(r1, r2) -> + fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2; + fprintf oc " vcvt.f64.s32 %a, %a\n" freg r1 freg_single r1; 2 + | Pfuitod(r1, r2) -> + fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2; + fprintf oc " vcvt.f64.u32 %a, %a\n" freg r1 freg_single r1; 2 + | Pftosizd(r1, r2) -> + fprintf oc " vcvt.s32.f64 %a, %a\n" freg_single FR6 freg r2; + fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6; 2 + | Pftouizd(r1, r2) -> + fprintf oc " vcvt.u32.f64 %a, %a\n" freg_single FR6 freg r2; + fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6; 2 + | Pfabss(r1, r2) -> + fprintf oc " vabs.f32 %a, %a\n" freg_single r1 freg_single r2; 1 + | Pfnegs(r1, r2) -> + fprintf oc " vneg.f32 %a, %a\n" freg_single r1 freg_single r2; 1 + | Pfadds(r1, r2, r3) -> + fprintf oc " vadd.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 + | Pfdivs(r1, r2, r3) -> + fprintf oc " vdiv.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 + | Pfmuls(r1, r2, r3) -> + fprintf oc " vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 + | Pfsubs(r1, r2, r3) -> + fprintf oc " vsub.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 + | Pflis(r1, f) -> + let f = camlint_of_coqint(Floats.Float32.to_bits f) in + if Opt.vfpv3 && is_immediate_float32 f then begin + fprintf oc " vmov.f32 %a, #%F\n" + freg_single r1 (Int32.float_of_bits f); 1 + (* immediate floats have at most 4 bits of fraction, so they + should print exactly with OCaml's F decimal format. *) + end else if !literals_in_code then begin + let lbl = label_float32 f in + fprintf oc " vldr %a, .L%d @ %.12g\n" + freg_single r1 lbl (Int32.float_of_bits f); 1 + end else begin + fprintf oc " movw r14, #%ld\n" (Int32.logand f 0xFFFFl); + fprintf oc " movt r14, #%ld\n" (Int32.shift_right_logical f 16); + fprintf oc " vmov %a, r14 @ %.12g\n" + freg_single r1 (Int32.float_of_bits f); 3 + end + | Pfcmps(r1, r2) -> + fprintf oc " vcmp.f32 %a, %a\n" freg_single r1 freg_single r2; + fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2 + | Pfcmpzs(r1) -> + fprintf oc " vcmp.f32 %a, #0\n" freg_single r1; + fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2 + | Pfsitos(r1, r2) -> + fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2; + fprintf oc " vcvt.f32.s32 %a, %a\n" freg_single r1 freg_single r1; 2 + | Pfuitos(r1, r2) -> + fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2; + fprintf oc " vcvt.f32.u32 %a, %a\n" freg_single r1 freg_single r1; 2 + | Pftosizs(r1, r2) -> + fprintf oc " vcvt.s32.f32 %a, %a\n" freg_single FR6 freg_single r2; + fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6; 2 + | Pftouizs(r1, r2) -> + fprintf oc " vcvt.u32.f32 %a, %a\n" freg_single FR6 freg_single r2; + fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6; 2 + | Pfcvtsd(r1, r2) -> + fprintf oc " vcvt.f32.f64 %a, %a\n" freg_single r1 freg r2; 1 + | Pfcvtds(r1, r2) -> + fprintf oc " vcvt.f64.f32 %a, %a\n" freg r1 freg_single r2; 1 + | Pfldd(r1, r2, n) | Pfldd_a(r1, r2, n) -> + fprintf oc " vldr %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1 + | Pflds(r1, r2, n) -> + fprintf oc " vldr %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1 + | Pfstd(r1, r2, n) | Pfstd_a(r1, r2, n) -> + fprintf oc " vstr %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1 + | Pfsts(r1, r2, n) -> + fprintf oc " vstr %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1 + (* Pseudo-instructions *) + | Pallocframe(sz, ofs) -> + fprintf oc " mov r12, sp\n"; + if (!current_function_sig).sig_cc.cc_vararg then begin + fprintf oc " push {r0, r1, r2, r3}\n"; + cfi_adjust oc 16l + end; + let sz' = camlint_of_coqint sz in + let ninstr = subimm oc "sp" "sp" sz in + cfi_adjust oc sz'; + fprintf oc " str r12, [sp, #%a]\n" coqint ofs; + current_function_stacksize := sz'; + ninstr + (if (!current_function_sig).sig_cc.cc_vararg then 3 else 2) + | Pfreeframe(sz, ofs) -> + let sz = + if (!current_function_sig).sig_cc.cc_vararg + then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz)) + else sz in + if Asmgen.is_immed_arith sz + then fprintf oc " add sp, sp, #%a\n" coqint sz + else fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; 1 + | Plabel lbl -> + fprintf oc "%a:\n" print_label lbl; 0 + | Ploadsymbol(r1, id, ofs) -> + loadsymbol oc r1 id ofs + | Pmovite(cond, r1, ifso, ifnot) -> + fprintf oc " ite %s\n" (condition_name cond); + fprintf oc " mov%s %a, %a\n" + (condition_name cond) ireg r1 shift_op ifso; + fprintf oc " mov%s %a, %a\n" + (neg_condition_name cond) ireg r1 shift_op ifnot; 2 + | Pbtbl(r, tbl) -> + if !Clflags.option_mthumb then begin + let lbl = new_label() in + fprintf oc " adr r14, .L%d\n" lbl; + fprintf oc " add r14, r14, %a, lsl #2\n" ireg r; + fprintf oc " mov pc, r14\n"; + fprintf oc ".L%d:\n" lbl; + List.iter + (fun l -> fprintf oc " b.w %a\n" print_label l) + tbl; + 3 + List.length tbl + end else begin + fprintf oc " add pc, pc, %a, lsl #2\n" ireg r; + fprintf oc " nop\n"; + List.iter + (fun l -> fprintf oc " b %a\n" print_label l) + tbl; + 2 + List.length tbl + end + | Pbuiltin(ef, args, res) -> + begin match ef with + | EF_builtin(name, sg) -> + print_builtin_inline oc (extern_atom name) args res + | EF_vload chunk -> + print_builtin_vload oc chunk args res + | EF_vstore chunk -> + print_builtin_vstore oc chunk args + | EF_vload_global(chunk, id, ofs) -> + print_builtin_vload_global oc chunk id ofs args res + | EF_vstore_global(chunk, id, ofs) -> + print_builtin_vstore_global oc chunk id ofs args + | EF_memcpy(sz, al) -> + print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz)) + (Int32.to_int (camlint_of_coqint al)) args + | EF_annot_val(txt, targ) -> + print_annot_val oc (extern_atom txt) args res + | EF_inline_asm txt -> + fprintf oc "%s begin inline assembly\n" comment; + fprintf oc " %s\n" (extern_atom txt); + fprintf oc "%s end inline assembly\n" comment; + 5 (* hoping this is an upper bound... *) + | _ -> + assert false + end + | Pannot(ef, args) -> + begin match ef with + | EF_annot(txt, targs) -> + print_annot_stmt oc (extern_atom txt) targs args; 0 + | _ -> + assert false + end + + let no_fallthrough = function + | Pb _ -> true + | Pbsymb _ -> true + | Pbreg _ -> true + | _ -> false + + let rec print_instructions oc instrs = + match instrs with + | [] -> () + | i :: il -> + let n = print_instruction oc i in + currpos := !currpos + n * 4; + let d = distance_to_emit_constants() in + if d < 256 && no_fallthrough i then + emit_constants oc + else if d < 16 then begin + let lbl = new_label() in + fprintf oc " b .L%d\n" lbl; + emit_constants oc; + fprintf oc ".L%d:\n" lbl + end; + print_instructions oc il + + let get_section_names name = + let (text, lit) = + match C2C.atom_sections name with + | t :: l :: _ -> (t, l) + | _ -> (Section_text, Section_literal) in + text,lit,Section_jumptable + + let print_align oc alignment = + fprintf oc " .balign %d\n" alignment + + let print_jumptable _ _ = () + + let cfi_startproc = cfi_startproc + + let cfi_endproc = cfi_endproc + + let print_optional_fun_info oc = + if !Clflags.option_mthumb then + fprintf oc " .thumb_func\n" + + let print_fun_info = elf_print_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 + + let print_instructions oc fn = + ignore (fixup_arguments oc Incoming fn.fn_sig); + print_instructions oc fn.fn_code; + if !literals_in_code then emit_constants oc + + let emit_constants oc lit = + if not !literals_in_code && !size_constants > 0 then begin + section oc lit; + emit_constants oc + end + +(* Data *) + + let print_init oc = function + | Init_int8 n -> + fprintf oc " .byte %ld\n" (camlint_of_coqint n) + | Init_int16 n -> + fprintf oc " .short %ld\n" (camlint_of_coqint n) + | Init_int32 n -> + fprintf oc " .word %ld\n" (camlint_of_coqint n) + | Init_int64 n -> + fprintf oc " .quad %Ld\n" (camlint64_of_coqint n) + | Init_float32 n -> + fprintf oc " .word 0x%lx %s %.15g \n" (camlint_of_coqint (Floats.Float32.to_bits n)) + comment (camlfloat_of_coqfloat n) + | Init_float64 n -> + fprintf oc " .quad %Ld %s %.18g\n" (camlint64_of_coqint (Floats.Float.to_bits n)) + comment (camlfloat_of_coqfloat n) + | Init_space n -> + if Z.gt n Z.zero then + 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" + (match Configuration.model with + | "armv6" -> "armv6" + | "armv7a" -> "armv7-a" + | "armv7r" -> "armv7-r" + | "armv7m" -> "armv7-m" + | _ -> "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") + + let print_epilogue oc = () + + let default_falignment = 4 + end + +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 + | _ -> false + + end in + (module Target(S):TARGET) diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml new file mode 100644 index 00000000..a6883339 --- /dev/null +++ b/backend/PrintAsm.ml @@ -0,0 +1,101 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +open AST +open Asm +open Camlcoq +open Datatypes +open PrintAsmaux +open Printf +open Sections +open TargetPrinter + +module Printer(Target:TARGET) = + struct + + let print_location oc loc = + if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc) + + let print_function oc name fn = + Hashtbl.clear current_function_labels; + Target.reset_constants (); + let (text, lit, jmptbl) = Target.get_section_names name in + Target.section oc text; + let alignment = + match !Clflags.option_falignfunctions with Some n -> n | None -> Target.default_falignment in + Target.print_align oc alignment; + if not (C2C.atom_is_static name) then + fprintf oc " .globl %a\n" Target.symbol name; + Target.print_optional_fun_info oc; + fprintf oc "%a:\n" Target.symbol name; + print_location oc (C2C.atom_location name); + Target.cfi_startproc oc; + Target.print_instructions oc fn; + Target.cfi_endproc oc; + Target.print_fun_info oc name; + Target.emit_constants oc lit; + Target.print_jumptable oc jmptbl + + + let print_init_data oc name id = + if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0 + && List.for_all (function Init_int8 _ -> true | _ -> false) id + then + fprintf oc " .ascii \"%s\"\n" (PrintCsyntax.string_of_init id) + else + List.iter (Target.print_init oc) id + + let print_var oc name v = + match v.gvar_init with + | [] -> () + | _ -> + let sec = + match C2C.atom_sections name with + | [s] -> s + | _ -> Section_data true + and align = + match C2C.atom_alignof name with + | Some a -> a + | None -> 8 in (* 8-alignment is a safe default *) + let name_sec = Target.name_of_section sec in + if name_sec <> "COMM" then begin + fprintf oc " %s\n" name_sec; + Target.print_align oc align; + if not (C2C.atom_is_static name) then + fprintf oc " .global %a\n" Target.symbol name; + fprintf oc "%a:\n" Target.symbol name; + print_init_data oc name v.gvar_init; + Target.print_var_info oc name; + end else + let sz = + match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in + Target.print_comm_symb oc sz name align + + + let print_globdef oc (name,gdef) = + match gdef with + | Gfun (Internal code) -> print_function oc name code + | Gfun (External ef) -> () + | Gvar v -> print_var oc name v + + end + +let print_program oc p = + let module Target = (val (sel_target ()):TARGET) in + let module Printer = Printer(Target) in + PrintAnnot.reset_filenames (); + PrintAnnot.print_version_and_options oc Target.comment; + Target.print_prologue oc; + List.iter (Printer.print_globdef oc) p.prog_defs; + Target.print_epilogue oc; + PrintAnnot.close_filenames () diff --git a/powerpc/PrintAsm.mli b/backend/PrintAsm.mli index aefe3a0a..eb63f1be 100644 --- a/powerpc/PrintAsm.mli +++ b/backend/PrintAsm.mli @@ -3,6 +3,7 @@ (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -10,4 +11,6 @@ (* *) (* *********************************************************************) +open PrintAsmaux + val print_program: out_channel -> Asm.program -> unit diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml new file mode 100644 index 00000000..64db2cb0 --- /dev/null +++ b/backend/PrintAsmaux.ml @@ -0,0 +1,134 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +open AST +open Asm +open Camlcoq +open Datatypes +open Printf +open Sections + +(** Auxiliary functions for printing of asm *) + +module type TARGET = + sig + val print_prologue: out_channel -> unit + val print_epilogue: out_channel -> unit + val print_align: out_channel -> int -> unit + val print_comm_symb: out_channel -> Z.t -> P.t -> int -> unit + val print_var_info: out_channel -> P.t -> unit + val print_fun_info: out_channel -> P.t -> unit + val print_init: out_channel -> init_data -> unit + val reset_constants: unit -> unit + val get_section_names: P.t -> section_name * section_name * section_name + val print_file_line: out_channel -> string -> int -> unit + val print_optional_fun_info: out_channel -> unit + val cfi_startproc: out_channel -> unit + val print_instructions: out_channel -> coq_function -> unit + val cfi_endproc: out_channel -> unit + val emit_constants: out_channel -> section_name -> unit + val print_jumptable: out_channel -> section_name -> unit + val section: out_channel -> section_name -> unit + val name_of_section: section_name -> string + val comment: string + val symbol: out_channel -> P.t -> unit + val default_falignment: int + end + +(* On-the-fly label renaming *) + +let next_label = ref 100 + +let new_label () = + let lbl = !next_label in incr next_label; lbl + +let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t) + +let transl_label lbl = + try + Hashtbl.find current_function_labels lbl + with Not_found -> + let lbl' = new_label() in + Hashtbl.add current_function_labels lbl lbl'; + lbl' + +let elf_label oc lbl = + fprintf oc ".L%d" lbl + +(* List of literals and jumptables used in the code *) + +let float64_literals : (int * int64) list ref = ref [] +let float32_literals : (int * int32) list ref = ref [] +let jumptables : (int * label list) list ref = ref [] + +let reset_constants () = + float64_literals := []; + float32_literals := []; + jumptables := [] + +(* Variables used for the handling of varargs *) + +let current_function_stacksize = ref 0l +let current_function_sig = + ref { sig_args = []; sig_res = None; sig_cc = cc_default } + +(* Functions for printing of symbol names *) +let elf_symbol oc symb = + fprintf oc "%s" (extern_atom symb) + +let elf_symbol_offset oc (symb, ofs) = + elf_symbol oc symb; + let ofs = camlint_of_coqint ofs in + if ofs <> 0l then fprintf oc " + %ld" ofs + +(* Functions for fun and var info *) +let elf_print_fun_info oc name = + fprintf oc " .type %a, @function\n" elf_symbol name; + fprintf oc " .size %a, . - %a\n" elf_symbol name elf_symbol name + +let elf_print_var_info oc name = + fprintf oc " .type %a, @object\n" elf_symbol name; + fprintf oc " .size %a, . - %a\n" elf_symbol name elf_symbol name + +(* Emit .cfi directives *) +let cfi_startproc = + if Configuration.asm_supports_cfi then + (fun oc -> fprintf oc " .cfi_startproc\n") + else + (fun _ -> ()) + +let cfi_endproc = + if Configuration.asm_supports_cfi then + (fun oc -> fprintf oc " .cfi_endproc\n") + else + (fun _ -> ()) + + +let cfi_adjust = + if Configuration.asm_supports_cfi then + (fun oc delta -> fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta) + else + (fun _ _ -> ()) + +let cfi_rel_offset = + if Configuration.asm_supports_cfi then + (fun oc reg ofs -> fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs) + else + (fun _ _ _ -> ()) + +(* For handling of annotations *) +let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" + +(* Basic printing functions *) +let coqint oc n = + fprintf oc "%ld" (camlint_of_coqint n) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 0ccf569b..2b9a54a4 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -365,8 +365,10 @@ a constant)"; Integers.Int.zero in | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be a constant)"; Integers.Int.one in (* to check: sz1 > 0, al1 divides sz1, al1 = 1|2|4|8 *) + (* Issue #28: must decay array types to pointer types *) Ebuiltin(EF_memcpy(sz1, al1), - Tcons(typeof dst, Tcons(typeof src, Tnil)), + Tcons(typeconv(typeof dst), + Tcons(typeconv(typeof src), Tnil)), Econs(dst, Econs(src, Enil)), Tvoid) | _ -> assert false diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml deleted file mode 100644 index 0ca51173..00000000 --- a/ia32/PrintAsm.ml +++ /dev/null @@ -1,1067 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Printing IA32 assembly code in asm syntax *) - -open Printf -open Datatypes -open Camlcoq -open Sections -open AST -open Memdata -open Asm - -module StringSet = Set.Make(String) - -(* Basic printing functions used in definition of the systems *) - -let int_reg_name = function - | EAX -> "%eax" | EBX -> "%ebx" | ECX -> "%ecx" | EDX -> "%edx" - | ESI -> "%esi" | EDI -> "%edi" | EBP -> "%ebp" | ESP -> "%esp" - -let int8_reg_name = function - | EAX -> "%al" | EBX -> "%bl" | ECX -> "%cl" | EDX -> "%dl" - | _ -> assert false - -let high_int8_reg_name = function - | EAX -> "%ah" | EBX -> "%bh" | ECX -> "%ch" | EDX -> "%dh" - | _ -> assert false - -let int16_reg_name = function - | EAX -> "%ax" | EBX -> "%bx" | ECX -> "%cx" | EDX -> "%dx" - | ESI -> "%si" | EDI -> "%di" | EBP -> "%bp" | ESP -> "%sp" - -let float_reg_name = function - | XMM0 -> "%xmm0" | XMM1 -> "%xmm1" | XMM2 -> "%xmm2" | XMM3 -> "%xmm3" - | XMM4 -> "%xmm4" | XMM5 -> "%xmm5" | XMM6 -> "%xmm6" | XMM7 -> "%xmm7" - -let ireg oc r = output_string oc (int_reg_name r) -let ireg8 oc r = output_string oc (int8_reg_name r) -let high_ireg8 oc r = output_string oc (high_int8_reg_name r) -let ireg16 oc r = output_string oc (int16_reg_name r) -let freg oc r = output_string oc (float_reg_name r) - -let preg oc = function - | IR r -> ireg oc r - | FR r -> freg oc r - | _ -> assert false - - -(* System dependend printer functions *) -module type SYSTEM = - sig - val raw_symbol: out_channel -> string -> unit - val symbol: out_channel -> P.t -> unit - val label: out_channel -> int -> unit - val name_of_section: section_name -> string - val stack_alignment: int - val print_align: out_channel -> int -> unit - val print_mov_ra: out_channel -> ireg -> ident -> unit - val print_fun_info: out_channel -> P.t -> unit - val print_var_info: out_channel -> P.t -> unit - val print_epilogue: out_channel -> 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 - -(* Printer functions for cygwin *) -module Cygwin_System = - (struct - - let raw_symbol oc s = - fprintf oc "_%s" s - - let symbol oc symb = - raw_symbol oc (extern_atom symb) - - let label oc lbl = - fprintf oc "L%d" lbl - - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else "COMM" - | Section_const i | Section_small_const i -> - if i then ".section .rdata,\"dr\"" else "COMM" - | Section_string -> ".section .rdata,\"dr\"" - | Section_literal -> ".section .rdata,\"dr\"" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\", \"%s\"\n" - s (if ex then "xr" else if wr then "d" else "dr") - - let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) - - let print_align oc n = - fprintf oc " .align %d\n" n - - let print_mov_ra oc rd id = - fprintf oc " movl $%a, %a\n" symbol id ireg rd - - let print_fun_info _ _ = () - - let print_var_info _ _ = () - - let print_epilogue _ = () - - 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:SYSTEM) - -(* Printer functions for ELF *) -module ELF_System = - (struct - - let raw_symbol oc s = - fprintf oc "%s" s - - let symbol oc symb = - raw_symbol oc (extern_atom symb) - - let label oc lbl = - fprintf oc ".L%d" lbl - - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else "COMM" - | Section_const i | Section_small_const i -> - if i then ".section .rodata" else "COMM" - | Section_string -> ".section .rodata" - | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\",\"a%s%s\",@progbits" - s (if wr then "w" else "") (if ex then "x" else "") - - let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) - - let print_align oc n = - fprintf oc " .align %d\n" n - - let print_mov_ra oc rd id = - fprintf oc " movl $%a, %a\n" symbol id ireg rd - - let print_fun_info oc name = - fprintf oc " .type %a, @function\n" symbol name; - fprintf oc " .size %a, . - %a\n" symbol name symbol name - - let print_var_info oc name = - fprintf oc " .type %a, @object\n" symbol name; - fprintf oc " .size %a, . - %a\n" symbol name symbol name - - let print_epilogue _ = () - - 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:SYSTEM) - -(* Printer functions for MacOS *) -module MacOS_System = - (struct - - let raw_symbol oc s = - fprintf oc "_%s" s - - let symbol oc symb = - raw_symbol oc (extern_atom symb) - - let label oc lbl = - fprintf oc "L%d" lbl - - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else "COMM" - | Section_const i | Section_small_const i -> - if i then ".const" else "COMM" - | Section_string -> ".const" - | Section_literal -> ".literal8" - | Section_jumptable -> ".const" - | 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") - - let stack_alignment = 16 (* mandatory *) - - (* 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) - - let print_align oc n = - fprintf oc " .align %d\n" (log2 n) - - let indirect_symbols : StringSet.t ref = ref StringSet.empty - - let print_mov_ra oc rd id = - let id = extern_atom id in - indirect_symbols := StringSet.add id !indirect_symbols; - fprintf oc " movl L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd - - let print_fun_info _ _ = () - - let print_var_info _ _ = () - - let print_epilogue oc = - fprintf oc " .section __IMPORT,__pointers,non_lazy_symbol_pointers\n"; - StringSet.iter - (fun s -> - fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s; - fprintf oc " .indirect_symbol %a\n" raw_symbol s; - fprintf oc " .long 0\n") - !indirect_symbols; - indirect_symbols := StringSet.empty - - 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:SYSTEM) - - -module AsmPrinter(Target: SYSTEM) = - (struct - open Target -(* On-the-fly label renaming *) - -let next_label = ref 100 - -let new_label() = - let lbl = !next_label in incr next_label; lbl - -let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t) - -let transl_label lbl = - try - Hashtbl.find current_function_labels lbl - with Not_found -> - let lbl' = new_label() in - Hashtbl.add current_function_labels lbl lbl'; - lbl' - -(* Basic printing functions *) - -let comment = "#" - -let symbol_offset oc (symb, ofs) = - symbol oc symb; - if ofs <> 0l then fprintf oc " + %ld" ofs - -let coqint oc n = - fprintf oc "%ld" (camlint_of_coqint n) - -let addressing oc (Addrmode(base, shift, cst)) = - begin match cst with - | Coq_inl n -> - let n = camlint_of_coqint n in - fprintf oc "%ld" n - | Coq_inr(id, ofs) -> - let ofs = camlint_of_coqint ofs in - if ofs = 0l - then symbol oc id - else fprintf oc "(%a + %ld)" symbol id ofs - end; - begin match base, shift with - | None, None -> () - | Some r1, None -> fprintf oc "(%a)" ireg r1 - | None, Some(r2,sc) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc - | Some r1, Some(r2,sc) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 coqint sc - end - -let name_of_condition = function - | Cond_e -> "e" | Cond_ne -> "ne" - | Cond_b -> "b" | Cond_be -> "be" | Cond_ae -> "ae" | Cond_a -> "a" - | Cond_l -> "l" | Cond_le -> "le" | Cond_ge -> "ge" | Cond_g -> "g" - | Cond_p -> "p" | Cond_np -> "np" - -let name_of_neg_condition = function - | Cond_e -> "ne" | Cond_ne -> "e" - | Cond_b -> "ae" | Cond_be -> "a" | Cond_ae -> "b" | Cond_a -> "be" - | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le" - | Cond_p -> "np" | Cond_np -> "p" - - -(* Names of sections *) - -let section oc sec = - fprintf oc " %s\n" (name_of_section sec) - -(* SP adjustment to allocate or free a stack frame *) - -let int32_align n a = - if n >= 0l - then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a)) - else Int32.logand n (Int32.of_int (-a)) - -let sp_adjustment sz = - let sz = camlint_of_coqint sz in - (* Preserve proper alignment of the stack *) - let sz = int32_align sz stack_alignment in - (* The top 4 bytes have already been allocated by the "call" instruction. *) - let sz = Int32.sub sz 4l in - sz - -(* 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) - -(* Emit a align directive *) - -let need_masks = ref false - -(* Emit .file / .loc debugging directives *) - -let print_file_line oc file line = - PrintAnnot.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) - -(* Emit .cfi directives *) - -let cfi_startproc oc = - if Configuration.asm_supports_cfi then fprintf oc " .cfi_startproc\n" - -let cfi_endproc oc = - if Configuration.asm_supports_cfi then fprintf oc " .cfi_endproc\n" - -let cfi_adjust oc delta = - if Configuration.asm_supports_cfi then - fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta - -(* Built-in functions *) - -(* Built-ins. They come in two flavors: - - annotation statements: take their arguments in registers or stack - locations; generate no code; - - inlined by the compiler: take their arguments in arbitrary - registers; preserve all registers except ECX, EDX, XMM6 and XMM7. *) - -(* Handling of annotations *) - -let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" - -let print_annot_stmt oc txt targs args = - if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) - (int_of_string (Str.matched_group 2 txt)) - end else begin - fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args - end - -let print_annot_val oc txt args res = - fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_val preg oc txt args; - match args, res with - | [IR src], [IR dst] -> - if dst <> src then fprintf oc " movl %a, %a\n" ireg src ireg dst - | [FR src], [FR dst] -> - if dst <> src then fprintf oc " movapd %a, %a\n" freg src freg dst - | _, _ -> assert false - -(* Handling of memcpy *) - -(* Unaligned memory accesses are quite fast on IA32, so use large - memory accesses regardless of alignment. *) - -let print_builtin_memcpy_small oc sz al src dst = - assert (src = EDX && dst = EAX); - let rec copy ofs sz = - if sz >= 8 && !Clflags.option_ffpu then begin - fprintf oc " movq %d(%a), %a\n" ofs ireg src freg XMM7; - fprintf oc " movq %a, %d(%a)\n" freg XMM7 ofs ireg dst; - copy (ofs + 8) (sz - 8) - end else if sz >= 4 then begin - fprintf oc " movl %d(%a), %a\n" ofs ireg src ireg ECX; - fprintf oc " movl %a, %d(%a)\n" ireg ECX ofs ireg dst; - copy (ofs + 4) (sz - 4) - end else if sz >= 2 then begin - fprintf oc " movw %d(%a), %a\n" ofs ireg src ireg16 ECX; - fprintf oc " movw %a, %d(%a)\n" ireg16 ECX ofs ireg dst; - copy (ofs + 2) (sz - 2) - end else if sz >= 1 then begin - fprintf oc " movb %d(%a), %a\n" ofs ireg src ireg8 ECX; - fprintf oc " movb %a, %d(%a)\n" ireg8 ECX ofs ireg dst; - copy (ofs + 1) (sz - 1) - end in - copy 0 sz - -let print_builtin_memcpy_big oc sz al src dst = - assert (src = ESI && dst = EDI); - fprintf oc " movl $%d, %a\n" (sz / 4) ireg ECX; - fprintf oc " rep movsl\n"; - if sz mod 4 >= 2 then fprintf oc " movsw\n"; - if sz mod 2 >= 1 then fprintf oc " movsb\n" - -let print_builtin_memcpy oc sz al args = - let (dst, src) = - match args with [IR d; IR s] -> (d, s) | _ -> assert false in - fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n" - comment sz al; - if sz <= 32 - then print_builtin_memcpy_small oc sz al src dst - else print_builtin_memcpy_big oc sz al src dst; - fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment - -(* Handling of volatile reads and writes *) - -let offset_addressing (Addrmode(base, ofs, cst)) delta = - Addrmode(base, ofs, - match cst with - | Coq_inl n -> Coq_inl(Integers.Int.add n delta) - | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta)) - -let print_builtin_vload_common oc chunk addr res = - match chunk, res with - | Mint8unsigned, [IR res] -> - fprintf oc " movzbl %a, %a\n" addressing addr ireg res - | Mint8signed, [IR res] -> - fprintf oc " movsbl %a, %a\n" addressing addr ireg res - | Mint16unsigned, [IR res] -> - fprintf oc " movzwl %a, %a\n" addressing addr ireg res - | Mint16signed, [IR res] -> - fprintf oc " movswl %a, %a\n" addressing addr ireg res - | Mint32, [IR res] -> - fprintf oc " movl %a, %a\n" addressing addr ireg res - | Mint64, [IR res1; IR res2] -> - let addr' = offset_addressing addr (coqint_of_camlint 4l) in - if not (Asmgen.addressing_mentions addr res2) then begin - fprintf oc " movl %a, %a\n" addressing addr ireg res2; - fprintf oc " movl %a, %a\n" addressing addr' ireg res1 - end else begin - fprintf oc " movl %a, %a\n" addressing addr' ireg res1; - fprintf oc " movl %a, %a\n" addressing addr ireg res2 - end - | Mfloat32, [FR res] -> - fprintf oc " movss %a, %a\n" addressing addr freg res - | Mfloat64, [FR res] -> - fprintf oc " movsd %a, %a\n" addressing addr freg res - | _ -> - assert false - -let print_builtin_vload oc chunk args res = - fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; - begin match args with - | [IR addr] -> - print_builtin_vload_common oc chunk - (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) res - | _ -> - assert false - end; - fprintf oc "%s end builtin __builtin_volatile_read\n" comment - -let print_builtin_vload_global oc chunk id ofs args res = - fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; - print_builtin_vload_common oc chunk - (Addrmode(None, None, Coq_inr(id,ofs))) res; - fprintf oc "%s end builtin __builtin_volatile_read\n" comment - -let print_builtin_vstore_common oc chunk addr src tmp = - match chunk, src with - | (Mint8signed | Mint8unsigned), [IR src] -> - if Asmgen.low_ireg src then - fprintf oc " movb %a, %a\n" ireg8 src addressing addr - else begin - fprintf oc " movl %a, %a\n" ireg src ireg tmp; - fprintf oc " movb %a, %a\n" ireg8 tmp addressing addr - end - | (Mint16signed | Mint16unsigned), [IR src] -> - fprintf oc " movw %a, %a\n" ireg16 src addressing addr - | Mint32, [IR src] -> - fprintf oc " movl %a, %a\n" ireg src addressing addr - | Mint64, [IR src1; IR src2] -> - let addr' = offset_addressing addr (coqint_of_camlint 4l) in - fprintf oc " movl %a, %a\n" ireg src2 addressing addr; - fprintf oc " movl %a, %a\n" ireg src1 addressing addr' - | Mfloat32, [FR src] -> - fprintf oc " movss %a, %a\n" freg src addressing addr - | Mfloat64, [FR src] -> - fprintf oc " movsd %a, %a\n" freg src addressing addr - | _ -> - assert false - -let print_builtin_vstore oc chunk args = - fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; - begin match args with - | IR addr :: src -> - print_builtin_vstore_common oc chunk - (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src - (if addr = EAX then ECX else EAX) - | _ -> - assert false - end; - fprintf oc "%s end builtin __builtin_volatile_write\n" comment - -let print_builtin_vstore_global oc chunk id ofs args = - fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; - print_builtin_vstore_common oc chunk - (Addrmode(None, None, Coq_inr(id,ofs))) args EAX; - fprintf oc "%s end builtin __builtin_volatile_write\n" comment - -(* Handling of varargs *) - -let current_function_stacksize = ref 0l -let current_function_sig = - ref { sig_args = []; sig_res = None; sig_cc = cc_default } - -let print_builtin_va_start oc r = - if not (!current_function_sig).sig_cc.cc_vararg then - invalid_arg "Fatal error: va_start used in non-vararg function"; - let ofs = - Int32.(add (add !current_function_stacksize 4l) - (mul 4l (Z.to_int32 (Conventions1.size_arguments - !current_function_sig)))) in - fprintf oc " movl %%esp, 0(%a)\n" ireg r; - fprintf oc " addl $%ld, 0(%a)\n" ofs ireg r - -(* Handling of compiler-inlined builtins *) - -let print_builtin_inline oc name args res = - fprintf oc "%s begin builtin %s\n" comment name; - begin match name, args, res with - (* Integer arithmetic *) - | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] -> - if a1 <> res then - fprintf oc " movl %a, %a\n" ireg a1 ireg res; - fprintf oc " bswap %a\n" ireg res - | "__builtin_bswap16", [IR a1], [IR res] -> - if a1 <> res then - fprintf oc " movl %a, %a\n" ireg a1 ireg res; - fprintf oc " rolw $8, %a\n" ireg16 res - | "__builtin_clz", [IR a1], [IR res] -> - fprintf oc " bsrl %a, %a\n" ireg a1 ireg res; - fprintf oc " xorl $31, %a\n" ireg res - | "__builtin_ctz", [IR a1], [IR res] -> - fprintf oc " bsfl %a, %a\n" ireg a1 ireg res - (* Float arithmetic *) - | "__builtin_fabs", [FR a1], [FR res] -> - need_masks := true; - if a1 <> res then - fprintf oc " movapd %a, %a\n" freg a1 freg res; - fprintf oc " andpd %a, %a\n" raw_symbol "__absd_mask" freg res - | "__builtin_fsqrt", [FR a1], [FR res] -> - fprintf oc " sqrtsd %a, %a\n" freg a1 freg res - | "__builtin_fmax", [FR a1; FR a2], [FR res] -> - if res = a1 then - fprintf oc " maxsd %a, %a\n" freg a2 freg res - else if res = a2 then - fprintf oc " maxsd %a, %a\n" freg a1 freg res - else begin - fprintf oc " movapd %a, %a\n" freg a1 freg res; - fprintf oc " maxsd %a, %a\n" freg a2 freg res - end - | "__builtin_fmin", [FR a1; FR a2], [FR res] -> - if res = a1 then - fprintf oc " minsd %a, %a\n" freg a2 freg res - else if res = a2 then - fprintf oc " minsd %a, %a\n" freg a1 freg res - else begin - fprintf oc " movapd %a, %a\n" freg a1 freg res; - fprintf oc " minsd %a, %a\n" freg a2 freg res - end - | ("__builtin_fmadd"|"__builtin_fmsub"|"__builtin_fnmadd"|"__builtin_fnmsub"), - [FR a1; FR a2; FR a3], [FR res] -> - let opcode = - match name with - | "__builtin_fmadd" -> "vfmadd" - | "__builtin_fmsub" -> "vfmsub" - | "__builtin_fnmadd" -> "vfnmadd" - | "__builtin_fnmsub" -> "vfnmsub" - | _ -> assert false in - if res = a1 then - fprintf oc " %s132sd %a, %a, %a\n" opcode freg a2 freg a3 freg res - else if res = a2 then - fprintf oc " %s213sd %a, %a, %a\n" opcode freg a3 freg a1 freg res - else if res = a3 then - fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res - else begin - fprintf oc " movapd %a, %a\n" freg a3 freg res; - fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res - end - (* 64-bit integer arithmetic *) - | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> - assert (ah = EDX && al = EAX && rh = EDX && rl = EAX); - fprintf oc " negl %a\n" ireg EAX; - fprintf oc " adcl $0, %a\n" ireg EDX; - fprintf oc " negl %a\n" ireg EDX - | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); - fprintf oc " addl %a, %a\n" ireg EBX ireg EAX; - fprintf oc " adcl %a, %a\n" ireg ECX ireg EDX - | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); - fprintf oc " subl %a, %a\n" ireg EBX ireg EAX; - fprintf oc " sbbl %a, %a\n" ireg ECX ireg EDX - | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> - assert (a = EAX && b = EDX && rh = EDX && rl = EAX); - fprintf oc " mull %a\n" ireg EDX - (* Memory accesses *) - | "__builtin_read16_reversed", [IR a1], [IR res] -> - fprintf oc " movzwl 0(%a), %a\n" ireg a1 ireg res; - fprintf oc " rolw $8, %a\n" ireg16 res - | "__builtin_read32_reversed", [IR a1], [IR res] -> - fprintf oc " movl 0(%a), %a\n" ireg a1 ireg res; - fprintf oc " bswap %a\n" ireg res - | "__builtin_write16_reversed", [IR a1; IR a2], _ -> - let tmp = if a1 = ECX then EDX else ECX in - if a2 <> tmp then - fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; - fprintf oc " xchg %a, %a\n" ireg8 tmp high_ireg8 tmp; - fprintf oc " movw %a, 0(%a)\n" ireg16 tmp ireg a1 - | "__builtin_write32_reversed", [IR a1; IR a2], _ -> - let tmp = if a1 = ECX then EDX else ECX in - if a2 <> tmp then - fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; - fprintf oc " bswap %a\n" ireg tmp; - fprintf oc " movl %a, 0(%a)\n" ireg tmp ireg a1 - (* Synchronization *) - | "__builtin_membar", [], _ -> - () - (* Vararg stuff *) - | "__builtin_va_start", [IR a], _ -> - print_builtin_va_start oc a - (* Catch-all *) - | _ -> - invalid_arg ("unrecognized builtin " ^ name) - end; - fprintf oc "%s end builtin %s\n" comment name - -(* Printing of instructions *) - -let float64_literals : (int * int64) list ref = ref [] -let float32_literals : (int * int32) list ref = ref [] -let jumptables : (int * label list) list ref = ref [] - -(* Reminder on AT&T syntax: op source, dest *) - -let print_instruction oc = function - (* Moves *) - | Pmov_rr(rd, r1) -> - fprintf oc " movl %a, %a\n" ireg r1 ireg rd - | Pmov_ri(rd, n) -> - fprintf oc " movl $%ld, %a\n" (camlint_of_coqint n) ireg rd - | Pmov_ra(rd, id) -> - print_mov_ra oc rd id - | Pmov_rm(rd, a) | Pmov_rm_a(rd, a) -> - fprintf oc " movl %a, %a\n" addressing a ireg rd - | Pmov_mr(a, r1) | Pmov_mr_a(a, r1) -> - fprintf oc " movl %a, %a\n" ireg r1 addressing a - | Pmovsd_ff(rd, r1) -> - fprintf oc " movapd %a, %a\n" freg r1 freg rd - | Pmovsd_fi(rd, n) -> - let b = camlint64_of_coqint (Floats.Float.to_bits n) in - let lbl = new_label() in - fprintf oc " movsd %a, %a %s %.18g\n" label lbl freg rd comment (camlfloat_of_coqfloat n); - float64_literals := (lbl, b) :: !float64_literals - | Pmovsd_fm(rd, a) | Pmovsd_fm_a(rd, a) -> - fprintf oc " movsd %a, %a\n" addressing a freg rd - | Pmovsd_mf(a, r1) | Pmovsd_mf_a(a, r1) -> - fprintf oc " movsd %a, %a\n" freg r1 addressing a - | Pmovss_fi(rd, n) -> - let b = camlint_of_coqint (Floats.Float32.to_bits n) in - let lbl = new_label() in - fprintf oc " movss %a, %a %s %.18g\n" label lbl freg rd comment (camlfloat_of_coqfloat32 n); - float32_literals := (lbl, b) :: !float32_literals - | Pmovss_fm(rd, a) -> - fprintf oc " movss %a, %a\n" addressing a freg rd - | Pmovss_mf(a, r1) -> - fprintf oc " movss %a, %a\n" freg r1 addressing a - | Pfldl_m(a) -> - fprintf oc " fldl %a\n" addressing a - | Pfstpl_m(a) -> - fprintf oc " fstpl %a\n" addressing a - | Pflds_m(a) -> - fprintf oc " flds %a\n" addressing a - | Pfstps_m(a) -> - fprintf oc " fstps %a\n" addressing a - | Pxchg_rr(r1, r2) -> - fprintf oc " xchgl %a, %a\n" ireg r1 ireg r2 - (** Moves with conversion *) - | Pmovb_mr(a, r1) -> - fprintf oc " movb %a, %a\n" ireg8 r1 addressing a - | Pmovw_mr(a, r1) -> - fprintf oc " movw %a, %a\n" ireg16 r1 addressing a - | Pmovzb_rr(rd, r1) -> - fprintf oc " movzbl %a, %a\n" ireg8 r1 ireg rd - | Pmovzb_rm(rd, a) -> - fprintf oc " movzbl %a, %a\n" addressing a ireg rd - | Pmovsb_rr(rd, r1) -> - fprintf oc " movsbl %a, %a\n" ireg8 r1 ireg rd - | Pmovsb_rm(rd, a) -> - fprintf oc " movsbl %a, %a\n" addressing a ireg rd - | Pmovzw_rr(rd, r1) -> - fprintf oc " movzwl %a, %a\n" ireg16 r1 ireg rd - | Pmovzw_rm(rd, a) -> - fprintf oc " movzwl %a, %a\n" addressing a ireg rd - | Pmovsw_rr(rd, r1) -> - fprintf oc " movswl %a, %a\n" ireg16 r1 ireg rd - | Pmovsw_rm(rd, a) -> - fprintf oc " movswl %a, %a\n" addressing a ireg rd - | Pcvtsd2ss_ff(rd, r1) -> - fprintf oc " cvtsd2ss %a, %a\n" freg r1 freg rd - | Pcvtss2sd_ff(rd, r1) -> - fprintf oc " cvtss2sd %a, %a\n" freg r1 freg rd - | Pcvttsd2si_rf(rd, r1) -> - fprintf oc " cvttsd2si %a, %a\n" freg r1 ireg rd - | Pcvtsi2sd_fr(rd, r1) -> - fprintf oc " cvtsi2sd %a, %a\n" ireg r1 freg rd - | Pcvttss2si_rf(rd, r1) -> - fprintf oc " cvttss2si %a, %a\n" freg r1 ireg rd - | Pcvtsi2ss_fr(rd, r1) -> - fprintf oc " cvtsi2ss %a, %a\n" ireg r1 freg rd - (** Arithmetic and logical operations over integers *) - | Plea(rd, a) -> - fprintf oc " leal %a, %a\n" addressing a ireg rd - | Pneg(rd) -> - fprintf oc " negl %a\n" ireg rd - | Psub_rr(rd, r1) -> - fprintf oc " subl %a, %a\n" ireg r1 ireg rd - | Pimul_rr(rd, r1) -> - fprintf oc " imull %a, %a\n" ireg r1 ireg rd - | Pimul_ri(rd, n) -> - fprintf oc " imull $%a, %a\n" coqint n ireg rd - | Pimul_r(r1) -> - fprintf oc " imull %a\n" ireg r1 - | Pmul_r(r1) -> - fprintf oc " mull %a\n" ireg r1 - | Pdiv(r1) -> - fprintf oc " xorl %%edx, %%edx\n"; - fprintf oc " divl %a\n" ireg r1 - | Pidiv(r1) -> - fprintf oc " cltd\n"; - fprintf oc " idivl %a\n" ireg r1 - | Pand_rr(rd, r1) -> - fprintf oc " andl %a, %a\n" ireg r1 ireg rd - | Pand_ri(rd, n) -> - fprintf oc " andl $%a, %a\n" coqint n ireg rd - | Por_rr(rd, r1) -> - fprintf oc " orl %a, %a\n" ireg r1 ireg rd - | Por_ri(rd, n) -> - fprintf oc " orl $%a, %a\n" coqint n ireg rd - | Pxor_r(rd) -> - fprintf oc " xorl %a, %a\n" ireg rd ireg rd - | Pxor_rr(rd, r1) -> - fprintf oc " xorl %a, %a\n" ireg r1 ireg rd - | Pxor_ri(rd, n) -> - fprintf oc " xorl $%a, %a\n" coqint n ireg rd - | Pnot(rd) -> - fprintf oc " notl %a\n" ireg rd - | Psal_rcl(rd) -> - fprintf oc " sall %%cl, %a\n" ireg rd - | Psal_ri(rd, n) -> - fprintf oc " sall $%a, %a\n" coqint n ireg rd - | Pshr_rcl(rd) -> - fprintf oc " shrl %%cl, %a\n" ireg rd - | Pshr_ri(rd, n) -> - fprintf oc " shrl $%a, %a\n" coqint n ireg rd - | Psar_rcl(rd) -> - fprintf oc " sarl %%cl, %a\n" ireg rd - | Psar_ri(rd, n) -> - fprintf oc " sarl $%a, %a\n" coqint n ireg rd - | Pshld_ri(rd, r1, n) -> - fprintf oc " shldl $%a, %a, %a\n" coqint n ireg r1 ireg rd - | Pror_ri(rd, n) -> - fprintf oc " rorl $%a, %a\n" coqint n ireg rd - | Pcmp_rr(r1, r2) -> - fprintf oc " cmpl %a, %a\n" ireg r2 ireg r1 - | Pcmp_ri(r1, n) -> - fprintf oc " cmpl $%a, %a\n" coqint n ireg r1 - | Ptest_rr(r1, r2) -> - fprintf oc " testl %a, %a\n" ireg r2 ireg r1 - | Ptest_ri(r1, n) -> - fprintf oc " testl $%a, %a\n" coqint n ireg r1 - | Pcmov(c, rd, r1) -> - fprintf oc " cmov%s %a, %a\n" (name_of_condition c) ireg r1 ireg rd - | Psetcc(c, rd) -> - fprintf oc " set%s %a\n" (name_of_condition c) ireg8 rd; - fprintf oc " movzbl %a, %a\n" ireg8 rd ireg rd - (** Arithmetic operations over floats *) - | Paddd_ff(rd, r1) -> - fprintf oc " addsd %a, %a\n" freg r1 freg rd - | Psubd_ff(rd, r1) -> - fprintf oc " subsd %a, %a\n" freg r1 freg rd - | Pmuld_ff(rd, r1) -> - fprintf oc " mulsd %a, %a\n" freg r1 freg rd - | Pdivd_ff(rd, r1) -> - fprintf oc " divsd %a, %a\n" freg r1 freg rd - | Pnegd (rd) -> - need_masks := true; - fprintf oc " xorpd %a, %a\n" raw_symbol "__negd_mask" freg rd - | Pabsd (rd) -> - need_masks := true; - fprintf oc " andpd %a, %a\n" raw_symbol "__absd_mask" freg rd - | Pcomisd_ff(r1, r2) -> - fprintf oc " comisd %a, %a\n" freg r2 freg r1 - | Pxorpd_f (rd) -> - fprintf oc " xorpd %a, %a\n" freg rd freg rd - | Padds_ff(rd, r1) -> - fprintf oc " addss %a, %a\n" freg r1 freg rd - | Psubs_ff(rd, r1) -> - fprintf oc " subss %a, %a\n" freg r1 freg rd - | Pmuls_ff(rd, r1) -> - fprintf oc " mulss %a, %a\n" freg r1 freg rd - | Pdivs_ff(rd, r1) -> - fprintf oc " divss %a, %a\n" freg r1 freg rd - | Pnegs (rd) -> - need_masks := true; - fprintf oc " xorpd %a, %a\n" raw_symbol "__negs_mask" freg rd - | Pabss (rd) -> - need_masks := true; - fprintf oc " andpd %a, %a\n" raw_symbol "__abss_mask" freg rd - | Pcomiss_ff(r1, r2) -> - fprintf oc " comiss %a, %a\n" freg r2 freg r1 - | Pxorps_f (rd) -> - fprintf oc " xorpd %a, %a\n" freg rd freg rd - (** Branches and calls *) - | Pjmp_l(l) -> - fprintf oc " jmp %a\n" label (transl_label l) - | Pjmp_s(f, sg) -> - assert (not sg.sig_cc.cc_structret); - fprintf oc " jmp %a\n" symbol f - | Pjmp_r(r, sg) -> - assert (not sg.sig_cc.cc_structret); - fprintf oc " jmp *%a\n" ireg r - | Pjcc(c, l) -> - let l = transl_label l in - fprintf oc " j%s %a\n" (name_of_condition c) label l - | Pjcc2(c1, c2, l) -> - let l = transl_label l in - let l' = new_label() in - fprintf oc " j%s %a\n" (name_of_neg_condition c1) label l'; - fprintf oc " j%s %a\n" (name_of_condition c2) label l; - fprintf oc "%a:\n" label l' - | Pjmptbl(r, tbl) -> - let l = new_label() in - fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r; - jumptables := (l, tbl) :: !jumptables - | Pcall_s(f, sg) -> - fprintf oc " call %a\n" symbol f; - if sg.sig_cc.cc_structret then - fprintf oc " pushl %%eax\n" - | Pcall_r(r, sg) -> - fprintf oc " call *%a\n" ireg r; - if sg.sig_cc.cc_structret then - fprintf oc " pushl %%eax\n" - | Pret -> - if (!current_function_sig).sig_cc.cc_structret then begin - fprintf oc " movl 0(%%esp), %%eax\n"; - fprintf oc " ret $4\n" - end else begin - fprintf oc " ret\n" - end - (** Pseudo-instructions *) - | Plabel(l) -> - fprintf oc "%a:\n" label (transl_label l) - | Pallocframe(sz, ofs_ra, ofs_link) -> - let sz = sp_adjustment sz in - let ofs_link = camlint_of_coqint ofs_link in - fprintf oc " subl $%ld, %%esp\n" sz; - cfi_adjust oc sz; - fprintf oc " leal %ld(%%esp), %%edx\n" (Int32.add sz 4l); - fprintf oc " movl %%edx, %ld(%%esp)\n" ofs_link; - current_function_stacksize := sz - | Pfreeframe(sz, ofs_ra, ofs_link) -> - let sz = sp_adjustment sz in - fprintf oc " addl $%ld, %%esp\n" sz - | Pbuiltin(ef, args, res) -> - begin match ef with - | EF_builtin(name, sg) -> - print_builtin_inline oc (extern_atom name) args res - | EF_vload chunk -> - print_builtin_vload oc chunk args res - | EF_vstore chunk -> - print_builtin_vstore oc chunk args - | EF_vload_global(chunk, id, ofs) -> - print_builtin_vload_global oc chunk id ofs args res - | EF_vstore_global(chunk, id, ofs) -> - print_builtin_vstore_global oc chunk id ofs args - | EF_memcpy(sz, al) -> - print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz)) - (Int32.to_int (camlint_of_coqint al)) args - | EF_annot_val(txt, targ) -> - print_annot_val oc (extern_atom txt) args res - | EF_inline_asm txt -> - fprintf oc "%s begin inline assembly\n" comment; - fprintf oc " %s\n" (extern_atom txt); - fprintf oc "%s end inline assembly\n" comment - | _ -> - assert false - end - | Pannot(ef, args) -> - begin match ef with - | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) targs args - | _ -> - assert false - end - -let print_literal64 oc (lbl, n) = - fprintf oc "%a: .quad 0x%Lx\n" label lbl n -let print_literal32 oc (lbl, n) = - fprintf oc "%a: .long 0x%lx\n" label lbl n - -let print_jumptable oc (lbl, tbl) = - fprintf oc "%a:" label lbl; - List.iter - (fun l -> fprintf oc " .long %a\n" label (transl_label l)) - tbl - -let print_function oc name fn = - Hashtbl.clear current_function_labels; - float64_literals := []; float32_literals := []; - jumptables := []; - current_function_sig := fn.fn_sig; - let (text, lit, jmptbl) = - match C2C.atom_sections name with - | [t;l;j] -> (t, l, j) - | _ -> (Section_text, Section_literal, Section_jumptable) in - section oc text; - let alignment = - match !Clflags.option_falignfunctions with Some n -> n | None -> 16 in - print_align oc alignment; - if not (C2C.atom_is_static name) then - fprintf oc " .globl %a\n" symbol name; - fprintf oc "%a:\n" symbol name; - print_location oc (C2C.atom_location name); - cfi_startproc oc; - List.iter (print_instruction oc) fn.fn_code; - cfi_endproc oc; - print_fun_info oc name; - if !float64_literals <> [] || !float32_literals <> [] then begin - section oc lit; - print_align oc 8; - List.iter (print_literal64 oc) !float64_literals; - float64_literals := []; - List.iter (print_literal32 oc) !float32_literals; - float32_literals := [] - end; - if !jumptables <> [] then begin - section oc jmptbl; - print_align oc 4; - List.iter (print_jumptable oc) !jumptables; - jumptables := [] - end - -let print_init oc = function - | Init_int8 n -> - fprintf oc " .byte %ld\n" (camlint_of_coqint n) - | Init_int16 n -> - fprintf oc " .short %ld\n" (camlint_of_coqint n) - | Init_int32 n -> - fprintf oc " .long %ld\n" (camlint_of_coqint n) - | Init_int64 n -> - fprintf oc " .quad %Ld\n" (camlint64_of_coqint n) - | Init_float32 n -> - fprintf oc " .long %ld %s %.18g\n" - (camlint_of_coqint (Floats.Float32.to_bits n)) - comment (camlfloat_of_coqfloat n) - | Init_float64 n -> - fprintf oc " .quad %Ld %s %.18g\n" - (camlint64_of_coqint (Floats.Float.to_bits n)) - comment (camlfloat_of_coqfloat n) - | Init_space n -> - if Z.gt n Z.zero then - fprintf oc " .space %s\n" (Z.to_string n) - | Init_addrof(symb, ofs) -> - fprintf oc " .long %a\n" - symbol_offset (symb, camlint_of_coqint ofs) - -let print_init_data oc name id = - if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0 - && List.for_all (function Init_int8 _ -> true | _ -> false) id - then - fprintf oc " .ascii \"%s\"\n" (PrintCsyntax.string_of_init id) - else - List.iter (print_init oc) id - -let print_var oc name v = - match v.gvar_init with - | [] -> () - | _ -> - let sec = - match C2C.atom_sections name with - | [s] -> s - | _ -> Section_data true - and align = - match C2C.atom_alignof name with - | Some a -> a - | None -> 8 in (* 8-alignment is a safe default *) - let name_sec = - name_of_section sec in - if name_sec <> "COMM" then begin - fprintf oc " %s\n" name_sec; - print_align oc align; - if not (C2C.atom_is_static name) then - fprintf oc " .globl %a\n" symbol name; - fprintf oc "%a:\n" symbol name; - print_init_data oc name v.gvar_init; - print_var_info oc name - end else begin - let sz = - match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in - if C2C.atom_is_static name - then Target.print_lcomm_decl oc name sz align - else Target.print_comm_decl oc name sz align - end - -let print_globdef oc (name, gdef) = - match gdef with - | Gfun(Internal code) -> print_function oc name code - | Gfun(External ef) -> () - | Gvar v -> print_var oc name v -end) - -let print_program oc p = - let module Target = (val (match Configuration.system with - | "macosx" -> (module MacOS_System:SYSTEM) - | "linux" | "bsd" -> (module ELF_System:SYSTEM) - | "cygwin" -> (module Cygwin_System:SYSTEM) - | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")):SYSTEM) in - let module Printer = AsmPrinter(Target) in - PrintAnnot.print_version_and_options oc Printer.comment; - PrintAnnot.reset_filenames(); - Printer.need_masks := false; - List.iter (Printer.print_globdef oc) p.prog_defs; - if !Printer.need_masks then begin - Printer.section oc (Section_const true); - (* not Section_literal because not 8-bytes *) - Target.print_align oc 16; - fprintf oc "%a: .quad 0x8000000000000000, 0\n" - Target.raw_symbol "__negd_mask"; - fprintf oc "%a: .quad 0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n" - Target.raw_symbol "__absd_mask"; - fprintf oc "%a: .long 0x80000000, 0, 0, 0\n" - Target.raw_symbol "__negs_mask"; - fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" - Target.raw_symbol "__abss_mask" - end; - Target.print_epilogue oc; - PrintAnnot.close_filenames() diff --git a/ia32/PrintAsm.mli b/ia32/PrintAsm.mli deleted file mode 100644 index aefe3a0a..00000000 --- a/ia32/PrintAsm.mli +++ /dev/null @@ -1,13 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -val print_program: out_channel -> Asm.program -> unit diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml new file mode 100644 index 00000000..d5ce2899 --- /dev/null +++ b/ia32/TargetPrinter.ml @@ -0,0 +1,993 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Printing IA32 assembly code in asm syntax *) + +open Printf +open Datatypes +open Camlcoq +open Sections +open AST +open Memdata +open Asm +open PrintAsmaux + +module StringSet = Set.Make(String) + +(* Basic printing functions used in definition of the systems *) + +let int_reg_name = function + | EAX -> "%eax" | EBX -> "%ebx" | ECX -> "%ecx" | EDX -> "%edx" + | ESI -> "%esi" | EDI -> "%edi" | EBP -> "%ebp" | ESP -> "%esp" + +let int8_reg_name = function + | EAX -> "%al" | EBX -> "%bl" | ECX -> "%cl" | EDX -> "%dl" + | _ -> assert false + +let high_int8_reg_name = function + | EAX -> "%ah" | EBX -> "%bh" | ECX -> "%ch" | EDX -> "%dh" + | _ -> assert false + +let int16_reg_name = function + | EAX -> "%ax" | EBX -> "%bx" | ECX -> "%cx" | EDX -> "%dx" + | ESI -> "%si" | EDI -> "%di" | EBP -> "%bp" | ESP -> "%sp" + +let float_reg_name = function + | XMM0 -> "%xmm0" | XMM1 -> "%xmm1" | XMM2 -> "%xmm2" | XMM3 -> "%xmm3" + | XMM4 -> "%xmm4" | XMM5 -> "%xmm5" | XMM6 -> "%xmm6" | XMM7 -> "%xmm7" + +let ireg oc r = output_string oc (int_reg_name r) +let ireg8 oc r = output_string oc (int8_reg_name r) +let high_ireg8 oc r = output_string oc (high_int8_reg_name r) +let ireg16 oc r = output_string oc (int16_reg_name r) +let freg oc r = output_string oc (float_reg_name r) + +let preg oc = function + | IR r -> ireg oc r + | FR r -> freg oc r + | _ -> assert false + +(* The comment deliminiter *) +let comment = "#" + +(* System dependend printer functions *) +module type SYSTEM = + sig + val raw_symbol: out_channel -> string -> unit + val symbol: out_channel -> P.t -> unit + val label: out_channel -> int -> unit + val name_of_section: section_name -> string + val stack_alignment: int + val print_align: out_channel -> int -> unit + val print_mov_ra: out_channel -> ireg -> ident -> unit + val print_fun_info: out_channel -> P.t -> unit + val print_var_info: out_channel -> P.t -> unit + val print_epilogue: out_channel -> 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 + +(* Printer functions for cygwin *) +module Cygwin_System : SYSTEM = + struct + + let raw_symbol oc s = + fprintf oc "_%s" s + + let symbol oc symb = + raw_symbol oc (extern_atom symb) + + let label oc lbl = + fprintf oc "L%d" lbl + + let name_of_section = function + | Section_text -> ".text" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".section .rdata,\"dr\"" else "COMM" + | Section_string -> ".section .rdata,\"dr\"" + | Section_literal -> ".section .rdata,\"dr\"" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\", \"%s\"\n" + s (if ex then "xr" else if wr then "d" else "dr") + + let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) + + let print_align oc n = + fprintf oc " .align %d\n" n + + let print_mov_ra oc rd id = + fprintf oc " movl $%a, %a\n" symbol id ireg rd + + let print_fun_info _ _ = () + + let print_var_info _ _ = () + + let print_epilogue _ = () + + 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 + +(* Printer functions for ELF *) +module ELF_System : SYSTEM = + struct + + let raw_symbol oc s = + fprintf oc "%s" s + + let symbol = elf_symbol + + let label = elf_label + + let name_of_section = function + | Section_text -> ".text" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".section .rodata" else "COMM" + | Section_string -> ".section .rodata" + | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\",\"a%s%s\",@progbits" + s (if wr then "w" else "") (if ex then "x" else "") + + let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) + + let print_align oc n = + fprintf oc " .align %d\n" n + + let print_mov_ra oc rd id = + fprintf oc " movl $%a, %a\n" symbol id ireg rd + + let print_fun_info = elf_print_fun_info + + let print_var_info = elf_print_var_info + + let print_epilogue _ = () + + 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 + +(* Printer functions for MacOS *) +module MacOS_System : SYSTEM = + struct + + let raw_symbol oc s = + fprintf oc "_%s" s + + let symbol oc symb = + raw_symbol oc (extern_atom symb) + + let label oc lbl = + fprintf oc "L%d" lbl + + let name_of_section = function + | Section_text -> ".text" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".const" else "COMM" + | Section_string -> ".const" + | Section_literal -> ".literal8" + | Section_jumptable -> ".const" + | 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") + + let stack_alignment = 16 (* mandatory *) + + (* 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) + + let print_align oc n = + fprintf oc " .align %d\n" (log2 n) + + let indirect_symbols : StringSet.t ref = ref StringSet.empty + + let print_mov_ra oc rd id = + let id = extern_atom id in + indirect_symbols := StringSet.add id !indirect_symbols; + fprintf oc " movl L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd + + let print_fun_info _ _ = () + + let print_var_info _ _ = () + + let print_epilogue oc = + fprintf oc " .section __IMPORT,__pointers,non_lazy_symbol_pointers\n"; + StringSet.iter + (fun s -> + fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s; + fprintf oc " .indirect_symbol %a\n" raw_symbol s; + fprintf oc " .long 0\n") + !indirect_symbols; + indirect_symbols := StringSet.empty + + 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 Target(System: SYSTEM):TARGET = + struct + open System + let symbol = symbol + +(* Basic printing functions *) + + let symbol_offset oc (symb, ofs) = + symbol oc symb; + if ofs <> 0l then fprintf oc " + %ld" ofs + + + let addressing oc (Addrmode(base, shift, cst)) = + begin match cst with + | Coq_inl n -> + let n = camlint_of_coqint n in + fprintf oc "%ld" n + | Coq_inr(id, ofs) -> + let ofs = camlint_of_coqint ofs in + if ofs = 0l + then symbol oc id + else fprintf oc "(%a + %ld)" symbol id ofs + end; + begin match base, shift with + | None, None -> () + | Some r1, None -> fprintf oc "(%a)" ireg r1 + | None, Some(r2,sc) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc + | Some r1, Some(r2,sc) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 coqint sc + end + + let name_of_condition = function + | Cond_e -> "e" | Cond_ne -> "ne" + | Cond_b -> "b" | Cond_be -> "be" | Cond_ae -> "ae" | Cond_a -> "a" + | Cond_l -> "l" | Cond_le -> "le" | Cond_ge -> "ge" | Cond_g -> "g" + | Cond_p -> "p" | Cond_np -> "np" + + let name_of_neg_condition = function + | Cond_e -> "ne" | Cond_ne -> "e" + | Cond_b -> "ae" | Cond_be -> "a" | Cond_ae -> "b" | Cond_a -> "be" + | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le" + | Cond_p -> "np" | Cond_np -> "p" + + +(* Names of sections *) + + let section oc sec = + fprintf oc " %s\n" (name_of_section sec) + +(* SP adjustment to allocate or free a stack frame *) + + let int32_align n a = + if n >= 0l + then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a)) + else Int32.logand n (Int32.of_int (-a)) + + let sp_adjustment sz = + let sz = camlint_of_coqint sz in + (* Preserve proper alignment of the stack *) + let sz = int32_align sz stack_alignment in + (* The top 4 bytes have already been allocated by the "call" instruction. *) + let sz = Int32.sub sz 4l in + sz + +(* 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) + +(* Emit a align directive *) + + let need_masks = ref false + +(* Emit .file / .loc debugging directives *) + + let print_file_line oc file line = + PrintAnnot.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) + + +(* Built-in functions *) + +(* Built-ins. They come in two flavors: + - annotation statements: take their arguments in registers or stack + locations; generate no code; + - inlined by the compiler: take their arguments in arbitrary + registers; preserve all registers except ECX, EDX, XMM6 and XMM7. *) + +(* Handling of annotations *) + + let print_annot_stmt oc txt targs args = + if Str.string_match re_file_line txt 0 then begin + print_file_line oc (Str.matched_group 1 txt) + (int_of_string (Str.matched_group 2 txt)) + end else begin + fprintf oc "%s annotation: " comment; + PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args + end + + let print_annot_val oc txt args res = + fprintf oc "%s annotation: " comment; + PrintAnnot.print_annot_val preg oc txt args; + match args, res with + | [IR src], [IR dst] -> + if dst <> src then fprintf oc " movl %a, %a\n" ireg src ireg dst + | [FR src], [FR dst] -> + if dst <> src then fprintf oc " movapd %a, %a\n" freg src freg dst + | _, _ -> assert false + +(* Handling of memcpy *) + +(* Unaligned memory accesses are quite fast on IA32, so use large + memory accesses regardless of alignment. *) + + let print_builtin_memcpy_small oc sz al src dst = + assert (src = EDX && dst = EAX); + let rec copy ofs sz = + if sz >= 8 && !Clflags.option_ffpu then begin + fprintf oc " movq %d(%a), %a\n" ofs ireg src freg XMM7; + fprintf oc " movq %a, %d(%a)\n" freg XMM7 ofs ireg dst; + copy (ofs + 8) (sz - 8) + end else if sz >= 4 then begin + fprintf oc " movl %d(%a), %a\n" ofs ireg src ireg ECX; + fprintf oc " movl %a, %d(%a)\n" ireg ECX ofs ireg dst; + copy (ofs + 4) (sz - 4) + end else if sz >= 2 then begin + fprintf oc " movw %d(%a), %a\n" ofs ireg src ireg16 ECX; + fprintf oc " movw %a, %d(%a)\n" ireg16 ECX ofs ireg dst; + copy (ofs + 2) (sz - 2) + end else if sz >= 1 then begin + fprintf oc " movb %d(%a), %a\n" ofs ireg src ireg8 ECX; + fprintf oc " movb %a, %d(%a)\n" ireg8 ECX ofs ireg dst; + copy (ofs + 1) (sz - 1) + end in + copy 0 sz + + let print_builtin_memcpy_big oc sz al src dst = + assert (src = ESI && dst = EDI); + fprintf oc " movl $%d, %a\n" (sz / 4) ireg ECX; + fprintf oc " rep movsl\n"; + if sz mod 4 >= 2 then fprintf oc " movsw\n"; + if sz mod 2 >= 1 then fprintf oc " movsb\n" + + let print_builtin_memcpy oc sz al args = + let (dst, src) = + match args with [IR d; IR s] -> (d, s) | _ -> assert false in + fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n" + comment sz al; + if sz <= 32 + then print_builtin_memcpy_small oc sz al src dst + else print_builtin_memcpy_big oc sz al src dst; + fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment + +(* Handling of volatile reads and writes *) + + let offset_addressing (Addrmode(base, ofs, cst)) delta = + Addrmode(base, ofs, + match cst with + | Coq_inl n -> Coq_inl(Integers.Int.add n delta) + | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta)) + + let print_builtin_vload_common oc chunk addr res = + match chunk, res with + | Mint8unsigned, [IR res] -> + fprintf oc " movzbl %a, %a\n" addressing addr ireg res + | Mint8signed, [IR res] -> + fprintf oc " movsbl %a, %a\n" addressing addr ireg res + | Mint16unsigned, [IR res] -> + fprintf oc " movzwl %a, %a\n" addressing addr ireg res + | Mint16signed, [IR res] -> + fprintf oc " movswl %a, %a\n" addressing addr ireg res + | Mint32, [IR res] -> + fprintf oc " movl %a, %a\n" addressing addr ireg res + | Mint64, [IR res1; IR res2] -> + let addr' = offset_addressing addr (coqint_of_camlint 4l) in + if not (Asmgen.addressing_mentions addr res2) then begin + fprintf oc " movl %a, %a\n" addressing addr ireg res2; + fprintf oc " movl %a, %a\n" addressing addr' ireg res1 + end else begin + fprintf oc " movl %a, %a\n" addressing addr' ireg res1; + fprintf oc " movl %a, %a\n" addressing addr ireg res2 + end + | Mfloat32, [FR res] -> + fprintf oc " movss %a, %a\n" addressing addr freg res + | Mfloat64, [FR res] -> + fprintf oc " movsd %a, %a\n" addressing addr freg res + | _ -> + assert false + + let print_builtin_vload oc chunk args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + begin match args with + | [IR addr] -> + print_builtin_vload_common oc chunk + (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) res + | _ -> + assert false + end; + fprintf oc "%s end builtin __builtin_volatile_read\n" comment + + let print_builtin_vload_global oc chunk id ofs args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + print_builtin_vload_common oc chunk + (Addrmode(None, None, Coq_inr(id,ofs))) res; + fprintf oc "%s end builtin __builtin_volatile_read\n" comment + + let print_builtin_vstore_common oc chunk addr src tmp = + match chunk, src with + | (Mint8signed | Mint8unsigned), [IR src] -> + if Asmgen.low_ireg src then + fprintf oc " movb %a, %a\n" ireg8 src addressing addr + else begin + fprintf oc " movl %a, %a\n" ireg src ireg tmp; + fprintf oc " movb %a, %a\n" ireg8 tmp addressing addr + end + | (Mint16signed | Mint16unsigned), [IR src] -> + fprintf oc " movw %a, %a\n" ireg16 src addressing addr + | Mint32, [IR src] -> + fprintf oc " movl %a, %a\n" ireg src addressing addr + | Mint64, [IR src1; IR src2] -> + let addr' = offset_addressing addr (coqint_of_camlint 4l) in + fprintf oc " movl %a, %a\n" ireg src2 addressing addr; + fprintf oc " movl %a, %a\n" ireg src1 addressing addr' + | Mfloat32, [FR src] -> + fprintf oc " movss %a, %a\n" freg src addressing addr + | Mfloat64, [FR src] -> + fprintf oc " movsd %a, %a\n" freg src addressing addr + | _ -> + assert false + + let print_builtin_vstore oc chunk args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + begin match args with + | IR addr :: src -> + print_builtin_vstore_common oc chunk + (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src + (if addr = EAX then ECX else EAX) + | _ -> + assert false + end; + fprintf oc "%s end builtin __builtin_volatile_write\n" comment + + let print_builtin_vstore_global oc chunk id ofs args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + print_builtin_vstore_common oc chunk + (Addrmode(None, None, Coq_inr(id,ofs))) args EAX; + fprintf oc "%s end builtin __builtin_volatile_write\n" comment + +(* Handling of varargs *) + + let print_builtin_va_start oc r = + if not (!current_function_sig).sig_cc.cc_vararg then + invalid_arg "Fatal error: va_start used in non-vararg function"; + let ofs = + Int32.(add (add !current_function_stacksize 4l) + (mul 4l (Z.to_int32 (Conventions1.size_arguments + !current_function_sig)))) in + fprintf oc " movl %%esp, 0(%a)\n" ireg r; + fprintf oc " addl $%ld, 0(%a)\n" ofs ireg r + +(* Handling of compiler-inlined builtins *) + + let print_builtin_inline oc name args res = + fprintf oc "%s begin builtin %s\n" comment name; + begin match name, args, res with + (* Integer arithmetic *) + | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] -> + if a1 <> res then + fprintf oc " movl %a, %a\n" ireg a1 ireg res; + fprintf oc " bswap %a\n" ireg res + | "__builtin_bswap16", [IR a1], [IR res] -> + if a1 <> res then + fprintf oc " movl %a, %a\n" ireg a1 ireg res; + fprintf oc " rolw $8, %a\n" ireg16 res + | "__builtin_clz", [IR a1], [IR res] -> + fprintf oc " bsrl %a, %a\n" ireg a1 ireg res; + fprintf oc " xorl $31, %a\n" ireg res + | "__builtin_ctz", [IR a1], [IR res] -> + fprintf oc " bsfl %a, %a\n" ireg a1 ireg res + (* Float arithmetic *) + | "__builtin_fabs", [FR a1], [FR res] -> + need_masks := true; + if a1 <> res then + fprintf oc " movapd %a, %a\n" freg a1 freg res; + fprintf oc " andpd %a, %a\n" raw_symbol "__absd_mask" freg res + | "__builtin_fsqrt", [FR a1], [FR res] -> + fprintf oc " sqrtsd %a, %a\n" freg a1 freg res + | "__builtin_fmax", [FR a1; FR a2], [FR res] -> + if res = a1 then + fprintf oc " maxsd %a, %a\n" freg a2 freg res + else if res = a2 then + fprintf oc " maxsd %a, %a\n" freg a1 freg res + else begin + fprintf oc " movapd %a, %a\n" freg a1 freg res; + fprintf oc " maxsd %a, %a\n" freg a2 freg res + end + | "__builtin_fmin", [FR a1; FR a2], [FR res] -> + if res = a1 then + fprintf oc " minsd %a, %a\n" freg a2 freg res + else if res = a2 then + fprintf oc " minsd %a, %a\n" freg a1 freg res + else begin + fprintf oc " movapd %a, %a\n" freg a1 freg res; + fprintf oc " minsd %a, %a\n" freg a2 freg res + end + | ("__builtin_fmadd"|"__builtin_fmsub"|"__builtin_fnmadd"|"__builtin_fnmsub"), + [FR a1; FR a2; FR a3], [FR res] -> + let opcode = + match name with + | "__builtin_fmadd" -> "vfmadd" + | "__builtin_fmsub" -> "vfmsub" + | "__builtin_fnmadd" -> "vfnmadd" + | "__builtin_fnmsub" -> "vfnmsub" + | _ -> assert false in + if res = a1 then + fprintf oc " %s132sd %a, %a, %a\n" opcode freg a2 freg a3 freg res + else if res = a2 then + fprintf oc " %s213sd %a, %a, %a\n" opcode freg a3 freg a1 freg res + else if res = a3 then + fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res + else begin + fprintf oc " movapd %a, %a\n" freg a3 freg res; + fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res + end + (* 64-bit integer arithmetic *) + | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> + assert (ah = EDX && al = EAX && rh = EDX && rl = EAX); + fprintf oc " negl %a\n" ireg EAX; + fprintf oc " adcl $0, %a\n" ireg EDX; + fprintf oc " negl %a\n" ireg EDX + | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); + fprintf oc " addl %a, %a\n" ireg EBX ireg EAX; + fprintf oc " adcl %a, %a\n" ireg ECX ireg EDX + | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); + fprintf oc " subl %a, %a\n" ireg EBX ireg EAX; + fprintf oc " sbbl %a, %a\n" ireg ECX ireg EDX + | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> + assert (a = EAX && b = EDX && rh = EDX && rl = EAX); + fprintf oc " mull %a\n" ireg EDX + (* Memory accesses *) + | "__builtin_read16_reversed", [IR a1], [IR res] -> + fprintf oc " movzwl 0(%a), %a\n" ireg a1 ireg res; + fprintf oc " rolw $8, %a\n" ireg16 res + | "__builtin_read32_reversed", [IR a1], [IR res] -> + fprintf oc " movl 0(%a), %a\n" ireg a1 ireg res; + fprintf oc " bswap %a\n" ireg res + | "__builtin_write16_reversed", [IR a1; IR a2], _ -> + let tmp = if a1 = ECX then EDX else ECX in + if a2 <> tmp then + fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; + fprintf oc " xchg %a, %a\n" ireg8 tmp high_ireg8 tmp; + fprintf oc " movw %a, 0(%a)\n" ireg16 tmp ireg a1 + | "__builtin_write32_reversed", [IR a1; IR a2], _ -> + let tmp = if a1 = ECX then EDX else ECX in + if a2 <> tmp then + fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; + fprintf oc " bswap %a\n" ireg tmp; + fprintf oc " movl %a, 0(%a)\n" ireg tmp ireg a1 + (* Synchronization *) + | "__builtin_membar", [], _ -> + () + (* Vararg stuff *) + | "__builtin_va_start", [IR a], _ -> + print_builtin_va_start oc a + (* Catch-all *) + | _ -> + invalid_arg ("unrecognized builtin " ^ name) + end; + fprintf oc "%s end builtin %s\n" comment name + +(* Printing of instructions *) + +(* Reminder on AT&T syntax: op source, dest *) + + let print_instruction oc = function + (* Moves *) + | Pmov_rr(rd, r1) -> + fprintf oc " movl %a, %a\n" ireg r1 ireg rd + | Pmov_ri(rd, n) -> + fprintf oc " movl $%ld, %a\n" (camlint_of_coqint n) ireg rd + | Pmov_ra(rd, id) -> + print_mov_ra oc rd id + | Pmov_rm(rd, a) | Pmov_rm_a(rd, a) -> + fprintf oc " movl %a, %a\n" addressing a ireg rd + | Pmov_mr(a, r1) | Pmov_mr_a(a, r1) -> + fprintf oc " movl %a, %a\n" ireg r1 addressing a + | Pmovsd_ff(rd, r1) -> + fprintf oc " movapd %a, %a\n" freg r1 freg rd + | Pmovsd_fi(rd, n) -> + let b = camlint64_of_coqint (Floats.Float.to_bits n) in + let lbl = new_label() in + fprintf oc " movsd %a, %a %s %.18g\n" label lbl freg rd comment (camlfloat_of_coqfloat n); + float64_literals := (lbl, b) :: !float64_literals + | Pmovsd_fm(rd, a) | Pmovsd_fm_a(rd, a) -> + fprintf oc " movsd %a, %a\n" addressing a freg rd + | Pmovsd_mf(a, r1) | Pmovsd_mf_a(a, r1) -> + fprintf oc " movsd %a, %a\n" freg r1 addressing a + | Pmovss_fi(rd, n) -> + let b = camlint_of_coqint (Floats.Float32.to_bits n) in + let lbl = new_label() in + fprintf oc " movss %a, %a %s %.18g\n" label lbl freg rd comment (camlfloat_of_coqfloat32 n); + float32_literals := (lbl, b) :: !float32_literals + | Pmovss_fm(rd, a) -> + fprintf oc " movss %a, %a\n" addressing a freg rd + | Pmovss_mf(a, r1) -> + fprintf oc " movss %a, %a\n" freg r1 addressing a + | Pfldl_m(a) -> + fprintf oc " fldl %a\n" addressing a + | Pfstpl_m(a) -> + fprintf oc " fstpl %a\n" addressing a + | Pflds_m(a) -> + fprintf oc " flds %a\n" addressing a + | Pfstps_m(a) -> + fprintf oc " fstps %a\n" addressing a + | Pxchg_rr(r1, r2) -> + fprintf oc " xchgl %a, %a\n" ireg r1 ireg r2 + (** Moves with conversion *) + | Pmovb_mr(a, r1) -> + fprintf oc " movb %a, %a\n" ireg8 r1 addressing a + | Pmovw_mr(a, r1) -> + fprintf oc " movw %a, %a\n" ireg16 r1 addressing a + | Pmovzb_rr(rd, r1) -> + fprintf oc " movzbl %a, %a\n" ireg8 r1 ireg rd + | Pmovzb_rm(rd, a) -> + fprintf oc " movzbl %a, %a\n" addressing a ireg rd + | Pmovsb_rr(rd, r1) -> + fprintf oc " movsbl %a, %a\n" ireg8 r1 ireg rd + | Pmovsb_rm(rd, a) -> + fprintf oc " movsbl %a, %a\n" addressing a ireg rd + | Pmovzw_rr(rd, r1) -> + fprintf oc " movzwl %a, %a\n" ireg16 r1 ireg rd + | Pmovzw_rm(rd, a) -> + fprintf oc " movzwl %a, %a\n" addressing a ireg rd + | Pmovsw_rr(rd, r1) -> + fprintf oc " movswl %a, %a\n" ireg16 r1 ireg rd + | Pmovsw_rm(rd, a) -> + fprintf oc " movswl %a, %a\n" addressing a ireg rd + | Pcvtsd2ss_ff(rd, r1) -> + fprintf oc " cvtsd2ss %a, %a\n" freg r1 freg rd + | Pcvtss2sd_ff(rd, r1) -> + fprintf oc " cvtss2sd %a, %a\n" freg r1 freg rd + | Pcvttsd2si_rf(rd, r1) -> + fprintf oc " cvttsd2si %a, %a\n" freg r1 ireg rd + | Pcvtsi2sd_fr(rd, r1) -> + fprintf oc " cvtsi2sd %a, %a\n" ireg r1 freg rd + | Pcvttss2si_rf(rd, r1) -> + fprintf oc " cvttss2si %a, %a\n" freg r1 ireg rd + | Pcvtsi2ss_fr(rd, r1) -> + fprintf oc " cvtsi2ss %a, %a\n" ireg r1 freg rd + (** Arithmetic and logical operations over integers *) + | Plea(rd, a) -> + fprintf oc " leal %a, %a\n" addressing a ireg rd + | Pneg(rd) -> + fprintf oc " negl %a\n" ireg rd + | Psub_rr(rd, r1) -> + fprintf oc " subl %a, %a\n" ireg r1 ireg rd + | Pimul_rr(rd, r1) -> + fprintf oc " imull %a, %a\n" ireg r1 ireg rd + | Pimul_ri(rd, n) -> + fprintf oc " imull $%a, %a\n" coqint n ireg rd + | Pimul_r(r1) -> + fprintf oc " imull %a\n" ireg r1 + | Pmul_r(r1) -> + fprintf oc " mull %a\n" ireg r1 + | Pdiv(r1) -> + fprintf oc " xorl %%edx, %%edx\n"; + fprintf oc " divl %a\n" ireg r1 + | Pidiv(r1) -> + fprintf oc " cltd\n"; + fprintf oc " idivl %a\n" ireg r1 + | Pand_rr(rd, r1) -> + fprintf oc " andl %a, %a\n" ireg r1 ireg rd + | Pand_ri(rd, n) -> + fprintf oc " andl $%a, %a\n" coqint n ireg rd + | Por_rr(rd, r1) -> + fprintf oc " orl %a, %a\n" ireg r1 ireg rd + | Por_ri(rd, n) -> + fprintf oc " orl $%a, %a\n" coqint n ireg rd + | Pxor_r(rd) -> + fprintf oc " xorl %a, %a\n" ireg rd ireg rd + | Pxor_rr(rd, r1) -> + fprintf oc " xorl %a, %a\n" ireg r1 ireg rd + | Pxor_ri(rd, n) -> + fprintf oc " xorl $%a, %a\n" coqint n ireg rd + | Pnot(rd) -> + fprintf oc " notl %a\n" ireg rd + | Psal_rcl(rd) -> + fprintf oc " sall %%cl, %a\n" ireg rd + | Psal_ri(rd, n) -> + fprintf oc " sall $%a, %a\n" coqint n ireg rd + | Pshr_rcl(rd) -> + fprintf oc " shrl %%cl, %a\n" ireg rd + | Pshr_ri(rd, n) -> + fprintf oc " shrl $%a, %a\n" coqint n ireg rd + | Psar_rcl(rd) -> + fprintf oc " sarl %%cl, %a\n" ireg rd + | Psar_ri(rd, n) -> + fprintf oc " sarl $%a, %a\n" coqint n ireg rd + | Pshld_ri(rd, r1, n) -> + fprintf oc " shldl $%a, %a, %a\n" coqint n ireg r1 ireg rd + | Pror_ri(rd, n) -> + fprintf oc " rorl $%a, %a\n" coqint n ireg rd + | Pcmp_rr(r1, r2) -> + fprintf oc " cmpl %a, %a\n" ireg r2 ireg r1 + | Pcmp_ri(r1, n) -> + fprintf oc " cmpl $%a, %a\n" coqint n ireg r1 + | Ptest_rr(r1, r2) -> + fprintf oc " testl %a, %a\n" ireg r2 ireg r1 + | Ptest_ri(r1, n) -> + fprintf oc " testl $%a, %a\n" coqint n ireg r1 + | Pcmov(c, rd, r1) -> + fprintf oc " cmov%s %a, %a\n" (name_of_condition c) ireg r1 ireg rd + | Psetcc(c, rd) -> + fprintf oc " set%s %a\n" (name_of_condition c) ireg8 rd; + fprintf oc " movzbl %a, %a\n" ireg8 rd ireg rd + (** Arithmetic operations over floats *) + | Paddd_ff(rd, r1) -> + fprintf oc " addsd %a, %a\n" freg r1 freg rd + | Psubd_ff(rd, r1) -> + fprintf oc " subsd %a, %a\n" freg r1 freg rd + | Pmuld_ff(rd, r1) -> + fprintf oc " mulsd %a, %a\n" freg r1 freg rd + | Pdivd_ff(rd, r1) -> + fprintf oc " divsd %a, %a\n" freg r1 freg rd + | Pnegd (rd) -> + need_masks := true; + fprintf oc " xorpd %a, %a\n" raw_symbol "__negd_mask" freg rd + | Pabsd (rd) -> + need_masks := true; + fprintf oc " andpd %a, %a\n" raw_symbol "__absd_mask" freg rd + | Pcomisd_ff(r1, r2) -> + fprintf oc " comisd %a, %a\n" freg r2 freg r1 + | Pxorpd_f (rd) -> + fprintf oc " xorpd %a, %a\n" freg rd freg rd + | Padds_ff(rd, r1) -> + fprintf oc " addss %a, %a\n" freg r1 freg rd + | Psubs_ff(rd, r1) -> + fprintf oc " subss %a, %a\n" freg r1 freg rd + | Pmuls_ff(rd, r1) -> + fprintf oc " mulss %a, %a\n" freg r1 freg rd + | Pdivs_ff(rd, r1) -> + fprintf oc " divss %a, %a\n" freg r1 freg rd + | Pnegs (rd) -> + need_masks := true; + fprintf oc " xorpd %a, %a\n" raw_symbol "__negs_mask" freg rd + | Pabss (rd) -> + need_masks := true; + fprintf oc " andpd %a, %a\n" raw_symbol "__abss_mask" freg rd + | Pcomiss_ff(r1, r2) -> + fprintf oc " comiss %a, %a\n" freg r2 freg r1 + | Pxorps_f (rd) -> + fprintf oc " xorpd %a, %a\n" freg rd freg rd + (** Branches and calls *) + | Pjmp_l(l) -> + fprintf oc " jmp %a\n" label (transl_label l) + | Pjmp_s(f, sg) -> + assert (not sg.sig_cc.cc_structret); + fprintf oc " jmp %a\n" symbol f + | Pjmp_r(r, sg) -> + assert (not sg.sig_cc.cc_structret); + fprintf oc " jmp *%a\n" ireg r + | Pjcc(c, l) -> + let l = transl_label l in + fprintf oc " j%s %a\n" (name_of_condition c) label l + | Pjcc2(c1, c2, l) -> + let l = transl_label l in + let l' = new_label() in + fprintf oc " j%s %a\n" (name_of_neg_condition c1) label l'; + fprintf oc " j%s %a\n" (name_of_condition c2) label l; + fprintf oc "%a:\n" label l' + | Pjmptbl(r, tbl) -> + let l = new_label() in + fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r; + jumptables := (l, tbl) :: !jumptables + | Pcall_s(f, sg) -> + fprintf oc " call %a\n" symbol f; + if sg.sig_cc.cc_structret then + fprintf oc " pushl %%eax\n" + | Pcall_r(r, sg) -> + fprintf oc " call *%a\n" ireg r; + if sg.sig_cc.cc_structret then + fprintf oc " pushl %%eax\n" + | Pret -> + if (!current_function_sig).sig_cc.cc_structret then begin + fprintf oc " movl 0(%%esp), %%eax\n"; + fprintf oc " ret $4\n" + end else begin + fprintf oc " ret\n" + end + (** Pseudo-instructions *) + | Plabel(l) -> + fprintf oc "%a:\n" label (transl_label l) + | Pallocframe(sz, ofs_ra, ofs_link) -> + let sz = sp_adjustment sz in + let ofs_link = camlint_of_coqint ofs_link in + fprintf oc " subl $%ld, %%esp\n" sz; + cfi_adjust oc sz; + fprintf oc " leal %ld(%%esp), %%edx\n" (Int32.add sz 4l); + fprintf oc " movl %%edx, %ld(%%esp)\n" ofs_link; + current_function_stacksize := sz + | Pfreeframe(sz, ofs_ra, ofs_link) -> + let sz = sp_adjustment sz in + fprintf oc " addl $%ld, %%esp\n" sz + | Pbuiltin(ef, args, res) -> + begin match ef with + | EF_builtin(name, sg) -> + print_builtin_inline oc (extern_atom name) args res + | EF_vload chunk -> + print_builtin_vload oc chunk args res + | EF_vstore chunk -> + print_builtin_vstore oc chunk args + | EF_vload_global(chunk, id, ofs) -> + print_builtin_vload_global oc chunk id ofs args res + | EF_vstore_global(chunk, id, ofs) -> + print_builtin_vstore_global oc chunk id ofs args + | EF_memcpy(sz, al) -> + print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz)) + (Int32.to_int (camlint_of_coqint al)) args + | EF_annot_val(txt, targ) -> + print_annot_val oc (extern_atom txt) args res + | EF_inline_asm txt -> + fprintf oc "%s begin inline assembly\n" comment; + fprintf oc " %s\n" (extern_atom txt); + fprintf oc "%s end inline assembly\n" comment + | _ -> + assert false + end + | Pannot(ef, args) -> + begin match ef with + | EF_annot(txt, targs) -> + print_annot_stmt oc (extern_atom txt) targs args + | _ -> + assert false + end + + let print_literal64 oc (lbl, n) = + fprintf oc "%a: .quad 0x%Lx\n" label lbl n + let print_literal32 oc (lbl, n) = + fprintf oc "%a: .long 0x%lx\n" label lbl n + + let print_jumptable oc jmptbl = + let print_jumptable oc (lbl, tbl) = + fprintf oc "%a:" label lbl; + List.iter + (fun l -> fprintf oc " .long %a\n" label (transl_label l)) + tbl in + if !jumptables <> [] then begin + section oc jmptbl; + print_align oc 4; + List.iter (print_jumptable oc) !jumptables; + jumptables := [] + end + + let print_init oc = function + | Init_int8 n -> + fprintf oc " .byte %ld\n" (camlint_of_coqint n) + | Init_int16 n -> + fprintf oc " .short %ld\n" (camlint_of_coqint n) + | Init_int32 n -> + fprintf oc " .long %ld\n" (camlint_of_coqint n) + | Init_int64 n -> + fprintf oc " .quad %Ld\n" (camlint64_of_coqint n) + | Init_float32 n -> + fprintf oc " .long %ld %s %.18g\n" + (camlint_of_coqint (Floats.Float32.to_bits n)) + comment (camlfloat_of_coqfloat n) + | Init_float64 n -> + fprintf oc " .quad %Ld %s %.18g\n" + (camlint64_of_coqint (Floats.Float.to_bits n)) + comment (camlfloat_of_coqfloat n) + | Init_space n -> + if Z.gt n Z.zero then + fprintf oc " .space %s\n" (Z.to_string n) + | Init_addrof(symb, ofs) -> + fprintf oc " .long %a\n" + symbol_offset (symb, camlint_of_coqint ofs) + + let print_align = print_align + + let print_comm_symb oc sz name align = + if C2C.atom_is_static name + then System.print_lcomm_decl oc name sz align + else System.print_comm_decl oc name sz align + + let name_of_section = name_of_section + + let emit_constants oc lit = + if !float64_literals <> [] || !float32_literals <> [] then begin + section oc lit; + print_align oc 8; + List.iter (print_literal64 oc) !float64_literals; + float64_literals := []; + List.iter (print_literal32 oc) !float32_literals; + float32_literals := [] + end + + let cfi_startproc = cfi_startproc + let cfi_endproc = cfi_endproc + + let print_instructions oc fn = List.iter (print_instruction oc) fn.fn_code + + let print_optional_fun_info _ = () + + let get_section_names name = + match C2C.atom_sections name with + | [t;l;j] -> (t, l, j) + | _ -> (Section_text, Section_literal, Section_jumptable) + + let reset_constants = reset_constants + + let print_fun_info = print_fun_info + + let print_var_info = print_var_info + + let print_prologue _ = + need_masks := false + + let print_epilogue oc = + if !need_masks then begin + section oc (Section_const true); + (* not Section_literal because not 8-bytes *) + print_align oc 16; + fprintf oc "%a: .quad 0x8000000000000000, 0\n" + raw_symbol "__negd_mask"; + fprintf oc "%a: .quad 0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n" + raw_symbol "__absd_mask"; + fprintf oc "%a: .long 0x80000000, 0, 0, 0\n" + raw_symbol "__negs_mask"; + fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" + raw_symbol "__abss_mask" + end; + System.print_epilogue oc + + let comment = comment + + let default_falignment = 16 +end + +let sel_target () = + let module S = (val (match Configuration.system with + | "macosx" -> (module MacOS_System:SYSTEM) + | "linux" + | "bsd" -> (module ELF_System:SYSTEM) + | "cygwin" -> (module Cygwin_System:SYSTEM) + | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") ):SYSTEM) in + (module Target(S):TARGET) diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml deleted file mode 100644 index 0c4356ec..00000000 --- a/powerpc/PrintAsm.ml +++ /dev/null @@ -1,849 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Printing PPC assembly code in asm syntax *) - -open Printf -open Datatypes -open Maps -open Camlcoq -open Sections -open AST -open Memdata -open Asm - -(* Recognition of target ABI and asm syntax *) - -module type SYSTEM = - sig - val comment: string - val constant: out_channel -> constant -> unit - val ireg: out_channel -> ireg -> unit - val freg: out_channel -> freg -> unit - val creg: out_channel -> int -> unit - val name_of_section: section_name -> string - val print_file_line: out_channel -> string -> int -> unit - val cfi_startproc: out_channel -> unit - val cfi_endproc: out_channel -> unit - val cfi_adjust: out_channel -> int32 -> unit - val cfi_rel_offset: out_channel -> string -> int32 -> unit - val print_prologue: out_channel -> unit - end - -let symbol oc symb = - fprintf oc "%s" (extern_atom symb) - -let symbol_offset oc (symb, ofs) = - symbol oc symb; - if ofs <> 0l then fprintf oc " + %ld" ofs - -let symbol_fragment oc s n op = - fprintf oc "(%a)%s" symbol_offset (s, camlint_of_coqint n) op - - -let int_reg_name = function - | GPR0 -> "0" | GPR1 -> "1" | GPR2 -> "2" | GPR3 -> "3" - | GPR4 -> "4" | GPR5 -> "5" | GPR6 -> "6" | GPR7 -> "7" - | GPR8 -> "8" | GPR9 -> "9" | GPR10 -> "10" | GPR11 -> "11" - | GPR12 -> "12" | GPR13 -> "13" | GPR14 -> "14" | GPR15 -> "15" - | GPR16 -> "16" | GPR17 -> "17" | GPR18 -> "18" | GPR19 -> "19" - | GPR20 -> "20" | GPR21 -> "21" | GPR22 -> "22" | GPR23 -> "23" - | GPR24 -> "24" | GPR25 -> "25" | GPR26 -> "26" | GPR27 -> "27" - | GPR28 -> "28" | GPR29 -> "29" | GPR30 -> "30" | GPR31 -> "31" - -let float_reg_name = function - | FPR0 -> "0" | FPR1 -> "1" | FPR2 -> "2" | FPR3 -> "3" - | FPR4 -> "4" | FPR5 -> "5" | FPR6 -> "6" | FPR7 -> "7" - | FPR8 -> "8" | FPR9 -> "9" | FPR10 -> "10" | FPR11 -> "11" - | FPR12 -> "12" | FPR13 -> "13" | FPR14 -> "14" | FPR15 -> "15" - | FPR16 -> "16" | FPR17 -> "17" | FPR18 -> "18" | FPR19 -> "19" - | FPR20 -> "20" | FPR21 -> "21" | FPR22 -> "22" | FPR23 -> "23" - | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27" - | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31" - -module Linux_System : SYSTEM = - struct - let comment = "#" - - let constant oc cst = - match cst with - | Cint n -> - fprintf oc "%ld" (camlint_of_coqint n) - | Csymbol_low(s, n) -> - symbol_fragment oc s n "@l" - | Csymbol_high(s, n) -> - symbol_fragment oc s n "@ha" - | Csymbol_sda(s, n) -> - symbol_fragment oc s n "@sda21" - (* 32-bit relative addressing is supported by the Diab tools but not by - GNU binutils. In the latter case, for testing purposes, we treat - them as absolute addressings. The default base register being GPR0, - this produces correct code, albeit with absolute addresses. *) - | Csymbol_rel_low(s, n) -> - symbol_fragment oc s n "@l" - | Csymbol_rel_high(s, n) -> - symbol_fragment oc s n "@ha" - - let ireg oc r = - output_string oc (int_reg_name r) - - let freg oc r = - output_string oc (float_reg_name r) - - let creg oc r = - fprintf oc "%d" r - - let name_of_section = function - | Section_text -> ".text" - | Section_data i -> - if i then ".data" else "COMM" - | Section_small_data i -> - if i then ".section .sdata,\"aw\",@progbits" else "COMM" - | Section_const i -> - if i then ".rodata" else "COMM" - | Section_small_const i -> - if i then ".section .sdata2,\"a\",@progbits" else "COMM" - | Section_string -> ".rodata" - | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\",\"a%s%s\",@progbits" - s (if wr then "w" else "") (if ex then "x" else "") - - let print_file_line oc file line = - PrintAnnot.print_file_line oc comment file line - - (* Emit .cfi directives *) - let cfi_startproc = - if Configuration.asm_supports_cfi then - (fun oc -> fprintf oc " .cfi_startproc\n") - else - (fun _ -> ()) - - let cfi_endproc = - if Configuration.asm_supports_cfi then - (fun oc -> fprintf oc " .cfi_endproc\n") - else - (fun _ -> ()) - - - let cfi_adjust = - if Configuration.asm_supports_cfi then - (fun oc delta -> fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta) - else - (fun _ _ -> ()) - - let cfi_rel_offset = - if Configuration.asm_supports_cfi then - (fun oc reg ofs -> fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs) - else - (fun _ _ _ -> ()) - - - let print_prologue oc = () - - end - -module Diab_System : SYSTEM = - struct - let comment = ";" - - let constant oc cst = - match cst with - | Cint n -> - fprintf oc "%ld" (camlint_of_coqint n) - | Csymbol_low(s, n) -> - symbol_fragment oc s n "@l" - | Csymbol_high(s, n) -> - symbol_fragment oc s n "@ha" - | Csymbol_sda(s, n) -> - symbol_fragment oc s n "@sdarx" - | Csymbol_rel_low(s, n) -> - symbol_fragment oc s n "@sdax@l" - | Csymbol_rel_high(s, n) -> - symbol_fragment oc s n "@sdarx@ha" - - let ireg oc r = - output_char oc 'r'; - output_string oc (int_reg_name r) - - let freg oc r = - output_char oc 'f'; - output_string oc (float_reg_name r) - - let creg oc r = - fprintf oc "cr%d" r - - let name_of_section = function - | Section_text -> ".text" - | Section_data i -> if i then ".data" else "COMM" - | Section_small_data i -> if i then ".sdata" else ".sbss" - | Section_const _ -> ".text" - | Section_small_const _ -> ".sdata2" - | Section_string -> ".text" - | Section_literal -> ".text" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\",,%c" - s - (match wr, ex with - | true, true -> 'm' (* text+data *) - | true, false -> 'd' (* data *) - | false, true -> 'c' (* text *) - | false, false -> 'r') (* const *) - - let print_file_line oc file line = - PrintAnnot.print_file_line_d1 oc comment file line - - (* Emit .cfi directives *) - let cfi_startproc oc = () - - let cfi_endproc oc = () - - let cfi_adjust oc delta = () - - let cfi_rel_offset oc reg ofs = () - - let print_prologue oc = - fprintf oc " .xopt align-fill-text=0x60000000\n"; - if !Clflags.option_g then - fprintf oc " .xopt asm-debug-on\n" - - end - -module AsmPrinter (Target : SYSTEM) = - struct - open Target - -(* On-the-fly label renaming *) - -let next_label = ref 100 - -let new_label() = - let lbl = !next_label in incr next_label; lbl - -let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t) - -let transl_label lbl = - try - Hashtbl.find current_function_labels lbl - with Not_found -> - let lbl' = new_label() in - Hashtbl.add current_function_labels lbl lbl'; - lbl' - -(* Basic printing functions *) - -let coqint oc n = - fprintf oc "%ld" (camlint_of_coqint n) - -let raw_symbol oc s = - fprintf oc "%s" s - - -let label oc lbl = - fprintf oc ".L%d" lbl - -let label_low oc lbl = - fprintf oc ".L%d@l" lbl - -let label_high oc lbl = - fprintf oc ".L%d@ha" lbl - - -let num_crbit = function - | CRbit_0 -> 0 - | CRbit_1 -> 1 - | CRbit_2 -> 2 - | CRbit_3 -> 3 - | CRbit_6 -> 6 - -let crbit oc bit = - fprintf oc "%d" (num_crbit bit) - -let ireg_or_zero oc r = - if r = GPR0 then output_string oc "0" else ireg oc r - -let preg oc = function - | IR r -> ireg oc r - | FR r -> freg oc r - | _ -> assert false - -let section oc sec = - let name = name_of_section sec in - assert (name <> "COMM"); - fprintf oc " %s\n" name - -let print_location oc loc = - if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) - -(* Encoding masks for rlwinm instructions *) - -let rolm_mask n = - let mb = ref 0 (* location of last 0->1 transition *) - and me = ref 32 (* location of last 1->0 transition *) - and last = ref ((Int32.logand n 1l) <> 0l) (* last bit seen *) - and count = ref 0 (* number of transitions *) - and mask = ref 0x8000_0000l in - for mx = 0 to 31 do - if Int32.logand n !mask <> 0l then - if !last then () else (incr count; mb := mx; last := true) - else - if !last then (incr count; me := mx; last := false) else (); - mask := Int32.shift_right_logical !mask 1 - done; - if !me = 0 then me := 32; - assert (!count = 2 || (!count = 0 && !last)); - (!mb, !me-1) - -(* Handling of annotations *) - -let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" - -let print_annot_stmt oc txt targs args = - if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) - (int_of_string (Str.matched_group 2 txt)) - end else begin - fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "R1" oc txt targs args - end - -(* Determine if the displacement of a conditional branch fits the short form *) - -let short_cond_branch tbl pc lbl_dest = - match PTree.get lbl_dest tbl with - | None -> assert false - | Some pc_dest -> - let disp = pc_dest - pc in -0x2000 <= disp && disp < 0x2000 - -(* Printing of instructions *) - -let float_literals : (int * int64) list ref = ref [] -let float32_literals : (int * int32) list ref = ref [] -let jumptables : (int * label list) list ref = ref [] - -let print_instruction oc tbl pc fallthrough = function - | Padd(r1, r2, r3) -> - fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Paddc(r1, r2, r3) -> - fprintf oc " addc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Padde(r1, r2, r3) -> - fprintf oc " adde %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Paddi(r1, r2, c) -> - fprintf oc " addi %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c - | Paddic(r1, r2, c) -> - fprintf oc " addic %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c - | Paddis(r1, r2, c) -> - fprintf oc " addis %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c - | Paddze(r1, r2) -> - fprintf oc " addze %a, %a\n" ireg r1 ireg r2 - | Pallocframe(sz, ofs) -> - assert false - | Pand_(r1, r2, r3) -> - fprintf oc " and. %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pandc(r1, r2, r3) -> - fprintf oc " andc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pandi_(r1, r2, c) -> - fprintf oc " andi. %a, %a, %a\n" ireg r1 ireg r2 constant c - | Pandis_(r1, r2, c) -> - fprintf oc " andis. %a, %a, %a\n" ireg r1 ireg r2 constant c - | Pb lbl -> - fprintf oc " b %a\n" label (transl_label lbl) - | Pbctr sg -> - fprintf oc " bctr\n" - | Pbctrl sg -> - fprintf oc " bctrl\n" - | Pbdnz lbl -> - fprintf oc " bdnz %a\n" label (transl_label lbl) - | Pbf(bit, lbl) -> - if !Clflags.option_faligncondbranchs > 0 then - fprintf oc " .balign %d\n" !Clflags.option_faligncondbranchs; - if short_cond_branch tbl pc lbl then - fprintf oc " bf %a, %a\n" crbit bit label (transl_label lbl) - else begin - let next = new_label() in - fprintf oc " bt %a, %a\n" crbit bit label next; - fprintf oc " b %a\n" label (transl_label lbl); - fprintf oc "%a:\n" label next - end - | Pbl(s, sg) -> - fprintf oc " bl %a\n" symbol s - | Pbs(s, sg) -> - fprintf oc " b %a\n" symbol s - | Pblr -> - fprintf oc " blr\n" - | Pbt(bit, lbl) -> - if !Clflags.option_faligncondbranchs > 0 then - fprintf oc " .balign %d\n" !Clflags.option_faligncondbranchs; - if short_cond_branch tbl pc lbl then - fprintf oc " bt %a, %a\n" crbit bit label (transl_label lbl) - else begin - let next = new_label() in - fprintf oc " bf %a, %a\n" crbit bit label next; - fprintf oc " b %a\n" label (transl_label lbl); - fprintf oc "%a:\n" label next - end - | Pbtbl(r, tbl) -> - let lbl = new_label() in - fprintf oc "%s begin pseudoinstr btbl(%a)\n" comment ireg r; - fprintf oc "%s jumptable [ " comment; - List.iter (fun l -> fprintf oc "%a " label (transl_label l)) tbl; - fprintf oc "]\n"; - fprintf oc " slwi %a, %a, 2\n" ireg GPR12 ireg r; - fprintf oc " addis %a, %a, %a\n" ireg GPR12 ireg GPR12 label_high lbl; - fprintf oc " lwz %a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12; - fprintf oc " mtctr %a\n" ireg GPR12; - fprintf oc " bctr\n"; - jumptables := (lbl, tbl) :: !jumptables; - fprintf oc "%s end pseudoinstr btbl\n" comment - | Pcmplw(r1, r2) -> - fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2 - | Pcmplwi(r1, c) -> - fprintf oc " cmplwi %a, %a, %a\n" creg 0 ireg r1 constant c - | Pcmpw(r1, r2) -> - fprintf oc " cmpw %a, %a, %a\n" creg 0 ireg r1 ireg r2 - | Pcmpwi(r1, c) -> - fprintf oc " cmpwi %a, %a, %a\n" creg 0 ireg r1 constant c - | Pcntlz(r1, r2) -> - fprintf oc " cntlz %a, %a\n" ireg r1 ireg r2 - | Pcreqv(c1, c2, c3) -> - fprintf oc " creqv %a, %a, %a\n" crbit c1 crbit c2 crbit c3 - | Pcror(c1, c2, c3) -> - fprintf oc " cror %a, %a, %a\n" crbit c1 crbit c2 crbit c3 - | Pcrxor(c1, c2, c3) -> - fprintf oc " crxor %a, %a, %a\n" crbit c1 crbit c2 crbit c3 - | Pdivw(r1, r2, r3) -> - fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pdivwu(r1, r2, r3) -> - fprintf oc " divwu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Peieio -> - fprintf oc " eieio\n" - | Peqv(r1, r2, r3) -> - fprintf oc " eqv %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pextsb(r1, r2) -> - fprintf oc " extsb %a, %a\n" ireg r1 ireg r2 - | Pextsh(r1, r2) -> - fprintf oc " extsh %a, %a\n" ireg r1 ireg r2 - | Pfreeframe(sz, ofs) -> - assert false - | Pfabs(r1, r2) | Pfabss(r1, r2) -> - fprintf oc " fabs %a, %a\n" freg r1 freg r2 - | Pfadd(r1, r2, r3) -> - fprintf oc " fadd %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfadds(r1, r2, r3) -> - fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfcmpu(r1, r2) -> - fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2 - | Pfcti(r1, r2) -> - assert false - | Pfctiw(r1, r2) -> - fprintf oc " fctiw %a, %a\n" freg r1 freg r2 - | Pfctiwz(r1, r2) -> - fprintf oc " fctiwz %a, %a\n" freg r1 freg r2 - | Pfdiv(r1, r2, r3) -> - fprintf oc " fdiv %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfdivs(r1, r2, r3) -> - fprintf oc " fdivs %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfmake(rd, r1, r2) -> - assert false - | Pfmr(r1, r2) -> - fprintf oc " fmr %a, %a\n" freg r1 freg r2 - | Pfmul(r1, r2, r3) -> - fprintf oc " fmul %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfmuls(r1, r2, r3) -> - fprintf oc " fmuls %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfneg(r1, r2) | Pfnegs(r1, r2) -> - fprintf oc " fneg %a, %a\n" freg r1 freg r2 - | Pfrsp(r1, r2) -> - fprintf oc " frsp %a, %a\n" freg r1 freg r2 - | Pfxdp(r1, r2) -> - assert false - | Pfsub(r1, r2, r3) -> - fprintf oc " fsub %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfsubs(r1, r2, r3) -> - fprintf oc " fsubs %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfmadd(r1, r2, r3, r4) -> - fprintf oc " fmadd %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 - | Pfmsub(r1, r2, r3, r4) -> - fprintf oc " fmsub %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 - | Pfnmadd(r1, r2, r3, r4) -> - fprintf oc " fnmadd %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 - | Pfnmsub(r1, r2, r3, r4) -> - fprintf oc " fnmsub %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 - | Pfsqrt(r1, r2) -> - fprintf oc " fsqrt %a, %a\n" freg r1 freg r2 - | Pfrsqrte(r1, r2) -> - fprintf oc " frsqrte %a, %a\n" freg r1 freg r2 - | Pfres(r1, r2) -> - fprintf oc " fres %a, %a\n" freg r1 freg r2 - | Pfsel(r1, r2, r3, r4) -> - fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 - | Pisync -> - fprintf oc " isync\n" - | Plbz(r1, c, r2) -> - fprintf oc " lbz %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Plbzx(r1, r2, r3) -> - fprintf oc " lbzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plfd(r1, c, r2) | Plfd_a(r1, c, r2) -> - fprintf oc " lfd %a, %a(%a)\n" freg r1 constant c ireg r2 - | Plfdx(r1, r2, r3) | Plfdx_a(r1, r2, r3) -> - fprintf oc " lfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3 - | Plfs(r1, c, r2) -> - fprintf oc " lfs %a, %a(%a)\n" freg r1 constant c ireg r2 - | Plfsx(r1, r2, r3) -> - fprintf oc " lfsx %a, %a, %a\n" freg r1 ireg r2 ireg r3 - | Plha(r1, c, r2) -> - fprintf oc " lha %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Plhax(r1, r2, r3) -> - fprintf oc " lhax %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plhbrx(r1, r2, r3) -> - fprintf oc " lhbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plhz(r1, c, r2) -> - fprintf oc " lhz %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Plhzx(r1, r2, r3) -> - fprintf oc " lhzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plfi(r1, c) -> - let lbl = new_label() in - fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; - fprintf oc " lfd %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat c); - float_literals := (lbl, camlint64_of_coqint (Floats.Float.to_bits c)) :: !float_literals; - | Plfis(r1, c) -> - let lbl = new_label() in - fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; - fprintf oc " lfs %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat32 c); - float32_literals := (lbl, camlint_of_coqint (Floats.Float32.to_bits c)) :: !float32_literals; - | Plwarx(r1, r2, r3) -> - fprintf oc " lwarx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plwbrx(r1, r2, r3) -> - fprintf oc " lwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plwz(r1, c, r2) | Plwz_a(r1, c, r2) -> - fprintf oc " lwz %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Plwzu(r1, c, r2) -> - fprintf oc " lwzu %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Plwzx(r1, r2, r3) | Plwzx_a(r1, r2, r3) -> - fprintf oc " lwzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pmfcr(r1) -> - fprintf oc " mfcr %a\n" ireg r1 - | Pmfcrbit(r1, bit) -> - assert false - | Pmflr(r1) -> - fprintf oc " mflr %a\n" ireg r1 - | Pmr(r1, r2) -> - fprintf oc " mr %a, %a\n" ireg r1 ireg r2 - | Pmtctr(r1) -> - fprintf oc " mtctr %a\n" ireg r1 - | Pmtlr(r1) -> - fprintf oc " mtlr %a\n" ireg r1 - | Pmulli(r1, r2, c) -> - fprintf oc " mulli %a, %a, %a\n" ireg r1 ireg r2 constant c - | Pmullw(r1, r2, r3) -> - fprintf oc " mullw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pmulhw(r1, r2, r3) -> - fprintf oc " mulhw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pmulhwu(r1, r2, r3) -> - fprintf oc " mulhwu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pnand(r1, r2, r3) -> - fprintf oc " nand %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pnor(r1, r2, r3) -> - fprintf oc " nor %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Por(r1, r2, r3) -> - fprintf oc " or %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Porc(r1, r2, r3) -> - fprintf oc " orc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pori(r1, r2, c) -> - fprintf oc " ori %a, %a, %a\n" ireg r1 ireg r2 constant c - | Poris(r1, r2, c) -> - fprintf oc " oris %a, %a, %a\n" ireg r1 ireg r2 constant c - | Prlwinm(r1, r2, c1, c2) -> - let (mb, me) = rolm_mask (camlint_of_coqint c2) in - fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n" - ireg r1 ireg r2 (camlint_of_coqint c1) mb me - comment (camlint_of_coqint c2) - | Prlwimi(r1, r2, c1, c2) -> - let (mb, me) = rolm_mask (camlint_of_coqint c2) in - fprintf oc " rlwimi %a, %a, %ld, %d, %d %s 0x%lx\n" - ireg r1 ireg r2 (camlint_of_coqint c1) mb me - comment (camlint_of_coqint c2) - | Pslw(r1, r2, r3) -> - fprintf oc " slw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Psraw(r1, r2, r3) -> - fprintf oc " sraw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Psrawi(r1, r2, c) -> - fprintf oc " srawi %a, %a, %ld\n" ireg r1 ireg r2 (camlint_of_coqint c) - | Psrw(r1, r2, r3) -> - fprintf oc " srw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstb(r1, c, r2) -> - fprintf oc " stb %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Pstbx(r1, r2, r3) -> - fprintf oc " stbx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstfd(r1, c, r2) | Pstfd_a(r1, c, r2) -> - fprintf oc " stfd %a, %a(%a)\n" freg r1 constant c ireg r2 - | Pstfdu(r1, c, r2) -> - fprintf oc " stfdu %a, %a(%a)\n" freg r1 constant c ireg r2 - | Pstfdx(r1, r2, r3) | Pstfdx_a(r1, r2, r3) -> - fprintf oc " stfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3 - | Pstfs(r1, c, r2) -> - fprintf oc " stfs %a, %a(%a)\n" freg r1 constant c ireg r2 - | Pstfsx(r1, r2, r3) -> - fprintf oc " stfsx %a, %a, %a\n" freg r1 ireg r2 ireg r3 - | Psth(r1, c, r2) -> - fprintf oc " sth %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Psthx(r1, r2, r3) -> - fprintf oc " sthx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Psthbrx(r1, r2, r3) -> - fprintf oc " sthbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstw(r1, c, r2) | Pstw_a(r1, c, r2) -> - fprintf oc " stw %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Pstwu(r1, c, r2) -> - fprintf oc " stwu %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Pstwx(r1, r2, r3) | Pstwx_a(r1, r2, r3) -> - fprintf oc " stwx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstwxu(r1, r2, r3) -> - fprintf oc " stwxu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstwbrx(r1, r2, r3) -> - fprintf oc " stwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstwcx_(r1, r2, r3) -> - fprintf oc " stwcx. %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Psubfc(r1, r2, r3) -> - fprintf oc " subfc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Psubfe(r1, r2, r3) -> - fprintf oc " subfe %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Psubfze(r1, r2) -> - fprintf oc " subfze %a, %a\n" ireg r1 ireg r2 - | Psubfic(r1, r2, c) -> - fprintf oc " subfic %a, %a, %a\n" ireg r1 ireg r2 constant c - | Psync -> - fprintf oc " sync\n" - | Ptrap -> - fprintf oc " trap\n" - | Pxor(r1, r2, r3) -> - fprintf oc " xor %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pxori(r1, r2, c) -> - fprintf oc " xori %a, %a, %a\n" ireg r1 ireg r2 constant c - | Pxoris(r1, r2, c) -> - fprintf oc " xoris %a, %a, %a\n" ireg r1 ireg r2 constant c - | Plabel lbl -> - if (not fallthrough) && !Clflags.option_falignbranchtargets > 0 then - fprintf oc " .balign %d\n" !Clflags.option_falignbranchtargets; - fprintf oc "%a:\n" label (transl_label lbl) - | Pbuiltin(ef, args, res) -> - begin match ef with - | EF_inline_asm txt -> - fprintf oc "%s begin inline assembly\n" comment; - fprintf oc " %s\n" (extern_atom txt); - fprintf oc "%s end inline assembly\n" comment - | _ -> - assert false - end - | Pannot(ef, args) -> - begin match ef with - | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) targs args - | _ -> - assert false - end - | Pcfi_adjust n -> - cfi_adjust oc (camlint_of_coqint n) - | Pcfi_rel_offset n -> - cfi_rel_offset oc "lr" (camlint_of_coqint n) - -(* Determine if an instruction falls through *) - -let instr_fall_through = function - | Pb _ -> false - | Pbctr _ -> false - | Pbs _ -> false - | Pblr -> false - | _ -> true - -(* Estimate the size of an Asm instruction encoding, in number of actual - PowerPC instructions. We can over-approximate. *) - -let instr_size = function - | Pbf(bit, lbl) -> 2 - | Pbt(bit, lbl) -> 2 - | Pbtbl(r, tbl) -> 5 - | Plfi(r1, c) -> 2 - | Plfis(r1, c) -> 2 - | Plabel lbl -> 0 - | Pbuiltin(ef, args, res) -> 0 - | Pannot(ef, args) -> 0 - | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0 - | _ -> 1 - -(* Build a table label -> estimated position in generated code. - Used to predict if relative conditional branches can use the short form. *) - -let rec label_positions tbl pc = function - | [] -> tbl - | Plabel lbl :: c -> label_positions (PTree.set lbl pc tbl) pc c - | i :: c -> label_positions tbl (pc + instr_size i) c - -(* Emit a sequence of instructions *) - -let rec print_instructions oc tbl pc fallthrough = function - | [] -> () - | i :: c -> - print_instruction oc tbl pc fallthrough i; - print_instructions oc tbl (pc + instr_size i) (instr_fall_through i) c - -(* Print the code for a function *) - -let print_literal64 oc (lbl, n) = - let nlo = Int64.to_int32 n - and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in - fprintf oc "%a: .long 0x%lx, 0x%lx\n" label lbl nhi nlo - -let print_literal32 oc (lbl, n) = - fprintf oc "%a: .long 0x%lx\n" label lbl n - -let print_jumptable oc (lbl, tbl) = - fprintf oc "%a:" label lbl; - List.iter - (fun l -> fprintf oc " .long %a\n" label (transl_label l)) - tbl - -let print_function oc name fn = - Hashtbl.clear current_function_labels; - float_literals := []; - float32_literals := []; - jumptables := []; - let (text, lit, jmptbl) = - match C2C.atom_sections name with - | [t;l;j] -> (t, l, j) - | _ -> (Section_text, Section_literal, Section_jumptable) in - section oc text; - let alignment = - match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in - fprintf oc " .balign %d\n" alignment; - if not (C2C.atom_is_static name) then - fprintf oc " .globl %a\n" symbol name; - fprintf oc "%a:\n" symbol name; - print_location oc (C2C.atom_location name); - cfi_startproc oc; - print_instructions oc (label_positions PTree.empty 0 fn.fn_code) - 0 true fn.fn_code; - cfi_endproc oc; - fprintf oc " .type %a, @function\n" symbol name; - fprintf oc " .size %a, . - %a\n" symbol name symbol name; - if !float_literals <> [] || !float32_literals <> [] then begin - section oc lit; - fprintf oc " .balign 8\n"; - List.iter (print_literal64 oc) !float_literals; - List.iter (print_literal32 oc) !float32_literals; - float_literals := []; float32_literals := [] - end; - if !jumptables <> [] then begin - section oc jmptbl; - fprintf oc " .balign 4\n"; - List.iter (print_jumptable oc) !jumptables; - jumptables := [] - end - -let print_init oc = function - | Init_int8 n -> - fprintf oc " .byte %ld\n" (camlint_of_coqint n) - | Init_int16 n -> - fprintf oc " .short %ld\n" (camlint_of_coqint n) - | Init_int32 n -> - fprintf oc " .long %ld\n" (camlint_of_coqint n) - | Init_int64 n -> - let b = camlint64_of_coqint n in - fprintf oc " .long 0x%Lx, 0x%Lx\n" - (Int64.shift_right_logical b 32) - (Int64.logand b 0xFFFFFFFFL) - | Init_float32 n -> - fprintf oc " .long 0x%lx %s %.18g\n" - (camlint_of_coqint (Floats.Float32.to_bits n)) - comment (camlfloat_of_coqfloat n) - | Init_float64 n -> - let b = camlint64_of_coqint (Floats.Float.to_bits n) in - fprintf oc " .long 0x%Lx, 0x%Lx %s %.18g\n" - (Int64.shift_right_logical b 32) - (Int64.logand b 0xFFFFFFFFL) - comment (camlfloat_of_coqfloat n) - | Init_space n -> - if Z.gt n Z.zero then - fprintf oc " .space %s\n" (Z.to_string n) - | Init_addrof(symb, ofs) -> - fprintf oc " .long %a\n" - symbol_offset (symb, camlint_of_coqint ofs) - -let print_init_data oc name id = - if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0 - && List.for_all (function Init_int8 _ -> true | _ -> false) id - then - fprintf oc " .ascii \"%s\"\n" (PrintCsyntax.string_of_init id) - else - List.iter (print_init oc) id - -let print_var oc name v = - match v.gvar_init with - | [] -> () - | _ -> - let sec = - match C2C.atom_sections name with - | [s] -> s - | _ -> Section_data true - and align = - match C2C.atom_alignof name with - | Some a -> a - | None -> 8 in (* 8-alignment is a safe default *) - let name_sec = - name_of_section sec in - if name_sec <> "COMM" then begin - fprintf oc " %s\n" name_sec; - fprintf oc " .balign %d\n" align; - if not (C2C.atom_is_static name) then - fprintf oc " .globl %a\n" symbol name; - fprintf oc "%a:\n" symbol name; - print_init_data oc name v.gvar_init; - fprintf oc " .type %a, @object\n" symbol name; - fprintf oc " .size %a, . - %a\n" symbol name symbol name - end else begin - let sz = - match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in - fprintf oc " %s %a, %s, %d\n" - (if C2C.atom_is_static name then ".lcomm" else ".comm") - symbol name - (Z.to_string sz) - align - end - -let print_globdef oc (name, gdef) = - match gdef with - | Gfun (Internal code) -> print_function oc name code - | Gfun (External ef) -> () - | Gvar v -> print_var oc name v - - end - -type target = Linux | Diab - -let print_program oc p = - let target = - (match Configuration.system with - | "linux" -> Linux - | "diab" -> Diab - | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")) in - let module Target = (val (match target with - | Linux -> (module Linux_System:SYSTEM) - | Diab -> (module Diab_System:SYSTEM)):SYSTEM) in - PrintAnnot.reset_filenames(); - PrintAnnot.print_version_and_options oc Target.comment; - let module Printer = AsmPrinter(Target) in - Target.print_prologue oc; - List.iter (Printer.print_globdef oc) p.prog_defs; - PrintAnnot.close_filenames() - - diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml new file mode 100644 index 00000000..70aec6c0 --- /dev/null +++ b/powerpc/TargetPrinter.ml @@ -0,0 +1,753 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Printing PPC assembly code in asm syntax *) + +open Printf +open Datatypes +open Maps +open Camlcoq +open Sections +open AST +open Memdata +open Asm +open PrintAsmaux + +(* Recognition of target ABI and asm syntax *) + +module type SYSTEM = + sig + val comment: string + val constant: out_channel -> constant -> unit + val ireg: out_channel -> ireg -> unit + val freg: out_channel -> freg -> unit + val creg: out_channel -> int -> unit + val name_of_section: section_name -> string + val print_file_line: out_channel -> string -> int -> unit + val cfi_startproc: out_channel -> unit + val cfi_endproc: out_channel -> unit + val cfi_adjust: out_channel -> int32 -> unit + val cfi_rel_offset: out_channel -> string -> int32 -> unit + val print_prologue: out_channel -> unit + end + +let symbol = elf_symbol + +let symbol_offset = elf_symbol_offset + +let symbol_fragment oc s n op = + fprintf oc "(%a)%s" symbol_offset (s, n) op + + +let int_reg_name = function + | GPR0 -> "0" | GPR1 -> "1" | GPR2 -> "2" | GPR3 -> "3" + | GPR4 -> "4" | GPR5 -> "5" | GPR6 -> "6" | GPR7 -> "7" + | GPR8 -> "8" | GPR9 -> "9" | GPR10 -> "10" | GPR11 -> "11" + | GPR12 -> "12" | GPR13 -> "13" | GPR14 -> "14" | GPR15 -> "15" + | GPR16 -> "16" | GPR17 -> "17" | GPR18 -> "18" | GPR19 -> "19" + | GPR20 -> "20" | GPR21 -> "21" | GPR22 -> "22" | GPR23 -> "23" + | GPR24 -> "24" | GPR25 -> "25" | GPR26 -> "26" | GPR27 -> "27" + | GPR28 -> "28" | GPR29 -> "29" | GPR30 -> "30" | GPR31 -> "31" + +let float_reg_name = function + | FPR0 -> "0" | FPR1 -> "1" | FPR2 -> "2" | FPR3 -> "3" + | FPR4 -> "4" | FPR5 -> "5" | FPR6 -> "6" | FPR7 -> "7" + | FPR8 -> "8" | FPR9 -> "9" | FPR10 -> "10" | FPR11 -> "11" + | FPR12 -> "12" | FPR13 -> "13" | FPR14 -> "14" | FPR15 -> "15" + | FPR16 -> "16" | FPR17 -> "17" | FPR18 -> "18" | FPR19 -> "19" + | FPR20 -> "20" | FPR21 -> "21" | FPR22 -> "22" | FPR23 -> "23" + | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27" + | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31" + +module Linux_System : SYSTEM = + struct + + let comment = "#" + + let constant oc cst = + match cst with + | Cint n -> + fprintf oc "%ld" (camlint_of_coqint n) + | Csymbol_low(s, n) -> + symbol_fragment oc s n "@l" + | Csymbol_high(s, n) -> + symbol_fragment oc s n "@ha" + | Csymbol_sda(s, n) -> + symbol_fragment oc s n "@sda21" + (* 32-bit relative addressing is supported by the Diab tools but not by + GNU binutils. In the latter case, for testing purposes, we treat + them as absolute addressings. The default base register being GPR0, + this produces correct code, albeit with absolute addresses. *) + | Csymbol_rel_low(s, n) -> + symbol_fragment oc s n "@l" + | Csymbol_rel_high(s, n) -> + symbol_fragment oc s n "@ha" + + let ireg oc r = + output_string oc (int_reg_name r) + + let freg oc r = + output_string oc (float_reg_name r) + + let creg oc r = + fprintf oc "%d" r + + let name_of_section = function + | Section_text -> ".text" + | Section_data i -> + if i then ".data" else "COMM" + | Section_small_data i -> + if i then ".section .sdata,\"aw\",@progbits" else "COMM" + | Section_const i -> + if i then ".rodata" else "COMM" + | Section_small_const i -> + if i then ".section .sdata2,\"a\",@progbits" else "COMM" + | Section_string -> ".rodata" + | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\",\"a%s%s\",@progbits" + s (if wr then "w" else "") (if ex then "x" else "") + + let print_file_line oc file line = + PrintAnnot.print_file_line oc comment file line + + (* Emit .cfi directives *) + let cfi_startproc = cfi_startproc + + let cfi_endproc = cfi_endproc + + let cfi_adjust = cfi_adjust + + let cfi_rel_offset = cfi_rel_offset + + let print_prologue oc = () + + end + +module Diab_System : SYSTEM = + struct + + let comment = ";" + + let constant oc cst = + match cst with + | Cint n -> + fprintf oc "%ld" (camlint_of_coqint n) + | Csymbol_low(s, n) -> + symbol_fragment oc s n "@l" + | Csymbol_high(s, n) -> + symbol_fragment oc s n "@ha" + | Csymbol_sda(s, n) -> + symbol_fragment oc s n "@sdarx" + | Csymbol_rel_low(s, n) -> + symbol_fragment oc s n "@sdax@l" + | Csymbol_rel_high(s, n) -> + symbol_fragment oc s n "@sdarx@ha" + + let ireg oc r = + output_char oc 'r'; + output_string oc (int_reg_name r) + + let freg oc r = + output_char oc 'f'; + output_string oc (float_reg_name r) + + let creg oc r = + fprintf oc "cr%d" r + + let name_of_section = function + | Section_text -> ".text" + | Section_data i -> if i then ".data" else "COMM" + | Section_small_data i -> if i then ".sdata" else ".sbss" + | Section_const _ -> ".text" + | Section_small_const _ -> ".sdata2" + | Section_string -> ".text" + | Section_literal -> ".text" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\",,%c" + s + (match wr, ex with + | true, true -> 'm' (* text+data *) + | true, false -> 'd' (* data *) + | false, true -> 'c' (* text *) + | false, false -> 'r') (* const *) + + let print_file_line oc file line = + PrintAnnot.print_file_line_d1 oc comment file line + + (* Emit .cfi directives *) + let cfi_startproc oc = () + + let cfi_endproc oc = () + + let cfi_adjust oc delta = () + + let cfi_rel_offset oc reg ofs = () + + let print_prologue oc = + fprintf oc " .xopt align-fill-text=0x60000000\n"; + if !Clflags.option_g then + fprintf oc " .xopt asm-debug-on\n" + + end + +module Target (System : SYSTEM):TARGET = + struct + include System + + (* Basic printing functions *) + let symbol = symbol + + let raw_symbol oc s = + fprintf oc "%s" s + + let label = elf_label + + let label_low oc lbl = + fprintf oc ".L%d@l" lbl + + let label_high oc lbl = + fprintf oc ".L%d@ha" lbl + + + let num_crbit = function + | CRbit_0 -> 0 + | CRbit_1 -> 1 + | CRbit_2 -> 2 + | CRbit_3 -> 3 + | CRbit_6 -> 6 + + let crbit oc bit = + fprintf oc "%d" (num_crbit bit) + + let ireg_or_zero oc r = + if r = GPR0 then output_string oc "0" else ireg oc r + + let preg oc = function + | IR r -> ireg oc r + | FR r -> freg oc r + | _ -> assert false + + let section oc sec = + let name = name_of_section sec in + assert (name <> "COMM"); + fprintf oc " %s\n" name + + let print_location oc loc = + if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) + + (* Encoding masks for rlwinm instructions *) + + let rolm_mask n = + let mb = ref 0 (* location of last 0->1 transition *) + and me = ref 32 (* location of last 1->0 transition *) + and last = ref ((Int32.logand n 1l) <> 0l) (* last bit seen *) + and count = ref 0 (* number of transitions *) + and mask = ref 0x8000_0000l in + for mx = 0 to 31 do + if Int32.logand n !mask <> 0l then + if !last then () else (incr count; mb := mx; last := true) + else + if !last then (incr count; me := mx; last := false) else (); + mask := Int32.shift_right_logical !mask 1 + done; + if !me = 0 then me := 32; + assert (!count = 2 || (!count = 0 && !last)); + (!mb, !me-1) + + (* Handling of annotations *) + + let print_annot_stmt oc txt targs args = + if Str.string_match re_file_line txt 0 then begin + print_file_line oc (Str.matched_group 1 txt) + (int_of_string (Str.matched_group 2 txt)) + end else begin + fprintf oc "%s annotation: " comment; + PrintAnnot.print_annot_stmt preg "R1" oc txt targs args + end + + (* Determine if the displacement of a conditional branch fits the short form *) + + let short_cond_branch tbl pc lbl_dest = + match PTree.get lbl_dest tbl with + | None -> assert false + | Some pc_dest -> + let disp = pc_dest - pc in -0x2000 <= disp && disp < 0x2000 + + (* Printing of instructions *) + + let print_instruction oc tbl pc fallthrough = function + | Padd(r1, r2, r3) -> + fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Paddc(r1, r2, r3) -> + fprintf oc " addc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Padde(r1, r2, r3) -> + fprintf oc " adde %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Paddi(r1, r2, c) -> + fprintf oc " addi %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c + | Paddic(r1, r2, c) -> + fprintf oc " addic %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c + | Paddis(r1, r2, c) -> + fprintf oc " addis %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c + | Paddze(r1, r2) -> + fprintf oc " addze %a, %a\n" ireg r1 ireg r2 + | Pallocframe(sz, ofs) -> + assert false + | Pand_(r1, r2, r3) -> + fprintf oc " and. %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pandc(r1, r2, r3) -> + fprintf oc " andc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pandi_(r1, r2, c) -> + fprintf oc " andi. %a, %a, %a\n" ireg r1 ireg r2 constant c + | Pandis_(r1, r2, c) -> + fprintf oc " andis. %a, %a, %a\n" ireg r1 ireg r2 constant c + | Pb lbl -> + fprintf oc " b %a\n" label (transl_label lbl) + | Pbctr sg -> + fprintf oc " bctr\n" + | Pbctrl sg -> + fprintf oc " bctrl\n" + | Pbdnz lbl -> + fprintf oc " bdnz %a\n" label (transl_label lbl) + | Pbf(bit, lbl) -> + if !Clflags.option_faligncondbranchs > 0 then + fprintf oc " .balign %d\n" !Clflags.option_faligncondbranchs; + if short_cond_branch tbl pc lbl then + fprintf oc " bf %a, %a\n" crbit bit label (transl_label lbl) + else begin + let next = new_label() in + fprintf oc " bt %a, %a\n" crbit bit label next; + fprintf oc " b %a\n" label (transl_label lbl); + fprintf oc "%a:\n" label next + end + | Pbl(s, sg) -> + fprintf oc " bl %a\n" symbol s + | Pbs(s, sg) -> + fprintf oc " b %a\n" symbol s + | Pblr -> + fprintf oc " blr\n" + | Pbt(bit, lbl) -> + if !Clflags.option_faligncondbranchs > 0 then + fprintf oc " .balign %d\n" !Clflags.option_faligncondbranchs; + if short_cond_branch tbl pc lbl then + fprintf oc " bt %a, %a\n" crbit bit label (transl_label lbl) + else begin + let next = new_label() in + fprintf oc " bf %a, %a\n" crbit bit label next; + fprintf oc " b %a\n" label (transl_label lbl); + fprintf oc "%a:\n" label next + end + | Pbtbl(r, tbl) -> + let lbl = new_label() in + fprintf oc "%s begin pseudoinstr btbl(%a)\n" comment ireg r; + fprintf oc "%s jumptable [ " comment; + List.iter (fun l -> fprintf oc "%a " label (transl_label l)) tbl; + fprintf oc "]\n"; + fprintf oc " slwi %a, %a, 2\n" ireg GPR12 ireg r; + fprintf oc " addis %a, %a, %a\n" ireg GPR12 ireg GPR12 label_high lbl; + fprintf oc " lwz %a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12; + fprintf oc " mtctr %a\n" ireg GPR12; + fprintf oc " bctr\n"; + jumptables := (lbl, tbl) :: !jumptables; + fprintf oc "%s end pseudoinstr btbl\n" comment + | Pcmplw(r1, r2) -> + fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2 + | Pcmplwi(r1, c) -> + fprintf oc " cmplwi %a, %a, %a\n" creg 0 ireg r1 constant c + | Pcmpw(r1, r2) -> + fprintf oc " cmpw %a, %a, %a\n" creg 0 ireg r1 ireg r2 + | Pcmpwi(r1, c) -> + fprintf oc " cmpwi %a, %a, %a\n" creg 0 ireg r1 constant c + | Pcntlz(r1, r2) -> + fprintf oc " cntlz %a, %a\n" ireg r1 ireg r2 + | Pcreqv(c1, c2, c3) -> + fprintf oc " creqv %a, %a, %a\n" crbit c1 crbit c2 crbit c3 + | Pcror(c1, c2, c3) -> + fprintf oc " cror %a, %a, %a\n" crbit c1 crbit c2 crbit c3 + | Pcrxor(c1, c2, c3) -> + fprintf oc " crxor %a, %a, %a\n" crbit c1 crbit c2 crbit c3 + | Pdivw(r1, r2, r3) -> + fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pdivwu(r1, r2, r3) -> + fprintf oc " divwu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Peieio -> + fprintf oc " eieio\n" + | Peqv(r1, r2, r3) -> + fprintf oc " eqv %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pextsb(r1, r2) -> + fprintf oc " extsb %a, %a\n" ireg r1 ireg r2 + | Pextsh(r1, r2) -> + fprintf oc " extsh %a, %a\n" ireg r1 ireg r2 + | Pfreeframe(sz, ofs) -> + assert false + | Pfabs(r1, r2) | Pfabss(r1, r2) -> + fprintf oc " fabs %a, %a\n" freg r1 freg r2 + | Pfadd(r1, r2, r3) -> + fprintf oc " fadd %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfadds(r1, r2, r3) -> + fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfcmpu(r1, r2) -> + fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2 + | Pfcti(r1, r2) -> + assert false + | Pfctiw(r1, r2) -> + fprintf oc " fctiw %a, %a\n" freg r1 freg r2 + | Pfctiwz(r1, r2) -> + fprintf oc " fctiwz %a, %a\n" freg r1 freg r2 + | Pfdiv(r1, r2, r3) -> + fprintf oc " fdiv %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfdivs(r1, r2, r3) -> + fprintf oc " fdivs %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfmake(rd, r1, r2) -> + assert false + | Pfmr(r1, r2) -> + fprintf oc " fmr %a, %a\n" freg r1 freg r2 + | Pfmul(r1, r2, r3) -> + fprintf oc " fmul %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfmuls(r1, r2, r3) -> + fprintf oc " fmuls %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfneg(r1, r2) | Pfnegs(r1, r2) -> + fprintf oc " fneg %a, %a\n" freg r1 freg r2 + | Pfrsp(r1, r2) -> + fprintf oc " frsp %a, %a\n" freg r1 freg r2 + | Pfxdp(r1, r2) -> + assert false + | Pfsub(r1, r2, r3) -> + fprintf oc " fsub %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfsubs(r1, r2, r3) -> + fprintf oc " fsubs %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfmadd(r1, r2, r3, r4) -> + fprintf oc " fmadd %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pfmsub(r1, r2, r3, r4) -> + fprintf oc " fmsub %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pfnmadd(r1, r2, r3, r4) -> + fprintf oc " fnmadd %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pfnmsub(r1, r2, r3, r4) -> + fprintf oc " fnmsub %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pfsqrt(r1, r2) -> + fprintf oc " fsqrt %a, %a\n" freg r1 freg r2 + | Pfrsqrte(r1, r2) -> + fprintf oc " frsqrte %a, %a\n" freg r1 freg r2 + | Pfres(r1, r2) -> + fprintf oc " fres %a, %a\n" freg r1 freg r2 + | Pfsel(r1, r2, r3, r4) -> + fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pisync -> + fprintf oc " isync\n" + | Plbz(r1, c, r2) -> + fprintf oc " lbz %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Plbzx(r1, r2, r3) -> + fprintf oc " lbzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Plfd(r1, c, r2) | Plfd_a(r1, c, r2) -> + fprintf oc " lfd %a, %a(%a)\n" freg r1 constant c ireg r2 + | Plfdx(r1, r2, r3) | Plfdx_a(r1, r2, r3) -> + fprintf oc " lfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3 + | Plfs(r1, c, r2) -> + fprintf oc " lfs %a, %a(%a)\n" freg r1 constant c ireg r2 + | Plfsx(r1, r2, r3) -> + fprintf oc " lfsx %a, %a, %a\n" freg r1 ireg r2 ireg r3 + | Plha(r1, c, r2) -> + fprintf oc " lha %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Plhax(r1, r2, r3) -> + fprintf oc " lhax %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Plhbrx(r1, r2, r3) -> + fprintf oc " lhbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Plhz(r1, c, r2) -> + fprintf oc " lhz %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Plhzx(r1, r2, r3) -> + fprintf oc " lhzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Plfi(r1, c) -> + let lbl = new_label() in + fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; + fprintf oc " lfd %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat c); + float64_literals := (lbl, camlint64_of_coqint (Floats.Float.to_bits c)) :: !float64_literals; + | Plfis(r1, c) -> + let lbl = new_label() in + fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; + fprintf oc " lfs %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat32 c); + float32_literals := (lbl, camlint_of_coqint (Floats.Float32.to_bits c)) :: !float32_literals; + | Plwarx(r1, r2, r3) -> + fprintf oc " lwarx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Plwbrx(r1, r2, r3) -> + fprintf oc " lwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Plwz(r1, c, r2) | Plwz_a(r1, c, r2) -> + fprintf oc " lwz %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Plwzu(r1, c, r2) -> + fprintf oc " lwzu %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Plwzx(r1, r2, r3) | Plwzx_a(r1, r2, r3) -> + fprintf oc " lwzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmfcr(r1) -> + fprintf oc " mfcr %a\n" ireg r1 + | Pmfcrbit(r1, bit) -> + assert false + | Pmflr(r1) -> + fprintf oc " mflr %a\n" ireg r1 + | Pmr(r1, r2) -> + fprintf oc " mr %a, %a\n" ireg r1 ireg r2 + | Pmtctr(r1) -> + fprintf oc " mtctr %a\n" ireg r1 + | Pmtlr(r1) -> + fprintf oc " mtlr %a\n" ireg r1 + | Pmulli(r1, r2, c) -> + fprintf oc " mulli %a, %a, %a\n" ireg r1 ireg r2 constant c + | Pmullw(r1, r2, r3) -> + fprintf oc " mullw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmulhw(r1, r2, r3) -> + fprintf oc " mulhw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmulhwu(r1, r2, r3) -> + fprintf oc " mulhwu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pnand(r1, r2, r3) -> + fprintf oc " nand %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pnor(r1, r2, r3) -> + fprintf oc " nor %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Por(r1, r2, r3) -> + fprintf oc " or %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Porc(r1, r2, r3) -> + fprintf oc " orc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pori(r1, r2, c) -> + fprintf oc " ori %a, %a, %a\n" ireg r1 ireg r2 constant c + | Poris(r1, r2, c) -> + fprintf oc " oris %a, %a, %a\n" ireg r1 ireg r2 constant c + | Prlwinm(r1, r2, c1, c2) -> + let (mb, me) = rolm_mask (camlint_of_coqint c2) in + fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n" + ireg r1 ireg r2 (camlint_of_coqint c1) mb me + comment (camlint_of_coqint c2) + | Prlwimi(r1, r2, c1, c2) -> + let (mb, me) = rolm_mask (camlint_of_coqint c2) in + fprintf oc " rlwimi %a, %a, %ld, %d, %d %s 0x%lx\n" + ireg r1 ireg r2 (camlint_of_coqint c1) mb me + comment (camlint_of_coqint c2) + | Pslw(r1, r2, r3) -> + fprintf oc " slw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Psraw(r1, r2, r3) -> + fprintf oc " sraw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Psrawi(r1, r2, c) -> + fprintf oc " srawi %a, %a, %ld\n" ireg r1 ireg r2 (camlint_of_coqint c) + | Psrw(r1, r2, r3) -> + fprintf oc " srw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pstb(r1, c, r2) -> + fprintf oc " stb %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Pstbx(r1, r2, r3) -> + fprintf oc " stbx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pstfd(r1, c, r2) | Pstfd_a(r1, c, r2) -> + fprintf oc " stfd %a, %a(%a)\n" freg r1 constant c ireg r2 + | Pstfdu(r1, c, r2) -> + fprintf oc " stfdu %a, %a(%a)\n" freg r1 constant c ireg r2 + | Pstfdx(r1, r2, r3) | Pstfdx_a(r1, r2, r3) -> + fprintf oc " stfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3 + | Pstfs(r1, c, r2) -> + fprintf oc " stfs %a, %a(%a)\n" freg r1 constant c ireg r2 + | Pstfsx(r1, r2, r3) -> + fprintf oc " stfsx %a, %a, %a\n" freg r1 ireg r2 ireg r3 + | Psth(r1, c, r2) -> + fprintf oc " sth %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Psthx(r1, r2, r3) -> + fprintf oc " sthx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Psthbrx(r1, r2, r3) -> + fprintf oc " sthbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pstw(r1, c, r2) | Pstw_a(r1, c, r2) -> + fprintf oc " stw %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Pstwu(r1, c, r2) -> + fprintf oc " stwu %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Pstwx(r1, r2, r3) | Pstwx_a(r1, r2, r3) -> + fprintf oc " stwx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pstwxu(r1, r2, r3) -> + fprintf oc " stwxu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pstwbrx(r1, r2, r3) -> + fprintf oc " stwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pstwcx_(r1, r2, r3) -> + fprintf oc " stwcx. %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Psubfc(r1, r2, r3) -> + fprintf oc " subfc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Psubfe(r1, r2, r3) -> + fprintf oc " subfe %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Psubfze(r1, r2) -> + fprintf oc " subfze %a, %a\n" ireg r1 ireg r2 + | Psubfic(r1, r2, c) -> + fprintf oc " subfic %a, %a, %a\n" ireg r1 ireg r2 constant c + | Psync -> + fprintf oc " sync\n" + | Ptrap -> + fprintf oc " trap\n" + | Pxor(r1, r2, r3) -> + fprintf oc " xor %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pxori(r1, r2, c) -> + fprintf oc " xori %a, %a, %a\n" ireg r1 ireg r2 constant c + | Pxoris(r1, r2, c) -> + fprintf oc " xoris %a, %a, %a\n" ireg r1 ireg r2 constant c + | Plabel lbl -> + if (not fallthrough) && !Clflags.option_falignbranchtargets > 0 then + fprintf oc " .balign %d\n" !Clflags.option_falignbranchtargets; + fprintf oc "%a:\n" label (transl_label lbl) + | Pbuiltin(ef, args, res) -> + begin match ef with + | EF_inline_asm txt -> + fprintf oc "%s begin inline assembly\n" comment; + fprintf oc " %s\n" (extern_atom txt); + fprintf oc "%s end inline assembly\n" comment + | _ -> + assert false + end + | Pannot(ef, args) -> + begin match ef with + | EF_annot(txt, targs) -> + print_annot_stmt oc (extern_atom txt) targs args + | _ -> + assert false + end + | Pcfi_adjust n -> + cfi_adjust oc (camlint_of_coqint n) + | Pcfi_rel_offset n -> + cfi_rel_offset oc "lr" (camlint_of_coqint n) + + (* Determine if an instruction falls through *) + + let instr_fall_through = function + | Pb _ -> false + | Pbctr _ -> false + | Pbs _ -> false + | Pblr -> false + | _ -> true + + (* Estimate the size of an Asm instruction encoding, in number of actual + PowerPC instructions. We can over-approximate. *) + + let instr_size = function + | Pbf(bit, lbl) -> 2 + | Pbt(bit, lbl) -> 2 + | Pbtbl(r, tbl) -> 5 + | Plfi(r1, c) -> 2 + | Plfis(r1, c) -> 2 + | Plabel lbl -> 0 + | Pbuiltin(ef, args, res) -> 0 + | Pannot(ef, args) -> 0 + | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0 + | _ -> 1 + + (* Build a table label -> estimated position in generated code. + Used to predict if relative conditional branches can use the short form. *) + + let rec label_positions tbl pc = function + | [] -> tbl + | Plabel lbl :: c -> label_positions (PTree.set lbl pc tbl) pc c + | i :: c -> label_positions tbl (pc + instr_size i) c + + (* Emit a sequence of instructions *) + + let print_instructions oc fn = + let rec aux oc tbl pc fallthrough = function + | [] -> () + | i :: c -> + print_instruction oc tbl pc fallthrough i; + aux oc tbl (pc + instr_size i) (instr_fall_through i) c in + aux oc (label_positions PTree.empty 0 fn.fn_code) 0 true fn.fn_code + + (* Print the code for a function *) + + let print_literal64 oc (lbl, n) = + let nlo = Int64.to_int32 n + and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in + fprintf oc "%a: .long 0x%lx, 0x%lx\n" label lbl nhi nlo + + let print_literal32 oc (lbl, n) = + fprintf oc "%a: .long 0x%lx\n" label lbl n + + let print_init oc = function + | Init_int8 n -> + fprintf oc " .byte %ld\n" (camlint_of_coqint n) + | Init_int16 n -> + fprintf oc " .short %ld\n" (camlint_of_coqint n) + | Init_int32 n -> + fprintf oc " .long %ld\n" (camlint_of_coqint n) + | Init_int64 n -> + let b = camlint64_of_coqint n in + fprintf oc " .long 0x%Lx, 0x%Lx\n" + (Int64.shift_right_logical b 32) + (Int64.logand b 0xFFFFFFFFL) + | Init_float32 n -> + fprintf oc " .long 0x%lx %s %.18g\n" + (camlint_of_coqint (Floats.Float32.to_bits n)) + comment (camlfloat_of_coqfloat n) + | Init_float64 n -> + let b = camlint64_of_coqint (Floats.Float.to_bits n) in + fprintf oc " .long 0x%Lx, 0x%Lx %s %.18g\n" + (Int64.shift_right_logical b 32) + (Int64.logand b 0xFFFFFFFFL) + comment (camlfloat_of_coqfloat n) + | Init_space n -> + if Z.gt n Z.zero then + fprintf oc " .space %s\n" (Z.to_string n) + | Init_addrof(symb, ofs) -> + fprintf oc " .long %a\n" + symbol_offset (symb, ofs) + + + let print_fun_info = elf_print_fun_info + + let emit_constants oc lit = + if !float64_literals <> [] || !float32_literals <> [] then begin + section oc lit; + fprintf oc " .balign 8\n"; + List.iter (print_literal64 oc) !float64_literals; + List.iter (print_literal32 oc) !float32_literals; + float64_literals := []; float32_literals := [] + end + + let print_optional_fun_info _ = () + + let get_section_names name = + match C2C.atom_sections name with + | [t;l;j] -> (t, l, j) + | _ -> (Section_text, Section_literal, Section_jumptable) + + let reset_constants = reset_constants + + let print_var_info = elf_print_var_info + + let print_comm_symb oc sz name align = + fprintf oc " %s %a, %s, %d\n" + (if C2C.atom_is_static name then ".lcomm" else ".comm") + symbol name + (Z.to_string sz) + align + + let print_align oc align = + fprintf oc " .balign %d\n" align + + let print_epilogue _ = () + + let print_jumptable oc jmptbl = + let print_jumptable oc (lbl, tbl) = + fprintf oc "%a:" label lbl; + List.iter + (fun l -> fprintf oc " .long %a\n" label (transl_label l)) + tbl in + if !jumptables <> [] then begin + section oc jmptbl; + fprintf oc " .balign 4\n"; + List.iter (print_jumptable oc) !jumptables; + jumptables := [] + end + + let default_falignment = 4 + end + +let sel_target () = + let module S = (val + (match Configuration.system with + | "linux" -> (module Linux_System:SYSTEM) + | "diab" -> (module Diab_System:SYSTEM) + | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")):SYSTEM) in + (module Target(S):TARGET) |