cprover
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 "prefix.h"
20 #include "std_expr.h"
21 #include "string_constant.h"
22 
24  const exprt &expr,
25  mp_integer &address)
26 {
27  if(expr.id() == ID_dereference)
28  {
29  const auto &pointer = to_dereference_expr(expr).pointer();
30 
31  if(
32  pointer.id() == ID_typecast &&
33  to_typecast_expr(pointer).op().is_constant() &&
34  !to_integer(to_constant_expr(to_typecast_expr(pointer).op()), address))
35  {
36  return true;
37  }
38 
39  if(pointer.is_constant())
40  {
41  const constant_exprt &constant = to_constant_expr(pointer);
42 
43  if(constant.get_value() == ID_NULL && config.ansi_c.NULL_is_zero) // NULL
44  {
45  address=0;
46  return true;
47  }
48  else if(!to_integer(constant, address))
49  return true;
50  }
51  }
52 
53  return false;
54 }
55 
58 {
59  if(expr.id()==ID_index)
60  {
61  auto new_index_expr = to_index_expr(expr);
62 
63  bool no_change = true;
64 
65  auto array_result = simplify_address_of_arg(new_index_expr.array());
66 
67  if(array_result.has_changed())
68  {
69  no_change = false;
70  new_index_expr.array() = array_result.expr;
71  }
72 
73  auto index_result = simplify_rec(new_index_expr.index());
74 
75  if(index_result.has_changed())
76  {
77  no_change = false;
78  new_index_expr.index() = index_result.expr;
79  }
80 
81  // rewrite (*(type *)int) [index] by
82  // pushing the index inside
83 
84  mp_integer address;
85  if(is_dereference_integer_object(new_index_expr.array(), address))
86  {
87  // push index into address
88  auto step_size = pointer_offset_size(new_index_expr.type(), ns);
89 
90  if(step_size.has_value())
91  {
92  const auto index = numeric_cast<mp_integer>(new_index_expr.index());
93 
94  if(index.has_value())
95  {
97  to_dereference_expr(new_index_expr.array()).pointer().type());
98  pointer_type.subtype() = new_index_expr.type();
99 
100  typecast_exprt typecast_expr(
101  from_integer((*step_size) * (*index) + address, index_type()),
102  pointer_type);
103 
104  return dereference_exprt{typecast_expr};
105  }
106  }
107  }
108 
109  if(!no_change)
110  return new_index_expr;
111  }
112  else if(expr.id()==ID_member)
113  {
114  auto new_member_expr = to_member_expr(expr);
115 
116  bool no_change = true;
117 
118  auto struct_op_result =
119  simplify_address_of_arg(new_member_expr.struct_op());
120 
121  if(struct_op_result.has_changed())
122  {
123  new_member_expr.struct_op() = struct_op_result.expr;
124  no_change = false;
125  }
126 
127  const typet &op_type = ns.follow(new_member_expr.struct_op().type());
128 
129  if(op_type.id() == ID_struct)
130  {
131  // rewrite NULL -> member by
132  // pushing the member inside
133 
134  mp_integer address;
135  if(is_dereference_integer_object(new_member_expr.struct_op(), address))
136  {
137  const irep_idt &member = to_member_expr(expr).get_component_name();
138  auto offset = member_offset(to_struct_type(op_type), member, ns);
139  if(offset.has_value())
140  {
142  to_dereference_expr(new_member_expr.struct_op()).pointer().type());
143  pointer_type.subtype() = new_member_expr.type();
144  typecast_exprt typecast_expr(
145  from_integer(address + *offset, index_type()), pointer_type);
146  return dereference_exprt{typecast_expr};
147  }
148  }
149  }
150 
151  if(!no_change)
152  return new_member_expr;
153  }
154  else if(expr.id()==ID_dereference)
155  {
156  auto new_expr = to_dereference_expr(expr);
157  auto r_pointer = simplify_rec(new_expr.pointer());
158  if(r_pointer.has_changed())
159  {
160  new_expr.pointer() = r_pointer.expr;
161  return std::move(new_expr);
162  }
163  }
164  else if(expr.id()==ID_if)
165  {
166  auto new_if_expr = to_if_expr(expr);
167 
168  bool no_change = true;
169 
170  auto r_cond = simplify_rec(new_if_expr.cond());
171  if(r_cond.has_changed())
172  {
173  new_if_expr.cond() = r_cond.expr;
174  no_change = false;
175  }
176 
177  auto true_result = simplify_address_of_arg(new_if_expr.true_case());
178  if(true_result.has_changed())
179  {
180  new_if_expr.true_case() = true_result.expr;
181  no_change = false;
182  }
183 
184  auto false_result = simplify_address_of_arg(new_if_expr.false_case());
185 
186  if(false_result.has_changed())
187  {
188  new_if_expr.false_case() = false_result.expr;
189  no_change = false;
190  }
191 
192  // condition is a constant?
193  if(new_if_expr.cond().is_true())
194  {
195  return new_if_expr.true_case();
196  }
197  else if(new_if_expr.cond().is_false())
198  {
199  return new_if_expr.false_case();
200  }
201 
202  if(!no_change)
203  return new_if_expr;
204  }
205 
206  return unchanged(expr);
207 }
208 
211 {
212  if(expr.type().id() != ID_pointer)
213  return unchanged(expr);
214 
215  auto new_object = simplify_address_of_arg(expr.object());
216 
217  if(new_object.expr.id() == ID_index)
218  {
219  auto index_expr = to_index_expr(new_object.expr);
220 
221  if(!index_expr.index().is_zero())
222  {
223  // we normalize &a[i] to (&a[0])+i
224  exprt offset = index_expr.op1();
225  index_expr.op1()=from_integer(0, offset.type());
226  auto new_address_of_expr = expr;
227  new_address_of_expr.object() = std::move(index_expr);
228  return plus_exprt(std::move(new_address_of_expr), offset);
229  }
230  }
231  else if(new_object.expr.id() == ID_dereference)
232  {
233  // simplify &*p to p
234  return to_dereference_expr(new_object.expr).pointer();
235  }
236 
237  if(new_object.has_changed())
238  {
239  auto new_expr = expr;
240  new_expr.object() = new_object;
241  return new_expr;
242  }
243  else
244  return unchanged(expr);
245 }
246 
249 {
250  const exprt &ptr = expr.op();
251 
252  if(ptr.id()==ID_if && ptr.operands().size()==3)
253  {
254  if_exprt if_expr=lift_if(expr, 0);
255  if_expr.true_case() =
257  if_expr.false_case() =
259  return changed(simplify_if(if_expr));
260  }
261 
262  if(ptr.type().id()!=ID_pointer)
263  return unchanged(expr);
264 
265  if(ptr.id()==ID_address_of)
266  {
267  auto offset = compute_pointer_offset(to_address_of_expr(ptr).object(), ns);
268 
269  if(offset.has_value())
270  return from_integer(*offset, expr.type());
271  }
272  else if(ptr.id()==ID_typecast) // pointer typecast
273  {
274  const auto &op = to_typecast_expr(ptr).op();
275  const typet &op_type = op.type();
276 
277  if(op_type.id()==ID_pointer)
278  {
279  // Cast from pointer to pointer.
280  // This just passes through, remove typecast.
281  auto new_expr = expr;
282  new_expr.op() = op;
283 
284  return changed(simplify_node(new_expr)); // recursive call
285  }
286  else if(op_type.id()==ID_signedbv ||
287  op_type.id()==ID_unsignedbv)
288  {
289  // Cast from integer to pointer, say (int *)x.
290 
291  if(op.is_constant())
292  {
293  // (T *)0x1234 -> 0x1234
294  exprt tmp = typecast_exprt(op, expr.type());
295  return changed(simplify_node(tmp));
296  }
297  else
298  {
299  // We do a bit of special treatment for (TYPE *)(a+(int)&o),
300  // which is re-written to 'a'.
301 
302  typet type = expr.type();
303  exprt tmp = op;
304  if(tmp.id()==ID_plus && tmp.operands().size()==2)
305  {
306  const auto &plus_expr = to_plus_expr(tmp);
307 
308  if(
309  plus_expr.op0().id() == ID_typecast &&
310  to_typecast_expr(plus_expr.op0()).op().id() == ID_address_of)
311  {
312  auto new_expr =
313  typecast_exprt::conditional_cast(plus_expr.op1(), type);
314 
315  return changed(simplify_node(new_expr));
316  }
317  else if(
318  plus_expr.op1().id() == ID_typecast &&
319  to_typecast_expr(plus_expr.op1()).op().id() == ID_address_of)
320  {
321  auto new_expr =
322  typecast_exprt::conditional_cast(plus_expr.op0(), type);
323 
324  return changed(simplify_node(new_expr));
325  }
326  }
327  }
328  }
329  }
330  else if(ptr.id()==ID_plus) // pointer arithmetic
331  {
332  exprt::operandst ptr_expr;
333  exprt::operandst int_expr;
334 
335  for(const auto &op : ptr.operands())
336  {
337  if(op.type().id()==ID_pointer)
338  ptr_expr.push_back(op);
339  else if(!op.is_zero())
340  {
341  exprt tmp=op;
342  if(tmp.type()!=expr.type())
343  tmp = simplify_node(typecast_exprt(tmp, expr.type()));
344 
345  int_expr.push_back(tmp);
346  }
347  }
348 
349  if(ptr_expr.size()!=1 || int_expr.empty())
350  return unchanged(expr);
351 
352  typet pointer_sub_type=ptr_expr.front().type().subtype();
353  if(pointer_sub_type.id()==ID_empty)
354  pointer_sub_type=char_type();
355 
356  auto element_size = pointer_offset_size(pointer_sub_type, ns);
357 
358  if(!element_size.has_value())
359  return unchanged(expr);
360 
361  // this might change the type of the pointer!
362  exprt pointer_offset_expr = simplify_node(pointer_offset(ptr_expr.front()));
363 
364  exprt sum;
365 
366  if(int_expr.size()==1)
367  sum=int_expr.front();
368  else
369  {
370  sum=exprt(ID_plus, expr.type());
371  sum.operands()=int_expr;
372  }
373 
374  sum = simplify_node(sum);
375 
376  exprt size_expr = from_integer(*element_size, expr.type());
377 
378  exprt product = mult_exprt(sum, size_expr);
379 
380  product = simplify_node(product);
381 
382  auto new_expr = plus_exprt(pointer_offset_expr, product);
383 
384  return changed(simplify_node(new_expr));
385  }
386  else if(ptr.id()==ID_constant)
387  {
388  const constant_exprt &c_ptr = to_constant_expr(ptr);
389 
390  if(c_ptr.get_value()==ID_NULL ||
391  c_ptr.value_is_zero_string())
392  {
393  auto new_expr = from_integer(0, expr.type());
394  return changed(simplify_node(new_expr));
395  }
396  else
397  {
398  // this is a pointer, we can't use to_integer
399  const auto width = to_pointer_type(ptr.type()).get_width();
400  mp_integer number = bvrep2integer(c_ptr.get_value(), width, false);
401  // a null pointer would have been caught above, return value 0
402  // will indicate that conversion failed
403  if(number==0)
404  return unchanged(expr);
405 
406  // The constant address consists of OBJECT-ID || OFFSET.
407  mp_integer offset_bits =
409  number%=power(2, offset_bits);
410 
411  auto new_expr = from_integer(number, expr.type());
412 
413  return changed(simplify_node(new_expr));
414  }
415  }
416 
417  return unchanged(expr);
418 }
419 
421  const binary_relation_exprt &expr)
422 {
423  // the operands of the relation are both either one of
424  // a) an address_of_exprt
425  // b) a typecast_exprt with an address_of_exprt operand
426 
427  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
428 
429  // skip over the typecast
430  exprt tmp0 = skip_typecast(expr.op0());
431  PRECONDITION(tmp0.id() == ID_address_of);
432 
433  auto &tmp0_address_of = to_address_of_expr(tmp0);
434 
435  if(
436  tmp0_address_of.object().id() == ID_index &&
437  to_index_expr(tmp0_address_of.object()).index().is_zero())
438  {
439  tmp0_address_of =
440  address_of_exprt(to_index_expr(tmp0_address_of.object()).array());
441  }
442 
443  // skip over the typecast
444  exprt tmp1 = skip_typecast(expr.op1());
445  PRECONDITION(tmp1.id() == ID_address_of);
446 
447  auto &tmp1_address_of = to_address_of_expr(tmp1);
448 
449  if(
450  tmp1_address_of.object().id() == ID_index &&
451  to_index_expr(tmp1_address_of.object()).index().is_zero())
452  {
453  tmp1 = address_of_exprt(to_index_expr(tmp1_address_of.object()).array());
454  }
455 
456  const auto &tmp0_object = tmp0_address_of.object();
457  const auto &tmp1_object = tmp1_address_of.object();
458 
459  if(tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_symbol)
460  {
461  bool equal = to_symbol_expr(tmp0_object).get_identifier() ==
462  to_symbol_expr(tmp1_object).get_identifier();
463 
464  return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
465  }
466  else if(
467  tmp0_object.id() == ID_dynamic_object &&
468  tmp1_object.id() == ID_dynamic_object)
469  {
470  bool equal = to_dynamic_object_expr(tmp0_object).get_instance() ==
471  to_dynamic_object_expr(tmp1_object).get_instance();
472 
473  return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
474  }
475  else if(
476  (tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_dynamic_object) ||
477  (tmp0_object.id() == ID_dynamic_object && tmp1_object.id() == ID_symbol))
478  {
479  return make_boolean_expr(expr.id() != ID_equal);
480  }
481 
482  return unchanged(expr);
483 }
484 
486  const binary_relation_exprt &expr)
487 {
488  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
489  PRECONDITION(expr.type().id() == ID_bool);
490 
491  exprt::operandst new_inequality_ops;
492  forall_operands(it, expr)
493  {
494  PRECONDITION(it->id() == ID_pointer_object);
495  const exprt &op = to_unary_expr(*it).op();
496 
497  if(op.id()==ID_address_of)
498  {
499  const auto &op_object = to_address_of_expr(op).object();
500 
501  if((op_object.id() != ID_symbol && op_object.id() != ID_dynamic_object &&
502  op_object.id() != ID_string_constant))
503  {
504  return unchanged(expr);
505  }
506  }
507  else if(op.id() != ID_constant || !op.is_zero())
508  {
509  return unchanged(expr);
510  }
511 
512  if(new_inequality_ops.empty())
513  new_inequality_ops.push_back(op);
514  else
515  {
516  new_inequality_ops.push_back(
518  op, new_inequality_ops.front().type())));
519  }
520  }
521 
522  auto new_expr = expr;
523 
524  new_expr.operands() = std::move(new_inequality_ops);
525 
526  return changed(simplify_inequality(new_expr));
527 }
528 
531 {
532  const exprt &op = expr.op();
533 
534  auto op_result = simplify_object(op);
535 
536  if(op_result.expr.id() == ID_if)
537  {
538  const if_exprt &if_expr = to_if_expr(op_result.expr);
539  exprt cond=if_expr.cond();
540 
541  auto p_o_false = expr;
542  p_o_false.op() = if_expr.false_case();
543 
544  auto p_o_true = expr;
545  p_o_true.op() = if_expr.true_case();
546 
547  auto new_expr = if_exprt(cond, p_o_true, p_o_false, expr.type());
548  return changed(simplify_rec(new_expr));
549  }
550 
551  if(op_result.has_changed())
552  {
553  auto new_expr = expr;
554  new_expr.op() = op_result;
555  return std::move(new_expr);
556  }
557  else
558  return unchanged(expr);
559 }
560 
563 {
564  auto new_expr = expr;
565  exprt &op = new_expr.op();
566 
567  if(op.id()==ID_if && op.operands().size()==3)
568  {
569  if_exprt if_expr=lift_if(expr, 0);
570  if_expr.true_case() =
572  if_expr.false_case() =
574  return changed(simplify_if(if_expr));
575  }
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
588  if(op.id() == ID_constant && op.get(ID_value) == ID_NULL)
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(
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
636  if(op.id()==ID_constant && op.get(ID_value)==ID_NULL)
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.op();
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  {
683  size = typecast_exprt(size, expr_type);
684  size = simplify_node(size);
685  }
686 
687  return size;
688  }
689  }
690  else if(op_object.id() == ID_string_constant)
691  {
692  typet type=expr.type();
693  return from_integer(
694  to_string_constant(op_object).get_value().size() + 1, type);
695  }
696  }
697 
698  if(no_change)
699  return unchanged(expr);
700  else
701  return std::move(new_expr);
702 }
703 
706 {
707  // we expand the definition
708  exprt def = good_pointer_def(expr.op(), ns);
709 
710  // recursive call
711  return changed(simplify_node(def));
712 }
simplify_exprt::simplify_rec
resultt simplify_rec(const exprt &)
Definition: simplify_expr.cpp:2462
simplify_exprt::simplify_is_invalid_pointer
resultt simplify_is_invalid_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:621
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:256
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1788
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:168
typet::subtype
const typet & subtype() const
Definition: type.h:47
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:219
simplify_expr_class.h
configt::bv_encoding
struct configt::bv_encodingt bv_encoding
arith_tools.h
simplify_exprt::simplify_address_of
resultt simplify_address_of(const address_of_exprt &)
Definition: simplify_expr_pointer.cpp:210
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:339
good_pointer_def
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:84
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:442
typet
The type of an expression, extends irept.
Definition: type.h:28
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:386
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
pointer_predicates.h
Various predicates over pointers in programs.
simplify_exprt::simplify_inequality_address_of
resultt simplify_inequality_address_of(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:420
simplify_exprt::simplify_is_dynamic_object
resultt simplify_is_dynamic_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:562
prefix.h
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
to_integer
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
lift_if
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:203
simplify_exprt::simplify_pointer_offset
resultt simplify_pointer_offset(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:248
configt::ansi_c
struct configt::ansi_ct ansi_c
namespace.h
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
simplify_exprt::unchanged
static resultt unchanged(exprt expr)
Definition: simplify_expr_class.h:129
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2123
simplify_exprt::simplify_node
resultt simplify_node(exprt)
Definition: simplify_expr.cpp:2216
is_dereference_integer_object
static bool is_dereference_integer_object(const exprt &expr, mp_integer &address)
Definition: simplify_expr_pointer.cpp:23
simplify_exprt::simplify_if
resultt simplify_if(const if_exprt &)
Definition: simplify_expr_if.cpp:331
compute_pointer_offset
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:500
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
dynamic_object_exprt::get_instance
unsigned int get_instance() const
Definition: pointer_expr.cpp:24
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
SYMEX_DYNAMIC_PREFIX
#define SYMEX_DYNAMIC_PREFIX
Definition: pointer_predicates.h:17
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
simplify_exprt::changed
static resultt changed(resultt<> result)
Definition: simplify_expr_class.h:134
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:399
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:869
pointer_expr.h
API to expression classes for Pointers.
exprt::op1
exprt & op1()
Definition: expr.h:106
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:935
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
simplify_exprt::simplify_inequality
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1212
index_exprt::index
exprt & index()
Definition: std_expr.h:1268
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1258
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
simplify_exprt::simplify_good_pointer
resultt simplify_good_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:705
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
simplify_exprt::resultt
Definition: simplify_expr_class.h:96
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
simplify_exprt::simplify_pointer_object
resultt simplify_pointer_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:530
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:38
config
configt config
Definition: config.cpp:24
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:91
expr_util.h
Deprecated expression utility functions.
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:402
simplify_exprt::simplify_object
resultt simplify_object(const exprt &)
Definition: simplify_expr.cpp:1493
pointer_offset_size
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Definition: pointer_offset_size.cpp:89
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2113
simplify_exprt::simplify_inequality_pointer_object
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:485
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:23
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2103
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:195
config.h
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:278
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:244
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2541
make_boolean_expr
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:285
simplify_exprt::simplify_address_of_arg
resultt simplify_address_of_arg(const exprt &)
Definition: simplify_expr_pointer.cpp:57
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
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
simplify_exprt::simplify_object_size
resultt simplify_object_size(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:654
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
is_constant
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
std_expr.h
API to expression classes.
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2675
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:23
c_types.h
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700