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 <cassert>
12 
13 #include "arith_tools.h"
14 #include "c_types.h"
15 #include "config.h"
16 #include "expr_util.h"
17 #include "namespace.h"
18 #include "pointer_offset_size.h"
19 #include "pointer_predicates.h"
20 #include "prefix.h"
21 #include "std_expr.h"
22 #include "string_constant.h"
23 #include "threeval.h"
24 
26  const exprt &expr,
27  mp_integer &address)
28 {
29  if(expr.id() == ID_dereference)
30  {
31  const auto &pointer = to_dereference_expr(expr).pointer();
32 
33  if(
34  pointer.id() == ID_typecast &&
35  to_typecast_expr(pointer).op().is_constant() &&
36  !to_integer(to_constant_expr(to_typecast_expr(pointer).op()), address))
37  {
38  return true;
39  }
40 
41  if(pointer.is_constant())
42  {
43  const constant_exprt &constant = to_constant_expr(pointer);
44 
45  if(constant.get_value() == ID_NULL && config.ansi_c.NULL_is_zero) // NULL
46  {
47  address=0;
48  return true;
49  }
50  else if(!to_integer(constant, address))
51  return true;
52  }
53  }
54 
55  return false;
56 }
57 
60 {
61  if(expr.id()==ID_index)
62  {
63  auto new_index_expr = to_index_expr(expr);
64 
65  bool no_change = true;
66 
67  auto array_result = simplify_address_of_arg(new_index_expr.array());
68 
69  if(array_result.has_changed())
70  {
71  no_change = false;
72  new_index_expr.array() = array_result.expr;
73  }
74 
75  auto index_result = simplify_rec(new_index_expr.index());
76 
77  if(index_result.has_changed())
78  {
79  no_change = false;
80  new_index_expr.index() = index_result.expr;
81  }
82 
83  // rewrite (*(type *)int) [index] by
84  // pushing the index inside
85 
86  mp_integer address;
87  if(is_dereference_integer_object(new_index_expr.array(), address))
88  {
89  // push index into address
90  auto step_size = pointer_offset_size(new_index_expr.type(), ns);
91 
92  if(step_size.has_value())
93  {
94  const auto index = numeric_cast<mp_integer>(new_index_expr.index());
95 
96  if(index.has_value())
97  {
99  to_dereference_expr(new_index_expr.array()).pointer().type());
100  pointer_type.subtype() = new_index_expr.type();
101 
102  typecast_exprt typecast_expr(
103  from_integer((*step_size) * (*index) + address, index_type()),
104  pointer_type);
105 
106  return dereference_exprt{typecast_expr};
107  }
108  }
109  }
110 
111  if(!no_change)
112  return new_index_expr;
113  }
114  else if(expr.id()==ID_member)
115  {
116  auto new_member_expr = to_member_expr(expr);
117 
118  bool no_change = true;
119 
120  auto struct_op_result =
121  simplify_address_of_arg(new_member_expr.struct_op());
122 
123  if(struct_op_result.has_changed())
124  {
125  new_member_expr.struct_op() = struct_op_result.expr;
126  no_change = false;
127  }
128 
129  const typet &op_type = ns.follow(new_member_expr.struct_op().type());
130 
131  if(op_type.id() == ID_struct)
132  {
133  // rewrite NULL -> member by
134  // pushing the member inside
135 
136  mp_integer address;
137  if(is_dereference_integer_object(new_member_expr.struct_op(), address))
138  {
139  const irep_idt &member = to_member_expr(expr).get_component_name();
140  auto offset = member_offset(to_struct_type(op_type), member, ns);
141  if(offset.has_value())
142  {
144  to_dereference_expr(new_member_expr.struct_op()).pointer().type());
145  pointer_type.subtype() = new_member_expr.type();
146  typecast_exprt typecast_expr(
147  from_integer(address + *offset, index_type()), pointer_type);
148  return dereference_exprt{typecast_expr};
149  }
150  }
151  }
152 
153  if(!no_change)
154  return new_member_expr;
155  }
156  else if(expr.id()==ID_dereference)
157  {
158  auto new_expr = to_dereference_expr(expr);
159  auto r_pointer = simplify_rec(new_expr.pointer());
160  if(r_pointer.has_changed())
161  {
162  new_expr.pointer() = r_pointer.expr;
163  return std::move(new_expr);
164  }
165  }
166  else if(expr.id()==ID_if)
167  {
168  auto new_if_expr = to_if_expr(expr);
169 
170  bool no_change = true;
171 
172  auto r_cond = simplify_rec(new_if_expr.cond());
173  if(r_cond.has_changed())
174  {
175  new_if_expr.cond() = r_cond.expr;
176  no_change = false;
177  }
178 
179  auto true_result = simplify_address_of_arg(new_if_expr.true_case());
180  if(true_result.has_changed())
181  {
182  new_if_expr.true_case() = true_result.expr;
183  no_change = false;
184  }
185 
186  auto false_result = simplify_address_of_arg(new_if_expr.false_case());
187 
188  if(false_result.has_changed())
189  {
190  new_if_expr.false_case() = false_result.expr;
191  no_change = false;
192  }
193 
194  // condition is a constant?
195  if(new_if_expr.cond().is_true())
196  {
197  return new_if_expr.true_case();
198  }
199  else if(new_if_expr.cond().is_false())
200  {
201  return new_if_expr.false_case();
202  }
203 
204  if(!no_change)
205  return new_if_expr;
206  }
207 
208  return unchanged(expr);
209 }
210 
213 {
214  if(expr.type().id() != ID_pointer)
215  return unchanged(expr);
216 
217  auto new_object = simplify_address_of_arg(expr.object());
218 
219  if(new_object.expr.id() == ID_index)
220  {
221  auto index_expr = to_index_expr(new_object.expr);
222 
223  if(!index_expr.index().is_zero())
224  {
225  // we normalize &a[i] to (&a[0])+i
226  exprt offset = index_expr.op1();
227  index_expr.op1()=from_integer(0, offset.type());
228  auto new_address_of_expr = expr;
229  new_address_of_expr.object() = std::move(index_expr);
230  return plus_exprt(std::move(new_address_of_expr), offset);
231  }
232  }
233  else if(new_object.expr.id() == ID_dereference)
234  {
235  // simplify &*p to p
236  return to_dereference_expr(new_object.expr).pointer();
237  }
238 
239  if(new_object.has_changed())
240  {
241  auto new_expr = expr;
242  new_expr.object() = new_object;
243  return new_expr;
244  }
245  else
246  return unchanged(expr);
247 }
248 
251 {
252  const exprt &ptr = expr.op();
253 
254  if(ptr.id()==ID_if && ptr.operands().size()==3)
255  {
256  if_exprt if_expr=lift_if(expr, 0);
257  if_expr.true_case() =
259  if_expr.false_case() =
261  return changed(simplify_if(if_expr));
262  }
263 
264  if(ptr.type().id()!=ID_pointer)
265  return unchanged(expr);
266 
267  if(ptr.id()==ID_address_of)
268  {
269  auto offset = compute_pointer_offset(to_address_of_expr(ptr).object(), ns);
270 
271  if(offset.has_value())
272  return from_integer(*offset, expr.type());
273  }
274  else if(ptr.id()==ID_typecast) // pointer typecast
275  {
276  const auto &op = to_typecast_expr(ptr).op();
277  const typet &op_type = op.type();
278 
279  if(op_type.id()==ID_pointer)
280  {
281  // Cast from pointer to pointer.
282  // This just passes through, remove typecast.
283  auto new_expr = expr;
284  new_expr.op() = op;
285 
286  return changed(simplify_node(new_expr)); // recursive call
287  }
288  else if(op_type.id()==ID_signedbv ||
289  op_type.id()==ID_unsignedbv)
290  {
291  // Cast from integer to pointer, say (int *)x.
292 
293  if(op.is_constant())
294  {
295  // (T *)0x1234 -> 0x1234
296  exprt tmp = typecast_exprt(op, expr.type());
297  return changed(simplify_node(tmp));
298  }
299  else
300  {
301  // We do a bit of special treatment for (TYPE *)(a+(int)&o),
302  // which is re-written to 'a'.
303 
304  typet type = expr.type();
305  exprt tmp = op;
306  if(tmp.id()==ID_plus && tmp.operands().size()==2)
307  {
308  const auto &plus_expr = to_plus_expr(tmp);
309 
310  if(
311  plus_expr.op0().id() == ID_typecast &&
312  to_typecast_expr(plus_expr.op0()).op().id() == ID_address_of)
313  {
314  auto new_expr =
315  typecast_exprt::conditional_cast(plus_expr.op1(), type);
316 
317  return changed(simplify_node(new_expr));
318  }
319  else if(
320  plus_expr.op1().id() == ID_typecast &&
321  to_typecast_expr(plus_expr.op1()).op().id() == ID_address_of)
322  {
323  auto new_expr =
324  typecast_exprt::conditional_cast(plus_expr.op0(), type);
325 
326  return changed(simplify_node(new_expr));
327  }
328  }
329  }
330  }
331  }
332  else if(ptr.id()==ID_plus) // pointer arithmetic
333  {
334  exprt::operandst ptr_expr;
335  exprt::operandst int_expr;
336 
337  for(const auto &op : ptr.operands())
338  {
339  if(op.type().id()==ID_pointer)
340  ptr_expr.push_back(op);
341  else if(!op.is_zero())
342  {
343  exprt tmp=op;
344  if(tmp.type()!=expr.type())
345  tmp = simplify_node(typecast_exprt(tmp, expr.type()));
346 
347  int_expr.push_back(tmp);
348  }
349  }
350 
351  if(ptr_expr.size()!=1 || int_expr.empty())
352  return unchanged(expr);
353 
354  typet pointer_sub_type=ptr_expr.front().type().subtype();
355  if(pointer_sub_type.id()==ID_empty)
356  pointer_sub_type=char_type();
357 
358  auto element_size = pointer_offset_size(pointer_sub_type, ns);
359 
360  if(!element_size.has_value())
361  return unchanged(expr);
362 
363  // this might change the type of the pointer!
364  exprt pointer_offset_expr = simplify_node(pointer_offset(ptr_expr.front()));
365 
366  exprt sum;
367 
368  if(int_expr.size()==1)
369  sum=int_expr.front();
370  else
371  {
372  sum=exprt(ID_plus, expr.type());
373  sum.operands()=int_expr;
374  }
375 
376  sum = simplify_node(sum);
377 
378  exprt size_expr = from_integer(*element_size, expr.type());
379 
380  exprt product = mult_exprt(sum, size_expr);
381 
382  product = simplify_node(product);
383 
384  auto new_expr = plus_exprt(pointer_offset_expr, product);
385 
386  return changed(simplify_node(new_expr));
387  }
388  else if(ptr.id()==ID_constant)
389  {
390  const constant_exprt &c_ptr = to_constant_expr(ptr);
391 
392  if(c_ptr.get_value()==ID_NULL ||
393  c_ptr.value_is_zero_string())
394  {
395  auto new_expr = from_integer(0, expr.type());
396  return changed(simplify_node(new_expr));
397  }
398  else
399  {
400  // this is a pointer, we can't use to_integer
401  const auto width = to_pointer_type(ptr.type()).get_width();
402  mp_integer number = bvrep2integer(c_ptr.get_value(), width, false);
403  // a null pointer would have been caught above, return value 0
404  // will indicate that conversion failed
405  if(number==0)
406  return unchanged(expr);
407 
408  // The constant address consists of OBJECT-ID || OFFSET.
409  mp_integer offset_bits =
411  number%=power(2, offset_bits);
412 
413  auto new_expr = from_integer(number, expr.type());
414 
415  return changed(simplify_node(new_expr));
416  }
417  }
418 
419  return unchanged(expr);
420 }
421 
423  const binary_relation_exprt &expr)
424 {
425  // the operands of the relation are both either one of
426  // a) an address_of_exprt
427  // b) a typecast_exprt with an address_of_exprt operand
428 
429  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
430 
431  exprt tmp0=expr.op0();
432 
433  // skip over the typecast
434  if(tmp0.id()==ID_typecast)
435  tmp0 = to_typecast_expr(tmp0).op();
436 
437  PRECONDITION(tmp0.id() == ID_address_of);
438 
439  auto &tmp0_address_of = to_address_of_expr(tmp0);
440 
441  if(
442  tmp0_address_of.object().id() == ID_index &&
443  to_index_expr(tmp0_address_of.object()).index().is_zero())
444  {
445  tmp0_address_of =
446  address_of_exprt(to_index_expr(tmp0_address_of.object()).array());
447  }
448 
449  exprt tmp1=expr.op1();
450 
451  // skip over the typecast
452  if(tmp1.id()==ID_typecast)
453  tmp1 = to_typecast_expr(tmp1).op();
454 
455  PRECONDITION(tmp1.id() == ID_address_of);
456 
457  auto &tmp1_address_of = to_address_of_expr(tmp1);
458 
459  if(
460  tmp1_address_of.object().id() == ID_index &&
461  to_index_expr(tmp1_address_of.object()).index().is_zero())
462  {
463  tmp1 = address_of_exprt(to_index_expr(tmp1_address_of.object()).array());
464  }
465 
466  const auto &tmp0_object = tmp0_address_of.object();
467  const auto &tmp1_object = tmp1_address_of.object();
468 
469  if(tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_symbol)
470  {
471  bool equal = to_symbol_expr(tmp0_object).get_identifier() ==
472  to_symbol_expr(tmp1_object).get_identifier();
473 
474  return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
475  }
476  else if(
477  tmp0_object.id() == ID_dynamic_object &&
478  tmp1_object.id() == ID_dynamic_object)
479  {
480  bool equal = to_dynamic_object_expr(tmp0_object).get_instance() ==
481  to_dynamic_object_expr(tmp1_object).get_instance();
482 
483  return make_boolean_expr(expr.id() == ID_equal ? equal : !equal);
484  }
485  else if(
486  (tmp0_object.id() == ID_symbol && tmp1_object.id() == ID_dynamic_object) ||
487  (tmp0_object.id() == ID_dynamic_object && tmp1_object.id() == ID_symbol))
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.type().id() == ID_bool);
500 
501  exprt::operandst new_inequality_ops;
502  forall_operands(it, expr)
503  {
504  PRECONDITION(it->id() == ID_pointer_object);
505  const exprt &op = to_unary_expr(*it).op();
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.id() != ID_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.op();
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  if(op.id()==ID_if && op.operands().size()==3)
578  {
579  if_exprt if_expr=lift_if(expr, 0);
580  if_expr.true_case() =
582  if_expr.false_case() =
584  return changed(simplify_if(if_expr));
585  }
586 
587  bool no_change = true;
588 
589  auto op_result = simplify_object(op);
590 
591  if(op_result.has_changed())
592  {
593  op = op_result.expr;
594  no_change = false;
595  }
596 
597  // NULL is not dynamic
598  if(op.id() == ID_constant && op.get(ID_value) == ID_NULL)
599  return false_exprt();
600 
601  // &something depends on the something
602  if(op.id() == ID_address_of)
603  {
604  const auto &op_object = to_address_of_expr(op).object();
605 
606  if(op_object.id() == ID_symbol)
607  {
608  const irep_idt identifier = to_symbol_expr(op_object).get_identifier();
609 
610  // this is for the benefit of symex
611  return make_boolean_expr(
613  }
614  else if(op_object.id() == ID_string_constant)
615  {
616  return false_exprt();
617  }
618  else if(op_object.id() == ID_array)
619  {
620  return false_exprt();
621  }
622  }
623 
624  if(no_change)
625  return unchanged(expr);
626  else
627  return std::move(new_expr);
628 }
629 
632 {
633  auto new_expr = expr;
634  exprt &op = new_expr.op();
635  bool no_change = true;
636 
637  auto op_result = simplify_object(op);
638 
639  if(op_result.has_changed())
640  {
641  op = op_result.expr;
642  no_change = false;
643  }
644 
645  // NULL is not invalid
646  if(op.id()==ID_constant && op.get(ID_value)==ID_NULL)
647  {
648  return false_exprt();
649  }
650 
651  // &anything is not invalid
652  if(op.id()==ID_address_of)
653  {
654  return false_exprt();
655  }
656 
657  if(no_change)
658  return unchanged(expr);
659  else
660  return std::move(new_expr);
661 }
662 
664 {
665  if(a==b)
666  return tvt(true);
667 
668  if(a.id() == ID_address_of && b.id() == ID_address_of)
669  {
671  to_address_of_expr(a).object(), to_address_of_expr(b).object());
672  }
673 
674  if(a.id()==ID_constant && b.id()==ID_constant &&
675  a.get(ID_value)==ID_NULL && b.get(ID_value)==ID_NULL)
676  return tvt(true);
677 
678  if(a.id()==ID_constant && b.id()==ID_address_of &&
679  a.get(ID_value)==ID_NULL)
680  return tvt(false);
681 
682  if(b.id()==ID_constant && a.id()==ID_address_of &&
683  b.get(ID_value)==ID_NULL)
684  return tvt(false);
685 
686  return tvt::unknown();
687 }
688 
690 {
691  if(a==b)
692  return tvt(true);
693 
694  if(a.id()==ID_symbol && b.id()==ID_symbol)
695  {
696  if(to_symbol_expr(a).get_identifier() == to_symbol_expr(b).get_identifier())
697  return tvt(true);
698  }
699  else if(a.id()==ID_index && b.id()==ID_index)
700  {
702  to_index_expr(a).array(), to_index_expr(b).array());
703  }
704  else if(a.id()==ID_member && b.id()==ID_member)
705  {
707  to_member_expr(a).compound(), to_member_expr(b).compound());
708  }
709 
710  return tvt::unknown();
711 }
712 
715 {
716  auto new_expr = expr;
717  bool no_change = true;
718  exprt &op = new_expr.op();
719  auto op_result = simplify_object(op);
720 
721  if(op_result.has_changed())
722  {
723  op = op_result.expr;
724  no_change = false;
725  }
726 
727  if(op.id() == ID_address_of)
728  {
729  const auto &op_object = to_address_of_expr(op).object();
730 
731  if(op_object.id() == ID_symbol)
732  {
733  // just get the type
734  auto size_opt = size_of_expr(op_object.type(), ns);
735 
736  if(size_opt.has_value())
737  {
738  const typet &expr_type = expr.type();
739  exprt size = size_opt.value();
740 
741  if(size.type() != expr_type)
742  {
743  size = typecast_exprt(size, expr_type);
744  size = simplify_node(size);
745  }
746 
747  return size;
748  }
749  }
750  else if(op_object.id() == ID_string_constant)
751  {
752  typet type=expr.type();
753  return from_integer(
754  to_string_constant(op_object).get_value().size() + 1, type);
755  }
756  }
757 
758  if(no_change)
759  return unchanged(expr);
760  else
761  return std::move(new_expr);
762 }
763 
766 {
767  // we expand the definition
768  exprt def = good_pointer_def(expr.op(), ns);
769 
770  // recursive call
771  return changed(simplify_node(def));
772 }
simplify_exprt::simplify_rec
resultt simplify_rec(const exprt &)
Definition: simplify_expr.cpp:2603
simplify_exprt::simplify_is_invalid_pointer
resultt simplify_is_invalid_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:631
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:176
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:88
typet::subtype
const typet & subtype() const
Definition: type.h:47
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:212
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
good_pointer_def
exprt good_pointer_def(const exprt &pointer, const namespacet &ns)
Definition: pointer_predicates.cpp:83
typet
The type of an expression, extends irept.
Definition: type.h:29
threeval.h
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
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:422
simplify_exprt::simplify_is_dynamic_object
resultt simplify_is_dynamic_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:572
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:881
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:53
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:269
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:19
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:201
simplify_exprt::simplify_pointer_offset
resultt simplify_pointer_offset(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:250
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:130
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
simplify_exprt::simplify_node
resultt simplify_node(exprt)
Definition: simplify_expr.cpp:2371
is_dereference_integer_object
static bool is_dereference_integer_object(const exprt &expr, mp_integer &address)
Definition: simplify_expr_pointer.cpp:25
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:507
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
dynamic_object_exprt::get_instance
unsigned int get_instance() const
Definition: std_expr.cpp:46
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:135
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:2901
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:920
exprt::op1
exprt & op1()
Definition: expr.h:105
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
simplify_exprt::simplify_inequality
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1202
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
simplify_exprt::simplify_good_pointer
resultt simplify_good_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:765
irept::id
const irep_idt & id() const
Definition: irep.h:418
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
to_dynamic_object_expr
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: std_expr.h:1963
simplify_exprt::resultt
Definition: simplify_expr_class.h:97
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
simplify_exprt::simplify_pointer_object
resultt simplify_pointer_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:540
pointer_offset
exprt pointer_offset(const exprt &pointer)
Definition: pointer_predicates.cpp:37
tvt
Definition: threeval.h:20
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:1041
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
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:401
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
simplify_exprt::simplify_object
resultt simplify_object(const exprt &)
Definition: simplify_expr.cpp:1488
simplify_exprt::objects_equal
static tvt objects_equal(const exprt &a, const exprt &b)
Definition: simplify_expr_pointer.cpp:663
simplify_exprt::objects_equal_address_of
static tvt objects_equal_address_of(const exprt &a, const exprt &b)
Definition: simplify_expr_pointer.cpp:689
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:2991
simplify_exprt::simplify_inequality_pointer_object
resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
Definition: simplify_expr_pointer.cpp:495
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
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:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
config.h
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:246
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
make_boolean_expr
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:283
simplify_exprt::simplify_address_of_arg
resultt simplify_address_of_arg(const exprt &)
Definition: simplify_expr_pointer.cpp:59
exprt::operands
operandst & operands()
Definition: expr.h:95
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
simplify_exprt::simplify_object_size
resultt simplify_object_size(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:714
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
is_constant
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:30
std_expr.h
API to expression classes.
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
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:102
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939