cprover
Loading...
Searching...
No Matches
goto_symex.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
13#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
14
15#include <util/message.h>
16
17#include "complexity_limiter.h"
18#include "shadow_memory.h"
19#include "symex_config.h"
21
25class path_storaget;
28class symex_assignt;
29class typet;
30
37{
38public:
41
55 const optionst &options,
56 path_storaget &path_storage,
58 : should_pause_symex(false),
59 symex_config(options),
63 target(_target),
65 log(mh),
66 path_storage(path_storage),
68 _total_vccs(std::numeric_limits<unsigned>::max()),
69 _remaining_vccs(std::numeric_limits<unsigned>::max()),
70 complexity_module(mh, options),
72 std::bind(
74 this,
75 std::placeholders::_1,
76 std::placeholders::_2,
77 std::placeholders::_3),
78 ns,
79 mh)
80 {
81 }
82
84 virtual ~goto_symext() = default;
85
91 typedef
92 std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
94
103
119
128 symbol_table_baset &new_symbol_table,
130
144 const statet &saved_state,
145 symex_target_equationt *saved_equation);
146
160 virtual symbol_tablet
161 symex_with_state(statet &state, const get_goto_functiont &get_goto_functions);
162
171
174 bool ignore_assertions = false;
175
184 virtual bool check_break(const irep_idt &loop_id, unsigned unwind);
185
186protected:
189
194 std::unique_ptr<statet>
196
203 statet &state,
205
213 virtual void
215
226 statet &state);
227
232
235 void print_symex_step(statet &state);
236
239
240public:
241
245
246protected:
253
262
267
270
274
278 std::vector<symbol_exprt> instruction_local_symbols;
279
281 mutable messaget log;
282
284
294 exprt clean_expr(exprt expr, statet &state, bool write);
295
296 void trigger_auto_object(const exprt &, statet &);
297 void initialize_auto_object(const exprt &, statet &);
298
305 virtual void dereference(exprt &, statet &, bool write);
306
307 symbol_exprt cache_dereference(exprt &dereference_result, statet &state);
309 exprt &expr,
310 statet &state,
311 bool write,
312 bool is_in_quantifier);
314 const exprt &,
315 statet &,
316 bool keep_array);
317
320 virtual void symex_goto(statet &state);
323 void symex_unreachable_goto(statet &state);
327 void symex_set_return_value(statet &state, const exprt &return_value);
330 virtual void symex_start_thread(statet &state);
333 virtual void symex_atomic_begin(statet &state);
336 virtual void symex_atomic_end(statet &state);
339 virtual void symex_decl(statet &state);
344 virtual void symex_decl(statet &state, const symbol_exprt &expr);
347 virtual void symex_dead(statet &state);
351 void symex_dead(statet &state, const symbol_exprt &symbol_expr);
354 virtual void symex_other(statet &state);
355
357
368 goto_symex_statet &current_state,
369 goto_statet &jump_taken_state,
370 goto_statet &jump_not_taken_state,
371 const exprt &original_guard,
372 const exprt &new_guard,
373 const namespacet &ns);
374
391 goto_symex_statet &state,
392 exprt condition,
393 const value_sett &original_value_set,
394 value_sett *jump_taken_value_set,
395 value_sett *jump_not_taken_value_set,
396 const namespacet &ns);
397
403 virtual void vcc(
404 const exprt &cond,
405 const irep_idt &property_id,
406 const std::string &msg,
407 statet &state);
408
413 virtual void symex_assume(statet &state, const exprt &cond);
414 void symex_assume_l2(statet &, const exprt &cond);
415
420 void merge_gotos(statet &state);
421
428 virtual void merge_goto(
429 const symex_targett::sourcet &source,
430 goto_statet &&goto_state,
431 statet &state);
432
436 void phi_function(const goto_statet &goto_state, statet &dest_state);
437
443 virtual bool should_stop_unwind(
444 const symex_targett::sourcet &source,
445 const call_stackt &context,
446 unsigned unwind);
447
448 virtual void loop_bound_exceeded(statet &state, const exprt &guard);
449
452 virtual void no_body(const irep_idt &identifier)
453 {
454 }
455
463 virtual void symex_function_call(
465 statet &state,
466 const goto_programt::instructiont &instruction);
467
473 virtual void locality(
474 const irep_idt &function_identifier,
475 goto_symext::statet &state,
476 const goto_functionst::goto_functiont &goto_function);
477
480 virtual void symex_end_of_function(statet &);
481
489 virtual void symex_function_call_symbol(
491 statet &state,
492 const exprt &lhs,
493 const symbol_exprt &function,
494 const exprt::operandst &arguments);
495
510 statet &state,
511 const exprt &cleaned_lhs,
512 const symbol_exprt &function,
513 const exprt::operandst &cleaned_arguments);
514
515 virtual bool get_unwind_recursion(
516 const irep_idt &identifier,
517 unsigned thread_nr,
518 unsigned unwind);
519
527 const irep_idt &function_identifier,
528 const goto_functionst::goto_functiont &goto_function,
529 statet &state,
530 const exprt::operandst &arguments);
531
532 // exceptions
535 void symex_throw(statet &state);
538 void symex_catch(statet &state);
539
540 virtual void do_simplify(exprt &expr);
541
547 void symex_assign(statet &state, const exprt &lhs, const exprt &rhs);
548
558 statet &state,
560 const exprt &lhs,
561 const exprt &rhs);
562
570 statet &state,
572 const function_application_exprt &f_l1);
573
583 statet &state,
585 const function_application_exprt &f_l1);
586
596 statet &state,
598 const function_application_exprt &f_l1);
599
609 statet &state,
611 const function_application_exprt &f_l1);
612
622 statet &state,
624 const function_application_exprt &f_l1);
625
635 statet &state,
637 const function_application_exprt &f_l1);
638
653 statet &state,
655 const function_application_exprt &f_l1);
656
666 statet &state,
668 const function_application_exprt &f_l1);
669
672 statet &state,
674 const function_application_exprt &f_l1);
675
678 statet &state,
680 const function_application_exprt &f_l1,
681 bool to_upper);
682
685 statet &state,
687 const function_application_exprt &f_l1);
688
710 statet &state,
712 const ssa_exprt &length,
713 const constant_exprt &new_length,
714 const ssa_exprt &char_array,
715 const array_exprt &new_char_array);
716
726 statet &state,
728 const std::string &aux_symbol_name,
729 const ssa_exprt &char_array,
730 const array_exprt &new_char_array);
731
743 statet &state,
745 const array_exprt &new_char_array,
746 const address_of_exprt &string_data);
747
749 try_evaluate_constant_string(const statet &state, const exprt &content);
750
751 // clang-format off
754 const statet &state,
755 const exprt &expr);
756 // clang-format on
757
758 // havocs the given object
759 void havoc_rec(statet &state, const guardt &guard, const exprt &dest);
760
762
768 void lift_lets(statet &, exprt &);
769
774 void lift_let(statet &state, const let_exprt &let_expr);
775
776 virtual void
777 symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &);
778
784 virtual void symex_allocate(
785 statet &state,
786 const exprt &lhs,
787 const side_effect_exprt &code);
791 virtual void symex_cpp_delete(statet &state, const codet &code);
797 virtual void
798 symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code);
799
803 virtual void symex_printf(statet &state, const exprt &rhs);
807 virtual void symex_input(statet &state, const codet &code);
811 virtual void symex_output(statet &state, const codet &code);
812
813 void rewrite_quantifiers(exprt &, statet &);
814
819 path_storaget &path_storage;
820
821public:
831 std::size_t path_segment_vccs;
832
833protected:
841
844
846
849
850public:
851 unsigned get_total_vccs() const
852 {
853 INVARIANT(
854 _total_vccs != std::numeric_limits<unsigned>::max(),
855 "symex_threaded_step should have been executed at least once before "
856 "attempting to read total_vccs");
857 return _total_vccs;
858 }
859
860 unsigned get_remaining_vccs() const
861 {
862 INVARIANT(
863 _remaining_vccs != std::numeric_limits<unsigned>::max(),
864 "symex_threaded_step should have been executed at least once before "
865 "attempting to read remaining_vccs");
866 return _remaining_vccs;
867 }
868
869 void validate(const validation_modet vm) const
870 {
871 target.validate(ns, vm);
872 }
873};
874
882
886 bool is_backwards_goto);
887
899 renamedt<exprt, L2> condition,
900 const value_sett &value_set,
901 const irep_idt &language_mode,
902 const namespacet &ns);
903
904#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
static exprt guard(const exprt::operandst &guards, exprt cond)
Abstract interface to eager or lazy GOTO models.
Operator to return the address of an object.
Array constructor from list of elements.
Definition std_expr.h:1563
Data structure for representing an arbitrary statement in a program.
Symex complexity module.
A constant literal expression.
Definition std_expr.h:2942
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
Application of (mathematical) function.
::goto_functiont goto_functiont
This class represents an instruction in the GOTO intermediate representation.
instructionst::const_iterator const_targett
Container for data that varies per program point, e.g.
Definition goto_state.h:32
Central data structure: state.
The main class for the forward symbolic simulator.
Definition goto_symex.h:37
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...
virtual NODISCARD symbol_tablet symex_with_state(statet &state, const get_goto_functiont &get_goto_functions)
Symbolically execute the entire program starting from entry point.
virtual void symex_function_call_symbol(const get_goto_functiont &get_goto_function, statet &state, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments)
Symbolic execution of a call to a function call.
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 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.
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.
complexity_limitert complexity_module
Definition goto_symex.h:845
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
Definition goto_symex.h:40
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:252
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:244
void symex_set_return_value(statet &state, const exprt &return_value)
Symbolically execute a SET_RETURN_VALUE instruction.
virtual void no_body(const irep_idt &identifier)
Log a warning that a function has no body.
Definition goto_symex.h:452
bool ignore_assertions
If this flag is set to true then assertions will be temporarily ignored by the symbolic executions.
Definition goto_symex.h:174
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...
bool constant_propagate_delete_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate deleting a character from a string.
bool constant_propagate_set_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate setting the char at the given index.
bool constant_propagate_assignment_with_side_effects(statet &state, symex_assignt &symex_assign, const exprt &lhs, const exprt &rhs)
Attempt to constant propagate side effects of the assignment (if any)
virtual void symex_goto(statet &state)
Symbolically execute a GOTO instruction.
unsigned get_remaining_vccs() const
Definition goto_symex.h:860
virtual void symex_decl(statet &state)
Symbolically execute a DECL instruction.
void symex_catch(statet &state)
Symbolically execute a CATCH instruction.
bool constant_propagate_delete(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate deleting a substring from a string.
void phi_function(const goto_statet &goto_state, statet &dest_state)
Merge the SSA assignments from goto_state into dest_state.
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.
void havoc_rec(statet &state, const guardt &guard, const exprt &dest)
void constant_propagate_empty_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Create an empty string constant.
unsigned _total_vccs
Definition goto_symex.h:842
symex_target_equationt & target
The equation that this execution is building up.
Definition goto_symex.h:269
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
bool constant_propagate_case_change(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1, bool to_upper)
Attempt to constant propagate case changes, both upper and lower.
bool constant_propagate_integer_to_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate converting an integer to a string.
guard_managert & guard_manager
Used to create guards.
Definition goto_symex.h:266
goto_symext(message_handlert &mh, const symbol_table_baset &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager)
Construct a goto_symext to execute a particular program.
Definition goto_symex.h:51
unsigned atomic_section_counter
A monotonically increasing index for each encountered ATOMIC_BEGIN instruction.
Definition goto_symex.h:273
virtual NODISCARD 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 &)
unsigned get_total_vccs() const
Definition goto_symex.h:851
virtual void loop_bound_exceeded(statet &state, const exprt &guard)
bool constant_propagate_trim(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate trim operations.
virtual void symex_dead(statet &state)
Symbolically execute a DEAD instruction.
shadow_memoryt shadow_memory
Shadow memory instrumentation API.
Definition goto_symex.h:848
static optionalt< std::reference_wrapper< const constant_exprt > > try_evaluate_constant(const statet &state, const exprt &expr)
std::size_t path_segment_vccs
Execute any let expressions in expr using symex_assignt::assign_symbol.
Definition goto_symex.h:831
virtual void symex_start_thread(statet &state)
Symbolically execute a START_THREAD instruction.
void initialize_auto_object(const exprt &, statet &)
virtual NODISCARD 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.
void parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)
Iterates over arguments and assigns them to the parameters, which are symbols whose name and type are...
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition goto_symex.h:261
void trigger_auto_object(const exprt &, statet &)
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 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 symex_end_of_function(statet &)
Symbolically execute a END_FUNCTION instruction.
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
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.
exprt make_auto_object(const typet &, statet &)
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.
exprt address_arithmetic(const exprt &, statet &, bool keep_array)
const symbolt & get_new_string_data_symbol(statet &state, symex_assignt &symex_assign, const std::string &aux_symbol_name, const ssa_exprt &char_array, const array_exprt &new_char_array)
Installs a new symbol in the symbol table to represent the given character array, and assigns the cha...
void associate_array_to_pointer(statet &state, symex_assignt &symex_assign, const array_exprt &new_char_array, const address_of_exprt &string_data)
Generate array to pointer association primitive.
virtual void do_simplify(exprt &expr)
unsigned _remaining_vccs
Definition goto_symex.h:842
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:93
virtual void symex_function_call_post_clean(const get_goto_functiont &get_goto_function, statet &state, const exprt &cleaned_lhs, const symbol_exprt &function, const exprt::operandst &cleaned_arguments)
Symbolic execution of a function call by inlining.
bool constant_propagate_set_length(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate setting the length of a string.
virtual void dereference(exprt &, statet &, bool write)
Replace all dereference operations within expr with explicit references to the objects they may refer...
symbol_exprt cache_dereference(exprt &dereference_result, statet &state)
messaget log
The messaget to write log messages to.
Definition goto_symex.h:281
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition goto_symex.h:188
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:170
bool constant_propagate_string_substring(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate getting a substring of a string.
void symex_assume_l2(statet &, const exprt &cond)
void merge_gotos(statet &state)
Merge all branches joining at the current program point.
symex_targett::assignment_typet assignment_typet
Definition goto_symex.h:761
virtual void locality(const irep_idt &function_identifier, goto_symext::statet &state, const goto_functionst::goto_functiont &goto_function)
Preserves locality of parameters of a given function by applying L1 renaming to them.
virtual ~goto_symext()=default
A virtual destructor allowing derived classes to be cleaned up correctly.
bool constant_propagate_replace(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant proagate character replacement.
messaget::mstreamt & print_callstack_entry(const symex_targett::sourcet &target)
void dereference_rec(exprt &expr, statet &state, bool write, bool is_in_quantifier)
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:278
void validate(const validation_modet vm) const
Definition goto_symex.h:869
bool constant_propagate_string_concat(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
Attempt to constant propagate string concatenation.
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 assign_string_constant(statet &state, symex_assignt &symex_assign, const ssa_exprt &length, const constant_exprt &new_length, const ssa_exprt &char_array, const array_exprt &new_char_array)
Assign constant string length and string data given by a char array to given ssa variables.
optionalt< std::reference_wrapper< const array_exprt > > try_evaluate_constant_string(const statet &state, const exprt &content)
void process_array_expr(statet &, exprt &)
Given an expression, find the root object and the offset into it.
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.
A let expression.
Definition std_expr.h:3149
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Storage for symbolic execution paths to be resumed later.
Wrapper for expressions or types which have been renamed up to a given level.
Definition renamed.h:33
The shadow memory field definitions.
The shadow memory instrumentation performed during symbolic execution.
An expression containing a side effect.
Definition std_code.h:1450
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
Expression to hold a symbol (variable)
Definition std_expr.h:113
The symbol table base class interface.
The symbol table.
Symbol table entry.
Definition symbol.h:28
Functor for symex assignment.
Callback object that goto_symext::dereference_rec provides to value_set_dereferencet to provide value...
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
void validate(const namespacet &ns, const validation_modet vm) const
The type of an expression, extends irept.
Definition type.h:29
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition value_set.h:44
Symbolic Execution.
void symex_transition(goto_symext::statet &state)
Transition to the next instruction, which increments the internal program counter and initializes the...
renamedt< exprt, L2 > try_evaluate_pointer_comparisons(renamedt< exprt, L2 > condition, const value_sett &value_set, const irep_idt &language_mode, const namespacet &ns)
Try to evaluate pointer comparisons where they can be trivially determined using the value-set.
STL namespace.
#define NODISCARD
Definition nodiscard.h:22
nonstd::optional< T > optionalt
Definition optional.h:35
Symex Shadow Memory Instrumentation.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition guard_expr.h:20
Configuration used for a symbolic execution.
Identifies source in the context of symbolic execution.
Symbolic Execution.
Generate Equation using Symbolic Execution.
unsigned int statet
validation_modet