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: run.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 <stdlib.h>
13 
#include "spin.h"
14 
#include "y.tab.h"
15 
 
16 
extern RunList	*X, *run;
17 
extern Symbol	*Fname;
18 
extern Element	*LastStep;
19 
extern int	Rvous, lineno, Tval, interactive, MadeChoice;
20 
extern int	TstOnly, verbose, s_trail, xspin, jumpsteps, depth;
21 
extern int	analyze, nproc, nstop, no_print, like_java;
22 
 
23 
static long	Seed = 1;
24 
static int	E_Check = 0, Escape_Check = 0;
25 
 
26 
static int	eval_sync(Element *);
27 
static int	pc_enabled(Lextok *n);
28 
extern void	sr_buf(int, int);
29 
 
30 
void
31 
Srand(unsigned int s)
32 
{	Seed = s;
33 
}
34 
 
35 
long
36 
Rand(void)
37 
{	/* CACM 31(10), Oct 1988 */
38 
	Seed = 16807*(Seed%127773) - 2836*(Seed/127773);
39 
	if (Seed <= 0) Seed += 2147483647;
40 
	return Seed;
41 
}
42 
 
43 
Element *
44 
rev_escape(SeqList *e)
45 
{	Element *r;
46 
 
47 
	if (!e)
48 
		return (Element *) 0;
49 
 
50 
	if ((r = rev_escape(e->nxt)) != ZE) /* reversed order */
51 
		return r;
52 
 
53 
	return eval_sub(e->this->frst);
54 
}
55 
 
