trunk/verif/Spin/Src5.1.6/structs.c

   1 /***** spin: structs.c *****/
   2
   3 /* Copyright (c) 1989-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 #include "spin.h"
  13 #include "y.tab.h"
  14
  15 typedef struct UType {
  16         Symbol *nm;     /* name of the type */
  17         Lextok *cn;     /* contents */
  18         struct UType *nxt;      /* linked list */
  19 } UType;
  20
  21 extern  Symbol  *Fname;
  22 extern  int     lineno, depth, Expand_Ok, has_hidden;
  23
  24 Symbol  *owner;
  25
  26 static UType *Unames = 0;
  27 static UType *Pnames = 0;
  28
  29 static Lextok   *cpnn(Lextok *, int, int, int);
  30 extern void     sr_mesg(FILE *, int, int);
  31
  32 void
  33 setuname(Lextok *n)
  34 {       UType *tmp;
  35
  36         if (!owner)
  37                 fatal("illegal reference inside typedef", (char *) 0);
  38
  39         for (tmp = Unames; tmp; tmp = tmp->nxt)
  40                 if (!strcmp(owner->name, tmp->nm->name))
  41                 {       non_fatal("typename %s was defined before",
  42                                 tmp->nm->name);
  43                         return;
  44                 }
  45
  46         tmp = (UType *) emalloc(sizeof(UType));
  47         tmp->nm = owner;
  48         tmp->cn = n;
  49         tmp->nxt = Unames;
  50         Unames = tmp;
  51 }
  52
  53 static void
  54 putUname(FILE *fd, UType *tmp)
  55 {       Lextok *fp, *tl;
  56
  57         if (!tmp) return;
  58         putUname(fd, tmp->nxt); /* postorder */
  59         fprintf(fd, "struct %s { /* user defined type */\n",
  60                 tmp->nm->name);
  61         for (fp = tmp->cn; fp; fp = fp->rgt)
  62         for (tl = fp->lft; tl; tl = tl->rgt)
  63                 typ2c(tl->sym);
  64         fprintf(fd, "};\n");
  65 }
  66
  67 void
  68 putunames(FILE *fd)
  69 {
  70         putUname(fd, Unames);
  71 }
  72
  73 int
  74 isutype(char *t)
  75 {       UType *tmp;
  76
  77         for (tmp = Unames; tmp; tmp = tmp->nxt)
  78         {       if (!strcmp(t, tmp->nm->name))
  79                         return 1;
  80         }
  81         return 0;
  82 }
  83
  84 Lextok *
  85 getuname(Symbol *t)
  86 {       UType *tmp;
  87
  88         for (tmp = Unames; tmp; tmp = tmp->nxt)
  89         {       if (!strcmp(t->name, tmp->nm->name))
  90                         return tmp->cn;
  91         }
  92         fatal("%s is not a typename", t->name);
  93         return (Lextok *)0;
  94 }
  95
  96 void
  97 setutype(Lextok *p, Symbol *t, Lextok *vis)     /* user-defined types */
  98 {       int oln = lineno;
  99         Symbol *ofn = Fname;
 100         Lextok *m, *n;
 101
 102         m = getuname(t);
 103         for (n = p; n; n = n->rgt)
 104         {       lineno = n->ln;
 105                 Fname = n->fn;
 106                 if (n->sym->type)
 107                 non_fatal("redeclaration of '%s'", n->sym->name);
 108
 109                 if (n->sym->nbits > 0)
 110                 non_fatal("(%s) only an unsigned can have width-field",
 111                         n->sym->name);
 112
 113                 if (Expand_Ok)
 114                         n->sym->hidden |= (4|8|16); /* formal par */
 115
 116                 if (vis)
 117                 {       if (strncmp(vis->sym->name, ":hide:", (size_t) 6) == 0)
 118                         {       n->sym->hidden |= 1;
 119                                 has_hidden++;
 120                         } else if (strncmp(vis->sym->name, ":show:", (size_t) 6) == 0)
 121                                 n->sym->hidden |= 2;
 122                         else if (strncmp(vis->sym->name, ":local:", (size_t) 7) == 0)
 123                                 n->sym->hidden |= 64;
 124                 }
 125                 n->sym->type = STRUCT;  /* classification   */
 126                 n->sym->Slst = m;       /* structure itself */
 127                 n->sym->Snm  = t;       /* name of typedef  */
 128                 n->sym->Nid  = 0;       /* this is no chan  */
 129                 n->sym->hidden |= 4;
 130                 if (n->sym->nel <= 0)
 131                 non_fatal("bad array size for '%s'", n->sym->name);
 132         }
 133         lineno = oln;
 134         Fname = ofn;
 135 }
 136
 137 static Symbol *
 138 do_same(Lextok *n, Symbol *v, int xinit)
 139 {       Lextok *tmp, *fp, *tl;
 140         int ix = eval(n->lft);
 141         int oln = lineno;
 142         Symbol *ofn = Fname;
 143
 144         lineno = n->ln;
 145         Fname = n->fn;
 146
 147         /* n->sym->type == STRUCT
 148          * index:               n->lft
 149          * subfields:           n->rgt
 150          * structure template:  n->sym->Slst
 151          * runtime values:      n->sym->Sval
 152          */
 153         if (xinit) ini_struct(v);       /* once, at top level */
 154
 155         if (ix >= v->nel || ix < 0)
 156         {       printf("spin: indexing %s[%d] - size is %d\n",
 157                                 v->name, ix, v->nel);
 158                 fatal("indexing error \'%s\'", v->name);
 159         }
 160         if (!n->rgt || !n->rgt->lft)
 161         {       non_fatal("no subfields %s", v->name);  /* i.e., wants all */
 162                 lineno = oln; Fname = ofn;
 163                 return ZS;
 164         }
 165
 166         if (n->rgt->ntyp != '.')
 167         {       printf("bad subfield type %d\n", n->rgt->ntyp);
 168                 alldone(1);
 169         }
 170
 171         tmp = n->rgt->lft;
 172         if (tmp->ntyp != NAME && tmp->ntyp != TYPE)
 173         {       printf("bad subfield entry %d\n", tmp->ntyp);
 174                 alldone(1);
 175         }
 176         for (fp = v->Sval[ix]; fp; fp = fp->rgt)
 177         for (tl = fp->lft; tl; tl = tl->rgt)
 178                 if (!strcmp(tl->sym->name, tmp->sym->name))
 179                 {       lineno = oln; Fname = ofn;
 180                         return tl->sym;
 181                 }
 182         fatal("cannot locate subfield %s", tmp->sym->name);
 183         return ZS;
 184 }
 185
 186 int
 187 Rval_struct(Lextok *n, Symbol *v, int xinit)    /* n varref, v valref */
 188 {       Symbol *tl;
 189         Lextok *tmp;
 190         int ix;
 191
 192         if (!n || !(tl = do_same(n, v, xinit)))
 193                 return 0;
 194
 195         tmp = n->rgt->lft;
 196         if (tmp->sym->type == STRUCT)
 197         {       return Rval_struct(tmp, tl, 0);
 198         } else if (tmp->rgt)
 199                 fatal("non-zero 'rgt' on non-structure", 0);
 200
 201         ix = eval(tmp->lft);
 202         if (ix >= tl->nel || ix < 0)
 203                 fatal("indexing error \'%s\'", tl->name);
 204
 205         return cast_val(tl->type, tl->val[ix], tl->nbits);
 206 }
 207
 208 int
 209 Lval_struct(Lextok *n, Symbol *v, int xinit, int a)  /* a = assigned value */
 210 {       Symbol *tl;
 211         Lextok *tmp;
 212         int ix;
 213
 214         if (!(tl = do_same(n, v, xinit)))
 215                 return 1;
 216
 217         tmp = n->rgt->lft;
 218         if (tmp->sym->type == STRUCT)
 219                 return Lval_struct(tmp, tl, 0, a);
 220         else if (tmp->rgt)
 221                 fatal("non-zero 'rgt' on non-structure", 0);
 222
 223         ix = eval(tmp->lft);
 224         if (ix >= tl->nel || ix < 0)
 225                 fatal("indexing error \'%s\'", tl->name);
 226
 227         if (tl->nbits > 0)
 228                 a = (a & ((1<<tl->nbits)-1));
 229
 230         if (a != tl->val[ix])
 231         {       tl->val[ix] = a;
 232                 tl->setat = depth;
 233         }
 234         return 1;
 235 }
 236
 237 int
 238 Cnt_flds(Lextok *m)
 239 {       Lextok *fp, *tl, *n;
 240         int cnt = 0;
 241
 242         if (m->ntyp == ',')
 243         {       n = m;
 244                 goto is_lst;
 245         }
 246         if (!m->sym || m->ntyp != STRUCT)
 247                 return 1;
 248
 249         n = getuname(m->sym);
 250 is_lst:
 251         for (fp = n; fp; fp = fp->rgt)
 252         for (tl = fp->lft; tl; tl = tl->rgt)
 253         {       if (tl->sym->type == STRUCT)
 254                 {       if (tl->sym->nel != 1)
 255                                 fatal("array of structures in param list, %s",
 256                                         tl->sym->name);
 257                         cnt += Cnt_flds(tl->sym->Slst);
 258                 }  else
 259                         cnt += tl->sym->nel;
 260         }
 261         return cnt;
 262 }
 263
 264 int
 265 Sym_typ(Lextok *t)
 266 {       Symbol *s = t->sym;
 267
 268         if (!s) return 0;
 269
 270         if (s->type != STRUCT)
 271                 return s->type;
 272
 273         if (!t->rgt
 274         ||   t->rgt->ntyp != '.'        /* gh: had ! in wrong place */
 275         ||  !t->rgt->lft)
 276                 return STRUCT;          /* not a field reference */
 277
 278         return Sym_typ(t->rgt->lft);
 279 }
 280
 281 int
 282 Width_set(int *wdth, int i, Lextok *n)
 283 {       Lextok *fp, *tl;
 284         int j = i, k;
 285
 286         for (fp = n; fp; fp = fp->rgt)
 287         for (tl = fp->lft; tl; tl = tl->rgt)
 288         {       if (tl->sym->type == STRUCT)
 289                         j = Width_set(wdth, j, tl->sym->Slst);
 290                 else
 291                 {       for (k = 0; k < tl->sym->nel; k++, j++)
 292                                 wdth[j] = tl->sym->type;
 293         }       }
 294         return j;
 295 }
 296
 297 void
 298 ini_struct(Symbol *s)
 299 {       int i; Lextok *fp, *tl;
 300
 301         if (s->type != STRUCT)  /* last step */
 302         {       (void) checkvar(s, 0);
 303                 return;
 304         }
 305         if (s->Sval == (Lextok **) 0)
 306         {       s->Sval = (Lextok **) emalloc(s->nel * sizeof(Lextok *));
 307                 for (i = 0; i < s->nel; i++)
 308                 {       s->Sval[i] = cpnn(s->Slst, 1, 1, 1);
 309
 310                         for (fp = s->Sval[i]; fp; fp = fp->rgt)
 311                         for (tl = fp->lft; tl; tl = tl->rgt)
 312                                 ini_struct(tl->sym);
 313         }       }
 314 }
 315
 316 static Lextok *
 317 cpnn(Lextok *s, int L, int R, int S)
 318 {       Lextok *d; extern int Nid;
 319
 320         if (!s) return ZN;
 321
 322         d = (Lextok *) emalloc(sizeof(Lextok));
 323         d->ntyp = s->ntyp;
 324         d->val  = s->val;
 325         d->ln   = s->ln;
 326         d->fn   = s->fn;
 327         d->sym  = s->sym;
 328         if (L) d->lft = cpnn(s->lft, 1, 1, S);
 329         if (R) d->rgt = cpnn(s->rgt, 1, 1, S);
 330
 331         if (S && s->sym)
 332         {       d->sym = (Symbol *) emalloc(sizeof(Symbol));
 333                 memcpy(d->sym, s->sym, sizeof(Symbol));
 334                 if (d->sym->type == CHAN)
 335                         d->sym->Nid = ++Nid;
 336         }
 337         if (s->sq || s->sl)
 338                 fatal("cannot happen cpnn", (char *) 0);
 339
 340         return d;
 341 }
 342
 343 int
 344 full_name(FILE *fd, Lextok *n, Symbol *v, int xinit)
 345 {       Symbol *tl;
 346         Lextok *tmp;
 347         int hiddenarrays = 0;
 348
 349         fprintf(fd, "%s", v->name);
 350
 351         if (!n || !(tl = do_same(n, v, xinit)))
 352                 return 0;
 353         tmp = n->rgt->lft;
 354
 355         if (tmp->sym->type == STRUCT)
 356         {       fprintf(fd, ".");
 357                 hiddenarrays = full_name(fd, tmp, tl, 0);
 358                 goto out;
 359         }
 360         fprintf(fd, ".%s", tl->name);
 361 out:    if (tmp->sym->nel > 1)
 362         {       fprintf(fd, "[%d]", eval(tmp->lft));
 363                 hiddenarrays = 1;
 364         }
 365         return hiddenarrays;
 366 }
 367
 368 void
 369 validref(Lextok *p, Lextok *c)
 370 {       Lextok *fp, *tl;
 371         char lbuf[512];
 372
 373         for (fp = p->sym->Slst; fp; fp = fp->rgt)
 374         for (tl = fp->lft; tl; tl = tl->rgt)
 375                 if (strcmp(tl->sym->name, c->sym->name) == 0)
 376                         return;
 377
 378         sprintf(lbuf, "no field '%s' defined in structure '%s'\n",
 379                 c->sym->name, p->sym->name);
 380         non_fatal(lbuf, (char *) 0);
 381 }
 382
 383 void
 384 struct_name(Lextok *n, Symbol *v, int xinit, char *buf)
 385 {       Symbol *tl;
 386         Lextok *tmp;
 387         char lbuf[512];
 388
 389         if (!n || !(tl = do_same(n, v, xinit)))
 390                 return;
 391         tmp = n->rgt->lft;
 392         if (tmp->sym->type == STRUCT)
 393         {       strcat(buf, ".");
 394                 struct_name(tmp, tl, 0, buf);
 395                 return;
 396         }
 397         sprintf(lbuf, ".%s", tl->name);
 398         strcat(buf, lbuf);
 399         if (tmp->sym->nel > 1)
 400         {       sprintf(lbuf, "[%d]", eval(tmp->lft));
 401                 strcat(buf, lbuf);
 402         }
 403 }
 404
 405 void
 406 walk2_struct(char *s, Symbol *z)
 407 {       Lextok *fp, *tl;
 408         char eprefix[128];
 409         int ix;
 410         extern void Done_case(char *, Symbol *);
 411
 412         ini_struct(z);
 413         if (z->nel == 1)
 414                 sprintf(eprefix, "%s%s.", s, z->name);
 415         for (ix = 0; ix < z->nel; ix++)
 416         {       if (z->nel > 1)
 417                         sprintf(eprefix, "%s%s[%d].", s, z->name, ix);
 418                 for (fp = z->Sval[ix]; fp; fp = fp->rgt)
 419                 for (tl = fp->lft; tl; tl = tl->rgt)
 420                 {       if (tl->sym->type == STRUCT)
 421                                 walk2_struct(eprefix, tl->sym);
 422                         else if (tl->sym->type == CHAN)
 423                                 Done_case(eprefix, tl->sym);
 424         }       }
 425 }
 426
 427 void
 428 walk_struct(FILE *ofd, int dowhat, char *s, Symbol *z, char *a, char *b, char *c)
 429 {       Lextok *fp, *tl;
 430         char eprefix[128];
 431         int ix;
 432
 433         ini_struct(z);
 434         if (z->nel == 1)
 435                 sprintf(eprefix, "%s%s.", s, z->name);
 436         for (ix = 0; ix < z->nel; ix++)
 437         {       if (z->nel > 1)
 438                         sprintf(eprefix, "%s%s[%d].", s, z->name, ix);
 439                 for (fp = z->Sval[ix]; fp; fp = fp->rgt)
 440                 for (tl = fp->lft; tl; tl = tl->rgt)
 441                 {       if (tl->sym->type == STRUCT)
 442                          walk_struct(ofd, dowhat, eprefix, tl->sym, a,b,c);
 443                         else
 444                          do_var(ofd, dowhat, eprefix, tl->sym, a,b,c);
 445         }       }
 446 }
 447
 448 void
 449 c_struct(FILE *fd, char *ipref, Symbol *z)
 450 {       Lextok *fp, *tl;
 451         char pref[256], eprefix[300];
 452         int ix;
 453
 454         ini_struct(z);
 455
 456         for (ix = 0; ix < z->nel; ix++)
 457         for (fp = z->Sval[ix]; fp; fp = fp->rgt)
 458         for (tl = fp->lft; tl; tl = tl->rgt)
 459         {       strcpy(eprefix, ipref);
 460                 if (z->nel > 1)
 461                 {       /* insert index before last '.' */
 462                         eprefix[strlen(eprefix)-1] = '\0';
 463                         sprintf(pref, "[ %d ].", ix);
 464                         strcat(eprefix, pref);
 465                 }
 466                 if (tl->sym->type == STRUCT)
 467                 {       strcat(eprefix, tl->sym->name);
 468                         strcat(eprefix, ".");
 469                         c_struct(fd, eprefix, tl->sym);
 470                 } else
 471                         c_var(fd, eprefix, tl->sym);
 472         }
 473 }
 474
 475 void
 476 dump_struct(Symbol *z, char *prefix, RunList *r)
 477 {       Lextok *fp, *tl;
 478         char eprefix[256];
 479         int ix, jx;
 480
 481         ini_struct(z);
 482
 483         for (ix = 0; ix < z->nel; ix++)
 484         {       if (z->nel > 1)
 485                         sprintf(eprefix, "%s[%d]", prefix, ix);
 486                 else
 487                         strcpy(eprefix, prefix);
 488
 489                 for (fp = z->Sval[ix]; fp; fp = fp->rgt)
 490                 for (tl = fp->lft; tl; tl = tl->rgt)
 491                 {       if (tl->sym->type == STRUCT)
 492                         {       char pref[300];
 493                                 strcpy(pref, eprefix);
 494                                 strcat(pref, ".");
 495                                 strcat(pref, tl->sym->name);
 496                                 dump_struct(tl->sym, pref, r);
 497                         } else
 498                         for (jx = 0; jx < tl->sym->nel; jx++)
 499                         {       if (tl->sym->type == CHAN)
 500                                         doq(tl->sym, jx, r);
 501                                 else
 502                                 {       printf("\t\t");
 503                                         if (r)
 504                                         printf("%s(%d):", r->n->name, r->pid);
 505                                         printf("%s.%s", eprefix, tl->sym->name);
 506                                         if (tl->sym->nel > 1)
 507                                                 printf("[%d]", jx);
 508                                         printf(" = ");
 509                                         sr_mesg(stdout, tl->sym->val[jx],
 510                                                 tl->sym->type == MTYPE);
 511                                         printf("\n");
 512                 }       }       }
 513         }
 514 }
 515
 516 static int
 517 retrieve(Lextok **targ, int i, int want, Lextok *n, int Ntyp)
 518 {       Lextok *fp, *tl;
 519         int j = i, k;
 520
 521         for (fp = n; fp; fp = fp->rgt)
 522         for (tl = fp->lft; tl; tl = tl->rgt)
 523         {       if (tl->sym->type == STRUCT)
 524                 {       j = retrieve(targ, j, want, tl->sym->Slst, Ntyp);
 525                         if (j < 0)
 526                         {       Lextok *x = cpnn(tl, 1, 0, 0);
 527                                 x->rgt = nn(ZN, '.', (*targ), ZN);
 528                                 (*targ) = x;
 529                                 return -1;
 530                         }
 531                 } else
 532                 {       for (k = 0; k < tl->sym->nel; k++, j++)
 533                         {       if (j == want)
 534                                 {       *targ = cpnn(tl, 1, 0, 0);
 535                                         (*targ)->lft = nn(ZN, CONST, ZN, ZN);
 536                                         (*targ)->lft->val = k;
 537                                         if (Ntyp)
 538                                         (*targ)->ntyp = (short) Ntyp;
 539                                         return -1;
 540                                 }
 541         }       }       }
 542         return j;
 543 }
 544
 545 static int
 546 is_explicit(Lextok *n)
 547 {
 548         if (!n) return 0;
 549         if (!n->sym) fatal("unexpected - no symbol", 0);
 550         if (n->sym->type != STRUCT) return 1;
 551         if (!n->rgt) return 0;
 552         if (n->rgt->ntyp != '.')
 553         {       lineno = n->ln;
 554                 Fname  = n->fn;
 555                 printf("ntyp %d\n", n->rgt->ntyp);
 556                 fatal("unexpected %s, no '.'", n->sym->name);
 557         }
 558         return is_explicit(n->rgt->lft);
 559 }
 560
 561 Lextok *
 562 expand(Lextok *n, int Ok)
 563         /* turn rgt-lnked list of struct nms, into ',' list of flds */
 564 {       Lextok *x = ZN, *y;
 565
 566         if (!Ok) return n;
 567
 568         while (n)
 569         {       y = mk_explicit(n, 1, 0);
 570                 if (x)
 571                         (void) tail_add(x, y);
 572                 else
 573                         x = y;
 574
 575                 n = n->rgt;
 576         }
 577         return x;
 578 }
 579
 580 Lextok *
 581 mk_explicit(Lextok *n, int Ok, int Ntyp)
 582         /* produce a single ',' list of fields */
 583 {       Lextok *bld = ZN, *x;
 584         int i, cnt; extern int IArgs;
 585
 586         if (n->sym->type != STRUCT
 587         ||  is_explicit(n))
 588                 return n;
 589
 590         if (n->rgt
 591         &&  n->rgt->ntyp == '.'
 592         &&  n->rgt->lft
 593         &&  n->rgt->lft->sym
 594         &&  n->rgt->lft->sym->type == STRUCT)
 595         {       Lextok *y;
 596                 bld = mk_explicit(n->rgt->lft, Ok, Ntyp);
 597                 for (x = bld; x; x = x->rgt)
 598                 {       y = cpnn(n, 1, 0, 0);
 599                         y->rgt = nn(ZN, '.', x->lft, ZN);
 600                         x->lft = y;
 601                 }
 602
 603                 return bld;
 604         }
 605
 606         if (!Ok || !n->sym->Slst)
 607         {       if (IArgs) return n;
 608                 printf("spin: saw '");
 609                 comment(stdout, n, 0);
 610                 printf("'\n");
 611                 fatal("incomplete structure ref '%s'", n->sym->name);
 612         }
 613
 614         cnt = Cnt_flds(n->sym->Slst);
 615         for (i = cnt-1; i >= 0; i--)
 616         {       bld = nn(ZN, ',', ZN, bld);
 617                 if (retrieve(&(bld->lft), 0, i, n->sym->Slst, Ntyp) >= 0)
 618                 {       printf("cannot retrieve field %d\n", i);
 619                         fatal("bad structure %s", n->sym->name);
 620                 }
 621                 x = cpnn(n, 1, 0, 0);
 622                 x->rgt = nn(ZN, '.', bld->lft, ZN);
 623                 bld->lft = x;
 624         }
 625         return bld;
 626 }
 627
 628 Lextok *
 629 tail_add(Lextok *a, Lextok *b)
 630 {       Lextok *t;
 631
 632         for (t = a; t->rgt; t = t->rgt)
 633                 if (t->ntyp != ',')
 634                 fatal("unexpected type - tail_add", 0);
 635         t->rgt = b;
 636         return a;
 637 }
 638
 639 void
 640 setpname(Lextok *n)
 641 {       UType *tmp;
 642
 643         for (tmp = Pnames; tmp; tmp = tmp->nxt)
 644                 if (!strcmp(n->sym->name, tmp->nm->name))
 645                 {       non_fatal("proctype %s redefined",
 646                                 n->sym->name);
 647                         return;
 648                 }
 649         tmp = (UType *) emalloc(sizeof(UType));
 650         tmp->nm = n->sym;
 651         tmp->nxt = Pnames;
 652         Pnames = tmp;
 653 }
 654
 655 int
 656 isproctype(char *t)
 657 {       UType *tmp;
 658
 659         for (tmp = Pnames; tmp; tmp = tmp->nxt)
 660         {       if (!strcmp(t, tmp->nm->name))
 661                         return 1;
 662         }
 663         return 0;
 664 }