Public Types
using	StatOrDeclVector = IR::IndexedVector<IR::StatOrDecl>

Public Member Functions
	ParserSymbolicInterpreter (ParserStructure structure, ReferenceMap refMap, TypeMap *typeMap, bool unroll, bool &wasError)
	constructor

void	addOutOfBound (ParserStateInfo *stateInfo, std::unordered_set< cstring > &newStates, bool checkBefore=true, StatOrDeclVector components=StatOrDeclVector())
	generate call OutOfBound

ParserInfo *	run ()
	running symbolic execution

Public Attributes
bool	hasOutOfboundState

Protected Types
using	EvaluationSelectResult

using	EvaluationStateResult

Protected Member Functions
bool	checkLoops (ParserStateInfo *state) const
	Return true if we have detected a loop we cannot unroll.

bool	equStackVariableMap (const StackVariableMap &l, const StackVariableMap &r) const
	True if both structures are equal.

EvaluationSelectResult	evaluateSelect (ParserStateInfo state, ValueMap valueMap)

EvaluationStateResult	evaluateState (ParserStateInfo *state, std::unordered_set< cstring > &newStates)

const IR::StatOrDecl *	executeStatement (ParserStateInfo state, const IR::StatOrDecl sord, ValueMap *valueMap)

IR::ID	getNewName (ParserStateInfo *state)
	Gets new name for a state.

ValueMap *	initializeVariables ()

ParserStateInfo *	newStateInfo (const ParserStateInfo predecessor, cstring stateName, ValueMap values, size_t index)

bool	reportIfError (const ParserStateInfo state, SymbolicValue value) const
	Return false if an error can be detected statically.

Static Protected Member Functions
static bool	headerValidityChange (const ValueMap before, const ValueMap after)
	True if any header has changed its "validity" bit.

static bool	headerValidityChanged (const SymbolicValue first, const SymbolicValue second)

static cstring	stateChain (const ParserStateInfo *state)

static void	stateChain (const ParserStateInfo *state, std::stringstream &stream)

Protected Attributes
SymbolicValueFactory *	factory

const IR::P4Parser *	parser

ReferenceMap *	refMap

ParserStructure *	structure

ParserInfo *	synthesizedParser

TypeMap *	typeMap

bool	unroll

StatesVisitedMap	visitedStates

bool &	wasError

Friends
class	ParserStateRewriter

Member Typedef Documentation

◆ EvaluationSelectResult

using P4::ParserStructureImpl::ParserSymbolicInterpreter::EvaluationSelectResult

protected

Initial value:

std::pair<std::vector<ParserStateInfo *> *, const IR::Expression *>

◆ EvaluationStateResult

using P4::ParserStructureImpl::ParserSymbolicInterpreter::EvaluationStateResult

protected

Initial value:

std::tuple<std::vector<ParserStateInfo *> *, bool, IR::IndexedVector<IR::StatOrDecl>>

P4::IR::IndexedVector

Definition indexed_vector.h:40

Member Function Documentation

◆ evaluateState()

EvaluationStateResult P4::ParserStructureImpl::ParserSymbolicInterpreter::evaluateState	(	ParserStateInfo *	state,
		std::unordered_set< cstring > &	newStates )

inlineprotected

Generates new state with the help of symbolic execution. If corresponded state was generated previously then it returns nullptr and false.

Parameters

newStates is a set of parsers' names which were genereted.

◆ executeStatement()

const IR::StatOrDecl * P4::ParserStructureImpl::ParserSymbolicInterpreter::executeStatement	(	ParserStateInfo *	state,
		const IR::StatOrDecl *	sord,
		ValueMap *	valueMap )

inlineprotected

Executes symbolically the specified statement. Returns pointer to generated statement if execution completes successfully, and 'nullptr' if an error occurred.

Public Types

Public Member Functions

Public Attributes

Protected Types

Protected Member Functions

Static Protected Member Functions