0b55f123 |
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 | } |