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

   1 /***** spin: sym.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 extern Symbol   *Fname, *owner;
  16 extern int      lineno, depth, verbose, NamesNotAdded, deadvar, has_hidden;
  17 extern short    has_xu;
  18
  19 Symbol  *context = ZS;
  20 Ordered *all_names = (Ordered *)0;
  21 int     Nid = 0;
  22
  23 Lextok *Mtype = (Lextok *) 0;
  24
  25 static Ordered  *last_name = (Ordered *)0;
  26 static Symbol   *symtab[Nhash+1];
  27 static Lextok *runstmnts = ZN;
  28
  29 static int
  30 samename(Symbol *a, Symbol *b)
  31 {
  32         if (!a && !b) return 1;
  33         if (!a || !b) return 0;
  34         return !strcmp(a->name, b->name);
  35 }
  36
  37 int
  38 hash(char *s)
  39 {       int h=0;
  40
  41         while (*s)
  42         {       h += *s++;
  43                 h <<= 1;
  44                 if (h&(Nhash+1))
  45                         h |= 1;
  46         }
  47         return h&Nhash;
  48 }
  49
  50 Symbol *
  51 lookup(char *s)
  52 {       Symbol *sp; Ordered *no;
  53         int h = hash(s);
  54
  55         for (sp = symtab[h]; sp; sp = sp->next)
  56                 if (strcmp(sp->name, s) == 0
  57                 &&  samename(sp->context, context)
  58                 &&  samename(sp->owner, owner))
  59                         return sp;              /* found */
  60
  61         if (context)                            /* in proctype */
  62         for (sp = symtab[h]; sp; sp = sp->next)
  63                 if (strcmp(sp->name, s) == 0
  64                 && !sp->context
  65                 &&  samename(sp->owner, owner))
  66                         return sp;              /* global */
  67
  68         sp = (Symbol *) emalloc(sizeof(Symbol));
  69         sp->name = (char *) emalloc(strlen(s) + 1);
  70         strcpy(sp->name, s);
  71         sp->nel = 1;
  72         sp->setat = depth;
  73         sp->context = context;
  74         sp->owner = owner;                      /* if fld in struct */
  75
  76         if (NamesNotAdded == 0)
  77         {       sp->next = symtab[h];
  78                 symtab[h] = sp;
  79                 no = (Ordered *) emalloc(sizeof(Ordered));
  80                 no->entry = sp;
  81                 if (!last_name)
  82                         last_name = all_names = no;
  83                 else
  84                 {       last_name->next = no;
  85                         last_name = no;
  86         }       }
  87
  88         return sp;
  89 }
  90
  91 void
  92 trackvar(Lextok *n, Lextok *m)
  93 {       Symbol *sp = n->sym;
  94
  95         if (!sp) return;        /* a structure list */
  96         switch (m->ntyp) {
  97         case NAME:
  98                 if (m->sym->type != BIT)
  99                 {       sp->hidden |= 4;
 100                         if (m->sym->type != BYTE)
 101                                 sp->hidden |= 8;
 102                 }
 103                 break;
 104         case CONST:
 105                 if (m->val != 0 && m->val != 1)
 106                         sp->hidden |= 4;
 107                 if (m->val < 0 || m->val > 256)
 108                         sp->hidden |= 8; /* ditto byte-equiv */
 109                 break;
 110         default:        /* unknown */
 111                 sp->hidden |= (4|8); /* not known bit-equiv */
 112         }
 113 }
 114
 115 void
 116 trackrun(Lextok *n)
 117 {
 118         runstmnts = nn(ZN, 0, n, runstmnts);
 119 }
 120
 121 void
 122 checkrun(Symbol *parnm, int posno)
 123 {       Lextok *n, *now, *v; int i, m;
 124         int res = 0; char buf[16], buf2[16];
 125
 126         for (n = runstmnts; n; n = n->rgt)
 127         {       now = n->lft;
 128                 if (now->sym != parnm->context)
 129                         continue;
 130                 for (v = now->lft, i = 0; v; v = v->rgt, i++)
 131                         if (i == posno)
 132                         {       m = v->lft->ntyp;
 133                                 if (m == CONST)
 134                                 {       m = v->lft->val;
 135                                         if (m != 0 && m != 1)
 136                                                 res |= 4;
 137                                         if (m < 0 || m > 256)
 138                                                 res |= 8;
 139                                 } else if (m == NAME)
 140                                 {       m = v->lft->sym->type;
 141                                         if (m != BIT)
 142                                         {       res |= 4;
 143                                                 if (m != BYTE)
 144                                                         res |= 8;
 145                                         }
 146                                 } else
 147                                         res |= (4|8); /* unknown */
 148                                 break;
 149         }               }
 150         if (!(res&4) || !(res&8))
 151         {       if (!(verbose&32)) return;
 152                 strcpy(buf2, (!(res&4))?"bit":"byte");
 153                 sputtype(buf, parnm->type);
 154                 i = (int) strlen(buf);
 155                 while (i > 0 && buf[--i] == ' ') buf[i] = '\0';
 156                 if (i == 0 || strcmp(buf, buf2) == 0) return;
 157                 prehint(parnm);
 158                 printf("proctype %s, '%s %s' could be declared",
 159                         parnm->context?parnm->context->name:"", buf, parnm->name);
 160                 printf(" '%s %s'\n", buf2, parnm->name);
 161         }
 162 }
 163
 164 void
 165 trackchanuse(Lextok *m, Lextok *w, int t)
 166 {       Lextok *n = m; int cnt = 1;
 167         while (n)
 168         {       if (n->lft
 169                 &&  n->lft->sym
 170                 &&  n->lft->sym->type == CHAN)
 171                         setaccess(n->lft->sym, w?w->sym:ZS, cnt, t);
 172                 n = n->rgt; cnt++;
 173         }
 174 }
 175
 176 void
 177 setptype(Lextok *n, int t, Lextok *vis) /* predefined types */
 178 {       int oln = lineno, cnt = 1; extern int Expand_Ok;
 179
 180         while (n)
 181         {       if (n->sym->type && !(n->sym->hidden&32))
 182                 { lineno = n->ln; Fname = n->fn;
 183                   non_fatal("redeclaration of '%s'", n->sym->name);
 184                   lineno = oln;
 185                 }
 186                 n->sym->type = (short) t;
 187
 188                 if (Expand_Ok)
 189                 {       n->sym->hidden |= (4|8|16); /* formal par */
 190                         if (t == CHAN)
 191                         setaccess(n->sym, ZS, cnt, 'F');
 192                 }
 193                 if (t == UNSIGNED)
 194                 {       if (n->sym->nbits < 0 || n->sym->nbits >= 32)
 195                         fatal("(%s) has invalid width-field", n->sym->name);
 196                         if (n->sym->nbits == 0)
 197                         {       n->sym->nbits = 16;
 198                                 non_fatal("unsigned without width-field", 0);
 199                         }
 200                 } else if (n->sym->nbits > 0)
 201                 {       non_fatal("(%s) only an unsigned can have width-field",
 202                                 n->sym->name);
 203                 }
 204                 if (vis)
 205                 {       if (strncmp(vis->sym->name, ":hide:", (size_t) 6) == 0)
 206                         {       n->sym->hidden |= 1;
 207                                 has_hidden++;
 208                                 if (t == BIT)
 209                                 fatal("bit variable (%s) cannot be hidden",
 210                                         n->sym->name);
 211                         } else if (strncmp(vis->sym->name, ":show:", (size_t) 6) == 0)
 212                         {       n->sym->hidden |= 2;
 213                         } else if (strncmp(vis->sym->name, ":local:", (size_t) 7) == 0)
 214                         {       n->sym->hidden |= 64;
 215                         }
 216                 }
 217                 if (t == CHAN)
 218                         n->sym->Nid = ++Nid;
 219                 else
 220                 {       n->sym->Nid = 0;
 221                         if (n->sym->ini
 222                         &&  n->sym->ini->ntyp == CHAN)
 223                         {       Fname = n->fn;
 224                                 lineno = n->ln;
 225                                 fatal("chan initializer for non-channel %s",
 226                                 n->sym->name);
 227                         }
 228                 }
 229                 if (n->sym->nel <= 0)
 230                 { lineno = n->ln; Fname = n->fn;
 231                   non_fatal("bad array size for '%s'", n->sym->name);
 232                   lineno = oln;
 233                 }
 234                 n = n->rgt; cnt++;
 235         }
 236 }
 237
 238 static void
 239 setonexu(Symbol *sp, int t)
 240 {
 241         sp->xu |= t;
 242         if (t == XR || t == XS)
 243         {       if (sp->xup[t-1]
 244                 &&  strcmp(sp->xup[t-1]->name, context->name))
 245                 {       printf("error: x[rs] claims from %s and %s\n",
 246                                 sp->xup[t-1]->name, context->name);
 247                         non_fatal("conflicting claims on chan '%s'",
 248                                 sp->name);
 249                 }
 250                 sp->xup[t-1] = context;
 251         }
 252 }
 253
 254 static void
 255 setallxu(Lextok *n, int t)
 256 {       Lextok *fp, *tl;
 257
 258         for (fp = n; fp; fp = fp->rgt)
 259         for (tl = fp->lft; tl; tl = tl->rgt)
 260         {       if (tl->sym->type == STRUCT)
 261                         setallxu(tl->sym->Slst, t);
 262                 else if (tl->sym->type == CHAN)
 263                         setonexu(tl->sym, t);
 264         }
 265 }
 266
 267 Lextok *Xu_List = (Lextok *) 0;
 268
 269 void
 270 setxus(Lextok *p, int t)
 271 {       Lextok *m, *n;
 272
 273         has_xu = 1;
 274         if (!context)
 275         {       lineno = p->ln;
 276                 Fname = p->fn;
 277                 fatal("non-local x[rs] assertion", (char *)0);
 278         }
 279         for (m = p; m; m = m->rgt)
 280         {       Lextok *Xu_new = (Lextok *) emalloc(sizeof(Lextok));
 281                 Xu_new->val = t;
 282                 Xu_new->lft = m->lft;
 283                 Xu_new->sym = context;
 284                 Xu_new->rgt = Xu_List;
 285                 Xu_List = Xu_new;
 286
 287                 n = m->lft;
 288                 if (n->sym->type == STRUCT)
 289                         setallxu(n->sym->Slst, t);
 290                 else if (n->sym->type == CHAN)
 291                         setonexu(n->sym, t);
 292                 else
 293                 {       int oln = lineno;
 294                         lineno = n->ln; Fname = n->fn;
 295                         non_fatal("xr or xs of non-chan '%s'",
 296                                 n->sym->name);
 297                         lineno = oln;
 298                 }
 299         }
 300 }
 301
 302 void
 303 setmtype(Lextok *m)
 304 {       Lextok *n;
 305         int cnt, oln = lineno;
 306
 307         if (m) { lineno = m->ln; Fname = m->fn; }
 308
 309         if (!Mtype)
 310                 Mtype = m;
 311         else
 312         {       for (n = Mtype; n->rgt; n = n->rgt)
 313                         ;
 314                 n->rgt = m;     /* concatenate */
 315         }
 316
 317         for (n = Mtype, cnt = 1; n; n = n->rgt, cnt++)  /* syntax check */
 318         {       if (!n->lft || !n->lft->sym
 319                 ||   n->lft->ntyp != NAME
 320                 ||   n->lft->lft)       /* indexed variable */
 321                         fatal("bad mtype definition", (char *)0);
 322
 323                 /* label the name */
 324                 if (n->lft->sym->type != MTYPE)
 325                 {       n->lft->sym->hidden |= 128;     /* is used */
 326                         n->lft->sym->type = MTYPE;
 327                         n->lft->sym->ini = nn(ZN,CONST,ZN,ZN);
 328                         n->lft->sym->ini->val = cnt;
 329                 } else if (n->lft->sym->ini->val != cnt)
 330                         non_fatal("name %s appears twice in mtype declaration",
 331                                 n->lft->sym->name);
 332         }
 333         lineno = oln;
 334         if (cnt > 256)
 335         fatal("too many mtype elements (>255)", (char *)0);
 336 }
 337
 338 int
 339 ismtype(char *str)      /* name to number */
 340 {       Lextok *n;
 341         int cnt = 1;
 342
 343         for (n = Mtype; n; n = n->rgt)
 344         {       if (strcmp(str, n->lft->sym->name) == 0)
 345                         return cnt;
 346                 cnt++;
 347         }
 348         return 0;
 349 }
 350
 351 int
 352 sputtype(char *foo, int m)
 353 {
 354         switch (m) {
 355         case UNSIGNED:  strcpy(foo, "unsigned "); break;
 356         case BIT:       strcpy(foo, "bit   "); break;
 357         case BYTE:      strcpy(foo, "byte  "); break;
 358         case CHAN:      strcpy(foo, "chan  "); break;
 359         case SHORT:     strcpy(foo, "short "); break;
 360         case INT:       strcpy(foo, "int   "); break;
 361         case MTYPE:     strcpy(foo, "mtype "); break;
 362         case STRUCT:    strcpy(foo, "struct"); break;
 363         case PROCTYPE:  strcpy(foo, "proctype"); break;
 364         case LABEL:     strcpy(foo, "label "); return 0;
 365         default:        strcpy(foo, "value "); return 0;
 366         }
 367         return 1;
 368 }
 369
 370
 371 static int
 372 puttype(int m)
 373 {       char buf[128];
 374
 375         if (sputtype(buf, m))
 376         {       printf("%s", buf);
 377                 return 1;
 378         }
 379         return 0;
 380 }
 381
 382 void
 383 symvar(Symbol *sp)
 384 {       Lextok *m;
 385
 386         if (!puttype(sp->type))
 387                 return;
 388
 389         printf("\t");
 390         if (sp->owner) printf("%s.", sp->owner->name);
 391         printf("%s", sp->name);
 392         if (sp->nel > 1) printf("[%d]", sp->nel);
 393
 394         if (sp->type == CHAN)
 395                 printf("\t%d", (sp->ini)?sp->ini->val:0);
 396         else if (sp->type == STRUCT) /* Frank Weil, 2.9.8 */
 397                 printf("\t%s", sp->Snm->name);
 398         else
 399                 printf("\t%d", eval(sp->ini));
 400
 401         if (sp->owner)
 402                 printf("\t<:struct-field:>");
 403         else
 404         if (!sp->context)
 405                 printf("\t<:global:>");
 406         else
 407                 printf("\t<%s>", sp->context->name);
 408
 409         if (sp->Nid < 0)        /* formal parameter */
 410                 printf("\t<parameter %d>", -(sp->Nid));
 411         else
 412                 printf("\t<variable>");
 413         if (sp->type == CHAN && sp->ini)
 414         {       int i;
 415                 for (m = sp->ini->rgt, i = 0; m; m = m->rgt)
 416                         i++;
 417                 printf("\t%d\t", i);
 418                 for (m = sp->ini->rgt; m; m = m->rgt)
 419                 {       if (m->ntyp == STRUCT)
 420                                 printf("struct %s", m->sym->name);
 421                         else
 422                                 (void) puttype(m->ntyp);
 423                         if (m->rgt) printf("\t");
 424                 }
 425         }
 426         printf("\n");
 427 }
 428
 429 void
 430 symdump(void)
 431 {       Ordered *walk;
 432
 433         for (walk = all_names; walk; walk = walk->next)
 434                 symvar(walk->entry);
 435 }
 436
 437 void
 438 chname(Symbol *sp)
 439 {       printf("chan ");
 440         if (sp->context) printf("%s-", sp->context->name);
 441         if (sp->owner) printf("%s.", sp->owner->name);
 442         printf("%s", sp->name);
 443         if (sp->nel > 1) printf("[%d]", sp->nel);
 444         printf("\t");
 445 }
 446
 447 static struct X {
 448         int typ; char *nm;
 449 } xx[] = {
 450         { 'A', "exported as run parameter" },
 451         { 'F', "imported as proctype parameter" },
 452         { 'L', "used as l-value in asgnmnt" },
 453         { 'V', "used as r-value in asgnmnt" },
 454         { 'P', "polled in receive stmnt" },
 455         { 'R', "used as parameter in receive stmnt" },
 456         { 'S', "used as parameter in send stmnt" },
 457         { 'r', "received from" },
 458         { 's', "sent to" },
 459 };
 460
 461 static void
 462 chan_check(Symbol *sp)
 463 {       Access *a; int i, b=0, d;
 464
 465         if (verbose&1) goto report;     /* -C -g */
 466
 467         for (a = sp->access; a; a = a->lnk)
 468                 if (a->typ == 'r')
 469                         b |= 1;
 470                 else if (a->typ == 's')
 471                         b |= 2;
 472         if (b == 3 || (sp->hidden&16))  /* balanced or formal par */
 473                 return;
 474 report:
 475         chname(sp);
 476         for (i = d = 0; i < (int) (sizeof(xx)/sizeof(struct X)); i++)
 477         {       b = 0;
 478                 for (a = sp->access; a; a = a->lnk)
 479                         if (a->typ == xx[i].typ) b++;
 480                 if (b == 0) continue; d++;
 481                 printf("\n\t%s by: ", xx[i].nm);
 482                 for (a = sp->access; a; a = a->lnk)
 483                   if (a->typ == xx[i].typ)
 484                   {     printf("%s", a->who->name);
 485                         if (a->what) printf(" to %s", a->what->name);
 486                         if (a->cnt)  printf(" par %d", a->cnt);
 487                         if (--b > 0) printf(", ");
 488                   }
 489         }
 490         printf("%s\n", (!d)?"\n\tnever used under this name":"");
 491 }
 492
 493 void
 494 chanaccess(void)
 495 {       Ordered *walk;
 496         char buf[128];
 497         extern int Caccess, separate;
 498         extern short has_code;
 499
 500         for (walk = all_names; walk; walk = walk->next)
 501         {       if (!walk->entry->owner)
 502                 switch (walk->entry->type) {
 503                 case CHAN:
 504                         if (Caccess) chan_check(walk->entry);
 505                         break;
 506                 case MTYPE:
 507                 case BIT:
 508                 case BYTE:
 509                 case SHORT:
 510                 case INT:
 511                 case UNSIGNED:
 512                         if ((walk->entry->hidden&128))  /* was: 32 */
 513                                 continue;
 514
 515                         if (!separate
 516                         &&  !walk->entry->context
 517                         &&  !has_code
 518                         &&   deadvar)
 519                                 walk->entry->hidden |= 1; /* auto-hide */
 520
 521                         if (!(verbose&32) || has_code) continue;
 522
 523                         printf("spin: warning, %s, ", Fname->name);
 524                         sputtype(buf, walk->entry->type);
 525                         if (walk->entry->context)
 526                                 printf("proctype %s",
 527                                         walk->entry->context->name);
 528                         else
 529                                 printf("global");
 530                         printf(", '%s%s' variable is never used\n",
 531                                 buf, walk->entry->name);
 532         }       }
 533 }