{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module What4.Protocol.SMTWriter
(
SupportTermOps(..)
, ArrayConstantFn
, SMTWriter(..)
, SMTReadWriter (..)
, SMTEvalBVArrayFn
, SMTEvalBVArrayWrapper(..)
, Term
, app
, app_list
, builder_list
, WriterConn( supportFunctionDefs
, supportFunctionArguments
, supportQuantifiers
, supportedFeatures
, connHandle
, connInputHandle
, smtWriterName
)
, connState
, newWriterConn
, resetEntryStack
, popEntryStackToTop
, entryStackHeight
, pushEntryStack
, popEntryStack
, Command
, addCommand
, addCommandNoAck
, addCommands
, mkFreeVar
, bindVarAsFree
, TypeMap(..)
, typeMap
, freshBoundVarName
, assumeFormula
, assumeFormulaWithName
, assumeFormulaWithFreshName
, DefineStyle(..)
, AcknowledgementAction(..)
, nullAcknowledgementAction
, assume
, mkSMTTerm
, mkFormula
, mkAtomicFormula
, SMTEvalFunctions(..)
, smtExprGroundEvalFn
, CollectorResults(..)
, mkBaseExpr
, runInSandbox
, What4.Interface.RoundingMode(..)
) where
#if !MIN_VERSION_base(4,13,0)
import Control.Monad.Fail( MonadFail )
#endif
import Control.Exception
import Control.Lens hiding ((.>))
import Control.Monad.Extra
import Control.Monad.IO.Class
import Control.Monad.Reader
import Control.Monad.ST
import Control.Monad.State.Strict
import Control.Monad.Trans.Maybe
import qualified Data.Bits as Bits
import qualified Data.BitVector.Sized as BV
import Data.ByteString (ByteString)
import Data.IORef
import Data.Kind
import Data.List (last)
import Data.List.NonEmpty (NonEmpty(..))
import Data.Maybe
import Data.Parameterized.Classes (ShowF(..))
import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.HashTable as PH
import Data.Parameterized.Nonce (Nonce)
import Data.Parameterized.Some
import Data.Parameterized.TraversableFC
import Data.Ratio
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Text.Lazy.Builder (Builder)
import qualified Data.Text.Lazy.Builder as Builder
import qualified Data.Text.Lazy.Builder.Int as Builder (decimal)
import qualified Data.Text.Lazy as Lazy
import Data.Word
import Numeric.Natural
import Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>))
import System.IO.Streams (OutputStream, InputStream)
import qualified System.IO.Streams as Streams
import What4.BaseTypes
import What4.Interface (RoundingMode(..), stringInfo)
import What4.ProblemFeatures
import qualified What4.Expr.ArrayUpdateMap as AUM
import qualified What4.Expr.BoolMap as BM
import What4.Expr.Builder
import What4.Expr.GroundEval
import qualified What4.Expr.StringSeq as SSeq
import qualified What4.Expr.WeightedSum as WSum
import qualified What4.Expr.UnaryBV as UnaryBV
import What4.ProgramLoc
import What4.SatResult
import qualified What4.SemiRing as SR
import What4.Symbol
import What4.Utils.AbstractDomains
import qualified What4.Utils.BVDomain as BVD
import What4.Utils.Complex
import What4.Utils.StringLiteral
data TypeMap (tp::BaseType) where
BoolTypeMap :: TypeMap BaseBoolType
NatTypeMap :: TypeMap BaseNatType
IntegerTypeMap :: TypeMap BaseIntegerType
RealTypeMap :: TypeMap BaseRealType
BVTypeMap :: (1 <= w) => !(NatRepr w) -> TypeMap (BaseBVType w)
FloatTypeMap :: !(FloatPrecisionRepr fpp) -> TypeMap (BaseFloatType fpp)
Char8TypeMap :: TypeMap (BaseStringType Char8)
ComplexToStructTypeMap:: TypeMap BaseComplexType
ComplexToArrayTypeMap :: TypeMap BaseComplexType
PrimArrayTypeMap :: !(Ctx.Assignment TypeMap (idxl Ctx.::> idx))
-> !(TypeMap tp)
-> TypeMap (BaseArrayType (idxl Ctx.::> idx) tp)
FnArrayTypeMap :: !(Ctx.Assignment TypeMap (idxl Ctx.::> idx))
-> TypeMap tp
-> TypeMap (BaseArrayType (idxl Ctx.::> idx) tp)
StructTypeMap :: !(Ctx.Assignment TypeMap idx)
-> TypeMap (BaseStructType idx)
instance ShowF TypeMap
instance Show (TypeMap a) where
show BoolTypeMap = "BoolTypeMap"
show NatTypeMap = "NatTypeMap"
show IntegerTypeMap = "IntegerTypeMap"
show RealTypeMap = "RealTypeMap"
show (BVTypeMap n) = "BVTypeMap " ++ show n
show (FloatTypeMap x) = "FloatTypeMap " ++ show x
show Char8TypeMap = "Char8TypeMap"
show (ComplexToStructTypeMap) = "ComplexToStructTypeMap"
show ComplexToArrayTypeMap = "ComplexToArrayTypeMap"
show (PrimArrayTypeMap ctx a) = "PrimArrayTypeMap " ++ showF ctx ++ " " ++ showF a
show (FnArrayTypeMap ctx a) = "FnArrayTypeMap " ++ showF ctx ++ " " ++ showF a
show (StructTypeMap ctx) = "StructTypeMap " ++ showF ctx
instance Eq (TypeMap tp) where
x == y = isJust (testEquality x y)
instance TestEquality TypeMap where
testEquality BoolTypeMap BoolTypeMap = Just Refl
testEquality NatTypeMap NatTypeMap = Just Refl
testEquality IntegerTypeMap IntegerTypeMap = Just Refl
testEquality RealTypeMap RealTypeMap = Just Refl
testEquality Char8TypeMap Char8TypeMap = Just Refl
testEquality (FloatTypeMap x) (FloatTypeMap y) = do
Refl <- testEquality x y
return Refl
testEquality (BVTypeMap x) (BVTypeMap y) = do
Refl <- testEquality x y
return Refl
testEquality ComplexToStructTypeMap ComplexToStructTypeMap =
Just Refl
testEquality ComplexToArrayTypeMap ComplexToArrayTypeMap =
Just Refl
testEquality (PrimArrayTypeMap xa xr) (PrimArrayTypeMap ya yr) = do
Refl <- testEquality xa ya
Refl <- testEquality xr yr
Just Refl
testEquality (FnArrayTypeMap xa xr) (FnArrayTypeMap ya yr) = do
Refl <- testEquality xa ya
Refl <- testEquality xr yr
Just Refl
testEquality (StructTypeMap x) (StructTypeMap y) = do
Refl <- testEquality x y
Just Refl
testEquality _ _ = Nothing
semiRingTypeMap :: SR.SemiRingRepr sr -> TypeMap (SR.SemiRingBase sr)
semiRingTypeMap SR.SemiRingNatRepr = NatTypeMap
semiRingTypeMap SR.SemiRingIntegerRepr = IntegerTypeMap
semiRingTypeMap SR.SemiRingRealRepr = RealTypeMap
semiRingTypeMap (SR.SemiRingBVRepr _flv w) = BVTypeMap w
type ArrayConstantFn v
= [Some TypeMap]
-> Some TypeMap
-> v
-> v
class Num v => SupportTermOps v where
boolExpr :: Bool -> v
notExpr :: v -> v
andAll :: [v] -> v
orAll :: [v] -> v
(.&&) :: v -> v -> v
x .&& y = andAll [x, y]
(.||) :: v -> v -> v
x .|| y = orAll [x, y]
(.==) :: v -> v -> v
(./=) :: v -> v -> v
x ./= y = notExpr (x .== y)
impliesExpr :: v -> v -> v
impliesExpr x y = notExpr x .|| y
letExpr :: [(Text, v)] -> v -> v
ite :: v -> v -> v -> v
sumExpr :: [v] -> v
sumExpr [] = 0
sumExpr (h:r) = foldl (+) h r
termIntegerToReal :: v -> v
termRealToInteger :: v -> v
integerTerm :: Integer -> v
rationalTerm :: Rational -> v
(.<=) :: v -> v -> v
(.<) :: v -> v -> v
x .< y = notExpr (y .<= x)
(.>) :: v -> v -> v
x .> y = y .< x
(.>=) :: v -> v -> v
x .>= y = y .<= x
intAbs :: v -> v
intDiv :: v -> v -> v
intMod :: v -> v -> v
intDivisible :: v -> Natural -> v
bvTerm :: NatRepr w -> BV.BV w -> v
bvNeg :: v -> v
bvAdd :: v -> v -> v
bvSub :: v -> v -> v
bvMul :: v -> v -> v
bvSLe :: v -> v -> v
bvULe :: v -> v -> v
bvSLt :: v -> v -> v
bvULt :: v -> v -> v
bvUDiv :: v -> v -> v
bvURem :: v -> v -> v
bvSDiv :: v -> v -> v
bvSRem :: v -> v -> v
bvAnd :: v -> v -> v
bvOr :: v -> v -> v
bvXor :: v -> v -> v
bvNot :: v -> v
bvShl :: v -> v -> v
bvLshr :: v -> v -> v
bvAshr :: v -> v -> v
bvConcat :: v -> v -> v
bvExtract :: NatRepr w -> Natural -> Natural -> v -> v
bvTestBit :: NatRepr w -> Natural -> v -> v
bvTestBit w i x = (bvExtract w i 1 x .== bvTerm w1 (BV.one w1))
where w1 :: NatRepr 1
w1 = knownNat
bvSumExpr :: NatRepr w -> [v] -> v
bvSumExpr w [] = bvTerm w (BV.zero w)
bvSumExpr _ (h:r) = foldl bvAdd h r
floatPZero :: FloatPrecisionRepr fpp -> v
floatNZero :: FloatPrecisionRepr fpp -> v
floatNaN :: FloatPrecisionRepr fpp -> v
floatPInf :: FloatPrecisionRepr fpp -> v
floatNInf :: FloatPrecisionRepr fpp -> v
floatNeg :: v -> v
floatAbs :: v -> v
floatSqrt :: RoundingMode -> v -> v
floatAdd :: RoundingMode -> v -> v -> v
floatSub :: RoundingMode -> v -> v -> v
floatMul :: RoundingMode -> v -> v -> v
floatDiv :: RoundingMode -> v -> v -> v
floatRem :: v -> v -> v
floatMin :: v -> v -> v
floatMax :: v -> v -> v
floatFMA :: RoundingMode -> v -> v -> v -> v
floatEq :: v -> v -> v
floatFpEq :: v -> v -> v
floatLe :: v -> v -> v
floatLt :: v -> v -> v
floatIsNaN :: v -> v
floatIsInf :: v -> v
floatIsZero :: v -> v
floatIsPos :: v -> v
floatIsNeg :: v -> v
floatIsSubnorm :: v -> v
floatIsNorm :: v -> v
floatCast :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v
floatRound :: RoundingMode -> v -> v
floatFromBinary :: FloatPrecisionRepr fpp -> v -> v
bvToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v
sbvToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v
realToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v
floatToBV :: Natural -> RoundingMode -> v -> v
floatToSBV :: Natural -> RoundingMode -> v -> v
floatToReal :: v -> v
realIsInteger :: v -> v
realDiv :: v -> v -> v
realSin :: v -> v
realCos :: v -> v
realATan2 :: v -> v -> v
realSinh :: v -> v
realCosh :: v -> v
realExp :: v -> v
realLog :: v -> v
smtFnApp :: v -> [v] -> v
smtFnUpdate :: Maybe (v -> [v] -> v -> v)
smtFnUpdate = Nothing
lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> v -> v)
lambdaTerm = Nothing
fromText :: Text -> v
infixr 3 .&&
infixr 2 .||
infix 4 .==
infix 4 ./=
infix 4 .>
infix 4 .>=
infix 4 .<
infix 4 .<=
structComplexRealPart :: forall h. SMTWriter h => Term h -> Term h
structComplexRealPart c = structProj @h (Ctx.Empty Ctx.:> RealTypeMap Ctx.:> RealTypeMap) (Ctx.natIndex @0) c
structComplexImagPart :: forall h. SMTWriter h => Term h -> Term h
structComplexImagPart c = structProj @h (Ctx.Empty Ctx.:> RealTypeMap Ctx.:> RealTypeMap) (Ctx.natIndex @1) c
arrayComplexRealPart :: forall h . SMTWriter h => Term h -> Term h
arrayComplexRealPart c = arraySelect @h c [boolExpr False]
arrayComplexImagPart :: forall h . SMTWriter h => Term h -> Term h
arrayComplexImagPart c = arraySelect @h c [boolExpr True]
app :: Builder -> [Builder] -> Builder
app o [] = o
app o args = app_list o args
app_list :: Builder -> [Builder] -> Builder
app_list o args = "(" <> o <> go args
where go [] = ")"
go (f:r) = " " <> f <> go r
builder_list :: [Builder] -> Builder
builder_list [] = "()"
builder_list (h:l) = app_list h l
type family Term (h :: Type) :: Type
data SMTExpr h (tp :: BaseType) where
SMTName :: !(TypeMap tp) -> !Text -> SMTExpr h tp
SMTExpr :: !(TypeMap tp) -> !(Term h) -> SMTExpr h tp
asBase :: SupportTermOps (Term h)
=> SMTExpr h tp
-> Term h
asBase (SMTName _ n) = fromText n
asBase (SMTExpr _ e) = e
smtExprType :: SMTExpr h tp -> TypeMap tp
smtExprType (SMTName tp _) = tp
smtExprType (SMTExpr tp _) = tp
data WriterState = WriterState { _nextTermIdx :: !Word64
, _lastPosition :: !Position
, _position :: !Position
}
nextTermIdx :: Lens' WriterState Word64
nextTermIdx = lens _nextTermIdx (\s v -> s { _nextTermIdx = v })
lastPosition :: Lens' WriterState Position
lastPosition = lens _lastPosition (\s v -> s { _lastPosition = v })
position :: Lens' WriterState Position
position = lens _position (\s v -> s { _position = v })
emptyState :: WriterState
emptyState = WriterState { _nextTermIdx = 0
, _lastPosition = InternalPos
, _position = InternalPos
}
freshVarName :: State WriterState Text
freshVarName = freshVarName' "x!"
freshVarName' :: Builder -> State WriterState Text
freshVarName' prefix = do
n <- use nextTermIdx
nextTermIdx += 1
return $! (Lazy.toStrict $ Builder.toLazyText $ prefix <> Builder.decimal n)
data SMTSymFn ctx where
SMTSymFn :: !Text
-> !(Ctx.Assignment TypeMap args)
-> !(TypeMap ret)
-> SMTSymFn (args Ctx.::> ret)
data StackEntry t (h :: Type) = StackEntry
{ symExprCache :: !(IdxCache t (SMTExpr h))
, symFnCache :: !(PH.HashTable PH.RealWorld (Nonce t) SMTSymFn)
}
data WriterConn t (h :: Type) =
WriterConn { smtWriterName :: !String
, connHandle :: !(OutputStream Text)
, connInputHandle :: !(InputStream Text)
, supportFunctionDefs :: !Bool
, supportFunctionArguments :: !Bool
, supportQuantifiers :: !Bool
, supportedFeatures :: !ProblemFeatures
, entryStack :: !(IORef [StackEntry t h])
, stateRef :: !(IORef WriterState)
, varBindings :: !(SymbolVarBimap t)
, connState :: !h
, consumeAcknowledgement :: AcknowledgementAction t h
}
newtype AcknowledgementAction t h =
AckAction { runAckAction :: WriterConn t h -> Command h -> IO () }
nullAcknowledgementAction :: AcknowledgementAction t h
nullAcknowledgementAction = AckAction (\_ _ -> return ())
newStackEntry :: IO (StackEntry t h)
newStackEntry = do
exprCache <- newIdxCache
fnCache <- stToIO $ PH.new
return StackEntry
{ symExprCache = exprCache
, symFnCache = fnCache
}
resetEntryStack :: WriterConn t h -> IO ()
resetEntryStack c = do
entry <- newStackEntry
writeIORef (entryStack c) [entry]
popEntryStackToTop :: WriterConn t h -> IO Int
popEntryStackToTop c = do
stk <- readIORef (entryStack c)
if null stk then
do entry <- newStackEntry
writeIORef (entryStack c) [entry]
return 0
else
do writeIORef (entryStack c) [last stk]
return (length stk)
entryStackHeight :: WriterConn t h -> IO Int
entryStackHeight c =
do es <- readIORef (entryStack c)
return (length es - 1)
pushEntryStack :: WriterConn t h -> IO ()
pushEntryStack c = do
entry <- newStackEntry
modifyIORef' (entryStack c) $ (entry:)
popEntryStack :: WriterConn t h -> IO ()
popEntryStack c = do
stk <- readIORef (entryStack c)
case stk of
[] -> fail "Could not pop from empty entry stack."
[_] -> fail "Could not pop from empty entry stack."
(_:r) -> writeIORef (entryStack c) r
newWriterConn :: OutputStream Text
-> InputStream Text
-> AcknowledgementAction t cs
-> String
-> ProblemFeatures
-> SymbolVarBimap t
-> cs
-> IO (WriterConn t cs)
newWriterConn h in_h ack solver_name features bindings cs = do
entry <- newStackEntry
stk_ref <- newIORef [entry]
r <- newIORef emptyState
return $! WriterConn { smtWriterName = solver_name
, connHandle = h
, connInputHandle = in_h
, supportFunctionDefs = False
, supportFunctionArguments = False
, supportQuantifiers = False
, supportedFeatures = features
, entryStack = stk_ref
, stateRef = r
, varBindings = bindings
, connState = cs
, consumeAcknowledgement = ack
}
data TermLifetime
= DeleteNever
| DeleteOnPop
deriving (Eq)
cacheValue
:: WriterConn t h
-> TermLifetime
-> (StackEntry t h -> IO ())
-> IO ()
cacheValue conn lifetime insert_action =
readIORef (entryStack conn) >>= \case
s@(h:_) -> case lifetime of
DeleteOnPop -> insert_action h
DeleteNever -> mapM_ insert_action s
[] -> error "cacheValue: empty cache stack!"
cacheLookup
:: WriterConn t h
-> (StackEntry t h -> IO (Maybe a))
-> IO (Maybe a)
cacheLookup conn lookup_action =
readIORef (entryStack conn) >>= firstJustM lookup_action
cacheLookupExpr :: WriterConn t h -> Nonce t tp -> IO (Maybe (SMTExpr h tp))
cacheLookupExpr c n = cacheLookup c $ \entry ->
lookupIdx (symExprCache entry) n
cacheLookupFn :: WriterConn t h -> Nonce t ctx -> IO (Maybe (SMTSymFn ctx))
cacheLookupFn c n = cacheLookup c $ \entry ->
stToIO $ PH.lookup (symFnCache entry) n
cacheValueExpr
:: WriterConn t h -> Nonce t tp -> TermLifetime -> SMTExpr h tp -> IO ()
cacheValueExpr conn n lifetime value = cacheValue conn lifetime $ \entry ->
insertIdxValue (symExprCache entry) n value
cacheValueFn
:: WriterConn t h -> Nonce t ctx -> TermLifetime -> SMTSymFn ctx -> IO ()
cacheValueFn conn n lifetime value = cacheValue conn lifetime $ \entry ->
stToIO $ PH.insert (symFnCache entry) n value
withWriterState :: WriterConn t h -> State WriterState a -> IO a
withWriterState c m = do
s0 <- readIORef (stateRef c)
let (v,s) = runState m s0
writeIORef (stateRef c) $! s
return v
updateProgramLoc :: WriterConn t h -> ProgramLoc -> IO ()
updateProgramLoc c l = withWriterState c $ position .= plSourceLoc l
type family Command (h :: Type) :: Type
class (SupportTermOps (Term h)) => SMTWriter h where
forallExpr :: [(Text, Some TypeMap)] -> Term h -> Term h
existsExpr :: [(Text, Some TypeMap)] -> Term h -> Term h
arrayConstant :: Maybe (ArrayConstantFn (Term h))
arrayConstant = Nothing
arraySelect :: Term h -> [Term h] -> Term h
arrayUpdate :: Term h -> [Term h] -> Term h -> Term h
commentCommand :: f h -> Builder -> Command h
assertCommand :: f h -> Term h -> Command h
assertNamedCommand :: f h -> Term h -> Text -> Command h
pushCommand :: f h -> Command h
popCommand :: f h -> Command h
popManyCommands :: f h -> Int -> [Command h]
popManyCommands w n = replicate n (popCommand w)
resetCommand :: f h -> Command h
checkCommands :: f h -> [Command h]
checkWithAssumptionsCommands :: f h -> [Text] -> [Command h]
getUnsatAssumptionsCommand :: f h -> Command h
getUnsatCoreCommand :: f h -> Command h
setOptCommand :: f h -> Text -> Text -> Command h
declareCommand :: f h
-> Text
-> Ctx.Assignment TypeMap args
-> TypeMap rtp
-> Command h
defineCommand :: f h
-> Text
-> [(Text, Some TypeMap)]
-> TypeMap rtp
-> Term h
-> Command h
declareStructDatatype :: WriterConn t h -> Ctx.Assignment TypeMap args -> IO ()
structCtor :: Ctx.Assignment TypeMap args -> [Term h] -> Term h
structProj :: Ctx.Assignment TypeMap args -> Ctx.Index args tp -> Term h -> Term h
stringTerm :: ByteString -> Term h
stringLength :: Term h -> Term h
stringIndexOf :: Term h -> Term h -> Term h -> Term h
stringContains :: Term h -> Term h -> Term h
stringIsPrefixOf :: Term h -> Term h -> Term h
stringIsSuffixOf :: Term h -> Term h -> Term h
stringSubstring :: Term h -> Term h -> Term h -> Term h
stringAppend :: [Term h] -> Term h
resetDeclaredStructs :: WriterConn t h -> IO ()
writeCommand :: WriterConn t h -> Command h -> IO ()
addCommand :: SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommand conn cmd = do
addCommandNoAck conn cmd
runAckAction (consumeAcknowledgement conn) conn cmd
addCommandNoAck :: SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck conn cmd = do
las <- withWriterState conn $ use lastPosition
cur <- withWriterState conn $ use position
when (las /= cur) $ do
writeCommand conn $ commentCommand conn $ Builder.fromText $ Text.pack $ show $ pretty cur
withWriterState conn $ lastPosition .= cur
writeCommand conn cmd
addCommands :: SMTWriter h => WriterConn t h -> [Command h] -> IO ()
addCommands _ [] = fail "internal: empty list in addCommands"
addCommands conn cmds = do
mapM_ (addCommand conn) (init cmds)
addCommandNoAck conn (last cmds)
mkFreeVar :: SMTWriter h
=> WriterConn t h
-> Ctx.Assignment TypeMap args
-> TypeMap rtp
-> IO Text
mkFreeVar conn arg_types return_type = do
var <- withWriterState conn $ freshVarName
traverseFC_ (declareTypes conn) arg_types
declareTypes conn return_type
addCommand conn $ declareCommand conn var arg_types return_type
return var
mkFreeVar' :: SMTWriter h => WriterConn t h -> TypeMap tp -> IO (SMTExpr h tp)
mkFreeVar' conn tp = SMTName tp <$> mkFreeVar conn Ctx.empty tp
bindVarAsFree :: SMTWriter h
=> WriterConn t h
-> ExprBoundVar t tp
-> IO ()
bindVarAsFree conn var = do
cacheLookupExpr conn (bvarId var) >>= \case
Just _ -> fail $ "Internal error in SMTLIB exporter: bound variables cannot be made free."
++ show (bvarId var) ++ " defined at "
++ show (plSourceLoc (bvarLoc var)) ++ "."
Nothing -> do
smt_type <- runOnLiveConnection conn $ do
checkVarTypeSupport var
getBaseSMT_Type var
var_name <- getSymbolName conn (VarSymbolBinding var)
declareTypes conn smt_type
addCommand conn $ declareCommand conn var_name Ctx.empty smt_type
cacheValueExpr conn (bvarId var) DeleteOnPop $ SMTName smt_type var_name
assumeFormula :: SMTWriter h => WriterConn t h -> Term h -> IO ()
assumeFormula c p = addCommand c (assertCommand c p)
assumeFormulaWithName :: SMTWriter h => WriterConn t h -> Term h -> Text -> IO ()
assumeFormulaWithName conn p nm =
do unless (supportedFeatures conn `hasProblemFeature` useUnsatCores) $
fail $ show $ text (smtWriterName conn) <+> text "is not configured to produce UNSAT cores"
addCommand conn (assertNamedCommand conn p nm)
assumeFormulaWithFreshName :: SMTWriter h => WriterConn t h -> Term h -> IO Text
assumeFormulaWithFreshName conn p =
do var <- withWriterState conn $ freshVarName
assumeFormulaWithName conn p var
return var
declareTypes ::
SMTWriter h =>
WriterConn t h ->
TypeMap tp ->
IO ()
declareTypes conn = \case
BoolTypeMap -> return ()
NatTypeMap -> return ()
IntegerTypeMap -> return ()
RealTypeMap -> return ()
BVTypeMap _ -> return ()
FloatTypeMap _ -> return ()
Char8TypeMap -> return ()
ComplexToStructTypeMap -> declareStructDatatype conn (Ctx.Empty Ctx.:> RealTypeMap Ctx.:> RealTypeMap)
ComplexToArrayTypeMap -> return ()
PrimArrayTypeMap args ret ->
do traverseFC_ (declareTypes conn) args
declareTypes conn ret
FnArrayTypeMap args ret ->
do traverseFC_ (declareTypes conn) args
declareTypes conn ret
StructTypeMap flds ->
do traverseFC_ (declareTypes conn) flds
declareStructDatatype conn flds
data DefineStyle
= FunctionDefinition
| EqualityDefinition
deriving (Eq, Show)
defineSMTVar :: SMTWriter h
=> WriterConn t h
-> DefineStyle
-> Text
-> [(Text, Some TypeMap)]
-> TypeMap rtp
-> Term h
-> IO ()
defineSMTVar conn defSty var args return_type expr
| supportFunctionDefs conn && defSty == FunctionDefinition = do
mapM_ (viewSome (declareTypes conn) . snd) args
declareTypes conn return_type
addCommand conn $ defineCommand conn var args return_type expr
| otherwise = do
when (not (null args)) $ do
fail $ smtWriterName conn ++ " interface does not support defined functions."
declareTypes conn return_type
addCommand conn $ declareCommand conn var Ctx.empty return_type
assumeFormula conn $ fromText var .== expr
freshBoundVarName :: SMTWriter h
=> WriterConn t h
-> DefineStyle
-> [(Text, Some TypeMap)]
-> TypeMap rtp
-> Term h
-> IO Text
freshBoundVarName conn defSty args return_type expr = do
var <- withWriterState conn $ freshVarName
defineSMTVar conn defSty var args return_type expr
return var
data FreshVarFn h = FreshVarFn (forall tp . TypeMap tp -> IO (SMTExpr h tp))
data SMTCollectorState t h
= SMTCollectorState
{ scConn :: !(WriterConn t h)
, freshBoundTermFn :: !(forall rtp . Text -> [(Text, Some TypeMap)] -> TypeMap rtp -> Term h -> IO ())
, freshConstantFn :: !(Maybe (FreshVarFn h))
, recordSideCondFn :: !(Maybe (Term h -> IO ()))
}
type SMTCollector t h = ReaderT (SMTCollectorState t h) IO
freshConstant :: String
-> TypeMap tp
-> SMTCollector t h (SMTExpr h tp)
freshConstant nm tpr = do
mf <- asks freshConstantFn
case mf of
Nothing -> do
conn <- asks scConn
liftIO $ do
loc <- withWriterState conn $ use position
fail $ "Cannot create the free constant within a function needed to define the "
++ nm ++ " term created at " ++ show loc ++ "."
Just (FreshVarFn f) ->
liftIO $ f tpr
data BaseTypeError = ComplexTypeUnsupported
| ArrayUnsupported
| StringTypeUnsupported (Some StringInfoRepr)
typeMap :: WriterConn t h -> BaseTypeRepr tp -> Either BaseTypeError (TypeMap tp)
typeMap conn tp0 = do
case typeMapFirstClass conn tp0 of
Right tm -> Right tm
Left ArrayUnsupported
| supportFunctionDefs conn
, BaseArrayRepr idxTp eltTp <- tp0 ->
FnArrayTypeMap <$> traverseFC (typeMapFirstClass conn) idxTp
<*> typeMapFirstClass conn eltTp
Left e -> Left e
typeMapFirstClass :: WriterConn t h -> BaseTypeRepr tp -> Either BaseTypeError (TypeMap tp)
typeMapFirstClass conn tp0 = do
let feat = supportedFeatures conn
case tp0 of
BaseBoolRepr -> Right BoolTypeMap
BaseBVRepr w -> Right $! BVTypeMap w
BaseFloatRepr fpp -> Right $! FloatTypeMap fpp
BaseRealRepr -> Right RealTypeMap
BaseNatRepr -> Right NatTypeMap
BaseIntegerRepr -> Right IntegerTypeMap
BaseStringRepr Char8Repr -> Right Char8TypeMap
BaseStringRepr si -> Left (StringTypeUnsupported (Some si))
BaseComplexRepr
| feat `hasProblemFeature` useStructs -> Right ComplexToStructTypeMap
| feat `hasProblemFeature` useSymbolicArrays -> Right ComplexToArrayTypeMap
| otherwise -> Left ComplexTypeUnsupported
BaseArrayRepr idxTp eltTp -> do
let mkArray = if feat `hasProblemFeature` useSymbolicArrays
then PrimArrayTypeMap
else FnArrayTypeMap
mkArray <$> traverseFC (typeMapFirstClass conn) idxTp
<*> typeMapFirstClass conn eltTp
BaseStructRepr flds ->
StructTypeMap <$> traverseFC (typeMapFirstClass conn) flds
getBaseSMT_Type :: ExprBoundVar t tp -> SMTCollector t h (TypeMap tp)
getBaseSMT_Type v = do
conn <- asks scConn
let errMsg typename =
show
$ text (show (bvarName v))
<+> text "is a"
<+> text typename
<+> text "variable, and we do not support this with"
<+> text (smtWriterName conn ++ ".")
case typeMap conn (bvarType v) of
Left (StringTypeUnsupported (Some si)) -> fail $ errMsg ("string " ++ show si)
Left ComplexTypeUnsupported -> fail $ errMsg "complex"
Left ArrayUnsupported -> fail $ errMsg "array"
Right smtType -> return smtType
freshBoundFn :: [(Text, Some TypeMap)]
-> TypeMap rtp
-> Term h
-> SMTCollector t h Text
freshBoundFn args tp t = do
conn <- asks scConn
f <- asks freshBoundTermFn
liftIO $ do
var <- withWriterState conn $ freshVarName
f var args tp t
return var
freshBoundTerm :: TypeMap tp -> Term h -> SMTCollector t h (SMTExpr h tp)
freshBoundTerm tp t = SMTName tp <$> freshBoundFn [] tp t
freshBoundTerm' :: SupportTermOps (Term h) => SMTExpr h tp -> SMTCollector t h (SMTExpr h tp)
freshBoundTerm' t = SMTName tp <$> freshBoundFn [] tp (asBase t)
where tp = smtExprType t
addSideCondition ::
String ->
Term h ->
SMTCollector t h ()
addSideCondition nm t = do
conn <- asks scConn
mf <- asks recordSideCondFn
loc <- liftIO $ withWriterState conn $ use position
case mf of
Just f ->
liftIO $ f t
Nothing -> do
fail $ "Cannot add a side condition within a function needed to define the "
++ nm ++ " term created at " ++ show loc ++ "."
addPartialSideCond ::
forall t h tp.
SMTWriter h =>
WriterConn t h ->
Term h ->
TypeMap tp ->
Maybe (AbstractValue tp) ->
SMTCollector t h ()
addPartialSideCond _ t NatTypeMap Nothing =
do addSideCondition "nat_range" $ t .>= 0
addPartialSideCond _ _ _ Nothing = return ()
addPartialSideCond _ _ BoolTypeMap (Just Nothing) = return ()
addPartialSideCond _ t BoolTypeMap (Just (Just b)) =
addSideCondition "bool_val" $ t .== boolExpr b
addPartialSideCond _ t NatTypeMap (Just rng) =
do addSideCondition "nat_range" $ t .>= integerTerm (toInteger (natRangeLow rng))
case natRangeHigh rng of
Unbounded -> return ()
Inclusive hi -> addSideCondition "nat_range" $ t .<= integerTerm (toInteger hi)
addPartialSideCond _ t IntegerTypeMap (Just rng) =
do case rangeLowBound rng of
Unbounded -> return ()
Inclusive lo -> addSideCondition "int_range" $ t .>= integerTerm lo
case rangeHiBound rng of
Unbounded -> return ()
Inclusive hi -> addSideCondition "int_range" $ t .<= integerTerm hi
addPartialSideCond _ t RealTypeMap (Just rng) =
do case rangeLowBound (ravRange rng) of
Unbounded -> return ()
Inclusive lo -> addSideCondition "real_range" $ t .>= rationalTerm lo
case rangeHiBound (ravRange rng) of
Unbounded -> return ()
Inclusive hi -> addSideCondition "real_range" $ t .<= rationalTerm hi
addPartialSideCond _ t (BVTypeMap w) (Just (BVD.BVDArith rng)) = assertRange (BVD.arithDomainData rng)
where
assertRange Nothing = return ()
assertRange (Just (lo, sz)) =
addSideCondition "bv_range" $ bvULe (bvSub t (bvTerm w (BV.mkBV w lo))) (bvTerm w (BV.mkBV w sz))
addPartialSideCond _ t (BVTypeMap w) (Just (BVD.BVDBitwise rng)) = assertBitRange (BVD.bitbounds rng)
where
assertBitRange (lo, hi) = do
when (lo > 0) $
addSideCondition "bv_bitrange" $ (bvOr (bvTerm w (BV.mkBV w lo)) t) .== t
when (hi < maxUnsigned w) $
addSideCondition "bv_bitrange" $ (bvOr t (bvTerm w (BV.mkBV w hi))) .== (bvTerm w (BV.mkBV w hi))
addPartialSideCond _ t (Char8TypeMap) (Just (StringAbs len)) =
do case natRangeLow len of
0 -> return ()
lo -> addSideCondition "string length low range" $
integerTerm (toInteger lo) .<= stringLength @h t
case natRangeHigh len of
Unbounded -> return ()
Inclusive hi ->
addSideCondition "string length high range" $
stringLength @h t .<= integerTerm (toInteger hi)
addPartialSideCond _ _ (FloatTypeMap _) (Just ()) = return ()
addPartialSideCond conn t ComplexToStructTypeMap (Just (realRng :+ imagRng)) =
do let r = arrayComplexRealPart @h t
let i = arrayComplexImagPart @h t
addPartialSideCond conn r RealTypeMap (Just realRng)
addPartialSideCond conn i RealTypeMap (Just imagRng)
addPartialSideCond conn t ComplexToArrayTypeMap (Just (realRng :+ imagRng)) =
do let r = arrayComplexRealPart @h t
let i = arrayComplexImagPart @h t
addPartialSideCond conn r RealTypeMap (Just realRng)
addPartialSideCond conn i RealTypeMap (Just imagRng)
addPartialSideCond conn t (StructTypeMap ctx) (Just abvs) =
Ctx.forIndex (Ctx.size ctx)
(\start i ->
do start
addPartialSideCond conn
(structProj @h ctx i t)
(ctx Ctx.! i)
(Just (unwrapAV (abvs Ctx.! i))))
(return ())
addPartialSideCond _ _t (PrimArrayTypeMap _idxTp _resTp) (Just _abv) =
fail "SMTWriter.addPartialSideCond: bounds on array values not supported"
addPartialSideCond _ _t (FnArrayTypeMap _idxTp _resTp) (Just _abv) =
fail "SMTWriter.addPartialSideCond: bounds on array values not supported"
runOnLiveConnection :: SMTWriter h => WriterConn t h -> SMTCollector t h a -> IO a
runOnLiveConnection conn coll = runReaderT coll s
where s = SMTCollectorState
{ scConn = conn
, freshBoundTermFn = defineSMTVar conn FunctionDefinition
, freshConstantFn = Just $! FreshVarFn (mkFreeVar' conn)
, recordSideCondFn = Just $! assumeFormula conn
}
prependToRefList :: IORef [a] -> a -> IO ()
prependToRefList r a = seq a $ modifyIORef' r (a:)
freshSandboxBoundTerm :: SupportTermOps v
=> IORef [(Text, v)]
-> Text
-> [(Text, Some TypeMap)]
-> TypeMap rtp
-> v
-> IO ()
freshSandboxBoundTerm ref var [] _ t = do
prependToRefList ref (var,t)
freshSandboxBoundTerm ref var args _ t = do
case lambdaTerm of
Nothing -> do
fail $ "Cannot create terms with arguments inside defined functions."
Just lambdaFn -> do
let r = lambdaFn args t
seq r $ prependToRefList ref (var, r)
freshSandboxConstant :: WriterConn t h
-> IORef [(Text, Some TypeMap)]
-> TypeMap tp
-> IO (SMTExpr h tp)
freshSandboxConstant conn ref tp = do
var <- withWriterState conn $ freshVarName
prependToRefList ref (var, Some tp)
return $! SMTName tp var
data CollectorResults h a =
CollectorResults { crResult :: !a
, crBindings :: !([(Text, Term h)])
, crFreeConstants :: !([(Text, Some TypeMap)])
, crSideConds :: !([Term h])
}
forallResult :: forall h
. SMTWriter h
=> CollectorResults h (Term h)
-> Term h
forallResult cr =
forallExpr @h (crFreeConstants cr) $
letExpr (crBindings cr) $
impliesAllExpr (crSideConds cr) (crResult cr)
impliesAllExpr :: SupportTermOps v => [v] -> v -> v
impliesAllExpr l r = orAll ((notExpr <$> l) ++ [r])
existsResult :: forall h
. SMTWriter h
=> CollectorResults h (Term h)
-> Term h
existsResult cr =
existsExpr @h (crFreeConstants cr) $
letExpr (crBindings cr) $
andAll (crSideConds cr ++ [crResult cr])
runInSandbox :: SupportTermOps (Term h)
=> WriterConn t h
-> SMTCollector t h a
-> IO (CollectorResults h a)
runInSandbox conn sc = do
boundTermRef <- newIORef []
freeConstantRef <- (newIORef [] :: IO (IORef [(Text, Some TypeMap)]))
sideCondRef <- newIORef []
let s = SMTCollectorState
{ scConn = conn
, freshBoundTermFn = freshSandboxBoundTerm boundTermRef
, freshConstantFn = Just $! FreshVarFn (freshSandboxConstant conn freeConstantRef)
, recordSideCondFn = Just $! prependToRefList sideCondRef
}
r <- runReaderT sc s
boundTerms <- readIORef boundTermRef
freeConstants <- readIORef freeConstantRef
sideConds <- readIORef sideCondRef
return $! CollectorResults { crResult = r
, crBindings = reverse boundTerms
, crFreeConstants = reverse freeConstants
, crSideConds = reverse sideConds
}
cacheWriterResult :: Nonce t tp
-> TermLifetime
-> SMTCollector t h (SMTExpr h tp)
-> SMTCollector t h (SMTExpr h tp)
cacheWriterResult n lifetime fallback = do
c <- asks scConn
(liftIO $ cacheLookupExpr c n) >>= \case
Just x -> return x
Nothing -> do
x <- fallback
liftIO $ cacheValueExpr c n lifetime x
return x
bindVar :: ExprBoundVar t tp
-> SMTExpr h tp
-> SMTCollector t h ()
bindVar v x = do
let n = bvarId v
c <- asks scConn
liftIO $ do
whenM (isJust <$> cacheLookupExpr c n) $ fail "Variable is already bound."
cacheValueExpr c n DeleteOnPop x
bvIntTerm :: forall v w
. (SupportTermOps v, 1 <= w)
=> NatRepr w
-> v
-> v
bvIntTerm w x = sumExpr ((\i -> digit (i-1)) <$> [1..natValue w])
where digit :: Natural -> v
digit d = ite (bvTestBit w d x)
(fromInteger (2^d))
0
sbvIntTerm :: SupportTermOps v
=> NatRepr w
-> v
-> v
sbvIntTerm w0 x0 = sumExpr (signed_offset : go w0 x0 (natValue w0 - 2))
where signed_offset = ite (bvTestBit w0 (natValue w0 - 1) x0)
(fromInteger (negate (2^(widthVal w0 - 1))))
0
go :: SupportTermOps v => NatRepr w -> v -> Natural -> [v]
go w x n
| n > 0 = digit w x n : go w x (n-1)
| n == 0 = [digit w x 0]
| otherwise = []
digit :: SupportTermOps v => NatRepr w -> v -> Natural -> v
digit w x d = ite (bvTestBit w d x)
(fromInteger (2^d))
0
unsupportedTerm :: MonadFail m => Expr t tp -> m a
unsupportedTerm e =
fail $ show $
text "Cannot generate solver output for term generated at"
<+> pretty (plSourceLoc (exprLoc e)) <> text ":" <$$>
indent 2 (pretty e)
checkVarTypeSupport :: ExprBoundVar n tp -> SMTCollector n h ()
checkVarTypeSupport var = do
let t = BoundVarExpr var
case bvarType var of
BaseNatRepr -> checkIntegerSupport t
BaseIntegerRepr -> checkIntegerSupport t
BaseRealRepr -> checkLinearSupport t
BaseComplexRepr -> checkLinearSupport t
BaseStringRepr _ -> checkStringSupport t
BaseFloatRepr _ -> checkFloatSupport t
BaseBVRepr _ -> checkBitvectorSupport t
_ -> return ()
theoryUnsupported :: MonadFail m => WriterConn t h -> String -> Expr t tp -> m a
theoryUnsupported conn theory_name t =
fail $ show $
text (smtWriterName conn) <+> text "does not support the" <+> text theory_name
<+> text "term generated at" <+> pretty (plSourceLoc (exprLoc t))
checkIntegerSupport :: Expr t tp -> SMTCollector t h ()
checkIntegerSupport t = do
conn <- asks scConn
unless (supportedFeatures conn `hasProblemFeature` useIntegerArithmetic) $ do
theoryUnsupported conn "integer arithmetic" t
checkStringSupport :: Expr t tp -> SMTCollector t h ()
checkStringSupport t = do
conn <- asks scConn
unless (supportedFeatures conn `hasProblemFeature` useStrings) $ do
theoryUnsupported conn "string" t
checkBitvectorSupport :: Expr t tp -> SMTCollector t h ()
checkBitvectorSupport t = do
conn <- asks scConn
unless (supportedFeatures conn `hasProblemFeature` useBitvectors) $ do
theoryUnsupported conn "bitvector" t
checkFloatSupport :: Expr t tp -> SMTCollector t h ()
checkFloatSupport t = do
conn <- asks scConn
unless (supportedFeatures conn `hasProblemFeature` useFloatingPoint) $ do
theoryUnsupported conn "floating-point arithmetic" t
checkLinearSupport :: Expr t tp -> SMTCollector t h ()
checkLinearSupport t = do
conn <- asks scConn
unless (supportedFeatures conn `hasProblemFeature` useLinearArithmetic) $ do
theoryUnsupported conn "linear arithmetic" t
checkNonlinearSupport :: Expr t tp -> SMTCollector t h ()
checkNonlinearSupport t = do
conn <- asks scConn
unless (supportedFeatures conn `hasProblemFeature` useNonlinearArithmetic) $ do
theoryUnsupported conn "non-linear arithmetic" t
checkComputableSupport :: Expr t tp -> SMTCollector t h ()
checkComputableSupport t = do
conn <- asks scConn
unless (supportedFeatures conn `hasProblemFeature` useComputableReals) $ do
theoryUnsupported conn "computable arithmetic" t
checkQuantifierSupport :: String -> Expr t p -> SMTCollector t h ()
checkQuantifierSupport nm t = do
conn <- asks scConn
when (supportQuantifiers conn == False) $ do
theoryUnsupported conn nm t
checkArgumentTypes :: WriterConn t h -> Ctx.Assignment TypeMap args -> IO ()
checkArgumentTypes conn types = do
forFC_ types $ \tp -> do
case tp of
FnArrayTypeMap{} | supportFunctionArguments conn == False -> do
fail $ show $ text (smtWriterName conn)
<+> text "does not allow arrays encoded as functions to be function arguments."
_ ->
return ()
type SMTSource = String -> BaseTypeError -> Doc
ppBaseTypeError :: BaseTypeError -> Doc
ppBaseTypeError ComplexTypeUnsupported = text "complex values"
ppBaseTypeError ArrayUnsupported = text "arrays encoded as a functions"
ppBaseTypeError (StringTypeUnsupported (Some si)) = text ("string values " ++ show si)
eltSource :: Expr t tp -> SMTSource
eltSource e solver_name cause =
text solver_name <+>
text "does not support" <+> ppBaseTypeError cause <>
text ", and cannot interpret the term generated at" <+>
pretty (plSourceLoc (exprLoc e)) <> text ":" <$$>
indent 2 (pretty e) <> text "."
fnSource :: SolverSymbol -> ProgramLoc -> SMTSource
fnSource fn_name loc solver_name cause =
text solver_name <+>
text "does not support" <+> ppBaseTypeError cause <>
text ", and cannot interpret the function" <+> text (show fn_name) <+>
text "generated at" <+> pretty (plSourceLoc loc) <> text "."
evalFirstClassTypeRepr :: MonadFail m
=> WriterConn t h
-> SMTSource
-> BaseTypeRepr tp
-> m (TypeMap tp)
evalFirstClassTypeRepr conn src base_tp =
case typeMapFirstClass conn base_tp of
Left e -> fail $ show $ src (smtWriterName conn) e
Right smt_ret -> return smt_ret
withConnEntryStack :: WriterConn t h -> IO a -> IO a
withConnEntryStack conn = bracket_ (pushEntryStack conn) (popEntryStack conn)
mkIndexLitTerm :: SupportTermOps v
=> IndexLit tp
-> v
mkIndexLitTerm (NatIndexLit i) = fromIntegral i
mkIndexLitTerm (BVIndexLit w i) = bvTerm w i
mkIndexLitTerms :: SupportTermOps v
=> Ctx.Assignment IndexLit ctx
-> [v]
mkIndexLitTerms = toListFC mkIndexLitTerm
createTypeMapArgsForArray :: forall t h args
. WriterConn t h
-> Ctx.Assignment TypeMap args
-> IO [(Text, Some TypeMap)]
createTypeMapArgsForArray conn types = do
let mkIndexVar :: TypeMap utp -> IO (Text, Some TypeMap)
mkIndexVar base_tp = do
i_nm <- withWriterState conn $ freshVarName' "i!"
return (i_nm, Some base_tp)
sequence $ toListFC mkIndexVar types
smt_array_select :: forall h idxl idx tp
. SMTWriter h
=> SMTExpr h (BaseArrayType (idxl Ctx.::> idx) tp)
-> [Term h]
-> SMTExpr h tp
smt_array_select aexpr idxl =
case smtExprType aexpr of
PrimArrayTypeMap _ res_type ->
SMTExpr res_type $ arraySelect @h (asBase aexpr) idxl
FnArrayTypeMap _ res_type ->
SMTExpr res_type $ smtFnApp (asBase aexpr) idxl
getSymbolName :: WriterConn t h -> SymbolBinding t -> IO Text
getSymbolName conn b =
case lookupSymbolOfBinding b (varBindings conn) of
Just sym -> return $! solverSymbolAsText sym
Nothing -> withWriterState conn $ freshVarName
defineSMTFunction :: SMTWriter h
=> WriterConn t h
-> Text
-> (FreshVarFn h -> SMTCollector t h (SMTExpr h ret))
-> IO (TypeMap ret)
defineSMTFunction conn var action =
withConnEntryStack conn $ do
freeConstantRef <- (newIORef [] :: IO (IORef [(Text, Some TypeMap)]))
boundTermRef <- newIORef []
let s = SMTCollectorState { scConn = conn
, freshBoundTermFn = freshSandboxBoundTerm boundTermRef
, freshConstantFn = Nothing
, recordSideCondFn = Nothing
}
let varFn = FreshVarFn (freshSandboxConstant conn freeConstantRef)
pair <- flip runReaderT s (action varFn)
args <- readIORef freeConstantRef
boundTerms <- readIORef boundTermRef
let res = letExpr (reverse boundTerms) (asBase pair)
defineSMTVar conn FunctionDefinition var (reverse args) (smtExprType pair) res
return $! smtExprType pair
mkExpr :: forall h t tp. SMTWriter h => Expr t tp -> SMTCollector t h (SMTExpr h tp)
mkExpr (BoolExpr b _) =
return (SMTExpr BoolTypeMap (boolExpr b))
mkExpr t@(SemiRingLiteral SR.SemiRingNatRepr n _) = do
checkLinearSupport t
return (SMTExpr NatTypeMap (fromIntegral n))
mkExpr t@(SemiRingLiteral SR.SemiRingIntegerRepr i _) = do
checkLinearSupport t
return (SMTExpr IntegerTypeMap (fromIntegral i))
mkExpr t@(SemiRingLiteral SR.SemiRingRealRepr r _) = do
checkLinearSupport t
return (SMTExpr RealTypeMap (rationalTerm r))
mkExpr t@(SemiRingLiteral (SR.SemiRingBVRepr _flv w) x _) = do
checkBitvectorSupport t
return $ SMTExpr (BVTypeMap w) $ bvTerm w x
mkExpr t@(StringExpr l _) =
case l of
Char8Literal bs -> do
checkStringSupport t
return $ SMTExpr Char8TypeMap $ stringTerm @h bs
_ -> do
conn <- asks scConn
theoryUnsupported conn ("strings " ++ show (stringLiteralInfo l)) t
mkExpr (NonceAppExpr ea) =
cacheWriterResult (nonceExprId ea) DeleteOnPop $
predSMTExpr ea
mkExpr (AppExpr ea) =
cacheWriterResult (appExprId ea) DeleteOnPop $ do
appSMTExpr ea
mkExpr (BoundVarExpr var) = do
case bvarKind var of
QuantifierVarKind -> do
conn <- asks scConn
mr <- liftIO $ cacheLookupExpr conn (bvarId var)
case mr of
Just x -> return x
Nothing -> do
fail $ "Internal error in SMTLIB exporter due to unbound variable "
++ show (bvarId var) ++ " defined at "
++ show (plSourceLoc (bvarLoc var)) ++ "."
LatchVarKind ->
fail $ "SMTLib exporter does not support the latch defined at "
++ show (plSourceLoc (bvarLoc var)) ++ "."
UninterpVarKind -> do
conn <- asks scConn
cacheWriterResult (bvarId var) DeleteNever $ do
checkVarTypeSupport var
var_name <- liftIO $ getSymbolName conn (VarSymbolBinding var)
smt_type <- getBaseSMT_Type var
liftIO $
do declareTypes conn smt_type
addCommand conn $ declareCommand conn var_name Ctx.empty smt_type
addPartialSideCond conn (fromText var_name) smt_type (bvarAbstractValue var)
return $ SMTName smt_type var_name
mkBaseExpr :: SMTWriter h => Expr t tp -> SMTCollector t h (Term h)
mkBaseExpr e = asBase <$> mkExpr e
mkIndicesTerms :: SMTWriter h
=> Ctx.Assignment (Expr t) ctx
-> SMTCollector t h [Term h]
mkIndicesTerms = foldrFC (\e r -> (:) <$> mkBaseExpr e <*> r) (pure [])
predSMTExpr :: forall t h tp
. SMTWriter h
=> NonceAppExpr t tp
-> SMTCollector t h (SMTExpr h tp)
predSMTExpr e0 = do
conn <- asks scConn
let i = NonceAppExpr e0
h <- asks scConn
liftIO $ updateProgramLoc h (nonceExprLoc e0)
case nonceExprApp e0 of
Annotation _tpr _n e -> mkExpr e
Forall var e -> do
checkQuantifierSupport "universal quantifier" i
smtType <- getBaseSMT_Type var
liftIO $ declareTypes h smtType
cr <- liftIO $ withConnEntryStack conn $ do
runInSandbox conn $ do
checkVarTypeSupport var
Just (FreshVarFn f) <- asks freshConstantFn
t <- liftIO $ f smtType
bindVar var t
addPartialSideCond conn (asBase t) smtType (bvarAbstractValue var)
mkBaseExpr e
freshBoundTerm BoolTypeMap $ forallResult cr
Exists var e -> do
checkQuantifierSupport "existential quantifiers" i
smtType <- getBaseSMT_Type var
liftIO $ declareTypes h smtType
cr <- liftIO $ withConnEntryStack conn $ do
runInSandbox conn $ do
checkVarTypeSupport var
Just (FreshVarFn f) <- asks freshConstantFn
t <- liftIO $ f smtType
bindVar var t
addPartialSideCond conn (asBase t) smtType (bvarAbstractValue var)
mkBaseExpr e
freshBoundTerm BoolTypeMap $ existsResult cr
ArrayFromFn f -> do
smt_arg_types <-
traverseFC (evalFirstClassTypeRepr conn (eltSource i))
(symFnArgTypes f)
(smt_f, ret_tp) <- liftIO $ getSMTSymFn conn f smt_arg_types
let array_tp = FnArrayTypeMap smt_arg_types ret_tp
return $! SMTName array_tp smt_f
MapOverArrays f idx_types arrays -> do
smt_idx_types <- traverseFC (evalFirstClassTypeRepr conn (eltSource i)) idx_types
let evalArray :: forall idx itp etp
. ArrayResultWrapper (Expr t) (idx Ctx.::> itp) etp
-> SMTCollector t h (ArrayResultWrapper (SMTExpr h) (idx Ctx.::> itp) etp)
evalArray (ArrayResultWrapper a) = ArrayResultWrapper <$> mkExpr a
smt_arrays <- traverseFC evalArray arrays
liftIO $ do
nm <- liftIO $ withWriterState conn $ freshVarName
ret_type <-
defineSMTFunction conn nm $ \(FreshVarFn freshVar) -> do
smt_indices <- traverseFC (\tp -> liftIO (freshVar tp)) smt_idx_types
let idxl = toListFC asBase smt_indices
let select :: forall idxl idx etp
. ArrayResultWrapper (SMTExpr h) (idxl Ctx.::> idx) etp
-> SMTExpr h etp
select (ArrayResultWrapper a) = smt_array_select a idxl
let array_vals = fmapFC select smt_arrays
(smt_f, ret_type) <- liftIO $ getSMTSymFn conn f (fmapFC smtExprType array_vals)
return $ SMTExpr ret_type $ smtFnApp (fromText smt_f) (toListFC asBase array_vals)
let array_tp = FnArrayTypeMap smt_idx_types ret_type
return $! SMTName array_tp nm
ArrayTrueOnEntries{} -> do
fail $ "SMTWriter does not yet support ArrayTrueOnEntries.\n" ++ show i
FnApp f args -> do
smt_args <- traverseFC mkExpr args
(smt_f, ret_type) <- liftIO $ getSMTSymFn conn f (fmapFC smtExprType smt_args)
freshBoundTerm ret_type $! smtFnApp (fromText smt_f) (toListFC asBase smt_args)
appSMTExpr :: forall t h tp
. SMTWriter h
=> AppExpr t tp
-> SMTCollector t h (SMTExpr h tp)
appSMTExpr ae = do
conn <- asks scConn
let i = AppExpr ae
liftIO $ updateProgramLoc conn (appExprLoc ae)
case appExprApp ae of
BaseEq _ x y ->
do xe <- mkExpr x
ye <- mkExpr y
let xtp = smtExprType xe
let ytp = smtExprType ye
let checkArrayType z (FnArrayTypeMap{}) = do
fail $ show $ text (smtWriterName conn) <+>
text "does not support checking equality for the array generated at"
<+> pretty (plSourceLoc (exprLoc z)) <> text ":" <$$>
indent 2 (pretty z)
checkArrayType _ _ = return ()
checkArrayType x xtp
checkArrayType y ytp
when (xtp /= ytp) $ do
fail $ unwords ["Type representations are not equal:", show xtp, show ytp]
freshBoundTerm BoolTypeMap $ asBase xe .== asBase ye
BaseIte btp _ c x y -> do
let errMsg typename =
show
$ text "we do not support if/then/else expressions at type"
<+> text typename
<+> text "with solver"
<+> text (smtWriterName conn ++ ".")
case typeMap conn btp of
Left (StringTypeUnsupported (Some si)) -> fail $ errMsg ("string " ++ show si)
Left ComplexTypeUnsupported -> fail $ errMsg "complex"
Left ArrayUnsupported -> fail $ errMsg "array"
Right FnArrayTypeMap{} -> fail $ errMsg "function-backed array"
Right tym ->
do cb <- mkBaseExpr c
xb <- mkBaseExpr x
yb <- mkBaseExpr y
freshBoundTerm tym $ ite cb xb yb
SemiRingLe _sr x y -> do
xb <- mkBaseExpr x
yb <- mkBaseExpr y
freshBoundTerm BoolTypeMap $ xb .<= yb
RealIsInteger r -> do
rb <- mkBaseExpr r
freshBoundTerm BoolTypeMap $! realIsInteger rb
BVTestBit n xe -> do
x <- mkBaseExpr xe
let this_bit = bvExtract (bvWidth xe) n 1 x
one = bvTerm (knownNat :: NatRepr 1) (BV.one knownNat)
freshBoundTerm BoolTypeMap $ this_bit .== one
BVSlt xe ye -> do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm BoolTypeMap $ x `bvSLt` y
BVUlt xe ye -> do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm BoolTypeMap $ x `bvULt` y
IntDiv xe ye -> do
case ye of
SemiRingLiteral _ _ _ -> return ()
_ -> checkNonlinearSupport i
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm IntegerTypeMap (intDiv x y)
IntMod xe ye -> do
case ye of
SemiRingLiteral _ _ _ -> return ()
_ -> checkNonlinearSupport i
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm IntegerTypeMap (intMod x y)
IntAbs xe -> do
x <- mkBaseExpr xe
freshBoundTerm IntegerTypeMap (intAbs x)
IntDivisible xe k -> do
x <- mkBaseExpr xe
freshBoundTerm BoolTypeMap (intDivisible x k)
NatDiv xe ye -> do
case ye of
SemiRingLiteral _ _ _ -> return ()
_ -> checkNonlinearSupport i
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm NatTypeMap (intDiv x y)
NatMod xe ye -> do
case ye of
SemiRingLiteral _ _ _ -> return ()
_ -> checkNonlinearSupport i
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm NatTypeMap (intMod x y)
NotPred x -> freshBoundTerm BoolTypeMap . notExpr =<< mkBaseExpr x
ConjPred xs ->
let pol (x,Positive) = mkBaseExpr x
pol (x,Negative) = notExpr <$> mkBaseExpr x
in
case BM.viewBoolMap xs of
BM.BoolMapUnit ->
return $ SMTExpr BoolTypeMap $ boolExpr True
BM.BoolMapDualUnit ->
return $ SMTExpr BoolTypeMap $ boolExpr False
BM.BoolMapTerms (t:|[]) ->
SMTExpr BoolTypeMap <$> pol t
BM.BoolMapTerms (t:|ts) ->
do cnj <- andAll <$> mapM pol (t:ts)
freshBoundTerm BoolTypeMap cnj
SemiRingProd pd ->
case WSum.prodRepr pd of
SR.SemiRingBVRepr SR.BVArithRepr w ->
do pd' <- WSum.prodEvalM (\a b -> pure (bvMul a b)) mkBaseExpr pd
maybe (return $ SMTExpr (BVTypeMap w) $ bvTerm w (BV.one w))
(freshBoundTerm (BVTypeMap w))
pd'
SR.SemiRingBVRepr SR.BVBitsRepr w ->
do pd' <- WSum.prodEvalM (\a b -> pure (bvAnd a b)) mkBaseExpr pd
maybe (return $ SMTExpr (BVTypeMap w) $ bvTerm w (BV.maxUnsigned w))
(freshBoundTerm (BVTypeMap w))
pd'
sr ->
do checkNonlinearSupport i
pd' <- WSum.prodEvalM (\a b -> pure (a * b)) mkBaseExpr pd
maybe (return $ SMTExpr (semiRingTypeMap sr) $ integerTerm 1)
(freshBoundTerm (semiRingTypeMap sr))
pd'
SemiRingSum s ->
case WSum.sumRepr s of
SR.SemiRingNatRepr ->
let smul c e
| c == 1 = (:[]) <$> mkBaseExpr e
| otherwise = (:[]) . (integerTerm (toInteger c) *) <$> mkBaseExpr e
cnst 0 = []
cnst x = [integerTerm (toInteger x)]
add x y = pure (y ++ x)
in
freshBoundTerm NatTypeMap . sumExpr
=<< WSum.evalM add smul (pure . cnst) s
SR.SemiRingIntegerRepr ->
let smul c e
| c == 1 = (:[]) <$> mkBaseExpr e
| c == -1 = (:[]) . negate <$> mkBaseExpr e
| otherwise = (:[]) . (integerTerm c *) <$> mkBaseExpr e
cnst 0 = []
cnst x = [integerTerm x]
add x y = pure (y ++ x)
in
freshBoundTerm IntegerTypeMap . sumExpr
=<< WSum.evalM add smul (pure . cnst) s
SR.SemiRingRealRepr ->
let smul c e
| c == 1 = (:[]) <$> mkBaseExpr e
| c == -1 = (:[]) . negate <$> mkBaseExpr e
| otherwise = (:[]) . (rationalTerm c *) <$> mkBaseExpr e
cnst 0 = []
cnst x = [rationalTerm x]
add x y = pure (y ++ x)
in
freshBoundTerm RealTypeMap . sumExpr
=<< WSum.evalM add smul (pure . cnst) s
SR.SemiRingBVRepr SR.BVArithRepr w ->
let smul c e
| c == BV.one w = (:[]) <$> mkBaseExpr e
| c == BV.maxUnsigned w = (:[]) . bvNeg <$> mkBaseExpr e
| otherwise = (:[]) <$> (bvMul (bvTerm w c)) <$> mkBaseExpr e
cnst (BV.BV 0) = []
cnst x = [bvTerm w x]
add x y = pure (y ++ x)
in
freshBoundTerm (BVTypeMap w) . bvSumExpr w
=<< WSum.evalM add smul (pure . cnst) s
SR.SemiRingBVRepr SR.BVBitsRepr w ->
let smul c e
| c == BV.maxUnsigned w = (:[]) <$> mkBaseExpr e
| otherwise = (:[]) <$> (bvAnd (bvTerm w c)) <$> mkBaseExpr e
cnst (BV.BV 0) = []
cnst x = [bvTerm w x]
add x y = pure (y ++ x)
xorsum [] = bvTerm w (BV.zero w)
xorsum xs = foldr1 bvXor xs
in
freshBoundTerm (BVTypeMap w) . xorsum
=<< WSum.evalM add smul (pure . cnst) s
RealDiv xe ye -> do
x <- mkBaseExpr xe
case ye of
SemiRingLiteral SR.SemiRingRealRepr r _ | r /= 0 -> do
freshBoundTerm RealTypeMap $ x * rationalTerm (recip r)
_ -> do
checkNonlinearSupport i
y <- mkBaseExpr ye
freshBoundTerm RealTypeMap $ realDiv x y
RealSqrt xe -> do
checkNonlinearSupport i
x <- mkBaseExpr xe
nm <- freshConstant "real sqrt" RealTypeMap
let v = asBase nm
addSideCondition "real sqrt" $ v * v .== x .|| x .< 0
addSideCondition "real sqrt" $ v .>= 0
return nm
Pi -> do
unsupportedTerm i
RealSin xe -> do
checkComputableSupport i
x <- mkBaseExpr xe
freshBoundTerm RealTypeMap $ realSin x
RealCos xe -> do
checkComputableSupport i
x <- mkBaseExpr xe
freshBoundTerm RealTypeMap $ realCos x
RealATan2 xe ye -> do
checkComputableSupport i
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm RealTypeMap $ realATan2 x y
RealSinh xe -> do
checkComputableSupport i
x <- mkBaseExpr xe
freshBoundTerm RealTypeMap $ realSinh x
RealCosh xe -> do
checkComputableSupport i
x <- mkBaseExpr xe
freshBoundTerm RealTypeMap $ realCosh x
RealExp xe -> do
checkComputableSupport i
x <- mkBaseExpr xe
freshBoundTerm RealTypeMap $ realExp x
RealLog xe -> do
checkComputableSupport i
x <- mkBaseExpr xe
freshBoundTerm RealTypeMap $ realLog x
BVUnaryTerm t -> do
let w = UnaryBV.width t
let entries = UnaryBV.unsignedRanges t
nm <- freshConstant "unary term" (BVTypeMap w)
let nm_s = asBase nm
forM_ entries $ \(pr,l,u) -> do
q <- mkBaseExpr pr
addSideCondition "unary term" $ q .== nm_s `bvULe` bvTerm w (BV.mkBV w l)
addSideCondition "unary term" $ q .== nm_s `bvULe` bvTerm w (BV.mkBV w u)
case entries of
(_, l, _):_ | l > 0 -> do
addSideCondition "unary term" $ bvTerm w (BV.mkBV w l) `bvULe` nm_s
_ ->
return ()
return nm
BVOrBits w bs ->
do bs' <- traverse mkBaseExpr (bvOrToList bs)
freshBoundTerm (BVTypeMap w) $!
case bs' of
[] -> bvTerm w (BV.zero w)
x:xs -> foldl bvOr x xs
BVConcat w xe ye -> do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm (BVTypeMap w) $ bvConcat x y
BVSelect idx n xe -> do
x <- mkBaseExpr xe
freshBoundTerm (BVTypeMap n) $ bvExtract (bvWidth xe) (natValue idx) (natValue n) x
BVUdiv w xe ye -> do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm (BVTypeMap w) $ bvUDiv x y
BVUrem w xe ye -> do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm (BVTypeMap w) $ bvURem x y
BVSdiv w xe ye -> do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm (BVTypeMap w) $ bvSDiv x y
BVSrem w xe ye -> do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm (BVTypeMap w) $ bvSRem x y
BVShl w xe ye -> do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm (BVTypeMap w) $ bvShl x y
BVLshr w xe ye -> do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm (BVTypeMap w) $ bvLshr x y
BVAshr w xe ye -> do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm (BVTypeMap w) $ bvAshr x y
BVRol w xe ye -> do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
let w' = bvTerm w (BV.width w)
y' <- asBase <$> (freshBoundTerm (BVTypeMap w) $ bvURem y w')
let lo = bvLshr x (bvSub w' y')
let hi = bvShl x y'
freshBoundTerm (BVTypeMap w) $ bvXor hi lo
BVRor w xe ye -> do
x <- mkBaseExpr xe
y <- mkBaseExpr ye
let w' = bvTerm w (BV.width w)
y' <- asBase <$> (freshBoundTerm (BVTypeMap w) $ bvURem y w')
let lo = bvLshr x y'
let hi = bvShl x (bvSub w' y')
freshBoundTerm (BVTypeMap w) $ bvXor hi lo
BVZext w' xe -> do
let w = bvWidth xe
x <- mkBaseExpr xe
let n = intValue w' - intValue w
case someNat n of
Just (Some w2) | Just LeqProof <- isPosNat w' -> do
let zeros = bvTerm w2 (BV.zero w2)
freshBoundTerm (BVTypeMap w') $ bvConcat zeros x
_ -> fail "invalid zero extension"
BVSext w' xe -> do
let w = bvWidth xe
x <- mkBaseExpr xe
let n = intValue w' - intValue w
case someNat n of
Just (Some w2) | Just LeqProof <- isPosNat w' -> do
let zeros = bvTerm w2 (BV.zero w2)
let ones = bvTerm w2 (BV.maxUnsigned w2)
let sgn = bvTestBit w (natValue w - 1) x
freshBoundTerm (BVTypeMap w') $ bvConcat (ite sgn ones zeros) x
_ -> fail "invalid sign extension"
BVFill w xe ->
do x <- mkBaseExpr xe
let zeros = bvTerm w (BV.zero w)
let ones = bvTerm w (BV.maxUnsigned w)
freshBoundTerm (BVTypeMap w) $ ite x ones zeros
BVPopcount w xe ->
do x <- mkBaseExpr xe
let zs = [ ite (bvTestBit w idx x) (bvTerm w (BV.one w)) (bvTerm w (BV.zero w))
| idx <- [ 0 .. natValue w - 1 ]
]
freshBoundTerm (BVTypeMap w) $! bvSumExpr w zs
BVCountLeadingZeros w xe ->
do x <- mkBaseExpr xe
freshBoundTerm (BVTypeMap w) $! go 0 x
where
go !idx x
| idx < natValue w = ite (bvTestBit w (natValue w - idx - 1) x) (bvTerm w (BV.mkBV w (toInteger idx))) (go (idx+1) x)
| otherwise = bvTerm w (BV.width w)
BVCountTrailingZeros w xe ->
do x <- mkBaseExpr xe
freshBoundTerm (BVTypeMap w) $! go 0 x
where
go !idx x
| idx < natValue w = ite (bvTestBit w idx x) (bvTerm w (BV.mkBV w (toInteger idx))) (go (idx+1) x)
| otherwise = bvTerm w (BV.width w)
StringLength xe -> do
case stringInfo xe of
Char8Repr -> do
checkStringSupport i
x <- mkBaseExpr xe
freshBoundTerm NatTypeMap $ stringLength @h x
si -> fail ("Unsupported symbolic string length operation " ++ show si)
StringIndexOf xe ye ke ->
case stringInfo xe of
Char8Repr -> do
checkStringSupport i
x <- mkBaseExpr xe
y <- mkBaseExpr ye
k <- mkBaseExpr ke
freshBoundTerm IntegerTypeMap $ stringIndexOf @h x y k
si -> fail ("Unsupported symbolic string index-of operation " ++ show si)
StringSubstring _ xe offe lene ->
case stringInfo xe of
Char8Repr -> do
checkStringSupport i
x <- mkBaseExpr xe
off <- mkBaseExpr offe
len <- mkBaseExpr lene
freshBoundTerm Char8TypeMap $ stringSubstring @h x off len
si -> fail ("Unsupported symbolic string substring operation " ++ show si)
StringContains xe ye ->
case stringInfo xe of
Char8Repr -> do
checkStringSupport i
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm BoolTypeMap $ stringContains @h x y
si -> fail ("Unsupported symbolic string contains operation " ++ show si)
StringIsPrefixOf xe ye ->
case stringInfo xe of
Char8Repr -> do
checkStringSupport i
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm BoolTypeMap $ stringIsPrefixOf @h x y
si -> fail ("Unsupported symbolic string is-prefix-of operation " ++ show si)
StringIsSuffixOf xe ye ->
case stringInfo xe of
Char8Repr -> do
checkStringSupport i
x <- mkBaseExpr xe
y <- mkBaseExpr ye
freshBoundTerm BoolTypeMap $ stringIsSuffixOf @h x y
si -> fail ("Unsupported symbolic string is-suffix-of operation " ++ show si)
StringAppend si xes ->
case si of
Char8Repr -> do
checkStringSupport i
let f (SSeq.StringSeqLiteral l) = return $ stringTerm @h $ fromChar8Lit l
f (SSeq.StringSeqTerm t) = mkBaseExpr t
xs <- mapM f $ SSeq.toList xes
freshBoundTerm Char8TypeMap $ stringAppend @h xs
_ -> fail ("Unsupported symbolic string append operation " ++ show si)
FloatPZero fpp ->
freshBoundTerm (FloatTypeMap fpp) $ floatPZero fpp
FloatNZero fpp ->
freshBoundTerm (FloatTypeMap fpp) $ floatNZero fpp
FloatNaN fpp ->
freshBoundTerm (FloatTypeMap fpp) $ floatNaN fpp
FloatPInf fpp ->
freshBoundTerm (FloatTypeMap fpp) $ floatPInf fpp
FloatNInf fpp ->
freshBoundTerm (FloatTypeMap fpp) $ floatNInf fpp
FloatNeg fpp x -> do
xe <- mkBaseExpr x
freshBoundTerm (FloatTypeMap fpp) $ floatNeg xe
FloatAbs fpp x -> do
xe <- mkBaseExpr x
freshBoundTerm (FloatTypeMap fpp) $ floatAbs xe
FloatSqrt fpp r x -> do
xe <- mkBaseExpr x
freshBoundTerm (FloatTypeMap fpp) $ floatSqrt r xe
FloatAdd fpp r x y -> do
xe <- mkBaseExpr x
ye <- mkBaseExpr y
freshBoundTerm (FloatTypeMap fpp) $ floatAdd r xe ye
FloatSub fpp r x y -> do
xe <- mkBaseExpr x
ye <- mkBaseExpr y
freshBoundTerm (FloatTypeMap fpp) $ floatSub r xe ye
FloatMul fpp r x y -> do
xe <- mkBaseExpr x
ye <- mkBaseExpr y
freshBoundTerm (FloatTypeMap fpp) $ floatMul r xe ye
FloatDiv fpp r x y -> do
xe <- mkBaseExpr x
ye <- mkBaseExpr y
freshBoundTerm (FloatTypeMap fpp) $ floatDiv r xe ye
FloatRem fpp x y -> do
xe <- mkBaseExpr x
ye <- mkBaseExpr y
freshBoundTerm (FloatTypeMap fpp) $ floatRem xe ye
FloatMin fpp x y -> do
xe <- mkBaseExpr x
ye <- mkBaseExpr y
freshBoundTerm (FloatTypeMap fpp) $ floatMin xe ye
FloatMax fpp x y -> do
xe <- mkBaseExpr x
ye <- mkBaseExpr y
freshBoundTerm (FloatTypeMap fpp) $ floatMax xe ye
FloatFMA fpp r x y z -> do
xe <- mkBaseExpr x
ye <- mkBaseExpr y
ze <- mkBaseExpr z
freshBoundTerm (FloatTypeMap fpp) $ floatFMA r xe ye ze
FloatFpEq x y -> do
xe <- mkBaseExpr x
ye <- mkBaseExpr y
freshBoundTerm BoolTypeMap $ floatFpEq xe ye
FloatFpNe x y -> do
xe <- mkBaseExpr x
ye <- mkBaseExpr y
freshBoundTerm BoolTypeMap $
notExpr (floatEq xe ye)
.&& notExpr (floatIsNaN xe)
.&& notExpr (floatIsNaN ye)
FloatLe x y -> do
xe <- mkBaseExpr x
ye <- mkBaseExpr y
freshBoundTerm BoolTypeMap $ floatLe xe ye
FloatLt x y -> do
xe <- mkBaseExpr x
ye <- mkBaseExpr y
freshBoundTerm BoolTypeMap $ floatLt xe ye
FloatIsNaN x -> do
xe <- mkBaseExpr x
freshBoundTerm BoolTypeMap $ floatIsNaN xe
FloatIsInf x -> do
xe <- mkBaseExpr x
freshBoundTerm BoolTypeMap $ floatIsInf xe
FloatIsZero x -> do
xe <- mkBaseExpr x
freshBoundTerm BoolTypeMap $ floatIsZero xe
FloatIsPos x -> do
xe <- mkBaseExpr x
freshBoundTerm BoolTypeMap $ floatIsPos xe
FloatIsNeg x -> do
xe <- mkBaseExpr x
freshBoundTerm BoolTypeMap $ floatIsNeg xe
FloatIsSubnorm x -> do
xe <- mkBaseExpr x
freshBoundTerm BoolTypeMap $ floatIsSubnorm xe
FloatIsNorm x -> do
xe <- mkBaseExpr x
freshBoundTerm BoolTypeMap $ floatIsNorm xe
FloatCast fpp r x -> do
xe <- mkBaseExpr x
freshBoundTerm (FloatTypeMap fpp) $
floatCast fpp r xe
FloatRound fpp r x -> do
xe <- mkBaseExpr x
freshBoundTerm (FloatTypeMap fpp)$ floatRound r xe
FloatToBinary fpp@(FloatingPointPrecisionRepr eb sb) x -> do
xe <- mkBaseExpr x
val <- asBase <$> (freshConstant "float_binary" $ BVTypeMap $ addNat eb sb)
addSideCondition "float_binary" $
floatFromBinary fpp val .== xe
let qnan = bvTerm (addNat eb sb) $
BV.mkBV (addNat eb sb) $
Bits.shiftL
(2 ^ (natValue eb + 1) - 1)
(fromIntegral (natValue sb - 2))
freshBoundTerm (BVTypeMap $ addNat eb sb) $ ite (floatIsNaN xe) qnan val
FloatFromBinary fpp x -> do
xe <- mkBaseExpr x
freshBoundTerm (FloatTypeMap fpp) $
floatFromBinary fpp xe
BVToFloat fpp r x -> do
xe <- mkBaseExpr x
freshBoundTerm (FloatTypeMap fpp) $
bvToFloat fpp r xe
SBVToFloat fpp r x -> do
xe <- mkBaseExpr x
freshBoundTerm (FloatTypeMap fpp) $
sbvToFloat fpp r xe
RealToFloat fpp r x -> do
xe <- mkBaseExpr x
freshBoundTerm (FloatTypeMap fpp) $
realToFloat fpp r xe
FloatToBV w r x -> do
xe <- mkBaseExpr x
freshBoundTerm (BVTypeMap w) $ floatToBV (natValue w) r xe
FloatToSBV w r x -> do
xe <- mkBaseExpr x
freshBoundTerm (BVTypeMap w) $ floatToSBV (natValue w) r xe
FloatToReal x -> do
xe <- mkBaseExpr x
freshBoundTerm RealTypeMap $ floatToReal xe
ArrayMap _ _ elts def -> do
base_array <- mkExpr def
elt_exprs <- (traverse._2) mkBaseExpr (AUM.toList elts)
let array_type = smtExprType base_array
case array_type of
PrimArrayTypeMap{} -> do
let set_at_index :: Term h
-> (Ctx.Assignment IndexLit ctx, Term h)
-> Term h
set_at_index ma (idx, elt) =
arrayUpdate @h ma (mkIndexLitTerms idx) elt
freshBoundTerm array_type $
foldl set_at_index (asBase base_array) elt_exprs
FnArrayTypeMap idx_types resType -> do
case smtFnUpdate of
Just updateFn -> do
let set_at_index :: Term h
-> (Ctx.Assignment IndexLit ctx, Term h)
-> Term h
set_at_index ma (idx, elt) =
updateFn ma (toListFC mkIndexLitTerm idx) elt
freshBoundTerm array_type $
foldl set_at_index (asBase base_array) elt_exprs
Nothing -> do