#include <data_dependency_context.h>

Inheritance diagram for data_dependency_contextt:

Collaboration diagram for data_dependency_contextt:

Classes
class	location_ordert

Public Member Functions
	data_dependency_contextt (const abstract_object_pointert child, const typet &type, bool top, bool bottom)

	data_dependency_contextt (const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)

abstract_object_pointert	write (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
	A helper function to evaluate writing to a component of an abstract object.

bool	has_been_modified (const abstract_object_pointert &before) const override
	Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state.

std::set< goto_programt::const_targett, goto_programt::target_less_than >	get_data_dependencies () const
	Return the set of data dependencies associated with this node.

std::set< goto_programt::const_targett, goto_programt::target_less_than >	get_data_dominators () const
	Return the set of data dominators associated with this node.

void	output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
	Output a representation of the value of this abstract object.

Public Member Functions inherited from write_location_contextt
	write_location_contextt (const abstract_object_pointert child, const typet &type, bool top, bool bottom)

	write_location_contextt (const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)

virtual	~write_location_contextt ()

bool	has_been_modified (const abstract_object_pointert &before) const override
	Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state.

locationst	get_location_union (const locationst &locations) const
	Construct the union of the location set of the current object, and a the provided location set.

void	output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
	Output a representation of the value of this abstract object.

Public Member Functions inherited from context_abstract_objectt
	context_abstract_objectt (const abstract_object_pointert child, const typet &type, bool top, bool bottom)

	context_abstract_objectt (const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)

virtual	~context_abstract_objectt ()

const typet &	type () const override
	Get the real type of the variable this abstract object is representing.

bool	is_top () const override
	Find out if the abstract object is top.

bool	is_bottom () const override
	Find out if the abstract object is bottom.

exprt	to_constant () const override
	Converts to a constant expression if possible.

abstract_object_pointert	expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
	Try to resolve an expression with the maximum level of precision available.

abstract_object_pointert	write_location_context (const locationt &location) const override
	Update the location context for an abstract object.

abstract_object_pointert	envelop (abstract_object_pointert &child) const

abstract_object_pointert	unwrap_context () const override

void	get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override

abstract_object_pointert	get_child () const

Public Member Functions inherited from abstract_objectt
	abstract_objectt (const typet &type, bool top, bool bottom)
	Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true.

	abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
	Construct an abstract object from the expression.

virtual	~abstract_objectt ()

virtual bool	verify () const
	Verify the internal structure of an abstract_object is correct.

exprt	to_predicate (const exprt &name) const
	Converts to an invariant expression.

virtual abstract_object_pointert	merge_location_context (const locationt &location) const
	Update the merge location context for an abstract object.

abstract_object_pointert	make_top () const

abstract_object_pointert	clear_top () const

virtual abstract_object_pointert	visit_sub_elements (const abstract_object_visitort &visitor) const
	Apply a visitor operation to all sub elements of this abstract_object.

virtual size_t	internal_hash () const

virtual bool	internal_equality (const abstract_object_pointert &other) const

Protected Member Functions
internal_abstract_object_pointert	mutable_clone () const override

abstract_object_pointert	merge (const abstract_object_pointert &other, const widen_modet &widen_mode) const override
	Create a new abstract object that is the result of merging this abstract object with a given abstract_object.

abstract_object_pointert	meet (const abstract_object_pointert &other) const override
	Base implementation of the meet operation: only used if no more precise abstraction can be used, can only result in {TOP, BOTTOM, one of the original objects}.

abstract_object_pointert	abstract_object_merge_internal (const abstract_object_pointert &other) const override
	Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed its actions but immediately prior to it returning.

Protected Member Functions inherited from write_location_contextt
internal_abstract_object_pointert	mutable_clone () const override

abstract_object_pointert	merge (const abstract_object_pointert &other, const widen_modet &widen_mode) const override
	Create a new abstract object that is the result of merging this abstract object with a given abstract_object.

abstract_object_pointert	meet (const abstract_object_pointert &other) const override
	Base implementation of the meet operation: only used if no more precise abstraction can be used, can only result in {TOP, BOTTOM, one of the original objects}.

abstract_object_pointert	abstract_object_merge_internal (const abstract_object_pointert &other) const override
	Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed its actions but immediately prior to it returning.

abstract_object_pointert	write (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
	A helper function to evaluate writing to a component of an abstract object.

virtual locationst	get_last_written_locations () const

void	set_last_written_locations (const locationst &locations)
	Sets the last written locations for this context.

Protected Member Functions inherited from context_abstract_objectt
void	set_child (const abstract_object_pointert &child)

void	set_top_internal () override

void	set_not_top_internal () override

exprt	to_predicate_internal (const exprt &name) const override
	to_predicate implementation - derived classes will override

Protected Member Functions inherited from abstract_objectt
abstract_object_pointert	abstract_object_merge (const abstract_object_pointert &other) const
	Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.

bool	should_use_base_merge (const abstract_object_pointert &other) const
	To detect the cases where the base merge is sufficient to do a merge We can't do if this->is_bottom() since we want the specific.

abstract_object_pointert	abstract_object_meet (const abstract_object_pointert &other) const
	Helper function for base meet.

bool	should_use_base_meet (const abstract_object_pointert &other) const
	Helper function to decide if base meet implementation should be used.

void	set_top ()

void	set_not_top ()

void	set_not_bottom ()

Private Types
using	data_dependency_context_ptrt = std::shared_ptr< const data_dependency_contextt >

typedef std::set< goto_programt::const_targett, location_ordert >	dependenciest

Private Member Functions
abstract_object_pointert	combine (const data_dependency_context_ptrt &other, const data_dependency_context_ptrt &parent) const

abstract_object_pointert	insert_data_deps (const dependenciest &dependencies) const
	Insert the given set of data dependencies into the data dependencies set for this data_dependency_context object.

context_abstract_object_ptrt	update_location_context_internal (const locationst &locations) const override

void	set_data_deps (const locationst &locations)
	Set the given set of data dependencies for from the locations.

void	set_data_deps (const dependenciest &dependences)
	Set the given set of data dependencies for this data_dependency_context object.

Private Attributes
dependenciest	data_deps

dependenciest	data_dominators

Additional Inherited Members
Public Types inherited from abstract_objectt
typedef goto_programt::const_targett	locationt

typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash >	shared_mapt

Static Public Member Functions inherited from abstract_objectt
static void	dump_map (std::ostream out, const shared_mapt &m)

static void	dump_map_diff (std::ostream out, const shared_mapt &m1, const shared_mapt &m2)
	Dump all elements in m1 that are different or missing in m2.

static combine_result	merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)

static combine_result	merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const widen_modet &widen_mode)

