28e9566dc5
from Ori_B:
There were a small number of changes needed from the tarball
on spinroot.org:
- The mkfile needed to be updated
- Memory.h needed to not be included
- It needed to invoke /bin/cpp instead of gcc -E
- It depended on `yychar`, which our yacc doesn't
provide.
I'm still figuring out how to use spin, but it seems to do
the right thing when testing a few of the examples:
% cd $home/src/Spin/Examples/
% spin -a peterson.pml
% pcc pan.c -D_POSIX_SOURCE
% ./6.out
(Spin Version 6.4.7 -- 19 August 2017)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 32 byte, depth reached 24, errors: 0
40 states, stored
27 states, matched
67 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.002 equivalent memory usage for states (stored*(State-vector + overhead))
0.292 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in proctype user
/tmp/Spin/Examples/peterson.pml:20, state 10, "-end-"
(1 of 10 states)
pan: elapsed time 1.25 seconds
pan: rate 32 states/second
425 lines
9.9 KiB
C
425 lines
9.9 KiB
C
/***** spin: dstep.c *****/
|
|
|
|
/*
|
|
* This file is part of the public release of Spin. It is subject to the
|
|
* terms in the LICENSE file that is included in this source directory.
|
|
* Tool documentation is available at http://spinroot.com
|
|
*/
|
|
|
|
#include <assert.h>
|
|
#include "spin.h"
|
|
#include "y.tab.h"
|
|
|
|
#define MAXDSTEP 2048 /* was 512 */
|
|
|
|
char *NextLab[64]; /* must match value in pangen2.c:41 */
|
|
int Level=0, GenCode=0, IsGuard=0, TestOnly=0;
|
|
|
|
static int Tj=0, Jt=0, LastGoto=0;
|
|
static int Tojump[MAXDSTEP], Jumpto[MAXDSTEP], Special[MAXDSTEP];
|
|
static void putCode(FILE *, Element *, Element *, Element *, int);
|
|
|
|
extern int Pid, separate, OkBreak;
|
|
|
|
static void
|
|
Sourced(int n, int special)
|
|
{ int i;
|
|
for (i = 0; i < Tj; i++)
|
|
if (Tojump[i] == n)
|
|
return;
|
|
if (Tj >= MAXDSTEP)
|
|
fatal("d_step sequence too long", (char *)0);
|
|
Special[Tj] = special;
|
|
Tojump[Tj++] = n;
|
|
}
|
|
|
|
static void
|
|
Dested(int n)
|
|
{ int i;
|
|
for (i = 0; i < Tj; i++)
|
|
if (Tojump[i] == n)
|
|
return;
|
|
for (i = 0; i < Jt; i++)
|
|
if (Jumpto[i] == n)
|
|
return;
|
|
if (Jt >= MAXDSTEP)
|
|
fatal("d_step sequence too long", (char *)0);
|
|
Jumpto[Jt++] = n;
|
|
LastGoto = 1;
|
|
}
|
|
|
|
static void
|
|
Mopup(FILE *fd)
|
|
{ int i, j;
|
|
|
|
for (i = 0; i < Jt; i++)
|
|
{ for (j = 0; j < Tj; j++)
|
|
if (Tojump[j] == Jumpto[i])
|
|
break;
|
|
if (j == Tj)
|
|
{ char buf[16];
|
|
if (Jumpto[i] == OkBreak)
|
|
{ if (!LastGoto)
|
|
fprintf(fd, "S_%.3d_0: /* break-dest */\n",
|
|
OkBreak);
|
|
} else {
|
|
sprintf(buf, "S_%.3d_0", Jumpto[i]);
|
|
non_fatal("goto %s breaks from d_step seq", buf);
|
|
} } }
|
|
for (j = 0; j < Tj; j++)
|
|
{ for (i = 0; i < Jt; i++)
|
|
if (Tojump[j] == Jumpto[i])
|
|
break;
|
|
#ifdef DEBUG
|
|
if (i == Jt && !Special[i])
|
|
fprintf(fd, "\t\t/* no goto's to S_%.3d_0 */\n",
|
|
Tojump[j]);
|
|
#endif
|
|
}
|
|
for (j = i = 0; j < Tj; j++)
|
|
if (Special[j])
|
|
{ if (i >= MAXDSTEP)
|
|
{ fatal("cannot happen (dstep.c)", (char *)0);
|
|
}
|
|
Tojump[i] = Tojump[j];
|
|
Special[i] = 2;
|
|
i++;
|
|
}
|
|
Tj = i; /* keep only the global exit-labels */
|
|
Jt = 0;
|
|
}
|
|
|
|
static int
|
|
FirstTime(int n)
|
|
{ int i;
|
|
for (i = 0; i < Tj; i++)
|
|
if (Tojump[i] == n)
|
|
return (Special[i] <= 1);
|
|
return 1;
|
|
}
|
|
|
|
static void
|
|
illegal(Element *e, char *str)
|
|
{
|
|
printf("illegal operator in 'd_step:' '");
|
|
comment(stdout, e->n, 0);
|
|
printf("'\n");
|
|
fatal("'%s'", str);
|
|
}
|
|
|
|
static void
|
|
filterbad(Element *e)
|
|
{
|
|
switch (e->n->ntyp) {
|
|
case ASSERT:
|
|
case PRINT:
|
|
case 'c':
|
|
/* run cannot be completely undone
|
|
* with sv_save-sv_restor
|
|
*/
|
|
if (any_oper(e->n->lft, RUN))
|
|
illegal(e, "run operator in d_step");
|
|
|
|
/* remote refs inside d_step sequences
|
|
* would be okay, but they cannot always
|
|
* be interpreted by the simulator the
|
|
* same as by the verifier (e.g., for an
|
|
* error trail)
|
|
*/
|
|
if (any_oper(e->n->lft, 'p'))
|
|
illegal(e, "remote reference in d_step");
|
|
break;
|
|
case '@':
|
|
illegal(e, "process termination");
|
|
break;
|
|
case D_STEP:
|
|
illegal(e, "nested d_step sequence");
|
|
break;
|
|
case ATOMIC:
|
|
illegal(e, "nested atomic sequence");
|
|
break;
|
|
default:
|
|
break;
|
|
}
|
|
}
|
|
|
|
static int
|
|
CollectGuards(FILE *fd, Element *e, int inh)
|
|
{ SeqList *h; Element *ee;
|
|
|
|
for (h = e->sub; h; h = h->nxt)
|
|
{ ee = huntstart(h->this->frst);
|
|
filterbad(ee);
|
|
switch (ee->n->ntyp) {
|
|
case NON_ATOMIC:
|
|
inh += CollectGuards(fd, ee->n->sl->this->frst, inh);
|
|
break;
|
|
case IF:
|
|
inh += CollectGuards(fd, ee, inh);
|
|
break;
|
|
case '.':
|
|
if (ee->nxt->n->ntyp == DO)
|
|
inh += CollectGuards(fd, ee->nxt, inh);
|
|
break;
|
|
case ELSE:
|
|
if (inh++ > 0) fprintf(fd, " || ");
|
|
/* 4.2.5 */ if (!pid_is_claim(Pid))
|
|
fprintf(fd, "(boq == -1 /* else */)");
|
|
else
|
|
fprintf(fd, "(1 /* else */)");
|
|
break;
|
|
case 'R':
|
|
if (inh++ > 0) fprintf(fd, " || ");
|
|
fprintf(fd, "("); TestOnly=1;
|
|
putstmnt(fd, ee->n, ee->seqno);
|
|
fprintf(fd, ")"); TestOnly=0;
|
|
break;
|
|
case 'r':
|
|
if (inh++ > 0) fprintf(fd, " || ");
|
|
fprintf(fd, "("); TestOnly=1;
|
|
putstmnt(fd, ee->n, ee->seqno);
|
|
fprintf(fd, ")"); TestOnly=0;
|
|
break;
|
|
case 's':
|
|
if (inh++ > 0) fprintf(fd, " || ");
|
|
fprintf(fd, "("); TestOnly=1;
|
|
/* 4.2.1 */ if (!pid_is_claim(Pid)) fprintf(fd, "(boq == -1) && ");
|
|
putstmnt(fd, ee->n, ee->seqno);
|
|
fprintf(fd, ")"); TestOnly=0;
|
|
break;
|
|
case 'c':
|
|
if (inh++ > 0) fprintf(fd, " || ");
|
|
fprintf(fd, "("); TestOnly=1;
|
|
if (!pid_is_claim(Pid))
|
|
fprintf(fd, "(boq == -1 && ");
|
|
putstmnt(fd, ee->n->lft, e->seqno);
|
|
if (!pid_is_claim(Pid))
|
|
fprintf(fd, ")");
|
|
fprintf(fd, ")"); TestOnly=0;
|
|
break;
|
|
} }
|
|
return inh;
|
|
}
|
|
|
|
int
|
|
putcode(FILE *fd, Sequence *s, Element *nxt, int justguards, int ln, int seqno)
|
|
{ int isg=0;
|
|
static char buf[64];
|
|
|
|
NextLab[0] = "continue";
|
|
filterbad(s->frst);
|
|
|
|
switch (s->frst->n->ntyp) {
|
|
case UNLESS:
|
|
non_fatal("'unless' inside d_step - ignored", (char *) 0);
|
|
return putcode(fd, s->frst->n->sl->this, nxt, 0, ln, seqno);
|
|
case NON_ATOMIC:
|
|
(void) putcode(fd, s->frst->n->sl->this, ZE, 1, ln, seqno);
|
|
if (justguards) return 0; /* 6.2.5 */
|
|
break;
|
|
case IF:
|
|
fprintf(fd, "if (!(");
|
|
if (!CollectGuards(fd, s->frst, 0)) /* what about boq? */
|
|
fprintf(fd, "1");
|
|
fprintf(fd, "))\n\t\t\tcontinue;");
|
|
isg = 1;
|
|
break;
|
|
case '.':
|
|
if (s->frst->nxt->n->ntyp == DO)
|
|
{ fprintf(fd, "if (!(");
|
|
if (!CollectGuards(fd, s->frst->nxt, 0))
|
|
fprintf(fd, "1");
|
|
fprintf(fd, "))\n\t\t\tcontinue;");
|
|
isg = 1;
|
|
}
|
|
break;
|
|
case 'R': /* <- can't really happen (it's part of a 'c') */
|
|
fprintf(fd, "if (!("); TestOnly=1;
|
|
putstmnt(fd, s->frst->n, s->frst->seqno);
|
|
fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
|
|
break;
|
|
case 'r':
|
|
fprintf(fd, "if (!("); TestOnly=1;
|
|
putstmnt(fd, s->frst->n, s->frst->seqno);
|
|
fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
|
|
break;
|
|
case 's':
|
|
fprintf(fd, "if (");
|
|
#if 1
|
|
/* 4.2.1 */ if (!pid_is_claim(Pid)) fprintf(fd, "(boq != -1) || ");
|
|
#endif
|
|
fprintf(fd, "!("); TestOnly=1;
|
|
putstmnt(fd, s->frst->n, s->frst->seqno);
|
|
fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
|
|
break;
|
|
case 'c':
|
|
fprintf(fd, "if (!(");
|
|
if (!pid_is_claim(Pid)) fprintf(fd, "boq == -1 && ");
|
|
TestOnly=1;
|
|
putstmnt(fd, s->frst->n->lft, s->frst->seqno);
|
|
fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
|
|
break;
|
|
case ELSE:
|
|
fprintf(fd, "if (boq != -1 || (");
|
|
if (separate != 2) fprintf(fd, "trpt->");
|
|
fprintf(fd, "o_pm&1))\n\t\t\tcontinue;");
|
|
{ extern FILE *th;
|
|
fprintf(th, "#ifndef ELSE_IN_GUARD\n");
|
|
fprintf(th, " #define ELSE_IN_GUARD\n");
|
|
fprintf(th, "#endif\n");
|
|
}
|
|
break;
|
|
case ASGN: /* new 3.0.8 */
|
|
fprintf(fd, "IfNotBlocked");
|
|
break;
|
|
default:
|
|
fprintf(fd, "/* default %d */\n\t\t", s->frst->n->ntyp);
|
|
}
|
|
|
|
/* 6.2.5 : before TstOnly */
|
|
fprintf(fd, "\n\n\t\treached[%d][%d] = 1;\n\t\t", Pid, seqno);
|
|
fprintf(fd, "reached[%d][t->st] = 1;\n\t\t", Pid); /* next state */
|
|
fprintf(fd, "reached[%d][tt] = 1;\n", Pid); /* current state */
|
|
|
|
/* 6.2.5 : before sv_save() */
|
|
if (s->frst->n->ntyp != NON_ATOMIC)
|
|
fprintf(fd, "\n\t\tif (TstOnly) return 1;\n"); /* if called from enabled() */
|
|
|
|
if (justguards) return 0;
|
|
|
|
fprintf(fd, "\n\t\tsv_save();\n\t\t");
|
|
sprintf(buf, "Uerror(\"block in d_step seq, line %d\")", ln);
|
|
NextLab[0] = buf;
|
|
putCode(fd, s->frst, s->extent, nxt, isg);
|
|
|
|
if (nxt)
|
|
{ extern Symbol *Fname;
|
|
extern int lineno;
|
|
|
|
if (FirstTime(nxt->Seqno)
|
|
&& (!(nxt->status & DONE2) || !(nxt->status & D_ATOM)))
|
|
{ fprintf(fd, "S_%.3d_0: /* 1 */\n", nxt->Seqno);
|
|
nxt->status |= DONE2;
|
|
LastGoto = 0;
|
|
}
|
|
Sourced(nxt->Seqno, 1);
|
|
lineno = ln;
|
|
Fname = nxt->n->fn;
|
|
Mopup(fd);
|
|
}
|
|
unskip(s->frst->seqno);
|
|
return LastGoto;
|
|
}
|
|
|
|
static void
|
|
putCode(FILE *fd, Element *f, Element *last, Element *next, int isguard)
|
|
{ Element *e, *N;
|
|
SeqList *h; int i;
|
|
char NextOpt[64];
|
|
static int bno = 0;
|
|
|
|
for (e = f; e; e = e->nxt)
|
|
{ if (e->status & DONE2)
|
|
continue;
|
|
e->status |= DONE2;
|
|
|
|
if (!(e->status & D_ATOM))
|
|
{ if (!LastGoto)
|
|
{ fprintf(fd, "\t\tgoto S_%.3d_0;\n",
|
|
e->Seqno);
|
|
Dested(e->Seqno);
|
|
}
|
|
break;
|
|
}
|
|
fprintf(fd, "S_%.3d_0: /* 2 */\n", e->Seqno);
|
|
LastGoto = 0;
|
|
Sourced(e->Seqno, 0);
|
|
|
|
if (!e->sub)
|
|
{ filterbad(e);
|
|
switch (e->n->ntyp) {
|
|
case NON_ATOMIC:
|
|
h = e->n->sl;
|
|
putCode(fd, h->this->frst,
|
|
h->this->extent, e->nxt, 0);
|
|
break;
|
|
case BREAK:
|
|
if (LastGoto) break;
|
|
if (e->nxt)
|
|
{ i = target( huntele(e->nxt,
|
|
e->status, -1))->Seqno;
|
|
fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
|
|
fprintf(fd, "/* 'break' */\n");
|
|
Dested(i);
|
|
} else
|
|
{ if (next)
|
|
{ fprintf(fd, "\t\tgoto S_%.3d_0;",
|
|
next->Seqno);
|
|
fprintf(fd, " /* NEXT */\n");
|
|
Dested(next->Seqno);
|
|
} else
|
|
fatal("cannot interpret d_step", 0);
|
|
}
|
|
break;
|
|
case GOTO:
|
|
if (LastGoto) break;
|
|
i = huntele( get_lab(e->n,1),
|
|
e->status, -1)->Seqno;
|
|
fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
|
|
fprintf(fd, "/* 'goto' */\n");
|
|
Dested(i);
|
|
break;
|
|
case '.':
|
|
if (LastGoto) break;
|
|
if (e->nxt && (e->nxt->status & DONE2))
|
|
{ i = e->nxt->Seqno;
|
|
fprintf(fd, "\t\tgoto S_%.3d_0;", i);
|
|
fprintf(fd, " /* '.' */\n");
|
|
Dested(i);
|
|
}
|
|
break;
|
|
default:
|
|
putskip(e->seqno);
|
|
GenCode = 1; IsGuard = isguard;
|
|
fprintf(fd, "\t\t");
|
|
putstmnt(fd, e->n, e->seqno);
|
|
fprintf(fd, ";\n");
|
|
GenCode = IsGuard = isguard = LastGoto = 0;
|
|
break;
|
|
}
|
|
i = e->nxt?e->nxt->Seqno:0;
|
|
if (e->nxt && (e->nxt->status & DONE2) && !LastGoto)
|
|
{ fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
|
|
fprintf(fd, "/* ';' */\n");
|
|
Dested(i);
|
|
break;
|
|
}
|
|
} else
|
|
{ for (h = e->sub, i=1; h; h = h->nxt, i++)
|
|
{ sprintf(NextOpt, "goto S_%.3d_%d",
|
|
e->Seqno, i);
|
|
NextLab[++Level] = NextOpt;
|
|
N = (e->n && e->n->ntyp == DO) ? e : e->nxt;
|
|
putCode(fd, h->this->frst,
|
|
h->this->extent, N, 1);
|
|
Level--;
|
|
fprintf(fd, "%s: /* 3 */\n", &NextOpt[5]);
|
|
LastGoto = 0;
|
|
}
|
|
if (!LastGoto)
|
|
{ fprintf(fd, "\t\tUerror(\"blocking sel ");
|
|
fprintf(fd, "in d_step (nr.%d, near line %d)\");\n",
|
|
bno++, (e->n)?e->n->ln:0);
|
|
LastGoto = 0;
|
|
}
|
|
}
|
|
if (e == last)
|
|
{ if (!LastGoto && next)
|
|
{ fprintf(fd, "\t\tgoto S_%.3d_0;\n",
|
|
next->Seqno);
|
|
Dested(next->Seqno);
|
|
}
|
|
break;
|
|
} }
|
|
}
|