P4Tools::P4Testgen::RandomBacktrack Class Reference

#include <random_backtrack.h>

Inheritance diagram for P4Tools::P4Testgen::RandomBacktrack:

Public Member Functions
	RandomBacktrack (AbstractSolver &solver, const ProgramInfo &programInfo)
	Constructor for this strategy, considering inheritance.
void	runImpl (const Callback &callBack, ExecutionStateReference executionState) override
Public Member Functions inherited from 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 P4Tools::P4Testgen::SymbolicExecutor
using	Branch = SmallStepEvaluator::Branch
using	Callback = std::function<bool(const FinalState &)>
using	StepResult = SmallStepEvaluator::Result
Protected Member Functions inherited from 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 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 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

A simple random traversal strategy. If this selection strategy hits a branch point, it will choose a path at random and continue execution downwards. Once the selection strategy has hit a terminal state, it will pop a random state from the container of unexplored, remaining branches.

Member Function Documentation

runImpl()

void P4Tools::P4Testgen::RandomBacktrack::runImpl ( const Callback & callBack, ExecutionStateReference executionState )

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 P4Tools::P4Testgen::SymbolicExecutor.