Lang.Crucible.Simulator.BoundedRecursion

This module provides an execution feature for bounding recursion. Essentially, we bound the number of times any particular function is allowed to have active frames on the call stack.

Documentation

boundedRecursionFeature

Arguments

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

Action for computing what recursion depth to allow for the given function

-> 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 recursive calls that a function can execute. Each time a function is called, the number of activations of the functions is incremented, and the path is aborted if the bound is exceeded.

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

Orphan instances

IntrinsicClass sym "BoundedRecursionData"

Associated Types

type Intrinsic sym "BoundedRecursionData" ctx

Methods

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

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

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