Go to the documentation of this file.
45 const code_typet &function_type=goto_function.type;
48 exprt::operandst::const_iterator it1=arguments.begin();
51 for(
const auto &identifier : goto_function.parameter_identifiers)
54 !identifier.empty(),
"function parameter must have an identifier");
61 const typet ¶meter_type = symbol.
type;
66 if(it1==arguments.end())
73 "not enough arguments, inserting non-deterministic value"
77 parameter_type, state.
source.
pc->source_location);
89 if(parameter_type != rhs.
type())
97 (parameter_type.
id() == ID_signedbv ||
98 parameter_type.
id() == ID_unsignedbv ||
99 parameter_type.
id() == ID_c_enum_tag ||
100 parameter_type.
id() == ID_bool ||
101 parameter_type.
id() == ID_pointer ||
102 parameter_type.
id() == ID_union ||
103 parameter_type.
id() == ID_union_tag) &&
104 (rhs_type.
id() == ID_signedbv ||
105 rhs_type.
id() == ID_unsignedbv ||
106 rhs_type.
id() == ID_c_bit_field ||
107 rhs_type.
id() == ID_c_enum_tag ||
108 rhs_type.
id() == ID_bool ||
109 rhs_type.
id() == ID_pointer ||
110 rhs_type.
id() == ID_union ||
111 rhs_type.
id() == ID_union_tag))
123 std::ostringstream error;
124 error << state.
source.
pc->source_location.as_string() <<
": "
125 <<
"function call: parameter \"" << identifier
126 <<
"\" type mismatch:\ngot " << rhs.
type().
pretty()
127 <<
"\nexpected " << parameter_type.
pretty();
143 rhs =
clean_expr(std::move(rhs), state,
false);
150 if(it1!=arguments.end())
157 for(; it1 != arguments.end(); it1++)
164 ns.
lookup(function_identifier).mode,
173 else if(it1!=arguments.end())
206 *it =
clean_expr(std::move(*it), state,
false);
236 auto emplace_safe_pointers_result =
238 if(emplace_safe_pointers_result.second)
239 emplace_safe_pointers_result.first->second(goto_function.body);
268 const std::vector<renamedt<exprt, L2>> renamed_arguments =
273 const bool callee_is_hidden =
ns.
lookup(identifier).is_hidden();
281 if(!goto_function.body_available())
304 arg.type().id() == ID_pointer &&
305 !arg.type().subtype().get_bool(ID_C_constant) &&
306 arg.type().subtype().id() != ID_code)
346 if(pair.second.is_recursion)
362 bool doing_path_exploration)
388 if(state.
threads.size() == 1 && !doing_path_exploration)
396 std::vector<irep_idt> keys_to_erase;
398 for(
const auto &pair : view)
400 const irep_idt l1_o_id = pair.second.first.get_l1_object_identifier();
406 path_storage.
dirty(pair.second.first.get_object_name())))
411 keys_to_erase.push_back(pair.first);
414 for(
const irep_idt &key : keys_to_erase)
439 const irep_idt &function_identifier,
449 for(
const auto ¶m : goto_function.parameter_identifiers)
452 ns.
lookup(param).symbol_expr(),
453 [&path_storage, &frame_nr](
const irep_idt &l0_name) {
bool havoc_undefined_functions
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool has_ellipsis() const
#define Forall_expr(it, expr)
void symex_assume_l2(statet &, const exprt &cond)
#define CPROVER_FKT_PREFIX
Symbolic Execution of assignments.
void restore_from(const symex_level1t &other)
Insert the content of other into this renaming.
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
virtual void symex_function_call_code(const get_goto_functiont &get_goto_function, statet &state, const code_function_callt &call)
Symbolic execution of a function call by inlining.
The type of an expression, extends irept.
Fresh auxiliary symbol creation.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
goto_programt::const_targett pc
symex_target_equationt & target
The equation that this execution is building up.
Storage for symbolic execution paths to be resumed later.
typet type
Type of symbol.
Operator to dereference a pointer.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Central data structure: state.
irep_idt function_identifier
Thrown when we encounter an instruction, parameters to an instruction etc.
symex_targett::sourcet calling_location
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
guard_managert & guard_manager
virtual void symex_fkt(statet &state, const code_function_callt &code)
Symbolically execute a FUNCTION_CALL instruction for a function whose name starts with CPROVER_FKT_PR...
Base class for all expressions.
guardt guard_at_function_start
symex_targett::sourcet source
Functor for symex assignment.
Expression to hold a symbol (variable)
bitvector_typet index_type()
void symex_assign(statet &state, const code_assignt &code)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
@ VISIBLE_ACTUAL_PARAMETER
messaget log
The messaget to write log messages to.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
irep_idt byte_extract_id()
typet & type()
Return the type of the expression.
framet & new_frame(symex_targett::sourcet calling_location, const guardt &guard)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
std::vector< threadt > threads
std::vector< irep_idt > parameter_names
std::shared_ptr< lexical_loopst > get_loop_analysis(const irep_idt &function_id)
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...
Expression classes for byte-level operators.
std::shared_ptr< lexical_loopst > loops_info
call_stackt & call_stack()
const std::string & id2string(const irep_idt &d)
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
@ HIDDEN_ACTUAL_PARAMETER
static void pop_frame(goto_symext::statet &state, const path_storaget &path_storage, bool doing_path_exploration)
pop one call frame
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
bool doing_path_exploration
bool unwinding_assertions
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.
std::unordered_map< irep_idt, loop_infot > loop_iterations
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
virtual void symex_end_of_function(statet &)
Symbolically execute a END_FUNCTION instruction.
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
virtual void symex_function_call_symbol(const get_goto_functiont &get_goto_function, statet &state, const code_function_callt &code)
Symbolic execution of a call to a function call.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
goto_programt::const_targett end_of_function
Ranges: pair of begin and end iterators, which can be initialized from containers,...
std::vector< exprt > operandst
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 Boolean constant false.
Stack frames – these are used for function calls and for exceptions.
void symex_transition(goto_symext::statet &state)
Transition to the next instruction, which increments the internal program counter and initializes the...
void get_view(viewt &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
A side_effect_exprt that returns a non-deterministically chosen value.
::goto_functiont goto_functiont
void havoc_rec(statet &state, const guardt &guard, const exprt &dest)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
bool complexity_limits_active
Whether this run of symex is under complexity limits.
const framet & previous_frame()
symex_renaming_levelt current_names
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Map function identifiers to local_safe_pointerst instances.
virtual void function_call(const exprt &guard, const irep_idt &function_id, const std::vector< renamedt< exprt, L2 >> &ssa_function_arguments, const sourcet &source, bool hidden)
Record a function call.
const symex_level2t & get_level2() const
virtual void vcc(const exprt &, const std::string &msg, statet &)
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 ...
const symex_configt symex_config
The configuration to use for this symbolic execution.
std::set< irep_idt > local_objects
std::size_t get_unique_l1_index(const irep_idt &id, std::size_t minimum_index)
Provide a unique L1 index for a given id, starting from minimum_index.
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.
bool has_prefix(const std::string &s, const std::string &prefix)
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
virtual void no_body(const irep_idt &identifier)
Log a warning that a function has no body.
static void locality(const irep_idt &function_identifier, goto_symext::statet &state, path_storaget &path_storage, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Preserves locality of parameters of a given function by applying L1 renaming to them.
A codet representing an assignment in the program.
virtual void symex_function_call(const get_goto_functiont &get_goto_function, statet &state, const code_function_callt &code)
Symbolically execute a FUNCTION_CALL instruction.
The Boolean constant true.
mstreamt & warning() const
const source_locationt & source_location() const
ssa_exprt add_object(const symbol_exprt &expr, std::function< std::size_t(const irep_idt &)> index_generator, const namespacet &ns)
Instantiate the object expr.
ranget< iteratort > make_range(iteratort begin, iteratort end)
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
irep_idt name
The unique identifier.
void drop_existing_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
Expression in which some part is missing and can be substituted for another expression.