56 
Element *
57 
eval_sub(Element *e)
58 
{	Element *f, *g;
59 
	SeqList *z;
60 
	int i, j, k, only_pos;
61 
 
62 
	if (!e || !e->n)
63 
		return ZE;
64 
#ifdef DEBUG
65 
	printf("\n\teval_sub(%d %s: line %d) ",
66 
		e->Seqno, e->esc?"+esc":"", e->n?e->n->ln:0);
67 
	comment(stdout, e->n, 0);
68 
	printf("\n");
69 
#endif
70 
	if (e->n->ntyp == GOTO)
71 
	{	if (Rvous) return ZE;
72 
		LastStep = e;
73 
		f = get_lab(e->n, 1);
74 
		f = huntele(f, e->status, -1); /* 5.2.3: was missing */
75 
		cross_dsteps(e->n, f->n);
76 
#ifdef DEBUG
77 
		printf("GOTO leads to %d\n", f->seqno);
78 
#endif
79 
		return f;
80 
	}
81 
	if (e->n->ntyp == UNLESS)
82 
	{	/* escapes were distributed into sequence */
83 
		return eval_sub(e->sub->this->frst);
84 
	} else if (e->sub)	/* true for IF, DO, and UNLESS */
85 
	{	Element *has_else = ZE;
86 
		Element *bas_else = ZE;
87 
		int nr_else = 0, nr_choices = 0;
88 
		only_pos = -1;
89 
 
90 
		if (interactive
91 
		&& !MadeChoice && !E_Check
92 
		&& !Escape_Check
93 
		&& !(e->status&(D_ATOM))
94 
		&& depth >= jumpsteps)
95 
		{	printf("Select stmnt (");
96 
			whoruns(0); printf(")\n");
97 
			if (nproc-nstop > 1)
98 
			{	printf("\tchoice 0: other process\n");
99 
				nr_choices++;
100 
				only_pos = 0;
101 
		}	}
102 
		for (z = e->sub, j=0; z; z = z->nxt)
103 
		{	j++;
104 
			if (interactive
105 
			&& !MadeChoice && !E_Check
106 
			&& !Escape_Check
107 
			&& !(e->status&(D_ATOM))
108 
			&& depth >= jumpsteps
109 
			&& z->this->frst
110 
			&& (xspin || (verbose&32) || Enabled0(z->this->frst)))
111 
			{	if (z->this->frst->n->ntyp == ELSE)
112 
				{	has_else = (Rvous)?ZE:z->this->frst->nxt;
113 
					nr_else = j;
114 
					continue;
115 
				}
116 
				printf("\tchoice %d: ", j);
117 
#if 0
118 
				if (z->this->frst->n)
119 
					printf("line %d, ", z->this->frst->n->ln);
120 
#endif
121 
				if (!Enabled0(z->this->frst))
122 
					printf("unexecutable, ");
123 
				else
124 
				{	nr_choices++;
125 
					only_pos = j;
126 
				}
127 
				comment(stdout, z->this->frst->n, 0);
128 
				printf("\n");
129 
		}	}
130 
 
131 
		if (nr_choices == 0 && has_else)
132 
		{	printf("\tchoice %d: (else)\n", nr_else);
133 
			only_pos = nr_else;
134 
		}
135 
 
136 
		if (nr_choices <= 1 && only_pos != -1 && !MadeChoice)
137 
		{	MadeChoice = only_pos;
138 
		}
139 
 
140 
		if (interactive && depth >= jumpsteps
141 
		&& !Escape_Check
142 
		&& !(e->status&(D_ATOM))
143 
		&& !E_Check)
144 
		{	if (!MadeChoice)
145 
			{	char buf[256];
146 
				if (xspin)
147 
					printf("Make Selection %d\n\n", j);
148 
				else
149 
					printf("Select [0-%d]: ", j);
150 
				fflush(stdout);
151 
				if (scanf("%64s", buf) <= 0)
152 
				{	printf("no input\n");
153 
					return ZE;
154 
				}
155 
				if (isdigit((int)buf[0]))
156 
					k = atoi(buf);
157 
				else
158 
				{	if (buf[0] == 'q')
159 
						alldone(0);
160 
					k = -1;
161 
				}
162 
			} else
163 
			{	k = MadeChoice;
164 
				MadeChoice = 0;
165 
			}
166 
			if (k < 1 || k > j)
167 
			{	if (k != 0) printf("\tchoice outside range\n");
168 
				return ZE;
169 
			}
170 
			k--;
171 
		} else
172 
		{	if (e->n && e->n->indstep >= 0)
173 
				k = 0;	/* select 1st executable guard */
174 
			else
175 
				k = Rand()%j;	/* nondeterminism */
176 
		}
177 
 
178 
		has_else = ZE;
179 
		bas_else = ZE;
180 
		for (i = 0, z = e->sub; i < j+k; i++)
181 
		{	if (z->this->frst
182 
			&&  z->this->frst->n->ntyp == ELSE)
183 
			{	bas_else = z->this->frst;
184 
				has_else = (Rvous)?ZE:bas_else->nxt;
185 
				if (!interactive || depth < jumpsteps
186 
				|| Escape_Check
187 
				|| (e->status&(D_ATOM)))
188 
				{	z = (z->nxt)?z->nxt:e->sub;
189 
					continue;
190 
				}
191 
			}
192 
			if (z->this->frst
193 
			&&  ((z->this->frst->n->ntyp == ATOMIC
194 
			  ||  z->this->frst->n->ntyp == D_STEP)
195 
			  &&  z->this->frst->n->sl->this->frst->n->ntyp == ELSE))
196 
			{	bas_else = z->this->frst->n->sl->this->frst;
197 
				has_else = (Rvous)?ZE:bas_else->nxt;
198 
				if (!interactive || depth < jumpsteps
199 
				|| Escape_Check
200 
				|| (e->status&(D_ATOM)))
201 
				{	z = (z->nxt)?z->nxt:e->sub;
202 
					continue;
203 
				}
204 
			}
205 
			if (i >= k)
206 
			{	if ((f = eval_sub(z->this->frst)) != ZE)
207 
					return f;
208 
				else if (interactive && depth >= jumpsteps
209 
				&& !(e->status&(D_ATOM)))
210 
				{	if (!E_Check && !Escape_Check)
211 
						printf("\tunexecutable\n");
212 
					return ZE;
213 
			}	}
214 
			z = (z->nxt)?z->nxt:e->sub;
215 
		}
216 
		LastStep = bas_else;
217 
		return has_else;
218 
	} else
219 
	{	if (e->n->ntyp == ATOMIC
220 
		||  e->n->ntyp == D_STEP)
221 
		{	f = e->n->sl->this->frst;
222 
			g = e->n->sl->this->last;
223 
			g->nxt = e->nxt;
224 
			if (!(g = eval_sub(f)))	/* atomic guard */
225 
				return ZE;
226 
			return g;
227 
		} else if (e->n->ntyp == NON_ATOMIC)
228 
		{	f = e->n->sl->this->frst;
229 
			g = e->n->sl->this->last;
230 
			g->nxt = e->nxt;		/* close it */
231 
			return eval_sub(f);
232 
		} else if (e->n->ntyp == '.')
233 
		{	if (!Rvous) return e->nxt;
234 
			return eval_sub(e->nxt);
235 
		} else
236 
		{	SeqList *x;
237 
			if (!(e->status & (D_ATOM))
238 
			&&  e->esc && verbose&32)
239 
			{	printf("Stmnt [");
240 
				comment(stdout, e->n, 0);
241 
				printf("] has escape(s): ");
242 
				for (x = e->esc; x; x = x->nxt)
243 
				{	printf("[");
244 
					g = x->this->frst;
245 
					if (g->n->ntyp == ATOMIC
246 
					||  g->n->ntyp == NON_ATOMIC)
247 
						g = g->n->sl->this->frst;
248 
					comment(stdout, g->n, 0);
249 
					printf("] ");
250 
				}
251 
				printf("\n");
252 
			}
253 
#if 0
254 
			if (!(e->status & D_ATOM))	/* escapes don't reach inside d_steps */
255 
			/* 4.2.4: only the guard of a d_step can have an escape */
256 
#endif
257 
#if 1
258 
			if (!s_trail)	/* trail determines selections, new 5.2.5 */
259 
#endif
260 
			{	Escape_Check++;
261 
				if (like_java)
262 
				{	if ((g = rev_escape(e->esc)) != ZE)
263 
					{	if (verbose&4)
264 
							printf("\tEscape taken\n");
265 
						Escape_Check--;
266 
						return g;
267 
					}
268 
				} else
269 
				{	for (x = e->esc; x; x = x->nxt)
270 
					{	if ((g = eval_sub(x->this->frst)) != ZE)
271 
						{	if (verbose&4)
272 
							{	printf("\tEscape taken ");
273 
								if (g->n && g->n->fn)
274 
									printf("%s:%d", g->n->fn->name, g->n->ln);
275 
								printf("\n");
276 
							}
277 
							Escape_Check--;
278 
							return g;
279 
				}	}	}
280 
				Escape_Check--;
281 
			}
282 
 
283 
			switch (e->n->ntyp) {
284 
			case TIMEOUT: case RUN:
285 
			case PRINT: case PRINTM:
286 
			case C_CODE: case C_EXPR:
287 
			case ASGN: case ASSERT:
288 
			case 's': case 'r': case 'c':
289 
				/* toplevel statements only */
290 
				LastStep = e;
291 
			default:
292 
				break;
293 
			}
294 
			if (Rvous)
295 
			{
296 
				return (eval_sync(e))?e->nxt:ZE;
297 
			}
298 
			return (eval(e->n))?e->nxt:ZE;
299 
		}
300 
	}
301 
	return ZE; /* not reached */
302 
}
303 
 
