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 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 Minisat_Alloc_h
22 : : #define Minisat_Alloc_h
23 : :
24 : : #include "base/check.h"
25 : : #include "prop/minisat/mtl/Vec.h"
26 : : #include "prop/minisat/mtl/XAlloc.h"
27 : :
28 : : namespace cvc5::internal {
29 : : namespace Minisat {
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 : 53768 : explicit RegionAllocator(uint32_t start_cap = 1024*1024) : memory(NULL), sz(0), cap(0), wasted_(0){ capacity(start_cap); }
51 : 53512 : ~RegionAllocator()
52 : : {
53 [ + + ]: 53512 : if (memory != NULL)
54 : 50219 : ::free(memory);
55 : 53512 : }
56 : :
57 : :
58 : 2056630 : uint32_t size () const { return sz; }
59 : 122024 : uint32_t wasted () const { return wasted_; }
60 : :
61 : : Ref alloc (int size);
62 : 801588 : void free (int size) { wasted_ += size; }
63 : :
64 : : // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
65 : 832639000 : T& operator[](Ref r)
66 : : {
67 [ - + ][ - + ]: 832639000 : Assert(r >= 0 && r < sz);
[ - - ]
68 : 832639000 : return memory[r];
69 : : }
70 : 3323870 : const T& operator[](Ref r) const
71 : : {
72 [ - + ][ - + ]: 3323870 : Assert(r >= 0 && r < sz);
[ - - ]
73 : 3323870 : return memory[r];
74 : : }
75 : :
76 : 7354710 : T* lea(Ref r)
77 : : {
78 [ - + ][ - + ]: 7354710 : Assert(r >= 0 && r < sz);
[ - - ]
79 : 7354710 : return &memory[r];
80 : : }
81 : 128940 : const T* lea(Ref r) const
82 : : {
83 [ - + ][ - + ]: 128940 : Assert(r >= 0 && r < sz);
[ - - ]
84 : 128940 : 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 : 3291 : void moveTo(RegionAllocator& to) {
94 [ + - ]: 3291 : if (to.memory != NULL) ::free(to.memory);
95 : 3291 : to.memory = memory;
96 : 3291 : to.sz = sz;
97 : 3291 : to.cap = cap;
98 : 3291 : to.wasted_ = wasted_;
99 : :
100 : 3291 : memory = NULL;
101 : 3291 : sz = cap = wasted_ = 0;
102 : 3291 : }
103 : :
104 : :
105 : : };
106 : :
107 : : template<class T>
108 : 7408480 : void RegionAllocator<T>::capacity(uint32_t min_cap)
109 : : {
110 [ + + ]: 7408480 : if (cap >= min_cap) return;
111 : :
112 : 58308 : uint32_t prev_cap = cap;
113 [ + + ]: 1459060 : 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 : 1400750 : uint32_t delta = ((cap >> 1) + (cap >> 3) + 2) & ~1;
119 : 1400750 : cap += delta;
120 : :
121 [ - + ]: 1400750 : if (cap <= prev_cap)
122 : 0 : throw OutOfMemoryException();
123 : : }
124 : : // printf(" .. (%p) cap = %u\n", this, cap);
125 : :
126 [ - + ][ - + ]: 58308 : Assert(cap > 0);
[ - - ]
127 : 58308 : memory = (T*)xrealloc(memory, sizeof(T)*cap);
128 : : }
129 : :
130 : :
131 : : template<class T>
132 : : typename RegionAllocator<T>::Ref
133 : 7354710 : RegionAllocator<T>::alloc(int size)
134 : : {
135 : : // printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout);
136 [ - + ][ - + ]: 7354710 : Assert(size > 0);
[ - - ]
137 : 7354710 : capacity(sz + size);
138 : :
139 : 7354710 : uint32_t prev_sz = sz;
140 : 7354710 : sz += size;
141 : :
142 : : // Handle overflow:
143 [ - + ]: 7354710 : if (sz < prev_sz)
144 : 0 : throw OutOfMemoryException();
145 : :
146 : 7354710 : return prev_sz;
147 : : }
148 : :
149 : :
150 : : //=================================================================================================
151 : : }
152 : : } // namespace cvc5::internal
153 : :
154 : : #endif
|
