/***** spin: pangen2.c *****/

/* Copyright (c) 1991 by AT&T Bell Telephone Laboratories, Inc.
 * All Rights Reserved. This software is for educational purposes only.
 * No part of this source code may be reproduced in any form
 * without explicit written permission from the copyright owner.
 * This software was written by Gerard J. Holzmann, as part of the book
 * ``Design and Validation of Computer Protocols,'' ISBN 0-13-539925-4,
 * Prentice Hall, Englewood Cliffs, NJ, 07632.
 * Send bug-reports to: gerard@research.att.com
 */

#include <stdio.h>
#include "spin.h"
#include "y.tab.h"
#include "pangen2.h"

extern ProcList	*rdy;
extern RunList	*run;
extern Symbol	*Fname;
extern char	*claimproc;
extern int	lineno;
extern int	Mpars;

FILE	*tc, *th, *tt, *tm, *tb;
int	uniq=1;
int	nocast=0;	/* to turn off casts in lvalues */
int	terse=0;	/* terse printing of varnames */
int	nps=0;		/* number of processes */
int	mst=0;		/* max nr of state/process */
int	claimnr = -1;	/* claim process, if any */
int	Pid;		/* proc currently processed */

fproc(s)
	char *s;
{
	ProcList *p;
	int i;

	if (strcmp("_init", s) == 0)
		return 0;
	for (p = rdy, i = 1; p; p = p->nxt, i++)
		if (strcmp(p->n->name, s) == 0)
			return i;
	fatal("proctype %s not found", s);
}

void
gensrc()
{	ProcList *p;
	int i;

	if (!(tc = fopen("pan.c", "w"))		/* main routines */
	||  !(th = fopen("pan.h", "w"))		/* header file   */
	||  !(tt = fopen("pan.t", "w"))		/* transition matrix */
	||  !(tm = fopen("pan.m", "w"))		/* forward  moves */
	||  !(tb = fopen("pan.b", "w")))	/* backward moves */
	{	printf("spin: cannot create pan.[chtmb]\n");
		exit(1);
	}
	fprintf(th, "/*** %s ***/\n", Fname->name);
	fprintf(th, "#define uchar	unsigned char\n");
	if (claimproc)
	{	claimnr = fproc(claimproc);
		fprintf(th, "#define VERI	%d\n",	claimnr);
		fprintf(th, "#define claimline");
		fprintf(th, "	src_ln%d[((P0 *)pptr(1))->_p]\n",
							claimnr);
	}
	fprintf(th, "#define endclaim	endstate%d\n",	claimnr);
	ntimes(tc, 0, 1, Preamble);

	mst = (run)?run->maxseq:0;
	for (p = rdy, i = 1; p; p = p->nxt, i++)
		mst = max(p->s->last->seqno, mst);
	nps = i+1;	/* add progress checker */

	fprintf(tt, "settable()\n{\tTrans *T, *settr();\n\n");
	fprintf(tt, "\ttrans = (Trans ***) ");
	fprintf(tt, "emalloc(%d*sizeof(Trans **));\n", nps);

	fprintf(tm, "	switch (t->forw) {\n");
	fprintf(tm, "	default: Uerror(\"bad forward move\");\n");

	fprintf(tb, "	switch (t->back) {\n");
	fprintf(tb, "	default: Uerror(\"bad return move\");\n");
	fprintf(tb, "	case  0: goto R999; /* nothing to undo */\n");

	if (!run) fatal("no runable process", (char *)0);

	putproc(run->n, run->pc, 0, run->maxseq);
	for (p = rdy, i = 1; p; p = p->nxt, i++)
		putproc(p->n, p->s->frst, i, p->s->last->seqno);
	putprogress(i, 2);
	ntimes(tt, 0, 1, Tail);
	genheader();
	genaddproc();
	genother(i);
	genaddqueue();
	genunio();
}

void
putproc(n, e, i, j)
	Symbol *n;
	Element *e;
{
	Pid = i;
	fprintf(th, "\nshort nstates%d=%d;\t/* %s */\n", i,j+1,n->name);
	fprintf(tm, "\n		 /* PROC %s */\n", n->name);
	fprintf(tb, "\n		 /* PROC %s */\n", n->name);
	fprintf(tt, "\n	/* proctype %d: %s */\n", i, n->name);
	fprintf(tt, "\n	trans[%d] = (Trans **)", i);
	fprintf(tt, " emalloc(%d*sizeof(Trans *));\n\n", j+1);
	putseq(e);
	dumpsrc(j, i);
}

