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/Constantexpand.ml | 197 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 197 insertions(+) create mode 100644 arm/Constantexpand.ml (limited to 'arm/Constantexpand.ml') 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 () -- cgit