sbvPlugin 9.0.1 → 9.2.2
raw patch · 11 files changed
+73/−20 lines, 11 filesdep ~ghcdep ~sbv
Dependency ranges changed: ghc, sbv
Files
- CHANGES.md +5/−1
- COPYRIGHT +1/−1
- Data/SBV/Plugin/Analyze.hs +15/−6
- Data/SBV/Plugin/Common.hs +2/−1
- Data/SBV/Plugin/Env.hs +2/−1
- Data/SBV/Plugin/Examples/Maximum.hs +37/−0
- Data/SBV/Plugin/Examples/MicroController.hs +2/−2
- Data/SBV/Plugin/Plugin.hs +1/−1
- LICENSE +1/−1
- README.md +1/−1
- sbvPlugin.cabal +6/−5
CHANGES.md view
@@ -1,7 +1,11 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub: <http://github.com/LeventErkok/sbvPlugin> -* Latest Hackage released version: 9.0.1, 2021-03-22+* Latest Hackage released version: 9.2.2, 2022-04-27++### Version 9.2.2, 2022-04-27+ * Changes required to compile with GHC 9.2.2+ * Bump up sbv dependence to >= 9.0 ### Version 9.0.1, 2021-03-22 * Changes required to compile with GHC 9.0.1
COPYRIGHT view
@@ -1,4 +1,4 @@-Copyright (c) 2015-2017, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2015-2022, Levent Erkok (erkokl@gmail.com) All rights reserved. The sbvPlugin is distributed with the BSD3 license. See the LICENSE file
Data/SBV/Plugin/Analyze.hs view
@@ -240,8 +240,14 @@ LitNumber lt i -> case lt of LitNumInteger -> return $ Base $ S.svInteger S.KUnbounded i LitNumInt -> return $ Base $ S.svInteger (S.KBounded True machWordSize) i+ LitNumInt8 -> return $ Base $ S.svInteger (S.KBounded True 8 ) i+ LitNumInt16 -> return $ Base $ S.svInteger (S.KBounded True 16 ) i+ LitNumInt32 -> return $ Base $ S.svInteger (S.KBounded True 32 ) i LitNumInt64 -> return $ Base $ S.svInteger (S.KBounded True 64 ) i LitNumWord -> return $ Base $ S.svInteger (S.KBounded False machWordSize) i+ LitNumWord8 -> return $ Base $ S.svInteger (S.KBounded False 8 ) i+ LitNumWord16 -> return $ Base $ S.svInteger (S.KBounded False 16 ) i+ LitNumWord32 -> return $ Base $ S.svInteger (S.KBounded False 32 ) i LitNumWord64 -> return $ Base $ S.svInteger (S.KBounded False 64 ) i LitNumNatural -> unint @@ -354,12 +360,14 @@ = 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- isDefault (DEFAULT, _, _) = True- isDefault _ = False++ isDefault (Alt DEFAULT _ _) = True+ isDefault _ = False+ (defs, nonDefs) = partition isDefault alts walk [] = caseTooComplicated "with-non-exhaustive-match" [] -- can't really happen- walk ((p, bs, rhs) : rest) =+ walk (Alt p bs rhs : rest) = do -- try to get a "good" location for this alternative, if possible: let eLoc = case (rhs, bs) of (Tick t _, _ ) -> tickSpan t@@ -493,7 +501,7 @@ prevUninterpreted <- liftIO $ readIORef rUninterpreted case [r | ((v, t'), r) <- prevUninterpreted, var == v && t `eqType` t'] of (_, _, val):_ -> return val- [] -> do let (tvs, t') = splitForAllTys t+ [] -> do let (tvs, t') = splitForAllTyCoVars t (args, res) = splitFunTys t' sp = getSrcSpan var argKs <- mapM (getType sp . unScale) args@@ -533,8 +541,9 @@ xs -> return $ Tup xs walk (_:ks) nmk args = return $ Func Nothing $ \a -> walk ks nmk (a:args)+ wrap [] f = f- wrap (_:ts) f = Func Nothing $ \(Typ _) -> return (wrap ts f)+ wrap (_:ts) f = Func Nothing $ \_ -> return (wrap ts f) -- not every name is good, sigh mkValidName :: String -> Eval String@@ -563,7 +572,7 @@ -- | Convert a Core type to an SBV Type, retaining functions and tuples getType :: SrcSpan -> Type -> Eval SKind-getType sp typ = do let (tvs, typ') = splitForAllTys typ+getType sp typ = do let (tvs, typ') = splitForAllTyCoVars typ (args, res) = splitFunTys typ' argKs <- mapM (getType sp . unScale) args resK <- getComposite res
Data/SBV/Plugin/Common.hs view
@@ -20,6 +20,7 @@ import GHC.Plugins +import GHC.Types.Tickish import GHC.Types.CostCentre import GHC.Types.Unique (nonDetCmpUnique) @@ -165,7 +166,7 @@ ] -- | Compute the span given a Tick. Returns the old-span if the tick span useless.-tickSpan :: Tickish t -> SrcSpan+tickSpan :: GenTickish t -> SrcSpan tickSpan (ProfNote cc _ _) = cc_loc cc tickSpan (SourceNote s _) = RealSrcSpan s Nothing tickSpan _ = noSrcSpan
Data/SBV/Plugin/Env.hs view
@@ -20,8 +20,9 @@ import GHC.Plugins import GHC.Prim import GHC.Types hiding (Type, TyCon)+import GHC.Types.TyThing -import GHC.Driver.Finder+import GHC.Unit.Finder import GHC.Iface.Env import qualified Data.Map as M
+ Data/SBV/Plugin/Examples/Maximum.hs view
@@ -0,0 +1,37 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Plugin.Examples.Maximum+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Shows that a naive definition of maximum doing bit-vector arithmetic+-- is incorrect.+-----------------------------------------------------------------------------+{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}++{-# OPTIONS_GHC -Wall -Werror #-}++module Data.SBV.Plugin.Examples.Maximum where++import Data.SBV.Plugin++myMax :: Int -> Int -> Int -> Int+myMax x y z | x-y >= 0 && x-z >= 0 = x+ | y-x >= 0 && y-z >= 0 = y+ | otherwise = z++-- | Show that this function fails to compute maximum correctly.+-- We have:+--+-- @+-- [SBV] a.hs:11:1-7 Proving "correct", using Z3.+-- [Z3] Falsifiable. Counter-example:+-- x = -2816883406898309583 :: Int64+-- y = -2816883406898309583 :: Int64+-- z = 6694719001794338309 :: Int64+-- @+correct :: Proved (Int -> Int -> Int -> Bool)+correct x y z = m >= x && m >= y && m >= z+ where m = myMax x y z
Data/SBV/Plugin/Examples/MicroController.hs view
@@ -74,12 +74,12 @@ -- @ -- [SBV] MicroController.hs:85:1-8 Proving "checkBad", using Z3. -- [Z3] Falsifiable. Counter-example:--- range = 200 :: Int64+-- range = 0 :: Int64 -- manual = False :: Bool -- timeSince = 9 :: Int64 -- @ ----- We're being told that if the range is 200, and manual override is off, and time-since last is 9,+-- We're being told that if the range is 0, and manual override is off, and time-since last is 9, -- 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]} #-}
Data/SBV/Plugin/Plugin.hs view
@@ -64,7 +64,7 @@ rUsedNames <- liftIO $ newIORef [] rUITypes <- liftIO $ newIORef [] - let cfg = Config { isGHCi = hscTarget df == HscInterpreted+ let cfg = Config { isGHCi = ghcMode df == CompManager , opts = [] , sbvAnnotation = lookupWithDefaultUFM anns [] . varName , cfgEnv = Env { curLoc = []
LICENSE view
@@ -1,6 +1,6 @@ sbvPlugin: SMT based theorem prover for Haskell -Copyright (c) 2015-2017, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2015-2022, Levent Erkok (erkokl@gmail.com) All rights reserved. Redistribution and use in source and binary forms, with or without
README.md view
@@ -2,7 +2,7 @@ On Hackage: http://hackage.haskell.org/package/sbvPlugin -[](http://travis-ci.org/LeventErkok/sbvPlugin)+[](http://travis-ci.com/LeventErkok/sbvPlugin) ### Example
sbvPlugin.cabal view
@@ -1,5 +1,5 @@ Name : sbvPlugin-Version : 9.0.1+Version : 9.2.2 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,7 +18,7 @@ Cabal-Version : 1.14 Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md -Tested-With : GHC==9.0.1+Tested-With : GHC==9.2.2 source-repository head type: git@@ -29,14 +29,15 @@ ghc-options : -Wall -fplugin-opt Data.SBV.Plugin:skip Exposed-modules : Data.SBV.Plugin , Data.SBV.Plugin.Data+ , Data.SBV.Plugin.Examples.BitTricks+ , Data.SBV.Plugin.Examples.Maximum , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController- , Data.SBV.Plugin.Examples.BitTricks build-depends : base >= 4.11 && < 5- , ghc+ , ghc >= 9.2.2 , ghc-prim , containers- , sbv >= 8.13+ , sbv >= 9.0 , mtl , template-haskell Other-modules : Data.SBV.Plugin.Analyze