1 /***** tl_spin: tl_cache.c *****/
2
3 /*
4 * This file is part of the public release of Spin. It is subject to the
5 * terms in the LICENSE file that is included in this source directory.
6 * Tool documentation is available at http://spinroot.com
7 *
8 * Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
9 * presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
10 */
11
12 #include "tl.h"
13
14 typedef struct Cache {
15 Node *before;
16 Node *after;
17 int same;
18 struct Cache *nxt;
19 } Cache;
20
21 static Cache *stored = (Cache *) 0;
22 static unsigned long Caches, CacheHits;
23
24 static int ismatch(Node *, Node *);
25 static int sameform(Node *, Node *);
26
27 extern void fatal(char *, char *);
28
29 void
ini_cache(void)30 ini_cache(void)
31 {
32 stored = (Cache *) 0;
33 Caches = 0;
34 CacheHits = 0;
35 }
36
37 #if 0
38 void
39 cache_dump(void)
40 { Cache *d; int nr=0;
41
42 printf("\nCACHE DUMP:\n");
43 for (d = stored; d; d = d->nxt, nr++)
44 { if (d->same) continue;
45 printf("B%3d: ", nr); dump(d->before); printf("\n");
46 printf("A%3d: ", nr); dump(d->after); printf("\n");
47 }
48 printf("============\n");
49 }
50 #endif
51
52 Node *
in_cache(Node * n)53 in_cache(Node *n)
54 { Cache *d; int nr=0;
55
56 for (d = stored; d; d = d->nxt, nr++)
57 if (isequal(d->before, n))
58 { CacheHits++;
59 if (d->same && ismatch(n, d->before)) return n;
60 return dupnode(d->after);
61 }
62 return ZN;
63 }
64
65 Node *
cached(Node * n)66 cached(Node *n)
67 { Cache *d;
68 Node *m;
69
70 if (!n) return n;
71 if ((m = in_cache(n)) != ZN)
72 return m;
73
74 Caches++;
75 d = (Cache *) tl_emalloc(sizeof(Cache));
76 d->before = dupnode(n);
77 d->after = Canonical(n); /* n is released */
78
79 if (ismatch(d->before, d->after))
80 { d->same = 1;
81 releasenode(1, d->after);
82 d->after = d->before;
83 }
84 d->nxt = stored;
85 stored = d;
86 return dupnode(d->after);
87 }
88
89 void
cache_stats(void)90 cache_stats(void)
91 {
92 printf("cache stores : %9ld\n", Caches);
93 printf("cache hits : %9ld\n", CacheHits);
94 }
95
96 void
releasenode(int all_levels,Node * n)97 releasenode(int all_levels, Node *n)
98 {
99 if (!n) return;
100
101 if (all_levels)
102 { releasenode(1, n->lft);
103 n->lft = ZN;
104 releasenode(1, n->rgt);
105 n->rgt = ZN;
106 }
107 tfree((void *) n);
108 }
109
110 Node *
tl_nn(int t,Node * ll,Node * rl)111 tl_nn(int t, Node *ll, Node *rl)
112 { Node *n = (Node *) tl_emalloc(sizeof(Node));
113
114 n->ntyp = (short) t;
115 n->lft = ll;
116 n->rgt = rl;
117
118 return n;
119 }
120
121 Node *
getnode(Node * p)122 getnode(Node *p)
123 { Node *n;
124
125 if (!p) return p;
126
127 n = (Node *) tl_emalloc(sizeof(Node));
128 n->ntyp = p->ntyp;
129 n->sym = p->sym; /* same name */
130 n->lft = p->lft;
131 n->rgt = p->rgt;
132
133 return n;
134 }
135
136 Node *
dupnode(Node * n)137 dupnode(Node *n)
138 { Node *d;
139
140 if (!n) return n;
141 d = getnode(n);
142 d->lft = dupnode(n->lft);
143 d->rgt = dupnode(n->rgt);
144 return d;
145 }
146
147 int
one_lft(int ntyp,Node * x,Node * in)148 one_lft(int ntyp, Node *x, Node *in)
149 {
150 if (!x) return 1;
151 if (!in) return 0;
152
153 if (sameform(x, in))
154 return 1;
155
156 if (in->ntyp != ntyp)
157 return 0;
158
159 if (one_lft(ntyp, x, in->lft))
160 return 1;
161
162 return one_lft(ntyp, x, in->rgt);
163 }
164
165 int
all_lfts(int ntyp,Node * from,Node * in)166 all_lfts(int ntyp, Node *from, Node *in)
167 {
168 if (!from) return 1;
169
170 if (from->ntyp != ntyp)
171 return one_lft(ntyp, from, in);
172
173 if (!one_lft(ntyp, from->lft, in))
174 return 0;
175
176 return all_lfts(ntyp, from->rgt, in);
177 }
178
179 int
sametrees(int ntyp,Node * a,Node * b)180 sametrees(int ntyp, Node *a, Node *b)
181 { /* toplevel is an AND or OR */
182 /* both trees are right-linked, but the leafs */
183 /* can be in different places in the two trees */
184
185 if (!all_lfts(ntyp, a, b))
186 return 0;
187
188 return all_lfts(ntyp, b, a);
189 }
190
191 static int /* a better isequal() */
sameform(Node * a,Node * b)192 sameform(Node *a, Node *b)
193 {
194 if (!a && !b) return 1;
195 if (!a || !b) return 0;
196 if (a->ntyp != b->ntyp) return 0;
197
198 if (a->sym
199 && b->sym
200 && strcmp(a->sym->name, b->sym->name) != 0)
201 return 0;
202
203 switch (a->ntyp) {
204 case TRUE:
205 case FALSE:
206 return 1;
207 case PREDICATE:
208 if (!a->sym || !b->sym) fatal("sameform...", (char *) 0);
209 return !strcmp(a->sym->name, b->sym->name);
210
211 case NOT:
212 #ifdef NXT
213 case NEXT:
214 #endif
215 case CEXPR:
216 return sameform(a->lft, b->lft);
217 case U_OPER:
218 case V_OPER:
219 if (!sameform(a->lft, b->lft))
220 return 0;
221 if (!sameform(a->rgt, b->rgt))
222 return 0;
223 return 1;
224
225 case AND:
226 case OR: /* the hard case */
227 return sametrees(a->ntyp, a, b);
228
229 default:
230 printf("type: %d\n", a->ntyp);
231 fatal("cannot happen, sameform", (char *) 0);
232 }
233
234 return 0;
235 }
236
237 int
isequal(Node * a,Node * b)238 isequal(Node *a, Node *b)
239 {
240 if (!a && !b)
241 return 1;
242
243 if (!a || !b)
244 { if (!a)
245 { if (b->ntyp == TRUE)
246 return 1;
247 } else
248 { if (a->ntyp == TRUE)
249 return 1;
250 }
251 return 0;
252 }
253 if (a->ntyp != b->ntyp)
254 return 0;
255
256 if (a->sym
257 && b->sym
258 && strcmp(a->sym->name, b->sym->name) != 0)
259 return 0;
260
261 if (isequal(a->lft, b->lft)
262 && isequal(a->rgt, b->rgt))
263 return 1;
264
265 return sameform(a, b);
266 }
267
268 static int
ismatch(Node * a,Node * b)269 ismatch(Node *a, Node *b)
270 {
271 if (!a && !b) return 1;
272 if (!a || !b) return 0;
273 if (a->ntyp != b->ntyp) return 0;
274
275 if (a->sym
276 && b->sym
277 && strcmp(a->sym->name, b->sym->name) != 0)
278 return 0;
279
280 if (ismatch(a->lft, b->lft)
281 && ismatch(a->rgt, b->rgt))
282 return 1;
283
284 return 0;
285 }
286
287 int
any_term(Node * srch,Node * in)288 any_term(Node *srch, Node *in)
289 {
290 if (!in) return 0;
291
292 if (in->ntyp == AND)
293 return any_term(srch, in->lft) ||
294 any_term(srch, in->rgt);
295
296 return isequal(in, srch);
297 }
298
299 int
any_and(Node * srch,Node * in)300 any_and(Node *srch, Node *in)
301 {
302 if (!in) return 0;
303
304 if (srch->ntyp == AND)
305 return any_and(srch->lft, in) &&
306 any_and(srch->rgt, in);
307
308 return any_term(srch, in);
309 }
310
311 int
any_lor(Node * srch,Node * in)312 any_lor(Node *srch, Node *in)
313 {
314 if (!in) return 0;
315
316 if (in->ntyp == OR)
317 return any_lor(srch, in->lft) ||
318 any_lor(srch, in->rgt);
319
320 return isequal(in, srch);
321 }
322
323 int
anywhere(int tok,Node * srch,Node * in)324 anywhere(int tok, Node *srch, Node *in)
325 {
326 if (!in) return 0;
327
328 switch (tok) {
329 case AND: return any_and(srch, in);
330 case OR: return any_lor(srch, in);
331 case 0: return any_term(srch, in);
332 }
333 fatal("cannot happen, anywhere", (char *) 0);
334 return 0;
335 }
336