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  * STORES FOR ALLOCATION/RELEASE OF (SMALL) OBJECTS OF FIXED SIZE.
21  */
22 
23 #ifndef __OBJECT_STORES_H
24 #define __OBJECT_STORES_H
25 
26 #include <stdint.h>
27 #include <string.h>
28 
29 #include "mt/yices_locks.h"
30 
31 /*
32  * Bank = a block of objects
33  * - blocks are linked in a list
34  * - for correct pointer alignment, we (try to) force the offset
35  *   (bank->block - bank) to be a multiple of 8)
36  * - we also force object sizes to be multiple of 8 bytes
37  *
38  * All this is based on the assumption that addresses that are
39  * multiple of 8 have the right alignment for all hardware we
40  * support.
41  */
42 typedef struct object_bank_s object_bank_t;
43 
44 struct object_bank_s {
45   union {
46     object_bank_t *next;
47     char padding[8]; // for alignment
48   } h;
49   char block[0]; // real size determined at allocation time
50 };
51 
52 /*
53  * Store = a list of blocks
54  * - allocations are performed via a free list,
55  * - or in the first block of the bank list,
56  * - or by adding a new block.
57  */
58 typedef struct object_store_s {
59 #ifdef THREAD_SAFE
60   yices_lock_t lock;   // a lock protecting the object_store
61 #endif
62   object_bank_t *bnk;  // first block in the bank list
63   void *free_list;
64   uint32_t free_index; // index of last allocated object in first block
65   uint32_t objsize;    // size of all objects (in bytes)
66   uint32_t blocksize;  // size of blocks (multiple of objsize).
67 } object_store_t;
68 
69 
70 /*
71  * Bounds on objsize and nobj per block: to avoid numerical overflows,
72  * we need objsize * nobj <= UINT32_MAX.  Stores are intended for
73  * small objects so the following bounds should be more than enough.
74  */
75 #define MAX_OBJ_SIZE 512
76 #define MAX_OBJ_PER_BLOCK 4096
77 
78 
79 /*
80  * Initialize store s for object of the given size
81  * - n = number of objects in each block
82  */
83 extern void init_objstore(object_store_t *s, uint32_t objsize, uint32_t n);
84 
85 /*
86  * Delete the full store: all banks are freed
87  */
88 extern void delete_objstore(object_store_t *s);
89 
90 /*
91  * Reset the store: remove all objects
92  */
93 extern void reset_objstore(object_store_t *s);
94 
95 
96 /*
97  * Delete with finalizer: apply function f to all
98  * objects in the store before freeing the banks.
99  */
100 extern void objstore_delete_finalize(object_store_t *s, void (*f)(void *));
101 
102 /*
103  * Allocate an object
104  */
105 extern void *objstore_alloc(object_store_t *s);
106 
107 /*
108  * Free an allocated object: add it to s->free_list.
109  * next pointer is stored in *object
110  */
111 extern void objstore_free(object_store_t *s, void *object);
112 
113 
114 #endif /* __OBJECT_STORES_H */
115