P4Tools::P4Testgen::FinalState Class Reference

Represents the final state after execution. More...

#include <final_state.h>

Public Member Functions
	FinalState (AbstractSolver &solver, const ExecutionState &finalState)
	FinalState (AbstractSolver &solver, const ExecutionState &finalState, const Model &finalModel)
	This constructor takes the input model as is and does not invoke processModel().
std::optional< std::reference_wrapper< const FinalState > >	computeConcolicState (const ConcolicVariableMap &resolvedConcolicVariables) const
const ExecutionState *	getExecutionState () const
const Model &	getFinalModel () const
AbstractSolver &	getSolver () const
const std::vector< std::reference_wrapper< const TraceEvent > > *	getTraces () const
const P4::Coverage::CoverageSet &	getVisited () const

Detailed Description

Represents the final state after execution.

Constructor & Destructor Documentation

FinalState()

P4Tools::P4Testgen::FinalState::FinalState	(	AbstractSolver &	solver,
		const ExecutionState &	finalState )

This constructor invokes processModel() to produce the model based on the solver and the executionState.

Member Function Documentation

computeConcolicState()

std::optional< std::reference_wrapper< const FinalState > > P4Tools::P4Testgen::FinalState::computeConcolicState ( const ConcolicVariableMap & resolvedConcolicVariables ) const

nodiscard

If there are concolic variables in the program, compute a new final state by rerunning the solver on the concolic assignments. If the concolic assignment is not satisfiable, return std::nullopt. Otherwise, create a new final state with the new assignment. IMPORTANT: Some variables in this final state may have been added in post, e.g., the payload size. If the concolic variables do not recompute these variables, the model will simply copy these variables over manually to the newly generated model.

Transfer any derived variables from that are missing in this model. Do NOT update any variables that already exist.

getExecutionState()

const ExecutionState * P4Tools::P4Testgen::FinalState::getExecutionState ( ) const

nodiscard

Returns

the execution state of this final state.

getFinalModel()

const Model & P4Tools::P4Testgen::FinalState::getFinalModel ( ) const

nodiscard

Returns

the model after it was augmented by completions from the symbolic environment.

getSolver()

AbstractSolver & P4Tools::P4Testgen::FinalState::getSolver ( ) const

nodiscard

Returns

the solver associated with this final state.

getTraces()

const std::vector< std::reference_wrapper< const TraceEvent > > * P4Tools::P4Testgen::FinalState::getTraces ( ) const

nodiscard

Returns

the computed traces of this final state.

getVisited()

const P4::Coverage::CoverageSet & P4Tools::P4Testgen::FinalState::getVisited ( ) const

nodiscard

Returns

the list of visited nodes of this state.