/***** spin: mesg.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" #ifndef MAXQ#define MAXQ	2500		/* default max # queues  */#endif extern RunList	*X;extern Symbol	*Fname;extern Lextok	*Mtype;extern int	verbose, TstOnly, s_trail, analyze, columns;extern int	lineno, depth, xspin, m_loss, jumpsteps;extern int	nproc, nstop;extern short	Have_claim; Queue	*qtab = (Queue *) 0;	/* linked list of queues */Queue	*ltab[MAXQ];		/* linear list of queues */int	nqs = 0, firstrow = 1;char	Buf[4096]; static Lextok	*n_rem = (Lextok *) 0;static Queue	*q_rem = (Queue  *) 0; static int	a_rcv(Queue *, Lextok *, int);static int	a_snd(Queue *, Lextok *);static int	sa_snd(Queue *, Lextok *);static int	s_snd(Queue *, Lextok *);extern void	sr_buf(int, int);extern void	sr_mesg(FILE *, int, int);extern void	putarrow(int, int);static void	sr_talk(Lextok *, int, char *, char *, int, Queue *); intcnt_mpars(Lextok *n){	Lextok *m;	int i=0; 	for (m = n; m; m = m->rgt)		i += Cnt_flds(m);	return i;} intqmake(Symbol *s){	Lextok *m;	Queue *q;	int i; 	if (!s->ini)		return 0; 	if (nqs >= MAXQ)	{	lineno = s->ini->ln;		Fname  = s->ini->fn;		fatal("too many queues (%s)", s->name);	}	if (analyze && nqs >= 255)	{	fatal("too many channel types", (char *)0);	} 	if (s->ini->ntyp != CHAN)		return eval(s->ini); 	q = (Queue *) emalloc(sizeof(Queue));	q->qid    = ++nqs;	q->nslots = s->ini->val;	q->nflds  = cnt_mpars(s->ini->rgt);	q->setat  = depth; 	i = max(1, q->nslots);	/* 0-slot qs get 1 slot minimum */ 	q->contents  = (int *) emalloc(q->nflds*i*sizeof(int));	q->fld_width = (int *) emalloc(q->nflds*sizeof(int));	q->stepnr = (int *)   emalloc(i*sizeof(int)); 	for (m = s->ini->rgt, i = 0; m; m = m->rgt)	{	if (m->sym && m->ntyp == STRUCT)			i = Width_set(q->fld_width, i, getuname(m->sym));		else			q->fld_width[i++] = m->ntyp;	}	q->nxt = qtab;	qtab = q;	ltab[q->qid-1] = q; 	return q->qid;} intqfull(Lextok *n){	int whichq = eval(n->lft)-1; 	if (whichq < MAXQ && whichq >= 0 && ltab[whichq])		return (ltab[whichq]->qlen >= ltab[whichq]->nslots);	return 0;} intqlen(Lextok *n){	int whichq = eval(n->lft)-1; 	if (whichq < MAXQ && whichq >= 0 && ltab[whichq])		return ltab[whichq]->qlen;	return 0;} intq_is_sync(Lextok *n){	int whichq = eval(n->lft)-1; 	if (whichq < MAXQ && whichq >= 0 && ltab[whichq])		return (ltab[whichq]->nslots == 0);	return 0;} intqsend(Lextok *n){	int whichq = eval(n->lft)-1; 	if (whichq == -1)	{	printf("Error: sending to an uninitialized chan\n");		whichq = 0;		return 0;	}	if (whichq < MAXQ && whichq >= 0 && ltab[whichq])	{	ltab[whichq]->setat = depth;		if (ltab[whichq]->nslots > 0)			return a_snd(ltab[whichq], n);		else			return s_snd(ltab[whichq], n);	}	return 0;} intqrecv(Lextok *n, int full){	int whichq = eval(n->lft)-1; 	if (whichq == -1)	{	if (n->sym && !strcmp(n->sym->name, "STDIN"))		{	Lextok *m; 			if (TstOnly) return 1; 			for (m = n->rgt; m; m = m->rgt)			if (m->lft->ntyp != CONST && m->lft->ntyp != EVAL)			{	int c = getchar();				(void) setval(m->lft, c);			} else				fatal("invalid use of STDIN", (char *)0); 			whichq = 0;			return 1;		}		printf("Error: receiving from an uninitialized chan %s\n",			n->sym?n->sym->name:"");		whichq = 0;		return 0;	}	if (whichq < MAXQ && whichq >= 0 && ltab[whichq])	{	ltab[whichq]->setat = depth;		return a_rcv(ltab[whichq], n, full);	}	return 0;} static intsa_snd(Queue *q, Lextok *n)	/* sorted asynchronous */{	Lextok *m;	int i, j, k;	int New, Old; 	for (i = 0; i < q->qlen; i++)	for (j = 0, m = n->rgt; m && j < q->nflds; m = m->rgt, j++)	{	New = cast_val(q->fld_width[j], eval(m->lft), 0);		Old = q->contents[i*q->nflds+j];		if (New == Old)			continue;		if (New >  Old)			break;	/* inner loop */		goto found;	/* New < Old */	}found:	for (j = q->qlen-1; j >= i; j--)	for (k = 0; k < q->nflds; k++)	{	q->contents[(j+1)*q->nflds+k] =			q->contents[j*q->nflds+k];	/* shift up */		if (k == 0)			q->stepnr[j+1] = q->stepnr[j];	}	return i*q->nflds;				/* new q offset */} voidtyp_ck(int ft, int at, char *s){	if ((verbose&32) && ft != at	&& (ft == CHAN || at == CHAN))	{	char buf[128], tag1[64], tag2[64];		(void) sputtype(tag1, ft);		(void) sputtype(tag2, at);		sprintf(buf, "type-clash in %s, (%s<-> %s)", s, tag1, tag2);		non_fatal("%s", buf);	}} static inta_snd(Queue *q, Lextok *n){	Lextok *m;	int i = q->qlen*q->nflds;	/* q offset */	int j = 0;			/* q field# */ 	if (q->nslots > 0 && q->qlen >= q->nslots)		return m_loss;	/* q is full */ 	if (TstOnly) return 1; 	if (n->val) i = sa_snd(q, n);	/* sorted insert */ 	q->stepnr[i/q->nflds] = depth; 	for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++)	{	int New = eval(m->lft);		q->contents[i+j] = cast_val(q->fld_width[j], New, 0);		if ((verbose&16) && depth >= jumpsteps)			sr_talk(n, New, "Send ", "->", j, q);		typ_ck(q->fld_width[j], Sym_typ(m->lft), "send");	}	if ((verbose&16) && depth >= jumpsteps)	{	for (i = j; i < q->nflds; i++)			sr_talk(n, 0, "Send ", "->", i, q);		if (j < q->nflds)			printf("%3d: warning: missing params in send\n",				depth);		if (m)			printf("%3d: warning: too many params in send\n",				depth);	}	q->qlen++;	return 1;} static inta_rcv(Queue *q, Lextok *n, int full){	Lextok *m;	int i=0, oi, j, k;	extern int Rvous; 	if (q->qlen == 0)		return 0;	/* q is empty */try_slot:	/* test executability */	for (m = n->rgt, j=0; m && j < q->nflds; m = m->rgt, j++)		if ((m->lft->ntyp == CONST		   && q->contents[i*q->nflds+j] != m->lft->val)		||  (m->lft->ntyp == EVAL		   && q->contents[i*q->nflds+j] != eval(m->lft->lft)))		{	if (n->val == 0		/* fifo recv */			||  n->val == 2		/* fifo poll */			|| ++i >= q->qlen)	/* last slot */				return 0;	/* no match  */			goto try_slot;		}	if (TstOnly) return 1; 	if (verbose&8)	{	if (j < q->nflds)			printf("%3d: warning: missing params in next recv\n",				depth);		else if (m)			printf("%3d: warning: too many params in next recv\n",				depth);	} 	/* set the fields */	if (Rvous)	{	n_rem = n;		q_rem = q;	} 	oi = q->stepnr[i];	for (m = n->rgt, j = 0; m && j < q->nflds; m = m->rgt, j++)	{	if (columns && !full)	/* was columns == 1 */			continue;		if ((verbose&8) && !Rvous && depth >= jumpsteps)		{	sr_talk(n, q->contents[i*q->nflds+j],			(full && n->val < 2)?"Recv ":"[Recv] ", "<-", j, q);		}		if (!full)			continue;	/* test */		if (m && m->lft->ntyp != CONST && m->lft->ntyp != EVAL)		{	(void) setval(m->lft, q->contents[i*q->nflds+j]);			typ_ck(q->fld_width[j], Sym_typ(m->lft), "recv");		}		if (n->val < 2)		/* not a poll */		for (k = i; k < q->qlen-1; k++)		{	q->contents[k*q->nflds+j] =			  q->contents[(k+1)*q->nflds+j];			if (j == 0)			  q->stepnr[k] = q->stepnr[k+1];		}	} 	if ((!columns || full)	&& (verbose&8) && !Rvous && depth >= jumpsteps)	for (i = j; i < q->nflds; i++)	{	sr_talk(n, 0,		(full && n->val < 2)?"Recv ":"[Recv] ", "<-", i, q);	}	if (columns == 2 && full && !Rvous && depth >= jumpsteps)		putarrow(oi, depth); 	if (full && n->val < 2)		q->qlen--;	return 1;} static ints_snd(Queue *q, Lextok *n){	Lextok *m;	RunList *rX, *sX = X;	/* rX=recvr, sX=sendr */	int i, j = 0;	/* q field# */ 	for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++)	{	q->contents[j] = cast_val(q->fld_width[j], eval(m->lft), 0);		typ_ck(q->fld_width[j], Sym_typ(m->lft), "rv-send");	}	q->qlen = 1;	if (!complete_rendez())	{	q->qlen = 0;		return 0;	}	if (TstOnly)	{	q->qlen = 0;		return 1;	}	q->stepnr[0] = depth;	if ((verbose&16) && depth >= jumpsteps)	{	m = n->rgt;		rX = X; X = sX;		for (j = 0; m && j < q->nflds; m = m->rgt, j++)			sr_talk(n, eval(m->lft), "Sent ", "->", j, q);		for (i = j; i < q->nflds; i++)			sr_talk(n, 0, "Sent ", "->", i, q);		if (j < q->nflds)			  printf("%3d: warning: missing params in rv-send\n",				depth);		else if (m)			  printf("%3d: warning: too many params in rv-send\n",				depth);		X = rX;	/* restore receiver's context */		if (!s_trail)		{	if (!n_rem || !q_rem)				fatal("cannot happen, s_snd", (char *) 0);			m = n_rem->rgt;			for (j = 0; m && j < q->nflds; m = m->rgt, j++)			{	if (m->lft->ntyp != NAME				||  strcmp(m->lft->sym->name, "_") != 0)					i = eval(m->lft);				else	i = 0; 				if (verbose&8)				sr_talk(n_rem,i,"Recv ","<-",j,q_rem);			}			if (verbose&8)			for (i = j; i < q->nflds; i++)				sr_talk(n_rem, 0, "Recv ", "<-", j, q_rem);			if (columns == 2)				putarrow(depth, depth);		}		n_rem = (Lextok *) 0;		q_rem = (Queue *) 0;	}	return 1;} static voidchannm(Lextok *n){	char lbuf[512]; 	if (n->sym->type == CHAN)		strcat(Buf, n->sym->name);	else if (n->sym->type == NAME)		strcat(Buf, lookup(n->sym->name)->name);	else if (n->sym->type == STRUCT)	{	Symbol *r = n->sym;		if (r->context)		{	r = findloc(r);			if (!r)			{	strcat(Buf, "*?*");				return;		}	}		ini_struct(r);		printf("%s", r->name);		strcpy(lbuf, "");		struct_name(n->lft, r, 1, lbuf);		strcat(Buf, lbuf);	} else		strcat(Buf, "-");	if (n->lft->lft)	{	sprintf(lbuf, "[%d]", eval(n->lft->lft));		strcat(Buf, lbuf);	}} static voiddifcolumns(Lextok *n, char *tr, int v, int j, Queue *q){	extern int pno; 	if (j == 0)	{	Buf[0] = '\0';		channm(n);		strcat(Buf, (strncmp(tr, "Sen", 3))?"?":"!");	} else		strcat(Buf, ",");	if (tr[0] == '[') strcat(Buf, "[");	sr_buf(v, q->fld_width[j] == MTYPE);	if (j == q->nflds - 1)	{	int cnr;		if (s_trail) cnr = pno; else cnr = X?X->pid - Have_claim:0;		if (tr[0] == '[') strcat(Buf, "]");		pstext(cnr, Buf);	}} static voiddocolumns(Lextok *n, char *tr, int v, int j, Queue *q){	int i; 	if (firstrow)	{	printf("q\\p");		for (i = 0; i < nproc-nstop - Have_claim; i++)			printf(" %3d", i);		printf("\n");		firstrow = 0;	}	if (j == 0)	{	printf("%3d", q->qid);		if (X)		for (i = 0; i < X->pid - Have_claim; i++)			printf("   .");		printf("   ");		Buf[0] = '\0';		channm(n);		printf("%s%c", Buf, (strncmp(tr, "Sen", 3))?'?':'!');	} else		printf(",");	if (tr[0] == '[') printf("[");	sr_mesg(stdout, v, q->fld_width[j] == MTYPE);	if (j == q->nflds - 1)	{	if (tr[0] == '[') printf("]");		printf("\n");	}} typedef struct QH {	int	n;	struct	QH *nxt;} QH;static QH *qh; voidqhide(int q){	QH *p = (QH *) emalloc(sizeof(QH));	p->n = q;	p->nxt = qh;	qh = p;} intqishidden(int q){	QH *p;	for (p = qh; p; p = p->nxt)		if (p->n == q)			return 1;	return 0;} static voidsr_talk(Lextok *n, int v, char *tr, char *a, int j, Queue *q){	char s[128]; 	if (qishidden(eval(n->lft)))		return; 	if (columns)	{	if (columns == 2)			difcolumns(n, tr, v, j, q);		else

Lines 1–500 of 785. Load more