CBMC: /home/runner/work/cbmc/cbmc/src/cprover/simplify_state_expr.cpp Source File

CBMC
Loading...
Searching...
No Matches
simplify_state_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Simplify State Expressions
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#include "simplify_state_expr.h"
13
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/expr_util.h>
17#include <util/namespace.h>
18#include <util/pointer_offset_size.h>
19#include <util/pointer_predicates.h>
20#include <util/simplify_expr.h>
21#include <util/std_expr.h>
22#include <util/symbol.h>
23
24#include "may_alias.h"
25#include "may_be_same_object.h"
26#include "sentinel_dll.h"
27#include "state.h"
28
29 std::size_t allocate_counter = 0;
30
31exprt simplify_state_expr_node(
32 exprt,
33 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
34 const namespacet &);
35
36 static bool types_are_compatible(const typet &a, const typet &b)
37{
38 if(a == b)
39 return true;
40 else if(a.id() == ID_pointer && b.id() == ID_pointer)
41 return true;
42 else
43 return false;
44}
45
47 evaluate_exprt evaluate_expr,
48 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
49 const namespacet &ns)
50{
51 PRECONDITION(evaluate_expr.state().id() == ID_update_state);
52
53 const auto &update_state_expr = to_update_state_expr(evaluate_expr.state());
54
55#if 0
56 std::cout << "U: " << format(update_state_expr) << "\n";
57 std::cout << "u: " << format(update_state_expr.address()) << "\n";
58 std::cout << "T: " << format(update_state_expr.address().type()) << "\n";
59 std::cout << "E: " << format(evaluate_expr.address()) << "\n";
60 std::cout << "T: " << format(evaluate_expr.address().type()) << "\n";
61#endif
62
64 evaluate_expr.address(), update_state_expr.address(), address_taken, ns);
65
66#if 0
67 if(may_alias.has_value())
68 std::cout << "M: " << format(*may_alias) << "\n";
69 else
70 std::cout << "M: ?\n";
71#endif
72
73 if(may_alias.has_value())
74 {
75 // 'simple' case
76 if(*may_alias == true)
77 {
78 // The object is known to be the same.
79 // (ς[A:=V])(A) --> V
82 update_state_expr.new_value(), evaluate_expr.type()),
84 ns);
85 }
86 else if(*may_alias == false)
87 {
88 // The object is known to be different.
89 // (ς[❝x❞:=V])(❝y❞) --> ς(❝y❞)
90 // It might be possible to further simplify ς(❝y❞).
92 evaluate_expr.with_state(update_state_expr.state()), address_taken, ns);
93 }
94 else
95 {
96 // The object may or may not be the same.
97 // (ς[A:=V])(B) --> if cond then V else ς(B) endif
100 evaluate_expr.with_state(update_state_expr.state());
102 new_evaluate_expr, address_taken, ns); // rec. call
103 auto if_expr = if_exprt(
104 std::move(simplified_cond),
107 update_state_expr.new_value(), evaluate_expr.type()),
109 ns),
111 return simplify_expr(if_expr, ns);
112 }
113 }
114
115 auto new_evaluate_expr = evaluate_expr.with_state(update_state_expr.state());
118
119 // Types are compatible?
121 update_state_expr.new_value().type(), evaluate_expr.type()))
122 {
123 // Disregard case where the two memory regions overlap.
124 //
125 // (ς[w:=v])(r) -->
126 // IF same_object(w, r) ∧ offset(w) = offset(r) THEN
127 // v
128 // ELSE
129 // ς(r)
130 // ENDIF
131 auto same_object =
132 ::same_object(evaluate_expr.address(), update_state_expr.address());
133
136
138 pointer_offset(evaluate_expr.address()), address_taken, ns);
139
142
144
146
147 auto simplified_same =
149
150 auto new_value = typecast_exprt::conditional_cast(
151 update_state_expr.new_value(), evaluate_expr.type());
152
153 auto if_expr =
155
156 return simplify_expr(if_expr, ns);
157 }
158 else
159 {
160 // Complex case. Types don't match.
162
163#if 0
164 auto object = update_state_expr.new_value();
165
166 auto offset = simplify_state_expr_node(
167 pointer_offset(evaluate_expr.address()), address_taken, ns);
168
169 auto byte_extract = make_byte_extract(object, offset, evaluate_expr.type());
170
171 return if_exprt(
172 std::move(simplified_same_object),
173 std::move(byte_extract),
175#endif
176 }
177}
178
180{
181 // A store does not affect the result.
182 // allocate(ς[A:=V]), size) --> allocate(ς, size)
183 if(src.state().id() == ID_update_state)
184 {
185 // rec. call
186 return simplify_allocate(
187 src.with_state(to_update_state_expr(src.state()).state()));
188 }
189 else if(src.state().id() == ID_enter_scope_state)
190 {
191 // rec. call
192 return simplify_allocate(
193 src.with_state(to_enter_scope_state_expr(src.state()).state()));
194 }
195 else if(src.state().id() == ID_exit_scope_state)
196 {
197 // rec. call
198 return simplify_allocate(
199 src.with_state(to_exit_scope_state_expr(src.state()).state()));
200 }
201
202 return std::move(src);
203}
204
206 evaluate_exprt evaluate_expr,
207 const namespacet &ns)
208{
209 PRECONDITION(evaluate_expr.state().id() == ID_allocate_state);
210
211 // const auto &allocate_expr = to_allocate_expr(evaluate_expr.state());
212
213#if 0
214 // Same address?
215 if(evaluate_expr.address() == allocate_expr.address())
216 {
217# if 0
218 irep_idt identifier = "allocate-" + std::to_string(++allocate_counter);
219 auto object_size = allocate_expr.size();
220 auto object_type = array_typet(char_type(), object_size);
221 auto symbol_expr = symbol_exprt(identifier, object_type);
222 return object_address_exprt(symbol_expr);
223# endif
224 return std::move(evaluate_expr);
225 }
226 else // different
227 {
228 auto new_evaluate_expr = evaluate_expr;
229 new_evaluate_expr.state() = allocate_expr.state();
230 return std::move(new_evaluate_expr);
231 }
232#endif
233 return std::move(evaluate_expr);
234}
235
237 evaluate_exprt evaluate_expr,
238 const namespacet &ns)
239{
240 PRECONDITION(evaluate_expr.state().id() == ID_deallocate_state);
241
242 // deallocate isn't visible to 'evaluate'
243 const auto &deallocate_state_expr =
244 to_deallocate_state_expr(evaluate_expr.state());
245 auto new_evaluate_expr =
246 evaluate_expr.with_state(deallocate_state_expr.state());
247 return std::move(new_evaluate_expr);
248}
249
251 evaluate_exprt evaluate_expr,
252 const namespacet &ns)
253{
254 PRECONDITION(evaluate_expr.state().id() == ID_enter_scope_state);
255
256 const auto &enter_scope_state_expr =
257 to_enter_scope_state_expr(evaluate_expr.state());
258 auto new_evaluate_expr =
259 evaluate_expr.with_state(enter_scope_state_expr.state());
260 return std::move(new_evaluate_expr);
261}
262
264 evaluate_exprt evaluate_expr,
265 const namespacet &ns)
266{
267 PRECONDITION(evaluate_expr.state().id() == ID_exit_scope_state);
268
269 const auto &exit_scope_state_expr =
270 to_exit_scope_state_expr(evaluate_expr.state());
271 auto new_evaluate_expr =
272 evaluate_expr.with_state(exit_scope_state_expr.state());
273 return std::move(new_evaluate_expr);
274}
275
277{
278 if(src.id() == ID_object_address)
279 return src;
280 else if(src.id() == ID_element_address)
282 else if(src.id() == ID_field_address)
284 else if(src.id() == ID_plus)
285 {
286 const auto &plus_expr = to_plus_expr(src);
287 for(auto &op : plus_expr.operands())
288 if(op.type().id() == ID_pointer)
290 return src; // no change
291 }
292 else if(src.id() == ID_typecast)
293 {
294 const auto &op = to_typecast_expr(src).op();
295 if(op.type().id() == ID_pointer)
297 else
298 return src; // no change
299 }
300 else
301 return src;
302}
303
308
311 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
312 const namespacet &ns)
313{
314 const auto &pointer = src.address();
315
316 auto object = simplify_object_expression(pointer);
317
318 if(object.id() == ID_object_address)
319 {
320 auto identifier = to_object_address_expr(object).object_identifier();
321
322 if(identifier.starts_with("allocate-"))
323 {
324 }
325 else if(identifier == "return_value")
326 {
327 return true_exprt(); // never dies
328 }
329 else if(identifier.starts_with("va_args::"))
330 {
331 return true_exprt(); // might be 'dead'
332 }
333 else
334 {
335 const auto &symbol = ns.lookup(identifier);
336 if(symbol.is_static_lifetime)
337 {
338 return true_exprt(); // always live
339 }
340 }
341 }
342
343 // A store does not affect the result.
344 // live_object(ς[A:=V]), p) --> live_object(ς, p)
345 if(src.state().id() == ID_update_state)
346 {
347 src.state() = to_update_state_expr(src.state()).state();
348
349 // rec. call
350 return simplify_live_object_expr(std::move(src), address_taken, ns);
351 }
352 else if(src.state().id() == ID_deallocate_state)
353 {
355 // live_object(deallocate_state(ς, p), q) -->
356 // IF same_object(p, q) THEN false ELSE live_object(ς, q) ENDIF
357 auto same_object = ::same_object(object, deallocate_state_expr.address());
362 return if_exprt(
364 }
365 else if(src.state().id() == ID_enter_scope_state)
366 {
367 // This begins the life of a local-scoped variable.
369 if(
370 address_taken.find(enter_scope_state_expr.symbol()) !=
371 address_taken.end())
372 {
373 // live_object(enter_scope_state(ς, p), q) -->
374 // IF same_object(p, q) THEN true ELSE live_object(ς, q) ENDIF
375 auto same_object =
376 ::same_object(object, enter_scope_state_expr.address());
382 ns);
383 return if_exprt(
385 }
386 else
387 {
388 return simplify_live_object_expr( // rec. call
391 ns);
392 }
393 }
394 else if(src.state().id() == ID_exit_scope_state)
395 {
396 // This ends the life of a local-scoped variable.
398 if(
399 address_taken.find(exit_scope_state_expr.symbol()) != address_taken.end())
400 {
401 // live_object(exit_scope_state(ς, p), q) -->
402 // IF same_object(p, q) THEN false ELSE live_object(ς, q) ENDIF
403 auto same_object = ::same_object(object, exit_scope_state_expr.address());
409 ns);
410 return if_exprt(
412 }
413 else
414 {
415 return simplify_live_object_expr( // rec. call
418 ns);
419 }
420 }
421
422 return std::move(src);
423}
424
427 const namespacet &ns)
428{
429 const auto &pointer = src.address();
430
431 auto object = simplify_object_expression(pointer);
432
433 if(object.id() == ID_object_address)
434 {
435 auto identifier = to_object_address_expr(object).object_identifier();
436
437 if(identifier.starts_with("allocate-"))
438 {
439 }
440 else if(identifier.starts_with("va_args::"))
441 {
442 return true_exprt(); // always writeable
443 }
444 else
445 {
446 const auto &symbol = ns.lookup(identifier);
447 return make_boolean_expr(!symbol.type.get_bool(ID_C_constant));
448 }
449 }
450
451 // A store does not affect the result.
452 // writeable_object(ς[A:=V]), p) --> writeable_object(ς, p)
453 if(src.state().id() == ID_update_state)
454 {
455 src.state() = to_update_state_expr(src.state()).state();
456 return std::move(src);
457 }
458
459 return std::move(src);
460}
461
463{
464 const auto &pointer = src.address();
465
466 auto object = simplify_object_expression(pointer);
467
468 if(object.id() == ID_object_address)
469 {
470 // these are not dynamic
471 return false_exprt();
472 }
473
474 // A store does not affect the result.
475 // is_dynamic_object(ς[A:=V]), p) --> is_dynamic_object(ς, p)
476 if(src.state().id() == ID_update_state)
477 {
478 src.state() = to_update_state_expr(src.state()).state();
479 // rec. call
480 return simplify_is_dynamic_object_expr(std::move(src));
481 }
482 else if(src.state().id() == ID_enter_scope_state)
483 {
485 src.with_state(to_enter_scope_state_expr(src.state()).state()));
486 }
487 else if(src.state().id() == ID_exit_scope_state)
488 {
490 src.with_state(to_exit_scope_state_expr(src.state()).state()));
491 }
492
493 return std::move(src);
494}
495
498 const namespacet &ns)
499{
500 const auto &pointer = src.address();
501
502 auto object = simplify_object_expression(pointer);
503
504 if(object.id() == ID_object_address)
505 {
506 const auto &object_address_expr = to_object_address_expr(object);
507 auto size_opt = size_of_expr(object_address_expr.object_type(), ns);
508 if(size_opt.has_value())
510 else
511 return std::move(src); // no change
512 }
513
514 // A store does not affect the result.
515 // object_size(ς[A:=V]), p) --> object_size(ς, p)
516 if(src.state().id() == ID_update_state)
517 {
518 return src.with_state(to_update_state_expr(src.state()).state());
519 }
520 else if(src.state().id() == ID_exit_scope_state)
521 {
522 return src.with_state(to_exit_scope_state_expr(src.state()).state());
523 }
524
525 return std::move(src);
526}
527
529 state_ok_exprt src,
530 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
531 const namespacet &ns)
532{
533 auto &state = src.state();
534 auto &pointer = src.address();
535 auto &size = src.size();
536
537 if(state.id() == ID_update_state)
538 {
539 // A store does not affect the result.
540 // X_ok(ς[A:=V]), A, S) --> X_ok(ς, A, S)
541 state = to_update_state_expr(state).state();
542
543 // rec. call
544 return simplify_state_expr_node(std::move(src), address_taken, ns);
545 }
546 else if(state.id() == ID_enter_scope_state)
547 {
549
550 // rec. call
553
554#if 0
555 // replace array by array[0]
557 enter_scope_state_expr.object_type().id() == ID_array ?
559 enter_scope_state_expr.address();
560
561 auto may_alias =
563
564 if(may_alias.has_value() && *may_alias == false_exprt())
565 return rec_result;
566
567 auto same_object = ::same_object(pointer, enter_scope_state_expr.address());
568#else
570 pointer, enter_scope_state_expr.address(), address_taken, ns);
571#endif
572
575
576 // Known to be live, only need to check upper bound.
577 // Extend one bit, to cover overflow case.
578 auto size_type = ::size_type();
579 auto size_type_ext = unsignedbv_typet(size_type.get_width() + 1);
580 auto offset = pointer_offset_exprt(pointer, size_type_ext);
582 auto object_size_opt =
583 size_of_expr(enter_scope_state_expr.object_type(), ns);
584 if(!object_size_opt.has_value())
585 return std::move(src);
586
587 auto upper = binary_relation_exprt(
588 plus_exprt(offset, size_casted),
589 ID_le,
591
593
594 auto implication =
596
597 return std::move(implication);
598 }
599 else if(state.id() == ID_exit_scope_state)
600 {
601#if 0
603
604 // rec. call
607
608 auto same_object = ::same_object(pointer, exit_scope_state_expr.address());
609
612
613 // Known to be dead if it's the same object.
614 auto implication =
616
617 return implication;
618#else
620 src.with_state(to_exit_scope_state_expr(state).state()),
622 ns);
623#endif
624 }
625
626 return std::move(src);
627}
628
629#if 0
630static bool is_one(const exprt &src)
631{
632 if(src.id() == ID_typecast)
633 return is_one(to_typecast_expr(src).op());
634 else if(src.is_constant())
635 {
636 auto value_opt = numeric_cast<mp_integer>(src);
637 return value_opt.has_value() && *value_opt == 1;
638 }
639 else
640 return false;
641}
642#endif
643
644 static bool is_a_char_type(const typet &type)
645{
646 return (type.id() == ID_signedbv || type.id() == ID_unsignedbv) &&
647 to_bitvector_type(type).get_width() == char_type().get_width();
648}
649
650 static bool is_zero_char(const exprt &src, const namespacet &ns)
651{
652 if(!is_a_char_type(src.type()))
653 return false;
654
655 auto src_simplified = simplify_expr(src, ns);
656
658
659 return integer_opt.has_value() && *integer_opt == 0;
660}
661
664 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
665 const namespacet &ns)
666{
667 PRECONDITION(src.type().id() == ID_bool);
668 const auto &state = src.state();
669 const auto &pointer = src.address();
670
671 if(state.id() == ID_update_state)
672 {
673 const auto &update_state_expr = to_update_state_expr(state);
674
675 auto cstring_in_old_state = src;
679
680 auto may_alias =
681 ::may_alias(pointer, update_state_expr.address(), address_taken, ns);
682
683 if(may_alias.has_value() && *may_alias == false)
684 {
685 // different objects
686 // cstring(s[x:=v], p) --> cstring(s, p)
688 }
689
690 // maybe the same
691
692 // Are we writing zero?
693 if(update_state_expr.new_value() == 0)
694 {
695 // cstring(s[p:=0], q) --> if p alias q then true else cstring(s, q)
696 auto same_object = ::same_object(pointer, update_state_expr.address());
697
700
701 return if_exprt(
703 }
704 }
705 else if(state.id() == ID_enter_scope_state)
706 {
707 // rec. call
709 src.with_state(to_enter_scope_state_expr(state).state()),
711 ns);
712 }
713 else if(state.id() == ID_exit_scope_state)
714 {
715 // rec. call
717 src.with_state(to_exit_scope_state_expr(state).state()),
719 ns);
720 }
721
722 if(pointer.id() == ID_plus)
723 {
724#if 0
725 auto &plus_expr = to_plus_expr(pointer);
726 if(plus_expr.operands().size() == 2 && is_one(plus_expr.op1()))
727 {
728 // is_cstring(ς, p + 1)) --> is_cstring(ς, p) ∨ ς(p)=0
729 auto new_is_cstring = src;
730 new_is_cstring.op1() = plus_expr.op0();
731 auto type = to_pointer_type(pointer.type()).base_type();
732 auto zero = from_integer(0, type);
733 auto is_zero =
734 equal_exprt(evaluate_exprt(state, plus_expr.op0(), type), zero);
735 return or_exprt(new_is_cstring, is_zero);
736 }
737#endif
738 }
739 else if(
740 pointer.id() == ID_address_of &&
741 to_address_of_expr(pointer).object().id() == ID_string_constant)
742 {
743 // is_cstring(ς, &"...")) --> true
744 return true_exprt();
745 }
746 else if(
747 pointer.id() == ID_element_address &&
748 to_element_address_expr(pointer).base().id() == ID_address_of &&
749 to_address_of_expr(to_element_address_expr(pointer).base()).object().id() ==
751 {
752 // TODO: compare offset to length
753 // is_cstring(ς, element_address(&"...", 0))) --> true
754 return true_exprt();
755 }
756
757 return std::move(src);
758}
759
762 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
763 const namespacet &ns)
764{
765 const auto &state = src.state();
766 const auto &pointer = src.address();
767
768 if(state.id() == ID_update_state)
769 {
770 const auto &update_state_expr = to_update_state_expr(state);
771
775
777 pointer, update_state_expr.address(), address_taken, ns);
778
779 if(may_be_same_object == false)
780 {
781 // different objects
782 // cstrlen(s[x:=v], p) --> cstrlen(s, p)
784 }
785
786 // maybe the same
787
788 // Are we writing zero?
789 if(is_zero_char(update_state_expr.new_value(), ns))
790 {
791 // cstrlen(s[p:=0], p) --> 0
792 if(pointer == update_state_expr.address())
793 return from_integer(0, src.type());
794 }
795 }
796
797 if(pointer.id() == ID_plus)
798 {
799#if 0
800 auto &plus_expr = to_plus_expr(pointer);
801 if(plus_expr.operands().size() == 2 && is_one(plus_expr.op1()))
802 {
803 // is_cstring(ς, p + 1)) --> is_cstring(ς, p) ∨ ς(p)=0
804 auto new_is_cstring = src;
805 new_is_cstring.op1() = plus_expr.op0();
806 auto type = to_pointer_type(pointer.type()).base_type();
807 auto zero = from_integer(0, type);
808 auto is_zero =
809 equal_exprt(evaluate_exprt(state, plus_expr.op0(), type), zero);
810 return or_exprt(new_is_cstring, is_zero);
811 }
812#endif
813 }
814 else if(
815 pointer.id() == ID_address_of &&
816 to_address_of_expr(pointer).object().id() == ID_string_constant)
817 {
818#if 0
819 // is_cstring(ς, &"...")) --> true
820 return true_exprt();
821#endif
822 }
823 else if(
824 pointer.id() == ID_element_address &&
825 to_element_address_expr(pointer).base().id() == ID_address_of &&
826 to_address_of_expr(to_element_address_expr(pointer).base()).object().id() ==
828 {
829#if 0
830 // TODO: compare offset to length
831 // is_cstring(ς, element_address(&"...", 0))) --> true
832 return true_exprt();
833#endif
834 }
835
836 return std::move(src);
837}
838
841 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
842 const namespacet &ns)
843{
844 PRECONDITION(src.type().id() == ID_bool);
845 const auto &state = src.state();
846 const auto &head = src.head();
847 const auto &tail = src.tail();
848
849 {
850 // ς(h.❝n❞) = t ∧ ς(t.❝p❞) = h --> is_sentinel_dll(ς, h, t)
851 auto head_next = sentinel_dll_next(state, head, ns);
852 auto tail_prev = sentinel_dll_prev(state, tail, ns);
853
854 if(head_next.has_value() && tail_prev.has_value())
855 {
856 // rec. calls
861 if(head_next_simplified == tail && tail_prev_simplified == head)
862 return true_exprt();
863 }
864 }
865
866 if(state.id() == ID_update_state)
867 {
868 const auto &update_state_expr = to_update_state_expr(state);
869
870 // are we writing to something that might be a node pointer?
871 const auto &update_type = update_state_expr.new_value().type();
872 if(update_type != src.head().type())
873 {
874 // update is irrelevant, drop update
875 auto without_update = src.with_state(update_state_expr.state());
877 }
878 }
879 else if(state.id() == ID_enter_scope_state)
880 {
882 src.with_state(to_enter_scope_state_expr(state).state()),
884 ns);
885 }
886 else if(state.id() == ID_exit_scope_state)
887 {
889 src.with_state(to_exit_scope_state_expr(state).state()),
891 ns);
892 }
893
894 return std::move(src);
895}
896
899 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
900 const namespacet &ns)
901{
902 if(src.pointer().id() == ID_object_address)
903 {
904 // pointer_offset(❝x❞) -> 0
905 return from_integer(0, src.type());
906 }
907 else if(src.pointer().id() == ID_element_address)
908 {
910 // pointer_offset(element_address(Z, y)) -->
911 // pointer_offset(Z) + y*sizeof(x)
912 auto size_opt = size_of_expr(element_address_expr.element_type(), ns);
913 if(size_opt.has_value())
914 {
915 auto product = mult_exprt(
917 element_address_expr.index(), src.type()),
922 ns);
923 auto sum = plus_exprt(pointer_offset, std::move(product));
924 return std::move(sum);
925 }
926 }
927 else if(src.pointer().id() == ID_address_of)
928 {
929 const auto &address_of_expr = to_address_of_expr(src.pointer());
930 if(address_of_expr.object().id() == ID_string_constant)
931 return from_integer(0, src.type());
932 }
933 else if(src.pointer().id() == ID_typecast)
934 {
935 if(to_typecast_expr(src.pointer()).op().type().id() == ID_pointer)
936 {
937 // remove the typecast
941 ns);
942 }
943 }
944
945 return std::move(src);
946}
947
950 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
951 const namespacet &ns)
952{
954
955 if(src.pointer() != simplified_pointer)
957
958 return std::move(src);
959}
960
962 exprt src,
963 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
964 const namespacet &ns)
965{
966 if(src.id() == ID_allocate)
967 {
969 }
970 else if(src.id() == ID_evaluate)
971 {
972 auto &evaluate_expr = to_evaluate_expr(src);
973
974 if(evaluate_expr.state().id() == ID_update_state)
975 {
976 return simplify_evaluate_update(evaluate_expr, address_taken, ns);
977 }
978 else if(evaluate_expr.state().id() == ID_allocate_state)
979 {
980 return simplify_evaluate_allocate_state(evaluate_expr, ns);
981 }
982 else if(evaluate_expr.state().id() == ID_deallocate_state)
983 {
984 return simplify_evaluate_deallocate_state(evaluate_expr, ns);
985 }
986 else if(evaluate_expr.state().id() == ID_enter_scope_state)
987 {
988 return simplify_evaluate_enter_scope_state(evaluate_expr, ns);
989 }
990 else if(evaluate_expr.state().id() == ID_exit_scope_state)
991 {
992 return simplify_evaluate_exit_scope_state(evaluate_expr, ns);
993 }
994 }
995 else if(
996 src.id() == ID_state_r_ok || src.id() == ID_state_w_ok ||
997 src.id() == ID_state_rw_ok)
998 {
1000 }
1001 else if(src.id() == ID_state_live_object)
1002 {
1005 }
1006 else if(src.id() == ID_state_writeable_object)
1007 {
1010 }
1011 else if(src.id() == ID_state_is_cstring)
1012 {
1015 }
1016 else if(src.id() == ID_state_cstrlen)
1017 {
1019 }
1020 else if(src.id() == ID_state_is_sentinel_dll)
1021 {
1024 }
1025 else if(src.id() == ID_state_is_dynamic_object)
1026 {
1029 }
1030 else if(src.id() == ID_plus)
1031 {
1032 auto &plus_expr = to_plus_expr(src);
1033 if(
1034 src.type().id() == ID_pointer &&
1035 plus_expr.op0().id() == ID_element_address)
1036 {
1037 // element_address(X, Y) + Z --> element_address(X, Y + Z)
1042 plus_expr.op1(), new_element_address_expr.index().type()));
1043 new_element_address_expr.index() =
1047 }
1048 }
1049 else if(src.id() == ID_pointer_offset)
1050 {
1053 }
1054 else if(src.id() == ID_pointer_object)
1055 {
1058 }
1059 else if(src.id() == ID_state_object_size)
1060 {
1062 }
1063 else if(src.id() == ID_equal)
1064 {
1065 const auto &equal_expr = to_equal_expr(src);
1066 if(
1067 equal_expr.lhs().id() == ID_pointer_object &&
1068 equal_expr.rhs().id() == ID_pointer_object)
1069 {
1070 const auto &lhs_p = to_pointer_object_expr(equal_expr.lhs()).pointer();
1071 const auto &rhs_p = to_pointer_object_expr(equal_expr.rhs()).pointer();
1072 if(lhs_p.id() == ID_object_address && rhs_p.id() == ID_object_address)
1073 {
1074 if(
1075 to_object_address_expr(lhs_p).object_identifier() ==
1076 to_object_address_expr(rhs_p).object_identifier())
1077 return true_exprt();
1078 else
1079 return false_exprt();
1080 }
1081 }
1082 }
1083
1084 return src;
1085}
1086
1088 exprt src,
1089 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
1090 const namespacet &ns)
1091{
1092 // operands first, recursively
1093 for(auto &op : src.operands())
1094 op = simplify_state_expr(op, address_taken, ns);
1095
1096 // now the node itself
1098
1099 return src;
1100}
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
bitvector_typet char_type()
Definition c_types.cpp:106
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Definition state.h:218
allocate_exprt with_state(exprt state) const
Definition state.h:246
const exprt & state() const
Definition state.h:230
Boolean AND All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2043
Arrays with given size.
Definition std_types.h:806
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:784
std::size_t get_width() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Operator to return the address of an array element relative to a base address.
Definition pointer_expr.h:748
Equality.
Definition std_expr.h:1339
Definition state.h:78
const exprt & address() const
Definition state.h:110
const exprt & state() const
Definition state.h:100
evaluate_exprt with_state(exprt state) const
Definition state.h:116
Base class for all expressions.
Definition expr.h:57
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:213
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
The Boolean constant false.
Definition std_expr.h:3135
The trinary if-then-else operator.
Definition std_expr.h:2426
const irep_idt & id() const
Definition irep.h:388
Binary multiplication Associativity is not specified.
Definition std_expr.h:1104
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition namespace.cpp:134
Operator to return the address of an object.
Definition pointer_expr.h:596
Boolean OR All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2193
The plus expression Associativity is not specified.
Definition std_expr.h:1006
A numerical identifier for the object a pointer points to.
exprt & pointer()
The offset (in bytes) of a pointer relative to the object.
exprt & pointer()
Definition state.h:634
const exprt & state() const
Definition state.h:647
state_cstrlen_exprt with_state(exprt state) const
Definition state.h:663
const exprt & address() const
Definition state.h:657
Definition state.h:573
const exprt & address() const
Definition state.h:595
const exprt & state() const
Definition state.h:585
state_is_cstring_exprt with_state(exprt state) const
Definition state.h:601
Definition state.h:696
const exprt & state() const
Definition state.h:708
const exprt & address() const
Definition state.h:718
state_is_dynamic_object_exprt with_state(exprt state) const
Definition state.h:724
Definition sentinel_dll.h:15
const exprt & head() const
Definition sentinel_dll.h:49
const exprt & state() const
Definition sentinel_dll.h:39
state_is_sentinel_dll_exprt with_state(exprt state) const
Definition sentinel_dll.h:70
const exprt & tail() const
Definition sentinel_dll.h:59
Definition state.h:456
const exprt & address() const
Definition state.h:478
const exprt & state() const
Definition state.h:468
state_live_object_exprt with_state(exprt state) const
Definition state.h:484
Definition state.h:760
const exprt & state() const
Definition state.h:773
state_object_size_exprt with_state(exprt state) const
Definition state.h:789
const exprt & address() const
Definition state.h:783
Definition state.h:823
state_ok_exprt with_state(exprt state) const
Definition state.h:868
const exprt & size() const
Definition state.h:857
const exprt & address() const
Definition state.h:847
const exprt & state() const
Definition state.h:837
Definition state.h:518
const exprt & address() const
Definition state.h:540
const exprt & state() const
Definition state.h:530
Expression to hold a symbol (variable)
Definition std_expr.h:132
The Boolean constant true.
Definition std_expr.h:3126
Semantic type conversion.
Definition std_expr.h:1995
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2003
The type of an expression, extends irept.
Definition type.h:29
Fixed-width bit-vector with unsigned binary interpretation.
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition expr_util.cpp:308
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition format.h:37
static exprt implication(exprt lhs, exprt rhs)
std::optional< exprt > may_alias(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
Definition may_alias.cpp:221
May Alias.
exprt may_be_same_object(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
May Be Same Object.
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
Definition pointer_expr.h:814
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
Definition pointer_expr.h:643
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition pointer_expr.h:577
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition pointer_expr.h:93
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.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
Definition pointer_expr.h:727
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
std::optional< exprt > sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &ns)
std::optional< exprt > sentinel_dll_next(const exprt &state, const exprt &node, const namespacet &ns)
const state_is_sentinel_dll_exprt & to_state_is_sentinel_dll_expr(const exprt &expr)
Cast an exprt to a state_is_sentinel_dll_exprt.
Definition sentinel_dll.h:85
exprt simplify_expr(exprt src, const namespacet &ns)
exprt simplify_evaluate_enter_scope_state(evaluate_exprt evaluate_expr, const namespacet &ns)
exprt simplify_allocate(allocate_exprt src)
exprt simplify_is_dynamic_object_expr(state_is_dynamic_object_exprt src)
exprt simplify_object_expression_rec(exprt src)
static bool is_zero_char(const exprt &src, const namespacet &ns)
exprt simplify_live_object_expr(state_live_object_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_is_sentinel_dll_expr(state_is_sentinel_dll_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_evaluate_exit_scope_state(evaluate_exprt evaluate_expr, const namespacet &ns)
exprt simplify_ok_expr(state_ok_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_state_expr_node(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
exprt simplify_is_cstring_expr(state_is_cstring_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_evaluate_update(evaluate_exprt evaluate_expr, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_cstrlen_expr(state_cstrlen_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
std::size_t allocate_counter
exprt simplify_pointer_offset_expr(pointer_offset_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
static bool is_a_char_type(const typet &type)
exprt simplify_evaluate_deallocate_state(evaluate_exprt evaluate_expr, const namespacet &ns)
exprt simplify_object_expression(exprt src)
exprt simplify_object_size_expr(state_object_size_exprt src, const namespacet &ns)
exprt simplify_state_expr(exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_writeable_object_expr(state_writeable_object_exprt src, const namespacet &ns)
exprt simplify_pointer_object_expr(pointer_object_exprt src, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
exprt simplify_evaluate_allocate_state(evaluate_exprt evaluate_expr, const namespacet &ns)
static bool types_are_compatible(const typet &a, const typet &b)
Simplify State Expression.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const state_ok_exprt & to_state_ok_expr(const exprt &expr)
Cast an exprt to a state_ok_exprt.
Definition state.h:882
const state_is_cstring_exprt & to_state_is_cstring_expr(const exprt &expr)
Cast an exprt to a state_is_cstring_exprt.
Definition state.h:615
const state_cstrlen_exprt & to_state_cstrlen_expr(const exprt &expr)
Cast an exprt to a state_cstrlen_exprt.
Definition state.h:677
const exit_scope_state_exprt & to_exit_scope_state_expr(const exprt &expr)
Cast an exprt to a exit_scope_state_exprt.
Definition state.h:1119
const enter_scope_state_exprt & to_enter_scope_state_expr(const exprt &expr)
Cast an exprt to a enter_scope_state_exprt.
Definition state.h:1042
const state_writeable_object_exprt & to_state_writeable_object_expr(const exprt &expr)
Cast an exprt to a state_writeable_object_exprt.
Definition state.h:553
const state_is_dynamic_object_exprt & to_state_is_dynamic_object_expr(const exprt &expr)
Cast an exprt to a state_is_dynamic_object_exprt.
Definition state.h:739
const state_object_size_exprt & to_state_object_size_expr(const exprt &expr)
Cast an exprt to a state_object_size_exprt.
Definition state.h:804
const update_state_exprt & to_update_state_expr(const exprt &expr)
Cast an exprt to a update_state_exprt.
Definition state.h:200
const deallocate_state_exprt & to_deallocate_state_expr(const exprt &expr)
Cast an exprt to a deallocate_state_exprt.
Definition state.h:446
const allocate_exprt & to_allocate_expr(const exprt &expr)
Cast an exprt to a allocate_exprt.
Definition state.h:260
const evaluate_exprt & to_evaluate_expr(const exprt &expr)
Cast an exprt to a evaluate_exprt.
Definition state.h:130
const state_live_object_exprt & to_state_live_object_expr(const exprt &expr)
Cast an exprt to a state_live_object_exprt.
Definition state.h:499
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2024
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1045
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1375
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:887
Symbol table entry.
#define size_type
Definition unistd.c:186

AltStyle によって変換されたページ (->オリジナル) /