1 /***** spin: pangen2.c *****/
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 */
20 #define DELTA 500 /* sets an upperbound on nr of chan names */
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); }
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
[];
39 FILE *tc
, *th
, *tt
, *tb
;
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 */
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 */
64 #define MAXMERGE 256 /* max nr of bups per merge sequence */
66 static short CnT
[MAXMERGE
];
67 static Lextok XZ
, YZ
[MAXMERGE
];
68 static int didcase
, YZmax
, YZcnt
;
71 static int Det
; /* set if deterministic */
72 static int T_sum
, T_mus
, t_cyc
;
73 static int TPE
[2], EPT
[2];
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 _ */
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*);
96 for (p
= rdy
; p
; p
= p
->nxt
)
97 if (strcmp(p
->n
->name
, s
) == 0)
100 fatal("proctype %s not found", s
);
105 reverse_procs(RunList
*q
)
108 reverse_procs(q
->nxt
);
109 fprintf(tc
, " Addproc(%d);\n", q
->tn
);
113 forward_procs(RunList
*q
)
116 fprintf(tc
, " Addproc(%d);\n", q
->tn
);
117 forward_procs(q
->nxt
);
123 fprintf(th
, "#define _T5 %d\n", uniq
++);
124 fprintf(th
, "#define _T2 %d\n", uniq
++);
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");
131 { fprintf(th
, "#define T_ID unsigned int\n");
134 fprintf(tm
, "\tcase _T5:\t/* np_ */\n");
137 fprintf(tm
, "\t\tif (!((!(o_pm&4) && !(tau&128))))\n");
139 fprintf(tm
, "\t\tif (!((!(trpt->o_pm&4) && !(trpt->tau&128))))\n");
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");
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");
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" } }
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");
184 fprintf(th
, "#define SpinVersion \"%s\"\n", SpinVersion
);
185 fprintf(th
, "#define PanSource \"%s\"\n\n", oFname
->name
);
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");
195 { fprintf(th
, "char *TrailFile = PanSource; /* default */\n");
196 fprintf(th
, "char *trailfilename;\n");
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");
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");
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");
221 if (sizeof(long)==sizeof(int))
222 fprintf(th
, "#define long int\n");
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
);
232 { printf("spin: warning, make sure that the S1 model\n");
233 printf(" includes the same remote references\n");
235 fprintf(th
, "#ifndef NFAIR\n");
236 fprintf(th
, "#define NFAIR 2 /* must be >= 2 */\n");
237 fprintf(th
, "#endif\n");
239 fprintf(th
, "#define HAS_LAST %d\n", has_last
);
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");
259 fprintf(th
, "#define NTIM %d\n", Ntimeouts
);
261 fprintf(th
, "#define ETIM %d\n", Etimeouts
);
263 fprintf(th
, "#define REM_VARS 1\n");
265 fprintf(th
, "#define REM_REFS %d\n", has_remote
); /* not yet used */
267 fprintf(th
, "#define HAS_HIDDEN %d\n", has_hidden
);
269 fprintf(th
, "#define HAS_LAST %d\n", has_last
);
271 fprintf(th
, "#define HAS_SORTED %d\n", has_sorted
);
273 fprintf(th
, "#define M_LOSS\n");
275 fprintf(th
, "#define HAS_RANDOM %d\n", has_random
);
276 fprintf(th
, "#define HAS_CODE\n"); /* doesn't seem to cause measurable overhead */
278 fprintf(th
, "#define HAS_STACK %d\n", has_stack
);
280 fprintf(th
, "#define HAS_ENABLED 1\n");
282 fprintf(th
, "#define HAS_UNLESS %d\n", has_unless
);
284 fprintf(th
, "#define HAS_PROVIDED %d\n", has_provided
);
286 fprintf(th
, "#define HAS_PCVALUE %d\n", has_pcvalue
);
288 fprintf(th
, "#define HAS_BADELSE %d\n", has_badelse
);
293 { fprintf(th
, "#ifndef NOREDUCE\n");
294 fprintf(th
, "#define NOREDUCE 1\n");
295 fprintf(th
, "#endif\n");
298 fprintf(th
, "#define HAS_NP %d\n", has_np
);
300 fprintf(th
, "#define MERGED 1\n");
303 fprintf(th
, "#ifdef NP /* includes np_ demon */\n");
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");
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");
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");
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");
329 fprintf(tc
, "/*** Generated by %s ***/\n", SpinVersion
);
330 fprintf(tc
, "/*** From source: %s ***/\n\n", oFname
->name
);
332 ntimes(tc
, 0, 1, Pre0
);
334 plunk_c_decls(tc
); /* types can be refered to in State */
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;
342 fprintf(tc
, "#ifdef LOOPSTATE\n");
343 fprintf(tc
, "double cnt_loops;\n");
344 fprintf(tc
, "#endif\n");
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 */
351 ntimes(tc
, 0, 1, Preamble
);
353 fprintf(tc
, "extern int verbose; extern long depth;\n");
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");
361 c_preview(); /* sets hastrack */
363 for (p
= rdy
; p
; p
= p
->nxt
)
364 mst
= max(p
->s
->maxel
, mst
);
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");
381 { fprintf(tt
, "#else\n");
382 fprintf(tt
, "#define tr_2_src(m,f,l)\n");
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 */
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");
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");
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");
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");
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");
426 fprintf(tm
, " IfNotBlocked\n");
427 fprintf(tm
, " _m = 3; goto P999;\n");
428 fprintf(tm
, " case 2: /* generic 'else' */\n");
430 fprintf(tm
, " if (o_pm&1) continue;\n");
432 { fprintf(tm
, " IfNotBlocked\n");
433 fprintf(tm
, " if (trpt->o_pm&1) continue;\n");
435 fprintf(tm
, " _m = 3; goto P999;\n");
439 fprintf(tb
, " if (II == 0) goto R999;\n");
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");
445 for (p
= rdy
; p
; p
= p
->nxt
)
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",
456 fprintf(th
, " { 0, (short *) 0 }\n");
458 fprintf(th
, "short *frm_st0;\n"); /* records src states for transitions in never claim */
460 { fprintf(th
, "extern short *frm_st0;\n");
469 fprintf(tt
, "}\n\n"); /* end of settable() */
471 fprintf(tm
, "#undef rand\n");
472 fprintf(tm
, " }\n\n");
473 fprintf(tb
, " }\n\n");
476 { ntimes(tt
, 0, 1, Tail
);
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");
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");
495 if (!run
) fatal("no runable process", (char *)0);
496 fprintf(tc
, "void\n");
497 fprintf(tc
, "active_procs(void)\n{\n");
499 fprintf(tc
, " if (!permuted) {\n");
501 fprintf(tc
, " } else {\n");
508 ntimes(tc
, 0, 1, Dfa
);
509 ntimes(tc
, 0, 1, Xpt
);
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");
516 if (u_sync
&& !u_async
)
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");
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");
545 fprintf(tc
, "\n\tswitch (n) {\n");
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");
560 ntimes(tc
, 0, 1, Nvr1
);
573 for (p
= rdy
; p
; p
= p
->nxt
)
580 dolen(Symbol
*s
, char *pre
, int pid
, int ai
, int qln
)
583 fprintf(tc
, "\n\t\t\t || ");
584 fprintf(tc
, "%s(", pre
);
587 fprintf(tc
, "((P%d *)this)->", pid
);
591 fprintf(tc
, "%s", s
->name
);
592 if (qln
> 1) fprintf(tc
, "[%d]", ai
);
596 struct AA
{ char TT
[9]; char CC
[8]; };
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" }
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" }
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
622 bb_or_dd(int j
, int which
)
626 fprintf(tc
, "%s", DD
[j
].CC
);
628 fprintf(tc
, "%s", BB
[j
].CC
);
631 fprintf(tc
, "%s", DD
[j
].TT
);
633 fprintf(tc
, "%s", BB
[j
].TT
);
638 Done_case(char *nm
, Symbol
*z
)
643 fprintf(tc
, "\t\tcase %d: if (", nid
);
644 for (j
= 0; j
< 4; j
++)
645 { fprintf(tc
, "\t(t->ty[i] == ");
647 fprintf(tc
, " && (");
648 for (k
= 0; k
< qln
; k
++)
650 fprintf(tc
, "\n\t\t\t || ");
652 fprintf(tc
, "(%s%s", nm
, z
->name
);
654 fprintf(tc
, "[%d]", k
);
657 fprintf(tc
, "))\n\t\t\t ");
663 fprintf(tc
, ") return 0; break;\n");
667 Docase(Symbol
*s
, int pid
, int nid
)
670 fprintf(tc
, "\t\tcase %d: if (", nid
);
671 for (j
= 0; j
< 4; j
++)
672 { fprintf(tc
, "\t(t->ty[i] == ");
674 fprintf(tc
, " && (");
676 { for (i
= 0; i
< s
->nel
; i
++)
677 dolen(s
, DD
[j
].CC
, pid
, i
, s
->nel
);
679 { for (i
= 0; i
< s
->nel
; i
++)
680 dolen(s
, BB
[j
].CC
, pid
, i
, s
->nel
);
682 fprintf(tc
, "))\n\t\t\t ");
688 fprintf(tc
, ") return 0; break;\n");
692 genconditionals(void)
695 extern Ordered
*all_names
;
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");
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");
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)
729 fprintf(tc
, " switch (t->qu[i]) {\n");
730 fprintf(tc
, " case 0: break;\n");
732 for (walk
= all_names
; walk
; walk
= walk
->next
)
734 if (s
->owner
) continue;
735 j
= find_id(s
->context
);
737 { if (last
== s
->Nid
) continue; /* chan array */
740 } else if (s
->type
== STRUCT
)
741 { /* struct may contain a chan */
743 extern void walk2_struct(char *, Symbol
*);
747 sprintf(pregat
, "((P%d *)this)->",j
);
749 sprintf(pregat
, "now.");
751 walk2_struct(pregat
, s
);
754 fprintf(tc
, " \tdefault: Uerror(\"unknown qid - q_cond\");\n");
755 fprintf(tc
, " \t\t\treturn 0;\n");
756 fprintf(tc
, " \t}\n");
758 fprintf(tc
, " return 1;\n");
769 { fprintf(th
, "extern uchar reached%d[];\n", Pid
);
771 fprintf(th
, "extern short nstates%d;\n", Pid
);
773 fprintf(th
, "\n#define nstates%d %d\t/* %s */\n",
774 Pid
, p
->s
->maxel
, p
->n
->name
);
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
);
787 { fprintf(th
, "extern short src_ln%d[];\n", Pid
);
788 fprintf(th
, "extern uchar *loopstate%d;\n", Pid
);
792 AllGlobal
= (p
->prov
)?1:0; /* process has provided clause */
794 fprintf(th
, "\n#define nstates%d %d\t/* %s */\n",
795 Pid
, p
->s
->maxel
, p
->n
->name
);
797 fprintf(th
, "#define nstates_claim nstates%d\n", Pid
);
798 if (Pid
== eventmapnr
)
799 fprintf(th
, "#define nstates_event nstates%d\n", Pid
);
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
);
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");
815 if (Pid
== eventmapnr
)
816 { fprintf(th
, "\n\n");
819 dumpsrc(p
->s
->maxel
, Pid
);
828 for (i
= 0; i
< T_sum
; i
++)
831 TPE
[(T_sum
++)%2] = x
;
840 for (f
= s
->frst
; f
; f
= f
->nxt
)
841 { Tpe(f
->n
); /* sets EPT */
844 for (h
= f
->sub
; h
; h
= h
->nxt
)
855 TPE
[0] = 2; TPE
[1] = 0;
857 if (T_sum
> 2) /* more than one type */
858 { TPE
[0] = 5*DELTA
; /* non-mixing */
868 case FULL
: case EMPTY
:
869 case NFULL
: case NEMPTY
: case TIMEOUT
:
872 case '!': case UMIN
: case '~': case ASSERT
: case 'c':
873 (void) hidden(n
->lft
);
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
);
890 && n
->sym
->type
== STRUCT
891 && n
->rgt
&& n
->rgt
->lft
)
892 return getNid(n
->rgt
->lft
);
894 if (!n
->sym
|| n
->sym
->Nid
== 0)
895 { fatal("bad channel name '%s'",
896 (n
->sym
)?n
->sym
->name
:"no name");
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)
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 */
918 case NEMPTY
: res
+= DELTA
; /* add 1*DELTA + chan nr */
920 case NFULL
: res
+= getNid(n
->lft
); /* add channel nr */
923 case TIMEOUT
: res
= 6*DELTA
; break;
924 case '@': res
= 7*DELTA
; break;
931 Tpe(Lextok
*n
) /* mixing in selections */
933 EPT
[0] = 2; EPT
[1] = 0;
941 { if (hidden(n
->lft
) > 2)
942 { EPT
[0] = 5*DELTA
; /* non-mixing */
949 if (Nn
[0]) EPT
[0] = valTpe(Nn
[0]);
950 if (Nn
[1]) EPT
[1] = valTpe(Nn
[1]);
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",
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?? */
971 fprintf(tt
, " /* end-escapes */\n");
976 put_sub(Element
*e
, int Tt0
, int Tt1
)
977 { Sequence
*s
= e
->n
->sl
->this;
982 putskip(s
->frst
->seqno
);
983 g
= huntstart(s
->frst
);
986 if (0) printf("put_sub %d -> %d -> %d\n", e
->seqno
, s
->frst
->seqno
, a
);
988 if ((e
->n
->ntyp
== ATOMIC
989 || e
->n
->ntyp
== D_STEP
)
992 s
->last
->nxt
= e
->nxt
;
994 typ_seq(s
); /* sets TPE */
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");
1004 if (s
->last
->n
->ntyp
== BREAK
)
1005 OkBreak
= target(huntele(s
->last
->nxt
,
1006 s
->last
->status
, -1))->Seqno
;
1010 if (!putcode(tm
, s
, e
->nxt
, 0, e
->n
->ln
, e
->seqno
))
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");
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");
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");
1027 a
= huntele(e
->nxt
, e
->status
, -1)->seqno
;
1031 fprintf(tt
, "/*->*/\ttrans[%d][%d]\t= ",
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]);
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
);
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
);
1059 put_seq(s
, Tt0
, Tt1
);
1061 { fprintf(tt
, "%d, %d);", TPE
[0], TPE
[1]);
1063 put_seq(s
, TPE
[0], TPE
[1]);
1068 typedef struct CaseCache
{
1073 struct CaseCache
*nxt
;
1076 static CaseCache
*casing
[6];
1079 identical(Lextok
*p
, Lextok
*q
)
1081 if ((!p
&& q
) || (p
&& !q
))
1086 if (p
->ntyp
!= q
->ntyp
1087 || p
->ismtyp
!= q
->ismtyp
1089 || p
->indstep
!= q
->indstep
1095 return identical(p
->lft
, q
->lft
)
1096 && identical(p
->rgt
, q
->rgt
);
1100 samedeads(FSM_use
*a
, FSM_use
*b
)
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
)
1111 findnext(Element
*f
)
1114 if (f
->n
->ntyp
== GOTO
)
1115 { g
= get_lab(f
->n
, 1);
1116 return huntele(g
, f
->status
, -1);
1122 advance(Element
*e
, int stopat
)
1126 while (f
&& f
->seqno
!= stopat
)
1131 switch (f
->n
->ntyp
) {
1140 return (Element
*) 0;
1144 equiv_merges(Element
*a
, Element
*b
)
1146 int stopat_a
, stopat_b
;
1149 stopat_a
= a
->merge_start
;
1151 stopat_a
= a
->merge
;
1154 stopat_b
= b
->merge_start
;
1156 stopat_b
= b
->merge
;
1158 if (!stopat_a
&& !stopat_b
)
1163 f
= advance(a
, stopat_a
);
1164 g
= advance(b
, stopat_b
);
1168 return identical(f
->n
, g
->n
);
1172 return 1; /* not reached */
1176 prev_case(Element
*e
, int owner
)
1177 { int j
; CaseCache
*nc
;
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;
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
)
1194 return (CaseCache
*) 0;
1198 new_case(Element
*e
, int m
, int b
, int owner
)
1199 { int j
; CaseCache
*nc
;
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;
1209 nc
= (CaseCache
*) emalloc(sizeof(CaseCache
));
1216 nc
->nxt
= casing
[j
];
1226 switch (e
->n
->ntyp
) {
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
))
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)
1252 case 1: /* dead after read */
1261 { Element
*f
= e
, *g
;
1266 stopat
= e
->merge_start
;
1270 printf("merge: %d merge_start %d - seqno %d\n",
1271 e
->merge
, e
->merge_start
, e
->seqno
);
1276 if (f
->n
->ntyp
== GOTO
)
1277 { g
= get_lab(f
->n
, 1);
1278 if (g
->seqno
== stopat
)
1281 f
= huntele(g
, f
->status
, stopat
);
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
);
1295 } while (f
&& f
->seqno
!= stopat
);
1304 { fprintf(tm
, "(trpt+1)->bup.ovals = grab_ints(%d);\n\t\t",
1306 multi_undo
= multi_needed
;
1312 doforward(FILE *tm_fd
, Element
*e
)
1315 putstmnt(tm_fd
, e
->n
, e
->seqno
);
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\")");
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
);
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 */
1333 if (e
->n
->ntyp
!= 'r')
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");
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 */
1346 fprintf(tm_fd
, "(trpt+1)->bup.ovals[%d] = ",
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");
1359 fprintf(tm_fd
, ";\n\t\t");
1363 dobackward(Element
*e
, int casenr
)
1365 if (!any_undo(e
->n
) && CnT
[YZcnt
] == 0)
1371 { fprintf(tb
, "\n\tcase %d: ", casenr
);
1372 fprintf(tb
, "/* STATE %d */\n\t\t", e
->seqno
);
1377 while (CnT
[YZcnt
] > 0) /* undo dead variable resets */
1381 fatal("cannot happen, dobackward", (char *)0);
1382 fprintf(tb
, ";\n\t/* %d */\t", YZmax
);
1383 putname(tb
, "", &YZ
[YZmax
], 0, " = trpt->bup.oval");
1386 fprintf(tb
, "s[%d]", multi_oval
-1);
1390 if (e
->n
->ntyp
!= '.')
1391 { fprintf(tb
, ";\n\t\t");
1392 undostmnt(e
->n
, e
->seqno
);
1401 lastfirst(int stopat
, Element
*fin
, int casenr
)
1402 { Element
*f
= fin
, *g
;
1404 if (f
->n
->ntyp
== GOTO
)
1405 { g
= get_lab(f
->n
, 1);
1406 if (g
->seqno
== stopat
)
1409 f
= huntele(g
, f
->status
, stopat
);
1413 if (!f
|| f
->seqno
== stopat
1414 || (!f
->merge
&& !f
->merge_single
))
1416 lastfirst(stopat
, f
, casenr
);
1418 fprintf(tb
, "\n\t/* merge %d -- %d:%d %d:%d:%d (casenr %d) ",
1420 f
->merge_start
, f
->merge
,
1421 f
->seqno
, f
?f
->seqno
:-1, stopat
,
1423 comment(tb
, f
->n
, 0);
1424 fprintf(tb
, " */\n");
1427 dobackward(f
, casenr
);
1430 static int modifier
;
1433 lab_transfer(Element
*to
, Element
*from
)
1434 { Symbol
*ns
, *s
= has_lab(from
, (1|2|4));
1440 /* "from" could have all three labels -- rename
1441 * to prevent jumps to the transfered copies
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
);
1450 context
= s
->context
;
1454 context
= oc
; /* restore */
1456 { if (modifier
++ > 990)
1457 fatal("modifier overflow error", (char *) 0);
1462 case_cache(Element
*e
, int a
)
1463 { int bupcase
= 0, casenr
= uniq
, fromcache
= 0;
1464 CaseCache
*Cached
= (CaseCache
*) 0;
1466 int j
, nrbups
, mark
, ntarget
;
1469 mark
= (e
->status
&ATOM
); /* could lose atomicity in a merge chain */
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");
1481 { fprintf(tt
, "\ttrans[%d][%d]\t= ", Pid
, e
->seqno
);
1482 casenr
= 1; /* mhs example */
1484 goto haveit
; /* pakula's example */
1490 fprintf(tt
, "\ttrans[%d][%d]\t= ", Pid
, e
->seqno
);
1494 && Pid
!= eventmapnr
1495 && (Cached
= prev_case(e
, Pid
)))
1496 { bupcase
= Cached
->b
;
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
,
1506 Cached
->e
->merge_start
, Cached
->e
->merge
, Cached
->e
->merge_in
);
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
);
1518 if (nrbups
> MAXMERGE
-1)
1519 fatal("merge requires more than 256 bups", (char *)0);
1521 if (e
->n
->ntyp
!= 'r' && Pid
!= claimnr
&& Pid
!= eventmapnr
)
1522 fprintf(tm
, "IfNotBlocked\n\t\t");
1524 if (multi_needed
!= 0 || multi_undo
!= 0)
1525 fatal("cannot happen, case_cache", (char *) 0);
1529 multi_needed
= nrbups
; /* allocated after edge condition */
1533 memset(CnT
, 0, sizeof(CnT
));
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");
1552 /* the src xrefs have the numbers in e->seqno builtin */
1553 fprintf(tm
, "reached[%d][%d] = 1;\n\t\t", Pid
, e
->seqno
);
1558 ntarget
= e
->merge_start
;
1565 more
: if (f
->n
->ntyp
== GOTO
)
1566 { g
= get_lab(f
->n
, 1);
1567 if (g
->seqno
== ntarget
)
1570 f
= huntele(g
, f
->status
, ntarget
);
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",
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
);
1587 mark
= f
->status
&(ATOM
|L_ATOM
); /* last step wins */
1589 if (f
->merge_in
== 1) f
->merge_mark
++;
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
);
1602 lastfirst(ntarget
, e
, casenr
); /* mergesteps only */
1604 dobackward(e
, casenr
); /* the original step */
1606 fprintf(tb
, ";\n\t\t");
1608 if (e
->merge
|| e
->merge_start
)
1610 { fprintf(tb
, "\n\tcase %d: ", casenr
);
1611 fprintf(tb
, "/* STATE %d */", e
->seqno
);
1617 fprintf(tb
, "\n\t\t");
1620 { fprintf(tb
, "ungrab_ints(trpt->bup.ovals, %d);\n\t\t",
1625 { fprintf(tb
, "goto R999;\n");
1629 if (!e
->merge
&& !e
->merge_start
)
1630 new_case(e
, casenr
, bupcase
, Pid
);
1639 fprintf(tt
, "%ssettr(%d,%d,%d,%d,%d,\"", fromcache
?"/* c */ ":"",
1640 e
->Seqno
, mark
, j
, casenr
, bupcase
);
1642 return (fromcache
)?0:casenr
;
1646 put_el(Element
*e
, int Tt0
, int Tt1
)
1647 { int a
, casenr
, Global_ref
;
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
);
1656 { g
= huntele(e
->nxt
, e
->status
, -1);
1661 && (g
->status
&CHECK2
/* entering remotely ref'd state */
1662 || e
->status
&CHECK2
)) /* leaving remotely ref'd state */
1663 e
->status
|= I_GLOB
;
1665 /* don't remove dead edges in here, to preserve structure of fsm */
1666 if (e
->merge_start
|| e
->merge
)
1669 /*** avoid duplicate or redundant cases in pan.m ***/
1670 switch (e
->n
->ntyp
) {
1672 casenr
= 2; /* standard else */
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
);
1692 if (e
->n
->lft
->ntyp
== CONST
1693 && e
->n
->lft
->val
== 1) /* skip or true */
1702 casenr
= case_cache(e
, a
);
1703 if (casenr
< 0) return; /* unreachable state */
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
);
1711 { fprintf(tt
, "%d, %d);", Tt0
, Tt1
);
1713 { Tpe(e
->n
); /* sets EPT */
1714 fprintf(tt
, "%d, %d);", EPT
[0], EPT
[1]);
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 */
1731 nested_unless(Element
*e
, Element
*g
)
1732 { struct SeqList
*y
= e
->esc
, *z
= g
->esc
;
1734 for ( ; y
&& z
; y
= y
->nxt
, z
= z
->nxt
)
1735 if (z
->this != y
->this)
1740 if (g
->n
->ntyp
!= GOTO
1741 && g
->n
->ntyp
!= '.'
1743 { printf("error: (%s:%d) saw 'unless' on a guard:\n",
1744 (e
->n
)?e
->n
->fn
->name
:"-",
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");
1761 put_seq(Sequence
*s
, int Tt0
, int Tt1
)
1766 if (0) printf("put_seq %d\n", s
->frst
->seqno
);
1768 for (e
= s
->frst
; e
; e
= e
->nxt
)
1770 if (0) printf(" step %d\n", e
->seqno
);
1771 if (e
->status
& DONE
)
1773 if (0) printf(" done before\n");
1781 if (e
->n
->ntyp
== UNLESS
)
1783 if (0) printf(" an unless\n");
1784 put_seq(e
->sub
->this, Tt0
, Tt1
);
1787 if (0) printf(" has sub\n");
1788 fprintf(tt
, "\tT = trans[%d][%d] = ",
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
);
1798 for (h
= e
->sub
; h
; h
= h
->nxt
)
1799 { putskip(h
->this->frst
->seqno
);
1800 g
= huntstart(h
->this->frst
);
1802 nested_unless(e
, g
);
1805 if (g
->n
->ntyp
== 'c'
1806 && g
->n
->lft
->ntyp
== CONST
1807 && g
->n
->lft
->val
== 0 /* 0 or false */
1809 { fprintf(tt
, "#if 0\n\t/* dead link: */\n");
1812 printf("spin: line %3d %s, Warning: condition is always false\n",
1813 g
->n
->ln
, g
->n
->fn
?g
->n
->fn
->name
:"");
1816 if (0) printf(" settr %d %d\n", a
, 0);
1818 fprintf(tt
, "\tT = T->nxt\t= ");
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,
1831 fprintf(tt
, "#endif\n");
1833 for (h
= e
->sub
; h
; h
= h
->nxt
)
1834 put_seq(h
->this, Tt0
, Tt1
);
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
);
1844 if (0) printf(" put_el %d\n", e
->seqno
);
1845 put_el(e
, Tt0
, Tt1
);
1848 checklast
: if (e
== s
->last
)
1851 if (0) printf("put_seq done\n");
1855 patch_atomic(Sequence
*s
) /* catch goto's that break the chain */
1859 for (f
= s
->frst
; f
; f
= f
->nxt
)
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
;
1869 /* bridge atomics */
1870 if ((f
->status
& L_ATOM
)
1871 && (g
->status
& (ATOM
|L_ATOM
)))
1872 { f
->status
&= ~L_ATOM
;
1876 for (h
= f
->sub
; h
; h
= h
->nxt
)
1877 patch_atomic(h
->this);
1884 mark_seq(Sequence
*s
)
1888 for (f
= s
->frst
; f
; f
= f
->nxt
)
1889 { f
->status
|= I_GLOB
;
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);
1896 for (h
= f
->sub
; h
; h
= h
->nxt
)
1904 find_target(Element
*e
)
1910 { fatal("cycle of goto jumps", (char *) 0);
1912 switch (e
->n
->ntyp
) {
1914 f
= get_lab(e
->n
,1);
1915 cross_dsteps(e
->n
, f
->n
);
1920 { f
= find_target(huntele(e
->nxt
, e
->status
, -1));
1921 break; /* new 5.0 -- was missing */
1923 /* else fall through */
1938 return find_target(e
);
1942 seq_has_el(Sequence
*s
, Element
*g
) /* new to version 5.0 */
1946 for (f
= s
->frst
; f
; f
= f
->nxt
) /* g in same atomic? */
1950 if (f
->status
& CHECK3
)
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
))
1962 scan_seq(Sequence
*s
)
1966 for (f
= s
->frst
; f
; f
= f
->nxt
)
1967 { if ((f
->status
&CHECK2
)
1968 || has_global(f
->n
))
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
1978 if (g
&& !seq_has_el(s
, g
)) /* not internal to this atomic/dstep */
1982 && !(f
->status
& L_ATOM
)
1983 && !(g
->status
& (ATOM
|L_ATOM
)))
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 */
1988 for (h
= f
->sub
; h
; h
= h
->nxt
)
1989 if (scan_seq(h
->this))
1998 glob_args(Lextok
*n
)
2002 for (v
= n
->rgt
; v
; v
= v
->rgt
)
2003 { if (v
->lft
->ntyp
== CONST
)
2005 if (v
->lft
->ntyp
== EVAL
)
2006 result
+= has_global(v
->lft
->lft
);
2008 result
+= has_global(v
->lft
);
2014 proc_is_safe(const Lextok
*n
)
2016 /* not safe unless no local var inits are used */
2017 /* note that a local variable init could refer to a global */
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);
2024 non_fatal("bad call to proc_is_safe", (char *) 0);
2030 has_global(Lextok
*n
)
2034 if (AllGlobal
) return 1; /* global provided clause */
2040 return scan_seq(n
->sl
->this);
2048 case ELSE
: return n
->val
; /* true if combined with chan refs */
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
));
2061 || (n
->sym
->hidden
&64)
2062 || strcmp(n
->sym
->name
, "_pid") == 0
2063 || strcmp(n
->sym
->name
, "_") == 0)
2068 return proc_is_safe(n
);
2070 case C_CODE
: case C_EXPR
:
2071 return glob_inline(n
->sym
->name
);
2073 case ENABLED
: case PC_VAL
: case NONPROGRESS
:
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
2086 case '!': case UMIN
: case '~': case ASSERT
:
2087 return has_global(n
->lft
);
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
);
2097 for (v
= n
->lft
; v
; v
= v
->rgt
)
2098 if (has_global(v
->lft
)) return 1;
2101 return has_global(n
->lft
);
2107 Bailout(FILE *fd
, char *str
)
2110 fprintf(fd
, "continue%s", str
);
2112 fprintf(fd
, "%s%s", NextLab
[Level
], str
);
2114 fprintf(fd
, "Uerror(\"block in step seq\")%s", str
);
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)
2124 putstmnt(FILE *fd
, Lextok
*now
, int m
)
2128 if (!now
) { fprintf(fd
, "0"); return; }
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;
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;
2159 fprintf(fd
, "((tau)&1)");
2161 fprintf(fd
, "((trpt->tau)&1)");
2163 printf("spin: line %3d, warning: 'timeout' in d_step sequence\n",
2165 /* is okay as a guard */
2169 if (now
->sym
== NULL
)
2170 Fatal("internal error pangen2.c", (char *) 0);
2172 && strcmp(now
->sym
->name
, claimproc
) == 0)
2173 fatal("claim %s, (not runnable)", claimproc
);
2175 && strcmp(now
->sym
->name
, eventmap
) == 0)
2176 fatal("eventmap %s, (not runnable)", eventmap
);
2179 fatal("'run' in d_step sequence (use atomic)",
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
);
2186 check_param_count(i
, now
);
2189 { /* printf("\t%d parameters used, max %d expected\n", i, Npars); */
2190 fatal("too many parameters in run %s(...)", now
->sym
->name
);
2192 for ( ; i
< Npars
; i
++)
2198 cat3("enabled(II, ", now
->lft
, ")");
2202 /* o_pm&4=progress, tau&128=claim stutter */
2204 fprintf(fd
, "(!(o_pm&4) && !(tau&128))");
2206 fprintf(fd
, "(!(trpt->o_pm&4) && !(trpt->tau&128))");
2210 cat3("((P0 *) Pptr(", now
->lft
, "+BASE))->_p");
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");
2223 putname(fd
, "q_len(", now
->lft
, m
, ")");
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");
2236 putname(fd
, "q_full(", now
->lft
, m
, ")");
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");
2249 putname(fd
, "(q_len(", now
->lft
, m
, ")==0)");
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");
2259 putname(fd
, "(!q_full(", now
->lft
, m
, "))");
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");
2269 putname(fd
, "(q_len(", now
->lft
, m
, ")>0)");
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
)
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
);
2287 putstmnt(fd
, v
->lft
->lft
, m
);
2290 fprintf(fd
, "\t\t continue");
2291 putname(th
, " || (x_y3_ == ", now
->lft
, m
, ")");
2298 putname(fd
, "!q_full(", now
->lft
, m
, ")");
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");
2307 fprintf(fd
, "if (q_%s",
2308 (u_sync
> 0 && u_async
== 0)?"len":"full");
2309 putname(fd
, "(", now
->lft
, m
, "))\n");
2312 fprintf(fd
, "\t\t{ nlost++; delta_m = 1; } else {");
2314 { fprintf(fd
, "\t\t\t");
2319 fprintf(fd
, "\n\t\tif (TstOnly) return 1;");
2321 if (u_sync
&& !u_async
&& rvopt
)
2322 fprintf(fd
, "\n\n\t\tif (no_recvs(II)) continue;\n");
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");
2329 for (v
= now
->rgt
, i
= 0; v
; v
= v
->rgt
, i
++)
2330 { cat3("\t\tsprintf(simtmp, \"%%d\", ", v
->lft
, "); strcat(simvals, simtmp);");
2332 fprintf(fd
, "\t\tstrcat(simvals, \",\");\n");
2335 fprintf(fd
, "\t\t}\n");
2336 fprintf(fd
, "#endif\n\t\t");
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
);
2345 putname(stdout
, "channel name: ", now
->lft
, m
, "\n");
2347 printf(" %d msg parameters sent, %d expected\n", i
, Mpars
);
2348 fatal("too many pars in send", "");
2350 for (j
= i
; i
< Mpars
; i
++)
2352 fprintf(fd
, ", %d)", j
);
2354 { fprintf(fd
, ";\n\t\t");
2356 putname(fd
, "if (q_zero(", now
->lft
, m
, ")) ");
2357 putname(fd
, "{ boq = ", now
->lft
, m
, "");
2359 fprintf(fd
, "; Uerror(\"rv-attempt in d_step\")");
2363 fprintf(fd
, ";\n\t\t}\n\t\t"); /* end of m_loss else */
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
)
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
);
2380 putstmnt(fd
, v
->lft
->lft
, m
);
2383 fprintf(fd
, "\t\t continue");
2385 putname(tc
, " || (x_y3_ == ", now
->lft
, m
, ")");
2390 { fprintf(fd
, "((");
2391 if (u_sync
) fprintf(fd
, "(boq == -1 && ");
2393 putname(fd
, "q_len(", now
->lft
, m
, ")");
2395 if (u_sync
&& now
->val
<= 1)
2396 { putname(fd
, ") || (boq == ", now
->lft
,m
," && ");
2397 putname(fd
, "q_zero(", now
->lft
,m
,"))");
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
);
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
);
2426 { fprintf(fd
, ", 0, 0");
2428 for ( ; i
< Mpars
; i
++)
2429 fprintf(fd
, ", 0, 0");
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");
2442 { if (now
->val
>= 2)
2444 { fprintf(fd
, "if (");
2445 putname(fd
, "q_zero(", now
->lft
,m
,"))");
2446 fprintf(fd
, "\n\t\t{\t");
2448 fprintf(fd
, "uerror(\"polling ");
2449 fprintf(fd
, "rv chan\");\n\t\t");
2451 fprintf(fd
, " continue;\n\t\t}\n\t\t");
2452 fprintf(fd
, "IfNotBlocked\n\t\t");
2454 { fprintf(fd
, "if (");
2456 putname(fd
, "boq != ", now
->lft
,m
,") ");
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) ");
2464 Bailout(fd
, ";\n\t\t");
2466 fprintf(fd
, "}\n\t\t");
2468 putname(fd
, "if (q_len(", now
->lft
, m
, ") == 0) ");
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 */
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
);
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
);
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
);
2503 { fprintf(fd
, ", 0, 0");
2505 for ( ; i
< Mpars
; i
++)
2506 fprintf(fd
, ", 0, 0");
2507 fprintf(fd
, "))) ");
2509 fprintf(fd
, ";\n\t\t");
2512 fprintf(fd
, "(trpt+1)->bup.ovals[%d] = ",
2516 fprintf(fd
, "(trpt+1)->bup.oval = ");
2521 fprintf(fd
, ";\n\t\tif (TstOnly) return 1");
2523 if (j
== 0 && now
->val
>= 2)
2524 { fprintf(fd
, ";\n\t\t");
2525 break; /* poll without side-effect */
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");
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 */
2545 for (v
= now
->rgt
, i
= 0; v
; v
= v
->rgt
, i
++)
2548 if ((v
->lft
->ntyp
== CONST
2549 || v
->lft
->ntyp
== EVAL
))
2554 sprintf(tempbuf
, "(trpt+1)->bup.ovals[%d] = ",
2558 sprintf(tempbuf
, "(trpt+1)->bup.oval = ");
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
);
2566 cat3(tempbuf
, v
->lft
, ";\n\t\t");
2571 if (jj
) /* check for double entries q?x,x */
2574 for (v
= now
->rgt
; v
; v
= v
->rgt
)
2575 { if (v
->lft
->ntyp
!= CONST
2576 && v
->lft
->ntyp
!= EVAL
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",
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
)
2591 fprintf(fd
, ";\n\t\t");
2593 if (v
->lft
->ntyp
!= CONST
2594 && v
->lft
->ntyp
!= EVAL
2595 && v
->lft
->sym
!= NULL
2596 && strcmp(v
->lft
->sym
->name
, "_") != 0)
2599 putstmnt(fd
, v
->lft
, m
);
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);
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;
2618 putstmnt(fd
,v
->lft
,m
);
2619 withprocname
= terse
= nocast
= 0;
2620 fprintf(fd
, "\", ");
2621 putstmnt(fd
,v
->lft
,m
);
2623 fprintf(fd
, ");\n#endif\n");
2624 fprintf(fd
, "\t\t");
2627 fprintf(fd
, ";\n\t\t");
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");
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);");
2638 { cat3("\t\tsprintf(simtmp, \"%%d\", ", v
->lft
->lft
, "); strcat(simvals, simtmp);");
2641 fprintf(fd
, "\t\tstrcat(simvals, \",\");\n");
2644 fprintf(fd
, "\t\t}\n");
2645 fprintf(fd
, "#endif\n\t\t");
2648 { putname(fd
, "if (q_zero(", now
->lft
, m
, "))");
2649 fprintf(fd
, "\n\t\t{ boq = -1;\n");
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");
2670 fprintf(fd
, "\n\t\t}");
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");
2685 putname(fd
, "not_RV(", now
->lft
, m
, ") && \\\n\t\t");
2687 for (v
= now
->rgt
, i
=j
=0; v
; v
= v
->rgt
, i
++)
2688 if (v
->lft
->ntyp
!= CONST
2689 && v
->lft
->ntyp
!= EVAL
)
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
)
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
);
2704 putstmnt(fd
, v
->lft
->lft
, m
);
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
);
2717 fprintf(fd
, ", 0, 0");
2719 for ( ; i
< Mpars
; i
++)
2720 fprintf(fd
, ", 0, 0");
2726 preruse(fd
, now
->lft
); /* preconditions */
2727 cat3("if (!(", now
->lft
, "))\n\t\t\t");
2733 { if (separate
== 2)
2734 fprintf(fd
, "if (o_pm&1)\n\t\t\t");
2736 fprintf(fd
, "if (trpt->o_pm&1)\n\t\t\t");
2739 { fprintf(fd
, "/* else */");
2745 { cat3("( (", now
->lft
, ") ? ");
2748 { cat3("(", now
->rgt
->lft
, ") : ");
2749 cat3("(", now
->rgt
->rgt
, ") )");
2755 fprintf(fd
, "if (TstOnly) return 1;\n\t\t");
2762 sprintf(tempbuf
, "(trpt+1)->bup.ovals[%d] = ",
2765 cat3(tempbuf
, now
->lft
, ";\n\t\t");
2767 { cat3("(trpt+1)->bup.oval = ", now
->lft
, ";\n\t\t");
2769 nocast
= 1; putstmnt(fd
,now
->lft
,m
); nocast
= 0;
2772 putstmnt(fd
,now
->rgt
,m
);
2774 if (now
->sym
->type
!= CHAN
2776 { fprintf(fd
, ";\n#ifdef VAR_RANGES");
2777 fprintf(fd
, "\n\t\tlogval(\"");
2778 withprocname
= terse
= nocast
= 1;
2780 putstmnt(fd
,now
->lft
,m
);
2781 withprocname
= terse
= nocast
= 0;
2782 fprintf(fd
, "\", ");
2783 putstmnt(fd
,now
->lft
,m
);
2785 fprintf(fd
, ");\n#endif\n");
2786 fprintf(fd
, "\t\t");
2792 fprintf(fd
, "if (TstOnly) return 1;\n\t\t");
2794 fprintf(fd
, "printf(%s", now
->sym
->name
);
2796 fprintf(fd
, "Printf(%s", now
->sym
->name
);
2798 for (v
= now
->lft
; v
; v
= v
->rgt
)
2799 { cat2(", ", v
->lft
);
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
);
2811 putstmnt(fd
, now
->lft
, m
);
2816 if (!nocast
&& now
->sym
&& Sym_typ(now
) < SHORT
)
2817 putname(fd
, "((int)", now
, m
, ")");
2819 putname(fd
, "", now
, m
, "");
2823 putremote(fd
, now
, m
);
2828 fprintf(fd
, "%s", now
->sym
->name
);
2830 fprintf(fd
, "%d", remotelab(now
));
2835 plunk_expr(fd
, now
->sym
->name
);
2839 fprintf(fd
, ") /* %s */ ", now
->sym
->name
);
2845 fprintf(fd
, "/* %s */\n\t\t", now
->sym
->name
);
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 */
2854 plunk_inline(fd
, now
->sym
->name
, 1);
2856 Fatal("internal error pangen2.c", (char *) 0);
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");
2868 fprintf(fd
, "if (TstOnly) return 1;\n\t\t");
2870 cat3("assert(", now
->lft
, ", ");
2872 cat3("\"", now
->lft
, "\", II, tt, t)");
2879 if (Pid
== eventmapnr
)
2880 fprintf(fd
, "Uerror(\"cannot get here\")");
2885 if (Pid
== eventmapnr
)
2886 { fprintf(fd
, "return 0");
2891 { fprintf(fd
, "if (TstOnly)\n\t\t\t");
2892 fprintf(fd
, "return (II+1 == now._nr_pr);\n\t\t");
2894 fprintf(fd
, "if (!delproc(1, II)) ");
2899 printf("spin: bad node type %d (.m) - line %d\n",
2900 now
->ntyp
, now
->ln
);
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
;
2912 fatal("no name - putname", (char *) 0);
2914 if (s
->context
&& context
&& s
->type
)
2915 s
= findloc(s
); /* it's a local var */
2918 { fprintf(fd
, "%s%s%s", pre
, n
->sym
->name
, suff
);
2921 if (!s
->type
) /* not a local name */
2922 s
= lookup(s
->name
); /* must be a global */
2925 { if (strcmp(pre
, ".") != 0)
2926 non_fatal("undeclared variable '%s'", s
->name
);
2930 if (s
->type
== PROCTYPE
)
2931 fatal("proctype-name '%s' used as array-name", s
->name
);
2934 if (!terse
&& !s
->owner
&& evalindex
!= 1)
2936 || strcmp(s
->name
, "_p") == 0
2937 || strcmp(s
->name
, "_pid") == 0)
2938 { fprintf(fd
, "((P%d *)this)->", Pid
);
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);
2949 && strcmp(pre
, "."))
2950 fprintf(fd
, "%s:", s
->context
->name
);
2953 fprintf(fd
, "%s", s
->name
);
2958 non_fatal("ref to array element invalid in this context",
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");
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())
2973 { fprintf(fd
, "[%%d]");
2974 } else if (evalindex
== 1)
2975 { evalindex
= 0; /* no good if index is indexed array */
2977 putstmnt(fd
, n
->lft
, m
);
2982 && n
->lft
->ntyp
== CONST
2983 && n
->lft
->val
< s
->nel
)
2984 || (!n
->lft
&& s
->nel
> 0))
2985 { cat3("[", n
->lft
, "]");
2987 { cat3("[ Index(", n
->lft
, ", ");
2988 fprintf(fd
, "%d) ]", s
->nel
);
2992 if (s
->type
== STRUCT
&& n
->rgt
&& n
->rgt
->lft
)
2993 { putname(fd
, ".", n
->rgt
->lft
, m
, "");
2999 putremote(FILE *fd
, Lextok
*n
, int m
) /* remote reference */
3004 { fprintf(fd
, "%s", n
->lft
->sym
->name
); /* proctype name */
3007 putstmnt(fd
, n
->lft
->lft
, m
); /* pid */
3010 fprintf(fd
, ".%s", n
->sym
->name
);
3012 { if (Sym_typ(n
) < SHORT
)
3014 fprintf(fd
, "((int)");
3017 pt
= fproc(n
->lft
->sym
->name
);
3018 fprintf(fd
, "((P%d *)Pptr(", pt
);
3020 { fprintf(fd
, "BASE+");
3021 putstmnt(fd
, n
->lft
->lft
, m
);
3023 fprintf(fd
, "f_pid(%d)", pt
);
3024 fprintf(fd
, "))->%s", n
->sym
->name
);
3028 putstmnt(fd
, n
->rgt
, m
); /* array var ref */
3031 if (promoted
) fprintf(fd
, ")");
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.
3044 case TIMEOUT
: return 1;
3045 case 'c': if (has_typ(n
->lft
, TIMEOUT
)) return 1;
3051 has_typ(Lextok
*n
, int m
)
3054 if (n
->ntyp
== m
) return 1;
3055 return (has_typ(n
->lft
, m
) || has_typ(n
->rgt
, m
));
3058 static int runcount
, opcount
;
3061 do_count(Lextok
*n
, int checkop
)
3070 if (checkop
) opcount
++;
3073 do_count(n
->lft
, checkop
&& (n
->ntyp
!= RUN
));
3074 do_count(n
->rgt
, checkop
);
3078 count_runs(Lextok
*n
)
3080 runcount
= opcount
= 0;
3083 fatal("more than one run operator in expression", "");
3084 if (runcount
== 1 && opcount
> 1)
3085 fatal("use of run operator in compound expression", "");
3091 runcount
= opcount
= 0;
3094 fatal("run operator used in invalid context", "");
This page took 0.228541 seconds and 4 git commands to generate.