1 /***** spin: pangen2.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 "version.h" 14 #ifdef PC 15 #include "y_tab.h" 16 #else 17 #include "y.tab.h" 18 #endif 19 #include "pangen2.h" 20 #include "pangen4.h" 21 #include "pangen5.h" 22 23 #define DELTA 500 /* sets an upperbound on nr of chan names */ 24 25 #define blurb(fd, e) { fprintf(fd, "\n"); if (!merger) fprintf(fd, "\t\t/* %s:%d */\n", \ 26 e->n->fn->name, e->n->ln); } 27 #define tr_map(m, e) { if (!merger) fprintf(tt, "\t\ttr_2_src(%d, %s, %d);\n", \ 28 m, e->n->fn->name, e->n->ln); } 29 30 extern ProcList *rdy; 31 extern RunList *run; 32 extern Symbol *Fname, *oFname, *context; 33 extern char *claimproc, *eventmap; 34 extern int lineno, verbose, Npars, Mpars; 35 extern int m_loss, has_remote, has_remvar, merger, rvopt, separate; 36 extern int Ntimeouts, Etimeouts, deadvar; 37 extern int u_sync, u_async, nrRdy; 38 extern int GenCode, IsGuard, Level, TestOnly; 39 extern short has_stack; 40 extern char *NextLab[]; 41 42 FILE *tc, *th, *tt, *tm, *tb; 43 44 int OkBreak = -1; 45 short nocast=0; /* to turn off casts in lvalues */ 46 short terse=0; /* terse printing of varnames */ 47 short no_arrays=0; 48 short has_last=0; /* spec refers to _last */ 49 short has_badelse=0; /* spec contains else combined with chan refs */ 50 short has_enabled=0; /* spec contains enabled() */ 51 short has_pcvalue=0; /* spec contains pc_value() */ 52 short has_np=0; /* spec contains np_ */ 53 short has_sorted=0; /* spec contains `!!' (sorted-send) operator */ 54 short has_random=0; /* spec contains `??' (random-recv) operator */ 55 short has_xu=0; /* spec contains xr or xs assertions */ 56 short has_unless=0; /* spec contains unless statements */ 57 short has_provided=0; /* spec contains PROVIDED clauses on procs */ 58 short has_code=0; /* spec contains c_code, c_expr, c_state */ 59 short _isok=0; /* checks usage of predefined variable _ */ 60 short evalindex=0; /* evaluate index of var names */ 61 short withprocname=0; /* prefix local varnames with procname */ 62 int mst=0; /* max nr of state/process */ 63 int claimnr = -1; /* claim process, if any */ 64 int eventmapnr = -1; /* event trace, if any */ 65 int Pid; /* proc currently processed */ 66 int multi_oval; /* set in merges, used also in pangen4.c */ 67 68 #define MAXMERGE 256 /* max nr of bups per merge sequence */ 69 70 static short CnT[MAXMERGE]; 71 static Lextok XZ, YZ[MAXMERGE]; 72 static int didcase, YZmax, YZcnt; 73 74 static Lextok *Nn[2]; 75 static int Det; /* set if deterministic */ 76 static int T_sum, T_mus, t_cyc; 77 static int TPE[2], EPT[2]; 78 static int uniq=1; 79 static int multi_needed, multi_undo; 80 static short AllGlobal=0; /* set if process has provided clause */ 81 82 int has_global(Lextok *); 83 static int getweight(Lextok *); 84 static int scan_seq(Sequence *); 85 static void genconditionals(void); 86 static void mark_seq(Sequence *); 87 static void patch_atomic(Sequence *); 88 static void put_seq(Sequence *, int, int); 89 static void putproc(ProcList *); 90 static void Tpe(Lextok *); 91 extern void spit_recvs(FILE *, FILE*); 92 93 static int 94 fproc(char *s) 95 { ProcList *p; 96 97 for (p = rdy; p; p = p->nxt) 98 if (strcmp(p->n->name, s) == 0) 99 return p->tn; 100 101 fatal("proctype %s not found", s); 102 return -1; 103 } 104 105 static void 106 reverse_procs(RunList *q) 107 { 108 if (!q) return; 109 reverse_procs(q->nxt); 110 fprintf(tc, " Addproc(%d);\n", q->tn); 111 } 112 113 static void 114 tm_predef_np(void) 115 { 116 fprintf(th, "#define _T5 %d\n", uniq++); 117 fprintf(th, "#define _T2 %d\n", uniq++); 118 fprintf(tm, "\tcase _T5:\t/* np_ */\n"); 119 120 if (separate == 2) 121 fprintf(tm, "\t\tif (!((!(o_pm&4) && !(tau&128))))\n"); 122 else 123 fprintf(tm, "\t\tif (!((!(trpt->o_pm&4) && !(trpt->tau&128))))\n"); 124 125 fprintf(tm, "\t\t\tcontinue;\n"); 126 fprintf(tm, "\t\t/* else fall through */\n"); 127 fprintf(tm, "\tcase _T2:\t/* true */\n"); 128 fprintf(tm, "\t\t_m = 3; goto P999;\n"); 129 } 130 131 static void 132 tt_predef_np(void) 133 { 134 fprintf(tt, "\t/* np_ demon: */\n"); 135 fprintf(tt, "\ttrans[_NP_] = "); 136 fprintf(tt, "(Trans **) emalloc(2*sizeof(Trans *));\n"); 137 fprintf(tt, "\tT = trans[_NP_][0] = "); 138 fprintf(tt, "settr(9997,0,1,_T5,0,\"(np_)\", 1,2,0);\n"); 139 fprintf(tt, "\t T->nxt = "); 140 fprintf(tt, "settr(9998,0,0,_T2,0,\"(1)\", 0,2,0);\n"); 141 fprintf(tt, "\tT = trans[_NP_][1] = "); 142 fprintf(tt, "settr(9999,0,1,_T5,0,\"(np_)\", 1,2,0);\n"); 143 } 144 145 static struct { 146 char *nm[3]; 147 } Cfile[] = { 148 { { "pan.c", "pan_s.c", "pan_t.c" } }, 149 { { "pan.h", "pan_s.h", "pan_t.h" } }, 150 { { "pan.t", "pan_s.t", "pan_t.t" } }, 151 { { "pan.m", "pan_s.m", "pan_t.m" } }, 152 { { "pan.b", "pan_s.b", "pan_t.b" } } 153 }; 154 155 void 156 gensrc(void) 157 { ProcList *p; 158 159 if (!(tc = fopen(Cfile[0].nm[separate], "w")) /* main routines */ 160 || !(th = fopen(Cfile[1].nm[separate], "w")) /* header file */ 161 || !(tt = fopen(Cfile[2].nm[separate], "w")) /* transition matrix */ 162 || !(tm = fopen(Cfile[3].nm[separate], "w")) /* forward moves */ 163 || !(tb = fopen(Cfile[4].nm[separate], "w"))) /* backward moves */ 164 { printf("spin: cannot create pan.[chtmfb]\n"); 165 alldone(1); 166 } 167 168 fprintf(th, "#define Version \"%s\"\n", Version); 169 fprintf(th, "#define Source \"%s\"\n\n", oFname->name); 170 if (separate != 2) 171 fprintf(th, "char *TrailFile = Source; /* default */\n"); 172 173 fprintf(th, "#if defined(BFS)\n"); 174 fprintf(th, "#ifndef SAFETY\n"); 175 fprintf(th, "#define SAFETY\n"); 176 fprintf(th, "#endif\n"); 177 fprintf(th, "#ifndef XUSAFE\n"); 178 fprintf(th, "#define XUSAFE\n"); 179 fprintf(th, "#endif\n"); 180 fprintf(th, "#endif\n"); 181 182 fprintf(th, "#ifndef uchar\n"); 183 fprintf(th, "#define uchar unsigned char\n"); 184 fprintf(th, "#endif\n"); 185 fprintf(th, "#ifndef uint\n"); 186 fprintf(th, "#define uint unsigned int\n"); 187 fprintf(th, "#endif\n"); 188 189 if (sizeof(long) > 4) /* 64 bit machine */ 190 { fprintf(th, "#ifndef HASH32\n"); 191 fprintf(th, "#define HASH64\n"); 192 fprintf(th, "#endif\n"); 193 } 194 195 if (sizeof(long)==sizeof(int)) 196 fprintf(th, "#define long int\n"); 197 198 if (separate == 1 && !claimproc) 199 { Symbol *n = (Symbol *) emalloc(sizeof(Symbol)); 200 Sequence *s = (Sequence *) emalloc(sizeof(Sequence)); 201 claimproc = n->name = "_:never_template:_"; 202 ready(n, ZN, s, 0, ZN); 203 } 204 if (separate == 2) 205 { if (has_remote) 206 { printf("spin: warning, make sure that the S1 model\n"); 207 printf(" includes the same remote references\n"); 208 } 209 fprintf(th, "#ifndef NFAIR\n"); 210 fprintf(th, "#define NFAIR 2 /* must be >= 2 */\n"); 211 fprintf(th, "#endif\n"); 212 if (has_last) 213 fprintf(th, "#define HAS_LAST %d\n", has_last); 214 goto doless; 215 } 216 217 fprintf(th, "#define DELTA %d\n", DELTA); 218 fprintf(th, "#ifdef MA\n"); 219 fprintf(th, "#if MA==1\n"); /* user typed -DMA without size */ 220 fprintf(th, "#undef MA\n#define MA 100\n"); 221 fprintf(th, "#endif\n#endif\n"); 222 fprintf(th, "#ifdef W_XPT\n"); 223 fprintf(th, "#if W_XPT==1\n"); /* user typed -DW_XPT without size */ 224 fprintf(th, "#undef W_XPT\n#define W_XPT 1000000\n"); 225 fprintf(th, "#endif\n#endif\n"); 226 fprintf(th, "#ifndef NFAIR\n"); 227 fprintf(th, "#define NFAIR 2 /* must be >= 2 */\n"); 228 fprintf(th, "#endif\n"); 229 if (Ntimeouts) 230 fprintf(th, "#define NTIM %d\n", Ntimeouts); 231 if (Etimeouts) 232 fprintf(th, "#define ETIM %d\n", Etimeouts); 233 if (has_remvar) 234 fprintf(th, "#define REM_VARS 1\n"); 235 if (has_remote) 236 fprintf(th, "#define REM_REFS %d\n", has_remote); /* not yet used */ 237 if (has_last) 238 fprintf(th, "#define HAS_LAST %d\n", has_last); 239 if (has_sorted) 240 fprintf(th, "#define HAS_SORTED %d\n", has_sorted); 241 if (m_loss) 242 fprintf(th, "#define M_LOSS\n"); 243 if (has_random) 244 fprintf(th, "#define HAS_RANDOM %d\n", has_random); 245 fprintf(th, "#define HAS_CODE\n"); /* doesn't seem to cause measurable overhead */ 246 if (has_stack) 247 fprintf(th, "#define HAS_STACK\n"); 248 if (has_enabled) 249 fprintf(th, "#define HAS_ENABLED 1\n"); 250 if (has_unless) 251 fprintf(th, "#define HAS_UNLESS %d\n", has_unless); 252 if (has_provided) 253 fprintf(th, "#define HAS_PROVIDED %d\n", has_provided); 254 if (has_pcvalue) 255 fprintf(th, "#define HAS_PCVALUE %d\n", has_pcvalue); 256 if (has_badelse) 257 fprintf(th, "#define HAS_BADELSE %d\n", has_badelse); 258 if (has_enabled 259 || has_pcvalue 260 || has_badelse 261 || has_last) 262 { fprintf(th, "#ifndef NOREDUCE\n"); 263 fprintf(th, "#define NOREDUCE 1\n"); 264 fprintf(th, "#endif\n"); 265 } 266 if (has_np) 267 fprintf(th, "#define HAS_NP %d\n", has_np); 268 if (merger) 269 fprintf(th, "#define MERGED 1\n"); 270 271 doless: 272 fprintf(th, "#ifdef NP /* includes np_ demon */\n"); 273 if (!has_np) 274 fprintf(th, "#define HAS_NP 2\n"); 275 fprintf(th, "#define VERI %d\n", nrRdy); 276 fprintf(th, "#define endclaim 3 /* none */\n"); 277 fprintf(th, "#endif\n"); 278 if (claimproc) 279 { claimnr = fproc(claimproc); 280 /* NP overrides claimproc */ 281 fprintf(th, "#if !defined(NOCLAIM) && !defined NP\n"); 282 fprintf(th, "#define VERI %d\n", claimnr); 283 fprintf(th, "#define endclaim endstate%d\n", claimnr); 284 fprintf(th, "#endif\n"); 285 } 286 if (eventmap) 287 { eventmapnr = fproc(eventmap); 288 fprintf(th, "#define EVENT_TRACE %d\n", eventmapnr); 289 fprintf(th, "#define endevent endstate%d\n", eventmapnr); 290 if (eventmap[2] == 'o') /* ":notrace:" */ 291 fprintf(th, "#define NEGATED_TRACE 1\n"); 292 } 293 294 fprintf(th, "typedef struct S_F_MAP {\n"); 295 fprintf(th, " char *fnm; int from; int upto;\n"); 296 fprintf(th, "} S_F_MAP;\n"); 297 298 fprintf(tc, "/*** Generated by %s ***/\n", Version); 299 fprintf(tc, "/*** From source: %s ***/\n\n", oFname->name); 300 301 ntimes(tc, 0, 1, Pre0); 302 303 plunk_c_decls(tc); /* types can be refered to in State */ 304 305 switch (separate) { 306 case 0: fprintf(tc, "#include \"pan.h\"\n"); break; 307 case 1: fprintf(tc, "#include \"pan_s.h\"\n"); break; 308 case 2: fprintf(tc, "#include \"pan_t.h\"\n"); break; 309 } 310 311 fprintf(tc, "State A_Root; /* seed-state for cycles */\n"); 312 fprintf(tc, "State now; /* the full state-vector */\n"); 313 plunk_c_fcts(tc); /* State can be used in fcts */ 314 315 if (separate != 2) 316 ntimes(tc, 0, 1, Preamble); 317 318 fprintf(tc, "#ifndef NOBOUNDCHECK\n"); 319 fprintf(tc, "#define Index(x, y)\tBoundcheck(x, y, II, tt, t)\n"); 320 fprintf(tc, "#else\n"); 321 fprintf(tc, "#define Index(x, y)\tx\n"); 322 fprintf(tc, "#endif\n"); 323 324 c_preview(); /* sets hastrack */ 325 326 for (p = rdy; p; p = p->nxt) 327 mst = max(p->s->maxel, mst); 328 329 if (separate != 2) 330 { fprintf(tt, "#ifdef PEG\n"); 331 fprintf(tt, "struct T_SRC {\n"); 332 fprintf(tt, " char *fl; int ln;\n"); 333 fprintf(tt, "} T_SRC[NTRANS];\n\n"); 334 fprintf(tt, "void\ntr_2_src(int m, char *file, int ln)\n"); 335 fprintf(tt, "{ T_SRC[m].fl = file;\n"); 336 fprintf(tt, " T_SRC[m].ln = ln;\n"); 337 fprintf(tt, "}\n\n"); 338 fprintf(tt, "void\nputpeg(int n, int m)\n"); 339 fprintf(tt, "{ printf(\"%%5d\ttrans %%4d \", m, n);\n"); 340 fprintf(tt, " printf(\"file %%s line %%3d\\n\",\n"); 341 fprintf(tt, " T_SRC[n].fl, T_SRC[n].ln);\n"); 342 fprintf(tt, "}\n"); 343 if (!merger) 344 { fprintf(tt, "#else\n"); 345 fprintf(tt, "#define tr_2_src(m,f,l)\n"); 346 } 347 fprintf(tt, "#endif\n\n"); 348 fprintf(tt, "void\nsettable(void)\n{\tTrans *T;\n"); 349 fprintf(tt, "\tTrans *settr(int, int, int, int, int,"); 350 fprintf(tt, " char *, int, int, int);\n\n"); 351 fprintf(tt, "\ttrans = (Trans ***) "); 352 fprintf(tt, "emalloc(%d*sizeof(Trans **));\n", nrRdy+1); 353 /* +1 for np_ automaton */ 354 355 if (separate == 1) 356 { 357 fprintf(tm, " if (II == 0)\n"); 358 fprintf(tm, " { _m = step_claim(trpt->o_pm, trpt->tau, tt, ot, t);\n"); 359 fprintf(tm, " if (_m) goto P999; else continue;\n"); 360 fprintf(tm, " } else\n"); 361 } 362 363 fprintf(tm, "#define rand pan_rand\n"); 364 fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n"); 365 fprintf(tm, " printf(\"Pr: %%d Tr: %%d\\n\", II, t->forw);\n"); 366 fprintf(tm, "#endif\n"); 367 fprintf(tm, " switch (t->forw) {\n"); 368 } else 369 { fprintf(tt, "#ifndef PEG\n"); 370 fprintf(tt, "#define tr_2_src(m,f,l)\n"); 371 fprintf(tt, "#endif\n"); 372 fprintf(tt, "void\nset_claim(void)\n{\tTrans *T;\n"); 373 fprintf(tt, "\textern Trans ***trans;\n"); 374 fprintf(tt, "\textern Trans *settr(int, int, int, int, int,"); 375 fprintf(tt, " char *, int, int, int);\n\n"); 376 377 fprintf(tm, "#define rand pan_rand\n"); 378 fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n"); 379 fprintf(tm, " printf(\"Pr: %%d Tr: %%d\\n\", II, forw);\n"); 380 fprintf(tm, "#endif\n"); 381 fprintf(tm, " switch (forw) {\n"); 382 } 383 384 fprintf(tm, " default: Uerror(\"bad forward move\");\n"); 385 fprintf(tm, " case 0: /* if without executable clauses */\n"); 386 fprintf(tm, " continue;\n"); 387 fprintf(tm, " case 1: /* generic 'goto' or 'skip' */\n"); 388 if (separate != 2) 389 fprintf(tm, " IfNotBlocked\n"); 390 fprintf(tm, " _m = 3; goto P999;\n"); 391 fprintf(tm, " case 2: /* generic 'else' */\n"); 392 if (separate == 2) 393 fprintf(tm, " if (o_pm&1) continue;\n"); 394 else 395 { fprintf(tm, " IfNotBlocked\n"); 396 fprintf(tm, " if (trpt->o_pm&1) continue;\n"); 397 } 398 fprintf(tm, " _m = 3; goto P999;\n"); 399 uniq = 3; 400 401 if (separate == 1) 402 fprintf(tb, " if (II == 0) goto R999;\n"); 403 404 fprintf(tb, " switch (t->back) {\n"); 405 fprintf(tb, " default: Uerror(\"bad return move\");\n"); 406 fprintf(tb, " case 0: goto R999; /* nothing to undo */\n"); 407 408 for (p = rdy; p; p = p->nxt) 409 putproc(p); 410 411 if (separate != 2) 412 { fprintf(th, "struct {\n"); 413 fprintf(th, " int tp; short *src;\n"); 414 fprintf(th, "} src_all[] = {\n"); 415 for (p = rdy; p; p = p->nxt) 416 fprintf(th, " { %d, &src_ln%d[0] },\n", 417 p->tn, p->tn); 418 fprintf(th, " { 0, (short *) 0 }\n"); 419 fprintf(th, "};\n"); 420 } 421 422 gencodetable(th); 423 424 if (separate != 1) 425 { tm_predef_np(); 426 tt_predef_np(); 427 } 428 fprintf(tt, "}\n\n"); /* end of settable() */ 429 430 fprintf(tm, "#undef rand\n"); 431 fprintf(tm, " }\n\n"); 432 fprintf(tb, " }\n\n"); 433 434 if (separate != 2) 435 { ntimes(tt, 0, 1, Tail); 436 genheader(); 437 if (separate == 1) 438 { fprintf(th, "#define FORWARD_MOVES\t\"pan_s.m\"\n"); 439 fprintf(th, "#define REVERSE_MOVES\t\"pan_s.b\"\n"); 440 fprintf(th, "#define SEPARATE\n"); 441 fprintf(th, "#define TRANSITIONS\t\"pan_s.t\"\n"); 442 fprintf(th, "extern void ini_claim(int, int);\n"); 443 } else 444 { fprintf(th, "#define FORWARD_MOVES\t\"pan.m\"\n"); 445 fprintf(th, "#define REVERSE_MOVES\t\"pan.b\"\n"); 446 fprintf(th, "#define TRANSITIONS\t\"pan.t\"\n"); 447 } 448 genaddproc(); 449 genother(); 450 genaddqueue(); 451 genunio(); 452 genconditionals(); 453 gensvmap(); 454 if (!run) fatal("no runable process", (char *)0); 455 fprintf(tc, "void\n"); 456 fprintf(tc, "active_procs(void)\n{\n"); 457 reverse_procs(run); 458 fprintf(tc, "}\n"); 459 ntimes(tc, 0, 1, Dfa); 460 ntimes(tc, 0, 1, Xpt); 461 462 fprintf(th, "#define NTRANS %d\n", uniq); 463 fprintf(th, "#ifdef PEG\n"); 464 fprintf(th, "long peg[NTRANS];\n"); 465 fprintf(th, "#endif\n"); 466 467 if (u_sync && !u_async) 468 spit_recvs(th, tc); 469 } else 470 { genheader(); 471 fprintf(th, "#define FORWARD_MOVES\t\"pan_t.m\"\n"); 472 fprintf(th, "#define REVERSE_MOVES\t\"pan_t.b\"\n"); 473 fprintf(th, "#define TRANSITIONS\t\"pan_t.t\"\n"); 474 fprintf(tc, "extern int Maxbody;\n"); 475 fprintf(tc, "extern int proc_offset[];\n"); 476 fprintf(tc, "extern int proc_skip[];\n"); 477 fprintf(tc, "extern uchar *reached[];\n"); 478 fprintf(tc, "extern uchar *accpstate[];\n"); 479 fprintf(tc, "extern uchar *progstate[];\n"); 480 fprintf(tc, "extern uchar *stopstate[];\n"); 481 fprintf(tc, "extern uchar *visstate[];\n\n"); 482 fprintf(tc, "extern short *mapstate[];\n"); 483 484 fprintf(tc, "void\nini_claim(int n, int h)\n{"); 485 fprintf(tc, "\textern State now;\n"); 486 fprintf(tc, "\textern void set_claim(void);\n\n"); 487 fprintf(tc, "#ifdef PROV\n"); 488 fprintf(tc, "#include PROV\n"); 489 fprintf(tc, "#endif\n"); 490 fprintf(tc, "\tset_claim();\n"); 491 genother(); 492 fprintf(tc, "\n\tswitch (n) {\n"); 493 genaddproc(); 494 fprintf(tc, "\t}\n"); 495 fprintf(tc, "\n}\n"); 496 fprintf(tc, "int\nstep_claim(int o_pm, int tau, int tt, int ot, Trans *t)\n"); 497 fprintf(tc, "{ int forw = t->forw; int _m = 0; extern char *noptr; int II=0;\n"); 498 fprintf(tc, " extern State now;\n"); 499 fprintf(tc, "#define continue return 0\n"); 500 fprintf(tc, "#include \"pan_t.m\"\n"); 501 fprintf(tc, "P999:\n\treturn _m;\n}\n"); 502 fprintf(tc, "#undef continue\n"); 503 fprintf(tc, "int\nrev_claim(int backw)\n{ return 0; }\n"); 504 fprintf(tc, "#include TRANSITIONS\n"); 505 } 506 if (separate != 1) 507 ntimes(tc, 0, 1, Nvr1); 508 509 if (separate != 2) 510 { c_wrapper(tc); 511 c_chandump(tc); 512 } 513 } 514 515 static int 516 find_id(Symbol *s) 517 { ProcList *p; 518 519 if (s) 520 for (p = rdy; p; p = p->nxt) 521 if (s == p->n) 522 return p->tn; 523 return 0; 524 } 525 526 static void 527 dolen(Symbol *s, char *pre, int pid, int ai, int qln) 528 { 529 if (ai > 0) 530 fprintf(tc, "\n\t\t\t || "); 531 fprintf(tc, "%s(", pre); 532 if (!(s->hidden&1)) 533 { if (s->context) 534 fprintf(tc, "((P%d *)this)->", pid); 535 else 536 fprintf(tc, "now."); 537 } 538 fprintf(tc, "%s", s->name); 539 if (qln > 1) fprintf(tc, "[%d]", ai); 540 fprintf(tc, ")"); 541 } 542 543 struct AA { char TT[9]; char CC[8]; }; 544 545 static struct AA BB[4] = { 546 { "Q_FULL_F", " q_full" }, 547 { "Q_FULL_T", "!q_full" }, 548 { "Q_EMPT_F", " !q_len" }, 549 { "Q_EMPT_T", " q_len" } 550 }; 551 552 static struct AA DD[4] = { 553 { "Q_FULL_F", " q_e_f" }, /* empty or full */ 554 { "Q_FULL_T", "!q_full" }, 555 { "Q_EMPT_F", " q_e_f" }, 556 { "Q_EMPT_T", " q_len" } 557 }; 558 /* this reduces the number of cases where 's' and 'r' 559 are considered conditionally safe under the 560 partial order reduction rules; as a price for 561 this simple implementation, it also affects the 562 cases where nfull and nempty can be considered 563 safe -- since these are labeled the same way as 564 's' and 'r' respectively 565 it only affects reduction, not functionality 566 */ 567 568 void 569 bb_or_dd(int j, int which) 570 { 571 if (which) 572 { if (has_unless) 573 fprintf(tc, "%s", DD[j].CC); 574 else 575 fprintf(tc, "%s", BB[j].CC); 576 } else 577 { if (has_unless) 578 fprintf(tc, "%s", DD[j].TT); 579 else 580 fprintf(tc, "%s", BB[j].TT); 581 } 582 } 583 584 void 585 Done_case(char *nm, Symbol *z) 586 { int j, k; 587 int nid = z->Nid; 588 int qln = z->nel; 589 590 fprintf(tc, "\t\tcase %d: if (", nid); 591 for (j = 0; j < 4; j++) 592 { fprintf(tc, "\t(t->ty[i] == "); 593 bb_or_dd(j, 0); 594 fprintf(tc, " && ("); 595 for (k = 0; k < qln; k++) 596 { if (k > 0) 597 fprintf(tc, "\n\t\t\t || "); 598 bb_or_dd(j, 1); 599 fprintf(tc, "(%s%s", nm, z->name); 600 if (qln > 1) 601 fprintf(tc, "[%d]", k); 602 fprintf(tc, ")"); 603 } 604 fprintf(tc, "))\n\t\t\t "); 605 if (j < 3) 606 fprintf(tc, "|| "); 607 else 608 fprintf(tc, " "); 609 } 610 fprintf(tc, ") return 0; break;\n"); 611 } 612 613 static void 614 Docase(Symbol *s, int pid, int nid) 615 { int i, j; 616 617 fprintf(tc, "\t\tcase %d: if (", nid); 618 for (j = 0; j < 4; j++) 619 { fprintf(tc, "\t(t->ty[i] == "); 620 bb_or_dd(j, 0); 621 fprintf(tc, " && ("); 622 if (has_unless) 623 { for (i = 0; i < s->nel; i++) 624 dolen(s, DD[j].CC, pid, i, s->nel); 625 } else 626 { for (i = 0; i < s->nel; i++) 627 dolen(s, BB[j].CC, pid, i, s->nel); 628 } 629 fprintf(tc, "))\n\t\t\t "); 630 if (j < 3) 631 fprintf(tc, "|| "); 632 else 633 fprintf(tc, " "); 634 } 635 fprintf(tc, ") return 0; break;\n"); 636 } 637 638 static void 639 genconditionals(void) 640 { Symbol *s; 641 int last=0, j; 642 extern Ordered *all_names; 643 Ordered *walk; 644 645 fprintf(th, "#define LOCAL 1\n"); 646 fprintf(th, "#define Q_FULL_F 2\n"); 647 fprintf(th, "#define Q_EMPT_F 3\n"); 648 fprintf(th, "#define Q_EMPT_T 4\n"); 649 fprintf(th, "#define Q_FULL_T 5\n"); 650 fprintf(th, "#define TIMEOUT_F 6\n"); 651 fprintf(th, "#define GLOBAL 7\n"); 652 fprintf(th, "#define BAD 8\n"); 653 fprintf(th, "#define ALPHA_F 9\n"); 654 655 fprintf(tc, "int\n"); 656 fprintf(tc, "q_cond(short II, Trans *t)\n"); 657 fprintf(tc, "{ int i = 0;\n"); 658 fprintf(tc, " for (i = 0; i < 6; i++)\n"); 659 fprintf(tc, " { if (t->ty[i] == TIMEOUT_F) return %s;\n", 660 (Etimeouts)?"(!(trpt->tau&1))":"1"); 661 fprintf(tc, " if (t->ty[i] == ALPHA_F)\n"); 662 fprintf(tc, "#ifdef GLOB_ALPHA\n"); 663 fprintf(tc, " return 0;\n"); 664 fprintf(tc, "#else\n\t\t\treturn "); 665 fprintf(tc, "(II+1 == (short) now._nr_pr && II+1 < MAXPROC);\n"); 666 fprintf(tc, "#endif\n"); 667 668 /* we switch on the chan name from the spec (as identified by 669 * the corresponding Nid number) rather than the actual qid 670 * because we cannot predict at compile time which specific qid 671 * will be accessed by the statement at runtime. that is: 672 * we do not know which qid to pass to q_cond at runtime 673 * but we do know which name is used. if it's a chan array, we 674 * must check all elements of the array for compliance (bummer) 675 */ 676 fprintf(tc, " switch (t->qu[i]) {\n"); 677 fprintf(tc, " case 0: break;\n"); 678 679 for (walk = all_names; walk; walk = walk->next) 680 { s = walk->entry; 681 if (s->owner) continue; 682 j = find_id(s->context); 683 if (s->type == CHAN) 684 { if (last == s->Nid) continue; /* chan array */ 685 last = s->Nid; 686 Docase(s, j, last); 687 } else if (s->type == STRUCT) 688 { /* struct may contain a chan */ 689 char pregat[128]; 690 extern void walk2_struct(char *, Symbol *); 691 strcpy(pregat, ""); 692 if (!(s->hidden&1)) 693 { if (s->context) 694 sprintf(pregat, "((P%d *)this)->",j); 695 else 696 sprintf(pregat, "now."); 697 } 698 walk2_struct(pregat, s); 699 } 700 } 701 fprintf(tc, " \tdefault: Uerror(\"unknown qid - q_cond\");\n"); 702 fprintf(tc, " \t\t\treturn 0;\n"); 703 fprintf(tc, " \t}\n"); 704 fprintf(tc, " }\n"); 705 fprintf(tc, " return 1;\n"); 706 fprintf(tc, "}\n"); 707 } 708 709 static void 710 putproc(ProcList *p) 711 { Pid = p->tn; 712 Det = p->det; 713 714 if (Pid == claimnr 715 && separate == 1) 716 { fprintf(th, "extern uchar reached%d[];\n", Pid); 717 fprintf(th, "extern short nstates%d;\n", Pid); 718 fprintf(th, "extern short src_ln%d[];\n", Pid); 719 fprintf(th, "extern S_F_MAP src_file%d[];\n", Pid); 720 fprintf(th, "#define endstate%d %d\n", 721 Pid, p->s->last?p->s->last->seqno:0); 722 fprintf(th, "#define src_claim src_ln%d\n", claimnr); 723 724 return; 725 } 726 if (Pid != claimnr 727 && separate == 2) 728 { fprintf(th, "extern short src_ln%d[];\n", Pid); 729 return; 730 } 731 732 AllGlobal = (p->prov)?1:0; /* process has provided clause */ 733 734 fprintf(th, "\nshort nstates%d=%d;\t/* %s */\n", 735 Pid, p->s->maxel, p->n->name); 736 if (Pid == claimnr) 737 fprintf(th, "#define nstates_claim nstates%d\n", Pid); 738 if (Pid == eventmapnr) 739 fprintf(th, "#define nstates_event nstates%d\n", Pid); 740 741 fprintf(th, "#define endstate%d %d\n", 742 Pid, p->s->last->seqno); 743 fprintf(tm, "\n /* PROC %s */\n", p->n->name); 744 fprintf(tb, "\n /* PROC %s */\n", p->n->name); 745 fprintf(tt, "\n /* proctype %d: %s */\n", Pid, p->n->name); 746 fprintf(tt, "\n trans[%d] = (Trans **)", Pid); 747 fprintf(tt, " emalloc(%d*sizeof(Trans *));\n\n", p->s->maxel); 748 749 if (Pid == eventmapnr) 750 { fprintf(th, "\n#define in_s_scope(x_y3_) 0"); 751 fprintf(tc, "\n#define in_r_scope(x_y3_) 0"); 752 } 753 754 put_seq(p->s, 2, 0); 755 if (Pid == eventmapnr) 756 { fprintf(th, "\n\n"); 757 fprintf(tc, "\n\n"); 758 } 759 dumpsrc(p->s->maxel, Pid); 760 } 761 762 static void 763 addTpe(int x) 764 { int i; 765 766 if (x <= 2) return; 767 768 for (i = 0; i < T_sum; i++) 769 if (TPE[i] == x) 770 return; 771 TPE[(T_sum++)%2] = x; 772 } 773 774 static void 775 cnt_seq(Sequence *s) 776 { Element *f; 777 SeqList *h; 778 779 if (s) 780 for (f = s->frst; f; f = f->nxt) 781 { Tpe(f->n); /* sets EPT */ 782 addTpe(EPT[0]); 783 addTpe(EPT[1]); 784 for (h = f->sub; h; h = h->nxt) 785 cnt_seq(h->this); 786 if (f == s->last) 787 break; 788 } 789 } 790 791 static void 792 typ_seq(Sequence *s) 793 { 794 T_sum = 0; 795 TPE[0] = 2; TPE[1] = 0; 796 cnt_seq(s); 797 if (T_sum > 2) /* more than one type */ 798 { TPE[0] = 5*DELTA; /* non-mixing */ 799 TPE[1] = 0; 800 } 801 } 802 803 static int 804 hidden(Lextok *n) 805 { 806 if (n) 807 switch (n->ntyp) { 808 case FULL: case EMPTY: 809 case NFULL: case NEMPTY: case TIMEOUT: 810 Nn[(T_mus++)%2] = n; 811 break; 812 case '!': case UMIN: case '~': case ASSERT: case 'c': 813 (void) hidden(n->lft); 814 break; 815 case '/': case '*': case '-': case '+': 816 case '%': case LT: case GT: case '&': case '^': 817 case '|': case LE: case GE: case NE: case '?': 818 case EQ: case OR: case AND: case LSHIFT: case RSHIFT: 819 (void) hidden(n->lft); 820 (void) hidden(n->rgt); 821 break; 822 } 823 return T_mus; 824 } 825 826 static int 827 getNid(Lextok *n) 828 { 829 if (n->sym->type == STRUCT 830 && n->rgt && n->rgt->lft) 831 return getNid(n->rgt->lft); 832 833 if (!n->sym || n->sym->Nid == 0) 834 { fatal("bad channel name '%s'", 835 (n->sym)?n->sym->name:"no name"); 836 } 837 return n->sym->Nid; 838 } 839 840 static int 841 valTpe(Lextok *n) 842 { int res = 2; 843 /* 844 2 = local 845 2+1 .. 2+1*DELTA = nfull, 's' - require q_full==false 846 2+1+1*DELTA .. 2+2*DELTA = nempty, 'r' - require q_len!=0 847 2+1+2*DELTA .. 2+3*DELTA = empty - require q_len==0 848 2+1+3*DELTA .. 2+4*DELTA = full - require q_full==true 849 5*DELTA = non-mixing (i.e., always makes the selection global) 850 6*DELTA = timeout (conditionally safe) 851 7*DELTA = @, process deletion (conditionally safe) 852 */ 853 switch (n->ntyp) { /* a series of fall-thru cases: */ 854 case FULL: res += DELTA; /* add 3*DELTA + chan nr */ 855 case EMPTY: res += DELTA; /* add 2*DELTA + chan nr */ 856 case 'r': 857 case NEMPTY: res += DELTA; /* add 1*DELTA + chan nr */ 858 case 's': 859 case NFULL: res += getNid(n->lft); /* add channel nr */ 860 break; 861 862 case TIMEOUT: res = 6*DELTA; break; 863 case '@': res = 7*DELTA; break; 864 default: break; 865 } 866 return res; 867 } 868 869 static void 870 Tpe(Lextok *n) /* mixing in selections */ 871 { 872 EPT[0] = 2; EPT[1] = 0; 873 874 if (!n) return; 875 876 T_mus = 0; 877 Nn[0] = Nn[1] = ZN; 878 879 if (n->ntyp == 'c') 880 { if (hidden(n->lft) > 2) 881 { EPT[0] = 5*DELTA; /* non-mixing */ 882 EPT[1] = 0; 883 return; 884 } 885 } else 886 Nn[0] = n; 887 888 if (Nn[0]) EPT[0] = valTpe(Nn[0]); 889 if (Nn[1]) EPT[1] = valTpe(Nn[1]); 890 } 891 892 static void 893 put_escp(Element *e) 894 { int n; 895 SeqList *x; 896 897 if (e->esc /* && e->n->ntyp != GOTO */ && e->n->ntyp != '.') 898 { for (x = e->esc, n = 0; x; x = x->nxt, n++) 899 { int i = huntele(x->this->frst, e->status, -1)->seqno; 900 fprintf(tt, "\ttrans[%d][%d]->escp[%d] = %d;\n", 901 Pid, e->seqno, n, i); 902 fprintf(tt, "\treached%d[%d] = 1;\n", 903 Pid, i); 904 } 905 for (x = e->esc, n=0; x; x = x->nxt, n++) 906 { fprintf(tt, " /* escape #%d: %d */\n", n, 907 huntele(x->this->frst, e->status, -1)->seqno); 908 put_seq(x->this, 2, 0); /* args?? */ 909 } 910 fprintf(tt, " /* end-escapes */\n"); 911 } 912 } 913 914 static void 915 put_sub(Element *e, int Tt0, int Tt1) 916 { Sequence *s = e->n->sl->this; 917 Element *g = ZE; 918 int a; 919 920 patch_atomic(s); 921 putskip(s->frst->seqno); 922 g = huntstart(s->frst); 923 a = g->seqno; 924 925 if (0) printf("put_sub %d -> %d -> %d\n", e->seqno, s->frst->seqno, a); 926 927 if ((e->n->ntyp == ATOMIC 928 || e->n->ntyp == D_STEP) 929 && scan_seq(s)) 930 mark_seq(s); 931 s->last->nxt = e->nxt; 932 933 typ_seq(s); /* sets TPE */ 934 935 if (e->n->ntyp == D_STEP) 936 { int inherit = (e->status&(ATOM|L_ATOM)); 937 fprintf(tm, "\tcase %d: ", uniq++); 938 fprintf(tm, "/* STATE %d - line %d %s - [", 939 e->seqno, e->n->ln, e->n->fn->name); 940 comment(tm, e->n, 0); 941 fprintf(tm, "] */\n\t\t"); 942 943 if (s->last->n->ntyp == BREAK) 944 OkBreak = target(huntele(s->last->nxt, 945 s->last->status, -1))->Seqno; 946 else 947 OkBreak = -1; 948 949 if (!putcode(tm, s, e->nxt, 0, e->n->ln, e->seqno)) 950 { 951 fprintf(tm, "\n#if defined(C_States) && (HAS_TRACK==1)\n"); 952 fprintf(tm, "\t\tc_update((uchar *) &(now.c_state[0]));\n"); 953 fprintf(tm, "#endif\n"); 954 955 fprintf(tm, "\t\t_m = %d", getweight(s->frst->n)); 956 if (m_loss && s->frst->n->ntyp == 's') 957 fprintf(tm, "+delta_m; delta_m = 0"); 958 fprintf(tm, "; goto P999;\n\n"); 959 } 960 961 fprintf(tb, "\tcase %d: ", uniq-1); 962 fprintf(tb, "/* STATE %d */\n", e->seqno); 963 fprintf(tb, "\t\tsv_restor();\n"); 964 fprintf(tb, "\t\tgoto R999;\n"); 965 if (e->nxt) 966 a = huntele(e->nxt, e->status, -1)->seqno; 967 else 968 a = 0; 969 tr_map(uniq-1, e); 970 fprintf(tt, "/*->*/\ttrans[%d][%d]\t= ", 971 Pid, e->seqno); 972 fprintf(tt, "settr(%d,%d,%d,%d,%d,\"", 973 e->Seqno, D_ATOM|inherit, a, uniq-1, uniq-1); 974 comment(tt, e->n, e->seqno); 975 fprintf(tt, "\", %d, ", (s->frst->status&I_GLOB)?1:0); 976 fprintf(tt, "%d, %d);\n", TPE[0], TPE[1]); 977 put_escp(e); 978 } else 979 { /* ATOMIC or NON_ATOMIC */ 980 fprintf(tt, "\tT = trans[ %d][%d] = ", Pid, e->seqno); 981 fprintf(tt, "settr(%d,%d,0,0,0,\"", 982 e->Seqno, (e->n->ntyp == ATOMIC)?ATOM:0); 983 comment(tt, e->n, e->seqno); 984 if ((e->status&CHECK2) 985 || (g->status&CHECK2)) 986 s->frst->status |= I_GLOB; 987 fprintf(tt, "\", %d, %d, %d);", 988 (s->frst->status&I_GLOB)?1:0, Tt0, Tt1); 989 blurb(tt, e); 990 fprintf(tt, "\tT->nxt\t= "); 991 fprintf(tt, "settr(%d,%d,%d,0,0,\"", 992 e->Seqno, (e->n->ntyp == ATOMIC)?ATOM:0, a); 993 comment(tt, e->n, e->seqno); 994 fprintf(tt, "\", %d, ", (s->frst->status&I_GLOB)?1:0); 995 if (e->n->ntyp == NON_ATOMIC) 996 { fprintf(tt, "%d, %d);", Tt0, Tt1); 997 blurb(tt, e); 998 put_seq(s, Tt0, Tt1); 999 } else 1000 { fprintf(tt, "%d, %d);", TPE[0], TPE[1]); 1001 blurb(tt, e); 1002 put_seq(s, TPE[0], TPE[1]); 1003 } 1004 } 1005 } 1006 1007 typedef struct CaseCache { 1008 int m, b, owner; 1009 Element *e; 1010 Lextok *n; 1011 FSM_use *u; 1012 struct CaseCache *nxt; 1013 } CaseCache; 1014 1015 CaseCache *casing[6]; 1016 1017 static int 1018 identical(Lextok *p, Lextok *q) 1019 { 1020 if ((!p && q) || (p && !q)) 1021 return 0; 1022 if (!p) 1023 return 1; 1024 1025 if (p->ntyp != q->ntyp 1026 || p->ismtyp != q->ismtyp 1027 || p->val != q->val 1028 || p->indstep != q->indstep 1029 || p->sym != q->sym 1030 || p->sq != q->sq 1031 || p->sl != q->sl) 1032 return 0; 1033 1034 return identical(p->lft, q->lft) 1035 && identical(p->rgt, q->rgt); 1036 } 1037 1038 static int 1039 samedeads(FSM_use *a, FSM_use *b) 1040 { FSM_use *p, *q; 1041 1042 for (p = a, q = b; p && q; p = p->nxt, q = q->nxt) 1043 if (p->var != q->var 1044 || p->special != q->special) 1045 return 0; 1046 return (!p && !q); 1047 } 1048 1049 static Element * 1050 findnext(Element *f) 1051 { Element *g; 1052 1053 if (f->n->ntyp == GOTO) 1054 { g = get_lab(f->n, 1); 1055 return huntele(g, f->status, -1); 1056 } 1057 return f->nxt; 1058 } 1059 1060 static Element * 1061 advance(Element *e, int stopat) 1062 { Element *f = e; 1063 1064 if (stopat) 1065 while (f && f->seqno != stopat) 1066 { f = findnext(f); 1067 switch (f->n->ntyp) { 1068 case GOTO: 1069 case '.': 1070 case PRINT: 1071 case PRINTM: 1072 break; 1073 default: 1074 return f; 1075 } 1076 } 1077 return (Element *) 0; 1078 } 1079 1080 static int 1081 equiv_merges(Element *a, Element *b) 1082 { Element *f, *g; 1083 int stopat_a, stopat_b; 1084 1085 if (a->merge_start) 1086 stopat_a = a->merge_start; 1087 else 1088 stopat_a = a->merge; 1089 1090 if (b->merge_start) 1091 stopat_b = b->merge_start; 1092 else 1093 stopat_b = b->merge; 1094 1095 if (!stopat_a && !stopat_b) 1096 return 1; 1097 1098 for (;;) 1099 { 1100 f = advance(a, stopat_a); 1101 g = advance(b, stopat_b); 1102 if (!f && !g) 1103 return 1; 1104 if (f && g) 1105 return identical(f->n, g->n); 1106 else 1107 return 0; 1108 } 1109 return 1; 1110 } 1111 1112 static CaseCache * 1113 prev_case(Element *e, int owner) 1114 { int j; CaseCache *nc; 1115 1116 switch (e->n->ntyp) { 1117 case 'r': j = 0; break; 1118 case 's': j = 1; break; 1119 case 'c': j = 2; break; 1120 case ASGN: j = 3; break; 1121 case ASSERT: j = 4; break; 1122 default: j = 5; break; 1123 } 1124 for (nc = casing[j]; nc; nc = nc->nxt) 1125 if (identical(nc->n, e->n) 1126 && samedeads(nc->u, e->dead) 1127 && equiv_merges(nc->e, e) 1128 && nc->owner == owner) 1129 return nc; 1130 1131 return (CaseCache *) 0; 1132 } 1133 1134 static void 1135 new_case(Element *e, int m, int b, int owner) 1136 { int j; CaseCache *nc; 1137 1138 switch (e->n->ntyp) { 1139 case 'r': j = 0; break; 1140 case 's': j = 1; break; 1141 case 'c': j = 2; break; 1142 case ASGN: j = 3; break; 1143 case ASSERT: j = 4; break; 1144 default: j = 5; break; 1145 } 1146 nc = (CaseCache *) emalloc(sizeof(CaseCache)); 1147 nc->owner = owner; 1148 nc->m = m; 1149 nc->b = b; 1150 nc->e = e; 1151 nc->n = e->n; 1152 nc->u = e->dead; 1153 nc->nxt = casing[j]; 1154 casing[j] = nc; 1155 } 1156 1157 static int 1158 nr_bup(Element *e) 1159 { FSM_use *u; 1160 Lextok *v; 1161 int nr = 0; 1162 1163 switch (e->n->ntyp) { 1164 case ASGN: 1165 nr++; 1166 break; 1167 case 'r': 1168 if (e->n->val >= 1) 1169 nr++; /* random recv */ 1170 for (v = e->n->rgt; v; v = v->rgt) 1171 { if ((v->lft->ntyp == CONST 1172 || v->lft->ntyp == EVAL)) 1173 continue; 1174 nr++; 1175 } 1176 break; 1177 default: 1178 break; 1179 } 1180 for (u = e->dead; u; u = u->nxt) 1181 { switch (u->special) { 1182 case 2: /* dead after write */ 1183 if (e->n->ntyp == ASGN 1184 && e->n->rgt->ntyp == CONST 1185 && e->n->rgt->val == 0) 1186 break; 1187 nr++; 1188 break; 1189 case 1: /* dead after read */ 1190 nr++; 1191 break; 1192 } } 1193 return nr; 1194 } 1195 1196 static int 1197 nrhops(Element *e) 1198 { Element *f = e, *g; 1199 int cnt = 0; 1200 int stopat; 1201 1202 if (e->merge_start) 1203 stopat = e->merge_start; 1204 else 1205 stopat = e->merge; 1206 #if 0 1207 printf("merge: %d merge_start %d - seqno %d\n", 1208 e->merge, e->merge_start, e->seqno); 1209 #endif 1210 do { 1211 cnt += nr_bup(f); 1212 1213 if (f->n->ntyp == GOTO) 1214 { g = get_lab(f->n, 1); 1215 if (g->seqno == stopat) 1216 f = g; 1217 else 1218 f = huntele(g, f->status, stopat); 1219 } else 1220 { 1221 f = f->nxt; 1222 } 1223 1224 if (f && !f->merge && !f->merge_single && f->seqno != stopat) 1225 { fprintf(tm, "\n\t\tbad hop %s:%d -- at %d, <", 1226 f->n->fn->name,f->n->ln, f->seqno); 1227 comment(tm, f->n, 0); 1228 fprintf(tm, "> looking for %d -- merge %d:%d:%d\n\t\t", 1229 stopat, f->merge, f->merge_start, f->merge_single); 1230 break; 1231 } 1232 } while (f && f->seqno != stopat); 1233 1234 return cnt; 1235 } 1236 1237 static void 1238 check_needed(void) 1239 { 1240 if (multi_needed) 1241 { fprintf(tm, "(trpt+1)->bup.ovals = grab_ints(%d);\n\t\t", 1242 multi_needed); 1243 multi_undo = multi_needed; 1244 multi_needed = 0; 1245 } 1246 } 1247 1248 static void 1249 doforward(FILE *tm, Element *e) 1250 { FSM_use *u; 1251 1252 putstmnt(tm, e->n, e->seqno); 1253 1254 if (e->n->ntyp != ELSE && Det) 1255 { fprintf(tm, ";\n\t\tif (trpt->o_pm&1)\n\t\t"); 1256 fprintf(tm, "\tuerror(\"non-determinism in D_proctype\")"); 1257 } 1258 if (deadvar && !has_code) 1259 for (u = e->dead; u; u = u->nxt) 1260 { fprintf(tm, ";\n\t\t/* dead %d: %s */ ", 1261 u->special, u->var->name); 1262 1263 switch (u->special) { 1264 case 2: /* dead after write -- lval already bupped */ 1265 if (e->n->ntyp == ASGN) /* could be recv or asgn */ 1266 { if (e->n->rgt->ntyp == CONST 1267 && e->n->rgt->val == 0) 1268 continue; /* already set to 0 */ 1269 } 1270 if (e->n->ntyp != 'r') 1271 { XZ.sym = u->var; 1272 fprintf(tm, "\n#ifdef HAS_CODE\n"); 1273 fprintf(tm, "\t\tif (!readtrail)\n"); 1274 fprintf(tm, "#endif\n\t\t\t"); 1275 putname(tm, "", &XZ, 0, " = 0"); 1276 break; 1277 } /* else fall through */ 1278 case 1: /* dead after read -- add asgn of rval -- needs bup */ 1279 YZ[YZmax].sym = u->var; /* store for pan.b */ 1280 CnT[YZcnt]++; /* this step added bups */ 1281 if (multi_oval) 1282 { check_needed(); 1283 fprintf(tm, "(trpt+1)->bup.ovals[%d] = ", 1284 multi_oval-1); 1285 multi_oval++; 1286 } else 1287 fprintf(tm, "(trpt+1)->bup.oval = "); 1288 putname(tm, "", &YZ[YZmax], 0, ";\n"); 1289 fprintf(tm, "#ifdef HAS_CODE\n"); 1290 fprintf(tm, "\t\tif (!readtrail)\n"); 1291 fprintf(tm, "#endif\n\t\t\t"); 1292 putname(tm, "", &YZ[YZmax], 0, " = 0"); 1293 YZmax++; 1294 break; 1295 } } 1296 fprintf(tm, ";\n\t\t"); 1297 } 1298 1299 static int 1300 dobackward(Element *e, int casenr) 1301 { 1302 if (!any_undo(e->n) && CnT[YZcnt] == 0) 1303 { YZcnt--; 1304 return 0; 1305 } 1306 1307 if (!didcase) 1308 { fprintf(tb, "\n\tcase %d: ", casenr); 1309 fprintf(tb, "/* STATE %d */\n\t\t", e->seqno); 1310 didcase++; 1311 } 1312 1313 _isok++; 1314 while (CnT[YZcnt] > 0) /* undo dead variable resets */ 1315 { CnT[YZcnt]--; 1316 YZmax--; 1317 if (YZmax < 0) 1318 fatal("cannot happen, dobackward", (char *)0); 1319 fprintf(tb, ";\n\t/* %d */\t", YZmax); 1320 putname(tb, "", &YZ[YZmax], 0, " = trpt->bup.oval"); 1321 if (multi_oval > 0) 1322 { multi_oval--; 1323 fprintf(tb, "s[%d]", multi_oval-1); 1324 } 1325 } 1326 1327 if (e->n->ntyp != '.') 1328 { fprintf(tb, ";\n\t\t"); 1329 undostmnt(e->n, e->seqno); 1330 } 1331 _isok--; 1332 1333 YZcnt--; 1334 return 1; 1335 } 1336 1337 static void 1338 lastfirst(int stopat, Element *fin, int casenr) 1339 { Element *f = fin, *g; 1340 1341 if (f->n->ntyp == GOTO) 1342 { g = get_lab(f->n, 1); 1343 if (g->seqno == stopat) 1344 f = g; 1345 else 1346 f = huntele(g, f->status, stopat); 1347 } else 1348 f = f->nxt; 1349 1350 if (!f || f->seqno == stopat 1351 || (!f->merge && !f->merge_single)) 1352 return; 1353 lastfirst(stopat, f, casenr); 1354 #if 0 1355 fprintf(tb, "\n\t/* merge %d -- %d:%d %d:%d:%d (casenr %d) ", 1356 YZcnt, 1357 f->merge_start, f->merge, 1358 f->seqno, f?f->seqno:-1, stopat, 1359 casenr); 1360 comment(tb, f->n, 0); 1361 fprintf(tb, " */\n"); 1362 fflush(tb); 1363 #endif 1364 dobackward(f, casenr); 1365 } 1366 1367 static int modifier; 1368 1369 static void 1370 lab_transfer(Element *to, Element *from) 1371 { Symbol *ns, *s = has_lab(from, (1|2|4)); 1372 Symbol *oc; 1373 int ltp, usedit=0; 1374 1375 if (!s) return; 1376 1377 /* "from" could have all three labels -- rename 1378 * to prevent jumps to the transfered copies 1379 */ 1380 oc = context; /* remember */ 1381 for (ltp = 1; ltp < 8; ltp *= 2) /* 1, 2, and 4 */ 1382 if ((s = has_lab(from, ltp)) != (Symbol *) 0) 1383 { ns = (Symbol *) emalloc(sizeof(Symbol)); 1384 ns->name = (char *) emalloc((int) strlen(s->name) + 4); 1385 sprintf(ns->name, "%s%d", s->name, modifier); 1386 1387 context = s->context; 1388 set_lab(ns, to); 1389 usedit++; 1390 } 1391 context = oc; /* restore */ 1392 if (usedit) 1393 { if (modifier++ > 990) 1394 fatal("modifier overflow error", (char *) 0); 1395 } 1396 } 1397 1398 static int 1399 case_cache(Element *e, int a) 1400 { int bupcase = 0, casenr = uniq, fromcache = 0; 1401 CaseCache *Cached = (CaseCache *) 0; 1402 Element *f, *g; 1403 int j, nrbups, mark, target; 1404 extern int ccache; 1405 1406 mark = (e->status&ATOM); /* could lose atomicity in a merge chain */ 1407 1408 if (e->merge_mark > 0 1409 || (merger && e->merge_in == 0)) 1410 { /* state nominally unreachable (part of merge chains) */ 1411 if (e->n->ntyp != '.' 1412 && e->n->ntyp != GOTO) 1413 { fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno); 1414 fprintf(tt, "settr(0,0,0,0,0,\""); 1415 comment(tt, e->n, e->seqno); 1416 fprintf(tt, "\",0,0,0);\n"); 1417 } else 1418 { fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno); 1419 casenr = 1; /* mhs example */ 1420 j = a; 1421 goto haveit; /* pakula's example */ 1422 } 1423 1424 return -1; 1425 } 1426 1427 fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno); 1428 1429 if (ccache 1430 && Pid != claimnr 1431 && Pid != eventmapnr 1432 && (Cached = prev_case(e, Pid))) 1433 { bupcase = Cached->b; 1434 casenr = Cached->m; 1435 fromcache = 1; 1436 1437 fprintf(tm, "/* STATE %d - line %d %s - [", 1438 e->seqno, e->n->ln, e->n->fn->name); 1439 comment(tm, e->n, 0); 1440 fprintf(tm, "] (%d:%d - %d) same as %d (%d:%d - %d) */\n", 1441 e->merge_start, e->merge, e->merge_in, 1442 casenr, 1443 Cached->e->merge_start, Cached->e->merge, Cached->e->merge_in); 1444 1445 goto gotit; 1446 } 1447 1448 fprintf(tm, "\tcase %d: /* STATE %d - line %d %s - [", 1449 uniq++, e->seqno, e->n->ln, e->n->fn->name); 1450 comment(tm, e->n, 0); 1451 nrbups = (e->merge || e->merge_start) ? nrhops(e) : nr_bup(e); 1452 fprintf(tm, "] (%d:%d:%d - %d) */\n\t\t", 1453 e->merge_start, e->merge, nrbups, e->merge_in); 1454 1455 if (nrbups > MAXMERGE-1) 1456 fatal("merge requires more than 256 bups", (char *)0); 1457 1458 if (e->n->ntyp != 'r' && Pid != claimnr && Pid != eventmapnr) 1459 fprintf(tm, "IfNotBlocked\n\t\t"); 1460 1461 if (multi_needed != 0 || multi_undo != 0) 1462 fatal("cannot happen, case_cache", (char *) 0); 1463 1464 if (nrbups > 1) 1465 { multi_oval = 1; 1466 multi_needed = nrbups; /* allocated after edge condition */ 1467 } else 1468 multi_oval = 0; 1469 1470 memset(CnT, 0, sizeof(CnT)); 1471 YZmax = YZcnt = 0; 1472 1473 /* the src xrefs have the numbers in e->seqno builtin */ 1474 fprintf(tm, "reached[%d][%d] = 1;\n\t\t", Pid, e->seqno); 1475 1476 doforward(tm, e); 1477 1478 if (e->merge_start) 1479 target = e->merge_start; 1480 else 1481 target = e->merge; 1482 1483 if (target) 1484 { f = e; 1485 1486 more: if (f->n->ntyp == GOTO) 1487 { g = get_lab(f->n, 1); 1488 if (g->seqno == target) 1489 f = g; 1490 else 1491 f = huntele(g, f->status, target); 1492 } else 1493 f = f->nxt; 1494 1495 1496 if (f && f->seqno != target) 1497 { if (!f->merge && !f->merge_single) 1498 { fprintf(tm, "/* stop at bad hop %d, %d */\n\t\t", 1499 f->seqno, target); 1500 goto out; 1501 } 1502 fprintf(tm, "/* merge: "); 1503 comment(tm, f->n, 0); 1504 fprintf(tm, "(%d, %d, %d) */\n\t\t", f->merge, f->seqno, target); 1505 fprintf(tm, "reached[%d][%d] = 1;\n\t\t", Pid, f->seqno); 1506 YZcnt++; 1507 lab_transfer(e, f); 1508 mark = f->status&(ATOM|L_ATOM); /* last step wins */ 1509 doforward(tm, f); 1510 if (f->merge_in == 1) f->merge_mark++; 1511 1512 goto more; 1513 } } 1514 out: 1515 fprintf(tm, "_m = %d", getweight(e->n)); 1516 if (m_loss && e->n->ntyp == 's') fprintf(tm, "+delta_m; delta_m = 0"); 1517 fprintf(tm, "; goto P999; /* %d */\n", YZcnt); 1518 1519 multi_needed = 0; 1520 didcase = 0; 1521 1522 if (target) 1523 lastfirst(target, e, casenr); /* mergesteps only */ 1524 1525 dobackward(e, casenr); /* the original step */ 1526 1527 fprintf(tb, ";\n\t\t"); 1528 1529 if (e->merge || e->merge_start) 1530 { if (!didcase) 1531 { fprintf(tb, "\n\tcase %d: ", casenr); 1532 fprintf(tb, "/* STATE %d */", e->seqno); 1533 didcase++; 1534 } else 1535 fprintf(tb, ";"); 1536 } else 1537 fprintf(tb, ";"); 1538 fprintf(tb, "\n\t\t"); 1539 1540 if (multi_undo) 1541 { fprintf(tb, "ungrab_ints(trpt->bup.ovals, %d);\n\t\t", 1542 multi_undo); 1543 multi_undo = 0; 1544 } 1545 if (didcase) 1546 { fprintf(tb, "goto R999;\n"); 1547 bupcase = casenr; 1548 } 1549 1550 if (!e->merge && !e->merge_start) 1551 new_case(e, casenr, bupcase, Pid); 1552 1553 gotit: 1554 j = a; 1555 if (e->merge_start) 1556 j = e->merge_start; 1557 else if (e->merge) 1558 j = e->merge; 1559 haveit: 1560 fprintf(tt, "%ssettr(%d,%d,%d,%d,%d,\"", fromcache?"/* c */ ":"", 1561 e->Seqno, mark, j, casenr, bupcase); 1562 1563 return (fromcache)?0:casenr; 1564 } 1565 1566 static void 1567 put_el(Element *e, int Tt0, int Tt1) 1568 { int a, casenr, Global_ref; 1569 Element *g = ZE; 1570 1571 if (e->n->ntyp == GOTO) 1572 { g = get_lab(e->n, 1); 1573 g = huntele(g, e->status, -1); 1574 cross_dsteps(e->n, g->n); 1575 a = g->seqno; 1576 } else if (e->nxt) 1577 { g = huntele(e->nxt, e->status, -1); 1578 a = g->seqno; 1579 } else 1580 a = 0; 1581 if (g 1582 && (g->status&CHECK2 /* entering remotely ref'd state */ 1583 || e->status&CHECK2)) /* leaving remotely ref'd state */ 1584 e->status |= I_GLOB; 1585 1586 /* don't remove dead edges in here, to preserve structure of fsm */ 1587 if (e->merge_start || e->merge) 1588 goto non_generic; 1589 1590 /*** avoid duplicate or redundant cases in pan.m ***/ 1591 switch (e->n->ntyp) { 1592 case ELSE: 1593 casenr = 2; /* standard else */ 1594 putskip(e->seqno); 1595 goto generic_case; 1596 /* break; */ 1597 case '.': 1598 case GOTO: 1599 case BREAK: 1600 putskip(e->seqno); 1601 casenr = 1; /* standard goto */ 1602 generic_case: fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno); 1603 fprintf(tt, "settr(%d,%d,%d,%d,0,\"", 1604 e->Seqno, e->status&ATOM, a, casenr); 1605 break; 1606 #ifndef PRINTF 1607 case PRINT: 1608 goto non_generic; 1609 case PRINTM: 1610 goto non_generic; 1611 #endif 1612 case 'c': 1613 if (e->n->lft->ntyp == CONST 1614 && e->n->lft->val == 1) /* skip or true */ 1615 { casenr = 1; 1616 putskip(e->seqno); 1617 goto generic_case; 1618 } 1619 goto non_generic; 1620 1621 default: 1622 non_generic: 1623 casenr = case_cache(e, a); 1624 if (casenr < 0) return; /* unreachable state */ 1625 break; 1626 } 1627 /* tailend of settr(...); */ 1628 Global_ref = (e->status&I_GLOB)?1:has_global(e->n); 1629 comment(tt, e->n, e->seqno); 1630 fprintf(tt, "\", %d, ", Global_ref); 1631 if (Tt0 != 2) 1632 { fprintf(tt, "%d, %d);", Tt0, Tt1); 1633 } else 1634 { Tpe(e->n); /* sets EPT */ 1635 fprintf(tt, "%d, %d);", EPT[0], EPT[1]); 1636 } 1637 if ((e->merge_start && e->merge_start != a) 1638 || (e->merge && e->merge != a)) 1639 { fprintf(tt, " /* m: %d -> %d,%d */\n", 1640 a, e->merge_start, e->merge); 1641 fprintf(tt, " reached%d[%d] = 1;", 1642 Pid, a); /* Sheinman's example */ 1643 } 1644 fprintf(tt, "\n"); 1645 1646 if (casenr > 2) 1647 tr_map(casenr, e); 1648 put_escp(e); 1649 } 1650 1651 static void 1652 nested_unless(Element *e, Element *g) 1653 { struct SeqList *y = e->esc, *z = g->esc; 1654 1655 for ( ; y && z; y = y->nxt, z = z->nxt) 1656 if (z->this != y->this) 1657 break; 1658 if (!y && !z) 1659 return; 1660 1661 if (g->n->ntyp != GOTO 1662 && g->n->ntyp != '.' 1663 && e->sub->nxt) 1664 { printf("error: (%s:%d) saw 'unless' on a guard:\n", 1665 (e->n)?e->n->fn->name:"-", 1666 (e->n)?e->n->ln:0); 1667 printf("=====>instead of\n"); 1668 printf(" do (or if)\n"); 1669 printf(" :: ...\n"); 1670 printf(" :: stmnt1 unless stmnt2\n"); 1671 printf(" od (of fi)\n"); 1672 printf("=====>use\n"); 1673 printf(" do (or if)\n"); 1674 printf(" :: ...\n"); 1675 printf(" :: stmnt1\n"); 1676 printf(" od (or fi) unless stmnt2\n"); 1677 printf("=====>or rewrite\n"); 1678 } 1679 } 1680 1681 static void 1682 put_seq(Sequence *s, int Tt0, int Tt1) 1683 { SeqList *h; 1684 Element *e, *g; 1685 int a, deadlink; 1686 1687 if (0) printf("put_seq %d\n", s->frst->seqno); 1688 1689 for (e = s->frst; e; e = e->nxt) 1690 { 1691 if (0) printf(" step %d\n", e->seqno); 1692 if (e->status & DONE) 1693 { 1694 if (0) printf(" done before\n"); 1695 goto checklast; 1696 } 1697 e->status |= DONE; 1698 1699 if (e->n->ln) 1700 putsrc(e); 1701 1702 if (e->n->ntyp == UNLESS) 1703 { 1704 if (0) printf(" an unless\n"); 1705 put_seq(e->sub->this, Tt0, Tt1); 1706 } else if (e->sub) 1707 { 1708 if (0) printf(" has sub\n"); 1709 fprintf(tt, "\tT = trans[%d][%d] = ", 1710 Pid, e->seqno); 1711 fprintf(tt, "settr(%d,%d,0,0,0,\"", 1712 e->Seqno, e->status&ATOM); 1713 comment(tt, e->n, e->seqno); 1714 if (e->status&CHECK2) 1715 e->status |= I_GLOB; 1716 fprintf(tt, "\", %d, %d, %d);", 1717 (e->status&I_GLOB)?1:0, Tt0, Tt1); 1718 blurb(tt, e); 1719 for (h = e->sub; h; h = h->nxt) 1720 { putskip(h->this->frst->seqno); 1721 g = huntstart(h->this->frst); 1722 if (g->esc) 1723 nested_unless(e, g); 1724 a = g->seqno; 1725 1726 if (g->n->ntyp == 'c' 1727 && g->n->lft->ntyp == CONST 1728 && g->n->lft->val == 0 /* 0 or false */ 1729 && !g->esc) 1730 { fprintf(tt, "#if 0\n\t/* dead link: */\n"); 1731 deadlink = 1; 1732 if (verbose&32) 1733 printf("spin: line %3d %s, Warning: condition is always false\n", 1734 g->n->ln, g->n->fn?g->n->fn->name:""); 1735 } else 1736 deadlink = 0; 1737 if (0) printf(" settr %d %d\n", a, 0); 1738 if (h->nxt) 1739 fprintf(tt, "\tT = T->nxt\t= "); 1740 else 1741 fprintf(tt, "\t T->nxt\t= "); 1742 fprintf(tt, "settr(%d,%d,%d,0,0,\"", 1743 e->Seqno, e->status&ATOM, a); 1744 comment(tt, e->n, e->seqno); 1745 if (g->status&CHECK2) 1746 h->this->frst->status |= I_GLOB; 1747 fprintf(tt, "\", %d, %d, %d);", 1748 (h->this->frst->status&I_GLOB)?1:0, 1749 Tt0, Tt1); 1750 blurb(tt, e); 1751 if (deadlink) 1752 fprintf(tt, "#endif\n"); 1753 } 1754 for (h = e->sub; h; h = h->nxt) 1755 put_seq(h->this, Tt0, Tt1); 1756 } else 1757 { 1758 if (0) printf(" [non]atomic %d\n", e->n->ntyp); 1759 if (e->n->ntyp == ATOMIC 1760 || e->n->ntyp == D_STEP 1761 || e->n->ntyp == NON_ATOMIC) 1762 put_sub(e, Tt0, Tt1); 1763 else 1764 { 1765 if (0) printf(" put_el %d\n", e->seqno); 1766 put_el(e, Tt0, Tt1); 1767 } 1768 } 1769 checklast: if (e == s->last) 1770 break; 1771 } 1772 if (0) printf("put_seq done\n"); 1773 } 1774 1775 static void 1776 patch_atomic(Sequence *s) /* catch goto's that break the chain */ 1777 { Element *f, *g; 1778 SeqList *h; 1779 1780 for (f = s->frst; f ; f = f->nxt) 1781 { 1782 if (f->n && f->n->ntyp == GOTO) 1783 { g = get_lab(f->n,1); 1784 cross_dsteps(f->n, g->n); 1785 if ((f->status & (ATOM|L_ATOM)) 1786 && !(g->status & (ATOM|L_ATOM))) 1787 { f->status &= ~ATOM; 1788 f->status |= L_ATOM; 1789 } 1790 /* bridge atomics */ 1791 if ((f->status & L_ATOM) 1792 && (g->status & (ATOM|L_ATOM))) 1793 { f->status &= ~L_ATOM; 1794 f->status |= ATOM; 1795 } 1796 } else 1797 for (h = f->sub; h; h = h->nxt) 1798 patch_atomic(h->this); 1799 if (f == s->extent) 1800 break; 1801 } 1802 } 1803 1804 static void 1805 mark_seq(Sequence *s) 1806 { Element *f; 1807 SeqList *h; 1808 1809 for (f = s->frst; f; f = f->nxt) 1810 { f->status |= I_GLOB; 1811 1812 if (f->n->ntyp == ATOMIC 1813 || f->n->ntyp == NON_ATOMIC 1814 || f->n->ntyp == D_STEP) 1815 mark_seq(f->n->sl->this); 1816 1817 for (h = f->sub; h; h = h->nxt) 1818 mark_seq(h->this); 1819 if (f == s->last) 1820 return; 1821 } 1822 } 1823 1824 static Element * 1825 find_target(Element *e) 1826 { Element *f; 1827 1828 if (!e) return e; 1829 1830 if (t_cyc++ > 32) 1831 { fatal("cycle of goto jumps", (char *) 0); 1832 } 1833 switch (e->n->ntyp) { 1834 case GOTO: 1835 f = get_lab(e->n,1); 1836 cross_dsteps(e->n, f->n); 1837 f = find_target(f); 1838 break; 1839 case BREAK: 1840 if (e->nxt) 1841 f = find_target(huntele(e->nxt, e->status, -1)); 1842 /* else fall through */ 1843 default: 1844 f = e; 1845 break; 1846 } 1847 return f; 1848 } 1849 1850 Element * 1851 target(Element *e) 1852 { 1853 if (!e) return e; 1854 lineno = e->n->ln; 1855 Fname = e->n->fn; 1856 t_cyc = 0; 1857 return find_target(e); 1858 } 1859 1860 static int 1861 scan_seq(Sequence *s) 1862 { Element *f, *g; 1863 SeqList *h; 1864 1865 for (f = s->frst; f; f = f->nxt) 1866 { if ((f->status&CHECK2) 1867 || has_global(f->n)) 1868 return 1; 1869 if (f->n->ntyp == GOTO) /* may reach other atomic */ 1870 { g = target(f); 1871 if (g 1872 && !(f->status & L_ATOM) 1873 && !(g->status & (ATOM|L_ATOM))) 1874 { fprintf(tt, " /* goto mark-down, "); 1875 fprintf(tt, "line %d - %d */\n", 1876 f->n->ln, (g->n)?g->n->ln:0); 1877 return 1; /* assume worst case */ 1878 } } 1879 for (h = f->sub; h; h = h->nxt) 1880 if (scan_seq(h->this)) 1881 return 1; 1882 if (f == s->last) 1883 break; 1884 } 1885 return 0; 1886 } 1887 1888 static int 1889 glob_args(Lextok *n) 1890 { int result = 0; 1891 Lextok *v; 1892 1893 for (v = n->rgt; v; v = v->rgt) 1894 { if (v->lft->ntyp == CONST) 1895 continue; 1896 if (v->lft->ntyp == EVAL) 1897 result += has_global(v->lft->lft); 1898 else 1899 result += has_global(v->lft); 1900 } 1901 return result; 1902 } 1903 1904 int 1905 has_global(Lextok *n) 1906 { Lextok *v; extern int runsafe; 1907 1908 if (!n) return 0; 1909 if (AllGlobal) return 1; /* global provided clause */ 1910 1911 switch (n->ntyp) { 1912 case ATOMIC: 1913 case D_STEP: 1914 case NON_ATOMIC: 1915 return scan_seq(n->sl->this); 1916 1917 case '.': 1918 case BREAK: 1919 case GOTO: 1920 case CONST: 1921 return 0; 1922 1923 case ELSE: return n->val; /* true if combined with chan refs */ 1924 1925 case 's': return glob_args(n)!=0 || ((n->sym->xu&(XS|XX)) != XS); 1926 case 'r': return glob_args(n)!=0 || ((n->sym->xu&(XR|XX)) != XR); 1927 case 'R': return glob_args(n)!=0 || (((n->sym->xu)&(XR|XS|XX)) != (XR|XS)); 1928 case NEMPTY: return ((n->sym->xu&(XR|XX)) != XR); 1929 case NFULL: return ((n->sym->xu&(XS|XX)) != XS); 1930 case FULL: return ((n->sym->xu&(XR|XX)) != XR); 1931 case EMPTY: return ((n->sym->xu&(XS|XX)) != XS); 1932 case LEN: return (((n->sym->xu)&(XR|XS|XX)) != (XR|XS)); 1933 1934 case NAME: 1935 if (n->sym->context 1936 || (n->sym->hidden&64) 1937 || strcmp(n->sym->name, "_pid") == 0 1938 || strcmp(n->sym->name, "_") == 0) 1939 return 0; 1940 return 1; 1941 1942 case RUN: return 1-runsafe; 1943 1944 case C_CODE: case C_EXPR: 1945 return glob_inline(n->sym->name); 1946 1947 case ENABLED: case PC_VAL: case NONPROGRESS: 1948 case 'p': case 'q': 1949 case TIMEOUT: 1950 return 1; 1951 1952 /* @ was 1 (global) since 2.8.5 1953 in 3.0 it is considered local and 1954 conditionally safe, provided: 1955 II is the youngest process 1956 and nrprocs < MAXPROCS 1957 */ 1958 case '@': return 0; 1959 1960 case '!': case UMIN: case '~': case ASSERT: 1961 return has_global(n->lft); 1962 1963 case '/': case '*': case '-': case '+': 1964 case '%': case LT: case GT: case '&': case '^': 1965 case '|': case LE: case GE: case NE: case '?': 1966 case EQ: case OR: case AND: case LSHIFT: 1967 case RSHIFT: case 'c': case ASGN: 1968 return has_global(n->lft) || has_global(n->rgt); 1969 1970 case PRINT: 1971 for (v = n->lft; v; v = v->rgt) 1972 if (has_global(v->lft)) return 1; 1973 return 0; 1974 case PRINTM: 1975 return has_global(n->lft); 1976 } 1977 return 0; 1978 } 1979 1980 static void 1981 Bailout(FILE *fd, char *str) 1982 { 1983 if (!GenCode) 1984 fprintf(fd, "continue%s", str); 1985 else if (IsGuard) 1986 fprintf(fd, "%s%s", NextLab[Level], str); 1987 else 1988 fprintf(fd, "Uerror(\"block in step seq\")%s", str); 1989 } 1990 1991 #define cat0(x) putstmnt(fd,now->lft,m); fprintf(fd, x); \ 1992 putstmnt(fd,now->rgt,m) 1993 #define cat1(x) fprintf(fd,"("); cat0(x); fprintf(fd,")") 1994 #define cat2(x,y) fprintf(fd,x); putstmnt(fd,y,m) 1995 #define cat3(x,y,z) fprintf(fd,x); putstmnt(fd,y,m); fprintf(fd,z) 1996 1997 void 1998 putstmnt(FILE *fd, Lextok *now, int m) 1999 { Lextok *v; 2000 int i, j; 2001 2002 if (!now) { fprintf(fd, "0"); return; } 2003 lineno = now->ln; 2004 Fname = now->fn; 2005 2006 switch (now->ntyp) { 2007 case CONST: fprintf(fd, "%d", now->val); break; 2008 case '!': cat3(" !(", now->lft, ")"); break; 2009 case UMIN: cat3(" -(", now->lft, ")"); break; 2010 case '~': cat3(" ~(", now->lft, ")"); break; 2011 2012 case '/': cat1("/"); break; 2013 case '*': cat1("*"); break; 2014 case '-': cat1("-"); break; 2015 case '+': cat1("+"); break; 2016 case '%': cat1("%%"); break; 2017 case '&': cat1("&"); break; 2018 case '^': cat1("^"); break; 2019 case '|': cat1("|"); break; 2020 case LT: cat1("<"); break; 2021 case GT: cat1(">"); break; 2022 case LE: cat1("<="); break; 2023 case GE: cat1(">="); break; 2024 case NE: cat1("!="); break; 2025 case EQ: cat1("=="); break; 2026 case OR: cat1("||"); break; 2027 case AND: cat1("&&"); break; 2028 case LSHIFT: cat1("<<"); break; 2029 case RSHIFT: cat1(">>"); break; 2030 2031 case TIMEOUT: 2032 if (separate == 2) 2033 fprintf(fd, "((tau)&1)"); 2034 else 2035 fprintf(fd, "((trpt->tau)&1)"); 2036 if (GenCode) 2037 printf("spin: line %3d, warning: 'timeout' in d_step sequence\n", 2038 lineno); 2039 /* is okay as a guard */ 2040 break; 2041 2042 case RUN: 2043 if (claimproc 2044 && strcmp(now->sym->name, claimproc) == 0) 2045 fatal("claim %s, (not runnable)", claimproc); 2046 if (eventmap 2047 && strcmp(now->sym->name, eventmap) == 0) 2048 fatal("eventmap %s, (not runnable)", eventmap); 2049 2050 if (GenCode) 2051 fatal("'run' in d_step sequence (use atomic)", 2052 (char *)0); 2053 2054 fprintf(fd,"addproc(%d", fproc(now->sym->name)); 2055 for (v = now->lft, i = 0; v; v = v->rgt, i++) 2056 { cat2(", ", v->lft); 2057 } 2058 2059 if (i > Npars) 2060 { printf(" %d parameters used, %d expected\n", i, Npars); 2061 fatal("too many parameters in run %s(...)", 2062 now->sym->name); 2063 } 2064 for ( ; i < Npars; i++) 2065 fprintf(fd, ", 0"); 2066 fprintf(fd, ")"); 2067 break; 2068 2069 case ENABLED: 2070 cat3("enabled(II, ", now->lft, ")"); 2071 break; 2072 2073 case NONPROGRESS: 2074 /* o_pm&4=progress, tau&128=claim stutter */ 2075 if (separate == 2) 2076 fprintf(fd, "(!(o_pm&4) && !(tau&128))"); 2077 else 2078 fprintf(fd, "(!(trpt->o_pm&4) && !(trpt->tau&128))"); 2079 break; 2080 2081 case PC_VAL: 2082 cat3("((P0 *) Pptr(", now->lft, "+BASE))->_p"); 2083 break; 2084 2085 case LEN: 2086 if (!terse && !TestOnly && has_xu) 2087 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 2088 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || "); 2089 putname(fd, "q_R_check(", now->lft, m, ""); 2090 fprintf(fd, ", II)) &&\n\t\t"); 2091 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || "); 2092 putname(fd, "q_S_check(", now->lft, m, ", II)) &&"); 2093 fprintf(fd, "\n#endif\n\t\t"); 2094 } 2095 putname(fd, "q_len(", now->lft, m, ")"); 2096 break; 2097 2098 case FULL: 2099 if (!terse && !TestOnly && has_xu) 2100 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 2101 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || "); 2102 putname(fd, "q_R_check(", now->lft, m, ""); 2103 fprintf(fd, ", II)) &&\n\t\t"); 2104 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || "); 2105 putname(fd, "q_S_check(", now->lft, m, ", II)) &&"); 2106 fprintf(fd, "\n#endif\n\t\t"); 2107 } 2108 putname(fd, "q_full(", now->lft, m, ")"); 2109 break; 2110 2111 case EMPTY: 2112 if (!terse && !TestOnly && has_xu) 2113 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 2114 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || "); 2115 putname(fd, "q_R_check(", now->lft, m, ""); 2116 fprintf(fd, ", II)) &&\n\t\t"); 2117 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || "); 2118 putname(fd, "q_S_check(", now->lft, m, ", II)) &&"); 2119 fprintf(fd, "\n#endif\n\t\t"); 2120 } 2121 putname(fd, "(q_len(", now->lft, m, ")==0)"); 2122 break; 2123 2124 case NFULL: 2125 if (!terse && !TestOnly && has_xu) 2126 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 2127 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || "); 2128 putname(fd, "q_S_check(", now->lft, m, ", II)) &&"); 2129 fprintf(fd, "\n#endif\n\t\t"); 2130 } 2131 putname(fd, "(!q_full(", now->lft, m, "))"); 2132 break; 2133 2134 case NEMPTY: 2135 if (!terse && !TestOnly && has_xu) 2136 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 2137 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || "); 2138 putname(fd, "q_R_check(", now->lft, m, ", II)) &&"); 2139 fprintf(fd, "\n#endif\n\t\t"); 2140 } 2141 putname(fd, "(q_len(", now->lft, m, ")>0)"); 2142 break; 2143 2144 case 's': 2145 if (Pid == eventmapnr) 2146 { fprintf(fd, "if ((ot == EVENT_TRACE && _tp != 's') "); 2147 putname(fd, "|| _qid+1 != ", now->lft, m, ""); 2148 for (v = now->rgt, i=0; v; v = v->rgt, i++) 2149 { if (v->lft->ntyp != CONST 2150 && v->lft->ntyp != EVAL) 2151 continue; 2152 fprintf(fd, " \\\n\t\t|| qrecv("); 2153 putname(fd, "", now->lft, m, ", "); 2154 putname(fd, "q_len(", now->lft, m, ")-1, "); 2155 fprintf(fd, "%d, 0) != ", i); 2156 if (v->lft->ntyp == CONST) 2157 putstmnt(fd, v->lft, m); 2158 else /* EVAL */ 2159 putstmnt(fd, v->lft->lft, m); 2160 } 2161 fprintf(fd, ")\n"); 2162 fprintf(fd, "\t\t continue"); 2163 putname(th, " || (x_y3_ == ", now->lft, m, ")"); 2164 break; 2165 } 2166 if (TestOnly) 2167 { if (m_loss) 2168 fprintf(fd, "1"); 2169 else 2170 putname(fd, "!q_full(", now->lft, m, ")"); 2171 break; 2172 } 2173 if (has_xu) 2174 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 2175 putname(fd, "if (q_claim[", now->lft, m, "]&2) "); 2176 putname(fd, "q_S_check(", now->lft, m, ", II);"); 2177 fprintf(fd, "\n#endif\n\t\t"); 2178 } 2179 fprintf(fd, "if (q_%s", 2180 (u_sync > 0 && u_async == 0)?"len":"full"); 2181 putname(fd, "(", now->lft, m, "))\n"); 2182 2183 if (m_loss) 2184 fprintf(fd, "\t\t{ nlost++; delta_m = 1; } else {"); 2185 else 2186 { fprintf(fd, "\t\t\t"); 2187 Bailout(fd, ";"); 2188 } 2189 2190 if (has_enabled) 2191 fprintf(fd, "\n\t\tif (TstOnly) return 1;"); 2192 2193 if (u_sync && !u_async && rvopt) 2194 fprintf(fd, "\n\n\t\tif (no_recvs(II)) continue;\n"); 2195 2196 fprintf(fd, "\n#ifdef HAS_CODE\n"); 2197 fprintf(fd, "\t\tif (readtrail && gui) {\n"); 2198 fprintf(fd, "\t\t\tchar simtmp[32];\n"); 2199 putname(fd, "\t\t\tsprintf(simvals, \"%%d!\", ", now->lft, m, ");\n"); 2200 _isok++; 2201 for (v = now->rgt, i = 0; v; v = v->rgt, i++) 2202 { cat3("\t\tsprintf(simtmp, \"%%d\", ", v->lft, "); strcat(simvals, simtmp);"); 2203 if (v->rgt) 2204 fprintf(fd, "\t\tstrcat(simvals, \",\");\n"); 2205 } 2206 _isok--; 2207 fprintf(fd, "\t\t}\n"); 2208 fprintf(fd, "#endif\n\t\t"); 2209 2210 putname(fd, "\n\t\tqsend(", now->lft, m, ""); 2211 fprintf(fd, ", %d", now->val); 2212 for (v = now->rgt, i = 0; v; v = v->rgt, i++) 2213 { cat2(", ", v->lft); 2214 } 2215 if (i > Mpars) 2216 { terse++; 2217 putname(stdout, "channel name: ", now->lft, m, "\n"); 2218 terse--; 2219 printf(" %d msg parameters sent, %d expected\n", i, Mpars); 2220 fatal("too many pars in send", ""); 2221 } 2222 for ( ; i < Mpars; i++) 2223 fprintf(fd, ", 0"); 2224 fprintf(fd, ")"); 2225 if (u_sync) 2226 { fprintf(fd, ";\n\t\t"); 2227 if (u_async) 2228 putname(fd, "if (q_zero(", now->lft, m, ")) "); 2229 putname(fd, "{ boq = ", now->lft, m, ""); 2230 if (GenCode) 2231 fprintf(fd, "; Uerror(\"rv-attempt in d_step\")"); 2232 fprintf(fd, "; }"); 2233 } 2234 if (m_loss) 2235 fprintf(fd, ";\n\t\t}\n\t\t"); /* end of m_loss else */ 2236 break; 2237 2238 case 'r': 2239 if (Pid == eventmapnr) 2240 { fprintf(fd, "if ((ot == EVENT_TRACE && _tp != 'r') "); 2241 putname(fd, "|| _qid+1 != ", now->lft, m, ""); 2242 for (v = now->rgt, i=0; v; v = v->rgt, i++) 2243 { if (v->lft->ntyp != CONST 2244 && v->lft->ntyp != EVAL) 2245 continue; 2246 fprintf(fd, " \\\n\t\t|| qrecv("); 2247 putname(fd, "", now->lft, m, ", "); 2248 fprintf(fd, "0, %d, 0) != ", i); 2249 if (v->lft->ntyp == CONST) 2250 putstmnt(fd, v->lft, m); 2251 else /* EVAL */ 2252 putstmnt(fd, v->lft->lft, m); 2253 } 2254 fprintf(fd, ")\n"); 2255 fprintf(fd, "\t\t continue"); 2256 2257 putname(tc, " || (x_y3_ == ", now->lft, m, ")"); 2258 2259 break; 2260 } 2261 if (TestOnly) 2262 { fprintf(fd, "(("); 2263 if (u_sync) fprintf(fd, "(boq == -1 && "); 2264 2265 putname(fd, "q_len(", now->lft, m, ")"); 2266 2267 if (u_sync && now->val <= 1) 2268 { putname(fd, ") || (boq == ", now->lft,m," && "); 2269 putname(fd, "q_zero(", now->lft,m,"))"); 2270 } 2271 2272 fprintf(fd, ")"); 2273 if (now->val == 0 || now->val == 2) 2274 { for (v = now->rgt, i=j=0; v; v = v->rgt, i++) 2275 { if (v->lft->ntyp == CONST) 2276 { cat3("\n\t\t&& (", v->lft, " == "); 2277 putname(fd, "qrecv(", now->lft, m, ", "); 2278 fprintf(fd, "0, %d, 0))", i); 2279 } else if (v->lft->ntyp == EVAL) 2280 { cat3("\n\t\t&& (", v->lft->lft, " == "); 2281 putname(fd, "qrecv(", now->lft, m, ", "); 2282 fprintf(fd, "0, %d, 0))", i); 2283 } else 2284 { j++; continue; 2285 } 2286 } 2287 } else 2288 { fprintf(fd, "\n\t\t&& Q_has("); 2289 putname(fd, "", now->lft, m, ""); 2290 for (v = now->rgt, i=0; v; v = v->rgt, i++) 2291 { if (v->lft->ntyp == CONST) 2292 { fprintf(fd, ", 1, "); 2293 putstmnt(fd, v->lft, m); 2294 } else if (v->lft->ntyp == EVAL) 2295 { fprintf(fd, ", 1, "); 2296 putstmnt(fd, v->lft->lft, m); 2297 } else 2298 { fprintf(fd, ", 0, 0"); 2299 } } 2300 for ( ; i < Mpars; i++) 2301 fprintf(fd, ", 0, 0"); 2302 fprintf(fd, ")"); 2303 } 2304 fprintf(fd, ")"); 2305 break; 2306 } 2307 if (has_xu) 2308 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 2309 putname(fd, "if (q_claim[", now->lft, m, "]&1) "); 2310 putname(fd, "q_R_check(", now->lft, m, ", II);"); 2311 fprintf(fd, "\n#endif\n\t\t"); 2312 } 2313 if (u_sync) 2314 { if (now->val >= 2) 2315 { if (u_async) 2316 { fprintf(fd, "if ("); 2317 putname(fd, "q_zero(", now->lft,m,"))"); 2318 fprintf(fd, "\n\t\t{\t"); 2319 } 2320 fprintf(fd, "uerror(\"polling "); 2321 fprintf(fd, "rv chan\");\n\t\t"); 2322 if (u_async) 2323 fprintf(fd, " continue;\n\t\t}\n\t\t"); 2324 fprintf(fd, "IfNotBlocked\n\t\t"); 2325 } else 2326 { fprintf(fd, "if ("); 2327 if (u_async == 0) 2328 putname(fd, "boq != ", now->lft,m,") "); 2329 else 2330 { putname(fd, "q_zero(", now->lft,m,"))"); 2331 fprintf(fd, "\n\t\t{\tif (boq != "); 2332 putname(fd, "", now->lft,m,") "); 2333 Bailout(fd, ";\n\t\t} else\n\t\t"); 2334 fprintf(fd, "{\tif (boq != -1) "); 2335 } 2336 Bailout(fd, ";\n\t\t"); 2337 if (u_async) 2338 fprintf(fd, "}\n\t\t"); 2339 } } 2340 putname(fd, "if (q_len(", now->lft, m, ") == 0) "); 2341 Bailout(fd, ""); 2342 2343 for (v = now->rgt, j=0; v; v = v->rgt) 2344 { if (v->lft->ntyp != CONST 2345 && v->lft->ntyp != EVAL) 2346 j++; /* count settables */ 2347 } 2348 fprintf(fd, ";\n\n\t\tXX=1"); 2349 /* test */ if (now->val == 0 || now->val == 2) 2350 { for (v = now->rgt, i=0; v; v = v->rgt, i++) 2351 { if (v->lft->ntyp == CONST) 2352 { fprintf(fd, ";\n\t\t"); 2353 cat3("if (", v->lft, " != "); 2354 putname(fd, "qrecv(", now->lft, m, ", "); 2355 fprintf(fd, "0, %d, 0)) ", i); 2356 Bailout(fd, ""); 2357 } else if (v->lft->ntyp == EVAL) 2358 { fprintf(fd, ";\n\t\t"); 2359 cat3("if (", v->lft->lft, " != "); 2360 putname(fd, "qrecv(", now->lft, m, ", "); 2361 fprintf(fd, "0, %d, 0)) ", i); 2362 Bailout(fd, ""); 2363 } } 2364 } else /* random receive: val 1 or 3 */ 2365 { fprintf(fd, ";\n\t\tif (!(XX = Q_has("); 2366 putname(fd, "", now->lft, m, ""); 2367 for (v = now->rgt, i=0; v; v = v->rgt, i++) 2368 { if (v->lft->ntyp == CONST) 2369 { fprintf(fd, ", 1, "); 2370 putstmnt(fd, v->lft, m); 2371 } else if (v->lft->ntyp == EVAL) 2372 { fprintf(fd, ", 1, "); 2373 putstmnt(fd, v->lft->lft, m); 2374 } else 2375 { fprintf(fd, ", 0, 0"); 2376 } } 2377 for ( ; i < Mpars; i++) 2378 fprintf(fd, ", 0, 0"); 2379 fprintf(fd, "))) "); 2380 Bailout(fd, ""); 2381 fprintf(fd, ";\n\t\t"); 2382 if (multi_oval) 2383 { check_needed(); 2384 fprintf(fd, "(trpt+1)->bup.ovals[%d] = ", 2385 multi_oval-1); 2386 multi_oval++; 2387 } else 2388 fprintf(fd, "(trpt+1)->bup.oval = "); 2389 fprintf(fd, "XX"); 2390 } 2391 2392 if (has_enabled) 2393 fprintf(fd, ";\n\t\tif (TstOnly) return 1"); 2394 2395 if (j == 0 && now->val >= 2) 2396 { fprintf(fd, ";\n\t\t"); 2397 break; /* poll without side-effect */ 2398 } 2399 2400 if (!GenCode) 2401 { int jj = 0; 2402 fprintf(fd, ";\n\t\t"); 2403 /* no variables modified */ 2404 if (j == 0 && now->val == 0) 2405 { fprintf(fd, "if (q_flds[((Q0 *)qptr("); 2406 putname(fd, "", now->lft, m, "-1))->_t]"); 2407 fprintf(fd, " != %d)\n\t", i); 2408 fprintf(fd, "\t\tUerror(\"wrong nr of msg fields in rcv\");\n\t\t"); 2409 } 2410 2411 for (v = now->rgt; v; v = v->rgt) 2412 if ((v->lft->ntyp != CONST 2413 && v->lft->ntyp != EVAL)) 2414 jj++; /* nr of vars needing bup */ 2415 2416 if (jj) 2417 for (v = now->rgt, i = 0; v; v = v->rgt, i++) 2418 { char tempbuf[64]; 2419 2420 if ((v->lft->ntyp == CONST 2421 || v->lft->ntyp == EVAL)) 2422 continue; 2423 2424 if (multi_oval) 2425 { check_needed(); 2426 sprintf(tempbuf, "(trpt+1)->bup.ovals[%d] = ", 2427 multi_oval-1); 2428 multi_oval++; 2429 } else 2430 sprintf(tempbuf, "(trpt+1)->bup.oval = "); 2431 2432 if (v->lft->sym && !strcmp(v->lft->sym->name, "_")) 2433 { fprintf(fd, tempbuf); 2434 putname(fd, "qrecv(", now->lft, m, ""); 2435 fprintf(fd, ", XX-1, %d, 0);\n\t\t", i); 2436 } else 2437 { _isok++; 2438 cat3(tempbuf, v->lft, ";\n\t\t"); 2439 _isok--; 2440 } 2441 } 2442 2443 if (jj) /* check for double entries q?x,x */ 2444 { Lextok *w; 2445 2446 for (v = now->rgt; v; v = v->rgt) 2447 { if (v->lft->ntyp != CONST 2448 && v->lft->ntyp != EVAL 2449 && v->lft->sym 2450 && v->lft->sym->type != STRUCT /* not a struct */ 2451 && v->lft->sym->nel == 1 /* not an array */ 2452 && strcmp(v->lft->sym->name, "_") != 0) 2453 for (w = v->rgt; w; w = w->rgt) 2454 if (v->lft->sym == w->lft->sym) 2455 { fatal("cannot use var ('%s') in multiple msg fields", 2456 v->lft->sym->name); 2457 } } } 2458 } 2459 /* set */ for (v = now->rgt, i = 0; v; v = v->rgt, i++) 2460 { if ((v->lft->ntyp == CONST 2461 || v->lft->ntyp == EVAL) && v->rgt) 2462 continue; 2463 fprintf(fd, ";\n\t\t"); 2464 2465 if (v->lft->ntyp != CONST 2466 && v->lft->ntyp != EVAL 2467 && strcmp(v->lft->sym->name, "_") != 0) 2468 { nocast=1; 2469 _isok++; 2470 putstmnt(fd, v->lft, m); 2471 _isok--; 2472 nocast=0; 2473 fprintf(fd, " = "); 2474 } 2475 putname(fd, "qrecv(", now->lft, m, ", "); 2476 fprintf(fd, "XX-1, %d, ", i); 2477 fprintf(fd, "%d)", (v->rgt || now->val >= 2)?0:1); 2478 2479 if (v->lft->ntyp != CONST 2480 && v->lft->ntyp != EVAL 2481 && strcmp(v->lft->sym->name, "_") != 0 2482 && (v->lft->ntyp != NAME 2483 || v->lft->sym->type != CHAN)) 2484 { fprintf(fd, ";\n#ifdef VAR_RANGES"); 2485 fprintf(fd, "\n\t\tlogval(\""); 2486 withprocname = terse = nocast = 1; 2487 _isok++; 2488 putstmnt(fd,v->lft,m); 2489 withprocname = terse = nocast = 0; 2490 fprintf(fd, "\", "); 2491 putstmnt(fd,v->lft,m); 2492 _isok--; 2493 fprintf(fd, ");\n#endif\n"); 2494 fprintf(fd, "\t\t"); 2495 } 2496 } 2497 fprintf(fd, ";\n\t\t"); 2498 2499 fprintf(fd, "\n#ifdef HAS_CODE\n"); 2500 fprintf(fd, "\t\tif (readtrail && gui) {\n"); 2501 fprintf(fd, "\t\t\tchar simtmp[32];\n"); 2502 putname(fd, "\t\t\tsprintf(simvals, \"%%d?\", ", now->lft, m, ");\n"); 2503 _isok++; 2504 for (v = now->rgt, i = 0; v; v = v->rgt, i++) 2505 { if (v->lft->ntyp != EVAL) 2506 { cat3("\t\tsprintf(simtmp, \"%%d\", ", v->lft, "); strcat(simvals, simtmp);"); 2507 } else 2508 { cat3("\t\tsprintf(simtmp, \"%%d\", ", v->lft->lft, "); strcat(simvals, simtmp);"); 2509 } 2510 if (v->rgt) 2511 fprintf(fd, "\t\tstrcat(simvals, \",\");\n"); 2512 } 2513 _isok--; 2514 fprintf(fd, "\t\t}\n"); 2515 fprintf(fd, "#endif\n\t\t"); 2516 2517 if (u_sync) 2518 { putname(fd, "if (q_zero(", now->lft, m, "))"); 2519 fprintf(fd, "\n\t\t{ boq = -1;\n"); 2520 2521 fprintf(fd, "#ifndef NOFAIR\n"); /* NEW 3.0.8 */ 2522 fprintf(fd, "\t\t\tif (fairness\n"); 2523 fprintf(fd, "\t\t\t&& !(trpt->o_pm&32)\n"); 2524 fprintf(fd, "\t\t\t&& (now._a_t&2)\n"); 2525 fprintf(fd, "\t\t\t&& now._cnt[now._a_t&1] == II+2)\n"); 2526 fprintf(fd, "\t\t\t{ now._cnt[now._a_t&1] -= 1;\n"); 2527 fprintf(fd, "#ifdef VERI\n"); 2528 fprintf(fd, "\t\t\t if (II == 1)\n"); 2529 fprintf(fd, "\t\t\t now._cnt[now._a_t&1] = 1;\n"); 2530 fprintf(fd, "#endif\n"); 2531 fprintf(fd, "#ifdef DEBUG\n"); 2532 fprintf(fd, "\t\t\tprintf(\"%%3d: proc %%d fairness \", depth, II);\n"); 2533 fprintf(fd, "\t\t\tprintf(\"Rule 2: --cnt to %%d (%%d)\\n\",\n"); 2534 fprintf(fd, "\t\t\t now._cnt[now._a_t&1], now._a_t);\n"); 2535 fprintf(fd, "#endif\n"); 2536 fprintf(fd, "\t\t\t trpt->o_pm |= (32|64);\n"); 2537 fprintf(fd, "\t\t\t}\n"); 2538 fprintf(fd, "#endif\n"); 2539 2540 fprintf(fd, "\n\t\t}"); 2541 } 2542 break; 2543 2544 case 'R': 2545 if (!terse && !TestOnly && has_xu) 2546 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t"); 2547 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || "); 2548 fprintf(fd, "q_R_check("); 2549 putname(fd, "", now->lft, m, ", II)) &&\n\t\t"); 2550 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || "); 2551 putname(fd, "q_S_check(", now->lft, m, ", II)) &&"); 2552 fprintf(fd, "\n#endif\n\t\t"); 2553 } 2554 if (u_sync>0) 2555 putname(fd, "not_RV(", now->lft, m, ") && \\\n\t\t"); 2556 2557 for (v = now->rgt, i=j=0; v; v = v->rgt, i++) 2558 if (v->lft->ntyp != CONST 2559 && v->lft->ntyp != EVAL) 2560 { j++; continue; 2561 } 2562 if (now->val == 0 || i == j) 2563 { putname(fd, "(q_len(", now->lft, m, ") > 0"); 2564 for (v = now->rgt, i=0; v; v = v->rgt, i++) 2565 { if (v->lft->ntyp != CONST 2566 && v->lft->ntyp != EVAL) 2567 continue; 2568 fprintf(fd, " \\\n\t\t&& qrecv("); 2569 putname(fd, "", now->lft, m, ", "); 2570 fprintf(fd, "0, %d, 0) == ", i); 2571 if (v->lft->ntyp == CONST) 2572 putstmnt(fd, v->lft, m); 2573 else /* EVAL */ 2574 putstmnt(fd, v->lft->lft, m); 2575 } 2576 fprintf(fd, ")"); 2577 } else 2578 { putname(fd, "Q_has(", now->lft, m, ""); 2579 for (v = now->rgt, i=0; v; v = v->rgt, i++) 2580 { if (v->lft->ntyp == CONST) 2581 { fprintf(fd, ", 1, "); 2582 putstmnt(fd, v->lft, m); 2583 } else if (v->lft->ntyp == EVAL) 2584 { fprintf(fd, ", 1, "); 2585 putstmnt(fd, v->lft->lft, m); 2586 } else 2587 fprintf(fd, ", 0, 0"); 2588 } 2589 for ( ; i < Mpars; i++) 2590 fprintf(fd, ", 0, 0"); 2591 fprintf(fd, ")"); 2592 } 2593 break; 2594 2595 case 'c': 2596 preruse(fd, now->lft); /* preconditions */ 2597 cat3("if (!(", now->lft, "))\n\t\t\t"); 2598 Bailout(fd, ""); 2599 break; 2600 2601 case ELSE: 2602 if (!GenCode) 2603 { if (separate == 2) 2604 fprintf(fd, "if (o_pm&1)\n\t\t\t"); 2605 else 2606 fprintf(fd, "if (trpt->o_pm&1)\n\t\t\t"); 2607 Bailout(fd, ""); 2608 } else 2609 { fprintf(fd, "/* else */"); 2610 } 2611 break; 2612 2613 case '?': 2614 if (now->lft) 2615 { cat3("( (", now->lft, ") ? "); 2616 } 2617 if (now->rgt) 2618 { cat3("(", now->rgt->lft, ") : "); 2619 cat3("(", now->rgt->rgt, ") )"); 2620 } 2621 break; 2622 2623 case ASGN: 2624 if (has_enabled) 2625 fprintf(fd, "if (TstOnly) return 1;\n\t\t"); 2626 _isok++; 2627 2628 if (!GenCode) 2629 { if (multi_oval) 2630 { char tempbuf[64]; 2631 check_needed(); 2632 sprintf(tempbuf, "(trpt+1)->bup.ovals[%d] = ", 2633 multi_oval-1); 2634 multi_oval++; 2635 cat3(tempbuf, now->lft, ";\n\t\t"); 2636 } else 2637 { cat3("(trpt+1)->bup.oval = ", now->lft, ";\n\t\t"); 2638 } } 2639 nocast = 1; putstmnt(fd,now->lft,m); nocast = 0; 2640 fprintf(fd," = "); 2641 _isok--; 2642 putstmnt(fd,now->rgt,m); 2643 2644 if (now->sym->type != CHAN 2645 || verbose > 0) 2646 { fprintf(fd, ";\n#ifdef VAR_RANGES"); 2647 fprintf(fd, "\n\t\tlogval(\""); 2648 withprocname = terse = nocast = 1; 2649 _isok++; 2650 putstmnt(fd,now->lft,m); 2651 withprocname = terse = nocast = 0; 2652 fprintf(fd, "\", "); 2653 putstmnt(fd,now->lft,m); 2654 _isok--; 2655 fprintf(fd, ");\n#endif\n"); 2656 fprintf(fd, "\t\t"); 2657 } 2658 break; 2659 2660 case PRINT: 2661 if (has_enabled) 2662 fprintf(fd, "if (TstOnly) return 1;\n\t\t"); 2663 #ifdef PRINTF 2664 fprintf(fd, "printf(%s", now->sym->name); 2665 #else 2666 fprintf(fd, "Printf(%s", now->sym->name); 2667 #endif 2668 for (v = now->lft; v; v = v->rgt) 2669 { cat2(", ", v->lft); 2670 } 2671 fprintf(fd, ")"); 2672 break; 2673 2674 case PRINTM: 2675 if (has_enabled) 2676 fprintf(fd, "if (TstOnly) return 1;\n\t\t"); 2677 fprintf(fd, "printm("); 2678 if (now->lft && now->lft->ismtyp) 2679 fprintf(fd, "%d", now->lft->val); 2680 else 2681 putstmnt(fd, now->lft, m); 2682 fprintf(fd, ")"); 2683 break; 2684 2685 case NAME: 2686 if (!nocast && now->sym && Sym_typ(now) < SHORT) 2687 putname(fd, "((int)", now, m, ")"); 2688 else 2689 putname(fd, "", now, m, ""); 2690 break; 2691 2692 case 'p': 2693 putremote(fd, now, m); 2694 break; 2695 2696 case 'q': 2697 if (terse) 2698 fprintf(fd, "%s", now->sym->name); 2699 else 2700 fprintf(fd, "%d", remotelab(now)); 2701 break; 2702 2703 case C_EXPR: 2704 fprintf(fd, "("); 2705 plunk_expr(fd, now->sym->name); 2706 fprintf(fd, ") /* %s */ ", now->sym->name); 2707 break; 2708 2709 case C_CODE: 2710 fprintf(fd, "/* %s */\n\t\t", now->sym->name); 2711 if (has_enabled) 2712 fprintf(fd, "if (TstOnly) return 1;\n\t\t"); 2713 if (!GenCode) /* not in d_step */ 2714 { fprintf(fd, "sv_save();\n\t\t"); 2715 /* store the old values for reverse moves */ 2716 } 2717 plunk_inline(fd, now->sym->name, 1); 2718 if (!GenCode) 2719 { fprintf(fd, "\n"); /* state changed, capture it */ 2720 fprintf(fd, "#if defined(C_States) && (HAS_TRACK==1)\n"); 2721 fprintf(fd, "\t\tc_update((uchar *) &(now.c_state[0]));\n"); 2722 fprintf(fd, "#endif\n"); 2723 } 2724 break; 2725 2726 case ASSERT: 2727 if (has_enabled) 2728 fprintf(fd, "if (TstOnly) return 1;\n\t\t"); 2729 2730 cat3("assert(", now->lft, ", "); 2731 terse = nocast = 1; 2732 cat3("\"", now->lft, "\", II, tt, t)"); 2733 terse = nocast = 0; 2734 break; 2735 2736 case '.': 2737 case BREAK: 2738 case GOTO: 2739 if (Pid == eventmapnr) 2740 fprintf(fd, "Uerror(\"cannot get here\")"); 2741 putskip(m); 2742 break; 2743 2744 case '@': 2745 if (Pid == eventmapnr) 2746 { fprintf(fd, "return 0"); 2747 break; 2748 } 2749 2750 if (has_enabled) 2751 { fprintf(fd, "if (TstOnly)\n\t\t\t"); 2752 fprintf(fd, "return (II+1 == now._nr_pr);\n\t\t"); 2753 } 2754 fprintf(fd, "if (!delproc(1, II)) "); 2755 Bailout(fd, ""); 2756 break; 2757 2758 default: 2759 printf("spin: bad node type %d (.m) - line %d\n", 2760 now->ntyp, now->ln); 2761 fflush(tm); 2762 alldone(1); 2763 } 2764 } 2765 2766 void 2767 putname(FILE *fd, char *pre, Lextok *n, int m, char *suff) /* varref */ 2768 { Symbol *s = n->sym; 2769 lineno = n->ln; Fname = n->fn; 2770 2771 if (!s) 2772 fatal("no name - putname", (char *) 0); 2773 2774 if (s->context && context && s->type) 2775 s = findloc(s); /* it's a local var */ 2776 2777 if (!s) 2778 { fprintf(fd, "%s%s%s", pre, n->sym->name, suff); 2779 return; 2780 } 2781 if (!s->type) /* not a local name */ 2782 s = lookup(s->name); /* must be a global */ 2783 2784 if (!s->type) 2785 { if (strcmp(pre, ".") != 0) 2786 non_fatal("undeclared variable '%s'", s->name); 2787 s->type = INT; 2788 } 2789 2790 if (s->type == PROCTYPE) 2791 fatal("proctype-name '%s' used as array-name", s->name); 2792 2793 fprintf(fd, pre); 2794 if (!terse && !s->owner && evalindex != 1) 2795 { if (s->context 2796 || strcmp(s->name, "_p") == 0 2797 || strcmp(s->name, "_pid") == 0) 2798 { fprintf(fd, "((P%d *)this)->", Pid); 2799 } else 2800 { int x = strcmp(s->name, "_"); 2801 if (!(s->hidden&1) && x != 0) 2802 fprintf(fd, "now."); 2803 if (x == 0 && _isok == 0) 2804 fatal("attempt to read value of '_'", 0); 2805 } } 2806 2807 if (withprocname 2808 && s->context 2809 && strcmp(pre, ".")) 2810 fprintf(fd, "%s:", s->context->name); 2811 2812 if (evalindex != 1) 2813 fprintf(fd, "%s", s->name); 2814 2815 if (s->nel != 1) 2816 { if (no_arrays) 2817 { 2818 non_fatal("ref to array element invalid in this context", 2819 (char *)0); 2820 printf("\thint: instead of, e.g., x[rs] qu[3], use\n"); 2821 printf("\tchan nm_3 = qu[3]; x[rs] nm_3;\n"); 2822 printf("\tand use nm_3 in sends/recvs instead of qu[3]\n"); 2823 } 2824 /* an xr or xs reference to an array element 2825 * becomes an exclusion tag on the array itself - 2826 * which could result in invalidly labeling 2827 * operations on other elements of this array to 2828 * be also safe under the partial order reduction 2829 * (see procedure has_global()) 2830 */ 2831 2832 if (evalindex == 2) 2833 { fprintf(fd, "[%%d]"); 2834 } else if (evalindex == 1) 2835 { evalindex = 0; /* no good if index is indexed array */ 2836 fprintf(fd, ", "); 2837 putstmnt(fd, n->lft, m); 2838 evalindex = 1; 2839 } else 2840 { if (terse 2841 || (n->lft 2842 && n->lft->ntyp == CONST 2843 && n->lft->val < s->nel) 2844 || (!n->lft && s->nel > 0)) 2845 { cat3("[", n->lft, "]"); 2846 } else 2847 { cat3("[ Index(", n->lft, ", "); 2848 fprintf(fd, "%d) ]", s->nel); 2849 } 2850 } 2851 } 2852 if (s->type == STRUCT && n->rgt && n->rgt->lft) 2853 { putname(fd, ".", n->rgt->lft, m, ""); 2854 } 2855 fprintf(fd, suff); 2856 } 2857 2858 void 2859 putremote(FILE *fd, Lextok *n, int m) /* remote reference */ 2860 { int promoted = 0; 2861 int pt; 2862 2863 if (terse) 2864 { fprintf(fd, "%s", n->lft->sym->name); /* proctype name */ 2865 if (n->lft->lft) 2866 { fprintf(fd, "["); 2867 putstmnt(fd, n->lft->lft, m); /* pid */ 2868 fprintf(fd, "]"); 2869 } 2870 fprintf(fd, ".%s", n->sym->name); 2871 } else 2872 { if (Sym_typ(n) < SHORT) 2873 { promoted = 1; 2874 fprintf(fd, "((int)"); 2875 } 2876 2877 pt = fproc(n->lft->sym->name); 2878 fprintf(fd, "((P%d *)Pptr(", pt); 2879 if (n->lft->lft) 2880 { fprintf(fd, "BASE+"); 2881 putstmnt(fd, n->lft->lft, m); 2882 } else 2883 fprintf(fd, "f_pid(%d)", pt); 2884 fprintf(fd, "))->%s", n->sym->name); 2885 } 2886 if (n->rgt) 2887 { fprintf(fd, "["); 2888 putstmnt(fd, n->rgt, m); /* array var ref */ 2889 fprintf(fd, "]"); 2890 } 2891 if (promoted) fprintf(fd, ")"); 2892 } 2893 2894 static int 2895 getweight(Lextok *n) 2896 { /* this piece of code is a remnant of early versions 2897 * of the verifier -- in the current version of Spin 2898 * only non-zero values matter - so this could probably 2899 * simply return 1 in all cases. 2900 */ 2901 switch (n->ntyp) { 2902 case 'r': return 4; 2903 case 's': return 2; 2904 case TIMEOUT: return 1; 2905 case 'c': if (has_typ(n->lft, TIMEOUT)) return 1; 2906 } 2907 return 3; 2908 } 2909 2910 int 2911 has_typ(Lextok *n, int m) 2912 { 2913 if (!n) return 0; 2914 if (n->ntyp == m) return 1; 2915 return (has_typ(n->lft, m) || has_typ(n->rgt, m)); 2916 } 2917 2918 static int runcount, opcount; 2919 2920 static void 2921 do_count(Lextok *n, int checkop) 2922 { 2923 if (!n) return; 2924 2925 switch (n->ntyp) { 2926 case RUN: 2927 runcount++; 2928 break; 2929 default: 2930 if (checkop) opcount++; 2931 break; 2932 } 2933 do_count(n->lft, checkop && (n->ntyp != RUN)); 2934 do_count(n->rgt, checkop); 2935 } 2936 2937 void 2938 count_runs(Lextok *n) 2939 { 2940 runcount = opcount = 0; 2941 do_count(n, 1); 2942 if (runcount > 1) 2943 fatal("more than one run operator in expression", ""); 2944 if (runcount == 1 && opcount > 1) 2945 fatal("use of run operator in compound expression", ""); 2946 } 2947