22588689854

Committed 02 Mar 2026 05:54PM UTC coverage: 66.415% (+0.001%) from 66.414%

Build # 22588689854

Build Type

Pull #606

github

Committed by

disteph

Commit Message

tests: stabilize mcsat tuple regression across configs

Pull Request Pull Request #606: MCSAT: add tuple/function preprocessing + interpolant regression coverage

Run Details

218 of 549 new or added lines in 2 files covered. (39.71%)

33 existing lines in 4 files now uncovered.

83246 of 125343 relevant lines covered (66.41%)

1689418.64 hits per line

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

63.98

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

/*
 * MAPS TUPLES (ARRAYS) OF 32BIT INTEGERS TO 32BIT INTEGERS
 */

#include <assert.h>

#include "utils/hash_functions.h"
#include "utils/memalloc.h"
#include "utils/tuple_hash_map.h"


/*
 * RECORDS
 */

/*
 * Hash code for key[0 ... n-1]
 */
static inline uint32_t hash_tuple_key(uint32_t n, int32_t key[]) {
  return jenkins_hash_intarray(key, n);
}


/*
 * Check whether two keys of same size are equal.
 * - n = size of the two arrays
 */
static bool equal_tuples(uint32_t n, int32_t a[], int32_t b[]) {
  uint32_t i;

  for (i=0; i<n; i++) {
    if (a[i] != b[i]) {
      return false;
    }
  }

  return true;
}


/*
 * Create record for the given key and hash value
 * - key must be an array of n integers
 * - hash must be the hash code for key
 * - the value field is not initialized
 */
static tuple_hmap_rec_t *new_tuple_hmap_record(uint32_t hash, uint32_t n, int32_t key[]) {
  tuple_hmap_rec_t *tmp;
  uint32_t i;

  assert(n < TUPLE_HMAP_MAX_ARITY && hash == hash_tuple_key(n, key));

  tmp = (tuple_hmap_rec_t *) safe_malloc(sizeof(tuple_hmap_rec_t) + n * sizeof(int32_t));
  tmp->hash = hash;
  tmp->arity = n;
  for (i=0; i<n; i++) {
    tmp->key[i] = key[i];
  }

  return tmp;
}



/*
 * HASH TABLE
 */

/*
 * Allocate and initialize and array of n record pointers
 */
static tuple_hmap_rec_t **alloc_rec_array(uint32_t n) {
  tuple_hmap_rec_t **tmp;
  uint32_t i;

  tmp = (tuple_hmap_rec_t **) safe_malloc(n * sizeof(tuple_hmap_rec_t *));
  for (i=0; i<n; i++) {
    tmp[i] = NULL;
  }

  return tmp;
}




/*
 * 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 a power of 2)
 * - if n = 0, the default initial size is used
 */
void init_tuple_hmap(tuple_hmap_t *hmap, uint32_t n) {
  if (n == 0) {
    n = TUPLE_HMAP_DEF_SIZE;
  }

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

  assert(is_power_of_two(n));

  hmap->data = alloc_rec_array(n);
  hmap->size = n;
  hmap->nelems = 0;
  hmap->ndeleted = 0;
  hmap->resize_threshold = (uint32_t) (n * TUPLE_HMAP_RESIZE_RATIO);
  hmap->cleanup_threshold = (uint32_t) (n * TUPLE_HMAP_CLEANUP_RATIO);
}



/*
 * Check whether r is a valid record pointer
 */
static inline bool live_tuple_record(tuple_hmap_rec_t *r) {
  return (r != NULL) && (r != TUPLE_HMAP_DELETED);
}



/*
 * Free all memory used by hmap
 */
