packages feed

sbvPlugin (empty) → 0.1

raw patch · 39 files changed

+1446/−0 lines, 39 filesdep +basedep +containersdep +directorysetup-changed

Dependencies added: base, containers, directory, filepath, ghc, ghc-prim, mtl, process, sbv, sbvPlugin, tasty, tasty-golden, template-haskell

Files

+ CHANGES.md view
@@ -0,0 +1,10 @@+* Hackage: <http://hackage.haskell.org/package/sbvPlugin>+* GitHub:  <http://github.com/LeventErkok/sbvPlugin>++* Latest Hackage released version: 0.1, 2015-12-06++### 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!
@@ -0,0 +1,5 @@+Copyright (c) 2010-2015, Levent Erkok (erkokl@gmail.com)+All rights reserved.++The sbvPlugin is distributed with the BSD3 license. See the LICENSE file+for details.
+ Data/SBV/Plugin.hs view
@@ -0,0 +1,61 @@+---------------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Plugin+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- (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+--+-- <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:+--+--  > {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}+--  >+--  > module Test where+--  >+--  > import Data.SBV.Plugin+--  >+--  > {-# ANN test theorem #-}+--  > test :: Integer -> Integer -> Bool+--  > test x y = x + y >= x - y+--+-- We have:+--+--  > $ ghc -c Test.hs+--  >+--  > [SBV] Test.hs:9:1-4 Proving "test", using Z3.+--  > [Z3] Falsifiable. Counter-example:+--  >   x =  0 :: Integer+--  >   y = -1 :: Integer+--  > [SBV] Failed. (Use option 'IgnoreFailure' to continue.)+--+-- Note that the compilation will be aborted, since the theorem doesn't hold. As shown in the hint, GHC+-- can be instructed to continue in that case, using an annotation of the form:+--+-- > {-# ANN test theorem {options = [IgnoreFailure]} #-}+--+-- 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+-- the load process.+---------------------------------------------------------------------------------+module Data.SBV.Plugin(+       -- * Entry point+         plugin+       -- * Annotations+       , SBVAnnotation(..)+       , sbv, theorem+       -- * Plugin options+       , SBVOption(..)+       ) where++import Data.SBV.Plugin.Plugin+import Data.SBV.Plugin.Data
+ Data/SBV/Plugin/Analyze.hs view
@@ -0,0 +1,367 @@+---------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Plugin.Analyze+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- Walk the GHC Core, proving theorems/checking safety as they are found+-----------------------------------------------------------------------------++{-# LANGUAGE NamedFieldPuns       #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++module Data.SBV.Plugin.Analyze (analyzeBind) where++import GhcPlugins++import Control.Monad.Reader+import System.Exit hiding (die)++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 qualified Data.Map as M++import qualified Data.SBV           as S hiding (proveWith, proveWithAny)+import qualified Data.SBV.Dynamic   as S+import qualified Data.SBV.Internals as S++import qualified Control.Exception as C++import Data.SBV.Plugin.Common+import Data.SBV.Plugin.Data++-- | Dispatch the analyzer over bindings+analyzeBind :: Config -> CoreBind -> CoreM ()+analyzeBind cfg@Config{sbvAnnotation} = 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"+                 | Uninterpret `elem` opts = return ()+                 | True                    = liftIO $ prove cfg opts b topLoc 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+        unless (success || isGHCi || IgnoreFailure `elem` opts) $ do+            putStrLn $ "[SBV] Failed. (Use option '" ++ show IgnoreFailure ++ "' to continue.)" +            exitFailure++-- | Safely execute an action, catching the exceptions, printing and returning False if something goes wrong+safely :: IO Bool -> IO Bool+safely a = a `C.catch` bad+  where bad :: C.SomeException -> IO Bool+        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+        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+            slvrTag = ", using " ++ tag ++ "."+              where tag = case solverConfigs of+                            []     -> "no solvers"  -- can't really happen+                            [x]    -> show x+                            [x, y] -> show x ++ " and " ++ show y+                            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+                        return (finalResult, finalUninterps)+        case finalResult of+          Right (solver, sres@(S.ThmResult smtRes)) -> do+                let success = case smtRes of+                                S.Unsatisfiable{} -> True+                                S.Satisfiable{}   -> False+                                S.Unknown{}       -> False   -- conservative+                                S.ProofError{}    -> False   -- conservative+                                S.TimeOut{}       -> False   -- conservative+                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+                        let plu | length finalUninterps > 1 = "s:"+                                | True                      = ":"+                            shUI (e, t) = (showSDoc (dflags cfg) (ppr (getSrcSpan e)), sh e, sh t)+                            ls   = map shUI unintFuns+                            len1 = maximum (0 : [length s | (s, _, _) <- ls])+                            len2 = maximum (0 : [length s | (_, s, _) <- ls])+                            pad n s = take n (s ++ repeat ' ')+                            put (a, b, c) = putStrLn $ "  [" ++ pad len1 a ++ "] " ++ pad len2 b ++ " :: " ++ c+                        putStrLn $ "[SBV] Counter-example might be bogus due to uninterpreted constant" ++ plu+                        mapM_ put ls++                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+                                                    }+               case v of+                 Base r -> return r+                 Func{} -> error "Impossible happened. Final result reduced to a non-base value!"++        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++        sh o = showSDoc (dflags cfg) (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)++        isUninterpretedBinding :: Var -> Bool+        isUninterpretedBinding v = any (Uninterpret `elem`) [opt | SBV opt <- sbvAnnotation v]++        go :: CoreExpr -> Eval Val+        go e = tgo (exprType e) e++        -- Main symbolic evaluator:+        tgo :: Type -> CoreExpr -> Eval Val++        -- tgo t e | trace ("--> " ++ show (sh (e, t))) False = undefined++        tgo t (Var v) = do Env{envMap, coreMap, specMap} <- ask+                           k <- getBaseType (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++        tgo t e@(Lit l) = do Env{machWordSize} <- ask+                             case l of+                               MachChar{}        -> unint+                               MachStr{}         -> unint+                               MachNullAddr      -> unint+                               MachLabel{}       -> unint+                               MachInt      i    -> return $ Base $ S.svInteger (S.KBounded True  machWordSize) i+                               MachInt64    i    -> return $ Base $ S.svInteger (S.KBounded True  64          ) i+                               MachWord     i    -> return $ Base $ S.svInteger (S.KBounded False machWordSize) i+                               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+                  where unint = do Env{flags} <- ask+                                   k  <- getBaseType noSrcSpan t+                                   nm <- mkValidName "lit" (showSDoc flags (ppr e))+                                   return $ Base $ S.svUninterpreted k nm Nothing []++        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 _ (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)]++        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)++        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 _ e@(Let _ _)+           = tbd "Unsupported let-binding with a recursive binder" [sh e]++        -- 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)+           = 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)+           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+                                     Nothing    -> do stb <- tb+                                                      sfb <- fb+                                                      case (stb, sfb) of+                                                        (Base a, Base b) -> return $ Base $ S.svIte t a b+                                                        _                -> 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++        tgo t (Cast e _)+           = tgo t 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 _ e@(Coercion{})+           = tbd "Unsupported coercion-expression" [sh e]++-- | 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))++-- not every name is good, sigh+mkValidName :: String -> String -> Eval String+mkValidName origin origName =+        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+  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 ++ "|"+        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 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
+ Data/SBV/Plugin/Common.hs view
@@ -0,0 +1,88 @@+---------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Plugin.Common+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- Common data-structures/utilities+-----------------------------------------------------------------------------++module Data.SBV.Plugin.Common where++import Control.Monad.Reader++import CostCentre+import GhcPlugins++import Data.Maybe (mapMaybe)+import qualified Data.Map as M++import Data.IORef++import qualified Data.SBV         as S+import qualified Data.SBV.Dynamic as S++import Data.SBV.Plugin.Data++-- | Interpreter environment+data Env = Env { curLoc         :: SrcSpan+               , flags          :: DynFlags+               , machWordSize   :: Int+               , rUninterpreted :: IORef [((Var, Type), String)]+               , 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+               }++-- | 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+                     , 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+                     }++-- | Given the user options, determine which solver(s) to use+pickSolvers :: [SBVOption] -> IO [S.SMTConfig]+pickSolvers slvrs+  | AnySolver `elem` slvrs = S.sbvAvailableSolvers+  | True                   = case mapMaybe (`lookup` solvers) slvrs of+                                [] -> return [S.defaultSMTCfg]+                                xs -> return xs+  where solvers = [ (Z3,        S.z3)+                  , (Yices,     S.yices)+                  , (Boolector, S.boolector)+                  , (CVC4,      S.cvc4)+                  , (MathSAT,   S.mathSAT)+                  , (ABC,       S.abc)+                  ]++-- | The values kept track of by the interpreter+data Val = Base S.SVal+         | Func (S.Kind, Maybe String) (S.SVal -> Eval Val)++-- | 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++-- | Compute the span for a binding.+bindSpan :: Var -> SrcSpan+bindSpan = nameSrcSpan . varName++-- | 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
+ Data/SBV/Plugin/Data.hs view
@@ -0,0 +1,48 @@+---------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Plugin.Data+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- Internal data-structures for the sbvPlugin+-----------------------------------------------------------------------------++{-# LANGUAGE DeriveDataTypeable #-}++module Data.SBV.Plugin.Data where++import Data.Data  (Data, Typeable)++-- | Plugin options. Note that we allow picking multiple solvers, which+-- will all be run in parallel. If you want to run all available solvers,+-- use the option 'AnySolver'. The default is to error-out on failure, using+-- the default-SMT solver picked by SBV, which is currently Z3.+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+               | QuickCheck     -- ^ Perform quickCheck+               | Uninterpret    -- ^ Uninterpret this binding for proof purposes+               | Names [String] -- ^ Use these names for the arguments; need not be exhaustive+               | Z3             -- ^ Use Z3+               | Yices          -- ^ Use Yices+               | Boolector      -- ^ Use Boolector+               | CVC4           -- ^ Use CVC4+               | MathSAT        -- ^ Use MathSAT+               | ABC            -- ^ Use ABC+               | AnySolver      -- ^ Use all installed solvers+               deriving (Show, Eq, Data, Typeable)++-- | The actual annotation.+newtype SBVAnnotation = SBV {options :: [SBVOption]}+                      deriving (Eq, Data, Typeable)++-- | A property annotation, using default options.+sbv :: SBVAnnotation+sbv = SBV {options = []}++-- | Synonym for sbv really, just looks cooler+theorem :: SBVAnnotation+theorem = sbv
+ Data/SBV/Plugin/Env.hs view
@@ -0,0 +1,166 @@+---------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Plugin.Env+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- The environment for mapping concrete functions/types to symbolic ones.+-----------------------------------------------------------------------------++{-# LANGUAGE MagicHash       #-}+{-# LANGUAGE TemplateHaskell #-}++module Data.SBV.Plugin.Env (buildFunEnv, buildTCEnv, buildSpecialEnv) where++import GhcPlugins+import GHC.Types++import qualified Data.Map            as M+import qualified Language.Haskell.TH as TH++import Data.Int+import Data.Word+import Data.Bits+import Data.Maybe (fromMaybe)+import Data.Ratio++import qualified Data.SBV         as S hiding (proveWith, proveWithAny)+import qualified Data.SBV.Dynamic as S++import Data.SBV.Plugin.Common++-- | Build the initial environment containing types+buildTCEnv :: Int -> CoreM (M.Map (TyCon, [TyCon]) S.Kind)+buildTCEnv isz = do xs <- mapM grabTyCon basics+                    ys <- mapM grabTyApp apps+                    return $ M.fromList $ xs ++ ys++  where grab x = do Just fn <- thNameToGhcName x+                    lookupTyCon fn++        grabTyCon (x, k) = grabTyApp (x, [], k)++        grabTyApp (x, as, k) = do fn   <- grab x+                                  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)+                 ]++        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)++         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)+                  ]++-- | 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)]]++          -- arithmetic+       ++ [(op, k, lift1 k sOp) | k <- arithKinds, (op, sOp) <- unaryOps]+       ++ [(op, k, lift2 k sOp) | k <- arithKinds, (op, sOp) <- binaryOps]++          -- literal conversions from Integer+       ++ [(op, k, lift1Int sOp) | k <- integerKinds, (op, sOp) <- [('fromInteger, S.svInteger k)]]++          -- comparisons+       ++ [(op, k, lift2 k 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)]]++         -- bit-vector+      ++ [ (op, k, lift2 k sOp) | k <- bvKinds, (op, sOp) <- bvBinOps]++ where+       -- Bit-vectors+       bvKinds    = [S.KBounded s sz | s <- [False, True], sz <- [8, 16, 32, 64]]++       -- Those that are "integral"ish+       integralKinds = S.KUnbounded : bvKinds++       -- Those that can be converted from an Integer+       integerKinds = S.KReal : integralKinds++       -- Float kinds+       floatKinds = [S.KFloat, S.KDouble]++       -- All arithmetic kinds+       arithKinds = floatKinds ++ integerKinds++       -- Everything+       allKinds   = S.KBool : arithKinds++       -- Unary arithmetic ops+       unaryOps   = [ ('abs,    S.svAbs)+                    , ('negate, S.svUNeg)+                    ]++       -- Binary arithmetic ops+       binaryOps  = [ ('(+), S.svPlus)+                    , ('(-), S.svMinus)+                    , ('(*), S.svTimes)+                    , ('(/), S.svDivide)+                    ]++       -- Comparisons+       compOps = [ ('(<),  S.svLessThan)+                 , ('(>),  S.svGreaterThan)+                 , ('(<=), S.svLessEq)+                 , ('(>=), S.svGreaterEq)+                 ]++       -- Binary bit-vector ops+       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++-- | Lift a unary SBV function that takes and integer value to the plugin value space+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)))++-- | 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))
+ Data/SBV/Plugin/Plugin.hs view
@@ -0,0 +1,69 @@+---------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Plugin.Analyze+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- Main entry point to the SBV Plugin+-----------------------------------------------------------------------------++{-# LANGUAGE NamedFieldPuns #-}++module Data.SBV.Plugin.Plugin(plugin) where++import GhcPlugins+import System.Exit++import Data.Maybe (fromJust)+import Data.List  (sortBy)+import Data.Ord   (comparing)+import Data.Bits  (bitSizeMaybe)++import qualified Data.Map as M++import Data.SBV.Plugin.Common+import Data.SBV.Plugin.Env+import Data.SBV.Plugin.Analyze (analyzeBind)++-- | Entry point to the plugin+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++       sbvPass = CoreDoPluginPass "SBV based analysis" pass++       pass :: ModGuts -> CoreM ModGuts+       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++          let cfg = Config { dflags        = df+                           , opts          = []+                           , wordSize      = wsz+                           , isGHCi        = hscTarget df == HscInterpreted+                           , knownTCs      = baseTCs+                           , knownFuns     = baseEnv+                           , knownSpecials = baseSpecials+                           , sbvAnnotation = lookupWithDefaultUFM anns [] . varUnique+                           , allBinds      = M.fromList (flattenBinds mg_binds)+                           }++          let bindLoc (NonRec b _)     = bindSpan b+              bindLoc (Rec [])         = noSrcSpan+              bindLoc (Rec ((b, _):_)) = bindSpan b++          mapM_ (analyzeBind cfg) $ sortBy (comparing bindLoc) mg_binds++          return guts
+ INSTALL view
@@ -0,0 +1,8 @@+The sbvPlugin can be installed simply by issuing cabal install:++     cabal install sbvPlugin++This will also install the SBV library if you do not already have it.+You should also install an SMT solver, preferably the default solver+used by SBV; i.e., Z3 from Microsoft: http://github.com/Z3Prover/z3.+Please make sure that the "z3" executable is in your path.
+ LICENSE view
@@ -0,0 +1,26 @@+sbvPlugin: SMT based analyzer for Haskell++Copyright (c) 2015, Levent Erkok (erkokl@gmail.com)+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:+    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.+    * Redistributions in binary form must reproduce the above copyright+      notice, this list of conditions and the following disclaimer in the+      documentation and/or other materials provided with the distribution.+    * Neither the name of the developer (Levent Erkok) nor the+      names of its contributors may be used to endorse or promote products+      derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL LEVENT ERKOK BE LIABLE FOR ANY+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,46 @@+## SBVPlugin: SBV Plugin for GHC++[![Hackage version](http://img.shields.io/hackage/v/sbvPlugin.svg?label=Hackage)](http://hackage.haskell.org/package/sbvPlugin)+    [![Build Status](http://img.shields.io/travis/LeventErkok/sbvPlugin.svg?label=Build)](http://travis-ci.org/LeventErkok/sbvPlugin)++### Example++```haskell+{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}++module Test where++import Data.SBV.Plugin++{-# ANN test theorem #-}+test :: Integer -> Integer -> Bool+test x y = x + y >= x - y+```++*Note the GHC option on the very first line. Either decorate your file with+this option, or pass `-fplugin=Data.SBV.Plugin` as an argument to GHC, either on the command line+or via cabal. Same trick also works for GHCi.*++When compiled or loaded in to ghci, we get:++```+$ ghc -c Test.hs++[SBV] Test.hs:9:1-4 Proving "test", using Z3.+[Z3] Falsifiable. Counter-example:+  x =  0 :: Integer+  y = -1 :: Integer+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)+```++Note that the compilation will be aborted, since the theorem doesn't hold. As shown in the hint, GHC+can be instructed to continue in that case, using an annotation of the form:++```haskell+{-# ANN test theorem {options = [IgnoreFailure]} #-}+```++### Using SBVPlugin 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` argument is given on all annotations, so that failures do not stop+the load process.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ sbvPlugin.cabal view
@@ -0,0 +1,42 @@+Name              : sbvPlugin+Version           : 0.1+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+                    on the <http://hackage.haskell.org/package/sbv SBV> package.+                    .+                    See "Data.SBV.Plugin" for a quick example.+License           : BSD3+License-file      : LICENSE+Stability         : Experimental+Author            : Levent Erkok+Homepage          : http://github.com/LeventErkok/sbvPlugin+Bug-reports       : http://github.com/LeventErkok/sbvPlugin/issues+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+    type:       git+    location:   git://github.com/LeventErkok/sbvPlugin.git++Library+  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+  Other-modules   : Data.SBV.Plugin.Analyze+                  , Data.SBV.Plugin.Data+                  , Data.SBV.Plugin.Common+                  , Data.SBV.Plugin.Env+                  , Data.SBV.Plugin.Plugin++Test-Suite sbvPluginTests+  type            : exitcode-stdio-1.0+  default-language: Haskell2010+  ghc-options     : -Wall+  Build-depends   : base >= 4.8 && < 5, sbvPlugin, tasty, tasty-golden, filepath, process, directory+  Hs-Source-Dirs  : tests+  main-is         : Run.hs
+ tests/GoldFiles/T00.hs.golden view
@@ -0,0 +1,8 @@++[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
+ tests/GoldFiles/T01.hs.golden view
@@ -0,0 +1,7 @@++[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.)
+ tests/GoldFiles/T02.hs.golden view
@@ -0,0 +1,5 @@++[SBV] tests/T02.hs:9:1 Proving "f", using Z3.+[Z3] Falsifiable. Counter-example:+  x = 1 :: Integer+  y = 0 :: Integer
+ tests/GoldFiles/T03.hs.golden view
@@ -0,0 +1,3 @@++[SBV] tests/T03.hs:10:1 Proving "f", using Z3.+[Z3] Q.E.D.
+ tests/GoldFiles/T04.hs.golden view
@@ -0,0 +1,3 @@++[SBV] tests/T04.hs:10:1 Proving "f", using Z3.+[Z3] Q.E.D.
+ tests/GoldFiles/T05.hs.golden view
@@ -0,0 +1,5 @@++[SBV] tests/T05.hs:9:1 Proving "f", using CVC4 and Yices.+[Yices] Falsifiable. Counter-example:+  x =  0 :: Integer+  y = -1 :: Integer
+ tests/GoldFiles/T06.hs.golden view
@@ -0,0 +1,5 @@++[SBV] tests/T06.hs:10:1 Proving "f", using Z3.+[Z3] Falsifiable. Counter-example:+  x = -128 :: Int8+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
+ tests/GoldFiles/T07.hs.golden view
@@ -0,0 +1,5 @@++[SBV] tests/T07.hs:9:1 Proving "f", using Z3.+[Z3] Falsifiable. Counter-example:+  x = NaN :: Double+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
+ tests/GoldFiles/T08.hs.golden view
@@ -0,0 +1,5 @@++[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.)
+ tests/GoldFiles/T09.hs.golden view
@@ -0,0 +1,3 @@++[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.
+ tests/GoldFiles/T10.hs.golden view
@@ -0,0 +1,3 @@++[SBV] tests/T10.hs:12:1 Proving "f", using Z3.+[Z3] Q.E.D.
+ tests/GoldFiles/T11.hs.golden view
@@ -0,0 +1,5 @@++[SBV] tests/T11.hs:15:1 Proving "f", using Z3.+[Z3] Falsifiable. Counter-example:+  x = 11 :: Integer+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
+ tests/GoldFiles/T12.hs.golden view
@@ -0,0 +1,6 @@++[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.)
+ tests/GoldFiles/T13.hs.golden view
@@ -0,0 +1,7 @@++[SBV] tests/T13.hs:9:1 Proving "f", using Z3.+[Z3] Falsifiable. Counter-example:+  i =     2 :: Integer+  d =   0.0 :: Double+  b = False :: Bool+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
+ tests/GoldFiles/T14.hs.golden view
@@ -0,0 +1,5 @@++[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.)
+ tests/GoldFiles/T15.hs.golden view
@@ -0,0 +1,51 @@++[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
@@ -0,0 +1,62 @@++[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] Failed. (Use option 'IgnoreFailure' to continue.)
+ tests/GoldFiles/T17.hs.golden view
@@ -0,0 +1,7 @@++[SBV] tests/T17.hs:13: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.)
+ tests/GoldFiles/T18.hs.golden view
@@ -0,0 +1,63 @@++[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+  [uninterpreted] |==| :: Age -> Age -> SBool+USER GIVEN CODE SEGMENTS+AXIOMS+DEFINE+  s2 :: SBool = s0 [uninterpreted] |==| 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 ---+(declare-fun |==| (Age Age) Bool)+; --- 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] 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
@@ -0,0 +1,65 @@++[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] Falsifiable. Counter-example:+  s = |[Char]!val!0| :: |[Char]|+[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.)
+ tests/GoldFiles/T20.hs.golden view
@@ -0,0 +1,1 @@+[SBV] tests/T20.hs:10:1 Skipping "f": Don't want to prove this now.
+ tests/GoldFiles/T21.hs.golden view
@@ -0,0 +1,72 @@++[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+** 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/T21.hs:9:3+(declare-sort String 0)  ; N.B. Uninterpreted: originating from sbvPlugin: tests/T21.hs:9:5+; --- 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"+; --- 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)))))+** 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))+** 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.)
+ tests/GoldFiles/T22.hs.golden view
@@ -0,0 +1,65 @@++[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..+[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]+[SBV] Failed. (Use option 'IgnoreFailure' to continue.)
+ tests/GoldFiles/T23.hs.golden view
@@ -0,0 +1,3 @@++[SBV] tests/T23.hs:9:1 Proving "f", using Z3.+[Z3] Q.E.D.
+ tests/GoldFiles/T24.hs.golden view
@@ -0,0 +1,3 @@++[SBV] tests/T24.hs:10:1 Proving "f", using Z3.+[Z3] Q.E.D.
+ tests/Run.hs view
@@ -0,0 +1,41 @@+module Main(main) where++import Control.Monad (void)++import Data.Char (isDigit)++import Test.Tasty+import Test.Tasty.Golden++import System.Directory+import System.FilePath+import System.Process++main :: IO ()+main = do tests <- findTests+          defaultMain (testGroup "Tests" [unitTests tests])+  where unitTests = testGroup "Unit tests" . map (runTest . takeBaseName)++findTests :: IO [FilePath]+findTests = do allEntries <- getDirectoryContents "tests"+               let testFile f = let b = takeBaseName f+                                    e = takeExtension f+                                in e == ".hs" && case b of+                                                  'T':xs -> all isDigit xs+                                                  _      -> False+               return $ filter testFile allEntries++runTest :: String -> TestTree+runTest f = goldenVsFile f gld out act+  where (inp, hi, o, gld, out) = fileNames f+        act = do void $ system $ unwords ["ghc", "-c", inp, ">", out, "2>&1"]+                 void $ system $ unwords ["/bin/rm", "-f", hi, o]++fileNames :: FilePath -> (FilePath, FilePath, FilePath, FilePath, FilePath)+fileNames fp = (inp, hi, o, gld, out)+  where f   = takeBaseName fp+        inp = "tests" </> f <.> "hs"+        hi  = "tests" </> f <.> "hi"+        o   = "tests" </> f <.> "o"+        gld = "tests/GoldFiles" </> f <.> "hs.golden"+        out = "tests/GoldFiles" </> f <.> "hs.current"