diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,11 @@ * Hackage: * GitHub: -* 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 diff --git a/COPYRIGHT b/COPYRIGHT --- a/COPYRIGHT +++ b/COPYRIGHT @@ -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 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 @@ -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 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 @@ -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 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 @@ -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 diff --git a/Data/SBV/Plugin/Examples/Maximum.hs b/Data/SBV/Plugin/Examples/Maximum.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Plugin/Examples/Maximum.hs @@ -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 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 @@ -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]} #-} 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 @@ -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 = [] diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ On Hackage: http://hackage.haskell.org/package/sbvPlugin -[![Build Status](http://img.shields.io/travis/LeventErkok/sbvPlugin.svg?label=Build)](http://travis-ci.org/LeventErkok/sbvPlugin) +[![Build Status](http://img.shields.io/travis/LeventErkok/sbvPlugin.svg?label=Build)](http://travis-ci.com/LeventErkok/sbvPlugin) ### Example diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -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