{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module What4.Interface
(
SymExpr
, BoundVar
, SymFn
, SymAnnotation
, IsExpr(..)
, IsSymFn(..)
, UnfoldPolicy(..)
, shouldUnfold
, IsExprBuilder(..)
, IsSymExprBuilder(..)
, SolverEvent(..)
, bvJoinVector
, bvSplitVector
, bvSwap
, bvBitreverse
, RoundingMode(..)
, Statistics(..)
, zeroStatistics
, Pred
, SymNat
, SymInteger
, SymReal
, SymFloat
, SymString
, SymCplx
, SymStruct
, SymBV
, SymArray
, IndexLit(..)
, indexLit
, ArrayResultWrapper(..)
, asConcrete
, concreteToSym
, baseIsConcrete
, baseDefaultValue
, realExprAsInteger
, rationalAsInteger
, cplxExprAsRational
, cplxExprAsInteger
, SymEncoder(..)
, backendPred
, andAllOf
, orOneOf
, itePredM
, iteM
, predToReal
, cplxDiv
, cplxLog
, cplxLogBase
, mkRational
, mkReal
, isNonZero
, isReal
, muxRange
, module Data.Parameterized.NatRepr
, module What4.BaseTypes
, HasAbsValue
, What4.Symbol.SolverSymbol
, What4.Symbol.emptySymbol
, What4.Symbol.userSymbol
, What4.Symbol.safeSymbol
, NatValueRange(..)
, ValueRange(..)
, StringLiteral(..)
, stringLiteralInfo
) where
#if !MIN_VERSION_base(4,13,0)
import Control.Monad.Fail( MonadFail )
#endif
import Control.Exception (assert)
import Control.Lens
import Control.Monad
import Control.Monad.IO.Class
import qualified Data.BitVector.Sized as BV
import Data.Coerce (coerce)
import Data.Foldable
import Data.Hashable
import Data.Kind ( Type )
import qualified Data.Map as Map
import Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Ctx
import Data.Parameterized.Utils.Endian (Endian(..))
import Data.Parameterized.NatRepr
import Data.Parameterized.TraversableFC
import qualified Data.Parameterized.Vector as Vector
import Data.Ratio
import Data.Scientific (Scientific)
import GHC.Generics (Generic)
import Numeric.Natural
import Text.PrettyPrint.ANSI.Leijen (Doc)
import What4.BaseTypes
import What4.Config
import qualified What4.Expr.ArrayUpdateMap as AUM
import What4.IndexLit
import What4.ProgramLoc
import What4.Concrete
import What4.SatResult
import What4.Symbol
import What4.Utils.AbstractDomains
import What4.Utils.Arithmetic
import What4.Utils.Complex
import What4.Utils.StringLiteral
type Pred sym = SymExpr sym BaseBoolType
type SymNat sym = SymExpr sym BaseNatType
type SymInteger sym = SymExpr sym BaseIntegerType
type SymReal sym = SymExpr sym BaseRealType
type SymFloat sym fpp = SymExpr sym (BaseFloatType fpp)
type SymCplx sym = SymExpr sym BaseComplexType
type SymStruct sym flds = SymExpr sym (BaseStructType flds)
type SymArray sym idx b = SymExpr sym (BaseArrayType idx b)
type SymBV sym n = SymExpr sym (BaseBVType n)
type SymString sym si = SymExpr sym (BaseStringType si)
type family SymExpr (sym :: Type) :: BaseType -> Type
type family BoundVar (sym :: Type) :: BaseType -> Type
type family SymAnnotation (sym :: Type) :: BaseType -> Type
itePredM :: (IsExpr (SymExpr sym), IsExprBuilder sym, MonadIO m)
=> sym
-> Pred sym
-> m (Pred sym)
-> m (Pred sym)
-> m (Pred sym)
itePredM sym c mx my =
case asConstantPred c of
Just True -> mx
Just False -> my
Nothing -> do
x <- mx
y <- my
liftIO $ itePred sym c x y
class HasAbsValue e => IsExpr e where
asConstantPred :: e BaseBoolType -> Maybe Bool
asConstantPred _ = Nothing
asNat :: e BaseNatType -> Maybe Natural
asNat _ = Nothing
natBounds :: e BaseNatType -> NatValueRange
asInteger :: e BaseIntegerType -> Maybe Integer
asInteger _ = Nothing
integerBounds :: e BaseIntegerType -> ValueRange Integer
asRational :: e BaseRealType -> Maybe Rational
asRational _ = Nothing
rationalBounds :: e BaseRealType -> ValueRange Rational
asComplex :: e BaseComplexType -> Maybe (Complex Rational)
asComplex _ = Nothing
asBV :: e (BaseBVType w) -> Maybe (BV.BV w)
asBV _ = Nothing
unsignedBVBounds :: (1 <= w) => e (BaseBVType w) -> Maybe (Integer, Integer)
signedBVBounds :: (1 <= w) => e (BaseBVType w) -> Maybe (Integer, Integer)
asAffineVar :: e tp -> Maybe (ConcreteVal tp, e tp, ConcreteVal tp)
asString :: e (BaseStringType si) -> Maybe (StringLiteral si)
asString _ = Nothing
stringInfo :: e (BaseStringType si) -> StringInfoRepr si
stringInfo e =
case exprType e of
BaseStringRepr si -> si
asConstantArray :: e (BaseArrayType idx bt) -> Maybe (e bt)
asConstantArray _ = Nothing
asStruct :: e (BaseStructType flds) -> Maybe (Ctx.Assignment e flds)
asStruct _ = Nothing
exprType :: e tp -> BaseTypeRepr tp
bvWidth :: e (BaseBVType w) -> NatRepr w
bvWidth e =
case exprType e of
BaseBVRepr w -> w
printSymExpr :: e tp -> Doc
newtype ArrayResultWrapper f idx tp =
ArrayResultWrapper { unwrapArrayResult :: f (BaseArrayType idx tp) }
instance TestEquality f => TestEquality (ArrayResultWrapper f idx) where
testEquality (ArrayResultWrapper x) (ArrayResultWrapper y) = do
Refl <- testEquality x y
return Refl
instance HashableF e => HashableF (ArrayResultWrapper e idx) where
hashWithSaltF s (ArrayResultWrapper v) = hashWithSaltF s v
data SolverEvent
= SolverStartSATQuery
{ satQuerySolverName :: !String
, satQueryReason :: !String
}
| SolverEndSATQuery
{ satQueryResult :: !(SatResult () ())
, satQueryError :: !(Maybe String)
}
deriving (Show, Generic)
class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
, TestEquality (SymAnnotation sym), OrdF (SymAnnotation sym)
, HashableF (SymAnnotation sym)
) => IsExprBuilder sym where
getConfiguration :: sym -> Config
setSolverLogListener :: sym -> Maybe (SolverEvent -> IO ()) -> IO ()
getSolverLogListener :: sym -> IO (Maybe (SolverEvent -> IO ()))
logSolverEvent :: sym -> SolverEvent -> IO ()
getStatistics :: sym -> IO Statistics
getStatistics _ = return zeroStatistics
getCurrentProgramLoc :: sym -> IO ProgramLoc
setCurrentProgramLoc :: sym -> ProgramLoc -> IO ()
isEq :: sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
isEq sym x y =
case exprType x of
BaseBoolRepr -> eqPred sym x y
BaseBVRepr{} -> bvEq sym x y
BaseNatRepr -> natEq sym x y
BaseIntegerRepr -> intEq sym x y
BaseRealRepr -> realEq sym x y
BaseFloatRepr{} -> floatEq sym x y
BaseComplexRepr -> cplxEq sym x y
BaseStringRepr{} -> stringEq sym x y
BaseStructRepr{} -> structEq sym x y
BaseArrayRepr{} -> arrayEq sym x y
baseTypeIte :: sym
-> Pred sym
-> SymExpr sym tp
-> SymExpr sym tp
-> IO (SymExpr sym tp)
baseTypeIte sym c x y =
case exprType x of
BaseBoolRepr -> itePred sym c x y
BaseBVRepr{} -> bvIte sym c x y
BaseNatRepr -> natIte sym c x y
BaseIntegerRepr -> intIte sym c x y
BaseRealRepr -> realIte sym c x y
BaseFloatRepr{} -> floatIte sym c x y
BaseStringRepr{} -> stringIte sym c x y
BaseComplexRepr -> cplxIte sym c x y
BaseStructRepr{} -> structIte sym c x y
BaseArrayRepr{} -> arrayIte sym c x y
annotateTerm :: sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
truePred :: sym -> Pred sym
falsePred :: sym -> Pred sym
notPred :: sym -> Pred sym -> IO (Pred sym)
andPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
impliesPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
impliesPred sym x y = do
nx <- notPred sym x
orPred sym y nx
xorPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
eqPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred :: sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
natLit :: sym -> Natural -> IO (SymNat sym)
natAdd :: sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natSub :: sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natMul :: sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natDiv :: sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natMod :: sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natIte :: sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natEq :: sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLe :: sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLt :: sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLt sym x y = notPred sym =<< natLe sym y x
intLit :: sym -> Integer -> IO (SymInteger sym)
intNeg :: sym -> SymInteger sym -> IO (SymInteger sym)
intAdd :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intSub :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intSub sym x y = intAdd sym x =<< intNeg sym y
intMul :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intIte :: sym -> Pred sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intEq :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLe :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt :: sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
intLt sym x y = notPred sym =<< intLe sym y x
intAbs :: sym -> SymInteger sym -> IO (SymInteger sym)
intDiv :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intMod :: sym -> SymInteger sym -> SymInteger sym -> IO (SymInteger sym)
intDivisible :: sym -> SymInteger sym -> Natural -> IO (Pred sym)
bvLit :: (1 <= w) => sym -> NatRepr w -> BV.BV w -> IO (SymBV sym w)
bvConcat :: (1 <= u, 1 <= v)
=> sym
-> SymBV sym u
-> SymBV sym v
-> IO (SymBV sym (u+v))
bvSelect :: forall idx n w. (1 <= n, idx + n <= w)
=> sym
-> NatRepr idx
-> NatRepr n
-> SymBV sym w
-> IO (SymBV sym n)
bvNeg :: (1 <= w)
=> sym
-> SymBV sym w
-> IO (SymBV sym w)
bvAdd :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvSub :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvSub sym x y = bvAdd sym x =<< bvNeg sym y
bvMul :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvUdiv :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvUrem :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvSdiv :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvSrem :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
testBitBV :: (1 <= w)
=> sym
-> Natural
-> SymBV sym w
-> IO (Pred sym)
bvIsNeg :: (1 <= w) => sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym x = bvSlt sym x =<< bvLit sym (bvWidth x) (BV.zero (bvWidth x))
bvIte :: (1 <= w)
=> sym
-> Pred sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvEq :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym)
bvNe :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym)
bvNe sym x y = notPred sym =<< bvEq sym x y
bvUlt :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym)
bvUle :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym)
bvUle sym x y = notPred sym =<< bvUlt sym y x
bvUge :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUge sym x y = bvUle sym y x
bvUgt :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUgt sym x y = bvUlt sym y x
bvSlt :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSgt :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSgt sym x y = bvSlt sym y x
bvSle :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSle sym x y = notPred sym =<< bvSlt sym y x
bvSge :: (1 <= w) => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSge sym x y = notPred sym =<< bvSlt sym x y
bvIsNonzero :: (1 <= w) => sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym x = do
let w = bvWidth x
zro <- bvLit sym w (BV.zero w)
notPred sym =<< bvEq sym x zro
bvShl :: (1 <= w) => sym ->
SymBV sym w ->
SymBV sym w ->
IO (SymBV sym w)
bvLshr :: (1 <= w) => sym ->
SymBV sym w ->
SymBV sym w ->
IO (SymBV sym w)
bvAshr :: (1 <= w) => sym ->
SymBV sym w ->
SymBV sym w ->
IO (SymBV sym w)
bvRol :: (1 <= w) =>
sym ->
SymBV sym w ->
SymBV sym w ->
IO (SymBV sym w)
bvRor :: (1 <= w) =>
sym ->
SymBV sym w ->
SymBV sym w ->
IO (SymBV sym w)
bvZext :: (1 <= u, u+1 <= r) => sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvSext :: (1 <= u, u+1 <= r) => sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
bvTrunc :: (1 <= r, r+1 <= w)
=> sym
-> NatRepr r
-> SymBV sym w
-> IO (SymBV sym r)
bvTrunc sym w x
| LeqProof <- leqTrans
(addIsLeq w (knownNat @1))
(leqProof (incNat w) (bvWidth x))
= bvSelect sym (knownNat @0) w x
bvAndBits :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvOrBits :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvXorBits :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
bvNotBits :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
bvSet :: forall w
. (1 <= w)
=> sym
-> SymBV sym w
-> Natural
-> Pred sym
-> IO (SymBV sym w)
bvSet sym v i p = assert (i < natValue (bvWidth v)) $
do let w = bvWidth v
let mask = BV.bit' w i
pbits <- bvFill sym w p
vbits <- bvAndBits sym v =<< bvLit sym w (BV.complement w mask)
bvXorBits sym vbits =<< bvAndBits sym pbits =<< bvLit sym w mask
bvFill :: forall w. (1 <= w) =>
sym ->
NatRepr w ->
Pred sym ->
IO (SymBV sym w)
minUnsignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
minUnsignedBV sym w = bvLit sym w (BV.zero w)
maxUnsignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
maxUnsignedBV sym w = bvLit sym w (BV.maxUnsigned w)
maxSignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
maxSignedBV sym w = bvLit sym w (BV.maxSigned w)
minSignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
minSignedBV sym w = bvLit sym w (BV.minSigned w)
bvPopcount :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
bvCountLeadingZeros :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
bvCountTrailingZeros :: (1 <= w) => sym -> SymBV sym w -> IO (SymBV sym w)
addUnsignedOF :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym, SymBV sym w)
addUnsignedOF sym x y = do
r <- bvAdd sym x y
ovx <- bvUlt sym r x
ovy <- bvUlt sym r y
ov <- orPred sym ovx ovy
return (ov, r)
addSignedOF :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym, SymBV sym w)
addSignedOF sym x y = do
xy <- bvAdd sym x y
sx <- bvIsNeg sym x
sy <- bvIsNeg sym y
sxy <- bvIsNeg sym xy
not_sx <- notPred sym sx
not_sy <- notPred sym sy
not_sxy <- notPred sym sxy
ov1 <- andPred sym not_sxy =<< andPred sym sx sy
ov2 <- andPred sym sxy =<< andPred sym not_sx not_sy
ov <- orPred sym ov1 ov2
return (ov, xy)
subUnsignedOF ::
(1 <= w) =>
sym ->
SymBV sym w ->
SymBV sym w ->
IO (Pred sym, SymBV sym w)
subUnsignedOF sym x y = do
xy <- bvSub sym x y
ov <- bvUlt sym x y
return (ov, xy)
subSignedOF :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (Pred sym, SymBV sym w)
subSignedOF sym x y = do
xy <- bvSub sym x y
sx <- bvIsNeg sym x
sy <- bvIsNeg sym y
sxy <- bvIsNeg sym xy
ov <- join (pure (andPred sym) <*> xorPred sym sx sxy <*> xorPred sym sx sy)
return (ov, xy)
carrylessMultiply ::
(1 <= w) =>
sym ->
SymBV sym w ->
SymBV sym w ->
IO (SymBV sym (w+w))
carrylessMultiply sym x0 y0
| Just _ <- BV.asUnsigned <$> asBV x0
, Nothing <- BV.asUnsigned <$> asBV y0
= go y0 x0
| otherwise
= go x0 y0
where
go :: (1 <= w) => SymBV sym w -> SymBV sym w -> IO (SymBV sym (w+w))
go x y =
do let w = bvWidth x
let w2 = addNat w w
one_leq_w@LeqProof <- return (leqProof (knownNat @1) w)
LeqProof <- return (leqAdd one_leq_w w)
w_leq_w@LeqProof <- return (leqProof w w)
LeqProof <- return (leqAdd2 w_leq_w one_leq_w)
z <- bvLit sym w2 (BV.zero w2)
x' <- bvZext sym w2 x
xs <- sequence [ do p <- testBitBV sym (BV.asNatural i) y
iteM bvIte sym
p
(bvShl sym x' =<< bvLit sym w2 i)
(return z)
| i <- BV.enumFromToUnsigned (BV.zero w2) (BV.mkBV w2 (intValue w - 1))
]
foldM (bvXorBits sym) z xs
unsignedWideMultiplyBV :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w, SymBV sym w)
unsignedWideMultiplyBV sym x y = do
let w = bvWidth x
let dbl_w = addNat w w
one_leq_w@LeqProof <- return (leqProof (knownNat @1) w)
LeqProof <- return (leqAdd one_leq_w w)
w_leq_w@LeqProof <- return (leqProof w w)
LeqProof <- return (leqAdd2 w_leq_w one_leq_w)
x' <- bvZext sym dbl_w x
y' <- bvZext sym dbl_w y
s <- bvMul sym x' y'
lo <- bvTrunc sym w s
n <- bvLit sym dbl_w (BV.zext dbl_w (BV.width w))
hi <- bvTrunc sym w =<< bvLshr sym s n
return (hi, lo)
mulUnsignedOF ::
(1 <= w) =>
sym ->
SymBV sym w ->
SymBV sym w ->
IO (Pred sym, SymBV sym w)
mulUnsignedOF sym x y =
do let w = bvWidth x
let dbl_w = addNat w w
one_leq_w@LeqProof <- return (leqProof (knownNat @1) w)
LeqProof <- return (leqAdd one_leq_w w)
w_leq_w@LeqProof <- return (leqProof w w)
LeqProof <- return (leqAdd2 w_leq_w one_leq_w)
x' <- bvZext sym dbl_w x
y' <- bvZext sym dbl_w y
s <- bvMul sym x' y'
lo <- bvTrunc sym w s
ov <- bvUgt sym s =<< bvLit sym dbl_w (BV.zext dbl_w (BV.maxUnsigned w))
return (ov, lo)
signedWideMultiplyBV :: (1 <= w)
=> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w, SymBV sym w)
signedWideMultiplyBV sym x y = do
let w = bvWidth x
let dbl_w = addNat w w
one_leq_w@LeqProof <- return (leqProof (knownNat @1) w)
LeqProof <- return (leqAdd one_leq_w w)
w_leq_w@LeqProof <- return (leqProof w w)
LeqProof <- return (leqAdd2 w_leq_w one_leq_w)
x' <- bvSext sym dbl_w x
y' <- bvSext sym dbl_w y
s <- bvMul sym x' y'
lo <- bvTrunc sym w s
n <- bvLit sym dbl_w (BV.zext dbl_w (BV.width w))
hi <- bvTrunc sym w =<< bvLshr sym s n
return (hi, lo)
mulSignedOF ::
(1 <= w) =>
sym ->
SymBV sym w ->
SymBV sym w ->
IO (Pred sym, SymBV sym w)
mulSignedOF sym x y =
do let w = bvWidth x
let dbl_w = addNat w w
one_leq_w@LeqProof <- return (leqProof (knownNat @1) w)
LeqProof <- return (leqAdd one_leq_w w)
w_leq_w@LeqProof <- return (leqProof w w)
LeqProof <- return (leqAdd2 w_leq_w one_leq_w)
x' <- bvSext sym dbl_w x
y' <- bvSext sym dbl_w y
s <- bvMul sym x' y'
lo <- bvTrunc sym w s
ov1 <- bvSlt sym s =<< bvLit sym dbl_w (BV.sext w dbl_w (BV.minSigned w))
ov2 <- bvSgt sym s =<< bvLit sym dbl_w (BV.sext w dbl_w (BV.maxSigned w))
ov <- orPred sym ov1 ov2
return (ov, lo)
mkStruct :: sym
-> Ctx.Assignment (SymExpr sym) flds
-> IO (SymStruct sym flds)
structField :: sym
-> SymStruct sym flds
-> Ctx.Index flds tp
-> IO (SymExpr sym tp)
structEq :: forall flds
. sym
-> SymStruct sym flds
-> SymStruct sym flds
-> IO (Pred sym)
structEq sym x y = do
case exprType x of
BaseStructRepr fld_types -> do
let sz = Ctx.size fld_types
let f :: IO (Pred sym) -> Ctx.Index flds tp -> IO (Pred sym)
f mp i = do
xi <- structField sym x i
yi <- structField sym y i
i_eq <- isEq sym xi yi
case asConstantPred i_eq of
Just True -> mp
Just False -> return (falsePred sym)
_ -> andPred sym i_eq =<< mp
Ctx.forIndex sz f (return (truePred sym))
structIte :: sym
-> Pred sym
-> SymStruct sym flds
-> SymStruct sym flds
-> IO (SymStruct sym flds)
constantArray :: sym
-> Ctx.Assignment BaseTypeRepr (idx::>tp)
-> SymExpr sym b
-> IO (SymArray sym (idx::>tp) b)
arrayFromFn :: sym
-> SymFn sym (idx ::> itp) ret
-> IO (SymArray sym (idx ::> itp) ret)
arrayMap :: sym
-> SymFn sym (ctx::>d) r
-> Ctx.Assignment (ArrayResultWrapper (SymExpr sym) (idx ::> itp)) (ctx::>d)
-> IO (SymArray sym (idx ::> itp) r)
arrayUpdate :: sym
-> SymArray sym (idx::>tp) b
-> Ctx.Assignment (SymExpr sym) (idx::>tp)
-> SymExpr sym b
-> IO (SymArray sym (idx::>tp) b)
arrayLookup :: sym
-> SymArray sym (idx::>tp) b
-> Ctx.Assignment (SymExpr sym) (idx::>tp)
-> IO (SymExpr sym b)
arrayFromMap :: sym
-> Ctx.Assignment BaseTypeRepr (idx ::> itp)
-> AUM.ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
-> SymExpr sym tp
-> IO (SymArray sym (idx ::> itp) tp)
arrayFromMap sym idx_tps m default_value = do
a0 <- constantArray sym idx_tps default_value
arrayUpdateAtIdxLits sym m a0
arrayUpdateAtIdxLits :: sym
-> AUM.ArrayUpdateMap (SymExpr sym) (idx ::> itp) tp
-> SymArray sym (idx ::> itp) tp
-> IO (SymArray sym (idx ::> itp) tp)
arrayUpdateAtIdxLits sym m a0 = do
let updateAt a (i,v) = do
idx <- traverseFC (indexLit sym) i
arrayUpdate sym a idx v
foldlM updateAt a0 (AUM.toList m)
arrayIte :: sym
-> Pred sym
-> SymArray sym idx b
-> SymArray sym idx b
-> IO (SymArray sym idx b)
arrayEq :: sym
-> SymArray sym idx b
-> SymArray sym idx b
-> IO (Pred sym)
allTrueEntries :: sym -> SymArray sym idx BaseBoolType -> IO (Pred sym)
allTrueEntries sym a = do
case exprType a of
BaseArrayRepr idx_tps _ ->
arrayEq sym a =<< constantArray sym idx_tps (truePred sym)
arrayTrueOnEntries
:: sym
-> SymFn sym (idx::>itp) BaseBoolType
-> SymArray sym (idx ::> itp) BaseBoolType
-> IO (Pred sym)
natToInteger :: sym -> SymNat sym -> IO (SymInteger sym)
integerToReal :: sym -> SymInteger sym -> IO (SymReal sym)
bvToNat :: (1 <= w) => sym -> SymBV sym w -> IO (SymNat sym)
bvToInteger :: (1 <= w) => sym -> SymBV sym w -> IO (SymInteger sym)
sbvToInteger :: (1 <= w) => sym -> SymBV sym w -> IO (SymInteger sym)
predToBV :: (1 <= w) => sym -> Pred sym -> NatRepr w -> IO (SymBV sym w)
natToReal :: sym -> SymNat sym -> IO (SymReal sym)
natToReal sym = natToInteger sym >=> integerToReal sym
uintToReal :: (1 <= w) => sym -> SymBV sym w -> IO (SymReal sym)
uintToReal sym = bvToInteger sym >=> integerToReal sym
sbvToReal :: (1 <= w) => sym -> SymBV sym w -> IO (SymReal sym)
sbvToReal sym = sbvToInteger sym >=> integerToReal sym
realRound :: sym -> SymReal sym -> IO (SymInteger sym)
realRoundEven :: sym -> SymReal sym -> IO (SymInteger sym)
realFloor :: sym -> SymReal sym -> IO (SymInteger sym)
realCeil :: sym -> SymReal sym -> IO (SymInteger sym)
realTrunc :: sym -> SymReal sym -> IO (SymInteger sym)
realTrunc sym x =
do pneg <- realLt sym x =<< realLit sym 0
iteM intIte sym pneg (realCeil sym x) (realFloor sym x)
integerToBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
integerToNat :: sym -> SymInteger sym -> IO (SymNat sym)
realToInteger :: sym -> SymReal sym -> IO (SymInteger sym)
realToNat :: sym -> SymReal sym -> IO (SymNat sym)
realToNat sym r = realToInteger sym r >>= integerToNat sym
realToBV :: (1 <= w) => sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
realToBV sym r w = do
i <- realRound sym r
clampedIntToBV sym i w
realToSBV :: (1 <= w) => sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
realToSBV sym r w = do
i <- realRound sym r
clampedIntToSBV sym i w
clampedIntToSBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
clampedIntToSBV sym i w
| Just v <- asInteger i = do
bvLit sym w $ BV.signedClamp w v
| otherwise = do
let min_val = minSigned w
min_val_bv = BV.minSigned w
min_sym <- intLit sym min_val
is_lt <- intLt sym i min_sym
iteM bvIte sym is_lt (bvLit sym w min_val_bv) $ do
let max_val = maxSigned w
max_val_bv = BV.maxSigned w
max_sym <- intLit sym max_val
is_gt <- intLt sym max_sym i
iteM bvIte sym is_gt (bvLit sym w max_val_bv) $ do
integerToBV sym i w
clampedIntToBV :: (1 <= w) => sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
clampedIntToBV sym i w
| Just v <- asInteger i = do
bvLit sym w $ BV.unsignedClamp w v
| otherwise = do
min_sym <- intLit sym 0
is_lt <- intLt sym i min_sym
iteM bvIte sym is_lt (bvLit sym w (BV.zero w)) $ do
let max_val = maxUnsigned w
max_val_bv = BV.maxUnsigned w
max_sym <- intLit sym max_val
is_gt <- intLt sym max_sym i
iteM bvIte sym is_gt (bvLit sym w max_val_bv) $
integerToBV sym i w
intSetWidth :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
intSetWidth sym e n = do
let m = bvWidth e
case n `testNatCases` m of
NatCaseLT LeqProof -> do
does_underflow <- bvSlt sym e =<< bvLit sym m (BV.sext n m (BV.minSigned n))
iteM bvIte sym does_underflow (bvLit sym n (BV.minSigned n)) $ do
does_overflow <- bvSgt sym e =<< bvLit sym m (BV.mkBV m (maxSigned n))
iteM bvIte sym does_overflow (bvLit sym n (BV.maxSigned n)) $ do
bvTrunc sym n e
NatCaseEQ -> return e
NatCaseGT LeqProof -> bvSext sym n e
uintSetWidth :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
uintSetWidth sym e n = do
let m = bvWidth e
case n `testNatCases` m of
NatCaseLT LeqProof -> do
does_overflow <- bvUgt sym e =<< bvLit sym m (BV.mkBV m (maxUnsigned n))
iteM bvIte sym does_overflow (bvLit sym n (BV.maxUnsigned n)) $ bvTrunc sym n e
NatCaseEQ -> return e
NatCaseGT LeqProof -> bvZext sym n e
intToUInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
intToUInt sym e w = do
p <- bvIsNeg sym e
iteM bvIte sym p (bvLit sym w (BV.zero w)) (uintSetWidth sym e w)
uintToInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
uintToInt sym e n = do
let m = bvWidth e
case n `testNatCases` m of
NatCaseLT LeqProof -> do
max_val <- bvLit sym m (BV.sext n m (BV.maxSigned n))
p <- bvUle sym e max_val
bvTrunc sym n =<< bvIte sym p e max_val
NatCaseEQ -> do
max_val <- maxSignedBV sym n
p <- bvUle sym e max_val
bvIte sym p e max_val
NatCaseGT LeqProof -> do
bvZext sym n e
stringEmpty :: sym -> StringInfoRepr si -> IO (SymString sym si)
stringLit :: sym -> StringLiteral si -> IO (SymString sym si)
stringEq :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
stringIte :: sym -> Pred sym -> SymString sym si -> SymString sym si -> IO (SymString sym si)
stringConcat :: sym -> SymString sym si -> SymString sym si -> IO (SymString sym si)
stringContains :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
stringIsPrefixOf :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
stringIsSuffixOf :: sym -> SymString sym si -> SymString sym si -> IO (Pred sym)
stringIndexOf :: sym -> SymString sym si -> SymString sym si -> SymNat sym -> IO (SymInteger sym)
stringLength :: sym -> SymString sym si -> IO (SymNat sym)
stringSubstring :: sym -> SymString sym si -> SymNat sym -> SymNat sym -> IO (SymString sym si)
realZero :: sym -> SymReal sym
realLit :: sym -> Rational -> IO (SymReal sym)
sciLit :: sym -> Scientific -> IO (SymReal sym)
sciLit sym s = realLit sym (toRational s)
realEq :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realNe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realNe sym x y = notPred sym =<< realEq sym x y
realLe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLt :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realLt sym x y = notPred sym =<< realLe sym y x
realGe :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realGe sym x y = realLe sym y x
realGt :: sym -> SymReal sym -> SymReal sym -> IO (Pred sym)
realGt sym x y = realLt sym y x
realIte :: sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realNeg :: sym -> SymReal sym -> IO (SymReal sym)
realAdd :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMul :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realSub :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realSub sym x y = realAdd sym x =<< realNeg sym y
realSq :: sym -> SymReal sym -> IO (SymReal sym)
realSq sym x = realMul sym x x
realDiv :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMod :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realMod sym x y = do
isZero <- realEq sym y (realZero sym)
iteM realIte sym isZero (return x) $ do
realSub sym x =<< realMul sym y
=<< integerToReal sym
=<< realFloor sym
=<< realDiv sym x y
isInteger :: sym -> SymReal sym -> IO (Pred sym)
realIsNonNeg :: sym -> SymReal sym -> IO (Pred sym)
realIsNonNeg sym x = realLe sym (realZero sym) x
realSqrt :: sym -> SymReal sym -> IO (SymReal sym)
realAtan2 :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realPi :: sym -> IO (SymReal sym)
realLog :: sym -> SymReal sym -> IO (SymReal sym)
realExp :: sym -> SymReal sym -> IO (SymReal sym)
realSin :: sym -> SymReal sym -> IO (SymReal sym)
realCos :: sym -> SymReal sym -> IO (SymReal sym)
realTan :: sym -> SymReal sym -> IO (SymReal sym)
realTan sym x = do
sin_x <- realSin sym x
cos_x <- realCos sym x
realDiv sym sin_x cos_x
realSinh :: sym -> SymReal sym -> IO (SymReal sym)
realCosh :: sym -> SymReal sym -> IO (SymReal sym)
realTanh :: sym -> SymReal sym -> IO (SymReal sym)
realTanh sym x = do
sinh_x <- realSinh sym x
cosh_x <- realCosh sym x
realDiv sym sinh_x cosh_x
realAbs :: sym -> SymReal sym -> IO (SymReal sym)
realAbs sym x = do
c <- realGe sym x (realZero sym)
realIte sym c x =<< realNeg sym x
realHypot :: sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realHypot sym x y = do
case (asRational x, asRational y) of
(Just 0, _) -> realAbs sym y
(_, Just 0) -> realAbs sym x
_ -> do
x2 <- realSq sym x
y2 <- realSq sym y
realSqrt sym =<< realAdd sym x2 y2
floatPZero :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatNZero :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatNaN :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatPInf :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatNInf :: sym -> FloatPrecisionRepr fpp -> IO (SymFloat sym fpp)
floatLit
:: sym -> FloatPrecisionRepr fpp -> Rational -> IO (SymFloat sym fpp)
floatNeg
:: sym
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatAbs
:: sym
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatSqrt
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatAdd
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatSub
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatMul
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatDiv
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatRem
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatMin
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatMax
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatFMA
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatEq
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatNe
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatFpEq
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatFpNe
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatLe
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatLt
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatGe
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatGt
:: sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (Pred sym)
floatIsNaN :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsInf :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsZero :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsPos :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsNeg :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsSubnorm :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIsNorm :: sym -> SymFloat sym fpp -> IO (Pred sym)
floatIte
:: sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatCast
:: sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymFloat sym fpp'
-> IO (SymFloat sym fpp)
floatRound
:: sym
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatFromBinary
:: (2 <= eb, 2 <= sb)
=> sym
-> FloatPrecisionRepr (FloatingPointPrecision eb sb)
-> SymBV sym (eb + sb)
-> IO (SymFloat sym (FloatingPointPrecision eb sb))
floatToBinary
:: (2 <= eb, 2 <= sb)
=> sym
-> SymFloat sym (FloatingPointPrecision eb sb)
-> IO (SymBV sym (eb + sb))
bvToFloat
:: (1 <= w)
=> sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymBV sym w
-> IO (SymFloat sym fpp)
sbvToFloat
:: (1 <= w)
=> sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymBV sym w
-> IO (SymFloat sym fpp)
realToFloat
:: sym
-> FloatPrecisionRepr fpp
-> RoundingMode
-> SymReal sym
-> IO (SymFloat sym fpp)
floatToBV
:: (1 <= w)
=> sym
-> NatRepr w
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymBV sym w)
floatToSBV
:: (1 <= w)
=> sym
-> NatRepr w
-> RoundingMode
-> SymFloat sym fpp
-> IO (SymBV sym w)
floatToReal :: sym -> SymFloat sym fpp -> IO (SymReal sym)
mkComplex :: sym -> Complex (SymReal sym) -> IO (SymCplx sym)
getRealPart :: sym -> SymCplx sym -> IO (SymReal sym)
getImagPart :: sym -> SymCplx sym -> IO (SymReal sym)
cplxGetParts :: sym -> SymCplx sym -> IO (Complex (SymReal sym))
mkComplexLit :: sym -> Complex Rational -> IO (SymCplx sym)
mkComplexLit sym d = mkComplex sym =<< traverse (realLit sym) d
cplxFromReal :: sym -> SymReal sym -> IO (SymCplx sym)
cplxFromReal sym r = mkComplex sym (r :+ realZero sym)
cplxIte :: sym -> Pred sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxIte sym c x y = do
case asConstantPred c of
Just True -> return x
Just False -> return y
_ -> do
xr :+ xi <- cplxGetParts sym x
yr :+ yi <- cplxGetParts sym y
zr <- realIte sym c xr yr
zi <- realIte sym c xi yi
mkComplex sym (zr :+ zi)
cplxNeg :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxNeg sym x = mkComplex sym =<< traverse (realNeg sym) =<< cplxGetParts sym x
cplxAdd :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxAdd sym x y = do
xr :+ xi <- cplxGetParts sym x
yr :+ yi <- cplxGetParts sym y
zr <- realAdd sym xr yr
zi <- realAdd sym xi yi
mkComplex sym (zr :+ zi)
cplxSub :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxSub sym x y = do
xr :+ xi <- cplxGetParts sym x
yr :+ yi <- cplxGetParts sym y
zr <- realSub sym xr yr
zi <- realSub sym xi yi
mkComplex sym (zr :+ zi)
cplxMul :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxMul sym x y = do
xr :+ xi <- cplxGetParts sym x
yr :+ yi <- cplxGetParts sym y
rz0 <- realMul sym xr yr
rz <- realSub sym rz0 =<< realMul sym xi yi
iz0 <- realMul sym xi yr
iz <- realAdd sym iz0 =<< realMul sym xr yi
mkComplex sym (rz :+ iz)
cplxMag :: sym -> SymCplx sym -> IO (SymReal sym)
cplxMag sym x = do
(xr :+ xi) <- cplxGetParts sym x
realHypot sym xr xi
cplxSqrt :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxSqrt sym x = do
(r_part :+ i_part) <- cplxGetParts sym x
case (asRational r_part :+ asRational i_part)of
(Just r :+ Just i) | Just z <- tryComplexSqrt tryRationalSqrt (r :+ i) ->
mkComplexLit sym z
(_ :+ Just 0) -> do
c <- realGe sym r_part (realZero sym)
u <- iteM realIte sym c
(realSqrt sym r_part)
(realLit sym 0)
v <- iteM realIte sym c
(realLit sym 0)
(realSqrt sym =<< realNeg sym r_part)
mkComplex sym (u :+ v)
_ -> do
m <- realHypot sym r_part i_part
m_plus_r <- realAdd sym m r_part
m_sub_r <- realSub sym m r_part
two <- realLit sym 2
u <- realSqrt sym =<< realDiv sym m_plus_r two
v <- realSqrt sym =<< realDiv sym m_sub_r two
neg_v <- realNeg sym v
i_part_nonneg <- realIsNonNeg sym i_part
v' <- realIte sym i_part_nonneg v neg_v
mkComplex sym (u :+ v')
cplxSin :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxSin sym arg = do
c@(x :+ y) <- cplxGetParts sym arg
case asRational <$> c of
(Just 0 :+ Just 0) -> cplxFromReal sym (realZero sym)
(_ :+ Just 0) -> cplxFromReal sym =<< realSin sym x
(Just 0 :+ _) -> do
sinh_y <- realSinh sym y
mkComplex sym (realZero sym :+ sinh_y)
_ -> do
sin_x <- realSin sym x
cos_x <- realCos sym x
sinh_y <- realSinh sym y
cosh_y <- realCosh sym y
r_part <- realMul sym sin_x cosh_y
i_part <- realMul sym cos_x sinh_y
mkComplex sym (r_part :+ i_part)
cplxCos :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxCos sym arg = do
c@(x :+ y) <- cplxGetParts sym arg
case asRational <$> c of
(Just 0 :+ Just 0) -> cplxFromReal sym =<< realLit sym 1
(_ :+ Just 0) -> cplxFromReal sym =<< realCos sym x
(Just 0 :+ _) -> do
cosh_y <- realCosh sym y
cplxFromReal sym cosh_y
_ -> do
neg_sin_x <- realNeg sym =<< realSin sym x
cos_x <- realCos sym x
sinh_y <- realSinh sym y
cosh_y <- realCosh sym y
r_part <- realMul sym cos_x cosh_y
i_part <- realMul sym neg_sin_x sinh_y
mkComplex sym (r_part :+ i_part)
cplxTan :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxTan sym arg = do
c@(x :+ y) <- cplxGetParts sym arg
case asRational <$> c of
(Just 0 :+ Just 0) -> cplxFromReal sym (realZero sym)
(_ :+ Just 0) -> do
cplxFromReal sym =<< realTan sym x
(Just 0 :+ _) -> do
i_part <- realTanh sym y
mkComplex sym (realZero sym :+ i_part)
_ -> do
sin_x <- realSin sym x
cos_x <- realCos sym x
sinh_y <- realSinh sym y
cosh_y <- realCosh sym y
u <- realMul sym cos_x cosh_y
v <- realMul sym sin_x sinh_y
u2 <- realMul sym u u
v2 <- realMul sym v v
m <- realAdd sym u2 v2
sin_x_cos_x <- realMul sym sin_x cos_x
sinh_y_cosh_y <- realMul sym sinh_y cosh_y
r_part <- realDiv sym sin_x_cos_x m
i_part <- realDiv sym sinh_y_cosh_y m
mkComplex sym (r_part :+ i_part)
cplxHypot :: sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxHypot sym x y = do
(xr :+ xi) <- cplxGetParts sym x
(yr :+ yi) <- cplxGetParts sym y
xr2 <- realSq sym xr
xi2 <- realSq sym xi
yr2 <- realSq sym yr
yi2 <- realSq sym yi
r2 <- foldM (realAdd sym) xr2 [xi2, yr2, yi2]
cplxFromReal sym =<< realSqrt sym r2
cplxRound :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxRound sym x = do
c <- cplxGetParts sym x
mkComplex sym =<< traverse (integerToReal sym <=< realRound sym) c
cplxFloor :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxFloor sym x =
mkComplex sym =<< traverse (integerToReal sym <=< realFloor sym)
=<< cplxGetParts sym x
cplxCeil :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxCeil sym x =
mkComplex sym =<< traverse (integerToReal sym <=< realCeil sym)
=<< cplxGetParts sym x
cplxConj :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxConj sym x = do
r :+ i <- cplxGetParts sym x
ic <- realNeg sym i
mkComplex sym (r :+ ic)
cplxExp :: sym -> SymCplx sym -> IO (SymCplx sym)
cplxExp sym x = do
(rx :+ i_part) <- cplxGetParts sym x
expx <- realExp sym rx
cosx <- realCos sym i_part
sinx <- realSin sym i_part
rz <- realMul sym expx cosx
iz <- realMul sym expx sinx
mkComplex sym (rz :+ iz)
cplxEq :: sym -> SymCplx sym -> SymCplx sym -> IO (Pred sym)
cplxEq sym x y = do
xr :+ xi <- cplxGetParts sym x
yr :+ yi <- cplxGetParts sym y
pr <- realEq sym xr yr
pj <- realEq sym xi yi
andPred sym pr pj
cplxNe :: sym -> SymCplx sym -> SymCplx sym -> IO (Pred sym)
cplxNe sym x y = do
xr :+ xi <- cplxGetParts sym x
yr :+ yi <- cplxGetParts sym y
pr <- realNe sym xr yr
pj <- realNe sym xi yi
orPred sym pr pj
newtype SymBV' sym w = MkSymBV' (SymBV sym w)
bvJoinVector :: forall sym n w. (1 <= w, IsExprBuilder sym)
=> sym
-> NatRepr w
-> Vector.Vector n (SymBV sym w)
-> IO (SymBV sym (n * w))
bvJoinVector sym w =
coerce $ Vector.joinWithM @IO @(SymBV' sym) @n bvConcat' w
where bvConcat' :: forall l. (1 <= l)
=> NatRepr l
-> SymBV' sym w
-> SymBV' sym l
-> IO (SymBV' sym (w + l))
bvConcat' _ (MkSymBV' x) (MkSymBV' y) = MkSymBV' <$> bvConcat sym x y
bvSplitVector :: forall sym n w. (IsExprBuilder sym, 1 <= w, 1 <= n)
=> sym
-> NatRepr n
-> NatRepr w
-> SymBV sym (n * w)
-> IO (Vector.Vector n (SymBV sym w))
bvSplitVector sym n w x =
coerce $ Vector.splitWithA @IO LittleEndian bvSelect' n w (MkSymBV' @sym x)
where
bvSelect' :: forall i. (i + w <= n * w)
=> NatRepr (n * w)
-> NatRepr i
-> SymBV' sym (n * w)
-> IO (SymBV' sym w)
bvSelect' _ i (MkSymBV' y) =
fmap MkSymBV' $ bvSelect @_ @i @w sym i w y
bvSwap :: forall sym n. (1 <= n, IsExprBuilder sym)
=> sym
-> NatRepr n
-> SymBV sym (n*8)
-> IO (SymBV sym (n*8))
bvSwap sym n v = do
bvJoinVector sym (knownNat @8) . Vector.reverse
=<< bvSplitVector sym n (knownNat @8) v
bvBitreverse :: forall sym w.
(1 <= w, IsExprBuilder sym) =>
sym ->
SymBV sym w ->
IO (SymBV sym w)
bvBitreverse sym v = do
bvJoinVector sym (knownNat @1) . Vector.reverse
=<< bvSplitVector sym (bvWidth v) (knownNat @1) v
data RoundingMode
= RNE
| RNA
| RTP
| RTN
| RTZ
deriving (Eq, Generic, Ord, Show, Enum)
instance Hashable RoundingMode
indexLit :: IsExprBuilder sym => sym -> IndexLit idx -> IO (SymExpr sym idx)
indexLit sym (NatIndexLit i) = natLit sym i
indexLit sym (BVIndexLit w v) = bvLit sym w v
iteM :: IsExprBuilder sym
=> (sym -> Pred sym -> v -> v -> IO v)
-> sym -> Pred sym -> IO v -> IO v -> IO v
iteM ite sym p mx my = do
case asConstantPred p of
Just True -> mx
Just False -> my
Nothing -> join $ ite sym p <$> mx <*> my
type family SymFn sym :: Ctx BaseType -> BaseType -> Type
class IsSymFn fn where
fnArgTypes :: fn args ret -> Ctx.Assignment BaseTypeRepr args
fnReturnType :: fn args ret -> BaseTypeRepr ret
data UnfoldPolicy
= NeverUnfold
| AlwaysUnfold
| UnfoldConcrete
deriving (Eq, Ord, Show)
shouldUnfold :: IsExpr e => UnfoldPolicy -> Ctx.Assignment e args -> Bool
shouldUnfold AlwaysUnfold _ = True
shouldUnfold NeverUnfold _ = False
shouldUnfold UnfoldConcrete args = allFC baseIsConcrete args
class ( IsExprBuilder sym
, IsSymFn (SymFn sym)
, OrdF (SymExpr sym)
) => IsSymExprBuilder sym where
freshConstant :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshLatch :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
freshBoundedBV :: (1 <= w) => sym -> SolverSymbol -> NatRepr w -> Maybe Natural -> Maybe Natural -> IO (SymBV sym w)
freshBoundedSBV :: (1 <= w) => sym -> SolverSymbol -> NatRepr w -> Maybe Integer -> Maybe Integer -> IO (SymBV sym w)
freshBoundedNat :: sym -> SolverSymbol -> Maybe Natural -> Maybe Natural -> IO (SymNat sym)
freshBoundedInt :: sym -> SolverSymbol -> Maybe Integer -> Maybe Integer -> IO (SymInteger sym)
freshBoundedReal :: sym -> SolverSymbol -> Maybe Rational -> Maybe Rational -> IO (SymReal sym)
freshBoundVar :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
varExpr :: sym -> BoundVar sym tp -> SymExpr sym tp
forallPred :: sym
-> BoundVar sym tp
-> Pred sym
-> IO (Pred sym)
existsPred :: sym
-> BoundVar sym tp
-> Pred sym
-> IO (Pred sym)
definedFn :: sym
-> SolverSymbol
-> Ctx.Assignment (BoundVar sym) args
-> SymExpr sym ret
-> UnfoldPolicy
-> IO (SymFn sym args ret)
inlineDefineFun :: Ctx.CurryAssignmentClass args
=> sym
-> SolverSymbol
-> Ctx.Assignment BaseTypeRepr args
-> UnfoldPolicy
-> Ctx.CurryAssignment args (SymExpr sym) (IO (SymExpr sym ret))
-> IO (SymFn sym args ret)
inlineDefineFun sym nm tps policy f = do
vars <- traverseFC (freshBoundVar sym emptySymbol) tps
r <- Ctx.uncurryAssignment f (fmapFC (varExpr sym) vars)
definedFn sym nm vars r policy
freshTotalUninterpFn :: forall args ret
. sym
-> SolverSymbol
-> Ctx.Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
applySymFn :: sym
-> SymFn sym args ret
-> Ctx.Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
baseIsConcrete :: forall e bt
. IsExpr e
=> e bt
-> Bool
baseIsConcrete x =
case exprType x of
BaseBoolRepr -> isJust $ asConstantPred x
BaseNatRepr -> isJust $ asNat x
BaseIntegerRepr -> isJust $ asInteger x
BaseBVRepr _ -> isJust $ asBV x
BaseRealRepr -> isJust $ asRational x
BaseFloatRepr _ -> False
BaseStringRepr{} -> isJust $ asString x
BaseComplexRepr -> isJust $ asComplex x
BaseStructRepr _ -> case asStruct x of
Just flds -> allFC baseIsConcrete flds
Nothing -> False
BaseArrayRepr _ _bt' -> do
case asConstantArray x of
Just x' -> baseIsConcrete x'
Nothing -> False
baseDefaultValue :: forall sym bt
. IsExprBuilder sym
=> sym
-> BaseTypeRepr bt
-> IO (SymExpr sym bt)
baseDefaultValue sym bt =
case bt of
BaseBoolRepr -> return $! falsePred sym
BaseNatRepr -> natLit sym 0
BaseIntegerRepr -> intLit sym 0
BaseBVRepr w -> bvLit sym w (BV.zero w)
BaseRealRepr -> return $! realZero sym
BaseFloatRepr fpp -> floatPZero sym fpp
BaseComplexRepr -> mkComplexLit sym (0 :+ 0)
BaseStringRepr si -> stringEmpty sym si
BaseStructRepr flds -> do
let f :: BaseTypeRepr tp -> IO (SymExpr sym tp)
f v = baseDefaultValue sym v
mkStruct sym =<< traverseFC f flds
BaseArrayRepr idx bt' -> do
elt <- baseDefaultValue sym bt'
constantArray sym idx elt
backendPred :: IsExprBuilder sym => sym -> Bool -> Pred sym
backendPred sym True = truePred sym
backendPred sym False = falsePred sym
mkRational :: IsExprBuilder sym => sym -> Rational -> IO (SymCplx sym)
mkRational sym v = mkComplexLit sym (v :+ 0)
mkReal :: (IsExprBuilder sym, Real a) => sym -> a -> IO (SymCplx sym)
mkReal sym v = mkRational sym (toRational v)
predToReal :: IsExprBuilder sym => sym -> Pred sym -> IO (SymReal sym)
predToReal sym p = do
r1 <- realLit sym 1
realIte sym p r1 (realZero sym)
realExprAsRational :: (MonadFail m, IsExpr e) => e BaseRealType -> m Rational
realExprAsRational x = do
case asRational x of
Just r -> return r
Nothing -> fail "Value is not a constant expression."
cplxExprAsRational :: (MonadFail m, IsExpr e) => e BaseComplexType -> m Rational
cplxExprAsRational x = do
case asComplex x of
Just (r :+ i) -> do
when (i /= 0) $
fail "Complex value has an imaginary part."
return r
Nothing -> do
fail "Complex value is not a constant expression."
cplxExprAsInteger :: (MonadFail m, IsExpr e) => e BaseComplexType -> m Integer
cplxExprAsInteger x = rationalAsInteger =<< cplxExprAsRational x
rationalAsInteger :: MonadFail m => Rational -> m Integer
rationalAsInteger r = do
when (denominator r /= 1) $ do
fail "Value is not an integer."
return (numerator r)
realExprAsInteger :: (IsExpr e, MonadFail m) => e BaseRealType -> m Integer
realExprAsInteger x =
rationalAsInteger =<< realExprAsRational x
andAllOf :: IsExprBuilder sym
=> sym
-> Fold s (Pred sym)
-> s
-> IO (Pred sym)
andAllOf sym f s = foldlMOf f (andPred sym) (truePred sym) s
orOneOf :: IsExprBuilder sym
=> sym
-> Fold s (Pred sym)
-> s
-> IO (Pred sym)
orOneOf sym f s = foldlMOf f (orPred sym) (falsePred sym) s
isNonZero :: IsExprBuilder sym => sym -> SymCplx sym -> IO (Pred sym)
isNonZero sym v = cplxNe sym v =<< mkRational sym 0
isReal :: IsExprBuilder sym => sym -> SymCplx sym -> IO (Pred sym)
isReal sym v = do
i <- getImagPart sym v
realEq sym i (realZero sym)
cplxDiv :: IsExprBuilder sym
=> sym
-> SymCplx sym
-> SymCplx sym
-> IO (SymCplx sym)
cplxDiv sym x y = do
xr :+ xi <- cplxGetParts sym x
yc@(yr :+ yi) <- cplxGetParts sym y
case asRational <$> yc of
(_ :+ Just 0) -> do
zc <- (:+) <$> realDiv sym xr yr <*> realDiv sym xi yr
mkComplex sym zc
(Just 0 :+ _) -> do
zc <- (:+) <$> realDiv sym xi yi <*> realDiv sym xr yi
mkComplex sym zc
_ -> do
yr_abs <- realMul sym yr yr
yi_abs <- realMul sym yi yi
y_abs <- realAdd sym yr_abs yi_abs
zr_1 <- realMul sym xr yr
zr_2 <- realMul sym xi yi
zr <- realAdd sym zr_1 zr_2
zi_1 <- realMul sym xi yr
zi_2 <- realMul sym xr yi
zi <- realSub sym zi_1 zi_2
zc <- (:+) <$> realDiv sym zr y_abs <*> realDiv sym zi y_abs
mkComplex sym zc
cplxLog' :: IsExprBuilder sym
=> sym -> SymCplx sym -> IO (Complex (SymReal sym))
cplxLog' sym x = do
xr :+ xi <- cplxGetParts sym x
xm <- realHypot sym xr xi
xa <- realAtan2 sym xi xr
zr <- realLog sym xm
return $! zr :+ xa
cplxLog :: IsExprBuilder sym
=> sym -> SymCplx sym -> IO (SymCplx sym)
cplxLog sym x = mkComplex sym =<< cplxLog' sym x
cplxLogBase :: IsExprBuilder sym
=> Rational
-> sym
-> SymCplx sym
-> IO (SymCplx sym)
cplxLogBase base sym x = do
b <- realLog sym =<< realLit sym base
z <- traverse (\r -> realDiv sym r b) =<< cplxLog' sym x
mkComplex sym z
asConcrete :: IsExpr e => e tp -> Maybe (ConcreteVal tp)
asConcrete x =
case exprType x of
BaseBoolRepr -> ConcreteBool <$> asConstantPred x
BaseNatRepr -> ConcreteNat <$> asNat x
BaseIntegerRepr -> ConcreteInteger <$> asInteger x
BaseRealRepr -> ConcreteReal <$> asRational x
BaseStringRepr _si -> ConcreteString <$> asString x
BaseComplexRepr -> ConcreteComplex <$> asComplex x
BaseBVRepr w -> ConcreteBV w <$> asBV x
BaseFloatRepr _ -> Nothing
BaseStructRepr _ -> Nothing
BaseArrayRepr _ _ -> Nothing
concreteToSym :: IsExprBuilder sym => sym -> ConcreteVal tp -> IO (SymExpr sym tp)
concreteToSym sym = \case
ConcreteBool True -> return (truePred sym)
ConcreteBool False -> return (falsePred sym)
ConcreteNat x -> natLit sym x
ConcreteInteger x -> intLit sym x
ConcreteReal x -> realLit sym x
ConcreteString x -> stringLit sym x
ConcreteComplex x -> mkComplexLit sym x
ConcreteBV w x -> bvLit sym w x
ConcreteStruct xs -> mkStruct sym =<< traverseFC (concreteToSym sym) xs
ConcreteArray idxTy def xs0 -> go (Map.toAscList xs0) =<< constantArray sym idxTy =<< concreteToSym sym def
where
go [] arr = return arr
go ((i,x):xs) arr =
do arr' <- go xs arr
i' <- traverseFC (concreteToSym sym) i
x' <- concreteToSym sym x
arrayUpdate sym arr' i' x'
{-# INLINABLE muxRange #-}
muxRange :: (IsExpr e, Monad m) =>
(Natural -> m (e BaseBoolType))
->
(e BaseBoolType -> a -> a -> m a) ->
(Natural -> m a) ->
Natural ->
Natural ->
m a
muxRange predFn iteFn f l h
| l < h = do
c <- predFn l
case asConstantPred c of
Just True -> f l
Just False -> muxRange predFn iteFn f (succ l) h
Nothing ->
do match_branch <- f l
other_branch <- muxRange predFn