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