1 /***** spin: pangen1.c *****/ 2 3 /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */ 4 /* 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.att.com */ 12 13 #include "spin.h" 14 #include "y.tab.h" 15 #include "pangen1.h" 16 #include "pangen3.h" 17 18 extern FILE *tc, *th; 19 extern Lextok *Mtype; 20 extern ProcList *rdy; 21 extern Queue *qtab; 22 extern Symbol *symtab[Nhash+1], *Fname; 23 extern char *claimproc; 24 extern int lineno, has_sorted, has_random; 25 extern int nrRdy, nqs, mst, Mpars, claimnr; 26 27 enum { INIV, PUTV }; 28 int Npars=0, u_sync=0, u_async=0; 29 int acceptors=0, progressors=0, nBits=0; 30 Symbol *LstSet=ZS; 31 32 void 33 reverse_names(ProcList *p) 34 { 35 if (!p) return; 36 reverse_names(p->nxt); 37 fprintf(tc, " \"%s\",\n", p->n->name); 38 } 39 40 void 41 genheader(void) 42 { ProcList *p; int i; 43 44 fprintf(th, "#define SYNC %d\n", u_sync); 45 fprintf(th, "#define ASYNC %d\n\n", u_async); 46 47 putunames(th); 48 49 fprintf(tc, "short Air[] = { "); 50 for (p = rdy, i=0; p; p = p->nxt, i++) 51 fprintf(tc, "%s Air%d", (p!=rdy)?",":"", i); 52 fprintf(tc, " };\n"); 53 54 fprintf(tc, "char *procname[] = {\n"); 55 reverse_names(rdy); 56 fprintf(tc, "};\n\n"); 57 for (p = rdy; p; p = p->nxt) 58 put_ptype(p->n->name, p->tn, mst, nrRdy); 59 60 ntimes(th, 0, 1, Header); 61 LstSet = ZS; 62 doglobal(PUTV); 63 fprintf(th, " uchar sv[VECTORSZ];\n"); 64 fprintf(th, "} State;\n\n"); 65 dohidden(); 66 } 67 68 void 69 genaddproc(void) 70 { ProcList *p; 71 int i; 72 73 fprintf(tc, "int\naddproc(int n"); 74 for (i = 0; i < Npars; i++) 75 fprintf(tc, ", int par%d", i); 76 77 ntimes(tc, 0, 1, Addp0); 78 ntimes(tc, 1, nrRdy, R5); 79 ntimes(tc, 0, 1, Addp1); 80 81 for (p = rdy; p; p = p->nxt) 82 put_pinit(p->s->frst, p->n, p->p, p->tn); 83 84 ntimes(tc, i, i+1, R6); 85 } 86 87 void 88 genother(void) 89 { ProcList *p; 90 91 ntimes(tc, 0, 1, Code0); 92 ntimes(tc, 0, nrRdy, R0); 93 ntimes(tc, nrRdy, nrRdy+1, R1); 94 95 for (p = rdy; p; p = p->nxt) 96 end_labs(p->n, p->tn); 97 98 ntimes(tc, 0, nrRdy, R0a); 99 ntimes(tc, 0, 1, R0b); 100 101 ntimes(th, acceptors, acceptors+1, Code1); 102 ntimes(th, progressors, progressors+1, Code3); 103 ntimes(th, nrRdy+1, nrRdy+2, R2); 104 105 doglobal(INIV); 106 ntimes(tc, 1, nqs+1, R3); 107 ntimes(tc, 0, 1, Code2); 108 ntimes(tc, 0, nrRdy, R4); 109 fprintf(tc, "}\n\n"); 110 } 111 112 static struct { 113 char *s, *t; int n, m, p; 114 } ln[] = { 115 "end", "stopstate", 3, 0, 0, 116 "progress", "progstate", 8, 0, 1, 117 "accept", "accpstate", 6, 1, 0, 118 0, 0, 0, 0, 0, 119 }; 120 121 void 122 end_labs(Symbol *s, int i) 123 { extern Label *labtab; 124 Label *l; 125 int j; 126 127 for (l = labtab; l; l = l->nxt) 128 for (j = 0; ln[j].n; j++) 129 if (strncmp(l->s->name, ln[j].s, ln[j].n) == 0 130 && strcmp(l->s->context->name, s->name) == 0) 131 { fprintf(tc, "\t%s[%d][%d] = 1;\n", 132 ln[j].t, i, l->e->seqno); 133 acceptors += ln[j].m; 134 progressors += ln[j].p; 135 } 136 } 137 138 void 139 ntimes(FILE *fd, int n, int m, char *c[]) 140 { 141 int i, j; 142 for (j = 0; c[j]; j++) 143 for (i = n; i < m; i++) 144 { fprintf(fd, c[j], i, i, i, i, i, i); 145 fprintf(fd, "\n"); 146 } 147 } 148 149 int Types[] = { BIT, BYTE, CHAN, SHORT, INT, STRUCT }; 150 151 int 152 dolocal(int dowhat, int p, char *s) 153 { int i, j, k=0; extern int nr_errs; 154 Symbol *sp; 155 char buf[64]; 156 157 for (j = 0; j < 6; j++) 158 for (i = 0; i <= Nhash; i++) 159 for (sp = symtab[i]; sp; sp = sp->next) 160 if (sp->context 161 && !sp->owner 162 && sp->type == Types[j] 163 && strcmp(s, sp->context->name) == 0) 164 { sprintf(buf, "((P%d *)pptr(h))->", p); 165 do_var(dowhat, buf, sp); k++; 166 if (strcmp(s, ":never:") == 0) 167 { printf("error: %s defines local %s\n", s, sp->name); 168 nr_errs++; 169 } } 170 return k; 171 } 172 173 void 174 doglobal(int dowhat) 175 { Symbol *sp; 176 int i, j; 177 178 for (j = 0; j < 6; j++) 179 for (i = 0; i <= Nhash; i++) 180 for (sp = symtab[i]; sp; sp = sp->next) 181 if (!sp->context 182 && !sp->owner 183 && !sp->hidden 184 && sp->type == Types[j]) 185 do_var(dowhat, "now.", sp); 186 } 187 188 void 189 dohidden(void) 190 { Symbol *sp; 191 int i, j; 192 193 for (j = 0; j < 6; j++) 194 for (i = 0; i <= Nhash; i++) 195 for (sp = symtab[i]; sp; sp = sp->next) 196 if (sp->hidden 197 && sp->type == Types[j]) 198 { if (sp->context || sp->owner) 199 fatal("cannot hide non-globals (%s)", sp->name); 200 if (sp->type == CHAN) 201 fatal("cannot hide channels (%s)", sp->name); 202 fprintf(th, "/* hidden variable: */"); 203 typ2c(sp); 204 } 205 } 206 207 void 208 do_var(int dowhat, char *s, Symbol *sp) 209 { int i; 210 211 switch(dowhat) { 212 case PUTV: 213 typ2c(sp); 214 break; 215 case INIV: 216 if (sp->type == STRUCT) 217 { /* struct may contain a chan */ 218 char gather[128]; 219 char pregat[128]; Symbol *z = (Symbol *)0; 220 int nc, ov=0, last; 221 sprintf(pregat, "%s%s", s, sp->name); 222 do { 223 strcpy(gather, pregat); 224 nc = fill_struct(sp, 0, ov, gather, &z); 225 if (z && last != z->Nid) 226 { last = z->Nid; 227 if (nc < 0) 228 do_var(INIV, gather, z); 229 } 230 ov = -nc; 231 } while (nc < 0); 232 break; 233 } 234 if (!sp->ini) 235 break; 236 if (sp->nel == 1) 237 { fprintf(tc, "\t\t%s%s = ", s, sp->name); 238 do_init(sp); 239 } else 240 for (i = 0; i < sp->nel; i++) 241 { fprintf(tc, "\t\t%s%s[%d] = ", s, sp->name, i); 242 do_init(sp); 243 } 244 break; 245 } 246 } 247 248 void 249 do_init(Symbol *sp) 250 { int i; extern Queue *ltab[]; 251 252 if (sp->type == CHAN && ((i = qmake(sp)) > 0)) 253 { if (sp->ini->ntyp == CHAN) 254 fprintf(tc, "addqueue(%d, %d);\n", 255 i, ltab[i-1]->nslots == 0); 256 else 257 fprintf(tc, "%d;\n", i); 258 } else 259 { putstmnt(tc, sp->ini, 0); 260 fprintf(tc, ";\n"); 261 } 262 } 263 264 int 265 blog(int n) /* for small log2 without rounding problems */ 266 { int m=1, r=2; 267 268 while (r < n) { m++; r *= 2; } 269 return 1+m; 270 } 271 272 void 273 put_ptype(char *s, int i, int m0, int m1) 274 { int k; 275 276 fprintf(th, "typedef struct P%d { /* %s */\n", i, s); 277 fprintf(th, " unsigned _pid : 8; /* 0..255 */\n"); 278 fprintf(th, " unsigned _t : %d; /* proctype */\n", blog(m1)); 279 fprintf(th, " unsigned _p : %d; /* state */\n", blog(m0)); 280 LstSet = ZS; 281 nBits = 8 + blog(m1) + blog(m0); 282 k = dolocal(PUTV, i, s); /* includes pars */ 283 fprintf(th, "} P%d;\n", i); 284 if (!LstSet && k > 0) 285 fprintf(th, "#define Air%d 0\n", i); 286 else 287 { fprintf(th, "#define Air%d (sizeof(P%d) - ", i, i); 288 if (k == 0) 289 { fprintf(th, "%d", (nBits+7)/8); 290 goto done; 291 } 292 if (LstSet->type != BIT || LstSet->nel != 1) 293 { fprintf(th, "Offsetof(P%d, %s%s) - %d*sizeof(", 294 i, 295 LstSet->name, 296 (LstSet->nel > 1)?"[0]":"", 297 LstSet->nel); 298 } 299 switch(LstSet->type) { 300 case BIT: 301 if (LstSet->type == 1) 302 { fprintf(th, "%d", (nBits+7)/8); 303 break; 304 } /* else fall through */ 305 case BYTE: case CHAN: 306 fprintf(th, "uchar)"); break; 307 case SHORT: 308 fprintf(th, "short)"); break; 309 case INT: 310 fprintf(th, "int)"); break; 311 default: 312 fatal("cannot happen Air %s", 313 LstSet->name); 314 } 315 done: fprintf(th, ")\n"); 316 } 317 } 318 319 void 320 put_pinit(Element *e, Symbol *s, Lextok *p, int i) 321 { Lextok *fp, *fpt, *t; 322 int ini, j; 323 324 ini = huntele(e, e->status)->seqno; 325 fprintf(th, "#define start%d %d\n", i, ini); 326 if (i == claimnr) 327 fprintf(th, "#define start_claim %d\n", ini); 328 329 fprintf(tc, "\tcase %d: /* %s */\n", i, s->name); 330 fprintf(tc, "\t\t((P%d *)pptr(h))->_t = %d;\n", i, i); 331 fprintf(tc, "\t\t((P%d *)pptr(h))->_p = %d;", i, ini); 332 fprintf(tc, " reached%d[%d]=1;\n", i, ini); 333 334 (void) dolocal(INIV, i, s->name); 335 336 for (fp = p, j=0; fp; fp = fp->rgt) 337 for (fpt = fp->lft; fpt; fpt = fpt->rgt, j++) 338 { t = (fpt->ntyp == ',') ? fpt->lft : fpt; 339 if (t->sym->nel != 1) 340 { lineno = t->ln; 341 Fname = t->fn; 342 fatal("array in parameter list, %s", 343 t->sym->name); 344 } 345 fprintf(tc, "\t\t((P%d *)pptr(h))->", i); 346 if (t->sym->type == STRUCT) 347 full_name(tc, t, t->sym, 1); 348 else 349 fprintf(tc, "%s", t->sym->name); 350 fprintf(tc, " = par%d;\n", j); 351 } 352 dumpclaims(tc, i, s->name); 353 fprintf(tc, "\t break;\n"); 354 } 355 356 Element * 357 huntstart(Element *f) 358 { Element *e = f; 359 360 if (e->n) 361 { if (e->n->ntyp == '.' && e->nxt) 362 e = e->nxt; 363 else if (e->n->ntyp == ATOMIC 364 || e->n->ntyp == D_STEP 365 || e->n->ntyp == NON_ATOMIC) 366 e->n->sl->this->last->nxt = e->nxt; 367 else if (e->n->ntyp == UNLESS) 368 return e->sub->this->frst; 369 } 370 return e; 371 } 372 373 Element * 374 huntele(Element *f, int o) 375 { Element *g, *e = f; 376 int cnt; /* a precaution against loops */ 377 378 if (e) 379 for (cnt=0; cnt < 10 && e->n; cnt++) 380 { switch (e->n->ntyp) { 381 case GOTO: 382 g = get_lab(e->n,1); 383 cross_dsteps(e->n, g->n); 384 break; 385 case '.': 386 case BREAK: 387 if (!e->nxt) 388 return e; 389 g = e->nxt; 390 break; 391 case UNLESS: 392 g = huntele(e->sub->this->frst, o); 393 break; 394 case D_STEP: 395 case ATOMIC: 396 case NON_ATOMIC: 397 e->n->sl->this->last->nxt = e->nxt; 398 default: /* fall through */ 399 return e; 400 } 401 if ((o & ATOM) && !(g->status & ATOM)) 402 return e; 403 e = g; 404 } 405 return e; 406 } 407 408 void 409 typ2c(Symbol *sp) 410 { 411 switch (sp->type) { 412 case BIT: 413 if (sp->nel == 1) 414 { fprintf(th, "\tunsigned %s : 1", sp->name); 415 LstSet = sp; 416 nBits++; 417 break; 418 } /* else fall through */ 419 nBits += 8*sp->nel; 420 case BYTE: 421 case CHAN: /* good for up to 255 channels */ 422 fprintf(th, "\tuchar %s", sp->name); 423 LstSet = sp; 424 break; 425 case SHORT: 426 fprintf(th, "\tshort %s", sp->name); 427 LstSet = sp; 428 break; 429 case INT: 430 fprintf(th, "\tint %s", sp->name); 431 LstSet = sp; 432 break; 433 case STRUCT: 434 fprintf(th, "\tstruct %s %s", 435 sp->Snm->name, 436 sp->name); 437 LstSet = ZS; 438 break; 439 case PREDEF: 440 return; 441 default: 442 fatal("variable %s undeclared", sp->name); 443 } 444 445 if (sp->nel != 1) 446 fprintf(th, "[%d]", sp->nel); 447 fprintf(th, ";\n"); 448 } 449 450 void 451 ncases(FILE *fd, int p, int n, int m, char *c[]) 452 { int i, j; 453 454 for (j = 0; c[j]; j++) 455 for (i = n; i < m; i++) 456 { fprintf(fd, c[j], i, p, i); 457 fprintf(fd, "\n"); 458 } 459 } 460 461 void 462 genaddqueue(void) 463 { char *buf0; 464 int j; 465 Queue *q; 466 467 buf0 = (char *) emalloc(32); 468 ntimes(tc, 0, 1, Addq0); 469 fprintf(th, "short q_flds[%d];\n", nqs+1); 470 for (q = qtab; q; q = q->nxt) 471 { j = q->qid; 472 fprintf(tc, "\tcase %d: j = sizeof(Q%d);", j, j); 473 fprintf(tc, " q_flds[%d] = %d;", j, q->nflds); 474 fprintf(tc, " break;\n"); 475 476 ntimes(th, j, j+1, R9); 477 for (j = 0; j < q->nflds; j++) 478 { switch (q->fld_width[j]) { 479 case BIT: 480 if (q->nflds != 1) 481 { fprintf(th, "\t\tunsigned"); 482 fprintf(th, " fld%d : 1;\n", j); 483 break; 484 } /* else fall through: gives smaller struct */ 485 case MTYPE: 486 case CHAN: 487 case BYTE: 488 fprintf(th, "\t\tuchar fld%d;\n", j); 489 break; 490 case SHORT: 491 fprintf(th, "\t\tshort fld%d;\n", j); 492 break; 493 case INT: 494 fprintf(th, "\t\tint fld%d;\n", j); 495 break; 496 default: 497 fatal("bad channel spec", ""); 498 } 499 } 500 fprintf(th, " } contents[%d];\n", max(1, q->nslots)); 501 fprintf(th, "} Q%d;\n", q->qid); 502 } 503 ntimes(th, 0, 1, R10); 504 ntimes(tc, 0, 1, Addq1); 505 506 if (has_random) 507 { fprintf(tc, "int\nQ_has(int into"); 508 for (j = 0; j < Mpars; j++) 509 fprintf(tc, ", int want%d, int fld%d", j, j); 510 fprintf(tc, ")\n"); 511 fprintf(tc, "{ int i;\n\n"); 512 fprintf(tc, " if (!into--)\n"); 513 fprintf(tc, " uerror(\"ref to unknown chan (recv-poll)\");\n\n"); 514 fprintf(tc, " if (into >= now._nr_qs || into < 0)\n"); 515 fprintf(tc, " Uerror(\"qrecv bad queue#\");\n\n"); 516 fprintf(tc, " for (i = 0; i < ((Q0 *)qptr(into))->Qlen; i++)\n"); 517 fprintf(tc, " {\n"); 518 for (j = 0; j < Mpars; j++) 519 { fprintf(tc, " if (want%d && ", j); 520 fprintf(tc, "qrecv(into+1, i, %d, 0) != fld%d)\n", j, j); 521 fprintf(tc, " continue;\n"); 522 } 523 fprintf(tc, " return i+1;\n"); 524 fprintf(tc, " }\n"); 525 fprintf(tc, " return 0;\n"); 526 fprintf(tc, "}\n"); 527 } 528 529 fprintf(tc, "void\nqsend(int into, int sorted"); 530 for (j = 0; j < Mpars; j++) 531 fprintf(tc, ", int fld%d", j); 532 fprintf(tc, ")\n"); 533 ntimes(tc, 0, 1, Addq11); 534 535 for (q = qtab; q; q = q->nxt) 536 { sprintf(buf0, "((Q%d *)z)->", q->qid); 537 fprintf(tc, "\tcase %d:%s\n", q->qid, (q->nslots)?"":" /* =rv= */"); 538 if (q->nslots == 0) /* reset handshake point */ 539 fprintf(tc, "\t\t(trpt+2)->o_m = 0;\n"); 540 541 if (has_sorted) 542 { fprintf(tc, "\t\tif (!sorted) goto append%d;\n", q->qid); 543 fprintf(tc, "\t\tfor (j = 0; j < %sQlen; j++)\n", buf0); 544 fprintf(tc, "\t\t{\t/* find insertion point */\n"); 545 sprintf(buf0, "((Q%d *)z)->contents[j].fld", q->qid); 546 for (j = 0; j < q->nflds; j++) 547 { fprintf(tc, "\t\t\tif (fld%d > %s%d) continue;\n", 548 j, buf0, j); 549 fprintf(tc, "\t\t\tif (fld%d < %s%d) goto found%d;\n\n", 550 j, buf0, j, q->qid); 551 } 552 fprintf(tc, "\t\t}\n"); 553 fprintf(tc, "\tfound%d:\n", q->qid); 554 sprintf(buf0, "((Q%d *)z)->", q->qid); 555 fprintf(tc, "\t\tfor (k = %sQlen - 1; k >= j; k--)\n", buf0); 556 fprintf(tc, "\t\t{\t/* shift up */\n"); 557 for (j = 0; j < q->nflds; j++) 558 { fprintf(tc, "\t\t\t%scontents[k+1].fld%d = ", buf0, j); 559 fprintf(tc, "%scontents[k].fld%d;\n", buf0, j); 560 } 561 fprintf(tc, "\t\t}\n"); 562 563 fprintf(tc, "\tappend%d:\t/* insert in slot j */\n", q->qid); 564 } 565 566 fprintf(tc, "\t\t(trpt+1)->oval = j;\n"); 567 fprintf(tc, "\t\t%sQlen = %sQlen + 1;\n", buf0, buf0); 568 sprintf(buf0, "((Q%d *)z)->contents[j].fld", q->qid); 569 for (j = 0; j < q->nflds; j++) 570 fprintf(tc, "\t\t%s%d = fld%d;\n", buf0, j, j); 571 fprintf(tc, "\t\tbreak;\n"); 572 } 573 ntimes(tc, 0, 1, Addq2); 574 575 for (q = qtab; q; q = q->nxt) 576 fprintf(tc, "\tcase %d: return %d;\n", q->qid, (!q->nslots)); 577 578 ntimes(tc, 0, 1, Addq3); 579 580 for (q = qtab; q; q = q->nxt) 581 fprintf(tc, "\tcase %d: return (q_sz(from) == %d);\n", 582 q->qid, max(1, q->nslots)); 583 584 ntimes(tc, 0, 1, Addq4); 585 for (q = qtab; q; q = q->nxt) 586 { sprintf(buf0, "((Q%d *)z)->", q->qid); 587 fprintf(tc, " case %d:%s\n\t\t", 588 q->qid, (q->nslots)?"":" /* =rv= */"); 589 if (q->nflds == 1) 590 { fprintf(tc, "if (fld == 0) r = %s", buf0); 591 fprintf(tc, "contents[slot].fld0;\n"); 592 } else 593 { fprintf(tc, "switch (fld) {\n"); 594 ncases(tc, q->qid, 0, q->nflds, R12); 595 fprintf(tc, "\t\t}\n"); 596 } 597 fprintf(tc, "\t\tif (done)\n"); 598 fprintf(tc, "\t\t{ j = %sQlen;\n", buf0); 599 fprintf(tc, "\t\t %sQlen = --j;\n", buf0); 600 fprintf(tc, "\t\t for (k=slot; k<j; k++)\n"); 601 fprintf(tc, "\t\t {\n"); 602 603 sprintf(buf0, "\t\t\t((Q%d *)z)->contents", q->qid); 604 for (j = 0; j < q->nflds; j++) 605 { fprintf(tc, "\t%s[k].fld%d = \n", buf0, j); 606 fprintf(tc, "\t\t%s[k+1].fld%d;\n", buf0, j); 607 } 608 fprintf(tc, "\t\t }\n"); 609 for (j = 0; j < q->nflds; j++) 610 fprintf(tc, "%s[j].fld%d = 0;\n", buf0, j); 611 fprintf(tc, "\t\t\tif (fld+1 != %d)\n\t\t\t", q->nflds); 612 fprintf(tc, "\tuerror(\"missing pars in receive\");\n"); 613 /* incompletely received msgs cannot be unrecv'ed */ 614 fprintf(tc, "\t\t}\n"); 615 fprintf(tc, "\t\tbreak;\n"); 616 } 617 ntimes(tc, 0, 1, Addq5); 618 ntimes(th, 0, 1, Proto); /* tag on function prototypes */ 619 fprintf(th, "void qsend(int, int"); 620 for (j = 0; j < Mpars; j++) 621 fprintf(th, ", int"); 622 fprintf(th, ");\n"); 623 624 fprintf(th, "#define Addproc(x) addproc(x"); 625 for (j = 0; j < Npars; j++) 626 fprintf(th, ", 0"); 627 fprintf(th, ")\n"); 628 } 629