#include <variable_sensitivity_dependence_graph.h>

Inheritance diagram for variable_sensitivity_dependence_domaint:

Collaboration diagram for variable_sensitivity_dependence_domaint:

Classes
class	dependency_ordert

Public Types
typedef grapht< vs_dep_nodet >::node_indext	node_indext

Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett	locationt

typedef ai_history_baset::trace_ptrt	trace_ptrt

Public Member Functions
	variable_sensitivity_dependence_domaint (node_indext id, variable_sensitivity_object_factory_ptrt object_factory, const vsd_configt &configuration)

void	transform (const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) override
	Compute the abstract transformer for a single instruction.

void	make_bottom () override
	no states

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

bool	is_bottom () const override

bool	is_top () const override

bool	merge (const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to) override
	Computes the join between "this" and "b".

void	merge_three_way_function_return (const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns) override
	Merges just the things that have changes between "function_start" and "function_end" into "this".

void	output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
	Basic text output of the abstract domain.

jsont	output_json (const ai_baset &ai, const namespacet &ns) const override
	Outputs the current value of the domain.

void	populate_dep_graph (variable_sensitivity_dependence_grapht &, goto_programt::const_targett) const

node_indext	get_node_id () const

Public Member Functions inherited from variable_sensitivity_domaint
	variable_sensitivity_domaint (variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)

void	transform (const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) override
	Compute the abstract transformer for a single instruction.

void	make_bottom () override
	Sets the domain to bottom (no states / unreachable).

void	make_top () override
	Sets the domain to top (all states).

void	output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
	Basic text output of the abstract domain.

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

exprt	to_predicate (const exprt &expr, const namespacet &ns) const

exprt	to_predicate (const exprt::operandst &exprs, const namespacet &ns) const

bool	ai_simplify (exprt &condition, const namespacet &ns) const override
	Use the information in the domain to simplify the expression with respect to the current location.

bool	is_bottom () const override
	Find out if the domain is currently unreachable.

bool	is_top () const override
	Is the domain completely top at this state.

virtual abstract_object_pointert	eval (const exprt &expr, const namespacet &ns) const

Public Member Functions inherited from ai_domain_baset
virtual	~ai_domain_baset ()

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

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

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

Private Types
typedef std::map< goto_programt::const_targett, std::set< exprt >, dependency_ordert >	data_depst

typedef std::map< goto_programt::const_targett, tvt, goto_programt::target_less_than >	control_depst

typedef std::set< goto_programt::const_targett, goto_programt::target_less_than >	control_dep_candidatest

typedef std::set< goto_programt::const_targett, goto_programt::target_less_than >	control_dep_callst

Private Member Functions
void	eval_data_deps (const exprt &expr, const namespacet &ns, data_depst &deps) const
	Evaluate an expression and accumulate all the data dependencies involved in the evaluation.

void	control_dependencies (const irep_idt &from_function, goto_programt::const_targett from, const irep_idt &to_function, goto_programt::const_targett to, variable_sensitivity_dependence_grapht &dep_graph)

void	data_dependencies (goto_programt::const_targett from, goto_programt::const_targett to, variable_sensitivity_dependence_grapht &dep_graph, const namespacet &ns)

bool	merge_control_dependencies (const control_depst &other_control_deps, const control_dep_candidatest &other_control_dep_candidates, const control_dep_callst &other_control_dep_calls, const control_dep_callst &other_control_dep_call_candidates)

Private Attributes
node_indext	node_id

tvt	has_values

bool	has_changed

data_depst	domain_data_deps

control_depst	control_deps

control_dep_candidatest	control_dep_candidates

control_dep_callst	control_dep_calls

control_dep_callst	control_dep_call_candidates

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

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

Detailed Description

Definition at line 70 of file variable_sensitivity_dependence_graph.h.

Member Typedef Documentation

◆ control_dep_callst

typedef std:: set<goto_programt::const_targett, goto_programt::target_less_than> variable_sensitivity_dependence_domaint::control_dep_callst

private

Definition at line 188 of file variable_sensitivity_dependence_graph.h.

◆ control_dep_candidatest

typedef std:: set<goto_programt::const_targett, goto_programt::target_less_than> variable_sensitivity_dependence_domaint::control_dep_candidatest

private

Definition at line 183 of file variable_sensitivity_dependence_graph.h.

◆ control_depst

typedef std:: map<goto_programt::const_targett, tvt, goto_programt::target_less_than> variable_sensitivity_dependence_domaint::control_depst

private

