Represents state of execution after having reached a program point. More...

Inheritance diagram for P4Tools::P4Testgen::ExecutionState:

Classes
class	StackFrame

Public Member Functions
	ExecutionState (ExecutionState &&)=delete
	No move semantics because of constant members. We always need to clone a state.

void	add (const TraceEvent &event)
	Add a new trace event to the state.

void	addTestObject (cstring category, cstring objectLabel, const TestObject *object)

void	appendToEmitBuffer (const IR::Expression *expr)
	Append data to the emit buffer.

void	appendToInputPacket (const IR::Expression *expr)
	Append data to the input packet.

void	appendToPacketBuffer (const IR::Expression *expr)
	Append data to the packet buffer.

ExecutionState &	clone () const override

void	deleteTestObject (cstring category, cstring objectLabel)
	Remove a test object from a category.

void	deleteTestObjectCategory (cstring category)
	Remove a test category entirely.

const IR::Expression *	get (const IR::StateVariable &var) const override

const Continuation::Body &	getBody () const

const IR::StateVariable &	getCurrentParserErrorLabel () const

const IR::Expression *	getEmitBuffer () const

const IR::Expression *	getInputPacket () const

int	getInputPacketCursor () const

int	getInputPacketSize () const

std::optional< const Continuation::Command >	getNextCmd () const

const IR::Expression *	getPacketBuffer () const

int	getPacketBufferSize () const

const std::vector< const IR::Expression * > &	getPathConstraint () const

template<class T >
T	getProperty (cstring propertyName) const

ReachabilityEngineState *	getReachabilityEngineState () const
	Get the current state of the reachability engine.

const std::vector< uint64_t > &	getSelectedBranches () const

const std::stack< std::reference_wrapper< const StackFrame > > &	getStack () const

template<class T >
const T *	getTestObject (cstring category, cstring objectLabel) const

const TestObject *	getTestObject (cstring category, cstring objectLabel, bool checked) const

TestObjectMap	getTestObjectCategory (cstring category) const

const std::vector< std::reference_wrapper< const TraceEvent > > &	getTrace () const

const P4::Coverage::CoverageSet &	getVisited () const

void	handleException (Continuation::Exception e)
	Invokes first handler for e found on the stack.

bool	hasProperty (cstring propertyName) const

bool	isTerminal () const
	Determines whether this state represents the end of an execution.

void	markVisited (const IR::Node *node)
	Checks whether the node has been visited in this state.

ExecutionState &	operator= (ExecutionState &&)=delete

const IR::Expression *	peekPacketBuffer (int amount)

void	popBody ()
	Pops the top element of @body.

void	popContinuation (std::optional< const IR::Node * > argument_opt=std::nullopt)

void	prependToInputPacket (const IR::Expression *expr)
	Prepend data to the input packet.

void	prependToPacketBuffer (const IR::Expression *expr)
	Prepend data to the packet buffer.

void	pushBranchDecision (uint64_t)

void	pushContinuation (const StackFrame &frame)
	Pushes a new frame onto the continuation stack.

void	pushCurrentContinuation (StackFrame::ExceptionHandlers handlers)

void	pushCurrentContinuation (std::optional< const IR::Type * > parameterType_opt=std::nullopt, StackFrame::ExceptionHandlers={})

void	pushPathConstraint (const IR::Expression *e)
	Adds path constraint.

void	replaceBody (const Continuation::Body &body)
	Replaces @body with the given argument.

void	replaceTopBody (const Continuation::Command &cmd)
	Replaces the top element of @body with @cmd.

template<class N >
void	replaceTopBody (const std::vector< const N * > *nodes)

void	replaceTopBody (const std::vector< Continuation::Command > *cmds)

void	replaceTopBody (std::initializer_list< Continuation::Command > cmds)

void	resetEmitBuffer ()
	Reset the emit buffer to zero.

void	resetPacketBuffer ()
	Reset the packet buffer to zero.

void	set (const IR::StateVariable &var, const IR::Expression *value) override

void	setParserErrorLabel (const IR::StateVariable &parserError)
	Set the parser error label to the. More...

void	setProperty (cstring propertyName, Continuation::PropertyValue property)
	Set the property with. More...

void	setReachabilityEngineState (ReachabilityEngineState *newEngineState)
	Update the reachability engine state.

const IR::Expression *	slicePacketBuffer (int amount)

Public Member Functions inherited from P4Tools::AbstractExecutionState
	AbstractExecutionState (AbstractExecutionState &&)=default

	AbstractExecutionState (const IR::P4Program *program)
	Creates an initial execution state for the given program.

void	assignStructLike (const IR::StateVariable &left, const IR::Expression *right)

