Copyright	(c) Galois Inc 2018
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.Backend.AssumptionStack

Contents

Assertions and proof goals
Frames and assumption stacks

Description

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.

Synopsis

data ProofGoal asmp goal = ProofGoal {
- proofAssumptions :: asmp
- proofGoal :: goal
}
data Goals asmp goal
- = Assuming asmp !(Goals asmp goal)
- | Prove goal
- | ProveConj !(Goals asmp goal) !(Goals asmp goal)
data FrameIdentifier
data AssumptionFrame asmp = AssumptionFrame {
- assumeFrameIdent :: FrameIdentifier
- assumeFrameCond :: asmp
}
data AssumptionFrames asmp = AssumptionFrames {
- baseFrame :: !asmp
- pushedFrames :: !(Seq (FrameIdentifier, asmp))
}
data AssumptionStack asmp ast = AssumptionStack {
- assumeStackGen :: IO FrameIdentifier
- proofObligations :: IORef (GoalCollector asmp ast)
}
initAssumptionStack :: NonceGenerator IO t -> IO (AssumptionStack asmp ast)
saveAssumptionStack :: Monoid asmp => AssumptionStack asmp ast -> IO (GoalCollector asmp ast)
restoreAssumptionStack :: Monoid asmp => GoalCollector asmp ast -> AssumptionStack asmp ast -> IO ()
pushFrame :: AssumptionStack asmp ast -> IO FrameIdentifier
popFrame :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO asmp
popFrameAndGoals :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO (asmp, Maybe (Goals asmp ast))
popFramesUntil :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO Int
resetStack :: Monoid asmp => AssumptionStack asmp ast -> IO ()
getProofObligations :: Monoid asmp => AssumptionStack asmp ast -> IO (Maybe (Goals asmp ast))
clearProofObligations :: Monoid asmp => AssumptionStack asmp ast -> IO ()
addProofObligation :: ast -> AssumptionStack asmp ast -> IO ()
inFreshFrame :: Monoid asmp => AssumptionStack asmp ast -> IO a -> IO (asmp, a)
collectAssumptions :: Monoid asmp => AssumptionStack asmp ast -> IO asmp
appendAssumptions :: Monoid asmp => asmp -> AssumptionStack asmp ast -> IO ()
allAssumptionFrames :: Monoid asmp => AssumptionStack asmp ast -> IO (AssumptionFrames asmp)

Assertions and proof goals

data ProofGoal asmp goal Source #

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 Source #

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

Instances details

(Show asmp, Show goal) => Show (Goals asmp goal) Source #
Instance details 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 Source #

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

Instances details

Show FrameIdentifier Source #
Instance details Defined in Lang.Crucible.Backend.ProofGoals Methods showsPrec :: Int -> FrameIdentifier -> ShowS # show :: FrameIdentifier -> String # showList :: [FrameIdentifier] -> ShowS #
Eq FrameIdentifier Source #
Instance details Defined in Lang.Crucible.Backend.ProofGoals Methods (==) :: FrameIdentifier -> FrameIdentifier -> Bool # (/=) :: FrameIdentifier -> FrameIdentifier -> Bool #
Ord FrameIdentifier Source #
Instance details 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 Source #

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 Source #

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 Source #

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) Source #

Produce a fresh assumption stack.

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

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 () Source #

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 Source #

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 Source #

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)) Source #

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

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 () Source #

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)) Source #

Retrieve the current collection of proof obligations.

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

Remove all pending proof obligations.

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

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) Source #

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 Source #

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 () Source #

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

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