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