From cdf6681b3450baa1489c6a62e1903a450c0e2c3f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 14 Dec 2017 22:40:57 +0100 Subject: Moved constant expansion into Asmexpand. (#40) This commit introduces a new pass which is run after the expansion of the builtin functions which performs the expansion and placement of constants inside the function code. --- arm/Asm.v | 25 ++- arm/AsmToJSON.ml | 39 +++-- arm/Asmexpand.ml | 4 +- arm/Constantexpand.ml | 197 +++++++++++++++++++++ arm/TargetPrinter.ml | 472 ++++++++++++++++++-------------------------------- 5 files changed, 419 insertions(+), 318 deletions(-) create mode 100644 arm/Constantexpand.ml (limited to 'arm') diff --git a/arm/Asm.v b/arm/Asm.v index 613f027b..c05ec3e9 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -130,6 +130,11 @@ Inductive testcond : Type := | TCgt: testcond (**r signed greater *) | TCle: testcond. (**r signed less than or equal *) +Inductive code_constant: Type := +| Float32 : label -> float32 -> code_constant +| Float64 : label -> float -> code_constant +| Symbol : label -> ident -> ptrofs -> code_constant. + Inductive instruction : Type := (* Core instructions *) | Padd: ireg -> ireg -> shift_op -> instruction (**r integer addition *) @@ -246,8 +251,16 @@ Inductive instruction : Type := | Pfcpy_fii: freg -> ireg -> ireg -> instruction (**r copy integer register pair to double fp-register *) | Pfcpy_fi: freg -> ireg -> instruction (**r copy integer register to single fp-register *) | Pfcpy_iif: ireg -> ireg -> freg -> instruction (**r copy double fp-register to integer register pair *) - | Pfcpy_if: ireg -> freg -> instruction. (**r copy single fp-register to integer register *) + | Pfcpy_if: ireg -> freg -> instruction (**r copy single fp-register to integer register *) + (* Instructions for the emitting of constants *) + | Pconstants: list code_constant -> instruction (**r constants in code*) + | Ploadsymbol_imm: ireg -> ident -> ptrofs -> instruction (**r move symbol address in register *) + | Pflid_lbl: freg -> label -> float -> instruction (**r load float64 from label *) + | Pflis_lbl: freg -> label -> float32 -> instruction (**r load float32 from label *) + | Pflid_imm: freg -> float -> instruction (**r move float64 into register *) + | Pflis_imm: freg -> float32 -> instruction (**r move float32 into register *) + | Ploadsymbol_lbl: ireg -> label -> ident -> ptrofs -> instruction. (**r load symbol address from label *) (** The pseudo-instructions are the following: @@ -807,7 +820,15 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfcpy_fii _ _ _ | Pfcpy_fi _ _ | Pfcpy_iif _ _ _ - | Pfcpy_if _ _ => + | Pfcpy_if _ _ + | Pconstants _ + | Ploadsymbol_imm _ _ _ + | Pflid_lbl _ _ _ + | Pflis_lbl _ _ _ + | Pflid_imm _ _ + | Pflis_imm _ _ + | Ploadsymbol_lbl _ _ _ _ + => Stuck end. diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml index 2627f29b..e105ea20 100644 --- a/arm/AsmToJSON.ml +++ b/arm/AsmToJSON.ml @@ -20,24 +20,26 @@ open Camlcoq open Json let mnemonic_names = [ "Padc"; "Padd"; "Padds"; "Pand";"Pannot"; "Pasr"; "Pb"; "Pbc"; "Pbic"; "Pblreg"; - "Pblsymb"; "Pbne"; "Pbreg"; "Pbsymb"; "Pbtbl"; "Pclz"; "Pcmp"; "Pfcpy_iif"; - "Pfcpy_fii"; "Pfcpy_fi"; "Pfcpy_sf"; "Pdmb"; "Pdsb"; "Peor"; "Pfabsd"; + "Pblsymb"; "Pbne"; "Pbreg"; "Pbsymb"; "Pbtbl"; "Pclz"; "Pcmp"; "Pconstants";"Pfcpy_iif"; + "Pfcpy_fii"; "Pfcpy_fi"; "Pfcpy_sf"; "Pflid_lbl"; "Pflis_lbl"; "Pdmb"; "Pdsb"; "Peor"; "Pfabsd"; "Pfabss"; "Pfaddd"; "Pfadds"; "Pfcmpd"; "Pfcmps"; "Pfcmpzd"; "Pfcmpzs"; "Pfcpyd"; "Pfcpy_fs"; "Pfcpy_if";"Pfcvtds"; "Pfcvtsd"; "Pfdivd"; "Pfdivs"; "Pfldd"; - "Pfldd_a"; "Pflds"; "Pflid"; "Pflis"; "Pfmuld"; "Pfmuls"; "Pfnegd"; + "Pfldd_a"; "Pflid"; "Pflds"; "Pflid_imm"; "Pflis_imm"; "Pfmuld"; "Pfmuls"; "Pfnegd"; "Pfnegs"; "Pfreeframe"; "Pfsitod"; "Pfsitos"; "Pfsqrt"; "Pfstd"; "Pfstd_a"; "Pfsts"; "Pfsubd"; "Pfsubs"; "Pftosizd"; "Pftosizs"; "Pftouizd"; "Pftouizs"; "Pfuitod"; "Pfuitos"; "Pinlineasm"; "Pisb"; "Plabel"; "Pldr"; - "Pldr_a"; "Pldr_p"; "Pldrb"; "Pldrb_p"; "Pldrh"; "Pldrh_p"; "Pldrsb"; - "Pldrsh"; "Ploadsymbol"; "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite"; - "Pmovt"; "Pmovw"; "Pmul"; "Pmvn"; "Porr"; "Ppush"; "Prev"; "Prev16"; "Prsb"; - "Prsbs"; "Prsc"; "Psbc"; "Psbfx"; "Psdiv"; "Psmull"; "Pstr"; "Pstr_a"; - "Pstr_p"; "Pstrb"; "Pstrb_p"; "Pstrh"; "Pstrh_p"; "Psub"; "Psubs"; "Pudiv"; + "Pldr_a"; "Ploadsymbol_lbl"; "Pldr_p"; "Pldrb"; "Pldrb_p"; "Pldrh"; "Pldrh_p"; "Pldrsb"; + "Pldrsh"; "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite"; + "Pmovt"; "Pmovw"; "Pmul"; "Pmvn"; "Ploadsymbol_imm"; "Porr"; + "Ppush"; "Prev"; "Prev16"; "Prsb"; "Prsbs"; "Prsc"; "Psbc"; "Psbfx"; "Psdiv"; "Psmull"; + "Pstr"; "Pstr_a"; "Pstr_p"; "Pstrb"; "Pstrb_p"; "Pstrh"; "Pstrh_p"; "Psub"; "Psubs"; "Pudiv"; "Pumull" ] type instruction_arg = | ALabel of positive | Atom of positive + | Data32 of Integers.Int.int + | Data64 of Integers.Int64.int | DFreg of freg | Float32 of Floats.float32 | Float64 of Floats.float @@ -51,6 +53,12 @@ type instruction_arg = | Symbol of ident * BinNums.coq_Z | Condition of string +let makedata (c : code_constant) : instruction_arg = + match c with + | Asm.Float32(_, f) -> Data32 (Floats.Float32.to_bits f) + | Asm.Float64(_, f) -> Data64 (Floats.Float.to_bits f) + | Asm.Symbol(_, id, ofs) -> Symbol(id, ofs) + let pp_reg pp reg = pp_jsingle_object pp "Register" pp_jstring reg @@ -104,6 +112,8 @@ let pp_symbol pp (id, ofs) = let pp_arg pp = function | ALabel lbl -> pp_label pp lbl | Atom a -> pp_atom_constant pp a + | Data32 i -> pp_jsingle_object pp "Data32" pp_int i + | Data64 i -> pp_jsingle_object pp "Data64" pp_int64 i | DFreg fr -> pp_freg pp fr | Float32 f -> pp_float32_constant pp f | Float64 f -> pp_float64_constant pp f @@ -177,6 +187,9 @@ let pp_instructions pp ic = (* Call Frame Information, only debug relevant and not exported *) | Pcfi_adjust _ -> assert false | Pcfi_rel_offset _ -> assert false + (* Should be eliminated in constant expansion step *) + | Pflis(r1, f) -> assert false + | Ploadsymbol(r1, id, ofs) -> assert false (* ARM instructions *) | Padc(r1, r2, so) -> instruction pp "Padc" [Ireg r1; Ireg r2; Shift so] | Padd(r1, r2, so) -> instruction pp "Padd" [Ireg r1; Ireg r2; Shift so] @@ -213,7 +226,6 @@ let pp_instructions pp ic = | Pfldd(r1, r2, n) | Pfldd_a(r1, r2, n) -> instruction pp "Pfldd" [DFreg r1; Ireg r2; Long n] | Pflds(r1, r2, n) -> instruction pp "Pflds" [SFreg r1; Ireg r2; Long n] | Pflid(r1, f) -> instruction pp "Pflid" [DFreg r1; Float64 f] - | Pflis(r1, f) -> instruction pp "Pflis" [SFreg r1; Float32 f] | Pfmuld(r1, r2, r3) -> instruction pp "Pfmuld" [DFreg r1; DFreg r2; DFreg r3] | Pfmuls(r1, r2, r3) -> instruction pp "Pfmuls" [SFreg r1; SFreg r2; SFreg r3] | Pfnegd(r1, r2) -> instruction pp "Pfnegd" [DFreg r1; DFreg r2] @@ -241,7 +253,6 @@ let pp_instructions pp ic = | Pldrh_p(r1, r2, so) -> instruction pp "Pldrh_p" [Ireg r1; Ireg r2; Shift so] | Pldrsb(r1, r2, so) -> instruction pp "Pldrsb" [Ireg r1; Ireg r2; Shift so] | Pldrsh(r1, r2, so) -> instruction pp "Pldrsh" [Ireg r1; Ireg r2; Shift so] - | Ploadsymbol(r1, id, ofs) -> instruction pp "Ploadsymbol" [Ireg r1; Symbol (id, ofs)] | Plsl(r1, r2, r3) -> instruction pp "Plsl" [Ireg r1; Ireg r2; Ireg r3] | Plsr(r1, r2, r3) -> instruction pp "Plsr" [Ireg r1; Ireg r2; Ireg r3] | Pmla(r1, r2, r3, r4) -> instruction pp "Pmla" [Ireg r1; Ireg r2; Ireg r3; Ireg r4] @@ -279,6 +290,14 @@ let pp_instructions pp ic = | Pfcpy_fi(r1, r2) -> instruction pp "Pfcpy_fi" [SFreg r1; Ireg r2] | Pfcpy_iif(r1, r2, r3) -> instruction pp "Pfcpy_iif" [Ireg r1; Ireg r2; DFreg r3] | Pfcpy_if (r1,r2) -> instruction pp "Pfcpy_if" [Ireg r1; SFreg r2] + (* Pseudo instructions from constant expansion step *) + | Pconstants consts -> instruction pp "Pconstants" (List.map makedata consts) + | Ploadsymbol_imm (r1,id,ofs) -> instruction pp "Ploadsymbol_imm" [Ireg r1; Symbol (id,ofs)] + | Pflid_lbl (r1,lbl,f) -> instruction pp "Pflid_lbl" [DFreg r1; ALabel lbl; Float64 f] + | Pflis_lbl (r1,lbl,f) -> instruction pp "Pflis_lbl" [SFreg r1; ALabel lbl; Float32 f] + | Pflid_imm (r1,f) -> instruction pp "Pflid_imm" [DFreg r1; Float64 f] + | Pflis_imm (r1,f) -> instruction pp "Pflis_imm" [SFreg r1; Float32 f] + | Ploadsymbol_lbl (r1,lbl,id,ofs) -> instruction pp "Ploadsymbol_lbl" [Ireg r1; ALabel lbl; Symbol (id,ofs)] in pp_jarray instruction pp ic diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 6c6b4a11..7c18be6b 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -669,7 +669,9 @@ let expand_function id fn = expand_debug id 13 preg_to_dwarf expand_instruction fn.fn_code else List.iter expand_instruction fn.fn_code; - Errors.OK (get_current_function ()) + let fn = get_current_function () in + let fn = Constantexpand.expand_constants fn in + Errors.OK fn with Error s -> Errors.Error (Errors.msg (coqstring_of_camlstring s)) diff --git a/arm/Constantexpand.ml b/arm/Constantexpand.ml new file mode 100644 index 00000000..408b291e --- /dev/null +++ b/arm/Constantexpand.ml @@ -0,0 +1,197 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open Asm +open Asmexpandaux +open AST + open Camlcoq +(* open Integers *) + +let _0 = Integers.Int.zero + +(* Options controlling the output of the constants *) + +let literals_in_code = ref true (* to be turned into a proper option *) + +let vfpv3 = Configuration.model >= "armv7" + + +(* 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 : (Floats.float, label) Hashtbl.t) +let float32_labels = (Hashtbl.create 39 : (Floats.float32, label) Hashtbl.t) +let symbol_labels = + (Hashtbl.create 39 : (ident * Integers.Int.int, label) Hashtbl.t) + +let get_label tbl sz pinc bf = + try + Hashtbl.find tbl bf + with Not_found -> + let lbl' = new_label () in + Hashtbl.add tbl bf lbl'; + size_constants := !size_constants + sz; + max_pos_constants := min !max_pos_constants (!currpos + pinc); + lbl' + +let label_float = get_label float_labels 8 1024 +let label_float32 = get_label float32_labels 4 1024 +let label_symbol id ofs = get_label symbol_labels 4 4096 (id,ofs) + +let reset_constants () = + Hashtbl.clear float_labels; + Hashtbl.clear float32_labels; + Hashtbl.clear symbol_labels; + size_constants := 0; + max_pos_constants := max_int + + +(* 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 + +let no_fallthrough = function + | Pb _ -> true + | Pbsymb _ -> true + | Pbreg _ -> true + | _ -> false + +let estimate_size = function + | Pflid _ + | Pflis _ -> 3 + | Pfcmpd _ + | Pfcmpzd _ + | Pfsitod _ + | Pfuitod _ + | Pftosizd _ + | Pftouizd _ + | Pfcmps _ + | Pfcmpzs _ + | Pfsitos _ + | Pfuitos _ + | Pftosizs _ + | Pftouizs _ + | Pmovite _ -> 2 + | Pbuiltin (ef,_,_) -> + begin match ef with + | EF_inline_asm _ -> 256 + | _ -> 0 end + | Pcfi_adjust _ + | Pcfi_rel_offset _ + | Plabel _ -> 0 + | Pbtbl (r,tbl) -> 2 + List.length tbl + | _ -> 1 + +let expand_constants () = + let consts = Hashtbl.fold (fun bf lbl c -> + Float64 (lbl, bf)::c) + float_labels [] in + let consts = Hashtbl.fold (fun bf lbl c -> + Float32 (lbl, bf)::c) + float32_labels consts in + let consts = Hashtbl.fold (fun (id,ofs) lbl c -> + Symbol (lbl,id,ofs)::c) + symbol_labels consts in + if consts <> [] then + emit (Pconstants consts); + reset_constants () + +let expand_instruction = function + | Pflid (r1,f) -> + let f' = camlint64_of_coqint(Floats.Float.to_bits f) in + if vfpv3 && is_immediate_float64 f' then begin + emit (Pflid_imm (r1,f)); + 1 + end else if !literals_in_code then begin + let lbl = label_float f in + emit (Pflid_lbl (r1,lbl,f)); + 1 + end else begin + emit (Pflid (r1,f)); + 3 + end + | Pflis (r1,f) -> + let f' = camlint_of_coqint(Floats.Float32.to_bits f) in + if vfpv3 && is_immediate_float32 f' then begin + emit (Pflis_imm (r1,f)); + 1 + end else if !literals_in_code then begin + let lbl = label_float32 f in + emit (Pflis_lbl (r1,lbl,f)); + 1 + end else begin + let lo = coqint_of_camlint (Int32.logand f' 0xFFFFl) + and hi = coqint_of_camlint (Int32.shift_right_logical f' 16) in + emit (Pmovw (IR14,lo)); + emit (Pmovt (IR14,hi)); + emit (Pfcpy_fi (r1,IR14)); + 3 + end + | Ploadsymbol(r1, id, ofs) -> + let o = camlint_of_coqint ofs in + if o >= -32768l && o <= 32767l && !Clflags.option_mthumb then begin + emit (Ploadsymbol_imm (r1,id,ofs)); + 2 + end else begin + let lbl = label_symbol id ofs in + emit (Ploadsymbol_lbl (r1,lbl,id,ofs)); + 1 + end + | inst -> + emit inst; + estimate_size inst + +let rec expand_instructions no_fall = function + | [] -> () + | i :: il -> + let estimate = estimate_size i * 4 in + let d = distance_to_emit_constants() - estimate in + if d < 256 && no_fall then + expand_constants () + else if d < 16 then begin + let lbl = new_label () in + emit (Pb lbl); + expand_constants (); + emit (Plabel lbl) + end; + let n = expand_instruction i in + currpos := !currpos + n * 4; + expand_instructions (no_fallthrough i) il + +let expand_constants fn = + reset_constants (); + set_current_function fn; + expand_instructions false fn.fn_code; + expand_constants (); + get_current_function () diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index ebaaf50e..93733f56 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -95,9 +95,6 @@ let neg_condition_name = function 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 *) @@ -171,115 +168,6 @@ struct 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 *) - - 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 = @@ -288,6 +176,24 @@ struct (* Printing of instructions *) + let print_literal64 oc n lbl = + let bfhi = Int64.shift_right_logical n 32 + and bflo = Int64.logand n 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 + + let print_constants oc = function + | Float32 (lbl,c) -> + let c = camlint_of_coqint (Floats.Float32.to_bits c) in + fprintf oc "%a: .word 0x%lx\n" print_label lbl c + | Float64 (lbl,bf) -> + let bf = camlint64_of_coqint (Floats.Float.to_bits bf) + and lbl = transl_label lbl in + print_literal64 oc bf lbl + | Symbol (lbl,id,ofs) -> + fprintf oc "%a: .word %a\n" print_label lbl symbol_offset (id, ofs) + let shift_op oc = function | SOimm n -> fprintf oc "#%a" coqint n | SOreg r -> ireg oc r @@ -299,286 +205,254 @@ struct 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 + fprintf oc " adc %a, %a, %a\n" ireg r1 ireg r2 shift_op so | 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 + ireg r1 ireg r2 shift_op so | Padds (r1,r2,so) -> - fprintf oc " adds %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 + fprintf oc " adds %a, %a, %a\n" ireg r1 ireg r2 shift_op so | Pand(r1, r2, so) -> fprintf oc " and%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 + thumbS ireg r1 ireg r2 shift_op so | Pasr(r1, r2, r3) -> fprintf oc " asr%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 ireg r3; 1 + thumbS ireg r1 ireg r2 ireg r3 | Pb lbl -> - fprintf oc " b %a\n" print_label lbl; 1 + fprintf oc " b %a\n" print_label lbl | Pbc(bit, lbl) -> - fprintf oc " b%s %a\n" (condition_name bit) print_label lbl; 1 + fprintf oc " b%s %a\n" (condition_name bit) print_label lbl | Pbne lbl -> - fprintf oc " bne %a\n" print_label lbl; 1 + fprintf oc " bne %a\n" print_label lbl | Pbsymb(id, sg) -> - fprintf oc " b %a\n" symbol id; 1 + fprintf oc " b %a\n" symbol id | Pbreg(r, sg) -> - fprintf oc " bx %a\n" ireg r; 1 + fprintf oc " bx %a\n" ireg r | Pblsymb(id, sg) -> - fprintf oc " bl %a\n" symbol id; 1 + fprintf oc " bl %a\n" symbol id | Pblreg(r, sg) -> - fprintf oc " blx %a\n" ireg r; 1 + fprintf oc " blx %a\n" ireg r | Pbic(r1, r2, so) -> fprintf oc " bic%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 + thumbS ireg r1 ireg r2 shift_op so | Pclz (r1,r2) -> - fprintf oc " clz %a, %a\n" ireg r1 ireg r2; 1 + fprintf oc " clz %a, %a\n" ireg r1 ireg r2 | Pcmp(r1, so) -> - fprintf oc " cmp %a, %a\n" ireg r1 shift_op so; 1 + fprintf oc " cmp %a, %a\n" ireg r1 shift_op so | Pdmb -> - fprintf oc " dmb\n"; 1 + fprintf oc " dmb\n" | Pdsb -> - fprintf oc " dsb\n"; 1 + fprintf oc " dsb\n" | Peor(r1, r2, so) -> fprintf oc " eor%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 + thumbS ireg r1 ireg r2 shift_op so | Pisb -> - fprintf oc " isb\n"; 1 + fprintf oc " isb\n" | Pldr(r1, r2, sa) | Pldr_a(r1, r2, sa) -> - fprintf oc " ldr %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " ldr %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa | Pldrb(r1, r2, sa) -> - fprintf oc " ldrb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " ldrb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa | Pldrh(r1, r2, sa) -> - fprintf oc " ldrh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " ldrh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa | Pldr_p(r1, r2, sa) -> - fprintf oc " ldr %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " ldr %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa | Pldrb_p(r1, r2, sa) -> - fprintf oc " ldrb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " ldrb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa | Pldrh_p(r1, r2, sa) -> - fprintf oc " ldrh %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " ldrh %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa | Pldrsb(r1, r2, sa) -> - fprintf oc " ldrsb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " ldrsb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa | Pldrsh(r1, r2, sa) -> - fprintf oc " ldrsh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " ldrsh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa | Plsl(r1, r2, r3) -> fprintf oc " lsl%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 ireg r3; 1 + thumbS ireg r1 ireg r2 ireg r3 | Plsr(r1, r2, r3) -> fprintf oc " lsr%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 ireg r3; 1 + thumbS ireg r1 ireg r2 ireg r3 | Pmla(r1, r2, r3, r4) -> - fprintf oc " mla %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 + fprintf oc " mla %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4 | 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 + fprintf oc " mov %a, %a\n" ireg r1 shift_op so | Pmov(r1, so) -> - fprintf oc " mov%t %a, %a\n" thumbS ireg r1 shift_op so; 1 + fprintf oc " mov%t %a, %a\n" thumbS ireg r1 shift_op so | Pmovw(r1, n) -> - fprintf oc " movw %a, #%a\n" ireg r1 coqint n; 1 + fprintf oc " movw %a, #%a\n" ireg r1 coqint n | Pmovt(r1, n) -> - fprintf oc " movt %a, #%a\n" ireg r1 coqint n; 1 + fprintf oc " movt %a, #%a\n" ireg r1 coqint n | Pmul(r1, r2, r3) -> - fprintf oc " mul %a, %a, %a\n" ireg r1 ireg r2 ireg r3; 1 + fprintf oc " mul %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pmvn(r1, so) -> - fprintf oc " mvn%t %a, %a\n" thumbS ireg r1 shift_op so; 1 + fprintf oc " mvn%t %a, %a\n" thumbS ireg r1 shift_op so | Porr(r1, r2, so) -> fprintf oc " orr%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 + thumbS ireg r1 ireg r2 shift_op so | Prev (r1,r2) -> - fprintf oc " rev %a, %a\n" ireg r1 ireg r2; 1 + fprintf oc " rev %a, %a\n" ireg r1 ireg r2 | Prev16 (r1,r2) -> - fprintf oc " rev16 %a, %a\n" ireg r1 ireg r2; 1 + fprintf oc " rev16 %a, %a\n" ireg r1 ireg r2 | Prsb(r1, r2, so) -> fprintf oc " rsb%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 + thumbS ireg r1 ireg r2 shift_op so | Prsbs(r1, r2, so) -> fprintf oc " rsbs %a, %a, %a\n" - ireg r1 ireg r2 shift_op so; 1 + ireg r1 ireg r2 shift_op so | Prsc (r1,r2,so) -> - fprintf oc " rsc %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 + fprintf oc " rsc %a, %a, %a\n" ireg r1 ireg r2 shift_op so | Pfsqrt (f1,f2) -> - fprintf oc " vsqrt.f64 %a, %a\n" freg f1 freg f2; 1 + fprintf oc " vsqrt.f64 %a, %a\n" freg f1 freg f2 | Psbc (r1,r2,sa) -> - fprintf oc " sbc %a, %a, %a\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " sbc %a, %a, %a\n" ireg r1 ireg r2 shift_op sa | Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) -> - fprintf oc " str %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " str %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa | Pstrb(r1, r2, sa) -> - fprintf oc " strb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " strb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa | Pstrh(r1, r2, sa) -> - fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa | Pstr_p(r1, r2, sa) -> - fprintf oc " str %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " str %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa | Pstrb_p(r1, r2, sa) -> - fprintf oc " strb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " strb %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa | Pstrh_p(r1, r2, sa) -> - fprintf oc " strh %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " strh %a, [%a], %a\n" ireg r1 ireg r2 shift_op sa | 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 + if Opt.hardware_idiv then + fprintf oc " sdiv r0, r0, r1\n" + else + fprintf oc " bl __aeabi_idiv\n" | Psbfx(r1, r2, lsb, sz) -> - fprintf oc " sbfx %a, %a, #%a, #%a\n" ireg r1 ireg r2 coqint lsb coqint sz; 1 + fprintf oc " sbfx %a, %a, #%a, #%a\n" ireg r1 ireg r2 coqint lsb coqint sz | Psmull(r1, r2, r3, r4) -> - fprintf oc " smull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 + fprintf oc " smull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4 | Psub(r1, r2, so) -> fprintf oc " sub%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 + thumbS ireg r1 ireg r2 shift_op so | Psubs(r1, r2, so) -> fprintf oc " subs %a, %a, %a\n" - ireg r1 ireg r2 shift_op so; 1 + ireg r1 ireg r2 shift_op so | 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 + if Opt.hardware_idiv then + fprintf oc " udiv r0, r0, r1\n" + else + fprintf oc " bl __aeabi_uidiv\n" | Pumull(r1, r2, r3, r4) -> - fprintf oc " umull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 + fprintf oc " umull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4 (* Floating-point VFD instructions *) | Pfcpyd(r1, r2) -> - fprintf oc " vmov.f64 %a, %a\n" freg r1 freg r2; 1 + fprintf oc " vmov.f64 %a, %a\n" freg r1 freg r2 | Pfabsd(r1, r2) -> - fprintf oc " vabs.f64 %a, %a\n" freg r1 freg r2; 1 + fprintf oc " vabs.f64 %a, %a\n" freg r1 freg r2 | Pfnegd(r1, r2) -> - fprintf oc " vneg.f64 %a, %a\n" freg r1 freg r2; 1 + fprintf oc " vneg.f64 %a, %a\n" freg r1 freg r2 | Pfaddd(r1, r2, r3) -> - fprintf oc " vadd.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 + fprintf oc " vadd.f64 %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfdivd(r1, r2, r3) -> - fprintf oc " vdiv.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 + fprintf oc " vdiv.f64 %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfmuld(r1, r2, r3) -> - fprintf oc " vmul.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 + fprintf oc " vmul.f64 %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfsubd(r1, r2, r3) -> - fprintf oc " vsub.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1 + fprintf oc " vsub.f64 %a, %a, %a\n" freg r1 freg r2 freg r3 | 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 + let lbl = label_literal64 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) | Pfcmpd(r1, r2) -> fprintf oc " vcmp.f64 %a, %a\n" freg r1 freg r2; - fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2 + fprintf oc " vmrs APSR_nzcv, FPSCR\n" | Pfcmpzd(r1) -> fprintf oc " vcmp.f64 %a, #0\n" freg r1; - fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2 + fprintf oc " vmrs APSR_nzcv, FPSCR\n" | 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 + fprintf oc " vcvt.f64.s32 %a, %a\n" freg r1 freg_single r1 | 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 + fprintf oc " vcvt.f64.u32 %a, %a\n" freg r1 freg_single r1 | 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 + fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6 | 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 + fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6 | Pfabss(r1, r2) -> - fprintf oc " vabs.f32 %a, %a\n" freg_single r1 freg_single r2; 1 + fprintf oc " vabs.f32 %a, %a\n" freg_single r1 freg_single r2 | Pfnegs(r1, r2) -> - fprintf oc " vneg.f32 %a, %a\n" freg_single r1 freg_single r2; 1 + fprintf oc " vneg.f32 %a, %a\n" freg_single r1 freg_single r2 | Pfadds(r1, r2, r3) -> - fprintf oc " vadd.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 + fprintf oc " vadd.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3 | Pfdivs(r1, r2, r3) -> - fprintf oc " vdiv.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 + fprintf oc " vdiv.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3 | Pfmuls(r1, r2, r3) -> - fprintf oc " vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 + fprintf oc " vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3 | 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 + fprintf oc " push {%a}\n" (fun oc rl -> List.iter (fun ir -> sep (); ireg oc ir) rl) rl | 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 + fprintf oc " vsub.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3 + | Pflis(r1, f) -> assert false (* Should be eliminated in expand constants *) | Pfcmps(r1, r2) -> fprintf oc " vcmp.f32 %a, %a\n" freg_single r1 freg_single r2; - fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2 + fprintf oc " vmrs APSR_nzcv, FPSCR\n" | Pfcmpzs(r1) -> fprintf oc " vcmp.f32 %a, #0\n" freg_single r1; - fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2 + fprintf oc " vmrs APSR_nzcv, FPSCR\n" | 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 + fprintf oc " vcvt.f32.s32 %a, %a\n" freg_single r1 freg_single r1 | 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 + fprintf oc " vcvt.f32.u32 %a, %a\n" freg_single r1 freg_single r1 | 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 + fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6 | 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 + fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6 | Pfcvtsd(r1, r2) -> - fprintf oc " vcvt.f32.f64 %a, %a\n" freg_single r1 freg r2; 1 + fprintf oc " vcvt.f32.f64 %a, %a\n" freg_single r1 freg r2 | Pfcvtds(r1, r2) -> - fprintf oc " vcvt.f64.f32 %a, %a\n" freg r1 freg_single r2; 1 + fprintf oc " vcvt.f64.f32 %a, %a\n" freg r1 freg_single r2 | Pfldd(r1, r2, n) | Pfldd_a(r1, r2, n) -> - fprintf oc " vldr %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1 + fprintf oc " vldr %a, [%a, #%a]\n" freg r1 ireg r2 coqint n | Pflds(r1, r2, n) -> - fprintf oc " vldr %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1 + fprintf oc " vldr %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n | Pfstd(r1, r2, n) | Pfstd_a(r1, r2, n) -> - fprintf oc " vstr %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1 + fprintf oc " vstr %a, [%a, #%a]\n" freg r1 ireg r2 coqint n | Pfsts(r1, r2, n) -> - fprintf oc " vstr %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1 + fprintf oc " vstr %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n (* 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 + fprintf oc "%a:\n" print_label lbl + | Ploadsymbol(r1, id, ofs) -> assert false (* Should be eliminated in expand constants *) | 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 + (neg_condition_name cond) ireg r1 shift_op ifnot | Pbtbl(r, tbl) -> if !Clflags.option_mthumb then begin fprintf oc " lsl r14, %a, #2\n" ireg r; fprintf oc " add pc, r14\n"; (* 16-bit encoding *) - fprintf oc " nop\n"; (* 16-bit encoding *) + fprintf oc " nop\n"; (* 16-bit encoding *) List.iter (fun l -> fprintf oc " b.w %a\n" print_label l) - tbl; - 2 + List.length tbl + 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 + tbl end | Pbuiltin(ef, args, res) -> begin match ef with @@ -591,71 +465,57 @@ struct ais_annot_text lbl preg_annot "sp" (camlstring_of_coqstring txt) args | _ -> assert false end in - fprintf oc "%s annotation: %S\n" comment annot; - 0 + fprintf oc "%s annotation: %S\n" comment annot | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg_annot "sp" oc - (P.to_int kind) (extern_atom txt) args; - 0 + (P.to_int kind) (extern_atom txt) args | 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 *) + fprintf oc "%s end inline assembly\n" comment | _ -> assert false end - | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz); 0 - | Pcfi_rel_offset ofs -> cfi_rel_offset oc "lr" (camlint_of_coqint ofs); 0 + | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz) + | Pcfi_rel_offset ofs -> cfi_rel_offset oc "lr" (camlint_of_coqint ofs) (* Fixup instructions for calling conventions *) | Pfcpy_fs(r1, r2) -> - fprintf oc " vmov.f32 %a, %a\n" freg_single r1 freg_param_single r2; 1 + fprintf oc " vmov.f32 %a, %a\n" freg_single r1 freg_param_single r2 | Pfcpy_sf(r1, r2) -> - fprintf oc " vmov.f32 %a, %a\n" freg_param_single r1 freg_single r2; 1 + fprintf oc " vmov.f32 %a, %a\n" freg_param_single r1 freg_single r2 | Pfcpy_fii (r1, r2, r3) -> - fprintf oc " vmov %a, %a, %a\n" freg r1 ireg r2 ireg r3; 1 + fprintf oc " vmov %a, %a, %a\n" freg r1 ireg r2 ireg r3 | Pfcpy_fi (r1, r2) -> - fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2; 1 + fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2 | Pfcpy_iif (r1, r2, r3) -> - fprintf oc " vmov %a, %a, %a\n" ireg r1 ireg r2 freg r3; 1 + fprintf oc " vmov %a, %a, %a\n" ireg r1 ireg r2 freg r3 | Pfcpy_if (r1, r2) -> - fprintf oc " vmov %a, %a\n" ireg r1 freg_single r2; 1 - - - let no_fallthrough = function - | Pb _ -> true - | Pbsymb _ -> true - | Pbreg _ -> true - | _ -> false + fprintf oc " vmov %a, %a\n" ireg r1 freg_single r2 + | Pconstants consts -> + fprintf oc " .balign 4\n"; + List.iter (print_constants oc) consts + | Ploadsymbol_imm (r1,id,ofs) -> + fprintf oc " movw %a, #:lower16:%a\n" + ireg r1 symbol_offset (id, ofs); + fprintf oc " movt %a, #:upper16:%a\n" + ireg r1 symbol_offset (id, ofs) + | Pflid_lbl (r1,lbl,f) -> + fprintf oc " vldr %a, %a\n" freg r1 print_label lbl + | Pflis_lbl (r1,lbl,f) -> + fprintf oc " vldr %a, %a\n" + freg_single r1 print_label lbl + | Pflid_imm (r1,f) -> + let f = camlint64_of_coqint(Floats.Float.to_bits f) in + fprintf oc " vmov.f64 %a, #%.15F\n" + freg r1 (Int64.float_of_bits f) + | Pflis_imm (r1,f) -> + let f = camlint_of_coqint(Floats.Float32.to_bits f) in + fprintf oc " vmov.f32 %a, #%.15F\n" + freg_single r1 (Int32.float_of_bits f) + | Ploadsymbol_lbl (r1,lbl,id,ofs) -> + fprintf oc " ldr %a, %a\n" + ireg r1 print_label lbl - 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) = @@ -695,14 +555,16 @@ struct let print_instructions oc fn = current_function_sig := fn.fn_sig; - print_instructions oc false fn.fn_code; - if !literals_in_code then emit_constants oc + List.iter (print_instruction oc) fn.fn_code + let emit_constants oc lit = - if not !literals_in_code && !size_constants > 0 then begin + if not !Constantexpand.literals_in_code && exists_constants () then begin section oc lit; - emit_constants oc - end + fprintf oc " .balign 4\n"; + Hashtbl.iter (print_literal64 oc) literal64_labels; + end; + reset_constants () (* Data *) -- cgit