/***** spin: structures.c *****/

/* Copyright (c) 1991,1995 by AT&T Corporation.  All Rights Reserved.     */
/* This software is for educational purposes only.                        */
/* Permission is given to distribute this code provided that this intro-  */
/* ductory message is not removed and no monies are exchanged.            */
/* No guarantee is expressed or implied by the distribution of this code. */
/* Software 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 and/or questions to: gerard@research.att.com          */

#include "spin.h"
#include "y.tab.h"

extern	Symbol	*context;
extern	RunList	*X;
extern	Symbol	*Fname;
extern	int	lineno, depth;

Symbol	*owner;

typedef struct UType {
	Symbol *nm;		/* name of the type */
	Lextok *cn;		/* contents */
	struct UType *nxt;	/* linked list */
} UType;

static UType *Unames = 0;
static UType *Pnames = 0;

void
setuname(Lextok *n)
{	UType *tmp;

	for (tmp = Unames; tmp; tmp = tmp->nxt)
		if (!strcmp(owner->name, tmp->nm->name))
		{	non_fatal("typename %s was defined before",
				tmp->nm->name);
			return;
		}
	tmp = (UType *) emalloc(sizeof(UType));
	tmp->nm = owner;
	tmp->cn = n;
	tmp->nxt = Unames;
	Unames = tmp;
}

void
putUname(FILE *fd, UType *tmp)
{	Lextok *fp, *tl;

	if (!tmp) return;
	putUname(fd, tmp->nxt); /* postorder */
	fprintf(fd, "struct %s { /* user defined type */\n",
		tmp->nm->name);
	for (fp = tmp->cn; fp; fp = fp->rgt)
	for (tl = fp->lft; tl; tl = tl->rgt)
		typ2c(tl->sym);
	fprintf(fd, "};\n");
}

void
putunames(FILE *fd)
{
	putUname(fd, Unames);
}

int
isutype(char *t)
{	UType *tmp;

	for (tmp = Unames; tmp; tmp = tmp->nxt)
	{	if (!strcmp(t, tmp->nm->name))
			return 1;
	}
	return 0;
}

Lextok *
getuname(Symbol *t)
{	UType *tmp;

	for (tmp = Unames; tmp; tmp = tmp->nxt)
	{	if (!strcmp(t->name, tmp->nm->name))
			return tmp->cn;
	}
	fatal("%s is not a typename", t->name);
	return (Lextok *)0;
}

void
setutype(Lextok *p, Symbol *t, Lextok *vis)	/* user-defined types */
{	int oln = lineno;
	Symbol *ofn = Fname;
	Lextok *m, *n;

	m = getuname(t);
	for (n = p; n; n = n->rgt)
	{	lineno = n->ln;
		Fname = n->fn;
		if (n->sym->type)
		non_fatal("redeclaration of '%s'", n->sym->name);

		if (vis) n->sym->hidden = 1;
		n->sym->type = STRUCT;	/* classification   */
		n->sym->Slst = m;	/* structure itself */
		n->sym->Snm  = t;	/* name of typedef  */
		n->sym->Nid  = 0;	/* this is no chan  */
		if (n->sym->nel <= 0)
		non_fatal("bad array size for '%s'", n->sym->name);
	}
	lineno = oln;
	Fname = ofn;
}

Symbol *
do_same(Lextok *n, Symbol *v, int xinit)
{	Lextok *tmp, *fp, *tl;
	int ix = eval(n->lft);

	lineno = n->ln;
	Fname = n->fn;
	
	/* n->sym->type == STRUCT
	 * index:		n->lft
	 * subfields:		n->rgt
	 * structure template:	n->sym->Slst
	 * runtime values:	n->sym->Sval
	 */
	if (xinit) ini_struct(v);	/* once, at top level */

	if (ix >= v->nel || ix < 0)
	{	printf("spin: indexing %s[%d] - size is %d\n",
				v->name, ix, v->nel);
		fatal("indexing error %s", v->name);
	}
	if (!n->rgt || !n->rgt->lft)
	{	printf(">>%u %d<<\n", n->rgt, (n->rgt)?n->rgt->ntyp:-1);
		non_fatal("no subfields %s", v->name);	/* i.e., wants all */
		return ZS;
	}

	if (n->rgt->ntyp != '.')
	{	printf("bad subfield type %d\n", n->rgt->ntyp);
		exit(1);
	}

	tmp = n->rgt->lft;
	if (tmp->ntyp != NAME && tmp->ntyp != TYPE)
	{	printf("bad subfield entry %d\n", tmp->ntyp);
		exit(1);
	}
	for (fp = v->Sval[ix]; fp; fp = fp->rgt)
	for (tl = fp->lft; tl; tl = tl->rgt)
	{	if (!strcmp(tl->sym->name, tmp->sym->name))
			return tl->sym;
	}
	fatal("cannot locate subfield %s", tmp->sym->name);
	return ZS;
}

