sbvPlugin 0.6 → 0.7
raw patch · 6 files changed
+49/−34 lines, 6 filesdep ~basedep ~sbvPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base, sbv
API changes (from Hackage documentation)
Files
- CHANGES.md +8/−3
- Data/SBV/Plugin/Analyze.hs +33/−25
- Data/SBV/Plugin/Env.hs +1/−1
- INSTALL +1/−1
- README.md +4/−2
- sbvPlugin.cabal +2/−2
CHANGES.md view
@@ -1,8 +1,13 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub: <http://github.com/LeventErkok/sbvPlugin> -* Latest Hackage released version: 0.6, 2015-01-01+* Latest Hackage released version: 0.7, 2015-06-06 +### Version 0.7, 2016-06-06++ * Compile with GHC-8.0. Plugin at least requires GHC-8.0.1 and SBV 5.12+ * Fix a few dead links+ ### Version 0.6, 2016-01-01 * Support for list expressions of the form [x .. y] and@@ -30,8 +35,8 @@ ### Version 0.3, 2015-12-21 * Added the micro-controller example, adapted from- the original SBV variant by Anthony Cowley- (http://acowley.github.io/NYHUG/FunctionalRoboticist.pdf)+ the original SBV variant by Anthony Cowley:+ <http://acowley.github.io/NYHUG/FunctionalRoboticist.pdf> * Add the "skip" option for the plugin itself. Handy when compiling the plugin itself!
Data/SBV/Plugin/Analyze.hs view
@@ -9,6 +9,7 @@ -- Walk the GHC Core, proving theorems/checking safety as they are found ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} {-# LANGUAGE NamedFieldPuns #-} module Data.SBV.Plugin.Analyze (analyzeBind) where@@ -21,7 +22,7 @@ import Data.IORef import Data.Char (isAlpha, isAlphaNum, toLower, isUpper)-import Data.List (intercalate, partition, nub, sort, sortBy, isPrefixOf)+import Data.List (intercalate, partition, nub, nubBy, sort, sortBy, isPrefixOf) import Data.Maybe (listToMaybe, fromMaybe) import Data.Ord (comparing) @@ -101,7 +102,9 @@ print sres -- If proof failed and there are uninterpreted non-input values, print a warning; except for "uninteresting" types- let unintVals = filter ((`notElem` uninteresting cfgEnv) . snd) $ nub $ sortBy (comparing fst) [vt | (vt, (False, _, _)) <- finalUninterps]+ let ok t = not . any (eqType t)+ eq (a, b) (c, d) = a == c && b `eqType` d+ unintVals = filter ((`ok` uninteresting cfgEnv) . snd) $ nubBy eq $ sortBy (comparing fst) [vt | (vt, (False, _, _)) <- finalUninterps] unless (success || null unintVals) $ do let plu | length finalUninterps > 1 = "s:" | True = ":"@@ -125,7 +128,12 @@ let marker = "[SBV] " ++ showSpan flags (pickSpan curLoc) tag s = marker ++ " " ++ s tab s = replicate (length marker) ' ' ++ " " ++ s- error $ concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es+ msg = concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es+#if MIN_VERSION_base(4,9,0)+ errorWithoutStackTrace msg+#else+ error msg+#endif res initEnv topLoc = do v <- runReaderT (symEval topExpr) initEnv { curLoc = [topLoc]@@ -331,7 +339,7 @@ -- Case expressions. We take advantage of the core-invariant that each case alternative -- is exhaustive; and DEFAULT (if present) is the first alternative. We turn it into a -- simple if-then-else chain with the last element on the DEFAULT, or whatever comes last.- tgo _ e@(Case ce caseBinder caseType alts)+ tgo _ e@(Case ce cBinder caseType alts) = do sce <- go ce let caseTooComplicated w [] = tbd ("Unsupported case-expression (" ++ w ++ ")") [sh e] caseTooComplicated w xs = tbd ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs@@ -346,7 +354,7 @@ (Tick t _, _ ) -> tickSpan t (Var v, _ ) -> varSpan v (_, b:_) -> varSpan b- _ -> varSpan caseBinder+ _ -> varSpan cBinder mr <- match eLoc sce p bs case mr of Just (m, bs') -> do let result = local (\env -> env{curLoc = eLoc : curLoc env, envMap = foldr (uncurry M.insert) (envMap env) bs'}) $ go rhs@@ -355,8 +363,8 @@ else choose (caseTooComplicated "with-complicated-alternatives-during-merging") m result (walk rest) Nothing -> caseTooComplicated "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs] - k <- getType (getSrcSpan caseBinder) caseType- local (\env -> env{envMap = M.insert (caseBinder, k) sce (envMap env)}) $ walk (nonDefs ++ defs)+ k <- getType (getSrcSpan cBinder) caseType+ local (\env -> env{envMap = M.insert (cBinder, k) sce (envMap env)}) $ walk (nonDefs ++ defs) where choose bailOut t tb fb = case S.svAsBool t of Nothing -> do stb <- tb@@ -468,18 +476,18 @@ uninterpret isInput t var = do Env{rUninterpreted, flags} <- ask prevUninterpreted <- liftIO $ readIORef rUninterpreted- case (var, t) `lookup` prevUninterpreted of- Just (_, _, val) -> return val- Nothing -> do let (tvs, t') = splitForAllTys t- (args, res) = splitFunTys t'- sp = getSrcSpan var- argKs <- mapM (getType sp) args- resK <- getType sp res- nm <- mkValidName $ showSDoc flags (ppr var)- body <- walk argKs (nm, resK) []- let fVal = wrap tvs body- liftIO $ modifyIORef rUninterpreted (((var, t), (isInput, nm, fVal)) :)- return fVal+ case [r | ((v, t'), r) <- prevUninterpreted, var == v && t `eqType` t'] of+ (_, _, val):_ -> return val+ [] -> do let (tvs, t') = splitForAllTys t+ (args, res) = splitFunTys t'+ sp = getSrcSpan var+ argKs <- mapM (getType sp) args+ resK <- getType sp res+ nm <- mkValidName $ showSDoc flags (ppr var)+ body <- walk argKs (nm, resK) []+ let fVal = wrap tvs body+ liftIO $ modifyIORef rUninterpreted (((var, t), (isInput, nm, fVal)) :)+ return fVal where walk :: [SKind] -> (String, SKind) -> [Val] -> Eval Val walk [] (nm, k) args = do Env{mbListSize, bailOut} <- ask @@ -576,11 +584,11 @@ -- 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+ case [k | (bt', k) <- uiTypes, bt `eqType` bt'] of+ k:_ -> return k+ [] -> 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 {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
Data/SBV/Plugin/Env.hs view
@@ -17,7 +17,7 @@ import GhcPlugins import GHC.Prim-import GHC.Types+import GHC.Types hiding (Type, TyCon) import qualified Data.Map as M import qualified Language.Haskell.TH as TH
INSTALL view
@@ -4,5 +4,5 @@ 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.+used by SBV; i.e., Z3 from Microsoft: <http://github.com/Z3Prover/z3>. Please make sure that the "z3" executable is in your path.
README.md view
@@ -1,7 +1,9 @@ ## SBVPlugin: SBV Plugin for GHC -[](https://hackage.haskell.org/package/sbvPlugin)- [](http://travis-ci.org/LeventErkok/sbvPlugin)+[]+ (http://hackage.haskell.org/package/sbvPlugin)+[]+ (http://travis-ci.org/LeventErkok/sbvPlugin) ### Example
sbvPlugin.cabal view
@@ -1,5 +1,5 @@ Name : sbvPlugin-Version : 0.6+Version : 0.7 Category : Formal methods, Theorem provers, Math, SMT, Symbolic Computation Synopsis : Formally prove properties of Haskell programs using SBV/SMT Description : GHC plugin for proving properties over Haskell functions using SMT solvers, based@@ -29,7 +29,7 @@ , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController , Data.SBV.Plugin.Examples.BitTricks- build-depends : base >= 4.8 && < 5, ghc, ghc-prim, containers, sbv >= 5.8, mtl, template-haskell+ build-depends : base >= 4.9 && < 5, ghc, ghc-prim, containers, sbv >= 5.12, mtl, template-haskell Other-modules : Data.SBV.Plugin.Analyze , Data.SBV.Plugin.Data , Data.SBV.Plugin.Common