29 const irept &sizeof_type=expr.
find(ID_C_c_sizeof_type);
33 return static_cast<const typet &
>(sizeof_type);
35 else if(expr.
id()==ID_mult)
37 for(
const auto &op : expr.
operands())
48void goto_symext::symex_allocate(
59 std::optional<typet> object_type;
61 INVARIANT(function_symbol,
"function associated with allocation not found");
62 const irep_idt &mode = function_symbol->mode;
66 code.
type().
id() == ID_pointer &&
74 exprt tmp_size = state.rename(size,
ns).get();
75 simplify_expr_with_value_sett{state.value_set,
language_mode,
ns}.simplify(
82 if(tmp_type.has_value())
88 if(!elem_size.has_value() || *elem_size==0)
92 !alloc_size.has_value() && tmp_size.
id() == ID_mult &&
108 object_type = array_typet(*tmp_type, s);
110 else if(alloc_size.has_value())
112 if(*alloc_size == *elem_size)
113 object_type = *tmp_type;
116 mp_integer elements = *alloc_size / (*elem_size);
118 if(elements * (*elem_size) == *alloc_size)
126 if(!object_type.has_value())
133 object_type->id() == ID_array &&
141 "dynamic_object_size",
145 size_symbol.
type.
set(ID_C_constant,
true);
146 size_symbol.
value = array_size;
148 auto array_size_rhs = array_size;
166 value_symbol.
type.
set(ID_C_dynamic,
true);
170 simplify_expr_with_value_sett{state.value_set,
language_mode,
ns}.simplify(
174 zero_init.
is_constant(),
"allocate expects constant as second argument");
178 const auto zero_value =
193 if(object_type->id() == ID_array)
196 index_exprt index_expr(
198 rhs = address_of_exprt(index_expr,
pointer_type(array_type.element_type()));
202 rhs=address_of_exprt(
227 auto parameter_size =
size_of_expr(parameter_expr.type(), ns);
248void goto_symext::symex_va_start(
266 bool parameter_id_found =
false;
267 for(
auto ¶meter : state.call_stack().top().parameter_names)
269 if(!parameter_id_found)
271 parameter_id_found = parameter == start_parameter;
275 va_arg_operands.push_back(
278 const std::size_t va_arg_size = va_arg_operands.size();
280 const auto array_type = array_typet{
pointer_type(empty_typet{}),
283 exprt array = array_exprt{std::move(va_arg_operands), array_type};
289 state.source.pc->source_location(),
290 ns.lookup(state.source.function_id).mode,
292 va_array.
value = array;
294 array =
clean_expr(std::move(array), state,
false);
295 array = state.rename(std::move(array),
ns).
get();
299 exprt rhs = address_of_exprt{index_exprt{
301 rhs = state.rename(std::move(rhs),
ns).
get();
307 if(src.
id()==ID_typecast)
311 else if(src.
id()==ID_address_of)
315 if(
object.
id() == ID_index)
320 index_expr.array().id() == ID_string_constant &&
321 index_expr.index().is_zero())
323 const exprt &fmt_str = index_expr.array();
327 else if(
object.
id() == ID_string_constant)
351 if(operands.size() != 2)
355 if(second_op.
id() == ID_struct)
359 if(second_op.
operands().size() != 5)
365 if(second_op.
id() != ID_address_of)
372 if(
object.
id() != ID_index)
379 return index_expr.
array();
382void goto_symext::symex_printf(
390 tmp_rhs = state.rename(std::move(tmp_rhs),
ns).
get();
394 std::list<exprt> args;
397 std::optional<exprt> va_args =
get_va_args(operands);
399 if(!va_args.has_value())
401 args.insert(args.end(), std::next(operands.begin()), operands.end());
406 *va_args = state.field_sensitivity.apply(
ns, state, *va_args,
false);
407 *va_args = state.rename(*va_args,
ns).get();
408 if(va_args->id() != ID_array)
417 const bool need_deref =
418 operands.back().type().id() == ID_struct_tag ||
419 (operands.back().type().
id() == ID_pointer &&
422 for(
const auto &op : va_args->operands())
425 if(need_deref && parameter.
id() == ID_address_of)
428 parameter = state.rename(std::move(parameter),
ns).
get();
431 args.push_back(std::move(parameter));
438 if(!format_string.
empty())
440 state.guard.as_expr(),
441 state.source,
"printf", format_string, args);
444void goto_symext::symex_input(
450 exprt id_arg = state.rename(code.
op0(),
ns).get();
452 std::list<exprt> args;
454 for(std::size_t i=1; i<code.
operands().size(); i++)
456 exprt l2_arg = state.rename(code.
operands()[i],
ns).get();
458 args.emplace_back(std::move(l2_arg));
464 target.input(state.guard.as_expr(), state.source, input_id, args);
467void goto_symext::symex_output(
472 exprt id_arg = state.rename(code.
op0(),
ns).
get();
474 std::list<renamedt<exprt, L2>> args;
476 for(std::size_t i=1; i<code.
operands().size(); i++)
478 renamedt<exprt, L2> l2_arg = state.rename(code.
operands()[i],
ns);
481 simplify_expr_with_value_sett simp{state.value_set,
language_mode,
ns};
484 args.emplace_back(l2_arg);
490 target.output(state.guard.as_expr(), state.source, output_id, args);
493void goto_symext::symex_cpp_new(
500 const bool do_array =
501 (code.
get(ID_statement) == ID_cpp_new_array ||
502 code.
get(ID_statement) == ID_java_new_array_data);
505 std::optional<typet> type;
509 clean_expr(
static_cast<const exprt &
>(code.
find(ID_size)), state,
false);
517 code.
get(ID_statement) == ID_cpp_new_array ||
518 code.
get(ID_statement) == ID_cpp_new)
522 else if(code.
get(ID_statement) == ID_java_new_array_data)
530 (do_array ?
"dynamic_array" :
"dynamic_value"),
537 symbol.
type.
set(ID_C_dynamic,
true);
555void goto_symext::symex_cpp_delete(
561 bool do_array=code.
get(ID_statement)==ID_cpp_delete_array;
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
unsignedbv_typet unsigned_char_type()
Operator to return the address of an object.
typet index_type() const
The type of the index expressions into any instance of this type.
const exprt & size() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
std::size_t get_width() const
Data structure for representing an arbitrary statement in a program.
Base class for all expressions.
std::vector< exprt > operandst
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
bool is_false() const
Return whether the expression is a constant representing false.
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
const symbol_table_baset & outer_symbol_table
The symbol table associated with the goto-program being executed.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
symex_target_equationt & target
The equation that this execution is building up.
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
shadow_memoryt shadow_memory
Shadow memory instrumentation API.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
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.
const symex_configt symex_config
The configuration to use for this symbolic execution.
The trinary if-then-else operator.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
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 simplify(simplify_exprt &simplifier)
An expression containing a side effect.
virtual bool simplify(exprt &expr)
irep_idt get_object_name() const
void value(const irep_idt &)
Expression to hold a symbol (variable)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
exprt value
Initial value of symbol.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
State type in value_set_domaint, used in value-set analysis and goto-symex.
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.
#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)
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)
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const string_constantt & to_string_constant(const exprt &expr)
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 ¶meter, 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 value_sett &value_set, const irep_idt &language_mode, const namespacet &ns)