crux 0.7.2 → 0.8.0.0

raw patch · 10 files changed

+278/−52 lines, 10 filesdep +file-embeddep +githashdep +rme-what4dep ~crucible-debugnew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: file-embed, githash, rme-what4

Dependency ranges changed: crucible-debug

API changes (from Hackage documentation)

Files

• CHANGELOG.md +10/−0
• crux.buildinfo.json +5/−0
• crux.cabal +7/−2
• src/Crux.hs +51/−24
• src/Crux/Config/Solver.hs +8/−5
• src/Crux/GitHash.hs +29/−0
• src/Crux/Log.hs +19/−5
• src/Crux/Model.hs +27/−4
• src/Crux/UI/JS.hs +35/−11
• src/Crux/Version.hs +87/−1

@@ -1,3 +1,13 @@+# 0.8 -- 2025-11-09++* We now support running simulations with custom users state.+  For this reason, some of the Crux types now have an additional `st`+  parameter.++* `showBVLiteral` has been renamed to `showBVLiteralSigned` and+  two additional functions `showBVLiteralUnsigned` and `showBVLiteralDecimal`+  were added to improve printing of bit vectors+ # 0.7.2 -- 2025-03-21  * Add support for the Bitwuzla SMT solver.

@@ -0,0 +1,5 @@+{+  "hash": null,+  "branch": null,+  "dirty": null+}

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crux-Version:       0.7.2+Version:       0.8.0.0 Copyright:     (c) Galois, Inc. 2018-2022 Author:        sweirich@galois.com Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com@@ -18,6 +18,7 @@   the source language.  extra-doc-files:  CHANGELOG.md+extra-source-files: crux.buildinfo.json  source-repository head   type:     git@@ -39,8 +40,10 @@     crucible-debug,     crucible-syntax,     directory,+    file-embed ^>= 0.0.16,     filepath,     generic-lens,+    githash ^>= 0.1.7,     lens,     libBF >= 0.6 && < 0.7,     lumberjack >= 1.0 && < 1.1,@@ -60,7 +63,8 @@     config-schema >= 1.2.2.0,     semigroupoids,     xml,-    yaml >= 0.11 && < 0.12+    yaml >= 0.11 && < 0.12,+    rme-what4 ^>= 0.1,    hs-source-dirs: src @@ -86,6 +90,7 @@     Crux.Version    other-modules:+   Crux.GitHash,    Crux.UI.Jquery,    Crux.UI.IndexHtml    Paths_crux

