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

Run Details

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

86.93

/src/utils/ptr_hash_map.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/>.
 */

/*
 * HASH MAPS
 * - keys are 32bit integers, values are void * pointers
 * - keys are assumed positive, -1 and -2 are special markers
 */

#include <stdbool.h>
#include <assert.h>

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


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


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

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

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

  assert(is_power_of_two(n));

  tmp = (ptr_hmap_pair_t *) safe_malloc(n * sizeof(ptr_hmap_pair_t));
  for (i=0; i<n; i++) {
    tmp[i].key = PHMAP_EMPTY_KEY;
  }

  hmap->data = tmp;
  hmap->size = n;
  hmap->nelems = 0;
  hmap->ndeleted = 0;

  hmap->resize_threshold = (uint32_t)(n * PTR_HMAP_RESIZE_RATIO);
  hmap->cleanup_threshold = (uint32_t) (n * PTR_HMAP_CLEANUP_RATIO);
}


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


/*
 * Hash of a key (Jenkins hash)
 */
static uint32_t hash_key(int32_t k) {
  uint32_t x;

  x = (uint32_t) k;
  x = (x + 0x7ed55d16) + (x<<12);
  x = (x ^ 0xc761c23c) ^ (x>>19);
  x = (x + 0x165667b1) + (x<<5);
  x = (x + 0xd3a2646c) ^ (x<<9);
  x = (x + 0xfd7046c5) + (x<<3);
  x = (x ^ 0xb55a4f09) ^ (x>>16);

  return x;
}

/*
 * Make a copy of record d in a clean array data
 * - mask = size of data - 1 (size must be a power of 2)
 */
static void ptr_hmap_clean_copy(ptr_hmap_pair_t *data, ptr_hmap_pair_t *d, uint32_t mask) {
  uint32_t j;

  j = hash_key(d->key) & mask;
  while (data[j].key != PHMAP_EMPTY_KEY) {
    j ++;
    j &= mask;
  }

  data[j].key = d->key;
  data[j].val = d->val;
}


/*
 * Remove deleted records
 */
static void ptr_hmap_cleanup(ptr_hmap_t *hmap) {
  ptr_hmap_pair_t *tmp, *d;
  uint32_t j, n, mask;

  n = hmap->size;
  tmp = (ptr_hmap_pair_t *) safe_malloc(n * sizeof(ptr_hmap_pair_t));
  for (j=0; j<n; j++) {
    tmp[j].key = PHMAP_EMPTY_KEY;
  }

  mask = n - 1;
  d = hmap->data;
  for (j=0; j<n; j++) {
    if (d->key >= 0) {
      ptr_hmap_clean_copy(tmp, d, mask);
    }
    d++;
  }

  safe_free(hmap->data);
  hmap->data = tmp;
  hmap->ndeleted = 0;
}


/*
 * Remove deleted records and make the table twice as large
 */
static void ptr_hmap_extend(ptr_hmap_t *hmap) {
  ptr_hmap_pair_t *tmp, *d;
  uint32_t j, n, n2, mask;

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

  tmp = (ptr_hmap_pair_t *) safe_malloc(n2 * sizeof(ptr_hmap_pair_t));
  for (j=0; j<n2; j++) {
    tmp[j].key = PHMAP_EMPTY_KEY;
  }

  mask = n2 - 1;
  d = hmap->data;
  for (j=0; j<n; j++) {
    if (d->key >= 0) {
      ptr_hmap_clean_copy(tmp, d, mask);
    }
    d ++;
  }

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

  hmap->resize_threshold = (uint32_t)(n2 * PTR_HMAP_RESIZE_RATIO);
  hmap->cleanup_threshold = (uint32_t)(n2 * PTR_HMAP_CLEANUP_RATIO);
}


/*
 * Find record with key k
 * - return NULL if k is not in the table
 */
ptr_hmap_pair_t *ptr_hmap_find(const ptr_hmap_t *hmap, int32_t k) {
  uint32_t mask, j;
  ptr_hmap_pair_t *d;

  assert(k >= 0);

  mask = hmap->size - 1;
  j = hash_key(k) & mask;
  for (;;) {
    d = hmap->data + j;
    if (d->key == k) return d;
    if (d->key == PHMAP_EMPTY_KEY) return NULL;
    j ++;
    j &= mask;
  }
}


/*
 * Add record with key k after hmap was extended:
 * - initialize val to NULL
 * - we know that no record with key k is present
 */
