1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Dejan Jovanovic, Andres Noetzli |
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::ContextMemoryManager. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include <cstring> |
17 |
|
#include <iostream> |
18 |
|
#include <vector> |
19 |
|
|
20 |
|
#include "context/context_mm.h" |
21 |
|
#include "test.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
|
25 |
|
using namespace context; |
26 |
|
|
27 |
|
namespace test { |
28 |
|
|
29 |
4 |
class TestContextBlackMM : public TestInternal |
30 |
|
{ |
31 |
|
protected: |
32 |
2 |
void SetUp() override { d_cmm.reset(new ContextMemoryManager()); } |
33 |
|
std::unique_ptr<ContextMemoryManager> d_cmm; |
34 |
|
}; |
35 |
|
|
36 |
10 |
TEST_F(TestContextBlackMM, push_pop) |
37 |
|
{ |
38 |
|
#ifdef CVC5_DEBUG_CONTEXT_MEMORY_MANAGER |
39 |
|
#warning "Using the debug context memory manager, omitting unit tests" |
40 |
|
#else |
41 |
|
// Push, then allocate, then pop |
42 |
|
// We make sure that we don't allocate too much so that all the regions |
43 |
|
// should be reclaimed |
44 |
2 |
uint32_t chunk_size_bytes = 16384; |
45 |
2 |
uint32_t max_free_chunks = 100; |
46 |
2 |
uint32_t pieces_per_chunk = 13; |
47 |
|
uint32_t len; |
48 |
|
uint32_t n; |
49 |
|
|
50 |
2 |
len = chunk_size_bytes / pieces_per_chunk; // Length of the individual block |
51 |
2 |
n = max_free_chunks * pieces_per_chunk; |
52 |
12 |
for (uint32_t p = 0; p < 5; ++p) |
53 |
|
{ |
54 |
10 |
d_cmm->push(); |
55 |
13010 |
for (uint32_t i = 0; i < n; ++i) |
56 |
|
{ |
57 |
13000 |
char* newMem = (char*)d_cmm->newData(len); |
58 |
|
// We only setup the memory in the first run, the others should |
59 |
|
// reclaim the same memory |
60 |
13000 |
if (p == 0) |
61 |
|
{ |
62 |
3276000 |
for (uint32_t k = 0; k < len - 1; k++) |
63 |
|
{ |
64 |
3273400 |
newMem[k] = 'a'; |
65 |
|
} |
66 |
2600 |
newMem[len - 1] = 0; |
67 |
|
} |
68 |
13000 |
if (strlen(newMem) != len - 1) |
69 |
|
{ |
70 |
|
std::cout << strlen(newMem) << " : " << len - 1 << std::endl; |
71 |
|
} |
72 |
13000 |
ASSERT_EQ(strlen(newMem), len - 1); |
73 |
|
} |
74 |
10 |
d_cmm->pop(); |
75 |
|
} |
76 |
|
|
77 |
2 |
uint32_t factor = 3; |
78 |
2 |
n = 16384 / factor; |
79 |
|
// Push, then allocate, then pop all at once |
80 |
12 |
for (uint32_t p = 0; p < 5; ++p) |
81 |
|
{ |
82 |
10 |
d_cmm->push(); |
83 |
54610 |
for (uint32_t i = 1; i < n; ++i) |
84 |
|
{ |
85 |
54600 |
len = i * factor; |
86 |
54600 |
char* newMem = (char*)d_cmm->newData(len); |
87 |
447255900 |
for (uint32_t k = 0; k < len - 1; k++) |
88 |
|
{ |
89 |
447201300 |
newMem[k] = 'a'; |
90 |
|
} |
91 |
54600 |
newMem[len - 1] = 0; |
92 |
54600 |
ASSERT_EQ(strlen(newMem), len - 1); |
93 |
|
} |
94 |
|
} |
95 |
12 |
for (uint32_t p = 0; p < 5; ++p) |
96 |
|
{ |
97 |
10 |
d_cmm->pop(); |
98 |
|
} |
99 |
|
|
100 |
|
// Try popping out of scope |
101 |
2 |
ASSERT_DEATH(d_cmm->pop(), "d_nextFreeStack.size\\(\\) > 0"); |
102 |
|
#endif |
103 |
|
} |
104 |
|
|
105 |
|
} // namespace test |
106 |
6 |
} // namespace cvc5 |