CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symex_function_call.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution of ANSI-C
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_symex.h"
13
14#include <util/arith_tools.h>
15#include <util/byte_operators.h>
16#include <util/c_types.h>
18#include <util/fresh_symbol.h>
19#include <util/invariant.h>
20#include <util/range.h>
21#include <util/std_code.h>
22
23#include "expr_skeleton.h"
24#include "path_storage.h"
25#include "symex_assign.h"
26
27bool goto_symext::get_unwind_recursion(const irep_idt &, unsigned, unsigned)
28{
29 return false;
30}
31
33 const irep_idt &function_identifier,
34 const goto_functionst::goto_functiont &goto_function,
35 statet &state,
36 const exprt::operandst &arguments)
37{
38 // iterates over the arguments
39 exprt::operandst::const_iterator it1=arguments.begin();
40
41 // iterates over the types of the parameters
42 for(const auto &identifier : goto_function.parameter_identifiers)
43 {
45 !identifier.empty(), "function parameter must have an identifier");
46 state.call_stack().top().parameter_names.push_back(identifier);
47
48 const symbolt &symbol=ns.lookup(identifier);
49 symbol_exprt lhs=symbol.symbol_expr();
50
51 // this is the type that the n-th argument should have
52 const typet &parameter_type = symbol.type;
53
54 exprt rhs;
55
56 // if you run out of actual arguments there was a mismatch
57 if(it1==arguments.end())
58 {
59 log.warning() << state.source.pc->source_location().as_string()
60 << ": "
61 "call to '"
62 << id2string(function_identifier)
63 << "': "
64 "not enough arguments, inserting non-deterministic value"
65 << log.eom;
66
68 parameter_type, state.source.pc->source_location());
69 }
70 else
71 rhs=*it1;
72
73 if(rhs.is_nil())
74 {
75 // 'nil' argument doesn't get assigned
76 }
77 else
78 {
79 // It should be the same exact type.
80 if(parameter_type != rhs.type())
81 {
82 const typet &rhs_type = rhs.type();
83
84 // But we are willing to do some limited conversion.
85 // This is highly dubious, obviously.
86 // clang-format off
87 if(
88 (parameter_type.id() == ID_signedbv ||
91 parameter_type.id() == ID_bool ||
92 parameter_type.id() == ID_pointer ||
93 parameter_type.id() == ID_union ||
95 (rhs_type.id() == ID_signedbv ||
96 rhs_type.id() == ID_unsignedbv ||
97 rhs_type.id() == ID_c_bit_field ||
98 rhs_type.id() == ID_c_enum_tag ||
99 rhs_type.id() == ID_bool ||
100 rhs_type.id() == ID_pointer ||
101 rhs_type.id() == ID_union ||
102 rhs_type.id() == ID_union_tag))
103 // clang-format on
104 {
105 rhs = make_byte_extract(
107 }
108 else
109 {
110 std::ostringstream error;
111 error << state.source.pc->source_location().as_string() << ": "
112 << "function call: parameter \"" << identifier
113 << "\" type mismatch:\ngot " << rhs.type().pretty()
114 << "\nexpected " << parameter_type.pretty();
115 throw unsupported_operation_exceptiont(error.str());
116 }
117 }
118
119 assignment_typet assignment_type;
120
121 // We hide if we are in a hidden function.
122 if(state.call_stack().top().hidden_function)
123 assignment_type =
125 else
126 assignment_type =
128
129 lhs = to_symbol_expr(clean_expr(std::move(lhs), state, true));
130 rhs = clean_expr(std::move(rhs), state, false);
131
134 shadow_memory, state, assignment_type, ns, symex_config, target}
135 .assign_rec(lhs, expr_skeletont{}, rhs, lhs_conditions);
136 }
137
138 if(it1!=arguments.end())
139 it1++;
140 }
141
142 if(to_code_type(ns.lookup(function_identifier).type).has_ellipsis())
143 {
144 // These are va_arg arguments; their types may differ from call to call
145 for(; it1 != arguments.end(); it1++)
146 {
148 it1->type(),
149 id2string(function_identifier),
150 "va_arg",
151 state.source.pc->source_location(),
152 ns.lookup(function_identifier).mode,
153 state.symbol_table);
154 va_arg.is_parameter = true;
155
156 state.call_stack().top().parameter_names.push_back(va_arg.name);
157
158 symex_assign(state, va_arg.symbol_expr(), *it1);
159 }
160 }
161 else if(it1!=arguments.end())
162 {
163 // we got too many arguments, but we will just ignore them
164 }
165}
166
168 const get_goto_functiont &get_goto_function,
169 statet &state,
170 const goto_programt::instructiont &instruction)
171{
172 const exprt &function = instruction.call_function();
173
174 // If at some point symex_function_call can support more
175 // expression ids(), like ID_Dereference, please expand the
176 // precondition appropriately.
177 PRECONDITION(function.id() == ID_symbol);
178
181 state,
182 instruction.call_lhs(),
183 to_symbol_expr(instruction.call_function()),
184 instruction.call_arguments());
185}
186
188 const get_goto_functiont &get_goto_function,
189 statet &state,
190 const exprt &lhs,
191 const symbol_exprt &function,
192 const exprt::operandst &arguments)
193{
195
196 if(lhs.is_nil())
197 cleaned_lhs = lhs;
198 else
199 cleaned_lhs = clean_expr(lhs, state, true);
200
201 // no need to clean the function, which is a symbol only
202
204
205 for(auto &argument : arguments)
206 cleaned_arguments.push_back(clean_expr(argument, state, false));
207
208 target.location(state.guard.as_expr(), state.source);
209
210 PRECONDITION(function.id() == ID_symbol);
211 const irep_idt &identifier = to_symbol_expr(function).get_identifier();
212
214 {
216 symex_transition(state);
217 }
218 else if(identifier == CPROVER_PREFIX SHADOW_MEMORY_SET_FIELD)
219 {
221 symex_transition(state);
222 }
223 else
224 {
227 }
228}
229
231 const get_goto_functiont &get_goto_function,
232 statet &state,
233 const exprt &cleaned_lhs,
234 const symbol_exprt &function,
236{
237 const irep_idt &identifier = function.get_identifier();
238
239 const goto_functionst::goto_functiont &goto_function =
240 get_goto_function(identifier);
241
242 path_storage.dirty.populate_dirty_for_function(identifier, goto_function);
243
245 path_storage.safe_pointers.emplace(identifier, local_safe_pointerst{});
247 emplace_safe_pointers_result.first->second(goto_function.body);
248
250 identifier,
251 state.source.thread_nr,
252 state.call_stack().top().loop_iterations[identifier].count);
253
254 // see if it's too much
256 {
257 if(symex_config.unwinding_assertions)
258 {
259 vcc(
260 false_exprt(),
261 id2string(identifier) + ".recursion",
262 "recursion unwinding assertion",
263 state);
264 }
265 if(!symex_config.partial_loops)
266 {
267 // Rule out this path:
269 }
270
271 symex_transition(state);
272 return;
273 }
274
275 // read the arguments -- before the locality renaming
276 const std::vector<renamedt<exprt, L2>> renamed_arguments =
277 make_range(cleaned_arguments).map([&](const exprt &a) {
278 return state.rename(a, ns);
279 });
280
281 // we hide the call if the caller and callee are both hidden
282 const bool hidden =
283 state.call_stack().top().hidden_function && goto_function.is_hidden();
284
285 // record the call
287 state.guard.as_expr(), identifier, renamed_arguments, state.source, hidden);
288
289 if(!goto_function.body_available())
290 {
291 // create a fatal assertion
292 if(symex_config.unwinding_assertions)
293 {
294 const auto &symbol = ns.lookup(identifier);
295 const std::string property_id =
296 id2string(state.source.pc->source_location().get_function()) +
297 ".no-body." + id2string(identifier);
298 vcc(
299 false_exprt(),
300 property_id,
301 "no body for callee " + id2string(symbol.display_name()),
302 state);
303 }
304
305 // record the return
307 state.guard.as_expr(), identifier, state.source, hidden);
308
309 if(cleaned_lhs.is_not_nil())
310 {
311 const auto rhs = side_effect_expr_nondett(
312 cleaned_lhs.type(), state.source.pc->source_location());
313 symex_assign(state, cleaned_lhs, rhs);
314 }
315
316 symex_transition(state);
317 return;
318 }
319
320 // produce a new frame
321 PRECONDITION(!state.call_stack().empty());
322 framet &frame = state.call_stack().new_frame(state.source, state.guard);
323
324 // Only enable loop analysis when complexity is enabled.
325 if(symex_config.complexity_limits_active)
326 {
327 // Analyzes loops if required.
328 path_storage.add_function_loops(identifier, goto_function.body);
329 frame.loops_info = path_storage.get_loop_analysis(identifier);
330 }
331
332 // preserve locality of local variables
333 locality(identifier, state, goto_function);
334
335 // assign actuals to formal parameters
336 parameter_assignments(identifier, goto_function, state, cleaned_arguments);
337
338 frame.call_lhs = cleaned_lhs;
339 frame.end_of_function = --goto_function.body.instructions.end();
340 frame.function_identifier=identifier;
341 frame.hidden_function = goto_function.is_hidden();
342
343 // set up the 'return value symbol' when needed
344 if(frame.call_lhs.is_not_nil())
345 {
347 "goto_symex::return_value::" + id2string(identifier);
348
350 {
351 const symbolt &function_symbol = ns.lookup(identifier);
353 new_symbol; // these are thread-local and have dynamic lifetime
354 new_symbol.base_name = "return_value";
356 new_symbol.type = to_code_type(function_symbol.type).return_type();
357 new_symbol.mode = function_symbol.mode;
358 state.symbol_table.add(new_symbol);
359 }
360
361 frame.return_value_symbol =
363 }
364
365 const framet &p_frame = state.call_stack().previous_frame();
366 for(const auto &pair : p_frame.loop_iterations)
367 {
368 if(pair.second.is_recursion)
369 frame.loop_iterations.insert(pair);
370 }
371
372 // increase unwinding counter
373 frame.loop_iterations[identifier].is_recursion=true;
374 frame.loop_iterations[identifier].count++;
375
376 state.source.function_id = identifier;
377 symex_transition(state, goto_function.body.instructions.begin(), false);
378}
379
381static void pop_frame(
382 goto_symext::statet &state,
383 const path_storaget &path_storage,
384 bool doing_path_exploration)
385{
386 PRECONDITION(!state.call_stack().empty());
387
388 const framet &frame = state.call_stack().top();
389
390 // restore program counter
391 symex_transition(state, frame.calling_location.pc, false);
393
394 // restore L1 renaming
395 state.level1.restore_from(frame.old_level1);
396
397 // If the program is multi-threaded then the state guard is used to
398 // accumulate assumptions (in symex_assume_l2) and must be left alone.
399 // If however it is single-threaded then we should restore the guard, as the
400 // guard coming out of the function may be more complex (e.g. if the callee
401 // was { if(x) while(true) { } } then the guard may still be `!x`),
402 // but at this point all control-flow paths have either converged or been
403 // proven unviable, so we can stop specifying the callee's constraints when
404 // we generate an assumption or VCC.
405
406 // If we're doing path exploration then we do tail-duplication, and we
407 // actually *are* in a more-restricted context than we were when the
408 // function began.
409 if(state.threads.size() == 1 && !doing_path_exploration)
410 {
411 state.guard = frame.guard_at_function_start;
412 }
413
414 for(const irep_idt &l1_o_id : frame.local_objects)
415 {
416 const auto l2_entry_opt = state.get_level2().current_names.find(l1_o_id);
417
418 if(
419 l2_entry_opt.has_value() &&
420 (state.threads.size() == 1 ||
421 !path_storage.dirty(l2_entry_opt->get().first.get_object_name())))
422 {
424 }
425 }
426
427 state.call_stack().pop();
428}
429
432{
433 PRECONDITION(!state.call_stack().empty());
434
435 const bool hidden = state.call_stack().top().hidden_function;
436
437 // first record the return
439 state.guard.as_expr(), state.source.function_id, state.source, hidden);
440
441 // before we drop the frame, remember the call LHS
442 // and the return value symbol, if any
443 auto call_lhs = state.call_stack().top().call_lhs;
445
446 // now get rid of the frame
447 pop_frame(state, path_storage, symex_config.doing_path_exploration);
448
449 // after dropping the frame, assign the return value, if any
450 if(state.reachable && call_lhs.is_not_nil())
451 {
453 return_value_symbol.has_value(),
454 "must have return value symbol when assigning call lhs");
455 // the type of the call lhs and the return type might not match
457 return_value_symbol.value(), call_lhs.type());
458 symex_assign(state, call_lhs, casted_return_value);
459 }
460}
461
463 const irep_idt &function_identifier,
464 goto_symext::statet &state,
465 const goto_functionst::goto_functiont &goto_function)
466{
467 unsigned &frame_nr=
468 state.threads[state.source.thread_nr].function_frame[function_identifier];
469 frame_nr++;
470
471 for(const auto &param : goto_function.parameter_identifiers)
472 {
473 const ssa_exprt &renamed_param = state.add_object(
474 ns.lookup(param).symbol_expr(),
475 [this, &frame_nr](const irep_idt &l0_name) {
477 },
478 ns);
479
480 // Allocate shadow memory for parameters.
481 // They are like local variables.
483 }
484}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
bitvector_typet c_index_type()
Definition c_types.cpp:16
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition symbol.h:153
void pop()
Definition call_stack.h:36
framet & top()
Definition call_stack.h:17
framet & new_frame(symex_targett::sourcet calling_location, const guardt &guard)
Definition call_stack.h:30
const framet & previous_frame()
Definition call_stack.h:42
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Expression in which some part is missing and can be substituted for another expression.
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3199
Stack frames – these are used for function calls and for exceptions.
guardt guard_at_function_start
Definition frame.h:36
std::optional< symbol_exprt > return_value_symbol
Definition frame.h:39
exprt call_lhs
Definition frame.h:38
symex_targett::sourcet calling_location
Definition frame.h:34
std::unordered_map< irep_idt, loop_infot > loop_iterations
Definition frame.h:77
bool hidden_function
Definition frame.h:40
std::vector< irep_idt > parameter_names
Definition frame.h:35
symex_level1t old_level1
Definition frame.h:42
goto_programt::const_targett end_of_function
Definition frame.h:37
std::set< irep_idt > local_objects
Definition frame.h:44
irep_idt function_identifier
Definition frame.h:28
std::shared_ptr< lexical_loopst > loops_info
Definition frame.h:74
::goto_functiont goto_functiont
This class represents an instruction in the GOTO intermediate representation.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
guardt guard
Definition goto_state.h:58
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition goto_state.h:62
const symex_level2t & get_level2() const
Definition goto_state.h:45
Central data structure: state.
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.
call_stackt & call_stack()
symex_level1t level1
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
std::vector< threadt > threads
void drop_existing_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
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.
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 ...
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition goto_symex.h:810
symex_target_equationt & target
The equation that this execution is building up.
Definition goto_symex.h:266
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
shadow_memoryt shadow_memory
Shadow memory instrumentation API.
Definition goto_symex.h:839
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:258
virtual void vcc(const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state)
Symbolically execute a verification condition (assertion).
virtual void symex_end_of_function(statet &)
Symbolically execute a END_FUNCTION instruction.
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.
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.
messaget log
The messaget to write log messages to.
Definition goto_symex.h:278
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition goto_symex.h:185
void symex_assume_l2(statet &, const exprt &cond)
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 void symex_function_call(const get_goto_functiont &get_goto_function, statet &state, const goto_programt::instructiont &instruction)
Symbolically execute a FUNCTION_CALL instruction.
exprt as_expr() const
Definition guard_expr.h:46
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
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
bool is_not_nil() const
Definition irep.h:372
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...
mstreamt & warning() const
Definition message.h:396
static eomt eom
Definition message.h:289
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Storage for symbolic execution paths to be resumed later.
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
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::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.
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.
void symex_get_field(goto_symex_statet &state, const exprt &lhs, const exprt::operandst &arguments)
Symbolically executes a __CPROVER_get_field call.
void symex_field_local_init(goto_symex_statet &state, const ssa_exprt &expr)
Initialize local-scope shadow memory for local variables and parameters.
void symex_set_field(goto_symex_statet &state, const exprt::operandst &arguments)
Symbolically executes a __CPROVER_set_field call.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
Expression providing an SSA-renamed symbol of expressions.
Definition ssa_expr.h:17
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
irep_idt mode
Language mode.
Definition symbol.h:49
Functor for symex assignment.
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
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.
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
Thrown when we encounter an instruction, parameters to an instruction etc.
#define CPROVER_PREFIX
Expression skeleton.
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 ...
Fresh auxiliary symbol creation.
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
Storage of symbolic execution paths to resume.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
symbol_exprt return_value_symbol(const irep_idt &identifier, const namespacet &ns)
produces the symbol that is used to store the return value of the function with the given identifier
#define SHADOW_MEMORY_SET_FIELD
#define SHADOW_MEMORY_GET_FIELD
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
void restore_from(const symex_level1t &other)
Insert the content of other into this renaming.
goto_programt::const_targett pc
Symbolic Execution of assignments.
static void pop_frame(goto_symext::statet &state, const path_storaget &path_storage, bool doing_path_exploration)
pop one call frame