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*) override { d_ncalls = d_notify.d_ncalls; }
58 : :
59 : 8 : void makeCurrent() { ContextObj::makeCurrent(); }
60 : :
61 : : int32_t d_ncalls;
62 : : int32_t d_nsaves;
63 : :
64 : : private:
65 : 8 : MyContextObj(const MyContextObj& other)
66 : 8 : : ContextObj(other), d_ncalls(0), d_nsaves(0), d_notify(other.d_notify)
67 : : {
68 : 8 : }
69 : : MyContextNotifyObj& d_notify;
70 : : };
71 : :
72 : : class TestContextBlack : public TestContext
73 : : {
74 : : };
75 : :
76 : 4 : TEST_F(TestContextBlack, push_pop)
77 : : {
78 : : // Test what happens when the context is popped below 0
79 : : // the interface doesn't declare any exceptions
80 : 1 : d_context->push();
81 : 1 : d_context->pop();
82 : : #ifdef CVC5_ASSERTIONS
83 : 1 : ASSERT_DEATH(d_context->pop(), "Cannot pop below level 0");
84 : 1 : ASSERT_DEATH(d_context->pop(), "Cannot pop below level 0");
85 : : #endif /* CVC5_ASSERTIONS */
86 : : }
87 : :
88 : 4 : TEST_F(TestContextBlack, dtor)
89 : : {
90 : : // Destruction of ContextObj was broken in revision 324 (bug #45) when
91 : : // at a higher context level with an intervening modification.
92 : : // (The following caused a "pure virtual method called" error.)
93 : 1 : CDO<int32_t> i(d_context.get());
94 : 1 : d_context->push();
95 : 1 : i = 5;
96 : 1 : }
97 : :
98 : 4 : TEST_F(TestContextBlack, pre_post_notify)
99 : : {
100 : : // This is tricky; we want to detect if pre- and post-notifies are
101 : : // done correctly. For that, we have to use a special ContextObj,
102 : : // since that's the only thing that runs between pre- and post-.
103 : :
104 : 1 : MyContextNotifyObj a(d_context.get(), true), b(d_context.get(), false);
105 : :
106 : : try
107 : : {
108 : 1 : MyContextNotifyObj c(d_context.get(), true), d(d_context.get(), false);
109 : :
110 [ - + ][ + - ]: 1 : ASSERT_EQ(a.d_ncalls, 0);
111 [ - + ][ + - ]: 1 : ASSERT_EQ(b.d_ncalls, 0);
112 [ - + ][ + - ]: 1 : ASSERT_EQ(c.d_ncalls, 0);
113 [ - + ][ + - ]: 1 : ASSERT_EQ(d.d_ncalls, 0);
114 : :
115 : 1 : MyContextObj w(d_context.get(), a);
116 : 1 : MyContextObj x(d_context.get(), b);
117 : 1 : MyContextObj y(d_context.get(), c);
118 : 1 : MyContextObj z(d_context.get(), d);
119 : :
120 : 1 : d_context->push();
121 : :
122 : 1 : w.makeCurrent();
123 : 1 : x.makeCurrent();
124 : 1 : y.makeCurrent();
125 : 1 : z.makeCurrent();
126 : :
127 [ - + ][ + - ]: 1 : ASSERT_EQ(a.d_ncalls, 0);
128 [ - + ][ + - ]: 1 : ASSERT_EQ(b.d_ncalls, 0);
129 [ - + ][ + - ]: 1 : ASSERT_EQ(c.d_ncalls, 0);
130 [ - + ][ + - ]: 1 : ASSERT_EQ(d.d_ncalls, 0);
131 : :
132 [ - + ][ + - ]: 1 : ASSERT_EQ(w.d_ncalls, 0);
133 [ - + ][ + - ]: 1 : ASSERT_EQ(x.d_ncalls, 0);
134 [ - + ][ + - ]: 1 : ASSERT_EQ(y.d_ncalls, 0);
135 [ - + ][ + - ]: 1 : ASSERT_EQ(z.d_ncalls, 0);
136 : :
137 : 1 : d_context->push();
138 : :
139 : 1 : w.makeCurrent();
140 : 1 : x.makeCurrent();
141 : 1 : y.makeCurrent();
142 : 1 : z.makeCurrent();
143 : :
144 [ - + ][ + - ]: 1 : ASSERT_EQ(a.d_ncalls, 0);
145 [ - + ][ + - ]: 1 : ASSERT_EQ(b.d_ncalls, 0);
146 [ - + ][ + - ]: 1 : ASSERT_EQ(c.d_ncalls, 0);
147 [ - + ][ + - ]: 1 : ASSERT_EQ(d.d_ncalls, 0);
148 : :
149 [ - + ][ + - ]: 1 : ASSERT_EQ(w.d_ncalls, 0);
150 [ - + ][ + - ]: 1 : ASSERT_EQ(x.d_ncalls, 0);
151 [ - + ][ + - ]: 1 : ASSERT_EQ(y.d_ncalls, 0);
152 [ - + ][ + - ]: 1 : ASSERT_EQ(z.d_ncalls, 0);
153 : :
154 : 1 : d_context->pop();
155 : :
156 [ - + ][ + - ]: 1 : ASSERT_EQ(a.d_ncalls, 1);
157 [ - + ][ + - ]: 1 : ASSERT_EQ(b.d_ncalls, 1);
158 [ - + ][ + - ]: 1 : ASSERT_EQ(c.d_ncalls, 1);
159 [ - + ][ + - ]: 1 : ASSERT_EQ(d.d_ncalls, 1);
160 : :
161 [ - + ][ + - ]: 1 : ASSERT_EQ(w.d_ncalls, 1);
162 [ - + ][ + - ]: 1 : ASSERT_EQ(x.d_ncalls, 0);
163 [ - + ][ + - ]: 1 : ASSERT_EQ(y.d_ncalls, 1);
164 [ - + ][ + - ]: 1 : ASSERT_EQ(z.d_ncalls, 0);
165 : :
166 : 1 : d_context->pop();
167 : :
168 [ - + ][ + - ]: 1 : ASSERT_EQ(a.d_ncalls, 2);
169 [ - + ][ + - ]: 1 : ASSERT_EQ(b.d_ncalls, 2);
170 [ - + ][ + - ]: 1 : ASSERT_EQ(c.d_ncalls, 2);
171 [ - + ][ + - ]: 1 : ASSERT_EQ(d.d_ncalls, 2);
172 : :
173 [ - + ][ + - ]: 1 : ASSERT_EQ(w.d_ncalls, 2);
174 [ - + ][ + - ]: 1 : ASSERT_EQ(x.d_ncalls, 1);
175 [ - + ][ + - ]: 1 : ASSERT_EQ(y.d_ncalls, 2);
176 [ - + ][ + - ]: 1 : ASSERT_EQ(z.d_ncalls, 1);
177 [ + - ][ + - ]: 1 : }
178 [ - - ]: 0 : catch (Exception& e)
179 : : {
180 : 0 : std::cerr << e.toString() << std::endl;
181 : 0 : ASSERT_TRUE(false) << "Exception thrown from test";
182 [ - - ]: 0 : }
183 : :
184 : : // we do this (together with the { } block above) to get full code
185 : : // coverage of destruction paths; a and b haven't been destructed
186 : : // yet, here.
187 : 1 : d_context.reset(nullptr);
188 [ + - ][ + - ]: 1 : }
189 : :
190 : 4 : TEST_F(TestContextBlack, detect_invalid_obj)
191 : : {
192 : 1 : MyContextNotifyObj n(d_context.get(), true);
193 : :
194 : : {
195 : : // Objects allocated at the bottom scope are allowed to outlive the scope
196 : : // that they have been allocated in.
197 : 1 : d_context->push();
198 : 1 : MyContextObj x(d_context.get(), n);
199 : 1 : d_context->pop();
200 : 1 : }
201 : 1 : }
202 : :
203 : : } // namespace test
204 : : } // namespace cvc5::internal
|
