diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,12 @@ * Hackage: * GitHub: +### Version 10.10, 2024-05-11 + + * Add EqSymbolic, OrdSymbolic and Mergeable instances for NonEmpty type + + * Better handling of spawned processes, avoiding zombies. Thanks to Sirui Lu for the patch. + ### Version 10.9, 2024-04-05 * Fix printing of floats to be more consistent, using lowercase letters @@ -1195,7 +1201,7 @@ due to the current limitations in SMT-solvers. However, there is a pending SMTLib proposal to support unicode, and SBV will track these changes to have full unicode support: For further details - see: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml + see: https://smt-lib.org/theories-UnicodeStrings.shtml The 'SString' type is the type of symbolic strings, consisting of characters from the Latin-1 character set currently, just @@ -2116,7 +2122,7 @@ * Tracking changes in the SMT-Lib floating-point theory. If you are using symbolic floating-point types (i.e., SFloat and SDouble), then you should upgrade to this version and also get a very latest (unstable) - Z3 release. See http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml + Z3 release. See https://smt-lib.org/theories-FloatingPoint.shtml for details. * Introduce a new class, 'RoundingFloat', which supports floating-point diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -113,7 +113,7 @@ -- all satisfying assignments. -- -- The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: --- +-- -- -- The SBV library is designed to work with any SMT-Lib compliant SMT-solver. -- Currently, we support the following SMT-Solvers out-of-the box: @@ -541,7 +541,7 @@ design goal is to let SMT solvers be used without any knowledge of how SMT solvers work or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers. -To that end, we use the SMT-Lib standard () +To that end, we use the SMT-Lib standard () to communicate with arbitrary SMT solvers. -} @@ -788,7 +788,7 @@ others are not (such as pi and e). SBV can deal with real numbers just fine, since the theory of reals is decidable. (See -.) In addition, by leveraging backend +.) In addition, by leveraging backend solver capabilities, SBV can also represent and solve non-linear equations involving real-variables. (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.) -} @@ -801,7 +801,7 @@ {- $strings Support for characters, strings, and regular expressions (initial version contributed by Joel Burget) -adds support for QF_S logic, described here: +adds support for QF_S logic, described here: See "Data.SBV.Char", "Data.SBV.String", "Data.SBV.RegExp" for related functions. -} diff --git a/Data/SBV/Char.hs b/Data/SBV/Char.hs --- a/Data/SBV/Char.hs +++ b/Data/SBV/Char.hs @@ -14,7 +14,7 @@ -- and strings. -- -- 'SChar' type only covers all unicode characters, following the specification --- in . +-- in . -- However, some of the recognizers only support the Latin1 subset, suffixed -- by @L1@. The reason for this is that there is no performant way of performing -- these functions for the entire unicode set. As SMTLib's capabilities increase, diff --git a/Data/SBV/Control/Types.hs b/Data/SBV/Control/Types.hs --- a/Data/SBV/Control/Types.hs +++ b/Data/SBV/Control/Types.hs @@ -84,7 +84,7 @@ show Version = ":version" show (InfoKeyword s) = s --- | Option values that can be set in the solver, following the SMTLib specification . +-- | Option values that can be set in the solver, following the SMTLib specification . -- -- Note that not all solvers may support all of these! -- @@ -183,7 +183,7 @@ -- | SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the -- user can override this choice using a call to 'Data.SBV.setLogic' This is especially handy if one is experimenting with custom --- logics that might be supported on new solvers. See for the official list. +-- logics that might be supported on new solvers. See for the official list. data Logic = AUFLIA -- ^ Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values. | AUFLIRA -- ^ Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value. diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -1898,7 +1898,17 @@ liftIO $ writeIORef (runMode st) $ SMTMode qc IRun isSAT cfg - lift $ join $ liftIO $ backend cfg' st (show pgm) $ extractIO . runReaderT userQuery + let terminateSolver maybeForwardedException = do + qs <- readIORef $ rQueryState st + case qs of + Nothing -> return () + Just QueryState{queryTerminate} -> queryTerminate maybeForwardedException + + lift $ join $ liftIO $ C.mask $ \restore -> do + r <- restore (extractIO $ join $ liftIO $ backend cfg' st (show pgm) $ extractIO . runReaderT userQuery) + `C.catch` \e -> terminateSolver (Just e) >> C.throwIO (e :: C.SomeException) + terminateSolver Nothing + return r -- Already in a query, in theory we can just continue, but that causes use-case issues -- so we reject it. TODO: Review if we should actually support this. The issue arises with diff --git a/Data/SBV/Core/Data.hs b/Data/SBV/Core/Data.hs --- a/Data/SBV/Core/Data.hs +++ b/Data/SBV/Core/Data.hs @@ -174,7 +174,7 @@ type SFPQuad = SBV FPQuad -- | A symbolic character. Note that this is the full unicode character set. --- see: +-- see: -- for details. type SChar = SBV Char @@ -717,7 +717,7 @@ -- newArray, we must provide a dummy implementation for newArrayInState: newArrayInState = error "undefined: newArrayInState" --- | Arrays implemented in terms of SMT-arrays: +-- | Arrays implemented in terms of SMT-arrays: -- -- * Maps directly to SMT-lib arrays -- diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -71,6 +71,9 @@ import Data.String (IsString(..)) import Data.Word (Word8, Word16, Word32, Word64) +import Data.List.NonEmpty (NonEmpty(..)) +import qualified Data.List.NonEmpty as NE + import qualified Data.Set as Set import Data.Proxy @@ -959,6 +962,13 @@ _ .< [] = sFalse (x:xs) .< (y:ys) = x .< y .|| (x .== y .&& xs .< ys) +-- NonEmpty +instance EqSymbolic a => EqSymbolic (NonEmpty a) where + (x :| xs) .== (y :| ys) = x : xs .== y : ys + +instance OrdSymbolic a => OrdSymbolic (NonEmpty a) where + (x :| xs) .< (y :| ys) = x : xs .< y : ys + -- Maybe instance EqSymbolic a => EqSymbolic (Maybe a) where Nothing .== Nothing = sTrue @@ -2041,6 +2051,15 @@ ("Branches produce different sizes: " ++ show lxs ++ " vs " ++ show lys ++ ". Must have the same length.") "Use the 'SList' type (and Data.SBV.List routines) to model fully symbolic lists." where (lxs, lys) = (length xs, length ys) + +-- NonEmpty +instance Mergeable a => Mergeable (NonEmpty a) where + symbolicMerge f t xs ys + | lxs == lys = NE.zipWith (symbolicMerge f t) xs ys + | True = cannotMerge "non-empty lists" + ("Branches produce different sizes: " ++ show lxs ++ " vs " ++ show lys ++ ". Must have the same length.") + "Use the 'SList' type (and Data.SBV.List routines) to model fully symbolic lists." + where (lxs, lys) = (length xs, length ys) -- ZipList instance Mergeable a => Mergeable (ZipList a) where diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -89,6 +89,7 @@ import GHC.Stack.Types import GHC.Generics (Generic) +import qualified Control.Exception as C import qualified Control.Monad.State.Lazy as LS import qualified Control.Monad.State.Strict as SS import qualified Control.Monad.Writer.Lazy as LW @@ -778,7 +779,7 @@ , querySend :: Maybe Int -> String -> IO () , queryRetrieveResponse :: Maybe Int -> IO String , queryConfig :: SMTConfig - , queryTerminate :: IO () + , queryTerminate :: Maybe C.SomeException -> IO () , queryTimeOutValue :: Maybe Int , queryAssertionStackDepth :: Int } @@ -1967,12 +1968,6 @@ = contextMismatchError (sbvContext st) ctx Nothing Nothing mapM_ check $ nub $ G.universeBi res - - -- Clean-up after ourselves - qs <- liftIO $ readIORef $ rQueryState st - case qs of - Nothing -> return () - Just QueryState{queryTerminate} -> liftIO queryTerminate return (r, res) diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -862,7 +862,7 @@ ex <- waitForProcess pid `C.catch` (\(e :: C.SomeException) -> handleAsync e (return (ExitFailure (-999)))) return (out, err, ex) - cleanUp + cleanUp maybeForwardedException = do (out, err, ex) <- terminateSolver msg $ [ "Solver : " ++ nm @@ -874,23 +874,24 @@ finalizeTranscript (transcript cfg) ex recordEndTime cfg ctx - case ex of - ExitSuccess -> return () - _ -> if ignoreExitCode cfg - then msg ["Ignoring non-zero exit code of " ++ show ex ++ " per user request!"] - else C.throwIO SBVException { sbvExceptionDescription = "Failed to complete the call to " ++ nm - , sbvExceptionSent = Nothing - , sbvExceptionExpected = Nothing - , sbvExceptionReceived = Nothing - , sbvExceptionStdOut = Just out - , sbvExceptionStdErr = Just err - , sbvExceptionExitCode = Just ex - , sbvExceptionConfig = cfg { solver = (solver cfg) { executable = execPath } } - , sbvExceptionReason = Nothing - , sbvExceptionHint = if not (verbose cfg) - then Just ["Run with 'verbose=True' for further information"] - else Nothing - } + case (ex, maybeForwardedException) of + (_, Just forwardedException) -> C.throwIO forwardedException + (ExitSuccess, _) -> return () + _ -> if ignoreExitCode cfg + then msg ["Ignoring non-zero exit code of " ++ show ex ++ " per user request!"] + else C.throwIO SBVException { sbvExceptionDescription = "Failed to complete the call to " ++ nm + , sbvExceptionSent = Nothing + , sbvExceptionExpected = Nothing + , sbvExceptionReceived = Nothing + , sbvExceptionStdOut = Just out + , sbvExceptionStdErr = Just err + , sbvExceptionExitCode = Just ex + , sbvExceptionConfig = cfg { solver = (solver cfg) { executable = execPath } } + , sbvExceptionReason = Nothing + , sbvExceptionHint = if not (verbose cfg) + then Just ["Run with 'verbose=True' for further information"] + else Nothing + } return (send, ask, getResponseFromSolver, terminateSolver, cleanUp, pid) diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -1299,7 +1299,7 @@ in c1 ++ c2 ----------------------------------------------------------------------------------------------- --- Casts supported by SMTLib. (From: ) +-- Casts supported by SMTLib. (From: ) -- ; from another floating point sort -- ((_ to_fp eb sb) RoundingMode (_ FloatingPoint mb nb) (_ FloatingPoint eb sb)) -- diff --git a/Data/SBV/Utils/ExtractIO.hs b/Data/SBV/Utils/ExtractIO.hs --- a/Data/SBV/Utils/ExtractIO.hs +++ b/Data/SBV/Utils/ExtractIO.hs @@ -32,7 +32,7 @@ -- | Trivial IO extraction for 'IO'. instance ExtractIO IO where - extractIO = pure + extractIO = fmap pure -- | IO extraction for 'MaybeT'. instance ExtractIO m => ExtractIO (MaybeT m) where diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -148,6 +148,7 @@ John Matthews, Curran McConnell, Philipp Meyer, +Fabian Mitterwallner, Joshua Moerman, Matt Parker, Jan Path, diff --git a/SBVTestSuite/GoldFiles/allSat8.gold b/SBVTestSuite/GoldFiles/allSat8.gold --- a/SBVTestSuite/GoldFiles/allSat8.gold +++ b/SBVTestSuite/GoldFiles/allSat8.gold @@ -38,6 +38,8 @@ [RECV] sat [SEND] (get-value (f)) [RECV] ((f (lambda ((x!1 Int)) (+ 1 x!1)))) +*** Solver : Z3 +*** Exit code: ExitFailure (-15) EXCEPTION CAUGHT: @@ -61,4 +63,4 @@ *** NB. If this is a use case you'd like SBV to support, please get in touch! CallStack (from HasCallStack): - error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.9-inplace:Data.SBV.Control.Utils + error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.10-inplace:Data.SBV.Control.Utils diff --git a/SBVTestSuite/GoldFiles/nested1.gold b/SBVTestSuite/GoldFiles/nested1.gold --- a/SBVTestSuite/GoldFiles/nested1.gold +++ b/SBVTestSuite/GoldFiles/nested1.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.9-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.10-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested2.gold b/SBVTestSuite/GoldFiles/nested2.gold --- a/SBVTestSuite/GoldFiles/nested2.gold +++ b/SBVTestSuite/GoldFiles/nested2.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.9-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.10-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested3.gold b/SBVTestSuite/GoldFiles/nested3.gold --- a/SBVTestSuite/GoldFiles/nested3.gold +++ b/SBVTestSuite/GoldFiles/nested3.gold @@ -37,4 +37,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.9-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.10-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested4.gold b/SBVTestSuite/GoldFiles/nested4.gold --- a/SBVTestSuite/GoldFiles/nested4.gold +++ b/SBVTestSuite/GoldFiles/nested4.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.9-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.10-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/noOpt1.gold b/SBVTestSuite/GoldFiles/noOpt1.gold --- a/SBVTestSuite/GoldFiles/noOpt1.gold +++ b/SBVTestSuite/GoldFiles/noOpt1.gold @@ -22,6 +22,8 @@ [GOOD] ; --- arraySetups --- [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- +*** Solver : Z3 +*** Exit code: ExitFailure (-15) @@ -29,4 +31,4 @@ *** Use "sat" for plain satisfaction CallStack (from HasCallStack): - + error, called at ./Data/SBV/Provers/Prover.hs:261:27 in sbv-10.10-inplace:Data.SBV.Provers.Prover diff --git a/SBVTestSuite/GoldFiles/noOpt2.gold b/SBVTestSuite/GoldFiles/noOpt2.gold --- a/SBVTestSuite/GoldFiles/noOpt2.gold +++ b/SBVTestSuite/GoldFiles/noOpt2.gold @@ -24,6 +24,8 @@ [GOOD] ; --- arraySetups --- [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- +*** Solver : Z3 +*** Exit code: ExitFailure (-15) @@ -31,4 +33,4 @@ *** Use "optimize"/"optimizeWith" to calculate optimal satisfaction! CallStack (from HasCallStack): - + error, called at ./Data/SBV/Provers/Prover.hs:608:33 in sbv-10.10-inplace:Data.SBV.Provers.Prover diff --git a/SBVTestSuite/TestSuite/Optimization/NoOpt.hs b/SBVTestSuite/TestSuite/Optimization/NoOpt.hs --- a/SBVTestSuite/TestSuite/Optimization/NoOpt.hs +++ b/SBVTestSuite/TestSuite/Optimization/NoOpt.hs @@ -28,6 +28,4 @@ [ goldenCapturedIO "noOpt1" $ \rf -> c rf $ optimizeWith z3{verbose=True, redirectVerbose=Just rf} Lexicographic (\x -> x .== (x::SWord8)) , goldenCapturedIO "noOpt2" $ \rf -> c rf $ satWith z3{verbose=True, redirectVerbose=Just rf} (\x -> maximize "mx" (x::SWord8)) ] - where -- catch the exception and put it in the file. Note that we trim the last line since it contains the - -- cabal hash of the library, which is bound to change - c rf cont = void cont `C.catch` (\(e :: C.SomeException) -> appendFile rf ("\n\n" ++ unlines (init (lines (show e))) ++ "\n")) + where c rf cont = void cont `C.catch` (\(e :: C.SomeException) -> appendFile rf ("\n\n" ++ show e)) diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv -Version : 10.9 +Version : 10.10 Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT