Wrapper for a function dereferencing pointer expressions using a value set. More...

#include <value_set_dereference.h>

Collaboration diagram for value_set_dereferencet:

Classes
class	valuet
	Return value for `build_reference_to`; see that method for documentation. More...

Public Member Functions
	value_set_dereferencet (const namespacet &_ns, symbol_table_baset &_new_symbol_table, dereference_callbackt &_dereference_callback, const irep_idt _language_mode, bool _exclude_null_derefs, message_handlert &_message_handler)

virtual	~value_set_dereferencet ()

exprt	dereference (const exprt &pointer, bool display_points_to_sets=false)
	Dereference the given pointer-expression.

Static Public Member Functions
static bool	should_ignore_value (const exprt &what, bool exclude_null_derefs, const irep_idt &language_mode)
	Determine whether possible alias `what` should be ignored when replacing a pointer by its referees.

static valuet	build_reference_to (const exprt &what, const exprt &pointer, const namespacet &ns)

static bool	dereference_type_compare (const typet &object_type, const typet &dereference_type, const namespacet &ns)
	Check if the two types have matching number of ID_pointer levels, with the dereference type eventually pointing to void; then this is ok for example:

static bool	memory_model (exprt &value, const typet &type, const exprt &offset, const namespacet &ns)
	Replace `value` by an expression of type `to_type` corresponding to the value at memory address `value + offset`.

static bool	memory_model_bytes (exprt &value, const typet &type, const exprt &offset, const namespacet &ns)
	Replace `value` by an expression of type `to_type` corresponding to the value at memory address `value + offset`.

Private Member Functions
valuet	get_failure_value (const exprt &pointer, const typet &type)

exprt	handle_dereference_base_case (const exprt &pointer, bool display_points_to_sets)

Private Attributes
const namespacet &	ns

symbol_table_baset &	new_symbol_table

dereference_callbackt &	dereference_callback

const irep_idt	language_mode
	language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise.

const bool	exclude_null_derefs
	Flag indicating whether `value_set_dereferencet::dereference` should disregard an apparent attempt to dereference NULL.

message_handlert &	message_handler

Detailed Description

Wrapper for a function dereferencing pointer expressions using a value set.

Definition at line 22 of file value_set_dereference.h.

Constructor & Destructor Documentation

◆ value_set_dereferencet()

value_set_dereferencet::value_set_dereferencet	(	const namespacet &	_ns,
		symbol_table_baset &	_new_symbol_table,
		dereference_callbackt &	_dereference_callback,
		const irep_idt	_language_mode,
		bool	_exclude_null_derefs,
		message_handlert &	_message_handler
	)

inline

Parameters

_ns	Namespace
_new_symbol_table	A symbol_table to store new symbols in
_dereference_callback	Callback object for getting the set of objects a given pointer may point to.
_language_mode	Mode for any new symbols created to represent a dereference failure
_exclude_null_derefs	Ignore value-set entries that indicate a
_message_handler	Message handler for displaying points-to set

Definition at line 34 of file value_set_dereference.h.

◆ ~value_set_dereferencet()

virtual value_set_dereferencet::~value_set_dereferencet ( )

inlinevirtual

Definition at line 49 of file value_set_dereference.h.

Member Function Documentation

◆ build_reference_to()

value_set_dereferencet::valuet value_set_dereferencet::build_reference_to	(	const exprt &	what,
		const exprt &	pointer_expr,
		const namespacet &	ns
	)

static

Parameters

what	value set entry to convert to an expression: either ID_unknown, ID_invalid, or an object_descriptor_exprt giving a referred object and offset.
pointer_expr	pointer expression that may point to `what`
ns	A namespace

Returns: a valuet object containing guard and value fields. The guard is an appropriate check to determine whether pointer_expr really points to what; for example pointer_expr == &what. The value corresponds to the dereferenced pointer_expr assuming it is pointing to the object described by what. For example, we might return {.value = global, .pointer_guard = (pointer_expr == &global)}

Definition at line 460 of file value_set_dereference.cpp.

◆ dereference()

exprt value_set_dereferencet::dereference	(	const exprt &	pointer,
		bool	display_points_to_sets = `false`
	)

Dereference the given pointer-expression.

Any errors are reported to the callback method given in the constructor.

Parameters

pointer	A pointer-typed expression, to be dereferenced.
display_points_to_sets	Display size and contents of points to sets

Definition at line 143 of file value_set_dereference.cpp.

◆ dereference_type_compare()

