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