@@ -12,6 +12,9 @@  module Crux   ( runSimulator+  , runSimulatorWithUserState+  , InitUserState(..)+  , noInitUserState   , postprocessSimResult   , loadOptions   , mkOutputConfig@@ -54,7 +57,6 @@ 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(..) ) @@ -85,6 +87,7 @@ import           What4.Solver.CVC5 (cvc5Timeout) import           What4.Solver.Yices (yicesEnableMCSat, yicesGoalTimeout) import           What4.Solver.Z3 (z3Timeout)+import           Data.RME.What4 (rmeAdapter)  import           Crux.Config import           Crux.Config.Common@@ -98,13 +101,20 @@ import           Crux.Report import           Crux.Types -pattern RunnableState :: forall sym . () => forall ext personality . (IsSyntaxExtension ext) => ExecState (personality sym) sym ext (RegEntry sym UnitType) -> RunnableState sym+pattern RunnableState ::+  forall sym. () =>+  forall ext personality.+  ( IsSyntaxExtension ext+  , Debug.HasContext (personality sym) Void sym ext UnitType+  ) =>+  ExecState (personality sym) sym ext (RegEntry sym UnitType) ->+  RunnableState sym pattern RunnableState es = RunnableStateWithExtensions es []  -- | A crucible @ExecState@ that is ready to be passed into the simulator. --   This will usually, but not necessarily, be an @InitialState@. data RunnableState sym where-  RunnableStateWithExtensions :: (IsSyntaxExtension ext)+  RunnableStateWithExtensions :: (IsSyntaxExtension ext, Debug.HasContext (personality sym) Void sym ext UnitType)                               => ExecState (personality sym) sym ext (RegEntry sym UnitType)                               -> [ExecutionFeature (personality sym) sym ext (RegEntry sym UnitType)]                               -> RunnableState sym@@ -121,10 +131,10 @@ --   * When simulation ends, regardless of the outcome, to interpret the results. -- --   All of these callbacks have access to the symbolic backend.-newtype SimulatorCallbacks msgs r+newtype SimulatorCallbacks msgs st r   = SimulatorCallbacks     { getSimulatorCallbacks ::-        forall sym bak t st fs.+        forall sym bak t fs.           ( IsSymBackend sym bak           , Logs msgs           , sym ~ WE.ExprBuilder t st fs@@ -562,6 +572,7 @@   case solverOff of     CCS.Boolector -> k WS.boolectorAdapter     CCS.DReal -> k WS.drealAdapter+    CCS.RME -> k rmeAdapter     CCS.SolverOnline CCS.CVC4 -> k WS.cvc4Adapter     CCS.SolverOnline CCS.CVC5 -> k WS.cvc5Adapter     CCS.SolverOnline CCS.STP -> k WS.stpAdapter@@ -576,6 +587,16 @@     base adapters = k adapters     go nextOff withAdapters adapters = withSolverAdapter nextOff (\adapter -> withAdapters (adapter:adapters)) ++{- | Create a fresh user state.+We use this to create a fresh user input when we create a new simulator. -}+newtype InitUserState s =+  InitUserState { initUserState :: forall t. IO (s t) }++-- | A helper to use when we don't have interesting user state.+noInitUserState :: InitUserState WE.EmptyExprBuilderState+noInitUserState = InitUserState { initUserState = pure WE.EmptyExprBuilderState }+ -- | Parse through all of the user-provided options and start up the verification process -- -- This figures out which solvers need to be run, and in which modes.  It takes@@ -586,23 +607,39 @@   Logs msgs =>   SupportsCruxLogMessage msgs =>   CruxOptions ->-  SimulatorCallbacks msgs r ->+  SimulatorCallbacks msgs WE.EmptyExprBuilderState r ->   IO r-runSimulator cruxOpts simCallback = do+runSimulator = runSimulatorWithUserState noInitUserState++-- | Parse through all of the user-provided options and start up the verification process+--+-- This figures out which solvers need to be run, and in which modes.  It takes+-- as arguments some of the results of common setup code.  It also tries to+-- minimize code duplication between the different verification paths (e.g.,+-- online vs offline solving).+runSimulatorWithUserState ::+  Logs msgs =>+  SupportsCruxLogMessage msgs =>+  InitUserState st ->+  CruxOptions ->+  SimulatorCallbacks msgs st r ->+  IO r+runSimulatorWithUserState mkUser cruxOpts simCallback = do   sayCrux (Log.Checking (inputFiles cruxOpts))   createDirectoryIfMissing True (outDir cruxOpts)   Some (nonceGen :: NonceGenerator IO s) <- newIONonceGenerator+  userState <- initUserState mkUser   case CCS.parseSolverConfig cruxOpts of      Right (CCS.SingleOnlineSolver onSolver) ->-      withSelectedOnlineBackend cruxOpts nonceGen onSolver Nothing WE.EmptyExprBuilderState $ \bak -> do+      withSelectedOnlineBackend cruxOpts nonceGen onSolver Nothing userState $ \bak -> do         let monline = Just (SomeOnlineSolver bak)         setupSolver cruxOpts (pathSatSolverOutput cruxOpts) (backendGetSym bak)         (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts bak monline         doSimWithResults cruxOpts simCallback bak execFeatures profInfo monline (proveGoalsOnline bak)      Right (CCS.OnlineSolverWithOfflineGoals onSolver offSolver) ->-      withSelectedOnlineBackend cruxOpts nonceGen onSolver Nothing WE.EmptyExprBuilderState $ \bak -> do+      withSelectedOnlineBackend cruxOpts nonceGen onSolver Nothing userState $ \bak -> do         let monline = Just (SomeOnlineSolver bak)         setupSolver cruxOpts (pathSatSolverOutput cruxOpts) (backendGetSym bak)         (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts bak monline@@ -616,9 +653,9 @@           doSimWithResults cruxOpts simCallback bak execFeatures profInfo monline (proveGoalsOffline [adapter])      Right (CCS.OnlyOfflineSolvers offSolvers) ->-      withFloatRepr (WE.EmptyExprBuilderState @s) cruxOpts offSolvers $ \floatRepr -> do+      withFloatRepr userState cruxOpts offSolvers $ \floatRepr -> do         withSolverAdapters offSolvers $ \adapters -> do-          sym <- WE.newExprBuilder floatRepr WE.EmptyExprBuilderState nonceGen+          sym <- WE.newExprBuilder floatRepr userState nonceGen           bak <- CBS.newSimpleBackend sym           setupSolver cruxOpts Nothing sym           -- Since we have a bare SimpleBackend here, we have to initialize it@@ -631,7 +668,7 @@       -- This case is probably the most complicated because it needs two       -- separate online solvers.  The two must agree on the floating point       -- mode.-      withSelectedOnlineBackend cruxOpts nonceGen pathSolver Nothing WE.EmptyExprBuilderState $ \pathSatBak -> do+      withSelectedOnlineBackend cruxOpts nonceGen pathSolver Nothing userState $ \pathSatBak -> do         let sym = backendGetSym pathSatBak         setupSolver cruxOpts (pathSatSolverOutput cruxOpts) sym         (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts pathSatBak (Just (SomeOnlineSolver pathSatBak))@@ -657,7 +694,7 @@   Logs msgs =>   SupportsCruxLogMessage msgs =>   CruxOptions ->-  SimulatorCallbacks msgs r ->+  SimulatorCallbacks msgs st r ->   bak ->   [GenericExecutionFeature sym] ->   ProfData sym ->@@ -690,17 +727,7 @@       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]+        pure [Debug.debugger Debug.voidImpl]       else pure []      -- execute the simulator

@@ -25,7 +25,7 @@  data SolverOnline = Yices | Z3 | CVC4 | CVC5 | STP | Bitwuzla   deriving (Eq, Ord, Show)-data SolverOffline = SolverOnline SolverOnline | Boolector | DReal+data SolverOffline = SolverOnline SolverOnline | Boolector | DReal | RME   deriving (Eq, Ord, Show)  class HasDefaultFloatRepr solver where@@ -50,6 +50,7 @@     case s of       SolverOnline s' -> withDefaultFloatRepr st s' k       Boolector -> k WEB.FloatUninterpretedRepr+      RME -> k WEB.FloatUninterpretedRepr       DReal -> k WEB.FloatRealRepr  -- | Test to see if an online and offline solver are actually the same@@ -106,31 +107,33 @@ invalid :: String -> Validated a invalid rsn = Invalid [rsn] --- | Boolector and DReal only support offline solving (for our purposes), so+-- | Boolector, RME and DReal only support offline solving (for our purposes), so -- attempt to parse them from the given string asOnlyOfflineSolver :: String -> Validated SolverOffline asOnlyOfflineSolver s =   case s of     "dreal" -> pure DReal     "boolector" -> pure Boolector-    _ -> invalid (printf "%s is not an offline-only solver (expected dreal or boolector)" s)+    "rme" -> pure RME+    _ -> invalid (printf "%s is not an offline-only solver (expected dreal, rme or boolector)" s)  -- | Solvers that can be used in offline mode asAnyOfflineSolver :: String -> Validated SolverOffline asAnyOfflineSolver s = case s of       "dreal" -> pure DReal       "boolector" -> pure Boolector+      "rme" -> pure RME       "z3" -> pure (SolverOnline Z3)       "yices" -> pure (SolverOnline Yices)       "cvc4" -> pure (SolverOnline CVC4)       "cvc5" -> pure (SolverOnline CVC5)       "stp" -> pure (SolverOnline STP)       "bitwuzla" -> pure (SolverOnline Bitwuzla)-      _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, stp, or bitwuzla)" s)+      _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, stp, rme, or bitwuzla)" s)  asManyOfflineSolvers :: String -> Validated [SolverOffline] asManyOfflineSolvers s-  | s == "all"         = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc4,cvc5,stp,bitwuzla"+  | s == "all"         = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc4,cvc5,stp,bitwuzla,rme"   | 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

