Subversion Repositories planix.SVN

Rev

Rev 2 | Details | Compare with Previous | Last modification | View Log | RSS feed

Rev Author Line No. Line
2 - 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
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_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
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
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 
}