void
putprogress(i, j)	/* loop detector */
{
	fprintf(th, "\nshort nstates%d=%d;\t/* _progress */\n", i, j+1);

	fprintf(tt, "\n	/* proctype %d: _progress */\n", i);
	fprintf(tt, "\n	trans[%d] = (Trans **)", i);
	fprintf(tt, " emalloc(%d*sizeof(Trans *));\n\n", j+1);
	fprintf(tt, "	trans[%d][1]	= settr(1,2,%d,%d);\n",
						i, uniq+1, uniq+1);
	fprintf(tt, "	trans[%d][2]	= settr(1,0,%d,%d);\n",
						i, uniq+2, uniq+2);
	fprintf(tt, "}\n");

	fprintf(tm, "\n		 /* _progress */\n");
	fprintf(tm, "	case %d:	/* progress */\n", uniq+1);
	fprintf(tm, "		IfNotBlocked\n");
	fprintf(tm, "		now._p_t = 1;\n");
	fprintf(tm, "		m = 3; goto P999;\n");
	fprintf(tm, "	case %d:\n", uniq+2);
	fprintf(tm, "		continue;\n");
	fprintf(tm, "	}\n\n");

	fprintf(tb, "\n		 /* _progress */\n");
	fprintf(tb, "	case %d:	/* progress */\n", uniq+1);
	fprintf(tb, "		now._p_t = 0;\n");
	fprintf(tb, "		goto R999;\n");
	fprintf(tb, "	case %d:\n", uniq+2);
	fprintf(tb, "		goto R999;\n");
	fprintf(tb, "	}\n\n");
}

void
putseq(f)
	Element *f;
{
	Element *e;
	SeqList *h;
	int n, a;

	for (e = f; e; e = e->nxt)
	{	if (e->status & DONE) continue;
		e->status |= DONE;
		if (e->n->nval) putsrc(e->n->nval, e->seqno);
		if (e->sub)
		{	fprintf(tt, "\tT = trans[%d][%d] = ",
							Pid, e->seqno);
			fprintf(tt, "settr(%d,0,0,0);", e->status);
			blurb(tt, e->n->ntyp, e->n->nval);
			for (h = e->sub; h; h = h->nxt)
			{	putskip(h->this->frst->seqno);
				a = huntstart(h->this->frst);
				if (h->nxt)
					fprintf(tt, "\tT = T->nxt\t= ");
				else
					fprintf(tt, "\t    T->nxt\t= ");
				fprintf(tt, "settr(%d,%d,0,0);",
							e->status, a);
				blurb(tt, e->n->ntyp, e->n->nval);
			}
			for (h = e->sub; h; h = h->nxt)
				putseq(h->this->frst);
		} else
		{	if (e->n && e->n->ntyp == ATOMIC)
			{	patch_atomic(e->n->seql->this);
				putskip(e->n->seql->this->frst->seqno);
				a = huntstart(e->n->seql->this->frst);
				fprintf(tt, "\tT = trans[%d][%d] = ",
						Pid, e->seqno);
				fprintf(tt, "settr(%d,0,0,0);", ATOM);
				blurb(tt, e->n->ntyp, e->n->nval);
				fprintf(tt, "\t    T->nxt\t= ");
				fprintf(tt, "settr(%d,%d,0,0);", ATOM,a);
				blurb(tt, e->n->ntyp, e->n->nval);
				e->n->seql->this->last->nxt = e->nxt;

				putseq(e->n->seql->this->frst);
				break;
			}
			if (e->n->ntyp == GOTO)
				a = huntele(get_lab(e->n->nsym),
						e->status)->seqno;
			else if (e->nxt)
				a = huntele(e->nxt, e->status)->seqno;
			else
				a = 0;
			fprintf(tt, "\ttrans[%d][%d]\t= ",
						Pid, e->seqno);
			if (any_undo(e->n))
				fprintf(tt, "settr(%d,%d,%d,%d);",
					e->status, a, uniq, uniq);
			else
				fprintf(tt, "settr(%d,%d,%d,0);",
					e->status, a, uniq);
			blurb(tt, e->n->ntyp, e->n->nval);
			fprintf(tm, "\tcase  %d: /* STATE ", uniq++);
			fprintf(tm, "%d - type %d - line %d */\n\t\t",
				e->seqno, e->n->ntyp, e->n->nval);
			if (e->n && e->n->ntyp != 'r' && Pid != claimnr)
				fprintf(tm, "IfNotBlocked\n\t\t");
			putstmnt(tm, e->n, e->seqno);
			n = getweight(e->n);
			fprintf(tm, ";\n\t\tm = %d; goto P999;\n", n);
			if (any_undo(e->n))
			{	fprintf(tb, "\tcase  %d: ", uniq-1);
				fprintf(tb, "/* STATE %d */\n\t\t",
							e->seqno);
				undostmnt(e->n, e->seqno);
				fprintf(tb, ";\n\t\tgoto R999;\n", n);
			}
		}
	}
}