Definition at line 178 of file variable_sensitivity_dependence_graph.h.

◆ data_depst

typedef std:: map<goto_programt::const_targett, std::set<exprt>, dependency_ordert> variable_sensitivity_dependence_domaint::data_depst

private

Definition at line 173 of file variable_sensitivity_dependence_graph.h.

◆ node_indext

typedef grapht<vs_dep_nodet>::node_indext variable_sensitivity_dependence_domaint::node_indext

Definition at line 74 of file variable_sensitivity_dependence_graph.h.

Constructor & Destructor Documentation

◆ variable_sensitivity_dependence_domaint()

variable_sensitivity_dependence_domaint::variable_sensitivity_dependence_domaint	(	node_indext	id,
		variable_sensitivity_object_factory_ptrt	object_factory,
		const vsd_configt &	configuration
	)

inlineexplicit

Definition at line 76 of file variable_sensitivity_dependence_graph.h.

Member Function Documentation

◆ control_dependencies()

void variable_sensitivity_dependence_domaint::control_dependencies	(	const irep_idt &	from_function,
		goto_programt::const_targett	from,
		const irep_idt &	to_function,
		goto_programt::const_targett	to,
		variable_sensitivity_dependence_grapht &	dep_graph
	)

private

Definition at line 204 of file variable_sensitivity_dependence_graph.cpp.

◆ data_dependencies()

void variable_sensitivity_dependence_domaint::data_dependencies	(	goto_programt::const_targett	from,
		goto_programt::const_targett	to,
		variable_sensitivity_dependence_grapht &	dep_graph,
		const namespacet &	ns
	)

private

Definition at line 135 of file variable_sensitivity_dependence_graph.cpp.

◆ eval_data_deps()

void variable_sensitivity_dependence_domaint::eval_data_deps	(	const exprt &	expr,
		const namespacet &	ns,
		data_depst &	deps
	)		const

private

Evaluate an expression and accumulate all the data dependencies involved in the evaluation.

Parameters

expr	the expression to evaluate
ns	the namespace to use
deps	the destination in which to accumlate data dependencies

Definition at line 27 of file variable_sensitivity_dependence_graph.cpp.

◆ get_node_id()

node_indext variable_sensitivity_dependence_domaint::get_node_id ( ) const

inline

Definition at line 148 of file variable_sensitivity_dependence_graph.h.

◆ is_bottom()

bool variable_sensitivity_dependence_domaint::is_bottom ( ) const

inlineoverridevirtual

Implements ai_domain_baset.

Definition at line 119 of file variable_sensitivity_dependence_graph.h.

◆ is_top()

bool variable_sensitivity_dependence_domaint::is_top ( ) const

inlineoverridevirtual

Implements ai_domain_baset.

Definition at line 124 of file variable_sensitivity_dependence_graph.h.

◆ make_bottom()

void variable_sensitivity_dependence_domaint::make_bottom ( )

inlineoverridevirtual

no states

Implements ai_domain_baset.

Definition at line 95 of file variable_sensitivity_dependence_graph.h.

◆ make_top()

void variable_sensitivity_dependence_domaint::make_top ( )

inlineoverridevirtual

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

Implements ai_domain_baset.

Definition at line 107 of file variable_sensitivity_dependence_graph.h.

◆ merge()

bool variable_sensitivity_dependence_domaint::merge	(	const variable_sensitivity_domaint &	b,
		trace_ptrt	from,
		trace_ptrt	to
	)

overridevirtual

Computes the join between "this" and "b".

Parameters

b	the other domain
from	the location preceding the 'b' domain
to	the current location

Returns: true if something has changed in the merge

Reimplemented from variable_sensitivity_domaint.

Definition at line 404 of file variable_sensitivity_dependence_graph.cpp.

◆ merge_control_dependencies()

bool variable_sensitivity_dependence_domaint::merge_control_dependencies	(	const control_depst &	other_control_deps,
		const control_dep_candidatest &	other_control_dep_candidates,
		const control_dep_callst &	other_control_dep_calls,
		const control_dep_callst &	other_control_dep_call_candidates
	)

private

Definition at line 314 of file variable_sensitivity_dependence_graph.cpp.

◆ merge_three_way_function_return()

void variable_sensitivity_dependence_domaint::merge_three_way_function_return	(	const ai_domain_baset &	function_start,
		const ai_domain_baset &	function_end,
		const namespacet &	ns
	)

overridevirtual

Merges just the things that have changes between "function_start" and "function_end" into "this".

