sched.c 19 KB

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