void
patch_atomic(s)
	Sequence *s;
{	/* catch goto's that break the chain */
	Element *f, *g;
	SeqList *h;
	for (f = s->frst; ; f = f->nxt)
	{	if (f->n && f->n->ntyp == GOTO)
		{	g = get_lab(f->n->nsym);
			if ((f->status & ATOM)
			&& !(g->status & ATOM))
			{	f->status &= ~ATOM;
				f->status |= L_ATOM;
			}
		} else
		for (h = f->sub; h; h = h->nxt)
			patch_atomic(h->this);
		if (f == s->last)
			break;
	}
}

#define cat0(x)   	putstmnt(fd,now->lft,m); fprintf(fd, x); \
			putstmnt(fd,now->rgt,m)
#define cat1(x)		fprintf(fd,"("); cat0(x); fprintf(fd,")")
#define cat2(x,y)  	fprintf(fd,x); putstmnt(fd,y,m)
#define cat3(x,y,z)	fprintf(fd,x); putstmnt(fd,y,m); fprintf(fd,z)

void
putstmnt(fd, now, m)
	FILE *fd;
	Node *now;
{
	Node *v;
	int i, j; extern int m_loss;

	if (!now) { fprintf(fd, "0"); return; }
	if (now->ntyp != CONST) lineno = now->nval;
	switch (now->ntyp) {
	case CONST:	fprintf(fd, "%d", now->nval); break;
	case '!':	cat3("!(", now->lft, ")"); break;
	case UMIN:	cat3("-(", now->lft, ")"); break;
	case '~':	cat3("~(", now->lft, ")"); break;

	case '/':	cat1("/");  break;
	case '*':	cat1("*");  break;
	case '-':	cat1("-");  break;
	case '+':	cat1("+");  break;
	case '%':	cat1("%%"); break;
	case '<':	cat1("<");  break;
	case '>':	cat1(">");  break;
	case '&':	cat1("&");  break;
	case '|':	cat1("|");  break;
	case LE:	cat1("<="); break;
	case GE:	cat1(">="); break;
	case NE:	cat1("!="); break;
	case EQ:	cat1("=="); break;
	case OR:	cat1("||"); break;
	case AND:	cat1("&&"); break;
	case LSHIFT:	cat1("<<"); break;
	case RSHIFT:	cat1(">>"); break;

	case TIMEOUT:	fprintf(fd, "((trpt->tau)&1)"); break;

	case RUN:	if (claimproc
			&&  strcmp(now->nsym->name, claimproc) == 0)
				fatal("%s is claim, not runnable",
							claimproc);
			fprintf(fd,"addproc(%d", fproc(now->nsym->name));
			for (v = now->lft; v; v = v->rgt)
			{	cat2(", ", v->lft);
			}
			fprintf(fd, ")");
			break;
	case LEN:	putname(fd, "q_sz(", now->lft, m, ")");
			break;

	case 's':	fprintf(fd, "\n#if (SYNC>0 && ASYNC==0)\n\t\t");
			putname(fd, "if (q_sz(", now->lft, m, "))\n");
			fprintf(fd, "#else\n\t\t");
			putname(fd, "if (q_full(", now->lft, m, "))\n");
			fprintf(fd, "#endif\n");
			if (m_loss)
				fprintf(fd, "\t\t{ m=3; goto P999; }\n");
			else
				fprintf(fd, "\t\t\tcontinue;\n");
			putname(fd, "\t\tqsend(", now->lft, m, "");
			for (v = now->rgt, i = 0; v; v = v->rgt, i++)
			{	cat2(", ", v->lft);
			}
			if (i > Mpars)
				fatal("too many pars in send", "");
			for ( ; i < Mpars; i++)
				fprintf(fd, ", 0");
			fprintf(fd, ");\n");
			fprintf(fd, "#if SYNC\n#if ASYNC==0\n");
			putname(fd, "\t\tboq = ", now->lft, m, ";\n");
			fprintf(fd, "#else\n\t\t");
			putname(fd, "if (q_zero(", now->lft, m, ")) ");
			putname(fd, "boq = ",now->lft,m,";\n");
			fprintf(fd, "#endif\n#endif\n\t\t");
			break;
	case 'r':	fprintf(fd, "\n#if SYNC\n#if ASYNC==0\n");
			putname(fd, "\t\tif (boq != ", now->lft,m,")");
			fprintf(fd, " continue;\n#else\n");
			putname(fd, "\t\tif (q_zero(", now->lft,m,"))");
			fprintf(fd, "\n\t\t");
			putname(fd, "{	if (boq != ",  now->lft,m,")");
			fprintf(fd, " continue;\n\t\t} else\n\t\t");
			fprintf(fd, "{	if (boq != -1) continue;\n\t\t");
			fprintf(fd, "}\n#endif\n#endif\n\t\t");
			putname(fd, "if (q_sz(", now->lft, m, ") == 0)");
			fprintf(fd, " continue");
	/* test */	for (v = now->rgt, i=j=0; v; v = v->rgt, i++)
			{	if (v->lft->ntyp != CONST)
				{	j++; continue;
				}
				fprintf(fd, ";\n\t\t");
				cat3("if (", v->lft, " != ");
				putname(fd, "qrecv(", now->lft, m, ", ");
				fprintf(fd, "0, %d, 0)) continue", i);
			}
			if (j > 0)
				fprintf(fd, ";\n\t\tsv_save()");
	/* set */	for (v = now->rgt, i = 0; v; v = v->rgt, i++)
			{	if (v->lft->ntyp == CONST && v->rgt)
					continue;
				fprintf(fd, ";\n\t\t");
				if (v->lft->ntyp != CONST)
				{	nocast=1;
					putstmnt(fd, v->lft, m);
					nocast=0; fprintf(fd, " = ");
				}
				putname(fd, "qrecv(", now->lft, m, "");
				fprintf(fd, ", 0, %d, ", i);
				fprintf(fd, "%d)", (v->rgt)?0:1);
			}
			fprintf(fd, ";\n#if SYNC\n");
			putname(fd, "\t\tif (q_zero(", now->lft, m, "");
			fprintf(fd, ")) boq = -1;\n#endif\n\t\t");
			break;
	case 'R':	putname(fd, "(q_sz(", now->lft, m, ") > 0");
	/* test */	for (v = now->rgt, i=j=0; v; v = v->rgt, i++)
			{	if (v->lft->ntyp != CONST)
				{	j++; continue;
				}
				fprintf(fd, "\n\t\t&& qrecv(");
				putname(fd, "", now->lft, m, "");
				fprintf(fd, ", 0, %d, 0) == ", i);
				putstmnt(fd, v->lft, m);
			}
			fprintf(fd, ")");
			break;

	case 'c':	cat3("if (!(", now->lft, "))\n");
			fprintf(fd, "\t\t\tcontinue");
			break;
	case ASGN:	cat3("(trpt+1)->oval = ", now->lft, ";\n\t\t");
			nocast = 1; putstmnt(fd,now->lft,m); nocast = 0;
			fprintf(fd," = ");
			putstmnt(fd,now->rgt,m);
			break;
	case PRINT:	fprintf(fd, "printf(%s", now->nsym->name);
			for (v = now->lft; v; v = v->rgt)
			{	cat2(", ", v->lft);
			}
			fprintf(fd, ")");
			break;
	case NAME:	if (!nocast && now->nsym
			&&  now->nsym->type < SHORT)
				putname(fd, "((int)", now, m, ")");
			else
				putname(fd, "", now, m, "");
			break;
	case   'p':	putremote(fd, now, m);
			break;
	case   'q':	if (terse)
				fprintf(fd, "%s", now->nsym->name);
			else
				fprintf(fd, "%d", remotelab(now));
			break;
	case ASSERT:	cat3("assert(", now->lft, ", ");
			terse = nocast = 1;
			cat3("\"", now->lft, "\\n\", II, tt, t)");
			terse = nocast = 0;
			break;
	case   '.':
	case BREAK:
	case  GOTO:	putskip(m);
			break;
	case   '@':	fprintf(fd, "if (!delproc(1, II)) continue");
			fprintf(th, "#define endstate%d	%d\n", Pid, m);
			break;
	default   :	printf("spin: bad node type %d (.m)\n",
							now->ntyp);
			exit(1);
	}
}

