Skip to content

Commit 694d646

Browse files
tautschnigtautschnig
committed
Field-sensitive level-2 SSA renaming
- Currently for structs only, extension to arrays pending
1 parent f14d301 commit 694d646

14 files changed

+461
-38
lines changed

‎regression/cbmc/Struct_Propagation1/main.c

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
struct S
2+
{
3+
int v;
4+
struct Inner
5+
{
6+
int x;
7+
} inner;
8+
};
9+
10+
struct S works;
11+
12+
int main()
13+
{
14+
struct S fails;
15+
16+
works.v=2;
17+
fails.v=2;
18+
19+
while(works.v>0)
20+
--(works.v);
21+
22+
while(fails.v>0)
23+
--(fails.v);
24+
25+
__CPROVER_assert(works.inner.x==0, "");
26+
27+
_Bool b;
28+
if(b)
29+
{
30+
struct S s={ 42, { 42 } };
31+
}
32+
33+
return 0;
34+
}

‎regression/cbmc/Struct_Propagation1/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--unwind 5
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
\(Starting CEGAR Loop\|VCC(s), 0 remaining after simplification$\)
8+
--
9+
^warning: ignoring

‎src/goto-symex/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ SRC = symex_target.cpp symex_target_equation.cpp goto_symex.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 \
11-
memory_model_tso.cpp memory_model_pso.cpp substitute.cpp
11+
memory_model_tso.cpp memory_model_pso.cpp substitute.cpp field_sensitivity.cpp
1212

1313
INCLUDES= -I ..
1414

‎src/goto-symex/field_sensitivity.cpp

