Fine tuning for Pfmovimm

- Functions to check a float logical immediate were translated from ocaml target printer in coq Asmblock
- Some proof are admitted for now (we'll see if it is a good idea after some tests)

1 files changed, 2 insertions, 17 deletions

diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index 324bd727..5b3919d3 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -21,21 +21,6 @@ open AisAnnot
 open PrintAsmaux
 open Fileinfo
 
-(* Recognition of FP numbers that are supported by the fmov #imm instructions:
-   "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
-
 (* Module containing the printing functions *)
 
 module Target (*: TARGET*) =
@@ -431,7 +416,7 @@ module Target (*: TARGET*) =
         fprintf oc "	fmov	%a, %a\n" dreg rd dreg r1
     | Pfmovimmd(rd, f) ->
         let d = camlint64_of_coqint (Floats.Float.to_bits f) in
-        if is_immediate_float64 d then
+        if Asmblock.is_immediate_float64 f then
           fprintf oc "	fmov	%a, #%.7f\n" dreg rd (Int64.float_of_bits d)
         else begin
           let lbl = label_literal64 d in
@@ -440,7 +425,7 @@ module Target (*: TARGET*) =
         end
     | Pfmovimms(rd, f) ->
         let d = camlint_of_coqint (Floats.Float32.to_bits f) in
-        if is_immediate_float32 d then
+        if Asmblock.is_immediate_float32 f then
           fprintf oc "	fmov	%a, #%.7f\n" sreg rd (Int32.float_of_bits d)
         else begin
           let lbl = label_literal32 d in