The interface offered by a domain, allows code to manipulate domains without knowing their exact type. More...

#include <ai_domain.h>

Inheritance diagram for ai_domain_baset:

Public Types
typedef goto_programt::const_targett	locationt

typedef ai_history_baset::trace_ptrt	trace_ptrt

Public Member Functions
virtual	~ai_domain_baset ()

virtual void	transform (const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt to, ai_baset &ai, const namespacet &ns)=0
	how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable) More...

virtual void	output (std::ostream &, const ai_baset &, const namespacet &) const

virtual jsont	output_json (const ai_baset &ai, const namespacet &ns) const

virtual xmlt	output_xml (const ai_baset &ai, const namespacet &ns) const

virtual void	make_bottom ()=0
	no states More...

virtual void	make_top ()=0
	all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it. More...

virtual void	make_entry ()
	Make this domain a reasonable entry-point state For most domains top is sufficient. More...

virtual bool	is_bottom () const =0

virtual bool	is_top () const =0

virtual bool	ai_simplify (exprt &condition, const namespacet &) const
	also add More...

virtual bool	ai_simplify_lhs (exprt &condition, const namespacet &ns) const
	Simplifies the expression but keeps it as an l-value. More...

virtual exprt	to_predicate (void) const
	Gives a Boolean condition that is true for all values represented by the domain. More...

Protected Member Functions
	ai_domain_baset ()
	The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface. More...

	ai_domain_baset (const ai_domain_baset &old)
	A copy constructor is part of the domain interface. More...

Detailed Description

The interface offered by a domain, allows code to manipulate domains without knowing their exact type.

Derive from this to implement domains.

Definition at line 53 of file ai_domain.h.

Member Typedef Documentation

◆ locationt

typedef goto_programt::const_targett ai_domain_baset::locationt

Definition at line 72 of file ai_domain.h.

◆ trace_ptrt

typedef ai_history_baset::trace_ptrt ai_domain_baset::trace_ptrt

Definition at line 73 of file ai_domain.h.

Constructor & Destructor Documentation

◆ ai_domain_baset() [1/2]

ai_domain_baset::ai_domain_baset ( )

inlineprotected

The constructor is expected to produce 'false' or 'bottom' A default constructor is not part of the domain interface.

Definition at line 58 of file ai_domain.h.

◆ ai_domain_baset() [2/2]

ai_domain_baset::ai_domain_baset ( const ai_domain_baset & old )

inlineprotected

A copy constructor is part of the domain interface.

Definition at line 63 of file ai_domain.h.

◆ ~ai_domain_baset()

virtual ai_domain_baset::~ai_domain_baset ( )

inlinevirtual

Definition at line 68 of file ai_domain.h.

Member Function Documentation

◆ ai_simplify()

virtual bool ai_domain_baset::ai_simplify	(	exprt &	condition,
		const namespacet &
	)		const

inlinevirtual

also add

bool merge(const T &b, locationt from, locationt to); or bool merge(const T &b, trace_ptrt from, trace_ptrt to);

This computes the join between "this" and "b". Return true if "this" has changed. In the usual case, "b" is the updated state after "from" and "this" is the state before "to".

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") This method allows an expression to be simplified / evaluated using the current state. It is used to evaluate assertions and in program simplification return true if unchanged

Reimplemented in variable_sensitivity_domaint, interval_domaint, and constant_propagator_domaint.

Definition at line 149 of file ai_domain.h.

◆ ai_simplify_lhs()

bool ai_domain_baset::ai_simplify_lhs	(	exprt &	condition,
		const namespacet &	ns
	)		const

virtual

Simplifies the expression but keeps it as an l-value.

Use the information in the domain to simplify the expression on the LHS of an assignment.

This for example won't simplify symbols to their values, but does simplify indices in arrays, members of structs and dereferencing of pointers

Parameters

condition	The expression to simplify
ns	The namespace

Returns: True if condition did not change. False otherwise. condition will be updated with the simplified condition if it has worked

Definition at line 43 of file ai_domain.cpp.

◆ is_bottom()

virtual bool ai_domain_baset::is_bottom ( ) const

pure virtual

Implemented in uninitialized_domaint, rd_range_domaint, is_threaded_domaint, invariant_set_domaint, interval_domaint, escape_domaint, value_set_domain_templatet< VST >, variable_sensitivity_domaint, variable_sensitivity_dependence_domaint, global_may_alias_domaint, dep_graph_domaint, custom_bitvector_domaint, and constant_propagator_domaint.

◆ is_top()

virtual bool ai_domain_baset::is_top ( ) const

pure virtual

