cprover
Loading...
Searching...
No Matches
auto_objects.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 <util/fresh_symbol.h>
13#include <util/pointer_expr.h>
14#include <util/std_code.h>
15#include <util/std_expr.h>
16
17#include "goto_symex.h"
18
20{
21 // produce auto-object symbol
23 type,
24 "symex",
25 "auto_object",
26 state.source.pc->source_location(),
27 ID_C,
28 state.symbol_table);
29 symbol.is_thread_local = false;
30 symbol.is_file_local = false;
31
32 return symbol.symbol_expr();
33}
34
36{
38 expr.type().id() != ID_struct,
39 "no L2-renamed expression expected, all struct-like types should be tags");
40
41 if(
42 auto struct_tag_type = type_try_dynamic_cast<struct_tag_typet>(expr.type()))
43 {
44 const struct_typet &struct_type = ns.follow_tag(*struct_tag_type);
45
46 for(const auto &comp : struct_type.components())
47 {
48 member_exprt member_expr(expr, comp.get_name(), comp.type());
49
50 initialize_auto_object(member_expr, state);
51 }
52 }
54 {
55 const typet &base_type = pointer_type->base_type();
56
57 // we don't like function pointers and
58 // we don't like void *
59 if(base_type.id() != ID_code && base_type.id() != ID_empty)
60 {
61 // could be NULL nondeterministically
62
63 address_of_exprt address_of_expr(
64 make_auto_object(base_type, state), *pointer_type);
65
66 if_exprt rhs(
69 address_of_expr);
70
71 symex_assign(state, expr, rhs);
72 }
73 }
74}
75
77{
78 expr.visit_pre([&state, this](const exprt &e) {
79 if(is_ssa_expr(e))
80 {
81 const ssa_exprt &ssa_expr = to_ssa_expr(e);
82 const irep_idt &obj_identifier = ssa_expr.get_object_name();
83
84 if(obj_identifier != statet::guard_identifier())
85 {
86 const symbolt &symbol = ns.lookup(obj_identifier);
87
88 if(symbol.base_name.starts_with("symex::auto_object"))
89 {
90 // done already?
92 ssa_expr.get_identifier()))
93 {
94 initialize_auto_object(e, state);
95 }
96 }
97 }
98 }
99 });
100}
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
Operator to return the address of an object.
The Boolean type.
Definition std_types.h:36
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
Base class for all expressions.
Definition expr.h:56
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:227
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:231
const symex_level2t & get_level2() const
Definition goto_state.h:45
static irep_idt guard_identifier()
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
symex_targett::sourcet source
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
Definition goto_symex.h:40
void initialize_auto_object(const exprt &, statet &)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition goto_symex.h:258
void trigger_auto_object(const exprt &, statet &)
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 &)
The trinary if-then-else operator.
Definition std_expr.h:2375
const irep_idt & id() const
Definition irep.h:388
Extract member of struct or union.
Definition std_expr.h:2849
The null pointer constant.
bool has_key(const key_type &k) const
Check if key is in map.
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
irep_idt get_object_name() const
Definition ssa_expr.cpp:145
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentst & components() const
Definition std_types.h:147
const irep_idt & get_identifier() const
Definition std_expr.h:160
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
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
The type of an expression, extends irept.
Definition type.h:29
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
Definition expr_cast.h:135
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.
API to expression classes for Pointers.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
bool is_ssa_expr(const exprt &expr)
Definition ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition ssa_expr.h:145
API to expression classes.
symex_renaming_levelt current_names
goto_programt::const_targett pc
dstringt irep_idt