cprover
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>
20#include <util/prefix.h>
21#include <util/simplify_expr.h>
22#include <util/std_expr.h>
23#include <util/symbol.h>
24
25#include "may_alias.h"
26#include "may_be_same_object.h"
27#include "sentinel_dll.h"
28#include "state.h"
29
30std::size_t allocate_counter = 0;
31
33 exprt,
34 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
35 const namespacet &);
36
37static bool types_are_compatible(const typet &a, const typet &b)
38{
39 if(a == b)
40 return true;
41 else if(a.id() == ID_pointer && b.id() == ID_pointer)
42 return true;
43 else
44 return false;
45}
46
48 evaluate_exprt evaluate_expr,
49 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
50 const namespacet &ns)
51{
52 PRECONDITION(evaluate_expr.state().id() == ID_update_state);
53
54 const auto &update_state_expr = to_update_state_expr(evaluate_expr.state());
55
56#if 0
57 std::cout << "U: " << format(update_state_expr) << "\n";
58 std::cout << "u: " << format(update_state_expr.address()) << "\n";
59 std::cout << "T: " << format(update_state_expr.address().type()) << "\n";
60 std::cout << "E: " << format(evaluate_expr.address()) << "\n";
61 std::cout << "T: " << format(evaluate_expr.address().type()) << "\n";
62#endif
63
65 evaluate_expr.address(), update_state_expr.address(), address_taken, ns);
66
67#if 0
68 if(may_alias.has_value())
69 std::cout << "M: " << format(*may_alias) << "\n";
70 else
71 std::cout << "M: ?\n";
72#endif
73
74 if(may_alias.has_value())
75 {
76 // 'simple' case
77 if(may_alias->is_true())
78 {
79 // The object is known to be the same.
80 // (ς[A:=V])(A) --> V
83 update_state_expr.new_value(), evaluate_expr.type()),
85 ns);
86 }
87 else if(may_alias->is_false())
88 {
89 // The object is known to be different.
90 // (ς[❝x❞:=V])(❝y❞) --> ς(❝y❞)
91 // It might be possible to further simplify ς(❝y❞).
93 evaluate_expr.with_state(update_state_expr.state()), address_taken, ns);
94 }
95 else
96 {
97 // The object may or may not be the same.
98 // (ς[A:=V])(B) --> if cond then V else ς(B) endif
100 auto new_evaluate_expr =
101 evaluate_expr.with_state(update_state_expr.state());
103 new_evaluate_expr, address_taken, ns); // rec. call
104 auto if_expr = if_exprt(
105 std::move(simplified_cond),
108 update_state_expr.new_value(), evaluate_expr.type()),
110 ns),
112 return simplify_expr(if_expr, ns);
113 }
114 }
115
116 auto new_evaluate_expr = evaluate_expr.with_state(update_state_expr.state());
119
120 // Types are compatible?
122 update_state_expr.new_value().type(), evaluate_expr.type()))
123 {
124 // Disregard case where the two memory regions overlap.
125 //
126 // (ς[w:=v])(r) -->
127 // IF same_object(w, r) ∧ offset(w) = offset(r) THEN
128 // v
129 // ELSE
130 // ς(r)
131 // ENDIF
132 auto same_object =
133 ::same_object(evaluate_expr.address(), update_state_expr.address());
134
137
139 pointer_offset(evaluate_expr.address()), address_taken, ns);
140
143
145
147
148 auto simplified_same =
150
151 auto new_value = typecast_exprt::conditional_cast(
152 update_state_expr.new_value(), evaluate_expr.type());
153
154 auto if_expr =
156
157 return simplify_expr(if_expr, ns);
158 }
159 else
160 {
161 // Complex case. Types don't match.
163
164#if 0
165 auto object = update_state_expr.new_value();
166
167 auto offset = simplify_state_expr_node(
168 pointer_offset(evaluate_expr.address()), address_taken, ns);
169
170 auto byte_extract = make_byte_extract(object, offset, evaluate_expr.type());
171
172 return if_exprt(
173 std::move(simplified_same_object),
174 std::move(byte_extract),
176#endif
177 }
178}
179
181{
182 // A store does not affect the result.
183 // allocate(ς[A:=V]), size) --> allocate(ς, size)
184 if(src.state().id() == ID_update_state)
185 {
186 // rec. call
187 return simplify_allocate(
188 src.with_state(to_update_state_expr(src.state()).state()));
189 }
190 else if(src.state().id() == ID_enter_scope_state)
191 {
192 // rec. call
193 return simplify_allocate(
194 src.with_state(to_enter_scope_state_expr(src.state()).state()));
195 }
196 else if(src.state().id() == ID_exit_scope_state)
197 {
198 // rec. call
199 return simplify_allocate(
200 src.with_state(to_exit_scope_state_expr(src.state()).state()));
201 }
202
203 return std::move(src);
204}
205
207 evaluate_exprt evaluate_expr,
208 const namespacet &ns)
209{
210 PRECONDITION(evaluate_expr.state().id() == ID_allocate_state);
211
212 // const auto &allocate_expr = to_allocate_expr(evaluate_expr.state());
213
214#if 0
215 // Same address?
216 if(evaluate_expr.address() == allocate_expr.address())
217 {
218# if 0
219 irep_idt identifier = "allocate-" + std::to_string(++allocate_counter);
220 auto object_size = allocate_expr.size();
221 auto object_type = array_typet(char_type(), object_size);
222 auto symbol_expr = symbol_exprt(identifier, object_type);
223 return object_address_exprt(symbol_expr);
224# endif
225 return std::move(evaluate_expr);
226 }
227 else // different
228 {
229 auto new_evaluate_expr = evaluate_expr;
230 new_evaluate_expr.state() = allocate_expr.state();
231 return std::move(new_evaluate_expr);
232 }
233#endif
234 return std::move(evaluate_expr);
235}
236
238 evaluate_exprt evaluate_expr,
239 const namespacet &ns)
240{
241 PRECONDITION(evaluate_expr.state().id() == ID_deallocate_state);
242
243 // deallocate isn't visible to 'evaluate'
244 const auto &deallocate_state_expr =
245 to_deallocate_state_expr(evaluate_expr.state());
246 auto new_evaluate_expr =
247 evaluate_expr.with_state(deallocate_state_expr.state());
248 return std::move(new_evaluate_expr);
249}
250
252 evaluate_exprt evaluate_expr,
253 const namespacet &ns)
254{
255 PRECONDITION(evaluate_expr.state().id() == ID_enter_scope_state);
256
257 const auto &enter_scope_state_expr =
258 to_enter_scope_state_expr(evaluate_expr.state());
259 auto new_evaluate_expr =
260 evaluate_expr.with_state(enter_scope_state_expr.state());
261 return std::move(new_evaluate_expr);
262}
263
265 evaluate_exprt evaluate_expr,
266 const namespacet &ns)
267{
268 PRECONDITION(evaluate_expr.state().id() == ID_exit_scope_state);
269
270 const auto &exit_scope_state_expr =
271 to_exit_scope_state_expr(evaluate_expr.state());
272 auto new_evaluate_expr =
273 evaluate_expr.with_state(exit_scope_state_expr.state());
274 return std::move(new_evaluate_expr);
275}
276
278{
279 if(src.id() == ID_object_address)
280 return src;
281 else if(src.id() == ID_element_address)
283 else if(src.id() == ID_field_address)
285 else if(src.id() == ID_plus)
286 {
287 const auto &plus_expr = to_plus_expr(src);
288 for(auto &op : plus_expr.operands())
289 if(op.type().id() == ID_pointer)
291 return src; // no change
292 }
293 else if(src.id() == ID_typecast)
294 {
295 const auto &op = to_typecast_expr(src).op();
296 if(op.type().id() == ID_pointer)
298 else
299 return src; // no change
300 }
301 else
302 return src;
303}
304
309
312 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
313 const namespacet &ns)
314{
315 const auto &pointer = src.address();
316
317 auto object = simplify_object_expression(pointer);
318
319 if(object.id() == ID_object_address)
320 {
321 auto identifier = to_object_address_expr(object).object_identifier();
322
323 if(has_prefix(id2string(identifier), "allocate-"))
324 {
325 }
326 else if(identifier == "return_value")
327 {
328 return true_exprt(); // never dies
329 }
330 else if(has_prefix(id2string(identifier), "va_args::"))
331 {
332 return true_exprt(); // might be 'dead'
333 }
334 else
335 {
336 const auto &symbol = ns.lookup(identifier);
337 if(symbol.is_static_lifetime)
338 {
339 return true_exprt(); // always live
340 }
341 }
342 }
343
344 // A store does not affect the result.
345 // live_object(ς[A:=V]), p) --> live_object(ς, p)
346 if(src.state().id() == ID_update_state)
347 {
348 src.state() = to_update_state_expr(src.state()).state();
349
350 // rec. call
351 return simplify_live_object_expr(std::move(src), address_taken, ns);
352 }
353 else if(src.state().id() == ID_deallocate_state)
354 {
356 // live_object(deallocate_state(ς, p), q) -->
357 // IF same_object(p, q) THEN false ELSE live_object(ς, q) ENDIF
358 auto same_object = ::same_object(object, deallocate_state_expr.address());
363 return if_exprt(
365 }
366 else if(src.state().id() == ID_enter_scope_state)
367 {
368 // This begins the life of a local-scoped variable.
370 if(
371 address_taken.find(enter_scope_state_expr.symbol()) !=
372 address_taken.end())
373 {
374 // live_object(enter_scope_state(ς, p), q) -->
375 // IF same_object(p, q) THEN true ELSE live_object(ς, q) ENDIF
376 auto same_object =
377 ::same_object(object, enter_scope_state_expr.address());
383 ns);
384 return if_exprt(
386 }
387 else
388 {
389 return simplify_live_object_expr( // rec. call
392 ns);
393 }
394 }
395 else if(src.state().id() == ID_exit_scope_state)
396 {
397 // This ends the life of a local-scoped variable.
399 if(
400 address_taken.find(exit_scope_state_expr.symbol()) != address_taken.end())
401 {
402 // live_object(exit_scope_state(ς, p), q) -->
403 // IF same_object(p, q) THEN false ELSE live_object(ς, q) ENDIF
404 auto same_object = ::same_object(object, exit_scope_state_expr.address());
410 ns);
411 return if_exprt(
413 }
414 else
415 {
416 return simplify_live_object_expr( // rec. call
419 ns);
420 }
421 }
422
423 return std::move(src);
424}
425
428 const namespacet &ns)
429{
430 const auto &pointer = src.address();
431
432 auto object = simplify_object_expression(pointer);
433
434 if(object.id() == ID_object_address)
435 {
436 auto identifier = to_object_address_expr(object).object_identifier();
437
438 if(has_prefix(id2string(identifier), "allocate-"))
439 {
440 }
441 else if(has_prefix(id2string(identifier), "va_args::"))
442 {
443 return true_exprt(); // always writeable
444 }
445 else
446 {
447 const auto &symbol = ns.lookup(identifier);
448 return make_boolean_expr(!symbol.type.get_bool(ID_C_constant));
449 }
450 }
451
452 // A store does not affect the result.
453 // writeable_object(ς[A:=V]), p) --> writeable_object(ς, p)
454 if(src.state().id() == ID_update_state)
455 {
456 src.state() = to_update_state_expr(src.state()).state();
457 return std::move(src);
458 }
459
460 return std::move(src);
461}
462
464{
465 const auto &pointer = src.address();
466
467 auto object = simplify_object_expression(pointer);
468
469 if(object.id() == ID_object_address)
470 {
471 // these are not dynamic
472 return false_exprt();
473 }
474
475 // A store does not affect the result.
476 // is_dynamic_object(ς[A:=V]), p) --> is_dynamic_object(ς, p)
477 if(src.state().id() == ID_update_state)
478 {
479 src.state() = to_update_state_expr(src.state()).state();
480 // rec. call
481 return simplify_is_dynamic_object_expr(std::move(src));
482 }
483 else if(src.state().id() == ID_enter_scope_state)
484 {
486 src.with_state(to_enter_scope_state_expr(src.state()).state()));
487 }
488 else if(src.state().id() == ID_exit_scope_state)
489 {
491 src.with_state(to_exit_scope_state_expr(src.state()).state()));
492 }
493
494 return std::move(src);
495}
496
499 const namespacet &ns)
500{
501 const auto &pointer = src.address();
502
503 auto object = simplify_object_expression(pointer);
504
505 if(object.id() == ID_object_address)
506 {
507 const auto &object_address_expr = to_object_address_expr(object);
508 auto size_opt = size_of_expr(object_address_expr.object_type(), ns);
509 if(size_opt.has_value())
511 else
512 return std::move(src); // no change
513 }
514
515 // A store does not affect the result.
516 // object_size(ς[A:=V]), p) --> object_size(ς, p)
517 if(src.state().id() == ID_update_state)
518 {
519 return src.with_state(to_update_state_expr(src.state()).state());
520 }
521
522 return std::move(src);
523}
524
526 state_ok_exprt src,
527 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
528 const namespacet &ns)
529{
530 auto &state = src.state();
531 auto &pointer = src.address();
532 auto &size = src.size();
533
534 if(state.id() == ID_update_state)
535 {
536 // A store does not affect the result.
537 // X_ok(ς[A:=V]), A, S) --> X_ok(ς, A, S)
538 state = to_update_state_expr(state).state();
539
540 // rec. call
541 return simplify_state_expr_node(std::move(src), address_taken, ns);
542 }
543 else if(state.id() == ID_enter_scope_state)
544 {
546
547 // rec. call
550
551#if 0
552 // replace array by array[0]
554 enter_scope_state_expr.object_type().id() == ID_array ?
556 enter_scope_state_expr.address();
557
558 auto may_alias =
560
561 if(may_alias.has_value() && *may_alias == false_exprt())
562 return rec_result;
563
564 auto same_object = ::same_object(pointer, enter_scope_state_expr.address());
565#else
567 pointer, enter_scope_state_expr.address(), address_taken, ns);
568#endif
569
572
573 // Known to be live, only need to check upper bound.
574 // Extend one bit, to cover overflow case.
575 auto size_type = ::size_type();
577 auto offset = pointer_offset_exprt(pointer, size_type_ext);
579 auto object_size_opt =
580 size_of_expr(enter_scope_state_expr.object_type(), ns);
581 if(!object_size_opt.has_value())
582 return std::move(src);
583
584 auto upper = binary_relation_exprt(
585 plus_exprt(offset, size_casted),
586 ID_le,
588
590
591 auto implication =
593
594 return std::move(implication);
595 }
596 else if(state.id() == ID_exit_scope_state)
597 {
598#if 0
600
601 // rec. call
604
605 auto same_object = ::same_object(pointer, exit_scope_state_expr.address());
606
609
610 // Known to be dead if it's the same object.
611 auto implication =
613
614 return implication;
615#else
617 src.with_state(to_exit_scope_state_expr(state).state()),
619 ns);
620#endif
621 }
622
623 return std::move(src);
624}
625
626#if 0
627static bool is_one(const exprt &src)
628{
629 if(src.id() == ID_typecast)
630 return is_one(to_typecast_expr(src).op());
631 else if(src.is_constant())
632 {
634 return value_opt.has_value() && *value_opt == 1;
635 }
636 else
637 return false;
638}
639#endif
640
641static bool is_a_char_type(const typet &type)
642{
643 return (type.id() == ID_signedbv || type.id() == ID_unsignedbv) &&
644 to_bitvector_type(type).get_width() == char_type().get_width();
645}
646
647static bool is_zero_char(const exprt &src, const namespacet &ns)
648{
649 if(!is_a_char_type(src.type()))
650 return false;
651
652 auto src_simplified = simplify_expr(src, ns);
653
655
656 return integer_opt.has_value() && *integer_opt == 0;
657}
658
661 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
662 const namespacet &ns)
663{
664 PRECONDITION(src.type().id() == ID_bool);
665 const auto &state = src.state();
666 const auto &pointer = src.address();
667
668 if(state.id() == ID_update_state)
669 {
670 const auto &update_state_expr = to_update_state_expr(state);
671
672 auto cstring_in_old_state = src;
676
677 auto may_alias =
678 ::may_alias(pointer, update_state_expr.address(), address_taken, ns);
679
680 if(may_alias.has_value() && may_alias->is_false())
681 {
682 // different objects
683 // cstring(s[x:=v], p) --> cstring(s, p)
685 }
686
687 // maybe the same
688
689 // Are we writing zero?
690 if(update_state_expr.new_value().is_zero())
691 {
692 // cstring(s[p:=0], q) --> if p alias q then true else cstring(s, q)
693 auto same_object = ::same_object(pointer, update_state_expr.address());
694
697
698 return if_exprt(
700 }
701 }
702 else if(state.id() == ID_enter_scope_state)
703 {
704 // rec. call
706 src.with_state(to_enter_scope_state_expr(state).state()),
708 ns);
709 }
710 else if(state.id() == ID_exit_scope_state)
711 {
712 // rec. call
714 src.with_state(to_exit_scope_state_expr(state).state()),
716 ns);
717 }
718
719 if(pointer.id() == ID_plus)
720 {
721#if 0
722 auto &plus_expr = to_plus_expr(pointer);
723 if(plus_expr.operands().size() == 2 && is_one(plus_expr.op1()))
724 {
725 // is_cstring(ς, p + 1)) --> is_cstring(ς, p) ∨ ς(p)=0
726 auto new_is_cstring = src;
727 new_is_cstring.op1() = plus_expr.op0();
728 auto type = to_pointer_type(pointer.type()).base_type();
729 auto zero = from_integer(0, type);
730 auto is_zero =
731 equal_exprt(evaluate_exprt(state, plus_expr.op0(), type), zero);
732 return or_exprt(new_is_cstring, is_zero);
733 }
734#endif
735 }
736 else if(
737 pointer.id() == ID_address_of &&
738 to_address_of_expr(pointer).object().id() == ID_string_constant)
739 {
740 // is_cstring(ς, &"...")) --> true
741 return true_exprt();
742 }
743 else if(
744 pointer.id() == ID_element_address &&
745 to_element_address_expr(pointer).base().id() == ID_address_of &&
746 to_address_of_expr(to_element_address_expr(pointer).base()).object().id() ==
748 {
749 // TODO: compare offset to length
750 // is_cstring(ς, element_address(&"...", 0))) --> true
751 return true_exprt();
752 }
753
754 return std::move(src);
755}
756
759 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
760 const namespacet &ns)
761{
762 const auto &state = src.state();
763 const auto &pointer = src.address();
764
765 if(state.id() == ID_update_state)
766 {
767 const auto &update_state_expr = to_update_state_expr(state);
768
772
774 pointer, update_state_expr.address(), address_taken, ns);
775
777 {
778 // different objects
779 // cstrlen(s[x:=v], p) --> cstrlen(s, p)
781 }
782
783 // maybe the same
784
785 // Are we writing zero?
786 if(is_zero_char(update_state_expr.new_value(), ns))
787 {
788 // cstrlen(s[p:=0], p) --> 0
789 if(pointer == update_state_expr.address())
790 return from_integer(0, src.type());
791 }
792 }
793
794 if(pointer.id() == ID_plus)
795 {
796#if 0
797 auto &plus_expr = to_plus_expr(pointer);
798 if(plus_expr.operands().size() == 2 && is_one(plus_expr.op1()))
799 {
800 // is_cstring(ς, p + 1)) --> is_cstring(ς, p) ∨ ς(p)=0
801 auto new_is_cstring = src;
802 new_is_cstring.op1() = plus_expr.op0();
803 auto type = to_pointer_type(pointer.type()).base_type();
804 auto zero = from_integer(0, type);
805 auto is_zero =
806 equal_exprt(evaluate_exprt(state, plus_expr.op0(), type), zero);
807 return or_exprt(new_is_cstring, is_zero);
808 }
809#endif
810 }
811 else if(
812 pointer.id() == ID_address_of &&
813 to_address_of_expr(pointer).object().id() == ID_string_constant)
814 {
815#if 0
816 // is_cstring(ς, &"...")) --> true
817 return true_exprt();
818#endif
819 }
820 else if(
821 pointer.id() == ID_element_address &&
822 to_element_address_expr(pointer).base().id() == ID_address_of &&
823 to_address_of_expr(to_element_address_expr(pointer).base()).object().id() ==
825 {
826#if 0
827 // TODO: compare offset to length
828 // is_cstring(ς, element_address(&"...", 0))) --> true
829 return true_exprt();
830#endif
831 }
832
833 return std::move(src);
834}
835
838 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
839 const namespacet &ns)
840{
841 PRECONDITION(src.type().id() == ID_bool);
842 const auto &state = src.state();
843 const auto &head = src.head();
844 const auto &tail = src.tail();
845
846 {
847 // ς(h.❝n❞) = t ∧ ς(t.❝p❞) = h --> is_sentinel_dll(ς, h, t)
848 auto head_next = sentinel_dll_next(state, head, ns);
849 auto tail_prev = sentinel_dll_prev(state, tail, ns);
850
851 if(head_next.has_value() && tail_prev.has_value())
852 {
853 // rec. calls
858 if(head_next_simplified == tail && tail_prev_simplified == head)
859 return true_exprt();
860 }
861 }
862
863 if(state.id() == ID_update_state)
864 {
865 const auto &update_state_expr = to_update_state_expr(state);
866
867 // are we writing to something that might be a node pointer?
868 const auto &update_type = update_state_expr.new_value().type();
869 if(update_type != src.head().type())
870 {
871 // update is irrelevant, drop update
872 auto without_update = src.with_state(update_state_expr.state());
874 }
875 }
876 else if(state.id() == ID_enter_scope_state)
877 {
879 src.with_state(to_enter_scope_state_expr(state).state()),
881 ns);
882 }
883 else if(state.id() == ID_exit_scope_state)
884 {
886 src.with_state(to_exit_scope_state_expr(state).state()),
888 ns);
889 }
890
891 return std::move(src);
892}
893
896 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
897 const namespacet &ns)
898{
899 if(src.pointer().id() == ID_object_address)
900 {
901 // pointer_offset(❝x❞) -> 0
902 return from_integer(0, src.type());
903 }
904 else if(src.pointer().id() == ID_element_address)
905 {
907 // pointer_offset(element_address(Z, y)) -->
908 // pointer_offset(Z) + y*sizeof(x)
909 auto size_opt = size_of_expr(element_address_expr.element_type(), ns);
910 if(size_opt.has_value())
911 {
912 auto product = mult_exprt(
914 element_address_expr.index(), src.type()),
919 ns);
920 auto sum = plus_exprt(pointer_offset, std::move(product));
921 return std::move(sum);
922 }
923 }
924 else if(src.pointer().id() == ID_address_of)
925 {
926 const auto &address_of_expr = to_address_of_expr(src.pointer());
927 if(address_of_expr.object().id() == ID_string_constant)
928 return from_integer(0, src.type());
929 }
930 else if(src.pointer().id() == ID_typecast)
931 {
932 if(to_typecast_expr(src.pointer()).op().type().id() == ID_pointer)
933 {
934 // remove the typecast
938 ns);
939 }
940 }
941
942 return std::move(src);
943}
944
947 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
948 const namespacet &ns)
949{
951
952 if(src.pointer() != simplified_pointer)
954
955 return std::move(src);
956}
957
959 exprt src,
960 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
961 const namespacet &ns)
962{
963 if(src.id() == ID_allocate)
964 {
966 }
967 else if(src.id() == ID_evaluate)
968 {
969 auto &evaluate_expr = to_evaluate_expr(src);
970
971 if(evaluate_expr.state().id() == ID_update_state)
972 {
973 return simplify_evaluate_update(evaluate_expr, address_taken, ns);
974 }
975 else if(evaluate_expr.state().id() == ID_allocate_state)
976 {
977 return simplify_evaluate_allocate_state(evaluate_expr, ns);
978 }
979 else if(evaluate_expr.state().id() == ID_deallocate_state)
980 {
981 return simplify_evaluate_deallocate_state(evaluate_expr, ns);
982 }
983 else if(evaluate_expr.state().id() == ID_enter_scope_state)
984 {
985 return simplify_evaluate_enter_scope_state(evaluate_expr, ns);
986 }
987 else if(evaluate_expr.state().id() == ID_exit_scope_state)
988 {
989 return simplify_evaluate_exit_scope_state(evaluate_expr, ns);
990 }
991 }
992 else if(
993 src.id() == ID_state_r_ok || src.id() == ID_state_w_ok ||
994 src.id() == ID_state_rw_ok)
995 {
997 }
998 else if(src.id() == ID_state_live_object)
999 {
1002 }
1003 else if(src.id() == ID_state_writeable_object)
1004 {
1007 }
1008 else if(src.id() == ID_state_is_cstring)
1009 {
1012 }
1013 else if(src.id() == ID_state_cstrlen)
1014 {
1016 }
1017 else if(src.id() == ID_state_is_sentinel_dll)
1018 {
1021 }
1022 else if(src.id() == ID_state_is_dynamic_object)
1023 {
1026 }
1027 else if(src.id() == ID_plus)
1028 {
1029 auto &plus_expr = to_plus_expr(src);
1030 if(
1031 src.type().id() == ID_pointer &&
1032 plus_expr.op0().id() == ID_element_address)
1033 {
1034 // element_address(X, Y) + Z --> element_address(X, Y + Z)
1039 plus_expr.op1(), new_element_address_expr.index().type()));
1040 new_element_address_expr.index() =
1044 }
1045 }
1046 else if(src.id() == ID_pointer_offset)
1047 {
1050 }
1051 else if(src.id() == ID_pointer_object)
1052 {
1055 }
1056 else if(src.id() == ID_state_object_size)
1057 {
1059 }
1060 else if(src.id() == ID_equal)
1061 {
1062 const auto &equal_expr = to_equal_expr(src);
1063 if(
1064 equal_expr.lhs().id() == ID_pointer_object &&
1065 equal_expr.rhs().id() == ID_pointer_object)
1066 {
1067 const auto &lhs_p = to_pointer_object_expr(equal_expr.lhs()).pointer();
1068 const auto &rhs_p = to_pointer_object_expr(equal_expr.rhs()).pointer();
1069 if(lhs_p.id() == ID_object_address && rhs_p.id() == ID_object_address)
1070 {
1071 if(
1072 to_object_address_expr(lhs_p).object_identifier() ==
1073 to_object_address_expr(rhs_p).object_identifier())
1074 return true_exprt();
1075 else
1076 return false_exprt();
1077 }
1078 }
1079 }
1080
1081 return src;
1082}
1083
1085 exprt src,
1086 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
1087 const namespacet &ns)
1088{
1089 // operands first, recursively
1090 for(auto &op : src.operands())
1091 op = simplify_state_expr(op, address_taken, ns);
1092
1093 // now the node itself
1095
1096 return src;
1097}
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.
unsignedbv_typet size_type()
Definition c_types.cpp:55
bitvector_typet char_type()
Definition c_types.cpp:111
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
allocate_exprt with_state(exprt state) const
Definition state.h:246
const exprt & state() const
Definition state.h:230
Boolean AND.
Definition std_expr.h:2071
Arrays with given size.
Definition std_types.h:763
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Operator to return the address of an array element relative to a base address.
Equality.
Definition std_expr.h:1306
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:56
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
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
The Boolean constant false.
Definition std_expr.h:3017
The trinary if-then-else operator.
Definition std_expr.h:2323
const irep_idt & id() const
Definition irep.h:396
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
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().
Operator to return the address of an object.
Boolean OR.
Definition std_expr.h:2179
The plus expression Associativity is not specified.
Definition std_expr.h:947
A numerical identifier for the object a pointer points to.
The offset (in bytes) of a pointer relative to the object.
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
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
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
const exprt & head() const
const exprt & state() const
state_is_sentinel_dll_exprt with_state(exprt state) const
const exprt & tail() const
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
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
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
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:113
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
Fixed-width bit-vector with unsigned binary interpretation.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition format.h:37
static exprt implication(exprt lhs, exprt rhs)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
optionalt< exprt > may_alias(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
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.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
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 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.
optionalt< 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.
optionalt< exprt > sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &ns)
optionalt< 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.
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:2051
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:986
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1347
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
Symbol table entry.