void	copyIn (const Target &target, const IR::Parameter *internalParam, cstring externalParamName)

void	copyOut (const IR::Parameter *internalParam, cstring externalParamName)

void	declareVariable (const Target &target, const IR::Declaration_Variable &declVar)

bool	exists (const IR::StateVariable &var) const
	Checks whether the given variable exists in the symbolic environment of this state.

const IR::IDeclaration *	findDecl (const IR::Path *path) const
	Looks up a declaration from a path. A BUG occurs if no declaration is found.

const IR::IDeclaration *	findDecl (const IR::PathExpression *pathExpr) const
	Looks up a declaration from a path expression. A BUG occurs if no declaration is found.

const IR::P4Table *	findTable (const IR::Member *member) const

std::vector< IR::StateVariable >	getFlatFields (const IR::StateVariable &parent, std::vector< IR::StateVariable > *validVector=nullptr) const

const NamespaceContext *	getNamespaceContext () const

const IR::P4Action *	getP4Action (const IR::MethodCallExpression *actionExpr) const

const SymbolicEnv &	getSymbolicEnv () const

void	initializeBlockParams (const Target &target, const IR::Type_Declaration typeDecl, const std::vector< cstring > blockParams)

void	initializeStructLike (const Target &target, const IR::StateVariable &targetVar, bool forceTaint)

AbstractExecutionState &	operator= (AbstractExecutionState &&)=delete

void	popNamespace ()
	Exists a namespace of declarations.

void	printSymbolicEnv (std::ostream &out=std::cout) const
	Produce a formatted output of the current symbolic environment.

void	pushNamespace (const IR::INamespace *ns)
	Enters a namespace of declarations.

const IR::Type *	resolveType (const IR::Type *type) const
	Resolves a Type in the current environment.

void	setNamespaceContext (const NamespaceContext *namespaces)
	Replaces the namespace context in the current state with the given context.

void	setStructLike (const IR::StateVariable &targetVar, const IR::StateVariable &sourceVar)
	Set the members of struct-like @target with the values of struct-like @source.

Static Public Member Functions
static ExecutionState &	create (const IR::P4Program *program)

static const IR::SymbolicVariable *	getInputPacketSizeVar ()

static int	getMaxPacketLength ()

Friends
class	Test::SmallStepTest

Additional Inherited Members
Protected Member Functions inherited from P4Tools::AbstractExecutionState
	AbstractExecutionState ()
	Used for debugging and testing.

	AbstractExecutionState (const AbstractExecutionState &)=default
	Execution state needs to be explicitly copied using the clone call..

const IR::Expression *	convertToComplexExpression (const IR::StateVariable &parent) const

AbstractExecutionState &	operator= (const AbstractExecutionState &)=default
	Do not accidentally copy-assign the execution state.

Static Protected Member Functions inherited from P4Tools::AbstractExecutionState
static std::vector< const IR::Expression * >	flattenComplexExpression (const IR::Expression inputExpression, std::vector< const IR::Expression > &flatValids)

Protected Attributes inherited from P4Tools::AbstractExecutionState
SymbolicEnv	env
	The symbolic environment. Maps program variables to their symbolic values.

const NamespaceContext *	namespaces

Detailed Description

Represents state of execution after having reached a program point.

Member Function Documentation

◆ addTestObject()

void P4Tools::P4Testgen::ExecutionState::addTestObject	(	cstring	category,
		cstring	objectLabel,
		const TestObject *	object
	)

Add a test object. Create the category and label, if necessary. Overrides the object label if it already exists in the object map.

◆ clone()

ExecutionState & P4Tools::P4Testgen::ExecutionState::clone ( ) const

overridevirtual

Allocate a new execution state object with the same state as this object. Returns a reference, not a pointer.

Implements P4Tools::AbstractExecutionState.

◆ create()

ExecutionState & P4Tools::P4Testgen::ExecutionState::create ( const IR::P4Program * program )

static

Create a new execution state object from the input program. Returns a reference not a pointer.

◆ get()

const IR::Expression * P4Tools::P4Testgen::ExecutionState::get ( const IR::StateVariable & var ) const

overridevirtual

Returns: the symbolic value of the given state variable.

Implements P4Tools::AbstractExecutionState.

◆ getBody()

const Continuation::Body & P4Tools::P4Testgen::ExecutionState::getBody ( ) const

Returns: the current body.

◆ getCurrentParserErrorLabel()

const IR::StateVariable & P4Tools::P4Testgen::ExecutionState::getCurrentParserErrorLabel ( ) const

Returns: the current parser error label. Throws a BUG if the label is a nullptr.

