cprover
simplify_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "simplify_expr.h"
10 
11 #include <algorithm>
12 
13 #include "bitvector_expr.h"
14 #include "byte_operators.h"
15 #include "c_types.h"
16 #include "config.h"
17 #include "expr_util.h"
18 #include "fixedbv.h"
19 #include "floatbv_expr.h"
20 #include "invariant.h"
21 #include "mathematical_expr.h"
22 #include "namespace.h"
23 #include "pointer_expr.h"
24 #include "pointer_offset_size.h"
25 #include "pointer_offset_sum.h"
26 #include "range.h"
27 #include "rational.h"
28 #include "rational_tools.h"
29 #include "simplify_utils.h"
30 #include "std_expr.h"
31 #include "string_expr.h"
32 
33 // #define DEBUGX
34 
35 #ifdef DEBUGX
36 #include "format_expr.h"
37 #include <iostream>
38 #endif
39 
40 #include "simplify_expr_class.h"
41 
42 // #define USE_CACHE
43 
44 #ifdef USE_CACHE
45 struct simplify_expr_cachet
46 {
47 public:
48  #if 1
49  typedef std::unordered_map<
50  exprt, exprt, irep_full_hash, irep_full_eq> containert;
51  #else
52  typedef std::unordered_map<exprt, exprt, irep_hash> containert;
53  #endif
54 
55  containert container_normal;
56 
57  containert &container()
58  {
59  return container_normal;
60  }
61 };
62 
63 simplify_expr_cachet simplify_expr_cache;
64 #endif
65 
67 {
68  if(expr.op().is_constant())
69  {
70  const typet &type = to_unary_expr(expr).op().type();
71 
72  if(type.id()==ID_floatbv)
73  {
74  ieee_floatt value(to_constant_expr(to_unary_expr(expr).op()));
75  value.set_sign(false);
76  return value.to_expr();
77  }
78  else if(type.id()==ID_signedbv ||
79  type.id()==ID_unsignedbv)
80  {
81  auto value = numeric_cast<mp_integer>(to_unary_expr(expr).op());
82  if(value.has_value())
83  {
84  if(*value >= 0)
85  {
86  return to_unary_expr(expr).op();
87  }
88  else
89  {
90  value->negate();
91  return from_integer(*value, type);
92  }
93  }
94  }
95  }
96 
97  return unchanged(expr);
98 }
99 
101 {
102  if(expr.op().is_constant())
103  {
104  const typet &type = expr.op().type();
105 
106  if(type.id()==ID_floatbv)
107  {
108  ieee_floatt value(to_constant_expr(expr.op()));
109  return make_boolean_expr(value.get_sign());
110  }
111  else if(type.id()==ID_signedbv ||
112  type.id()==ID_unsignedbv)
113  {
114  const auto value = numeric_cast<mp_integer>(expr.op());
115  if(value.has_value())
116  {
117  return make_boolean_expr(*value >= 0);
118  }
119  }
120  }
121 
122  return unchanged(expr);
123 }
124 
127 {
128  const exprt &op = expr.op();
129 
130  if(op.is_constant())
131  {
132  const typet &op_type = op.type();
133 
134  if(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv)
135  {
136  const auto width = to_bitvector_type(op_type).get_width();
137  const auto &value = to_constant_expr(op).get_value();
138  std::size_t result = 0;
139 
140  for(std::size_t i = 0; i < width; i++)
141  if(get_bvrep_bit(value, width, i))
142  result++;
143 
144  return from_integer(result, expr.type());
145  }
146  }
147 
148  return unchanged(expr);
149 }
150 
153 {
154  const auto const_bits_opt = expr2bits(
155  expr.op(), byte_extract_id() == ID_byte_extract_little_endian, ns);
156 
157  if(!const_bits_opt.has_value())
158  return unchanged(expr);
159 
160  // expr2bits generates a bit string starting with the least-significant bit
161  std::size_t n_leading_zeros = const_bits_opt->rfind('1');
162  if(n_leading_zeros == std::string::npos)
163  {
164  if(!expr.zero_permitted())
165  return unchanged(expr);
166 
167  n_leading_zeros = const_bits_opt->size();
168  }
169  else
170  n_leading_zeros = const_bits_opt->size() - n_leading_zeros - 1;
171 
172  return from_integer(n_leading_zeros, expr.type());
173 }
174 
180  const function_application_exprt &expr,
181  const namespacet &ns)
182 {
183  const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
184  const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
185 
186  if(!s1_data_opt)
187  return simplify_exprt::unchanged(expr);
188 
189  const array_exprt &s1_data = s1_data_opt->get();
190  const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1));
191  const auto s2_data_opt = try_get_string_data_array(s2.content(), ns);
192 
193  if(!s2_data_opt)
194  return simplify_exprt::unchanged(expr);
195 
196  const array_exprt &s2_data = s2_data_opt->get();
197  const bool res = s2_data.operands().size() <= s1_data.operands().size() &&
198  std::equal(
199  s2_data.operands().rbegin(),
200  s2_data.operands().rend(),
201  s1_data.operands().rbegin());
202 
203  return from_integer(res ? 1 : 0, expr.type());
204 }
205 
208  const function_application_exprt &expr,
209  const namespacet &ns)
210 {
211  // We want to get both arguments of any starts-with comparison, and
212  // trace them back to the actual string instance. All variables on the
213  // way must be constant for us to be sure this will work.
214  auto &first_argument = to_string_expr(expr.arguments().at(0));
215  auto &second_argument = to_string_expr(expr.arguments().at(1));
216 
217  const auto first_value_opt =
218  try_get_string_data_array(first_argument.content(), ns);
219 
220  if(!first_value_opt)
221  {
222  return simplify_exprt::unchanged(expr);
223  }
224 
225  const array_exprt &first_value = first_value_opt->get();
226 
227  const auto second_value_opt =
228  try_get_string_data_array(second_argument.content(), ns);
229 
230  if(!second_value_opt)
231  {
232  return simplify_exprt::unchanged(expr);
233  }
234 
235  const array_exprt &second_value = second_value_opt->get();
236 
237  // Is our 'contains' array directly contained in our target.
238  const bool includes =
239  std::search(
240  first_value.operands().begin(),
241  first_value.operands().end(),
242  second_value.operands().begin(),
243  second_value.operands().end()) != first_value.operands().end();
244 
245  return from_integer(includes ? 1 : 0, expr.type());
246 }
247 
253  const function_application_exprt &expr,
254  const namespacet &ns)
255 {
256  const function_application_exprt &function_app =
258  const refined_string_exprt &s =
259  to_string_expr(function_app.arguments().at(0));
260 
261  if(s.length().id() != ID_constant)
262  return simplify_exprt::unchanged(expr);
263 
264  const auto numeric_length =
265  numeric_cast_v<mp_integer>(to_constant_expr(s.length()));
266 
267  return from_integer(numeric_length == 0 ? 1 : 0, expr.type());
268 }
269 
278  const function_application_exprt &expr,
279  const namespacet &ns)
280 {
281  const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
282  const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
283 
284  if(!s1_data_opt)
285  return simplify_exprt::unchanged(expr);
286 
287  const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1));
288  const auto s2_data_opt = try_get_string_data_array(s2.content(), ns);
289 
290  if(!s2_data_opt)
291  return simplify_exprt::unchanged(expr);
292 
293  const array_exprt &s1_data = s1_data_opt->get();
294  const array_exprt &s2_data = s2_data_opt->get();
295 
296  if(s1_data.operands() == s2_data.operands())
297  return from_integer(0, expr.type());
298 
299  const mp_integer s1_size = s1_data.operands().size();
300  const mp_integer s2_size = s2_data.operands().size();
301  const bool first_shorter = s1_size < s2_size;
302  const exprt::operandst &ops1 =
303  first_shorter ? s1_data.operands() : s2_data.operands();
304  const exprt::operandst &ops2 =
305  first_shorter ? s2_data.operands() : s1_data.operands();
306  auto it_pair = std::mismatch(ops1.begin(), ops1.end(), ops2.begin());
307 
308  if(it_pair.first == ops1.end())
309  return from_integer(s1_size - s2_size, expr.type());
310 
311  const mp_integer char1 =
312  numeric_cast_v<mp_integer>(to_constant_expr(*it_pair.first));
313  const mp_integer char2 =
314  numeric_cast_v<mp_integer>(to_constant_expr(*it_pair.second));
315 
316  return from_integer(
317  first_shorter ? char1 - char2 : char2 - char1, expr.type());
318 }
319 
327  const function_application_exprt &expr,
328  const namespacet &ns,
329  const bool search_from_end)
330 {
331  std::size_t starting_index = 0;
332 
333  // Determine starting index for the comparison (if given)
334  if(expr.arguments().size() == 3)
335  {
336  auto &starting_index_expr = expr.arguments().at(2);
337 
338  if(starting_index_expr.id() != ID_constant)
339  {
340  return simplify_exprt::unchanged(expr);
341  }
342 
343  const mp_integer idx =
344  numeric_cast_v<mp_integer>(to_constant_expr(starting_index_expr));
345 
346  // Negative indices are treated like 0
347  if(idx > 0)
348  {
349  starting_index = numeric_cast_v<std::size_t>(idx);
350  }
351  }
352 
353  const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
354 
355  const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
356 
357  if(!s1_data_opt)
358  {
359  return simplify_exprt::unchanged(expr);
360  }
361 
362  const array_exprt &s1_data = s1_data_opt->get();
363 
364  const auto search_string_size = s1_data.operands().size();
365  if(starting_index >= search_string_size)
366  {
367  return from_integer(-1, expr.type());
368  }
369 
370  unsigned long starting_offset =
371  starting_index > 0 ? (search_string_size - 1) - starting_index : 0;
373  {
374  // Second argument is a string
375 
376  const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1));
377 
378  const auto s2_data_opt = try_get_string_data_array(s2.content(), ns);
379 
380  if(!s2_data_opt)
381  {
382  return simplify_exprt::unchanged(expr);
383  }
384 
385  const array_exprt &s2_data = s2_data_opt->get();
386 
387  // Searching for empty string is a special case and is simply the
388  // "always found at the first searched position. This needs to take into
389  // account starting position and if you're starting from the beginning or
390  // end.
391  if(s2_data.operands().empty())
392  return from_integer(
393  search_from_end
394  ? starting_index > 0 ? starting_index : search_string_size
395  : 0,
396  expr.type());
397 
398  if(search_from_end)
399  {
400  auto end = std::prev(s1_data.operands().end(), starting_offset);
401  auto it = std::find_end(
402  s1_data.operands().begin(),
403  end,
404  s2_data.operands().begin(),
405  s2_data.operands().end());
406  if(it != end)
407  return from_integer(
408  std::distance(s1_data.operands().begin(), it), expr.type());
409  }
410  else
411  {
412  auto it = std::search(
413  std::next(s1_data.operands().begin(), starting_index),
414  s1_data.operands().end(),
415  s2_data.operands().begin(),
416  s2_data.operands().end());
417 
418  if(it != s1_data.operands().end())
419  return from_integer(
420  std::distance(s1_data.operands().begin(), it), expr.type());
421  }
422  }
423  else if(expr.arguments().at(1).id() == ID_constant)
424  {
425  // Second argument is a constant character
426 
427  const constant_exprt &c1 = to_constant_expr(expr.arguments().at(1));
428  const auto c1_val = numeric_cast_v<mp_integer>(c1);
429 
430  auto pred = [&](const exprt &c2) {
431  const auto c2_val = numeric_cast_v<mp_integer>(to_constant_expr(c2));
432 
433  return c1_val == c2_val;
434  };
435 
436  if(search_from_end)
437  {
438  auto it = std::find_if(
439  std::next(s1_data.operands().rbegin(), starting_offset),
440  s1_data.operands().rend(),
441  pred);
442  if(it != s1_data.operands().rend())
443  return from_integer(
444  std::distance(s1_data.operands().begin(), it.base() - 1),
445  expr.type());
446  }
447  else
448  {
449  auto it = std::find_if(
450  std::next(s1_data.operands().begin(), starting_index),
451  s1_data.operands().end(),
452  pred);
453  if(it != s1_data.operands().end())
454  return from_integer(
455  std::distance(s1_data.operands().begin(), it), expr.type());
456  }
457  }
458  else
459  {
460  return simplify_exprt::unchanged(expr);
461  }
462 
463  return from_integer(-1, expr.type());
464 }
465 
472  const function_application_exprt &expr,
473  const namespacet &ns)
474 {
475  if(expr.arguments().at(1).id() != ID_constant)
476  {
477  return simplify_exprt::unchanged(expr);
478  }
479 
480  const auto &index = to_constant_expr(expr.arguments().at(1));
481 
482  const refined_string_exprt &s = to_string_expr(expr.arguments().at(0));
483 
484  const auto char_seq_opt = try_get_string_data_array(s.content(), ns);
485 
486  if(!char_seq_opt)
487  {
488  return simplify_exprt::unchanged(expr);
489  }
490 
491  const array_exprt &char_seq = char_seq_opt->get();
492 
493  const auto i_opt = numeric_cast<std::size_t>(index);
494 
495  if(!i_opt || *i_opt >= char_seq.operands().size())
496  {
497  return simplify_exprt::unchanged(expr);
498  }
499 
500  const auto &c = to_constant_expr(char_seq.operands().at(*i_opt));
501 
502  if(c.type() != expr.type())
503  {
504  return simplify_exprt::unchanged(expr);
505  }
506 
507  return c;
508 }
509 
511 static bool lower_case_string_expression(array_exprt &string_data)
512 {
513  auto &operands = string_data.operands();
514  for(auto &operand : operands)
515  {
516  auto &constant_value = to_constant_expr(operand);
517  auto character = numeric_cast_v<unsigned int>(constant_value);
518 
519  // Can't guarantee matches against non-ASCII characters.
520  if(character >= 128)
521  return false;
522 
523  if(isalpha(character))
524  {
525  if(isupper(character))
526  constant_value =
527  from_integer(tolower(character), constant_value.type());
528  }
529  }
530 
531  return true;
532 }
533 
540  const function_application_exprt &expr,
541  const namespacet &ns)
542 {
543  // We want to get both arguments of any starts-with comparison, and
544  // trace them back to the actual string instance. All variables on the
545  // way must be constant for us to be sure this will work.
546  auto &first_argument = to_string_expr(expr.arguments().at(0));
547  auto &second_argument = to_string_expr(expr.arguments().at(1));
548 
549  const auto first_value_opt =
550  try_get_string_data_array(first_argument.content(), ns);
551 
552  if(!first_value_opt)
553  {
554  return simplify_exprt::unchanged(expr);
555  }
556 
557  array_exprt first_value = first_value_opt->get();
558 
559  const auto second_value_opt =
560  try_get_string_data_array(second_argument.content(), ns);
561 
562  if(!second_value_opt)
563  {
564  return simplify_exprt::unchanged(expr);
565  }
566 
567  array_exprt second_value = second_value_opt->get();
568 
569  // Just lower-case both expressions.
570  if(
571  !lower_case_string_expression(first_value) ||
572  !lower_case_string_expression(second_value))
573  return simplify_exprt::unchanged(expr);
574 
575  bool is_equal = first_value == second_value;
576  return from_integer(is_equal ? 1 : 0, expr.type());
577 }
578 
585  const function_application_exprt &expr,
586  const namespacet &ns)
587 {
588  // We want to get both arguments of any starts-with comparison, and
589  // trace them back to the actual string instance. All variables on the
590  // way must be constant for us to be sure this will work.
591  auto &first_argument = to_string_expr(expr.arguments().at(0));
592  auto &second_argument = to_string_expr(expr.arguments().at(1));
593 
594  const auto first_value_opt =
595  try_get_string_data_array(first_argument.content(), ns);
596 
597  if(!first_value_opt)
598  {
599  return simplify_exprt::unchanged(expr);
600  }
601 
602  const array_exprt &first_value = first_value_opt->get();
603 
604  const auto second_value_opt =
605  try_get_string_data_array(second_argument.content(), ns);
606 
607  if(!second_value_opt)
608  {
609  return simplify_exprt::unchanged(expr);
610  }
611 
612  const array_exprt &second_value = second_value_opt->get();
613 
614  mp_integer offset_int = 0;
615  if(expr.arguments().size() == 3)
616  {
617  auto &offset = expr.arguments()[2];
618  if(offset.id() != ID_constant)
619  return simplify_exprt::unchanged(expr);
620  offset_int = numeric_cast_v<mp_integer>(to_constant_expr(offset));
621  }
622 
623  // test whether second_value is a prefix of first_value
624  bool is_prefix =
625  offset_int >= 0 && mp_integer(first_value.operands().size()) >=
626  offset_int + second_value.operands().size();
627  if(is_prefix)
628  {
629  exprt::operandst::const_iterator second_it =
630  second_value.operands().begin();
631  for(const auto &first_op : first_value.operands())
632  {
633  if(offset_int > 0)
634  --offset_int;
635  else if(second_it == second_value.operands().end())
636  break;
637  else if(first_op != *second_it)
638  {
639  is_prefix = false;
640  break;
641  }
642  else
643  ++second_it;
644  }
645  }
646 
647  return from_integer(is_prefix ? 1 : 0, expr.type());
648 }
649 
651  const function_application_exprt &expr)
652 {
653  if(expr.function().id() == ID_lambda)
654  {
655  // expand the function application
656  return to_lambda_expr(expr.function()).application(expr.arguments());
657  }
658 
659  if(expr.function().id() != ID_symbol)
660  return unchanged(expr);
661 
662  const irep_idt &func_id = to_symbol_expr(expr.function()).get_identifier();
663 
664  // String.startsWith() is used to implement String.equals() in the models
665  // library
666  if(func_id == ID_cprover_string_startswith_func)
667  {
668  return simplify_string_startswith(expr, ns);
669  }
670  else if(func_id == ID_cprover_string_endswith_func)
671  {
672  return simplify_string_endswith(expr, ns);
673  }
674  else if(func_id == ID_cprover_string_is_empty_func)
675  {
676  return simplify_string_is_empty(expr, ns);
677  }
678  else if(func_id == ID_cprover_string_compare_to_func)
679  {
680  return simplify_string_compare_to(expr, ns);
681  }
682  else if(func_id == ID_cprover_string_index_of_func)
683  {
684  return simplify_string_index_of(expr, ns, false);
685  }
686  else if(func_id == ID_cprover_string_char_at_func)
687  {
688  return simplify_string_char_at(expr, ns);
689  }
690  else if(func_id == ID_cprover_string_contains_func)
691  {
692  return simplify_string_contains(expr, ns);
693  }
694  else if(func_id == ID_cprover_string_last_index_of_func)
695  {
696  return simplify_string_index_of(expr, ns, true);
697  }
698  else if(func_id == ID_cprover_string_equals_ignore_case_func)
699  {
701  }
702 
703  return unchanged(expr);
704 }
705 
708 {
709  const typet &expr_type = expr.type();
710  const typet &op_type = expr.op().type();
711 
712  // eliminate casts of infinity
713  if(expr.op().id() == ID_infinity)
714  {
715  typet new_type=expr.type();
716  exprt tmp = expr.op();
717  tmp.type()=new_type;
718  return std::move(tmp);
719  }
720 
721  // casts from NULL to any integer
722  if(
723  op_type.id() == ID_pointer && expr.op().is_constant() &&
724  to_constant_expr(expr.op()).get_value() == ID_NULL &&
725  (expr_type.id() == ID_unsignedbv || expr_type.id() == ID_signedbv) &&
727  {
728  return from_integer(0, expr_type);
729  }
730 
731  // casts from pointer to integer
732  // where width of integer >= width of pointer
733  // (void*)(intX)expr -> (void*)expr
734  if(
735  expr_type.id() == ID_pointer && expr.op().id() == ID_typecast &&
736  (op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv) &&
737  to_bitvector_type(op_type).get_width() >=
738  to_bitvector_type(expr_type).get_width())
739  {
740  auto new_expr = expr;
741  new_expr.op() = to_typecast_expr(expr.op()).op();
742  return changed(simplify_typecast(new_expr)); // rec. call
743  }
744 
745  // eliminate redundant typecasts
746  if(expr.type() == expr.op().type())
747  {
748  return expr.op();
749  }
750 
751  // eliminate casts to proper bool
752  if(expr_type.id()==ID_bool)
753  {
754  // rewrite (bool)x to x!=0
755  binary_relation_exprt inequality(
756  expr.op(),
757  op_type.id() == ID_floatbv ? ID_ieee_float_notequal : ID_notequal,
758  from_integer(0, op_type));
759  inequality.add_source_location()=expr.source_location();
760  return changed(simplify_node(inequality));
761  }
762 
763  // eliminate casts from proper bool
764  if(
765  op_type.id() == ID_bool &&
766  (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv ||
767  expr_type.id() == ID_c_bool || expr_type.id() == ID_c_bit_field))
768  {
769  // rewrite (T)(bool) to bool?1:0
770  auto one = from_integer(1, expr_type);
771  auto zero = from_integer(0, expr_type);
772  exprt new_expr = if_exprt(expr.op(), std::move(one), std::move(zero));
773  return changed(simplify_rec(new_expr)); // recursive call
774  }
775 
776  // circular casts through types shorter than `int`
777  if(op_type == signedbv_typet(32) && expr.op().id() == ID_typecast)
778  {
779  if(expr_type==c_bool_typet(8) ||
780  expr_type==signedbv_typet(8) ||
781  expr_type==signedbv_typet(16) ||
782  expr_type==unsignedbv_typet(16))
783  {
784  // We checked that the id was ID_typecast in the enclosing `if`
785  const auto &typecast = expr_checked_cast<typecast_exprt>(expr.op());
786  if(typecast.op().type()==expr_type)
787  {
788  return typecast.op();
789  }
790  }
791  }
792 
793  // eliminate casts to _Bool
794  if(expr_type.id()==ID_c_bool &&
795  op_type.id()!=ID_bool)
796  {
797  // rewrite (_Bool)x to (_Bool)(x!=0)
798  exprt inequality = is_not_zero(expr.op(), ns);
799  auto new_expr = expr;
800  new_expr.op() = simplify_node(std::move(inequality));
801  return changed(simplify_typecast(new_expr)); // recursive call
802  }
803 
804  // eliminate typecasts from NULL
805  if(
806  expr_type.id() == ID_pointer && expr.op().is_constant() &&
807  (to_constant_expr(expr.op()).get_value() == ID_NULL ||
808  (expr.op().is_zero() && config.ansi_c.NULL_is_zero)))
809  {
810  exprt tmp = expr.op();
811  tmp.type()=expr.type();
812  to_constant_expr(tmp).set_value(ID_NULL);
813  return std::move(tmp);
814  }
815 
816  // eliminate duplicate pointer typecasts
817  // (T1 *)(T2 *)x -> (T1 *)x
818  if(
819  expr_type.id() == ID_pointer && expr.op().id() == ID_typecast &&
820  op_type.id() == ID_pointer)
821  {
822  auto new_expr = expr;
823  new_expr.op() = to_typecast_expr(expr.op()).op();
824  return changed(simplify_typecast(new_expr)); // recursive call
825  }
826 
827  // casts from integer to pointer and back:
828  // (int)(void *)int -> (int)(size_t)int
829  if(
830  (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv) &&
831  expr.op().id() == ID_typecast && expr.op().operands().size() == 1 &&
832  op_type.id() == ID_pointer)
833  {
834  auto inner_cast = to_typecast_expr(expr.op());
835  inner_cast.type() = size_type();
836 
837  auto outer_cast = expr;
838  outer_cast.op() = simplify_typecast(inner_cast); // rec. call
839  return changed(simplify_typecast(outer_cast)); // rec. call
840  }
841 
842  // mildly more elaborate version of the above:
843  // (int)((T*)0 + int) -> (int)(sizeof(T)*(size_t)int) if NULL is zero
844  if(
846  (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv) &&
847  op_type.id() == ID_pointer && expr.op().id() == ID_plus &&
848  expr.op().operands().size() == 2)
849  {
850  const auto &op_plus_expr = to_plus_expr(expr.op());
851 
852  if(((op_plus_expr.op0().id() == ID_typecast &&
853  to_typecast_expr(op_plus_expr.op0()).op().is_zero()) ||
854  (op_plus_expr.op0().is_constant() &&
855  to_constant_expr(op_plus_expr.op0()).get_value() == ID_NULL)))
856  {
857  auto sub_size =
858  pointer_offset_size(to_pointer_type(op_type).subtype(), ns);
859  if(sub_size.has_value())
860  {
861  auto new_expr = expr;
862 
863  // void*
864  if(*sub_size == 0 || *sub_size == 1)
865  new_expr.op() = typecast_exprt(op_plus_expr.op1(), size_type());
866  else
867  new_expr.op() = mult_exprt(
868  from_integer(*sub_size, size_type()),
869  typecast_exprt(op_plus_expr.op1(), size_type()));
870 
871  new_expr.op() = simplify_rec(new_expr.op()); // rec. call
872 
873  return changed(simplify_typecast(new_expr)); // rec. call
874  }
875  }
876  }
877 
878  // Push a numerical typecast into various integer operations, i.e.,
879  // (T)(x OP y) ---> (T)x OP (T)y
880  //
881  // Doesn't work for many, e.g., pointer difference, floating-point,
882  // division, modulo.
883  // Many operations fail if the width of T
884  // is bigger than that of (x OP y). This includes ID_bitnot and
885  // anything that might overflow, e.g., ID_plus.
886  //
887  if((expr_type.id()==ID_signedbv || expr_type.id()==ID_unsignedbv) &&
888  (op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv))
889  {
890  bool enlarge=
891  to_bitvector_type(expr_type).get_width()>
892  to_bitvector_type(op_type).get_width();
893 
894  if(!enlarge)
895  {
896  irep_idt op_id = expr.op().id();
897 
898  if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
899  op_id==ID_unary_minus ||
900  op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
901  {
902  exprt result = expr.op();
903 
904  if(
905  result.operands().size() >= 1 &&
906  to_multi_ary_expr(result).op0().type() == result.type())
907  {
908  result.type()=expr.type();
909 
910  Forall_operands(it, result)
911  {
912  auto new_operand = typecast_exprt(*it, expr.type());
913  *it = simplify_typecast(new_operand); // recursive call
914  }
915 
916  return changed(simplify_node(result)); // possibly recursive call
917  }
918  }
919  else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
920  {
921  }
922  }
923  }
924 
925  // Push a numerical typecast into pointer arithmetic
926  // (T)(ptr + int) ---> (T)((size_t)ptr + sizeof(subtype)*(size_t)int)
927  //
928  if(
929  (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv) &&
930  op_type.id() == ID_pointer && expr.op().id() == ID_plus)
931  {
932  const auto step = pointer_offset_size(to_pointer_type(op_type).subtype(), ns);
933 
934  if(step.has_value() && *step != 0)
935  {
936  const typet size_t_type(size_type());
937  auto new_expr = expr;
938 
939  new_expr.op().type() = size_t_type;
940 
941  for(auto &op : new_expr.op().operands())
942  {
943  if(op.type().id()==ID_pointer)
944  {
945  op = typecast_exprt(op, size_t_type);
946  }
947  else
948  {
949  op = typecast_exprt(op, size_t_type);
950  if(*step > 1)
951  op = mult_exprt(from_integer(*step, size_t_type), op);
952  }
953  }
954 
955  return changed(simplify_rec(new_expr)); // recursive call
956  }
957  }
958 
959  #if 0
960  // (T)(a?b:c) --> a?(T)b:(T)c
961  if(expr.op().id()==ID_if &&
962  expr.op().operands().size()==3)
963  {
964  typecast_exprt tmp_op1(expr.op().op1(), expr_type);
965  typecast_exprt tmp_op2(expr.op().op2(), expr_type);
966  simplify_typecast(tmp_op1);
967  simplify_typecast(tmp_op2);
968  auto new_expr=if_exprt(expr.op().op0(), tmp_op1, tmp_op2, expr_type);
969  simplify_if(new_expr);
970  return std::move(new_expr);
971  }
972  #endif
973 
974  const irep_idt &expr_type_id=expr_type.id();
975  const exprt &operand = expr.op();
976  const irep_idt &op_type_id=op_type.id();
977 
978  if(operand.is_constant())
979  {
980  const irep_idt &value=to_constant_expr(operand).get_value();
981 
982  // preserve the sizeof type annotation
983  typet c_sizeof_type=
984  static_cast<const typet &>(operand.find(ID_C_c_sizeof_type));
985 
986  if(op_type_id==ID_integer ||
987  op_type_id==ID_natural)
988  {
989  // from integer to ...
990 
991  mp_integer int_value=string2integer(id2string(value));
992 
993  if(expr_type_id==ID_bool)
994  {
995  return make_boolean_expr(int_value != 0);
996  }
997 
998  if(expr_type_id==ID_unsignedbv ||
999  expr_type_id==ID_signedbv ||
1000  expr_type_id==ID_c_enum ||
1001  expr_type_id==ID_c_bit_field ||
1002  expr_type_id==ID_integer)
1003  {
1004  return from_integer(int_value, expr_type);
1005  }
1006  else if(expr_type_id == ID_c_enum_tag)
1007  {
1008  const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
1009  if(!c_enum_type.is_incomplete()) // possibly incomplete
1010  {
1011  exprt tmp = from_integer(int_value, c_enum_type);
1012  tmp.type() = expr_type; // we maintain the tag type
1013  return std::move(tmp);
1014  }
1015  }
1016  }
1017  else if(op_type_id==ID_rational)
1018  {
1019  }
1020  else if(op_type_id==ID_real)
1021  {
1022  }
1023  else if(op_type_id==ID_bool)
1024  {
1025  if(expr_type_id==ID_unsignedbv ||
1026  expr_type_id==ID_signedbv ||
1027  expr_type_id==ID_integer ||
1028  expr_type_id==ID_natural ||
1029  expr_type_id==ID_rational ||
1030  expr_type_id==ID_c_bool ||
1031  expr_type_id==ID_c_enum ||
1032  expr_type_id==ID_c_bit_field)
1033  {
1034  if(operand.is_true())
1035  {
1036  return from_integer(1, expr_type);
1037  }
1038  else if(operand.is_false())
1039  {
1040  return from_integer(0, expr_type);
1041  }
1042  }
1043  else if(expr_type_id==ID_c_enum_tag)
1044  {
1045  const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
1046  if(!c_enum_type.is_incomplete()) // possibly incomplete
1047  {
1048  unsigned int_value = operand.is_true() ? 1u : 0u;
1049  exprt tmp=from_integer(int_value, c_enum_type);
1050  tmp.type()=expr_type; // we maintain the tag type
1051  return std::move(tmp);
1052  }
1053  }
1054  else if(expr_type_id==ID_pointer &&
1055  operand.is_false() &&
1057  {
1058  return null_pointer_exprt(to_pointer_type(expr_type));
1059  }
1060  }
1061  else if(op_type_id==ID_unsignedbv ||
1062  op_type_id==ID_signedbv ||
1063  op_type_id==ID_c_bit_field ||
1064  op_type_id==ID_c_bool)
1065  {
1066  mp_integer int_value;
1067 
1068  if(to_integer(to_constant_expr(operand), int_value))
1069  return unchanged(expr);
1070 
1071  if(expr_type_id==ID_bool)
1072  {
1073  return make_boolean_expr(int_value != 0);
1074  }
1075 
1076  if(expr_type_id==ID_c_bool)
1077  {
1078  return from_integer(int_value != 0, expr_type);
1079  }
1080 
1081  if(expr_type_id==ID_integer)
1082  {
1083  return from_integer(int_value, expr_type);
1084  }
1085 
1086  if(expr_type_id==ID_natural)
1087  {
1088  if(int_value>=0)
1089  {
1090  return from_integer(int_value, expr_type);
1091  }
1092  }
1093 
1094  if(expr_type_id==ID_unsignedbv ||
1095  expr_type_id==ID_signedbv ||
1096  expr_type_id==ID_bv ||
1097  expr_type_id==ID_c_bit_field)
1098  {
1099  auto result = from_integer(int_value, expr_type);
1100 
1101  if(c_sizeof_type.is_not_nil())
1102  result.set(ID_C_c_sizeof_type, c_sizeof_type);
1103 
1104  return std::move(result);
1105  }
1106 
1107  if(expr_type_id==ID_c_enum_tag)
1108  {
1109  const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
1110  if(!c_enum_type.is_incomplete()) // possibly incomplete
1111  {
1112  exprt tmp=from_integer(int_value, c_enum_type);
1113  tmp.type()=expr_type; // we maintain the tag type
1114  return std::move(tmp);
1115  }
1116  }
1117 
1118  if(expr_type_id==ID_c_enum)
1119  {
1120  return from_integer(int_value, expr_type);
1121  }
1122 
1123  if(expr_type_id==ID_fixedbv)
1124  {
1125  // int to float
1126  const fixedbv_typet &f_expr_type=
1127  to_fixedbv_type(expr_type);
1128 
1129  fixedbvt f;
1130  f.spec=fixedbv_spect(f_expr_type);
1131  f.from_integer(int_value);
1132  return f.to_expr();
1133  }
1134 
1135  if(expr_type_id==ID_floatbv)
1136  {
1137  // int to float
1138  const floatbv_typet &f_expr_type=
1139  to_floatbv_type(expr_type);
1140 
1141  ieee_floatt f(f_expr_type);
1142  f.from_integer(int_value);
1143 
1144  return f.to_expr();
1145  }
1146 
1147  if(expr_type_id==ID_rational)
1148  {
1149  rationalt r(int_value);
1150  return from_rational(r);
1151  }
1152  }
1153  else if(op_type_id==ID_fixedbv)
1154  {
1155  if(expr_type_id==ID_unsignedbv ||
1156  expr_type_id==ID_signedbv)
1157  {
1158  // cast from fixedbv to int
1159  fixedbvt f(to_constant_expr(expr.op()));
1160  return from_integer(f.to_integer(), expr_type);
1161  }
1162  else if(expr_type_id==ID_fixedbv)
1163  {
1164  // fixedbv to fixedbv
1165  fixedbvt f(to_constant_expr(expr.op()));
1166  f.round(fixedbv_spect(to_fixedbv_type(expr_type)));
1167  return f.to_expr();
1168  }
1169  else if(expr_type_id == ID_bv)
1170  {
1171  fixedbvt f{to_constant_expr(expr.op())};
1172  return from_integer(f.get_value(), expr_type);
1173  }
1174  }
1175  else if(op_type_id==ID_floatbv)
1176  {
1177  ieee_floatt f(to_constant_expr(expr.op()));
1178 
1179  if(expr_type_id==ID_unsignedbv ||
1180  expr_type_id==ID_signedbv)
1181  {
1182  // cast from float to int
1183  return from_integer(f.to_integer(), expr_type);
1184  }
1185  else if(expr_type_id==ID_floatbv)
1186  {
1187  // float to double or double to float
1189  return f.to_expr();
1190  }
1191  else if(expr_type_id==ID_fixedbv)
1192  {
1193  fixedbvt fixedbv;
1194  fixedbv.spec=fixedbv_spect(to_fixedbv_type(expr_type));
1195  ieee_floatt factor(f.spec);
1196  factor.from_integer(power(2, fixedbv.spec.get_fraction_bits()));
1197  f*=factor;
1198  fixedbv.set_value(f.to_integer());
1199  return fixedbv.to_expr();
1200  }
1201  else if(expr_type_id == ID_bv)
1202  {
1203  return from_integer(f.pack(), expr_type);
1204  }
1205  }
1206  else if(op_type_id==ID_bv)
1207  {
1208  if(
1209  expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1210  expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1211  expr_type_id == ID_c_bit_field)
1212  {
1213  const auto width = to_bv_type(op_type).get_width();
1214  const auto int_value = bvrep2integer(value, width, false);
1215  if(expr_type_id != ID_c_enum_tag)
1216  return from_integer(int_value, expr_type);
1217  else
1218  {
1219  c_enum_tag_typet tag_type = to_c_enum_tag_type(expr_type);
1220  auto result = from_integer(int_value, ns.follow_tag(tag_type));
1221  result.type() = tag_type;
1222  return std::move(result);
1223  }
1224  }
1225  else if(expr_type_id == ID_floatbv)
1226  {
1227  const auto width = to_bv_type(op_type).get_width();
1228  const auto int_value = bvrep2integer(value, width, false);
1229  ieee_floatt ieee_float{to_floatbv_type(expr_type)};
1230  ieee_float.unpack(int_value);
1231  return ieee_float.to_expr();
1232  }
1233  else if(expr_type_id == ID_fixedbv)
1234  {
1235  const auto width = to_bv_type(op_type).get_width();
1236  const auto int_value = bvrep2integer(value, width, false);
1237  fixedbvt fixedbv{fixedbv_spect{to_fixedbv_type(expr_type)}};
1238  fixedbv.set_value(int_value);
1239  return fixedbv.to_expr();
1240  }
1241  }
1242  else if(op_type_id==ID_c_enum_tag) // enum to int
1243  {
1244  const typet &base_type =
1246  if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv)
1247  {
1248  // enum constants use the representation of their base type
1249  auto new_expr = expr;
1250  new_expr.op().type() = base_type;
1251  return changed(simplify_typecast(new_expr)); // recursive call
1252  }
1253  }
1254  else if(op_type_id==ID_c_enum) // enum to int
1255  {
1256  const typet &base_type=to_c_enum_type(op_type).subtype();
1257  if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv)
1258  {
1259  // enum constants use the representation of their base type
1260  auto new_expr = expr;
1261  new_expr.op().type() = base_type;
1262  return changed(simplify_typecast(new_expr)); // recursive call
1263  }
1264  }
1265  }
1266  else if(operand.id()==ID_typecast) // typecast of typecast
1267  {
1268  // (T1)(T2)x ---> (T1)
1269  // where T1 has fewer bits than T2
1270  if(
1271  op_type_id == expr_type_id &&
1272  (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv) &&
1273  to_bitvector_type(expr_type).get_width() <=
1274  to_bitvector_type(operand.type()).get_width())
1275  {
1276  auto new_expr = expr;
1277  new_expr.op() = to_typecast_expr(operand).op();
1278  // might enable further simplification
1279  return changed(simplify_typecast(new_expr)); // recursive call
1280  }
1281  }
1282  else if(operand.id()==ID_address_of)
1283  {
1284  const exprt &o=to_address_of_expr(operand).object();
1285 
1286  // turn &array into &array[0] when casting to pointer-to-element-type
1287  if(
1288  o.type().id() == ID_array &&
1289  expr_type == pointer_type(o.type().subtype()))
1290  {
1291  auto result =
1293 
1294  return changed(simplify_rec(result)); // recursive call
1295  }
1296  }
1297 
1298  return unchanged(expr);
1299 }
1300 
1303 {
1304  const exprt &pointer = expr.pointer();
1305 
1306  if(pointer.type().id()!=ID_pointer)
1307  return unchanged(expr);
1308 
1309  if(pointer.id()==ID_if && pointer.operands().size()==3)
1310  {
1311  const if_exprt &if_expr=to_if_expr(pointer);
1312 
1313  auto tmp_op1 = expr;
1314  tmp_op1.op() = if_expr.true_case();
1315  exprt tmp_op1_result = simplify_dereference(tmp_op1);
1316 
1317  auto tmp_op2 = expr;
1318  tmp_op2.op() = if_expr.false_case();
1319  exprt tmp_op2_result = simplify_dereference(tmp_op2);
1320 
1321  if_exprt tmp{if_expr.cond(), tmp_op1_result, tmp_op2_result};
1322 
1323  return changed(simplify_if(tmp));
1324  }
1325 
1326  if(pointer.id()==ID_address_of)
1327  {
1328  exprt tmp=to_address_of_expr(pointer).object();
1329  // one address_of is gone, try again
1330  return changed(simplify_rec(tmp));
1331  }
1332  // rewrite *(&a[0] + x) to a[x]
1333  else if(
1334  pointer.id() == ID_plus && pointer.operands().size() == 2 &&
1335  to_plus_expr(pointer).op0().id() == ID_address_of)
1336  {
1337  const auto &pointer_plus_expr = to_plus_expr(pointer);
1338 
1339  const address_of_exprt &address_of =
1340  to_address_of_expr(pointer_plus_expr.op0());
1341 
1342  if(address_of.object().id()==ID_index)
1343  {
1344  const index_exprt &old=to_index_expr(address_of.object());
1345  if(old.array().type().id() == ID_array)
1346  {
1347  index_exprt idx(
1348  old.array(),
1349  pointer_offset_sum(old.index(), pointer_plus_expr.op1()),
1350  old.array().type().subtype());
1351  return changed(simplify_rec(idx));
1352  }
1353  }
1354  }
1355 
1356  return unchanged(expr);
1357 }
1358 
1361 {
1362  return unchanged(expr);
1363 }
1364 
1366 {
1367  bool no_change = true;
1368 
1369  if((expr.operands().size()%2)!=1)
1370  return unchanged(expr);
1371 
1372  // copy
1373  auto with_expr = expr;
1374 
1375  const typet old_type_followed = ns.follow(with_expr.old().type());
1376 
1377  // now look at first operand
1378 
1379  if(old_type_followed.id() == ID_struct)
1380  {
1381  if(with_expr.old().id() == ID_struct || with_expr.old().id() == ID_constant)
1382  {
1383  while(with_expr.operands().size() > 1)
1384  {
1385  const irep_idt &component_name =
1386  with_expr.where().get(ID_component_name);
1387 
1388  if(!to_struct_type(old_type_followed).has_component(component_name))
1389  return unchanged(expr);
1390 
1391  std::size_t number =
1392  to_struct_type(old_type_followed).component_number(component_name);
1393 
1394  if(number >= with_expr.old().operands().size())
1395  return unchanged(expr);
1396 
1397  with_expr.old().operands()[number].swap(with_expr.new_value());
1398 
1399  with_expr.operands().erase(++with_expr.operands().begin());
1400  with_expr.operands().erase(++with_expr.operands().begin());
1401 
1402  no_change = false;
1403  }
1404  }
1405  }
1406  else if(
1407  with_expr.old().type().id() == ID_array ||
1408  with_expr.old().type().id() == ID_vector)
1409  {
1410  if(
1411  with_expr.old().id() == ID_array || with_expr.old().id() == ID_constant ||
1412  with_expr.old().id() == ID_vector)
1413  {
1414  while(with_expr.operands().size() > 1)
1415  {
1416  const auto i = numeric_cast<mp_integer>(with_expr.where());
1417 
1418  if(!i.has_value())
1419  break;
1420 
1421  if(*i < 0 || *i >= with_expr.old().operands().size())
1422  break;
1423 
1424  with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
1425  with_expr.new_value());
1426 
1427  with_expr.operands().erase(++with_expr.operands().begin());
1428  with_expr.operands().erase(++with_expr.operands().begin());
1429 
1430  no_change = false;
1431  }
1432  }
1433  }
1434 
1435  if(with_expr.operands().size() == 1)
1436  return with_expr.old();
1437 
1438  if(no_change)
1439  return unchanged(expr);
1440  else
1441  return std::move(with_expr);
1442 }
1443 
1446 {
1447  // this is to push updates into (possibly nested) constants
1448 
1449  const exprt::operandst &designator = expr.designator();
1450 
1451  exprt updated_value = expr.old();
1452  exprt *value_ptr=&updated_value;
1453 
1454  for(const auto &e : designator)
1455  {
1456  const typet &value_ptr_type=ns.follow(value_ptr->type());
1457 
1458  if(e.id()==ID_index_designator &&
1459  value_ptr->id()==ID_array)
1460  {
1461  const auto i = numeric_cast<mp_integer>(to_index_designator(e).index());
1462 
1463  if(!i.has_value())
1464  return unchanged(expr);
1465 
1466  if(*i < 0 || *i >= value_ptr->operands().size())
1467  return unchanged(expr);
1468 
1469  value_ptr = &value_ptr->operands()[numeric_cast_v<std::size_t>(*i)];
1470  }
1471  else if(e.id()==ID_member_designator &&
1472  value_ptr->id()==ID_struct)
1473  {
1474  const irep_idt &component_name=
1475  e.get(ID_component_name);
1476  const struct_typet &value_ptr_struct_type =
1477  to_struct_type(value_ptr_type);
1478  if(!value_ptr_struct_type.has_component(component_name))
1479  return unchanged(expr);
1480  auto &designator_as_struct_expr = to_struct_expr(*value_ptr);
1481  value_ptr = &designator_as_struct_expr.component(component_name, ns);
1482  CHECK_RETURN(value_ptr->is_not_nil());
1483  }
1484  else
1485  return unchanged(expr); // give up, unknown designator
1486  }
1487 
1488  // found, done
1489  *value_ptr = expr.new_value();
1490  return updated_value;
1491 }
1492 
1494 {
1495  if(expr.id()==ID_plus)
1496  {
1497  if(expr.type().id()==ID_pointer)
1498  {
1499  // kill integers from sum
1500  for(auto &op : expr.operands())
1501  if(op.type().id() == ID_pointer)
1502  return changed(simplify_object(op)); // recursive call
1503  }
1504  }
1505  else if(expr.id()==ID_typecast)
1506  {
1507  auto const &typecast_expr = to_typecast_expr(expr);
1508  const typet &op_type = typecast_expr.op().type();
1509 
1510  if(op_type.id()==ID_pointer)
1511  {
1512  // cast from pointer to pointer
1513  return changed(simplify_object(typecast_expr.op())); // recursive call
1514  }
1515  else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
1516  {
1517  // cast from integer to pointer
1518 
1519  // We do a bit of special treatment for (TYPE *)(a+(int)&o) and
1520  // (TYPE *)(a+(int)((T*)&o+x)), which are re-written to '&o'.
1521 
1522  const exprt &casted_expr = typecast_expr.op();
1523  if(casted_expr.id() == ID_plus && casted_expr.operands().size() == 2)
1524  {
1525  const auto &plus_expr = to_plus_expr(casted_expr);
1526 
1527  const exprt &cand = plus_expr.op0().id() == ID_typecast
1528  ? plus_expr.op0()
1529  : plus_expr.op1();
1530 
1531  if(cand.id() == ID_typecast)
1532  {
1533  const auto &typecast_op = to_typecast_expr(cand).op();
1534 
1535  if(typecast_op.id() == ID_address_of)
1536  {
1537  return typecast_op;
1538  }
1539  else if(
1540  typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1541  to_plus_expr(typecast_op).op0().id() == ID_typecast &&
1542  to_typecast_expr(to_plus_expr(typecast_op).op0()).op().id() ==
1543  ID_address_of)
1544  {
1545  return to_typecast_expr(to_plus_expr(typecast_op).op0()).op();
1546  }
1547  }
1548  }
1549  }
1550  }
1551  else if(expr.id()==ID_address_of)
1552  {
1553  const auto &object = to_address_of_expr(expr).object();
1554 
1555  if(object.id() == ID_index)
1556  {
1557  // &some[i] -> &some
1558  address_of_exprt new_expr(to_index_expr(object).array());
1559  return changed(simplify_object(new_expr)); // recursion
1560  }
1561  else if(object.id() == ID_member)
1562  {
1563  // &some.f -> &some
1564  address_of_exprt new_expr(to_member_expr(object).compound());
1565  return changed(simplify_object(new_expr)); // recursion
1566  }
1567  }
1568 
1569  return unchanged(expr);
1570 }
1571 
1574 {
1575  // lift up any ID_if on the object
1576  if(expr.op().id()==ID_if)
1577  {
1578  if_exprt if_expr=lift_if(expr, 0);
1579  if_expr.true_case() =
1581  if_expr.false_case() =
1583  return changed(simplify_if(if_expr));
1584  }
1585 
1586  const auto el_size = pointer_offset_bits(expr.type(), ns);
1587  if(el_size.has_value() && *el_size < 0)
1588  return unchanged(expr);
1589 
1590  // byte_extract(byte_extract(root, offset1), offset2) =>
1591  // byte_extract(root, offset1+offset2)
1592  if(expr.op().id()==expr.id())
1593  {
1594  auto tmp = expr;
1595 
1596  tmp.offset() = simplify_plus(
1597  plus_exprt(to_byte_extract_expr(expr.op()).offset(), expr.offset()));
1598  tmp.op() = to_byte_extract_expr(expr.op()).op();
1599 
1600  return changed(simplify_byte_extract(tmp)); // recursive call
1601  }
1602 
1603  // byte_extract(byte_update(root, offset, value), offset) =>
1604  // value
1605  if(
1606  ((expr.id() == ID_byte_extract_big_endian &&
1607  expr.op().id() == ID_byte_update_big_endian) ||
1608  (expr.id() == ID_byte_extract_little_endian &&
1609  expr.op().id() == ID_byte_update_little_endian)) &&
1610  expr.offset() == to_byte_update_expr(as_const(expr).op()).offset())
1611  {
1612  const auto &op_byte_update = to_byte_update_expr(expr.op());
1613 
1614  if(expr.type() == op_byte_update.value().type())
1615  {
1616  return op_byte_update.value();
1617  }
1618  else if(
1619  el_size.has_value() &&
1620  *el_size <= pointer_offset_bits(op_byte_update.value().type(), ns))
1621  {
1622  auto tmp = expr;
1623  tmp.op() = op_byte_update.value();
1624  tmp.offset() = from_integer(0, expr.offset().type());
1625 
1626  return changed(simplify_byte_extract(tmp)); // recursive call
1627  }
1628  }
1629 
1630  // the following require a constant offset
1631  auto offset = numeric_cast<mp_integer>(expr.offset());
1632  if(!offset.has_value() || *offset < 0)
1633  return unchanged(expr);
1634 
1635  // don't do any of the following if endianness doesn't match, as
1636  // bytes need to be swapped
1637  if(*offset == 0 && byte_extract_id() == expr.id())
1638  {
1639  // byte extract of full object is object
1640  if(expr.type() == expr.op().type())
1641  {
1642  return expr.op();
1643  }
1644  else if(
1645  expr.type().id() == ID_pointer && expr.op().type().id() == ID_pointer)
1646  {
1647  return typecast_exprt(expr.op(), expr.type());
1648  }
1649  }
1650 
1651  // no proper simplification for expr.type()==void
1652  // or types of unknown size
1653  if(!el_size.has_value() || *el_size == 0)
1654  return unchanged(expr);
1655 
1656  if(expr.op().id()==ID_array_of &&
1657  to_array_of_expr(expr.op()).op().id()==ID_constant)
1658  {
1659  const auto const_bits_opt = expr2bits(
1660  to_array_of_expr(expr.op()).op(),
1661  byte_extract_id() == ID_byte_extract_little_endian,
1662  ns);
1663 
1664  if(!const_bits_opt.has_value())
1665  return unchanged(expr);
1666 
1667  std::string const_bits=const_bits_opt.value();
1668 
1669  DATA_INVARIANT(!const_bits.empty(), "bit representation must be non-empty");
1670 
1671  // double the string until we have sufficiently many bits
1672  while(mp_integer(const_bits.size()) < *offset * 8 + *el_size)
1673  const_bits+=const_bits;
1674 
1675  std::string el_bits = std::string(
1676  const_bits,
1677  numeric_cast_v<std::size_t>(*offset * 8),
1678  numeric_cast_v<std::size_t>(*el_size));
1679 
1680  auto tmp = bits2expr(
1681  el_bits, expr.type(), expr.id() == ID_byte_extract_little_endian, ns);
1682 
1683  if(tmp.has_value())
1684  return std::move(*tmp);
1685  }
1686 
1687  // in some cases we even handle non-const array_of
1688  if(
1689  expr.op().id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
1690  *el_size <=
1692  {
1693  auto tmp = expr;
1694  tmp.op() = index_exprt(expr.op(), expr.offset());
1695  tmp.offset() = from_integer(0, expr.offset().type());
1696  return changed(simplify_rec(tmp));
1697  }
1698 
1699  // extract bits of a constant
1700  const auto bits =
1701  expr2bits(expr.op(), expr.id() == ID_byte_extract_little_endian, ns);
1702 
1703  // make sure we don't lose bits with structs containing flexible array members
1704  const bool struct_has_flexible_array_member = has_subtype(
1705  expr.type(),
1706  [&](const typet &type) {
1707  if(type.id() != ID_struct && type.id() != ID_struct_tag)
1708  return false;
1709 
1710  const struct_typet &st = to_struct_type(ns.follow(type));
1711  const auto &comps = st.components();
1712  if(comps.empty() || comps.back().type().id() != ID_array)
1713  return false;
1714 
1715  const auto size =
1716  numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1717  return !size.has_value() || *size <= 1;
1718  },
1719  ns);
1720  if(
1721  bits.has_value() && mp_integer(bits->size()) >= *el_size + *offset * 8 &&
1722  !struct_has_flexible_array_member)
1723  {
1724  std::string bits_cut = std::string(
1725  bits.value(),
1726  numeric_cast_v<std::size_t>(*offset * 8),
1727  numeric_cast_v<std::size_t>(*el_size));
1728 
1729  auto tmp = bits2expr(
1730  bits_cut, expr.type(), expr.id() == ID_byte_extract_little_endian, ns);
1731 
1732  if(tmp.has_value())
1733  return std::move(*tmp);
1734  }
1735 
1736  // try to refine it down to extracting from a member or an index in an array
1737  auto subexpr =
1738  get_subexpression_at_offset(expr.op(), *offset, expr.type(), ns);
1739  if(!subexpr.has_value() || subexpr.value() == expr)
1740  return unchanged(expr);
1741 
1742  return changed(simplify_rec(subexpr.value())); // recursive call
1743 }
1744 
1747 {
1748  // byte_update(byte_update(root, offset, value), offset, value2) =>
1749  // byte_update(root, offset, value2)
1750  if(
1751  expr.id() == expr.op().id() &&
1752  expr.offset() == to_byte_update_expr(expr.op()).offset() &&
1753  expr.value().type() == to_byte_update_expr(expr.op()).value().type())
1754  {
1755  auto tmp = expr;
1756  tmp.set_op(to_byte_update_expr(expr.op()).op());
1757  return std::move(tmp);
1758  }
1759 
1760  const exprt &root = expr.op();
1761  const exprt &offset = expr.offset();
1762  const exprt &value = expr.value();
1763  const auto val_size = pointer_offset_bits(value.type(), ns);
1764  const auto root_size = pointer_offset_bits(root.type(), ns);
1765 
1766  // byte update of full object is byte_extract(new value)
1767  if(
1768  offset.is_zero() && val_size.has_value() && *val_size > 0 &&
1769  root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
1770  {
1771  byte_extract_exprt be(
1772  expr.id()==ID_byte_update_little_endian ?
1773  ID_byte_extract_little_endian :
1774  ID_byte_extract_big_endian,
1775  value, offset, expr.type());
1776 
1777  return changed(simplify_byte_extract(be));
1778  }
1779 
1780  // update bits in a constant
1781  const auto offset_int = numeric_cast<mp_integer>(offset);
1782  if(
1783  root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
1784  *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
1785  *offset_int + *val_size <= *root_size)
1786  {
1787  auto root_bits =
1788  expr2bits(root, expr.id() == ID_byte_update_little_endian, ns);
1789 
1790  if(root_bits.has_value())
1791  {
1792  const auto val_bits =
1793  expr2bits(value, expr.id() == ID_byte_update_little_endian, ns);
1794 
1795  if(val_bits.has_value())
1796  {
1797  root_bits->replace(
1798  numeric_cast_v<std::size_t>(*offset_int * 8),
1799  numeric_cast_v<std::size_t>(*val_size),
1800  *val_bits);
1801 
1802  auto tmp = bits2expr(
1803  *root_bits,
1804  expr.type(),
1805  expr.id() == ID_byte_update_little_endian,
1806  ns);
1807 
1808  if(tmp.has_value())
1809  return std::move(*tmp);
1810  }
1811  }
1812  }
1813 
1814  /*
1815  * byte_update(root, offset,
1816  * extract(root, offset) WITH component:=value)
1817  * =>
1818  * byte_update(root, offset + component offset,
1819  * value)
1820  */
1821 
1822  if(expr.id()!=ID_byte_update_little_endian)
1823  return unchanged(expr);
1824 
1825  if(value.id()==ID_with)
1826  {
1827  const with_exprt &with=to_with_expr(value);
1828 
1829  if(with.old().id()==ID_byte_extract_little_endian)
1830  {
1831  const byte_extract_exprt &extract=to_byte_extract_expr(with.old());
1832 
1833  /* the simplification can be used only if
1834  root and offset of update and extract
1835  are the same */
1836  if(!(root==extract.op()))
1837  return unchanged(expr);
1838  if(!(offset==extract.offset()))
1839  return unchanged(expr);
1840 
1841  const typet &tp=ns.follow(with.type());
1842  if(tp.id()==ID_struct)
1843  {
1844  const struct_typet &struct_type=to_struct_type(tp);
1845  const irep_idt &component_name=with.where().get(ID_component_name);
1846  const typet &c_type = struct_type.get_component(component_name).type();
1847 
1848  // is this a bit field?
1849  if(c_type.id() == ID_c_bit_field || c_type.id() == ID_bool)
1850  {
1851  // don't touch -- might not be byte-aligned
1852  }
1853  else
1854  {
1855  // new offset = offset + component offset
1856  auto i = member_offset(struct_type, component_name, ns);
1857  if(i.has_value())
1858  {
1859  exprt compo_offset = from_integer(*i, offset.type());
1860  plus_exprt new_offset(offset, compo_offset);
1861  exprt new_value(with.new_value());
1862  auto tmp = expr;
1863  tmp.set_offset(simplify_node(std::move(new_offset)));
1864  tmp.set_value(std::move(new_value));
1865  return changed(simplify_byte_update(tmp)); // recursive call
1866  }
1867  }
1868  }
1869  else if(tp.id()==ID_array)
1870  {
1871  auto i = pointer_offset_size(to_array_type(tp).subtype(), ns);
1872  if(i.has_value())
1873  {
1874  const exprt &index=with.where();
1875  exprt index_offset =
1876  simplify_node(mult_exprt(index, from_integer(*i, index.type())));
1877 
1878  // index_offset may need a typecast
1879  if(offset.type() != index.type())
1880  {
1881  index_offset =
1882  simplify_node(typecast_exprt(index_offset, offset.type()));
1883  }
1884 
1885  plus_exprt new_offset(offset, index_offset);
1886  exprt new_value(with.new_value());
1887  auto tmp = expr;
1888  tmp.set_offset(simplify_node(std::move(new_offset)));
1889  tmp.set_value(std::move(new_value));
1890  return changed(simplify_byte_update(tmp)); // recursive call
1891  }
1892  }
1893  }
1894  }
1895 
1896  // the following require a constant offset
1897  if(!offset_int.has_value() || *offset_int < 0)
1898  return unchanged(expr);
1899 
1900  const typet &op_type=ns.follow(root.type());
1901 
1902  // size must be known
1903  if(!val_size.has_value() || *val_size == 0)
1904  return unchanged(expr);
1905 
1906  // Are we updating (parts of) a struct? Do individual member updates
1907  // instead, unless there are non-byte-sized bit fields
1908  if(op_type.id()==ID_struct)
1909  {
1910  exprt result_expr;
1911  result_expr.make_nil();
1912 
1913  auto update_size = pointer_offset_size(value.type(), ns);
1914 
1915  const struct_typet &struct_type=
1916  to_struct_type(op_type);
1917  const struct_typet::componentst &components=
1918  struct_type.components();
1919 
1920  for(const auto &component : components)
1921  {
1922  auto m_offset = member_offset(struct_type, component.get_name(), ns);
1923 
1924  auto m_size_bits = pointer_offset_bits(component.type(), ns);
1925 
1926  // can we determine the current offset?
1927  if(!m_offset.has_value())
1928  {
1929  result_expr.make_nil();
1930  break;
1931  }
1932 
1933  // is it a byte-sized member?
1934  if(!m_size_bits.has_value() || *m_size_bits == 0 || (*m_size_bits) % 8 != 0)
1935  {
1936  result_expr.make_nil();
1937  break;
1938  }
1939 
1940  mp_integer m_size_bytes = (*m_size_bits) / 8;
1941 
1942  // is that member part of the update?
1943  if(*m_offset + m_size_bytes <= *offset_int)
1944  continue;
1945  // are we done updating?
1946  else if(
1947  update_size.has_value() && *update_size > 0 &&
1948  *m_offset >= *offset_int + *update_size)
1949  {
1950  break;
1951  }
1952 
1953  if(result_expr.is_nil())
1954  result_expr = as_const(expr).op();
1955 
1956  exprt member_name(ID_member_name);
1957  member_name.set(ID_component_name, component.get_name());
1958  result_expr=with_exprt(result_expr, member_name, nil_exprt());
1959 
1960  // are we updating on member boundaries?
1961  if(
1962  *m_offset < *offset_int ||
1963  (*m_offset == *offset_int && update_size.has_value() &&
1964  *update_size > 0 && m_size_bytes > *update_size))
1965  {
1967  ID_byte_update_little_endian,
1968  member_exprt(root, component.get_name(), component.type()),
1969  from_integer(*offset_int - *m_offset, offset.type()),
1970  value);
1971 
1972  to_with_expr(result_expr).new_value().swap(v);
1973  }
1974  else if(
1975  update_size.has_value() && *update_size > 0 &&
1976  *m_offset + m_size_bytes > *offset_int + *update_size)
1977  {
1978  // we don't handle this for the moment
1979  result_expr.make_nil();
1980  break;
1981  }
1982  else
1983  {
1985  ID_byte_extract_little_endian,
1986  value,
1987  from_integer(*m_offset - *offset_int, offset.type()),
1988  component.type());
1989 
1990  to_with_expr(result_expr).new_value().swap(v);
1991  }
1992  }
1993 
1994  if(result_expr.is_not_nil())
1995  return changed(simplify_rec(result_expr));
1996  }
1997 
1998  // replace elements of array or struct expressions, possibly using
1999  // byte_extract
2000  if(root.id()==ID_array)
2001  {
2002  auto el_size = pointer_offset_bits(op_type.subtype(), ns);
2003 
2004  if(!el_size.has_value() || *el_size == 0 ||
2005  (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
2006  {
2007  return unchanged(expr);
2008  }
2009 
2010  exprt result=root;
2011 
2012  mp_integer m_offset_bits=0, val_offset=0;
2013  Forall_operands(it, result)
2014  {
2015  if(*offset_int * 8 + (*val_size) <= m_offset_bits)
2016  break;
2017 
2018  if(*offset_int * 8 < m_offset_bits + *el_size)
2019  {
2020  mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
2021  bytes_req-=val_offset;
2022  if(val_offset + bytes_req > (*val_size) / 8)
2023  bytes_req = (*val_size) / 8 - val_offset;
2024 
2025  byte_extract_exprt new_val(
2026  byte_extract_id(),
2027  value,
2028  from_integer(val_offset, offset.type()),
2030  from_integer(bytes_req, offset.type())));
2031 
2032  *it = byte_update_exprt(
2033  expr.id(),
2034  *it,
2035  from_integer(
2036  *offset_int + val_offset - m_offset_bits / 8, offset.type()),
2037  new_val);
2038 
2039  *it = simplify_rec(*it); // recursive call
2040 
2041  val_offset+=bytes_req;
2042  }
2043 
2044  m_offset_bits += *el_size;
2045  }
2046 
2047  return std::move(result);
2048  }
2049 
2050  return unchanged(expr);
2051 }
2052 
2055 {
2056  if(expr.id() == ID_complex_real)
2057  {
2058  auto &complex_real_expr = to_complex_real_expr(expr);
2059 
2060  if(complex_real_expr.op().id() == ID_complex)
2061  return to_complex_expr(complex_real_expr.op()).real();
2062  }
2063  else if(expr.id() == ID_complex_imag)
2064  {
2065  auto &complex_imag_expr = to_complex_imag_expr(expr);
2066 
2067  if(complex_imag_expr.op().id() == ID_complex)
2068  return to_complex_expr(complex_imag_expr.op()).imag();
2069  }
2070 
2071  return unchanged(expr);
2072 }
2073 
2076 {
2077  // zero is a neutral element for all operations supported here
2078  if(
2079  expr.op1().is_zero() ||
2080  (expr.op0().is_zero() && expr.id() != ID_overflow_minus))
2081  {
2082  return false_exprt{};
2083  }
2084 
2085  // we only handle the case of same operand types
2086  if(expr.op0().type() != expr.op1().type())
2087  return unchanged(expr);
2088 
2089  // catch some cases over mathematical types
2090  const irep_idt &op_type_id = expr.op0().type().id();
2091  if(
2092  op_type_id == ID_integer || op_type_id == ID_rational ||
2093  op_type_id == ID_real)
2094  {
2095  return false_exprt{};
2096  }
2097 
2098  if(op_type_id == ID_natural && expr.id() != ID_overflow_minus)
2099  return false_exprt{};
2100 
2101  // we only handle constants over signedbv/unsignedbv for the remaining cases
2102  if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2103  return unchanged(expr);
2104 
2105  if(!expr.op0().is_constant() || !expr.op1().is_constant())
2106  return unchanged(expr);
2107 
2108  const auto op0_value = numeric_cast<mp_integer>(expr.op0());
2109  const auto op1_value = numeric_cast<mp_integer>(expr.op1());
2110  if(!op0_value.has_value() || !op1_value.has_value())
2111  return unchanged(expr);
2112 
2113  mp_integer no_overflow_result;
2114  if(expr.id() == ID_overflow_plus)
2115  no_overflow_result = *op0_value + *op1_value;
2116  else if(expr.id() == ID_overflow_minus)
2117  no_overflow_result = *op0_value - *op1_value;
2118  else if(expr.id() == ID_overflow_mult)
2119  no_overflow_result = *op0_value * *op1_value;
2120  else if(expr.id() == ID_overflow_shl)
2121  no_overflow_result = *op0_value << *op1_value;
2122  else
2123  UNREACHABLE;
2124 
2125  const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
2126  const integer_bitvector_typet bv_type{op_type_id, width};
2127  if(
2128  no_overflow_result < bv_type.smallest() ||
2129  no_overflow_result > bv_type.largest())
2130  {
2131  return true_exprt{};
2132  }
2133  else
2134  return false_exprt{};
2135 }
2136 
2139 {
2140  // zero is a neutral element for all operations supported here
2141  if(expr.op().is_zero())
2142  return false_exprt{};
2143 
2144  // catch some cases over mathematical types
2145  const irep_idt &op_type_id = expr.op().type().id();
2146  if(
2147  op_type_id == ID_integer || op_type_id == ID_rational ||
2148  op_type_id == ID_real)
2149  {
2150  return false_exprt{};
2151  }
2152 
2153  if(op_type_id == ID_natural)
2154  return true_exprt{};
2155 
2156  // we only handle constants over signedbv/unsignedbv for the remaining cases
2157  if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2158  return unchanged(expr);
2159 
2160  if(!expr.op().is_constant())
2161  return unchanged(expr);
2162 
2163  const auto op_value = numeric_cast<mp_integer>(expr.op());
2164  if(!op_value.has_value())
2165  return unchanged(expr);
2166 
2167  mp_integer no_overflow_result;
2168  if(expr.id() == ID_overflow_unary_minus)
2169  no_overflow_result = -*op_value;
2170  else
2171  UNREACHABLE;
2172 
2173  const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
2174  const integer_bitvector_typet bv_type{op_type_id, width};
2175  if(
2176  no_overflow_result < bv_type.smallest() ||
2177  no_overflow_result > bv_type.largest())
2178  {
2179  return true_exprt{};
2180  }
2181  else
2182  return false_exprt{};
2183 }
2184 
2186 {
2187  bool result=true;
2188 
2189  // The ifs below could one day be replaced by a switch()
2190 
2191  if(expr.id()==ID_address_of)
2192  {
2193  // the argument of this expression needs special treatment
2194  }
2195  else if(expr.id()==ID_if)
2196  result=simplify_if_preorder(to_if_expr(expr));
2197  else
2198  {
2199  if(expr.has_operands())
2200  {
2201  Forall_operands(it, expr)
2202  {
2203  auto r_it = simplify_rec(*it); // recursive call
2204  if(r_it.has_changed())
2205  {
2206  *it = r_it.expr;
2207  result=false;
2208  }
2209  }
2210  }
2211  }
2212 
2213  return result;
2214 }
2215 
2217 {
2218  if(!node.has_operands())
2219  return unchanged(node); // no change
2220 
2221  // #define DEBUGX
2222 
2223 #ifdef DEBUGX
2224  exprt old(node);
2225 #endif
2226 
2227  exprt expr = node;
2228  bool no_change_join_operands = join_operands(expr);
2229 
2230  resultt<> r = unchanged(expr);
2231 
2232  if(expr.id()==ID_typecast)
2233  {
2235  }
2236  else if(expr.id()==ID_equal || expr.id()==ID_notequal ||
2237  expr.id()==ID_gt || expr.id()==ID_lt ||
2238  expr.id()==ID_ge || expr.id()==ID_le)
2239  {
2241  }
2242  else if(expr.id()==ID_if)
2243  {
2244  r = simplify_if(to_if_expr(expr));
2245  }
2246  else if(expr.id()==ID_lambda)
2247  {
2248  r = simplify_lambda(to_lambda_expr(expr));
2249  }
2250  else if(expr.id()==ID_with)
2251  {
2252  r = simplify_with(to_with_expr(expr));
2253  }
2254  else if(expr.id()==ID_update)
2255  {
2256  r = simplify_update(to_update_expr(expr));
2257  }
2258  else if(expr.id()==ID_index)
2259  {
2260  r = simplify_index(to_index_expr(expr));
2261  }
2262  else if(expr.id()==ID_member)
2263  {
2264  r = simplify_member(to_member_expr(expr));
2265  }
2266  else if(expr.id()==ID_byte_update_little_endian ||
2267  expr.id()==ID_byte_update_big_endian)
2268  {
2270  }
2271  else if(expr.id()==ID_byte_extract_little_endian ||
2272  expr.id()==ID_byte_extract_big_endian)
2273  {
2275  }
2276  else if(expr.id()==ID_pointer_object)
2277  {
2279  }
2280  else if(expr.id() == ID_is_dynamic_object)
2281  {
2283  }
2284  else if(expr.id() == ID_is_invalid_pointer)
2285  {
2287  }
2288  else if(expr.id()==ID_object_size)
2289  {
2291  }
2292  else if(expr.id()==ID_good_pointer)
2293  {
2295  }
2296  else if(expr.id()==ID_div)
2297  {
2298  r = simplify_div(to_div_expr(expr));
2299  }
2300  else if(expr.id()==ID_mod)
2301  {
2302  r = simplify_mod(to_mod_expr(expr));
2303  }
2304  else if(expr.id()==ID_bitnot)
2305  {
2306  r = simplify_bitnot(to_bitnot_expr(expr));
2307  }
2308  else if(expr.id()==ID_bitand ||
2309  expr.id()==ID_bitor ||
2310  expr.id()==ID_bitxor)
2311  {
2313  }
2314  else if(expr.id()==ID_ashr || expr.id()==ID_lshr || expr.id()==ID_shl)
2315  {
2316  r = simplify_shifts(to_shift_expr(expr));
2317  }
2318  else if(expr.id()==ID_power)
2319  {
2320  r = simplify_power(to_binary_expr(expr));
2321  }
2322  else if(expr.id()==ID_plus)
2323  {
2324  r = simplify_plus(to_plus_expr(expr));
2325  }
2326  else if(expr.id()==ID_minus)
2327  {
2328  r = simplify_minus(to_minus_expr(expr));
2329  }
2330  else if(expr.id()==ID_mult)
2331  {
2332  r = simplify_mult(to_mult_expr(expr));
2333  }
2334  else if(expr.id()==ID_floatbv_plus ||
2335  expr.id()==ID_floatbv_minus ||
2336  expr.id()==ID_floatbv_mult ||
2337  expr.id()==ID_floatbv_div)
2338  {
2340  }
2341  else if(expr.id()==ID_floatbv_typecast)
2342  {
2344  }
2345  else if(expr.id()==ID_unary_minus)
2346  {
2348  }
2349  else if(expr.id()==ID_unary_plus)
2350  {
2352  }
2353  else if(expr.id()==ID_not)
2354  {
2355  r = simplify_not(to_not_expr(expr));
2356  }
2357  else if(expr.id()==ID_implies ||
2358  expr.id()==ID_or || expr.id()==ID_xor ||
2359  expr.id()==ID_and)
2360  {
2361  r = simplify_boolean(expr);
2362  }
2363  else if(expr.id()==ID_dereference)
2364  {
2366  }
2367  else if(expr.id()==ID_address_of)
2368  {
2370  }
2371  else if(expr.id()==ID_pointer_offset)
2372  {
2374  }
2375  else if(expr.id()==ID_extractbit)
2376  {
2378  }
2379  else if(expr.id()==ID_concatenation)
2380  {
2382  }
2383  else if(expr.id()==ID_extractbits)
2384  {
2386  }
2387  else if(expr.id()==ID_ieee_float_equal ||
2388  expr.id()==ID_ieee_float_notequal)
2389  {
2391  }
2392  else if(expr.id() == ID_bswap)
2393  {
2394  r = simplify_bswap(to_bswap_expr(expr));
2395  }
2396  else if(expr.id()==ID_isinf)
2397  {
2398  r = simplify_isinf(to_unary_expr(expr));
2399  }
2400  else if(expr.id()==ID_isnan)
2401  {
2402  r = simplify_isnan(to_unary_expr(expr));
2403  }
2404  else if(expr.id()==ID_isnormal)
2405  {
2407  }
2408  else if(expr.id()==ID_abs)
2409  {
2410  r = simplify_abs(to_abs_expr(expr));
2411  }
2412  else if(expr.id()==ID_sign)
2413  {
2414  r = simplify_sign(to_sign_expr(expr));
2415  }
2416  else if(expr.id() == ID_popcount)
2417  {
2419  }
2420  else if(expr.id() == ID_count_leading_zeros)
2421  {
2423  }
2424  else if(expr.id() == ID_function_application)
2425  {
2427  }
2428  else if(expr.id() == ID_complex_real || expr.id() == ID_complex_imag)
2429  {
2430  r = simplify_complex(to_unary_expr(expr));
2431  }
2432  else if(
2433  expr.id() == ID_overflow_plus || expr.id() == ID_overflow_minus ||
2434  expr.id() == ID_overflow_mult || expr.id() == ID_overflow_shl)
2435  {
2437  }
2438  else if(expr.id() == ID_overflow_unary_minus)
2439  {
2441  }
2442 
2443  if(!no_change_join_operands)
2444  r = changed(r);
2445 
2446 #ifdef DEBUGX
2447  if(
2448  r.has_changed()
2449 # ifdef DEBUG_ON_DEMAND
2450  && debug_on
2451 # endif
2452  )
2453  {
2454  std::cout << "===== " << node.id() << ": " << format(node) << '\n'
2455  << " ---> " << format(r.expr) << '\n';
2456  }
2457 #endif
2458 
2459  return r;
2460 }
2461 
2463 {
2464  // look up in cache
2465 
2466  #ifdef USE_CACHE
2467  std::pair<simplify_expr_cachet::containert::iterator, bool>
2468  cache_result=simplify_expr_cache.container().
2469  insert(std::pair<exprt, exprt>(expr, exprt()));
2470 
2471  if(!cache_result.second) // found!
2472  {
2473  const exprt &new_expr=cache_result.first->second;
2474 
2475  if(new_expr.id().empty())
2476  return true; // no change
2477 
2478  expr=new_expr;
2479  return false;
2480  }
2481  #endif
2482 
2483  // We work on a copy to prevent unnecessary destruction of sharing.
2484  exprt tmp=expr;
2485  bool no_change = simplify_node_preorder(tmp);
2486 
2487  auto simplify_node_result = simplify_node(tmp);
2488 
2489  if(simplify_node_result.has_changed())
2490  {
2491  no_change = false;
2492  tmp = simplify_node_result.expr;
2493  }
2494 
2495 #ifdef USE_LOCAL_REPLACE_MAP
2496  #if 1
2497  replace_mapt::const_iterator it=local_replace_map.find(tmp);
2498  if(it!=local_replace_map.end())
2499  {
2500  tmp=it->second;
2501  no_change = false;
2502  }
2503  #else
2504  if(!local_replace_map.empty() &&
2505  !replace_expr(local_replace_map, tmp))
2506  {
2507  simplify_rec(tmp);
2508  no_change = false;
2509  }
2510  #endif
2511 #endif
2512 
2513  if(no_change) // no change
2514  {
2515  return unchanged(expr);
2516  }
2517  else // change, new expression is 'tmp'
2518  {
2519  POSTCONDITION(as_const(tmp).type() == expr.type());
2520 
2521 #ifdef USE_CACHE
2522  // save in cache
2523  cache_result.first->second = tmp;
2524 #endif
2525 
2526  return std::move(tmp);
2527  }
2528 }
2529 
2532 {
2533 #ifdef DEBUG_ON_DEMAND
2534  if(debug_on)
2535  std::cout << "TO-SIMP " << format(expr) << "\n";
2536 #endif
2537  auto result = simplify_rec(expr);
2538 #ifdef DEBUG_ON_DEMAND
2539  if(debug_on)
2540  std::cout << "FULLSIMP " << format(result.expr) << "\n";
2541 #endif
2542  if(result.has_changed())
2543  {
2544  expr = result.expr;
2545  return false; // change
2546  }
2547  else
2548  return true; // no change
2549 }
2550 
2552 bool simplify(exprt &expr, const namespacet &ns)
2553 {
2554  return simplify_exprt(ns).simplify(expr);
2555 }
2556 
2558 {
2559  simplify_exprt(ns).simplify(src);
2560  return src;
2561 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2172
simplify_exprt::simplify_rec
resultt simplify_rec(const exprt &)
Definition: simplify_expr.cpp:2462
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
exprt::op2
exprt & op2()
Definition: expr.h:109
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
simplify_exprt::simplify_is_invalid_pointer
resultt simplify_is_invalid_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:621
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:215
simplify_exprt::simplify_isnormal
resultt simplify_isnormal(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:52
ieee_floatt
Definition: ieee_float.h:120
format
static format_containert< T > format(const T &o)
Definition: format.h:37
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2421
to_extractbit_expr
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: bitvector_expr.h:411
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:168
simplify_exprt::simplify_shifts
resultt simplify_shifts(const shift_exprt &)
Definition: simplify_expr_int.cpp:909
simplify_string_index_of
static simplify_exprt::resultt simplify_string_index_of(const function_application_exprt &expr, const namespacet &ns, const bool search_from_end)
Simplify String.indexOf function when arguments are constant.
Definition: simplify_expr.cpp:326
typet::subtype
const typet & subtype() const
Definition: type.h:47
simplify_exprt::simplify_dereference
resultt simplify_dereference(const dereference_exprt &)
Definition: simplify_expr.cpp:1302
simplify_exprt::simplify_concatenation
resultt simplify_concatenation(const concatenation_exprt &)
Definition: simplify_expr_int.cpp:807
to_lambda_expr
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
Definition: mathematical_expr.h:423
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1029
simplify_expr_class.h
fixedbvt::from_integer
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:33
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:81
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
simplify_exprt::simplify_address_of
resultt simplify_address_of(const address_of_exprt &)
Definition: simplify_expr_pointer.cpp:210
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
rational.h
simplify_exprt::simplify_unary_plus
resultt simplify_unary_plus(const unary_plus_exprt &)
Definition: simplify_expr_int.cpp:1114
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
simplify_exprt::simplify_bitwise
resultt simplify_bitwise(const multi_ary_exprt &)
Definition: simplify_expr_int.cpp:601
rational_tools.h
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:339
ieee_floatt::set_sign
void set_sign(bool _sign)
Definition: ieee_float.h:172
simplify_exprt::simplify_if_preorder
bool simplify_if_preorder(if_exprt &expr)
Definition: simplify_expr_if.cpp:215
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:442
array_of_exprt::what
exprt & what()
Definition: std_expr.h:1333
irept::make_nil
void make_nil()
Definition: irep.h:465
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
simplify_exprt::simplify_bitnot
resultt simplify_bitnot(const bitnot_exprt &)
Definition: simplify_expr_int.cpp:1181
to_string_expr
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:150
typet
The type of an expression, extends irept.
Definition: type.h:28
update_exprt::old
exprt & old()
Definition: std_expr.h:2368
simplify_exprt::simplify_overflow_binary
resultt simplify_overflow_binary(const binary_overflow_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
Definition: simplify_expr.cpp:2075
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
fixedbvt::to_integer
mp_integer to_integer() const
Definition: fixedbv.cpp:38
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
bits2expr
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
Definition: simplify_utils.cpp:194
simplify_string_endswith
static simplify_exprt::resultt simplify_string_endswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.endsWith function when arguments are constant.
Definition: simplify_expr.cpp:179
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:386
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
byte_update_exprt::offset
const exprt & offset() const
Definition: byte_operators.h:109
simplify_exprt::simplify_popcount
resultt simplify_popcount(const popcount_exprt &)
Definition: simplify_expr.cpp:126
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: bitvector_types.h:322
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
simplify_exprt::simplify
virtual bool simplify(exprt &expr)
Definition: simplify_expr.cpp:2531
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:277
simplify_exprt::simplify_is_dynamic_object
resultt simplify_is_dynamic_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:562
fixedbv_spect::get_fraction_bits
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
with_exprt::new_value
exprt & new_value()
Definition: std_expr.h:2202
fixedbv.h
simplify_string_char_at
static simplify_exprt::resultt simplify_string_char_at(const function_application_exprt &expr, const namespacet &ns)
Simplify String.charAt function when arguments are constant.
Definition: simplify_expr.cpp:471
s1
int8_t s1
Definition: bytecode_info.h:59
simplify_exprt::simplify_clz
resultt simplify_clz(const count_leading_zeros_exprt &)
Try to simplify count-leading-zeros to a constant expression.
Definition: simplify_expr.cpp:152
simplify_exprt::simplify_update
resultt simplify_update(const update_exprt &)
Definition: simplify_expr.cpp:1445
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1361
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
simplify_exprt::simplify_boolean
resultt simplify_boolean(const exprt &)
Definition: simplify_expr_boolean.cpp:20
ieee_floatt::change_spec
void change_spec(const ieee_float_spect &dest_spec)
Definition: ieee_float.cpp:1045
simplify_exprt::simplify_overflow_unary
resultt simplify_overflow_unary(const unary_overflow_exprt &)
Try to simplify overflow-unary-.
Definition: simplify_expr.cpp:2138
simplify_string_compare_to
static simplify_exprt::resultt simplify_string_compare_to(const function_application_exprt &expr, const namespacet &ns)
Simplify String.compareTo function when arguments are constant.
Definition: simplify_expr.cpp:277
simplify_string_equals_ignore_case
static simplify_exprt::resultt simplify_string_equals_ignore_case(const function_application_exprt &expr, const namespacet &ns)
Simplify String.equalsIgnorecase function when arguments are constant.
Definition: simplify_expr.cpp:539
exprt
Base class for all expressions.
Definition: expr.h:54
to_complex_expr
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1670
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
simplify_exprt::simplify_extractbit
resultt simplify_extractbit(const extractbit_exprt &)
Definition: simplify_expr_int.cpp:778
to_bv_type
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: bitvector_types.h:82
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:66
byte_update_exprt::set_op
void set_op(exprt e)
Definition: byte_operators.h:95
sign_exprt
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:506
exprt::op0
exprt & op0()
Definition: expr.h:103
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
to_bitnot_expr
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: bitvector_expr.h:106
lift_if
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:203
can_cast_expr< refined_string_exprt >
bool can_cast_expr< refined_string_exprt >(const exprt &base)
Definition: string_expr.h:165
ieee_floatt::to_integer
mp_integer to_integer() const
Definition: ieee_float.cpp:1070
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:60
simplify_exprt::simplify_complex
resultt simplify_complex(const unary_exprt &)
Definition: simplify_expr.cpp:2054
simplify_exprt::simplify_pointer_offset
resultt simplify_pointer_offset(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:248
configt::ansi_c
struct configt::ansi_ct ansi_c
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
try_get_string_data_array
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)
Get char sequence from content field of a refined string expression.
Definition: simplify_utils.cpp:481
simplify_exprt::simplify_plus
resultt simplify_plus(const plus_exprt &)
Definition: simplify_expr_int.cpp:403
namespace.h
struct_union_typet::component_number
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:36
from_rational
constant_exprt from_rational(const rationalt &a)
Definition: rational_tools.cpp:81
fixedbvt::to_expr
constant_exprt to_expr() const
Definition: fixedbv.cpp:44
to_popcount_expr
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: bitvector_expr.h:667
simplify_exprt::simplify_byte_extract
resultt simplify_byte_extract(const byte_extract_exprt &)
Definition: simplify_expr.cpp:1573
simplify_exprt::simplify_not
resultt simplify_not(const not_exprt &)
Definition: simplify_expr_boolean.cpp:165
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:914
simplify_exprt::unchanged
static resultt unchanged(exprt expr)
Definition: simplify_expr_class.h:129
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2123
simplify_exprt::simplify_node
resultt simplify_node(exprt)
Definition: simplify_expr.cpp:2216
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:69
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: bitvector_types.h:159
refined_string_exprt
Definition: string_expr.h:109
refined_string_exprt::length
const exprt & length() const
Definition: string_expr.h:128
to_floatbv_typecast_expr
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: bitvector_types.h:305
ieee_float_spect
Definition: ieee_float.h:26
to_unary_plus_expr
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:464
to_complex_real_expr
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1715
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
to_bswap_expr
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: bitvector_expr.h:63
simplify_exprt::simplify_if
resultt simplify_if(const if_exprt &)
Definition: simplify_expr_if.cpp:331
c_bool_typet
The C/C++ Booleans.
Definition: c_types.h:62
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
complex_exprt::imag
exprt imag()
Definition: std_expr.h:1642
simplify_string_startswith
static simplify_exprt::resultt simplify_string_startswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.startsWith function when arguments are constant.
Definition: simplify_expr.cpp:584
byte_extract_id
irep_idt byte_extract_id()
Definition: byte_operators.cpp:13
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
simplify_exprt::simplify_minus
resultt simplify_minus(const minus_exprt &)
Definition: simplify_expr_int.cpp:559
count_leading_zeros_exprt::zero_permitted
bool zero_permitted() const
Definition: bitvector_expr.h:844
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
with_exprt::old
exprt & old()
Definition: std_expr.h:2182
byte_operators.h
Expression classes for byte-level operators.
simplify_exprt::simplify_power
resultt simplify_power(const binary_exprt &)
Definition: simplify_expr_int.cpp:1017
simplify_exprt::simplify_div
resultt simplify_div(const div_exprt &)
Definition: simplify_expr_int.cpp:272
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
simplify_exprt::simplify_typecast
resultt simplify_typecast(const typecast_exprt &)
Definition: simplify_expr.cpp:707
base_type
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:110
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1074
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:960
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:461
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
simplify_exprt::simplify_mod
resultt simplify_mod(const mod_exprt &)
Definition: simplify_expr_int.cpp:366
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
simplify_exprt::simplify_isnan
resultt simplify_isnan(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:38
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:317
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:120
binary_overflow_exprt
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
Definition: bitvector_expr.h:687
simplify_exprt::changed
static resultt changed(resultt<> result)
Definition: simplify_expr_class.h:134
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
has_subtype
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Definition: expr_util.cpp:155
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:399
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: bitvector_types.h:208
pointer_offset_sum
exprt pointer_offset_sum(const exprt &a, const exprt &b)
Definition: pointer_offset_sum.cpp:16
join_operands
bool join_operands(exprt &expr)
Definition: simplify_utils.cpp:189
simplify_exprt::simplify_bswap
resultt simplify_bswap(const bswap_exprt &)
Definition: simplify_expr_int.cpp:30
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:869
pointer_expr.h
API to expression classes for Pointers.
simplify_exprt::simplify_node_preorder
bool simplify_node_preorder(exprt &expr)
Definition: simplify_expr.cpp:2185
integer_bitvector_typet
Fixed-width bit-vector representing a signed or unsigned integer.
Definition: bitvector_types.h:99
to_unary_overflow_expr
const unary_overflow_exprt & to_unary_overflow_expr(const exprt &expr)
Cast an exprt to a unary_overflow_exprt.
Definition: bitvector_expr.h:807
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2552
exprt::op1
exprt & op1()
Definition: expr.h:106
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:194
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:935
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2557
simplify_exprt::simplify_inequality
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1212
index_exprt::index
exprt & index()
Definition: std_expr.h:1268
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
ieee_floatt::pack
mp_integer pack() const
Definition: ieee_float.cpp:371
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
simplify_exprt
Definition: simplify_expr_class.h:73
index_exprt::array
exprt & array()
Definition: std_expr.h:1258
irept::swap
void swap(irept &irep)
Definition: irep.h:453
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
struct_union_typet::has_component
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:151
simplify_exprt::simplify_good_pointer
resultt simplify_good_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:705
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
dstringt::empty
bool empty() const
Definition: dstring.h:88
abs_exprt
Absolute value.
Definition: std_expr.h:346
simplify_string_contains
static simplify_exprt::resultt simplify_string_contains(const function_application_exprt &expr, const namespacet &ns)
Simplify String.contains function when arguments are constant.
Definition: simplify_expr.cpp:207
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
floatbv_expr.h
API to expression classes for floating-point arithmetic.
simplify_exprt::simplify_mult
resultt simplify_mult(const mult_exprt &)
Definition: simplify_expr_int.cpp:160
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
fixedbvt::set_value
void set_value(const mp_integer &_v)
Definition: fixedbv.h:96
simplify_exprt::simplify_with
resultt simplify_with(const with_exprt &)
Definition: simplify_expr.cpp:1365
simplify_exprt::resultt
Definition: simplify_expr_class.h:96
simplify_exprt::simplify_unary_minus
resultt simplify_unary_minus(const unary_minus_exprt &)
Definition: simplify_expr_int.cpp:1121
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:512
to_complex_imag_expr
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1760
simplify_exprt::simplify_function_application
resultt simplify_function_application(const function_application_exprt &)
Attempt to simplify mathematical function applications if we have enough information to do so.
Definition: simplify_expr.cpp:650
simplify_exprt::simplify_pointer_object
resultt simplify_pointer_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:530
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: bitvector_expr.h:278
fixedbv_spect
Definition: fixedbv.h:20
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2234
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2356
update_exprt::designator
exprt::operandst & designator()
Definition: std_expr.h:2382
simplify_exprt::simplify_index
resultt simplify_index(const index_exprt &)
Definition: simplify_expr_array.cpp:20
config
configt config
Definition: config.cpp:24
ieee_floatt::spec
ieee_float_spect spec
Definition: ieee_float.h:134
expr2bits
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
Definition: simplify_utils.cpp:406
fixedbv_typet
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: bitvector_types.h:261
to_binary_overflow_expr
const binary_overflow_exprt & to_binary_overflow_expr(const exprt &expr)
Cast an exprt to a binary_overflow_exprt.
Definition: bitvector_expr.h:741
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
to_ieee_float_op_expr
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: floatbv_expr.h:425
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:44
to_concatenation_expr
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: bitvector_expr.h:618
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:91
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
simplify_exprt::simplify_member
resultt simplify_member(const member_exprt &)
Definition: simplify_expr_struct.cpp:21
expr_util.h
Deprecated expression utility functions.
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:402
unary_overflow_exprt
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Definition: bitvector_expr.h:766
refined_string_exprt::content
const exprt & content() const
Definition: string_expr.h:138
format_expr.h
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:480
simplify_exprt::simplify_object
resultt simplify_object(const exprt &)
Definition: simplify_expr.cpp:1493
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
byte_update_exprt::value
const exprt & value() const
Definition: byte_operators.h:110
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:292
pointer_offset_size
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Definition: pointer_offset_size.cpp:89
array_typet
Arrays with given size.
Definition: std_types.h:757
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2113
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
to_sign_expr
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:531
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2066
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
is_not_zero
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:100
update_exprt::new_value
exprt & new_value()
Definition: std_expr.h:2392
function_application_exprt::function
exprt & function()
Definition: mathematical_expr.h:202
lambda_exprt
A (mathematical) lambda expression.
Definition: mathematical_expr.h:387
simplify_exprt::simplify_sign
resultt simplify_sign(const sign_exprt &)
Definition: simplify_expr.cpp:100
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
get_subexpression_at_offset
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
Definition: pointer_offset_size.cpp:605
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:53
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2103
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
invariant.h
fixedbvt::round
void round(const fixedbv_spect &dest_spec)
Definition: fixedbv.cpp:53
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:195
fixedbvt::spec
fixedbv_spect spec
Definition: fixedbv.h:44
simplify_exprt::simplify_lambda
resultt simplify_lambda(const lambda_exprt &)
Definition: simplify_expr.cpp:1360
config.h
fixedbvt
Definition: fixedbv.h:42
to_extractbits_expr
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: bitvector_expr.h:499
simplify_exprt::simplify_extractbits
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
Definition: simplify_expr_int.cpp:1038
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:244
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
irep_full_eq
Definition: irep.h:506
lambda_exprt::application
exprt application(const operandst &) const
Definition: mathematical_expr.cpp:90
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:699
make_boolean_expr
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:285
ieee_floatt::get_sign
bool get_sign() const
Definition: ieee_float.h:236
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:367
exprt::operands
operandst & operands()
Definition: expr.h:96
simplify_exprt::simplify_byte_update
resultt simplify_byte_update(const byte_update_exprt &)
Definition: simplify_expr.cpp:1746
r
static int8_t r
Definition: irep_hash.h:59
index_exprt
Array index operator.
Definition: std_expr.h:1242
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: bitvector_expr.h:633
s2
int16_t s2
Definition: bytecode_info.h:60
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
true_exprt
The Boolean constant true.
Definition: std_expr.h:2716
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
pointer_offset_sum.h
Pointer Dereferencing.
simplify_exprt::simplify_object_size
resultt simplify_object_size(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:654
simplify_exprt::simplify_abs
resultt simplify_abs(const abs_exprt &)
Definition: simplify_expr.cpp:66
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
simplify_utils.h
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:815
std_expr.h
API to expression classes.
string_expr.h
String expressions for the string solver.
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:723
constant_exprt::set_value
void set_value(const irep_idt &value)
Definition: std_expr.h:2680
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2675
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
with_exprt::where
exprt & where()
Definition: std_expr.h:2192
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:23
byte_update_exprt::op
const exprt & op() const
Definition: byte_operators.h:108
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1381
simplify_exprt::simplify_ieee_float_relation
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
Definition: simplify_expr_floatbv.cpp:339
c_types.h
rationalt
Definition: rational.h:18
to_function_application_expr
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: mathematical_expr.h:244
irep_full_hash
Definition: irep.h:497
complex_exprt::real
exprt real()
Definition: std_expr.h:1632
to_count_leading_zeros_expr
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
Definition: bitvector_expr.h:899
bitvector_expr.h
API to expression classes for bitvectors.
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1605
simplify_exprt::simplify_floatbv_typecast
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
Definition: simplify_expr_floatbv.cpp:140
to_abs_expr
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:370
get_bvrep_bit
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
Definition: arith_tools.cpp:262
count_leading_zeros_exprt
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
Definition: bitvector_expr.h:831
byte_update_exprt::set_offset
void set_offset(exprt e)
Definition: byte_operators.h:99
lower_case_string_expression
static bool lower_case_string_expression(array_exprt &string_data)
Take the passed-in constant string array and lower-case every character.
Definition: simplify_expr.cpp:511
simplify_exprt::simplify_floatbv_op
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
Definition: simplify_expr_floatbv.cpp:274
to_index_designator
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2287
simplify_string_is_empty
static simplify_exprt::resultt simplify_string_is_empty(const function_application_exprt &expr, const namespacet &ns)
Simplify String.isEmpty function when arguments are constant.
Definition: simplify_expr.cpp:252
mathematical_expr.h
API to expression classes for 'mathematical' expressions.
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700
simplify_exprt::simplify_isinf
resultt simplify_isinf(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:24