Implemented in uninitialized_domaint, rd_range_domaint, is_threaded_domaint, invariant_set_domaint, interval_domaint, escape_domaint, value_set_domain_templatet< VST >, variable_sensitivity_domaint, variable_sensitivity_dependence_domaint, global_may_alias_domaint, dep_graph_domaint, custom_bitvector_domaint, and constant_propagator_domaint.

◆ make_bottom()

virtual void ai_domain_baset::make_bottom ( )

pure virtual

no states

Implemented in value_set_domain_templatet< VST >, variable_sensitivity_domaint, variable_sensitivity_dependence_domaint, uninitialized_domaint, rd_range_domaint, is_threaded_domaint, invariant_set_domaint, interval_domaint, global_may_alias_domaint, escape_domaint, dep_graph_domaint, custom_bitvector_domaint, and constant_propagator_domaint.

◆ make_entry()

virtual void ai_domain_baset::make_entry ( )

inlinevirtual

Make this domain a reasonable entry-point state For most domains top is sufficient.

Reimplemented in value_set_domain_templatet< VST >, is_threaded_domaint, invariant_set_domaint, and dep_graph_domaint.

Definition at line 121 of file ai_domain.h.

◆ make_top()

virtual void ai_domain_baset::make_top ( )

pure virtual

all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implement it.

Implemented in value_set_domain_templatet< VST >, variable_sensitivity_domaint, variable_sensitivity_dependence_domaint, uninitialized_domaint, rd_range_domaint, is_threaded_domaint, invariant_set_domaint, interval_domaint, global_may_alias_domaint, escape_domaint, dep_graph_domaint, custom_bitvector_domaint, and constant_propagator_domaint.

◆ output()

virtual void ai_domain_baset::output	(	std::ostream &	,
		const ai_baset &	,
		const namespacet &
	)		const

inlinevirtual

Reimplemented in constant_propagator_domaint, variable_sensitivity_domaint, variable_sensitivity_dependence_domaint, interval_domaint, global_may_alias_domaint, escape_domaint, dep_graph_domaint, custom_bitvector_domaint, uninitialized_domaint, value_set_domain_templatet< VST >, rd_range_domaint, and invariant_set_domaint.

Definition at line 104 of file ai_domain.h.

◆ output_json()

jsont ai_domain_baset::output_json	(	const ai_baset &	ai,
		const namespacet &	ns
	)		const

virtual

Reimplemented in variable_sensitivity_dependence_domaint, and dep_graph_domaint.

Definition at line 17 of file ai_domain.cpp.

◆ output_xml()

xmlt ai_domain_baset::output_xml	(	const ai_baset &	ai,
		const namespacet &	ns
	)		const

virtual

Reimplemented in value_set_domain_templatet< VST >.

Definition at line 26 of file ai_domain.cpp.

◆ to_predicate()

virtual exprt ai_domain_baset::to_predicate ( void ) const

inlinevirtual

Gives a Boolean condition that is true for all values represented by the domain.

This allows domains to be converted into program invariants.

Reimplemented in variable_sensitivity_domaint.

Definition at line 160 of file ai_domain.h.

◆ transform()

virtual void ai_domain_baset::transform	(	const irep_idt &	function_from,
		trace_ptrt	from,
		const irep_idt &	function_to,
		trace_ptrt	to,
		ai_baset &	ai,
		const namespacet &	ns
	)

pure virtual

how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)

in some cases, function calls are skipped, in which case: c) there is an edge from the call instruction to the instruction after

"this" is the domain before the instruction "from" "from" is the instruction to be interpreted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())

The history aware version is used by the abstract interpreter for backwards compatability it calls the older signature

Implemented in constant_propagator_domaint, variable_sensitivity_domaint, variable_sensitivity_dependence_domaint, uninitialized_domaint, rd_range_domaint, invariant_set_domaint, interval_domaint, global_may_alias_domaint, escape_domaint, dep_graph_domaint, custom_bitvector_domaint, value_set_domain_templatet< VST >, and is_threaded_domaint.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/analyses/ai_domain.h
/home/runner/work/cbmc/cbmc/src/analyses/ai_domain.cpp

Public Types

Public Member Functions

Protected Member Functions

Detailed Description

Member Typedef Documentation

◆ locationt

◆ trace_ptrt

Constructor & Destructor Documentation

◆ ai_domain_baset() [1/2]

◆ ai_domain_baset() [2/2]

◆ ~ai_domain_baset()

Member Function Documentation

◆ ai_simplify()

◆ ai_simplify_lhs()

◆ is_bottom()

◆ is_top()

◆ make_bottom()

◆ make_entry()

◆ make_top()

◆ output()

◆ output_json()

◆ output_xml()

◆ to_predicate()

◆ transform()