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.2.2, 2022-04-27 +* Latest Hackage released version: 9.4.4, 2023-01-16 + +### Version 9.4.4, 2023-01-16 + * Changes required to compile with GHC 9.4.4 + * Bump up sbv dependence to >= 9.2 ### Version 9.2.2, 2022-04-27 * Changes required to compile with GHC 9.2.2 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 @@ -39,6 +39,8 @@ import Data.SBV.Plugin.Common import Data.SBV.Plugin.Data +import Debug.Trace + -- | Dispatch the analyzer over bindings analyzeBind :: Config -> CoreBind -> CoreM () analyzeBind cfg@Config{sbvAnnotation, cfgEnv} = go @@ -138,11 +140,11 @@ let marker = "[SBV] " ++ showSpan flags (pickSpan curLoc) tag s = marker ++ " " ++ s tab s = replicate (length marker) ' ' ++ " " ++ s - msg = concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es + note = concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es #if MIN_VERSION_base(4,9,0) - errorWithoutStackTrace msg + errorWithoutStackTrace note #else - error msg + error note #endif res initEnv topLoc = do @@ -228,6 +230,13 @@ Nothing -> debugTrace ("Uninterpreting: " ++ sh (v, k, nub $ sort $ map (fst . fst) (M.toList envMap))) $ uninterpret False t v + tgo _ (App (Var dataCon) (Lit (LitNumber LitNumInt i))) + | Just con <- isDataConWorkId_maybe dataCon, con `elem` [integerISDataCon, integerIPDataCon, integerINDataCon] + = return $ Base $ S.svInteger S.KUnbounded (v con) + where v con | con == integerINDataCon = -i + | True = i + + -- Other literals tgo t e@(Lit l) = do Env{machWordSize} <- ask case l of LitChar{} -> unint @@ -238,7 +247,7 @@ 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 + LitNumBigNat -> unint 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 @@ -249,7 +258,6 @@ 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 where unint = do Env{flags} <- ask k <- getType noSrcSpan t 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 @@ -19,6 +19,7 @@ import Control.Monad.Reader import GHC.Plugins +import qualified GHC.Data.Strict as GDS (Maybe(Nothing)) import GHC.Types.Tickish import GHC.Types.CostCentre @@ -168,7 +169,7 @@ -- | Compute the span given a Tick. Returns the old-span if the tick span useless. tickSpan :: GenTickish t -> SrcSpan tickSpan (ProfNote cc _ _) = cc_loc cc -tickSpan (SourceNote s _) = RealSrcSpan s Nothing +tickSpan (SourceNote s _) = RealSrcSpan s GDS.Nothing tickSpan _ = noSrcSpan -- | Compute the span for a binding. 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 @@ -9,9 +9,9 @@ -- The environment for mapping concrete functions/types to symbolic ones. ----------------------------------------------------------------------------- -{-# LANGUAGE MagicHash #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE TemplateHaskellQuotes #-} {-# OPTIONS_GHC -Wall -Werror #-} @@ -363,8 +363,8 @@ Nothing -> f =<< lookInModule (TH.nameModule n) (TH.nameBase n) where lookInModule Nothing _ = error $ "[SBV] Impossible happened, while trying to locate GHC name for: " ++ show n lookInModule (Just inModule) bn = do - env <- getHscEnv - liftIO $ do r <- findImportedModule env (mkModuleName inModule) Nothing + env@HscEnv{hsc_NC} <- getHscEnv + liftIO $ do r <- findImportedModule env (mkModuleName inModule) NoPkgQual case r of - Found _ mdl -> lookupOrigIO env mdl (mkVarOcc bn) + Found _ mdl -> lookupNameCache hsc_NC mdl (mkVarOcc bn) _ -> error $ "[SBV] Impossible happened, can't find " ++ show bn ++ " in module " ++ show inModule 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 @@ -10,7 +10,11 @@ -- ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} + +#ifndef HADDOCK {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} +#endif {-# OPTIONS_GHC -Wall -Werror #-} @@ -24,7 +28,9 @@ import Prelude hiding(elem) -- | SBVPlugin can only see definitions in the current module. So we define `elem` ourselves. -elem :: Eq a => a -> [a] -> Bool +-- Also, it has to be monomoprhized, as the plugin isn't smart enough to deal with polymorphic +-- functions out-of-the-box. +elem :: Word32 -> [Word32] -> Bool elem _ [] = False elem k (x:xs) = k == x || elem k xs @@ -99,3 +105,6 @@ hasZero = b3 || b2 || b1 || b0 fastHasZero = ((v - 0x01010101) .&. complement v .&. 0x80808080) /= 0 + +{-# ANN module ("HLint: ignore Use min" :: String) #-} +{-# ANN module ("HLint: ignore Use max" :: String) #-} diff --git a/Data/SBV/Plugin/Examples/Maximum.hs b/Data/SBV/Plugin/Examples/Maximum.hs --- a/Data/SBV/Plugin/Examples/Maximum.hs +++ b/Data/SBV/Plugin/Examples/Maximum.hs @@ -9,7 +9,12 @@ -- Shows that a naive definition of maximum doing bit-vector arithmetic -- is incorrect. ----------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} + +#ifndef HADDOCK {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} +#endif {-# OPTIONS_GHC -Wall -Werror #-} @@ -17,6 +22,9 @@ import Data.SBV.Plugin +-- | Compute the maximum of three integers, which +-- is intuitively correct for unbounded values, but +-- not for bounded bit-vectors. myMax :: Int -> Int -> Int -> Int myMax x y z | x-y >= 0 && x-z >= 0 = x | y-x >= 0 && y-z >= 0 = y 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 @@ -9,7 +9,11 @@ -- An implementation of merge-sort and its correctness. ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} + +#ifndef HADDOCK {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} +#endif {-# OPTIONS_GHC -Wall -Werror #-} @@ -28,7 +32,7 @@ -} -- | Merging two given sorted lists, preserving the order. -merge :: Ord a => [a] -> [a] -> [a] +merge :: [Int] -> [Int] -> [Int] merge [] ys = ys merge xs [] = xs merge xs@(x:xr) ys@(y:yr) @@ -36,12 +40,12 @@ | True = y : merge xs yr -- | Simple merge-sort implementation. -mergeSort :: Ord a => [a] -> [a] +mergeSort :: [Int] -> [Int] mergeSort [] = [] mergeSort [x] = [x] mergeSort xs = merge (mergeSort th) (mergeSort bh) where (th, bh) = halve xs ([], []) - halve :: [a] -> ([a], [a]) -> ([a], [a]) + halve :: [Int] -> ([Int], [Int]) -> ([Int], [Int]) halve [] sofar = sofar halve (a:as) (fs, ss) = halve as (ss, a:fs) @@ -58,7 +62,7 @@ -} -- | Check whether a given sequence is non-decreasing. -nonDecreasing :: Ord a => [a] -> Bool +nonDecreasing :: [Int] -> Bool nonDecreasing [] = True nonDecreasing [_] = True nonDecreasing (a:b:xs) = a <= b && nonDecreasing (b:xs) @@ -66,9 +70,9 @@ -- | Check whether two given sequences are permutations. We simply check that each sequence -- is a subset of the other, when considered as a set. The check is slightly complicated -- for the need to account for possibly duplicated elements. -isPermutationOf :: Eq a => [a] -> [a] -> Bool +isPermutationOf :: [Int] -> [Int] -> Bool isPermutationOf as bs = go as [(b, True) | b <- bs] && go bs [(a, True) | a <- as] - where go :: Eq a => [a] -> [(a, Bool)] -> Bool + where go :: [Int] -> [(Int, Bool)] -> Bool go [] _ = True go (x:xs) ys = found && go xs ys' where (found, ys') = mark x ys @@ -76,7 +80,7 @@ -- Go and mark off an instance of 'x' in the list, if possible. We keep track -- of unmarked elements by associating a boolean bit. Note that we have to -- keep the lists equal size for the recursive result to merge properly. - mark :: Eq a => a -> [(a, Bool)] -> (Bool, [(a, Bool)]) + mark :: Int -> [(Int, Bool)] -> (Bool, [(Int, Bool)]) mark _ [] = (False, []) mark x ((y, v) : ys) | v && x == y = (True, (y, not v) : ys) 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 @@ -11,7 +11,11 @@ -- ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} + +#ifndef HADDOCK {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} +#endif {-# OPTIONS_GHC -Wall -Werror #-} @@ -74,12 +78,12 @@ -- @ -- [SBV] MicroController.hs:85:1-8 Proving "checkBad", using Z3. -- [Z3] Falsifiable. Counter-example: --- range = 0 :: Int64 +-- range = 200 :: Int64 -- manual = False :: Bool -- timeSince = 9 :: Int64 -- @ -- --- We're being told that if the range is 0, and manual override is off, and time-since last is 9, +-- 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 -- never want to go 'maxTimeSince' cycles without sending a signal! {-# ANN checkBad theorem {options = [IgnoreFailure]} #-} 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 @@ -11,7 +11,11 @@ -- ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-} + +#ifndef HADDOCK {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} +#endif {-# OPTIONS_GHC -Wall -Werror #-} diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -2,8 +2,6 @@ On Hackage: http://hackage.haskell.org/package/sbvPlugin -[![Build Status](http://img.shields.io/travis/LeventErkok/sbvPlugin.svg?label=Build)](http://travis-ci.com/LeventErkok/sbvPlugin) - ### Example ```haskell diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -1,5 +1,5 @@ Name : sbvPlugin -Version : 9.2.2 +Version : 9.4.4 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.2.2 +Tested-With : GHC==9.4.4 source-repository head type: git @@ -34,10 +34,10 @@ , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController build-depends : base >= 4.11 && < 5 - , ghc >= 9.2.2 + , sbv >= 9.2 + , ghc >= 9.4.4 , ghc-prim , containers - , sbv >= 9.0 , 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 @@ -31,6 +31,7 @@ runTest f = goldenVsFile f gld out act where (inp, hi, o, gld, out) = fileNames f act = do void $ system $ unwords ["ghc", "-c", inp, ">", out, "2>&1"] + void $ system $ unwords ["sed", "-i", "''", "'s/^Loaded package environment from.*/Loaded package environment from test-modified path/g'", out] void $ system $ unwords ["/bin/rm", "-f", hi, o] fileNames :: FilePath -> (FilePath, FilePath, FilePath, FilePath, FilePath)