Copyright	(c) Galois Inc 2021
License	BSD3
Stability	provisional
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.LLVM.SimpleLoopFixpointCHC

Description

This offers a similar API to what is offered in Lang.Crucible.LLVM.SimpleLoopFixpoint, but this generates proof obligations involving a predicate function (named inv). The intent is that a user will leverage Z3's constrained horn-clause (CHC) functionality to synthesize an implementation of inv and then substitute it back into the proof obligations.

Synopsis

data FixpointEntry sym tp = FixpointEntry {
- headerValue :: SymExpr sym tp
- bodyValue :: SymExpr sym tp
}
data FixpointState sym wptr blocks args
- = BeforeFixpoint
- | ComputeFixpoint (FixpointRecord sym wptr blocks args)
- | CheckFixpoint (FixpointRecord sym wptr blocks args) (SomeSymFn sym) (Some (Assignment (SymExpr sym))) (Pred sym)
- | AfterFixpoint (FixpointRecord sym wptr blocks args)
data CallFrameContext sym wptr ext init ret blocks = CallFrameContext {
- callFrameContextFixpointStates :: MapF (BlockID blocks) (FixpointState sym wptr blocks)
- callFrameContextLoopHeaders :: [Some (BlockID blocks)]
- callFrameContextCFG :: CFG ext blocks init ret
- callFrameContextParentLoop :: Map (Some (BlockID blocks)) (Some (BlockID blocks))
- callFrameContextLoopHeaderBlockIds :: Set (Some (BlockID blocks))
}
data SomeCallFrameContext sym wptr ext init ret = forall blocks. SomeCallFrameContext (CallFrameContext sym wptr ext init ret blocks)
data ExecutionFeatureContext sym wptr ext = ExecutionFeatureContext {
- executionFeatureContextFixpointStates :: FnHandleMap (SomeCallFrameContext sym wptr ext)
- executionFeatureContextInvPreds :: [SomeSymFn sym]
- executionFeatureContextLoopFunEquivConds :: [Pred sym]
}
simpleLoopFixpoint :: (IsSymInterface sym, sym ~ ExprBuilder t st fs, HasPtrWidth wptr, KnownNat wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) => sym -> CFG ext blocks init ret -> GlobalVar Mem -> Maybe (MapF (SymExpr sym) (FixpointEntry sym) -> Pred sym -> IO (MapF (SymExpr sym) (SymExpr sym), Maybe (Pred sym))) -> IO (ExecutionFeature p sym ext rtp, IORef (ExecutionFeatureContext sym wptr ext))

Documentation

data FixpointEntry sym tp Source #

When live loop-carried dependencies are discovered as we traverse a loop body, new "widening" variables are introduced to stand in for those locations. When we introduce such a variable, we capture what value the variable had when we entered the loop (the "header" value); this is essentially the initial value of the variable. We also compute what value the variable should take on its next iteration assuming the loop doesn't exit and executes along its backedge. This "body" value will be computed in terms of the the set of all discovered live variables so far. We know we have reached fixpoint when we don't need to introduce and more fresh widening variables, and the body values for each variable are stable across iterations.

Constructors

FixpointEntry
Fields headerValue :: SymExpr sym tp bodyValue :: SymExpr sym tp

Instances

Instances details

OrdF (FixpointEntry sym) => TestEquality (FixpointEntry sym :: BaseType -> Type) Source #
Instance details Defined in Lang.Crucible.LLVM.SimpleLoopFixpointCHC Methods testEquality :: forall (a :: k) (b :: k). FixpointEntry sym a -> FixpointEntry sym b -> Maybe (a :~: b) #
OrdF (SymExpr sym) => OrdF (FixpointEntry sym :: BaseType -> Type) Source #
Instance details Defined in Lang.Crucible.LLVM.SimpleLoopFixpointCHC Methods compareF :: forall (x :: k) (y :: k). FixpointEntry sym x -> FixpointEntry sym y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). FixpointEntry sym x -> FixpointEntry sym y -> Bool # ltF :: forall (x :: k) (y :: k). FixpointEntry sym x -> FixpointEntry sym y -> Bool # geqF :: forall (x :: k) (y :: k). FixpointEntry sym x -> FixpointEntry sym y -> Bool # gtF :: forall (x :: k) (y :: k). FixpointEntry sym x -> FixpointEntry sym y -> Bool #

