Data structures and algorithms used by smt2_incremental_decision_proceduret to track data about the objects which pointers point to. More...

#include <util/expr.h>
#include <util/pointer_expr.h>
#include <unordered_map>

Include dependency graph for object_tracking.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	decision_procedure_objectt
	Information the decision procedure holds about each object. More...

Typedefs
using	smt_object_mapt = std::unordered_map< exprt, decision_procedure_objectt, irep_hash >
	Mapping from an object's base expression to the set of information about it which we track. More...

Functions
exprt	find_object_base_expression (const address_of_exprt &address_of)
	The model of addresses we use consists of a unique object identifier and an offset. More...

template<typename output_object_functiont >
void	find_object_base_expressions (const exprt &expression, const output_object_functiont &output_object)
	Arbitrary expressions passed to the decision procedure may have multiple address of operations as its sub expressions. More...

smt_object_mapt	initial_smt_object_map ()
	Constructs an initial object map containing the null object. More...

void	track_expression_objects (const exprt &expression, const namespacet &ns, smt_object_mapt &object_map)
	Finds all the object expressions in the given expression and adds them to the object map for cases where the map does not contain them already. More...

bool	objects_are_already_tracked (const exprt &expression, const smt_object_mapt &object_map)
	Finds whether all base object expressions in the given expression are already tracked in the given object map. More...

exprt	make_invalid_pointer_expr ()
	Create the invalid pointer constant. More...

Detailed Description

Data structures and algorithms used by smt2_incremental_decision_proceduret to track data about the objects which pointers point to.

An object here is the whole of an allocated block of memory. Objects in this sense have no sub objects; only offsets. Valid examples of objects include -

Primitives stored on the stack such as int foo;.
Pointer primitives stored on the stack such as int *sam;.
The entirety of a struct stored on the stack such as - struct bart{int eggs, int ham} bar;
The entirety of an array stored on the stack such as int green[20];
The memory allocated by a malloc call - malloc(20). Examples of things / expressions which are not objects -
A pointer to a primitive stored on the stack, such as &foo or &sam. The value of these pointers encodes the combination of the unique object identifier of foo / sam objects and a (zero) offset, but these pointer values / memory addresses are not in themselves objects, although the values may be stored in another object. This is a distinction between values and the objects which contain them.
A field within a struct, such as bar.ham from the previous example. A pointer to this field is an offset into the base bar object.
A pointer to element within an array, such as &(green[5]). A pointer to an element in this example is an offset into the base int green[20] object.
Note
The functionality in this file is intended to cover tracking objects and their sizes only. It does not track anything to do with the offsets into objects or the SMT encodings of objects / offsets / pointers.

Definition in file object_tracking.h.

Typedef Documentation

◆ smt_object_mapt

using smt_object_mapt = std::unordered_map<exprt, decision_procedure_objectt, irep_hash>

Mapping from an object's base expression to the set of information about it which we track.

Definition at line 90 of file object_tracking.h.

Function Documentation

◆ find_object_base_expression()

exprt find_object_base_expression ( const address_of_exprt & address_of )

The model of addresses we use consists of a unique object identifier and an offset.

In order to encode the offset identifiers we need to assign unique identifiers to the objects. This function finds the base object expression in an address of expression for which a unique identifier needs to be assigned.

Definition at line 18 of file object_tracking.cpp.

◆ find_object_base_expressions()

template<typename output_object_functiont >

void find_object_base_expressions	(	const exprt &	expression,
		const output_object_functiont &	output_object
	)

Arbitrary expressions passed to the decision procedure may have multiple address of operations as its sub expressions.

This means the overall expression may contain multiple base objects which need to be assigned unique identifiers.

Parameters

expression	The expression within which to find base objects.
output_object	This function is called with each of the base object expressions found, as they are found.

The found objects are returned through an output function in order to separate the implementation of the storage and deduplication of the results from finding the object expressions. The type of output_object is a template parameter in order to eliminate potential performance overheads of using std::function.

Definition at line 76 of file object_tracking.h.

◆ initial_smt_object_map()

smt_object_mapt initial_smt_object_map ( )

Constructs an initial object map containing the null object.

The null object must be added at construction in order to ensure it is allocated a unique identifier of 0.

Definition at line 69 of file object_tracking.cpp.

◆ make_invalid_pointer_expr()

exprt make_invalid_pointer_expr ( )

Create the invalid pointer constant.

Definition at line 13 of file object_tracking.cpp.

◆ objects_are_already_tracked()

bool objects_are_already_tracked	(	const exprt &	expression,
		const smt_object_mapt &	object_map
	)

Finds whether all base object expressions in the given expression are already tracked in the given object map.

This supports writing invariants on the base object expressions already being tracked in the map in contexts where the map is const.

Definition at line 120 of file object_tracking.cpp.

◆ track_expression_objects()

void track_expression_objects	(	const exprt &	expression,
		const namespacet &	ns,
		smt_object_mapt &	object_map
	)

Finds all the object expressions in the given expression and adds them to the object map for cases where the map does not contain them already.