1 /***** ltl2ba : mem.c *****/
2
3 /* Written by Denis Oddoux, LIAFA, France */
4 /* Copyright (c) 2001 Denis Oddoux */
5 /* Modified by Paul Gastin, LSV, France */
6 /* Copyright (c) 2007 Paul Gastin */
7 /* */
8 /* This program is free software; you can redistribute it and/or modify */
9 /* it under the terms of the GNU General Public License as published by */
10 /* the Free Software Foundation; either version 2 of the License, or */
11 /* (at your option) any later version. */
12 /* */
13 /* This program is distributed in the hope that it will be useful, */
14 /* but WITHOUT ANY WARRANTY; without even the implied warranty of */
15 /* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
16 /* GNU General Public License for more details. */
17 /* */
18 /* You should have received a copy of the GNU General Public License */
19 /* along with this program; if not, write to the Free Software */
20 /* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/
21 /* */
22 /* Based on the translation algorithm by Gastin and Oddoux, */
23 /* presented at the 13th International Conference on Computer Aided */
24 /* Verification, CAV 2001, Paris, France. */
25 /* Proceedings - LNCS 2102, pp. 53-65 */
26 /* */
27 /* Send bug-reports and/or questions to Paul Gastin */
28 /* http://www.lsv.ens-cachan.fr/~gastin */
29 /* */
30 /* Some of the code in this file was taken from the Spin software */
31 /* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */
32
33 #include "ltl2ba.h"
34
35 #if 1
36 #define log(e, u, d) event[e][(int) u] += (long) d;
37 #else
38 #define log(e, u, d)
39 #endif
40
41 #define A_LARGE 80
42 #define A_USER 0x55000000
43 #define NOTOOBIG 32768
44
45 #define POOL 0
46 #define ALLOC 1
47 #define FREE 2
48 #define NREVENT 3
49
50 extern unsigned long All_Mem;
51 extern int tl_verbose;
52
53 ATrans *atrans_list = (ATrans *)0;
54 GTrans *gtrans_list = (GTrans *)0;
55 BTrans *btrans_list = (BTrans *)0;
56
57 int aallocs = 0, afrees = 0, apool = 0;
58 int gallocs = 0, gfrees = 0, gpool = 0;
59 int ballocs = 0, bfrees = 0, bpool = 0;
60
61 union M {
62 long size;
63 union M *link;
64 };
65
66 static union M *freelist[A_LARGE];
67 static long req[A_LARGE];
68 static long event[NREVENT][A_LARGE];
69
70 void *
tl_emalloc(int U)71 tl_emalloc(int U)
72 { union M *m;
73 long r, u;
74 void *rp;
75
76 u = (long) ((U-1)/sizeof(union M) + 2);
77
78 if (u >= A_LARGE)
79 { log(ALLOC, 0, 1);
80 if (tl_verbose)
81 printf("tl_spin: memalloc %ld bytes\n", u);
82 m = (union M *) emalloc((int) u*sizeof(union M));
83 All_Mem += (unsigned long) u*sizeof(union M);
84 } else
85 { if (!freelist[u])
86 { r = req[u] += req[u] ? req[u] : 1;
87 if (r >= NOTOOBIG)
88 r = req[u] = NOTOOBIG;
89 log(POOL, u, r);
90 freelist[u] = (union M *)
91 emalloc((int) r*u*sizeof(union M));
92 All_Mem += (unsigned long) r*u*sizeof(union M);
93 m = freelist[u] + (r-2)*u;
94 for ( ; m >= freelist[u]; m -= u)
95 m->link = m+u;
96 }
97 log(ALLOC, u, 1);
98 m = freelist[u];
99 freelist[u] = m->link;
100 }
101 m->size = (u|A_USER);
102
103 for (r = 1; r < u; )
104 (&m->size)[r++] = 0;
105
106 rp = (void *) (m+1);
107 memset(rp, 0, U);
108 return rp;
109 }
110
111 void
tfree(void * v)112 tfree(void *v)
113 { union M *m = (union M *) v;
114 long u;
115
116 --m;
117 if ((m->size&0xFF000000) != A_USER)
118 Fatal("releasing a free block");
119
120 u = (m->size &= 0xFFFFFF);
121 if (u >= A_LARGE)
122 { log(FREE, 0, 1);
123 /* free(m); */
124 } else
125 { log(FREE, u, 1);
126 m->link = freelist[u];
127 freelist[u] = m;
128 }
129 }
130
emalloc_atrans()131 ATrans* emalloc_atrans() {
132 ATrans *result;
133 if(!atrans_list) {
134 result = (ATrans *)tl_emalloc(sizeof(GTrans));
135 result->pos = new_set(1);
136 result->neg = new_set(1);
137 result->to = new_set(0);
138 apool++;
139 }
140 else {
141 result = atrans_list;
142 atrans_list = atrans_list->nxt;
143 result->nxt = (ATrans *)0;
144 }
145 aallocs++;
146 return result;
147 }
148
free_atrans(ATrans * t,int rec)149 void free_atrans(ATrans *t, int rec) {
150 if(!t) return;
151 if(rec) free_atrans(t->nxt, rec);
152 t->nxt = atrans_list;
153 atrans_list = t;
154 afrees++;
155 }
156
free_all_atrans()157 void free_all_atrans() {
158 ATrans *t;
159 while(atrans_list) {
160 t = atrans_list;
161 atrans_list = t->nxt;
162 tfree(t->to);
163 tfree(t->pos);
164 tfree(t->neg);
165 tfree(t);
166 }
167 }
168
emalloc_gtrans()169 GTrans* emalloc_gtrans() {
170 GTrans *result;
171 if(!gtrans_list) {
172 result = (GTrans *)tl_emalloc(sizeof(GTrans));
173 result->pos = new_set(1);
174 result->neg = new_set(1);
175 result->final = new_set(0);
176 gpool++;
177 }
178 else {
179 result = gtrans_list;
180 gtrans_list = gtrans_list->nxt;
181 }
182 gallocs++;
183 return result;
184 }
185
free_gtrans(GTrans * t,GTrans * sentinel,int fly)186 void free_gtrans(GTrans *t, GTrans *sentinel, int fly) {
187 gfrees++;
188 if(sentinel && (t != sentinel)) {
189 free_gtrans(t->nxt, sentinel, fly);
190 if(fly) t->to->incoming--;
191 }
192 t->nxt = gtrans_list;
193 gtrans_list = t;
194 }
195
emalloc_btrans()196 BTrans* emalloc_btrans() {
197 BTrans *result;
198 if(!btrans_list) {
199 result = (BTrans *)tl_emalloc(sizeof(BTrans));
200 result->pos = new_set(1);
201 result->neg = new_set(1);
202 bpool++;
203 }
204 else {
205 result = btrans_list;
206 btrans_list = btrans_list->nxt;
207 }
208 ballocs++;
209 return result;
210 }
211
free_btrans(BTrans * t,BTrans * sentinel,int fly)212 void free_btrans(BTrans *t, BTrans *sentinel, int fly) {
213 bfrees++;
214 if(sentinel && (t != sentinel)) {
215 free_btrans(t->nxt, sentinel, fly);
216 if(fly) t->to->incoming--;
217 }
218 t->nxt = btrans_list;
219 btrans_list = t;
220 }
221
222 void
a_stats(void)223 a_stats(void)
224 { long p, a, f;
225 int i;
226
227 printf(" size\t pool\tallocs\t frees\n");
228
229 for (i = 0; i < A_LARGE; i++)
230 { p = event[POOL][i];
231 a = event[ALLOC][i];
232 f = event[FREE][i];
233
234 if(p|a|f)
235 printf("%5d\t%6ld\t%6ld\t%6ld\n",
236 i, p, a, f);
237 }
238
239 printf("atrans\t%6d\t%6d\t%6d\n",
240 apool, aallocs, afrees);
241 printf("gtrans\t%6d\t%6d\t%6d\n",
242 gpool, gallocs, gfrees);
243 printf("btrans\t%6d\t%6d\t%6d\n",
244 bpool, ballocs, bfrees);
245 }
246