Inheritance diagram for P4Tools::P4Testgen::AbstractStepper:

[legend]

Public Types
using	Branch = SmallStepEvaluator::Branch

using	Result = SmallStepEvaluator::Result

Public Member Functions
	AbstractStepper (ExecutionState &state, AbstractSolver &solver, const ProgramInfo &programInfo)

bool	preorder (const IR::Node *) override
	Provides generic handling of unsupported nodes.

Result	step (const IR::Node *)

Protected Member Functions
void	declareBaseType (ExecutionState &nextState, const IR::StateVariable &paramPath, const IR::Type_Base *baseType) const

void	declareStructLike (ExecutionState &nextState, const IR::StateVariable &parentExpr, bool forceTaint=false) const

const IR::Literal *	evaluateExpression (const IR::Expression expr, std::optional< const IR::Expression > cond) const

virtual std::string	getClassName ()=0

virtual const ProgramInfo &	getProgramInfo () const

void	logStep (const IR::Node *node)
	Helper function for debugging execution of small stepper.

void	setHeaderValidity (const IR::StateVariable &headerRef, bool validity, ExecutionState &state)

void	setTargetUninitialized (ExecutionState &nextState, const IR::StateVariable &ref, bool forceTaint) const

bool	stepGetHeaderValidity (const IR::StateVariable &headerRef)

bool	stepSetHeaderValidity (const IR::StateVariable &headerRef, bool validity)

bool	stepStackPushPopFront (const IR::Expression stackRef, const IR::Vector< IR::Argument > args, bool isPush=true)

bool	stepSymbolicValue (const IR::Node *)

bool	stepToException (Continuation::Exception)

Static Protected Member Functions
static void	checkMemberInvariant (const IR::Node *node)

static bool	stepToListSubexpr (const IR::BaseListExpression subexpr, SmallStepEvaluator::Result &result, const ExecutionState &state, std::function< const Continuation::Command(const IR::BaseListExpression )> rebuildCmd)

static bool	stepToStructSubexpr (const IR::StructExpression subexpr, SmallStepEvaluator::Result &result, const ExecutionState &state, std::function< const Continuation::Command(const IR::StructExpression )> rebuildCmd)

static bool	stepToSubexpr (const IR::Expression subexpr, SmallStepEvaluator::Result &result, const ExecutionState &state, std::function< const Continuation::Command(const Continuation::Parameter )> rebuildCmd)

Protected Attributes
const ProgramInfo &	programInfo
	Target-specific information about the P4 program being evaluated.

Result	result
	The output of the evaluation.

AbstractSolver &	solver
	The solver backing the state being executed.

ExecutionState &	state
	The state being evaluated.

Detailed Description

A framework for implementing small-step operational semantics. Each instance is good for one small-step evaluation.

Though this inherits from the compiler's visitor framework, it's not really a visitor. It just leverages the framework to obtain multiple dispatch on IR nodes. Implementations should override the preorder methods for those nodes whose evaluation they support and place the result of the evaluation in result.

Member Function Documentation

◆ checkMemberInvariant()

void P4Tools::P4Testgen::AbstractStepper::checkMemberInvariant ( const IR::Node * node )

staticprotected

Checks our assumption that chains of Member expressions terminate in a PathExpression. Throws a BUG if node is not a chain of one or more Member expressions terminating in a PathExpression. if node is local variable then returns created member for it.

◆ declareBaseType()

void P4Tools::P4Testgen::AbstractStepper::declareBaseType	(	ExecutionState &	nextState,
		const IR::StateVariable &	paramPath,
		const IR::Type_Base *	baseType ) const

protected

This is a helper function to declare base type variables. Because all variables need to be a member in the execution state environment, this helper function suffixes a "*".

◆ declareStructLike()

void P4Tools::P4Testgen::AbstractStepper::declareStructLike	(	ExecutionState &	nextState,
		const IR::StateVariable &	parentExpr,
		bool	forceTaint = false ) const

protected

This is a helper function to declare structlike data structures. This also is used to declare the members of a stack. This function is primarily used by the Declaration_Variable preorder function.

◆ evaluateExpression()

const IR::Literal * P4Tools::P4Testgen::AbstractStepper::evaluateExpression	(	const IR::Expression *	expr,
		std::optional< const IR::Expression * >	cond ) const

protected

Evaluates an expression by invoking the solver under the current collected constraints. Optionally, a condition can be provided that is temporarily added to the list of assertions. If the solver can find a solution, it

Returns: the assigned value to the expression. If not, this function; nullptr.

◆ getClassName()

virtual std::string P4Tools::P4Testgen::AbstractStepper::getClassName ( )

protectedpure virtual

Returns: the name of the dynamic type of this object.

Implemented in P4Tools::P4Testgen::Bmv2::Bmv2V1ModelCmdStepper, P4Tools::P4Testgen::Bmv2::Bmv2V1ModelExprStepper, P4Tools::P4Testgen::EBPF::EBPFCmdStepper, P4Tools::P4Testgen::EBPF::EBPFExprStepper, P4Tools::P4Testgen::Pna::PnaDpdkCmdStepper, and P4Tools::P4Testgen::Pna::PnaDpdkExprStepper.

