| 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 | } |