void
putname(fd, pre, n, m, suff)	/* varref */
	FILE *fd;
	Node *n;
	char *pre, *suff;
{
	Symbol *s = n->nsym;
	if (!s)
		fatal("no name - putname", "");
	if (s->context && !s->type)	/* not a local name */
		s = lookup(s->name);	/* must be a global */
	if (!s->type)
		yyerror("undeclared name `%s'", s->name);
	fprintf(fd, pre);
	if (s->context || !strcmp(s->name, "_p"))
	{	if (!terse) fprintf(fd, "((P%d *)this)->", Pid);
		fprintf(fd, "%s", s->name);
	} else
	{	if (!terse) fprintf(fd, "now.");
		fprintf(fd, "%s", s->name);
	}
	if (s->nel != 1)
	{	cat3("[", n->lft, "]");
	}
	fprintf(fd, suff);
}

void
putremote(fd, n, m)		/* remote reference */
	FILE *fd;
	Node *n;
{
	if (terse)
	{	fprintf(fd, "%s[", n->lft->nsym->name);
		putstmnt(fd, n->lft->lft, m);
		if (strcmp(n->nsym->name, "_p") == 0)
			fprintf(fd, "]:");
		else
			fprintf(fd, "].%s", n->nsym->name);
	} else
	{	fprintf(fd, "((P%d *)Pptr(loops+",
			fproc(n->lft->nsym->name));
		if (claimproc) fprintf(fd, "1+");
		putstmnt(fd, n->lft->lft, m);
		fprintf(fd, "))->%s", n->nsym->name);
	}
	if (n->rgt)
	{	fprintf(fd, "[");
		putstmnt(fd, n->rgt, m);
		fprintf(fd, "]");
	}
}

