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