1 /***** spin: pangen2.c *****/
4 * This file is part of the public release of Spin. It is subject to the
5 * terms in the LICENSE file that is included in this source directory.
6 * Tool documentation is available at http://spinroot.com
17 #define DELTA 500 /* sets an upperbound on nr of chan names */
19 #define blurb(fd, e) { fprintf(fd, "\n"); if (!merger) fprintf(fd, "\t\t/* %s:%d */\n", \
20 e->n->fn->name, e->n->ln); }
21 #define tr_map(m, e) { if (!merger) fprintf(tt, "\t\ttr_2_src(%d, \"%s\", %d);\n", \
22 m, e->n->fn->name, e->n->ln); }
26 extern Lextok *runstmnts;
27 extern Symbol *Fname, *oFname, *context;
28 extern char *claimproc, *eventmap;
29 extern int lineno, verbose, Npars, Mpars, nclaims;
30 extern int m_loss, has_remote, has_remvar, merger, rvopt, separate;
31 extern int Ntimeouts, Etimeouts, deadvar, old_scope_rules, old_priority_rules;
32 extern int u_sync, u_async, nrRdy, Unique;
33 extern int GenCode, IsGuard, Level, TestOnly;
34 extern int globmin, globmax, ltl_mode, dont_simplify;
36 extern short has_stack;
37 extern char *NextLab[64]; /* must match value in dstep.c:18 */
40 FILE *tc, *th, *tt, *tb;
43 int OkBreak = -1, has_hidden = 0; /* has_hidden set in sym.c and structs.c */
44 short nocast=0; /* to turn off casts in lvalues */
45 short terse=0; /* terse printing of varnames */
47 short has_last=0; /* spec refers to _last */
48 short has_priority=0; /* spec refers to _priority */
49 short has_badelse=0; /* spec contains else combined with chan refs */
50 short has_enabled=0; /* spec contains enabled() */
51 short has_pcvalue=0; /* spec contains pc_value() */
52 short has_np=0; /* spec contains np_ */
53 short has_sorted=0; /* spec contains `!!' (sorted-send) operator */
54 short has_random=0; /* spec contains `??' (random-recv) operator */
55 short has_xu=0; /* spec contains xr or xs assertions */
56 short has_unless=0; /* spec contains unless statements */
57 short has_provided=0; /* spec contains PROVIDED clauses on procs */
58 short has_code=0; /* spec contains c_code, c_expr, c_state */
59 short has_ltl=0; /* has inline ltl formulae */
60 int mst=0; /* max nr of state/process */
61 int claimnr = -1; /* claim process, if any */
62 int eventmapnr = -1; /* event trace, if any */
63 int Pid; /* proc currently processed */
64 int multi_oval; /* set in merges, used also in pangen4.c */
66 #define MAXMERGE 256 /* max nr of bups per merge sequence */
68 static short CnT[MAXMERGE];
69 static Lextok XZ, YZ[MAXMERGE];
70 static int didcase, YZmax, YZcnt;
73 static int Det; /* set if deterministic */
74 static int T_sum, T_mus, t_cyc;
75 static int TPE[2], EPT[2];
77 static int multi_needed, multi_undo;
78 static short AllGlobal=0; /* set if process has provided clause */
79 static short withprocname=0; /* prefix local varnames with procname */
80 static short _isok=0; /* checks usage of predefined variable _ */
81 static short evalindex=0; /* evaluate index of var names */
83 int has_global(Lextok *);
84 static int getweight(Lextok *);
85 static int scan_seq(Sequence *);
86 static void genconditionals(void);
87 static void mark_seq(Sequence *);
88 static void patch_atomic(Sequence *);
89 static void put_seq(Sequence *, int, int);
90 static void putproc(ProcList *);
91 static void Tpe(Lextok *);
92 extern void spit_recvs(FILE *, FILE*);
94 static L_List *keep_track;
97 keep_track_off(Lextok *n)
100 p = (L_List *) emalloc(sizeof(L_List));
107 check_track(Lextok *n)
110 for (p = keep_track; p; p = p->nxt)
112 { return n->sym?n->sym->type:0;
121 for (p = rdy; p; p = p->nxt)
122 if (strcmp(p->n->name, s) == 0)
125 fatal("proctype %s not found", s);
130 pid_is_claim(int p) /* Pid (p->tn) to type (p->b) */
133 for (r = rdy; r; r = r->nxt)
134 { if (r->tn == p) return (r->b == N_CLAIM);
136 printf("spin: error, cannot find pid %d\n", p);
141 reverse_procs(RunList *q)
144 reverse_procs(q->nxt);
145 fprintf(tc, " Addproc(%d, %d);\n",
146 q->tn, q->priority < 1 ? 1 : q->priority);
150 forward_procs(RunList *q)
153 fprintf(tc, " Addproc(%d, %d);\n",
154 q->tn, q->priority < 1 ? 1 : q->priority);
155 forward_procs(q->nxt);
161 fprintf(th, "#define _T5 %d\n", uniq++);
162 fprintf(th, "#define _T2 %d\n", uniq++);
164 fprintf(tm, "\tcase _T5:\t/* np_ */\n");
167 { fprintf(tm, "\t\tif (!((!(o_pm&4) && !(tau&128))))\n");
169 { fprintf(tm, "\t\tif (!((!(trpt->o_pm&4) && !(trpt->tau&128))))\n");
171 fprintf(tm, "\t\t\tcontinue;\n");
172 fprintf(tm, "\t\t/* else fall through */\n");
173 fprintf(tm, "\tcase _T2:\t/* true */\n");
174 fprintf(tm, "\t\t_m = 3; goto P999;\n");
180 fprintf(tt, "\t/* np_ demon: */\n");
181 fprintf(tt, "\ttrans[_NP_] = ");
182 fprintf(tt, "(Trans **) emalloc(2*sizeof(Trans *));\n");
183 fprintf(tt, "\tT = trans[_NP_][0] = ");
184 fprintf(tt, "settr(9997,0,1,_T5,0,\"(np_)\", 1,2,0);\n");
185 fprintf(tt, "\t T->nxt = ");
186 fprintf(tt, "settr(9998,0,0,_T2,0,\"(1)\", 0,2,0);\n");
187 fprintf(tt, "\tT = trans[_NP_][1] = ");
188 fprintf(tt, "settr(9999,0,1,_T5,0,\"(np_)\", 1,2,0);\n");
194 { { "pan.c", "pan_s.c", "pan_t.c" } },
195 { { "pan.h", "pan_s.h", "pan_t.h" } },
196 { { "pan.t", "pan_s.t", "pan_t.t" } },
197 { { "pan.m", "pan_s.m", "pan_t.m" } },
198 { { "pan.b", "pan_s.b", "pan_t.b" } }
206 disambiguate(); /* avoid name-clashes between scopes */
208 if (!(tc = fopen(Cfile[0].nm[separate], MFLAGS)) /* main routines */
209 || !(th = fopen(Cfile[1].nm[separate], MFLAGS)) /* header file */
210 || !(tt = fopen(Cfile[2].nm[separate], MFLAGS)) /* transition matrix */
211 || !(tm = fopen(Cfile[3].nm[separate], MFLAGS)) /* forward moves */
212 || !(tb = fopen(Cfile[4].nm[separate], MFLAGS))) /* backward moves */
213 { printf("spin: cannot create pan.[chtmfb]\n");
217 fprintf(th, "#ifndef PAN_H\n");
218 fprintf(th, "#define PAN_H\n\n");
220 fprintf(th, "#define SpinVersion \"%s\"\n", SpinVersion);
221 fprintf(th, "#define PanSource \"");
222 for (i = 0; oFname->name[i] != '\0'; i++)
223 { char c = oFname->name[i];
224 if (c == '\\' || c == ' ') /* Windows path */
227 fprintf(th, "%c", c);
229 fprintf(th, "\"\n\n");
231 fprintf(th, "#define G_long %d\n", (int) sizeof(long));
232 fprintf(th, "#define G_int %d\n\n", (int) sizeof(int));
233 fprintf(th, "#define ulong unsigned long\n");
234 fprintf(th, "#define ushort unsigned short\n");
236 fprintf(th, "#ifdef WIN64\n");
237 fprintf(th, " #define ONE_L (1L)\n");
238 fprintf(th, "/* #define long long long */\n");
239 fprintf(th, "#else\n");
240 fprintf(th, " #define ONE_L (1L)\n");
241 fprintf(th, "#endif\n\n");
243 fprintf(th, "#ifdef BFS_PAR\n");
244 fprintf(th, " #define NRUNS %d\n", (runstmnts)?1:0);
245 fprintf(th, " #ifndef BFS\n");
246 fprintf(th, " #define BFS\n");
247 fprintf(th, " #endif\n");
248 fprintf(th, " #ifndef PUTPID\n");
249 fprintf(th, " #define PUTPID\n");
250 fprintf(th, " #endif\n\n");
251 fprintf(th, " #if !defined(USE_TDH) && !defined(NO_TDH)\n");
252 fprintf(th, " #define USE_TDH\n");
253 fprintf(th, " #endif\n");
254 fprintf(th, " #if defined(USE_TDH) && !defined(NO_HC)\n");
255 fprintf(th, " #define HC /* default for USE_TDH */\n");
256 fprintf(th, " #endif\n");
257 fprintf(th, " #ifndef BFS_MAXPROCS\n");
258 fprintf(th, " #define BFS_MAXPROCS 64 /* max nr of cores to use */\n");
259 fprintf(th, " #endif\n");
261 fprintf(th, " #define BFS_GLOB 0 /* global lock */\n");
262 fprintf(th, " #define BFS_ORD 1 /* used with -DCOLLAPSE */\n");
263 fprintf(th, " #define BFS_MEM 2 /* malloc from shared heap */\n");
264 fprintf(th, " #define BFS_PRINT 3 /* protect printfs */\n");
265 fprintf(th, " #define BFS_STATE 4 /* hashtable */\n\n");
266 fprintf(th, " #define BFS_INQ 2 /* state is in q */\n\n");
268 fprintf(th, " #ifdef BFS_FIFO\n"); /* queue access */
269 fprintf(th, " #define BFS_ID(a,b) (BFS_STATE + (int) ((a)*BFS_MAXPROCS+(b)))\n");
270 fprintf(th, " #define BFS_MAXLOCKS (BFS_STATE + (BFS_MAXPROCS*BFS_MAXPROCS))\n");
271 fprintf(th, " #else\n"); /* h_store access (not needed for o_store) */
272 fprintf(th, " #ifndef BFS_W\n");
273 fprintf(th, " #define BFS_W 10\n"); /* 1<<BFS_W locks */
274 fprintf(th, " #endif\n");
275 fprintf(th, " #define BFS_MASK ((1<<BFS_W) - 1)\n");
276 fprintf(th, " #define BFS_ID (BFS_STATE + (int) (j1_spin & (BFS_MASK)))\n");
277 fprintf(th, " #define BFS_MAXLOCKS (BFS_STATE + (1<<BFS_W))\n"); /* 4+1024 */
278 fprintf(th, " #endif\n");
280 fprintf(th, " #undef NCORE\n");
281 fprintf(th, " extern int Cores, who_am_i;\n");
282 fprintf(th, " #ifndef SAFETY\n");
283 fprintf(th, " #if !defined(BFS_STAGGER) && !defined(BFS_DISK)\n");
284 fprintf(th, " #define BFS_STAGGER 64 /* randomizer, was 16 */\n");
285 fprintf(th, " #endif\n");
286 fprintf(th, " #ifndef L_BOUND\n");
287 fprintf(th, " #define L_BOUND 10 /* default */\n");
288 fprintf(th, " #endif\n");
289 fprintf(th, " extern int L_bound;\n");
290 fprintf(th, " #endif\n");
291 fprintf(th, " #if defined(BFS_DISK) && defined(BFS_STAGGER)\n");
292 fprintf(th, " #error BFS_DISK and BFS_STAGGER are not compatible\n");
293 fprintf(th, " #endif\n");
294 fprintf(th, "#endif\n\n");
296 fprintf(th, "#if defined(BFS)\n");
297 fprintf(th, " #ifndef SAFETY\n");
298 fprintf(th, " #define SAFETY\n");
299 fprintf(th, " #endif\n");
300 fprintf(th, " #ifndef XUSAFE\n");
301 fprintf(th, " #define XUSAFE\n");
302 fprintf(th, " #endif\n");
303 fprintf(th, "#endif\n");
305 fprintf(th, "#ifndef uchar\n");
306 fprintf(th, " #define uchar unsigned char\n");
307 fprintf(th, "#endif\n");
308 fprintf(th, "#ifndef uint\n");
309 fprintf(th, " #define uint unsigned int\n");
310 fprintf(th, "#endif\n");
312 if (separate == 1 && !claimproc)
313 { Symbol *n = (Symbol *) emalloc(sizeof(Symbol));
314 Sequence *s = (Sequence *) emalloc(sizeof(Sequence));
316 claimproc = n->name = "_:never_template:_";
317 ready(n, ZN, s, 0, ZN, N_CLAIM);
321 { printf("spin: warning, make sure that the S1 model\n");
322 printf(" includes the same remote references\n");
324 fprintf(th, "#ifndef NFAIR\n");
325 fprintf(th, "#define NFAIR 2 /* must be >= 2 */\n");
326 fprintf(th, "#endif\n");
328 fprintf(th, "#define HAS_LAST %d\n", has_last);
329 if (has_priority && !old_priority_rules)
330 fprintf(th, "#define HAS_PRIORITY %d\n", has_priority);
334 fprintf(th, "#define DELTA %d\n", DELTA);
335 fprintf(th, "#ifdef MA\n");
336 fprintf(th, " #if NCORE>1 && !defined(SEP_STATE)\n");
337 fprintf(th, " #define SEP_STATE\n");
338 fprintf(th, " #endif\n");
339 fprintf(th, " #if MA==1\n"); /* user typed -DMA without size */
340 fprintf(th, " #undef MA\n");
341 fprintf(th, " #define MA 100\n");
342 fprintf(th, " #endif\n");
343 fprintf(th, "#endif\n");
344 fprintf(th, "#ifdef W_XPT\n");
345 fprintf(th, " #if W_XPT==1\n"); /* user typed -DW_XPT without size */
346 fprintf(th, " #undef W_XPT\n");
347 fprintf(th, " #define W_XPT 1000000\n");
348 fprintf(th, " #endif\n");
349 fprintf(th, "#endif\n");
350 fprintf(th, "#ifndef NFAIR\n");
351 fprintf(th, " #define NFAIR 2 /* must be >= 2 */\n");
352 fprintf(th, "#endif\n");
354 fprintf(th, "#define NTIM %d\n", Ntimeouts);
356 fprintf(th, "#define ETIM %d\n", Etimeouts);
358 fprintf(th, "#define REM_VARS 1\n");
360 fprintf(th, "#define REM_REFS %d\n", has_remote); /* not yet used */
362 { fprintf(th, "#define HAS_HIDDEN %d\n", has_hidden);
363 fprintf(th, "#if defined(BFS_PAR) || defined(BFS)\n");
364 fprintf(th, " #error cannot use BFS on models with variables declared hidden\n");
365 fprintf(th, "#endif\n");
368 fprintf(th, "#define HAS_LAST %d\n", has_last);
369 if (has_priority && !old_priority_rules)
370 fprintf(th, "#define HAS_PRIORITY %d\n", has_priority);
372 fprintf(th, "#define HAS_SORTED %d\n", has_sorted);
374 fprintf(th, "#define M_LOSS\n");
376 fprintf(th, "#define HAS_RANDOM %d\n", has_random);
378 fprintf(th, "#define HAS_LTL 1\n");
379 fprintf(th, "#define HAS_CODE 1\n"); /* could also be set to has_code */
380 /* always defining it doesn't seem to cause measurable overhead though */
381 /* and allows for pan -r etc to work for non-embedded code as well */
382 fprintf(th, "#if defined(RANDSTORE) && !defined(RANDSTOR)\n");
383 fprintf(th, " #define RANDSTOR RANDSTORE\n"); /* xspin uses RANDSTORE... */
384 fprintf(th, "#endif\n");
386 fprintf(th, "#define HAS_STACK %d\n", has_stack);
387 if (has_enabled || (has_priority && !old_priority_rules))
388 fprintf(th, "#define HAS_ENABLED 1\n");
390 fprintf(th, "#define HAS_UNLESS %d\n", has_unless);
392 fprintf(th, "#define HAS_PROVIDED %d\n", has_provided);
394 fprintf(th, "#define HAS_PCVALUE %d\n", has_pcvalue);
396 fprintf(th, "#define HAS_BADELSE %d\n", has_badelse);
398 || (has_priority && !old_priority_rules)
402 { fprintf(th, "#ifndef NOREDUCE\n");
403 fprintf(th, " #define NOREDUCE 1\n");
404 fprintf(th, "#endif\n");
407 fprintf(th, "#define HAS_NP %d\n", has_np);
409 fprintf(th, "#define MERGED 1\n");
412 fprintf(th, "#if !defined(HAS_LAST) && defined(BCS)\n");
413 fprintf(th, " #define HAS_LAST 1 /* use it, but */\n");
414 fprintf(th, " #ifndef STORE_LAST\n"); /* unless the user insists */
415 fprintf(th, " #define NO_LAST 1 /* dont store it */\n");
416 fprintf(th, " #endif\n");
417 fprintf(th, "#endif\n");
419 fprintf(th, "#if defined(BCS) && defined(BITSTATE)\n");
420 fprintf(th, " #ifndef NO_CTX\n");
421 fprintf(th, " #define STORE_CTX 1\n");
422 fprintf(th, " #endif\n");
423 fprintf(th, "#endif\n");
425 fprintf(th, "#ifdef NP\n");
427 fprintf(th, " #define HAS_NP 2\n");
428 fprintf(th, " #define VERI %d /* np_ */\n", nrRdy);
429 fprintf(th, "#endif\n");
431 { claimnr = fproc(claimproc); /* the default claim */
432 fprintf(th, "#ifndef NOCLAIM\n");
433 fprintf(th, " #define NCLAIMS %d\n", nclaims);
434 fprintf(th, " #ifndef NP\n");
435 fprintf(th, " #define VERI %d\n", claimnr);
436 fprintf(th, " #endif\n");
437 fprintf(th, "#endif\n");
440 { eventmapnr = fproc(eventmap);
441 fprintf(th, "#define EVENT_TRACE %d\n", eventmapnr);
442 fprintf(th, "#define endevent _endstate%d\n", eventmapnr);
443 if (eventmap[2] == 'o') /* ":notrace:" */
444 fprintf(th, "#define NEGATED_TRACE 1\n");
447 fprintf(th, "\ntypedef struct S_F_MAP {\n");
448 fprintf(th, " char *fnm;\n\tint from;\n\tint upto;\n");
449 fprintf(th, "} S_F_MAP;\n");
451 fprintf(tc, "/*** Generated by %s ***/\n", SpinVersion);
452 fprintf(tc, "/*** From source: %s ***/\n\n", oFname->name);
454 ntimes(tc, 0, 1, Pre0);
456 plunk_c_decls(tc); /* types can be refered to in State */
459 case 0: fprintf(tc, "#include \"pan.h\"\n"); break;
460 case 1: fprintf(tc, "#include \"pan_s.h\"\n"); break;
461 case 2: fprintf(tc, "#include \"pan_t.h\"\n"); break;
465 { fprintf(tc, "char *TrailFile = PanSource; /* default */\n");
466 fprintf(tc, "char *trailfilename;\n");
469 fprintf(tc, "#ifdef LOOPSTATE\n");
470 fprintf(tc, "double cnt_loops;\n");
471 fprintf(tc, "#endif\n");
473 fprintf(tc, "State A_Root; /* seed-state for cycles */\n");
474 fprintf(tc, "State now; /* the full state-vector */\n");
475 fprintf(tc, "#if NQS > 0\n");
476 fprintf(tc, "short q_flds[NQS+1];\n");
477 fprintf(tc, "short q_max[NQS+1];\n");
478 fprintf(tc, "#endif\n");
480 plunk_c_fcts(tc); /* State can be used in fcts */
483 { ntimes(tc, 0, 1, Preamble);
484 ntimes(tc, 0, 1, Separate); /* things that moved out of pan.h */
486 { fprintf(tc, "extern int verbose;\n");
487 fprintf(tc, "extern long depth, depthfound;\n");
490 fprintf(tc, "#ifndef NOBOUNDCHECK\n");
491 fprintf(tc, " #define Index(x, y)\tBoundcheck(x, y, II, tt, t)\n");
492 fprintf(tc, "#else\n");
493 fprintf(tc, " #define Index(x, y)\tx\n");
494 fprintf(tc, "#endif\n");
496 c_preview(); /* sets hastrack */
498 for (p = rdy; p; p = p->nxt)
499 mst = max(p->s->maxel, mst);
502 { fprintf(tt, "#ifdef PEG\n");
503 fprintf(tt, "struct T_SRC {\n");
504 fprintf(tt, " char *fl; int ln;\n");
505 fprintf(tt, "} T_SRC[NTRANS];\n\n");
506 fprintf(tt, "void\ntr_2_src(int m, char *file, int ln)\n");
507 fprintf(tt, "{ T_SRC[m].fl = file;\n");
508 fprintf(tt, " T_SRC[m].ln = ln;\n");
509 fprintf(tt, "}\n\n");
510 fprintf(tt, "void\nputpeg(int n, int m)\n");
511 fprintf(tt, "{ printf(\"%%5d\ttrans %%4d \", m, n);\n");
512 fprintf(tt, " printf(\"%%s:%%d\\n\",\n");
513 fprintf(tt, " T_SRC[n].fl, T_SRC[n].ln);\n");
516 { fprintf(tt, "#else\n");
517 fprintf(tt, "#define tr_2_src(m,f,l)\n");
519 fprintf(tt, "#endif\n\n");
520 fprintf(tt, "void\nsettable(void)\n{\tTrans *T;\n");
521 fprintf(tt, "\tTrans *settr(int, int, int, int, int,");
522 fprintf(tt, " char *, int, int, int);\n\n");
523 fprintf(tt, "\ttrans = (Trans ***) ");
524 fprintf(tt, "emalloc(%d*sizeof(Trans **));\n", nrRdy+1);
525 /* +1 for np_ automaton */
529 fprintf(tm, " if (II == 0)\n");
530 fprintf(tm, " { _m = step_claim(trpt->o_pm, trpt->tau, tt, ot, t);\n");
531 fprintf(tm, " if (_m) goto P999; else continue;\n");
532 fprintf(tm, " } else\n");
535 fprintf(tm, "#define rand pan_rand\n");
536 fprintf(tm, "#define pthread_equal(a,b) ((a)==(b))\n");
537 fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n");
538 fprintf(tm, " #ifdef BFS_PAR\n");
539 fprintf(tm, " bfs_printf(\"Pr: %%d Tr: %%d\\n\", II, t->forw);\n");
540 fprintf(tm, " #else\n");
541 fprintf(tm, " cpu_printf(\"Pr: %%d Tr: %%d\\n\", II, t->forw);\n");
542 fprintf(tm, " #endif\n");
543 fprintf(tm, "#endif\n");
544 fprintf(tm, " switch (t->forw) {\n");
546 { fprintf(tt, "#ifndef PEG\n");
547 fprintf(tt, " #define tr_2_src(m,f,l)\n");
548 fprintf(tt, "#endif\n");
549 fprintf(tt, "void\nset_claim(void)\n{\tTrans *T;\n");
550 fprintf(tt, "\textern Trans ***trans;\n");
551 fprintf(tt, "\textern Trans *settr(int, int, int, int, int,");
552 fprintf(tt, " char *, int, int, int);\n\n");
554 fprintf(tm, "#define rand pan_rand\n");
555 fprintf(tm, "#define pthread_equal(a,b) ((a)==(b))\n");
556 fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n");
557 fprintf(tm, " cpu_printf(\"Pr: %%d Tr: %%d\\n\", II, forw);\n");
558 fprintf(tm, "#endif\n");
559 fprintf(tm, " switch (forw) {\n");
562 fprintf(tm, " default: Uerror(\"bad forward move\");\n");
563 fprintf(tm, " case 0: /* if without executable clauses */\n");
564 fprintf(tm, " continue;\n");
565 fprintf(tm, " case 1: /* generic 'goto' or 'skip' */\n");
567 fprintf(tm, " IfNotBlocked\n");
568 fprintf(tm, " _m = 3; goto P999;\n");
569 fprintf(tm, " case 2: /* generic 'else' */\n");
571 fprintf(tm, " if (o_pm&1) continue;\n");
573 { fprintf(tm, " IfNotBlocked\n");
574 fprintf(tm, " if (trpt->o_pm&1) continue;\n");
576 fprintf(tm, " _m = 3; goto P999;\n");
580 fprintf(tb, " if (II == 0) goto R999;\n");
582 fprintf(tb, " switch (t->back) {\n");
583 fprintf(tb, " default: Uerror(\"bad return move\");\n");
584 fprintf(tb, " case 0: goto R999; /* nothing to undo */\n");
586 for (p = rdy; p; p = p->nxt)
592 for (p = rdy; p; p = p->nxt)
593 fprintf(th, "extern short src_ln%d[];\n", p->tn);
594 for (p = rdy; p; p = p->nxt)
595 fprintf(th, "extern S_F_MAP src_file%d[];\n", p->tn);
598 fprintf(tc, "uchar reached%d[3]; /* np_ */\n", nrRdy);
599 fprintf(tc, "uchar *loopstate%d; /* np_ */\n", nrRdy);
601 fprintf(tc, "struct {\n");
602 fprintf(tc, " int tp; short *src;\n");
603 fprintf(tc, "} src_all[] = {\n");
604 for (p = rdy; p; p = p->nxt)
605 fprintf(tc, " { %d, &src_ln%d[0] },\n",
607 fprintf(tc, " { 0, (short *) 0 }\n");
610 fprintf(tc, "S_F_MAP *flref[] = {\n"); /* 5.3.0 */
611 for (p = rdy; p; p = p->nxt)
612 { fprintf(tc, " src_file%d%c\n", p->tn, p->nxt?',':' ');
614 fprintf(tc, "};\n\n");
616 { fprintf(tc, "extern uchar reached%d[3]; /* np_ */\n", nrRdy);
619 gencodetable(tc); /* was th */
621 if (Unique < (1 << (8*sizeof(unsigned char)) )) /* was uniq before */
622 { fprintf(th, "#define T_ID unsigned char\n");
623 } else if (Unique < (1 << (8*sizeof(unsigned short)) ))
624 { fprintf(th, "#define T_ID unsigned short\n");
626 { fprintf(th, "#define T_ID unsigned int\n");
633 fprintf(tt, "}\n\n"); /* end of settable() */
635 fprintf(tm, "#undef rand\n");
636 fprintf(tm, " }\n\n");
637 fprintf(tb, " }\n\n");
640 { ntimes(tt, 0, 1, Tail);
643 { fprintf(th, "#define FORWARD_MOVES\t\"pan_s.m\"\n");
644 fprintf(th, "#define BACKWARD_MOVES\t\"pan_s.b\"\n");
645 fprintf(th, "#define SEPARATE\n");
646 fprintf(th, "#define TRANSITIONS\t\"pan_s.t\"\n");
647 fprintf(th, "extern void ini_claim(int, int);\n");
649 { fprintf(th, "#define FORWARD_MOVES\t\"pan.m\"\n");
650 fprintf(th, "#define BACKWARD_MOVES\t\"pan.b\"\n");
651 fprintf(th, "#define TRANSITIONS\t\"pan.t\"\n");
659 if (!run) fatal("no runable process", (char *)0);
660 fprintf(tc, "void\n");
661 fprintf(tc, "active_procs(void)\n{\n");
663 fprintf(tc, " if (reversing == 0) {\n");
665 fprintf(tc, " } else {\n");
670 ntimes(tc, 0, 1, Dfa);
671 ntimes(tc, 0, 1, Xpt);
673 fprintf(th, "#define NTRANS %d\n", uniq);
674 if (u_sync && !u_async)
675 { spit_recvs(th, tc);
679 fprintf(th, "#define FORWARD_MOVES\t\"pan_t.m\"\n");
680 fprintf(th, "#define BACKWARD_MOVES\t\"pan_t.b\"\n");
681 fprintf(th, "#define TRANSITIONS\t\"pan_t.t\"\n");
682 fprintf(tc, "extern int Maxbody;\n");
683 fprintf(tc, "#if VECTORSZ>32000\n");
684 fprintf(tc, " extern int *proc_offset;\n");
685 fprintf(tc, "#else\n");
686 fprintf(tc, " extern short *proc_offset;\n");
687 fprintf(tc, "#endif\n");
688 fprintf(tc, "extern uchar *proc_skip;\n");
689 fprintf(tc, "extern uchar *reached[];\n");
690 fprintf(tc, "extern uchar *accpstate[];\n");
691 fprintf(tc, "extern uchar *progstate[];\n");
692 fprintf(tc, "extern uchar *loopstate[];\n");
693 fprintf(tc, "extern uchar *stopstate[];\n");
694 fprintf(tc, "extern uchar *visstate[];\n\n");
695 fprintf(tc, "extern short *mapstate[];\n");
697 fprintf(tc, "void\nini_claim(int n, int h)\n{");
698 fprintf(tc, "\textern State now;\n");
699 fprintf(tc, "\textern void set_claim(void);\n\n");
700 fprintf(tc, "#ifdef PROV\n");
701 fprintf(tc, " #include PROV\n");
702 fprintf(tc, "#endif\n");
703 fprintf(tc, "\tset_claim();\n");
705 fprintf(tc, "\n\tswitch (n) {\n");
707 fprintf(tc, "\t}\n");
708 fprintf(tc, "\n}\n");
709 fprintf(tc, "int\nstep_claim(int o_pm, int tau, int tt, int ot, Trans *t)\n");
710 fprintf(tc, "{ int forw = t->forw; int _m = 0; extern char *noptr; int II=0;\n");
711 fprintf(tc, " extern State now;\n");
712 fprintf(tc, "#define continue return 0\n");
713 fprintf(tc, "#include \"pan_t.m\"\n");
714 fprintf(tc, "P999:\n\treturn _m;\n}\n");
715 fprintf(tc, "#undef continue\n");
716 fprintf(tc, "int\nrev_claim(int backw)\n{ return 0; }\n");
717 fprintf(tc, "#include TRANSITIONS\n");
725 fprintf(th, "#if defined(BFS_PAR) || NCORE>1\n");
726 fprintf(th, " void e_critical(int);\n");
727 fprintf(th, " void x_critical(int);\n");
728 fprintf(th, " #ifdef BFS_PAR\n");
729 fprintf(th, " void bfs_main(int, int);\n");
730 fprintf(th, " void bfs_report_mem(void);\n");
731 fprintf(th, " #endif\n");
732 fprintf(th, "#endif\n");
734 fprintf(th, "\n\n/* end of PAN_H */\n#endif\n");
740 if (!(th = fopen("pan.p", MFLAGS)))
741 { printf("spin: cannot create pan.p for -DBFS_PAR\n");
742 return; /* we're done anyway */
745 ntimes(th, 0, 1, pan_par); /* BFS_PAR */
748 fprintf(tc, "\nTrans *t_id_lkup[%d];\n\n", globmax+1);
751 { fprintf(tc, "\n#ifdef BFS_PAR\n\t#include \"pan.p\"\n#endif\n");
753 fprintf(tc, "\n/* end of pan.c */\n");
762 for (p = rdy; p; p = p->nxt)
769 dolen(Symbol *s, char *pre, int pid, int ai, int qln)
772 fprintf(tc, "\n\t\t\t || ");
773 fprintf(tc, "%s(", pre);
776 fprintf(tc, "(int) ( ((P%d *)this)->", pid);
778 fprintf(tc, "(int) ( now.");
780 fprintf(tc, "%s", s->name);
781 if (qln > 1 || s->isarray) fprintf(tc, "[%d]", ai);
785 struct AA { char TT[9]; char CC[8]; };
787 static struct AA BB[4] = {
788 { "Q_FULL_F", " q_full" },
789 { "Q_FULL_T", "!q_full" },
790 { "Q_EMPT_F", " !q_len" },
791 { "Q_EMPT_T", " q_len" }
794 static struct AA DD[4] = {
795 { "Q_FULL_F", " q_e_f" }, /* empty or full */
796 { "Q_FULL_T", "!q_full" },
797 { "Q_EMPT_F", " q_e_f" },
798 { "Q_EMPT_T", " q_len" }
800 /* this reduces the number of cases where 's' and 'r'
801 are considered conditionally safe under the
802 partial order reduction rules; as a price for
803 this simple implementation, it also affects the
804 cases where nfull and nempty can be considered
805 safe -- since these are labeled the same way as
806 's' and 'r' respectively
807 it only affects reduction, not functionality
811 bb_or_dd(int j, int which)
815 fprintf(tc, "%s", DD[j].CC);
817 fprintf(tc, "%s", BB[j].CC);
820 fprintf(tc, "%s", DD[j].TT);
822 fprintf(tc, "%s", BB[j].TT);
827 Done_case(char *nm, Symbol *z)
832 fprintf(tc, "\t\tcase %d: if (", nid);
833 for (j = 0; j < 4; j++)
834 { fprintf(tc, "\t(t->ty[i] == ");
836 fprintf(tc, " && (");
837 for (k = 0; k < qln; k++)
839 fprintf(tc, "\n\t\t\t || ");
841 fprintf(tc, "(%s%s", nm, z->name);
843 fprintf(tc, "[%d]", k);
846 fprintf(tc, "))\n\t\t\t ");
852 fprintf(tc, ") return 0; break;\n");
856 Docase(Symbol *s, int pid, int nid)
859 fprintf(tc, "\t\tcase %d: if (", nid);
860 for (j = 0; j < 4; j++)
861 { fprintf(tc, "\t(t->ty[i] == ");
863 fprintf(tc, " && (");
865 { for (i = 0; i < s->nel; i++)
866 dolen(s, DD[j].CC, pid, i, s->nel);
868 { for (i = 0; i < s->nel; i++)
869 dolen(s, BB[j].CC, pid, i, s->nel);
871 fprintf(tc, "))\n\t\t\t ");
877 fprintf(tc, ") return 0; break;\n");
881 genconditionals(void)
884 extern Ordered *all_names;
887 fprintf(th, "#define LOCAL 1\n");
888 fprintf(th, "#define Q_FULL_F 2\n");
889 fprintf(th, "#define Q_EMPT_F 3\n");
890 fprintf(th, "#define Q_EMPT_T 4\n");
891 fprintf(th, "#define Q_FULL_T 5\n");
892 fprintf(th, "#define TIMEOUT_F 6\n");
893 fprintf(th, "#define GLOBAL 7\n");
894 fprintf(th, "#define BAD 8\n");
895 fprintf(th, "#define ALPHA_F 9\n");
897 fprintf(tc, "int\n");
898 fprintf(tc, "q_cond(short II, Trans *t)\n");
899 fprintf(tc, "{ int i = 0;\n");
900 fprintf(tc, " for (i = 0; i < 6; i++)\n");
901 fprintf(tc, " { if (t->ty[i] == TIMEOUT_F) return %s;\n",
902 (Etimeouts)?"(!(trpt->tau&1))":"1");
903 fprintf(tc, " if (t->ty[i] == ALPHA_F)\n");
904 fprintf(tc, "#ifdef GLOB_ALPHA\n");
905 fprintf(tc, " return 0;\n");
906 fprintf(tc, "#else\n\t\t\treturn ");
907 fprintf(tc, "(II+1 == (short) now._nr_pr && II+1 < MAXPROC);\n");
908 fprintf(tc, "#endif\n");
910 /* we switch on the chan name from the spec (as identified by
911 * the corresponding Nid number) rather than the actual qid
912 * because we cannot predict at compile time which specific qid
913 * will be accessed by the statement at runtime. that is:
914 * we do not know which qid to pass to q_cond at runtime
915 * but we do know which name is used. if it's a chan array, we
916 * must check all elements of the array for compliance (bummer)
918 fprintf(tc, " switch (t->qu[i]) {\n");
919 fprintf(tc, " case 0: break;\n");
921 for (walk = all_names; walk; walk = walk->next)
923 if (s->owner) continue;
924 j = find_id(s->context);
926 { if (last == s->Nid) continue; /* chan array */
929 } else if (s->type == STRUCT)
930 { /* struct may contain a chan */
932 extern void walk2_struct(char *, Symbol *);
936 sprintf(pregat, "((P%d *)this)->",j);
938 sprintf(pregat, "now.");
940 walk2_struct(pregat, s);
943 fprintf(tc, " \tdefault: Uerror(\"unknown qid - q_cond\");\n");
944 fprintf(tc, " \t\t\treturn 0;\n");
945 fprintf(tc, " \t}\n");
947 fprintf(tc, " return 1;\n");
951 extern int find_min(Sequence *);
952 extern int find_max(Sequence *);
959 if (pid_is_claim(Pid)
961 { fprintf(th, "extern uchar reached%d[];\n", Pid);
963 fprintf(th, "extern short _nstates%d;\n", Pid);
965 fprintf(th, "\n#define _nstates%d %d\t/* %s */\n",
966 Pid, p->s->maxel, p->n->name);
968 fprintf(th, "extern short src_ln%d[];\n", Pid);
969 fprintf(th, "extern uchar *loopstate%d;\n", Pid);
970 fprintf(th, "extern S_F_MAP src_file%d[];\n", Pid);
971 fprintf(th, "#define _endstate%d %d\n",
972 Pid, p->s->last?p->s->last->seqno:0);
975 if (!pid_is_claim(Pid)
977 { fprintf(th, "extern short src_ln%d[];\n", Pid);
978 fprintf(th, "extern uchar *loopstate%d;\n", Pid);
982 AllGlobal = (p->prov)?1:0; /* process has provided clause */
984 fprintf(th, "\n#define _nstates%d %d\t/* %s */\n",
985 Pid, p->s->maxel, p->n->name);
987 fprintf(th, "#define minseq%d %d\n", Pid, find_min(p->s));
988 fprintf(th, "#define maxseq%d %d\n", Pid, find_max(p->s));
992 if (Pid == eventmapnr)
993 fprintf(th, "#define nstates_event _nstates%d\n", Pid);
995 fprintf(th, "#define _endstate%d %d\n", Pid, p->s->last?p->s->last->seqno:0);
997 if (p->b == N_CLAIM || p->b == E_TRACE || p->b == N_TRACE)
998 { fprintf(tm, "\n /* CLAIM %s */\n", p->n->name);
999 fprintf(tb, "\n /* CLAIM %s */\n", p->n->name);
1002 { fprintf(tm, "\n /* PROC %s */\n", p->n->name);
1003 fprintf(tb, "\n /* PROC %s */\n", p->n->name);
1005 fprintf(tt, "\n /* proctype %d: %s */\n", Pid, p->n->name);
1006 fprintf(tt, "\n trans[%d] = (Trans **)", Pid);
1007 fprintf(tt, " emalloc(%d*sizeof(Trans *));\n\n", p->s->maxel);
1009 if (Pid == eventmapnr)
1010 { fprintf(th, "\n#define in_s_scope(x_y3_) 0");
1011 fprintf(tc, "\n#define in_r_scope(x_y3_) 0");
1013 put_seq(p->s, 2, 0);
1014 if (Pid == eventmapnr)
1015 { fprintf(th, "\n\n");
1016 fprintf(tc, "\n\n");
1018 dumpsrc(p->s->maxel, Pid);
1027 for (i = 0; i < T_sum; i++)
1030 TPE[(T_sum++)%2] = x;
1034 cnt_seq(Sequence *s)
1039 for (f = s->frst; f; f = f->nxt)
1040 { Tpe(f->n); /* sets EPT */
1043 for (h = f->sub; h; h = h->nxt)
1051 typ_seq(Sequence *s)
1054 TPE[0] = 2; TPE[1] = 0;
1056 if (T_sum > 2) /* more than one type */
1057 { TPE[0] = 5*DELTA; /* non-mixing */
1067 case FULL: case EMPTY:
1068 case NFULL: case NEMPTY: case TIMEOUT:
1069 Nn[(T_mus++)%2] = n;
1071 case '!': case UMIN: case '~': case ASSERT: case 'c':
1072 (void) hidden(n->lft);
1074 case '/': case '*': case '-': case '+':
1075 case '%': case LT: case GT: case '&': case '^':
1076 case '|': case LE: case GE: case NE: case '?':
1077 case EQ: case OR: case AND: case LSHIFT: case RSHIFT:
1078 (void) hidden(n->lft);
1079 (void) hidden(n->rgt);
1089 && n->sym->type == STRUCT
1090 && n->rgt && n->rgt->lft)
1091 return getNid(n->rgt->lft);
1093 if (!n->sym || n->sym->Nid == 0)
1094 { fatal("bad channel name '%s'",
1095 (n->sym)?n->sym->name:"no name");
1105 2+1 .. 2+1*DELTA = nfull, 's' - require q_full==false
1106 2+1+1*DELTA .. 2+2*DELTA = nempty, 'r' - require q_len!=0
1107 2+1+2*DELTA .. 2+3*DELTA = empty - require q_len==0
1108 2+1+3*DELTA .. 2+4*DELTA = full - require q_full==true
1109 5*DELTA = non-mixing (i.e., always makes the selection global)
1110 6*DELTA = timeout (conditionally safe)
1111 7*DELTA = @, process deletion (conditionally safe)
1113 switch (n->ntyp) { /* a series of fall-thru cases: */
1114 case FULL: res += DELTA; /* add 3*DELTA + chan nr */
1115 case EMPTY: res += DELTA; /* add 2*DELTA + chan nr */
1117 case NEMPTY: res += DELTA; /* add 1*DELTA + chan nr */
1119 case NFULL: res += getNid(n->lft); /* add channel nr */
1122 case TIMEOUT: res = 6*DELTA; break;
1123 case '@': res = 7*DELTA; break;
1130 Tpe(Lextok *n) /* mixing in selections */
1132 EPT[0] = 2; EPT[1] = 0;
1140 { if (hidden(n->lft) > 2)
1141 { EPT[0] = 5*DELTA; /* non-mixing */
1148 if (Nn[0]) EPT[0] = valTpe(Nn[0]);
1149 if (Nn[1]) EPT[1] = valTpe(Nn[1]);
1153 put_escp(Element *e)
1157 if (e->esc /* && e->n->ntyp != GOTO */ && e->n->ntyp != '.')
1158 { for (x = e->esc, n = 0; x; x = x->nxt, n++)
1159 { int i = huntele(x->this->frst, e->status, -1)->seqno;
1160 fprintf(tt, "\ttrans[%d][%d]->escp[%d] = %d;\n",
1161 Pid, e->seqno, n, i);
1162 fprintf(tt, "\treached%d[%d] = 1;\n",
1165 for (x = e->esc, n=0; x; x = x->nxt, n++)
1166 { fprintf(tt, " /* escape #%d: %d */\n", n,
1167 huntele(x->this->frst, e->status, -1)->seqno);
1168 put_seq(x->this, 2, 0); /* args?? */
1170 fprintf(tt, " /* end-escapes */\n");
1175 put_sub(Element *e, int Tt0, int Tt1)
1176 { Sequence *s = e->n->sl->this;
1181 putskip(s->frst->seqno);
1182 g = huntstart(s->frst);
1185 if (0) printf("put_sub %d -> %d -> %d\n", e->seqno, s->frst->seqno, a);
1187 if ((e->n->ntyp == ATOMIC
1188 || e->n->ntyp == D_STEP)
1191 s->last->nxt = e->nxt;
1193 typ_seq(s); /* sets TPE */
1195 if (e->n->ntyp == D_STEP)
1196 { int inherit = (e->status&(ATOM|L_ATOM));
1197 fprintf(tm, "\tcase %d: ", uniq++);
1198 fprintf(tm, "// STATE %d - %s:%d - [",
1199 e->seqno, e->n->fn->name, e->n->ln);
1200 comment(tm, e->n, 0);
1201 fprintf(tm, "]\n\t\t");
1203 if (s->last->n->ntyp == BREAK)
1204 OkBreak = target(huntele(s->last->nxt,
1205 s->last->status, -1))->Seqno;
1209 if (!putcode(tm, s, e->nxt, 0, e->n->ln, e->seqno))
1211 fprintf(tm, "\n#if defined(C_States) && (HAS_TRACK==1)\n");
1212 fprintf(tm, "\t\tc_update((uchar *) &(now.c_state[0]));\n");
1213 fprintf(tm, "#endif\n");
1215 fprintf(tm, "\t\t_m = %d", getweight(s->frst->n));
1216 if (m_loss && s->frst->n->ntyp == 's')
1217 fprintf(tm, "+delta_m; delta_m = 0");
1218 fprintf(tm, "; goto P999;\n\n");
1221 fprintf(tb, "\tcase %d: ", uniq-1);
1222 fprintf(tb, "// STATE %d\n", e->seqno);
1223 fprintf(tb, "\t\tsv_restor();\n");
1224 fprintf(tb, "\t\tgoto R999;\n");
1226 a = huntele(e->nxt, e->status, -1)->seqno;
1230 fprintf(tt, "/*->*/\ttrans[%d][%d]\t= ",
1232 fprintf(tt, "settr(%d,%d,%d,%d,%d,\"",
1233 e->Seqno, D_ATOM|inherit, a, uniq-1, uniq-1);
1234 comment(tt, e->n, e->seqno);
1235 fprintf(tt, "\", %d, ", (s->frst->status&I_GLOB)?1:0);
1236 fprintf(tt, "%d, %d);\n", TPE[0], TPE[1]);
1239 { /* ATOMIC or NON_ATOMIC */
1240 fprintf(tt, "\tT = trans[ %d][%d] = ", Pid, e->seqno);
1241 fprintf(tt, "settr(%d,%d,0,0,0,\"",
1242 e->Seqno, (e->n->ntyp == ATOMIC)?ATOM:0);
1243 comment(tt, e->n, e->seqno);
1244 if ((e->status&CHECK2)
1245 || (g->status&CHECK2))
1246 s->frst->status |= I_GLOB;
1247 fprintf(tt, "\", %d, %d, %d);",
1248 (s->frst->status&I_GLOB)?1:0, Tt0, Tt1);
1250 fprintf(tt, "\tT->nxt\t= ");
1251 fprintf(tt, "settr(%d,%d,%d,0,0,\"",
1252 e->Seqno, (e->n->ntyp == ATOMIC)?ATOM:0, a);
1253 comment(tt, e->n, e->seqno);
1254 fprintf(tt, "\", %d, ", (s->frst->status&I_GLOB)?1:0);
1255 if (e->n->ntyp == NON_ATOMIC)
1256 { fprintf(tt, "%d, %d);", Tt0, Tt1);
1258 put_seq(s, Tt0, Tt1);
1260 { fprintf(tt, "%d, %d);", TPE[0], TPE[1]);
1262 put_seq(s, TPE[0], TPE[1]);
1267 typedef struct CaseCache {
1272 struct CaseCache *nxt;
1275 static CaseCache *casing[6];
1278 identical(Lextok *p, Lextok *q)
1280 if ((!p && q) || (p && !q))
1285 if (p->ntyp != q->ntyp
1286 || p->ismtyp != q->ismtyp
1288 || p->indstep != q->indstep
1294 return identical(p->lft, q->lft)
1295 && identical(p->rgt, q->rgt);
1299 samedeads(FSM_use *a, FSM_use *b)
1302 for (p = a, q = b; p && q; p = p->nxt, q = q->nxt)
1303 if (p->var != q->var
1304 || p->special != q->special)
1310 findnext(Element *f)
1313 if (f->n->ntyp == GOTO)
1314 { g = get_lab(f->n, 1);
1315 return huntele(g, f->status, -1);
1321 advance(Element *e, int stopat)
1325 while (f && f->seqno != stopat)
1330 switch (f->n->ntyp) {
1339 return (Element *) 0;
1343 equiv_merges(Element *a, Element *b)
1345 int stopat_a, stopat_b;
1348 stopat_a = a->merge_start;
1350 stopat_a = a->merge;
1353 stopat_b = b->merge_start;
1355 stopat_b = b->merge;
1357 if (!stopat_a && !stopat_b)
1360 f = advance(a, stopat_a);
1361 g = advance(b, stopat_b);
1367 return identical(f->n, g->n);
1373 prev_case(Element *e, int owner)
1374 { int j; CaseCache *nc;
1376 switch (e->n->ntyp) {
1377 case 'r': j = 0; break;
1378 case 's': j = 1; break;
1379 case 'c': j = 2; break;
1380 case ASGN: j = 3; break;
1381 case ASSERT: j = 4; break;
1382 default: j = 5; break;
1384 for (nc = casing[j]; nc; nc = nc->nxt)
1385 if (identical(nc->n, e->n)
1386 && samedeads(nc->u, e->dead)
1387 && equiv_merges(nc->e, e)
1388 && nc->owner == owner)
1391 return (CaseCache *) 0;
1395 new_case(Element *e, int m, int b, int owner)
1396 { int j; CaseCache *nc;
1398 switch (e->n->ntyp) {
1399 case 'r': j = 0; break;
1400 case 's': j = 1; break;
1401 case 'c': j = 2; break;
1402 case ASGN: j = 3; break;
1403 case ASSERT: j = 4; break;
1404 default: j = 5; break;
1406 nc = (CaseCache *) emalloc(sizeof(CaseCache));
1413 nc->nxt = casing[j];
1423 switch (e->n->ntyp) {
1425 if (check_track(e->n) == STRUCT) { break; }
1430 nr++; /* random recv */
1431 for (v = e->n->rgt; v; v = v->rgt)
1432 { if ((v->lft->ntyp == CONST
1433 || v->lft->ntyp == EVAL))
1441 for (u = e->dead; u; u = u->nxt)
1442 { switch (u->special) {
1443 case 2: /* dead after write */
1444 if (e->n->ntyp == ASGN
1445 && e->n->rgt->ntyp == CONST
1446 && e->n->rgt->val == 0)
1450 case 1: /* dead after read */
1459 { Element *f = e, *g;
1464 stopat = e->merge_start;
1468 printf("merge: %d merge_start %d - seqno %d\n",
1469 e->merge, e->merge_start, e->seqno);
1474 if (f->n->ntyp == GOTO)
1475 { g = get_lab(f->n, 1);
1476 if (g->seqno == stopat)
1479 f = huntele(g, f->status, stopat);
1485 if (f && !f->merge && !f->merge_single && f->seqno != stopat)
1486 { fprintf(tm, "\n\t\t// bad hop %s:%d -- at %d, <",
1487 f->n->fn->name,f->n->ln, f->seqno);
1488 comment(tm, f->n, 0);
1489 fprintf(tm, "> looking for %d -- merge %d:%d:%d ",
1490 stopat, f->merge, f->merge_start, f->merge_single);
1493 } while (f && f->seqno != stopat);
1502 { fprintf(tm, "(trpt+1)->bup.ovals = grab_ints(%d);\n\t\t",
1504 multi_undo = multi_needed;
1510 doforward(FILE *tm_fd, Element *e)
1513 putstmnt(tm_fd, e->n, e->seqno);
1515 if (e->n->ntyp != ELSE && Det)
1516 { fprintf(tm_fd, ";\n\t\tif (trpt->o_pm&1)\n\t\t");
1517 fprintf(tm_fd, "\tuerror(\"non-determinism in D_proctype\")");
1519 if (deadvar && !has_code)
1520 for (u = e->dead; u; u = u->nxt)
1521 { fprintf(tm_fd, ";\n\t\t");
1522 fprintf(tm_fd, "if (TstOnly) return 1; /* TT */\n");
1523 fprintf(tm_fd, "\t\t/* dead %d: %s */ ",
1524 u->special, u->var->name);
1526 switch (u->special) {
1527 case 2: /* dead after write -- lval already bupped */
1528 if (e->n->ntyp == ASGN) /* could be recv or asgn */
1529 { if (e->n->rgt->ntyp == CONST
1530 && e->n->rgt->val == 0)
1531 continue; /* already set to 0 */
1533 if (e->n->ntyp != 'r')
1535 fprintf(tm_fd, "\n#ifdef HAS_CODE\n");
1536 fprintf(tm_fd, "\t\tif (!readtrail)\n");
1537 fprintf(tm_fd, "#endif\n\t\t\t");
1538 putname(tm_fd, "", &XZ, 0, " = 0");
1540 } /* else fall through */
1541 case 1: /* dead after read -- add asgn of rval -- needs bup */
1542 YZ[YZmax].sym = u->var; /* store for pan.b */
1543 CnT[YZcnt]++; /* this step added bups */
1546 fprintf(tm_fd, "(trpt+1)->bup.ovals[%d] = ",
1550 fprintf(tm_fd, "(trpt+1)->bup.oval = ");
1551 putname(tm_fd, "", &YZ[YZmax], 0, ";\n");
1552 fprintf(tm_fd, "#ifdef HAS_CODE\n");
1553 fprintf(tm_fd, "\t\tif (!readtrail)\n");
1554 fprintf(tm_fd, "#endif\n\t\t\t");
1555 putname(tm_fd, "", &YZ[YZmax], 0, " = 0");
1559 fprintf(tm_fd, ";\n\t\t");
1563 dobackward(Element *e, int casenr)
1565 if (!any_undo(e->n) && CnT[YZcnt] == 0)
1571 { fprintf(tb, "\n\tcase %d: ", casenr);
1572 fprintf(tb, "// STATE %d\n\t\t", e->seqno);
1577 while (CnT[YZcnt] > 0) /* undo dead variable resets */
1581 fatal("cannot happen, dobackward", (char *)0);
1582 fprintf(tb, ";\n\t/* %d */\t", YZmax);
1583 putname(tb, "", &YZ[YZmax], 0, " = trpt->bup.oval");
1586 fprintf(tb, "s[%d]", multi_oval-1);
1590 if (e->n->ntyp != '.')
1591 { fprintf(tb, ";\n\t\t");
1592 undostmnt(e->n, e->seqno);
1601 lastfirst(int stopat, Element *fin, int casenr)
1602 { Element *f = fin, *g;
1604 if (f->n->ntyp == GOTO)
1605 { g = get_lab(f->n, 1);
1606 if (g->seqno == stopat)
1609 f = huntele(g, f->status, stopat);
1613 if (!f || f->seqno == stopat
1614 || (!f->merge && !f->merge_single))
1616 lastfirst(stopat, f, casenr);
1618 fprintf(tb, "\n\t/* merge %d -- %d:%d %d:%d:%d (casenr %d) ",
1620 f->merge_start, f->merge,
1621 f->seqno, f?f->seqno:-1, stopat,
1623 comment(tb, f->n, 0);
1624 fprintf(tb, " */\n");
1627 dobackward(f, casenr);
1630 static int modifier;
1633 lab_transfer(Element *to, Element *from)
1634 { Symbol *ns, *s = has_lab(from, (1|2|4));
1640 /* "from" could have all three labels -- rename
1641 * to prevent jumps to the transfered copies
1643 oc = context; /* remember */
1644 for (ltp = 1; ltp < 8; ltp *= 2) /* 1, 2, and 4 */
1645 if ((s = has_lab(from, ltp)) != (Symbol *) 0)
1646 { ns = (Symbol *) emalloc(sizeof(Symbol));
1647 ns->name = (char *) emalloc((int) strlen(s->name) + 4);
1648 sprintf(ns->name, "%s%d", s->name, modifier);
1650 context = s->context;
1654 context = oc; /* restore */
1656 { if (modifier++ > 990)
1657 fatal("modifier overflow error", (char *) 0);
1662 case_cache(Element *e, int a)
1663 { int bupcase = 0, casenr = uniq, fromcache = 0;
1664 CaseCache *Cached = (CaseCache *) 0;
1666 int j, nrbups, mark, ntarget;
1669 mark = (e->status&ATOM); /* could lose atomicity in a merge chain */
1671 if (e->merge_mark > 0
1672 || (merger && e->merge_in == 0))
1673 { /* state nominally unreachable (part of merge chains) */
1674 if (e->n->ntyp != '.'
1675 && e->n->ntyp != GOTO)
1676 { fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno);
1677 fprintf(tt, "settr(0,0,0,0,0,\"");
1678 comment(tt, e->n, e->seqno);
1679 fprintf(tt, "\",0,0,0);\n");
1681 { fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno);
1682 casenr = 1; /* mhs example */
1684 goto haveit; /* pakula's example */
1690 fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno);
1693 && !pid_is_claim(Pid)
1694 && Pid != eventmapnr
1695 && (Cached = prev_case(e, Pid)))
1696 { bupcase = Cached->b;
1700 fprintf(tm, "// STATE %d - %s:%d - [",
1701 e->seqno, e->n->fn->name, e->n->ln);
1702 comment(tm, e->n, 0);
1703 fprintf(tm, "] (%d:%d - %d) same as %d (%d:%d - %d)\n",
1704 e->merge_start, e->merge, e->merge_in,
1706 Cached->e->merge_start, Cached->e->merge, Cached->e->merge_in);
1711 fprintf(tm, "\tcase %d: // STATE %d - %s:%d - [",
1712 uniq++, e->seqno, e->n->fn->name, e->n->ln);
1713 comment(tm, e->n, 0);
1714 nrbups = (e->merge || e->merge_start) ? nrhops(e) : nr_bup(e);
1715 fprintf(tm, "] (%d:%d:%d - %d)\n\t\t",
1716 e->merge_start, e->merge, nrbups, e->merge_in);
1718 if (nrbups > MAXMERGE-1)
1719 fatal("merge requires more than 256 bups", (char *)0);
1721 if (e->n->ntyp != 'r' && !pid_is_claim(Pid) && Pid != eventmapnr)
1722 fprintf(tm, "IfNotBlocked\n\t\t");
1724 if (multi_needed != 0 || multi_undo != 0)
1725 fatal("cannot happen, case_cache", (char *) 0);
1729 multi_needed = nrbups; /* allocated after edge condition */
1733 memset(CnT, 0, sizeof(CnT));
1736 /* new 4.2.6, revised 6.0.0 */
1737 if (pid_is_claim(Pid))
1738 { fprintf(tm, "\n#if defined(VERI) && !defined(NP)\n");
1739 fprintf(tm, "#if NCLAIMS>1\n\t\t");
1740 fprintf(tm, "{ static int reported%d = 0;\n\t\t", e->seqno);
1741 fprintf(tm, " if (verbose && !reported%d)\n\t\t", e->seqno);
1742 fprintf(tm, " { int nn = (int) ((Pclaim *)pptr(0))->_n;\n\t\t");
1743 fprintf(tm, " printf(\"depth %%ld: Claim %%s (%%d), state %%d (line %%d)\\n\",\n\t\t");
1744 fprintf(tm, " depth, procname[spin_c_typ[nn]], nn, ");
1745 fprintf(tm, "(int) ((Pclaim *)pptr(0))->_p, src_claim[ (int) ((Pclaim *)pptr(0))->_p ]);\n\t\t");
1746 fprintf(tm, " reported%d = 1;\n\t\t", e->seqno);
1747 fprintf(tm, " fflush(stdout);\n\t\t");
1748 fprintf(tm, "} }\n");
1749 fprintf(tm, "#else\n\t\t");
1750 fprintf(tm, "{ static int reported%d = 0;\n\t\t", e->seqno);
1751 fprintf(tm, " if (verbose && !reported%d)\n\t\t", e->seqno);
1752 fprintf(tm, " { printf(\"depth %%d: Claim, state %%d (line %%d)\\n\",\n\t\t");
1753 fprintf(tm, " (int) depth, (int) ((Pclaim *)pptr(0))->_p, ");
1754 fprintf(tm, "src_claim[ (int) ((Pclaim *)pptr(0))->_p ]);\n\t\t");
1755 fprintf(tm, " reported%d = 1;\n\t\t", e->seqno);
1756 fprintf(tm, " fflush(stdout);\n\t\t");
1757 fprintf(tm, "} }\n");
1758 fprintf(tm, "#endif\n");
1759 fprintf(tm, "#endif\n\t\t");
1763 /* the src xrefs have the numbers in e->seqno builtin */
1764 fprintf(tm, "reached[%d][%d] = 1;\n\t\t", Pid, e->seqno);
1769 ntarget = e->merge_start;
1776 more: if (f->n->ntyp == GOTO)
1777 { g = get_lab(f->n, 1);
1778 if (g->seqno == ntarget)
1781 f = huntele(g, f->status, ntarget);
1786 if (f && f->seqno != ntarget)
1787 { if (!f->merge && !f->merge_single)
1788 { fprintf(tm, "/* stop at bad hop %d, %d */\n\t\t",
1792 fprintf(tm, "/* merge: ");
1793 comment(tm, f->n, 0);
1794 fprintf(tm, "(%d, %d, %d) */\n\t\t", f->merge, f->seqno, ntarget);
1795 fprintf(tm, "reached[%d][%d] = 1;\n\t\t", Pid, f->seqno);
1798 mark = f->status&(ATOM|L_ATOM); /* last step wins */
1800 if (f->merge_in == 1) f->merge_mark++;
1805 fprintf(tm, "_m = %d", getweight(e->n));
1806 if (m_loss && e->n->ntyp == 's') fprintf(tm, "+delta_m; delta_m = 0");
1807 fprintf(tm, "; goto P999; /* %d */\n", YZcnt);
1813 lastfirst(ntarget, e, casenr); /* mergesteps only */
1815 dobackward(e, casenr); /* the original step */
1817 fprintf(tb, ";\n\t\t");
1819 if (e->merge || e->merge_start)
1821 { fprintf(tb, "\n\tcase %d: ", casenr);
1822 fprintf(tb, "// STATE %d", e->seqno);
1828 fprintf(tb, "\n\t\t");
1831 { fprintf(tb, "ungrab_ints(trpt->bup.ovals, %d);\n\t\t",
1836 { fprintf(tb, "goto R999;\n");
1840 if (!e->merge && !e->merge_start)
1841 new_case(e, casenr, bupcase, Pid);
1850 fprintf(tt, "%ssettr(%d,%d,%d,%d,%d,\"", fromcache?"/* c */ ":"",
1851 e->Seqno, mark, j, casenr, bupcase);
1853 return (fromcache)?0:casenr;
1857 put_el(Element *e, int Tt0, int Tt1)
1858 { int a, casenr, Global_ref;
1861 if (e->n->ntyp == GOTO)
1862 { g = get_lab(e->n, 1);
1863 g = huntele(g, e->status, -1);
1864 cross_dsteps(e->n, g->n);
1867 { g = huntele(e->nxt, e->status, -1);
1872 && ((g->status&CHECK2) /* entering remotely ref'd state */
1873 || (e->status&CHECK2))) /* leaving remotely ref'd state */
1874 e->status |= I_GLOB;
1876 /* don't remove dead edges in here, to preserve structure of fsm */
1877 if (e->merge_start || e->merge)
1880 /*** avoid duplicate or redundant cases in pan.m ***/
1881 switch (e->n->ntyp) {
1883 casenr = 2; /* standard else */
1891 casenr = 1; /* standard goto */
1892 generic_case: fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno);
1893 fprintf(tt, "settr(%d,%d,%d,%d,0,\"",
1894 e->Seqno, e->status&ATOM, a, casenr);
1903 if (e->n->lft->ntyp == CONST
1904 && e->n->lft->val == 1) /* skip or true */
1913 casenr = case_cache(e, a);
1914 if (casenr < 0) return; /* unreachable state */
1917 /* tailend of settr(...); */
1918 Global_ref = (e->status&I_GLOB)?1:has_global(e->n);
1919 comment(tt, e->n, e->seqno);
1920 fprintf(tt, "\", %d, ", Global_ref);
1922 { fprintf(tt, "%d, %d);", Tt0, Tt1);
1924 { Tpe(e->n); /* sets EPT */
1925 fprintf(tt, "%d, %d);", EPT[0], EPT[1]);
1927 if ((e->merge_start && e->merge_start != a)
1928 || (e->merge && e->merge != a))
1929 { fprintf(tt, " /* m: %d -> %d,%d */\n",
1930 a, e->merge_start, e->merge);
1931 fprintf(tt, " reached%d[%d] = 1;",
1932 Pid, a); /* Sheinman's example */
1942 nested_unless(Element *e, Element *g)
1943 { struct SeqList *y = e->esc, *z = g->esc;
1945 for ( ; y && z; y = y->nxt, z = z->nxt)
1946 if (z->this != y->this)
1951 if (g->n->ntyp != GOTO
1952 && g->n->ntyp != '.'
1954 { printf("error: (%s:%d) saw 'unless' on a guard:\n",
1955 (e->n)?e->n->fn->name:"-",
1957 printf("=====>instead of\n");
1958 printf(" do (or if)\n");
1959 printf(" :: ...\n");
1960 printf(" :: stmnt1 unless stmnt2\n");
1961 printf(" od (of fi)\n");
1962 printf("=====>use\n");
1963 printf(" do (or if)\n");
1964 printf(" :: ...\n");
1965 printf(" :: stmnt1\n");
1966 printf(" od (or fi) unless stmnt2\n");
1967 printf("=====>or rewrite\n");
1972 put_seq(Sequence *s, int Tt0, int Tt1)
1977 if (0) printf("put_seq %d\n", s->frst->seqno);
1979 for (e = s->frst; e; e = e->nxt)
1981 if (0) printf(" step %d\n", e->seqno);
1982 if (e->status & DONE)
1984 if (0) printf(" done before\n");
1992 if (e->n->ntyp == UNLESS)
1994 if (0) printf(" an unless\n");
1995 put_seq(e->sub->this, Tt0, Tt1);
1998 if (0) printf(" has sub\n");
1999 fprintf(tt, "\tT = trans[%d][%d] = ",
2001 fprintf(tt, "settr(%d,%d,0,0,0,\"",
2002 e->Seqno, e->status&ATOM);
2003 comment(tt, e->n, e->seqno);
2004 if (e->status&CHECK2)
2005 e->status |= I_GLOB;
2006 fprintf(tt, "\", %d, %d, %d);",
2007 (e->status&I_GLOB)?1:0, Tt0, Tt1);
2009 for (h = e->sub; h; h = h->nxt)
2010 { putskip(h->this->frst->seqno);
2011 g = huntstart(h->this->frst);
2013 nested_unless(e, g);
2016 if (g->n->ntyp == 'c'
2017 && g->n->lft->ntyp == CONST
2018 && g->n->lft->val == 0 /* 0 or false */
2020 { fprintf(tt, "#if 0\n\t/* dead link: */\n");
2023 printf("spin: %s:%d, warning, condition is always false\n",
2024 g->n->fn?g->n->fn->name:"", g->n->ln);
2027 if (0) printf(" settr %d %d\n", a, 0);
2029 fprintf(tt, "\tT = T->nxt\t= ");
2031 fprintf(tt, "\t T->nxt\t= ");
2032 fprintf(tt, "settr(%d,%d,%d,0,0,\"",
2033 e->Seqno, e->status&ATOM, a);
2034 comment(tt, e->n, e->seqno);
2035 if (g->status&CHECK2)
2036 h->this->frst->status |= I_GLOB;
2037 fprintf(tt, "\", %d, %d, %d);",
2038 (h->this->frst->status&I_GLOB)?1:0,
2042 fprintf(tt, "#endif\n");
2044 for (h = e->sub; h; h = h->nxt)
2045 put_seq(h->this, Tt0, Tt1);
2048 if (0) printf(" [non]atomic %d\n", e->n->ntyp);
2049 if (e->n->ntyp == ATOMIC
2050 || e->n->ntyp == D_STEP
2051 || e->n->ntyp == NON_ATOMIC)
2052 put_sub(e, Tt0, Tt1);
2055 if (0) printf(" put_el %d\n", e->seqno);
2056 put_el(e, Tt0, Tt1);
2059 checklast: if (e == s->last)
2062 if (0) printf("put_seq done\n");
2066 patch_atomic(Sequence *s) /* catch goto's that break the chain */
2070 for (f = s->frst; f ; f = f->nxt)
2072 if (f->n && f->n->ntyp == GOTO)
2073 { g = get_lab(f->n,1);
2074 cross_dsteps(f->n, g->n);
2075 if ((f->status & (ATOM|L_ATOM))
2076 && !(g->status & (ATOM|L_ATOM)))
2077 { f->status &= ~ATOM;
2078 f->status |= L_ATOM;
2080 /* bridge atomics */
2081 if ((f->status & L_ATOM)
2082 && (g->status & (ATOM|L_ATOM)))
2083 { f->status &= ~L_ATOM;
2087 for (h = f->sub; h; h = h->nxt)
2088 patch_atomic(h->this);
2095 mark_seq(Sequence *s)
2099 for (f = s->frst; f; f = f->nxt)
2100 { f->status |= I_GLOB;
2102 if (f->n->ntyp == ATOMIC
2103 || f->n->ntyp == NON_ATOMIC
2104 || f->n->ntyp == D_STEP)
2105 mark_seq(f->n->sl->this);
2107 for (h = f->sub; h; h = h->nxt)
2115 find_target(Element *e)
2121 { fatal("cycle of goto jumps", (char *) 0);
2123 switch (e->n->ntyp) {
2125 f = get_lab(e->n,1);
2126 cross_dsteps(e->n, f->n);
2131 { f = find_target(huntele(e->nxt, e->status, -1));
2132 break; /* new 5.0 -- was missing */
2134 /* else fall through */
2149 return find_target(e);
2153 seq_has_el(Sequence *s, Element *g) /* new to version 5.0 */
2157 for (f = s->frst; f; f = f->nxt) /* g in same atomic? */
2161 if (f->status & CHECK3)
2164 f->status |= CHECK3; /* protect against cycles */
2165 for (h = f->sub; h; h = h->nxt)
2166 { if (h->this && seq_has_el(h->this, g))
2173 scan_seq(Sequence *s)
2177 for (f = s->frst; f; f = f->nxt)
2178 { if ((f->status&CHECK2)
2179 || has_global(f->n))
2181 if (f->n->ntyp == GOTO /* may exit or reach other atomic */
2182 && !(f->status & D_ATOM)) /* cannot jump from d_step */
2183 { /* consider jump from an atomic without globals into
2184 * an atomic with globals
2185 * example by Claus Traulsen, 22 June 2007
2189 if (g && !seq_has_el(s, g)) /* not internal to this atomic/dstep */
2193 && !(f->status & L_ATOM)
2194 && !(g->status & (ATOM|L_ATOM)))
2196 { fprintf(tt, "\t/* mark-down line %d status %d = %d */\n", f->n->ln, f->status, (f->status & D_ATOM));
2197 return 1; /* assume worst case */
2199 for (h = f->sub; h; h = h->nxt)
2200 if (scan_seq(h->this))
2209 glob_args(Lextok *n)
2213 for (v = n->rgt; v; v = v->rgt)
2214 { if (v->lft->ntyp == CONST)
2216 if (v->lft->ntyp == EVAL)
2217 result += has_global(v->lft->lft);
2219 result += has_global(v->lft);
2225 proc_is_safe(const Lextok *n)
2227 /* not safe unless no local var inits are used */
2228 /* note that a local variable init could refer to a global */
2230 for (p = rdy; p; p = p->nxt)
2231 { if (strcmp(n->sym->name, p->n->name) == 0)
2232 { /* printf("proc %s safety: %d\n", p->n->name, p->unsafe); */
2233 return (p->unsafe != 0);
2235 /* non_fatal("bad call to proc_is_safe", (char *) 0); */
2241 has_global(Lextok *n)
2243 static Symbol *n_seen = (Symbol *) 0;
2246 if (AllGlobal) return 1; /* global provided clause */
2252 return scan_seq(n->sl->this);
2260 case ELSE: return n->val; /* true if combined with chan refs */
2262 case 's': return glob_args(n)!=0 || ((n->sym->xu&(XS|XX)) != XS);
2263 case 'r': return glob_args(n)!=0 || ((n->sym->xu&(XR|XX)) != XR);
2264 case 'R': return glob_args(n)!=0 || (((n->sym->xu)&(XR|XS|XX)) != (XR|XS));
2265 case NEMPTY: return ((n->sym->xu&(XR|XX)) != XR);
2266 case NFULL: return ((n->sym->xu&(XS|XX)) != XS);
2267 case FULL: return ((n->sym->xu&(XR|XX)) != XR);
2268 case EMPTY: return ((n->sym->xu&(XS|XX)) != XS);
2269 case LEN: return (((n->sym->xu)&(XR|XS|XX)) != (XR|XS));
2272 if (strcmp(n->sym->name, "_priority") == 0)
2273 { if (old_priority_rules)
2274 { if (n_seen != n->sym)
2275 fatal("cannot refer to _priority with -o6", (char *) 0);
2281 || (n->sym->hidden&64)
2282 || strcmp(n->sym->name, "_pid") == 0
2283 || strcmp(n->sym->name, "_") == 0)
2288 return proc_is_safe(n);
2290 case C_CODE: case C_EXPR:
2291 return glob_inline(n->sym->name);
2293 case ENABLED: case PC_VAL: case NONPROGRESS:
2295 case TIMEOUT: case SET_P: case GET_P:
2298 /* @ was 1 (global) since 2.8.5
2299 in 3.0 it is considered local and
2300 conditionally safe, provided:
2301 II is the youngest process
2302 and nrprocs < MAXPROCS
2306 case '!': case UMIN: case '~': case ASSERT:
2307 return has_global(n->lft);
2309 case '/': case '*': case '-': case '+':
2310 case '%': case LT: case GT: case '&': case '^':
2311 case '|': case LE: case GE: case NE: case '?':
2312 case EQ: case OR: case AND: case LSHIFT:
2313 case RSHIFT: case 'c': case ASGN:
2314 return has_global(n->lft) || has_global(n->rgt);
2317 for (v = n->lft; v; v = v->rgt)
2318 if (has_global(v->lft)) return 1;
2321 return has_global(n->lft);
2327 Bailout(FILE *fd, char *str)
2330 { fprintf(fd, "continue%s", str);
2332 { fprintf(fd, "%s%s", NextLab[Level], str);
2334 { fprintf(fd, "Uerror(\"block in d_step seq\")%s", str);
2338 #define cat0(x) putstmnt(fd,now->lft,m); fprintf(fd, x); \
2339 putstmnt(fd,now->rgt,m)
2340 #define cat1(x) fprintf(fd,"("); cat0(x); fprintf(fd,")")
2341 #define cat2(x,y) fprintf(fd,x); putstmnt(fd,y,m)
2342 #define cat3(x,y,z) fprintf(fd,x); putstmnt(fd,y,m); fprintf(fd,z)
2343 #define cat30(x,y,z) fprintf(fd,x,0); putstmnt(fd,y,m); fprintf(fd,z)
2346 putstmnt(FILE *fd, Lextok *now, int m)
2350 if (!now) { fprintf(fd, "0"); return; }
2354 switch (now->ntyp) {
2355 case CONST: fprintf(fd, "%d", now->val); break;
2356 case '!': cat3(" !(", now->lft, ")"); break;
2357 case UMIN: cat3(" -(", now->lft, ")"); break;
2358 case '~': cat3(" ~(", now->lft, ")"); break;
2360 case '/': cat1("/"); break;
2361 case '*': cat1("*"); break;
2362 case '-': cat1("-"); break;
2363 case '+': cat1("+"); break;
2364 case '%': cat1("%%"); break;
2365 case '&': cat1("&"); break;
2366 case '^': cat1("^"); break;
2367 case '|': cat1("|"); break;
2368 case LT: cat1("<"); break;
2369 case GT: cat1(">"); break;
2370 case LE: cat1("<="); break;
2371 case GE: cat1(">="); break;
2372 case NE: cat1("!="); break;
2373 case EQ: cat1("=="); break;
2374 case OR: cat1("||"); break;
2375 case AND: cat1("&&"); break;
2376 case LSHIFT: cat1("<<"); break;
2377 case RSHIFT: cat1(">>"); break;
2381 fprintf(fd, "((tau)&1)");
2383 fprintf(fd, "((trpt->tau)&1)");
2385 printf("spin: %s:%d, warning, 'timeout' in d_step sequence\n",
2386 Fname->name, lineno);
2387 /* is okay as a guard */
2391 if (now->sym == NULL)
2392 fatal("internal error pangen2.c", (char *) 0);
2394 && strcmp(now->sym->name, claimproc) == 0)
2395 fatal("claim %s, (not runnable)", claimproc);
2397 && strcmp(now->sym->name, eventmap) == 0)
2398 fatal("eventmap %s, (not runnable)", eventmap);
2401 fatal("'run' in d_step sequence (use atomic)", (char *)0);
2403 fprintf(fd,"addproc(II, %d, %d",
2404 (now->val > 0 && !old_priority_rules) ? now->val : 1,
2405 fproc(now->sym->name));
2406 for (v = now->lft, i = 0; v; v = v->rgt, i++)
2407 { cat2(", ", v->lft);
2409 check_param_count(i, now);
2412 { /* printf("\t%d parameters used, max %d expected\n", i, Npars); */
2413 fatal("too many parameters in run %s(...)", now->sym->name);
2415 for ( ; i < Npars; i++)
2419 /* process now->sym->name has run priority now->val */
2420 if (now->val > 0 && now->val < 256 && !old_priority_rules)
2421 { fprintf(fd, " && (((P0 *)pptr(now._nr_pr - 1))->_priority = %d)", now->val);
2424 if (now->val < 0 || now->val > 255) /* 0 itself is allowed */
2425 { fatal("bad process in run %s, valid range: 1..255", now->sym->name);
2430 cat3("enabled(II, ", now->lft, ")");
2434 if (old_priority_rules)
2437 { cat3("get_priority(", now->lft, ")");
2442 if (!old_priority_rules)
2443 { fprintf(fd, "if (TstOnly) return 1; /* T30 */\n\t\t");
2444 fprintf(fd, "set_priority(");
2445 putstmnt(fd, now->lft->lft, m);
2447 putstmnt(fd, now->lft->rgt, m);
2453 /* o_pm&4=progress, tau&128=claim stutter */
2455 fprintf(fd, "(!(o_pm&4) && !(tau&128))");
2457 fprintf(fd, "(!(trpt->o_pm&4) && !(trpt->tau&128))");
2461 cat3("((P0 *) Pptr(", now->lft, "+BASE))->_p");
2465 if (!terse && !TestOnly && has_xu)
2466 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2467 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
2468 putname(fd, "q_R_check(", now->lft, m, "");
2469 fprintf(fd, ", II)) &&\n\t\t");
2470 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
2471 putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
2472 fprintf(fd, "\n#endif\n\t\t");
2474 putname(fd, "q_len(", now->lft, m, ")");
2478 if (!terse && !TestOnly && has_xu)
2479 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2480 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
2481 putname(fd, "q_R_check(", now->lft, m, "");
2482 fprintf(fd, ", II)) &&\n\t\t");
2483 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
2484 putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
2485 fprintf(fd, "\n#endif\n\t\t");
2487 putname(fd, "q_full(", now->lft, m, ")");
2491 if (!terse && !TestOnly && has_xu)
2492 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2493 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
2494 putname(fd, "q_R_check(", now->lft, m, "");
2495 fprintf(fd, ", II)) &&\n\t\t");
2496 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
2497 putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
2498 fprintf(fd, "\n#endif\n\t\t");
2500 putname(fd, "(q_len(", now->lft, m, ")==0)");
2504 if (!terse && !TestOnly && has_xu)
2505 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2506 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
2507 putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
2508 fprintf(fd, "\n#endif\n\t\t");
2510 putname(fd, "(!q_full(", now->lft, m, "))");
2514 if (!terse && !TestOnly && has_xu)
2515 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2516 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
2517 putname(fd, "q_R_check(", now->lft, m, ", II)) &&");
2518 fprintf(fd, "\n#endif\n\t\t");
2520 putname(fd, "(q_len(", now->lft, m, ")>0)");
2524 if (Pid == eventmapnr)
2525 { fprintf(fd, "if ((II == -EVENT_TRACE && _tp != 's') ");
2526 putname(fd, "|| _qid+1 != ", now->lft, m, "");
2527 for (v = now->rgt, i=0; v; v = v->rgt, i++)
2528 { if (v->lft->ntyp != CONST
2529 && v->lft->ntyp != EVAL)
2531 fprintf(fd, " \\\n\t\t|| qrecv(");
2532 putname(fd, "", now->lft, m, ", ");
2533 putname(fd, "q_len(", now->lft, m, ")-1, ");
2534 fprintf(fd, "%d, 0) != ", i);
2535 if (v->lft->ntyp == CONST)
2536 putstmnt(fd, v->lft, m);
2538 putstmnt(fd, v->lft->lft, m);
2541 fprintf(fd, "\t\t continue");
2542 putname(th, " || (x_y3_ == ", now->lft, m, ")");
2549 putname(fd, "!q_full(", now->lft, m, ")");
2553 { fprintf(fd, "\n#if !defined(XUSAFE) && !defined(NOREDUCE)\n\t\t");
2554 putname(fd, "if (q_claim[", now->lft, m, "]&2)\n\t\t");
2555 putname(fd, "{ q_S_check(", now->lft, m, ", II);\n\t\t");
2557 if (has_sorted && now->val == 1)
2558 { putname(fd, "\t\tif (q_claim[", now->lft, m, "]&1)\n\t\t"); /* &1 iso &2 */
2559 fprintf(fd, "{ uerror(\"sorted send on xr channel violates po reduction\");\n\t\t");
2562 fprintf(fd, "#endif\n\t\t");
2564 fprintf(fd, "if (q_%s",
2565 (u_sync > 0 && u_async == 0)?"len":"full");
2566 putname(fd, "(", now->lft, m, "))\n");
2569 { fprintf(fd, "\t\t{ nlost++; delta_m = 1; } else {");
2571 { fprintf(fd, "\t\t\t");
2575 if (has_enabled || has_priority)
2576 fprintf(fd, "\n\t\tif (TstOnly) return 1; /* T1 */");
2578 if (u_sync && !u_async && rvopt)
2579 fprintf(fd, "\n\n\t\tif (no_recvs(II)) continue;\n");
2581 fprintf(fd, "\n#ifdef HAS_CODE\n");
2582 fprintf(fd, "\t\tif (readtrail && gui) {\n");
2583 fprintf(fd, "\t\t\tchar simtmp[64];\n");
2584 putname(fd, "\t\t\tsprintf(simvals, \"%%d!\", ", now->lft, m, ");\n");
2586 for (v = now->rgt, i = 0; v; v = v->rgt, i++)
2587 { cat3("\t\tsprintf(simtmp, \"%%d\", ", v->lft, "); strcat(simvals, simtmp);");
2589 fprintf(fd, "\t\tstrcat(simvals, \",\");\n");
2592 fprintf(fd, "\t\t}\n");
2593 fprintf(fd, "#endif\n\t\t");
2595 putname(fd, "\n\t\tqsend(", now->lft, m, "");
2596 fprintf(fd, ", %d", now->val);
2597 for (v = now->rgt, i = 0; v; v = v->rgt, i++)
2598 { cat2(", ", v->lft);
2602 putname(stdout, "channel name: ", now->lft, m, "\n");
2604 printf(" %d msg parameters sent, %d expected\n", i, Mpars);
2605 fatal("too many pars in send", "");
2607 for (j = i; i < Mpars; i++)
2609 fprintf(fd, ", %d)", j);
2611 { fprintf(fd, ";\n\t\t");
2613 putname(fd, "if (q_zero(", now->lft, m, ")) ");
2614 putname(fd, "{ boq = ", now->lft, m, "");
2616 fprintf(fd, "; Uerror(\"rv-attempt in d_step\")");
2620 fprintf(fd, ";\n\t\t}\n\t\t"); /* end of m_loss else */
2624 if (Pid == eventmapnr)
2625 { fprintf(fd, "if ((II == -EVENT_TRACE && _tp != 'r') ");
2626 putname(fd, "|| _qid+1 != ", now->lft, m, "");
2627 for (v = now->rgt, i=0; v; v = v->rgt, i++)
2628 { if (v->lft->ntyp != CONST
2629 && v->lft->ntyp != EVAL)
2631 fprintf(fd, " \\\n\t\t|| qrecv(");
2632 putname(fd, "", now->lft, m, ", ");
2633 fprintf(fd, "0, %d, 0) != ", i);
2634 if (v->lft->ntyp == CONST)
2635 putstmnt(fd, v->lft, m);
2637 putstmnt(fd, v->lft->lft, m);
2640 fprintf(fd, "\t\t continue");
2642 putname(tc, " || (x_y3_ == ", now->lft, m, ")");
2647 { fprintf(fd, "((");
2648 if (u_sync) fprintf(fd, "(boq == -1 && ");
2650 putname(fd, "q_len(", now->lft, m, ")");
2652 if (u_sync && now->val <= 1)
2653 { putname(fd, ") || (boq == ", now->lft,m," && ");
2654 putname(fd, "q_zero(", now->lft,m,"))");
2658 if (now->val == 0 || now->val == 2)
2659 { for (v = now->rgt, i=j=0; v; v = v->rgt, i++)
2660 { if (v->lft->ntyp == CONST)
2661 { cat3("\n\t\t&& (", v->lft, " == ");
2662 putname(fd, "qrecv(", now->lft, m, ", ");
2663 fprintf(fd, "0, %d, 0))", i);
2664 } else if (v->lft->ntyp == EVAL)
2665 { cat3("\n\t\t&& (", v->lft->lft, " == ");
2666 putname(fd, "qrecv(", now->lft, m, ", ");
2667 fprintf(fd, "0, %d, 0))", i);
2673 { fprintf(fd, "\n\t\t&& Q_has(");
2674 putname(fd, "", now->lft, m, "");
2675 for (v = now->rgt, i=0; v; v = v->rgt, i++)
2676 { if (v->lft->ntyp == CONST)
2677 { fprintf(fd, ", 1, ");
2678 putstmnt(fd, v->lft, m);
2679 } else if (v->lft->ntyp == EVAL)
2680 { fprintf(fd, ", 1, ");
2681 putstmnt(fd, v->lft->lft, m);
2683 { fprintf(fd, ", 0, 0");
2685 for ( ; i < Mpars; i++)
2686 fprintf(fd, ", 0, 0");
2693 { fprintf(fd, "\n#if !defined(XUSAFE) && !defined(NOREDUCE)\n\t\t");
2694 putname(fd, "if (q_claim[", now->lft, m, "]&1)\n\t\t");
2695 putname(fd, "{ q_R_check(", now->lft, m, ", II);\n\t\t");
2696 if (has_random && now->val != 0)
2697 fprintf(fd, " uerror(\"rand receive on xr channel violates po reduction\");\n\t\t");
2699 fprintf(fd, "#endif\n\t\t");
2702 { if (now->val >= 2)
2704 { fprintf(fd, "if (");
2705 putname(fd, "q_zero(", now->lft,m,"))");
2706 fprintf(fd, "\n\t\t{\t");
2708 fprintf(fd, "uerror(\"polling ");
2709 fprintf(fd, "rv chan\");\n\t\t");
2711 fprintf(fd, " continue;\n\t\t}\n\t\t");
2712 fprintf(fd, "IfNotBlocked\n\t\t");
2714 { fprintf(fd, "if (");
2716 putname(fd, "boq != ", now->lft,m,") ");
2718 { putname(fd, "q_zero(", now->lft,m,"))");
2719 fprintf(fd, "\n\t\t{\tif (boq != ");
2720 putname(fd, "", now->lft,m,") ");
2721 Bailout(fd, ";\n\t\t} else\n\t\t");
2722 fprintf(fd, "{\tif (boq != -1) ");
2724 Bailout(fd, ";\n\t\t");
2726 fprintf(fd, "}\n\t\t");
2728 putname(fd, "if (q_len(", now->lft, m, ") == 0) ");
2731 for (v = now->rgt, j=0; v; v = v->rgt)
2732 { if (v->lft->ntyp != CONST
2733 && v->lft->ntyp != EVAL)
2734 j++; /* count settables */
2736 fprintf(fd, ";\n\n\t\tXX=1");
2737 /* test */ if (now->val == 0 || now->val == 2)
2738 { for (v = now->rgt, i=0; v; v = v->rgt, i++)
2739 { if (v->lft->ntyp == CONST)
2740 { fprintf(fd, ";\n\t\t");
2741 cat3("if (", v->lft, " != ");
2742 putname(fd, "qrecv(", now->lft, m, ", ");
2743 fprintf(fd, "0, %d, 0)) ", i);
2745 } else if (v->lft->ntyp == EVAL)
2746 { fprintf(fd, ";\n\t\t");
2747 cat3("if (", v->lft->lft, " != ");
2748 putname(fd, "qrecv(", now->lft, m, ", ");
2749 fprintf(fd, "0, %d, 0)) ", i);
2752 if (has_enabled || has_priority)
2753 fprintf(fd, ";\n\t\tif (TstOnly) return 1 /* T2 */");
2754 } else /* random receive: val 1 or 3 */
2755 { fprintf(fd, ";\n\t\tif (!(XX = Q_has(");
2756 putname(fd, "", now->lft, m, "");
2757 for (v = now->rgt, i=0; v; v = v->rgt, i++)
2758 { if (v->lft->ntyp == CONST)
2759 { fprintf(fd, ", 1, ");
2760 putstmnt(fd, v->lft, m);
2761 } else if (v->lft->ntyp == EVAL)
2762 { fprintf(fd, ", 1, ");
2763 putstmnt(fd, v->lft->lft, m);
2765 { fprintf(fd, ", 0, 0");
2767 for ( ; i < Mpars; i++)
2768 fprintf(fd, ", 0, 0");
2769 fprintf(fd, "))) ");
2772 if (has_enabled || has_priority)
2773 fprintf(fd, ";\n\t\tif (TstOnly) return 1 /* T2 */");
2775 fprintf(fd, ";\n\t\t");
2778 fprintf(fd, "(trpt+1)->bup.ovals[%d] = ",
2782 { fprintf(fd, "(trpt+1)->bup.oval = ");
2787 if (j == 0 && now->val >= 2)
2788 { fprintf(fd, ";\n\t\t");
2789 break; /* poll without side-effect */
2794 fprintf(fd, ";\n\t\t");
2795 /* no variables modified */
2796 if (j == 0 && now->val == 0)
2797 { fprintf(fd, "\n#ifndef BFS_PAR\n\t\t");
2798 /* q_flds values are not shared among cores */
2799 fprintf(fd, "if (q_flds[((Q0 *)qptr(");
2800 putname(fd, "", now->lft, m, "-1))->_t]");
2801 fprintf(fd, " != %d)\n\t\t\t", i);
2802 fprintf(fd, "Uerror(\"wrong nr of msg fields in rcv\");\n");
2803 fprintf(fd, "#endif\n\t\t");
2806 for (v = now->rgt; v; v = v->rgt)
2807 { if ((v->lft->ntyp != CONST
2808 && v->lft->ntyp != EVAL))
2809 { jj++; /* nr of vars needing bup */
2813 for (v = now->rgt, i = 0; v; v = v->rgt, i++)
2816 if ((v->lft->ntyp == CONST
2817 || v->lft->ntyp == EVAL))
2822 sprintf(tempbuf, "(trpt+1)->bup.ovals[%d] = ",
2826 sprintf(tempbuf, "(trpt+1)->bup.oval = ");
2828 if (v->lft->sym && !strcmp(v->lft->sym->name, "_"))
2829 { fprintf(fd, tempbuf, (char *) 0);
2830 putname(fd, "qrecv(", now->lft, m, "");
2831 fprintf(fd, ", XX-1, %d, 0);\n\t\t", i);
2834 cat30(tempbuf, v->lft, ";\n\t\t");
2839 if (jj) /* check for double entries q?x,x */
2842 for (v = now->rgt; v; v = v->rgt)
2843 { if (v->lft->ntyp != CONST
2844 && v->lft->ntyp != EVAL
2846 && v->lft->sym->type != STRUCT /* not a struct */
2847 && (v->lft->sym->nel == 1 && v->lft->sym->isarray == 0) /* not array */
2848 && strcmp(v->lft->sym->name, "_") != 0)
2849 for (w = v->rgt; w; w = w->rgt)
2850 if (v->lft->sym == w->lft->sym)
2851 { fatal("cannot use var ('%s') in multiple msg fields",
2855 /* set */ for (v = now->rgt, i = 0; v; v = v->rgt, i++)
2856 { if ((v->lft->ntyp == CONST
2857 || v->lft->ntyp == EVAL) && v->rgt)
2859 fprintf(fd, ";\n\t\t");
2861 if (v->lft->ntyp != CONST
2862 && v->lft->ntyp != EVAL
2863 && v->lft->sym != NULL
2864 && strcmp(v->lft->sym->name, "_") != 0)
2867 putstmnt(fd, v->lft, m);
2872 putname(fd, "qrecv(", now->lft, m, ", ");
2873 fprintf(fd, "XX-1, %d, ", i);
2874 fprintf(fd, "%d)", (v->rgt || now->val >= 2)?0:1);
2876 if (v->lft->ntyp != CONST
2877 && v->lft->ntyp != EVAL
2878 && v->lft->sym != NULL
2879 && strcmp(v->lft->sym->name, "_") != 0
2880 && (v->lft->ntyp != NAME
2881 || v->lft->sym->type != CHAN))
2882 { fprintf(fd, ";\n#ifdef VAR_RANGES");
2883 fprintf(fd, "\n\t\tlogval(\"");
2884 withprocname = terse = nocast = 1;
2886 putstmnt(fd,v->lft,m);
2887 withprocname = terse = nocast = 0;
2888 fprintf(fd, "\", ");
2889 putstmnt(fd,v->lft,m);
2891 fprintf(fd, ");\n#endif\n");
2892 fprintf(fd, "\t\t");
2895 fprintf(fd, ";\n\t\t");
2897 fprintf(fd, "\n#ifdef HAS_CODE\n");
2898 fprintf(fd, "\t\tif (readtrail && gui) {\n");
2899 fprintf(fd, "\t\t\tchar simtmp[32];\n");
2900 putname(fd, "\t\t\tsprintf(simvals, \"%%d?\", ", now->lft, m, ");\n");
2902 for (v = now->rgt, i = 0; v; v = v->rgt, i++)
2903 { if (v->lft->ntyp != EVAL)
2904 { cat3("\t\tsprintf(simtmp, \"%%d\", ", v->lft, "); strcat(simvals, simtmp);");
2906 { cat3("\t\tsprintf(simtmp, \"%%d\", ", v->lft->lft, "); strcat(simvals, simtmp);");
2909 fprintf(fd, "\t\tstrcat(simvals, \",\");\n");
2912 fprintf(fd, "\t\t}\n");
2913 fprintf(fd, "#endif\n\t\t");
2916 { putname(fd, "if (q_zero(", now->lft, m, "))");
2917 fprintf(fd, "\n\t\t{ boq = -1;\n");
2919 fprintf(fd, "#ifndef NOFAIR\n"); /* NEW 3.0.8 */
2920 fprintf(fd, "\t\t\tif (fairness\n");
2921 fprintf(fd, "\t\t\t&& !(trpt->o_pm&32)\n");
2922 fprintf(fd, "\t\t\t&& (now._a_t&2)\n");
2923 fprintf(fd, "\t\t\t&& now._cnt[now._a_t&1] == II+2)\n");
2924 fprintf(fd, "\t\t\t{ now._cnt[now._a_t&1] -= 1;\n");
2925 fprintf(fd, "#ifdef VERI\n");
2926 fprintf(fd, "\t\t\t if (II == 1)\n");
2927 fprintf(fd, "\t\t\t now._cnt[now._a_t&1] = 1;\n");
2928 fprintf(fd, "#endif\n");
2929 fprintf(fd, "#ifdef DEBUG\n");
2930 fprintf(fd, "\t\t\tprintf(\"%%3d: proc %%d fairness \", depth, II);\n");
2931 fprintf(fd, "\t\t\tprintf(\"Rule 2: --cnt to %%d (%%d)\\n\",\n");
2932 fprintf(fd, "\t\t\t now._cnt[now._a_t&1], now._a_t);\n");
2933 fprintf(fd, "#endif\n");
2934 fprintf(fd, "\t\t\t trpt->o_pm |= (32|64);\n");
2935 fprintf(fd, "\t\t\t}\n");
2936 fprintf(fd, "#endif\n");
2938 fprintf(fd, "\n\t\t}");
2943 if (!terse && !TestOnly && has_xu)
2944 { fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
2945 putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
2946 fprintf(fd, "q_R_check(");
2947 putname(fd, "", now->lft, m, ", II)) &&\n\t\t");
2948 putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
2949 putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
2950 fprintf(fd, "\n#endif\n\t\t");
2953 putname(fd, "not_RV(", now->lft, m, ") && \\\n\t\t");
2955 for (v = now->rgt, i=j=0; v; v = v->rgt, i++)
2956 if (v->lft->ntyp != CONST
2957 && v->lft->ntyp != EVAL)
2960 if (now->val == 0 || i == j)
2961 { putname(fd, "(q_len(", now->lft, m, ") > 0");
2962 for (v = now->rgt, i=0; v; v = v->rgt, i++)
2963 { if (v->lft->ntyp != CONST
2964 && v->lft->ntyp != EVAL)
2966 fprintf(fd, " \\\n\t\t&& qrecv(");
2967 putname(fd, "", now->lft, m, ", ");
2968 fprintf(fd, "0, %d, 0) == ", i);
2969 if (v->lft->ntyp == CONST)
2970 putstmnt(fd, v->lft, m);
2972 putstmnt(fd, v->lft->lft, m);
2976 { putname(fd, "Q_has(", now->lft, m, "");
2977 for (v = now->rgt, i=0; v; v = v->rgt, i++)
2978 { if (v->lft->ntyp == CONST)
2979 { fprintf(fd, ", 1, ");
2980 putstmnt(fd, v->lft, m);
2981 } else if (v->lft->ntyp == EVAL)
2982 { fprintf(fd, ", 1, ");
2983 putstmnt(fd, v->lft->lft, m);
2985 fprintf(fd, ", 0, 0");
2987 for ( ; i < Mpars; i++)
2988 fprintf(fd, ", 0, 0");
2994 preruse(fd, now->lft); /* preconditions */
2995 cat3("if (!(", now->lft, "))\n\t\t\t");
3001 { if (separate == 2)
3002 fprintf(fd, "if (o_pm&1)\n\t\t\t");
3004 fprintf(fd, "if (trpt->o_pm&1)\n\t\t\t");
3007 { fprintf(fd, "/* else */");
3013 { cat3("( (", now->lft, ") ? ");
3016 { cat3("(", now->rgt->lft, ") : ");
3017 cat3("(", now->rgt->rgt, ") )");
3022 if (check_track(now) == STRUCT) { break; }
3024 if (has_enabled || has_priority)
3025 fprintf(fd, "if (TstOnly) return 1; /* T3 */\n\t\t");
3032 sprintf(tempbuf, "(trpt+1)->bup.ovals[%d] = ",
3035 cat30(tempbuf, now->lft, ";\n\t\t");
3037 { cat3("(trpt+1)->bup.oval = ", now->lft, ";\n\t\t");
3040 && now->lft->sym->type == PREDEF
3041 && strcmp(now->lft->sym->name, "_") != 0
3042 && strcmp(now->lft->sym->name, "_priority") != 0)
3043 { fatal("invalid assignment to %s", now->lft->sym->name);
3046 nocast = 1; putstmnt(fd,now->lft,m); nocast = 0;
3049 if (now->lft->sym->isarray
3050 && now->rgt->ntyp == ',') /* array initializer */
3051 { putstmnt(fd, now->rgt->lft, m);
3052 non_fatal("cannot use an array list initializer here", (char *) 0);
3054 { putstmnt(fd, now->rgt, m);
3057 if (now->sym->type != CHAN
3059 { fprintf(fd, ";\n#ifdef VAR_RANGES");
3060 fprintf(fd, "\n\t\tlogval(\"");
3061 withprocname = terse = nocast = 1;
3063 putstmnt(fd,now->lft,m);
3064 withprocname = terse = nocast = 0;
3065 fprintf(fd, "\", ");
3066 putstmnt(fd,now->lft,m);
3068 fprintf(fd, ");\n#endif\n");
3069 fprintf(fd, "\t\t");
3074 if (has_enabled || has_priority)
3075 fprintf(fd, "if (TstOnly) return 1; /* T4 */\n\t\t");
3077 fprintf(fd, "printf(%s", now->sym->name);
3079 fprintf(fd, "Printf(%s", now->sym->name);
3081 for (v = now->lft; v; v = v->rgt)
3082 { cat2(", ", v->lft);
3088 if (has_enabled || has_priority)
3089 fprintf(fd, "if (TstOnly) return 1; /* T5 */\n\t\t");
3090 fprintf(fd, "printm(");
3091 if (now->lft && now->lft->ismtyp)
3092 fprintf(fd, "%d", now->lft->val);
3094 putstmnt(fd, now->lft, m);
3099 if (!nocast && now->sym && Sym_typ(now) < SHORT)
3100 putname(fd, "((int)", now, m, ")");
3102 putname(fd, "", now, m, "");
3106 putremote(fd, now, m);
3111 fprintf(fd, "%s", now->sym?now->sym->name:"?");
3113 fprintf(fd, "%d", remotelab(now));
3118 plunk_expr(fd, now->sym->name);
3122 fprintf(fd, ") /* %s */ ", now->sym->name);
3128 fprintf(fd, "/* %s */\n\t\t", now->sym->name);
3129 if (has_enabled || has_priority)
3130 fprintf(fd, "if (TstOnly) return 1; /* T6 */\n\t\t");
3133 plunk_inline(fd, now->sym->name, 1, GenCode);
3135 fatal("internal error pangen2.c", (char *) 0);
3138 { fprintf(fd, "\n"); /* state changed, capture it */
3139 fprintf(fd, "#if defined(C_States) && (HAS_TRACK==1)\n");
3140 fprintf(fd, "\t\tc_update((uchar *) &(now.c_state[0]));\n");
3141 fprintf(fd, "#endif\n");
3146 if (has_enabled || has_priority)
3147 fprintf(fd, "if (TstOnly) return 1; /* T7 */\n\t\t");
3149 cat3("spin_assert(", now->lft, ", ");
3151 cat3("\"", now->lft, "\", II, tt, t)");
3158 if (Pid == eventmapnr)
3159 fprintf(fd, "Uerror(\"cannot get here\")");
3164 if (Pid == eventmapnr)
3165 { fprintf(fd, "return 0");
3169 if (has_enabled || has_priority)
3170 { fprintf(fd, "if (TstOnly)\n\t\t\t");
3171 fprintf(fd, "return (II+1 == now._nr_pr);\n\t\t");
3173 fprintf(fd, "if (!delproc(1, II)) ");
3178 printf("spin: error, %s:%d, bad node type %d (.m)\n",
3179 now->fn->name, now->ln, now->ntyp);
3186 simplify_name(char *s)
3189 if (!old_scope_rules)
3190 { while (*t == '_' || isdigit((int)*t))
3198 putname(FILE *fd, char *pre, Lextok *n, int m, char *suff) /* varref */
3199 { Symbol *s = n->sym;
3202 lineno = n->ln; Fname = n->fn;
3205 fatal("no name - putname", (char *) 0);
3207 if (s->context && context && s->type)
3208 s = findloc(s); /* it's a local var */
3211 { fprintf(fd, "%s%s%s", pre, n->sym->name, suff);
3215 if (!s->type) /* not a local name */
3216 s = lookup(s->name); /* must be a global */
3219 { if (strcmp(pre, ".") != 0)
3220 fatal("undeclared variable '%s'", s->name);
3224 if (s->type == PROCTYPE)
3225 fatal("proctype-name '%s' used as array-name", s->name);
3227 fprintf(fd, pre, 0);
3228 if (!terse && !s->owner && evalindex != 1)
3229 { if (old_priority_rules
3230 && strcmp(s->name, "_priority") == 0)
3235 || strcmp(s->name, "_p") == 0
3236 || strcmp(s->name, "_pid") == 0
3237 || strcmp(s->name, "_priority") == 0)
3238 { fprintf(fd, "((P%d *)this)->", Pid);
3240 { int x = strcmp(s->name, "_");
3241 if (!(s->hidden&1) && x != 0)
3242 fprintf(fd, "now.");
3243 if (x == 0 && _isok == 0)
3244 fatal("attempt to read value of '_'", 0);
3247 if (terse && buzzed == 1)
3248 { fprintf(fd, "B_state.%s", (s->context)?"local[B_pid].":"");
3253 if (!dont_simplify /* new 6.4.3 */
3254 && s->type != PREDEF) /* new 6.0.2 */
3257 && strcmp(pre, "."))
3258 { fprintf(fd, "%s:", s->context->name);
3259 ptr = simplify_name(ptr);
3262 { ptr = simplify_name(ptr);
3266 fprintf(fd, "%s", ptr);
3268 if (s->nel > 1 || s->isarray == 1)
3270 { non_fatal("ref to array element invalid in this context",
3272 printf("\thint: instead of, e.g., x[rs] qu[3], use\n");
3273 printf("\tchan nm_3 = qu[3]; x[rs] nm_3;\n");
3274 printf("\tand use nm_3 in sends/recvs instead of qu[3]\n");
3276 /* an xr or xs reference to an array element
3277 * becomes an exclusion tag on the array itself -
3278 * which could result in invalidly labeling
3279 * operations on other elements of this array to
3280 * be also safe under the partial order reduction
3281 * (see procedure has_global())
3285 { fprintf(fd, "[%%d]");
3286 } else if (evalindex == 1)
3287 { evalindex = 0; /* no good if index is indexed array */
3289 putstmnt(fd, n->lft, m);
3294 && n->lft->ntyp == CONST
3295 && n->lft->val < s->nel)
3296 || (!n->lft && s->nel > 0))
3297 { cat3("[", n->lft, "]");
3299 { /* attempt to catch arrays that are indexed with an array element in the same array
3300 * this causes trouble in the verifier in the backtracking
3301 * e.g., restoring a[?] in the assignment: a [a[1]] = x where a[1] == 1
3302 * but it is hard when the array is inside a structure, so the names dont match
3305 if (n->lft->ntyp == NAME)
3306 { printf("%4d: Basename %s index %s\n",
3307 n->lft->ln, s->name, n->lft->sym->name);
3310 cat3("[ Index(", n->lft, ", ");
3311 fprintf(fd, "%d) ]", s->nel);
3314 { if (n->lft /* effectively a scalar, but with an index */
3315 && (n->lft->ntyp != CONST
3316 || n->lft->val != 0))
3317 { fatal("ref to scalar '%s' using array index", (char *) ptr);
3320 if (s->type == STRUCT && n->rgt && n->rgt->lft)
3321 { putname(fd, ".", n->rgt->lft, m, "");
3324 fprintf(fd, suff, 0);
3328 putremote(FILE *fd, Lextok *n, int m) /* remote reference */
3333 { fprintf(fd, "%s", n->lft->sym->name); /* proctype name */
3336 putstmnt(fd, n->lft->lft, m); /* pid */
3340 { fprintf(fd, ":%s", n->sym->name);
3342 { fprintf(fd, ".%s", n->sym->name);
3345 { if (Sym_typ(n) < SHORT)
3347 fprintf(fd, "((int)");
3350 pt = fproc(n->lft->sym->name);
3351 fprintf(fd, "((P%d *)Pptr(", pt);
3353 { fprintf(fd, "BASE+");
3354 putstmnt(fd, n->lft->lft, m);
3356 fprintf(fd, "f_pid(%d)", pt);
3357 fprintf(fd, "))->%s", n->sym->name);
3361 putstmnt(fd, n->rgt, m); /* array var ref */
3364 if (promoted) fprintf(fd, ")");
3368 getweight(Lextok *n)
3369 { /* this piece of code is a remnant of early versions
3370 * of the verifier -- in the current version of Spin
3371 * only non-zero values matter - so this could probably
3372 * simply return 1 in all cases.
3377 case TIMEOUT: return 1;
3378 case 'c': if (has_typ(n->lft, TIMEOUT)) return 1;
3384 has_typ(Lextok *n, int m)
3387 if (n->ntyp == m) return 1;
3388 return (has_typ(n->lft, m) || has_typ(n->rgt, m));
3391 static int runcount, opcount;
3394 do_count(Lextok *n, int checkop)
3403 if (checkop) opcount++;
3406 do_count(n->lft, checkop && (n->ntyp != RUN));
3407 do_count(n->rgt, checkop);
3411 count_runs(Lextok *n)
3413 runcount = opcount = 0;
3416 fatal("more than one run operator in expression", "");
3417 if (runcount == 1 && opcount > 1)
3418 fatal("use of run operator in compound expression", "");
3424 runcount = opcount = 0;
3427 fatal("run operator used in invalid context", "");