General implementation of an abstract_objectt which tracks the last written locations for a given abstract_objectt. More...

#include <write_location_context.h>

Inheritance diagram for write_location_contextt:

Collaboration diagram for write_location_contextt:

Public Member Functions
	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. More...

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

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

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

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

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

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

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

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

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

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

virtual	~abstract_objectt ()

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

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

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

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

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

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

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

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

virtual locationst	get_last_written_locations () const

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

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

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

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

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

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

void	set_top ()

void	set_not_top ()

void	set_not_bottom ()

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

Private Types
using	combine_fn = std::function< abstract_objectt::combine_result(const abstract_object_pointert &op1, const abstract_object_pointert &op2)>

using	write_location_context_ptrt = std::shared_ptr< const write_location_contextt >

Private Member Functions
abstract_object_pointert	combine (const write_location_context_ptrt &other, combine_fn fn) const

context_abstract_object_ptrt	update_location_context_internal (const locationst &locations) const override

Private Attributes
locationst	last_written_locations

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

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

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

Protected Attributes inherited from context_abstract_objectt
abstract_object_pointert	child_abstract_object

Detailed Description

General implementation of an abstract_objectt which tracks the last written locations for a given abstract_objectt.

Instances of this class are constructed with an abstract_object_pointert, to which most operations are delegated, while at the same time this class handles the tracking of the 'last_written_location' information.

Instances of this class are best constructed via the templated version of this, 'context_abstract_objectt<T>' which provides the same constructors as the standard 'abstract_objectt' class.

Definition at line 34 of file write_location_context.h.

Member Typedef Documentation

◆ combine_fn

using write_location_contextt::combine_fn = std::function<abstract_objectt::combine_result( const abstract_object_pointert &op1, const abstract_object_pointert &op2)>

private

Definition at line 95 of file write_location_context.h.

◆ write_location_context_ptrt

using write_location_contextt::write_location_context_ptrt = std::shared_ptr<const write_location_contextt>

private

Definition at line 98 of file write_location_context.h.

Constructor & Destructor Documentation

◆ write_location_contextt() [1/2]

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

inline

Definition at line 37 of file write_location_context.h.

◆ write_location_contextt() [2/2]

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

inlineexplicit

Definition at line 46 of file write_location_context.h.

◆ ~write_location_contextt()

virtual write_location_contextt::~write_location_contextt ( )

inlinevirtual

Definition at line 55 of file write_location_context.h.

Member Function Documentation

◆ abstract_object_merge_internal()

abstract_object_pointert write_location_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 163 of file write_location_context.cpp.

◆ combine()

abstract_object_pointert write_location_contextt::combine	(	const write_location_context_ptrt &	other,
		combine_fn	fn
	)		const

private

Definition at line 119 of file write_location_context.cpp.

◆ get_last_written_locations()

context_abstract_objectt::locationst write_location_contextt::get_last_written_locations ( ) const

protectedvirtual

Definition at line 14 of file write_location_context.cpp.

◆ get_location_union()

context_abstract_objectt::locationst write_location_contextt::get_location_union ( const locationst & locations ) const

Construct the union of the location set of the current object, and a the provided location set.

Parameters

locations the set of locations to be unioned with this context

Returns: the union of this objects location set, and 'locations'

Definition at line 235 of file write_location_context.cpp.

◆ has_been_modified()

bool write_location_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 253 of file write_location_context.cpp.

◆ meet()

abstract_object_pointert write_location_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 108 of file write_location_context.cpp.

◆ merge()

abstract_object_pointert write_location_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 79 of file write_location_context.cpp.

◆ mutable_clone()

internal_abstract_object_pointert write_location_contextt::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 69 of file write_location_context.h.

◆ output()

void write_location_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 214 of file write_location_context.cpp.

◆ output_last_written_locations()

void write_location_contextt::output_last_written_locations	(	std::ostream &	out,
		const locationst &	locations
	)

staticprotected

Internal helper function to format and output a given set of locations.

Parameters

out	the stream on which to output the locations
locations	the set of locations to output

Definition at line 331 of file write_location_context.cpp.

◆ set_last_written_locations()

void write_location_contextt::set_last_written_locations ( const locationst & locations )

protected

Sets the last written locations for this context.

Parameters

locations the locations to set

Definition at line 200 of file write_location_context.cpp.

◆ update_location_context_internal()

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

overrideprivatevirtual

Implements context_abstract_objectt.

Definition at line 186 of file write_location_context.cpp.

◆ write()

abstract_object_pointert write_location_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

overrideprotectedvirtual

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 35 of file write_location_context.cpp.

Member Data Documentation

◆ last_written_locations

locationst write_location_contextt::last_written_locations

private

Definition at line 105 of file write_location_context.h.

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

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

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Private Types

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ combine_fn

◆ write_location_context_ptrt

Constructor & Destructor Documentation

◆ write_location_contextt() [1/2]

◆ write_location_contextt() [2/2]

◆ ~write_location_contextt()

Member Function Documentation

◆ abstract_object_merge_internal()

◆ combine()

◆ get_last_written_locations()

◆ get_location_union()

◆ has_been_modified()

◆ meet()

◆ merge()

◆ mutable_clone()

◆ output()

◆ output_last_written_locations()

◆ set_last_written_locations()

◆ update_location_context_internal()

◆ write()

Member Data Documentation

◆ last_written_locations