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