#include <full_array_abstract_object.h>

Inheritance diagram for full_array_abstract_objectt:

Collaboration diagram for full_array_abstract_objectt:

Classes
struct	mp_integer_hasht

Public Types
typedef sharing_ptrt< full_array_abstract_objectt > const	full_array_pointert

typedef abstract_aggregate_objectt< full_array_abstract_objectt, array_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 Member Functions
	full_array_abstract_objectt (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...

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

void	output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
	the current known value about this object. More...

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

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

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

Public Member Functions inherited from abstract_aggregate_objectt< full_array_abstract_objectt, array_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. 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...

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

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

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

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

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

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

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

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

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 &env, const exprt &expr, const namespacet &ns) const override
	A helper function to read elements from an array. More...

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 index of an array. More...

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

abstract_object_pointert	merge (const abstract_object_pointert &other, const widen_modet &widen_mode) const override
	Tries to do an array/array merge if merging with a constant array If it can't, falls back to parent merge. More...

bool	verify () const override
	To validate that the struct object is in a valid state. More...

void	set_top_internal () override
	Perform any additional structural modifications when setting this object to TOP. 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 ()

Private Types
typedef sharing_mapt< mp_integer, abstract_object_pointert, false, mp_integer_hasht >	shared_array_mapt

Private Member Functions
abstract_object_pointert	read_element (const abstract_environmentt &env, const exprt &expr, const namespacet &ns) const

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

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

