Safe Haskell	None
Language	Haskell2010

Copilot.Verifier.Log

Synopsis

type SupportsCopilotLogMessage msgs = ?injectCopilotLogMessage :: CopilotLogMessage -> msgs
data CopilotLogMessage where
- GeneratedCFile :: FilePath -> CopilotLogMessage
- CompiledBitcodeFile :: String -> FilePath -> CopilotLogMessage
- TranslatedToCrucible :: CopilotLogMessage
- GeneratingProofState :: CopilotLogMessage
- ComputingConditions :: VerificationStep -> CopilotLogMessage
- ProvingConditions :: VerificationStep -> CopilotLogMessage
- AllGoalsProved :: CopilotLogMessage
- OnlySomeGoalsProved :: Integer -> Integer -> CopilotLogMessage
- SuccessfulProofSummary :: FilePath -> Integer -> Integer -> CopilotLogMessage
- NoisyVerbositySuggestion :: CopilotLogMessage
- StreamValueEqualityProofGoal :: forall sym copilotType (crucibleType :: CrucibleType). IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> StreamValueEquality sym copilotType crucibleType -> CopilotLogMessage
- TriggersInvokedCorrespondinglyProofGoal :: forall sym. IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> TriggersInvokedCorrespondingly sym -> CopilotLogMessage
- TriggerArgumentEqualityProofGoal :: forall sym copilotType (crucibleType :: CrucibleType). IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> TriggerArgumentEquality sym copilotType crucibleType -> CopilotLogMessage
- RingBufferLoadProofGoal :: forall sym copilotType (crucibleType :: CrucibleType). IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> RingBufferLoad sym copilotType crucibleType -> CopilotLogMessage
- RingBufferIndexLoadProofGoal :: forall sym. IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> RingBufferIndexLoad sym -> CopilotLogMessage
- PointerArgumentLoadProofGoal :: forall sym copilotType (crucibleType :: CrucibleType). IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> PointerArgumentLoad sym copilotType crucibleType -> CopilotLogMessage
- AccessorFunctionLoadProofGoal :: forall sym. IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> AccessorFunctionLoad sym -> CopilotLogMessage
- GuardFunctionLoadProofGoal :: forall sym. IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> GuardFunctionLoad sym -> CopilotLogMessage
- UnknownFunctionLoadProofGoal :: forall sym. IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> UnknownFunctionLoad sym -> CopilotLogMessage
- LLVMBadBehaviorCheckProofGoal :: forall sym. IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> LLVMBadBehaviorCheck sym -> CopilotLogMessage
data VerificationStep
- = InitialState
- | StepBisimulation
data StateRelationStep
data VerifierAssertion sym
- = StreamValueEqualityAssertion (SomeSome (StreamValueEquality sym))
- | TriggersInvokedCorrespondinglyAssertion (TriggersInvokedCorrespondingly sym)
- | TriggerArgumentEqualityAssertion (SomeSome (TriggerArgumentEquality sym))
- | RingBufferLoadAssertion (SomeSome (RingBufferLoad sym))
- | RingBufferIndexLoadAssertion (RingBufferIndexLoad sym)
- | PointerArgumentLoadAssertion (SomeSome (PointerArgumentLoad sym))
- | AccessorFunctionLoadAssertion (AccessorFunctionLoad sym)
- | GuardFunctionLoadAssertion (GuardFunctionLoad sym)
- | UnknownFunctionLoadAssertion (UnknownFunctionLoad sym)
- | LLVMBadBehaviorCheckAssertion (LLVMBadBehaviorCheck sym)
data SomeSome (f :: j -> k -> Type) where
- SomeSome :: forall {j} {k} (f :: j -> k -> Type) (x :: j) (y :: k). f x y -> SomeSome f
data StreamValueEquality sym copilotType (crucibleType :: CrucibleType) where
- StreamValueEquality :: forall sym copilotType (crucibleType :: CrucibleType). sym -> StateRelationStep -> ProgramLoc -> Text -> Integer -> Integer -> Type copilotType -> XExpr sym -> TypeRepr crucibleType -> RegValue sym crucibleType -> StreamValueEquality sym copilotType crucibleType
data TriggersInvokedCorrespondingly sym where
- TriggersInvokedCorrespondingly :: forall sym. ProgramLoc -> Name -> SymNat sym -> SymNat sym -> TriggersInvokedCorrespondingly sym
data TriggerArgumentEquality sym copilotType (crucibleType :: CrucibleType) where
- TriggerArgumentEquality :: forall sym copilotType (crucibleType :: CrucibleType). sym -> ProgramLoc -> Name -> Integer -> Type copilotType -> XExpr sym -> TypeRepr crucibleType -> RegValue sym crucibleType -> TriggerArgumentEquality sym copilotType crucibleType
data RingBufferLoad sym copilotType (crucibleType :: CrucibleType) where
- RingBufferLoad :: forall sym copilotType (crucibleType :: CrucibleType). sym -> StateRelationStep -> ProgramLoc -> Text -> Integer -> Integer -> Type copilotType -> TypeRepr crucibleType -> Pred sym -> RingBufferLoad sym copilotType crucibleType
data RingBufferIndexLoad sym where
- RingBufferIndexLoad :: forall sym. sym -> StateRelationStep -> ProgramLoc -> Text -> Pred sym -> RingBufferIndexLoad sym
data PointerArgumentLoad sym copilotType (crucibleType :: CrucibleType) where
- PointerArgumentLoad :: forall sym copilotType (crucibleType :: CrucibleType). sym -> ProgramLoc -> Type copilotType -> TypeRepr crucibleType -> Pred sym -> PointerArgumentLoad sym copilotType crucibleType
data AccessorFunctionLoad sym where
- AccessorFunctionLoad :: forall sym. sym -> ProgramLoc -> FunctionName -> Pred sym -> AccessorFunctionLoad sym
data GuardFunctionLoad sym where
- GuardFunctionLoad :: forall sym. sym -> ProgramLoc -> FunctionName -> Pred sym -> GuardFunctionLoad sym
data UnknownFunctionLoad sym where
- UnknownFunctionLoad :: forall sym. sym -> ProgramLoc -> FunctionName -> Pred sym -> UnknownFunctionLoad sym
data LLVMBadBehaviorCheck sym where
- LLVMBadBehaviorCheck :: forall sym. sym -> ProgramLoc -> CallStack -> BadBehavior sym -> Pred sym -> LLVMBadBehaviorCheck sym
sayCopilot :: (Logs msgs, SupportsCopilotLogMessage msgs) => CopilotLogMessage -> IO ()
copilotLogMessageToSayWhat :: CopilotLogMessage -> SayWhat