304 
static int
305 
eval_sync(Element *e)
306 
{	/* allow only synchronous receives
307 
	   and related node types    */
308 
	Lextok *now = (e)?e->n:ZN;
309 
 
310 
	if (!now
311 
	||  now->ntyp != 'r'
312 
	||  now->val >= 2	/* no rv with a poll */
313 
	||  !q_is_sync(now))
314 
	{
315 
		return 0;
316 
	}
317 
 
318 
	LastStep = e;
319 
	return eval(now);
320 
}
321 
 
322 
static int
323 
assign(Lextok *now)
324 
{	int t;
325 
 
326 
	if (TstOnly) return 1;
327 
 
328 
	switch (now->rgt->ntyp) {
329 
	case FULL:	case NFULL:
330 
	case EMPTY:	case NEMPTY:
331 
	case RUN:	case LEN:
332 
		t = BYTE;
333 
		break;
334 
	default:
335 
		t = Sym_typ(now->rgt);
336 
		break;
337 
	}
338 
	typ_ck(Sym_typ(now->lft), t, "assignment");
339 
	return setval(now->lft, eval(now->rgt));
340 
}
341 
 
342 
static int
343 
nonprogress(void)	/* np_ */
344 
{	RunList	*r;
345 
 
346 
	for (r = run; r; r = r->nxt)
347 
	{	if (has_lab(r->pc, 4))	/* 4=progress */
348 
			return 0;
349 
	}
350 
	return 1;
351 
}
352 
 
