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