Documentation

type SupportsCopilotLogMessage msgs = ?injectCopilotLogMessage :: CopilotLogMessage -> msgs Source #

data CopilotLogMessage where Source #

Constructors

GeneratedCFile
Fields :: FilePath The path of the generated C File -> CopilotLogMessage
CompiledBitcodeFile
Fields :: String The prefix to use in the compiled bitcode's directory -> FilePath The name of the generated LLVM bitcode file -> CopilotLogMessage
TranslatedToCrucible :: CopilotLogMessage
GeneratingProofState :: CopilotLogMessage
ComputingConditions :: VerificationStep -> CopilotLogMessage
ProvingConditions :: VerificationStep -> CopilotLogMessage
AllGoalsProved :: CopilotLogMessage
OnlySomeGoalsProved
Fields :: Integer Number of goals proved -> Integer Number of total goals -> CopilotLogMessage
SuccessfulProofSummary
Fields :: FilePath Name of the generated C file. -> Integer Number of goals proven during for the initial state of the proof. -> Integer Number of goals proven during the bisimulation step of the proof. -> CopilotLogMessage
NoisyVerbositySuggestion :: CopilotLogMessage
StreamValueEqualityProofGoal :: forall sym copilotType (crucibleType :: CrucibleType). IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> StreamValueEquality sym copilotType crucibleType -> CopilotLogMessage
TriggersInvokedCorrespondinglyProofGoal :: forall sym. IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> TriggersInvokedCorrespondingly sym -> CopilotLogMessage
TriggerArgumentEqualityProofGoal :: forall sym copilotType (crucibleType :: CrucibleType). IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> TriggerArgumentEquality sym copilotType crucibleType -> CopilotLogMessage
RingBufferLoadProofGoal :: forall sym copilotType (crucibleType :: CrucibleType). IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> RingBufferLoad sym copilotType crucibleType -> CopilotLogMessage
RingBufferIndexLoadProofGoal :: forall sym. IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> RingBufferIndexLoad sym -> CopilotLogMessage
PointerArgumentLoadProofGoal :: forall sym copilotType (crucibleType :: CrucibleType). IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> PointerArgumentLoad sym copilotType crucibleType -> CopilotLogMessage
AccessorFunctionLoadProofGoal :: forall sym. IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> AccessorFunctionLoad sym -> CopilotLogMessage
GuardFunctionLoadProofGoal :: forall sym. IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> GuardFunctionLoad sym -> CopilotLogMessage
UnknownFunctionLoadProofGoal :: forall sym. IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> UnknownFunctionLoad sym -> CopilotLogMessage
LLVMBadBehaviorCheckProofGoal :: forall sym. IsSymExprBuilder sym => VerificationStep -> Integer -> Integer -> LLVMBadBehaviorCheck sym -> CopilotLogMessage