getweight(n)
	Node *n;
{
	switch (n->ntyp) {
	case 'r':     return 4;
	case 's':     return 2;
	case TIMEOUT: return 1;	/* lowest priority */
	case 'c':     if (has_tau(n->lft)) return 1;
	}
	return 3;
}

has_tau(n)
	Node *n;
{
	if (!n) return 0;
	if (n->ntyp == TIMEOUT) return 1;
	return (has_tau(n->lft) || has_tau(n->rgt));
}

#include <ctype.h>

void
blurb(fd, t, n)
	FILE *fd;
{
	fprintf(fd, "	/* ");
	switch (t) {
	case ATOMIC:	fprintf(fd, "ATOMIC"); break;
	case IF:	fprintf(fd, "IF"); break;
	case DO:	fprintf(fd, "DO"); break;
	case BREAK:	fprintf(fd, "BREAK"); break;
	case GOTO:	fprintf(fd, "GOTO"); break;
	case ASSERT:	fprintf(fd, "ASSERT"); break;
	case TIMEOUT:	fprintf(fd, "TIMEOUT"); break;
	case LEN:	fprintf(fd, "LEN"); break;
	case RUN:	fprintf(fd, "RUN"); break;
	case PRINT:	fprintf(fd, "PRINT"); break;
	case NAME:	fprintf(fd, "NAME"); break;
	default:	if (isprint(t))
				fprintf(fd, "`%c'", t);
			else
				fprintf(fd, "%d", t);
			break;
	}
	fprintf(fd, " line %d */\n", n);
}