Crux.Types

Documentation

type SimCtxt personality sym p = SimContext (personality sym) sym p

A simulator context

type OverM personality sym ext a = forall r args ret. OverrideSim (personality sym) sym ext r args ret a

The instance of the override monad we use, when we don't care about the context of the surrounding function.

type Fun personality sym ext args ret = forall r. OverrideSim (personality sym) sym ext r args ret (RegValue sym ret)

This is the instance of the OverrideSim monad that we use.

data Result personality sym where

Constructors

Result :: ExecResult (personality sym) sym ext (RegEntry sym UnitType) -> Result personality sym

data ProcessedGoals

Constructors

ProcessedGoals

Fields

• totalProcessedGoals :: !Integer
• provedGoals :: !Integer
• disprovedGoals :: !Integer
• incompleteGoals :: !Integer

data ProofResult sym

Constructors

Proved [Either (Assumption sym) (Assertion sym)]

NotProved (Doc Void) (Maybe (ModelView, [CrucibleEvent GroundValueWrapper])) [String]

The first argument is an explanation of the failure and counter example as provided by the Explainer (if any), the second maybe a model for the counter-example, and the third is a list of abducts provided which may be empty

type LPred sym = LabeledPred (Pred sym)

data ProvedGoals

Constructors

Branch ProvedGoals ProvedGoals

NotProvedGoal [CrucibleAssumption (Const ())] SimError (Doc Void) [ProgramLoc] (Maybe (ModelView, [CrucibleEvent GroundValueWrapper])) [String]

ProvedGoal [CrucibleAssumption (Const ())] SimError [ProgramLoc] Bool

Keeps only the explanations for the relevant assumptions.

• The array of (AssumptionReason,String) is the set of assumptions for this Goal.
• The (SimError,String) is information about the failure, with the specific SimError (Lang.Crucible.Simulator) and a string representation of the Crucible term that encountered the error.
• The Bool (third argument) indicates if the goal is trivial (i.e., the assumptions are inconsistent)

data ProgramCompleteness

Constructors

ProgramComplete

ProgramIncomplete

Instances

Show ProgramCompleteness

Defined in Crux.Types

Methods

showsPrec :: Int -> ProgramCompleteness -> ShowS

show :: ProgramCompleteness -> String

showList :: [ProgramCompleteness] -> ShowS

Eq ProgramCompleteness

Defined in Crux.Types

Methods

(==) :: ProgramCompleteness -> ProgramCompleteness -> Bool

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

Ord ProgramCompleteness

Defined in Crux.Types

Methods

compare :: ProgramCompleteness -> ProgramCompleteness -> Ordering

(<) :: ProgramCompleteness -> ProgramCompleteness -> Bool

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

(>) :: ProgramCompleteness -> ProgramCompleteness -> Bool

(>=) :: ProgramCompleteness -> ProgramCompleteness -> Bool

max :: ProgramCompleteness -> ProgramCompleteness -> ProgramCompleteness

min :: ProgramCompleteness -> ProgramCompleteness -> ProgramCompleteness

data CruxSimulationResult

Constructors

CruxSimulationResult

Fields

• cruxSimResultCompleteness :: ProgramCompleteness
• cruxSimResultGoals :: Seq (ProcessedGoals, ProvedGoals)

data Crux sym

A dummy datatype that can be used for the "personality" type parameter.

Constructors

CruxPersonality

newtype Vals ty

A list of named GroundValues of the same type (used to report SMT models in a portable way -- see the ModelView datatype).

Constructors

Vals [Entry (GroundValue ty)]

data Entry a

A named value of type a with a program location. Used to describe and report models from SMT queries (see Model and ModelView datatypes).

Constructors

Entry

Fields

• entryName :: String
• entryLoc :: ProgramLoc
• entryValue :: a

newtype ModelView

A portable/concrete view of a model's contents, organized by crucible type. I.e., each crucible type is associated with the list of entries (i.e. named GroundValues) at that type for the given model, used to describe the conditions under which an SMT query is satisfiable.

Constructors

ModelView

Fields

• modelVals :: MapF BaseTypeRepr Vals

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