0b55f123 |
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 1024 /* 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, claimnr, separate, OkBreak; |
25 | |
26 | static void |
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 |
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 |
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 |
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 |
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 |
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 |
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 != claimnr) |
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 != claimnr) 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 != claimnr) |
195 | fprintf(fd, "(boq == -1 && "); |
196 | putstmnt(fd, ee->n->lft, e->seqno); |
197 | if (Pid != claimnr) |
198 | fprintf(fd, ")"); |
199 | fprintf(fd, ")"); TestOnly=0; |
200 | break; |
201 | } } |
202 | return inh; |
203 | } |
204 | |
205 | int |
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 != claimnr) 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 != claimnr) 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 |
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 | } |