Lines changed: 254 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,254 @@
1+
/*******************************************************************\
2+
3+
Module: Field-sensitive SSA
4+
5+
Author: Michael Tautschnig, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include <util/simplify_expr.h>
10+
#include <util/std_expr.h>
11+
12+
#include "symex_target.h"
13+
#include "goto_symex_state.h"
14+
15+
#include "field_sensitivity.h"
16+
17+
/*******************************************************************\
18+
19+
Function: field_sensitivityt::operator()
20+
21+
Inputs:
22+
23+
Outputs:
24+
25+
Purpose:
26+
27+
\*******************************************************************/
28+
29+
void field_sensitivityt::operator()(
30+
const namespacet &ns,
31+
exprt &expr,
32+
bool write) const
33+
{
34+
#if 1
35+
if(expr.id()!=ID_address_of)
36+
Forall_operands(it, expr)
37+
operator()(ns, *it, write);
38+
39+
if(expr.id()==ID_symbol &&
40+
expr.get_bool(ID_C_SSA_symbol) &&
41+
!write)
42+
{
43+
ssa_exprt ssa=to_ssa_expr(expr);
44+
get_fields(ns, ssa, expr);
45+
}
46+
else if(!write &&
47+
expr.id()==ID_member &&
48+
to_member_expr(expr).struct_op().id()==ID_struct)
49+
{
50+
simplify(expr, ns);
51+
}
52+
else if(write && expr.id()==ID_member)
53+
{
54+
member_exprt &member=to_member_expr(expr);
55+
56+
if(member.struct_op().id()==ID_symbol &&
57+
member.struct_op().get_bool(ID_C_SSA_symbol) &&
58+
ns.follow(member.struct_op().type()).id()==ID_struct)
59+
{
60+
ssa_exprt tmp=to_ssa_expr(member.struct_op());
61+
62+
member.struct_op()=tmp.get_original_expr();
63+
64+
tmp.type()=member.type();
65+
tmp.set(ID_expression, member);
66+
tmp.update_identifier();
67+
68+
expr.swap(tmp);
69+
}
70+
}
71+
#endif
72+
}
73+
74+
/*******************************************************************\
75+
76+
Function: field_sensitivityt::get_fields
77+
78+
Inputs:
79+
80+
Outputs:
81+
82+
Purpose:
83+
84+
\*******************************************************************/
85+
86+
void field_sensitivityt::get_fields(
87+
const namespacet &ns,
88+
const ssa_exprt &ssa_expr,
89+
exprt &dest) const
90+
{
91+
#if 1
92+
if(ns.follow(ssa_expr.type()).id()==ID_struct)
93+
{
94+
const exprt &struct_op=ssa_expr.get_original_expr();
95+
96+
const struct_typet &type=
97+
to_struct_type(ns.follow(ssa_expr.type()));
98+
99+
const struct_union_typet::componentst &components=
100+
type.components();
101+
102+
dest=struct_exprt(ssa_expr.type());
103+
dest.reserve_operands(components.size());
104+
105+
for(struct_union_typet::componentst::const_iterator
106+
it=components.begin();
107+
it!=components.end();
108+
++it)
109+
{
110+
member_exprt member(struct_op, it->get_name(), it->type());
111+
112+
ssa_exprt tmp=ssa_expr;
113+
114+
tmp.type()=member.type();
115+
tmp.set(ID_expression, member);
116+
tmp.update_identifier();
117+
118+
exprt tmp_dest;
119+
get_fields(ns, tmp, tmp_dest);
120+
dest.copy_to_operands(tmp_dest);
121+
}
122+
}
123+
else
124+
#endif
125+
dest=ssa_expr;
126+
}
127+
128+
/*******************************************************************\
129+
130+
Function: field_sensitivityt::field_assignments
131+
132+
Inputs:
133+
134+
Outputs:
135+
136+
Purpose:
137+
138+
\*******************************************************************/
139+
140+
void field_sensitivityt::field_assignments(
141+
const namespacet &ns,
142+
goto_symex_statet &state,
143+
symex_targett &target,
144+
const exprt &lhs) const
145+
{
146+
exprt lhs_fs=lhs;
147+
operator()(ns, lhs_fs, false);
148+
149+
field_assignments_rec(ns, state, target, lhs_fs, lhs);
150+
}
151+
152+
/*******************************************************************\
153+
154+
Function: field_sensitivityt::field_assignments_rec
155+
156+
Inputs:
157+
158+
Outputs:
159+
160+
Purpose:
161+
162+
\*******************************************************************/
163+
164+
void field_sensitivityt::field_assignments_rec(
165+
const namespacet &ns,
166+
goto_symex_statet &state,
167+
symex_targett &target,
168+
const exprt &lhs_fs,
169+
const exprt &lhs) const
170+
{
171+
if(lhs==lhs_fs)
172+
return;
173+
else if(lhs_fs.id()==ID_symbol &&
174+
lhs_fs.get_bool(ID_C_SSA_symbol))
175+
{
176+
exprt ssa_rhs=lhs;
177+
178+
state.rename(ssa_rhs, ns);
179+
simplify(ssa_rhs, ns);
180+
181+
ssa_exprt ssa_lhs=to_ssa_expr(lhs_fs);
182+
state.assignment(ssa_lhs, ssa_rhs, ns, true);
183+
184+
// do the assignment
185+
target.assignment(
186+
state.guard.as_expr(),
187+
ssa_lhs,
188+
ssa_lhs, ssa_lhs.get_original_expr(),
189+
ssa_rhs,
190+
state.source,
191+
symex_targett::STATE);
192+
}
193+
else if(ns.follow(lhs.type()).id()==ID_struct)
194+
{
195+
const struct_typet &type=
196+
to_struct_type(ns.follow(lhs.type()));
197+
198+
const struct_union_typet::componentst &components=
199+
type.components();
200+
201+
assert(components.empty() ||
202+
(lhs_fs.has_operands() &&
203+
lhs_fs.operands().size()==components.size()));
204+
205+
unsigned number=0;
206+
for(struct_union_typet::componentst::const_iterator
207+
it=components.begin();
208+
it!=components.end();
209+
++it, ++number)
210+
{
211+
member_exprt member_rhs(lhs, it->get_name(), it->type());
212+
exprt member_lhs=lhs_fs.operands()[number];
213+
214+
field_assignments_rec(ns, state, target, member_lhs, member_rhs);
215+
}
216+
}
217+
else if(lhs_fs.has_operands())
218+
{
219+
assert(lhs.has_operands() &&
220+
lhs_fs.operands().size()==lhs.operands().size());
221+
222+
exprt::operandst::const_iterator fs_it=lhs_fs.operands().begin();
223+
for(exprt::operandst::const_iterator it=lhs.operands().begin();
224+
it!=lhs.operands().end();
225+
++it, ++fs_it)
226+
field_assignments_rec(ns, state, target, *fs_it, *it);
227+
}
228+
else
229+
{
230+
assert(false);
231+
}
232+
}
233+
234+
/*******************************************************************\
235+
236+
Function: field_sensitivityt::is_indivisible
237+
238+
Inputs:
239+
240+
Outputs:
241+
242+
Purpose:
243+
244+
\*******************************************************************/
245+
246+
bool field_sensitivityt::is_indivisible(
247+
const namespacet &ns,
248+
const ssa_exprt &expr) const
249+
{
250+
exprt tmp;
251+
get_fields(ns, expr, tmp);
252+
253+
return expr==tmp;
254+
}

