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