◆ setHeaderValidity()

void P4Tools::P4Testgen::AbstractStepper::setHeaderValidity	(	const IR::StateVariable &	headerRef,
		bool	validity,
		ExecutionState &	state )

protected

Sets validity for a header if expr is a header. if expr is a part of a header union then it sets invalid for other headers in the union. Otherwise it generates an exception.

◆ setTargetUninitialized()

void P4Tools::P4Testgen::AbstractStepper::setTargetUninitialized	(	ExecutionState &	nextState,
		const IR::StateVariable &	ref,
		bool	forceTaint ) const

protected

Reset the given reference to an uninitialized value. If the reference has a Type_StructLike, unroll the reference and reset each member. If forceTaint is active, all references are set tainted. Otherwise a target-specific mechanism is used.

◆ step()

AbstractStepper::Result P4Tools::P4Testgen::AbstractStepper::step ( const IR::Node * node )

Steps on the given node. This is the main entry point into a stepper.

The given node is assumed to be derived from the command at the top of the current continuation body. No checks are done to enforce this assumption.

◆ stepGetHeaderValidity()

bool P4Tools::P4Testgen::AbstractStepper::stepGetHeaderValidity ( const IR::StateVariable & headerRef )

protected

Transition function for isValid calls.

Parameters

headerRef the header instance whose validity is being queried. Arguments must be either Members or PathExpressions.

Returns: false

◆ stepSetHeaderValidity()

bool P4Tools::P4Testgen::AbstractStepper::stepSetHeaderValidity	(	const IR::StateVariable &	headerRef,
		bool	validity )

protected

Transition function for setValid and setInvalid calls.

Parameters

headerRef	the header instance being set valid or invalid. This is either a Member or a PathExpression.
validity	the validity state being assigned to the header instance.

Returns: false

◆ stepStackPushPopFront()

bool P4Tools::P4Testgen::AbstractStepper::stepStackPushPopFront	(	const IR::Expression *	stackRef,
		const IR::Vector< IR::Argument > *	args,
		bool	isPush = true )

protected

Transition function for push_front/pop_front calls.

Parameters

stackRef	the stack begin push_front/pop_front. This is either a Member or a PathExpression.
args	the list of arguments being passed to method.
isPush	is true for push_front and false otherwise.

Returns: false

◆ stepSymbolicValue()

bool P4Tools::P4Testgen::AbstractStepper::stepSymbolicValue ( const IR::Node * expr )

protected

Transition function for a symbolic value. Expressions in the metalanguage include P4 non-expressions. Because of this, the given node does not necessarily need to be an instance of IR::Expression.

Returns: false

◆ stepToException()

bool P4Tools::P4Testgen::AbstractStepper::stepToException ( Continuation::Exception exception )

protected

Transitions to an exception.

Returns: false

◆ stepToListSubexpr()

bool P4Tools::P4Testgen::AbstractStepper::stepToListSubexpr	(	const IR::BaseListExpression *	subexpr,
		SmallStepEvaluator::Result &	result,
		const ExecutionState &	state,
		std::function< const Continuation::Command(const IR::BaseListExpression *)>	rebuildCmd )

staticprotected

Transitions to a subexpression of the topmost command in the current continuation body. The subexpression is expected to be a ListExpression. This is a specialized version of stepToSubExpr that can be used in contexts that explicitly expect a ListExpression instead of a generic Expression.

Parameters

rebuildCmd Rebuilds the command containing the subexpression by replacing @subexpr with the given list expression.

Returns: false

◆ stepToStructSubexpr()

bool P4Tools::P4Testgen::AbstractStepper::stepToStructSubexpr	(	const IR::StructExpression *	subexpr,
		SmallStepEvaluator::Result &	result,
		const ExecutionState &	state,
		std::function< const Continuation::Command(const IR::StructExpression *)>	rebuildCmd )

staticprotected

See also: stepToListSubexpr.IR::StructExpression differs slightly from IR::BaseListExpression in that the components are IR::NamedExpression instead of just IR::Expression. To keep things simple, and to avoid excessive type casting, these two functions are kept separate.

◆ stepToSubexpr()

bool P4Tools::P4Testgen::AbstractStepper::stepToSubexpr	(	const IR::Expression *	subexpr,
		SmallStepEvaluator::Result &	result,
		const ExecutionState &	state,
		std::function< const Continuation::Command(const Continuation::Parameter *)>	rebuildCmd )

staticprotected

Transitions to a subexpression of the topmost command in the current continuation body.

Parameters

rebuildCmd Rebuilds the command containing the subexpression by replacing @subexpr with the given parameter.

Returns: false

Public Types

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Member Function Documentation

◆ checkMemberInvariant()

◆ declareBaseType()

◆ declareStructLike()

◆ evaluateExpression()

◆ getClassName()

◆ setHeaderValidity()

◆ setTargetUninitialized()

◆ step()

◆ stepGetHeaderValidity()

◆ stepSetHeaderValidity()

◆ stepStackPushPopFront()

◆ stepSymbolicValue()

◆ stepToException()

◆ stepToListSubexpr()

◆ stepToStructSubexpr()

◆ stepToSubexpr()