#include <symbolic_executor.h>

Inheritance diagram for P4::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 P4::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 P4::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 P4::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 P4::P4Tools::P4Testgen::SymbolicExecutor::popRandomBranch ( std::vector< SymbolicExecutor::Branch > & candidateBranches )

staticprotected

Select a branch at random from the input.

Parameters

candidateBranches.

◆ printCurrentTraceAndBranches()

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

Writes a list of the selected branches into.

Parameters

out.

◆ run()

void P4::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 P4::P4Tools::P4Testgen::SymbolicExecutor::runImpl	(	const Callback &	callBack,
		ExecutionStateReference	executionState )

pure virtual

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

Public Types

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Protected Attributes