CBMC
Loading...
Searching...
No Matches
simplify_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "simplify_expr.h"
10
11#include <algorithm>
12
13#include "bitvector_expr.h"
14#include "byte_operators.h"
15#include "c_types.h"
16#include "config.h"
17#include "expr_util.h"
18#include "fixedbv.h"
19#include "floatbv_expr.h"
20#include "invariant.h"
21#include "mathematical_expr.h"
22#include "namespace.h"
23#include "pointer_expr.h"
24#include "pointer_offset_size.h"
25#include "pointer_offset_sum.h"
26#include "rational.h"
27#include "rational_tools.h"
28#include "simplify_utils.h"
29#include "std_expr.h"
30#include "string_expr.h"
31
32// #define DEBUGX
33
34#ifdef DEBUGX
35#include "format_expr.h"
36#include <iostream>
37#endif
38
39#include "simplify_expr_class.h"
40
41// #define USE_CACHE
42
43#ifdef USE_CACHE
45{
46public:
47 #if 1
48 typedef std::unordered_map<
50 #else
51 typedef std::unordered_map<exprt, exprt, irep_hash> containert;
52 #endif
53
55
56 containert &container()
57 {
58 return container_normal;
59 }
60};
61
63#endif
64
66{
67 if(expr.op().is_constant())
68 {
69 const typet &type = to_unary_expr(expr).op().type();
70
71 if(type.id()==ID_floatbv)
72 {
74 value.set_sign(false);
75 return value.to_expr();
76 }
77 else if(type.id()==ID_signedbv ||
78 type.id()==ID_unsignedbv)
79 {
80 auto value = numeric_cast<mp_integer>(to_unary_expr(expr).op());
81 if(value.has_value())
82 {
83 if(*value >= 0)
84 {
85 return to_unary_expr(expr).op();
86 }
87 else
88 {
89 value->negate();
90 return from_integer(*value, type);
91 }
92 }
93 }
94 }
95
96 return unchanged(expr);
97}
98
100{
101 if(expr.op().is_constant())
102 {
103 const typet &type = expr.op().type();
104
105 if(type.id()==ID_floatbv)
106 {
108 return make_boolean_expr(value.get_sign());
109 }
110 else if(type.id()==ID_signedbv ||
111 type.id()==ID_unsignedbv)
112 {
113 const auto value = numeric_cast<mp_integer>(expr.op());
114 if(value.has_value())
115 {
116 return make_boolean_expr(*value >= 0);
117 }
118 }
119 }
120
121 return unchanged(expr);
122}
123
126{
127 const exprt &op = expr.op();
128
129 if(op.is_constant())
130 {
131 const typet &op_type = op.type();
132
133 if(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv)
134 {
135 const auto width = to_bitvector_type(op_type).get_width();
136 const auto &value = to_constant_expr(op).get_value();
137 std::size_t result = 0;
138
139 for(std::size_t i = 0; i < width; i++)
140 if(get_bvrep_bit(value, width, i))
141 result++;
142
143 return from_integer(result, expr.type());
144 }
145 }
146
147 return unchanged(expr);
148}
149
152{
153 const bool is_little_endian =
155
156 const auto const_bits_opt = expr2bits(expr.op(), is_little_endian, ns);
157
158 if(!const_bits_opt.has_value())
159 return unchanged(expr);
160
161 std::size_t n_leading_zeros =
162 is_little_endian ? const_bits_opt->rfind('1') : const_bits_opt->find('1');
163 if(n_leading_zeros == std::string::npos)
164 {
165 if(!expr.zero_permitted())
166 return unchanged(expr);
167
169 }
170 else if(is_little_endian)
172
173 return from_integer(n_leading_zeros, expr.type());
174}
175
178{
179 const bool is_little_endian =
181
182 const auto const_bits_opt = expr2bits(expr.op(), is_little_endian, ns);
183
184 if(!const_bits_opt.has_value())
185 return unchanged(expr);
186
187 std::size_t n_trailing_zeros =
188 is_little_endian ? const_bits_opt->find('1') : const_bits_opt->rfind('1');
189 if(n_trailing_zeros == std::string::npos)
190 {
191 if(!expr.zero_permitted())
192 return unchanged(expr);
193
195 }
196 else if(!is_little_endian)
198
199 return from_integer(n_trailing_zeros, expr.type());
200}
201
204{
205 const bool is_little_endian =
207
208 const auto const_bits_opt = expr2bits(expr.op(), is_little_endian, ns);
209
210 if(!const_bits_opt.has_value())
211 return unchanged(expr);
212
213 std::size_t first_one_bit =
214 is_little_endian ? const_bits_opt->find('1') : const_bits_opt->rfind('1');
215 if(first_one_bit == std::string::npos)
216 first_one_bit = 0;
217 else if(is_little_endian)
219 else
221
222 return from_integer(first_one_bit, expr.type());
223}
224
230 const function_application_exprt &expr,
231 const namespacet &ns)
232{
233 const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
234 const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
235
236 if(!s1_data_opt)
237 return simplify_exprt::unchanged(expr);
238
239 const array_exprt &s1_data = s1_data_opt->get();
240 const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1));
241 const auto s2_data_opt = try_get_string_data_array(s2.content(), ns);
242
243 if(!s2_data_opt)
244 return simplify_exprt::unchanged(expr);
245
246 const array_exprt &s2_data = s2_data_opt->get();
247 const bool res = s2_data.operands().size() <= s1_data.operands().size() &&
248 std::equal(
249 s2_data.operands().rbegin(),
250 s2_data.operands().rend(),
251 s1_data.operands().rbegin());
252
253 return from_integer(res ? 1 : 0, expr.type());
254}
255
258 const function_application_exprt &expr,
259 const namespacet &ns)
260{
261 // We want to get both arguments of any starts-with comparison, and
262 // trace them back to the actual string instance. All variables on the
263 // way must be constant for us to be sure this will work.
264 auto &first_argument = to_string_expr(expr.arguments().at(0));
265 auto &second_argument = to_string_expr(expr.arguments().at(1));
266
267 const auto first_value_opt =
269
270 if(!first_value_opt)
271 {
272 return simplify_exprt::unchanged(expr);
273 }
274
276
277 const auto second_value_opt =
279
281 {
282 return simplify_exprt::unchanged(expr);
283 }
284
286
287 // Is our 'contains' array directly contained in our target.
288 const bool includes =
289 std::search(
290 first_value.operands().begin(),
291 first_value.operands().end(),
292 second_value.operands().begin(),
293 second_value.operands().end()) != first_value.operands().end();
294
295 return from_integer(includes ? 1 : 0, expr.type());
296}
297
303 const function_application_exprt &expr,
304 const namespacet &ns)
305{
308 const refined_string_exprt &s =
309 to_string_expr(function_app.arguments().at(0));
310
311 if(!s.length().is_constant())
312 return simplify_exprt::unchanged(expr);
313
314 const auto numeric_length =
316
317 return from_integer(numeric_length == 0 ? 1 : 0, expr.type());
318}
319
328 const function_application_exprt &expr,
329 const namespacet &ns)
330{
331 const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
332 const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
333
334 if(!s1_data_opt)
335 return simplify_exprt::unchanged(expr);
336
337 const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1));
338 const auto s2_data_opt = try_get_string_data_array(s2.content(), ns);
339
340 if(!s2_data_opt)
341 return simplify_exprt::unchanged(expr);
342
343 const array_exprt &s1_data = s1_data_opt->get();
344 const array_exprt &s2_data = s2_data_opt->get();
345
346 if(s1_data.operands() == s2_data.operands())
347 return from_integer(0, expr.type());
348
349 const mp_integer s1_size = s1_data.operands().size();
350 const mp_integer s2_size = s2_data.operands().size();
351 const bool first_shorter = s1_size < s2_size;
352 const exprt::operandst &ops1 =
353 first_shorter ? s1_data.operands() : s2_data.operands();
354 const exprt::operandst &ops2 =
355 first_shorter ? s2_data.operands() : s1_data.operands();
356 auto it_pair = std::mismatch(ops1.begin(), ops1.end(), ops2.begin());
357
358 if(it_pair.first == ops1.end())
359 return from_integer(s1_size - s2_size, expr.type());
360
361 const mp_integer char1 =
363 const mp_integer char2 =
365
366 return from_integer(
367 first_shorter ? char1 - char2 : char2 - char1, expr.type());
368}
369
377 const function_application_exprt &expr,
378 const namespacet &ns,
379 const bool search_from_end)
380{
381 std::size_t starting_index = 0;
382
383 // Determine starting index for the comparison (if given)
384 if(expr.arguments().size() == 3)
385 {
386 auto &starting_index_expr = expr.arguments().at(2);
387
388 if(!starting_index_expr.is_constant())
389 {
390 return simplify_exprt::unchanged(expr);
391 }
392
393 const mp_integer idx =
395
396 // Negative indices are treated like 0
397 if(idx > 0)
398 {
400 }
401 }
402
403 const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
404
405 const auto s1_data_opt = try_get_string_data_array(s1.content(), ns);
406
407 if(!s1_data_opt)
408 {
409 return simplify_exprt::unchanged(expr);
410 }
411
412 const array_exprt &s1_data = s1_data_opt->get();
413
414 const auto search_string_size = s1_data.operands().size();
416 {
417 return from_integer(-1, expr.type());
418 }
419
420 unsigned long starting_offset =
423 {
424 // Second argument is a string
425
426 const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1));
427
428 const auto s2_data_opt = try_get_string_data_array(s2.content(), ns);
429
430 if(!s2_data_opt)
431 {
432 return simplify_exprt::unchanged(expr);
433 }
434
435 const array_exprt &s2_data = s2_data_opt->get();
436
437 // Searching for empty string is a special case and is simply the
438 // "always found at the first searched position. This needs to take into
439 // account starting position and if you're starting from the beginning or
440 // end.
441 if(s2_data.operands().empty())
442 return from_integer(
445 : 0,
446 expr.type());
447
449 {
450 auto end = std::prev(s1_data.operands().end(), starting_offset);
451 auto it = std::find_end(
452 s1_data.operands().begin(),
453 end,
454 s2_data.operands().begin(),
455 s2_data.operands().end());
456 if(it != end)
457 return from_integer(
458 std::distance(s1_data.operands().begin(), it), expr.type());
459 }
460 else
461 {
462 auto it = std::search(
463 std::next(s1_data.operands().begin(), starting_index),
464 s1_data.operands().end(),
465 s2_data.operands().begin(),
466 s2_data.operands().end());
467
468 if(it != s1_data.operands().end())
469 return from_integer(
470 std::distance(s1_data.operands().begin(), it), expr.type());
471 }
472 }
473 else if(expr.arguments().at(1).is_constant())
474 {
475 // Second argument is a constant character
476
477 const constant_exprt &c1 = to_constant_expr(expr.arguments().at(1));
479
480 auto pred = [&](const exprt &c2) {
482
483 return c1_val == c2_val;
484 };
485
487 {
488 auto it = std::find_if(
489 std::next(s1_data.operands().rbegin(), starting_offset),
490 s1_data.operands().rend(),
491 pred);
492 if(it != s1_data.operands().rend())
493 return from_integer(
494 std::distance(s1_data.operands().begin(), it.base() - 1),
495 expr.type());
496 }
497 else
498 {
499 auto it = std::find_if(
500 std::next(s1_data.operands().begin(), starting_index),
501 s1_data.operands().end(),
502 pred);
503 if(it != s1_data.operands().end())
504 return from_integer(
505 std::distance(s1_data.operands().begin(), it), expr.type());
506 }
507 }
508 else
509 {
510 return simplify_exprt::unchanged(expr);
511 }
512
513 return from_integer(-1, expr.type());
514}
515
522 const function_application_exprt &expr,
523 const namespacet &ns)
524{
525 if(!expr.arguments().at(1).is_constant())
526 {
527 return simplify_exprt::unchanged(expr);
528 }
529
530 const auto &index = to_constant_expr(expr.arguments().at(1));
531
532 const refined_string_exprt &s = to_string_expr(expr.arguments().at(0));
533
534 const auto char_seq_opt = try_get_string_data_array(s.content(), ns);
535
536 if(!char_seq_opt)
537 {
538 return simplify_exprt::unchanged(expr);
539 }
540
541 const array_exprt &char_seq = char_seq_opt->get();
542
543 const auto i_opt = numeric_cast<std::size_t>(index);
544
545 if(!i_opt || *i_opt >= char_seq.operands().size())
546 {
547 return simplify_exprt::unchanged(expr);
548 }
549
550 const auto &c = to_constant_expr(char_seq.operands().at(*i_opt));
551
552 if(c.type() != expr.type())
553 {
554 return simplify_exprt::unchanged(expr);
555 }
556
557 return c;
558}
559
562{
563 auto &operands = string_data.operands();
564 for(auto &operand : operands)
565 {
568
569 // Can't guarantee matches against non-ASCII characters.
570 if(character >= 128)
571 return false;
572
573 if(isalpha(character))
574 {
575 if(isupper(character))
577 from_integer(tolower(character), constant_value.type());
578 }
579 }
580
581 return true;
582}
583
590 const function_application_exprt &expr,
591 const namespacet &ns)
592{
593 // We want to get both arguments of any starts-with comparison, and
594 // trace them back to the actual string instance. All variables on the
595 // way must be constant for us to be sure this will work.
596 auto &first_argument = to_string_expr(expr.arguments().at(0));
597 auto &second_argument = to_string_expr(expr.arguments().at(1));
598
599 const auto first_value_opt =
601
602 if(!first_value_opt)
603 {
604 return simplify_exprt::unchanged(expr);
605 }
606
608
609 const auto second_value_opt =
611
613 {
614 return simplify_exprt::unchanged(expr);
615 }
616
618
619 // Just lower-case both expressions.
620 if(
623 return simplify_exprt::unchanged(expr);
624
625 bool is_equal = first_value == second_value;
626 return from_integer(is_equal ? 1 : 0, expr.type());
627}
628
635 const function_application_exprt &expr,
636 const namespacet &ns)
637{
638 // We want to get both arguments of any starts-with comparison, and
639 // trace them back to the actual string instance. All variables on the
640 // way must be constant for us to be sure this will work.
641 auto &first_argument = to_string_expr(expr.arguments().at(0));
642 auto &second_argument = to_string_expr(expr.arguments().at(1));
643
644 const auto first_value_opt =
646
647 if(!first_value_opt)
648 {
649 return simplify_exprt::unchanged(expr);
650 }
651
653
654 const auto second_value_opt =
656
658 {
659 return simplify_exprt::unchanged(expr);
660 }
661
663
665 if(expr.arguments().size() == 3)
666 {
667 auto &offset = expr.arguments()[2];
668 if(!offset.is_constant())
669 return simplify_exprt::unchanged(expr);
671 }
672
673 // test whether second_value is a prefix of first_value
674 bool is_prefix =
675 offset_int >= 0 && mp_integer(first_value.operands().size()) >=
676 offset_int + second_value.operands().size();
677 if(is_prefix)
678 {
679 exprt::operandst::const_iterator second_it =
680 second_value.operands().begin();
681 for(const auto &first_op : first_value.operands())
682 {
683 if(offset_int > 0)
684 --offset_int;
685 else if(second_it == second_value.operands().end())
686 break;
687 else if(first_op != *second_it)
688 {
689 is_prefix = false;
690 break;
691 }
692 else
693 ++second_it;
694 }
695 }
696
697 return from_integer(is_prefix ? 1 : 0, expr.type());
698}
699
701 const function_application_exprt &expr)
702{
703 if(expr.function().id() == ID_lambda)
704 {
705 // expand the function application
706 return to_lambda_expr(expr.function()).application(expr.arguments());
707 }
708
709 if(expr.function().id() != ID_symbol)
710 return unchanged(expr);
711
712 const irep_idt &func_id = to_symbol_expr(expr.function()).get_identifier();
713
714 // String.startsWith() is used to implement String.equals() in the models
715 // library
717 {
718 return simplify_string_startswith(expr, ns);
719 }
721 {
722 return simplify_string_endswith(expr, ns);
723 }
725 {
726 return simplify_string_is_empty(expr, ns);
727 }
729 {
730 return simplify_string_compare_to(expr, ns);
731 }
733 {
734 return simplify_string_index_of(expr, ns, false);
735 }
737 {
738 return simplify_string_char_at(expr, ns);
739 }
741 {
742 return simplify_string_contains(expr, ns);
743 }
745 {
746 return simplify_string_index_of(expr, ns, true);
747 }
749 {
751 }
752
753 return unchanged(expr);
754}
755
758{
759 const typet &expr_type = expr.type();
760 const typet &op_type = expr.op().type();
761
762 // eliminate casts of infinity
763 if(expr.op().id() == ID_infinity)
764 {
765 typet new_type=expr.type();
766 exprt tmp = expr.op();
767 tmp.type()=new_type;
768 return std::move(tmp);
769 }
770
771 // casts from NULL to any integer
772 if(
773 op_type.id() == ID_pointer && expr.op().is_constant() &&
774 to_constant_expr(expr.op()).get_value() == ID_NULL &&
775 (expr_type.id() == ID_unsignedbv || expr_type.id() == ID_signedbv) &&
776 config.ansi_c.NULL_is_zero)
777 {
778 return from_integer(0, expr_type);
779 }
780
781 // casts from pointer to integer
782 // where width of integer >= width of pointer
783 // (void*)(intX)expr -> (void*)expr
784 if(
785 expr_type.id() == ID_pointer && expr.op().id() == ID_typecast &&
786 (op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv ||
787 op_type.id() == ID_bv) &&
788 to_bitvector_type(op_type).get_width() >=
789 to_bitvector_type(expr_type).get_width())
790 {
791 auto new_expr = expr;
792 new_expr.op() = to_typecast_expr(expr.op()).op();
793 return changed(simplify_typecast(new_expr)); // rec. call
794 }
795
796 // eliminate redundant typecasts
797 if(expr.type() == expr.op().type())
798 {
799 return expr.op();
800 }
801
802 // eliminate casts to proper bool
803 if(expr_type.id()==ID_bool)
804 {
805 // rewrite (bool)x to x!=0
807 expr.op(),
810 inequality.add_source_location()=expr.source_location();
812 }
813
814 // eliminate casts from proper bool
815 if(
816 op_type.id() == ID_bool &&
817 (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv ||
818 expr_type.id() == ID_c_bool || expr_type.id() == ID_c_bit_field))
819 {
820 // rewrite (T)(bool) to bool?1:0
821 auto one = from_integer(1, expr_type);
822 auto zero = from_integer(0, expr_type);
824 if_exprt{expr.op(), std::move(one), std::move(zero)}));
825 }
826
827 // circular casts through types shorter than `int`
828 // we use fixed bit widths as this is specifically for the Java bytecode
829 // front-end
830 if(op_type == signedbv_typet(32) && expr.op().id() == ID_typecast)
831 {
832 if(expr_type==c_bool_typet(8) ||
836 {
837 // We checked that the id was ID_typecast in the enclosing `if`
838 const auto &typecast = expr_checked_cast<typecast_exprt>(expr.op());
839 if(typecast.op().type()==expr_type)
840 {
841 return typecast.op();
842 }
843 }
844 }
845
846 // eliminate casts to _Bool
847 if(expr_type.id()==ID_c_bool &&
848 op_type.id()!=ID_bool)
849 {
850 // rewrite (_Bool)x to (_Bool)(x!=0)
851 exprt inequality = is_not_zero(expr.op(), ns);
852 auto new_expr = expr;
853 new_expr.op() = simplify_node(std::move(inequality));
854 return changed(simplify_typecast(new_expr)); // recursive call
855 }
856
857 // eliminate typecasts from NULL
858 if(
859 expr_type.id() == ID_pointer && expr.op().is_constant() &&
860 (to_constant_expr(expr.op()).get_value() == ID_NULL ||
861 (expr.op().is_zero() && config.ansi_c.NULL_is_zero)))
862 {
863 exprt tmp = expr.op();
864 tmp.type()=expr.type();
865 to_constant_expr(tmp).set_value(ID_NULL);
866 return std::move(tmp);
867 }
868
869 // eliminate duplicate pointer typecasts
870 // (T1 *)(T2 *)x -> (T1 *)x
871 if(
872 expr_type.id() == ID_pointer && expr.op().id() == ID_typecast &&
873 op_type.id() == ID_pointer)
874 {
875 auto new_expr = expr;
876 new_expr.op() = to_typecast_expr(expr.op()).op();
877 return changed(simplify_typecast(new_expr)); // recursive call
878 }
879
880 // casts from integer to pointer and back:
881 // (int)(void *)int -> (int)(size_t)int
882 if(
883 (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv) &&
884 expr.op().id() == ID_typecast && expr.op().operands().size() == 1 &&
885 op_type.id() == ID_pointer)
886 {
887 auto inner_cast = to_typecast_expr(expr.op());
888 inner_cast.type() = size_type();
889
890 auto outer_cast = expr;
891 outer_cast.op() = simplify_typecast(inner_cast); // rec. call
892 return changed(simplify_typecast(outer_cast)); // rec. call
893 }
894
895 // mildly more elaborate version of the above:
896 // (int)((T*)0 + int) -> (int)(sizeof(T)*(size_t)int) if NULL is zero
897 if(
898 config.ansi_c.NULL_is_zero &&
899 (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv) &&
900 op_type.id() == ID_pointer && expr.op().id() == ID_plus &&
901 expr.op().operands().size() == 2)
902 {
903 const auto &op_plus_expr = to_plus_expr(expr.op());
904
905 if(
906 (op_plus_expr.op0().id() == ID_typecast &&
907 to_typecast_expr(op_plus_expr.op0()).op().is_zero()) ||
908 (op_plus_expr.op0().is_constant() &&
909 to_constant_expr(op_plus_expr.op0()).is_null_pointer()))
910 {
911 auto sub_size =
913 if(sub_size.has_value())
914 {
915 auto new_expr = expr;
918
919 // void*
920 if(*sub_size == 0 || *sub_size == 1)
921 new_expr.op() = offset_expr;
922 else
923 {
924 new_expr.op() = simplify_mult(
926 }
927
928 return changed(simplify_typecast(new_expr)); // rec. call
929 }
930 }
931 }
932
933 // Push a numerical typecast into various integer operations, i.e.,
934 // (T)(x OP y) ---> (T)x OP (T)y
935 //
936 // Doesn't work for many, e.g., pointer difference, floating-point,
937 // division, modulo.
938 // Many operations fail if the width of T
939 // is bigger than that of (x OP y). This includes ID_bitnot and
940 // anything that might overflow, e.g., ID_plus.
941 //
942 if((expr_type.id()==ID_signedbv || expr_type.id()==ID_unsignedbv) &&
943 (op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv))
944 {
945 bool enlarge=
946 to_bitvector_type(expr_type).get_width()>
947 to_bitvector_type(op_type).get_width();
948
949 if(!enlarge)
950 {
951 irep_idt op_id = expr.op().id();
952
953 if(
954 op_id == ID_plus || op_id == ID_minus || op_id == ID_mult ||
955 op_id == ID_unary_minus || op_id == ID_bitxor || op_id == ID_bitxnor ||
956 op_id == ID_bitor || op_id == ID_bitand)
957 {
958 exprt result = expr.op();
959
960 if(
961 result.operands().size() >= 1 &&
962 to_multi_ary_expr(result).op0().type() == result.type())
963 {
964 result.type()=expr.type();
965
966 Forall_operands(it, result)
967 {
968 auto new_operand = typecast_exprt(*it, expr.type());
969 *it = simplify_typecast(new_operand); // recursive call
970 }
971
972 return changed(simplify_node(result)); // possibly recursive call
973 }
974 }
975 else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
976 {
977 }
978 }
979 }
980
981 // Push a numerical typecast into pointer arithmetic
982 // (T)(ptr + int) ---> (T)((size_t)ptr + sizeof(subtype)*(size_t)int)
983 //
984 if(
985 (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv) &&
986 op_type.id() == ID_pointer && expr.op().id() == ID_plus)
987 {
988 const auto step =
990
991 if(step.has_value() && *step != 0)
992 {
993 const typet size_t_type(size_type());
994 auto new_expr = expr;
995
996 new_expr.op().type() = size_t_type;
997
998 for(auto &op : new_expr.op().operands())
999 {
1001 if(op.type().id() != ID_pointer && *step > 1)
1002 {
1003 new_op =
1005 }
1006 op = std::move(new_op);
1007 }
1008
1010
1011 return changed(simplify_typecast(new_expr)); // recursive call
1012 }
1013 }
1014
1015 const irep_idt &expr_type_id=expr_type.id();
1016 const exprt &operand = expr.op();
1017 const irep_idt &op_type_id=op_type.id();
1018
1019 if(operand.is_constant())
1020 {
1021 const irep_idt &value=to_constant_expr(operand).get_value();
1022
1023 // preserve the sizeof type annotation
1025 static_cast<const typet &>(operand.find(ID_C_c_sizeof_type));
1026
1027 if(op_type_id==ID_integer ||
1029 {
1030 // from integer to ...
1031
1033
1035 {
1036 return make_boolean_expr(int_value != 0);
1037 }
1038
1044 {
1046 }
1047 else if(expr_type_id == ID_c_enum_tag)
1048 {
1049 const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
1050 if(!c_enum_type.is_incomplete()) // possibly incomplete
1051 {
1053 tmp.type() = expr_type; // we maintain the tag type
1054 return std::move(tmp);
1055 }
1056 }
1057 }
1058 else if(op_type_id==ID_rational)
1059 {
1060 }
1061 else if(op_type_id==ID_real)
1062 {
1063 }
1064 else if(op_type_id==ID_bool)
1065 {
1074 {
1075 if(operand.is_true())
1076 {
1077 return from_integer(1, expr_type);
1078 }
1079 else if(operand.is_false())
1080 {
1081 return from_integer(0, expr_type);
1082 }
1083 }
1084 else if(expr_type_id==ID_c_enum_tag)
1085 {
1086 const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
1087 if(!c_enum_type.is_incomplete()) // possibly incomplete
1088 {
1089 unsigned int_value = operand.is_true() ? 1u : 0u;
1091 tmp.type()=expr_type; // we maintain the tag type
1092 return std::move(tmp);
1093 }
1094 }
1095 else if(expr_type_id==ID_pointer &&
1096 operand.is_false() &&
1097 config.ansi_c.NULL_is_zero)
1098 {
1100 }
1101 }
1102 else if(op_type_id==ID_unsignedbv ||
1106 {
1108
1110 return unchanged(expr);
1111
1113 {
1114 return make_boolean_expr(int_value != 0);
1115 }
1116
1118 {
1119 return from_integer(int_value != 0, expr_type);
1120 }
1121
1123 {
1125 }
1126
1128 {
1129 if(int_value>=0)
1130 {
1132 }
1133 }
1134
1139 {
1140 auto result = from_integer(int_value, expr_type);
1141
1142 if(c_sizeof_type.is_not_nil())
1143 result.set(ID_C_c_sizeof_type, c_sizeof_type);
1144
1145 return std::move(result);
1146 }
1147
1149 {
1150 const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type));
1151 if(!c_enum_type.is_incomplete()) // possibly incomplete
1152 {
1154 tmp.type()=expr_type; // we maintain the tag type
1155 return std::move(tmp);
1156 }
1157 }
1158
1160 {
1162 }
1163
1165 {
1166 // int to float
1169
1170 fixedbvt f;
1173 return f.to_expr();
1174 }
1175
1177 {
1178 // int to float
1181
1185
1186 return f.to_expr();
1187 }
1188
1190 {
1192 return from_rational(r);
1193 }
1194 }
1195 else if(op_type_id==ID_fixedbv)
1196 {
1199 {
1200 // cast from fixedbv to int
1201 fixedbvt f(to_constant_expr(expr.op()));
1202 return from_integer(f.to_integer(), expr_type);
1203 }
1204 else if(expr_type_id==ID_fixedbv)
1205 {
1206 // fixedbv to fixedbv
1207 fixedbvt f(to_constant_expr(expr.op()));
1209 return f.to_expr();
1210 }
1211 else if(expr_type_id == ID_bv)
1212 {
1213 fixedbvt f{to_constant_expr(expr.op())};
1214 return from_integer(f.get_value(), expr_type);
1215 }
1216 }
1217 else if(op_type_id==ID_floatbv)
1218 {
1219 ieee_floatt f(
1220 to_constant_expr(expr.op()),
1222
1225 {
1226 // cast from float to int
1227 return from_integer(f.to_integer(), expr_type);
1228 }
1229 else if(expr_type_id==ID_floatbv)
1230 {
1231 // float to double or double to float
1233 return f.to_expr();
1234 }
1235 else if(expr_type_id==ID_fixedbv)
1236 {
1240 factor.from_integer(power(2, fixedbv.spec.get_fraction_bits()));
1241 f*=factor;
1242 fixedbv.set_value(f.to_integer());
1243 return fixedbv.to_expr();
1244 }
1245 else if(expr_type_id == ID_bv)
1246 {
1247 return from_integer(f.pack(), expr_type);
1248 }
1249 }
1250 else if(op_type_id==ID_bv)
1251 {
1252 if(
1256 {
1257 const auto width = to_bv_type(op_type).get_width();
1258 const auto int_value = bvrep2integer(value, width, false);
1261 else
1262 {
1264 auto result = from_integer(int_value, ns.follow_tag(tag_type));
1265 result.type() = tag_type;
1266 return std::move(result);
1267 }
1268 }
1269 else if(expr_type_id == ID_floatbv)
1270 {
1271 const auto width = to_bv_type(op_type).get_width();
1272 const auto int_value = bvrep2integer(value, width, false);
1274 ieee_float.unpack(int_value);
1275 return ieee_float.to_expr();
1276 }
1277 else if(expr_type_id == ID_fixedbv)
1278 {
1279 const auto width = to_bv_type(op_type).get_width();
1280 const auto int_value = bvrep2integer(value, width, false);
1282 fixedbv.set_value(int_value);
1283 return fixedbv.to_expr();
1284 }
1285 }
1286 else if(op_type_id==ID_c_enum_tag) // enum to int
1287 {
1288 const typet &base_type =
1289 ns.follow_tag(to_c_enum_tag_type(op_type)).underlying_type();
1290 if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv)
1291 {
1292 // enum constants use the representation of their base type
1293 auto new_expr = expr;
1294 new_expr.op().type() = base_type;
1295 return changed(simplify_typecast(new_expr)); // recursive call
1296 }
1297 }
1298 else if(op_type_id==ID_c_enum) // enum to int
1299 {
1300 const typet &base_type = to_c_enum_type(op_type).underlying_type();
1301 if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv)
1302 {
1303 // enum constants use the representation of their base type
1304 auto new_expr = expr;
1305 new_expr.op().type() = base_type;
1306 return changed(simplify_typecast(new_expr)); // recursive call
1307 }
1308 }
1309 }
1310 else if(operand.id()==ID_typecast) // typecast of typecast
1311 {
1312 // (T1)(T2)x ---> (T1)
1313 // where T1 has fewer bits than T2
1314 if(
1317 expr_type_id == ID_bv) &&
1318 to_bitvector_type(expr_type).get_width() <=
1319 to_bitvector_type(operand.type()).get_width())
1320 {
1321 auto new_expr = expr;
1322 new_expr.op() = to_typecast_expr(operand).op();
1323 // might enable further simplification
1324 return changed(simplify_typecast(new_expr)); // recursive call
1325 }
1326 }
1327 else if(operand.id()==ID_address_of)
1328 {
1329 const exprt &o=to_address_of_expr(operand).object();
1330
1331 // turn &array into &array[0] when casting to pointer-to-element-type
1332 if(
1333 o.type().id() == ID_array &&
1334 expr_type == pointer_type(to_array_type(o.type()).element_type()))
1335 {
1336 auto result =
1338
1339 return changed(simplify_address_of(result)); // recursive call
1340 }
1341 }
1343 {
1344 if(
1348 to_bitvector_type(expr_type).get_width() ==
1349 to_bitvector_type(operand.type()).get_width())
1350 {
1352 result.type() = expr_type;
1353 return changed(simplify_extractbits(result));
1354 }
1355 }
1356
1357 return unchanged(expr);
1358}
1359
1362{
1363 const typet &expr_type = expr.type();
1364 const typet &op_type = expr.op().type();
1365
1366 // (T)(a?b:c) --> a?(T)b:(T)c; don't do this for floating-point type casts as
1367 // the type cast itself may be costly
1368 if(
1369 expr.op().id() == ID_if && expr_type.id() != ID_floatbv &&
1370 op_type.id() != ID_floatbv)
1371 {
1372 if_exprt if_expr = lift_if(expr, 0);
1374 }
1375 else
1376 {
1377 auto r_it = simplify_rec(expr.op()); // recursive call
1378 if(r_it.has_changed())
1379 {
1380 auto tmp = expr;
1381 tmp.op() = r_it.expr;
1382 return tmp;
1383 }
1384 }
1385
1386 return unchanged(expr);
1387}
1388
1391{
1392 const exprt &pointer = expr.pointer();
1393
1394 if(pointer.type().id()!=ID_pointer)
1395 return unchanged(expr);
1396
1397 if(pointer.id()==ID_address_of)
1398 {
1399 exprt tmp=to_address_of_expr(pointer).object();
1400 // one address_of is gone, try again
1401 return changed(simplify_rec(tmp));
1402 }
1403 // rewrite *(&a[0] + x) to a[x]
1404 else if(
1405 pointer.id() == ID_plus && pointer.operands().size() == 2 &&
1406 to_plus_expr(pointer).op0().id() == ID_address_of)
1407 {
1408 const auto &pointer_plus_expr = to_plus_expr(pointer);
1409
1412
1413 if(address_of.object().id()==ID_index)
1414 {
1415 const index_exprt &old=to_index_expr(address_of.object());
1416 if(old.array().type().id() == ID_array)
1417 {
1418 index_exprt idx(
1419 old.array(),
1421 to_array_type(old.array().type()).element_type());
1422 return changed(simplify_rec(idx));
1423 }
1424 }
1425 }
1426
1427 return unchanged(expr);
1428}
1429
1432{
1433 const exprt &pointer = expr.pointer();
1434
1435 if(pointer.id() == ID_if)
1436 {
1437 if_exprt if_expr = lift_if(expr, 0);
1439 }
1440 else
1441 {
1442 auto r_it = simplify_rec(pointer); // recursive call
1443 if(r_it.has_changed())
1444 {
1445 auto tmp = expr;
1446 tmp.pointer() = r_it.expr;
1447 return tmp;
1448 }
1449 }
1450
1451 return unchanged(expr);
1452}
1453
1456{
1457 return unchanged(expr);
1458}
1459
1461{
1462 // now look at first operand
1463
1464 if(
1465 expr.old().type().id() == ID_struct ||
1466 expr.old().type().id() == ID_struct_tag)
1467 {
1468 if(expr.old().id() == ID_struct || expr.old().is_constant())
1469 {
1470 const irep_idt &component_name = expr.where().get(ID_component_name);
1471
1473 expr.old().type().id() == ID_struct_tag
1474 ? ns.follow_tag(to_struct_tag_type(expr.old().type()))
1475 : to_struct_type(expr.old().type());
1476 if(!old_type_followed.has_component(component_name))
1477 return unchanged(expr);
1478
1479 std::size_t number = old_type_followed.component_number(component_name);
1480
1481 if(number >= expr.old().operands().size())
1482 return unchanged(expr);
1483
1484 exprt result = expr.old();
1485 result.operands()[number] = expr.new_value();
1486 return result;
1487 }
1488 }
1489 else if(
1490 expr.old().type().id() == ID_array || expr.old().type().id() == ID_vector)
1491 {
1492 if(
1493 expr.old().id() == ID_array || expr.old().is_constant() ||
1494 expr.old().id() == ID_vector)
1495 {
1496 const auto i = numeric_cast<mp_integer>(expr.where());
1497
1498 if(i.has_value() && *i >= 0 && *i < expr.old().operands().size())
1499 {
1500 exprt result = expr.old();
1501 result.operands()[numeric_cast_v<std::size_t>(*i)] = expr.new_value();
1502 return result;
1503 }
1504 }
1505 }
1506
1507 return unchanged(expr);
1508}
1509
1512{
1513 // this is to push updates into (possibly nested) constants
1514
1515 const exprt::operandst &designator = expr.designator();
1516
1517 exprt updated_value = expr.old();
1519
1520 for(const auto &e : designator)
1521 {
1522 if(e.id()==ID_index_designator &&
1523 value_ptr->id()==ID_array)
1524 {
1525 const auto i = numeric_cast<mp_integer>(to_index_designator(e).index());
1526
1527 if(!i.has_value())
1528 return unchanged(expr);
1529
1530 if(*i < 0 || *i >= value_ptr->operands().size())
1531 return unchanged(expr);
1532
1534 }
1535 else if(e.id()==ID_member_designator &&
1536 value_ptr->id()==ID_struct)
1537 {
1538 const irep_idt &component_name=
1539 e.get(ID_component_name);
1541 value_ptr->type().id() == ID_struct_tag
1542 ? ns.follow_tag(to_struct_tag_type(value_ptr->type()))
1543 : to_struct_type(value_ptr->type());
1544 if(!value_ptr_struct_type.has_component(component_name))
1545 return unchanged(expr);
1547 value_ptr = &designator_as_struct_expr.component(component_name, ns);
1548 CHECK_RETURN(value_ptr->is_not_nil());
1549 }
1550 else
1551 return unchanged(expr); // give up, unknown designator
1552 }
1553
1554 // found, done
1555 *value_ptr = expr.new_value();
1556 return updated_value;
1557}
1558
1560{
1561 if(expr.id()==ID_plus)
1562 {
1563 if(expr.type().id()==ID_pointer)
1564 {
1565 // kill integers from sum
1566 for(auto &op : expr.operands())
1567 if(op.type().id() == ID_pointer)
1568 return changed(simplify_object(op)); // recursive call
1569 }
1570 }
1571 else if(expr.id()==ID_typecast)
1572 {
1573 auto const &typecast_expr = to_typecast_expr(expr);
1574 const typet &op_type = typecast_expr.op().type();
1575
1576 if(op_type.id()==ID_pointer)
1577 {
1578 // cast from pointer to pointer
1579 return changed(simplify_object(typecast_expr.op())); // recursive call
1580 }
1581 else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
1582 {
1583 // cast from integer to pointer
1584
1585 // We do a bit of special treatment for (TYPE *)(a+(int)&o) and
1586 // (TYPE *)(a+(int)((T*)&o+x)), which are re-written to '&o'.
1587
1588 const exprt &casted_expr = typecast_expr.op();
1589 if(casted_expr.id() == ID_plus && casted_expr.operands().size() == 2)
1590 {
1591 const auto &plus_expr = to_plus_expr(casted_expr);
1592
1593 const exprt &cand = plus_expr.op0().id() == ID_typecast
1594 ? plus_expr.op0()
1595 : plus_expr.op1();
1596
1597 if(cand.id() == ID_typecast)
1598 {
1599 const auto &typecast_op = to_typecast_expr(cand).op();
1600
1601 if(typecast_op.id() == ID_address_of)
1602 {
1603 return typecast_op;
1604 }
1605 else if(
1606 typecast_op.id() == ID_plus && typecast_op.operands().size() == 2 &&
1607 to_plus_expr(typecast_op).op0().id() == ID_typecast &&
1608 to_typecast_expr(to_plus_expr(typecast_op).op0()).op().id() ==
1610 {
1611 return to_typecast_expr(to_plus_expr(typecast_op).op0()).op();
1612 }
1613 }
1614 }
1615 }
1616 }
1617 else if(expr.id()==ID_address_of)
1618 {
1619 const auto &object = to_address_of_expr(expr).object();
1620
1621 if(object.id() == ID_index)
1622 {
1623 // &some[i] -> &some
1624 address_of_exprt new_expr(to_index_expr(object).array());
1625 return changed(simplify_object(new_expr)); // recursion
1626 }
1627 else if(object.id() == ID_member)
1628 {
1629 // &some.f -> &some
1630 address_of_exprt new_expr(to_member_expr(object).compound());
1631 return changed(simplify_object(new_expr)); // recursion
1632 }
1633 }
1634
1635 return unchanged(expr);
1636}
1637
1640{
1641 // lift up any ID_if on the object
1642 if(expr.op().id() == ID_if)
1643 {
1644 if_exprt if_expr = lift_if(expr, 0);
1645 if_expr.true_case() =
1647 if_expr.false_case() =
1649 return changed(simplify_if(if_expr));
1650 }
1651
1652 const auto el_size = pointer_offset_bits(expr.type(), ns);
1653 if(el_size.has_value() && *el_size < 0)
1654 return unchanged(expr);
1655
1656 // byte_extract(byte_extract(root, offset1), offset2) =>
1657 // byte_extract(root, offset1+offset2)
1658 if(expr.op().id()==expr.id())
1659 {
1660 auto tmp = expr;
1661
1662 tmp.offset() = simplify_rec(plus_exprt(
1664 to_byte_extract_expr(expr.op()).offset(), expr.offset().type()),
1665 expr.offset()));
1666 tmp.op() = to_byte_extract_expr(expr.op()).op();
1667
1668 return changed(simplify_byte_extract(tmp)); // recursive call
1669 }
1670
1671 // byte_extract(byte_update(root, offset, value), offset) =>
1672 // value
1673 if(
1674 ((expr.id() == ID_byte_extract_big_endian &&
1675 expr.op().id() == ID_byte_update_big_endian) ||
1676 (expr.id() == ID_byte_extract_little_endian &&
1677 expr.op().id() == ID_byte_update_little_endian)) &&
1678 expr.offset() == to_byte_update_expr(as_const(expr).op()).offset())
1679 {
1680 const auto &op_byte_update = to_byte_update_expr(expr.op());
1681
1682 if(expr.type() == op_byte_update.value().type())
1683 {
1684 return op_byte_update.value();
1685 }
1686 else if(el_size.has_value())
1687 {
1688 const auto update_bits_opt =
1689 pointer_offset_bits(op_byte_update.value().type(), ns);
1690
1691 if(update_bits_opt.has_value() && *el_size <= *update_bits_opt)
1692 {
1693 auto tmp = expr;
1694 tmp.op() = op_byte_update.value();
1695 tmp.offset() = from_integer(0, expr.offset().type());
1696
1697 return changed(simplify_byte_extract(tmp)); // recursive call
1698 }
1699 }
1700 }
1701
1702 auto offset = numeric_cast<mp_integer>(expr.offset());
1703 if(offset.has_value() && *offset < 0)
1704 return unchanged(expr);
1705
1706 // try to simplify byte_extract(byte_update(...))
1707 auto const bu = expr_try_dynamic_cast<byte_update_exprt>(expr.op());
1708 std::optional<mp_integer> update_offset;
1709 if(bu)
1711 if(
1712 offset.has_value() && bu && el_size.has_value() &&
1713 update_offset.has_value())
1714 {
1715 // byte_extract(byte_update(root, offset_u, value), offset_e) so that the
1716 // update does not affect what is being extracted simplifies to
1717 // byte_extract(root, offset_e)
1718 //
1719 // byte_extract(byte_update(root, offset_u, value), offset_e) so that the
1720 // extracted range fully lies within the update value simplifies to
1721 // byte_extract(value, offset_e - offset_u)
1722 if(
1723 *offset * expr.get_bits_per_byte() + *el_size <=
1724 *update_offset * bu->get_bits_per_byte())
1725 {
1726 // extracting before the update
1727 auto tmp = expr;
1728 tmp.op() = bu->op();
1729 return changed(simplify_byte_extract(tmp)); // recursive call
1730 }
1731 else if(
1732 const auto update_size = pointer_offset_bits(bu->value().type(), ns))
1733 {
1734 if(
1735 *offset * expr.get_bits_per_byte() >=
1736 *update_offset * bu->get_bits_per_byte() + *update_size)
1737 {
1738 // extracting after the update
1739 auto tmp = expr;
1740 tmp.op() = bu->op();
1741 return changed(simplify_byte_extract(tmp)); // recursive call
1742 }
1743 else if(
1744 *offset >= *update_offset &&
1745 *offset * expr.get_bits_per_byte() + *el_size <=
1746 *update_offset * bu->get_bits_per_byte() + *update_size)
1747 {
1748 // extracting from the update
1749 auto tmp = expr;
1750 tmp.op() = bu->value();
1751 tmp.offset() =
1752 from_integer(*offset - *update_offset, expr.offset().type());
1753 return changed(simplify_byte_extract(tmp)); // recursive call
1754 }
1755 }
1756 }
1757
1758 // don't do any of the following if endianness doesn't match, as
1759 // bytes need to be swapped
1760 if(
1761 offset.has_value() && *offset == 0 &&
1762 ((expr.id() == ID_byte_extract_little_endian &&
1763 config.ansi_c.endianness ==
1765 (expr.id() == ID_byte_extract_big_endian &&
1766 config.ansi_c.endianness ==
1768 {
1769 // byte extract of full object is object
1770 if(expr.type() == expr.op().type())
1771 {
1772 return expr.op();
1773 }
1774 else if(
1775 expr.type().id() == ID_pointer && expr.op().type().id() == ID_pointer)
1776 {
1777 return typecast_exprt(expr.op(), expr.type());
1778 }
1779 }
1780
1781 if(
1782 (expr.type().id() == ID_union &&
1783 to_union_type(expr.type()).components().empty()) ||
1784 (expr.type().id() == ID_union_tag &&
1785 ns.follow_tag(to_union_tag_type(expr.type())).components().empty()))
1786 {
1787 return empty_union_exprt{expr.type()};
1788 }
1789 else if(
1790 (expr.type().id() == ID_struct &&
1791 to_struct_type(expr.type()).components().empty()) ||
1792 (expr.type().id() == ID_struct_tag &&
1793 ns.follow_tag(to_struct_tag_type(expr.type())).components().empty()))
1794 {
1795 return struct_exprt{{}, expr.type()};
1796 }
1797
1798 // no proper simplification for expr.type()==void
1799 // or types of unknown size
1800 if(!el_size.has_value() || *el_size == 0)
1801 return unchanged(expr);
1802
1803 if(
1804 offset.has_value() && expr.op().id() == ID_array_of &&
1805 to_array_of_expr(expr.op()).op().is_constant())
1806 {
1807 const auto const_bits_opt = expr2bits(
1808 to_array_of_expr(expr.op()).op(),
1809 config.ansi_c.endianness ==
1811 ns);
1812
1813 if(!const_bits_opt.has_value())
1814 return unchanged(expr);
1815
1816 std::string const_bits=const_bits_opt.value();
1817
1818 DATA_INVARIANT(!const_bits.empty(), "bit representation must be non-empty");
1819
1820 // double the string until we have sufficiently many bits
1821 while(mp_integer(const_bits.size()) <
1822 *offset * expr.get_bits_per_byte() + *el_size)
1823 {
1825 }
1826
1827 std::string el_bits = std::string(
1828 const_bits,
1831
1832 auto tmp = bits2expr(
1833 el_bits, expr.type(), expr.id() == ID_byte_extract_little_endian, ns);
1834
1835 if(tmp.has_value())
1836 return std::move(*tmp);
1837 }
1838
1839 // in some cases we even handle non-const array_of
1840 if(
1841 offset.has_value() && expr.op().id() == ID_array_of &&
1842 (*offset * expr.get_bits_per_byte()) % (*el_size) == 0 &&
1843 *el_size <=
1844 pointer_offset_bits(to_array_of_expr(expr.op()).what().type(), ns))
1845 {
1846 auto tmp = expr;
1847 tmp.op() = simplify_index(index_exprt(expr.op(), expr.offset()));
1848 tmp.offset() = from_integer(0, expr.offset().type());
1850 }
1851
1852 // extract bits of a constant
1853 const auto bits =
1854 expr2bits(expr.op(), expr.id() == ID_byte_extract_little_endian, ns);
1855
1856 if(
1857 offset.has_value() && bits.has_value() &&
1858 mp_integer(bits->size()) >= *el_size + *offset * expr.get_bits_per_byte())
1859 {
1860 // make sure we don't lose bits with structs containing flexible array
1861 // members
1863 expr.type(),
1864 [&](const typet &type) {
1865 if(type.id() != ID_struct && type.id() != ID_struct_tag)
1866 return false;
1867
1868 const struct_typet &st = type.id() == ID_struct_tag
1869 ? ns.follow_tag(to_struct_tag_type(type))
1870 : to_struct_type(type);
1871 const auto &comps = st.components();
1872 if(comps.empty() || comps.back().type().id() != ID_array)
1873 return false;
1874
1875 if(comps.back().type().get_bool(ID_C_flexible_array_member))
1876 return true;
1877
1878 const auto size =
1879 numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
1880 return !size.has_value() || *size <= 1;
1881 },
1882 ns);
1884 {
1885 std::string bits_cut = std::string(
1886 bits.value(),
1889
1890 auto tmp = bits2expr(
1891 bits_cut, expr.type(), expr.id() == ID_byte_extract_little_endian, ns);
1892
1893 if(tmp.has_value())
1894 return std::move(*tmp);
1895 }
1896 }
1897
1898 // push byte extracts into struct or union expressions, just like
1899 // lower_byte_extract does (this is the same code, except recursive calls use
1900 // simplify rather than lower_byte_extract)
1901 if(expr.op().id() == ID_struct || expr.op().id() == ID_union)
1902 {
1903 if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
1904 {
1905 const struct_typet &struct_type =
1906 expr.type().id() == ID_struct_tag
1907 ? ns.follow_tag(to_struct_tag_type(expr.type()))
1908 : to_struct_type(expr.type());
1909 const struct_typet::componentst &components = struct_type.components();
1910
1911 bool failed = false;
1912 struct_exprt s({}, expr.type());
1913
1914 for(const auto &comp : components)
1915 {
1916 auto component_bits = pointer_offset_bits(comp.type(), ns);
1917
1918 // the next member would be misaligned, abort
1919 if(
1920 !component_bits.has_value() || *component_bits == 0 ||
1921 *component_bits % expr.get_bits_per_byte() != 0)
1922 {
1923 failed = true;
1924 break;
1925 }
1926
1927 auto member_offset_opt =
1928 member_offset_expr(struct_type, comp.get_name(), ns);
1929
1930 if(!member_offset_opt.has_value())
1931 {
1932 failed = true;
1933 break;
1934 }
1935
1937 plus_exprt{expr.offset(),
1939 member_offset_opt.value(), expr.offset().type())});
1940
1941 byte_extract_exprt tmp = expr;
1942 tmp.type() = comp.type();
1943 tmp.offset() = new_offset;
1944
1946 }
1947
1948 if(!failed)
1949 return s;
1950 }
1951 else if(expr.type().id() == ID_union || expr.type().id() == ID_union_tag)
1952 {
1953 const union_typet &union_type =
1954 expr.type().id() == ID_union_tag
1955 ? ns.follow_tag(to_union_tag_type(expr.type()))
1956 : to_union_type(expr.type());
1957 auto widest_member_opt = union_type.find_widest_union_component(ns);
1958 if(widest_member_opt.has_value())
1959 {
1960 byte_extract_exprt be = expr;
1961 be.type() = widest_member_opt->first.type();
1962 return union_exprt{widest_member_opt->first.get_name(),
1964 expr.type()};
1965 }
1966 }
1967 }
1968 else if(expr.op().id() == ID_array)
1969 {
1970 const array_typet &array_type = to_array_type(expr.op().type());
1971 const auto &element_bit_width =
1972 pointer_offset_bits(array_type.element_type(), ns);
1973 if(
1974 offset.has_value() && element_bit_width.has_value() &&
1975 *element_bit_width > 0)
1976 {
1977 if(
1978 *offset > 0 &&
1979 *offset * expr.get_bits_per_byte() % *element_bit_width == 0)
1980 {
1982 (*offset * expr.get_bits_per_byte()) / *element_bit_width);
1984 slice.operands().erase(
1985 slice.operands().begin(),
1986 slice.operands().begin() +
1987 std::min(elements_to_erase, slice.operands().size()));
1988 slice.type().size() =
1989 from_integer(slice.operands().size(), slice.type().size().type());
1990 byte_extract_exprt be = expr;
1991 be.op() = slice;
1992 be.offset() = from_integer(0, expr.offset().type());
1994 }
1995 else if(*offset == 0 && *el_size % *element_bit_width == 0)
1996 {
1997 const auto elements_to_keep =
2000 if(slice.operands().size() > elements_to_keep)
2001 {
2002 slice.operands().resize(elements_to_keep);
2003 slice.type().size() =
2004 from_integer(slice.operands().size(), slice.type().size().type());
2005 byte_extract_exprt be = expr;
2006 be.op() = slice;
2008 }
2009 }
2010 }
2011 }
2012
2013 // try to refine it down to extracting from a member or an index in an array
2014 auto subexpr =
2015 get_subexpression_at_offset(expr.op(), expr.offset(), expr.type(), ns);
2016 if(subexpr.has_value() && subexpr.value() != expr)
2017 return changed(simplify_rec(subexpr.value())); // recursive call
2018
2019 if(can_forward_propagatet(ns)(expr))
2020 return changed(simplify_rec(lower_byte_extract(expr, ns)));
2021
2022 return unchanged(expr);
2023}
2024
2027{
2028 // lift up any ID_if on the object
2029 if(expr.op().id() == ID_if)
2030 {
2031 if_exprt if_expr = lift_if(expr, 0);
2033 }
2034 else
2035 {
2036 std::optional<exprt::operandst> new_operands;
2037
2038 for(std::size_t i = 0; i < expr.operands().size(); ++i)
2039 {
2040 auto r_it = simplify_rec(expr.operands()[i]); // recursive call
2041 if(r_it.has_changed())
2042 {
2043 if(!new_operands.has_value())
2044 new_operands = expr.operands();
2045 (*new_operands)[i] = std::move(r_it.expr);
2046 }
2047 }
2048
2049 if(new_operands.has_value())
2050 {
2051 exprt result = expr;
2052 std::swap(result.operands(), *new_operands);
2053 return result;
2054 }
2055 }
2056
2057 return unchanged(expr);
2058}
2059
2062{
2063 // byte_update(byte_update(root, offset, value), offset, value2) =>
2064 // byte_update(root, offset, value2)
2065 if(
2066 expr.id() == expr.op().id() &&
2067 expr.offset() == to_byte_update_expr(expr.op()).offset() &&
2068 expr.value().type() == to_byte_update_expr(expr.op()).value().type())
2069 {
2070 auto tmp = expr;
2071 tmp.set_op(to_byte_update_expr(expr.op()).op());
2072 return std::move(tmp);
2073 }
2074
2075 const exprt &root = expr.op();
2076 const exprt &offset = expr.offset();
2077 const exprt &value = expr.value();
2078 const auto val_size = pointer_offset_bits(value.type(), ns);
2079 const auto root_size = pointer_offset_bits(root.type(), ns);
2080
2081 const auto matching_byte_extract_id =
2084
2085 // byte update of full object is byte_extract(new value)
2086 if(
2087 offset.is_zero() && val_size.has_value() && *val_size > 0 &&
2088 root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
2089 {
2092 value,
2093 offset,
2094 expr.get_bits_per_byte(),
2095 expr.type());
2096
2098 }
2099
2100 // update bits in a constant
2101 const auto offset_int = numeric_cast<mp_integer>(offset);
2102 if(
2103 root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
2104 *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
2106 {
2107 auto root_bits =
2108 expr2bits(root, expr.id() == ID_byte_update_little_endian, ns);
2109
2110 if(root_bits.has_value())
2111 {
2112 const auto val_bits =
2113 expr2bits(value, expr.id() == ID_byte_update_little_endian, ns);
2114
2115 if(val_bits.has_value())
2116 {
2117 root_bits->replace(
2120 *val_bits);
2121
2122 auto tmp = bits2expr(
2123 *root_bits,
2124 expr.type(),
2126 ns);
2127
2128 if(tmp.has_value())
2129 return std::move(*tmp);
2130 }
2131 }
2132 }
2133
2134 /*
2135 * byte_update(root, offset,
2136 * extract(root, offset) WITH component:=value)
2137 * =>
2138 * byte_update(root, offset + component offset,
2139 * value)
2140 */
2141
2142 if(value.id()==ID_with)
2143 {
2144 const with_exprt &with=to_with_expr(value);
2145
2146 if(with.old().id() == matching_byte_extract_id)
2147 {
2148 const byte_extract_exprt &extract=to_byte_extract_expr(with.old());
2149
2150 /* the simplification can be used only if
2151 root and offset of update and extract
2152 are the same */
2153 if(!(root==extract.op()))
2154 return unchanged(expr);
2155 if(!(offset==extract.offset()))
2156 return unchanged(expr);
2157
2158 if(with.type().id() == ID_struct || with.type().id() == ID_struct_tag)
2159 {
2160 const struct_typet &struct_type =
2161 with.type().id() == ID_struct_tag
2162 ? ns.follow_tag(to_struct_tag_type(with.type()))
2163 : to_struct_type(with.type());
2164 const irep_idt &component_name=with.where().get(ID_component_name);
2165 const typet &c_type = struct_type.get_component(component_name).type();
2166
2167 // is this a bit field?
2168 if(c_type.id() == ID_c_bit_field || c_type.id() == ID_bool)
2169 {
2170 // don't touch -- might not be byte-aligned
2171 }
2172 else
2173 {
2174 // new offset = offset + component offset
2175 auto i = member_offset(struct_type, component_name, ns);
2176 if(i.has_value())
2177 {
2178 exprt compo_offset = from_integer(*i, offset.type());
2180 exprt new_value(with.new_value());
2181 auto tmp = expr;
2182 tmp.set_offset(simplify_node(std::move(new_offset)));
2183 tmp.set_value(std::move(new_value));
2184 return changed(simplify_byte_update(tmp)); // recursive call
2185 }
2186 }
2187 }
2188 else if(with.type().id() == ID_array)
2189 {
2190 auto i =
2191 pointer_offset_size(to_array_type(with.type()).element_type(), ns);
2192 if(i.has_value())
2193 {
2194 const exprt &index=with.where();
2196 simplify_mult(mult_exprt(index, from_integer(*i, index.type())));
2197
2198 // index_offset may need a typecast
2199 if(offset.type() != index.type())
2200 {
2201 index_offset =
2203 }
2204
2206 exprt new_value(with.new_value());
2207 auto tmp = expr;
2208 tmp.set_offset(simplify_plus(std::move(new_offset)));
2209 tmp.set_value(std::move(new_value));
2210 return changed(simplify_byte_update(tmp)); // recursive call
2211 }
2212 }
2213 }
2214 }
2215
2216 // size must be known
2217 if(!val_size.has_value() || *val_size == 0)
2218 return unchanged(expr);
2219
2220 // byte_update(root, offset, value) is with(root, index, value) when root is
2221 // array-typed, the size of value matches the array-element width, and offset
2222 // is guaranteed to be a multiple of the array-element width
2224 {
2225 auto el_size = pointer_offset_bits(array_type->element_type(), ns);
2226
2227 if(el_size.has_value() && *el_size > 0 && *val_size % *el_size == 0)
2228 {
2229 if(
2230 offset_int.has_value() &&
2231 (*offset_int * expr.get_bits_per_byte()) % *el_size == 0)
2232 {
2234 (*offset_int * expr.get_bits_per_byte()) / *el_size;
2236 root,
2237 from_integer(base_offset, array_type->index_type()),
2240 value,
2241 from_integer(0, offset.type()),
2242 expr.get_bits_per_byte(),
2243 array_type->element_type()}};
2245
2246 for(mp_integer i = 1; i < n_elements; ++i)
2247 {
2250 from_integer(base_offset + i, array_type->index_type()),
2253 value,
2255 i * (*el_size / expr.get_bits_per_byte()), offset.type()),
2256 expr.get_bits_per_byte(),
2257 array_type->element_type()}};
2258 }
2259
2261 }
2262 // if we have an offset C + x (where C is a constant) we can try to
2263 // recurse by first looking at the member at offset C
2264 else if(
2265 offset.id() == ID_plus && offset.operands().size() == 2 &&
2266 (to_multi_ary_expr(offset).op0().is_constant() ||
2267 to_multi_ary_expr(offset).op1().is_constant()))
2268 {
2269 const plus_exprt &offset_plus = to_plus_expr(offset);
2270 const auto &const_factor = offset_plus.op0().is_constant()
2271 ? offset_plus.op0()
2272 : offset_plus.op1();
2273 const exprt &other_factor = offset_plus.op0().is_constant()
2274 ? offset_plus.op1()
2275 : offset_plus.op0();
2276
2277 auto tmp = expr;
2278 tmp.set_offset(const_factor);
2280
2281 if(
2282 expr_at_offset_C.id() == ID_with &&
2283 to_with_expr(expr_at_offset_C).where().is_zero())
2284 {
2285 tmp.set_op(to_with_expr(expr_at_offset_C).old());
2286 tmp.set_offset(other_factor);
2288 }
2289 }
2290 else if(
2291 offset.id() == ID_mult && offset.operands().size() == 2 &&
2292 (to_multi_ary_expr(offset).op0().is_constant() ||
2293 to_multi_ary_expr(offset).op1().is_constant()))
2294 {
2295 const mult_exprt &offset_mult = to_mult_expr(offset);
2297 offset_mult.op0().is_constant() ? offset_mult.op0()
2298 : offset_mult.op1()));
2299 const exprt &other_factor = offset_mult.op0().is_constant()
2300 ? offset_mult.op1()
2301 : offset_mult.op0();
2302
2303 if((const_factor * expr.get_bits_per_byte()) % *el_size == 0)
2304 {
2309 other_factor.type())};
2311 root,
2313 base_offset, array_type->index_type()),
2316 value,
2317 from_integer(0, offset.type()),
2318 expr.get_bits_per_byte(),
2319 array_type->element_type()}};
2321 for(mp_integer i = 1; i < n_elements; ++i)
2322 {
2327 array_type->index_type()),
2330 value,
2332 i * (*el_size / expr.get_bits_per_byte()), offset.type()),
2333 expr.get_bits_per_byte(),
2334 array_type->element_type()}};
2335 }
2337 }
2338 }
2339 }
2340 }
2341
2342 // the following require a constant offset
2343 if(!offset_int.has_value() || *offset_int < 0)
2344 return unchanged(expr);
2345
2346 // Are we updating (parts of) a struct? Do individual member updates
2347 // instead, unless there are non-byte-sized bit fields
2348 if(root.type().id() == ID_struct || root.type().id() == ID_struct_tag)
2349 {
2351 result_expr.make_nil();
2352
2353 auto update_size = pointer_offset_size(value.type(), ns);
2354
2355 const struct_typet &struct_type =
2356 root.type().id() == ID_struct_tag
2357 ? ns.follow_tag(to_struct_tag_type(root.type()))
2358 : to_struct_type(root.type());
2359 const struct_typet::componentst &components=
2360 struct_type.components();
2361
2362 for(const auto &component : components)
2363 {
2364 auto m_offset = member_offset(struct_type, component.get_name(), ns);
2365
2367
2368 // can we determine the current offset?
2369 if(!m_offset.has_value())
2370 {
2371 result_expr.make_nil();
2372 break;
2373 }
2374
2375 // is it a byte-sized member?
2376 if(
2377 !m_size_bits.has_value() || *m_size_bits == 0 ||
2378 (*m_size_bits) % expr.get_bits_per_byte() != 0)
2379 {
2380 result_expr.make_nil();
2381 break;
2382 }
2383
2384 mp_integer m_size_bytes = (*m_size_bits) / expr.get_bits_per_byte();
2385
2386 // is that member part of the update?
2388 continue;
2389 // are we done updating?
2390 else if(
2391 update_size.has_value() && *update_size > 0 &&
2393 {
2394 break;
2395 }
2396
2397 if(result_expr.is_nil())
2398 result_expr = as_const(expr).op();
2399
2401 member_name.set(ID_component_name, component.get_name());
2403
2404 // are we updating on member boundaries?
2405 if(
2406 *m_offset < *offset_int ||
2407 (*m_offset == *offset_int && update_size.has_value() &&
2409 {
2411 expr.id(),
2412 member_exprt(root, component.get_name(), component.type()),
2413 from_integer(*offset_int - *m_offset, offset.type()),
2414 value,
2415 expr.get_bits_per_byte());
2416
2417 to_with_expr(result_expr).new_value().swap(v);
2418 }
2419 else if(
2420 update_size.has_value() && *update_size > 0 &&
2422 {
2423 // we don't handle this for the moment
2424 result_expr.make_nil();
2425 break;
2426 }
2427 else
2428 {
2431 value,
2432 from_integer(*m_offset - *offset_int, offset.type()),
2433 expr.get_bits_per_byte(),
2434 component.type());
2435
2436 to_with_expr(result_expr).new_value().swap(v);
2437 }
2438 }
2439
2440 if(result_expr.is_not_nil())
2442 }
2443
2444 // replace elements of array or struct expressions, possibly using
2445 // byte_extract
2446 if(root.id()==ID_array)
2447 {
2448 auto el_size =
2449 pointer_offset_bits(to_type_with_subtype(root.type()).subtype(), ns);
2450
2451 if(
2452 !el_size.has_value() || *el_size == 0 ||
2453 (*el_size) % expr.get_bits_per_byte() != 0 ||
2454 (*val_size) % expr.get_bits_per_byte() != 0)
2455 {
2456 return unchanged(expr);
2457 }
2458
2459 exprt result=root;
2460
2462 Forall_operands(it, result)
2463 {
2465 break;
2466
2468 {
2474
2477 value,
2478 from_integer(val_offset, offset.type()),
2479 expr.get_bits_per_byte(),
2482 from_integer(bytes_req, offset.type())));
2483
2484 *it = byte_update_exprt(
2485 expr.id(),
2486 *it,
2489 offset.type()),
2490 new_val,
2491 expr.get_bits_per_byte());
2492
2493 *it = simplify_rec(*it); // recursive call
2494
2496 }
2497
2499 }
2500
2501 return std::move(result);
2502 }
2503
2504 return unchanged(expr);
2505}
2506
2509{
2510 if(expr.id() == ID_complex_real)
2511 {
2513
2514 if(complex_real_expr.op().id() == ID_complex)
2515 return to_complex_expr(complex_real_expr.op()).real();
2516 }
2517 else if(expr.id() == ID_complex_imag)
2518 {
2520
2521 if(complex_imag_expr.op().id() == ID_complex)
2522 return to_complex_expr(complex_imag_expr.op()).imag();
2523 }
2524
2525 return unchanged(expr);
2526}
2527
2530{
2531 // When one operand is zero, an overflow can only occur for a subtraction from
2532 // zero.
2533 if(
2534 expr.op1().is_zero() ||
2535 (expr.op0().is_zero() && !can_cast_expr<minus_overflow_exprt>(expr)))
2536 {
2537 return false_exprt{};
2538 }
2539
2540 // One is neutral element for multiplication
2541 if(
2543 (expr.op0().is_one() || expr.op1().is_one()))
2544 {
2545 return false_exprt{};
2546 }
2547
2548 // we only handle the case of same operand types
2549 if(expr.op0().type() != expr.op1().type())
2550 return unchanged(expr);
2551
2552 // catch some cases over mathematical types
2553 const irep_idt &op_type_id = expr.op0().type().id();
2554 if(
2557 {
2558 return false_exprt{};
2559 }
2560
2562 return false_exprt{};
2563
2564 // we only handle constants over signedbv/unsignedbv for the remaining cases
2566 return unchanged(expr);
2567
2568 if(!expr.op0().is_constant() || !expr.op1().is_constant())
2569 return unchanged(expr);
2570
2571 const auto op0_value = numeric_cast<mp_integer>(expr.op0());
2572 const auto op1_value = numeric_cast<mp_integer>(expr.op1());
2573 if(!op0_value.has_value() || !op1_value.has_value())
2574 return unchanged(expr);
2575
2578 no_overflow_result = *op0_value + *op1_value;
2580 no_overflow_result = *op0_value - *op1_value;
2582 no_overflow_result = *op0_value * *op1_value;
2584 no_overflow_result = *op0_value << *op1_value;
2585 else
2587
2588 const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
2590 if(
2591 no_overflow_result < bv_type.smallest() ||
2592 no_overflow_result > bv_type.largest())
2593 {
2594 return true_exprt{};
2595 }
2596 else
2597 return false_exprt{};
2598}
2599
2602{
2603 // zero is a neutral element for all operations supported here
2604 if(expr.op().is_zero())
2605 return false_exprt{};
2606
2607 // catch some cases over mathematical types
2608 const irep_idt &op_type_id = expr.op().type().id();
2609 if(
2612 {
2613 return false_exprt{};
2614 }
2615
2616 if(op_type_id == ID_natural)
2617 return true_exprt{};
2618
2619 // we only handle constants over signedbv/unsignedbv for the remaining cases
2621 return unchanged(expr);
2622
2623 if(!expr.op().is_constant())
2624 return unchanged(expr);
2625
2626 const auto op_value = numeric_cast<mp_integer>(expr.op());
2627 if(!op_value.has_value())
2628 return unchanged(expr);
2629
2633 else
2635
2636 const std::size_t width = to_bitvector_type(expr.op().type()).get_width();
2638 if(
2639 no_overflow_result < bv_type.smallest() ||
2640 no_overflow_result > bv_type.largest())
2641 {
2642 return true_exprt{};
2643 }
2644 else
2645 return false_exprt{};
2646}
2647
2650{
2652 {
2653 // zero is a neutral element
2654 if(expr.op0().is_zero())
2655 return struct_exprt{{expr.op0(), false_exprt{}}, expr.type()};
2656
2657 // catch some cases over mathematical types
2658 const irep_idt &op_type_id = expr.op0().type().id();
2659 if(
2662 {
2663 return struct_exprt{{expr.op0(), false_exprt{}}, expr.type()};
2664 }
2665
2666 // always an overflow for natural numbers, but the result is not
2667 // representable
2668 if(op_type_id == ID_natural)
2669 return unchanged(expr);
2670
2671 // we only handle constants over signedbv/unsignedbv for the remaining cases
2673 return unchanged(expr);
2674
2675 if(!expr.op0().is_constant())
2676 return unchanged(expr);
2677
2678 const auto op_value = numeric_cast<mp_integer>(expr.op0());
2679 if(!op_value.has_value())
2680 return unchanged(expr);
2681
2683
2684 const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
2686 if(
2687 no_overflow_result < bv_type.smallest() ||
2688 no_overflow_result > bv_type.largest())
2689 {
2690 return struct_exprt{
2692 expr.type()};
2693 }
2694 else
2695 {
2696 return struct_exprt{
2698 expr.type()};
2699 }
2700 }
2701 else
2702 {
2703 // When one operand is zero, an overflow can only occur for a subtraction
2704 // from zero.
2705 if(expr.op0().is_zero())
2706 {
2707 if(
2708 expr.id() == ID_overflow_result_plus ||
2709 expr.id() == ID_overflow_result_shl)
2710 {
2711 return struct_exprt{{expr.op1(), false_exprt{}}, expr.type()};
2712 }
2713 else if(expr.id() == ID_overflow_result_mult)
2714 {
2715 return struct_exprt{
2716 {from_integer(0, expr.op0().type()), false_exprt{}}, expr.type()};
2717 }
2718 }
2719 else if(expr.op1().is_zero())
2720 {
2721 if(
2722 expr.id() == ID_overflow_result_plus ||
2723 expr.id() == ID_overflow_result_minus ||
2724 expr.id() == ID_overflow_result_shl)
2725 {
2726 return struct_exprt{{expr.op0(), false_exprt{}}, expr.type()};
2727 }
2728 else
2729 {
2730 return struct_exprt{
2731 {from_integer(0, expr.op0().type()), false_exprt{}}, expr.type()};
2732 }
2733 }
2734
2735 // One is neutral element for multiplication
2736 if(
2737 expr.id() == ID_overflow_result_mult &&
2738 (expr.op0().is_one() || expr.op1().is_one()))
2739 {
2740 return struct_exprt{
2741 {expr.op0().is_one() ? expr.op1() : expr.op0(), false_exprt{}},
2742 expr.type()};
2743 }
2744
2745 // we only handle the case of same operand types
2746 if(
2747 expr.id() != ID_overflow_result_shl &&
2748 expr.op0().type() != expr.op1().type())
2749 {
2750 return unchanged(expr);
2751 }
2752
2753 // catch some cases over mathematical types
2754 const irep_idt &op_type_id = expr.op0().type().id();
2755 if(
2756 expr.id() != ID_overflow_result_shl &&
2758 op_type_id == ID_real))
2759 {
2760 irep_idt id =
2761 expr.id() == ID_overflow_result_plus
2762 ? ID_plus
2764 return struct_exprt{
2765 {simplify_node(binary_exprt{expr.op0(), id, expr.op1()}),
2766 false_exprt{}},
2767 expr.type()};
2768 }
2769
2770 if(
2771 (expr.id() == ID_overflow_result_plus ||
2772 expr.id() == ID_overflow_result_mult) &&
2774 {
2775 return struct_exprt{
2777 expr.op0(),
2779 expr.op1()}),
2780 false_exprt{}},
2781 expr.type()};
2782 }
2783
2784 // we only handle constants over signedbv/unsignedbv for the remaining cases
2786 return unchanged(expr);
2787
2788 // a special case of overflow-minus checking with operands (X + n) and X
2789 if(expr.id() == ID_overflow_result_minus)
2790 {
2791 const exprt &tc_op0 = skip_typecast(expr.op0());
2792 const exprt &tc_op1 = skip_typecast(expr.op1());
2793
2795 {
2796 if(skip_typecast(sum->op0()) == tc_op1 && sum->operands().size() == 2)
2797 {
2798 std::optional<exprt> offset;
2799 if(sum->type().id() == ID_pointer)
2800 {
2801 offset = std::move(simplify_pointer_offset(
2802 pointer_offset_exprt{*sum, expr.op0().type()})
2803 .expr);
2804 if(offset->id() == ID_pointer_offset)
2805 return unchanged(expr);
2806 }
2807 else
2808 offset = std::move(
2809 simplify_typecast(typecast_exprt{sum->op1(), expr.op0().type()})
2810 .expr);
2811
2812 exprt offset_op = skip_typecast(*offset);
2813 if(
2814 offset_op.type().id() != ID_signedbv &&
2815 offset_op.type().id() != ID_unsignedbv)
2816 {
2817 return unchanged(expr);
2818 }
2819
2820 const std::size_t width =
2821 to_bitvector_type(expr.op0().type()).get_width();
2823
2826 offset_op,
2827 ID_lt,
2828 from_integer(bv_type.smallest(), offset_op.type())},
2830 offset_op,
2831 ID_gt,
2832 from_integer(bv_type.largest(), offset_op.type())}};
2833
2834 return struct_exprt{
2835 {*offset, simplify_rec(not_representable)}, expr.type()};
2836 }
2837 }
2838 }
2839
2840 if(!expr.op0().is_constant() || !expr.op1().is_constant())
2841 return unchanged(expr);
2842
2843 // preserve the sizeof type annotation
2844 std::optional<typet> c_sizeof_type;
2845 for(const auto &op : expr.operands())
2846 {
2847 const typet &sizeof_type =
2848 static_cast<const typet &>(op.find(ID_C_c_sizeof_type));
2849 if(sizeof_type.is_not_nil())
2850 {
2852 break;
2853 }
2854 }
2855
2856 const auto op0_value = numeric_cast<mp_integer>(expr.op0());
2857 const auto op1_value = numeric_cast<mp_integer>(expr.op1());
2858 if(!op0_value.has_value() || !op1_value.has_value())
2859 return unchanged(expr);
2860
2862 if(expr.id() == ID_overflow_result_plus)
2863 no_overflow_result = *op0_value + *op1_value;
2864 else if(expr.id() == ID_overflow_result_minus)
2865 no_overflow_result = *op0_value - *op1_value;
2866 else if(expr.id() == ID_overflow_result_mult)
2867 no_overflow_result = *op0_value * *op1_value;
2868 else if(expr.id() == ID_overflow_result_shl)
2869 no_overflow_result = *op0_value << *op1_value;
2870 else
2872
2875 if(c_sizeof_type.has_value())
2877
2878 const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
2880 if(
2881 no_overflow_result < bv_type.smallest() ||
2882 no_overflow_result > bv_type.largest())
2883 {
2884 return struct_exprt{
2885 {std::move(no_overflow_result_expr), true_exprt{}}, expr.type()};
2886 }
2887 else
2888 {
2889 return struct_exprt{
2890 {std::move(no_overflow_result_expr), false_exprt{}}, expr.type()};
2891 }
2892 }
2893}
2894
2897{
2898 auto result = unchanged(expr);
2899
2900 // The ifs below could one day be replaced by a switch()
2901
2902 if(expr.id()==ID_address_of)
2903 {
2904 // the argument of this expression needs special treatment
2905 }
2906 else if(expr.id()==ID_if)
2907 {
2908 result = simplify_if_preorder(to_if_expr(expr));
2909 }
2910 else if(expr.id() == ID_typecast)
2911 {
2913 }
2914 else if(
2917 {
2919 }
2920 else if(expr.id() == ID_dereference)
2921 {
2923 }
2924 else if(expr.id() == ID_index)
2925 {
2926 result = simplify_index_preorder(to_index_expr(expr));
2927 }
2928 else if(expr.id() == ID_member)
2929 {
2931 }
2932 else if(
2933 expr.id() == ID_is_dynamic_object || expr.id() == ID_is_invalid_pointer ||
2934 expr.id() == ID_object_size || expr.id() == ID_pointer_object ||
2935 expr.id() == ID_pointer_offset)
2936 {
2938 }
2939 else if(expr.has_operands())
2940 {
2941 std::optional<exprt::operandst> new_operands;
2942
2943 for(std::size_t i = 0; i < expr.operands().size(); ++i)
2944 {
2945 auto r_it = simplify_rec(expr.operands()[i]); // recursive call
2946 if(r_it.has_changed())
2947 {
2948 if(!new_operands.has_value())
2949 new_operands = expr.operands();
2950 (*new_operands)[i] = std::move(r_it.expr);
2951 }
2952 }
2953
2954 if(new_operands.has_value())
2955 {
2956 std::swap(result.expr.operands(), *new_operands);
2957 result.expr_changed = resultt<>::CHANGED;
2958 }
2959 }
2960
2961 if(as_const(result.expr).type().id() == ID_array)
2962 {
2963 const array_typet &array_type = to_array_type(as_const(result.expr).type());
2965 if(simp_size.has_changed())
2966 {
2967 to_array_type(result.expr.type()).size() = simp_size.expr;
2968 result.expr_changed = resultt<>::CHANGED;
2969 }
2970 }
2971
2972 return result;
2973}
2974
2976{
2977 if(!node.has_operands())
2978 return unchanged(node); // no change
2979
2980 // #define DEBUGX
2981
2982#ifdef DEBUGX
2983 exprt old(node);
2984#endif
2985
2986 exprt expr = node;
2988
2989 resultt<> r = unchanged(expr);
2990
2991 if(expr.id()==ID_typecast)
2992 {
2994 }
2995 else if(expr.id()==ID_equal || expr.id()==ID_notequal ||
2996 expr.id()==ID_gt || expr.id()==ID_lt ||
2997 expr.id()==ID_ge || expr.id()==ID_le)
2998 {
3000 }
3001 else if(expr.id()==ID_if)
3002 {
3003 r = simplify_if(to_if_expr(expr));
3004 }
3005 else if(expr.id()==ID_lambda)
3006 {
3008 }
3009 else if(expr.id()==ID_with)
3010 {
3011 r = simplify_with(to_with_expr(expr));
3012 }
3013 else if(expr.id()==ID_update)
3014 {
3016 }
3017 else if(expr.id()==ID_index)
3018 {
3020 }
3021 else if(expr.id()==ID_member)
3022 {
3024 }
3025 else if(expr.id()==ID_byte_update_little_endian ||
3027 {
3029 }
3030 else if(expr.id()==ID_byte_extract_little_endian ||
3032 {
3034 }
3035 else if(expr.id()==ID_pointer_object)
3036 {
3038 }
3039 else if(expr.id() == ID_is_dynamic_object)
3040 {
3042 }
3043 else if(expr.id() == ID_is_invalid_pointer)
3044 {
3046 }
3047 else if(
3049 {
3051 }
3052 else if(expr.id()==ID_div)
3053 {
3054 r = simplify_div(to_div_expr(expr));
3055 }
3056 else if(expr.id()==ID_mod)
3057 {
3058 r = simplify_mod(to_mod_expr(expr));
3059 }
3060 else if(expr.id()==ID_bitnot)
3061 {
3063 }
3064 else if(
3065 expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_bitxor ||
3066 expr.id() == ID_bitxnor)
3067 {
3069 }
3070 else if(expr.id()==ID_ashr || expr.id()==ID_lshr || expr.id()==ID_shl)
3071 {
3073 }
3074 else if(expr.id()==ID_power)
3075 {
3077 }
3078 else if(expr.id()==ID_plus)
3079 {
3080 r = simplify_plus(to_plus_expr(expr));
3081 }
3082 else if(expr.id()==ID_minus)
3083 {
3085 }
3086 else if(expr.id()==ID_mult)
3087 {
3088 r = simplify_mult(to_mult_expr(expr));
3089 }
3090 else if(expr.id()==ID_floatbv_plus ||
3091 expr.id()==ID_floatbv_minus ||
3092 expr.id()==ID_floatbv_mult ||
3093 expr.id()==ID_floatbv_div)
3094 {
3096 }
3097 else if(expr.id() == ID_floatbv_round_to_integral)
3098 {
3101 }
3102 else if(expr.id()==ID_floatbv_typecast)
3103 {
3105 }
3106 else if(expr.id()==ID_unary_minus)
3107 {
3109 }
3110 else if(expr.id()==ID_unary_plus)
3111 {
3113 }
3114 else if(expr.id()==ID_not)
3115 {
3116 r = simplify_not(to_not_expr(expr));
3117 }
3118 else if(expr.id()==ID_implies ||
3119 expr.id()==ID_or || expr.id()==ID_xor ||
3120 expr.id()==ID_and)
3121 {
3122 r = simplify_boolean(expr);
3123 }
3124 else if(expr.id()==ID_dereference)
3125 {
3127 }
3128 else if(expr.id()==ID_address_of)
3129 {
3131 }
3132 else if(expr.id()==ID_pointer_offset)
3133 {
3135 }
3136 else if(expr.id()==ID_extractbit)
3137 {
3139 }
3140 else if(expr.id()==ID_concatenation)
3141 {
3143 }
3144 else if(expr.id()==ID_extractbits)
3145 {
3147 }
3148 else if(expr.id() == ID_zero_extend)
3149 {
3151 }
3152 else if(expr.id()==ID_ieee_float_equal ||
3153 expr.id()==ID_ieee_float_notequal)
3154 {
3156 }
3157 else if(expr.id() == ID_bswap)
3158 {
3160 }
3161 else if(expr.id()==ID_isinf)
3162 {
3164 }
3165 else if(expr.id()==ID_isnan)
3166 {
3168 }
3169 else if(expr.id()==ID_isnormal)
3170 {
3172 }
3173 else if(expr.id()==ID_abs)
3174 {
3175 r = simplify_abs(to_abs_expr(expr));
3176 }
3177 else if(expr.id()==ID_sign)
3178 {
3179 r = simplify_sign(to_sign_expr(expr));
3180 }
3181 else if(expr.id() == ID_popcount)
3182 {
3184 }
3185 else if(expr.id() == ID_count_leading_zeros)
3186 {
3188 }
3189 else if(expr.id() == ID_count_trailing_zeros)
3190 {
3192 }
3193 else if(expr.id() == ID_find_first_set)
3194 {
3196 }
3197 else if(expr.id() == ID_function_application)
3198 {
3200 }
3201 else if(expr.id() == ID_complex_real || expr.id() == ID_complex_imag)
3202 {
3204 }
3205 else if(
3206 const auto binary_overflow =
3208 {
3210 }
3211 else if(
3212 const auto unary_overflow =
3214 {
3216 }
3217 else if(
3218 const auto overflow_result =
3220 {
3222 }
3223 else if(expr.id() == ID_bitreverse)
3224 {
3226 }
3227 else if(
3228 const auto prophecy_r_or_w_ok =
3230 {
3232 }
3233 else if(
3234 const auto prophecy_pointer_in_range =
3236 {
3238 }
3239 else if(expr.id() == ID_exists || expr.id() == ID_forall)
3240 {
3242 }
3243
3245 r = changed(r);
3246
3247#ifdef DEBUGX
3248 if(
3249 r.has_changed()
3251 && debug_on
3252# endif
3253 )
3254 {
3255 std::cout << "===== " << node.id() << ": " << format(node) << '\n'
3256 << " ---> " << format(r.expr) << '\n';
3257 }
3258#endif
3259
3260 return r;
3261}
3262
3264{
3265 // look up in cache
3266
3267 #ifdef USE_CACHE
3268 std::pair<simplify_expr_cachet::containert::iterator, bool>
3270 insert(std::pair<exprt, exprt>(expr, exprt()));
3271
3272 if(!cache_result.second) // found!
3273 {
3274 const exprt &new_expr=cache_result.first->second;
3275
3276 if(new_expr.id().empty())
3277 return true; // no change
3278
3279 expr=new_expr;
3280 return false;
3281 }
3282 #endif
3283
3284 // We work on a copy to prevent unnecessary destruction of sharing.
3286
3288
3289 if(
3290 !simplify_node_result.has_changed() &&
3291 simplify_node_preorder_result.has_changed())
3292 {
3293 simplify_node_result.expr_changed =
3294 simplify_node_preorder_result.expr_changed;
3295 }
3296
3297#ifdef USE_LOCAL_REPLACE_MAP
3299# if 1
3300 replace_mapt::const_iterator it =
3302 if(it!=local_replace_map.end())
3303 simplify_node_result = changed(it->second);
3304# else
3305 if(
3306 !local_replace_map.empty() &&
3308 {
3310 }
3311# endif
3312#endif
3313
3314 if(!simplify_node_result.has_changed())
3315 {
3316 return unchanged(expr);
3317 }
3318 else
3319 {
3321 (as_const(simplify_node_result.expr).type().id() == ID_array &&
3322 expr.type().id() == ID_array) ||
3323 as_const(simplify_node_result.expr).type() == expr.type(),
3324 simplify_node_result.expr.pretty(),
3325 expr.pretty());
3326
3327#ifdef USE_CACHE
3328 // save in cache
3329 cache_result.first->second = simplify_node_result.expr;
3330#endif
3331
3332 return simplify_node_result;
3333 }
3334}
3335
3338{
3339#ifdef DEBUG_ON_DEMAND
3340 if(debug_on)
3341 std::cout << "TO-SIMP " << format(expr) << "\n";
3342#endif
3343 auto result = simplify_rec(expr);
3344#ifdef DEBUG_ON_DEMAND
3345 if(debug_on)
3346 std::cout << "FULLSIMP " << format(result.expr) << "\n";
3347#endif
3348 if(result.has_changed())
3349 {
3350 expr = result.expr;
3351 return false; // change
3352 }
3353 else
3354 return true; // no change
3355}
3356
3358bool simplify(exprt &expr, const namespacet &ns)
3359{
3360 return simplify_exprt(ns).simplify(expr);
3361}
3362
3364{
3365 simplify_exprt(ns).simplify(src);
3366 return src;
3367}
configt config
Definition config.cpp:25
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const zero_extend_exprt & to_zero_extend_expr(const exprt &expr)
Cast an exprt to a zero_extend_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition bmc_util.cpp:193
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition c_types.h:377
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
Absolute value.
Definition std_expr.h:442
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
ait()
Definition ai.h:565
Array constructor from list of elements.
Definition std_expr.h:1621
Arrays with given size.
Definition std_types.h:807
A base class for binary expressions.
Definition std_expr.h:638
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
Expression of type type extracted from some object op starting at position offset (given in number of...
std::size_t get_bits_per_byte() const
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & offset() const
const exprt & op() const
std::size_t get_bits_per_byte() const
const exprt & value() const
The C/C++ Booleans.
Definition c_types.h:97
C enum tag type, i.e., c_enum_typet with an identifier.
Definition c_types.h:352
Determine whether an expression is constant.
Definition expr_util.h:87
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition std_expr.h:3118
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Union constructor to support unions without any member (a GCC/Clang feature).
Definition std_expr.h:1834
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_one() const
Return whether the expression is a constant representing 1.
Definition expr.cpp:96
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:91
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition std_expr.h:3200
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
Fixed-width bit-vector with signed fixed-point interpretation.
fixedbv_spect spec
Definition fixedbv.h:44
void from_integer(const mp_integer &i)
Definition fixedbv.cpp:32
mp_integer to_integer() const
Definition fixedbv.cpp:37
void round(const fixedbv_spect &dest_spec)
Definition fixedbv.cpp:52
constant_exprt to_expr() const
Definition fixedbv.cpp:43
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
An IEEE 754 floating-point value, including specificiation.
Definition ieee_float.h:117
void set_sign(bool _sign)
Definition ieee_float.h:160
ieee_float_spect spec
Definition ieee_float.h:119
constant_exprt to_expr() const
mp_integer pack() const
bool get_sign() const
Definition ieee_float.h:254
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
Definition ieee_float.h:338
mp_integer to_integer() const
void from_integer(const mp_integer &i)
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
Definition std_expr.h:2502
Array index operator.
Definition std_expr.h:1470
exprt & index()
Definition std_expr.h:1510
exprt & array()
Definition std_expr.h:1500
Fixed-width bit-vector representing a signed or unsigned integer.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
A (mathematical) lambda expression.
Extract member of struct or union.
Definition std_expr.h:2972
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3209
The null pointer constant.
Boolean OR.
Definition std_expr.h:2275
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
The plus expression Associativity is not specified.
Definition std_expr.h:1002
The offset (in bytes) of a pointer relative to the object.
The popcount (counting the number of bits set to 1) expression.
const exprt & length() const
const exprt & content() const
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:596
Fixed-width bit-vector with two's complement interpretation.
resultt simplify_isnan(const unary_exprt &)
resultt simplify_bitwise(const multi_ary_exprt &)
const namespacet & ns
resultt simplify_quantifier_expr(const quantifier_exprt &)
Try to simplify exists/forall to a constant expression.
resultt simplify_div(const div_exprt &)
resultt simplify_byte_extract(const byte_extract_exprt &)
resultt simplify_bitreverse(const bitreverse_exprt &)
Try to simplify bit-reversing to a constant expression.
resultt simplify_abs(const abs_exprt &)
resultt simplify_isnormal(const unary_exprt &)
resultt simplify_dereference(const dereference_exprt &)
resultt simplify_bitnot(const bitnot_exprt &)
resultt simplify_zero_extend(const zero_extend_exprt &)
resultt simplify_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &)
Try to simplify prophecy_{r,w,rw}_ok to a constant expression.
resultt simplify_member_preorder(const member_exprt &)
resultt simplify_popcount(const popcount_exprt &)
static resultt changed(resultt<> result)
resultt simplify_dereference_preorder(const dereference_exprt &)
resultt simplify_unary_pointer_predicate_preorder(const unary_exprt &)
resultt simplify_address_of(const address_of_exprt &)
resultt simplify_if(const if_exprt &)
resultt simplify_node(const exprt &)
resultt simplify_node_preorder(const exprt &)
resultt simplify_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &)
Try to simplify prophecy_pointer_in_range to a constant expression.
resultt simplify_overflow_unary(const unary_overflow_exprt &)
Try to simplify overflow-unary-.
resultt simplify_minus(const minus_exprt &)
resultt simplify_extractbit(const extractbit_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_shifts(const shift_exprt &)
resultt simplify_index_preorder(const index_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_pointer_object(const pointer_object_exprt &)
resultt simplify_boolean(const exprt &)
resultt simplify_object(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
resultt simplify_with(const with_exprt &)
virtual resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_not(const not_exprt &)
resultt simplify_isinf(const unary_exprt &)
resultt simplify_overflow_binary(const binary_overflow_exprt &)
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
resultt simplify_function_application(const function_application_exprt &)
Attempt to simplify mathematical function applications if we have enough information to do so.
resultt simplify_index(const index_exprt &)
resultt simplify_bswap(const bswap_exprt &)
resultt simplify_member(const member_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_byte_update(const byte_update_exprt &)
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
resultt simplify_update(const update_exprt &)
resultt simplify_is_invalid_pointer(const unary_exprt &)
resultt simplify_mod(const mod_exprt &)
resultt simplify_complex(const unary_exprt &)
virtual resultt simplify_pointer_offset(const pointer_offset_exprt &)
resultt simplify_plus(const plus_exprt &)
virtual bool simplify(exprt &expr)
resultt simplify_unary_plus(const unary_plus_exprt &)
resultt simplify_overflow_result(const overflow_result_exprt &)
Try to simplify overflow_result-+, overflow_result-*, overflow_result–, overflow_result-shl,...
resultt simplify_ffs(const find_first_set_exprt &)
Try to simplify find-first-set to a constant expression.
resultt simplify_if_preorder(const if_exprt &expr)
resultt simplify_byte_extract_preorder(const byte_extract_exprt &)
resultt simplify_is_dynamic_object(const unary_exprt &)
resultt simplify_power(const power_exprt &)
resultt simplify_object_size(const object_size_exprt &)
resultt simplify_lambda(const lambda_exprt &)
resultt simplify_concatenation(const concatenation_exprt &)
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
resultt simplify_ctz(const count_trailing_zeros_exprt &)
Try to simplify count-trailing-zeros to a constant expression.
resultt simplify_clz(const count_leading_zeros_exprt &)
Try to simplify count-leading-zeros to a constant expression.
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
resultt simplify_typecast_preorder(const typecast_exprt &)
resultt simplify_sign(const sign_exprt &)
resultt simplify_unary_minus(const unary_minus_exprt &)
resultt simplify_floatbv_round_to_integral(const floatbv_round_to_integral_exprt &)
Struct constructor from list of elements.
Definition std_expr.h:1877
Structure type, corresponds to C style structs.
Definition std_types.h:231
std::vector< componentt > componentst
Definition std_types.h:140
The Boolean constant true.
Definition std_expr.h:3191
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
const exprt & op() const
Definition std_expr.h:391
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
Definition std_expr.h:1770
The union type.
Definition c_types.h:147
Fixed-width bit-vector with unsigned binary interpretation.
Operator to update elements in structs and arrays.
Definition std_expr.h:2783
exprt & old()
Definition std_expr.h:2795
exprt::operandst & designator()
Definition std_expr.h:2809
exprt & new_value()
Definition std_expr.h:2819
Operator to update elements in structs and arrays.
Definition std_expr.h:2603
exprt & new_value()
Definition std_expr.h:2633
exprt & where()
Definition std_expr.h:2623
exprt & old()
Definition std_expr.h:2613
int isalpha(int c)
Definition ctype.c:9
int tolower(int c)
Definition ctype.c:109
int isupper(int c)
Definition ctype.c:90
#define Forall_operands(it, expr)
Definition expr.h:27
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition expr_util.cpp:69
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
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
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const floatbv_round_to_integral_exprt & to_floatbv_round_to_integral_expr(const exprt &expr)
Cast an exprt to a floatbv_round_to_integral_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
static format_containert< T > format(const T &o)
Definition format.h:37
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
static int8_t r
Definition irep_hash.h:60
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const power_exprt & to_power_expr(const exprt &expr)
Cast an exprt to a power_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
Definition mp_arith.cpp:54
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Pointer Logic.
exprt pointer_offset_sum(const exprt &a, const exprt &b)
Pointer Dereferencing.
exprt object_size(const exprt &pointer)
constant_exprt from_rational(const rationalt &a)
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify(exprt &expr, const namespacet &ns)
static simplify_exprt::resultt simplify_string_compare_to(const function_application_exprt &expr, const namespacet &ns)
Simplify String.compareTo function when arguments are constant.
static simplify_exprt::resultt simplify_string_contains(const function_application_exprt &expr, const namespacet &ns)
Simplify String.contains function when arguments are constant.
static simplify_exprt::resultt simplify_string_endswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.endsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_char_at(const function_application_exprt &expr, const namespacet &ns)
Simplify String.charAt function when arguments are constant.
static simplify_exprt::resultt simplify_string_startswith(const function_application_exprt &expr, const namespacet &ns)
Simplify String.startsWith function when arguments are constant.
static simplify_exprt::resultt simplify_string_is_empty(const function_application_exprt &expr, const namespacet &ns)
Simplify String.isEmpty function when arguments are constant.
static bool lower_case_string_expression(array_exprt &string_data)
Take the passed-in constant string array and lower-case every character.
static simplify_exprt::resultt simplify_string_index_of(const function_application_exprt &expr, const namespacet &ns, const bool search_from_end)
Simplify String.indexOf function when arguments are constant.
static simplify_exprt::resultt simplify_string_equals_ignore_case(const function_application_exprt &expr, const namespacet &ns)
Simplify String.equalsIgnorecase function when arguments are constant.
exprt simplify_expr(exprt src, const namespacet &ns)
std::optional< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
std::optional< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
std::optional< 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.
bool join_operands(exprt &expr)
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define POSTCONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:480
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:122
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1900
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1603
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:895
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition std_expr.h:556
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1277
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1137
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1665
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1206
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1041
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition std_expr.h:466
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2582
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition std_expr.h:1086
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:2053
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition std_expr.h:2714
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:2010
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3173
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2484
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2661
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition std_expr.h:1965
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2866
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:514
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition std_expr.h:621
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:29
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
String expressions for the string solver.
refined_string_exprt & to_string_expr(exprt &expr)
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208
#define size_type
Definition unistd.c:186