From c7f3bd8555c1cae001cc93d21398b52b19d58df0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 26 Nov 2020 23:43:37 +0100 Subject: Proof of Pfmovimm fine tuned OK, moving float checks in Asm Also some simplifications in Asmblockdeps --- aarch64/Asmblock.v | 33 --------------------------------- 1 file changed, 33 deletions(-) (limited to 'aarch64/Asmblock.v') 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) -- cgit