verif/Spin/Src5.1.6/mesg.c

   1 /***** spin: mesg.c *****/
   2
   3 /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     */
   4 /* All Rights Reserved.  This software is for educational purposes only.  */
   5 /* No guarantee whatsoever is expressed or implied by the distribution of */
   6 /* this code.  Permission is given to distribute this code provided that  */
   7 /* this introductory message is not removed and no monies are exchanged.  */
   8 /* Software written by Gerard J. Holzmann.  For tool documentation see:   */
   9 /*             http://spinroot.com/                                       */
  10 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
  11
  12 #include "spin.h"
  13 #include "y.tab.h"
  14
  15 #ifndef MAXQ
  16 #define MAXQ    2500            /* default max # queues  */
  17 #endif
  18
  19 extern RunList  *X;
  20 extern Symbol   *Fname;
  21 extern Lextok   *Mtype;
  22 extern int      verbose, TstOnly, s_trail, analyze, columns;
  23 extern int      lineno, depth, xspin, m_loss, jumpsteps;
  24 extern int      nproc, nstop;
  25 extern short    Have_claim;
  26
  27 Queue   *qtab = (Queue *) 0;    /* linked list of queues */
  28 Queue   *ltab[MAXQ];            /* linear list of queues */
  29 int     nqs = 0, firstrow = 1;
  30 char    Buf[4096];
  31
  32 static Lextok   *n_rem = (Lextok *) 0;
  33 static Queue    *q_rem = (Queue  *) 0;
  34
  35 static int      a_rcv(Queue *, Lextok *, int);
  36 static int      a_snd(Queue *, Lextok *);
  37 static int      sa_snd(Queue *, Lextok *);
  38 static int      s_snd(Queue *, Lextok *);
  39 extern void     sr_buf(int, int);
  40 extern void     sr_mesg(FILE *, int, int);
  41 extern void     putarrow(int, int);
  42 static void     sr_talk(Lextok *, int, char *, char *, int, Queue *);
  43
  44 int
  45 cnt_mpars(Lextok *n)
  46 {       Lextok *m;
  47         int i=0;
  48
  49         for (m = n; m; m = m->rgt)
  50                 i += Cnt_flds(m);
  51         return i;
  52 }
  53
  54 int
  55 qmake(Symbol *s)
  56 {       Lextok *m;
  57         Queue *q;
  58         int i;
  59
  60         if (!s->ini)
  61                 return 0;
  62
  63         if (nqs >= MAXQ)
  64         {       lineno = s->ini->ln;
  65                 Fname  = s->ini->fn;
  66                 fatal("too many queues (%s)", s->name);
  67         }
  68         if (analyze && nqs >= 255)
  69         {       fatal("too many channel types", (char *)0);
  70         }
  71
  72         if (s->ini->ntyp != CHAN)
  73                 return eval(s->ini);
  74
  75         q = (Queue *) emalloc(sizeof(Queue));
  76         q->qid    = ++nqs;
  77         q->nslots = s->ini->val;
  78         q->nflds  = cnt_mpars(s->ini->rgt);
  79         q->setat  = depth;
  80
  81         i = max(1, q->nslots);  /* 0-slot qs get 1 slot minimum */
  82
  83         q->contents  = (int *) emalloc(q->nflds*i*sizeof(int));
  84         q->fld_width = (int *) emalloc(q->nflds*sizeof(int));
  85         q->stepnr = (int *)   emalloc(i*sizeof(int));
  86
  87         for (m = s->ini->rgt, i = 0; m; m = m->rgt)
  88         {       if (m->sym && m->ntyp == STRUCT)
  89                         i = Width_set(q->fld_width, i, getuname(m->sym));
  90                 else
  91                         q->fld_width[i++] = m->ntyp;
  92         }
  93         q->nxt = qtab;
  94         qtab = q;
  95         ltab[q->qid-1] = q;
  96
  97         return q->qid;
  98 }
  99
 100 int
 101 qfull(Lextok *n)
 102 {       int whichq = eval(n->lft)-1;
 103
 104         if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
 105                 return (ltab[whichq]->qlen >= ltab[whichq]->nslots);
 106         return 0;
 107 }
 108
 109 int
 110 qlen(Lextok *n)
 111 {       int whichq = eval(n->lft)-1;
 112
 113         if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
 114                 return ltab[whichq]->qlen;
 115         return 0;
 116 }
 117
 118 int
 119 q_is_sync(Lextok *n)
 120 {       int whichq = eval(n->lft)-1;
 121
 122         if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
 123                 return (ltab[whichq]->nslots == 0);
 124         return 0;
 125 }
 126
 127 int
 128 qsend(Lextok *n)
 129 {       int whichq = eval(n->lft)-1;
 130
 131         if (whichq == -1)
 132         {       printf("Error: sending to an uninitialized chan\n");
 133                 whichq = 0;
 134                 return 0;
 135         }
 136         if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
 137         {       ltab[whichq]->setat = depth;
 138                 if (ltab[whichq]->nslots > 0)
 139                         return a_snd(ltab[whichq], n);
 140                 else
 141                         return s_snd(ltab[whichq], n);
 142         }
 143         return 0;
 144 }
 145
 146 int
 147 qrecv(Lextok *n, int full)
 148 {       int whichq = eval(n->lft)-1;
 149
 150         if (whichq == -1)
 151         {       if (n->sym && !strcmp(n->sym->name, "STDIN"))
 152                 {       Lextok *m;
 153
 154                         if (TstOnly) return 1;
 155
 156                         for (m = n->rgt; m; m = m->rgt)
 157                         if (m->lft->ntyp != CONST && m->lft->ntyp != EVAL)
 158                         {       int c = getchar();
 159                                 (void) setval(m->lft, c);
 160                         } else
 161                                 fatal("invalid use of STDIN", (char *)0);
 162
 163                         whichq = 0;
 164                         return 1;
 165                 }
 166                 printf("Error: receiving from an uninitialized chan %s\n",
 167                         n->sym?n->sym->name:"");
 168                 whichq = 0;
 169                 return 0;
 170         }
 171         if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
 172         {       ltab[whichq]->setat = depth;
 173                 return a_rcv(ltab[whichq], n, full);
 174         }
 175         return 0;
 176 }
 177
 178 static int
 179 sa_snd(Queue *q, Lextok *n)     /* sorted asynchronous */
 180 {       Lextok *m;
 181         int i, j, k;
 182         int New, Old;
 183
 184         for (i = 0; i < q->qlen; i++)
 185         for (j = 0, m = n->rgt; m && j < q->nflds; m = m->rgt, j++)
 186         {       New = cast_val(q->fld_width[j], eval(m->lft), 0);
 187                 Old = q->contents[i*q->nflds+j];
 188                 if (New == Old)
 189                         continue;
 190                 if (New >  Old)
 191                         break;  /* inner loop */
 192                 goto found;     /* New < Old */
 193         }
 194 found:
 195         for (j = q->qlen-1; j >= i; j--)
 196         for (k = 0; k < q->nflds; k++)
 197         {       q->contents[(j+1)*q->nflds+k] =
 198                         q->contents[j*q->nflds+k];      /* shift up */
 199                 if (k == 0)
 200                         q->stepnr[j+1] = q->stepnr[j];
 201         }
 202         return i*q->nflds;                              /* new q offset */
 203 }
 204
 205 void
 206 typ_ck(int ft, int at, char *s)
 207 {
 208         if ((verbose&32) && ft != at
 209         && (ft == CHAN || at == CHAN))
 210         {       char buf[128], tag1[64], tag2[64];
 211                 (void) sputtype(tag1, ft);
 212                 (void) sputtype(tag2, at);
 213                 sprintf(buf, "type-clash in %s, (%s<-> %s)", s, tag1, tag2);
 214                 non_fatal("%s", buf);
 215         }
 216 }
 217
 218 static int
 219 a_snd(Queue *q, Lextok *n)
 220 {       Lextok *m;
 221         int i = q->qlen*q->nflds;       /* q offset */
 222         int j = 0;                      /* q field# */
 223
 224         if (q->nslots > 0 && q->qlen >= q->nslots)
 225                 return m_loss;  /* q is full */
 226
 227         if (TstOnly) return 1;
 228
 229         if (n->val) i = sa_snd(q, n);   /* sorted insert */
 230
 231         q->stepnr[i/q->nflds] = depth;
 232
 233         for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++)
 234         {       int New = eval(m->lft);
 235                 q->contents[i+j] = cast_val(q->fld_width[j], New, 0);
 236                 if ((verbose&16) && depth >= jumpsteps)
 237                         sr_talk(n, New, "Send ", "->", j, q);
 238                 typ_ck(q->fld_width[j], Sym_typ(m->lft), "send");
 239         }
 240         if ((verbose&16) && depth >= jumpsteps)
 241         {       for (i = j; i < q->nflds; i++)
 242                         sr_talk(n, 0, "Send ", "->", i, q);
 243                 if (j < q->nflds)
 244                         printf("%3d: warning: missing params in send\n",
 245                                 depth);
 246                 if (m)
 247                         printf("%3d: warning: too many params in send\n",
 248                                 depth);
 249         }
 250         q->qlen++;
 251         return 1;
 252 }
 253
 254 static int
 255 a_rcv(Queue *q, Lextok *n, int full)
 256 {       Lextok *m;
 257         int i=0, oi, j, k;
 258         extern int Rvous;
 259
 260         if (q->qlen == 0)
 261                 return 0;       /* q is empty */
 262 try_slot:
 263         /* test executability */
 264         for (m = n->rgt, j=0; m && j < q->nflds; m = m->rgt, j++)
 265                 if ((m->lft->ntyp == CONST
 266                    && q->contents[i*q->nflds+j] != m->lft->val)
 267                 ||  (m->lft->ntyp == EVAL
 268                    && q->contents[i*q->nflds+j] != eval(m->lft->lft)))
 269                 {       if (n->val == 0         /* fifo recv */
 270                         ||  n->val == 2         /* fifo poll */
 271                         || ++i >= q->qlen)      /* last slot */
 272                                 return 0;       /* no match  */
 273                         goto try_slot;
 274                 }
 275         if (TstOnly) return 1;
 276
 277         if (verbose&8)
 278         {       if (j < q->nflds)
 279                         printf("%3d: warning: missing params in next recv\n",
 280                                 depth);
 281                 else if (m)
 282                         printf("%3d: warning: too many params in next recv\n",
 283                                 depth);
 284         }
 285
 286         /* set the fields */
 287         if (Rvous)
 288         {       n_rem = n;
 289                 q_rem = q;
 290         }
 291
 292         oi = q->stepnr[i];
 293         for (m = n->rgt, j = 0; m && j < q->nflds; m = m->rgt, j++)
 294         {       if (columns && !full)   /* was columns == 1 */
 295                         continue;
 296                 if ((verbose&8) && !Rvous && depth >= jumpsteps)
 297                 {       sr_talk(n, q->contents[i*q->nflds+j],
 298                         (full && n->val < 2)?"Recv ":"[Recv] ", "<-", j, q);
 299                 }
 300                 if (!full)
 301                         continue;       /* test */
 302                 if (m && m->lft->ntyp != CONST && m->lft->ntyp != EVAL)
 303                 {       (void) setval(m->lft, q->contents[i*q->nflds+j]);
 304                         typ_ck(q->fld_width[j], Sym_typ(m->lft), "recv");
 305                 }
 306                 if (n->val < 2)         /* not a poll */
 307                 for (k = i; k < q->qlen-1; k++)
 308                 {       q->contents[k*q->nflds+j] =
 309                           q->contents[(k+1)*q->nflds+j];
 310                         if (j == 0)
 311                           q->stepnr[k] = q->stepnr[k+1];
 312                 }
 313         }
 314
 315         if ((!columns || full)
 316         && (verbose&8) && !Rvous && depth >= jumpsteps)
 317         for (i = j; i < q->nflds; i++)
 318         {       sr_talk(n, 0,
 319                 (full && n->val < 2)?"Recv ":"[Recv] ", "<-", i, q);
 320         }
 321         if (columns == 2 && full && !Rvous && depth >= jumpsteps)
 322                 putarrow(oi, depth);
 323
 324         if (full && n->val < 2)
 325                 q->qlen--;
 326         return 1;
 327 }
 328
 329 static int
 330 s_snd(Queue *q, Lextok *n)
 331 {       Lextok *m;
 332         RunList *rX, *sX = X;   /* rX=recvr, sX=sendr */
 333         int i, j = 0;   /* q field# */
 334
 335         for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++)
 336         {       q->contents[j] = cast_val(q->fld_width[j], eval(m->lft), 0);
 337                 typ_ck(q->fld_width[j], Sym_typ(m->lft), "rv-send");
 338         }
 339         q->qlen = 1;
 340         if (!complete_rendez())
 341         {       q->qlen = 0;
 342                 return 0;
 343         }
 344         if (TstOnly)
 345         {       q->qlen = 0;
 346                 return 1;
 347         }
 348         q->stepnr[0] = depth;
 349         if ((verbose&16) && depth >= jumpsteps)
 350         {       m = n->rgt;
 351                 rX = X; X = sX;
 352                 for (j = 0; m && j < q->nflds; m = m->rgt, j++)
 353                         sr_talk(n, eval(m->lft), "Sent ", "->", j, q);
 354                 for (i = j; i < q->nflds; i++)
 355                         sr_talk(n, 0, "Sent ", "->", i, q);
 356                 if (j < q->nflds)
 357                           printf("%3d: warning: missing params in rv-send\n",
 358                                 depth);
 359                 else if (m)
 360                           printf("%3d: warning: too many params in rv-send\n",
 361                                 depth);
 362                 X = rX; /* restore receiver's context */
 363                 if (!s_trail)
 364                 {       if (!n_rem || !q_rem)
 365                                 fatal("cannot happen, s_snd", (char *) 0);
 366                         m = n_rem->rgt;
 367                         for (j = 0; m && j < q->nflds; m = m->rgt, j++)
 368                         {       if (m->lft->ntyp != NAME
 369                                 ||  strcmp(m->lft->sym->name, "_") != 0)
 370                                         i = eval(m->lft);
 371                                 else    i = 0;
 372
 373                                 if (verbose&8)
 374                                 sr_talk(n_rem,i,"Recv ","<-",j,q_rem);
 375                         }
 376                         if (verbose&8)
 377                         for (i = j; i < q->nflds; i++)
 378                                 sr_talk(n_rem, 0, "Recv ", "<-", j, q_rem);
 379                         if (columns == 2)
 380                                 putarrow(depth, depth);
 381                 }
 382                 n_rem = (Lextok *) 0;
 383                 q_rem = (Queue *) 0;
 384         }
 385         return 1;
 386 }
 387
 388 static void
 389 channm(Lextok *n)
 390 {       char lbuf[512];
 391
 392         if (n->sym->type == CHAN)
 393                 strcat(Buf, n->sym->name);
 394         else if (n->sym->type == NAME)
 395                 strcat(Buf, lookup(n->sym->name)->name);
 396         else if (n->sym->type == STRUCT)
 397         {       Symbol *r = n->sym;
 398                 if (r->context)
 399                 {       r = findloc(r);
 400                         if (!r)
 401                         {       strcat(Buf, "*?*");
 402                                 return;
 403                 }       }
 404                 ini_struct(r);
 405                 printf("%s", r->name);
 406                 strcpy(lbuf, "");
 407                 struct_name(n->lft, r, 1, lbuf);
 408                 strcat(Buf, lbuf);
 409         } else
 410                 strcat(Buf, "-");
 411         if (n->lft->lft)
 412         {       sprintf(lbuf, "[%d]", eval(n->lft->lft));
 413                 strcat(Buf, lbuf);
 414         }
 415 }
 416
 417 static void
 418 difcolumns(Lextok *n, char *tr, int v, int j, Queue *q)
 419 {       extern int pno;
 420
 421         if (j == 0)
 422         {       Buf[0] = '\0';
 423                 channm(n);
 424                 strcat(Buf, (strncmp(tr, "Sen", 3))?"?":"!");
 425         } else
 426                 strcat(Buf, ",");
 427         if (tr[0] == '[') strcat(Buf, "[");
 428         sr_buf(v, q->fld_width[j] == MTYPE);
 429         if (j == q->nflds - 1)
 430         {       int cnr;
 431                 if (s_trail) cnr = pno; else cnr = X?X->pid - Have_claim:0;
 432                 if (tr[0] == '[') strcat(Buf, "]");
 433                 pstext(cnr, Buf);
 434         }
 435 }
 436
 437 static void
 438 docolumns(Lextok *n, char *tr, int v, int j, Queue *q)
 439 {       int i;
 440
 441         if (firstrow)
 442         {       printf("q\\p");
 443                 for (i = 0; i < nproc-nstop - Have_claim; i++)
 444                         printf(" %3d", i);
 445                 printf("\n");
 446                 firstrow = 0;
 447         }
 448         if (j == 0)
 449         {       printf("%3d", q->qid);
 450                 if (X)
 451                 for (i = 0; i < X->pid - Have_claim; i++)
 452                         printf("   .");
 453                 printf("   ");
 454                 Buf[0] = '\0';
 455                 channm(n);
 456                 printf("%s%c", Buf, (strncmp(tr, "Sen", 3))?'?':'!');
 457         } else
 458                 printf(",");
 459         if (tr[0] == '[') printf("[");
 460         sr_mesg(stdout, v, q->fld_width[j] == MTYPE);
 461         if (j == q->nflds - 1)
 462         {       if (tr[0] == '[') printf("]");
 463                 printf("\n");
 464         }
 465 }
 466
 467 typedef struct QH {
 468         int     n;
 469         struct  QH *nxt;
 470 } QH;
 471 static QH *qh;
 472
 473 void
 474 qhide(int q)
 475 {       QH *p = (QH *) emalloc(sizeof(QH));
 476         p->n = q;
 477         p->nxt = qh;
 478         qh = p;
 479 }
 480
 481 int
 482 qishidden(int q)
 483 {       QH *p;
 484         for (p = qh; p; p = p->nxt)
 485                 if (p->n == q)
 486                         return 1;
 487         return 0;
 488 }
 489
 490 static void
 491 sr_talk(Lextok *n, int v, char *tr, char *a, int j, Queue *q)
 492 {       char s[128];
 493
 494         if (qishidden(eval(n->lft)))
 495                 return;
 496
 497         if (columns)
 498         {       if (columns == 2)
 499                         difcolumns(n, tr, v, j, q);
 500                 else
 501                         docolumns(n, tr, v, j, q);
 502                 return;
 503         }
 504         if (xspin)
 505         {       if ((verbose&4) && tr[0] != '[')
 506                 sprintf(s, "(state -)\t[values: %d",
 507                         eval(n->lft));
 508                 else
 509                 sprintf(s, "(state -)\t[%d", eval(n->lft));
 510                 if (strncmp(tr, "Sen", 3) == 0)
 511                         strcat(s, "!");
 512                 else
 513                         strcat(s, "?");
 514         } else
 515         {       strcpy(s, tr);
 516         }
 517
 518         if (j == 0)
 519         {       whoruns(1);
 520                 printf("line %3d %s %s",
 521                         n->ln, n->fn->name, s);
 522         } else
 523                 printf(",");
 524         sr_mesg(stdout, v, q->fld_width[j] == MTYPE);
 525
 526         if (j == q->nflds - 1)
 527         {       if (xspin)
 528                 {       printf("]\n");
 529                         if (!(verbose&4)) printf("\n");
 530                         return;
 531                 }
 532                 printf("\t%s queue %d (", a, eval(n->lft));
 533                 Buf[0] = '\0';
 534                 channm(n);
 535                 printf("%s)\n", Buf);
 536         }
 537         fflush(stdout);
 538 }
 539
 540 void
 541 sr_buf(int v, int j)
 542 {       int cnt = 1; Lextok *n;
 543         char lbuf[512];
 544
 545         for (n = Mtype; n && j; n = n->rgt, cnt++)
 546                 if (cnt == v)
 547                 {       if(strlen(n->lft->sym->name) >= sizeof(lbuf))
 548                         {       non_fatal("mtype name %s too long", n->lft->sym->name);
 549                                 break;
 550                         }
 551                         sprintf(lbuf, "%s", n->lft->sym->name);
 552                         strcat(Buf, lbuf);
 553                         return;
 554                 }
 555         sprintf(lbuf, "%d", v);
 556         strcat(Buf, lbuf);
 557 }
 558
 559 void
 560 sr_mesg(FILE *fd, int v, int j)
 561 {       Buf[0] ='\0';
 562         sr_buf(v, j);
 563         fprintf(fd, Buf);
 564 }
 565
 566 void
 567 doq(Symbol *s, int n, RunList *r)
 568 {       Queue *q;
 569         int j, k;
 570
 571         if (!s->val)    /* uninitialized queue */
 572                 return;
 573         for (q = qtab; q; q = q->nxt)
 574         if (q->qid == s->val[n])
 575         {       if (xspin > 0
 576                 && (verbose&4)
 577                 && q->setat < depth)
 578                         continue;
 579                 if (q->nslots == 0)
 580                         continue; /* rv q always empty */
 581                 printf("\t\tqueue %d (", q->qid);
 582                 if (r)
 583                 printf("%s(%d):", r->n->name, r->pid - Have_claim);
 584                 if (s->nel != 1)
 585                   printf("%s[%d]): ", s->name, n);
 586                 else
 587                   printf("%s): ", s->name);
 588                 for (k = 0; k < q->qlen; k++)
 589                 {       printf("[");
 590                         for (j = 0; j < q->nflds; j++)
 591                         {       if (j > 0) printf(",");
 592                                 sr_mesg(stdout, q->contents[k*q->nflds+j],
 593                                         q->fld_width[j] == MTYPE);
 594                         }
 595                         printf("]");
 596                 }
 597                 printf("\n");
 598                 break;
 599         }
 600 }
 601
 602 void
 603 nochan_manip(Lextok *p, Lextok *n, int d)
 604 {       int e = 1;
 605
 606         if (d == 0 && p->sym && p->sym->type == CHAN)
 607         {       setaccess(p->sym, ZS, 0, 'L');
 608
 609                 if (n && n->ntyp == CONST)
 610                         fatal("invalid asgn to chan", (char *) 0);
 611
 612                 if (n && n->sym && n->sym->type == CHAN)
 613                 {       setaccess(n->sym, ZS, 0, 'V');
 614                         return;
 615                 }
 616         }
 617
 618         if (!n || n->ntyp == LEN || n->ntyp == RUN)
 619                 return;
 620
 621         if (n->sym && n->sym->type == CHAN)
 622         {       if (d == 1)
 623                         fatal("invalid use of chan name", (char *) 0);
 624                 else
 625                         setaccess(n->sym, ZS, 0, 'V');
 626         }
 627
 628         if (n->ntyp == NAME
 629         ||  n->ntyp == '.')
 630                 e = 0;  /* array index or struct element */
 631
 632         nochan_manip(p, n->lft, e);
 633         nochan_manip(p, n->rgt, 1);
 634 }
 635
 636 void
 637 no_internals(Lextok *n)
 638 {       char *sp;
 639
 640         if (!n->sym
 641         ||  !n->sym->name)
 642                 return;
 643
 644         sp = n->sym->name;
 645
 646         if ((strlen(sp) == strlen("_nr_pr") && strcmp(sp, "_nr_pr") == 0)
 647         ||  (strlen(sp) == strlen("_p") && strcmp(sp, "_p") == 0))
 648         {       fatal("attempt to assign value to system variable %s", sp);
 649         }
 650 }