CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
symex_builtin_functions.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/c_types.h>
17#include <util/expr_util.h>
18#include <util/fresh_symbol.h>
22#include <util/simplify_expr.h>
23#include <util/std_code.h>
25
26#include "path_storage.h"
27
28inline static std::optional<typet> c_sizeof_type_rec(const exprt &expr)
29{
31
32 if(!sizeof_type.is_nil())
33 {
34 return static_cast<const typet &>(sizeof_type);
35 }
36 else if(expr.id()==ID_mult)
37 {
38 for(const auto &op : expr.operands())
39 {
40 const auto t = c_sizeof_type_rec(op);
41 if(t.has_value())
42 return t;
43 }
44 }
45
46 return {};
47}
48
50 statet &state,
51 const exprt &lhs,
52 const side_effect_exprt &code)
53{
54 PRECONDITION(code.operands().size() == 2);
55
56 if(lhs.is_nil())
57 return; // ignore
58
59 exprt size = to_binary_expr(code).op0();
60 std::optional<typet> object_type;
62 INVARIANT(function_symbol, "function associated with allocation not found");
63 const irep_idt &mode = function_symbol->mode;
64
65 // is the type given?
66 if(
67 code.type().id() == ID_pointer &&
68 to_pointer_type(code.type()).base_type().id() != ID_empty)
69 {
70 object_type = to_pointer_type(code.type()).base_type();
71 }
72 else
73 {
74 // to allow constant propagation
75 exprt tmp_size = state.rename(size, ns).get();
77
78 // special treatment for sizeof(T)*x
79 {
81
82 if(tmp_type.has_value())
83 {
84 // Did the size get multiplied?
87
88 if(!elem_size.has_value() || *elem_size==0)
89 {
90 }
91 else if(
92 !alloc_size.has_value() && tmp_size.id() == ID_mult &&
93 tmp_size.operands().size() == 2 &&
96 {
97 exprt s = to_mult_expr(tmp_size).op0();
98 if(s.is_constant())
99 {
100 s = to_mult_expr(tmp_size).op1();
103 }
104 else
107
108 object_type = array_typet(*tmp_type, s);
109 }
110 else if(alloc_size.has_value())
111 {
112 if(*alloc_size == *elem_size)
113 object_type = *tmp_type;
114 else
115 {
116 mp_integer elements = *alloc_size / (*elem_size);
117
118 if(elements * (*elem_size) == *alloc_size)
119 object_type =
120 array_typet(*tmp_type, from_integer(elements, tmp_size.type()));
121 }
122 }
123 }
124 }
125
126 if(!object_type.has_value())
128
129 // we introduce a fresh symbol for the size
130 // to prevent any issues of the size getting ever changed
131
132 if(
133 object_type->id() == ID_array &&
134 !to_array_type(*object_type).size().is_constant())
135 {
136 exprt &array_size = to_array_type(*object_type).size();
137
139 tmp_size.type(),
141 "dynamic_object_size",
142 code.source_location(),
143 mode,
144 state.symbol_table);
145 size_symbol.type.set(ID_C_constant, true);
146 size_symbol.value = array_size;
147
149 array_size = size_symbol.symbol_expr();
150
151 symex_assign(state, size_symbol.symbol_expr(), array_size_rhs);
152 }
153 }
154
155 // value
157 *object_type,
159 "dynamic_object",
160 code.source_location(),
161 mode,
162 state.symbol_table);
163 value_symbol.is_auxiliary = false;
164 value_symbol.is_thread_local = false;
165 value_symbol.is_file_local = false;
166 value_symbol.type.set(ID_C_dynamic, true);
167
168 // to allow constant propagation
169 exprt zero_init = state.rename(to_binary_expr(code).op1(), ns).get();
171
172 INVARIANT(
173 zero_init.is_constant(), "allocate expects constant as second argument");
174
175 if(!zero_init.is_zero() && !zero_init.is_false())
176 {
177 const auto zero_value =
178 zero_initializer(*object_type, code.source_location(), ns);
179 CHECK_RETURN(zero_value.has_value());
180 symex_assign(state, value_symbol.symbol_expr(), *zero_value);
181 }
182 else
183 {
184 auto lhs = value_symbol.symbol_expr();
185 auto rhs =
186 path_storage.build_symex_nondet(*object_type, code.source_location());
187 symex_assign(state, lhs, rhs);
188 }
189
190 exprt rhs;
191
192 if(object_type->id() == ID_array)
193 {
194 const auto &array_type = to_array_type(*object_type);
196 value_symbol.symbol_expr(), from_integer(0, array_type.index_type()));
197 rhs = address_of_exprt(index_expr, pointer_type(array_type.element_type()));
198 }
199 else
200 {
202 value_symbol.symbol_expr(), pointer_type(value_symbol.type));
203 }
205 state, value_symbol.symbol_expr(), code);
206
207 symex_assign(state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
208}
209
214 const irep_idt &parameter,
215 const pointer_typet &lhs_type,
216 const namespacet &ns)
217{
219
220 symbol_exprt parameter_expr = ns.lookup(parameter).symbol_expr();
221
222 // Visual Studio has va_list == char* and stores parameters of size no
223 // greater than the size of a pointer as immediate values
224 if(lhs_type.base_type().id() != ID_pointer)
225 {
226 auto parameter_size = size_of_expr(parameter_expr.type(), ns);
227 CHECK_RETURN(parameter_size.has_value());
228
231 ID_le,
232 from_integer(lhs_type.get_width(), parameter_size->type())};
233
234 return if_exprt{
235 fits_slot,
239 }
240 else
241 {
244 }
245}
246
248 statet &state,
249 const exprt &lhs,
250 const side_effect_exprt &code)
251{
252 PRECONDITION(code.operands().size() == 1);
253
254 if(lhs.is_nil())
255 return; // ignore
256
257 // create an array holding pointers to the parameters, starting after the
258 // parameter that the operand points to
259 const exprt &op = skip_typecast(to_unary_expr(code).op());
260 // this must be the address of a symbol
262 to_ssa_expr(to_address_of_expr(op).object()).get_object_name();
263
265 bool parameter_id_found = false;
266 for(auto &parameter : state.call_stack().top().parameter_names)
267 {
269 {
271 continue;
272 }
273
274 va_arg_operands.push_back(
276 }
277 const std::size_t va_arg_size = va_arg_operands.size();
278
281
282 exprt array = array_exprt{std::move(va_arg_operands), array_type};
283
285 array.type(),
287 "va_args",
288 state.source.pc->source_location(),
289 ns.lookup(state.source.function_id).mode,
290 state.symbol_table);
291 va_array.value = array;
292
293 array = clean_expr(std::move(array), state, false);
294 array = state.rename(std::move(array), ns).get();
295 do_simplify(array);
296 symex_assign(state, va_array.symbol_expr(), std::move(array));
297
299 va_array.symbol_expr(), from_integer(0, array_type.index_type())}};
300 rhs = state.rename(std::move(rhs), ns).get();
301 symex_assign(state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
302}
303
305{
306 if(src.id()==ID_typecast)
307 {
309 }
310 else if(src.id()==ID_address_of)
311 {
312 const exprt &object = to_address_of_expr(src).object();
313
314 if(object.id() == ID_index)
315 {
316 const auto &index_expr = to_index_expr(object);
317
318 if(
319 index_expr.array().id() == ID_string_constant &&
320 index_expr.index().is_zero())
321 {
322 const exprt &fmt_str = index_expr.array();
323 return to_string_constant(fmt_str).value();
324 }
325 }
326 else if(object.id() == ID_string_constant)
327 {
328 return to_string_constant(object).value();
329 }
330 }
331
332 return irep_idt();
333}
334
335static irep_idt get_string_argument(const exprt &src, const namespacet &ns)
336{
337 exprt tmp=src;
338 simplify(tmp, ns);
340}
341
344static std::optional<exprt> get_va_args(const exprt::operandst &operands)
345{
346 if(operands.size() != 2)
347 return {};
348
349 const exprt &second_op = skip_typecast(operands.back());
350 if(second_op.id() != ID_address_of)
351 return {};
352
354 return {};
355
356 const exprt &object = to_address_of_expr(second_op).object();
357 if(object.id() != ID_index)
358 return {};
359
360 const index_exprt &index_expr = to_index_expr(object);
361 if(!index_expr.index().is_zero())
362 return {};
363 else
364 return index_expr.array();
365}
366
368 statet &state,
369 const exprt &rhs)
370{
371 PRECONDITION(!rhs.operands().empty());
372
373 exprt tmp_rhs = rhs;
374 clean_expr(tmp_rhs, state, false);
375 tmp_rhs = state.rename(std::move(tmp_rhs), ns).get();
377
378 const exprt::operandst &operands=tmp_rhs.operands();
379 std::list<exprt> args;
380
381 // we either have any number of operands or a va_list as second operand
382 std::optional<exprt> va_args = get_va_args(operands);
383
384 if(!va_args.has_value())
385 {
386 args.insert(args.end(), std::next(operands.begin()), operands.end());
387 }
388 else
389 {
390 clean_expr(*va_args, state, false);
391 *va_args = state.field_sensitivity.apply(ns, state, *va_args, false);
392 *va_args = state.rename(*va_args, ns).get();
393 if(va_args->id() != ID_array)
394 {
395 // we were not able to constant-propagate va_args, and thus don't have
396 // sufficient information to generate printf -- give up
397 return;
398 }
399
400 // Visual Studio has va_list == char*, else we have va_list == void** and
401 // need to add dereferencing
402 const bool need_deref =
403 operands.back().type().id() == ID_pointer &&
404 to_pointer_type(operands.back().type()).base_type().id() == ID_pointer;
405
406 for(const auto &op : va_args->operands())
407 {
409 if(need_deref && parameter.id() == ID_address_of)
411 clean_expr(parameter, state, false);
412 parameter = state.rename(std::move(parameter), ns).get();
414
415 args.push_back(std::move(parameter));
416 }
417 }
418
419 const irep_idt format_string=
420 get_string_argument(operands[0], ns);
421
422 if(!format_string.empty())
424 state.guard.as_expr(),
425 state.source, "printf", format_string, args);
426}
427
429 statet &state,
430 const codet &code)
431{
432 PRECONDITION(code.operands().size() >= 2);
433
434 exprt id_arg = state.rename(code.op0(), ns).get();
435
436 std::list<exprt> args;
437
438 for(std::size_t i=1; i<code.operands().size(); i++)
439 {
440 exprt l2_arg = state.rename(code.operands()[i], ns).get();
442 args.emplace_back(std::move(l2_arg));
443 }
444
446
447 target.input(state.guard.as_expr(), state.source, input_id, args);
448}
449
451 statet &state,
452 const codet &code)
453{
454 PRECONDITION(code.operands().size() >= 2);
455 exprt id_arg = state.rename(code.op0(), ns).get();
456
457 std::list<renamedt<exprt, L2>> args;
458
459 for(std::size_t i=1; i<code.operands().size(); i++)
460 {
461 renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
462 if(symex_config.simplify_opt)
463 l2_arg.simplify(ns);
464 args.emplace_back(l2_arg);
465 }
466
468
469 target.output(state.guard.as_expr(), state.source, output_id, args);
470}
471
473 statet &state,
474 const exprt &lhs,
475 const side_effect_exprt &code)
476{
477 const auto &pointer_type = to_pointer_type(code.type());
478
479 const bool do_array =
482
483 // value
484 std::optional<typet> type;
485 if(do_array)
486 {
488 clean_expr(static_cast<const exprt &>(code.find(ID_size)), state, false);
490 }
491 else
492 type = pointer_type.base_type();
493
494 irep_idt mode;
495 if(
497 code.get(ID_statement) == ID_cpp_new)
498 {
499 mode = ID_cpp;
500 }
501 else if(code.get(ID_statement) == ID_java_new_array_data)
502 mode = ID_java;
503 else
504 INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code);
505
507 *type,
509 (do_array ? "dynamic_array" : "dynamic_value"),
510 code.source_location(),
511 mode,
512 state.symbol_table);
513 symbol.is_auxiliary = false;
514 symbol.is_thread_local = false;
515 symbol.is_file_local = false;
516 symbol.type.set(ID_C_dynamic, true);
517
518 // make symbol expression
519
521
522 if(do_array)
523 {
525 symbol.symbol_expr(),
526 from_integer(0, to_array_type(symbol.type).index_type())));
527 }
528 else
529 rhs.copy_to_operands(symbol.symbol_expr());
530
531 symex_assign(state, lhs, rhs);
532}
533
535 statet &,
536 const codet &)
537{
538 // TODO
539 #if 0
541 #endif
542}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
unsignedbv_typet unsigned_char_type()
Definition c_types.cpp:127
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
Arrays with given size.
Definition std_types.h:807
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:731
framet & top()
Definition call_stack.h:17
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:133
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:163
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
std::vector< irep_idt > parameter_names
Definition frame.h:35
guardt guard
Definition goto_state.h:58
Central data structure: state.
call_stackt & call_stack()
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.
field_sensitivityt field_sensitivity
symex_targett::sourcet source
const symbol_table_baset & outer_symbol_table
The symbol table associated with the goto-program being executed.
Definition goto_symex.h:249
virtual void symex_input(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP input.
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 void symex_cpp_delete(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP delete
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.
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
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:258
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.
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.
virtual void do_simplify(exprt &expr)
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.
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition goto_symex.h:185
exprt as_expr() const
Definition guard_expr.h:46
The trinary if-then-else operator.
Definition std_expr.h:2497
Array index operator.
Definition std_expr.h:1470
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
symex_nondet_generatort build_symex_nondet
Counter for nondet objects, which require unique names.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
void symex_field_dynamic_init(goto_symex_statet &state, const exprt &expr, const side_effect_exprt &code)
Initialize global-scope shadow memory for dynamically allocated memory.
An expression containing a side effect.
Definition std_code.h:1450
Expression to hold a symbol (variable)
Definition std_expr.h:131
Symbol table entry.
Definition symbol.h:28
bool is_auxiliary
Definition symbol.h:77
bool is_file_local
Definition symbol.h:73
bool is_thread_local
Definition symbol.h:71
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
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
Record formatted output.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 > > &args)
Record an output.
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
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
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.
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(I...
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
Storage of symbolic execution paths to resume.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
bool simplify(exprt &expr, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#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 ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition ssa_expr.h:145
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1137
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:29
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const string_constantt & to_string_constant(const exprt &expr)
goto_programt::const_targett pc
static std::optional< exprt > get_va_args(const exprt::operandst &operands)
Return an expression if operands fulfills all criteria that we expect of the expression to be a varia...
static std::optional< typet > c_sizeof_type_rec(const exprt &expr)
static irep_idt get_string_argument_rec(const exprt &src)
static exprt va_list_entry(const irep_idt &parameter, const pointer_typet &lhs_type, const namespacet &ns)
Construct an entry for the var args array.
static irep_idt get_string_argument(const exprt &src, const namespacet &ns)
#define size_type
Definition unistd.c:186
dstringt irep_idt