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 "std_expr.h"
16 
17 class namespacet;
18 
21 {
22 public:
24  : binary_exprt(
25  exprt(ID_unknown),
26  ID_object_descriptor,
27  exprt(ID_unknown),
28  typet())
29  {
30  }
31 
32  explicit object_descriptor_exprt(exprt _object)
33  : binary_exprt(
34  std::move(_object),
35  ID_object_descriptor,
36  exprt(ID_unknown),
37  typet())
38  {
39  }
40 
45  void build(const exprt &expr, const namespacet &ns);
46 
48  {
49  return op0();
50  }
51 
52  const exprt &object() const
53  {
54  return op0();
55  }
56 
57  const exprt &root_object() const;
58 
60  {
61  return op1();
62  }
63 
64  const exprt &offset() const
65  {
66  return op1();
67  }
68 };
69 
70 template <>
72 {
73  return base.id() == ID_object_descriptor;
74 }
75 
76 inline void validate_expr(const object_descriptor_exprt &value)
77 {
78  validate_operands(value, 2, "Object descriptor must have two operands");
79 }
80 
87 inline const object_descriptor_exprt &
89 {
90  PRECONDITION(expr.id() == ID_object_descriptor);
91  const object_descriptor_exprt &ret =
92  static_cast<const object_descriptor_exprt &>(expr);
93  validate_expr(ret);
94  return ret;
95 }
96 
99 {
100  PRECONDITION(expr.id() == ID_object_descriptor);
101  object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
102  validate_expr(ret);
103  return ret;
104 }
105 
108 {
109 public:
111  : binary_exprt(
112  exprt(ID_unknown),
113  ID_dynamic_object,
114  exprt(ID_unknown),
115  std::move(type))
116  {
117  }
118 
119  void set_instance(unsigned int instance);
120 
121  unsigned int get_instance() const;
122 
124  {
125  return op1();
126  }
127 
128  const exprt &valid() const
129  {
130  return op1();
131  }
132 };
133 
134 template <>
136 {
137  return base.id() == ID_dynamic_object;
138 }
139 
140 inline void validate_expr(const dynamic_object_exprt &value)
141 {
142  validate_operands(value, 2, "Dynamic object must have two operands");
143 }
144 
152 {
153  PRECONDITION(expr.id() == ID_dynamic_object);
154  const dynamic_object_exprt &ret =
155  static_cast<const dynamic_object_exprt &>(expr);
156  validate_expr(ret);
157  return ret;
158 }
159 
162 {
163  PRECONDITION(expr.id() == ID_dynamic_object);
164  dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
165  validate_expr(ret);
166  return ret;
167 }
168 
171 {
172 public:
174  : unary_predicate_exprt(ID_is_dynamic_object, op)
175  {
176  }
177 };
178 
179 inline const is_dynamic_object_exprt &
181 {
182  PRECONDITION(expr.id() == ID_is_dynamic_object);
184  expr.operands().size() == 1, "is_dynamic_object must have one operand");
185  return static_cast<const is_dynamic_object_exprt &>(expr);
186 }
187 
191 {
192  PRECONDITION(expr.id() == ID_is_dynamic_object);
194  expr.operands().size() == 1, "is_dynamic_object must have one operand");
195  return static_cast<is_dynamic_object_exprt &>(expr);
196 }
197 
200 {
201 public:
202  explicit address_of_exprt(const exprt &op);
203 
205  : unary_exprt(ID_address_of, std::move(op), std::move(_type))
206  {
207  }
208 
210  {
211  return op0();
212  }
213 
214  const exprt &object() const
215  {
216  return op0();
217  }
218 };
219 
220 template <>
221 inline bool can_cast_expr<address_of_exprt>(const exprt &base)
222 {
223  return base.id() == ID_address_of;
224 }
225 
226 inline void validate_expr(const address_of_exprt &value)
227 {
228  validate_operands(value, 1, "Address of must have one operand");
229 }
230 
237 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
238 {
239  PRECONDITION(expr.id() == ID_address_of);
240  const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
241  validate_expr(ret);
242  return ret;
243 }
244 
247 {
248  PRECONDITION(expr.id() == ID_address_of);
249  address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
250  validate_expr(ret);
251  return ret;
252 }
253 
256 {
257 public:
258  explicit dereference_exprt(const exprt &op)
259  : unary_exprt(ID_dereference, op, op.type().subtype())
260  {
261  PRECONDITION(op.type().id() == ID_pointer);
262  }
263 
265  : unary_exprt(ID_dereference, std::move(op), std::move(type))
266  {
267  }
268 
270  {
271  return op0();
272  }
273 
274  const exprt &pointer() const
275  {
276  return op0();
277  }
278 
279  static void check(
280  const exprt &expr,
282  {
283  DATA_CHECK(
284  vm,
285  expr.operands().size() == 1,
286  "dereference expression must have one operand");
287  }
288 
289  static void validate(
290  const exprt &expr,
291  const namespacet &ns,
293 };
294 
295 template <>
296 inline bool can_cast_expr<dereference_exprt>(const exprt &base)
297 {
298  return base.id() == ID_dereference;
299 }
300 
301 inline void validate_expr(const dereference_exprt &value)
302 {
303  validate_operands(value, 1, "Dereference must have one operand");
304 }
305 
312 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
313 {
314  PRECONDITION(expr.id() == ID_dereference);
315  const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
316  validate_expr(ret);
317  return ret;
318 }
319 
322 {
323  PRECONDITION(expr.id() == ID_dereference);
324  dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
325  validate_expr(ret);
326  return ret;
327 }
328 
329 #endif // CPROVER_UTIL_POINTER_EXPR_H
Operator to return the address of an object.
Definition: pointer_expr.h:200
address_of_exprt(const exprt &op)
const exprt & object() const
Definition: pointer_expr.h:214
address_of_exprt(exprt op, pointer_typet _type)
Definition: pointer_expr.h:204
exprt & object()
Definition: pointer_expr.h:209
A base class for binary expressions.
Definition: std_expr.h:551
exprt & op1()
Definition: expr.h:106
exprt & op0()
Definition: expr.h:103
Operator to dereference a pointer.
Definition: pointer_expr.h:256
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:279
dereference_exprt(const exprt &op)
Definition: pointer_expr.h:258
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...
const exprt & pointer() const
Definition: pointer_expr.h:274
dereference_exprt(exprt op, typet type)
Definition: pointer_expr.h:264
Representation of heap-allocated objects.
Definition: pointer_expr.h:108
unsigned int get_instance() const
const exprt & valid() const
Definition: pointer_expr.h:128
void set_instance(unsigned int instance)
dynamic_object_exprt(typet type)
Definition: pointer_expr.h:110
exprt & op0()
Definition: expr.h:103
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
const irep_idt & id() const
Definition: irep.h:407
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:171
is_dynamic_object_exprt(const exprt &op)
Definition: pointer_expr.h:173
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:21
const exprt & root_object() const
object_descriptor_exprt(exprt _object)
Definition: pointer_expr.h:32
const exprt & object() const
Definition: pointer_expr.h:52
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...
const exprt & offset() const
Definition: pointer_expr.h:64
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
The type of an expression, extends irept.
Definition: type.h:28
Generic base class for unary expressions.
Definition: std_expr.h:282
const exprt & op() const
Definition: std_expr.h:294
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:496
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
void validate_expr(const object_descriptor_exprt &value)
Definition: pointer_expr.h:76
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: pointer_expr.h:135
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: pointer_expr.h:296
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: pointer_expr.h:221
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: pointer_expr.h:88
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
Definition: pointer_expr.h:180
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: pointer_expr.h:71
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: pointer_expr.h:151
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
API to expression classes.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
validation_modet