static combine_result	meet (const abstract_object_pointert &op1, const abstract_object_pointert &op2)
	Interface method for the meet operation.

Protected Types inherited from context_abstract_objectt
using	context_abstract_object_ptrt = std::shared_ptr< context_abstract_objectt >

typedef std::set< locationt, goto_programt::target_less_than >	locationst

Protected Types inherited from abstract_objectt
template<class T >
using	internal_sharing_ptrt = std::shared_ptr< T >

typedef internal_sharing_ptrt< class abstract_objectt >	internal_abstract_object_pointert

Static Protected Member Functions inherited from write_location_contextt
static void	output_last_written_locations (std::ostream &out, const locationst &locations)
	Internal helper function to format and output a given set of locations.

Protected Attributes inherited from context_abstract_objectt
abstract_object_pointert	child_abstract_object

Detailed Description

Definition at line 19 of file data_dependency_context.h.

Member Typedef Documentation

◆ data_dependency_context_ptrt

using data_dependency_contextt::data_dependency_context_ptrt = std::shared_ptr<const data_dependency_contextt>

private

Definition at line 73 of file data_dependency_context.h.

◆ dependenciest

typedef std::set<goto_programt::const_targett, location_ordert> data_dependency_contextt::dependenciest

private

Definition at line 90 of file data_dependency_context.h.

Constructor & Destructor Documentation

◆ data_dependency_contextt() [1/2]

data_dependency_contextt::data_dependency_contextt	(	const abstract_object_pointert	child,
		const typet &	type,
		bool	top,
		bool	bottom
	)

inline

Definition at line 24 of file data_dependency_context.h.

◆ data_dependency_contextt() [2/2]

data_dependency_contextt::data_dependency_contextt	(	const abstract_object_pointert	child,
		const exprt &	expr,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)

inlineexplicit

Definition at line 33 of file data_dependency_context.h.

Member Function Documentation

◆ abstract_object_merge_internal()

abstract_object_pointert data_dependency_contextt::abstract_object_merge_internal ( const abstract_object_pointert & other ) const

overrideprotectedvirtual

Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed its actions but immediately prior to it returning.

As such, this function gives the ability to perform additional work for a merge.

For the dependency context, this additional work is the tracking of last_written_locations across the merge

Parameters

other the object to merge with this

Returns: the result of the merge

Reimplemented from abstract_objectt.

Definition at line 308 of file data_dependency_context.cpp.

◆ combine()

abstract_object_pointert data_dependency_contextt::combine	(	const data_dependency_context_ptrt &	other,
		const data_dependency_context_ptrt &	parent
	)		const

private

Definition at line 260 of file data_dependency_context.cpp.

◆ get_data_dependencies()

std::set< goto_programt::const_targett, goto_programt::target_less_than > data_dependency_contextt::get_data_dependencies ( ) const

Return the set of data dependencies associated with this node.

Returns: set of data dependencies

Definition at line 331 of file data_dependency_context.cpp.

◆ get_data_dominators()

std::set< goto_programt::const_targett, goto_programt::target_less_than > data_dependency_contextt::get_data_dominators ( ) const

Return the set of data dominators associated with this node.

Returns: set of data dominators

Definition at line 346 of file data_dependency_context.cpp.

