Lang.Crucible.Simulator.BoundedExec

This module provides an execution feature for bounding the number of iterations that a loop will execute in the simulator.

Documentation

boundedExecFeature

Arguments

:: (SomeHandle -> IO (Maybe Word64))

Action for computing loop bounds for functions when they are called

-> Bool

Produce a proof obligation when resources are exhausted?

-> IO (GenericExecutionFeature sym)

This execution feature allows users to place a bound on the number of iterations that a loop will execute. Each time a function is called, the included action is called to determine if the loops in that function should be bounded, and what their iteration bound should be.

The boolean argument indicates if we should generate proof obligations when we cut off loop execution. If true, loop cutoffs will generate proof obligations which will be provable only if the loop actually could not have executed that number of iterations. If false, the execution of loops will be aborted without generating side conditions.

Note that we compute a weak topological ordering on control flow graphs to determine loop heads and loop nesting structure. Loop bounds for inner loops are reset on every iteration through an outer loop.

Orphan instances

IntrinsicClass sym "BoundedExecFrameData"

Associated Types

type Intrinsic sym "BoundedExecFrameData" ctx

Methods

pushBranchIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "BoundedExecFrameData" -> CtxRepr ctx -> Intrinsic sym "BoundedExecFrameData" ctx -> IO (Intrinsic sym "BoundedExecFrameData" ctx)

abortBranchIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "BoundedExecFrameData" -> CtxRepr ctx -> Intrinsic sym "BoundedExecFrameData" ctx -> IO (Intrinsic sym "BoundedExecFrameData" ctx)

muxIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "BoundedExecFrameData" -> CtxRepr ctx -> Pred sym -> Intrinsic sym "BoundedExecFrameData" ctx -> Intrinsic sym "BoundedExecFrameData" ctx -> IO (Intrinsic sym "BoundedExecFrameData" ctx)