Crux.Log

Output Configuration

type Logs msgs = ?outputConfig :: OutputConfig msgs

The Logs constraint should be applied for any function that will use the main logging functions: says, logException, logSimResult, or logGoal.

data OutputConfig msgs

Global options for Crux's main. These are not CruxOptions because they are expected to be set directly by main, rather than by a user's command-line options. They exist primarily to improve the testability of the code.

The Crux mkOutputConfig is recommended as a helper function for creating this object, although it can be initialized directly if needed.

Constructors

OutputConfig

Fields

• _outputHandle :: Handle
• _quiet :: Bool
• _logMsg :: LogAction IO msgs
• _logExc :: LogAction IO SomeException
• _logSimResult :: Bool -> LogAction IO CruxSimulationResult

  True to show individual goals, false for summary only

• _logGoal :: LogAction IO ProvedGoals

outputHandle :: Getter (OutputConfig msgs) Handle

Some client code will want to output to the main output stream 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.

quiet :: Getter (OutputConfig msgs) Bool

Lens to allow client code to determine if running in quiet mode.

Standard output API functions

data CruxLogMessage

All messages that Crux wants to output should be listed here.

Messages ought to be serializable to JSON so that they have a somewhat portable machine-readable representation. Some tools may rely on the serialization format, so be sure to check with consumers before changing the ToJSON instance.

Other crux-based tools are encouraged to create their own:

• log message datatype 'ToolLogMessage', similar to CruxLogMessage below,
• constraint synonym 'SupportsToolLogMessage' similar to SupportsCruxLogMessage below,
• constraint dispatcher 'withToolLogMessage' similar to withCruxLogMessage below,
• logger method 'sayTool' similar to sayCrux below,
• default log message converter 'ToolLogMessageToSayWhat' similar to cruxLogMessageToSayWhat.

The default log message converter can be used to decide how messages are displayed to the standard output for a human consumer. Automated tools may prefer to filter and encode log messages in some machine-readable format and exchange it over a separate channel.

Constructors

AttemptingProvingVCs

Checking [FilePath]

DisablingBranchCoverageRequiresPathSatisfiability

DisablingProfilingIncompatibleWithPathSplitting

EndedGoal Integer

FoundCounterExample

Help LogDoc

PathsUnexplored Int

ProofObligations [LogProofObligation]

SimulationComplete

SimulationTimedOut

SkippingUnsatCoresBecauseMCSatEnabled

StartedGoal Integer

TotalPathsExplored Word64

UnsupportedTimeoutFor String

name of the backend

Version Text Version

Instances

ToJSON CruxLogMessage

Defined in Crux.Log

Methods

toJSON :: CruxLogMessage -> Value

toEncoding :: CruxLogMessage -> Encoding

toJSONList :: [CruxLogMessage] -> Value

toEncodingList :: [CruxLogMessage] -> Encoding

omitField :: CruxLogMessage -> Bool

Generic CruxLogMessage

Defined in Crux.Log

Associated Types

type Rep CruxLogMessage :: Type -> Type

Methods

from :: CruxLogMessage -> Rep CruxLogMessage x

to :: Rep CruxLogMessage x -> CruxLogMessage

type Rep CruxLogMessage

Defined in Crux.Log