data FixpointState sym wptr blocks args Source #

This datatype captures the state machine that progresses as we attempt to compute a loop invariant for a simple structured loop.

Constructors

BeforeFixpoint	We have not yet encoundered the loop head
ComputeFixpoint (FixpointRecord sym wptr blocks args)	We have encountered the loop head at least once, and are in the process of converging to an inductive representation of the live variables in the loop.
CheckFixpoint	We have found an inductively-strong representation of the live variables of the loop, and have discovered the loop index structure controling the execution of the loop. We are now executing the loop once more to compute verification conditions for executions that reamain in the loop.
Fields (FixpointRecord sym wptr blocks args) (SomeSymFn sym) function that represents the loop invariant (Some (Assignment (SymExpr sym))) arguments to the loop invariant (Pred sym) predicate that represents the loop condition
AfterFixpoint (FixpointRecord sym wptr blocks args)	Finally, we stitch everything we have found together into the rest of the program. Starting from the loop header one final time, we now force execution to exit the loop and continue into the rest of the program.

data CallFrameContext sym wptr ext init ret blocks Source #

Constructors

CallFrameContext
Fields callFrameContextFixpointStates :: MapF (BlockID blocks) (FixpointState sym wptr blocks) callFrameContextLoopHeaders :: [Some (BlockID blocks)] callFrameContextCFG :: CFG ext blocks init ret callFrameContextParentLoop :: Map (Some (BlockID blocks)) (Some (BlockID blocks)) callFrameContextLoopHeaderBlockIds :: Set (Some (BlockID blocks))

data SomeCallFrameContext sym wptr ext init ret Source #

Constructors

forall blocks. SomeCallFrameContext (CallFrameContext sym wptr ext init ret blocks)

data ExecutionFeatureContext sym wptr ext Source #

Constructors

ExecutionFeatureContext
Fields executionFeatureContextFixpointStates :: FnHandleMap (SomeCallFrameContext sym wptr ext) executionFeatureContextInvPreds :: [SomeSymFn sym] executionFeatureContextLoopFunEquivConds :: [Pred sym]

simpleLoopFixpoint Source #

Arguments

:: (IsSymInterface sym, sym ~ ExprBuilder t st fs, HasPtrWidth wptr, KnownNat wptr, HasLLVMAnn sym, ?memOpts :: MemOptions)
=> sym
-> CFG ext blocks init ret	The function we want to verify
-> GlobalVar Mem	global variable representing memory
-> Maybe (MapF (SymExpr sym) (FixpointEntry sym) -> Pred sym -> IO (MapF (SymExpr sym) (SymExpr sym), Maybe (Pred sym)))
-> IO (ExecutionFeature p sym ext rtp, IORef (ExecutionFeatureContext sym wptr ext))

This execution feature is designed to allow a limited form of verification for programs with unbounded looping structures.

It is currently highly experimental and has many limitations. Most notably, it only really works properly for functions consisting of a single, non-nested loop with a single exit point. Moreover, the loop must have an indexing variable that counts up from a starting point by a fixed stride amount.

Currently, these assumptions about the loop structure are not checked.

The basic use case here is for verifying functions that loop through an array of data of symbolic length. This is done by providing a ""fixpoint function" which describes how the live values in the loop at an arbitrary iteration are used to compute the final values of those variables before execution leaves the loop. The number and order of these variables depends on internal details of the representation, so is relatively fragile.