cprover
simplify_expr.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.h"
10 
11 #include <algorithm>
12 
13 #include "arith_tools.h"
14 #include "base_type.h"
15 #include "byte_operators.h"
16 #include "c_types.h"
17 #include "config.h"
18 #include "endianness_map.h"
19 #include "expr_util.h"
20 #include "fixedbv.h"
21 #include "invariant.h"
22 #include "namespace.h"
23 #include "pointer_offset_size.h"
24 #include "rational.h"
25 #include "rational_tools.h"
26 #include "simplify_utils.h"
27 #include "std_expr.h"
28 #include "type_eq.h"
29 
30 // #define DEBUGX
31 
32 #ifdef DEBUGX
33 #include <iostream>
34 #endif
35 
36 #include "simplify_expr_class.h"
37 
38 // #define USE_CACHE
39 
40 #ifdef USE_CACHE
41 struct simplify_expr_cachet
42 {
43 public:
44  #if 1
45  typedef std::unordered_map<
46  exprt, exprt, irep_full_hash, irep_full_eq> containert;
47  #else
48  typedef std::unordered_map<exprt, exprt, irep_hash> containert;
49  #endif
50 
51  containert container_normal;
52 
53  containert &container()
54  {
55  return container_normal;
56  }
57 };
58 
59 simplify_expr_cachet simplify_expr_cache;
60 #endif
61 
63 {
64  if(expr.operands().size()!=1)
65  return true;
66 
67  if(expr.op0().is_constant())
68  {
69  const typet &type=ns.follow(expr.op0().type());
70 
71  if(type.id()==ID_floatbv)
72  {
73  ieee_floatt value(to_constant_expr(expr.op0()));
74  value.set_sign(false);
75  expr=value.to_expr();
76  return false;
77  }
78  else if(type.id()==ID_signedbv ||
79  type.id()==ID_unsignedbv)
80  {
81  auto value = numeric_cast<mp_integer>(expr.op0());
82  if(value.has_value())
83  {
84  if(*value >= 0)
85  {
86  expr=expr.op0();
87  return false;
88  }
89  else
90  {
91  value->negate();
92  expr = from_integer(*value, type);
93  return false;
94  }
95  }
96  }
97  }
98 
99  return true;
100 }
101 
103 {
104  if(expr.operands().size()!=1)
105  return true;
106 
107  if(expr.op0().is_constant())
108  {
109  const typet &type=ns.follow(expr.op0().type());
110 
111  if(type.id()==ID_floatbv)
112  {
113  ieee_floatt value(to_constant_expr(expr.op0()));
114  expr.make_bool(value.get_sign());
115  return false;
116  }
117  else if(type.id()==ID_signedbv ||
118  type.id()==ID_unsignedbv)
119  {
120  const auto value = numeric_cast<mp_integer>(expr.op0());
121  if(value.has_value())
122  {
123  expr.make_bool(*value >= 0);
124  return false;
125  }
126  }
127  }
128 
129  return true;
130 }
131 
133 {
134  const exprt &op = expr.op();
135 
136  if(op.is_constant())
137  {
138  const typet &op_type = op.type();
139 
140  if(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv)
141  {
142  const auto width = to_bitvector_type(op_type).get_width();
143  const auto &value = to_constant_expr(op).get_value();
144  std::size_t result = 0;
145 
146  for(std::size_t i = 0; i < width; i++)
147  if(get_bvrep_bit(value, width, i))
148  result++;
149 
150  auto result_expr = from_integer(result, expr.type());
151  expr.swap(result_expr);
152 
153  return false;
154  }
155  }
156 
157  return true;
158 }
159 
161 {
162  if(expr.operands().size()!=1)
163  return true;
164 
165  const typet &expr_type=ns.follow(expr.type());
166  const typet &op_type=ns.follow(expr.op0().type());
167 
168  // eliminate casts of infinity
169  if(expr.op0().id()==ID_infinity)
170  {
171  typet new_type=expr.type();
172  exprt tmp;
173  tmp.swap(expr.op0());
174  tmp.type()=new_type;
175  expr.swap(tmp);
176  return false;
177  }
178 
179  // casts from NULL to any integer
180  if(op_type.id()==ID_pointer &&
181  expr.op0().is_constant() &&
182  to_constant_expr(expr.op0()).get_value()==ID_NULL &&
183  (expr_type.id()==ID_unsignedbv || expr_type.id()==ID_signedbv) &&
185  {
186  exprt tmp=from_integer(0, expr_type);
187  expr.swap(tmp);
188  return false;
189  }
190 
191  // casts from pointer to integer
192  // where width of integer >= width of pointer
193  // (void*)(intX)expr -> (void*)expr
194  if(expr_type.id()==ID_pointer &&
195  expr.op0().id()==ID_typecast &&
196  expr.op0().operands().size()==1 &&
197  (op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv) &&
198  to_bitvector_type(op_type).get_width()>=
199  to_bitvector_type(expr_type).get_width())
200  {
201  exprt tmp=expr.op0().op0();
202  expr.op0().swap(tmp);
203  simplify_typecast(expr); // rec. call
204  return false;
205  }
206 
207  // eliminate redundant typecasts
208  if(type_eq(expr.type(), expr.op0().type(), ns))
209  {
210  exprt tmp;
211  tmp.swap(expr.op0());
212  expr.swap(tmp);
213  return false;
214  }
215 
216  // eliminate casts to proper bool
217  if(expr_type.id()==ID_bool)
218  {
219  // rewrite (bool)x to x!=0
220  binary_relation_exprt inequality;
221  inequality.id(op_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal);
222  inequality.add_source_location()=expr.source_location();
223  inequality.lhs()=expr.op0();
224  inequality.rhs()=from_integer(0, op_type);
225  CHECK_RETURN(inequality.rhs().is_not_nil());
226  simplify_node(inequality);
227  expr.swap(inequality);
228  return false;
229  }
230 
231  // circular casts through types shorter than `int`
232  if(op_type==signedbv_typet(32) &&
233  expr.op0().id()==ID_typecast)
234  {
235  if(expr_type==c_bool_typet(8) ||
236  expr_type==signedbv_typet(8) ||
237  expr_type==signedbv_typet(16) ||
238  expr_type==unsignedbv_typet(16))
239  {
240  // We checked that the id was ID_typecast in the enclosing `if`
241  const auto &typecast=expr_checked_cast<typecast_exprt>(expr.op0());
242  if(typecast.op().type()==expr_type)
243  {
244  expr=typecast.op0();
245  return false;
246  }
247  }
248  }
249 
250  // eliminate casts to _Bool
251  if(expr_type.id()==ID_c_bool &&
252  op_type.id()!=ID_bool)
253  {
254  // rewrite (_Bool)x to (_Bool)(x!=0)
255  exprt inequality = is_not_zero(expr.op0(), ns);
256  simplify_node(inequality);
257  expr.op0()=inequality;
258  simplify_typecast(expr); // recursive call
259  return false;
260  }
261 
262  // eliminate typecasts from NULL
263  if(expr_type.id()==ID_pointer &&
264  expr.op0().is_constant() &&
265  (to_constant_expr(expr.op0()).get_value()==ID_NULL ||
266  (expr.op0().is_zero() && config.ansi_c.NULL_is_zero)))
267  {
268  exprt tmp=expr.op0();
269  tmp.type()=expr.type();
270  to_constant_expr(tmp).set_value(ID_NULL);
271  expr.swap(tmp);
272  return false;
273  }
274 
275  // eliminate duplicate pointer typecasts
276  // (T1 *)(T2 *)x -> (T1 *)x
277  if(expr_type.id()==ID_pointer &&
278  expr.op0().id()==ID_typecast &&
279  op_type.id()==ID_pointer &&
280  expr.op0().operands().size()==1)
281  {
282  exprt tmp;
283  tmp.swap(expr.op0().op0());
284  expr.op0().swap(tmp);
285  // recursive call
286  simplify_node(expr);
287  return false;
288  }
289 
290  // casts from integer to pointer and back:
291  // (int)(void *)int -> (int)(size_t)int
292  if((expr_type.id()==ID_signedbv || expr_type.id()==ID_unsignedbv) &&
293  expr.op0().id()==ID_typecast &&
294  expr.op0().operands().size()==1 &&
295  op_type.id()==ID_pointer)
296  {
297  expr.op0().type()=size_type();
298  simplify_typecast(expr.op0()); // rec. call
299  simplify_typecast(expr); // rec. call
300  return false;
301  }
302 
303  // mildly more elaborate version of the above:
304  // (int)((T*)0 + int) -> (int)(sizeof(T)*(size_t)int) if NULL is zero
306  (expr_type.id()==ID_signedbv || expr_type.id()==ID_unsignedbv) &&
307  op_type.id()==ID_pointer &&
308  expr.op0().id()==ID_plus &&
309  expr.op0().operands().size()==2 &&
310  ((expr.op0().op0().id()==ID_typecast &&
311  expr.op0().op0().operands().size()==1 &&
312  expr.op0().op0().op0().is_zero()) ||
313  (expr.op0().op0().is_constant() &&
314  to_constant_expr(expr.op0().op0()).get_value()==ID_NULL)))
315  {
316  auto sub_size = pointer_offset_size(to_pointer_type(op_type).subtype(), ns);
317  if(sub_size.has_value())
318  {
319  // void*
320  if(*sub_size == 0 || *sub_size == 1)
321  expr.op0()=typecast_exprt(expr.op0().op1(), size_type());
322  else
323  expr.op0() = mult_exprt(
324  from_integer(*sub_size, size_type()),
325  typecast_exprt(expr.op0().op1(), size_type()));
326 
327  simplify_rec(expr.op0());
328  simplify_typecast(expr); // rec. call
329  return false;
330  }
331  }
332 
333  // Push a numerical typecast into various integer operations, i.e.,
334  // (T)(x OP y) ---> (T)x OP (T)y
335  //
336  // Doesn't work for many, e.g., pointer difference, floating-point,
337  // division, modulo.
338  // Many operations fail if the width of T
339  // is bigger than that of (x OP y). This includes ID_bitnot and
340  // anything that might overflow, e.g., ID_plus.
341  //
342  if((expr_type.id()==ID_signedbv || expr_type.id()==ID_unsignedbv) &&
343  (op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv))
344  {
345  bool enlarge=
346  to_bitvector_type(expr_type).get_width()>
347  to_bitvector_type(op_type).get_width();
348 
349  if(!enlarge)
350  {
351  irep_idt op_id=expr.op0().id();
352 
353  if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
354  op_id==ID_unary_minus ||
355  op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
356  {
357  exprt result=expr.op0();
358 
359  if(result.operands().size()>=1 &&
360  base_type_eq(result.op0().type(), result.type(), ns))
361  {
362  result.type()=expr.type();
363 
364  Forall_operands(it, result)
365  {
366  it->make_typecast(expr.type());
367  simplify_typecast(*it); // recursive call
368  }
369 
370  simplify_node(result); // possibly recursive call
371  expr.swap(result);
372  return false;
373  }
374  }
375  else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
376  {
377  }
378  }
379  }
380 
381  // Push a numerical typecast into pointer arithmetic
382  // (T)(ptr + int) ---> (T)((size_t)ptr + sizeof(subtype)*(size_t)int)
383  //
384  if((expr_type.id()==ID_signedbv || expr_type.id()==ID_unsignedbv) &&
385  op_type.id()==ID_pointer &&
386  expr.op0().id()==ID_plus)
387  {
388  const auto step = pointer_offset_size(to_pointer_type(op_type).subtype(), ns);
389 
390  if(step.has_value() && *step != 0)
391  {
392  const typet size_t_type(size_type());
393  expr.op0().type()=size_t_type;
394 
395  for(auto &op : expr.op0().operands())
396  {
397  if(op.type().id()==ID_pointer)
398  {
399  op.make_typecast(size_t_type);
400  }
401  else
402  {
403  op.make_typecast(size_t_type);
404  if(*step > 1)
405  op = mult_exprt(from_integer(*step, size_t_type), op);
406  }
407  }
408 
409  simplify_rec(expr);
410  return false;
411  }
412  }
413 
414  #if 0
415  // (T)(a?b:c) --> a?(T)b:(T)c
416  if(expr.op0().id()==ID_if &&
417  expr.op0().operands().size()==3)
418  {
419  typecast_exprt tmp_op1(expr.op0().op1(), expr_type);
420  typecast_exprt tmp_op2(expr.op0().op2(), expr_type);
421  simplify_typecast(tmp_op1);
422  simplify_typecast(tmp_op2);
423  expr=if_exprt(expr.op0().op0(), tmp_op1, tmp_op2, expr_type);
424  simplify_if(to_if_expr(expr));
425  return false;
426  }
427  #endif
428 
429  const irep_idt &expr_type_id=expr_type.id();
430  const exprt &operand=expr.op0();
431  const irep_idt &op_type_id=op_type.id();
432 
433  if(operand.is_constant())
434  {
435  const irep_idt &value=to_constant_expr(operand).get_value();
436 
437  // preserve the sizeof type annotation
438  typet c_sizeof_type=
439  static_cast<const typet &>(operand.find(ID_C_c_sizeof_type));
440 
441  if(op_type_id==ID_integer ||
442  op_type_id==ID_natural)
443  {
444  // from integer to ...
445 
446  mp_integer int_value=string2integer(id2string(value));
447 
448  if(expr_type_id==ID_bool)
449  {
450  expr.make_bool(int_value!=0);
451  return false;
452  }
453 
454  if(expr_type_id==ID_unsignedbv ||
455  expr_type_id==ID_signedbv ||
456  expr_type_id==ID_c_enum ||
457  expr_type_id==ID_c_bit_field ||
458  expr_type_id==ID_integer)
459  {
460  expr=from_integer(int_value, expr_type);
461  return false;
462  }
463  }
464  else if(op_type_id==ID_rational)
465  {
466  }
467  else if(op_type_id==ID_real)
468  {
469  }
470  else if(op_type_id==ID_bool)
471  {
472  if(expr_type_id==ID_unsignedbv ||
473  expr_type_id==ID_signedbv ||
474  expr_type_id==ID_integer ||
475  expr_type_id==ID_natural ||
476  expr_type_id==ID_rational ||
477  expr_type_id==ID_c_bool ||
478  expr_type_id==ID_c_enum ||
479  expr_type_id==ID_c_bit_field)
480  {
481  if(operand.is_true())
482  {
483  expr=from_integer(1, expr_type);
484  CHECK_RETURN(expr.is_not_nil());
485  return false;
486  }
487  else if(operand.is_false())
488  {
489  expr=from_integer(0, expr_type);
490  CHECK_RETURN(expr.is_not_nil());
491  return false;
492  }
493  }
494  else if(expr_type_id==ID_c_enum_tag)
495  {
496  const typet &c_enum_type=ns.follow_tag(to_c_enum_tag_type(expr_type));
497  if(c_enum_type.id()==ID_c_enum) // possibly incomplete
498  {
499  unsigned int_value = operand.is_true() ? 1u : 0u;
500  exprt tmp=from_integer(int_value, c_enum_type);
501  tmp.type()=expr_type; // we maintain the tag type
502  expr=tmp;
503  return false;
504  }
505  }
506  else if(expr_type_id==ID_pointer &&
507  operand.is_false() &&
509  {
510  expr=null_pointer_exprt(to_pointer_type(expr_type));
511  return false;
512  }
513  }
514  else if(op_type_id==ID_unsignedbv ||
515  op_type_id==ID_signedbv ||
516  op_type_id==ID_c_bit_field ||
517  op_type_id==ID_c_bool)
518  {
519  mp_integer int_value;
520 
521  if(to_integer(to_constant_expr(operand), int_value))
522  return true;
523 
524  if(expr_type_id==ID_bool)
525  {
526  expr.make_bool(int_value!=0);
527  return false;
528  }
529 
530  if(expr_type_id==ID_c_bool)
531  {
532  expr=from_integer(int_value!=0, expr_type);
533  return false;
534  }
535 
536  if(expr_type_id==ID_integer)
537  {
538  expr=from_integer(int_value, expr_type);
539  return false;
540  }
541 
542  if(expr_type_id==ID_natural)
543  {
544  if(int_value>=0)
545  {
546  expr=from_integer(int_value, expr_type);
547  return false;
548  }
549  }
550 
551  if(expr_type_id==ID_unsignedbv ||
552  expr_type_id==ID_signedbv ||
553  expr_type_id==ID_bv ||
554  expr_type_id==ID_c_bit_field)
555  {
556  expr=from_integer(int_value, expr_type);
557 
558  if(c_sizeof_type.is_not_nil())
559  expr.set(ID_C_c_sizeof_type, c_sizeof_type);
560 
561  return false;
562  }
563 
564  if(expr_type_id==ID_c_enum_tag)
565  {
566  const typet &c_enum_type=ns.follow_tag(to_c_enum_tag_type(expr_type));
567  if(c_enum_type.id()==ID_c_enum) // possibly incomplete
568  {
569  exprt tmp=from_integer(int_value, c_enum_type);
570  tmp.type()=expr_type; // we maintain the tag type
571  expr=tmp;
572  return false;
573  }
574  }
575 
576  if(expr_type_id==ID_c_enum)
577  {
578  expr=from_integer(int_value, expr_type);
579  return false;
580  }
581 
582  if(expr_type_id==ID_fixedbv)
583  {
584  // int to float
585  const fixedbv_typet &f_expr_type=
586  to_fixedbv_type(expr_type);
587 
588  fixedbvt f;
589  f.spec=fixedbv_spect(f_expr_type);
590  f.from_integer(int_value);
591  expr=f.to_expr();
592 
593  return false;
594  }
595 
596  if(expr_type_id==ID_floatbv)
597  {
598  // int to float
599  const floatbv_typet &f_expr_type=
600  to_floatbv_type(expr_type);
601 
602  ieee_floatt f(f_expr_type);
603  f.from_integer(int_value);
604  expr=f.to_expr();
605 
606  return false;
607  }
608 
609  if(expr_type_id==ID_rational)
610  {
611  rationalt r(int_value);
612  expr=from_rational(r);
613  return false;
614  }
615  }
616  else if(op_type_id==ID_fixedbv)
617  {
618  if(expr_type_id==ID_unsignedbv ||
619  expr_type_id==ID_signedbv)
620  {
621  // cast from fixedbv to int
622  fixedbvt f(to_constant_expr(expr.op0()));
623  expr=from_integer(f.to_integer(), expr_type);
624  return false;
625  }
626  else if(expr_type_id==ID_fixedbv)
627  {
628  // fixedbv to fixedbv
629  fixedbvt f(to_constant_expr(expr.op0()));
630  f.round(fixedbv_spect(to_fixedbv_type(expr_type)));
631  expr=f.to_expr();
632  return false;
633  }
634  }
635  else if(op_type_id==ID_floatbv)
636  {
637  ieee_floatt f(to_constant_expr(expr.op0()));
638 
639  if(expr_type_id==ID_unsignedbv ||
640  expr_type_id==ID_signedbv)
641  {
642  // cast from float to int
643  expr=from_integer(f.to_integer(), expr_type);
644  return false;
645  }
646  else if(expr_type_id==ID_floatbv)
647  {
648  // float to double or double to float
650  expr=f.to_expr();
651  return false;
652  }
653  else if(expr_type_id==ID_fixedbv)
654  {
655  fixedbvt fixedbv;
656  fixedbv.spec=fixedbv_spect(to_fixedbv_type(expr_type));
657  ieee_floatt factor(f.spec);
658  factor.from_integer(power(2, fixedbv.spec.get_fraction_bits()));
659  f*=factor;
660  fixedbv.set_value(f.to_integer());
661  expr=fixedbv.to_expr();
662  return false;
663  }
664  }
665  else if(op_type_id==ID_bv)
666  {
667  if(expr_type_id==ID_unsignedbv ||
668  expr_type_id==ID_signedbv ||
669  expr_type_id==ID_floatbv)
670  {
671  const auto width = to_bv_type(op_type).get_width();
672  const auto int_value = bvrep2integer(value, width, false);
673  expr=from_integer(int_value, expr_type);
674  return false;
675  }
676  }
677  else if(op_type_id==ID_c_enum_tag) // enum to int
678  {
679  const typet &base_type =
680  to_c_enum_type(ns.follow_tag(to_c_enum_tag_type(op_type))).subtype();
681  if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv)
682  {
683  // enum constants use the representation of their base type
684  expr.op0().type()=base_type;
685  simplify_typecast(expr);
686  return false;
687  }
688  }
689  else if(op_type_id==ID_c_enum) // enum to int
690  {
691  const typet &base_type=to_c_enum_type(op_type).subtype();
692  if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv)
693  {
694  // enum constants use the representation of their base type
695  expr.op0().type()=base_type;
696  simplify_typecast(expr);
697  return false;
698  }
699  }
700  }
701  else if(operand.id()==ID_typecast) // typecast of typecast
702  {
703  // (T1)(T2)x ---> (T1)
704  // where T1 has fewer bits than T2
705  if(operand.operands().size()==1 &&
706  op_type_id==expr_type_id &&
707  (expr_type_id==ID_unsignedbv || expr_type_id==ID_signedbv) &&
708  to_bitvector_type(expr_type).get_width()<=
709  to_bitvector_type(operand.type()).get_width())
710  {
711  exprt tmp;
712  tmp.swap(expr.op0().op0());
713  expr.op0().swap(tmp);
714  // might enable further simplification
715  simplify_typecast(expr); // recursive call
716  return false;
717  }
718  }
719  else if(operand.id()==ID_address_of)
720  {
721  const exprt &o=to_address_of_expr(operand).object();
722 
723  // turn &array into &array[0] when casting to pointer-to-element-type
724  if(o.type().id()==ID_array &&
725  base_type_eq(expr_type, pointer_type(o.type().subtype()), ns))
726  {
728 
729  simplify_rec(expr);
730  return false;
731  }
732  }
733 
734  return true;
735 }
736 
738 {
739  const exprt &pointer=to_dereference_expr(expr).pointer();
740 
741  if(pointer.type().id()!=ID_pointer)
742  return true;
743 
744  if(pointer.id()==ID_if && pointer.operands().size()==3)
745  {
746  const if_exprt &if_expr=to_if_expr(pointer);
747 
748  exprt tmp_op1=expr;
749  tmp_op1.op0()=if_expr.true_case();
750  simplify_dereference(tmp_op1);
751  exprt tmp_op2=expr;
752  tmp_op2.op0()=if_expr.false_case();
753  simplify_dereference(tmp_op2);
754 
755  expr=if_exprt(if_expr.cond(), tmp_op1, tmp_op2);
756 
757  simplify_if(to_if_expr(expr));
758 
759  return false;
760  }
761 
762  if(pointer.id()==ID_address_of)
763  {
764  exprt tmp=to_address_of_expr(pointer).object();
765  // one address_of is gone, try again
766  simplify_rec(tmp);
767  expr.swap(tmp);
768  return false;
769  }
770  // rewrite *(&a[0] + x) to a[x]
771  else if(pointer.id()==ID_plus &&
772  pointer.operands().size()==2 &&
773  pointer.op0().id()==ID_address_of)
774  {
775  const address_of_exprt &address_of=
776  to_address_of_expr(pointer.op0());
777  if(address_of.object().id()==ID_index)
778  {
779  const index_exprt &old=to_index_expr(address_of.object());
780  if(ns.follow(old.array().type()).id()==ID_array)
781  {
782  index_exprt idx(old.array(),
783  plus_exprt(old.index(), pointer.op1()),
784  ns.follow(old.array().type()).subtype());
785  simplify_rec(idx);
786  expr.swap(idx);
787  return false;
788  }
789  }
790  }
791 
792  return true;
793 }
794 
796  exprt &expr,
797  const exprt &cond,
798  bool truth,
799  bool &new_truth)
800 {
801  if(expr==cond)
802  {
803  new_truth = truth;
804  return false;
805  }
806 
807  if(truth && cond.id()==ID_lt && expr.id()==ID_lt)
808  {
809  if(cond.op0()==expr.op0() &&
810  cond.op1().is_constant() &&
811  expr.op1().is_constant() &&
812  cond.op1().type()==expr.op1().type())
813  {
814  mp_integer i1, i2;
815 
816  if(
817  !to_integer(to_constant_expr(cond.op1()), i1) &&
818  !to_integer(to_constant_expr(expr.op1()), i2))
819  {
820  if(i1 >= i2)
821  {
822  new_truth = true;
823  return false;
824  }
825  }
826  }
827 
828  if(cond.op1()==expr.op1() &&
829  cond.op0().is_constant() &&
830  expr.op0().is_constant() &&
831  cond.op0().type()==expr.op0().type())
832  {
833  mp_integer i1, i2;
834 
835  if(
836  !to_integer(to_constant_expr(cond.op0()), i1) &&
837  !to_integer(to_constant_expr(expr.op0()), i2))
838  {
839  if(i1 <= i2)
840  {
841  new_truth = true;
842  return false;
843  }
844  }
845  }
846  }
847 
848  return true;
849 }
850 
852  exprt &expr,
853  const exprt &cond,
854  bool truth)
855 {
856  if(expr.type().id()==ID_bool)
857  {
858  bool new_truth;
859 
860  if(!simplify_if_implies(expr, cond, truth, new_truth))
861  {
862  if(new_truth)
863  {
864  expr=true_exprt();
865  return false;
866  }
867  else
868  {
869  expr=false_exprt();
870  return false;
871  }
872  }
873  }
874 
875  bool result = true;
876 
877  Forall_operands(it, expr)
878  result = simplify_if_recursive(*it, cond, truth) && result;
879 
880  return result;
881 }
882 
884  exprt &expr,
885  const exprt &cond)
886 {
887  forall_operands(it, cond)
888  {
889  if(expr==*it)
890  {
891  expr=true_exprt();
892  return false;
893  }
894  }
895 
896  bool result=true;
897 
898  Forall_operands(it, expr)
899  result=simplify_if_conj(*it, cond) && result;
900 
901  return result;
902 }
903 
905  exprt &expr,
906  const exprt &cond)
907 {
908  forall_operands(it, cond)
909  {
910  if(expr==*it)
911  {
912  expr=false_exprt();
913  return false;
914  }
915  }
916 
917  bool result=true;
918 
919  Forall_operands(it, expr)
920  result=simplify_if_disj(*it, cond) && result;
921 
922  return result;
923 }
924 
926  exprt &trueexpr,
927  exprt &falseexpr,
928  const exprt &cond)
929 {
930  bool tresult = true;
931  bool fresult = true;
932 
933  if(cond.id()==ID_and)
934  {
935  tresult = simplify_if_conj(trueexpr, cond) && tresult;
936  fresult = simplify_if_recursive(falseexpr, cond, false) && fresult;
937  }
938  else if(cond.id()==ID_or)
939  {
940  tresult = simplify_if_recursive(trueexpr, cond, true) && tresult;
941  fresult = simplify_if_disj(falseexpr, cond) && fresult;
942  }
943  else
944  {
945  tresult = simplify_if_recursive(trueexpr, cond, true) && tresult;
946  fresult = simplify_if_recursive(falseexpr, cond, false) && fresult;
947  }
948 
949  if(!tresult)
950  simplify_rec(trueexpr);
951  if(!fresult)
952  simplify_rec(falseexpr);
953 
954  return tresult && fresult;
955 }
956 
958 {
959  bool result=true;
960  bool tmp=false;
961 
962  while(!tmp)
963  {
964  tmp=true;
965 
966  if(expr.id()==ID_and)
967  {
968  if(expr.has_operands())
969  {
970  exprt::operandst &operands = expr.operands();
971  for(exprt::operandst::iterator it1=operands.begin();
972  it1!=operands.end(); it1++)
973  {
974  for(exprt::operandst::iterator it2=operands.begin();
975  it2!=operands.end(); it2++)
976  {
977  if(it1!=it2)
978  tmp=simplify_if_recursive(*it1, *it2, true) && tmp;
979  }
980  }
981  }
982  }
983 
984  if(!tmp)
985  simplify_rec(expr);
986 
987  result=tmp && result;
988  }
989 
990  return result;
991 }
992 
994 {
995  exprt &cond=expr.cond();
996  exprt &truevalue=expr.true_case();
997  exprt &falsevalue=expr.false_case();
998 
999  // we first want to look at the condition
1000  bool result=simplify_rec(cond);
1001 
1002  // 1 ? a : b -> a and 0 ? a : b -> b
1003  if(cond.is_constant())
1004  {
1005  exprt tmp=cond.is_true()?truevalue:falsevalue;
1006  simplify_rec(tmp);
1007  expr.swap(tmp);
1008  return false;
1009  }
1010 
1011  if(do_simplify_if)
1012  {
1013  if(cond.id()==ID_not)
1014  {
1015  exprt tmp;
1016  tmp.swap(cond.op0());
1017  cond.swap(tmp);
1018  truevalue.swap(falsevalue);
1019  result=false;
1020  }
1021 
1022 #ifdef USE_LOCAL_REPLACE_MAP
1023  replace_mapt map_before(local_replace_map);
1024 
1025  // a ? b : c --> a ? b[a/true] : c
1026  if(cond.id()==ID_and)
1027  {
1028  forall_operands(it, cond)
1029  {
1030  if(it->id()==ID_not)
1031  local_replace_map.insert(
1032  std::make_pair(it->op0(), false_exprt()));
1033  else
1034  local_replace_map.insert(
1035  std::make_pair(*it, true_exprt()));
1036  }
1037  }
1038  else
1039  local_replace_map.insert(std::make_pair(cond, true_exprt()));
1040 
1041  result=simplify_rec(truevalue) && result;
1042 
1043  local_replace_map=map_before;
1044 
1045  // a ? b : c --> a ? b : c[a/false]
1046  if(cond.id()==ID_or)
1047  {
1048  forall_operands(it, cond)
1049  {
1050  if(it->id()==ID_not)
1051  local_replace_map.insert(
1052  std::make_pair(it->op0(), true_exprt()));
1053  else
1054  local_replace_map.insert(
1055  std::make_pair(*it, false_exprt()));
1056  }
1057  }
1058  else
1059  local_replace_map.insert(std::make_pair(cond, false_exprt()));
1060 
1061  result=simplify_rec(falsevalue) && result;
1062 
1063  local_replace_map.swap(map_before);
1064 #else
1065  result=simplify_rec(truevalue) && result;
1066  result=simplify_rec(falsevalue) && result;
1067 #endif
1068  }
1069  else
1070  {
1071  result=simplify_rec(truevalue) && result;
1072  result=simplify_rec(falsevalue) && result;
1073  }
1074 
1075  return result;
1076 }
1077 
1079 {
1080  exprt &cond=expr.cond();
1081  exprt &truevalue=expr.true_case();
1082  exprt &falsevalue=expr.false_case();
1083 
1084  bool result=true;
1085 
1086  if(do_simplify_if)
1087  {
1088  #if 0
1089  result = simplify_if_cond(cond) && result;
1090  result = simplify_if_branch(truevalue, falsevalue, cond) && result;
1091  #endif
1092 
1093  if(expr.type()==bool_typet())
1094  {
1095  // a?b:c <-> (a && b) || (!a && c)
1096 
1097  if(truevalue.is_true() && falsevalue.is_false())
1098  {
1099  // a?1:0 <-> a
1100  exprt tmp;
1101  tmp.swap(cond);
1102  expr.swap(tmp);
1103  return false;
1104  }
1105  else if(truevalue.is_false() && falsevalue.is_true())
1106  {
1107  // a?0:1 <-> !a
1108  exprt tmp = boolean_negate(cond);
1109  simplify_node(tmp);
1110  expr.swap(tmp);
1111  return false;
1112  }
1113  else if(falsevalue.is_false())
1114  {
1115  // a?b:0 <-> a AND b
1116  and_exprt tmp(cond, truevalue);
1117  simplify_node(tmp);
1118  expr.swap(tmp);
1119  return false;
1120  }
1121  else if(falsevalue.is_true())
1122  {
1123  // a?b:1 <-> !a OR b
1124  or_exprt tmp(boolean_negate(cond), truevalue);
1125  simplify_node(tmp.op0());
1126  simplify_node(tmp);
1127  expr.swap(tmp);
1128  return false;
1129  }
1130  else if(truevalue.is_true())
1131  {
1132  // a?1:b <-> a||(!a && b) <-> a OR b
1133  or_exprt tmp(cond, falsevalue);
1134  simplify_node(tmp);
1135  expr.swap(tmp);
1136  return false;
1137  }
1138  else if(truevalue.is_false())
1139  {
1140  // a?0:b <-> !a && b
1141  and_exprt tmp(boolean_negate(cond), falsevalue);
1142  simplify_node(tmp.op0());
1143  simplify_node(tmp);
1144  expr.swap(tmp);
1145  return false;
1146  }
1147  }
1148  }
1149 
1150  if(truevalue==falsevalue)
1151  {
1152  exprt tmp;
1153  tmp.swap(truevalue);
1154  expr.swap(tmp);
1155  return false;
1156  }
1157 
1158  if(((truevalue.id()==ID_struct && falsevalue.id()==ID_struct) ||
1159  (truevalue.id()==ID_array && falsevalue.id()==ID_array)) &&
1160  truevalue.operands().size()==falsevalue.operands().size())
1161  {
1162  exprt cond_copy=cond;
1163  exprt falsevalue_copy=falsevalue;
1164  expr.swap(truevalue);
1165 
1166  exprt::operandst::const_iterator f_it=
1167  falsevalue_copy.operands().begin();
1168  Forall_operands(it, expr)
1169  {
1170  if_exprt if_expr(cond_copy, *it, *f_it);
1171  it->swap(if_expr);
1172  simplify_if(to_if_expr(*it));
1173  ++f_it;
1174  }
1175 
1176  return false;
1177  }
1178 
1179  return result;
1180 }
1181 
1183  const exprt &expr,
1184  value_listt &value_list)
1185 {
1186  if(expr.is_constant())
1187  {
1188  mp_integer int_value;
1189  if(to_integer(to_constant_expr(expr), int_value))
1190  return true;
1191 
1192  value_list.insert(int_value);
1193 
1194  return false;
1195  }
1196  else if(expr.id()==ID_if)
1197  {
1198  if(expr.operands().size()!=3)
1199  return true;
1200 
1201  return get_values(expr.op1(), value_list) ||
1202  get_values(expr.operands().back(), value_list);
1203  }
1204 
1205  return true;
1206 }
1207 
1209 {
1210  bool result=true;
1211 
1212  return result;
1213 }
1214 
1216 {
1217  bool result=true;
1218 
1219  if((expr.operands().size()%2)!=1)
1220  return true;
1221 
1222  const typet op0_type=ns.follow(expr.op0().type());
1223 
1224  // now look at first operand
1225 
1226  if(op0_type.id()==ID_struct)
1227  {
1228  if(expr.op0().id()==ID_struct ||
1229  expr.op0().id()==ID_constant)
1230  {
1231  while(expr.operands().size()>1)
1232  {
1233  const irep_idt &component_name=
1234  expr.op1().get(ID_component_name);
1235 
1236  if(!to_struct_type(op0_type).
1237  has_component(component_name))
1238  return result;
1239 
1240  std::size_t number=to_struct_type(op0_type).
1241  component_number(component_name);
1242 
1243  expr.op0().operands()[number].swap(expr.op2());
1244 
1245  expr.operands().erase(++expr.operands().begin());
1246  expr.operands().erase(++expr.operands().begin());
1247 
1248  result=false;
1249  }
1250  }
1251  }
1252  else if(expr.op0().type().id()==ID_array)
1253  {
1254  if(expr.op0().id()==ID_array ||
1255  expr.op0().id()==ID_constant)
1256  {
1257  while(expr.operands().size()>1)
1258  {
1259  const auto i = numeric_cast<mp_integer>(expr.op1());
1260 
1261  if(!i.has_value())
1262  break;
1263 
1264  if(*i < 0 || *i >= expr.op0().operands().size())
1265  break;
1266 
1267  expr.op0().operands()[numeric_cast_v<std::size_t>(*i)].swap(expr.op2());
1268 
1269  expr.operands().erase(++expr.operands().begin());
1270  expr.operands().erase(++expr.operands().begin());
1271 
1272  result=false;
1273  }
1274  }
1275  }
1276 
1277  if(expr.operands().size()==1)
1278  {
1279  exprt tmp;
1280  tmp.swap(expr.op0());
1281  expr.swap(tmp);
1282  result=false;
1283  }
1284 
1285  return result;
1286 }
1287 
1289 {
1290  if(expr.operands().size()!=3)
1291  return true;
1292 
1293  // this is to push updates into (possibly nested) constants
1294 
1295  const exprt::operandst &designator=to_update_expr(expr).designator();
1296 
1297  exprt updated_value=to_update_expr(expr).old();
1298  exprt *value_ptr=&updated_value;
1299 
1300  for(const auto &e : designator)
1301  {
1302  const typet &value_ptr_type=ns.follow(value_ptr->type());
1303 
1304  if(e.id()==ID_index_designator &&
1305  value_ptr->id()==ID_array)
1306  {
1307  const auto i = numeric_cast<mp_integer>(e.op0());
1308 
1309  if(!i.has_value())
1310  return true;
1311 
1312  if(*i < 0 || *i >= value_ptr->operands().size())
1313  return true;
1314 
1315  value_ptr = &value_ptr->operands()[numeric_cast_v<std::size_t>(*i)];
1316  }
1317  else if(e.id()==ID_member_designator &&
1318  value_ptr->id()==ID_struct)
1319  {
1320  const irep_idt &component_name=
1321  e.get(ID_component_name);
1322  const struct_typet &value_ptr_struct_type =
1323  to_struct_type(value_ptr_type);
1324  if(!value_ptr_struct_type.has_component(component_name))
1325  return true;
1326  auto &designator_as_struct_expr = to_struct_expr(*value_ptr);
1327  value_ptr = &designator_as_struct_expr.component(component_name, ns);
1328  CHECK_RETURN(value_ptr->is_not_nil());
1329  }
1330  else
1331  return true; // give up, unknown designator
1332  }
1333 
1334  // found, done
1335  *value_ptr=to_update_expr(expr).new_value();
1336  expr.swap(updated_value);
1337 
1338  return false;
1339 }
1340 
1342 {
1343  if(expr.id()==ID_plus)
1344  {
1345  if(expr.type().id()==ID_pointer)
1346  {
1347  // kill integers from sum
1348  Forall_operands(it, expr)
1349  if(ns.follow(it->type()).id()==ID_pointer)
1350  {
1351  exprt tmp=*it;
1352  expr.swap(tmp);
1353  simplify_object(expr);
1354  return false;
1355  }
1356  }
1357  }
1358  else if(expr.id()==ID_typecast)
1359  {
1360  auto const &typecast_expr = to_typecast_expr(expr);
1361  const typet &op_type = ns.follow(typecast_expr.op().type());
1362 
1363  if(op_type.id()==ID_pointer)
1364  {
1365  // cast from pointer to pointer
1366  expr = typecast_expr.op();
1367  simplify_object(expr);
1368  return false;
1369  }
1370  else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
1371  {
1372  // cast from integer to pointer
1373 
1374  // We do a bit of special treatment for (TYPE *)(a+(int)&o) and
1375  // (TYPE *)(a+(int)((T*)&o+x)), which are re-written to '&o'.
1376 
1377  const exprt &casted_expr = typecast_expr.op();
1378  if(casted_expr.id() == ID_plus && casted_expr.operands().size() == 2)
1379  {
1380  const exprt &cand = casted_expr.op0().id() == ID_typecast
1381  ? casted_expr.op0()
1382  : casted_expr.op1();
1383 
1384  if(cand.id()==ID_typecast &&
1385  cand.operands().size()==1 &&
1386  cand.op0().id()==ID_address_of)
1387  {
1388  expr=cand.op0();
1389  return false;
1390  }
1391  else if(cand.id()==ID_typecast &&
1392  cand.operands().size()==1 &&
1393  cand.op0().id()==ID_plus &&
1394  cand.op0().operands().size()==2 &&
1395  cand.op0().op0().id()==ID_typecast &&
1396  cand.op0().op0().operands().size()==1 &&
1397  cand.op0().op0().op0().id()==ID_address_of)
1398  {
1399  expr=cand.op0().op0().op0();
1400  return false;
1401  }
1402  }
1403  }
1404  }
1405  else if(expr.id()==ID_address_of)
1406  {
1407  if(expr.operands().size()==1)
1408  {
1409  if(expr.op0().id()==ID_index && expr.op0().operands().size()==2)
1410  {
1411  // &some[i] -> &some
1412  address_of_exprt new_expr(expr.op0().op0());
1413  expr.swap(new_expr);
1414  simplify_object(expr); // recursion
1415  return false;
1416  }
1417  else if(expr.op0().id()==ID_member && expr.op0().operands().size()==1)
1418  {
1419  // &some.f -> &some
1420  address_of_exprt new_expr(expr.op0().op0());
1421  expr.swap(new_expr);
1422  simplify_object(expr); // recursion
1423  return false;
1424  }
1425  }
1426  }
1427 
1428  return true;
1429 }
1430 
1432  const std::string &bits,
1433  const typet &_type,
1434  bool little_endian)
1435 {
1436  // bits start at lowest memory address
1437  const typet &type=ns.follow(_type);
1438 
1439  auto type_bits = pointer_offset_bits(type, ns);
1440 
1441  if(!type_bits.has_value() || *type_bits != bits.size())
1442  return nil_exprt();
1443 
1444  if(type.id()==ID_unsignedbv ||
1445  type.id()==ID_signedbv ||
1446  type.id()==ID_floatbv ||
1447  type.id()==ID_fixedbv)
1448  {
1449  endianness_mapt map(type, little_endian, ns);
1450 
1451  std::string tmp=bits;
1452  for(std::string::size_type i=0; i<bits.size(); ++i)
1453  tmp[i]=bits[map.map_bit(i)];
1454 
1455  std::reverse(tmp.begin(), tmp.end());
1456 
1457  mp_integer i = binary2integer(tmp, false);
1458  return constant_exprt(integer2bvrep(i, bits.size()), type);
1459  }
1460  else if(type.id()==ID_c_enum)
1461  {
1462  exprt val = bits2expr(bits, to_c_enum_type(type).subtype(), little_endian);
1463  val.type()=type;
1464  return val;
1465  }
1466  else if(type.id()==ID_c_enum_tag)
1467  return
1468  bits2expr(
1469  bits,
1471  little_endian);
1472  else if(type.id()==ID_union)
1473  {
1474  // find a suitable member
1475  const union_typet &union_type=to_union_type(type);
1476  const union_typet::componentst &components=
1477  union_type.components();
1478 
1479  for(const auto &component : components)
1480  {
1481  exprt val=bits2expr(bits, component.type(), little_endian);
1482  if(val.is_nil())
1483  continue;
1484 
1485  return union_exprt(component.get_name(), val, type);
1486  }
1487  }
1488  else if(type.id()==ID_struct)
1489  {
1490  const struct_typet &struct_type=to_struct_type(type);
1491  const struct_typet::componentst &components=
1492  struct_type.components();
1493 
1494  struct_exprt result(type);
1495  result.reserve_operands(components.size());
1496 
1497  mp_integer m_offset_bits=0;
1498  for(const auto &component : components)
1499  {
1500  const auto m_size = pointer_offset_bits(component.type(), ns);
1501  CHECK_RETURN(m_size.has_value() && *m_size>=0);
1502 
1503  std::string comp_bits = std::string(
1504  bits,
1505  numeric_cast_v<std::size_t>(m_offset_bits),
1506  numeric_cast_v<std::size_t>(*m_size));
1507 
1508  exprt comp=bits2expr(comp_bits, component.type(), little_endian);
1509  if(comp.is_nil())
1510  return nil_exprt();
1511  result.move_to_operands(comp);
1512 
1513  m_offset_bits += *m_size;
1514  }
1515 
1516  return std::move(result);
1517  }
1518  else if(type.id()==ID_array)
1519  {
1520  const array_typet &array_type=to_array_type(type);
1521 
1522  const std::size_t n_el = numeric_cast_v<std::size_t>(array_type.size());
1523 
1524  const auto el_size_opt = pointer_offset_bits(array_type.subtype(), ns);
1525  CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
1526 
1527  const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
1528 
1529  array_exprt result(array_type);
1530  result.reserve_operands(n_el);
1531 
1532  for(std::size_t i=0; i<n_el; ++i)
1533  {
1534  std::string el_bits=std::string(bits, i*el_size, el_size);
1535  exprt el = bits2expr(el_bits, array_type.subtype(), little_endian);
1536  if(el.is_nil())
1537  return nil_exprt();
1538  result.move_to_operands(el);
1539  }
1540 
1541  return std::move(result);
1542  }
1543 
1544  return nil_exprt();
1545 }
1546 
1548  const exprt &expr,
1549  bool little_endian)
1550 {
1551  // extract bits from lowest to highest memory address
1552  const typet &type=ns.follow(expr.type());
1553 
1554  if(expr.id()==ID_constant)
1555  {
1556  const auto &value = to_constant_expr(expr).get_value();
1557 
1558  if(type.id()==ID_unsignedbv ||
1559  type.id()==ID_signedbv ||
1560  type.id()==ID_floatbv ||
1561  type.id()==ID_fixedbv)
1562  {
1563  const auto width = to_bitvector_type(type).get_width();
1564 
1565  endianness_mapt map(type, little_endian, ns);
1566 
1567  std::string result(width, ' ');
1568 
1569  for(std::string::size_type i = 0; i < width; ++i)
1570  result[map.map_bit(i)] = get_bvrep_bit(value, width, i) ? '1' : '0';
1571 
1572  return result;
1573  }
1574  else if(type.id() == ID_c_enum_tag)
1575  {
1576  const typet &c_enum_type = ns.follow_tag(to_c_enum_tag_type(type));
1577  return expr2bits(constant_exprt(value, c_enum_type), little_endian);
1578  }
1579  else if(type.id() == ID_c_enum)
1580  {
1581  return expr2bits(
1582  constant_exprt(value, to_c_enum_type(type).subtype()), little_endian);
1583  }
1584  }
1585  else if(expr.id()==ID_union)
1586  {
1587  return expr2bits(to_union_expr(expr).op(), little_endian);
1588  }
1589  else if(expr.id()==ID_struct)
1590  {
1591  std::string result;
1592  forall_operands(it, expr)
1593  {
1594  auto tmp=expr2bits(*it, little_endian);
1595  if(!tmp.has_value())
1596  return {}; // failed
1597  result+=tmp.value();
1598  }
1599 
1600  return result;
1601  }
1602  else if(expr.id()==ID_array)
1603  {
1604  std::string result;
1605  forall_operands(it, expr)
1606  {
1607  auto tmp=expr2bits(*it, little_endian);
1608  if(!tmp.has_value())
1609  return {}; // failed
1610  result+=tmp.value();
1611  }
1612 
1613  return result;
1614  }
1615 
1616  return {};
1617 }
1618 
1620 {
1621  // lift up any ID_if on the object
1622  if(expr.op().id()==ID_if)
1623  {
1624  if_exprt if_expr=lift_if(expr, 0);
1627  simplify_if(if_expr);
1628  expr.swap(if_expr);
1629  return false;
1630  }
1631 
1632  const auto el_size = pointer_offset_bits(expr.type(), ns);
1633 
1634  // byte_extract(byte_extract(root, offset1), offset2) =>
1635  // byte_extract(root, offset1+offset2)
1636  if(expr.op().id()==expr.id())
1637  {
1638  expr.offset()=plus_exprt(
1639  to_byte_extract_expr(expr.op()).offset(),
1640  expr.offset());
1641  simplify_plus(expr.offset());
1642 
1643  expr.op()=to_byte_extract_expr(expr.op()).op();
1644  simplify_byte_extract(expr);
1645 
1646  return false;
1647  }
1648 
1649  // byte_extract(byte_update(root, offset, value), offset) =>
1650  // value
1651  if(((expr.id()==ID_byte_extract_big_endian &&
1652  expr.op().id()==ID_byte_update_big_endian) ||
1653  (expr.id()==ID_byte_extract_little_endian &&
1654  expr.op().id()==ID_byte_update_little_endian)) &&
1655  expr.offset()==expr.op().op1())
1656  {
1657  if(base_type_eq(expr.type(), expr.op().op2().type(), ns))
1658  {
1659  exprt tmp=expr.op().op2();
1660  expr.swap(tmp);
1661 
1662  return false;
1663  }
1664  else if(
1665  el_size.has_value() &&
1666  *el_size <= pointer_offset_bits(expr.op().op2().type(), ns))
1667  {
1668  expr.op()=expr.op().op2();
1669  expr.offset()=from_integer(0, expr.offset().type());
1670 
1671  simplify_byte_extract(expr);
1672 
1673  return false;
1674  }
1675  }
1676 
1677  // the following require a constant offset
1678  auto offset = numeric_cast<mp_integer>(expr.offset());
1679  if(!offset.has_value() || *offset < 0)
1680  return true;
1681 
1682  // don't do any of the following if endianness doesn't match, as
1683  // bytes need to be swapped
1684  if(*offset == 0 && byte_extract_id() == expr.id())
1685  {
1686  // byte extract of full object is object
1687  if(base_type_eq(expr.type(), expr.op().type(), ns))
1688  {
1689  exprt tmp = expr.op();
1690  expr.swap(tmp);
1691 
1692  return false;
1693  }
1694  else if(
1695  expr.type().id() == ID_pointer && expr.op().type().id() == ID_pointer)
1696  {
1697  typecast_exprt tc(expr.op(), expr.type());
1698  expr.swap(tc);
1699 
1700  return false;
1701  }
1702  }
1703 
1704  // no proper simplification for expr.type()==void
1705  // or types of unknown size
1706  if(!el_size.has_value() || *el_size == 0)
1707  return true;
1708 
1709  if(expr.op().id()==ID_array_of &&
1710  to_array_of_expr(expr.op()).op().id()==ID_constant)
1711  {
1712  const auto const_bits_opt=
1713  expr2bits(to_array_of_expr(expr.op()).op(),
1714  byte_extract_id()==ID_byte_extract_little_endian);
1715 
1716  if(!const_bits_opt.has_value())
1717  return true;
1718 
1719  std::string const_bits=const_bits_opt.value();
1720 
1721  DATA_INVARIANT(!const_bits.empty(), "bit representation must be non-empty");
1722 
1723  // double the string until we have sufficiently many bits
1724  while(mp_integer(const_bits.size()) < *offset * 8 + *el_size)
1725  const_bits+=const_bits;
1726 
1727  std::string el_bits = std::string(
1728  const_bits,
1729  numeric_cast_v<std::size_t>(*offset * 8),
1730  numeric_cast_v<std::size_t>(*el_size));
1731 
1732  exprt tmp=
1733  bits2expr(
1734  el_bits,
1735  expr.type(),
1736  expr.id()==ID_byte_extract_little_endian);
1737 
1738  if(tmp.is_not_nil())
1739  {
1740  expr.swap(tmp);
1741  return false;
1742  }
1743  }
1744 
1745  // in some cases we even handle non-const array_of
1746  if(
1747  expr.op().id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
1748  *el_size <= pointer_offset_bits(expr.op().op0().type(), ns))
1749  {
1750  expr.op()=index_exprt(expr.op(), expr.offset());
1751  expr.offset()=from_integer(0, expr.offset().type());
1752  simplify_rec(expr);
1753 
1754  return false;
1755  }
1756 
1757  // extract bits of a constant
1758  const auto bits=
1759  expr2bits(expr.op(), expr.id()==ID_byte_extract_little_endian);
1760 
1761  // exact match of length only - otherwise we might lose bits of
1762  // flexible array members at the end of a struct
1763  if(bits.has_value() && mp_integer(bits->size()) == *el_size + *offset * 8)
1764  {
1765  std::string bits_cut = std::string(
1766  bits.value(),
1767  numeric_cast_v<std::size_t>(*offset * 8),
1768  numeric_cast_v<std::size_t>(*el_size));
1769 
1770  exprt tmp=
1771  bits2expr(
1772  bits_cut,
1773  expr.type(),
1774  expr.id()==ID_byte_extract_little_endian);
1775 
1776  if(tmp.is_not_nil())
1777  {
1778  expr.swap(tmp);
1779 
1780  return false;
1781  }
1782  }
1783 
1784  // try to refine it down to extracting from a member or an index in an array
1785  exprt subexpr =
1786  get_subexpression_at_offset(expr.op(), *offset, expr.type(), ns);
1787  if(subexpr.is_nil() || subexpr == expr)
1788  return true;
1789 
1790  simplify_rec(subexpr);
1791  expr.swap(subexpr);
1792  return false;
1793 }
1794 
1796 {
1797  // byte_update(byte_update(root, offset, value), offset, value2) =>
1798  // byte_update(root, offset, value2)
1799  if(expr.id()==expr.op().id() &&
1800  expr.offset()==expr.op().op1() &&
1801  base_type_eq(expr.value().type(), expr.op().op2().type(), ns))
1802  {
1803  expr.op()=expr.op().op0();
1804  return false;
1805  }
1806 
1807  const exprt &root=expr.op();
1808  const exprt &offset=expr.offset();
1809  const exprt &value=expr.value();
1810  const auto val_size = pointer_offset_bits(value.type(), ns);
1811  const auto root_size = pointer_offset_bits(root.type(), ns);
1812 
1813  // byte update of full object is byte_extract(new value)
1814  if(
1815  offset.is_zero() && val_size.has_value() && *val_size > 0 &&
1816  root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
1817  {
1818  byte_extract_exprt be(
1819  expr.id()==ID_byte_update_little_endian ?
1820  ID_byte_extract_little_endian :
1821  ID_byte_extract_big_endian,
1822  value, offset, expr.type());
1823 
1825  expr.swap(be);
1826 
1827  return false;
1828  }
1829 
1830  /*
1831  * byte_update(root, offset,
1832  * extract(root, offset) WITH component:=value)
1833  * =>
1834  * byte_update(root, offset + component offset,
1835  * value)
1836  */
1837 
1838  if(expr.id()!=ID_byte_update_little_endian)
1839  return true;
1840 
1841  if(value.id()==ID_with)
1842  {
1843  const with_exprt &with=to_with_expr(value);
1844 
1845  if(with.old().id()==ID_byte_extract_little_endian)
1846  {
1847  const byte_extract_exprt &extract=to_byte_extract_expr(with.old());
1848 
1849  /* the simplification can be used only if
1850  root and offset of update and extract
1851  are the same */
1852  if(!(root==extract.op()))
1853  return true;
1854  if(!(offset==extract.offset()))
1855  return true;
1856 
1857  const typet &tp=ns.follow(with.type());
1858  if(tp.id()==ID_struct)
1859  {
1860  const struct_typet &struct_type=to_struct_type(tp);
1861  const irep_idt &component_name=with.where().get(ID_component_name);
1862  const typet &c_type = struct_type.get_component(component_name).type();
1863 
1864  // is this a bit field?
1865  if(c_type.id() == ID_c_bit_field || c_type.id() == ID_bool)
1866  {
1867  // don't touch -- might not be byte-aligned
1868  }
1869  else
1870  {
1871  // new offset = offset + component offset
1872  auto i = member_offset(struct_type, component_name, ns);
1873  if(i.has_value())
1874  {
1875  exprt compo_offset = from_integer(*i, offset.type());
1876  plus_exprt new_offset(offset, compo_offset);
1877  simplify_node(new_offset);
1878  exprt new_value(with.op2());
1879  expr.op1().swap(new_offset);
1880  expr.op2().swap(new_value);
1881  simplify_byte_update(expr); // do this recursively
1882  return false;
1883  }
1884  }
1885  }
1886  else if(tp.id()==ID_array)
1887  {
1888  auto i = pointer_offset_size(to_array_type(tp).subtype(), ns);
1889  if(i.has_value())
1890  {
1891  const exprt &index=with.where();
1892  mult_exprt index_offset(index, from_integer(*i, index.type()));
1893  simplify_node(index_offset);
1894 
1895  // index_offset may need a typecast
1896  if(!base_type_eq(offset.type(), index.type(), ns))
1897  {
1898  typecast_exprt tmp(index_offset, offset.type());
1899  simplify_node(tmp);
1900  index_offset.swap(tmp);
1901  }
1902 
1903  plus_exprt new_offset(offset, index_offset);
1904  simplify_node(new_offset);
1905  exprt new_value(with.op2());
1906  expr.op1().swap(new_offset);
1907  expr.op2().swap(new_value);
1908  simplify_byte_update(expr); // do this recursively
1909  return false;
1910  }
1911  }
1912  }
1913  }
1914 
1915  // the following require a constant offset
1916  const auto offset_int = numeric_cast<mp_integer>(offset);
1917  if(!offset_int.has_value() || *offset_int < 0)
1918  return true;
1919 
1920  const typet &op_type=ns.follow(root.type());
1921 
1922  // size must be known
1923  if(!val_size.has_value() || *val_size == 0)
1924  return true;
1925 
1926  // Are we updating (parts of) a struct? Do individual member updates
1927  // instead, unless there are non-byte-sized bit fields
1928  if(op_type.id()==ID_struct)
1929  {
1930  exprt result_expr;
1931  result_expr.make_nil();
1932 
1933  auto update_size = pointer_offset_size(value.type(), ns);
1934 
1935  const struct_typet &struct_type=
1936  to_struct_type(op_type);
1937  const struct_typet::componentst &components=
1938  struct_type.components();
1939 
1940  for(const auto &component : components)
1941  {
1942  auto m_offset = member_offset(struct_type, component.get_name(), ns);
1943 
1944  auto m_size_bits = pointer_offset_bits(component.type(), ns);
1945 
1946  // can we determine the current offset?
1947  if(!m_offset.has_value())
1948  {
1949  result_expr.make_nil();
1950  break;
1951  }
1952 
1953  // is it a byte-sized member?
1954  if(!m_size_bits.has_value() || *m_size_bits == 0 || (*m_size_bits) % 8 != 0)
1955  {
1956  result_expr.make_nil();
1957  break;
1958  }
1959 
1960  mp_integer m_size_bytes = (*m_size_bits) / 8;
1961 
1962  // is that member part of the update?
1963  if(*m_offset + m_size_bytes <= *offset_int)
1964  continue;
1965  // are we done updating?
1966  else if(
1967  update_size.has_value() && *update_size > 0 &&
1968  *m_offset >= *offset_int + *update_size)
1969  {
1970  break;
1971  }
1972 
1973  if(result_expr.is_nil())
1974  result_expr=expr.op();
1975 
1976  exprt member_name(ID_member_name);
1977  member_name.set(ID_component_name, component.get_name());
1978  result_expr=with_exprt(result_expr, member_name, nil_exprt());
1979 
1980  // are we updating on member boundaries?
1981  if(
1982  *m_offset < *offset_int ||
1983  (*m_offset == *offset_int && update_size.has_value() &&
1984  *update_size > 0 && m_size_bytes > *update_size))
1985  {
1987  ID_byte_update_little_endian,
1988  member_exprt(root, component.get_name(), component.type()),
1989  from_integer(*offset_int - *m_offset, offset.type()),
1990  value);
1991 
1992  to_with_expr(result_expr).new_value().swap(v);
1993  }
1994  else if(
1995  update_size.has_value() && *update_size > 0 &&
1996  *m_offset + m_size_bytes > *offset_int + *update_size)
1997  {
1998  // we don't handle this for the moment
1999  result_expr.make_nil();
2000  break;
2001  }
2002  else
2003  {
2005  ID_byte_extract_little_endian,
2006  value,
2007  from_integer(*m_offset - *offset_int, offset.type()),
2008  component.type());
2009 
2010  to_with_expr(result_expr).new_value().swap(v);
2011  }
2012  }
2013 
2014  if(result_expr.is_not_nil())
2015  {
2016  simplify_rec(result_expr);
2017  expr.swap(result_expr);
2018 
2019  return false;
2020  }
2021 
2022  if(result_expr.is_not_nil())
2023  {
2024  simplify_rec(result_expr);
2025  expr.swap(result_expr);
2026 
2027  return false;
2028  }
2029  }
2030 
2031  // replace elements of array or struct expressions, possibly using
2032  // byte_extract
2033  if(root.id()==ID_array)
2034  {
2035  auto el_size = pointer_offset_bits(op_type.subtype(), ns);
2036 
2037  if(!el_size.has_value() || *el_size == 0 ||
2038  (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
2039  {
2040  return true;
2041  }
2042 
2043  exprt result=root;
2044 
2045  mp_integer m_offset_bits=0, val_offset=0;
2046  Forall_operands(it, result)
2047  {
2048  if(*offset_int * 8 + (*val_size) <= m_offset_bits)
2049  break;
2050 
2051  if(*offset_int * 8 < m_offset_bits + *el_size)
2052  {
2053  mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
2054  bytes_req-=val_offset;
2055  if(val_offset + bytes_req > (*val_size) / 8)
2056  bytes_req = (*val_size) / 8 - val_offset;
2057 
2058  byte_extract_exprt new_val(
2059  byte_extract_id(),
2060  value,
2061  from_integer(val_offset, offset.type()),
2063  from_integer(bytes_req, offset.type())));
2064 
2065  *it = byte_update_exprt(
2066  expr.id(),
2067  *it,
2068  from_integer(
2069  *offset_int + val_offset - m_offset_bits / 8, offset.type()),
2070  new_val);
2071 
2072  simplify_rec(*it);
2073 
2074  val_offset+=bytes_req;
2075  }
2076 
2077  m_offset_bits += *el_size;
2078  }
2079 
2080  expr.swap(result);
2081 
2082  return false;
2083  }
2084 
2085  return true;
2086 }
2087 
2089 {
2090  bool result=true;
2091 
2092  // The ifs below could one day be replaced by a switch()
2093 
2094  if(expr.id()==ID_address_of)
2095  {
2096  // the argument of this expression needs special treatment
2097  }
2098  else if(expr.id()==ID_if)
2099  result=simplify_if_preorder(to_if_expr(expr));
2100  else
2101  {
2102  if(expr.has_operands())
2103  {
2104  Forall_operands(it, expr)
2105  if(!simplify_rec(*it)) // recursive call
2106  result=false;
2107  }
2108  }
2109 
2110  return result;
2111 }
2112 
2114 {
2115  if(!expr.has_operands())
2116  return true;
2117 
2118  // #define DEBUGX
2119 
2120  #ifdef DEBUGX
2121  exprt old(expr);
2122  #endif
2123 
2124  bool result=true;
2125 
2126  result=sort_and_join(expr) && result;
2127 
2128  if(expr.id()==ID_typecast)
2129  result=simplify_typecast(expr) && result;
2130  else if(expr.id()==ID_equal || expr.id()==ID_notequal ||
2131  expr.id()==ID_gt || expr.id()==ID_lt ||
2132  expr.id()==ID_ge || expr.id()==ID_le)
2133  result=simplify_inequality(expr) && result;
2134  else if(expr.id()==ID_if)
2135  result=simplify_if(to_if_expr(expr)) && result;
2136  else if(expr.id()==ID_lambda)
2137  result=simplify_lambda(expr) && result;
2138  else if(expr.id()==ID_with)
2139  result=simplify_with(expr) && result;
2140  else if(expr.id()==ID_update)
2141  result=simplify_update(expr) && result;
2142  else if(expr.id()==ID_index)
2143  result=simplify_index(expr) && result;
2144  else if(expr.id()==ID_member)
2145  result=simplify_member(expr) && result;
2146  else if(expr.id()==ID_byte_update_little_endian ||
2147  expr.id()==ID_byte_update_big_endian)
2148  result=simplify_byte_update(to_byte_update_expr(expr)) && result;
2149  else if(expr.id()==ID_byte_extract_little_endian ||
2150  expr.id()==ID_byte_extract_big_endian)
2151  result=simplify_byte_extract(to_byte_extract_expr(expr)) && result;
2152  else if(expr.id()==ID_pointer_object)
2153  result=simplify_pointer_object(expr) && result;
2154  else if(expr.id()==ID_dynamic_object)
2155  result=simplify_dynamic_object(expr) && result;
2156  else if(expr.id()==ID_invalid_pointer)
2157  result=simplify_invalid_pointer(expr) && result;
2158  else if(expr.id()==ID_object_size)
2159  result=simplify_object_size(expr) && result;
2160  else if(expr.id()==ID_good_pointer)
2161  result=simplify_good_pointer(expr) && result;
2162  else if(expr.id()==ID_div)
2163  result=simplify_div(expr) && result;
2164  else if(expr.id()==ID_mod)
2165  result=simplify_mod(expr) && result;
2166  else if(expr.id()==ID_bitnot)
2167  result=simplify_bitnot(expr) && result;
2168  else if(expr.id()==ID_bitand ||
2169  expr.id()==ID_bitor ||
2170  expr.id()==ID_bitxor)
2171  result=simplify_bitwise(expr) && result;
2172  else if(expr.id()==ID_ashr || expr.id()==ID_lshr || expr.id()==ID_shl)
2173  result=simplify_shifts(expr) && result;
2174  else if(expr.id()==ID_power)
2175  result=simplify_power(expr) && result;
2176  else if(expr.id()==ID_plus)
2177  result=simplify_plus(expr) && result;
2178  else if(expr.id()==ID_minus)
2179  result=simplify_minus(expr) && result;
2180  else if(expr.id()==ID_mult)
2181  result=simplify_mult(expr) && result;
2182  else if(expr.id()==ID_floatbv_plus ||
2183  expr.id()==ID_floatbv_minus ||
2184  expr.id()==ID_floatbv_mult ||
2185  expr.id()==ID_floatbv_div)
2186  result=simplify_floatbv_op(expr) && result;
2187  else if(expr.id()==ID_floatbv_typecast)
2188  result=simplify_floatbv_typecast(expr) && result;
2189  else if(expr.id()==ID_unary_minus)
2190  result=simplify_unary_minus(expr) && result;
2191  else if(expr.id()==ID_unary_plus)
2192  result=simplify_unary_plus(expr) && result;
2193  else if(expr.id()==ID_not)
2194  result=simplify_not(expr) && result;
2195  else if(expr.id()==ID_implies ||
2196  expr.id()==ID_or || expr.id()==ID_xor ||
2197  expr.id()==ID_and)
2198  result=simplify_boolean(expr) && result;
2199  else if(expr.id()==ID_dereference)
2200  result=simplify_dereference(expr) && result;
2201  else if(expr.id()==ID_address_of)
2202  result=simplify_address_of(expr) && result;
2203  else if(expr.id()==ID_pointer_offset)
2204  result=simplify_pointer_offset(expr) && result;
2205  else if(expr.id()==ID_extractbit)
2206  result=simplify_extractbit(expr) && result;
2207  else if(expr.id()==ID_concatenation)
2208  result=simplify_concatenation(expr) && result;
2209  else if(expr.id()==ID_extractbits)
2210  result = simplify_extractbits(to_extractbits_expr(expr)) && result;
2211  else if(expr.id()==ID_ieee_float_equal ||
2212  expr.id()==ID_ieee_float_notequal)
2213  result=simplify_ieee_float_relation(expr) && result;
2214  else if(expr.id() == ID_bswap)
2215  result = simplify_bswap(to_bswap_expr(expr)) && result;
2216  else if(expr.id()==ID_isinf)
2217  result=simplify_isinf(expr) && result;
2218  else if(expr.id()==ID_isnan)
2219  result=simplify_isnan(expr) && result;
2220  else if(expr.id()==ID_isnormal)
2221  result=simplify_isnormal(expr) && result;
2222  else if(expr.id()==ID_abs)
2223  result=simplify_abs(expr) && result;
2224  else if(expr.id()==ID_sign)
2225  result=simplify_sign(expr) && result;
2226  else if(expr.id() == ID_popcount)
2227  result = simplify_popcount(to_popcount_expr(expr)) && result;
2228 
2229  #ifdef DEBUGX
2230  if(!result
2231  #ifdef DEBUG_ON_DEMAND
2232  && debug_on
2233  #endif
2234  )
2235  {
2236  std::cout << "===== " << format(old) << "\n ---> " << format(expr)
2237  << "\n";
2238  }
2239  #endif
2240 
2241  return result;
2242 }
2243 
2246 {
2247  // look up in cache
2248 
2249  #ifdef USE_CACHE
2250  std::pair<simplify_expr_cachet::containert::iterator, bool>
2251  cache_result=simplify_expr_cache.container().
2252  insert(std::pair<exprt, exprt>(expr, exprt()));
2253 
2254  if(!cache_result.second) // found!
2255  {
2256  const exprt &new_expr=cache_result.first->second;
2257 
2258  if(new_expr.id().empty())
2259  return true; // no change
2260 
2261  expr=new_expr;
2262  return false;
2263  }
2264  #endif
2265 
2266  // We work on a copy to prevent unnecessary destruction of sharing.
2267  exprt tmp=expr;
2268  bool result=true;
2269 
2270  result=simplify_node_preorder(tmp);
2271 
2272  if(!simplify_node(tmp))
2273  result=false;
2274 
2275 #ifdef USE_LOCAL_REPLACE_MAP
2276  #if 1
2277  replace_mapt::const_iterator it=local_replace_map.find(tmp);
2278  if(it!=local_replace_map.end())
2279  {
2280  tmp=it->second;
2281  result=false;
2282  }
2283  #else
2284  if(!local_replace_map.empty() &&
2285  !replace_expr(local_replace_map, tmp))
2286  {
2287  simplify_rec(tmp);
2288  result=false;
2289  }
2290  #endif
2291 #endif
2292 
2293  if(!result)
2294  {
2295  expr.swap(tmp);
2296 
2297  #ifdef USE_CACHE
2298  // save in cache
2299  cache_result.first->second=expr;
2300  #endif
2301  }
2302 
2303  return result;
2304 }
2305 
2307 {
2308 #ifdef DEBUG_ON_DEMAND
2309  if(debug_on)
2310  std::cout << "TO-SIMP " << format(expr) << "\n";
2311 #endif
2312  bool res=simplify_rec(expr);
2313 #ifdef DEBUG_ON_DEMAND
2314  if(debug_on)
2315  std::cout << "FULLSIMP " << format(expr) << "\n";
2316 #endif
2317  return res;
2318 }
2319 
2320 bool simplify(exprt &expr, const namespacet &ns)
2321 {
2322  return simplify_exprt(ns).simplify(expr);
2323 }
2324 
2325 exprt simplify_expr(const exprt &src, const namespacet &ns)
2326 {
2327  exprt tmp=src;
2328  simplify_exprt(ns).simplify(tmp);
2329  return tmp;
2330 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
simplify_exprt::simplify_node
bool simplify_node(exprt &expr)
Definition: simplify_expr.cpp:2113
to_popcount_expr
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: std_expr.h:4840
exprt::op2
exprt & op2()
Definition: expr.h:90
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
simplify_exprt::simplify_if_recursive
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
Definition: simplify_expr.cpp:851
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
pointer_offset_size.h
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:737
ieee_floatt
Definition: ieee_float.h:119
format
static format_containert< T > format(const T &o)
Definition: format.h:35
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:3770
simplify_exprt::simplify_if_disj
bool simplify_if_disj(exprt &expr, const exprt &cond)
Definition: simplify_expr.cpp:904
exprt::move_to_operands
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
Definition: expr.cpp:29
simplify_exprt::simplify_pointer_object
bool simplify_pointer_object(exprt &expr)
Definition: simplify_expr_pointer.cpp:487
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:87
simplify_exprt::simplify_extractbit
bool simplify_extractbit(exprt &expr)
Definition: simplify_expr_int.cpp:835
simplify_exprt::simplify_index
bool simplify_index(exprt &expr)
Definition: simplify_expr_array.cpp:17
simplify_exprt::simplify_minus
bool simplify_minus(exprt &expr)
Definition: simplify_expr_int.cpp:592
typet::subtype
const typet & subtype() const
Definition: type.h:38
simplify_exprt::simplify_mult
bool simplify_mult(exprt &expr)
Definition: simplify_expr_int.cpp:160
simplify_exprt::simplify_inequality
bool simplify_inequality(exprt &expr)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1305
simplify_expr_class.h
to_integer
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
fixedbvt::from_integer
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
byte_update_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:70
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
arith_tools.h
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
rational.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
rational_tools.h
address_of_exprt::object
exprt & object()
Definition: std_expr.h:3265
simplify_exprt::simplify_isnormal
bool simplify_isnormal(exprt &expr)
Definition: simplify_expr_floatbv.cpp:52
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
ieee_floatt::set_sign
void set_sign(bool _sign)
Definition: ieee_float.h:172
simplify_exprt::simplify_if_preorder
bool simplify_if_preorder(if_exprt &expr)
Definition: simplify_expr.cpp:993
irept::make_nil
void make_nil()
Definition: irep.h:315
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:697
typet
The type of an expression, extends irept.
Definition: type.h:27
update_exprt::old
exprt & old()
Definition: std_expr.h:3729
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:53
fixedbvt::to_integer
mp_integer to_integer() const
Definition: fixedbv.cpp:37
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1398
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
simplify_exprt::simplify
virtual bool simplify(exprt &expr)
Definition: simplify_expr.cpp:2306
fixedbv_spect::get_fraction_bits
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
with_exprt::new_value
exprt & new_value()
Definition: std_expr.h:3552
simplify_exprt::simplify_if_conj
bool simplify_if_conj(exprt &expr, const exprt &cond)
Definition: simplify_expr.cpp:883
fixedbv.h
simplify_exprt::get_values
bool get_values(const exprt &expr, value_listt &value_list)
Definition: simplify_expr.cpp:1182
exprt::make_bool
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
Definition: expr.cpp:109
and_exprt
Boolean AND.
Definition: std_expr.h:2409
union_exprt
Union constructor from single element.
Definition: std_expr.h:1840
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1709
binary_relation_exprt::rhs
exprt & rhs()
Definition: std_expr.h:931
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
ieee_floatt::change_spec
void change_spec(const ieee_float_spect &dest_spec)
Definition: ieee_float.cpp:1044
exprt
Base class for all expressions.
Definition: expr.h:54
simplify_exprt::simplify_if_cond
bool simplify_if_cond(exprt &expr)
Definition: simplify_expr.cpp:957
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:203
simplify_exprt::simplify_bitwise
bool simplify_bitwise(exprt &expr)
Definition: simplify_expr_int.cpp:649
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1890
binary_relation_exprt::lhs
exprt & lhs()
Definition: std_expr.h:921
exprt::op0
exprt & op0()
Definition: expr.h:84
invariant.h
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
bool_typet
The Boolean type.
Definition: std_types.h:28
configt::ansi_c
struct configt::ansi_ct ansi_c
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:199
ieee_floatt::to_integer
mp_integer to_integer() const
Definition: ieee_float.cpp:1069
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
simplify_exprt::simplify_lambda
bool simplify_lambda(exprt &expr)
Definition: simplify_expr.cpp:1208
simplify_exprt::simplify_boolean
bool simplify_boolean(exprt &expr)
Definition: simplify_expr_boolean.cpp:19
namespace.h
simplify_expr
exprt simplify_expr(const exprt &src, const namespacet &ns)
Definition: simplify_expr.cpp:2325
simplify_exprt::simplify_popcount
bool simplify_popcount(popcount_exprt &expr)
Definition: simplify_expr.cpp:132
from_rational
constant_exprt from_rational(const rationalt &a)
Definition: rational_tools.cpp:81
simplify_exprt::simplify_abs
bool simplify_abs(exprt &expr)
Definition: simplify_expr.cpp:62
fixedbvt::to_expr
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
simplify_exprt::simplify_dynamic_object
bool simplify_dynamic_object(exprt &expr)
Definition: simplify_expr_pointer.cpp:515
simplify_exprt::simplify_typecast
bool simplify_typecast(exprt &expr)
Definition: simplify_expr.cpp:160
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3465
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
simplify_exprt::simplify_member
bool simplify_member(exprt &expr)
Definition: simplify_expr_struct.cpp:19
to_bv_type
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: std_types.h:1205
simplify_exprt::simplify_good_pointer
bool simplify_good_pointer(exprt &expr)
Definition: simplify_expr_pointer.cpp:694
ieee_float_spect
Definition: ieee_float.h:25
simplify_exprt::simplify_concatenation
bool simplify_concatenation(exprt &expr)
Definition: simplify_expr_int.cpp:869
simplify_exprt::bits2expr
exprt bits2expr(const std::string &bits, const typet &type, bool little_endian)
Definition: simplify_expr.cpp:1431
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1920
array_typet::size
const exprt & size() const
Definition: std_types.h:1010
c_bool_typet
The C/C++ Booleans.
Definition: std_types.h:1611
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
byte_extract_id
irep_idt byte_extract_id()
Definition: byte_operators.cpp:13
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
with_exprt::old
exprt & old()
Definition: std_expr.h:3532
type_eq.h
byte_operators.h
Expression classes for byte-level operators.
type_eq
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality at the top level.
Definition: type_eq.cpp:31
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1380
or_exprt
Boolean OR.
Definition: std_expr.h:2531
integer2bvrep
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
Definition: arith_tools.cpp:403
base_type
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:135
base_type.h
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:4471
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:3282
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:46
simplify_exprt::simplify_shifts
bool simplify_shifts(exprt &expr)
Definition: simplify_expr_int.cpp:967
simplify_exprt::simplify_not
bool simplify_not(exprt &expr)
Definition: simplify_expr_boolean.cpp:159
namespace_baset::follow_tag
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:91
simplify_exprt::simplify_update
bool simplify_update(exprt &expr)
Definition: simplify_expr.cpp:1288
base_type_eq
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
simplify_exprt::value_listt
std::set< mp_integer > value_listt
Definition: simplify_expr_class.h:141
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:3380
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:127
simplify_exprt::simplify_unary_minus
bool simplify_unary_minus(exprt &expr)
Definition: simplify_expr_int.cpp:1189
simplify_exprt::simplify_invalid_pointer
bool simplify_invalid_pointer(exprt &expr)
Definition: simplify_expr_pointer.cpp:571
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:101
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1278
endianness_mapt::map_bit
size_t map_bit(size_t bit) const
Definition: endianness_map.h:48
simplify_exprt::simplify_node_preorder
bool simplify_node_preorder(exprt &expr)
Definition: simplify_expr.cpp:2088
simplify_exprt::simplify_object_size
bool simplify_object_size(exprt &expr)
Definition: simplify_expr_pointer.cpp:648
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2320
exprt::op1
exprt & op1()
Definition: expr.h:87
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
simplify_exprt::simplify_bswap
bool simplify_bswap(bswap_exprt &expr)
Definition: simplify_expr_int.cpp:29
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
simplify_exprt::simplify_sign
bool simplify_sign(exprt &expr)
Definition: simplify_expr.cpp:102
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
simplify_exprt
Definition: simplify_expr_class.h:43
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
simplify_exprt::simplify_bitnot
bool simplify_bitnot(exprt &expr)
Definition: simplify_expr_int.cpp:1266
irept::swap
void swap(irept &irep)
Definition: irep.h:303
struct_union_typet::has_component
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:215
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
dstringt::empty
bool empty() const
Definition: dstring.h:75
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
union_typet
The union type.
Definition: std_types.h:425
simplify_exprt::simplify_unary_plus
bool simplify_unary_plus(exprt &expr)
Definition: simplify_expr_int.cpp:1179
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
fixedbvt::set_value
void set_value(const mp_integer &_v)
Definition: fixedbv.h:96
simplify_exprt::simplify_pointer_offset
bool simplify_pointer_offset(exprt &expr)
Definition: simplify_expr_pointer.cpp:211
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:512
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
to_bswap_expr
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: std_expr.h:600
simplify_exprt::simplify_floatbv_op
bool simplify_floatbv_op(exprt &expr)
Definition: simplify_expr_floatbv.cpp:283
fixedbv_spect
Definition: fixedbv.h:19
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3569
update_exprt::designator
exprt::operandst & designator()
Definition: std_expr.h:3743
simplify_exprt::simplify_if_branch
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
Definition: simplify_expr.cpp:925
config
configt config
Definition: config.cpp:24
endianness_map.h
ieee_floatt::spec
ieee_float_spect spec
Definition: ieee_float.h:134
fixedbv_typet
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: std_types.h:1337
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1117
simplify_exprt::expr2bits
optionalt< std::string > expr2bits(const exprt &, bool little_endian)
Definition: simplify_expr.cpp:1547
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:47
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
simplify_exprt::simplify_power
bool simplify_power(exprt &expr)
Definition: simplify_expr_int.cpp:1079
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:425
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
simplify_exprt::simplify_ieee_float_relation
bool simplify_ieee_float_relation(exprt &expr)
Definition: simplify_expr_floatbv.cpp:354
simplify_exprt::simplify_isinf
bool simplify_isinf(exprt &expr)
Definition: simplify_expr_floatbv.cpp:19
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
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:90
array_typet
Arrays with given size.
Definition: std_types.h:1000
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3455
to_extractbits_expr
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: std_expr.h:3225
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
is_not_zero
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:98
simplify_exprt::simplify_byte_update
bool simplify_byte_update(byte_update_exprt &expr)
Definition: simplify_expr.cpp:1795
sort_and_join
static bool sort_and_join(const struct saj_tablet &saj_entry, const irep_idt &type_id)
Definition: simplify_utils.cpp:97
update_exprt::new_value
exprt & new_value()
Definition: std_expr.h:3753
simplify_exprt::simplify_address_of
bool simplify_address_of(exprt &expr)
Definition: simplify_expr_pointer.cpp:173
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
byte_update_exprt::value
exprt & value()
Definition: byte_operators.h:84
simplify_exprt::simplify_rec
bool simplify_rec(exprt &expr)
Definition: simplify_expr.cpp:2245
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
replace_mapt
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition: replace_expr.h:22
binary2integer
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3445
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
simplify_exprt::simplify_isnan
bool simplify_isnan(exprt &expr)
Definition: simplify_expr_floatbv.cpp:37
fixedbvt::round
void round(const fixedbv_spect &dest_spec)
Definition: fixedbv.cpp:52
byte_extract_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:25
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
simplify_exprt::simplify_object
bool simplify_object(exprt &expr)
Definition: simplify_expr.cpp:1341
simplify_exprt::simplify_mod
bool simplify_mod(exprt &expr)
Definition: simplify_expr_int.cpp:388
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:218
fixedbvt::spec
fixedbv_spect spec
Definition: fixedbv.h:44
endianness_mapt
Maps a big-endian offset to a little-endian offset.
Definition: endianness_map.h:31
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
simplify_exprt::simplify_if_implies
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
Definition: simplify_expr.cpp:795
byte_update_exprt::offset
exprt & offset()
Definition: byte_operators.h:83
config.h
fixedbvt
Definition: fixedbv.h:41
simplify_exprt::simplify_if
bool simplify_if(if_exprt &expr)
Definition: simplify_expr.cpp:1078
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:158
irep_full_eq
Definition: irep.h:458
simplify_exprt::do_simplify_if
bool do_simplify_if
Definition: simplify_expr_class.h:63
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
ieee_floatt::get_sign
bool get_sign() const
Definition: ieee_float.h:236
exprt::operands
operandst & operands()
Definition: expr.h:78
simplify_exprt::simplify_plus
bool simplify_plus(exprt &expr)
Definition: simplify_expr_int.cpp:437
r
static int8_t r
Definition: irep_hash.h:59
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
index_exprt
Array index operator.
Definition: std_expr.h:1595
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:233
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4815
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
byte_update_exprt::op
exprt & op()
Definition: byte_operators.h:82
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
simplify_utils.h
std_expr.h
constant_exprt::set_value
void set_value(const irep_idt &value)
Definition: std_expr.h:4408
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:4403
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
with_exprt::where
exprt & where()
Definition: std_expr.h:3542
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:24
get_subexpression_at_offset
exprt get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
Definition: pointer_offset_size.cpp:642
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1739
c_types.h
rationalt
Definition: rational.h:17
simplify_exprt::simplify_with
bool simplify_with(exprt &expr)
Definition: simplify_expr.cpp:1215
simplify_exprt::simplify_extractbits
bool simplify_extractbits(extractbits_exprt &expr)
Simplifies extracting of bits from a constant.
Definition: simplify_expr_int.cpp:1102
simplify_exprt::simplify_dereference
bool simplify_dereference(exprt &expr)
Definition: simplify_expr.cpp:737
irep_full_hash
Definition: irep.h:449
simplify_exprt::simplify_byte_extract
bool simplify_byte_extract(byte_extract_exprt &expr)
Definition: simplify_expr.cpp:1619
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1942
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1158
get_bvrep_bit
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
Definition: arith_tools.cpp:285
simplify_exprt::simplify_div
bool simplify_div(exprt &expr)
Definition: simplify_expr_int.cpp:268
simplify_exprt::simplify_floatbv_typecast
bool simplify_floatbv_typecast(exprt &expr)
Definition: simplify_expr_floatbv.cpp:141
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470