int
Rval_struct(Lextok *n, Symbol *v, int xinit)	/* n varref, v valref */
{	Symbol *tl;
	Lextok *tmp;
	int ix;

	if (!n || !(tl = do_same(n, v, xinit)))
		return 0;

	tmp = n->rgt->lft;
	if (tmp->sym->type == STRUCT)
	{
		return Rval_struct(tmp, tl, 0);
	} else if (tmp->rgt)
		fatal("non-zero 'rgt' on non-structure", 0);

	ix = eval(tmp->lft);
	if (ix >= tl->nel || ix < 0)
		fatal("indexing error %s", tl->name);

	return cast_val(tl->type, tl->val[ix]);
}

int
Lval_struct(Lextok *n, Symbol *v, int xinit, int a)  /* a = assigned value */
{	Symbol *tl;
	Lextok *tmp;
	int ix;

	if (!(tl = do_same(n, v, xinit)))
		return 1;

	tmp = n->rgt->lft;
	if (tmp->sym->type == STRUCT)
		return Lval_struct(tmp, tl, 0, a);
	else if (tmp->rgt)
		fatal("non-zero 'rgt' on non-structure", 0);

	ix = eval(tmp->lft);
	if (ix >= tl->nel || ix < 0)
		fatal("indexing error %s", tl->name);

	tl->val[ix] = a;
	tl->setat = depth;

	return 1;
}

int
Cnt_flds(Lextok *m)
{	Lextok *fp, *tl, *n;
	int cnt = 0;

	if (m->ntyp == ',')
	{	n = m;
		goto is_lst;
	}
	if (!m->sym || m->ntyp != STRUCT)
		return 1;

	n = getuname(m->sym);
is_lst:
	for (fp = n; fp; fp = fp->rgt)
	for (tl = fp->lft; tl; tl = tl->rgt)
	{	if (tl->sym->type == STRUCT)
			cnt += Cnt_flds(tl->sym->Slst);
		else
			cnt += tl->sym->nel;
	}

	return cnt;
}

int
Sym_typ(Lextok *t)
{	Symbol *s = t->sym;

	if (!s) return 0;

	if (s->type != STRUCT)
		return s->type;

	if (!t->rgt
	||  !t->rgt->ntyp == '.'
	||  !t->rgt->lft)
		fatal("unexpected struct layout %s", s->name);

	return Sym_typ(t->rgt->lft);
}

int
Width_set(int *wdth, int i, Lextok *n)
{	Lextok *fp, *tl;
	int j = i, k;

	for (fp = n; fp; fp = fp->rgt)
	for (tl = fp->lft; tl; tl = tl->rgt)
	{	if (tl->sym->type == STRUCT)
			j = Width_set(wdth, j, tl->sym->Slst);
		else
		{	for (k = 0; k < tl->sym->nel; k++, j++)
				wdth[j] = tl->sym->type;
	}	}
	return j;
}

void
ini_struct(Symbol *s)
{	int i; Lextok *fp, *tl;

	if (s->type != STRUCT)	/* last step */
	{	(void) checkvar(s, 0);
		return;
	}
	if (s->Sval == (Lextok **) 0)
	{	s->Sval = (Lextok **) emalloc(s->nel * sizeof(Lextok *));
		for (i = 0; i < s->nel; i++)
		{	s->Sval[i] = cpnn(s->Slst, 1, 1, 1);

			for (fp = s->Sval[i]; fp; fp = fp->rgt)
			for (tl = fp->lft; tl; tl = tl->rgt)
				ini_struct(tl->sym);
	}	}
}

