1 /***** spin: pangen1.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 #include "pangen1.h" 15 #include "pangen3.h" 16 17 extern FILE *tc, *th, *tt; 18 extern Label *labtab; 19 extern Ordered *all_names; 20 extern ProcList *rdy; 21 extern Queue *qtab; 22 extern Symbol *Fname; 23 extern int lineno, verbose, Pid, separate; 24 extern int nrRdy, nqs, mst, Mpars, claimnr, eventmapnr; 25 extern short has_sorted, has_random, has_provided; 26 27 int Npars=0, u_sync=0, u_async=0, hastrack = 1; 28 short has_io = 0; 29 short has_state=0; /* code contains c_state */ 30 31 static Symbol *LstSet=ZS; 32 static int acceptors=0, progressors=0, nBits=0; 33 static int Types[] = { UNSIGNED, BIT, BYTE, CHAN, MTYPE, SHORT, INT, STRUCT }; 34 35 static int doglobal(char *, int); 36 static void dohidden(void); 37 static void do_init(FILE *, Symbol *); 38 static void end_labs(Symbol *, int); 39 static void put_ptype(char *, int, int, int); 40 static void tc_predef_np(void); 41 static void put_pinit(ProcList *); 42 void walk_struct(FILE *, int, char *, Symbol *, char *, char *, char *); 43 44 static void 45 reverse_names(ProcList *p) 46 { 47 if (!p) return; 48 reverse_names(p->nxt); 49 fprintf(th, " \"%s\",\n", p->n->name); 50 } 51 52 void 53 genheader(void) 54 { ProcList *p; int i; 55 56 if (separate == 2) 57 { putunames(th); 58 goto here; 59 } 60 61 fprintf(th, "#define SYNC %d\n", u_sync); 62 fprintf(th, "#define ASYNC %d\n\n", u_async); 63 64 putunames(th); 65 66 fprintf(tc, "short Air[] = { "); 67 for (p = rdy, i=0; p; p = p->nxt, i++) 68 fprintf(tc, "%s (short) Air%d", (p!=rdy)?",":"", i); 69 fprintf(tc, ", (short) Air%d", i); /* np_ */ 70 fprintf(tc, " };\n"); 71 72 fprintf(th, "char *procname[] = {\n"); 73 reverse_names(rdy); 74 fprintf(th, " \":np_:\",\n"); 75 fprintf(th, "};\n\n"); 76 77 here: 78 for (p = rdy; p; p = p->nxt) 79 put_ptype(p->n->name, p->tn, mst, nrRdy+1); 80 /* +1 for np_ */ 81 put_ptype("np_", nrRdy, mst, nrRdy+1); 82 83 ntimes(th, 0, 1, Head0); 84 85 if (separate != 2) 86 { extern void c_add_stack(FILE *); 87 88 ntimes(th, 0, 1, Header); 89 c_add_stack(th); 90 ntimes(th, 0, 1, Header0); 91 } 92 ntimes(th, 0, 1, Head1); 93 94 LstSet = ZS; 95 (void) doglobal("", PUTV); 96 97 hastrack = c_add_sv(th); 98 99 fprintf(th, " uchar sv[VECTORSZ];\n"); 100 fprintf(th, "} State"); 101 #ifdef SOLARIS 102 fprintf(th,"\n#ifdef GCC\n"); 103 fprintf(th, "\t__attribute__ ((aligned(8)))"); 104 fprintf(th, "\n#endif\n\t"); 105 #endif 106 fprintf(th, ";\n\n"); 107 108 fprintf(th, "#define HAS_TRACK %d\n", hastrack); 109 110 if (separate != 2) 111 dohidden(); 112 } 113 114 void 115 genaddproc(void) 116 { ProcList *p; 117 int i = 0; 118 119 if (separate ==2) goto shortcut; 120 121 fprintf(tc, "int\naddproc(int n"); 122 for (i = 0; i < Npars; i++) 123 fprintf(tc, ", int par%d", i); 124 125 ntimes(tc, 0, 1, Addp0); 126 ntimes(tc, 1, nrRdy+1, R5); /* +1 for np_ */ 127 ntimes(tc, 0, 1, Addp1); 128 129 if (has_provided) 130 { fprintf(tt, "\nint\nprovided(int II, unsigned char ot, "); 131 fprintf(tt, "int tt, Trans *t)\n"); 132 fprintf(tt, "{\n\tswitch(ot) {\n"); 133 } 134 shortcut: 135 tc_predef_np(); 136 for (p = rdy; p; p = p->nxt) 137 { Pid = p->tn; 138 put_pinit(p); 139 } 140 if (separate == 2) return; 141 142 Pid = 0; 143 if (has_provided) 144 { fprintf(tt, "\tdefault: return 1; /* e.g., a claim */\n"); 145 fprintf(tt, "\t}\n\treturn 0;\n}\n"); 146 } 147 148 ntimes(tc, i, i+1, R6); 149 if (separate == 0) 150 ntimes(tc, 1, nrRdy+1, R5); /* +1 for np_ */ 151 else 152 ntimes(tc, 1, nrRdy, R5); 153 ntimes(tc, 0, 1, R8a); 154 } 155 156 void 157 do_locinits(FILE *fd) 158 { ProcList *p; 159 160 for (p = rdy; p; p = p->nxt) 161 c_add_locinit(fd, p->tn, p->n->name); 162 } 163 164 void 165 genother(void) 166 { ProcList *p; 167 168 switch (separate) { 169 case 2: 170 if (claimnr >= 0) 171 ntimes(tc, claimnr, claimnr+1, R0); /* claim only */ 172 break; 173 case 1: 174 ntimes(tc, 0, 1, Code0); 175 ntimes(tc, 0, claimnr, R0); /* all except claim */ 176 ntimes(tc, claimnr+1, nrRdy, R0); 177 break; 178 case 0: 179 ntimes(tc, 0, 1, Code0); 180 ntimes(tc, 0, nrRdy+1, R0); /* +1 for np_ */ 181 break; 182 } 183 184 for (p = rdy; p; p = p->nxt) 185 end_labs(p->n, p->tn); 186 187 switch (separate) { 188 case 2: 189 if (claimnr >= 0) 190 ntimes(tc, claimnr, claimnr+1, R0a); /* claim only */ 191 return; 192 case 1: 193 ntimes(tc, 0, claimnr, R0a); /* all except claim */ 194 ntimes(tc, claimnr+1, nrRdy, R0a); 195 fprintf(tc, " if (state_tables)\n"); 196 fprintf(tc, " ini_claim(%d, 0);\n", claimnr); 197 break; 198 case 0: 199 ntimes(tc, 0, nrRdy, R0a); /* all */ 200 break; 201 } 202 203 ntimes(tc, 0, 1, R0b); 204 if (separate == 1 && acceptors == 0) 205 acceptors = 1; /* assume at least 1 acceptstate */ 206 ntimes(th, acceptors, acceptors+1, Code1); 207 ntimes(th, progressors, progressors+1, Code3); 208 ntimes(th, nrRdy+1, nrRdy+2, R2); /* +1 for np_ */ 209 210 fprintf(tc, " iniglobals();\n"); 211 ntimes(tc, 0, 1, Code2a); 212 ntimes(tc, 0, 1, Code2b); /* bfs option */ 213 ntimes(tc, 0, 1, Code2c); 214 ntimes(tc, 0, nrRdy, R4); 215 fprintf(tc, "}\n\n"); 216 217 fprintf(tc, "void\n"); 218 fprintf(tc, "iniglobals(void)\n{\n"); 219 if (doglobal("", INIV) > 0) 220 { fprintf(tc, "#ifdef VAR_RANGES\n"); 221 (void) doglobal("logval(\"", LOGV); 222 fprintf(tc, "#endif\n"); 223 } 224 ntimes(tc, 1, nqs+1, R3); 225 fprintf(tc, "\tMaxbody = max(Maxbody, sizeof(State)-VECTORSZ);"); 226 fprintf(tc, "\n}\n\n"); 227 } 228 229 void 230 gensvmap(void) 231 { 232 ntimes(tc, 0, 1, SvMap); 233 } 234 235 static struct { 236 char *s, *t; int n, m, p; 237 } ln[] = { 238 {"end", "stopstate", 3, 0, 0}, 239 {"progress", "progstate", 8, 0, 1}, 240 {"accept", "accpstate", 6, 1, 0}, 241 {0, 0, 0, 0, 0}, 242 }; 243 244 static void 245 end_labs(Symbol *s, int i) 246 { int oln = lineno; 247 Symbol *ofn = Fname; 248 Label *l; 249 int j; char foo[128]; 250 251 if ((i == claimnr && separate == 1) 252 || (i != claimnr && separate == 2)) 253 return; 254 255 for (l = labtab; l; l = l->nxt) 256 for (j = 0; ln[j].n; j++) 257 if (strncmp(l->s->name, ln[j].s, ln[j].n) == 0 258 && strcmp(l->c->name, s->name) == 0) 259 { fprintf(tc, "\t%s[%d][%d] = 1;\n", 260 ln[j].t, i, l->e->seqno); 261 acceptors += ln[j].m; 262 progressors += ln[j].p; 263 if (l->e->status & D_ATOM) 264 { sprintf(foo, "%s label inside d_step", 265 ln[j].s); 266 goto complain; 267 } 268 if (j > 0 && (l->e->status & ATOM)) 269 { sprintf(foo, "%s label inside atomic", 270 ln[j].s); 271 complain: lineno = l->e->n->ln; 272 Fname = l->e->n->fn; 273 printf("spin: %3d:%s, warning, %s - is invisible\n", 274 lineno, Fname?Fname->name:"-", foo); 275 } 276 } 277 /* visible states -- through remote refs: */ 278 for (l = labtab; l; l = l->nxt) 279 if (l->visible 280 && strcmp(l->s->context->name, s->name) == 0) 281 fprintf(tc, "\tvisstate[%d][%d] = 1;\n", 282 i, l->e->seqno); 283 284 lineno = oln; 285 Fname = ofn; 286 } 287 288 void 289 ntimes(FILE *fd, int n, int m, char *c[]) 290 { 291 int i, j; 292 for (j = 0; c[j]; j++) 293 for (i = n; i < m; i++) 294 { fprintf(fd, c[j], i, i, i, i, i, i); 295 fprintf(fd, "\n"); 296 } 297 } 298 299 void 300 prehint(Symbol *s) 301 { Lextok *n; 302 303 printf("spin: warning, "); 304 if (!s) return; 305 306 n = (s->context != ZS)?s->context->ini:s->ini; 307 if (n) 308 printf("line %3d %s, ", n->ln, n->fn->name); 309 } 310 311 void 312 checktype(Symbol *sp, char *s) 313 { char buf[128]; int i; 314 315 if (!s 316 || (sp->type != BYTE 317 && sp->type != SHORT 318 && sp->type != INT)) 319 return; 320 321 if (sp->hidden&16) /* formal parameter */ 322 { ProcList *p; Lextok *f, *t; 323 int posnr = 0; 324 for (p = rdy; p; p = p->nxt) 325 if (p->n->name 326 && strcmp(s, p->n->name) == 0) 327 break; 328 if (p) 329 for (f = p->p; f; f = f->rgt) /* list of types */ 330 for (t = f->lft; t; t = t->rgt, posnr++) 331 if (t->sym 332 && strcmp(t->sym->name, sp->name) == 0) 333 { checkrun(sp, posnr); 334 return; 335 } 336 337 } else if (!(sp->hidden&4)) 338 { if (!(verbose&32)) return; 339 sputtype(buf, sp->type); 340 i = (int) strlen(buf); 341 while (buf[--i] == ' ') buf[i] = '\0'; 342 prehint(sp); 343 if (sp->context) 344 printf("proctype %s:", s); 345 else 346 printf("global"); 347 printf(" '%s %s' could be declared 'bit %s'\n", 348 buf, sp->name, sp->name); 349 } else if (sp->type != BYTE && !(sp->hidden&8)) 350 { if (!(verbose&32)) return; 351 sputtype(buf, sp->type); 352 i = (int) strlen(buf); 353 while (buf[--i] == ' ') buf[i] = '\0'; 354 prehint(sp); 355 if (sp->context) 356 printf("proctype %s:", s); 357 else 358 printf("global"); 359 printf(" '%s %s' could be declared 'byte %s'\n", 360 buf, sp->name, sp->name); 361 } 362 } 363 364 int 365 dolocal(FILE *ofd, char *pre, int dowhat, int p, char *s) 366 { int h, j, k=0; extern int nr_errs; 367 Ordered *walk; 368 Symbol *sp; 369 char buf[64], buf2[128], buf3[128]; 370 371 if (dowhat == INIV) 372 { /* initialize in order of declaration */ 373 for (walk = all_names; walk; walk = walk->next) 374 { sp = walk->entry; 375 if (sp->context 376 && !sp->owner 377 && strcmp(s, sp->context->name) == 0) 378 { checktype(sp, s); /* fall through */ 379 if (!(sp->hidden&16)) 380 { sprintf(buf, "((P%d *)pptr(h))->", p); 381 do_var(ofd, dowhat, buf, sp, "", " = ", ";\n"); 382 } 383 k++; 384 } } 385 } else 386 { for (j = 0; j < 8; j++) 387 for (h = 0; h <= 1; h++) 388 for (walk = all_names; walk; walk = walk->next) 389 { sp = walk->entry; 390 if (sp->context 391 && !sp->owner 392 && sp->type == Types[j] 393 && ((h == 0 && sp->nel == 1) || (h == 1 && sp->nel > 1)) 394 && strcmp(s, sp->context->name) == 0) 395 { switch (dowhat) { 396 case LOGV: 397 if (sp->type == CHAN 398 && verbose == 0) 399 break; 400 sprintf(buf, "%s%s:", pre, s); 401 { sprintf(buf2, "\", ((P%d *)pptr(h))->", p); 402 sprintf(buf3, ");\n"); 403 } 404 do_var(ofd, dowhat, "", sp, buf, buf2, buf3); 405 break; 406 case PUTV: 407 sprintf(buf, "((P%d *)pptr(h))->", p); 408 do_var(ofd, dowhat, buf, sp, "", " = ", ";\n"); 409 k++; 410 break; 411 } 412 if (strcmp(s, ":never:") == 0) 413 { printf("error: %s defines local %s\n", 414 s, sp->name); 415 nr_errs++; 416 } } } } 417 418 return k; 419 } 420 421 void 422 c_chandump(FILE *fd) 423 { Queue *q; 424 char buf[256]; 425 int i; 426 427 if (!qtab) 428 { fprintf(fd, "void\nc_chandump(int unused) "); 429 fprintf(fd, "{ unused = unused++; /* avoid complaints */ }\n"); 430 return; 431 } 432 433 fprintf(fd, "void\nc_chandump(int from)\n"); 434 fprintf(fd, "{ uchar *z; int slot;\n"); 435 436 fprintf(fd, " from--;\n"); 437 fprintf(fd, " if (from >= (int) now._nr_qs || from < 0)\n"); 438 fprintf(fd, " { printf(\"pan: bad qid %%d\\n\", from+1);\n"); 439 fprintf(fd, " return;\n"); 440 fprintf(fd, " }\n"); 441 fprintf(fd, " z = qptr(from);\n"); 442 fprintf(fd, " switch (((Q0 *)z)->_t) {\n"); 443 444 for (q = qtab; q; q = q->nxt) 445 { fprintf(fd, " case %d:\n\t\t", q->qid); 446 sprintf(buf, "((Q%d *)z)->", q->qid); 447 448 fprintf(fd, "for (slot = 0; slot < %sQlen; slot++)\n\t\t", buf); 449 fprintf(fd, "{ printf(\" [\");\n\t\t"); 450 for (i = 0; i < q->nflds; i++) 451 { if (q->fld_width[i] == MTYPE) 452 { fprintf(fd, "\tprintm(%scontents[slot].fld%d);\n\t\t", 453 buf, i); 454 } else 455 fprintf(fd, "\tprintf(\"%%d,\", %scontents[slot].fld%d);\n\t\t", 456 buf, i); 457 } 458 fprintf(fd, " printf(\"],\");\n\t\t"); 459 fprintf(fd, "}\n\t\t"); 460 fprintf(fd, "break;\n"); 461 } 462 fprintf(fd, " }\n"); 463 fprintf(fd, " printf(\"\\n\");\n}\n"); 464 } 465 466 void 467 c_var(FILE *fd, char *pref, Symbol *sp) 468 { char buf[256]; 469 int i; 470 471 switch (sp->type) { 472 case STRUCT: 473 /* c_struct(fd, pref, sp); */ 474 fprintf(fd, "\t\tprintf(\"\t(struct %s)\\n\");\n", 475 sp->name); 476 sprintf(buf, "%s%s.", pref, sp->name); 477 c_struct(fd, buf, sp); 478 break; 479 case BIT: case BYTE: 480 case SHORT: case INT: 481 case UNSIGNED: 482 sputtype(buf, sp->type); 483 if (sp->nel == 1) 484 { fprintf(fd, "\tprintf(\"\t%s %s:\t%%d\\n\", %s%s);\n", 485 buf, sp->name, pref, sp->name); 486 } else 487 { fprintf(fd, "\t{\tint l_in;\n"); 488 fprintf(fd, "\t\tfor (l_in = 0; l_in < %d; l_in++)\n", sp->nel); 489 fprintf(fd, "\t\t{\n"); 490 fprintf(fd, "\t\t\tprintf(\"\t%s %s[%%d]:\t%%d\\n\", l_in, %s%s[l_in]);\n", 491 buf, sp->name, pref, sp->name); 492 fprintf(fd, "\t\t}\n"); 493 fprintf(fd, "\t}\n"); 494 } 495 break; 496 case CHAN: 497 if (sp->nel == 1) 498 { fprintf(fd, "\tprintf(\"\tchan %s (=%%d):\tlen %%d:\\t\", ", 499 sp->name); 500 fprintf(fd, "%s%s, q_len(%s%s));\n", 501 pref, sp->name, pref, sp->name); 502 fprintf(fd, "\tc_chandump(%s%s);\n", pref, sp->name); 503 } else 504 for (i = 0; i < sp->nel; i++) 505 { fprintf(fd, "\tprintf(\"\tchan %s[%d] (=%%d):\tlen %%d:\\t\", ", 506 sp->name, i); 507 fprintf(fd, "%s%s[%d], q_len(%s%s[%d]));\n", 508 pref, sp->name, i, pref, sp->name, i); 509 fprintf(fd, "\tc_chandump(%s%s[%d]);\n", 510 pref, sp->name, i); 511 } 512 break; 513 } 514 } 515 516 int 517 c_splurge_any(ProcList *p) 518 { Ordered *walk; 519 Symbol *sp; 520 521 if (strcmp(p->n->name, ":never:") != 0 522 && strcmp(p->n->name, ":trace:") != 0 523 && strcmp(p->n->name, ":notrace:") != 0) 524 for (walk = all_names; walk; walk = walk->next) 525 { sp = walk->entry; 526 if (!sp->context 527 || sp->type == 0 528 || strcmp(sp->context->name, p->n->name) != 0 529 || sp->owner || (sp->hidden&1) 530 || (sp->type == MTYPE && ismtype(sp->name))) 531 continue; 532 533 return 1; 534 } 535 return 0; 536 } 537 538 void 539 c_splurge(FILE *fd, ProcList *p) 540 { Ordered *walk; 541 Symbol *sp; 542 char pref[64]; 543 544 if (strcmp(p->n->name, ":never:") != 0 545 && strcmp(p->n->name, ":trace:") != 0 546 && strcmp(p->n->name, ":notrace:") != 0) 547 for (walk = all_names; walk; walk = walk->next) 548 { sp = walk->entry; 549 if (!sp->context 550 || sp->type == 0 551 || strcmp(sp->context->name, p->n->name) != 0 552 || sp->owner || (sp->hidden&1) 553 || (sp->type == MTYPE && ismtype(sp->name))) 554 continue; 555 556 sprintf(pref, "((P%d *)pptr(pid))->", p->tn); 557 c_var(fd, pref, sp); 558 } 559 } 560 561 void 562 c_wrapper(FILE *fd) /* allow pan.c to print out global sv entries */ 563 { Ordered *walk; 564 ProcList *p; 565 Symbol *sp; 566 Lextok *n; 567 extern Lextok *Mtype; 568 int j; 569 570 fprintf(fd, "void\nc_globals(void)\n{\t/* int i; */\n"); 571 fprintf(fd, " printf(\"global vars:\\n\");\n"); 572 for (walk = all_names; walk; walk = walk->next) 573 { sp = walk->entry; 574 if (sp->context || sp->owner || (sp->hidden&1) 575 || (sp->type == MTYPE && ismtype(sp->name))) 576 continue; 577 578 c_var(fd, "now.", sp); 579 } 580 fprintf(fd, "}\n"); 581 582 fprintf(fd, "void\nc_locals(int pid, int tp)\n{\t/* int i; */\n"); 583 fprintf(fd, " switch(tp) {\n"); 584 for (p = rdy; p; p = p->nxt) 585 { fprintf(fd, " case %d:\n", p->tn); 586 fprintf(fd, " \tprintf(\"local vars proc %%d (%s):\\n\", pid);\n", 587 p->n->name); 588 if (c_splurge_any(p)) 589 { fprintf(fd, " \tprintf(\"local vars proc %%d (%s):\\n\", pid);\n", 590 p->n->name); 591 c_splurge(fd, p); 592 } else 593 { fprintf(fd, " \t/* none */\n"); 594 } 595 fprintf(fd, " \tbreak;\n"); 596 } 597 fprintf(fd, " }\n}\n"); 598 599 fprintf(fd, "void\nprintm(int x)\n{\n"); 600 fprintf(fd, " switch (x) {\n"); 601 for (n = Mtype, j = 1; n && j; n = n->rgt, j++) 602 fprintf(fd, "\tcase %d: Printf(\"%s\"); break;\n", 603 j, n->lft->sym->name); 604 fprintf(fd, " default: Printf(\"%%d\", x);\n"); 605 fprintf(fd, " }\n"); 606 fprintf(fd, "}\n"); 607 } 608 609 static int 610 doglobal(char *pre, int dowhat) 611 { Ordered *walk; 612 Symbol *sp; 613 int j, cnt = 0; 614 615 for (j = 0; j < 8; j++) 616 for (walk = all_names; walk; walk = walk->next) 617 { sp = walk->entry; 618 if (!sp->context 619 && !sp->owner 620 && sp->type == Types[j]) 621 { if (Types[j] != MTYPE || !ismtype(sp->name)) 622 switch (dowhat) { 623 case LOGV: 624 if (sp->type == CHAN 625 && verbose == 0) 626 break; 627 if (sp->hidden&1) 628 break; 629 do_var(tc, dowhat, "", sp, 630 pre, "\", now.", ");\n"); 631 break; 632 case INIV: 633 checktype(sp, (char *) 0); 634 cnt++; /* fall through */ 635 case PUTV: 636 do_var(tc, dowhat, (sp->hidden&1)?"":"now.", sp, 637 "", " = ", ";\n"); 638 break; 639 } } } 640 return cnt; 641 } 642 643 static void 644 dohidden(void) 645 { Ordered *walk; 646 Symbol *sp; 647 int j; 648 649 for (j = 0; j < 8; j++) 650 for (walk = all_names; walk; walk = walk->next) 651 { sp = walk->entry; 652 if ((sp->hidden&1) 653 && sp->type == Types[j]) 654 { if (sp->context || sp->owner) 655 fatal("cannot hide non-globals (%s)", sp->name); 656 if (sp->type == CHAN) 657 fatal("cannot hide channels (%s)", sp->name); 658 fprintf(th, "/* hidden variable: */"); 659 typ2c(sp); 660 } } 661 fprintf(th, "int _; /* a predefined write-only variable */\n\n"); 662 } 663 664 void 665 do_var(FILE *ofd, int dowhat, char *s, Symbol *sp, 666 char *pre, char *sep, char *ter) 667 { int i; 668 669 switch(dowhat) { 670 case PUTV: 671 672 if (sp->hidden&1) break; 673 674 typ2c(sp); 675 break; 676 case LOGV: 677 case INIV: 678 if (sp->type == STRUCT) 679 { /* struct may contain a chan */ 680 walk_struct(ofd, dowhat, s, sp, pre, sep, ter); 681 break; 682 } 683 if (!sp->ini && dowhat != LOGV) /* it defaults to 0 */ 684 break; 685 if (sp->nel == 1) 686 { fprintf(ofd, "\t\t%s%s%s%s", 687 pre, s, sp->name, sep); 688 if (dowhat == LOGV) 689 fprintf(ofd, "%s%s", s, sp->name); 690 else 691 do_init(ofd, sp); 692 fprintf(ofd, "%s", ter); 693 } else 694 { if (sp->ini && sp->ini->ntyp == CHAN) 695 { for (i = 0; i < sp->nel; i++) 696 { fprintf(ofd, "\t\t%s%s%s[%d]%s", 697 pre, s, sp->name, i, sep); 698 if (dowhat == LOGV) 699 fprintf(ofd, "%s%s[%d]", 700 s, sp->name, i); 701 else 702 do_init(ofd, sp); 703 fprintf(ofd, "%s", ter); 704 } 705 } else 706 { fprintf(ofd, "\t{\tint l_in;\n"); 707 fprintf(ofd, "\t\tfor (l_in = 0; l_in < %d; l_in++)\n", sp->nel); 708 fprintf(ofd, "\t\t{\n"); 709 fprintf(ofd, "\t\t\t%s%s%s[l_in]%s", 710 pre, s, sp->name, sep); 711 if (dowhat == LOGV) 712 fprintf(ofd, "%s%s[l_in]", s, sp->name); 713 else 714 putstmnt(ofd, sp->ini, 0); 715 fprintf(ofd, "%s", ter); 716 fprintf(ofd, "\t\t}\n"); 717 fprintf(ofd, "\t}\n"); 718 } } 719 break; 720 } 721 } 722 723 static void 724 do_init(FILE *ofd, Symbol *sp) 725 { int i; extern Queue *ltab[]; 726 727 if (sp->ini 728 && sp->type == CHAN 729 && ((i = qmake(sp)) > 0)) 730 { if (sp->ini->ntyp == CHAN) 731 fprintf(ofd, "addqueue(%d, %d)", 732 i, ltab[i-1]->nslots == 0); 733 else 734 fprintf(ofd, "%d", i); 735 } else 736 putstmnt(ofd, sp->ini, 0); 737 } 738 739 static int 740 blog(int n) /* for small log2 without rounding problems */ 741 { int m=1, r=2; 742 743 while (r < n) { m++; r *= 2; } 744 return 1+m; 745 } 746 747 static void 748 put_ptype(char *s, int i, int m0, int m1) 749 { int k; 750 751 if (strcmp(s, ":init:") == 0) 752 fprintf(th, "#define Pinit ((P%d *)this)\n", i); 753 754 if (strcmp(s, ":never:") != 0 755 && strcmp(s, ":trace:") != 0 756 && strcmp(s, ":notrace:") != 0 757 && strcmp(s, ":init:") != 0 758 && strcmp(s, "_:never_template:_") != 0 759 && strcmp(s, "np_") != 0) 760 fprintf(th, "#define P%s ((P%d *)this)\n", s, i); 761 762 fprintf(th, "typedef struct P%d { /* %s */\n", i, s); 763 fprintf(th, " unsigned _pid : 8; /* 0..255 */\n"); 764 fprintf(th, " unsigned _t : %d; /* proctype */\n", blog(m1)); 765 fprintf(th, " unsigned _p : %d; /* state */\n", blog(m0)); 766 LstSet = ZS; 767 nBits = 8 + blog(m1) + blog(m0); 768 k = dolocal(tc, "", PUTV, i, s); /* includes pars */ 769 770 c_add_loc(th, s); 771 772 fprintf(th, "} P%d;\n", i); 773 if ((!LstSet && k > 0) || has_state) 774 fprintf(th, "#define Air%d 0\n", i); 775 else 776 { fprintf(th, "#define Air%d (sizeof(P%d) - ", i, i); 777 if (k == 0) 778 { fprintf(th, "%d", (nBits+7)/8); 779 goto done; 780 } 781 if ((LstSet->type != BIT && LstSet->type != UNSIGNED) 782 || LstSet->nel != 1) 783 { fprintf(th, "Offsetof(P%d, %s) - %d*sizeof(", 784 i, LstSet->name, LstSet->nel); 785 } 786 switch(LstSet->type) { 787 case UNSIGNED: 788 fprintf(th, "%d", (nBits+7)/8); 789 break; 790 case BIT: 791 if (LstSet->nel == 1) 792 { fprintf(th, "%d", (nBits+7)/8); 793 break; 794 } /* else fall through */ 795 case MTYPE: case BYTE: case CHAN: 796 fprintf(th, "uchar)"); break; 797 case SHORT: 798 fprintf(th, "short)"); break; 799 case INT: 800 fprintf(th, "int)"); break; 801 default: 802 fatal("cannot happen Air %s", 803 LstSet->name); 804 } 805 done: fprintf(th, ")\n"); 806 } 807 } 808 809 static void 810 tc_predef_np(void) 811 { int i = nrRdy; /* 1+ highest proctype nr */ 812 813 fprintf(th, "#define _NP_ %d\n", i); 814 /* if (separate == 2) fprintf(th, "extern "); */ 815 fprintf(th, "uchar reached%d[3]; /* np_ */\n", i); 816 817 fprintf(th, "#define nstates%d 3 /* np_ */\n", i); 818 fprintf(th, "#define endstate%d 2 /* np_ */\n\n", i); 819 fprintf(th, "#define start%d 0 /* np_ */\n", i); 820 821 fprintf(tc, "\tcase %d: /* np_ */\n", i); 822 if (separate == 1) 823 { fprintf(tc, "\t\tini_claim(%d, h);\n", i); 824 } else 825 { fprintf(tc, "\t\t((P%d *)pptr(h))->_t = %d;\n", i, i); 826 fprintf(tc, "\t\t((P%d *)pptr(h))->_p = 0;\n", i); 827 fprintf(tc, "\t\treached%d[0] = 1;\n", i); 828 fprintf(tc, "\t\taccpstate[%d][1] = 1;\n", i); 829 } 830 fprintf(tc, "\t\tbreak;\n"); 831 } 832 833 static void 834 put_pinit(ProcList *P) 835 { Lextok *fp, *fpt, *t; 836 Element *e = P->s->frst; 837 Symbol *s = P->n; 838 Lextok *p = P->p; 839 int i = P->tn; 840 int ini, j, k; 841 842 if (i == claimnr 843 && separate == 1) 844 { fprintf(tc, "\tcase %d: /* %s */\n", i, s->name); 845 fprintf(tc, "\t\tini_claim(%d, h);\n", i); 846 fprintf(tc, "\t\tbreak;\n"); 847 return; 848 } 849 if (i != claimnr 850 && separate == 2) 851 return; 852 853 ini = huntele(e, e->status, -1)->seqno; 854 fprintf(th, "#define start%d %d\n", i, ini); 855 if (i == claimnr) 856 fprintf(th, "#define start_claim %d\n", ini); 857 if (i == eventmapnr) 858 fprintf(th, "#define start_event %d\n", ini); 859 860 fprintf(tc, "\tcase %d: /* %s */\n", i, s->name); 861 862 fprintf(tc, "\t\t((P%d *)pptr(h))->_t = %d;\n", i, i); 863 fprintf(tc, "\t\t((P%d *)pptr(h))->_p = %d;", i, ini); 864 fprintf(tc, " reached%d[%d]=1;\n", i, ini); 865 866 if (has_provided) 867 { fprintf(tt, "\tcase %d: /* %s */\n\t\t", i, s->name); 868 if (P->prov) 869 { fprintf(tt, "if ("); 870 putstmnt(tt, P->prov, 0); 871 fprintf(tt, ")\n\t\t\t"); 872 } 873 fprintf(tt, "return 1;\n"); 874 if (P->prov) 875 fprintf(tt, "\t\tbreak;\n"); 876 } 877 878 fprintf(tc, "\t\t/* params: */\n"); 879 for (fp = p, j=0; fp; fp = fp->rgt) 880 for (fpt = fp->lft; fpt; fpt = fpt->rgt, j++) 881 { t = (fpt->ntyp == ',') ? fpt->lft : fpt; 882 if (t->sym->nel != 1) 883 { lineno = t->ln; 884 Fname = t->fn; 885 fatal("array in parameter list, %s", 886 t->sym->name); 887 } 888 fprintf(tc, "\t\t((P%d *)pptr(h))->", i); 889 if (t->sym->type == STRUCT) 890 { if (full_name(tc, t, t->sym, 1)) 891 { lineno = t->ln; 892 Fname = t->fn; 893 fatal("hidden array in parameter %s", 894 t->sym->name); 895 } 896 } else 897 fprintf(tc, "%s", t->sym->name); 898 fprintf(tc, " = par%d;\n", j); 899 } 900 fprintf(tc, "\t\t/* locals: */\n"); 901 k = dolocal(tc, "", INIV, i, s->name); 902 if (k > 0) 903 { fprintf(tc, "#ifdef VAR_RANGES\n"); 904 (void) dolocal(tc, "logval(\"", LOGV, i, s->name); 905 fprintf(tc, "#endif\n"); 906 } 907 908 fprintf(tc, "#ifdef HAS_CODE\n"); 909 fprintf(tc, "\t\tlocinit%d(h);\n", i); 910 fprintf(tc, "#endif\n"); 911 912 dumpclaims(tc, i, s->name); 913 fprintf(tc, "\t break;\n"); 914 } 915 916 Element * 917 huntstart(Element *f) 918 { Element *e = f; 919 Element *elast = (Element *) 0; 920 int cnt = 0; 921 922 while (elast != e && cnt++ < 200) /* new 4.0.8 */ 923 { elast = e; 924 if (e->n) 925 { if (e->n->ntyp == '.' && e->nxt) 926 e = e->nxt; 927 else if (e->n->ntyp == UNLESS) 928 e = e->sub->this->frst; 929 } } 930 931 if (cnt >= 200 || !e) 932 fatal("confusing control structure", (char *) 0); 933 return e; 934 } 935 936 Element * 937 huntele(Element *f, int o, int stopat) 938 { Element *g, *e = f; 939 int cnt=0; /* a precaution against loops */ 940 941 if (e) 942 for (cnt = 0; cnt < 200 && e->n; cnt++) 943 { 944 if (e->seqno == stopat) 945 break; 946 947 switch (e->n->ntyp) { 948 case GOTO: 949 g = get_lab(e->n,1); 950 cross_dsteps(e->n, g->n); 951 break; 952 case '.': 953 case BREAK: 954 if (!e->nxt) 955 return e; 956 g = e->nxt; 957 break; 958 case UNLESS: 959 g = huntele(e->sub->this->frst, o, stopat); 960 break; 961 case D_STEP: 962 case ATOMIC: 963 case NON_ATOMIC: 964 default: 965 return e; 966 } 967 if ((o & ATOM) && !(g->status & ATOM)) 968 return e; 969 e = g; 970 } 971 if (cnt >= 200 || !e) 972 fatal("confusing control structure", (char *) 0); 973 return e; 974 } 975 976 void 977 typ2c(Symbol *sp) 978 { int wsbits = sizeof(long)*8; /* wordsize in bits */ 979 switch (sp->type) { 980 case UNSIGNED: 981 if (sp->hidden&1) 982 fprintf(th, "\tuchar %s;", sp->name); 983 else 984 fprintf(th, "\tunsigned %s : %d", 985 sp->name, sp->nbits); 986 LstSet = sp; 987 if (nBits%wsbits > 0 988 && wsbits - nBits%wsbits < sp->nbits) 989 { /* must padd to a word-boundary */ 990 nBits += wsbits - nBits%wsbits; 991 } 992 nBits += sp->nbits; 993 break; 994 case BIT: 995 if (sp->nel == 1 && !(sp->hidden&1)) 996 { fprintf(th, "\tunsigned %s : 1", sp->name); 997 LstSet = sp; 998 nBits++; 999 break; 1000 } /* else fall through */ 1001 if (!(sp->hidden&1) && (verbose&32)) 1002 printf("spin: warning: bit-array %s[%d] mapped to byte-array\n", 1003 sp->name, sp->nel); 1004 nBits += 8*sp->nel; /* mapped onto array of uchars */ 1005 case MTYPE: 1006 case BYTE: 1007 case CHAN: /* good for up to 255 channels */ 1008 fprintf(th, "\tuchar %s", sp->name); 1009 LstSet = sp; 1010 break; 1011 case SHORT: 1012 fprintf(th, "\tshort %s", sp->name); 1013 LstSet = sp; 1014 break; 1015 case INT: 1016 fprintf(th, "\tint %s", sp->name); 1017 LstSet = sp; 1018 break; 1019 case STRUCT: 1020 if (!sp->Snm) 1021 fatal("undeclared structure element %s", sp->name); 1022 fprintf(th, "\tstruct %s %s", 1023 sp->Snm->name, 1024 sp->name); 1025 LstSet = ZS; 1026 break; 1027 case CODE_FRAG: 1028 case PREDEF: 1029 return; 1030 default: 1031 fatal("variable %s undeclared", sp->name); 1032 } 1033 1034 if (sp->nel != 1) 1035 fprintf(th, "[%d]", sp->nel); 1036 fprintf(th, ";\n"); 1037 } 1038 1039 static void 1040 ncases(FILE *fd, int p, int n, int m, char *c[]) 1041 { int i, j; 1042 1043 for (j = 0; c[j]; j++) 1044 for (i = n; i < m; i++) 1045 { fprintf(fd, c[j], i, p, i); 1046 fprintf(fd, "\n"); 1047 } 1048 } 1049 1050 void 1051 qlen_type(int qmax) 1052 { 1053 fprintf(th, "\t"); 1054 if (qmax < 256) 1055 fprintf(th, "uchar"); 1056 else if (qmax < 65535) 1057 fprintf(th, "ushort"); 1058 else 1059 fprintf(th, "uint"); 1060 fprintf(th, " Qlen; /* q_size */\n"); 1061 } 1062 1063 void 1064 genaddqueue(void) 1065 { char buf0[256]; 1066 int j, qmax = 0; 1067 Queue *q; 1068 1069 ntimes(tc, 0, 1, Addq0); 1070 if (has_io && !nqs) 1071 fprintf(th, "#define NQS 1 /* nqs=%d, but has_io */\n", nqs); 1072 else 1073 fprintf(th, "#define NQS %d\n", nqs); 1074 fprintf(th, "short q_flds[%d];\n", nqs+1); 1075 fprintf(th, "short q_max[%d];\n", nqs+1); 1076 1077 for (q = qtab; q; q = q->nxt) 1078 if (q->nslots > qmax) 1079 qmax = q->nslots; 1080 1081 for (q = qtab; q; q = q->nxt) 1082 { j = q->qid; 1083 fprintf(tc, "\tcase %d: j = sizeof(Q%d);", j, j); 1084 fprintf(tc, " q_flds[%d] = %d;", j, q->nflds); 1085 fprintf(tc, " q_max[%d] = %d;", j, max(1,q->nslots)); 1086 fprintf(tc, " break;\n"); 1087 1088 fprintf(th, "typedef struct Q%d {\n", j); 1089 qlen_type(qmax); /* 4.2.2 */ 1090 fprintf(th, " uchar _t; /* q_type */\n"); 1091 fprintf(th, " struct {\n"); 1092 1093 for (j = 0; j < q->nflds; j++) 1094 { switch (q->fld_width[j]) { 1095 case BIT: 1096 if (q->nflds != 1) 1097 { fprintf(th, "\t\tunsigned"); 1098 fprintf(th, " fld%d : 1;\n", j); 1099 break; 1100 } /* else fall through: smaller struct */ 1101 case MTYPE: 1102 case CHAN: 1103 case BYTE: 1104 fprintf(th, "\t\tuchar fld%d;\n", j); 1105 break; 1106 case SHORT: 1107 fprintf(th, "\t\tshort fld%d;\n", j); 1108 break; 1109 case INT: 1110 fprintf(th, "\t\tint fld%d;\n", j); 1111 break; 1112 default: 1113 fatal("bad channel spec", ""); 1114 } 1115 } 1116 fprintf(th, " } contents[%d];\n", max(1, q->nslots)); 1117 fprintf(th, "} Q%d;\n", q->qid); 1118 } 1119 1120 fprintf(th, "typedef struct Q0 {\t/* generic q */\n"); 1121 qlen_type(qmax); /* 4.2.2 */ 1122 fprintf(th, " uchar _t;\n"); 1123 fprintf(th, "} Q0;\n"); 1124 1125 ntimes(tc, 0, 1, Addq1); 1126 1127 if (has_random) 1128 { fprintf(th, "int Q_has(int"); 1129 for (j = 0; j < Mpars; j++) 1130 fprintf(th, ", int, int"); 1131 fprintf(th, ");\n"); 1132 1133 fprintf(tc, "int\nQ_has(int into"); 1134 for (j = 0; j < Mpars; j++) 1135 fprintf(tc, ", int want%d, int fld%d", j, j); 1136 fprintf(tc, ")\n"); 1137 fprintf(tc, "{ int i;\n\n"); 1138 fprintf(tc, " if (!into--)\n"); 1139 fprintf(tc, " uerror(\"ref to unknown chan "); 1140 fprintf(tc, "(recv-poll)\");\n\n"); 1141 fprintf(tc, " if (into >= now._nr_qs || into < 0)\n"); 1142 fprintf(tc, " Uerror(\"qrecv bad queue#\");\n\n"); 1143 fprintf(tc, " for (i = 0; i < ((Q0 *)qptr(into))->Qlen;"); 1144 fprintf(tc, " i++)\n"); 1145 fprintf(tc, " {\n"); 1146 for (j = 0; j < Mpars; j++) 1147 { fprintf(tc, " if (want%d && ", j); 1148 fprintf(tc, "qrecv(into+1, i, %d, 0) != fld%d)\n", 1149 j, j); 1150 fprintf(tc, " continue;\n"); 1151 } 1152 fprintf(tc, " return i+1;\n"); 1153 fprintf(tc, " }\n"); 1154 fprintf(tc, " return 0;\n"); 1155 fprintf(tc, "}\n"); 1156 } 1157 1158 fprintf(tc, "#if NQS>0\n"); 1159 fprintf(tc, "void\nqsend(int into, int sorted"); 1160 for (j = 0; j < Mpars; j++) 1161 fprintf(tc, ", int fld%d", j); 1162 fprintf(tc, ")\n"); 1163 ntimes(tc, 0, 1, Addq11); 1164 1165 for (q = qtab; q; q = q->nxt) 1166 { sprintf(buf0, "((Q%d *)z)->", q->qid); 1167 fprintf(tc, "\tcase %d:%s\n", q->qid, 1168 (q->nslots)?"":" /* =rv= */"); 1169 if (q->nslots == 0) /* reset handshake point */ 1170 fprintf(tc, "\t\t(trpt+2)->o_m = 0;\n"); 1171 1172 if (has_sorted) 1173 { fprintf(tc, "\t\tif (!sorted) goto append%d;\n", q->qid); 1174 fprintf(tc, "\t\tfor (j = 0; j < %sQlen; j++)\n", buf0); 1175 fprintf(tc, "\t\t{\t/* find insertion point */\n"); 1176 sprintf(buf0, "((Q%d *)z)->contents[j].fld", q->qid); 1177 for (j = 0; j < q->nflds; j++) 1178 { fprintf(tc, "\t\t\tif (fld%d > %s%d) continue;\n", 1179 j, buf0, j); 1180 fprintf(tc, "\t\t\tif (fld%d < %s%d) ", j, buf0, j); 1181 fprintf(tc, "goto found%d;\n\n", q->qid); 1182 } 1183 fprintf(tc, "\t\t}\n"); 1184 fprintf(tc, "\tfound%d:\n", q->qid); 1185 sprintf(buf0, "((Q%d *)z)->", q->qid); 1186 fprintf(tc, "\t\tfor (k = %sQlen - 1; k >= j; k--)\n", buf0); 1187 fprintf(tc, "\t\t{\t/* shift up */\n"); 1188 for (j = 0; j < q->nflds; j++) 1189 { fprintf(tc, "\t\t\t%scontents[k+1].fld%d = ", 1190 buf0, j); 1191 fprintf(tc, "%scontents[k].fld%d;\n", 1192 buf0, j); 1193 } 1194 fprintf(tc, "\t\t}\n"); 1195 fprintf(tc, "\tappend%d:\t/* insert in slot j */\n", q->qid); 1196 } 1197 1198 fprintf(tc, "#ifdef HAS_SORTED\n"); 1199 fprintf(tc, "\t\t(trpt+1)->ipt = j;\n"); /* ipt was bup.oval */ 1200 fprintf(tc, "#endif\n"); 1201 fprintf(tc, "\t\t%sQlen = %sQlen + 1;\n", buf0, buf0); 1202 sprintf(buf0, "((Q%d *)z)->contents[j].fld", q->qid); 1203 for (j = 0; j < q->nflds; j++) 1204 fprintf(tc, "\t\t%s%d = fld%d;\n", buf0, j, j); 1205 fprintf(tc, "\t\tbreak;\n"); 1206 } 1207 ntimes(tc, 0, 1, Addq2); 1208 1209 for (q = qtab; q; q = q->nxt) 1210 fprintf(tc, "\tcase %d: return %d;\n", q->qid, (!q->nslots)); 1211 1212 ntimes(tc, 0, 1, Addq3); 1213 1214 for (q = qtab; q; q = q->nxt) 1215 fprintf(tc, "\tcase %d: return (q_sz(from) == %d);\n", 1216 q->qid, max(1, q->nslots)); 1217 1218 ntimes(tc, 0, 1, Addq4); 1219 for (q = qtab; q; q = q->nxt) 1220 { sprintf(buf0, "((Q%d *)z)->", q->qid); 1221 fprintf(tc, " case %d:%s\n\t\t", 1222 q->qid, (q->nslots)?"":" /* =rv= */"); 1223 if (q->nflds == 1) 1224 { fprintf(tc, "if (fld == 0) r = %s", buf0); 1225 fprintf(tc, "contents[slot].fld0;\n"); 1226 } else 1227 { fprintf(tc, "switch (fld) {\n"); 1228 ncases(tc, q->qid, 0, q->nflds, R12); 1229 fprintf(tc, "\t\tdefault: Uerror"); 1230 fprintf(tc, "(\"too many fields in recv\");\n"); 1231 fprintf(tc, "\t\t}\n"); 1232 } 1233 fprintf(tc, "\t\tif (done)\n"); 1234 if (q->nslots == 0) 1235 { fprintf(tc, "\t\t{ j = %sQlen - 1;\n", buf0); 1236 fprintf(tc, "\t\t %sQlen = 0;\n", buf0); 1237 sprintf(buf0, "\t\t\t((Q%d *)z)->contents", q->qid); 1238 } else 1239 { fprintf(tc, "\t\t{ j = %sQlen;\n", buf0); 1240 fprintf(tc, "\t\t %sQlen = --j;\n", buf0); 1241 fprintf(tc, "\t\t for (k=slot; k<j; k++)\n"); 1242 fprintf(tc, "\t\t {\n"); 1243 sprintf(buf0, "\t\t\t((Q%d *)z)->contents", q->qid); 1244 for (j = 0; j < q->nflds; j++) 1245 { fprintf(tc, "\t%s[k].fld%d = \n", buf0, j); 1246 fprintf(tc, "\t\t%s[k+1].fld%d;\n", buf0, j); 1247 } 1248 fprintf(tc, "\t\t }\n"); 1249 } 1250 1251 for (j = 0; j < q->nflds; j++) 1252 fprintf(tc, "%s[j].fld%d = 0;\n", buf0, j); 1253 fprintf(tc, "\t\t\tif (fld+1 != %d)\n\t\t\t", q->nflds); 1254 fprintf(tc, "\tuerror(\"missing pars in receive\");\n"); 1255 /* incompletely received msgs cannot be unrecv'ed */ 1256 fprintf(tc, "\t\t}\n"); 1257 fprintf(tc, "\t\tbreak;\n"); 1258 } 1259 ntimes(tc, 0, 1, Addq5); 1260 for (q = qtab; q; q = q->nxt) 1261 fprintf(tc, " case %d: j = sizeof(Q%d); break;\n", 1262 q->qid, q->qid); 1263 ntimes(tc, 0, 1, R8b); 1264 1265 ntimes(th, 0, 1, Proto); /* tag on function prototypes */ 1266 fprintf(th, "void qsend(int, int"); 1267 for (j = 0; j < Mpars; j++) 1268 fprintf(th, ", int"); 1269 fprintf(th, ");\n"); 1270 1271 fprintf(th, "#define Addproc(x) addproc(x"); 1272 for (j = 0; j < Npars; j++) 1273 fprintf(th, ", 0"); 1274 fprintf(th, ")\n"); 1275 } 1276