#include <model.h>

Public Types
using	ExpressionMap = std::map<const IR::Expression , const IR::Literal >

Public Member Functions
	Model (const Model &)=default

	Model (Model &&)=default

	Model (SymbolicMapping symbolicMap)
	A model is initialized with a symbolic map. Usually, these are derived from the solver.

const IR::Literal *	evaluate (const IR::Expression expr, bool doComplete, ExpressionMap resolvedExpressions=nullptr) const

const IR::BaseListExpression *	evaluateListExpr (const IR::BaseListExpression listExpr, bool doComplete, ExpressionMap resolvedExpressions=nullptr) const

const IR::StructExpression *	evaluateStructExpr (const IR::StructExpression structExpr, bool doComplete, ExpressionMap resolvedExpressions=nullptr) const

const IR::Expression *	get (const IR::SymbolicVariable *var, bool checked) const

const SymbolicMapping &	getSymbolicMap () const

void	mergeMap (const SymbolicMapping &sourceMap)
	Merge a sumbolic map into this model, do NOT override existing values.

Model &	operator= (const Model &)=default

Model &	operator= (Model &&)=default

void	set (const IR::SymbolicVariable var, const IR::Expression val)

Detailed Description

Represents a solution found by the solver. A model is a concretized form of a symbolic environment. All the expressions in a Model must be of type IR::Literal.

Member Function Documentation

◆ evaluate()

const IR::Literal * P4::P4Tools::Model::evaluate	(	const IR::Expression *	expr,
		bool	doComplete,
		ExpressionMap *	resolvedExpressions = nullptr ) const

Evaluates a P4 expression in the context of this model.

A BUG occurs if the given expression refers to a variable that is not bound by this model. If the input list

Parameters

resolvedExpressions is not null, we also collect the resolved value of this expression.

◆ get()

const IR::Expression * P4::P4Tools::Model::get	(	const IR::SymbolicVariable *	var,
		bool	checked ) const

nodiscard

Tries to retrieve

Parameters

var	from the model. If
checked	is true, this function throws a BUG if the variable can not be found. Otherwise, it returns a nullptr.

◆ getSymbolicMap()

const SymbolicMapping & P4::P4Tools::Model::getSymbolicMap ( ) const

nodiscard

Returns: the symbolic map contained within this model.

◆ set()

void P4::P4Tools::Model::set	(	const IR::SymbolicVariable *	var,
		const IR::Expression *	val )

Set (and possibly override) a symbolic variable in the model. This is for example useful for payload calculation or concolic execution after we have reached a leaf state.