Skip to content

Commit ee5a025

Browse files
author
kroening
committed
ssa_exprt now gets its own header file
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4651 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
1 parent c84fb12 commit ee5a025

File tree

5 files changed

+237
-213
lines changed

5 files changed

+237
-213
lines changed

‎src/goto-symex/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ SRC = symex_target.cpp symex_target_equation.cpp goto_symex.cpp \
44
symex_goto.cpp symex_builtin_functions.cpp slice.cpp symex_other.cpp \
55
slice_by_trace.cpp symex_decl.cpp symex_dead.cpp rewrite_union.cpp \
66
precondition.cpp postcondition.cpp symex_clean_expr.cpp \
7-
symex_dereference_state.cpp auto_objects.cpp \
7+
symex_dereference_state.cpp auto_objects.cpp ssa_expr.cpp \
88
symex_catch.cpp symex_start_thread.cpp symex_assign.cpp \
99
symex_throw.cpp symex_atomic_section.cpp memory_model.cpp \
1010
memory_model_sc.cpp partial_order_concurrency.cpp \

‎src/goto-symex/ssa_expr.cpp

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include <sstream>
10+
11+
#include <util/arith_tools.h>
12+
13+
#include "ssa_expr.h"
14+
15+
/*******************************************************************\
16+
17+
Function: build_identifier_rec
18+
19+
Inputs:
20+
21+
Outputs:
22+
23+
Purpose:
24+
25+
\*******************************************************************/
26+
27+
static void build_ssa_identifier_rec(
28+
const exprt &expr,
29+
const irep_idt &l0,
30+
const irep_idt &l1,
31+
std::ostream &os)
32+
{
33+
if(expr.id()==ID_member)
34+
{
35+
const member_exprt &member=to_member_expr(expr);
36+
37+
build_ssa_identifier_rec(member.struct_op(), l0, l1, os);
38+
39+
os << '.' << member.get_component_name();
40+
}
41+
else if(expr.id()==ID_index)
42+
{
43+
const index_exprt &index=to_index_expr(expr);
44+
45+
build_ssa_identifier_rec(index.array(), l0, l1, os);
46+
47+
mp_integer idx;
48+
if(to_integer(to_constant_expr(index.index()), idx))
49+
assert(false);
50+
51+
os << '[' << idx << ']';
52+
}
53+
else if(expr.id()==ID_symbol)
54+
{
55+
os << to_symbol_expr(expr).get_identifier();
56+
57+
if(!l0.empty())
58+
os << '!' << l0;
59+
60+
if(!l1.empty())
61+
os << '@' << l1;
62+
}
63+
else
64+
assert(false);
65+
}
66+
67+
/*******************************************************************\
68+
69+
Function: ssa_exprt::update_identifier
70+
71+
Inputs:
72+
73+
Outputs:
74+
75+
Purpose:
76+
77+
\*******************************************************************/
78+
79+
void ssa_exprt::update_identifier()
80+
{
81+
std::ostringstream oss;
82+
83+
const irep_idt &l0=get_level_0();
84+
const irep_idt &l1=get_level_1();
85+
const irep_idt &l2=get_level_2();
86+
87+
build_ssa_identifier_rec(get_original_expr(), l0, l1, oss);
88+
89+
if(!l2.empty())
90+
oss << '#' << l2;
91+
92+
set_identifier(oss.str());
93+
}

‎src/goto-symex/ssa_expr.h