Lextok *
cpnn(Lextok *s, int L, int R, int S)
{	Lextok *d; extern int Nid;

	if (!s) return ZN;

	d = (Lextok *) emalloc(sizeof(Lextok));
	d->ntyp = s->ntyp;
	d->val  = s->val;
	d->ln   = s->ln;
	d->fn   = s->fn;
	d->sym  = s->sym;
	if (L) d->lft = cpnn(s->lft, 1, 1, S);
	if (R) d->rgt = cpnn(s->rgt, 1, 1, S);

	if (S && s->sym)
	{	d->sym = (Symbol *) emalloc(sizeof(Symbol));
		memcpy(d->sym, s->sym, sizeof(Symbol));
		if (d->sym->type == CHAN)
		{	d->sym->Nid = ++Nid;
	}	}
	if (s->sq || s->sl)
		fatal("cannot happen cpnn", (char *) 0);

	return d;
}

void
full_name(FILE *fd, Lextok *n, Symbol *v, int xinit)
{	Symbol *tl;
	Lextok *tmp;

	fprintf(fd, "%s", v->name);

	if (!n || !(tl = do_same(n, v, xinit)))
		return;
	tmp = n->rgt->lft;
	if (tmp->sym->type == STRUCT)
	{	fprintf(fd, ".");
		full_name(fd, tmp, tl, 0);
		return;
	}
	fprintf(fd, ".%s", tl->name);
	if (tmp->sym->nel > 1)
		fprintf(fd, "[%d]", eval(tmp->lft));
}

void
struct_name(Lextok *n, Symbol *v, int xinit)
{	Symbol *tl;
	Lextok *tmp;

	if (!n || !(tl = do_same(n, v, xinit)))
		return;
	tmp = n->rgt->lft;
	if (tmp->sym->type == STRUCT)
	{	printf(".");
		struct_name(tmp, tl, 0);
		return;
	}
	printf(".%s", tl->name);
	if (tmp->sym->nel > 1)
		printf("[%d]", eval(tmp->lft));
}

void
dump_struct(Symbol *z, char *prefix, RunList *r)
{	Lextok *fp, *tl;
	int ix, jx;

	ini_struct(z);

	for (ix = 0; ix < z->nel; ix++)
	for (fp = z->Sval[ix]; fp; fp = fp->rgt)
	for (tl = fp->lft; tl; tl = tl->rgt)
	{	if (tl->sym->type == STRUCT)
		{	char pref[128];
			strcpy(pref, prefix);
			strcat(pref, ".");
			strcat(pref, tl->sym->name);
			dump_struct(tl->sym, pref, r);
		} else
		for (jx = 0; jx < tl->sym->nel; jx++)
		{	if (tl->sym->type == CHAN)
				doq(tl->sym, jx, r);
			else
			{	printf("\t\t");
				if (r)
				printf("%s(%d):", r->n->name, r->pid);
				printf("%s.%s", prefix, tl->sym->name);
				if (tl->sym->nel > 1)
					printf("[%d]", jx);
				printf(" = %d\n", tl->sym->val[jx]);
	}	}	}
}

int
fill_struct(Symbol *z, int cur, int ov, char *gather, Symbol **sp)
{	Lextok *fp, *tl;
	int ix;
	int nc = cur;
	int nv = ov;
	char newpref[128];

	ini_struct(z);

	for (ix = 0; ix < z->nel; ix++)
	for (fp = z->Sval[ix]; fp; fp = fp->rgt)
	for (tl = fp->lft; tl; tl = tl->rgt)
	{	if (tl->sym->type == STRUCT)
		{	sprintf(newpref, "%s.%s",
				gather, tl->sym->name);
			nc = fill_struct(tl->sym, nc, nv, newpref, sp);
			if (nc < 0)
			{	strcpy(gather, newpref);
				return nc;
			}
			if (nv < nc) nv = nc;
			continue;
		} else
		if (tl->sym->type == CHAN
		&&  nv-nc < tl->sym->nel)
		{	strcat(gather, ".");
			*sp = tl->sym;
			return -nv-1;
		}
		nc++; if (nv < nc) nv = nc;
	}
	return nc;
}

