Skip to content

Commit 0902ae7

Browse files
NathanJPhillipsNathanJPhillips
committed
Tests to demonstrate expected sharing behaviour of irept
1 parent 2239ec1 commit 0902ae7

File tree

2 files changed

+203
-0
lines changed

2 files changed

+203
-0
lines changed

Diff for: ‎unit/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ SRC += unit_tests.cpp \
4646
util/expr_cast/expr_cast.cpp \
4747
util/expr_iterator.cpp \
4848
util/irep.cpp \
49+
util/irep_sharing.cpp \
4950
util/message.cpp \
5051
util/parameter_indices.cpp \
5152
util/simplify_expr.cpp \

Diff for: ‎unit/util/irep_sharing.cpp

+202
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,202 @@
1+
/// Author: Diffblue Ltd.
2+
3+
/// \file Tests that irep sharing works correctly
4+
5+
#include <testing-utils/catch.hpp>
6+
#include <util/irep.h>
7+
8+
#ifdef SHARING
9+
10+
SCENARIO("irept_sharing_trade_offs", "[!mayfail][core][utils][irept]")
11+
{
12+
GIVEN("An irept created with move_to_sub")
13+
{
14+
irept test_irep(ID_1);
15+
irept test_subirep(ID_1);
16+
irept test_subsubirep(ID_1);
17+
test_subirep.move_to_sub(test_subsubirep);
18+
test_irep.move_to_sub(test_subirep);
19+
THEN("Calling read() on a copy should return object with the same address")
20+
{
21+
irept irep = test_irep;
22+
REQUIRE(&irep.read() == &test_irep.read());
23+
}
24+
THEN("Changing subs in the original using a reference taken before "
25+
"copying should not change them in the copy")
26+
{
27+
irept &sub = test_irep.get_sub()[0];
28+
irept irep = test_irep;
29+
sub.id(ID_0);
30+
REQUIRE(test_irep.get_sub()[0].id() == ID_0);
31+
REQUIRE(irep.get_sub()[0].id() == ID_1);
32+
}
33+
THEN("Holding a reference to a sub should not prevent sharing")
34+
{
35+
irept &sub = test_irep.get_sub()[0];
36+
irept irep = test_irep;
37+
REQUIRE(&irep.read() == &test_irep.read());
38+
sub = irept(ID_0);
39+
REQUIRE(irep.get_sub()[0].id() == test_irep.get_sub()[0].id());
40+
}
41+
}
42+
}
43+
44+
SCENARIO("irept_sharing", "[core][utils][irept]")
45+
{
46+
GIVEN("An irept created with move_to_sub")
47+
{
48+
irept test_irep(ID_1);
49+
irept test_subirep(ID_1);
50+
irept test_subsubirep(ID_1);
51+
test_subirep.move_to_sub(test_subsubirep);
52+
test_irep.move_to_sub(test_subirep);
53+
THEN("Copies of a copy should return object with the same address")
54+
{
55+
irept irep1 = test_irep;
56+
irept irep2 = irep1;
57+
REQUIRE(&irep1.read() == &irep2.read());
58+
}
59+
THEN("Changing subs in the original should not change them in a copy")
60+
{
61+
irept irep = test_irep;
62+
test_irep.get_sub()[0].id(ID_0);
63+
REQUIRE(irep.get_sub()[0].id() == ID_1);
64+
}
65+
THEN("Changing subs in a copy should not change them in the original")
66+
{
67+
irept irep = test_irep;
68+
irep.get_sub()[0].id(ID_0);
69+
REQUIRE(test_irep.get_sub()[0].id() == ID_1);
70+
REQUIRE(irep.get_sub()[0].id() == ID_0);
71+
}
72+
THEN("Getting a reference to a sub in a copy should break sharing")
73+
{
74+
irept irep = test_irep;
75+
irept &sub = irep.get_sub()[0];
76+
REQUIRE(&irep.read() != &test_irep.read());
77+
sub = irept(ID_0);
78+
REQUIRE(irep.get_sub()[0].id() != test_irep.get_sub()[0].id());
79+
}
80+
THEN(
81+
"Getting a reference to a sub in the original should break sharing")
82+
{
83+
irept irep = test_irep;
84+
irept &sub = test_irep.get_sub()[0];
85+
REQUIRE(&irep.read() != &test_irep.read());
86+
sub = irept(ID_0);
87+
REQUIRE(irep.get_sub()[0].id() != test_irep.get_sub()[0].id());
88+
}
89+
THEN("Changing an id in the original should break sharing")
90+
{
91+
irept irep = test_irep;
92+
test_irep.id(ID_0);
93+
REQUIRE(&irep.read() != &test_irep.read());
94+
REQUIRE(irep.id() != test_irep.id());
95+
}
96+
THEN("Changing an id should not prevent sharing")
97+
{
98+
test_irep.id(ID_0);
99+
irept irep = test_irep;
100+
REQUIRE(&irep.read() == &test_irep.read());
101+
}
102+
}
103+
}
104+
105+
#include <util/expr.h>
106+
107+
SCENARIO("exprt_sharing_trade_offs", "[!mayfail][core][utils][exprt]")
108+
{
109+
GIVEN("An expression created with move_to_operands")
110+
{
111+
exprt test_expr(ID_1);
112+
exprt test_subexpr(ID_1);
113+
exprt test_subsubexpr(ID_1);
114+
test_subexpr.move_to_operands(test_subsubexpr);
115+
test_expr.move_to_operands(test_subexpr);
116+
THEN("Calling read() on a copy should return object with the same address")
117+
{
118+
exprt expr = test_expr;
119+
REQUIRE(&expr.read() == &test_expr.read());
120+
}
121+
THEN("Changing operands in the original using a reference taken before "
122+
"copying should not change them in the copy")
123+
{
124+
exprt &operand = test_expr.op0();
125+
exprt expr = test_expr;
126+
operand.id(ID_0);
127+
REQUIRE(test_expr.op0().id() == ID_0);
128+
REQUIRE(expr.op0().id() == ID_1);
129+
}
130+
THEN("Holding a reference to an operand should not prevent sharing")
131+
{
132+
exprt &operand = test_expr.op0();
133+
exprt expr = test_expr;
134+
REQUIRE(&expr.read() == &test_expr.read());
135+
operand = exprt(ID_0);
136+
REQUIRE(expr.op0().id() == test_expr.op0().id());
137+
}
138+
}
139+
}
140+
141+
SCENARIO("exprt_sharing", "[core][utils][exprt]")
142+
{
143+
GIVEN("An expression created with move_to_operands")
144+
{
145+
exprt test_expr(ID_1);
146+
exprt test_subexpr(ID_1);
147+
exprt test_subsubexpr(ID_1);
148+
test_subexpr.move_to_operands(test_subsubexpr);
149+
test_expr.move_to_operands(test_subexpr);
150+
THEN("Copies of a copy should return object with the same address")
151+
{
152+
exprt expr1 = test_expr;
153+
exprt expr2 = expr1;
154+
REQUIRE(&expr1.read() == &expr2.read());
155+
}
156+
THEN("Changing operands in the original should not change them in a copy")
157+
{
158+
exprt expr = test_expr;
159+
test_expr.op0().id(ID_0);
160+
REQUIRE(expr.op0().id() == ID_1);
161+
}
162+
THEN("Changing operands in a copy should not change them in the original")
163+
{
164+
exprt expr = test_expr;
165+
expr.op0().id(ID_0);
166+
REQUIRE(test_expr.op0().id() == ID_1);
167+
REQUIRE(expr.op0().id() == ID_0);
168+
}
169+
THEN("Getting a reference to an operand in a copy should break sharing")
170+
{
171+
exprt expr = test_expr;
172+
exprt &operand = expr.op0();
173+
REQUIRE(&expr.read() != &test_expr.read());
174+
operand = exprt(ID_0);
175+
REQUIRE(expr.op0().id() != test_expr.op0().id());
176+
}
177+
THEN(
178+
"Getting a reference to an operand in the original should break sharing")
179+
{
180+
exprt expr = test_expr;
181+
exprt &operand = test_expr.op0();
182+
REQUIRE(&expr.read() != &test_expr.read());
183+
operand = exprt(ID_0);
184+
REQUIRE(expr.op0().id() != test_expr.op0().id());
185+
}
186+
THEN("Changing an id in the original should break sharing")
187+
{
188+
exprt expr = test_expr;
189+
test_expr.id(ID_0);
190+
REQUIRE(&expr.read() != &test_expr.read());
191+
REQUIRE(expr.id() != test_expr.id());
192+
}
193+
THEN("Changing an id should not prevent sharing")
194+
{
195+
test_expr.id(ID_0);
196+
exprt expr = test_expr;
197+
REQUIRE(&expr.read() == &test_expr.read());
198+
}
199+
}
200+
}
201+
202+
#endif

0 commit comments

Comments
 (0)