sbv 0.9.4 → 0.9.5
raw patch · 6 files changed
+117/−29 lines, 6 files
Files
- Data/SBV/BitVectors/Data.hs +9/−3
- Data/SBV/BitVectors/Model.hs +13/−0
- Data/SBV/Provers/Prover.hs +7/−7
- Data/SBV/Provers/Yices.hs +51/−2
- Data/SBV/SMT/SMT.hs +36/−16
- sbv.cabal +1/−1
Data/SBV/BitVectors/Data.hs view
@@ -38,6 +38,7 @@ import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT) import Control.Monad.Trans (MonadIO, liftIO) import Data.Bits (Bits(..))+import Data.Char (isAlpha, isAlphaNum) import Data.Int (Int8, Int16, Int32, Int64) import Data.Word (Word8, Word16, Word32, Word64) import Data.IORef (IORef, newIORef, modifyIORef, readIORef, writeIORef)@@ -336,7 +337,9 @@ -- Needed to satisfy the Num hierarchy instance Show (SBV a) where show (SBV _ (Left c)) = show c- show (SBV (sgn, sz) (Right _)) = "<SBV> :: [" ++ show sz ++ (if sgn then "S" else "U") ++ "]"+ show (SBV (sgn, sz) (Right _)) = "<symbolic> :: " ++ t+ where t | not sgn && sz == 1 = "SBool"+ | True = (if sgn then "SInt" else "SWord") ++ show sz instance Eq (SBV a) where SBV _ (Left a) == SBV _ (Left b) = a == b@@ -355,11 +358,14 @@ return ctr newUninterpreted :: State -> String -> SBVType -> IO ()-newUninterpreted st nm t = do+newUninterpreted st nm t+ | null nm || not (isAlpha (head nm)) || not (all isAlphaNum (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' -> if t /= t'- then error $ "Uninterpreted constant " ++ nm ++ " used at incompatible types\n"+ then error $ "Uninterpreted constant " ++ show nm ++ " used at incompatible types\n" ++ " Current type : " ++ show t ++ "\n" ++ " Previously used at: " ++ show t' else return ()
Data/SBV/BitVectors/Model.hs view
@@ -656,6 +656,12 @@ result st = do newUninterpreted st nm (SBVType [sgnsza]) newExpr st sgnsza $ SBVApp (Uninterpreted nm) [] +-- Forcing an argument; this is a necessary evil to make sure all the arguments+-- to an uninterpreted function are evaluated before called; the semantics of+-- such functions is necessarily strict; deviating from Haskell's+forceArg :: SW -> IO ()+forceArg (SW (b, s) n) = b `seq` s `seq` n `seq` return ()+ -- Functions of one argument instance (HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV b -> SBV a) where uninterpret nm arg0 = SBV sgnsza $ Right $ cache result@@ -663,6 +669,7 @@ sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b)) result st = do newUninterpreted st nm (SBVType [sgnszb, sgnsza]) sw0 <- sbvToSW st arg0+ mapM_ forceArg [sw0] newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0] -- Functions of two arguments@@ -674,6 +681,7 @@ result st = do newUninterpreted st nm (SBVType [sgnszc, sgnszb, sgnsza]) sw0 <- sbvToSW st arg0 sw1 <- sbvToSW st arg1+ mapM_ forceArg [sw0, sw1] newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1] -- Functions of three arguments@@ -687,6 +695,7 @@ sw0 <- sbvToSW st arg0 sw1 <- sbvToSW st arg1 sw2 <- sbvToSW st arg2+ mapM_ forceArg [sw0, sw1, sw2] newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2] -- Functions of four arguments@@ -703,6 +712,7 @@ sw1 <- sbvToSW st arg1 sw2 <- sbvToSW st arg2 sw3 <- sbvToSW st arg3+ mapM_ forceArg [sw0, sw1, sw2, sw3] newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3] -- Functions of five arguments@@ -721,6 +731,7 @@ sw2 <- sbvToSW st arg2 sw3 <- sbvToSW st arg3 sw4 <- sbvToSW st arg4+ mapM_ forceArg [sw0, sw1, sw2, sw3, sw4] newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4] -- Functions of six arguments@@ -741,6 +752,7 @@ sw3 <- sbvToSW st arg3 sw4 <- sbvToSW st arg4 sw5 <- sbvToSW st arg5+ mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5] newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5] -- Functions of seven arguments@@ -763,6 +775,7 @@ sw4 <- sbvToSW st arg4 sw5 <- sbvToSW st arg5 sw6 <- sbvToSW st arg6+ mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6] newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6] -- Uncurried functions of two arguments
Data/SBV/Provers/Prover.hs view
@@ -255,13 +255,13 @@ where loop !n nonEqConsts = do SatResult r <- callSolver nonEqConsts ("Looking for solution " ++ show n) SatResult config sbvPgm case r of- Satisfiable _ [] -> final r- Unknown _ [] -> final r- ProofError _ _ -> final r- TimeOut _ -> stop- Unsatisfiable _ -> stop- Satisfiable _ model -> add r >> loop (n+1) (model : nonEqConsts)- Unknown _ model -> add r >> loop (n+1) (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
Data/SBV/Provers/Yices.hs view
@@ -14,6 +14,7 @@ module Data.SBV.Provers.Yices(yices, timeout) where +import Control.Monad (foldM) import Data.Char (isDigit) import Data.List (sortBy, isPrefixOf) import System.Environment (getEnv)@@ -48,11 +49,18 @@ interpret :: SMTConfig -> [NamedSymVar] -> [String] -> SMTResult interpret cfg _ ("unsat":_) = Unsatisfiable cfg-interpret cfg inps ("unknown":rest) = Unknown cfg $ map (\(_, y) -> y) $ sortByNodeId $ concatMap (getCounterExample inps) rest-interpret cfg inps ("sat":rest) = Satisfiable cfg $ map (\(_, y) -> y) $ sortByNodeId $ concatMap (getCounterExample inps) rest+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 +extractMap :: [NamedSymVar] -> [String] -> SMTModel+extractMap inps solverLines =+ SMTModel { modelAssocs = map (\(_, y) -> y) $ sortByNodeId $ concatMap (getCounterExample inps) modelLines+ , modelUninterps = extractUnints unintLines+ }+ where (modelLines, unintLines) = break ("--- uninterpreted_" `isPrefixOf`) solverLines+ getCounterExample :: [NamedSymVar] -> String -> [(Int, (String, CW))] getCounterExample inps line | isComment line = []@@ -77,3 +85,44 @@ 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++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+ f = takeWhile (/= ' ') (tail tag')++getUIVal :: String -> (Int, [String]) -> String -> Maybe (Int, [String])+getUIVal f (cnt, sofar) s+ | "default: " `isPrefixOf` s+ = getDefaultVal cnt f (dropWhile (/= ' ') s) >>= \d -> return (cnt, d : sofar)+ | 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)+ _ -> 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++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)++getArg :: SExpr -> Maybe String+getArg (S_Num i) = Just (show i)+getArg _ = Nothing
Data/SBV/SMT/SMT.hs view
@@ -47,16 +47,23 @@ , engine :: SMTEngine -- ^ The solver engine, responsible for interpreting solver output } +-- | A model, as returned by a solver+data SMTModel = SMTModel {+ modelAssocs :: [(String, CW)]+ , modelUninterps :: [(String, [String])] -- very crude!+ }+ deriving Show+ -- | The result of an SMT solver call. Each constructor is tagged with -- the 'SMTConfig' that created it so that further tools can inspect it -- and build layers of results, if needed. For ordinary uses of the library, -- this type should not be needed, instead use the accessor functions on -- it. (Custom Show instances and model extractors.)-data SMTResult = Unsatisfiable SMTConfig -- ^ Unsatisfiable- | Satisfiable SMTConfig [(String, CW)] -- ^ Satisfiable with model- | Unknown SMTConfig [(String, CW)] -- ^ Prover returned unknown, with a potential (possibly bogus) model- | ProofError SMTConfig [String] -- ^ Prover errored out- | TimeOut SMTConfig -- ^ Computation timed out (see the 'timeout' combinator)+data SMTResult = Unsatisfiable SMTConfig -- ^ Unsatisfiable+ | Satisfiable SMTConfig SMTModel -- ^ Satisfiable with model+ | Unknown SMTConfig SMTModel -- ^ Prover returned unknown, with a potential (possibly bogus) model+ | ProofError SMTConfig [String] -- ^ Prover errored out+ | TimeOut SMTConfig -- ^ Computation timed out (see the 'timeout' combinator) resultConfig :: SMTResult -> SMTConfig resultConfig (Unsatisfiable c) = c@@ -72,6 +79,9 @@ rnf (ProofError _ xs) = rnf xs `seq` () rnf (TimeOut _) = () +instance NFData SMTModel where+ rnf (SMTModel assocs unints) = rnf assocs `seq` rnf unints `seq` ()+ -- | A 'prove' call results in a 'ThmResult' newtype ThmResult = ThmResult SMTResult @@ -201,7 +211,7 @@ getModel (Unknown _ _) = error "Impossible! Backend solver returned unknown for Bit-vector problem!" getModel (ProofError _ s) = error $ unlines $ "An error happened: " : s getModel (TimeOut _) = error $ "Timeout"-getModel (Satisfiable _ m) = case parseCWs [c | (_, c) <- m] of+getModel (Satisfiable _ m) = case parseCWs [c | (_, c) <- modelAssocs m] of Just (x, []) -> x Just (_, ys) -> error $ "SBV.getModel: Partially constructed model; remaining elements: " ++ show ys Nothing -> error $ "SBV.getModel: Cannot construct a model from: " ++ show m@@ -217,22 +227,32 @@ showSMTResult :: String -> String -> String -> String -> String -> SMTResult -> String showSMTResult unsatMsg unkMsg unkMsgModel satMsg satMsgModel result = case result of- Unsatisfiable _ -> unsatMsg- Satisfiable _ [] -> satMsg- Satisfiable _ m -> satMsgModel ++ intercalate "\n" (map (shM cfg) m)- Unknown _ [] -> unkMsg- Unknown _ m -> unkMsgModel ++ intercalate "\n" (map (shM 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"+ 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" where cfg = resultConfig result -shM :: SMTConfig -> (String, CW) -> String-shM cfg (s, v) = " " ++ s ++ " = " ++ sh (printBase cfg) v+shCW :: SMTConfig -> CW -> String+shCW cfg v = sh (printBase cfg) v where sh 2 = binS sh 10 = show sh 16 = hexS sh n = \w -> show w ++ " -- Ignoring unsupported printBase " ++ show n ++ ", use 2, 10, or 16."++shM :: SMTConfig -> (String, CW) -> String+shM cfg (s, v) = " " ++ s ++ " = " ++ shCW cfg v++-- very crude..+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 pipeProcess :: String -> String -> [String] -> String -> IO (Either String [String]) pipeProcess nm execName opts script = do
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 0.9.4+Version: 0.9.5 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math Synopsis: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers. Description: Adds support for symbolic bit vectors, allowing formal models of bit-precise