crux 0.9 → 0.10
raw patch · 10 files changed
+143/−66 lines, 10 filesdep +microlensdep −generic-lensdep −lensdep ~parameterized-utils
Dependencies added: microlens
Dependencies removed: generic-lens, lens
Dependency ranges changed: parameterized-utils
Files
- CHANGELOG.md +14/−0
- crux.cabal +3/−4
- src/Crux.hs +28/−25
- src/Crux/Config.hs +3/−2
- src/Crux/Config/Common.hs +26/−14
- src/Crux/Config/Load.hs +15/−12
- src/Crux/FormatOut.hs +7/−2
- src/Crux/Goal.hs +2/−1
- src/Crux/Log.hs +5/−4
- src/Crux/Overrides.hs +40/−2
CHANGELOG.md view
@@ -1,3 +1,17 @@+# 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
crux.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: crux-Version: 0.9+Version: 0.10 Copyright: (c) Galois, Inc. 2018-2022 Author: sweirich@galois.com Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com@@ -42,12 +42,11 @@ directory, file-embed ^>= 0.0.16, filepath,- generic-lens, githash ^>= 0.1.7,- lens, 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,
src/Crux.hs view
@@ -33,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@@ -47,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@@ -54,7 +53,7 @@ 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 Data.Parameterized.Nonce (newIONonceGenerator, NonceGenerator)@@ -134,12 +133,12 @@ newtype SimulatorCallbacks msgs st r = SimulatorCallbacks { getSimulatorCallbacks ::- forall sym bak t 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) } @@ -201,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)@@ -290,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@@ -365,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@@ -389,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 =>@@ -401,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@@ -632,14 +634,14 @@ case CCS.parseSolverConfig cruxOpts of Right (CCS.SingleOnlineSolver onSolver) ->- withSelectedOnlineBackend cruxOpts nonceGen onSolver Nothing userState $ \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 userState $ \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@@ -650,7 +652,7 @@ -- 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 userState cruxOpts offSolvers $ \floatRepr -> do@@ -662,18 +664,18 @@ -- 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 userState $ \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) @@ -688,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 st r ->+ WE.FloatModeRepr fm -> bak -> [GenericExecutionFeature sym] -> ProfData sym ->@@ -703,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@@ -757,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/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/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,7 +41,6 @@ ) 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@@ -50,6 +49,8 @@ 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 )@@ -302,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/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 }