Proof of Pfmovimm fine tuned OK, moving float checks in Asm

Also some simplifications in Asmblockdeps

1 files changed, 0 insertions, 33 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 32170a0a..6ea592dd 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -755,39 +755,6 @@ 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 d => negb (is_immediate_float32 d)