static ptr_hmap_pair_t *ptr_hmap_get_clean(ptr_hmap_t *hmap, int32_t k) {
  uint32_t mask, j;
  ptr_hmap_pair_t *d;

  mask = hmap->size - 1;
  j = hash_key(k) & mask;
  for (;;) {
    d = hmap->data + j;
    if (d->key < 0) {
      hmap->nelems ++;
      d->key = k;
      d->val = NULL;
      return d;
    }
    j ++;
    j &= mask;
  }
}


/*
 * Find or add record with key k
 */
ptr_hmap_pair_t *ptr_hmap_get(ptr_hmap_t *hmap, int32_t k) {
  uint32_t mask, j;
  ptr_hmap_pair_t *d, *aux;

  assert(k >= 0);
  assert(hmap->size > hmap->ndeleted + hmap->nelems);

  mask = hmap->size - 1;
  j = hash_key(k) & mask;

  for (;;) {
    d = hmap->data + j;
    if (d->key == k) return d;
    if (d->key < 0) break;
    j ++;
    j &= mask;
  }

  aux = d; // new record, if needed, will be aux
  while (d->key != PHMAP_EMPTY_KEY) {
    j ++;
    j &= mask;
    d = hmap->data + j;
    if (d->key == k) return d;
  }

  if (aux->key == PHMAP_DEL_KEY) {
    assert(hmap->ndeleted > 0);
    hmap->ndeleted --;
  }

  if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {
    ptr_hmap_extend(hmap);
    aux = ptr_hmap_get_clean(hmap, k);
  } else {
    hmap->nelems ++;
    aux->key = k;
    aux->val = NULL;
  }

  return aux;
}


/*
 * Erase record r
 */
void ptr_hmap_erase(ptr_hmap_t *hmap, ptr_hmap_pair_t *r) {
  assert(ptr_hmap_find(hmap, r->key) == r);

  r->key = PHMAP_DEL_KEY;
  hmap->nelems --;
  hmap->ndeleted ++;
  if (hmap->ndeleted > hmap->cleanup_threshold) {
    ptr_hmap_cleanup(hmap);
  }
}


/*
 * Empty the map
 */
void ptr_hmap_reset(ptr_hmap_t *hmap) {
  uint32_t i, n;
  ptr_hmap_pair_t *d;

  n = hmap->size;
  d = hmap->data;
  for (i=0; i<n; i++) {
    d->key = PHMAP_EMPTY_KEY;
    d ++;
  }

  hmap->nelems = 0;
  hmap->ndeleted = 0;
}


/*
 * Remove all records that satisfy f
 * - for every record r in the table, call f(aux, r)
 * - if that returns true, then the record r is deleted
 * - f must not have side effects
 */
void ptr_hmap_remove_records(ptr_hmap_t *hmap, void *aux, ptr_hmap_filter_t f) {
  ptr_hmap_pair_t *d;
  uint32_t i, n, k;

  n = hmap->size;
  d = hmap->data;
  k = 0;
  for (i=0; i<n; i++) {
    if (d->key >= 0 && f(aux, d)) {
      d->key = PHMAP_DEL_KEY;
      k ++;
    }
  }

  // k = number of deletions
  assert(k <= hmap->nelems);
  hmap->nelems -= k;
  hmap->ndeleted += k;
  if (hmap->ndeleted >= hmap->cleanup_threshold) {
    ptr_hmap_cleanup(hmap);
  }
}



/*
 * First non-empty record in the table, starting from p
 */
static const ptr_hmap_pair_t *ptr_hmap_get_next(const ptr_hmap_t *hmap, const ptr_hmap_pair_t *p) {
  ptr_hmap_pair_t *end;

  end = hmap->data + hmap->size;
  while (p < end) {
    if (p->key >= 0) return p;
    p ++;
  }

  return NULL;
}


/*
 * Get the first non-empty record or NULL if the table is empty
 */
ptr_hmap_pair_t *ptr_hmap_first_record(const ptr_hmap_t *hmap) {
  return (ptr_hmap_pair_t *) ptr_hmap_get_next(hmap, hmap->data);
}


/*
 * Next record after p or NULL
 */
