/***** spin: pangen1.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 <math.h>
#include "spin.h"
#include "y.tab.h"
#include "pangen1.h"
#include "pangen3.h"

extern FILE	*tc, *th;
extern Node	*Mtype;
extern ProcList	*rdy;
extern Queue	*qtab;
extern RunList	*run;
extern Symbol	*symtab[Nhash+1];
extern int	nqs, nps, mst, Mpars;
extern char	*claimproc;

enum { INIV, PUTV };
int Npars=0, u_sync=0, u_async=0;
int acceptors=0;

void
genheader()
{	ProcList *p;
	int i;
	fprintf(th, "#define SYNC	%d\n", u_sync);
	fprintf(th, "#define ASYNC	%d\n\n", u_async);

	fprintf(tc, "char *procname[] = {\n");
	put_ptype(run->n->name, (Node *) 0, 0, mst, nps);
	for (p = rdy, i = 1; p; p = p->nxt, i++)
		put_ptype(p->n->name, p->p, i, mst, nps);
	put_ptype("_progress", (Node *) 0, i, mst, nps);
	fprintf(tc, "};\n\n");
	ntimes(th, 0, 1, Header);
	doglobal(PUTV);
	fprintf(th, "	uchar sv[VECTORSZ];\n");
	fprintf(th, "} State;\n");
}

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

	fprintf(tc, "addproc(n");
	for (i = 0; i < Npars; i++)
		fprintf(tc, ", par%d", i);

	ntimes(tc, 0, 1, Addp0);
	ntimes(tc, 1, nps, R5);
	ntimes(tc, 0, 1, Addp1);

	put_pinit(run->pc, run->n, (Node *) 0, 0);
	for (p = rdy, i = 1; p; p = p->nxt, i++)
		put_pinit(p->s->frst, p->n, p->p, i);

	ntimes(tc, i, i+1, R6);
}

void
genother(cnt)
{	ProcList *p;
	int i;

	ntimes(tc,   0,   1, Code0);
	ntimes(tc,   0, cnt,   R0);
	ntimes(tc, cnt, cnt+1, R1);
	end_labs(run->n, 0);
	for (p = rdy, i = 1; p; p = p->nxt, i++)
		end_labs(p->n, i);
	ntimes(tc, 0, cnt, R0a);
	ntimes(th, acceptors, acceptors+1, Code1);
	ntimes(th, i+1, i+2, R2);

	doglobal(INIV);
	ntimes(tc, 1, nqs+1, R3);
	ntimes(tc, 0,     1, Code2);
	ntimes(tc, 0,     i, R4);
	fprintf(tc, "}\n\n");
}

static struct {
	char *s, *t; int n, m;
} ln[] = {
	"end",  	"stopstate",	3,	0,
	"progress",	"progstate",	8,	0,
	"accept",	"accpstate",	6,	1,
	0,		0,		0,	0,
};

void
end_labs(s, i)
	Symbol *s;
{
	extern Label *labtab;
	Label *l;
	int j;

	for (l = labtab; l; l = l->nxt)
	for (j = 0; ln[j].n; j++)
		if (strncmp(l->s->name, ln[j].s, ln[j].n) == 0
		&&  strcmp(l->s->context->name, s->name) == 0)
		{	fprintf(tc, "\t%s[%d][%d] = 1;\n",
				ln[j].t, i, l->e->seqno);
			acceptors += ln[j].m;
		}
}

void
ntimes(fd, n, m, c)
	FILE *fd;
	char *c[];
{
	int i, j;
	for (j = 0; c[j]; j++)
	for (i = n; i < m; i++)
	{	fprintf(fd, c[j], i, i, i, i);
		fprintf(fd, "\n");
	}
}

short Types[] = { BIT, BYTE, CHAN, SHORT, INT };

void
dolocal(dowhat, p, s)
	char *s;
{
	int i, j;
	Symbol *sp;
	char buf[64];

	for (j = 0; j < 5; j++)
	for (i = 0; i <= Nhash; i++)
	for (sp = symtab[i]; sp; sp = sp->next)
		if (sp->context && sp->type == Types[j]
		&&  strcmp(s, sp->context->name) == 0)
		{	sprintf(buf, "((P%d *)pptr(h))->", p);
			do_var(dowhat, buf, sp);
		}
}

void
doglobal(dowhat)
{	Symbol *sp;
	int i, j;

	for (j = 0; j < 5; j++)
	for (i = 0; i <= Nhash; i++)
	for (sp = symtab[i]; sp; sp = sp->next)
		if (!sp->context && sp->type == Types[j])
			do_var(dowhat, "now.", sp);
}

void
do_var(dowhat, s, sp)
	char *s;
	Symbol *sp;
{
	int i;

	switch(dowhat) {
	case PUTV:
		typ2c(sp);
		break;
	case INIV:
		if (!sp->ini)
			break;
		if (sp->nel == 1)
		{	fprintf(tc, "\t\t%s%s = ", s, sp->name);
			do_init(sp);
		} else
		for (i = 0; i < sp->nel; i++)
		{	fprintf(tc, "\t\t%s%s[%d] = ", s, sp->name, i);
			do_init(sp);
		}
		break;
	}
}

void
do_init(sp)
	Symbol *sp;
{
	int i;

	if (sp->type == CHAN && ((i = qmake(sp)) > 0))
		fprintf(tc, "addqueue(%d);\n", i);
	else
		fprintf(tc, "%d;\n", eval(sp->ini));
}

blog(n)	/* for small log2 without rounding problems */
{	int m=1, r=2;
	while (r < n) { m++; r *= 2; }
	return 1+m;
}

