Implements small-step operational semantics for expressions. More...

Inheritance diagram for P4Tools::P4Testgen::ExprStepper:

[legend]

Classes
struct	PacketCursorAdvanceInfo

Public Member Functions
	ExprStepper (const ExprStepper &)=default

	ExprStepper (ExecutionState &state, AbstractSolver &solver, const ProgramInfo &programInfo)

	ExprStepper (ExprStepper &&)=default

ExprStepper &	operator= (const ExprStepper &)=delete

ExprStepper &	operator= (ExprStepper &&)=delete

bool	preorder (const IR::ArrayIndex *arr) override

bool	preorder (const IR::BaseListExpression *listExpression) override

bool	preorder (const IR::BoolLiteral *boolLiteral) override

bool	preorder (const IR::Constant *constant) override

bool	preorder (const IR::Member *member) override

bool	preorder (const IR::MethodCallExpression *call) override

bool	preorder (const IR::Mux *mux) override

bool	preorder (const IR::Operation_Binary *binary) override

bool	preorder (const IR::Operation_Unary *unary) override

bool	preorder (const IR::P4Table *table) override

bool	preorder (const IR::P4ValueSet *valueSet) override

bool	preorder (const IR::PathExpression *pathExpression) override

bool	preorder (const IR::SelectExpression *selectExpression) override

bool	preorder (const IR::Slice *slice) override

bool	preorder (const IR::StructExpression *structExpression) override

Public Member Functions inherited from P4Tools::P4Testgen::AbstractStepper
	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
virtual PacketCursorAdvanceInfo	calculateAdvanceExpression (const ExecutionState &state, const IR::Expression advanceExpr, const IR::Expression restrictions) const

virtual PacketCursorAdvanceInfo	calculateSuccessfulParserAdvance (const ExecutionState &state, int advanceSize) const

void	evalActionCall (const IR::P4Action action, const IR::MethodCallExpression call)

virtual void	evalExternMethodCall (const IR::MethodCallExpression call, const IR::Expression receiver, IR::ID name, const IR::Vector< IR::Argument > *args, ExecutionState &state)

virtual void	evalInternalExternMethodCall (const IR::MethodCallExpression call, const IR::Expression receiver, IR::ID name, const IR::Vector< IR::Argument > *args, const ExecutionState &state)

void	generateCopyIn (ExecutionState &nextState, const IR::StateVariable &targetPath, const IR::StateVariable &srcPath, cstring dir, bool forceTaint) const
	TODO: Consolidate this into the copy_in_out extern.

void	handleHitMissActionRun (const IR::Member *member)

bool	resolveMethodCallArguments (const IR::MethodCallExpression *call)

virtual void	stepNoMatch (std::string traceLog, const IR::Expression *condition=nullptr)

Protected Member Functions inherited from P4Tools::P4Testgen::AbstractStepper
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 std::vector< std::pair< IR::StateVariable, const IR::Expression * > >	setFields (ExecutionState &nextState, const std::vector< IR::StateVariable > &flatFields, int varBitFieldSize)

Static Protected Member Functions inherited from P4Tools::P4Testgen::AbstractStepper
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)

Friends
class	ExtractUtils
	Extract utils may access some protected members of the expression stepper.

class	TableStepper
	We delegate evaluation to the TableStepper, which needs to access protected members.

Additional Inherited Members
Public Types inherited from P4Tools::P4Testgen::AbstractStepper
using	Branch = SmallStepEvaluator::Branch

using	Result = SmallStepEvaluator::Result

Protected Attributes inherited from P4Tools::P4Testgen::AbstractStepper
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

Implements small-step operational semantics for expressions.

Class Documentation

◆ P4Tools::P4Testgen::ExprStepper::PacketCursorAdvanceInfo

struct P4Tools::P4Testgen::ExprStepper::PacketCursorAdvanceInfo

Contains information that is useful for externs that advance the parser cursor. For example, advance, extract, or lookahead.

Class Members
const Expression *	advanceCond	The condition that needs to be satisfied to successfully advance the parser cursor.
const Expression *	advanceFailCond	The condition that needs to be satisfied for the advance/extract to be rejected.
int	advanceFailSize	Specifies at what point the parser cursor advancement will fail.
int	advanceSize	How much the parser cursor will be advanced in a successful parsing case.

Member Function Documentation

◆ calculateAdvanceExpression()

ExprStepper::PacketCursorAdvanceInfo P4Tools::P4Testgen::ExprStepper::calculateAdvanceExpression	(	const ExecutionState &	state,
		const IR::Expression *	advanceExpr,
		const IR::Expression *	restrictions ) const

protectedvirtual

Calculates the conditions that need to be satisfied for a successful parser advance. This assumes that the advance amount is a run-time value. We need to pick a satisfying value assignment for a reject or advance of the parser. Targets may override this function with custom behavior.

◆ calculateSuccessfulParserAdvance()

ExprStepper::PacketCursorAdvanceInfo P4Tools::P4Testgen::ExprStepper::calculateSuccessfulParserAdvance	(	const ExecutionState &	state,
		int	advanceSize ) const

