cprover
auto_objects.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_symex.h"
13 
14 #include <util/prefix.h>
15 #include <util/cprover_prefix.h>
16 #include <util/symbol_table.h>
17 #include <util/std_expr.h>
18 
20 {
22 
23  // produce auto-object symbol
24  symbolt symbol;
25 
26  symbol.base_name="auto_object"+std::to_string(dynamic_counter);
27  symbol.name="symex::"+id2string(symbol.base_name);
28  symbol.is_lvalue=true;
29  symbol.type=type;
30  symbol.mode=ID_C;
31 
32  state.symbol_table.add(symbol);
33 
34  return symbol_exprt(symbol.name, symbol.type);
35 }
36 
38 {
39  const typet &type=ns.follow(expr.type());
40 
41  if(type.id()==ID_struct)
42  {
43  const struct_typet &struct_type=to_struct_type(type);
44 
45  for(const auto &comp : struct_type.components())
46  {
47  member_exprt member_expr(expr, comp.get_name(), comp.type());
48 
49  initialize_auto_object(member_expr, state);
50  }
51  }
52  else if(type.id()==ID_pointer)
53  {
55  const typet &subtype = pointer_type.subtype();
56 
57  // we don't like function pointers and
58  // we don't like void *
59  if(subtype.id()!=ID_code &&
60  subtype.id()!=ID_empty)
61  {
62  // could be NULL nondeterministically
63 
64  address_of_exprt address_of_expr(
66 
67  if_exprt rhs(
70  address_of_expr);
71 
72  symex_assign(state, expr, rhs);
73  }
74  }
75 }
76 
78 {
79  expr.visit_pre([&state, this](const exprt &e) {
80  if(is_ssa_expr(e))
81  {
82  const ssa_exprt &ssa_expr = to_ssa_expr(e);
83  const irep_idt &obj_identifier = ssa_expr.get_object_name();
84 
85  if(obj_identifier != statet::guard_identifier())
86  {
87  const symbolt &symbol = ns.lookup(obj_identifier);
88 
89  if(has_prefix(id2string(symbol.base_name), "auto_object"))
90  {
91  // done already?
92  if(!state.get_level2().current_names.has_key(
93  ssa_expr.get_identifier()))
94  {
95  initialize_auto_object(e, state);
96  }
97  }
98  }
99  }
100  });
101 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet::subtype
const typet & subtype() const
Definition: type.h:47
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
goto_symext::dynamic_counter
static unsigned dynamic_counter
A monotonically increasing index for each created dynamic object.
Definition: goto_symex.h:789
goto_symex_statet::guard_identifier
static irep_idt guard_identifier()
Definition: goto_symex_state.h:141
typet
The type of an expression, extends irept.
Definition: type.h:28
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2087
prefix.h
exprt
Base class for all expressions.
Definition: expr.h:54
ssa_exprt::get_object_name
irep_idt get_object_name() const
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool_typet
The Boolean type.
Definition: std_types.h:37
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
goto_symext::trigger_auto_object
void trigger_auto_object(const exprt &, statet &)
Definition: auto_objects.cpp:77
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:2751
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
goto_symex_statet::symbol_table
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
Definition: goto_symex_state.h:69
goto_symext::initialize_auto_object
void initialize_auto_object(const exprt &, statet &)
Definition: auto_objects.cpp:37
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
goto_symex.h
Symbolic Execution.
goto_symext::make_auto_object
exprt make_auto_object(const typet &, statet &)
Definition: auto_objects.cpp:19
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
cprover_prefix.h
sharing_mapt::has_key
bool has_key(const key_type &k) const
Check if key is in map.
Definition: sharing_map.h:377
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
goto_symext::ns
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:256
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2528
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
symex_level2t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:77
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_statet::get_level2
const symex_level2t & get_level2() const
Definition: goto_state.h:41
exprt::visit_pre
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:259
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:200
symbol_table.h
Author: Diffblue Ltd.
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
std_expr.h
API to expression classes.
goto_symext::symex_assign
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.
Definition: goto_symex.cpp:39
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40