To be used correctly "this" must be derived from the function call site. Anything that is not modified in the function (such as globals) will not be changed.

Parameters

function_start	The base of the diff - changes that have been made between here and the end will be retained.
function_end	The end of the merge - changes that have been made between the start and here will be retained.
ns	The global namespace

Reimplemented from variable_sensitivity_domaint.

Definition at line 443 of file variable_sensitivity_dependence_graph.cpp.

◆ output()

void variable_sensitivity_dependence_domaint::output	(	std::ostream &	out,
		const ai_baset &	ai,
		const namespacet &	ns
	)		const

overridevirtual

Basic text output of the abstract domain.

Parameters

out	the stream to output onto
ai	the abstract domain
ns	the namespace

Reimplemented from ai_domain_baset.

Definition at line 464 of file variable_sensitivity_dependence_graph.cpp.

◆ output_json()

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

overridevirtual

Outputs the current value of the domain.

Parameters

ai	the abstract interpreter
ns	the namespace

Returns: the domain, formatted as a JSON object.

Reimplemented from ai_domain_baset.

Definition at line 534 of file variable_sensitivity_dependence_graph.cpp.

◆ populate_dep_graph()

void variable_sensitivity_dependence_domaint::populate_dep_graph	(	variable_sensitivity_dependence_grapht &	dep_graph,
		goto_programt::const_targett	this_loc
	)		const

Definition at line 587 of file variable_sensitivity_dependence_graph.cpp.

◆ transform()

void variable_sensitivity_dependence_domaint::transform	(	const irep_idt &	function_from,
		trace_ptrt	trace_from,
		const irep_idt &	function_to,
		trace_ptrt	trace_to,
		ai_baset &	ai,
		const namespacet &	ns
	)

overridevirtual

Compute the abstract transformer for a single instruction.

For the data dependencies, this involves calculating all the data dependencies that exist in the 'to' instruction.

Parameters

function_from	the function of the instruction before the abstract domain
trace_from	the instruction before the abstract domain
function_to	the function of the instruction after the abstract domain
trace_to	the instruction after the abstract domain
ai	the abstract interpreter
ns	the namespace

Implements ai_domain_baset.

Definition at line 68 of file variable_sensitivity_dependence_graph.cpp.

Member Data Documentation

◆ control_dep_call_candidates

control_dep_callst variable_sensitivity_dependence_domaint::control_dep_call_candidates

private

Definition at line 190 of file variable_sensitivity_dependence_graph.h.

◆ control_dep_calls

control_dep_callst variable_sensitivity_dependence_domaint::control_dep_calls

private

Definition at line 189 of file variable_sensitivity_dependence_graph.h.

◆ control_dep_candidates

control_dep_candidatest variable_sensitivity_dependence_domaint::control_dep_candidates

private

Definition at line 184 of file variable_sensitivity_dependence_graph.h.

◆ control_deps

control_depst variable_sensitivity_dependence_domaint::control_deps

private

Definition at line 179 of file variable_sensitivity_dependence_graph.h.

◆ domain_data_deps

data_depst variable_sensitivity_dependence_domaint::domain_data_deps

private

Definition at line 174 of file variable_sensitivity_dependence_graph.h.

◆ has_changed

bool variable_sensitivity_dependence_domaint::has_changed

private

Definition at line 159 of file variable_sensitivity_dependence_graph.h.

◆ has_values

tvt variable_sensitivity_dependence_domaint::has_values

private

Definition at line 158 of file variable_sensitivity_dependence_graph.h.

◆ node_id

node_indext variable_sensitivity_dependence_domaint::node_id

private

Definition at line 157 of file variable_sensitivity_dependence_graph.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.h
/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp

Classes

Public Types

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ control_dep_callst

◆ control_dep_candidatest

◆ control_depst

◆ data_depst

◆ node_indext

Constructor & Destructor Documentation

◆ variable_sensitivity_dependence_domaint()

Member Function Documentation

◆ control_dependencies()

◆ data_dependencies()

◆ eval_data_deps()

◆ get_node_id()

◆ is_bottom()

◆ is_top()

◆ make_bottom()

◆ make_top()

◆ merge()

◆ merge_control_dependencies()

◆ merge_three_way_function_return()

◆ output()

◆ output_json()

◆ populate_dep_graph()

◆ transform()

Member Data Documentation

◆ control_dep_call_candidates

◆ control_dep_calls

◆ control_dep_candidates

◆ control_deps

◆ domain_data_deps

◆ has_changed

◆ has_values

◆ node_id