packages feed

sbvPlugin 0.1 → 0.2

raw patch · 35 files changed

+804/−566 lines, 35 filesdep ~sbv

Dependency ranges changed: sbv

Files

CHANGES.md view
@@ -1,10 +1,18 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub:  <http://github.com/LeventErkok/sbvPlugin> -* 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!
Data/SBV/Plugin.hs view
@@ -9,15 +9,14 @@ -- (The sbvPlugin is hosted at <http://github.com/LeventErkok/sbvPlugin>. -- 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 -- -- <http://github.com/LeventErkok/sbv SBV> 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
Data/SBV/Plugin/Analyze.hs view
@@ -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
Data/SBV/Plugin/Common.hs view
@@ -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
Data/SBV/Plugin/Data.hs view
@@ -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
Data/SBV/Plugin/Env.hs view
@@ -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
Data/SBV/Plugin/Plugin.hs view
@@ -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
sbvPlugin.cabal view
@@ -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
tests/GoldFiles/T05.hs.golden view
@@ -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
tests/GoldFiles/T13.hs.golden view
@@ -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.)
tests/GoldFiles/T15.hs.golden view
@@ -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: <no location info>-; --- 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.
tests/GoldFiles/T16.hs.golden view
@@ -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: <no location info>-; --- 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:+  [<no location info>] ds_d6ci :: Int [SBV] Failed. (Use option 'IgnoreFailure' to continue.)
tests/GoldFiles/T17.hs.golden view
@@ -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:
tests/GoldFiles/T18.hs.golden view
@@ -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:-  [<no location info>] == :: Age -> Age -> Bool [SBV] Failed. (Use option 'IgnoreFailure' to continue.)
tests/GoldFiles/T19.hs.golden view
@@ -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:-  [<no location info>] ==      :: [Char] -> [Char] -> Bool-  [<no location info>] reverse :: [Char] -> [Char]-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)+  [<wired into compiler>] C# :: Char# -> Char
tests/GoldFiles/T21.hs.golden view
@@ -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:-  [<no location info>] == :: String -> String -> Bool-  [<no location info>] == :: Char -> Char -> Bool-[SBV] Failed. (Use option 'IgnoreFailure' to continue.)+[Z3] Q.E.D.
tests/GoldFiles/T22.hs.golden view
@@ -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:-  [<no location info>] ==      :: [Char] -> [Char] -> Bool-  [<no location info>] reverse :: [Char] -> [Char]+  s0 = -1 :: Int64 [SBV] Failed. (Use option 'IgnoreFailure' to continue.)
+ tests/GoldFiles/T25.hs.golden view
@@ -0,0 +1,3 @@++[SBV] tests/T25.hs:9:1 Proving "f", using Z3.+[Z3] Q.E.D.
+ tests/GoldFiles/T26.hs.golden view
@@ -0,0 +1,4 @@++[SBV] tests/T26.hs:9:1 Proving "f", using Z3.+[Z3] Falsifiable+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
+ tests/GoldFiles/T27.hs.golden view
@@ -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.
+ tests/GoldFiles/T28.hs.golden view
@@ -0,0 +1,3 @@++[SBV] tests/T28.hs:13:1 Proving "g", using Z3.+[Z3] Q.E.D.
+ tests/GoldFiles/T29.hs.golden view
@@ -0,0 +1,4 @@++[SBV] tests/T29.hs:13:1 Proving "g", using Z3.+[Z3] Falsifiable+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
+ tests/GoldFiles/T30.hs.golden view
@@ -0,0 +1,3 @@++[SBV] tests/T30.hs:9:1 Proving "f", using Z3.+[Z3] Q.E.D.
+ tests/GoldFiles/T31.hs.golden view
@@ -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
+ tests/GoldFiles/T32.hs.golden view
@@ -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
+ tests/GoldFiles/T33.hs.golden view
@@ -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.
+ tests/GoldFiles/T34.hs.golden view
@@ -0,0 +1,3 @@++[SBV] tests/T34.hs:9:1 Proving "f", using Z3.+[Z3] Q.E.D.
+ tests/GoldFiles/T35.hs.golden view
@@ -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.)
+ tests/GoldFiles/T36.hs.golden view
@@ -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
+ tests/GoldFiles/T37.hs.golden view
@@ -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.)
+ tests/GoldFiles/T38.hs.golden view
@@ -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.)
+ tests/GoldFiles/T39.hs.golden view
@@ -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.)
+ tests/GoldFiles/T40.hs.golden view
@@ -0,0 +1,3 @@++[SBV] tests/T40.hs:9:1 Proving "f", using Z3.+[Z3] Q.E.D.
+ tests/GoldFiles/T41.hs.golden view
@@ -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
+ tests/GoldFiles/T42.hs.golden view
@@ -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.)