CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symex_goto.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13#include <util/expr_util.h>
14#include <util/invariant.h>
15#include <util/pointer_expr.h>
17#include <util/simplify_expr.h>
18#include <util/std_expr.h>
19
23
24#include "goto_symex.h"
26#include "path_storage.h"
27
28#include <algorithm>
29
34 const exprt &original_guard,
35 const exprt &new_guard,
36 const namespacet &ns)
37{
38 // It would be better to call try_filter_value_sets after apply_condition,
39 // and pass nullptr for value sets which apply_condition successfully updated
40 // already. However, try_filter_value_sets calls rename to do constant
41 // propagation, and apply_condition can update the constant propagator. Since
42 // apply condition will never succeed on both jump_taken_state and
43 // jump_not_taken_state, it should be possible to pass a reference to an
44 // unmodified goto_statet to use for renaming. But renaming needs a
45 // goto_symex_statet, not just a goto_statet, and we only have access to one
46 // of those. A future improvement would be to split rename into two parts:
47 // one part on goto_symex_statet which is non-const and deals with
48 // l2 thread reads, and one part on goto_statet which is const and could be
49 // used in try_filter_value_sets.
50
54 jump_taken_state.value_set,
55 &jump_taken_state.value_set,
56 &jump_not_taken_state.value_set,
57 ns);
58
59 if(!symex_config.constant_propagation)
60 return;
61
62 jump_taken_state.apply_condition(new_guard, current_state, ns);
63
64 // Could use not_exprt + simplify, but let's avoid paying that cost on quite
65 // a hot path:
68}
69
81static std::optional<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
82 const irep_idt &operation,
83 const symbol_exprt &symbol_expr,
84 const exprt &other_operand,
85 const value_sett &value_set,
86 const irep_idt language_mode,
87 const namespacet &ns)
88{
91
92 if(
94 (!constant_expr || !constant_expr->is_null_pointer()))
95 {
96 return {};
97 }
98
101
103 l1_expr.remove_level_2();
104 const std::vector<exprt> value_set_elements =
105 value_set.get_value_set(l1_expr, ns);
106
107 bool constant_found = false;
108
109 for(const auto &value_set_element : value_set_elements)
110 {
111 if(
117 {
118 // We can't conclude anything about the value-set
119 return {};
120 }
121
122 if(!constant_found)
123 {
125 value_set_element, false, language_mode))
126 {
127 continue;
128 }
129
132 value_set_element, symbol_expr, ns);
133
134 // use the simplifier to test equality as we need to skip over typecasts
135 // and cannot rely on canonical representations, which would permit a
136 // simple syntactic equality test
141 ns);
142 if(test_equal.is_true())
143 {
144 constant_found = true;
145 // We can't break because we have to make sure we find any instances of
146 // ID_unknown or ID_invalid
147 }
148 else if(!test_equal.is_false())
149 {
150 // We can't conclude anything about the value-set
151 return {};
152 }
153 }
154 }
155
156 if(!constant_found)
157 {
158 // The symbol cannot possibly have the value \p other_operand because it
159 // isn't in the symbol's value-set
160 return operation == ID_equal ? make_renamed<L2>(false_exprt{})
162 }
163 else if(value_set_elements.size() == 1)
164 {
165 // The symbol must have the value \p other_operand because it is the only
166 // thing in the symbol's value-set
167 return operation == ID_equal ? make_renamed<L2>(true_exprt{})
169 }
170 else
171 {
172 return {};
173 }
174}
175
183static std::optional<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
185 const value_sett &value_set,
186 const irep_idt &language_mode,
187 const namespacet &ns)
188{
189 const exprt &expr = renamed_expr.get();
190
191 if(expr.id() != ID_equal && expr.id() != ID_notequal)
192 return {};
193
194 if(!can_cast_type<pointer_typet>(to_binary_expr(expr).op0().type()))
195 return {};
196
197 exprt lhs = to_binary_expr(expr).op0(), rhs = to_binary_expr(expr).op1();
199 std::swap(lhs, rhs);
200
203
204 if(!symbol_expr_lhs)
205 return {};
206
208 return {};
209
211 expr.id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
212}
213
215 renamedt<exprt, L2> condition,
216 const value_sett &value_set,
217 const irep_idt &language_mode,
218 const namespacet &ns)
219{
221 condition,
222 [&value_set, &language_mode, &ns](const renamedt<exprt, L2> &expr) {
224 expr, value_set, language_mode, ns);
225 });
226
227 return condition;
228}
229
231{
232 PRECONDITION(state.reachable);
233
234 const goto_programt::instructiont &instruction=*state.source.pc;
235
236 exprt new_guard = clean_expr(instruction.condition(), state, false);
237
240 std::move(renamed_guard), state.value_set, language_mode, ns);
241 if(symex_config.simplify_opt)
242 renamed_guard.simplify(ns);
243 new_guard = renamed_guard.get();
244
245 if(new_guard.is_false())
246 {
247 target.location(state.guard.as_expr(), state.source);
248
249 // next instruction
250 symex_transition(state);
251 return; // nothing to do
252 }
253
255
257 !instruction.targets.empty(), "goto should have at least one target");
258
259 // we only do deterministic gotos for now
261 instruction.targets.size() == 1, "no support for non-deterministic gotos");
262
264 instruction.get_target();
265
266 const bool backward = instruction.is_backwards_goto();
267
268 if(backward)
269 {
270 // is it label: goto label; or while(cond); - popular in SV-COMP
271 if(
272 symex_config.self_loops_to_assumptions &&
273 // label: goto label; or do {} while(cond);
274 (goto_target == state.source.pc ||
275 // while(cond);
276 (instruction.incoming_edges.size() == 1 &&
277 *instruction.incoming_edges.begin() == goto_target &&
278 goto_target->is_goto() && new_guard.is_true())))
279 {
280 // generate assume(false) or a suitable negation if this
281 // instruction is a conditional goto
284 log.statistics() << "replacing self-loop at "
285 << state.source.pc->source_location() << " by assume("
287 << ")" << messaget::eom;
288 if(symex_config.unwinding_assertions)
289 {
290 log.warning()
291 << "no unwinding assertion will be generated for self-loop at "
292 << state.source.pc->source_location() << messaget::eom;
293 }
295
296 // next instruction
297 symex_transition(state);
298 return;
299 }
300
301 const auto loop_id =
303
304 unsigned &unwind = state.call_stack().top().loop_iterations[loop_id].count;
305 unwind++;
306
307 if(should_stop_unwind(state.source, state.call_stack(), unwind))
308 {
309 // we break the loop
311
312 // next instruction
313 symex_transition(state);
314 return;
315 }
316
317 if(new_guard.is_true())
318 {
319 // we continue executing the loop
320 if(check_break(loop_id, unwind))
321 {
322 should_pause_symex = true;
323 }
324 symex_transition(state, goto_target, true);
325 return; // nothing else to do
326 }
327 }
328
329 // No point executing both branches of an unconditional goto.
330 if(
331 new_guard.is_true() && // We have an unconditional goto, AND
332 // either there are no reachable blocks between us and the target in the
333 // surrounding scope (because state.guard == true implies there is no path
334 // around this GOTO instruction)
335 (state.guard.is_true() ||
336 // or there is another block, but we're doing path exploration so
337 // we're going to skip over it for now and return to it later.
338 symex_config.doing_path_exploration))
339 {
341 instruction.targets.size() > 0,
342 "Instruction is an unconditional goto with no target: " +
343 instruction.code().pretty());
344 symex_transition(state, instruction.get_target(), true);
345 return;
346 }
347
350
351 if(!backward)
352 {
354 state_pc=state.source.pc;
355 state_pc++;
356
357 // skip dead instructions
358 if(new_guard.is_true())
359 while(state_pc!=goto_target && !state_pc->is_target())
360 ++state_pc;
361
363 {
364 symex_transition(state, goto_target, false);
365 return; // nothing else to do
366 }
367 }
368 else
369 {
370 new_state_pc=state.source.pc;
371 new_state_pc++;
373 }
374
375 // Normally the next instruction to execute would be state_pc and we save
376 // new_state_pc for later. But if we're executing from a saved state, then
377 // new_state_pc should be the state that we saved from earlier, so let's
378 // execute that instead.
379 if(state.has_saved_jump_target)
380 {
381 INVARIANT(
382 new_state_pc == state.saved_target,
383 "Tried to explore the other path of a branch, but the next "
384 "instruction along that path is not the same as the instruction "
385 "that we saved at the branch point. Saved instruction is " +
386 state.saved_target->code().pretty() +
387 "\nwe were intending "
388 "to explore " +
389 new_state_pc->code().pretty() +
390 "\nthe "
391 "instruction we think we saw on a previous path exploration is " +
392 state_pc->code().pretty());
395 state_pc = tmp;
396
397 log.debug() << "Resuming from jump target '" << state_pc->source_location()
398 << "'" << log.eom;
399 }
400 else if(state.has_saved_next_instruction)
401 {
402 log.debug() << "Resuming from next instruction '"
403 << state_pc->source_location() << "'" << log.eom;
404 }
405 else if(symex_config.doing_path_exploration)
406 {
407 // We should save both the instruction after this goto, and the target of
408 // the goto.
409
411 next_instruction.state.saved_target = state_pc;
412 next_instruction.state.has_saved_next_instruction = true;
413
415 jump_target.state.saved_target = new_state_pc;
416 jump_target.state.has_saved_jump_target = true;
417 // `forward` tells us where the branch we're _currently_ executing is
418 // pointing to; this needs to be inverted for the branch that we're saving,
419 // so let its truth value for `backwards` be the same as ours for `forward`.
420
421 log.debug() << "Saving next instruction '"
422 << next_instruction.state.saved_target->source_location() << "'"
423 << log.eom;
424 log.debug() << "Saving jump target '"
425 << jump_target.state.saved_target->source_location() << "'"
426 << log.eom;
429
430 // It is now up to the caller of symex to decide which path to continue
431 // executing. Signal to the caller that states have been pushed (therefore
432 // symex has not yet completed and must be resumed), and bail out.
433 should_pause_symex = true;
434 return;
435 }
436
437 // put a copy of the current state into the state-queue, to be used by
438 // merge_gotos when we visit new_state_pc
441
442 // On an unconditional GOTO we don't need our state, as it will be overwritten
443 // by merge_goto. Therefore we move it onto goto_state_list instead of copying
444 // as usual.
445 if(new_guard.is_true())
446 {
447 // The move here only moves goto_statet, the base class of goto_symex_statet
448 // and not the entire thing.
449 goto_state_list.emplace_back(state.source, std::move(state));
450
452
454 state.reachable = false;
455 }
456 else
457 {
458 goto_state_list.emplace_back(state.source, state);
459
461
462 if(!symex_config.doing_path_exploration)
463 {
464 // This doesn't work for --paths (single-path mode) yet, as in multi-path
465 // mode we remove the implied constants at a control-flow merge, but in
466 // single-path mode we don't run merge_gotos.
467 auto &taken_state = backward ? state : goto_state_list.back().second;
468 auto &not_taken_state = backward ? goto_state_list.back().second : state;
469
471 state,
474 instruction.condition(),
475 new_guard,
476 ns);
477 }
478
479 // produce new guard symbol
480 exprt guard_expr;
481
482 if(
483 new_guard.id() == ID_symbol ||
484 (new_guard.id() == ID_not &&
485 to_not_expr(new_guard).op().id() == ID_symbol))
486 {
487 guard_expr=new_guard;
488 }
489 else
490 {
494
497 new_lhs =
498 state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get();
499
501
503 log.debug(),
504 [this, &new_lhs](messaget::mstreamt &mstream) {
505 mstream << "Assignment to " << new_lhs.get_identifier()
506 << " [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
507 << messaget::eom;
508 });
509
511 guard.as_expr(),
513 new_rhs,
516
517 guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns).get();
518 }
519
520 if(state.has_saved_jump_target)
521 {
522 if(!backward)
523 state.guard.add(guard_expr);
524 else
525 state.guard.add(boolean_negate(guard_expr));
526 }
527 else
528 {
529 goto_statet &new_state = goto_state_list.back().second;
530 if(!backward)
531 {
532 new_state.guard.add(guard_expr);
533 state.guard.add(boolean_negate(guard_expr));
534 }
535 else
536 {
537 state.guard.add(guard_expr);
538 new_state.guard.add(boolean_negate(guard_expr));
539 }
540 }
541 }
542}
543
545{
546 PRECONDITION(!state.reachable);
547 // This is like symex_goto, except the state is unreachable. We try to take
548 // some arbitrary choice that maintains the state guard in a reasonable state
549 // in order that it simplifies properly when states are merged (in
550 // merge_gotos). Note we can't try to evaluate the actual GOTO guard because
551 // our constant propagator might be out of date, since we haven't been
552 // executing assign instructions.
553
554 // If the guard is already false then there's no value in this state; just
555 // carry on and check the next instruction.
556 if(state.guard.is_false())
557 {
558 symex_transition(state);
559 return;
560 }
561
562 const goto_programt::instructiont &instruction = *state.source.pc;
563 PRECONDITION(instruction.is_goto());
565
570 new_state.guard = state.guard;
571 new_state.reachable = false;
572 goto_state_list.emplace_back(state.source, std::move(new_state));
573 };
574
575 if(instruction.condition().is_true())
576 {
577 if(instruction.is_backwards_goto())
578 {
579 // Give up trying to salvage the guard
580 // (this state's guard is squashed, without queueing it at the target)
581 }
582 else
583 {
584 // Take the branch:
586 }
587
588 state.guard.add(false_exprt());
589 }
590 else
591 {
592 // Arbitrarily assume a conditional branch is not-taken, except for when
593 // there's an incoming backedge, when we guess that the taken case is less
594 // likely to lead to that backedge than the not-taken case.
595 bool maybe_loop_head = std::any_of(
596 instruction.incoming_edges.begin(),
597 instruction.incoming_edges.end(),
598 [&instruction](const goto_programt::const_targett predecessor) {
599 return predecessor->location_number > instruction.location_number;
600 });
601
602 if(instruction.is_backwards_goto() || !maybe_loop_head)
603 {
604 // Assume branch not taken (fall through)
605 }
606 else
607 {
608 // Assume branch taken:
610 state.guard.add(false_exprt());
611 }
612 }
613
614 symex_transition(state);
615}
616
617bool goto_symext::check_break(const irep_idt &loop_id, unsigned unwind)
618{
619 // dummy implementation
620 return false;
621}
622
624{
625 framet &frame = state.call_stack().top();
626
627 // first, see if this is a target at all
628 auto state_map_it = frame.goto_state_map.find(state.source.pc);
629
630 if(state_map_it==frame.goto_state_map.end())
631 return; // nothing to do
632
633 // we need to merge
635
636 for(auto list_it = state_list.rbegin(); list_it != state_list.rend();
637 ++list_it)
638 {
639 merge_goto(list_it->first, std::move(list_it->second), state);
640 }
641
642 // clean up to save some memory
643 frame.goto_state_map.erase(state_map_it);
644}
645
646static guardt
648{
649 // adjust guard, even using guards from unreachable states. This helps to
650 // shrink the state guard if the incoming edge is from a path that was
651 // truncated by config.unwind, config.depth or an assume-false instruction.
652
653 // Note when an unreachable state contributes its guard, merging it in is
654 // optional, since the formula already implies the unreachable guard is
655 // impossible. Therefore we only integrate it when to do so simplifies the
656 // state guard.
657
658 // This function can trash either state's guards, since goto_state is dying
659 // and state's guard will shortly be overwritten.
660
661 if(
662 (goto_state.reachable && state.reachable) ||
664 {
665 state.guard |= goto_state.guard;
666 return std::move(state.guard);
667 }
668 else if(!state.reachable && goto_state.reachable)
669 {
670 return std::move(goto_state.guard);
671 }
672 else
673 {
674 return std::move(state.guard);
675 }
676}
677
681 statet &state)
682{
683 // check atomic section
684 if(state.atomic_section_id != goto_state.atomic_section_id)
686 "atomic sections differ across branches",
687 state.source.pc->source_location());
688
689 // Merge guards. Don't write this to `state` yet because we might move
690 // goto_state over it below.
692
693 // Merge constant propagator, value-set etc. only if the incoming state is
694 // reachable:
695 if(goto_state.reachable)
696 {
697 if(!state.reachable)
698 {
699 // Important to note that we're moving into our base class here.
700 // Note this overwrites state.guard, but we restore it below.
701 static_cast<goto_statet &>(state) = std::move(goto_state);
702 }
703 else
704 {
705 // do SSA phi functions
706 phi_function(goto_state, state);
707
708 // merge value sets
709 state.value_set.make_union(goto_state.value_set);
710
711 // adjust depth
712 state.depth = std::min(state.depth, goto_state.depth);
713 }
714 }
715
716 // Save the new state guard
717 state.guard = std::move(new_guard);
718}
719
735static void merge_names(
736 const goto_statet &goto_state,
738 const namespacet &ns,
739 const guardt &diff_guard,
740 messaget &log,
741 const bool do_simplify,
743 const incremental_dirtyt &dirty,
744 const ssa_exprt &ssa,
745 const unsigned goto_count,
746 const unsigned dest_count)
747{
748 const irep_idt l1_identifier = ssa.get_identifier();
749 const irep_idt &obj_identifier = ssa.get_object_name();
750
752 return; // just a guard, don't bother
753
755 return; // not at all changed
756
757 // changed - but only on a branch that is now dead, and the other branch is
758 // uninitialized/invalid
759 if(
760 (!dest_state.reachable && goto_count == 0) ||
761 (!goto_state.reachable && dest_count == 0))
762 {
763 return;
764 }
765
766 // field sensitivity: only merge on individual fields
767 if(dest_state.field_sensitivity.is_divisible(ssa, true))
768 return;
769
770 // shared variables are renamed on every access anyway, we don't need to
771 // merge anything
772 const symbolt &symbol = ns.lookup(obj_identifier);
773
774 // shared?
775 if(
776 dest_state.atomic_section_id == 0 && dest_state.threads.size() >= 2 &&
777 (symbol.is_shared() || dirty(symbol.name)))
778 {
779 return; // no phi nodes for shared stuff
780 }
781
782 // don't merge (thread-)locals across different threads, which
783 // may have been introduced by symex_start_thread (and will
784 // only later be removed from level2.current_names by pop_frame
785 // once the thread is executed)
786 const irep_idt level_0 = ssa.get_level_0();
787 if(
788 !level_0.empty() &&
789 level_0 != std::to_string(dest_state.source.thread_nr) && dest_count != 0)
790 {
791 return;
792 }
793
795
796 {
797 const auto p_it = goto_state.propagation.find(l1_identifier);
798
799 if(p_it.has_value())
801 else
803 }
804
805 {
806 const auto p_it = dest_state.propagation.find(l1_identifier);
807
808 if(p_it.has_value())
810 else
812 }
813
814 exprt rhs;
815
816 // Don't add a conditional to the assignment when:
817 // 1. Either guard is false, so we can't follow that branch.
818 // 2. Either identifier is of generation zero, and so hasn't been
819 // initialized and therefore an invalid target.
820
821 // These rules only apply to dynamic objects and locals.
822 if(!dest_state.reachable)
823 rhs = goto_state_rhs;
824 else if(!goto_state.reachable)
825 rhs = dest_state_rhs;
826 else if(goto_count == 0)
827 rhs = dest_state_rhs;
828 else if(dest_count == 0)
829 rhs = goto_state_rhs;
830 else
831 {
833 if(do_simplify)
834 simplify(rhs, ns);
835 }
836
837 dest_state.record_events.push(false);
838 const ssa_exprt new_lhs =
839 dest_state.assignment(ssa, rhs, ns, true, true).get();
840 dest_state.record_events.pop();
841
842 log.conditional_output(
843 log.debug(), [ns, &new_lhs](messaget::mstreamt &mstream) {
844 mstream << "Assignment to " << new_lhs.get_identifier() << " ["
845 << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
846 << messaget::eom;
847 });
848
849 target.assignment(
850 true_exprt(),
851 new_lhs,
852 new_lhs,
853 new_lhs.get_original_expr(),
854 rhs,
855 dest_state.source,
857}
858
860 const goto_statet &goto_state,
862{
863 if(
864 goto_state.get_level2().current_names.empty() &&
865 dest_state.get_level2().current_names.empty())
866 return;
867
869 // this gets the diff between the guards
870 diff_guard -= dest_state.guard;
871
873 goto_state.get_level2().current_names.get_delta_view(
874 dest_state.get_level2().current_names, delta_view, false);
875
876 for(const auto &delta_item : delta_view)
877 {
878 const ssa_exprt &ssa = delta_item.m.first;
879 unsigned goto_count = delta_item.m.second;
880 unsigned dest_count = !delta_item.is_in_both_maps()
881 ? 0
882 : delta_item.get_other_map_value().second;
883
887 ns,
889 log,
890 symex_config.simplify_opt,
891 target,
893 ssa,
895 dest_count);
896 }
897
899 dest_state.get_level2().current_names.get_delta_view(
900 goto_state.get_level2().current_names, delta_view, false);
901
902 for(const auto &delta_item : delta_view)
903 {
904 if(delta_item.is_in_both_maps())
905 continue;
906
907 const ssa_exprt &ssa = delta_item.m.first;
908 unsigned goto_count = 0;
909 unsigned dest_count = delta_item.m.second;
910
914 ns,
916 log,
917 symex_config.simplify_opt,
918 target,
920 ssa,
922 dest_count);
923 }
924}
925
927 statet &state,
928 const exprt &guard)
929{
930 const std::string loop_number = std::to_string(state.source.pc->loop_number);
931
933
934 if(symex_config.unwinding_assertions)
935 {
936 // Generate VCC for unwinding assertion.
937 const std::string property_id =
938 id2string(state.source.pc->source_location().get_function()) +
939 ".unwind." + loop_number;
940 vcc(
942 property_id,
943 "unwinding assertion loop " + loop_number,
944 state);
945 }
946
947 if(!symex_config.partial_loops)
948 {
949 // generate unwinding assumption, unless we permit partial loops
951 }
952}
953
956 const call_stackt &,
957 unsigned)
958{
959 // by default, we keep going
960 return false;
961}
Pointer Dereferencing.
bool is_failed_symbol(const exprt &expr)
Return true if, and only if, expr is the result of failed dereferencing.
static exprt guard(const exprt::operandst &guards, exprt cond)
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
The Boolean type.
Definition std_types.h:36
framet & top()
Definition call_stack.h:17
A constant literal expression.
Definition std_expr.h:3117
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
The Boolean constant false.
Definition std_expr.h:3199
Stack frames – these are used for function calls and for exceptions.
std::list< std::pair< symex_targett::sourcet, goto_statet > > goto_state_listt
Definition frame.h:25
std::unordered_map< irep_idt, loop_infot > loop_iterations
Definition frame.h:77
std::map< goto_programt::const_targett, goto_state_listt, goto_programt::target_less_than > goto_state_map
Definition frame.h:33
This class represents an instruction in the GOTO intermediate representation.
const goto_instruction_codet & code() const
Get the code represented by this instruction.
targetst targets
The list of successor instructions.
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
std::set< targett, target_less_than > incoming_edges
const exprt & condition() const
Get the condition of gotos, assume, assert.
const_targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
instructionst::const_iterator const_targett
Container for data that varies per program point, e.g.
Definition goto_state.h:32
guardt guard
Definition goto_state.h:58
unsigned depth
Distance from entry.
Definition goto_state.h:35
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition goto_state.h:62
unsigned atomic_section_id
Threads.
Definition goto_state.h:76
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition goto_state.h:51
Central data structure: state.
goto_programt::const_targett saved_target
call_stackt & call_stack()
static irep_idt guard_identifier()
renamedt< ssa_exprt, L2 > assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
guard_managert & guard_manager
renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
symex_targett::sourcet source
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind)
Determine whether to unwind a loop.
void try_filter_value_sets(goto_symex_statet &state, exprt condition, const value_sett &original_value_set, value_sett *jump_taken_value_set, value_sett *jump_not_taken_value_set, const namespacet &ns)
Try to filter value sets based on whether possible values of a pointer-typed symbol make the conditio...
void apply_goto_condition(goto_symex_statet &current_state, goto_statet &jump_taken_state, goto_statet &jump_not_taken_state, const exprt &original_guard, const exprt &new_guard, const namespacet &ns)
Propagate constants and points-to information implied by a GOTO condition.
virtual bool check_break(const irep_idt &loop_id, unsigned unwind)
Defines condition for interrupting symbolic execution for a specific loop.
void symex_unreachable_goto(statet &state)
Symbolically execute a GOTO instruction in the context of unreachable code.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
Definition goto_symex.h:241
virtual void symex_goto(statet &state)
Symbolically execute a GOTO instruction.
void phi_function(const goto_statet &goto_state, statet &dest_state)
Merge the SSA assignments from goto_state into dest_state.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition goto_symex.h:810
symex_target_equationt & target
The equation that this execution is building up.
Definition goto_symex.h:266
guard_managert & guard_manager
Used to create guards.
Definition goto_symex.h:263
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
virtual void loop_bound_exceeded(statet &state, const exprt &guard)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition goto_symex.h:258
virtual void vcc(const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state)
Symbolically execute a verification condition (assertion).
virtual void merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state)
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall sy...
virtual void do_simplify(exprt &expr)
messaget log
The messaget to write log messages to.
Definition goto_symex.h:278
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition goto_symex.h:185
bool should_pause_symex
Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution ...
Definition goto_symex.h:167
void symex_assume_l2(statet &, const exprt &cond)
void merge_gotos(statet &state)
Merge all branches joining at the current program point.
void add(const exprt &expr)
bool is_true() const
Definition guard_expr.h:60
bool disjunction_may_simplify(const guard_exprt &other_guard)
Returns true if operator|= with other_guard may result in a simpler expression.
exprt as_expr() const
Definition guard_expr.h:46
bool is_false() const
Definition guard_expr.h:65
The trinary if-then-else operator.
Definition std_expr.h:2497
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
Definition dirty.h:118
const irep_idt & id() const
Definition irep.h:388
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & debug() const
Definition message.h:421
mstreamt & statistics() const
Definition message.h:411
mstreamt & warning() const
Definition message.h:396
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition message.cpp:139
static eomt eom
Definition message.h:289
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().
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
virtual void push(const patht &)=0
Add a path to resume to the storage.
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
Expression to hold a symbol (variable)
Definition std_expr.h:131
Symbol table entry.
Definition symbol.h:28
irep_idt name
The unique identifier.
Definition symbol.h:40
bool is_shared() const
Definition symbol.h:101
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)
Write to a local variable.
The Boolean constant true.
Definition std_expr.h:3190
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
Return value for build_reference_to; see that method for documentation.
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
static bool should_ignore_value(const exprt &what, bool exclude_null_derefs, const irep_idt &language_mode)
Determine whether possible alias what should be ignored when replacing a pointer by its referees.
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition value_set.h:44
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
Symbolic Execution.
void symex_transition(goto_symext::statet &state)
Transition to the next instruction, which increments the internal program counter and initializes the...
renamedt< exprt, L2 > try_evaluate_pointer_comparisons(renamedt< exprt, L2 > condition, const value_sett &value_set, const irep_idt &language_mode, const namespacet &ns)
Try to evaluate pointer comparisons where they can be trivially determined using the value-set.
GOTO Symex constant propagation.
guard_exprt guardt
Definition guard.h:29
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
double log(double x)
Definition math.c:2449
Storage of symbolic execution paths to resume.
API to expression classes for Pointers.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Pointer Logic.
@ L1
Definition renamed.h:24
void selectively_mutate(renamedt< exprt, level > &renamed, typename renamedt< exprt, level >::mutator_functiont get_mutated_expr)
This permits replacing subexpressions of the renamed value, so long as each replacement is consistent...
Definition renamed.h:95
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#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 PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition ssa_expr.h:145
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2479
Information saved at a conditional goto to resume execution.
Identifies source in the context of symbolic execution.
goto_programt::const_targett pc
static void merge_names(const goto_statet &goto_state, goto_symext::statet &dest_state, const namespacet &ns, const guardt &diff_guard, messaget &log, const bool do_simplify, symex_target_equationt &target, const incremental_dirtyt &dirty, const ssa_exprt &ssa, const unsigned goto_count, const unsigned dest_count)
Helper function for phi_function which merges the names of an identifier for two different states.
static std::optional< renamedt< exprt, L2 > > try_evaluate_pointer_comparison(const irep_idt &operation, const symbol_exprt &symbol_expr, const exprt &other_operand, const value_sett &value_set, const irep_idt language_mode, const namespacet &ns)
Try to evaluate a simple pointer comparison.
renamedt< exprt, L2 > try_evaluate_pointer_comparisons(renamedt< exprt, L2 > condition, const value_sett &value_set, const irep_idt &language_mode, const namespacet &ns)
Try to evaluate pointer comparisons where they can be trivially determined using the value-set.
static guardt merge_state_guards(goto_statet &goto_state, goto_symex_statet &state)
Pointer Dereferencing.