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) continue; 189 if (New > Old) break; /* inner loop */ 190 if (New < Old) goto found; 191 } 192 found: 193 for (j = q->qlen-1; j >= i; j--) 194 for (k = 0; k < q->nflds; k++) 195 { q->contents[(j+1)*q->nflds+k] = 196 q->contents[j*q->nflds+k]; /* shift up */ 197 if (k == 0) 198 q->stepnr[j+1] = q->stepnr[j]; 199 } 200 return i*q->nflds; /* new q offset */ 201 } 202 203 void 204 typ_ck(int ft, int at, char *s) 205 { 206 if ((verbose&32) && ft != at 207 && (ft == CHAN || at == CHAN)) 208 { char buf[128], tag1[64], tag2[64]; 209 (void) sputtype(tag1, ft); 210 (void) sputtype(tag2, at); 211 sprintf(buf, "type-clash in %s, (%s<-> %s)", s, tag1, tag2); 212 non_fatal("%s", buf); 213 } 214 } 215 216 static int 217 a_snd(Queue *q, Lextok *n) 218 { Lextok *m; 219 int i = q->qlen*q->nflds; /* q offset */ 220 int j = 0; /* q field# */ 221 222 if (q->nslots > 0 && q->qlen >= q->nslots) 223 return m_loss; /* q is full */ 224 225 if (TstOnly) return 1; 226 227 if (n->val) i = sa_snd(q, n); /* sorted insert */ 228 229 q->stepnr[i/q->nflds] = depth; 230 231 for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++) 232 { int New = eval(m->lft); 233 q->contents[i+j] = cast_val(q->fld_width[j], New, 0); 234 if ((verbose&16) && depth >= jumpsteps) 235 sr_talk(n, New, "Send ", "->", j, q); 236 typ_ck(q->fld_width[j], Sym_typ(m->lft), "send"); 237 } 238 if ((verbose&16) && depth >= jumpsteps) 239 { for (i = j; i < q->nflds; i++) 240 sr_talk(n, 0, "Send ", "->", i, q); 241 if (j < q->nflds) 242 printf("%3d: warning: missing params in send\n", 243 depth); 244 if (m) 245 printf("%3d: warning: too many params in send\n", 246 depth); 247 } 248 q->qlen++; 249 return 1; 250 } 251 252 static int 253 a_rcv(Queue *q, Lextok *n, int full) 254 { Lextok *m; 255 int i=0, oi, j, k; 256 extern int Rvous; 257 258 if (q->qlen == 0) 259 return 0; /* q is empty */ 260 try_slot: 261 /* test executability */ 262 for (m = n->rgt, j=0; m && j < q->nflds; m = m->rgt, j++) 263 if ((m->lft->ntyp == CONST 264 && q->contents[i*q->nflds+j] != m->lft->val) 265 || (m->lft->ntyp == EVAL 266 && q->contents[i*q->nflds+j] != eval(m->lft->lft))) 267 { if (n->val == 0 /* fifo recv */ 268 || n->val == 2 /* fifo poll */ 269 || ++i >= q->qlen) /* last slot */ 270 return 0; /* no match */ 271 goto try_slot; 272 } 273 if (TstOnly) return 1; 274 275 if (verbose&8) 276 { if (j < q->nflds) 277 printf("%3d: warning: missing params in next recv\n", 278 depth); 279 else if (m) 280 printf("%3d: warning: too many params in next recv\n", 281 depth); 282 } 283 284 /* set the fields */ 285 if (Rvous) 286 { n_rem = n; 287 q_rem = q; 288 } 289 290 oi = q->stepnr[i]; 291 for (m = n->rgt, j = 0; m && j < q->nflds; m = m->rgt, j++) 292 { if (columns && !full) /* was columns == 1 */ 293 continue; 294 if ((verbose&8) && !Rvous && depth >= jumpsteps) 295 { sr_talk(n, q->contents[i*q->nflds+j], 296 (full && n->val < 2)?"Recv ":"[Recv] ", "<-", j, q); 297 } 298 if (!full) 299 continue; /* test */ 300 if (m && m->lft->ntyp != CONST && m->lft->ntyp != EVAL) 301 { (void) setval(m->lft, q->contents[i*q->nflds+j]); 302 typ_ck(q->fld_width[j], Sym_typ(m->lft), "recv"); 303 } 304 if (n->val < 2) /* not a poll */ 305 for (k = i; k < q->qlen-1; k++) 306 { q->contents[k*q->nflds+j] = 307 q->contents[(k+1)*q->nflds+j]; 308 if (j == 0) 309 q->stepnr[k] = q->stepnr[k+1]; 310 } 311 } 312 313 if ((!columns || full) 314 && (verbose&8) && !Rvous && depth >= jumpsteps) 315 for (i = j; i < q->nflds; i++) 316 { sr_talk(n, 0, 317 (full && n->val < 2)?"Recv ":"[Recv] ", "<-", i, q); 318 } 319 if (columns == 2 && full && !Rvous && depth >= jumpsteps) 320 putarrow(oi, depth); 321 322 if (full && n->val < 2) 323 q->qlen--; 324 return 1; 325 } 326 327 static int 328 s_snd(Queue *q, Lextok *n) 329 { Lextok *m; 330 RunList *rX, *sX = X; /* rX=recvr, sX=sendr */ 331 int i, j = 0; /* q field# */ 332 333 for (m = n->rgt; m && j < q->nflds; m = m->rgt, j++) 334 { q->contents[j] = cast_val(q->fld_width[j], eval(m->lft), 0); 335 typ_ck(q->fld_width[j], Sym_typ(m->lft), "rv-send"); 336 } 337 q->qlen = 1; 338 if (!complete_rendez()) 339 { q->qlen = 0; 340 return 0; 341 } 342 if (TstOnly) 343 { q->qlen = 0; 344 return 1; 345 } 346 q->stepnr[0] = depth; 347 if ((verbose&16) && depth >= jumpsteps) 348 { m = n->rgt; 349 rX = X; X = sX; 350 for (j = 0; m && j < q->nflds; m = m->rgt, j++) 351 sr_talk(n, eval(m->lft), "Sent ", "->", j, q); 352 for (i = j; i < q->nflds; i++) 353 sr_talk(n, 0, "Sent ", "->", i, q); 354 if (j < q->nflds) 355 printf("%3d: warning: missing params in rv-send\n", 356 depth); 357 else if (m) 358 printf("%3d: warning: too many params in rv-send\n", 359 depth); 360 X = rX; /* restore receiver's context */ 361 if (!s_trail) 362 { if (!n_rem || !q_rem) 363 fatal("cannot happen, s_snd", (char *) 0); 364 m = n_rem->rgt; 365 for (j = 0; m && j < q->nflds; m = m->rgt, j++) 366 { if (m->lft->ntyp != NAME 367 || strcmp(m->lft->sym->name, "_") != 0) 368 i = eval(m->lft); 369 else i = 0; 370 371 if (verbose&8) 372 sr_talk(n_rem,i,"Recv ","<-",j,q_rem); 373 } 374 if (verbose&8) 375 for (i = j; i < q->nflds; i++) 376 sr_talk(n_rem, 0, "Recv ", "<-", j, q_rem); 377 if (columns == 2) 378 putarrow(depth, depth); 379 } 380 n_rem = (Lextok *) 0; 381 q_rem = (Queue *) 0; 382 } 383 return 1; 384 } 385 386 void 387 channm(Lextok *n) 388 { char lbuf[512]; 389 390 if (n->sym->type == CHAN) 391 strcat(Buf, n->sym->name); 392 else if (n->sym->type == NAME) 393 strcat(Buf, lookup(n->sym->name)->name); 394 else if (n->sym->type == STRUCT) 395 { Symbol *r = n->sym; 396 if (r->context) 397 r = findloc(r); 398 ini_struct(r); 399 printf("%s", r->name); 400 strcpy(lbuf, ""); 401 struct_name(n->lft, r, 1, lbuf); 402 strcat(Buf, lbuf); 403 } else 404 strcat(Buf, "-"); 405 if (n->lft->lft) 406 { sprintf(lbuf, "[%d]", eval(n->lft->lft)); 407 strcat(Buf, lbuf); 408 } 409 } 410 411 static void 412 difcolumns(Lextok *n, char *tr, int v, int j, Queue *q) 413 { extern int pno; 414 415 if (j == 0) 416 { Buf[0] = '\0'; 417 channm(n); 418 strcat(Buf, (strncmp(tr, "Sen", 3))?"?":"!"); 419 } else 420 strcat(Buf, ","); 421 if (tr[0] == '[') strcat(Buf, "["); 422 sr_buf(v, q->fld_width[j] == MTYPE); 423 if (j == q->nflds - 1) 424 { int cnr; 425 if (s_trail) cnr = pno; else cnr = X?X->pid - Have_claim:0; 426 if (tr[0] == '[') strcat(Buf, "]"); 427 pstext(cnr, Buf); 428 } 429 } 430 431 static void 432 docolumns(Lextok *n, char *tr, int v, int j, Queue *q) 433 { int i; 434 435 if (firstrow) 436 { printf("q\\p"); 437 for (i = 0; i < nproc-nstop - Have_claim; i++) 438 printf(" %3d", i); 439 printf("\n"); 440 firstrow = 0; 441 } 442 if (j == 0) 443 { printf("%3d", q->qid); 444 if (X) 445 for (i = 0; i < X->pid - Have_claim; i++) 446 printf(" ."); 447 printf(" "); 448 Buf[0] = '\0'; 449 channm(n); 450 printf("%s%c", Buf, (strncmp(tr, "Sen", 3))?'?':'!'); 451 } else 452 printf(","); 453 if (tr[0] == '[') printf("["); 454 sr_mesg(stdout, v, q->fld_width[j] == MTYPE); 455 if (j == q->nflds - 1) 456 { if (tr[0] == '[') printf("]"); 457 printf("\n"); 458 } 459 } 460 461 typedef struct QH { 462 int n; 463 struct QH *nxt; 464 } QH; 465 QH *qh; 466 467 void 468 qhide(int q) 469 { QH *p = (QH *) emalloc(sizeof(QH)); 470 p->n = q; 471 p->nxt = qh; 472 qh = p; 473 } 474 475 int 476 qishidden(int q) 477 { QH *p; 478 for (p = qh; p; p = p->nxt) 479 if (p->n == q) 480 return 1; 481 return 0; 482 } 483 484 static void 485 sr_talk(Lextok *n, int v, char *tr, char *a, int j, Queue *q) 486 { char s[64]; 487 488 if (qishidden(eval(n->lft))) 489 return; 490 491 if (columns) 492 { if (columns == 2) 493 difcolumns(n, tr, v, j, q); 494 else 495 docolumns(n, tr, v, j, q); 496 return; 497 } 498 if (xspin) 499 { if ((verbose&4) && tr[0] != '[') 500 sprintf(s, "(state -)\t[values: %d", 501 eval(n->lft)); 502 else 503 sprintf(s, "(state -)\t[%d", eval(n->lft)); 504 if (strncmp(tr, "Sen", 3) == 0) 505 strcat(s, "!"); 506 else 507 strcat(s, "?"); 508 } else 509 { strcpy(s, tr); 510 } 511 512 if (j == 0) 513 { whoruns(1); 514 printf("line %3d %s %s", 515 n->ln, n->fn->name, s); 516 } else 517 printf(","); 518 sr_mesg(stdout, v, q->fld_width[j] == MTYPE); 519 520 if (j == q->nflds - 1) 521 { if (xspin) 522 { printf("]\n"); 523 if (!(verbose&4)) printf("\n"); 524 return; 525 } 526 printf("\t%s queue %d (", a, eval(n->lft)); 527 Buf[0] = '\0'; 528 channm(n); 529 printf("%s)\n", Buf); 530 } 531 fflush(stdout); 532 } 533 534 void 535 sr_buf(int v, int j) 536 { int cnt = 1; Lextok *n; 537 char lbuf[512]; 538 539 for (n = Mtype; n && j; n = n->rgt, cnt++) 540 if (cnt == v) 541 { if(strlen(n->lft->sym->name) >= sizeof(lbuf)) 542 { non_fatal("mtype name %s too long", n->lft->sym->name); 543 break; 544 } 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 630 void 631 no_internals(Lextok *n) 632 { char *sp; 633 634 if (!n->sym 635 || !n->sym->name) 636 return; 637 638 sp = n->sym->name; 639 640 if ((strlen(sp) == strlen("_nr_pr") && strcmp(sp, "_nr_pr") == 0) 641 || (strlen(sp) == strlen("_p") && strcmp(sp, "_p") == 0)) 642 { fatal("attempt to assign value to system variable %s", sp); 643 } 644 } 645