1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * STORE FOR ALLOCATION OF (SMALL) OBJECTS
21 */
22
23 #include <assert.h>
24 #include <stdbool.h>
25 #include <stddef.h>
26
27 #include "utils/memalloc.h"
28 #include "utils/object_stores.h"
29 #include "mt/thread_macros.h"
30
31 #ifndef NDEBUG
32
33 /*
34 * For debugging: check alignment.
35 * We want pointers aligned to multiples of 8.
36 */
ptr_is_aligned(void * p)37 static bool ptr_is_aligned(void *p) {
38 uintptr_t x;
39
40 x = (uintptr_t) p;
41 return (x & (uintptr_t) 7) == 0;
42 }
43
44 // p <= q here
offset_is_aligned(void * p,void * q)45 static bool offset_is_aligned(void *p, void *q) {
46 uintptr_t x, y;
47
48 x = (uintptr_t) p;
49 y = (uintptr_t) q;
50 assert(x <= y);
51
52 return ((y - x) & (uintptr_t) 7) == 0;
53 }
54
55 #endif
56
57
58
59 /*
60 * Initialize s:
61 * - objsize = size of all objects in s
62 * - n = number of objects per block
63 */
_o_init_objstore(object_store_t * s,uint32_t objsize,uint32_t n)64 static void _o_init_objstore(object_store_t *s, uint32_t objsize, uint32_t n) {
65 assert(objsize <= MAX_OBJ_SIZE);
66 assert(0 < n && n <= MAX_OBJ_PER_BLOCK);
67
68 // round up objsize to a multiple of 8 for pointer alignment
69 objsize = (objsize + 7) & ((uint32_t )(~7));
70
71 s->bnk = NULL;
72 s->free_list = NULL;
73 s->free_index = 0;
74 s->objsize = objsize;
75 s->blocksize = objsize * n;
76 }
77
init_objstore(object_store_t * s,uint32_t objsize,uint32_t n)78 void init_objstore(object_store_t *s, uint32_t objsize, uint32_t n) {
79 #ifdef THREAD_SAFE
80 create_yices_lock(&(s->lock));
81 #endif
82 MT_PROTECT_VOID(s->lock, _o_init_objstore(s, objsize, n));
83 }
84
85
86 /*
87 * Allocate an object in s
88 */
_o_objstore_alloc(object_store_t * s)89 static void *_o_objstore_alloc(object_store_t *s) {
90 void *tmp;
91 uint32_t i;
92 object_bank_t *new_bank;
93
94 tmp = s->free_list;
95 if (tmp != NULL) {
96 // This may be unsafe. Replaced by memcpy.
97 // s->free_list = * ((void **) tmp);
98 memcpy(&s->free_list, tmp, sizeof(void*));
99
100 assert(ptr_is_aligned(tmp));
101
102 return tmp;
103 }
104
105 i = s->free_index;
106 if (i == 0) {
107 new_bank = (object_bank_t *) safe_malloc(sizeof(object_bank_t) + s->blocksize * sizeof(char));
108 new_bank->h.next = s->bnk;
109 s->bnk = new_bank;
110 i = s->blocksize;
111
112 assert(offset_is_aligned(new_bank, new_bank->block));
113 }
114
115 assert(i >= s->objsize);
116
117 i -= s->objsize;
118 s->free_index = i;
119 tmp = s->bnk->block + i;
120
121 assert(ptr_is_aligned(tmp));
122
123 return tmp;
124 }
125
objstore_alloc(object_store_t * s)126 void *objstore_alloc(object_store_t *s) {
127 MT_PROTECT(void *, s->lock, _o_objstore_alloc(s));
128 }
129
130
131 /*
132 * Delete all objects
133 */
_o_delete_objstore(object_store_t * s)134 static void _o_delete_objstore(object_store_t *s) {
135 object_bank_t *b, *next;
136
137 b = s->bnk;
138 while (b != NULL) {
139 next = b->h.next;
140 safe_free(b);
141 b = next;
142 }
143
144 s->bnk = NULL;
145 s->free_list = NULL;
146 s->free_index = 0;
147 }
148
delete_objstore(object_store_t * s)149 void delete_objstore(object_store_t *s) {
150 MT_PROTECT_VOID(s->lock, _o_delete_objstore(s));
151 #ifdef THREAD_SAFE
152 destroy_yices_lock(&(s->lock));
153 #endif
154 }
155
156 /*
157 * Free an allocated object: add it to s->free_list.
158 * next pointer is stored in *object
159 */
_o_objstore_free(object_store_t * s,void * object)160 static void _o_objstore_free(object_store_t *s, void *object) {
161 /*
162 * BUG: This violates the strict aliasing rules and causes
163 * errors when optimizations are enabled?
164 */
165 // * ((void **) object) = s->free_list;
166 // Try this instead.
167 memcpy(object, &s->free_list, sizeof(void*));
168 s->free_list = object;
169 }
objstore_free(object_store_t * s,void * object)170 void objstore_free(object_store_t *s, void *object) {
171 MT_PROTECT_VOID(s->lock, _o_objstore_free(s, object));
172 }
173
174 /*
175 * Apply finalizer f to all objects then delete s
176 */
_o_objstore_delete_finalize(object_store_t * s,void (* f)(void *))177 static void _o_objstore_delete_finalize(object_store_t *s, void (*f)(void *)) {
178 object_bank_t *b, *next;
179 void *obj;
180 uint32_t k, i;
181
182 b = s->bnk;
183 k = s->free_index;
184 while (b != NULL) {
185 next = b->h.next;
186 for (i=k; i<s->blocksize; i += s->objsize) {
187 obj = (void *) (b->block + i);
188 f(obj);
189 }
190 safe_free(b);
191 k = 0;
192 b = next;
193 }
194
195 s->bnk = NULL;
196 s->free_list = NULL;
197 s->free_index = 0;
198 }
objstore_delete_finalize(object_store_t * s,void (* f)(void *))199 void objstore_delete_finalize(object_store_t *s, void (*f)(void *)) {
200 MT_PROTECT_VOID(s->lock, _o_objstore_delete_finalize(s, f));
201 #ifdef THREAD_SAFE
202 destroy_yices_lock(&(s->lock));
203 #endif
204 }
205
206
207 /*
208 * Reset store s: remove all objects
209 * - keep only one bank
210 */
_o_reset_objstore(object_store_t * s)211 static void _o_reset_objstore(object_store_t *s) {
212 object_bank_t *b, *next;
213
214 b = s->bnk;
215 if (b != NULL) {
216 next = b->h.next;
217 while (next != NULL) {
218 safe_free(b);
219 b = next;
220 next = b->h.next;
221 }
222 }
223
224 s->bnk = b;
225 s->free_list = NULL;
226 s->free_index = 0;
227 }
reset_objstore(object_store_t * s)228 void reset_objstore(object_store_t *s) {
229 MT_PROTECT_VOID(s->lock, _o_reset_objstore(s));
230 }
231