◆ has_been_modified()

bool data_dependency_contextt::has_been_modified ( const abstract_object_pointert & before ) const

overridevirtual

Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state.

Parameters

before the abstract_object_pointert to use as a reference to compare against

Returns: true if 'this' is considered to have been modified in comparison to 'before', false otherwise.

Reimplemented from context_abstract_objectt.

Definition at line 28 of file data_dependency_context.cpp.

◆ insert_data_deps()

abstract_object_pointert data_dependency_contextt::insert_data_deps ( const dependenciest & dependencies ) const

private

Insert the given set of data dependencies into the data dependencies set for this data_dependency_context object.

Parameters

dependencies the set of dependencies to add

Returns: a new data_dependency_context if new dependencies were added, or 'this' if no addtional dependencies were added.

Definition at line 82 of file data_dependency_context.cpp.

◆ meet()

abstract_object_pointert data_dependency_contextt::meet ( const abstract_object_pointert & other ) const

overrideprotectedvirtual

Base implementation of the meet operation: only used if no more precise abstraction can be used, can only result in {TOP, BOTTOM, one of the original objects}.

Parameters

other pointer to the abstract object to meet

Returns: the resulting abstract object pointer

Reimplemented from abstract_objectt.

Definition at line 243 of file data_dependency_context.cpp.

◆ merge()

abstract_object_pointert data_dependency_contextt::merge	(	const abstract_object_pointert &	other,
		const widen_modet &	widen_mode
	)		const

overrideprotectedvirtual

Create a new abstract object that is the result of merging this abstract object with a given abstract_object.

Parameters

other	the abstract object to merge with
widen_mode	Indicates if this is a widening merge

Returns: the result of the merge, or 'this' if the merge would not change the current abstract object

Reimplemented from abstract_objectt.

Definition at line 223 of file data_dependency_context.cpp.

◆ mutable_clone()

internal_abstract_object_pointert data_dependency_contextt::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 61 of file data_dependency_context.h.

◆ output()

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

overridevirtual

Output a representation of the value of this abstract object.

Parameters

out	the stream to write to
ai	the abstract interpreter that contains the abstract domain (that contains the object ... )
ns	the current namespace

Reimplemented from context_abstract_objectt.

Definition at line 355 of file data_dependency_context.cpp.

◆ set_data_deps() [1/2]

void data_dependency_contextt::set_data_deps ( const dependenciest & dependencies )

private

Set the given set of data dependencies for this data_dependency_context object.

Parameters

dependencies the set of dependencies to set

Definition at line 159 of file data_dependency_context.cpp.

◆ set_data_deps() [2/2]

void data_dependency_contextt::set_data_deps ( const locationst & locations )

private

Set the given set of data dependencies for from the locations.

Parameters

locations the write locations

Definition at line 146 of file data_dependency_context.cpp.

◆ update_location_context_internal()

context_abstract_objectt::context_abstract_object_ptrt data_dependency_contextt::update_location_context_internal ( const locationst & locations ) const

overrideprivatevirtual

Implements context_abstract_objectt.

Definition at line 131 of file data_dependency_context.cpp.

◆ write()

abstract_object_pointert data_dependency_contextt::write	(	abstract_environmentt &	environment,
		const namespacet &	ns,
		const std::stack< exprt > &	stack,
		const exprt &	specifier,
		const abstract_object_pointert &	value,
		bool	merging_write
	)		const

overridevirtual

A helper function to evaluate writing to a component of an abstract object.

More precise abstractions may override this to update what they are storing for a specific component.

Parameters

environment	the abstract environment
ns	the current namespace
stack	the remaining stack of expressions on the LHS to evaluate
specifier	the expression uses to access a specific component
value	the value we are trying to write to the component
merging_write	if true, this and all future writes will be merged with the current value

Returns: the abstract_objectt representing the result of writing to a specific component.

Reimplemented from context_abstract_objectt.

Definition at line 194 of file data_dependency_context.cpp.

Member Data Documentation

◆ data_deps

dependenciest data_dependency_contextt::data_deps

private

Definition at line 91 of file data_dependency_context.h.

◆ data_dominators

dependenciest data_dependency_contextt::data_dominators

private

Definition at line 92 of file data_dependency_context.h.

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

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

Classes

Public Member Functions

Protected Member Functions

Private Types

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ data_dependency_context_ptrt

◆ dependenciest

Constructor & Destructor Documentation

◆ data_dependency_contextt() [1/2]

◆ data_dependency_contextt() [2/2]

Member Function Documentation

◆ abstract_object_merge_internal()

◆ combine()

◆ get_data_dependencies()

◆ get_data_dominators()

◆ has_been_modified()

◆ insert_data_deps()

◆ meet()

◆ merge()

◆ mutable_clone()

◆ output()

◆ set_data_deps() [1/2]

◆ set_data_deps() [2/2]

◆ update_location_context_internal()

◆ write()

Member Data Documentation

◆ data_deps

◆ data_dominators