Import sources from 2011-03-30 iso image

1 files changed, 411 insertions, 0 deletions

diff --git a/sys/src/cmd/spin/dstep.c b/sys/src/cmd/spin/dstep.c
new file mode 100755
index 000000000..f24860309
--- /dev/null
+++ b/sys/src/cmd/spin/dstep.c
@@ -0,0 +1,411 @@
+/***** 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	1024	/* 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, claimnr, separate, OkBreak;
+
+static void
+Sourced(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 void
+Dested(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 void
+Mopup(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[12];
+			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 int
+FirstTime(int n)
+{	int i;
+	for (i = 0; i < Tj; i++)
+		if (Tojump[i] == n)
+			return (Special[i] <= 1);
+	return 1;
+}
+
+static void
+illegal(Element *e, char *str)
+{
+	printf("illegal operator in 'd_step:' '");
+	comment(stdout, e->n, 0);
+	printf("'\n");
+	fatal("'%s'", str);
+}
+
+static void
+filterbad(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 int
+CollectGuards(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 != claimnr)
+				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 != claimnr) 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 != claimnr)
+				fprintf(fd, "(boq == -1 && ");
+			putstmnt(fd, ee->n->lft, e->seqno);
+			if (Pid != claimnr)
+				fprintf(fd, ")");
+			fprintf(fd, ")"); TestOnly=0;
+			break;
+	}	}
+	return inh;
+}
+
+int
+putcode(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 != claimnr) 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 != claimnr) 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 void
+putCode(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;
+	}	}
+}