verif/Spin/Src5.1.6/tl_cache.c

   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 }