type Rep CruxLogMessage = D1 ('MetaData "CruxLogMessage" "Crux.Log" "crux-0.7-DD4jascIe8aJ5p2f7vnjLq" 'False) ((((C1 ('MetaCons "AttemptingProvingVCs" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Checking" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]))) :+: (C1 ('MetaCons "DisablingBranchCoverageRequiresPathSatisfiability" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DisablingProfilingIncompatibleWithPathSplitting" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "EndedGoal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: C1 ('MetaCons "FoundCounterExample" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Help" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LogDoc)) :+: C1 ('MetaCons "PathsUnexplored" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))) :+: (((C1 ('MetaCons "ProofObligations" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LogProofObligation])) :+: C1 ('MetaCons "SimulationComplete" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SimulationTimedOut" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SkippingUnsatCoresBecauseMCSatEnabled" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "StartedGoal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: C1 ('MetaCons "TotalPathsExplored" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word64))) :+: (C1 ('MetaCons "UnsupportedTimeoutFor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "Version" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Version))))))

newtype LogDoc

Constructors

LogDoc (SimpleDocStream ())

Instances

ToJSON LogDoc

Defined in Crux.Log

Methods

toJSON :: LogDoc -> Value

toEncoding :: LogDoc -> Encoding

toJSONList :: [LogDoc] -> Value

toEncodingList :: [LogDoc] -> Encoding

omitField :: LogDoc -> Bool

data LogProofObligation

A version of ProofObligation that supports a ToJSON instance.

Constructors

forall t st fs. LogProofObligation (ProofObligation (ExprBuilder t st fs))

Instances

ToJSON LogProofObligation

Defined in Crux.Log

Methods

toJSON :: LogProofObligation -> Value

toEncoding :: LogProofObligation -> Encoding

toJSONList :: [LogProofObligation] -> Value

toEncodingList :: [LogProofObligation] -> Encoding

omitField :: LogProofObligation -> Bool

data SayWhat

Specify some general text that should be presented (to the user).

Constructors

SayWhat SayLevel Text Text

fields are: Level From Message

SayMore SayWhat SayWhat

SayNothing

data SayLevel

Specify the verbosity/severity level of a message. These are in ordinal order for possible filtering, and higher levels may be sent to a different location (e.g. stderr v.s. stdout).

Constructors

Noisily

Simply

OK

Warn

Fail

Instances

Eq SayLevel

Defined in Crux.Types

Methods

(==) :: SayLevel -> SayLevel -> Bool

(/=) :: SayLevel -> SayLevel -> Bool

Ord SayLevel

Defined in Crux.Types

Methods

compare :: SayLevel -> SayLevel -> Ordering

(<) :: SayLevel -> SayLevel -> Bool

(<=) :: SayLevel -> SayLevel -> Bool

(>) :: SayLevel -> SayLevel -> Bool

(>=) :: SayLevel -> SayLevel -> Bool

max :: SayLevel -> SayLevel -> SayLevel

min :: SayLevel -> SayLevel -> SayLevel

type SupportsCruxLogMessage msgs = ?injectCruxLogMessage :: CruxLogMessage -> msgs

cruxLogMessageToSayWhat :: CruxLogMessage -> SayWhat

cruxLogTag :: Text

logException :: Logs msgs => SomeException -> IO ()

Function used to log/output exception information

logGoal :: Logs msgs => ProvedGoals -> IO ()

Function used to output any individual goal proof failures from a simulation

logSimResult :: Logs msgs => Bool -> CruxSimulationResult -> IO ()

Function used to output the summary result for a completed simulation. If the flag is true, show the details of each failed goal before showing the summary.

say :: Logs msgs => (?injectMessage :: msg -> msgs) => msg -> IO ()

Main function used to log/output a general text message of some kind

sayCrux :: Logs msgs => SupportsCruxLogMessage msgs => CruxLogMessage -> IO ()

withCruxLogMessage :: (SupportsCruxLogMessage CruxLogMessage => a) -> a

Low-level output API functions

output :: Logs msgs => String -> IO ()

This function emits output to the normal output handle (specified at initialization time). This function is not recommended for general use (the says, logException, logSimResult, logGoal, etc. are preferred), but can be used by code needing more control over the output formatting.

This function does _not_ emit a newline at the end of the output.

outputLn :: Logs msgs => String -> IO ()

This function emits output to the normal output handle (specified at initialization time). This function is not recommended for general use (the says, logException, logSimResult, logGoal, etc. are preferred), but can be used by code needing more control over the output formatting.

This function emits a newline at the end of the output.

Converting and emitting output

logToStd :: (Handle, Bool) -> (Handle, Bool) -> SayWhat -> IO ()

This is the default logging output function for a SayWhat message. It will emit the information with possible coloring (if enabled via the first argument) to the proper handle (normal output goes to the first handle, error output goes to the second handle, and the same handle may be used for both).

Front-ends that don't have specific output needs can simply use this function. Alternative output functions can be used where useful (e.g. JSON output).