1 /***** spin: sched.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 <stdlib.h> 13 #include "spin.h" 14 #include "y.tab.h" 15 16 extern int verbose, s_trail, analyze, no_wrapup; 17 extern char *claimproc, *eventmap, Buf[]; 18 extern Ordered *all_names; 19 extern Symbol *Fname, *context; 20 extern int lineno, nr_errs, dumptab, xspin, jumpsteps, columns; 21 extern int u_sync, Elcnt, interactive, TstOnly, cutoff; 22 extern short has_enabled; 23 extern int limited_vis, old_scope_rules, product, nclaims; 24 25 RunList *X = (RunList *) 0; 26 RunList *run = (RunList *) 0; 27 RunList *LastX = (RunList *) 0; /* previous executing proc */ 28 ProcList *rdy = (ProcList *) 0; 29 Element *LastStep = ZE; 30 int nproc=0, nstop=0, Tval=0; 31 int Rvous=0, depth=0, nrRdy=0, MadeChoice; 32 short Have_claim=0, Skip_claim=0; 33 34 static int Priority_Sum = 0; 35 static void setlocals(RunList *); 36 static void setparams(RunList *, ProcList *, Lextok *); 37 static void talk(RunList *); 38 39 void 40 runnable(ProcList *p, int weight, int noparams) 41 { RunList *r = (RunList *) emalloc(sizeof(RunList)); 42 43 r->n = p->n; 44 r->tn = p->tn; 45 r->b = p->b; 46 r->pid = nproc++ - nstop + Skip_claim; 47 48 if (!noparams && ((verbose&4) || (verbose&32))) 49 printf("Starting %s with pid %d\n", 50 p->n?p->n->name:"--", r->pid); 51 52 if (!p->s) 53 fatal("parsing error, no sequence %s", 54 p->n?p->n->name:"--"); 55 56 r->pc = huntele(p->s->frst, p->s->frst->status, -1); 57 r->ps = p->s; 58 59 if (p->s->last) 60 p->s->last->status |= ENDSTATE; /* normal end state */ 61 62 r->nxt = run; 63 r->prov = p->prov; 64 r->priority = weight; 65 66 if (noparams) setlocals(r); 67 Priority_Sum += weight; 68 69 run = r; 70 } 71 72 ProcList * 73 ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov, enum btypes b) 74 /* n=name, p=formals, s=body det=deterministic prov=provided */ 75 { ProcList *r = (ProcList *) emalloc(sizeof(ProcList)); 76 Lextok *fp, *fpt; int j; extern int Npars; 77 78 r->n = n; 79 r->p = p; 80 r->s = s; 81 r->b = b; 82 r->prov = prov; 83 r->tn = nrRdy++; 84 if (det != 0 && det != 1) 85 { fprintf(stderr, "spin: bad value for det (cannot happen)\n"); 86 } 87 r->det = (short) det; 88 r->nxt = rdy; 89 rdy = r; 90 91 for (fp = p, j = 0; fp; fp = fp->rgt) 92 for (fpt = fp->lft; fpt; fpt = fpt->rgt) 93 j++; /* count # of parameters */ 94 Npars = max(Npars, j); 95 96 return rdy; 97 } 98 99 int 100 find_maxel(Symbol *s) 101 { ProcList *p; 102 103 for (p = rdy; p; p = p->nxt) 104 if (p->n == s) 105 return p->s->maxel++; 106 return Elcnt++; 107 } 108 109 static void 110 formdump(void) 111 { ProcList *p; 112 Lextok *f, *t; 113 int cnt; 114 115 for (p = rdy; p; p = p->nxt) 116 { if (!p->p) continue; 117 cnt = -1; 118 for (f = p->p; f; f = f->rgt) /* types */ 119 for (t = f->lft; t; t = t->rgt) /* formals */ 120 { if (t->ntyp != ',') 121 t->sym->Nid = cnt--; /* overload Nid */ 122 else 123 t->lft->sym->Nid = cnt--; 124 } 125 } 126 } 127 128 void 129 announce(char *w) 130 { 131 if (columns) 132 { extern char Buf[]; 133 extern int firstrow; 134 firstrow = 1; 135 if (columns == 2) 136 { sprintf(Buf, "%d:%s", 137 run->pid - Have_claim, run->n->name); 138 pstext(run->pid - Have_claim, Buf); 139 } else 140 printf("proc %d = %s\n", 141 run->pid - Have_claim, run->n->name); 142 return; 143 } 144 145 if (dumptab 146 || analyze 147 || product 148 || s_trail 149 || !(verbose&4)) 150 return; 151 152 if (w) 153 printf(" 0: proc - (%s) ", w); 154 else 155 whoruns(1); 156 printf("creates proc %2d (%s)", 157 run->pid - Have_claim, 158 run->n->name); 159 if (run->priority > 1) 160 printf(" priority %d", run->priority); 161 printf("\n"); 162 } 163 164 #ifndef MAXP 165 #define MAXP 255 /* matches max nr of processes in verifier */ 166 #endif 167 168 int 169 enable(Lextok *m) 170 { ProcList *p; 171 Symbol *s = m->sym; /* proctype name */ 172 Lextok *n = m->lft; /* actual parameters */ 173 174 if (m->val < 1) m->val = 1; /* minimum priority */ 175 for (p = rdy; p; p = p->nxt) 176 if (strcmp(s->name, p->n->name) == 0) 177 { if (nproc-nstop >= MAXP) 178 { printf("spin: too many processes (%d max)\n", MAXP); 179 break; 180 } 181 runnable(p, m->val, 0); 182 announce((char *) 0); 183 setparams(run, p, n); 184 setlocals(run); /* after setparams */ 185 return run->pid - Have_claim + Skip_claim; /* effective simu pid */ 186 } 187 return 0; /* process not found */ 188 } 189 190 void 191 check_param_count(int i, Lextok *m) 192 { ProcList *p; 193 Symbol *s = m->sym; /* proctype name */ 194 Lextok *f, *t; /* formal pars */ 195 int cnt = 0; 196 197 for (p = rdy; p; p = p->nxt) 198 { if (strcmp(s->name, p->n->name) == 0) 199 { if (m->lft) /* actual param list */ 200 { lineno = m->lft->ln; 201 Fname = m->lft->fn; 202 } 203 for (f = p->p; f; f = f->rgt) /* one type at a time */ 204 for (t = f->lft; t; t = t->rgt) /* count formal params */ 205 { cnt++; 206 } 207 if (i != cnt) 208 { printf("spin: saw %d parameters, expected %d\n", i, cnt); 209 non_fatal("wrong number of parameters", ""); 210 } 211 break; 212 } } 213 } 214 215 void 216 start_claim(int n) 217 { ProcList *p; 218 RunList *r, *q = (RunList *) 0; 219 220 for (p = rdy; p; p = p->nxt) 221 if (p->tn == n && p->b == N_CLAIM) 222 { runnable(p, 1, 1); 223 goto found; 224 } 225 printf("spin: couldn't find claim %d (ignored)\n", n); 226 if (verbose&32) 227 for (p = rdy; p; p = p->nxt) 228 printf("\t%d = %s\n", p->tn, p->n->name); 229 230 Skip_claim = 1; 231 goto done; 232 found: 233 /* move claim to far end of runlist, and reassign it pid 0 */ 234 if (columns == 2) 235 { extern char Buf[]; 236 depth = 0; 237 sprintf(Buf, "%d:%s", 0, p->n->name); 238 pstext(0, Buf); 239 for (r = run; r; r = r->nxt) 240 { if (r->b != N_CLAIM) 241 { sprintf(Buf, "%d:%s", r->pid+1, r->n->name); 242 pstext(r->pid+1, Buf); 243 } } } 244 245 if (run->pid == 0) return; /* it is the first process started */ 246 247 q = run; run = run->nxt; 248 q->pid = 0; q->nxt = (RunList *) 0; /* remove */ 249 done: 250 Have_claim = 1; 251 for (r = run; r; r = r->nxt) 252 { r->pid = r->pid+Have_claim; /* adjust */ 253 if (!r->nxt) 254 { r->nxt = q; 255 break; 256 } } 257 } 258 259 int 260 f_pid(char *n) 261 { RunList *r; 262 int rval = -1; 263 264 for (r = run; r; r = r->nxt) 265 if (strcmp(n, r->n->name) == 0) 266 { if (rval >= 0) 267 { printf("spin: remote ref to proctype %s, ", n); 268 printf("has more than one match: %d and %d\n", 269 rval, r->pid); 270 } else 271 rval = r->pid; 272 } 273 return rval; 274 } 275 276 void 277 wrapup(int fini) 278 { 279 limited_vis = 0; 280 if (columns) 281 { extern void putpostlude(void); 282 if (columns == 2) putpostlude(); 283 if (!no_wrapup) 284 printf("-------------\nfinal state:\n-------------\n"); 285 } 286 if (no_wrapup) 287 goto short_cut; 288 if (nproc != nstop) 289 { int ov = verbose; 290 printf("#processes: %d\n", nproc-nstop - Have_claim + Skip_claim); 291 verbose &= ~4; 292 dumpglobals(); 293 verbose = ov; 294 verbose &= ~1; /* no more globals */ 295 verbose |= 32; /* add process states */ 296 for (X = run; X; X = X->nxt) 297 talk(X); 298 verbose = ov; /* restore */ 299 } 300 printf("%d process%s created\n", 301 nproc - Have_claim + Skip_claim, 302 (xspin || nproc!=1)?"es":""); 303 short_cut: 304 if (xspin) alldone(0); /* avoid an abort from xspin */ 305 if (fini) alldone(1); 306 } 307 308 static char is_blocked[256]; 309 310 static int 311 p_blocked(int p) 312 { int i, j; 313 314 is_blocked[p%256] = 1; 315 for (i = j = 0; i < nproc - nstop; i++) 316 j += is_blocked[i]; 317 if (j >= nproc - nstop) 318 { memset(is_blocked, 0, 256); 319 return 1; 320 } 321 return 0; 322 } 323 324 static Element * 325 silent_moves(Element *e) 326 { Element *f; 327 328 if (e->n) 329 switch (e->n->ntyp) { 330 case GOTO: 331 if (Rvous) break; 332 f = get_lab(e->n, 1); 333 cross_dsteps(e->n, f->n); 334 return f; /* guard against goto cycles */ 335 case UNLESS: 336 return silent_moves(e->sub->this->frst); 337 case NON_ATOMIC: 338 case ATOMIC: 339 case D_STEP: 340 e->n->sl->this->last->nxt = e->nxt; 341 return silent_moves(e->n->sl->this->frst); 342 case '.': 343 return silent_moves(e->nxt); 344 } 345 return e; 346 } 347 348 static RunList * 349 pickproc(RunList *Y) 350 { SeqList *z; Element *has_else; 351 short Choices[256]; 352 int j, k, nr_else = 0; 353 354 if (nproc <= nstop+1) 355 { X = run; 356 return NULL; 357 } 358 if (!interactive || depth < jumpsteps) 359 { /* was: j = (int) Rand()%(nproc-nstop); */ 360 if (Priority_Sum < nproc-nstop) 361 fatal("cannot happen - weights", (char *)0); 362 j = (int) Rand()%Priority_Sum; 363 364 while (j - X->priority >= 0) 365 { j -= X->priority; 366 Y = X; 367 X = X->nxt; 368 if (!X) { Y = NULL; X = run; } 369 } 370 } else 371 { int only_choice = -1; 372 int no_choice = 0, proc_no_ch, proc_k; 373 374 Tval = 0; /* new 4.2.6 */ 375 try_again: printf("Select a statement\n"); 376 try_more: for (X = run, k = 1; X; X = X->nxt) 377 { if (X->pid > 255) break; 378 379 Choices[X->pid] = (short) k; 380 381 if (!X->pc 382 || (X->prov && !eval(X->prov))) 383 { if (X == run) 384 Choices[X->pid] = 0; 385 continue; 386 } 387 X->pc = silent_moves(X->pc); 388 if (!X->pc->sub && X->pc->n) 389 { int unex; 390 unex = !Enabled0(X->pc); 391 if (unex) 392 no_choice++; 393 else 394 only_choice = k; 395 if (!xspin && unex && !(verbose&32)) 396 { k++; 397 continue; 398 } 399 printf("\tchoice %d: ", k++); 400 p_talk(X->pc, 0); 401 if (unex) 402 printf(" unexecutable,"); 403 printf(" ["); 404 comment(stdout, X->pc->n, 0); 405 if (X->pc->esc) printf(" + Escape"); 406 printf("]\n"); 407 } else { 408 has_else = ZE; 409 proc_no_ch = no_choice; 410 proc_k = k; 411 for (z = X->pc->sub, j=0; z; z = z->nxt) 412 { Element *y = silent_moves(z->this->frst); 413 int unex; 414 if (!y) continue; 415 416 if (y->n->ntyp == ELSE) 417 { has_else = (Rvous)?ZE:y; 418 nr_else = k++; 419 continue; 420 } 421 422 unex = !Enabled0(y); 423 if (unex) 424 no_choice++; 425 else 426 only_choice = k; 427 if (!xspin && unex && !(verbose&32)) 428 { k++; 429 continue; 430 } 431 printf("\tchoice %d: ", k++); 432 p_talk(X->pc, 0); 433 if (unex) 434 printf(" unexecutable,"); 435 printf(" ["); 436 comment(stdout, y->n, 0); 437 printf("]\n"); 438 } 439 if (has_else) 440 { if (no_choice-proc_no_ch >= (k-proc_k)-1) 441 { only_choice = nr_else; 442 printf("\tchoice %d: ", nr_else); 443 p_talk(X->pc, 0); 444 printf(" [else]\n"); 445 } else 446 { no_choice++; 447 printf("\tchoice %d: ", nr_else); 448 p_talk(X->pc, 0); 449 printf(" unexecutable, [else]\n"); 450 } } 451 } } 452 X = run; 453 if (k - no_choice < 2 && Tval == 0) 454 { Tval = 1; 455 no_choice = 0; only_choice = -1; 456 goto try_more; 457 } 458 if (xspin) 459 printf("Make Selection %d\n\n", k-1); 460 else 461 { if (k - no_choice < 2) 462 { printf("no executable choices\n"); 463 alldone(0); 464 } 465 printf("Select [1-%d]: ", k-1); 466 } 467 if (!xspin && k - no_choice == 2) 468 { printf("%d\n", only_choice); 469 j = only_choice; 470 } else 471 { char buf[256]; 472 fflush(stdout); 473 if (scanf("%64s", buf) == 0) 474 { printf("\tno input\n"); 475 goto try_again; 476 } 477 j = -1; 478 if (isdigit((int) buf[0])) 479 j = atoi(buf); 480 else 481 { if (buf[0] == 'q') 482 alldone(0); 483 } 484 if (j < 1 || j >= k) 485 { printf("\tchoice is outside range\n"); 486 goto try_again; 487 } } 488 MadeChoice = 0; 489 Y = NULL; 490 for (X = run; X; Y = X, X = X->nxt) 491 { if (!X->nxt 492 || X->nxt->pid > 255 493 || j < Choices[X->nxt->pid]) 494 { 495 MadeChoice = 1+j-Choices[X->pid]; 496 break; 497 } } 498 } 499 return Y; 500 } 501 502 void 503 multi_claims(void) 504 { ProcList *p, *q = NULL; 505 506 if (nclaims > 1) 507 { printf(" the model contains %d never claims:", nclaims); 508 for (p = rdy; p; p = p->nxt) 509 { if (p->b == N_CLAIM) 510 { printf("%s%s", q?", ":" ", p->n->name); 511 q = p; 512 } } 513 printf("\n"); 514 printf(" only one claim is used in a verification run\n"); 515 printf(" choose which one with ./pan -N name (defaults to -N %s)\n", 516 q?q->n->name:"--"); 517 } 518 } 519 520 void 521 sched(void) 522 { Element *e; 523 RunList *Y = NULL; /* previous process in run queue */ 524 RunList *oX; 525 int go, notbeyond = 0; 526 #ifdef PC 527 int bufmax = 100; 528 #endif 529 if (dumptab) 530 { formdump(); 531 symdump(); 532 dumplabels(); 533 return; 534 } 535 536 if (has_enabled && u_sync > 0) 537 { printf("spin: error, cannot use 'enabled()' in "); 538 printf("models with synchronous channels.\n"); 539 nr_errs++; 540 } 541 if (product) 542 { sync_product(); 543 alldone(0); 544 } 545 if (analyze) 546 { gensrc(); 547 multi_claims(); 548 return; 549 } 550 if (s_trail) 551 { match_trail(); 552 return; 553 } 554 if (claimproc) 555 printf("warning: never claim not used in random simulation\n"); 556 if (eventmap) 557 printf("warning: trace assertion not used in random simulation\n"); 558 559 X = run; 560 Y = pickproc(Y); 561 562 while (X) 563 { context = X->n; 564 if (X->pc && X->pc->n) 565 { lineno = X->pc->n->ln; 566 Fname = X->pc->n->fn; 567 } 568 if (cutoff > 0 && depth >= cutoff) 569 { printf("-------------\n"); 570 printf("depth-limit (-u%d steps) reached\n", cutoff); 571 break; 572 } 573 #ifdef PC 574 if (xspin && !interactive && --bufmax <= 0) 575 { int c; /* avoid buffer overflow on pc's */ 576 printf("spin: type return to proceed\n"); 577 fflush(stdout); 578 c = getc(stdin); 579 if (c == 'q') wrapup(0); 580 bufmax = 100; 581 } 582 #endif 583 depth++; LastStep = ZE; 584 oX = X; /* a rendezvous could change it */ 585 go = 1; 586 if (X->prov && X->pc 587 && !(X->pc->status & D_ATOM) 588 && !eval(X->prov)) 589 { if (!xspin && ((verbose&32) || (verbose&4))) 590 { p_talk(X->pc, 1); 591 printf("\t<<Not Enabled>>\n"); 592 } 593 go = 0; 594 } 595 if (go && (e = eval_sub(X->pc))) 596 { if (depth >= jumpsteps 597 && ((verbose&32) || (verbose&4))) 598 { if (X == oX) 599 if (!(e->status & D_ATOM) || (verbose&32)) /* no talking in d_steps */ 600 { p_talk(X->pc, 1); 601 printf(" ["); 602 if (!LastStep) LastStep = X->pc; 603 comment(stdout, LastStep->n, 0); 604 printf("]\n"); 605 } 606 if (verbose&1) dumpglobals(); 607 if (verbose&2) dumplocal(X); 608 609 if (!(e->status & D_ATOM)) 610 if (xspin) 611 printf("\n"); 612 } 613 if (oX != X 614 || (X->pc->status & (ATOM|D_ATOM))) /* new 5.0 */ 615 { e = silent_moves(e); 616 notbeyond = 0; 617 } 618 oX->pc = e; LastX = X; 619 620 if (!interactive) Tval = 0; 621 memset(is_blocked, 0, 256); 622 623 if (X->pc && (X->pc->status & (ATOM|L_ATOM)) 624 && (notbeyond == 0 || oX != X)) 625 { if ((X->pc->status & L_ATOM)) 626 notbeyond = 1; 627 continue; /* no process switch */ 628 } 629 } else 630 { depth--; 631 if (oX->pc && (oX->pc->status & D_ATOM)) 632 { non_fatal("stmnt in d_step blocks", (char *)0); 633 } 634 if (X->pc 635 && X->pc->n 636 && X->pc->n->ntyp == '@' 637 && X->pid == (nproc-nstop-1)) 638 { if (X != run && Y != NULL) 639 Y->nxt = X->nxt; 640 else 641 run = X->nxt; 642 nstop++; 643 Priority_Sum -= X->priority; 644 if (verbose&4) 645 { whoruns(1); 646 dotag(stdout, "terminates\n"); 647 } 648 LastX = X; 649 if (!interactive) Tval = 0; 650 if (nproc == nstop) break; 651 memset(is_blocked, 0, 256); 652 /* proc X is no longer in runlist */ 653 X = (X->nxt) ? X->nxt : run; 654 } else 655 { if (p_blocked(X->pid)) 656 { if (Tval) break; 657 Tval = 1; 658 if (depth >= jumpsteps) 659 { oX = X; 660 X = (RunList *) 0; /* to suppress indent */ 661 dotag(stdout, "timeout\n"); 662 X = oX; 663 } } } } 664 665 if (!run || !X) break; /* new 5.0 */ 666 667 Y = pickproc(X); 668 notbeyond = 0; 669 } 670 context = ZS; 671 wrapup(0); 672 } 673 674 int 675 complete_rendez(void) 676 { RunList *orun = X, *tmp; 677 Element *s_was = LastStep; 678 Element *e; 679 int j, ointer = interactive; 680 681 if (s_trail) 682 return 1; 683 if (orun->pc->status & D_ATOM) 684 fatal("rv-attempt in d_step sequence", (char *)0); 685 Rvous = 1; 686 interactive = 0; 687 688 j = (int) Rand()%Priority_Sum; /* randomize start point */ 689 X = run; 690 while (j - X->priority >= 0) 691 { j -= X->priority; 692 X = X->nxt; 693 if (!X) X = run; 694 } 695 for (j = nproc - nstop; j > 0; j--) 696 { if (X != orun 697 && (!X->prov || eval(X->prov)) 698 && (e = eval_sub(X->pc))) 699 { if (TstOnly) 700 { X = orun; 701 Rvous = 0; 702 goto out; 703 } 704 if ((verbose&32) || (verbose&4)) 705 { tmp = orun; orun = X; X = tmp; 706 if (!s_was) s_was = X->pc; 707 p_talk(s_was, 1); 708 printf(" ["); 709 comment(stdout, s_was->n, 0); 710 printf("]\n"); 711 tmp = orun; orun = X; X = tmp; 712 if (!LastStep) LastStep = X->pc; 713 p_talk(LastStep, 1); 714 printf(" ["); 715 comment(stdout, LastStep->n, 0); 716 printf("]\n"); 717 } 718 Rvous = 0; /* before silent_moves */ 719 X->pc = silent_moves(e); 720 out: interactive = ointer; 721 return 1; 722 } 723 724 X = X->nxt; 725 if (!X) X = run; 726 } 727 Rvous = 0; 728 X = orun; 729 interactive = ointer; 730 return 0; 731 } 732 733 /***** Runtime - Local Variables *****/ 734 735 static void 736 addsymbol(RunList *r, Symbol *s) 737 { Symbol *t; 738 int i; 739 740 for (t = r->symtab; t; t = t->next) 741 if (strcmp(t->name, s->name) == 0 742 && (old_scope_rules 743 || strcmp((const char *)t->bscp, (const char *)s->bscp) == 0)) 744 return; /* it's already there */ 745 746 t = (Symbol *) emalloc(sizeof(Symbol)); 747 t->name = s->name; 748 t->type = s->type; 749 t->hidden = s->hidden; 750 t->nbits = s->nbits; 751 t->nel = s->nel; 752 t->ini = s->ini; 753 t->setat = depth; 754 t->context = r->n; 755 756 t->bscp = (unsigned char *) emalloc(strlen((const char *)s->bscp)+1); 757 strcpy((char *)t->bscp, (const char *)s->bscp); 758 759 if (s->type != STRUCT) 760 { if (s->val) /* if already initialized, copy info */ 761 { t->val = (int *) emalloc(s->nel*sizeof(int)); 762 for (i = 0; i < s->nel; i++) 763 t->val[i] = s->val[i]; 764 } else 765 { (void) checkvar(t, 0); /* initialize it */ 766 } 767 } else 768 { if (s->Sval) 769 fatal("saw preinitialized struct %s", s->name); 770 t->Slst = s->Slst; 771 t->Snm = s->Snm; 772 t->owner = s->owner; 773 /* t->context = r->n; */ 774 } 775 t->next = r->symtab; /* add it */ 776 r->symtab = t; 777 } 778 779 static void 780 setlocals(RunList *r) 781 { Ordered *walk; 782 Symbol *sp; 783 RunList *oX = X; 784 785 X = r; 786 for (walk = all_names; walk; walk = walk->next) 787 { sp = walk->entry; 788 if (sp 789 && sp->context 790 && strcmp(sp->context->name, r->n->name) == 0 791 && sp->Nid >= 0 792 && (sp->type == UNSIGNED 793 || sp->type == BIT 794 || sp->type == MTYPE 795 || sp->type == BYTE 796 || sp->type == CHAN 797 || sp->type == SHORT 798 || sp->type == INT 799 || sp->type == STRUCT)) 800 { if (!findloc(sp)) 801 non_fatal("setlocals: cannot happen '%s'", 802 sp->name); 803 } 804 } 805 X = oX; 806 } 807 808 static void 809 oneparam(RunList *r, Lextok *t, Lextok *a, ProcList *p) 810 { int k; int at, ft; 811 RunList *oX = X; 812 813 if (!a) 814 fatal("missing actual parameters: '%s'", p->n->name); 815 if (t->sym->nel > 1 || t->sym->isarray) 816 fatal("array in parameter list, %s", t->sym->name); 817 k = eval(a->lft); 818 819 at = Sym_typ(a->lft); 820 X = r; /* switch context */ 821 ft = Sym_typ(t); 822 823 if (at != ft && (at == CHAN || ft == CHAN)) 824 { char buf[256], tag1[64], tag2[64]; 825 (void) sputtype(tag1, ft); 826 (void) sputtype(tag2, at); 827 sprintf(buf, "type-clash in params of %s(..), (%s<-> %s)", 828 p->n->name, tag1, tag2); 829 non_fatal("%s", buf); 830 } 831 t->ntyp = NAME; 832 addsymbol(r, t->sym); 833 (void) setval(t, k); 834 835 X = oX; 836 } 837 838 static void 839 setparams(RunList *r, ProcList *p, Lextok *q) 840 { Lextok *f, *a; /* formal and actual pars */ 841 Lextok *t; /* list of pars of 1 type */ 842 843 if (q) 844 { lineno = q->ln; 845 Fname = q->fn; 846 } 847 for (f = p->p, a = q; f; f = f->rgt) /* one type at a time */ 848 for (t = f->lft; t; t = t->rgt, a = (a)?a->rgt:a) 849 { if (t->ntyp != ',') 850 oneparam(r, t, a, p); /* plain var */ 851 else 852 oneparam(r, t->lft, a, p); /* expanded struct */ 853 } 854 } 855 856 Symbol * 857 findloc(Symbol *s) 858 { Symbol *r; 859 860 if (!X) 861 { /* fatal("error, cannot eval '%s' (no proc)", s->name); */ 862 return ZS; 863 } 864 for (r = X->symtab; r; r = r->next) 865 if (strcmp(r->name, s->name) == 0 866 && (old_scope_rules || strcmp((const char *)r->bscp, (const char *)s->bscp) == 0)) 867 break; 868 if (!r) 869 { addsymbol(X, s); 870 r = X->symtab; 871 } 872 return r; 873 } 874 875 int 876 in_bound(Symbol *r, int n) 877 { 878 if (!r) return 0; 879 880 if (n >= r->nel || n < 0) 881 { printf("spin: indexing %s[%d] - size is %d\n", 882 r->name, n, r->nel); 883 non_fatal("indexing array \'%s\'", r->name); 884 return 0; 885 } 886 return 1; 887 } 888 889 int 890 getlocal(Lextok *sn) 891 { Symbol *r, *s = sn->sym; 892 int n = eval(sn->lft); 893 894 r = findloc(s); 895 if (r && r->type == STRUCT) 896 return Rval_struct(sn, r, 1); /* 1 = check init */ 897 if (in_bound(r, n)) 898 return cast_val(r->type, r->val[n], r->nbits); 899 return 0; 900 } 901 902 int 903 setlocal(Lextok *p, int m) 904 { Symbol *r = findloc(p->sym); 905 int n = eval(p->lft); 906 907 if (in_bound(r, n)) 908 { if (r->type == STRUCT) 909 (void) Lval_struct(p, r, 1, m); /* 1 = check init */ 910 else 911 { 912 #if 0 913 if (r->nbits > 0) 914 m = (m & ((1<<r->nbits)-1)); 915 r->val[n] = m; 916 #else 917 r->val[n] = cast_val(r->type, m, r->nbits); 918 #endif 919 r->setat = depth; 920 } } 921 922 return 1; 923 } 924 925 void 926 whoruns(int lnr) 927 { if (!X) return; 928 929 if (lnr) printf("%3d: ", depth); 930 printf("proc "); 931 if (Have_claim && X->pid == 0) 932 printf(" -"); 933 else 934 printf("%2d", X->pid - Have_claim); 935 printf(" (%s) ", X->n->name); 936 } 937 938 static void 939 talk(RunList *r) 940 { 941 if ((verbose&32) || (verbose&4)) 942 { p_talk(r->pc, 1); 943 printf("\n"); 944 if (verbose&1) dumpglobals(); 945 if (verbose&2) dumplocal(r); 946 } 947 } 948 949 void 950 p_talk(Element *e, int lnr) 951 { static int lastnever = -1; 952 static char nbuf[128]; 953 int newnever = -1; 954 955 if (e && e->n) 956 newnever = e->n->ln; 957 958 if (Have_claim && X && X->pid == 0 959 && lastnever != newnever && e) 960 { if (xspin) 961 { printf("MSC: ~G line %d\n", newnever); 962 #if 0 963 printf("%3d: proc - (NEVER) line %d \"never\" ", 964 depth, newnever); 965 printf("(state 0)\t[printf('MSC: never\\\\n')]\n"); 966 } else 967 { printf("%3d: proc - (NEVER) line %d \"never\"\n", 968 depth, newnever); 969 #endif 970 } 971 lastnever = newnever; 972 } 973 974 whoruns(lnr); 975 if (e) 976 { if (e->n) 977 { char *ptr = e->n->fn->name; 978 char *qtr = nbuf; 979 while (*ptr != '\0') 980 { if (*ptr != '"') 981 { *qtr++ = *ptr; 982 } 983 ptr++; 984 } 985 *qtr = '\0'; 986 } else 987 { strcpy(nbuf, "-"); 988 } 989 printf("%s:%d (state %d)", 990 nbuf, 991 e->n?e->n->ln:-1, 992 e->seqno); 993 if (!xspin 994 && ((e->status&ENDSTATE) || has_lab(e, 2))) /* 2=end */ 995 { printf(" <valid end state>"); 996 } 997 } 998 } 999 1000 int 1001 remotelab(Lextok *n) 1002 { int i; 1003 1004 lineno = n->ln; 1005 Fname = n->fn; 1006 if (n->sym->type != 0 && n->sym->type != LABEL) 1007 { printf("spin: error, type: %d\n", n->sym->type); 1008 fatal("not a labelname: '%s'", n->sym->name); 1009 } 1010 if (n->indstep >= 0) 1011 { fatal("remote ref to label '%s' inside d_step", 1012 n->sym->name); 1013 } 1014 if ((i = find_lab(n->sym, n->lft->sym, 1)) == 0) 1015 fatal("unknown labelname: %s", n->sym->name); 1016 return i; 1017 } 1018 1019 int 1020 remotevar(Lextok *n) 1021 { int prno, i, added=0; 1022 RunList *Y, *oX; 1023 Lextok *onl; 1024 Symbol *os; 1025 1026 lineno = n->ln; 1027 Fname = n->fn; 1028 1029 if (!n->lft->lft) 1030 prno = f_pid(n->lft->sym->name); 1031 else 1032 { prno = eval(n->lft->lft); /* pid - can cause recursive call */ 1033 #if 0 1034 if (n->lft->lft->ntyp == CONST) /* user-guessed pid */ 1035 #endif 1036 { prno += Have_claim; 1037 added = Have_claim; 1038 } } 1039 1040 if (prno < 0) 1041 return 0; /* non-existing process */ 1042 #if 0 1043 i = nproc - nstop; 1044 for (Y = run; Y; Y = Y->nxt) 1045 { --i; 1046 printf(" %s: i=%d, prno=%d, ->pid=%d\n", Y->n->name, i, prno, Y->pid); 1047 } 1048 #endif 1049 i = nproc - nstop + Skip_claim; /* 6.0: added Skip_claim */ 1050 for (Y = run; Y; Y = Y->nxt) 1051 if (--i == prno) 1052 { if (strcmp(Y->n->name, n->lft->sym->name) != 0) 1053 { printf("spin: remote reference error on '%s[%d]'\n", 1054 n->lft->sym->name, prno-added); 1055 non_fatal("refers to wrong proctype '%s'", Y->n->name); 1056 } 1057 if (strcmp(n->sym->name, "_p") == 0) 1058 { if (Y->pc) 1059 return Y->pc->seqno; 1060 /* harmless, can only happen with -t */ 1061 return 0; 1062 } 1063 #if 1 1064 /* new 4.0 allow remote variables */ 1065 oX = X; 1066 X = Y; 1067 1068 onl = n->lft; 1069 n->lft = n->rgt; 1070 1071 os = n->sym; 1072 n->sym = findloc(n->sym); 1073 1074 i = getval(n); 1075 1076 n->sym = os; 1077 n->lft = onl; 1078 X = oX; 1079 return i; 1080 #else 1081 break; 1082 #endif 1083 } 1084 printf("remote ref: %s[%d] ", n->lft->sym->name, prno-added); 1085 non_fatal("%s not found", n->sym->name); 1086 printf("have only:\n"); 1087 i = nproc - nstop - 1; 1088 for (Y = run; Y; Y = Y->nxt, i--) 1089 if (!strcmp(Y->n->name, n->lft->sym->name)) 1090 printf("\t%d\t%s\n", i, Y->n->name); 1091 1092 return 0; 1093 } 1094