sys/src/cmd/spin/tl_cache.c

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