--- /dev/null
+/***** 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 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;
+
+ 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);
+ cross_dsteps(e->n, f->n);
+ 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;
+
+ 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");
+ }
+ 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++;
+ comment(stdout, z->this->frst->n, 0);
+ printf("\n");
+ } }
+
+ if (nr_choices == 0 && has_else)
+ printf("\tchoice %d: (else)\n", nr_else);
+
+ 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);
+ scanf("%64s", buf);
+ if (isdigit(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
+ { 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\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: printf("%s:\t", now->sym->name);
+ plunk_inline(stdout, now->sym->name, 0);
+ return 1; /* uninterpreted */
+
+ case C_EXPR: 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;
+}
projects / lttv.git / blobdiff