--- /dev/null
+/***** 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 *);
+
+int
+cnt_mpars(Lextok *n)
+{ Lextok *m;
+ int i=0;
+
+ for (m = n; m; m = m->rgt)
+ i += Cnt_flds(m);
+ return i;
+}
+
+int
+qmake(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;
+}
+
+int
+qfull(Lextok *n)
+{ int whichq = eval(n->lft)-1;
+
+ if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
+ return (ltab[whichq]->qlen >= ltab[whichq]->nslots);
+ return 0;
+}
+
+int
+qlen(Lextok *n)
+{ int whichq = eval(n->lft)-1;
+
+ if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
+ return ltab[whichq]->qlen;
+ return 0;
+}
+
+int
+q_is_sync(Lextok *n)
+{ int whichq = eval(n->lft)-1;
+
+ if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
+ return (ltab[whichq]->nslots == 0);
+ return 0;
+}
+
+int
+qsend(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;
+}
+
+int
+qrecv(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 int
+sa_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 */
+}
+
+void
+typ_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 int
+a_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 int
+a_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 int
+s_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 void
+channm(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 void
+difcolumns(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 void
+docolumns(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;
+
+void
+qhide(int q)
+{ QH *p = (QH *) emalloc(sizeof(QH));
+ p->n = q;
+ p->nxt = qh;
+ qh = p;
+}
+
+int
+qishidden(int q)
+{ QH *p;
+ for (p = qh; p; p = p->nxt)
+ if (p->n == q)
+ return 1;
+ return 0;
+}
+
+static void
+sr_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
+ docolumns(n, tr, v, j, q);
+ return;
+ }
+ if (xspin)
+ { if ((verbose&4) && tr[0] != '[')
+ sprintf(s, "(state -)\t[values: %d",
+ eval(n->lft));
+ else
+ sprintf(s, "(state -)\t[%d", eval(n->lft));
+ if (strncmp(tr, "Sen", 3) == 0)
+ strcat(s, "!");
+ else
+ strcat(s, "?");
+ } else
+ { strcpy(s, tr);
+ }
+
+ if (j == 0)
+ { whoruns(1);
+ printf("line %3d %s %s",
+ n->ln, n->fn->name, s);
+ } else
+ printf(",");
+ sr_mesg(stdout, v, q->fld_width[j] == MTYPE);
+
+ if (j == q->nflds - 1)
+ { if (xspin)
+ { printf("]\n");
+ if (!(verbose&4)) printf("\n");
+ return;
+ }
+ printf("\t%s queue %d (", a, eval(n->lft));
+ Buf[0] = '\0';
+ channm(n);
+ printf("%s)\n", Buf);
+ }
+ fflush(stdout);
+}
+
+void
+sr_buf(int v, int j)
+{ int cnt = 1; Lextok *n;
+ char lbuf[512];
+
+ for (n = Mtype; n && j; n = n->rgt, cnt++)
+ if (cnt == v)
+ { if(strlen(n->lft->sym->name) >= sizeof(lbuf))
+ { non_fatal("mtype name %s too long", n->lft->sym->name);
+ break;
+ }
+ sprintf(lbuf, "%s", n->lft->sym->name);
+ strcat(Buf, lbuf);
+ return;
+ }
+ sprintf(lbuf, "%d", v);
+ strcat(Buf, lbuf);
+}
+
+void
+sr_mesg(FILE *fd, int v, int j)
+{ Buf[0] ='\0';
+ sr_buf(v, j);
+ fprintf(fd, Buf);
+}
+
+void
+doq(Symbol *s, int n, RunList *r)
+{ Queue *q;
+ int j, k;
+
+ if (!s->val) /* uninitialized queue */
+ return;
+ for (q = qtab; q; q = q->nxt)
+ if (q->qid == s->val[n])
+ { if (xspin > 0
+ && (verbose&4)
+ && q->setat < depth)
+ continue;
+ if (q->nslots == 0)
+ continue; /* rv q always empty */
+ printf("\t\tqueue %d (", q->qid);
+ if (r)
+ printf("%s(%d):", r->n->name, r->pid - Have_claim);
+ if (s->nel != 1)
+ printf("%s[%d]): ", s->name, n);
+ else
+ printf("%s): ", s->name);
+ for (k = 0; k < q->qlen; k++)
+ { printf("[");
+ for (j = 0; j < q->nflds; j++)
+ { if (j > 0) printf(",");
+ sr_mesg(stdout, q->contents[k*q->nflds+j],
+ q->fld_width[j] == MTYPE);
+ }
+ printf("]");
+ }
+ printf("\n");
+ break;
+ }
+}
+
+void
+nochan_manip(Lextok *p, Lextok *n, int d)
+{ int e = 1;
+
+ if (d == 0 && p->sym && p->sym->type == CHAN)
+ { setaccess(p->sym, ZS, 0, 'L');
+
+ if (n && n->ntyp == CONST)
+ fatal("invalid asgn to chan", (char *) 0);
+
+ if (n && n->sym && n->sym->type == CHAN)
+ { setaccess(n->sym, ZS, 0, 'V');
+ return;
+ }
+ }
+
+ if (!n || n->ntyp == LEN || n->ntyp == RUN)
+ return;
+
+ if (n->sym && n->sym->type == CHAN)
+ { if (d == 1)
+ fatal("invalid use of chan name", (char *) 0);
+ else
+ setaccess(n->sym, ZS, 0, 'V');
+ }
+
+ if (n->ntyp == NAME
+ || n->ntyp == '.')
+ e = 0; /* array index or struct element */
+
+ nochan_manip(p, n->lft, e);
+ nochan_manip(p, n->rgt, 1);
+}
+
+void
+no_internals(Lextok *n)
+{ char *sp;
+
+ if (!n->sym
+ || !n->sym->name)
+ return;
+
+ sp = n->sym->name;
+
+ if ((strlen(sp) == strlen("_nr_pr") && strcmp(sp, "_nr_pr") == 0)
+ || (strlen(sp) == strlen("_p") && strcmp(sp, "_p") == 0))
+ { fatal("attempt to assign value to system variable %s", sp);
+ }
+}
projects / lttv.git / blobdiff