CBMC
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;
30class value_sett;
31
38{
39public:
42
83
85 virtual ~goto_symext() = default;
86
92 typedef
93 std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
95
104
119
128 symbol_table_baset &new_symbol_table,
130
143 const statet &saved_state,
145
158 [[nodiscard]] virtual symbol_tablet
159 symex_with_state(statet &state, const get_goto_functiont &get_goto_functions);
160
169
172 bool ignore_assertions = false;
173
182 virtual bool check_break(const irep_idt &loop_id, unsigned unwind);
183
184protected:
187
192 std::unique_ptr<statet>
194
201 statet &state,
203
211 virtual void
213
224 statet &state);
225
230
233 void print_symex_step(statet &state);
234
237
238public:
239
243
244protected:
251
260
265
268
272
276 std::vector<symbol_exprt> instruction_local_symbols;
277
279 mutable messaget log;
280
282
292 exprt clean_expr(exprt expr, statet &state, bool write);
293
294 void trigger_auto_object(const exprt &, statet &);
295 void initialize_auto_object(const exprt &, statet &);
296
303 virtual void dereference(exprt &, statet &, bool write);
304
306 void dereference_rec(
307 exprt &expr,
308 statet &state,
309 bool write,
310 bool is_in_quantifier);
312 const exprt &,
313 statet &,
314 bool keep_array);
315
318 virtual void symex_goto(statet &state);
321 void symex_unreachable_goto(statet &state);
325 void symex_set_return_value(statet &state, const exprt &return_value);
328 virtual void symex_start_thread(statet &state);
331 virtual void symex_atomic_begin(statet &state);
334 virtual void symex_atomic_end(statet &state);
337 virtual void symex_decl(statet &state);
342 virtual void symex_decl(statet &state, const symbol_exprt &expr);
345 virtual void symex_dead(statet &state);
349 void symex_dead(statet &state, const symbol_exprt &symbol_expr);
352 virtual void symex_other(statet &state);
353
355
369 const exprt &original_guard,
370 const exprt &new_guard,
371 const namespacet &ns);
372
389 goto_symex_statet &state,
390 exprt condition,
394 const namespacet &ns);
395
401 virtual void vcc(
402 const exprt &cond,
403 const irep_idt &property_id,
404 const std::string &msg,
405 statet &state);
406
411 virtual void symex_assume(statet &state, const exprt &cond);
412 void symex_assume_l2(statet &, const exprt &cond);
413
418 void merge_gotos(statet &state);
419
426 virtual void merge_goto(
427 const symex_targett::sourcet &source,
429 statet &state);
430
435
441 virtual bool should_stop_unwind(
442 const symex_targett::sourcet &source,
443 const call_stackt &context,
444 unsigned unwind);
445
446 virtual void loop_bound_exceeded(statet &state, const exprt &guard);
447
455 virtual void symex_function_call(
457 statet &state,
458 const goto_programt::instructiont &instruction);
459
465 virtual void locality(
466 const irep_idt &function_identifier,
467 goto_symext::statet &state,
468 const goto_functionst::goto_functiont &goto_function);
469
472 virtual void symex_end_of_function(statet &);
473
481 virtual void symex_function_call_symbol(
483 statet &state,
484 const exprt &lhs,
485 const symbol_exprt &function,
486 const exprt::operandst &arguments);
487
502 statet &state,
503 const exprt &cleaned_lhs,
504 const symbol_exprt &function,
506
507 virtual bool get_unwind_recursion(
508 const irep_idt &identifier,
509 unsigned thread_nr,
510 unsigned unwind);
511
519 const irep_idt &function_identifier,
520 const goto_functionst::goto_functiont &goto_function,
521 statet &state,
522 const exprt::operandst &arguments);
523
524 // exceptions
527 void symex_throw(statet &state);
530 void symex_catch(statet &state);
531
532 virtual void do_simplify(exprt &expr, const value_sett &value_set);
533
539 void symex_assign(statet &state, const exprt &lhs, const exprt &rhs);
540
550 statet &state,
552 const exprt &lhs,
553 const exprt &rhs);
554
562 statet &state,
565
575 statet &state,
578
588 statet &state,
591
601 statet &state,
604
614 statet &state,
617
627 statet &state,
630
645 statet &state,
648
658 statet &state,
661
664 statet &state,
667
670 statet &state,
673 bool to_upper);
674
677 statet &state,
680
702 statet &state,
704 const ssa_exprt &length,
706 const ssa_exprt &char_array,
708
718 statet &state,
720 const std::string &aux_symbol_name,
721 const ssa_exprt &char_array,
723
735 statet &state,
739
740 std::optional<std::reference_wrapper<const array_exprt>>
741 try_evaluate_constant_string(const statet &state, const exprt &content);
742
743 // clang-format off
744 static std::optional<std::reference_wrapper<const constant_exprt>>
746 const statet &state,
747 const exprt &expr);
748 // clang-format on
749
750 // havocs the given object
751 void havoc_rec(statet &state, const guardt &guard, const exprt &dest);
752
754
760 void lift_lets(statet &, exprt &);
761
766 void lift_let(statet &state, const let_exprt &let_expr);
767
768 virtual void
769 symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &);
770
776 virtual void symex_allocate(
777 statet &state,
778 const exprt &lhs,
779 const side_effect_exprt &code);
783 virtual void symex_cpp_delete(statet &state, const codet &code);
789 virtual void
790 symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code);
791
795 virtual void symex_printf(statet &state, const exprt &rhs);
799 virtual void symex_input(statet &state, const codet &code);
803 virtual void symex_output(statet &state, const codet &code);
804
806
812
813public:
823 std::size_t path_segment_vccs;
824
825protected:
833
836
838
841
842public:
843 unsigned get_total_vccs() const
844 {
845 INVARIANT(
846 _total_vccs != std::numeric_limits<unsigned>::max(),
847 "symex_threaded_step should have been executed at least once before "
848 "attempting to read total_vccs");
849 return _total_vccs;
850 }
851
852 unsigned get_remaining_vccs() const
853 {
854 INVARIANT(
855 _remaining_vccs != std::numeric_limits<unsigned>::max(),
856 "symex_threaded_step should have been executed at least once before "
857 "attempting to read remaining_vccs");
858 return _remaining_vccs;
859 }
860
861 void validate(const validation_modet vm) const
862 {
863 target.validate(ns, vm);
864 }
865};
866
874
878 bool is_backwards_goto);
879
880#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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Array constructor from list of elements.
Definition std_expr.h:1621
Data structure for representing an arbitrary statement in a program.
Symex complexity module.
A constant literal expression.
Definition std_expr.h:3118
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
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:38
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 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_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:837
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
Definition goto_symex.h:41
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.
virtual void symex_input(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP input.
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...
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)
void lift_let(statet &state, const let_exprt &let_expr)
Execute a single let expression, which should not have any nested let expressions (use lift_lets inst...
virtual void symex_goto(statet &state)
Symbolically execute a GOTO instruction.
unsigned get_remaining_vccs() const
Definition goto_symex.h:852
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.
static std::optional< std::reference_wrapper< const constant_exprt > > try_evaluate_constant(const statet &state, const exprt &expr)
void phi_function(const goto_statet &goto_state, statet &dest_state)
Merge the SSA assignments from goto_state into dest_state.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition goto_symex.h: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.
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:834
symex_target_equationt & target
The equation that this execution is building up.
Definition goto_symex.h:267
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
virtual void symex_cpp_delete(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP delete
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.
virtual void symex_allocate(statet &state, const exprt &lhs, const side_effect_exprt &code)
Symbolically execute an assignment instruction that has an allocate on the right hand side.
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:264
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:52
unsigned atomic_section_counter
A monotonically increasing index for each encountered ATOMIC_BEGIN instruction.
Definition goto_symex.h:271
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.
unsigned get_total_vccs() const
Definition goto_symex.h:843
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:840
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.
void initialize_auto_object(const exprt &, statet &)
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.
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...
virtual void symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition goto_symex.h:259
void trigger_auto_object(const exprt &, statet &)
void lift_lets(statet &, exprt &)
Execute any let expressions in expr using symex_assignt::assign_symbol.
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.
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.
exprt make_auto_object(const typet &, statet &)
void print_symex_step(statet &state)
Prints the route of symex as it walks through the code.
virtual void symex_printf(statet &state, const exprt &rhs)
Symbolically execute an OTHER instruction that does a CPP printf
virtual void symex_output(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP output.
void symex_throw(statet &state)
Symbolically execute a THROW instruction.
exprt address_arithmetic(const exprt &, statet &, bool keep_array)
Transforms an lvalue expression by replacing any dereference operations it contains with explicit ref...
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.
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
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.
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.
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.
symbol_exprt cache_dereference(exprt &dereference_result, statet &state)
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
virtual void dereference(exprt &, statet &, bool write)
Replace all dereference operations within expr with explicit references to the objects they may refer...
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:753
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)
If expr is a dereference_exprt, replace it with explicit references to the objects it may point to.
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
void validate(const validation_modet vm) const
Definition goto_symex.h:861
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.
void process_array_expr(statet &, exprt &)
Given an expression, find the root object and the offset into it.
std::optional< std::reference_wrapper< const array_exprt > > try_evaluate_constant_string(const statet &state, const exprt &content)
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:3332
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
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.
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:131
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:43
Symbolic Execution.
void symex_transition(goto_symext::statet &state)
Transition to the next instruction, which increments the internal program counter and initializes the...
STL namespace.
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.
ssize_t write(int fildes, const void *buf, size_t nbyte)
Definition unistd.c:195
validation_modet