P4::P4Tools::P4Testgen::GreedyNodeSelection Class Reference

#include <greedy_node_cov.h>

Inheritance diagram for P4::P4Tools::P4Testgen::GreedyNodeSelection:

Public Member Functions
	GreedyNodeSelection (AbstractSolver &solver, const ProgramInfo &programInfo)
	Constructor for this strategy, considering inheritance.
void	runImpl (const Callback &callBack, ExecutionStateReference state) override
Public Member Functions inherited from P4::P4Tools::P4Testgen::SymbolicExecutor
	SymbolicExecutor (AbstractSolver &solver, const ProgramInfo &programInfo)
	SymbolicExecutor (const SymbolicExecutor &)=default
	SymbolicExecutor (SymbolicExecutor &&)=delete
const P4::Coverage::CoverageSet &	getVisitedNodes ()
	Getter to access visitedNodes.
SymbolicExecutor &	operator= (const SymbolicExecutor &)=delete
SymbolicExecutor &	operator= (SymbolicExecutor &&)=delete
void	printCurrentTraceAndBranches (std::ostream &out, const ExecutionState &executionState)
	Writes a list of the selected branches into.
virtual void	run (const Callback &callBack)
bool	updateVisitedNodes (const P4::Coverage::CoverageSet &newNodes)
	Update the set of visited nodes. Returns true if there was an update.

Additional Inherited Members
Public Types inherited from P4::P4Tools::P4Testgen::SymbolicExecutor
using	Branch = SmallStepEvaluator::Branch
using	Callback = std::function<bool(const FinalState &)>
using	StepResult = SmallStepEvaluator::Result
Protected Member Functions inherited from P4::P4Tools::P4Testgen::SymbolicExecutor
bool	handleTerminalState (const Callback &callback, const ExecutionState &terminalState)
StepResult	step (ExecutionState &state)
	Take one step in the program and return list of possible branches.
Static Protected Member Functions inherited from P4::P4Tools::P4Testgen::SymbolicExecutor
static bool	evaluateBranch (const SymbolicExecutor::Branch &branch, AbstractSolver &solver)
static SymbolicExecutor::Branch	popRandomBranch (std::vector< SymbolicExecutor::Branch > &candidateBranches)
	Select a branch at random from the input.
Protected Attributes inherited from P4::P4Tools::P4Testgen::SymbolicExecutor
const P4::Coverage::CoverageSet &	coverableNodes
	Set of all nodes, to be retrieved from programInfo.
const ProgramInfo &	programInfo
	Target-specific information about the P4 program.
AbstractSolver &	solver
	The SMT solver backing this executor.
P4::Coverage::CoverageSet	visitedNodes
	Set of all nodes executed in any testcase that has been outputted.

Detailed Description

Greedy path selection strategy, which, at branch points, picks the first execution state which has covered or potentially will cover program nodes which have not been visited yet. Potential nodes are computed using the CoverableNodesScanner visitor, which collects nodes in the top-level statement of the execution state. These nodes are latent because execution is not guaranteed. They may be guarded by an if condition or select expression. If the strategy does not find a new statement, it falls back to random. Similarly, if the strategy cycles without a test for a specific threshold, it will fall back to random. This is to prevent getting caught in a parser cycle.

Member Function Documentation

runImpl()

void P4::P4Tools::P4Testgen::GreedyNodeSelection::runImpl ( const Callback & callBack, ExecutionStateReference state )

overridevirtual

Executes the P4 program along a randomly chosen path. When the program terminates, the given callback is invoked. If the callback returns true, then the executor terminates. Otherwise, execution of the P4 program continues on a different random path.

Implements P4::P4Tools::P4Testgen::SymbolicExecutor.