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

77.38

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

/*
 * STORE FOR ALLOCATION OF (SMALL) OBJECTS
 */

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

#include "utils/memalloc.h"
#include "utils/object_stores.h"
#include "mt/thread_macros.h"

#ifndef NDEBUG

/*
 * For debugging: check alignment.
 * We want pointers aligned to multiples of 8.
 */
static bool ptr_is_aligned(void *p) {
  uintptr_t x;

  x = (uintptr_t) p;
  return (x & (uintptr_t) 7) == 0;
}

// p <= q here
static bool offset_is_aligned(void *p, void *q) {
  uintptr_t x, y;

  x = (uintptr_t) p;
  y = (uintptr_t) q;
  assert(x <= y);

  return ((y - x) & (uintptr_t) 7) == 0;
}

#endif



/*
 * Initialize s:
 * - objsize = size of all objects in s
 * - n = number of objects per block
 */
static void _o_init_objstore(object_store_t *s, uint32_t objsize, uint32_t n) {
  assert(objsize <= MAX_OBJ_SIZE);
  assert(0 < n && n <= MAX_OBJ_PER_BLOCK);

  // round up objsize to a multiple of 8 for pointer alignment
  objsize = (objsize + 7) & ((uint32_t )(~7));

  s->bnk = NULL;
  s->free_list = NULL;
  s->free_index = 0;
  s->objsize = objsize;
  s->blocksize = objsize * n;
}

void init_objstore(object_store_t *s, uint32_t objsize, uint32_t n) {
#ifdef THREAD_SAFE
  create_yices_lock(&(s->lock));
#endif
  MT_PROTECT_VOID(s->lock, _o_init_objstore(s, objsize, n));
}


/*
 * Allocate an object in s
 */
static void *_o_objstore_alloc(object_store_t *s) {
  void *tmp;
  uint32_t i;
  object_bank_t *new_bank;

  tmp = s->free_list;
  if (tmp != NULL) {
    // This may be unsafe. Replaced by memcpy.
    //    s->free_list = * ((void **) tmp);
    memcpy(&s->free_list, tmp, sizeof(void*));

    assert(ptr_is_aligned(tmp));

    return tmp;
  }

  i = s->free_index;
  if (i == 0) {
    new_bank = (object_bank_t *) safe_malloc(sizeof(object_bank_t) + s->blocksize * sizeof(char));
    new_bank->h.next = s->bnk;
    s->bnk = new_bank;
    i = s->blocksize;

    assert(offset_is_aligned(new_bank, new_bank->block));
  }

  assert(i >= s->objsize);

  i -= s->objsize;
  s->free_index = i;
  tmp = s->bnk->block + i;

  assert(ptr_is_aligned(tmp));

  return tmp;
}

void *objstore_alloc(object_store_t *s) {
  MT_PROTECT(void *, s->lock, _o_objstore_alloc(s));
}


/*
 * Delete all objects
 */
static void _o_delete_objstore(object_store_t *s) {
  object_bank_t *b, *next;

  b = s->bnk;
  while (b != NULL) {
    next = b->h.next;
    safe_free(b);
    b = next;
  }

  s->bnk = NULL;
  s->free_list = NULL;
  s->free_index = 0;
}

void delete_objstore(object_store_t *s) {
  MT_PROTECT_VOID(s->lock, _o_delete_objstore(s));
#ifdef THREAD_SAFE
  destroy_yices_lock(&(s->lock));
#endif
}

/*
 * Free an allocated object: add it to s->free_list.
 * next pointer is stored in *object
 */
static void _o_objstore_free(object_store_t *s, void *object) {
  /*
   * BUG: This violates the strict aliasing rules and causes
   * errors when optimizations are enabled?
   */
  //  * ((void **) object) = s->free_list;
  // Try this instead.
  memcpy(object, &s->free_list, sizeof(void*));
  s->free_list = object;
}
void objstore_free(object_store_t *s, void *object) {
  MT_PROTECT_VOID(s->lock, _o_objstore_free(s, object));
}

/*
 * Apply finalizer f to all objects then delete s
 */
