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/prefix.h>
15#include <util/std_code.h>
16#include <util/std_expr.h>
17
18#include "goto_symex.h"
19
21{
22 // produce auto-object symbol
24 type,
25 "symex",
26 "auto_object",
27 state.source.pc->source_location(),
28 ID_C,
29 state.symbol_table);
30 symbol.is_thread_local = false;
31 symbol.is_file_local = false;
32
33 return symbol.symbol_expr();
34}
35
37{
38 const typet &type=ns.follow(expr.type());
39
40 if(type.id()==ID_struct)
41 {
42 const struct_typet &struct_type=to_struct_type(type);
43
44 for(const auto &comp : struct_type.components())
45 {
46 member_exprt member_expr(expr, comp.get_name(), comp.type());
47
48 initialize_auto_object(member_expr, state);
49 }
50 }
51 else if(type.id()==ID_pointer)
52 {
54 const typet &base_type = pointer_type.base_type();
55
56 // we don't like function pointers and
57 // we don't like void *
58 if(base_type.id() != ID_code && base_type.id() != ID_empty)
59 {
60 // could be NULL nondeterministically
61
62 address_of_exprt address_of_expr(
63 make_auto_object(base_type, state), pointer_type);
64
65 if_exprt rhs(
68 address_of_expr);
69
70 symex_assign(state, expr, rhs);
71 }
72 }
73}
74
76{
77 expr.visit_pre([&state, this](const exprt &e) {
78 if(is_ssa_expr(e))
79 {
80 const ssa_exprt &ssa_expr = to_ssa_expr(e);
81 const irep_idt &obj_identifier = ssa_expr.get_object_name();
82
83 if(obj_identifier != statet::guard_identifier())
84 {
85 const symbolt &symbol = ns.lookup(obj_identifier);
86
87 if(has_prefix(id2string(symbol.base_name), "symex::auto_object"))
88 {
89 // done already?
91 ssa_expr.get_identifier()))
92 {
93 initialize_auto_object(e, state);
94 }
95 }
96 }
97 }
98 });
99}
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
Operator to return the address of an object.
The Boolean type.
Definition std_types.h:36
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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:223
const symex_level2t & get_level2() const
Definition goto_state.h:45
Central data structure: state.
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
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:261
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:2323
const irep_idt & id() const
Definition irep.h:396
Extract member of struct or union.
Definition std_expr.h:2794
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
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.
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:144
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:142
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
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
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.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
symex_renaming_levelt current_names
goto_programt::const_targett pc