| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Crux
Synopsis
- runSimulator :: Logs msgs => SupportsCruxLogMessage msgs => CruxOptions -> SimulatorCallbacks msgs r -> IO r
- postprocessSimResult :: Logs msgs => Bool -> CruxOptions -> CruxSimulationResult -> IO ExitCode
- loadOptions :: SupportsCruxLogMessage msgs => (Maybe OutputOptions -> OutputConfig msgs) -> Text -> Version -> Config opts -> (Logs msgs => (CruxOptions, opts) -> IO a) -> IO a
- mkOutputConfig :: ToJSON msgs => (Handle, Bool) -> (Handle, Bool) -> (msgs -> SayWhat) -> Maybe OutputOptions -> OutputConfig msgs
- defaultOutputConfig :: ToJSON msgs => (msgs -> SayWhat) -> IO (Maybe OutputOptions -> OutputConfig msgs)
- newtype SimulatorCallbacks msgs r = SimulatorCallbacks {
- getSimulatorCallbacks :: forall sym bak t st fs. (IsSymBackend sym bak, Logs msgs, sym ~ ExprBuilder t st fs) => IO (SimulatorHooks sym bak t r)
- data SimulatorHooks sym bak t r = SimulatorHooks {
- setupHook :: bak -> Maybe (SomeOnlineSolver sym bak) -> IO (RunnableState sym)
- onErrorHook :: bak -> IO (Explainer sym t Void)
- resultHook :: bak -> CruxSimulationResult -> IO r
- data RunnableState sym where
- RunnableStateWithExtensions :: IsSyntaxExtension ext => ExecState (personality sym) sym ext (RegEntry sym UnitType) -> [ExecutionFeature (personality sym) sym ext (RegEntry sym UnitType)] -> RunnableState sym
- pattern RunnableState :: forall sym. () => forall ext personality. IsSyntaxExtension ext => ExecState (personality sym) sym ext (RegEntry sym UnitType) -> RunnableState sym
- type Explainer sym t ann = Maybe (GroundEvalFn t) -> LPred sym SimError -> IO (Doc ann)
- data CruxOptions = CruxOptions {
- inputFiles :: [FilePath]
- outDir :: FilePath
- bldDir :: FilePath
- checkPathSat :: Bool
- profileCrucibleFunctions :: Bool
- profileSolver :: Bool
- branchCoverage :: Bool
- pathStrategy :: PathStrategy
- globalTimeout :: Maybe NominalDiffTime
- goalTimeout :: Maybe DiffTime
- profileOutputInterval :: NominalDiffTime
- loopBound :: Maybe Word64
- recursionBound :: Maybe Word64
- makeCexes :: Bool
- unsatCores :: Bool
- getNAbducts :: Maybe Word64
- solver :: String
- pathSatSolver :: Maybe String
- forceOfflineGoalSolving :: Bool
- pathSatSolverOutput :: Maybe FilePath
- onlineSolverOutput :: Maybe FilePath
- offlineSolverOutput :: Maybe FilePath
- yicesMCSat :: Bool
- floatMode :: String
- proofGoalsFailFast :: Bool
- skipReport :: Bool
- skipSuccessReports :: Bool
- skipIncompleteReports :: Bool
- hashConsing :: Bool
- onlineProblemFeatures :: ProblemFeatures
- outputOptions :: OutputOptions
- data SomeOnlineSolver sym bak where
- SomeOnlineSolver :: (sym ~ ExprBuilder scope st fs, bak ~ OnlineBackend solver scope st fs, IsSymBackend sym bak, OnlineSolver solver) => bak -> SomeOnlineSolver sym bak
- data Crux sym = CruxPersonality
- module Crux.Config
- module Crux.Log
- module Crux.Log
Documentation
runSimulator :: Logs msgs => SupportsCruxLogMessage msgs => CruxOptions -> SimulatorCallbacks msgs r -> IO r Source #
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).
postprocessSimResult :: Logs msgs => Bool -> CruxOptions -> CruxSimulationResult -> IO ExitCode Source #
Given the result of a simulation and proof run, report the overall status, generate user-consumable reports and compute the exit code.
Arguments
| :: SupportsCruxLogMessage msgs | |
| => (Maybe OutputOptions -> OutputConfig msgs) | |
| -> Text | Name |
| -> Version | |
| -> Config opts | |
| -> (Logs msgs => (CruxOptions, opts) -> IO a) | |
| -> IO a |
Load crux generic and the provided options, and provide them to the given continuation.
IMPORTANT: This processes options like help and version, which
just print something and exit, so this function may never call
its continuation.
mkOutputConfig :: ToJSON msgs => (Handle, Bool) -> (Handle, Bool) -> (msgs -> SayWhat) -> Maybe OutputOptions -> OutputConfig msgs Source #
Create an OutputConfig for Crux, based on an indication of whether colored output should be used, the normal and error output handles, and the parsed CruxOptions.
If no CruxOptions are available (i.e. Nothing, as used in the preliminary portions of loadOptions), then a default output stance is applied; the default stance is described along with the individual option below.
The following CruxOptions affect the generated OutputConfig:
- noColorsErr (default stance: False when the error handle supports colors, as reported by System.Console.ANSI.hSupportsANSIColor)
- noColorsOut (default stance: False when the output handle supports colors, as reported by System.Console.ANSI.hSupportsANSIColor)
- printFailures (default stance: True)
- quietMode (default stance: False)
- simVerbose (default stance: False)
defaultOutputConfig :: ToJSON msgs => (msgs -> SayWhat) -> IO (Maybe OutputOptions -> OutputConfig msgs) Source #
newtype SimulatorCallbacks msgs r Source #
Individual crux tools will generally call the runSimulator combinator to
handle the nitty-gritty of setting up and running the simulator. Tools
provide SimulatorCallbacks to hook into the simulation process at three
points:
- Before simulation begins, to set up global variables, register override
functions, construct the initial program entry point, and generally do
any necessary language-specific setup (i.e., to produce a
RunnableState) - When simulation ends with an assertion failure (
Explainer) - When simulation ends, regardless of the outcome, to interpret the results.
All of these callbacks have access to the symbolic backend.
Constructors
| SimulatorCallbacks | |
Fields
| |
data SimulatorHooks sym bak t r Source #
Constructors
| SimulatorHooks | |
Fields
| |
data RunnableState sym where Source #
A crucible ExecState that is ready to be passed into the simulator.
This will usually, but not necessarily, be an InitialState.
Constructors
| RunnableStateWithExtensions :: IsSyntaxExtension ext => ExecState (personality sym) sym ext (RegEntry sym UnitType) -> [ExecutionFeature (personality sym) sym ext (RegEntry sym UnitType)] -> RunnableState sym |
pattern RunnableState :: forall sym. () => forall ext personality. IsSyntaxExtension ext => ExecState (personality sym) sym ext (RegEntry sym UnitType) -> RunnableState sym Source #
type Explainer sym t ann = Maybe (GroundEvalFn t) -> LPred sym SimError -> IO (Doc ann) Source #
A function that can be used to generate a pretty explanation of a simulation error.
data CruxOptions Source #
Common options for Crux-based binaries.
Constructors
| CruxOptions | |
Fields
| |
Instances
data SomeOnlineSolver sym bak where Source #
A GADT to capture the online solver constraints when we need them
Constructors
| SomeOnlineSolver :: (sym ~ ExprBuilder scope st fs, bak ~ OnlineBackend solver scope st fs, IsSymBackend sym bak, OnlineSolver solver) => bak -> SomeOnlineSolver sym bak |
A dummy datatype that can be used for the "personality" type parameter.
Constructors
| CruxPersonality |
module Crux.Config
module Crux.Log
module Crux.Log