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