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