sbvPlugin 0.12 → 9.0.1
raw patch · 13 files changed
+72/−41 lines, 13 filesdep ~sbv
Dependency ranges changed: sbv
Files
- CHANGES.md +7/−1
- Data/SBV/Plugin.hs +3/−0
- Data/SBV/Plugin/Analyze.hs +26/−22
- Data/SBV/Plugin/Common.hs +6/−6
- Data/SBV/Plugin/Data.hs +2/−0
- Data/SBV/Plugin/Env.hs +5/−3
- Data/SBV/Plugin/Examples/BitTricks.hs +2/−0
- Data/SBV/Plugin/Examples/MergeSort.hs +3/−1
- Data/SBV/Plugin/Examples/MicroController.hs +2/−0
- Data/SBV/Plugin/Examples/Proved.hs +2/−0
- Data/SBV/Plugin/Plugin.hs +9/−5
- sbvPlugin.cabal +3/−3
- tests/Run.hs +2/−0
CHANGES.md view
@@ -1,7 +1,13 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub: <http://github.com/LeventErkok/sbvPlugin> -* Latest Hackage released version: 0.12, 2019-09-05+* Latest Hackage released version: 9.0.1, 2021-03-22++### Version 9.0.1, 2021-03-22+ * Changes required to compile with GHC 9.0.1+ * SBVPlugin version now matches the version of GHC we compiled it with.+ It might work with newer versions of GHC, though not tested/guaranteed.+ * Bump up sbv dependence to >= 8.13 ### Version 0.12, 2020-09-05 * Changes required to compile with GHC 8.10.2
Data/SBV/Plugin.hs view
@@ -59,6 +59,9 @@ -- Please report if you find any crucial differences when the plugin is run first or last, especially -- if the outputs are different. ---------------------------------------------------------------------------------++{-# OPTIONS_GHC -Wall -Werror #-}+ module Data.SBV.Plugin( -- * Entry point plugin
Data/SBV/Plugin/Analyze.hs view
@@ -12,10 +12,12 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE NamedFieldPuns #-} +{-# OPTIONS_GHC -Wall -Werror #-}+ module Data.SBV.Plugin.Analyze (analyzeBind) where -import GhcPlugins-import TyCoRep+import GHC.Core.TyCo.Rep as TyCoRep+import GHC.Plugins import Control.Monad.Reader import System.Exit@@ -105,6 +107,7 @@ S.Unknown{} -> False -- conservative S.ProofError{} -> False -- conservative S.SatExtField{} -> False -- conservative+ S.DeltaSat{} -> False -- conservative putStr $ "[" ++ show solver ++ "] " print sres @@ -227,23 +230,20 @@ tgo t e@(Lit l) = do Env{machWordSize} <- ask case l of- 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- KBase b -> return $ Base $ S.svInteger b i- _ -> error $ "Impossible: The type for literal resulted in non base kind: " ++ sh (e, k)- LitNumNatural -> unint- LitNumInt -> return $ Base $ S.svInteger (S.KBounded True machWordSize) i- LitNumInt64 -> return $ Base $ S.svInteger (S.KBounded True 64 ) i- LitNumWord -> return $ Base $ S.svInteger (S.KBounded False machWordSize) i- LitNumWord64 -> return $ Base $ S.svInteger (S.KBounded False 64 ) i+ 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 -> case lt of+ LitNumInteger -> return $ Base $ S.svInteger S.KUnbounded i+ LitNumInt -> return $ Base $ S.svInteger (S.KBounded True machWordSize) i+ LitNumInt64 -> return $ Base $ S.svInteger (S.KBounded True 64 ) i+ LitNumWord -> return $ Base $ S.svInteger (S.KBounded False machWordSize) i+ LitNumWord64 -> return $ Base $ S.svInteger (S.KBounded False 64 ) i+ LitNumNatural -> unint where unint = do Env{flags} <- ask k <- getType noSrcSpan t@@ -429,7 +429,7 @@ 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+ Lam x b -> do reduced <- betaReduce $ substExpr (extendSubstList emptySubst [(x, a)]) b () <- debugTrace ("Beta reduce:\n" ++ sh (orig, reduced)) $ return () return reduced _ -> return (App rf a)@@ -482,6 +482,10 @@ ] +-- | Unscale a value. We don't really care about the scale itself, so far as SBV is concerned+unScale :: Scaled a -> a+unScale (Scaled _ a) = a+ -- | Uninterpret an expression uninterpret :: Bool -> Type -> Var -> Eval Val uninterpret isInput t var = do@@ -492,7 +496,7 @@ [] -> do let (tvs, t') = splitForAllTys t (args, res) = splitFunTys t' sp = getSrcSpan var- argKs <- mapM (getType sp) args+ argKs <- mapM (getType sp . unScale) args resK <- getType sp res nm <- mkValidName $ showSDoc flags (ppr var) body <- walk argKs (nm, resK) []@@ -561,7 +565,7 @@ getType :: SrcSpan -> Type -> Eval SKind getType sp typ = do let (tvs, typ') = splitForAllTys typ (args, res) = splitFunTys typ'- argKs <- mapM (getType sp) args+ argKs <- mapM (getType sp . unScale) args resK <- getComposite res return $ wrap tvs $ foldr KFun resK argKs where wrap ts f = foldr (KFun . mkUninterpreted) f ts
Data/SBV/Plugin/Common.hs view
@@ -12,16 +12,16 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE RankNTypes #-} -{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-} module Data.SBV.Plugin.Common where import Control.Monad.Reader -import CostCentre-import GhcPlugins+import GHC.Plugins -import Unique (nonDetCmpUnique)+import GHC.Types.CostCentre+import GHC.Types.Unique (nonDetCmpUnique) import Data.Maybe (mapMaybe) import qualified Data.Map as M@@ -91,7 +91,7 @@ -- | Given the user options, determine which solver(s) to use pickSolvers :: [SBVOption] -> IO [S.SMTConfig] pickSolvers slvrs- | AnySolver `elem` slvrs = S.sbvAvailableSolvers+ | AnySolver `elem` slvrs = S.getAvailableSolvers | True = case mapMaybe (`lookup` solvers) slvrs of [] -> return [S.defaultSMTCfg] xs -> return xs@@ -167,7 +167,7 @@ -- | Compute the span given a Tick. Returns the old-span if the tick span useless. tickSpan :: Tickish t -> SrcSpan tickSpan (ProfNote cc _ _) = cc_loc cc-tickSpan (SourceNote s _) = RealSrcSpan s+tickSpan (SourceNote s _) = RealSrcSpan s Nothing tickSpan _ = noSrcSpan -- | Compute the span for a binding.
Data/SBV/Plugin/Data.hs view
@@ -11,6 +11,8 @@ {-# LANGUAGE DeriveDataTypeable #-} +{-# OPTIONS_GHC -Wall -Werror #-}+ module Data.SBV.Plugin.Data where import Data.Data (Data, Typeable)
Data/SBV/Plugin/Env.hs view
@@ -13,14 +13,16 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -Wall -Werror #-}+ module Data.SBV.Plugin.Env (buildTCEnv, buildFunEnv, buildDests, buildSpecials, uninterestingTypes) where -import GhcPlugins+import GHC.Plugins import GHC.Prim import GHC.Types hiding (Type, TyCon) -import Finder-import IfaceEnv+import GHC.Driver.Finder+import GHC.Iface.Env import qualified Data.Map as M import qualified Language.Haskell.TH as TH
Data/SBV/Plugin/Examples/BitTricks.hs view
@@ -12,6 +12,8 @@ {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} +{-# OPTIONS_GHC -Wall -Werror #-}+ module Data.SBV.Plugin.Examples.BitTricks where import Data.SBV.Plugin
Data/SBV/Plugin/Examples/MergeSort.hs view
@@ -8,8 +8,10 @@ -- -- An implementation of merge-sort and its correctness. --------------------------------------------------------------------------------+ {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}++{-# OPTIONS_GHC -Wall -Werror #-} module Data.SBV.Plugin.Examples.MergeSort where
Data/SBV/Plugin/Examples/MicroController.hs view
@@ -13,6 +13,8 @@ {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} +{-# OPTIONS_GHC -Wall -Werror #-}+ module Data.SBV.Plugin.Examples.MicroController where import Data.SBV.Plugin
Data/SBV/Plugin/Examples/Proved.hs view
@@ -13,6 +13,8 @@ {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} +{-# OPTIONS_GHC -Wall -Werror #-}+ module Data.SBV.Plugin.Examples.Proved where import Data.SBV.Plugin
Data/SBV/Plugin/Plugin.hs view
@@ -11,13 +11,15 @@ {-# LANGUAGE NamedFieldPuns #-} +{-# OPTIONS_GHC -Wall -Werror #-}+ module Data.SBV.Plugin.Plugin(plugin) where -import GhcPlugins+import GHC.Plugins import System.Exit import Data.Maybe (fromJust)-import Data.List (sortOn)+import Data.List (sortBy) import Data.Bits (bitSizeMaybe) import Data.IORef@@ -48,7 +50,7 @@ pass guts@ModGuts{mg_binds} = do df <- getDynFlags- anns <- getAnnotations deserializeWithData guts+ anns <- snd <$> getAnnotations deserializeWithData guts let wsz = fromJust (bitSizeMaybe (0::Int)) @@ -64,7 +66,7 @@ let cfg = Config { isGHCi = hscTarget df == HscInterpreted , opts = []- , sbvAnnotation = lookupWithDefaultUFM anns [] . varUnique+ , sbvAnnotation = lookupWithDefaultUFM anns [] . varName , cfgEnv = Env { curLoc = [] , flags = df , machWordSize = wsz@@ -86,6 +88,8 @@ bindLoc (Rec []) = noSrcSpan bindLoc (Rec ((b, _):_)) = varSpan b - mapM_ (analyzeBind cfg) $ sortOn bindLoc mg_binds+ cmp a b = bindLoc a `leftmost_smallest` bindLoc b++ mapM_ (analyzeBind cfg) $ sortBy cmp mg_binds return guts
sbvPlugin.cabal view
@@ -1,5 +1,5 @@ Name : sbvPlugin-Version : 0.12+Version : 9.0.1 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==8.10.2+Tested-With : GHC==9.0.1 source-repository head type: git@@ -36,7 +36,7 @@ , ghc , ghc-prim , containers- , sbv >= 8.8+ , sbv >= 8.13 , mtl , template-haskell Other-modules : Data.SBV.Plugin.Analyze
tests/Run.hs view
@@ -1,3 +1,5 @@+{-# OPTIONS_GHC -Wall -Werror #-}+ module Main(main) where import Control.Monad (void)