/***** spin: vars.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"

extern RunList	*X;

getval(s, n)
	Symbol *s;
{
	if (s->context && s->type)
		return getlocal(s, n);
	if (!s->type)	/* not declared locally */
		s = lookup(s->name); /* try global */
	return getglobal(s, n);
}

setval(v, n)
	Node *v;
{
	if (v->nsym->context && v->nsym->type)
		return setlocal(v, n);
	if (!v->nsym->type)
		v->nsym = lookup(v->nsym->name);
	return setglobal(v, n);
}

checkvar(s, n)
	Symbol *s;
{
	int i;

	if (n >= s->nel || n < 0)
	{	yyerror("array indexing error, `%s'", s->name);
		return 0;
	}
	if (s->type == 0)
	{	yyerror("undecl var `%s' (assuming int)", s->name);
		s->type = INT;
	}
	if (s->val == (int *) 0)	/* uninitialized */
	{	s->val = (int *) emalloc(s->nel*sizeof(int));
		for (i = 0; i < s->nel; i++)
		{	if (s->type != CHAN)
				s->val[i] = eval(s->ini);
			else
				s->val[i] = qmake(s);
	}	}
	return 1;
}

getglobal(s, n)
	Symbol *s;
{
	int i;
	if (strcmp(s->name, "_p") == 0)
		return (X && X->pc)?X->pc->seqno:0;
	if (s->type == 0 && X && (i = find_lab(s, X->n)))
		return i;
	if (checkvar(s, n))
		return cast_val(s->type, s->val[n]);
	return 0;
}

void
typex(n, t)
	Node *n;
{
	if (n->ntyp == NAME && n->nsym->type != t
	&& (t == CHAN || n->nsym->type == CHAN))
		yyerror("type clash (chan) in mesg pars", 0);
}

cast_val(t, v)
{	int i=0; short s=0; unsigned char u=0;

	if (t == INT || t == CHAN) i = v;
	else if (t == SHORT) s = (short) v;
	else if (t == BYTE)  u = (unsigned char)v;
	else if (t == BIT)   u = (unsigned char)(v&1);

	if (v != i+s+u)
		yyerror("value %d truncated in assignment", v);
	return (int)(i+s+u);
}

setglobal(v, m)
	Node *v;
{
	int n = eval(v->lft);

	if (checkvar(v->nsym, n))
		v->nsym->val[n] = m;
	return 1;
}

void
dumpglobals()
{	extern Symbol *symtab[Nhash+1];
	register Symbol *sp;
	register int i, j, k, n, m;

	for (i = 0; i <= Nhash; i++)
	for (sp = symtab[i]; sp; sp = sp->next)
	{	if (!sp->type || sp->context)
			continue;
		for (j = 0, m = -1; j < sp->nel; j++)
		{	if (sp->type == CHAN)
			{	doq(sp, j);
				k = 0;
				continue;
			}
			n = getglobal(sp, j);
			if (j == 0 || n != k)
			{	if (m != j-1)
					printf("\t\t...\n");
				if (sp->nel > 1)
				  printf("\t\t%s[%d] = %d\n",
					sp->name, j, n);
				else
				  printf("\t\t%s = %d\n",
					sp->name, n);
				m = j;
			}
			k = n;
	}	}
}

void
dumplocal(s)
	Symbol *s;
{
	Symbol *z;
	int i;

	for (z = s; z; z = z->next)
	for (i = 0; i < z->nel; i++)
	{	if (z->type == CHAN)
			doq(z, i);
		else
		{	if (z->nel > 1)
			  printf("\t\t%s[%d] = %d\n",
			  z->name, i, getval(z,i));
			else
			  printf("\t\t%s = %d\n",
			  z->name, getval(z,0));
	}	}
}