diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,15 @@ * Hackage: * GitHub: -* Latest Hackage released version: 0.4, 2015-12-24 +* Latest Hackage released version: 0.5, 2015-12-26 + +### Version 0.5, 2015-12-26 + + * Allow higher-order (i.e., function) arguments to theorems. + * Rework uninterpreted functions, generalize types + * Simplify cabal file; no need to ship gold-files for tests + * Add merge-sort example "Data/SBV/Plugin/Examples/MergeSort.hs" + * Add bit-tricks example "Data/SBV/Plugin/Examples/BitTricks.hs" ### Version 0.4, 2015-12-24 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 @@ -44,16 +44,18 @@ 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 (flags cfgEnv) (ppr b)) ++ ": " ++ s - | Uninterpret `elem` opts = return () - | True = liftIO $ prove cfg opts b topLoc e + | Just s <- hasSkip opts + = liftIO $ putStrLn $ "[SBV] " ++ showSpan cfg (pickSpan [varSpan b]) ++ " Skipping " ++ show (showSDoc (flags cfgEnv) (ppr b)) ++ ": " ++ s + | Uninterpret `elem` opts + = return () + | True + = liftIO $ prove cfg opts b e hasSkip opts = listToMaybe [s | Skip s <- opts] - topLoc = bindSpan b -- | Prove an SBVTheorem -prove :: Config -> [SBVOption] -> Var -> SrcSpan -> CoreExpr -> IO () -prove cfg@Config{isGHCi} opts b topLoc e = do - success <- safely $ proveIt cfg opts (topLoc, b) e +prove :: Config -> [SBVOption] -> Var -> CoreExpr -> IO () +prove cfg@Config{isGHCi} opts b e = do + success <- safely $ proveIt cfg opts b e unless (success || isGHCi || IgnoreFailure `elem` opts) $ do putStrLn $ "[SBV] Failed. (Use option '" ++ show IgnoreFailure ++ "' to continue.)" exitFailure @@ -65,16 +67,24 @@ bad e = do print e return False +-- | Sometimes life is hard. Giving up is an option. +die :: Config -> [SrcSpan] -> String -> [String] -> a +die cfg locs w es = error $ concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es + where marker = "[SBV] " ++ showSpan cfg (pickSpan locs) + tag s = marker ++ " " ++ s + tab s = replicate (length marker) ' ' ++ " " ++ s + -- | Returns True if proof went thru -proveIt :: Config -> [SBVOption] -> (SrcSpan, Var) -> CoreExpr -> IO Bool -proveIt cfg@Config{cfgEnv, sbvAnnotation} opts (topLoc, topBind) topExpr = do +proveIt :: Config -> [SBVOption] -> Var -> CoreExpr -> IO Bool +proveIt cfg@Config{cfgEnv, sbvAnnotation} opts topBind topExpr = do solverConfigs <- pickSolvers opts let verbose = Verbose `elem` opts qCheck = QuickCheck `elem` opts runProver prop | qCheck = Left `fmap` S.svQuickCheck prop | True = Right `fmap` S.proveWithAny [s{S.verbose = verbose} | s <- solverConfigs] prop - loc = "[SBV] " ++ showSpan cfg topBind topLoc + topLoc = varSpan topBind + loc = "[SBV] " ++ showSpan cfg topLoc slvrTag = ", using " ++ tag ++ "." where tag = case solverConfigs of [] -> "no solvers" -- can't really happen @@ -83,7 +93,7 @@ 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 - finalResult <- runProver (res cfgEnv) + finalResult <- runProver (res cfgEnv topLoc) finalUninterps <- readIORef (rUninterpreted cfgEnv) return (finalResult, finalUninterps) case finalResult of @@ -97,8 +107,8 @@ putStr $ "[" ++ show solver ++ "] " print sres - -- 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] + -- If proof failed and there are uninterpreted non-input values, print a warning; except for "uninteresting" types + let unintVals = filter ((`notElem` uninteresting cfgEnv) . snd) $ nub $ sortBy (comparing fst) [vt | (vt, (False, _, _)) <- finalUninterps] unless (success || null unintVals) $ do let plu | length finalUninterps > 1 = "s:" | True = ":" @@ -116,21 +126,17 @@ where debug = Debug `elem` opts - res initEnv = do - v <- runReaderT (symEval topExpr) initEnv{curLoc = topLoc} + res initEnv topLoc = do + v <- runReaderT (symEval topExpr) initEnv { curLoc = [topLoc] + , mbListSize = listToMaybe [n | ListSize n <- opts] + } case v of Base r -> return r 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 - where marker = "[SBV] " ++ showSpan cfg topBind loc - tag s = marker ++ " " ++ s - tab s = replicate (length marker) ' ' ++ " " ++ s - tbd :: String -> [String] -> Eval Val tbd w ws = do Env{curLoc} <- ask - die curLoc w ws + die cfg curLoc w ws sh o = showSDoc (flags cfgEnv) (ppr o) @@ -140,8 +146,7 @@ symEval :: CoreExpr -> Eval Val symEval e = do let (bs, body) = collectBinders (pushLetLambda e) Env{curLoc} <- ask - let mbListSize = listToMaybe [n | ListSize n <- opts] - bodyType <- getType curLoc (exprType body) + bodyType <- getType (pickSpan curLoc) (exprType body) -- Figure out if there were some unmentioned variables; happens if the top -- level wasn't fully saturated. @@ -152,22 +157,22 @@ 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)) + let mkVar ((b, k), mbN) = do sv <- mkSym cfg (Just b) (varSpan b) (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)) + bArgs <- mapM 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 + feed (k:ks) (Func _ f) = do sv <- mkSym cfg Nothing (pickSpan 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)] + _ -> die cfg 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"] ]) @@ -175,39 +180,11 @@ 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 (Tick t e) = local (\envMap -> envMap{curLoc = tickSpan t (curLoc envMap)}) $ go e + go (Tick t e) = local (\envMap -> envMap{curLoc = tickSpan t : curLoc envMap}) $ go e go e = tgo (exprType e) e debugTrace s w @@ -224,11 +201,11 @@ 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 -> debugTrace ("Uninterpreting: " ++ sh (v, k, nub $ sort $ map (fst . fst) (M.toList envMap))) - $ uninterpret t v + Just (l, b) -> if isUninterpretedBinding v + then uninterpret cfg False t v + else local (\env -> env{curLoc = l : curLoc env}) $ go b + Nothing -> debugTrace ("Uninterpreting: " ++ sh (v, k, nub $ sort $ map (fst . fst) (M.toList envMap))) + $ uninterpret cfg False t v tgo t e@(Lit l) = do Env{machWordSize} <- ask case l of @@ -259,15 +236,21 @@ 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 + let getVar (Var v) = Just v + getVar (Tick _ e) = getVar e + getVar _ = Nothing + isEq (App (App ev (Type _)) dict) | Just v <- getVar ev, isReallyADictionary dict, Just f <- isEquality specials v = Just f + isEq _ = Nothing + isTup (Var v) = isTuple specials v isTup (App f (Type _)) = isTup f + isTup (Tick _ e) = isTup e isTup _ = Nothing isLst (Var v) = isList specials v isLst (App f (Type _)) = isLst f + isLst (Tick _ e) = isLst e isLst _ = Nothing isSpecial e = isEq e `mplus` isTup e `mplus` isLst e @@ -275,6 +258,23 @@ case isSpecial reduced of Just f -> debugTrace ("Special located: " ++ sh (orig, f)) $ return f Nothing -> case reduced of + + -- special case for split and join; there must be a better way to do this + App (App (App (Var v) (Type t1)) (Type t2)) dict | isReallyADictionary dict -> do + Env{envMap} <- ask + let vSpan = getSrcSpan v + k1 <- getType vSpan t1 + k2 <- getType vSpan t2 + let kSplit = KFun k1 (KTup [k2, k2]) + kJoin = KFun k1 (KFun k1 k2) + case ((v, kSplit) `M.lookup` envMap, (v, kJoin) `M.lookup` envMap) of + (Just b, _) -> debugTrace ("Located split: " ++ sh (reduced, kSplit)) $ return b + (_, Just b) -> debugTrace ("Located join: " ++ sh (reduced, kJoin)) $ return b + _ -> do Env{coreMap} <- ask + case v `M.lookup` coreMap of + Just (l, e) -> local (\env -> env{curLoc = l : curLoc env}) $ tgo tFun (App (App (App e (Type t1)) (Type t2)) dict) + Nothing -> tgo tFun (Var v) + App (App (Var v) (Type t)) dict | isReallyADictionary dict -> do Env{envMap} <- ask k <- getType (getSrcSpan v) t @@ -282,14 +282,14 @@ 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) + Just (l, e) -> local (\env -> env{curLoc = l : curLoc env}) $ 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) + Just (l, e) -> local (\env -> env{curLoc = l : curLoc env}) $ tgo tFun (App e (Type t)) + Nothing -> tgo tFun (Var v) App (Let (Rec bs) f) a -> go (Let (Rec bs) (App f a)) @@ -307,35 +307,38 @@ 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) = local (\env -> env{coreMap = M.insert b e (coreMap env)}) (go body) + tgo _ (Let (NonRec b e) body) = local (\env -> env{coreMap = M.insert b (varSpan b, e) (coreMap env)}) (go body) - tgo _ (Let (Rec bs) body) = local (\env -> env{coreMap = foldr (uncurry M.insert) (coreMap env) bs}) (go body) + tgo _ (Let (Rec bs) body) = local (\env -> env{coreMap = foldr (\(b, e) m -> M.insert b (varSpan b, e) m) (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 caseBinder caseType alts) = do sce <- go ce - Env{curLoc} <- ask - let caseTooComplicated l w [] = die l ("Unsupported case-expression (" ++ w ++ ")") [sh e] - caseTooComplicated l w xs = die l ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs + let caseTooComplicated l w [] = die cfg l ("Unsupported case-expression (" ++ w ++ ")") [sh e] + caseTooComplicated l w xs = die cfg l ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs isDefault (DEFAULT, _, _) = True isDefault _ = False (defs, nonDefs) = partition isDefault alts walk ((p, bs, rhs) : rest) = do -- try to get a "good" location for this alternative, if possible: let eLoc = case (rhs, bs) of - (Tick t _, _ ) -> tickSpan t curLoc - (_, b:_) -> bindSpan b - _ -> curLoc + (Tick t _, _ ) -> tickSpan t + (Var v, _ ) -> varSpan v + (_, b:_) -> varSpan b + _ -> varSpan caseBinder mr <- match eLoc 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 + Just (m, bs') -> do let result = local (\env -> env{curLoc = eLoc : curLoc env, envMap = foldr (uncurry M.insert) (envMap env) bs'}) $ go rhs if null rest then result - else choose (caseTooComplicated eLoc "with-complicated-alternatives-during-merging") m result (walk rest) - Nothing -> caseTooComplicated eLoc "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs] - walk [] = caseTooComplicated curLoc "with-non-exhaustive-match" [] -- can't really happen + else do Env{curLoc} <- ask + choose (caseTooComplicated (eLoc : curLoc) "with-complicated-alternatives-during-merging") m result (walk rest) + Nothing -> do Env{curLoc} <- ask + caseTooComplicated (eLoc : curLoc) "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs] + walk [] = do Env{curLoc} <- ask + caseTooComplicated curLoc "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 choose bailOut t tb fb = case S.svAsBool t of @@ -363,11 +366,11 @@ 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 _ (Type t) = do Env{curLoc} <- ask - k <- getType curLoc t + k <- getType (pickSpan curLoc) t return (Typ k) tgo _ e@Coercion{} @@ -384,8 +387,8 @@ 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 + Nothing -> return (Var x) + Just (_, b) -> chaseVars b chaseVars (Tick _ x) = chaseVars x chaseVars x = return x func <- chaseVars rf @@ -405,29 +408,86 @@ isReallyADictionary (Var v) = "$" `isPrefixOf` unpackFS (occNameFS (occName (varName v))) isReallyADictionary _ = False +-- Create a symbolic variable. +mkSym :: Config -> Maybe Var -> SrcSpan -> Maybe Type -> SKind -> Maybe String -> Eval Val +mkSym cfg@Config{cfgEnv} mbBind curLoc mbBType = sym + where sh o = showSDoc (flags cfgEnv) (ppr o) + + tinfo k = case mbBType of + Nothing -> "Kind: " ++ sh k + Just t -> "Type: " ++ sh t + + sym (KBase k) nm = do v <- lift $ 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 Env{mbListSize} <- ask + let ls = fromMaybe bad mbListSize + bad = die cfg [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@KFun{} nm = case mbBind of + Just v -> uninterpret cfg True (varType v) v + _ -> die cfg [curLoc] "Unsupported unnamed higher-order symbolic input" + [ "Name: " ++ fromMaybe "" nm + , tinfo k + , "Hint: Name all higher-order inputs explicitly" + ] + + -- | Uninterpret an expression -uninterpret :: Type -> Var -> Eval Val -uninterpret t v = do +uninterpret :: Config -> Bool -> Type -> Var -> Eval Val +uninterpret cfg isInput t var = do 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) + case (var, t) `lookup` prevUninterpreted of + Just (_, _, val) -> return val + Nothing -> do let (tvs, t') = splitForAllTys t + (args, res) = splitFunTys t' + sp = getSrcSpan var + argKs <- mapM (getType sp) args + resK <- getType sp res + nm <- mkValidName $ showSDoc flags (ppr var) + body <- walk argKs (nm, resK) [] + let fVal = wrap tvs body + liftIO $ modifyIORef rUninterpreted (((var, t), (isInput, nm, fVal)) :) + return fVal + where walk :: [SKind] -> (String, SKind) -> [Val] -> Eval Val + walk [] (nm, k) args = do Env{curLoc, mbListSize} <- ask + + let ls = fromMaybe bad mbListSize + bad = die cfg curLoc "List-argument found in uninterpreted function, with no size info" + ["Hint: Use the \"ListSize\" annotation"] + + mkArg :: Val -> [S.SVal] + mkArg (Base v) = [v] + mkArg (Tup vs) = concatMap mkArg vs + mkArg (Lst vs) = concatMap mkArg vs + mkArg sk = error $ "Not yet supported uninterpreted function with a higher-order argument: " ++ showSDocUnsafe (ppr sk) + + bArgs = concatMap mkArg (reverse args) + + mkRes :: String -> SKind -> [S.SVal] + mkRes n (KBase b) = [S.svUninterpreted b n Nothing bArgs] + mkRes n (KTup bs) = concat $ zipWith mkRes [n ++ "_" ++ show i | i <- [(1 :: Int) .. ]] bs + mkRes n (KLst b) = concat [mkRes (n ++ "_" ++ show i) b | i <- [(1 :: Int) .. ls]] + mkRes _ sk = error $ "Not yet supported uninterpreted function with a higher-order result: " ++ showSDocUnsafe (ppr sk) + + res = map Base $ mkRes nm k + case res of + [x] -> return x + _ -> return $ Tup res + + walk (_:ks) nmk args = return $ Func Nothing $ \a -> walk ks nmk (a:args) wrap [] f = f wrap (_:ts) f = Func Nothing $ \(Typ _) -> return (wrap ts f) @@ -458,7 +518,7 @@ -- | 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 +getType sp typ = do let (tvs, typ') = splitForAllTys typ (args, res) = splitFunTys typ' argKs <- mapM (getType sp) args resK <- getComposite res 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 @@ -10,6 +10,8 @@ ----------------------------------------------------------------------------- {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Data.SBV.Plugin.Common where @@ -36,18 +38,19 @@ } -- | Interpreter environment -data Env = Env { curLoc :: SrcSpan +data Env = Env { curLoc :: [SrcSpan] , flags :: DynFlags , machWordSize :: Int + , mbListSize :: Maybe Int , uninteresting :: [Type] - , rUninterpreted :: IORef [((Var, Type), (String, Val))] + , rUninterpreted :: IORef [((Var, Type), (Bool, String, Val))] , rUsedNames :: IORef [String] , rUITypes :: IORef [(Type, S.Kind)] , 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 + , coreMap :: M.Map Var (SrcSpan, CoreExpr) } @@ -138,15 +141,38 @@ ] -- | 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 -tickSpan (SourceNote s _) _ = RealSrcSpan s -tickSpan _ s = s +tickSpan :: Tickish t -> SrcSpan +tickSpan (ProfNote cc _ _) = cc_loc cc +tickSpan (SourceNote s _) = RealSrcSpan s +tickSpan _ = noSrcSpan -- | Compute the span for a binding. -bindSpan :: Var -> SrcSpan -bindSpan = nameSrcSpan . varName +varSpan :: Var -> SrcSpan +varSpan = nameSrcSpan . varName --- | Show a GHC span in user-friendly form. -showSpan :: Config -> Var -> SrcSpan -> String -showSpan Config{cfgEnv} b s = showSDoc (flags cfgEnv) $ if isGoodSrcSpan s then ppr s else ppr b +-- | Pick the first "good" span, hopefully corresponding to +-- the closest location to where we are in the code +-- when we issue an error message. +pickSpan :: [SrcSpan] -> SrcSpan +pickSpan ss = case filter isGoodSrcSpan ss of + (s:_) -> s + [] -> noSrcSpan + +-- | Show a GHC span in user-friendly form +showSpan :: Config -> SrcSpan -> String +showSpan Config{cfgEnv} s = showSDoc (flags cfgEnv) (ppr s) + +-- | This comes mighty handy! Wonder why GHC doesn't have it already: +instance Show CoreExpr where + show = go + where sh x = showSDocUnsafe (ppr x) + go (Var i) = "(Var " ++ sh i ++ ")" + go (Lit l) = "(Lit " ++ sh l ++ ")" + go (App f a) = "(App " ++ go f ++ " " ++ go a ++ ")" + go (Lam b e) = "(Lam " ++ sh b ++ " " ++ go e ++ ")" + go (Let b e) = "(Let " ++ sh b ++ " " ++ go e ++ ")" + go (Case e b t _) = "(Case " ++ go e ++ " " ++ sh b ++ " " ++ sh t ++ "...)" + go (Cast e _) = "(Cast " ++ go e ++ " ...)" + go (Tick _ e) = "(Tick " ++ go e ++ ")" + go (Type t) = "(Type " ++ sh t ++ ")" + go (Coercion _) = "(Coercion ...)" 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 @@ -32,7 +32,6 @@ 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] @@ -108,9 +107,15 @@ ++ [ (op, tlift2 (KBase k), lift2 sOp) | k <- bvKinds, (op, sOp) <- bvBinOps ] ++ [ (op, tlift2ShRot wsz (KBase k), lift2 sOp) | k <- bvKinds, (op, sOp) <- bvShiftRots] + -- bv-splits + ++ [('S.split, tSplit s, liftSplit s) | s <- [16, 32, 64]] + + -- bv-joins + ++ [ ('(S.#), tJoin s, lift2 S.svJoin) | s <- [8, 16, 32]] + where -- Bit-vectors - bvKinds = [S.KBounded s sz | s <- [False, True], sz <- [8, 16, 32, 64]] + bvKinds = [S.KBounded s sz | s <- [False, True], sz <- [8, 16, 32, 64]] -- Those that are "integral"ish integralKinds = S.KUnbounded : bvKinds @@ -262,6 +267,18 @@ tlift2ShRot :: Int -> SKind -> SKind tlift2ShRot wsz k = KFun k (KFun (KBase (S.KBounded True wsz)) k) +-- | Construct the type for a split operation +tSplit :: Int -> SKind +tSplit n = KFun a (KTup [r, r]) + where a = KBase (S.KBounded False n) + r = KBase (S.KBounded False (n `div` 2)) + +-- | Construct the type for a join operation +tJoin :: Int -> SKind +tJoin n = KFun a (KFun a r) + where a = KBase (S.KBounded False n) + r = KBase (S.KBounded False (n*2)) + -- | Lift a unary SBV function that via kind/integer lift1Int :: (Integer -> S.SVal) -> Val lift1Int f = Func Nothing g @@ -285,6 +302,16 @@ 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 splits +liftSplit :: Int -> Val +liftSplit n = Func Nothing g + where g (Typ _) = return $ Func Nothing g + g (Base a) = do let half = n `div` 2 + f = Base $ S.svExtract (n-1) half a + s = Base $ S.svExtract (half-1) 0 a + return $ Tup [f, s] + g v = error $ "Impossible happened: liftSplit received unexpected argument: " ++ showSDocUnsafe (ppr (n, v)) -- | Lifting an equality is special; since it acts uniformly over tuples. liftEq :: (S.SVal -> S.SVal -> S.SVal) -> Val diff --git a/Data/SBV/Plugin/Examples/BitTricks.hs b/Data/SBV/Plugin/Examples/BitTricks.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Plugin/Examples/BitTricks.hs @@ -0,0 +1,73 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Plugin.Examples.BitTricks +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Checks the correctness of a few tricks from the large collection found in: +-- +----------------------------------------------------------------------------- + +{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} + +module Data.SBV.Plugin.Examples.BitTricks where + +import Data.SBV.Plugin + +import Data.Bits +import Data.Word + +-- | Returns 1 if bool is @True@ +oneIf :: Num a => Bool -> a +oneIf True = 1 +oneIf False = 0 + +-- | Formalizes +{-# ANN fastMinCorrect theorem #-} +fastMinCorrect :: Int -> Int -> Bool +fastMinCorrect x y = m == fm + where m = if x < y then x else y + fm = y `xor` ((x `xor` y) .&. (-(oneIf (x < y)))); + +-- | Formalizes +{-# ANN fastMaxCorrect theorem #-} +fastMaxCorrect :: Int -> Int -> Bool +fastMaxCorrect x y = m == fm + where m = if x < y then y else x + fm = x `xor` ((x `xor` y) .&. (-(oneIf (x < y)))); + +-- | Formalizes +{-# ANN oppositeSignsCorrect theorem #-} +oppositeSignsCorrect :: Int -> Int -> Bool +oppositeSignsCorrect x y = r == os + where r = (x < 0 && y >= 0) || (x >= 0 && y < 0) + os = (x `xor` y) < 0 + +-- | Formalizes +{-# ANN conditionalSetClearCorrect theorem #-} +conditionalSetClearCorrect :: Bool -> Word32 -> Word32 -> Bool +conditionalSetClearCorrect f m w = r == r' + where r | f = w .|. m + | True = w .&. complement m + r' = w `xor` ((-(oneIf f) `xor` w) .&. m) + +-- | Formalizes +{-# ANN powerOfTwoCorrect theorem #-} +powerOfTwoCorrect :: Word32 -> Bool +powerOfTwoCorrect v = f == search powers + where f = (v /= 0) && ((v .&. (v-1)) == 0) + + powers :: [Word32] + powers = [ 1, 2, 4, 8, 16, 32, 64, 128 + , 256, 512, 1024, 2048, 4096, 8192, 16384, 32768 + , 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608 + , 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648 + ] + + search :: [Word32] -> Bool + search [] = False + search (x:xs) + | x == v = True + | True = search xs diff --git a/Data/SBV/Plugin/Examples/MergeSort.hs b/Data/SBV/Plugin/Examples/MergeSort.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Plugin/Examples/MergeSort.hs @@ -0,0 +1,101 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Plugin.Examples.MergeSort +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- An implementation of merge-sort and its correctness. +----------------------------------------------------------------------------- +-- +{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} + +module Data.SBV.Plugin.Examples.MergeSort where + +import Data.SBV.Plugin + +----------------------------------------------------------------------------- +-- * Implementing merge-sort +-- ${mergeSort} +----------------------------------------------------------------------------- +{- $mergeSort +A straightforward implementation of merge sort. We simply divide the input list +in to two halves so long as it has at least two elements, sort each half on its +own, and then merge. +-} + +-- | Merging two given sorted lists, preserving the order. +merge :: Ord a => [a] -> [a] -> [a] +merge [] ys = ys +merge xs [] = xs +merge xs@(x:xr) ys@(y:yr) + | x < y = x : merge xr ys + | True = y : merge xs yr + +-- | Simple merge-sort implementation. +mergeSort :: Ord a => [a] -> [a] +mergeSort [] = [] +mergeSort [x] = [x] +mergeSort xs = merge (mergeSort th) (mergeSort bh) + where (th, bh) = split xs ([], []) + split :: [a] -> ([a], [a]) -> ([a], [a]) + split [] sofar = sofar + split (a:as) (fs, ss) = split as (ss, a:fs) + +----------------------------------------------------------------------------- +-- * Proving correctness of sorting +-- ${props} +----------------------------------------------------------------------------- +{- $props +There are two main parts to proving that a sorting algorithm is correct: + + * Prove that the output is non-decreasing + + * Prove that the output is a permutation of the input +-} + +-- | Check whether a given sequence is non-decreasing. +nonDecreasing :: Ord a => [a] -> Bool +nonDecreasing [] = True +nonDecreasing [_] = True +nonDecreasing (a:b:xs) = a <= b && nonDecreasing (b:xs) + +-- | Check whether two given sequences are permutations. We simply check that each sequence +-- is a subset of the other, when considered as a set. The check is slightly complicated +-- for the need to account for possibly duplicated elements. +isPermutationOf :: Eq a => [a] -> [a] -> Bool +isPermutationOf as bs = go as [(b, True) | b <- bs] && go bs [(a, True) | a <- as] + where go :: Eq a => [a] -> [(a, Bool)] -> Bool + go [] _ = True + go (x:xs) ys = found && go xs ys' + where (found, ys') = mark x ys + + -- Go and mark off an instance of 'x' in the list, if possible. We keep track + -- of unmarked elements by associating a boolean bit. Note that we have to + -- keep the lists equal size for the recursive result to merge properly. + mark :: Eq a => a -> [(a, Bool)] -> (Bool, [(a, Bool)]) + mark _ [] = (False, []) + mark x ((y, v) : ys) + | v && x == y = (True, (y, not v) : ys) + | True = (r, (y, v) : ys') + where (r, ys') = mark x ys + +----------------------------------------------------------------------------- +-- * The correctness theorem +----------------------------------------------------------------------------- + +-- | Asserting correctness of merge-sort for a list of the given size. Note that we can +-- only check correctness for fixed-size lists. Also, the proof will get more and more +-- complicated for the backend SMT solver as 'n' increases. Here we try it with 4. +-- +-- We have: +-- +-- @ +-- [SBV] tests/T48.hs:100:1-16 Proving "mergeSortCorrect", using Z3. +-- [Z3] Q.E.D. +-- @ +{-# ANN mergeSortCorrect theorem { options = [ListSize 4] } #-} +mergeSortCorrect :: [Int] -> Bool +mergeSortCorrect xs = nonDecreasing ys && isPermutationOf xs ys + where ys = mergeSort xs 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 @@ -66,9 +66,10 @@ let cfg = Config { isGHCi = hscTarget df == HscInterpreted , opts = [] , sbvAnnotation = lookupWithDefaultUFM anns [] . varUnique - , cfgEnv = Env { curLoc = noSrcSpan + , cfgEnv = Env { curLoc = [] , flags = df , machWordSize = wsz + , mbListSize = Nothing , uninteresting = uninteresting , rUninterpreted = rUninterpreted , rUsedNames = rUsedNames @@ -77,13 +78,13 @@ , tcMap = baseTCs , envMap = baseEnv , destMap = baseDests - , coreMap = M.fromList (flattenBinds mg_binds) + , coreMap = M.fromList [(b, (varSpan b, e)) | (b, e) <- flattenBinds mg_binds] } } - let bindLoc (NonRec b _) = bindSpan b + let bindLoc (NonRec b _) = varSpan b bindLoc (Rec []) = noSrcSpan - bindLoc (Rec ((b, _):_)) = bindSpan b + bindLoc (Rec ((b, _):_)) = varSpan b mapM_ (analyzeBind cfg) $ sortBy (comparing bindLoc) mg_binds diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -1,5 +1,5 @@ Name : sbvPlugin -Version : 0.4 +Version : 0.5 Category : Formal methods, Theorem provers, Math, SMT, Symbolic Computation Synopsis : Formally prove properties of Haskell programs using SBV/SMT Description : GHC plugin for proving properties over Haskell functions using SMT solvers, based @@ -16,7 +16,6 @@ Maintainer : Levent Erkok (erkokl@gmail.com) Build-Type : Simple Cabal-Version : >= 1.14 -Data-Files : tests/GoldFiles/*.hs.golden Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md source-repository head @@ -27,7 +26,9 @@ default-language: Haskell2010 ghc-options : -Wall -fplugin-opt Data.SBV.Plugin:skip Exposed-modules : Data.SBV.Plugin + , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController + , Data.SBV.Plugin.Examples.BitTricks 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 diff --git a/tests/GoldFiles/T00.hs.golden b/tests/GoldFiles/T00.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T00.hs.golden +++ /dev/null @@ -1,8 +0,0 @@ - -[SBV] tests/T00.hs:12:1 Proving "f", using Z3. -[Z3] Q.E.D. - -[SBV] tests/T00.hs:16:1 Proving "g", using Z3. -[Z3] Falsifiable. Counter-example: - _x = 0 :: Int8 - _y = False :: Bool diff --git a/tests/GoldFiles/T01.hs.golden b/tests/GoldFiles/T01.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T01.hs.golden +++ /dev/null @@ -1,7 +0,0 @@ - -[SBV] tests/T01.hs:9:1 Proving "f", using Z3. -[Z3] Falsifiable. Counter-example: - x = 40959.98499298095 :: Double - y = -73732.00109529495 :: Double - z = 257.9890136271454 :: Double -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T02.hs.golden b/tests/GoldFiles/T02.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T02.hs.golden +++ /dev/null @@ -1,5 +0,0 @@ - -[SBV] tests/T02.hs:9:1 Proving "f", using Z3. -[Z3] Falsifiable. Counter-example: - x = 1 :: Integer - y = 0 :: Integer diff --git a/tests/GoldFiles/T03.hs.golden b/tests/GoldFiles/T03.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T03.hs.golden +++ /dev/null @@ -1,3 +0,0 @@ - -[SBV] tests/T03.hs:10:1 Proving "f", using Z3. -[Z3] Q.E.D. diff --git a/tests/GoldFiles/T04.hs.golden b/tests/GoldFiles/T04.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T04.hs.golden +++ /dev/null @@ -1,3 +0,0 @@ - -[SBV] tests/T04.hs:10:1 Proving "f", using Z3. -[Z3] Q.E.D. diff --git a/tests/GoldFiles/T05.hs.golden b/tests/GoldFiles/T05.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T05.hs.golden +++ /dev/null @@ -1,5 +0,0 @@ - -[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/T06.hs.golden b/tests/GoldFiles/T06.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T06.hs.golden +++ /dev/null @@ -1,5 +0,0 @@ - -[SBV] tests/T06.hs:10:1 Proving "f", using Z3. -[Z3] Falsifiable. Counter-example: - x = -128 :: Int8 -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T07.hs.golden b/tests/GoldFiles/T07.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T07.hs.golden +++ /dev/null @@ -1,5 +0,0 @@ - -[SBV] tests/T07.hs:9:1 Proving "f", using Z3. -[Z3] Falsifiable. Counter-example: - x = NaN :: Double -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T08.hs.golden b/tests/GoldFiles/T08.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T08.hs.golden +++ /dev/null @@ -1,5 +0,0 @@ - -[SBV] tests/T08.hs:9:1 Proving "f", using Z3. -[Z3] Falsifiable. Counter-example: - x = 0.0 :: Double -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T09.hs.golden b/tests/GoldFiles/T09.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T09.hs.golden +++ /dev/null @@ -1,3 +0,0 @@ - -[SBV] tests/T09.hs:10:1 QuickChecking "f", using Z3. -(0 tests) (1 test) (2 tests) (3 tests) (4 tests) (5 tests) (6 tests) (7 tests) (8 tests) (9 tests) (10 tests) (11 tests) (12 tests) (13 tests) (14 tests) (15 tests) (16 tests) (17 tests) (18 tests) (19 tests) (20 tests) (21 tests) (22 tests) (23 tests) (24 tests) (25 tests) (26 tests) (27 tests) (28 tests) (29 tests) (30 tests) (31 tests) (32 tests) (33 tests) (34 tests) (35 tests) (36 tests) (37 tests) (38 tests) (39 tests) (40 tests) (41 tests) (42 tests) (43 tests) (44 tests) (45 tests) (46 tests) (47 tests) (48 tests) (49 tests) (50 tests) (51 tests) (52 tests) (53 tests) (54 tests) (55 tests) (56 tests) (57 tests) (58 tests) (59 tests) (60 tests) (61 tests) (62 tests) (63 tests) (64 tests) (65 tests) (66 tests) (67 tests) (68 tests) (69 tests) (70 tests) (71 tests) (72 tests) (73 tests) (74 tests) (75 tests) (76 tests) (77 tests) (78 tests) (79 tests) (80 tests) (81 tests) (82 tests) (83 tests) (84 tests) (85 tests) (86 tests) (87 tests) (88 tests) (89 tests) (90 tests) (91 tests) (92 tests) (93 tests) (94 tests) (95 tests) (96 tests) (97 tests) (98 tests) (99 tests) +++ OK, passed 100 tests. diff --git a/tests/GoldFiles/T10.hs.golden b/tests/GoldFiles/T10.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T10.hs.golden +++ /dev/null @@ -1,3 +0,0 @@ - -[SBV] tests/T10.hs:12:1 Proving "f", using Z3. -[Z3] Q.E.D. diff --git a/tests/GoldFiles/T11.hs.golden b/tests/GoldFiles/T11.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T11.hs.golden +++ /dev/null @@ -1,5 +0,0 @@ - -[SBV] tests/T11.hs:15:1 Proving "f", using Z3. -[Z3] Falsifiable. Counter-example: - x = 11 :: Integer -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T12.hs.golden b/tests/GoldFiles/T12.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T12.hs.golden +++ /dev/null @@ -1,6 +0,0 @@ - -[SBV] tests/T12.hs:9:1 Proving "f", using Z3. -[Z3] Falsifiable. Counter-example: - i = 2 :: Integer - b = False :: Bool -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T13.hs.golden b/tests/GoldFiles/T13.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T13.hs.golden +++ /dev/null @@ -1,7 +0,0 @@ - -[SBV] tests/T13.hs:9:1 Proving "f", using Z3. -[Z3] Falsifiable. Counter-example: - i = 0 :: Integer - d = 0.0 :: Double - b = False :: Bool -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T14.hs.golden b/tests/GoldFiles/T14.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T14.hs.golden +++ /dev/null @@ -1,5 +0,0 @@ - -[SBV] tests/T14.hs:10:1 Proving "f", using Z3. -[Z3] Falsifiable. Counter-example: - x = 1.0 :: Real -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T15.hs.golden b/tests/GoldFiles/T15.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T15.hs.golden +++ /dev/null @@ -1,3 +0,0 @@ - -[SBV] tests/T15.hs:11:1 Proving "f", using Z3. -[Z3] Q.E.D. diff --git a/tests/GoldFiles/T16.hs.golden b/tests/GoldFiles/T16.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T16.hs.golden +++ /dev/null @@ -1,7 +0,0 @@ - -[SBV] tests/T16.hs:11:1 Proving "f", using Z3. -[Z3] Falsifiable. Counter-example: - age = Age!val!0 :: Age -[SBV] Counter-example might be bogus due to uninterpreted constant: - [] ds_d6ck :: Int -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T17.hs.golden b/tests/GoldFiles/T17.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T17.hs.golden +++ /dev/null @@ -1,7 +0,0 @@ - -[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: - [tests/T17.hs:9:1] g :: Int -> Int -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T18.hs.golden b/tests/GoldFiles/T18.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T18.hs.golden +++ /dev/null @@ -1,59 +0,0 @@ - -[SBV] tests/T18.hs:11:1 Proving "f", using Z3. -** Starting symbolic simulation.. -** Generated symbolic trace: -SORTS - Age -INPUTS - s0 :: Age, aliasing "a" - s1 :: Age, aliasing "b" -CONSTANTS - s_2 = False :: Bool - s_1 = True :: Bool -TABLES -ARRAYS -UNINTERPRETED CONSTANTS -USER GIVEN CODE SEGMENTS -AXIOMS -DEFINE - s2 :: SBool = s0 == s1 -CONSTRAINTS -ASSERTIONS -OUTPUTS - s2 -** 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: tests/T18.hs:11:3 -; --- literal constants --- -(define-fun s_2 () Bool false) -(define-fun s_1 () Bool true) -; --- skolem constants --- -(declare-fun s0 () Age) ; tracks user variable "a" -(declare-fun s1 () Age) ; tracks user variable "b" -; --- constant tables --- -; --- skolemized tables --- -; --- arrays --- -; --- uninterpreted constants --- -; --- user given axioms --- -; --- formula --- -(assert ; no quantifiers - (let ((s2 (= s0 s1))) - (not s2))) -** Calling: "z3 -nw -in -smt2" -** Sending the following model extraction commands: -(get-value (s0)) -(get-value (s1)) -** Z3 output: -sat -((s0 Age!val!0)) -((s1 Age!val!1)) -** Done.. -[Z3] Falsifiable. Counter-example: - a = Age!val!0 :: Age - b = Age!val!1 :: Age -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T19.hs.golden b/tests/GoldFiles/T19.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T19.hs.golden +++ /dev/null @@ -1,14 +0,0 @@ - -[SBV] tests/T19.hs:9:1 Proving "f", using Z3. -[Z3] Q.E.D. - -[SBV] tests/T19.hs:15:1 Proving "g", using Z3. -[Z3] Falsifiable. Counter-example: - 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: - [] C# :: Char# -> Char diff --git a/tests/GoldFiles/T20.hs.golden b/tests/GoldFiles/T20.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T20.hs.golden +++ /dev/null @@ -1,1 +0,0 @@ -[SBV] tests/T20.hs:10:1 Skipping "f": Don't want to prove this now. diff --git a/tests/GoldFiles/T21.hs.golden b/tests/GoldFiles/T21.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T21.hs.golden +++ /dev/null @@ -1,36 +0,0 @@ - -[SBV] tests/T21.hs:9:1 Proving "f", 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) -; has user-defined sorts, no logic specified. -; --- uninterpreted sorts --- -(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 () 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 --- -; --- 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/T22.hs.golden b/tests/GoldFiles/T22.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T22.hs.golden +++ /dev/null @@ -1,5 +0,0 @@ - -[SBV] tests/T22.hs:12:1 Proving "g", using Z3. -[Z3] Falsifiable. Counter-example: - s0 = -1 :: Int64 -[SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T23.hs.golden b/tests/GoldFiles/T23.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T23.hs.golden +++ /dev/null @@ -1,3 +0,0 @@ - -[SBV] tests/T23.hs:9:1 Proving "f", using Z3. -[Z3] Q.E.D. diff --git a/tests/GoldFiles/T24.hs.golden b/tests/GoldFiles/T24.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T24.hs.golden +++ /dev/null @@ -1,3 +0,0 @@ - -[SBV] tests/T24.hs:10:1 Proving "f", using Z3. -[Z3] Q.E.D. diff --git a/tests/GoldFiles/T25.hs.golden b/tests/GoldFiles/T25.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T25.hs.golden +++ /dev/null @@ -1,3 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T26.hs.golden +++ /dev/null @@ -1,4 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T27.hs.golden +++ /dev/null @@ -1,29 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T28.hs.golden +++ /dev/null @@ -1,3 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T29.hs.golden +++ /dev/null @@ -1,4 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T30.hs.golden +++ /dev/null @@ -1,3 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T31.hs.golden +++ /dev/null @@ -1,19 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T32.hs.golden +++ /dev/null @@ -1,7 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T33.hs.golden +++ /dev/null @@ -1,7 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T34.hs.golden +++ /dev/null @@ -1,3 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T35.hs.golden +++ /dev/null @@ -1,6 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T36.hs.golden +++ /dev/null @@ -1,9 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T37.hs.golden +++ /dev/null @@ -1,6 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T38.hs.golden +++ /dev/null @@ -1,7 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T39.hs.golden +++ /dev/null @@ -1,6 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T40.hs.golden +++ /dev/null @@ -1,3 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T41.hs.golden +++ /dev/null @@ -1,8 +0,0 @@ - -[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 deleted file mode 100644 --- a/tests/GoldFiles/T42.hs.golden +++ /dev/null @@ -1,9 +0,0 @@ - -[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.) diff --git a/tests/GoldFiles/T43.hs.golden b/tests/GoldFiles/T43.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T43.hs.golden +++ /dev/null @@ -1,21 +0,0 @@ - -[SBV] tests/T43.hs:13:1 Proving "t", using Z3. -[Z3] Q.E.D. - -[SBV] tests/T43.hs:19:1 Proving "r", using Z3. - -[SBV] tests/T43.hs:19:1 Skipping proof. Unsupported case-expression (with-complicated-alternatives-during-merging): - case == @ Int $fEqInt x (I# 0) of _ [Occ=Dead] { - False -> - (\ _ [Occ=Dead, OS=OneShot] -> - : @ Int x (: @ Int x (: @ Int x (: @ Int x ([] @ Int))))) - void#; - True -> : @ Int x (: @ Int x (: @ Int x ([] @ Int))) -} - While Analyzing: - Alternatives are producing lists of differing sizes: - Length 4: [ :: SInt64, - :: SInt64, - :: SInt64, - :: SInt64] - vs Length 3: [ :: SInt64, :: SInt64, :: SInt64] diff --git a/tests/GoldFiles/T44.hs.golden b/tests/GoldFiles/T44.hs.golden deleted file mode 100644 --- a/tests/GoldFiles/T44.hs.golden +++ /dev/null @@ -1,9 +0,0 @@ - -[SBV] tests/T44.hs:12:1 Proving "t", using Z3. -[Z3] Q.E.D. - -[SBV] tests/T44.hs:20:1 Proving "r", using Z3. -[Z3] Falsifiable. Counter-example: - b = False :: Bool - x = 0 :: Integer - y = -1 :: Integer