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 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 * 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 * 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 92 cache_stats(void) 93 { 94 printf("cache stores : %9ld\n", Caches); 95 printf("cache hits : %9ld\n", CacheHits); 96 } 97 98 void 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 * 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 * 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 * 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 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 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 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() */ 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 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 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 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 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 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 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