From a3c0094508f9f4985de4509380dada5f5c85e115 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 9 Feb 2015 14:54:42 +0100 Subject: Changed arm backend to the common backend printer. --- arm/TargetPrinter.ml | 1140 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1140 insertions(+) create mode 100644 arm/TargetPrinter.ml (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml new file mode 100644 index 00000000..73cdeae0 --- /dev/null +++ b/arm/TargetPrinter.ml @@ -0,0 +1,1140 @@ +(* *********************************************************************) +(* *) +(* 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 = label oc (transl_label lbl) + + let comment = "@" + + 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 = true + + let print_var_info = true + + 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 = () + + 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) -- cgit From 8677f50de8515bd83221e6a3d79b0f3d6dae4cbf Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 18 Feb 2015 12:52:54 +0100 Subject: Removed some style issues. --- arm/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 73cdeae0..079d78ff 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -37,7 +37,7 @@ module type PRINTER_OPTIONS = (* Module containing the printing functions *) module Target (Opt: PRINTER_OPTIONS) : TARGET = - (struct + struct (* Code generation options. *) let literals_in_code = ref true (* to be turned into a proper option *) @@ -1119,7 +1119,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let print_epilogue oc = () - end) + end let sel_target () = let module S : PRINTER_OPTIONS = struct -- cgit From 71260eff997f5d3c25d9ccda92b8176c893be26d Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 18 Feb 2015 13:06:58 +0100 Subject: Changed print_fun/var_info to be functions instead of booleans. --- arm/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 079d78ff..7eb01084 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -1058,9 +1058,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = if !Clflags.option_mthumb then fprintf oc " .thumb_func\n" - let print_fun_info = true + let print_fun_info = print_fun_info - let print_var_info = true + let print_var_info = print_var_info let print_comm_symb oc sz name align = if C2C.atom_is_static name then -- cgit From fcd5ba10674f499d4e270bfb68fa40da8857fb47 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 18 Feb 2015 15:06:53 +0100 Subject: Added an elf prefix to all common elf functions in PrintAsmaux. --- arm/TargetPrinter.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 7eb01084..1d37d237 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -44,10 +44,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (* Basic printing functions *) - let print_label oc lbl = label oc (transl_label lbl) + 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 @@ -1058,9 +1060,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = if !Clflags.option_mthumb then fprintf oc " .thumb_func\n" - let print_fun_info = print_fun_info + let print_fun_info = elf_print_fun_info - let print_var_info = print_var_info + let print_var_info = elf_print_var_info let print_comm_symb oc sz name align = if C2C.atom_is_static name then -- cgit From cb1da9d8176ea397b833f56ee49af5c75338676f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 19 Feb 2015 10:12:16 +0100 Subject: Removed unused sel_target, changed cygwin symbol names and changed the default function aligment to be target dependent. --- arm/TargetPrinter.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 1d37d237..62dd2bc2 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -1120,7 +1120,8 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " .%s\n" (if !Clflags.option_mthumb then "thumb" else "arm") let print_epilogue oc = () - + + let default_falignment = 4 end let sel_target () = -- cgit