cprover
value_set.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_H
13 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_H
14 
15 #include <set>
16 
17 #include <util/mp_arith.h>
19 
20 #include "object_numbering.h"
21 #include "value_sets.h"
22 
23 class namespacet;
24 
26 {
27 public:
29  {
30  }
31 
32  static bool field_sensitive(
33  const irep_idt &id,
34  const typet &type,
35  const namespacet &);
36 
37  unsigned location_number;
39 
40  typedef irep_idt idt;
41 
42  class objectt
43  {
44  public:
46  {
47  }
48 
49  explicit objectt(const mp_integer &_offset):
50  offset(_offset),
51  offset_is_set(true)
52  {
53  }
54 
57  bool offset_is_zero() const
58  { return offset_is_set && offset.is_zero(); }
59  };
60 
61  class object_map_dt:public std::map<unsigned, objectt>
62  {
63  public:
65  static const object_map_dt blank;
66  };
67 
68  exprt to_expr(object_map_dt::const_iterator it) const;
69 
71 
72  void set(object_mapt &dest, object_map_dt::const_iterator it) const
73  {
74  dest.write()[it->first]=it->second;
75  }
76 
77  bool insert(object_mapt &dest, object_map_dt::const_iterator it) const
78  {
79  return insert(dest, it->first, it->second);
80  }
81 
82  bool insert(object_mapt &dest, const exprt &src) const
83  {
84  return insert(dest, object_numbering.number(src), objectt());
85  }
86 
87  bool insert(
88  object_mapt &dest,
89  const exprt &src,
90  const mp_integer &offset) const
91  {
92  return insert(dest, object_numbering.number(src), objectt(offset));
93  }
94 
95  bool insert(object_mapt &dest, unsigned n, const objectt &object) const;
96 
97  bool insert(object_mapt &dest, const exprt &expr, const objectt &object) const
98  {
99  return insert(dest, object_numbering.number(expr), object);
100  }
101 
102  struct entryt
103  {
106  std::string suffix;
107 
109  {
110  }
111 
112  entryt(const idt &_identifier, const std::string &_suffix):
113  identifier(_identifier),
114  suffix(_suffix)
115  {
116  }
117  };
118 
119  typedef std::set<exprt> expr_sett;
120 
121  typedef std::set<unsigned int> dynamic_object_id_sett;
122 
123  #ifdef USE_DSTRING
124  typedef std::map<idt, entryt> valuest;
125  #else
126  typedef std::unordered_map<idt, entryt, string_hash> valuest;
127  #endif
128 
129  void get_value_set(
130  const exprt &expr,
131  value_setst::valuest &dest,
132  const namespacet &ns) const;
133 
134  expr_sett &get(
135  const idt &identifier,
136  const std::string &suffix);
137 
138  void make_any()
139  {
140  values.clear();
141  }
142 
143  void clear()
144  {
145  values.clear();
146  }
147 
148  entryt &get_entry(
149  const entryt &e, const typet &type,
150  const namespacet &);
151 
152  void output(
153  const namespacet &ns,
154  std::ostream &out) const;
155 
157 
158  // true = added something new
159  bool make_union(object_mapt &dest, const object_mapt &src) const;
160 
161  // true = added something new
162  bool make_union(const valuest &new_values);
163 
164  // true = added something new
165  bool make_union(const value_sett &new_values)
166  {
167  return make_union(new_values.values);
168  }
169 
170  void guard(
171  const exprt &expr,
172  const namespacet &ns);
173 
174  void apply_code(
175  const codet &code,
176  const namespacet &ns);
177 
178  void assign(
179  const exprt &lhs,
180  const exprt &rhs,
181  const namespacet &ns,
182  bool is_simplified,
183  bool add_to_sets);
184 
185  void do_function_call(
186  const irep_idt &function,
187  const exprt::operandst &arguments,
188  const namespacet &ns);
189 
190  // edge back to call site
191  void do_end_function(
192  const exprt &lhs,
193  const namespacet &ns);
194 
195  void get_reference_set(
196  const exprt &expr,
197  value_setst::valuest &dest,
198  const namespacet &ns) const;
199 
200  bool eval_pointer_offset(
201  exprt &expr,
202  const namespacet &ns) const;
203 
204 protected:
205  void get_value_set_rec(
206  const exprt &expr,
207  object_mapt &dest,
208  const std::string &suffix,
209  const typet &original_type,
210  const namespacet &ns) const;
211 
212  void get_value_set(
213  const exprt &expr,
214  object_mapt &dest,
215  const namespacet &ns,
216  bool is_simplified) const;
217 
219  const exprt &expr,
220  object_mapt &dest,
221  const namespacet &ns) const
222  {
223  get_reference_set_rec(expr, dest, ns);
224  }
225 
227  const exprt &expr,
228  object_mapt &dest,
229  const namespacet &ns) const;
230 
231  void dereference_rec(
232  const exprt &src,
233  exprt &dest) const;
234 
235  void assign_rec(
236  const exprt &lhs,
237  const object_mapt &values_rhs,
238  const std::string &suffix,
239  const namespacet &ns,
240  bool add_to_sets);
241 
242  void do_free(
243  const exprt &op,
244  const namespacet &ns);
245 
247  const exprt &src,
248  const irep_idt &component_name,
249  const namespacet &ns);
250 };
251 
252 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H
The type of an expression.
Definition: type.h:20
bool insert(object_mapt &dest, object_map_dt::const_iterator it) const
Definition: value_set.h:77
BigInt mp_integer
Definition: mp_arith.h:19
objectt(const mp_integer &_offset)
Definition: value_set.h:49
object_mapt object_map
Definition: value_set.h:104
entryt(const idt &_identifier, const std::string &_suffix)
Definition: value_set.h:112
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Definition: value_set.cpp:1089
bool make_union(object_mapt &dest, const object_mapt &src) const
Definition: value_set.cpp:246
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
Definition: value_set.cpp:924
bool offset_is_zero() const
Definition: value_set.h:57
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Definition: value_set.cpp:314
static const object_map_dt blank
Definition: value_set.h:65
static object_numberingt object_numbering
Definition: value_set.h:38
void dereference_rec(const exprt &src, exprt &dest) const
Definition: value_set.cpp:891
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
Definition: value_set.cpp:1290
mp_integer offset
Definition: value_set.h:55
exprt to_expr(object_map_dt::const_iterator it) const
Definition: value_set.cpp:187
static bool field_sensitive(const irep_idt &id, const typet &type, const namespacet &)
Definition: value_set.cpp:39
irep_idt idt
Definition: value_set.h:40
bool eval_pointer_offset(exprt &expr, const namespacet &ns) const
Definition: value_set.cpp:261
Value Set Propagation.
std::set< exprt > expr_sett
Definition: value_set.h:119
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Definition: value_set.cpp:1423
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
Definition: value_set.cpp:348
bool insert(object_mapt &dest, const exprt &src) const
Definition: value_set.h:82
bool insert(object_mapt &dest, const exprt &src, const mp_integer &offset) const
Definition: value_set.h:87
void make_any()
Definition: value_set.h:138
std::vector< exprt > operandst
Definition: expr.h:49
std::unordered_map< idt, entryt, string_hash > valuest
Definition: value_set.h:126
entryt & get_entry(const entryt &e, const typet &type, const namespacet &)
Definition: value_set.cpp:54
void do_end_function(const exprt &lhs, const namespacet &ns)
Definition: value_set.cpp:1469
bool insert(object_mapt &dest, const exprt &expr, const objectt &object) const
Definition: value_set.h:97
void get_reference_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Definition: value_set.cpp:909
Base class for all expressions.
Definition: expr.h:46
Reference Counting.
std::set< unsigned int > dynamic_object_id_sett
Definition: value_set.h:121
value_sett()
Definition: value_set.h:28
void clear()
Definition: value_set.h:143
bool make_union(const value_sett &new_values)
Definition: value_set.h:165
void output(const namespacet &ns, std::ostream &out) const
Definition: value_set.cpp:97
A statement in a programming language.
Definition: std_code.h:19
void guard(const exprt &expr, const namespacet &ns)
Definition: value_set.cpp:1616
void do_free(const exprt &op, const namespacet &ns)
Definition: value_set.cpp:1210
number_type number(const T &a)
Definition: numbering.h:80
std::list< exprt > valuest
Definition: value_sets.h:28
void get_reference_set(const exprt &expr, object_mapt &dest, const namespacet &ns) const
Definition: value_set.h:218
std::string suffix
Definition: value_set.h:106
valuest values
Definition: value_set.h:156
void apply_code(const codet &code, const namespacet &ns)
Definition: value_set.cpp:1481
unsigned location_number
Definition: value_set.h:37
reference_counting< object_map_dt > object_mapt
Definition: value_set.h:70
exprt make_member(const exprt &src, const irep_idt &component_name, const namespacet &ns)
Definition: value_set.cpp:1650