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