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>
16#include <util/simplify_expr.h>
17#include <util/std_expr.h>
18
20
21#include "goto_symex.h"
22#include "path_storage.h"
24
25#include <algorithm>
26
28 goto_symex_statet &current_state,
29 goto_statet &jump_taken_state,
30 goto_statet &jump_not_taken_state,
31 const exprt &original_guard,
32 const exprt &new_guard,
33 const namespacet &ns)
34{
35 // It would be better to call try_filter_value_sets after apply_condition,
36 // and pass nullptr for value sets which apply_condition successfully updated
37 // already. However, try_filter_value_sets calls rename to do constant
38 // propagation, and apply_condition can update the constant propagator. Since
39 // apply condition will never succeed on both jump_taken_state and
40 // jump_not_taken_state, it should be possible to pass a reference to an
41 // unmodified goto_statet to use for renaming. But renaming needs a
42 // goto_symex_statet, not just a goto_statet, and we only have access to one
43 // of those. A future improvement would be to split rename into two parts:
44 // one part on goto_symex_statet which is non-const and deals with
45 // l2 thread reads, and one part on goto_statet which is const and could be
46 // used in try_filter_value_sets.
47
49 current_state,
50 original_guard,
51 jump_taken_state.value_set,
52 &jump_taken_state.value_set,
53 &jump_not_taken_state.value_set,
54 ns);
55
56 if(!symex_config.constant_propagation)
57 return;
58
59 jump_taken_state.apply_condition(new_guard, current_state, ns);
60
61 // Could use not_exprt + simplify, but let's avoid paying that cost on quite
62 // a hot path:
63 const exprt negated_new_guard = boolean_negate(new_guard);
64 jump_not_taken_state.apply_condition(negated_new_guard, current_state, ns);
65}
66
68{
70
71 const goto_programt::instructiont &instruction=*state.source.pc;
72
73 exprt new_guard = clean_expr(instruction.condition(), state, false);
74
75 renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
76 if(symex_config.simplify_opt)
77 {
79 renamed_guard.simplify(simp);
80 }
81 new_guard = renamed_guard.get();
82
83 if(new_guard.is_false())
84 {
85 target.location(state.guard.as_expr(), state.source);
86
87 // next instruction
88 symex_transition(state);
89 return; // nothing to do
90 }
91
92 target.goto_instruction(state.guard.as_expr(), renamed_guard, state.source);
93
95 !instruction.targets.empty(), "goto should have at least one target");
96
97 // we only do deterministic gotos for now
99 instruction.targets.size() == 1, "no support for non-deterministic gotos");
100
102 instruction.get_target();
103
104 const bool backward = instruction.is_backwards_goto();
105
106 if(backward)
107 {
108 // is it label: goto label; or while(cond); - popular in SV-COMP
109 if(
110 symex_config.self_loops_to_assumptions &&
111 // label: goto label; or do {} while(cond);
112 (goto_target == state.source.pc ||
113 // while(cond);
114 (instruction.incoming_edges.size() == 1 &&
115 *instruction.incoming_edges.begin() == goto_target &&
116 goto_target->is_goto() && new_guard.is_true())))
117 {
118 // generate assume(false) or a suitable negation if this
119 // instruction is a conditional goto
120 exprt negated_guard = boolean_negate(new_guard);
121 do_simplify(negated_guard, state.value_set);
122 log.statistics() << "replacing self-loop at "
123 << state.source.pc->source_location() << " by assume("
124 << from_expr(ns, state.source.function_id, negated_guard)
125 << ")" << messaget::eom;
126 if(symex_config.unwinding_assertions)
127 {
128 log.warning()
129 << "no unwinding assertion will be generated for self-loop at "
130 << state.source.pc->source_location() << messaget::eom;
131 }
132 symex_assume_l2(state, negated_guard);
133
134 // next instruction
135 symex_transition(state);
136 return;
137 }
138
139 const auto loop_id =
141
142 unsigned &unwind = state.call_stack().top().loop_iterations[loop_id].count;
143 unwind++;
144
145 if(should_stop_unwind(state.source, state.call_stack(), unwind))
146 {
147 // we break the loop
148 loop_bound_exceeded(state, new_guard);
149
150 // next instruction
151 symex_transition(state);
152 return;
153 }
154
155 if(new_guard.is_true())
156 {
157 // we continue executing the loop
158 if(check_break(loop_id, unwind))
159 {
160 should_pause_symex = true;
161 }
162 symex_transition(state, goto_target, true);
163 return; // nothing else to do
164 }
165 }
166
167 // No point executing both branches of an unconditional goto.
168 if(
169 new_guard.is_true() && // We have an unconditional goto, AND
170 // either there are no reachable blocks between us and the target in the
171 // surrounding scope (because state.guard == true implies there is no path
172 // around this GOTO instruction)
173 (state.guard.is_true() ||
174 // or there is another block, but we're doing path exploration so
175 // we're going to skip over it for now and return to it later.
176 symex_config.doing_path_exploration))
177 {
179 instruction.targets.size() > 0,
180 "Instruction is an unconditional goto with no target: " +
181 instruction.code().pretty());
182 symex_transition(state, instruction.get_target(), true);
183 return;
184 }
185
186 goto_programt::const_targett new_state_pc, state_pc;
187 symex_targett::sourcet original_source=state.source;
188
189 if(!backward)
190 {
191 new_state_pc=goto_target;
192 state_pc=state.source.pc;
193 state_pc++;
194
195 // skip dead instructions
196 if(new_guard.is_true())
197 while(state_pc!=goto_target && !state_pc->is_target())
198 ++state_pc;
199
200 if(state_pc==goto_target)
201 {
202 symex_transition(state, goto_target, false);
203 return; // nothing else to do
204 }
205 }
206 else
207 {
208 new_state_pc=state.source.pc;
209 new_state_pc++;
210 state_pc=goto_target;
211 }
212
213 // Normally the next instruction to execute would be state_pc and we save
214 // new_state_pc for later. But if we're executing from a saved state, then
215 // new_state_pc should be the state that we saved from earlier, so let's
216 // execute that instead.
217 if(state.has_saved_jump_target)
218 {
219 INVARIANT(
220 new_state_pc == state.saved_target,
221 "Tried to explore the other path of a branch, but the next "
222 "instruction along that path is not the same as the instruction "
223 "that we saved at the branch point. Saved instruction is " +
224 state.saved_target->code().pretty() +
225 "\nwe were intending "
226 "to explore " +
227 new_state_pc->code().pretty() +
228 "\nthe "
229 "instruction we think we saw on a previous path exploration is " +
230 state_pc->code().pretty());
231 goto_programt::const_targett tmp = new_state_pc;
232 new_state_pc = state_pc;
233 state_pc = tmp;
234
235 log.debug() << "Resuming from jump target '" << state_pc->source_location()
236 << "'" << log.eom;
237 }
238 else if(state.has_saved_next_instruction)
239 {
240 log.debug() << "Resuming from next instruction '"
241 << state_pc->source_location() << "'" << log.eom;
242 }
243 else if(symex_config.doing_path_exploration)
244 {
245 // We should save both the instruction after this goto, and the target of
246 // the goto.
247
248 path_storaget::patht next_instruction(target, state);
249 next_instruction.state.saved_target = state_pc;
250 next_instruction.state.has_saved_next_instruction = true;
251
252 path_storaget::patht jump_target(target, state);
253 jump_target.state.saved_target = new_state_pc;
254 jump_target.state.has_saved_jump_target = true;
255 // `forward` tells us where the branch we're _currently_ executing is
256 // pointing to; this needs to be inverted for the branch that we're saving,
257 // so let its truth value for `backwards` be the same as ours for `forward`.
258
259 log.debug() << "Saving next instruction '"
260 << next_instruction.state.saved_target->source_location() << "'"
261 << log.eom;
262 log.debug() << "Saving jump target '"
263 << jump_target.state.saved_target->source_location() << "'"
264 << log.eom;
265 path_storage.push(next_instruction);
266 path_storage.push(jump_target);
267
268 // It is now up to the caller of symex to decide which path to continue
269 // executing. Signal to the caller that states have been pushed (therefore
270 // symex has not yet completed and must be resumed), and bail out.
271 should_pause_symex = true;
272 return;
273 }
274
275 // put a copy of the current state into the state-queue, to be used by
276 // merge_gotos when we visit new_state_pc
277 framet::goto_state_listt &goto_state_list =
278 state.call_stack().top().goto_state_map[new_state_pc];
279
280 // On an unconditional GOTO we don't need our state, as it will be overwritten
281 // by merge_goto. Therefore we move it onto goto_state_list instead of copying
282 // as usual.
283 if(new_guard.is_true())
284 {
285 // The move here only moves goto_statet, the base class of goto_symex_statet
286 // and not the entire thing.
287 goto_state_list.emplace_back(state.source, std::move(state));
288
289 symex_transition(state, state_pc, backward);
290
292 state.reachable = false;
293 }
294 else
295 {
296 goto_state_list.emplace_back(state.source, state);
297
298 symex_transition(state, state_pc, backward);
299
300 if(!symex_config.doing_path_exploration)
301 {
302 // This doesn't work for --paths (single-path mode) yet, as in multi-path
303 // mode we remove the implied constants at a control-flow merge, but in
304 // single-path mode we don't run merge_gotos.
305 auto &taken_state = backward ? state : goto_state_list.back().second;
306 auto &not_taken_state = backward ? goto_state_list.back().second : state;
307
309 state,
310 taken_state,
311 not_taken_state,
312 instruction.condition(),
313 new_guard,
314 ns);
315 }
316
317 // produce new guard symbol
318 exprt guard_expr;
319
320 if(
321 new_guard.id() == ID_symbol ||
322 (new_guard.id() == ID_not &&
323 to_not_expr(new_guard).op().id() == ID_symbol))
324 {
325 guard_expr=new_guard;
326 }
327 else
328 {
329 symbol_exprt guard_symbol_expr =
331 exprt new_rhs = boolean_negate(new_guard);
332
333 ssa_exprt new_lhs =
334 state.rename_ssa<L1>(ssa_exprt{guard_symbol_expr}, ns).get();
335 new_lhs =
336 state.assignment(std::move(new_lhs), new_rhs, ns, true, false).get();
337
339
340 log.conditional_output(
341 log.debug(),
342 [this, &new_lhs](messaget::mstreamt &mstream) {
343 mstream << "Assignment to " << new_lhs.get_identifier()
344 << " [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
345 << messaget::eom;
346 });
347
348 target.assignment(
349 guard.as_expr(),
350 new_lhs, new_lhs, guard_symbol_expr,
351 new_rhs,
352 original_source,
354
355 guard_expr = state.rename(boolean_negate(guard_symbol_expr), ns).get();
356 }
357
358 if(state.has_saved_jump_target)
359 {
360 if(!backward)
361 state.guard.add(guard_expr);
362 else
363 state.guard.add(boolean_negate(guard_expr));
364 }
365 else
366 {
367 goto_statet &new_state = goto_state_list.back().second;
368 if(!backward)
369 {
370 new_state.guard.add(guard_expr);
371 state.guard.add(boolean_negate(guard_expr));
372 }
373 else
374 {
375 state.guard.add(guard_expr);
376 new_state.guard.add(boolean_negate(guard_expr));
377 }
378 }
379 }
380}
381
383{
384 PRECONDITION(!state.reachable);
385 // This is like symex_goto, except the state is unreachable. We try to take
386 // some arbitrary choice that maintains the state guard in a reasonable state
387 // in order that it simplifies properly when states are merged (in
388 // merge_gotos). Note we can't try to evaluate the actual GOTO guard because
389 // our constant propagator might be out of date, since we haven't been
390 // executing assign instructions.
391
392 // If the guard is already false then there's no value in this state; just
393 // carry on and check the next instruction.
394 if(state.guard.is_false())
395 {
396 symex_transition(state);
397 return;
398 }
399
400 const goto_programt::instructiont &instruction = *state.source.pc;
401 PRECONDITION(instruction.is_goto());
402 goto_programt::const_targett goto_target = instruction.get_target();
403
404 auto queue_unreachable_state_at_target = [&]() {
405 framet::goto_state_listt &goto_state_list =
406 state.call_stack().top().goto_state_map[goto_target];
407 goto_statet new_state(state.guard_manager);
408 new_state.guard = state.guard;
409 new_state.reachable = false;
410 goto_state_list.emplace_back(state.source, std::move(new_state));
411 };
412
413 if(instruction.condition().is_true())
414 {
415 if(instruction.is_backwards_goto())
416 {
417 // Give up trying to salvage the guard
418 // (this state's guard is squashed, without queueing it at the target)
419 }
420 else
421 {
422 // Take the branch:
423 queue_unreachable_state_at_target();
424 }
425
426 state.guard.add(false_exprt());
427 }
428 else
429 {
430 // Arbitrarily assume a conditional branch is not-taken, except for when
431 // there's an incoming backedge, when we guess that the taken case is less
432 // likely to lead to that backedge than the not-taken case.
433 bool maybe_loop_head = std::any_of(
434 instruction.incoming_edges.begin(),
435 instruction.incoming_edges.end(),
436 [&instruction](const goto_programt::const_targett predecessor) {
437 return predecessor->location_number > instruction.location_number;
438 });
439
440 if(instruction.is_backwards_goto() || !maybe_loop_head)
441 {
442 // Assume branch not taken (fall through)
443 }
444 else
445 {
446 // Assume branch taken:
447 queue_unreachable_state_at_target();
448 state.guard.add(false_exprt());
449 }
450 }
451
452 symex_transition(state);
453}
454
455bool goto_symext::check_break(const irep_idt &loop_id, unsigned unwind)
456{
457 // dummy implementation
458 return false;
459}
460
462{
463 framet &frame = state.call_stack().top();
464
465 // first, see if this is a target at all
466 auto state_map_it = frame.goto_state_map.find(state.source.pc);
467
468 if(state_map_it==frame.goto_state_map.end())
469 return; // nothing to do
470
471 // we need to merge
472 framet::goto_state_listt &state_list = state_map_it->second;
473
474 for(auto list_it = state_list.rbegin(); list_it != state_list.rend();
475 ++list_it)
476 {
477 merge_goto(list_it->first, std::move(list_it->second), state);
478 }
479
480 // clean up to save some memory
481 frame.goto_state_map.erase(state_map_it);
482}
483
484static guardt
486{
487 // adjust guard, even using guards from unreachable states. This helps to
488 // shrink the state guard if the incoming edge is from a path that was
489 // truncated by config.unwind, config.depth or an assume-false instruction.
490
491 // Note when an unreachable state contributes its guard, merging it in is
492 // optional, since the formula already implies the unreachable guard is
493 // impossible. Therefore we only integrate it when to do so simplifies the
494 // state guard.
495
496 // This function can trash either state's guards, since goto_state is dying
497 // and state's guard will shortly be overwritten.
498
499 if(
500 (goto_state.reachable && state.reachable) ||
501 state.guard.disjunction_may_simplify(goto_state.guard))
502 {
503 state.guard |= goto_state.guard;
504 return std::move(state.guard);
505 }
506 else if(!state.reachable && goto_state.reachable)
507 {
508 return std::move(goto_state.guard);
509 }
510 else
511 {
512 return std::move(state.guard);
513 }
514}
515
518 goto_statet &&goto_state,
519 statet &state)
520{
521 // check atomic section
522 if(state.atomic_section_id != goto_state.atomic_section_id)
524 "atomic sections differ across branches",
525 state.source.pc->source_location());
526
527 // Merge guards. Don't write this to `state` yet because we might move
528 // goto_state over it below.
529 guardt new_guard = merge_state_guards(goto_state, state);
530
531 // Merge constant propagator, value-set etc. only if the incoming state is
532 // reachable:
533 if(goto_state.reachable)
534 {
535 if(!state.reachable)
536 {
537 // Important to note that we're moving into our base class here.
538 // Note this overwrites state.guard, but we restore it below.
539 static_cast<goto_statet &>(state) = std::move(goto_state);
540 }
541 else
542 {
543 // do SSA phi functions
544 phi_function(goto_state, state);
545
546 // merge value sets
547 state.value_set.make_union(goto_state.value_set);
548
549 // adjust depth
550 state.depth = std::min(state.depth, goto_state.depth);
551 }
552 }
553
554 // Save the new state guard
555 state.guard = std::move(new_guard);
556}
557
573static void merge_names(
574 const goto_statet &goto_state,
575 goto_symext::statet &dest_state,
576 const namespacet &ns,
577 const guardt &diff_guard,
578 messaget &log,
579 const bool do_simplify,
581 const incremental_dirtyt &dirty,
582 const ssa_exprt &ssa,
583 const std::size_t goto_count,
584 const std::size_t dest_count)
585{
586 const irep_idt l1_identifier = ssa.get_identifier();
587 const irep_idt &obj_identifier = ssa.get_object_name();
588
589 if(obj_identifier == goto_symext::statet::guard_identifier())
590 return; // just a guard, don't bother
591
592 if(goto_count == dest_count)
593 return; // not at all changed
594
595 // changed - but only on a branch that is now dead, and the other branch is
596 // uninitialized/invalid
597 if(
598 (!dest_state.reachable && goto_count == 0) ||
599 (!goto_state.reachable && dest_count == 0))
600 {
601 return;
602 }
603
604 // field sensitivity: only merge on individual fields
605 if(dest_state.field_sensitivity.is_divisible(ssa, true))
606 return;
607
608 // shared variables are renamed on every access anyway, we don't need to
609 // merge anything
610 const symbolt &symbol = ns.lookup(obj_identifier);
611
612 // shared?
613 if(
614 dest_state.atomic_section_id == 0 && dest_state.threads.size() >= 2 &&
615 (symbol.is_shared() || dirty(symbol.name)))
616 {
617 return; // no phi nodes for shared stuff
618 }
619
620 // don't merge (thread-)locals across different threads, which
621 // may have been introduced by symex_start_thread (and will
622 // only later be removed from level2.current_names by pop_frame
623 // once the thread is executed)
624 const irep_idt level_0 = ssa.get_level_0();
625 if(
626 !level_0.empty() &&
627 level_0 != std::to_string(dest_state.source.thread_nr) && dest_count != 0)
628 {
629 return;
630 }
631
632 exprt goto_state_rhs = ssa, dest_state_rhs = ssa;
633
634 {
635 const auto p_it = goto_state.propagation.find(l1_identifier);
636
637 if(p_it.has_value())
638 goto_state_rhs = *p_it;
639 else
640 to_ssa_expr(goto_state_rhs).set_level_2(goto_count);
641 }
642
643 {
644 const auto p_it = dest_state.propagation.find(l1_identifier);
645
646 if(p_it.has_value())
647 dest_state_rhs = *p_it;
648 else
649 to_ssa_expr(dest_state_rhs).set_level_2(dest_count);
650 }
651
652 exprt rhs;
653
654 // Don't add a conditional to the assignment when:
655 // 1. Either guard is false, so we can't follow that branch.
656 // 2. Either identifier is of generation zero, and so hasn't been
657 // initialized and therefore an invalid target.
658
659 // These rules only apply to dynamic objects and locals.
660 if(!dest_state.reachable)
661 rhs = goto_state_rhs;
662 else if(!goto_state.reachable)
663 rhs = dest_state_rhs;
664 else if(goto_count == 0)
665 rhs = dest_state_rhs;
666 else if(dest_count == 0)
667 rhs = goto_state_rhs;
668 else
669 {
670 rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);
671 if(do_simplify)
672 {
673 // Do not value-set supported filtering here as neither dest_state nor
674 // goto_state necessarily have a comprehensive value set.
675 simplify(rhs, ns);
676 }
677 }
678
679 dest_state.record_events.push(false);
680 const ssa_exprt new_lhs =
681 dest_state.assignment(ssa, rhs, ns, true, true).get();
682 dest_state.record_events.pop();
683
685 log.debug(), [ns, &new_lhs](messaget::mstreamt &mstream) {
686 mstream << "Assignment to " << new_lhs.get_identifier() << " ["
687 << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
688 << messaget::eom;
689 });
690
691 target.assignment(
692 true_exprt(),
693 new_lhs,
694 new_lhs,
695 new_lhs.get_original_expr(),
696 rhs,
697 dest_state.source,
699}
700
702 const goto_statet &goto_state,
703 statet &dest_state)
704{
705 if(
706 goto_state.get_level2().current_names.empty() &&
707 dest_state.get_level2().current_names.empty())
708 return;
709
710 guardt diff_guard = goto_state.guard;
711 // this gets the diff between the guards
712 diff_guard -= dest_state.guard;
713
716 dest_state.get_level2().current_names, delta_view, false);
717
718 for(const auto &delta_item : delta_view)
719 {
720 const ssa_exprt &ssa = delta_item.m.first;
721 std::size_t goto_count = delta_item.m.second;
722 std::size_t dest_count = !delta_item.is_in_both_maps()
723 ? 0
724 : delta_item.get_other_map_value().second;
725
727 goto_state,
728 dest_state,
729 ns,
730 diff_guard,
731 log,
732 symex_config.simplify_opt,
733 target,
734 path_storage.dirty,
735 ssa,
736 goto_count,
737 dest_count);
738 }
739
740 delta_view.clear();
742 goto_state.get_level2().current_names, delta_view, false);
743
744 for(const auto &delta_item : delta_view)
745 {
746 if(delta_item.is_in_both_maps())
747 continue;
748
749 const ssa_exprt &ssa = delta_item.m.first;
750 std::size_t goto_count = 0;
751 std::size_t dest_count = delta_item.m.second;
752
754 goto_state,
755 dest_state,
756 ns,
757 diff_guard,
758 log,
759 symex_config.simplify_opt,
760 target,
761 path_storage.dirty,
762 ssa,
763 goto_count,
764 dest_count);
765 }
766}
767
769 statet &state,
770 const exprt &guard)
771{
772 const std::string loop_number = std::to_string(state.source.pc->loop_number);
773
774 exprt negated_cond = boolean_negate(guard);
775
776 if(symex_config.unwinding_assertions)
777 {
778 // Generate VCC for unwinding assertion.
779 const std::string property_id =
780 id2string(state.source.pc->source_location().get_function()) +
781 ".unwind." + loop_number;
782 vcc(
783 negated_cond,
784 property_id,
785 "unwinding assertion loop " + loop_number,
786 state);
787 }
788
789 if(!symex_config.partial_loops)
790 {
791 // generate unwinding assumption, unless we permit partial loops
792 symex_assume_l2(state, negated_cond);
793 }
794}
795
798 const call_stackt &,
799 unsigned)
800{
801 // by default, we keep going
802 return false;
803}
static exprt guard(const exprt::operandst &guards, exprt cond)
The Boolean type.
Definition std_types.h:36
framet & top()
Definition call_stack.h:17
bool empty() const
Definition dstring.h:89
Base class for all expressions.
Definition expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
The Boolean constant false.
Definition std_expr.h:3200
bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
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:24
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?
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.
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()
std::stack< bool > record_events
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...
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.
renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
std::vector< threadt > threads
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.
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
Definition goto_symex.h:41
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:242
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.
symex_target_equationt & target
The equation that this execution is building up.
Definition goto_symex.h:267
guard_managert & guard_manager
Used to create guards.
Definition goto_symex.h:264
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:259
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, const value_sett &value_set)
messaget log
The messaget to write log messages to.
Definition goto_symex.h:279
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition goto_symex.h:186
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:168
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:2502
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
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
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
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().
Wrapper for expressions or types which have been renamed up to a given level.
Definition renamed.h:33
void simplify(simplify_exprt &simplifier)
Definition renamed.h:45
const underlyingt & get() const
Definition renamed.h:40
bool empty() const
Check if map is empty.
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.
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:193
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:145
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
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 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:3191
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition expr_util.cpp:98
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...
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)
Storage of symbolic execution paths to resume.
Pointer Logic.
@ L1
Definition renamed.h:24
bool simplify(exprt &expr, 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 not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2484
Information saved at a conditional goto to resume execution.
goto_symex_statet state
symex_renaming_levelt current_names
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 std::size_t goto_count, const std::size_t dest_count)
Helper function for phi_function which merges the names of an identifier for two different states.
static guardt merge_state_guards(goto_statet &goto_state, goto_symex_statet &state)
dstringt irep_idt