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