#include <dependence_graph.h>

Inheritance diagram for dep_graph_domaint:

Collaboration diagram for dep_graph_domaint:

Public Types
typedef grapht< 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
	dep_graph_domaint (node_indext id, message_handlert &message_handler)

bool	merge (const dep_graph_domaint &src, trace_ptrt from, trace_ptrt to)

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) final override
	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...

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

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

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

void	make_bottom () final override
	no states More...

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

bool	is_top () const final override

bool	is_bottom () const final override

node_indext	get_node_id () const

void	populate_dep_graph (dependence_grapht &, goto_programt::const_targett) 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 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...

Private Types
typedef std::set< goto_programt::const_targett, goto_programt::target_less_than >	depst

Private Member Functions
void	control_dependencies (const irep_idt &function_id, goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)

void	data_dependencies (goto_programt::const_targett from, const irep_idt &function_to, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns)

Private Attributes
tvt	has_values

node_indext	node_id

bool	has_changed

depst	control_deps

depst	control_dep_candidates

depst	data_deps

message_handlert &	message_handler

Friends
const depst &	dependence_graph_test_get_control_deps (const dep_graph_domaint &)

const depst &	dependence_graph_test_get_data_deps (const dep_graph_domaint &)

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. More...

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

Detailed Description

Definition at line 66 of file dependence_graph.h.

Member Typedef Documentation

◆ depst

typedef std:: set<goto_programt::const_targett, goto_programt::target_less_than> dep_graph_domaint::depst

private

Definition at line 180 of file dependence_graph.h.

◆ node_indext

typedef grapht<dep_nodet>::node_indext dep_graph_domaint::node_indext

Definition at line 69 of file dependence_graph.h.

Constructor & Destructor Documentation

◆ dep_graph_domaint()

dep_graph_domaint::dep_graph_domaint	(	node_indext	id,
		message_handlert &	message_handler
	)

inline

Definition at line 71 of file dependence_graph.h.

Member Function Documentation

◆ control_dependencies()

void dep_graph_domaint::control_dependencies	(	const irep_idt &	function_id,
		goto_programt::const_targett	from,
		goto_programt::const_targett	to,
		dependence_grapht &	dep_graph
	)

private

Definition at line 52 of file dependence_graph.cpp.

◆ data_dependencies()

void dep_graph_domaint::data_dependencies	(	goto_programt::const_targett	from,
		const irep_idt &	function_to,
		goto_programt::const_targett	to,
		dependence_grapht &	dep_graph,
		const namespacet &	ns
	)

private

Definition at line 154 of file dependence_graph.cpp.

◆ get_node_id()

node_indext dep_graph_domaint::get_node_id ( ) const

inline

Definition at line 164 of file dependence_graph.h.

◆ is_bottom()

bool dep_graph_domaint::is_bottom ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 150 of file dependence_graph.h.

◆ is_top()

bool dep_graph_domaint::is_top ( ) const

inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 136 of file dependence_graph.h.

◆ make_bottom()

void dep_graph_domaint::make_bottom ( )

inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 109 of file dependence_graph.h.

◆ make_entry()

void dep_graph_domaint::make_entry ( )

inlinefinaloverridevirtual

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

Reimplemented from ai_domain_baset.

Definition at line 122 of file dependence_graph.h.

◆ make_top()

void dep_graph_domaint::make_top ( )

inlinefinaloverridevirtual

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 98 of file dependence_graph.h.

◆ merge()

bool dep_graph_domaint::merge	(	const dep_graph_domaint &	src,
		trace_ptrt	from,
		trace_ptrt	to
	)

Definition at line 22 of file dependence_graph.cpp.

◆ output()

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

finaloverridevirtual

Reimplemented from ai_domain_baset.

Definition at line 272 of file dependence_graph.cpp.

◆ output_json()

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

overridevirtual

Outputs the current value of the domain.

parameters: The abstract interpreter and the namespace.

Returns: The domain, formatted as a JSON object.

Reimplemented from ai_domain_baset.

Definition at line 311 of file dependence_graph.cpp.

◆ populate_dep_graph()

void dep_graph_domaint::populate_dep_graph	(	dependence_grapht &	dep_graph,
		goto_programt::const_targett	this_loc
	)		const

Definition at line 393 of file dependence_graph.cpp.

◆ transform()

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

finaloverridevirtual

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

Implements ai_domain_baset.

Definition at line 217 of file dependence_graph.cpp.

Friends And Related Function Documentation

◆ dependence_graph_test_get_control_deps

const depst& dependence_graph_test_get_control_deps ( const dep_graph_domaint & )

friend

◆ dependence_graph_test_get_data_deps

const depst& dependence_graph_test_get_data_deps ( const dep_graph_domaint & )

friend

Member Data Documentation

◆ control_dep_candidates

depst dep_graph_domaint::control_dep_candidates

private

Definition at line 189 of file dependence_graph.h.

◆ control_deps

depst dep_graph_domaint::control_deps

private

Definition at line 184 of file dependence_graph.h.

◆ data_deps

depst dep_graph_domaint::data_deps

private

Definition at line 193 of file dependence_graph.h.

◆ has_changed

bool dep_graph_domaint::has_changed

private

Definition at line 176 of file dependence_graph.h.

◆ has_values

tvt dep_graph_domaint::has_values

private

Definition at line 174 of file dependence_graph.h.

◆ message_handler

message_handlert& dep_graph_domaint::message_handler

private

Definition at line 195 of file dependence_graph.h.

◆ node_id

node_indext dep_graph_domaint::node_id

private

Definition at line 175 of file dependence_graph.h.

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

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

Public Types

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Friends

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ depst

◆ node_indext

Constructor & Destructor Documentation

◆ dep_graph_domaint()

Member Function Documentation

◆ control_dependencies()

◆ data_dependencies()

◆ get_node_id()

◆ is_bottom()

◆ is_top()

◆ make_bottom()

◆ make_entry()

◆ make_top()

◆ merge()

◆ output()

◆ output_json()

◆ populate_dep_graph()

◆ transform()

Friends And Related Function Documentation

◆ dependence_graph_test_get_control_deps

◆ dependence_graph_test_get_data_deps

Member Data Documentation

◆ control_dep_candidates

◆ control_deps

◆ data_deps

◆ has_changed

◆ has_values

◆ message_handler

◆ node_id