static void _o_objstore_delete_finalize(object_store_t *s, void (*f)(void *)) {
  object_bank_t *b, *next;
  void *obj;
  uint32_t k, i;

  b = s->bnk;
  k = s->free_index;
  while (b != NULL) {
    next = b->h.next;
    for (i=k; i<s->blocksize; i += s->objsize) {
      obj = (void *) (b->block + i);
      f(obj);
    }
    safe_free(b);
    k = 0;
    b = next;
  }

  s->bnk = NULL;
  s->free_list = NULL;
  s->free_index = 0;
}
void objstore_delete_finalize(object_store_t *s, void (*f)(void *)) {
  MT_PROTECT_VOID(s->lock, _o_objstore_delete_finalize(s, f));
#ifdef THREAD_SAFE
  destroy_yices_lock(&(s->lock));
#endif
}


/*
 * Reset store s: remove all objects
 * - keep only one bank
 */
static void _o_reset_objstore(object_store_t *s) {
  object_bank_t *b, *next;

  b = s->bnk;
  if (b != NULL) {
    next = b->h.next;
    while (next != NULL) {
      safe_free(b);
      b = next;
      next = b->h.next;
    }
  }

  s->bnk = b;
  s->free_list = NULL;
  s->free_index = 0;
}
void reset_objstore(object_store_t *s) {
  MT_PROTECT_VOID(s->lock, _o_reset_objstore(s));
}

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	* STORE FOR ALLOCATION OF (SMALL) OBJECTS
21	*/
22
23	#include <assert.h>
24	#include <stdbool.h>
25	#include <stddef.h>
26
27	#include "utils/memalloc.h"
28	#include "utils/object_stores.h"
29	#include "mt/thread_macros.h"
30
31	#ifndef NDEBUG
32
33	/*
34	* For debugging: check alignment.
35	* We want pointers aligned to multiples of 8.
36	*/
37	static bool ptr_is_aligned(void *p) {
38	uintptr_t x;
39
40	x = (uintptr_t) p;
41	return (x & (uintptr_t) 7) == 0;
42	}
43
44	// p <= q here
45	static bool offset_is_aligned(void p, void q) {
46	uintptr_t x, y;
47
48	x = (uintptr_t) p;
49	y = (uintptr_t) q;
50	assert(x <= y);
51
52	return ((y - x) & (uintptr_t) 7) == 0;
53	}
54
55	#endif
56
57
58
59	/*
60	* Initialize s:
61	* - objsize = size of all objects in s
62	* - n = number of objects per block
63	*/
64	static void _o_init_objstore(object_store_t *s, uint32_t objsize, uint32_t n) {	217,558✔
65	assert(objsize <= MAX_OBJ_SIZE);
66	assert(0 < n && n <= MAX_OBJ_PER_BLOCK);
67
68	// round up objsize to a multiple of 8 for pointer alignment
69	objsize = (objsize + 7) & ((uint32_t )(~7));	217,558✔
70
71	s->bnk = NULL;	217,558✔
72	s->free_list = NULL;	217,558✔
73	s->free_index = 0;	217,558✔
74	s->objsize = objsize;	217,558✔
75	s->blocksize = objsize * n;	217,558✔
76	}	217,558✔
77
78	void init_objstore(object_store_t *s, uint32_t objsize, uint32_t n) {	217,558✔
79	#ifdef THREAD_SAFE
80	create_yices_lock(&(s->lock));	217,558✔
81	#endif
82	MT_PROTECT_VOID(s->lock, _o_init_objstore(s, objsize, n));	217,558✔
83	}	217,558✔
84
85
86	/*
87	* Allocate an object in s
88	*/
89	static void _o_objstore_alloc(object_store_t s) {	514,736✔
90	void *tmp;
91	uint32_t i;
92	object_bank_t *new_bank;
93
94	tmp = s->free_list;	514,736✔
95	if (tmp != NULL) {	514,736✔
96	// This may be unsafe. Replaced by memcpy.
97	// s->free_list = * ((void **) tmp);
98	memcpy(&s->free_list, tmp, sizeof(void*));	95,894✔
99
100	assert(ptr_is_aligned(tmp));
101
102	return tmp;	95,894✔
103	}
104
105	i = s->free_index;	418,842✔
106	if (i == 0) {	418,842✔
107	new_bank = (object_bank_t ) safe_malloc(sizeof(object_bank_t) + s->blocksize sizeof(char));	134,193✔
108	new_bank->h.next = s->bnk;	134,193✔
109	s->bnk = new_bank;	134,193✔
110	i = s->blocksize;	134,193✔
111
112	assert(offset_is_aligned(new_bank, new_bank->block));
113	}
114
115	assert(i >= s->objsize);
116
117	i -= s->objsize;	418,842✔
118	s->free_index = i;	418,842✔
119	tmp = s->bnk->block + i;	418,842✔
120
121	assert(ptr_is_aligned(tmp));
122
123	return tmp;	418,842✔
124	}
125
126	void objstore_alloc(object_store_t s) {	514,736✔
127	MT_PROTECT(void *, s->lock, _o_objstore_alloc(s));	514,736✔
128	}
129
130
131	/*
132	* Delete all objects
133	*/
134	static void _o_delete_objstore(object_store_t *s) {	217,558✔
135	object_bank_t b, next;
136
137	b = s->bnk;	217,558✔
138	while (b != NULL) {	351,634✔
139	next = b->h.next;	134,076✔
140	safe_free(b);	134,076✔
141	b = next;	134,076✔
142	}
143
144	s->bnk = NULL;	217,558✔
145	s->free_list = NULL;	217,558✔
146	s->free_index = 0;	217,558✔
147	}	217,558✔
148
149	void delete_objstore(object_store_t *s) {	217,558✔
150	MT_PROTECT_VOID(s->lock, _o_delete_objstore(s));	217,558✔
151	#ifdef THREAD_SAFE
152	destroy_yices_lock(&(s->lock));	217,558✔
153	#endif
154	}	217,558✔
155
156	/*
157	* Free an allocated object: add it to s->free_list.
158	* next pointer is stored in *object
159	*/
160	static void _o_objstore_free(object_store_t s, void object) {	433,175✔
161	/*
162	* BUG: This violates the strict aliasing rules and causes
163	* errors when optimizations are enabled?
164	*/
165	// * ((void **) object) = s->free_list;
166	// Try this instead.
167	memcpy(object, &s->free_list, sizeof(void*));	433,175✔
168	s->free_list = object;	433,175✔
169	}	433,175✔
170	void objstore_free(object_store_t s, void object) {	433,175✔
171	MT_PROTECT_VOID(s->lock, _o_objstore_free(s, object));	433,175✔
172	}	433,175✔
173
174	/*
175	* Apply finalizer f to all objects then delete s
176	*/
177	static void _o_objstore_delete_finalize(object_store_t s, void (f)(void *)) {	×
178	object_bank_t b, next;
179	void *obj;
180	uint32_t k, i;
181
182	b = s->bnk;	×
183	k = s->free_index;	×
184	while (b != NULL) {	×
185	next = b->h.next;	×
186	for (i=k; i<s->blocksize; i += s->objsize) {	×
187	obj = (void *) (b->block + i);	×
188	f(obj);	×
189	}
190	safe_free(b);	×
191	k = 0;	×
192	b = next;	×
193	}
194
195	s->bnk = NULL;	×
196	s->free_list = NULL;	×
197	s->free_index = 0;	×
198	}	×
199	void objstore_delete_finalize(object_store_t s, void (f)(void *)) {	×
200	MT_PROTECT_VOID(s->lock, _o_objstore_delete_finalize(s, f));	×
201	#ifdef THREAD_SAFE
202	destroy_yices_lock(&(s->lock));	×
203	#endif
204	}	×
205
206
207	/*
208	* Reset store s: remove all objects
209	* - keep only one bank
210	*/
211	static void _o_reset_objstore(object_store_t *s) {	195,325✔
212	object_bank_t b, next;
213
214	b = s->bnk;	195,325✔
215	if (b != NULL) {	195,325✔
216	next = b->h.next;	29,645✔
217	while (next != NULL) {	29,762✔
218	safe_free(b);	117✔
219	b = next;	117✔
220	next = b->h.next;	117✔
221	}
222	}
223
224	s->bnk = b;	195,325✔
225	s->free_list = NULL;	195,325✔
226	s->free_index = 0;	195,325✔
227	}	195,325✔
228	void reset_objstore(object_store_t *s) {	195,325✔
229	MT_PROTECT_VOID(s->lock, _o_reset_objstore(s));	195,325✔
230	}	195,325✔

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