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