353 
int
354 
eval(Lextok *now)
355 
{
356 
	if (now) {
357 
	lineno = now->ln;
358 
	Fname  = now->fn;
359 
#ifdef DEBUG
360 
	printf("eval ");
361 
	comment(stdout, now, 0);
362 
	printf("\n");
363 
#endif
364 
	switch (now->ntyp) {
365 
	case CONST: return now->val;
366 
	case   '!': return !eval(now->lft);
367 
	case  UMIN: return -eval(now->lft);
368 
	case   '~': return ~eval(now->lft);
369 
 
370 
	case   '/': return (eval(now->lft) / eval(now->rgt));
371 
	case   '*': return (eval(now->lft) * eval(now->rgt));
372 
	case   '-': return (eval(now->lft) - eval(now->rgt));
373 
	case   '+': return (eval(now->lft) + eval(now->rgt));
374 
	case   '%': return (eval(now->lft) % eval(now->rgt));
375 
	case    LT: return (eval(now->lft) <  eval(now->rgt));
376 
	case    GT: return (eval(now->lft) >  eval(now->rgt));
377 
	case   '&': return (eval(now->lft) &  eval(now->rgt));
378 
	case   '^': return (eval(now->lft) ^  eval(now->rgt));
379 
	case   '|': return (eval(now->lft) |  eval(now->rgt));
380 
	case    LE: return (eval(now->lft) <= eval(now->rgt));
381 
	case    GE: return (eval(now->lft) >= eval(now->rgt));
382 
	case    NE: return (eval(now->lft) != eval(now->rgt));
383 
	case    EQ: return (eval(now->lft) == eval(now->rgt));
384 
	case    OR: return (eval(now->lft) || eval(now->rgt));
385 
	case   AND: return (eval(now->lft) && eval(now->rgt));
386 
	case LSHIFT: return (eval(now->lft) << eval(now->rgt));
387 
	case RSHIFT: return (eval(now->lft) >> eval(now->rgt));
388 
	case   '?': return (eval(now->lft) ? eval(now->rgt->lft)
389 
					   : eval(now->rgt->rgt));
390 
 
391 
	case     'p': return remotevar(now);	/* _p for remote reference */
392 
	case     'q': return remotelab(now);
393 
	case     'R': return qrecv(now, 0);	/* test only    */
394 
	case     LEN: return qlen(now);
395 
	case    FULL: return (qfull(now));
396 
	case   EMPTY: return (qlen(now)==0);
397 
	case   NFULL: return (!qfull(now));
398 
	case  NEMPTY: return (qlen(now)>0);
399 
	case ENABLED: if (s_trail) return 1;
400 
		      return pc_enabled(now->lft);
401 
	case    EVAL: return eval(now->lft);
402 
	case  PC_VAL: return pc_value(now->lft);
403 
	case NONPROGRESS: return nonprogress();
404 
	case    NAME: return getval(now);
405 
 
406 
	case TIMEOUT: return Tval;
407 
	case     RUN: return TstOnly?1:enable(now);
408 
 
409 
	case   's': return qsend(now);		/* send         */
410 
	case   'r': return qrecv(now, 1);	/* receive or poll */
411 
	case   'c': return eval(now->lft);	/* condition    */
412 
	case PRINT: return TstOnly?1:interprint(stdout, now);
413 
	case PRINTM: return TstOnly?1:printm(stdout, now);
414 
	case  ASGN: return assign(now);
415 
 
416 
	case C_CODE: if (!analyze)
417 
		     {	printf("%s:\t", now->sym->name);
418 
		     	plunk_inline(stdout, now->sym->name, 0, 1);
419 
		     }
420 
		     return 1; /* uninterpreted */
421 
 
422 
	case C_EXPR: if (!analyze)
423 
		     {	printf("%s:\t", now->sym->name);
424 
		     	plunk_expr(stdout, now->sym->name);
425 
		     	printf("\n");
426 
		     }
427 
		     return 1; /* uninterpreted */
428 
 
429 
	case ASSERT: if (TstOnly || eval(now->lft)) return 1;
430 
		     non_fatal("assertion violated", (char *) 0);
431 
			printf("spin: text of failed assertion: assert(");
432 
			comment(stdout, now->lft, 0);
433 
			printf(")\n");
434 
		     if (s_trail && !xspin) return 1;
435 
		     wrapup(1); /* doesn't return */
436 
 
437 
	case  IF: case DO: case BREAK: case UNLESS:	/* compound */
438 
	case   '.': return 1;	/* return label for compound */
439 
	case   '@': return 0;	/* stop state */
440 
	case  ELSE: return 1;	/* only hit here in guided trails */
441 
	default   : printf("spin: bad node type %d (run)\n", now->ntyp);
442 
		    if (s_trail) printf("spin: trail file doesn't match spec?\n");
443 
		    fatal("aborting", 0);
444 
	}}
445 
	return 0;
446 
}
447 
 
