1 /***** spin: dstep.c *****/
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 */
15 #define MAXDSTEP 1024 /* was 512 */
18 int Level
=0, GenCode
=0, IsGuard
=0, TestOnly
=0;
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);
24 extern int Pid
, claimnr
, separate
, OkBreak
;
27 Sourced(int n
, int special
)
29 for (i
= 0; i
< Tj
; i
++)
33 fatal("d_step sequence too long", (char *)0);
34 Special
[Tj
] = special
;
41 for (i
= 0; i
< Tj
; i
++)
44 for (i
= 0; i
< Jt
; i
++)
48 fatal("d_step sequence too long", (char *)0);
57 for (i
= 0; i
< Jt
; i
++)
58 { for (j
= 0; j
< Tj
; j
++)
59 if (Tojump
[j
] == Jumpto
[i
])
63 if (Jumpto
[i
] == OkBreak
)
65 fprintf(fd
, "S_%.3d_0: /* break-dest */\n",
68 sprintf(buf
, "S_%.3d_0", Jumpto
[i
]);
69 non_fatal("goto %s breaks from d_step seq", buf
);
71 for (j
= 0; j
< Tj
; j
++)
72 { for (i
= 0; i
< Jt
; i
++)
73 if (Tojump
[j
] == Jumpto
[i
])
76 if (i
== Jt
&& !Special
[i
])
77 fprintf(fd
, "\t\t/* no goto's to S_%.3d_0 */\n",
81 for (j
= i
= 0; j
< Tj
; j
++)
83 { Tojump
[i
] = Tojump
[j
];
86 fatal("cannot happen (dstep.c)", (char *)0);
89 Tj
= i
; /* keep only the global exit-labels */
96 for (i
= 0; i
< Tj
; i
++)
98 return (Special
[i
] <= 1);
103 illegal(Element
*e
, char *str
)
105 printf("illegal operator in 'd_step:' '");
106 comment(stdout
, e
->n
, 0);
112 filterbad(Element
*e
)
114 switch (e
->n
->ntyp
) {
118 /* run cannot be completely undone
119 * with sv_save-sv_restor
121 if (any_oper(e
->n
->lft
, RUN
))
122 illegal(e
, "run operator in d_step");
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
130 if (any_oper(e
->n
->lft
, 'p'))
131 illegal(e
, "remote reference in d_step");
134 illegal(e
, "process termination");
137 illegal(e
, "nested d_step sequence");
140 illegal(e
, "nested atomic sequence");
148 CollectGuards(FILE *fd
, Element
*e
, int inh
)
149 { SeqList
*h
; Element
*ee
;
151 for (h
= e
->sub
; h
; h
= h
->nxt
)
152 { ee
= huntstart(h
->this->frst
);
154 switch (ee
->n
->ntyp
) {
156 inh
+= CollectGuards(fd
, ee
->n
->sl
->this->frst
, inh
);
159 inh
+= CollectGuards(fd
, ee
, inh
);
162 if (ee
->nxt
->n
->ntyp
== DO
)
163 inh
+= CollectGuards(fd
, ee
->nxt
, inh
);
166 if (inh
++ > 0) fprintf(fd
, " || ");
167 /* 4.2.5 */ if (Pid
!= claimnr
)
168 fprintf(fd
, "(boq == -1 /* else */)");
170 fprintf(fd
, "(1 /* else */)");
173 if (inh
++ > 0) fprintf(fd
, " || ");
174 fprintf(fd
, "("); TestOnly
=1;
175 putstmnt(fd
, ee
->n
, ee
->seqno
);
176 fprintf(fd
, ")"); TestOnly
=0;
179 if (inh
++ > 0) fprintf(fd
, " || ");
180 fprintf(fd
, "("); TestOnly
=1;
181 putstmnt(fd
, ee
->n
, ee
->seqno
);
182 fprintf(fd
, ")"); TestOnly
=0;
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;
192 if (inh
++ > 0) fprintf(fd
, " || ");
193 fprintf(fd
, "("); TestOnly
=1;
195 fprintf(fd
, "(boq == -1 && ");
196 putstmnt(fd
, ee
->n
->lft
, e
->seqno
);
199 fprintf(fd
, ")"); TestOnly
=0;
206 putcode(FILE *fd
, Sequence
*s
, Element
*nxt
, int justguards
, int ln
, int seqno
)
207 { int isg
=0; char buf
[64];
209 NextLab
[0] = "continue";
212 switch (s
->frst
->n
->ntyp
) {
214 non_fatal("'unless' inside d_step - ignored", (char *) 0);
215 return putcode(fd
, s
->frst
->n
->sl
->this, nxt
, 0, ln
, seqno
);
217 (void) putcode(fd
, s
->frst
->n
->sl
->this, ZE
, 1, ln
, seqno
);
220 fprintf(fd
, "if (!(");
221 if (!CollectGuards(fd
, s
->frst
, 0)) /* what about boq? */
223 fprintf(fd
, "))\n\t\t\tcontinue;");
227 if (s
->frst
->nxt
->n
->ntyp
== DO
)
228 { fprintf(fd
, "if (!(");
229 if (!CollectGuards(fd
, s
->frst
->nxt
, 0))
231 fprintf(fd
, "))\n\t\t\tcontinue;");
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;
241 fprintf(fd
, "if (!("); TestOnly
=1;
242 putstmnt(fd
, s
->frst
->n
, s
->frst
->seqno
);
243 fprintf(fd
, "))\n\t\t\tcontinue;"); TestOnly
=0;
248 /* 4.2.1 */ if (Pid
!= claimnr
) fprintf(fd
, "(boq != -1) || ");
250 fprintf(fd
, "!("); TestOnly
=1;
251 putstmnt(fd
, s
->frst
->n
, s
->frst
->seqno
);
252 fprintf(fd
, "))\n\t\t\tcontinue;"); TestOnly
=0;
255 fprintf(fd
, "if (!(");
256 if (Pid
!= claimnr
) fprintf(fd
, "boq == -1 && ");
258 putstmnt(fd
, s
->frst
->n
->lft
, s
->frst
->seqno
);
259 fprintf(fd
, "))\n\t\t\tcontinue;"); TestOnly
=0;
262 fprintf(fd
, "if (boq != -1 || (");
263 if (separate
!= 2) fprintf(fd
, "trpt->");
264 fprintf(fd
, "o_pm&1))\n\t\t\tcontinue;");
266 case ASGN
: /* new 3.0.8 */
267 fprintf(fd
, "IfNotBlocked");
270 if (justguards
) return 0;
272 fprintf(fd
, "\n\t\tsv_save();\n\t\t");
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 */
278 sprintf(buf
, "Uerror(\"block in d_step seq, line %d\")", ln
);
280 putCode(fd
, s
->frst
, s
->extent
, nxt
, isg
);
283 { extern Symbol
*Fname
;
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
;
292 Sourced(nxt
->Seqno
, 1);
297 unskip(s
->frst
->seqno
);
302 putCode(FILE *fd
, Element
*f
, Element
*last
, Element
*next
, int isguard
)
308 for (e
= f
; e
; e
= e
->nxt
)
309 { if (e
->status
& DONE2
)
313 if (!(e
->status
& D_ATOM
))
315 { fprintf(fd
, "\t\tgoto S_%.3d_0;\n",
321 fprintf(fd
, "S_%.3d_0: /* 2 */\n", e
->Seqno
);
323 Sourced(e
->Seqno
, 0);
327 switch (e
->n
->ntyp
) {
330 putCode(fd
, h
->this->frst
,
331 h
->this->extent
, e
->nxt
, 0);
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");
343 { fprintf(fd
, "\t\tgoto S_%.3d_0;",
345 fprintf(fd
, " /* NEXT */\n");
348 fatal("cannot interpret d_step", 0);
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");
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");
370 GenCode
= 1; IsGuard
= isguard
;
372 putstmnt(fd
, e
->n
, e
->seqno
);
374 GenCode
= IsGuard
= isguard
= LastGoto
= 0;
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");
385 { for (h
= e
->sub
, i
=1; h
; h
= h
->nxt
, i
++)
386 { sprintf(NextOpt
, "goto S_%.3d_%d",
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);
393 fprintf(fd
, "%s: /* 3 */\n", &NextOpt
[5]);
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);
404 { if (!LastGoto
&& next
)
405 { fprintf(fd
, "\t\tgoto S_%.3d_0;\n",
This page took 0.05932 seconds and 4 git commands to generate.