int
retrieve(Lextok **targ, int i, int want, Lextok *n, int Ntyp)
{	Lextok *fp, *tl;
	int j = i, k;

	for (fp = n; fp; fp = fp->rgt)
	for (tl = fp->lft; tl; tl = tl->rgt)
	{	if (tl->sym->type == STRUCT)
		{	j = retrieve(targ, j, want, tl->sym->Slst, Ntyp);
			if (j < 0)
			{	Lextok *x = cpnn(tl, 1, 0, 0);
				x->rgt = nn(ZN, '.', (*targ), ZN);
				(*targ) = x;
				return -1;
			}
		} else
		{	for (k = 0; k < tl->sym->nel; k++, j++)
			{	if (j == want)
				{	*targ = cpnn(tl, 1, 0, 0);
					(*targ)->lft = nn(ZN, CONST, ZN, ZN);
					(*targ)->lft->val = k;
					if (Ntyp)
					(*targ)->ntyp = Ntyp; /* was TYPE */
					return -1;
				}
	}	}	}
	return j;
}

int
is_explicit(Lextok *n)
{
	if (!n) return 0;
	if (!n->sym) fatal("unexpected - no symbol", 0);
	if (n->sym->type != STRUCT) return 1;
	if (!n->rgt) return 0;
	if (n->rgt->ntyp != '.')
	{	lineno = n->ln;
		Fname  = n->fn;
		printf("ntyp %d\n", n->rgt->ntyp);
		fatal("unexpected %s, no '.'", n->sym->name);
	}
	return is_explicit(n->rgt->lft);
}

Lextok *
expand(Lextok *n, int Ok)
	/* turn rgt-lnked list of struct nms, into ',' list of flds */
{	Lextok *x = ZN, *y;

	if (!Ok) return n;

	while (n)
	{	y = mk_explicit(n, 1, 0);
		if (x)
			(void) tail_add(x, y);
		else
			x = y;

		n = n->rgt;
	}
	return x;
}

Lextok *
mk_explicit(Lextok *n, int Ok, int Ntyp) /* produce a single ',' list of fields */
{	Lextok *bld = ZN, *x;
	int i, cnt;

	if (n->sym->type != STRUCT
	||  is_explicit(n))
		return n;

	if (!Ok) fatal("incomplete structure ref %s", n->sym->name);

	cnt = Cnt_flds(n->sym->Slst);
	for (i = cnt-1; i >= 0; i--)
	{	bld = nn(ZN, ',', ZN, bld);
		if (retrieve(&(bld->lft), 0, i, n->sym->Slst, Ntyp) >= 0)
		{	printf("cannot retrieve field %d\n", i);
			fatal("bad structure %s", n->sym->name);
		}
		x = cpnn(n, 1, 0, 0);
		x->rgt = nn(ZN, '.', bld->lft, ZN);
		bld->lft = x;
	}
	return bld;
}

Lextok *
tail_add(Lextok *a, Lextok *b)
{	Lextok *t;

	for (t = a; t->rgt; t = t->rgt)
		if (t->ntyp != ',')
		fatal("unexpected type - tail_add", 0);
	t->rgt = b;
	return a;
}

void
setpname(Lextok *n)
{	UType *tmp;

	for (tmp = Pnames; tmp; tmp = tmp->nxt)
		if (!strcmp(n->sym->name, tmp->nm->name))
		{	non_fatal("proctype %s redefined",
				n->sym->name);
			return;
		}
	tmp = (UType *) emalloc(sizeof(UType));
	tmp->nm = n->sym;
	tmp->nxt = Pnames;
	Pnames = tmp;
}

int
isproctype(char *t)
{	UType *tmp;

	for (tmp = Pnames; tmp; tmp = tmp->nxt)
	{	if (!strcmp(t, tmp->nm->name))
			return 1;
	}
	return 0;
}