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