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
runnable(ProcList * p,int weight,int noparams)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 *
ready(Symbol * n,Lextok * p,Sequence * s,int det,Lextok * prov,enum btypes b)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
find_maxel(Symbol * s)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
formdump(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
announce(char * w)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
enable(Lextok * m)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
check_param_count(int i,Lextok * m)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
start_claim(int n)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
f_pid(char * n)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
wrapup(int fini)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
p_blocked(int p)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 *
silent_moves(Element * e)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 *
pickproc(RunList * Y)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
multi_claims(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
sched(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
complete_rendez(void)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
addsymbol(RunList * r,Symbol * s)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
setlocals(RunList * r)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
oneparam(RunList * r,Lextok * t,Lextok * a,ProcList * p)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
setparams(RunList * r,ProcList * p,Lextok * q)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 *
findloc(Symbol * s)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
in_bound(Symbol * r,int n)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
getlocal(Lextok * sn)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
setlocal(Lextok * p,int m)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
whoruns(int lnr)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
talk(RunList * r)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
p_talk(Element * e,int lnr)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
remotelab(Lextok * n)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
remotevar(Lextok * n)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