cprover
value_set_dereferencet Class Reference

TO_BE_DOCUMENTED. More...

#include <value_set_dereference.h>

Collaboration diagram for value_set_dereferencet:
[legend]

Classes

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

Public Types

enum  modet { modet::READ, modet::WRITE }
 
typedef std::unordered_set< exprt, irep_hashexpr_sett
 

Public Member Functions

 value_set_dereferencet (const namespacet &_ns, symbol_tablet &_new_symbol_table, const optionst &_options, dereference_callbackt &_dereference_callback, const irep_idt _language_mode, bool _exclude_null_derefs)
 Constructor. More...
 
virtual ~value_set_dereferencet ()
 
virtual exprt dereference (const exprt &pointer, const guardt &guard, const modet mode)
 

Private Member Functions

bool dereference_type_compare (const typet &object_type, const typet &dereference_type) const
 
void offset_sum (exprt &dest, const exprt &offset) const
 
valuet build_reference_to (const exprt &what, const modet mode, const exprt &pointer, const guardt &guard)
 Get a guard and expression to access what under guard. More...
 
bool get_value_guard (const exprt &symbol, const exprt &premise, exprt &value)
 
void bounds_check (const index_exprt &expr, const guardt &guard)
 
void valid_check (const exprt &expr, const guardt &guard, const modet mode)
 
void invalid_pointer (const exprt &expr, const guardt &guard)
 
bool memory_model (exprt &value, const typet &type, const guardt &guard, const exprt &offset)
 
bool memory_model_conversion (exprt &value, const typet &type, const guardt &guard, const exprt &offset)
 
bool memory_model_bytes (exprt &value, const typet &type, const guardt &guard, const exprt &offset)
 

Static Private Member Functions

static const exprtget_symbol (const exprt &object)
 

Private Attributes

const namespacetns
 
symbol_tabletnew_symbol_table
 
const optionstoptions
 
dereference_callbacktdereference_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. More...
 
const bool exclude_null_derefs
 Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to dereference NULL. More...
 

Static Private Attributes

static unsigned invalid_counter =0
 

Detailed Description

TO_BE_DOCUMENTED.

Definition at line 29 of file value_set_dereference.h.

Member Typedef Documentation

◆ expr_sett

typedef std::unordered_set<exprt, irep_hash> value_set_dereferencet::expr_sett

Definition at line 81 of file value_set_dereference.h.

Member Enumeration Documentation

◆ modet

Enumerator
READ 
WRITE 

Definition at line 60 of file value_set_dereference.h.

Constructor & Destructor Documentation

◆ value_set_dereferencet()

value_set_dereferencet::value_set_dereferencet ( const namespacet _ns,
symbol_tablet _new_symbol_table,
const optionst _options,
dereference_callbackt _dereference_callback,
const irep_idt  _language_mode,
bool  _exclude_null_derefs 
)
inline

Constructor.

Parameters
_nsNamespace
_new_symbol_tableA symbol_table to store new symbols in
_optionsOptions, in particular whether pointer checks are to be performed
_dereference_callbackCallback object for error reporting
_language_modeMode for any new symbols created to represent a dereference failure
_exclude_null_derefsIgnore value-set entries that indicate a given dereference may follow a null pointer

Definition at line 43 of file value_set_dereference.h.

◆ ~value_set_dereferencet()

virtual value_set_dereferencet::~value_set_dereferencet ( )
inlinevirtual

Definition at line 58 of file value_set_dereference.h.

Member Function Documentation

◆ bounds_check()

◆ build_reference_to()

value_set_dereferencet::valuet value_set_dereferencet::build_reference_to ( const exprt what,
const modet  mode,
const exprt pointer,
const guardt guard 
)
private

Get a guard and expression to access what under guard.

