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