void delete_tuple_hmap(tuple_hmap_t *hmap) {
  tuple_hmap_rec_t **tmp;
  uint32_t i, n;

  tmp = hmap->data;
  n = hmap->size;
  for (i=0; i<n; i++) {
    if (live_tuple_record(tmp[i])) {
      safe_free(tmp[i]);
    }
  }

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


/*
 * Empty the hash table
 */
void reset_tuple_hmap(tuple_hmap_t *hmap) {
  tuple_hmap_rec_t **tmp;
  uint32_t i, n;

  tmp = hmap->data;
  n = hmap->size;
  for (i=0; i<n; i++) {
    if (live_tuple_record(tmp[i])) {
      safe_free(tmp[i]);
    }
    tmp[i] = NULL;
  }

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



/*
 * Add record r to array a
 * - a must be an array of size 2^k for k > 0
 * - mask must be equal to (2^k -1)
 * - there must be no deleted markers in a
 * - a must not be full.
 */
static void tuple_hmap_clean_copy(tuple_hmap_rec_t **a, tuple_hmap_rec_t *r, uint32_t mask) {
  uint32_t i;

  i = r->hash & mask;
  while (a[i] != NULL) {
    i ++;
    i &= mask;
  }
  a[i] = r;
}



/*
 * Remove the deletion marks
 */
static void tuple_hmap_cleanup(tuple_hmap_t *hmap) {
  tuple_hmap_rec_t **tmp;
  tuple_hmap_rec_t *r;
  uint32_t i, n, mask;

  n = hmap->size;
  tmp = alloc_rec_array(n);
  mask = n - 1;
  for (i=0; i<n; i++) {
    r = hmap->data[i];
    if (live_tuple_record(r)) {
      tuple_hmap_clean_copy(tmp, r, mask);
    }
  }

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


/*
 * Double the hash-table size and keep its content
 */
static void tuple_hmap_extend(tuple_hmap_t *hmap) {
  tuple_hmap_rec_t **tmp;
  tuple_hmap_rec_t *r;
  uint32_t i, n, n2, mask;

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

  assert(is_power_of_two(n2));

  tmp = alloc_rec_array(n2);
  mask = n2 - 1;
  for (i=0; i<n; i++) {
    r = hmap->data[i];
    if (live_tuple_record(r)) {
      tuple_hmap_clean_copy(tmp, r, mask);
    }
  }

  safe_free(hmap->data);
  hmap->data = tmp;
  hmap->size = n2;
  hmap->ndeleted = 0;
  hmap->resize_threshold = (uint32_t) (n2 * TUPLE_HMAP_RESIZE_RATIO);
  hmap->cleanup_threshold = (uint32_t) (n2 * TUPLE_HMAP_CLEANUP_RATIO);
}






/*
 * Find record that matches the given key
 * - key must be an array of n integers
 * - return NULL if there's no matching record
 */
tuple_hmap_rec_t *tuple_hmap_find(tuple_hmap_t *hmap, uint32_t n, int32_t key[]) {
  tuple_hmap_rec_t *r;
  uint32_t i, h, mask;

  assert(n <= TUPLE_HMAP_MAX_ARITY && hmap->nelems < hmap->size
         && is_power_of_two(hmap->size));

  h = hash_tuple_key(n, key);
  mask = hmap->size - 1;
  i = h & mask;

  for (;;) {
    r = hmap->data[i];
    if (r == NULL ||
        (r != TUPLE_HMAP_DELETED && r->hash == h && r->arity == n && equal_tuples(n, key, r->key))) {
      return r;
    }
    i ++;
    i &= mask;
  }
}



/*
 * Find or add a record with the given key
 * - key must be an array of n integers
 * - if there's a matching record in the table, it's returned and *new is set to false.
 * - otherwise, a new record is created and added to the table, *new is set to true,
 *   and the new record is returned.
 *   The value field of the new record is not initialized.
 */
tuple_hmap_rec_t *tuple_hmap_get(tuple_hmap_t *hmap, uint32_t n, int32_t key[], bool *new) {
  tuple_hmap_rec_t *r;
  uint32_t i, j, h, mask;

  assert(n <= TUPLE_HMAP_MAX_ARITY && hmap->nelems < hmap->size &&
         is_power_of_two(hmap->size));

  h = hash_tuple_key(n, key);
  mask = hmap->size - 1;
  i = h & mask;

  for (;;) {
    r = hmap->data[i];
    if (r == NULL) goto add;
    if (r == TUPLE_HMAP_DELETED) break;
    if (r->hash == h && r->arity == n && equal_tuples(n, key, r->key)) goto found;
    i ++;
    i &= mask;
  }

  // i = where the new record will be added if necessary
  j = i;
  for (;;) {
    j ++;
    j &= mask;
    r = hmap->data[j];
    if (r == NULL) {
      hmap->ndeleted --;
      goto add;
    }
    if (r != TUPLE_HMAP_DELETED && r->hash == h && r->arity == n && equal_tuples(n, key, r->key)) {
      goto found;
    }
  }

 add:
  assert(hmap->data[i] == NULL || hmap->data[i] == TUPLE_HMAP_DELETED);
  r = new_tuple_hmap_record(h, n, key);
  hmap->data[i] = r;
  hmap->nelems ++;
  if (hmap->nelems + hmap->ndeleted > hmap->resize_threshold) {
    tuple_hmap_extend(hmap);
  }
  *new = true;
  return r;

 found:
  *new = false;
  return r;
}



/*
 * Add the record (key, val) to the table
 * - key must be an array of n integers
 * - n must be no more than TUPLE_HMAP_MAX_ARITY
 * - there must not be a record with the same key in the table.
 */
void tuple_hmap_add(tuple_hmap_t *hmap, uint32_t n, int32_t key[], int32_t val) {
  tuple_hmap_rec_t *r;
  uint32_t i, h, mask;

  assert(tuple_hmap_find(hmap, n, key) == NULL);

  h = hash_tuple_key(n, key);
  r = new_tuple_hmap_record(h, n, key);
  r->value = val;

  mask = hmap->size - 1;
  i = h & mask;
  while (live_tuple_record(hmap->data[i])) {
    i ++;
    i &= mask;
  }

  assert(hmap->data[i] == NULL || hmap->data[i] == TUPLE_HMAP_DELETED);
  if (hmap->data[i] == TUPLE_HMAP_DELETED) {
    hmap->ndeleted --;
  }
  hmap->data[i] = r;
  hmap->nelems ++;
  if (hmap->nelems + hmap->ndeleted > hmap->resize_threshold) {
    tuple_hmap_extend(hmap);
  }
}


/*
 * Remove record r from the table
 */
void tuple_hmap_erase(tuple_hmap_t *hmap, tuple_hmap_rec_t *r) {
  uint32_t i, mask;

  assert(tuple_hmap_find(hmap, r->arity, r->key) == r);

  mask = hmap->size - 1;
  i = r->hash & mask;
  while (hmap->data[i] != r) {
    i ++;
    i &= mask;
  }

  safe_free(r);

  hmap->data[i] = TUPLE_HMAP_DELETED;
  hmap->nelems --;
  hmap->ndeleted ++;
  if (hmap->ndeleted > hmap->cleanup_threshold) {
    tuple_hmap_cleanup(hmap);
  }
}



/*
 * Remove record that matches the given key
 * - key must be an array of n integers
 * - n must be no more than TUPLE_HMAP_MAX_ARITY
 * - no change if there's no matching record in the table.
 */
void tuple_hmap_remove(tuple_hmap_t *hmap, uint32_t n, int32_t key[]) {
  tuple_hmap_rec_t *r;
  uint32_t i, h, mask;

  assert(n <= TUPLE_HMAP_MAX_ARITY && hmap->nelems < hmap->size &&
         is_power_of_two(hmap->size));

  h = hash_tuple_key(n, key);
  mask = hmap->size - 1;
  i = h & mask;

  for (;;) {
    r = hmap->data[i];
    if (r == NULL) return;
    if (r != TUPLE_HMAP_DELETED && r->hash == h &&
        r->arity == n && equal_tuples(n, key, r->key)) break;
    i ++;
    i &= mask;
  }

  safe_free(r);

  hmap->data[i] = TUPLE_HMAP_DELETED;
  hmap->nelems --;
  hmap->ndeleted ++;
  if (hmap->ndeleted > hmap->cleanup_threshold) {
    tuple_hmap_cleanup(hmap);
  }
}



/*
 * Garbage collection
 * - f is a function that indicates whether a record should be kept or not
 * - aux is an auxiliary pointer passed as argument to f
 * The function scans the hash table and calls f(aux, r) for every record r
 * in the table. If f returns false, r is deleted, otherwise, r is kept.
 */
void tuple_hmap_gc(tuple_hmap_t *hmap, void *aux, tuple_hmap_keep_fun_t f) {
  tuple_hmap_rec_t *r;
  uint32_t i, n;

  n = hmap->size;
  for (i=0; i< n; i++) {
    r = hmap->data[i];
    if (live_tuple_record(r) && !f(aux, r)) {
      // r must be deleted
      safe_free(r);
      hmap->data[i] = TUPLE_HMAP_DELETED;
      hmap->nelems --;
      hmap->ndeleted ++;
    }
  }

  if (hmap->ndeleted > hmap->cleanup_threshold) {
    tuple_hmap_cleanup(hmap);
  }
}


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 TUPLES (ARRAYS) OF 32BIT INTEGERS TO 32BIT INTEGERS
21	*/
22
23	#include <assert.h>
24
25	#include "utils/hash_functions.h"
26	#include "utils/memalloc.h"
27	#include "utils/tuple_hash_map.h"
28
29
30	/*
31	* RECORDS
32	*/
33
34	/*
35	* Hash code for key[0 ... n-1]
36	*/
37	static inline uint32_t hash_tuple_key(uint32_t n, int32_t key[]) {	14,002,144✔
38	return jenkins_hash_intarray(key, n);	14,002,144✔
39	}
40
41
42	/*
43	* Check whether two keys of same size are equal.
44	* - n = size of the two arrays
45	*/
46	static bool equal_tuples(uint32_t n, int32_t a[], int32_t b[]) {	8,307,132✔
47	uint32_t i;
48
49	for (i=0; i<n; i++) {	33,228,528✔
50	if (a[i] != b[i]) {	24,921,396✔
UNCOV 51	return false;	×
52	}
53	}
54
55	return true;	8,307,132✔
56	}
57
58
59	/*
60	* Create record for the given key and hash value
61	* - key must be an array of n integers
62	* - hash must be the hash code for key
63	* - the value field is not initialized
64	*/
65	static tuple_hmap_rec_t *new_tuple_hmap_record(uint32_t hash, uint32_t n, int32_t key[]) {	2,724,847✔
66	tuple_hmap_rec_t *tmp;
67	uint32_t i;
68
69	assert(n < TUPLE_HMAP_MAX_ARITY && hash == hash_tuple_key(n, key));
70
71	tmp = (tuple_hmap_rec_t ) safe_malloc(sizeof(tuple_hmap_rec_t) + n sizeof(int32_t));	2,724,847✔
72	tmp->hash = hash;	2,724,847✔
73	tmp->arity = n;	2,724,847✔
74	for (i=0; i<n; i++) {	10,899,387✔
75	tmp->key[i] = key[i];	8,174,540✔
76	}
77
78	return tmp;	2,724,847✔
79	}
80
81
82
83	/*
84	* HASH TABLE
85	*/
86
87	/*
88	* Allocate and initialize and array of n record pointers
89	*/
90	static tuple_hmap_rec_t **alloc_rec_array(uint32_t n) {	725✔
91	tuple_hmap_rec_t **tmp;
92	uint32_t i;
93
94	tmp = (tuple_hmap_rec_t *) safe_malloc(n sizeof(tuple_hmap_rec_t *));	725✔
95	for (i=0; i<n; i++) {	486,741✔
96	tmp[i] = NULL;	486,016✔
97	}
98
99	return tmp;	725✔
100	}
101
102
103
104
105	/*
106	* For debugging: check whether n is 0 or a power of 2
107	*/
108	#ifndef NDEBUG
109	static bool is_power_of_two(uint32_t n) {
110	return (n & (n-1)) == 0;
111	}
112	#endif
113
114
115	/*
116	* Initialization:
117	* - n = initial size (must be a power of 2)
118	* - if n = 0, the default initial size is used
119	*/
120	void init_tuple_hmap(tuple_hmap_t *hmap, uint32_t n) {	668✔
121	if (n == 0) {	668✔
122	n = TUPLE_HMAP_DEF_SIZE;	668✔
123	}
124
125	if (n >= TUPLE_HMAP_MAX_SIZE) {	668✔
126	out_of_memory();	×
127	}
128
129	assert(is_power_of_two(n));
130
131	hmap->data = alloc_rec_array(n);	668✔
132	hmap->size = n;	668✔
133	hmap->nelems = 0;	668✔
134	hmap->ndeleted = 0;	668✔
135	hmap->resize_threshold = (uint32_t) (n * TUPLE_HMAP_RESIZE_RATIO);	668✔
136	hmap->cleanup_threshold = (uint32_t) (n * TUPLE_HMAP_CLEANUP_RATIO);	668✔
137	}	668✔
138
139
140
141	/*
142	* Check whether r is a valid record pointer
143	*/
144	static inline bool live_tuple_record(tuple_hmap_rec_t *r) {	20,390,144✔
145	return (r != NULL) && (r != TUPLE_HMAP_DELETED);	20,390,144✔
146	}
147
148
149
150	/*
151	* Free all memory used by hmap
152	*/
153	void delete_tuple_hmap(tuple_hmap_t *hmap) {	668✔
154	tuple_hmap_rec_t **tmp;
155	uint32_t i, n;
156
157	tmp = hmap->data;	668✔
158	n = hmap->size;	668✔
159	for (i=0; i<n; i++) {	254,364✔
160	if (live_tuple_record(tmp[i])) {	253,696✔
161	safe_free(tmp[i]);	1✔
162	}
163	}
164
165	safe_free(tmp);	668✔
166	hmap->data = NULL;	668✔
167	}	668✔
168
169
170	/*
171	* Empty the hash table
172	*/
173	void reset_tuple_hmap(tuple_hmap_t *hmap) {	1,179✔
174	tuple_hmap_rec_t **tmp;
175	uint32_t i, n;
176
177	tmp = hmap->data;	1,179✔
178	n = hmap->size;	1,179✔
179	for (i=0; i<n; i++) {	16,210,779✔
180	if (live_tuple_record(tmp[i])) {	16,209,600✔
181	safe_free(tmp[i]);	2,724,846✔
182	}
183	tmp[i] = NULL;	16,209,600✔
184	}
185
186	hmap->nelems = 0;	1,179✔
187	hmap->ndeleted = 0;	1,179✔
188	}	1,179✔
189
190
191
192	/*
193	* Add record r to array a
194	* - a must be an array of size 2^k for k > 0
195	* - mask must be equal to (2^k -1)
196	* - there must be no deleted markers in a
197	* - a must not be full.
198	*/
199	static void tuple_hmap_clean_copy(tuple_hmap_rec_t *a, tuple_hmap_rec_t r, uint32_t mask) {	139,423✔
200	uint32_t i;
201
202	i = r->hash & mask;	139,423✔
203	while (a[i] != NULL) {	169,498✔
204	i ++;	30,075✔
205	i &= mask;	30,075✔
206	}
207	a[i] = r;	139,423✔
208	}	139,423✔
209
210
211
212	/*
213	* Remove the deletion marks
214	*/
215	static void tuple_hmap_cleanup(tuple_hmap_t *hmap) {	×
216	tuple_hmap_rec_t **tmp;
217	tuple_hmap_rec_t *r;
218	uint32_t i, n, mask;
219
220	n = hmap->size;	×
221	tmp = alloc_rec_array(n);	×
222	mask = n - 1;	×
223	for (i=0; i<n; i++) {	×
224	r = hmap->data[i];	×
225	if (live_tuple_record(r)) {	×
226	tuple_hmap_clean_copy(tmp, r, mask);	×
227	}
228	}
229
230	safe_free(hmap->data);	×
231	hmap->data = tmp;	×
232	hmap->ndeleted = 0;	×
233	}	×
234
235
236	/*
237	* Double the hash-table size and keep its content
238	*/
239	static void tuple_hmap_extend(tuple_hmap_t *hmap) {	57✔
240	tuple_hmap_rec_t **tmp;
241	tuple_hmap_rec_t *r;
242	uint32_t i, n, n2, mask;
243
244	n = hmap->size;	57✔
245	n2 = n << 1;	57✔
246	if (n2 >= TUPLE_HMAP_MAX_SIZE) {	57✔
247	out_of_memory();	×
248	}
249
250	assert(is_power_of_two(n2));
251
252	tmp = alloc_rec_array(n2);	57✔
253	mask = n2 - 1;	57✔
254	for (i=0; i<n; i++) {	232,377✔
255	r = hmap->data[i];	232,320✔
256	if (live_tuple_record(r)) {	232,320✔
257	tuple_hmap_clean_copy(tmp, r, mask);	139,423✔
258	}
259	}
260
261	safe_free(hmap->data);	57✔
262	hmap->data = tmp;	57✔
263	hmap->size = n2;	57✔
264	hmap->ndeleted = 0;	57✔
265	hmap->resize_threshold = (uint32_t) (n2 * TUPLE_HMAP_RESIZE_RATIO);	57✔
266	hmap->cleanup_threshold = (uint32_t) (n2 * TUPLE_HMAP_CLEANUP_RATIO);	57✔
267	}	57✔
268
269
270
271
272
273
274	/*
275	* Find record that matches the given key
276	* - key must be an array of n integers
277	* - return NULL if there's no matching record
278	*/
279	tuple_hmap_rec_t tuple_hmap_find(tuple_hmap_t hmap, uint32_t n, int32_t key[]) {	11,277,297✔
280	tuple_hmap_rec_t *r;
281	uint32_t i, h, mask;
282
283	assert(n <= TUPLE_HMAP_MAX_ARITY && hmap->nelems < hmap->size
284	&& is_power_of_two(hmap->size));
285
286	h = hash_tuple_key(n, key);	11,277,297✔
287	mask = hmap->size - 1;	11,277,297✔
288	i = h & mask;	11,277,297✔
289
290	for (;;) {
291	r = hmap->data[i];	15,308,983✔
292	if (r == NULL \|\|	15,308,983✔
293	(r != TUPLE_HMAP_DELETED && r->hash == h && r->arity == n && equal_tuples(n, key, r->key))) {	12,338,818✔
294	return r;	11,277,297✔
295	}
296	i ++;	4,031,686✔
297	i &= mask;	4,031,686✔
298	}
299	}
300
301
302
303	/*
304	* Find or add a record with the given key
305	* - key must be an array of n integers
306	* - if there's a matching record in the table, it's returned and *new is set to false.
307	* - otherwise, a new record is created and added to the table, *new is set to true,
308	* and the new record is returned.
309	* The value field of the new record is not initialized.
310	*/
311	tuple_hmap_rec_t tuple_hmap_get(tuple_hmap_t hmap, uint32_t n, int32_t key[], bool *new) {	1✔
312	tuple_hmap_rec_t *r;
313	uint32_t i, j, h, mask;
314
315	assert(n <= TUPLE_HMAP_MAX_ARITY && hmap->nelems < hmap->size &&
316	is_power_of_two(hmap->size));
317
318	h = hash_tuple_key(n, key);	1✔
319	mask = hmap->size - 1;	1✔
320	i = h & mask;	1✔
321
322	for (;;) {
323	r = hmap->data[i];	1✔
324	if (r == NULL) goto add;	1✔
325	if (r == TUPLE_HMAP_DELETED) break;	×
326	if (r->hash == h && r->arity == n && equal_tuples(n, key, r->key)) goto found;	×
327	i ++;	×
328	i &= mask;	×
329	}
330
331	// i = where the new record will be added if necessary
332	j = i;	×
333	for (;;) {
334	j ++;	×
335	j &= mask;	×
336	r = hmap->data[j];	×
337	if (r == NULL) {	×
338	hmap->ndeleted --;	×
339	goto add;	×
340	}
341	if (r != TUPLE_HMAP_DELETED && r->hash == h && r->arity == n && equal_tuples(n, key, r->key)) {	×
342	goto found;	×
343	}
344	}
345
346	add:	1✔
347	assert(hmap->data[i] == NULL \|\| hmap->data[i] == TUPLE_HMAP_DELETED);
348	r = new_tuple_hmap_record(h, n, key);	1✔
349	hmap->data[i] = r;	1✔
350	hmap->nelems ++;	1✔
351	if (hmap->nelems + hmap->ndeleted > hmap->resize_threshold) {	1✔
352	tuple_hmap_extend(hmap);	×
353	}
354	*new = true;	1✔
355	return r;	1✔
356
357	found:	×
358	*new = false;	×
359	return r;	×
360	}
361
362
363
364	/*
365	* Add the record (key, val) to the table
366	* - key must be an array of n integers
367	* - n must be no more than TUPLE_HMAP_MAX_ARITY
368	* - there must not be a record with the same key in the table.
369	*/
370	void tuple_hmap_add(tuple_hmap_t *hmap, uint32_t n, int32_t key[], int32_t val) {	2,724,846✔
371	tuple_hmap_rec_t *r;
372	uint32_t i, h, mask;
373
374	assert(tuple_hmap_find(hmap, n, key) == NULL);
375
376	h = hash_tuple_key(n, key);	2,724,846✔
377	r = new_tuple_hmap_record(h, n, key);	2,724,846✔
378	r->value = val;	2,724,846✔
379
380	mask = hmap->size - 1;	2,724,846✔
381	i = h & mask;	2,724,846✔
382	while (live_tuple_record(hmap->data[i])) {	3,694,464✔
383	i ++;	969,618✔
384	i &= mask;	969,618✔
385	}
386
387	assert(hmap->data[i] == NULL \|\| hmap->data[i] == TUPLE_HMAP_DELETED);
388	if (hmap->data[i] == TUPLE_HMAP_DELETED) {	2,724,846✔
389	hmap->ndeleted --;	×
390	}
391	hmap->data[i] = r;	2,724,846✔
392	hmap->nelems ++;	2,724,846✔
393	if (hmap->nelems + hmap->ndeleted > hmap->resize_threshold) {	2,724,846✔
394	tuple_hmap_extend(hmap);	57✔
395	}
396	}	2,724,846✔
397
398
399	/*
400	* Remove record r from the table
401	*/
402	void tuple_hmap_erase(tuple_hmap_t hmap, tuple_hmap_rec_t r) {	×
403	uint32_t i, mask;
404
405	assert(tuple_hmap_find(hmap, r->arity, r->key) == r);
406
407	mask = hmap->size - 1;	×
408	i = r->hash & mask;	×
409	while (hmap->data[i] != r) {	×
410	i ++;	×
411	i &= mask;	×
412	}
413
414	safe_free(r);	×
415
416	hmap->data[i] = TUPLE_HMAP_DELETED;	×
417	hmap->nelems --;	×
418	hmap->ndeleted ++;	×
419	if (hmap->ndeleted > hmap->cleanup_threshold) {	×
420	tuple_hmap_cleanup(hmap);	×
421	}
422	}	×
423
424
425
426	/*
427	* Remove record that matches the given key
428	* - key must be an array of n integers
429	* - n must be no more than TUPLE_HMAP_MAX_ARITY
430	* - no change if there's no matching record in the table.
431	*/
432	void tuple_hmap_remove(tuple_hmap_t *hmap, uint32_t n, int32_t key[]) {	×
433	tuple_hmap_rec_t *r;
434	uint32_t i, h, mask;
435
436	assert(n <= TUPLE_HMAP_MAX_ARITY && hmap->nelems < hmap->size &&
437	is_power_of_two(hmap->size));
438
439	h = hash_tuple_key(n, key);	×
440	mask = hmap->size - 1;	×
441	i = h & mask;	×
442
443	for (;;) {
444	r = hmap->data[i];	×
445	if (r == NULL) return;	×
446	if (r != TUPLE_HMAP_DELETED && r->hash == h &&	×
447	r->arity == n && equal_tuples(n, key, r->key)) break;	×
448	i ++;	×
449	i &= mask;	×
450	}
451
452	safe_free(r);	×
453
454	hmap->data[i] = TUPLE_HMAP_DELETED;	×
455	hmap->nelems --;	×
456	hmap->ndeleted ++;	×
457	if (hmap->ndeleted > hmap->cleanup_threshold) {	×
458	tuple_hmap_cleanup(hmap);	×
459	}
460	}
461
462
463
464	/*
465	* Garbage collection
466	* - f is a function that indicates whether a record should be kept or not
467	* - aux is an auxiliary pointer passed as argument to f
468	* The function scans the hash table and calls f(aux, r) for every record r
469	* in the table. If f returns false, r is deleted, otherwise, r is kept.
470	*/
471	void tuple_hmap_gc(tuple_hmap_t hmap, void aux, tuple_hmap_keep_fun_t f) {	2✔
472	tuple_hmap_rec_t *r;
473	uint32_t i, n;
474
475	n = hmap->size;	2✔
476	for (i=0; i< n; i++) {	66✔
477	r = hmap->data[i];	64✔
478	if (live_tuple_record(r) && !f(aux, r)) {	64✔
479	// r must be deleted
480	safe_free(r);	×
481	hmap->data[i] = TUPLE_HMAP_DELETED;	×
482	hmap->nelems --;	×
483	hmap->ndeleted ++;	×
484	}
485	}
486
487	if (hmap->ndeleted > hmap->cleanup_threshold) {	2✔
488	tuple_hmap_cleanup(hmap);	×
489	}
490	}	2✔
491

SRI-CSL / yices2 / 22588689854

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