bool value_set_dereferencet::dereference_type_compare	(	const typet &	object_type,
		const typet &	dereference_type,
		const namespacet &	ns
	)

static

Check if the two types have matching number of ID_pointer levels, with the dereference type eventually pointing to void; then this is ok for example:

dereference_type=void is ok (no matter what object_type is);
object_type=(int *), dereference_type=(void *) is ok;
object_type=(int **), dereference_type=(void **) is ok;
object_type=(int **), dereference_type=(void *) is ok;
object_type=(int *), dereference_type=(void **) is not ok;

Definition at line 341 of file value_set_dereference.cpp.

◆ get_failure_value()

value_set_dereferencet::valuet value_set_dereferencet::get_failure_value	(	const exprt &	pointer,
		const typet &	type
	)

private

Definition at line 294 of file value_set_dereference.cpp.

◆ handle_dereference_base_case()

exprt value_set_dereferencet::handle_dereference_base_case	(	const exprt &	pointer,
		bool	display_points_to_sets
	)

private

Definition at line 216 of file value_set_dereference.cpp.

◆ memory_model()

bool value_set_dereferencet::memory_model	(	exprt &	value,
		const typet &	to_type,
		const exprt &	offset,
		const namespacet &	ns
	)

static

Replace value by an expression of type to_type corresponding to the value at memory address value + offset.

If value is a bitvector or pointer of the same size as to_type, make value into the typecast expression (to_type)value. Otherwise perform the same operation as value_set_dereferencet::memory_model_bytes

Returns: true on success

Definition at line 708 of file value_set_dereference.cpp.

◆ memory_model_bytes()

bool value_set_dereferencet::memory_model_bytes	(	exprt &	value,
		const typet &	to_type,
		const exprt &	offset,
		const namespacet &	ns
	)

static

Replace value by an expression of type to_type corresponding to the value at memory address value + offset.

If the type of value is an array of bitvectors of size 1 byte, and to_type also is bitvector of size 1 byte, then the resulting expression is value[offset] or (to_type)value[offset] when typecast is required. Otherwise the expression is byte_extract(value, offset).

Returns: false if the conversion cannot be made

Definition at line 755 of file value_set_dereference.cpp.

◆ should_ignore_value()

bool value_set_dereferencet::should_ignore_value	(	const exprt &	what,
		bool	exclude_null_derefs,
		const irep_idt &	language_mode
	)

static

Determine whether possible alias what should be ignored when replacing a pointer by its referees.

We currently ignore a null object when exclude_null_derefs is true (pass true if you know the dereferenced pointer cannot be null), and also ignore integer addresses when language_mode is "java"

Parameters

what	value set entry to convert to an expression: either ID_unknown, ID_invalid, or an object_descriptor_exprt giving a referred object and offset.
exclude_null_derefs	Ignore value-set entries that indicate a given dereference may follow a null pointer
language_mode	Mode for any new symbols created to represent a dereference failure

Returns: true if what should be ignored as a possible alias

Definition at line 423 of file value_set_dereference.cpp.

Member Data Documentation

◆ dereference_callback

dereference_callbackt& value_set_dereferencet::dereference_callback

private

Definition at line 101 of file value_set_dereference.h.

◆ exclude_null_derefs

const bool value_set_dereferencet::exclude_null_derefs

private

Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to dereference NULL.

Definition at line 107 of file value_set_dereference.h.

◆ language_mode

const irep_idt value_set_dereferencet::language_mode

private

language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise.

Definition at line 104 of file value_set_dereference.h.

◆ message_handler

message_handlert& value_set_dereferencet::message_handler

private

Definition at line 108 of file value_set_dereference.h.

◆ new_symbol_table

symbol_table_baset& value_set_dereferencet::new_symbol_table

private

Definition at line 100 of file value_set_dereference.h.

◆ ns

const namespacet& value_set_dereferencet::ns

private

Definition at line 99 of file value_set_dereference.h.

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

/home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set_dereference.h
/home/runner/work/cbmc/cbmc/src/pointer-analysis/value_set_dereference.cpp

Classes

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ value_set_dereferencet()

◆ ~value_set_dereferencet()

Member Function Documentation

◆ build_reference_to()

◆ dereference()

◆ dereference_type_compare()

◆ get_failure_value()

◆ handle_dereference_base_case()

◆ memory_model()

◆ memory_model_bytes()

◆ should_ignore_value()

Member Data Documentation

◆ dereference_callback

◆ exclude_null_derefs

◆ language_mode

◆ message_handler

◆ new_symbol_table

◆ ns