cprover
Loading...
Searching...
No Matches
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
31 goto_symex_statet &current_state,
32 goto_statet &jump_taken_state,
33 goto_statet &jump_not_taken_state,
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
52 current_state,
53 original_guard,
54 jump_taken_state.value_set,
55 &jump_taken_state.value_set,
56 &jump_not_taken_state.value_set,
57 ns);
58
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:
66 const exprt negated_new_guard = boolean_negate(new_guard);
67 jump_not_taken_state.apply_condition(negated_new_guard, current_state, ns);
68}
69
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{
89 const constant_exprt *constant_expr =
90 expr_try_dynamic_cast<constant_exprt>(other_operand);
91
92 if(
93 skip_typecast(other_operand).id() != ID_address_of &&
94 (!constant_expr || constant_expr->get_value() != ID_NULL))
95 {
96 return {};
97 }
98
99 const ssa_exprt *ssa_symbol_expr =
100 expr_try_dynamic_cast<ssa_exprt>(symbol_expr);
101
102 ssa_exprt l1_expr{*ssa_symbol_expr};
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(
112 value_set_element.id() == ID_unknown ||
113 value_set_element.id() == ID_invalid ||
115 to_object_descriptor_expr(value_set_element).root_object()) ||
116 to_object_descriptor_expr(value_set_element).offset().id() == ID_unknown)
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
137 exprt test_equal = simplify_expr(
139 typecast_exprt::conditional_cast(value.pointer, other_operand.type()),
140 other_operand},
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{})
161 : make_renamed<L2>(true_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{})
168 : make_renamed<L2>(false_exprt{});
169 }
170 else
171 {
172 return {};
173 }
174}
175
184 const renamedt<exprt, L2> &renamed_expr,
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
201 const symbol_exprt *symbol_expr_lhs =
202 expr_try_dynamic_cast<symbol_exprt>(lhs);
203
204 if(!symbol_expr_lhs)
205 return {};
206
207 if(!goto_symex_is_constantt()(rhs))
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.get_condition(), state, false);
237
238 renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
239 renamed_guard = try_evaluate_pointer_comparisons(
240 std::move(renamed_guard), state.value_set, language_mode, ns);
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
254 target.goto_instruction(state.guard.as_expr(), renamed_guard, state.source);
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(
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
282 exprt negated_guard = not_exprt{new_guard};
283 do_simplify(negated_guard);
284 log.statistics() << "replacing self-loop at "
285 << state.source.pc->source_location() << " by assume("
286 << from_expr(ns, state.source.function_id, negated_guard)
287 << ")" << messaget::eom;
289 {
290 log.warning()
291 << "no unwinding assertion will be generated for self-loop at "
292 << state.source.pc->source_location() << messaget::eom;
293 }
294 symex_assume_l2(state, negated_guard);
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
310 loop_bound_exceeded(state, new_guard);
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.
339 {
341 instruction.targets.size() > 0,
342 "Instruction is an unconditional goto with no target: " +
343 instruction.get_code().pretty());
344 symex_transition(state, instruction.get_target(), true);
345 return;
346 }
347
348 goto_programt::const_targett new_state_pc, state_pc;
349 symex_targett::sourcet original_source=state.source;
350
351 if(!backward)
352 {
353 new_state_pc=goto_target;
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
362 if(state_pc==goto_target)
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++;
372 state_pc=goto_target;
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->get_code().pretty() +
387 "\nwe were intending "
388 "to explore " +
389 new_state_pc->get_code().pretty() +
390 "\nthe "
391 "instruction we think we saw on a previous path exploration is " +
392 state_pc->get_code().pretty());
393 goto_programt::const_targett tmp = new_state_pc;
394 new_state_pc = state_pc;
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 }
406 {
407 // We should save both the instruction after this goto, and the target of
408 // the goto.
409
410 path_storaget::patht next_instruction(target, state);
411 next_instruction.state.saved_target = state_pc;
412 next_instruction.state.has_saved_next_instruction = true;
413
414 path_storaget::patht jump_target(target, state);
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;
427 path_storage.push(next_instruction);
428 path_storage.push(jump_target);
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
439 framet::goto_state_listt &goto_state_list =
440 state.call_stack().top().goto_state_map[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
451 symex_transition(state, state_pc, backward);
452
454 state.reachable = false;
455 }
456 else
457 {
458 goto_state_list.emplace_back(state.source, state);
459
460 symex_transition(state, state_pc, backward);
461
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,
472 taken_state,
473 not_taken_state,
474 instruction.get_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 {
491 symbol_exprt guard_symbol_expr =
493 exprt new_rhs = boolean_negate(new_guard);
494
495 ssa_exprt new_lhs =
496 state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns).get();
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(),
512 new_lhs, new_lhs, guard_symbol_expr,
513 new_rhs,
514 original_source,
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());
564 goto_programt::const_targett goto_target = instruction.get_target();
565
566 auto queue_unreachable_state_at_target = [&]() {
567 framet::goto_state_listt &goto_state_list =
568 state.call_stack().top().goto_state_map[goto_target];
569 goto_statet new_state(state.guard_manager);
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.get_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:
585 queue_unreachable_state_at_target();
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:
609 queue_unreachable_state_at_target();
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
634 framet::goto_state_listt &state_list = state_map_it->second;
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) ||
663 state.guard.disjunction_may_simplify(goto_state.guard))
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
680 goto_statet &&goto_state,
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.
691 guardt new_guard = merge_state_guards(goto_state, state);
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,
737 goto_symext::statet &dest_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
751 if(obj_identifier == goto_symext::statet::guard_identifier())
752 return; // just a guard, don't bother
753
754 if(goto_count == dest_count)
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))
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(!level_0.empty() && level_0 != std::to_string(dest_state.source.thread_nr))
788 return;
789
790 exprt goto_state_rhs = ssa, dest_state_rhs = ssa;
791
792 {
793 const auto p_it = goto_state.propagation.find(l1_identifier);
794
795 if(p_it.has_value())
796 goto_state_rhs = *p_it;
797 else
798 to_ssa_expr(goto_state_rhs).set_level_2(goto_count);
799 }
800
801 {
802 const auto p_it = dest_state.propagation.find(l1_identifier);
803
804 if(p_it.has_value())
805 dest_state_rhs = *p_it;
806 else
807 to_ssa_expr(dest_state_rhs).set_level_2(dest_count);
808 }
809
810 exprt rhs;
811
812 // Don't add a conditional to the assignment when:
813 // 1. Either guard is false, so we can't follow that branch.
814 // 2. Either identifier is of generation zero, and so hasn't been
815 // initialized and therefore an invalid target.
816
817 // These rules only apply to dynamic objects and locals.
818 if(!dest_state.reachable)
819 rhs = goto_state_rhs;
820 else if(!goto_state.reachable)
821 rhs = dest_state_rhs;
822 else if(goto_count == 0)
823 rhs = dest_state_rhs;
824 else if(dest_count == 0)
825 rhs = goto_state_rhs;
826 else
827 {
828 rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);
829 if(do_simplify)
830 simplify(rhs, ns);
831 }
832
833 dest_state.record_events.push(false);
834 const ssa_exprt new_lhs =
835 dest_state.assignment(ssa, rhs, ns, true, true).get();
836 dest_state.record_events.pop();
837
839 log.debug(), [ns, &new_lhs](messaget::mstreamt &mstream) {
840 mstream << "Assignment to " << new_lhs.get_identifier() << " ["
841 << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
842 << messaget::eom;
843 });
844
845 target.assignment(
846 true_exprt(),
847 new_lhs,
848 new_lhs,
849 new_lhs.get_original_expr(),
850 rhs,
851 dest_state.source,
853}
854
856 const goto_statet &goto_state,
857 statet &dest_state)
858{
859 if(
860 goto_state.get_level2().current_names.empty() &&
861 dest_state.get_level2().current_names.empty())
862 return;
863
864 guardt diff_guard = goto_state.guard;
865 // this gets the diff between the guards
866 diff_guard -= dest_state.guard;
867
870 dest_state.get_level2().current_names, delta_view, false);
871
872 for(const auto &delta_item : delta_view)
873 {
874 const ssa_exprt &ssa = delta_item.m.first;
875 unsigned goto_count = delta_item.m.second;
876 unsigned dest_count = !delta_item.is_in_both_maps()
877 ? 0
878 : delta_item.get_other_map_value().second;
879
881 goto_state,
882 dest_state,
883 ns,
884 diff_guard,
885 log,
887 target,
889 ssa,
890 goto_count,
891 dest_count);
892 }
893
894 delta_view.clear();
896 goto_state.get_level2().current_names, delta_view, false);
897
898 for(const auto &delta_item : delta_view)
899 {
900 if(delta_item.is_in_both_maps())
901 continue;
902
903 const ssa_exprt &ssa = delta_item.m.first;
904 unsigned goto_count = 0;
905 unsigned dest_count = delta_item.m.second;
906
908 goto_state,
909 dest_state,
910 ns,
911 diff_guard,
912 log,
914 target,
916 ssa,
917 goto_count,
918 dest_count);
919 }
920}
921
923 statet &state,
924 const exprt &guard)
925{
926 const unsigned loop_number=state.source.pc->loop_number;
927
928 exprt negated_cond;
929
930 if(guard.is_true())
931 negated_cond=false_exprt();
932 else
933 negated_cond=not_exprt(guard);
934
936 {
938 {
939 // Generate VCC for unwinding assertion.
940 vcc(
941 negated_cond,
942 "unwinding assertion loop " + std::to_string(loop_number),
943 state);
944 }
945
946 // generate unwinding assumption, unless we permit partial loops
947 symex_assume_l2(state, negated_cond);
948
950 {
951 // add to state guard to prevent further assignments
952 state.guard.add(negated_cond);
953 }
954 }
955}
956
959 const call_stackt &,
960 unsigned)
961{
962 // by default, we keep going
963 return false;
964}
Pointer Dereferencing.
bool is_failed_symbol(const exprt &expr)
Return true if, and only if, expr is the result of failed dereferencing.
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
The Boolean type.
Definition: std_types.h:36
framet & top()
Definition: call_stack.h:17
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2865
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
std::set< targett > incoming_edges
Definition: goto_program.h:431
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
targetst targets
The list of successor instructions.
Definition: goto_program.h:403
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:367
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:550
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:407
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:781
instructionst::const_iterator const_targett
Definition: goto_program.h:593
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
void apply_condition(const exprt &condition, const goto_symex_statet &previous_state, const namespacet &ns)
Given a condition that must hold on this path, propagate as much knowledge as possible.
Definition: goto_state.cpp:42
unsigned atomic_section_id
Threads.
Definition: goto_state.h:76
sharing_mapt< irep_idt, exprt > propagation
Definition: goto_state.h:71
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:51
const symex_level2t & get_level2() const
Definition: goto_state.h:45
Central data structure: state.
goto_programt::const_targett saved_target
call_stackt & call_stack()
NODISCARD 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...
std::stack< bool > record_events
static irep_idt guard_identifier()
NODISCARD 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
field_sensitivityt field_sensitivity
symex_targett::sourcet source
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
std::vector< threadt > threads
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind)
Determine whether to unwind a loop.
Definition: symex_goto.cpp:957
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...
Definition: symex_main.cpp:781
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.
Definition: symex_goto.cpp:30
virtual bool check_break(const irep_idt &loop_id, unsigned unwind)
Defines condition for interrupting symbolic execution for a specific loop.
Definition: symex_goto.cpp:617
void symex_unreachable_goto(statet &state)
Symbolically execute a GOTO instruction in the context of unreachable code.
Definition: symex_goto.cpp:544
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:226
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:185
virtual void symex_goto(statet &state)
Symbolically execute a GOTO instruction.
Definition: symex_goto.cpp:230
void phi_function(const goto_statet &goto_state, statet &dest_state)
Merge the SSA assignments from goto_state into dest_state.
Definition: symex_goto.cpp:855
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:788
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:251
guard_managert & guard_manager
Used to create guards.
Definition: goto_symex.h:248
virtual void loop_bound_exceeded(statet &state, const exprt &guard)
Definition: symex_goto.cpp:922
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:243
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...
Definition: symex_goto.cpp:678
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:34
messaget log
The messaget to write log messages to.
Definition: goto_symex.h:263
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:170
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:152
void symex_assume_l2(statet &, const exprt &cond)
Definition: symex_main.cpp:222
void merge_gotos(statet &state)
Merge all branches joining at the current program point.
Definition: symex_goto.cpp:623
void add(const exprt &expr)
Definition: guard_expr.cpp:39
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.
Definition: guard_expr.cpp:124
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:2226
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:119
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irep_idt & id() const
Definition: irep.h:396
source_locationt source_location
Definition: message.h:247
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & debug() const
Definition: message.h:429
mstreamt & statistics() const
Definition: message.h:419
mstreamt & warning() const
Definition: message.h:404
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:297
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:138
Boolean negation.
Definition: std_expr.h:2181
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
Definition: path_storage.h:116
virtual void push(const patht &)=0
Add a path to resume to the storage.
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
void simplify(const namespacet &ns)
Definition: renamed.h:45
const underlyingt & get() const
Definition: renamed.h:40
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
Definition: sharing_map.h:439
bool empty() const
Check if map is empty.
Definition: sharing_map.h:360
void get_delta_view(const sharing_mapt &other, delta_viewt &delta_view, const bool only_common=true) const
Get a delta view of the elements in the map.
Definition: sharing_map.h:939
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
void set_level_2(std::size_t i)
Definition: ssa_expr.cpp:192
void remove_level_2()
Definition: ssa_expr.cpp:198
const irep_idt get_level_0() const
Definition: ssa_expr.h:63
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
irep_idt get_object_name() const
Definition: ssa_expr.cpp:144
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Symbol table entry.
Definition: symbol.h:28
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_shared() const
Definition: symbol.h:95
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:2856
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
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:43
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
Definition: value_set.cpp:354
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
Definition: value_set.cpp:287
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:126
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...
Definition: symex_main.cpp:150
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.
Definition: symex_goto.cpp:214
GOTO Symex constant propagation.
guard_exprt guardt
Definition: guard.h:27
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
nonstd::optional< T > optionalt
Definition: optional.h:35
Storage of symbolic execution paths to resume.
API to expression classes for Pointers.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:66
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: pointer_expr.h:238
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:510
#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:627
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:173
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206
Stack frames – these are used for function calls and for exceptions.
Definition: frame.h:22
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:73
std::map< goto_programt::const_targett, goto_state_listt > goto_state_map
Definition: frame.h:29
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:42
goto_symex_statet state
Definition: path_storage.h:44
bool partial_loops
Definition: symex_config.h:35
bool unwinding_assertions
Definition: symex_config.h:33
bool constant_propagation
Definition: symex_config.h:27
bool self_loops_to_assumptions
Definition: symex_config.h:29
bool doing_path_exploration
Definition: symex_config.h:23
symex_renaming_levelt current_names
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
goto_programt::const_targett pc
Definition: symex_target.h:42
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.
Definition: symex_goto.cpp:735
static optionalt< 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.
Definition: symex_goto.cpp:81
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.
Definition: symex_goto.cpp:214
static guardt merge_state_guards(goto_statet &goto_state, goto_symex_statet &state)
Definition: symex_goto.cpp:647
Pointer Dereferencing.