123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633 |
- /***** spin: run.c *****/
- /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
- /* All Rights Reserved. This software is for educational purposes only. */
- /* No guarantee whatsoever is expressed or implied by the distribution of */
- /* this code. Permission is given to distribute this code provided that */
- /* this introductory message is not removed and no monies are exchanged. */
- /* Software written by Gerard J. Holzmann. For tool documentation see: */
- /* http://spinroot.com/ */
- /* Send all bug-reports and/or questions to: bugs@spinroot.com */
- #include <stdlib.h>
- #include "spin.h"
- #include "y.tab.h"
- extern RunList *X, *run;
- extern Symbol *Fname;
- extern Element *LastStep;
- extern int Rvous, lineno, Tval, interactive, MadeChoice;
- extern int TstOnly, verbose, s_trail, xspin, jumpsteps, depth;
- extern int analyze, nproc, nstop, no_print, like_java;
- static long Seed = 1;
- static int E_Check = 0, Escape_Check = 0;
- static int eval_sync(Element *);
- static int pc_enabled(Lextok *n);
- extern void sr_buf(int, int);
- void
- Srand(unsigned int s)
- { Seed = s;
- }
- long
- Rand(void)
- { /* CACM 31(10), Oct 1988 */
- Seed = 16807*(Seed%127773) - 2836*(Seed/127773);
- if (Seed <= 0) Seed += 2147483647;
- return Seed;
- }
- Element *
- rev_escape(SeqList *e)
- { Element *r;
- if (!e)
- return (Element *) 0;
- if ((r = rev_escape(e->nxt)) != ZE) /* reversed order */
- return r;
- return eval_sub(e->this->frst);
- }
- Element *
- eval_sub(Element *e)
- { Element *f, *g;
- SeqList *z;
- int i, j, k, only_pos;
- if (!e || !e->n)
- return ZE;
- #ifdef DEBUG
- printf("\n\teval_sub(%d %s: line %d) ",
- e->Seqno, e->esc?"+esc":"", e->n?e->n->ln:0);
- comment(stdout, e->n, 0);
- printf("\n");
- #endif
- if (e->n->ntyp == GOTO)
- { if (Rvous) return ZE;
- LastStep = e;
- f = get_lab(e->n, 1);
- f = huntele(f, e->status, -1); /* 5.2.3: was missing */
- cross_dsteps(e->n, f->n);
- #ifdef DEBUG
- printf("GOTO leads to %d\n", f->seqno);
- #endif
- return f;
- }
- if (e->n->ntyp == UNLESS)
- { /* escapes were distributed into sequence */
- return eval_sub(e->sub->this->frst);
- } else if (e->sub) /* true for IF, DO, and UNLESS */
- { Element *has_else = ZE;
- Element *bas_else = ZE;
- int nr_else = 0, nr_choices = 0;
- only_pos = -1;
- if (interactive
- && !MadeChoice && !E_Check
- && !Escape_Check
- && !(e->status&(D_ATOM))
- && depth >= jumpsteps)
- { printf("Select stmnt (");
- whoruns(0); printf(")\n");
- if (nproc-nstop > 1)
- { printf("\tchoice 0: other process\n");
- nr_choices++;
- only_pos = 0;
- } }
- for (z = e->sub, j=0; z; z = z->nxt)
- { j++;
- if (interactive
- && !MadeChoice && !E_Check
- && !Escape_Check
- && !(e->status&(D_ATOM))
- && depth >= jumpsteps
- && z->this->frst
- && (xspin || (verbose&32) || Enabled0(z->this->frst)))
- { if (z->this->frst->n->ntyp == ELSE)
- { has_else = (Rvous)?ZE:z->this->frst->nxt;
- nr_else = j;
- continue;
- }
- printf("\tchoice %d: ", j);
- #if 0
- if (z->this->frst->n)
- printf("line %d, ", z->this->frst->n->ln);
- #endif
- if (!Enabled0(z->this->frst))
- printf("unexecutable, ");
- else
- { nr_choices++;
- only_pos = j;
- }
- comment(stdout, z->this->frst->n, 0);
- printf("\n");
- } }
- if (nr_choices == 0 && has_else)
- { printf("\tchoice %d: (else)\n", nr_else);
- only_pos = nr_else;
- }
- if (nr_choices <= 1 && only_pos != -1 && !MadeChoice)
- { MadeChoice = only_pos;
- }
- if (interactive && depth >= jumpsteps
- && !Escape_Check
- && !(e->status&(D_ATOM))
- && !E_Check)
- { if (!MadeChoice)
- { char buf[256];
- if (xspin)
- printf("Make Selection %d\n\n", j);
- else
- printf("Select [0-%d]: ", j);
- fflush(stdout);
- if (scanf("%64s", buf) <= 0)
- { printf("no input\n");
- return ZE;
- }
- if (isdigit((int)buf[0]))
- k = atoi(buf);
- else
- { if (buf[0] == 'q')
- alldone(0);
- k = -1;
- }
- } else
- { k = MadeChoice;
- MadeChoice = 0;
- }
- if (k < 1 || k > j)
- { if (k != 0) printf("\tchoice outside range\n");
- return ZE;
- }
- k--;
- } else
- { if (e->n && e->n->indstep >= 0)
- k = 0; /* select 1st executable guard */
- else
- k = Rand()%j; /* nondeterminism */
- }
- has_else = ZE;
- bas_else = ZE;
- for (i = 0, z = e->sub; i < j+k; i++)
- { if (z->this->frst
- && z->this->frst->n->ntyp == ELSE)
- { bas_else = z->this->frst;
- has_else = (Rvous)?ZE:bas_else->nxt;
- if (!interactive || depth < jumpsteps
- || Escape_Check
- || (e->status&(D_ATOM)))
- { z = (z->nxt)?z->nxt:e->sub;
- continue;
- }
- }
- if (z->this->frst
- && ((z->this->frst->n->ntyp == ATOMIC
- || z->this->frst->n->ntyp == D_STEP)
- && z->this->frst->n->sl->this->frst->n->ntyp == ELSE))
- { bas_else = z->this->frst->n->sl->this->frst;
- has_else = (Rvous)?ZE:bas_else->nxt;
- if (!interactive || depth < jumpsteps
- || Escape_Check
- || (e->status&(D_ATOM)))
- { z = (z->nxt)?z->nxt:e->sub;
- continue;
- }
- }
- if (i >= k)
- { if ((f = eval_sub(z->this->frst)) != ZE)
- return f;
- else if (interactive && depth >= jumpsteps
- && !(e->status&(D_ATOM)))
- { if (!E_Check && !Escape_Check)
- printf("\tunexecutable\n");
- return ZE;
- } }
- z = (z->nxt)?z->nxt:e->sub;
- }
- LastStep = bas_else;
- return has_else;
- } else
- { if (e->n->ntyp == ATOMIC
- || e->n->ntyp == D_STEP)
- { f = e->n->sl->this->frst;
- g = e->n->sl->this->last;
- g->nxt = e->nxt;
- if (!(g = eval_sub(f))) /* atomic guard */
- return ZE;
- return g;
- } else if (e->n->ntyp == NON_ATOMIC)
- { f = e->n->sl->this->frst;
- g = e->n->sl->this->last;
- g->nxt = e->nxt; /* close it */
- return eval_sub(f);
- } else if (e->n->ntyp == '.')
- { if (!Rvous) return e->nxt;
- return eval_sub(e->nxt);
- } else
- { SeqList *x;
- if (!(e->status & (D_ATOM))
- && e->esc && verbose&32)
- { printf("Stmnt [");
- comment(stdout, e->n, 0);
- printf("] has escape(s): ");
- for (x = e->esc; x; x = x->nxt)
- { printf("[");
- g = x->this->frst;
- if (g->n->ntyp == ATOMIC
- || g->n->ntyp == NON_ATOMIC)
- g = g->n->sl->this->frst;
- comment(stdout, g->n, 0);
- printf("] ");
- }
- printf("\n");
- }
- #if 0
- if (!(e->status & D_ATOM)) /* escapes don't reach inside d_steps */
- /* 4.2.4: only the guard of a d_step can have an escape */
- #endif
- #if 1
- if (!s_trail) /* trail determines selections, new 5.2.5 */
- #endif
- { Escape_Check++;
- if (like_java)
- { if ((g = rev_escape(e->esc)) != ZE)
- { if (verbose&4)
- printf("\tEscape taken\n");
- Escape_Check--;
- return g;
- }
- } else
- { for (x = e->esc; x; x = x->nxt)
- { if ((g = eval_sub(x->this->frst)) != ZE)
- { if (verbose&4)
- { printf("\tEscape taken ");
- if (g->n && g->n->fn)
- printf("%s:%d", g->n->fn->name, g->n->ln);
- printf("\n");
- }
- Escape_Check--;
- return g;
- } } }
- Escape_Check--;
- }
-
- switch (e->n->ntyp) {
- case TIMEOUT: case RUN:
- case PRINT: case PRINTM:
- case C_CODE: case C_EXPR:
- case ASGN: case ASSERT:
- case 's': case 'r': case 'c':
- /* toplevel statements only */
- LastStep = e;
- default:
- break;
- }
- if (Rvous)
- {
- return (eval_sync(e))?e->nxt:ZE;
- }
- return (eval(e->n))?e->nxt:ZE;
- }
- }
- return ZE; /* not reached */
- }
- static int
- eval_sync(Element *e)
- { /* allow only synchronous receives
- and related node types */
- Lextok *now = (e)?e->n:ZN;
- if (!now
- || now->ntyp != 'r'
- || now->val >= 2 /* no rv with a poll */
- || !q_is_sync(now))
- {
- return 0;
- }
- LastStep = e;
- return eval(now);
- }
- static int
- assign(Lextok *now)
- { int t;
- if (TstOnly) return 1;
- switch (now->rgt->ntyp) {
- case FULL: case NFULL:
- case EMPTY: case NEMPTY:
- case RUN: case LEN:
- t = BYTE;
- break;
- default:
- t = Sym_typ(now->rgt);
- break;
- }
- typ_ck(Sym_typ(now->lft), t, "assignment");
- return setval(now->lft, eval(now->rgt));
- }
- static int
- nonprogress(void) /* np_ */
- { RunList *r;
- for (r = run; r; r = r->nxt)
- { if (has_lab(r->pc, 4)) /* 4=progress */
- return 0;
- }
- return 1;
- }
- int
- eval(Lextok *now)
- {
- if (now) {
- lineno = now->ln;
- Fname = now->fn;
- #ifdef DEBUG
- printf("eval ");
- comment(stdout, now, 0);
- printf("\n");
- #endif
- switch (now->ntyp) {
- case CONST: return now->val;
- case '!': return !eval(now->lft);
- case UMIN: return -eval(now->lft);
- case '~': return ~eval(now->lft);
- case '/': return (eval(now->lft) / eval(now->rgt));
- case '*': return (eval(now->lft) * eval(now->rgt));
- case '-': return (eval(now->lft) - eval(now->rgt));
- case '+': return (eval(now->lft) + eval(now->rgt));
- case '%': return (eval(now->lft) % eval(now->rgt));
- case LT: return (eval(now->lft) < eval(now->rgt));
- case GT: return (eval(now->lft) > eval(now->rgt));
- case '&': return (eval(now->lft) & eval(now->rgt));
- case '^': return (eval(now->lft) ^ eval(now->rgt));
- case '|': return (eval(now->lft) | eval(now->rgt));
- case LE: return (eval(now->lft) <= eval(now->rgt));
- case GE: return (eval(now->lft) >= eval(now->rgt));
- case NE: return (eval(now->lft) != eval(now->rgt));
- case EQ: return (eval(now->lft) == eval(now->rgt));
- case OR: return (eval(now->lft) || eval(now->rgt));
- case AND: return (eval(now->lft) && eval(now->rgt));
- case LSHIFT: return (eval(now->lft) << eval(now->rgt));
- case RSHIFT: return (eval(now->lft) >> eval(now->rgt));
- case '?': return (eval(now->lft) ? eval(now->rgt->lft)
- : eval(now->rgt->rgt));
- case 'p': return remotevar(now); /* _p for remote reference */
- case 'q': return remotelab(now);
- case 'R': return qrecv(now, 0); /* test only */
- case LEN: return qlen(now);
- case FULL: return (qfull(now));
- case EMPTY: return (qlen(now)==0);
- case NFULL: return (!qfull(now));
- case NEMPTY: return (qlen(now)>0);
- case ENABLED: if (s_trail) return 1;
- return pc_enabled(now->lft);
- case EVAL: return eval(now->lft);
- case PC_VAL: return pc_value(now->lft);
- case NONPROGRESS: return nonprogress();
- case NAME: return getval(now);
- case TIMEOUT: return Tval;
- case RUN: return TstOnly?1:enable(now);
- case 's': return qsend(now); /* send */
- case 'r': return qrecv(now, 1); /* receive or poll */
- case 'c': return eval(now->lft); /* condition */
- case PRINT: return TstOnly?1:interprint(stdout, now);
- case PRINTM: return TstOnly?1:printm(stdout, now);
- case ASGN: return assign(now);
- case C_CODE: if (!analyze)
- { printf("%s:\t", now->sym->name);
- plunk_inline(stdout, now->sym->name, 0, 1);
- }
- return 1; /* uninterpreted */
- case C_EXPR: if (!analyze)
- { printf("%s:\t", now->sym->name);
- plunk_expr(stdout, now->sym->name);
- printf("\n");
- }
- return 1; /* uninterpreted */
- case ASSERT: if (TstOnly || eval(now->lft)) return 1;
- non_fatal("assertion violated", (char *) 0);
- printf("spin: text of failed assertion: assert(");
- comment(stdout, now->lft, 0);
- printf(")\n");
- if (s_trail && !xspin) return 1;
- wrapup(1); /* doesn't return */
- case IF: case DO: case BREAK: case UNLESS: /* compound */
- case '.': return 1; /* return label for compound */
- case '@': return 0; /* stop state */
- case ELSE: return 1; /* only hit here in guided trails */
- default : printf("spin: bad node type %d (run)\n", now->ntyp);
- if (s_trail) printf("spin: trail file doesn't match spec?\n");
- fatal("aborting", 0);
- }}
- return 0;
- }
- int
- printm(FILE *fd, Lextok *n)
- { extern char Buf[];
- int j;
- Buf[0] = '\0';
- if (!no_print)
- if (!s_trail || depth >= jumpsteps) {
- if (n->lft->ismtyp)
- j = n->lft->val;
- else
- j = eval(n->lft);
- sr_buf(j, 1);
- dotag(fd, Buf);
- }
- return 1;
- }
- int
- interprint(FILE *fd, Lextok *n)
- { Lextok *tmp = n->lft;
- char c, *s = n->sym->name;
- int i, j; char lbuf[512]; /* matches value in sr_buf() */
- extern char Buf[]; /* global, size 4096 */
- char tBuf[4096]; /* match size of global Buf[] */
- Buf[0] = '\0';
- if (!no_print)
- if (!s_trail || depth >= jumpsteps) {
- for (i = 0; i < (int) strlen(s); i++)
- switch (s[i]) {
- case '\"': break; /* ignore */
- case '\\':
- switch(s[++i]) {
- case 't': strcat(Buf, "\t"); break;
- case 'n': strcat(Buf, "\n"); break;
- default: goto onechar;
- }
- break;
- case '%':
- if ((c = s[++i]) == '%')
- { strcat(Buf, "%"); /* literal */
- break;
- }
- if (!tmp)
- { non_fatal("too few print args %s", s);
- break;
- }
- j = eval(tmp->lft);
- tmp = tmp->rgt;
- switch(c) {
- case 'c': sprintf(lbuf, "%c", j); break;
- case 'd': sprintf(lbuf, "%d", j); break;
- case 'e': strcpy(tBuf, Buf); /* event name */
- Buf[0] = '\0';
- sr_buf(j, 1);
- strcpy(lbuf, Buf);
- strcpy(Buf, tBuf);
- break;
- case 'o': sprintf(lbuf, "%o", j); break;
- case 'u': sprintf(lbuf, "%u", (unsigned) j); break;
- case 'x': sprintf(lbuf, "%x", j); break;
- default: non_fatal("bad print cmd: '%s'", &s[i-1]);
- lbuf[0] = '\0'; break;
- }
- goto append;
- default:
- onechar: lbuf[0] = s[i]; lbuf[1] = '\0';
- append: strcat(Buf, lbuf);
- break;
- }
- dotag(fd, Buf);
- }
- if (strlen(Buf) >= 4096) fatal("printf string too long", 0);
- return 1;
- }
- static int
- Enabled1(Lextok *n)
- { int i; int v = verbose;
- if (n)
- switch (n->ntyp) {
- case 'c':
- if (has_typ(n->lft, RUN))
- return 1; /* conservative */
- /* else fall through */
- default: /* side-effect free */
- verbose = 0;
- E_Check++;
- i = eval(n);
- E_Check--;
- verbose = v;
- return i;
- case C_CODE: case C_EXPR:
- case PRINT: case PRINTM:
- case ASGN: case ASSERT:
- return 1;
- case 's':
- if (q_is_sync(n))
- { if (Rvous) return 0;
- TstOnly = 1; verbose = 0;
- E_Check++;
- i = eval(n);
- E_Check--;
- TstOnly = 0; verbose = v;
- return i;
- }
- return (!qfull(n));
- case 'r':
- if (q_is_sync(n))
- return 0; /* it's never a user-choice */
- n->ntyp = 'R'; verbose = 0;
- E_Check++;
- i = eval(n);
- E_Check--;
- n->ntyp = 'r'; verbose = v;
- return i;
- }
- return 0;
- }
- int
- Enabled0(Element *e)
- { SeqList *z;
- if (!e || !e->n)
- return 0;
- switch (e->n->ntyp) {
- case '@':
- return X->pid == (nproc-nstop-1);
- case '.':
- return 1;
- case GOTO:
- if (Rvous) return 0;
- return 1;
- case UNLESS:
- return Enabled0(e->sub->this->frst);
- case ATOMIC:
- case D_STEP:
- case NON_ATOMIC:
- return Enabled0(e->n->sl->this->frst);
- }
- if (e->sub) /* true for IF, DO, and UNLESS */
- { for (z = e->sub; z; z = z->nxt)
- if (Enabled0(z->this->frst))
- return 1;
- return 0;
- }
- for (z = e->esc; z; z = z->nxt)
- { if (Enabled0(z->this->frst))
- return 1;
- }
- #if 0
- printf("enabled1 ");
- comment(stdout, e->n, 0);
- printf(" ==> %s\n", Enabled1(e->n)?"yes":"nope");
- #endif
- return Enabled1(e->n);
- }
- int
- pc_enabled(Lextok *n)
- { int i = nproc - nstop;
- int pid = eval(n);
- int result = 0;
- RunList *Y, *oX;
- if (pid == X->pid)
- fatal("used: enabled(pid=thisproc) [%s]", X->n->name);
- for (Y = run; Y; Y = Y->nxt)
- if (--i == pid)
- { oX = X; X = Y;
- result = Enabled0(Y->pc);
- X = oX;
- break;
- }
- return result;
- }
|