#include <full_struct_abstract_object.h>

Inheritance diagram for full_struct_abstract_objectt:

Collaboration diagram for full_struct_abstract_objectt:

Public Member Functions
	full_struct_abstract_objectt (const full_struct_abstract_objectt &ao)
	Explicit copy-constructor to make it clear that the shared_map used to store the values of fields is copy-constructed as well to ensure it shares as much data as possible.

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

	full_struct_abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)

void	output (std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
	To provide a human readable string to the out representing the current known value about this object.

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

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

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

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

Public Member Functions inherited from abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >
	abstract_aggregate_objectt (const typet &type, bool tp, bool bttm)

	abstract_aggregate_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)

abstract_object_pointert	expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
	Interface for transforms.

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.

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

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 const typet &	type () const
	Get the real type of the variable this abstract object is representing.

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

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

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

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

virtual void	output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
	Print the value of the abstract object.

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

virtual abstract_object_pointert	meet (const abstract_object_pointert &other) const
	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	make_top () const

abstract_object_pointert	clear_top () const

virtual abstract_object_pointert	unwrap_context () const

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	read_component (const abstract_environmentt &environment, const exprt &expr, const namespacet &ns) const override
	A helper function to evaluate the abstract object contained within a struct.

abstract_object_pointert	write_component (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const override
	A helper function to evaluate writing to a component of a struct.

bool	verify () const override
	Function: full_struct_abstract_objectt::verify.

abstract_object_pointert	merge (const abstract_object_pointert &other, const widen_modet &widen_mode) const override
	To merge an abstract object into this abstract object.

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
typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash >	shared_struct_mapt

Private Member Functions
abstract_object_pointert	merge_constant_structs (constant_struct_pointert other, const widen_modet &widen_mode) const
	Performs an element wise merge of the map for each struct.

Private Attributes
shared_struct_mapt	map

Additional Inherited Members
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 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 abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >
static bool	merge_shared_maps (const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map1, const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map2, sharing_mapt< keyt, abstract_object_pointert, false, hash > &out_map, const widen_modet &widen_mode)

Detailed Description

Definition at line 18 of file full_struct_abstract_object.h.

Member Typedef Documentation

◆ abstract_aggregate_baset

typedef abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet> full_struct_abstract_objectt::abstract_aggregate_baset

Definition at line 27 of file full_struct_abstract_object.h.

◆ constant_struct_pointert

typedef sharing_ptrt<full_struct_abstract_objectt> full_struct_abstract_objectt::constant_struct_pointert

Definition at line 23 of file full_struct_abstract_object.h.

◆ shared_struct_mapt

typedef sharing_mapt<irep_idt, abstract_object_pointert, false, irep_id_hash> full_struct_abstract_objectt::shared_struct_mapt

private

Definition at line 102 of file full_struct_abstract_object.h.

Constructor & Destructor Documentation

◆ full_struct_abstract_objectt() [1/3]

full_struct_abstract_objectt::full_struct_abstract_objectt ( const full_struct_abstract_objectt & ao )

Explicit copy-constructor to make it clear that the shared_map used to store the values of fields is copy-constructed as well to ensure it shares as much data as possible.

Definition at line 24 of file full_struct_abstract_object.cpp.

◆ full_struct_abstract_objectt() [2/3]

full_struct_abstract_objectt::full_struct_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.

Parameters

type	the type the abstract_object is representing
top	is the abstract_object starting as top
bottom	is the abstract_object starting as bottom

Definition at line 30 of file full_struct_abstract_object.cpp.

◆ full_struct_abstract_objectt() [3/3]

full_struct_abstract_objectt::full_struct_abstract_objectt	(	const exprt &	expr,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)

Parameters

expr	the expression to use as the starting pointer for an abstract object
environment	the environment in which we evaluate expr
ns	the current namespace

Definition at line 40 of file full_struct_abstract_object.cpp.

Member Function Documentation

◆ merge()

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

overrideprotectedvirtual

To merge an abstract object into this abstract object.

If the other is also a struct, we perform a constant_structs merge Otherwise we call back to the parent merge.

Parameters

other	the other object being merged
widen_mode	Indicates if this is a widening merge

Returns: Returns the result of the merge.

Reimplemented from abstract_objectt.

Definition at line 242 of file full_struct_abstract_object.cpp.

◆ merge_constant_structs()

abstract_object_pointert full_struct_abstract_objectt::merge_constant_structs	(	constant_struct_pointert	other,
		const widen_modet &	widen_mode
	)		const

private

Performs an element wise merge of the map for each struct.

Parameters

other	the other object being merged
widen_mode	Indicates if this is a widening merge

Returns: Returns a new abstract object that is the result of the merge unless the merge is the same as this abstract object, in which case it returns this.

Definition at line 254 of file full_struct_abstract_object.cpp.

◆ merge_location_context()

abstract_object_pointert full_struct_abstract_objectt::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 286 of file full_struct_abstract_object.cpp.

◆ mutable_clone()

internal_abstract_object_pointert full_struct_abstract_objectt::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 118 of file full_struct_abstract_object.h.

◆ output()

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

override

To provide a human readable string to the out representing the current known value about this object.

For this array we print: { .component_name=<output of object for component_name... }

Parameters

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

Definition at line 201 of file full_struct_abstract_object.cpp.

◆ read_component()

abstract_object_pointert full_struct_abstract_objectt::read_component	(	const abstract_environmentt &	environment,
		const exprt &	expr,
		const namespacet &	ns
	)		const

overrideprotectedvirtual

A helper function to evaluate the abstract object contained within a struct.

More precise abstractions may override this to return more precise results.

Parameters

environment	the abstract environment
expr	the expression uses to access a specific component
ns	the current namespace

Returns: The abstract object representing the value of that component. For this abstraction this will always be top since we are not tracking the struct.

Reimplemented from abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >.

Definition at line 71 of file full_struct_abstract_object.cpp.

◆ statistics()

void full_struct_abstract_objectt::statistics	(	abstract_object_statisticst &	statistics,
		abstract_object_visitedt &	visited,
		const abstract_environmentt &	env,
		const namespacet &	ns
	)		const

overridevirtual

Implements abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >.

Definition at line 326 of file full_struct_abstract_object.cpp.

◆ to_predicate_internal()

exprt full_struct_abstract_objectt::to_predicate_internal ( const exprt & name ) const

overrideprotectedvirtual

to_predicate implementation - derived classes will override

Parameters

name	- the variable name to substitute into the expression

Returns: Returns an exprt representing the object as an invariant.

Reimplemented from abstract_objectt.

Definition at line 303 of file full_struct_abstract_object.cpp.

◆ verify()

bool full_struct_abstract_objectt::verify ( ) const

overrideprotectedvirtual

Function: full_struct_abstract_objectt::verify.

Returns: Returns true if the struct is valid

To validate that the struct object is in a valid state. This means either it is top or bottom, or if neither of those then there exists something in the map of components. If there is something in the map, then it can't be top or bottom

Reimplemented from abstract_objectt.

Definition at line 235 of file full_struct_abstract_object.cpp.

◆ visit_sub_elements()

abstract_object_pointert full_struct_abstract_objectt::visit_sub_elements ( const abstract_object_visitort & visitor ) const

overridevirtual

Apply a visitor operation to all sub elements of this abstract_object.

A sub element might be a member of a struct, or an element of an array, for instance, but this is entirely determined by the particular derived instance of abstract_objectt.

Parameters

visitor an instance of a visitor class that will be applied to all sub elements

Returns: A new abstract_object if it's contents is modifed, or this if no modification is needed

Reimplemented from abstract_objectt.

Definition at line 292 of file full_struct_abstract_object.cpp.

◆ write_component()

abstract_object_pointert full_struct_abstract_objectt::write_component	(	abstract_environmentt &	environment,
		const namespacet &	ns,
		const std::stack< exprt > &	stack,
		const exprt &	expr,
		const abstract_object_pointert &	value,
		bool	merging_write
	)		const

overrideprotectedvirtual

A helper function to evaluate writing to a component of a struct.

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
expr	the expression uses to access a specific component
value	the value we are trying to write to the component
merging_write	whether to over-write or to merge with the current value. In other words is there any certainty that this write will happen.

Returns: The struct_abstract_objectt representing the result of writing to a specific component. In this case this will always be top as we are not tracking the value of this struct.

Reimplemented from abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >.

Definition at line 106 of file full_struct_abstract_object.cpp.

◆ write_location_context()

abstract_object_pointert full_struct_abstract_objectt::write_location_context ( const locationt & location ) const

overridevirtual

Update the 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 280 of file full_struct_abstract_object.cpp.

Member Data Documentation

◆ map

shared_struct_mapt full_struct_abstract_objectt::map

private

Definition at line 103 of file full_struct_abstract_object.h.

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

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

Public Types
typedef sharing_ptrt< full_struct_abstract_objectt >	constant_struct_pointert

typedef abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >	abstract_aggregate_baset

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

Public Types

Public Member Functions

Protected Member Functions

Private Types

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ abstract_aggregate_baset

◆ constant_struct_pointert

◆ shared_struct_mapt

Constructor & Destructor Documentation

◆ full_struct_abstract_objectt() [1/3]

◆ full_struct_abstract_objectt() [2/3]

◆ full_struct_abstract_objectt() [3/3]

Member Function Documentation

◆ merge()

◆ merge_constant_structs()

◆ merge_location_context()

◆ mutable_clone()

◆ output()

◆ read_component()

◆ statistics()

◆ to_predicate_internal()

◆ verify()

◆ visit_sub_elements()

◆ write_component()

◆ write_location_context()

Member Data Documentation

◆ map