16032530443

Committed 02 Jul 2025 06:08PM UTC coverage: 60.349% (-5.0%) from 65.357%

Build # 16032530443

Build Type

Pull #582

github

Committed by

web-flow

Commit Message

Merge b7e09d316 into b3af64ab1

Pull Request Pull Request #582: Update ci

Coverage Stats

63716 of 105580 relevant lines covered (60.35%)

1127640.75 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

84.3

/src/utils/int_hash_map2.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

/*
 * MAPS PAIRS OF 32BIT INTEGERS TO 32BIT INTEGERS
 *
 * The keys must be non-negative.
 * Supported operations: addition/query/garbage collection.
 * Removal of individual records is not supported.
 */

#include <assert.h>

#include "utils/int_hash_map2.h"
#include "utils/memalloc.h"


/*
 * For debugging: check whether n is 0 or a power of 2
 */
#ifndef NDEBUG
static bool is_power_of_two(uint32_t n) {
  return (n & (n - 1)) == 0;
}
#endif



/*
 * Initialization:
 * - n = initial size (must be 0 or a power of 2)
 * - if n = 0, the default size is used
 */
void init_int_hmap2(int_hmap2_t *hmap, uint32_t n) {
  int_hmap2_rec_t *tmp;
  uint32_t i;

  if (n == 0) {
    n = INT_HMAP2_DEF_SIZE;
  }

  if (n >= INT_HMAP2_MAX_SIZE) {
    out_of_memory();
  }

  assert(is_power_of_two(n));

  tmp = (int_hmap2_rec_t *) safe_malloc(n * sizeof(int_hmap2_rec_t));
  for (i=0; i<n; i++) {
    tmp[i].k0 = INT_HMAP2_EMPTY;
  }

  hmap->data = tmp;
  hmap->size = n;
  hmap->nelems = 0;
  hmap->resize_threshold = (uint32_t) (n * INT_HMAP2_RESIZE_RATIO);
}


/*
 * Free memory
 */
void delete_int_hmap2(int_hmap2_t *hmap) {
  safe_free(hmap->data);
  hmap->data = NULL;
}



/*
 * Hash a pair (k0, k1): Jenkins's hash.
 */

/* Jenkins's lookup3 code */
#define rot(x,k) (((x)<<(k)) | ((x)>>(32-(k))))

#define final(a,b,c)      \
{                         \
  c ^= b; c -= rot(b,14); \
  a ^= c; a -= rot(c,11); \
  b ^= a; b -= rot(a,25); \
  c ^= b; c -= rot(b,16); \
  a ^= c; a -= rot(c,4);  \
  b ^= a; b -= rot(a,14); \
  c ^= b; c -= rot(b,24); \
}

static uint32_t hash_pair(int32_t k0, int32_t k1) {
  uint32_t x, y, z;

  x = (uint32_t) k0;
  y = (uint32_t) k1;
  z = 0xdeadbeef;
  final(x, y, z);

  return z;
}



/*
 * Copy record d into a clean array
 * - data = array (its size must be 2^k for k>0)
 * - mask = 2^k-1
 * - data must not be full
 */
static void int_hmap2_clean_copy(int_hmap2_rec_t *data, int_hmap2_rec_t *r, uint32_t mask) {
  uint32_t j;

  j = hash_pair(r->k0, r->k1) & mask;
  while (data[j].k0 >= 0) {
    j ++;
    j &= mask;
  }
  data[j] = *r;
}



/*
 * Double the table size (keep the content).
 */
static void int_hmap2_extend(int_hmap2_t *hmap) {
  int_hmap2_rec_t *tmp, *r;
  uint32_t i, n, n2, mask;

  n = hmap->size;
  n2 = n<<1;
  if (n2 >= INT_HMAP2_MAX_SIZE) {
    out_of_memory();
  }

  assert(is_power_of_two(n2));

  tmp = (int_hmap2_rec_t *) safe_malloc(n2 * sizeof(int_hmap2_rec_t));
  for (i=0; i<n2; i++) {
    tmp[i].k0 = INT_HMAP2_EMPTY;
  }

  mask = n2 - 1;
  r = hmap->data;
  for (i=0; i<n; i++) {
    if (r->k0 >= 0) { // valid record
      int_hmap2_clean_copy(tmp, r, mask);
    }
    r ++;
  }

  safe_free(hmap->data);
  hmap->data = tmp;
  hmap->size = n2;

  hmap->resize_threshold = (uint32_t) (n2 * INT_HMAP2_RESIZE_RATIO);
}




