1 /***** spin: pangen2.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 "pangen2.h" 16 17 #define DELTA 500 /* sets an upperbound on nr of chan names */ 18 19 #define blurb(fd, e) fprintf(fd, "\n\t\t/* %s:%d */\n", \ 20 e->n->fn->name, e->n->ln) 21 #define tr_map(m, e) fprintf(tt, "\t\ttr_2_src(%d, %s, %d);\n", \ 22 m, e->n->fn->name, e->n->ln); 23 24 extern ProcList *rdy; 25 extern RunList *run; 26 extern Symbol *Fname, *oFname, *owner, *context; 27 extern char *claimproc; 28 extern int lineno, Npars, Mpars; 29 extern int m_loss, Nid, has_remote; 30 extern int Ntimeouts, Etimeouts; 31 extern int u_sync, u_async, nrRdy; 32 extern int GenCode, IsGuard, Level, TestOnly; 33 extern char *NextLab[]; 34 35 FILE *tc, *th, *tt, *tm, *tb; 36 int uniq=1; 37 int nocast=0; /* to turn off casts in lvalues */ 38 int terse=0; /* terse printing of varnames */ 39 int no_arrays=0; 40 int has_last=0; /* spec refers to _last */ 41 int has_enabled=0; /* spec contains enabled() */ 42 int has_sorted=0; /* spec contains `!!' (sorted-send) operator */ 43 int has_random=0; /* spec contains `??' (random-recv) operator */ 44 int has_xu=0; /* spec contains xr or xs assertions */ 45 int has_unless=0; /* spec contains unless statements */ 46 int mst=0; /* max nr of state/process */ 47 int claimnr = -1; /* claim process, if any */ 48 int Pid; /* proc currently processed */ 49 int T_sum, T_mus, t_cyc; 50 int TPE[2], EPT[2]; 51 Lextok *Nn[2]; 52 53 void Tpe(Lextok *); 54 55 int 56 fproc(char *s) 57 { ProcList *p; 58 59 for (p = rdy; p; p = p->nxt) 60 if (strcmp(p->n->name, s) == 0) 61 return p->tn; 62 63 fatal("proctype %s not found", s); 64 return -1; 65 } 66 67 void 68 reverse_procs(RunList *q) 69 { 70 if (!q) return; 71 reverse_procs(q->nxt); 72 fprintf(tc, " Addproc(%d);\n", q->tn); 73 } 74 75 void 76 gensrc(void) 77 { ProcList *p; 78 79 if (!(tc = fopen("pan.c", "w")) /* main routines */ 80 || !(th = fopen("pan.h", "w")) /* header file */ 81 || !(tt = fopen("pan.t", "w")) /* transition matrix */ 82 || !(tm = fopen("pan.m", "w")) /* forward moves */ 83 || !(tb = fopen("pan.b", "w"))) /* backward moves */ 84 { printf("spin: cannot create pan.[chtmfb]\n"); 85 exit(1); 86 } 87 fprintf(th, "#define Version \"%s\"\n", Version); 88 fprintf(th, "#define Source \"%s\"\n\n", oFname->name); 89 fprintf(th, "#define uchar unsigned char\n"); 90 fprintf(th, "#define DELTA %d\n", DELTA); 91 fprintf(th, "#if !defined(NFAIR)\n"); 92 fprintf(th, "#define NFAIR 2 /* must be >= 2 */\n"); 93 fprintf(th, "#endif\n"); 94 if (Ntimeouts) 95 fprintf(th, "#define NTIM %d\n", Ntimeouts); 96 if (Etimeouts) 97 fprintf(th, "#define ETIM %d\n", Etimeouts); 98 if (has_remote) 99 fprintf(th, "#define REM_REFS %d\n", has_remote); 100 if (has_last) 101 fprintf(th, "#define HAS_LAST %d\n", has_last); 102 if (has_sorted) 103 fprintf(th, "#define HAS_SORTED %d\n", has_sorted); 104 if (has_random) 105 fprintf(th, "#define HAS_RANDOM %d\n", has_random); 106 if (has_enabled == 0) 107 fprintf(th, "#define INLINE 1\n"); 108 if (has_unless) 109 fprintf(th, "#define HAS_UNLESS %d\n", has_unless); 110 if (claimproc) 111 { claimnr = fproc(claimproc); 112 fprintf(th, "#if !defined(NOCLAIM)\n"); 113 fprintf(th, "#define VERI %d\n", claimnr); 114 fprintf(th, "#endif\n"); 115 fprintf(th, "#define claimline"); 116 fprintf(th, " src_ln%d[((P0 *)pptr(1))->_p]\n", 117 claimnr); 118 } 119 fprintf(th, "#define endclaim endstate%d\n", claimnr); 120 121 fprintf(tc, "/*** Generated by %s ***/\n", Version); 122 fprintf(tc, "/*** From source: %s ***/\n\n", oFname->name); 123 124 ntimes(tc, 0, 1, Preamble); 125 126 fprintf(tc, "#ifndef NOBOUNDCHECK\n"); 127 fprintf(tc, "#define Index(x, y) Boundcheck(x, y, II, tt, t)\n"); 128 fprintf(tc, "#else\n"); 129 fprintf(tc, "#define Index(x, y) x\n"); 130 fprintf(tc, "#endif\n"); 131 132 for (p = rdy; p; p = p->nxt) 133 mst = max(p->s->maxel, mst); 134 135 fprintf(tt, "#ifdef PEG\n"); 136 fprintf(tt, "struct T_SRC {\n"); 137 fprintf(tt, " char *fl; int ln;\n"); 138 fprintf(tt, "} T_SRC[NTRANS];\n\n"); 139 fprintf(tt, "void\ntr_2_src(int m, char *file, int ln)\n"); 140 fprintf(tt, "{ T_SRC[m].fl = file;\n"); 141 fprintf(tt, " T_SRC[m].ln = ln;\n"); 142 fprintf(tt, "}\n\n"); 143 fprintf(tt, "void\nputpeg(int n, int m)\n"); 144 fprintf(tt, "{ printf(\"%%5d\ttrans %%4d file %%s line %%3d\\n\",\n"); 145 fprintf(tt, " m, n, T_SRC[n].fl, T_SRC[n].ln);\n"); 146 fprintf(tt, "}\n"); 147 fprintf(tt, "#else\n"); 148 fprintf(tt, "#define tr_2_src(m,f,l)\n"); 149 fprintf(tt, "#endif\n\n"); 150 151 fprintf(tt, "void\nsettable(void)\n{\tTrans *T;\n"); 152 fprintf(tt, "\tTrans *settr(int,int,int,int,int,char *,int,int,int);\n\n"); 153 fprintf(tt, "\ttrans = (Trans ***) "); 154 fprintf(tt, "emalloc(%d*sizeof(Trans **));\n", nrRdy); 155 156 fprintf(tm, " switch (t->forw) {\n"); 157 fprintf(tm, " default: Uerror(\"bad forward move\");\n"); 158 159 fprintf(tb, " switch (t->back) {\n"); 160 fprintf(tb, " default: Uerror(\"bad return move\");\n"); 161 fprintf(tb, " case 0: goto R999; /* nothing to undo */\n"); 162 163 for (p = rdy; p; p = p->nxt) 164 putproc(p->n, p->s, p->tn, 165 p->s->maxel, 166 p->s->last->seqno); 167 168 fprintf(tt, "}\n\n"); /* end of settable() */ 169 170 fprintf(tm, " }\n\n"); 171 fprintf(tb, " }\n\n"); 172 ntimes(tt, 0, 1, Tail); 173 genheader(); 174 genaddproc(); 175 genother(); 176 genaddqueue(); 177 genunio(); 178 genconditionals(); 179 180 if (!run) fatal("no runable process", (char *)0); 181 182 fprintf(tc, "void\n"); 183 fprintf(tc, "active_procs(void)\n{\n"); 184 reverse_procs(run); 185 fprintf(tc, "}\n"); 186 187 fprintf(th, "#define NTRANS %d\n", uniq); 188 fprintf(th, "#ifdef PEG\n"); 189 fprintf(th, " long peg[NTRANS];\n"); 190 fprintf(th, "#endif\n"); 191 } 192 193 int 194 find_id(Symbol *s) 195 { ProcList *p; 196 197 if (s) 198 for (p = rdy; p; p = p->nxt) 199 if (s == p->n) 200 return p->tn; 201 return 0; 202 } 203 204 void 205 dolen(Symbol *s, char *pre, int pid, int ai, int qln) 206 { 207 if (ai > 0) 208 fprintf(tc, "\n\t\t\t || "); 209 fprintf(tc, "%s(", pre); 210 if (s->context) 211 fprintf(tc, "((P%d *)this)->", pid); 212 else 213 fprintf(tc, "now."); 214 fprintf(tc, "%s", s->name); 215 if (qln > 1) fprintf(tc, "[%d]", ai); 216 fprintf(tc, ")"); 217 } 218 219 struct AA { 220 char TT[9]; char CC[8]; 221 } BB[4] = { 222 { "Q_FULL_F", " q_full" }, 223 { "Q_FULL_T", "!q_full" }, 224 { "Q_EMPT_F", " !q_len" }, 225 { "Q_EMPT_T", " q_len" } 226 }; 227 228 void 229 Done_case(char *nm, Symbol *z) 230 { int j, k; 231 int nid = z->Nid; 232 int qln = z->nel; 233 234 fprintf(tc, "\t\tcase %d: if (", nid); 235 for (j = 0; j < 4; j++) 236 { fprintf(tc, "\t(t->ty[i] == %s && (", BB[j].TT); 237 for (k = 0; k < qln; k++) 238 { if (k > 0) 239 fprintf(tc, "\n\t\t\t || "); 240 fprintf(tc, "%s(%s%s", BB[j].CC, nm, z->name); 241 if (qln > 1) 242 fprintf(tc, "[%d]", k); 243 fprintf(tc, ")"); 244 } 245 fprintf(tc, "))\n\t\t\t "); 246 if (j < 3) 247 fprintf(tc, "|| "); 248 else 249 fprintf(tc, " "); 250 } 251 fprintf(tc, ") return 0; break;\n"); 252 } 253 254 void 255 Docase(Symbol *s, int pid, int nid) 256 { int i, j; 257 258 fprintf(tc, "\t\tcase %d: if (", nid); 259 for (j = 0; j < 4; j++) 260 { fprintf(tc, "\t(t->ty[i] == %s && (", BB[j].TT); 261 for (i = 0; i < s->nel; i++) 262 dolen(s, BB[j].CC, pid, i, s->nel); 263 fprintf(tc, "))\n\t\t\t "); 264 if (j < 3) 265 fprintf(tc, "|| "); 266 else 267 fprintf(tc, " "); 268 } 269 fprintf(tc, ") return 0; break;\n"); 270 } 271 272 void 273 genconditionals(void) 274 { Symbol *s; 275 int last=0, j, i; 276 extern Queue *qtab; 277 extern Symbol *symtab[Nhash+1]; 278 279 fprintf(th, "#define LOCAL 1\n"); 280 fprintf(th, "#define Q_FULL_F 2\n"); 281 fprintf(th, "#define Q_EMPT_F 3\n"); 282 fprintf(th, "#define Q_EMPT_T 4\n"); 283 fprintf(th, "#define Q_FULL_T 5\n"); 284 fprintf(th, "#define TIMEOUT_F 6\n"); 285 fprintf(th, "#define GLOBAL 7\n"); 286 fprintf(th, "#define BAD 8\n"); 287 288 fprintf(tc, "int\n"); 289 fprintf(tc, "q_cond(Trans *t)\n"); 290 fprintf(tc, "{ int i = 0;\n"); 291 fprintf(tc, " for (i = 0; i < 6; i++)\n"); 292 fprintf(tc, " { if (t->ty[i] == TIMEOUT_F) return %s;\n", 293 (Etimeouts)?"(!(trpt->tau&1))":"1"); 294 /* we switch on the chan name from the spec (as identifief by 295 * the corresponding Nid number) rather than the actual qid 296 * because we cannot predict at compile time which specific qid 297 * will be accessed by the statement at runtime. that is: 298 * we do not know which qid to pass to q_cond at runtime 299 * but we do know which name is used. if it's a chan array, we 300 * must check all elements of the array for compliance (bummer) 301 */ 302 fprintf(tc, " switch (t->qu[i]) {\n"); 303 fprintf(tc, " case 0: break;\n"); 304 305 for (i = 0; i <= Nhash; i++) 306 for (s = symtab[i]; s; s = s->next) 307 { if (s->owner) continue; 308 j = find_id(s->context); 309 if (s->type == CHAN) 310 { if (last == s->Nid) continue; /* chan array */ 311 last = s->Nid; 312 Docase(s, j, last); 313 } else if (s->type == STRUCT) 314 { /* struct may contain a chan */ 315 char gather[128]; 316 char pregat[128]; Symbol *z = (Symbol *)0; 317 int nc, ov=0; 318 if (s->context) 319 sprintf(pregat, "((P%d *)this)->%s", 320 j, s->name); 321 else 322 sprintf(pregat, "now.%s", s->name); 323 do { 324 strcpy(gather, pregat); 325 nc = fill_struct(s, 0, ov, gather, &z); 326 if (z && last != z->Nid) 327 { last = z->Nid; 328 if (nc < 0) 329 Done_case(gather, z); 330 } 331 ov = -nc; 332 } while (nc < 0); 333 } 334 } 335 fprintf(tc, " default: Uerror(\"unknown qid - q_cond\");\n"); 336 fprintf(tc, " return 0;\n"); 337 fprintf(tc, " }\n"); 338 fprintf(tc, " }\n"); 339 fprintf(tc, " return 1;\n"); 340 fprintf(tc, "}\n"); 341 } 342 343 void 344 putproc(Symbol *n, Sequence *s, int i, int j, int k) 345 { 346 Pid = i; 347 fprintf(th, "\nshort nstates%d=%d;\t/* %s */\n", i, j, n->name); 348 if (i == claimnr) 349 fprintf(th, "#define nstates_claim nstates%d\n", i); 350 fprintf(th, "#define endstate%d %d\n", i, k); 351 fprintf(tm, "\n /* PROC %s */\n", n->name); 352 fprintf(tb, "\n /* PROC %s */\n", n->name); 353 fprintf(tt, "\n /* proctype %d: %s */\n", i, n->name); 354 fprintf(tt, "\n trans[%d] = (Trans **)", i); 355 fprintf(tt, " emalloc(%d*sizeof(Trans *));\n\n", j); 356 357 put_seq(s, 2, 0); 358 dumpsrc(j, i); 359 } 360 361 void 362 addTpe(int x) 363 { int i; 364 365 if (x <= 2) return; 366 367 for (i = 0; i < T_sum; i++) 368 if (TPE[i] == x) 369 return; 370 TPE[(T_sum++)%2] = x; 371 } 372 373 void 374 cnt_seq(Sequence *s) 375 { Element *f; 376 SeqList *h; 377 378 if (s) 379 for (f = s->frst; ; f = f->nxt) 380 { Tpe(f->n); /* sets EPT */ 381 addTpe(EPT[0]); 382 addTpe(EPT[1]); 383 for (h = f->sub; h; h = h->nxt) 384 cnt_seq(h->this); 385 if (f == s->last) 386 break; 387 } 388 } 389 390 void 391 typ_seq(Sequence *s) 392 { 393 T_sum = 0; 394 TPE[0] = 2; TPE[1] = 0; 395 cnt_seq(s); 396 if (T_sum > 2) /* more than one type */ 397 { TPE[0] = 5*DELTA; /* non-mixing */ 398 TPE[1] = 0; 399 } 400 } 401 402 int 403 hidden(Lextok *n) 404 { 405 if (n) 406 switch (n->ntyp) { 407 case FULL: case EMPTY: 408 case NFULL: case NEMPTY: case TIMEOUT: 409 Nn[(T_mus++)%2] = n; 410 break; 411 case '!': case UMIN: case '~': case ASSERT: case 'c': 412 (void) hidden(n->lft); 413 break; 414 case '/': case '*': case '-': case '+': 415 case '%': case LT: case GT: case '&': 416 case '|': case LE: case GE: case NE: case '?': 417 case EQ: case OR: case AND: case LSHIFT: case RSHIFT: 418 (void) hidden(n->lft); 419 (void) hidden(n->rgt); 420 break; 421 } 422 return T_mus; 423 } 424 425 int 426 valTpe(Lextok *n) 427 { int res = 2; 428 /* 429 2 = local 430 2+1 .. 2+1*DELTA = nfull, 's' - require q_full==false 431 2+1+1*DELTA .. 2+2*DELTA = nempty, 'r' - require q_len!=0 432 2+1+2*DELTA .. 2+3*DELTA = empty - require q_len==0 433 2+1+3*DELTA .. 2+4*DELTA = full - require q_full==true 434 5*DELTA = non-mixing (i.e., always makes the selection global) 435 6*DELTA = timeout (conditionally safe) 436 */ 437 switch (n->ntyp) { 438 case FULL: res += DELTA; /* adds 3*DELTA + chan nr */ 439 case EMPTY: res += DELTA; /* adds 2*DELTA + chan nr */ 440 case 'r': 441 case NEMPTY: res += DELTA; /* adds 1*DELTA + chan nr */ 442 case 's': 443 case NFULL: res += n->sym->Nid; /* add channel nr */ 444 break; 445 446 case TIMEOUT: res = 6*DELTA; 447 default: break; 448 } 449 return res; 450 } 451 452 void 453 Tpe(Lextok *n) /* mixing in selections */ 454 { 455 EPT[0] = 2; EPT[1] = 0; 456 457 if (!n) return; 458 459 T_mus = 0; 460 Nn[0] = Nn[1] = ZN; 461 462 if (n->ntyp == 'c') 463 { if (hidden(n->lft) > 2) 464 { EPT[0] = 5*DELTA; /* non-mixing */ 465 EPT[1] = 0; 466 return; 467 } 468 } else 469 Nn[0] = n; 470 471 if (Nn[0]) EPT[0] = valTpe(Nn[0]); 472 if (Nn[1]) EPT[1] = valTpe(Nn[1]); 473 } 474 475 void 476 put_sub(Element *e, int Tt0, int Tt1) 477 { Sequence *s = e->n->sl->this; 478 int a; 479 480 patch_atomic(s); 481 putskip(s->frst->seqno); 482 a = huntstart(s->frst)->seqno; 483 484 if ((e->n->ntyp == ATOMIC 485 || e->n->ntyp == D_STEP) 486 && scan_seq(s)) 487 mark_seq(s); 488 s->last->nxt = e->nxt; 489 490 typ_seq(s); /* sets TPE */ 491 492 if (e->n->ntyp == D_STEP) 493 { fprintf(tm, "\tcase %d: ", uniq++); 494 fprintf(tm, "/* STATE %d - line %d %s - [", 495 e->seqno, e->n->ln, e->n->fn->name); 496 comment(tm, e->n, 0); 497 fprintf(tm, "] */\n\t\t"); 498 if (e->n && e->n->ntyp != 'r' && Pid != claimnr) 499 fprintf(tm, "IfNotBlocked\n\t\t"); 500 if (!putcode(tm, s, e->nxt, 0)) 501 fprintf(tm, "\t\tm = %d; goto P999;\n\n", 502 getweight(s->frst->n)); 503 504 fprintf(tb, "\tcase %d: ", uniq-1); 505 fprintf(tb, "/* STATE %d */\n", e->seqno); 506 fprintf(tb, "#if defined(FULLSTACK) && defined(NOCOMP)\n"); 507 fprintf(tb, "\t\tsv_restor(!(t->atom&2));\n"); 508 fprintf(tb, "#else\n"); 509 fprintf(tb, "\t\tsv_restor(0);\n"); 510 fprintf(tb, "#endif\n"); 511 fprintf(tb, "\t\tgoto R999;\n"); 512 if (e->nxt) 513 a = huntele(e->nxt, e->status)->seqno; 514 else 515 a = 0; 516 tr_map(uniq-1, e); 517 fprintf(tt, "/*->*/\ttrans[%d][%d]\t= ", 518 Pid, e->seqno); 519 fprintf(tt, "settr(%d,%d,%d,%d,%d,\"", 520 e->Seqno, D_ATOM, a, uniq-1, uniq-1); 521 comment(tt, e->n, e->seqno); 522 fprintf(tt, "\", %d, ", (s->frst->status&I_GLOB)?1:0); 523 fprintf(tt, "%d, %d);", TPE[0], TPE[1]); 524 } else 525 { /* ATOMIC or NON_ATOMIC */ 526 fprintf(tt, "\tT = trans[ %d][%d] = ", Pid, e->seqno); 527 fprintf(tt, "settr(%d,%d,0,0,0,\"", 528 e->Seqno, (e->n->ntyp == ATOMIC)?ATOM:0); 529 comment(tt, e->n, e->seqno); 530 fprintf(tt, "\", %d, %d, %d);", 531 (s->frst->status&I_GLOB)?1:0, Tt0, Tt1); 532 blurb(tt, e); 533 fprintf(tt, "\tT->nxt\t= "); 534 fprintf(tt, "settr(%d,%d,%d,0,0,\"", 535 e->Seqno, (e->n->ntyp == ATOMIC)?ATOM:0, a); 536 comment(tt, e->n, e->seqno); 537 fprintf(tt, "\", %d, ", (s->frst->status&I_GLOB)?1:0); 538 if (e->n->ntyp == NON_ATOMIC) 539 fprintf(tt, "%d, %d);", Tt0, Tt1); 540 else 541 fprintf(tt, "%d, %d);", TPE[0], TPE[1]); 542 blurb(tt, e); 543 544 put_seq(s, TPE[0], TPE[1]); 545 } 546 } 547 548 void 549 put_el(Element *e, int Tt0, int Tt1) 550 { int n, a, Global_ref; 551 SeqList *x; 552 553 #ifdef DEBUG 554 printf("put_el %d (%d) (->%d (%d)) (", e->Seqno, e->seqno, 555 (e->nxt)?e->nxt->Seqno:-1, (e->nxt)?e->nxt->seqno:-1); 556 comment(stdout, e->n, 0); 557 printf(")"); 558 if (e->esc) printf(" - escaped by "); 559 for (x = e->esc; x; x = x->nxt) 560 { printf("%d (", x->this->frst->Seqno); 561 comment(stdout, x->this->frst->n, 0); 562 printf(") "); 563 } 564 printf("\n"); 565 #endif 566 if (e->n->ntyp == GOTO) 567 { Element *g = get_lab(e->n, 1); 568 cross_dsteps(e->n, g->n); 569 a = huntele(g, e->status)->seqno; 570 } else if (e->nxt) 571 a = huntele(e->nxt, e->status)->seqno; 572 else 573 a = 0; 574 575 tr_map(uniq, e); 576 fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno); 577 578 fprintf(tm, "\tcase %d: /* STATE %d - line %d %s - [", 579 uniq++, e->seqno, e->n->ln, e->n->fn->name); 580 comment(tm, e->n, 0); 581 fprintf(tm, "] */\n\t\t"); 582 if (e->n->ntyp != 'r' && Pid != claimnr) 583 fprintf(tm, "IfNotBlocked\n\t\t"); 584 Global_ref = (e->status&I_GLOB)?1:has_global(e->n); 585 586 putstmnt(tm, e->n, e->seqno); 587 n = getweight(e->n); 588 fprintf(tm, ";\n\t\tm = %d; goto P999;\n", n); 589 if (any_undo(e->n)) 590 { fprintf(tb, "\tcase %d: ", uniq-1); 591 fprintf(tb, "/* STATE %d */\n\t\t", e->seqno); 592 if (any_undo(e->n)) 593 undostmnt(e->n, e->seqno); 594 fprintf(tb, ";\n\t\tgoto R999;\n"); 595 fprintf(tt, "settr(%d,%d,%d,%d,%d,\"", 596 e->Seqno, e->status&2, a, uniq-1, uniq-1); 597 } else 598 fprintf(tt, "settr(%d,%d,%d,%d,0,\"", 599 e->Seqno, e->status&2, a, uniq-1); 600 comment(tt, e->n, e->seqno); 601 fprintf(tt, "\", %d, ", Global_ref); 602 if (Tt0 != 2) 603 fprintf(tt, "%d, %d);\n", Tt0, Tt1); 604 else 605 { Tpe(e->n); /* sets EPT */ 606 fprintf(tt, "%d, %d);\n", EPT[0], EPT[1]); 607 } 608 609 if (e->esc && e->n->ntyp != GOTO && e->n->ntyp != '.') 610 { for (x = e->esc, n = 0; x; x = x->nxt, n++) 611 { int i = huntele(x->this->frst, e->status)->seqno; 612 fprintf(tt, "\ttrans[%d][%d]->escp[%d] = %d;\n", 613 Pid, e->seqno, n, i); 614 fprintf(tt, "\treached%d[%d] = 1;\n", 615 Pid, i); 616 } 617 for (x = e->esc, n=0; x; x = x->nxt, n++) 618 { fprintf(tt, " /* escape #%d: %d */\n", 619 n, 620 huntele(x->this->frst, e->status)->seqno); 621 put_seq(x->this, 2, 0); /* args?? */ 622 } 623 fprintf(tt, " /* end-escapes */\n"); 624 } 625 } 626 627 void 628 put_seq(Sequence *s, int Tt0, int Tt1) 629 { SeqList *h; 630 Element *e; 631 int a; 632 633 #ifdef DEBUG 634 printf("put_seq %d - %d [%d] (%d,%d)\n", 635 s->frst->Seqno, 636 s->last->Seqno, 637 s->extent->Seqno, 638 Tt0, Tt1); 639 #endif 640 for (e = s->frst; e; e = e->nxt) 641 { 642 #ifdef DEBUG 643 printf("put_seq %d (%d) (; %d (%d)) ", e->Seqno, e->seqno, 644 e->nxt?e->nxt->Seqno:-1, e->nxt?e->nxt->seqno:-1); 645 comment(stdout, e->n, 0); 646 printf(" (%s)\n", (e->status & DONE)?"done":"new"); 647 #endif 648 if (e->status & DONE) continue; 649 650 e->status |= DONE; 651 652 if (e->n->ln) 653 putsrc(e->n->ln, e->seqno); 654 655 if (e->n->ntyp == UNLESS) 656 { 657 #ifdef DEBUG 658 printf("\t(unless) %d\n", e->sub->this->frst->seqno); 659 #endif 660 put_seq(e->sub->this, Tt0, Tt1); 661 } else if (e->sub) 662 { fprintf(tt, "\tT = trans[%d][%d] = ", Pid, e->seqno); 663 fprintf(tt, "settr(%d,%d,0,0,0,\"", 664 e->Seqno, e->status&2); 665 comment(tt, e->n, e->seqno); 666 fprintf(tt, "\", %d, %d, %d);", 667 (e->status&I_GLOB)?1:0, Tt0, Tt1); 668 blurb(tt, e); 669 for (h = e->sub; h; h = h->nxt) 670 { putskip(h->this->frst->seqno); 671 a = huntstart(h->this->frst)->seqno; 672 if (h->nxt) 673 fprintf(tt, "\tT = T->nxt\t= "); 674 else 675 fprintf(tt, "\t T->nxt\t= "); 676 fprintf(tt, "settr(%d,%d,%d,0,0,\"", 677 e->Seqno, e->status&2, a); 678 comment(tt, e->n, e->seqno); 679 fprintf(tt, "\", %d, %d, %d);", 680 (h->this->frst->status&I_GLOB)?1:0, Tt0, Tt1); 681 blurb(tt, e); 682 } 683 for (h = e->sub; h; h = h->nxt) 684 put_seq(h->this, Tt0, Tt1); 685 } else 686 { if (e->n->ntyp == ATOMIC 687 || e->n->ntyp == D_STEP 688 || e->n->ntyp == NON_ATOMIC) 689 put_sub(e, Tt0, Tt1); 690 else 691 put_el(e, Tt0, Tt1); 692 } 693 if (e == s->last) 694 break; 695 } 696 } 697 698 void 699 patch_atomic(Sequence *s) /* catch goto's that break the chain */ 700 { Element *f, *g; 701 SeqList *h; 702 703 for (f = s->frst; ; f = f->nxt) 704 { if (f->n && f->n->ntyp == GOTO) 705 { g = get_lab(f->n,1); 706 cross_dsteps(f->n, g->n); 707 if ((f->status & (ATOM|L_ATOM)) 708 && !(g->status & (ATOM|L_ATOM))) 709 { f->status &= ~ATOM; 710 f->status |= L_ATOM; 711 } 712 } else 713 for (h = f->sub; h; h = h->nxt) 714 patch_atomic(h->this); 715 if (f == s->extent) 716 break; 717 } 718 } 719 720 void 721 mark_seq(Sequence *s) 722 { Element *f; 723 SeqList *h; 724 725 for (f = s->frst; ; f = f->nxt) 726 { f->status |= I_GLOB; 727 for (h = f->sub; h; h = h->nxt) 728 mark_seq(h->this); 729 if (f == s->last) 730 return; 731 } 732 } 733 734 Element * 735 find_target(Element *e) 736 { Element *f; 737 738 if (!e) return e; 739 740 if (t_cyc++ > 32) 741 { fatal("cycle of goto jumps", (char *) 0); 742 } 743 switch (e->n->ntyp) { 744 case GOTO: 745 f = get_lab(e->n,1); 746 cross_dsteps(e->n, f->n); 747 f = find_target(f); 748 break; 749 case BREAK: 750 if (e->nxt) 751 f = find_target(huntele(e->nxt, e->status)); 752 /* else fall through */ 753 default: 754 f = e; 755 break; 756 } 757 return f; 758 } 759 760 Element * 761 target(Element *e) 762 { 763 if (!e) return e; 764 lineno = e->n->ln; 765 Fname = e->n->fn; 766 t_cyc = 0; 767 return find_target(e); 768 } 769 770 int 771 scan_seq(Sequence *s) 772 { Element *f, *g; 773 SeqList *h; 774 775 for (f = s->frst; ; f = f->nxt) 776 { if (has_global(f->n)) 777 return 1; 778 if (f->n->ntyp == GOTO) /* may reach other atomic */ 779 { g = target(f); 780 if (g 781 && !(f->status & L_ATOM) 782 && !(g->status & (ATOM|L_ATOM))) 783 { fprintf(tt, " /* goto mark-down, "); 784 fprintf(tt, "line %d - %d */\n", 785 f->n->ln, (g->n)?g->n->ln:0); 786 return 1; /* assume worst case */ 787 } } 788 for (h = f->sub; h; h = h->nxt) 789 if (scan_seq(h->this)) 790 return 1; 791 if (f == s->last) 792 break; 793 } 794 return 0; 795 } 796 797 int 798 has_global(Lextok *n) 799 { Lextok *v; 800 801 if (!n) return 0; 802 switch (n->ntyp) { 803 case '.': case BREAK: case GOTO: case CONST: 804 case RUN: case '@': case TIMEOUT: 805 return 0; 806 807 case ELSE: return n->val; /* true if Probe's appear in other guards */ 808 809 case NAME: return (n->sym->context)?0:1; 810 811 case 's': return ((n->sym->xu&(XS|XX)) != XS); 812 case 'r': return ((n->sym->xu&(XR|XX)) != XR); 813 case NEMPTY: return ((n->sym->xu&(XR|XX)) != XR); 814 case NFULL: return ((n->sym->xu&(XS|XX)) != XS); 815 case FULL: return ((n->sym->xu&(XR|XX)) != XR); 816 case EMPTY: return ((n->sym->xu&(XS|XX)) != XS); 817 case LEN: 818 case 'R': return (((n->sym->xu)&(XR|XS|XX)) != (XR|XS)); 819 820 case ENABLED: case PC_VAL: 821 case 'p': case 'q': 822 return 1; 823 824 case '!': case UMIN: case '~': case ASSERT: 825 return has_global(n->lft); 826 827 case '/': case '*': case '-': case '+': 828 case '%': case LT: case GT: case '&': 829 case '|': case LE: case GE: case NE: case '?': 830 case EQ: case OR: case AND: case LSHIFT: 831 case RSHIFT: case 'c': case ASGN: 832 return has_global(n->lft) || has_global(n->rgt); 833 834 case PRINT: 835 for (v = n->lft; v; v = v->rgt) 836 if (has_global(v->lft)) return 1; 837 return 0; 838 } 839 return 0; 840 } 841 842 void 843 Bailout(FILE *fd, char *str) 844 { 845 if (!GenCode) 846 fprintf(fd, "continue%s", str); 847 else if (IsGuard) 848 fprintf(fd, "%s%s", NextLab[Level], str); 849 else 850 fprintf(fd, "Uerror(\"block in step seq\")%s", str); 851 } 852 853 #define cat0(x) putstmnt(fd,now->lft,m); fprintf(fd, x); \ 854 putstmnt(fd,now->rgt,m) 855 #define cat1(x) fprintf(fd,"("); cat0(x); fprintf(fd,")") 856 #define cat2(x,y) fprintf(fd,x); putstmnt(fd,y,m) 857 #define cat3(x,y,z) fprintf(fd,x); putstmnt(fd,y,m); fprintf(fd,z) 858 859 void 860 putstmnt(FILE *fd, Lextok *now, int m) 861 { Lextok *v; 862 int i, j; 863 864 if (!now) { fprintf(fd, "0"); return; } 865 lineno = now->ln; 866 Fname = now->fn; 867 switch (now->ntyp) { 868 case CONST: fprintf(fd, "%d", now->val); break; 869 case '!': cat3(" !(", now->lft, ")"); break; 870 case UMIN: cat3(" -(", now->lft, ")"); break; 871 case '~': cat3(" ~(", now->lft, ")"); break; 872 873 case '/': cat1("/"); break; 874 case '*': cat1("*"); break; 875 case '-': cat1("-"); break; 876 case '+': cat1("+"); break; 877 case '%': cat1("%%"); break; 878 case '&': cat1("&"); break; 879 case '|': cat1("|"); break; 880 case LT: cat1("<"); break; 881 case GT: cat1(">"); break; 882 case LE: cat1("<="); break; 883 case GE: cat1(">="); break; 884 case NE: cat1("!="); break; 885 case EQ: cat1("=="); break; 886 case OR: cat1("||"); break; 887 case AND: cat1("&&"); break; 888 case LSHIFT: cat1("<<"); break; 889 case RSHIFT: cat1(">>"); break; 890 891 case TIMEOUT: fprintf(fd, "((trpt->tau)&1)"); 892 break; 893 894 case RUN: if (claimproc 895 && strcmp(now->sym->name, claimproc) == 0) 896 fatal("%s is claim, not runnable", claimproc); 897 fprintf(fd,"addproc(%d", fproc(now->sym->name)); 898 for (v = now->lft, i = 0; v; v = v->rgt, i++) 899 { cat2(", ", v->lft); 900 } 901 for ( ; i < Npars; i++) 902 fprintf(fd, ", 0"); 903 fprintf(fd, ")"); 904 break; 905 906 case ENABLED: cat3("enabled(II, ", now->lft, ")"); 907 break; 908 909 case PC_VAL: cat3("((P0 *) Pptr(", now->lft, "+BASE))->_p"); 910 break; 911 912 case LEN: if (!terse && !TestOnly && has_xu) 913 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 914 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || "); 915 putname(fd, "q_R_check(", now->lft, m, ", II)) &&\n\t\t"); 916 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || "); 917 putname(fd, "q_S_check(", now->lft, m, ", II)) &&"); 918 fprintf(fd, "\n#endif\n\t\t"); 919 } 920 putname(fd, "q_len(", now->lft, m, ")"); 921 break; 922 923 case FULL: if (!terse && !TestOnly && has_xu) 924 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 925 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || "); 926 putname(fd, "q_R_check(", now->lft, m, ", II)) &&\n\t\t"); 927 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || "); 928 putname(fd, "q_S_check(", now->lft, m, ", II)) &&"); 929 fprintf(fd, "\n#endif\n\t\t"); 930 } 931 putname(fd, "q_full(", now->lft, m, ")"); 932 break; 933 934 case EMPTY: if (!terse && !TestOnly && has_xu) 935 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 936 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || "); 937 putname(fd, "q_R_check(", now->lft, m, ", II)) &&\n\t\t"); 938 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || "); 939 putname(fd, "q_S_check(", now->lft, m, ", II)) &&"); 940 fprintf(fd, "\n#endif\n\t\t"); 941 } 942 putname(fd, "(q_len(", now->lft, m, ")==0)"); 943 break; 944 945 case NFULL: if (!terse && !TestOnly && has_xu) 946 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 947 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || "); 948 putname(fd, "q_S_check(", now->lft, m, ", II)) &&"); 949 fprintf(fd, "\n#endif\n\t\t"); 950 } 951 putname(fd, "(!q_full(", now->lft, m, "))"); 952 break; 953 954 case NEMPTY: if (!terse && !TestOnly && has_xu) 955 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 956 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || "); 957 putname(fd, "q_R_check(", now->lft, m, ", II)) &&"); 958 fprintf(fd, "\n#endif\n\t\t"); 959 } 960 putname(fd, "(q_len(", now->lft, m, ")>0)"); 961 break; 962 963 case 's': if (TestOnly) 964 { if (m_loss) 965 fprintf(fd, "1"); 966 else 967 putname(fd, "!q_full(", now->lft, m, ")"); 968 break; 969 } 970 if (has_xu) 971 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 972 putname(fd, "if (q_claim[", now->lft, m, "]&2) "); 973 putname(fd, "q_S_check(", now->lft, m, ", II);"); 974 fprintf(fd, "\n#endif\n\t\t"); 975 } 976 fprintf(fd, "if (q_%s", 977 (u_sync > 0 && u_async == 0)?"len":"full"); 978 putname(fd, "(", now->lft, m, "))\n"); 979 980 if (m_loss) 981 { if (!GenCode) 982 fprintf(fd, "\t\t{ nlost++; m=3; goto P999; }\n"); 983 else 984 fprintf(fd, "\t\t\tnlost++;\n\t\telse {"); 985 } else 986 { fprintf(fd, "\t\t\t"); 987 Bailout(fd, ";"); 988 } 989 990 if (has_enabled) 991 fprintf(fd, "\n\t\tif (TstOnly) return 1;"); 992 993 putname(fd, "\n\t\tqsend(", now->lft, m, ""); 994 fprintf(fd, ", %d", now->val); 995 for (v = now->rgt, i = 0; v; v = v->rgt, i++) 996 { cat2(", ", v->lft); 997 } 998 if (i > Mpars) 999 fatal("too many pars in send", ""); 1000 for ( ; i < Mpars; i++) 1001 fprintf(fd, ", 0"); 1002 fprintf(fd, ")"); 1003 if (u_sync) 1004 { fprintf(fd, ";\n\t\t"); 1005 if (u_async == 0) 1006 putname(fd, "boq = ", now->lft, m, ""); 1007 else 1008 { putname(fd, "if (q_zero(", now->lft, m, ")) "); 1009 putname(fd, "boq = ", now->lft, m, ""); 1010 } } 1011 if (m_loss && GenCode) 1012 fprintf(fd, ";\n\t\t}\n\t\t"); 1013 break; 1014 1015 case 'r': if (TestOnly) 1016 { fprintf(fd, "(("); 1017 if (u_sync) 1018 fprintf(fd, "(boq == -1 && "); 1019 putname(fd, "q_len(", now->lft, m, ")"); 1020 if (u_sync) 1021 { putname(fd, ") || (boq == ", now->lft,m," && "); 1022 putname(fd, "q_zero(", now->lft,m,"))"); 1023 } 1024 fprintf(fd, ")"); 1025 if (now->val == 0) 1026 { for (v = now->rgt, i=j=0; v; v = v->rgt, i++) 1027 { if (v->lft->ntyp != CONST) 1028 { j++; continue; 1029 } 1030 cat3("\n\t\t&& (", v->lft, " == "); 1031 putname(fd, "qrecv(", now->lft, m, ", "); 1032 fprintf(fd, "0, %d, 0))", i); 1033 } 1034 fprintf(fd, ")"); 1035 } else 1036 { putname(fd, "\n\t\t&& Q_has(", now->lft, m, ""); 1037 for (v = now->rgt, i=0; v; v = v->rgt, i++) 1038 { if (v->lft->ntyp != CONST) 1039 fprintf(fd, ", 0, 0"); 1040 else 1041 { fprintf(fd, ", 1, "); 1042 putstmnt(fd, v->lft, m); 1043 } } 1044 for ( ; i < Mpars; i++) 1045 fprintf(fd, ", 0, 0"); 1046 fprintf(fd, "))"); 1047 } 1048 break; 1049 } 1050 if (has_xu) 1051 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 1052 putname(fd, "if (q_claim[", now->lft, m, "]&1) "); 1053 putname(fd, "q_R_check(", now->lft, m, ", II);"); 1054 fprintf(fd, "\n#endif\n\t\t"); 1055 } 1056 if (u_sync) 1057 { fprintf(fd, "if ("); 1058 if (u_async == 0) 1059 putname(fd, "boq != ", now->lft,m,") "); 1060 else 1061 { putname(fd, "q_zero(", now->lft,m,"))"); 1062 fprintf(fd, "\n\t\t"); 1063 putname(fd, "{ if (boq != ", now->lft,m,") "); 1064 Bailout(fd, ";\n\t\t} else\n\t\t"); 1065 fprintf(fd, "{ if (boq != -1) "); 1066 } 1067 Bailout(fd, ";\n\t\t"); 1068 if (u_async) 1069 fprintf(fd, "}\n\t\t"); 1070 } 1071 putname(fd, "if (q_len(", now->lft, m, ") == 0) "); 1072 Bailout(fd, ""); 1073 1074 for (v = now->rgt, j=0; v; v = v->rgt) 1075 { if (v->lft->ntyp != CONST) 1076 j++; /* count settables */ 1077 } 1078 fprintf(fd, ";\n\t{\n\t\tint XX=1"); 1079 /* test */ if (now->val == 0) 1080 { for (v = now->rgt, i=0; v; v = v->rgt, i++) 1081 { if (v->lft->ntyp != CONST) 1082 continue; 1083 fprintf(fd, ";\n\t\t"); 1084 cat3("if (", v->lft, " != "); 1085 putname(fd, "qrecv(", now->lft, m, ", "); 1086 fprintf(fd, "0, %d, 0)) ", i); 1087 Bailout(fd, ""); 1088 } 1089 } else 1090 { putname(fd, ";\n\t\tif (!(XX = Q_has(", now->lft, m, ""); 1091 for (v = now->rgt, i=0; v; v = v->rgt, i++) 1092 { if (v->lft->ntyp != CONST) 1093 fprintf(fd, ", 0, 0"); 1094 else 1095 { fprintf(fd, ", 1, "); 1096 putstmnt(fd, v->lft, m); 1097 } } 1098 for ( ; i < Mpars; i++) 1099 fprintf(fd, ", 0, 0"); 1100 fprintf(fd, "))) "); 1101 Bailout(fd, ""); 1102 } 1103 1104 if (has_enabled) 1105 fprintf(fd, ";\n\t\tif (TstOnly) return 1"); 1106 1107 if (!GenCode) 1108 { fprintf(fd, ";\n"); 1109 if (j > 0) 1110 { fprintf(fd, "#if defined(FULLSTACK) && defined(NOCOMP)\n"); 1111 fprintf(fd, "\t\tif (t->atom&2)\n"); 1112 fprintf(fd, "#endif\n"); 1113 } else 1114 { fprintf(fd, "\t\tif (q_flds"); 1115 putname(fd, "[((Q0 *)qptr(", now->lft, m, "-1))->_t]"); 1116 fprintf(fd, " != %d)\n", i); 1117 fprintf(fd, "#if defined(FULLSTACK) && defined(NOCOMP)\n"); 1118 fprintf(fd, "\t\tif (t->atom&2)\n"); 1119 fprintf(fd, "#endif\n"); 1120 } 1121 fprintf(fd, "\t\t\tsv_save((char *)&now)"); 1122 } 1123 /* set */ for (v = now->rgt, i = 0; v; v = v->rgt, i++) 1124 { if (v->lft->ntyp == CONST && v->rgt) 1125 continue; 1126 fprintf(fd, ";\n\t\t"); 1127 if (v->lft->ntyp != CONST) 1128 { nocast=1; 1129 putstmnt(fd, v->lft, m); 1130 nocast=0; fprintf(fd, " = "); 1131 } 1132 putname(fd, "qrecv(", now->lft, m, ", "); 1133 fprintf(fd, "XX-1, %d, ", i); 1134 fprintf(fd, "%d)", (v->rgt)?0:1); 1135 } 1136 fprintf(fd, ";\n\t}\n\t\t"); 1137 if (u_sync) 1138 { putname(fd, "\t\tif (q_zero(", now->lft, m, ""); 1139 fprintf(fd, ")) boq = -1"); 1140 } 1141 break; 1142 1143 case 'R': if (!terse && !TestOnly && has_xu) 1144 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 1145 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || "); 1146 putname(fd, "q_R_check(", now->lft, m, ", II)) &&\n\t\t"); 1147 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || "); 1148 putname(fd, "q_S_check(", now->lft, m, ", II)) &&"); 1149 fprintf(fd, "\n#endif\n\t\t"); 1150 } 1151 1152 if (u_sync>0) 1153 putname(fd, "not_RV(", now->lft, m, ") &&\n\t\t"); 1154 1155 for (v = now->rgt, i=j=0; v; v = v->rgt, i++) 1156 if (v->lft->ntyp != CONST) 1157 { j++; continue; 1158 } 1159 if (now->val == 0 || i == j) 1160 { putname(fd, "(q_len(", now->lft, m, ") > 0"); 1161 for (v = now->rgt, i=0; v; v = v->rgt, i++) 1162 { if (v->lft->ntyp != CONST) 1163 continue; 1164 fprintf(fd, " \\\n\t\t&& qrecv("); 1165 putname(fd, "", now->lft, m, ", "); 1166 fprintf(fd, "0, %d, 0) == ", i); 1167 putstmnt(fd, v->lft, m); 1168 } 1169 fprintf(fd, ")"); 1170 } else 1171 { putname(fd, "Q_has(", now->lft, m, ""); 1172 for (v = now->rgt, i=0; v; v = v->rgt, i++) 1173 { if (v->lft->ntyp != CONST) 1174 fprintf(fd, ", 0, 0"); 1175 else 1176 { fprintf(fd, ", 1, "); 1177 putstmnt(fd, v->lft, m); 1178 } } 1179 for ( ; i < Mpars; i++) 1180 fprintf(fd, ", 0, 0"); 1181 fprintf(fd, ")"); 1182 } 1183 break; 1184 1185 case 'c': cat3("if (!(", now->lft, "))\n\t\t\t"); 1186 Bailout(fd, ""); 1187 break; 1188 case ELSE: 1189 if (!GenCode) 1190 fprintf(fd, "if (trpt->o_pm&1)\n\t\t\t"); 1191 else 1192 fprintf(fd, "/* else */ "); 1193 Bailout(fd, ""); 1194 break; 1195 1196 case '?': cat3("( (", now->lft, ") ? "); 1197 cat3("(", now->rgt->lft, ") : "); 1198 cat3("(", now->rgt->rgt, ") )"); 1199 break; 1200 1201 case ASGN: 1202 if (has_enabled) 1203 fprintf(fd, "if (TstOnly) return 1;\n\t\t"); 1204 1205 if (!GenCode) 1206 { cat3("(trpt+1)->oval = ", now->lft, ";\n\t\t"); 1207 } 1208 nocast = 1; putstmnt(fd,now->lft,m); nocast = 0; 1209 fprintf(fd," = "); 1210 putstmnt(fd,now->rgt,m); 1211 break; 1212 1213 case PRINT: 1214 if (has_enabled) 1215 fprintf(fd, "if (TstOnly) return 1;\n\t\t"); 1216 1217 fprintf(fd, "printf(%s", now->sym->name); 1218 for (v = now->lft; v; v = v->rgt) 1219 { cat2(", ", v->lft); 1220 } 1221 fprintf(fd, ")"); 1222 break; 1223 1224 case NAME: if (!nocast && now->sym && Sym_typ(now) < SHORT) 1225 putname(fd, "((int)", now, m, ")"); 1226 else 1227 putname(fd, "", now, m, ""); 1228 break; 1229 1230 case 'p': putremote(fd, now, m); 1231 break; 1232 1233 case 'q': if (terse) 1234 fprintf(fd, "%s", now->sym->name); 1235 else 1236 fprintf(fd, "%d", remotelab(now)); 1237 break; 1238 1239 case ASSERT: 1240 if (has_enabled) 1241 fprintf(fd, "if (TstOnly) return 1;\n\t\t"); 1242 1243 cat3("assert(", now->lft, ", "); 1244 terse = nocast = 1; 1245 cat3("\"", now->lft, "\", II, tt, t)"); 1246 terse = nocast = 0; 1247 break; 1248 case '.': 1249 case BREAK: 1250 case GOTO: putskip(m); 1251 break; 1252 case '@': 1253 if (has_enabled) 1254 fprintf(fd, "if (TstOnly) return (II+1 == now._nr_pr);\n\t\t"); 1255 1256 fprintf(fd, "if (!delproc(1, II)) "); 1257 Bailout(fd, ""); 1258 break; 1259 1260 default : printf("spin: bad node type %d (.m)\n", now->ntyp); 1261 exit(1); 1262 } 1263 } 1264 1265 void 1266 putname(FILE *fd, char *pre, Lextok *n, int m, char *suff) /* varref */ 1267 { Symbol *s = n->sym; 1268 lineno = n->ln; Fname = n->fn; 1269 1270 if (!s) 1271 fatal("no name - putname", ""); 1272 if (s->context && context && s->type) 1273 s = findloc(s); /* it's a local var */ 1274 1275 if (!s) 1276 { fprintf(fd, "%s%s%s", pre, n->sym->name, suff); 1277 return; 1278 } 1279 1280 if (!s->type) /* not a local name */ 1281 s = lookup(s->name); /* must be a global */ 1282 1283 if (!s->type) 1284 { if (strcmp(pre, ".") != 0) 1285 non_fatal("undeclared variable '%s'", s->name); 1286 s->type = INT; 1287 } 1288 1289 if (s->type == PROCTYPE) 1290 fatal("proctype-name '%s' used as array-name", s->name); 1291 1292 fprintf(fd, pre); 1293 if (!terse && !s->owner) 1294 { if (s->context 1295 || strcmp(s->name, "_p") == 0 1296 || strcmp(s->name, "_pid") == 0) 1297 { fprintf(fd, "((P%d *)this)->", Pid); 1298 } else 1299 { if (!s->hidden) fprintf(fd, "now."); 1300 } } 1301 fprintf(fd, "%s", s->name); 1302 1303 if (s->nel != 1) 1304 { if (no_arrays) 1305 { 1306 non_fatal("ref to array element is invalid in this context", 1307 (char *)0); 1308 printf("\thint: instead of, for instance, x[rs] qu[3], use\n"); 1309 printf("\tchan nm_3 = qu[3]; x[rs] nm_3;\n"); 1310 printf("\tand use nm_3 in all sends/recvs instead of qu[3]\n"); 1311 } 1312 /* an xr or xs reference to an array element 1313 * becomes an exclusion tag on the array itself - 1314 * which could result in invalidly labeling 1315 * operations on other elements of this array to 1316 * be also safe under the partial order reduction 1317 * (see procedure has_global()) 1318 */ 1319 if (terse 1320 || (n->lft 1321 && n->lft->ntyp == CONST 1322 && n->lft->val < s->nel) 1323 || (!n->lft && s->nel > 0)) 1324 { cat3("[", n->lft, "]"); 1325 } else 1326 { cat3("[ Index(", n->lft, ", "); 1327 fprintf(fd, "%d) ]", s->nel); 1328 } 1329 } 1330 if (s->type == STRUCT && n->rgt && n->rgt->lft) 1331 { putname(fd, ".", n->rgt->lft, m, ""); 1332 } 1333 fprintf(fd, suff); 1334 } 1335 1336 void 1337 putremote(FILE *fd, Lextok *n, int m) /* remote reference */ 1338 { int promoted = 0; 1339 1340 if (terse) 1341 { fprintf(fd, "%s[", n->lft->sym->name); 1342 putstmnt(fd, n->lft->lft, m); 1343 if (strcmp(n->sym->name, "_p") == 0) 1344 fprintf(fd, "]:"); 1345 else 1346 fprintf(fd, "].%s", n->sym->name); 1347 } else 1348 { if (Sym_typ(n) < SHORT) 1349 { promoted = 1; 1350 fprintf(fd, "((int)"); 1351 } 1352 fprintf(fd, "((P%d *)Pptr(", 1353 fproc(n->lft->sym->name)); 1354 if (claimproc) fprintf(fd, "1+"); 1355 putstmnt(fd, n->lft->lft, m); 1356 fprintf(fd, "))->%s", n->sym->name); 1357 } 1358 if (n->rgt) 1359 { fprintf(fd, "["); 1360 putstmnt(fd, n->rgt, m); 1361 fprintf(fd, "]"); 1362 } 1363 if (promoted) fprintf(fd, ")"); 1364 } 1365 1366 int 1367 getweight(Lextok *n) 1368 { 1369 switch (n->ntyp) { 1370 case 'r': return 4; 1371 case 's': return 2; 1372 case TIMEOUT: return 1; /* lowest priority */ 1373 case 'c': if (has_typ(n->lft, TIMEOUT)) return 1; 1374 } 1375 return 3; 1376 } 1377 1378 int 1379 has_typ(Lextok *n, int m) 1380 { 1381 if (!n) return 0; 1382 if (n->ntyp == m) return 1; 1383 return (has_typ(n->lft, m) || has_typ(n->rgt, m)); 1384 } 1385