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