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

85.07

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

/*
 * HASH MAP2
 *
 * - map pairs of 32bit integers to 32bit integers
 * - supports push and pop.
 */

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

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



/*********************
 *  BANK OF TRIPLES  *
 ********************/

/*
 * Initialize bank: nothing allocated yet
 */
static void init_pmap2_bank(pmap2_bank_t *bank) {
  bank->capacity = 0;
  bank->nblocks = 0;
  bank->free_block = 0;
  bank->alloc_ptr = PMAP2_BLOCK_SIZE;
  bank->block = NULL;
}


/*
 * Free memory
 */
static void delete_pmap2_bank(pmap2_bank_t *bank) {
  uint32_t i;

  for (i=0; i<bank->nblocks; i++) {
    safe_free(bank->block[i]);
  }
  safe_free(bank->block);
  bank->block = NULL;
}


/*
 * Empty the bank
 */
static inline void reset_pmap2_bank(pmap2_bank_t *bank) {
  bank->free_block = 0;
  bank->alloc_ptr = PMAP2_BLOCK_SIZE;
}


/*
 * Allocate the initial block array or increase it by 50%
 */
static void extend_pmap2_bank(pmap2_bank_t *bank) {
  uint32_t n;

  n = bank->capacity;
  n += n>>1;
  if (n < PMAP2_DEF_BANK_SIZE) {
    n = PMAP2_DEF_BANK_SIZE;
  }
  if (n >= PMAP2_MAX_BANK_SIZE) {
    out_of_memory();
  }

  bank->block = (pmap2_rec_t **) safe_realloc(bank->block, n * sizeof(pmap2_rec_t *));
  bank->capacity = n;
}


/*
 * Allocate a new block and store it in the block array
 */
static void allocate_pmap2_block(pmap2_bank_t *bank) {
  uint32_t i;

  i = bank->nblocks;
  if (i == bank->capacity) {
    extend_pmap2_bank(bank);
  }
  assert(i < bank->capacity);
  bank->block[i] = (pmap2_rec_t *) safe_malloc(PMAP2_BLOCK_SIZE * sizeof(pmap2_rec_t));
  bank->nblocks = i+1;
}


/*
 * Allocate a new triple
 */
static pmap2_rec_t *alloc_pmap2_record(pmap2_bank_t *bank) {
  uint32_t i, p;
  pmap2_rec_t *tmp;

  i = bank->free_block;
  p = bank->alloc_ptr;
  if (p == PMAP2_BLOCK_SIZE) {
    // free_block is full or the bank is empty:
    // get a new block
    if (i == bank->nblocks) {
      allocate_pmap2_block(bank);
    }
    assert(i < bank->nblocks);
    i ++;
    bank->free_block = i;
    p = 0;
  }

  // allocate element p in block i-1
  assert(0 < i && bank->block[i-1] != NULL);
  tmp = bank->block[i-1] + p;
  bank->alloc_ptr = p+1;

  return tmp;
}


/********************
 *  PUSH/POP STACK  *
 *******************/

/*
 * Initialize: no memory allocated yet
 */
static void init_pmap2_stack(pmap2_stack_t *stack) {
  stack->current_level = 0;
  stack->top_level = 0;
  stack->nmarks = 0;
  stack->size = 0;
  stack->data = NULL;
}

static void delete_pmap2_stack(pmap2_stack_t *stack) {
  safe_free(stack->data);
  stack->data = NULL;
}


/*
 * Empty the stack
 */
static void reset_pmap2_stack(pmap2_stack_t *stack) {
  stack->current_level = 0;
  stack->top_level = 0;
  stack->nmarks = 0;
}


/*
 * Push mark <b, p> on top of the stack
 * - b = block index
 * - p = allocation index in block b
 * - current_level must be larger than top_level
 */
static void push_alloc_mark(pmap2_stack_t *stack, uint32_t b, uint32_t p) {
  uint32_t i, k, n;

  assert(stack->current_level > stack->top_level);

  k = stack->current_level;
  i = stack->nmarks;
  n = stack->size;

  if (i == n) {
    // allocate data array or make it larger by 50%
    if (n < PMAP2_DEF_STACK_SIZE) {
      n = PMAP2_DEF_STACK_SIZE;
      assert(n < PMAP2_MAX_STACK_SIZE);
    } else {
      n += n>>1;
      if (n >= PMAP2_MAX_STACK_SIZE) {
        out_of_memory();
      }
    }
    stack->data = (pmap2_mark_t *) safe_realloc(stack->data, n * sizeof(pmap2_mark_t));
    stack->size = n;
  }

  assert(i < n);
  stack->data[i].level = k;
  stack->data[i].block_id = b;
  stack->data[i].alloc_idx = p;

  stack->nmarks = i+1;
  stack->top_level = k;
}


/*
 * Remove the top mark
 */
