cprover
symex_dereference_state.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 
13 
14 #include <util/symbol_table.h>
15 
17  const exprt &expr,
18  const symbolt *&symbol)
19 {
20  const namespacet &ns=goto_symex.ns;
21 
22  if(expr.id()==ID_symbol &&
23  expr.get_bool(ID_C_SSA_symbol))
24  {
25  const ssa_exprt &ssa_expr=to_ssa_expr(expr);
26  if(ssa_expr.get_original_expr().id()!=ID_symbol)
27  return false;
28 
29  const symbolt &ptr_symbol=
30  ns.lookup(to_ssa_expr(expr).get_object_name());
31 
32  const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
33 
34  if(failed_symbol!="" &&
35  !ns.lookup(failed_symbol, symbol))
36  {
37  symbolt sym=*symbol;
38  symbolt *sym_ptr=nullptr;
39  symbol_exprt sym_expr=sym.symbol_expr();
40  state.rename(sym_expr, ns, goto_symex_statet::L1);
41  sym.name=to_ssa_expr(sym_expr).get_identifier();
42  state.symbol_table.move(sym, sym_ptr);
43  symbol=sym_ptr;
44  return true;
45  }
46  }
47  else if(expr.id()==ID_symbol)
48  {
49  const symbolt &ptr_symbol=
50  ns.lookup(to_symbol_expr(expr).get_identifier());
51 
52  const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
53 
54  if(failed_symbol!="" &&
55  !ns.lookup(failed_symbol, symbol))
56  {
57  symbolt sym=*symbol;
58  symbolt *sym_ptr=nullptr;
59  symbol_exprt sym_expr=sym.symbol_expr();
60  state.rename(sym_expr, ns, goto_symex_statet::L1);
61  sym.name=to_ssa_expr(sym_expr).get_identifier();
62  state.symbol_table.move(sym, sym_ptr);
63  symbol=sym_ptr;
64  return true;
65  }
66  }
67 
68  return false;
69 }
70 
72  const exprt &expr,
73  value_setst::valuest &value_set)
74 {
75  state.value_set.get_value_set(expr, value_set, goto_symex.ns);
76 
77  #if 0
78  std::cout << "**************************\n";
79  state.value_set.output(goto_symex.ns, std::cout);
80  std::cout << "**************************\n";
81  #endif
82 
83  #if 0
84  std::cout << "E: " << from_expr(goto_symex.ns, "", expr) << '\n';
85  #endif
86 
87  #if 0
88  std::cout << "**************************\n";
89  for(value_setst::valuest::const_iterator it=value_set.begin();
90  it!=value_set.end();
91  it++)
92  std::cout << from_expr(goto_symex.ns, "", *it) << '\n';
93  std::cout << "**************************\n";
94  #endif
95 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symex_dereference_statet::state
goto_symext::statet & state
Definition: symex_dereference_state.h:33
symex_dereference_statet::has_failed_symbol
bool has_failed_symbol(const exprt &expr, const symbolt *&symbol) override
Definition: symex_dereference_state.cpp:16
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_symex_statet::L1
Definition: goto_symex_state.h:72
goto_symex_statet::rename
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Definition: goto_symex_state.cpp:273
exprt
Base class for all expressions.
Definition: expr.h:54
goto_symex_statet::value_set
value_sett value_set
Definition: goto_symex_state.h:109
value_sett::get_value_set
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
Definition: value_set.cpp:320
symex_dereference_state.h
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
symex_dereference_statet::get_value_set
void get_value_set(const exprt &expr, value_setst::valuest &value_set) override
Definition: symex_dereference_state.cpp:71
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
value_setst::valuest
std::list< exprt > valuest
Definition: value_sets.h:28
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
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:52
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:63
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:215
value_sett::output
void output(const namespacet &ns, std::ostream &out) const
Pretty-print this value-set.
Definition: value_set.cpp:103
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
symbolt
Symbol table entry.
Definition: symbol.h:27
symex_dereference_statet::goto_symex
goto_symext & goto_symex
Definition: symex_dereference_state.h:32
symbol_table.h
Author: Diffblue Ltd.
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40