Lang.Crucible.Backend.AssumptionStack

This module provides management support for keeping track of a context of logical assumptions. The API provided here is similar to the interactive mode of an SMT solver. Logical conditions can be assumed into the current context, and bundles of assumptions are organized into frames which are pushed and popped by the user to manage the state.

Additionally, proof goals can be asserted to the system. These will be turned into complete logical statements by assuming the current context and be stashed in a collection of remembered goals for later dispatch to solvers.

Assertions and proof goals

data ProofGoal asmp goal

A proof goal consists of a collection of assumptions that were in scope when an assertion was made, together with the given assertion.

Constructors

ProofGoal

Fields

• proofAssumptions :: asmp
• proofGoal :: goal

data Goals asmp goal

A collection of goals, which can represent shared assumptions.

Constructors

Assuming asmp !(Goals asmp goal)

Make an assumption that is in context for all the contained goals.

Prove goal

A proof obligation, to be proved in the context of all previously-made assumptions.

ProveConj !(Goals asmp goal) !(Goals asmp goal)

A conjunction of two goals.

Instances

(Show asmp, Show goal) => Show (Goals asmp goal)

Defined in Lang.Crucible.Backend.ProofGoals

Methods

showsPrec :: Int -> Goals asmp goal -> ShowS

show :: Goals asmp goal -> String

showList :: [Goals asmp goal] -> ShowS

Frames and assumption stacks

Basic data types

data FrameIdentifier

A FrameIdentifier is a value that identifies an an assumption frame. These are expected to be unique when a new frame is pushed onto the stack. This is primarily a debugging aid, to ensure that stack management remains well-bracketed.

Instances

Eq FrameIdentifier

Defined in Lang.Crucible.Backend.ProofGoals

Methods

(==) :: FrameIdentifier -> FrameIdentifier -> Bool

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

Ord FrameIdentifier

Defined in Lang.Crucible.Backend.ProofGoals

Methods

compare :: FrameIdentifier -> FrameIdentifier -> Ordering

(<) :: FrameIdentifier -> FrameIdentifier -> Bool

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

(>) :: FrameIdentifier -> FrameIdentifier -> Bool

(>=) :: FrameIdentifier -> FrameIdentifier -> Bool

max :: FrameIdentifier -> FrameIdentifier -> FrameIdentifier

min :: FrameIdentifier -> FrameIdentifier -> FrameIdentifier

data AssumptionFrame asmp

A single AssumptionFrame represents a collection of assumptions. They will later be rescinded when the associated frame is popped from the stack.

Constructors

AssumptionFrame

Fields

• assumeFrameIdent :: FrameIdentifier
• assumeFrameCond :: asmp

data AssumptionFrames asmp

The AssumptionFrames data structure captures the current state of assumptions made inside a GoalCollector.

Constructors

AssumptionFrames

Fields

• baseFrame :: !asmp

  Assumptions made at the top level of a solver.

• pushedFrames :: !(Seq (FrameIdentifier, asmp))

  A sequence of pushed frames, together with the assumptions that were made in each frame. The sequence is organized with newest frames on the end (right side) of the sequence.

data AssumptionStack asmp ast

An assumption stack is a data structure for tracking logical assumptions and proof obligations. Assumptions can be added to the current stack frame, and stack frames may be pushed (to remember a previous state) or popped to restore a previous state.

Constructors

AssumptionStack

Fields

• assumeStackGen :: IO FrameIdentifier
• proofObligations :: IORef (GoalCollector asmp ast)

Manipulating assumption stacks

initAssumptionStack :: NonceGenerator IO t -> IO (AssumptionStack asmp ast)

Produce a fresh assumption stack.

saveAssumptionStack :: Monoid asmp => AssumptionStack asmp ast -> IO (GoalCollector asmp ast)

Record the current state of the assumption stack in a data structure that can later be used to restore the current assumptions.

NOTE! however, that proof obligations are NOT copied into the saved stack data. Instead, proof obligations remain only in the original AssumptionStack and the new stack has an empty obligation list.

restoreAssumptionStack :: Monoid asmp => GoalCollector asmp ast -> AssumptionStack asmp ast -> IO ()

Restore a previously saved assumption stack. Any proof obligations in the saved stack will be copied into the assumption stack, which will also retain any proof obligations it had previously. A saved stack created with saveAssumptionStack will have no included proof obligations; restoring such a stack will have no effect on the current proof obligations.

pushFrame :: AssumptionStack asmp ast -> IO FrameIdentifier

Push a new assumption frame on top of the stack. The returned FrameIdentifier can be used later to pop this frame. Frames must be pushed and popped in a coherent, well-bracketed way.

popFrame :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO asmp

Pop a previously-pushed assumption frame from the stack. All assumptions in that frame will be forgotten. The assumptions contained in the popped frame are returned.

popFrameAndGoals :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO (asmp, Maybe (Goals asmp ast))

popFramesUntil :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO Int

Pop all frames up to and including the frame with the given identifier. The return value indicates how many stack frames were popped.

resetStack :: Monoid asmp => AssumptionStack asmp ast -> IO ()

Reset the AssumptionStack to an empty set of assumptions, but retain any pending proof obligations.

getProofObligations :: Monoid asmp => AssumptionStack asmp ast -> IO (Maybe (Goals asmp ast))

Retrieve the current collection of proof obligations.

clearProofObligations :: Monoid asmp => AssumptionStack asmp ast -> IO ()

Remove all pending proof obligations.

addProofObligation :: ast -> AssumptionStack asmp ast -> IO ()

Add a new proof obligation to the current collection of obligations based on all the assumptions currently in scope and the predicate in the given assertion.

inFreshFrame :: Monoid asmp => AssumptionStack asmp ast -> IO a -> IO (asmp, a)

Run an action in the scope of a fresh assumption frame. The frame will be popped and returned on successful completion of the action. If the action raises an exception, the frame will be popped and discarded.

Assumption management

collectAssumptions :: Monoid asmp => AssumptionStack asmp ast -> IO asmp

Collect all the assumptions currently in scope in this stack frame and all previously-pushed stack frames.

appendAssumptions :: Monoid asmp => asmp -> AssumptionStack asmp ast -> IO ()

Add the given collection logical assumptions to the current stack frame.

allAssumptionFrames :: Monoid asmp => AssumptionStack asmp ast -> IO (AssumptionFrames asmp)