diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 1642 | ||||
| -rw-r--r-- | cparser/Cerrors.ml | 6 | ||||
| -rw-r--r-- | cparser/Cerrors.mli | 1 | ||||
| -rw-r--r-- | doc/ccomp.1 | 4 | ||||
| -rwxr-xr-x[-rw-r--r--] | driver/Driver.ml | 17 | ||||
| -rw-r--r-- | lib/BoolEqual.v | 167 | ||||
| -rw-r--r-- | powerpc/AsmToJSON.ml | 7 | ||||
| -rw-r--r-- | x86/Op.v | 16 |
9 files changed, 1035 insertions, 827 deletions
@@ -58,7 +58,7 @@ FLOCQ=\ VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ Iteration.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \ Parmov.v UnionFind.v Wfsimpl.v \ - Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v + Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v # Parts common to the front-ends and the back-end (in common/) diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index eb1a7c4c..cb379f26 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -28,866 +28,878 @@ type float_abi_type = (* Module type for the options *) module type PRINTER_OPTIONS = - sig - val float_abi: float_abi_type - val vfpv3: bool - val hardware_idiv: bool - end +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_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 - mvn - orr - rsb - sub (but not sp - imm) - On the other hand, "mov rd, rs" and "mov rd, #imm" have shorter - encodings if they do not have the "S" flag. Moreover, the "S" - flag is not supported if rd or rs is sp. - - 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 "") - | Section_debug_info _ -> ".section .debug_info,\"\",%progbits" - | Section_debug_loc -> ".section .debug_loc,\"\",%progbits" - | Section_debug_abbrev -> ".section .debug_abbrev,\"\",%progbits" - | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" - | Section_debug_ranges -> ".section .debug_ranges,\"\",%progbits" - | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" - - let section oc sec = - fprintf oc " %s\n" (name_of_section sec) - -(* Record current code position and latest position at which to - emit float and symbol constants. *) - - let currpos = ref 0 - let size_constants = ref 0 - let max_pos_constants = ref max_int - - let distance_to_emit_constants () = - if !literals_in_code - then !max_pos_constants - (!currpos + !size_constants) - else max_int - -(* Associate labels to floating-point constants and to symbols *) - - let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t) - let float32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t) - - let label_float bf = - try - Hashtbl.find float_labels bf - 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 -> - (* Big or little-endian floats *) - let bfhi = Int64.shift_right_logical bf 32 - and bflo = Int64.logand bf 0xFFFF_FFFFL in - if Archi.big_endian - then fprintf oc ".L%d: .word 0x%Lx, 0x%Lx\n" lbl bfhi bflo - else 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 = - let o = camlint_of_coqint ofs in - if o >= -32768l && o <= 32767l && !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 +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_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 + mvn + orr + rsb + sub (but not sp - imm) + On the other hand, "mov rd, rs" and "mov rd, #imm" have shorter + encodings if they do not have the "S" flag. Moreover, the "S" + flag is not supported if rd or rs is sp. + + 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 "") + | Section_debug_info _ -> ".section .debug_info,\"\",%progbits" + | Section_debug_loc -> ".section .debug_loc,\"\",%progbits" + | Section_debug_abbrev -> ".section .debug_abbrev,\"\",%progbits" + | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" + | Section_debug_ranges -> ".section .debug_ranges,\"\",%progbits" + | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" + + let section oc sec = + fprintf oc " %s\n" (name_of_section sec) + + (* Record current code position and latest position at which to + emit float and symbol constants. *) + + let currpos = ref 0 + let size_constants = ref 0 + let max_pos_constants = ref max_int + + let distance_to_emit_constants () = + if !literals_in_code + then !max_pos_constants - (!currpos + !size_constants) + else max_int + + (* Associate labels to floating-point constants and to symbols *) + + let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t) + let float32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t) + + let label_float bf = + try + Hashtbl.find float_labels bf + 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 -> + (* Big or little-endian floats *) + let bfhi = Int64.shift_right_logical bf 32 + and bflo = Int64.logand bf 0xFFFF_FFFFL in + if Archi.big_endian + then fprintf oc ".L%d: .word 0x%Lx, 0x%Lx\n" lbl bfhi bflo + else 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 = + let o = camlint_of_coqint ofs in + if o >= -32768l && o <= 32767l && !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 -(* 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 *) + (* 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_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 + 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 *) + (* Emit .file / .loc debugging directives *) - let print_file_line oc file line = - print_file_line oc comment file line + let print_file_line oc file line = + print_file_line oc comment file line -(* Fixing up calling conventions *) + (* Fixing up calling conventions *) - type direction = Incoming | Outgoing + type direction = Incoming | Outgoing - module FixupEABI = struct + module FixupEABI = struct - let ireg_param = function - | 0 -> IR0 | 1 -> IR1 | 2 -> IR2 | 3 -> IR3 | _ -> assert false + 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 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_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 + 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' + fixup (i+1) tyl' | Tlong :: tyl' -> - fixup (((i + 1) land (-2)) + 2) 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 - if Archi.big_endian - then fixup_double oc dir (freg_param i) (ireg_param (i+1)) (ireg_param i) - else fixup_double oc dir (freg_param i) (ireg_param i) (ireg_param (i+1)); - 1 + fixup (i+2) tyl' - end + let i = (i + 1) land (-2) in + if i >= 4 then 0 else begin + if Archi.big_endian + then fixup_double oc dir (freg_param i) (ireg_param (i+1)) (ireg_param i) + else 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 + fixup_single oc dir (freg_param i) (ireg_param i); + 1 + fixup (i+1) tyl' + in fixup 0 tyl - let fixup_result oc dir sg = - fixup_conventions oc dir (proj_sig_res sg :: []) + let fixup_arguments oc dir sg = + fixup_conventions oc dir sg.sig_args - end + let fixup_result oc dir sg = + fixup_conventions oc dir (proj_sig_res sg :: []) - 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 + 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 (2*fr) = sr then n else begin - fprintf oc " vmov.f32 s%d, s%d\n" (2*fr) sr; - 1 + n - 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 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 + 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 (2*fr) = sr then n else begin + fprintf oc " vmov.f32 s%d, s%d\n" (2*fr) sr; + 1 + n 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 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_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 *) - | Padc (r1,r2,so) -> - fprintf oc " adc %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 - | 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 - | Padds (r1,r2,so) -> - fprintf oc " adds %a, %a, %a\n" 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 - | Pbne lbl -> - fprintf oc " bne %a\n" 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 - | Pclz (r1,r2) -> - fprintf oc " clz %a, %a\n" ireg r1 ireg r2; 1 - | Pcmp(r1, so) -> - fprintf oc " cmp %a, %a\n" ireg r1 shift_op so; 1 - | Pdmb -> - fprintf oc " dmb\n"; 1 - | Pdsb -> - fprintf oc " dsb\n"; 1 - | Peor(r1, r2, so) -> - fprintf oc " eor%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 - | Pisb -> - fprintf oc " isb\n"; 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 - | Pldr_p(r1, r2, sa) -> - fprintf oc " ldr %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 - | Pldrb_p(r1, r2, sa) -> - fprintf oc " ldrb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 - | Pldrh_p(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, (SOimm _ | SOreg _ as so)) -> - (* No S flag even in Thumb2 mode *) - fprintf oc " mov %a, %a\n" ireg r1 shift_op so; 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 - | Prev (r1,r2) -> - fprintf oc " rev %a, %a\n" ireg r1 ireg r2; 1 - | Prev16 (r1,r2) -> - fprintf oc " rev16 %a, %a\n" ireg r1 ireg r2; 1 - | Prsb(r1, r2, so) -> - fprintf oc " rsb%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 - | Prsbs(r1, r2, so) -> - fprintf oc " rsbs %a, %a, %a\n" - ireg r1 ireg r2 shift_op so; 1 - | Prsc (r1,r2,so) -> - fprintf oc " rsc %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 - | Pfsqrt (f1,f2) -> - fprintf oc " vsqrt.f64 %a, %a\n" freg f1 freg f2; 1 - | Psbc (r1,r2,sa) -> - fprintf oc " sbc %a, %a, %a\n" ireg r1 ireg r2 shift_op sa; 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 - | Pstr_p(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_p(r1, r2, sa) -> - fprintf oc " strb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 - | Pstrh_p(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 - | Psubs(r1, r2, so) -> - fprintf oc " subs %a, %a, %a\n" - 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, #%.15F\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 - | Ppush rl -> - let first = ref true in - let sep () = if !first then first := false else output_string oc ", " in - fprintf oc " push {%a}\n" (fun oc rl -> List.iter (fun ir -> sep (); ireg oc ir) rl) rl; ;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, #%.15F\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) -> - assert false - | Pfreeframe(sz, ofs) -> - assert false - | 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_annot(txt, targs) -> - fprintf oc "%s annotation: " comment; - print_annot_text preg "sp" oc (camlstring_of_coqstring txt) args; - 0 - | EF_debug(kind, txt, targs) -> - print_debug_info comment print_file_line preg "sp" oc - (P.to_int kind) (extern_atom txt) args; - 0 - | EF_inline_asm(txt, sg, clob) -> - fprintf oc "%s begin inline assembly\n\t" comment; - print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res; - fprintf oc "%s end inline assembly\n" comment; - 5 (* hoping this is an upper bound... *) - | _ -> - assert false - end - | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz); 0 - - let no_fallthrough = function - | Pb _ -> true - | Pbsymb _ -> true - | Pbreg _ -> true - | _ -> false + let fixup_result oc dir sg = + if sg.sig_cc.cc_vararg then + FixupEABI.fixup_result oc dir sg + else + 0 + end - 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 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_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 = - current_function_sig := fn.fn_sig; - 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 + 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 *) + | Padc (r1,r2,so) -> + fprintf oc " adc %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 + | 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 + | Padds (r1,r2,so) -> + fprintf oc " adds %a, %a, %a\n" 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 + | Pbne lbl -> + fprintf oc " bne %a\n" 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 + | Pclz (r1,r2) -> + fprintf oc " clz %a, %a\n" ireg r1 ireg r2; 1 + | Pcmp(r1, so) -> + fprintf oc " cmp %a, %a\n" ireg r1 shift_op so; 1 + | Pdmb -> + fprintf oc " dmb\n"; 1 + | Pdsb -> + fprintf oc " dsb\n"; 1 + | Peor(r1, r2, so) -> + fprintf oc " eor%t %a, %a, %a\n" + thumbS ireg r1 ireg r2 shift_op so; 1 + | Pisb -> + fprintf oc " isb\n"; 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 + | Pldr_p(r1, r2, sa) -> + fprintf oc " ldr %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + | Pldrb_p(r1, r2, sa) -> + fprintf oc " ldrb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + | Pldrh_p(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, (SOimm _ | SOreg _ as so)) -> + (* No S flag even in Thumb2 mode *) + fprintf oc " mov %a, %a\n" ireg r1 shift_op so; 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 + | Prev (r1,r2) -> + fprintf oc " rev %a, %a\n" ireg r1 ireg r2; 1 + | Prev16 (r1,r2) -> + fprintf oc " rev16 %a, %a\n" ireg r1 ireg r2; 1 + | Prsb(r1, r2, so) -> + fprintf oc " rsb%t %a, %a, %a\n" + thumbS ireg r1 ireg r2 shift_op so; 1 + | Prsbs(r1, r2, so) -> + fprintf oc " rsbs %a, %a, %a\n" + ireg r1 ireg r2 shift_op so; 1 + | Prsc (r1,r2,so) -> + fprintf oc " rsc %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 + | Pfsqrt (f1,f2) -> + fprintf oc " vsqrt.f64 %a, %a\n" freg f1 freg f2; 1 + | Psbc (r1,r2,sa) -> + fprintf oc " sbc %a, %a, %a\n" ireg r1 ireg r2 shift_op sa; 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 + | Pstr_p(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_p(r1, r2, sa) -> + fprintf oc " strb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + | Pstrh_p(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 - -(* 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_coqfloat32 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"); - if !Clflags.option_g then begin - section oc Section_text; - cfi_section oc + | 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 + | Psubs(r1, r2, so) -> + fprintf oc " subs %a, %a, %a\n" + 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 - - let print_epilogue oc = - if !Clflags.option_g then begin - Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); - section oc Section_text; + | 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, #%.15F\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 + | Ppush rl -> + let first = ref true in + let sep () = if !first then first := false else output_string oc ", " in + fprintf oc " push {%a}\n" (fun oc rl -> List.iter (fun ir -> sep (); ireg oc ir) rl) rl; ;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, #%.15F\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) -> + assert false + | Pfreeframe(sz, ofs) -> + assert false + | 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_annot(txt, targs) -> + fprintf oc "%s annotation: " comment; + print_annot_text preg "sp" oc (camlstring_of_coqstring txt) args; + 0 + | EF_debug(kind, txt, targs) -> + print_debug_info comment print_file_line preg "sp" oc + (P.to_int kind) (extern_atom txt) args; + 0 + | EF_inline_asm(txt, sg, clob) -> + fprintf oc "%s begin inline assembly\n\t" comment; + print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res; + fprintf oc "%s end inline assembly\n" comment; + 256 (* Better be safe than sorry *) + | _ -> + assert false + end + | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz); 0 + + let no_fallthrough = function + | Pb _ -> true + | Pbsymb _ -> true + | Pbreg _ -> true + | _ -> false + + let estimate_size = function + | Pbtbl (_,tbl) -> + let len = List.length tbl in + let add =if !Clflags.option_mthumb then + 3 + else + 2 in + (len + add) * 4 + | Pbuiltin (EF_inline_asm _,_,_) -> 1024 (* Better be safe than sorry *) + | _ -> 12 + + + let rec print_instructions oc no_fall instrs = + match instrs with + | [] -> () + | i :: il -> + let d = distance_to_emit_constants() - estimate_size i in + if d < 256 && no_fall 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; + let n = print_instruction oc i in + currpos := !currpos + n * 4; + print_instructions oc (no_fallthrough i) 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 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_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 = + current_function_sig := fn.fn_sig; + ignore (fixup_arguments oc Incoming fn.fn_sig); + print_instructions oc false 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 - let default_falignment = 4 + (* 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_coqfloat32 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"); + if !Clflags.option_g then begin + section oc Section_text; + cfi_section oc + end - let label = elf_label + let print_epilogue oc = + if !Clflags.option_g then begin + Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); + section oc Section_text; + end - let new_label = new_label + let default_falignment = 4 - let address = if Archi.ptr64 then ".quad" else ".4byte" - end + let label = elf_label + + let new_label = new_label + + let address = if Archi.ptr64 then ".quad" else ".4byte" +end let sel_target () = let module S : PRINTER_OPTIONS = struct - let vfpv3 = Configuration.model >= "armv7" + let vfpv3 = Configuration.model >= "armv7" - let float_abi = match Configuration.abi with - | "eabi" -> Soft - | "hardfloat" -> Hard - | _ -> assert false + 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 + let hardware_idiv = + match Configuration.model with + | "armv7r" | "armv7m" -> !Clflags.option_mthumb + | _ -> false - end in + end in (module Target(S):TARGET) diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index 562d8e89..612980f1 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -71,6 +71,7 @@ type warning_type = | Literal_range | Unknown_pragmas | CompCert_conformance + | Inline_asm_sdump let active_warnings: warning_type list ref = ref [ Unnamed; @@ -89,6 +90,7 @@ let active_warnings: warning_type list ref = ref [ Invalid_noreturn; Return_type; Literal_range; + Inline_asm_sdump; ] let error_warnings: warning_type list ref = ref [] @@ -113,6 +115,7 @@ let string_of_warning = function | Literal_range -> "literal-range" | Unknown_pragmas -> "unknown-pragmas" | CompCert_conformance -> "compcert-conformance" + | Inline_asm_sdump -> "inline-asm-sdump" let activate_warning w () = if not (List.mem w !active_warnings) then @@ -151,6 +154,7 @@ let wall () = Literal_range; Unknown_pragmas; CompCert_conformance; + Inline_asm_sdump; ] let werror () = @@ -173,6 +177,7 @@ let werror () = Return_type; Literal_range; Unknown_pragmas; + Inline_asm_sdump; ] @@ -294,6 +299,7 @@ let warning_options = error_option Literal_range @ error_option Unknown_pragmas @ error_option CompCert_conformance @ + error_option Inline_asm_sdump @ [Exact ("-Wfatal-errors"), Set error_fatal; Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *) Exact ("-fno-diagnostics-color"), Unset color_diagnostics; diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli index 56894c87..8501cfa0 100644 --- a/cparser/Cerrors.mli +++ b/cparser/Cerrors.mli @@ -44,6 +44,7 @@ type warning_type = | Literal_range (** literal ranges *) | Unknown_pragmas (** unknown/unsupported pragma *) | CompCert_conformance (** features that are not part of the CompCert C core language *) + | Inline_asm_sdump (** inline assembler used in combination of sdump *) val warning : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a (** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to diff --git a/doc/ccomp.1 b/doc/ccomp.1 index 88af8612..bb5a486e 100644 --- a/doc/ccomp.1 +++ b/doc/ccomp.1 @@ -405,6 +405,10 @@ Enabled by default. \fIzero\-length\-array\fP: GNU extension for zero length arrays. Disabled by default. +.sp +\fIinline\-asm\-sdump\fP: +Use of unsupported features in combination with dump of abstract syntax tree. +Enabled by default. . .TP .B \-Wno-<warning> diff --git a/driver/Driver.ml b/driver/Driver.ml index 145de6c5..e3b9ec52 100644..100755 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -348,6 +348,13 @@ let print_usage_and_exit () = let print_version_and_exit () = printf "%s" version_string; exit 0 +let enforce_buildnr nr = + let build = int_of_string Version.buildnr in + if nr != build then begin + eprintf "Mismatching builds: This is CompCert build %d, but QSK requires build %d.\n\ +Please use matching builds of QSK and CompCert.\n" build nr; exit 2 + end + let language_support_options = [ option_fbitfields; option_flongdouble; option_fstruct_passing; option_fvararg_calls; option_funprototyped; @@ -374,9 +381,14 @@ let cmdline_actions = Exact "--help", Unit print_usage_and_exit; (* Getting version info *) Exact "-version", Unit print_version_and_exit; - Exact "--version", Unit print_version_and_exit; + Exact "--version", Unit print_version_and_exit;] @ +(* Enforcing CompCert build numbers for QSKs *) + (if Version.buildnr <> "" then + [ Exact "-qsk-enforce-build", Integer enforce_buildnr; + Exact "--qsk-enforce-build", Integer enforce_buildnr; ] + else []) @ (* Processing options *) - Exact "-c", Set option_c; + [ Exact "-c", Set option_c; Exact "-E", Set option_E; Exact "-S", Set option_S; Exact "-o", String(fun s -> option_o := Some s); @@ -537,5 +549,6 @@ let _ = if (not nolink) && linker_args <> [] then begin linker (output_filename_default "a.out") linker_args end; + if Cerrors.check_errors () then exit 2 with Sys_error msg -> eprintf "I/O error: %s.\n" msg; exit 2 diff --git a/lib/BoolEqual.v b/lib/BoolEqual.v new file mode 100644 index 00000000..a5b543e1 --- /dev/null +++ b/lib/BoolEqual.v @@ -0,0 +1,167 @@ +(* *********************************************************************) +(* *) +(* 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 GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Tactics to generate Boolean-valued equalities *) + +(** The [decide equality] tactic can generate a term of type +[forall (x y: A), {x=y} + {x<>y}] if [A] is an inductive type. +This term is a decidable equality function. + +Similarly, this module defines a [boolean_equality] tactic that generates +a term of type [A -> A -> bool]. This term is a Boolean-valued equality +function over the inductive type [A]. Two internal tactics generate +proofs that show the correctness of this equality function [f], namely +proofs of the following two properties: +- [forall (x: A), f x x = true] +- [forall (x y: A), f x y = true -> x = y] + +Finally, the [decide_equality_from f] tactic wraps [f] (the Boolean equality +generated by [boolean_equality]) and those proofs together, producing +a decidable equality of type [forall (x y: A), {x=y} + {x<>y}]. + +The advantage of the present tactics over the standard [decide equality] +tactic is that the former produce smaller transparent definitions than +the latter. + +For a type [A] that has N constructors, [decide equality] produces a +single term of size O(N^3), which must be kept transparent so that +it computes and extracts as expected. Given such a big transparent +definition, the virtual machine compiler of Coq produces very big +chunks of VM code, causing memory overflows on 32-bit platforms. + +In contrast, the term produced by [boolean_equality] has size O(N^2) +only (so to speak). The proofs that this term is a correct boolean +equality are still O(N^3), but those proofs are opaque and do not need +to be compiled to VM code. Only the boolean equality itself is defined +transparently and compiled. + +The present tactics also have some restrictions: +- Constructors must have at most 4 arguments. +- Decidable equalities must be provided (as hypotheses in the context) + for all the types [T] of constructor arguments other than type [A]. +- They probably do not work for mutually-defined inductive types. +*) + +Require Import Coqlib. + +Module BE. + +Definition bool_eq {A: Type} (x y: A) : Type := bool. + +Ltac bool_eq_base x y := + change (bool_eq x y); + match goal with + | [ H: forall (x y: ?A), bool |- @bool_eq ?A x y ] => exact (H x y) + | [ H: forall (x y: ?A), {x=y} + {x<>y} |- @bool_eq ?A x y ] => exact (proj_sumbool (H x y)) + | _ => idtac + end. + +Ltac bool_eq_case := + match goal with + | |- bool_eq (?C ?x1 ?x2 ?x3 ?x4) (?C ?y1 ?y2 ?y3 ?y4) => + refine (_ && _ && _ && _); [bool_eq_base x1 y1|bool_eq_base x2 y2|bool_eq_base x3 y3|bool_eq_base x4 y4] + | |- bool_eq (?C ?x1 ?x2 ?x3) (?C ?y1 ?y2 ?y3) => + refine (_ && _ && _); [bool_eq_base x1 y1|bool_eq_base x2 y2|bool_eq_base x3 y3] + | |- bool_eq (?C ?x1 ?x2) (?C ?y1 ?y2) => + refine (_ && _); [bool_eq_base x1 y1|bool_eq_base x2 y2] + | |- bool_eq (?C ?x1) (?C ?y1) => bool_eq_base x1 y1 + | |- bool_eq ?C ?C => exact true + | |- bool_eq _ _ => exact false + end. + +Ltac bool_eq := + match goal with + | [ |- ?A -> ?A -> bool ] => + let f := fresh "rec" in let x := fresh "x" in let y := fresh "y" in + fix f 1; intros x y; change (bool_eq x y); destruct x, y; bool_eq_case + | [ |- _ -> _ ] => + let eq := fresh "eq" in intro eq; bool_eq + end. + +Lemma proj_sumbool_is_true: + forall (A: Type) (f: forall (x y: A), {x=y} + {x<>y}) (x: A), + proj_sumbool (f x x) = true. +Proof. + intros. unfold proj_sumbool. destruct (f x x). auto. elim n; auto. +Qed. + +Ltac bool_eq_refl_case := + match goal with + | [ |- true = true ] => reflexivity + | [ |- proj_sumbool _ = true ] => apply proj_sumbool_is_true + | [ |- _ && _ = true ] => apply andb_true_iff; split; bool_eq_refl_case + | _ => auto + end. + +Ltac bool_eq_refl := + let H := fresh "Hrec" in let x := fresh "x" in + fix H 1; intros x; destruct x; simpl; bool_eq_refl_case. + +Lemma false_not_true: + forall (P: Prop), false = true -> P. +Proof. + intros. discriminate. +Qed. + +Lemma proj_sumbool_true: + forall (A: Type) (x y: A) (a: {x=y} + {x<>y}), + proj_sumbool a = true -> x = y. +Proof. + intros. destruct a. auto. discriminate. +Qed. + +Ltac bool_eq_sound_case := + match goal with + | [ H: false = true |- _ ] => exact (false_not_true _ H) + | [ H: _ && _ = true |- _ ] => apply andb_prop in H; destruct H; bool_eq_sound_case + | [ H: proj_sumbool ?a = true |- _ ] => apply proj_sumbool_true in H; bool_eq_sound_case + | [ |- ?C ?x1 ?x2 ?x3 ?x4 = ?C ?y1 ?y2 ?y3 ?y4 ] => apply f_equal4; auto + | [ |- ?C ?x1 ?x2 ?x3 = ?C ?y1 ?y2 ?y3 ] => apply f_equal3; auto + | [ |- ?C ?x1 ?x2 = ?C ?y1 ?y2 ] => apply f_equal2; auto + | [ |- ?C ?x1 = ?C ?y1 ] => apply f_equal; auto + | [ |- ?x = ?x ] => reflexivity + | _ => idtac + end. + +Ltac bool_eq_sound := + let Hrec := fresh "Hrec" in let x := fresh "x" in let y := fresh "y" in + fix Hrec 1; intros x y; destruct x, y; simpl; intro; bool_eq_sound_case. + +Lemma dec_eq_from_bool_eq: + forall (A: Type) (f: A -> A -> bool) + (f_refl: forall x, f x x = true) (f_sound: forall x y, f x y = true -> x = y), + forall (x y: A), {x=y} + {x<>y}. +Proof. + intros. destruct (f x y) eqn:E. + left. apply f_sound. auto. + right; red; intros. subst y. rewrite f_refl in E. discriminate. +Defined. + +End BE. + +(** Applied to a goal of the form [t -> t -> bool], the [boolean_equality] + tactic defines a function with that type, returning [true] iff the two + arguments of type [t] are equal. [t] must be an inductive type. + For any type [u] other than [t] that appears in arguments of constructors + of [t], a decidable equality over [u] must be provided, as an hypothesis + of type [forall (x y: u), {x=y}+{x<>y}]. *) +Ltac boolean_equality := BE.bool_eq. + +(** Given a function [beq] of type [t -> t -> bool] produced by [boolean_equality], + the [decidable_equality_from beq] produces a decidable equality with type + [forall (x y: t], {x=y}+{x<>y}. *) + +Ltac decidable_equality_from beq := + apply (BE.dec_eq_from_bool_eq _ beq); [abstract BE.bool_eq_refl|abstract BE.bool_eq_sound]. diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index f0000035..5304b967 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -264,7 +264,12 @@ let p_instruction oc ic = | Pxori (ir1,ir2,c) ->instruction "Pxori" [Ireg ir1; Ireg ir2; Constant c] | Pxoris (ir1,ir2,c) -> instruction "Pxoris" [Ireg ir1; Ireg ir2; Constant c] | Plabel l -> instruction "Plabel" [ALabel l] - | Pbuiltin _ -> () + | Pbuiltin (ef,_,_) -> + begin match ef with + | EF_inline_asm _ -> + Cerrors.warning ("",-10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump" + | _ -> () + end | Pcfi_adjust _ (* Only debug relevant *) | Pcfi_rel_offset _ -> () (* Only debug relevant *) in List.iter instruction ic @@ -23,7 +23,7 @@ For a processor-independent set of operations, see the abstract syntax and dynamic semantics of the Cminor language. *) - +Require Import BoolEqual. Require Import Coqlib. Require Import AST. Require Import Integers. @@ -184,14 +184,14 @@ Proof. decide equality. Defined. -Definition eq_operation (x y: operation): {x=y} + {x<>y}. +Definition beq_operation: forall (x y: operation), bool. Proof. - generalize Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec; intros. - decide equality. - apply ident_eq. - apply eq_addressing. - apply eq_addressing. - apply eq_condition. + generalize Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_addressing eq_condition; boolean_equality. +Defined. + +Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}. +Proof. + decidable_equality_from beq_operation. Defined. Global Opaque eq_condition eq_addressing eq_operation. |