ptr_hmap_pair_t *ptr_hmap_next_record(const ptr_hmap_t *hmap, const ptr_hmap_pair_t *p) {
  assert(p != NULL && p<hmap->data + hmap->size && p->key >= 0);
  return (ptr_hmap_pair_t *) ptr_hmap_get_next(hmap, p+1);
}



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	* HASH MAPS
21	* - keys are 32bit integers, values are void * pointers
22	* - keys are assumed positive, -1 and -2 are special markers
23	*/
24
25	#include <stdbool.h>
26	#include <assert.h>
27
28	#include "utils/memalloc.h"
29	#include "utils/ptr_hash_map.h"
30
31
32	/*
33	* For debugging: check whether n is a power of two
34	*/
35	#ifndef NDEBUG
36	static bool is_power_of_two(uint32_t n) {
37	return (n & (n - 1)) == 0;
38	}
39	#endif
40
41
42	/*
43	* Initialization:
44	* - n = initial size, must be a power of 2
45	* - if n = 0, the default size is used
46	*/
47	void init_ptr_hmap(ptr_hmap_t *hmap, uint32_t n) {	18,812✔
48	uint32_t i;
49	ptr_hmap_pair_t *tmp;
50
51	if (n == 0) {	18,812✔
52	n = PTR_HMAP_DEFAULT_SIZE;	18,812✔
53	}
54
55	if (n >= PTR_HMAP_MAX_SIZE) {	18,812✔
56	out_of_memory();	×
57	}
58
59	assert(is_power_of_two(n));
60
61	tmp = (ptr_hmap_pair_t ) safe_malloc(n sizeof(ptr_hmap_pair_t));	18,812✔
62	for (i=0; i<n; i++) {	620,796✔
63	tmp[i].key = PHMAP_EMPTY_KEY;	601,984✔
64	}
65
66	hmap->data = tmp;	18,812✔
67	hmap->size = n;	18,812✔
68	hmap->nelems = 0;	18,812✔
69	hmap->ndeleted = 0;	18,812✔
70
71	hmap->resize_threshold = (uint32_t)(n * PTR_HMAP_RESIZE_RATIO);	18,812✔
72	hmap->cleanup_threshold = (uint32_t) (n * PTR_HMAP_CLEANUP_RATIO);	18,812✔
73	}	18,812✔
74
75
76	/*
77	* Free memory
78	*/
79	void delete_ptr_hmap(ptr_hmap_t *hmap) {	18,812✔
80	safe_free(hmap->data);	18,812✔
81	hmap->data = NULL;	18,812✔
82	}	18,812✔
83
84
85	/*
86	* Hash of a key (Jenkins hash)
87	*/
88	static uint32_t hash_key(int32_t k) {	1,488,317✔
89	uint32_t x;
90
91	x = (uint32_t) k;	1,488,317✔
92	x = (x + 0x7ed55d16) + (x<<12);	1,488,317✔
93	x = (x ^ 0xc761c23c) ^ (x>>19);	1,488,317✔
94	x = (x + 0x165667b1) + (x<<5);	1,488,317✔
95	x = (x + 0xd3a2646c) ^ (x<<9);	1,488,317✔
96	x = (x + 0xfd7046c5) + (x<<3);	1,488,317✔
97	x = (x ^ 0xb55a4f09) ^ (x>>16);	1,488,317✔
98
99	return x;	1,488,317✔
100	}
101
102	/*
103	* Make a copy of record d in a clean array data
104	* - mask = size of data - 1 (size must be a power of 2)
105	*/
106	static void ptr_hmap_clean_copy(ptr_hmap_pair_t data, ptr_hmap_pair_t d, uint32_t mask) {	389,610✔
107	uint32_t j;
108
109	j = hash_key(d->key) & mask;	389,610✔
110	while (data[j].key != PHMAP_EMPTY_KEY) {	472,837✔
111	j ++;	83,227✔
112	j &= mask;	83,227✔
113	}
114
115	data[j].key = d->key;	389,610✔
116	data[j].val = d->val;	389,610✔
117	}	389,610✔
118
119
120	/*
121	* Remove deleted records
122	*/
123	static void ptr_hmap_cleanup(ptr_hmap_t *hmap) {	2✔
124	ptr_hmap_pair_t tmp, d;
125	uint32_t j, n, mask;
126
127	n = hmap->size;	2✔
128	tmp = (ptr_hmap_pair_t ) safe_malloc(n sizeof(ptr_hmap_pair_t));	2✔
129	for (j=0; j<n; j++) {	8,194✔
130	tmp[j].key = PHMAP_EMPTY_KEY;	8,192✔
131	}
132
133	mask = n - 1;	2✔
134	d = hmap->data;	2✔
135	for (j=0; j<n; j++) {	8,194✔
136	if (d->key >= 0) {	8,192✔
137	ptr_hmap_clean_copy(tmp, d, mask);	896✔
138	}
139	d++;	8,192✔
140	}
141
142	safe_free(hmap->data);	2✔
143	hmap->data = tmp;	2✔
144	hmap->ndeleted = 0;	2✔
145	}	2✔
146
147
148	/*
149	* Remove deleted records and make the table twice as large
150	*/
151	static void ptr_hmap_extend(ptr_hmap_t *hmap) {	3,037✔
152	ptr_hmap_pair_t tmp, d;
153	uint32_t j, n, n2, mask;
154
155	n = hmap->size;	3,037✔
156	n2 = n << 1;	3,037✔
157	if (n2 >= PTR_HMAP_MAX_SIZE) {	3,037✔
158	out_of_memory();	×
159	}
160
161	tmp = (ptr_hmap_pair_t ) safe_malloc(n2 sizeof(ptr_hmap_pair_t));	3,037✔
162	for (j=0; j<n2; j++) {	1,302,941✔
163	tmp[j].key = PHMAP_EMPTY_KEY;	1,299,904✔
164	}
165
166	mask = n2 - 1;	3,037✔
167	d = hmap->data;	3,037✔
168	for (j=0; j<n; j++) {	652,989✔
169	if (d->key >= 0) {	649,952✔
170	ptr_hmap_clean_copy(tmp, d, mask);	388,714✔
171	}
172	d ++;	649,952✔
173	}
174
175	safe_free(hmap->data);	3,037✔
176	hmap->data = tmp;	3,037✔
177	hmap->size = n2;	3,037✔
178	hmap->ndeleted = 0;	3,037✔
179
180	hmap->resize_threshold = (uint32_t)(n2 * PTR_HMAP_RESIZE_RATIO);	3,037✔
181	hmap->cleanup_threshold = (uint32_t)(n2 * PTR_HMAP_CLEANUP_RATIO);	3,037✔
182	}	3,037✔
183
184
185	/*
186	* Find record with key k
187	* - return NULL if k is not in the table
188	*/
189	ptr_hmap_pair_t ptr_hmap_find(const ptr_hmap_t hmap, int32_t k) {	393,154✔
190	uint32_t mask, j;
191	ptr_hmap_pair_t *d;
192
193	assert(k >= 0);
194
195	mask = hmap->size - 1;	393,154✔
196	j = hash_key(k) & mask;	393,154✔
197	for (;;) {
198	d = hmap->data + j;	570,417✔
199	if (d->key == k) return d;	570,417✔
200	if (d->key == PHMAP_EMPTY_KEY) return NULL;	230,620✔
201	j ++;	177,263✔
202	j &= mask;	177,263✔
203	}
204	}
205
206
207	/*
208	* Add record with key k after hmap was extended:
209	* - initialize val to NULL
210	* - we know that no record with key k is present
211	*/
212	static ptr_hmap_pair_t ptr_hmap_get_clean(ptr_hmap_t hmap, int32_t k) {	3,037✔
213	uint32_t mask, j;
214	ptr_hmap_pair_t *d;
215
216	mask = hmap->size - 1;	3,037✔
217	j = hash_key(k) & mask;	3,037✔
218	for (;;) {
219	d = hmap->data + j;	4,361✔
220	if (d->key < 0) {	4,361✔
221	hmap->nelems ++;	3,037✔
222	d->key = k;	3,037✔
223	d->val = NULL;	3,037✔
224	return d;	3,037✔
225	}
226	j ++;	1,324✔
227	j &= mask;	1,324✔
228	}
229	}
230
231
232	/*
233	* Find or add record with key k
234	*/
235	ptr_hmap_pair_t ptr_hmap_get(ptr_hmap_t hmap, int32_t k) {	702,516✔
236	uint32_t mask, j;
237	ptr_hmap_pair_t d, aux;
238
239	assert(k >= 0);
240	assert(hmap->size > hmap->ndeleted + hmap->nelems);
241
242	mask = hmap->size - 1;	702,516✔
243	j = hash_key(k) & mask;	702,516✔
244
245	for (;;) {
246	d = hmap->data + j;	1,118,149✔
247	if (d->key == k) return d;	1,118,149✔
248	if (d->key < 0) break;	718,293✔
249	j ++;	415,633✔
250	j &= mask;	415,633✔
251	}
252
253	aux = d; // new record, if needed, will be aux	302,660✔
254	while (d->key != PHMAP_EMPTY_KEY) {	302,660✔
255	j ++;	×
256	j &= mask;	×
257	d = hmap->data + j;	×
258	if (d->key == k) return d;	×
259	}
260
261	if (aux->key == PHMAP_DEL_KEY) {	302,660✔
262	assert(hmap->ndeleted > 0);
263	hmap->ndeleted --;	×
264	}
265
266	if (hmap->nelems + hmap->ndeleted >= hmap->resize_threshold) {	302,660✔
267	ptr_hmap_extend(hmap);	3,037✔
268	aux = ptr_hmap_get_clean(hmap, k);	3,037✔
269	} else {
270	hmap->nelems ++;	299,623✔
271	aux->key = k;	299,623✔
272	aux->val = NULL;	299,623✔
273	}
274
275	return aux;	302,660✔
276	}
277
278
279	/*
280	* Erase record r
281	*/
282	void ptr_hmap_erase(ptr_hmap_t hmap, ptr_hmap_pair_t r) {	1,676✔
283	assert(ptr_hmap_find(hmap, r->key) == r);
284
285	r->key = PHMAP_DEL_KEY;	1,676✔
286	hmap->nelems --;	1,676✔
287	hmap->ndeleted ++;	1,676✔
288	if (hmap->ndeleted > hmap->cleanup_threshold) {	1,676✔
289	ptr_hmap_cleanup(hmap);	2✔
290	}
291	}	1,676✔
292
293
294	/*
295	* Empty the map
296	*/
297	void ptr_hmap_reset(ptr_hmap_t *hmap) {	13,818✔
298	uint32_t i, n;
299	ptr_hmap_pair_t *d;
300
301	n = hmap->size;	13,818✔
302	d = hmap->data;	13,818✔
303	for (i=0; i<n; i++) {	458,458✔
304	d->key = PHMAP_EMPTY_KEY;	444,640✔
305	d ++;	444,640✔
306	}
307
308	hmap->nelems = 0;	13,818✔
309	hmap->ndeleted = 0;	13,818✔
310	}	13,818✔
311
312
313	/*
314	* Remove all records that satisfy f
315	* - for every record r in the table, call f(aux, r)
316	* - if that returns true, then the record r is deleted
317	* - f must not have side effects
318	*/
319	void ptr_hmap_remove_records(ptr_hmap_t hmap, void aux, ptr_hmap_filter_t f) {	×
320	ptr_hmap_pair_t *d;
321	uint32_t i, n, k;
322
323	n = hmap->size;	×
324	d = hmap->data;	×
325	k = 0;	×
326	for (i=0; i<n; i++) {	×
327	if (d->key >= 0 && f(aux, d)) {	×
328	d->key = PHMAP_DEL_KEY;	×
329	k ++;	×
330	}
331	}
332
333	// k = number of deletions
334	assert(k <= hmap->nelems);
335	hmap->nelems -= k;	×
336	hmap->ndeleted += k;	×
337	if (hmap->ndeleted >= hmap->cleanup_threshold) {	×
338	ptr_hmap_cleanup(hmap);	×
339	}
340	}	×
341
342
343
344	/*
345	* First non-empty record in the table, starting from p
346	*/
347	static const ptr_hmap_pair_t ptr_hmap_get_next(const ptr_hmap_t hmap, const ptr_hmap_pair_t *p) {	358,903✔
348	ptr_hmap_pair_t *end;
349
350	end = hmap->data + hmap->size;	358,903✔
351	while (p < end) {	2,824,818✔
352	if (p->key >= 0) return p;	2,756,096✔
353	p ++;	2,465,915✔
354	}
355
356	return NULL;	68,722✔
357	}
358
359
360	/*
361	* Get the first non-empty record or NULL if the table is empty
362	*/
363	ptr_hmap_pair_t ptr_hmap_first_record(const ptr_hmap_t hmap) {	68,722✔
364	return (ptr_hmap_pair_t *) ptr_hmap_get_next(hmap, hmap->data);	68,722✔
365	}
366
367
368	/*
369	* Next record after p or NULL
370	*/
371	ptr_hmap_pair_t ptr_hmap_next_record(const ptr_hmap_t hmap, const ptr_hmap_pair_t *p) {	290,181✔
372	assert(p != NULL && p<hmap->data + hmap->size && p->key >= 0);
373	return (ptr_hmap_pair_t *) ptr_hmap_get_next(hmap, p+1);	290,181✔
374	}
375
376

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