P4Tools::P4Testgen::ExecutionState Class Reference

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

#include <execution_state.h>

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.
void	setProperty (cstring propertyName, Continuation::PropertyValue property)
	Set the property with.
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

nodiscardoverridevirtual

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 )

staticnodiscard

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

nodiscardoverridevirtual

Returns

the symbolic value of the given state variable.

Implements P4Tools::AbstractExecutionState.

getBody()

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

nodiscard

Returns

the current body.

getCurrentParserErrorLabel()

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

nodiscard

Returns

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

getEmitBuffer()

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

nodiscard

Returns

the current emit buffer

getInputPacket()

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

nodiscard

Returns

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

getInputPacketCursor()

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

nodiscard

Returns

how much of the current input packet has been parsed.

getInputPacketSize()

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

nodiscard

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

staticnodiscard

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

nodiscard

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

nodiscard

Returns

the current packet buffer.

getPacketBufferSize()

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

nodiscard

Returns

the current size of the packet buffer.

getPathConstraint()

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

nodiscard

Returns

list of paths constraints.

getProperty()

template<class T >

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

inlinenodiscard

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

nodiscard

Returns

list of branch decisions leading into this state.

getStack()

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

nodiscard

Returns

the current stack.

getTestObject() [1/2]

template<class T >

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

inlinenodiscard

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

nodiscard

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

nodiscard

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

nodiscard

Returns

the current event trace.

getVisited()

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

nodiscard

Returns

list of all nodes visited before reaching this state.

hasProperty()

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

nodiscard

Returns

whether the property with

• propertyName exists.

peekPacketBuffer()

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

nodiscard

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.