CBMC
Loading...
Searching...
No Matches
symex_main.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_iterator.h>
14#include <util/expr_util.h>
15#include <util/format.h>
16#include <util/format_expr.h>
17#include <util/invariant.h>
18#include <util/magic.h>
20#include <util/replace_symbol.h>
21#include <util/std_expr.h>
22
24
25#include "goto_symex.h"
26#include "path_storage.h"
27
28#include <memory>
29
31 : max_depth(options.get_unsigned_int_option("depth")),
32 doing_path_exploration(options.is_set("paths")),
33 allow_pointer_unsoundness(
34 options.get_bool_option("allow-pointer-unsoundness")),
35 constant_propagation(options.get_bool_option("propagation")),
36 self_loops_to_assumptions(
37 options.get_bool_option("self-loops-to-assumptions")),
38 simplify_opt(options.get_bool_option("simplify")),
39 unwinding_assertions(options.get_bool_option("unwinding-assertions")),
40 partial_loops(options.get_bool_option("partial-loops")),
41 run_validation_checks(options.get_bool_option("validate-ssa-equation")),
42 show_symex_steps(options.get_bool_option("show-goto-symex-steps")),
43 show_points_to_sets(options.get_bool_option("show-points-to-sets")),
44 max_field_sensitivity_array_size(
45 options.is_set("no-array-field-sensitivity")
46 ? 0
47 : options.is_set("max-field-sensitivity-array-size")
48 ? options.get_unsigned_int_option(
49 "max-field-sensitivity-array-size")
51 complexity_limits_active(
52 options.get_signed_int_option("symex-complexity-limit") > 0),
53 cache_dereferences{options.get_bool_option("symex-cache-dereferences")}
54{
55}
56
60static void pop_exited_loops(
62 std::vector<framet::active_loop_infot> &active_loops)
63{
64 while(!active_loops.empty())
65 {
66 if(!active_loops.back().loop.contains(to))
67 active_loops.pop_back();
68 else
69 break;
70 }
71}
72
76 bool is_backwards_goto)
77{
78 if(!state.call_stack().empty())
79 {
80 // initialize the loop counter of any loop we are newly entering
81 // upon this transition; we are entering a loop if
82 // 1. the transition from state.source.pc to "to" is not a backwards goto
83 // or
84 // 2. we are arriving from an outer loop
85
86 // TODO: This should all be replaced by natural loop analysis.
87 // This is because the way we detect loops is pretty imprecise.
88
89 framet &frame = state.call_stack().top();
90 const goto_programt::instructiont &instruction=*to;
91 for(const auto &i_e : instruction.incoming_edges)
92 {
93 if(
94 i_e->is_backwards_goto() && i_e->get_target() == to &&
95 (!is_backwards_goto ||
96 state.source.pc->location_number > i_e->location_number))
97 {
98 const auto loop_id =
100 auto &current_loop_info = frame.loop_iterations[loop_id];
101 current_loop_info.count = 0;
102
103 // We've found a loop, put it on the stack and say it's our current
104 // active loop.
105 if(
106 frame.loops_info && frame.loops_info->loop_map.find(to) !=
107 frame.loops_info->loop_map.end())
108 {
109 frame.active_loops.emplace_back(frame.loops_info->loop_map[to]);
110 }
111 }
112 }
113
114 // Only do this if we have active loop analysis going.
115 if(!frame.active_loops.empty())
116 {
117 // Otherwise if we find we're transitioning out of a loop, make sure
118 // to remove any loops we're not currently iterating over.
119
120 // Match the do-while pattern.
121 if(
122 state.source.pc->is_backwards_goto() &&
123 state.source.pc->location_number < to->location_number)
124 {
126 }
127
128 // Match for-each or while.
129 for(const auto &incoming_edge : state.source.pc->incoming_edges)
130 {
131 if(
132 incoming_edge->is_backwards_goto() &&
133 incoming_edge->location_number < to->location_number)
134 {
136 }
137 }
138 }
139 }
140
141 state.source.pc=to;
142}
143
145{
147 ++next;
148 symex_transition(state, next, false);
149}
150
152 const goto_programt::instructiont &instruction,
153 statet &state)
154{
155 exprt condition = clean_expr(instruction.condition(), state, false);
156
157 // First, push negations in and perhaps convert existential quantifiers into
158 // universals:
159 if(has_subexpr(condition, ID_exists) || has_subexpr(condition, ID_forall))
160 do_simplify(condition, state.value_set);
161
162 // Second, L2-rename universal quantifiers:
163 if(has_subexpr(condition, ID_forall))
164 rewrite_quantifiers(condition, state);
165
166 // now rename, enables propagation
167 exprt l2_condition = state.rename(std::move(condition), ns).get();
168
169 // now try simplifier on it
171
172 std::string msg = id2string(instruction.source_location().get_comment());
173 if(msg.empty())
174 msg = "assertion";
175
176 vcc(
177 l2_condition, instruction.source_location().get_property_id(), msg, state);
178}
179
181 const exprt &condition,
182 const irep_idt &property_id,
183 const std::string &msg,
184 statet &state)
185{
186 state.total_vccs++;
188
189 if(condition.is_true())
190 return;
191
192 const exprt guarded_condition = state.guard.guard_expr(condition);
193
194 state.remaining_vccs++;
196 state.guard.as_expr(), guarded_condition, property_id, msg, state.source);
197}
198
199void goto_symext::symex_assume(statet &state, const exprt &cond)
200{
201 exprt simplified_cond = clean_expr(cond, state, false);
202 simplified_cond = state.rename(std::move(simplified_cond), ns).get();
204
205 // It would be better to call try_filter_value_sets after apply_condition,
206 // but it is not currently possible. See the comment at the beginning of
207 // \ref apply_goto_condition for more information.
208
210 state, cond, state.value_set, &state.value_set, nullptr, ns);
211
212 // apply_condition must come after rename because it might change the
213 // constant propagator and the value-set and we read from those in rename
214 state.apply_condition(simplified_cond, state, ns);
215
217}
218
220{
221 if(cond.is_true())
222 return;
223
224 if(cond.is_false())
225 state.reachable = false;
226
227 // we are willing to re-write some quantified expressions
228 exprt rewritten_cond = cond;
231
232 if(state.threads.size()==1)
233 {
235 target.assumption(state.guard.as_expr(), tmp, state.source);
236 }
237 // symex_target_equationt::convert_assertions would fail to
238 // consider assumptions of threads that have a thread-id above that
239 // of the thread containing the assertion:
240 // T0 T1
241 // x=0; assume(x==1);
242 // assert(x!=42); x=42;
243 else
244 state.guard.add(rewritten_cond);
245
246 if(state.atomic_section_id!=0 &&
247 state.guard.is_false())
248 symex_atomic_end(state);
249}
250
252{
253 const bool is_assert = state.source.pc->is_assert();
254
255 if(
256 (is_assert && expr.id() == ID_forall) ||
257 (!is_assert && expr.id() == ID_exists))
258 {
259 // for assertions e can rewrite "forall X. P" to "P", and
260 // for assumptions we can rewrite "exists X. P" to "P"
261 // we keep the quantified variable unique by means of L2 renaming
262 auto &quant_expr = to_quantifier_expr(expr);
264 to_symbol_expr(to_ssa_expr(quant_expr.symbol()).get_original_expr());
265 symex_decl(state, tmp0);
267 exprt tmp = quant_expr.where();
268 rewrite_quantifiers(tmp, state);
269 quant_expr.swap(tmp);
270 }
271 else if(expr.id() == ID_or || expr.id() == ID_and)
272 {
273 for(auto &op : expr.operands())
274 rewrite_quantifiers(op, state);
275 }
276}
277
278static void
280{
281 PRECONDITION(state.source.thread_nr < state.threads.size());
282 PRECONDITION(thread_nb < state.threads.size());
283
284 // save PC
285 state.threads[state.source.thread_nr].pc = state.source.pc;
286 state.threads[state.source.thread_nr].atomic_section_id =
287 state.atomic_section_id;
288
289 // get new PC
290 state.source.thread_nr = thread_nb;
291 state.source.pc = state.threads[thread_nb].pc;
292 state.source.function_id = state.threads[thread_nb].function_id;
293
294 state.guard = state.threads[thread_nb].guard;
295 // A thread's initial state is certainly reachable:
296 state.reachable = true;
297}
298
300 statet &state, const get_goto_functiont &get_goto_function)
301{
303
304 _total_vccs = state.total_vccs;
306
308 return;
309
310 // is there another thread to execute?
311 if(state.call_stack().empty() &&
312 state.source.thread_nr+1<state.threads.size())
313 {
314 unsigned t=state.source.thread_nr+1;
315#if 0
316 std::cout << "********* Now executing thread " << t << '\n';
317#endif
318 switch_to_thread(state, t);
319 symex_transition(state, state.source.pc, false);
320 }
321}
322
324 statet &state,
325 const get_goto_functiont &get_goto_function)
326{
327 // resets the namespace to only wrap a single symbol table, and does so upon
328 // destruction of an object of this type; instantiating the type is thus all
329 // that's needed to achieve a reset upon exiting this method
330 struct reset_namespacet
331 {
332 explicit reset_namespacet(namespacet &ns) : ns(ns)
333 {
334 }
335
337 {
338 // Get symbol table 1, the outer symbol table from the GOTO program
339 const symbol_table_baset &st = ns.get_symbol_table();
340 // Move a new namespace containing this symbol table over the top of the
341 // current one
342 ns = namespacet(st);
343 }
344
345 namespacet &ns;
346 };
347
348 // We'll be using ns during symbolic execution and it needs to know
349 // about the names minted in `state`, so make it point both to
350 // `state`'s symbol table and the symbol table of the original
351 // goto-program.
353
354 // whichever way we exit this method, reset the namespace back to a sane state
355 // as state.symbol_table might go out of scope
357
358 PRECONDITION(state.call_stack().top().end_of_function->is_end_function());
359
362 return state.symbol_table;
363
364 while(!state.call_stack().empty())
365 {
366 state.has_saved_jump_target = false;
367 state.has_saved_next_instruction = false;
370 return state.symbol_table;
371 }
372
373 // Clients may need to construct a namespace with both the names in
374 // the original goto-program and the names generated during symbolic
375 // execution, so return the names generated through symbolic execution
376 return state.symbol_table;
377}
378
380 const get_goto_functiont &get_goto_function,
381 const statet &saved_state,
383{
384 // saved_state contains a pointer to a symex_target_equationt that is
385 // almost certainly stale. This is because equations are owned by bmcts,
386 // and we construct a new bmct for every path that we execute. We're on a
387 // new path now, so the old bmct and the equation that it owned have now
388 // been deallocated. So, construct a new state from the old one, and make
389 // its equation member point to the (valid) equation passed as an argument.
391
392 // Do NOT do the same initialization that `symex_with_state` does for a
393 // fresh state, as that would clobber the saved state's program counter
394 return symex_with_state(state, get_goto_function);
395}
396
397std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
398 const get_goto_functiont &get_goto_function)
399{
401
402 const goto_functionst::goto_functiont *start_function;
403 try
404 {
405 start_function = &get_goto_function(entry_point_id);
406 }
407 catch(const std::out_of_range &)
408 {
409 throw unsupported_operation_exceptiont("the program has no entry point");
410 }
411
412 // Get our path_storage pointer because this state will live beyond
413 // this instance of goto_symext, so we can't take the reference directly.
414 auto *storage = &path_storage;
415
416 // create and prepare the state
417 auto state = std::make_unique<statet>(
418 symex_targett::sourcet(entry_point_id, start_function->body),
419 symex_config.max_field_sensitivity_array_size,
420 symex_config.simplify_opt,
423 [storage](const irep_idt &id) { return storage->get_unique_l2_index(id); });
424
425 CHECK_RETURN(!state->threads.empty());
426 CHECK_RETURN(!state->call_stack().empty());
427
429 std::prev(start_function->body.instructions.end());
430 state->call_stack().top().end_of_function = limit;
431 state->call_stack().top().calling_location.pc =
432 state->call_stack().top().end_of_function;
433 state->call_stack().top().hidden_function = start_function->is_hidden();
434
435 state->symex_target = &target;
436
437 state->run_validation_checks = symex_config.run_validation_checks;
438
439 // initialize support analyses
443 emplace_safe_pointers_result.first->second(start_function->body);
444
446 entry_point_id, *start_function);
447 state->dirty = &path_storage.dirty;
448
449 // Only enable loop analysis when complexity is enabled.
450 if(symex_config.complexity_limits_active)
451 {
452 // Set initial loop analysis.
453 path_storage.add_function_loops(entry_point_id, start_function->body);
454 state->call_stack().top().loops_info =
456 }
457
458 // make the first step onto the instruction pointed to by the initial program
459 // counter
460 symex_transition(*state, state->source.pc, false);
461
462 return state;
463}
464
466 const get_goto_functiont &get_goto_function,
468{
470 // Initialize declared shadow memory fields
471 state->shadow_memory.fields = fields;
472
473 return symex_with_state(*state, get_goto_function);
474}
475
477 const get_goto_functiont &get_goto_function,
478 symbol_table_baset &new_symbol_table,
480{
482 // Initialize declared shadow memory fields
483 state->shadow_memory.fields = fields;
484
486 entry_point_start.state.saved_target = state->source.pc;
487 entry_point_start.state.has_saved_next_instruction = true;
488
490}
491
494{
495 return [&goto_model](
496 const irep_idt &id) -> const goto_functionst::goto_functiont & {
497 return goto_model.get_goto_function(id);
498 };
499}
500
503{
504 log.status() << source.function_id
505 << " location number: " << source.pc->location_number;
506
507 return log.status();
508}
509
511{
512 // If we're showing the route, begin outputting debug info, and don't print
513 // instructions we don't run.
514
515 // We also skip dead instructions as they don't add much to step-based
516 // debugging and if there's no code block at this point.
517 if(
518 !symex_config.show_symex_steps || !state.reachable ||
519 state.source.pc->type() == DEAD ||
520 (state.source.pc->code().is_nil() &&
521 state.source.pc->type() != END_FUNCTION))
522 {
523 return;
524 }
525
526 if(state.source.pc->code().is_not_nil())
527 {
528 auto guard_expression = state.guard.as_expr();
529 std::size_t size = 0;
530 for(auto it = guard_expression.depth_begin();
531 it != guard_expression.depth_end();
532 ++it)
533 {
534 size++;
535 }
536
537 log.status() << "[Guard size: " << size << "] "
538 << format(state.source.pc->code());
539
540 if(
541 state.source.pc->source_location().is_not_nil() &&
542 !state.source.pc->source_location().get_java_bytecode_index().empty())
543 {
544 log.status()
545 << " bytecode index: "
546 << state.source.pc->source_location().get_java_bytecode_index();
547 }
548
550 }
551
552 // Print the method we're returning too.
553 const auto &call_stack = state.threads[state.source.thread_nr].call_stack;
554 if(state.source.pc->type() == END_FUNCTION)
555 {
557
558 if(!call_stack.empty())
559 {
560 log.status() << "Returning to: ";
561 print_callstack_entry(call_stack.back().calling_location)
562 << messaget::eom;
563 }
564
566 }
567
568 // On a function call print the entire call stack.
569 if(state.source.pc->type() == FUNCTION_CALL)
570 {
572
573 if(!call_stack.empty())
574 {
575 log.status() << "Call stack:" << messaget::eom;
576
577 for(auto &frame : call_stack)
578 {
579 print_callstack_entry(frame.calling_location) << messaget::eom;
580 }
581
583
584 // Add the method we're about to enter with no location number.
585 log.status() << format(state.source.pc->call_function()) << messaget::eom
586 << messaget::eom;
587 }
588 }
589}
590
593 const get_goto_functiont &get_goto_function,
594 statet &state)
595{
596 // Print debug statements if they've been enabled.
597 print_symex_step(state);
600}
601
603 const get_goto_functiont &get_goto_function,
604 statet &state)
605{
606 PRECONDITION(!state.threads.empty());
607 PRECONDITION(!state.call_stack().empty());
608
609 const goto_programt::instructiont &instruction=*state.source.pc;
610
611 if(!symex_config.doing_path_exploration)
612 merge_gotos(state);
613
614 // depth exceeded?
615 if(state.depth > symex_config.max_depth)
616 {
617 // Rule out this path:
619 }
620 state.depth++;
621
622 // actually do instruction
623 switch(instruction.type())
624 {
625 case SKIP:
626 if(state.reachable)
627 target.location(state.guard.as_expr(), state.source);
628 symex_transition(state);
629 break;
630
631 case END_FUNCTION:
632 // do even if !state.reachable to clear out frame created
633 // in symex_start_thread
635 symex_transition(state);
636 break;
637
638 case LOCATION:
639 if(state.reachable)
640 target.location(state.guard.as_expr(), state.source);
641 symex_transition(state);
642 break;
643
644 case GOTO:
645 if(state.reachable)
646 symex_goto(state);
647 else
649 break;
650
651 case ASSUME:
652 if(state.reachable)
653 symex_assume(state, instruction.condition());
654 symex_transition(state);
655 break;
656
657 case ASSERT:
658 if(state.reachable && !ignore_assertions)
659 symex_assert(instruction, state);
660 symex_transition(state);
661 break;
662
663 case SET_RETURN_VALUE:
664 if(state.reachable)
665 symex_set_return_value(state, instruction.return_value());
666 symex_transition(state);
667 break;
668
669 case ASSIGN:
670 if(state.reachable)
671 symex_assign(state, instruction.assign_lhs(), instruction.assign_rhs());
672
673 symex_transition(state);
674 break;
675
676 case FUNCTION_CALL:
677 if(state.reachable)
678 symex_function_call(get_goto_function, state, instruction);
679 else
680 symex_transition(state);
681 break;
682
683 case OTHER:
684 if(state.reachable)
685 symex_other(state);
686 symex_transition(state);
687 break;
688
689 case DECL:
690 if(state.reachable)
691 symex_decl(state);
692 symex_transition(state);
693 break;
694
695 case DEAD:
696 symex_dead(state);
697 symex_transition(state);
698 break;
699
700 case START_THREAD:
701 symex_start_thread(state);
702 symex_transition(state);
703 break;
704
705 case END_THREAD:
706 // behaves like assume(0);
707 if(state.reachable)
708 state.reachable = false;
709 symex_transition(state);
710 break;
711
712 case ATOMIC_BEGIN:
713 symex_atomic_begin(state);
714 symex_transition(state);
715 break;
716
717 case ATOMIC_END:
718 symex_atomic_end(state);
719 symex_transition(state);
720 break;
721
722 case CATCH:
723 symex_catch(state);
724 symex_transition(state);
725 break;
726
727 case THROW:
728 symex_throw(state);
729 symex_transition(state);
730 break;
731
733 throw unsupported_operation_exceptiont("symex got NO_INSTRUCTION");
734
735 case INCOMPLETE_GOTO:
736 DATA_INVARIANT(false, "symex got unexpected instruction type");
737 }
738
743}
744
746{
747 for(const auto &symbol_expr : instruction_local_symbols)
748 symex_dead(state, symbol_expr);
750}
751
757static std::optional<symbol_exprt>
759{
760 std::optional<symbol_exprt> return_value;
761 for(auto it = expr.depth_cbegin(); it != expr.depth_cend(); ++it)
762 {
763 const symbol_exprt *symbol_expr = expr_try_dynamic_cast<symbol_exprt>(*it);
764 if(symbol_expr && can_cast_type<pointer_typet>(symbol_expr->type()))
765 {
766 // If we already have a potential return value, check if it is the same
767 // symbol, and return an empty std::optional if not
768 if(return_value && *symbol_expr != *return_value)
769 {
770 return {};
771 }
772 return_value = *symbol_expr;
773 }
774 }
775
776 // Either expr contains no pointer-typed symbols or it contains one unique
777 // pointer-typed symbol, possibly repeated multiple times
778 return return_value;
779}
780
782 goto_symex_statet &state,
783 exprt condition,
787 const namespacet &ns)
788{
789 condition = state.rename<L1>(std::move(condition), ns).get();
790
791 std::optional<symbol_exprt> symbol_expr =
793
794 if(!symbol_expr)
795 {
796 return;
797 }
798
799 const pointer_typet &symbol_type = to_pointer_type(symbol_expr->type());
800
801 const std::vector<exprt> value_set_elements =
802 original_value_set.get_value_set(*symbol_expr, ns);
803
804 std::unordered_set<exprt, irep_hash> erase_from_jump_taken_value_set;
805 std::unordered_set<exprt, irep_hash> erase_from_jump_not_taken_value_set;
808
809 // Try evaluating the condition with the symbol replaced by a pointer to each
810 // one of its possible values in turn. If that leads to a true for some
811 // value_set_element then we can delete it from the value set that will be
812 // used if the condition is false, and vice versa.
814 {
815 if(
818 {
819 continue;
820 }
821
822 const bool exclude_null_derefs = false;
824 value_set_element, exclude_null_derefs, language_mode))
825 {
826 continue;
827 }
828
831 value_set_element, *symbol_expr, ns);
832
833 if(value.pointer.is_nil())
834 continue;
835
836 exprt modified_condition(condition);
837
838 address_of_aware_replace_symbolt replace_symbol{};
839 replace_symbol.insert(*symbol_expr, value.pointer);
840 replace_symbol(modified_condition);
841
842 // This do_simplify() is needed for the following reason: if `condition` is
843 // `*p == a` and we replace `p` with `&a` then we get `*&a == a`. Suppose
844 // our constant propagation knows that `a` is `1`. Without this call to
845 // do_simplify(), state.rename() turns this into `*&a == 1` (because
846 // rename() doesn't do constant propagation inside addresses), which
847 // do_simplify() turns into `a == 1`, which cannot be evaluated as true
848 // without another round of constant propagation.
849 // It would be sufficient to replace this call to do_simplify() with
850 // something that just replaces `*&x` with `x` whenever it finds it.
852
853 state.record_events.push(false);
854 modified_condition = state.rename(std::move(modified_condition), ns).get();
855 state.record_events.pop();
856
858
860 {
862 }
863 else if(jump_not_taken_value_set && modified_condition.is_true())
864 {
866 }
867 }
869 {
870 auto entry_index = jump_taken_value_set->get_index_of_symbol(
871 symbol_expr->get_identifier(), symbol_type, "", ns);
872 jump_taken_value_set->erase_values_from_entry(
874 }
876 {
877 auto entry_index = jump_not_taken_value_set->get_index_of_symbol(
878 symbol_expr->get_identifier(), symbol_type, "", ns);
879 jump_not_taken_value_set->erase_values_from_entry(
881 }
882}
Abstract interface to eager or lazy GOTO models.
virtual const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id)=0
Get a GOTO function by name, or throw if no such function exists.
Replace symbols with constants while maintaining syntactically valid expressions.
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
framet & top()
Definition call_stack.h:17
complexity_violationt check_complexity(goto_symex_statet &state)
Checks the passed-in state to see if its become too complex for us to deal with, and if so set its gu...
void run_transformations(complexity_violationt complexity_violation, goto_symex_statet &current_state)
Runs a suite of transformations on the state and symex executable, performing whatever transformation...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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
const_depth_iteratort depth_cend() const
Definition expr.cpp:257
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
typet & type()
Return the type of the expression.
Definition expr.h:84
const_depth_iteratort depth_cbegin() const
Definition expr.cpp:255
operandst & operands()
Definition expr.h:94
The Boolean constant false.
Definition std_expr.h:3200
Stack frames – these are used for function calls and for exceptions.
std::vector< active_loop_infot > active_loops
Definition frame.h:75
std::unordered_map< irep_idt, loop_infot > loop_iterations
Definition frame.h:77
goto_programt::const_targett end_of_function
Definition frame.h:37
std::shared_ptr< lexical_loopst > loops_info
Definition frame.h:74
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
This class represents an instruction in the GOTO intermediate representation.
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
std::set< targett, target_less_than > incoming_edges
const exprt & condition() const
Get the condition of gotos, assume, assert.
const source_locationt & source_location() const
goto_program_instruction_typet type() const
What kind of instruction?
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
instructionst::const_iterator const_targett
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.
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.
call_stackt & call_stack()
std::stack< bool > record_events
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...
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
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.
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...
virtual symbol_tablet symex_with_state(statet &state, const get_goto_functiont &get_goto_functions)
Symbolically execute the entire program starting from entry point.
void rewrite_quantifiers(exprt &, statet &)
virtual void symex_assume(statet &state, const exprt &cond)
Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption.
void symex_threaded_step(statet &state, const get_goto_functiont &get_goto_function)
Invokes symex_step and verifies whether additional threads can be executed.
void symex_unreachable_goto(statet &state)
Symbolically execute a GOTO instruction in the context of unreachable code.
complexity_limitert complexity_module
Definition goto_symex.h:837
virtual void symex_atomic_begin(statet &state)
Symbolically execute an ATOMIC_BEGIN instruction.
const symbol_table_baset & outer_symbol_table
The symbol table associated with the goto-program being executed.
Definition goto_symex.h:250
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
void symex_set_return_value(statet &state, const exprt &return_value)
Symbolically execute a SET_RETURN_VALUE instruction.
bool ignore_assertions
If this flag is set to true then assertions will be temporarily ignored by the symbolic executions.
Definition goto_symex.h:172
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
virtual void symex_step(const get_goto_functiont &get_goto_function, statet &state)
Called for each step in the symbolic execution This calls print_symex_step to print symex's current i...
virtual void symex_goto(statet &state)
Symbolically execute a GOTO instruction.
virtual void symex_decl(statet &state)
Symbolically execute a DECL instruction.
void symex_catch(statet &state)
Symbolically execute a CATCH instruction.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition goto_symex.h:811
std::unique_ptr< statet > initialize_entry_point_state(const get_goto_functiont &get_goto_function)
Initialize the symbolic execution and the given state with the beginning of the entry point function.
unsigned _total_vccs
Definition goto_symex.h:834
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
virtual symbol_tablet resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation)
Performs symbolic execution using a state and equation that have already been used to symbolically ex...
void symex_assert(const goto_programt::instructiont &, statet &)
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
virtual void symex_dead(statet &state)
Symbolically execute a DEAD instruction.
std::size_t path_segment_vccs
Number of VCCs generated during the run of this goto_symext object.
Definition goto_symex.h:823
virtual void symex_start_thread(statet &state)
Symbolically execute a START_THREAD instruction.
virtual symbol_tablet symex_from_entry_point_of(const get_goto_functiont &get_goto_function, const shadow_memory_field_definitionst &fields)
Symbolically execute the entire program starting from entry point.
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).
void kill_instruction_local_symbols(statet &state)
Kills any variables in instruction_local_symbols (these are currently always let-bound variables defi...
virtual void symex_end_of_function(statet &)
Symbolically execute a END_FUNCTION instruction.
virtual void do_simplify(exprt &expr, const value_sett &value_set)
void symex_assign(statet &state, const exprt &lhs, const exprt &rhs)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
void print_symex_step(statet &state)
Prints the route of symex as it walks through the code.
void symex_throw(statet &state)
Symbolically execute a THROW instruction.
unsigned _remaining_vccs
Definition goto_symex.h:834
virtual void symex_other(statet &state)
Symbolically execute an OTHER instruction.
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
Definition goto_symex.h:94
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.
messaget::mstreamt & print_callstack_entry(const symex_targett::sourcet &target)
std::vector< symbol_exprt > instruction_local_symbols
Variables that should be killed at the end of the current symex_step invocation.
Definition goto_symex.h:276
virtual void symex_atomic_end(statet &state)
Symbolically execute an ATOMIC_END instruction.
virtual void symex_function_call(const get_goto_functiont &get_goto_function, statet &state, const goto_programt::instructiont &instruction)
Symbolically execute a FUNCTION_CALL instruction.
void execute_next_instruction(const get_goto_functiont &get_goto_function, statet &state)
Executes the instruction state.source.pc Case-switches over the type of the instruction being execute...
virtual void initialize_path_storage_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_table_baset &new_symbol_table, const shadow_memory_field_definitionst &fields)
Puts the initial state of the entry point function into the path storage.
void add(const exprt &expr)
exprt as_expr() const
Definition guard_expr.h:46
bool is_false() const
Definition guard_expr.h:65
exprt guard_expr(exprt expr) const
Return guard => dest or a simplified variant thereof if either guard or dest are trivial.
void populate_dirty_for_function(const irep_idt &id, const goto_functionst::goto_functiont &function)
Analyse the given function with dirtyt if it hasn't been seen before.
Definition dirty.cpp:112
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition namespace.h:123
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
std::shared_ptr< lexical_loopst > get_loop_analysis(const irep_idt &function_id)
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Map function identifiers to local_safe_pointerst instances.
virtual void push(const patht &)=0
Add a path to resume to the storage.
void add_function_loops(const irep_idt &identifier, const goto_programt &body)
Generates a loop analysis for the instructions in goto_programt and keys it against function ID.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
The shadow memory field definitions.
Expression to hold a symbol (variable)
Definition std_expr.h:131
The symbol table base class interface.
The symbol table.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void assertion(const exprt &guard, const exprt &cond, const irep_idt &property_id, const std::string &msg, const sourcet &source)
Record an assertion.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
Thrown when we encounter an instruction, parameters to an instruction etc.
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
complexity_violationt
What sort of symex-complexity violation has taken place.
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition format.h:37
@ FUNCTION_CALL
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
Symbolic Execution.
void symex_transition(goto_symext::statet &state)
Transition to the next instruction, which increments the internal program counter and initializes the...
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
Magic numbers used throughout the codebase.
constexpr std::size_t DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE
Limit the size of arrays for which field_sensitivity gets applied.
Definition magic.h:21
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Storage of symbolic execution paths to resume.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
@ L1
Definition renamed.h:24
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#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
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 symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
Information saved at a conditional goto to resume execution.
symex_configt(const optionst &options)
Construct a symex_configt using options specified in an optionst.
Identifies source in the context of symbolic execution.
goto_programt::const_targett pc
void symex_transition(goto_symext::statet &state, goto_programt::const_targett to, bool is_backwards_goto)
static std::optional< symbol_exprt > find_unique_pointer_typed_symbol(const exprt &expr)
Check if an expression only contains one unique symbol (possibly repeated multiple times)
static void switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
static void pop_exited_loops(const goto_programt::const_targett &to, std::vector< framet::active_loop_infot > &active_loops)
If 'to' is not an instruction in our currently top-most active loop, pop and re-check until we find a...
Pointer Dereferencing.