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