protectedvirtual

Calculates the conditions that need to be satisfied for a successful parser advance. This assumes that the advance amount is known already and a compile-time constant. Targets may override this function with custom behavior.

◆ evalActionCall()

void P4Tools::P4Testgen::ExprStepper::evalActionCall	(	const IR::P4Action *	action,
		const IR::MethodCallExpression *	call )

protected

Evaluates a call to an action. This usually only happens when a table is invoked or when action is directly invoked from a control. In other cases, actions should be inlined. When the action call is evaluated, we use symbolic variables to pass arguments across execution boundaries. These variables persist until the end of program execution.

Parameters

action	the action declaration that is being referenced.
call	the actual method call containing the arguments.

◆ evalExternMethodCall()

void P4Tools::P4Testgen::ExprStepper::evalExternMethodCall	(	const IR::MethodCallExpression *	call,
		const IR::Expression *	receiver,
		IR::ID	name,
		const IR::Vector< IR::Argument > *	args,
		ExecutionState &	state )

protectedvirtual

Evaluates a call to an extern method. Upon return, the given result will be augmented with the successor states resulting from evaluating the call.

Parameters

call	the original method call expression, can be used for stepInto calls.
receiver	a symbolic value representing the object on which the method is being called.
name	the name of the method being called.
args	the list of arguments being passed to method.
state	the state in which the call is being made, with the call at the top of the current continuation body. TODO(fruffy): Move this call out of the expression stepper. The location is confusing.

Iterate over all the fields that need to be set.

Reimplemented in P4Tools::P4Testgen::Bmv2::Bmv2V1ModelExprStepper, P4Tools::P4Testgen::EBPF::EBPFExprStepper, P4Tools::P4Testgen::Pna::PnaDpdkExprStepper, and P4Tools::P4Testgen::Pna::SharedPnaExprStepper.

◆ evalInternalExternMethodCall()

void P4Tools::P4Testgen::ExprStepper::evalInternalExternMethodCall	(	const IR::MethodCallExpression *	call,
		const IR::Expression *	receiver,
		IR::ID	name,
		const IR::Vector< IR::Argument > *	args,
		const ExecutionState &	state )

protectedvirtual

Evaluates a call to an extern method that only exists in the interpreter. These are helper functions used to execute custom operations and specific control flow. They do not exist as P4 code or call.

Parameters

call	the original method call expression, can be used for stepInto calls.
receiver	a symbolic value representing the object on which the method is being called.
name	the name of the method being called.
args	the list of arguments being passed to method.
state	the state in which the call is being made, with the call at the top of the current continuation body. TODO(fruffy): Move this call out of the expression stepper. The location is confusing.

◆ handleHitMissActionRun()

void P4Tools::P4Testgen::ExprStepper::handleHitMissActionRun ( const IR::Member * member )

protected

This function call is used in member expressions to cleanly resolve hit, miss, and action run expressions. These are return values of a table.apply() call, and fairly special in P4. We have to use this rewrite to execute the table, and then return the corresponding values for hit, miss and action_run after that.

◆ preorder()

bool P4Tools::P4Testgen::ExprStepper::preorder ( const IR::P4ValueSet * valueSet )

override

This is a special function that handles the case where structure include P4ValueSet. Returns an updated structure, replacing P4ValueSet with a list of P4ValueSet components, splitting the list into separate keys if possible

◆ resolveMethodCallArguments()

bool P4Tools::P4Testgen::ExprStepper::resolveMethodCallArguments ( const IR::MethodCallExpression * call )

protected

Resolve all arguments to the method call by stepping into each argument that is not yet symbolic or a pure reference (represented as Out direction).

Returns: false when an argument needs to be resolved, true otherwise.

◆ setFields()

std::vector< std::pair< IR::StateVariable, const IR::Expression * > > P4Tools::P4Testgen::ExprStepper::setFields	(	ExecutionState &	nextState,
		const std::vector< IR::StateVariable > &	flatFields,
		int	varBitFieldSize )

staticprotected

Iterate over the fields in

Parameters

flatFields	and set the corresponding values in
nextState.	If there is a varbit, assign the
varbitFieldSize	as size to it.

Returns: the list of members and their assigned values.

◆ stepNoMatch()

void P4Tools::P4Testgen::ExprStepper::stepNoMatch	(	std::string	traceLog,
		const IR::Expression *	condition = nullptr )

protectedvirtual

Takes a step to reflect a "select" expression failing to match. If condition is given, this will create a new state that is guarded by the given condition. The default implementation raises Continuation::Exception::NoMatch.

Classes

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Friends

Additional Inherited Members

Detailed Description

Class Documentation

◆ P4Tools::P4Testgen::ExprStepper::PacketCursorAdvanceInfo

Member Function Documentation

◆ calculateAdvanceExpression()

◆ calculateSuccessfulParserAdvance()

◆ evalActionCall()

◆ evalExternMethodCall()

◆ evalInternalExternMethodCall()

◆ handleHitMissActionRun()

◆ preorder()

◆ resolveMethodCallArguments()

◆ setFields()

◆ stepNoMatch()