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  const exprt &expr,
39  statet &state)
40 {
41  const typet &type=ns.follow(expr.type());
42 
43  if(type.id()==ID_struct)
44  {
45  const struct_typet &struct_type=to_struct_type(type);
46 
47  for(const auto &comp : struct_type.components())
48  {
49  member_exprt member_expr;
50  member_expr.struct_op()=expr;
51  member_expr.set_component_name(comp.get_name());
52  member_expr.type()=comp.type();
53 
54  initialize_auto_object(member_expr, state);
55  }
56  }
57  else if(type.id()==ID_pointer)
58  {
60  const typet &subtype = ns.follow(pointer_type.subtype());
61 
62  // we don't like function pointers and
63  // we don't like void *
64  if(subtype.id()!=ID_code &&
65  subtype.id()!=ID_empty)
66  {
67  // could be NULL nondeterministically
68 
69  address_of_exprt address_of_expr(
71 
72  if_exprt rhs(
75  address_of_expr);
76 
77  code_assignt assignment(expr, rhs);
78  symex_assign(state, assignment);
79  }
80  }
81 }
82 
84  const exprt &expr,
85  statet &state)
86 {
87  if(expr.id()==ID_symbol &&
88  expr.get_bool(ID_C_SSA_symbol))
89  {
90  const ssa_exprt &ssa_expr=to_ssa_expr(expr);
91  const irep_idt &obj_identifier=ssa_expr.get_object_name();
92 
93  if(obj_identifier!="goto_symex::\\guard")
94  {
95  const symbolt &symbol=
96  ns.lookup(obj_identifier);
97 
98  if(has_prefix(id2string(symbol.base_name), "auto_object"))
99  {
100  // done already?
101  if(state.level2.current_names.find(ssa_expr.get_identifier())==
102  state.level2.current_names.end())
103  {
104  initialize_auto_object(expr, state);
105  }
106  }
107  }
108  }
109 
110  // recursive call
111  forall_operands(it, expr)
112  trigger_auto_object(*it, state);
113 }
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irep_idt mode
Language mode.
Definition: symbol.h:49
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const irep_idt & get_identifier() const
Definition: std_expr.h:176
The null pointer constant.
Definition: std_expr.h:4471
const componentst & components() const
Definition: std_types.h:205
The trinary if-then-else operator.
Definition: std_expr.h:3427
typet & type()
Return the type of the expression.
Definition: expr.h:68
The Boolean type.
Definition: std_types.h:28
Symbol table entry.
Definition: symbol.h:27
Structure type, corresponds to C style structs.
Definition: std_types.h:276
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
Extract member of struct or union.
Definition: std_expr.h:3890
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:3920
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:215
const irep_idt & id() const
Definition: irep.h:259
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
static unsigned dynamic_counter
Definition: goto_symex.h:423
The pointer type These are both &#39;bitvector_typet&#39; (they have a width) and &#39;type_with_subtypet&#39; (they ...
Definition: std_types.h:1507
Symbolic Execution.
API to expression classes.
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define forall_operands(it, expr)
Definition: expr.h:20
current_namest current_names
exprt make_auto_object(const typet &, statet &)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Author: Diffblue Ltd.
Operator to return the address of an object.
Definition: std_expr.h:3255
symex_level2t level2
void symex_assign(statet &, const code_assignt &)
typet type
Type of symbol.
Definition: symbol.h:31
Base class for all expressions.
Definition: expr.h:54
const exprt & struct_op() const
Definition: std_expr.h:3931
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
void trigger_auto_object(const exprt &, statet &)
void initialize_auto_object(const exprt &, statet &)
irep_idt get_object_name() const
Definition: ssa_expr.h:46
const source_locationt & source_location() const
Definition: expr.h:228
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
const typet & subtype() const
Definition: type.h:38
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
A codet representing an assignment in the program.
Definition: std_code.h:256
bool is_lvalue
Definition: symbol.h:66