packages feed

crux 0.7.1 → 0.7.2

raw patch · 5 files changed

+82/−7 lines, 5 filesdep +crucible-debugdep +crucible-syntaxnew-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: crucible-debug, crucible-syntax

API changes (from Hackage documentation)

+ Crux: [debug] :: CruxOptions -> Bool
+ Crux.Config.Common: [debug] :: CruxOptions -> Bool
+ Crux.Config.Solver: Bitwuzla :: SolverOnline
- Crux: CruxOptions :: [FilePath] -> FilePath -> FilePath -> Bool -> Bool -> Bool -> Bool -> PathStrategy -> Maybe NominalDiffTime -> Maybe DiffTime -> NominalDiffTime -> Maybe Word64 -> Maybe Word64 -> Bool -> Bool -> Maybe Word64 -> String -> Maybe String -> Bool -> Maybe FilePath -> Maybe FilePath -> Maybe FilePath -> Bool -> String -> Bool -> Bool -> Bool -> Bool -> Bool -> ProblemFeatures -> OutputOptions -> CruxOptions
+ Crux: CruxOptions :: [FilePath] -> FilePath -> FilePath -> Bool -> Bool -> Bool -> Bool -> PathStrategy -> Maybe NominalDiffTime -> Maybe DiffTime -> NominalDiffTime -> Maybe Word64 -> Maybe Word64 -> Bool -> Bool -> Maybe Word64 -> String -> Maybe String -> Bool -> Maybe FilePath -> Maybe FilePath -> Maybe FilePath -> Bool -> String -> Bool -> Bool -> Bool -> Bool -> Bool -> ProblemFeatures -> OutputOptions -> Bool -> CruxOptions
- Crux.Config.Common: CruxOptions :: [FilePath] -> FilePath -> FilePath -> Bool -> Bool -> Bool -> Bool -> PathStrategy -> Maybe NominalDiffTime -> Maybe DiffTime -> NominalDiffTime -> Maybe Word64 -> Maybe Word64 -> Bool -> Bool -> Maybe Word64 -> String -> Maybe String -> Bool -> Maybe FilePath -> Maybe FilePath -> Maybe FilePath -> Bool -> String -> Bool -> Bool -> Bool -> Bool -> Bool -> ProblemFeatures -> OutputOptions -> CruxOptions
+ Crux.Config.Common: CruxOptions :: [FilePath] -> FilePath -> FilePath -> Bool -> Bool -> Bool -> Bool -> PathStrategy -> Maybe NominalDiffTime -> Maybe DiffTime -> NominalDiffTime -> Maybe Word64 -> Maybe Word64 -> Bool -> Bool -> Maybe Word64 -> String -> Maybe String -> Bool -> Maybe FilePath -> Maybe FilePath -> Maybe FilePath -> Bool -> String -> Bool -> Bool -> Bool -> Bool -> Bool -> ProblemFeatures -> OutputOptions -> Bool -> CruxOptions

Files