Parameters
whatvalue set entry to convert to an expression: either ID_unknown, ID_invalid, or an object_descriptor_exprt giving a referred object and offset.
modewhether the pointer is being read or written; used to create pointer validity checks if need be
pointerpointer expression that may point to what
guardguard under which the pointer is dereferenced
Returns
  • If we were explicitly instructed to ignore what as a possible pointer target: a valuet with ignore = true, and value and pointer_guard set to nil.
  • If we could build an expression corresponding to what: A valuet with non-nil value, and pointer_guard set to an appropriate check to determine if pointer_expr really points to what (for example, we might return {.value = global, .pointer_guard = (pointer_expr == &global)}
  • Otherwise, if we couldn't build an expression (e.g. for what == ID_unknown), a valuet with nil value and ignore == false.

Definition at line 288 of file value_set_dereference.cpp.

References guardt::add(), configt::ansi_c, base_type_eq(), bounds_check(), byte_extract_id(), config, CPROVER_PREFIX, deallocated(), dereference_callback, dereference_callbackt::dereference_failure(), dereference_type_compare(), dynamic_object(), dynamic_object_lower_bound(), dynamic_object_upper_bound(), configt::ansi_ct::endianness, exclude_null_derefs, namespace_baset::follow(), format(), from_integer(), optionst::get_bool_option(), get_subexpression_at_offset(), irept::id(), irept::id_string(), value_set_dereferencet::valuet::ignore, invalid_pointer(), exprt::is_constant(), exprt::is_zero(), language_mode, binary_relation_exprt::lhs(), namespacet::lookup(), exprt::make_typecast(), malloc_object(), memory_model(), symbolt::name, configt::ansi_ct::NO_ENDIANNESS, ns, null_object(), null_pointer(), object_descriptor_exprt::object(), object_descriptor_exprt::offset(), options, value_set_dereferencet::valuet::pointer_guard, pointer_offset(), pointer_offset_size(), irept::pretty(), binary_relation_exprt::rhs(), object_descriptor_exprt::root_object(), same_object(), size_of_expr(), typet::subtype(), to_object_descriptor_expr(), symbolt::type, exprt::type(), valid_check(), and value_set_dereferencet::valuet::value.

Referenced by dereference().

◆ dereference()

exprt value_set_dereferencet::dereference ( const exprt pointer,
const guardt guard,
const modet  mode 
)
virtual

The method 'dereference' dereferences the given pointer-expression. Any errors are reported to the callback method given in the constructor.

Parameters
pointerA pointer-typed expression, to be dereferenced.
guardA guard, which is assumed to hold when dereferencing.
modeIndicates whether the dereferencing is a load or store.
parameters: expression dest, to be dereferenced under given guard,
and given mode
Returns
returns pointer after dereferencing

Definition at line 48 of file value_set_dereference.cpp.

References guardt::add(), build_reference_to(), if_exprt::cond(), dereference_callback, if_exprt::false_case(), format(), get_fresh_aux_symbol(), dereference_callbackt::get_value_set(), dereference_callbackt::has_failed_symbol(), irept::id(), value_set_dereferencet::valuet::ignore, invalid_pointer(), symbolt::is_lvalue, irept::is_nil(), language_mode, new_symbol_table, value_set_dereferencet::valuet::pointer_guard, irept::pretty(), irept::set(), exprt::source_location(), typet::subtype(), symbolt::symbol_expr(), to_if_expr(), if_exprt::true_case(), exprt::type(), and value_set_dereferencet::valuet::value.

Referenced by goto_program_dereferencet::dereference_rec().

◆ dereference_type_compare()

bool value_set_dereferencet::dereference_type_compare ( const typet object_type,
const typet dereference_type 
) const
private

◆ get_symbol()

const exprt & value_set_dereferencet::get_symbol ( const exprt object)
staticprivate

Definition at line 37 of file value_set_dereference.cpp.

References irept::id(), and exprt::op0().

Referenced by valid_check().

◆ get_value_guard()

bool value_set_dereferencet::get_value_guard ( const exprt symbol,
const exprt premise,
exprt value 
)
private

◆ invalid_pointer()

void value_set_dereferencet::invalid_pointer ( const exprt expr,
const guardt guard 
)
private

◆ memory_model()

bool value_set_dereferencet::memory_model ( exprt value,
const typet type,
const guardt guard,
const exprt offset 
)
private

◆ memory_model_bytes()

◆ memory_model_conversion()

bool value_set_dereferencet::memory_model_conversion ( exprt value,
const typet type,
const guardt guard,
const exprt offset 
)
private

◆ offset_sum()

void value_set_dereferencet::offset_sum ( exprt dest,
const exprt offset 
) const
private

◆ valid_check()

Member Data Documentation

◆ dereference_callback

dereference_callbackt& value_set_dereferencet::dereference_callback
private

◆ 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 93 of file value_set_dereference.h.

Referenced by build_reference_to().

◆ invalid_counter

unsigned int value_set_dereferencet::invalid_counter =0
staticprivate

Definition at line 94 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 90 of file value_set_dereference.h.

Referenced by build_reference_to(), and dereference().

◆ new_symbol_table

symbol_tablet& value_set_dereferencet::new_symbol_table
private

Definition at line 85 of file value_set_dereference.h.

Referenced by dereference().

◆ ns

const namespacet& value_set_dereferencet::ns
private

◆ options

const optionst& value_set_dereferencet::options
private

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