Branch data Line data Source code
1 : : /*****************************************************************************************[Alloc.h]
2 : : Copyright (c) 2008-2010, Niklas Sorensson
3 : :
4 : : Permission is hereby granted, free of charge, to any person obtaining a copy of
5 : : this software and associated documentation files (the "Software"), to deal in
6 : : the Software without restriction, including without limitation the rights to
7 : : use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
8 : : the Software, and to permit persons to whom the Software is furnished to do so,
9 : : subject to the following conditions:
10 : :
11 : : The above copyright notice and this permission notice shall be included in all
12 : : copies or substantial portions of the Software.
13 : :
14 : : THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 : : IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
16 : : FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
17 : : COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
18 : : IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
19 : : CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
20 : : **************************************************************************************************/
21 : :
22 : : #ifndef Minisat_Alloc_h
23 : : #define Minisat_Alloc_h
24 : :
25 : : #include "base/check.h"
26 : : #include "prop/minisat/mtl/Vec.h"
27 : : #include "prop/minisat/mtl/XAlloc.h"
28 : :
29 : : namespace cvc5::internal {
30 : : namespace Minisat {
31 : :
32 : : //=================================================================================================
33 : : // Simple Region-based memory allocator:
34 : :
35 : : template <class T>
36 : : class RegionAllocator
37 : : {
38 : : T* memory;
39 : : uint32_t sz;
40 : : uint32_t cap;
41 : : uint32_t wasted_;
42 : :
43 : : void capacity(uint32_t min_cap);
44 : :
45 : : public:
46 : : // TODO: make this a class for better type-checking?
47 : : typedef uint32_t Ref;
48 : : enum
49 : : {
50 : : Ref_Undef = UINT32_MAX
51 : : };
52 : : enum
53 : : {
54 : : Unit_Size = sizeof(uint32_t)
55 : : };
56 : :
57 : 3500 : explicit RegionAllocator(uint32_t start_cap = 1024 * 1024)
58 : 3500 : : memory(nullptr), sz(0), cap(0), wasted_(0)
59 : : {
60 : 3500 : capacity(start_cap);
61 : 3500 : }
62 : 3499 : ~RegionAllocator()
63 : : {
64 [ + + ]: 3499 : if (memory != nullptr) ::free(memory);
65 : 3499 : }
66 : :
67 : 14247 : uint32_t size() const { return sz; }
68 : 5046 : uint32_t wasted() const { return wasted_; }
69 : :
70 : : Ref alloc(int size);
71 : 216774 : void free(int size) { wasted_ += size; }
72 : :
73 : : // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
74 : 4412809 : T& operator[](Ref r)
75 : : {
76 [ - + ][ - + ]: 4412809 : Assert(r < sz);
[ - - ]
77 : 4412809 : return memory[r];
78 : : }
79 : 181975 : const T& operator[](Ref r) const
80 : : {
81 [ - + ][ - + ]: 181975 : Assert(r < sz);
[ - - ]
82 : 181975 : return memory[r];
83 : : }
84 : :
85 : 402278 : T* lea(Ref r)
86 : : {
87 [ - + ][ - + ]: 402278 : Assert(r < sz);
[ - - ]
88 : 402278 : return &memory[r];
89 : : }
90 : 1419 : const T* lea(Ref r) const
91 : : {
92 [ - + ][ - + ]: 1419 : Assert(r < sz);
[ - - ]
93 : 1419 : return &memory[r];
94 : : }
95 : : Ref ael(const T* t)
96 : : {
97 : : Assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz - 1]);
98 : : return (Ref)(t - &memory[0]);
99 : : }
100 : :
101 : 364 : void moveTo(RegionAllocator& to)
102 : : {
103 [ + - ]: 364 : if (to.memory != nullptr) ::free(to.memory);
104 : 364 : to.memory = memory;
105 : 364 : to.sz = sz;
106 : 364 : to.cap = cap;
107 : 364 : to.wasted_ = wasted_;
108 : :
109 : 364 : memory = nullptr;
110 : 364 : sz = cap = wasted_ = 0;
111 : 364 : }
112 : : };
113 : :
114 : : template <class T>
115 : 405778 : void RegionAllocator<T>::capacity(uint32_t min_cap)
116 : : {
117 [ + + ]: 405778 : if (cap >= min_cap) return;
118 : :
119 : 4240 : uint32_t prev_cap = cap;
120 [ + + ]: 93543 : while (cap < min_cap)
121 : : {
122 : : // NOTE: Multiply by a factor (13/8) without causing overflow, then add 2
123 : : // and make the result even by clearing the least significant bit. The
124 : : // resulting sequence of capacities is carefully chosen to hit a maximum
125 : : // capacity that is close to the '2^32-1' limit when using 'uint32_t' as
126 : : // indices so that as much as possible of this space can be used.
127 : 89303 : uint32_t delta = ((cap >> 1) + (cap >> 3) + 2) & ~1;
128 : 89303 : cap += delta;
129 : :
130 [ - + ]: 89303 : if (cap <= prev_cap) throw OutOfMemoryException();
131 : : }
132 : : // printf(" .. (%p) cap = %u\n", this, cap);
133 : :
134 [ - + ][ - + ]: 4240 : Assert(cap > 0);
[ - - ]
135 : 4240 : memory = (T*)xrealloc(memory, sizeof(T) * cap);
136 : : }
137 : :
138 : : template <class T>
139 : 402278 : typename RegionAllocator<T>::Ref RegionAllocator<T>::alloc(int size)
140 : : {
141 : : // printf("ALLOC called (this = %p, size = %d)\n", this, size);
142 : : // fflush(stdout);
143 [ - + ][ - + ]: 402278 : Assert(size > 0);
[ - - ]
144 : 402278 : capacity(sz + size);
145 : :
146 : 402278 : uint32_t prev_sz = sz;
147 : 402278 : sz += size;
148 : :
149 : : // Handle overflow:
150 [ - + ]: 402278 : if (sz < prev_sz) throw OutOfMemoryException();
151 : :
152 : 402278 : return prev_sz;
153 : : }
154 : :
155 : : //=================================================================================================
156 : : } // namespace Minisat
157 : : } // namespace cvc5::internal
158 : :
159 : : #endif
|
