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 @@ -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 _)) = " :: [" ++ show sz ++ (if sgn then "S" else "U") ++ "]" + show (SBV (sgn, sz) (Right _)) = " :: " ++ 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 () diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs --- a/Data/SBV/BitVectors/Model.hs +++ b/Data/SBV/BitVectors/Model.hs @@ -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 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 @@ -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 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,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 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 @@ -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 diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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