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 
16 #ifdef DEBUG
17 # include <iostream>
18 #endif
19 
34 const symbolt *
36 {
37  if(expr.id()==ID_symbol &&
38  expr.get_bool(ID_C_SSA_symbol))
39  {
40  const ssa_exprt &ssa_expr=to_ssa_expr(expr);
41  if(ssa_expr.get_original_expr().id()!=ID_symbol)
42  return nullptr;
43 
44  const symbolt &ptr_symbol=
45  ns.lookup(to_ssa_expr(expr).get_object_name());
46 
47  const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
48 
49  const symbolt *symbol;
50  if(!failed_symbol.empty() && !ns.lookup(failed_symbol, symbol))
51  {
52  symbolt sym=*symbol;
53  symbolt *sym_ptr=nullptr;
54  const ssa_exprt sym_expr =
55  state.rename_ssa<L1>(ssa_exprt{sym.symbol_expr()}, ns).get();
56  sym.name = sym_expr.get_identifier();
57  state.symbol_table.move(sym, sym_ptr);
58  return sym_ptr;
59  }
60  }
61  else if(expr.id()==ID_symbol)
62  {
63  const symbolt &ptr_symbol=
64  ns.lookup(to_symbol_expr(expr).get_identifier());
65 
66  const irep_idt &failed_symbol = ptr_symbol.type.get(ID_C_failed_symbol);
67 
68  const symbolt *symbol;
69  if(!failed_symbol.empty() && !ns.lookup(failed_symbol, symbol))
70  {
71  symbolt sym=*symbol;
72  symbolt *sym_ptr=nullptr;
73  const ssa_exprt sym_expr =
74  state.rename_ssa<L1>(ssa_exprt{sym.symbol_expr()}, ns).get();
75  sym.name = sym_expr.get_identifier();
76  state.symbol_table.move(sym, sym_ptr);
77  return sym_ptr;
78  }
79  }
80 
81  return nullptr;
82 }
83 
86  const exprt &expr,
87  value_setst::valuest &value_set) const
88 {
89  state.value_set.get_value_set(expr, value_set, ns);
90 
91 #ifdef DEBUG
92  std::cout << "symex_dereference_statet state.value_set={\n";
93  state.value_set.output(ns, std::cout, " - ");
94  std::cout << "}" << std::endl;
95 #endif
96 
97 #if 0
98  std::cout << "E: " << from_expr(goto_symex.ns, irep_idt(), expr) << '\n';
99 #endif
100 
101 #if 0
102  std::cout << "**************************\n";
103  for(value_setst::valuest::const_iterator it=value_set.begin();
104  it!=value_set.end();
105  it++)
106  std::cout << from_expr(goto_symex.ns, irep_idt(), *it) << '\n';
107  std::cout << "**************************\n";
108 #endif
109 }
110 
112 std::vector<exprt>
114 {
115  return state.value_set.get_value_set(expr, ns);
116 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
value_sett::get_value_set
void get_value_set(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:359
symex_dereference_statet::state
goto_symext::statet & state
Definition: symex_dereference_state.h:34
L1
@ L1
Definition: renamed.h:18
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
symex_dereference_statet::get_or_create_failed_symbol
const symbolt * get_or_create_failed_symbol(const exprt &expr) override
Get or create a failed symbol for the given pointer-typed expression.
Definition: symex_dereference_state.cpp:35
exprt
Base class for all expressions.
Definition: expr.h:53
goto_symex_statet::rename_ssa
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
symex_dereference_state.h
Symbolic Execution of ANSI-C.
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
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:148
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
value_sett::output
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
Definition: value_set.cpp:144
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
symex_dereference_statet::ns
const namespacet & ns
Definition: symex_dereference_state.h:35
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
dstringt::empty
bool empty() const
Definition: dstring.h:88
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:69
symex_dereference_statet::get_value_set
void get_value_set(const exprt &expr, value_setst::valuest &value_set) const override
Just forwards a value-set query to state.value_set
Definition: symex_dereference_state.cpp:85
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table.h
Author: Diffblue Ltd.
goto_statet::value_set
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Definition: goto_state.h:43
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