Rev 2 | Blame | Compare with Previous | Last modification | View Log | RSS feed
/***** 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;
}