1 /***** spin: dstep.c *****/
2
3 /*
4 * This file is part of the public release of Spin. It is subject to the
5 * terms in the LICENSE file that is included in this source directory.
6 * Tool documentation is available at http://spinroot.com
7 */
8
9 #include <assert.h>
10 #include "spin.h"
11 #include "y.tab.h"
12
13 #define MAXDSTEP 2048 /* was 512 */
14
15 char *NextLab[64]; /* must match value in pangen2.c:41 */
16 int Level=0, GenCode=0, IsGuard=0, TestOnly=0;
17
18 static int Tj=0, Jt=0, LastGoto=0;
19 static int Tojump[MAXDSTEP], Jumpto[MAXDSTEP], Special[MAXDSTEP];
20 static void putCode(FILE *, Element *, Element *, Element *, int);
21
22 extern int Pid_nr, separate, OkBreak;
23
24 static void
Sourced(int n,int special)25 Sourced(int n, int special)
26 { int i;
27 for (i = 0; i < Tj; i++)
28 if (Tojump[i] == n)
29 return;
30 if (Tj >= MAXDSTEP)
31 fatal("d_step sequence too long", (char *)0);
32 Special[Tj] = special;
33 Tojump[Tj++] = n;
34 }
35
36 static void
Dested(int n)37 Dested(int n)
38 { int i;
39 for (i = 0; i < Tj; i++)
40 if (Tojump[i] == n)
41 return;
42 for (i = 0; i < Jt; i++)
43 if (Jumpto[i] == n)
44 return;
45 if (Jt >= MAXDSTEP)
46 fatal("d_step sequence too long", (char *)0);
47 Jumpto[Jt++] = n;
48 LastGoto = 1;
49 }
50
51 static void
Mopup(FILE * fd)52 Mopup(FILE *fd)
53 { int i, j;
54
55 for (i = 0; i < Jt; i++)
56 { for (j = 0; j < Tj; j++)
57 if (Tojump[j] == Jumpto[i])
58 break;
59 if (j == Tj)
60 { char buf[16];
61 if (Jumpto[i] == OkBreak)
62 { if (!LastGoto)
63 fprintf(fd, "S_%.3d_0: /* break-dest */\n",
64 OkBreak);
65 } else {
66 sprintf(buf, "S_%.3d_0", Jumpto[i]);
67 non_fatal("goto %s breaks from d_step seq", buf);
68 } } }
69 for (j = 0; j < Tj; j++)
70 { for (i = 0; i < Jt; i++)
71 if (Tojump[j] == Jumpto[i])
72 break;
73 #ifdef DEBUG
74 if (i == Jt && !Special[i])
75 fprintf(fd, "\t\t/* no goto's to S_%.3d_0 */\n",
76 Tojump[j]);
77 #endif
78 }
79 for (j = i = 0; j < Tj; j++)
80 if (Special[j])
81 { if (i >= MAXDSTEP)
82 { fatal("cannot happen (dstep.c)", (char *)0);
83 }
84 Tojump[i] = Tojump[j];
85 Special[i] = 2;
86 i++;
87 }
88 Tj = i; /* keep only the global exit-labels */
89 Jt = 0;
90 }
91
92 static int
FirstTime(int n)93 FirstTime(int n)
94 { int i;
95 for (i = 0; i < Tj; i++)
96 if (Tojump[i] == n)
97 return (Special[i] <= 1);
98 return 1;
99 }
100
101 static void
illegal(Element * e,char * str)102 illegal(Element *e, char *str)
103 {
104 printf("illegal operator in 'd_step:' '");
105 comment(stdout, e->n, 0);
106 printf("'\n");
107 fatal("'%s'", str);
108 }
109
110 static void
filterbad(Element * e)111 filterbad(Element *e)
112 {
113 switch (e->n->ntyp) {
114 case ASSERT:
115 case PRINT:
116 case 'c':
117 /* run cannot be completely undone
118 * with sv_save-sv_restor
119 */
120 if (any_oper(e->n->lft, RUN))
121 illegal(e, "run operator in d_step");
122
123 /* remote refs inside d_step sequences
124 * would be okay, but they cannot always
125 * be interpreted by the simulator the
126 * same as by the verifier (e.g., for an
127 * error trail)
128 */
129 if (any_oper(e->n->lft, 'p'))
130 illegal(e, "remote reference in d_step");
131 break;
132 case '@':
133 illegal(e, "process termination");
134 break;
135 case D_STEP:
136 illegal(e, "nested d_step sequence");
137 break;
138 case ATOMIC:
139 illegal(e, "nested atomic sequence");
140 break;
141 default:
142 break;
143 }
144 }
145
146 static int
CollectGuards(FILE * fd,Element * e,int inh)147 CollectGuards(FILE *fd, Element *e, int inh)
148 { SeqList *h; Element *ee;
149
150 for (h = e->sub; h; h = h->nxt)
151 { ee = huntstart(h->this->frst);
152 filterbad(ee);
153 switch (ee->n->ntyp) {
154 case NON_ATOMIC:
155 inh += CollectGuards(fd, ee->n->sl->this->frst, inh);
156 break;
157 case IF:
158 inh += CollectGuards(fd, ee, inh);
159 break;
160 case '.':
161 if (ee->nxt->n->ntyp == DO)
162 inh += CollectGuards(fd, ee->nxt, inh);
163 break;
164 case ELSE:
165 if (inh++ > 0) fprintf(fd, " || ");
166 /* 4.2.5 */ if (!pid_is_claim(Pid_nr))
167 fprintf(fd, "(boq == -1 /* else */)");
168 else
169 fprintf(fd, "(1 /* else */)");
170 break;
171 case 'R':
172 if (inh++ > 0) fprintf(fd, " || ");
173 fprintf(fd, "("); TestOnly=1;
174 putstmnt(fd, ee->n, ee->seqno);
175 fprintf(fd, ")"); TestOnly=0;
176 break;
177 case 'r':
178 if (inh++ > 0) fprintf(fd, " || ");
179 fprintf(fd, "("); TestOnly=1;
180 putstmnt(fd, ee->n, ee->seqno);
181 fprintf(fd, ")"); TestOnly=0;
182 break;
183 case 's':
184 if (inh++ > 0) fprintf(fd, " || ");
185 fprintf(fd, "("); TestOnly=1;
186 /* 4.2.1 */ if (!pid_is_claim(Pid_nr)) fprintf(fd, "(boq == -1) && ");
187 putstmnt(fd, ee->n, ee->seqno);
188 fprintf(fd, ")"); TestOnly=0;
189 break;
190 case 'c':
191 if (inh++ > 0) fprintf(fd, " || ");
192 fprintf(fd, "("); TestOnly=1;
193 if (!pid_is_claim(Pid_nr))
194 fprintf(fd, "(boq == -1 && ");
195 putstmnt(fd, ee->n->lft, e->seqno);
196 if (!pid_is_claim(Pid_nr))
197 fprintf(fd, ")");
198 fprintf(fd, ")"); TestOnly=0;
199 break;
200 } }
201 return inh;
202 }
203
204 int
putcode(FILE * fd,Sequence * s,Element * nxt,int justguards,int ln,int seqno)205 putcode(FILE *fd, Sequence *s, Element *nxt, int justguards, int ln, int seqno)
206 { int isg=0;
207 static char buf[64];
208
209 NextLab[0] = "continue";
210 filterbad(s->frst);
211
212 switch (s->frst->n->ntyp) {
213 case UNLESS:
214 non_fatal("'unless' inside d_step - ignored", (char *) 0);
215 return putcode(fd, s->frst->n->sl->this, nxt, 0, ln, seqno);
216 case NON_ATOMIC:
217 (void) putcode(fd, s->frst->n->sl->this, ZE, 1, ln, seqno);
218 if (justguards) return 0; /* 6.2.5 */
219 break;
220 case IF:
221 fprintf(fd, "if (!(");
222 if (!CollectGuards(fd, s->frst, 0)) /* what about boq? */
223 fprintf(fd, "1");
224 fprintf(fd, "))\n\t\t\tcontinue;");
225 isg = 1;
226 break;
227 case '.':
228 if (s->frst->nxt->n->ntyp == DO)
229 { fprintf(fd, "if (!(");
230 if (!CollectGuards(fd, s->frst->nxt, 0))
231 fprintf(fd, "1");
232 fprintf(fd, "))\n\t\t\tcontinue;");
233 isg = 1;
234 }
235 break;
236 case 'R': /* <- can't really happen (it's part of a 'c') */
237 fprintf(fd, "if (!("); TestOnly=1;
238 putstmnt(fd, s->frst->n, s->frst->seqno);
239 fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
240 break;
241 case 'r':
242 fprintf(fd, "if (!("); TestOnly=1;
243 putstmnt(fd, s->frst->n, s->frst->seqno);
244 fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
245 break;
246 case 's':
247 fprintf(fd, "if (");
248 #if 1
249 /* 4.2.1 */ if (!pid_is_claim(Pid_nr)) fprintf(fd, "(boq != -1) || ");
250 #endif
251 fprintf(fd, "!("); TestOnly=1;
252 putstmnt(fd, s->frst->n, s->frst->seqno);
253 fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
254 break;
255 case 'c':
256 fprintf(fd, "if (!(");
257 if (!pid_is_claim(Pid_nr)) fprintf(fd, "boq == -1 && ");
258 TestOnly=1;
259 putstmnt(fd, s->frst->n->lft, s->frst->seqno);
260 fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
261 break;
262 case ELSE:
263 fprintf(fd, "if (boq != -1 || (");
264 if (separate != 2) fprintf(fd, "trpt->");
265 fprintf(fd, "o_pm&1))\n\t\t\tcontinue;");
266 { extern FILE *fd_th;
267 fprintf(fd_th, "#ifndef ELSE_IN_GUARD\n");
268 fprintf(fd_th, " #define ELSE_IN_GUARD\n");
269 fprintf(fd_th, "#endif\n");
270 }
271 break;
272 case ASGN: /* new 3.0.8 */
273 fprintf(fd, "IfNotBlocked");
274 break;
275 default:
276 fprintf(fd, "/* default %d */\n\t\t", s->frst->n->ntyp);
277 }
278
279 /* 6.2.5 : before TstOnly */
280 fprintf(fd, "\n\n\t\treached[%d][%d] = 1;\n\t\t", Pid_nr, seqno);
281 fprintf(fd, "reached[%d][t->st] = 1;\n\t\t", Pid_nr); /* next state */
282 fprintf(fd, "reached[%d][tt] = 1;\n", Pid_nr); /* current state */
283
284 /* 6.2.5 : before sv_save() */
285 if (s->frst->n->ntyp != NON_ATOMIC)
286 fprintf(fd, "\n\t\tif (TstOnly) return 1;\n"); /* if called from enabled() */
287
288 if (justguards) return 0;
289
290 fprintf(fd, "\n\t\tsv_save();\n\t\t");
291 sprintf(buf, "Uerror(\"block in d_step seq, line %d\")", ln);
292 NextLab[0] = buf;
293 putCode(fd, s->frst, s->extent, nxt, isg);
294
295 if (nxt)
296 { extern Symbol *Fname;
297 extern int lineno;
298
299 if (FirstTime(nxt->Seqno)
300 && (!(nxt->status & DONE2) || !(nxt->status & D_ATOM)))
301 { fprintf(fd, "S_%.3d_0: /* 1 */\n", nxt->Seqno);
302 nxt->status |= DONE2;
303 LastGoto = 0;
304 }
305 Sourced(nxt->Seqno, 1);
306 lineno = ln;
307 Fname = nxt->n->fn;
308 Mopup(fd);
309 }
310 unskip(s->frst->seqno);
311 return LastGoto;
312 }
313
314 static void
putCode(FILE * fd,Element * f,Element * last,Element * next,int isguard)315 putCode(FILE *fd, Element *f, Element *last, Element *next, int isguard)
316 { Element *e, *N;
317 SeqList *h; int i;
318 char NextOpt[64];
319 static int bno = 0;
320
321 for (e = f; e; e = e->nxt)
322 { if (e->status & DONE2)
323 continue;
324 e->status |= DONE2;
325
326 if (!(e->status & D_ATOM))
327 { if (!LastGoto)
328 { fprintf(fd, "\t\tgoto S_%.3d_0;\n",
329 e->Seqno);
330 Dested(e->Seqno);
331 }
332 break;
333 }
334 fprintf(fd, "S_%.3d_0: /* 2 */\n", e->Seqno);
335 LastGoto = 0;
336 Sourced(e->Seqno, 0);
337
338 if (!e->sub)
339 { filterbad(e);
340 switch (e->n->ntyp) {
341 case NON_ATOMIC:
342 h = e->n->sl;
343 putCode(fd, h->this->frst,
344 h->this->extent, e->nxt, 0);
345 break;
346 case BREAK:
347 if (LastGoto) break;
348 if (e->nxt)
349 { i = target( huntele(e->nxt,
350 e->status, -1))->Seqno;
351 fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
352 fprintf(fd, "/* 'break' */\n");
353 Dested(i);
354 } else
355 { if (next)
356 { fprintf(fd, "\t\tgoto S_%.3d_0;",
357 next->Seqno);
358 fprintf(fd, " /* NEXT */\n");
359 Dested(next->Seqno);
360 } else
361 fatal("cannot interpret d_step", 0);
362 }
363 break;
364 case GOTO:
365 if (LastGoto) break;
366 i = huntele( get_lab(e->n,1),
367 e->status, -1)->Seqno;
368 fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
369 fprintf(fd, "/* 'goto' */\n");
370 Dested(i);
371 break;
372 case '.':
373 if (LastGoto) break;
374 if (e->nxt && (e->nxt->status & DONE2))
375 { i = e->nxt->Seqno;
376 fprintf(fd, "\t\tgoto S_%.3d_0;", i);
377 fprintf(fd, " /* '.' */\n");
378 Dested(i);
379 }
380 break;
381 default:
382 putskip(e->seqno);
383 GenCode = 1; IsGuard = isguard;
384 fprintf(fd, "\t\t");
385 putstmnt(fd, e->n, e->seqno);
386 fprintf(fd, ";\n");
387 GenCode = IsGuard = isguard = LastGoto = 0;
388 break;
389 }
390 i = e->nxt?e->nxt->Seqno:0;
391 if (e->nxt && (e->nxt->status & DONE2) && !LastGoto)
392 { fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
393 fprintf(fd, "/* ';' */\n");
394 Dested(i);
395 break;
396 }
397 } else
398 { for (h = e->sub, i=1; h; h = h->nxt, i++)
399 { sprintf(NextOpt, "goto S_%.3d_%d",
400 e->Seqno, i);
401 NextLab[++Level] = NextOpt;
402 N = (e->n && e->n->ntyp == DO) ? e : e->nxt;
403 putCode(fd, h->this->frst,
404 h->this->extent, N, 1);
405 Level--;
406 fprintf(fd, "%s: /* 3 */\n", &NextOpt[5]);
407 LastGoto = 0;
408 }
409 if (!LastGoto)
410 { fprintf(fd, "\t\tUerror(\"blocking sel ");
411 fprintf(fd, "in d_step (nr.%d, near line %d)\");\n",
412 bno++, (e->n)?e->n->ln:0);
413 LastGoto = 0;
414 }
415 }
416 if (e == last)
417 { if (!LastGoto && next)
418 { fprintf(fd, "\t\tgoto S_%.3d_0;\n",
419 next->Seqno);
420 Dested(next->Seqno);
421 }
422 break;
423 } }
424 }
425