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