cprover
value_set_dereference.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pointer Dereferencing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
14 
15 #include <unordered_set>
16 
17 #include <util/message.h>
18 #include <util/std_expr.h>
19 
20 #include "dereference_callback.h"
21 
22 class symbol_tablet;
23 class optionst;
24 class symbolt;
25 
28 {
29 public:
37  // given dereference may follow a null pointer
40  const namespacet &_ns,
41  symbol_tablet &_new_symbol_table,
42  dereference_callbackt &_dereference_callback,
43  const irep_idt _language_mode,
44  bool _exclude_null_derefs,
45  const messaget &_log)
46  : ns(_ns),
47  new_symbol_table(_new_symbol_table),
48  dereference_callback(_dereference_callback),
49  language_mode(_language_mode),
50  exclude_null_derefs(_exclude_null_derefs),
51  log(_log)
52  { }
53 
55 
60  exprt dereference(const exprt &pointer, bool display_points_to_sets = false);
61 
66  try_add_offset_to_indices(const exprt &expr, const exprt &offset);
67 
69  class valuet
70  {
71  public:
75 
78  {
79  }
80  };
81 
82  static bool should_ignore_value(
83  const exprt &what,
85  const irep_idt &language_mode);
86 
87  static valuet build_reference_to(
88  const exprt &what,
89  const exprt &pointer,
90  const namespacet &ns);
91 
92  static bool dereference_type_compare(
93  const typet &object_type,
94  const typet &dereference_type,
95  const namespacet &ns);
96 
97  static bool memory_model(
98  exprt &value,
99  const typet &type,
100  const exprt &offset,
101  const namespacet &ns);
102 
103  static bool memory_model_bytes(
104  exprt &value,
105  const typet &type,
106  const exprt &offset,
107  const namespacet &ns);
108 
109 private:
110  const namespacet &ns;
119  const messaget &log;
120  valuet get_failure_value(const exprt &pointer, const typet &type);
122  const exprt &pointer,
123  bool display_points_to_sets);
124 };
125 
126 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
value_set_dereferencet::valuet
Return value for build_reference_to; see that method for documentation.
Definition: value_set_dereference.h:70
value_set_dereferencet::valuet::pointer_guard
exprt pointer_guard
Definition: value_set_dereference.h:74
value_set_dereferencet::memory_model
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 + o...
Definition: value_set_dereference.cpp:684
optionst
Definition: options.h:23
value_set_dereferencet::ns
const namespacet & ns
Definition: value_set_dereference.h:110
typet
The type of an expression, extends irept.
Definition: type.h:28
dereference_callbackt
Base class for pointer value set analysis.
Definition: dereference_callback.h:28
value_set_dereferencet::language_mode
const irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
Definition: value_set_dereference.h:115
value_set_dereferencet::should_ignore_value
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.
Definition: value_set_dereference.cpp:407
value_set_dereferencet::exclude_null_derefs
const bool exclude_null_derefs
Flag indicating whether value_set_dereferencet::dereference should disregard an apparent attempt to d...
Definition: value_set_dereference.h:118
exprt
Base class for all expressions.
Definition: expr.h:54
value_set_dereferencet::get_failure_value
valuet get_failure_value(const exprt &pointer, const typet &type)
Definition: value_set_dereference.cpp:282
value_set_dereferencet::~value_set_dereferencet
virtual ~value_set_dereferencet()
Definition: value_set_dereference.h:54
value_set_dereferencet::dereference_type_compare
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 eventuall...
Definition: value_set_dereference.cpp:329
value_set_dereferencet::new_symbol_table
symbol_tablet & new_symbol_table
Definition: value_set_dereference.h:111
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
value_set_dereferencet::log
const messaget & log
Definition: value_set_dereference.h:119
value_set_dereferencet::valuet::pointer
exprt pointer
Definition: value_set_dereference.h:73
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
value_set_dereferencet::dereference_callback
dereference_callbackt & dereference_callback
Definition: value_set_dereference.h:112
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
value_set_dereferencet::memory_model_bytes
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 + o...
Definition: value_set_dereference.cpp:731
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
value_set_dereferencet::valuet::valuet
valuet()
Definition: value_set_dereference.h:76
value_set_dereferencet
Wrapper for a function dereferencing pointer expressions using a value set.
Definition: value_set_dereference.h:28
symbolt
Symbol table entry.
Definition: symbol.h:28
dereference_callback.h
Pointer Dereferencing.
value_set_dereferencet::build_reference_to
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
Definition: value_set_dereference.cpp:444
value_set_dereferencet::value_set_dereferencet
value_set_dereferencet(const namespacet &_ns, symbol_tablet &_new_symbol_table, dereference_callbackt &_dereference_callback, const irep_idt _language_mode, bool _exclude_null_derefs, const messaget &_log)
Definition: value_set_dereference.h:39
value_set_dereferencet::try_add_offset_to_indices
optionalt< exprt > try_add_offset_to_indices(const exprt &expr, const exprt &offset)
If expr is of the form (c1 ? e1[o1] : c2 ? e2[o2] : c3 ? ...) then return c1 ? e1[o1 + offset] : e2[o...
Definition: value_set_dereference.cpp:103
message.h
std_expr.h
API to expression classes.
value_set_dereferencet::dereference
exprt dereference(const exprt &pointer, bool display_points_to_sets=false)
Dereference the given pointer-expression.
Definition: value_set_dereference.cpp:133
value_set_dereferencet::valuet::value
exprt value
Definition: value_set_dereference.h:72
value_set_dereferencet::handle_dereference_base_case
exprt handle_dereference_base_case(const exprt &pointer, bool display_points_to_sets)
Definition: value_set_dereference.cpp:205