sbv 0.9.7 → 0.9.8
raw patch · 10 files changed
+264/−151 lines, 10 files
Files
- Data/SBV/BitVectors/Data.hs +87/−35
- Data/SBV/Examples/PrefixSum/PrefixSum.hs +28/−16
- Data/SBV/Examples/Uninterpreted/Function.hs +4/−4
- Data/SBV/Provers/Prover.hs +23/−16
- Data/SBV/Provers/SExpr.hs +7/−5
- Data/SBV/Provers/Yices.hs +71/−49
- Data/SBV/SMT/SMT.hs +23/−11
- Data/SBV/SMT/SMTLib.hs +12/−10
- SBVUnitTest/GoldFiles/auf-1.gold +3/−3
- sbv.cabal +6/−2
Data/SBV/BitVectors/Data.hs view
@@ -26,12 +26,12 @@ , mkConstCW, liftCW2, mapCW, mapCW2 , SW(..), trueSW, falseSW , SBV(..), NodeId(..), mkSymSBV- , ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), SArray(..)+ , ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), SArray(..), arrayUIKind , sbvToSW , SBVExpr(..), newExpr , cache, uncache, HasSignAndSize(..)- , Op(..), NamedSymVar, getTableIndex, Pgm, Symbolic, runSymbolic, State, Size, output, Result(..)- , SBVType(..), newUninterpreted+ , Op(..), NamedSymVar, UnintKind(..), getTableIndex, Pgm, Symbolic, runSymbolic, State, Size, output, Result(..)+ , SBVType(..), newUninterpreted, unintFnUIKind ) where import Control.DeepSeq (NFData(..))@@ -76,6 +76,10 @@ newtype SBVType = SBVType [(Bool, Size)] deriving (Eq, Ord) +-- how many arguments does the type take?+typeArity :: SBVType -> Int+typeArity (SBVType xs) = length xs - 1+ instance Show SBVType where show (SBVType []) = error "SBV: internal error, empty SBVType" show (SBVType xs) = intercalate " -> " $ map sh xs@@ -108,6 +112,7 @@ | True = if hasSign a then "SInt" else "SWord" ++ show (sizeOf a) instance HasSignAndSize Bit where {sizeOf _ = 1; hasSign _ = False}+instance HasSignAndSize Bool where {sizeOf _ = 1; hasSign _ = False} instance HasSignAndSize Int8 where {sizeOf _ = 8; hasSign _ = True } instance HasSignAndSize Word8 where {sizeOf _ = 8; hasSign _ = False} instance HasSignAndSize Int16 where {sizeOf _ = 16; hasSign _ = True }@@ -189,9 +194,9 @@ 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 (Uninterpreted i) = "ui_" ++ i+ show (ArrEq i j) = "array_" ++ show i ++ " == array_" ++ show j+ show (ArrRead i) = "select array_" ++ show i+ show (Uninterpreted i) = "uninterpreted_" ++ i show op | Just s <- op `lookup` syms = s | True = error "impossible happened; can't find op!"@@ -227,14 +232,19 @@ -- | 'NamedSymVar' pairs symbolic words and user given/automatically generated names type NamedSymVar = (SW, String) +-- | 'UnintKind' pairs array names and uninterpreted constants with their "kinds"+-- used mainly for printing counterexamples+data UnintKind = UFun Int String | UArr Int String -- in each case, arity and the aliasing name+ deriving Show+ -- | Result of running a symbolic computation-data Result = Result [NamedSymVar] -- inputs- [(SW, CW)] -- constants- [((Int, Int, Int), [SW])] -- tables (automatically constructed)- [(Int, ArrayInfo)] -- arrays (user specified)- [(String, SBVType)] -- uninterpreted constants- Pgm -- assignments- [SW] -- outputs+data Result = Result [NamedSymVar] -- inputs+ [(SW, CW)] -- constants+ [((Int, Int, Int), [SW])] -- tables (automatically constructed)+ [(Int, ArrayInfo)] -- arrays (user specified)+ [(String, SBVType)] -- uninterpreted constants+ Pgm -- assignments+ [SW] -- outputs instance Show Result where show (Result _ cs _ _ [] _ [r])@@ -267,21 +277,22 @@ where mkT (b, s) | s == 1 = "SBool" | True = if b then "SInt" else "SWord" ++ show s- ni = "array" ++ show i+ ni = "array_" ++ show i alias | ni == nm = "" | True = ", aliasing " ++ show nm- shui (nm, t) = " ui_" ++ nm ++ " :: " ++ show t+ shui (nm, t) = " uninterpreted_" ++ nm ++ " :: " ++ show t -data ArrayContext = ArrayFree- | ArrayInit SW+data ArrayContext = ArrayFree (Maybe SW)+ | ArrayReset Int SW | ArrayMutate Int SW SW | ArrayMerge SW Int Int instance Show ArrayContext where- show ArrayFree = " initialized with random elements"- show (ArrayInit s) = " initialized with " ++ show s ++ ":: " ++ showType s- show (ArrayMutate i a b) = " cloned from array" ++ show i ++ " with " ++ show a ++ " :: " ++ showType a ++ " |-> " ++ show b ++ " :: " ++ showType b- show (ArrayMerge s i j) = " merged arrays " ++ show i ++ " and " ++ show j ++ " on condition " ++ show s+ show (ArrayFree Nothing) = " initialized with random elements"+ show (ArrayFree (Just s)) = " initialized with " ++ show s ++ " :: " ++ showType s+ show (ArrayReset i s) = " reset array_" ++ show i ++ " with " ++ show s ++ " :: " ++ showType s+ show (ArrayMutate i a b) = " cloned from array_" ++ show i ++ " with " ++ show a ++ " :: " ++ showType a ++ " |-> " ++ show b ++ " :: " ++ showType 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@@ -290,6 +301,19 @@ type ArrayMap = IMap.IntMap ArrayInfo type UIMap = Map.Map String SBVType ++unintFnUIKind :: (String, SBVType) -> (String, UnintKind)+unintFnUIKind (s, t) = (s, UFun (typeArity t) s)++arrayUIKind :: (Int, ArrayInfo) -> Maybe (String, UnintKind)+arrayUIKind (i, (nm, _, ctx)) + | external ctx = Just ("array_" ++ show i, UArr 1 nm) -- arrays are always 1-dimensional in the SMT-land. (Unless encoded explicitly)+ | True = Nothing+ where external (ArrayFree{}) = True+ external (ArrayReset{}) = False+ external (ArrayMutate{}) = False+ external (ArrayMerge{}) = False+ data State = State { rctr :: IORef Int , rinps :: IORef [NamedSymVar] , routs :: IORef [SW]@@ -497,6 +521,8 @@ -- to be fed to a symbolic program. Note that these methods are typically not needed -- in casual uses with 'prove', 'sat', 'allSat' etc, as default instances automatically -- provide the necessary bits.+--+-- Minimal complete definiton: free, free_, literal, fromCW class Ord a => SymWord a where -- | Create a user named input free :: String -> Symbolic (SBV a)@@ -513,7 +539,7 @@ -- | Is the symbolic word really symbolic? isSymbolic :: SBV a -> Bool - -- | minimal complete definiton: free, free_, literal, fromCW+ -- minimal complete definiton: free, free_, literal, fromCW unliteral (SBV _ (Left c)) = Just $ fromCW c unliteral _ = Nothing isConcrete (SBV _ (Left _)) = True@@ -528,17 +554,19 @@ -- An @array a b@ is an array indexed by the type @'SBV' a@, with elements of type @'SBV' b@ -- If an initial value is not provided in 'newArray_' and 'newArray' methods, then the elements -- are left unspecified, i.e., the solver is free to choose any value. This is the right thing--- to do if arrays are used as inputs to functions to be verified, typically. Reading an--- uninitilized entry is an error.+-- to do if arrays are used as inputs to functions to be verified, typically. +-- -- While it's certainly possible for user to create instances of 'SymArray', the -- 'SArray' and 'SFunArray' instances already provided should cover most use cases--- in practice.+-- in practice. (There are some differences between these models, however, see the corresponding+-- declaration.) --+-- -- Minimal complete definition: All methods are required, no defaults. class SymArray array where -- | Create a new array, with an optional initial value newArray_ :: (HasSignAndSize a, HasSignAndSize b) => Maybe (SBV b) -> Symbolic (array a b)- -- | Create a named new array with, with an optional initial value+ -- | Create a named new array, with an optional initial value newArray :: (HasSignAndSize a, HasSignAndSize b) => String -> Maybe (SBV b) -> Symbolic (array a b) -- | Read the array element at @a@ readArray :: array a b -> SBV a -> SBV b@@ -552,6 +580,17 @@ mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a b -- | Arrays implemented in terms of SMT-arrays: <http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2>+--+-- * Maps directly to SMT-lib arrays+--+-- * Reading from an unintialized value is OK and yields an uninterpreted result+--+-- * Can check for equality of these arrays+--+-- * Cannot quick-check theorems using @SArray@ values+--+-- * Typically slower as it heavily relies on SMT-solving for the array theory+-- data SArray a b = SArray ((Bool, Size), (Bool, Size)) (Cached ArrayIndex) type ArrayIndex = Int @@ -559,17 +598,18 @@ show (SArray{}) = "SArray<" ++ showType (undefined :: a) ++ ":" ++ showType (undefined :: b) ++ ">" instance SymArray SArray where- newArray_ = declNewSArray (\t -> "array" ++ show t)+ newArray_ = declNewSArray (\t -> "array_" ++ show t) newArray n = declNewSArray (const n) readArray (SArray (_, bsgnsz) f) a = SBV bsgnsz $ Right $ cache r where r st = do arr <- uncache f st i <- sbvToSW st a newExpr st bsgnsz (SBVApp (ArrRead arr) [i])- resetArray (SArray ainfo _) b = SArray ainfo $ cache g+ resetArray (SArray ainfo f) b = SArray ainfo $ cache g where g st = do amap <- readIORef (rArrayMap st) val <- sbvToSW st b+ i <- uncache f st let j = IMap.size amap- j `seq` modifyIORef (rArrayMap st) (IMap.insert j ("array" ++ show j, ainfo, ArrayInit val))+ j `seq` modifyIORef (rArrayMap st) (IMap.insert j ("array_" ++ show j, ainfo, ArrayReset i val)) return j writeArray (SArray ainfo f) a b = SArray ainfo $ cache g where g st = do arr <- uncache f st@@ -577,7 +617,7 @@ val <- sbvToSW st b amap <- readIORef (rArrayMap st) let j = IMap.size amap- j `seq` modifyIORef (rArrayMap st) (IMap.insert j ("array" ++ show j, ainfo, ArrayMutate arr addr val))+ j `seq` modifyIORef (rArrayMap st) (IMap.insert j ("array_" ++ show j, ainfo, ArrayMutate arr addr val)) return j mergeArrays t (SArray ainfo a) (SArray _ b) = SArray ainfo $ cache h where h st = do ai <- uncache a st@@ -585,7 +625,7 @@ ts <- sbvToSW st t amap <- readIORef (rArrayMap st) let k = IMap.size amap- k `seq` modifyIORef (rArrayMap st) (IMap.insert k ("array" ++ show k, ainfo, ArrayMerge ts ai bi))+ k `seq` modifyIORef (rArrayMap st) (IMap.insert k ("array_" ++ show k, ainfo, ArrayMerge ts ai bi)) return k declNewSArray :: forall a b. (HasSignAndSize a, HasSignAndSize b) => (Int -> String) -> Maybe (SBV b) -> Symbolic (SArray a b)@@ -596,13 +636,24 @@ amap <- liftIO $ readIORef $ rArrayMap st let i = IMap.size amap nm = mkNm i- actx <- case mbInit of- Nothing -> return ArrayFree- Just ival -> liftIO $ ArrayInit `fmap` sbvToSW st ival+ actx <- liftIO $ case mbInit of+ Nothing -> return $ ArrayFree Nothing+ Just ival -> sbvToSW st ival >>= \sw -> return $ ArrayFree (Just sw) liftIO $ modifyIORef (rArrayMap st) (IMap.insert i (nm, (asgnsz, bsgnsz), actx)) return $ SArray (asgnsz, bsgnsz) $ cache $ const $ return i --- | Arrays implemented internally as functions, and rendered as SMT-Lib functions+-- | Arrays implemented internally as functions+--+-- * Internally handled by the library and not mapped to SMT-Lib+--+-- * Reading an uninitialized value is considered an error (will throw exception)+--+-- * Cannot check for equality (internally represented as functions)+--+-- * Can quick-check+--+-- * Typically faster as it gets compiled away during translation+-- data SFunArray a b = SFunArray (SBV a -> SBV b) instance (HasSignAndSize a, HasSignAndSize b) => Show (SFunArray a b) where@@ -659,6 +710,7 @@ instance NFData Pgm instance NFData SW instance NFData SBVType+instance NFData UnintKind -- Quickcheck interface on symbolic-booleans.. instance Testable SBool where
Data/SBV/Examples/PrefixSum/PrefixSum.hs view
@@ -8,7 +8,9 @@ -- Portability : portable -- -- The PrefixSum algorithm over power-lists and proof of--- the Fischer-Ladner implementation+-- the Ladner-Fischer implementation.+-- See <http://www.cs.utexas.edu/users/psp/powerlist.pdf>+-- and <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>. ----------------------------------------------------------------------------- {-# LANGUAGE Rank2Types #-}@@ -18,46 +20,56 @@ import Data.SBV --- A poor man's representation of powerlists and--- basic operations on them:+-- | A poor man's representation of powerlists and+-- basic operations on them: <http://www.cs.utexas.edu/users/psp/powerlist.pdf>.+-- We merely represent power-lists by ordinary lists. type PowerList a = [a] +-- | The tie operator, concatenation tiePL :: PowerList a -> PowerList a -> PowerList a tiePL = (++) +-- | The zip operator, zips the power-lists of the same size, returns+-- a powerlist of double the size. zipPL :: PowerList a -> PowerList a -> PowerList a zipPL [] [] = [] zipPL (x:xs) (y:ys) = x : y : zipPL xs ys zipPL _ _ = error "zipPL: nonsimilar powerlists received" +-- | Inverse of zipping unzipPL :: PowerList a -> (PowerList a, PowerList a) unzipPL = unzip . chunk2 where chunk2 [] = [] chunk2 (x:y:xs) = (x,y) : chunk2 xs- chunk2 _ = error "fl.unzipPL: malformed powerlist"+ chunk2 _ = error "unzipPL: malformed powerlist" --- Reference prefix sum is simply scanl1+-- | Reference prefix sum (@ps@) is simply Haskell's @scanl1@ function ps :: (a, a -> a -> a) -> PowerList a -> PowerList a ps (_, f) = scanl1 f --- Fischer-Ladner version-fl :: (a, a -> a -> a) -> PowerList a -> PowerList a-fl _ [] = error "fl: malformed (empty) powerlist"-fl _ [x] = [x]-fl (zero, f) pl = zipPL (zipWith f (rsh flpq) p) flpq+-- | The Ladner-Fischer (@lf@) implementation of prefix-sum. See <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>+-- or pg. 16 of <http://www.cs.utexas.edu/users/psp/powerlist.pdf>.+lf :: (a, a -> a -> a) -> PowerList a -> PowerList a+lf _ [] = error "lf: malformed (empty) powerlist"+lf _ [x] = [x]+lf (zero, f) pl = zipPL (zipWith f (rsh flpq) p) flpq where (p, q) = unzipPL pl pq = zipWith f p q- flpq = fl (zero, f) pq+ flpq = lf (zero, f) pq rsh xs = zero : init xs --- Correctness theorem, for a powerlist of given size and--- an associative operator. We'll run the symbolic execution over Word32's+-- | Correctness theorem, for a powerlist of given size, an associative operator, and its unit element flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool flIsCorrect n zf = do args :: PowerList SWord32 <- mapM (const free_) [1..n]- output $ ps zf args .== fl zf args+ output $ ps zf args .== lf zf args --- Instances that can be proven directly:-thm1, thm2 :: IO ThmResult+-- | Proves Ladner-Fischer is equivalent to reference specification for addition.+-- @0@ is the unit element, and we use a power-list of size @8@.+thm1 :: IO ThmResult thm1 = prove $ flIsCorrect 8 (0, (+))++-- | Proves Ladner-Fischer is equivalent to reference specification for the function @max@.+-- @0@ is the unit element, and we use a power-list of size @16@.+thm2 :: IO ThmResult thm2 = prove $ flIsCorrect 16 (0, smax)
Data/SBV/Examples/Uninterpreted/Function.hs view
@@ -27,13 +27,13 @@ -- function that is not commutative. We have: -- -- @--- ghci> prove thmBad+-- ghci> prove $ forAll ["x", "y"] thmBad -- Falsifiable. Counter-example:--- s0 = 0 :: SWord8--- s1 = 128 :: SWord8+-- x = 0 :: SWord8+-- y = 128 :: SWord8 -- -- uninterpreted: f -- f 128 0 = 32768--- f _ _ = 0+-- f _ _ = 0 -- @ -- -- Note how the counterexample function @f@ returned by Yices violates commutativity;
Data/SBV/Provers/Prover.hs view
@@ -36,7 +36,7 @@ import Control.Monad (when) import Control.Concurrent (forkIO) import Control.Concurrent.Chan.Strict (newChan, writeChan, getChanContents)-import Data.Maybe (fromJust, isJust)+import Data.Maybe (fromJust, isJust, catMaybes) import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model@@ -125,7 +125,7 @@ forAll (s:ss) k = free s >>= \a -> forAll ss $ k a forAll [] k = forAll_ k --- Memory+-- Arrays (memory) instance (HasSignAndSize a, HasSignAndSize b, SymArray array, Provable p) => Provable (array a b -> p) where forAll_ k = newArray_ Nothing >>= \a -> forAll_ $ k a forAll (s:ss) k = newArray s Nothing >>= \a -> forAll ss $ k a@@ -178,6 +178,11 @@ -- | Return all satisfying assignments for a predicate, equivalent to @'allSatWith' 'defaultSMTCfg'@. -- Satisfying assignments are constructed lazily, so they will be available as returned by the solver -- and on demand.+--+-- NB. Uninterpreted constant/function values and counter-examples for array values are ignored for+-- the purposes of @'allSat'@. That is, only the satisfying assignments modulo uninterpreted functions and+-- array inputs will be returned. This is due to the limitation of not having a robust means of getting a+-- function counter-example back from the SMT solver. allSat :: Provable a => a -> IO AllSatResult allSat = allSatWith defaultSMTCfg @@ -255,35 +260,37 @@ where loop !n nonEqConsts = do SatResult r <- callSolver nonEqConsts ("Looking for solution " ++ show n) SatResult config sbvPgm case r of- Satisfiable _ (SMTModel [] _) -> final r- Unknown _ (SMTModel [] _) -> final r- ProofError _ _ -> final r- TimeOut _ -> stop- Unsatisfiable _ -> stop- Satisfiable _ model -> add r >> loop (n+1) (modelAssocs model : nonEqConsts)- Unknown _ model -> add r >> loop (n+1) (modelAssocs model : nonEqConsts)+ Satisfiable _ (SMTModel [] _ _) -> final r+ Unknown _ (SMTModel [] _ _) -> final r+ ProofError _ _ -> final r+ TimeOut _ -> stop+ Unsatisfiable _ -> stop+ Satisfiable _ model -> add r >> loop (n+1) (modelAssocs model : nonEqConsts)+ Unknown _ model -> add r >> loop (n+1) (modelAssocs model : nonEqConsts) -callSolver :: [[(String, CW)]] -> String -> (SMTResult -> b) -> SMTConfig -> ([NamedSymVar], SMTLibPgm) -> IO b-callSolver nonEqConstraints checkMsg wrap config (inps, smtLibPgm) = do+callSolver :: [[(String, CW)]] -> String -> (SMTResult -> b) -> SMTConfig -> ([NamedSymVar], [(String, UnintKind)], SMTLibPgm) -> IO b+callSolver nonEqConstraints checkMsg wrap config (inps, modelMap, smtLibPgm) = do let msg = when (verbose config) . putStrLn . ("** " ++) msg checkMsg let finalPgm = addNonEqConstraints nonEqConstraints smtLibPgm msg $ "Generated SMTLib program:\n" ++ finalPgm- smtAnswer <- engine (solver config) config inps finalPgm+ smtAnswer <- engine (solver config) config inps modelMap finalPgm msg "Done.." return $ wrap smtAnswer -generateTrace :: Provable a => SMTConfig -> Bool -> a -> IO ([NamedSymVar], SMTLibPgm)+generateTrace :: Provable a => SMTConfig -> Bool -> a -> IO ([NamedSymVar], [(String, UnintKind)], SMTLibPgm) generateTrace config isSat predicate = do let msg = when (verbose config) . putStrLn . ("** " ++) isTiming = timing config- msg "Generating a symbolic trace.."+ msg "Starting symbolic simulation.." res <- timeIf isTiming "problem construction" $ runSymbolic $ forAll_ predicate msg $ "Generated symbolic trace:\n" ++ show res msg "Translating to SMT-Lib.." case res of- Result is consts tbls arrs uis pgm [o@(SW{})] -> timeIf isTiming "translation" $ return (is, toSMTLib isSat is consts tbls arrs uis pgm o)- _ -> error $ "SBVProver.callSolver: Impossible happened: " ++ show res+ Result is consts tbls arrs uis pgm [o@(SW{})] ->+ timeIf isTiming "translation" $ let uiMap = catMaybes (map arrayUIKind arrs) ++ map unintFnUIKind uis+ in return (is, uiMap, toSMTLib isSat is consts tbls arrs uis pgm o)+ _ -> error $ "SBVProver.callSolver: Impossible happened: " ++ show res -- | Equality as a proof method. Allows for -- very concise construction of equivalence proofs, which is very typical in
Data/SBV/Provers/SExpr.hs view
@@ -29,14 +29,16 @@ cln (':':':':r) sofar = cln r (" :: " ++ sofar) cln (c:r) sofar = cln r (c:sofar) in reverse (map reverse (words (cln inp "")))- parse [] = fail "ran out of tokens"+ die w = fail $ "SBV.Provers.SExpr: Failed to parse S-Expr: " ++ w+ ++ "\n*** Input : <" ++ inp ++ ">"+ parse [] = die "ran out of tokens" parse ("(":toks) = do (f, r) <- parseApp toks [] return (S_App f, r)- parse (")":_) = fail "extra tokens after close paren"+ parse (")":_) = die "extra tokens after close paren" parse [tok] = do t <- pTok tok return (t, [])- parse _ = fail "ill-formed s-expr"- parseApp [] _ = fail "failed to grab s-expr application"+ parse _ = die "ill-formed s-expr"+ parseApp [] _ = die "failed to grab s-expr application" parseApp (")":toks) sofar = return (reverse sofar, toks) parseApp ("(":toks) sofar = do (f, r) <- parse ("(":toks) parseApp r (f : sofar)@@ -47,4 +49,4 @@ pTok n | all isDigit n = mkNum $ readDec n pTok n = return $ S_Con $ n mkNum [(n, "")] = return $ S_Num n- mkNum _ = fail "cannot read number"+ mkNum _ = die "cannot read number"
Data/SBV/Provers/Yices.hs view
@@ -14,9 +14,9 @@ module Data.SBV.Provers.Yices(yices, timeout) where -import Control.Monad (foldM) import Data.Char (isDigit)-import Data.List (sortBy, isPrefixOf)+import Data.List (sortBy, isPrefixOf, intercalate, transpose, partition)+import Data.Maybe (catMaybes, isJust, fromJust) import System.Environment (getEnv) import Data.SBV.BitVectors.Data@@ -32,11 +32,11 @@ , executable = "yices" -- , options = ["-tc", "-smt", "-e"] -- For Yices1 , options = ["-m", "-f"] -- For Yices2- , engine = \cfg inps pgm -> do+ , engine = \cfg inps modelMap pgm -> do execName <- getEnv "SBV_YICES" `catch` (\_ -> return (executable (solver cfg))) execOpts <- (words `fmap` (getEnv "SBV_YICES_OPTIONS")) `catch` (\_ -> return (options (solver cfg))) let cfg' = cfg { solver = (solver cfg) {executable = execName, options = execOpts} }- standardSolver cfg' pgm (ProofError cfg) (interpret cfg inps)+ standardSolver cfg' pgm (ProofError cfg) (interpret cfg inps modelMap) } timeout :: Int -> SMTSolver -> SMTSolver@@ -47,24 +47,30 @@ sortByNodeId :: [(Int, a)] -> [(Int, a)] sortByNodeId = sortBy (\(x, _) (y, _) -> compare x y) -interpret :: SMTConfig -> [NamedSymVar] -> [String] -> SMTResult-interpret cfg _ ("unsat":_) = Unsatisfiable cfg-interpret cfg inps ("unknown":rest) = Unknown cfg $ extractMap inps rest-interpret cfg inps ("sat":rest) = Satisfiable cfg $ extractMap inps rest-interpret cfg _ ("timeout":_) = TimeOut cfg-interpret cfg _ ls = ProofError cfg $ ls+interpret :: SMTConfig -> [NamedSymVar] -> [(String, UnintKind)] -> [String] -> SMTResult+interpret cfg _ _ ("unsat":_) = Unsatisfiable cfg+interpret cfg inps modelMap ("unknown":rest) = Unknown cfg $ extractMap inps modelMap rest+interpret cfg inps modelMap ("sat":rest) = Satisfiable cfg $ extractMap inps modelMap rest+interpret cfg _ _ ("timeout":_) = TimeOut cfg+interpret cfg _ _ ls = ProofError cfg $ ls -extractMap :: [NamedSymVar] -> [String] -> SMTModel-extractMap inps solverLines =+extractMap :: [NamedSymVar] -> [(String, UnintKind)] -> [String] -> SMTModel+extractMap inps modelMap solverLines = SMTModel { modelAssocs = map (\(_, y) -> y) $ sortByNodeId $ concatMap (getCounterExample inps) modelLines- , modelUninterps = extractUnints unintLines+ , modelUninterps = [(n, ls) | (UFun _ n, ls) <- uis]+ , modelArrays = [(n, ls) | (UArr _ n, ls) <- uis] }- where (modelLines, unintLines) = break ("--- uninterpreted_" `isPrefixOf`) solverLines+ where (modelLines, unintLines) = moveConstUIs $ break ("--- " `isPrefixOf`) solverLines+ uis = extractUnints modelMap unintLines +-- another crude hack+moveConstUIs :: ([String], [String]) -> ([String], [String])+moveConstUIs (pre, post) = (pre', concatMap mkDecl extras ++ post)+ where (extras, pre') = partition ("(= uninterpreted_" `isPrefixOf`) pre+ mkDecl s = ["--- " ++ takeWhile (/= ' ') (drop 3 s) ++ " ---", s]+ getCounterExample :: [NamedSymVar] -> String -> [(Int, (String, CW))]-getCounterExample inps line- | isComment line = []- | True = either err extract (parseSExpr line)+getCounterExample inps line = either err extract (parseSExpr line) where err r = error $ "*** Failed to parse Yices model output from: " ++ "*** " ++ show line ++ "\n" ++ "*** Reason: " ++ r ++ "\n"@@ -81,48 +87,64 @@ extract (S_App [S_Con "=", S_Num i, S_Con v]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (hasSign s, sizeOf s) i))] extract _ = [] --- this is largely by observation of Yices output; not quite sure if it captures all-isComment :: String -> Bool-isComment s = any (`isPrefixOf` s) prefixes- where prefixes = ["---", "default"]--extractUnints :: [String] -> [(String, [String])]-extractUnints [] = []-extractUnints xs = case extractUnint first of- Nothing -> extractUnints rest- Just x -> x : extractUnints rest- where first = takeWhile p xs- rest = tail' (dropWhile p xs)- p = not . ("----" `isPrefixOf`)- tail' [] = []- tail' (_ : rs) = rs+extractUnints :: [(String, UnintKind)] -> [String] -> [(UnintKind, [String])]+extractUnints modelMap = catMaybes . map (extractUnint modelMap) . chunks+ where chunks [] = []+ chunks (x:xs) = let (f, r) = span (not . ("---" `isPrefixOf`)) xs in (x:f) : chunks r -extractUnint :: [String] -> Maybe (String, [String])-extractUnint [] = Nothing-extractUnint (tag : rest)- | null tag' = Nothing- | True = foldM (getUIVal f) (0, []) rest >>= \(_, xs) -> return (f, reverse xs)- where tag' = dropWhile (/= '_') tag+-- Parsing the Yices output is done extremely crudely and designed+-- mostly by observation of Yices output. Likely to have bugs and+-- brittle as Yices evolves. We really need an SMT-Lib2 like interface.+extractUnint :: [(String, UnintKind)] -> [String] -> Maybe (UnintKind, [String])+extractUnint _ [] = Nothing+extractUnint mmap (tag : rest)+ | null tag' = Nothing+ | not (isJust mbKnd) = Nothing+ | True = mapM (getUIVal knd) rest >>= \xs -> return (knd, format knd xs)+ where mbKnd | "--- uninterpreted_" `isPrefixOf` tag = uf `lookup` mmap+ | True = af `lookup` mmap+ knd = fromJust mbKnd+ tag' = dropWhile (/= '_') tag f = takeWhile (/= ' ') (tail tag')+ uf = f+ af = "array_" ++ f -getUIVal :: String -> (Int, [String]) -> String -> Maybe (Int, [String])-getUIVal f (cnt, sofar) s+getUIVal :: UnintKind -> String -> Maybe (String, [String], String)+getUIVal knd s | "default: " `isPrefixOf` s- = getDefaultVal cnt f (dropWhile (/= ' ') s) >>= \d -> return (cnt, d : sofar)+ = getDefaultVal knd (dropWhile (/= ' ') s) | True = case parseSExpr s of- Right (S_App [S_Con "=", (S_App (S_Con v : args)), S_Num i]) | v == "uninterpreted_" ++ f- -> getCallVal cnt f args i >>= \(cnt', d) -> return (cnt', d : sofar)+ Right (S_App [S_Con "=", (S_App (S_Con _ : args)), S_Num i]) -> getCallVal knd args i+ Right (S_App [S_Con "=", S_Con _, S_Num i]) -> getCallVal knd [] i _ -> Nothing -getDefaultVal :: Int -> String -> String -> Maybe String-getDefaultVal cnt f n = case parseSExpr n of- Right (S_Num i) -> Just $ f ++ " " ++ unwords (replicate cnt "_") ++ " = " ++ show i- _ -> Nothing+getDefaultVal :: UnintKind -> String -> Maybe (String, [String], String)+getDefaultVal knd n = case parseSExpr n of+ Right (S_Num i) -> Just $ showDefault knd (show i)+ _ -> Nothing -getCallVal :: Int -> String -> [SExpr] -> Integer -> Maybe (Int, String)-getCallVal cnt f args res = mapM getArg args >>= \as -> return (cnt `max` length as, f ++ " " ++ unwords as ++ " = " ++ show res)+getCallVal :: UnintKind -> [SExpr] -> Integer -> Maybe (String, [String], String)+getCallVal knd args res = mapM getArg args >>= \as -> return (showCall knd as (show res)) getArg :: SExpr -> Maybe String getArg (S_Num i) = Just (show i) getArg _ = Nothing++showDefault :: UnintKind -> String -> (String, [String], String)+showDefault (UFun cnt f) res = (f, replicate cnt "_", res)+showDefault (UArr cnt f) res = (f, replicate cnt "_", res)++showCall :: UnintKind -> [String] -> String -> (String, [String], String)+showCall (UFun _ f) as res = (f, as, res)+showCall (UArr _ f) as res = (f, as, res)++format :: UnintKind -> [(String, [String], String)] -> [String]+format (UFun{}) eqns = fmtFun eqns+format (UArr{}) eqns = let fmt (f, as, r) = f ++ "[" ++ intercalate ", " as ++ "] = " ++ r in map fmt eqns++fmtFun :: [(String, [String], String)] -> [String]+fmtFun ls = map fmt ls+ where fmt (f, as, r) = f ++ " " ++ unwords (map align (zip as (lens ++ repeat 0))) ++ " = " ++ r+ lens = map (maximum . (0:)) $ map (map length) $ transpose [as | (_, as, _) <- ls]+ align (s, i) = take (i `max` length s) (s ++ repeat ' ')
Data/SBV/SMT/SMT.hs view
@@ -37,7 +37,7 @@ , solver :: SMTSolver -- ^ The actual SMT solver } -type SMTEngine = SMTConfig -> [NamedSymVar] -> String -> IO SMTResult+type SMTEngine = SMTConfig -> [NamedSymVar] -> [(String, UnintKind)] -> String -> IO SMTResult -- | An SMT solver data SMTSolver = SMTSolver {@@ -50,6 +50,7 @@ -- | A model, as returned by a solver data SMTModel = SMTModel { modelAssocs :: [(String, CW)]+ , modelArrays :: [(String, [String])] -- very crude! , modelUninterps :: [(String, [String])] -- very crude! } deriving Show@@ -80,7 +81,7 @@ rnf (TimeOut _) = () instance NFData SMTModel where- rnf (SMTModel assocs unints) = rnf assocs `seq` rnf unints `seq` ()+ rnf (SMTModel assocs unints uarrs) = rnf assocs `seq` rnf unints `seq` rnf uarrs `seq` () -- | A 'prove' call results in a 'ThmResult' newtype ThmResult = ThmResult SMTResult@@ -227,16 +228,22 @@ showSMTResult :: String -> String -> String -> String -> String -> SMTResult -> String showSMTResult unsatMsg unkMsg unkMsgModel satMsg satMsgModel result = case result of- Unsatisfiable _ -> unsatMsg- Satisfiable _ (SMTModel [] []) -> satMsg- Satisfiable _ m -> satMsgModel ++ intercalate "\n" (map (shM cfg) (modelAssocs m) ++ concatMap shUI (modelUninterps m))- Unknown _ (SMTModel [] []) -> unkMsg- Unknown _ m -> unkMsgModel ++ intercalate "\n" (map (shM cfg) (modelAssocs m) ++ concatMap shUI (modelUninterps m))- ProofError _ [] -> "*** An error occurred. No additional information available. Try running in verbose mode"- ProofError _ ls -> "*** An error occurred.\n" ++ intercalate "\n" (map ("*** " ++) ls)- TimeOut _ -> "*** Timeout"+ Unsatisfiable _ -> unsatMsg+ Satisfiable _ (SMTModel [] [] []) -> satMsg+ Satisfiable _ m -> satMsgModel ++ showModel cfg m+ Unknown _ (SMTModel [] [] []) -> unkMsg+ Unknown _ m -> unkMsgModel ++ showModel cfg m+ ProofError _ [] -> "*** An error occurred. No additional information available. Try running in verbose mode"+ ProofError _ ls -> "*** An error occurred.\n" ++ intercalate "\n" (map ("*** " ++) ls)+ TimeOut _ -> "*** Timeout" where cfg = resultConfig result +showModel :: SMTConfig -> SMTModel -> String+showModel cfg m = intercalate "\n" (map (shM cfg) assocs ++ concatMap shUI uninterps ++ concatMap shUA arrs)+ where assocs = modelAssocs m+ uninterps = modelUninterps m+ arrs = modelArrays m+ shCW :: SMTConfig -> CW -> String shCW cfg v = sh (printBase cfg) v where sh 2 = binS@@ -247,12 +254,17 @@ shM :: SMTConfig -> (String, CW) -> String shM cfg (s, v) = " " ++ s ++ " = " ++ shCW cfg v --- very crude..+-- very crude.. printing uninterpreted functions shUI :: (String, [String]) -> [String] shUI (flong, cases) = (" -- uninterpreted: " ++ f) : map shC cases where tf = dropWhile (/= '_') flong f = if null tf then flong else tail tf shC s = " " ++ s++-- very crude.. printing array values+shUA :: (String, [String]) -> [String]+shUA (f, cases) = (" -- array: " ++ f) : map shC cases+ where shC s = " " ++ s pipeProcess :: String -> String -> [String] -> String -> IO (Either String [String]) pipeProcess nm execName opts script = do
Data/SBV/SMT/SMTLib.hs view
@@ -71,16 +71,18 @@ declArray :: (Int, ArrayInfo) -> [String] declArray (i, (_, ((_, at), (_, rt)), ctx)) = adecl : ctxInfo- where nm = "array" ++ show i+ where nm = "array_" ++ show i adecl = " :extrafuns ((" ++ nm ++ " Array[" ++ show at ++ ":" ++ show rt ++ "]))" ctxInfo = case ctx of- ArrayFree -> []- ArrayInit sw -> let iv = nm ++ "_freeInitializer"- in [ " :extrafuns ((" ++ iv ++ " BitVec[" ++ show at ++ "]))"- , " :assumption (= (select " ++ nm ++ " " ++ iv ++ ") " ++ show sw ++ ")"- ]- ArrayMutate j a b -> [" :assumption (= " ++ nm ++ " (store array" ++ show j ++ " " ++ show a ++ " " ++ show b ++ "))"]- ArrayMerge t j k -> [" :assumption (= " ++ nm ++ " (ite (= bv1[1] " ++ show t ++ ") array" ++ show j ++ " array" ++ show k ++ "))"]+ ArrayFree Nothing -> []+ ArrayFree (Just sw) -> declA sw+ ArrayReset _ sw -> declA sw+ ArrayMutate j a b -> [" :assumption (= " ++ nm ++ " (store array_" ++ show j ++ " " ++ show a ++ " " ++ show b ++ "))"]+ ArrayMerge t j k -> [" :assumption (= " ++ nm ++ " (ite (= bv1[1] " ++ show t ++ ") array_" ++ show j ++ " array_" ++ show k ++ "))"]+ declA sw = let iv = nm ++ "_freeInitializer"+ in [ " :extrafuns ((" ++ iv ++ " BitVec[" ++ show at ++ "]))"+ , " :assumption (= (select " ++ nm ++ " " ++ iv ++ ") " ++ show sw ++ ")"+ ] declUI :: (String, SBVType) -> [String] declUI (i, t) = [" :extrafuns ((uninterpreted_" ++ i ++ " " ++ cvtType t ++ "))"]@@ -165,8 +167,8 @@ le0 = "(" ++ less ++ " " ++ show i ++ " " ++ mkCnst 0 ++ ")" gtl = "(" ++ leq ++ " " ++ mkCnst l ++ " " ++ show i ++ ")" cvtExp (SBVApp (Extract i j) [a]) = "(extract[" ++ show i ++ ":" ++ show j ++ "] " ++ show a ++ ")"-cvtExp (SBVApp (ArrEq i j) []) = "(ite (= array" ++ show i ++ " array" ++ show j ++") bv1[1] bv0[1])"-cvtExp (SBVApp (ArrRead i) [a]) = "(select array" ++ show i ++ " " ++ show a ++ ")"+cvtExp (SBVApp (ArrEq i j) []) = "(ite (= array_" ++ show i ++ " array_" ++ show j ++") bv1[1] bv0[1])"+cvtExp (SBVApp (ArrRead i) [a]) = "(select array_" ++ show i ++ " " ++ show a ++ ")" cvtExp (SBVApp (Uninterpreted nm) []) = "uninterpreted_" ++ nm cvtExp (SBVApp (Uninterpreted nm) args) = "(uninterpreted_" ++ nm ++ " " ++ intercalate " " (map show args) ++ ")" cvtExp inp@(SBVApp op args)
SBVUnitTest/GoldFiles/auf-1.gold view
@@ -11,7 +11,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS- ui_f :: SWord32 -> SWord64+ uninterpreted_f :: SWord32 -> SWord64 DEFINE s4 :: SWord32 = s0 + s3 s5 :: SBool = s1 == s4@@ -19,10 +19,10 @@ s7 :: SWord32 = s1 - s3 s8 :: SBool = s0 == s7 s10 :: SWord32 = if s8 then s9 else s2- s11 :: SWord64 = ui_f s10+ s11 :: SWord64 = uninterpreted_f s10 s12 :: SWord32 = s1 - s0 s14 :: SWord32 = s12 + s13- s15 :: SWord64 = ui_f s14+ s15 :: SWord64 = uninterpreted_f s14 s16 :: SBool = s11 == s15 s17 :: SBool = s6 | s16 OUTPUTS
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 0.9.7+Version: 0.9.8 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math Synopsis: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers. Description: Express properties about bit-precise Haskell programs and automatically prove@@ -56,6 +56,10 @@ Data-Files: SBVUnitTest/GoldFiles/*.gold Extra-Source-Files: INSTALL, README, COPYRIGHT +source-repository head+ type: git+ location: git://github.com/LeventErkok/sbv.git+ Flag test Description: Run the unit-test suite after build Default : False@@ -80,6 +84,7 @@ , Data.SBV.Examples.BitPrecise.BitTricks , Data.SBV.Examples.BitPrecise.Legato , Data.SBV.Examples.Polynomials.Polynomials+ , Data.SBV.Examples.PrefixSum.PrefixSum , Data.SBV.Examples.Puzzles.DogCatMouse , Data.SBV.Examples.Puzzles.MagicSquare , Data.SBV.Examples.Puzzles.NQueens@@ -113,7 +118,6 @@ , Data.SBV.Examples.CRC.GenPoly , Data.SBV.Examples.CRC.Parity , Data.SBV.Examples.CRC.USB5- , Data.SBV.Examples.PrefixSum.PrefixSum , Data.SBV.Examples.Puzzles.PowerSet , Data.SBV.Examples.Puzzles.Temperature , Data.SBV.Examples.Uninterpreted.Uninterpreted