diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs --- a/Data/SBV/BitVectors/Data.hs +++ b/Data/SBV/BitVectors/Data.hs @@ -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: +-- +-- * 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 diff --git a/Data/SBV/Examples/PrefixSum/PrefixSum.hs b/Data/SBV/Examples/PrefixSum/PrefixSum.hs --- a/Data/SBV/Examples/PrefixSum/PrefixSum.hs +++ b/Data/SBV/Examples/PrefixSum/PrefixSum.hs @@ -8,7 +8,9 @@ -- Portability : portable -- -- The PrefixSum algorithm over power-lists and proof of --- the Fischer-Ladner implementation +-- the Ladner-Fischer implementation. +-- See +-- and . ----------------------------------------------------------------------------- {-# 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: . +-- 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 +-- or pg. 16 of . +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) diff --git a/Data/SBV/Examples/Uninterpreted/Function.hs b/Data/SBV/Examples/Uninterpreted/Function.hs --- a/Data/SBV/Examples/Uninterpreted/Function.hs +++ b/Data/SBV/Examples/Uninterpreted/Function.hs @@ -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; diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -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 diff --git a/Data/SBV/Provers/SExpr.hs b/Data/SBV/Provers/SExpr.hs --- a/Data/SBV/Provers/SExpr.hs +++ b/Data/SBV/Provers/SExpr.hs @@ -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" diff --git a/Data/SBV/Provers/Yices.hs b/Data/SBV/Provers/Yices.hs --- a/Data/SBV/Provers/Yices.hs +++ b/Data/SBV/Provers/Yices.hs @@ -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 ' ') diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -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 diff --git a/Data/SBV/SMT/SMTLib.hs b/Data/SBV/SMT/SMTLib.hs --- a/Data/SBV/SMT/SMTLib.hs +++ b/Data/SBV/SMT/SMTLib.hs @@ -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) diff --git a/SBVUnitTest/GoldFiles/auf-1.gold b/SBVUnitTest/GoldFiles/auf-1.gold --- a/SBVUnitTest/GoldFiles/auf-1.gold +++ b/SBVUnitTest/GoldFiles/auf-1.gold @@ -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 diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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