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