@@ -0,0 +1,29 @@+{-# LANGUAGE TemplateHaskell #-}++-- | These are placed in their own module to minimize the cost of recompilation+-- due to Template Haskell.+module Crux.GitHash (hash, branch, dirty, unknown) where++import GitHash (GitInfo, giBranch, giDirty, giHash, tGitInfoCwdTry)++gitInfo :: Either String GitInfo+gitInfo = $$tGitInfoCwdTry++hash :: String+hash = case gitInfo of+  Left _ -> unknown+  Right gi -> giHash gi++branch :: String+branch = case gitInfo of+  Left _ -> unknown+  Right gi -> giBranch gi++dirty :: Bool+dirty = case gitInfo of+  Left _ -> False+  Right gi -> giDirty gi++-- | What to report if we are unable to determine git-related information.+unknown :: String+unknown = "UNKNOWN"

@@ -44,6 +44,7 @@ import           Control.Lens ( Getter, view ) import qualified Data.Aeson as JSON import           Data.Aeson.TH ( deriveToJSON )+import qualified Data.List as List import qualified Data.Text as T import           Data.Text.IO as TIO ( hPutStr, hPutStrLn ) import           Data.Version ( Version, showVersion )@@ -59,7 +60,8 @@  import           Crux.Types     ( CruxSimulationResult, ProvedGoals, SayLevel(..), SayWhat(..) )-import           Crux.Version ( version )+import           Crux.Version+    ( commitBranch, commitDirty, commitHash, version ) import           Lang.Crucible.Backend ( ProofGoal(..), ProofObligation ) import           What4.Expr.Builder ( ExprBuilder ) import           What4.LabeledPred ( labeledPred, labeledPredMsg )@@ -129,7 +131,9 @@   | StartedGoal Integer   | TotalPathsExplored Word64   | UnsupportedTimeoutFor String -- ^ name of the backend-  | Version T.Text Version+  | Version+      T.Text -- ^ name of the backend+      Version -- ^ backend-specific version   deriving (Generic)  $(deriveToJSON JSON.defaultOptions ''CruxLogMessage)@@ -220,13 +224,23 @@ cruxLogMessageToSayWhat (Version nm ver) =   cruxOK     ( T.pack-        ( unwords+      ( List.intercalate+        "\n"+        [ unwords             [ "version: " <> version <> ",",               T.unpack nm,-              "version: " <> (showVersion ver)+              "version: " <> showVersion ver             ]-        )+        , "Git commit " <> commitHash+        , "    branch " <> commitBranch <> dirtyLab+        ]+      )     )+  where+    dirtyLab :: String+    dirtyLab+      | commitDirty = " (non-committed files present during build)"+      | otherwise = ""  -- | Main function used to log/output a general text message of some kind say ::

@@ -34,14 +34,25 @@ toDouble :: Rational -> Double toDouble = fromRational --showBVLiteral :: (1 <= w) => NatRepr w -> BV w -> String-showBVLiteral w bv =+showBVLiteralSigned :: (1 <= w) => NatRepr w -> BV w -> String+showBVLiteralSigned w bv =     (if x < 0 then "-0x" else "0x") ++ N.showHex i (if natValue w == 64 then "L" else "")   where   x = BV.asSigned w bv   i = abs x +showBVLiteralUnsigned :: (1 <= w) => NatRepr w -> BV w -> String+showBVLiteralUnsigned w bv =+    "0x" ++ N.showHex i (if natValue w == 64 then "L" else "")+  where+  i = BV.asUnsigned bv++showBVLiteralDecimal :: (1 <= w) => NatRepr w -> BV w -> String+showBVLiteralDecimal w bv =+    show x+  where+  x = BV.asSigned w bv+ showFloatLiteral :: BigFloat -> String showFloatLiteral x    | BF.bfIsNaN x     = "NAN"@@ -61,7 +72,7 @@ valsJS :: BaseTypeRepr ty -> Vals ty -> IO [JS] valsJS ty (Vals xs) =   let showEnt = case ty of-        BaseBVRepr n -> showEnt' (showBVLiteral n) n+        BaseBVRepr n -> showBVEnt n         BaseFloatRepr (FloatingPointPrecisionRepr eb sb)           | Just Refl <- testEquality eb (knownNat @8)           , Just Refl <- testEquality sb (knownNat @24)@@ -85,6 +96,18 @@          , "val"  ~> jsStr (repr (entryValue e))          , "bits" ~> jsStr (show n)          ]++  showBVEnt :: (1 <= w) => NatRepr w -> Entry (BV w) -> IO JS+  showBVEnt n e = do+    l <- fromMaybe jsNull <$> jsLoc (entryLoc e)+    pure $ jsObj+      [ "name"         ~> jsStr (entryName e)+      , "loc"          ~> l+      , "val"          ~> jsStr (showBVLiteralSigned n (entryValue e))+      , "val-unsigned" ~> jsStr (showBVLiteralUnsigned n (entryValue e))+      , "val-decimal"  ~> jsStr (showBVLiteralDecimal n (entryValue e))+      , "bits"         ~> jsStr (show n)+      ]  modelJS :: ModelView -> IO JS modelJS m =

@@ -3,27 +3,51 @@ -- | Utilites for generating JSON module Crux.UI.JS where -import Data.Text(unpack)+import Data.Text(unpack, Text)+import qualified Data.Text as Text+import Numeric import Data.List(intercalate) import Data.Maybe(fromMaybe) import System.Directory( canonicalizePath )  import What4.ProgramLoc +-- | 'jsLoc' takes a program location and renders it as a JavaScript string.+-- This returns @Nothing@ if it is unclear how to render the program location. jsLoc :: ProgramLoc -> IO (Maybe JS) jsLoc x =   case plSourceLoc x of-    SourcePos f l c ->-      do let fstr = unpack f-         fabsolute <--            if | null fstr -> pure ""-               | otherwise -> canonicalizePath fstr-         pure $ Just $ jsObj-           [ "file" ~> jsStr fabsolute-           , "line" ~> jsStr (show l)-           , "col"  ~> jsStr (show c)-           ]+    SourcePos fname l c -> parsePos fname l c+    -- Attempt to parse `OtherPos` in case it is in fact a code span:+    --+    --   * This case is necessary because of the particular shape of source+    --   spans that arise from `mir-json`+    --   (e.g., `test/symb_eval/num/checked_mul.rs:6:5: 6:12:`), which will+    --   always be represented as `OtherPos`.+    --   * While `crux` doesn't have the machinery to represent the entire+    --   source span in its UI framework, we can still achieve partial results+    --   by parsing the first location from the source span+    --   (e.g., `the test/symb_eval/num/checked_mul.rs:6:5:` bit). This does+    --   not show the entire span, but it is still better than nothing.+    OtherPos s+      | fname : line : col : _rest <- Text.split (==':') s+      , (l,[]):_ <- readDec (Text.unpack (Text.strip line))+      , (c,[]):_ <- readDec (Text.unpack (Text.strip col)) ->+        parsePos fname l c     _ -> pure Nothing+    where+    parsePos :: Text -> Int -> Int -> IO (Maybe JS)+    parsePos f l c = do+      let fstr = unpack f+      fabsolute <-+        if null fstr+          then pure ""+          else canonicalizePath fstr+      pure $ Just $ jsObj+        [ "file" ~> jsStr fabsolute+        , "line" ~> jsStr (show l)+        , "col"  ~> jsStr (show c)+        ]  -------------------------------------------------------------------------------- newtype JS = JS { renderJS :: String }

@@ -1,9 +1,95 @@-module Crux.Version where+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TemplateHaskell #-} +module Crux.Version+  ( version+  , commitHash+  , commitBranch+  , commitDirty+  ) where++import qualified Data.Aeson as Aeson+import qualified Data.Aeson.KeyMap as KeyMap+import qualified Data.ByteString as BS+import Data.FileEmbed (embedFileRelative)+import qualified Data.Text as Text import Data.Version (showVersion) import qualified Paths_crux (version) +import qualified Crux.GitHash as GitHash+ version :: String version = showVersion Paths_crux.version +commitHash :: String+commitHash+  | hash /= GitHash.unknown =+      hash+  -- See Note [crux.buildinfo.json]+  | Just buildinfoVal <- Aeson.decodeStrict buildinfo+  , Just (Aeson.String buildinfoHash) <- KeyMap.lookup "hash" buildinfoVal =+      Text.unpack buildinfoHash+  | otherwise =+      GitHash.unknown+ where+  hash = GitHash.hash +commitBranch :: String+commitBranch+  | branch /= GitHash.unknown =+      branch+  -- See Note [crux.buildinfo.json]+  | Just buildinfoVal <- Aeson.decodeStrict buildinfo+  , Just (Aeson.String buildinfoCommit) <- KeyMap.lookup "branch" buildinfoVal =+      Text.unpack buildinfoCommit+  | otherwise =+      GitHash.unknown+ where+  branch = GitHash.branch++commitDirty :: Bool+commitDirty+  | dirty =+      dirty+  -- See Note [crux.buildinfo.json]+  | Just buildinfoVal <- Aeson.decodeStrict buildinfo+  , Just (Aeson.Bool buildinfoDirty) <- KeyMap.lookup "dirty" buildinfoVal =+      buildinfoDirty+  | otherwise =+      False+ where+  dirty = GitHash.dirty++-- Helper, not exported+--+-- See Note [crux.buildinfo.json]+buildinfo :: BS.ByteString+buildinfo = $(embedFileRelative "crux.buildinfo.json")++{-+Note [crux.buildinfo.json]+~~~~~~~~~~~~~~~~~~~~~~~~~~+By default, we determine the git commit hash, branch, and dirty information+using the githash library, which invokes git at compile time to query the+relevant information in the .git subdirectory. This works well for local+developments where the git binary and the .git subdirectory are both readily+available. It does not work so well for building in a Docker image, as we+intentionally do not copy over the .git subdirectory into the image to prevent+spurious cache invalidations caused by the contents of .git changing (which+they do, quite often).++As an alternative to githash, we also employ a convention where a build system+can create a crux.buildinfo.json file locally which contains the necessary+git-related information. The schema for this file is:++  {+    "hash": <string>,+    "branch": <string>,+    "dirty": <bool>+  }++This way, a build system (which has access to git/.git) can write this+information to a file, proceed to build the Docker image (which does not have+access to git/.git), and then have all of the expected information embedded+into the output of --version.+-}