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 * USE VECTOR = VECTOR OF POINTERS TO TERMS OR OTHER OBJECTS
21 */
22
23 #ifndef __USE_VECTORS_H
24 #define __USE_VECTORS_H
25
26 #include <stddef.h>
27 #include <stdint.h>
28 #include <stdbool.h>
29 #include <assert.h>
30
31
32
33 /*
34 * - data is an array of pointers
35 * - the used entries are data[0 ... last-1]
36 * - the unused entries are data[last ... size-1]
37 * - every entry in data[0 ... last-1] contains a tagged pointer
38 * - the tag is in the two low-order bits
39 * if tag = 00, data[i] = a pointer to some object
40 * if tag = 01, data[i] = pointer with a special mark
41 * if tag = 11, data[i] is empty, and data[i]>>2 is
42 * an index in the data array used to maintain a free list
43 */
44 typedef struct use_vector_s {
45 void **data; // array of pointers
46 uint32_t size; // size of data array
47 uint32_t last; // first unused entry
48 uint32_t nelems; // number of valid entries (not marked or deleted)
49 int32_t free; // start of the free list or -1
50 } use_vector_t;
51
52
53
54 /*
55 * Maximal size
56 */
57 #define MAX_USE_VECTOR_SIZE (UINT32_MAX/8)
58
59 /*
60 * Minimum size after the first extension
61 */
62 #define DEFAULT_USE_VECTOR_SIZE 8
63
64
65 /*
66 * Tags
67 */
68 typedef enum uv_tag {
69 valid_tag = 0, // pointer: tag = 0b00
70 mark_tag = 1, // pointer with mark
71 free_tag = 3, // empty entry: tag = 0b11
72 } uv_tag_t;
73
74 #define TAG_MASK ((uintptr_t) 0x3)
75
76 /*
77 * Get the tag of p
78 */
entry_tag(void * p)79 static inline uv_tag_t entry_tag(void *p) {
80 return ((uintptr_t) p) & TAG_MASK;
81 }
82
83 /*
84 * Checks on a vector element p
85 */
valid_entry(void * p)86 static inline bool valid_entry(void *p) {
87 return entry_tag(p) == valid_tag;
88 }
89
marked_entry(void * p)90 static inline bool marked_entry(void *p) {
91 return entry_tag(p) == mark_tag;
92 }
93
empty_entry(void * p)94 static inline bool empty_entry(void *p) {
95 return entry_tag(p) == free_tag;
96 }
97
98
entry2index(void * p)99 static inline int32_t entry2index(void *p) {
100 return ((int32_t)((uintptr_t) p)) >> 2;
101 }
102
index2entry(int32_t idx)103 static inline void *index2entry(int32_t idx) {
104 return (void *) ((((uintptr_t) idx) << 2) | free_tag);
105 }
106
unmark_entry(void * p)107 static inline void *unmark_entry(void *p) {
108 return (void*)(((uintptr_t) p) & ~TAG_MASK);
109 }
110
mark_entry(void * p)111 static inline void *mark_entry(void *p) {
112 return (void*)(((uintptr_t) p) | mark_tag);
113 }
114
115
116 /*
117 * Initialization: n = initial size
118 */
119 extern void init_use_vector(use_vector_t *v, uint32_t n);
120
121
122 /*
123 * Resize: make size at least equal to n (no change if it's already
124 * large enough).
125 */
126 extern void resize_use_vector(use_vector_t *v, uint32_t n);
127
128
129 /*
130 * Deletion
131 */
132 extern void delete_use_vector(use_vector_t *v);
133
134
135 /*
136 * Allocate an entry in the data array
137 * - return its index in data
138 */
139 extern int32_t alloc_use_vector_entry(use_vector_t *v);
140
141
142 /*
143 * Check whether v is empty
144 */
empty_use_vector(use_vector_t * v)145 static inline bool empty_use_vector(use_vector_t *v) {
146 return v->nelems == 0;
147 }
148
149 /*
150 * Reset: empty the whole vector
151 */
reset_use_vector(use_vector_t * v)152 static inline void reset_use_vector(use_vector_t *v) {
153 v->free = -1;
154 v->nelems = 0;
155 v->last = 0;
156 }
157
158 /*
159 * Clear entry i: mark it as empty, add it to the free list
160 */
clear_use_vector_entry(use_vector_t * v,int32_t i)161 static inline void clear_use_vector_entry(use_vector_t *v, int32_t i) {
162 assert(0 <= i && i < (int32_t) v->last && valid_entry(v->data[i]));
163 v->data[i] = index2entry(v->free);
164 v->free = i;
165 v->nelems --;
166 }
167
168
169 /*
170 * Mark entry i: set tag to mark_tag
171 */
mark_use_vector_entry(use_vector_t * v,int32_t i)172 static inline void mark_use_vector_entry(use_vector_t *v, int32_t i) {
173 assert(0 <= i && i < (int32_t) v->last && valid_entry(v->data[i]));
174 v->data[i] = mark_entry(v->data[i]);
175 v->nelems --;
176 }
177
178
179 /*
180 * Remove mark on entry i: set tag to valid_tag
181 */
unmark_use_vector_entry(use_vector_t * v,int32_t i)182 static inline void unmark_use_vector_entry(use_vector_t *v, int32_t i) {
183 assert(0 <= i && i < (int32_t) v->last && marked_entry(v->data[i]));
184 v->data[i] = unmark_entry(v->data[i]);
185 v->nelems ++;
186 }
187
188 /*
189 * Store ptr in a new entry and return its index
190 */
use_vector_store(use_vector_t * v,void * ptr)191 static inline int32_t use_vector_store(use_vector_t *v, void *ptr) {
192 int32_t i;
193 assert(valid_entry(ptr));
194 i = alloc_use_vector_entry(v);
195 v->data[i] = ptr;
196 v->nelems ++;
197 return i;
198 }
199
200
201
202
203 #endif /* __USE_VECTORS_H */
204