‎src/goto-symex/field_sensitivity.h

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
/*******************************************************************\
2+
3+
Module: Field-sensitive SSA
4+
5+
Author: Michael Tautschnig, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_FIELD_SENSITIVITY_H
10+
#define CPROVER_FIELD_SENSITIVITY_H
11+
12+
class exprt;
13+
class ssa_exprt;
14+
class namespacet;
15+
class goto_symex_statet;
16+
class symex_targett;
17+
18+
/*! \brief Control granularity of object accesses
19+
*/
20+
class field_sensitivityt
21+
{
22+
public:
23+
void operator()(
24+
const namespacet &ns,
25+
exprt &expr,
26+
bool write) const;
27+
28+
void get_fields(
29+
const namespacet &ns,
30+
const ssa_exprt &ssa_expr,
31+
exprt &dest) const;
32+
33+
void field_assignments(
34+
const namespacet &ns,
35+
goto_symex_statet &state,
36+
symex_targett &target,
37+
const exprt &lhs) const;
38+
39+
bool is_indivisible(
40+
const namespacet &ns,
41+
const ssa_exprt &expr) const;
42+
43+
private:
44+
void field_assignments_rec(
45+
const namespacet &ns,
46+
goto_symex_statet &state,
47+
symex_targett &target,
48+
const exprt &lhs_fs,
49+
const exprt &lhs) const;
50+
};
51+
52+
#endif

‎src/goto-symex/goto_symex_state.cpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -639,6 +639,10 @@ bool goto_symex_statet::l2_thread_read_encoding(
639639
!dirty->is_dirty(obj_identifier)))
640640
return false;
641641

642+
// is it an indivisible object being accessed?
643+
if(!field_sensitivity.is_indivisible(ns, expr))
644+
return false;
645+
642646
ssa_exprt ssa_l1=expr;
643647
ssa_l1.remove_level_2();
644648
const irep_idt &l1_identifier=ssa_l1.get_identifier();
@@ -793,6 +797,10 @@ bool goto_symex_statet::l2_thread_write_encoding(
793797
(!ns.lookup(obj_identifier).is_shared() &&
794798
!dirty->is_dirty(obj_identifier)))
795799
return false; // not shared
800+
801+
// is it an indivisible object being accessed?
802+
if(!field_sensitivity.is_indivisible(ns, expr))
803+
return false;
796804

797805
// see whether we are within an atomic section
798806
if(atomic_section_id!=0)

‎src/goto-symex/goto_symex_state.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
2020
#include <goto-programs/goto_functions.h>
2121

2222
#include "symex_target.h"
23+
#include "field_sensitivity.h"
2324

2425
class dirtyt;
2526

@@ -345,6 +346,7 @@ class goto_symex_statet
345346
std::set<unsigned> cex_graph_nodes;
346347
bool cex_started;
347348
const dirtyt * dirty;
349+
field_sensitivityt field_sensitivity;
348350
};
349351

350352
#endif

0 commit comments

Comments
 (0)