#include <abstract_stepper.h>

Inheritance diagram for P4Tools::P4Testgen::AbstractStepper:

Public Types
using	Branch = SmallStepEvaluator::Branch

using	Result = SmallStepEvaluator::Result

Public Types inherited from Visitor
typedef Visitor_Context	Context

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 *)

Public Member Functions inherited from Inspector
const IR::Node *	apply_visitor (const IR::Node , const char name=0) override

profile_t	init_apply (const IR::Node *root) override

virtual void	loop_revisit (const IR::Node *)

virtual void	postorder (const IR::Node *)

virtual void	revisit (const IR::Node *)

void	revisit_visited ()

bool	visit_in_progress (const IR::Node *n) const

void	visitAgain () const override

void	visitOnce () const override

Public Member Functions inherited from Visitor
virtual bool	check_global (cstring)

virtual void	clear_globals ()

virtual Visitor *	clone () const

virtual ControlFlowVisitor *	controlFlowVisitor ()

virtual void	end_apply ()

virtual void	end_apply (const IR::Node *root)

virtual void	erase_global (cstring)

template<class T >
const T *	findContext () const

template<class T >
const T *	findContext (const Context *&c) const

template<class T >
const T *	findOrigCtxt () const

template<class T >
const T *	findOrigCtxt (const Context *&c) const

virtual Visitor &	flow_clone ()

virtual void	flow_merge (Visitor &)

virtual bool	flow_merge_closure (Visitor &)

virtual void	flow_merge_global_from (cstring)

virtual void	flow_merge_global_to (cstring)

const Context *	getChildContext () const

int	getChildrenVisited () const

const Context *	getContext () const

int	getContextDepth () const

const IR::Node *	getCurrentNode () const

template<class T >
const T *	getCurrentNode () const

const IR::Node *	getOriginal () const

template<class T >
const T *	getOriginal () const

template<class T >
const T *	getParent () const

virtual bool	has_flow_joins () const

profile_t	init_apply (const IR::Node root, const Context parent_context)

bool	isInContext (const IR::Node *n) const

virtual const char *	name () const

template<class T >
void	parallel_visit (const IR::Vector< T > &v, const char *name, int cidx)

template<class T >
void	parallel_visit (const IR::Vector< T > &v, const char *name=0)

template<class T >
void	parallel_visit (IR::Vector< T > &v, const char *name, int cidx)

template<class T >
void	parallel_visit (IR::Vector< T > &v, const char *name=0)

void	print_context () const

const Visitor &	setCalledBy (const Visitor *visitor)

void	setName (const char *name)

void	visit (const IR::Node &n, const char *name, int cidx)

void	visit (const IR::Node &n, const char *name=0)

void	visit (const IR::Node &n, const char name, int cidx)

void	visit (const IR::Node &n, const char name=0)

void	visit (const IR::Node const &n, const char name, int cidx)

void	visit (const IR::Node const &n, const char name=0)

void	visit (IR::Node &n, const char *name, int cidx)

void	visit (IR::Node &n, const char *name=0)

void	visit (IR::Node &, const char =0, int=0)

template<class T , typename = std::enable_if_t<Util::has_SourceInfo_v<T>>, class... Args>
void	warn (const int kind, const char *format, const T &node, Args &&...args)
	The const ref variant of the above.

template<class T , typename = std::enable_if_t<Util::has_SourceInfo_v<T>>, class... Args>
void	warn (const int kind, const char format, const T node, Args &&...args)

bool	warning_enabled (int warning_kind) const

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)

Protected Member Functions inherited from Visitor
virtual void	init_join_flows (const IR::Node *)

virtual bool	join_flows (const IR::Node *)

virtual void	post_join_flows (const IR::Node , const IR::Node )

void	visit_children (const IR::Node *, std::function< void()> fn)

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.

Protected Attributes inherited from Visitor
bool	dontForwardChildrenBeforePreorder = false

bool	joinFlows = false

bool	visitDagOnce = true

Additional Inherited Members
Static Public Member Functions inherited from Visitor
static cstring	demangle (const char *)

static bool	warning_enabled (const Visitor *visitor, int warning_kind)

Public Attributes inherited from Visitor
const Visitor *	called_by = nullptr

cstring	internalName

SplitFlowVisit_base *&	split_link

SplitFlowVisit_base *	split_link_mem = nullptr

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.

◆ preorder()

bool P4Tools::P4Testgen::AbstractStepper::preorder ( const IR::Node * node )

overridevirtual

Provides generic handling of unsupported nodes.

Reimplemented from Inspector.

◆ 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

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ checkMemberInvariant()

◆ declareBaseType()

◆ declareStructLike()

◆ evaluateExpression()

◆ getClassName()

◆ preorder()

◆ setHeaderValidity()

◆ setTargetUninitialized()

◆ step()

◆ stepGetHeaderValidity()

◆ stepSetHeaderValidity()

◆ stepStackPushPopFront()

◆ stepSymbolicValue()

◆ stepToException()

◆ stepToListSubexpr()

◆ stepToStructSubexpr()

◆ stepToSubexpr()