abstract_object_pointert	write_leaf_element (abstract_environmentt &environment, const namespacet &ns, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const

void	map_put (mp_integer index, const abstract_object_pointert &value, bool overrun)

abstract_object_pointert	map_find_or_top (mp_integer index, const abstract_environmentt &env, const namespacet &ns) const

abstract_object_pointert	get_top_entry (const abstract_environmentt &env, const namespacet &ns) const
	Short hand method for creating a top element of the array. More...

abstract_object_pointert	full_array_merge (const full_array_pointert &other, const widen_modet &widen_mode) const
	Merges an array into this array. More...

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

Private Attributes
shared_array_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. 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 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_array_abstract_objectt, array_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 21 of file full_array_abstract_object.h.

Member Typedef Documentation

◆ abstract_aggregate_baset

typedef abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet> full_array_abstract_objectt::abstract_aggregate_baset

Definition at line 30 of file full_array_abstract_object.h.

◆ full_array_pointert

typedef sharing_ptrt<full_array_abstract_objectt> const full_array_abstract_objectt::full_array_pointert

Definition at line 26 of file full_array_abstract_object.h.

◆ shared_array_mapt

typedef sharing_mapt< mp_integer, abstract_object_pointert, false, mp_integer_hasht> full_array_abstract_objectt::shared_array_mapt

private

Definition at line 199 of file full_array_abstract_object.h.

Constructor & Destructor Documentation

◆ full_array_abstract_objectt() [1/2]

full_array_abstract_objectt::full_array_abstract_objectt	(	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 67 of file full_array_abstract_object.cpp.

◆ full_array_abstract_objectt() [2/2]

full_array_abstract_objectt::full_array_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 the abstract object is being created in
ns	the namespace

Definition at line 76 of file full_array_abstract_object.cpp.

Member Function Documentation

◆ full_array_merge()

abstract_object_pointert full_array_abstract_objectt::full_array_merge	(	const full_array_pointert &	other,
		const widen_modet &	widen_mode
	)		const

private

Merges an array into this array.

Parameters

other	The object to merge in
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 123 of file full_array_abstract_object.cpp.

◆ get_top_entry()

abstract_object_pointert full_array_abstract_objectt::get_top_entry	(	const abstract_environmentt &	env,
		const namespacet &	ns
	)		const

private

Short hand method for creating a top element of the array.

Parameters

env	the abstract environment
ns	the namespace

Returns: An abstract object pointer of type type().subtype() (i.e. the type of the array's values).

Definition at line 387 of file full_array_abstract_object.cpp.

◆ map_find_or_top()

abstract_object_pointert full_array_abstract_objectt::map_find_or_top	(	mp_integer	index,
		const abstract_environmentt &	env,
		const namespacet &	ns
	)		const

private

Definition at line 376 of file full_array_abstract_object.cpp.

◆ map_put()

void full_array_abstract_objectt::map_put	(	mp_integer	index,
		const abstract_object_pointert &	value,
		bool	overrun
	)

private

Definition at line 354 of file full_array_abstract_object.cpp.

◆ merge()

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

overrideprotectedvirtual

Tries to do an array/array merge if merging with a constant array If it can't, falls back to parent merge.

Parameters

other	The object to merge in
widen_mode	Indicates if this is a widening merge

Returns: Returns the result of the merge.

Reimplemented from abstract_objectt.

Definition at line 111 of file full_array_abstract_object.cpp.

◆ merge_location_context()

abstract_object_pointert full_array_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 401 of file full_array_abstract_object.cpp.

◆ mutable_clone()

internal_abstract_object_pointert full_array_abstract_objectt::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 88 of file full_array_abstract_object.h.

◆ output()

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

override

the current known value about this object.

For this array we print: { [0] - <output of object at index 0... }

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 148 of file full_array_abstract_object.cpp.

◆ read_component()

abstract_object_pointert full_array_abstract_objectt::read_component	(	const abstract_environmentt &	env,
		const exprt &	expr,
		const namespacet &	ns
	)		const

overrideprotectedvirtual

A helper function to read elements from an array.

This will return the abstract object stored for that index, or top if we don't know about the specified index. If we can't resolve the index to a constant, we return top

Parameters

env	the environment
expr	the expression used to access the specific value in the array
ns	the namespace

Returns: An abstract object representing the value in the array

Reimplemented from abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >.

Definition at line 170 of file full_array_abstract_object.cpp.

◆ read_element()

abstract_object_pointert full_array_abstract_objectt::read_element	(	const abstract_environmentt &	env,
		const exprt &	expr,
		const namespacet &	ns
	)		const

private

Definition at line 208 of file full_array_abstract_object.cpp.

◆ set_top_internal()

void full_array_abstract_objectt::set_top_internal ( )

overrideprotectedvirtual

Perform any additional structural modifications when setting this object to TOP.

Reimplemented from abstract_objectt.

Definition at line 104 of file full_array_abstract_object.cpp.

◆ statistics()

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

overrideprotectedvirtual

Implements abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >.

Definition at line 440 of file full_array_abstract_object.cpp.

◆ to_predicate_internal()

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

overrideprivatevirtual

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 418 of file full_array_abstract_object.cpp.

◆ verify()

bool full_array_abstract_objectt::verify ( ) const

overrideprotectedvirtual

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

Returns: Returns true if the struct is valid

Reimplemented from abstract_objectt.

Definition at line 96 of file full_array_abstract_object.cpp.

◆ visit_sub_elements()

abstract_object_pointert full_array_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 407 of file full_array_abstract_object.cpp.

◆ write_component()

abstract_object_pointert full_array_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 index of an array.

Parameters

environment	the abstract environment
ns	the namespace
stack	the remaining stack of expressions on the LHS to evaluate
expr	the expression uses to access a specific index
value	the value we are trying to assign to that value in the array
merging_write	Should this and all future writes be merged with the current value

Returns: The abstract_object_pointert representing the result of writing to a specific index.

Reimplemented from abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >.

Definition at line 188 of file full_array_abstract_object.cpp.

◆ write_element()

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

private

Definition at line 236 of file full_array_abstract_object.cpp.

◆ write_leaf_element()

abstract_object_pointert full_array_abstract_objectt::write_leaf_element	(	abstract_environmentt &	environment,
		const namespacet &	ns,
		const exprt &	expr,
		const abstract_object_pointert &	value,
		bool	merging_write
	)		const

private

Definition at line 301 of file full_array_abstract_object.cpp.

◆ write_location_context()

abstract_object_pointert full_array_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 395 of file full_array_abstract_object.cpp.

◆ write_sub_element()

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

private

Definition at line 257 of file full_array_abstract_object.cpp.

Member Data Documentation

◆ map

shared_array_mapt full_array_abstract_objectt::map

private

Definition at line 201 of file full_array_abstract_object.h.

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

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

Classes

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

◆ full_array_pointert

◆ shared_array_mapt

Constructor & Destructor Documentation

◆ full_array_abstract_objectt() [1/2]

◆ full_array_abstract_objectt() [2/2]

Member Function Documentation

◆ full_array_merge()

◆ get_top_entry()

◆ map_find_or_top()

◆ map_put()

◆ merge()

◆ merge_location_context()

◆ mutable_clone()

◆ output()

◆ read_component()

◆ read_element()

◆ set_top_internal()

◆ statistics()

◆ to_predicate_internal()

◆ verify()

◆ visit_sub_elements()

◆ write_component()

◆ write_element()

◆ write_leaf_element()

◆ write_location_context()

◆ write_sub_element()

Member Data Documentation

◆ map