[−][src]Trait gf::ai::Interp

pub trait Interp<'a, D: Direction> {
    type State: Bottom + Clone;
    fn edge(&self, state: &mut Self::State, edge: Edge<'a>);

    fn apply(&self, state: &mut Self::State, stmt: Stmt<'a, Apply>);

    fn call(&self, state: &Self::State, stmt: Stmt<'a, Call>) -> Self::State;

    fn call_ret(
        &self, 
        caller_state: &mut Self::State, 
        callee_state: Self::State, 
        stmt: Stmt<'a, Call>
    );

    fn init(&self, state: &mut Self::State, stmt: Stmt<'a, Init>);

    fn load(&self, state: &mut Self::State, stmt: Stmt<'a, Load>);

    fn mix(&self, state: &mut Self::State, stmt: Stmt<'a, Mix>);

    fn slice(&self, state: &mut Self::State, stmt: Stmt<'a, Slice>);

    fn store(&self, state: &mut Self::State, stmt: Stmt<'a, Store>);
}

🟢 An abstract interpretation.

Each method of this trait is a transfer function that propagates abstract state across an edge, a statement, or part thereof. If a transfer function returns ⊥, this is interpreted as an impossible state.

A transfer function may still be called with ⊥ as input state. It is up to the implementation to ensure correct operation (which is to return ⊥).

Blanket implementations

A blanket implementation is provided for 2- and 3-tuples of same-direction interpretations.

Associated Types

type State: Bottom + Clone

Abstract state.

Loading content...

Required methods

fn edge(&self, state: &mut Self::State, edge: Edge<'a>)

Propagate state across an intraprocedural edge.

Forward interpretation

Input state is at the end of the predecessor. The output state is at the start of the successor.

Backward interpretation

Input state is at the start of the successor. The input state is at the end of the precedessor.

Common implementations

  • State::edge, except that it does nothing about the control variable, so normally preceded by an explicit state update and branch feasibility check.

fn apply(&self, state: &mut Self::State, stmt: Stmt<'a, Apply>)

Propagate state across an APPLY statement.

Forward interpretation

Input state is just before the statement. Output state is just after the statement.

Backward interpretation

Input state is just after the statement. Output state is just before the statement.

fn call(&self, state: &Self::State, stmt: Stmt<'a, Call>) -> Self::State

Propagate state across a CALL statement.

Forward interpretation

Input state is just before the statement. Output state is at the entry of the callee.

Backward interpretation

Input state is just after the statement. Output state is at the exit of the callee.

Common implementations

fn call_ret(
    &self,
    caller_state: &mut Self::State,
    callee_state: Self::State,
    stmt: Stmt<'a, Call>
)

Propagate state across a return from a CALL statement.

Forward interpretation

Input caller state is just before the statement. Input callee state is at the exit of the callee. Output caller state is just after the statement.

Backward interpretation

Input caller state is just after the statement. Input callee state is at the entry of the callee. Output caller state is just before the statement.

Common implementations

fn init(&self, state: &mut Self::State, stmt: Stmt<'a, Init>)

Propagate state across an INIT statement.

Forward interpretation

Input state is just before the statement. Output state is just after the statement.

Backward interpretation

Input state is just after the statement. Output state is just before the statement.

fn load(&self, state: &mut Self::State, stmt: Stmt<'a, Load>)

Propagate state across a LOAD statement.

Forward interpretation

Input state is just before the statement. Output state is just after the statement.

Backward interpretation

Input state is just after the statement. Output state is just before the statement.

fn mix(&self, state: &mut Self::State, stmt: Stmt<'a, Mix>)

Propagate state across a MIX statement.

Forward interpretation

Input state is just before the statement. Output state is just after the statement.

Backward interpretation

Input state is just after the statement. Output state is just before the statement.

Common implementations

fn slice(&self, state: &mut Self::State, stmt: Stmt<'a, Slice>)

Propagate state across a SLICE statement.

Forward interpretation

Input state is just before the statement. Output state is just after the statement.

Backward interpretation

Input state is just after the statement. Output state is just before the statement.

fn store(&self, state: &mut Self::State, stmt: Stmt<'a, Store>)

Propagate state across a STORE statement.

Forward interpretation

Input state is just before the statement. Output state is just after the statement.

Backward interpretation

Input state is just after the statement. Output state is just before the statement.

Loading content...

Implementations on Foreign Types

impl<'a, D, A, B> Interp<'a, D> for (A, B) where
    D: Direction,
    A: Interp<'a, D>,
    B: Interp<'a, D>, [src]

type State = (A::State, B::State)

impl<'a, D, A, B, C> Interp<'a, D> for (A, B, C) where
    D: Direction,
    A: Interp<'a, D>,
    B: Interp<'a, D>,
    C: Interp<'a, D>, [src]

type State = (A::State, B::State, C::State)

Loading content...

Implementors

impl<'a> Interp<'a, Forward> for ConcolicInterp<'a>[src]

type State = ConcolicState<'a>

impl<'a> Interp<'a, Forward> for ConcreteInterp<'a>[src]

type State = ConcreteState<'a>

impl<'a, C: Concretizer> Interp<'a, Forward> for SymbolicInterp<'a, C>[src]

type State = SymbolicState<'a>

Loading content...