GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/context/context_black.cpp Lines: 115 118 97.5 %
Date: 2021-09-29 Branches: 221 905 24.4 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Aina Niemetz, Morgan Deters, Dejan Jovanovic
4
 *
5
 * This file is part of the cvc5 project.
6
 *
7
 * Copyright (c) 2009-2021 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 {
25
26
using namespace context;
27
28
namespace test {
29
30
struct MyContextNotifyObj : public ContextNotifyObj
31
{
32
12
  MyContextNotifyObj(Context* context, bool pre)
33
12
      : ContextNotifyObj(context, pre), d_ncalls(0)
34
  {
35
12
  }
36
37
12
  ~MyContextNotifyObj() override {}
38
39
22
  void contextNotifyPop() override { ++d_ncalls; }
40
41
  int32_t d_ncalls;
42
};
43
44
class MyContextObj : public ContextObj
45
{
46
 public:
47
8
  MyContextObj(Context* context, MyContextNotifyObj& n)
48
8
      : ContextObj(context), d_ncalls(0), d_nsaves(0), d_notify(n)
49
  {
50
8
  }
51
52
6
  MyContextObj(bool topScope, Context* context, MyContextNotifyObj& n)
53
6
      : ContextObj(topScope, context), d_ncalls(0), d_nsaves(0), d_notify(n)
54
  {
55
6
  }
56
57
14
  ~MyContextObj() override { destroy(); }
58
59
22
  ContextObj* save(ContextMemoryManager* pcmm) override
60
  {
61
22
    ++d_nsaves;
62
22
    return new (pcmm) MyContextObj(*this);
63
  }
64
65
22
  void restore(ContextObj* contextObj) override
66
  {
67
22
    d_ncalls = d_notify.d_ncalls;
68
22
  }
69
70
24
  void makeCurrent() { ContextObj::makeCurrent(); }
71
72
  int32_t d_ncalls;
73
  int32_t d_nsaves;
74
75
 private:
76
22
  MyContextObj(const MyContextObj& other)
77
22
      : ContextObj(other), d_ncalls(0), d_nsaves(0), d_notify(other.d_notify)
78
  {
79
22
  }
80
  MyContextNotifyObj& d_notify;
81
};
82
83
20
class TestContextBlack : public TestContext
84
{
85
};
86
87
14
TEST_F(TestContextBlack, push_pop)
88
{
89
  // Test what happens when the context is popped below 0
90
  // the interface doesn't declare any exceptions
91
2
  d_context->push();
92
2
  d_context->pop();
93
#ifdef CVC5_ASSERTIONS
94
2
  ASSERT_DEATH(d_context->pop(), "Cannot pop below level 0");
95
2
  ASSERT_DEATH(d_context->pop(), "Cannot pop below level 0");
96
#endif /* CVC5_ASSERTIONS */
97
}
98
99
14
TEST_F(TestContextBlack, dtor)
100
{
101
  // Destruction of ContextObj was broken in revision 324 (bug #45) when
102
  // at a higher context level with an intervening modification.
103
  // (The following caused a "pure virtual method called" error.)
104
4
  CDO<int32_t> i(d_context.get());
105
2
  d_context->push();
106
2
  i = 5;
107
2
}
108
109
14
TEST_F(TestContextBlack, pre_post_notify)
110
{
111
  // This is tricky; we want to detect if pre- and post-notifies are
112
  // done correctly.  For that, we have to use a special ContextObj,
113
  // since that's the only thing that runs between pre- and post-.
114
115
4
  MyContextNotifyObj a(d_context.get(), true), b(d_context.get(), false);
116
117
  try
118
  {
119
4
    MyContextNotifyObj c(d_context.get(), true), d(d_context.get(), false);
120
121
2
    ASSERT_EQ(a.d_ncalls, 0);
122
2
    ASSERT_EQ(b.d_ncalls, 0);
123
2
    ASSERT_EQ(c.d_ncalls, 0);
124
2
    ASSERT_EQ(d.d_ncalls, 0);
125
126
4
    MyContextObj w(d_context.get(), a);
127
4
    MyContextObj x(d_context.get(), b);
128
4
    MyContextObj y(d_context.get(), c);
129
4
    MyContextObj z(d_context.get(), d);
130
131
2
    d_context->push();
132
133
2
    w.makeCurrent();
134
2
    x.makeCurrent();
135
2
    y.makeCurrent();
136
2
    z.makeCurrent();
137
138
2
    ASSERT_EQ(a.d_ncalls, 0);
139
2
    ASSERT_EQ(b.d_ncalls, 0);
140
2
    ASSERT_EQ(c.d_ncalls, 0);
141
2
    ASSERT_EQ(d.d_ncalls, 0);
142
143
2
    ASSERT_EQ(w.d_ncalls, 0);
144
2
    ASSERT_EQ(x.d_ncalls, 0);
145
2
    ASSERT_EQ(y.d_ncalls, 0);
146
2
    ASSERT_EQ(z.d_ncalls, 0);
147
148
2
    d_context->push();
149
150
2
    w.makeCurrent();
151
2
    x.makeCurrent();
152
2
    y.makeCurrent();
153
2
    z.makeCurrent();
154
155
2
    ASSERT_EQ(a.d_ncalls, 0);
156
2
    ASSERT_EQ(b.d_ncalls, 0);
157
2
    ASSERT_EQ(c.d_ncalls, 0);
158
2
    ASSERT_EQ(d.d_ncalls, 0);
159
160
2
    ASSERT_EQ(w.d_ncalls, 0);
161
2
    ASSERT_EQ(x.d_ncalls, 0);
162
2
    ASSERT_EQ(y.d_ncalls, 0);
163
2
    ASSERT_EQ(z.d_ncalls, 0);
164
165
2
    d_context->pop();
166
167
2
    ASSERT_EQ(a.d_ncalls, 1);
168
2
    ASSERT_EQ(b.d_ncalls, 1);
169
2
    ASSERT_EQ(c.d_ncalls, 1);
170
2
    ASSERT_EQ(d.d_ncalls, 1);
171
172
2
    ASSERT_EQ(w.d_ncalls, 1);
173
2
    ASSERT_EQ(x.d_ncalls, 0);
174
2
    ASSERT_EQ(y.d_ncalls, 1);
175
2
    ASSERT_EQ(z.d_ncalls, 0);
176
177
2
    d_context->pop();
178
179
2
    ASSERT_EQ(a.d_ncalls, 2);
180
2
    ASSERT_EQ(b.d_ncalls, 2);
181
2
    ASSERT_EQ(c.d_ncalls, 2);
182
2
    ASSERT_EQ(d.d_ncalls, 2);
183
184
2
    ASSERT_EQ(w.d_ncalls, 2);
185
2
    ASSERT_EQ(x.d_ncalls, 1);
186
2
    ASSERT_EQ(y.d_ncalls, 2);
187
2
    ASSERT_EQ(z.d_ncalls, 1);
188
  }
189
  catch (Exception& e)
190
  {
191
    std::cerr << e.toString() << std::endl;
192
    ASSERT_TRUE(false) << "Exception thrown from test";
193
  }
194
195
  // we do this (together with the { } block above) to get full code
196
  // coverage of destruction paths; a and b haven't been destructed
197
  // yet, here.
198
2
  d_context.reset(nullptr);
199
}
200
201
14
TEST_F(TestContextBlack, top_scope_context_obj)
202
{
203
  // this test's implementation is based on the fact that a
204
  // ContextObj allocated primordially "in the top scope" (first arg
205
  // to ctor is "true"), doesn't get updated if you immediately call
206
  // makeCurrent().
207
208
4
  MyContextNotifyObj n(d_context.get(), true);
209
210
2
  d_context->push();
211
212
4
  MyContextObj x(false, d_context.get(), n);
213
  {
214
4
    MyContextObj y(true, d_context.get(), n);
215
216
2
    ASSERT_EQ(x.d_nsaves, 0);
217
2
    ASSERT_EQ(y.d_nsaves, 0);
218
219
2
    x.makeCurrent();
220
2
    y.makeCurrent();
221
222
2
    ASSERT_EQ(x.d_nsaves, 1);
223
2
    ASSERT_EQ(y.d_nsaves, 0);
224
225
2
    d_context->push();
226
227
2
    x.makeCurrent();
228
2
    y.makeCurrent();
229
230
2
    ASSERT_EQ(x.d_nsaves, 2);
231
2
    ASSERT_EQ(y.d_nsaves, 1);
232
233
2
    d_context->pop();
234
235
    // `y` is invalid below the first level because it was allocated in the top
236
    // scope. We have to make sure to destroy it before the next pop.
237
  }
238
239
2
  d_context->pop();
240
241
2
  ASSERT_EQ(x.d_nsaves, 2);
242
}
243
244
14
TEST_F(TestContextBlack, detect_invalid_obj)
245
{
246
4
  MyContextNotifyObj n(d_context.get(), true);
247
248
  {
249
    // Objects allocated at the bottom scope are allowed to outlive the scope
250
    // that they have been allocated in.
251
2
    d_context->push();
252
4
    MyContextObj x(false, d_context.get(), n);
253
2
    d_context->pop();
254
  }
255
256
2
  ASSERT_DEATH(
257
      {
258
        // Objects allocated at the top scope are not allowed to outlive the
259
        // scope that they have been allocated in.
260
        d_context->push();
261
        MyContextObj y(true, d_context.get(), n);
262
        d_context->pop();
263
      },
264
      "d_pScope != nullptr");
265
}
266
267
}  // namespace test
268
18
}  // namespace cvc5