void
put_ptype(s, p, i, m0, m1)
	char *s;
	Node *p;
{
	Node *fp, *fpt;
	int j;
	fprintf(tc, "	\"%s\",\n", s);
	fprintf(th, "typedef struct P%d { /* %s */\n", i, s);
	fprintf(th, "	unsigned _t : %d; /* proctype */\n", blog(m1));
	fprintf(th, "	unsigned _p : %d; /* state    */\n", blog(m0));
	dolocal(PUTV, i, s);	/* includes pars */
	fprintf(th, "} P%d;\n", i);

	for (fp  = p, j = 0;  fp;  fp = fp->rgt)
	for (fpt = fp->lft;  fpt; fpt = fpt->rgt)
		j++;	/* count # of parameters */
	Npars = max(Npars, j);
}

void
put_pinit(e, s, p, i)
	Element *e;
	Symbol *s;
	Node *p;
{
	Node *fp, *fpt;
	int ini, j;

	ini = huntele(e, e->status)->seqno;

	fprintf(tc, "\tcase %d:	/* %s */\n", i, s->name);
	fprintf(tc, "\t\t((P%d *)pptr(h))->_t = %d;\n", i, i);
	fprintf(tc, "\t\t((P%d *)pptr(h))->_p = %d;", i, ini);
	fprintf(tc, " reached%d[%d]=1;\n", i, ini);
	dolocal(INIV, i, s->name);
	for (fp  = p, j=0; fp; fp = fp->rgt)
	for (fpt = fp->lft; fpt; fpt = fpt->rgt, j++)
	{	if (fpt->nsym->nel != 1)
		fatal("array in parameter list, %s", fpt->nsym->name);
		fprintf(tc, "\t\t((P%d *)pptr(h))->%s = par%d;\n",
				i, fpt->nsym->name, j);
	}
	fprintf(tc, "\t	break;\n");
}

huntstart(f)
	Element *f;
{
	Element *e = f;

	if (e->n)
	{	if (e->n->ntyp=='.' && e->nxt)
			e = e->nxt;
		else if (e->n->ntyp == ATOMIC)
			e->n->seql->this->last->nxt = e->nxt;
	}
	return e->seqno;
}

Element *
huntele(f, o)
	Element *f;
{
	Element *g, *e = f;
	int cnt; /* a precaution against loops */
	for (cnt=0; cnt < 10 && e->n; cnt++)
	{	switch (e->n->ntyp) {
		case GOTO:
			g = get_lab(e->n->nsym);
			break;
		case '.':
		case BREAK:
			if (!e->nxt)
				return e;
			g = e->nxt;
			break;
		case ATOMIC:
			e->n->seql->this->last->nxt = e->nxt;
		default:	/* fall through */
			return e;
		}
		if ((o & ATOM) && !(g->status & ATOM))
			return e;
		e = g;
	}
	return e;
}

void
typ2c(sp)
	Symbol *sp;
{
	switch (sp->type) {
	case BIT:
		if (sp->nel == 1)
		{	fprintf(th, "\tunsigned %s : 1", sp->name);
			break;
		} /* else fall through */
	case CHAN:	/* good for up to 255 channels */
	case BYTE:
		fprintf(th, "\tuchar %s", sp->name);
		break;
	case SHORT:
		fprintf(th, "\tshort %s", sp->name);
		break;
	case INT:
		fprintf(th, "\tint %s", sp->name);
		break;
	case PREDEF:
		return;
	default:
		fatal("variable %s undeclared", sp->name);
	}
	if (sp->nel != 1)
		fprintf(th, "[%d]", sp->nel);
	fprintf(th, ";\n");
}

