diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,13 @@ * Hackage: * GitHub: -* 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 diff --git a/Data/SBV/Plugin.hs b/Data/SBV/Plugin.hs --- a/Data/SBV/Plugin.hs +++ b/Data/SBV/Plugin.hs @@ -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 diff --git a/Data/SBV/Plugin/Analyze.hs b/Data/SBV/Plugin/Analyze.hs --- a/Data/SBV/Plugin/Analyze.hs +++ b/Data/SBV/Plugin/Analyze.hs @@ -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 diff --git a/Data/SBV/Plugin/Common.hs b/Data/SBV/Plugin/Common.hs --- a/Data/SBV/Plugin/Common.hs +++ b/Data/SBV/Plugin/Common.hs @@ -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. diff --git a/Data/SBV/Plugin/Data.hs b/Data/SBV/Plugin/Data.hs --- a/Data/SBV/Plugin/Data.hs +++ b/Data/SBV/Plugin/Data.hs @@ -11,6 +11,8 @@ {-# LANGUAGE DeriveDataTypeable #-} +{-# OPTIONS_GHC -Wall -Werror #-} + module Data.SBV.Plugin.Data where import Data.Data (Data, Typeable) diff --git a/Data/SBV/Plugin/Env.hs b/Data/SBV/Plugin/Env.hs --- a/Data/SBV/Plugin/Env.hs +++ b/Data/SBV/Plugin/Env.hs @@ -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 diff --git a/Data/SBV/Plugin/Examples/BitTricks.hs b/Data/SBV/Plugin/Examples/BitTricks.hs --- a/Data/SBV/Plugin/Examples/BitTricks.hs +++ b/Data/SBV/Plugin/Examples/BitTricks.hs @@ -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 diff --git a/Data/SBV/Plugin/Examples/MergeSort.hs b/Data/SBV/Plugin/Examples/MergeSort.hs --- a/Data/SBV/Plugin/Examples/MergeSort.hs +++ b/Data/SBV/Plugin/Examples/MergeSort.hs @@ -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 diff --git a/Data/SBV/Plugin/Examples/MicroController.hs b/Data/SBV/Plugin/Examples/MicroController.hs --- a/Data/SBV/Plugin/Examples/MicroController.hs +++ b/Data/SBV/Plugin/Examples/MicroController.hs @@ -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 diff --git a/Data/SBV/Plugin/Examples/Proved.hs b/Data/SBV/Plugin/Examples/Proved.hs --- a/Data/SBV/Plugin/Examples/Proved.hs +++ b/Data/SBV/Plugin/Examples/Proved.hs @@ -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 diff --git a/Data/SBV/Plugin/Plugin.hs b/Data/SBV/Plugin/Plugin.hs --- a/Data/SBV/Plugin/Plugin.hs +++ b/Data/SBV/Plugin/Plugin.hs @@ -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 diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -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 diff --git a/tests/Run.hs b/tests/Run.hs --- a/tests/Run.hs +++ b/tests/Run.hs @@ -1,3 +1,5 @@ +{-# OPTIONS_GHC -Wall -Werror #-} + module Main(main) where import Control.Monad (void)