{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.SBV.Core.Symbolic
( NodeId(..)
, SW(..), swKind, trueSW, falseSW
, Op(..), PBOp(..), OvOp(..), FPOp(..), StrOp(..), RegExp(..)
, Quantifier(..), needsExistentials
, RoundingMode(..)
, SBVType(..), svUninterpreted, newUninterpreted, addAxiom
, SVal(..)
, svMkSymVar, sWordN, sWordN_, sIntN, sIntN_
, ArrayContext(..), ArrayInfo
, svToSW, svToSymSW, forceSWArg
, SBVExpr(..), newExpr, isCodeGenMode, isSafetyCheckingIStage, isRunIStage, isSetupIStage
, Cached, cache, uncache, modifyState, modifyIncState
, ArrayIndex(..), FArrayIndex(..), uncacheAI, uncacheFAI
, NamedSymVar
, getSValPathCondition, extendSValPathCondition
, getTableIndex
, SBVPgm(..), Symbolic, runSymbolic, State(..), withNewIncState, IncState(..), incrementInternalCounter
, inSMTMode, SBVRunMode(..), IStage(..), Result(..)
, registerKind, registerLabel, recordObservable
, addAssertion, addNewSMTOption, imposeConstraint, internalConstraint, internalVariable
, SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension
, SolverCapabilities(..)
, extractSymbolicSimulationState
, OptimizeStyle(..), Objective(..), Penalty(..), objectiveName, addSValOptGoal
, Query(..), QueryState(..), QueryContext(..)
, SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), SMTEngine
, outputSVal
) where
import Control.Arrow (first, second, (***))
import Control.DeepSeq (NFData(..))
import Control.Monad (when, unless)
import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT)
import Control.Monad.State.Lazy (MonadState, StateT(..))
import Control.Monad.Trans (MonadIO, liftIO)
import Data.Char (isAlpha, isAlphaNum, toLower)
import Data.IORef (IORef, newIORef, readIORef)
import Data.List (intercalate, sortBy)
import Data.Maybe (isJust, fromJust, fromMaybe, listToMaybe)
import Data.String (IsString(fromString))
import Data.Time (getCurrentTime, UTCTime)
import GHC.Stack
import qualified Data.IORef as R (modifyIORef')
import qualified Data.Generics as G (Data(..))
import qualified Data.IntMap.Strict as IMap (IntMap, empty, toAscList, lookup, insertWith)
import qualified Data.Map.Strict as Map (Map, empty, toList, lookup, insert, size)
import qualified Data.Set as Set (Set, empty, toList, insert, member)
import qualified Data.Foldable as F (toList)
import qualified Data.Sequence as S (Seq, empty, (|>))
import System.Mem.StableName
import Data.SBV.Core.Kind
import Data.SBV.Core.Concrete
import Data.SBV.SMT.SMTLibNames
import Data.SBV.Utils.TDiff (Timing)
import Data.SBV.Utils.Lib (stringToQFS)
import Data.SBV.Control.Types
newtype NodeId = NodeId Int deriving (Eq, Ord)
data SW = SW !Kind !NodeId deriving (Eq, Ord)
instance HasKind SW where
kindOf (SW k _) = k
instance Show SW where
show (SW _ (NodeId n))
| n < 0 = "s_" ++ show (abs n)
| True = 's' : show n
swKind :: SW -> Kind
swKind (SW k _) = k
forceSWArg :: SW -> IO ()
forceSWArg (SW k n) = k `seq` n `seq` return ()
falseSW :: SW
falseSW = SW KBool $ NodeId (-2)
trueSW :: SW
trueSW = SW KBool $ NodeId (-1)
data Op = Plus
| Times
| Minus
| UNeg
| Abs
| Quot
| Rem
| Equal
| NotEqual
| LessThan
| GreaterThan
| LessEq
| GreaterEq
| Ite
| And
| Or
| XOr
| Not
| Shl
| Shr
| Rol Int
| Ror Int
| Extract Int Int
| Join
| LkUp (Int, Kind, Kind, Int) !SW !SW
| ArrEq ArrayIndex ArrayIndex
| ArrRead ArrayIndex
| KindCast Kind Kind
| Uninterpreted String
| Label String
| IEEEFP FPOp
| PseudoBoolean PBOp
| OverflowOp OvOp
| StrOp StrOp
deriving (Eq, Ord)
data FPOp = FP_Cast Kind Kind SW
| FP_Reinterpret Kind Kind
| FP_Abs
| FP_Neg
| FP_Add
| FP_Sub
| FP_Mul
| FP_Div
| FP_FMA
| FP_Sqrt
| FP_Rem
| FP_RoundToIntegral
| FP_Min
| FP_Max
| FP_ObjEqual
| FP_IsNormal
| FP_IsSubnormal
| FP_IsZero
| FP_IsInfinite
| FP_IsNaN
| FP_IsNegative
| FP_IsPositive
deriving (Eq, Ord)
instance Show FPOp where
show (FP_Cast f t r) = "(FP_Cast: " ++ show f ++ " -> " ++ show t ++ ", using RM [" ++ show r ++ "])"
show (FP_Reinterpret f t) = case (f, t) of
(KBounded False 32, KFloat) -> "(_ to_fp 8 24)"
(KBounded False 64, KDouble) -> "(_ to_fp 11 53)"
_ -> error $ "SBV.FP_Reinterpret: Unexpected conversion: " ++ show f ++ " to " ++ show t
show FP_Abs = "fp.abs"
show FP_Neg = "fp.neg"
show FP_Add = "fp.add"
show FP_Sub = "fp.sub"
show FP_Mul = "fp.mul"
show FP_Div = "fp.div"
show FP_FMA = "fp.fma"
show FP_Sqrt = "fp.sqrt"
show FP_Rem = "fp.rem"
show FP_RoundToIntegral = "fp.roundToIntegral"
show FP_Min = "fp.min"
show FP_Max = "fp.max"
show FP_ObjEqual = "="
show FP_IsNormal = "fp.isNormal"
show FP_IsSubnormal = "fp.isSubnormal"
show FP_IsZero = "fp.isZero"
show FP_IsInfinite = "fp.isInfinite"
show FP_IsNaN = "fp.isNaN"
show FP_IsNegative = "fp.isNegative"
show FP_IsPositive = "fp.isPositive"
data PBOp = PB_AtMost Int
| PB_AtLeast Int
| PB_Exactly Int
| PB_Le [Int] Int
| PB_Ge [Int] Int
| PB_Eq [Int] Int
deriving (Eq, Ord, Show)
data OvOp = Overflow_SMul_OVFL
| Overflow_SMul_UDFL
| Overflow_UMul_OVFL
deriving (Eq, Ord)
instance Show OvOp where
show Overflow_SMul_OVFL = "bvsmul_noovfl"
show Overflow_SMul_UDFL = "bvsmul_noudfl"
show Overflow_UMul_OVFL = "bvumul_noovfl"
data StrOp = StrConcat
| StrLen
| StrUnit
| StrSubstr
| StrIndexOf
| StrContains
| StrPrefixOf
| StrSuffixOf
| StrReplace
| StrStrToNat
| StrNatToStr
| StrInRe RegExp
deriving (Eq, Ord)
data RegExp = Literal String
| All
| None
| Range Char Char
| Conc [RegExp]
| KStar RegExp
| KPlus RegExp
| Opt RegExp
| Loop Int Int RegExp
| Union [RegExp]
| Inter RegExp RegExp
deriving (Eq, Ord)
instance IsString RegExp where
fromString = Literal
instance Num RegExp where
Conc xs * y = Conc (xs ++ [y])
x * Conc ys = Conc (x : ys)
x * y = Conc [x, y]
Union xs + y = Union (xs ++ [y])
x + Union ys = Union (x : ys)
x + y = Union [x, y]
abs = error "Num.RegExp: no abs method"
signum = error "Num.RegExp: no signum method"
fromInteger x
| x == 0 = None
| x == 1 = Literal ""
| True = error $ "Num.RegExp: Only 0 and 1 makes sense as a reg-exp, no meaning for: " ++ show x
negate = error "Num.RegExp: no negate method"
instance Show RegExp where
show (Literal s) = "(str.to.re \"" ++ stringToQFS s ++ "\")"
show All = "re.allchar"
show None = "re.nostr"
show (Range ch1 ch2) = "(re.range \"" ++ stringToQFS [ch1] ++ "\" \"" ++ stringToQFS [ch2] ++ "\")"
show (Conc []) = show (1 :: Integer)
show (Conc [x]) = show x
show (Conc xs) = "(re.++ " ++ unwords (map show xs) ++ ")"
show (KStar r) = "(re.* " ++ show r ++ ")"
show (KPlus r) = "(re.+ " ++ show r ++ ")"
show (Opt r) = "(re.opt " ++ show r ++ ")"
show (Loop lo hi r)
| lo >= 0, hi >= lo = "((_ re.loop " ++ show lo ++ " " ++ show hi ++ ") " ++ show r ++ ")"
| True = error $ "Invalid regular-expression Loop with arguments: " ++ show (lo, hi)
show (Inter r1 r2) = "(re.inter " ++ show r1 ++ " " ++ show r2 ++ ")"
show (Union []) = "re.nostr"
show (Union [x]) = show x
show (Union xs) = "(re.union " ++ unwords (map show xs) ++ ")"
instance Show StrOp where
show StrConcat = "str.++"
show StrLen = "str.len"
show StrUnit = "seq.unit"
show StrSubstr = "str.substr"
show StrIndexOf = "str.indexof"
show StrContains = "str.contains"
show StrPrefixOf = "str.prefixof"
show StrSuffixOf = "str.suffixof"
show StrReplace = "str.replace"
show StrStrToNat = "str.to.int"
show StrNatToStr = "int.to.str"
show (StrInRe s) = "str.in.re " ++ show s
instance Show Op where
show Shl = "<<"
show Shr = ">>"
show (Rol i) = "<<<" ++ show i
show (Ror i) = ">>>" ++ show i
show (Extract i j) = "choose [" ++ show i ++ ":" ++ show j ++ "]"
show (LkUp (ti, at, rt, l) i e)
= "lookup(" ++ tinfo ++ ", " ++ show i ++ ", " ++ show e ++ ")"
where tinfo = "table" ++ show ti ++ "(" ++ show at ++ " -> " ++ show rt ++ ", " ++ show l ++ ")"
show (ArrEq i j) = "array_" ++ show i ++ " == array_" ++ show j
show (ArrRead i) = "select array_" ++ show i
show (KindCast fr to) = "cast_" ++ show fr ++ "_" ++ show to
show (Uninterpreted i) = "[uninterpreted] " ++ i
show (Label s) = "[label] " ++ s
show (IEEEFP w) = show w
show (PseudoBoolean p) = show p
show (OverflowOp o) = show o
show (StrOp s) = show s
show op
| Just s <- op `lookup` syms = s
| True = error "impossible happened; can't find op!"
where syms = [ (Plus, "+"), (Times, "*"), (Minus, "-"), (UNeg, "-"), (Abs, "abs")
, (Quot, "quot")
, (Rem, "rem")
, (Equal, "=="), (NotEqual, "/=")
, (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=")
, (Ite, "if_then_else")
, (And, "&"), (Or, "|"), (XOr, "^"), (Not, "~")
, (Join, "#")
]
data Quantifier = ALL | EX deriving Eq
needsExistentials :: [Quantifier] -> Bool
needsExistentials = (EX `elem`)
newtype SBVType = SBVType [Kind]
deriving (Eq, Ord)
instance Show SBVType where
show (SBVType []) = error "SBV: internal error, empty SBVType"
show (SBVType xs) = intercalate " -> " $ map show xs
data SBVExpr = SBVApp !Op ![SW]
deriving (Eq, Ord)
reorder :: SBVExpr -> SBVExpr
reorder s = case s of
SBVApp op [a, b] | isCommutative op && a > b -> SBVApp op [b, a]
_ -> s
where isCommutative :: Op -> Bool
isCommutative o = o `elem` [Plus, Times, Equal, NotEqual, And, Or, XOr]
instance Show SBVExpr where
show (SBVApp Ite [t, a, b]) = unwords ["if", show t, "then", show a, "else", show b]
show (SBVApp Shl [a, i]) = unwords [show a, "<<", show i]
show (SBVApp Shr [a, i]) = unwords [show a, ">>", show i]
show (SBVApp (Rol i) [a]) = unwords [show a, "<<<", show i]
show (SBVApp (Ror i) [a]) = unwords [show a, ">>>", show i]
show (SBVApp (PseudoBoolean pb) args) = unwords (show pb : map show args)
show (SBVApp (OverflowOp op) args) = unwords (show op : map show args)
show (SBVApp op [a, b]) = unwords [show a, show op, show b]
show (SBVApp op args) = unwords (show op : map show args)
newtype SBVPgm = SBVPgm {pgmAssignments :: S.Seq (SW, SBVExpr)}
type NamedSymVar = (SW, String)
data OptimizeStyle = Lexicographic
| Independent
| Pareto (Maybe Int)
deriving (Eq, Show)
data Penalty = DefaultPenalty
| Penalty Rational (Maybe String)
deriving Show
data Objective a = Minimize String a
| Maximize String a
| AssertWithPenalty String a Penalty
deriving (Show, Functor)
objectiveName :: Objective a -> String
objectiveName (Minimize s _) = s
objectiveName (Maximize s _) = s
objectiveName (AssertWithPenalty s _ _) = s
data QueryState = QueryState { queryAsk :: Maybe Int -> String -> IO String
, querySend :: Maybe Int -> String -> IO ()
, queryRetrieveResponse :: Maybe Int -> IO String
, queryConfig :: SMTConfig
, queryTerminate :: IO ()
, queryTimeOutValue :: Maybe Int
, queryAssertionStackDepth :: Int
, queryTblArrPreserveIndex :: Maybe (Int, Int)
}
newtype Query a = Query (StateT State IO a)
deriving (Applicative, Functor, Monad, MonadIO, MonadState State)
instance NFData OptimizeStyle where
rnf x = x `seq` ()
instance NFData Penalty where
rnf DefaultPenalty = ()
rnf (Penalty p mbs) = rnf p `seq` rnf mbs `seq` ()
instance NFData a => NFData (Objective a) where
rnf (Minimize s a) = rnf s `seq` rnf a `seq` ()
rnf (Maximize s a) = rnf s `seq` rnf a `seq` ()
rnf (AssertWithPenalty s a p) = rnf s `seq` rnf a `seq` rnf p `seq` ()
data Result = Result { reskinds :: Set.Set Kind
, resTraces :: [(String, CW)]
, resObservables :: [(String, SW)]
, resUISegs :: [(String, [String])]
, resInputs :: ([(Quantifier, NamedSymVar)], [NamedSymVar])
, resConsts :: [(SW, CW)]
, resTables :: [((Int, Kind, Kind), [SW])]
, resArrays :: [(Int, ArrayInfo)]
, resUIConsts :: [(String, SBVType)]
, resAxioms :: [(String, [String])]
, resAsgns :: SBVPgm
, resConstraints :: [(Bool, [(String, String)], SW)]
, resAssertions :: [(String, Maybe CallStack, SW)]
, resOutputs :: [SW]
}
instance Show Result where
show Result{resConsts=cs, resOutputs=[r]}
| Just c <- r `lookup` cs
= show c
show (Result kinds _ _ cgs is cs ts as uis axs xs cstrs asserts os) = intercalate "\n" $
(if null usorts then [] else "SORTS" : map (" " ++) usorts)
++ ["INPUTS"]
++ map shn (fst is)
++ (if null (snd is) then [] else "TRACKER VARS" : map (shn . (EX,)) (snd is))
++ ["CONSTANTS"]
++ map shc cs
++ ["TABLES"]
++ map sht ts
++ ["ARRAYS"]
++ map sha as
++ ["UNINTERPRETED CONSTANTS"]
++ map shui uis
++ ["USER GIVEN CODE SEGMENTS"]
++ concatMap shcg cgs
++ ["AXIOMS"]
++ map shax axs
++ ["DEFINE"]
++ map (\(s, e) -> " " ++ shs s ++ " = " ++ show e) (F.toList (pgmAssignments xs))
++ ["CONSTRAINTS"]
++ map ((" " ++) . shCstr) cstrs
++ ["ASSERTIONS"]
++ map ((" "++) . shAssert) asserts
++ ["OUTPUTS"]
++ sh2 os
where sh2 :: Show a => [a] -> [String]
sh2 = map ((" "++) . show)
usorts = [sh s t | KUserSort s t <- Set.toList kinds]
where sh s (Left _) = s
sh s (Right es) = s ++ " (" ++ intercalate ", " es ++ ")"
shs sw = show sw ++ " :: " ++ show (swKind sw)
sht ((i, at, rt), es) = " Table " ++ show i ++ " : " ++ show at ++ "->" ++ show rt ++ " = " ++ show es
shc (sw, cw) = " " ++ show sw ++ " = " ++ show cw
shcg (s, ss) = ("Variable: " ++ s) : map (" " ++) ss
shn (q, (sw, nm)) = " " ++ ni ++ " :: " ++ show (swKind sw) ++ ex ++ alias
where ni = show sw
ex | q == ALL = ""
| True = ", existential"
alias | ni == nm = ""
| True = ", aliasing " ++ show nm
sha (i, (nm, (ai, bi), ctx)) = " " ++ ni ++ " :: " ++ show ai ++ " -> " ++ show bi ++ alias
++ "\n Context: " ++ show ctx
where ni = "array_" ++ show i
alias | ni == nm = ""
| True = ", aliasing " ++ show nm
shui (nm, t) = " [uninterpreted] " ++ nm ++ " :: " ++ show t
shax (nm, ss) = " -- user defined axiom: " ++ nm ++ "\n " ++ intercalate "\n " ss
shCstr (isSoft, [], c) = soft isSoft ++ show c
shCstr (isSoft, [(":named", nm)], c) = soft isSoft ++ nm ++ ": " ++ show c
shCstr (isSoft, attrs, c) = soft isSoft ++ show c ++ " (attributes: " ++ show attrs ++ ")"
soft True = "[SOFT] "
soft False = ""
shAssert (nm, stk, p) = " -- assertion: " ++ nm ++ " " ++ maybe "[No location]"
#if MIN_VERSION_base(4,9,0)
prettyCallStack
#else
showCallStack
#endif
stk ++ ": " ++ show p
data ArrayContext = ArrayFree (Maybe SW)
| ArrayMutate ArrayIndex SW SW
| ArrayMerge SW ArrayIndex ArrayIndex
instance Show ArrayContext where
show (ArrayFree Nothing) = " initialized with random elements"
show (ArrayFree (Just sw)) = " initialized with " ++ show sw
show (ArrayMutate i a b) = " cloned from array_" ++ show i ++ " with " ++ show a ++ " :: " ++ show (swKind a) ++ " |-> " ++ show b ++ " :: " ++ show (swKind b)
show (ArrayMerge s i j) = " merged arrays " ++ show i ++ " and " ++ show j ++ " on condition " ++ show s
type ExprMap = Map.Map SBVExpr SW
type CnstMap = Map.Map CW SW
type KindSet = Set.Set Kind
type TableMap = Map.Map (Kind, Kind, [SW]) Int
type ArrayInfo = (String, (Kind, Kind), ArrayContext)
type ArrayMap = IMap.IntMap ArrayInfo
type FArrayMap = IMap.IntMap (SVal -> SVal, IORef (IMap.IntMap SW))
type UIMap = Map.Map String SBVType
type CgMap = Map.Map String [String]
type Cache a = IMap.IntMap [(StableName (State -> IO a), a)]
data IStage = ISetup
| ISafe
| IRun
isSafetyCheckingIStage :: IStage -> Bool
isSafetyCheckingIStage s = case s of
ISetup -> False
ISafe -> True
IRun -> False
isSetupIStage :: IStage -> Bool
isSetupIStage s = case s of
ISetup -> True
ISafe -> False
IRun -> True
isRunIStage :: IStage -> Bool
isRunIStage s = case s of
ISetup -> False
ISafe -> False
IRun -> True
data SBVRunMode = SMTMode IStage Bool SMTConfig
| CodeGen
| Concrete
instance Show SBVRunMode where
show (SMTMode ISetup True _) = "Satisfiability setup"
show (SMTMode ISafe True _) = "Safety setup"
show (SMTMode IRun True _) = "Satisfiability"
show (SMTMode ISetup False _) = "Proof setup"
show (SMTMode ISafe False _) = error "ISafe-False is not an expected/supported combination for SBVRunMode!"
show (SMTMode IRun False _) = "Proof"
show CodeGen = "Code generation"
show Concrete = "Concrete evaluation"
isCodeGenMode :: State -> IO Bool
isCodeGenMode State{runMode} = do rm <- readIORef runMode
return $ case rm of
Concrete{} -> False
SMTMode{} -> False
CodeGen -> True
data IncState = IncState { rNewInps :: IORef [NamedSymVar]
, rNewKinds :: IORef KindSet
, rNewConsts :: IORef CnstMap
, rNewArrs :: IORef ArrayMap
, rNewTbls :: IORef TableMap
, rNewUIs :: IORef UIMap
, rNewAsgns :: IORef SBVPgm
}
newIncState :: IO IncState
newIncState = do
is <- newIORef []
ks <- newIORef Set.empty
nc <- newIORef Map.empty
am <- newIORef IMap.empty
tm <- newIORef Map.empty
ui <- newIORef Map.empty
pgm <- newIORef (SBVPgm S.empty)
return IncState { rNewInps = is
, rNewKinds = ks
, rNewConsts = nc
, rNewArrs = am
, rNewTbls = tm
, rNewUIs = ui
, rNewAsgns = pgm
}
withNewIncState :: State -> (State -> IO a) -> IO (IncState, a)
withNewIncState st cont = do
is <- newIncState
R.modifyIORef' (rIncState st) (const is)
r <- cont st
finalIncState <- readIORef (rIncState st)
return (finalIncState, r)
data State = State { pathCond :: SVal
, startTime :: UTCTime
, runMode :: IORef SBVRunMode
, rIncState :: IORef IncState
, rCInfo :: IORef [(String, CW)]
, rObservables :: IORef [(String, SW)]
, rctr :: IORef Int
, rUsedKinds :: IORef KindSet
, rUsedLbls :: IORef (Set.Set String)
, rinps :: IORef ([(Quantifier, NamedSymVar)], [NamedSymVar])
, rConstraints :: IORef [(Bool, [(String, String)], SW)]
, routs :: IORef [SW]
, rtblMap :: IORef TableMap
, spgm :: IORef SBVPgm
, rconstMap :: IORef CnstMap
, rexprMap :: IORef ExprMap
, rArrayMap :: IORef ArrayMap
, rFArrayMap :: IORef FArrayMap
, rUIMap :: IORef UIMap
, rCgMap :: IORef CgMap
, raxioms :: IORef [(String, [String])]
, rSMTOptions :: IORef [SMTOption]
, rOptGoals :: IORef [Objective (SW, SW)]
, rAsserts :: IORef [(String, Maybe CallStack, SW)]
, rSWCache :: IORef (Cache SW)
, rAICache :: IORef (Cache ArrayIndex)
, rFAICache :: IORef (Cache FArrayIndex)
, queryState :: IORef (Maybe QueryState)
}
instance NFData State where
rnf State{} = ()
getSValPathCondition :: State -> SVal
getSValPathCondition = pathCond
extendSValPathCondition :: State -> (SVal -> SVal) -> State
extendSValPathCondition st f = st{pathCond = f (pathCond st)}
inSMTMode :: State -> IO Bool
inSMTMode State{runMode} = do rm <- readIORef runMode
return $ case rm of
CodeGen -> False
Concrete{} -> False
SMTMode{} -> True
data SVal = SVal !Kind !(Either CW (Cached SW))
instance HasKind SVal where
kindOf (SVal k _) = k
instance Show SVal where
show (SVal KBool (Left c)) = showCW False c
show (SVal k (Left c)) = showCW False c ++ " :: " ++ show k
show (SVal k (Right _)) = "<symbolic> :: " ++ show k
instance Eq SVal where
a == b = error $ "Comparing symbolic bit-vectors; Use (.==) instead. Received: " ++ show (a, b)
a /= b = error $ "Comparing symbolic bit-vectors; Use (./=) instead. Received: " ++ show (a, b)
noInteractive :: [String] -> a
noInteractive ss = error $ unlines $ ""
: "*** Data.SBV: Unsupported interactive/query mode feature."
: map ("*** " ++) ss
++ ["*** Data.SBV: Please report this as a feature request!"]
modifyState :: State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState st@State{runMode} field update interactiveUpdate = do
R.modifyIORef' (field st) update
rm <- readIORef runMode
case rm of
SMTMode IRun _ _ -> interactiveUpdate
_ -> return ()
modifyIncState :: State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State{rIncState} field update = do
incState <- readIORef rIncState
R.modifyIORef' (field incState) update
recordObservable :: State -> String -> SW -> IO ()
recordObservable st nm sw = modifyState st rObservables ((nm, sw):) (return ())
incrementInternalCounter :: State -> IO Int
incrementInternalCounter st = do ctr <- readIORef (rctr st)
modifyState st rctr (+1) (return ())
return ctr
svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal
svUninterpreted k nm code args = SVal k $ Right $ cache result
where result st = do let ty = SBVType (map kindOf args ++ [k])
newUninterpreted st nm ty code
sws <- mapM (svToSW st) args
mapM_ forceSWArg sws
newExpr st k $ SBVApp (Uninterpreted nm) sws
newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
newUninterpreted st nm t mbCode
| null nm || not enclosed && (not (isAlpha (head nm)) || not (all validChar (tail nm)))
= error $ "Bad uninterpreted constant name: " ++ show nm ++ ". Must be a valid identifier."
| True = do uiMap <- readIORef (rUIMap st)
case nm `Map.lookup` uiMap of
Just t' -> checkType t' (return ())
Nothing -> do modifyState st rUIMap (Map.insert nm t)
$ modifyIncState st rNewUIs (\newUIs -> case nm `Map.lookup` newUIs of
Just t' -> checkType t' newUIs
Nothing -> Map.insert nm t newUIs)
when (isJust mbCode) $ modifyState st rCgMap (Map.insert nm (fromJust mbCode)) (return ())
where checkType t' cont
| t /= t' = error $ "Uninterpreted constant " ++ show nm ++ " used at incompatible types\n"
++ " Current type : " ++ show t ++ "\n"
++ " Previously used at: " ++ show t'
| True = cont
validChar x = isAlphaNum x || x `elem` "_"
enclosed = head nm == '|' && last nm == '|' && length nm > 2 && not (any (`elem` "|\\") (tail (init nm)))
addAssertion :: State -> Maybe CallStack -> String -> SW -> IO ()
addAssertion st cs msg cond = modifyState st rAsserts ((msg, cs, cond):)
$ noInteractive [ "Named assertions (sAssert):"
, " Tag: " ++ msg
, " Loc: " ++ maybe "Unknown" show cs
]
internalVariable :: State -> Kind -> IO SW
internalVariable st k = do (sw, nm) <- newSW st k
rm <- readIORef (runMode st)
let q = case rm of
SMTMode _ True _ -> EX
SMTMode _ False _ -> ALL
CodeGen -> ALL
Concrete{} -> ALL
modifyState st rinps (first ((:) (q, (sw, "__internal_sbv_" ++ nm))))
$ noInteractive [ "Internal variable creation:"
, " Named: " ++ nm
]
return sw
{-# INLINE internalVariable #-}
newSW :: State -> Kind -> IO (SW, String)
newSW st k = do ctr <- incrementInternalCounter st
let sw = SW k (NodeId ctr)
registerKind st k
return (sw, 's' : show ctr)
{-# INLINE newSW #-}
registerKind :: State -> Kind -> IO ()
registerKind st k
| KUserSort sortName _ <- k, map toLower sortName `elem` smtLibReservedNames
= error $ "SBV: " ++ show sortName ++ " is a reserved sort; please use a different name."
| True
= do ks <- readIORef (rUsedKinds st)
unless (k `Set.member` ks) $ modifyState st rUsedKinds (Set.insert k)
$ modifyIncState st rNewKinds (Set.insert k)
registerLabel :: String -> State -> String -> IO ()
registerLabel whence st nm
| map toLower nm `elem` smtLibReservedNames
= err "is a reserved string; please use a different name."
| '|' `elem` nm
= err "contains the character `|', which is not allowed!"
| '\\' `elem` nm
= err "contains the character `\', which is not allowed!"
| True
= do old <- readIORef $ rUsedLbls st
if nm `Set.member` old
then err "is used multiple times. Please do not use duplicate names!"
else modifyState st rUsedLbls (Set.insert nm) (return ())
where err w = error $ "SBV (" ++ whence ++ "): " ++ show nm ++ " " ++ w
newConst :: State -> CW -> IO SW
newConst st c = do
constMap <- readIORef (rconstMap st)
case c `Map.lookup` constMap of
Just sw -> return sw
Nothing -> do let k = kindOf c
(sw, _) <- newSW st k
let ins = Map.insert c sw
modifyState st rconstMap ins $ modifyIncState st rNewConsts ins
return sw
{-# INLINE newConst #-}
getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int
getTableIndex st at rt elts = do
let key = (at, rt, elts)
tblMap <- readIORef (rtblMap st)
case key `Map.lookup` tblMap of
Just i -> return i
_ -> do let i = Map.size tblMap
upd = Map.insert key i
modifyState st rtblMap upd $ modifyIncState st rNewTbls upd
return i
newExpr :: State -> Kind -> SBVExpr -> IO SW
newExpr st k app = do
let e = reorder app
exprMap <- readIORef (rexprMap st)
case e `Map.lookup` exprMap of
Just sw -> return sw
Nothing -> do (sw, _) <- newSW st k
let append (SBVPgm xs) = SBVPgm (xs S.|> (sw, e))
modifyState st spgm append $ modifyIncState st rNewAsgns append
modifyState st rexprMap (Map.insert e sw) (return ())
return sw
{-# INLINE newExpr #-}
svToSW :: State -> SVal -> IO SW
svToSW st (SVal _ (Left c)) = newConst st c
svToSW st (SVal _ (Right f)) = uncache f st
svToSymSW :: SVal -> Symbolic SW
svToSymSW sbv = do st <- ask
liftIO $ svToSW st sbv
newtype Symbolic a = Symbolic (ReaderT State IO a)
deriving (Applicative, Functor, Monad, MonadIO, MonadReader State)
svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar = svMkSymVarGen False
svMkTrackerVar :: Kind -> String -> State -> IO SVal
svMkTrackerVar k nm = svMkSymVarGen True (Just EX) k (Just nm)
sWordN :: Int -> String -> Symbolic SVal
sWordN w nm = ask >>= liftIO . svMkSymVar Nothing (KBounded False w) (Just nm)
sWordN_ :: Int -> Symbolic SVal
sWordN_ w = ask >>= liftIO . svMkSymVar Nothing (KBounded False w) Nothing
sIntN :: Int -> String -> Symbolic SVal
sIntN w nm = ask >>= liftIO . svMkSymVar Nothing (KBounded True w) (Just nm)
sIntN_ :: Int -> Symbolic SVal
sIntN_ w = ask >>= liftIO . svMkSymVar Nothing (KBounded True w) Nothing
svMkSymVarGen :: Bool -> Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVarGen isTracker mbQ k mbNm st = do
rm <- readIORef (runMode st)
let varInfo = case mbNm of
Nothing -> ", of type " ++ show k
Just nm -> ", while defining " ++ nm ++ " :: " ++ show k
disallow what = error $ "Data.SBV: Unsupported: " ++ what ++ varInfo ++ " in mode: " ++ show rm
noUI cont
| isUninterpreted k = disallow "Uninterpreted sorts"
| True = cont
mkS q = do (sw, internalName) <- newSW st k
let nm = fromMaybe internalName mbNm
introduceUserName st isTracker nm k q sw
mkC = do cw <- randomCW k
do registerKind st k
modifyState st rCInfo ((fromMaybe "_" mbNm, cw):) (return ())
return $ SVal k (Left cw)
case (mbQ, rm) of
(Just q, SMTMode{} ) -> mkS q
(Nothing, SMTMode _ isSAT _) -> mkS (if isSAT then EX else ALL)
(Just EX, CodeGen{}) -> disallow "Existentially quantified variables"
(_ , CodeGen) -> noUI $ mkS ALL
(Just EX, Concrete{}) -> disallow "Existentially quantified variables"
(_ , Concrete{}) -> noUI mkC
introduceUserName :: State -> Bool -> String -> Kind -> Quantifier -> SW -> IO SVal
introduceUserName st isTracker nm k q sw = do
(is, ints) <- readIORef (rinps st)
if nm `elem` [n | (_, (_, n)) <- is] ++ [n | (_, n) <- ints]
then error $ "SBV: Repeated user given name: " ++ show nm ++ ". Please use unique names."
else if isTracker && q == ALL
then error $ "SBV: Impossible happened! A universally quantified tracker variable is being introduced: " ++ show nm
else do let newInp olds = case q of
EX -> (sw, nm) : olds
ALL -> noInteractive [ "Adding a new universally quantified variable: "
, " Name : " ++ show nm
, " Kind : " ++ show k
, " Quantifier: Universal"
, " Node : " ++ show sw
, "Only existential variables are supported in query mode."
]
if isTracker
then modifyState st rinps (second ((:) (sw, nm)))
$ noInteractive ["Adding a new tracker variable in interactive mode: " ++ show nm]
else modifyState st rinps (first ((:) (q, (sw, nm))))
$ modifyIncState st rNewInps newInp
return $ SVal k $ Right $ cache (const (return sw))
addAxiom :: String -> [String] -> Symbolic ()
addAxiom nm ax = do
st <- ask
liftIO $ modifyState st raxioms ((nm, ax) :)
$ noInteractive [ "Adding a new axiom:"
, " Named: " ++ show nm
, " Axiom: " ++ unlines ax
]
runSymbolic :: SBVRunMode -> Symbolic a -> IO (a, Result)
runSymbolic currentRunMode (Symbolic c) = do
currTime <- getCurrentTime
rm <- newIORef currentRunMode
ctr <- newIORef (-2)
cInfo <- newIORef []
observes <- newIORef []
pgm <- newIORef (SBVPgm S.empty)
emap <- newIORef Map.empty
cmap <- newIORef Map.empty
inps <- newIORef ([], [])
outs <- newIORef []
tables <- newIORef Map.empty
arrays <- newIORef IMap.empty
fArrays <- newIORef IMap.empty
uis <- newIORef Map.empty
cgs <- newIORef Map.empty
axioms <- newIORef []
swCache <- newIORef IMap.empty
aiCache <- newIORef IMap.empty
faiCache <- newIORef IMap.empty
usedKinds <- newIORef Set.empty
usedLbls <- newIORef Set.empty
cstrs <- newIORef []
smtOpts <- newIORef []
optGoals <- newIORef []
asserts <- newIORef []
istate <- newIORef =<< newIncState
qstate <- newIORef Nothing
let st = State { runMode = rm
, startTime = currTime
, pathCond = SVal KBool (Left trueCW)
, rIncState = istate
, rCInfo = cInfo
, rObservables = observes
, rctr = ctr
, rUsedKinds = usedKinds
, rUsedLbls = usedLbls
, rinps = inps
, routs = outs
, rtblMap = tables
, spgm = pgm
, rconstMap = cmap
, rArrayMap = arrays
, rFArrayMap = fArrays
, rexprMap = emap
, rUIMap = uis
, rCgMap = cgs
, raxioms = axioms
, rSWCache = swCache
, rAICache = aiCache
, rFAICache = faiCache
, rConstraints = cstrs
, rSMTOptions = smtOpts
, rOptGoals = optGoals
, rAsserts = asserts
, queryState = qstate
}
_ <- newConst st falseCW
_ <- newConst st trueCW
r <- runReaderT c st
res <- extractSymbolicSimulationState st
qs <- readIORef qstate
case qs of
Nothing -> return ()
Just QueryState{queryTerminate} -> queryTerminate
return (r, res)
extractSymbolicSimulationState :: State -> IO Result
extractSymbolicSimulationState st@State{ spgm=pgm, rinps=inps, routs=outs, rtblMap=tables, rArrayMap=arrays, rUIMap=uis, raxioms=axioms
, rAsserts=asserts, rUsedKinds=usedKinds, rCgMap=cgs, rCInfo=cInfo, rConstraints=cstrs
, rObservables=observes
} = do
SBVPgm rpgm <- readIORef pgm
inpsO <- (reverse *** reverse) <$> readIORef inps
outsO <- reverse <$> readIORef outs
let swap (a, b) = (b, a)
cmp (a, _) (b, _) = a `compare` b
arrange (i, (at, rt, es)) = ((i, at, rt), es)
cnsts <- sortBy cmp . map swap . Map.toList <$> readIORef (rconstMap st)
tbls <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef tables
arrs <- IMap.toAscList <$> readIORef arrays
unint <- Map.toList <$> readIORef uis
axs <- reverse <$> readIORef axioms
knds <- readIORef usedKinds
cgMap <- Map.toList <$> readIORef cgs
traceVals <- reverse <$> readIORef cInfo
observables <- reverse <$> readIORef observes
extraCstrs <- reverse <$> readIORef cstrs
assertions <- reverse <$> readIORef asserts
return $ Result knds traceVals observables cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs assertions outsO
addNewSMTOption :: SMTOption -> Symbolic ()
addNewSMTOption o = do st <- ask
liftIO $ modifyState st rSMTOptions (o:) (return ())
imposeConstraint :: Bool -> [(String, String)] -> SVal -> Symbolic ()
imposeConstraint isSoft attrs c = do st <- ask
rm <- liftIO $ readIORef (runMode st)
case rm of
CodeGen -> error "SBV: constraints are not allowed in code-generation"
_ -> liftIO $ do mapM_ (registerLabel "Constraint" st) [nm | (":named", nm) <- attrs]
internalConstraint st isSoft attrs c
internalConstraint :: State -> Bool -> [(String, String)] -> SVal -> IO ()
internalConstraint st isSoft attrs b = do v <- svToSW st b
modifyState st rConstraints ((isSoft, attrs, v):)
$ noInteractive [ "Adding an internal " ++ soft ++ "constraint:"
, " Named: " ++ fromMaybe "<unnamed>" (listToMaybe [nm | (":named", nm) <- attrs])
]
where soft | isSoft = "soft-"
| True = ""
addSValOptGoal :: Objective SVal -> Symbolic ()
addSValOptGoal obj = do st <- ask
let mkGoal nm orig = liftIO $ do origSW <- svToSW st orig
track <- svMkTrackerVar (kindOf orig) nm st
trackSW <- svToSW st track
return (origSW, trackSW)
let walk (Minimize nm v) = Minimize nm <$> mkGoal nm v
walk (Maximize nm v) = Maximize nm <$> mkGoal nm v
walk (AssertWithPenalty nm v mbP) = flip (AssertWithPenalty nm) mbP <$> mkGoal nm v
obj' <- walk obj
liftIO $ modifyState st rOptGoals (obj' :)
$ noInteractive [ "Adding an optimization objective:"
, " Objective: " ++ show obj
]
outputSVal :: SVal -> Symbolic ()
outputSVal (SVal _ (Left c)) = do
st <- ask
sw <- liftIO $ newConst st c
liftIO $ modifyState st routs (sw:) (return ())
outputSVal (SVal _ (Right f)) = do
st <- ask
sw <- liftIO $ uncache f st
liftIO $ modifyState st routs (sw:) (return ())
newtype Cached a = Cached (State -> IO a)
cache :: (State -> IO a) -> Cached a
cache = Cached
uncache :: Cached SW -> State -> IO SW
uncache = uncacheGen rSWCache
newtype ArrayIndex = ArrayIndex { unArrayIndex :: Int } deriving (Eq, Ord)
instance Show ArrayIndex where
show (ArrayIndex i) = show i
newtype FArrayIndex = FArrayIndex { unFArrayIndex :: Int } deriving (Eq, Ord)
instance Show FArrayIndex where
show (FArrayIndex i) = show i
uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex
uncacheAI = uncacheGen rAICache
uncacheFAI :: Cached FArrayIndex -> State -> IO FArrayIndex
uncacheFAI = uncacheGen rFAICache
uncacheGen :: (State -> IORef (Cache a)) -> Cached a -> State -> IO a
uncacheGen getCache (Cached f) st = do
let rCache = getCache st
stored <- readIORef rCache
sn <- f `seq` makeStableName f
let h = hashStableName sn
case maybe Nothing (sn `lookup`) (h `IMap.lookup` stored) of
Just r -> return r
Nothing -> do r <- f st
r `seq` R.modifyIORef' rCache (IMap.insertWith (++) h [(sn, r)])
return r
data SMTLibVersion = SMTLib2
deriving (Bounded, Enum, Eq, Show)
smtLibVersionExtension :: SMTLibVersion -> String
smtLibVersionExtension SMTLib2 = "smt2"
data SMTLibPgm = SMTLibPgm SMTLibVersion [String]
instance NFData SMTLibVersion where rnf a = a `seq` ()
instance NFData SMTLibPgm where rnf (SMTLibPgm v p) = rnf v `seq` rnf p `seq` ()
instance Show SMTLibPgm where
show (SMTLibPgm _ pre) = intercalate "\n" pre
instance NFData CW where
rnf (CW x y) = x `seq` y `seq` ()
instance NFData GeneralizedCW where
rnf (ExtendedCW e) = e `seq` ()
rnf (RegularCW c) = c `seq` ()
#if MIN_VERSION_base(4,9,0)
#else
instance NFData CallStack where
rnf _ = ()
#endif
instance NFData Result where
rnf (Result kindInfo qcInfo obs cgs inps consts tbls arrs uis axs pgm cstr asserts outs)
= rnf kindInfo `seq` rnf qcInfo `seq` rnf obs `seq` rnf cgs
`seq` rnf inps `seq` rnf consts `seq` rnf tbls
`seq` rnf arrs `seq` rnf uis `seq` rnf axs
`seq` rnf pgm `seq` rnf cstr `seq` rnf asserts
`seq` rnf outs
instance NFData Kind where rnf a = seq a ()
instance NFData ArrayContext where rnf a = seq a ()
instance NFData SW where rnf a = seq a ()
instance NFData SBVExpr where rnf a = seq a ()
instance NFData Quantifier where rnf a = seq a ()
instance NFData SBVType where rnf a = seq a ()
instance NFData SBVPgm where rnf a = seq a ()
instance NFData (Cached a) where rnf (Cached f) = f `seq` ()
instance NFData SVal where rnf (SVal x y) = rnf x `seq` rnf y `seq` ()
instance NFData SMTResult where
rnf Unsatisfiable{} = ()
rnf (Satisfiable _ xs) = rnf xs `seq` ()
rnf (SatExtField _ xs) = rnf xs `seq` ()
rnf (Unknown _ xs) = rnf xs `seq` ()
rnf (ProofError _ xs) = rnf xs `seq` ()
instance NFData SMTModel where
rnf (SMTModel objs assocs) = rnf objs `seq` rnf assocs `seq` ()
instance NFData SMTScript where
rnf (SMTScript b m) = rnf b `seq` rnf m `seq` ()
data SolverCapabilities = SolverCapabilities {
supportsQuantifiers :: Bool
, supportsUninterpretedSorts :: Bool
, supportsUnboundedInts :: Bool
, supportsReals :: Bool
, supportsApproxReals :: Bool
, supportsIEEE754 :: Bool
, supportsOptimization :: Bool
, supportsPseudoBooleans :: Bool
, supportsCustomQueries :: Bool
, supportsGlobalDecls :: Bool
}
data RoundingMode = RoundNearestTiesToEven
| RoundNearestTiesToAway
| RoundTowardPositive
| RoundTowardNegative
| RoundTowardZero
deriving (Eq, Ord, Show, Read, G.Data, Bounded, Enum)
instance HasKind RoundingMode
data SMTConfig = SMTConfig {
verbose :: Bool
, timing :: Timing
, printBase :: Int
, printRealPrec :: Int
, satCmd :: String
, allSatMaxModelCount :: Maybe Int
, isNonModelVar :: String -> Bool
, transcript :: Maybe FilePath
, smtLibVersion :: SMTLibVersion
, solver :: SMTSolver
, roundingMode :: RoundingMode
, solverSetOptions :: [SMTOption]
, ignoreExitCode :: Bool
, redirectVerbose :: Maybe FilePath
}
instance NFData SMTConfig where
rnf SMTConfig{} = ()
data SMTModel = SMTModel {
modelObjectives :: [(String, GeneralizedCW)]
, modelAssocs :: [(String, CW)]
}
deriving Show
data SMTResult = Unsatisfiable SMTConfig (Maybe [String])
| Satisfiable SMTConfig SMTModel
| SatExtField SMTConfig SMTModel
| Unknown SMTConfig SMTReasonUnknown
| ProofError SMTConfig [String]
data SMTScript = SMTScript {
scriptBody :: String
, scriptModel :: [String]
}
type SMTEngine = forall res.
SMTConfig
-> State
-> String
-> (State -> IO res)
-> IO res
data Solver = Z3
| Yices
| Boolector
| CVC4
| MathSAT
| ABC
deriving (Show, Enum, Bounded)
data SMTSolver = SMTSolver {
name :: Solver
, executable :: String
, options :: SMTConfig -> [String]
, engine :: SMTEngine
, capabilities :: SolverCapabilities
}
data QueryContext = QueryInternal
| QueryExternal
{-# ANN type FPOp ("HLint: ignore Use camelCase" :: String) #-}
{-# ANN type PBOp ("HLint: ignore Use camelCase" :: String) #-}
{-# ANN type OvOp ("HLint: ignore Use camelCase" :: String) #-}