cprover
ssa_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "ssa_expr.h"
10 
11 #include <sstream>
12 #include <cassert>
13 
14 #include <util/arith_tools.h>
15 
22 static std::ostream &
23 initialize_ssa_identifier(std::ostream &os, const exprt &expr)
24 {
25  if(auto member = expr_try_dynamic_cast<member_exprt>(expr))
26  {
27  return initialize_ssa_identifier(os, member->struct_op())
28  << ".." << member->get_component_name();
29  }
30  if(auto index = expr_try_dynamic_cast<index_exprt>(expr))
31  {
32  const auto idx =
33  numeric_cast_v<mp_integer>(to_constant_expr(index->index()));
34  return initialize_ssa_identifier(os, index->array()) << "[[" << idx << "]]";
35  }
36  if(auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
37  return os << symbol->get_identifier();
38 
40 }
41 
42 ssa_exprt::ssa_exprt(const exprt &expr) : symbol_exprt(expr.type())
43 {
44  set(ID_C_SSA_symbol, true);
45  add(ID_expression, expr);
46  std::ostringstream os;
47  initialize_ssa_identifier(os, expr);
48  const std::string id = os.str();
49  set_identifier(id);
50  set(ID_L1_object_identifier, id);
51 }
52 
57 static void build_ssa_identifier_rec(
58  const exprt &expr,
59  const irep_idt &l0,
60  const irep_idt &l1,
61  const irep_idt &l2,
62  std::ostream &os,
63  std::ostream &l1_object_os)
64 {
65  if(expr.id()==ID_member)
66  {
67  const member_exprt &member=to_member_expr(expr);
68 
69  build_ssa_identifier_rec(member.struct_op(), l0, l1, l2, os, l1_object_os);
70 
71  os << ".." << member.get_component_name();
72  l1_object_os << ".." << member.get_component_name();
73  }
74  else if(expr.id()==ID_index)
75  {
76  const index_exprt &index=to_index_expr(expr);
77 
78  build_ssa_identifier_rec(index.array(), l0, l1, l2, os, l1_object_os);
79 
80  const mp_integer idx =
81  numeric_cast_v<mp_integer>(to_constant_expr(index.index()));
82  os << "[[" << idx << "]]";
83  l1_object_os << "[[" << idx << "]]";
84  }
85  else if(expr.id()==ID_symbol)
86  {
87  auto symid=to_symbol_expr(expr).get_identifier();
88  os << symid;
89  l1_object_os << symid;
90 
91  if(!l0.empty())
92  {
93  // Distinguish different threads of execution
94  os << '!' << l0;
95  l1_object_os << '!' << l0;
96  }
97 
98  if(!l1.empty())
99  {
100  // Distinguish different calls to the same function (~stack frame)
101  os << '@' << l1;
102  l1_object_os << '@' << l1;
103  }
104 
105  if(!l2.empty())
106  {
107  // Distinguish SSA steps for the same variable
108  os << '#' << l2;
109  }
110  }
111  else
112  UNREACHABLE;
113 }
114 
115 static std::pair<irep_idt, irep_idt> build_identifier(
116  const exprt &expr,
117  const irep_idt &l0,
118  const irep_idt &l1,
119  const irep_idt &l2)
120 {
121  std::ostringstream oss;
122  std::ostringstream l1_object_oss;
123 
124  build_ssa_identifier_rec(expr, l0, l1, l2, oss, l1_object_oss);
125 
126  return std::make_pair(irep_idt(oss.str()), irep_idt(l1_object_oss.str()));
127 }
128 
129 static void update_identifier(ssa_exprt &ssa)
130 {
131  const irep_idt &l0 = ssa.get_level_0();
132  const irep_idt &l1 = ssa.get_level_1();
133  const irep_idt &l2 = ssa.get_level_2();
134 
135  auto idpair = build_identifier(ssa.get_original_expr(), l0, l1, l2);
136  ssa.set_identifier(idpair.first);
137  ssa.set(ID_L1_object_identifier, idpair.second);
138 }
139 
140 void ssa_exprt::set_expression(const exprt &expr)
141 {
142  type() = expr.type();
143  add(ID_expression, expr);
144  ::update_identifier(*this);
145 }
146 
148 {
149  const exprt &original_expr = get_original_expr();
150 
151  if(original_expr.id() == ID_symbol)
152  return to_symbol_expr(original_expr).get_identifier();
153 
154  object_descriptor_exprt ode(original_expr);
155  return to_symbol_expr(ode.root_object()).get_identifier();
156 }
157 
159 {
161 
162  ssa_exprt root(ode.root_object());
163  if(!get_level_0().empty())
164  root.set(ID_L0, get(ID_L0));
165  if(!get_level_1().empty())
166  root.set(ID_L1, get(ID_L1));
167  ::update_identifier(root);
168 
169  return root;
170 }
171 
173 {
174 #if 0
175  return get_l1_object().get_identifier();
176 #else
177  // the above is the clean version, this is the fast one, using
178  // an identifier cached during build_identifier
179  return get(ID_L1_object_identifier);
180 #endif
181 }
182 
183 void ssa_exprt::set_level_0(std::size_t i)
184 {
185  set(ID_L0, i);
186  ::update_identifier(*this);
187 }
188 
189 void ssa_exprt::set_level_1(std::size_t i)
190 {
191  set(ID_L1, i);
192  ::update_identifier(*this);
193 }
194 
195 void ssa_exprt::set_level_2(std::size_t i)
196 {
197  set(ID_L2, i);
198  ::update_identifier(*this);
199 }
200 
202 {
203  remove(ID_L2);
205 }
206 
207 /* Used to determine whether or not an identifier can be built
208  * before trying and getting an exception */
209 bool ssa_exprt::can_build_identifier(const exprt &expr)
210 {
211  if(expr.id() == ID_symbol)
212  return true;
213  else if(expr.id() == ID_member)
214  return can_build_identifier(to_member_expr(expr).compound());
215  else if(expr.id() == ID_index)
216  return can_build_identifier(to_index_expr(expr).array());
217  else
218  return false;
219 }
220 
222 {
223  ::update_identifier(*this);
224 }
225 
227 {
228  ssa.remove_level_2();
229  return ssa;
230 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ssa_exprt::set_level_0
void set_level_0(std::size_t i)
arith_tools.h
ssa_exprt::remove_level_2
void remove_level_2()
ssa_exprt::get_level_0
const irep_idt get_level_0() const
Definition: ssa_expr.h:63
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1832
exprt
Base class for all expressions.
Definition: expr.h:53
ssa_exprt::get_object_name
irep_idt get_object_name() const
irep_idt
dstringt irep_idt
Definition: irep.h:32
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
ssa_exprt::set_level_1
void set_level_1(std::size_t i)
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:81
ssa_exprt::can_build_identifier
static bool can_build_identifier(const exprt &src)
Used to determine whether or not an identifier can be built before trying and getting an exception.
ssa_exprt::ssa_exprt
ssa_exprt(const exprt &expr)
Constructor.
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
ssa_exprt::get_l1_object
const ssa_exprt get_l1_object() const
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
ssa_exprt::get_level_2
const irep_idt get_level_2() const
Definition: ssa_expr.h:73
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
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
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:93
dstringt::empty
bool empty() const
Definition: dstring.h:88
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
ssa_expr.h
ssa_exprt::get_l1_object_identifier
const irep_idt get_l1_object_identifier() const
ssa_exprt::set_level_2
void set_level_2(std::size_t i)
ssa_exprt::set_expression
void set_expression(const exprt &expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
remove_level_2
ssa_exprt remove_level_2(ssa_exprt ssa)
ssa_exprt::update_identifier
void update_identifier()
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
ssa_exprt::get_level_1
const irep_idt get_level_1() const
Definition: ssa_expr.h:68
initialize_ssa_identifier
static std::ostream & initialize_ssa_identifier(std::ostream &os, const exprt &expr)
If expr is:
Definition: ssa_expr.cpp:23
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
index_exprt
Array index operator.
Definition: std_expr.h:1293
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:106
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939