diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/crux.cabal b/crux.cabal --- a/crux.cabal +++ b/crux.cabal @@ -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, diff --git a/src/Crux.hs b/src/Crux.hs --- a/src/Crux.hs +++ b/src/Crux.hs @@ -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 "" $ 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 <- diff --git a/src/Crux/Config.hs b/src/Crux/Config.hs --- a/src/Crux/Config.hs +++ b/src/Crux/Config.hs @@ -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 diff --git a/src/Crux/Config/Common.hs b/src/Crux/Config/Common.hs --- a/src/Crux/Config/Common.hs +++ b/src/Crux/Config/Common.hs @@ -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," diff --git a/src/Crux/Config/Load.hs b/src/Crux/Config/Load.hs --- a/src/Crux/Config/Load.hs +++ b/src/Crux/Config/Load.hs @@ -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) diff --git a/src/Crux/FormatOut.hs b/src/Crux/FormatOut.hs --- a/src/Crux/FormatOut.hs +++ b/src/Crux/FormatOut.hs @@ -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))] diff --git a/src/Crux/Goal.hs b/src/Crux/Goal.hs --- a/src/Crux/Goal.hs +++ b/src/Crux/Goal.hs @@ -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) diff --git a/src/Crux/Log.hs b/src/Crux/Log.hs --- a/src/Crux/Log.hs +++ b/src/Crux/Log.hs @@ -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) diff --git a/src/Crux/Overrides.hs b/src/Crux/Overrides.hs --- a/src/Crux/Overrides.hs +++ b/src/Crux/Overrides.hs @@ -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 }