cprover
pointer_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes for Pointers
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_POINTER_EXPR_H
10 #define CPROVER_UTIL_POINTER_EXPR_H
11 
14 
15 #include "bitvector_types.h"
16 #include "std_expr.h"
17 
18 class namespacet;
19 
24 {
25 public:
26  pointer_typet(typet _subtype, std::size_t width)
27  : bitvector_typet(ID_pointer, width)
28  {
29  subtype().swap(_subtype);
30  }
31 
33  {
34  return signedbv_typet(get_width());
35  }
36 
37  static void check(
38  const typet &type,
40  {
41  DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width");
42  }
43 };
44 
48 template <>
49 inline bool can_cast_type<pointer_typet>(const typet &type)
50 {
51  return type.id() == ID_pointer;
52 }
53 
62 inline const pointer_typet &to_pointer_type(const typet &type)
63 {
66  return static_cast<const pointer_typet &>(type);
67 }
68 
71 {
74  return static_cast<pointer_typet &>(type);
75 }
76 
79 inline bool is_void_pointer(const typet &type)
80 {
81  return type.id() == ID_pointer && type.subtype().id() == ID_empty;
82 }
83 
89 {
90 public:
91  reference_typet(typet _subtype, std::size_t _width)
92  : pointer_typet(std::move(_subtype), _width)
93  {
94  set(ID_C_reference, true);
95  }
96 
97  static void check(
98  const typet &type,
100  {
101  PRECONDITION(type.id() == ID_pointer);
103  static_cast<const reference_typet &>(type);
104  DATA_CHECK(
105  vm, !reference_type.get(ID_width).empty(), "reference must have width");
106  DATA_CHECK(
107  vm, reference_type.get_width() > 0, "reference must have non-zero width");
108  }
109 };
110 
114 template <>
115 inline bool can_cast_type<reference_typet>(const typet &type)
116 {
117  return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference);
118 }
119 
128 inline const reference_typet &to_reference_type(const typet &type)
129 {
131  return static_cast<const reference_typet &>(type);
132 }
133 
136 {
138  return static_cast<reference_typet &>(type);
139 }
140 
141 bool is_reference(const typet &type);
142 
143 bool is_rvalue_reference(const typet &type);
144 
147 {
148 public:
150  : binary_exprt(
151  exprt(ID_unknown),
152  ID_object_descriptor,
153  exprt(ID_unknown),
154  typet())
155  {
156  }
157 
158  explicit object_descriptor_exprt(exprt _object)
159  : binary_exprt(
160  std::move(_object),
161  ID_object_descriptor,
162  exprt(ID_unknown),
163  typet())
164  {
165  }
166 
171  void build(const exprt &expr, const namespacet &ns);
172 
174  {
175  return op0();
176  }
177 
178  const exprt &object() const
179  {
180  return op0();
181  }
182 
183  static const exprt &root_object(const exprt &expr);
184  const exprt &root_object() const
185  {
186  return root_object(object());
187  }
188 
190  {
191  return op1();
192  }
193 
194  const exprt &offset() const
195  {
196  return op1();
197  }
198 };
199 
200 template <>
202 {
203  return base.id() == ID_object_descriptor;
204 }
205 
206 inline void validate_expr(const object_descriptor_exprt &value)
207 {
208  validate_operands(value, 2, "Object descriptor must have two operands");
209 }
210 
217 inline const object_descriptor_exprt &
219 {
220  PRECONDITION(expr.id() == ID_object_descriptor);
221  const object_descriptor_exprt &ret =
222  static_cast<const object_descriptor_exprt &>(expr);
223  validate_expr(ret);
224  return ret;
225 }
226 
229 {
230  PRECONDITION(expr.id() == ID_object_descriptor);
231  object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
232  validate_expr(ret);
233  return ret;
234 }
235 
238 {
239 public:
241  : binary_exprt(
242  exprt(ID_unknown),
243  ID_dynamic_object,
244  exprt(ID_unknown),
245  std::move(type))
246  {
247  }
248 
249  void set_instance(unsigned int instance);
250 
251  unsigned int get_instance() const;
252 
254  {
255  return op1();
256  }
257 
258  const exprt &valid() const
259  {
260  return op1();
261  }
262 };
263 
264 template <>
266 {
267  return base.id() == ID_dynamic_object;
268 }
269 
270 inline void validate_expr(const dynamic_object_exprt &value)
271 {
272  validate_operands(value, 2, "Dynamic object must have two operands");
273 }
274 
282 {
283  PRECONDITION(expr.id() == ID_dynamic_object);
284  const dynamic_object_exprt &ret =
285  static_cast<const dynamic_object_exprt &>(expr);
286  validate_expr(ret);
287  return ret;
288 }
289 
292 {
293  PRECONDITION(expr.id() == ID_dynamic_object);
294  dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
295  validate_expr(ret);
296  return ret;
297 }
298 
301 {
302 public:
304  : unary_predicate_exprt(ID_is_dynamic_object, op)
305  {
306  }
307 };
308 
309 inline const is_dynamic_object_exprt &
311 {
312  PRECONDITION(expr.id() == ID_is_dynamic_object);
314  expr.operands().size() == 1, "is_dynamic_object must have one operand");
315  return static_cast<const is_dynamic_object_exprt &>(expr);
316 }
317 
321 {
322  PRECONDITION(expr.id() == ID_is_dynamic_object);
324  expr.operands().size() == 1, "is_dynamic_object must have one operand");
325  return static_cast<is_dynamic_object_exprt &>(expr);
326 }
327 
330 {
331 public:
332  explicit address_of_exprt(const exprt &op);
333 
335  : unary_exprt(ID_address_of, std::move(op), std::move(_type))
336  {
337  }
338 
340  {
341  return op0();
342  }
343 
344  const exprt &object() const
345  {
346  return op0();
347  }
348 };
349 
350 template <>
351 inline bool can_cast_expr<address_of_exprt>(const exprt &base)
352 {
353  return base.id() == ID_address_of;
354 }
355 
356 inline void validate_expr(const address_of_exprt &value)
357 {
358  validate_operands(value, 1, "Address of must have one operand");
359 }
360 
367 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
368 {
369  PRECONDITION(expr.id() == ID_address_of);
370  const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
371  validate_expr(ret);
372  return ret;
373 }
374 
377 {
378  PRECONDITION(expr.id() == ID_address_of);
379  address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
380  validate_expr(ret);
381  return ret;
382 }
383 
386 {
387 public:
388  explicit dereference_exprt(const exprt &op)
389  : unary_exprt(ID_dereference, op, op.type().subtype())
390  {
391  PRECONDITION(op.type().id() == ID_pointer);
392  }
393 
395  : unary_exprt(ID_dereference, std::move(op), std::move(type))
396  {
397  }
398 
400  {
401  return op0();
402  }
403 
404  const exprt &pointer() const
405  {
406  return op0();
407  }
408 
409  static void check(
410  const exprt &expr,
412  {
413  DATA_CHECK(
414  vm,
415  expr.operands().size() == 1,
416  "dereference expression must have one operand");
417  }
418 
419  static void validate(
420  const exprt &expr,
421  const namespacet &ns,
423 };
424 
425 template <>
426 inline bool can_cast_expr<dereference_exprt>(const exprt &base)
427 {
428  return base.id() == ID_dereference;
429 }
430 
431 inline void validate_expr(const dereference_exprt &value)
432 {
433  validate_operands(value, 1, "Dereference must have one operand");
434 }
435 
442 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
443 {
444  PRECONDITION(expr.id() == ID_dereference);
445  const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
446  validate_expr(ret);
447  return ret;
448 }
449 
452 {
453  PRECONDITION(expr.id() == ID_dereference);
454  dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
455  validate_expr(ret);
456  return ret;
457 }
458 
461 {
462 public:
464  : constant_exprt(ID_NULL, std::move(type))
465  {
466  }
467 };
468 
472 {
473 public:
475  : binary_predicate_exprt(std::move(pointer), id, std::move(size))
476  {
477  }
478 
479  const exprt &pointer() const
480  {
481  return op0();
482  }
483 
484  const exprt &size() const
485  {
486  return op1();
487  }
488 };
489 
490 inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)
491 {
492  PRECONDITION(expr.id() == ID_r_ok || expr.id() == ID_w_ok);
493  auto &ret = static_cast<const r_or_w_ok_exprt &>(expr);
494  validate_expr(ret);
495  return ret;
496 }
497 
500 {
501 public:
503  : r_or_w_ok_exprt(ID_r_ok, std::move(pointer), std::move(size))
504  {
505  }
506 };
507 
508 inline const r_ok_exprt &to_r_ok_expr(const exprt &expr)
509 {
510  PRECONDITION(expr.id() == ID_r_ok);
511  const r_ok_exprt &ret = static_cast<const r_ok_exprt &>(expr);
512  validate_expr(ret);
513  return ret;
514 }
515 
518 {
519 public:
521  : r_or_w_ok_exprt(ID_w_ok, std::move(pointer), std::move(size))
522  {
523  }
524 };
525 
526 inline const w_ok_exprt &to_w_ok_expr(const exprt &expr)
527 {
528  PRECONDITION(expr.id() == ID_w_ok);
529  const w_ok_exprt &ret = static_cast<const w_ok_exprt &>(expr);
530  validate_expr(ret);
531  return ret;
532 }
533 
534 #endif // CPROVER_UTIL_POINTER_EXPR_H
dynamic_object_exprt::dynamic_object_exprt
dynamic_object_exprt(typet type)
Definition: pointer_expr.h:240
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_r_or_w_ok_expr
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:490
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
typet::subtype
const typet & subtype() const
Definition: type.h:47
can_cast_expr< dynamic_object_exprt >
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: pointer_expr.h:265
can_cast_expr< address_of_exprt >
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: pointer_expr.h:351
object_descriptor_exprt::build
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
Definition: pointer_expr.cpp:108
w_ok_exprt::w_ok_exprt
w_ok_exprt(exprt pointer, exprt size)
Definition: pointer_expr.h:520
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:339
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:442
reference_typet
The reference type.
Definition: pointer_expr.h:89
typet
The type of an expression, extends irept.
Definition: type.h:28
reference_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:97
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:386
dynamic_object_exprt
Representation of heap-allocated objects.
Definition: pointer_expr.h:238
is_dynamic_object_exprt
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:301
validate_operands
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:147
dereference_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the dereference expression has the right number of operands, refers to something with a po...
Definition: pointer_expr.cpp:149
can_cast_expr< object_descriptor_exprt >
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: pointer_expr.h:201
address_of_exprt::address_of_exprt
address_of_exprt(const exprt &op)
Definition: pointer_expr.cpp:120
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
dereference_exprt::dereference_exprt
dereference_exprt(const exprt &op)
Definition: pointer_expr.h:388
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:550
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: pointer_expr.h:184
is_rvalue_reference
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:140
can_cast_type< pointer_typet >
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:49
r_or_w_ok_exprt::pointer
const exprt & pointer() const
Definition: pointer_expr.h:479
to_object_descriptor_expr
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: pointer_expr.h:218
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
expr_protectedt::op0
exprt & op0()
Definition: expr.h:103
dynamic_object_exprt::get_instance
unsigned int get_instance() const
Definition: pointer_expr.cpp:24
address_of_exprt::address_of_exprt
address_of_exprt(exprt op, pointer_typet _type)
Definition: pointer_expr.h:334
dereference_exprt::pointer
const exprt & pointer() const
Definition: pointer_expr.h:404
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:461
validate_expr
void validate_expr(const object_descriptor_exprt &value)
Definition: pointer_expr.h:206
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
pointer_typet::pointer_typet
pointer_typet(typet _subtype, std::size_t width)
Definition: pointer_expr.h:26
dereference_exprt::dereference_exprt
dereference_exprt(exprt op, typet type)
Definition: pointer_expr.h:394
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:399
bitvector_types.h
Pre-defined bitvector types.
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: bitvector_types.h:208
can_cast_expr< dereference_exprt >
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: pointer_expr.h:426
null_pointer_exprt::null_pointer_exprt
null_pointer_exprt(pointer_typet type)
Definition: pointer_expr.h:463
dynamic_object_exprt::valid
const exprt & valid() const
Definition: pointer_expr.h:258
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
is_dynamic_object_exprt::is_dynamic_object_exprt
is_dynamic_object_exprt(const exprt &op)
Definition: pointer_expr.h:303
to_reference_type
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: pointer_expr.h:128
irept::swap
void swap(irept &irep)
Definition: irep.h:453
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::id
const irep_idt & id() const
Definition: irep.h:407
dstringt::empty
bool empty() const
Definition: dstring.h:88
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
object_descriptor_exprt::object
const exprt & object() const
Definition: pointer_expr.h:178
reference_typet::reference_typet
reference_typet(typet _subtype, std::size_t _width)
Definition: pointer_expr.h:91
to_dynamic_object_expr
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: pointer_expr.h:281
r_ok_exprt::r_ok_exprt
r_ok_exprt(exprt pointer, exprt size)
Definition: pointer_expr.h:502
object_descriptor_exprt::object_descriptor_exprt
object_descriptor_exprt(exprt _object)
Definition: pointer_expr.h:158
to_r_ok_expr
const r_ok_exprt & to_r_ok_expr(const exprt &expr)
Definition: pointer_expr.h:508
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
reference_type
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:248
dynamic_object_exprt::set_instance
void set_instance(unsigned int instance)
Definition: pointer_expr.cpp:19
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:133
dynamic_object_exprt::valid
exprt & valid()
Definition: pointer_expr.h:253
r_ok_exprt
A predicate that indicates that an address range is ok to read.
Definition: pointer_expr.h:500
object_descriptor_exprt::offset
const exprt & offset() const
Definition: pointer_expr.h:194
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:826
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
w_ok_exprt
A predicate that indicates that an address range is ok to write.
Definition: pointer_expr.h:518
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
r_or_w_ok_exprt
A base class for a predicate that indicates that an address range is ok to read or write.
Definition: pointer_expr.h:472
r_or_w_ok_exprt::r_or_w_ok_exprt
r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
Definition: pointer_expr.h:474
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:367
exprt::operands
operandst & operands()
Definition: expr.h:96
is_void_pointer
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
Definition: pointer_expr.h:79
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
object_descriptor_exprt::object_descriptor_exprt
object_descriptor_exprt()
Definition: pointer_expr.h:149
address_of_exprt::object
const exprt & object() const
Definition: pointer_expr.h:344
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
object_descriptor_exprt::object
exprt & object()
Definition: pointer_expr.h:173
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
to_is_dynamic_object_expr
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
Definition: pointer_expr.h:310
std_expr.h
API to expression classes.
to_w_ok_expr
const w_ok_exprt & to_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:526
unary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:495
pointer_typet::check
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:37
pointer_typet::difference_type
signedbv_typet difference_type() const
Definition: pointer_expr.h:32
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
can_cast_type< reference_typet >
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
Definition: pointer_expr.h:115
dereference_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:409
r_or_w_ok_exprt::size
const exprt & size() const
Definition: pointer_expr.h:484
object_descriptor_exprt::offset
exprt & offset()
Definition: pointer_expr.h:189