1 /***** spin: run.c *****/
4 * This file is part of the public release of Spin. It is subject to the
5 * terms in the LICENSE file that is included in this source directory.
6 * Tool documentation is available at http://spinroot.com
13 extern RunList *X, *run;
15 extern Element *LastStep;
16 extern int Rvous, lineno, Tval, interactive, MadeChoice, Priority_Sum;
17 extern int TstOnly, verbose, s_trail, xspin, jumpsteps, depth;
18 extern int analyze, nproc, nstop, no_print, like_java, old_priority_rules;
19 extern short Have_claim;
22 static int E_Check = 0, Escape_Check = 0;
24 static int eval_sync(Element *);
25 static int pc_enabled(Lextok *n);
26 static int get_priority(Lextok *n);
27 static void set_priority(Lextok *n, Lextok *m);
28 extern void sr_buf(int, int);
37 { /* CACM 31(10), Oct 1988 */
38 Seed = 16807*(Seed%127773) - 2836*(Seed/127773);
39 if (Seed <= 0) Seed += 2147483647;
44 rev_escape(SeqList *e)
45 { Element *r = (Element *) 0;
48 { if ((r = rev_escape(e->nxt)) == ZE) /* reversed order */
49 { r = eval_sub(e->this->frst);
59 int i, j, k, only_pos;
64 printf("\n\teval_sub(%d %s: line %d) ",
65 e->Seqno, e->esc?"+esc":"", e->n?e->n->ln:0);
66 comment(stdout, e->n, 0);
69 if (e->n->ntyp == GOTO)
70 { if (Rvous) return ZE;
73 f = huntele(f, e->status, -1); /* 5.2.3: was missing */
74 cross_dsteps(e->n, f->n);
76 printf("GOTO leads to %d\n", f->seqno);
80 if (e->n->ntyp == UNLESS)
81 { /* escapes were distributed into sequence */
82 return eval_sub(e->sub->this->frst);
83 } else if (e->sub) /* true for IF, DO, and UNLESS */
84 { Element *has_else = ZE;
85 Element *bas_else = ZE;
86 int nr_else = 0, nr_choices = 0;
90 && !MadeChoice && !E_Check
92 && !(e->status&(D_ATOM))
93 && depth >= jumpsteps)
94 { printf("Select stmnt (");
95 whoruns(0); printf(")\n");
97 { printf("\tchoice 0: other process\n");
101 for (z = e->sub, j=0; z; z = z->nxt)
104 && !MadeChoice && !E_Check
106 && !(e->status&(D_ATOM))
107 && depth >= jumpsteps
109 && (xspin || (verbose&32) || Enabled0(z->this->frst)))
110 { if (z->this->frst->n->ntyp == ELSE)
111 { has_else = (Rvous)?ZE:z->this->frst->nxt;
115 printf("\tchoice %d: ", j);
117 if (z->this->frst->n)
118 printf("line %d, ", z->this->frst->n->ln);
120 if (!Enabled0(z->this->frst))
121 printf("unexecutable, ");
126 comment(stdout, z->this->frst->n, 0);
130 if (nr_choices == 0 && has_else)
131 { printf("\tchoice %d: (else)\n", nr_else);
135 if (nr_choices <= 1 && only_pos != -1 && !MadeChoice)
136 { MadeChoice = only_pos;
139 if (interactive && depth >= jumpsteps
141 && !(e->status&(D_ATOM))
146 printf("Make Selection %d\n\n", j);
148 printf("Select [0-%d]: ", j);
150 if (scanf("%64s", buf) <= 0)
151 { printf("no input\n");
154 if (isdigit((int)buf[0]))
166 { if (k != 0) printf("\tchoice outside range\n");
171 { if (e->n && e->n->indstep >= 0)
172 k = 0; /* select 1st executable guard */
174 k = Rand()%j; /* nondeterminism */
179 for (i = 0, z = e->sub; i < j+k; i++)
181 && z->this->frst->n->ntyp == ELSE)
182 { bas_else = z->this->frst;
183 has_else = (Rvous)?ZE:bas_else->nxt;
184 if (!interactive || depth < jumpsteps
186 || (e->status&(D_ATOM)))
187 { z = (z->nxt)?z->nxt:e->sub;
192 && ((z->this->frst->n->ntyp == ATOMIC
193 || z->this->frst->n->ntyp == D_STEP)
194 && z->this->frst->n->sl->this->frst->n->ntyp == ELSE))
195 { bas_else = z->this->frst->n->sl->this->frst;
196 has_else = (Rvous)?ZE:bas_else->nxt;
197 if (!interactive || depth < jumpsteps
199 || (e->status&(D_ATOM)))
200 { z = (z->nxt)?z->nxt:e->sub;
205 { if ((f = eval_sub(z->this->frst)) != ZE)
207 else if (interactive && depth >= jumpsteps
208 && !(e->status&(D_ATOM)))
209 { if (!E_Check && !Escape_Check)
210 printf("\tunexecutable\n");
213 z = (z->nxt)?z->nxt:e->sub;
218 { if (e->n->ntyp == ATOMIC
219 || e->n->ntyp == D_STEP)
220 { f = e->n->sl->this->frst;
221 g = e->n->sl->this->last;
223 if (!(g = eval_sub(f))) /* atomic guard */
226 } else if (e->n->ntyp == NON_ATOMIC)
227 { f = e->n->sl->this->frst;
228 g = e->n->sl->this->last;
229 g->nxt = e->nxt; /* close it */
231 } else if (e->n->ntyp == '.')
232 { if (!Rvous) return e->nxt;
233 return eval_sub(e->nxt);
236 if (!(e->status & (D_ATOM))
237 && e->esc && (verbose&32))
239 comment(stdout, e->n, 0);
240 printf("] has escape(s): ");
241 for (x = e->esc; x; x = x->nxt)
244 if (g->n->ntyp == ATOMIC
245 || g->n->ntyp == NON_ATOMIC)
246 g = g->n->sl->this->frst;
247 comment(stdout, g->n, 0);
253 if (!(e->status & D_ATOM)) /* escapes don't reach inside d_steps */
254 /* 4.2.4: only the guard of a d_step can have an escape */
257 if (!s_trail) /* trail determines selections, new 5.2.5 */
261 { if ((g = rev_escape(e->esc)) != ZE)
263 { printf("\tEscape taken (-J) ");
264 if (g->n && g->n->fn)
265 printf("%s:%d", g->n->fn->name, g->n->ln);
272 { for (x = e->esc; x; x = x->nxt)
273 { if ((g = eval_sub(x->this->frst)) != ZE)
275 { printf("\tEscape taken ");
276 if (g->n && g->n->fn)
277 printf("%s:%d", g->n->fn->name, g->n->ln);
285 switch (e->n->ntyp) {
287 if (check_track(e->n) == STRUCT) { break; }
289 case TIMEOUT: case RUN:
290 case PRINT: case PRINTM:
291 case C_CODE: case C_EXPR:
293 case 's': case 'r': case 'c':
294 /* toplevel statements only */
301 return (eval_sync(e))?e->nxt:ZE;
303 return (eval(e->n))?e->nxt:ZE;
306 return ZE; /* not reached */
310 eval_sync(Element *e)
311 { /* allow only synchronous receives
312 and related node types */
313 Lextok *now = (e)?e->n:ZN;
317 || now->val >= 2 /* no rv with a poll */
331 if (TstOnly) return 1;
333 switch (now->rgt->ntyp) {
334 case FULL: case NFULL:
335 case EMPTY: case NEMPTY:
340 t = Sym_typ(now->rgt);
343 typ_ck(Sym_typ(now->lft), t, "assignment");
345 return setval(now->lft, eval(now->rgt));
349 nonprogress(void) /* np_ */
352 for (r = run; r; r = r->nxt)
353 { if (has_lab(r->pc, 4)) /* 4=progress */
367 comment(stdout, now, 0);
371 case CONST: return now->val;
372 case '!': return !eval(now->lft);
373 case UMIN: return -eval(now->lft);
374 case '~': return ~eval(now->lft);
376 case '/': return (eval(now->lft) / eval(now->rgt));
377 case '*': return (eval(now->lft) * eval(now->rgt));
378 case '-': return (eval(now->lft) - eval(now->rgt));
379 case '+': return (eval(now->lft) + eval(now->rgt));
380 case '%': return (eval(now->lft) % eval(now->rgt));
381 case LT: return (eval(now->lft) < eval(now->rgt));
382 case GT: return (eval(now->lft) > eval(now->rgt));
383 case '&': return (eval(now->lft) & eval(now->rgt));
384 case '^': return (eval(now->lft) ^ eval(now->rgt));
385 case '|': return (eval(now->lft) | eval(now->rgt));
386 case LE: return (eval(now->lft) <= eval(now->rgt));
387 case GE: return (eval(now->lft) >= eval(now->rgt));
388 case NE: return (eval(now->lft) != eval(now->rgt));
389 case EQ: return (eval(now->lft) == eval(now->rgt));
390 case OR: return (eval(now->lft) || eval(now->rgt));
391 case AND: return (eval(now->lft) && eval(now->rgt));
392 case LSHIFT: return (eval(now->lft) << eval(now->rgt));
393 case RSHIFT: return (eval(now->lft) >> eval(now->rgt));
394 case '?': return (eval(now->lft) ? eval(now->rgt->lft)
395 : eval(now->rgt->rgt));
397 case 'p': return remotevar(now); /* _p for remote reference */
398 case 'q': return remotelab(now);
399 case 'R': return qrecv(now, 0); /* test only */
400 case LEN: return qlen(now);
401 case FULL: return (qfull(now));
402 case EMPTY: return (qlen(now)==0);
403 case NFULL: return (!qfull(now));
404 case NEMPTY: return (qlen(now)>0);
405 case ENABLED: if (s_trail) return 1;
406 return pc_enabled(now->lft);
408 case GET_P: return get_priority(now->lft);
409 case SET_P: set_priority(now->lft->lft, now->lft->rgt); return 1;
411 case EVAL: return eval(now->lft);
412 case PC_VAL: return pc_value(now->lft);
413 case NONPROGRESS: return nonprogress();
414 case NAME: return getval(now);
416 case TIMEOUT: return Tval;
417 case RUN: return TstOnly?1:enable(now);
419 case 's': return qsend(now); /* send */
420 case 'r': return qrecv(now, 1); /* receive or poll */
421 case 'c': return eval(now->lft); /* condition */
422 case PRINT: return TstOnly?1:interprint(stdout, now);
423 case PRINTM: return TstOnly?1:printm(stdout, now);
425 if (check_track(now) == STRUCT) { return 1; }
428 case C_CODE: if (!analyze)
429 { printf("%s:\t", now->sym->name);
430 plunk_inline(stdout, now->sym->name, 0, 1);
432 return 1; /* uninterpreted */
434 case C_EXPR: if (!analyze)
435 { printf("%s:\t", now->sym->name);
436 plunk_expr(stdout, now->sym->name);
439 return 1; /* uninterpreted */
441 case ASSERT: if (TstOnly || eval(now->lft)) return 1;
442 non_fatal("assertion violated", (char *) 0);
443 printf("spin: text of failed assertion: assert(");
444 comment(stdout, now->lft, 0);
446 if (s_trail && !xspin) return 1;
447 wrapup(1); /* doesn't return */
449 case IF: case DO: case BREAK: case UNLESS: /* compound */
450 case '.': return 1; /* return label for compound */
451 case '@': return 0; /* stop state */
452 case ELSE: return 1; /* only hit here in guided trails */
454 case ',': /* reached through option -A with array initializer */
456 return 0; /* not great, but safe */
458 default : printf("spin: bad node type %d (run)\n", now->ntyp);
459 if (s_trail) printf("spin: trail file doesn't match spec?\n");
460 fatal("aborting", 0);
466 printm(FILE *fd, Lextok *n)
472 if (!s_trail || depth >= jumpsteps) {
484 interprint(FILE *fd, Lextok *n)
485 { Lextok *tmp = n->lft;
486 char c, *s = n->sym->name;
487 int i, j; char lbuf[512]; /* matches value in sr_buf() */
488 extern char Buf[]; /* global, size 4096 */
489 char tBuf[4096]; /* match size of global Buf[] */
493 if (!s_trail || depth >= jumpsteps) {
494 for (i = 0; i < (int) strlen(s); i++)
496 case '\"': break; /* ignore */
499 case 't': strcat(Buf, "\t"); break;
500 case 'n': strcat(Buf, "\n"); break;
501 default: goto onechar;
505 if ((c = s[++i]) == '%')
506 { strcat(Buf, "%"); /* literal */
510 { non_fatal("too few print args %s", s);
516 case 'c': sprintf(lbuf, "%c", j); break;
517 case 'd': sprintf(lbuf, "%d", j); break;
519 case 'e': strcpy(tBuf, Buf); /* event name */
526 case 'o': sprintf(lbuf, "%o", j); break;
527 case 'u': sprintf(lbuf, "%u", (unsigned) j); break;
528 case 'x': sprintf(lbuf, "%x", j); break;
529 default: non_fatal("bad print cmd: '%s'", &s[i-1]);
530 lbuf[0] = '\0'; break;
534 onechar: lbuf[0] = s[i]; lbuf[1] = '\0';
535 append: strcat(Buf, lbuf);
540 if (strlen(Buf) >= 4096) fatal("printf string too long", 0);
546 { int i; int v = verbose;
551 if (has_typ(n->lft, RUN))
552 return 1; /* conservative */
553 /* else fall through */
554 default: /* side-effect free */
563 case C_CODE: case C_EXPR:
564 case PRINT: case PRINTM:
565 case ASGN: case ASSERT:
570 { if (Rvous) return 0;
571 TstOnly = 1; verbose = 0;
575 TstOnly = 0; verbose = v;
581 return 0; /* it's never a user-choice */
582 n->ntyp = 'R'; verbose = 0;
586 n->ntyp = 'r'; verbose = v;
599 switch (e->n->ntyp) {
601 return X->pid == (nproc-nstop-1);
609 return Enabled0(e->sub->this->frst);
613 return Enabled0(e->n->sl->this->frst);
615 if (e->sub) /* true for IF, DO, and UNLESS */
616 { for (z = e->sub; z; z = z->nxt)
617 if (Enabled0(z->this->frst))
621 for (z = e->esc; z; z = z->nxt)
622 { if (Enabled0(z->this->frst))
627 comment(stdout, e->n, 0);
628 printf(" ==> %s\n", Enabled1(e->n)?"yes":"nope");
630 return Enabled1(e->n);
634 pc_enabled(Lextok *n)
635 { int i = nproc - nstop;
641 fatal("used: enabled(pid=thisproc) [%s]", X->n->name);
643 for (Y = run; Y; Y = Y->nxt)
646 result = Enabled0(X->pc);
654 pc_highest(Lextok *n)
655 { int i = nproc - nstop;
657 int target = 0, result = 1;
660 if (X->prov && !eval(X->prov)) return 0; /* can't be highest unless fully enabled */
662 for (Y = run; Y; Y = Y->nxt)
664 { target = Y->priority;
667 if (0) printf("highest for pid %d @ priority = %d\n", pid, target);
671 for (Y = run; Y; Y = Y->nxt)
673 if (0) printf(" pid %d @ priority %d\t", Y->pid, Y->priority);
674 if (Y->priority > target)
676 if (0) printf("enabled: %s\n", Enabled0(X->pc)?"yes":"nope");
677 if (0) printf("provided: %s\n", eval(X->prov)?"yes":"nope");
678 if (Enabled0(X->pc) && (!X->prov || eval(X->prov)))
691 get_priority(Lextok *n)
692 { int i = nproc - nstop;
696 if (old_priority_rules)
700 for (Y = run; Y; Y = Y->nxt)
702 { return Y->priority;
708 set_priority(Lextok *n, Lextok *p)
709 { int i = nproc - nstop - Have_claim;
713 if (old_priority_rules)
716 for (Y = run; Y; Y = Y->nxt)
718 { Priority_Sum -= Y->priority;
719 Y->priority = eval(p);
720 Priority_Sum += Y->priority;
722 { printf("%3d: setting priority of proc %d (%s) to %d\n",
723 depth, pid, Y->n->name, Y->priority);
726 { printf("\tPid\tName\tPriority\n");
727 for (Y = run; Y; Y = Y->nxt)
728 { printf("\t%d\t%s\t%d\n",