Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Morgan Deters, Andres Noetzli
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Black box testing of cvc5::context::Context.
14 : : */
15 : :
16 : : #include <iostream>
17 : : #include <vector>
18 : :
19 : : #include "base/exception.h"
20 : : #include "context/cdlist.h"
21 : : #include "context/cdo.h"
22 : : #include "test_context.h"
23 : :
24 : : namespace cvc5::internal {
25 : :
26 : : using namespace context;
27 : :
28 : : namespace test {
29 : :
30 : : struct MyContextNotifyObj : public ContextNotifyObj
31 : : {
32 : 5 : MyContextNotifyObj(Context* context, bool pre)
33 : 5 : : ContextNotifyObj(context, pre), d_ncalls(0)
34 : : {
35 : 5 : }
36 : :
37 : 5 : ~MyContextNotifyObj() override {}
38 : :
39 : 9 : void contextNotifyPop() override { ++d_ncalls; }
40 : :
41 : : int32_t d_ncalls;
42 : : };
43 : :
44 : : class MyContextObj : public ContextObj
45 : : {
46 : : public:
47 : 5 : MyContextObj(Context* context, MyContextNotifyObj& n)
48 : 5 : : ContextObj(context), d_ncalls(0), d_nsaves(0), d_notify(n)
49 : : {
50 : 5 : }
51 : :
52 : 5 : ~MyContextObj() override { destroy(); }
53 : :
54 : 8 : ContextObj* save(ContextMemoryManager* pcmm) override
55 : : {
56 : 8 : ++d_nsaves;
57 : 8 : return new (pcmm) MyContextObj(*this);
58 : : }
59 : :
60 : 8 : void restore(ContextObj* contextObj) override
61 : : {
62 : 8 : d_ncalls = d_notify.d_ncalls;
63 : 8 : }
64 : :
65 : 8 : void makeCurrent() { ContextObj::makeCurrent(); }
66 : :
67 : : int32_t d_ncalls;
68 : : int32_t d_nsaves;
69 : :
70 : : private:
71 : 8 : MyContextObj(const MyContextObj& other)
72 : 8 : : ContextObj(other), d_ncalls(0), d_nsaves(0), d_notify(other.d_notify)
73 : : {
74 : 8 : }
75 : : MyContextNotifyObj& d_notify;
76 : : };
77 : :
78 : : class TestContextBlack : public TestContext
79 : : {
80 : : };
81 : :
82 : 2 : TEST_F(TestContextBlack, push_pop)
83 : : {
84 : : // Test what happens when the context is popped below 0
85 : : // the interface doesn't declare any exceptions
86 : 1 : d_context->push();
87 : 1 : d_context->pop();
88 : : #ifdef CVC5_ASSERTIONS
89 : 1 : ASSERT_DEATH(d_context->pop(), "Cannot pop below level 0");
90 : 1 : ASSERT_DEATH(d_context->pop(), "Cannot pop below level 0");
91 : : #endif /* CVC5_ASSERTIONS */
92 : : }
93 : :
94 : 2 : TEST_F(TestContextBlack, dtor)
95 : : {
96 : : // Destruction of ContextObj was broken in revision 324 (bug #45) when
97 : : // at a higher context level with an intervening modification.
98 : : // (The following caused a "pure virtual method called" error.)
99 : 1 : CDO<int32_t> i(d_context.get());
100 : 1 : d_context->push();
101 : 1 : i = 5;
102 : 1 : }
103 : :
104 : 2 : TEST_F(TestContextBlack, pre_post_notify)
105 : : {
106 : : // This is tricky; we want to detect if pre- and post-notifies are
107 : : // done correctly. For that, we have to use a special ContextObj,
108 : : // since that's the only thing that runs between pre- and post-.
109 : :
110 : 1 : MyContextNotifyObj a(d_context.get(), true), b(d_context.get(), false);
111 : :
112 : : try
113 : : {
114 : 1 : MyContextNotifyObj c(d_context.get(), true), d(d_context.get(), false);
115 : :
116 [ - + ]: 1 : ASSERT_EQ(a.d_ncalls, 0);
117 [ - + ]: 1 : ASSERT_EQ(b.d_ncalls, 0);
118 [ - + ]: 1 : ASSERT_EQ(c.d_ncalls, 0);
119 [ - + ]: 1 : ASSERT_EQ(d.d_ncalls, 0);
120 : :
121 : 1 : MyContextObj w(d_context.get(), a);
122 : 1 : MyContextObj x(d_context.get(), b);
123 : 1 : MyContextObj y(d_context.get(), c);
124 : 1 : MyContextObj z(d_context.get(), d);
125 : :
126 : 1 : d_context->push();
127 : :
128 : 1 : w.makeCurrent();
129 : 1 : x.makeCurrent();
130 : 1 : y.makeCurrent();
131 : 1 : z.makeCurrent();
132 : :
133 [ - + ]: 1 : ASSERT_EQ(a.d_ncalls, 0);
134 [ - + ]: 1 : ASSERT_EQ(b.d_ncalls, 0);
135 [ - + ]: 1 : ASSERT_EQ(c.d_ncalls, 0);
136 [ - + ]: 1 : ASSERT_EQ(d.d_ncalls, 0);
137 : :
138 [ - + ]: 1 : ASSERT_EQ(w.d_ncalls, 0);
139 [ - + ]: 1 : ASSERT_EQ(x.d_ncalls, 0);
140 [ - + ]: 1 : ASSERT_EQ(y.d_ncalls, 0);
141 [ - + ]: 1 : ASSERT_EQ(z.d_ncalls, 0);
142 : :
143 : 1 : d_context->push();
144 : :
145 : 1 : w.makeCurrent();
146 : 1 : x.makeCurrent();
147 : 1 : y.makeCurrent();
148 : 1 : z.makeCurrent();
149 : :
150 [ - + ]: 1 : ASSERT_EQ(a.d_ncalls, 0);
151 [ - + ]: 1 : ASSERT_EQ(b.d_ncalls, 0);
152 [ - + ]: 1 : ASSERT_EQ(c.d_ncalls, 0);
153 [ - + ]: 1 : ASSERT_EQ(d.d_ncalls, 0);
154 : :
155 [ - + ]: 1 : ASSERT_EQ(w.d_ncalls, 0);
156 [ - + ]: 1 : ASSERT_EQ(x.d_ncalls, 0);
157 [ - + ]: 1 : ASSERT_EQ(y.d_ncalls, 0);
158 [ - + ]: 1 : ASSERT_EQ(z.d_ncalls, 0);
159 : :
160 : 1 : d_context->pop();
161 : :
162 [ - + ]: 1 : ASSERT_EQ(a.d_ncalls, 1);
163 [ - + ]: 1 : ASSERT_EQ(b.d_ncalls, 1);
164 [ - + ]: 1 : ASSERT_EQ(c.d_ncalls, 1);
165 [ - + ]: 1 : ASSERT_EQ(d.d_ncalls, 1);
166 : :
167 [ - + ]: 1 : ASSERT_EQ(w.d_ncalls, 1);
168 [ - + ]: 1 : ASSERT_EQ(x.d_ncalls, 0);
169 [ - + ]: 1 : ASSERT_EQ(y.d_ncalls, 1);
170 [ - + ]: 1 : ASSERT_EQ(z.d_ncalls, 0);
171 : :
172 : 1 : d_context->pop();
173 : :
174 [ - + ]: 1 : ASSERT_EQ(a.d_ncalls, 2);
175 [ - + ]: 1 : ASSERT_EQ(b.d_ncalls, 2);
176 [ - + ]: 1 : ASSERT_EQ(c.d_ncalls, 2);
177 [ - + ]: 1 : ASSERT_EQ(d.d_ncalls, 2);
178 : :
179 [ - + ]: 1 : ASSERT_EQ(w.d_ncalls, 2);
180 [ - + ]: 1 : ASSERT_EQ(x.d_ncalls, 1);
181 [ - + ]: 1 : ASSERT_EQ(y.d_ncalls, 2);
182 [ - + ]: 1 : ASSERT_EQ(z.d_ncalls, 1);
183 : : }
184 [ - - ]: 0 : catch (Exception& e)
185 : : {
186 : 0 : std::cerr << e.toString() << std::endl;
187 [ - - ]: 0 : ASSERT_TRUE(false) << "Exception thrown from test";
188 : : }
189 : :
190 : : // we do this (together with the { } block above) to get full code
191 : : // coverage of destruction paths; a and b haven't been destructed
192 : : // yet, here.
193 : 1 : d_context.reset(nullptr);
194 : : }
195 : :
196 : 2 : TEST_F(TestContextBlack, detect_invalid_obj)
197 : : {
198 : 2 : MyContextNotifyObj n(d_context.get(), true);
199 : :
200 : : {
201 : : // Objects allocated at the bottom scope are allowed to outlive the scope
202 : : // that they have been allocated in.
203 : 1 : d_context->push();
204 : 2 : MyContextObj x(d_context.get(), n);
205 : 1 : d_context->pop();
206 : : }
207 : 1 : }
208 : :
209 : : } // namespace test
210 : : } // namespace cvc5::internal
|
