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