void
ncases(fd, p, n, m, c)
	FILE *fd;
	char *c[];
{
	int i, j;
	for (j = 0; c[j]; j++)
	for (i = n; i < m; i++)
	{	fprintf(fd, c[j], i, p, i);
		fprintf(fd, "\n");
	}
}

void
genaddqueue()
{	char *buf0;
	int j;
	Queue *q;

	buf0 = (char *) emalloc(32);
	ntimes(tc, 0, 1, Addq0);
	for (q = qtab; q; q = q->nxt)
	{	ntimes(tc, q->qid, q->qid+1, R8);
		ntimes(th, q->qid, q->qid+1, R9);
		for (j = 0; j < q->nflds; j++)
		{	switch (q->fld_width[j]) {
			case BIT:
				if (q->nflds != 1)
				{	fprintf(th, "\t\tunsigned");
					fprintf(th, " fld%d : 1;\n", j);
					break;
				} /* else fall through: gives smaller struct */
			case CHAN:
			case BYTE:
				fprintf(th, "\t\tuchar fld%d;\n", j);
				break;
			case SHORT:
				fprintf(th, "\t\tshort fld%d;\n", j);
				break;
			case INT:
				fprintf(th, "\t\tint fld%d;\n", j);
				break;
			default:
				fatal("bad channel spec", "");
			}
		}
		fprintf(th, "	} contents[%d];\n", max(1, q->nslots));
		fprintf(th, "} Q%d;\n", q->qid);
	}
	ntimes(th, 0, 1, R10);
	ntimes(tc, 0, 1, Addq1);

	fprintf(tc, "qsend(into");
	for (j = 0; j < Mpars; j++)
		fprintf(tc, ", fld%d", j);
	fprintf(tc, ")\n");
	ntimes(tc, 0, 1, Addq11);

	for (q = qtab; q; q = q->nxt)
	{	sprintf(buf0, "((Q%d *)z)->", q->qid);
		fprintf(tc, "\tcase %d: j = %sQlen;\n", q->qid, buf0);
		fprintf(tc, "\t\t%sQlen = j+1;\n", buf0);
		if (q->nslots == 0)	/* reset handshake point */
			fprintf(tc, "\t\t(trpt+2)->o_m = 0;\n");
		sprintf(buf0, "((Q%d *)z)->contents[j].fld", q->qid);
		for (j = 0; j < q->nflds; j++)
			fprintf(tc, "\t\t%s%d = fld%d;\n", buf0, j, j);
		fprintf(tc, "\t\tbreak;\n");
	}
	ntimes(tc, 0, 1, Addq2);

	for (q = qtab; q; q = q->nxt)
	fprintf(tc, "\tcase %d: return %d;\n", q->qid, (!q->nslots));

	ntimes(tc, 0, 1, Addq3);

	for (q = qtab; q; q = q->nxt)
	fprintf(tc, "\tcase %d: return (q_sz(from) == %d);\n",
			q->qid, max(1, q->nslots));

	ntimes(tc, 0, 1, Addq4);
	for (q = qtab; q; q = q->nxt)
	{	sprintf(buf0, "((Q%d *)z)->", q->qid);
		fprintf(tc, "	case %d:", q->qid);
		if (q->nflds == 1)
		{	fprintf(tc, "\tif (fld == 0) r = %s", buf0);
			fprintf(tc, "contents[slot].fld0;\n");
		} else
		{	fprintf(tc, "\tswitch (fld) {\n");
			ncases(tc, q->qid, 0, q->nflds, R12);
			fprintf(tc, "\t\t}\n");
		}
		fprintf(tc, "\t\tif (done)\n");
		fprintf(tc, "\t\t{	j = %sQlen;\n",  buf0);
		fprintf(tc, "\t\t	%sQlen = --j;\n", buf0);
		fprintf(tc, "\t\t	for (k=0; k<j; k++)\n", q->qid);
		fprintf(tc, "\t\t	{\n");

		sprintf(buf0, "\t\t\t((Q%d *)z)->contents", q->qid);
		for (j = 0; j < q->nflds; j++)
		{	fprintf(tc, "\t%s[k].fld%d = \n", buf0, j);
			fprintf(tc, "\t\t%s[k+1].fld%d;\n", buf0, j);
		}
		fprintf(tc, "\t\t	}\n");
		for (j = 0; j < q->nflds; j++)
			fprintf(tc, "%s[j].fld%d = 0;\n", buf0, j);
		fprintf(tc, "\t\t\tif (fld+1 != %d)\n\t\t\t", q->nflds);
		fprintf(tc, "\tuerror(\"missing pars in receive\");\n");
		/* incompletely received msgs cannot be unrecv'ed */
		fprintf(tc, "\t\t}\n");
		fprintf(tc, "\t\tbreak;\n");
	}
	ntimes(tc, 0, 1, Addq5);
}