diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/crux.buildinfo.json b/crux.buildinfo.json new file mode 100644 --- /dev/null +++ b/crux.buildinfo.json @@ -0,0 +1,5 @@ +{ + "hash": null, + "branch": null, + "dirty": null +} 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.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 diff --git a/src/Crux.hs b/src/Crux.hs --- a/src/Crux.hs +++ b/src/Crux.hs @@ -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 "" $ 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 <- 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/Config/Solver.hs b/src/Crux/Config/Solver.hs --- a/src/Crux/Config/Solver.hs +++ b/src/Crux/Config/Solver.hs @@ -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 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/GitHash.hs b/src/Crux/GitHash.hs new file mode 100644 --- /dev/null +++ b/src/Crux/GitHash.hs @@ -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" 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,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) diff --git a/src/Crux/Model.hs b/src/Crux/Model.hs --- a/src/Crux/Model.hs +++ b/src/Crux/Model.hs @@ -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) + ) 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 } diff --git a/src/Crux/UI/JS.hs b/src/Crux/UI/JS.hs --- a/src/Crux/UI/JS.hs +++ b/src/Crux/UI/JS.hs @@ -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 } diff --git a/src/Crux/Version.hs b/src/Crux/Version.hs --- a/src/Crux/Version.hs +++ b/src/Crux/Version.hs @@ -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": , + "branch": , + "dirty": + } + +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. +-}