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 }
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
int16_t s2
Definition: bytecode_info.h:60
int8_t s1
Definition: bytecode_info.h:59
unsignedbv_typet size_type()
Definition: c_types.cpp:58
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
Absolute value.
Definition: std_expr.h:347
Operator to return the address of an object.
Definition: pointer_expr.h:200
exprt & object()
Definition: pointer_expr.h:209
Array constructor from list of elements.
Definition: std_expr.h:1382
exprt & what()
Definition: std_expr.h:1334
Arrays with given size.
Definition: std_types.h:968
A base class for binary expressions.
Definition: std_expr.h:551
exprt & op1()
Definition: expr.h:106
exprt & op0()
Definition: expr.h:103
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
std::size_t get_width() const
Definition: std_types.h:1048
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & value() const
void set_offset(exprt e)
const exprt & op() const
const exprt & offset() const
void set_op(exprt e)
The C/C++ Booleans.
Definition: std_types.h:1618
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:704
exprt real()
Definition: std_expr.h:1633
exprt imag()
Definition: std_expr.h:1643
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition: std_expr.h:2668
const irep_idt & get_value() const
Definition: std_expr.h:2676
void set_value(const irep_idt &value)
Definition: std_expr.h:2681
Operator to dereference a pointer.
Definition: pointer_expr.h:256
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
exprt & op1()
Definition: expr.h:106
source_locationt & add_source_location()
Definition: expr.h:239
const source_locationt & source_location() const
Definition: expr.h:234
exprt & op2()
Definition: expr.h:109
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:78
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
exprt & op0()
Definition: expr.h:103
operandst & operands()
Definition: expr.h:96
The Boolean constant false.
Definition: std_expr.h:2726
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: std_types.h:1325
fixedbv_spect spec
Definition: fixedbv.h:44
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
mp_integer to_integer() const
Definition: fixedbv.cpp:37
void set_value(const mp_integer &_v)
Definition: fixedbv.h:96
void round(const fixedbv_spect &dest_spec)
Definition: fixedbv.cpp:52
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1386
Application of (mathematical) function.
ieee_float_spect spec
Definition: ieee_float.h:134
mp_integer to_integer() const
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
bool get_sign() const
Definition: ieee_float.h:236
void set_sign(bool _sign)
Definition: ieee_float.h:172
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:511
mp_integer pack() const
Definition: ieee_float.cpp:370
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
Definition: std_expr.h:2087
exprt & true_case()
Definition: std_expr.h:2114
exprt & false_case()
Definition: std_expr.h:2124
exprt & cond()
Definition: std_expr.h:2104
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
exprt & index()
Definition: std_expr.h:1269
Fixed-width bit-vector representing a signed or unsigned integer.
Definition: std_types.h:1163
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:464
void swap(irept &irep)
Definition: irep.h:452
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
bool is_nil() const
Definition: irep.h:387
A (mathematical) lambda expression.
exprt application(const operandst &) const
Extract member of struct or union.
Definition: std_expr.h:2528
Binary multiplication Associativity is not specified.
Definition: std_expr.h:936
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The NIL expression.
Definition: std_expr.h:2735
The null pointer constant.
Definition: std_expr.h:2751
The plus expression Associativity is not specified.
Definition: std_expr.h:831
The popcount (counting the number of bits set to 1) expression.
const exprt & length() const
Definition: string_expr.h:128
const exprt & content() const
Definition: string_expr.h:138
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:507
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1272
resultt simplify_isnan(const unary_exprt &)
resultt simplify_bitwise(const multi_ary_exprt &)
resultt simplify_power(const binary_exprt &)
const namespacet & ns
resultt simplify_div(const div_exprt &)
resultt simplify_overflow_unary(const unary_exprt &)
Try to simplify overflow-unary-.
resultt simplify_byte_extract(const byte_extract_exprt &)
resultt simplify_abs(const abs_exprt &)
resultt simplify_overflow_binary(const binary_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
resultt simplify_isnormal(const unary_exprt &)
resultt simplify_dereference(const dereference_exprt &)
resultt simplify_bitnot(const bitnot_exprt &)
resultt simplify_good_pointer(const unary_exprt &)
resultt simplify_popcount(const popcount_exprt &)
static resultt changed(resultt<> result)
bool simplify_if_preorder(if_exprt &expr)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_if(const if_exprt &)
resultt simplify_pointer_offset(const unary_exprt &)
resultt simplify_minus(const minus_exprt &)
resultt simplify_extractbit(const extractbit_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_shifts(const shift_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_boolean(const exprt &)
resultt simplify_object(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
resultt simplify_with(const with_exprt &)
resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_not(const not_exprt &)
resultt simplify_isinf(const unary_exprt &)
resultt simplify_function_application(const function_application_exprt &)
Attempt to simplify mathematical function applications if we have enough information to do so.
resultt simplify_index(const index_exprt &)
resultt simplify_bswap(const bswap_exprt &)
resultt simplify_object_size(const unary_exprt &)
resultt simplify_member(const member_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_byte_update(const byte_update_exprt &)
bool simplify_node_preorder(exprt &expr)
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
resultt simplify_update(const update_exprt &)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_mod(const mod_exprt &)
resultt simplify_complex(const unary_exprt &)
resultt simplify_plus(const plus_exprt &)
virtual bool simplify(exprt &expr)
resultt simplify_unary_plus(const unary_plus_exprt &)
resultt simplify_is_dynamic_object(const unary_exprt &)
resultt simplify_node(exprt)
resultt simplify_lambda(const lambda_exprt &)
resultt simplify_concatenation(const concatenation_exprt &)
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
resultt simplify_pointer_object(const unary_exprt &)
resultt simplify_sign(const sign_exprt &)
resultt simplify_unary_minus(const unary_minus_exprt &)
Structure type, corresponds to C style structs.
Definition: std_types.h:226
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:67
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:152
const componentst & components() const
Definition: std_types.h:142
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
std::vector< componentt > componentst
Definition: std_types.h:135
const irep_idt & get_identifier() const
Definition: std_expr.h:110
The Boolean constant true.
Definition: std_expr.h:2717
Semantic type conversion.
Definition: std_expr.h:1781
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
Generic base class for unary expressions.
Definition: std_expr.h:282
const exprt & op() const
Definition: std_expr.h:294
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
Operator to update elements in structs and arrays.
Definition: std_expr.h:2357
exprt::operandst & designator()
Definition: std_expr.h:2383
exprt & old()
Definition: std_expr.h:2369
exprt & new_value()
Definition: std_expr.h:2393
Operator to update elements in structs and arrays.
Definition: std_expr.h:2173
exprt & old()
Definition: std_expr.h:2183
exprt & new_value()
Definition: std_expr.h:2203
exprt & where()
Definition: std_expr.h:2193
configt config
Definition: config.cpp:24
#define Forall_operands(it, expr)
Definition: expr.h:25
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:284
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:99
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:202
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
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: floatbv_expr.h:425
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
static format_containert< T > format(const T &o)
Definition: format.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
static int8_t r
Definition: irep_hash.h:59
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
BigInt mp_integer
Definition: mp_arith.h:19
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset_sum(const exprt &a, const exprt &b)
Pointer Dereferencing.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
constant_exprt from_rational(const rationalt &a)
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify(exprt &expr, const namespacet &ns)
static simplify_exprt::resultt simplify_string_compare_to(const function_application_exprt &expr, const namespacet &ns)
Simplify String.compareTo function when arguments are constant.
static simplify_exprt::resultt simplify_string_contains(const function_application_exprt &expr, const namespacet &ns)
Simplify String.contains function when arguments are constant.
static simplify_exprt::resultt simplify_string_endswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.endsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_char_at(const function_application_exprt &expr, const namespacet &ns)
Simplify String.charAt function when arguments are constant.
static simplify_exprt::resultt simplify_string_startswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.startsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_is_empty(const function_application_exprt &expr, const namespacet &ns)
Simplify String.isEmpty function when arguments are constant.
static bool lower_case_string_expression(array_exprt &string_data)
Take the passed-in constant string array and lower-case every character.
static simplify_exprt::resultt simplify_string_index_of(const function_application_exprt &expr, const namespacet &ns, const bool search_from_end)
Simplify String.indexOf function when arguments are constant.
static simplify_exprt::resultt simplify_string_equals_ignore_case(const function_application_exprt &expr, const namespacet &ns)
Simplify String.equalsIgnorecase function when arguments are constant.
exprt simplify_expr(exprt src, const namespacet &ns)
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
bool join_operands(exprt &expr)
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)
Get char sequence from content field of a refined string expression.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define POSTCONDITION(CONDITION)
Definition: invariant.h:480
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
API to expression classes.
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2288
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2422
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:465
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1075
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1716
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2067
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:421
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1030
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:915
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:816
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2235
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1606
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1362
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:870
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1671
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1761
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:532
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:371
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:724
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:961
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1431
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1096
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:689
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1369
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
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: std_types.h:1146
String expressions for the string solver.
refined_string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:150
bool can_cast_expr< refined_string_exprt >(const exprt &base)
Definition: string_expr.h:165
bool NULL_is_zero
Definition: config.h:168
irep_idt byte_extract_id()