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