CBMC
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 "rational.h"
27 #include "rational_tools.h"
28 #include "simplify_utils.h"
29 #include "std_expr.h"
30 #include "string_expr.h"
31 
32 // #define DEBUGX
33 
34 #ifdef DEBUGX
35 #include "format_expr.h"
36 #include <iostream>
37 #endif
38 
39 #include "simplify_expr_class.h"
40 
41 // #define USE_CACHE
42 
43 #ifdef USE_CACHE
44 struct simplify_expr_cachet
45 {
46 public:
47  #if 1
48  typedef std::unordered_map<
49  exprt, exprt, irep_full_hash, irep_full_eq> containert;
50  #else
51  typedef std::unordered_map<exprt, exprt, irep_hash> containert;
52  #endif
53 
54  containert container_normal;
55 
56  containert &container()
57  {
58  return container_normal;
59  }
60 };
61 
62 simplify_expr_cachet simplify_expr_cache;
63 #endif
64 
66 {
67  if(expr.op().is_constant())
68  {
69  const typet &type = to_unary_expr(expr).op().type();
70 
71  if(type.id()==ID_floatbv)
72  {
73  ieee_floatt value(to_constant_expr(to_unary_expr(expr).op()));
74  value.set_sign(false);
75  return value.to_expr();
76  }
77  else if(type.id()==ID_signedbv ||
78  type.id()==ID_unsignedbv)
79  {
80  auto value = numeric_cast<mp_integer>(to_unary_expr(expr).op());
81  if(value.has_value())
82  {
83  if(*value >= 0)
84  {
85  return to_unary_expr(expr).op();
86  }
87  else
88  {
89  value->negate();
90  return from_integer(*value, type);
91  }
92  }
93  }
94  }
95 
96  return unchanged(expr);
97 }
98 
100 {
101  if(expr.op().is_constant())
102  {
103  const typet &type = expr.op().type();
104 
105  if(type.id()==ID_floatbv)
106  {
107  ieee_floatt value(to_constant_expr(expr.op()));
108  return make_boolean_expr(value.get_sign());
109  }
110  else if(type.id()==ID_signedbv ||
111  type.id()==ID_unsignedbv)
112  {
113  const auto value = numeric_cast<mp_integer>(expr.op());
114  if(value.has_value())
115  {
116  return make_boolean_expr(*value >= 0);
117  }
118  }
119  }
120 
121  return unchanged(expr);
122 }
123 
126 {
127  const exprt &op = expr.op();
128 
129  if(op.is_constant())
130  {
131  const typet &op_type = op.type();
132 
133  if(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv)
134  {
135  const auto width = to_bitvector_type(op_type).get_width();
136  const auto &value = to_constant_expr(op).get_value();
137  std::size_t result = 0;
138 
139  for(std::size_t i = 0; i < width; i++)
140  if(get_bvrep_bit(value, width, i))
141  result++;
142 
143  return from_integer(result, expr.type());
144  }
145  }
146 
147  return unchanged(expr);
148 }
149 
152 {
153  const bool is_little_endian =
155 
156  const auto const_bits_opt = expr2bits(expr.op(), is_little_endian, ns);
157 
158  if(!const_bits_opt.has_value())
159  return unchanged(expr);
160 
161  std::size_t n_leading_zeros =
162  is_little_endian ? const_bits_opt->rfind('1') : const_bits_opt->find('1');
163  if(n_leading_zeros == std::string::npos)
164  {
165  if(!expr.zero_permitted())
166  return unchanged(expr);
167 
168  n_leading_zeros = const_bits_opt->size();
169  }
170  else if(is_little_endian)
171  n_leading_zeros = const_bits_opt->size() - n_leading_zeros - 1;
172 
173  return from_integer(n_leading_zeros, expr.type());
174 }
175 
178 {
179  const bool is_little_endian =
181 
182  const auto const_bits_opt = expr2bits(expr.op(), is_little_endian, ns);
183 
184  if(!const_bits_opt.has_value())
185  return unchanged(expr);
186 
187  std::size_t n_trailing_zeros =
188  is_little_endian ? const_bits_opt->find('1') : const_bits_opt->rfind('1');
189  if(n_trailing_zeros == std::string::npos)
190  {
191  if(!expr.zero_permitted())
192  return unchanged(expr);
193 
194  n_trailing_zeros = const_bits_opt->size();
195  }
196  else if(!is_little_endian)
197  n_trailing_zeros = const_bits_opt->size() - n_trailing_zeros - 1;
198 
199  return from_integer(n_trailing_zeros, expr.type());
200 }
201 
204 {
205  const bool is_little_endian =
207 
208  const auto const_bits_opt = expr2bits(expr.op(), is_little_endian, ns);
209 
210  if(!const_bits_opt.has_value())
211  return unchanged(expr);
212 
213  std::size_t first_one_bit =
214  is_little_endian ? const_bits_opt->find('1') : const_bits_opt->rfind('1');
215  if(first_one_bit == std::string::npos)
216  first_one_bit = 0;
217  else if(is_little_endian)
218  ++first_one_bit;
219  else
220  first_one_bit = const_bits_opt->size() - first_one_bit;
221 
222  return from_integer(first_one_bit, expr.type());
223 }
224 
230  const function_application_exprt &expr,
231  const namespacet &ns)
232 {
233  const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
234  const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
235 
236  if(!s1_data_opt)
237  return simplify_exprt::unchanged(expr);
238 
239  const array_exprt &s1_data = s1_data_opt->get();
240  const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1));
241  const auto s2_data_opt = try_get_string_data_array(s2.content(), ns);
242 
243  if(!s2_data_opt)
244  return simplify_exprt::unchanged(expr);
245 
246  const array_exprt &s2_data = s2_data_opt->get();
247  const bool res = s2_data.operands().size() <= s1_data.operands().size() &&
248  std::equal(
249  s2_data.operands().rbegin(),
250  s2_data.operands().rend(),
251  s1_data.operands().rbegin());
252 
253  return from_integer(res ? 1 : 0, expr.type());
254 }
255 
258  const function_application_exprt &expr,
259  const namespacet &ns)
260 {
261  // We want to get both arguments of any starts-with comparison, and
262  // trace them back to the actual string instance. All variables on the
263  // way must be constant for us to be sure this will work.
264  auto &first_argument = to_string_expr(expr.arguments().at(0));
265  auto &second_argument = to_string_expr(expr.arguments().at(1));
266 
267  const auto first_value_opt =
268  try_get_string_data_array(first_argument.content(), ns);
269 
270  if(!first_value_opt)
271  {
272  return simplify_exprt::unchanged(expr);
273  }
274 
275  const array_exprt &first_value = first_value_opt->get();
276 
277  const auto second_value_opt =
278  try_get_string_data_array(second_argument.content(), ns);
279 
280  if(!second_value_opt)
281  {
282  return simplify_exprt::unchanged(expr);
283  }
284 
285  const array_exprt &second_value = second_value_opt->get();
286 
287  // Is our 'contains' array directly contained in our target.
288  const bool includes =
289  std::search(
290  first_value.operands().begin(),
291  first_value.operands().end(),
292  second_value.operands().begin(),
293  second_value.operands().end()) != first_value.operands().end();
294 
295  return from_integer(includes ? 1 : 0, expr.type());
296 }
297 
303  const function_application_exprt &expr,
304  const namespacet &ns)
305 {
306  const function_application_exprt &function_app =
308  const refined_string_exprt &s =
309  to_string_expr(function_app.arguments().at(0));
310 
311  if(!s.length().is_constant())
312  return simplify_exprt::unchanged(expr);
313 
314  const auto numeric_length =
315  numeric_cast_v<mp_integer>(to_constant_expr(s.length()));
316 
317  return from_integer(numeric_length == 0 ? 1 : 0, expr.type());
318 }
319 
328  const function_application_exprt &expr,
329  const namespacet &ns)
330 {
331  const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
332  const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
333 
334  if(!s1_data_opt)
335  return simplify_exprt::unchanged(expr);
336 
337  const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1));
338  const auto s2_data_opt = try_get_string_data_array(s2.content(), ns);
339 
340  if(!s2_data_opt)
341  return simplify_exprt::unchanged(expr);
342 
343  const array_exprt &s1_data = s1_data_opt->get();
344  const array_exprt &s2_data = s2_data_opt->get();
345 
346  if(s1_data.operands() == s2_data.operands())
347  return from_integer(0, expr.type());
348 
349  const mp_integer s1_size = s1_data.operands().size();
350  const mp_integer s2_size = s2_data.operands().size();
351  const bool first_shorter = s1_size < s2_size;
352  const exprt::operandst &ops1 =
353  first_shorter ? s1_data.operands() : s2_data.operands();
354  const exprt::operandst &ops2 =
355  first_shorter ? s2_data.operands() : s1_data.operands();
356  auto it_pair = std::mismatch(ops1.begin(), ops1.end(), ops2.begin());
357 
358  if(it_pair.first == ops1.end())
359  return from_integer(s1_size - s2_size, expr.type());
360 
361  const mp_integer char1 =
362  numeric_cast_v<mp_integer>(to_constant_expr(*it_pair.first));
363  const mp_integer char2 =
364  numeric_cast_v<mp_integer>(to_constant_expr(*it_pair.second));
365 
366  return from_integer(
367  first_shorter ? char1 - char2 : char2 - char1, expr.type());
368 }
369 
377  const function_application_exprt &expr,
378  const namespacet &ns,
379  const bool search_from_end)
380 {
381  std::size_t starting_index = 0;
382 
383  // Determine starting index for the comparison (if given)
384  if(expr.arguments().size() == 3)
385  {
386  auto &starting_index_expr = expr.arguments().at(2);
387 
388  if(!starting_index_expr.is_constant())
389  {
390  return simplify_exprt::unchanged(expr);
391  }
392 
393  const mp_integer idx =
394  numeric_cast_v<mp_integer>(to_constant_expr(starting_index_expr));
395 
396  // Negative indices are treated like 0
397  if(idx > 0)
398  {
399  starting_index = numeric_cast_v<std::size_t>(idx);
400  }
401  }
402 
403  const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
404 
405  const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
406 
407  if(!s1_data_opt)
408  {
409  return simplify_exprt::unchanged(expr);
410  }
411 
412  const array_exprt &s1_data = s1_data_opt->get();
413 
414  const auto search_string_size = s1_data.operands().size();
415  if(starting_index >= search_string_size)
416  {
417  return from_integer(-1, expr.type());
418  }
419 
420  unsigned long starting_offset =
421  starting_index > 0 ? (search_string_size - 1) - starting_index : 0;
423  {
424  // Second argument is a string
425 
426  const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1));
427 
428  const auto s2_data_opt = try_get_string_data_array(s2.content(), ns);
429 
430  if(!s2_data_opt)
431  {
432  return simplify_exprt::unchanged(expr);
433  }
434 
435  const array_exprt &s2_data = s2_data_opt->get();
436 
437  // Searching for empty string is a special case and is simply the
438  // "always found at the first searched position. This needs to take into
439  // account starting position and if you're starting from the beginning or
440  // end.
441  if(s2_data.operands().empty())
442  return from_integer(
443  search_from_end
444  ? starting_index > 0 ? starting_index : search_string_size
445  : 0,
446  expr.type());
447 
448  if(search_from_end)
449  {
450  auto end = std::prev(s1_data.operands().end(), starting_offset);
451  auto it = std::find_end(
452  s1_data.operands().begin(),
453  end,
454  s2_data.operands().begin(),
455  s2_data.operands().end());
456  if(it != end)
457  return from_integer(
458  std::distance(s1_data.operands().begin(), it), expr.type());
459  }
460  else
461  {
462  auto it = std::search(
463  std::next(s1_data.operands().begin(), starting_index),
464  s1_data.operands().end(),
465  s2_data.operands().begin(),
466  s2_data.operands().end());
467 
468  if(it != s1_data.operands().end())
469  return from_integer(
470  std::distance(s1_data.operands().begin(), it), expr.type());
471  }
472  }
473  else if(expr.arguments().at(1).is_constant())
474  {
475  // Second argument is a constant character
476 
477  const constant_exprt &c1 = to_constant_expr(expr.arguments().at(1));
478  const auto c1_val = numeric_cast_v<mp_integer>(c1);
479 
480  auto pred = [&](const exprt &c2) {
481  const auto c2_val = numeric_cast_v<mp_integer>(to_constant_expr(c2));
482 
483  return c1_val == c2_val;
484  };
485 
486  if(search_from_end)
487  {
488  auto it = std::find_if(
489  std::next(s1_data.operands().rbegin(), starting_offset),
490  s1_data.operands().rend(),
491  pred);
492  if(it != s1_data.operands().rend())
493  return from_integer(
494  std::distance(s1_data.operands().begin(), it.base() - 1),
495  expr.type());
496  }
497  else
498  {
499  auto it = std::find_if(
500  std::next(s1_data.operands().begin(), starting_index),
501  s1_data.operands().end(),
502  pred);
503  if(it != s1_data.operands().end())
504  return from_integer(
505  std::distance(s1_data.operands().begin(), it), expr.type());
506  }
507  }
508  else
509  {
510  return simplify_exprt::unchanged(expr);
511  }
512 
513  return from_integer(-1, expr.type());
514 }
515 
522  const function_application_exprt &expr,
523  const namespacet &ns)
524 {
525  if(!expr.arguments().at(1).is_constant())
526  {
527  return simplify_exprt::unchanged(expr);
528  }
529 
530  const auto &index = to_constant_expr(expr.arguments().at(1));
531 
532  const refined_string_exprt &s = to_string_expr(expr.arguments().at(0));
533 
534  const auto char_seq_opt = try_get_string_data_array(s.content(), ns);
535 
536  if(!char_seq_opt)
537  {
538  return simplify_exprt::unchanged(expr);
539  }
540 
541  const array_exprt &char_seq = char_seq_opt->get();
542 
543  const auto i_opt = numeric_cast<std::size_t>(index);
544 
545  if(!i_opt || *i_opt >= char_seq.operands().size())
546  {
547  return simplify_exprt::unchanged(expr);
548  }
549 
550  const auto &c = to_constant_expr(char_seq.operands().at(*i_opt));
551 
552  if(c.type() != expr.type())
553  {
554  return simplify_exprt::unchanged(expr);
555  }
556 
557  return c;
558 }
559 
561 static bool lower_case_string_expression(array_exprt &string_data)
562 {
563  auto &operands = string_data.operands();
564  for(auto &operand : operands)
565  {
566  auto &constant_value = to_constant_expr(operand);
567  auto character = numeric_cast_v<unsigned int>(constant_value);
568 
569  // Can't guarantee matches against non-ASCII characters.
570  if(character >= 128)
571  return false;
572 
573  if(isalpha(character))
574  {
575  if(isupper(character))
576  constant_value =
577  from_integer(tolower(character), constant_value.type());
578  }
579  }
580 
581  return true;
582 }
583 
590  const function_application_exprt &expr,
591  const namespacet &ns)
592 {
593  // We want to get both arguments of any starts-with comparison, and
594  // trace them back to the actual string instance. All variables on the
595  // way must be constant for us to be sure this will work.
596  auto &first_argument = to_string_expr(expr.arguments().at(0));
597  auto &second_argument = to_string_expr(expr.arguments().at(1));
598 
599  const auto first_value_opt =
600  try_get_string_data_array(first_argument.content(), ns);
601 
602  if(!first_value_opt)
603  {
604  return simplify_exprt::unchanged(expr);
605  }
606 
607  array_exprt first_value = first_value_opt->get();
608 
609  const auto second_value_opt =
610  try_get_string_data_array(second_argument.content(), ns);
611 
612  if(!second_value_opt)
613  {
614  return simplify_exprt::unchanged(expr);
615  }
616 
617  array_exprt second_value = second_value_opt->get();
618 
619  // Just lower-case both expressions.
620  if(
621  !lower_case_string_expression(first_value) ||
622  !lower_case_string_expression(second_value))
623  return simplify_exprt::unchanged(expr);
624 
625  bool is_equal = first_value == second_value;
626  return from_integer(is_equal ? 1 : 0, expr.type());
627 }
628 
635  const function_application_exprt &expr,
636  const namespacet &ns)
637 {
638  // We want to get both arguments of any starts-with comparison, and
639  // trace them back to the actual string instance. All variables on the
640  // way must be constant for us to be sure this will work.
641  auto &first_argument = to_string_expr(expr.arguments().at(0));
642  auto &second_argument = to_string_expr(expr.arguments().at(1));
643 
644  const auto first_value_opt =
645  try_get_string_data_array(first_argument.content(), ns);
646 
647  if(!first_value_opt)
648  {
649  return simplify_exprt::unchanged(expr);
650  }
651 
652  const array_exprt &first_value = first_value_opt->get();
653 
654  const auto second_value_opt =
655  try_get_string_data_array(second_argument.content(), ns);
656 
657  if(!second_value_opt)
658  {
659  return simplify_exprt::unchanged(expr);
660  }
661 
662  const array_exprt &second_value = second_value_opt->get();
663 
664  mp_integer offset_int = 0;
665  if(expr.arguments().size() == 3)
666  {
667  auto &offset = expr.arguments()[2];
668  if(!offset.is_constant())
669  return simplify_exprt::unchanged(expr);
670  offset_int = numeric_cast_v<mp_integer>(to_constant_expr(offset));
671  }
672 
673  // test whether second_value is a prefix of first_value
674  bool is_prefix =
675  offset_int >= 0 && mp_integer(first_value.operands().size()) >=
676  offset_int + second_value.operands().size();
677  if(is_prefix)
678  {
679  exprt::operandst::const_iterator second_it =
680  second_value.operands().begin();
681  for(const auto &first_op : first_value.operands())
682  {
683  if(offset_int > 0)
684  --offset_int;
685  else if(second_it == second_value.operands().end())
686  break;
687  else if(first_op != *second_it)
688  {
689  is_prefix = false;
690  break;
691  }
692  else
693  ++second_it;
694  }
695  }
696 
697  return from_integer(is_prefix ? 1 : 0, expr.type());
698 }
699 
701  const function_application_exprt &expr)
702 {
703  if(expr.function().id() == ID_lambda)
704  {
705  // expand the function application
706  return to_lambda_expr(expr.function()).application(expr.arguments());
707  }
708 
709  if(expr.function().id() != ID_symbol)
710  return unchanged(expr);
711 
712  const irep_idt &func_id = to_symbol_expr(expr.function()).get_identifier();
713 
714  // String.startsWith() is used to implement String.equals() in the models
715  // library
716  if(func_id == ID_cprover_string_startswith_func)
717  {
718  return simplify_string_startswith(expr, ns);
719  }
720  else if(func_id == ID_cprover_string_endswith_func)
721  {
722  return simplify_string_endswith(expr, ns);
723  }
724  else if(func_id == ID_cprover_string_is_empty_func)
725  {
726  return simplify_string_is_empty(expr, ns);
727  }
728  else if(func_id == ID_cprover_string_compare_to_func)
729  {
730  return simplify_string_compare_to(expr, ns);
731  }
732  else if(func_id == ID_cprover_string_index_of_func)
733  {
734  return simplify_string_index_of(expr, ns, false);
735  }
736  else if(func_id == ID_cprover_string_char_at_func)
737  {
738  return simplify_string_char_at(expr, ns);
739  }
740  else if(func_id == ID_cprover_string_contains_func)
741  {
742  return simplify_string_contains(expr, ns);
743  }
744  else if(func_id == ID_cprover_string_last_index_of_func)
745  {
746  return simplify_string_index_of(expr, ns, true);
747  }
748  else if(func_id == ID_cprover_string_equals_ignore_case_func)
749  {
751  }
752 
753  return unchanged(expr);
754 }
755 
758 {
759  const typet &expr_type = expr.type();
760  const typet &op_type = expr.op().type();
761 
762  // eliminate casts of infinity
763  if(expr.op().id() == ID_infinity)
764  {
765  typet new_type=expr.type();
766  exprt tmp = expr.op();
767  tmp.type()=new_type;
768  return std::move(tmp);
769  }
770 
771  // casts from NULL to any integer
772  if(
773  op_type.id() == ID_pointer && expr.op().is_constant() &&
774  to_constant_expr(expr.op()).get_value() == ID_NULL &&
775  (expr_type.id() == ID_unsignedbv || expr_type.id() == ID_signedbv) &&
777  {
778  return from_integer(0, expr_type);
779  }
780 
781  // casts from pointer to integer
782  // where width of integer >= width of pointer
783  // (void*)(intX)expr -> (void*)expr
784  if(
785  expr_type.id() == ID_pointer && expr.op().id() == ID_typecast &&
786  (op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv ||
787  op_type.id() == ID_bv) &&
788  to_bitvector_type(op_type).get_width() >=
789  to_bitvector_type(expr_type).get_width())
790  {
791  auto new_expr = expr;
792  new_expr.op() = to_typecast_expr(expr.op()).op();
793  return changed(simplify_typecast(new_expr)); // rec. call
794  }
795 
796  // eliminate redundant typecasts
797  if(expr.type() == expr.op().type())
798  {
799  return expr.op();
800  }
801 
802  // eliminate casts to proper bool
803  if(expr_type.id()==ID_bool)
804  {
805  // rewrite (bool)x to x!=0
806  binary_relation_exprt inequality(
807  expr.op(),
808  op_type.id() == ID_floatbv ? ID_ieee_float_notequal : ID_notequal,
809  from_integer(0, op_type));
810  inequality.add_source_location()=expr.source_location();
811  return changed(simplify_node(inequality));
812  }
813 
814  // eliminate casts from proper bool
815  if(
816  op_type.id() == ID_bool &&
817  (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv ||
818  expr_type.id() == ID_c_bool || expr_type.id() == ID_c_bit_field))
819  {
820  // rewrite (T)(bool) to bool?1:0
821  auto one = from_integer(1, expr_type);
822  auto zero = from_integer(0, expr_type);
824  if_exprt{expr.op(), std::move(one), std::move(zero)}));
825  }
826 
827  // circular casts through types shorter than `int`
828  // we use fixed bit widths as this is specifically for the Java bytecode
829  // front-end
830  if(op_type == signedbv_typet(32) && expr.op().id() == ID_typecast)
831  {
832  if(expr_type==c_bool_typet(8) ||
833  expr_type==signedbv_typet(8) ||
834  expr_type==signedbv_typet(16) ||
835  expr_type==unsignedbv_typet(16))
836  {
837  // We checked that the id was ID_typecast in the enclosing `if`
838  const auto &typecast = expr_checked_cast<typecast_exprt>(expr.op());
839  if(typecast.op().type()==expr_type)
840  {
841  return typecast.op();
842  }
843  }
844  }
845 
846  // eliminate casts to _Bool
847  if(expr_type.id()==ID_c_bool &&
848  op_type.id()!=ID_bool)
849  {
850  // rewrite (_Bool)x to (_Bool)(x!=0)
851  exprt inequality = is_not_zero(expr.op(), ns);
852  auto new_expr = expr;
853  new_expr.op() = simplify_node(std::move(inequality));
854  return changed(simplify_typecast(new_expr)); // recursive call
855  }
856 
857  // eliminate typecasts from NULL
858  if(
859  expr_type.id() == ID_pointer && expr.op().is_constant() &&
860  (to_constant_expr(expr.op()).get_value() == ID_NULL ||
861  (expr.op().is_zero() && config.ansi_c.NULL_is_zero)))
862  {
863  exprt tmp = expr.op();
864  tmp.type()=expr.type();
865  to_constant_expr(tmp).set_value(ID_NULL);
866  return std::move(tmp);
867  }
868 
869  // eliminate duplicate pointer typecasts
870  // (T1 *)(T2 *)x -> (T1 *)x
871  if(
872  expr_type.id() == ID_pointer && expr.op().id() == ID_typecast &&
873  op_type.id() == ID_pointer)
874  {
875  auto new_expr = expr;
876  new_expr.op() = to_typecast_expr(expr.op()).op();
877  return changed(simplify_typecast(new_expr)); // recursive call
878  }
879 
880  // casts from integer to pointer and back:
881  // (int)(void *)int -> (int)(size_t)int
882  if(
883  (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv) &&
884  expr.op().id() == ID_typecast && expr.op().operands().size() == 1 &&
885  op_type.id() == ID_pointer)
886  {
887  auto inner_cast = to_typecast_expr(expr.op());
888  inner_cast.type() = size_type();
889 
890  auto outer_cast = expr;
891  outer_cast.op() = simplify_typecast(inner_cast); // rec. call
892  return changed(simplify_typecast(outer_cast)); // rec. call
893  }
894 
895  // mildly more elaborate version of the above:
896  // (int)((T*)0 + int) -> (int)(sizeof(T)*(size_t)int) if NULL is zero
897  if(
899  (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv) &&
900  op_type.id() == ID_pointer && expr.op().id() == ID_plus &&
901  expr.op().operands().size() == 2)
902  {
903  const auto &op_plus_expr = to_plus_expr(expr.op());
904 
905  if(
906  (op_plus_expr.op0().id() == ID_typecast &&
907  to_typecast_expr(op_plus_expr.op0()).op().is_zero()) ||
908  (op_plus_expr.op0().is_constant() &&
909  is_null_pointer(to_constant_expr(op_plus_expr.op0()))))
910  {
911  auto sub_size =
912  pointer_offset_size(to_pointer_type(op_type).base_type(), ns);
913  if(sub_size.has_value())
914  {
915  auto new_expr = expr;
916  exprt offset_expr =
917  simplify_typecast(typecast_exprt(op_plus_expr.op1(), size_type()));
918 
919  // void*
920  if(*sub_size == 0 || *sub_size == 1)
921  new_expr.op() = offset_expr;
922  else
923  {
924  new_expr.op() = simplify_mult(
925  mult_exprt(from_integer(*sub_size, size_type()), offset_expr));
926  }
927 
928  return changed(simplify_typecast(new_expr)); // rec. call
929  }
930  }
931  }
932 
933  // Push a numerical typecast into various integer operations, i.e.,
934  // (T)(x OP y) ---> (T)x OP (T)y
935  //
936  // Doesn't work for many, e.g., pointer difference, floating-point,
937  // division, modulo.
938  // Many operations fail if the width of T
939  // is bigger than that of (x OP y). This includes ID_bitnot and
940  // anything that might overflow, e.g., ID_plus.
941  //
942  if((expr_type.id()==ID_signedbv || expr_type.id()==ID_unsignedbv) &&
943  (op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv))
944  {
945  bool enlarge=
946  to_bitvector_type(expr_type).get_width()>
947  to_bitvector_type(op_type).get_width();
948 
949  if(!enlarge)
950  {
951  irep_idt op_id = expr.op().id();
952 
953  if(op_id==ID_plus || op_id==ID_minus || op_id==ID_mult ||
954  op_id==ID_unary_minus ||
955  op_id==ID_bitxor || op_id==ID_bitor || op_id==ID_bitand)
956  {
957  exprt result = expr.op();
958 
959  if(
960  result.operands().size() >= 1 &&
961  to_multi_ary_expr(result).op0().type() == result.type())
962  {
963  result.type()=expr.type();
964 
965  Forall_operands(it, result)
966  {
967  auto new_operand = typecast_exprt(*it, expr.type());
968  *it = simplify_typecast(new_operand); // recursive call
969  }
970 
971  return changed(simplify_node(result)); // possibly recursive call
972  }
973  }
974  else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
975  {
976  }
977  }
978  }
979 
980  // Push a numerical typecast into pointer arithmetic
981  // (T)(ptr + int) ---> (T)((size_t)ptr + sizeof(subtype)*(size_t)int)
982  //
983  if(
984  (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv) &&
985  op_type.id() == ID_pointer && expr.op().id() == ID_plus)
986  {
987  const auto step =
988  pointer_offset_size(to_pointer_type(op_type).base_type(), ns);
989 
990  if(step.has_value() && *step != 0)
991  {
992  const typet size_t_type(size_type());
993  auto new_expr = expr;
994 
995  new_expr.op().type() = size_t_type;
996 
997  for(auto &op : new_expr.op().operands())
998  {
999  exprt new_op = simplify_typecast(typecast_exprt(op, size_t_type));
1000  if(op.type().id() != ID_pointer && *step > 1)
1001  {
1002  new_op =
1003  simplify_mult(mult_exprt(from_integer(*step, size_t_type), new_op));
1004  }
1005  op = std::move(new_op);
1006  }
1007 
1008  new_expr.op() = simplify_plus(to_plus_expr(new_expr.op()));
1009 
1010  return changed(simplify_typecast(new_expr)); // recursive call
1011  }
1012  }
1013 
1014  const irep_idt &expr_type_id=expr_type.id();
1015  const exprt &operand = expr.op();
1016  const irep_idt &op_type_id=op_type.id();
1017 
1018  if(operand.is_constant())
1019  {
1020  const irep_idt &value=to_constant_expr(operand).get_value();
1021 
1022  // preserve the sizeof type annotation
1023  typet c_sizeof_type=
1024  static_cast<const typet &>(operand.find(ID_C_c_sizeof_type));
1025 
1026  if(op_type_id==ID_integer ||
1027  op_type_id==ID_natural)
1028  {
1029  // from integer to ...
1030 
1031  mp_integer int_value=string2integer(id2string(value));
1032 
1033  if(expr_type_id==ID_bool)
1034  {
1035  return make_boolean_expr(int_value != 0);
1036  }
1037 
1038  if(expr_type_id==ID_unsignedbv ||
1039  expr_type_id==ID_signedbv ||
1040  expr_type_id==ID_c_enum ||
1041  expr_type_id==ID_c_bit_field ||
1042  expr_type_id==ID_integer)
1043  {
1044  return from_integer(int_value, expr_type);
1045  }
1046  else if(expr_type_id == ID_c_enum_tag)
1047  {
1048  const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
1049  if(!c_enum_type.is_incomplete()) // possibly incomplete
1050  {
1051  exprt tmp = from_integer(int_value, c_enum_type);
1052  tmp.type() = expr_type; // we maintain the tag type
1053  return std::move(tmp);
1054  }
1055  }
1056  }
1057  else if(op_type_id==ID_rational)
1058  {
1059  }
1060  else if(op_type_id==ID_real)
1061  {
1062  }
1063  else if(op_type_id==ID_bool)
1064  {
1065  if(expr_type_id==ID_unsignedbv ||
1066  expr_type_id==ID_signedbv ||
1067  expr_type_id==ID_integer ||
1068  expr_type_id==ID_natural ||
1069  expr_type_id==ID_rational ||
1070  expr_type_id==ID_c_bool ||
1071  expr_type_id==ID_c_enum ||
1072  expr_type_id==ID_c_bit_field)
1073  {
1074  if(operand.is_true())
1075  {
1076  return from_integer(1, expr_type);
1077  }
1078  else if(operand.is_false())
1079  {
1080  return from_integer(0, expr_type);
1081  }
1082  }
1083  else if(expr_type_id==ID_c_enum_tag)
1084  {
1085  const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
1086  if(!c_enum_type.is_incomplete()) // possibly incomplete
1087  {
1088  unsigned int_value = operand.is_true() ? 1u : 0u;
1089  exprt tmp=from_integer(int_value, c_enum_type);
1090  tmp.type()=expr_type; // we maintain the tag type
1091  return std::move(tmp);
1092  }
1093  }
1094  else if(expr_type_id==ID_pointer &&
1095  operand.is_false() &&
1097  {
1098  return null_pointer_exprt(to_pointer_type(expr_type));
1099  }
1100  }
1101  else if(op_type_id==ID_unsignedbv ||
1102  op_type_id==ID_signedbv ||
1103  op_type_id==ID_c_bit_field ||
1104  op_type_id==ID_c_bool)
1105  {
1106  mp_integer int_value;
1107 
1108  if(to_integer(to_constant_expr(operand), int_value))
1109  return unchanged(expr);
1110 
1111  if(expr_type_id==ID_bool)
1112  {
1113  return make_boolean_expr(int_value != 0);
1114  }
1115 
1116  if(expr_type_id==ID_c_bool)
1117  {
1118  return from_integer(int_value != 0, expr_type);
1119  }
1120 
1121  if(expr_type_id==ID_integer)
1122  {
1123  return from_integer(int_value, expr_type);
1124  }
1125 
1126  if(expr_type_id==ID_natural)
1127  {
1128  if(int_value>=0)
1129  {
1130  return from_integer(int_value, expr_type);
1131  }
1132  }
1133 
1134  if(expr_type_id==ID_unsignedbv ||
1135  expr_type_id==ID_signedbv ||
1136  expr_type_id==ID_bv ||
1137  expr_type_id==ID_c_bit_field)
1138  {
1139  auto result = from_integer(int_value, expr_type);
1140 
1141  if(c_sizeof_type.is_not_nil())
1142  result.set(ID_C_c_sizeof_type, c_sizeof_type);
1143 
1144  return std::move(result);
1145  }
1146 
1147  if(expr_type_id==ID_c_enum_tag)
1148  {
1149  const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
1150  if(!c_enum_type.is_incomplete()) // possibly incomplete
1151  {
1152  exprt tmp=from_integer(int_value, c_enum_type);
1153  tmp.type()=expr_type; // we maintain the tag type
1154  return std::move(tmp);
1155  }
1156  }
1157 
1158  if(expr_type_id==ID_c_enum)
1159  {
1160  return from_integer(int_value, expr_type);
1161  }
1162 
1163  if(expr_type_id==ID_fixedbv)
1164  {
1165  // int to float
1166  const fixedbv_typet &f_expr_type=
1167  to_fixedbv_type(expr_type);
1168 
1169  fixedbvt f;
1170  f.spec=fixedbv_spect(f_expr_type);
1171  f.from_integer(int_value);
1172  return f.to_expr();
1173  }
1174 
1175  if(expr_type_id==ID_floatbv)
1176  {
1177  // int to float
1178  const floatbv_typet &f_expr_type=
1179  to_floatbv_type(expr_type);
1180 
1181  ieee_floatt f(f_expr_type);
1182  f.from_integer(int_value);
1183 
1184  return f.to_expr();
1185  }
1186 
1187  if(expr_type_id==ID_rational)
1188  {
1189  rationalt r(int_value);
1190  return from_rational(r);
1191  }
1192  }
1193  else if(op_type_id==ID_fixedbv)
1194  {
1195  if(expr_type_id==ID_unsignedbv ||
1196  expr_type_id==ID_signedbv)
1197  {
1198  // cast from fixedbv to int
1199  fixedbvt f(to_constant_expr(expr.op()));
1200  return from_integer(f.to_integer(), expr_type);
1201  }
1202  else if(expr_type_id==ID_fixedbv)
1203  {
1204  // fixedbv to fixedbv
1205  fixedbvt f(to_constant_expr(expr.op()));
1206  f.round(fixedbv_spect(to_fixedbv_type(expr_type)));
1207  return f.to_expr();
1208  }
1209  else if(expr_type_id == ID_bv)
1210  {
1211  fixedbvt f{to_constant_expr(expr.op())};
1212  return from_integer(f.get_value(), expr_type);
1213  }
1214  }
1215  else if(op_type_id==ID_floatbv)
1216  {
1217  ieee_floatt f(to_constant_expr(expr.op()));
1218 
1219  if(expr_type_id==ID_unsignedbv ||
1220  expr_type_id==ID_signedbv)
1221  {
1222  // cast from float to int
1223  return from_integer(f.to_integer(), expr_type);
1224  }
1225  else if(expr_type_id==ID_floatbv)
1226  {
1227  // float to double or double to float
1229  return f.to_expr();
1230  }
1231  else if(expr_type_id==ID_fixedbv)
1232  {
1233  fixedbvt fixedbv;
1234  fixedbv.spec=fixedbv_spect(to_fixedbv_type(expr_type));
1235  ieee_floatt factor(f.spec);
1236  factor.from_integer(power(2, fixedbv.spec.get_fraction_bits()));
1237  f*=factor;
1238  fixedbv.set_value(f.to_integer());
1239  return fixedbv.to_expr();
1240  }
1241  else if(expr_type_id == ID_bv)
1242  {
1243  return from_integer(f.pack(), expr_type);
1244  }
1245  }
1246  else if(op_type_id==ID_bv)
1247  {
1248  if(
1249  expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1250  expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1251  expr_type_id == ID_c_bit_field)
1252  {
1253  const auto width = to_bv_type(op_type).get_width();
1254  const auto int_value = bvrep2integer(value, width, false);
1255  if(expr_type_id != ID_c_enum_tag)
1256  return from_integer(int_value, expr_type);
1257  else
1258  {
1259  c_enum_tag_typet tag_type = to_c_enum_tag_type(expr_type);
1260  auto result = from_integer(int_value, ns.follow_tag(tag_type));
1261  result.type() = tag_type;
1262  return std::move(result);
1263  }
1264  }
1265  else if(expr_type_id == ID_floatbv)
1266  {
1267  const auto width = to_bv_type(op_type).get_width();
1268  const auto int_value = bvrep2integer(value, width, false);
1269  ieee_floatt ieee_float{to_floatbv_type(expr_type)};
1270  ieee_float.unpack(int_value);
1271  return ieee_float.to_expr();
1272  }
1273  else if(expr_type_id == ID_fixedbv)
1274  {
1275  const auto width = to_bv_type(op_type).get_width();
1276  const auto int_value = bvrep2integer(value, width, false);
1277  fixedbvt fixedbv{fixedbv_spect{to_fixedbv_type(expr_type)}};
1278  fixedbv.set_value(int_value);
1279  return fixedbv.to_expr();
1280  }
1281  }
1282  else if(op_type_id==ID_c_enum_tag) // enum to int
1283  {
1284  const typet &base_type =
1285  ns.follow_tag(to_c_enum_tag_type(op_type)).underlying_type();
1286  if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv)
1287  {
1288  // enum constants use the representation of their base type
1289  auto new_expr = expr;
1290  new_expr.op().type() = base_type;
1291  return changed(simplify_typecast(new_expr)); // recursive call
1292  }
1293  }
1294  else if(op_type_id==ID_c_enum) // enum to int
1295  {
1296  const typet &base_type = to_c_enum_type(op_type).underlying_type();
1297  if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv)
1298  {
1299  // enum constants use the representation of their base type
1300  auto new_expr = expr;
1301  new_expr.op().type() = base_type;
1302  return changed(simplify_typecast(new_expr)); // recursive call
1303  }
1304  }
1305  }
1306  else if(operand.id()==ID_typecast) // typecast of typecast
1307  {
1308  // (T1)(T2)x ---> (T1)
1309  // where T1 has fewer bits than T2
1310  if(
1311  op_type_id == expr_type_id &&
1312  (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1313  expr_type_id == ID_bv) &&
1314  to_bitvector_type(expr_type).get_width() <=
1315  to_bitvector_type(operand.type()).get_width())
1316  {
1317  auto new_expr = expr;
1318  new_expr.op() = to_typecast_expr(operand).op();
1319  // might enable further simplification
1320  return changed(simplify_typecast(new_expr)); // recursive call
1321  }
1322  }
1323  else if(operand.id()==ID_address_of)
1324  {
1325  const exprt &o=to_address_of_expr(operand).object();
1326 
1327  // turn &array into &array[0] when casting to pointer-to-element-type
1328  if(
1329  o.type().id() == ID_array &&
1330  expr_type == pointer_type(to_array_type(o.type()).element_type()))
1331  {
1332  auto result =
1334 
1335  return changed(simplify_address_of(result)); // recursive call
1336  }
1337  }
1338 
1339  return unchanged(expr);
1340 }
1341 
1344 {
1345  const typet &expr_type = expr.type();
1346  const typet &op_type = expr.op().type();
1347 
1348  // (T)(a?b:c) --> a?(T)b:(T)c; don't do this for floating-point type casts as
1349  // the type cast itself may be costly
1350  if(
1351  expr.op().id() == ID_if && expr_type.id() != ID_floatbv &&
1352  op_type.id() != ID_floatbv)
1353  {
1354  if_exprt if_expr = lift_if(expr, 0);
1355  return changed(simplify_if_preorder(if_expr));
1356  }
1357  else
1358  {
1359  auto r_it = simplify_rec(expr.op()); // recursive call
1360  if(r_it.has_changed())
1361  {
1362  auto tmp = expr;
1363  tmp.op() = r_it.expr;
1364  return tmp;
1365  }
1366  }
1367 
1368  return unchanged(expr);
1369 }
1370 
1373 {
1374  const exprt &pointer = expr.pointer();
1375 
1376  if(pointer.type().id()!=ID_pointer)
1377  return unchanged(expr);
1378 
1379  if(pointer.id()==ID_address_of)
1380  {
1381  exprt tmp=to_address_of_expr(pointer).object();
1382  // one address_of is gone, try again
1383  return changed(simplify_rec(tmp));
1384  }
1385  // rewrite *(&a[0] + x) to a[x]
1386  else if(
1387  pointer.id() == ID_plus && pointer.operands().size() == 2 &&
1388  to_plus_expr(pointer).op0().id() == ID_address_of)
1389  {
1390  const auto &pointer_plus_expr = to_plus_expr(pointer);
1391 
1392  const address_of_exprt &address_of =
1393  to_address_of_expr(pointer_plus_expr.op0());
1394 
1395  if(address_of.object().id()==ID_index)
1396  {
1397  const index_exprt &old=to_index_expr(address_of.object());
1398  if(old.array().type().id() == ID_array)
1399  {
1400  index_exprt idx(
1401  old.array(),
1402  pointer_offset_sum(old.index(), pointer_plus_expr.op1()),
1403  to_array_type(old.array().type()).element_type());
1404  return changed(simplify_rec(idx));
1405  }
1406  }
1407  }
1408 
1409  return unchanged(expr);
1410 }
1411 
1414 {
1415  const exprt &pointer = expr.pointer();
1416 
1417  if(pointer.id() == ID_if)
1418  {
1419  if_exprt if_expr = lift_if(expr, 0);
1420  return changed(simplify_if_preorder(if_expr));
1421  }
1422  else
1423  {
1424  auto r_it = simplify_rec(pointer); // recursive call
1425  if(r_it.has_changed())
1426  {
1427  auto tmp = expr;
1428  tmp.pointer() = r_it.expr;
1429  return tmp;
1430  }
1431  }
1432 
1433  return unchanged(expr);
1434 }
1435 
1438 {
1439  return unchanged(expr);
1440 }
1441 
1443 {
1444  bool no_change = true;
1445 
1446  if((expr.operands().size()%2)!=1)
1447  return unchanged(expr);
1448 
1449  // copy
1450  auto with_expr = expr;
1451 
1452  const typet old_type_followed = ns.follow(with_expr.old().type());
1453 
1454  // now look at first operand
1455 
1456  if(old_type_followed.id() == ID_struct)
1457  {
1458  if(with_expr.old().id() == ID_struct || with_expr.old().is_constant())
1459  {
1460  while(with_expr.operands().size() > 1)
1461  {
1462  const irep_idt &component_name =
1463  with_expr.where().get(ID_component_name);
1464 
1465  if(!to_struct_type(old_type_followed).has_component(component_name))
1466  return unchanged(expr);
1467 
1468  std::size_t number =
1469  to_struct_type(old_type_followed).component_number(component_name);
1470 
1471  if(number >= with_expr.old().operands().size())
1472  return unchanged(expr);
1473 
1474  with_expr.old().operands()[number].swap(with_expr.new_value());
1475 
1476  with_expr.operands().erase(++with_expr.operands().begin());
1477  with_expr.operands().erase(++with_expr.operands().begin());
1478 
1479  no_change = false;
1480  }
1481  }
1482  }
1483  else if(
1484  with_expr.old().type().id() == ID_array ||
1485  with_expr.old().type().id() == ID_vector)
1486  {
1487  if(
1488  with_expr.old().id() == ID_array || with_expr.old().is_constant() ||
1489  with_expr.old().id() == ID_vector)
1490  {
1491  while(with_expr.operands().size() > 1)
1492  {
1493  const auto i = numeric_cast<mp_integer>(with_expr.where());
1494 
1495  if(!i.has_value())
1496  break;
1497 
1498  if(*i < 0 || *i >= with_expr.old().operands().size())
1499  break;
1500 
1501  with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
1502  with_expr.new_value());
1503 
1504  with_expr.operands().erase(++with_expr.operands().begin());
1505  with_expr.operands().erase(++with_expr.operands().begin());
1506 
1507  no_change = false;
1508  }
1509  }
1510  }
1511 
1512  if(with_expr.operands().size() == 1)
1513  return with_expr.old();
1514 
1515  if(no_change)
1516  return unchanged(expr);
1517  else
1518  return std::move(with_expr);
1519 }
1520 
1523 {
1524  // this is to push updates into (possibly nested) constants
1525 
1526  const exprt::operandst &designator = expr.designator();
1527 
1528  exprt updated_value = expr.old();
1529  exprt *value_ptr=&updated_value;
1530 
1531  for(const auto &e : designator)
1532  {
1533  const typet &value_ptr_type=ns.follow(value_ptr->type());
1534 
1535  if(e.id()==ID_index_designator &&
1536  value_ptr->id()==ID_array)
1537  {
1538  const auto i = numeric_cast<mp_integer>(to_index_designator(e).index());
1539 
1540  if(!i.has_value())
1541  return unchanged(expr);
1542 
1543  if(*i < 0 || *i >= value_ptr->operands().size())
1544  return unchanged(expr);
1545 
1546  value_ptr = &value_ptr->operands()[numeric_cast_v<std::size_t>(*i)];
1547  }
1548  else if(e.id()==ID_member_designator &&
1549  value_ptr->id()==ID_struct)
1550  {
1551  const irep_idt &component_name=
1552  e.get(ID_component_name);
1553  const struct_typet &value_ptr_struct_type =
1554  to_struct_type(value_ptr_type);
1555  if(!value_ptr_struct_type.has_component(component_name))
1556  return unchanged(expr);
1557  auto &designator_as_struct_expr = to_struct_expr(*value_ptr);
1558  value_ptr = &designator_as_struct_expr.component(component_name, ns);
1559  CHECK_RETURN(value_ptr->is_not_nil());
1560  }
1561  else
1562  return unchanged(expr); // give up, unknown designator
1563  }
1564 
1565  // found, done
1566  *value_ptr = expr.new_value();
1567  return updated_value;
1568 }
1569 
1571 {
1572  if(expr.id()==ID_plus)
1573  {
1574  if(expr.type().id()==ID_pointer)
1575  {
1576  // kill integers from sum
1577  for(auto &op : expr.operands())
1578  if(op.type().id() == ID_pointer)
1579  return changed(simplify_object(op)); // recursive call
1580  }
1581  }
1582  else if(expr.id()==ID_typecast)
1583  {
1584  auto const &typecast_expr = to_typecast_expr(expr);
1585  const typet &op_type = typecast_expr.op().type();
1586 
1587  if(op_type.id()==ID_pointer)
1588  {
1589  // cast from pointer to pointer
1590  return changed(simplify_object(typecast_expr.op())); // recursive call
1591  }
1592  else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
1593  {
1594  // cast from integer to pointer
1595 
1596  // We do a bit of special treatment for (TYPE *)(a+(int)&o) and
1597  // (TYPE *)(a+(int)((T*)&o+x)), which are re-written to '&o'.
1598 
1599  const exprt &casted_expr = typecast_expr.op();
1600  if(casted_expr.id() == ID_plus && casted_expr.operands().size() == 2)
1601  {
1602  const auto &plus_expr = to_plus_expr(casted_expr);
1603 
1604  const exprt &cand = plus_expr.op0().id() == ID_typecast
1605  ? plus_expr.op0()
1606  : plus_expr.op1();
1607 
1608  if(cand.id() == ID_typecast)
1609  {
1610  const auto &typecast_op = to_typecast_expr(cand).op();
1611 
1612  if(typecast_op.id() == ID_address_of)
1613  {
1614  return typecast_op;
1615  }
1616  else if(
1617  typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1618  to_plus_expr(typecast_op).op0().id() == ID_typecast &&
1619  to_typecast_expr(to_plus_expr(typecast_op).op0()).op().id() ==
1620  ID_address_of)
1621  {
1622  return to_typecast_expr(to_plus_expr(typecast_op).op0()).op();
1623  }
1624  }
1625  }
1626  }
1627  }
1628  else if(expr.id()==ID_address_of)
1629  {
1630  const auto &object = to_address_of_expr(expr).object();
1631 
1632  if(object.id() == ID_index)
1633  {
1634  // &some[i] -> &some
1635  address_of_exprt new_expr(to_index_expr(object).array());
1636  return changed(simplify_object(new_expr)); // recursion
1637  }
1638  else if(object.id() == ID_member)
1639  {
1640  // &some.f -> &some
1641  address_of_exprt new_expr(to_member_expr(object).compound());
1642  return changed(simplify_object(new_expr)); // recursion
1643  }
1644  }
1645 
1646  return unchanged(expr);
1647 }
1648 
1651 {
1652  // lift up any ID_if on the object
1653  if(expr.op().id() == ID_if)
1654  {
1655  if_exprt if_expr = lift_if(expr, 0);
1656  if_expr.true_case() =
1658  if_expr.false_case() =
1660  return changed(simplify_if(if_expr));
1661  }
1662 
1663  const auto el_size = pointer_offset_bits(expr.type(), ns);
1664  if(el_size.has_value() && *el_size < 0)
1665  return unchanged(expr);
1666 
1667  // byte_extract(byte_extract(root, offset1), offset2) =>
1668  // byte_extract(root, offset1+offset2)
1669  if(expr.op().id()==expr.id())
1670  {
1671  auto tmp = expr;
1672 
1673  tmp.offset() = simplify_rec(plus_exprt(
1675  to_byte_extract_expr(expr.op()).offset(), expr.offset().type()),
1676  expr.offset()));
1677  tmp.op() = to_byte_extract_expr(expr.op()).op();
1678 
1679  return changed(simplify_byte_extract(tmp)); // recursive call
1680  }
1681 
1682  // byte_extract(byte_update(root, offset, value), offset) =>
1683  // value
1684  if(
1685  ((expr.id() == ID_byte_extract_big_endian &&
1686  expr.op().id() == ID_byte_update_big_endian) ||
1687  (expr.id() == ID_byte_extract_little_endian &&
1688  expr.op().id() == ID_byte_update_little_endian)) &&
1689  expr.offset() == to_byte_update_expr(as_const(expr).op()).offset())
1690  {
1691  const auto &op_byte_update = to_byte_update_expr(expr.op());
1692 
1693  if(expr.type() == op_byte_update.value().type())
1694  {
1695  return op_byte_update.value();
1696  }
1697  else if(el_size.has_value())
1698  {
1699  const auto update_bits_opt =
1700  pointer_offset_bits(op_byte_update.value().type(), ns);
1701 
1702  if(update_bits_opt.has_value() && *el_size <= *update_bits_opt)
1703  {
1704  auto tmp = expr;
1705  tmp.op() = op_byte_update.value();
1706  tmp.offset() = from_integer(0, expr.offset().type());
1707 
1708  return changed(simplify_byte_extract(tmp)); // recursive call
1709  }
1710  }
1711  }
1712 
1713  // the following require a constant offset
1714  auto offset = numeric_cast<mp_integer>(expr.offset());
1715  if(!offset.has_value() || *offset < 0)
1716  return unchanged(expr);
1717 
1718  // try to simplify byte_extract(byte_update(...))
1719  auto const bu = expr_try_dynamic_cast<byte_update_exprt>(expr.op());
1720  std::optional<mp_integer> update_offset;
1721  if(bu)
1722  update_offset = numeric_cast<mp_integer>(bu->offset());
1723  if(bu && el_size.has_value() && update_offset.has_value())
1724  {
1725  // byte_extract(byte_update(root, offset_u, value), offset_e) so that the
1726  // update does not affect what is being extracted simplifies to
1727  // byte_extract(root, offset_e)
1728  //
1729  // byte_extract(byte_update(root, offset_u, value), offset_e) so that the
1730  // extracted range fully lies within the update value simplifies to
1731  // byte_extract(value, offset_e - offset_u)
1732  if(
1733  *offset * expr.get_bits_per_byte() + *el_size <=
1734  *update_offset * bu->get_bits_per_byte())
1735  {
1736  // extracting before the update
1737  auto tmp = expr;
1738  tmp.op() = bu->op();
1739  return changed(simplify_byte_extract(tmp)); // recursive call
1740  }
1741  else if(
1742  const auto update_size = pointer_offset_bits(bu->value().type(), ns))
1743  {
1744  if(
1745  *offset * expr.get_bits_per_byte() >=
1746  *update_offset * bu->get_bits_per_byte() + *update_size)
1747  {
1748  // extracting after the update
1749  auto tmp = expr;
1750  tmp.op() = bu->op();
1751  return changed(simplify_byte_extract(tmp)); // recursive call
1752  }
1753  else if(
1754  *offset >= *update_offset &&
1755  *offset * expr.get_bits_per_byte() + *el_size <=
1756  *update_offset * bu->get_bits_per_byte() + *update_size)
1757  {
1758  // extracting from the update
1759  auto tmp = expr;
1760  tmp.op() = bu->value();
1761  tmp.offset() =
1762  from_integer(*offset - *update_offset, expr.offset().type());
1763  return changed(simplify_byte_extract(tmp)); // recursive call
1764  }
1765  }
1766  }
1767 
1768  // don't do any of the following if endianness doesn't match, as
1769  // bytes need to be swapped
1770  if(
1771  *offset == 0 && ((expr.id() == ID_byte_extract_little_endian &&
1774  (expr.id() == ID_byte_extract_big_endian &&
1777  {
1778  // byte extract of full object is object
1779  if(expr.type() == expr.op().type())
1780  {
1781  return expr.op();
1782  }
1783  else if(
1784  expr.type().id() == ID_pointer && expr.op().type().id() == ID_pointer)
1785  {
1786  return typecast_exprt(expr.op(), expr.type());
1787  }
1788  }
1789 
1790  if(
1791  (expr.type().id() == ID_union || expr.type().id() == ID_union_tag) &&
1792  to_union_type(ns.follow(expr.type())).components().empty())
1793  {
1794  return empty_union_exprt{expr.type()};
1795  }
1796  else if(
1797  (expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag) &&
1798  to_struct_type(ns.follow(expr.type())).components().empty())
1799  {
1800  return struct_exprt{{}, expr.type()};
1801  }
1802 
1803  // no proper simplification for expr.type()==void
1804  // or types of unknown size
1805  if(!el_size.has_value() || *el_size == 0)
1806  return unchanged(expr);
1807 
1808  if(
1809  expr.op().id() == ID_array_of &&
1810  to_array_of_expr(expr.op()).op().is_constant())
1811  {
1812  const auto const_bits_opt = expr2bits(
1813  to_array_of_expr(expr.op()).op(),
1816  ns);
1817 
1818  if(!const_bits_opt.has_value())
1819  return unchanged(expr);
1820 
1821  std::string const_bits=const_bits_opt.value();
1822 
1823  DATA_INVARIANT(!const_bits.empty(), "bit representation must be non-empty");
1824 
1825  // double the string until we have sufficiently many bits
1826  while(mp_integer(const_bits.size()) <
1827  *offset * expr.get_bits_per_byte() + *el_size)
1828  {
1829  const_bits+=const_bits;
1830  }
1831 
1832  std::string el_bits = std::string(
1833  const_bits,
1834  numeric_cast_v<std::size_t>(*offset * expr.get_bits_per_byte()),
1835  numeric_cast_v<std::size_t>(*el_size));
1836 
1837  auto tmp = bits2expr(
1838  el_bits, expr.type(), expr.id() == ID_byte_extract_little_endian, ns);
1839 
1840  if(tmp.has_value())
1841  return std::move(*tmp);
1842  }
1843 
1844  // in some cases we even handle non-const array_of
1845  if(
1846  expr.op().id() == ID_array_of &&
1847  (*offset * expr.get_bits_per_byte()) % (*el_size) == 0 &&
1848  *el_size <=
1850  {
1851  auto tmp = expr;
1852  tmp.op() = simplify_index(index_exprt(expr.op(), expr.offset()));
1853  tmp.offset() = from_integer(0, expr.offset().type());
1854  return changed(simplify_byte_extract(tmp));
1855  }
1856 
1857  // extract bits of a constant
1858  const auto bits =
1859  expr2bits(expr.op(), expr.id() == ID_byte_extract_little_endian, ns);
1860 
1861  if(
1862  bits.has_value() &&
1863  mp_integer(bits->size()) >= *el_size + *offset * expr.get_bits_per_byte())
1864  {
1865  // make sure we don't lose bits with structs containing flexible array
1866  // members
1867  const bool struct_has_flexible_array_member = has_subtype(
1868  expr.type(),
1869  [&](const typet &type) {
1870  if(type.id() != ID_struct && type.id() != ID_struct_tag)
1871  return false;
1872 
1873  const struct_typet &st = to_struct_type(ns.follow(type));
1874  const auto &comps = st.components();
1875  if(comps.empty() || comps.back().type().id() != ID_array)
1876  return false;
1877 
1878  if(comps.back().type().get_bool(ID_C_flexible_array_member))
1879  return true;
1880 
1881  const auto size =
1882  numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1883  return !size.has_value() || *size <= 1;
1884  },
1885  ns);
1886  if(!struct_has_flexible_array_member)
1887  {
1888  std::string bits_cut = std::string(
1889  bits.value(),
1890  numeric_cast_v<std::size_t>(*offset * expr.get_bits_per_byte()),
1891  numeric_cast_v<std::size_t>(*el_size));
1892 
1893  auto tmp = bits2expr(
1894  bits_cut, expr.type(), expr.id() == ID_byte_extract_little_endian, ns);
1895 
1896  if(tmp.has_value())
1897  return std::move(*tmp);
1898  }
1899  }
1900 
1901  // push byte extracts into struct or union expressions, just like
1902  // lower_byte_extract does (this is the same code, except recursive calls use
1903  // simplify rather than lower_byte_extract)
1904  if(expr.op().id() == ID_struct || expr.op().id() == ID_union)
1905  {
1906  if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
1907  {
1908  const struct_typet &struct_type = to_struct_type(ns.follow(expr.type()));
1909  const struct_typet::componentst &components = struct_type.components();
1910 
1911  bool failed = false;
1912  struct_exprt s({}, expr.type());
1913 
1914  for(const auto &comp : components)
1915  {
1916  auto component_bits = pointer_offset_bits(comp.type(), ns);
1917 
1918  // the next member would be misaligned, abort
1919  if(
1920  !component_bits.has_value() || *component_bits == 0 ||
1921  *component_bits % expr.get_bits_per_byte() != 0)
1922  {
1923  failed = true;
1924  break;
1925  }
1926 
1927  auto member_offset_opt =
1928  member_offset_expr(struct_type, comp.get_name(), ns);
1929 
1930  if(!member_offset_opt.has_value())
1931  {
1932  failed = true;
1933  break;
1934  }
1935 
1936  exprt new_offset = simplify_rec(
1937  plus_exprt{expr.offset(),
1939  member_offset_opt.value(), expr.offset().type())});
1940 
1941  byte_extract_exprt tmp = expr;
1942  tmp.type() = comp.type();
1943  tmp.offset() = new_offset;
1944 
1946  }
1947 
1948  if(!failed)
1949  return s;
1950  }
1951  else if(expr.type().id() == ID_union || expr.type().id() == ID_union_tag)
1952  {
1953  const union_typet &union_type = to_union_type(ns.follow(expr.type()));
1954  auto widest_member_opt = union_type.find_widest_union_component(ns);
1955  if(widest_member_opt.has_value())
1956  {
1957  byte_extract_exprt be = expr;
1958  be.type() = widest_member_opt->first.type();
1959  return union_exprt{widest_member_opt->first.get_name(),
1961  expr.type()};
1962  }
1963  }
1964  }
1965  else if(expr.op().id() == ID_array)
1966  {
1967  const array_typet &array_type = to_array_type(expr.op().type());
1968  const auto &element_bit_width =
1969  pointer_offset_bits(array_type.element_type(), ns);
1970  if(element_bit_width.has_value() && *element_bit_width > 0)
1971  {
1972  if(
1973  *offset > 0 &&
1974  *offset * expr.get_bits_per_byte() % *element_bit_width == 0)
1975  {
1976  const auto elements_to_erase = numeric_cast_v<std::size_t>(
1977  (*offset * expr.get_bits_per_byte()) / *element_bit_width);
1978  array_exprt slice = to_array_expr(expr.op());
1979  slice.operands().erase(
1980  slice.operands().begin(),
1981  slice.operands().begin() +
1982  std::min(elements_to_erase, slice.operands().size()));
1983  slice.type().size() =
1984  from_integer(slice.operands().size(), slice.type().size().type());
1985  byte_extract_exprt be = expr;
1986  be.op() = slice;
1987  be.offset() = from_integer(0, expr.offset().type());
1988  return changed(simplify_byte_extract(be));
1989  }
1990  else if(*offset == 0 && *el_size % *element_bit_width == 0)
1991  {
1992  const auto elements_to_keep =
1993  numeric_cast_v<std::size_t>(*el_size / *element_bit_width);
1994  array_exprt slice = to_array_expr(expr.op());
1995  if(slice.operands().size() > elements_to_keep)
1996  {
1997  slice.operands().resize(elements_to_keep);
1998  slice.type().size() =
1999  from_integer(slice.operands().size(), slice.type().size().type());
2000  byte_extract_exprt be = expr;
2001  be.op() = slice;
2002  return changed(simplify_byte_extract(be));
2003  }
2004  }
2005  }
2006  }
2007 
2008  // try to refine it down to extracting from a member or an index in an array
2009  auto subexpr =
2010  get_subexpression_at_offset(expr.op(), *offset, expr.type(), ns);
2011  if(subexpr.has_value() && subexpr.value() != expr)
2012  return changed(simplify_rec(subexpr.value())); // recursive call
2013 
2014  if(can_forward_propagatet(ns)(expr))
2015  return changed(simplify_rec(lower_byte_extract(expr, ns)));
2016 
2017  return unchanged(expr);
2018 }
2019 
2022 {
2023  // lift up any ID_if on the object
2024  if(expr.op().id() == ID_if)
2025  {
2026  if_exprt if_expr = lift_if(expr, 0);
2027  return changed(simplify_if_preorder(if_expr));
2028  }
2029  else
2030  {
2031  std::optional<exprt::operandst> new_operands;
2032 
2033  for(std::size_t i = 0; i < expr.operands().size(); ++i)
2034  {
2035  auto r_it = simplify_rec(expr.operands()[i]); // recursive call
2036  if(r_it.has_changed())
2037  {
2038  if(!new_operands.has_value())
2039  new_operands = expr.operands();
2040  (*new_operands)[i] = std::move(r_it.expr);
2041  }
2042  }
2043 
2044  if(new_operands.has_value())
2045  {
2046  exprt result = expr;
2047  std::swap(result.operands(), *new_operands);
2048  return result;
2049  }
2050  }
2051 
2052  return unchanged(expr);
2053 }
2054 
2057 {
2058  // byte_update(byte_update(root, offset, value), offset, value2) =>
2059  // byte_update(root, offset, value2)
2060  if(
2061  expr.id() == expr.op().id() &&
2062  expr.offset() == to_byte_update_expr(expr.op()).offset() &&
2063  expr.value().type() == to_byte_update_expr(expr.op()).value().type())
2064  {
2065  auto tmp = expr;
2066  tmp.set_op(to_byte_update_expr(expr.op()).op());
2067  return std::move(tmp);
2068  }
2069 
2070  const exprt &root = expr.op();
2071  const exprt &offset = expr.offset();
2072  const exprt &value = expr.value();
2073  const auto val_size = pointer_offset_bits(value.type(), ns);
2074  const auto root_size = pointer_offset_bits(root.type(), ns);
2075 
2076  const auto matching_byte_extract_id =
2077  expr.id() == ID_byte_update_little_endian ? ID_byte_extract_little_endian
2078  : ID_byte_extract_big_endian;
2079 
2080  // byte update of full object is byte_extract(new value)
2081  if(
2082  offset.is_zero() && val_size.has_value() && *val_size > 0 &&
2083  root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
2084  {
2085  byte_extract_exprt be(
2086  matching_byte_extract_id,
2087  value,
2088  offset,
2089  expr.get_bits_per_byte(),
2090  expr.type());
2091 
2092  return changed(simplify_byte_extract(be));
2093  }
2094 
2095  // update bits in a constant
2096  const auto offset_int = numeric_cast<mp_integer>(offset);
2097  if(
2098  root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
2099  *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
2100  *offset_int * expr.get_bits_per_byte() + *val_size <= *root_size)
2101  {
2102  auto root_bits =
2103  expr2bits(root, expr.id() == ID_byte_update_little_endian, ns);
2104 
2105  if(root_bits.has_value())
2106  {
2107  const auto val_bits =
2108  expr2bits(value, expr.id() == ID_byte_update_little_endian, ns);
2109 
2110  if(val_bits.has_value())
2111  {
2112  root_bits->replace(
2113  numeric_cast_v<std::size_t>(*offset_int * expr.get_bits_per_byte()),
2114  numeric_cast_v<std::size_t>(*val_size),
2115  *val_bits);
2116 
2117  auto tmp = bits2expr(
2118  *root_bits,
2119  expr.type(),
2120  expr.id() == ID_byte_update_little_endian,
2121  ns);
2122 
2123  if(tmp.has_value())
2124  return std::move(*tmp);
2125  }
2126  }
2127  }
2128 
2129  /*
2130  * byte_update(root, offset,
2131  * extract(root, offset) WITH component:=value)
2132  * =>
2133  * byte_update(root, offset + component offset,
2134  * value)
2135  */
2136 
2137  if(value.id()==ID_with)
2138  {
2139  const with_exprt &with=to_with_expr(value);
2140 
2141  if(with.old().id() == matching_byte_extract_id)
2142  {
2143  const byte_extract_exprt &extract=to_byte_extract_expr(with.old());
2144 
2145  /* the simplification can be used only if
2146  root and offset of update and extract
2147  are the same */
2148  if(!(root==extract.op()))
2149  return unchanged(expr);
2150  if(!(offset==extract.offset()))
2151  return unchanged(expr);
2152 
2153  const typet &tp=ns.follow(with.type());
2154  if(tp.id()==ID_struct)
2155  {
2156  const struct_typet &struct_type=to_struct_type(tp);
2157  const irep_idt &component_name=with.where().get(ID_component_name);
2158  const typet &c_type = struct_type.get_component(component_name).type();
2159 
2160  // is this a bit field?
2161  if(c_type.id() == ID_c_bit_field || c_type.id() == ID_bool)
2162  {
2163  // don't touch -- might not be byte-aligned
2164  }
2165  else
2166  {
2167  // new offset = offset + component offset
2168  auto i = member_offset(struct_type, component_name, ns);
2169  if(i.has_value())
2170  {
2171  exprt compo_offset = from_integer(*i, offset.type());
2172  plus_exprt new_offset(offset, compo_offset);
2173  exprt new_value(with.new_value());
2174  auto tmp = expr;
2175  tmp.set_offset(simplify_node(std::move(new_offset)));
2176  tmp.set_value(std::move(new_value));
2177  return changed(simplify_byte_update(tmp)); // recursive call
2178  }
2179  }
2180  }
2181  else if(tp.id()==ID_array)
2182  {
2183  auto i = pointer_offset_size(to_array_type(tp).element_type(), ns);
2184  if(i.has_value())
2185  {
2186  const exprt &index=with.where();
2187  exprt index_offset =
2188  simplify_mult(mult_exprt(index, from_integer(*i, index.type())));
2189 
2190  // index_offset may need a typecast
2191  if(offset.type() != index.type())
2192  {
2193  index_offset =
2194  simplify_typecast(typecast_exprt(index_offset, offset.type()));
2195  }
2196 
2197  plus_exprt new_offset(offset, index_offset);
2198  exprt new_value(with.new_value());
2199  auto tmp = expr;
2200  tmp.set_offset(simplify_plus(std::move(new_offset)));
2201  tmp.set_value(std::move(new_value));
2202  return changed(simplify_byte_update(tmp)); // recursive call
2203  }
2204  }
2205  }
2206  }
2207 
2208  // the following require a constant offset
2209  if(!offset_int.has_value() || *offset_int < 0)
2210  return unchanged(expr);
2211 
2212  const typet &op_type=ns.follow(root.type());
2213 
2214  // size must be known
2215  if(!val_size.has_value() || *val_size == 0)
2216  return unchanged(expr);
2217 
2218  // Are we updating (parts of) a struct? Do individual member updates
2219  // instead, unless there are non-byte-sized bit fields
2220  if(op_type.id()==ID_struct)
2221  {
2222  exprt result_expr;
2223  result_expr.make_nil();
2224 
2225  auto update_size = pointer_offset_size(value.type(), ns);
2226 
2227  const struct_typet &struct_type=
2228  to_struct_type(op_type);
2229  const struct_typet::componentst &components=
2230  struct_type.components();
2231 
2232  for(const auto &component : components)
2233  {
2234  auto m_offset = member_offset(struct_type, component.get_name(), ns);
2235 
2236  auto m_size_bits = pointer_offset_bits(component.type(), ns);
2237 
2238  // can we determine the current offset?
2239  if(!m_offset.has_value())
2240  {
2241  result_expr.make_nil();
2242  break;
2243  }
2244 
2245  // is it a byte-sized member?
2246  if(
2247  !m_size_bits.has_value() || *m_size_bits == 0 ||
2248  (*m_size_bits) % expr.get_bits_per_byte() != 0)
2249  {
2250  result_expr.make_nil();
2251  break;
2252  }
2253 
2254  mp_integer m_size_bytes = (*m_size_bits) / expr.get_bits_per_byte();
2255 
2256  // is that member part of the update?
2257  if(*m_offset + m_size_bytes <= *offset_int)
2258  continue;
2259  // are we done updating?
2260  else if(
2261  update_size.has_value() && *update_size > 0 &&
2262  *m_offset >= *offset_int + *update_size)
2263  {
2264  break;
2265  }
2266 
2267  if(result_expr.is_nil())
2268  result_expr = as_const(expr).op();
2269 
2270  exprt member_name(ID_member_name);
2271  member_name.set(ID_component_name, component.get_name());
2272  result_expr=with_exprt(result_expr, member_name, nil_exprt());
2273 
2274  // are we updating on member boundaries?
2275  if(
2276  *m_offset < *offset_int ||
2277  (*m_offset == *offset_int && update_size.has_value() &&
2278  *update_size > 0 && m_size_bytes > *update_size))
2279  {
2281  expr.id(),
2282  member_exprt(root, component.get_name(), component.type()),
2283  from_integer(*offset_int - *m_offset, offset.type()),
2284  value,
2285  expr.get_bits_per_byte());
2286 
2287  to_with_expr(result_expr).new_value().swap(v);
2288  }
2289  else if(
2290  update_size.has_value() && *update_size > 0 &&
2291  *m_offset + m_size_bytes > *offset_int + *update_size)
2292  {
2293  // we don't handle this for the moment
2294  result_expr.make_nil();
2295  break;
2296  }
2297  else
2298  {
2300  matching_byte_extract_id,
2301  value,
2302  from_integer(*m_offset - *offset_int, offset.type()),
2303  expr.get_bits_per_byte(),
2304  component.type());
2305 
2306  to_with_expr(result_expr).new_value().swap(v);
2307  }
2308  }
2309 
2310  if(result_expr.is_not_nil())
2311  return changed(simplify_rec(result_expr));
2312  }
2313 
2314  // replace elements of array or struct expressions, possibly using
2315  // byte_extract
2316  if(root.id()==ID_array)
2317  {
2318  auto el_size =
2319  pointer_offset_bits(to_type_with_subtype(op_type).subtype(), ns);
2320 
2321  if(
2322  !el_size.has_value() || *el_size == 0 ||
2323  (*el_size) % expr.get_bits_per_byte() != 0 ||
2324  (*val_size) % expr.get_bits_per_byte() != 0)
2325  {
2326  return unchanged(expr);
2327  }
2328 
2329  exprt result=root;
2330 
2331  mp_integer m_offset_bits=0, val_offset=0;
2332  Forall_operands(it, result)
2333  {
2334  if(*offset_int * expr.get_bits_per_byte() + (*val_size) <= m_offset_bits)
2335  break;
2336 
2337  if(*offset_int * expr.get_bits_per_byte() < m_offset_bits + *el_size)
2338  {
2339  mp_integer bytes_req =
2340  (m_offset_bits + *el_size) / expr.get_bits_per_byte() - *offset_int;
2341  bytes_req-=val_offset;
2342  if(val_offset + bytes_req > (*val_size) / expr.get_bits_per_byte())
2343  bytes_req = (*val_size) / expr.get_bits_per_byte() - val_offset;
2344 
2345  byte_extract_exprt new_val(
2346  matching_byte_extract_id,
2347  value,
2348  from_integer(val_offset, offset.type()),
2349  expr.get_bits_per_byte(),
2350  array_typet(
2352  from_integer(bytes_req, offset.type())));
2353 
2354  *it = byte_update_exprt(
2355  expr.id(),
2356  *it,
2357  from_integer(
2358  *offset_int + val_offset - m_offset_bits / expr.get_bits_per_byte(),
2359  offset.type()),
2360  new_val,
2361  expr.get_bits_per_byte());
2362 
2363  *it = simplify_rec(*it); // recursive call
2364 
2365  val_offset+=bytes_req;
2366  }
2367 
2368  m_offset_bits += *el_size;
2369  }
2370 
2371  return std::move(result);
2372  }
2373 
2374  return unchanged(expr);
2375 }
2376 
2379 {
2380  if(expr.id() == ID_complex_real)
2381  {
2382  auto &complex_real_expr = to_complex_real_expr(expr);
2383 
2384  if(complex_real_expr.op().id() == ID_complex)
2385  return to_complex_expr(complex_real_expr.op()).real();
2386  }
2387  else if(expr.id() == ID_complex_imag)
2388  {
2389  auto &complex_imag_expr = to_complex_imag_expr(expr);
2390 
2391  if(complex_imag_expr.op().id() == ID_complex)
2392  return to_complex_expr(complex_imag_expr.op()).imag();
2393  }
2394 
2395  return unchanged(expr);
2396 }
2397 
2400 {
2401  // When one operand is zero, an overflow can only occur for a subtraction from
2402  // zero.
2403  if(
2404  expr.op1().is_zero() ||
2405  (expr.op0().is_zero() && !can_cast_expr<minus_overflow_exprt>(expr)))
2406  {
2407  return false_exprt{};
2408  }
2409 
2410  // One is neutral element for multiplication
2411  if(
2413  (expr.op0().is_one() || expr.op1().is_one()))
2414  {
2415  return false_exprt{};
2416  }
2417 
2418  // we only handle the case of same operand types
2419  if(expr.op0().type() != expr.op1().type())
2420  return unchanged(expr);
2421 
2422  // catch some cases over mathematical types
2423  const irep_idt &op_type_id = expr.op0().type().id();
2424  if(
2425  op_type_id == ID_integer || op_type_id == ID_rational ||
2426  op_type_id == ID_real)
2427  {
2428  return false_exprt{};
2429  }
2430 
2431  if(op_type_id == ID_natural && !can_cast_expr<minus_overflow_exprt>(expr))
2432  return false_exprt{};
2433 
2434  // we only handle constants over signedbv/unsignedbv for the remaining cases
2435  if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2436  return unchanged(expr);
2437 
2438  if(!expr.op0().is_constant() || !expr.op1().is_constant())
2439  return unchanged(expr);
2440 
2441  const auto op0_value = numeric_cast<mp_integer>(expr.op0());
2442  const auto op1_value = numeric_cast<mp_integer>(expr.op1());
2443  if(!op0_value.has_value() || !op1_value.has_value())
2444  return unchanged(expr);
2445 
2446  mp_integer no_overflow_result;
2448  no_overflow_result = *op0_value + *op1_value;
2450  no_overflow_result = *op0_value - *op1_value;
2451  else if(can_cast_expr<mult_overflow_exprt>(expr))
2452  no_overflow_result = *op0_value * *op1_value;
2453  else if(can_cast_expr<shl_overflow_exprt>(expr))
2454  no_overflow_result = *op0_value << *op1_value;
2455  else
2456  UNREACHABLE;
2457 
2458  const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
2459  const integer_bitvector_typet bv_type{op_type_id, width};
2460  if(
2461  no_overflow_result < bv_type.smallest() ||
2462  no_overflow_result > bv_type.largest())
2463  {
2464  return true_exprt{};
2465  }
2466  else
2467  return false_exprt{};
2468 }
2469 
2472 {
2473  // zero is a neutral element for all operations supported here
2474  if(expr.op().is_zero())
2475  return false_exprt{};
2476 
2477  // catch some cases over mathematical types
2478  const irep_idt &op_type_id = expr.op().type().id();
2479  if(
2480  op_type_id == ID_integer || op_type_id == ID_rational ||
2481  op_type_id == ID_real)
2482  {
2483  return false_exprt{};
2484  }
2485 
2486  if(op_type_id == ID_natural)
2487  return true_exprt{};
2488 
2489  // we only handle constants over signedbv/unsignedbv for the remaining cases
2490  if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2491  return unchanged(expr);
2492 
2493  if(!expr.op().is_constant())
2494  return unchanged(expr);
2495 
2496  const auto op_value = numeric_cast<mp_integer>(expr.op());
2497  if(!op_value.has_value())
2498  return unchanged(expr);
2499 
2500  mp_integer no_overflow_result;
2502  no_overflow_result = -*op_value;
2503  else
2504  UNREACHABLE;
2505 
2506  const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
2507  const integer_bitvector_typet bv_type{op_type_id, width};
2508  if(
2509  no_overflow_result < bv_type.smallest() ||
2510  no_overflow_result > bv_type.largest())
2511  {
2512  return true_exprt{};
2513  }
2514  else
2515  return false_exprt{};
2516 }
2517 
2520 {
2521  if(expr.id() == ID_overflow_result_unary_minus)
2522  {
2523  // zero is a neutral element
2524  if(expr.op0().is_zero())
2525  return struct_exprt{{expr.op0(), false_exprt{}}, expr.type()};
2526 
2527  // catch some cases over mathematical types
2528  const irep_idt &op_type_id = expr.op0().type().id();
2529  if(
2530  op_type_id == ID_integer || op_type_id == ID_rational ||
2531  op_type_id == ID_real)
2532  {
2533  return struct_exprt{{expr.op0(), false_exprt{}}, expr.type()};
2534  }
2535 
2536  // always an overflow for natural numbers, but the result is not
2537  // representable
2538  if(op_type_id == ID_natural)
2539  return unchanged(expr);
2540 
2541  // we only handle constants over signedbv/unsignedbv for the remaining cases
2542  if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2543  return unchanged(expr);
2544 
2545  if(!expr.op0().is_constant())
2546  return unchanged(expr);
2547 
2548  const auto op_value = numeric_cast<mp_integer>(expr.op0());
2549  if(!op_value.has_value())
2550  return unchanged(expr);
2551 
2552  mp_integer no_overflow_result = -*op_value;
2553 
2554  const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
2555  const integer_bitvector_typet bv_type{op_type_id, width};
2556  if(
2557  no_overflow_result < bv_type.smallest() ||
2558  no_overflow_result > bv_type.largest())
2559  {
2560  return struct_exprt{
2561  {from_integer(no_overflow_result, expr.op0().type()), true_exprt{}},
2562  expr.type()};
2563  }
2564  else
2565  {
2566  return struct_exprt{
2567  {from_integer(no_overflow_result, expr.op0().type()), false_exprt{}},
2568  expr.type()};
2569  }
2570  }
2571  else
2572  {
2573  // When one operand is zero, an overflow can only occur for a subtraction
2574  // from zero.
2575  if(expr.op0().is_zero())
2576  {
2577  if(
2578  expr.id() == ID_overflow_result_plus ||
2579  expr.id() == ID_overflow_result_shl)
2580  {
2581  return struct_exprt{{expr.op1(), false_exprt{}}, expr.type()};
2582  }
2583  else if(expr.id() == ID_overflow_result_mult)
2584  {
2585  return struct_exprt{
2586  {from_integer(0, expr.op0().type()), false_exprt{}}, expr.type()};
2587  }
2588  }
2589  else if(expr.op1().is_zero())
2590  {
2591  if(
2592  expr.id() == ID_overflow_result_plus ||
2593  expr.id() == ID_overflow_result_minus ||
2594  expr.id() == ID_overflow_result_shl)
2595  {
2596  return struct_exprt{{expr.op0(), false_exprt{}}, expr.type()};
2597  }
2598  else
2599  {
2600  return struct_exprt{
2601  {from_integer(0, expr.op0().type()), false_exprt{}}, expr.type()};
2602  }
2603  }
2604 
2605  // One is neutral element for multiplication
2606  if(
2607  expr.id() == ID_overflow_result_mult &&
2608  (expr.op0().is_one() || expr.op1().is_one()))
2609  {
2610  return struct_exprt{
2611  {expr.op0().is_one() ? expr.op1() : expr.op0(), false_exprt{}},
2612  expr.type()};
2613  }
2614 
2615  // we only handle the case of same operand types
2616  if(
2617  expr.id() != ID_overflow_result_shl &&
2618  expr.op0().type() != expr.op1().type())
2619  {
2620  return unchanged(expr);
2621  }
2622 
2623  // catch some cases over mathematical types
2624  const irep_idt &op_type_id = expr.op0().type().id();
2625  if(
2626  expr.id() != ID_overflow_result_shl &&
2627  (op_type_id == ID_integer || op_type_id == ID_rational ||
2628  op_type_id == ID_real))
2629  {
2630  irep_idt id =
2631  expr.id() == ID_overflow_result_plus
2632  ? ID_plus
2633  : expr.id() == ID_overflow_result_minus ? ID_minus : ID_mult;
2634  return struct_exprt{
2635  {simplify_node(binary_exprt{expr.op0(), id, expr.op1()}),
2636  false_exprt{}},
2637  expr.type()};
2638  }
2639 
2640  if(
2641  (expr.id() == ID_overflow_result_plus ||
2642  expr.id() == ID_overflow_result_mult) &&
2643  op_type_id == ID_natural)
2644  {
2645  return struct_exprt{
2647  expr.op0(),
2648  expr.id() == ID_overflow_result_plus ? ID_plus : ID_mult,
2649  expr.op1()}),
2650  false_exprt{}},
2651  expr.type()};
2652  }
2653 
2654  // we only handle constants over signedbv/unsignedbv for the remaining cases
2655  if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2656  return unchanged(expr);
2657 
2658  // a special case of overflow-minus checking with operands (X + n) and X
2659  if(expr.id() == ID_overflow_result_minus)
2660  {
2661  const exprt &tc_op0 = skip_typecast(expr.op0());
2662  const exprt &tc_op1 = skip_typecast(expr.op1());
2663 
2664  if(auto sum = expr_try_dynamic_cast<plus_exprt>(tc_op0))
2665  {
2666  if(skip_typecast(sum->op0()) == tc_op1 && sum->operands().size() == 2)
2667  {
2668  std::optional<exprt> offset;
2669  if(sum->type().id() == ID_pointer)
2670  {
2671  offset = std::move(simplify_pointer_offset(
2672  pointer_offset_exprt{*sum, expr.op0().type()})
2673  .expr);
2674  if(offset->id() == ID_pointer_offset)
2675  return unchanged(expr);
2676  }
2677  else
2678  offset = std::move(
2679  simplify_typecast(typecast_exprt{sum->op1(), expr.op0().type()})
2680  .expr);
2681 
2682  exprt offset_op = skip_typecast(*offset);
2683  if(
2684  offset_op.type().id() != ID_signedbv &&
2685  offset_op.type().id() != ID_unsignedbv)
2686  {
2687  return unchanged(expr);
2688  }
2689 
2690  const std::size_t width =
2691  to_bitvector_type(expr.op0().type()).get_width();
2692  const integer_bitvector_typet bv_type{op_type_id, width};
2693 
2694  or_exprt not_representable{
2696  offset_op,
2697  ID_lt,
2698  from_integer(bv_type.smallest(), offset_op.type())},
2700  offset_op,
2701  ID_gt,
2702  from_integer(bv_type.largest(), offset_op.type())}};
2703 
2704  return struct_exprt{
2705  {*offset, simplify_rec(not_representable)}, expr.type()};
2706  }
2707  }
2708  }
2709 
2710  if(!expr.op0().is_constant() || !expr.op1().is_constant())
2711  return unchanged(expr);
2712 
2713  // preserve the sizeof type annotation
2714  std::optional<typet> c_sizeof_type;
2715  for(const auto &op : expr.operands())
2716  {
2717  const typet &sizeof_type =
2718  static_cast<const typet &>(op.find(ID_C_c_sizeof_type));
2719  if(sizeof_type.is_not_nil())
2720  {
2721  c_sizeof_type = sizeof_type;
2722  break;
2723  }
2724  }
2725 
2726  const auto op0_value = numeric_cast<mp_integer>(expr.op0());
2727  const auto op1_value = numeric_cast<mp_integer>(expr.op1());
2728  if(!op0_value.has_value() || !op1_value.has_value())
2729  return unchanged(expr);
2730 
2731  mp_integer no_overflow_result;
2732  if(expr.id() == ID_overflow_result_plus)
2733  no_overflow_result = *op0_value + *op1_value;
2734  else if(expr.id() == ID_overflow_result_minus)
2735  no_overflow_result = *op0_value - *op1_value;
2736  else if(expr.id() == ID_overflow_result_mult)
2737  no_overflow_result = *op0_value * *op1_value;
2738  else if(expr.id() == ID_overflow_result_shl)
2739  no_overflow_result = *op0_value << *op1_value;
2740  else
2741  UNREACHABLE;
2742 
2743  exprt no_overflow_result_expr =
2744  from_integer(no_overflow_result, expr.op0().type());
2745  if(c_sizeof_type.has_value())
2746  no_overflow_result_expr.set(ID_C_c_sizeof_type, *c_sizeof_type);
2747 
2748  const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
2749  const integer_bitvector_typet bv_type{op_type_id, width};
2750  if(
2751  no_overflow_result < bv_type.smallest() ||
2752  no_overflow_result > bv_type.largest())
2753  {
2754  return struct_exprt{
2755  {std::move(no_overflow_result_expr), true_exprt{}}, expr.type()};
2756  }
2757  else
2758  {
2759  return struct_exprt{
2760  {std::move(no_overflow_result_expr), false_exprt{}}, expr.type()};
2761  }
2762  }
2763 }
2764 
2767 {
2768  auto result = unchanged(expr);
2769 
2770  // The ifs below could one day be replaced by a switch()
2771 
2772  if(expr.id()==ID_address_of)
2773  {
2774  // the argument of this expression needs special treatment
2775  }
2776  else if(expr.id()==ID_if)
2777  {
2778  result = simplify_if_preorder(to_if_expr(expr));
2779  }
2780  else if(expr.id() == ID_typecast)
2781  {
2783  }
2784  else if(
2785  expr.id() == ID_byte_extract_little_endian ||
2786  expr.id() == ID_byte_extract_big_endian)
2787  {
2789  }
2790  else if(expr.id() == ID_dereference)
2791  {
2793  }
2794  else if(expr.id() == ID_index)
2795  {
2796  result = simplify_index_preorder(to_index_expr(expr));
2797  }
2798  else if(expr.id() == ID_member)
2799  {
2800  result = simplify_member_preorder(to_member_expr(expr));
2801  }
2802  else if(
2803  expr.id() == ID_is_dynamic_object || expr.id() == ID_is_invalid_pointer ||
2804  expr.id() == ID_object_size || expr.id() == ID_pointer_object ||
2805  expr.id() == ID_pointer_offset)
2806  {
2808  }
2809  else if(expr.has_operands())
2810  {
2811  std::optional<exprt::operandst> new_operands;
2812 
2813  for(std::size_t i = 0; i < expr.operands().size(); ++i)
2814  {
2815  auto r_it = simplify_rec(expr.operands()[i]); // recursive call
2816  if(r_it.has_changed())
2817  {
2818  if(!new_operands.has_value())
2819  new_operands = expr.operands();
2820  (*new_operands)[i] = std::move(r_it.expr);
2821  }
2822  }
2823 
2824  if(new_operands.has_value())
2825  {
2826  std::swap(result.expr.operands(), *new_operands);
2827  result.expr_changed = resultt<>::CHANGED;
2828  }
2829  }
2830 
2831  if(as_const(result.expr).type().id() == ID_array)
2832  {
2833  const array_typet &array_type = to_array_type(as_const(result.expr).type());
2834  resultt<> simp_size = simplify_rec(array_type.size());
2835  if(simp_size.has_changed())
2836  {
2837  to_array_type(result.expr.type()).size() = simp_size.expr;
2838  result.expr_changed = resultt<>::CHANGED;
2839  }
2840  }
2841 
2842  return result;
2843 }
2844 
2846 {
2847  if(!node.has_operands())
2848  return unchanged(node); // no change
2849 
2850  // #define DEBUGX
2851 
2852 #ifdef DEBUGX
2853  exprt old(node);
2854 #endif
2855 
2856  exprt expr = node;
2857  bool no_change_join_operands = join_operands(expr);
2858 
2859  resultt<> r = unchanged(expr);
2860 
2861  if(expr.id()==ID_typecast)
2862  {
2864  }
2865  else if(expr.id()==ID_equal || expr.id()==ID_notequal ||
2866  expr.id()==ID_gt || expr.id()==ID_lt ||
2867  expr.id()==ID_ge || expr.id()==ID_le)
2868  {
2870  }
2871  else if(expr.id()==ID_if)
2872  {
2873  r = simplify_if(to_if_expr(expr));
2874  }
2875  else if(expr.id()==ID_lambda)
2876  {
2877  r = simplify_lambda(to_lambda_expr(expr));
2878  }
2879  else if(expr.id()==ID_with)
2880  {
2881  r = simplify_with(to_with_expr(expr));
2882  }
2883  else if(expr.id()==ID_update)
2884  {
2885  r = simplify_update(to_update_expr(expr));
2886  }
2887  else if(expr.id()==ID_index)
2888  {
2889  r = simplify_index(to_index_expr(expr));
2890  }
2891  else if(expr.id()==ID_member)
2892  {
2893  r = simplify_member(to_member_expr(expr));
2894  }
2895  else if(expr.id()==ID_byte_update_little_endian ||
2896  expr.id()==ID_byte_update_big_endian)
2897  {
2899  }
2900  else if(expr.id()==ID_byte_extract_little_endian ||
2901  expr.id()==ID_byte_extract_big_endian)
2902  {
2904  }
2905  else if(expr.id()==ID_pointer_object)
2906  {
2908  }
2909  else if(expr.id() == ID_is_dynamic_object)
2910  {
2912  }
2913  else if(expr.id() == ID_is_invalid_pointer)
2914  {
2916  }
2917  else if(
2918  const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
2919  {
2921  }
2922  else if(expr.id()==ID_div)
2923  {
2924  r = simplify_div(to_div_expr(expr));
2925  }
2926  else if(expr.id()==ID_mod)
2927  {
2928  r = simplify_mod(to_mod_expr(expr));
2929  }
2930  else if(expr.id()==ID_bitnot)
2931  {
2932  r = simplify_bitnot(to_bitnot_expr(expr));
2933  }
2934  else if(expr.id()==ID_bitand ||
2935  expr.id()==ID_bitor ||
2936  expr.id()==ID_bitxor)
2937  {
2939  }
2940  else if(expr.id()==ID_ashr || expr.id()==ID_lshr || expr.id()==ID_shl)
2941  {
2942  r = simplify_shifts(to_shift_expr(expr));
2943  }
2944  else if(expr.id()==ID_power)
2945  {
2946  r = simplify_power(to_binary_expr(expr));
2947  }
2948  else if(expr.id()==ID_plus)
2949  {
2950  r = simplify_plus(to_plus_expr(expr));
2951  }
2952  else if(expr.id()==ID_minus)
2953  {
2954  r = simplify_minus(to_minus_expr(expr));
2955  }
2956  else if(expr.id()==ID_mult)
2957  {
2958  r = simplify_mult(to_mult_expr(expr));
2959  }
2960  else if(expr.id()==ID_floatbv_plus ||
2961  expr.id()==ID_floatbv_minus ||
2962  expr.id()==ID_floatbv_mult ||
2963  expr.id()==ID_floatbv_div)
2964  {
2966  }
2967  else if(expr.id()==ID_floatbv_typecast)
2968  {
2970  }
2971  else if(expr.id()==ID_unary_minus)
2972  {
2974  }
2975  else if(expr.id()==ID_unary_plus)
2976  {
2978  }
2979  else if(expr.id()==ID_not)
2980  {
2981  r = simplify_not(to_not_expr(expr));
2982  }
2983  else if(expr.id()==ID_implies ||
2984  expr.id()==ID_or || expr.id()==ID_xor ||
2985  expr.id()==ID_and)
2986  {
2987  r = simplify_boolean(expr);
2988  }
2989  else if(expr.id()==ID_dereference)
2990  {
2992  }
2993  else if(expr.id()==ID_address_of)
2994  {
2996  }
2997  else if(expr.id()==ID_pointer_offset)
2998  {
3000  }
3001  else if(expr.id()==ID_extractbit)
3002  {
3004  }
3005  else if(expr.id()==ID_concatenation)
3006  {
3008  }
3009  else if(expr.id()==ID_extractbits)
3010  {
3012  }
3013  else if(expr.id()==ID_ieee_float_equal ||
3014  expr.id()==ID_ieee_float_notequal)
3015  {
3017  }
3018  else if(expr.id() == ID_bswap)
3019  {
3020  r = simplify_bswap(to_bswap_expr(expr));
3021  }
3022  else if(expr.id()==ID_isinf)
3023  {
3024  r = simplify_isinf(to_unary_expr(expr));
3025  }
3026  else if(expr.id()==ID_isnan)
3027  {
3028  r = simplify_isnan(to_unary_expr(expr));
3029  }
3030  else if(expr.id()==ID_isnormal)
3031  {
3033  }
3034  else if(expr.id()==ID_abs)
3035  {
3036  r = simplify_abs(to_abs_expr(expr));
3037  }
3038  else if(expr.id()==ID_sign)
3039  {
3040  r = simplify_sign(to_sign_expr(expr));
3041  }
3042  else if(expr.id() == ID_popcount)
3043  {
3045  }
3046  else if(expr.id() == ID_count_leading_zeros)
3047  {
3049  }
3050  else if(expr.id() == ID_count_trailing_zeros)
3051  {
3053  }
3054  else if(expr.id() == ID_find_first_set)
3055  {
3057  }
3058  else if(expr.id() == ID_function_application)
3059  {
3061  }
3062  else if(expr.id() == ID_complex_real || expr.id() == ID_complex_imag)
3063  {
3064  r = simplify_complex(to_unary_expr(expr));
3065  }
3066  else if(
3067  const auto binary_overflow =
3068  expr_try_dynamic_cast<binary_overflow_exprt>(expr))
3069  {
3070  r = simplify_overflow_binary(*binary_overflow);
3071  }
3072  else if(
3073  const auto unary_overflow =
3074  expr_try_dynamic_cast<unary_overflow_exprt>(expr))
3075  {
3076  r = simplify_overflow_unary(*unary_overflow);
3077  }
3078  else if(
3079  const auto overflow_result =
3080  expr_try_dynamic_cast<overflow_result_exprt>(expr))
3081  {
3082  r = simplify_overflow_result(*overflow_result);
3083  }
3084  else if(expr.id() == ID_bitreverse)
3085  {
3087  }
3088  else if(
3089  const auto prophecy_r_or_w_ok =
3090  expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(expr))
3091  {
3092  r = simplify_prophecy_r_or_w_ok(*prophecy_r_or_w_ok);
3093  }
3094  else if(
3095  const auto prophecy_pointer_in_range =
3096  expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(expr))
3097  {
3098  r = simplify_prophecy_pointer_in_range(*prophecy_pointer_in_range);
3099  }
3100 
3101  if(!no_change_join_operands)
3102  r = changed(r);
3103 
3104 #ifdef DEBUGX
3105  if(
3106  r.has_changed()
3107 # ifdef DEBUG_ON_DEMAND
3108  && debug_on
3109 # endif
3110  )
3111  {
3112  std::cout << "===== " << node.id() << ": " << format(node) << '\n'
3113  << " ---> " << format(r.expr) << '\n';
3114  }
3115 #endif
3116 
3117  return r;
3118 }
3119 
3121 {
3122  // look up in cache
3123 
3124  #ifdef USE_CACHE
3125  std::pair<simplify_expr_cachet::containert::iterator, bool>
3126  cache_result=simplify_expr_cache.container().
3127  insert(std::pair<exprt, exprt>(expr, exprt()));
3128 
3129  if(!cache_result.second) // found!
3130  {
3131  const exprt &new_expr=cache_result.first->second;
3132 
3133  if(new_expr.id().empty())
3134  return true; // no change
3135 
3136  expr=new_expr;
3137  return false;
3138  }
3139  #endif
3140 
3141  // We work on a copy to prevent unnecessary destruction of sharing.
3142  auto simplify_node_preorder_result = simplify_node_preorder(expr);
3143 
3144  auto simplify_node_result = simplify_node(simplify_node_preorder_result.expr);
3145 
3146  if(
3147  !simplify_node_result.has_changed() &&
3148  simplify_node_preorder_result.has_changed())
3149  {
3150  simplify_node_result.expr_changed =
3151  simplify_node_preorder_result.expr_changed;
3152  }
3153 
3154 #ifdef USE_LOCAL_REPLACE_MAP
3155  exprt tmp = simplify_node_result.expr;
3156 # if 1
3157  replace_mapt::const_iterator it =
3158  local_replace_map.find(simplify_node_result.expr);
3159  if(it!=local_replace_map.end())
3160  simplify_node_result = changed(it->second);
3161 # else
3162  if(
3163  !local_replace_map.empty() &&
3164  !replace_expr(local_replace_map, simplify_node_result.expr))
3165  {
3166  simplify_node_result = changed(simplify_rec(simplify_node_result.expr));
3167  }
3168 # endif
3169 #endif
3170 
3171  if(!simplify_node_result.has_changed())
3172  {
3173  return unchanged(expr);
3174  }
3175  else
3176  {
3178  (as_const(simplify_node_result.expr).type().id() == ID_array &&
3179  expr.type().id() == ID_array) ||
3180  as_const(simplify_node_result.expr).type() == expr.type(),
3181  simplify_node_result.expr.pretty(),
3182  expr.pretty());
3183 
3184 #ifdef USE_CACHE
3185  // save in cache
3186  cache_result.first->second = simplify_node_result.expr;
3187 #endif
3188 
3189  return simplify_node_result;
3190  }
3191 }
3192 
3195 {
3196 #ifdef DEBUG_ON_DEMAND
3197  if(debug_on)
3198  std::cout << "TO-SIMP " << format(expr) << "\n";
3199 #endif
3200  auto result = simplify_rec(expr);
3201 #ifdef DEBUG_ON_DEMAND
3202  if(debug_on)
3203  std::cout << "FULLSIMP " << format(result.expr) << "\n";
3204 #endif
3205  if(result.has_changed())
3206  {
3207  expr = result.expr;
3208  return false; // change
3209  }
3210  else
3211  return true; // no change
3212 }
3213 
3215 bool simplify(exprt &expr, const namespacet &ns)
3216 {
3217  return simplify_exprt(ns).simplify(expr);
3218 }
3219 
3221 {
3222  simplify_exprt(ns).simplify(src);
3223  return src;
3224 }
configt config
Definition: config.cpp:25
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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
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.
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
API to expression classes for bitvectors.
bool can_cast_expr< mult_overflow_exprt >(const exprt &base)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool can_cast_expr< minus_overflow_exprt >(const exprt &base)
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
bool can_cast_expr< shl_overflow_exprt >(const exprt &base)
const find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
bool can_cast_expr< plus_overflow_exprt >(const exprt &base)
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
bool can_cast_expr< unary_minus_overflow_exprt >(const exprt &base)
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:198
Expression classes for byte-level operators.
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
int16_t s2
Definition: bytecode_info.h:60
int8_t s1
Definition: bytecode_info.h:59
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:335
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:184
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:377
Absolute value.
Definition: std_expr.h:442
Operator to return the address of an object.
Definition: pointer_expr.h:540
exprt & object()
Definition: pointer_expr.h:549
Array constructor from list of elements.
Definition: std_expr.h:1616
exprt & what()
Definition: std_expr.h:1570
Arrays with given size.
Definition: std_types.h:807
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
const exprt & size() const
Definition: std_types.h:840
A base class for binary expressions.
Definition: std_expr.h:638
exprt & op1()
Definition: expr.h:136
exprt & op0()
Definition: expr.h:133
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
std::size_t get_width() const
Definition: std_types.h:920
Expression of type type extracted from some object op starting at position offset (given in number of...
std::size_t get_bits_per_byte() const
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & value() const
void set_offset(exprt e)
const exprt & op() const
const exprt & offset() const
void set_op(exprt e)
std::size_t get_bits_per_byte() const
The C/C++ Booleans.
Definition: c_types.h:97
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:352
const typet & underlying_type() const
Definition: c_types.h:307
Determine whether an expression is constant.
Definition: expr_util.h:89
exprt real()
Definition: std_expr.h:1922
exprt imag()
Definition: std_expr.h:1932
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition: std_expr.h:2987
const irep_idt & get_value() const
Definition: std_expr.h:2995
void set_value(const irep_idt &value)
Definition: std_expr.h:3000
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Operator to dereference a pointer.
Definition: pointer_expr.h:834
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Union constructor to support unions without any member (a GCC/Clang feature).
Definition: std_expr.h:1829
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:96
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:91
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
exprt & op1()
Definition: expr.h:136
source_locationt & add_source_location()
Definition: expr.h:236
const source_locationt & source_location() const
Definition: expr.h:231
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:47
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
exprt & op0()
Definition: expr.h:133
operandst & operands()
Definition: expr.h:94
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:170
The Boolean constant false.
Definition: std_expr.h:3064
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
Fixed-width bit-vector with signed fixed-point interpretation.
fixedbv_spect spec
Definition: fixedbv.h:44
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
mp_integer to_integer() const
Definition: fixedbv.cpp:37
void set_value(const mp_integer &_v)
Definition: fixedbv.h:96
void round(const fixedbv_spect &dest_spec)
Definition: fixedbv.cpp:52
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
ieee_float_spect spec
Definition: ieee_float.h:134
mp_integer to_integer() const
constant_exprt to_expr() const
Definition: ieee_float.cpp:703
bool get_sign() const
Definition: ieee_float.h:247
void set_sign(bool _sign)
Definition: ieee_float.h:183
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:516
mp_integer pack() const
Definition: ieee_float.cpp:375
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
Definition: std_expr.h:2370
exprt & true_case()
Definition: std_expr.h:2397
exprt & false_case()
Definition: std_expr.h:2407
Array index operator.
Definition: std_expr.h:1465
exprt & array()
Definition: std_expr.h:1495
exprt & index()
Definition: std_expr.h:1505
Fixed-width bit-vector representing a signed or unsigned integer.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:408
bool is_not_nil() const
Definition: irep.h:368
const irep_idt & id() const
Definition: irep.h:384
void make_nil()
Definition: irep.h:442
void swap(irept &irep)
Definition: irep.h:430
bool is_nil() const
Definition: irep.h:364
A (mathematical) lambda expression.
exprt application(const operandst &arguments) const
Extract member of struct or union.
Definition: std_expr.h:2841
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1107
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The NIL expression.
Definition: std_expr.h:3073
The null pointer constant.
Definition: pointer_expr.h:909
Boolean OR.
Definition: std_expr.h:2228
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
exprt & op1()
Definition: expr.h:136
exprt & op0()
Definition: expr.h:133
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
The offset (in bytes) of a pointer relative to the object.
The popcount (counting the number of bits set to 1) expression.
const exprt & length() const
Definition: string_expr.h:129
const exprt & content() const
Definition: string_expr.h:139
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:596
Fixed-width bit-vector with two's complement interpretation.
resultt simplify_isnan(const unary_exprt &)
resultt simplify_bitwise(const multi_ary_exprt &)
resultt simplify_power(const binary_exprt &)
const namespacet & ns
resultt simplify_div(const div_exprt &)
resultt simplify_byte_extract(const byte_extract_exprt &)
resultt simplify_bitreverse(const bitreverse_exprt &)
Try to simplify bit-reversing to a constant expression.
resultt simplify_abs(const abs_exprt &)
resultt simplify_isnormal(const unary_exprt &)
resultt simplify_dereference(const dereference_exprt &)
resultt simplify_bitnot(const bitnot_exprt &)
resultt simplify_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &)
Try to simplify prophecy_{r,w,rw}_ok to a constant expression.
resultt simplify_member_preorder(const member_exprt &)
resultt simplify_popcount(const popcount_exprt &)
static resultt changed(resultt<> result)
resultt simplify_dereference_preorder(const dereference_exprt &)
resultt simplify_unary_pointer_predicate_preorder(const unary_exprt &)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_if(const if_exprt &)
resultt simplify_node(const exprt &)
resultt simplify_node_preorder(const exprt &)
resultt simplify_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &)
Try to simplify prophecy_pointer_in_range to a constant expression.
resultt simplify_overflow_unary(const unary_overflow_exprt &)
Try to simplify overflow-unary-.
resultt simplify_minus(const minus_exprt &)
resultt simplify_extractbit(const extractbit_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_shifts(const shift_exprt &)
resultt simplify_index_preorder(const index_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_pointer_object(const pointer_object_exprt &)
resultt simplify_boolean(const exprt &)
resultt simplify_object(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
resultt simplify_with(const with_exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_not(const not_exprt &)
resultt simplify_isinf(const unary_exprt &)
resultt simplify_overflow_binary(const binary_overflow_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
resultt simplify_function_application(const function_application_exprt &)
Attempt to simplify mathematical function applications if we have enough information to do so.
resultt simplify_index(const index_exprt &)
resultt simplify_bswap(const bswap_exprt &)
resultt simplify_member(const member_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_byte_update(const byte_update_exprt &)
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
resultt simplify_update(const update_exprt &)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_mod(const mod_exprt &)
resultt simplify_complex(const unary_exprt &)
resultt simplify_pointer_offset(const pointer_offset_exprt &)
resultt simplify_plus(const plus_exprt &)
virtual bool simplify(exprt &expr)
resultt simplify_unary_plus(const unary_plus_exprt &)
resultt simplify_overflow_result(const overflow_result_exprt &)
Try to simplify overflow_result-+, overflow_result-*, overflow_result–, overflow_result-shl,...
resultt simplify_ffs(const find_first_set_exprt &)
Try to simplify find-first-set to a constant expression.
resultt simplify_if_preorder(const if_exprt &expr)
resultt simplify_byte_extract_preorder(const byte_extract_exprt &)
resultt simplify_is_dynamic_object(const unary_exprt &)
resultt simplify_object_size(const object_size_exprt &)
resultt simplify_lambda(const lambda_exprt &)
resultt simplify_concatenation(const concatenation_exprt &)
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
resultt simplify_ctz(const count_trailing_zeros_exprt &)
Try to simplify count-trailing-zeros to a constant expression.
resultt simplify_clz(const count_leading_zeros_exprt &)
Try to simplify count-leading-zeros to a constant expression.
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
resultt simplify_typecast_preorder(const typecast_exprt &)
resultt simplify_sign(const sign_exprt &)
resultt simplify_unary_minus(const unary_minus_exprt &)
Struct constructor from list of elements.
Definition: std_expr.h:1872
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:63
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
const componentst & components() const
Definition: std_types.h:147
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:46
std::vector< componentt > componentst
Definition: std_types.h:140
const irep_idt & get_identifier() const
Definition: std_expr.h:160
The Boolean constant true.
Definition: std_expr.h:3055
Semantic type conversion.
Definition: std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:361
const exprt & op1() const =delete
const exprt & op() const
Definition: std_expr.h:391
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
Definition: std_expr.h:1765
The union type.
Definition: c_types.h:147
std::optional< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
Definition: c_types.cpp:300
Fixed-width bit-vector with unsigned binary interpretation.
Operator to update elements in structs and arrays.
Definition: std_expr.h:2655
exprt::operandst & designator()
Definition: std_expr.h:2681
exprt & old()
Definition: std_expr.h:2667
exprt & new_value()
Definition: std_expr.h:2691
Operator to update elements in structs and arrays.
Definition: std_expr.h:2471
exprt & old()
Definition: std_expr.h:2481
exprt & new_value()
Definition: std_expr.h:2501
exprt & where()
Definition: std_expr.h:2491
int isalpha(int c)
Definition: ctype.c:9
int tolower(int c)
Definition: ctype.c:100
int isupper(int c)
Definition: ctype.c:90
#define Forall_operands(it, expr)
Definition: expr.h:27
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:338
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:100
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:219
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:203
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition: expr_util.cpp:369
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
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
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
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
static format_containert< T > format(const T &o)
Definition: format.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
static int8_t r
Definition: irep_hash.h:60
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
API to expression classes for Pointers.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Pointer Logic.
exprt pointer_offset_sum(const exprt &a, const exprt &b)
Pointer Dereferencing.
exprt object_size(const exprt &pointer)
constant_exprt from_rational(const rationalt &a)
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify(exprt &expr, const namespacet &ns)
static simplify_exprt::resultt simplify_string_compare_to(const function_application_exprt &expr, const namespacet &ns)
Simplify String.compareTo function when arguments are constant.
static simplify_exprt::resultt simplify_string_contains(const function_application_exprt &expr, const namespacet &ns)
Simplify String.contains function when arguments are constant.
static simplify_exprt::resultt simplify_string_endswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.endsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_char_at(const function_application_exprt &expr, const namespacet &ns)
Simplify String.charAt function when arguments are constant.
static simplify_exprt::resultt simplify_string_startswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.startsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_is_empty(const function_application_exprt &expr, const namespacet &ns)
Simplify String.isEmpty function when arguments are constant.
static bool lower_case_string_expression(array_exprt &string_data)
Take the passed-in constant string array and lower-case every character.
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.
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.
exprt simplify_expr(exprt src, const namespacet &ns)
std::optional< 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.
std::optional< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
std::optional< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
bool join_operands(exprt &expr)
BigInt mp_integer
Definition: smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define POSTCONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:480
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:80
API to expression classes.
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2586
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2735
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:556
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3037
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1272
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1660
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2102
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:2005
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2352
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:514
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1201
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1086
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:987
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2533
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1895
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:715
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1598
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:1041
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1960
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2933
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:426
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:2048
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:621
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:466
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:895
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1132
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
String expressions for the string solver.
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:151
bool can_cast_expr< refined_string_exprt >(const exprt &base)
Definition: string_expr.h:166
endiannesst endianness
Definition: config.h:207
bool NULL_is_zero
Definition: config.h:224
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:208
#define size_type
Definition: unistd.c:347