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

#include <cmd_stepper.h>

Inheritance diagram for P4Tools::P4Testgen::CmdStepper:

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

bool	preorder (const IR::AssignmentStatement *assign) override

bool	preorder (const IR::BlockStatement *block) override

bool	preorder (const IR::EmptyStatement *empty) override

bool	preorder (const IR::ExitStatement *e) override

bool	preorder (const IR::IfStatement *ifStatement) override

bool	preorder (const IR::MethodCallStatement *methodCallStatement) override

bool	preorder (const IR::P4Control *p4control) override

bool	preorder (const IR::P4Parser *p4parser) override

bool	preorder (const IR::P4Program *program) override

bool	preorder (const IR::ParserState *parserState) override

bool	preorder (const IR::SwitchStatement *switchStatement) 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 *)

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
virtual std::map< Continuation::Exception, Continuation >	getExceptionHandlers (const IR::P4Parser *parser, Continuation::Body normalContinuation, const ExecutionState &state) const =0

virtual void	initializeTargetEnvironment (ExecutionState &state) const =0

const Constraint *	startParser (const IR::P4Parser *parser, ExecutionState &state)

virtual std::optional< const Constraint * >	startParserImpl (const IR::P4Parser *parser, ExecutionState &state) const =0

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)

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)

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

using	Result = SmallStepEvaluator::Result

Public Types inherited from Visitor
typedef Visitor_Context	Context

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

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)

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.

Protected Attributes inherited from Visitor
bool	dontForwardChildrenBeforePreorder = false

bool	joinFlows = false

bool	visitDagOnce = true

Detailed Description

Implements small-step operational semantics for commands.

Member Function Documentation

◆ getExceptionHandlers()

virtual std::map< Continuation::Exception, Continuation > P4Tools::P4Testgen::CmdStepper::getExceptionHandlers	(	const IR::P4Parser *	parser,
		Continuation::Body	normalContinuation,
		const ExecutionState &	state ) const

protectedpure virtual

Provides exception-handler implementations for the given parser.

Parameters

normalContinuation is the continuation that would be executed if the parser finishes normally.

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

◆ initializeTargetEnvironment()

virtual void P4Tools::P4Testgen::CmdStepper::initializeTargetEnvironment ( ExecutionState & state ) const

protectedpure virtual

Initializes variables and adds constraints for the program initialization, which is target specific.

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

◆ preorder() [1/2]

bool P4Tools::P4Testgen::CmdStepper::preorder ( const IR::P4Program * program )

override

If the the vector of permitted port ranges is not empty, set the restrictions on the possible input port.

◆ preorder() [2/2]

bool P4Tools::P4Testgen::CmdStepper::preorder ( const IR::SwitchStatement * switchStatement )

override

Get the action list associated with this switch/case.

◆ startParser()

const Constraint * P4Tools::P4Testgen::CmdStepper::startParser	(	const IR::P4Parser *	parser,
		ExecutionState &	state )

protected

Initializes the given state for entry into the given parser.

Returns: constraints for associating packet data with symbolic state.

◆ startParserImpl()

virtual std::optional< const Constraint * > P4Tools::P4Testgen::CmdStepper::startParserImpl	(	const IR::P4Parser *	parser,
		ExecutionState &	state ) const

protectedpure virtual

See also: startParser. Implementations can assume that the parser has been registered, and the cursor position has been initialized.

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

Public Member Functions

Protected Member Functions

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ getExceptionHandlers()

◆ initializeTargetEnvironment()

◆ preorder() [1/2]

◆ preorder() [2/2]

◆ startParser()

◆ startParserImpl()