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