123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644 |
- /***** 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 */
- if (New < Old) goto found;
- }
- 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;
- }
- 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);
- 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;
- 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[64];
- 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);
- }
- }
|