diff options
Diffstat (limited to 'aarch64/Asmblock.v')
-rw-r--r-- | aarch64/Asmblock.v | 33 |
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) |