packages feed

sbvPlugin 9.2.2 → 9.4.4

raw patch · 12 files changed

+70/−29 lines, 12 filesdep ~ghcdep ~sbv

Dependency ranges changed: ghc, sbv

Files

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.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
Data/SBV/Plugin/Analyze.hs view
@@ -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
Data/SBV/Plugin/Common.hs view
@@ -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.
Data/SBV/Plugin/Env.hs view
@@ -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
Data/SBV/Plugin/Examples/BitTricks.hs view
@@ -10,7 +10,11 @@ --      <https://graphics.stanford.edu/~seander/bithacks.html> ----------------------------------------------------------------------------- +{-# 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) #-}
Data/SBV/Plugin/Examples/Maximum.hs view
@@ -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
Data/SBV/Plugin/Examples/MergeSort.hs view
@@ -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)
Data/SBV/Plugin/Examples/MicroController.hs view
@@ -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]} #-}
Data/SBV/Plugin/Examples/Proved.hs view
@@ -11,7 +11,11 @@ -- ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-}++#ifndef HADDOCK {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-}+#endif  {-# OPTIONS_GHC -Wall -Werror #-}
README.md view
@@ -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
sbvPlugin.cabal view
@@ -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
tests/Run.hs view
@@ -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)