/*
 * Find record with key (k0, kl)
 * - return NULL if that record is not in the table
 */
int_hmap2_rec_t *int_hmap2_find(const int_hmap2_t *hmap, int32_t k0, int32_t k1) {
  int_hmap2_rec_t *r;
  uint32_t i, mask;

  assert(k0 >= 0 && k1 >= 0 && hmap->nelems < hmap->size);

  mask = hmap->size - 1;
  i = hash_pair(k0, k1) & mask;
  for (;;) {
    r = hmap->data + i;
    if (r->k0 < 0) return NULL;
    if (r->k0 == k0 && r->k1 == k1) return r;
    i ++;
    i &= mask;
  }
}




/*
 * Add record (k0, k1) to the table after resizing
 * - return a pointer to the new record
 */
static int_hmap2_rec_t *get_clean(int_hmap2_t *hmap, int32_t k0, int32_t k1) {
  uint32_t j, mask;

  mask = hmap->size - 1;
  j = hash_pair(k0, k1) & mask;
  while (hmap->data[j].k0 >= 0) {
    j ++;
    j &= mask;
  }

  hmap->data[j].k0 = k0;
  hmap->data[j].k1 = k1;

  return hmap->data + j;
}


/*
 * Get record with key (k0, k1).
 * - if one is in the table return it and set *new to false.
 * - otherwise, create a fresh record with key (k0, k1), and
 *   set *new to false.
 * If a new record is created, val is not initialized.
 * - k0 and k2 must be non-negative.
 */
int_hmap2_rec_t *int_hmap2_get(int_hmap2_t *hmap, int32_t k0, int32_t k1, bool *new) {
  int_hmap2_rec_t *r;
  uint32_t i, mask;

  assert(k0 >= 0 && k1 >= 0 && hmap->nelems < hmap->size);

  *new = false;
  mask = hmap->size - 1;
  i = hash_pair(k0, k1) & mask;
  for (;;) {
    r = hmap->data + i;
    if (r->k0 < 0) break;
    if (r->k0 == k0 && r->k1 == k1) return r;
    i ++;
    i &= mask;
  }

  /*
   * add new record in hmap->data
   */
  *new = true;
  hmap->nelems ++;
  if (hmap->nelems >= hmap->resize_threshold) {
    // resize needed
    int_hmap2_extend(hmap);
    r = get_clean(hmap, k0, k1);
  } else {
    // add the new record in r
    r->k0 = k0;
    r->k1 = k1;
  }

  return r;
}



/*
 * Add record (k0, k1 :-> val) to hmap
 * - there must not be a record with the same key pair
 */
void int_hmap2_add(int_hmap2_t *hmap, int32_t k0, int32_t k1, int32_t val) {
  uint32_t i, mask;

  assert(k0 >= 0 && k1 >= 0 && hmap->nelems < hmap->size);

  mask = hmap->size - 1;
  i = hash_pair(k0, k1) & mask;
  while (hmap->data[i].k0 >= 0) {
    assert(hmap->data[i].k0 != k0 || hmap->data[i].k1 != k1);
    i ++;
    i &= mask;
  }

  // store the record in data[i]
  hmap->data[i].k0 = k0;
  hmap->data[i].k1 = k1;
  hmap->data[i].val = val;
  hmap->nelems ++;

  if (hmap->nelems >= hmap->resize_threshold) {
    int_hmap2_extend(hmap);
  }
}





/*
 * Empty the table
 */
void reset_int_hmap2(int_hmap2_t *hmap) {
  int_hmap2_rec_t *r;
  uint32_t i, n;

  r = hmap->data;
  n = hmap->size;
  for (i=0; i<n; i++) {
    r->k0 = INT_HMAP2_EMPTY;
    r ++;
  }

  hmap->nelems = 0;
}



