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