448 
int
449 
printm(FILE *fd, Lextok *n)
450 
{	extern char Buf[];
451 
	int j;
452 
 
453 
	Buf[0] = '\0';
454 
	if (!no_print)
455 
	if (!s_trail || depth >= jumpsteps) {
456 
		if (n->lft->ismtyp)
457 
			j = n->lft->val;
458 
		else
459 
			j = eval(n->lft);
460 
		sr_buf(j, 1);
461 
		dotag(fd, Buf);
462 
	}
463 
	return 1;
464 
}
465 
 
466 
int
467 
interprint(FILE *fd, Lextok *n)
468 
{	Lextok *tmp = n->lft;
469 
	char c, *s = n->sym->name;
470 
	int i, j; char lbuf[512]; /* matches value in sr_buf() */
471 
	extern char Buf[];	/* global, size 4096 */
472 
	char tBuf[4096];	/* match size of global Buf[] */
473 
 
474 
	Buf[0] = '\0';
475 
	if (!no_print)
476 
	if (!s_trail || depth >= jumpsteps) {
477 
	for (i = 0; i < (int) strlen(s); i++)
478 
		switch (s[i]) {
479 
		case '\"': break; /* ignore */
480 
		case '\\':
481 
			 switch(s[++i]) {
482 
			 case 't': strcat(Buf, "\t"); break;
483 
			 case 'n': strcat(Buf, "\n"); break;
484 
			 default:  goto onechar;
485 
			 }
486 
			 break;
487 
		case  '%':
488 
			 if ((c = s[++i]) == '%')
489 
			 {	strcat(Buf, "%"); /* literal */
490 
				break;
491 
			 }
492 
			 if (!tmp)
493 
			 {	non_fatal("too few print args %s", s);
494 
				break;
495 
			 }
496 
			 j = eval(tmp->lft);
497 
			 tmp = tmp->rgt;
498 
			 switch(c) {
499 
			 case 'c': sprintf(lbuf, "%c", j); break;
500 
			 case 'd': sprintf(lbuf, "%d", j); break;
501 
 
502 
			 case 'e': strcpy(tBuf, Buf);	/* event name */
503 
				   Buf[0] = '\0';
504 
				   sr_buf(j, 1);
505 
				   strcpy(lbuf, Buf);
506 
				   strcpy(Buf, tBuf);
507 
				   break;
508 
 
509 
			 case 'o': sprintf(lbuf, "%o", j); break;
510 
			 case 'u': sprintf(lbuf, "%u", (unsigned) j); break;
511 
			 case 'x': sprintf(lbuf, "%x", j); break;
512 
			 default:  non_fatal("bad print cmd: '%s'", &s[i-1]);
513 
				   lbuf[0] = '\0'; break;
514 
			 }
515 
			 goto append;
516 
		default:
517 
onechar:		 lbuf[0] = s[i]; lbuf[1] = '\0';
518 
append:			 strcat(Buf, lbuf);
519 
			 break;
520 
		}
521 
		dotag(fd, Buf);
522 
	}
523 
	if (strlen(Buf) >= 4096) fatal("printf string too long", 0);
524 
	return 1;
525 
}
526 
 