/*
 * Garbage collection:
 * - we call f(aux, r) on every record r in hmap.
 * - if f returns true we keep r, otherwise we delete it.
 * We do this by copying the content into a new array, which
 * may be somewhat expensive if most records are kept.
 */
void int_hmap2_gc(int_hmap2_t *hmap, void *aux, keep_alive_fun_t f) {
  int_hmap2_rec_t *tmp, *r;
  uint32_t i, n, nelems, mask;

  n = hmap->size;
  tmp = (int_hmap2_rec_t *) safe_malloc(n * sizeof(int_hmap2_rec_t));
  for (i=0; i<n; i++) {
    tmp[i].k0 = INT_HMAP2_EMPTY;
  }

  nelems = 0;    // number of elements kept
  mask = n - 1;
  r = hmap->data;
  for (i=0; i<n; i++) {
    if (r->k0 >= 0 && f(aux, r)) {
      // keep r
      int_hmap2_clean_copy(tmp, r, mask);
      nelems ++;
    }
    r ++;
  }

  safe_free(hmap->data);
  hmap->data = tmp;
  hmap->nelems = nelems;
}

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	* MAPS PAIRS OF 32BIT INTEGERS TO 32BIT INTEGERS
21	*
22	* The keys must be non-negative.
23	* Supported operations: addition/query/garbage collection.
24	* Removal of individual records is not supported.
25	*/
26
27	#include <assert.h>
28
29	#include "utils/int_hash_map2.h"
30	#include "utils/memalloc.h"
31
32
33	/*
34	* For debugging: check whether n is 0 or a power of 2
35	*/
36	#ifndef NDEBUG
37	static bool is_power_of_two(uint32_t n) {
38	return (n & (n - 1)) == 0;
39	}
40	#endif
41
42
43
44	/*
45	* Initialization:
46	* - n = initial size (must be 0 or a power of 2)
47	* - if n = 0, the default size is used
48	*/
49	void init_int_hmap2(int_hmap2_t *hmap, uint32_t n) {	6✔
50	int_hmap2_rec_t *tmp;
51	uint32_t i;
52
53	if (n == 0) {	6✔
54	n = INT_HMAP2_DEF_SIZE;	6✔
55	}
56
57	if (n >= INT_HMAP2_MAX_SIZE) {	6✔
58	out_of_memory();	×
59	}
60
61	assert(is_power_of_two(n));
62
63	tmp = (int_hmap2_rec_t ) safe_malloc(n sizeof(int_hmap2_rec_t));	6✔
64	for (i=0; i<n; i++) {	198✔
65	tmp[i].k0 = INT_HMAP2_EMPTY;	192✔
66	}
67
68	hmap->data = tmp;	6✔
69	hmap->size = n;	6✔
70	hmap->nelems = 0;	6✔
71	hmap->resize_threshold = (uint32_t) (n * INT_HMAP2_RESIZE_RATIO);	6✔
72	}	6✔
73
74
75	/*
76	* Free memory
77	*/
78	void delete_int_hmap2(int_hmap2_t *hmap) {	6✔
79	safe_free(hmap->data);	6✔
80	hmap->data = NULL;	6✔
81	}	6✔
82
83
84
85	/*
86	* Hash a pair (k0, k1): Jenkins's hash.
87	*/
88
89	/* Jenkins's lookup3 code */
90	#define rot(x,k) (((x)<<(k)) \| ((x)>>(32-(k))))
91
92	#define final(a,b,c) \
93	{ \
94	c ^= b; c -= rot(b,14); \
95	a ^= c; a -= rot(c,11); \
96	b ^= a; b -= rot(a,25); \
97	c ^= b; c -= rot(b,16); \
98	a ^= c; a -= rot(c,4); \
99	b ^= a; b -= rot(a,14); \
100	c ^= b; c -= rot(b,24); \
101	}
102
103	static uint32_t hash_pair(int32_t k0, int32_t k1) {	148✔
104	uint32_t x, y, z;
105
106	x = (uint32_t) k0;	148✔
107	y = (uint32_t) k1;	148✔
108	z = 0xdeadbeef;	148✔
109	final(x, y, z);	148✔
110
111	return z;	148✔
112	}
113
114
115
116	/*
117	* Copy record d into a clean array
118	* - data = array (its size must be 2^k for k>0)
119	* - mask = 2^k-1
120	* - data must not be full
121	*/
122	static void int_hmap2_clean_copy(int_hmap2_rec_t data, int_hmap2_rec_t r, uint32_t mask) {	55✔
123	uint32_t j;
124
125	j = hash_pair(r->k0, r->k1) & mask;	55✔
126	while (data[j].k0 >= 0) {	74✔
127	j ++;	19✔
128	j &= mask;	19✔
129	}
130	data[j] = *r;	55✔
131	}	55✔
132
133
134
135	/*
136	* Double the table size (keep the content).
137	*/
138	static void int_hmap2_extend(int_hmap2_t *hmap) {	2✔
139	int_hmap2_rec_t tmp, r;
140	uint32_t i, n, n2, mask;
141
142	n = hmap->size;	2✔
143	n2 = n<<1;	2✔
144	if (n2 >= INT_HMAP2_MAX_SIZE) {	2✔
145	out_of_memory();	×
146	}
147
148	assert(is_power_of_two(n2));
149
150	tmp = (int_hmap2_rec_t ) safe_malloc(n2 sizeof(int_hmap2_rec_t));	2✔
151	for (i=0; i<n2; i++) {	194✔
152	tmp[i].k0 = INT_HMAP2_EMPTY;	192✔
153	}
154
155	mask = n2 - 1;	2✔
156	r = hmap->data;	2✔
157	for (i=0; i<n; i++) {	98✔
158	if (r->k0 >= 0) { // valid record	96✔
159	int_hmap2_clean_copy(tmp, r, mask);	55✔
160	}
161	r ++;	96✔
162	}
163
164	safe_free(hmap->data);	2✔
165	hmap->data = tmp;	2✔
166	hmap->size = n2;	2✔
167
168	hmap->resize_threshold = (uint32_t) (n2 * INT_HMAP2_RESIZE_RATIO);	2✔
169	}	2✔
170
171
172
173
174	/*
175	* Find record with key (k0, kl)
176	* - return NULL if that record is not in the table
177	*/
178	int_hmap2_rec_t int_hmap2_find(const int_hmap2_t hmap, int32_t k0, int32_t k1) {	33✔
179	int_hmap2_rec_t *r;
180	uint32_t i, mask;
181
182	assert(k0 >= 0 && k1 >= 0 && hmap->nelems < hmap->size);
183
184	mask = hmap->size - 1;	33✔
185	i = hash_pair(k0, k1) & mask;	33✔
186	for (;;) {
187	r = hmap->data + i;	33✔
188	if (r->k0 < 0) return NULL;	33✔
189	if (r->k0 == k0 && r->k1 == k1) return r;	25✔
190	i ++;	×
191	i &= mask;	×
192	}
193	}
194
195
196
197
198	/*
199	* Add record (k0, k1) to the table after resizing
200	* - return a pointer to the new record
201	*/
202	static int_hmap2_rec_t get_clean(int_hmap2_t hmap, int32_t k0, int32_t k1) {	2✔
203	uint32_t j, mask;
204
205	mask = hmap->size - 1;	2✔
206	j = hash_pair(k0, k1) & mask;	2✔
207	while (hmap->data[j].k0 >= 0) {	2✔
208	j ++;	×
209	j &= mask;	×
210	}
211
212	hmap->data[j].k0 = k0;	2✔
213	hmap->data[j].k1 = k1;	2✔
214
215	return hmap->data + j;	2✔
216	}
217
218
219	/*
220	* Get record with key (k0, k1).
221	* - if one is in the table return it and set *new to false.
222	* - otherwise, create a fresh record with key (k0, k1), and
223	* set *new to false.
224	* If a new record is created, val is not initialized.
225	* - k0 and k2 must be non-negative.
226	*/
227	int_hmap2_rec_t int_hmap2_get(int_hmap2_t hmap, int32_t k0, int32_t k1, bool *new) {	50✔
228	int_hmap2_rec_t *r;
229	uint32_t i, mask;
230
231	assert(k0 >= 0 && k1 >= 0 && hmap->nelems < hmap->size);
232
233	*new = false;	50✔
234	mask = hmap->size - 1;	50✔
235	i = hash_pair(k0, k1) & mask;	50✔
236	for (;;) {
237	r = hmap->data + i;	96✔
238	if (r->k0 < 0) break;	96✔
239	if (r->k0 == k0 && r->k1 == k1) return r;	53✔
240	i ++;	46✔
241	i &= mask;	46✔
242	}
243
244	/*
245	* add new record in hmap->data
246	*/
247	*new = true;	43✔
248	hmap->nelems ++;	43✔
249	if (hmap->nelems >= hmap->resize_threshold) {	43✔
250	// resize needed
251	int_hmap2_extend(hmap);	2✔
252	r = get_clean(hmap, k0, k1);	2✔
253	} else {
254	// add the new record in r
255	r->k0 = k0;	41✔
256	r->k1 = k1;	41✔
257	}
258
259	return r;	43✔
260	}
261
262
263
264	/*
265	* Add record (k0, k1 :-> val) to hmap
266	* - there must not be a record with the same key pair
267	*/
268	void int_hmap2_add(int_hmap2_t *hmap, int32_t k0, int32_t k1, int32_t val) {	8✔
269	uint32_t i, mask;
270
271	assert(k0 >= 0 && k1 >= 0 && hmap->nelems < hmap->size);
272
273	mask = hmap->size - 1;	8✔
274	i = hash_pair(k0, k1) & mask;	8✔
275	while (hmap->data[i].k0 >= 0) {	8✔
276	assert(hmap->data[i].k0 != k0 \|\| hmap->data[i].k1 != k1);
277	i ++;	×
278	i &= mask;	×
279	}
280
281	// store the record in data[i]
282	hmap->data[i].k0 = k0;	8✔
283	hmap->data[i].k1 = k1;	8✔
284	hmap->data[i].val = val;	8✔
285	hmap->nelems ++;	8✔
286
287	if (hmap->nelems >= hmap->resize_threshold) {	8✔
288	int_hmap2_extend(hmap);	×
289	}
290	}	8✔
291
292
293
294
295
296	/*
297	* Empty the table
298	*/
299	void reset_int_hmap2(int_hmap2_t *hmap) {	×
300	int_hmap2_rec_t *r;
301	uint32_t i, n;
302
303	r = hmap->data;	×
304	n = hmap->size;	×
305	for (i=0; i<n; i++) {	×
306	r->k0 = INT_HMAP2_EMPTY;	×
307	r ++;	×
308	}
309
310	hmap->nelems = 0;	×
311	}	×
312
313
314
315	/*
316	* Garbage collection:
317	* - we call f(aux, r) on every record r in hmap.
318	* - if f returns true we keep r, otherwise we delete it.
319	* We do this by copying the content into a new array, which
320	* may be somewhat expensive if most records are kept.
321	*/
322	void int_hmap2_gc(int_hmap2_t hmap, void aux, keep_alive_fun_t f) {	1✔
323	int_hmap2_rec_t tmp, r;
324	uint32_t i, n, nelems, mask;
325
326	n = hmap->size;	1✔
327	tmp = (int_hmap2_rec_t ) safe_malloc(n sizeof(int_hmap2_rec_t));	1✔
328	for (i=0; i<n; i++) {	33✔
329	tmp[i].k0 = INT_HMAP2_EMPTY;	32✔
330	}
331
332	nelems = 0; // number of elements kept	1✔
333	mask = n - 1;	1✔
334	r = hmap->data;	1✔
335	for (i=0; i<n; i++) {	33✔
336	if (r->k0 >= 0 && f(aux, r)) {	32✔
337	// keep r
338	int_hmap2_clean_copy(tmp, r, mask);	×
339	nelems ++;	×
340	}
341	r ++;	32✔
342	}
343
344	safe_free(hmap->data);	1✔
345	hmap->data = tmp;	1✔
346	hmap->nelems = nelems;	1✔
347	}	1✔

SRI-CSL / yices2 / 16032530443

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous