mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-08-16 17:30:27 +03:00
Convert to using the SFloat module from What4.
Expose some additional primitives, such as FMA, abs, sqrt, and more classification predicates. Refactor the primitives table for floating-point values into a single generic table that uses methods from the `Backend` class.
This commit is contained in:
Rob Dockins
parent
e5d5a38597
commit
0909120a68
@ -75,7 +75,7 @@ library
|
||||
mtl >= 2.2.1,
|
||||
time >= 1.6.0.1,
|
||||
panic >= 0.3,
|
||||
what4 >= 1.0 && < 1.1
|
||||
what4 >= 1.1 && < 1.2
|
||||
|
||||
Build-tool-depends: alex:alex, happy:happy
|
||||
hs-source-dirs: src
|
||||
@ -165,7 +165,6 @@ library
|
||||
Cryptol.Backend.Monad,
|
||||
Cryptol.Backend.SBV,
|
||||
Cryptol.Backend.What4,
|
||||
Cryptol.Backend.What4.SFloat,
|
||||
|
||||
Cryptol.Eval,
|
||||
Cryptol.Eval.Concrete,
|
||||
|
||||
@ -79,6 +79,7 @@ primitive
|
||||
primitive
|
||||
fpPosInf : {e,p} ValidFloat e p => Float e p
|
||||
|
||||
/** Negative infinity. */
|
||||
fpNegInf : {e,p} ValidFloat e p => Float e p
|
||||
fpNegInf = - fpPosInf
|
||||
|
||||
@ -133,11 +134,31 @@ primitive
|
||||
|
||||
infix 20 =.=
|
||||
|
||||
/** Test if this value is not-a-number (NaN). */
|
||||
primitive fpIsNaN : {e,p} ValidFloat e p => Float e p -> Bool
|
||||
|
||||
/** Test if this value is positive or negative infinity. */
|
||||
primitive fpIsInf : {e,p} ValidFloat e p => Float e p -> Bool
|
||||
|
||||
/** Test if this value is positive or negative zero. */
|
||||
primitive fpIsZero : {e,p} ValidFloat e p => Float e p -> Bool
|
||||
|
||||
/** Test if this value is negative. */
|
||||
primitive fpIsNeg : {e,p} ValidFloat e p => Float e p -> Bool
|
||||
|
||||
/** Test if this value is normal (not NaN, not infinite, not zero, and not subnormal). */
|
||||
primitive fpIsNormal : {e,p} ValidFloat e p => Float e p -> Bool
|
||||
|
||||
/**
|
||||
* Test if this value is subnormal. Subnormal values are nonzero
|
||||
* values with magnitudes smaller than can be represented with the
|
||||
* normal implicit leading bit convention.
|
||||
*/
|
||||
primitive fpIsSubnormal : {e,p} ValidFloat e p => Float e p -> Bool
|
||||
|
||||
/* Returns true for numbers that are not an infinity or NaN. */
|
||||
primitive
|
||||
fpIsFinite : {e,p} ValidFloat e p => Float e p -> Bool
|
||||
|
||||
fpIsFinite : {e,p} ValidFloat e p => Float e p -> Bool
|
||||
fpIsFinite f = ~ (fpIsNaN f \/ fpIsInf f )
|
||||
|
||||
|
||||
/* ----------------------------------------------------------------------
|
||||
@ -165,6 +186,30 @@ primitive
|
||||
fpDiv : {e,p} ValidFloat e p =>
|
||||
RoundingMode -> Float e p -> Float e p -> Float e p
|
||||
|
||||
/**
|
||||
* Fused-multiply-add. 'fpFMA r x y z' computes the value '(x*y)+z',
|
||||
* rounding the result according to mode 'r' only after performing both
|
||||
* operations.
|
||||
*/
|
||||
primitive
|
||||
fpFMA : {e,p} ValidFloat e p =>
|
||||
RoundingMode -> Float e p -> Float e p -> Float e p -> Float e p
|
||||
|
||||
/**
|
||||
* Absolute value of a floating-point value.
|
||||
*/
|
||||
primitive
|
||||
fpAbs : {e,p} ValidFloat e p =>
|
||||
Float e p -> Float e p
|
||||
|
||||
/**
|
||||
* Square root of a floating-point value. The square root of
|
||||
* a negative value yiels NaN, except that the sqaure root of
|
||||
* '-0.0' is '-0.0'.
|
||||
*/
|
||||
primitive
|
||||
fpSqrt : {e,p} ValidFloat e p =>
|
||||
RoundingMode -> Float e p -> Float e p
|
||||
|
||||
/* ------------------------------------------------------------ *
|
||||
* Rationals *
|
||||
@ -181,4 +226,3 @@ given rounding mode, if the number cannot be represented exactly. */
|
||||
primitive
|
||||
fpFromRational : {e,p} ValidFloat e p =>
|
||||
RoundingMode -> Rational -> Float e p
|
||||
|
||||
|
||||
@ -310,6 +310,7 @@ class MonadIO (SEval sym) => Backend sym where
|
||||
iteBit :: sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
|
||||
iteWord :: sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
|
||||
iteInteger :: sym -> SBit sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
|
||||
iteFloat :: sym -> SBit sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
|
||||
|
||||
-- ==== Bit operations ====
|
||||
bitEq :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
|
||||
@ -318,7 +319,6 @@ class MonadIO (SEval sym) => Backend sym where
|
||||
bitXor :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
|
||||
bitComplement :: sym -> SBit sym -> SEval sym (SBit sym)
|
||||
|
||||
|
||||
-- ==== Word operations ====
|
||||
|
||||
-- | Extract the numbered bit from the word.
|
||||
@ -674,21 +674,51 @@ class MonadIO (SEval sym) => Backend sym where
|
||||
|
||||
fpLogicalEq :: sym -> SFloat sym -> SFloat sym -> SEval sym (SBit sym)
|
||||
|
||||
fpNaN :: sym -> Integer {- ^ exponent bits -} -> Integer {- ^ precision bits -} -> SEval sym (SFloat sym)
|
||||
fpPosInf :: sym -> Integer {- ^ exponent bits -} -> Integer {- ^ precision bits -} -> SEval sym (SFloat sym)
|
||||
|
||||
fpPlus, fpMinus, fpMult, fpDiv :: FPArith2 sym
|
||||
fpNeg :: sym -> SFloat sym -> SEval sym (SFloat sym)
|
||||
fpNeg, fpAbs :: sym -> SFloat sym -> SEval sym (SFloat sym)
|
||||
fpSqrt :: sym -> SWord sym -> SFloat sym -> SEval sym (SFloat sym)
|
||||
|
||||
fpFMA :: sym -> SWord sym -> SFloat sym -> SFloat sym -> SFloat sym -> SEval sym (SFloat sym)
|
||||
|
||||
fpIsZero, fpIsNeg, fpIsNaN, fpIsInf, fpIsNorm, fpIsSubnorm :: sym -> SFloat sym -> SEval sym (SBit sym)
|
||||
|
||||
fpToBits :: sym -> SFloat sym -> SEval sym (SWord sym)
|
||||
fpFromBits ::
|
||||
sym ->
|
||||
Integer {- ^ exponent bits -} ->
|
||||
Integer {- ^ precision bits -} ->
|
||||
SWord sym ->
|
||||
SEval sym (SFloat sym)
|
||||
|
||||
fpToInteger ::
|
||||
sym ->
|
||||
String {- ^ Name of the function for error reporting -} ->
|
||||
SWord sym {-^ Rounding mode -} ->
|
||||
SFloat sym -> SEval sym (SInteger sym)
|
||||
SWord sym {- ^ Rounding mode -} ->
|
||||
SFloat sym ->
|
||||
SEval sym (SInteger sym)
|
||||
|
||||
fpFromInteger ::
|
||||
sym ->
|
||||
Integer {- exp width -} ->
|
||||
Integer {- prec width -} ->
|
||||
Integer {- ^ exp width -} ->
|
||||
Integer {- ^ prec width -} ->
|
||||
SWord sym {- ^ rounding mode -} ->
|
||||
SInteger sym {- ^ the integeer to use -} ->
|
||||
SInteger sym {- ^ the integer to use -} ->
|
||||
SEval sym (SFloat sym)
|
||||
|
||||
fpToRational ::
|
||||
sym ->
|
||||
SFloat sym ->
|
||||
SEval sym (SRational sym)
|
||||
|
||||
fpFromRational ::
|
||||
sym ->
|
||||
Integer {- ^ exp width -} ->
|
||||
Integer {- ^ prec width -} ->
|
||||
SWord sym {- ^ rounding mode -} ->
|
||||
SRational sym ->
|
||||
SEval sym (SFloat sym)
|
||||
|
||||
type FPArith2 sym =
|
||||
|
||||
@ -37,6 +37,7 @@ module Cryptol.Backend.Concrete
|
||||
|
||||
import qualified Control.Exception as X
|
||||
import Data.Bits
|
||||
import Data.Ratio
|
||||
import Numeric (showIntAtBase)
|
||||
import qualified LibBF as FP
|
||||
import qualified GHC.Integer.GMP.Internals as Integer
|
||||
@ -177,6 +178,7 @@ instance Backend Concrete where
|
||||
iteBit _ b x y = pure $! if b then x else y
|
||||
iteWord _ b x y = pure $! if b then x else y
|
||||
iteInteger _ b x y = pure $! if b then x else y
|
||||
iteFloat _ b x y = pure $! if b then x else y
|
||||
|
||||
wordLit _ w i = pure $! mkBv w i
|
||||
wordAsLit _ (BV w i) = Just (w,i)
|
||||
@ -326,6 +328,10 @@ instance Backend Concrete where
|
||||
------------------------------------------------------------------------
|
||||
-- Floating Point
|
||||
fpLit _sym e p rat = pure (FP.fpLit e p rat)
|
||||
|
||||
fpNaN _sym e p = pure (FP.BF e p FP.bfNaN)
|
||||
fpPosInf _sym e p = pure (FP.BF e p FP.bfPosInf)
|
||||
|
||||
fpAsLit _ f = Just f
|
||||
fpExactLit _sym bf = pure bf
|
||||
fpEq _sym x y = pure (FP.bfValue x == FP.bfValue y)
|
||||
@ -336,7 +342,33 @@ instance Backend Concrete where
|
||||
fpMinus = fpBinArith FP.bfSub
|
||||
fpMult = fpBinArith FP.bfMul
|
||||
fpDiv = fpBinArith FP.bfDiv
|
||||
fpNeg _ x = pure x { FP.bfValue = FP.bfNeg (FP.bfValue x) }
|
||||
fpNeg _ x = pure $! x { FP.bfValue = FP.bfNeg (FP.bfValue x) }
|
||||
|
||||
fpAbs _ x = pure $! x { FP.bfValue = FP.bfAbs (FP.bfValue x) }
|
||||
fpSqrt sym r x =
|
||||
do r' <- fpRoundMode sym r
|
||||
let opts = FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x) r'
|
||||
pure $! x{ FP.bfValue = FP.fpCheckStatus (FP.bfSqrt opts (FP.bfValue x)) }
|
||||
|
||||
fpFMA sym r x y z =
|
||||
do r' <- fpRoundMode sym r
|
||||
let opts = FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x) r'
|
||||
pure $! x { FP.bfValue = FP.fpCheckStatus (FP.bfFMA opts (FP.bfValue x) (FP.bfValue y) (FP.bfValue z)) }
|
||||
|
||||
fpIsZero _ x = pure (FP.bfIsZero (FP.bfValue x))
|
||||
fpIsNeg _ x = pure (FP.bfIsNeg (FP.bfValue x))
|
||||
fpIsNaN _ x = pure (FP.bfIsNaN (FP.bfValue x))
|
||||
fpIsInf _ x = pure (FP.bfIsInf (FP.bfValue x))
|
||||
fpIsNorm _ x =
|
||||
let opts = FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x) FP.NearEven
|
||||
in pure (FP.bfIsNormal opts (FP.bfValue x))
|
||||
fpIsSubnorm _ x =
|
||||
let opts = FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x) FP.NearEven
|
||||
in pure (FP.bfIsSubnormal opts (FP.bfValue x))
|
||||
|
||||
fpFromBits _sym e p bv = pure (FP.floatFromBits e p (bvVal bv))
|
||||
fpToBits _sym (FP.BF e p v) = pure (mkBv (e+p) (FP.floatToBits e p v))
|
||||
|
||||
fpFromInteger sym e p r x =
|
||||
do r' <- fpRoundMode sym r
|
||||
pure FP.BF { FP.bfExpWidth = e
|
||||
@ -346,6 +378,14 @@ instance Backend Concrete where
|
||||
}
|
||||
fpToInteger = fpCvtToInteger
|
||||
|
||||
fpFromRational sym e p r x =
|
||||
do mode <- fpRoundMode sym r
|
||||
pure (FP.floatFromRational e p mode (sNum x % sDenom x))
|
||||
|
||||
fpToRational sym fp =
|
||||
case FP.floatToRational "fpToRational" fp of
|
||||
Left err -> raiseError sym err
|
||||
Right r -> pure $ SRational { sNum = numerator r, sDenom = denominator r }
|
||||
|
||||
{-# INLINE liftBinIntMod #-}
|
||||
liftBinIntMod :: Monad m =>
|
||||
@ -367,7 +407,7 @@ fpBinArith ::
|
||||
fpBinArith fun = \sym r x y ->
|
||||
do opts <- FP.fpOpts (FP.bfExpWidth x) (FP.bfPrecWidth x)
|
||||
<$> fpRoundMode sym r
|
||||
pure x { FP.bfValue = FP.fpCheckStatus
|
||||
pure $! x { FP.bfValue = FP.fpCheckStatus
|
||||
(fun opts (FP.bfValue x) (FP.bfValue y)) }
|
||||
|
||||
fpCvtToInteger ::
|
||||
|
||||
@ -11,9 +11,9 @@ import Cryptol.Backend.Monad( EvalError(..) )
|
||||
|
||||
|
||||
data BF = BF
|
||||
{ bfExpWidth :: Integer
|
||||
, bfPrecWidth :: Integer
|
||||
, bfValue :: BigFloat
|
||||
{ bfExpWidth :: !Integer
|
||||
, bfPrecWidth :: !Integer
|
||||
, bfValue :: !BigFloat
|
||||
}
|
||||
|
||||
|
||||
|
||||
@ -325,6 +325,9 @@ instance Backend SBV where
|
||||
znRecip = sModRecip
|
||||
|
||||
fpAsLit _ _ = Nothing
|
||||
iteFloat _ _ _ _ = unsupported "iteFloat"
|
||||
fpNaN _ _ _ = unsupported "fpNaN"
|
||||
fpPosInf _ _ _ = unsupported "fpPosInf"
|
||||
fpExactLit _ _ = unsupported "fpExactLit"
|
||||
fpLit _ _ _ _ = unsupported "fpLit"
|
||||
fpLogicalEq _ _ _ = unsupported "fpLogicalEq"
|
||||
@ -335,9 +338,23 @@ instance Backend SBV where
|
||||
fpMinus _ _ _ _ = unsupported "fpMinus"
|
||||
fpMult _ _ _ _ = unsupported "fpMult"
|
||||
fpDiv _ _ _ _ = unsupported "fpDiv"
|
||||
fpAbs _ _ = unsupported "fpAbs"
|
||||
fpSqrt _ _ _ = unsupported "fpSqrt"
|
||||
fpFMA _ _ _ _ _ = unsupported "fpFMA"
|
||||
fpNeg _ _ = unsupported "fpNeg"
|
||||
fpFromInteger _ _ _ _ _ = unsupported "fpFromInteger"
|
||||
fpToInteger _ _ _ _ = unsupported "fpToInteger"
|
||||
fpIsZero _ _ = unsupported "fpIsZero"
|
||||
fpIsInf _ _ = unsupported "fpIsInf"
|
||||
fpIsNeg _ _ = unsupported "fpIsNeg"
|
||||
fpIsNaN _ _ = unsupported "fpIsNaN"
|
||||
fpIsNorm _ _ = unsupported "fpIsNorm"
|
||||
fpIsSubnorm _ _ = unsupported "fpIsSubnorm"
|
||||
fpToBits _ _ = unsupported "fpToBits"
|
||||
fpFromBits _ _ _ _ = unsupported "fpFromBits"
|
||||
fpToRational _ _ = unsupported "fpToRational"
|
||||
fpFromRational _ _ _ _ _ = unsupported "fpFromRational"
|
||||
|
||||
|
||||
unsupported :: String -> SEval SBV a
|
||||
unsupported x = liftIO (X.throw (UnsupportedSymbolicOp x))
|
||||
|
||||
@ -32,8 +32,7 @@ import qualified GHC.Integer.GMP.Internals as Integer
|
||||
|
||||
import qualified What4.Interface as W4
|
||||
import qualified What4.SWord as SW
|
||||
|
||||
import qualified Cryptol.Backend.What4.SFloat as FP
|
||||
import qualified What4.SFloat as FP
|
||||
|
||||
import Cryptol.Backend
|
||||
import Cryptol.Backend.FloatHelpers
|
||||
@ -296,6 +295,7 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
|
||||
iteBit sym c x y = liftIO (W4.itePred (w4 sym) c x y)
|
||||
iteWord sym c x y = liftIO (SW.bvIte (w4 sym) c x y)
|
||||
iteInteger sym c x y = liftIO (W4.intIte (w4 sym) c x y)
|
||||
iteFloat sym p x y = liftIO (FP.fpIte (w4 sym) p x y)
|
||||
|
||||
bitEq sym x y = liftIO (W4.eqPred (w4 sym) x y)
|
||||
bitAnd sym x y = liftIO (W4.andPred (w4 sym) x y)
|
||||
@ -432,11 +432,18 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
|
||||
--------------------------------------------------------------
|
||||
|
||||
fpLit sym e p r = liftIO $ FP.fpFromRationalLit (w4 sym) e p r
|
||||
fpAsLit _ _ = Nothing -- TODO
|
||||
fpAsLit _ f = BF e p <$> FP.fpAsLit f
|
||||
where (e,p) = FP.fpSize f
|
||||
|
||||
fpExactLit sym BF{ bfExpWidth = e, bfPrecWidth = p, bfValue = bf } =
|
||||
liftIO (FP.fpFromBinary (w4 sym) e p =<< SW.bvLit (w4 sym) (e+p) (floatToBits e p bf))
|
||||
|
||||
fpNaN sym e p = liftIO (FP.fpNaN (w4 sym) e p)
|
||||
fpPosInf sym e p = liftIO (FP.fpPosInf (w4 sym) e p)
|
||||
|
||||
fpToBits sym f = liftIO (FP.fpToBinary (w4 sym) f)
|
||||
fpFromBits sym e p w = liftIO (FP.fpFromBinary (w4 sym) e p w)
|
||||
|
||||
fpEq sym x y = liftIO $ FP.fpEqIEEE (w4 sym) x y
|
||||
fpLessThan sym x y = liftIO $ FP.fpLtIEEE (w4 sym) x y
|
||||
fpGreaterThan sym x y = liftIO $ FP.fpGtIEEE (w4 sym) x y
|
||||
@ -448,6 +455,21 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
|
||||
fpDiv = fpBinArith FP.fpDiv
|
||||
|
||||
fpNeg sym x = liftIO $ FP.fpNeg (w4 sym) x
|
||||
fpAbs sym x = liftIO $ FP.fpAbs (w4 sym) x
|
||||
fpSqrt sym r x =
|
||||
do rm <- fpRoundingMode sym r
|
||||
liftIO $ FP.fpSqrt (w4 sym) rm x
|
||||
|
||||
fpFMA sym r x y z =
|
||||
do rm <- fpRoundingMode sym r
|
||||
liftIO $ FP.fpFMA (w4 sym) rm x y z
|
||||
|
||||
fpIsZero sym x = liftIO $ FP.fpIsZero (w4 sym) x
|
||||
fpIsNeg sym x = liftIO $ FP.fpIsNeg (w4 sym) x
|
||||
fpIsNaN sym x = liftIO $ FP.fpIsNaN (w4 sym) x
|
||||
fpIsInf sym x = liftIO $ FP.fpIsInf (w4 sym) x
|
||||
fpIsNorm sym x = liftIO $ FP.fpIsNorm (w4 sym) x
|
||||
fpIsSubnorm sym x = liftIO $ FP.fpIsSubnorm (w4 sym) x
|
||||
|
||||
fpFromInteger sym e p r x =
|
||||
do rm <- fpRoundingMode sym r
|
||||
@ -455,6 +477,9 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
|
||||
|
||||
fpToInteger = fpCvtToInteger
|
||||
|
||||
fpFromRational = fpCvtFromRational
|
||||
fpToRational = fpCvtToRational
|
||||
|
||||
sModAdd :: W4.IsSymExprBuilder sym =>
|
||||
sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
|
||||
sModAdd _sym 0 _ _ = evalPanic "sModAdd" ["0 modulus not allowed"]
|
||||
|
||||
@ -1,362 +0,0 @@
|
||||
{-# Language DataKinds #-}
|
||||
{-# Language FlexibleContexts #-}
|
||||
{-# Language GADTs #-}
|
||||
{-# Language RankNTypes #-}
|
||||
{-# Language TypeApplications #-}
|
||||
{-# Language TypeOperators #-}
|
||||
-- | Working with floats of dynamic sizes.
|
||||
-- This should probably be moved to What4 one day.
|
||||
module Cryptol.Backend.What4.SFloat
|
||||
( -- * Interface
|
||||
SFloat(..)
|
||||
, fpReprOf
|
||||
, fpSize
|
||||
, fpRepr
|
||||
|
||||
-- * Constants
|
||||
, fpFresh
|
||||
, fpNaN
|
||||
, fpPosInf
|
||||
, fpFromRationalLit
|
||||
|
||||
-- * Interchange formats
|
||||
, fpFromBinary
|
||||
, fpToBinary
|
||||
|
||||
-- * Relations
|
||||
, SFloatRel
|
||||
, fpEq
|
||||
, fpEqIEEE
|
||||
, fpLtIEEE
|
||||
, fpGtIEEE
|
||||
|
||||
-- * Arithmetic
|
||||
, SFloatBinArith
|
||||
, fpNeg
|
||||
, fpAdd
|
||||
, fpSub
|
||||
, fpMul
|
||||
, fpDiv
|
||||
|
||||
-- * Conversions
|
||||
, fpRound
|
||||
, fpToReal
|
||||
, fpFromReal
|
||||
, fpFromRational
|
||||
, fpToRational
|
||||
, fpFromInteger
|
||||
|
||||
-- * Queries
|
||||
, fpIsInf, fpIsNaN
|
||||
|
||||
-- * Exceptions
|
||||
, UnsupportedFloat(..)
|
||||
, FPTypeError(..)
|
||||
) where
|
||||
|
||||
import Control.Exception
|
||||
|
||||
import Data.Parameterized.Some
|
||||
import Data.Parameterized.NatRepr
|
||||
|
||||
import What4.BaseTypes
|
||||
import What4.Panic(panic)
|
||||
import What4.SWord
|
||||
import What4.Interface
|
||||
|
||||
-- | Symbolic floating point numbers.
|
||||
data SFloat sym where
|
||||
SFloat :: IsExpr (SymExpr sym) => SymFloat sym fpp -> SFloat sym
|
||||
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- | This exception is thrown if the operations try to create a
|
||||
-- floating point value we do not support
|
||||
data UnsupportedFloat =
|
||||
UnsupportedFloat { fpWho :: String, exponentBits, precisionBits :: Integer }
|
||||
deriving Show
|
||||
|
||||
|
||||
-- | Throw 'UnsupportedFloat' exception
|
||||
unsupported ::
|
||||
String {- ^ Label -} ->
|
||||
Integer {- ^ Exponent width -} ->
|
||||
Integer {- ^ Precision width -} ->
|
||||
IO a
|
||||
unsupported l e p =
|
||||
throwIO UnsupportedFloat { fpWho = l
|
||||
, exponentBits = e
|
||||
, precisionBits = p }
|
||||
|
||||
instance Exception UnsupportedFloat
|
||||
|
||||
-- | This exceptoin is throws if the types don't match.
|
||||
data FPTypeError =
|
||||
FPTypeError { fpExpected :: Some BaseTypeRepr
|
||||
, fpActual :: Some BaseTypeRepr
|
||||
}
|
||||
deriving Show
|
||||
|
||||
instance Exception FPTypeError
|
||||
|
||||
fpTypeMismatch :: BaseTypeRepr t1 -> BaseTypeRepr t2 -> IO a
|
||||
fpTypeMismatch expect actual =
|
||||
throwIO FPTypeError { fpExpected = Some expect
|
||||
, fpActual = Some actual
|
||||
}
|
||||
fpTypeError :: FloatPrecisionRepr t1 -> FloatPrecisionRepr t2 -> IO a
|
||||
fpTypeError t1 t2 =
|
||||
fpTypeMismatch (BaseFloatRepr t1) (BaseFloatRepr t2)
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- | Construct the 'FloatPrecisionRepr' with the given parameters.
|
||||
fpRepr ::
|
||||
Integer {- ^ Exponent width -} ->
|
||||
Integer {- ^ Precision width -} ->
|
||||
Maybe (Some FloatPrecisionRepr)
|
||||
fpRepr iE iP =
|
||||
do Some e <- someNat iE
|
||||
LeqProof <- testLeq (knownNat @2) e
|
||||
Some p <- someNat iP
|
||||
LeqProof <- testLeq (knownNat @2) p
|
||||
pure (Some (FloatingPointPrecisionRepr e p))
|
||||
|
||||
fpReprOf ::
|
||||
IsExpr (SymExpr sym) => sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
|
||||
fpReprOf _ e =
|
||||
case exprType e of
|
||||
BaseFloatRepr r -> r
|
||||
|
||||
fpSize :: SFloat sym -> (Integer,Integer)
|
||||
fpSize (SFloat f) =
|
||||
case exprType f of
|
||||
BaseFloatRepr (FloatingPointPrecisionRepr e p) -> (intValue e, intValue p)
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Constants
|
||||
|
||||
-- | A fresh variable of the given type.
|
||||
fpFresh ::
|
||||
IsSymExprBuilder sym =>
|
||||
sym ->
|
||||
Integer ->
|
||||
Integer ->
|
||||
IO (SFloat sym)
|
||||
fpFresh sym e p
|
||||
| Just (Some fpp) <- fpRepr e p =
|
||||
SFloat <$> freshConstant sym emptySymbol (BaseFloatRepr fpp)
|
||||
| otherwise = unsupported "fpFresh" e p
|
||||
|
||||
-- | Not a number
|
||||
fpNaN ::
|
||||
IsExprBuilder sym =>
|
||||
sym ->
|
||||
Integer {- ^ Exponent width -} ->
|
||||
Integer {- ^ Precision width -} ->
|
||||
IO (SFloat sym)
|
||||
fpNaN sym e p
|
||||
| Just (Some fpp) <- fpRepr e p = SFloat <$> floatNaN sym fpp
|
||||
| otherwise = unsupported "fpNaN" e p
|
||||
|
||||
|
||||
-- | Positive infinity
|
||||
fpPosInf ::
|
||||
IsExprBuilder sym =>
|
||||
sym ->
|
||||
Integer {- ^ Exponent width -} ->
|
||||
Integer {- ^ Precision width -} ->
|
||||
IO (SFloat sym)
|
||||
fpPosInf sym e p
|
||||
| Just (Some fpp) <- fpRepr e p = SFloat <$> floatPInf sym fpp
|
||||
| otherwise = unsupported "fpPosInf" e p
|
||||
|
||||
-- | A floating point number corresponding to the given rations.
|
||||
fpFromRationalLit ::
|
||||
IsExprBuilder sym =>
|
||||
sym ->
|
||||
Integer {- ^ Exponent width -} ->
|
||||
Integer {- ^ Precision width -} ->
|
||||
Rational ->
|
||||
IO (SFloat sym)
|
||||
fpFromRationalLit sym e p r
|
||||
| Just (Some fpp) <- fpRepr e p = SFloat <$> floatLitRational sym fpp r
|
||||
| otherwise = unsupported "fpFromRational" e p
|
||||
|
||||
|
||||
-- | Make a floating point number with the given bit representation.
|
||||
fpFromBinary ::
|
||||
IsExprBuilder sym =>
|
||||
sym ->
|
||||
Integer {- ^ Exponent width -} ->
|
||||
Integer {- ^ Precision width -} ->
|
||||
SWord sym ->
|
||||
IO (SFloat sym)
|
||||
fpFromBinary sym e p swe
|
||||
| DBV sw <- swe
|
||||
, Just (Some fpp) <- fpRepr e p
|
||||
, FloatingPointPrecisionRepr ew pw <- fpp
|
||||
, let expectW = addNat ew pw
|
||||
, actual@(BaseBVRepr actualW) <- exprType sw =
|
||||
case testEquality expectW actualW of
|
||||
Just Refl -> SFloat <$> floatFromBinary sym fpp sw
|
||||
Nothing -- we want to report type correct type errors! :-)
|
||||
| Just LeqProof <- testLeq (knownNat @1) expectW ->
|
||||
fpTypeMismatch (BaseBVRepr expectW) actual
|
||||
| otherwise -> panic "fpFromBits" [ "1 >= 2" ]
|
||||
| otherwise = unsupported "fpFromBits" e p
|
||||
|
||||
fpToBinary :: IsExprBuilder sym => sym -> SFloat sym -> IO (SWord sym)
|
||||
fpToBinary sym (SFloat f)
|
||||
| FloatingPointPrecisionRepr e p <- fpReprOf sym f
|
||||
, Just LeqProof <- testLeq (knownNat @1) (addNat e p)
|
||||
= DBV <$> floatToBinary sym f
|
||||
| otherwise = panic "fpToBinary" [ "we messed up the types" ]
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Arithmetic
|
||||
|
||||
fpNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)
|
||||
fpNeg sym (SFloat fl) = SFloat <$> floatNeg sym fl
|
||||
|
||||
fpBinArith ::
|
||||
IsExprBuilder sym =>
|
||||
(forall t.
|
||||
sym ->
|
||||
RoundingMode ->
|
||||
SymFloat sym t ->
|
||||
SymFloat sym t ->
|
||||
IO (SymFloat sym t)
|
||||
) ->
|
||||
sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)
|
||||
fpBinArith fun sym r (SFloat x) (SFloat y) =
|
||||
let t1 = sym `fpReprOf` x
|
||||
t2 = sym `fpReprOf` y
|
||||
in
|
||||
case testEquality t1 t2 of
|
||||
Just Refl -> SFloat <$> fun sym r x y
|
||||
_ -> fpTypeError t1 t2
|
||||
|
||||
type SFloatBinArith sym =
|
||||
sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)
|
||||
|
||||
fpAdd :: IsExprBuilder sym => SFloatBinArith sym
|
||||
fpAdd = fpBinArith floatAdd
|
||||
|
||||
fpSub :: IsExprBuilder sym => SFloatBinArith sym
|
||||
fpSub = fpBinArith floatSub
|
||||
|
||||
fpMul :: IsExprBuilder sym => SFloatBinArith sym
|
||||
fpMul = fpBinArith floatMul
|
||||
|
||||
fpDiv :: IsExprBuilder sym => SFloatBinArith sym
|
||||
fpDiv = fpBinArith floatDiv
|
||||
|
||||
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
fpRel ::
|
||||
IsExprBuilder sym =>
|
||||
(forall t.
|
||||
sym ->
|
||||
SymFloat sym t ->
|
||||
SymFloat sym t ->
|
||||
IO (Pred sym)
|
||||
) ->
|
||||
sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
|
||||
fpRel fun sym (SFloat x) (SFloat y) =
|
||||
let t1 = sym `fpReprOf` x
|
||||
t2 = sym `fpReprOf` y
|
||||
in
|
||||
case testEquality t1 t2 of
|
||||
Just Refl -> fun sym x y
|
||||
_ -> fpTypeError t1 t2
|
||||
|
||||
|
||||
|
||||
|
||||
type SFloatRel sym =
|
||||
sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
|
||||
|
||||
fpEq :: IsExprBuilder sym => SFloatRel sym
|
||||
fpEq = fpRel floatEq
|
||||
|
||||
fpEqIEEE :: IsExprBuilder sym => SFloatRel sym
|
||||
fpEqIEEE = fpRel floatFpEq
|
||||
|
||||
fpLtIEEE :: IsExprBuilder sym => SFloatRel sym
|
||||
fpLtIEEE = fpRel floatLt
|
||||
|
||||
fpGtIEEE :: IsExprBuilder sym => SFloatRel sym
|
||||
fpGtIEEE = fpRel floatGt
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
fpRound ::
|
||||
IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
|
||||
fpRound sym r (SFloat x) = SFloat <$> floatRound sym r x
|
||||
|
||||
-- | This is undefined on "special" values (NaN,infinity)
|
||||
fpToReal :: IsExprBuilder sym => sym -> SFloat sym -> IO (SymReal sym)
|
||||
fpToReal sym (SFloat x) = floatToReal sym x
|
||||
|
||||
fpFromReal ::
|
||||
IsExprBuilder sym =>
|
||||
sym -> Integer -> Integer -> RoundingMode -> SymReal sym -> IO (SFloat sym)
|
||||
fpFromReal sym e p r x
|
||||
| Just (Some repr) <- fpRepr e p = SFloat <$> realToFloat sym repr r x
|
||||
| otherwise = unsupported "fpFromReal" e p
|
||||
|
||||
|
||||
fpFromInteger ::
|
||||
IsExprBuilder sym =>
|
||||
sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> IO (SFloat sym)
|
||||
fpFromInteger sym e p r x = fpFromReal sym e p r =<< integerToReal sym x
|
||||
|
||||
|
||||
fpFromRational ::
|
||||
IsExprBuilder sym =>
|
||||
sym -> Integer -> Integer -> RoundingMode ->
|
||||
SymInteger sym -> SymInteger sym -> IO (SFloat sym)
|
||||
fpFromRational sym e p r x y =
|
||||
do num <- integerToReal sym x
|
||||
den <- integerToReal sym y
|
||||
res <- realDiv sym num den
|
||||
fpFromReal sym e p r res
|
||||
|
||||
{- | Returns a predicate and two integers, @x@ and @y@.
|
||||
If the the predicate holds, then @x / y@ is a rational representing
|
||||
the floating point number. Assumes the FP number is not one of the
|
||||
special ones that has no real representation. -}
|
||||
fpToRational ::
|
||||
IsSymExprBuilder sym =>
|
||||
sym ->
|
||||
SFloat sym ->
|
||||
IO (Pred sym, SymInteger sym, SymInteger sym)
|
||||
fpToRational sym fp =
|
||||
do r <- fpToReal sym fp
|
||||
x <- freshConstant sym emptySymbol BaseIntegerRepr
|
||||
y <- freshConstant sym emptySymbol BaseIntegerRepr
|
||||
num <- integerToReal sym x
|
||||
den <- integerToReal sym y
|
||||
res <- realDiv sym num den
|
||||
same <- realEq sym r res
|
||||
pure (same, x, y)
|
||||
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
fpIsInf :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
|
||||
fpIsInf sym (SFloat x) = floatIsInf sym x
|
||||
|
||||
fpIsNaN :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
|
||||
fpIsNaN sym (SFloat x) = floatIsNaN sym x
|
||||
|
||||
|
||||
|
||||
@ -27,7 +27,7 @@ module Cryptol.Eval.Concrete
|
||||
|
||||
import Control.Monad (guard, zipWithM, foldM, mzero)
|
||||
import Data.Bits (Bits(..))
|
||||
import Data.Ratio((%),numerator,denominator)
|
||||
import Data.Ratio(numerator,denominator)
|
||||
import Data.Word(Word32, Word64)
|
||||
import MonadLib( ChoiceT, findOne, lift )
|
||||
import qualified LibBF as FP
|
||||
@ -153,7 +153,7 @@ floatToExpr prims eT pT f =
|
||||
primTable :: IO EvalOpts -> Map PrimIdent (Prim Concrete)
|
||||
primTable getEOpts = let sym = Concrete in
|
||||
Map.union (genericPrimTable sym getEOpts) $
|
||||
Map.union (floatPrims sym) $
|
||||
Map.union (genericFloatTable sym) $
|
||||
Map.union suiteBPrims $
|
||||
Map.union primeECPrims $
|
||||
|
||||
@ -645,55 +645,3 @@ updateBack_word (Nat n) _eltTy bs (Left idx) val = do
|
||||
updateBack_word (Nat n) _eltTy bs (Right w) val = do
|
||||
idx <- bvVal <$> asWordVal Concrete w
|
||||
updateWordValue Concrete bs (n - idx - 1) (fromVBit <$> val)
|
||||
|
||||
|
||||
floatPrims :: Concrete -> Map PrimIdent (Prim Concrete)
|
||||
floatPrims sym = Map.fromList [ (floatPrim i,v) | (i,v) <- nonInfixTable ]
|
||||
where
|
||||
(~>) = (,)
|
||||
nonInfixTable =
|
||||
[ "fpNaN" ~> PFinPoly \e -> PFinPoly \p -> PVal $
|
||||
VFloat BF { bfValue = FP.bfNaN
|
||||
, bfExpWidth = e, bfPrecWidth = p }
|
||||
|
||||
, "fpPosInf" ~> PFinPoly \e -> PFinPoly \p -> PVal $
|
||||
VFloat BF { bfValue = FP.bfPosInf
|
||||
, bfExpWidth = e, bfPrecWidth = p }
|
||||
|
||||
, "fpFromBits" ~> PFinPoly \e -> PFinPoly \p -> PWordFun \bv -> PVal $
|
||||
VFloat $ floatFromBits e p $ bvVal bv
|
||||
|
||||
, "fpToBits" ~> PFinPoly \e -> PFinPoly \p -> PFloatFun \x -> PVal
|
||||
$ word sym (e + p)
|
||||
$ floatToBits e p
|
||||
$ bfValue x
|
||||
, "=.=" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x -> PFloatFun \y -> PVal
|
||||
$ VBit
|
||||
$ bitLit sym
|
||||
$ FP.bfCompare (bfValue x) (bfValue y) == EQ
|
||||
|
||||
, "fpIsFinite" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x -> PVal
|
||||
$ VBit $ bitLit sym $ FP.bfIsFinite $ bfValue x
|
||||
|
||||
-- From Backend class
|
||||
, "fpAdd" ~> fpBinArithV sym fpPlus
|
||||
, "fpSub" ~> fpBinArithV sym fpMinus
|
||||
, "fpMul" ~> fpBinArithV sym fpMult
|
||||
, "fpDiv" ~> fpBinArithV sym fpDiv
|
||||
|
||||
, "fpFromRational" ~>
|
||||
PFinPoly \e -> PFinPoly \p -> PWordFun \r -> PFun \x ->
|
||||
PPrim
|
||||
do rat <- fromVRational <$> x
|
||||
VFloat <$> do mode <- fpRoundMode sym r
|
||||
pure $ floatFromRational e p mode
|
||||
$ sNum rat % sDenom rat
|
||||
, "fpToRational" ~>
|
||||
PFinPoly \_e -> PFinPoly \_p -> PFloatFun \fp ->
|
||||
PPrim
|
||||
case floatToRational "fpToRational" fp of
|
||||
Left err -> raiseError sym err
|
||||
Right r -> pure $
|
||||
VRational
|
||||
SRational { sNum = numerator r, sDenom = denominator r }
|
||||
]
|
||||
|
||||
@ -43,7 +43,7 @@ import Cryptol.Testing.Random( randomValue )
|
||||
import Cryptol.Eval.Prims
|
||||
import Cryptol.Eval.Type
|
||||
import Cryptol.Eval.Value
|
||||
import Cryptol.Utils.Ident (PrimIdent, prelPrim)
|
||||
import Cryptol.Utils.Ident (PrimIdent, prelPrim, floatPrim)
|
||||
import Cryptol.Utils.Logger(logPrint)
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.Utils.PP
|
||||
@ -1957,6 +1957,7 @@ mergeValue sym c v1 v2 =
|
||||
(VBit b1 , VBit b2 ) -> VBit <$> iteBit sym c b1 b2
|
||||
(VInteger i1 , VInteger i2 ) -> VInteger <$> iteInteger sym c i1 i2
|
||||
(VRational q1, VRational q2) -> VRational <$> iteRational sym c q1 q2
|
||||
(VFloat f1 , VFloat f2) -> VFloat <$> iteFloat sym c f1 f2
|
||||
(VWord n1 w1 , VWord n2 w2 ) | n1 == n2 -> pure $ VWord n1 $ mergeWord' sym c w1 w2
|
||||
(VSeq n1 vs1 , VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 <$> memoMap sym (mergeSeqMap sym c vs1 vs2)
|
||||
(VStream vs1 , VStream vs2 ) -> VStream <$> memoMap sym (mergeSeqMap sym c vs1 vs2)
|
||||
@ -2092,6 +2093,16 @@ sparkParMap sym f n m =
|
||||
--------------------------------------------------------------------------------
|
||||
-- Floating Point Operations
|
||||
|
||||
-- | A helper for definitng floating point constants.
|
||||
fpConst ::
|
||||
Backend sym =>
|
||||
(Integer -> Integer -> SEval sym (SFloat sym)) ->
|
||||
Prim sym
|
||||
fpConst mk =
|
||||
PFinPoly \e ->
|
||||
PNumPoly \ ~(Nat p) ->
|
||||
PPrim (VFloat <$> mk e p)
|
||||
|
||||
-- | Make a Cryptol value for a binary arithmetic function.
|
||||
fpBinArithV :: Backend sym => sym -> FPArith2 sym -> Prim sym
|
||||
fpBinArithV sym fun =
|
||||
@ -2113,6 +2124,63 @@ fpRndRTN sym = wordLit sym 3 3 {- to -inf -}
|
||||
fpRndRTZ sym = wordLit sym 3 4 {- to 0 -}
|
||||
|
||||
|
||||
{-# SPECIALIZE genericFloatTable :: Concrete -> Map PrimIdent (Prim Concrete) #-}
|
||||
|
||||
genericFloatTable :: Backend sym => sym -> Map PrimIdent (Prim sym)
|
||||
genericFloatTable sym =
|
||||
let (~>) = (,) in
|
||||
Map.fromList $ map (\(n, v) -> (floatPrim n, v))
|
||||
[ "fpNaN" ~> fpConst (fpNaN sym)
|
||||
, "fpPosInf" ~> fpConst (fpPosInf sym)
|
||||
, "fpFromBits" ~> PFinPoly \e -> PFinPoly \p -> PWordFun \w ->
|
||||
PPrim (VFloat <$> fpFromBits sym e p w)
|
||||
, "fpToBits" ~> PFinPoly \e -> PFinPoly \p -> PFloatFun \x -> PVal
|
||||
$ VWord (e+p)
|
||||
$ WordVal <$> fpToBits sym x
|
||||
, "=.=" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x -> PFloatFun \y ->
|
||||
PPrim (VBit <$> fpLogicalEq sym x y)
|
||||
|
||||
, "fpIsNaN" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->
|
||||
PPrim (VBit <$> fpIsNaN sym x)
|
||||
, "fpIsInf" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->
|
||||
PPrim (VBit <$> fpIsInf sym x)
|
||||
, "fpIsZero" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->
|
||||
PPrim (VBit <$> fpIsZero sym x)
|
||||
, "fpIsNeg" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->
|
||||
PPrim (VBit <$> fpIsNeg sym x)
|
||||
, "fpIsNormal" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->
|
||||
PPrim (VBit <$> fpIsNorm sym x)
|
||||
, "fpIsSubnormal" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->
|
||||
PPrim (VBit <$> fpIsSubnorm sym x)
|
||||
|
||||
, "fpAdd" ~> fpBinArithV sym fpPlus
|
||||
, "fpSub" ~> fpBinArithV sym fpMinus
|
||||
, "fpMul" ~> fpBinArithV sym fpMult
|
||||
, "fpDiv" ~> fpBinArithV sym fpDiv
|
||||
, "fpFMA" ~> PFinPoly \_ -> PFinPoly \_ -> PWordFun \r ->
|
||||
PFloatFun \x -> PFloatFun \y -> PFloatFun \z ->
|
||||
PPrim (VFloat <$> fpFMA sym r x y z)
|
||||
|
||||
, "fpAbs" ~> PFinPoly \_ -> PFinPoly \_ ->
|
||||
PFloatFun \x ->
|
||||
PPrim (VFloat <$> fpAbs sym x)
|
||||
|
||||
, "fpSqrt" ~> PFinPoly \_ -> PFinPoly \_ ->
|
||||
PWordFun \r -> PFloatFun \x ->
|
||||
PPrim (VFloat <$> fpSqrt sym r x)
|
||||
|
||||
, "fpToRational" ~>
|
||||
PFinPoly \_e -> PFinPoly \_p -> PFloatFun \x ->
|
||||
PPrim (VRational <$> fpToRational sym x)
|
||||
|
||||
, "fpFromRational" ~>
|
||||
PFinPoly \e -> PFinPoly \p -> PWordFun \r -> PFun \x ->
|
||||
PPrim
|
||||
do rat <- fromVRational <$> x
|
||||
VFloat <$> fpFromRational sym e p r rat
|
||||
|
||||
]
|
||||
|
||||
|
||||
{-# SPECIALIZE genericPrimTable :: Concrete -> IO EvalOpts -> Map PrimIdent (Prim Concrete) #-}
|
||||
|
||||
|
||||
@ -18,7 +18,6 @@
|
||||
module Cryptol.Eval.What4
|
||||
( Value
|
||||
, primTable
|
||||
, floatPrims
|
||||
) where
|
||||
|
||||
import qualified Control.Exception as X
|
||||
@ -27,7 +26,6 @@ import Control.Monad (foldM)
|
||||
import Control.Monad.IO.Class
|
||||
import Data.Bits
|
||||
import qualified Data.Map as Map
|
||||
import Data.Map (Map)
|
||||
import qualified Data.Set as Set
|
||||
import Data.Text (Text)
|
||||
import qualified Data.Text as Text
|
||||
@ -43,7 +41,6 @@ import qualified What4.Utils.AbstractDomains as W4
|
||||
import Cryptol.Backend
|
||||
import Cryptol.Backend.Monad ( EvalError(..), Unsupported(..) )
|
||||
import Cryptol.Backend.What4
|
||||
import qualified Cryptol.Backend.What4.SFloat as W4
|
||||
|
||||
import Cryptol.Eval.Generic
|
||||
import Cryptol.Eval.Prims
|
||||
@ -64,9 +61,9 @@ type Value sym = GenValue (What4 sym)
|
||||
primTable :: W4.IsSymExprBuilder sym => What4 sym -> IO EvalOpts -> Map.Map PrimIdent (Prim (What4 sym))
|
||||
primTable sym getEOpts =
|
||||
let w4sym = w4 sym in
|
||||
Map.union (floatPrims sym) $
|
||||
Map.union (suiteBPrims sym) $
|
||||
Map.union (primeECPrims sym) $
|
||||
Map.union (genericFloatTable sym) $
|
||||
Map.union (genericPrimTable sym getEOpts) $
|
||||
|
||||
Map.fromList $ map (\(n, v) -> (prelPrim n, v))
|
||||
@ -859,56 +856,3 @@ updateBackSym_word sym (Nat n) eltTy bv (Right wv) val =
|
||||
|
||||
_ -> LargeBitsVal (wordValueSize sym wv) <$>
|
||||
updateBackSym sym (Nat n) eltTy (asBitsMap sym bv) (Right wv) val
|
||||
|
||||
|
||||
|
||||
-- | Table of floating point primitives
|
||||
floatPrims :: W4.IsSymExprBuilder sym => What4 sym -> Map PrimIdent (Prim (What4 sym))
|
||||
floatPrims sym =
|
||||
Map.fromList [ (floatPrim i,v) | (i,v) <- nonInfixTable ]
|
||||
where
|
||||
w4sym = w4 sym
|
||||
(~>) = (,)
|
||||
|
||||
nonInfixTable =
|
||||
[ "fpNaN" ~> fpConst (W4.fpNaN w4sym)
|
||||
, "fpPosInf" ~> fpConst (W4.fpPosInf w4sym)
|
||||
, "fpFromBits" ~> PFinPoly \e -> PFinPoly \p -> PWordFun \w ->
|
||||
PPrim (VFloat <$> liftIO (W4.fpFromBinary w4sym e p w))
|
||||
, "fpToBits" ~> PFinPoly \e -> PFinPoly \p -> PFloatFun \x -> PVal
|
||||
$ VWord (e+p)
|
||||
$ WordVal <$> liftIO (W4.fpToBinary w4sym x)
|
||||
, "=.=" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x -> PFloatFun \y ->
|
||||
PPrim (VBit <$> liftIO (W4.fpEq w4sym x y))
|
||||
, "fpIsFinite" ~> PFinPoly \_ -> PFinPoly \_ -> PFloatFun \x ->
|
||||
PPrim
|
||||
(VBit <$> liftIO do inf <- W4.fpIsInf w4sym x
|
||||
nan <- W4.fpIsNaN w4sym x
|
||||
weird <- W4.orPred w4sym inf nan
|
||||
W4.notPred w4sym weird)
|
||||
|
||||
, "fpAdd" ~> fpBinArithV sym fpPlus
|
||||
, "fpSub" ~> fpBinArithV sym fpMinus
|
||||
, "fpMul" ~> fpBinArithV sym fpMult
|
||||
, "fpDiv" ~> fpBinArithV sym fpDiv
|
||||
|
||||
, "fpFromRational" ~>
|
||||
PFinPoly \e -> PFinPoly \p -> PWordFun \r -> PFun \x ->
|
||||
PPrim
|
||||
do rat <- fromVRational <$> x
|
||||
VFloat <$> fpCvtFromRational sym e p r rat
|
||||
|
||||
, "fpToRational" ~>
|
||||
PFinPoly \_e -> PFinPoly \_p -> PFloatFun \fp ->
|
||||
PPrim (VRational <$> fpCvtToRational sym fp)
|
||||
]
|
||||
|
||||
-- | A helper for definitng floating point constants.
|
||||
fpConst ::
|
||||
W4.IsSymExprBuilder sym =>
|
||||
(Integer -> Integer -> IO (W4.SFloat sym)) ->
|
||||
Prim (What4 sym)
|
||||
fpConst mk =
|
||||
PFinPoly \e ->
|
||||
PNumPoly \ ~(Nat p) ->
|
||||
PPrim (VFloat <$> liftIO (mk e p))
|
||||
|
||||
@ -56,7 +56,6 @@ import qualified Cryptol.ModuleSystem.Name as M
|
||||
|
||||
import qualified Cryptol.Backend.FloatHelpers as FH
|
||||
import Cryptol.Backend.What4
|
||||
import qualified Cryptol.Backend.What4.SFloat as W4
|
||||
|
||||
import qualified Cryptol.Eval as Eval
|
||||
import qualified Cryptol.Eval.Concrete as Concrete
|
||||
@ -73,6 +72,7 @@ import qualified What4.Interface as W4
|
||||
import qualified What4.Expr.Builder as W4
|
||||
import qualified What4.Expr.GroundEval as W4
|
||||
import qualified What4.SatResult as W4
|
||||
import qualified What4.SFloat as W4
|
||||
import qualified What4.SWord as SW
|
||||
import What4.Solver
|
||||
import qualified What4.Solver.Adapter as W4
|
||||
|
||||
Loading…
Reference in New Issue
Block a user