static void pop_alloc_mark(pmap2_stack_t *stack) {
  uint32_t i;

  assert(stack->nmarks > 0);

  i = stack->nmarks - 1;
  stack->nmarks = i;
  if (i == 0) {
    stack->top_level = 0;
  } else {
    stack->top_level = stack->data[i-1].level;
  }
}



/****************
 *  HASH TABLE  *
 ***************/

/*
 * 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


/*
 * Initialize: use the default size
 */
static void init_pmap2_htbl(pmap2_htbl_t *table) {
  pmap2_rec_t **tmp;
  uint32_t i, n;

  n = PMAP2_DEF_HTBL_SIZE;
  assert(is_power_of_two(n) && n < PMAP2_MAX_HTBL_SIZE);

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

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

  table->resize_threshold = (uint32_t) (n * PMAP2_HTBL_RESIZE_RATIO);
  table->cleanup_threshold = (uint32_t) (n * PMAP2_HTBL_CLEANUP_RATIO);
}


static void delete_pmap2_htbl(pmap2_htbl_t *table) {
  safe_free(table->data);
  table->data = NULL;
}


/*
 * Empty the table: don't resize
 */
static void reset_pmap2_htbl(pmap2_htbl_t *table) {
  uint32_t i, n;

  n = table->size;
  for (i=0; i<n; i++) {
    table->data[i] = NULL;
  }
  table->nelems = 0;
  table->ndeleted = 0;
}


/*
 * Hash code for key (k0, k1) (based on Jenkin'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 pmap2_hash(int32_t k0, int32_t k1) {
  uint32_t a, b, c;

  a = (uint32_t) k0;
  b = (uint32_t) k1;
  c = 0x9341ad2a;
  final(a, b, c);

  return c;
}



/*
 * Store pointer e into clean array a:
 * - mask = size of a - 1 (the size of a must be a power of 2)
 * - a must not be full and must not contain deletion marks
 */
static void pmap2_htbl_clean_copy(pmap2_rec_t **a, pmap2_rec_t *e, uint32_t mask) {
  uint32_t j;

  j = pmap2_hash(e->k0, e->k1) & mask;
  while (a[j] != NULL) {
    j ++;
    j &= mask;
  }

  a[j] = e;
}


/*
 * Check whether pointer e is non NULL and different from
 * PMAP2_DELETED. (We use the fact that NULL = 0 and PMAP2_DELETED = 1.
 */
static inline bool live_record(const pmap2_rec_t *e) {
  return (((uintptr_t) e) >> 1) != 0;
}


/*
 * Cleanup: remove all the deletion marks
 */
