P4C
The P4 Compiler
Loading...
Searching...
No Matches
P4::P4Tools::P4Testgen::DepthFirstSearch Class Reference

#include <depth_first.h>

Inheritance diagram for P4::P4Tools::P4Testgen::DepthFirstSearch:
[legend]

Public Member Functions

 DepthFirstSearch (AbstractSolver &solver, const ProgramInfo &programInfo)
 Constructor for this strategy, considering inheritance.
 
void runImpl (const Callback &callBack, ExecutionStateReference executionState) 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::CoverageSetgetVisitedNodes ()
 Getter to access visitedNodes.
 
SymbolicExecutoroperator= (const SymbolicExecutor &)=delete
 
SymbolicExecutoroperator= (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::CoverageSetcoverableNodes
 Set of all nodes, to be retrieved from programInfo.
 
const ProgramInfoprogramInfo
 Target-specific information about the P4 program.
 
AbstractSolversolver
 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 depth-first 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 the last state from the container of unexplored, remaining branches.

Member Function Documentation

◆ runImpl()

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