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