#include <reachability.h>

Public Member Functions
	ReachabilityEngine (const NodesCallGraph &dcg, std::string reachabilityExpression, bool eliminateAnnotations=false)

const NodesCallGraph &	getDCG ()
	Returns current control flow graph.

ReachabilityResult	next (ReachabilityEngineState *, DCGVertexType)

Protected Member Functions
const IR::Expression *	addCondition (const IR::Expression *prev, DCGVertexType currentState)
	Adds user's condition the a node.

void	addEdge (DCGVertexType vertex, IR::ID vertexName=IR::ID())

void	addTransition (DCGVertexType, const std::unordered_set< DCGVertexType > &)
	Adds transition to engine control flow graph.

void	annotationToStatements (DCGVertexType node, std::unordered_set< DCGVertexType > &s)
	Translates current annotation into set of the parent nodes.

const IR::Expression *	getCondition (DCGVertexType)
	Gets a user's condition from a node.

std::unordered_set< DCGVertexType >	getName (std::string name)
	Translates string into the corresponding nodes.

Static Protected Member Functions
static const IR::Expression *	stringToNode (std::string name)

Detailed Description

The main class to support user input patterns. This class allows to move step-by-step via user's input expression. Syntax for the user's input expressions <behavior> ::= <behavior> ; <behavior> | <behavior> + <behavior> | <name> | <forbidden name> <name> ::= <p4c node name> ['(' <condition> ')'] <forbidden name> ::= ! <p4c node name> <p4c node name> - the name of the MethodCallStatement, P4Action, P4Parser, P4Table, ParserState, P4Control, ParserValueSet, Declaration. <p4c condition> - any conditions p4c in syntax, whcih should be returned by the

Constructor & Destructor Documentation

◆ ReachabilityEngine()

P4::P4Tools::ReachabilityEngine::ReachabilityEngine	(	const NodesCallGraph &	dcg,
		std::string	reachabilityExpression,
		bool	eliminateAnnotations = false )

Default constructor, where dcg is a control flow graph builded by P4ProgramDCGCreator, reachabilityExpression is a user's pattern wrote in the syntax presented above, eliminateAnnotations is true if after detection of the annotations it should to store corresponding parent IR::Node in a reachability engine state.

Member Function Documentation

◆ addEdge()

void P4::P4Tools::ReachabilityEngine::addEdge	(	DCGVertexType	vertex,
		IR::ID	vertexName = IR::ID() )

protected

Adds an edge to the current @vertex in DCG. The edge is a pair (@prev, @vertex).

◆ next()

ReachabilityResult P4::P4Tools::ReachabilityEngine::next	(	ReachabilityEngineState *	state,
		DCGVertexType	next )

Moves the next statement in a engine state. It returns a pair where the first argument is a flag for the possibility of such a movement and the second argument is an condition which should be checked additionally. If engine state is reachable from current node then it returns true. If engine state contain such node then it returns additional condition in case if it was inputed by user and moves engine state to the next state.

◆ stringToNode()

const IR::Expression * P4::P4Tools::ReachabilityEngine::stringToNode ( std::string name )

staticprotected

Translates a string representation into an IR::Expression. Not implemented yet.

Public Member Functions

Protected Member Functions