cryptol-2.11.0: src/Cryptol/Backend/What4.hs
-- |
-- Module : Cryptol.Backend.What4
-- Copyright : (c) 2020 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.Backend.What4 where
import qualified Control.Exception as X
import Control.Concurrent.MVar
import Control.Monad (foldM,ap,liftM)
import Control.Monad.IO.Class
import Data.Bits (bit)
import qualified Data.BitVector.Sized as BV
import Data.List
import Data.Map (Map)
import Data.Set (Set)
import Data.Text (Text)
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import qualified GHC.Integer.GMP.Internals as Integer
import qualified What4.Interface as W4
import qualified What4.SWord as SW
import qualified What4.SFloat as FP
import Cryptol.Backend
import Cryptol.Backend.FloatHelpers
import Cryptol.Backend.Monad
( Eval(..), EvalError(..), EvalErrorEx(..)
, Unsupported(..), delayFill, blackhole, evalSpark
, modifyCallStack, getCallStack
)
import Cryptol.Utils.Panic
data What4 sym =
What4
{ w4 :: sym
, w4defs :: MVar (W4.Pred sym)
, w4funs :: MVar (What4FunCache sym)
, w4uninterpWarns :: MVar (Set Text)
}
type What4FunCache sym = Map Text (SomeSymFn sym)
data SomeSymFn sym =
forall args ret. SomeSymFn (W4.SymFn sym args ret)
{- | This is the monad used for symbolic evaluation. It adds to
aspects to 'Eval'---'WConn' keeps track of the backend and collects
definitional predicates, and 'W4Eval` adds support for partially
defined values -}
newtype W4Eval sym a = W4Eval { evalPartial :: W4Conn sym (W4Result sym a) }
{- | This layer has the symbolic back-end, and can keep track of definitional
predicates used when working with uninterpreted constants defined
via a property. -}
newtype W4Conn sym a = W4Conn { evalConn :: sym -> Eval a }
-- | The symbolic value we computed.
data W4Result sym a
= W4Error !EvalErrorEx
-- ^ A malformed value
| W4Result !(W4.Pred sym) !a
-- ^ safety predicate and result: the result only makes sense when
-- the predicate holds.
--------------------------------------------------------------------------------
-- Moving between the layers
w4Eval :: W4Eval sym a -> sym -> Eval (W4Result sym a)
w4Eval (W4Eval (W4Conn m)) = m
w4Thunk :: Eval (W4Result sym a) -> W4Eval sym a
w4Thunk m = W4Eval (W4Conn \_ -> m)
-- | A value with no context.
doEval :: W4.IsSymExprBuilder sym => Eval a -> W4Conn sym a
doEval m = W4Conn \_sym -> m
-- | A total value.
total :: W4.IsSymExprBuilder sym => W4Conn sym a -> W4Eval sym a
total m = W4Eval
do sym <- getSym
W4Result (W4.backendPred sym True) <$> m
--------------------------------------------------------------------------------
-- Operations in WConn
instance W4.IsSymExprBuilder sym => Functor (W4Conn sym) where
fmap = liftM
instance W4.IsSymExprBuilder sym => Applicative (W4Conn sym) where
pure = doEval . pure
(<*>) = ap
instance W4.IsSymExprBuilder sym => Monad (W4Conn sym) where
m1 >>= f = W4Conn \sym ->
do res1 <- evalConn m1 sym
evalConn (f res1) sym
instance W4.IsSymExprBuilder sym => MonadIO (W4Conn sym) where
liftIO = doEval . liftIO
-- | Access the symbolic back-end
getSym :: W4Conn sym sym
getSym = W4Conn \sym -> pure sym
-- | Record a definition.
--addDef :: W4.Pred sym -> W4Conn sym ()
--addDef p = W4Conn \_ -> pure W4Defs { w4Defs = p, w4Result = () }
-- | Compute conjunction.
w4And :: W4.IsSymExprBuilder sym =>
W4.Pred sym -> W4.Pred sym -> W4Conn sym (W4.Pred sym)
w4And p q =
do sym <- getSym
liftIO (W4.andPred sym p q)
-- | Compute negation.
w4Not :: W4.IsSymExprBuilder sym => W4.Pred sym -> W4Conn sym (W4.Pred sym)
w4Not p =
do sym <- getSym
liftIO (W4.notPred sym p)
-- | Compute if-then-else.
w4ITE :: W4.IsSymExprBuilder sym =>
W4.Pred sym -> W4.Pred sym -> W4.Pred sym -> W4Conn sym (W4.Pred sym)
w4ITE ifP ifThen ifElse =
do sym <- getSym
liftIO (W4.itePred sym ifP ifThen ifElse)
--------------------------------------------------------------------------------
-- Operations in W4Eval
instance W4.IsSymExprBuilder sym => Functor (W4Eval sym) where
fmap = liftM
instance W4.IsSymExprBuilder sym => Applicative (W4Eval sym) where
pure = total . pure
(<*>) = ap
instance W4.IsSymExprBuilder sym => Monad (W4Eval sym) where
m1 >>= f = W4Eval
do res1 <- evalPartial m1
case res1 of
W4Error err -> pure (W4Error err)
W4Result px x' ->
do res2 <- evalPartial (f x')
case res2 of
W4Result py y ->
do pz <- w4And px py
pure (W4Result pz y)
W4Error _ -> pure res2
instance W4.IsSymExprBuilder sym => MonadIO (W4Eval sym) where
liftIO = total . liftIO
-- | Add a definitional equation.
-- This will always be asserted when we make queries to the solver.
addDefEqn :: W4.IsSymExprBuilder sym => What4 sym -> W4.Pred sym -> W4Eval sym ()
addDefEqn sym p =
liftIO (modifyMVar_ (w4defs sym) (W4.andPred (w4 sym) p))
-- | Add s safety condition.
addSafety :: W4.IsSymExprBuilder sym => W4.Pred sym -> W4Eval sym ()
addSafety p = W4Eval (pure (W4Result p ()))
-- | A fully undefined symbolic value
evalError :: W4.IsSymExprBuilder sym => EvalError -> W4Eval sym a
evalError err = W4Eval $ W4Conn $ \_sym ->
do stk <- getCallStack
pure (W4Error (EvalErrorEx stk err))
--------------------------------------------------------------------------------
assertBVDivisor :: W4.IsSymExprBuilder sym => What4 sym -> SW.SWord sym -> W4Eval sym ()
assertBVDivisor sym x =
do p <- liftIO (SW.bvIsNonzero (w4 sym) x)
assertSideCondition sym p DivideByZero
assertIntDivisor ::
W4.IsSymExprBuilder sym => What4 sym -> W4.SymInteger sym -> W4Eval sym ()
assertIntDivisor sym x =
do p <- liftIO (W4.notPred (w4 sym) =<< W4.intEq (w4 sym) x =<< W4.intLit (w4 sym) 0)
assertSideCondition sym p DivideByZero
instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
type SBit (What4 sym) = W4.Pred sym
type SWord (What4 sym) = SW.SWord sym
type SInteger (What4 sym) = W4.SymInteger sym
type SFloat (What4 sym) = FP.SFloat sym
type SEval (What4 sym) = W4Eval sym
raiseError _ = evalError
assertSideCondition _ cond err
| Just False <- W4.asConstantPred cond = evalError err
| otherwise = addSafety cond
isReady sym m =
case w4Eval m (w4 sym) of
Ready _ -> True
_ -> False
sDelayFill _ m retry msg =
total
do sym <- getSym
doEval (w4Thunk <$> delayFill (w4Eval m sym) (w4Eval <$> retry <*> pure sym) msg)
sSpark _ m =
total
do sym <- getSym
doEval (w4Thunk <$> evalSpark (w4Eval m sym))
sModifyCallStack _ f (W4Eval (W4Conn m)) =
W4Eval (W4Conn \sym -> modifyCallStack f (m sym))
sGetCallStack _ = total (doEval getCallStack)
sDeclareHole _ msg =
total
do (hole, fill) <- doEval (blackhole msg)
pure ( w4Thunk hole
, \m -> total
do sym <- getSym
doEval (fill (w4Eval m sym))
)
mergeEval _sym f c mx my = W4Eval
do rx <- evalPartial mx
ry <- evalPartial my
case (rx, ry) of
(W4Error err, W4Error _) ->
pure (W4Error err) -- arbitrarily choose left error to report
(W4Error _, W4Result p y) ->
do p' <- w4And p =<< w4Not c
pure (W4Result p' y)
(W4Result p x, W4Error _) ->
do p' <- w4And p c
pure (W4Result p' x)
(W4Result px x, W4Result py y) ->
do zr <- evalPartial (f c x y)
case zr of
W4Error err -> pure $ W4Error err
W4Result pz z ->
do p' <- w4And pz =<< w4ITE c px py
pure (W4Result p' z)
wordAsChar _ bv
| SW.bvWidth bv == 8 = toEnum . fromInteger <$> SW.bvAsUnsignedInteger bv
| otherwise = Nothing
wordLen _ bv = SW.bvWidth bv
bitLit sym b = W4.backendPred (w4 sym) b
bitAsLit _ v = W4.asConstantPred v
wordLit sym intw i
| Just (Some w) <- someNat intw
= case isPosNat w of
Nothing -> pure $ SW.ZBV
Just LeqProof -> SW.DBV <$> liftIO (W4.bvLit (w4 sym) w (BV.mkBV w i))
| otherwise = panic "what4: wordLit" ["invalid bit width:", show intw ]
wordAsLit _ v
| Just x <- SW.bvAsUnsignedInteger v = Just (SW.bvWidth v, x)
| otherwise = Nothing
integerLit sym i = liftIO (W4.intLit (w4 sym) i)
integerAsLit _ v = W4.asInteger v
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)
bitOr sym x y = liftIO (W4.orPred (w4 sym) x y)
bitXor sym x y = liftIO (W4.xorPred (w4 sym) x y)
bitComplement sym x = liftIO (W4.notPred (w4 sym) x)
wordBit sym bv idx = liftIO (SW.bvAtBE (w4 sym) bv idx)
wordUpdate sym bv idx b = liftIO (SW.bvSetBE (w4 sym) bv idx b)
packWord sym bs =
do z <- wordLit sym (genericLength bs) 0
let f w (idx,b) = wordUpdate sym w idx b
foldM f z (zip [0..] bs)
unpackWord sym bv = liftIO $
mapM (SW.bvAtBE (w4 sym) bv) [0 .. SW.bvWidth bv-1]
joinWord sym x y = liftIO $ SW.bvJoin (w4 sym) x y
splitWord _sym 0 _ bv = pure (SW.ZBV, bv)
splitWord _sym _ 0 bv = pure (bv, SW.ZBV)
splitWord sym lw rw bv = liftIO $
do l <- SW.bvSliceBE (w4 sym) 0 lw bv
r <- SW.bvSliceBE (w4 sym) lw rw bv
return (l, r)
extractWord sym bits idx bv =
liftIO $ SW.bvSliceLE (w4 sym) idx bits bv
wordEq sym x y = liftIO (SW.bvEq (w4 sym) x y)
wordLessThan sym x y = liftIO (SW.bvult (w4 sym) x y)
wordGreaterThan sym x y = liftIO (SW.bvugt (w4 sym) x y)
wordSignedLessThan sym x y = liftIO (SW.bvslt (w4 sym) x y)
wordOr sym x y = liftIO (SW.bvOr (w4 sym) x y)
wordAnd sym x y = liftIO (SW.bvAnd (w4 sym) x y)
wordXor sym x y = liftIO (SW.bvXor (w4 sym) x y)
wordComplement sym x = liftIO (SW.bvNot (w4 sym) x)
wordPlus sym x y = liftIO (SW.bvAdd (w4 sym) x y)
wordMinus sym x y = liftIO (SW.bvSub (w4 sym) x y)
wordMult sym x y = liftIO (SW.bvMul (w4 sym) x y)
wordNegate sym x = liftIO (SW.bvNeg (w4 sym) x)
wordLg2 sym x = sLg2 (w4 sym) x
wordDiv sym x y =
do assertBVDivisor sym y
liftIO (SW.bvUDiv (w4 sym) x y)
wordMod sym x y =
do assertBVDivisor sym y
liftIO (SW.bvURem (w4 sym) x y)
wordSignedDiv sym x y =
do assertBVDivisor sym y
liftIO (SW.bvSDiv (w4 sym) x y)
wordSignedMod sym x y =
do assertBVDivisor sym y
liftIO (SW.bvSRem (w4 sym) x y)
wordToInt sym x = liftIO (SW.bvToInteger (w4 sym) x)
wordFromInt sym width i = liftIO (SW.integerToBV (w4 sym) i width)
intPlus sym x y = liftIO $ W4.intAdd (w4 sym) x y
intMinus sym x y = liftIO $ W4.intSub (w4 sym) x y
intMult sym x y = liftIO $ W4.intMul (w4 sym) x y
intNegate sym x = liftIO $ W4.intNeg (w4 sym) x
-- NB: What4's division operation provides SMTLib's euclidean division,
-- which doesn't match the round-to-neg-infinity semantics of Cryptol,
-- so we have to do some work to get the desired semantics.
intDiv sym x y =
do assertIntDivisor sym y
liftIO $ do
neg <- liftIO (W4.intLt (w4 sym) y =<< W4.intLit (w4 sym) 0)
case W4.asConstantPred neg of
Just False -> W4.intDiv (w4 sym) x y
Just True ->
do xneg <- W4.intNeg (w4 sym) x
yneg <- W4.intNeg (w4 sym) y
W4.intDiv (w4 sym) xneg yneg
Nothing ->
do xneg <- W4.intNeg (w4 sym) x
yneg <- W4.intNeg (w4 sym) y
zneg <- W4.intDiv (w4 sym) xneg yneg
z <- W4.intDiv (w4 sym) x y
W4.intIte (w4 sym) neg zneg z
-- NB: What4's division operation provides SMTLib's euclidean division,
-- which doesn't match the round-to-neg-infinity semantics of Cryptol,
-- so we have to do some work to get the desired semantics.
intMod sym x y =
do assertIntDivisor sym y
liftIO $ do
neg <- liftIO (W4.intLt (w4 sym) y =<< W4.intLit (w4 sym) 0)
case W4.asConstantPred neg of
Just False -> W4.intMod (w4 sym) x y
Just True ->
do xneg <- W4.intNeg (w4 sym) x
yneg <- W4.intNeg (w4 sym) y
W4.intNeg (w4 sym) =<< W4.intMod (w4 sym) xneg yneg
Nothing ->
do xneg <- W4.intNeg (w4 sym) x
yneg <- W4.intNeg (w4 sym) y
z <- W4.intMod (w4 sym) x y
zneg <- W4.intNeg (w4 sym) =<< W4.intMod (w4 sym) xneg yneg
W4.intIte (w4 sym) neg zneg z
intEq sym x y = liftIO $ W4.intEq (w4 sym) x y
intLessThan sym x y = liftIO $ W4.intLt (w4 sym) x y
intGreaterThan sym x y = liftIO $ W4.intLt (w4 sym) y x
-- NB, we don't do reduction here on symbolic values
intToZn sym m x
| Just xi <- W4.asInteger x
= liftIO $ W4.intLit (w4 sym) (xi `mod` m)
| otherwise
= pure x
znToInt _ 0 _ = evalPanic "znToInt" ["0 modulus not allowed"]
znToInt sym m x = liftIO (W4.intMod (w4 sym) x =<< W4.intLit (w4 sym) m)
znEq _ 0 _ _ = evalPanic "znEq" ["0 modulus not allowed"]
znEq sym m x y = liftIO $
do diff <- W4.intSub (w4 sym) x y
W4.intDivisible (w4 sym) diff (fromInteger m)
znPlus sym m x y = liftIO $ sModAdd (w4 sym) m x y
znMinus sym m x y = liftIO $ sModSub (w4 sym) m x y
znMult sym m x y = liftIO $ sModMult (w4 sym) m x y
znNegate sym m x = liftIO $ sModNegate (w4 sym) m x
znRecip = sModRecip
--------------------------------------------------------------
fpLit sym e p r = liftIO $ FP.fpFromRationalLit (w4 sym) e p r
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
fpLogicalEq sym x y = liftIO $ FP.fpEq (w4 sym) x y
fpPlus = fpBinArith FP.fpAdd
fpMinus = fpBinArith FP.fpSub
fpMult = fpBinArith FP.fpMul
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
liftIO $ FP.fpFromInteger (w4 sym) e p rm x
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"]
sModAdd sym m x y
| Just xi <- W4.asInteger x
, Just yi <- W4.asInteger y
= W4.intLit sym ((xi+yi) `mod` m)
| otherwise
= W4.intAdd sym x y
sModSub :: W4.IsSymExprBuilder sym =>
sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModSub _sym 0 _ _ = evalPanic "sModSub" ["0 modulus not allowed"]
sModSub sym m x y
| Just xi <- W4.asInteger x
, Just yi <- W4.asInteger y
= W4.intLit sym ((xi-yi) `mod` m)
| otherwise
= W4.intSub sym x y
sModMult :: W4.IsSymExprBuilder sym =>
sym -> Integer -> W4.SymInteger sym -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModMult _sym 0 _ _ = evalPanic "sModMult" ["0 modulus not allowed"]
sModMult sym m x y
| Just xi <- W4.asInteger x
, Just yi <- W4.asInteger y
= W4.intLit sym ((xi*yi) `mod` m)
| otherwise
= W4.intMul sym x y
sModNegate :: W4.IsSymExprBuilder sym =>
sym -> Integer -> W4.SymInteger sym -> IO (W4.SymInteger sym)
sModNegate _sym 0 _ = evalPanic "sModMult" ["0 modulus not allowed"]
sModNegate sym m x
| Just xi <- W4.asInteger x
= W4.intLit sym ((negate xi) `mod` m)
| otherwise
= W4.intNeg sym x
-- | Try successive powers of 2 to find the first that dominates the input.
-- We could perhaps reduce to using CLZ instead...
sLg2 :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SEval (What4 sym) (SW.SWord sym)
sLg2 sym x = liftIO $ go 0
where
w = SW.bvWidth x
lit n = SW.bvLit sym w (toInteger n)
go i | toInteger i < w =
do p <- SW.bvule sym x =<< lit (bit i)
lazyIte (SW.bvIte sym) p (lit i) (go (i+1))
-- base case, should only happen when i = w
go i = lit i
-- Errors ----------------------------------------------------------------------
evalPanic :: String -> [String] -> a
evalPanic cxt = panic ("[What4] " ++ cxt)
lazyIte ::
(W4.IsExpr p, Monad m) =>
(p W4.BaseBoolType -> a -> a -> m a) ->
p W4.BaseBoolType ->
m a ->
m a ->
m a
lazyIte f c mx my
| Just b <- W4.asConstantPred c = if b then mx else my
| otherwise =
do x <- mx
y <- my
f c x y
w4bvShl :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvShl sym x y = liftIO $ SW.bvShl sym x y
w4bvLshr :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvLshr sym x y = liftIO $ SW.bvLshr sym x y
w4bvAshr :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvAshr sym x y = liftIO $ SW.bvAshr sym x y
w4bvRol :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvRol sym x y = liftIO $ SW.bvRol sym x y
w4bvRor :: W4.IsSymExprBuilder sym => sym -> SW.SWord sym -> SW.SWord sym -> W4Eval sym (SW.SWord sym)
w4bvRor sym x y = liftIO $ SW.bvRor sym x y
fpRoundingMode ::
W4.IsSymExprBuilder sym =>
What4 sym -> SWord (What4 sym) -> SEval (What4 sym) W4.RoundingMode
fpRoundingMode sym v =
case wordAsLit sym v of
Just (_w,i) ->
case i of
0 -> pure W4.RNE
1 -> pure W4.RNA
2 -> pure W4.RTP
3 -> pure W4.RTN
4 -> pure W4.RTZ
x -> raiseError sym (BadRoundingMode x)
_ -> liftIO $ X.throwIO $ UnsupportedSymbolicOp "rounding mode"
fpBinArith ::
W4.IsSymExprBuilder sym =>
FP.SFloatBinArith sym ->
What4 sym ->
SWord (What4 sym) ->
SFloat (What4 sym) ->
SFloat (What4 sym) ->
SEval (What4 sym) (SFloat (What4 sym))
fpBinArith fun = \sym r x y ->
do m <- fpRoundingMode sym r
liftIO (fun (w4 sym) m x y)
fpCvtToInteger ::
(W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
sym -> String -> SWord sym -> SFloat sym -> SEval sym (SInteger sym)
fpCvtToInteger sym fun r x =
do grd <- liftIO
do bad1 <- FP.fpIsInf (w4 sym) x
bad2 <- FP.fpIsNaN (w4 sym) x
W4.notPred (w4 sym) =<< W4.orPred (w4 sym) bad1 bad2
assertSideCondition sym grd (BadValue fun)
rnd <- fpRoundingMode sym r
liftIO
do y <- FP.fpToReal (w4 sym) x
case rnd of
W4.RNE -> W4.realRoundEven (w4 sym) y
W4.RNA -> W4.realRound (w4 sym) y
W4.RTP -> W4.realCeil (w4 sym) y
W4.RTN -> W4.realFloor (w4 sym) y
W4.RTZ -> W4.realTrunc (w4 sym) y
fpCvtToRational ::
(W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
sym -> SFloat sym -> SEval sym (SRational sym)
fpCvtToRational sym fp =
do grd <- liftIO
do bad1 <- FP.fpIsInf (w4 sym) fp
bad2 <- FP.fpIsNaN (w4 sym) fp
W4.notPred (w4 sym) =<< W4.orPred (w4 sym) bad1 bad2
assertSideCondition sym grd (BadValue "fpToRational")
(rel,x,y) <- liftIO (FP.fpToRational (w4 sym) fp)
addDefEqn sym =<< liftIO (W4.impliesPred (w4 sym) grd rel)
ratio sym x y
fpCvtFromRational ::
(W4.IsSymExprBuilder sy, sym ~ What4 sy) =>
sym -> Integer -> Integer -> SWord sym ->
SRational sym -> SEval sym (SFloat sym)
fpCvtFromRational sym e p r rat =
do rnd <- fpRoundingMode sym r
liftIO (FP.fpFromRational (w4 sym) e p rnd (sNum rat) (sDenom rat))
-- Create a fresh constant and assert that it is the
-- multiplicitive inverse of x; return the constant.
-- Such an inverse must exist under the precondition
-- that the modulus is prime and the input is nonzero.
sModRecip ::
W4.IsSymExprBuilder sym =>
What4 sym ->
Integer ->
W4.SymInteger sym ->
W4Eval sym (W4.SymInteger sym)
sModRecip _sym 0 _ = panic "sModRecip" ["0 modulus not allowed"]
sModRecip sym m x
-- If the input is concrete, evaluate the answer
| Just xi <- W4.asInteger x
= let r = Integer.recipModInteger xi m
in if r == 0 then raiseError sym DivideByZero else integerLit sym r
-- If the input is symbolic, create a new symbolic constant
-- and assert that it is the desired multiplicitive inverse.
-- Such an inverse will exist under the precondition that
-- the modulus is prime, and as long as the input is nonzero.
| otherwise
= do divZero <- liftIO (W4.intDivisible (w4 sym) x (fromInteger m))
ok <- liftIO (W4.notPred (w4 sym) divZero)
assertSideCondition sym ok DivideByZero
z <- liftIO (W4.freshBoundedInt (w4 sym) W4.emptySymbol (Just 1) (Just (m-1)))
xz <- liftIO (W4.intMul (w4 sym) x z)
rel <- znEq sym m xz =<< liftIO (W4.intLit (w4 sym) 1)
addDefEqn sym =<< liftIO (W4.orPred (w4 sym) divZero rel)
return z