Instances

Instances details

ToJSON CopilotLogMessage Source #
Instance details Defined in Copilot.Verifier.Log Methods toJSON :: CopilotLogMessage -> Value # toEncoding :: CopilotLogMessage -> Encoding # toJSONList :: [CopilotLogMessage] -> Value # toEncodingList :: [CopilotLogMessage] -> Encoding # omitField :: CopilotLogMessage -> Bool #

data VerificationStep Source #

Constructors

InitialState
StepBisimulation

Instances

Instances details

ToJSON VerificationStep Source #

Instance details

Defined in Copilot.Verifier.Log

Methods

toJSON :: VerificationStep -> Value #

toEncoding :: VerificationStep -> Encoding #

toJSONList :: [VerificationStep] -> Value #

toEncodingList :: [VerificationStep] -> Encoding #

omitField :: VerificationStep -> Bool #

Generic VerificationStep Source #

Instance details

Defined in Copilot.Verifier.Log

Associated Types

type Rep VerificationStep
Instance details Defined in Copilot.Verifier.Log type Rep VerificationStep = D1 ('MetaData "VerificationStep" "Copilot.Verifier.Log" "copilot-verifier-4.5.1-GRl6cYRYQsHESR1KdzXCiR" 'False) (C1 ('MetaCons "InitialState" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "StepBisimulation" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: VerificationStep -> Rep VerificationStep x #

to :: Rep VerificationStep x -> VerificationStep #

type Rep VerificationStep Source #

Instance details

Defined in Copilot.Verifier.Log

type Rep VerificationStep = D1 ('MetaData "VerificationStep" "Copilot.Verifier.Log" "copilot-verifier-4.5.1-GRl6cYRYQsHESR1KdzXCiR" 'False) (C1 ('MetaCons "InitialState" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "StepBisimulation" 'PrefixI 'False) (U1 :: Type -> Type))

data StateRelationStep Source #

At what step of the proof are we checking the state relation? We record this so that we can better distinguish between transition step–related proof goals that arise before or after calling the step() function.

Constructors

InitialStateRelation	Check the state relation for the initial state.
PreStepStateRelation	During the transition step of the proof, check the state relation before calling the `step()` function.
PostStepStateRelation	During the transition step of the proof, check the state relation after calling the `step()` function.

Instances

Instances details

ToJSON StateRelationStep Source #

Instance details

Defined in Copilot.Verifier.Log

Methods

toJSON :: StateRelationStep -> Value #

toEncoding :: StateRelationStep -> Encoding #

toJSONList :: [StateRelationStep] -> Value #

toEncodingList :: [StateRelationStep] -> Encoding #

omitField :: StateRelationStep -> Bool #

Generic StateRelationStep Source #

Instance details

Defined in Copilot.Verifier.Log

Associated Types

type Rep StateRelationStep

Instance details

Defined in Copilot.Verifier.Log

type Rep StateRelationStep = D1 ('MetaData "StateRelationStep" "Copilot.Verifier.Log" "copilot-verifier-4.5.1-GRl6cYRYQsHESR1KdzXCiR" 'False) (C1 ('MetaCons "InitialStateRelation" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PreStepStateRelation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PostStepStateRelation" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: StateRelationStep -> Rep StateRelationStep x #

to :: Rep StateRelationStep x -> StateRelationStep #

type Rep StateRelationStep Source #

Instance details

Defined in Copilot.Verifier.Log

type Rep StateRelationStep = D1 ('MetaData "StateRelationStep" "Copilot.Verifier.Log" "copilot-verifier-4.5.1-GRl6cYRYQsHESR1KdzXCiR" 'False) (C1 ('MetaCons "InitialStateRelation" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PreStepStateRelation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PostStepStateRelation" 'PrefixI 'False) (U1 :: Type -> Type)))

data VerifierAssertion sym Source #

Types of assertions that the verifier can make, which will count towards the total number of proof goals.

data SomeSome (f :: j -> k -> Type) where Source #

Like Some in parameterized-utils, but existentially closing over two type parameters instead of just one.

Constructors

SomeSome :: forall {j} {k} (f :: j -> k -> Type) (x :: j) (y :: k). f x y -> SomeSome f

data StreamValueEquality sym copilotType (crucibleType :: CrucibleType) where Source #

An assertion that an element in a Copilot stream is equal to the corresponding element in a C ring buffer.

Constructors

StreamValueEquality

Fields

:: forall sym copilotType (crucibleType :: CrucibleType). sym
-> StateRelationStep
When the values are checked for equality
-> ProgramLoc
The locations of the values
-> Text
The name of the buffer
-> Integer
The offset from the buffer's index, which is used to compute the element of the buffer to load
-> Integer
The number of elements in the buffer
-> Type copilotType
The Copilot type
-> XExpr sym
The Copilot value
-> TypeRepr crucibleType
The Crucible type
-> RegValue sym crucibleType
The Crucible value
-> StreamValueEquality sym copilotType crucibleType

Instances

Instances details

ToJSON (StreamValueEquality sym copilotType crucibleType) Source #

Instance details

Defined in Copilot.Verifier.Log

Methods

toJSON :: StreamValueEquality sym copilotType crucibleType -> Value #

toEncoding :: StreamValueEquality sym copilotType crucibleType -> Encoding #

toJSONList :: [StreamValueEquality sym copilotType crucibleType] -> Value #

toEncodingList :: [StreamValueEquality sym copilotType crucibleType] -> Encoding #

omitField :: StreamValueEquality sym copilotType crucibleType -> Bool #

data TriggersInvokedCorrespondingly sym where Source #

An assertion that, given a Copilot trigger stream and its corresponding C trigger function on a particular time step, either both fired at the same time or both did not fire at all.

Constructors

TriggersInvokedCorrespondingly
Fields :: forall sym. ProgramLoc The location of the trigger -> Name The trigger name -> SymNat sym The expected number of times the trigger was fired this step (should be either 1 or 0). -> SymNat sym The actual number of times the trigger was fired this step. -> TriggersInvokedCorrespondingly sym

Instances

Instances details

ToJSON (TriggersInvokedCorrespondingly sym) Source #
Instance details Defined in Copilot.Verifier.Log Methods toJSON :: TriggersInvokedCorrespondingly sym -> Value # toEncoding :: TriggersInvokedCorrespondingly sym -> Encoding # toJSONList :: [TriggersInvokedCorrespondingly sym] -> Value # toEncodingList :: [TriggersInvokedCorrespondingly sym] -> Encoding # omitField :: TriggersInvokedCorrespondingly sym -> Bool #

data TriggerArgumentEquality sym copilotType (crucibleType :: CrucibleType) where Source #

An assertion that an argument to a Copilot trigger is equal to the corresponding argument to a C trigger function.

Constructors

TriggerArgumentEquality

Fields

:: forall sym copilotType (crucibleType :: CrucibleType). sym
-> ProgramLoc
The locations of the arguments
-> Name
The trigger name
-> Integer
The number of the argument (starting from 0)
-> Type copilotType
The Copilot type
-> XExpr sym
The Copilot value
-> TypeRepr crucibleType
The Crucible type
-> RegValue sym crucibleType
The Crucible value
-> TriggerArgumentEquality sym copilotType crucibleType

Instances

Instances details

ToJSON (TriggerArgumentEquality sym copilotType crucibleType) Source #

Instance details

Defined in Copilot.Verifier.Log

Methods

toJSON :: TriggerArgumentEquality sym copilotType crucibleType -> Value #

toEncoding :: TriggerArgumentEquality sym copilotType crucibleType -> Encoding #

toJSONList :: [TriggerArgumentEquality sym copilotType crucibleType] -> Value #

toEncodingList :: [TriggerArgumentEquality sym copilotType crucibleType] -> Encoding #

omitField :: TriggerArgumentEquality sym copilotType crucibleType -> Bool #

data RingBufferLoad sym copilotType (crucibleType :: CrucibleType) where Source #

An assertion that a load from a ring buffer in C is valid.

Constructors

RingBufferLoad

Fields

:: forall sym copilotType (crucibleType :: CrucibleType). sym
-> StateRelationStep
When the ring buffer is loaded from
-> ProgramLoc
The location of the buffer
-> Text
The name of the buffer
-> Integer
The offset from the buffer's index, which is used to compute the element of the buffer to load
-> Integer
The number of elements in the buffer
-> Type copilotType
The Copilot type of the elements of the array
-> TypeRepr crucibleType
The Crucible type of the elements of the array
-> Pred sym
The assertion that must hold in order for this load to be valid
-> RingBufferLoad sym copilotType crucibleType

Instances

Instances details

ToJSON (RingBufferLoad sym copilotType crucibleType) Source #

Instance details

Defined in Copilot.Verifier.Log

Methods

toJSON :: RingBufferLoad sym copilotType crucibleType -> Value #

toEncoding :: RingBufferLoad sym copilotType crucibleType -> Encoding #

toJSONList :: [RingBufferLoad sym copilotType crucibleType] -> Value #

toEncodingList :: [RingBufferLoad sym copilotType crucibleType] -> Encoding #

omitField :: RingBufferLoad sym copilotType crucibleType -> Bool #

data RingBufferIndexLoad sym where Source #

An assertion that a load from a global variable representing a ring buffer's index in C is valid.

Constructors

RingBufferIndexLoad
Fields :: forall sym. sym -> StateRelationStep When the index's global variable is loaded from -> ProgramLoc The location of the global index -> Text The name of the global index -> Pred sym The assertion that must hold in order for this load to be valid -> RingBufferIndexLoad sym

Instances

Instances details

ToJSON (RingBufferIndexLoad sym) Source #
Instance details Defined in Copilot.Verifier.Log Methods toJSON :: RingBufferIndexLoad sym -> Value # toEncoding :: RingBufferIndexLoad sym -> Encoding # toJSONList :: [RingBufferIndexLoad sym] -> Value # toEncodingList :: [RingBufferIndexLoad sym] -> Encoding # omitField :: RingBufferIndexLoad sym -> Bool #

data PointerArgumentLoad sym copilotType (crucibleType :: CrucibleType) where Source #

An assertion that a load from a pointer argument to a trigger function in C is valid.

Constructors

PointerArgumentLoad
Fields :: forall sym copilotType (crucibleType :: CrucibleType). sym -> ProgramLoc The location of the pointer -> Type copilotType The Copilot type of the underlying memory -> TypeRepr crucibleType The Crucible type of the underlying memory -> Pred sym The assertion that must hold in order for this load to be valid -> PointerArgumentLoad sym copilotType crucibleType

Instances

Instances details

ToJSON (PointerArgumentLoad sym copilotType crucibleType) Source #

Instance details

Defined in Copilot.Verifier.Log

Methods

toJSON :: PointerArgumentLoad sym copilotType crucibleType -> Value #

toEncoding :: PointerArgumentLoad sym copilotType crucibleType -> Encoding #

toJSONList :: [PointerArgumentLoad sym copilotType crucibleType] -> Value #

toEncodingList :: [PointerArgumentLoad sym copilotType crucibleType] -> Encoding #

omitField :: PointerArgumentLoad sym copilotType crucibleType -> Bool #

data AccessorFunctionLoad sym where Source #

An assertion that a load occurring from somewhere in a stream accessor function in C (e.g., s0_get) is valid. This is a somewhat imprecise assertion, as it doesn't identify why the load occurs. (Most likely, it happens because of an array index.)

Constructors

AccessorFunctionLoad
Fields :: forall sym. sym -> ProgramLoc The location of the accessor function -> FunctionName The name of the accessor function -> Pred sym The assertion that must hold in order for this load to be valid -> AccessorFunctionLoad sym

Instances

Instances details

ToJSON (AccessorFunctionLoad sym) Source #
Instance details Defined in Copilot.Verifier.Log Methods toJSON :: AccessorFunctionLoad sym -> Value # toEncoding :: AccessorFunctionLoad sym -> Encoding # toJSONList :: [AccessorFunctionLoad sym] -> Value # toEncodingList :: [AccessorFunctionLoad sym] -> Encoding # omitField :: AccessorFunctionLoad sym -> Bool #

data GuardFunctionLoad sym where Source #

An assertion that a load occurring from somewhere in a trigger guard function in C (e.g., even_guard) is valid. This is a somewhat imprecise assertion, as it doesn't identify why the load occurs. (Most likely, it happens because of an array index.)

Constructors

GuardFunctionLoad
Fields :: forall sym. sym -> ProgramLoc The location of the guard function -> FunctionName The name of the guard function -> Pred sym The assertion that must hold in order for this load to be valid -> GuardFunctionLoad sym

Instances

Instances details

ToJSON (GuardFunctionLoad sym) Source #
Instance details Defined in Copilot.Verifier.Log Methods toJSON :: GuardFunctionLoad sym -> Value # toEncoding :: GuardFunctionLoad sym -> Encoding # toJSONList :: [GuardFunctionLoad sym] -> Value # toEncodingList :: [GuardFunctionLoad sym] -> Encoding # omitField :: GuardFunctionLoad sym -> Bool #

data UnknownFunctionLoad sym where Source #

An assertion that a load occurring in some function is valid. If you see this assertion, it is because the heuristics used to identify where load-related assertions come from could not identify a more precise cause for a load.

Constructors

UnknownFunctionLoad
Fields :: forall sym. sym -> ProgramLoc The location of the function -> FunctionName The name of the function -> Pred sym The assertion that must hold in order for this load to be valid -> UnknownFunctionLoad sym

Instances

Instances details

ToJSON (UnknownFunctionLoad sym) Source #
Instance details Defined in Copilot.Verifier.Log Methods toJSON :: UnknownFunctionLoad sym -> Value # toEncoding :: UnknownFunctionLoad sym -> Encoding # toJSONList :: [UnknownFunctionLoad sym] -> Value # toEncodingList :: [UnknownFunctionLoad sym] -> Encoding # omitField :: UnknownFunctionLoad sym -> Bool #

data LLVMBadBehaviorCheck sym where Source #

An assertion that checks that some form of bad behavior in LLVM does not occur. Bad behavior includes both undefined behavior and memory unsafety.

Constructors

LLVMBadBehaviorCheck
Fields :: forall sym. sym -> ProgramLoc The location of the check -> CallStack A call stack for the check, if one exists -> BadBehavior sym What type of LLVM bad behavior is being checked for -> Pred sym The assertion that must hold in order for this check to succeed -> LLVMBadBehaviorCheck sym

Instances

Instances details

ToJSON (LLVMBadBehaviorCheck sym) Source #
Instance details Defined in Copilot.Verifier.Log Methods toJSON :: LLVMBadBehaviorCheck sym -> Value # toEncoding :: LLVMBadBehaviorCheck sym -> Encoding # toJSONList :: [LLVMBadBehaviorCheck sym] -> Value # toEncodingList :: [LLVMBadBehaviorCheck sym] -> Encoding # omitField :: LLVMBadBehaviorCheck sym -> Bool #

sayCopilot :: (Logs msgs, SupportsCopilotLogMessage msgs) => CopilotLogMessage -> IO () Source #

copilotLogMessageToSayWhat :: CopilotLogMessage -> SayWhat Source #

StreamValueEqualityAssertion (SomeSome (StreamValueEquality sym))
TriggersInvokedCorrespondinglyAssertion (TriggersInvokedCorrespondingly sym)
TriggerArgumentEqualityAssertion (SomeSome (TriggerArgumentEquality sym))
RingBufferLoadAssertion (SomeSome (RingBufferLoad sym))
RingBufferIndexLoadAssertion (RingBufferIndexLoad sym)
PointerArgumentLoadAssertion (SomeSome (PointerArgumentLoad sym))
AccessorFunctionLoadAssertion (AccessorFunctionLoad sym)
GuardFunctionLoadAssertion (GuardFunctionLoad sym)
UnknownFunctionLoadAssertion (UnknownFunctionLoad sym)
LLVMBadBehaviorCheckAssertion (LLVMBadBehaviorCheck sym)