/***** spin: run.c *****//* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     *//* All Rights Reserved.  This software is for educational purposes only.  *//* No guarantee whatsoever is expressed or implied by the distribution of *//* this code.  Permission is given to distribute this code provided that  *//* this introductory message is not removed and no monies are exchanged.  *//* Software written by Gerard J. Holzmann.  For tool documentation see:   *//*             http://spinroot.com/                                       *//* Send all bug-reports and/or questions to: bugs@spinroot.com            */#include <stdlib.h>#include "spin.h"#include "y.tab.h"extern RunList	*X, *run;extern Symbol	*Fname;extern Element	*LastStep;extern int	Rvous, lineno, Tval, interactive, MadeChoice;extern int	TstOnly, verbose, s_trail, xspin, jumpsteps, depth;extern int	nproc, nstop, no_print, like_java;static long	Seed = 1;static int	E_Check = 0, Escape_Check = 0;static int	eval_sync(Element *);static int	pc_enabled(Lextok *n);extern void	sr_buf(int, int);voidSrand(unsigned int s){	Seed = s;}longRand(void){	/* CACM 31(10), Oct 1988 */	Seed = 16807*(Seed%127773) - 2836*(Seed/127773);	if (Seed <= 0) Seed += 2147483647;	return Seed;}Element *rev_escape(SeqList *e){	Element *r;	if (!e)		return (Element *) 0;	if ((r = rev_escape(e->nxt)) != ZE) /* reversed order */		return r;	return eval_sub(e->this->frst);		}Element *eval_sub(Element *e){	Element *f, *g;	SeqList *z;	int i, j, k;	if (!e || !e->n)		return ZE;#ifdef DEBUG	printf("\n\teval_sub(%d %s: line %d) ",		e->Seqno, e->esc?"+esc":"", e->n?e->n->ln:0);	comment(stdout, e->n, 0);	printf("\n");#endif	if (e->n->ntyp == GOTO)	{	if (Rvous) return ZE;		LastStep = e;		f = get_lab(e->n, 1);		cross_dsteps(e->n, f->n);		return f;	}	if (e->n->ntyp == UNLESS)	{	/* escapes were distributed into sequence */		return eval_sub(e->sub->this->frst);	} else if (e->sub)	/* true for IF, DO, and UNLESS */	{	Element *has_else = ZE;		Element *bas_else = ZE;		int nr_else = 0, nr_choices = 0;		if (interactive		&& !MadeChoice && !E_Check		&& !Escape_Check		&& !(e->status&(D_ATOM))		&& depth >= jumpsteps)		{	printf("Select stmnt (");			whoruns(0); printf(")\n");			if (nproc-nstop > 1)			printf("\tchoice 0: other process\n");		}		for (z = e->sub, j=0; z; z = z->nxt)		{	j++;			if (interactive			&& !MadeChoice && !E_Check			&& !Escape_Check			&& !(e->status&(D_ATOM))			&& depth >= jumpsteps			&& z->this->frst			&& (xspin || (verbose&32) || Enabled0(z->this->frst)))			{	if (z->this->frst->n->ntyp == ELSE)				{	has_else = (Rvous)?ZE:z->this->frst->nxt;					nr_else = j;					continue;				}				printf("\tchoice %d: ", j);#if 0				if (z->this->frst->n)					printf("line %d, ", z->this->frst->n->ln);#endif				if (!Enabled0(z->this->frst))					printf("unexecutable, ");				else					nr_choices++;				comment(stdout, z->this->frst->n, 0);				printf("\n");		}	}		if (nr_choices == 0 && has_else)			printf("\tchoice %d: (else)\n", nr_else);		if (interactive && depth >= jumpsteps		&& !Escape_Check		&& !(e->status&(D_ATOM))		&& !E_Check)		{	if (!MadeChoice)			{	char buf[256];				if (xspin)					printf("Make Selection %d\n\n", j);				else					printf("Select [0-%d]: ", j);				fflush(stdout);				scanf("%64s", buf);				if (isdigit(buf[0]))					k = atoi(buf);				else				{	if (buf[0] == 'q')						alldone(0);					k = -1;				}			} else			{	k = MadeChoice;				MadeChoice = 0;			}			if (k < 1 || k > j)			{	if (k != 0) printf("\tchoice outside range\n");				return ZE;			}			k--;		} else		{	if (e->n && e->n->indstep >= 0)				k = 0;	/* select 1st executable guard */			else				k = Rand()%j;	/* nondeterminism */		}		has_else = ZE;		bas_else = ZE;		for (i = 0, z = e->sub; i < j+k; i++)		{	if (z->this->frst			&&  z->this->frst->n->ntyp == ELSE)			{	bas_else = z->this->frst;				has_else = (Rvous)?ZE:bas_else->nxt;				if (!interactive || depth < jumpsteps				|| Escape_Check				|| (e->status&(D_ATOM)))				{	z = (z->nxt)?z->nxt:e->sub;					continue;				}			}			if (z->this->frst			&&  ((z->this->frst->n->ntyp == ATOMIC			  ||  z->this->frst->n->ntyp == D_STEP)			  &&  z->this->frst->n->sl->this->frst->n->ntyp == ELSE))			{	bas_else = z->this->frst->n->sl->this->frst;				has_else = (Rvous)?ZE:bas_else->nxt;				if (!interactive || depth < jumpsteps				|| Escape_Check				|| (e->status&(D_ATOM)))				{	z = (z->nxt)?z->nxt:e->sub;					continue;				}			}			if (i >= k)			{	if ((f = eval_sub(z->this->frst)) != ZE)					return f;				else if (interactive && depth >= jumpsteps				&& !(e->status&(D_ATOM)))				{	if (!E_Check && !Escape_Check)						printf("\tunexecutable\n");					return ZE;			}	}			z = (z->nxt)?z->nxt:e->sub;		}		LastStep = bas_else;		return has_else;	} else	{	if (e->n->ntyp == ATOMIC		||  e->n->ntyp == D_STEP)		{	f = e->n->sl->this->frst;			g = e->n->sl->this->last;			g->nxt = e->nxt;			if (!(g = eval_sub(f)))	/* atomic guard */				return ZE;			return g;		} else if (e->n->ntyp == NON_ATOMIC)		{	f = e->n->sl->this->frst;			g = e->n->sl->this->last;			g->nxt = e->nxt;		/* close it */			return eval_sub(f);		} else if (e->n->ntyp == '.')		{	if (!Rvous) return e->nxt;			return eval_sub(e->nxt);		} else		{	SeqList *x;			if (!(e->status & (D_ATOM))			&&  e->esc && verbose&32)			{	printf("Stmnt [");				comment(stdout, e->n, 0);				printf("] has escape(s): ");				for (x = e->esc; x; x = x->nxt)				{	printf("[");					g = x->this->frst;					if (g->n->ntyp == ATOMIC					||  g->n->ntyp == NON_ATOMIC)						g = g->n->sl->this->frst;					comment(stdout, g->n, 0);					printf("] ");				}				printf("\n");			}#if 0			if (!(e->status & D_ATOM))	/* escapes don't reach inside d_steps */			/* 4.2.4: only the guard of a d_step can have an escape */#endif			{	Escape_Check++;				if (like_java)				{	if ((g = rev_escape(e->esc)) != ZE)					{	if (verbose&4)							printf("\tEscape taken\n");						Escape_Check--;						return g;					}				} else				{	for (x = e->esc; x; x = x->nxt)					{	if ((g = eval_sub(x->this->frst)) != ZE)						{	if (verbose&4)								printf("\tEscape taken\n");							Escape_Check--;							return g;				}	}	}				Escape_Check--;			}					switch (e->n->ntyp) {			case TIMEOUT: case RUN:			case PRINT: case PRINTM:			case C_CODE: case C_EXPR:			case ASGN: case ASSERT:			case 's': case 'r': case 'c':				/* toplevel statements only */				LastStep = e;			default:				break;			}			if (Rvous)			{				return (eval_sync(e))?e->nxt:ZE;			}			return (eval(e->n))?e->nxt:ZE;		}	}	return ZE; /* not reached */}static inteval_sync(Element *e){	/* allow only synchronous receives	   and related node types    */	Lextok *now = (e)?e->n:ZN;	if (!now	||  now->ntyp != 'r'	||  now->val >= 2	/* no rv with a poll */	||  !q_is_sync(now))	{		return 0;	}	LastStep = e;	return eval(now);}static intassign(Lextok *now){	int t;	if (TstOnly) return 1;	switch (now->rgt->ntyp) {	case FULL:	case NFULL:	case EMPTY:	case NEMPTY:	case RUN:	case LEN:		t = BYTE;		break;	default:		t = Sym_typ(now->rgt);		break;	}	typ_ck(Sym_typ(now->lft), t, "assignment"); 	return setval(now->lft, eval(now->rgt));}static intnonprogress(void)	/* np_ */{	RunList	*r;	for (r = run; r; r = r->nxt)	{	if (has_lab(r->pc, 4))	/* 4=progress */			return 0;	}	return 1;}inteval(Lextok *now){	if (now) {	lineno = now->ln;	Fname  = now->fn;#ifdef DEBUG	printf("eval ");	comment(stdout, now, 0);	printf("\n");#endif	switch (now->ntyp) {	case CONST: return now->val;	case   '!': return !eval(now->lft);	case  UMIN: return -eval(now->lft);	case   '~': return ~eval(now->lft);	case   '/': return (eval(now->lft) / eval(now->rgt));	case   '*': return (eval(now->lft) * eval(now->rgt));	case   '-': return (eval(now->lft) - eval(now->rgt));	case   '+': return (eval(now->lft) + eval(now->rgt));	case   '%': return (eval(now->lft) % eval(now->rgt));	case    LT: return (eval(now->lft) <  eval(now->rgt));	case    GT: return (eval(now->lft) >  eval(now->rgt));	case   '&': return (eval(now->lft) &  eval(now->rgt));	case   '^': return (eval(now->lft) ^  eval(now->rgt));	case   '|': return (eval(now->lft) |  eval(now->rgt));	case    LE: return (eval(now->lft) <= eval(now->rgt));	case    GE: return (eval(now->lft) >= eval(now->rgt));	case    NE: return (eval(now->lft) != eval(now->rgt));	case    EQ: return (eval(now->lft) == eval(now->rgt));	case    OR: return (eval(now->lft) || eval(now->rgt));	case   AND: return (eval(now->lft) && eval(now->rgt));	case LSHIFT: return (eval(now->lft) << eval(now->rgt));	case RSHIFT: return (eval(now->lft) >> eval(now->rgt));	case   '?': return (eval(now->lft) ? eval(now->rgt->lft)					   : eval(now->rgt->rgt));	case     'p': return remotevar(now);	/* _p for remote reference */	case     'q': return remotelab(now);	case     'R': return qrecv(now, 0);	/* test only    */	case     LEN: return qlen(now);	case    FULL: return (qfull(now));	case   EMPTY: return (qlen(now)==0);	case   NFULL: return (!qfull(now));	case  NEMPTY: return (qlen(now)>0);	case ENABLED: if (s_trail) return 1;		      return pc_enabled(now->lft);	case    EVAL: return eval(now->lft);	case  PC_VAL: return pc_value(now->lft);	case NONPROGRESS: return nonprogress();	case    NAME: return getval(now);	case TIMEOUT: return Tval;	case     RUN: return TstOnly?1:enable(now);	case   's': return qsend(now);		/* send         */	case   'r': return qrecv(now, 1);	/* receive or poll */	case   'c': return eval(now->lft);	/* condition    */	case PRINT: return TstOnly?1:interprint(stdout, now);	case PRINTM: return TstOnly?1:printm(stdout, now);	case  ASGN: return assign(now);	case C_CODE: printf("%s:\t", now->sym->name);		     plunk_inline(stdout, now->sym->name, 0);		     return 1; /* uninterpreted */	case C_EXPR: printf("%s:\t", now->sym->name);		     plunk_expr(stdout, now->sym->name);		     printf("\n");		     return 1; /* uninterpreted */	case ASSERT: if (TstOnly || eval(now->lft)) return 1;		     non_fatal("assertion violated", (char *) 0);			printf("spin: text of failed assertion: assert(");			comment(stdout, now->lft, 0);			printf(")\n");		     if (s_trail && !xspin) return 1;		     wrapup(1); /* doesn't return */	case  IF: case DO: case BREAK: case UNLESS:	/* compound */	case   '.': return 1;	/* return label for compound */	case   '@': return 0;	/* stop state */	case  ELSE: return 1;	/* only hit here in guided trails */	default   : printf("spin: bad node type %d (run)\n", now->ntyp);		    if (s_trail) printf("spin: trail file doesn't match spec?\n");		    fatal("aborting", 0);	}}	return 0;}intprintm(FILE *fd, Lextok *n){	extern char Buf[];	int j;	Buf[0] = '\0';	if (!no_print)	if (!s_trail || depth >= jumpsteps) {		if (n->lft->ismtyp)			j = n->lft->val;		else			j = eval(n->lft);		sr_buf(j, 1);		dotag(fd, Buf);	}	return 1;}intinterprint(FILE *fd, Lextok *n){	Lextok *tmp = n->lft;	char c, *s = n->sym->name;	int i, j; char lbuf[512]; /* matches value in sr_buf() */	extern char Buf[];	/* global, size 4096 */	char tBuf[4096];	/* match size of global Buf[] */	Buf[0] = '\0';	if (!no_print)	if (!s_trail || depth >= jumpsteps) {	for (i = 0; i < (int) strlen(s); i++)		switch (s[i]) {		case '\"': break; /* ignore */		case '\\':			 switch(s[++i]) {			 case 't': strcat(Buf, "\t"); break;			 case 'n': strcat(Buf, "\n"); break;			 default:  goto onechar;			 }			 break;		case  '%':			 if ((c = s[++i]) == '%')			 {	strcat(Buf, "%"); /* literal */				break;			 }			 if (!tmp)			 {	non_fatal("too few print args %s", s);				break;			 }			 j = eval(tmp->lft);			 tmp = tmp->rgt;			 switch(c) {			 case 'c': sprintf(lbuf, "%c", j); break;			 case 'd': sprintf(lbuf, "%d", j); break;			 case 'e': strcpy(tBuf, Buf);	/* event name */				   Buf[0] = '\0';				   sr_buf(j, 1);				   strcpy(lbuf, Buf);				   strcpy(Buf, tBuf);				   break;			 case 'o': sprintf(lbuf, "%o", j); break;			 case 'u': sprintf(lbuf, "%u", (unsigned) j); break;			 case 'x': sprintf(lbuf, "%x", j); break;			 default:  non_fatal("bad print cmd: '%s'", &s[i-1]);				   lbuf[0] = '\0'; break;			 }			 goto append;		default:onechar:		 lbuf[0] = s[i]; lbuf[1] = '\0';append:			 strcat(Buf, lbuf);			 break;		}		dotag(fd, Buf);	}	if (strlen(Buf) >= 4096) fatal("printf string too long", 0);	return 1;}static intEnabled1(Lextok *n){	int i; int v = verbose;	if (n)	switch (n->ntyp) {	case 'c':		if (has_typ(n->lft, RUN))			return 1;	/* conservative */		/* else fall through */	default:	/* side-effect free */		verbose = 0;		E_Check++;		i = eval(n);		E_Check--;		verbose = v;		return i;	case C_CODE: case C_EXPR:	case PRINT: case PRINTM:	case   ASGN: case ASSERT:		return 1;	case 's':		if (q_is_sync(n))		{	if (Rvous) return 0;			TstOnly = 1; verbose = 0;			E_Check++;			i = eval(n);			E_Check--;			TstOnly = 0; verbose = v;			return i;		}		return (!qfull(n));	case 'r':		if (q_is_sync(n))			return 0;	/* it's never a user-choice */		n->ntyp = 'R'; verbose = 0;		E_Check++;		i = eval(n);		E_Check--;		n->ntyp = 'r'; verbose = v;		return i;	}	return 0;}intEnabled0(Element *e){	SeqList *z;	if (!e || !e->n)		return 0;	switch (e->n->ntyp) {	case '@':		return X->pid == (nproc-nstop-1);	case '.':		return 1;	case GOTO:		if (Rvous) return 0;		return 1;	case UNLESS:		return Enabled0(e->sub->this->frst);	case ATOMIC:	case D_STEP:	case NON_ATOMIC:		return Enabled0(e->n->sl->this->frst);	}	if (e->sub)	/* true for IF, DO, and UNLESS */	{	for (z = e->sub; z; z = z->nxt)			if (Enabled0(z->this->frst))				return 1;		return 0;	}	for (z = e->esc; z; z = z->nxt)	{	if (Enabled0(z->this->frst))			return 1;	}#if 0	printf("enabled1 ");	comment(stdout, e->n, 0);	printf(" ==> %s\n", Enabled1(e->n)?"yes":"nope");#endif	return Enabled1(e->n);}intpc_enabled(Lextok *n){	int i = nproc - nstop;	int pid = eval(n);	int result = 0;	RunList *Y, *oX;	if (pid == X->pid)		fatal("used: enabled(pid=thisproc) [%s]", X->n->name);	for (Y = run; Y; Y = Y->nxt)		if (--i == pid)		{	oX = X; X = Y;			result = Enabled0(Y->pc);			X = oX;			break;		}	return result;}