P4Tools::P4Testgen::SymbolicExecutor Class Reference

Inheritance diagram for P4Tools::P4Testgen::SymbolicExecutor:

Public Types
using	Branch = SmallStepEvaluator::Branch
using	Callback = std::function<bool(const FinalState &)>
using	StepResult = SmallStepEvaluator::Result

Public Member Functions
	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)
virtual void	runImpl (const Callback &callBack, ExecutionStateReference executionState)=0
bool	updateVisitedNodes (const P4::Coverage::CoverageSet &newNodes)
	Update the set of visited nodes. Returns true if there was an update.

Protected Member Functions
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
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
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

Base abstract class for symbolic execution. It requires the implementation of the run method, and carries the base Branch struct, to be reused in inherited classes. It also holds a default termination method, which can be overridden.

Member Typedef Documentation

Callback

using P4Tools::P4Testgen::SymbolicExecutor::Callback = std::function<bool(const FinalState &)>

Callbacks are invoked when the P4 program terminates. If the callback returns true, execution halts. Otherwise, execution of the P4 program continues on a different random path.

Member Function Documentation

evaluateBranch()

bool P4Tools::P4Testgen::SymbolicExecutor::evaluateBranch ( const SymbolicExecutor::Branch & branch, AbstractSolver & solver )

staticprotected

Take a branch and a solver as input. Compute the branch's path conditions using the solver. Return true if the solver can find a solution and does not time out.

handleTerminalState()

bool P4Tools::P4Testgen::SymbolicExecutor::handleTerminalState ( const Callback & callback, const ExecutionState & terminalState )

protected

Handles processing at the end of a P4 program.

Returns

true if symbolic execution should end; false if symbolic execution should continue on a different path.

popRandomBranch()

SymbolicExecutor::Branch P4Tools::P4Testgen::SymbolicExecutor::popRandomBranch ( std::vector< SymbolicExecutor::Branch > & candidateBranches )

staticprotected

Select a branch at random from the input.

Parameters

candidateBranches.

printCurrentTraceAndBranches()

void P4Tools::P4Testgen::SymbolicExecutor::printCurrentTraceAndBranches	(	std::ostream &	out,
		const ExecutionState &	executionState )

Writes a list of the selected branches into.

Parameters

out.

run()

void P4Tools::P4Testgen::SymbolicExecutor::run ( const Callback & callBack )

virtual

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.

runImpl()

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

pure virtual

Implemented in P4Tools::P4Testgen::DepthFirstSearch, P4Tools::P4Testgen::RandomBacktrack, P4Tools::P4Testgen::SelectedBranches, and P4Tools::P4Testgen::GreedyNodeSelection.