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 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
simplify_exprt::simplify_rec
resultt simplify_rec(const exprt &)
Definition: simplify_expr.cpp:2564
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
exprt::op2
exprt & op2()
Definition: expr.h:105
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:147
simplify_exprt::simplify_is_invalid_pointer
resultt simplify_is_invalid_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:611
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:213
simplify_exprt::simplify_isnormal
resultt simplify_isnormal(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:51
ieee_floatt
Definition: ieee_float.h:117
format
static format_containert< T > format(const T &o)
Definition: format.h:37
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2507
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
to_extractbit_expr
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: bitvector_expr.h:411
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:167
simplify_exprt::simplify_shifts
resultt simplify_shifts(const shift_exprt &)
Definition: simplify_expr_int.cpp:907
simplify_string_index_of
static simplify_exprt::resultt simplify_string_index_of(const function_application_exprt &expr, const namespacet &ns, const bool search_from_end)
Simplify String.indexOf function when arguments are constant.
Definition: simplify_expr.cpp:351
typet::subtype
const typet & subtype() const
Definition: type.h:47
simplify_exprt::simplify_dereference
resultt simplify_dereference(const dereference_exprt &)
Definition: simplify_expr.cpp:1328
simplify_exprt::simplify_concatenation
resultt simplify_concatenation(const concatenation_exprt &)
Definition: simplify_expr_int.cpp:805
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
to_lambda_expr
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
Definition: mathematical_expr.h:446
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1113
simplify_expr_class.h
fixedbvt::from_integer
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:78
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
count_trailing_zeros_exprt
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Definition: bitvector_expr.h:924
simplify_exprt::simplify_address_of
resultt simplify_address_of(const address_of_exprt &)
Definition: simplify_expr_pointer.cpp:210
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:49
rational.h
simplify_exprt::simplify_unary_plus
resultt simplify_unary_plus(const unary_plus_exprt &)
Definition: simplify_expr_int.cpp:1112
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
simplify_exprt::simplify_bitwise
resultt simplify_bitwise(const multi_ary_exprt &)
Definition: simplify_expr_int.cpp:600
rational_tools.h
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:350
ieee_floatt::set_sign
void set_sign(bool _sign)
Definition: ieee_float.h:184
simplify_exprt::simplify_if_preorder
bool simplify_if_preorder(if_exprt &expr)
Definition: simplify_expr_if.cpp:214
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
array_of_exprt::what
exprt & what()
Definition: std_expr.h:1419
irept::make_nil
void make_nil()
Definition: irep.h:465
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
simplify_exprt::simplify_bitnot
resultt simplify_bitnot(const bitnot_exprt &)
Definition: simplify_expr_int.cpp:1179
to_string_expr
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:150
typet
The type of an expression, extends irept.
Definition: type.h:28
update_exprt::old
exprt & old()
Definition: std_expr.h:2454
simplify_exprt::simplify_overflow_binary
resultt simplify_overflow_binary(const binary_overflow_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
Definition: simplify_expr.cpp:2173
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
fixedbvt::to_integer
mp_integer to_integer() const
Definition: fixedbv.cpp:37
union_typet::find_widest_union_component
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
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
bits2expr
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
Definition: simplify_utils.cpp:193
simplify_string_endswith
static simplify_exprt::resultt simplify_string_endswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.endsWith function when arguments are constant.
Definition: simplify_expr.cpp:204
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:628
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
byte_update_exprt::offset
const exprt & offset() const
Definition: byte_operators.h:106
simplify_exprt::simplify_popcount
resultt simplify_popcount(const popcount_exprt &)
Definition: simplify_expr.cpp:125
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: bitvector_types.h:322
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
simplify_exprt::simplify
virtual bool simplify(exprt &expr)
Definition: simplify_expr.cpp:2633
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:277
simplify_exprt::simplify_is_dynamic_object
resultt simplify_is_dynamic_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:552
fixedbv_spect::get_fraction_bits
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
with_exprt::new_value
exprt & new_value()
Definition: std_expr.h:2288
fixedbv.h
simplify_string_char_at
static simplify_exprt::resultt simplify_string_char_at(const function_application_exprt &expr, const namespacet &ns)
Simplify String.charAt function when arguments are constant.
Definition: simplify_expr.cpp:496
s1
int8_t s1
Definition: bytecode_info.h:59
simplify_exprt::simplify_clz
resultt simplify_clz(const count_leading_zeros_exprt &)
Try to simplify count-leading-zeros to a constant expression.
Definition: simplify_expr.cpp:151
union_exprt
Union constructor from single element.
Definition: std_expr.h:1602
simplify_exprt::simplify_update
resultt simplify_update(const update_exprt &)
Definition: simplify_expr.cpp:1471
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1447
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:914
simplify_exprt::simplify_boolean
resultt simplify_boolean(const exprt &)
Definition: simplify_expr_boolean.cpp:17
ieee_floatt::change_spec
void change_spec(const ieee_float_spect &dest_spec)
Definition: ieee_float.cpp:1048
simplify_exprt::simplify_overflow_unary
resultt simplify_overflow_unary(const unary_overflow_exprt &)
Try to simplify overflow-unary-.
Definition: simplify_expr.cpp:2236
simplify_string_compare_to
static simplify_exprt::resultt simplify_string_compare_to(const function_application_exprt &expr, const namespacet &ns)
Simplify String.compareTo function when arguments are constant.
Definition: simplify_expr.cpp:302
count_trailing_zeros_exprt::zero_permitted
bool zero_permitted() const
Definition: bitvector_expr.h:937
simplify_string_equals_ignore_case
static simplify_exprt::resultt simplify_string_equals_ignore_case(const function_application_exprt &expr, const namespacet &ns)
Simplify String.equalsIgnorecase function when arguments are constant.
Definition: simplify_expr.cpp:564
exprt
Base class for all expressions.
Definition: expr.h:54
simplify_exprt::simplify_ctz
resultt simplify_ctz(const count_trailing_zeros_exprt &)
Try to simplify count-trailing-zeros to a constant expression.
Definition: simplify_expr.cpp:177
to_complex_expr
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1756
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:140
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
simplify_exprt::simplify_extractbit
resultt simplify_extractbit(const extractbit_exprt &)
Definition: simplify_expr_int.cpp:776
to_bv_type
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: bitvector_types.h:82
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
byte_update_exprt::set_op
void set_op(exprt e)
Definition: byte_operators.h:92
sign_exprt
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:506
exprt::op0
exprt & op0()
Definition: expr.h:99
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
to_bitnot_expr
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: bitvector_expr.h:106
lift_if
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:199
can_cast_expr< refined_string_exprt >
bool can_cast_expr< refined_string_exprt >(const exprt &base)
Definition: string_expr.h:165
ieee_floatt::to_integer
mp_integer to_integer() const
Definition: ieee_float.cpp:1073
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
simplify_exprt::simplify_complex
resultt simplify_complex(const unary_exprt &)
Definition: simplify_expr.cpp:2152
simplify_exprt::simplify_pointer_offset
resultt simplify_pointer_offset(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:248
configt::ansi_c
struct configt::ansi_ct ansi_c
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
try_get_string_data_array
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)
Get char sequence from content field of a refined string expression.
Definition: simplify_utils.cpp:480
simplify_exprt::simplify_plus
resultt simplify_plus(const plus_exprt &)
Definition: simplify_expr_int.cpp:402
namespace.h
struct_union_typet::component_number
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:32
from_rational
constant_exprt from_rational(const rationalt &a)
Definition: rational_tools.cpp:81
fixedbvt::to_expr
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
to_popcount_expr
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: bitvector_expr.h:667
simplify_exprt::simplify_byte_extract
resultt simplify_byte_extract(const byte_extract_exprt &)
Definition: simplify_expr.cpp:1599
simplify_exprt::simplify_not
resultt simplify_not(const not_exprt &)
Definition: simplify_expr_boolean.cpp:162
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
simplify_exprt::unchanged
static resultt unchanged(exprt expr)
Definition: simplify_expr_class.h:130
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2209
simplify_exprt::simplify_node
resultt simplify_node(exprt)
Definition: simplify_expr.cpp:2314
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: bitvector_types.h:159
refined_string_exprt
Definition: string_expr.h:109
refined_string_exprt::length
const exprt & length() const
Definition: string_expr.h:128
to_floatbv_typecast_expr
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: bitvector_types.h:305
ieee_float_spect
Definition: ieee_float.h:23
to_unary_plus_expr
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:464
to_complex_real_expr
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1801
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
to_bswap_expr
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: bitvector_expr.h:63
simplify_exprt::simplify_if
resultt simplify_if(const if_exprt &)
Definition: simplify_expr_if.cpp:330
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1668
c_bool_typet
The C/C++ Booleans.
Definition: c_types.h:62
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
complex_exprt::imag
exprt imag()
Definition: std_expr.h:1728
simplify_string_startswith
static simplify_exprt::resultt simplify_string_startswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.startsWith function when arguments are constant.
Definition: simplify_expr.cpp:609
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
simplify_exprt::simplify_minus
resultt simplify_minus(const minus_exprt &)
Definition: simplify_expr_int.cpp:558
count_leading_zeros_exprt::zero_permitted
bool zero_permitted() const
Definition: bitvector_expr.h:844
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
@ IS_LITTLE_ENDIAN
with_exprt::old
exprt & old()
Definition: std_expr.h:2268
byte_operators.h
Expression classes for byte-level operators.
simplify_exprt::simplify_power
resultt simplify_power(const binary_exprt &)
Definition: simplify_expr_int.cpp:1015
simplify_exprt::simplify_div
resultt simplify_div(const div_exprt &)
Definition: simplify_expr_int.cpp:271
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
simplify_exprt::simplify_typecast
resultt simplify_typecast(const typecast_exprt &)
Definition: simplify_expr.cpp:732
base_type
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1160
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1044
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:703
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
simplify_exprt::simplify_mod
resultt simplify_mod(const mod_exprt &)
Definition: simplify_expr_int.cpp:365
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
failed
static bool failed(bool error_indicator)
Definition: symtab2gb_parse_options.cpp:37
simplify_exprt::simplify_isnan
resultt simplify_isnan(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:37
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:317
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:117
binary_overflow_exprt
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
Definition: bitvector_expr.h:687
simplify_exprt::changed
static resultt changed(resultt<> result)
Definition: simplify_expr_class.h:135
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
has_subtype
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Definition: expr_util.cpp:151
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:641
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:101
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: bitvector_types.h:208
pointer_offset_sum
exprt pointer_offset_sum(const exprt &a, const exprt &b)
Definition: pointer_offset_sum.cpp:16
join_operands
bool join_operands(exprt &expr)
Definition: simplify_utils.cpp:188
simplify_exprt::simplify_bswap
resultt simplify_bswap(const bswap_exprt &)
Definition: simplify_expr_int.cpp:29
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
pointer_expr.h
API to expression classes for Pointers.
simplify_exprt::simplify_node_preorder
bool simplify_node_preorder(exprt &expr)
Definition: simplify_expr.cpp:2283
integer_bitvector_typet
Fixed-width bit-vector representing a signed or unsigned integer.
Definition: bitvector_types.h:99
to_unary_overflow_expr
const unary_overflow_exprt & to_unary_overflow_expr(const exprt &expr)
Cast an exprt to a unary_overflow_exprt.
Definition: bitvector_expr.h:807
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2654
exprt::op1
exprt & op1()
Definition: expr.h:102
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:192
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2659
simplify_exprt::simplify_inequality
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
Definition: simplify_expr_int.cpp:1210
index_exprt::index
exprt & index()
Definition: std_expr.h:1354
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
ieee_floatt::pack
mp_integer pack() const
Definition: ieee_float.cpp:374
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
simplify_exprt
Definition: simplify_expr_class.h:74
index_exprt::array
exprt & array()
Definition: std_expr.h:1344
irept::swap
void swap(irept &irep)
Definition: irep.h:453
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
struct_union_typet::has_component
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
simplify_exprt::simplify_good_pointer
resultt simplify_good_pointer(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:692
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
dstringt::empty
bool empty() const
Definition: dstring.h:88
abs_exprt
Absolute value.
Definition: std_expr.h:346
simplify_string_contains
static simplify_exprt::resultt simplify_string_contains(const function_application_exprt &expr, const namespacet &ns)
Simplify String.contains function when arguments are constant.
Definition: simplify_expr.cpp:232
to_count_trailing_zeros_expr
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
Definition: bitvector_expr.h:992
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
floatbv_expr.h
API to expression classes for floating-point arithmetic.
union_typet
The union type.
Definition: c_types.h:112
simplify_exprt::simplify_mult
resultt simplify_mult(const mult_exprt &)
Definition: simplify_expr_int.cpp:159
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
fixedbvt::set_value
void set_value(const mp_integer &_v)
Definition: fixedbv.h:96
simplify_exprt::simplify_with
resultt simplify_with(const with_exprt &)
Definition: simplify_expr.cpp:1391
simplify_exprt::resultt
Definition: simplify_expr_class.h:97
simplify_exprt::simplify_unary_minus
resultt simplify_unary_minus(const unary_minus_exprt &)
Definition: simplify_expr_int.cpp:1119
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:515
to_complex_imag_expr
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1846
simplify_exprt::simplify_function_application
resultt simplify_function_application(const function_application_exprt &)
Attempt to simplify mathematical function applications if we have enough information to do so.
Definition: simplify_expr.cpp:675
simplify_exprt::simplify_pointer_object
resultt simplify_pointer_object(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:520
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: bitvector_expr.h:278
fixedbv_spect
Definition: fixedbv.h:20
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2320
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2442
update_exprt::designator
exprt::operandst & designator()
Definition: std_expr.h:2468
simplify_exprt::simplify_index
resultt simplify_index(const index_exprt &)
Definition: simplify_expr_array.cpp:19
config
configt config
Definition: config.cpp:25
ieee_floatt::spec
ieee_float_spect spec
Definition: ieee_float.h:135
expr2bits
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
Definition: simplify_utils.cpp:405
fixedbv_typet
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: bitvector_types.h:261
to_binary_overflow_expr
const binary_overflow_exprt & to_binary_overflow_expr(const exprt &expr)
Cast an exprt to a binary_overflow_exprt.
Definition: bitvector_expr.h:741
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:843
to_ieee_float_op_expr
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: floatbv_expr.h:425
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:44
to_concatenation_expr
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: bitvector_expr.h:618
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2613
simplify_exprt::simplify_member
resultt simplify_member(const member_exprt &)
Definition: simplify_expr_struct.cpp:21
expr_util.h
Deprecated expression utility functions.
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:401
unary_overflow_exprt
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Definition: bitvector_expr.h:766
refined_string_exprt::content
const exprt & content() const
Definition: string_expr.h:138
format_expr.h
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:479
simplify_exprt::simplify_object
resultt simplify_object(const exprt &)
Definition: simplify_expr.cpp:1519
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:231
byte_update_exprt::value
const exprt & value() const
Definition: byte_operators.h:107
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:292
pointer_offset_size
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Definition: pointer_offset_size.cpp:90
array_typet
Arrays with given size.
Definition: std_types.h:763
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2199
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
@ IS_BIG_ENDIAN
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
to_sign_expr
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:531
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2152
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
is_not_zero
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:96
update_exprt::new_value
exprt & new_value()
Definition: std_expr.h:2478
function_application_exprt::function
exprt & function()
Definition: mathematical_expr.h:200
lambda_exprt
A (mathematical) lambda expression.
Definition: mathematical_expr.h:407
simplify_exprt::simplify_sign
resultt simplify_sign(const sign_exprt &)
Definition: simplify_expr.cpp:99
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
get_subexpression_at_offset
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
Definition: pointer_offset_size.cpp:606
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2189
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
invariant.h
fixedbvt::round
void round(const fixedbv_spect &dest_spec)
Definition: fixedbv.cpp:52
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
fixedbvt::spec
fixedbv_spect spec
Definition: fixedbv.h:44
simplify_exprt::simplify_lambda
resultt simplify_lambda(const lambda_exprt &)
Definition: simplify_expr.cpp:1386
config.h
fixedbvt
Definition: fixedbv.h:42
to_extractbits_expr
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: bitvector_expr.h:499
simplify_exprt::simplify_extractbits
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
Definition: simplify_expr_int.cpp:1036
simplify_exprt::ns
const namespacet & ns
Definition: simplify_expr_class.h:248
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
irep_full_eq
Definition: irep.h:506
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
make_boolean_expr
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:281
ieee_floatt::get_sign
bool get_sign() const
Definition: ieee_float.h:248
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
exprt::operands
operandst & operands()
Definition: expr.h:92
simplify_exprt::simplify_byte_update
resultt simplify_byte_update(const byte_update_exprt &)
Definition: simplify_expr.cpp:1844
r
static int8_t r
Definition: irep_hash.h:60
index_exprt
Array index operator.
Definition: std_expr.h:1328
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:235
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: bitvector_expr.h:633
s2
int16_t s2
Definition: bytecode_info.h:60
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
constant_exprt
A constant literal expression.
Definition: std_expr.h:2753
pointer_offset_sum.h
Pointer Dereferencing.
simplify_exprt::simplify_object_size
resultt simplify_object_size(const unary_exprt &)
Definition: simplify_expr_pointer.cpp:644
simplify_exprt::simplify_abs
resultt simplify_abs(const abs_exprt &)
Definition: simplify_expr.cpp:65
member_offset_expr
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Definition: pointer_offset_size.cpp:220
binary_exprt::op1
exprt & op1()
Definition: expr.h:102
simplify_utils.h
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
std_expr.h
API to expression classes.
string_expr.h
String expressions for the string solver.
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
constant_exprt::set_value
void set_value(const irep_idt &value)
Definition: std_expr.h:2766
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2761
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:230
with_exprt::where
exprt & where()
Definition: std_expr.h:2278
lambda_exprt::application
exprt application(const operandst &arguments) const
Definition: mathematical_expr.h:423
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:24
byte_update_exprt::op
const exprt & op() const
Definition: byte_operators.h:105
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1467
simplify_exprt::simplify_ieee_float_relation
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
Definition: simplify_expr_floatbv.cpp:338
c_types.h
rationalt
Definition: rational.h:16
to_function_application_expr
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: mathematical_expr.h:242
irep_full_hash
Definition: irep.h:497
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:156
complex_exprt::real
exprt real()
Definition: std_expr.h:1718
to_count_leading_zeros_expr
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
Definition: bitvector_expr.h:899
bitvector_expr.h
API to expression classes for bitvectors.
binary_exprt::op0
exprt & op0()
Definition: expr.h:99
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1691
simplify_exprt::simplify_floatbv_typecast
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
Definition: simplify_expr_floatbv.cpp:139
to_abs_expr
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:370
get_bvrep_bit
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
Definition: arith_tools.cpp:261
count_leading_zeros_exprt
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
Definition: bitvector_expr.h:831
byte_update_exprt::set_offset
void set_offset(exprt e)
Definition: byte_operators.h:96
lower_case_string_expression
static bool lower_case_string_expression(array_exprt &string_data)
Take the passed-in constant string array and lower-case every character.
Definition: simplify_expr.cpp:536
simplify_exprt::simplify_floatbv_op
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
Definition: simplify_expr_floatbv.cpp:273
to_index_designator
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2373
simplify_string_is_empty
static simplify_exprt::resultt simplify_string_is_empty(const function_application_exprt &expr, const namespacet &ns)
Simplify String.isEmpty function when arguments are constant.
Definition: simplify_expr.cpp:277
mathematical_expr.h
API to expression classes for 'mathematical' expressions.
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
simplify_exprt::simplify_isinf
resultt simplify_isinf(const unary_exprt &)
Definition: simplify_expr_floatbv.cpp:23