static void pmap2_htbl_cleanup(pmap2_htbl_t *table) {
  pmap2_rec_t **tmp;
  pmap2_rec_t *e;
  uint32_t i, n, mask;

  n = table->size;
  assert(is_power_of_two(n));

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

  mask = n - 1;
  for (i=0; i<n; i++) {
    e = table->data[i];
    if (live_record(e)) {
      pmap2_htbl_clean_copy(tmp, e, mask);
    }
  }

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



/*
 * Cleanup if the cleanup threshold is reached.
 * Do nothing otherwise.
 */
static inline void pmap2_htbl_cleanup_if_needed(pmap2_htbl_t *table) {
  if (table->ndeleted > table->cleanup_threshold) {
    pmap2_htbl_cleanup(table);
  }
}


/*
 * Double the size and remove the deletion marks
 */
static void pmap2_htbl_extend(pmap2_htbl_t *table) {
  pmap2_rec_t **tmp;
  pmap2_rec_t *e;
  uint32_t i, n, new_size, mask;

  n = table->size;
  new_size = 2 * n;
  if (new_size >= PMAP2_MAX_HTBL_SIZE) {
    out_of_memory();
  }

  assert(is_power_of_two(new_size));

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

  mask = new_size - 1;
  for (i=0; i<n; i++) {
    e = table->data[i];
    if (live_record(e)) {
      pmap2_htbl_clean_copy(tmp, e, mask);
    }
  }

  safe_free(table->data);
  table->data = tmp;
  table->ndeleted = 0;
  table->size = new_size;
  table->resize_threshold = (uint32_t) (new_size * PMAP2_HTBL_RESIZE_RATIO);
  table->cleanup_threshold = (uint32_t) (new_size * PMAP2_HTBL_CLEANUP_RATIO);
}


/*
 * Remove e from the table.
 * - e must be present
 */
static void pmap2_htbl_remove(pmap2_htbl_t *table, pmap2_rec_t *e) {
  uint32_t mask, j;

  assert(is_power_of_two(table->size));

  mask = table->size - 1;
  j = pmap2_hash(e->k0, e->k1) & mask;
  while (table->data[j] != e) {
    j ++;
    j &= mask;
  }

  table->data[j] = PMAP2_DELETED;
  table->nelems --;
  table->ndeleted ++;
}




/**************
 *  FULL MAP  *
 *************/

/*
 * Initialize everything
 */
void init_pmap2(pmap2_t *pmap) {
  init_pmap2_htbl(&pmap->htbl);
  init_pmap2_stack(&pmap->stack);
  init_pmap2_bank(&pmap->bank);
}


/*
 * Delete everything
 */
void delete_pmap2(pmap2_t *pmap) {
  delete_pmap2_htbl(&pmap->htbl);
  delete_pmap2_stack(&pmap->stack);
  delete_pmap2_bank(&pmap->bank);
}


/*
 * Empty the table and set current level to 0
 */
void reset_pmap2(pmap2_t *pmap) {
  reset_pmap2_htbl(&pmap->htbl);
  reset_pmap2_stack(&pmap->stack);
  reset_pmap2_bank(&pmap->bank);
}



/*
 * Remove from htbl all the records allocated after the mark b, i
 * - b = block index = free_block at the time push was called
 * - i = index in block = alloc_ptr at the time push was called
 */
static void remove_level(pmap2_bank_t *bank, pmap2_htbl_t *htbl, uint32_t b, uint32_t i) {
  uint32_t n, p;
  pmap2_rec_t *blk;

  /*
   * n = current free_block
   * p = current alloc_ptr
   */
  n = bank->free_block;
  p = bank->alloc_ptr;

  /*
   * Restore free_block and alloc_ptr
   */
  bank->free_block = b;
  bank->alloc_ptr = i;


  /*
   * Records to remove:
   * - in block b-1: all records from i to BLOCK_SIZE -1
   * - in blocks b to n-2: all records (from 0 to BLOCK_SIZE - 1)
   * - in block n-1: all records from 0 to p-1
   */
  if (i == PMAP2_BLOCK_SIZE) {
    // either b = 0 or nothing to delete in block b-1
    i = 0;
    b ++;
  }

  assert(b > 0);

  while (b < n) {
    blk = bank->block[b - 1];
    while (i < PMAP2_BLOCK_SIZE) {
      pmap2_htbl_remove(htbl, blk + i);
      i ++;
    }
    i = 0;
    b ++;
  }

  // last block:
  assert(b == n && b > 0);
  blk = bank->block[b - 1];
  while (i < p) {
    pmap2_htbl_remove(htbl, blk + i);
    i ++;
  }
}


/*
 * Pop: remove all records allocated at the current level
 * - current level must be positive
 */
void pmap2_pop(pmap2_t *pmap) {
  pmap2_stack_t *stack;
  uint32_t i;

  stack = &pmap->stack;
  assert(stack->current_level > 0 && stack->current_level >= stack->top_level);

  if (stack->current_level == stack->top_level) {
    assert(stack->nmarks > 0);
    i = stack->nmarks - 1;
    assert(stack->data[i].level == stack->current_level);
    remove_level(&pmap->bank, &pmap->htbl, stack->data[i].block_id, stack->data[i].alloc_idx);
    pmap2_htbl_cleanup_if_needed(&pmap->htbl);
    pop_alloc_mark(stack);
  }

  stack->current_level --;

  assert(stack->current_level >= stack->top_level);
}



/*
 * Search for record of key <k0, k1>
 * - return NULL if there's no matching record
 */
pmap2_rec_t *pmap2_find(const pmap2_t *pmap, int32_t k0, int32_t k1) {
  const pmap2_htbl_t *htbl;
  pmap2_rec_t *e;
  uint32_t i, mask;

  htbl = &pmap->htbl;
  assert(htbl->nelems + htbl->ndeleted < htbl->size); // otherwise the function loops

  assert(is_power_of_two(htbl->size));
  mask = htbl->size -1;

  i = pmap2_hash(k0, k1) & mask;
  for (;;) {
    e = htbl->data[i];
    if (e == NULL || (e != PMAP2_DELETED && e->k0 == k0 && e->k1 == k1)) {
      return e;
    }
    i ++;
    i &= mask;
  }
}



/*
 * Push the current (free_block + alloc_ptr) onto the stack if current_level > top_level
 */
static inline void push_alloc_mark_if_needed(pmap2_stack_t *stack, pmap2_bank_t *bank) {
  if (stack->current_level > stack->top_level) {
    push_alloc_mark(stack, bank->free_block, bank->alloc_ptr);
  }
}


/*
 * Find or add a record with key <k0, k1>
 * - if a new record is created, set its value to -1
 */
pmap2_rec_t *pmap2_get(pmap2_t *pmap, int32_t k0, int32_t k1) {
  pmap2_htbl_t *htbl;
  pmap2_rec_t *e;
  uint32_t i, j, mask;

  htbl = &pmap->htbl;
  assert(htbl->nelems + htbl->ndeleted < htbl->size);

  assert(is_power_of_two(htbl->size));
  mask = htbl->size - 1;

  i = pmap2_hash(k0, k1) & mask;
  for (;;) {
    e = htbl->data[i];
    if (e == NULL) goto add;
    if (e == PMAP2_DELETED) break;
    if (e->k0 == k0 && e->k1 == k1) goto found;
    i ++;
    i &= mask;
  }

  // i = index where new record can be added
  assert(htbl->data[i] == PMAP2_DELETED);

  j = i;
  for (;;) {
    j ++;
    j &= mask;
    e = htbl->data[j];
    if (e == NULL) {
      htbl->ndeleted --;
      goto add;
    }
    if (e != PMAP2_DELETED && e->k0 == k0 && e->k1 == k1) goto found;
  }

 add:
  /*
   * Create a new record and store it in htbl->data[i].
   */
  push_alloc_mark_if_needed(&pmap->stack, &pmap->bank);

  e = alloc_pmap2_record(&pmap->bank);
  e->k0 = k0;
  e->k1 = k1;
  e->val = -1;
  htbl->data[i] = e;

  htbl->nelems ++;
  if (htbl->nelems + htbl->ndeleted > htbl->resize_threshold) {
    pmap2_htbl_extend(htbl);
  }

 found:
  assert(e->k0 == k0 && e->k1 == k1);
  return e;
}




/*
 * ITERATOR
 * - call f(aux, p) for every p in the table
 */
void pmap2_iterate(pmap2_t *pmap, void *aux, pmap2_iterator_t f) {
  pmap2_htbl_t *htbl;
  pmap2_rec_t *p;
  uint32_t i, n;

  htbl = &pmap->htbl;
  n = htbl->size;
  for (i=0; i<n; i++) {
    p = htbl->data[i];
    if (live_record(p)) {
      f(aux, p);
    }
  }
}

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 MAP2
21	*
22	* - map pairs of 32bit integers to 32bit integers
23	* - supports push and pop.
24	*/
25
26	#include <stdbool.h>
27	#include <stddef.h>
28	#include <assert.h>
29
30	#include "utils/memalloc.h"
31	#include "utils/pair_hash_map2.h"
32
33
34
35	/*********************
36	* BANK OF TRIPLES *
37	********************/
38
39	/*
40	* Initialize bank: nothing allocated yet
41	*/
42	static void init_pmap2_bank(pmap2_bank_t *bank) {	147✔
43	bank->capacity = 0;	147✔
44	bank->nblocks = 0;	147✔
45	bank->free_block = 0;	147✔
46	bank->alloc_ptr = PMAP2_BLOCK_SIZE;	147✔
47	bank->block = NULL;	147✔
48	}	147✔
49
50
51	/*
52	* Free memory
53	*/
54	static void delete_pmap2_bank(pmap2_bank_t *bank) {	147✔
55	uint32_t i;
56
57	for (i=0; i<bank->nblocks; i++) {	383✔
58	safe_free(bank->block[i]);	236✔
59	}
60	safe_free(bank->block);	147✔
61	bank->block = NULL;	147✔
62	}	147✔
63
64
65	/*
66	* Empty the bank
67	*/
68	static inline void reset_pmap2_bank(pmap2_bank_t *bank) {	×
69	bank->free_block = 0;	×
70	bank->alloc_ptr = PMAP2_BLOCK_SIZE;	×
71	}	×
72
73
74	/*
75	* Allocate the initial block array or increase it by 50%
76	*/
77	static void extend_pmap2_bank(pmap2_bank_t *bank) {	155✔
78	uint32_t n;
79
80	n = bank->capacity;	155✔
81	n += n>>1;	155✔
82	if (n < PMAP2_DEF_BANK_SIZE) {	155✔
83	n = PMAP2_DEF_BANK_SIZE;	147✔
84	}
85	if (n >= PMAP2_MAX_BANK_SIZE) {	155✔
86	out_of_memory();	×
87	}
88
89	bank->block = (pmap2_rec_t *) safe_realloc(bank->block, n sizeof(pmap2_rec_t *));	155✔
90	bank->capacity = n;	155✔
91	}	155✔
92
93
94	/*
95	* Allocate a new block and store it in the block array
96	*/
97	static void allocate_pmap2_block(pmap2_bank_t *bank) {	236✔
98	uint32_t i;
99
100	i = bank->nblocks;	236✔
101	if (i == bank->capacity) {	236✔
102	extend_pmap2_bank(bank);	155✔
103	}
104	assert(i < bank->capacity);
105	bank->block[i] = (pmap2_rec_t ) safe_malloc(PMAP2_BLOCK_SIZE sizeof(pmap2_rec_t));	236✔
106	bank->nblocks = i+1;	236✔
107	}	236✔
108
109
110	/*
111	* Allocate a new triple
112	*/
113	static pmap2_rec_t alloc_pmap2_record(pmap2_bank_t bank) {	53,411✔
114	uint32_t i, p;
115	pmap2_rec_t *tmp;
116
117	i = bank->free_block;	53,411✔
118	p = bank->alloc_ptr;	53,411✔
119	if (p == PMAP2_BLOCK_SIZE) {	53,411✔
120	// free_block is full or the bank is empty:
121	// get a new block
122	if (i == bank->nblocks) {	246✔
123	allocate_pmap2_block(bank);	236✔
124	}
125	assert(i < bank->nblocks);
126	i ++;	246✔
127	bank->free_block = i;	246✔
128	p = 0;	246✔
129	}
130
131	// allocate element p in block i-1
132	assert(0 < i && bank->block[i-1] != NULL);
133	tmp = bank->block[i-1] + p;	53,411✔
134	bank->alloc_ptr = p+1;	53,411✔
135
136	return tmp;	53,411✔
137	}
138
139
140	/********************
141	* PUSH/POP STACK *
142	*******************/
143
144	/*
145	* Initialize: no memory allocated yet
146	*/
147	static void init_pmap2_stack(pmap2_stack_t *stack) {	147✔
148	stack->current_level = 0;	147✔
149	stack->top_level = 0;	147✔
150	stack->nmarks = 0;	147✔
151	stack->size = 0;	147✔
152	stack->data = NULL;	147✔
153	}	147✔
154
155	static void delete_pmap2_stack(pmap2_stack_t *stack) {	147✔
156	safe_free(stack->data);	147✔
157	stack->data = NULL;	147✔
158	}	147✔
159
160
161	/*
162	* Empty the stack
163	*/
164	static void reset_pmap2_stack(pmap2_stack_t *stack) {	×
165	stack->current_level = 0;	×
166	stack->top_level = 0;	×
167	stack->nmarks = 0;	×
168	}	×
169
170
171	/*
172	* Push mark <b, p> on top of the stack
173	* - b = block index
174	* - p = allocation index in block b
175	* - current_level must be larger than top_level
176	*/
177	static void push_alloc_mark(pmap2_stack_t *stack, uint32_t b, uint32_t p) {	46✔
178	uint32_t i, k, n;
179
180	assert(stack->current_level > stack->top_level);
181
182	k = stack->current_level;	46✔
183	i = stack->nmarks;	46✔
184	n = stack->size;	46✔
185
186	if (i == n) {	46✔
187	// allocate data array or make it larger by 50%
188	if (n < PMAP2_DEF_STACK_SIZE) {	18✔
189	n = PMAP2_DEF_STACK_SIZE;	18✔
190	assert(n < PMAP2_MAX_STACK_SIZE);
191	} else {
192	n += n>>1;	×
193	if (n >= PMAP2_MAX_STACK_SIZE) {	×
194	out_of_memory();	×
195	}
196	}
197	stack->data = (pmap2_mark_t ) safe_realloc(stack->data, n sizeof(pmap2_mark_t));	18✔
198	stack->size = n;	18✔
199	}
200
201	assert(i < n);
202	stack->data[i].level = k;	46✔
203	stack->data[i].block_id = b;	46✔
204	stack->data[i].alloc_idx = p;	46✔
205
206	stack->nmarks = i+1;	46✔
207	stack->top_level = k;	46✔
208	}	46✔
209
210
211	/*
212	* Remove the top mark
213	*/
214	static void pop_alloc_mark(pmap2_stack_t *stack) {	36✔
215	uint32_t i;
216
217	assert(stack->nmarks > 0);
218
219	i = stack->nmarks - 1;	36✔
220	stack->nmarks = i;	36✔
221	if (i == 0) {	36✔
222	stack->top_level = 0;	24✔
223	} else {
224	stack->top_level = stack->data[i-1].level;	12✔
225	}
226	}	36✔
227
228
229
230	/****************
231	* HASH TABLE *
232	***************/
233
234	/*
235	* For debugging: check whether n is a power of two
236	*/
237	#ifndef NDEBUG
238	static bool is_power_of_two(uint32_t n) {
239	return (n & (n - 1)) == 0;
240	}
241	#endif
242
243
244	/*
245	* Initialize: use the default size
246	*/
247	static void init_pmap2_htbl(pmap2_htbl_t *table) {	147✔
248	pmap2_rec_t **tmp;
249	uint32_t i, n;
250
251	n = PMAP2_DEF_HTBL_SIZE;	147✔
252	assert(is_power_of_two(n) && n < PMAP2_MAX_HTBL_SIZE);
253
254	tmp = (pmap2_rec_t *) safe_malloc(n sizeof(pmap2_rec_t *));	147✔
255	for (i=0; i<n; i++) {	18,963✔
256	tmp[i] = NULL;	18,816✔
257	}
258
259	table->data = tmp;	147✔
260	table->size = n;	147✔
261	table->nelems = 0;	147✔
262	table->ndeleted = 0;	147✔
263
264	table->resize_threshold = (uint32_t) (n * PMAP2_HTBL_RESIZE_RATIO);	147✔
265	table->cleanup_threshold = (uint32_t) (n * PMAP2_HTBL_CLEANUP_RATIO);	147✔
266	}	147✔
267
268
269	static void delete_pmap2_htbl(pmap2_htbl_t *table) {	147✔
270	safe_free(table->data);	147✔
271	table->data = NULL;	147✔
272	}	147✔
273
274
275	/*
276	* Empty the table: don't resize
277	*/
278	static void reset_pmap2_htbl(pmap2_htbl_t *table) {	×
279	uint32_t i, n;
280
281	n = table->size;	×
282	for (i=0; i<n; i++) {	×
283	table->data[i] = NULL;	×
284	}
285	table->nelems = 0;	×
286	table->ndeleted = 0;	×
287	}	×
288
289
290	/*
291	* Hash code for key (k0, k1) (based on Jenkin's lookup3 code)
292	*/
293	#define rot(x,k) (((x)<<(k)) \| ((x)>>(32-(k))))
294
295	#define final(a,b,c) \
296	{ \
297	c ^= b; c -= rot(b,14); \
298	a ^= c; a -= rot(c,11); \
299	b ^= a; b -= rot(a,25); \
300	c ^= b; c -= rot(b,16); \
301	a ^= c; a -= rot(c,4); \
302	b ^= a; b -= rot(a,14); \
303	c ^= b; c -= rot(b,24); \
304	}
305
306
307	static uint32_t pmap2_hash(int32_t k0, int32_t k1) {	214,913✔
308	uint32_t a, b, c;
309
310	a = (uint32_t) k0;	214,913✔
311	b = (uint32_t) k1;	214,913✔
312	c = 0x9341ad2a;	214,913✔
313	final(a, b, c);	214,913✔
314
315	return c;	214,913✔
316	}
317
318
319
320	/*
321	* Store pointer e into clean array a:
322	* - mask = size of a - 1 (the size of a must be a power of 2)
323	* - a must not be full and must not contain deletion marks
324	*/
325	static void pmap2_htbl_clean_copy(pmap2_rec_t *a, pmap2_rec_t e, uint32_t mask) {	68,957✔
326	uint32_t j;
327
328	j = pmap2_hash(e->k0, e->k1) & mask;	68,957✔
329	while (a[j] != NULL) {	83,722✔
330	j ++;	14,765✔
331	j &= mask;	14,765✔
332	}
333
334	a[j] = e;	68,957✔
335	}	68,957✔
336
337
338	/*
339	* Check whether pointer e is non NULL and different from
340	* PMAP2_DELETED. (We use the fact that NULL = 0 and PMAP2_DELETED = 1.
341	*/
342	static inline bool live_record(const pmap2_rec_t *e) {	116,096✔
343	return (((uintptr_t) e) >> 1) != 0;	116,096✔
344	}
345
346
347	/*
348	* Cleanup: remove all the deletion marks
349	*/
350	static void pmap2_htbl_cleanup(pmap2_htbl_t *table) {	6✔
351	pmap2_rec_t **tmp;
352	pmap2_rec_t *e;
353	uint32_t i, n, mask;
354
355	n = table->size;	6✔
356	assert(is_power_of_two(n));
357
358	tmp = (pmap2_rec_t *) safe_malloc(n sizeof(pmap2_rec_t *));	6✔
359	for (i=0; i<n; i++) {	1,414✔
360	tmp[i] = NULL;	1,408✔
361	}
362
363	mask = n - 1;	6✔
364	for (i=0; i<n; i++) {	1,414✔
365	e = table->data[i];	1,408✔
366	if (live_record(e)) {	1,408✔
367	pmap2_htbl_clean_copy(tmp, e, mask);	113✔
368	}
369	}
370
371	safe_free(table->data);	6✔
372	table->data = tmp;	6✔
373	table->ndeleted = 0;	6✔
374	}	6✔
375
376
377
378	/*
379	* Cleanup if the cleanup threshold is reached.
380	* Do nothing otherwise.
381	*/
382	static inline void pmap2_htbl_cleanup_if_needed(pmap2_htbl_t *table) {	36✔
383	if (table->ndeleted > table->cleanup_threshold) {	36✔
384	pmap2_htbl_cleanup(table);	6✔
385	}
386	}	36✔
387
388
389	/*
390	* Double the size and remove the deletion marks
391	*/
392	static void pmap2_htbl_extend(pmap2_htbl_t *table) {	84✔
393	pmap2_rec_t **tmp;
394	pmap2_rec_t *e;
395	uint32_t i, n, new_size, mask;
396
397	n = table->size;	84✔
398	new_size = 2 * n;	84✔
399	if (new_size >= PMAP2_MAX_HTBL_SIZE) {	84✔
400	out_of_memory();	×
401	}
402
403	assert(is_power_of_two(new_size));
404
405	tmp = (pmap2_rec_t *) safe_malloc(new_size sizeof(pmap2_rec_t *));	84✔
406	for (i=0; i<new_size; i++) {	229,460✔
407	tmp[i] = NULL;	229,376✔
408	}
409
410	mask = new_size - 1;	84✔
411	for (i=0; i<n; i++) {	114,772✔
412	e = table->data[i];	114,688✔
413	if (live_record(e)) {	114,688✔
414	pmap2_htbl_clean_copy(tmp, e, mask);	68,844✔
415	}
416	}
417
418	safe_free(table->data);	84✔
419	table->data = tmp;	84✔
420	table->ndeleted = 0;	84✔
421	table->size = new_size;	84✔
422	table->resize_threshold = (uint32_t) (new_size * PMAP2_HTBL_RESIZE_RATIO);	84✔
423	table->cleanup_threshold = (uint32_t) (new_size * PMAP2_HTBL_CLEANUP_RATIO);	84✔
424	}	84✔
425
426
427	/*
428	* Remove e from the table.
429	* - e must be present
430	*/
431	static void pmap2_htbl_remove(pmap2_htbl_t table, pmap2_rec_t e) {	732✔
432	uint32_t mask, j;
433
434	assert(is_power_of_two(table->size));
435
436	mask = table->size - 1;	732✔
437	j = pmap2_hash(e->k0, e->k1) & mask;	732✔
438	while (table->data[j] != e) {	1,012✔
439	j ++;	280✔
440	j &= mask;	280✔
441	}
442
443	table->data[j] = PMAP2_DELETED;	732✔
444	table->nelems --;	732✔
445	table->ndeleted ++;	732✔
446	}	732✔
447
448
449
450
451	/**************
452	* FULL MAP *
453	*************/
454
455	/*
456	* Initialize everything
457	*/
458	void init_pmap2(pmap2_t *pmap) {	147✔
459	init_pmap2_htbl(&pmap->htbl);	147✔
460	init_pmap2_stack(&pmap->stack);	147✔
461	init_pmap2_bank(&pmap->bank);	147✔
462	}	147✔
463
464
465	/*
466	* Delete everything
467	*/
468	void delete_pmap2(pmap2_t *pmap) {	147✔
469	delete_pmap2_htbl(&pmap->htbl);	147✔
470	delete_pmap2_stack(&pmap->stack);	147✔
471	delete_pmap2_bank(&pmap->bank);	147✔
472	}	147✔
473
474
475	/*
476	* Empty the table and set current level to 0
477	*/
478	void reset_pmap2(pmap2_t *pmap) {	×
479	reset_pmap2_htbl(&pmap->htbl);	×
480	reset_pmap2_stack(&pmap->stack);	×
481	reset_pmap2_bank(&pmap->bank);	×
482	}	×
483
484
485
486	/*
487	* Remove from htbl all the records allocated after the mark b, i
488	* - b = block index = free_block at the time push was called
489	* - i = index in block = alloc_ptr at the time push was called
490	*/
491	static void remove_level(pmap2_bank_t bank, pmap2_htbl_t htbl, uint32_t b, uint32_t i) {	36✔
492	uint32_t n, p;
493	pmap2_rec_t *blk;
494
495	/*
496	* n = current free_block
497	* p = current alloc_ptr
498	*/
499	n = bank->free_block;	36✔
500	p = bank->alloc_ptr;	36✔
501
502	/*
503	* Restore free_block and alloc_ptr
504	*/
505	bank->free_block = b;	36✔
506	bank->alloc_ptr = i;	36✔
507
508
509	/*
510	* Records to remove:
511	* - in block b-1: all records from i to BLOCK_SIZE -1
512	* - in blocks b to n-2: all records (from 0 to BLOCK_SIZE - 1)
513	* - in block n-1: all records from 0 to p-1
514	*/
515	if (i == PMAP2_BLOCK_SIZE) {	36✔
516	// either b = 0 or nothing to delete in block b-1
517	i = 0;	18✔
518	b ++;	18✔
519	}
520
521	assert(b > 0);
522
523	while (b < n) {	36✔
524	blk = bank->block[b - 1];	×
525	while (i < PMAP2_BLOCK_SIZE) {	×
526	pmap2_htbl_remove(htbl, blk + i);	×
527	i ++;	×
528	}
529	i = 0;	×
530	b ++;	×
531	}
532
533	// last block:
534	assert(b == n && b > 0);
535	blk = bank->block[b - 1];	36✔
536	while (i < p) {	768✔
537	pmap2_htbl_remove(htbl, blk + i);	732✔
538	i ++;	732✔
539	}
540	}	36✔
541
542
543	/*
544	* Pop: remove all records allocated at the current level
545	* - current level must be positive
546	*/
547	void pmap2_pop(pmap2_t *pmap) {	85✔
548	pmap2_stack_t *stack;
549	uint32_t i;
550
551	stack = &pmap->stack;	85✔
552	assert(stack->current_level > 0 && stack->current_level >= stack->top_level);
553
554	if (stack->current_level == stack->top_level) {	85✔
555	assert(stack->nmarks > 0);
556	i = stack->nmarks - 1;	36✔
557	assert(stack->data[i].level == stack->current_level);
558	remove_level(&pmap->bank, &pmap->htbl, stack->data[i].block_id, stack->data[i].alloc_idx);	36✔
559	pmap2_htbl_cleanup_if_needed(&pmap->htbl);	36✔
560	pop_alloc_mark(stack);	36✔
561	}
562
563	stack->current_level --;	85✔
564
565	assert(stack->current_level >= stack->top_level);
566	}	85✔
567
568
569
570	/*
571	* Search for record of key <k0, k1>
572	* - return NULL if there's no matching record
573	*/
574	pmap2_rec_t pmap2_find(const pmap2_t pmap, int32_t k0, int32_t k1) {	91,813✔
575	const pmap2_htbl_t *htbl;
576	pmap2_rec_t *e;
577	uint32_t i, mask;
578
579	htbl = &pmap->htbl;	91,813✔
580	assert(htbl->nelems + htbl->ndeleted < htbl->size); // otherwise the function loops
581
582	assert(is_power_of_two(htbl->size));
583	mask = htbl->size -1;	91,813✔
584
585	i = pmap2_hash(k0, k1) & mask;	91,813✔
586	for (;;) {
587	e = htbl->data[i];	178,598✔
588	if (e == NULL \|\| (e != PMAP2_DELETED && e->k0 == k0 && e->k1 == k1)) {	178,598✔
589	return e;	91,813✔
590	}
591	i ++;	86,785✔
592	i &= mask;	86,785✔
593	}
594	}
595
596
597
598	/*
599	* Push the current (free_block + alloc_ptr) onto the stack if current_level > top_level
600	*/
601	static inline void push_alloc_mark_if_needed(pmap2_stack_t stack, pmap2_bank_t bank) {	53,411✔
602	if (stack->current_level > stack->top_level) {	53,411✔
603	push_alloc_mark(stack, bank->free_block, bank->alloc_ptr);	46✔
604	}
605	}	53,411✔
606
607
608	/*
609	* Find or add a record with key <k0, k1>
610	* - if a new record is created, set its value to -1
611	*/
612	pmap2_rec_t pmap2_get(pmap2_t pmap, int32_t k0, int32_t k1) {	53,411✔
613	pmap2_htbl_t *htbl;
614	pmap2_rec_t *e;
615	uint32_t i, j, mask;
616
617	htbl = &pmap->htbl;	53,411✔
618	assert(htbl->nelems + htbl->ndeleted < htbl->size);
619
620	assert(is_power_of_two(htbl->size));
621	mask = htbl->size - 1;	53,411✔
622
623	i = pmap2_hash(k0, k1) & mask;	53,411✔
624	for (;;) {
625	e = htbl->data[i];	109,981✔
626	if (e == NULL) goto add;	109,981✔
627	if (e == PMAP2_DELETED) break;	56,760✔
628	if (e->k0 == k0 && e->k1 == k1) goto found;	56,570✔
629	i ++;	56,570✔
630	i &= mask;	56,570✔
631	}
632
633	// i = index where new record can be added
634	assert(htbl->data[i] == PMAP2_DELETED);
635
636	j = i;	190✔
637	for (;;) {
638	j ++;	417✔
639	j &= mask;	417✔
640	e = htbl->data[j];	417✔
641	if (e == NULL) {	417✔
642	htbl->ndeleted --;	190✔
643	goto add;	190✔
644	}
645	if (e != PMAP2_DELETED && e->k0 == k0 && e->k1 == k1) goto found;	227✔
646	}
647
648	add:	53,411✔
649	/*
650	* Create a new record and store it in htbl->data[i].
651	*/
652	push_alloc_mark_if_needed(&pmap->stack, &pmap->bank);	53,411✔
653
654	e = alloc_pmap2_record(&pmap->bank);	53,411✔
655	e->k0 = k0;	53,411✔
656	e->k1 = k1;	53,411✔
657	e->val = -1;	53,411✔
658	htbl->data[i] = e;	53,411✔
659
660	htbl->nelems ++;	53,411✔
661	if (htbl->nelems + htbl->ndeleted > htbl->resize_threshold) {	53,411✔
662	pmap2_htbl_extend(htbl);	84✔
663	}
664
665	found:	53,327✔
666	assert(e->k0 == k0 && e->k1 == k1);
667	return e;	53,411✔
668	}
669
670
671
672
673	/*
674	* ITERATOR
675	* - call f(aux, p) for every p in the table
676	*/
677	void pmap2_iterate(pmap2_t pmap, void aux, pmap2_iterator_t f) {	×
678	pmap2_htbl_t *htbl;
679	pmap2_rec_t *p;
680	uint32_t i, n;
681
682	htbl = &pmap->htbl;	×
683	n = htbl->size;	×
684	for (i=0; i<n; i++) {	×
685	p = htbl->data[i];	×
686	if (live_record(p)) {	×
687	f(aux, p);	×
688	}
689	}
690	}	×

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