◆ getEmitBuffer()

const IR::Expression * P4Tools::P4Testgen::ExecutionState::getEmitBuffer ( ) const

Returns: the current emit buffer

◆ getInputPacket()

const IR::Expression * P4Tools::P4Testgen::ExecutionState::getInputPacket ( ) const

Returns: the current version of the packet that is intended as input.

◆ getInputPacketCursor()

int P4Tools::P4Testgen::ExecutionState::getInputPacketCursor ( ) const

Returns: how much of the current input packet has been parsed.

◆ getInputPacketSize()

int P4Tools::P4Testgen::ExecutionState::getInputPacketSize ( ) const

Returns: the current size of the input packet.

◆ getInputPacketSizeVar()

const IR::SymbolicVariable * P4Tools::P4Testgen::ExecutionState::getInputPacketSizeVar ( )

static

Returns: the symbolic constant representing the length of the input to the current parser, in bits.

◆ getMaxPacketLength()

int P4Tools::P4Testgen::ExecutionState::getMaxPacketLength ( )

static

Returns: the maximum length, in bits, of the packet in the current packet buffer. This is the network's MTU.

◆ getNextCmd()

std::optional< const Continuation::Command > P4Tools::P4Testgen::ExecutionState::getNextCmd ( ) const

Returns: the next command to be evaluated, if any.; std::nullopt if the current body is empty.

◆ getPacketBuffer()

const IR::Expression * P4Tools::P4Testgen::ExecutionState::getPacketBuffer ( ) const

Returns: the current packet buffer.

◆ getPacketBufferSize()

int P4Tools::P4Testgen::ExecutionState::getPacketBufferSize ( ) const

Returns: the current size of the packet buffer.

◆ getPathConstraint()

const std::vector< const IR::Expression * > & P4Tools::P4Testgen::ExecutionState::getPathConstraint ( ) const

Returns: list of paths constraints.

◆ getProperty()

template<class T >

T P4Tools::P4Testgen::ExecutionState::getProperty ( cstring propertyName ) const

inline

Returns

the property saved under

propertyName from the stateProperties map. Throws a BUG, If the specified type does not match or the property is not found.

◆ getSelectedBranches()

const std::vector< uint64_t > & P4Tools::P4Testgen::ExecutionState::getSelectedBranches ( ) const

Returns: list of branch decisions leading into this state.

◆ getStack()

const std::stack< std::reference_wrapper< const ExecutionState::StackFrame > > & P4Tools::P4Testgen::ExecutionState::getStack ( ) const

Returns: the current stack.

◆ getTestObject() [1/2]

template<class T >

const T* P4Tools::P4Testgen::ExecutionState::getTestObject	(	cstring	category,
		cstring	objectLabel
	)		const

inline

Returns: the uninterpreted test object using the provided category and object label. If

Parameters

checked is enabled, a BUG is thrown if the object label does not exist. Also casts the test object to the specified type. If the type does not match, a BUG is thrown.

◆ getTestObject() [2/2]

const TestObject * P4Tools::P4Testgen::ExecutionState::getTestObject	(	cstring	category,
		cstring	objectLabel,
		bool	checked
	)		const

Returns: the uninterpreted test object using the provided category and object label. If

Parameters

checked is enabled, a BUG is thrown if the object label does not exist.

◆ getTestObjectCategory()

TestObjectMap P4Tools::P4Testgen::ExecutionState::getTestObjectCategory ( cstring category ) const

Returns: the map of uninterpreted test objects for a specific test category. For example, all the table entries saved under "tableconfigs".

◆ getTrace()

const std::vector< std::reference_wrapper< const TraceEvent > > & P4Tools::P4Testgen::ExecutionState::getTrace ( ) const

Returns: the current event trace.

◆ getVisited()

const P4::Coverage::CoverageSet & P4Tools::P4Testgen::ExecutionState::getVisited ( ) const

Returns: list of all nodes visited before reaching this state.

◆ hasProperty()

bool P4Tools::P4Testgen::ExecutionState::hasProperty ( cstring propertyName ) const

Returns

whether the property with

propertyName exists.

◆ peekPacketBuffer()

const IR::Expression * P4Tools::P4Testgen::ExecutionState::peekPacketBuffer ( int amount )

Peeks ahead into the packet buffer. Works similarly to slicePacketBuffer but does NOT advance the parser cursor or removes content from the packet buffer. However, because functions such as lookahead may still produce a parser error, this function can also enlarge the minimum input packet required.

◆ popContinuation()

void P4Tools::P4Testgen::ExecutionState::popContinuation ( std::optional< const IR::Node * > argument_opt = std::nullopt )