Lines changed: 143 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,143 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_GOTO_SYMEX_SSA_EXPR_H
10+
#define CPROVER_GOTO_SYMEX_SSA_EXPR_H
11+
12+
#include <util/std_expr.h>
13+
14+
/*! \brief Expression providing an SSA-renamed symbol of expressions
15+
*/
16+
class ssa_exprt:public symbol_exprt
17+
{
18+
public:
19+
inline ssa_exprt()
20+
{
21+
set(ID_C_SSA_symbol, true);
22+
}
23+
24+
/*! \brief Constructor
25+
* \param expr Expression to be converted to SSA symbol
26+
*/
27+
inline explicit ssa_exprt(const exprt &expr):
28+
symbol_exprt(expr.type())
29+
{
30+
set(ID_C_SSA_symbol, true);
31+
add(ID_expression, expr);
32+
update_identifier();
33+
}
34+
35+
inline const exprt &get_original_expr() const
36+
{
37+
return static_cast<const exprt &>(find(ID_expression));
38+
}
39+
40+
inline const irep_idt &get_object_name() const
41+
{
42+
object_descriptor_exprt ode;
43+
ode.object()=get_original_expr();
44+
return to_symbol_expr(ode.root_object()).get_identifier();
45+
}
46+
47+
inline const irep_idt get_l1_object_identifier() const
48+
{
49+
object_descriptor_exprt ode;
50+
ode.object()=get_original_expr();
51+
52+
ssa_exprt root(ode.root_object());
53+
root.set(ID_L0, get(ID_L0));
54+
root.set(ID_L1, get(ID_L1));
55+
root.update_identifier();
56+
57+
return root.get_identifier();
58+
}
59+
60+
inline const irep_idt get_original_name() const
61+
{
62+
ssa_exprt o(get_original_expr());
63+
return o.get_identifier();
64+
}
65+
66+
inline void set_level_0(unsigned i)
67+
{
68+
set(ID_L0, i);
69+
update_identifier();
70+
}
71+
72+
inline void set_level_1(unsigned i)
73+
{
74+
set(ID_L1, i);
75+
update_identifier();
76+
}
77+
78+
inline void set_level_2(unsigned i)
79+
{
80+
set(ID_L2, i);
81+
update_identifier();
82+
}
83+
84+
inline void remove_level_2()
85+
{
86+
remove(ID_L2);
87+
update_identifier();
88+
}
89+
90+
inline const irep_idt get_level_0() const
91+
{
92+
return get(ID_L0);
93+
}
94+
95+
inline const irep_idt get_level_1() const
96+
{
97+
return get(ID_L1);
98+
}
99+
100+
inline const irep_idt get_level_2() const
101+
{
102+
return get(ID_L2);
103+
}
104+
105+
void update_identifier();
106+
};
107+
108+
/*! \brief Cast a generic exprt to an \ref ssa_exprt
109+
*
110+
* This is an unchecked conversion. \a expr must be known to be \ref
111+
* ssa_exprt.
112+
*
113+
* \param expr Source expression
114+
* \return Object of type \ref ssa_exprt
115+
*
116+
* \ingroup gr_std_expr
117+
*/
118+
extern inline const ssa_exprt &to_ssa_expr(const exprt &expr)
119+
{
120+
assert(expr.id()==ID_symbol &&
121+
expr.get_bool(ID_C_SSA_symbol) &&
122+
!expr.has_operands());
123+
return static_cast<const ssa_exprt &>(expr);
124+
}
125+
126+
/*! \copydoc to_ssa_expr(const exprt &)
127+
* \ingroup gr_std_expr
128+
*/
129+
extern inline ssa_exprt &to_ssa_expr(exprt &expr)
130+
{
131+
assert(expr.id()==ID_symbol &&
132+
expr.get_bool(ID_C_SSA_symbol) &&
133+
!expr.has_operands());
134+
return static_cast<ssa_exprt &>(expr);
135+
}
136+
137+
extern inline bool is_ssa_expr(const exprt &expr)
138+
{
139+
return expr.id()==ID_symbol &&
140+
expr.get_bool(ID_C_SSA_symbol);
141+
}
142+
143+
#endif

‎src/util/std_expr.cpp

Lines changed: 0 additions & 83 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
#include <sstream>
109
#include <cassert>
1110

1211
#include "arith_tools.h"
@@ -15,8 +14,6 @@ Author: Daniel Kroening, [email protected]
1514
#include "namespace.h"
1615
#include "pointer_offset_size.h"
1716

18-
#include "arith_tools.h"
19-
2017
#include "std_expr.h"
2118

2219
/*******************************************************************\
@@ -91,86 +88,6 @@ exprt conjunction(const exprt::operandst &op)
9188

9289
/*******************************************************************\
9390
94-
Function: build_identifier_rec
95-
96-
Inputs:
97-
98-
Outputs:
99-
100-
Purpose:
101-
102-
\*******************************************************************/
103-
104-
static void build_ssa_identifier_rec(
105-
const exprt &expr,
106-
const irep_idt &l0,
107-
const irep_idt &l1,
108-
std::ostream &os)
109-
{
110-
if(expr.id()==ID_member)
111-
{
112-
const member_exprt &member=to_member_expr(expr);
113-
114-
build_ssa_identifier_rec(member.struct_op(), l0, l1, os);
115-
116-
os << '.' << member.get_component_name();
117-
}
118-
else if(expr.id()==ID_index)
119-
{
120-
const index_exprt &index=to_index_expr(expr);
121-
122-
build_ssa_identifier_rec(index.array(), l0, l1, os);
123-
124-
mp_integer idx;
125-
if(to_integer(to_constant_expr(index.index()), idx))
126-
assert(false);
127-
128-
os << '[' << idx << ']';
129-
}
130-
else if(expr.id()==ID_symbol)
131-
{
132-
os << to_symbol_expr(expr).get_identifier();
133-
134-
if(!l0.empty())
135-
os << '!' << l0;
136-
137-
if(!l1.empty())
138-
os << '@' << l1;
139-
}
140-
else
141-
assert(false);
142-
}
143-
144-
/*******************************************************************\
145-
146-
Function: ssa_exprt::update_identifier
147-
148-
Inputs:
149-
150-
Outputs:
151-
152-
Purpose:
153-
154-
\*******************************************************************/
155-
156-
void ssa_exprt::update_identifier()
157-
{
158-
std::ostringstream oss;
159-
160-
const irep_idt &l0=get_level_0();
161-
const irep_idt &l1=get_level_1();
162-
const irep_idt &l2=get_level_2();
163-
164-
build_ssa_identifier_rec(get_original_expr(), l0, l1, oss);
165-
166-
if(!l2.empty())
167-
oss << '#' << l2;
168-
169-
set_identifier(oss.str());
170-
}
171-
172-
/*******************************************************************\
173-
17491
Function: build_object_descriptor_rec
17592
17693
Inputs:

0 commit comments

Comments
 (0)