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 =
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 =
961 
962  if(step.has_value() && *step != 0)
963  {
964  const typet size_t_type(size_type());
965  auto new_expr = expr;
966 
967  new_expr.op().type() = size_t_type;
968 
969  for(auto &op : new_expr.op().operands())
970  {
971  exprt new_op = simplify_typecast(typecast_exprt(op, size_t_type));
972  if(op.type().id() != ID_pointer && *step > 1)
973  {
974  new_op =
975  simplify_mult(mult_exprt(from_integer(*step, size_t_type), new_op));
976  }
977  op = std::move(new_op);
978  }
979 
980  new_expr.op() = simplify_plus(to_plus_expr(new_expr.op()));
981 
982  return changed(simplify_typecast(new_expr)); // recursive call
983  }
984  }
985 
986  #if 0
987  // (T)(a?b:c) --> a?(T)b:(T)c
988  if(expr.op().id()==ID_if &&
989  expr.op().operands().size()==3)
990  {
991  typecast_exprt tmp_op1(expr.op().op1(), expr_type);
992  typecast_exprt tmp_op2(expr.op().op2(), expr_type);
993  simplify_typecast(tmp_op1);
994  simplify_typecast(tmp_op2);
995  auto new_expr=if_exprt(expr.op().op0(), tmp_op1, tmp_op2, expr_type);
996  simplify_if(new_expr);
997  return std::move(new_expr);
998  }
999  #endif
1000 
1001  const irep_idt &expr_type_id=expr_type.id();
1002  const exprt &operand = expr.op();
1003  const irep_idt &op_type_id=op_type.id();
1004 
1005  if(operand.is_constant())
1006  {
1007  const irep_idt &value=to_constant_expr(operand).get_value();
1008 
1009  // preserve the sizeof type annotation
1010  typet c_sizeof_type=
1011  static_cast<const typet &>(operand.find(ID_C_c_sizeof_type));
1012 
1013  if(op_type_id==ID_integer ||
1014  op_type_id==ID_natural)
1015  {
1016  // from integer to ...
1017 
1018  mp_integer int_value=string2integer(id2string(value));
1019 
1020  if(expr_type_id==ID_bool)
1021  {
1022  return make_boolean_expr(int_value != 0);
1023  }
1024 
1025  if(expr_type_id==ID_unsignedbv ||
1026  expr_type_id==ID_signedbv ||
1027  expr_type_id==ID_c_enum ||
1028  expr_type_id==ID_c_bit_field ||
1029  expr_type_id==ID_integer)
1030  {
1031  return from_integer(int_value, expr_type);
1032  }
1033  else if(expr_type_id == ID_c_enum_tag)
1034  {
1035  const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
1036  if(!c_enum_type.is_incomplete()) // possibly incomplete
1037  {
1038  exprt tmp = from_integer(int_value, c_enum_type);
1039  tmp.type() = expr_type; // we maintain the tag type
1040  return std::move(tmp);
1041  }
1042  }
1043  }
1044  else if(op_type_id==ID_rational)
1045  {
1046  }
1047  else if(op_type_id==ID_real)
1048  {
1049  }
1050  else if(op_type_id==ID_bool)
1051  {
1052  if(expr_type_id==ID_unsignedbv ||
1053  expr_type_id==ID_signedbv ||
1054  expr_type_id==ID_integer ||
1055  expr_type_id==ID_natural ||
1056  expr_type_id==ID_rational ||
1057  expr_type_id==ID_c_bool ||
1058  expr_type_id==ID_c_enum ||
1059  expr_type_id==ID_c_bit_field)
1060  {
1061  if(operand.is_true())
1062  {
1063  return from_integer(1, expr_type);
1064  }
1065  else if(operand.is_false())
1066  {
1067  return from_integer(0, expr_type);
1068  }
1069  }
1070  else if(expr_type_id==ID_c_enum_tag)
1071  {
1072  const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
1073  if(!c_enum_type.is_incomplete()) // possibly incomplete
1074  {
1075  unsigned int_value = operand.is_true() ? 1u : 0u;
1076  exprt tmp=from_integer(int_value, c_enum_type);
1077  tmp.type()=expr_type; // we maintain the tag type
1078  return std::move(tmp);
1079  }
1080  }
1081  else if(expr_type_id==ID_pointer &&
1082  operand.is_false() &&
1084  {
1085  return null_pointer_exprt(to_pointer_type(expr_type));
1086  }
1087  }
1088  else if(op_type_id==ID_unsignedbv ||
1089  op_type_id==ID_signedbv ||
1090  op_type_id==ID_c_bit_field ||
1091  op_type_id==ID_c_bool)
1092  {
1093  mp_integer int_value;
1094 
1095  if(to_integer(to_constant_expr(operand), int_value))
1096  return unchanged(expr);
1097 
1098  if(expr_type_id==ID_bool)
1099  {
1100  return make_boolean_expr(int_value != 0);
1101  }
1102 
1103  if(expr_type_id==ID_c_bool)
1104  {
1105  return from_integer(int_value != 0, expr_type);
1106  }
1107 
1108  if(expr_type_id==ID_integer)
1109  {
1110  return from_integer(int_value, expr_type);
1111  }
1112 
1113  if(expr_type_id==ID_natural)
1114  {
1115  if(int_value>=0)
1116  {
1117  return from_integer(int_value, expr_type);
1118  }
1119  }
1120 
1121  if(expr_type_id==ID_unsignedbv ||
1122  expr_type_id==ID_signedbv ||
1123  expr_type_id==ID_bv ||
1124  expr_type_id==ID_c_bit_field)
1125  {
1126  auto result = from_integer(int_value, expr_type);
1127 
1128  if(c_sizeof_type.is_not_nil())
1129  result.set(ID_C_c_sizeof_type, c_sizeof_type);
1130 
1131  return std::move(result);
1132  }
1133 
1134  if(expr_type_id==ID_c_enum_tag)
1135  {
1136  const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
1137  if(!c_enum_type.is_incomplete()) // possibly incomplete
1138  {
1139  exprt tmp=from_integer(int_value, c_enum_type);
1140  tmp.type()=expr_type; // we maintain the tag type
1141  return std::move(tmp);
1142  }
1143  }
1144 
1145  if(expr_type_id==ID_c_enum)
1146  {
1147  return from_integer(int_value, expr_type);
1148  }
1149 
1150  if(expr_type_id==ID_fixedbv)
1151  {
1152  // int to float
1153  const fixedbv_typet &f_expr_type=
1154  to_fixedbv_type(expr_type);
1155 
1156  fixedbvt f;
1157  f.spec=fixedbv_spect(f_expr_type);
1158  f.from_integer(int_value);
1159  return f.to_expr();
1160  }
1161 
1162  if(expr_type_id==ID_floatbv)
1163  {
1164  // int to float
1165  const floatbv_typet &f_expr_type=
1166  to_floatbv_type(expr_type);
1167 
1168  ieee_floatt f(f_expr_type);
1169  f.from_integer(int_value);
1170 
1171  return f.to_expr();
1172  }
1173 
1174  if(expr_type_id==ID_rational)
1175  {
1176  rationalt r(int_value);
1177  return from_rational(r);
1178  }
1179  }
1180  else if(op_type_id==ID_fixedbv)
1181  {
1182  if(expr_type_id==ID_unsignedbv ||
1183  expr_type_id==ID_signedbv)
1184  {
1185  // cast from fixedbv to int
1186  fixedbvt f(to_constant_expr(expr.op()));
1187  return from_integer(f.to_integer(), expr_type);
1188  }
1189  else if(expr_type_id==ID_fixedbv)
1190  {
1191  // fixedbv to fixedbv
1192  fixedbvt f(to_constant_expr(expr.op()));
1193  f.round(fixedbv_spect(to_fixedbv_type(expr_type)));
1194  return f.to_expr();
1195  }
1196  else if(expr_type_id == ID_bv)
1197  {
1198  fixedbvt f{to_constant_expr(expr.op())};
1199  return from_integer(f.get_value(), expr_type);
1200  }
1201  }
1202  else if(op_type_id==ID_floatbv)
1203  {
1204  ieee_floatt f(to_constant_expr(expr.op()));
1205 
1206  if(expr_type_id==ID_unsignedbv ||
1207  expr_type_id==ID_signedbv)
1208  {
1209  // cast from float to int
1210  return from_integer(f.to_integer(), expr_type);
1211  }
1212  else if(expr_type_id==ID_floatbv)
1213  {
1214  // float to double or double to float
1216  return f.to_expr();
1217  }
1218  else if(expr_type_id==ID_fixedbv)
1219  {
1220  fixedbvt fixedbv;
1221  fixedbv.spec=fixedbv_spect(to_fixedbv_type(expr_type));
1222  ieee_floatt factor(f.spec);
1223  factor.from_integer(power(2, fixedbv.spec.get_fraction_bits()));
1224  f*=factor;
1225  fixedbv.set_value(f.to_integer());
1226  return fixedbv.to_expr();
1227  }
1228  else if(expr_type_id == ID_bv)
1229  {
1230  return from_integer(f.pack(), expr_type);
1231  }
1232  }
1233  else if(op_type_id==ID_bv)
1234  {
1235  if(
1236  expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1237  expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
1238  expr_type_id == ID_c_bit_field)
1239  {
1240  const auto width = to_bv_type(op_type).get_width();
1241  const auto int_value = bvrep2integer(value, width, false);
1242  if(expr_type_id != ID_c_enum_tag)
1243  return from_integer(int_value, expr_type);
1244  else
1245  {
1246  c_enum_tag_typet tag_type = to_c_enum_tag_type(expr_type);
1247  auto result = from_integer(int_value, ns.follow_tag(tag_type));
1248  result.type() = tag_type;
1249  return std::move(result);
1250  }
1251  }
1252  else if(expr_type_id == ID_floatbv)
1253  {
1254  const auto width = to_bv_type(op_type).get_width();
1255  const auto int_value = bvrep2integer(value, width, false);
1256  ieee_floatt ieee_float{to_floatbv_type(expr_type)};
1257  ieee_float.unpack(int_value);
1258  return ieee_float.to_expr();
1259  }
1260  else if(expr_type_id == ID_fixedbv)
1261  {
1262  const auto width = to_bv_type(op_type).get_width();
1263  const auto int_value = bvrep2integer(value, width, false);
1264  fixedbvt fixedbv{fixedbv_spect{to_fixedbv_type(expr_type)}};
1265  fixedbv.set_value(int_value);
1266  return fixedbv.to_expr();
1267  }
1268  }
1269  else if(op_type_id==ID_c_enum_tag) // enum to int
1270  {
1271  const typet &base_type =
1272  ns.follow_tag(to_c_enum_tag_type(op_type)).underlying_type();
1273  if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv)
1274  {
1275  // enum constants use the representation of their base type
1276  auto new_expr = expr;
1277  new_expr.op().type() = base_type;
1278  return changed(simplify_typecast(new_expr)); // recursive call
1279  }
1280  }
1281  else if(op_type_id==ID_c_enum) // enum to int
1282  {
1283  const typet &base_type = to_c_enum_type(op_type).underlying_type();
1284  if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv)
1285  {
1286  // enum constants use the representation of their base type
1287  auto new_expr = expr;
1288  new_expr.op().type() = base_type;
1289  return changed(simplify_typecast(new_expr)); // recursive call
1290  }
1291  }
1292  }
1293  else if(operand.id()==ID_typecast) // typecast of typecast
1294  {
1295  // (T1)(T2)x ---> (T1)
1296  // where T1 has fewer bits than T2
1297  if(
1298  op_type_id == expr_type_id &&
1299  (expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv) &&
1300  to_bitvector_type(expr_type).get_width() <=
1301  to_bitvector_type(operand.type()).get_width())
1302  {
1303  auto new_expr = expr;
1304  new_expr.op() = to_typecast_expr(operand).op();
1305  // might enable further simplification
1306  return changed(simplify_typecast(new_expr)); // recursive call
1307  }
1308  }
1309  else if(operand.id()==ID_address_of)
1310  {
1311  const exprt &o=to_address_of_expr(operand).object();
1312 
1313  // turn &array into &array[0] when casting to pointer-to-element-type
1314  if(
1315  o.type().id() == ID_array &&
1316  expr_type == pointer_type(to_array_type(o.type()).element_type()))
1317  {
1318  auto result =
1320 
1321  return changed(simplify_address_of(result)); // recursive call
1322  }
1323  }
1324 
1325  return unchanged(expr);
1326 }
1327 
1330 {
1331  const exprt &pointer = expr.pointer();
1332 
1333  if(pointer.type().id()!=ID_pointer)
1334  return unchanged(expr);
1335 
1336  if(pointer.id()==ID_if && pointer.operands().size()==3)
1337  {
1338  const if_exprt &if_expr=to_if_expr(pointer);
1339 
1340  auto tmp_op1 = expr;
1341  tmp_op1.op() = if_expr.true_case();
1342  exprt tmp_op1_result = simplify_dereference(tmp_op1);
1343 
1344  auto tmp_op2 = expr;
1345  tmp_op2.op() = if_expr.false_case();
1346  exprt tmp_op2_result = simplify_dereference(tmp_op2);
1347 
1348  if_exprt tmp{if_expr.cond(), tmp_op1_result, tmp_op2_result};
1349 
1350  return changed(simplify_if(tmp));
1351  }
1352 
1353  if(pointer.id()==ID_address_of)
1354  {
1355  exprt tmp=to_address_of_expr(pointer).object();
1356  // one address_of is gone, try again
1357  return changed(simplify_rec(tmp));
1358  }
1359  // rewrite *(&a[0] + x) to a[x]
1360  else if(
1361  pointer.id() == ID_plus && pointer.operands().size() == 2 &&
1362  to_plus_expr(pointer).op0().id() == ID_address_of)
1363  {
1364  const auto &pointer_plus_expr = to_plus_expr(pointer);
1365 
1366  const address_of_exprt &address_of =
1367  to_address_of_expr(pointer_plus_expr.op0());
1368 
1369  if(address_of.object().id()==ID_index)
1370  {
1371  const index_exprt &old=to_index_expr(address_of.object());
1372  if(old.array().type().id() == ID_array)
1373  {
1374  index_exprt idx(
1375  old.array(),
1376  pointer_offset_sum(old.index(), pointer_plus_expr.op1()),
1377  to_array_type(old.array().type()).element_type());
1378  return changed(simplify_rec(idx));
1379  }
1380  }
1381  }
1382 
1383  return unchanged(expr);
1384 }
1385 
1388 {
1389  return unchanged(expr);
1390 }
1391 
1393 {
1394  bool no_change = true;
1395 
1396  if((expr.operands().size()%2)!=1)
1397  return unchanged(expr);
1398 
1399  // copy
1400  auto with_expr = expr;
1401 
1402  const typet old_type_followed = ns.follow(with_expr.old().type());
1403 
1404  // now look at first operand
1405 
1406  if(old_type_followed.id() == ID_struct)
1407  {
1408  if(with_expr.old().id() == ID_struct || with_expr.old().id() == ID_constant)
1409  {
1410  while(with_expr.operands().size() > 1)
1411  {
1412  const irep_idt &component_name =
1413  with_expr.where().get(ID_component_name);
1414 
1415  if(!to_struct_type(old_type_followed).has_component(component_name))
1416  return unchanged(expr);
1417 
1418  std::size_t number =
1419  to_struct_type(old_type_followed).component_number(component_name);
1420 
1421  if(number >= with_expr.old().operands().size())
1422  return unchanged(expr);
1423 
1424  with_expr.old().operands()[number].swap(with_expr.new_value());
1425 
1426  with_expr.operands().erase(++with_expr.operands().begin());
1427  with_expr.operands().erase(++with_expr.operands().begin());
1428 
1429  no_change = false;
1430  }
1431  }
1432  }
1433  else if(
1434  with_expr.old().type().id() == ID_array ||
1435  with_expr.old().type().id() == ID_vector)
1436  {
1437  if(
1438  with_expr.old().id() == ID_array || with_expr.old().id() == ID_constant ||
1439  with_expr.old().id() == ID_vector)
1440  {
1441  while(with_expr.operands().size() > 1)
1442  {
1443  const auto i = numeric_cast<mp_integer>(with_expr.where());
1444 
1445  if(!i.has_value())
1446  break;
1447 
1448  if(*i < 0 || *i >= with_expr.old().operands().size())
1449  break;
1450 
1451  with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
1452  with_expr.new_value());
1453 
1454  with_expr.operands().erase(++with_expr.operands().begin());
1455  with_expr.operands().erase(++with_expr.operands().begin());
1456 
1457  no_change = false;
1458  }
1459  }
1460  }
1461 
1462  if(with_expr.operands().size() == 1)
1463  return with_expr.old();
1464 
1465  if(no_change)
1466  return unchanged(expr);
1467  else
1468  return std::move(with_expr);
1469 }
1470 
1473 {
1474  // this is to push updates into (possibly nested) constants
1475 
1476  const exprt::operandst &designator = expr.designator();
1477 
1478  exprt updated_value = expr.old();
1479  exprt *value_ptr=&updated_value;
1480 
1481  for(const auto &e : designator)
1482  {
1483  const typet &value_ptr_type=ns.follow(value_ptr->type());
1484 
1485  if(e.id()==ID_index_designator &&
1486  value_ptr->id()==ID_array)
1487  {
1488  const auto i = numeric_cast<mp_integer>(to_index_designator(e).index());
1489 
1490  if(!i.has_value())
1491  return unchanged(expr);
1492 
1493  if(*i < 0 || *i >= value_ptr->operands().size())
1494  return unchanged(expr);
1495 
1496  value_ptr = &value_ptr->operands()[numeric_cast_v<std::size_t>(*i)];
1497  }
1498  else if(e.id()==ID_member_designator &&
1499  value_ptr->id()==ID_struct)
1500  {
1501  const irep_idt &component_name=
1502  e.get(ID_component_name);
1503  const struct_typet &value_ptr_struct_type =
1504  to_struct_type(value_ptr_type);
1505  if(!value_ptr_struct_type.has_component(component_name))
1506  return unchanged(expr);
1507  auto &designator_as_struct_expr = to_struct_expr(*value_ptr);
1508  value_ptr = &designator_as_struct_expr.component(component_name, ns);
1509  CHECK_RETURN(value_ptr->is_not_nil());
1510  }
1511  else
1512  return unchanged(expr); // give up, unknown designator
1513  }
1514 
1515  // found, done
1516  *value_ptr = expr.new_value();
1517  return updated_value;
1518 }
1519 
1521 {
1522  if(expr.id()==ID_plus)
1523  {
1524  if(expr.type().id()==ID_pointer)
1525  {
1526  // kill integers from sum
1527  for(auto &op : expr.operands())
1528  if(op.type().id() == ID_pointer)
1529  return changed(simplify_object(op)); // recursive call
1530  }
1531  }
1532  else if(expr.id()==ID_typecast)
1533  {
1534  auto const &typecast_expr = to_typecast_expr(expr);
1535  const typet &op_type = typecast_expr.op().type();
1536 
1537  if(op_type.id()==ID_pointer)
1538  {
1539  // cast from pointer to pointer
1540  return changed(simplify_object(typecast_expr.op())); // recursive call
1541  }
1542  else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
1543  {
1544  // cast from integer to pointer
1545 
1546  // We do a bit of special treatment for (TYPE *)(a+(int)&o) and
1547  // (TYPE *)(a+(int)((T*)&o+x)), which are re-written to '&o'.
1548 
1549  const exprt &casted_expr = typecast_expr.op();
1550  if(casted_expr.id() == ID_plus && casted_expr.operands().size() == 2)
1551  {
1552  const auto &plus_expr = to_plus_expr(casted_expr);
1553 
1554  const exprt &cand = plus_expr.op0().id() == ID_typecast
1555  ? plus_expr.op0()
1556  : plus_expr.op1();
1557 
1558  if(cand.id() == ID_typecast)
1559  {
1560  const auto &typecast_op = to_typecast_expr(cand).op();
1561 
1562  if(typecast_op.id() == ID_address_of)
1563  {
1564  return typecast_op;
1565  }
1566  else if(
1567  typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1568  to_plus_expr(typecast_op).op0().id() == ID_typecast &&
1569  to_typecast_expr(to_plus_expr(typecast_op).op0()).op().id() ==
1570  ID_address_of)
1571  {
1572  return to_typecast_expr(to_plus_expr(typecast_op).op0()).op();
1573  }
1574  }
1575  }
1576  }
1577  }
1578  else if(expr.id()==ID_address_of)
1579  {
1580  const auto &object = to_address_of_expr(expr).object();
1581 
1582  if(object.id() == ID_index)
1583  {
1584  // &some[i] -> &some
1585  address_of_exprt new_expr(to_index_expr(object).array());
1586  return changed(simplify_object(new_expr)); // recursion
1587  }
1588  else if(object.id() == ID_member)
1589  {
1590  // &some.f -> &some
1591  address_of_exprt new_expr(to_member_expr(object).compound());
1592  return changed(simplify_object(new_expr)); // recursion
1593  }
1594  }
1595 
1596  return unchanged(expr);
1597 }
1598 
1601 {
1602  // lift up any ID_if on the object
1603  if(expr.op().id()==ID_if)
1604  {
1605  if_exprt if_expr=lift_if(expr, 0);
1606  if_expr.true_case() =
1608  if_expr.false_case() =
1610  return changed(simplify_if(if_expr));
1611  }
1612 
1613  const auto el_size = pointer_offset_bits(expr.type(), ns);
1614  if(el_size.has_value() && *el_size < 0)
1615  return unchanged(expr);
1616 
1617  // byte_extract(byte_extract(root, offset1), offset2) =>
1618  // byte_extract(root, offset1+offset2)
1619  if(expr.op().id()==expr.id())
1620  {
1621  auto tmp = expr;
1622 
1623  tmp.offset() = simplify_plus(
1624  plus_exprt(to_byte_extract_expr(expr.op()).offset(), expr.offset()));
1625  tmp.op() = to_byte_extract_expr(expr.op()).op();
1626 
1627  return changed(simplify_byte_extract(tmp)); // recursive call
1628  }
1629 
1630  // byte_extract(byte_update(root, offset, value), offset) =>
1631  // value
1632  if(
1633  ((expr.id() == ID_byte_extract_big_endian &&
1634  expr.op().id() == ID_byte_update_big_endian) ||
1635  (expr.id() == ID_byte_extract_little_endian &&
1636  expr.op().id() == ID_byte_update_little_endian)) &&
1637  expr.offset() == to_byte_update_expr(as_const(expr).op()).offset())
1638  {
1639  const auto &op_byte_update = to_byte_update_expr(expr.op());
1640 
1641  if(expr.type() == op_byte_update.value().type())
1642  {
1643  return op_byte_update.value();
1644  }
1645  else if(
1646  el_size.has_value() &&
1647  *el_size <= pointer_offset_bits(op_byte_update.value().type(), ns))
1648  {
1649  auto tmp = expr;
1650  tmp.op() = op_byte_update.value();
1651  tmp.offset() = from_integer(0, expr.offset().type());
1652 
1653  return changed(simplify_byte_extract(tmp)); // recursive call
1654  }
1655  }
1656 
1657  // the following require a constant offset
1658  auto offset = numeric_cast<mp_integer>(expr.offset());
1659  if(!offset.has_value() || *offset < 0)
1660  return unchanged(expr);
1661 
1662  // don't do any of the following if endianness doesn't match, as
1663  // bytes need to be swapped
1664  if(
1665  *offset == 0 && ((expr.id() == ID_byte_extract_little_endian &&
1668  (expr.id() == ID_byte_extract_big_endian &&
1671  {
1672  // byte extract of full object is object
1673  if(expr.type() == expr.op().type())
1674  {
1675  return expr.op();
1676  }
1677  else if(
1678  expr.type().id() == ID_pointer && expr.op().type().id() == ID_pointer)
1679  {
1680  return typecast_exprt(expr.op(), expr.type());
1681  }
1682  }
1683 
1684  // no proper simplification for expr.type()==void
1685  // or types of unknown size
1686  if(!el_size.has_value() || *el_size == 0)
1687  return unchanged(expr);
1688 
1689  if(expr.op().id()==ID_array_of &&
1690  to_array_of_expr(expr.op()).op().id()==ID_constant)
1691  {
1692  const auto const_bits_opt = expr2bits(
1693  to_array_of_expr(expr.op()).op(),
1696  ns);
1697 
1698  if(!const_bits_opt.has_value())
1699  return unchanged(expr);
1700 
1701  std::string const_bits=const_bits_opt.value();
1702 
1703  DATA_INVARIANT(!const_bits.empty(), "bit representation must be non-empty");
1704 
1705  // double the string until we have sufficiently many bits
1706  while(mp_integer(const_bits.size()) < *offset * 8 + *el_size)
1707  const_bits+=const_bits;
1708 
1709  std::string el_bits = std::string(
1710  const_bits,
1711  numeric_cast_v<std::size_t>(*offset * 8),
1712  numeric_cast_v<std::size_t>(*el_size));
1713 
1714  auto tmp = bits2expr(
1715  el_bits, expr.type(), expr.id() == ID_byte_extract_little_endian, ns);
1716 
1717  if(tmp.has_value())
1718  return std::move(*tmp);
1719  }
1720 
1721  // in some cases we even handle non-const array_of
1722  if(
1723  expr.op().id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
1724  *el_size <=
1726  {
1727  auto tmp = expr;
1728  tmp.op() = simplify_index(index_exprt(expr.op(), expr.offset()));
1729  tmp.offset() = from_integer(0, expr.offset().type());
1730  return changed(simplify_byte_extract(tmp));
1731  }
1732 
1733  // extract bits of a constant
1734  const auto bits =
1735  expr2bits(expr.op(), expr.id() == ID_byte_extract_little_endian, ns);
1736 
1737  // make sure we don't lose bits with structs containing flexible array members
1738  const bool struct_has_flexible_array_member = has_subtype(
1739  expr.type(),
1740  [&](const typet &type) {
1741  if(type.id() != ID_struct && type.id() != ID_struct_tag)
1742  return false;
1743 
1744  const struct_typet &st = to_struct_type(ns.follow(type));
1745  const auto &comps = st.components();
1746  if(comps.empty() || comps.back().type().id() != ID_array)
1747  return false;
1748 
1749  const auto size =
1750  numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1751  return !size.has_value() || *size <= 1;
1752  },
1753  ns);
1754  if(
1755  bits.has_value() && mp_integer(bits->size()) >= *el_size + *offset * 8 &&
1756  !struct_has_flexible_array_member)
1757  {
1758  std::string bits_cut = std::string(
1759  bits.value(),
1760  numeric_cast_v<std::size_t>(*offset * 8),
1761  numeric_cast_v<std::size_t>(*el_size));
1762 
1763  auto tmp = bits2expr(
1764  bits_cut, expr.type(), expr.id() == ID_byte_extract_little_endian, ns);
1765 
1766  if(tmp.has_value())
1767  return std::move(*tmp);
1768  }
1769 
1770  // push byte extracts into struct or union expressions, just like
1771  // lower_byte_extract does (this is the same code, except recursive calls use
1772  // simplify rather than lower_byte_extract)
1773  if(expr.op().id() == ID_struct || expr.op().id() == ID_union)
1774  {
1775  if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
1776  {
1777  const struct_typet &struct_type = to_struct_type(ns.follow(expr.type()));
1778  const struct_typet::componentst &components = struct_type.components();
1779 
1780  bool failed = false;
1781  struct_exprt s({}, expr.type());
1782 
1783  for(const auto &comp : components)
1784  {
1785  auto component_bits = pointer_offset_bits(comp.type(), ns);
1786 
1787  // the next member would be misaligned, abort
1788  if(
1789  !component_bits.has_value() || *component_bits == 0 ||
1790  *component_bits % 8 != 0)
1791  {
1792  failed = true;
1793  break;
1794  }
1795 
1796  auto member_offset_opt =
1797  member_offset_expr(struct_type, comp.get_name(), ns);
1798 
1799  if(!member_offset_opt.has_value())
1800  {
1801  failed = true;
1802  break;
1803  }
1804 
1805  exprt new_offset = simplify_rec(
1806  plus_exprt{expr.offset(),
1808  member_offset_opt.value(), expr.offset().type())});
1809 
1810  byte_extract_exprt tmp = expr;
1811  tmp.type() = comp.type();
1812  tmp.offset() = new_offset;
1813 
1815  }
1816 
1817  if(!failed)
1818  return s;
1819  }
1820  else if(expr.type().id() == ID_union || expr.type().id() == ID_union_tag)
1821  {
1822  const union_typet &union_type = to_union_type(ns.follow(expr.type()));
1823  auto widest_member_opt = union_type.find_widest_union_component(ns);
1824  if(widest_member_opt.has_value())
1825  {
1826  byte_extract_exprt be = expr;
1827  be.type() = widest_member_opt->first.type();
1828  return union_exprt{widest_member_opt->first.get_name(),
1830  expr.type()};
1831  }
1832  }
1833  }
1834 
1835  // try to refine it down to extracting from a member or an index in an array
1836  auto subexpr =
1837  get_subexpression_at_offset(expr.op(), *offset, expr.type(), ns);
1838  if(!subexpr.has_value() || subexpr.value() == expr)
1839  return unchanged(expr);
1840 
1841  return changed(simplify_rec(subexpr.value())); // recursive call
1842 }
1843 
1846 {
1847  // byte_update(byte_update(root, offset, value), offset, value2) =>
1848  // byte_update(root, offset, value2)
1849  if(
1850  expr.id() == expr.op().id() &&
1851  expr.offset() == to_byte_update_expr(expr.op()).offset() &&
1852  expr.value().type() == to_byte_update_expr(expr.op()).value().type())
1853  {
1854  auto tmp = expr;
1855  tmp.set_op(to_byte_update_expr(expr.op()).op());
1856  return std::move(tmp);
1857  }
1858 
1859  const exprt &root = expr.op();
1860  const exprt &offset = expr.offset();
1861  const exprt &value = expr.value();
1862  const auto val_size = pointer_offset_bits(value.type(), ns);
1863  const auto root_size = pointer_offset_bits(root.type(), ns);
1864 
1865  // byte update of full object is byte_extract(new value)
1866  if(
1867  offset.is_zero() && val_size.has_value() && *val_size > 0 &&
1868  root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
1869  {
1870  byte_extract_exprt be(
1871  expr.id()==ID_byte_update_little_endian ?
1872  ID_byte_extract_little_endian :
1873  ID_byte_extract_big_endian,
1874  value, offset, expr.type());
1875 
1876  return changed(simplify_byte_extract(be));
1877  }
1878 
1879  // update bits in a constant
1880  const auto offset_int = numeric_cast<mp_integer>(offset);
1881  if(
1882  root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
1883  *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
1884  *offset_int * 8 + *val_size <= *root_size)
1885  {
1886  auto root_bits =
1887  expr2bits(root, expr.id() == ID_byte_update_little_endian, ns);
1888 
1889  if(root_bits.has_value())
1890  {
1891  const auto val_bits =
1892  expr2bits(value, expr.id() == ID_byte_update_little_endian, ns);
1893 
1894  if(val_bits.has_value())
1895  {
1896  root_bits->replace(
1897  numeric_cast_v<std::size_t>(*offset_int * 8),
1898  numeric_cast_v<std::size_t>(*val_size),
1899  *val_bits);
1900 
1901  auto tmp = bits2expr(
1902  *root_bits,
1903  expr.type(),
1904  expr.id() == ID_byte_update_little_endian,
1905  ns);
1906 
1907  if(tmp.has_value())
1908  return std::move(*tmp);
1909  }
1910  }
1911  }
1912 
1913  /*
1914  * byte_update(root, offset,
1915  * extract(root, offset) WITH component:=value)
1916  * =>
1917  * byte_update(root, offset + component offset,
1918  * value)
1919  */
1920 
1921  if(expr.id()!=ID_byte_update_little_endian)
1922  return unchanged(expr);
1923 
1924  if(value.id()==ID_with)
1925  {
1926  const with_exprt &with=to_with_expr(value);
1927 
1928  if(with.old().id()==ID_byte_extract_little_endian)
1929  {
1930  const byte_extract_exprt &extract=to_byte_extract_expr(with.old());
1931 
1932  /* the simplification can be used only if
1933  root and offset of update and extract
1934  are the same */
1935  if(!(root==extract.op()))
1936  return unchanged(expr);
1937  if(!(offset==extract.offset()))
1938  return unchanged(expr);
1939 
1940  const typet &tp=ns.follow(with.type());
1941  if(tp.id()==ID_struct)
1942  {
1943  const struct_typet &struct_type=to_struct_type(tp);
1944  const irep_idt &component_name=with.where().get(ID_component_name);
1945  const typet &c_type = struct_type.get_component(component_name).type();
1946 
1947  // is this a bit field?
1948  if(c_type.id() == ID_c_bit_field || c_type.id() == ID_bool)
1949  {
1950  // don't touch -- might not be byte-aligned
1951  }
1952  else
1953  {
1954  // new offset = offset + component offset
1955  auto i = member_offset(struct_type, component_name, ns);
1956  if(i.has_value())
1957  {
1958  exprt compo_offset = from_integer(*i, offset.type());
1959  plus_exprt new_offset(offset, compo_offset);
1960  exprt new_value(with.new_value());
1961  auto tmp = expr;
1962  tmp.set_offset(simplify_node(std::move(new_offset)));
1963  tmp.set_value(std::move(new_value));
1964  return changed(simplify_byte_update(tmp)); // recursive call
1965  }
1966  }
1967  }
1968  else if(tp.id()==ID_array)
1969  {
1970  auto i = pointer_offset_size(to_array_type(tp).element_type(), ns);
1971  if(i.has_value())
1972  {
1973  const exprt &index=with.where();
1974  exprt index_offset =
1975  simplify_mult(mult_exprt(index, from_integer(*i, index.type())));
1976 
1977  // index_offset may need a typecast
1978  if(offset.type() != index.type())
1979  {
1980  index_offset =
1981  simplify_typecast(typecast_exprt(index_offset, offset.type()));
1982  }
1983 
1984  plus_exprt new_offset(offset, index_offset);
1985  exprt new_value(with.new_value());
1986  auto tmp = expr;
1987  tmp.set_offset(simplify_plus(std::move(new_offset)));
1988  tmp.set_value(std::move(new_value));
1989  return changed(simplify_byte_update(tmp)); // recursive call
1990  }
1991  }
1992  }
1993  }
1994 
1995  // the following require a constant offset
1996  if(!offset_int.has_value() || *offset_int < 0)
1997  return unchanged(expr);
1998 
1999  const typet &op_type=ns.follow(root.type());
2000 
2001  // size must be known
2002  if(!val_size.has_value() || *val_size == 0)
2003  return unchanged(expr);
2004 
2005  // Are we updating (parts of) a struct? Do individual member updates
2006  // instead, unless there are non-byte-sized bit fields
2007  if(op_type.id()==ID_struct)
2008  {
2009  exprt result_expr;
2010  result_expr.make_nil();
2011 
2012  auto update_size = pointer_offset_size(value.type(), ns);
2013 
2014  const struct_typet &struct_type=
2015  to_struct_type(op_type);
2016  const struct_typet::componentst &components=
2017  struct_type.components();
2018 
2019  for(const auto &component : components)
2020  {
2021  auto m_offset = member_offset(struct_type, component.get_name(), ns);
2022 
2023  auto m_size_bits = pointer_offset_bits(component.type(), ns);
2024 
2025  // can we determine the current offset?
2026  if(!m_offset.has_value())
2027  {
2028  result_expr.make_nil();
2029  break;
2030  }
2031 
2032  // is it a byte-sized member?
2033  if(!m_size_bits.has_value() || *m_size_bits == 0 || (*m_size_bits) % 8 != 0)
2034  {
2035  result_expr.make_nil();
2036  break;
2037  }
2038 
2039  mp_integer m_size_bytes = (*m_size_bits) / 8;
2040 
2041  // is that member part of the update?
2042  if(*m_offset + m_size_bytes <= *offset_int)
2043  continue;
2044  // are we done updating?
2045  else if(
2046  update_size.has_value() && *update_size > 0 &&
2047  *m_offset >= *offset_int + *update_size)
2048  {
2049  break;
2050  }
2051 
2052  if(result_expr.is_nil())
2053  result_expr = as_const(expr).op();
2054 
2055  exprt member_name(ID_member_name);
2056  member_name.set(ID_component_name, component.get_name());
2057  result_expr=with_exprt(result_expr, member_name, nil_exprt());
2058 
2059  // are we updating on member boundaries?
2060  if(
2061  *m_offset < *offset_int ||
2062  (*m_offset == *offset_int && update_size.has_value() &&
2063  *update_size > 0 && m_size_bytes > *update_size))
2064  {
2066  ID_byte_update_little_endian,
2067  member_exprt(root, component.get_name(), component.type()),
2068  from_integer(*offset_int - *m_offset, offset.type()),
2069  value);
2070 
2071  to_with_expr(result_expr).new_value().swap(v);
2072  }
2073  else if(
2074  update_size.has_value() && *update_size > 0 &&
2075  *m_offset + m_size_bytes > *offset_int + *update_size)
2076  {
2077  // we don't handle this for the moment
2078  result_expr.make_nil();
2079  break;
2080  }
2081  else
2082  {
2084  ID_byte_extract_little_endian,
2085  value,
2086  from_integer(*m_offset - *offset_int, offset.type()),
2087  component.type());
2088 
2089  to_with_expr(result_expr).new_value().swap(v);
2090  }
2091  }
2092 
2093  if(result_expr.is_not_nil())
2094  return changed(simplify_rec(result_expr));
2095  }
2096 
2097  // replace elements of array or struct expressions, possibly using
2098  // byte_extract
2099  if(root.id()==ID_array)
2100  {
2101  auto el_size =
2102  pointer_offset_bits(to_type_with_subtype(op_type).subtype(), ns);
2103 
2104  if(!el_size.has_value() || *el_size == 0 ||
2105  (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
2106  {
2107  return unchanged(expr);
2108  }
2109 
2110  exprt result=root;
2111 
2112  mp_integer m_offset_bits=0, val_offset=0;
2113  Forall_operands(it, result)
2114  {
2115  if(*offset_int * 8 + (*val_size) <= m_offset_bits)
2116  break;
2117 
2118  if(*offset_int * 8 < m_offset_bits + *el_size)
2119  {
2120  mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
2121  bytes_req-=val_offset;
2122  if(val_offset + bytes_req > (*val_size) / 8)
2123  bytes_req = (*val_size) / 8 - val_offset;
2124 
2125  byte_extract_exprt new_val(
2126  ID_byte_extract_little_endian,
2127  value,
2128  from_integer(val_offset, offset.type()),
2129  array_typet(
2130  unsignedbv_typet(8), from_integer(bytes_req, offset.type())));
2131 
2132  *it = byte_update_exprt(
2133  expr.id(),
2134  *it,
2135  from_integer(
2136  *offset_int + val_offset - m_offset_bits / 8, offset.type()),
2137  new_val);
2138 
2139  *it = simplify_rec(*it); // recursive call
2140 
2141  val_offset+=bytes_req;
2142  }
2143 
2144  m_offset_bits += *el_size;
2145  }
2146 
2147  return std::move(result);
2148  }
2149 
2150  return unchanged(expr);
2151 }
2152 
2155 {
2156  if(expr.id() == ID_complex_real)
2157  {
2158  auto &complex_real_expr = to_complex_real_expr(expr);
2159 
2160  if(complex_real_expr.op().id() == ID_complex)
2161  return to_complex_expr(complex_real_expr.op()).real();
2162  }
2163  else if(expr.id() == ID_complex_imag)
2164  {
2165  auto &complex_imag_expr = to_complex_imag_expr(expr);
2166 
2167  if(complex_imag_expr.op().id() == ID_complex)
2168  return to_complex_expr(complex_imag_expr.op()).imag();
2169  }
2170 
2171  return unchanged(expr);
2172 }
2173 
2176 {
2177  // When one operand is zero, an overflow can only occur for a subtraction from
2178  // zero.
2179  if(
2180  expr.op1().is_zero() ||
2181  (expr.op0().is_zero() && expr.id() != ID_overflow_minus))
2182  {
2183  return false_exprt{};
2184  }
2185 
2186  // One is neutral element for multiplication
2187  if(
2188  expr.id() == ID_overflow_mult &&
2189  (expr.op0().is_one() || expr.op1().is_one()))
2190  {
2191  return false_exprt{};
2192  }
2193 
2194  // we only handle the case of same operand types
2195  if(expr.op0().type() != expr.op1().type())
2196  return unchanged(expr);
2197 
2198  // catch some cases over mathematical types
2199  const irep_idt &op_type_id = expr.op0().type().id();
2200  if(
2201  op_type_id == ID_integer || op_type_id == ID_rational ||
2202  op_type_id == ID_real)
2203  {
2204  return false_exprt{};
2205  }
2206 
2207  if(op_type_id == ID_natural && expr.id() != ID_overflow_minus)
2208  return false_exprt{};
2209 
2210  // we only handle constants over signedbv/unsignedbv for the remaining cases
2211  if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2212  return unchanged(expr);
2213 
2214  if(!expr.op0().is_constant() || !expr.op1().is_constant())
2215  return unchanged(expr);
2216 
2217  const auto op0_value = numeric_cast<mp_integer>(expr.op0());
2218  const auto op1_value = numeric_cast<mp_integer>(expr.op1());
2219  if(!op0_value.has_value() || !op1_value.has_value())
2220  return unchanged(expr);
2221 
2222  mp_integer no_overflow_result;
2223  if(expr.id() == ID_overflow_plus)
2224  no_overflow_result = *op0_value + *op1_value;
2225  else if(expr.id() == ID_overflow_minus)
2226  no_overflow_result = *op0_value - *op1_value;
2227  else if(expr.id() == ID_overflow_mult)
2228  no_overflow_result = *op0_value * *op1_value;
2229  else if(expr.id() == ID_overflow_shl)
2230  no_overflow_result = *op0_value << *op1_value;
2231  else
2232  UNREACHABLE;
2233 
2234  const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
2235  const integer_bitvector_typet bv_type{op_type_id, width};
2236  if(
2237  no_overflow_result < bv_type.smallest() ||
2238  no_overflow_result > bv_type.largest())
2239  {
2240  return true_exprt{};
2241  }
2242  else
2243  return false_exprt{};
2244 }
2245 
2248 {
2249  // zero is a neutral element for all operations supported here
2250  if(expr.op().is_zero())
2251  return false_exprt{};
2252 
2253  // catch some cases over mathematical types
2254  const irep_idt &op_type_id = expr.op().type().id();
2255  if(
2256  op_type_id == ID_integer || op_type_id == ID_rational ||
2257  op_type_id == ID_real)
2258  {
2259  return false_exprt{};
2260  }
2261 
2262  if(op_type_id == ID_natural)
2263  return true_exprt{};
2264 
2265  // we only handle constants over signedbv/unsignedbv for the remaining cases
2266  if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv)
2267  return unchanged(expr);
2268 
2269  if(!expr.op().is_constant())
2270  return unchanged(expr);
2271 
2272  const auto op_value = numeric_cast<mp_integer>(expr.op());
2273  if(!op_value.has_value())
2274  return unchanged(expr);
2275 
2276  mp_integer no_overflow_result;
2277  if(expr.id() == ID_overflow_unary_minus)
2278  no_overflow_result = -*op_value;
2279  else
2280  UNREACHABLE;
2281 
2282  const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
2283  const integer_bitvector_typet bv_type{op_type_id, width};
2284  if(
2285  no_overflow_result < bv_type.smallest() ||
2286  no_overflow_result > bv_type.largest())
2287  {
2288  return true_exprt{};
2289  }
2290  else
2291  return false_exprt{};
2292 }
2293 
2295 {
2296  bool result=true;
2297 
2298  // The ifs below could one day be replaced by a switch()
2299 
2300  if(expr.id()==ID_address_of)
2301  {
2302  // the argument of this expression needs special treatment
2303  }
2304  else if(expr.id()==ID_if)
2305  result=simplify_if_preorder(to_if_expr(expr));
2306  else
2307  {
2308  if(expr.has_operands())
2309  {
2310  Forall_operands(it, expr)
2311  {
2312  auto r_it = simplify_rec(*it); // recursive call
2313  if(r_it.has_changed())
2314  {
2315  *it = r_it.expr;
2316  result=false;
2317  }
2318  }
2319  }
2320  }
2321 
2322  return result;
2323 }
2324 
2326 {
2327  if(!node.has_operands())
2328  return unchanged(node); // no change
2329 
2330  // #define DEBUGX
2331 
2332 #ifdef DEBUGX
2333  exprt old(node);
2334 #endif
2335 
2336  exprt expr = node;
2337  bool no_change_join_operands = join_operands(expr);
2338 
2339  resultt<> r = unchanged(expr);
2340 
2341  if(expr.id()==ID_typecast)
2342  {
2344  }
2345  else if(expr.id()==ID_equal || expr.id()==ID_notequal ||
2346  expr.id()==ID_gt || expr.id()==ID_lt ||
2347  expr.id()==ID_ge || expr.id()==ID_le)
2348  {
2350  }
2351  else if(expr.id()==ID_if)
2352  {
2353  r = simplify_if(to_if_expr(expr));
2354  }
2355  else if(expr.id()==ID_lambda)
2356  {
2357  r = simplify_lambda(to_lambda_expr(expr));
2358  }
2359  else if(expr.id()==ID_with)
2360  {
2361  r = simplify_with(to_with_expr(expr));
2362  }
2363  else if(expr.id()==ID_update)
2364  {
2365  r = simplify_update(to_update_expr(expr));
2366  }
2367  else if(expr.id()==ID_index)
2368  {
2369  r = simplify_index(to_index_expr(expr));
2370  }
2371  else if(expr.id()==ID_member)
2372  {
2373  r = simplify_member(to_member_expr(expr));
2374  }
2375  else if(expr.id()==ID_byte_update_little_endian ||
2376  expr.id()==ID_byte_update_big_endian)
2377  {
2379  }
2380  else if(expr.id()==ID_byte_extract_little_endian ||
2381  expr.id()==ID_byte_extract_big_endian)
2382  {
2384  }
2385  else if(expr.id()==ID_pointer_object)
2386  {
2388  }
2389  else if(expr.id() == ID_is_dynamic_object)
2390  {
2392  }
2393  else if(expr.id() == ID_is_invalid_pointer)
2394  {
2396  }
2397  else if(expr.id()==ID_object_size)
2398  {
2400  }
2401  else if(expr.id()==ID_good_pointer)
2402  {
2404  }
2405  else if(expr.id()==ID_div)
2406  {
2407  r = simplify_div(to_div_expr(expr));
2408  }
2409  else if(expr.id()==ID_mod)
2410  {
2411  r = simplify_mod(to_mod_expr(expr));
2412  }
2413  else if(expr.id()==ID_bitnot)
2414  {
2415  r = simplify_bitnot(to_bitnot_expr(expr));
2416  }
2417  else if(expr.id()==ID_bitand ||
2418  expr.id()==ID_bitor ||
2419  expr.id()==ID_bitxor)
2420  {
2422  }
2423  else if(expr.id()==ID_ashr || expr.id()==ID_lshr || expr.id()==ID_shl)
2424  {
2425  r = simplify_shifts(to_shift_expr(expr));
2426  }
2427  else if(expr.id()==ID_power)
2428  {
2429  r = simplify_power(to_binary_expr(expr));
2430  }
2431  else if(expr.id()==ID_plus)
2432  {
2433  r = simplify_plus(to_plus_expr(expr));
2434  }
2435  else if(expr.id()==ID_minus)
2436  {
2437  r = simplify_minus(to_minus_expr(expr));
2438  }
2439  else if(expr.id()==ID_mult)
2440  {
2441  r = simplify_mult(to_mult_expr(expr));
2442  }
2443  else if(expr.id()==ID_floatbv_plus ||
2444  expr.id()==ID_floatbv_minus ||
2445  expr.id()==ID_floatbv_mult ||
2446  expr.id()==ID_floatbv_div)
2447  {
2449  }
2450  else if(expr.id()==ID_floatbv_typecast)
2451  {
2453  }
2454  else if(expr.id()==ID_unary_minus)
2455  {
2457  }
2458  else if(expr.id()==ID_unary_plus)
2459  {
2461  }
2462  else if(expr.id()==ID_not)
2463  {
2464  r = simplify_not(to_not_expr(expr));
2465  }
2466  else if(expr.id()==ID_implies ||
2467  expr.id()==ID_or || expr.id()==ID_xor ||
2468  expr.id()==ID_and)
2469  {
2470  r = simplify_boolean(expr);
2471  }
2472  else if(expr.id()==ID_dereference)
2473  {
2475  }
2476  else if(expr.id()==ID_address_of)
2477  {
2479  }
2480  else if(expr.id()==ID_pointer_offset)
2481  {
2483  }
2484  else if(expr.id()==ID_extractbit)
2485  {
2487  }
2488  else if(expr.id()==ID_concatenation)
2489  {
2491  }
2492  else if(expr.id()==ID_extractbits)
2493  {
2495  }
2496  else if(expr.id()==ID_ieee_float_equal ||
2497  expr.id()==ID_ieee_float_notequal)
2498  {
2500  }
2501  else if(expr.id() == ID_bswap)
2502  {
2503  r = simplify_bswap(to_bswap_expr(expr));
2504  }
2505  else if(expr.id()==ID_isinf)
2506  {
2507  r = simplify_isinf(to_unary_expr(expr));
2508  }
2509  else if(expr.id()==ID_isnan)
2510  {
2511  r = simplify_isnan(to_unary_expr(expr));
2512  }
2513  else if(expr.id()==ID_isnormal)
2514  {
2516  }
2517  else if(expr.id()==ID_abs)
2518  {
2519  r = simplify_abs(to_abs_expr(expr));
2520  }
2521  else if(expr.id()==ID_sign)
2522  {
2523  r = simplify_sign(to_sign_expr(expr));
2524  }
2525  else if(expr.id() == ID_popcount)
2526  {
2528  }
2529  else if(expr.id() == ID_count_leading_zeros)
2530  {
2532  }
2533  else if(expr.id() == ID_count_trailing_zeros)
2534  {
2536  }
2537  else if(expr.id() == ID_function_application)
2538  {
2540  }
2541  else if(expr.id() == ID_complex_real || expr.id() == ID_complex_imag)
2542  {
2543  r = simplify_complex(to_unary_expr(expr));
2544  }
2545  else if(
2546  expr.id() == ID_overflow_plus || expr.id() == ID_overflow_minus ||
2547  expr.id() == ID_overflow_mult || expr.id() == ID_overflow_shl)
2548  {
2550  }
2551  else if(expr.id() == ID_overflow_unary_minus)
2552  {
2554  }
2555  else if(expr.id() == ID_bitreverse)
2556  {
2558  }
2559 
2560  if(!no_change_join_operands)
2561  r = changed(r);
2562 
2563 #ifdef DEBUGX
2564  if(
2565  r.has_changed()
2566 # ifdef DEBUG_ON_DEMAND
2567  && debug_on
2568 # endif
2569  )
2570  {
2571  std::cout << "===== " << node.id() << ": " << format(node) << '\n'
2572  << " ---> " << format(r.expr) << '\n';
2573  }
2574 #endif
2575 
2576  return r;
2577 }
2578 
2580 {
2581  // look up in cache
2582 
2583  #ifdef USE_CACHE
2584  std::pair<simplify_expr_cachet::containert::iterator, bool>
2585  cache_result=simplify_expr_cache.container().
2586  insert(std::pair<exprt, exprt>(expr, exprt()));
2587 
2588  if(!cache_result.second) // found!
2589  {
2590  const exprt &new_expr=cache_result.first->second;
2591 
2592  if(new_expr.id().empty())
2593  return true; // no change
2594 
2595  expr=new_expr;
2596  return false;
2597  }
2598  #endif
2599 
2600  // We work on a copy to prevent unnecessary destruction of sharing.
2601  exprt tmp=expr;
2602  bool no_change = simplify_node_preorder(tmp);
2603 
2604  auto simplify_node_result = simplify_node(tmp);
2605 
2606  if(simplify_node_result.has_changed())
2607  {
2608  no_change = false;
2609  tmp = simplify_node_result.expr;
2610  }
2611 
2612 #ifdef USE_LOCAL_REPLACE_MAP
2613  #if 1
2614  replace_mapt::const_iterator it=local_replace_map.find(tmp);
2615  if(it!=local_replace_map.end())
2616  {
2617  tmp=it->second;
2618  no_change = false;
2619  }
2620  #else
2621  if(!local_replace_map.empty() &&
2622  !replace_expr(local_replace_map, tmp))
2623  {
2624  simplify_rec(tmp);
2625  no_change = false;
2626  }
2627  #endif
2628 #endif
2629 
2630  if(no_change) // no change
2631  {
2632  return unchanged(expr);
2633  }
2634  else // change, new expression is 'tmp'
2635  {
2636  POSTCONDITION(as_const(tmp).type() == expr.type());
2637 
2638 #ifdef USE_CACHE
2639  // save in cache
2640  cache_result.first->second = tmp;
2641 #endif
2642 
2643  return std::move(tmp);
2644  }
2645 }
2646 
2649 {
2650 #ifdef DEBUG_ON_DEMAND
2651  if(debug_on)
2652  std::cout << "TO-SIMP " << format(expr) << "\n";
2653 #endif
2654  auto result = simplify_rec(expr);
2655 #ifdef DEBUG_ON_DEMAND
2656  if(debug_on)
2657  std::cout << "FULLSIMP " << format(result.expr) << "\n";
2658 #endif
2659  if(result.has_changed())
2660  {
2661  expr = result.expr;
2662  return false; // change
2663  }
2664  else
2665  return true; // no change
2666 }
2667 
2669 bool simplify(exprt &expr, const namespacet &ns)
2670 {
2671  return simplify_exprt(ns).simplify(expr);
2672 }
2673 
2675 {
2676  simplify_exprt(ns).simplify(src);
2677  return src;
2678 }
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
API to expression classes for bitvectors.
const binary_overflow_exprt & to_binary_overflow_expr(const exprt &expr)
Cast an exprt to a binary_overflow_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const unary_overflow_exprt & to_unary_overflow_expr(const exprt &expr)
Cast an exprt to a unary_overflow_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
int16_t s2
Definition: bytecode_info.h:60
int8_t s1
Definition: bytecode_info.h:59
unsignedbv_typet size_type()
Definition: c_types.cpp:68
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
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:344
Absolute value.
Definition: std_expr.h:346
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
Array constructor from list of elements.
Definition: std_expr.h:1476
exprt & what()
Definition: std_expr.h:1428
Arrays with given size.
Definition: std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
std::size_t get_width() const
Definition: std_types.h:864
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & value() const
void set_offset(exprt e)
const exprt & op() const
const exprt & offset() const
void set_op(exprt e)
The C/C++ Booleans.
Definition: c_types.h:75
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:319
const typet & underlying_type() const
Definition: c_types.h:274
exprt real()
Definition: std_expr.h:1772
exprt imag()
Definition: std_expr.h:1782
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
void set_value(const irep_idt &value)
Definition: std_expr.h:2820
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:114
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
exprt & op1()
Definition: expr.h:102
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
exprt & op2()
Definition: expr.h:105
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
exprt & op0()
Definition: expr.h:99
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
The Boolean constant false.
Definition: std_expr.h:2865
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
Fixed-width bit-vector with signed fixed-point interpretation.
fixedbv_spect spec
Definition: fixedbv.h:44
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
mp_integer to_integer() const
Definition: fixedbv.cpp:37
void set_value(const mp_integer &_v)
Definition: fixedbv.h:96
void round(const fixedbv_spect &dest_spec)
Definition: fixedbv.cpp:52
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
ieee_float_spect spec
Definition: ieee_float.h:135
mp_integer to_integer() const
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
bool get_sign() const
Definition: ieee_float.h:248
void set_sign(bool _sign)
Definition: ieee_float.h:184
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:515
mp_integer pack() const
Definition: ieee_float.cpp:374
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & true_case()
Definition: std_expr.h:2253
exprt & false_case()
Definition: std_expr.h:2263
exprt & cond()
Definition: std_expr.h:2243
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1353
exprt & index()
Definition: std_expr.h:1363
Fixed-width bit-vector representing a signed or unsigned integer.
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
void make_nil()
Definition: irep.h:454
void swap(irept &irep)
Definition: irep.h:442
bool is_nil() const
Definition: irep.h:376
A (mathematical) lambda expression.
exprt application(const operandst &arguments) const
Extract member of struct or union.
Definition: std_expr.h:2667
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
The null pointer constant.
Definition: pointer_expr.h:723
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The popcount (counting the number of bits set to 1) expression.
const exprt & length() const
Definition: string_expr.h:128
const exprt & content() const
Definition: string_expr.h:138
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:506
Fixed-width bit-vector with two's complement interpretation.
resultt simplify_isnan(const unary_exprt &)
resultt simplify_bitwise(const multi_ary_exprt &)
resultt simplify_power(const binary_exprt &)
const namespacet & ns
resultt simplify_div(const div_exprt &)
resultt simplify_byte_extract(const byte_extract_exprt &)
resultt simplify_bitreverse(const bitreverse_exprt &)
Try to simplify bit-reversing to a constant expression.
resultt simplify_abs(const abs_exprt &)
resultt simplify_isnormal(const unary_exprt &)
resultt simplify_dereference(const dereference_exprt &)
resultt simplify_bitnot(const bitnot_exprt &)
resultt simplify_good_pointer(const unary_exprt &)
resultt simplify_popcount(const popcount_exprt &)
static resultt changed(resultt<> result)
bool simplify_if_preorder(if_exprt &expr)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_if(const if_exprt &)
resultt simplify_overflow_unary(const unary_overflow_exprt &)
Try to simplify overflow-unary-.
resultt simplify_pointer_offset(const unary_exprt &)
resultt simplify_minus(const minus_exprt &)
resultt simplify_extractbit(const extractbit_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_shifts(const shift_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_boolean(const exprt &)
resultt simplify_object(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
resultt simplify_with(const with_exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_not(const not_exprt &)
resultt simplify_isinf(const unary_exprt &)
resultt simplify_overflow_binary(const binary_overflow_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
resultt simplify_function_application(const function_application_exprt &)
Attempt to simplify mathematical function applications if we have enough information to do so.
resultt simplify_index(const index_exprt &)
resultt simplify_bswap(const bswap_exprt &)
resultt simplify_object_size(const unary_exprt &)
resultt simplify_member(const member_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_byte_update(const byte_update_exprt &)
bool simplify_node_preorder(exprt &expr)
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
resultt simplify_update(const update_exprt &)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_mod(const mod_exprt &)
resultt simplify_complex(const unary_exprt &)
resultt simplify_plus(const plus_exprt &)
virtual bool simplify(exprt &expr)
resultt simplify_unary_plus(const unary_plus_exprt &)
resultt simplify_is_dynamic_object(const unary_exprt &)
resultt simplify_node(exprt)
resultt simplify_lambda(const lambda_exprt &)
resultt simplify_concatenation(const concatenation_exprt &)
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
resultt simplify_ctz(const count_trailing_zeros_exprt &)
Try to simplify count-trailing-zeros to a constant expression.
resultt simplify_clz(const count_leading_zeros_exprt &)
Try to simplify count-leading-zeros to a constant expression.
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
resultt simplify_pointer_object(const unary_exprt &)
resultt simplify_sign(const sign_exprt &)
resultt simplify_unary_minus(const unary_minus_exprt &)
Struct constructor from list of elements.
Definition: std_expr.h:1722
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:57
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
const componentst & components() const
Definition: std_types.h:147
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:40
std::vector< componentt > componentst
Definition: std_types.h:140
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The Boolean constant true.
Definition: std_expr.h:2856
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:281
const exprt & op() const
Definition: std_expr.h:293
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
Definition: std_expr.h:1611
The union type.
Definition: c_types.h:125
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:318
Fixed-width bit-vector with unsigned binary interpretation.
Operator to update elements in structs and arrays.
Definition: std_expr.h:2496
exprt::operandst & designator()
Definition: std_expr.h:2522
exprt & old()
Definition: std_expr.h:2508
exprt & new_value()
Definition: std_expr.h:2532
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
exprt & old()
Definition: std_expr.h:2322
exprt & new_value()
Definition: std_expr.h:2342
exprt & where()
Definition: std_expr.h:2332
configt config
Definition: config.cpp:25
#define Forall_operands(it, expr)
Definition: expr.h:25
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:283
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:97
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:200
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:152
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: floatbv_expr.h:425
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
static format_containert< T > format(const T &o)
Definition: format.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
static int8_t r
Definition: irep_hash.h:60
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Pointer Logic.
exprt pointer_offset_sum(const exprt &a, const exprt &b)
Pointer Dereferencing.
constant_exprt from_rational(const rationalt &a)
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify(exprt &expr, const namespacet &ns)
static simplify_exprt::resultt simplify_string_compare_to(const function_application_exprt &expr, const namespacet &ns)
Simplify String.compareTo function when arguments are constant.
static simplify_exprt::resultt simplify_string_contains(const function_application_exprt &expr, const namespacet &ns)
Simplify String.contains function when arguments are constant.
static simplify_exprt::resultt simplify_string_endswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.endsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_char_at(const function_application_exprt &expr, const namespacet &ns)
Simplify String.charAt function when arguments are constant.
static simplify_exprt::resultt simplify_string_startswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.startsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_is_empty(const function_application_exprt &expr, const namespacet &ns)
Simplify String.isEmpty function when arguments are constant.
static bool lower_case_string_expression(array_exprt &string_data)
Take the passed-in constant string array and lower-case every character.
static simplify_exprt::resultt simplify_string_index_of(const function_application_exprt &expr, const namespacet &ns, const bool search_from_end)
Simplify String.indexOf function when arguments are constant.
static simplify_exprt::resultt simplify_string_equals_ignore_case(const function_application_exprt &expr, const namespacet &ns)
Simplify String.equalsIgnorecase function when arguments are constant.
exprt simplify_expr(exprt src, const namespacet &ns)
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
bool join_operands(exprt &expr)
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)
Get char sequence from content field of a refined string expression.
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define POSTCONDITION(CONDITION)
Definition: invariant.h:479
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
API to expression classes.
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2427
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2561
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:464
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1160
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1855
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1113
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2374
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1745
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1456
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1810
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1900
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:531
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:370
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1044
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
String expressions for the string solver.
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:150
bool can_cast_expr< refined_string_exprt >(const exprt &base)
Definition: string_expr.h:165
endiannesst endianness
Definition: config.h:177
bool NULL_is_zero
Definition: config.h:194
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177