Pops the topmost frame in the stack of continuations. From the popped frame, the continuation (after β reduction) becomes the current body, and the namespace context becomes the current namespace context. A BUG occurs if the continuation stack is empty.

Expressions in the metalanguage include P4 non-expressions. Because of this, the argument (if provided) does not necessarily need to be an instance of IR::Expression.

◆ pushBranchDecision()

void P4Tools::P4Testgen::ExecutionState::pushBranchDecision ( uint64_t bIdx )

Adds branch decision identifier. Must be called for all branches with more than one successor. These branch decision identifiers are then used by track branches and selected (input) branches features.

◆ pushCurrentContinuation() [1/2]

void P4Tools::P4Testgen::ExecutionState::pushCurrentContinuation ( StackFrame::ExceptionHandlers handlers )

Pushes the current body and namespace context as a new frame on the continuation stack. The new frame will have a parameterless continuation, and will use the given set of exception handlers.

◆ pushCurrentContinuation() [2/2]

void P4Tools::P4Testgen::ExecutionState::pushCurrentContinuation	(	std::optional< const IR::Type * >	parameterType_opt = `std::nullopt`,
		StackFrame::ExceptionHandlers	handlers = `{}`
	)

Pushes the current body and namespace context as a new frame on the continuation stack. The new frame will use the given set of exception handlers. If @parameterType_opt is given, then the continuation in the new frame will have a function parameter, with the given type, that is ignored by the body.

◆ replaceTopBody() [1/3]

template<class N >

void P4Tools::P4Testgen::ExecutionState::replaceTopBody ( const std::vector< const N * > * nodes )

inline

A convenience method for the version that takes a vector of commands. Replaces the topmost command in @body with the contents of @nodes. A BUG occurs if @body is empty or if @nodes is empty.

◆ replaceTopBody() [2/3]

void P4Tools::P4Testgen::ExecutionState::replaceTopBody ( const std::vector< Continuation::Command > * cmds )

Replaces the topmost command in @body with the contents of @cmds. A BUG occurs if @body is empty or @cmds is empty.

◆ replaceTopBody() [3/3]

void P4Tools::P4Testgen::ExecutionState::replaceTopBody ( std::initializer_list< Continuation::Command > cmds )

Replaces the topmost command in @body with the contents of @cmds. A BUG occurs if @body is empty or @cmds is empty.

◆ set()

void P4Tools::P4Testgen::ExecutionState::set	(	const IR::StateVariable &	var,
		const IR::Expression *	value
	)

overridevirtual

Sets the symbolic value of the given state variable to the given value. Constant folding is done on the given value before updating the symbolic state.

Implements P4Tools::AbstractExecutionState.

◆ setParserErrorLabel()

void P4Tools::P4Testgen::ExecutionState::setParserErrorLabel ( const IR::StateVariable & parserError )

Set the parser error label to the.

Parameters

parserError.

◆ setProperty()

void P4Tools::P4Testgen::ExecutionState::setProperty	(	cstring	propertyName,
		Continuation::PropertyValue	property
	)

Set the property with.

propertyName to
property.

◆ slicePacketBuffer()

const IR::Expression * P4Tools::P4Testgen::ExecutionState::slicePacketBuffer ( int amount )

Consumes and

Returns: a slice from the available packet buffer. If the buffer is empty, this will produce variables constants that are appended to the input packet. This means we generate packet content as needed. The returned slice is optional in case one just needs to advance.

Classes

Public Member Functions

Static Public Member Functions

Friends

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ addTestObject()

◆ clone()

◆ create()

◆ get()

◆ getBody()

◆ getCurrentParserErrorLabel()

◆ getEmitBuffer()

◆ getInputPacket()

◆ getInputPacketCursor()

◆ getInputPacketSize()

◆ getInputPacketSizeVar()

◆ getMaxPacketLength()

◆ getNextCmd()

◆ getPacketBuffer()

◆ getPacketBufferSize()

◆ getPathConstraint()

◆ getProperty()

◆ getSelectedBranches()

◆ getStack()

◆ getTestObject() [1/2]

◆ getTestObject() [2/2]

◆ getTestObjectCategory()

◆ getTrace()

◆ getVisited()

◆ hasProperty()

◆ peekPacketBuffer()

◆ popContinuation()

◆ pushBranchDecision()

◆ pushCurrentContinuation() [1/2]

◆ pushCurrentContinuation() [2/2]

◆ replaceTopBody() [1/3]

◆ replaceTopBody() [2/3]

◆ replaceTopBody() [3/3]

◆ set()

◆ setParserErrorLabel()

◆ setProperty()

◆ slicePacketBuffer()