sbvPlugin 0.11 → 0.12
raw patch · 9 files changed
+51/−70 lines, 9 filesdep ~basedep ~ghcdep ~ghc-prim
Dependency ranges changed: base, ghc, ghc-prim, sbv
Files
- CHANGES.md +5/−1
- Data/SBV/Plugin.hs +0/−7
- Data/SBV/Plugin/Analyze.hs +12/−13
- Data/SBV/Plugin/Common.hs +12/−14
- Data/SBV/Plugin/Env.hs +0/−28
- Data/SBV/Plugin/Examples/MergeSort.hs +1/−1
- Data/SBV/Plugin/Examples/MicroController.hs +2/−2
- README.md +2/−1
- sbvPlugin.cabal +17/−3
CHANGES.md view
@@ -1,7 +1,11 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub: <http://github.com/LeventErkok/sbvPlugin> -* Latest Hackage released version: 0.11, 2019-01-14+* Latest Hackage released version: 0.12, 2019-09-05++### Version 0.12, 2020-09-05+ * Changes required to compile with GHC 8.10.2+ * Bump up sbv dependence to >= 8.8 ### Version 0.11, 2019-01-14
Data/SBV/Plugin.hs view
@@ -69,14 +69,7 @@ , SBVOption(..) -- * The 'Proved' type , Proved- -- * The splittable class- , Splittable(..) ) where import Data.SBV.Plugin.Plugin import Data.SBV.Plugin.Data---- TODO: Unfortunately we need to export the Splittable class directly--- from the plugin, due to issues arising from https://ghc.haskell.org/trac/ghc/ticket/16104--- Hopefully this is temporary and this export can be removed later.-import Data.SBV (Splittable(..))
Data/SBV/Plugin/Analyze.hs view
@@ -227,12 +227,13 @@ tgo t e@(Lit l) = do Env{machWordSize} <- ask case l of- MachChar{} -> unint- MachStr{} -> unint- MachNullAddr -> unint- MachLabel{} -> unint- MachFloat f -> return $ Base $ S.svFloat (fromRational f)- MachDouble d -> return $ Base $ S.svDouble (fromRational d)+ LitChar{} -> unint+ LitString{} -> unint+ LitNullAddr{} -> unint+ LitRubbish{} -> unint+ LitLabel{} -> unint+ LitFloat f -> return $ Base $ S.svFloat (fromRational f)+ LitDouble d -> return $ Base $ S.svDouble (fromRational d) LitNumber lt i it -> do k <- getType noSrcSpan it case lt of LitNumInteger -> case k of@@ -452,7 +453,7 @@ Nothing -> "Kind: " ++ sh k Just t -> "Type: " ++ sh t - sym (KBase k) nm = do v <- lift $ S.symbolicEnv >>= liftIO . S.svMkSymVar Nothing k nm+ sym (KBase k) nm = do v <- lift $ S.symbolicEnv >>= liftIO . S.svMkSymVar (S.NonQueryVar Nothing) k nm return (Base v) sym (KTup ks) nm = do let ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. length ks]@@ -564,7 +565,7 @@ resK <- getComposite res return $ wrap tvs $ foldr KFun resK argKs where wrap ts f = foldr (KFun . mkUninterpreted) f ts- mkUninterpreted v = KBase (S.KUninterpreted (show (occNameFS (occName (varName v)))) (Left "sbvPlugin"))+ mkUninterpreted v = KBase $ S.KUserSort (show (occNameFS (occName (varName v)))) Nothing -- | Extract tuples, lists, or base kinds getComposite :: Type -> Eval SKind@@ -579,10 +580,8 @@ 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+ Just k -> maybe unknown return (k `M.lookup` tcMap)+ _ -> 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 []@@ -597,7 +596,7 @@ case [k | (bt', k) <- uiTypes, bt `eqType` bt'] of k:_ -> return k [] -> do nm <- mkValidName $ showSDoc flags (ppr bt)- let k = S.KUninterpreted nm $ Left $ "originating from sbvPlugin: " ++ showSDoc flags (ppr sp)+ let k = S.KUserSort nm Nothing liftIO $ modifyIORef rUITypes ((bt, k) :) return k
Data/SBV/Plugin/Common.hs view
@@ -9,10 +9,8 @@ -- Common data-structures/utilities ----------------------------------------------------------------------------- -{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE RankNTypes #-} {-# OPTIONS_GHC -fno-warn-orphans #-} @@ -152,19 +150,19 @@ -- | Symbolic if-then-else over values. iteVal :: ([String] -> Eval Val) -> S.SVal -> Val -> Val -> Eval Val-iteVal bailOut t v1 v2 = k v1 v2+iteVal die t v1 v2 = k v1 v2 where k (Base a) (Base b) = return $ Base $ S.svIte t a b k (Tup as) (Tup bs) | length as == length bs = Tup `fmap` zipWithM k as bs k (Lst as) (Lst bs) | length as == length bs = Lst `fmap` zipWithM k as bs- | True = bailOut [ "Alternatives are producing lists of differing sizes:"- , " Length " ++ show (length as) ++ ": " ++ showSDocUnsafe (ppr (Lst as))- , "vs Length " ++ show (length bs) ++ ": " ++ showSDocUnsafe (ppr (Lst bs))- ]+ | True = die [ "Alternatives are producing lists of differing sizes:"+ , " Length " ++ show (length as) ++ ": " ++ showSDocUnsafe (ppr (Lst as))+ , "vs Length " ++ show (length bs) ++ ": " ++ showSDocUnsafe (ppr (Lst bs))+ ] k (Func n1 f) (Func n2 g) = return $ Func (n1 `mplus` n2) $ \a -> f a >>= \fa -> g a >>= \ga -> k fa ga- k _ _ = bailOut [ "Unsupported if-then-else/case with alternatives:"- , " Value:" ++ showSDocUnsafe (ppr v1)- , " vs:" ++ showSDocUnsafe (ppr v2)- ]+ k _ _ = die [ "Unsupported if-then-else/case with alternatives:"+ , " Value:" ++ showSDocUnsafe (ppr v1)+ , " vs:" ++ showSDocUnsafe (ppr v2)+ ] -- | Compute the span given a Tick. Returns the old-span if the tick span useless. tickSpan :: Tickish t -> SrcSpan@@ -186,7 +184,7 @@ -- | Show a GHC span in user-friendly form showSpan :: DynFlags -> SrcSpan -> String-showSpan flags s = showSDoc flags (ppr s)+showSpan fs s = showSDoc fs (ppr s) -- | This comes mighty handy! Wonder why GHC doesn't have it already: instance Show CoreExpr where
Data/SBV/Plugin/Env.hs view
@@ -113,12 +113,6 @@ ++ [ (op, tlift2 (KBase k), lift2 sOp) | k <- bvKinds, (op, sOp) <- bvBinOps ] ++ [ (op, tlift2ShRot wsz (KBase k), lift2 sOp) | k <- bvKinds, (op, sOp) <- bvShiftRots] - -- bv-splits- ++ [('S.split, tSplit s, liftSplit s) | s <- [16, 32, 64]]-- -- bv-joins- ++ [ ('(S.#), tJoin s, lift2 S.svJoin) | s <- [8, 16, 32]]- -- constructing "fixed-size" lists ++ [ ('enumFromTo, tEnumFromTo (KBase k), sEnumFromTo) | k <- arithKinds ] ++ [ ('enumFromThenTo, tEnumFromThenTo (KBase k), sEnumFromThenTo) | k <- arithKinds ]@@ -278,18 +272,6 @@ tlift2ShRot :: Int -> SKind -> SKind tlift2ShRot wsz k = KFun k (KFun (KBase (S.KBounded True wsz)) k) --- | Construct the type for a split operation-tSplit :: Int -> SKind-tSplit n = KFun a (KTup [r, r])- where a = KBase (S.KBounded False n)- r = KBase (S.KBounded False (n `div` 2))---- | Construct the type for a join operation-tJoin :: Int -> SKind-tJoin n = KFun a (KFun a r)- where a = KBase (S.KBounded False n)- r = KBase (S.KBounded False (n*2))- -- | Type of enumFromTo: [x .. y] tEnumFromTo :: SKind -> SKind tEnumFromTo a = KFun a (KFun a (KLst a))@@ -321,16 +303,6 @@ h v = error $ "Impossible happened: lift2 received non-base argument (h): " ++ showSDocUnsafe (ppr v) k a (Base b) = return $ Base $ f a b k _ v = error $ "Impossible happened: lift2 received non-base argument (k): " ++ showSDocUnsafe (ppr v)---- | Lifting splits-liftSplit :: Int -> Val-liftSplit n = Func Nothing g- where g (Typ _) = return $ Func Nothing g- g (Base a) = do let half = n `div` 2- f = Base $ S.svExtract (n-1) half a- s = Base $ S.svExtract (half-1) 0 a- return $ Tup [f, s]- g v = error $ "Impossible happened: liftSplit received unexpected argument: " ++ showSDocUnsafe (ppr (n, v)) -- | Lifting an equality is special; since it acts uniformly over tuples. liftEq :: (S.SVal -> S.SVal -> S.SVal) -> Val
Data/SBV/Plugin/Examples/MergeSort.hs view
@@ -87,7 +87,7 @@ -- | Asserting correctness of merge-sort for a list of the given size. Note that we can -- only check correctness for fixed-size lists. Also, the proof will get more and more--- complicated for the backend SMT solver as 'n' increases. Here we try it with 4.+-- complicated for the backend SMT solver as @n@ increases. Here we try it with 4. -- -- We have: --
Data/SBV/Plugin/Examples/MicroController.hs view
@@ -33,7 +33,7 @@ -- * The specification ----------------------------------------------------------------------------- --- | Given a last-signal-time calculator, named 'calculate', check that it satisfies the following+-- | Given a last-signal-time calculator, named @calculate@, check that it satisfies the following -- three requirements: We must've just sent a signal if: -- -- * /minRate/: The last-time we sent is strictly less than the 'maxTimeSince' amount@@ -78,7 +78,7 @@ -- @ -- -- We're being told that if the range is 200, and manual override is off, and time-since last is 9,--- then our "calculator" returns 10. But that violates the 'minRate' requirement, since we+-- then our "calculator" returns 10. But that violates the @minRate@ requirement, since we -- never want to go 'maxTimeSince' cycles without sending a signal! {-# ANN checkBad theorem {options = [IgnoreFailure]} #-} checkBad :: Int -> Bool -> Int -> Bool
README.md view
@@ -1,6 +1,7 @@ ## SBVPlugin: SBV Plugin for GHC -[](http://hackage.haskell.org/package/sbvPlugin)+On Hackage: http://hackage.haskell.org/package/sbvPlugin+ [](http://travis-ci.org/LeventErkok/sbvPlugin) ### Example
sbvPlugin.cabal view
@@ -1,5 +1,5 @@ Name : sbvPlugin-Version : 0.11+Version : 0.12 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@@ -18,6 +18,8 @@ Cabal-Version : 1.14 Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md +Tested-With : GHC==8.10.2+ source-repository head type: git location: git://github.com/LeventErkok/sbvPlugin.git@@ -30,7 +32,13 @@ , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController , Data.SBV.Plugin.Examples.BitTricks- build-depends : base >= 4.12 && < 5, ghc >= 8.6.1, ghc-prim >= 0.5.3, containers, sbv >= 8.0, mtl, template-haskell+ build-depends : base >= 4.11 && < 5+ , ghc+ , ghc-prim+ , containers+ , sbv >= 8.8+ , mtl+ , template-haskell Other-modules : Data.SBV.Plugin.Analyze , Data.SBV.Plugin.Common , Data.SBV.Plugin.Env@@ -41,6 +49,12 @@ type : exitcode-stdio-1.0 default-language: Haskell2010 ghc-options : -Wall- Build-depends : base >= 4.12 && < 5, sbvPlugin, tasty, tasty-golden, filepath, process, directory+ Build-depends : base >= 4.11 && < 5+ , sbvPlugin+ , tasty+ , tasty-golden+ , filepath+ , process+ , directory Hs-Source-Dirs : tests main-is : Run.hs