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

#include <liveness_context.h>

Inheritance diagram for liveness_contextt:

Collaboration diagram for liveness_contextt:

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

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

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

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.

locationt	get_location () const

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.

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	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 it's 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.

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	liveness_context_ptrt = std::shared_ptr< const liveness_contextt >

Private Member Functions
abstract_object_pointert	reset_location_on_merge (const liveness_context_ptrt &merged) const

context_abstract_object_ptrt	update_location_context_internal (const locationst &locations) const override

bool	has_location () const

void	set_location (const locationt &location)

Private Attributes
std::optional< locationt >	assign_location

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

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 33 of file liveness_context.h.

Member Typedef Documentation

◆ liveness_context_ptrt

using liveness_contextt::liveness_context_ptrt = std::shared_ptr<const liveness_contextt>

private

Definition at line 81 of file liveness_context.h.

Constructor & Destructor Documentation

◆ liveness_contextt() [1/2]

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

inline

Definition at line 36 of file liveness_context.h.

◆ liveness_contextt() [2/2]

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

inlineexplicit

Definition at line 45 of file liveness_context.h.

Member Function Documentation

◆ abstract_object_merge_internal()

abstract_object_pointert liveness_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 it's actions but immediately prior to it returning.

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

This default implementation just returns itself.

Parameters

other the object to merge with this

Returns: the result of the merge

Reimplemented from abstract_objectt.

Definition at line 88 of file liveness_context.cpp.

◆ get_location()

abstract_objectt::locationt liveness_contextt::get_location ( ) const

Definition at line 16 of file liveness_context.cpp.

◆ has_location()

bool liveness_contextt::has_location ( ) const

private

Definition at line 11 of file liveness_context.cpp.

◆ merge()

abstract_object_pointert liveness_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 72 of file liveness_context.cpp.

◆ merge_location_context()

abstract_object_pointert liveness_contextt::merge_location_context ( const locationt & location ) const

overridevirtual

Update the merge location context for an abstract object.

Parameters

location the location to be updated

Returns: a clone of this abstract object with its location context updated

Reimplemented from abstract_objectt.

Definition at line 145 of file liveness_context.cpp.

◆ mutable_clone()

internal_abstract_object_pointert liveness_contextt::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 63 of file liveness_context.h.

◆ output()

void liveness_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 131 of file liveness_context.cpp.

◆ reset_location_on_merge()

abstract_object_pointert liveness_contextt::reset_location_on_merge ( const liveness_context_ptrt & merged ) const

private

Definition at line 96 of file liveness_context.cpp.

◆ set_location()

void liveness_contextt::set_location ( const locationt & location )

private

Definition at line 118 of file liveness_context.cpp.

◆ update_location_context_internal()

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

overrideprivatevirtual

Implements context_abstract_objectt.

Definition at line 109 of file liveness_context.cpp.

◆ write()

abstract_object_pointert liveness_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 37 of file liveness_context.cpp.

Member Data Documentation

◆ assign_location

std::optional<locationt> liveness_contextt::assign_location

private

Definition at line 86 of file liveness_context.h.

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

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

Public Member Functions

Protected Member Functions

Private Types

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ liveness_context_ptrt

Constructor & Destructor Documentation

◆ liveness_contextt() [1/2]

◆ liveness_contextt() [2/2]

Member Function Documentation

◆ abstract_object_merge_internal()

◆ get_location()

◆ has_location()

◆ merge()

◆ merge_location_context()

◆ mutable_clone()

◆ output()

◆ reset_location_on_merge()

◆ set_location()

◆ update_location_context_internal()

◆ write()

Member Data Documentation

◆ assign_location