CBMC
simplify_expr_pointer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "simplify_expr_class.h"
10 
11 #include "arith_tools.h"
12 #include "c_types.h"
13 #include "config.h"
14 #include "expr_util.h"
15 #include "namespace.h"
16 #include "pointer_expr.h"
17 #include "pointer_offset_size.h"
18 #include "pointer_predicates.h"
19 #include "std_expr.h"
20 #include "string_constant.h"
21 
23  const exprt &expr,
24  mp_integer &address)
25 {
26  if(expr.id() == ID_dereference)
27  {
28  const auto &pointer = to_dereference_expr(expr).pointer();
29 
30  if(
31  pointer.id() == ID_typecast &&
32  to_typecast_expr(pointer).op().is_constant() &&
33  !to_integer(to_constant_expr(to_typecast_expr(pointer).op()), address))
34  {
35  return true;
36  }
37 
38  if(pointer.is_constant())
39  {
40  const constant_exprt &constant = to_constant_expr(pointer);
41 
42  if(is_null_pointer(constant))
43  {
44  address=0;
45  return true;
46  }
47  else if(!to_integer(constant, address))
48  return true;
49  }
50  }
51 
52  return false;
53 }
54 
57  const unary_exprt &expr)
58 {
59  const exprt &pointer = expr.op();
60  PRECONDITION(pointer.type().id() == ID_pointer);
61 
62  if(pointer.id() == ID_if)
63  {
64  if_exprt if_expr = lift_if(expr, 0);
65  return changed(simplify_if_preorder(if_expr));
66  }
67  else
68  {
69  auto r_it = simplify_rec(pointer); // recursive call
70  if(r_it.has_changed())
71  {
72  auto tmp = expr;
73  tmp.op() = r_it.expr;
74  return tmp;
75  }
76  }
77 
78  return unchanged(expr);
79 }
80 
83 {
84  if(expr.id()==ID_index)
85  {
86  auto new_index_expr = to_index_expr(expr);
87 
88  bool no_change = true;
89 
90  auto array_result = simplify_address_of_arg(new_index_expr.array());
91 
92  if(array_result.has_changed())
93  {
94  no_change = false;
95  new_index_expr.array() = array_result.expr;
96  }
97 
98  auto index_result = simplify_rec(new_index_expr.index());
99 
100  if(index_result.has_changed())
101  {
102  no_change = false;
103  new_index_expr.index() = index_result.expr;
104  }
105 
106  // rewrite (*(type *)int) [index] by
107  // pushing the index inside
108 
109  mp_integer address;
110  if(is_dereference_integer_object(new_index_expr.array(), address))
111  {
112  // push index into address
113  auto step_size = pointer_offset_size(new_index_expr.type(), ns);
114 
115  if(step_size.has_value())
116  {
117  const auto index = numeric_cast<mp_integer>(new_index_expr.index());
118 
119  if(index.has_value())
120  {
122  to_dereference_expr(new_index_expr.array()).pointer().type());
123  pointer_type.base_type() = new_index_expr.type();
124 
125  typecast_exprt typecast_expr(
126  from_integer((*step_size) * (*index) + address, c_index_type()),
127  pointer_type);
128 
129  return dereference_exprt{typecast_expr};
130  }
131  }
132  }
133 
134  if(!no_change)
135  return new_index_expr;
136  }
137  else if(expr.id()==ID_member)
138  {
139  auto new_member_expr = to_member_expr(expr);
140 
141  bool no_change = true;
142 
143  auto struct_op_result =
144  simplify_address_of_arg(new_member_expr.struct_op());
145 
146  if(struct_op_result.has_changed())
147  {
148  new_member_expr.struct_op() = struct_op_result.expr;
149  no_change = false;
150  }
151 
152  const typet &op_type = ns.follow(new_member_expr.struct_op().type());
153 
154  if(op_type.id() == ID_struct)
155  {
156  // rewrite NULL -> member by
157  // pushing the member inside
158 
159  mp_integer address;
160  if(is_dereference_integer_object(new_member_expr.struct_op(), address))
161  {
162  const irep_idt &member = to_member_expr(expr).get_component_name();
163  auto offset = member_offset(to_struct_type(op_type), member, ns);
164  if(offset.has_value())
165  {
167  to_dereference_expr(new_member_expr.struct_op()).pointer().type());
168  pointer_type.base_type() = new_member_expr.type();
169  typecast_exprt typecast_expr(
170  from_integer(address + *offset, c_index_type()), pointer_type);
171  return dereference_exprt{typecast_expr};
172  }
173  }
174  }
175 
176  if(!no_change)
177  return new_member_expr;
178  }
179  else if(expr.id()==ID_dereference)
180  {
181  auto new_expr = to_dereference_expr(expr);
182  auto r_pointer = simplify_rec(new_expr.pointer());
183  if(r_pointer.has_changed())
184  {
185  new_expr.pointer() = r_pointer.expr;
186  return std::move(new_expr);
187  }
188  }
189  else if(expr.id()==ID_if)
190  {
191  auto new_if_expr = to_if_expr(expr);
192 
193  bool no_change = true;
194 
195  auto r_cond = simplify_rec(new_if_expr.cond());
196  if(r_cond.has_changed())
197  {
198  new_if_expr.cond() = r_cond.expr;
199  no_change = false;
200  }
201 
202  auto true_result = simplify_address_of_arg(new_if_expr.true_case());
203  if(true_result.has_changed())
204  {
205  new_if_expr.true_case() = true_result.expr;
206  no_change = false;
207  }
208 
209  auto false_result = simplify_address_of_arg(new_if_expr.false_case());
210 
211  if(false_result.has_changed())
212  {
213  new_if_expr.false_case() = false_result.expr;
214  no_change = false;
215  }
216 
217  // condition is a constant?
218  if(new_if_expr.cond().is_true())
219  {
220  return new_if_expr.true_case();
221  }
222  else if(new_if_expr.cond().is_false())
223  {
224  return new_if_expr.false_case();
225  }
226 
227  if(!no_change)
228  return new_if_expr;
229  }
230 
231  return unchanged(expr);
232 }
233 
236 {
237  if(expr.type().id() != ID_pointer)
238  return unchanged(expr);
239 
240  auto new_object = simplify_address_of_arg(expr.object());
241 
242  if(new_object.expr.id() == ID_index)
243  {
244  auto index_expr = to_index_expr(new_object.expr);
245 
246  if(!index_expr.index().is_zero())
247  {
248  // we normalize &a[i] to (&a[0])+i
249  exprt offset = index_expr.op1();
250  index_expr.op1()=from_integer(0, offset.type());
251  auto new_address_of_expr = expr;
252  new_address_of_expr.object() = std::move(index_expr);
253  return plus_exprt(std::move(new_address_of_expr), offset);
254  }
255  }
256  else if(new_object.expr.id() == ID_dereference)
257  {
258  // simplify &*p to p
259  return to_dereference_expr(new_object.expr).pointer();
260  }
261 
262  if(new_object.has_changed())
263  {
264  auto new_expr = expr;
265  new_expr.object() = new_object;
266  return new_expr;
267  }
268  else
269  return unchanged(expr);
270 }
271 
274 {
275  const exprt &ptr = expr.pointer();
276 
277  if(ptr.type().id()!=ID_pointer)
278  return unchanged(expr);
279 
280  if(ptr.id()==ID_address_of)
281  {
282  auto offset = compute_pointer_offset(to_address_of_expr(ptr).object(), ns);
283 
284  if(offset.has_value())
285  return from_integer(*offset, expr.type());
286  }
287  else if(ptr.id()==ID_typecast) // pointer typecast
288  {
289  const auto &op = to_typecast_expr(ptr).op();
290  const typet &op_type = op.type();
291 
292  if(op_type.id()==ID_pointer)
293  {
294  // Cast from pointer to pointer.
295  // This just passes through, remove typecast.
296  auto new_expr = expr;
297  new_expr.op() = op;
298 
299  return changed(simplify_pointer_offset(new_expr)); // recursive call
300  }
301  else if(op_type.id()==ID_signedbv ||
302  op_type.id()==ID_unsignedbv)
303  {
304  // Cast from integer to pointer, say (int *)x.
305 
306  if(op.is_constant())
307  {
308  // (T *)0x1234 -> 0x1234
309  return changed(simplify_typecast(typecast_exprt{op, expr.type()}));
310  }
311  else
312  {
313  // We do a bit of special treatment for (TYPE *)(a+(int)&o),
314  // which is re-written to 'a'.
315 
316  typet type = expr.type();
317  exprt tmp = op;
318  if(tmp.id()==ID_plus && tmp.operands().size()==2)
319  {
320  const auto &plus_expr = to_plus_expr(tmp);
321 
322  if(
323  plus_expr.op0().id() == ID_typecast &&
324  to_typecast_expr(plus_expr.op0()).op().id() == ID_address_of)
325  {
326  auto new_expr =
327  typecast_exprt::conditional_cast(plus_expr.op1(), type);
328 
329  return changed(simplify_node(new_expr));
330  }
331  else if(
332  plus_expr.op1().id() == ID_typecast &&
333  to_typecast_expr(plus_expr.op1()).op().id() == ID_address_of)
334  {
335  auto new_expr =
336  typecast_exprt::conditional_cast(plus_expr.op0(), type);
337 
338  return changed(simplify_node(new_expr));
339  }
340  }
341  }
342  }
343  }
344  else if(ptr.id()==ID_plus) // pointer arithmetic
345  {
346  exprt::operandst ptr_expr;
347  exprt::operandst int_expr;
348 
349  for(const auto &op : ptr.operands())
350  {
351  if(op.type().id()==ID_pointer)
352  ptr_expr.push_back(op);
353  else if(!op.is_zero())
354  {
355  exprt tmp=op;
356  if(tmp.type()!=expr.type())
357  tmp = simplify_typecast(typecast_exprt(tmp, expr.type()));
358 
359  int_expr.push_back(tmp);
360  }
361  }
362 
363  if(ptr_expr.size()!=1 || int_expr.empty())
364  return unchanged(expr);
365 
366  typet pointer_base_type =
367  to_pointer_type(ptr_expr.front().type()).base_type();
368  if(pointer_base_type.id() == ID_empty)
369  pointer_base_type = char_type();
370 
371  auto element_size = pointer_offset_size(pointer_base_type, ns);
372 
373  if(!element_size.has_value())
374  return unchanged(expr);
375 
376  exprt pointer_offset_expr = simplify_pointer_offset(
377  pointer_offset_exprt(ptr_expr.front(), expr.type()));
378 
379  exprt sum;
380 
381  if(int_expr.size()==1)
382  sum=int_expr.front();
383  else
384  sum = simplify_plus(plus_exprt{int_expr, expr.type()});
385 
386  exprt size_expr = from_integer(*element_size, expr.type());
387 
388  exprt product = simplify_mult(mult_exprt{sum, size_expr});
389 
390  auto new_expr = plus_exprt(pointer_offset_expr, product);
391 
392  return changed(simplify_plus(new_expr));
393  }
394  else if(ptr.is_constant())
395  {
396  const constant_exprt &c_ptr = to_constant_expr(ptr);
397 
398  if(is_null_pointer(c_ptr))
399  {
400  return from_integer(0, expr.type());
401  }
402  else
403  {
404  // this is a pointer, we can't use to_integer
405  const auto width = to_pointer_type(ptr.type()).get_width();
406  mp_integer number = bvrep2integer(c_ptr.get_value(), width, false);
407  // a null pointer would have been caught above, return value 0
408  // will indicate that conversion failed
409  if(number==0)
410  return unchanged(expr);
411 
412  // The constant address consists of OBJECT-ID || OFFSET.
413  mp_integer offset_bits =
415  number%=power(2, offset_bits);
416 
417  return from_integer(number, expr.type());
418  }
419  }
420 
421  return unchanged(expr);
422 }
423 
425  const binary_relation_exprt &expr)
426 {
427  // the operands of the relation are both either one of
428  // a) an address_of_exprt
429  // b) a typecast_exprt with an address_of_exprt operand
430 
431  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
432 
433  // skip over the typecast
434  exprt tmp0 = skip_typecast(expr.op0());
435  PRECONDITION(tmp0.id() == ID_address_of);
436 
437  auto &tmp0_address_of = to_address_of_expr(tmp0);
438 
439  if(
440  tmp0_address_of.object().id() == ID_index &&
441  to_index_expr(tmp0_address_of.object()).index().is_zero())
442  {
443  tmp0_address_of =
444  address_of_exprt(to_index_expr(tmp0_address_of.object()).array());
445  }
446 
447  // skip over the typecast
448  exprt tmp1 = skip_typecast(expr.op1());
449  PRECONDITION(tmp1.id() == ID_address_of);
450 
451  auto &tmp1_address_of = to_address_of_expr(tmp1);
452 
453  if(
454  tmp1_address_of.object().id() == ID_index &&
455  to_index_expr(tmp1_address_of.object()).index().is_zero())
456  {
457  tmp1 = address_of_exprt(to_index_expr(tmp1_address_of.object()).array());
458  }
459 
460  const auto &tmp0_object = tmp0_address_of.object();
461  const auto &tmp1_object = tmp1_address_of.object();
462 
463  if(tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_symbol)
464  {
465  bool equal = to_symbol_expr(tmp0_object).get_identifier() ==
466  to_symbol_expr(tmp1_object).get_identifier();
467 
468  return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
469  }
470  else if(
471  tmp0_object.id() == ID_dynamic_object &&
472  tmp1_object.id() == ID_dynamic_object)
473  {
474  bool equal = to_dynamic_object_expr(tmp0_object).get_instance() ==
475  to_dynamic_object_expr(tmp1_object).get_instance();
476 
477  return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
478  }
479  else if(
480  (tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_dynamic_object) ||
481  (tmp0_object.id() == ID_dynamic_object && tmp1_object.id() == ID_symbol))
482  {
483  return make_boolean_expr(expr.id() != ID_equal);
484  }
485  else if(
486  tmp0_object.id() == ID_string_constant &&
487  tmp1_object.id() == ID_string_constant && tmp0_object == tmp1_object)
488  {
489  return make_boolean_expr(expr.id() == ID_equal);
490  }
491 
492  return unchanged(expr);
493 }
494 
496  const binary_relation_exprt &expr)
497 {
498  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
499  PRECONDITION(expr.is_boolean());
500 
501  exprt::operandst new_inequality_ops;
502  for(const auto &operand : expr.operands())
503  {
504  PRECONDITION(operand.id() == ID_pointer_object);
505  const exprt &op = to_pointer_object_expr(operand).pointer();
506 
507  if(op.id()==ID_address_of)
508  {
509  const auto &op_object = to_address_of_expr(op).object();
510 
511  if((op_object.id() != ID_symbol && op_object.id() != ID_dynamic_object &&
512  op_object.id() != ID_string_constant))
513  {
514  return unchanged(expr);
515  }
516  }
517  else if(!op.is_constant() || !op.is_zero())
518  {
519  return unchanged(expr);
520  }
521 
522  if(new_inequality_ops.empty())
523  new_inequality_ops.push_back(op);
524  else
525  {
526  new_inequality_ops.push_back(
528  op, new_inequality_ops.front().type())));
529  }
530  }
531 
532  auto new_expr = expr;
533 
534  new_expr.operands() = std::move(new_inequality_ops);
535 
536  return changed(simplify_inequality(new_expr));
537 }
538 
541 {
542  const exprt &op = expr.pointer();
543 
544  auto op_result = simplify_object(op);
545 
546  if(op_result.expr.id() == ID_if)
547  {
548  const if_exprt &if_expr = to_if_expr(op_result.expr);
549  exprt cond=if_expr.cond();
550 
551  auto p_o_false = expr;
552  p_o_false.op() = if_expr.false_case();
553 
554  auto p_o_true = expr;
555  p_o_true.op() = if_expr.true_case();
556 
557  auto new_expr = if_exprt(cond, p_o_true, p_o_false, expr.type());
558  return changed(simplify_rec(new_expr));
559  }
560 
561  if(op_result.has_changed())
562  {
563  auto new_expr = expr;
564  new_expr.op() = op_result;
565  return std::move(new_expr);
566  }
567  else
568  return unchanged(expr);
569 }
570 
573 {
574  auto new_expr = expr;
575  exprt &op = new_expr.op();
576 
577  bool no_change = true;
578 
579  auto op_result = simplify_object(op);
580 
581  if(op_result.has_changed())
582  {
583  op = op_result.expr;
584  no_change = false;
585  }
586 
587  // NULL is not dynamic
589  return false_exprt();
590 
591  // &something depends on the something
592  if(op.id() == ID_address_of)
593  {
594  const auto &op_object = to_address_of_expr(op).object();
595 
596  if(op_object.id() == ID_symbol)
597  {
598  const irep_idt identifier = to_symbol_expr(op_object).get_identifier();
599 
600  // this is for the benefit of symex
601  return make_boolean_expr(
602  identifier.starts_with(SYMEX_DYNAMIC_PREFIX "::"));
603  }
604  else if(op_object.id() == ID_string_constant)
605  {
606  return false_exprt();
607  }
608  else if(op_object.id() == ID_array)
609  {
610  return false_exprt();
611  }
612  }
613 
614  if(no_change)
615  return unchanged(expr);
616  else
617  return std::move(new_expr);
618 }
619 
622 {
623  auto new_expr = expr;
624  exprt &op = new_expr.op();
625  bool no_change = true;
626 
627  auto op_result = simplify_object(op);
628 
629  if(op_result.has_changed())
630  {
631  op = op_result.expr;
632  no_change = false;
633  }
634 
635  // NULL is not invalid
637  {
638  return false_exprt();
639  }
640 
641  // &anything is not invalid
642  if(op.id()==ID_address_of)
643  {
644  return false_exprt();
645  }
646 
647  if(no_change)
648  return unchanged(expr);
649  else
650  return std::move(new_expr);
651 }
652 
655 {
656  auto new_expr = expr;
657  bool no_change = true;
658  exprt &op = new_expr.pointer();
659  auto op_result = simplify_object(op);
660 
661  if(op_result.has_changed())
662  {
663  op = op_result.expr;
664  no_change = false;
665  }
666 
667  if(op.id() == ID_address_of)
668  {
669  const auto &op_object = to_address_of_expr(op).object();
670 
671  if(op_object.id() == ID_symbol)
672  {
673  // just get the type
674  auto size_opt = size_of_expr(op_object.type(), ns);
675 
676  if(size_opt.has_value())
677  {
678  const typet &expr_type = expr.type();
679  exprt size = size_opt.value();
680 
681  if(size.type() != expr_type)
682  size = simplify_typecast(typecast_exprt(size, expr_type));
683 
684  return size;
685  }
686  }
687  else if(op_object.id() == ID_string_constant)
688  {
689  typet type=expr.type();
690  return from_integer(
691  to_string_constant(op_object).value().size() + 1, type);
692  }
693  }
694 
695  if(no_change)
696  return unchanged(expr);
697  else
698  return std::move(new_expr);
699 }
700 
702  const prophecy_r_or_w_ok_exprt &expr)
703 {
704  exprt new_expr = simplify_rec(expr.lower(ns));
705  if(!new_expr.is_constant())
706  return unchanged(expr);
707  else
708  return std::move(new_expr);
709 }
710 
713 {
714  exprt new_expr = simplify_rec(expr.lower(ns));
715  if(!new_expr.is_constant())
716  return unchanged(expr);
717  else
718  return std::move(new_expr);
719 }
configt config
Definition: config.cpp:25
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
bitvector_typet char_type()
Definition: c_types.cpp:106
bitvector_typet c_index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: pointer_expr.h:540
exprt & object()
Definition: pointer_expr.h:549
exprt & op1()
Definition: expr.h:136
exprt & op0()
Definition: expr.h:133
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
std::size_t get_width() const
Definition: std_types.h:920
struct configt::bv_encodingt bv_encoding
A constant literal expression.
Definition: std_expr.h:2987
const irep_idt & get_value() const
Definition: std_expr.h:2995
Operator to dereference a pointer.
Definition: pointer_expr.h:834
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition: dstring.h:95
unsigned int get_instance() const
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
exprt & op1()
Definition: expr.h:136
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.h:224
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:47
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
operandst & operands()
Definition: expr.h:94
The Boolean constant false.
Definition: std_expr.h:3064
The trinary if-then-else operator.
Definition: std_expr.h:2370
exprt & true_case()
Definition: std_expr.h:2397
exprt & false_case()
Definition: std_expr.h:2407
exprt & cond()
Definition: std_expr.h:2387
exprt & array()
Definition: std_expr.h:1495
exprt & index()
Definition: std_expr.h:1505
const irep_idt & id() const
Definition: irep.h:384
irep_idt get_component_name() const
Definition: std_expr.h:2863
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1107
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
Expression for finding the size (in bytes) of the object a pointer points to.
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
A numerical identifier for the object a pointer points to.
The offset (in bytes) of a pointer relative to the object.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...
Definition: pointer_expr.h:453
exprt lower(const namespacet &ns) const
A base class for a predicate that indicates that an address range is ok to read or write or both.
exprt lower(const namespacet &ns) const
Lower an r_or_w_ok_exprt to arithmetic and logic expressions.
const namespacet & ns
resultt simplify_inequality_address_of(const binary_relation_exprt &)
resultt simplify_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &)
Try to simplify prophecy_{r,w,rw}_ok to a constant expression.
static resultt changed(resultt<> result)
resultt simplify_unary_pointer_predicate_preorder(const unary_exprt &)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_node(const exprt &)
resultt simplify_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &)
Try to simplify prophecy_pointer_in_range to a constant expression.
resultt simplify_rec(const exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_pointer_object(const pointer_object_exprt &)
resultt simplify_object(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_address_of_arg(const exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_pointer_offset(const pointer_offset_exprt &)
resultt simplify_plus(const plus_exprt &)
resultt simplify_if_preorder(const if_exprt &expr)
resultt simplify_is_dynamic_object(const unary_exprt &)
resultt simplify_object_size(const object_size_exprt &)
const irep_idt & get_identifier() const
Definition: std_expr.h:160
Semantic type conversion.
Definition: std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:361
const exprt & op() const
Definition: std_expr.h:391
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:338
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:219
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:203
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition: expr_util.cpp:369
Deprecated expression utility functions.
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: pointer_expr.h:315
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
std::optional< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Pointer Logic.
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
static bool is_dereference_integer_object(const exprt &expr, mp_integer &address)
BigInt mp_integer
Definition: smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3037
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2102
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:1041
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2933
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
const string_constantt & to_string_constant(const exprt &expr)
std::size_t object_bits
Definition: config.h:351