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