packages feed

crux 0.7.2 → 0.10

raw patch · 16 files changed

Files

CHANGELOG.md view
@@ -1,3 +1,29 @@+# 0.10 -- 2026-09-10++- Add support for GHC 9.12 (at 9.12.2) and bump from 9.10.1 to 9.10.3.++- **Breaking:** Drop the `Generic` instances from `ColorOptions`, `CruxOptions`,+  `EarlyConfig`, and `OutputOptions`.+- The following `Lens'` functions are now exported: `outputOptionsL`,+  `colorOptionsL`, `simVerboseL`, `printFailuresL`, `quietModeL` (from+  `Crux.Config.Common`), and `colorOptionsL`, `noColorsErrL`, `noColorsOutL`+  (from `Crux.Config.Load`).+- Add a `FloatModeRepr` argument to `SimulatorCallbacks`.+- Add `baseFreshFloatOverride` and `baseFreshFloatOverride'` to+  `Crux.Overrides`.++# 0.9 -- 2026-01-29++# 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.
+ crux.buildinfo.json view
@@ -0,0 +1,5 @@+{+  "hash": null,+  "branch": null,+  "dirty": null+}
crux.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crux-Version:       0.7.2+Version:       0.10 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,12 +40,13 @@     crucible-debug,     crucible-syntax,     directory,+    file-embed ^>= 0.0.16,     filepath,-    generic-lens,-    lens,+    githash ^>= 0.1.7,     libBF >= 0.6 && < 0.7,     lumberjack >= 1.0 && < 1.1,-    parameterized-utils >= 1.0 && < 2.2,+    microlens,+    parameterized-utils >= 2.3 && < 2.4,     prettyprinter >= 1.7.0,     split >= 0.2,     terminal-size,@@ -60,7 +62,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 +89,7 @@     Crux.Version    other-modules:+   Crux.GitHash,    Crux.UI.Jquery,    Crux.UI.IndexHtml    Paths_crux
src/Crux.hs view
@@ -12,6 +12,9 @@  module Crux   ( runSimulator+  , runSimulatorWithUserState+  , InitUserState(..)+  , noInitUserState   , postprocessSimResult   , loadOptions   , mkOutputConfig@@ -30,13 +33,11 @@  import qualified Control.Applicative as Applicative import qualified Control.Exception as Ex-import           Control.Lens import           Control.Monad ( unless, void, when ) import qualified Data.Aeson as JSON import           Data.Foldable import           Data.Functor.Contravariant ( (>$<) ) import           Data.Functor.Contravariant.Divisible ( divide )-import           Data.Generics.Product.Fields (field) import           Data.IORef import           Data.Maybe ( fromMaybe ) import qualified Data.Sequence as Seq@@ -44,6 +45,7 @@ import qualified Data.Text as T import           Data.Version (Version) import           Data.Void (Void)+import           Lens.Micro (set) import qualified Lumberjack as LJ import           Prettyprinter import qualified System.Console.ANSI as AC@@ -51,10 +53,9 @@ import           System.Directory (createDirectoryIfMissing) import           System.Exit (exitSuccess, ExitCode(..), exitFailure, exitWith) import           System.FilePath ((</>))-import           System.IO ( Handle, hPutStr, stdout, stderr )+import           System.IO ( Handle, hPutStrLn, 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 +86,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 +100,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,15 +130,15 @@ --   * 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 fm.           ( IsSymBackend sym bak           , Logs msgs-          , sym ~ WE.ExprBuilder t st fs+          , sym ~ WE.ExprBuilder t st (WE.Flags fm)           ) =>-          IO (SimulatorHooks sym bak t r)+          WE.FloatModeRepr fm -> IO (SimulatorHooks sym bak t r)     }  @@ -191,7 +200,7 @@              showVersion nm ver              exitSuccess        Cfg.Options (cruxWithoutColorOptions, os) files ->-          do let crux = set (field @"outputOptions" . field @"colorOptions") copts cruxWithoutColorOptions+          do let crux = set (outputOptionsL . colorOptionsL) copts cruxWithoutColorOptions              let ?outputConfig = mkOutCfg (Just (outputOptions crux))              crux' <- postprocessOptions crux { inputFiles = files ++ inputFiles crux }              cont (crux', os)@@ -280,7 +289,7 @@                               [ AC.SetConsoleIntensity AC.BoldIntensity                               , AC.SetColor AC.Foreground AC.Vivid AC.Red]                      seeCalm = AC.hSetSGR errHandle [AC.Reset]-                     dispExc = hPutStr errHandle . Ex.displayException+                     dispExc = hPutStrLn errHandle . Ex.displayException                  in if errShouldColor                     then LJ.LogAction $ \e -> Ex.bracket_ seeRed seeCalm $ dispExc e                     else LJ.LogAction $ dispExc@@ -355,8 +364,10 @@     ( OnlineSolver solver     , IsInterpretedFloatExprBuilder (WE.ExprBuilder scope st (WE.Flags fm))     ) =>-    (OnlineBackend solver scope st (WE.Flags fm) -> IO a)) ->-    IO a+    WE.FloatModeRepr fm ->+    OnlineBackend solver scope st (WE.Flags fm) ->+    IO a) ->+  IO a withSelectedOnlineBackend cruxOpts nonceGen selectedSolver maybeExplicitFloatMode initSt k =   case fromMaybe (floatMode cruxOpts) maybeExplicitFloatMode of     "real" -> withOnlineBackendFM WE.FloatRealRepr@@ -379,7 +390,7 @@       IO a     withOnlineBackendFM fm =       do sym <- WE.newExprBuilder fm initSt nonceGen-         withSelectedOnlineBackend' cruxOpts selectedSolver sym k+         withSelectedOnlineBackend' cruxOpts selectedSolver sym $ k fm  withSelectedOnlineBackend' ::   Logs msgs =>@@ -391,8 +402,9 @@   WE.ExprBuilder scope st fs ->   (forall solver.     OnlineSolver solver =>-    (OnlineBackend solver scope st fs -> IO a)) ->-    IO a+    OnlineBackend solver scope st fs ->+    IO a) ->+  IO a withSelectedOnlineBackend' cruxOpts selectedSolver sym k =   let unsatCoreFeat | unsatCores cruxOpts                     , not (yicesMCSat cruxOpts) = ProduceUnsatCores@@ -562,6 +574,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 +589,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 +609,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 $ \fm 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)+        doSimWithResults cruxOpts simCallback fm 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 $ \fm bak -> do         let monline = Just (SomeOnlineSolver bak)         setupSolver cruxOpts (pathSatSolverOutput cruxOpts) (backendGetSym bak)         (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts bak monline@@ -613,30 +652,30 @@           -- been a different solver)           unless (CCS.sameSolver onSolver offSolver) $             extendConfig (WS.solver_adapter_config_options adapter) (getConfiguration (backendGetSym bak))-          doSimWithResults cruxOpts simCallback bak execFeatures profInfo monline (proveGoalsOffline [adapter])+          doSimWithResults cruxOpts simCallback fm 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           -- with the options taken from the solver adapter (e.g., solver path)           extendConfig (WS.solver_adapter_config_options =<< adapters) (getConfiguration sym)           (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts bak Nothing-          doSimWithResults cruxOpts simCallback bak execFeatures profInfo Nothing (proveGoalsOffline adapters)+          doSimWithResults cruxOpts simCallback floatRepr bak execFeatures profInfo Nothing (proveGoalsOffline adapters)      Right (CCS.OnlineSolverWithSeparateOnlineGoals pathSolver goalSolver) ->       -- 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 $ \fm pathSatBak -> do         let sym = backendGetSym pathSatBak         setupSolver cruxOpts (pathSatSolverOutput cruxOpts) sym         (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts pathSatBak (Just (SomeOnlineSolver pathSatBak))         withSelectedOnlineBackend' cruxOpts goalSolver sym $ \goalBak -> do-          doSimWithResults cruxOpts simCallback pathSatBak execFeatures profInfo (Just (SomeOnlineSolver pathSatBak)) (proveGoalsOnline goalBak)+          doSimWithResults cruxOpts simCallback fm pathSatBak execFeatures profInfo (Just (SomeOnlineSolver pathSatBak)) (proveGoalsOnline goalBak)      Left rsns -> fail ("Invalid solver configuration:\n" ++ unlines rsns) @@ -651,13 +690,14 @@ -- The main work in this function is setting up appropriate solver frames and -- traversing the goals tree, as well as handling some reporting. doSimWithResults ::-  forall sym bak r t st fs msgs.-  sym ~ WE.ExprBuilder t st fs =>+  forall sym bak r t st fm msgs.+  sym ~ WE.ExprBuilder t st (WE.Flags fm) =>   IsSymBackend sym bak =>   Logs msgs =>   SupportsCruxLogMessage msgs =>   CruxOptions ->-  SimulatorCallbacks msgs r ->+  SimulatorCallbacks msgs st r ->+  WE.FloatModeRepr fm ->   bak ->   [GenericExecutionFeature sym] ->   ProfData sym ->@@ -666,14 +706,14 @@     {- ^ The function to use to prove goals; this is intended to be          one of 'proveGoalsOffline' or 'proveGoalsOnline' -} ->   IO r-doSimWithResults cruxOpts simCallback bak execFeatures profInfo monline goalProver = do+doSimWithResults cruxOpts simCallback fm bak execFeatures profInfo monline goalProver = do   compRef <- newIORef ProgramComplete   glsRef <- newIORef Seq.empty    frm <- pushAssumptionFrame bak    SimulatorHooks setup onError interpretResult <--    getSimulatorCallbacks simCallback+    getSimulatorCallbacks simCallback fm   inFrame profInfo "<Crux>" $ do     -- perform tool-specific setup     RunnableStateWithExtensions initSt exts <- setup bak monline@@ -690,17 +730,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@@ -730,7 +760,7 @@    -> IORef (Seq.Seq (ProcessedGoals, ProvedGoals))    -> FrameIdentifier    -> (Maybe (WE.GroundEvalFn t) -> LabeledPred (WE.Expr t BaseBoolType) SimError -> IO (Doc Void))-   -> Result personality (WE.ExprBuilder t st fs)+   -> Result personality (WE.ExprBuilder t st (WE.Flags fm))    -> IO Bool  resultCont compRef glsRef frm explainFailure (Result res) =    do timedOut <-
src/Crux/Config.hs view
@@ -18,9 +18,10 @@   , parsePosNum   ) where -import Control.Lens (Lens', set, view)-import Data.Text (Text) import Data.Maybe (fromMaybe)+import Data.Text (Text)+import Lens.Micro (Lens', set)+import Lens.Micro.Extras (view) import Text.Read(readMaybe)  import SimpleGetOpt
src/Crux/Config/Common.hs view
@@ -1,10 +1,7 @@ {-# LANGUAGE ApplicativeDo #-}-{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE DataKinds #-}  module Crux.Config.Common (   OutputOptions(..),@@ -13,17 +10,20 @@   cruxOptions,   defaultOutputOptions,   postprocessOptions,+  outputOptionsL,+  colorOptionsL,+  simVerboseL,+  printFailuresL,+  quietModeL, ) where -import Control.Lens (set)+import Data.Char(toLower) import Data.Functor.Alt-import Data.Generics.Product.Fields (field)-import Data.Time(DiffTime, NominalDiffTime) import Data.Maybe(fromMaybe)-import Data.Char(toLower)-import Data.Word (Word64) import Data.Text (pack)-import GHC.Generics (Generic)+import Data.Time(DiffTime, NominalDiffTime)+import Data.Word (Word64)+import Lens.Micro (Lens', lens, set) import System.Directory ( createDirectoryIfMissing )  import Crux.Config@@ -101,9 +101,20 @@     -- ^ If true, produce minimal output    }-  deriving (Generic) +colorOptionsL :: Lens' OutputOptions ColorOptions+colorOptionsL = lens colorOptions (\o v -> o { colorOptions = v }) +simVerboseL :: Lens' OutputOptions Int+simVerboseL = lens simVerbose (\o v -> o { simVerbose = v })++printFailuresL :: Lens' OutputOptions Bool+printFailuresL = lens printFailures (\o v -> o { printFailures = v })++quietModeL :: Lens' OutputOptions Bool+quietModeL = lens quietMode (\o v -> o { quietMode = v })++ defaultOutputOptions :: ColorOptions -> OutputOptions defaultOutputOptions copts = OutputOptions   { colorOptions = copts@@ -209,8 +220,9 @@     -- ^ Drop into the Crucible debugger before simulation begins    }-  deriving (Generic) +outputOptionsL :: Lens' CruxOptions OutputOptions+outputOptionsL = lens outputOptions (\c v -> c { outputOptions = v })   cruxOptions :: Config CruxOptions@@ -393,7 +405,7 @@        [ Option "d" ["sim-verbose"]         "Set simulator verbosity level."-        $ ReqArg "NUM" $ parsePosNum "NUM" $ \v -> set (field @"outputOptions" . field @"simVerbose") v+        $ ReqArg "NUM" $ parsePosNum "NUM" $ \v -> set (outputOptionsL . simVerboseL) v        , Option [] ["path-sat"]         "Enable path satisfiability checking"@@ -517,7 +529,7 @@        , Option [] ["skip-print-failures"]         "Skip printing messages related to failed verification goals"-        $ NoArg $ Right . set (field @"outputOptions" . field @"printFailures") False+        $ NoArg $ Right . set (outputOptionsL . printFailuresL) False        , Option [] ["fail-fast"]         "Stop attempting to prove goals as soon as one of them is disproved"@@ -525,7 +537,7 @@        , Option "q" ["quiet"]         "Quiet mode; produce minimal output"-        $ NoArg $ Right . set (field @"outputOptions" . field @"quietMode") True+        $ NoArg $ Right . set (outputOptionsL . quietModeL) True        , Option "f" ["floating-point"]         ("Select floating point representation,"
src/Crux/Config/Load.hs view
@@ -1,16 +1,12 @@-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE DataKinds #-}-{-# Language DeriveGeneric, MultiWayIf, OverloadedStrings #-}+{-# Language MultiWayIf, OverloadedStrings #-} -- | This module deals with loading configurations. module Crux.Config.Load where  -import Control.Lens (set)-import Control.Monad(foldM, (<=<)) import Control.Exception(Exception(..),catch,catches,throwIO, Handler(..))-import Data.Generics.Product.Fields (field, setField)+import Control.Monad(foldM, (<=<))+import Lens.Micro (Lens', lens, set) import Data.Text (Text)-import GHC.Generics (Generic)  import System.Environment @@ -32,7 +28,6 @@   { noColorsErr :: Bool   , noColorsOut :: Bool   }-  deriving (Generic)  defaultColorOptions :: ColorOptions defaultColorOptions = allColors@@ -49,7 +44,13 @@   , noColorsOut = True   } +noColorsErrL :: Lens' ColorOptions Bool+noColorsErrL = lens noColorsErr (\c v -> c { noColorsErr = v }) +noColorsOutL :: Lens' ColorOptions Bool+noColorsOutL = lens noColorsOut (\c v -> c { noColorsOut = v })++ -- | Command line options processed before loading the configuration file. data EarlyConfig opts = EarlyConfig   { showHelp      :: Bool -- ^ Describe options & quit@@ -61,9 +62,11 @@   , options       :: OptSetter opts   , files         :: [FilePath]   }-  deriving (Generic) +colorOptionsL :: Lens' (EarlyConfig opts) ColorOptions+colorOptionsL = lens colorOptions (\e v -> e { colorOptions = v }) + commandLineOptions :: Config opts -> OptSpec (EarlyConfig opts) commandLineOptions cfg = OptSpec   { progDefaults = EarlyConfig@@ -90,15 +93,15 @@        , Option [] ["no-colors-err"]         "Suppress color codes in the errors"-        $ NoArg $ Right . set (field @"colorOptions" . field @"noColorsErr") True+        $ NoArg $ Right . set (colorOptionsL . noColorsErrL) True        , Option [] ["no-colors-out"]         "Suppress color codes in the output"-        $ NoArg $ Right . set (field @"colorOptions" . field @"noColorsOut") True+        $ NoArg $ Right . set (colorOptionsL . noColorsOutL) True        , Option [] ["no-colors"]         "Suppress color codes in both the output and the errors"-        $ NoArg $ Right . setField @"colorOptions" noColors+        $ NoArg $ Right . set colorOptionsL noColors        ] ++ map (mapOptDescr delayOpt) (cfgCmdLineFlag cfg)
src/Crux/Config/Solver.hs view
@@ -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
src/Crux/FormatOut.hs view
@@ -29,6 +29,7 @@ import qualified Lang.Crucible.Simulator.SimError as CSE  import           Crux.Types+import Lang.Crucible.Simulator.SimError (ppProgramStack, simErrorContext)  sayWhatResultStatus :: CruxSimulationResult -> SayWhat sayWhatResultStatus (CruxSimulationResult cmpl gls) =@@ -76,8 +77,12 @@                -- n.b. prefer the prepared pretty explanation, but                -- if not available, use the NotProved information.                -- Don't show both: they tend to be duplications.-               , if null (show ex) then PP.viaShow err else ex-               ] -- if `showVars` is set, print the sequence of symbolic+               ] ++ case (show ex, simErrorContext err) of+                      ([], _) ->  [  PP.viaShow err ] +                      (_, Nothing) -> [ex]+                      (_, Just ctx) ->+                        [ex, "Context:", PP.indent 2 (ppProgramStack ctx)]+                 -- if `showVars` is set, print the sequence of symbolic                  -- variable events that led to this failure                  ++ if showVars then                       ["Symbolic variables:", PP.indent 2 (PP.vcat (ppVars evs))]
+ src/Crux/GitHash.hs view
@@ -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"
src/Crux/Goal.hs view
@@ -13,7 +13,8 @@  import Control.Concurrent.Async (async, asyncThreadId, waitAnyCatch) import Control.Exception (throwTo, SomeException, displayException)-import Control.Lens ((^.), view)+import Lens.Micro ((^.))+import Lens.Micro.Extras (view)  import Control.Monad (forM, forM_, unless, when) import Data.Either (partitionEithers)
src/Crux/Log.hs view
@@ -41,14 +41,16 @@   ) where  import           Control.Exception ( SomeException, bracket_,  )-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 ) import           Data.Word ( Word64 ) import           GHC.Generics ( Generic )+import           Lens.Micro (SimpleGetter)+import           Lens.Micro.Extras (view) import qualified Lumberjack as LJ import           Prettyprinter ( SimpleDocStream ) import           Prettyprinter.Render.Text ( renderStrict )@@ -59,7 +61,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 +132,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 +225,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 ::@@ -288,14 +303,14 @@ -- directly instead of using the logging/output functions above.  It -- can either get the _outputHandle directly or it can use the -- output/outputLn functions below.-outputHandle :: Getter (OutputConfig msgs) Handle+outputHandle :: SimpleGetter (OutputConfig msgs) Handle outputHandle f o = o <$ f (_outputHandle o)  -- | Lens to allow client code to determine if running in quiet mode.-quiet :: Getter (OutputConfig msgs) Bool+quiet :: SimpleGetter (OutputConfig msgs) Bool quiet f o = o <$ f (_quiet o) -logMsg :: Getter (OutputConfig msgs) (LJ.LogAction IO msgs)+logMsg :: SimpleGetter (OutputConfig msgs) (LJ.LogAction IO msgs) logMsg f o = o <$ f (_logMsg o)
src/Crux/Model.hs view
@@ -1,6 +1,7 @@ -- | This file is almost exactly the same as crucible-c/src/Model.hs  {-# Language DataKinds #-}+{-# Language OverloadedStrings #-} {-# Language PolyKinds #-} {-# Language Rank2Types #-} {-# Language TypeFamilies #-}@@ -19,6 +20,8 @@ import qualified Numeric as N import           LibBF (BigFloat) import qualified LibBF as BF+import qualified Prettyprinter as PP+import           Prettyprinter (Doc)  import           Lang.Crucible.Types @@ -34,14 +37,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"@@ -58,10 +72,14 @@                                                -- NB, 53 bits of precision for double    | otherwise        = BF.bfToString 16 (BF.showFree (Just 53) <> BF.addPrefix) x +showBoolLiteral :: Bool -> String+showBoolLiteral b = if b then "true" else "false"+ valsJS :: BaseTypeRepr ty -> Vals ty -> IO [JS] valsJS ty (Vals xs) =   let showEnt = case ty of-        BaseBVRepr n -> showEnt' (showBVLiteral n) n+        -- NOTE: Keep these cases in sync with those in 'prettyVals'.+        BaseBVRepr n -> showBVEnt n         BaseFloatRepr (FloatingPointPrecisionRepr eb sb)           | Just Refl <- testEquality eb (knownNat @8)           , Just Refl <- testEquality sb (knownNat @24)@@ -71,6 +89,7 @@           , Just Refl <- testEquality sb (knownNat @53)           -> showEnt' showDoubleLiteral (64 :: Int)         BaseRealRepr -> showEnt' (show . toDouble) (knownNat @64)+        BaseBoolRepr -> showBoolEnt         _ -> error ("Type not implemented: " ++ show ty)    in mapM showEnt xs@@ -86,6 +105,94 @@          , "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)+      ]++  showBoolEnt :: Entry Bool -> IO JS+  showBoolEnt e = do+    do l <- fromMaybe jsNull <$> jsLoc (entryLoc e)+       pure $ jsObj+         [ "name" ~> jsStr (entryName e)+         , "loc"  ~> l+         , "val"  ~> jsStr (showBoolLiteral (entryValue e))+         ]+ modelJS :: ModelView -> IO JS modelJS m =   jsList . concat <$> sequence (MapF.foldrWithKey (\k v xs -> valsJS k v : xs) [] (modelVals m))++-- Pretty-print all entries in a model for a given base type.+prettyVals :: BaseTypeRepr ty -> Vals ty -> [Doc ann]+prettyVals ty (Vals xs) =+  let ppEnt = case ty of+        -- NOTE: Keep these cases in sync with those in 'valsJS'.+        BaseBVRepr n -> prettyBVEnt n++        BaseFloatRepr (FloatingPointPrecisionRepr eb sb)+          | Just Refl <- testEquality eb (knownNat @8)+          , Just Refl <- testEquality sb (knownNat @24)+          -> prettyEnt' showFloatLiteral++        BaseFloatRepr (FloatingPointPrecisionRepr eb sb)+          | Just Refl <- testEquality eb (knownNat @11)+          , Just Refl <- testEquality sb (knownNat @53)+          -> prettyEnt' showDoubleLiteral++        BaseRealRepr ->+          -- same semantics as valsJS: print reals via toDouble+          prettyEnt' (show . toDouble)++        BaseBoolRepr ->+          prettyEnt' showBoolLiteral++        _ ->+          error ("Type not implemented: " ++ show ty)+  in+    map ppEnt xs++-- Generic entry printer for "simple" values.+prettyEnt' :: (a -> String) -> Entry a -> Doc ann+prettyEnt' repr e =+  PP.hsep+    [ PP.pretty (entryName e)+    , "="+    , PP.pretty (repr (entryValue e))+    ]++-- Bitvector entries: signed, unsigned, decimal on a single line.+prettyBVEnt :: (1 <= w) => NatRepr w -> Entry (BV w) -> Doc ann+prettyBVEnt n e =+  let v   = entryValue e+      sg  = showBVLiteralSigned   n v+      un  = showBVLiteralUnsigned n v+      dec = showBVLiteralDecimal  n v+  in+    PP.hsep+      [ PP.pretty (entryName e)+      , "="+      , PP.pretty sg+      , "(signed),"+      , PP.pretty un+      , "(unsigned),"+      , PP.pretty dec+      , "(decimal)"+      ]++-- Human-readable model as a Prettyprinter 'Doc'.+prettyModel :: ModelView -> Doc ann+prettyModel m =+  PP.vsep+    (MapF.foldrWithKey+       (\ty vals docs -> prettyVals ty vals ++ docs)+       []+       (modelVals m)+    )
src/Crux/Overrides.hs view
@@ -8,6 +8,8 @@   , mkFreshFloat   , baseFreshOverride   , baseFreshOverride'+  , baseFreshFloatOverride+  , baseFreshFloatOverride'   ) where  import qualified Data.Parameterized.Context as Ctx@@ -56,7 +58,7 @@  -- | Build an override that takes a string and returns a fresh constant with -- that string as its name.-baseFreshOverride :: +baseFreshOverride ::   C.IsSymInterface sym =>   W4.BaseTypeRepr bty ->   -- | The language's string type (e.g., @LLVMPointerType@ for LLVM)@@ -76,7 +78,7 @@ -- | Build an override that takes no arguments and returns a fresh -- constant that uses the given name. Generally, frontends should prefer -- 'baseFreshOverride', to allow users to specify variable names.-baseFreshOverride' :: +baseFreshOverride' ::   C.IsSymInterface sym =>   -- | Variable name   W4.SolverSymbol ->@@ -87,4 +89,40 @@   { C.typedOverrideHandler = \Ctx.Empty -> mkFresh nm bty   , C.typedOverrideArgs = Ctx.Empty   , C.typedOverrideRet = C.baseToType bty+  }++-- | Build an override that takes a string and returns a fresh floating-point+-- constant with that string as its name.+baseFreshFloatOverride ::+  C.IsSymInterface sym =>+  C.FloatInfoRepr fi ->+  -- | The language's string type (e.g., @LLVMPointerType@ for LLVM)+  C.TypeRepr stringTy ->+  -- | Get the variable name as a concrete string from the override arguments+  (C.RegValue' sym stringTy -> OverM p sym ext W4.SolverSymbol) ->+  C.TypedOverride (p sym) sym ext (C.EmptyCtx C.::> stringTy) (C.FloatType fi)+baseFreshFloatOverride fi sty getStr =+  C.TypedOverride+  { C.typedOverrideHandler = \(Ctx.Empty Ctx.:> strVal) -> do+      str <- getStr strVal+      mkFreshFloat str fi+  , C.typedOverrideArgs = Ctx.Empty Ctx.:> sty+  , C.typedOverrideRet = C.FloatRepr fi+  }++-- | Build an override that takes no arguments and returns a fresh+-- floating-point constant that uses the given name. Generally, frontends+-- should prefer 'baseFreshFloatOverride', to allow users to specify variable+-- names.+baseFreshFloatOverride' ::+  C.IsSymInterface sym =>+  -- | Variable name+  W4.SolverSymbol ->+  C.FloatInfoRepr fi ->+  C.TypedOverride (p sym) sym ext C.EmptyCtx (C.FloatType fi)+baseFreshFloatOverride' nm fi =+  C.TypedOverride+  { C.typedOverrideHandler = \Ctx.Empty -> mkFreshFloat nm fi+  , C.typedOverrideArgs = Ctx.Empty+  , C.typedOverrideRet = C.FloatRepr fi   }
src/Crux/UI/JS.hs view
@@ -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 }
src/Crux/Version.hs view
@@ -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.+-}