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