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