527 
static int
528 
Enabled1(Lextok *n)
529 
{	int i; int v = verbose;
530 
 
531 
	if (n)
532 
	switch (n->ntyp) {
533 
	case 'c':
534 
		if (has_typ(n->lft, RUN))
535 
			return 1;	/* conservative */
536 
		/* else fall through */
537 
	default:	/* side-effect free */
538 
		verbose = 0;
539 
		E_Check++;
540 
		i = eval(n);
541 
		E_Check--;
542 
		verbose = v;
543 
		return i;
544 
 
545 
	case C_CODE: case C_EXPR:
546 
	case PRINT: case PRINTM:
547 
	case   ASGN: case ASSERT:
548 
		return 1;
549 
 
550 
	case 's':
551 
		if (q_is_sync(n))
552 
		{	if (Rvous) return 0;
553 
			TstOnly = 1; verbose = 0;
554 
			E_Check++;
555 
			i = eval(n);
556 
			E_Check--;
557 
			TstOnly = 0; verbose = v;
558 
			return i;
559 
		}
560 
		return (!qfull(n));
561 
	case 'r':
562 
		if (q_is_sync(n))
563 
			return 0;	/* it's never a user-choice */
564 
		n->ntyp = 'R'; verbose = 0;
565 
		E_Check++;
566 
		i = eval(n);
567 
		E_Check--;
568 
		n->ntyp = 'r'; verbose = v;
569 
		return i;
570 
	}
571 
	return 0;
572 
}
573 
 
574 
int
575 
Enabled0(Element *e)
576 
{	SeqList *z;
577 
 
578 
	if (!e || !e->n)
579 
		return 0;
580 
 
581 
	switch (e->n->ntyp) {
582 
	case '@':
583 
		return X->pid == (nproc-nstop-1);
584 
	case '.':
585 
		return 1;
586 
	case GOTO:
587 
		if (Rvous) return 0;
588 
		return 1;
589 
	case UNLESS:
590 
		return Enabled0(e->sub->this->frst);
591 
	case ATOMIC:
592 
	case D_STEP:
593 
	case NON_ATOMIC:
594 
		return Enabled0(e->n->sl->this->frst);
595 
	}
596 
	if (e->sub)	/* true for IF, DO, and UNLESS */
597 
	{	for (z = e->sub; z; z = z->nxt)
598 
			if (Enabled0(z->this->frst))
599 
				return 1;
600 
		return 0;
601 
	}
602 
	for (z = e->esc; z; z = z->nxt)
603 
	{	if (Enabled0(z->this->frst))
604 
			return 1;
605 
	}
606 
#if 0
607 
	printf("enabled1 ");
608 
	comment(stdout, e->n, 0);
609 
	printf(" ==> %s\n", Enabled1(e->n)?"yes":"nope");
610 
#endif
611 
	return Enabled1(e->n);
612 
}
613 
 
614 
int
615 
pc_enabled(Lextok *n)
616 
{	int i = nproc - nstop;
617 
	int pid = eval(n);
618 
	int result = 0;
619 
	RunList *Y, *oX;
620 
 
621 
	if (pid == X->pid)
622 
		fatal("used: enabled(pid=thisproc) [%s]", X->n->name);
623 
 
624 
	for (Y = run; Y; Y = Y->nxt)
625 
		if (--i == pid)
626 
		{	oX = X; X = Y;
627 
			result = Enabled0(Y->pc);
628 
			X = oX;
629 
			break;
630 
		}
631 
	return result;
632 
}
633