+ CHANGELOG.md view
@@ -0,0 +1,21 @@+# 0.7.2 -- 2025-03-21++* Add support for the Bitwuzla SMT solver.+* Add `--debug` option for starting the Crucible debugger.+* For the sake of the `--debug` flag, Crux now depends on the+  `crucible-{debug,syntax}` packages.++# 0.7.1 -- 2024-08-30++* Add support for GHC 9.8++# 0.7 -- 2024-02-05++* Add a `Crux.Overrides` module, which defines common functionality for defining+  overrides, which are shared among several Crux backends.++# 0.6++* Corresponds to the 0.6 release of `crux-llvm` and `crux-mir`.+* `SimulatorCallbacks` now returns `SimulatorHooks`, a new data type that+  allows hooking into the simulation process at various steps.
crux.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crux-Version:       0.7.1+Version:       0.7.2 Copyright:     (c) Galois, Inc. 2018-2022 Author:        sweirich@galois.com Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com@@ -17,6 +17,8 @@   verification, usually by embedding verification specifications in   the source language. +extra-doc-files:  CHANGELOG.md+ source-repository head   type:     git   location: https://github.com/GaloisInc/crucible@@ -34,6 +36,8 @@     containers,     contravariant >= 1.5 && < 1.6,     crucible,+    crucible-debug,+    crucible-syntax,     directory,     filepath,     generic-lens,
src/Crux.hs view
@@ -28,6 +28,7 @@   , module Crux.Log   ) where +import qualified Control.Applicative as Applicative import qualified Control.Exception as Ex import           Control.Lens import           Control.Monad ( unless, void, when )@@ -53,6 +54,7 @@ import           System.IO ( Handle, hPutStr, stdout, stderr )  import           Data.Parameterized.Classes+import qualified Data.Parameterized.Map as MapF import           Data.Parameterized.Nonce (newIONonceGenerator, NonceGenerator) import           Data.Parameterized.Some ( Some(..) ) @@ -60,6 +62,7 @@ import           Lang.Crucible.Backend.Online import qualified Lang.Crucible.Backend.Simple as CBS import           Lang.Crucible.CFG.Extension+import qualified Lang.Crucible.Debug as Debug import           Lang.Crucible.Simulator import           Lang.Crucible.Simulator.BoundedExec import           Lang.Crucible.Simulator.BoundedRecursion@@ -67,6 +70,7 @@ import           Lang.Crucible.Simulator.PathSplitting import           Lang.Crucible.Simulator.PositionTracking import           Lang.Crucible.Simulator.Profiling+import qualified Lang.Crucible.Syntax.Concrete as Syn import           Lang.Crucible.Types  @@ -76,6 +80,7 @@ import           What4.Interface (IsExprBuilder, getConfiguration) import           What4.Protocol.Online (OnlineSolver) import qualified What4.Solver as WS+import           What4.Solver.Bitwuzla (bitwuzlaTimeout) import           What4.Solver.CVC4 (cvc4Timeout) import           What4.Solver.CVC5 (cvc5Timeout) import           What4.Solver.Yices (yicesEnableMCSat, yicesGoalTimeout)@@ -364,6 +369,7 @@         CCS.CVC5 -> withOnlineBackendFM WE.FloatRealRepr         CCS.STP -> withOnlineBackendFM WE.FloatRealRepr         CCS.Z3 -> withOnlineBackendFM WE.FloatIEEERepr+        CCS.Bitwuzla -> withOnlineBackendFM WE.FloatIEEERepr     fm -> fail ("Unknown floating point mode: " ++ fm ++ "; expected one of [real|ieee|uninterpreted|default]")    where@@ -415,6 +421,11 @@          Just s -> symCfg sym z3Timeout (floor (s * 1000))          Nothing -> return ()        k bak+     CCS.Bitwuzla -> withBitwuzlaOnlineBackend sym unsatCoreFeat extraFeatures $ \bak -> do+       case goalTimeout cruxOpts of+         Just s -> symCfg sym bitwuzlaTimeout (floor (s * 1000))+         Nothing -> return ()+       k bak      CCS.STP -> do        -- We don't have a timeout option for STP        case goalTimeout cruxOpts of@@ -556,6 +567,7 @@     CCS.SolverOnline CCS.STP -> k WS.stpAdapter     CCS.SolverOnline CCS.Yices -> k WS.yicesAdapter     CCS.SolverOnline CCS.Z3 -> k WS.z3Adapter+    CCS.SolverOnline CCS.Bitwuzla -> k WS.bitwuzlaAdapter  withSolverAdapters :: [CCS.SolverOffline] -> ([WS.SolverAdapter st] -> a) -> a withSolverAdapters solverOffs k =@@ -667,14 +679,38 @@     RunnableStateWithExtensions initSt exts <- setup bak monline     explainFailure <- onError bak +    -- This can't be initialized with the rest of the execution features,+    -- because it is not a 'GenericExecutionFeature'.+    --+    -- Ideally, we would use language-extension-specific command extensions+    -- (e.g., LLVM commands for Crux-LLVM) and parser hooks, but that would+    -- require some refactoring to pass those in...+    let debugging = debug cruxOpts+    debugger <-+      if debugging+      then do+        let ?parserHooks = Syn.ParserHooks Applicative.empty Applicative.empty+        let cExts = Debug.voidExts+        inps <- Debug.defaultDebuggerInputs cExts+        dbg <-+          Debug.debugger+            cExts+            Debug.voidImpl+            (Debug.IntrinsicPrinters MapF.empty)+            inps+            Debug.defaultDebuggerOutputs+            UnitRepr+        pure [dbg]+      else pure []+     -- execute the simulator     case pathStrategy cruxOpts of       AlwaysMergePaths ->-        do res <- executeCrucible (map genericToExecutionFeature execFeatures ++ exts) initSt+        do res <- executeCrucible (map genericToExecutionFeature execFeatures ++ exts ++ debugger) initSt            void $ resultCont compRef glsRef frm explainFailure (Result res)       SplitAndExploreDepthFirst ->         do (i,ws) <- executeCrucibleDFSPaths-                         (map genericToExecutionFeature execFeatures ++ exts)+                         (map genericToExecutionFeature execFeatures ++ exts ++ debugger)                          initSt                          (resultCont compRef glsRef frm explainFailure . Result)            sayCrux (Log.TotalPathsExplored i)
src/Crux/Config/Common.hs view
@@ -205,6 +205,9 @@   , outputOptions            :: OutputOptions     -- ^ Output options grouped together for easy transfer to the logger +  , debug                    :: Bool+    -- ^ Drop into the Crucible debugger before simulation begins+   }   deriving (Generic) @@ -364,6 +367,10 @@            onlineProblemFeatures <- pure noFeatures +          debug <-+            section "debug" yesOrNoSpec False+            "Drop into the Crucible debugger before simulation begins"+           pure CruxOptions             { outputOptions = OutputOptions               { colorOptions = ColorOptions@@ -525,6 +532,10 @@          ++ " i.e. one of [real|ieee|uninterpreted|default]. "          ++ "Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.")         $ ReqArg "FPREP" $ \v opts -> Right opts { floatMode = map toLower v }++      , Option [] ["debug"]+        "Drop into the Crucible debugger before simulation begins"+        $ NoArg $ \opts -> Right opts { debug = True }       ]   }
src/Crux/Config/Solver.hs view
@@ -23,7 +23,7 @@  import qualified Crux.Config.Common as CCC -data SolverOnline = Yices | Z3 | CVC4 | CVC5 | STP+data SolverOnline = Yices | Z3 | CVC4 | CVC5 | STP | Bitwuzla   deriving (Eq, Ord, Show) data SolverOffline = SolverOnline SolverOnline | Boolector | DReal   deriving (Eq, Ord, Show)@@ -43,6 +43,7 @@       STP -> k WEB.FloatRealRepr       Yices -> k WEB.FloatRealRepr       Z3 -> k WEB.FloatIEEERepr+      Bitwuzla -> k WEB.FloatIEEERepr  instance HasDefaultFloatRepr SolverOffline where   withDefaultFloatRepr st s k =@@ -124,11 +125,12 @@       "cvc4" -> pure (SolverOnline CVC4)       "cvc5" -> pure (SolverOnline CVC5)       "stp" -> pure (SolverOnline STP)-      _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, or stp)" s)+      "bitwuzla" -> pure (SolverOnline Bitwuzla)+      _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, stp, or bitwuzla)" s)  asManyOfflineSolvers :: String -> Validated [SolverOffline] asManyOfflineSolvers s-  | s == "all"         = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc4,cvc5,stp"+  | s == "all"         = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc4,cvc5,stp,bitwuzla"   | length solvers > 1 = traverse asAnyOfflineSolver solvers   | otherwise          = invalid (printf "%s is not a valid solver list (expected 'all' or a comma separated list of solvers)" s)   where@@ -143,7 +145,8 @@     "cvc5" -> pure CVC5     "z3" -> pure Z3     "stp" -> pure STP-    _ -> invalid (printf "%s is not a valid online solver (expected yices, cvc4, cvc5, z3, or stp)" s)+    "bitwuzla" -> pure Bitwuzla+    _ -> invalid (printf "%s is not a valid online solver (expected yices, cvc4, cvc5, z3, stp, or bitwuzla)" s)  -- | Examine a 'CCC.CruxOptions' and determine what solver configuration to use for -- symbolic execution.  This can fail if an invalid solver configuration is