P4Tools::P4Testgen::CmdStepper Class Reference

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

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

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)

Additional Inherited Members
Public Types inherited from P4Tools::P4Testgen::AbstractStepper
using	Branch = SmallStepEvaluator::Branch
using	Result = SmallStepEvaluator::Result
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.

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.