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

Also some simplifications in Asmblockdeps

1 files changed, 41 insertions, 3 deletions

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 618341a3..19601024 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -660,6 +660,38 @@ Definition float64_of_bits (v: val): val :=
   | _ => Vundef
   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)).
 
 (** Translation of the LTL/Linear/Mach view of machine registers
   to the AArch64 view.  Note that no LTL register maps to [X16],
@@ -1092,10 +1124,16 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   (** Floating-point move *)
   | Pfmov rd r1 =>
       Next (nextinstr (rs#rd <- (rs#r1))) m
-  | Pfmovimms rd f =>
-      Next (nextinstr ((rs#rd <- (Vsingle f))#X16 <- Vundef)) m
+  | Pfmovimms rd f => 
+      if is_immediate_float32 f then
+        Next (nextinstr (rs#rd <- (Vsingle f))) m
+      else
+        Next (nextinstr ((rs#rd <- (Vsingle f))#X16 <- Vundef)) m
   | Pfmovimmd rd f =>
-      Next (nextinstr ((rs#rd <- (Vfloat f))#X16 <- Vundef)) m
+      if is_immediate_float64 f then
+        Next (nextinstr (rs#rd <- (Vfloat f))) m
+      else
+        Next (nextinstr ((rs#rd <- (Vfloat f))#X16 <- Vundef)) m
   | Pfmovi S rd r1 =>
       Next (nextinstr (rs#rd <- (float32_of_bits rs##r1))) m
   | Pfmovi D rd r1 =>