diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,10 +1,18 @@ * Hackage: * GitHub: -* Latest Hackage released version: 0.1, 2015-12-06 +* Latest Hackage released version: 0.1, 2015-12-21 +### Version 0.2, 2015-12-21 + + * Further fleshing of internals + * Support for case-expressions + * Support for uninterpreted types/functions + * Lots of test cases, refactoring. + ### Version 0.1, 2015-12-06 - * Basic functionality. Initial design exploration. The plugin - is mostly functional, but there are rough edges around - the details. Please report any issues you might find! + * Basic functionality. Initial design exploration. + * The plugin functional on base values, but there + are a lot of rough edges around the details. + Please report any issues you might find! diff --git a/Data/SBV/Plugin.hs b/Data/SBV/Plugin.hs --- a/Data/SBV/Plugin.hs +++ b/Data/SBV/Plugin.hs @@ -9,15 +9,14 @@ -- (The sbvPlugin is hosted at . -- Comments, bug reports, and patches are always welcome.) -- --- SBVPlugin: A GHC Plugin for SBV, SMT Based Verification +-- == SBVPlugin: A GHC Plugin for SBV, SMT Based Verification -- -- is a library for express properties about Haskell programs and -- automatically proving them using SMT solvers. The SBVPlugin allows -- simple annotations on Haskell functions to prove them directly during -- GHC compilation time. -- --- Consider the following simple program: --- +-- === /Example/ -- > {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} -- > -- > module Test where @@ -28,10 +27,8 @@ -- > test :: Integer -> Integer -> Bool -- > test x y = x + y >= x - y -- --- We have: +-- When compiled via GHC or loaded into GHCi, we get: -- --- > $ ghc -c Test.hs --- > -- > [SBV] Test.hs:9:1-4 Proving "test", using Z3. -- > [Z3] Falsifiable. Counter-example: -- > x = 0 :: Integer @@ -43,9 +40,24 @@ -- -- > {-# ANN test theorem {options = [IgnoreFailure]} #-} -- +-- === /Using the plugin from GHCi/ -- The plugin should work from GHCi with no changes. Note that when run from GHCi, the plugin will --- behave as if the /IgnoreFailure/ option is given on all annotations, so that failures do not stop +-- behave as if the @IgnoreFailure@ option is given on all annotations, so that failures do not stop -- the load process. +-- +-- === /Plugin order/ +-- By default, sbvPlugin runs before GHCs optimizer passes. While the order of the run should +-- not matter in general, the simplifier can rearrange the core in various ways that can have +-- an impact on the verification conditions generated by the plugin. As an experiment, you can +-- pass the argument @runLast@ to the plugin to see if it makes any difference, using the following +-- argument to GHC: +-- +-- @ +-- -fplugin-opt Data.SBV.Plugin:runLast +-- @ +-- +-- Please report if you find any crucial differences when the plugin is run first or last, especially +-- if the outputs are different. --------------------------------------------------------------------------------- module Data.SBV.Plugin( -- * Entry point diff --git a/Data/SBV/Plugin/Analyze.hs b/Data/SBV/Plugin/Analyze.hs --- a/Data/SBV/Plugin/Analyze.hs +++ b/Data/SBV/Plugin/Analyze.hs @@ -9,8 +9,7 @@ -- Walk the GHC Core, proving theorems/checking safety as they are found ----------------------------------------------------------------------------- -{-# LANGUAGE NamedFieldPuns #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE NamedFieldPuns #-} module Data.SBV.Plugin.Analyze (analyzeBind) where @@ -21,10 +20,10 @@ import Data.IORef -import Data.Char (isAlpha, isAlphaNum) -import Data.List (intercalate, partition, nub, sortBy) -import Data.Maybe (isJust, listToMaybe) -import Data.Ord (comparing) +import Data.Char (isAlpha, isAlphaNum, toLower, isUpper) +import Data.List (intercalate, partition, nub, sort, sortBy, isPrefixOf) +import Data.Maybe (listToMaybe, fromMaybe) +import Data.Ord (comparing) import qualified Data.Map as M @@ -39,14 +38,13 @@ -- | Dispatch the analyzer over bindings analyzeBind :: Config -> CoreBind -> CoreM () -analyzeBind cfg@Config{sbvAnnotation} = go +analyzeBind cfg@Config{sbvAnnotation, cfgEnv} = go where go (NonRec b e) = bind (b, e) go (Rec binds) = mapM_ bind binds bind (b, e) = mapM_ work (sbvAnnotation b) where work (SBV opts) - | Just s <- hasSkip opts = liftIO $ putStrLn $ "[SBV] " ++ showSpan cfg b topLoc ++ " Skipping " ++ show (showSDoc (dflags cfg) (ppr b)) ++ ": " ++ s - | Safety `elem` opts = error "SBV: Safety pragma is not implemented yet" + | Just s <- hasSkip opts = liftIO $ putStrLn $ "[SBV] " ++ showSpan cfg b topLoc ++ " Skipping " ++ show (showSDoc (flags cfgEnv) (ppr b)) ++ ": " ++ s | Uninterpret `elem` opts = return () | True = liftIO $ prove cfg opts b topLoc e hasSkip opts = listToMaybe [s | Skip s <- opts] @@ -67,16 +65,9 @@ bad e = do print e return False -instance Outputable S.Kind where - ppr = text . show - -instance Outputable Val where - ppr (Base s) = text (show s) - ppr (Func k _) = text ("Func<" ++ show k ++ ">") - -- | Returns True if proof went thru proveIt :: Config -> [SBVOption] -> (SrcSpan, Var) -> CoreExpr -> IO Bool -proveIt cfg@Config{sbvAnnotation} opts (topLoc, topBind) topExpr = do +proveIt cfg@Config{cfgEnv, sbvAnnotation} opts (topLoc, topBind) topExpr = do solverConfigs <- pickSolvers opts let verbose = Verbose `elem` opts qCheck = QuickCheck `elem` opts @@ -92,11 +83,8 @@ xs -> intercalate ", " (map show (init xs)) ++ ", and " ++ show (last xs) putStrLn $ "\n" ++ loc ++ (if qCheck then " QuickChecking " else " Proving ") ++ show (sh topBind) ++ slvrTag (finalResult, finalUninterps) <- do - rUninterps <- newIORef [] - rUnms <- newIORef [] - rUItys <- newIORef [] - finalResult <- runProver (res rUninterps rUnms rUItys) - finalUninterps <- readIORef rUninterps + finalResult <- runProver (res cfgEnv) + finalUninterps <- readIORef (rUninterpreted cfgEnv) return (finalResult, finalUninterps) case finalResult of Right (solver, sres@(S.ThmResult smtRes)) -> do @@ -109,13 +97,13 @@ putStr $ "[" ++ show solver ++ "] " print sres - -- If proof failed and there are uninterpreted functions, print a warning: - let unintFuns = [p | (p@(_, t), _) <- nub $ sortBy (comparing (fst . fst)) finalUninterps, isJust (splitFunTy_maybe t)] - unless (success || null unintFuns) $ do + -- If proof failed and there are uninterpreted values, print a warning; except for "uninteresting" types + let unintVals = filter ((`notElem` uninteresting cfgEnv) . snd) $ nub $ sortBy (comparing fst) [vt | (vt, _) <- finalUninterps] + unless (success || null unintVals) $ do let plu | length finalUninterps > 1 = "s:" | True = ":" - shUI (e, t) = (showSDoc (dflags cfg) (ppr (getSrcSpan e)), sh e, sh t) - ls = map shUI unintFuns + shUI (e, t) = (showSDoc (flags cfgEnv) (ppr (getSrcSpan e)), sh e, sh t) + ls = map shUI unintVals len1 = maximum (0 : [length s | (s, _, _) <- ls]) len2 = maximum (0 : [length s | (_, s, _) <- ls]) pad n s = take n (s ++ repeat ' ') @@ -126,21 +114,13 @@ return success Left success -> return success - where res uis unms uitys = do - v <- runReaderT (symEval topExpr) Env{ curLoc = topLoc - , flags = dflags cfg - , rUninterpreted = uis - , rUsedNames = unms - , rUITypes = uitys - , machWordSize = wordSize cfg - , envMap = knownFuns cfg - , baseTCs = knownTCs cfg - , specMap = knownSpecials cfg - , coreMap = allBinds cfg - } + where debug = Debug `elem` opts + + res initEnv = do + v <- runReaderT (symEval topExpr) initEnv{curLoc = topLoc} case v of Base r -> return r - Func{} -> error "Impossible happened. Final result reduced to a non-base value!" + r -> error $ "Impossible happened. Final result reduced to a non-base value: " ++ showSDocUnsafe (ppr r) die :: SrcSpan -> String -> [String] -> a die loc w es = error $ concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es @@ -152,41 +132,103 @@ tbd w ws = do Env{curLoc} <- ask die curLoc w ws - sh o = showSDoc (dflags cfg) (ppr o) + sh o = showSDoc (flags cfgEnv) (ppr o) -- Given an alleged theorem, first establish it has the right type, and -- then go ahead and evaluate it symbolicly after applying it to sufficient -- number of symbolic arguments symEval :: CoreExpr -> Eval Val - symEval e = do let (bs, body) = collectBinders e - ats <- mapM (\b -> getBaseType (getSrcSpan b) (varType b) >>= \bt -> return (b, bt)) bs - let mkVar ((b, k), mbN) = do v <- S.svMkSymVar Nothing k (mbN `mplus` Just (sh b)) - return ((b, k), Base v) - sArgs <- mapM (lift . mkVar) (zip ats (concat [map Just ns | Names ns <- opts] ++ repeat Nothing)) - local (\env -> env{envMap = foldr (uncurry M.insert) (envMap env) sArgs}) (go body) + symEval e = do let (bs, body) = collectBinders (pushLetLambda e) + Env{curLoc} <- ask + let mbListSize = listToMaybe [n | ListSize n <- opts] + bodyType <- getType curLoc (exprType body) + -- Figure out if there were some unmentioned variables; happens if the top + -- level wasn't fully saturated. + let (extraArgs, finalType) = walk bodyType [] + where walk (KFun d c) sofar = walk c (d:sofar) + walk k sofar = (reverse sofar, k) + + case finalType of + KBase S.KBool -> do -- First collect the named arguments: + argKs <- mapM (\b -> getType (getSrcSpan b) (varType b) >>= \bt -> return (b, bt)) bs + let mkVar ((b, k), mbN) = do sv <- mkSym mbListSize curLoc (Just (idType b)) k (mbN `mplus` Just (sh b)) + return ((b, k), sv) + bArgs <- mapM (lift . mkVar) (zip argKs (concat [map Just ns | Names ns <- opts] ++ repeat Nothing)) + + -- Go ahead and run the body symbolically; on bArgs + bRes <- local (\env -> env{envMap = foldr (uncurry M.insert) (envMap env) bArgs}) (go body) + + -- If there are extraArgs; then create symbolics and apply to the result: + let feed [] sres = return sres + feed (k:ks) (Func _ f) = do sv <- lift $ mkSym mbListSize curLoc Nothing k Nothing + f sv >>= feed ks + feed ks v = error $ "Impossible! Left with extra args to apply on a non-function: " ++ sh (ks, v) + + feed extraArgs bRes + + _ -> die curLoc "Non-boolean property declaration" (concat [ ["Found : " ++ sh (exprType e)] + , ["Returning: " ++ sh (exprType body) | not (null bs)] + , ["Expected : Bool" ++ if null bs then "" else " result"] + ]) + where -- Sometimes the core has a wrapper let, floated out on top. Float that in. + pushLetLambda (Let b (Lam x bd)) = Lam x (pushLetLambda (Let b bd)) + pushLetLambda o = o + + -- Create a symbolic variable: + mkSym :: Maybe Int -> SrcSpan -> Maybe Type -> SKind -> Maybe String -> S.Symbolic Val + mkSym mbLs curLoc mbBType = sym + where tinfo k = case mbBType of + Nothing -> "Kind: " ++ sh k + Just t -> "Type: " ++ sh t + + sym (KBase k) nm = do v <- S.svMkSymVar Nothing k nm + return (Base v) + + sym (KTup ks) nm = do let ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. length ks] + vs <- zipWithM sym ks ns + return $ Tup vs + + sym (KLst ks) nm = do let ls = fromMaybe bad mbLs + bad = die curLoc "List-argument found, with no size info" + [ "Name: " ++ fromMaybe "anonymous" nm + , tinfo (KLst ks) + , "Hint: Use the \"ListSize\" annotation" + ] + ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. ls] + vs <- zipWithM sym (replicate ls ks) ns + return (Lst vs) + + sym k nm = die curLoc "Unsupported symbolic input" [ "Name: " ++ show nm + , tinfo k + ] + isUninterpretedBinding :: Var -> Bool isUninterpretedBinding v = any (Uninterpret `elem`) [opt | SBV opt <- sbvAnnotation v] go :: CoreExpr -> Eval Val - go e = tgo (exprType e) e + go (Tick t e) = local (\envMap -> envMap{curLoc = tickSpan t (curLoc envMap)}) $ go e + go e = tgo (exprType e) e + debugTrace s w + | debug = trace ("--> " ++ s) w + | True = w + -- Main symbolic evaluator: tgo :: Type -> CoreExpr -> Eval Val - -- tgo t e | trace ("--> " ++ show (sh (e, t))) False = undefined + tgo t e | debugTrace (sh (e, t)) False = undefined - tgo t (Var v) = do Env{envMap, coreMap, specMap} <- ask - k <- getBaseType (getSrcSpan v) t + tgo t (Var v) = do Env{envMap, coreMap} <- ask + k <- getType (getSrcSpan v) t case (v, k) `M.lookup` envMap of Just b -> return b Nothing -> case v `M.lookup` coreMap of Just b -> if isUninterpretedBinding v then uninterpret t v else go b - Nothing -> case v `M.lookup` specMap of - Just b -> return b - Nothing -> uninterpret t v + Nothing -> debugTrace ("Uninterpreting: " ++ sh (v, k, nub $ sort $ map (fst . fst) (M.toList envMap))) + $ uninterpret t v tgo t e@(Lit l) = do Env{machWordSize} <- ask case l of @@ -200,62 +242,94 @@ MachWord64 i -> return $ Base $ S.svInteger (S.KBounded False 64 ) i MachFloat f -> return $ Base $ S.svFloat (fromRational f) MachDouble d -> return $ Base $ S.svDouble (fromRational d) - LitInteger i it -> do k <- getBaseType noSrcSpan it - return $ Base $ S.svInteger k i + LitInteger i it -> do k <- getType noSrcSpan it + case k of + KBase b -> return $ Base $ S.svInteger b i + _ -> error $ "Impossible: The type for literal resulted in non base kind: " ++ sh (e, k) where unint = do Env{flags} <- ask - k <- getBaseType noSrcSpan t - nm <- mkValidName "lit" (showSDoc flags (ppr e)) - return $ Base $ S.svUninterpreted k nm Nothing [] + k <- getType noSrcSpan t + nm <- mkValidName (showSDoc flags (ppr e)) + case k of + KBase b -> return $ Base $ S.svUninterpreted b nm Nothing [] + _ -> error $ "Impossible: The type for literal resulted in non base kind: " ++ sh (e, k) - tgo tFun (App (App (Var v) (Type t)) (Var dict)) - | isReallyADictionary dict = do Env{envMap} <- ask - k <- getBaseType (getSrcSpan v) t - case (v, k) `M.lookup` envMap of - Just b -> return b - _ -> uninterpret tFun v - tgo t (App a (Type _)) - = tgo t a + tgo tFun orig@App{} = do + reduced <- betaReduce orig - tgo _ (App f e) - = do func <- go f - arg <- go e - let ok (S.KUserSort s1 _) (S.KUserSort s2 _) = s1 == s2 - ok k1 k2 = k1 == k2 - case (func, arg) of - (Func (k, _) sf, Base sv) | S.kindOf sv `ok` k -> sf sv - (_, Func{}) -> tbd "Unsupported higher-order application" [sh f, sh e] - _ -> error $ "[SBV] Impossible happened. Got an application with mismatched types: " - ++ sh [(f, func), (e, arg)] + Env{specials} <- ask + -- handle specials: Equality, tuples, and lists + let isEq (App (App (Var v) (Type _)) dict) | isReallyADictionary dict, Just f <- isEquality specials v = Just f + isEq _ = Nothing + + isTup (Var v) = isTuple specials v + isTup (App f (Type _)) = isTup f + isTup _ = Nothing + + isLst (Var v) = isList specials v + isLst (App f (Type _)) = isLst f + isLst _ = Nothing + + isSpecial e = isEq e `mplus` isTup e `mplus` isLst e + + case isSpecial reduced of + Just f -> debugTrace ("Special located: " ++ sh (orig, f)) $ return f + Nothing -> case reduced of + App (App (Var v) (Type t)) dict | isReallyADictionary dict -> do + Env{envMap} <- ask + k <- getType (getSrcSpan v) t + case (v, k) `M.lookup` envMap of + Just b -> return b + Nothing -> do Env{coreMap} <- ask + case v `M.lookup` coreMap of + Just e -> tgo tFun (App (App e (Type t)) dict) + Nothing -> tgo tFun (Var v) + + App (Var v) (Type t) -> do + Env{coreMap} <- ask + case v `M.lookup` coreMap of + Just e -> tgo tFun (App e (Type t)) + Nothing -> tgo tFun (Var v) + + App (Let (Rec bs) f) a -> go (Let (Rec bs) (App f a)) + + App f e -> do + func <- go f + arg <- go e + case (func, arg) of + (Func _ sf, sv) -> sf sv + _ -> error $ "[SBV] Impossible happened. Got an application with mismatched types: " ++ sh [(f, func), (e, arg)] + + e -> go e + tgo _ (Lam b body) = do - k <- getBaseType (getSrcSpan b) (varType b) - return $ Func (k, Just (sh b)) $ \s -> local (\env -> env{envMap = M.insert (b, k) (Base s) (envMap env)}) (go body) + k <- getType (getSrcSpan b) (varType b) + Env{envMap} <- ask + return $ Func (Just (sh b)) $ \s -> local (\env -> env{envMap = M.insert (b, k) s envMap}) (go body) - tgo _ (Let (NonRec b e) body) = do - k <- getBaseType (getSrcSpan b) (varType b) - v <- go e - local (\env -> env{envMap = M.insert (b, k) v (envMap env)}) (go body) + tgo _ (Let (NonRec b e) body) = local (\env -> env{coreMap = M.insert b e (coreMap env)}) (go body) - tgo _ e@(Let _ _) - = tbd "Unsupported let-binding with a recursive binder" [sh e] + tgo _ (Let (Rec bs) body) = local (\env -> env{coreMap = foldr (uncurry M.insert) (coreMap env) bs}) (go body) -- Case expressions. We take advantage of the core-invariant that each case alternative -- is exhaustive; and DEFAULT (if present) is the first alternative. We turn it into a -- simple if-then-else chain with the last element on the DEFAULT, or whatever comes last. - tgo _ e@(Case ce _b _t alts) + tgo _ e@(Case ce caseBinder caseType alts) = do sce <- go ce let isDefault (DEFAULT, _, _) = True isDefault _ = False - (nonDefs, defs) = partition isDefault alts - walk [(_, _, rhs)] = go rhs - walk ((p, _, rhs) : rest) = case sce of - Base a -> do mr <- match a p - case mr of - Just m -> choose m (go rhs) (walk rest) - Nothing -> caseTooComplicated "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs] - _ -> caseTooComplicated "with-non-base-scrutinee" [] - walk [] = caseTooComplicated "with-non-exhaustive-match" [] -- can't really happen - walk (nonDefs ++ defs) + (defs, nonDefs) = partition isDefault alts + walk ((p, bs, rhs) : rest) = + do mr <- match (bindSpan caseBinder) sce p bs + case mr of + Just (m, bs') -> do let result = local (\env -> env{envMap = foldr (uncurry M.insert) (envMap env) bs'}) $ go rhs + if null rest + then result + else choose m result (walk rest) + Nothing -> caseTooComplicated "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs] + walk [] = caseTooComplicated "with-non-exhaustive-match" [] -- can't really happen + k <- getType (getSrcSpan caseBinder) caseType + local (\env -> env{envMap = M.insert (caseBinder, k) sce (envMap env)}) $ walk (nonDefs ++ defs) where caseTooComplicated w [] = tbd ("Unsupported case-expression (" ++ w ++ ")") [sh e] caseTooComplicated w xs = tbd ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs choose t tb fb = case S.svAsBool t of @@ -266,102 +340,159 @@ _ -> caseTooComplicated "with-non-base-alternatives" [] Just True -> tb Just False -> fb - match :: S.SVal -> AltCon -> Eval (Maybe S.SVal) - match a c = case c of - DEFAULT -> return $ Just S.svTrue - LitAlt l -> do le <- go (Lit l) - case le of - Base b -> return $ Just $ a `S.svEqual` b - Func{} -> return Nothing - DataAlt dc -> do Env{specMap} <- ask - case dataConWorkId dc `M.lookup` specMap of - Just (Base b) -> return $ Just $ a `S.svEqual` b - _ -> return Nothing + match :: SrcSpan -> Val -> AltCon -> [Var] -> Eval (Maybe (S.SVal, [((Var, SKind), Val)])) + match sp a c bs = case c of + DEFAULT -> return $ Just (S.svTrue, []) + LitAlt l -> do b <- go (Lit l) + return $ Just (a `eqVal` b, []) + DataAlt dc -> do Env{envMap, destMap} <- ask + k <- getType sp (dataConRepType dc) + let wid = dataConWorkId dc + -- The following lookup in env essentially gets True/False constructors (or other base-values if we add them) + case (wid, k) `M.lookup` envMap of + Just (Base b) -> return $ Just (a `eqVal` Base b, []) + _ -> case wid `M.lookup` destMap of + Nothing -> return Nothing + Just f -> do bts <- mapM (\b -> getType (getSrcSpan b) (varType b) >>= \bt -> return (b, bt)) bs + return $ Just (f a bts) - tgo t (Cast e _) - = tgo t e + tgo t (Cast e c) + = debugTrace ("Going thru a Cast: " ++ sh c) $ tgo t e - tgo _ (Tick t e) - = local (\envMap -> envMap{curLoc = tickSpan t (curLoc envMap)}) $ go e + tgo _ (Tick t e) = local (\envMap -> envMap{curLoc = tickSpan t (curLoc envMap)}) $ go e - tgo _ e@(Type{}) - = tbd "Unsupported type-expression" [sh e] + tgo _ (Type t) + = do Env{curLoc} <- ask + k <- getType curLoc t + return (Typ k) - tgo _ e@(Coercion{}) + tgo _ e@Coercion{} = tbd "Unsupported coercion-expression" [sh e] + isBetaReducable (Type _) = True + isBetaReducable e = isReallyADictionary e + + betaReduce :: CoreExpr -> Eval CoreExpr + betaReduce orig@(App f a) = do + rf <- betaReduce f + if not (isBetaReducable a) + then return (App rf a) + else do let chaseVars :: CoreExpr -> Eval CoreExpr + chaseVars (Var x) = do Env{coreMap} <- ask + case x `M.lookup` coreMap of + Nothing -> return (Var x) + Just b -> chaseVars b + chaseVars (Tick _ x) = chaseVars x + chaseVars x = return x + func <- chaseVars rf + case func of + Lam x b -> do reduced <- betaReduce $ substExpr (ppr "SBV.betaReduce") (extendSubstList emptySubst [(x, a)]) b + () <- debugTrace ("Beta reduce:\n" ++ sh (orig, reduced)) $ return () + return reduced + _ -> return (App rf a) + betaReduce e = return e + +-- | Is this really a dictionary in disguise? This is a terrible hack, and the ice is thin here. But it seems to work. +-- TODO: Figure out if there's a better way of doing this. Note that this function really does get applications, when +-- those dictionaries are parameterized by others. Think of the case where "Eq [a]" dictionary depends on "Eq a", for +-- instance. In these cases, GHC to produces applications. +isReallyADictionary :: CoreExpr -> Bool +isReallyADictionary (App f _) = isReallyADictionary f +isReallyADictionary (Var v) = "$" `isPrefixOf` unpackFS (occNameFS (occName (varName v))) +isReallyADictionary _ = False + -- | Uninterpret an expression uninterpret :: Type -> Var -> Eval Val uninterpret t v = do - let (args, res) = splitFunTys t - sp = getSrcSpan v - argKs <- mapM (getBaseType sp) args - resK <- getBaseType sp res - Env{flags, rUninterpreted} <- ask - uis <- liftIO $ readIORef rUninterpreted - nm <- case (v, t) `lookup` uis of - Just nm -> return nm - Nothing -> do nm <- mkValidName "expr" $ showSDoc flags (ppr v) - liftIO $ modifyIORef rUninterpreted (((v, t), nm) :) - return nm - return $ walk argKs (nm, resK) [] - where walk [] (nm, k) args = Base $ S.svUninterpreted k nm Nothing (reverse args) - walk (a:as) nmk args = Func (a, Nothing) $ \p -> return (walk as nmk (p:args)) + Env{rUninterpreted, flags} <- ask + prevUninterpreted <- liftIO $ readIORef rUninterpreted + case (v, t) `lookup` prevUninterpreted of + Just (_, val) -> return val + Nothing -> do let (tvs, t') = splitForAllTys t + (args, res) = splitFunTys t' + sp = getSrcSpan v + argKs <- mapM (getType sp) args + resK <- getType sp res + nm <- mkValidName $ showSDoc flags (ppr v) + let fVal = wrap tvs $ walk argKs (nm, resK) [] + liftIO $ modifyIORef rUninterpreted (((v, t), (nm, fVal)) :) + return fVal + where walk :: [SKind] -> (String, SKind) -> [S.SVal] -> Val + walk [] (nm, k) args = case k of + KBase b -> Base $ S.svUninterpreted b nm Nothing (reverse args) + _ -> error $ "Not yet supported uninterpreted type with non-base type: " ++ showSDocUnsafe (ppr k) + walk (_:as) nmk args = Func Nothing $ \a -> case a of + Base p -> return (walk as nmk (p:args)) + _ -> return (walk as nmk args) + wrap [] f = f + wrap (_:ts) f = Func Nothing $ \(Typ _) -> return (wrap ts f) -- not every name is good, sigh -mkValidName :: String -> String -> Eval String -mkValidName origin origName = +mkValidName :: String -> Eval String +mkValidName name = do Env{rUsedNames} <- ask usedNames <- liftIO $ readIORef rUsedNames - let name = if null origName || origName `elem` S.smtLibReservedNames - then "sbvPlugin_" ++ origin ++ "_" ++ origName - else origName - nm = genSym usedNames name - liftIO $ modifyIORef rUsedNames (nm :) - return $ escape nm + let unm = unSMT $ genSym usedNames name + liftIO $ modifyIORef rUsedNames (unm :) + return $ escape unm where genSym bad nm | nm `elem` bad = head [nm' | i <- [(0::Int) ..], let nm' = nm ++ "_" ++ show i, nm' `notElem` bad] | True = nm - escape nm - | isAlpha (head nm) && all isGood (tail nm) = nm - | True = "|" ++ map tr nm ++ "|" + unSMT nm + | map toLower nm `elem` S.smtLibReservedNames + = if not (null nm) && isUpper (head nm) + then "sbv" ++ nm + else "sbv_" ++ nm + | True + = nm + escape nm | isAlpha (head nm) && all isGood (tail nm) = nm + | True = "|" ++ map tr nm ++ "|" isGood c = isAlphaNum c || c == '_' tr '|' = '_' tr '\\' = '_' tr c = c --- | Is this variable really a dictionary? -isReallyADictionary :: Var -> Bool -isReallyADictionary v = case classifyPredType (varType v) of - ClassPred{} -> True - EqPred{} -> True - TuplePred{} -> True - IrredPred{} -> False +-- | Convert a Core type to an SBV Type, retaining functions and tuples +getType :: SrcSpan -> Type -> Eval SKind +getType sp typ = do let (tvs, typ') = splitForAllTys typ + (args, res) = splitFunTys typ' + argKs <- mapM (getType sp) args + resK <- getComposite res + return $ wrap tvs $ foldr KFun resK argKs + where wrap ts f = foldr (KFun . mkUserSort) f ts + mkUserSort v = KBase (S.KUserSort (show (occNameFS (occName (varName v)))) (Left "sbvPlugin")) --- | Convert a Core type to an SBV kind, if known --- Otherwise, create an uninterpreted kind, and return that. -getBaseType :: SrcSpan -> Type -> Eval S.Kind -getBaseType sp t = do - Env{baseTCs} <- ask - case grabTCs (splitTyConApp_maybe t) of - Just k -> case k `M.lookup` baseTCs of - Just knd -> return knd - Nothing -> unknown - _ -> unknown - where -- allow one level of nesting - grabTCs Nothing = Nothing - grabTCs (Just (top, ts)) = do as <- walk ts [] - return (top, as) - walk [] sofar = Just $ reverse sofar - walk (a:as) sofar = case splitTyConApp_maybe a of - Just (ac, []) -> walk as (ac:sofar) - _ -> Nothing - -- Check if we uninterpreted this before; if so, return it, otherwise create a new one - unknown = do Env{flags, rUITypes} <- ask - uiTypes <- liftIO $ readIORef rUITypes - case t `lookup` uiTypes of - Just k -> return k - Nothing -> do nm <- mkValidName "type" $ showSDoc flags (ppr t) - let k = S.KUserSort nm $ Left $ "originating from sbvPlugin: " ++ showSDoc flags (ppr sp) - liftIO $ modifyIORef rUITypes ((t, k) :) - return k + -- | Extract tuples, lists, or base kinds + getComposite :: Type -> Eval SKind + getComposite t = case splitTyConApp_maybe t of + Just (k, ts) | isTupleTyCon k -> KTup `fmap` mapM (getType sp) ts + Just (k, [a]) | listTyCon == k -> KLst `fmap` getType sp a + _ -> KBase `fmap` getBaseType t + + -- | Convert a Core type to an SBV kind, if known + -- Otherwise, create an uninterpreted kind, and return that. + getBaseType :: Type -> Eval S.Kind + getBaseType bt = do + Env{tcMap} <- ask + case grabTCs (splitTyConApp_maybe bt) of + Just k -> case k `M.lookup` tcMap of + Just knd -> return knd + Nothing -> unknown + _ -> unknown + where -- allow one level of nesting, essentially to support Haskell's 'Ratio Integer' to map to 'SReal' + grabTCs Nothing = Nothing + grabTCs (Just (top, ts)) = do as <- walk ts [] + return (top, as) + walk [] sofar = Just $ reverse sofar + walk (a:as) sofar = case splitTyConApp_maybe a of + Just (ac, []) -> walk as (ac:sofar) + _ -> Nothing + -- Check if we uninterpreted this before; if so, return it, otherwise create a new one + unknown = do Env{flags, rUITypes} <- ask + uiTypes <- liftIO $ readIORef rUITypes + case bt `lookup` uiTypes of + Just k -> return k + Nothing -> do nm <- mkValidName $ showSDoc flags (ppr bt) + let k = S.KUserSort nm $ Left $ "originating from sbvPlugin: " ++ showSDoc flags (ppr sp) + liftIO $ modifyIORef rUITypes ((bt, k) :) + return k diff --git a/Data/SBV/Plugin/Common.hs b/Data/SBV/Plugin/Common.hs --- a/Data/SBV/Plugin/Common.hs +++ b/Data/SBV/Plugin/Common.hs @@ -9,6 +9,9 @@ -- Common data-structures/utilities ----------------------------------------------------------------------------- +{-# LANGUAGE NamedFieldPuns #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + module Data.SBV.Plugin.Common where import Control.Monad.Reader @@ -26,32 +29,36 @@ import Data.SBV.Plugin.Data +-- | Certain "very-polymorphic" things are just special +data Specials = Specials { isEquality :: Var -> Maybe Val + , isTuple :: Var -> Maybe Val + , isList :: Var -> Maybe Val + } + -- | Interpreter environment data Env = Env { curLoc :: SrcSpan , flags :: DynFlags , machWordSize :: Int - , rUninterpreted :: IORef [((Var, Type), String)] + , uninteresting :: [Type] + , rUninterpreted :: IORef [((Var, Type), (String, Val))] , rUsedNames :: IORef [String] , rUITypes :: IORef [(Type, S.Kind)] - , baseTCs :: M.Map (TyCon, [TyCon]) S.Kind - , envMap :: M.Map (Var, S.Kind) Val - , specMap :: M.Map Var Val - , coreMap :: M.Map Var CoreExpr + , specials :: Specials + , tcMap :: M.Map (TyCon, [TyCon]) S.Kind + , envMap :: M.Map (Var, SKind) Val + , destMap :: M.Map Var (Val -> [(Var, SKind)] -> (S.SVal, [((Var, SKind), Val)])) + , coreMap :: M.Map Var CoreExpr } + -- | The interpreter monad type Eval a = ReaderT Env S.Symbolic a -- | Configuration info as we run the plugin -data Config = Config { dflags :: DynFlags - , wordSize :: Int - , isGHCi :: Bool +data Config = Config { isGHCi :: Bool , opts :: [SBVAnnotation] - , knownTCs :: M.Map (TyCon, [TyCon]) S.Kind - , knownFuns :: M.Map (Var, S.Kind) Val - , knownSpecials :: M.Map Var Val , sbvAnnotation :: Var -> [SBVAnnotation] - , allBinds :: M.Map Var CoreExpr + , cfgEnv :: Env } -- | Given the user options, determine which solver(s) to use @@ -69,10 +76,51 @@ , (ABC, S.abc) ] +-- | The kinds used by the plugin +data SKind = KBase S.Kind + | KTup [SKind] + | KLst SKind + | KFun SKind SKind + deriving (Eq, Ord) + -- | The values kept track of by the interpreter data Val = Base S.SVal - | Func (S.Kind, Maybe String) (S.SVal -> Eval Val) + | Typ SKind + | Tup [Val] + | Lst [Val] + | Func (Maybe String) (Val -> Eval Val) +-- | Outputable instance for SKind +instance Outputable SKind where + ppr (KBase k) = text (show k) + ppr (KTup ks) = parens $ sep (punctuate (text ",") (map ppr ks)) + ppr (KLst k) = brackets $ ppr k + ppr (KFun k r) = parens (ppr k) <+> text "->" <+> ppr r + +-- | Outputable instance for S.Kind +instance Outputable S.Kind where + ppr = text . show + +-- | Outputable instance for Val +instance Outputable Val where + ppr (Base s) = text (show s) + ppr (Typ k) = ppr k + ppr (Tup vs) = parens $ sep $ punctuate (text ",") (map ppr vs) + ppr (Lst vs) = brackets $ sep $ punctuate (text ",") (map ppr vs) + ppr (Func k _) = text ("Func<" ++ show k ++ ">") + +-- | Structural lifting of a boolean function (eq/neq) over Val +liftEqVal :: (S.SVal -> S.SVal -> S.SVal) -> Val -> Val -> S.SVal +liftEqVal baseEq v1 v2 = k v1 v2 + where k (Base a) (Base b) = a `baseEq` b + k (Tup as) (Tup bs) | length as == length bs = foldr S.svAnd S.svTrue (zipWith k as bs) + k (Lst as) (Lst bs) = foldr S.svAnd (S.svBool (length as == length bs)) (zipWith k as bs) + k _ _ = error $ "Impossible happened: liftEq received unexpected arguments: " ++ showSDocUnsafe (ppr (v1, v2)) + +-- | Symbolic equality over variables +eqVal :: Val -> Val -> S.SVal +eqVal = liftEqVal S.svEqual + -- | Compute the span given a Tick. Returns the old-span if the tick span useless. tickSpan :: Tickish t -> SrcSpan -> SrcSpan tickSpan (ProfNote cc _ _) _ = cc_loc cc @@ -85,4 +133,4 @@ -- | Show a GHC span in user-friendly form. showSpan :: Config -> Var -> SrcSpan -> String -showSpan cfg b s = showSDoc (dflags cfg) $ if isGoodSrcSpan s then ppr s else ppr b +showSpan Config{cfgEnv} b s = showSDoc (flags cfgEnv) $ if isGoodSrcSpan s then ppr s else ppr b diff --git a/Data/SBV/Plugin/Data.hs b/Data/SBV/Plugin/Data.hs --- a/Data/SBV/Plugin/Data.hs +++ b/Data/SBV/Plugin/Data.hs @@ -22,10 +22,11 @@ data SBVOption = IgnoreFailure -- ^ Continue even if proof fails | Skip String -- ^ Skip the proof. Can be handy for properties that we currently do not want to focus on. | Verbose -- ^ Produce verbose output, good for debugging - | Safety -- ^ Check for safety + | Debug -- ^ Produce really verbose output, use only when things go really wrong! | QuickCheck -- ^ Perform quickCheck | Uninterpret -- ^ Uninterpret this binding for proof purposes | Names [String] -- ^ Use these names for the arguments; need not be exhaustive + | ListSize Int -- ^ If a list-input is found, use this length. If not specified, we will complain! | Z3 -- ^ Use Z3 | Yices -- ^ Use Yices | Boolector -- ^ Use Boolector diff --git a/Data/SBV/Plugin/Env.hs b/Data/SBV/Plugin/Env.hs --- a/Data/SBV/Plugin/Env.hs +++ b/Data/SBV/Plugin/Env.hs @@ -1,4 +1,4 @@ ---------------------------------------------------------------------------- +-------------------------------------------------------------------------- -- | -- Module : Data.SBV.Plugin.Env -- Copyright : (c) Levent Erkok @@ -12,9 +12,10 @@ {-# LANGUAGE MagicHash #-} {-# LANGUAGE TemplateHaskell #-} -module Data.SBV.Plugin.Env (buildFunEnv, buildTCEnv, buildSpecialEnv) where +module Data.SBV.Plugin.Env (buildTCEnv, buildFunEnv, buildDests, buildSpecials, uninterestingTypes) where import GhcPlugins +import GHC.Prim import GHC.Types import qualified Data.Map as M @@ -31,14 +32,18 @@ import Data.SBV.Plugin.Common + +-- | What tuple-sizes we support? We go upto 15, but would be easy to change if necessary +supportTupleSizes :: [Int] +supportTupleSizes = [2 .. 15] + -- | Build the initial environment containing types buildTCEnv :: Int -> CoreM (M.Map (TyCon, [TyCon]) S.Kind) -buildTCEnv isz = do xs <- mapM grabTyCon basics +buildTCEnv wsz = do xs <- mapM grabTyCon basics ys <- mapM grabTyApp apps return $ M.fromList $ xs ++ ys - where grab x = do Just fn <- thNameToGhcName x - lookupTyCon fn + where grab = grabTH lookupTyCon grabTyCon (x, k) = grabTyApp (x, [], k) @@ -46,68 +51,62 @@ args <- mapM grab as return ((fn, args), k) - basics = [ (''Bool, S.KBool) - , (''Integer, S.KUnbounded) - , (''Float, S.KFloat) - , (''Double, S.KDouble) - , (''Int, S.KBounded True isz) - , (''Int8, S.KBounded True 8) - , (''Int16, S.KBounded True 16) - , (''Int32, S.KBounded True 32) - , (''Int64, S.KBounded True 64) - , (''Word8, S.KBounded False 8) - , (''Word16, S.KBounded False 16) - , (''Word32, S.KBounded False 32) - , (''Word64, S.KBounded False 64) - ] + basics = concat [ [(t, S.KBool) | t <- [''Bool ]] + , [(t, S.KUnbounded) | t <- [''Integer ]] + , [(t, S.KFloat) | t <- [''Float, ''Float# ]] + , [(t, S.KDouble) | t <- [''Double, ''Double#]] + , [(t, S.KBounded True wsz) | t <- [''Int, ''Int# ]] + , [(t, S.KBounded True 8) | t <- [''Int8 ]] + , [(t, S.KBounded True 16) | t <- [''Int16 ]] + , [(t, S.KBounded True 32) | t <- [''Int32, ''Int32# ]] + , [(t, S.KBounded True 64) | t <- [''Int64, ''Int64# ]] + , [(t, S.KBounded False wsz) | t <- [''Word, ''Word# ]] + , [(t, S.KBounded False 8) | t <- [''Word8 ]] + , [(t, S.KBounded False 16) | t <- [''Word16 ]] + , [(t, S.KBounded False 32) | t <- [''Word32, ''Word32#]] + , [(t, S.KBounded False 64) | t <- [''Word64, ''Word64#]] + ] apps = [ (''Ratio, [''Integer], S.KReal) ] -- | Build the initial environment containing functions -buildFunEnv :: CoreM (M.Map (Id, S.Kind) Val) -buildFunEnv = M.fromList `fmap` mapM grabVar symFuncs - where grabVar (n, k, sfn) = do Just fn <- thNameToGhcName n - f <- lookupId fn - return ((f, k), sfn) - --- | Special functions that have a fixed-type -buildSpecialEnv :: Int -> CoreM (M.Map Id Val) -buildSpecialEnv wsz = M.fromList `fmap` mapM grabVar basics - where grabVar (n, sfn) = do Just fn <- thNameToGhcName n - f <- lookupId fn - return (f, sfn) +buildFunEnv :: Int -> CoreM (M.Map (Id, SKind) Val) +buildFunEnv wsz = M.fromList `fmap` mapM thToGHC (basicFuncs wsz ++ symFuncs wsz) - basics = [ ('F#, Func (S.KFloat, Nothing) (return . Base)) - , ('D#, Func (S.KDouble, Nothing) (return . Base)) - , ('I#, Func (S.KBounded True wsz, Nothing) (return . Base)) - , ('W#, Func (S.KBounded False wsz, Nothing) (return . Base)) - , ('True, Base S.svTrue) - , ('False, Base S.svFalse) - , ('(&&), lift2 S.KBool S.svAnd) - , ('(||), lift2 S.KBool S.svOr) - , ('not, lift1 S.KBool S.svNot) - ] +-- | Basic conversions, only on one kind +basicFuncs :: Int -> [(TH.Name, SKind, Val)] +basicFuncs wsz = [ ('F#, tlift1 (KBase S.KFloat), Func Nothing return) + , ('D#, tlift1 (KBase S.KDouble), Func Nothing return) + , ('I#, tlift1 (KBase (S.KBounded True wsz)), Func Nothing return) + , ('W#, tlift1 (KBase (S.KBounded False wsz)), Func Nothing return) + , ('True, KBase S.KBool, Base S.svTrue) + , ('False, KBase S.KBool, Base S.svFalse) + , ('(&&), tlift2 (KBase S.KBool), lift2 S.svAnd) + , ('(||), tlift2 (KBase S.KBool), lift2 S.svOr) + , ('not, tlift1 (KBase S.KBool), lift1 S.svNot) + ] -- | Symbolic functions supported by the plugin; those from a class. -symFuncs :: [(TH.Name, S.Kind, Val)] -symFuncs = -- equality is for all kinds - [(op, k, lift2 k sOp) | k <- allKinds, (op, sOp) <- [('(==), S.svEqual), ('(/=), S.svNotEqual)]] +symFuncs :: Int -> [(TH.Name, SKind, Val)] +symFuncs wsz = -- equality is for all kinds + [(op, tlift2Bool (KBase k), lift2 sOp) | k <- allKinds, (op, sOp) <- [('(==), S.svEqual), ('(/=), S.svNotEqual)]] -- arithmetic - ++ [(op, k, lift1 k sOp) | k <- arithKinds, (op, sOp) <- unaryOps] - ++ [(op, k, lift2 k sOp) | k <- arithKinds, (op, sOp) <- binaryOps] + ++ [(op, tlift1 (KBase k), lift1 sOp) | k <- arithKinds, (op, sOp) <- unaryOps] + ++ [(op, tlift2 (KBase k), lift2 sOp) | k <- arithKinds, (op, sOp) <- binaryOps] -- literal conversions from Integer - ++ [(op, k, lift1Int sOp) | k <- integerKinds, (op, sOp) <- [('fromInteger, S.svInteger k)]] + ++ [(op, KFun (KBase S.KUnbounded) (KBase k), lift1Int sOp) | k <- integerKinds, (op, sOp) <- [('fromInteger, S.svInteger k)]] -- comparisons - ++ [(op, k, lift2 k sOp) | k <- arithKinds, (op, sOp) <- compOps ] + ++ [(op, tlift2Bool (KBase k), lift2 sOp) | k <- arithKinds, (op, sOp) <- compOps ] -- integer div/rem - ++ [(op, k, lift2 k sOp) | k <- integralKinds, (op, sOp) <- [('div, S.svDivide), ('quot, S.svQuot), ('rem, S.svRem)]] + ++ [(op, tlift2 (KBase k), lift2 sOp) | k <- integralKinds, (op, sOp) <- [('div, S.svDivide), ('quot, S.svQuot), ('rem, S.svRem)]] -- bit-vector - ++ [ (op, k, lift2 k sOp) | k <- bvKinds, (op, sOp) <- bvBinOps] + ++ [ (op, tlift2 (KBase k), lift2 sOp) | k <- bvKinds, (op, sOp) <- bvBinOps ] + ++ [ (op, tlift2ShRot wsz (KBase k), lift2 sOp) | k <- bvKinds, (op, sOp) <- bvShiftRots] where -- Bit-vectors @@ -129,15 +128,18 @@ allKinds = S.KBool : arithKinds -- Unary arithmetic ops - unaryOps = [ ('abs, S.svAbs) - , ('negate, S.svUNeg) + unaryOps = [ ('abs, S.svAbs) + , ('negate, S.svUNeg) + , ('complement, S.svNot) ] -- Binary arithmetic ops - binaryOps = [ ('(+), S.svPlus) - , ('(-), S.svMinus) - , ('(*), S.svTimes) - , ('(/), S.svDivide) + binaryOps = [ ('(+), S.svPlus) + , ('(-), S.svMinus) + , ('(*), S.svTimes) + , ('(/), S.svDivide) + , ('quot, S.svQuot) + , ('rem, S.svRem) ] -- Comparisons @@ -148,19 +150,154 @@ ] -- Binary bit-vector ops - bvBinOps = [ ('(.&.), S.svAnd) - , ('(.|.), S.svOr) - , ('xor, S.svXOr) + bvBinOps = [ ('(.&.), S.svAnd) + , ('(.|.), S.svOr) + , ('xor, S.svXOr) ] --- | Lift a unary SBV function to the plugin value space -lift1 :: S.Kind -> (S.SVal -> S.SVal) -> Val -lift1 k f = Func (k, Nothing) $ return . Base . f + -- Shift/rotates, where second argument is an int + bvShiftRots = [ ('shiftL, S.svShiftLeft) + , ('shiftR, S.svShiftRight) + , ('rotateL, S.svRotateLeft) + , ('rotateR, S.svRotateRight) + ] --- | Lift a unary SBV function that takes and integer value to the plugin value space + +-- | Destructors +buildDests :: CoreM (M.Map Var (Val -> [(Var, SKind)] -> (S.SVal, [((Var, SKind), Val)]))) +buildDests = do simple <- mapM mkSingle dests + tups <- mapM mkTuple supportTupleSizes + nil <- mkNil + cons <- mkCons + return $ M.fromList (simple ++ tups ++ [nil, cons]) + where + dests = [ ('W#, dest1) + , ('I#, dest1) + , ('F#, dest1) + , ('D#, dest1) + ] + + dest1 a [bk] = (S.svTrue, [(bk, a)]) + dest1 a bs = error $ "Impossible happened: Mistmatched arity case-binder for: " ++ showSDocUnsafe (ppr a) ++ ". Expected 1, got: " ++ show (length bs) ++ " arguments." + + mkSingle :: (TH.Name, b) -> CoreM (Id, b) + mkSingle (n, sfn) = do f <- grabTH lookupId n + return (f, sfn) + + mkTuple n = do d <- grabTH lookupId (TH.tupleDataName n) + let dest (Tup xs) bs + | length xs == n && length bs == n + = (S.svTrue, zip bs xs) + dest a b = error $ "Impossible: Tuple-case mismatch: " ++ showSDocUnsafe (ppr (n, a, b)) + return (d, dest) + + mkNil = do d <- lookupId nilDataConName + let dest (Lst []) [] = (S.svTrue, []) + dest (Lst _) _ = (S.svFalse, []) + dest a b = error $ "Impossible: []-case mismatch: " ++ showSDocUnsafe (ppr (a, b)) + return (d, dest) + + mkCons = do d <- lookupId consDataConName + let dest (Lst []) _ = (S.svFalse, []) + dest (Lst (x:xs)) [h, t] = (S.svTrue, [(h, x), (t, Lst xs)]) + dest a b = error $ "Impossible: (:)-case mismatch: " ++ showSDocUnsafe (ppr (a, b)) + return (d, dest) + +-- | These types show up during uninterpretation, but are not really "interesting" as they +-- are singly inhabited. +uninterestingTypes :: CoreM [Type] +uninterestingTypes = map varType `fmap` mapM (grabTH lookupId) ['void#] + +-- | Certain things are just too special, as they uniformly apply to uninterpreted types. +buildSpecials :: CoreM Specials +buildSpecials = do isEq <- do eq <- grabTH lookupId '(==) + neq <- grabTH lookupId '(/=) + + let choose = [(eq, liftEq S.svEqual), (neq, liftEq S.svNotEqual)] + + return (`lookup` choose) + + isTup <- do let mkTup n = Func Nothing g + where g (Typ _) = return $ Func Nothing g + g v = h (n-1) [v] + h 0 sofar = return $ Tup (reverse sofar) + h i sofar = return $ Func Nothing $ \v -> h (i-1) (v:sofar) + ts <- mapM (grabTH lookupId . TH.tupleDataName) supportTupleSizes + let choose = zip ts (map mkTup supportTupleSizes) + return (`lookup` choose) + + isLst <- do nil <- lookupId nilDataConName + cons <- lookupId consDataConName + + let snil = Lst [] + + scons = Func Nothing g + where g (Typ _) = return $ Func Nothing g + g v = return $ Func Nothing (k v) + k v (Lst xs) = return (Lst (v:xs)) + k v a = error $ "Impossible: (:) received incompatible arguments: " ++ showSDocUnsafe (ppr (v, a)) + + choose = [(nil, snil), (cons, scons)] + + return (`lookup` choose) + + return Specials{ isEquality = isEq + , isTuple = isTup + , isList = isLst + } + +-- | Lift a binary type, with result bool +tlift2Bool :: SKind -> SKind +tlift2Bool k = KFun k (KFun k (KBase S.KBool)) + +-- | Lift a unary type +tlift1 :: SKind -> SKind +tlift1 k = KFun k k + +-- | Lift a binary type +tlift2 :: SKind -> SKind +tlift2 k = KFun k (tlift1 k) + +-- | Lift a binary type, where second argument is Int +tlift2ShRot :: Int -> SKind -> SKind +tlift2ShRot wsz k = KFun k (KFun (KBase (S.KBounded True wsz)) k) + +-- | Lift a unary SBV function that via kind/integer lift1Int :: (Integer -> S.SVal) -> Val -lift1Int f = Func (S.KUnbounded, Nothing) $ \i -> return $ Base (f (fromMaybe (error ("Cannot extract an integer from value: " ++ show i)) (S.svAsInteger i))) +lift1Int f = Func Nothing g + where g (Base i) = return $ Base $ f (fromMaybe (error ("Cannot extract an integer from value: " ++ show i)) (S.svAsInteger i)) + g _ = error "Impossible happened: lift1Int received non-base argument!" +-- | Lift a unary SBV function to the plugin value space +lift1 :: (S.SVal -> S.SVal) -> Val +lift1 f = Func Nothing g + where g (Typ _) = return $ Func Nothing h + g v = h v + h (Base a) = return $ Base $ f a + h v = error $ "Impossible happened: lift1 received non-base argument: " ++ showSDocUnsafe (ppr v) + -- | Lift a two argument SBV function to our the plugin value space -lift2 :: S.Kind -> (S.SVal -> S.SVal -> S.SVal) -> Val -lift2 k f = Func (k, Nothing) $ \a -> return $ Func (k, Nothing) $ \b -> return (Base (f a b)) +lift2 :: (S.SVal -> S.SVal -> S.SVal) -> Val +lift2 f = Func Nothing g + where g (Typ _) = return $ Func Nothing h + g v = h v + h (Base a) = return $ Func Nothing (k a) + h v = error $ "Impossible happened: lift2 received non-base argument (h): " ++ showSDocUnsafe (ppr v) + k a (Base b) = return $ Base $ f a b + k _ v = error $ "Impossible happened: lift2 received non-base argument (k): " ++ showSDocUnsafe (ppr v) + +-- | Lifting an equality is special; since it acts uniformly over tuples. +liftEq :: (S.SVal -> S.SVal -> S.SVal) -> Val +liftEq baseEq = Func Nothing g + where g (Typ _) = return $ Func Nothing g + g v1 = return $ Func Nothing $ \v2 -> return $ Base $ liftEqVal baseEq v1 v2 + +thToGHC :: (TH.Name, a, b) -> CoreM ((Id, a), b) +thToGHC (n, k, sfn) = do f <- grabTH lookupId n + return ((f, k), sfn) + +grabTH :: (Name -> CoreM b) -> TH.Name -> CoreM b +grabTH f n = do mbN <- thNameToGhcName n + case mbN of + Just gn -> f gn + Nothing -> error $ "[SBV] Impossible happened, while trying to locate GHC name for: " ++ show n diff --git a/Data/SBV/Plugin/Plugin.hs b/Data/SBV/Plugin/Plugin.hs --- a/Data/SBV/Plugin/Plugin.hs +++ b/Data/SBV/Plugin/Plugin.hs @@ -21,6 +21,8 @@ import Data.Ord (comparing) import Data.Bits (bitSizeMaybe) +import Data.IORef + import qualified Data.Map as M import Data.SBV.Plugin.Common @@ -31,33 +33,50 @@ plugin :: Plugin plugin = defaultPlugin {installCoreToDos = install} where install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo] - install [] todos = reinitializeGlobals >> return (sbvPass : todos) - install opts _ = do liftIO $ putStrLn $ "[SBV] Unexpected command line options: " ++ show opts - liftIO exitFailure + install [] todos = reinitializeGlobals >> return (sbvPass : todos) + install ["runLast"] todos = reinitializeGlobals >> return (todos ++ [sbvPass]) + install opts _ = do liftIO $ putStrLn $ "[SBV] Unexpected command line options: " ++ show opts + liftIO $ putStrLn "" + liftIO $ putStrLn "Options:" + liftIO $ putStrLn " runLast (run the SBV analyzer last)" + liftIO exitFailure sbvPass = CoreDoPluginPass "SBV based analysis" pass pass :: ModGuts -> CoreM ModGuts - pass guts@(ModGuts {mg_binds}) = do + pass guts@ModGuts{mg_binds} = do df <- getDynFlags anns <- getAnnotations deserializeWithData guts let wsz = fromJust (bitSizeMaybe (0::Int)) - baseTCs <- buildTCEnv wsz - baseEnv <- buildFunEnv - baseSpecials <- buildSpecialEnv wsz + baseTCs <- buildTCEnv wsz + baseEnv <- buildFunEnv wsz + baseDests <- buildDests + uninteresting <- uninterestingTypes + specials <- buildSpecials - let cfg = Config { dflags = df + rUninterpreted <- liftIO $ newIORef [] + rUsedNames <- liftIO $ newIORef [] + rUITypes <- liftIO $ newIORef [] + + let cfg = Config { isGHCi = hscTarget df == HscInterpreted , opts = [] - , wordSize = wsz - , isGHCi = hscTarget df == HscInterpreted - , knownTCs = baseTCs - , knownFuns = baseEnv - , knownSpecials = baseSpecials , sbvAnnotation = lookupWithDefaultUFM anns [] . varUnique - , allBinds = M.fromList (flattenBinds mg_binds) + , cfgEnv = Env { curLoc = noSrcSpan + , flags = df + , machWordSize = wsz + , uninteresting = uninteresting + , rUninterpreted = rUninterpreted + , rUsedNames = rUsedNames + , rUITypes = rUITypes + , specials = specials + , tcMap = baseTCs + , envMap = baseEnv + , destMap = baseDests + , coreMap = M.fromList (flattenBinds mg_binds) + } } let bindLoc (NonRec b _) = bindSpan b diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -1,5 +1,5 @@ Name : sbvPlugin -Version : 0.1 +Version : 0.2 Category : Formal methods, Theorem provers, Math, SMT, Symbolic Computation Synopsis : Analyze Haskell expressions using SBV/SMT Description : GHC plugin for analyzing expressions using SMT solvers, based @@ -26,7 +26,7 @@ default-language: Haskell2010 ghc-options : -Wall Exposed-modules : Data.SBV.Plugin - build-depends : base >= 4.8 && < 5, ghc, ghc-prim, containers, sbv >= 5.6, mtl, template-haskell + build-depends : base >= 4.8 && < 5, ghc, ghc-prim, containers, sbv >= 5.7, mtl, template-haskell Other-modules : Data.SBV.Plugin.Analyze , Data.SBV.Plugin.Data , Data.SBV.Plugin.Common diff --git a/tests/GoldFiles/T05.hs.golden b/tests/GoldFiles/T05.hs.golden --- a/tests/GoldFiles/T05.hs.golden +++ b/tests/GoldFiles/T05.hs.golden @@ -1,5 +1,5 @@ -[SBV] tests/T05.hs:9:1 Proving "f", using CVC4 and Yices. -[Yices] Falsifiable. Counter-example: +[SBV] tests/T05.hs:9:1 Proving "f", using CVC4. +[CVC4] Falsifiable. Counter-example: x = 0 :: Integer y = -1 :: Integer diff --git a/tests/GoldFiles/T13.hs.golden b/tests/GoldFiles/T13.hs.golden --- a/tests/GoldFiles/T13.hs.golden +++ b/tests/GoldFiles/T13.hs.golden @@ -1,7 +1,7 @@ [SBV] tests/T13.hs:9:1 Proving "f", using Z3. [Z3] Falsifiable. Counter-example: - i = 2 :: Integer + i = 0 :: Integer d = 0.0 :: Double b = False :: Bool [SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T15.hs.golden b/tests/GoldFiles/T15.hs.golden --- a/tests/GoldFiles/T15.hs.golden +++ b/tests/GoldFiles/T15.hs.golden @@ -1,51 +1,3 @@ [SBV] tests/T15.hs:11:1 Proving "f", using Z3. -** Starting symbolic simulation.. -** Generated symbolic trace: -SORTS - Age -INPUTS - s0 :: Age, aliasing "age" -CONSTANTS - s_2 = False :: Bool - s_1 = True :: Bool -TABLES -ARRAYS -UNINTERPRETED CONSTANTS - [uninterpreted] ds_d6XY :: SInt64 -USER GIVEN CODE SEGMENTS -AXIOMS -DEFINE - s1 :: SInt64 = [uninterpreted] ds_d6XY -CONSTRAINTS -ASSERTIONS -OUTPUTS - s_1 -** Translating to SMT-Lib.. -** Checking Theoremhood.. -** Generated SMTLib program: -; Automatically generated by SBV. Do not edit. -(set-option :produce-models true) -; has user-defined sorts, no logic specified. -; --- uninterpreted sorts --- -(declare-sort Age 0) ; N.B. Uninterpreted: originating from sbvPlugin: -; --- literal constants --- -(define-fun s_2 () Bool false) -(define-fun s_1 () Bool true) -; --- skolem constants --- -(declare-fun s0 () Age) ; tracks user variable "age" -; --- constant tables --- -; --- skolemized tables --- -; --- arrays --- -; --- uninterpreted constants --- -(declare-fun ds_d6XY () (_ BitVec 64)) -; --- user given axioms --- -; --- formula --- -(assert ; no quantifiers - (let ((s1 ds_d6XY)) - (not s_1))) -** Calling: "z3 -nw -in -smt2" -** Z3 output: -unsat -** Done.. [Z3] Q.E.D. diff --git a/tests/GoldFiles/T16.hs.golden b/tests/GoldFiles/T16.hs.golden --- a/tests/GoldFiles/T16.hs.golden +++ b/tests/GoldFiles/T16.hs.golden @@ -1,62 +1,7 @@ [SBV] tests/T16.hs:11:1 Proving "f", using Z3. -** Starting symbolic simulation.. -** Generated symbolic trace: -SORTS - Age -INPUTS - s0 :: Age, aliasing "age" -CONSTANTS - s_2 = False :: Bool - s_1 = True :: Bool - s2 = 1 :: Int64 -TABLES -ARRAYS -UNINTERPRETED CONSTANTS - [uninterpreted] ds_d79t :: SInt64 -USER GIVEN CODE SEGMENTS -AXIOMS -DEFINE - s1 :: SInt64 = [uninterpreted] ds_d79t - s3 :: SInt64 = s1 + s2 - s4 :: SBool = s1 == s3 -CONSTRAINTS -ASSERTIONS -OUTPUTS - s4 -** Translating to SMT-Lib.. -** Checking Theoremhood.. -** Generated SMTLib program: -; Automatically generated by SBV. Do not edit. -(set-option :produce-models true) -; has user-defined sorts, no logic specified. -; --- uninterpreted sorts --- -(declare-sort Age 0) ; N.B. Uninterpreted: originating from sbvPlugin: -; --- literal constants --- -(define-fun s_2 () Bool false) -(define-fun s_1 () Bool true) -(define-fun s2 () (_ BitVec 64) #x0000000000000001) -; --- skolem constants --- -(declare-fun s0 () Age) ; tracks user variable "age" -; --- constant tables --- -; --- skolemized tables --- -; --- arrays --- -; --- uninterpreted constants --- -(declare-fun ds_d79t () (_ BitVec 64)) -; --- user given axioms --- -; --- formula --- -(assert ; no quantifiers - (let ((s1 ds_d79t)) - (let ((s3 (bvadd s1 s2))) - (let ((s4 (= s1 s3))) - (not s4))))) -** Calling: "z3 -nw -in -smt2" -** Sending the following model extraction commands: -(get-value (s0)) -** Z3 output: -sat -((s0 Age!val!0)) -** Done.. [Z3] Falsifiable. Counter-example: age = Age!val!0 :: Age +[SBV] Counter-example might be bogus due to uninterpreted constant: + [] ds_d6ci :: Int [SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T17.hs.golden b/tests/GoldFiles/T17.hs.golden --- a/tests/GoldFiles/T17.hs.golden +++ b/tests/GoldFiles/T17.hs.golden @@ -1,5 +1,5 @@ -[SBV] tests/T17.hs:13:1 Proving "f", using Z3. +[SBV] tests/T17.hs:14:1 Proving "f", using Z3. [Z3] Falsifiable. Counter-example: x = 0 :: Int64 [SBV] Counter-example might be bogus due to uninterpreted constant: diff --git a/tests/GoldFiles/T18.hs.golden b/tests/GoldFiles/T18.hs.golden --- a/tests/GoldFiles/T18.hs.golden +++ b/tests/GoldFiles/T18.hs.golden @@ -13,11 +13,10 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS - [uninterpreted] |==| :: Age -> Age -> SBool USER GIVEN CODE SEGMENTS AXIOMS DEFINE - s2 :: SBool = s0 [uninterpreted] |==| s1 + s2 :: SBool = s0 == s1 CONSTRAINTS ASSERTIONS OUTPUTS @@ -40,11 +39,10 @@ ; --- skolemized tables --- ; --- arrays --- ; --- uninterpreted constants --- -(declare-fun |==| (Age Age) Bool) ; --- user given axioms --- ; --- formula --- (assert ; no quantifiers - (let ((s2 (|==| s0 s1))) + (let ((s2 (= s0 s1))) (not s2))) ** Calling: "z3 -nw -in -smt2" ** Sending the following model extraction commands: @@ -58,6 +56,4 @@ [Z3] Falsifiable. Counter-example: a = Age!val!0 :: Age b = Age!val!1 :: Age -[SBV] Counter-example might be bogus due to uninterpreted constant: - [] == :: Age -> Age -> Bool [SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T19.hs.golden b/tests/GoldFiles/T19.hs.golden --- a/tests/GoldFiles/T19.hs.golden +++ b/tests/GoldFiles/T19.hs.golden @@ -1,65 +1,14 @@ [SBV] tests/T19.hs:9:1 Proving "f", using Z3. -** Starting symbolic simulation.. -** Generated symbolic trace: -SORTS - |[Char]| -INPUTS - s0 :: |[Char]|, aliasing "s" -CONSTANTS - s_2 = False :: Bool - s_1 = True :: Bool -TABLES -ARRAYS -UNINTERPRETED CONSTANTS - [uninterpreted] reverse :: |[Char]| -> |[Char]| - [uninterpreted] |==| :: |[Char]| -> |[Char]| -> SBool -USER GIVEN CODE SEGMENTS -AXIOMS -DEFINE - s1 :: |[Char]| = [uninterpreted] reverse s0 - s2 :: |[Char]| = [uninterpreted] reverse s1 - s3 :: SBool = s2 [uninterpreted] |==| s0 -CONSTRAINTS -ASSERTIONS -OUTPUTS - s3 -** Translating to SMT-Lib.. -** Checking Theoremhood.. -** Generated SMTLib program: -; Automatically generated by SBV. Do not edit. -(set-option :produce-models true) -; has user-defined sorts, no logic specified. -; --- uninterpreted sorts --- -(declare-sort |[Char]| 0) ; N.B. Uninterpreted: originating from sbvPlugin: tests/T19.hs:9:3 -; --- literal constants --- -(define-fun s_2 () Bool false) -(define-fun s_1 () Bool true) -; --- skolem constants --- -(declare-fun s0 () |[Char]|) ; tracks user variable "s" -; --- constant tables --- -; --- skolemized tables --- -; --- arrays --- -; --- uninterpreted constants --- -(declare-fun reverse (|[Char]|) |[Char]|) -(declare-fun |==| (|[Char]| |[Char]|) Bool) -; --- user given axioms --- -; --- formula --- -(assert ; no quantifiers - (let ((s1 (reverse s0))) - (let ((s2 (reverse s1))) - (let ((s3 (|==| s2 s0))) - (not s3))))) -** Calling: "z3 -nw -in -smt2" -** Sending the following model extraction commands: -(get-value (s0)) -** Z3 output: -sat -((s0 |[Char]!val!0|)) -** Done.. +[Z3] Q.E.D. + +[SBV] tests/T19.hs:15:1 Proving "g", using Z3. [Z3] Falsifiable. Counter-example: - s = |[Char]!val!0| :: |[Char]| + s_1 = sbvChar!val!0 :: sbvChar + s_2 = sbvChar!val!0 :: sbvChar + s_3 = sbvChar!val!0 :: sbvChar + s_4 = sbvChar!val!0 :: sbvChar + s_5 = sbvChar!val!0 :: sbvChar + s_6 = sbvChar!val!0 :: sbvChar [SBV] Counter-example might be bogus due to uninterpreted constants: - [] == :: [Char] -> [Char] -> Bool - [] reverse :: [Char] -> [Char] -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) + [] C# :: Char# -> Char diff --git a/tests/GoldFiles/T21.hs.golden b/tests/GoldFiles/T21.hs.golden --- a/tests/GoldFiles/T21.hs.golden +++ b/tests/GoldFiles/T21.hs.golden @@ -2,30 +2,7 @@ [SBV] tests/T21.hs:9:1 Proving "f", using Z3. ** Starting symbolic simulation.. ** Generated symbolic trace: -SORTS - Char - String -INPUTS - s0 :: Char, aliasing "c" - s1 :: String, aliasing "s" -CONSTANTS - s_2 = False :: Bool - s_1 = True :: Bool -TABLES -ARRAYS -UNINTERPRETED CONSTANTS - [uninterpreted] |==_0| :: String -> String -> SBool - [uninterpreted] |==| :: Char -> Char -> SBool -USER GIVEN CODE SEGMENTS -AXIOMS -DEFINE - s2 :: SBool = s0 [uninterpreted] |==| s0 - s3 :: SBool = s1 [uninterpreted] |==_0| s1 - s4 :: SBool = s2 & s3 -CONSTRAINTS -ASSERTIONS -OUTPUTS - s4 +True :: Bool ** Translating to SMT-Lib.. ** Checking Theoremhood.. ** Generated SMTLib program: @@ -33,40 +10,27 @@ (set-option :produce-models true) ; has user-defined sorts, no logic specified. ; --- uninterpreted sorts --- -(declare-sort Char 0) ; N.B. Uninterpreted: originating from sbvPlugin: tests/T21.hs:9:3 -(declare-sort String 0) ; N.B. Uninterpreted: originating from sbvPlugin: tests/T21.hs:9:5 +(declare-sort sbvChar 0) ; N.B. Uninterpreted: originating from sbvPlugin: tests/T21.hs:9:3 ; --- literal constants --- (define-fun s_2 () Bool false) (define-fun s_1 () Bool true) ; --- skolem constants --- -(declare-fun s0 () Char) ; tracks user variable "c" -(declare-fun s1 () String) ; tracks user variable "s" +(declare-fun s0 () sbvChar) ; tracks user variable "c" +(declare-fun s1 () sbvChar) ; tracks user variable "s_1" +(declare-fun s2 () sbvChar) ; tracks user variable "s_2" +(declare-fun s3 () sbvChar) ; tracks user variable "s_3" +(declare-fun s4 () sbvChar) ; tracks user variable "s_4" +(declare-fun s5 () sbvChar) ; tracks user variable "s_5" ; --- constant tables --- ; --- skolemized tables --- ; --- arrays --- ; --- uninterpreted constants --- -(declare-fun |==_0| (String String) Bool) -(declare-fun |==| (Char Char) Bool) ; --- user given axioms --- ; --- formula --- (assert ; no quantifiers - (let ((s2 (|==| s0 s0))) - (let ((s3 (|==_0| s1 s1))) - (let ((s4 (and s2 s3))) - (not s4))))) + (not s_1)) ** Calling: "z3 -nw -in -smt2" -** Sending the following model extraction commands: -(get-value (s0)) -(get-value (s1)) ** Z3 output: -sat -((s0 Char!val!0)) -((s1 String!val!0)) +unsat ** Done.. -[Z3] Falsifiable. Counter-example: - c = Char!val!0 :: Char - s = String!val!0 :: String -[SBV] Counter-example might be bogus due to uninterpreted constants: - [] == :: String -> String -> Bool - [] == :: Char -> Char -> Bool -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) +[Z3] Q.E.D. diff --git a/tests/GoldFiles/T22.hs.golden b/tests/GoldFiles/T22.hs.golden --- a/tests/GoldFiles/T22.hs.golden +++ b/tests/GoldFiles/T22.hs.golden @@ -1,65 +1,5 @@ -[SBV] tests/T22.hs:9:1 Proving "f", using Z3. -** Starting symbolic simulation.. -** Generated symbolic trace: -SORTS - String -INPUTS - s0 :: String, aliasing "s" -CONSTANTS - s_2 = False :: Bool - s_1 = True :: Bool -TABLES -ARRAYS -UNINTERPRETED CONSTANTS - [uninterpreted] reverse :: String -> String - [uninterpreted] |==| :: String -> String -> SBool -USER GIVEN CODE SEGMENTS -AXIOMS -DEFINE - s1 :: String = [uninterpreted] reverse s0 - s2 :: String = [uninterpreted] reverse s1 - s3 :: SBool = s2 [uninterpreted] |==| s0 -CONSTRAINTS -ASSERTIONS -OUTPUTS - s3 -** Translating to SMT-Lib.. -** Checking Theoremhood.. -** Generated SMTLib program: -; Automatically generated by SBV. Do not edit. -(set-option :produce-models true) -; has user-defined sorts, no logic specified. -; --- uninterpreted sorts --- -(declare-sort String 0) ; N.B. Uninterpreted: originating from sbvPlugin: tests/T22.hs:9:3 -; --- literal constants --- -(define-fun s_2 () Bool false) -(define-fun s_1 () Bool true) -; --- skolem constants --- -(declare-fun s0 () String) ; tracks user variable "s" -; --- constant tables --- -; --- skolemized tables --- -; --- arrays --- -; --- uninterpreted constants --- -(declare-fun reverse (String) String) -(declare-fun |==| (String String) Bool) -; --- user given axioms --- -; --- formula --- -(assert ; no quantifiers - (let ((s1 (reverse s0))) - (let ((s2 (reverse s1))) - (let ((s3 (|==| s2 s0))) - (not s3))))) -** Calling: "z3 -nw -in -smt2" -** Sending the following model extraction commands: -(get-value (s0)) -** Z3 output: -sat -((s0 String!val!0)) -** Done.. +[SBV] tests/T22.hs:12:1 Proving "g", using Z3. [Z3] Falsifiable. Counter-example: - s = String!val!0 :: String -[SBV] Counter-example might be bogus due to uninterpreted constants: - [] == :: [Char] -> [Char] -> Bool - [] reverse :: [Char] -> [Char] + s0 = -1 :: Int64 [SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T25.hs.golden b/tests/GoldFiles/T25.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T25.hs.golden @@ -0,0 +1,3 @@ + +[SBV] tests/T25.hs:9:1 Proving "f", using Z3. +[Z3] Q.E.D. diff --git a/tests/GoldFiles/T26.hs.golden b/tests/GoldFiles/T26.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T26.hs.golden @@ -0,0 +1,4 @@ + +[SBV] tests/T26.hs:9:1 Proving "f", using Z3. +[Z3] Falsifiable +[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T27.hs.golden b/tests/GoldFiles/T27.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T27.hs.golden @@ -0,0 +1,29 @@ + +[SBV] tests/T27.hs:9:1 Proving "g", using Z3. +** Starting symbolic simulation.. +** Generated symbolic trace: +True :: Bool +** Translating to SMT-Lib.. +** Checking Theoremhood.. +** Generated SMTLib program: +; Automatically generated by SBV. Do not edit. +(set-option :produce-models true) +(set-logic QF_BV) +; --- uninterpreted sorts --- +; --- literal constants --- +(define-fun s_2 () Bool false) +(define-fun s_1 () Bool true) +; --- skolem constants --- +; --- constant tables --- +; --- skolemized tables --- +; --- arrays --- +; --- uninterpreted constants --- +; --- user given axioms --- +; --- formula --- +(assert ; no quantifiers + (not s_1)) +** Calling: "z3 -nw -in -smt2" +** Z3 output: +unsat +** Done.. +[Z3] Q.E.D. diff --git a/tests/GoldFiles/T28.hs.golden b/tests/GoldFiles/T28.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T28.hs.golden @@ -0,0 +1,3 @@ + +[SBV] tests/T28.hs:13:1 Proving "g", using Z3. +[Z3] Q.E.D. diff --git a/tests/GoldFiles/T29.hs.golden b/tests/GoldFiles/T29.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T29.hs.golden @@ -0,0 +1,4 @@ + +[SBV] tests/T29.hs:13:1 Proving "g", using Z3. +[Z3] Falsifiable +[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T30.hs.golden b/tests/GoldFiles/T30.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T30.hs.golden @@ -0,0 +1,3 @@ + +[SBV] tests/T30.hs:9:1 Proving "f", using Z3. +[Z3] Q.E.D. diff --git a/tests/GoldFiles/T31.hs.golden b/tests/GoldFiles/T31.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T31.hs.golden @@ -0,0 +1,19 @@ + +[SBV] tests/T31.hs:9:1 Proving "f", using Z3. + +[SBV] tests/T31.hs:9:1 Skipping proof. Non-boolean property declaration: + Found : Int -> Int + Returning: Int + Expected : Bool result + +[SBV] tests/T31.hs:13:1 Proving "g", using Z3. + +[SBV] tests/T31.hs:13:1 Skipping proof. Non-boolean property declaration: + Found : Char + Expected : Bool + +[SBV] tests/T31.hs:17:1 Proving "h", using Z3. + +[SBV] tests/T31.hs:17:1 Skipping proof. Non-boolean property declaration: + Found : Double + Expected : Bool diff --git a/tests/GoldFiles/T32.hs.golden b/tests/GoldFiles/T32.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T32.hs.golden @@ -0,0 +1,7 @@ + +[SBV] tests/T32.hs:11:1 Proving "f", using Z3. +[Z3] Q.E.D. + +[SBV] tests/T32.hs:15:1 Proving "g", using Z3. +[Z3] Falsifiable. Counter-example: + x = 32 :: Word8 diff --git a/tests/GoldFiles/T33.hs.golden b/tests/GoldFiles/T33.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T33.hs.golden @@ -0,0 +1,7 @@ + +[SBV] tests/T33.hs:9:1 Proving "f", using Z3. +[Z3] Falsifiable. Counter-example: + x = 0 :: Int64 + +[SBV] tests/T33.hs:15:1 Proving "g", using Z3. +[Z3] Q.E.D. diff --git a/tests/GoldFiles/T34.hs.golden b/tests/GoldFiles/T34.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T34.hs.golden @@ -0,0 +1,3 @@ + +[SBV] tests/T34.hs:9:1 Proving "f", using Z3. +[Z3] Q.E.D. diff --git a/tests/GoldFiles/T35.hs.golden b/tests/GoldFiles/T35.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T35.hs.golden @@ -0,0 +1,6 @@ + +[SBV] tests/T35.hs:9:1 Proving "f", using Z3. +[Z3] Falsifiable. Counter-example: + x = -1 :: Int64 + y = 0 :: Int64 +[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T36.hs.golden b/tests/GoldFiles/T36.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T36.hs.golden @@ -0,0 +1,9 @@ + +[SBV] tests/T36.hs:9:1 Proving "f", using Z3. +[Z3] Q.E.D. + +[SBV] tests/T36.hs:14:1 Proving "g", using Z3. +[Z3] Falsifiable. Counter-example: + a = -65 :: Int64 + b = -65 :: Int64 + c = 64 :: Int64 diff --git a/tests/GoldFiles/T37.hs.golden b/tests/GoldFiles/T37.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T37.hs.golden @@ -0,0 +1,6 @@ + +[SBV] tests/T37.hs:9:1 Proving "f", using Z3. +[Z3] Falsifiable. Counter-example: + a = 2 :: Int64 + b = 2.3 :: Double +[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T38.hs.golden b/tests/GoldFiles/T38.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T38.hs.golden @@ -0,0 +1,7 @@ + +[SBV] tests/T38.hs:9:1 Proving "f", using Z3. +[Z3] Falsifiable. Counter-example: + a = 1 :: Int64 + b = 2 :: Int64 + c = 4 :: Int64 +[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T39.hs.golden b/tests/GoldFiles/T39.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T39.hs.golden @@ -0,0 +1,6 @@ + +[SBV] tests/T39.hs:9:1 Proving "f", using Z3. +[Z3] Falsifiable. Counter-example: + p_1 = -1 :: Int64 + p_2 = 0 :: Int64 +[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T40.hs.golden b/tests/GoldFiles/T40.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T40.hs.golden @@ -0,0 +1,3 @@ + +[SBV] tests/T40.hs:9:1 Proving "f", using Z3. +[Z3] Q.E.D. diff --git a/tests/GoldFiles/T41.hs.golden b/tests/GoldFiles/T41.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T41.hs.golden @@ -0,0 +1,8 @@ + +[SBV] tests/T41.hs:9:1 Proving "f", using Z3. +[Z3] Q.E.D. + +[SBV] tests/T41.hs:13:1 Proving "g", using Z3. +[Z3] Falsifiable. Counter-example: + x = -1 :: Int64 + y = 0 :: Int64 diff --git a/tests/GoldFiles/T42.hs.golden b/tests/GoldFiles/T42.hs.golden new file mode 100644 --- /dev/null +++ b/tests/GoldFiles/T42.hs.golden @@ -0,0 +1,9 @@ + +[SBV] tests/T42.hs:9:1 Proving "f", using Z3. +[Z3] Falsifiable. Counter-example: + xs_1 = 10 :: Int64 + xs_2 = 0 :: Int64 + xs_3 = 0 :: Int64 + xs_4 = 0 :: Int64 + xs_5 = 0 :: Int64 +[SBV] Failed. (Use option 'IgnoreFailure' to continue.)