Skip to content

Commit 2ae3d87

Browse files
ChuyueSunChuyueSun
authored
add scoped vector unit test (#7307)
* add scoped vector unit test * fix dlist tests * add new scoped vector invariants
1 parent 2ce89e5 commit 2ae3d87

File tree

5 files changed

+180
-44
lines changed

5 files changed

+180
-44
lines changed

‎src/test/CMakeLists.txt

+1
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,7 @@ add_executable(test-z3
106106
sat_lookahead.cpp
107107
sat_user_scope.cpp
108108
scoped_timer.cpp
109+
scoped_vector.cpp
109110
simple_parser.cpp
110111
simplex.cpp
111112
simplifier.cpp

‎src/test/dlist.cpp

+38-41
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ Module Name:
1515
1616
--*/
1717

18-
#include <cassert>
1918
#include <iostream>
2019
#include "util/dlist.h"
2120

@@ -30,38 +29,38 @@ class TestNode : public dll_base<TestNode> {
3029
// Test the prev() method
3130
void test_prev() {
3231
TestNode node(1);
33-
assert(node.prev() == &node);
32+
SASSERT(node.prev() == &node);
3433
std::cout << "test_prev passed." << std::endl;
3534
}
3635

3736
// Test the next() method
3837
void test_next() {
3938
TestNode node(1);
40-
assert(node.next() == &node);
39+
SASSERT(node.next() == &node);
4140
std::cout << "test_next passed." << std::endl;
4241
}
4342

4443
// Test the const prev() method
4544
void test_const_prev() {
4645
const TestNode node(1);
47-
assert(node.prev() == &node);
46+
SASSERT(node.prev() == &node);
4847
std::cout << "test_const_prev passed." << std::endl;
4948
}
5049

5150
// Test the const next() method
5251
void test_const_next() {
5352
const TestNode node(1);
54-
assert(node.next() == &node);
53+
SASSERT(node.next() == &node);
5554
std::cout << "test_const_next passed." << std::endl;
5655
}
5756

5857
// Test the init() method
5958
void test_init() {
6059
TestNode node(1);
6160
node.init(&node);
62-
assert(node.next() == &node);
63-
assert(node.prev() == &node);
64-
assert(node.invariant());
61+
SASSERT(node.next() == &node);
62+
SASSERT(node.prev() == &node);
63+
SASSERT(node.invariant());
6564
std::cout << "test_init passed." << std::endl;
6665
}
6766

@@ -71,10 +70,10 @@ void test_pop() {
7170
TestNode node1(1);
7271
TestNode::push_to_front(list, &node1);
7372
TestNode* popped = TestNode::pop(list);
74-
assert(popped == &node1);
75-
assert(list == nullptr);
76-
assert(popped->next() == popped);
77-
assert(popped->prev() == popped);
73+
SASSERT(popped == &node1);
74+
SASSERT(list == nullptr);
75+
SASSERT(popped->next() == popped);
76+
SASSERT(popped->prev() == popped);
7877
std::cout << "test_pop passed." << std::endl;
7978
}
8079

@@ -83,12 +82,12 @@ void test_insert_after() {
8382
TestNode node1(1);
8483
TestNode node2(2);
8584
node1.insert_after(&node2);
86-
assert(node1.next() == &node2);
87-
assert(node2.prev() == &node1);
88-
assert(node1.prev() == &node2);
89-
assert(node2.next() == &node1);
90-
assert(node1.invariant());
91-
assert(node2.invariant());
85+
SASSERT(node1.next() == &node2);
86+
SASSERT(node2.prev() == &node1);
87+
SASSERT(node1.prev() == &node2);
88+
SASSERT(node2.next() == &node1);
89+
SASSERT(node1.invariant());
90+
SASSERT(node2.invariant());
9291
std::cout << "test_insert_after passed." << std::endl;
9392
}
9493

@@ -97,12 +96,12 @@ void test_insert_before() {
9796
TestNode node1(1);
9897
TestNode node2(2);
9998
node1.insert_before(&node2);
100-
assert(node1.prev() == &node2);
101-
assert(node2.next() == &node1);
102-
assert(node1.next() == &node2);
103-
assert(node2.prev() == &node1);
104-
assert(node1.invariant());
105-
assert(node2.invariant());
99+
SASSERT(node1.prev() == &node2);
100+
SASSERT(node2.next() == &node1);
101+
SASSERT(node1.next() == &node2);
102+
SASSERT(node2.prev() == &node1);
103+
SASSERT(node1.invariant());
104+
SASSERT(node2.invariant());
106105
std::cout << "test_insert_before passed." << std::endl;
107106
}
108107

@@ -114,11 +113,9 @@ void test_remove_from() {
114113
TestNode::push_to_front(list, &node1);
115114
TestNode::push_to_front(list, &node2);
116115
TestNode::remove_from(list, &node1);
117-
assert(list == &node2);
118-
assert(node2.next() == &node2);
119-
assert(node2.prev() == &node2);
120-
assert(node1.next() == &node1);
121-
assert(node1.prev() == &node1);
116+
SASSERT(list == &node2);
117+
SASSERT(node2.next() == &node2);
118+
SASSERT(node2.prev() == &node2);
122119
std::cout << "test_remove_from passed." << std::endl;
123120
}
124121

@@ -127,30 +124,30 @@ void test_push_to_front() {
127124
TestNode* list = nullptr;
128125
TestNode node1(1);
129126
TestNode::push_to_front(list, &node1);
130-
assert(list == &node1);
131-
assert(node1.next() == &node1);
132-
assert(node1.prev() == &node1);
127+
SASSERT(list == &node1);
128+
SASSERT(node1.next() == &node1);
129+
SASSERT(node1.prev() == &node1);
133130
std::cout << "test_push_to_front passed." << std::endl;
134131
}
135132

136133
// Test the detach() method
137134
void test_detach() {
138135
TestNode node(1);
139136
TestNode::detach(&node);
140-
assert(node.next() == &node);
141-
assert(node.prev() == &node);
142-
assert(node.invariant());
137+
SASSERT(node.next() == &node);
138+
SASSERT(node.prev() == &node);
139+
SASSERT(node.invariant());
143140
std::cout << "test_detach passed." << std::endl;
144141
}
145142

146143
// Test the invariant() method
147144
void test_invariant() {
148145
TestNode node1(1);
149-
assert(node1.invariant());
146+
SASSERT(node1.invariant());
150147
TestNode node2(2);
151148
node1.insert_after(&node2);
152-
assert(node1.invariant());
153-
assert(node2.invariant());
149+
SASSERT(node1.invariant());
150+
SASSERT(node2.invariant());
154151
std::cout << "test_invariant passed." << std::endl;
155152
}
156153

@@ -161,10 +158,10 @@ void test_contains() {
161158
TestNode node2(2);
162159
TestNode::push_to_front(list, &node1);
163160
TestNode::push_to_front(list, &node2);
164-
assert(TestNode::contains(list, &node1));
165-
assert(TestNode::contains(list, &node2));
161+
SASSERT(TestNode::contains(list, &node1));
162+
SASSERT(TestNode::contains(list, &node2));
166163
TestNode node3(3);
167-
assert(!TestNode::contains(list, &node3));
164+
SASSERT(!TestNode::contains(list, &node3));
168165
std::cout << "test_contains passed." << std::endl;
169166
}
170167

‎src/test/main.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -269,4 +269,5 @@ int main(int argc, char ** argv) {
269269
TST(euf_bv_plugin);
270270
TST(euf_arith_plugin);
271271
TST(sls_test);
272+
TST(scoped_vector);
272273
}

‎src/test/scoped_vector.cpp

+99
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
#include <iostream>
2+
#include "util/scoped_vector.h"
3+
4+
void test_push_back_and_access() {
5+
scoped_vector<int> sv;
6+
sv.push_back(10);
7+
8+
sv.push_back(20);
9+
10+
SASSERT(sv.size() == 2);
11+
SASSERT(sv[0] == 10);
12+
SASSERT(sv[1] == 20);
13+
14+
std::cout << "test_push_back_and_access passed." << std::endl;
15+
}
16+
17+
void test_scopes() {
18+
scoped_vector<int> sv;
19+
sv.push_back(10);
20+
sv.push_back(20);
21+
22+
sv.push_scope();
23+
sv.push_back(30);
24+
sv.push_back(40);
25+
26+
SASSERT(sv.size() == 4);
27+
SASSERT(sv[2] == 30);
28+
SASSERT(sv[3] == 40);
29+
30+
sv.pop_scope(1);
31+
32+
std::cout << "test_scopes passed." << std::endl;
33+
SASSERT(sv.size() == 2);
34+
SASSERT(sv[0] == 10);
35+
SASSERT(sv[1] == 20);
36+
37+
std::cout << "test_scopes passed." << std::endl;
38+
}
39+
40+
void test_set() {
41+
scoped_vector<int> sv;
42+
sv.push_back(10);
43+
sv.push_back(20);
44+
45+
sv.set(0, 30);
46+
sv.set(1, 40);
47+
48+
SASSERT(sv.size() == 2);
49+
SASSERT(sv[0] == 30);
50+
SASSERT(sv[1] == 40);
51+
52+
sv.push_scope();
53+
sv.set(0, 50);
54+
SASSERT(sv[0] == 50);
55+
sv.pop_scope(1);
56+
SASSERT(sv[0] == 30);
57+
58+
std::cout << "test_set passed." << std::endl;
59+
}
60+
61+
void test_pop_back() {
62+
scoped_vector<int> sv;
63+
sv.push_back(10);
64+
sv.push_back(20);
65+
66+
SASSERT(sv.size() == 2);
67+
sv.pop_back();
68+
SASSERT(sv.size() == 1);
69+
SASSERT(sv[0] == 10);
70+
sv.pop_back();
71+
SASSERT(sv.size() == 0);
72+
73+
std::cout << "test_pop_back passed." << std::endl;
74+
}
75+
76+
void test_erase_and_swap() {
77+
scoped_vector<int> sv;
78+
sv.push_back(10);
79+
sv.push_back(20);
80+
sv.push_back(30);
81+
82+
sv.erase_and_swap(1);
83+
84+
SASSERT(sv.size() == 2);
85+
SASSERT(sv[0] == 10);
86+
SASSERT(sv[1] == 30);
87+
88+
std::cout << "test_erase_and_swap passed." << std::endl;
89+
}
90+
91+
void tst_scoped_vector() {
92+
test_push_back_and_access();
93+
test_scopes();
94+
test_set();
95+
test_pop_back();
96+
test_erase_and_swap();
97+
98+
std::cout << "All tests passed." << std::endl;
99+
}

‎src/util/scoped_vector.h

+41-3
Original file line numberDiff line numberDiff line change
@@ -176,8 +176,46 @@ class scoped_vector {
176176
}
177177

178178
bool invariant() const {
179-
return
180-
m_size <= m_elems.size() &&
181-
m_elems_start <= m_elems.size();
179+
180+
181+
if (!(m_size <= m_elems.size() && m_elems_start <= m_elems.size()))
182+
return false;
183+
184+
// Check that source and destination trails have the same length.
185+
if (m_src.size() != m_dst.size())
186+
return false;
187+
// The size of m_src, m_dst, and m_src_lim should be consistent with the scope stack.
188+
if (m_src_lim.size() != m_sizes.size() || m_src.size() != m_dst.size())
189+
return false;
190+
191+
// m_elems_lim stores the past sizes of m_elems for each scope. Each element in m_elems_lim should be
192+
// within bounds and in non-decreasing order.
193+
for (unsigned i = 1; i < m_elems_lim.size(); ++i) {
194+
if (m_elems_lim[i - 1] > m_elems_lim[i]) return false;
195+
}
196+
197+
198+
// m_sizes tracks the size of the vector at each scope level.
199+
// Each element in m_sizes should be non-decreasing and within the size of m_elems.
200+
for (unsigned i = 1; i < m_sizes.size(); ++i) {
201+
if (m_sizes[i - 1] > m_sizes[i])
202+
return false;
203+
}
204+
205+
// The m_src and m_dst vectors should have the same size and should contain valid indices.
206+
if (m_src.size() != m_dst.size()) return false;
207+
for (unsigned i = 0; i < m_src.size(); ++i) {
208+
if (m_src[i] >= m_index.size() || m_dst[i] >= m_elems.size()) return false;
209+
}
210+
211+
212+
// The size of m_src_lim should be less than or equal to the size of m_sizes and store valid indices.
213+
if (m_src_lim.size() > m_sizes.size()) return false;
214+
for (unsigned elem : m_src_lim) {
215+
if (elem > m_src.size()) return false;
216+
}
217+
218+
return true;
219+
182220
}
183221
};

0 commit comments

Comments
 (0)