/***** spin: dstep.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 "spin.h"#include "y.tab.h" #define MAXDSTEP	2048	/* was 512 */ char	*NextLab[64];int	Level=0, GenCode=0, IsGuard=0, TestOnly=0; static int	Tj=0, Jt=0, LastGoto=0;static int	Tojump[MAXDSTEP], Jumpto[MAXDSTEP], Special[MAXDSTEP];static void	putCode(FILE *, Element *, Element *, Element *, int); extern int	Pid, separate, OkBreak; static voidSourced(int n, int special){	int i;	for (i = 0; i < Tj; i++)		if (Tojump[i] == n)			return;	if (Tj >= MAXDSTEP)		fatal("d_step sequence too long", (char *)0);	Special[Tj] = special;	Tojump[Tj++] = n;} static voidDested(int n){	int i;	for (i = 0; i < Tj; i++)		if (Tojump[i] == n)			return;	for (i = 0; i < Jt; i++)		if (Jumpto[i] == n)			return;	if (Jt >= MAXDSTEP)		fatal("d_step sequence too long", (char *)0);	Jumpto[Jt++] = n;	LastGoto = 1;} static voidMopup(FILE *fd){	int i, j; 	for (i = 0; i < Jt; i++)	{	for (j = 0; j < Tj; j++)			if (Tojump[j] == Jumpto[i])				break;		if (j == Tj)		{	char buf[16];			if (Jumpto[i] == OkBreak)			{	if (!LastGoto)				fprintf(fd, "S_%.3d_0:	/* break-dest */\n",					OkBreak);			} else {				sprintf(buf, "S_%.3d_0", Jumpto[i]);				non_fatal("goto %s breaks from d_step seq", buf);	}	}	}	for (j = 0; j < Tj; j++)	{	for (i = 0; i < Jt; i++)			if (Tojump[j] == Jumpto[i])				break;#ifdef DEBUG		if (i == Jt && !Special[i])			fprintf(fd, "\t\t/* no goto's to S_%.3d_0 */\n",			Tojump[j]);#endif	}	for (j = i = 0; j < Tj; j++)		if (Special[j])		{	Tojump[i] = Tojump[j];			Special[i] = 2;			if (i >= MAXDSTEP)			fatal("cannot happen (dstep.c)", (char *)0);			i++;		}	Tj = i;	/* keep only the global exit-labels */	Jt = 0;} static intFirstTime(int n){	int i;	for (i = 0; i < Tj; i++)		if (Tojump[i] == n)			return (Special[i] <= 1);	return 1;} static voidillegal(Element *e, char *str){	printf("illegal operator in 'd_step:' '");	comment(stdout, e->n, 0);	printf("'\n");	fatal("'%s'", str);} static voidfilterbad(Element *e){	switch (e->n->ntyp) {	case ASSERT:	case PRINT:	case 'c':		/* run cannot be completely undone		 * with sv_save-sv_restor		 */		if (any_oper(e->n->lft, RUN))			illegal(e, "run operator in d_step"); 		/* remote refs inside d_step sequences		 * would be okay, but they cannot always		 * be interpreted by the simulator the		 * same as by the verifier (e.g., for an		 * error trail)		 */		if (any_oper(e->n->lft, 'p'))			illegal(e, "remote reference in d_step");		break;	case '@':		illegal(e, "process termination");		break;	case D_STEP:		illegal(e, "nested d_step sequence");		break;	case ATOMIC:		illegal(e, "nested atomic sequence");		break;	default:		break;	}} static intCollectGuards(FILE *fd, Element *e, int inh){	SeqList *h; Element *ee; 	for (h = e->sub; h; h = h->nxt)	{	ee = huntstart(h->this->frst);		filterbad(ee);		switch (ee->n->ntyp) {		case NON_ATOMIC:			inh += CollectGuards(fd, ee->n->sl->this->frst, inh);			break;		case  IF:			inh += CollectGuards(fd, ee, inh);			break;		case '.':			if (ee->nxt->n->ntyp == DO)				inh += CollectGuards(fd, ee->nxt, inh);			break;		case ELSE:			if (inh++ > 0) fprintf(fd, " || ");/* 4.2.5 */		if (!pid_is_claim(Pid))				fprintf(fd, "(boq == -1 /* else */)");			else				fprintf(fd, "(1 /* else */)");			break;		case 'R':			if (inh++ > 0) fprintf(fd, " || ");			fprintf(fd, "("); TestOnly=1;			putstmnt(fd, ee->n, ee->seqno);			fprintf(fd, ")"); TestOnly=0;			break;		case 'r':			if (inh++ > 0) fprintf(fd, " || ");			fprintf(fd, "("); TestOnly=1;			putstmnt(fd, ee->n, ee->seqno);			fprintf(fd, ")"); TestOnly=0;			break;		case 's':			if (inh++ > 0) fprintf(fd, " || ");			fprintf(fd, "("); TestOnly=1;/* 4.2.1 */		if (!pid_is_claim(Pid)) fprintf(fd, "(boq == -1) && ");			putstmnt(fd, ee->n, ee->seqno);			fprintf(fd, ")"); TestOnly=0;			break;		case 'c':			if (inh++ > 0) fprintf(fd, " || ");			fprintf(fd, "("); TestOnly=1;			if (!pid_is_claim(Pid))				fprintf(fd, "(boq == -1 && ");			putstmnt(fd, ee->n->lft, e->seqno);			if (!pid_is_claim(Pid))				fprintf(fd, ")");			fprintf(fd, ")"); TestOnly=0;			break;	}	}	return inh;} intputcode(FILE *fd, Sequence *s, Element *nxt, int justguards, int ln, int seqno){	int isg=0; char buf[64]; 	NextLab[0] = "continue";	filterbad(s->frst); 	switch (s->frst->n->ntyp) {	case UNLESS:		non_fatal("'unless' inside d_step - ignored", (char *) 0);		return putcode(fd, s->frst->n->sl->this, nxt, 0, ln, seqno);	case NON_ATOMIC:		(void) putcode(fd, s->frst->n->sl->this, ZE, 1, ln, seqno);		break;	case IF:		fprintf(fd, "if (!(");		if (!CollectGuards(fd, s->frst, 0))	/* what about boq? */			fprintf(fd, "1");		fprintf(fd, "))\n\t\t\tcontinue;");		isg = 1;		break;	case '.':		if (s->frst->nxt->n->ntyp == DO)		{	fprintf(fd, "if (!(");			if (!CollectGuards(fd, s->frst->nxt, 0))				fprintf(fd, "1");			fprintf(fd, "))\n\t\t\tcontinue;");			isg = 1;		}		break;	case 'R': /* <- can't really happen (it's part of a 'c') */		fprintf(fd, "if (!("); TestOnly=1;		putstmnt(fd, s->frst->n, s->frst->seqno);		fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;		break;	case 'r':		fprintf(fd, "if (!("); TestOnly=1;		putstmnt(fd, s->frst->n, s->frst->seqno);		fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;		break;	case 's':		fprintf(fd, "if (");#if 1/* 4.2.1 */	if (!pid_is_claim(Pid)) fprintf(fd, "(boq != -1) || ");#endif		fprintf(fd, "!("); TestOnly=1;		putstmnt(fd, s->frst->n, s->frst->seqno);		fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;		break;	case 'c':		fprintf(fd, "if (!(");		if (!pid_is_claim(Pid)) fprintf(fd, "boq == -1 && ");		TestOnly=1;		putstmnt(fd, s->frst->n->lft, s->frst->seqno);		fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;		break;	case ELSE:		fprintf(fd, "if (boq != -1 || (");		if (separate != 2) fprintf(fd, "trpt->");		fprintf(fd, "o_pm&1))\n\t\t\tcontinue;");		break;	case ASGN:	/* new 3.0.8 */		fprintf(fd, "IfNotBlocked");		break;	}	if (justguards) return 0; 	fprintf(fd, "\n\t\tsv_save();\n\t\t");#if 1	fprintf(fd, "reached[%d][%d] = 1;\n\t\t", Pid, seqno);	fprintf(fd, "reached[%d][t->st] = 1;\n\t\t", Pid);	/* true next state */	fprintf(fd, "reached[%d][tt] = 1;\n", Pid);		/* true current state */#endif	sprintf(buf, "Uerror(\"block in d_step seq, line %d\")", ln);	NextLab[0] = buf;	putCode(fd, s->frst, s->extent, nxt, isg); 	if (nxt)	{	extern Symbol *Fname;		extern int lineno; 		if (FirstTime(nxt->Seqno)		&& (!(nxt->status & DONE2) || !(nxt->status & D_ATOM)))		{	fprintf(fd, "S_%.3d_0: /* 1 */\n", nxt->Seqno);			nxt->status |= DONE2;			LastGoto = 0;		}		Sourced(nxt->Seqno, 1);		lineno = ln;		Fname = nxt->n->fn;			Mopup(fd);	}	unskip(s->frst->seqno);	return LastGoto;} static voidputCode(FILE *fd, Element *f, Element *last, Element *next, int isguard){	Element *e, *N;	SeqList *h; int i;	char NextOpt[64];	static int bno = 0; 	for (e = f; e; e = e->nxt)	{	if (e->status & DONE2)			continue;		e->status |= DONE2; 		if (!(e->status & D_ATOM))		{	if (!LastGoto)			{	fprintf(fd, "\t\tgoto S_%.3d_0;\n",					e->Seqno);				Dested(e->Seqno);			}			break;		}		fprintf(fd, "S_%.3d_0: /* 2 */\n", e->Seqno);		LastGoto = 0;		Sourced(e->Seqno, 0); 		if (!e->sub)		{	filterbad(e);			switch (e->n->ntyp) {			case NON_ATOMIC:				h = e->n->sl;				putCode(fd, h->this->frst,					h->this->extent, e->nxt, 0);				break;			case BREAK:				if (LastGoto) break;				if (e->nxt)				{	i = target( huntele(e->nxt,						e->status, -1))->Seqno;					fprintf(fd, "\t\tgoto S_%.3d_0;	", i);					fprintf(fd, "/* 'break' */\n");					Dested(i);				} else				{	if (next)					{	fprintf(fd, "\t\tgoto S_%.3d_0;",							next->Seqno);						fprintf(fd, " /* NEXT */\n");						Dested(next->Seqno);					} else					fatal("cannot interpret d_step", 0);				}				break;			case GOTO:				if (LastGoto) break;				i = huntele( get_lab(e->n,1),					e->status, -1)->Seqno;				fprintf(fd, "\t\tgoto S_%.3d_0;	", i);				fprintf(fd, "/* 'goto' */\n");				Dested(i);				break;			case '.':				if (LastGoto) break;				if (e->nxt && (e->nxt->status & DONE2))				{	i = e->nxt?e->nxt->Seqno:0;					fprintf(fd, "\t\tgoto S_%.3d_0;", i);					fprintf(fd, " /* '.' */\n");					Dested(i);				}				break;			default:				putskip(e->seqno);				GenCode = 1; IsGuard = isguard;				fprintf(fd, "\t\t");				putstmnt(fd, e->n, e->seqno);				fprintf(fd, ";\n");				GenCode = IsGuard = isguard = LastGoto = 0;				break;			}			i = e->nxt?e->nxt->Seqno:0;			if (e->nxt && e->nxt->status & DONE2 && !LastGoto)			{	fprintf(fd, "\t\tgoto S_%.3d_0; ", i);				fprintf(fd, "/* ';' */\n");				Dested(i);				break;			}		} else		{	for (h = e->sub, i=1; h; h = h->nxt, i++)			{	sprintf(NextOpt, "goto S_%.3d_%d",					e->Seqno, i);				NextLab[++Level] = NextOpt;				N = (e->n && e->n->ntyp == DO) ? e : e->nxt;				putCode(fd, h->this->frst,					h->this->extent, N, 1);				Level--;				fprintf(fd, "%s: /* 3 */\n", &NextOpt[5]);				LastGoto = 0;			}			if (!LastGoto)			{	fprintf(fd, "\t\tUerror(\"blocking sel ");				fprintf(fd, "in d_step (nr.%d, near line %d)\");\n",				bno++, (e->n)?e->n->ln:0);				LastGoto = 0;			}		}		if (e == last)		{	if (!LastGoto && next)			{	fprintf(fd, "\t\tgoto S_%.3d_0;\n",					next->Seqno);				Dested(next->Seqno);			}			break;	}	}}