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, 35 insertions, 1 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 7f94a087..32170a0a 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -755,9 +755,43 @@ Definition arith_eval_p (i : arith_p) : val :=
   | Pfmovimmd f => Vfloat f
   end.
 
+(* 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"
+*)
+
+Definition is_immediate_float64 (f: float): bool :=
+  let bits := Float.to_bits f in
+  let exp :=
+    Int64.sub
+      (Int64.and (Int64.shr' bits (Int.repr 52))
+        (Int64.repr 2047)) (Int64.repr 1023) in
+  let mant :=
+    Int64.and bits (Int64.repr 4503599627370495) in
+    andb (Int64.cmp Cge exp (Int64.repr (-3)))
+    (andb (Int64.cmp Cle exp (Int64.repr 4))
+      (Int64.eq
+        (Int64.and mant
+          (Int64.repr 4222124650659840)) mant)).
+
+Definition is_immediate_float32 (f: float32): bool :=
+  let bits := Float32.to_bits f in
+  let exp :=
+    Int.sub
+      (Int.and (Int.shr bits (Int.repr 23))
+        (Int.repr 255)) (Int.repr 127) in
+  let mant :=
+    Int.and bits (Int.repr 8388607) in
+    andb (Int.cmp Cge exp (Int.repr (-3)))
+    (andb (Int.cmp Cle exp (Int.repr 4))
+      (Int.eq
+        (Int.and mant
+          (Int.repr 7864320)) mant)).
+
 Definition destroy_X16 (i : arith_p) : bool :=
   match i with
-  | Pfmovimms _ | Pfmovimmd _ => true (* TODO: we may refine this condition, according to the value of the immediate like in TargetPrinter *)
+  | Pfmovimms d => negb (is_immediate_float32 d)
+  | Pfmovimmd d => negb (is_immediate_float64 d)
   | _ => false
   end.