EliasFleckenstein03
/
plan9front
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

spin: Update to most recent version. (thanks Ori_B) 

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
front
cinap_lenrek 2017-11-22 21:09:31 +01:00
parent 077e719dfb
commit 28e9566dc5
40 changed files with 19245 additions and 3936 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

71
sys/src/cmd/spin/dstep.c
View File

@ -1,27 +1,25 @@
/***** spin: dstep.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 */
/*
* 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 1024 /* was 512 */
#define MAXDSTEP 2048 /* was 512 */
char *NextLab[64];
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, claimnr, separate, OkBreak;
extern int Pid, separate, OkBreak;
static void
Sourced(int n, int special)
@ -59,7 +57,7 @@ Mopup(FILE *fd)
if (Tojump[j] == Jumpto[i])
break;
if (j == Tj)
{ char buf[12];
{ char buf[16];
if (Jumpto[i] == OkBreak)
{ if (!LastGoto)
fprintf(fd, "S_%.3d_0: /* break-dest */\n",
@ -80,10 +78,11 @@ Mopup(FILE *fd)
}
for (j = i = 0; j < Tj; j++)
if (Special[j])
{ Tojump[i] = Tojump[j];
{ if (i >= MAXDSTEP)
{ fatal("cannot happen (dstep.c)", (char *)0);
}
Tojump[i] = Tojump[j];
Special[i] = 2;
if (i >= MAXDSTEP)
fatal("cannot happen (dstep.c)", (char *)0);
i++;
}
Tj = i; /* keep only the global exit-labels */
@ -164,7 +163,7 @@ CollectGuards(FILE *fd, Element *e, int inh)
break;
case ELSE:
if (inh++ > 0) fprintf(fd, " || ");
/* 4.2.5 */ if (Pid != claimnr)
/* 4.2.5 */ if (!pid_is_claim(Pid))
fprintf(fd, "(boq == -1 /* else */)");
else
fprintf(fd, "(1 /* else */)");
@ -184,17 +183,17 @@ CollectGuards(FILE *fd, Element *e, int inh)
case 's':
if (inh++ > 0) fprintf(fd, " || ");
fprintf(fd, "("); TestOnly=1;
/* 4.2.1 */ if (Pid != claimnr) fprintf(fd, "(boq == -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 != claimnr)
if (!pid_is_claim(Pid))
fprintf(fd, "(boq == -1 && ");
putstmnt(fd, ee->n->lft, e->seqno);
if (Pid != claimnr)
if (!pid_is_claim(Pid))
fprintf(fd, ")");
fprintf(fd, ")"); TestOnly=0;
break;
@ -204,7 +203,8 @@ CollectGuards(FILE *fd, Element *e, int inh)
int
putcode(FILE *fd, Sequence *s, Element *nxt, int justguards, int ln, int seqno)
{ int isg=0; char buf[64];
{ int isg=0;
static char buf[64];
NextLab[0] = "continue";
filterbad(s->frst);
@ -215,6 +215,7 @@ putcode(FILE *fd, Sequence *s, Element *nxt, int justguards, int ln, int seqno)
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 (!(");
@ -245,7 +246,7 @@ putcode(FILE *fd, Sequence *s, Element *nxt, int justguards, int ln, int seqno)
case 's':
fprintf(fd, "if (");
#if 1
/* 4.2.1 */ if (Pid != claimnr) fprintf(fd, "(boq != -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);
@ -253,7 +254,7 @@ putcode(FILE *fd, Sequence *s, Element *nxt, int justguards, int ln, int seqno)
break;
case 'c':
fprintf(fd, "if (!(");
if (Pid != claimnr) fprintf(fd, "boq == -1 && ");
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;
@ -262,19 +263,31 @@ putcode(FILE *fd, Sequence *s, Element *nxt, int justguards, int ln, int seqno)
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");
#if 1
fprintf(fd, "reached[%d][%d] = 1;\n\t\t", Pid, seqno);
fprintf(fd, "reached[%d][t->st] = 1;\n\t\t", Pid); /* true next state */
fprintf(fd, "reached[%d][tt] = 1;\n", Pid); /* true current state */
#endif
sprintf(buf, "Uerror(\"block in d_step seq, line %d\")", ln);
NextLab[0] = buf;
putCode(fd, s->frst, s->extent, nxt, isg);
@ -359,7 +372,7 @@ putCode(FILE *fd, Element *f, Element *last, Element *next, int isguard)
case '.':
if (LastGoto) break;
if (e->nxt && (e->nxt->status & DONE2))
{ i = e->nxt?e->nxt->Seqno:0;
{ i = e->nxt->Seqno;
fprintf(fd, "\t\tgoto S_%.3d_0;", i);
fprintf(fd, " /* '.' */\n");
Dested(i);
@ -375,7 +388,7 @@ putCode(FILE *fd, Element *f, Element *last, Element *next, int isguard)
break;
}
i = e->nxt?e->nxt->Seqno:0;
if (e->nxt && e->nxt->status & DONE2 && !LastGoto)
if (e->nxt && (e->nxt->status & DONE2) && !LastGoto)
{ fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
fprintf(fd, "/* ';' */\n");
Dested(i);

452
sys/src/cmd/spin/flow.c
View File

@ -1,24 +1,24 @@
/***** spin: flow.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 */
/*
* 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 "spin.h"
#include "y.tab.h"
extern Symbol *Fname;
extern int nr_errs, lineno, verbose;
extern short has_unless, has_badelse;
extern int nr_errs, lineno, verbose, in_for, old_scope_rules, s_trail;
extern short has_unless, has_badelse, has_xu;
extern char CurScope[MAXSCOPESZ];
Element *Al_El = ZE;
Label *labtab = (Label *) 0;
int Unique=0, Elcnt=0, DstepStart = -1;
int Unique = 0, Elcnt = 0, DstepStart = -1;
int initialization_ok = 1;
short has_accept;
static Lbreak *breakstack = (Lbreak *) 0;
static Lextok *innermost;
@ -37,10 +37,16 @@ void
open_seq(int top)
{ SeqList *t;
Sequence *s = (Sequence *) emalloc(sizeof(Sequence));
s->minel = -1;
t = seqlist(s, cur_s);
cur_s = t;
if (top) Elcnt = 1;
if (top)
{ Elcnt = 1;
initialization_ok = 1;
} else
{ initialization_ok = 0;
}
}
void
@ -84,6 +90,7 @@ cross_dsteps(Lextok *a, Lextok *b)
&& a->indstep != b->indstep)
{ lineno = a->ln;
Fname = a->fn;
if (!s_trail)
fatal("jump into d_step sequence", (char *) 0);
}
}
@ -113,8 +120,8 @@ check_sequence(Sequence *s)
&& n->ntyp != PRINT
&& n->ntyp != PRINTM)
{ if (verbose&32)
printf("spin: line %d %s, redundant skip\n",
n->ln, n->fn->name);
printf("spin: %s:%d, redundant skip\n",
n->fn->name, n->ln);
if (e != s->frst
&& e != s->last
&& e != s->extent)
@ -147,7 +154,11 @@ close_seq(int nottop)
{ Sequence *s = cur_s->this;
Symbol *z;
if (nottop > 0 && (z = has_lab(s->frst, 0)))
if (nottop == 0) /* end of proctype body */
{ initialization_ok = 1;
}
if (nottop > 0 && s->frst && (z = has_lab(s->frst, 0)))
{ printf("error: (%s:%d) label %s placed incorrectly\n",
(s->frst->n)?s->frst->n->fn->name:"-",
(s->frst->n)?s->frst->n->ln:0,
@ -183,12 +194,12 @@ close_seq(int nottop)
printf("\"Label: { statement ... }\"\n");
break;
case 6:
printf("=====>instead of\n");
printf("=====> instead of\n");
printf(" do (or if)\n");
printf(" :: ...\n");
printf(" :: Label: statement\n");
printf(" od (of fi)\n");
printf("=====>always use\n");
printf("=====> use\n");
printf("Label: do (or if)\n");
printf(" :: ...\n");
printf(" :: statement\n");
@ -198,8 +209,9 @@ close_seq(int nottop)
printf("cannot happen - labels\n");
break;
}
alldone(1);
}
if (nottop != 6)
{ alldone(1);
} }
if (nottop == 4
&& !Rjumpslocal(s->frst, s->last))
@ -217,13 +229,14 @@ Lextok *
do_unless(Lextok *No, Lextok *Es)
{ SeqList *Sl;
Lextok *Re = nn(ZN, UNLESS, ZN, ZN);
Re->ln = No->ln;
Re->fn = No->fn;
has_unless++;
if (Es->ntyp == NON_ATOMIC)
Sl = Es->sl;
else
{ Sl = Es->sl;
} else
{ open_seq(0); add_seq(Es);
Sl = seqlist(close_seq(1), 0);
}
@ -348,6 +361,31 @@ loose_ends(void) /* properly tie-up ends of sub-sequences */
} }
}
void
popbreak(void)
{
if (!breakstack)
fatal("cannot happen, breakstack", (char *) 0);
breakstack = breakstack->nxt; /* pop stack */
}
static Lbreak *ob = (Lbreak *) 0;
void
safe_break(void)
{
ob = breakstack;
popbreak();
}
void
restore_break(void)
{
breakstack = ob;
ob = (Lbreak *) 0;
}
static Element *
if_seq(Lextok *n)
{ int tok = n->ntyp;
@ -388,21 +426,26 @@ if_seq(Lextok *n)
&& prev_z->this->frst->n->ntyp == ELSE)
{ prev_z->this->frst->n->val = 1;
has_badelse++;
non_fatal("dubious use of 'else' combined with i/o,",
(char *)0);
if (has_xu)
{ fatal("invalid use of 'else' combined with i/o and xr/xs assertions,",
(char *)0);
} else
{ non_fatal("dubious use of 'else' combined with i/o,",
(char *)0);
}
nr_errs--;
}
e->n = nn(n, tok, ZN, ZN);
e->n->sl = s; /* preserve as info only */
e->sub = s;
for (z = s; z; prev_z = z, z = z->nxt)
for (z = s; z; z = z->nxt)
add_el(t, z->this); /* append target */
if (tok == DO)
{ add_el(t, cur_s->this); /* target upfront */
t = new_el(nn(n, BREAK, ZN, ZN)); /* break target */
set_lab(break_dest(), t); /* new exit */
breakstack = breakstack->nxt; /* pop stack */
popbreak();
}
add_el(e, cur_s->this);
add_el(t, cur_s->this);
@ -563,33 +606,86 @@ add_seq(Lextok *n)
void
set_lab(Symbol *s, Element *e)
{ Label *l; extern Symbol *context;
int cur_uiid = is_inline();
if (!s) return;
for (l = labtab; l; l = l->nxt)
if (l->s == s && l->c == context)
{ if (strcmp(l->s->name, s->name) == 0
&& l->c == context
&& (old_scope_rules || strcmp((const char *) s->bscp, (const char *) l->s->bscp) == 0)
&& l->uiid == cur_uiid)
{ non_fatal("label %s redeclared", s->name);
break;
}
} }
if (strncmp(s->name, "accept", 6) == 0
&& strncmp(s->name, "accept_all", 10) != 0)
{ has_accept = 1;
}
l = (Label *) emalloc(sizeof(Label));
l->s = s;
l->c = context;
l->e = e;
l->uiid = cur_uiid;
l->nxt = labtab;
labtab = l;
}
static Label *
get_labspec(Lextok *n)
{ Symbol *s = n->sym;
Label *l, *anymatch = (Label *) 0;
int ln;
/*
* try to find a label with the same inline id (uiid)
* but if it doesn't exist, return any other match
* within the same scope
*/
for (l = labtab; l; l = l->nxt)
{ if (strcmp(l->s->name, s->name) == 0 /* labelname matches */
&& s->context == l->s->context) /* same scope */
{
#if 0
if (anymatch && n->uiid == anymatch->uiid)
{ if (0) non_fatal("label %s re-declared", s->name);
}
if (0)
{ printf("Label %s uiid now::then %d :: %d bcsp %s :: %s\n",
s->name, n->uiid, l->uiid, s->bscp, l->s->bscp);
printf("get_labspec match on %s %s (bscp goto %s - label %s)\n",
s->name, s->context->name, s->bscp, l->s->bscp);
}
#endif
/* same block scope */
if (strcmp((const char *) s->bscp, (const char *) l->s->bscp) == 0)
{ return l; /* definite match */
}
/* higher block scope */
ln = strlen((const char *) l->s->bscp);
if (strncmp((const char *) s->bscp, (const char *) l->s->bscp, ln) == 0)
{ anymatch = l; /* possible match */
} else if (!anymatch)
{ anymatch = l; /* somewhere else in same context */
} } }
return anymatch; /* return best match */
}
Element *
get_lab(Lextok *n, int md)
{ Label *l;
Symbol *s = n->sym;
{ Label *l = get_labspec(n);
for (l = labtab; l; l = l->nxt)
if (s == l->s)
return (l->e);
if (l != (Label *) 0)
{ return (l->e);
}
lineno = n->ln;
Fname = n->fn;
if (md) fatal("undefined label %s", s->name);
if (md)
{ lineno = n->ln;
Fname = n->fn;
fatal("undefined label %s", n->sym->name);
}
return ZE;
}
@ -670,21 +766,46 @@ fix_dest(Symbol *c, Symbol *a) /* c:label name, a:proctype name */
}
l->e->status |= CHECK2; /* treat as if global */
if (l->e->status & (ATOM | L_ATOM | D_ATOM))
{ non_fatal("cannot reference label inside atomic or d_step (%s)",
c->name);
{ printf("spin: %s:%d, warning, reference to label ",
Fname->name, lineno);
printf("from inside atomic or d_step (%s)\n", c->name);
}
}
int
find_lab(Symbol *s, Symbol *c, int markit)
{ Label *l;
{ Label *l, *pm = (Label *) 0, *apm = (Label *) 0;
int ln;
/* generally called for remote references in never claims */
for (l = labtab; l; l = l->nxt)
{ if (strcmp(s->name, l->s->name) == 0
{
if (strcmp(s->name, l->s->name) == 0
&& strcmp(c->name, l->c->name) == 0)
{ l->visible |= markit;
return (l->e->seqno);
} }
{ ln = strlen((const char *) l->s->bscp);
if (0)
{ printf("want '%s' in context '%s', scope ref '%s' - label '%s'\n",
s->name, c->name, s->bscp, l->s->bscp);
}
/* same or higher block scope */
if (strcmp((const char *) s->bscp, (const char *) l->s->bscp) == 0)
{ pm = l; /* definite match */
break;
}
if (strncmp((const char *) s->bscp, (const char *) l->s->bscp, ln) == 0)
{ pm = l; /* possible match */
} else
{ apm = l; /* remote */
} } }
if (pm)
{ pm->visible |= markit;
return pm->e->seqno;
}
if (apm)
{ apm->visible |= markit;
return apm->e->seqno;
} /* else printf("Not Found\n"); */
return 0;
}
@ -735,6 +856,226 @@ make_atomic(Sequence *s, int added)
}
}
#if 0
static int depth = 0;
void dump_sym(Symbol *, char *);
void
dump_lex(Lextok *t, char *s)
{ int i;
depth++;
printf(s);
for (i = 0; i < depth; i++)
printf("\t");
explain(t->ntyp);
if (t->ntyp == NAME) printf(" %s ", t->sym->name);
if (t->ntyp == CONST) printf(" %d ", t->val);
if (t->ntyp == STRUCT)
{ dump_sym(t->sym, "\n:Z:");
}
if (t->lft)
{ dump_lex(t->lft, "\nL");
}
if (t->rgt)
{ dump_lex(t->rgt, "\nR");
}
depth--;
}
void
dump_sym(Symbol *z, char *s)
{ int i;
char txt[64];
depth++;
printf(s);
for (i = 0; i < depth; i++)
printf("\t");
if (z->type == CHAN)
{ if (z->ini && z->ini->rgt && z->ini->rgt->sym)
{ /* dump_sym(z->ini->rgt->sym, "\n:I:"); -- could also be longer list */
if (z->ini->rgt->rgt
|| !z->ini->rgt->sym)
fatal("chan %s in for should have only one field (a typedef)", z->name);
printf(" -- %s %p -- ", z->ini->rgt->sym->name, z->ini->rgt->sym);
}
} else if (z->type == STRUCT)
{ if (z->Snm)
printf(" == %s %p == ", z->Snm->name, z->Snm);
else
{ if (z->Slst)
dump_lex(z->Slst, "\n:X:");
if (z->ini)
dump_lex(z->ini, "\n:I:");
}
}
depth--;
}
#endif
int
match_struct(Symbol *s, Symbol *t)
{
if (!t
|| !t->ini
|| !t->ini->rgt
|| !t->ini->rgt->sym
|| t->ini->rgt->rgt)
{ fatal("chan %s in for should have only one field (a typedef)", t?t->name:"--");
}
/* we already know that s is a STRUCT */
if (0)
{ printf("index type %s %p ==\n", s->Snm->name, s->Snm);
printf("chan type %s %p --\n\n", t->ini->rgt->sym->name, t->ini->rgt->sym);
}
return (s->Snm == t->ini->rgt->sym);
}
void
valid_name(Lextok *a3, Lextok *a5, Lextok *a8, char *tp)
{
if (a3->ntyp != NAME)
{ fatal("%s ( .name : from .. to ) { ... }", tp);
}
if (a3->sym->type == CHAN
|| a3->sym->type == STRUCT
|| a3->sym->isarray != 0)
{ fatal("bad index in for-construct %s", a3->sym->name);
}
if (a5->ntyp == CONST && a8->ntyp == CONST && a5->val > a8->val)
{ non_fatal("start value for %s exceeds end-value", a3->sym->name);
}
}
void
for_setup(Lextok *a3, Lextok *a5, Lextok *a8)
{ /* for ( a3 : a5 .. a8 ) */
valid_name(a3, a5, a8, "for");
/* a5->ntyp = a8->ntyp = CONST; */
add_seq(nn(a3, ASGN, a3, a5)); /* start value */
open_seq(0);
add_seq(nn(ZN, 'c', nn(a3, LE, a3, a8), ZN)); /* condition */
}
Lextok *
for_index(Lextok *a3, Lextok *a5)
{ Lextok *z0, *z1, *z2, *z3;
Symbol *tmp_cnt;
char tmp_nm[MAXSCOPESZ+16];
/* for ( a3 in a5 ) { ... } */
if (a3->ntyp != NAME)
{ fatal("for ( .name in name ) { ... }", (char *) 0);
}
if (a5->ntyp != NAME)
{ fatal("for ( %s in .name ) { ... }", a3->sym->name);
}
if (a3->sym->type == STRUCT)
{ if (a5->sym->type != CHAN)
{ fatal("for ( %s in .channel_name ) { ... }",
a3->sym->name);
}
z0 = a5->sym->ini;
if (!z0
|| z0->val <= 0
|| z0->rgt->ntyp != STRUCT
|| z0->rgt->rgt != NULL)
{ fatal("bad channel type %s in for", a5->sym->name);
}
if (!match_struct(a3->sym, a5->sym))
{ fatal("type of %s does not match chan", a3->sym->name);
}
z1 = nn(ZN, CONST, ZN, ZN); z1->val = 0;
z2 = nn(a5, LEN, a5, ZN);
sprintf(tmp_nm, "_f0r_t3mp%s", CurScope); /* make sure it's unique */
tmp_cnt = lookup(tmp_nm);
if (z0->val > 255) /* check nr of slots, i.e. max length */
{ tmp_cnt->type = SHORT; /* should be rare */
} else
{ tmp_cnt->type = BYTE;
}
z3 = nn(ZN, NAME, ZN, ZN);
z3->sym = tmp_cnt;
add_seq(nn(z3, ASGN, z3, z1)); /* start value 0 */
open_seq(0);
add_seq(nn(ZN, 'c', nn(z3, LT, z3, z2), ZN)); /* condition */
/* retrieve message from the right slot -- for now: rotate contents */
in_for = 0;
add_seq(nn(a5, 'r', a5, expand(a3, 1))); /* receive */
add_seq(nn(a5, 's', a5, expand(a3, 1))); /* put back in to rotate */
in_for = 1;
return z3;
} else
{ if (a5->sym->isarray == 0
|| a5->sym->nel <= 0)
{ fatal("bad arrayname %s", a5->sym->name);
}
z1 = nn(ZN, CONST, ZN, ZN); z1->val = 0;
z2 = nn(ZN, CONST, ZN, ZN); z2->val = a5->sym->nel - 1;
for_setup(a3, z1, z2);
return a3;
}
}
Lextok *
for_body(Lextok *a3, int with_else)
{ Lextok *t1, *t2, *t0, *rv;
rv = nn(ZN, CONST, ZN, ZN); rv->val = 1;
rv = nn(ZN, '+', a3, rv);
rv = nn(a3, ASGN, a3, rv);
add_seq(rv); /* initial increment */
/* completed loop body, main sequence */
t1 = nn(ZN, 0, ZN, ZN);
t1->sq = close_seq(8);
open_seq(0); /* add else -> break sequence */
if (with_else)
{ add_seq(nn(ZN, ELSE, ZN, ZN));
}
t2 = nn(ZN, GOTO, ZN, ZN);
t2->sym = break_dest();
add_seq(t2);
t2 = nn(ZN, 0, ZN, ZN);
t2->sq = close_seq(9);
t0 = nn(ZN, 0, ZN, ZN);
t0->sl = seqlist(t2->sq, seqlist(t1->sq, 0));
rv = nn(ZN, DO, ZN, ZN);
rv->sl = t0->sl;
return rv;
}
Lextok *
sel_index(Lextok *a3, Lextok *a5, Lextok *a7)
{ /* select ( a3 : a5 .. a7 ) */
valid_name(a3, a5, a7, "select");
/* a5->ntyp = a7->ntyp = CONST; */
add_seq(nn(a3, ASGN, a3, a5)); /* start value */
open_seq(0);
add_seq(nn(ZN, 'c', nn(a3, LT, a3, a7), ZN)); /* condition */
pushbreak(); /* new 6.2.1 */
return for_body(a3, 0); /* no else, just a non-deterministic break */
}
static void
walk_atomic(Element *a, Element *b, int added)
{ Element *f; Symbol *ofn; int oln;
@ -747,16 +1088,16 @@ walk_atomic(Element *a, Element *b, int added)
switch (f->n->ntyp) {
case ATOMIC:
if (verbose&32)
printf("spin: warning, line %3d %s, atomic inside %s (ignored)\n",
f->n->ln, f->n->fn->name, (added)?"d_step":"atomic");
printf("spin: %s:%d, warning, atomic inside %s (ignored)\n",
f->n->fn->name, f->n->ln, (added)?"d_step":"atomic");
goto mknonat;
case D_STEP:
if (!(verbose&32))
{ if (added) goto mknonat;
break;
}
printf("spin: warning, line %3d %s, d_step inside ",
f->n->ln, f->n->fn->name);
printf("spin: %s:%d, warning, d_step inside ",
f->n->fn->name, f->n->ln);
if (added)
{ printf("d_step (ignored)\n");
goto mknonat;
@ -770,8 +1111,8 @@ mknonat: f->n->ntyp = NON_ATOMIC; /* can jump here */
break;
case UNLESS:
if (added)
{ printf("spin: error, line %3d %s, unless in d_step (ignored)\n",
f->n->ln, f->n->fn->name);
{ printf("spin: error, %s:%d, unless in d_step (ignored)\n",
f->n->fn->name, f->n->ln);
}
}
for (h = f->sub; h; h = h->nxt)
@ -789,6 +1130,15 @@ dumplabels(void)
for (l = labtab; l; l = l->nxt)
if (l->c != 0 && l->s->name[0] != ':')
printf("label %s %d <%s>\n",
l->s->name, l->e->seqno, l->c->name);
{ printf("label %s %d ",
l->s->name, l->e->seqno);
if (l->uiid == 0)
printf("<%s>", l->c->name);
else
printf("<%s i%d>", l->c->name, l->uiid);
if (!old_scope_rules)
{ printf("\t{scope %s}", l->s->bscp);
}
printf("\n");
}
}

160
sys/src/cmd/spin/guided.c
View File

@ -1,17 +1,15 @@
/***** spin: guided.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 */
/*
* 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 "spin.h"
#include <sys/types.h>
#include <sys/stat.h>
#include <limits.h>
#include "y.tab.h"
extern RunList *run, *X;
@ -19,8 +17,9 @@ extern Element *Al_El;
extern Symbol *Fname, *oFname;
extern int verbose, lineno, xspin, jumpsteps, depth, merger, cutoff;
extern int nproc, nstop, Tval, ntrail, columns;
extern short Have_claim, Skip_claim;
extern short Have_claim, Skip_claim, has_code;
extern void ana_src(int, int);
extern char **trailfilename;
int TstOnly = 0, pno;
@ -73,12 +72,70 @@ not_claim(void)
return (!Have_claim || !X || X->pid != 0);
}
int globmin = INT_MAX;
int globmax = 0;
int
find_min(Sequence *s)
{ SeqList *l;
Element *e;
if (s->minel < 0)
{ s->minel = INT_MAX;
for (e = s->frst; e; e = e->nxt)
{ if (e->status & 512)
{ continue;
}
e->status |= 512;
if (e->n->ntyp == ATOMIC
|| e->n->ntyp == NON_ATOMIC
|| e->n->ntyp == D_STEP)
{ int n = find_min(e->n->sl->this);
if (n < s->minel)
{ s->minel = n;
}
} else if (e->Seqno < s->minel)
{ s->minel = e->Seqno;
}
for (l = e->sub; l; l = l->nxt)
{ int n = find_min(l->this);
if (n < s->minel)
{ s->minel = n;
} } }
}
if (s->minel < globmin)
{ globmin = s->minel;
}
return s->minel;
}
int
find_max(Sequence *s)
{
if (s->last->Seqno > globmax)
{ globmax = s->last->Seqno;
}
return s->last->Seqno;
}
void
match_trail(void)
{ int i, a, nst;
Element *dothis;
char snap[512], *q;
if (has_code)
{ printf("spin: important:\n");
printf(" =======================================warning====\n");
printf(" this model contains embedded c code statements\n");
printf(" these statements will not be executed when the trail\n");
printf(" is replayed in this way -- they are just printed,\n");
printf(" which will likely lead to inaccurate variable values.\n");
printf(" for an accurate replay use: ./pan -r\n");
printf(" =======================================warning====\n\n");
}
/*
* if source model name is leader.pml
* look for the trail file under these names:
@ -88,10 +145,18 @@ match_trail(void)
* leader.tra
*/
if (ntrail)
sprintf(snap, "%s%d.trail", oFname->name, ntrail);
else
sprintf(snap, "%s.trail", oFname->name);
if (trailfilename)
{ if (strlen(*trailfilename) < sizeof(snap))
{ strcpy(snap, (const char *) *trailfilename);
} else
{ fatal("filename %s too long", *trailfilename);
}
} else
{ if (ntrail)
sprintf(snap, "%s%d.trail", oFname->name, ntrail);
else
sprintf(snap, "%s.trail", oFname->name);
}
if ((fd = fopen(snap, "r")) == NULL)
{ snap[strlen(snap)-2] = '\0'; /* .tra */
@ -118,9 +183,9 @@ match_trail(void)
} }
okay:
if (xspin == 0 && newer(oFname->name, snap))
printf("spin: warning, \"%s\" is newer than %s\n",
oFname->name, snap);
{ printf("spin: warning, \"%s\" is newer than %s\n",
oFname->name, snap);
}
Tval = 1;
/*
@ -132,10 +197,23 @@ okay:
hookup();
while (fscanf(fd, "%d:%d:%d\n", &depth, &pno, &nst) == 3)
{ if (depth == -2) { start_claim(pno); continue; }
if (depth == -4) { merger = 1; ana_src(0, 1); continue; }
if (depth == -1)
{ if (depth == -2)
{ if (verbose)
{ printf("starting claim %d\n", pno);
}
start_claim(pno);
continue;
}
if (depth == -4)
{ if (verbose)
{ printf("using statement merging\n");
}
merger = 1;
ana_src(0, 1);
continue;
}
if (depth == -1)
{ if (1 || verbose)
{ if (columns == 2)
dotag(stdout, " CYCLE>\n");
else
@ -188,16 +266,50 @@ okay:
pno - Have_claim, i, nst, dothis->n->ntyp);
lost_trail();
}
if (0 && !xspin && (verbose&32))
{ printf("step %d i=%d pno %d stmnt %d\n", depth, i, pno, nst);
}
for (X = run; X; X = X->nxt)
{ if (--i == pno)
break;
}
if (!X)
{ printf("%3d: no process %d ", depth, pno - Have_claim);
printf("(state %d)\n", nst);
lost_trail();
{ if (verbose&32)
{ printf("%3d: no process %d (stmnt %d)\n", depth, pno - Have_claim, nst);
printf(" max %d (%d - %d + %d) claim %d ",
nproc - nstop + Skip_claim,
nproc, nstop, Skip_claim, Have_claim);
printf("active processes:\n");
for (X = run; X; X = X->nxt)
{ printf("\tpid %d\tproctype %s\n", X->pid, X->n->name);
}
printf("\n");
continue;
} else
{ printf("%3d:\tproc %d (?) ", depth, pno);
lost_trail();
}
} else
{ int min_seq = find_min(X->ps);
int max_seq = find_max(X->ps);
if (nst < min_seq || nst > max_seq)
{ printf("%3d: error: invalid statement", depth);
if (verbose&32)
{ printf(": pid %d:%d (%s:%d:%d) stmnt %d (valid range %d .. %d)",
pno, X->pid, X->n->name, X->tn, X->b, nst, min_seq, max_seq);
}
printf("\n");
continue;
/* lost_trail(); */
}
X->pc = dothis;
}
X->pc = dothis;
lineno = dothis->n->ln;
Fname = dothis->n->fn;
@ -271,7 +383,7 @@ keepgoing: if (dothis->merge_start)
} }
if (Have_claim && X && X->pid == 0
&& dothis && dothis->n
&& dothis->n
&& lastclaim != dothis->n->ln)
{ lastclaim = dothis->n->ln;
if (columns == 2)

1107
sys/src/cmd/spin/main.c
View File

File diff suppressed because it is too large Load Diff

266
sys/src/cmd/spin/mesg.c
View File

@ -1,14 +1,12 @@
/***** spin: mesg.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 */
/*
* 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 <stdlib.h>
#include "spin.h"
#include "y.tab.h"
@ -24,9 +22,10 @@ extern int lineno, depth, xspin, m_loss, jumpsteps;
extern int nproc, nstop;
extern short Have_claim;
QH *qh;
Queue *qtab = (Queue *) 0; /* linked list of queues */
Queue *ltab[MAXQ]; /* linear list of queues */
int nqs = 0, firstrow = 1;
int nqs = 0, firstrow = 1, has_stdin = 0;
char Buf[4096];
static Lextok *n_rem = (Lextok *) 0;
@ -73,7 +72,7 @@ qmake(Symbol *s)
return eval(s->ini);
q = (Queue *) emalloc(sizeof(Queue));
q->qid = ++nqs;
q->qid = (short) ++nqs;
q->nslots = s->ini->val;
q->nflds = cnt_mpars(s->ini->rgt);
q->setat = depth;
@ -130,7 +129,7 @@ qsend(Lextok *n)
if (whichq == -1)
{ printf("Error: sending to an uninitialized chan\n");
whichq = 0;
/* whichq = 0; */
return 0;
}
if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
@ -143,6 +142,37 @@ qsend(Lextok *n)
return 0;
}
#ifndef PC
#include <termios.h>
static struct termios initial_settings, new_settings;
void
peek_ch_init(void)
{
tcgetattr(0,&initial_settings);
new_settings = initial_settings;
new_settings.c_lflag &= ~ICANON;
new_settings.c_lflag &= ~ECHO;
new_settings.c_lflag &= ~ISIG;
new_settings.c_cc[VMIN] = 0;
new_settings.c_cc[VTIME] = 0;
}
int
peek_ch(void)
{ int n;
has_stdin = 1;
tcsetattr(0, TCSANOW, &new_settings);
n = getchar();
tcsetattr(0, TCSANOW, &initial_settings);
return n;
}
#endif
int
qrecv(Lextok *n, int full)
{ int whichq = eval(n->lft)-1;
@ -150,22 +180,37 @@ qrecv(Lextok *n, int full)
if (whichq == -1)
{ if (n->sym && !strcmp(n->sym->name, "STDIN"))
{ Lextok *m;
#ifndef PC
static int did_once = 0;
if (!did_once) /* 6.2.4 */
{ peek_ch_init();
did_once = 1;
}
#endif
if (TstOnly) return 1;
for (m = n->rgt; m; m = m->rgt)
if (m->lft->ntyp != CONST && m->lft->ntyp != EVAL)
{ int c = getchar();
{
#ifdef PC
int c = getchar();
#else
int c = peek_ch(); /* 6.2.4, was getchar(); */
#endif
if (c == 27 || c == 3) /* escape or control-c */
{ printf("quit\n");
exit(0);
} /* else: non-blocking */
if (c == EOF) return 0; /* no char available */
(void) setval(m->lft, c);
} else
fatal("invalid use of STDIN", (char *)0);
whichq = 0;
{ fatal("invalid use of STDIN", (char *)0);
}
return 1;
}
printf("Error: receiving from an uninitialized chan %s\n",
n->sym?n->sym->name:"");
whichq = 0;
/* whichq = 0; */
return 0;
}
if (whichq < MAXQ && whichq >= 0 && ltab[whichq])
@ -185,9 +230,11 @@ sa_snd(Queue *q, Lextok *n) /* sorted asynchronous */
for (j = 0, m = n->rgt; m && j < q->nflds; m = m->rgt, j++)
{ New = cast_val(q->fld_width[j], eval(m->lft), 0);
Old = q->contents[i*q->nflds+j];
if (New == Old) continue;
if (New > Old) break; /* inner loop */
if (New < Old) goto found;
if (New == Old)
continue;
if (New > Old)
break; /* inner loop */
goto found; /* New < Old */
}
found:
for (j = q->qlen-1; j >= i; j--)
@ -204,7 +251,8 @@ void
typ_ck(int ft, int at, char *s)
{
if ((verbose&32) && ft != at
&& (ft == CHAN || at == CHAN))
&& (ft == CHAN || at == CHAN)
&& (at != PREDEF || strcmp(s, "recv") != 0))
{ char buf[128], tag1[64], tag2[64];
(void) sputtype(tag1, ft);
(void) sputtype(tag2, at);
@ -383,7 +431,7 @@ s_snd(Queue *q, Lextok *n)
return 1;
}
void
static void
channm(Lextok *n)
{ char lbuf[512];
@ -394,7 +442,11 @@ channm(Lextok *n)
else if (n->sym->type == STRUCT)
{ Symbol *r = n->sym;
if (r->context)
r = findloc(r);
{ r = findloc(r);
if (!r)
{ strcat(Buf, "*?*");
return;
} }
ini_struct(r);
printf("%s", r->name);
strcpy(lbuf, "");
@ -422,7 +474,11 @@ difcolumns(Lextok *n, char *tr, int v, int j, Queue *q)
sr_buf(v, q->fld_width[j] == MTYPE);
if (j == q->nflds - 1)
{ int cnr;
if (s_trail) cnr = pno; else cnr = X?X->pid - Have_claim:0;
if (s_trail)
{ cnr = pno;
} else
{ cnr = X?X->pid - Have_claim:0;
}
if (tr[0] == '[') strcat(Buf, "]");
pstext(cnr, Buf);
}
@ -458,12 +514,6 @@ docolumns(Lextok *n, char *tr, int v, int j, Queue *q)
}
}
typedef struct QH {
int n;
struct QH *nxt;
} QH;
QH *qh;
void
qhide(int q)
{ QH *p = (QH *) emalloc(sizeof(QH));
@ -483,7 +533,7 @@ qishidden(int q)
static void
sr_talk(Lextok *n, int v, char *tr, char *a, int j, Queue *q)
{ char s[64];
{ char s[128];
if (qishidden(eval(n->lft)))
return;
@ -510,9 +560,20 @@ sr_talk(Lextok *n, int v, char *tr, char *a, int j, Queue *q)
}
if (j == 0)
{ whoruns(1);
printf("line %3d %s %s",
n->ln, n->fn->name, s);
{ char snm[128];
whoruns(1);
{ char *ptr = n->fn->name;
char *qtr = snm;
while (*ptr != '\0')
{ if (*ptr != '\"')
{ *qtr++ = *ptr;
}
ptr++;
}
*qtr = '\0';
printf("%s:%d %s",
snm, n->ln, s);
}
} else
printf(",");
sr_mesg(stdout, v, q->fld_width[j] == MTYPE);
@ -554,7 +615,11 @@ void
sr_mesg(FILE *fd, int v, int j)
{ Buf[0] ='\0';
sr_buf(v, j);
#if 1
fprintf(fd, Buf, (char *) 0); /* prevent compiler warning */
#else
fprintf(fd, Buf);
#endif
}
void
@ -572,10 +637,15 @@ doq(Symbol *s, int n, RunList *r)
continue;
if (q->nslots == 0)
continue; /* rv q always empty */
#if 0
if (q->qlen == 0) /* new 7/10 -- dont show if queue is empty */
{ continue;
}
#endif
printf("\t\tqueue %d (", q->qid);
if (r)
printf("%s(%d):", r->n->name, r->pid - Have_claim);
if (s->nel != 1)
if (s->nel > 1 || s->isarray)
printf("%s[%d]): ", s->name, n);
else
printf("%s): ", s->name);
@ -609,7 +679,11 @@ nochan_manip(Lextok *p, Lextok *n, int d)
}
}
if (!n || n->ntyp == LEN || n->ntyp == RUN)
/* ok on the rhs of an assignment: */
if (!n || n->ntyp == LEN || n->ntyp == RUN
|| n->ntyp == FULL || n->ntyp == NFULL
|| n->ntyp == EMPTY || n->ntyp == NEMPTY
|| n->ntyp == 'R')
return;
if (n->sym && n->sym->type == CHAN)
@ -627,6 +701,121 @@ nochan_manip(Lextok *p, Lextok *n, int d)
nochan_manip(p, n->rgt, 1);
}
typedef struct BaseName {
char *str;
int cnt;
struct BaseName *nxt;
} BaseName;
static BaseName *bsn;
void
newbasename(char *s)
{ BaseName *b;
/* printf("+++++++++%s\n", s); */
for (b = bsn; b; b = b->nxt)
if (strcmp(b->str, s) == 0)
{ b->cnt++;
return;
}
b = (BaseName *) emalloc(sizeof(BaseName));
b->str = emalloc(strlen(s)+1);
b->cnt = 1;
strcpy(b->str, s);
b->nxt = bsn;
bsn = b;
}
void
delbasename(char *s)
{ BaseName *b, *prv = (BaseName *) 0;
for (b = bsn; b; prv = b, b = b->nxt)
{ if (strcmp(b->str, s) == 0)
{ b->cnt--;
if (b->cnt == 0)
{ if (prv)
{ prv->nxt = b->nxt;
} else
{ bsn = b->nxt;
} }
/* printf("---------%s\n", s); */
break;
} }
}
void
checkindex(char *s, char *t)
{ BaseName *b;
/* printf("xxx Check %s (%s)\n", s, t); */
for (b = bsn; b; b = b->nxt)
{
/* printf(" %s\n", b->str); */
if (strcmp(b->str, s) == 0)
{ non_fatal("do not index an array with itself (%s)", t);
break;
} }
}
void
scan_tree(Lextok *t, char *mn, char *mx)
{ char sv[512];
char tmp[32];
int oln = lineno;
if (!t) return;
lineno = t->ln;
if (t->ntyp == NAME)
{ strcat(mn, t->sym->name);
strcat(mx, t->sym->name);
if (t->lft) /* array index */
{ strcat(mn, "[]");
newbasename(mn);
strcpy(sv, mn); /* save */
strcpy(mn, ""); /* clear */
strcat(mx, "[");
scan_tree(t->lft, mn, mx); /* index */
strcat(mx, "]");
checkindex(mn, mx); /* match against basenames */
strcpy(mn, sv); /* restore */
delbasename(mn);
}
if (t->rgt) /* structure element */
{ scan_tree(t->rgt, mn, mx);
}
} else if (t->ntyp == CONST)
{ strcat(mn, "1"); /* really: t->val */
sprintf(tmp, "%d", t->val);
strcat(mx, tmp);
} else if (t->ntyp == '.')
{ strcat(mn, ".");
strcat(mx, ".");
scan_tree(t->lft, mn, mx);
} else
{ strcat(mn, "??");
strcat(mx, "??");
}
lineno = oln;
}
void
no_nested_array_refs(Lextok *n) /* a [ a[1] ] with a[1] = 1, causes trouble in pan.b */
{ char mn[512];
char mx[512];
/* printf("==================================ZAP\n"); */
bsn = (BaseName *) 0; /* start new list */
strcpy(mn, "");
strcpy(mx, "");
scan_tree(n, mn, mx);
/* printf("==> %s\n", mn); */
}
void
no_internals(Lextok *n)
{ char *sp;
@ -638,7 +827,10 @@ no_internals(Lextok *n)
sp = n->sym->name;
if ((strlen(sp) == strlen("_nr_pr") && strcmp(sp, "_nr_pr") == 0)
|| (strlen(sp) == strlen("_pid") && strcmp(sp, "_pid") == 0)
|| (strlen(sp) == strlen("_p") && strcmp(sp, "_p") == 0))
{ fatal("attempt to assign value to system variable %s", sp);
{ fatal("invalid assignment to %s", sp);
}
no_nested_array_refs(n);
}

6
sys/src/cmd/spin/mkfile
View File

@ -8,14 +8,14 @@ SPIN_OS=\
guided.$O\
main.$O\
mesg.$O\
msc_tcl.$O\
pangen1.$O\
pangen2.$O\
pangen3.$O\
pangen4.$O\
pangen5.$O\
pangen6.$O\
pc_zpp.$O\
ps_msc.$O\
pangen7.$O\
reprosrc.$O\
run.$O\
sched.$O\
@ -45,7 +45,7 @@ BIN=/$objtype/bin
</sys/src/cmd/mkone
CC=pcc -c
CFLAGS=-B -D_POSIX_SOURCE
CFLAGS=-B -D_POSIX_SOURCE -D_PLAN9
YFLAGS=-S -d
$SPIN_OS: spin.h

376
sys/src/cmd/spin/msc_tcl.c Normal file
View File

@ -0,0 +1,376 @@
/***** spin: msc_tcl.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 <stdlib.h>
#include "spin.h"
#include "version.h"
#define MW 500 /* page width */
#define RH 100 /* right margin */
#define WW 80 /* distance between process lines */
#define HH 12 /* vertical distance between steps */
#define LW 2 /* line width of message arrows */
#define RVC "darkred" /* rendezvous arrows */
#define MPC "darkblue" /* asynchronous message passing arrow */
#define GRC "lightgrey" /* grid lines */
static int MH = 600; /* anticipated page-length */
static FILE *pfd;
static char **I; /* initial procs */
static int *D,*R; /* maps between depth (stepnr) and ldepth (msc-step) */
static short *M; /* x location of each box at index y */
static short *T; /* y index of match for each box at index y */
static char **L; /* text labels */
static int ProcLine[256]; /* active processes */
static int UsedLine[256]; /* process line has at least one entry */
static int ldepth = 1;
static int maxx, TotSteps = 2*4096; /* max nr of steps for simulation output */
static float Scaler = (float) 1.0;
static int xscale = 2;
static int yscale = 1;
static int no_box;
extern int ntrail, s_trail, pno, depth;
extern Symbol *oFname;
extern void exit(int);
extern void putpostlude(void);
static void putpages(void);
static void
psline(int x0, int y0, int x1, int y1, char *color)
{ char *side = "last";
if (x0 == x1) /* gridline */
{ fprintf(pfd, ".c create line %d %d %d %d -fill %s -tags grid -width 1 \n",
xscale*(x0+1)*WW-20, yscale*y0+20,
xscale*(x1+1)*WW-20, yscale*y1+20, color);
fprintf(pfd, ".c lower grid\n");
} else
{ int xm = xscale*(x0+1)*WW + (xscale*(x1 - x0)*WW)/2 - 20; /* mid x */
if (y1 - y0 <= HH+20)
{ y1 = y0+20; /* close enough to horizontal - looks better */
}
fprintf(pfd, ".c create line %d %d %d %d -fill %s -tags mesg -width %d\n",
xscale*(x0+1)*WW-20, yscale*y0+20+10,
xm, yscale*y0+20+10, color, LW);
if (y1 != y0+20)
{ fprintf(pfd, ".c create line %d %d %d %d -fill %s -tags mesg -width %d\n",
xm, yscale*y0+20+10,
xm, yscale*y1+20-10, color, LW);
}
fprintf(pfd, ".c create line %d %d %d %d -fill %s -width %d ",
xm, yscale*y1+20-10,
xscale*(x1+1)*WW-20, yscale*y1+20-10, color, LW);
if (strcmp(color, RVC) == 0)
{ side = "both";
}
fprintf(pfd, "-arrow %s -arrowshape {5 5 5} -tags mesg\n", side);
fprintf(pfd, ".c raise mesg\n");
}
}
static void
colbox(int ix, int iy, int w, int h_unused, char *color)
{ int x = ix*WW;
int y = iy*HH;
if (ix < 0 || ix > 255)
{ fatal("msc_tcl: unexpected\n", (char *) 0);
}
if (ProcLine[ix] < iy)
{ /* if (ProcLine[ix] > 0) */
{ psline(ix-1, ProcLine[ix]*HH+HH+4,
ix-1, iy*HH-HH, GRC);
}
fprintf(pfd, "# ProcLine[%d] from %d to %d (Used %d nobox %d)\n",
ix, ProcLine[ix], iy, UsedLine[ix], no_box);
ProcLine[ix] = iy;
} else
{ fprintf(pfd, "# ProcLine[%d] stays at %d (Used %d nobox %d)\n",
ix, ProcLine[ix], UsedLine[ix], no_box);
}
if (UsedLine[ix])
{ no_box = 2;
}
if (strcmp(color, "black") == 0)
{ if (no_box == 0) /* shadow */
{ fprintf(pfd, ".c create rectangle %d %d %d %d -fill black\n",
xscale*x-(xscale*4*w/3)-20+4, (yscale*y-10)+20+2,
xscale*x+(xscale*4*w/3)-20, (yscale*y+10)+20+2);
}
} else
{ if (no_box == 0) /* box with outline */
{ fprintf(pfd, ".c create rectangle %d %d %d %d -fill ivory\n",
xscale*x-(xscale*4*w/3)-20, (yscale*y-10)+20,
xscale*x+(xscale*4*w/3)-20, (yscale*y+10)+20);
UsedLine[ix]++;
} else /* no outline */
{ fprintf(pfd, ".c create rectangle %d %d %d %d -fill white -width 0\n",
xscale*x-(xscale*4*w/3)-20, (yscale*y-10)+20,
xscale*x+(xscale*4*w/3)-20, (yscale*y+10)+20);
} }
if (no_box > 0)
{ no_box--;
}
}
static void
stepnumber(int i)
{ int y = (yscale*i*HH) + 20;
fprintf(pfd, ".c create text %d %d -fill #eef -text \"%d\"\n",
-10+(xscale*WW)/2, y, i);
/* horizontal dashed grid line */
fprintf(pfd, ".c create line %d %d %d %d -fill #eef -dash {6 4}\n",
-20+WW*xscale, y, (maxx+1)*WW*xscale-20, y);
}
static void
spitbox(int ix, int y, char *s)
{ float bw; /* box width */
char d[256], *t, *z;
int a, i, x = ix+1;
char *color = "black";
if (y > 0)
{ stepnumber(y);
}
bw = (float)1.8*(float)strlen(s); /* guess at default font width */
colbox(x, y, (int) (bw+1.0), 5, "black");
if (s[0] == '~')
{ switch (s[1]) {
default :
case 'R': color = "red"; break;
case 'B': color = "blue"; break;
case 'G': color = "green"; break;
}
s += 2;
} else if (strchr(s, '!'))
{ color = "ivory";
} else if (strchr(s, '?'))
{ color = "azure";
} else
{ color = "pink";
if (sscanf(s, "%d:%250s", &a, d) == 2
&& a >= 0 && a < TotSteps)
{ if (!I[a] || strlen(I[a]) <= strlen(s))
{ I[a] = (char *) emalloc((int) strlen(s)+1);
}
strcpy(I[a], s);
} }
colbox(x, y, (int) bw, 4, color);
z = t = (char *) emalloc(2*strlen(s)+1);
for (i = 0; i < (int) strlen(s); i++)
{ if (s[i] == '\n')
{ continue;
}
if (s[i] == '[' || s[i] == ']')
{ *t++ = '\\';
}
*t++ = s[i];
}
fprintf(pfd, ".c create text %d %d -text \"%s\"\n",
xscale*x*WW-20, yscale*y*HH+20, z);
}
static void
putpages(void)
{ int i, lasti=0; float nmh;
if (maxx*xscale*WW > MW-RH/2)
{ Scaler = (float) (MW-RH/2) / (float) (maxx*xscale*WW);
nmh = (float) MH; nmh /= Scaler; MH = (int) nmh;
fprintf(pfd, "# Scaler %f, MH %d\n", Scaler, MH);
}
if (ldepth >= TotSteps)
{ ldepth = TotSteps-1;
}
/* W: (maxx+2)*xscale*WW */
/* H: ldepth*HH*yscale+50 */
fprintf(pfd, "wm title . \"scenario\"\n");
fprintf(pfd, "wm geometry . %dx600+650+100\n", (maxx+2)*xscale*WW);
fprintf(pfd, "canvas .c -width 800 -height 800 \\\n");
fprintf(pfd, " -scrollregion {0c -1c 30c 100c} \\\n");
fprintf(pfd, " -xscrollcommand \".hscroll set\" \\\n");
fprintf(pfd, " -yscrollcommand \".vscroll set\" \\\n");
fprintf(pfd, " -bg white -relief raised -bd 2\n");
fprintf(pfd, "scrollbar .vscroll -relief sunken ");
fprintf(pfd, " -command \".c yview\"\n");
fprintf(pfd, "scrollbar .hscroll -relief sunken -orient horiz ");
fprintf(pfd, " -command \".c xview\"\n");
fprintf(pfd, "pack append . \\\n");
fprintf(pfd, " .vscroll {right filly} \\\n");
fprintf(pfd, " .hscroll {bottom fillx} \\\n");
fprintf(pfd, " .c {top expand fill}\n");
fprintf(pfd, ".c yview moveto 0\n");
for (i = TotSteps-1; i >= 0; i--)
{ if (I[i])
{ spitbox(i, -1, I[i]);
} }
for (i = 0; i <= ldepth; i++)
{ if (!M[i] && !L[i])
{ continue; /* no box */
}
if (T[i] > 0) /* arrow */
{ if (T[i] == i) /* rv handshake */
{ psline( M[lasti], lasti*HH,
M[i], i*HH, RVC);
} else
{ psline( M[i], i*HH,
M[T[i]], T[i]*HH, MPC);
} }
if (L[i])
{ spitbox(M[i], i, L[i]);
lasti = i;
} }
}
static void
putbox(int x)
{
if (ldepth >= TotSteps)
{ fprintf(stderr, "max length of %d steps exceeded - ps file truncated\n",
TotSteps);
putpostlude();
}
M[ldepth] = x;
if (x > maxx)
{ maxx = x;
fprintf(pfd, "# maxx %d\n", x);
}
}
/* functions called externally: */
extern int WhatSeed(void);
void
putpostlude(void)
{ char cmd[512];
putpages();
fprintf(pfd, ".c lower grid\n");
fprintf(pfd, ".c raise mesg\n");
fclose(pfd);
fprintf(stderr, "seed used: -n%d\n", WhatSeed());
sprintf(cmd, "wish -f %s.tcl &", oFname?oFname->name:"msc");
fprintf(stderr, "%s\n", cmd);
(void) unlink("pan.pre");
exit (system(cmd));
}
void
putprelude(void)
{ char snap[256]; FILE *fd;
sprintf(snap, "%s.tcl", oFname?oFname->name:"msc");
if (!(pfd = fopen(snap, MFLAGS)))
{ fatal("cannot create file '%s'", snap);
}
if (s_trail)
{ if (ntrail)
sprintf(snap, "%s%d.trail", oFname?oFname->name:"msc", ntrail);
else
sprintf(snap, "%s.trail", oFname?oFname->name:"msc");
if (!(fd = fopen(snap, "r")))
{ snap[strlen(snap)-2] = '\0';
if (!(fd = fopen(snap, "r")))
fatal("cannot open trail file", (char *) 0);
}
TotSteps = 1;
while (fgets(snap, 256, fd)) TotSteps++;
fclose(fd);
}
TotSteps *= 2;
R = (int *) emalloc(TotSteps * sizeof(int));
D = (int *) emalloc(TotSteps * sizeof(int));
M = (short *) emalloc(TotSteps * sizeof(short));
T = (short *) emalloc(TotSteps * sizeof(short));
L = (char **) emalloc(TotSteps * sizeof(char *));
I = (char **) emalloc(TotSteps * sizeof(char *));
}
void
putarrow(int from, int to)
{
/* from rv if from == to */
/* which means that D[from] == D[to] */
/* which means that T[x] == x */
if (from < TotSteps
&& to < TotSteps
&& D[from] < TotSteps)
{ T[D[from]] = D[to];
}
}
void
pstext(int x, char *s)
{ char *tmp = emalloc((int) strlen(s)+1);
strcpy(tmp, s);
if (depth == 0)
{ I[x] = tmp;
} else
{ if (depth >= TotSteps || ldepth >= TotSteps)
{ fprintf(stderr, "spin: error: max nr of %d steps exceeded\n",
TotSteps);
fatal("use -uN to limit steps", (char *) 0);
}
putbox(x);
D[depth] = ldepth;
R[ldepth] = depth;
L[ldepth] = tmp;
ldepth += 2;
}
}
void
dotag(FILE *fd, char *s)
{ extern int columns, notabs; extern RunList *X;
int i = (!strncmp(s, "MSC: ", 5))?5:0;
int pid = s_trail ? pno : (X?X->pid:0);
if (columns == 2)
{ pstext(pid, &s[i]);
} else
{ if (!notabs)
{ printf(" ");
for (i = 0; i <= pid; i++)
{ printf(" ");
} }
fprintf(fd, "%s", s);
fflush(fd);
}
}

655
sys/src/cmd/spin/pangen1.c
View File

File diff suppressed because it is too large Load Diff

6955
sys/src/cmd/spin/pangen1.h
View File

File diff suppressed because it is too large Load Diff

1082
sys/src/cmd/spin/pangen2.c
View File

File diff suppressed because it is too large Load Diff

798
sys/src/cmd/spin/pangen2.h
View File

File diff suppressed because it is too large Load Diff

253
sys/src/cmd/spin/pangen3.c
View File

@ -1,22 +1,20 @@
/***** spin: pangen3.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 */
/*
* 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 "spin.h"
#include "y.tab.h"
#include <assert.h>
extern FILE *th;
extern int claimnr, eventmapnr;
extern FILE *th, *tc;
extern int eventmapnr, old_priority_rules;
typedef struct SRC {
short ln, st; /* linenr, statenr */
int ln, st; /* linenr, statenr */
Symbol *fn; /* filename */
struct SRC *nxt;
} SRC;
@ -28,16 +26,18 @@ static int lastfrom;
static SRC *frst = (SRC *) 0;
static SRC *skip = (SRC *) 0;
extern int ltl_mode;
extern void sr_mesg(FILE *, int, int);
static void
putnr(int n)
{
if (col++ == 8)
{ fprintf(th, "\n\t");
{ fprintf(tc, "\n\t"); /* was th */
col = 1;
}
fprintf(th, "%3d, ", n);
fprintf(tc, "%3d, ", n); /* was th */
}
static void
@ -47,7 +47,7 @@ putfnm(int j, Symbol *s)
return;
if (lastfnm)
fprintf(th, "{ %s, %d, %d },\n\t",
fprintf(tc, "{ \"%s\", %d, %d },\n\t", /* was th */
lastfnm->name,
lastfrom,
j-1);
@ -59,73 +59,118 @@ static void
putfnm_flush(int j)
{
if (lastfnm)
fprintf(th, "{ %s, %d, %d }\n",
fprintf(tc, "{ \"%s\", %d, %d }\n", /* was th */
lastfnm->name,
lastfrom, j);
}
static SRC *
newsrc(int m, SRC *n)
{ SRC *tmp;
tmp = (SRC *) emalloc(sizeof(SRC));
tmp->st = m;
tmp->nxt = n;
return tmp;
}
void
putskip(int m) /* states that need not be reached */
{ SRC *tmp;
for (tmp = skip; tmp; tmp = tmp->nxt)
if (tmp->st == m)
return;
tmp = (SRC *) emalloc(sizeof(SRC));
tmp->st = (short) m;
tmp->nxt = skip;
skip = tmp;
{ SRC *tmp, *lst = (SRC *)0;
/* 6.4.0: now an ordered list */
for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
{ if (tmp->st == m)
{ return;
}
if (tmp->st > m) /* insert before */
{ if (tmp == skip)
{ tmp = newsrc(m, skip);
skip = tmp;
} else
{ assert(lst);
tmp = newsrc(m, lst->nxt);
lst->nxt = tmp;
}
return;
} }
/* insert at the end */
if (lst)
{ lst->nxt = newsrc(m, 0);
} else /* empty list */
{ skip = newsrc(m, 0);
}
}
void
unskip(int m) /* a state that needs to be reached after all */
{ SRC *tmp, *lst=(SRC *)0;
{ SRC *tmp, *lst = (SRC *)0;
for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
if (tmp->st == m)
{ if (tmp->st == m)
{ if (tmp == skip)
skip = skip->nxt;
else
else if (lst) /* always true, but helps coverity */
lst->nxt = tmp->nxt;
break;
}
if (tmp->st > m)
{ break; /* m is not in list */
} }
}
void
putsrc(Element *e) /* match states to source lines */
{ SRC *tmp;
{ SRC *tmp, *lst = (SRC *)0;
int n, m;
if (!e || !e->n) return;
n = e->n->ln;
m = e->seqno;
for (tmp = frst; tmp; tmp = tmp->nxt)
if (tmp->st == m)
/* 6.4.0: now an ordered list */
for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt)
{ if (tmp->st == m)
{ if (tmp->ln != n || tmp->fn != e->n->fn)
printf("putsrc mismatch %d - %d, file %s\n", n,
printf("putsrc mismatch seqno %d, line %d - %d, file %s\n", m, n,
tmp->ln, tmp->fn->name);
return;
}
tmp = (SRC *) emalloc(sizeof(SRC));
tmp->ln = (short) n;
tmp->st = (short) m;
if (tmp->st > m) /* insert before */
{ if (tmp == frst)
{ tmp = newsrc(m, frst);
frst = tmp;
} else
{ assert(lst);
tmp = newsrc(m, lst->nxt);
lst->nxt = tmp;
}
tmp->ln = n;
tmp->fn = e->n->fn;
return;
} }
/* insert at the end */
tmp = newsrc(m, lst?lst->nxt:0);
tmp->ln = n;
tmp->fn = e->n->fn;
tmp->nxt = frst;
frst = tmp;
if (lst)
{ lst->nxt = tmp;
} else
{ frst = tmp;
}
}
static void
dumpskip(int n, int m)
{ SRC *tmp, *lst;
FILE *tz = tc; /* was th */
int j;
fprintf(th, "uchar reached%d [] = {\n\t", m);
fprintf(tz, "uchar reached%d [] = {\n\t", m);
tmp = skip;
lst = (SRC *) 0;
for (j = 0, col = 0; j <= n; j++)
{ lst = (SRC *) 0;
for (tmp = skip; tmp; lst = tmp, tmp = tmp->nxt)
if (tmp->st == j)
{ /* find j in the sorted list */
for ( ; tmp; lst = tmp, tmp = tmp->nxt)
{ if (tmp->st == j)
{ putnr(1);
if (lst)
lst->nxt = tmp->nxt;
@ -133,12 +178,17 @@ dumpskip(int n, int m)
skip = tmp->nxt;
break;
}
if (tmp->st > j)
{ putnr(0);
break; /* j is not in the list */
} }
if (!tmp)
putnr(0);
}
fprintf(th, "};\n");
if (m == claimnr)
fprintf(th, "#define reached_claim reached%d\n", m);
{ putnr(0);
} }
fprintf(tz, "};\n");
fprintf(tz, "uchar *loopstate%d;\n", m);
if (m == eventmapnr)
fprintf(th, "#define reached_event reached%d\n", m);
@ -149,27 +199,34 @@ void
dumpsrc(int n, int m)
{ SRC *tmp, *lst;
int j;
static int did_claim = 0;
FILE *tz = tc; /* was th */
fprintf(th, "short src_ln%d [] = {\n\t", m);
fprintf(tz, "\nshort src_ln%d [] = {\n\t", m);
tmp = frst;
for (j = 0, col = 0; j <= n; j++)
{ lst = (SRC *) 0;
for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt)
if (tmp->st == j)
{ for ( ; tmp; tmp = tmp->nxt)
{ if (tmp->st == j)
{ putnr(tmp->ln);
break;
}
if (tmp->st > j)
{ putnr(0);
break;
} }
if (!tmp)
putnr(0);
}
fprintf(th, "};\n");
{ putnr(0);
} }
fprintf(tz, "};\n");
lastfnm = (Symbol *) 0;
lastdef.name = "\"-\"";
fprintf(th, "S_F_MAP src_file%d [] = {\n\t", m);
lastdef.name = "-";
fprintf(tz, "S_F_MAP src_file%d [] = {\n\t", m);
tmp = frst;
lst = (SRC *) 0;
for (j = 0, col = 0; j <= n; j++)
{ lst = (SRC *) 0;
for (tmp = frst; tmp; lst = tmp, tmp = tmp->nxt)
if (tmp->st == j)
{ for ( ; tmp; lst = tmp, tmp = tmp->nxt)
{ if (tmp->st == j)
{ putfnm(j, tmp->fn);
if (lst)
lst->nxt = tmp->nxt;
@ -177,14 +234,20 @@ dumpsrc(int n, int m)
frst = tmp->nxt;
break;
}
if (tmp->st > j)
{ putfnm(j, &lastdef);
break;
} }
if (!tmp)
putfnm(j, &lastdef);
}
{ putfnm(j, &lastdef);
} }
putfnm_flush(j);
fprintf(th, "};\n");
fprintf(tz, "};\n");
if (m == claimnr)
fprintf(th, "#define src_claim src_ln%d\n", m);
if (pid_is_claim(m) && !did_claim)
{ fprintf(tz, "short *src_claim;\n");
did_claim++;
}
if (m == eventmapnr)
fprintf(th, "#define src_event src_ln%d\n", m);
@ -237,7 +300,27 @@ comwork(FILE *fd, Lextok *now, int m)
case GT: Cat1(">"); break;
case LT: Cat1("<"); break;
case NE: Cat1("!="); break;
case EQ: Cat1("=="); break;
case EQ:
if (ltl_mode
&& now->lft->ntyp == 'p'
&& now->rgt->ntyp == 'q') /* remote ref */
{ Lextok *p = now->lft->lft;
fprintf(fd, "(");
fprintf(fd, "%s", p->sym->name);
if (p->lft)
{ fprintf(fd, "[");
putstmnt(fd, p->lft, 0); /* pid */
fprintf(fd, "]");
}
fprintf(fd, "@");
fprintf(fd, "%s", now->rgt->sym->name);
fprintf(fd, ")");
break;
}
Cat1("==");
break;
case OR: Cat1("||"); break;
case AND: Cat1("&&"); break;
case LSHIFT: Cat1("<<"); break;
@ -298,6 +381,22 @@ comwork(FILE *fd, Lextok *now, int m)
case ENABLED: Cat3("enabled(", now->lft, ")");
break;
case GET_P: if (old_priority_rules)
{ fprintf(fd, "1");
} else
{ Cat3("get_priority(", now->lft, ")");
}
break;
case SET_P: if (!old_priority_rules)
{ fprintf(fd, "set_priority(");
comwork(fd, now->lft->lft, m);
fprintf(fd, ", ");
comwork(fd, now->lft->rgt, m);
fprintf(fd, ")");
}
break;
case EVAL: Cat3("eval(", now->lft, ")");
break;
@ -320,12 +419,14 @@ comwork(FILE *fd, Lextok *now, int m)
}
break;
case ASGN: comwork(fd,now->lft,m);
case ASGN:
if (check_track(now) == STRUCT) { break; }
comwork(fd,now->lft,m);
fprintf(fd," = ");
comwork(fd,now->rgt,m);
break;
case PRINT: { char c, buf[512];
case PRINT: { char c, buf[1024];
strncpy(buf, now->sym->name, 510);
for (i = j = 0; i < 510; i++, j++)
{ c = now->sym->name[i];
@ -349,9 +450,23 @@ comwork(FILE *fd, Lextok *now, int m)
comwork(fd, now->lft, m);
fprintf(fd, ")");
break;
case NAME: putname(fd, "", now, m, "");
case NAME:
putname(fd, "", now, m, "");
break;
case 'p': putremote(fd, now, m);
case 'p':
if (ltl_mode)
{ fprintf(fd, "%s", now->lft->sym->name); /* proctype */
if (now->lft->lft)
{ fprintf(fd, "[");
putstmnt(fd, now->lft->lft, 0); /* pid */
fprintf(fd, "]");
}
fprintf(fd, ":"); /* remote varref */
fprintf(fd, "%s", now->sym->name); /* varname */
break;
}
putremote(fd, now, m);
break;
case 'q': fprintf(fd, "%s", now->sym->name);
break;
@ -366,7 +481,7 @@ comwork(FILE *fd, Lextok *now, int m)
case ELSE: fprintf(fd, "else"); break;
case '@': fprintf(fd, "-end-"); break;
case D_STEP: fprintf(fd, "D_STEP"); break;
case D_STEP: fprintf(fd, "D_STEP%d", now->ln); break;
case ATOMIC: fprintf(fd, "ATOMIC"); break;
case NON_ATOMIC: fprintf(fd, "sub-sequence"); break;
case IF: fprintf(fd, "IF"); break;

1148
sys/src/cmd/spin/pangen3.h
View File

File diff suppressed because it is too large Load Diff

40
sys/src/cmd/spin/pangen4.c
View File

@ -1,13 +1,10 @@
/***** spin: pangen4.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 */
/*
* 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 "spin.h"
#include "y.tab.h"
@ -17,7 +14,7 @@ extern Queue *qtab;
extern Symbol *Fname;
extern int lineno, m_loss, Pid, eventmapnr, multi_oval;
extern short nocast, has_provided, has_sorted;
extern char *R13[], *R14[], *R15[];
extern const char *R13[], *R14[], *R15[];
static void check_proc(Lextok *, int);
@ -44,7 +41,7 @@ undostmnt(Lextok *now, int m)
case FULL: case EMPTY: case 'R':
case NFULL: case NEMPTY: case ENABLED:
case '?': case PC_VAL: case '^':
case C_EXPR:
case C_EXPR: case GET_P:
case NONPROGRESS:
putstmnt(tb, now, m);
break;
@ -153,7 +150,14 @@ undostmnt(Lextok *now, int m)
fprintf(tb, "p_restor(II);\n\t\t");
break;
case SET_P:
fprintf(tb, "((P0 *)pptr((trpt->o_priority >> 8)))");
fprintf(tb, "->_priority = trpt->o_priority & 255");
break;
case ASGN:
if (check_track(now) == STRUCT) { break; }
nocast=1; putstmnt(tb,now->lft,m);
nocast=0; fprintf(tb, " = trpt->bup.oval");
if (multi_oval > 0)
@ -307,6 +311,8 @@ genunio(void)
ntimes(tc, 0, 1, R15);
}
extern void explain(int);
int
proper_enabler(Lextok *n)
{
@ -317,15 +323,19 @@ proper_enabler(Lextok *n)
case LEN: case 'R':
case NAME:
has_provided = 1;
if (strcmp(n->sym->name, "_pid") == 0)
if (strcmp(n->sym->name, "_pid") == 0
|| strcmp(n->sym->name, "_priority") == 0)
return 1;
return (!(n->sym->context));
case CONST: case TIMEOUT:
case C_EXPR:
case CONST:
case TIMEOUT:
has_provided = 1;
return 1;
case ENABLED: case PC_VAL:
case GET_P: /* not SET_P */
return proper_enabler(n->lft);
case '!': case UMIN: case '~':
@ -335,10 +345,14 @@ proper_enabler(Lextok *n)
case '%': case LT: case GT: case '&': case '^':
case '|': case LE: case GE: case NE: case '?':
case EQ: case OR: case AND: case LSHIFT:
case RSHIFT: case 'c':
case RSHIFT: case 'c': /* case ',': */
return proper_enabler(n->lft) && proper_enabler(n->rgt);
default:
break;
}
printf("spin: saw ");
explain(n->ntyp);
printf("\n");
return 0;
}

34
sys/src/cmd/spin/pangen4.h
View File

@ -1,24 +1,21 @@
/***** spin: pangen4.h *****/
/* Copyright (c) 1997-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 */
/*
* 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
*
* The DFA code below was written by Anuj Puri and Gerard J. Holzmann in
* May 1997, and was inspired by earlier work on data compression using
* sharing tree data structures and graph-encoded sets by J-Ch. Gregoire
* (INRS Telecom, Quebec, Canada) and D.Zampunieris (Univ.Namur, Belgium)
* The splay routine code included here is based on the public domain
* version written by D. Sleator <sleator@cs.cmu.edu> in 1992.
*/
/* The DFA code below was written by Anuj Puri and Gerard J. Holzmann in */
/* May 1997, and was inspired by earlier work on data compression using */
/* sharing tree data structures and graph-encoded sets by J-Ch. Gregoire */
/* (INRS Telecom, Quebec, Canada) and D.Zampunieris (Univ.Namur, Belgium) */
/* The splay routine code included here is based on the public domain */
/* version written by D. Sleator <sleator@cs.cmu.edu> in 1992. */
static char *Dfa[] = {
static const char *Dfa[] = {
"#ifdef MA",
#if 0
"/*",
"#include <stdio.h>",
"#define uchar unsigned char",
@ -26,6 +23,7 @@ static char *Dfa[] = {
"#define ulong unsigned long",
"#define ushort unsigned short",
"",
#endif
"#define TWIDTH 256",
"#define HASH(y,n) (n)*(((long)y))",
"#define INRANGE(e,h) ((h>=e->From && h<=e->To)||(e->s==1 && e->S==h))",
@ -466,7 +464,7 @@ static char *Dfa[] = {
" for (j = 0; j < TWIDTH; j++)",
" for (i = 0; i < dfa_depth+1; i++)",
" cnt += tree_stats(layers[i*TWIDTH+j]);",
" printf(\"Minimized Automaton:\t%%6d nodes and %%6g edges\\n\",",
" printf(\"Minimized Automaton:\t%%6lu nodes and %%6g edges\\n\",",
" nr_states, cnt);",
"}",
"",

90
sys/src/cmd/spin/pangen5.c
View File

@ -1,13 +1,10 @@
/***** spin: pangen5.c *****/
/* Copyright (c) 1999-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 */
/*
* 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 "spin.h"
#include "y.tab.h"
@ -140,6 +137,7 @@ eligible(FSM_trans *v)
|| lt->ntyp == C_CODE
|| lt->ntyp == C_EXPR
|| has_lab(el, 0) /* any label at all */
|| lt->ntyp == SET_P /* to prevent multiple set_p merges */
|| lt->ntyp == DO
|| lt->ntyp == UNLESS
@ -211,13 +209,18 @@ popbuild(void)
static int
build_step(FSM_trans *v)
{ FSM_state *f;
Element *el = v->step;
Element *el;
#if 0
Lextok *lt = ZN;
#endif
int st = v->to;
int st;
int r;
if (!v) return -1;
el = v->step;
st = v->to;
if (!el) return -1;
if (v->step->merge)
@ -234,9 +237,7 @@ build_step(FSM_trans *v)
lt = v->step->n;
if (verbose&32)
{ if (++howdeep == 1)
printf("spin: %s, line %3d, merge:\n",
lt->fn->name,
lt->ln);
printf("spin: %s:%d, merge:\n", lt->fn->name, lt->ln);
printf("\t[%d] <seqno %d>\t", howdeep, el->seqno);
comment(stdout, lt, 0);
printf(";\n");
@ -257,7 +258,7 @@ build_step(FSM_trans *v)
}
static void
FSM_MERGER(char *pname_unused) /* find candidates for safely merging steps */
FSM_MERGER(/* char *pname */ void) /* find candidates for safely merging steps */
{ FSM_state *f, *g;
FSM_trans *t;
Lextok *lt;
@ -281,14 +282,14 @@ FSM_MERGER(char *pname_unused) /* find candidates for safely merging steps */
continue;
g = fsm_tbl[t->to];
if (!eligible(g->t))
if (!g || !eligible(g->t))
{
#define SINGLES
#ifdef SINGLES
t->step->merge_single = t->to;
#if 0
if ((verbose&32))
{ printf("spin: %s, line %3d, merge_single:\n\t<seqno %d>\t",
{ printf("spin: %s:%d, merge_single:\n\t<seqno %d>\t",
t->step->n->fn->name,
t->step->n->ln,
t->step->seqno);
@ -321,14 +322,17 @@ FSM_MERGER(char *pname_unused) /* find candidates for safely merging steps */
lt = t->step->n;
#if 0
4.1.3:
an rv send operation inside an atomic, *loses* atomicity
when executed
and should therefore never be merged with a subsequent
an rv send operation ('s') inside an atomic, *loses* atomicity
when executed, and should therefore never be merged with a subsequent
statement within the atomic sequence
the same is not true for non-rv send operations
the same is not true for non-rv send operations;
6.2.2:
RUN statements can start a new process at a higher priority level
which interferes with statement merging, so it too is not a suitable
merge target
#endif
if (lt->ntyp == 'c' /* potentially blocking stmnts */
if ((lt->ntyp == 'c' && !any_oper(lt->lft, RUN)) /* 2nd clause 6.2.2 */
|| lt->ntyp == 'r'
|| (lt->ntyp == 's' && u_sync == 0)) /* added !u_sync in 4.1.3 */
{ if (!canfill_in(t)) /* atomic, non-global, etc. */
@ -346,9 +350,8 @@ FSM_MERGER(char *pname_unused) /* find candidates for safely merging steps */
#if 0
if ((verbose&32)
&& t->step->merge_start)
{ printf("spin: %s, line %3d, merge_START:\n\t<seqno %d>\t",
lt->fn->name,
lt->ln,
{ printf("spin: %s:%d, merge_START:\n\t<seqno %d>\t",
lt->fn->name, lt->ln,
t->step->seqno);
comment(stdout, lt, 0);
printf(";\n");
@ -532,6 +535,7 @@ ana_var(FSM_trans *t, Lextok *now, int usage)
if (now->sym->name[0] == '_'
&& (strcmp(now->sym->name, "_") == 0
|| strcmp(now->sym->name, "_pid") == 0
|| strcmp(now->sym->name, "_priority") == 0
|| strcmp(now->sym->name, "_last") == 0))
return;
@ -588,10 +592,17 @@ ana_stmnt(FSM_trans *t, Lextok *now, int usage)
case C_EXPR:
break;
case ',': /* reached with SET_P and array initializers */
if (now->lft && now->lft->rgt)
{ ana_stmnt(t, now->lft->rgt, RVAL);
}
break;
case '!':
case UMIN:
case '~':
case ENABLED:
case GET_P:
case PC_VAL:
case LEN:
case FULL:
@ -603,6 +614,11 @@ ana_stmnt(FSM_trans *t, Lextok *now, int usage)
ana_stmnt(t, now->lft, RVAL);
break;
case SET_P:
ana_stmnt(t, now->lft, RVAL); /* ',' */
ana_stmnt(t, now->lft->rgt, RVAL);
break;
case '/':
case '*':
case '-':
@ -626,8 +642,11 @@ ana_stmnt(FSM_trans *t, Lextok *now, int usage)
break;
case ASGN:
if (check_track(now) == STRUCT) { break; }
ana_stmnt(t, now->lft, LVAL);
ana_stmnt(t, now->rgt, RVAL);
if (now->rgt->ntyp)
ana_stmnt(t, now->rgt, RVAL);
break;
case PRINT:
@ -679,7 +698,8 @@ ana_stmnt(FSM_trans *t, Lextok *now, int usage)
break;
default:
printf("spin: bad node type %d line %d (ana_stmnt)\n", now->ntyp, now->ln);
printf("spin: %s:%d, bad node type %d (ana_stmnt)\n",
now->fn->name, now->ln, now->ntyp);
fatal("aborting", (char *) 0);
}
}
@ -692,10 +712,7 @@ ana_src(int dataflow, int merger) /* called from main.c and guided.c */
int counter = 1;
#endif
for (p = rdy; p; p = p->nxt)
{ if (p->tn == eventmapnr
|| p->tn == claimnr)
continue;
{
ana_seq(p->s);
fsm_table();
@ -711,7 +728,7 @@ ana_src(int dataflow, int merger) /* called from main.c and guided.c */
{ FSM_ANA();
}
if (merger)
{ FSM_MERGER(p->n->name);
{ FSM_MERGER(/* p->n->name */);
huntele(e, e->status, -1)->merge_in = 1; /* start-state */
#if 0
printf("\n");
@ -726,8 +743,7 @@ ana_src(int dataflow, int merger) /* called from main.c and guided.c */
{
if (!(e->status&DONE) && (verbose&32))
{ printf("unreachable code: ");
printf("%s, line %3d: ",
e->n->fn->name, e->n->ln);
printf("%s:%3d ", e->n->fn->name, e->n->ln);
comment(stdout, e->n, 0);
printf("\n");
}
@ -735,7 +751,7 @@ ana_src(int dataflow, int merger) /* called from main.c and guided.c */
}
if (export_ast)
{ AST_slice();
exit(0);
alldone(0); /* changed in 5.3.0: was exit(0) */
}
}
@ -831,9 +847,15 @@ ana_seq(Sequence *s)
{ if (e->n->ntyp == GOTO)
{ g = get_lab(e->n, 1);
g = huntele(g, e->status, -1);
if (!g)
{ fatal("unexpected error 2", (char *) 0);
}
To = g->seqno;
} else if (e->nxt)
{ g = huntele(e->nxt, e->status, -1);
if (!g)
{ fatal("unexpected error 3", (char *) 0);
}
To = g->seqno;
} else
To = 0;

23
sys/src/cmd/spin/pangen5.h
View File

@ -1,15 +1,12 @@
/***** spin: pangen5.h *****/
/* Copyright (c) 1997-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 */
/*
* 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
*/
static char *Xpt[] = {
static const char *Xpt[] = {
"#if defined(MA) && (defined(W_XPT) || defined(R_XPT))",
"static Vertex **temptree;",
"static char wbuf[4096];",
@ -80,7 +77,7 @@ static char *Xpt[] = {
" int i, j; uchar c;",
" static uchar xwarned = 0;",
"",
" sprintf(nm, \"%%s.xpt\", Source);",
" sprintf(nm, \"%%s.xpt\", PanSource);",
" if ((fd = creat(nm, 0666)) <= 0)",
" if (!xwarned)",
" { xwarned = 1;",
@ -136,7 +133,7 @@ static char *Xpt[] = {
" stacker[dfa_depth-1] = 0; r = dfa_store(stacker);",
" stacker[dfa_depth-1] = 4; j = dfa_member(dfa_depth-1);",
" if (r != 1 || j != 0)",
" { printf(\"%%d: \", stackcnt);",
" { printf(\"%%lu: \", stackcnt);",
" for (i = 0; i < dfa_depth; i++)",
" printf(\"%%d,\", stacker[i]);",
" printf(\" -- not a stackstate <o:%%d,4:%%d>\\n\", r, j);",
@ -372,7 +369,7 @@ static char *Xpt[] = {
" int i, j;",
"",
" wcnt = 0;",
" sprintf(nm, \"%%s.xpt\", Source);",
" sprintf(nm, \"%%s.xpt\", PanSource);",
" if ((fd = open(nm, 0)) < 0) /* O_RDONLY */",
" Uerror(\"cannot open checkpoint file\");",
"",
@ -416,7 +413,7 @@ static char *Xpt[] = {
" x_cleanup(d);",
" close(fd);",
"",
" printf(\"pan: removed %%d stackstates\\n\", stackcnt);",
" printf(\"pan: removed %%lu stackstates\\n\", stackcnt);",
" nstates -= (double) stackcnt;",
"}",
"#endif",

157
sys/src/cmd/spin/pangen6.c
View File

@ -1,20 +1,10 @@
/***** spin: pangen6.c *****/
/* Copyright (c) 2000-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 */
/* Abstract syntax tree analysis / slicing (spin option -A) */
/* AST_store stores the fsms's for each proctype */
/* AST_track keeps track of variables used in properties */
/* AST_slice starts the slicing algorithm */
/* it first collects more info and then calls */
/* AST_criteria to process the slice criteria */
/*
* 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 "spin.h"
#include "y.tab.h"
@ -90,7 +80,6 @@ static Slicer *slicer;
static Slicer *rel_vars; /* all relevant variables */
static int AST_Changes;
static int AST_Round;
static FSM_state no_state;
static RPN *rpn;
static int in_recv = 0;
@ -145,7 +134,7 @@ name_def_indices(Lextok *n, int code)
{
if (!n || !n->sym) return;
if (n->sym->nel != 1)
if (n->sym->nel > 1 || n->sym->isarray)
def_use(n->lft, code); /* process the index */
if (n->sym->type == STRUCT /* and possible deeper ones */
@ -202,6 +191,8 @@ def_use(Lextok *now, int code)
case '~':
case 'c':
case ENABLED:
case SET_P:
case GET_P:
case ASSERT:
case EVAL:
def_use(now->lft, USE|code);
@ -503,7 +494,7 @@ AST_mutual(Lextok *a, Lextok *b, int toplevel)
if (strcmp(as->name, bs->name) != 0)
return 0;
if (as->type == STRUCT && a->rgt && b->rgt)
if (as->type == STRUCT && a->rgt && b->rgt) /* we know that a and b are not null */
return AST_mutual(a->rgt->lft, b->rgt->lft, 0);
return 1;
@ -545,14 +536,14 @@ AST_other(AST *a) /* check chan params in asgns and recvs */
case 'r':
/* guess sends where name may originate */
for (cl = chanlist; cl; cl = cl->nxt) /* all sends */
{ int a = AST_nrpar(cl->s);
int b = AST_nrpar(t->step->n);
if (a != b) /* matching nrs of params */
{ int aa = AST_nrpar(cl->s);
int bb = AST_nrpar(t->step->n);
if (aa != bb) /* matching nrs of params */
continue;
a = AST_ord(cl->s, cl->n);
b = AST_ord(t->step->n, u->n);
if (a != b) /* same position in parlist */
aa = AST_ord(cl->s, cl->n);
bb = AST_ord(t->step->n, u->n);
if (aa != bb) /* same position in parlist */
continue;
AST_add_alias(cl->n, 4); /* RCV assume possible match */
@ -692,9 +683,7 @@ AST_relevant(Lextok *n)
}
for (a = ast; a; a = a->nxt) /* all other stmnts */
{ if (strcmp(a->p->n->name, ":never:") != 0
&& strcmp(a->p->n->name, ":trace:") != 0
&& strcmp(a->p->n->name, ":notrace:") != 0)
{ if (a->p->b != N_CLAIM && a->p->b != E_TRACE && a->p->b != N_TRACE)
for (f = a->fsm; f; f = f->nxt)
for (t = f->t; t; t = t->nxt)
{ if (!(t->relevant&1))
@ -786,10 +775,8 @@ AST_tagruns(void)
*/
for (a = ast; a; a = a->nxt)
{ if (strcmp(a->p->n->name, ":never:") == 0
|| strcmp(a->p->n->name, ":trace:") == 0
|| strcmp(a->p->n->name, ":notrace:") == 0
|| strcmp(a->p->n->name, ":init:") == 0)
{ if (a->p->b == N_CLAIM || a->p->b == I_PROC
|| a->p->b == E_TRACE || a->p->b == N_TRACE)
{ a->relevant |= 1; /* the proctype is relevant */
continue;
}
@ -823,9 +810,9 @@ AST_report(AST *a, Element *e) /* ALSO deduce irrelevant vars */
printf("spin: redundant in proctype %s (for given property):\n",
a->p->n->name);
}
printf(" line %3d %s (state %d)",
e->n?e->n->ln:-1,
printf(" %s:%d (state %d)",
e->n?e->n->fn->name:"-",
e->n?e->n->ln:-1,
e->seqno);
printf(" [");
comment(stdout, e->n, 0);
@ -1016,7 +1003,8 @@ name_AST_track(Lextok *n, int code)
printf(" -- %d\n", code);
#endif
if (in_recv && (code&DEF) && (code&USE))
{ printf("spin: error: DEF and USE of same var in rcv stmnt: ");
{ printf("spin: %s:%d, error: DEF and USE of same var in rcv stmnt: ",
n->fn->name, n->ln);
AST_var(n, n->sym, 1);
printf(" -- %d\n", code);
nr_errs++;
@ -1065,6 +1053,8 @@ AST_track(Lextok *now, int code) /* called from main.c */
case '~':
case 'c':
case ENABLED:
case SET_P:
case GET_P:
case ASSERT:
AST_track(now->lft, USE|code);
break;
@ -1075,8 +1065,8 @@ AST_track(Lextok *now, int code) /* called from main.c */
case NAME:
name_AST_track(now, code);
if (now->sym->nel != 1)
AST_track(now->lft, USE|code); /* index */
if (now->sym->nel > 1 || now->sym->isarray)
AST_track(now->lft, USE); /* index, was USE|code */
break;
case 'R':
@ -1569,7 +1559,8 @@ AST_ctrl(AST *a)
{ t->relevant &= ~2; /* clear mark */
if (verbose&32)
{ printf("\t\tnomark ");
comment(stdout, t->step->n, 0);
if (t->step && t->step->n)
comment(stdout, t->step->n, 0);
printf("\n");
} } }
@ -1601,7 +1592,8 @@ AST_ctrl(AST *a)
t->relevant |= 2; /* lift */
if (verbose&32)
{ printf("\t\t\tliftmark ");
comment(stdout, t->step->n, 0);
if (t->step && t->step->n)
comment(stdout, t->step->n, 0);
printf("\n");
}
AST_spread(a, t->to); /* and spread to all guards */
@ -1621,10 +1613,9 @@ AST_control_dep(void)
{ AST *a;
for (a = ast; a; a = a->nxt)
if (strcmp(a->p->n->name, ":never:") != 0
&& strcmp(a->p->n->name, ":trace:") != 0
&& strcmp(a->p->n->name, ":notrace:") != 0)
AST_ctrl(a);
{ if (a->p->b != N_CLAIM && a->p->b != E_TRACE && a->p->b != N_TRACE)
{ AST_ctrl(a);
} }
}
static void
@ -1634,9 +1625,7 @@ AST_prelabel(void)
FSM_trans *t;
for (a = ast; a; a = a->nxt)
{ if (strcmp(a->p->n->name, ":never:") != 0
&& strcmp(a->p->n->name, ":trace:") != 0
&& strcmp(a->p->n->name, ":notrace:") != 0)
{ if (a->p->b != N_CLAIM && a->p->b != E_TRACE && a->p->b != N_TRACE)
for (f = a->fsm; f; f = f->nxt)
for (t = f->t; t; t = t->nxt)
{ if (t->step
@ -1692,8 +1681,7 @@ AST_slice(void)
int spurious = 0;
if (!slicer)
{ non_fatal("no slice criteria (or no claim) specified",
(char *) 0);
{ printf("spin: warning: no slice criteria found (no assertions and no claim)\n");
spurious = 1;
}
AST_dorelevant(); /* mark procs refered to in remote refs */
@ -1730,9 +1718,7 @@ void
AST_store(ProcList *p, int start_state)
{ AST *n_ast;
if (strcmp(p->n->name, ":never:") != 0
&& strcmp(p->n->name, ":trace:") != 0
&& strcmp(p->n->name, ":notrace:") != 0)
if (p->b != N_CLAIM && p->b != E_TRACE && p->b != N_TRACE)
{ n_ast = (AST *) emalloc(sizeof(AST));
n_ast->p = p;
n_ast->i_st = start_state;
@ -1809,12 +1795,10 @@ AST_par_init(void) /* parameter passing -- hidden assignments */
int cnt;
for (a = ast; a; a = a->nxt)
{ if (strcmp(a->p->n->name, ":never:") == 0
|| strcmp(a->p->n->name, ":trace:") == 0
|| strcmp(a->p->n->name, ":notrace:") == 0
|| strcmp(a->p->n->name, ":init:") == 0)
continue; /* have no params */
{ if (a->p->b == N_CLAIM || a->p->b == I_PROC
|| a->p->b == E_TRACE || a->p->b == N_TRACE)
{ continue; /* has no params */
}
cnt = 0;
for (f = a->p->p; f; f = f->rgt) /* types */
for (t = f->lft; t; t = t->rgt) /* formals */
@ -1845,9 +1829,8 @@ AST_var_init(void) /* initialized vars (not chans) - hidden assignments */
} }
for (a = ast; a; a = a->nxt)
{ if (strcmp(a->p->n->name, ":never:") != 0
&& strcmp(a->p->n->name, ":trace:") != 0
&& strcmp(a->p->n->name, ":notrace:") != 0) /* claim has no locals */
{ if (a->p->b != N_CLAIM
&& a->p->b != E_TRACE && a->p->b != N_TRACE) /* has no locals */
for (walk = all_names; walk; walk = walk->next)
{ sp = walk->entry;
if (sp
@ -1995,7 +1978,7 @@ subgraph(AST *a, FSM_state *f, int out)
h = fsm_tbl[out];
i = f->from / BPW;
j = f->from % BPW;
j = f->from % BPW; /* assert(j <= 32); else lshift undefined? */
g = h->mod;
if (verbose&32)
@ -2023,28 +2006,30 @@ act_dom(AST *a)
d. the dominator is reachable, and not equal to this node
#endif
for (t = f->p, i = 0; t; t = t->nxt)
i += fsm_tbl[t->to]->seen;
if (i <= 1) continue; /* a. */
{ i += fsm_tbl[t->to]->seen;
}
if (i <= 1)
{ continue; /* a. */
}
for (cnt = 1; cnt < a->nstates; cnt++) /* 0 is endstate */
{ if (cnt == f->from
|| !fsm_tbl[cnt]->seen)
continue; /* c. */
{ continue; /* c. */
}
i = cnt / BPW;
j = cnt % BPW;
j = cnt % BPW; /* assert(j <= 32); */
if (!(f->dom[i]&(1<<j)))
continue;
{ continue;
}
for (t = fsm_tbl[cnt]->t, i = 0; t; t = t->nxt)
i += fsm_tbl[t->to]->seen;
{ i += fsm_tbl[t->to]->seen;
}
if (i <= 1)
continue; /* b. */
{ continue; /* b. */
}
if (f->mod) /* final check in 2nd phase */
subgraph(a, f, cnt); /* possible entry-exit pair */
}
}
{ subgraph(a, f, cnt); /* possible entry-exit pair */
} } }
}
static void
@ -2178,27 +2163,26 @@ init_dom(AST *a)
for (f = a->fsm; f; f = f->nxt)
{ if (!f->seen) continue;
f->dom = (ulong *)
emalloc(a->nwords * sizeof(ulong));
f->dom = (ulong *) emalloc(a->nwords * sizeof(ulong));
if (f->from == a->i_st)
{ i = a->i_st / BPW;
j = a->i_st % BPW;
j = a->i_st % BPW; /* assert(j <= 32); */
f->dom[i] = (1<<j); /* (1) */
} else /* (2) */
{ for (i = 0; i < a->nwords; i++)
f->dom[i] = (ulong) ~0; /* all 1's */
{ f->dom[i] = (ulong) ~0; /* all 1's */
}
if (a->nstates % BPW)
for (i = (a->nstates % BPW); i < (int) BPW; i++)
f->dom[a->nwords-1] &= ~(1<<i); /* clear tail */
{ f->dom[a->nwords-1] &= ~(1<< ((ulong) i)); /* clear tail */
}
for (cnt = 0; cnt < a->nstates; cnt++)
if (!fsm_tbl[cnt]->seen)
{ if (!fsm_tbl[cnt]->seen)
{ i = cnt / BPW;
j = cnt % BPW;
f->dom[i] &= ~(1<<j);
} } }
j = cnt % BPW; /* assert(j <= 32); */
f->dom[i] &= ~(1<< ((ulong) j));
} } } }
}
static int
@ -2226,7 +2210,7 @@ dom_perculate(AST *a, FSM_state *f)
}
i = f->from / BPW;
j = f->from % BPW;
j = f->from % BPW; /* assert(j <= 32); */
ndom[i] |= (1<<j); /* (5a) */
for (i = 0; i < a->nwords; i++)
@ -2261,6 +2245,7 @@ AST_dominant(void)
FSM_trans *t;
AST *a;
int oi;
static FSM_state no_state;
#if 0
find dominators
Aho, Sethi, & Ullman, Compilers - principles, techniques, and tools

2878
sys/src/cmd/spin/pangen6.h Normal file
View File

File diff suppressed because it is too large Load Diff

923
sys/src/cmd/spin/pangen7.c Normal file
View File

@ -0,0 +1,923 @@
/***** spin: pangen7.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 <stdlib.h>
#include <assert.h>
#include "spin.h"
#include "y.tab.h"
#include <assert.h>
#ifndef PC
#include <unistd.h>
#endif
extern ProcList *rdy;
extern Element *Al_El;
extern int nclaims, verbose, Strict;
extern short has_accept;
typedef struct Succ_List Succ_List;
typedef struct SQueue SQueue;
typedef struct OneState OneState;
typedef struct State_Stack State_Stack;
typedef struct Guard Guard;
struct Succ_List {
SQueue *s;
Succ_List *nxt;
};
struct OneState {
int *combo; /* the combination of claim states */
Succ_List *succ; /* list of ptrs to immediate successor states */
};
struct SQueue {
OneState state;
SQueue *nxt;
};
struct State_Stack {
int *n;
State_Stack *nxt;
};
struct Guard {
Lextok *t;
Guard *nxt;
};
static SQueue *sq, *sd, *render; /* states move from sq to sd to render to holding */
static SQueue *holding, *lasthold;
static State_Stack *dsts;
static int nst; /* max nr of states in claims */
static int *Ist; /* initial states */
static int *Nacc; /* number of accept states in claim */
static int *Nst; /* next states */
static int **reached; /* n claims x states */
static int unfolding; /* to make sure all accept states are reached */
static int is_accept; /* remember if the current state is accepting in any claim */
static int not_printing; /* set during explore_product */
static Element ****matrix; /* n x two-dimensional arrays state x state */
static Element **Selfs; /* self-loop states at end of claims */
static void get_seq(int, Sequence *);
static void set_el(int n, Element *e);
static void gen_product(void);
static void print_state_nm(char *, int *, char *);
static SQueue *find_state(int *);
static SQueue *retrieve_state(int *);
static int
same_state(int *a, int *b)
{ int i;
for (i = 0; i < nclaims; i++)
{ if (a[i] != b[i])
{ return 0;
} }
return 1;
}
static int
in_stack(SQueue *s, SQueue *in)
{ SQueue *q;
for (q = in; q; q = q->nxt)
{ if (same_state(q->state.combo, s->state.combo))
{ return 1;
} }
return 0;
}
static void
to_render(SQueue *s)
{ SQueue *a, *q, *last; /* find in sd/sq and move to render, if not already there */
int n;
for (n = 0; n < nclaims; n++)
{ reached[n][ s->state.combo[n] ] |= 2;
}
for (q = render; q; q = q->nxt)
{ if (same_state(q->state.combo, s->state.combo))
{ return;
} }
for (q = holding; q; q = q->nxt)
{ if (same_state(q->state.combo, s->state.combo))
{ return;
} }
a = sd;
more:
for (q = a, last = 0; q; last = q, q = q->nxt)
{ if (same_state(q->state.combo, s->state.combo))
{ if (!last)
{ if (a == sd)
{ sd = q->nxt;
} else if (a == sq)
{ sq = q->nxt;
} else
{ holding = q->nxt;
}
} else
{ last->nxt = q->nxt;
}
q->nxt = render;
render = q;
return;
} }
if (verbose)
{ print_state_nm("looking for: ", s->state.combo, "\n");
}
(void) find_state(s->state.combo); /* creates it in sq */
if (a != sq)
{ a = sq;
goto more;
}
fatal("cannot happen, to_render", 0);
}
static void
wrap_text(char *pre, Lextok *t, char *post)
{
printf(pre, (char *) 0);
comment(stdout, t, 0);
printf(post, (char *) 0);
}
static State_Stack *
push_dsts(int *n)
{ State_Stack *s;
int i;
for (s = dsts; s; s = s->nxt)
{ if (same_state(s->n, n))
{ if (verbose&64)
{ printf("\n");
for (s = dsts; s; s = s->nxt)
{ print_state_nm("\t", s->n, "\n");
}
print_state_nm("\t", n, "\n");
}
return s;
} }
s = (State_Stack *) emalloc(sizeof(State_Stack));
s->n = (int *) emalloc(nclaims * sizeof(int));
for (i = 0; i < nclaims; i++)
s->n[i] = n[i];
s->nxt = dsts;
dsts = s;
return 0;
}
static void
pop_dsts(void)
{
assert(dsts != NULL);
dsts = dsts->nxt;
}
static void
complete_transition(Succ_List *sl, Guard *g)
{ Guard *w;
int cnt = 0;
printf(" :: ");
for (w = g; w; w = w->nxt)
{ if (w->t->ntyp == CONST
&& w->t->val == 1)
{ continue;
} else if (w->t->ntyp == 'c'
&& w->t->lft->ntyp == CONST
&& w->t->lft->val == 1)
{ continue; /* 'true' */
}
if (cnt > 0)
{ printf(" && ");
}
wrap_text("", w->t, "");
cnt++;
}
if (cnt == 0)
{ printf("true");
}
print_state_nm(" -> goto ", sl->s->state.combo, "");
if (is_accept > 0)
{ printf("_U%d\n", (unfolding+1)%nclaims);
} else
{ printf("_U%d\n", unfolding);
}
}
static void
state_body(OneState *s, Guard *guard)
{ Succ_List *sl;
State_Stack *y;
Guard *g;
int i, once;
for (sl = s->succ; sl; sl = sl->nxt)
{ once = 0;
for (i = 0; i < nclaims; i++)
{ Element *e;
e = matrix[i][s->combo[i]][sl->s->state.combo[i]];
/* if one of the claims has a DO or IF move
then pull its target state forward, once
*/
if (!e
|| e->n->ntyp == NON_ATOMIC
|| e->n->ntyp == DO
|| e->n->ntyp == IF)
{ s = &(sl->s->state);
y = push_dsts(s->combo);
if (!y)
{ if (once++ == 0)
{ assert(s->succ != NULL);
state_body(s, guard);
}
pop_dsts();
} else if (!y->nxt) /* self-loop transition */
{ if (!not_printing) printf(" /* self-loop */\n");
} else
{ /* non_fatal("loop in state body", 0); ** maybe ok */
}
continue;
} else
{ g = (Guard *) emalloc(sizeof(Guard));
g->t = e->n;
g->nxt = guard;
guard = g;
} }
if (guard && !once)
{ if (!not_printing) complete_transition(sl, guard);
to_render(sl->s);
} }
}
static struct X {
char *s; int n;
} spl[] = {
{"end", 3 },
{"accept", 6 },
{0, 0 },
};
static int slcnt;
extern Label *labtab;
static ProcList *
locate_claim(int n)
{ ProcList *p;
int i;
for (p = rdy, i = 0; p; p = p->nxt, i++) /* find claim name */
{ if (i == n)
{ break;
} }
assert(p && p->b == N_CLAIM);
return p;
}
static void
elim_lab(Element *e)
{ Label *l, *lst;
for (l = labtab, lst = NULL; l; lst = l, l = l->nxt)
{ if (l->e == e)
{ if (lst)
{ lst->nxt = l->nxt;
} else
{ labtab = l->nxt;
}
break;
} }
}
static int
claim_has_accept(ProcList *p)
{ Label *l;
for (l = labtab; l; l = l->nxt)
{ if (strcmp(l->c->name, p->n->name) == 0
&& strncmp(l->s->name, "accept", 6) == 0)
{ return 1;
} }
return 0;
}
static void
prune_accept(void)
{ int n;
for (n = 0; n < nclaims; n++)
{ if ((reached[n][Selfs[n]->seqno] & 2) == 0)
{ if (verbose)
{ printf("claim %d: selfloop not reachable\n", n);
}
elim_lab(Selfs[n]);
Nacc[n] = claim_has_accept(locate_claim(n));
} }
}
static void
mk_accepting(int n, Element *e)
{ ProcList *p;
Label *l;
int i;
assert(!Selfs[n]);
Selfs[n] = e;
l = (Label *) emalloc(sizeof(Label));
l->s = (Symbol *) emalloc(sizeof(Symbol));
l->s->name = "accept00";
l->c = (Symbol *) emalloc(sizeof(Symbol));
l->uiid = 0; /* this is not in an inline */
for (p = rdy, i = 0; p; p = p->nxt, i++) /* find claim name */
{ if (i == n)
{ l->c->name = p->n->name;
break;
} }
assert(p && p->b == N_CLAIM);
Nacc[n] = 1;
has_accept = 1;
l->e = e;
l->nxt = labtab;
labtab = l;
}
static void
check_special(int *nrs)
{ ProcList *p;
Label *l;
int i, j, nmatches;
int any_accepts = 0;
for (i = 0; i < nclaims; i++)
{ any_accepts += Nacc[i];
}
is_accept = 0;
for (j = 0; spl[j].n; j++) /* 2 special label prefixes */
{ nmatches = 0;
for (p = rdy, i = 0; p; p = p->nxt, i++) /* check each claim */
{ if (p->b != N_CLAIM)
{ continue;
}
/* claim i in state nrs[i], type p->tn, name p->n->name
* either the state has an accept label, or the claim has none,
* so that all its states should be considered accepting
* --- but only if other claims do have accept states!
*/
if (Strict == 0 && j == 1 && Nacc[i] == 0 && any_accepts > 0)
{ if ((verbose&32) && i == unfolding)
{ printf(" /* claim %d pseudo-accept */\n", i);
}
goto is_accepting;
}
for (l = labtab; l; l = l->nxt) /* check its labels */
{ if (strcmp(l->c->name, p->n->name) == 0 /* right claim */
&& l->e->seqno == nrs[i] /* right state */
&& strncmp(l->s->name, spl[j].s, spl[j].n) == 0)
{ if (j == 1) /* accept state */
{ char buf[32];
is_accepting: if (strchr(p->n->name, ':'))
{ sprintf(buf, "N%d", i);
} else
{ assert(strlen(p->n->name) < sizeof(buf));
strcpy(buf, p->n->name);
}
if (unfolding == 0 && i == 0)
{ if (!not_printing)
printf("%s_%s_%d:\n", /* true accept */
spl[j].s, buf, slcnt++);
} else if (verbose&32)
{ if (!not_printing)
printf("%s_%s%d:\n",
buf, spl[j].s, slcnt++);
}
if (i == unfolding)
{ is_accept++; /* move to next unfolding */
}
} else
{ nmatches++;
}
break;
} } }
if (j == 0 && nmatches == nclaims) /* end-state */
{ if (!not_printing)
{ printf("%s%d:\n", spl[j].s, slcnt++);
} } }
}
static int
render_state(SQueue *q)
{
if (!q || !q->state.succ)
{ if (verbose&64)
{ printf(" no exit\n");
}
return 0;
}
check_special(q->state.combo); /* accept or end-state labels */
dsts = (State_Stack *) 0;
push_dsts(q->state.combo); /* to detect loops */
if (!not_printing)
{ print_state_nm("", q->state.combo, ""); /* the name */
printf("_U%d:\n\tdo\n", unfolding);
}
state_body(&(q->state), (Guard *) 0);
if (!not_printing)
{ printf("\tod;\n");
}
pop_dsts();
return 1;
}
static void
explore_product(void)
{ SQueue *q;
/* all states are in the sd queue */
q = retrieve_state(Ist); /* retrieve from the sd q */
q->nxt = render; /* put in render q */
render = q;
do {
q = render;
render = render->nxt;
q->nxt = 0; /* remove from render q */
if (verbose&64)
{ print_state_nm("explore: ", q->state.combo, "\n");
}
not_printing = 1;
render_state(q); /* may add new states */
not_printing = 0;
if (lasthold)
{ lasthold->nxt = q;
lasthold = q;
} else
{ holding = lasthold = q;
}
} while (render);
assert(!dsts);
}
static void
print_product(void)
{ SQueue *q;
int cnt;
if (unfolding == 0)
{ printf("never Product {\n"); /* name expected by iSpin */
q = find_state(Ist); /* should find it in the holding q */
assert(q != NULL);
q->nxt = holding; /* put it at the front */
holding = q;
}
render = holding;
holding = lasthold = 0;
printf("/* ============= U%d ============= */\n", unfolding);
cnt = 0;
do {
q = render;
render = render->nxt;
q->nxt = 0;
if (verbose&64)
{ print_state_nm("print: ", q->state.combo, "\n");
}
cnt += render_state(q);
if (lasthold)
{ lasthold->nxt = q;
lasthold = q;
} else
{ holding = lasthold = q;
}
} while (render);
assert(!dsts);
if (cnt == 0)
{ printf(" 0;\n");
}
if (unfolding == nclaims-1)
{ printf("}\n");
}
}
static void
prune_dead(void)
{ Succ_List *sl, *last;
SQueue *q;
int cnt;
do { cnt = 0;
for (q = sd; q; q = q->nxt)
{ /* if successor is deadend, remove it
* unless it's a move to the end-state of the claim
*/
last = (Succ_List *) 0;
for (sl = q->state.succ; sl; last = sl, sl = sl->nxt)
{ if (!sl->s->state.succ) /* no successor */
{ if (!last)
{ q->state.succ = sl->nxt;
} else
{ last->nxt = sl->nxt;
}
cnt++;
} } }
} while (cnt > 0);
}
static void
print_raw(void)
{ int i, j, n;
printf("#if 0\n");
for (n = 0; n < nclaims; n++)
{ printf("C%d:\n", n);
for (i = 0; i < nst; i++)
{ if (reached[n][i])
for (j = 0; j < nst; j++)
{ if (matrix[n][i][j])
{ if (reached[n][i] & 2) printf("+");
if (i == Ist[n]) printf("*");
printf("\t%d", i);
wrap_text(" -[", matrix[n][i][j]->n, "]->\t");
printf("%d\n", j);
} } } }
printf("#endif\n\n");
fflush(stdout);
}
void
sync_product(void)
{ ProcList *p;
Element *e;
int n, i;
if (nclaims <= 1) return;
(void) unlink("pan.pre");
Ist = (int *) emalloc(sizeof(int) * nclaims);
Nacc = (int *) emalloc(sizeof(int) * nclaims);
Nst = (int *) emalloc(sizeof(int) * nclaims);
reached = (int **) emalloc(sizeof(int *) * nclaims);
Selfs = (Element **) emalloc(sizeof(Element *) * nclaims);
matrix = (Element ****) emalloc(sizeof(Element ***) * nclaims); /* claims */
for (p = rdy, i = 0; p; p = p->nxt, i++)
{ if (p->b == N_CLAIM)
{ nst = max(p->s->maxel, nst);
Nacc[i] = claim_has_accept(p);
} }
for (n = 0; n < nclaims; n++)
{ reached[n] = (int *) emalloc(sizeof(int) * nst);
matrix[n] = (Element ***) emalloc(sizeof(Element **) * nst); /* rows */
for (i = 0; i < nst; i++) /* cols */
{ matrix[n][i] = (Element **) emalloc(sizeof(Element *) * nst);
} }
for (e = Al_El; e; e = e->Nxt)
{ e->status &= ~DONE;
}
for (p = rdy, n=0; p; p = p->nxt, n++)
{ if (p->b == N_CLAIM)
{ /* fill in matrix[n] */
e = p->s->frst;
Ist[n] = huntele(e, e->status, -1)->seqno;
reached[n][Ist[n]] = 1|2;
get_seq(n, p->s);
} }
if (verbose) /* show only the input automata */
{ print_raw();
}
gen_product(); /* create product automaton */
}
static int
nxt_trans(int n, int cs, int frst)
{ int j;
for (j = frst; j < nst; j++)
{ if (reached[n][cs]
&& matrix[n][cs][j])
{ return j;
} }
return -1;
}
static void
print_state_nm(char *p, int *s, char *a)
{ int i;
printf("%sP", p);
for (i = 0; i < nclaims; i++)
{ printf("_%d", s[i]);
}
printf("%s", a);
}
static void
create_transition(OneState *s, SQueue *it)
{ int n, from, upto;
int *F = s->combo;
int *T = it->state.combo;
Succ_List *sl;
Lextok *t;
if (verbose&64)
{ print_state_nm("", F, " ");
print_state_nm("-> ", T, "\t");
}
/* check if any of the claims is blocked */
/* which makes the state a dead-end */
for (n = 0; n < nclaims; n++)
{ from = F[n];
upto = T[n];
t = matrix[n][from][upto]->n;
if (verbose&64)
{ wrap_text("", t, " ");
}
if (t->ntyp == 'c'
&& t->lft->ntyp == CONST)
{ if (t->lft->val == 0) /* i.e., false */
{ goto done;
} } }
sl = (Succ_List *) emalloc(sizeof(Succ_List));
sl->s = it;
sl->nxt = s->succ;
s->succ = sl;
done:
if (verbose&64)
{ printf("\n");
}
}
static SQueue *
find_state(int *cs)
{ SQueue *nq, *a = sq;
int i;
again: /* check in nq, sq, and then in the render q */
for (nq = a; nq; nq = nq->nxt)
{ if (same_state(nq->state.combo, cs))
{ return nq; /* found */
} }
if (a == sq && sd)
{ a = sd;
goto again; /* check the other stack too */
} else if (a == sd && render)
{ a = render;
goto again;
}
nq = (SQueue *) emalloc(sizeof(SQueue));
nq->state.combo = (int *) emalloc(nclaims * sizeof(int));
for (i = 0; i < nclaims; i++)
{ nq->state.combo[i] = cs[i];
}
nq->nxt = sq; /* add to sq stack */
sq = nq;
return nq;
}
static SQueue *
retrieve_state(int *s)
{ SQueue *nq, *last = NULL;
for (nq = sd; nq; last = nq, nq = nq->nxt)
{ if (same_state(nq->state.combo, s))
{ if (last)
{ last->nxt = nq->nxt;
} else
{ sd = nq->nxt; /* 6.4.0: was sd = nq */
}
return nq; /* found */
} }
fatal("cannot happen: retrieve_state", 0);
return (SQueue *) 0;
}
static void
all_successors(int n, OneState *cur)
{ int i, j = 0;
if (n >= nclaims)
{ create_transition(cur, find_state(Nst));
} else
{ i = cur->combo[n];
for (;;)
{ j = nxt_trans(n, i, j);
if (j < 0) break;
Nst[n] = j;
all_successors(n+1, cur);
j++;
} }
}
static void
gen_product(void)
{ OneState *cur_st;
SQueue *q;
find_state(Ist); /* create initial state */
while (sq)
{ if (in_stack(sq, sd))
{ sq = sq->nxt;
continue;
}
cur_st = &(sq->state);
q = sq;
sq = sq->nxt; /* delete from sq stack */
q->nxt = sd; /* and move to done stack */
sd = q;
all_successors(0, cur_st);
}
/* all states are in the sd queue now */
prune_dead();
explore_product(); /* check if added accept-self-loops are reachable */
prune_accept();
if (verbose)
{ print_raw();
}
/* PM: merge states with identical successor lists */
/* all outgoing transitions from accept-states
from claim n in copy n connect to states in copy (n+1)%nclaims
only accept states from claim 0 in copy 0 are true accept states
in the product
PM: what about claims that have no accept states (e.g., restrictions)
*/
for (unfolding = 0; unfolding < nclaims; unfolding++)
{ print_product();
}
}
static void
t_record(int n, Element *e, Element *g)
{ int from = e->seqno, upto = g?g->seqno:0;
assert(from >= 0 && from < nst);
assert(upto >= 0 && upto < nst);
matrix[n][from][upto] = e;
reached[n][upto] |= 1;
}
static void
get_sub(int n, Element *e)
{
if (e->n->ntyp == D_STEP
|| e->n->ntyp == ATOMIC)
{ fatal("atomic or d_step in never claim product", 0);
}
/* NON_ATOMIC */
e->n->sl->this->last->nxt = e->nxt;
get_seq(n, e->n->sl->this);
t_record(n, e, e->n->sl->this->frst);
}
static void
set_el(int n, Element *e)
{ Element *g;
if (e->n->ntyp == '@') /* change to self-loop */
{ e->n->ntyp = CONST;
e->n->val = 1; /* true */
e->nxt = e;
g = e;
mk_accepting(n, e);
} else
if (e->n->ntyp == GOTO)
{ g = get_lab(e->n, 1);
g = huntele(g, e->status, -1);
} else if (e->nxt)
{ g = huntele(e->nxt, e->status, -1);
} else
{ g = NULL;
}
t_record(n, e, g);
}
static void
get_seq(int n, Sequence *s)
{ SeqList *h;
Element *e;
e = huntele(s->frst, s->frst->status, -1);
for ( ; e; e = e->nxt)
{ if (e->status & DONE)
{ goto checklast;
}
e->status |= DONE;
if (e->n->ntyp == UNLESS)
{ fatal("unless stmnt in never claim product", 0);
}
if (e->sub) /* IF or DO */
{ Lextok *x = NULL;
Lextok *y = NULL;
Lextok *haselse = NULL;
for (h = e->sub; h; h = h->nxt)
{ Lextok *t = h->this->frst->n;
if (t->ntyp == ELSE)
{ if (verbose&64) printf("else at line %d\n", t->ln);
haselse = t;
continue;
}
if (t->ntyp != 'c')
{ fatal("product, 'else' combined with non-condition", 0);
}
if (t->lft->ntyp == CONST /* true */
&& t->lft->val == 1
&& y == NULL)
{ y = nn(ZN, CONST, ZN, ZN);
y->val = 0;
} else
{ if (!x)
x = t;
else
x = nn(ZN, OR, x, t);
if (verbose&64)
{ wrap_text(" [", x, "]\n");
} } }
if (haselse)
{ if (!y)
{ y = nn(ZN, '!', x, ZN);
}
if (verbose&64)
{ wrap_text(" [else: ", y, "]\n");
}
haselse->ntyp = 'c'; /* replace else */
haselse->lft = y;
}
for (h = e->sub; h; h = h->nxt)
{ t_record(n, e, h->this->frst);
get_seq(n, h->this);
}
} else
{ if (e->n->ntyp == ATOMIC
|| e->n->ntyp == D_STEP
|| e->n->ntyp == NON_ATOMIC)
{ get_sub(n, e);
} else
{ set_el(n, e);
}
}
checklast: if (e == s->last)
break;
}
}

2413
sys/src/cmd/spin/pangen7.h Normal file
View File

File diff suppressed because it is too large Load Diff

270
sys/src/cmd/spin/reprosrc.c
View File

@ -1,22 +1,21 @@
/***** spin: reprosrc.c *****/
/* Copyright (c) 2002-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 */
/*
* 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 <stdio.h>
#include <assert.h>
#include "spin.h"
#include "y.tab.h"
static int indent = 1;
extern YYSTYPE yylval;
extern ProcList *rdy;
void repro_seq(Sequence *);
static void repro_seq(Sequence *);
void
doindent(void)
@ -48,7 +47,7 @@ repro_sub(Element *e)
printf(" };\n");
}
void
static void
repro_seq(Sequence *s)
{ Element *e;
Symbol *v;
@ -96,7 +95,7 @@ repro_seq(Sequence *s)
doindent();
if (e->n->ntyp == C_CODE)
{ printf("c_code ");
plunk_inline(stdout, e->n->sym->name, 1);
plunk_inline(stdout, e->n->sym->name, 1, 1);
} else if (e->n->ntyp == 'c'
&& e->n->lft->ntyp == C_EXPR)
{ printf("c_expr { ");
@ -134,3 +133,252 @@ repro_src(void)
{
repro_proc(rdy);
}
static int in_decl;
static int in_c_decl;
static int in_c_code;
void
blip(int n, char *b)
{ char mtxt[1024];
strcpy(mtxt, "");
switch (n) {
default: if (n > 0 && n < 256)
sprintf(mtxt, "%c", n);
else
sprintf(mtxt, "<%d?>", n);
break;
case '(': strcpy(mtxt, "("); in_decl++; break;
case ')': strcpy(mtxt, ")"); in_decl--; break;
case '{': strcpy(mtxt, "{"); break;
case '}': strcpy(mtxt, "}"); break;
case '\t': sprintf(mtxt, "\\t"); break;
case '\f': sprintf(mtxt, "\\f"); break;
case '\n': sprintf(mtxt, "\\n"); break;
case '\r': sprintf(mtxt, "\\r"); break;
case 'c': sprintf(mtxt, "condition"); break;
case 's': sprintf(mtxt, "send"); break;
case 'r': sprintf(mtxt, "recv"); break;
case 'R': sprintf(mtxt, "recv poll"); break;
case '@': sprintf(mtxt, "@"); break;
case '?': sprintf(mtxt, "(x->y:z)"); break;
case NEXT: sprintf(mtxt, "X"); break;
case ALWAYS: sprintf(mtxt, "[]"); break;
case EVENTUALLY: sprintf(mtxt, "<>"); break;
case IMPLIES: sprintf(mtxt, "->"); break;
case EQUIV: sprintf(mtxt, "<->"); break;
case UNTIL: sprintf(mtxt, "U"); break;
case WEAK_UNTIL: sprintf(mtxt, "W"); break;
case IN: sprintf(mtxt, "in"); break;
case ACTIVE: sprintf(mtxt, "active"); break;
case AND: sprintf(mtxt, "&&"); break;
case ARROW: sprintf(mtxt, "->"); break;
case ASGN: sprintf(mtxt, "="); break;
case ASSERT: sprintf(mtxt, "assert"); break;
case ATOMIC: sprintf(mtxt, "atomic"); break;
case BREAK: sprintf(mtxt, "break"); break;
case C_CODE: sprintf(mtxt, "c_code"); in_c_code++; break;
case C_DECL: sprintf(mtxt, "c_decl"); in_c_decl++; break;
case C_EXPR: sprintf(mtxt, "c_expr"); break;
case C_STATE: sprintf(mtxt, "c_state"); break;
case C_TRACK: sprintf(mtxt, "c_track"); break;
case CLAIM: sprintf(mtxt, "never"); break;
case CONST: sprintf(mtxt, "%d", yylval->val); break;
case DECR: sprintf(mtxt, "--"); break;
case D_STEP: sprintf(mtxt, "d_step"); break;
case D_PROCTYPE: sprintf(mtxt, "d_proctype"); break;
case DO: sprintf(mtxt, "do"); break;
case DOT: sprintf(mtxt, "."); break;
case ELSE: sprintf(mtxt, "else"); break;
case EMPTY: sprintf(mtxt, "empty"); break;
case ENABLED: sprintf(mtxt, "enabled"); break;
case EQ: sprintf(mtxt, "=="); break;
case EVAL: sprintf(mtxt, "eval"); break;
case FI: sprintf(mtxt, "fi"); break;
case FULL: sprintf(mtxt, "full"); break;
case GE: sprintf(mtxt, ">="); break;
case GET_P: sprintf(mtxt, "get_priority"); break;
case GOTO: sprintf(mtxt, "goto"); break;
case GT: sprintf(mtxt, ">"); break;
case HIDDEN: sprintf(mtxt, "hidden"); break;
case IF: sprintf(mtxt, "if"); break;
case INCR: sprintf(mtxt, "++"); break;
case INLINE: sprintf(mtxt, "inline"); break;
case INIT: sprintf(mtxt, "init"); break;
case ISLOCAL: sprintf(mtxt, "local"); break;
case LABEL: sprintf(mtxt, "<label-name>"); break;
case LE: sprintf(mtxt, "<="); break;
case LEN: sprintf(mtxt, "len"); break;
case LSHIFT: sprintf(mtxt, "<<"); break;
case LT: sprintf(mtxt, "<"); break;
case LTL: sprintf(mtxt, "ltl"); break;
case NAME: sprintf(mtxt, "%s", yylval->sym->name); break;
case XU: switch (yylval->val) {
case XR: sprintf(mtxt, "xr"); break;
case XS: sprintf(mtxt, "xs"); break;
default: sprintf(mtxt, "<?>"); break;
}
break;
case TYPE: switch (yylval->val) {
case BIT: sprintf(mtxt, "bit"); break;
case BYTE: sprintf(mtxt, "byte"); break;
case CHAN: sprintf(mtxt, "chan"); in_decl++; break;
case INT: sprintf(mtxt, "int"); break;
case MTYPE: sprintf(mtxt, "mtype"); break;
case SHORT: sprintf(mtxt, "short"); break;
case UNSIGNED: sprintf(mtxt, "unsigned"); break;
default: sprintf(mtxt, "<unknown type>"); break;
}
break;
case NE: sprintf(mtxt, "!="); break;
case NEG: sprintf(mtxt, "!"); break;
case NEMPTY: sprintf(mtxt, "nempty"); break;
case NFULL: sprintf(mtxt, "nfull"); break;
case NON_ATOMIC: sprintf(mtxt, "<sub-sequence>"); break;
case NONPROGRESS: sprintf(mtxt, "np_"); break;
case OD: sprintf(mtxt, "od"); break;
case OF: sprintf(mtxt, "of"); break;
case OR: sprintf(mtxt, "||"); break;
case O_SND: sprintf(mtxt, "!!"); break;
case PC_VAL: sprintf(mtxt, "pc_value"); break;
case PRINT: sprintf(mtxt, "printf"); break;
case PRINTM: sprintf(mtxt, "printm"); break;
case PRIORITY: sprintf(mtxt, "priority"); break;
case PROCTYPE: sprintf(mtxt, "proctype"); break;
case PROVIDED: sprintf(mtxt, "provided"); break;
case RCV: sprintf(mtxt, "?"); break;
case R_RCV: sprintf(mtxt, "??"); break;
case RSHIFT: sprintf(mtxt, ">>"); break;
case RUN: sprintf(mtxt, "run"); break;
case SEP: sprintf(mtxt, "::"); break;
case SEMI: sprintf(mtxt, ";"); break;
case SET_P: sprintf(mtxt, "set_priority"); break;
case SHOW: sprintf(mtxt, "show"); break;
case SND: sprintf(mtxt, "!"); break;
case INAME:
case UNAME:
case PNAME:
case STRING: sprintf(mtxt, "%s", yylval->sym->name); break;
case TRACE: sprintf(mtxt, "trace"); break;
case TIMEOUT: sprintf(mtxt, "timeout"); break;
case TYPEDEF: sprintf(mtxt, "typedef"); break;
case UMIN: sprintf(mtxt, "-"); break;
case UNLESS: sprintf(mtxt, "unless"); break;
}
strcat(b, mtxt);
}
void
purge(char *b)
{
if (strlen(b) == 0) return;
if (b[strlen(b)-1] != ':') /* label? */
{ if (b[0] == ':' && b[1] == ':')
{ indent--;
doindent();
indent++;
} else
{ doindent();
}
}
printf("%s\n", b);
strcpy(b, "");
in_decl = 0;
in_c_code = 0;
in_c_decl = 0;
}
int pp_mode;
extern int lex(void);
void
pretty_print(void)
{ int c, lastc = 0;
char buf[1024];
pp_mode = 1;
indent = 0;
strcpy(buf, "");
while ((c = lex()) != EOF)
{
if ((lastc == IF || lastc == DO) && c != SEP)
{ indent--; /* c_code if */
}
if (c == C_DECL || c == C_STATE
|| c == C_TRACK || c == SEP
|| c == DO || c == IF
|| (c == TYPE && !in_decl))
{ purge(buf); /* start on new line */
}
if (c == '{'
&& lastc != OF && lastc != IN
&& lastc != ATOMIC && lastc != D_STEP
&& lastc != C_CODE && lastc != C_DECL && lastc != C_EXPR)
{ purge(buf);
}
if (c == PREPROC)
{ int oi = indent;
purge(buf);
assert(strlen(yylval->sym->name) < sizeof(buf));
strcpy(buf, yylval->sym->name);
indent = 0;
purge(buf);
indent = oi;
continue;
}
if (c != ':' && c != SEMI
&& c != ',' && c != '('
&& c != '#' && lastc != '#'
&& c != ARROW && lastc != ARROW
&& c != '.' && lastc != '.'
&& c != '!' && lastc != '!'
&& c != SND && lastc != SND
&& c != RCV && lastc != RCV
&& c != O_SND && lastc != O_SND
&& c != R_RCV && lastc != R_RCV
&& (c != ']' || lastc != '[')
&& (c != '>' || lastc != '<')
&& (c != GT || lastc != LT)
&& c != '@' && lastc != '@'
&& c != DO && c != OD && c != IF && c != FI
&& c != SEP && strlen(buf) > 0)
strcat(buf, " ");
if (c == '}' || c == OD || c == FI)
{ purge(buf);
indent--;
}
blip(c, buf);
if (c == '{' || c == DO || c == IF)
{ purge(buf);
indent++;
}
if (c == '}' || c == BREAK || c == SEMI
|| (c == ':' && lastc == NAME))
{ purge(buf);
}
lastc = c;
}
purge(buf);
}

219
sys/src/cmd/spin/run.c
View File

@ -1,13 +1,10 @@
/***** 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 */
/*
* 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 <stdlib.h>
#include "spin.h"
@ -16,15 +13,18 @@
extern RunList *X, *run;
extern Symbol *Fname;
extern Element *LastStep;
extern int Rvous, lineno, Tval, interactive, MadeChoice;
extern int Rvous, lineno, Tval, interactive, MadeChoice, Priority_Sum;
extern int TstOnly, verbose, s_trail, xspin, jumpsteps, depth;
extern int nproc, nstop, no_print, like_java;
extern int analyze, nproc, nstop, no_print, like_java, old_priority_rules;
extern short Have_claim;
static long Seed = 1;
static int E_Check = 0, Escape_Check = 0;
static int eval_sync(Element *);
static int pc_enabled(Lextok *n);
static int get_priority(Lextok *n);
static void set_priority(Lextok *n, Lextok *m);
extern void sr_buf(int, int);
void
@ -42,24 +42,23 @@ Rand(void)
Element *
rev_escape(SeqList *e)
{ Element *r;
{ Element *r = (Element *) 0;
if (!e)
return (Element *) 0;
if (e)
{ if ((r = rev_escape(e->nxt)) == ZE) /* reversed order */
{ r = eval_sub(e->this->frst);
} }
if ((r = rev_escape(e->nxt)) != ZE) /* reversed order */
return r;
return eval_sub(e->this->frst);
return r;
}
Element *
eval_sub(Element *e)
{ Element *f, *g;
SeqList *z;
int i, j, k;
int i, j, k, only_pos;
if (!e->n)
if (!e || !e->n)
return ZE;
#ifdef DEBUG
printf("\n\teval_sub(%d %s: line %d) ",
@ -69,8 +68,13 @@ eval_sub(Element *e)
#endif
if (e->n->ntyp == GOTO)
{ if (Rvous) return ZE;
LastStep = e; f = get_lab(e->n, 1);
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)
@ -80,6 +84,7 @@ eval_sub(Element *e)
{ Element *has_else = ZE;
Element *bas_else = ZE;
int nr_else = 0, nr_choices = 0;
only_pos = -1;
if (interactive
&& !MadeChoice && !E_Check
@ -89,8 +94,10 @@ eval_sub(Element *e)
{ printf("Select stmnt (");
whoruns(0); printf(")\n");
if (nproc-nstop > 1)
printf("\tchoice 0: other process\n");
}
{ printf("\tchoice 0: other process\n");
nr_choices++;
only_pos = 0;
} }
for (z = e->sub, j=0; z; z = z->nxt)
{ j++;
if (interactive
@ -113,13 +120,21 @@ eval_sub(Element *e)
if (!Enabled0(z->this->frst))
printf("unexecutable, ");
else
nr_choices++;
{ 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);
{ 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
@ -132,8 +147,11 @@ eval_sub(Element *e)
else
printf("Select [0-%d]: ", j);
fflush(stdout);
scanf("%s", buf);
if (isdigit(buf[0]))
if (scanf("%64s", buf) <= 0)
{ printf("no input\n");
return ZE;
}
if (isdigit((int)buf[0]))
k = atoi(buf);
else
{ if (buf[0] == 'q')
@ -155,6 +173,7 @@ eval_sub(Element *e)
else
k = Rand()%j; /* nondeterminism */
}
has_else = ZE;
bas_else = ZE;
for (i = 0, z = e->sub; i < j+k; i++)
@ -215,7 +234,7 @@ eval_sub(Element *e)
} else
{ SeqList *x;
if (!(e->status & (D_ATOM))
&& e->esc && verbose&32)
&& e->esc && (verbose&32))
{ printf("Stmnt [");
comment(stdout, e->n, 0);
printf("] has escape(s): ");
@ -233,12 +252,19 @@ eval_sub(Element *e)
#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");
{ printf("\tEscape taken (-J) ");
if (g->n && g->n->fn)
printf("%s:%d", g->n->fn->name, g->n->ln);
printf("\n");
}
Escape_Check--;
return g;
}
@ -246,18 +272,24 @@ eval_sub(Element *e)
{ for (x = e->esc; x; x = x->nxt)
{ if ((g = eval_sub(x->this->frst)) != ZE)
{ if (verbose&4)
printf("\tEscape taken\n");
{ 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 ASGN:
if (check_track(e->n) == STRUCT) { break; }
/* else fall thru */
case TIMEOUT: case RUN:
case PRINT: case PRINTM:
case C_CODE: case C_EXPR:
case ASGN: case ASSERT:
case ASSERT:
case 's': case 'r': case 'c':
/* toplevel statements only */
LastStep = e;
@ -308,7 +340,8 @@ assign(Lextok *now)
t = Sym_typ(now->rgt);
break;
}
typ_ck(Sym_typ(now->lft), t, "assignment");
typ_ck(Sym_typ(now->lft), t, "assignment");
return setval(now->lft, eval(now->rgt));
}
@ -371,6 +404,10 @@ eval(Lextok *now)
case NEMPTY: return (qlen(now)>0);
case ENABLED: if (s_trail) return 1;
return pc_enabled(now->lft);
case GET_P: return get_priority(now->lft);
case SET_P: set_priority(now->lft->lft, now->lft->rgt); return 1;
case EVAL: return eval(now->lft);
case PC_VAL: return pc_value(now->lft);
case NONPROGRESS: return nonprogress();
@ -384,15 +421,21 @@ eval(Lextok *now)
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 ASGN:
if (check_track(now) == STRUCT) { return 1; }
return assign(now);
case C_CODE: printf("%s:\t", now->sym->name);
plunk_inline(stdout, now->sym->name, 0);
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: printf("%s:\t", now->sym->name);
plunk_expr(stdout, now->sym->name);
printf("\n");
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;
@ -407,6 +450,11 @@ eval(Lextok *now)
case '.': return 1; /* return label for compound */
case '@': return 0; /* stop state */
case ELSE: return 1; /* only hit here in guided trails */
case ',': /* reached through option -A with array initializer */
case 0:
return 0; /* not great, but safe */
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);
@ -426,7 +474,6 @@ printm(FILE *fd, Lextok *n)
j = n->lft->val;
else
j = eval(n->lft);
Buf[0] = '\0';
sr_buf(j, 1);
dotag(fd, Buf);
}
@ -437,9 +484,9 @@ int
interprint(FILE *fd, Lextok *n)
{ Lextok *tmp = n->lft;
char c, *s = n->sym->name;
int i, j; char lbuf[512];
extern char Buf[];
char tBuf[4096];
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)
@ -490,7 +537,7 @@ append: strcat(Buf, lbuf);
}
dotag(fd, Buf);
}
if (strlen(Buf) > 4096) fatal("printf string too long", 0);
if (strlen(Buf) >= 4096) fatal("printf string too long", 0);
return 1;
}
@ -512,6 +559,7 @@ Enabled1(Lextok *n)
verbose = v;
return i;
case SET_P:
case C_CODE: case C_EXPR:
case PRINT: case PRINTM:
case ASGN: case ASSERT:
@ -552,6 +600,7 @@ Enabled0(Element *e)
case '@':
return X->pid == (nproc-nstop-1);
case '.':
case SET_P:
return 1;
case GOTO:
if (Rvous) return 0;
@ -594,9 +643,91 @@ pc_enabled(Lextok *n)
for (Y = run; Y; Y = Y->nxt)
if (--i == pid)
{ oX = X; X = Y;
result = Enabled0(Y->pc);
result = Enabled0(X->pc);
X = oX;
break;
}
return result;
}
int
pc_highest(Lextok *n)
{ int i = nproc - nstop;
int pid = eval(n);
int target = 0, result = 1;
RunList *Y, *oX;
if (X->prov && !eval(X->prov)) return 0; /* can't be highest unless fully enabled */
for (Y = run; Y; Y = Y->nxt)
{ if (--i == pid)
{ target = Y->priority;
break;
} }
if (0) printf("highest for pid %d @ priority = %d\n", pid, target);
oX = X;
i = nproc - nstop;
for (Y = run; Y; Y = Y->nxt)
{ i--;
if (0) printf(" pid %d @ priority %d\t", Y->pid, Y->priority);
if (Y->priority > target)
{ X = Y;
if (0) printf("enabled: %s\n", Enabled0(X->pc)?"yes":"nope");
if (0) printf("provided: %s\n", eval(X->prov)?"yes":"nope");
if (Enabled0(X->pc) && (!X->prov || eval(X->prov)))
{ result = 0;
break;
} }
else
if (0) printf("\n");
}
X = oX;
return result;
}
int
get_priority(Lextok *n)
{ int i = nproc - nstop;
int pid = eval(n);
RunList *Y;
if (old_priority_rules)
{ return 1;
}
for (Y = run; Y; Y = Y->nxt)
{ if (--i == pid)
{ return Y->priority;
} }
return 0;
}
void
set_priority(Lextok *n, Lextok *p)
{ int i = nproc - nstop - Have_claim;
int pid = eval(n);
RunList *Y;
if (old_priority_rules)
{ return;
}
for (Y = run; Y; Y = Y->nxt)
{ if (--i == pid)
{ Priority_Sum -= Y->priority;
Y->priority = eval(p);
Priority_Sum += Y->priority;
if (1)
{ printf("%3d: setting priority of proc %d (%s) to %d\n",
depth, pid, Y->n->name, Y->priority);
} } }
if (verbose&32)
{ printf("\tPid\tName\tPriority\n");
for (Y = run; Y; Y = Y->nxt)
{ printf("\t%d\t%s\t%d\n",
Y->pid,
Y->n->name,
Y->priority);
} }
}

296
sys/src/cmd/spin/sched.c
View File

@ -1,13 +1,10 @@
/***** spin: sched.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 */
/*
* 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 <stdlib.h>
#include "spin.h"
@ -19,19 +16,21 @@ extern Ordered *all_names;
extern Symbol *Fname, *context;
extern int lineno, nr_errs, dumptab, xspin, jumpsteps, columns;
extern int u_sync, Elcnt, interactive, TstOnly, cutoff;
extern short has_enabled;
extern int limited_vis;
extern short has_enabled, has_priority, has_code, replay;
extern int limited_vis, product, nclaims, old_priority_rules;
extern int old_scope_rules, scope_seq[128], scope_level, has_stdin;
extern int pc_highest(Lextok *n);
RunList *X = (RunList *) 0;
RunList *run = (RunList *) 0;
RunList *LastX = (RunList *) 0; /* previous executing proc */
ProcList *rdy = (ProcList *) 0;
Element *LastStep = ZE;
int nproc=0, nstop=0, Tval=0;
int nproc=0, nstop=0, Tval=0, Priority_Sum = 0;
int Rvous=0, depth=0, nrRdy=0, MadeChoice;
short Have_claim=0, Skip_claim=0;
static int Priority_Sum = 0;
static void setlocals(RunList *);
static void setparams(RunList *, ProcList *, Lextok *);
static void talk(RunList *);
@ -42,13 +41,20 @@ runnable(ProcList *p, int weight, int noparams)
r->n = p->n;
r->tn = p->tn;
r->b = p->b;
r->pid = nproc++ - nstop + Skip_claim;
r->priority = weight;
p->priority = (unsigned char) weight; /* not quite the best place of course */
if ((verbose&4) || (verbose&32))
printf("Starting %s with pid %d\n", p->n->name, r->pid);
if (!noparams && ((verbose&4) || (verbose&32)))
{ printf("Starting %s with pid %d",
p->n?p->n->name:"--", r->pid);
if (has_priority) printf(" priority %d", r->priority);
printf("\n");
}
if (!p->s)
fatal("parsing error, no sequence %s", p->n?p->n->name:"--");
fatal("parsing error, no sequence %s",
p->n?p->n->name:"--");
r->pc = huntele(p->s->frst, p->s->frst->status, -1);
r->ps = p->s;
@ -58,14 +64,18 @@ runnable(ProcList *p, int weight, int noparams)
r->nxt = run;
r->prov = p->prov;
r->priority = weight;
if (weight < 1 || weight > 255)
{ fatal("bad process priority, valid range: 1..255", (char *) 0);
}
if (noparams) setlocals(r);
Priority_Sum += weight;
run = r;
}
ProcList *
ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov)
ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov, enum btypes b)
/* n=name, p=formals, s=body det=deterministic prov=provided */
{ ProcList *r = (ProcList *) emalloc(sizeof(ProcList));
Lextok *fp, *fpt; int j; extern int Npars;
@ -73,9 +83,15 @@ ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov)
r->n = n;
r->p = p;
r->s = s;
r->b = b;
r->prov = prov;
r->tn = nrRdy++;
r->det = (short) det;
r->tn = (short) nrRdy++;
n->sc = scope_seq[scope_level]; /* scope_level should be 0 */
if (det != 0 && det != 1)
{ fprintf(stderr, "spin: bad value for det (cannot happen)\n");
}
r->det = (unsigned char) det;
r->nxt = rdy;
rdy = r;
@ -128,13 +144,15 @@ announce(char *w)
run->pid - Have_claim, run->n->name);
pstext(run->pid - Have_claim, Buf);
} else
printf("proc %d = %s\n",
run->pid - Have_claim, run->n->name);
{ printf("proc %d = %s\n",
run->pid - Have_claim, run->n->name);
}
return;
}
if (dumptab
|| analyze
|| product
|| s_trail
|| !(verbose&4))
return;
@ -161,9 +179,11 @@ enable(Lextok *m)
Symbol *s = m->sym; /* proctype name */
Lextok *n = m->lft; /* actual parameters */
if (m->val < 1) m->val = 1; /* minimum priority */
if (m->val < 1)
{ m->val = 1; /* minimum priority */
}
for (p = rdy; p; p = p->nxt)
if (strcmp(s->name, p->n->name) == 0)
{ if (strcmp(s->name, p->n->name) == 0)
{ if (nproc-nstop >= MAXP)
{ printf("spin: too many processes (%d max)\n", MAXP);
break;
@ -173,7 +193,7 @@ enable(Lextok *m)
setparams(run, p, n);
setlocals(run); /* after setparams */
return run->pid - Have_claim + Skip_claim; /* effective simu pid */
}
} }
return 0; /* process not found */
}
@ -208,26 +228,29 @@ start_claim(int n)
RunList *r, *q = (RunList *) 0;
for (p = rdy; p; p = p->nxt)
if (p->tn == n
&& strcmp(p->n->name, ":never:") == 0)
if (p->tn == n && p->b == N_CLAIM)
{ runnable(p, 1, 1);
goto found;
}
printf("spin: couldn't find claim (ignored)\n");
printf("spin: couldn't find claim %d (ignored)\n", n);
if (verbose&32)
for (p = rdy; p; p = p->nxt)
printf("\t%d = %s\n", p->tn, p->n->name);
Skip_claim = 1;
goto done;
found:
/* move claim to far end of runlist, and reassign it pid 0 */
if (columns == 2)
{ depth = 0;
pstext(0, "0::never:");
{ extern char Buf[];
depth = 0;
sprintf(Buf, "%d:%s", 0, p->n->name);
pstext(0, Buf);
for (r = run; r; r = r->nxt)
{ if (!strcmp(r->n->name, ":never:"))
continue;
sprintf(Buf, "%d:%s",
r->pid+1, r->n->name);
pstext(r->pid+1, Buf);
} }
{ if (r->b != N_CLAIM)
{ sprintf(Buf, "%d:%s", r->pid+1, r->n->name);
pstext(r->pid+1, Buf);
} } }
if (run->pid == 0) return; /* it is the first process started */
@ -288,7 +311,7 @@ wrapup(int fini)
nproc - Have_claim + Skip_claim,
(xspin || nproc!=1)?"es":"");
short_cut:
if (xspin) alldone(0); /* avoid an abort from xspin */
if (s_trail || xspin) alldone(0); /* avoid an abort from xspin */
if (fini) alldone(1);
}
@ -332,6 +355,24 @@ silent_moves(Element *e)
return e;
}
static int
x_can_run(void) /* the currently selected process in X can run */
{
if (X->prov && !eval(X->prov))
{
if (0) printf("pid %d cannot run: not provided\n", X->pid);
return 0;
}
if (has_priority && !old_priority_rules)
{ Lextok *n = nn(ZN, CONST, ZN, ZN);
n->val = X->pid;
if (0) printf("pid %d %s run (priority)\n", X->pid, pc_highest(n)?"can":"cannot");
return pc_highest(n);
}
if (0) printf("pid %d can run\n", X->pid);
return 1;
}
static RunList *
pickproc(RunList *Y)
{ SeqList *z; Element *has_else;
@ -343,7 +384,25 @@ pickproc(RunList *Y)
return NULL;
}
if (!interactive || depth < jumpsteps)
{ /* was: j = (int) Rand()%(nproc-nstop); */
{ if (has_priority && !old_priority_rules) /* new 6.3.2 */
{ j = Rand()%(nproc-nstop);
for (X = run; X; X = X->nxt)
{ if (j-- <= 0)
break;
}
if (X == NULL)
{ fatal("unexpected, pickproc", (char *)0);
}
j = nproc - nstop;
while (j-- > 0)
{ if (x_can_run())
{ Y = X;
break;
}
X = (X->nxt)?X->nxt:run;
}
return Y;
}
if (Priority_Sum < nproc-nstop)
fatal("cannot happen - weights", (char *)0);
j = (int) Rand()%Priority_Sum;
@ -354,6 +413,7 @@ pickproc(RunList *Y)
X = X->nxt;
if (!X) { Y = NULL; X = run; }
}
} else
{ int only_choice = -1;
int no_choice = 0, proc_no_ch, proc_k;
@ -365,8 +425,7 @@ try_more: for (X = run, k = 1; X; X = X->nxt)
Choices[X->pid] = (short) k;
if (!X->pc
|| (X->prov && !eval(X->prov)))
if (!X->pc || !x_can_run())
{ if (X == run)
Choices[X->pid] = 0;
continue;
@ -457,9 +516,12 @@ try_more: for (X = run, k = 1; X; X = X->nxt)
} else
{ char buf[256];
fflush(stdout);
scanf("%s", buf);
if (scanf("%64s", buf) == 0)
{ printf("\tno input\n");
goto try_again;
}
j = -1;
if (isdigit(buf[0]))
if (isdigit((int) buf[0]))
j = atoi(buf);
else
{ if (buf[0] == 'q')
@ -483,6 +545,26 @@ try_more: for (X = run, k = 1; X; X = X->nxt)
return Y;
}
void
multi_claims(void)
{ ProcList *p, *q = NULL;
if (nclaims > 1)
{ printf(" the model contains %d never claims:", nclaims);
for (p = rdy; p; p = p->nxt)
{ if (p->b == N_CLAIM)
{ printf("%s%s", q?", ":" ", p->n->name);
q = p;
} }
printf("\n");
printf(" only one claim is used in a verification run\n");
printf(" choose which one with ./pan -a -N name (defaults to -N %s)\n",
q?q->n->name:"--");
printf(" or use e.g.: spin -search -ltl %s %s\n",
q?q->n->name:"--", Fname?Fname->name:"filename");
}
}
void
sched(void)
{ Element *e;
@ -498,19 +580,33 @@ sched(void)
dumplabels();
return;
}
if (has_code && !analyze)
{ printf("spin: warning: c_code fragments remain uninterpreted\n");
printf(" in random simulations with spin; use ./pan -r instead\n");
}
if (has_enabled && u_sync > 0)
{ printf("spin: error, cannot use 'enabled()' in ");
printf("models with synchronous channels.\n");
nr_errs++;
}
if (analyze)
if (product)
{ sync_product();
alldone(0);
}
if (analyze && (!replay || has_code))
{ gensrc();
multi_claims();
return;
} else if (s_trail)
}
if (replay && !has_code)
{ return;
}
if (s_trail)
{ match_trail();
return;
}
if (claimproc)
printf("warning: never claim not used in random simulation\n");
if (eventmap)
@ -543,9 +639,9 @@ sched(void)
depth++; LastStep = ZE;
oX = X; /* a rendezvous could change it */
go = 1;
if (X && X->prov && X->pc
if (X->pc
&& !(X->pc->status & D_ATOM)
&& !eval(X->prov))
&& !x_can_run())
{ if (!xspin && ((verbose&32) || (verbose&4)))
{ p_talk(X->pc, 1);
printf("\t<<Not Enabled>>\n");
@ -557,9 +653,10 @@ sched(void)
&& ((verbose&32) || (verbose&4)))
{ if (X == oX)
if (!(e->status & D_ATOM) || (verbose&32)) /* no talking in d_steps */
{ p_talk(X->pc, 1);
{ if (!LastStep) LastStep = X->pc;
/* A. Tanaka, changed order */
p_talk(LastStep, 1);
printf(" [");
if (!LastStep) LastStep = X->pc;
comment(stdout, LastStep->n, 0);
printf("]\n");
}
@ -570,7 +667,8 @@ sched(void)
if (xspin)
printf("\n");
}
if (oX != X)
if (oX != X
|| (X->pc->status & (ATOM|D_ATOM))) /* new 5.0 */
{ e = silent_moves(e);
notbeyond = 0;
}
@ -587,10 +685,12 @@ sched(void)
}
} else
{ depth--;
if (oX->pc->status & D_ATOM)
non_fatal("stmnt in d_step blocks", (char *)0);
if (X->pc->n->ntyp == '@'
if (oX->pc && (oX->pc->status & D_ATOM))
{ non_fatal("stmnt in d_step blocks", (char *)0);
}
if (X->pc
&& X->pc->n
&& X->pc->n->ntyp == '@'
&& X->pid == (nproc-nstop-1))
{ if (X != run && Y != NULL)
Y->nxt = X->nxt;
@ -610,14 +710,19 @@ sched(void)
X = (X->nxt) ? X->nxt : run;
} else
{ if (p_blocked(X->pid))
{ if (Tval) break;
Tval = 1;
if (depth >= jumpsteps)
{ if (Tval && !has_stdin)
{ break;
}
if (!Tval && depth >= jumpsteps)
{ oX = X;
X = (RunList *) 0; /* to suppress indent */
dotag(stdout, "timeout\n");
X = oX;
Tval = 1;
} } } }
if (!run || !X) break; /* new 5.0 */
Y = pickproc(X);
notbeyond = 0;
}
@ -662,7 +767,7 @@ complete_rendez(void)
printf(" [");
comment(stdout, s_was->n, 0);
printf("]\n");
tmp = orun; orun = X; X = tmp;
tmp = orun; /* orun = X; */ X = tmp;
if (!LastStep) LastStep = X->pc;
p_talk(LastStep, 1);
printf(" [");
@ -692,25 +797,33 @@ addsymbol(RunList *r, Symbol *s)
int i;
for (t = r->symtab; t; t = t->next)
if (strcmp(t->name, s->name) == 0)
if (strcmp(t->name, s->name) == 0
&& (old_scope_rules
|| strcmp((const char *)t->bscp, (const char *)s->bscp) == 0))
return; /* it's already there */
t = (Symbol *) emalloc(sizeof(Symbol));
t->name = s->name;
t->type = s->type;
t->hidden = s->hidden;
t->isarray = s->isarray;
t->nbits = s->nbits;
t->nel = s->nel;
t->ini = s->ini;
t->setat = depth;
t->context = r->n;
t->bscp = (unsigned char *) emalloc(strlen((const char *)s->bscp)+1);
strcpy((char *)t->bscp, (const char *)s->bscp);
if (s->type != STRUCT)
{ if (s->val) /* if already initialized, copy info */
{ t->val = (int *) emalloc(s->nel*sizeof(int));
for (i = 0; i < s->nel; i++)
t->val[i] = s->val[i];
} else
(void) checkvar(t, 0); /* initialize it */
{ (void) checkvar(t, 0); /* initialize it */
}
} else
{ if (s->Sval)
fatal("saw preinitialized struct %s", s->name);
@ -759,7 +872,7 @@ oneparam(RunList *r, Lextok *t, Lextok *a, ProcList *p)
if (!a)
fatal("missing actual parameters: '%s'", p->n->name);
if (t->sym->nel != 1)
if (t->sym->nel > 1 || t->sym->isarray)
fatal("array in parameter list, %s", t->sym->name);
k = eval(a->lft);
@ -768,7 +881,7 @@ oneparam(RunList *r, Lextok *t, Lextok *a, ProcList *p)
ft = Sym_typ(t);
if (at != ft && (at == CHAN || ft == CHAN))
{ char buf[128], tag1[64], tag2[64];
{ char buf[256], tag1[64], tag2[64];
(void) sputtype(tag1, ft);
(void) sputtype(tag2, at);
sprintf(buf, "type-clash in params of %s(..), (%s<-> %s)",
@ -809,8 +922,11 @@ findloc(Symbol *s)
return ZS;
}
for (r = X->symtab; r; r = r->next)
if (strcmp(r->name, s->name) == 0)
break;
{ if (strcmp(r->name, s->name) == 0
&& (old_scope_rules
|| strcmp((const char *)r->bscp, (const char *)s->bscp) == 0))
{ break;
} }
if (!r)
{ addsymbol(X, s);
r = X->symtab;
@ -878,7 +994,11 @@ whoruns(int lnr)
printf(" -");
else
printf("%2d", X->pid - Have_claim);
printf(" (%s) ", X->n->name);
if (old_priority_rules)
{ printf(" (%s) ", X->n->name);
} else
{ printf(" (%s:%d) ", X->n->name, X->priority);
}
}
static void
@ -895,6 +1015,7 @@ talk(RunList *r)
void
p_talk(Element *e, int lnr)
{ static int lastnever = -1;
static char nbuf[128];
int newnever = -1;
if (e && e->n)
@ -918,9 +1039,22 @@ p_talk(Element *e, int lnr)
whoruns(lnr);
if (e)
{ printf("line %3d %s (state %d)",
{ if (e->n)
{ char *ptr = e->n->fn->name;
char *qtr = nbuf;
while (*ptr != '\0')
{ if (*ptr != '"')
{ *qtr++ = *ptr;
}
ptr++;
}
*qtr = '\0';
} else
{ strcpy(nbuf, "-");
}
printf("%s:%d (state %d)",
nbuf,
e->n?e->n->ln:-1,
e->n?e->n->fn->name:"-",
e->seqno);
if (!xspin
&& ((e->status&ENDSTATE) || has_lab(e, 2))) /* 2=end */
@ -943,8 +1077,9 @@ remotelab(Lextok *n)
{ fatal("remote ref to label '%s' inside d_step",
n->sym->name);
}
if ((i = find_lab(n->sym, n->lft->sym, 1)) == 0)
fatal("unknown labelname: %s", n->sym->name);
if ((i = find_lab(n->sym, n->lft->sym, 1)) == 0) /* remotelab */
{ fatal("unknown labelname: %s", n->sym->name);
}
return i;
}
@ -970,7 +1105,8 @@ remotevar(Lextok *n)
} }
if (prno < 0)
return 0; /* non-existing process */
{ return 0; /* non-existing process */
}
#if 0
i = nproc - nstop;
for (Y = run; Y; Y = Y->nxt)
@ -978,7 +1114,7 @@ remotevar(Lextok *n)
printf(" %s: i=%d, prno=%d, ->pid=%d\n", Y->n->name, i, prno, Y->pid);
}
#endif
i = nproc - nstop;
i = nproc - nstop + Skip_claim; /* 6.0: added Skip_claim */
for (Y = run; Y; Y = Y->nxt)
if (--i == prno)
{ if (strcmp(Y->n->name, n->lft->sym->name) != 0)
@ -988,12 +1124,13 @@ remotevar(Lextok *n)
}
if (strcmp(n->sym->name, "_p") == 0)
{ if (Y->pc)
return Y->pc->seqno;
{ return Y->pc->seqno;
}
/* harmless, can only happen with -t */
return 0;
}
#if 1
/* new 4.0 allow remote variables */
/* check remote variables */
oX = X;
X = Y;
@ -1001,17 +1138,20 @@ remotevar(Lextok *n)
n->lft = n->rgt;
os = n->sym;
n->sym = findloc(n->sym);
if (!n->sym->context)
{ n->sym->context = Y->n;
}
{ int rs = old_scope_rules;
old_scope_rules = 1; /* 6.4.0 */
n->sym = findloc(n->sym);
old_scope_rules = rs;
}
i = getval(n);
n->sym = os;
n->lft = onl;
X = oX;
return i;
#else
break;
#endif
}
printf("remote ref: %s[%d] ", n->lft->sym->name, prno-added);
non_fatal("%s not found", n->sym->name);

91
sys/src/cmd/spin/spin.h
View File

@ -1,13 +1,10 @@
/***** spin: spin.h *****/
/* 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 */
/*
* 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
*/
#ifndef SEEN_SPIN_H
#define SEEN_SPIN_H
@ -15,6 +12,15 @@
#include <stdio.h>
#include <string.h>
#include <ctype.h>
#if !defined(WIN32) && !defined(WIN64)
#include <unistd.h>
#endif
#if !defined(PC) && !defined(_PLAN9)
#include <memory.h>
#endif
enum { INIV, PUTV, LOGV }; /* used in pangen1.c */
enum btypes { NONE, N_CLAIM, I_PROC, A_PROC, P_PROC, E_TRACE, N_TRACE };
typedef struct Lextok {
unsigned short ntyp; /* node type */
@ -22,6 +28,7 @@ typedef struct Lextok {
int val; /* value attribute */
int ln; /* line number */
int indstep; /* part of d_step sequence */
int uiid; /* inline id, if non-zero */
struct Symbol *fn; /* file name */
struct Symbol *sym; /* symbol reference */
struct Sequence *sq; /* sequence */
@ -54,6 +61,9 @@ typedef struct Symbol {
64=treat as if local; 128=read at least once
*/
unsigned char colnr; /* for use with xspin during simulation */
unsigned char isarray; /* set if decl specifies array bound */
unsigned char *bscp; /* block scope */
int sc; /* scope seq no -- set only for proctypes */
int nbits; /* optional width specifier */
int nel; /* 1 if scalar, >1 if array */
int setat; /* last depth value changed */
@ -124,7 +134,7 @@ typedef struct Element {
int merge_single;
short merge_in; /* nr of incoming edges */
short merge_mark; /* state was generated in merge sequence */
unsigned char status; /* used by analyzer generator */
unsigned int status; /* used by analyzer generator */
struct FSM_use *dead; /* optional dead variable list */
struct SeqList *sub; /* subsequences, for compounds */
struct SeqList *esc; /* zero or more escape sequences */
@ -136,6 +146,7 @@ typedef struct Sequence {
Element *frst;
Element *last; /* links onto continuations */
Element *extent; /* last element in original */
int minel; /* minimum Seqno, set and used only in guided.c */
int maxel; /* 1+largest id in sequence */
} Sequence;
@ -148,6 +159,7 @@ typedef struct Label {
Symbol *s;
Symbol *c;
Element *e;
int uiid; /* non-zero if label appears in an inline */
int visible; /* label referenced in claim (slice relevant) */
struct Label *nxt;
} Label;
@ -157,11 +169,17 @@ typedef struct Lbreak {
struct Lbreak *nxt;
} Lbreak;
typedef struct L_List {
Lextok *n;
struct L_List *nxt;
} L_List;
typedef struct RunList {
Symbol *n; /* name */
int tn; /* ordinal of type */
int pid; /* process id */
int priority; /* for simulations only */
enum btypes b; /* the type of process */
Element *pc; /* current stmnt */
Sequence *ps; /* used by analyzer generator */
Lextok *prov; /* provided clause */
@ -174,11 +192,19 @@ typedef struct ProcList {
Lextok *p; /* parameters */
Sequence *s; /* body */
Lextok *prov; /* provided clause */
enum btypes b; /* e.g., claim, trace, proc */
short tn; /* ordinal number */
short det; /* deterministic */
unsigned char det; /* deterministic */
unsigned char unsafe; /* contains global var inits */
unsigned char priority; /* process priority, if any */
struct ProcList *nxt; /* linked list */
} ProcList;
typedef struct QH {
int n;
struct QH *nxt;
} QH;
typedef Lextok *Lexptr;
#define YYSTYPE Lexptr
@ -194,7 +220,8 @@ typedef Lextok *Lexptr;
#define DONE2 16 /* used in putcode and main*/
#define D_ATOM 32 /* deterministic atomic */
#define ENDSTATE 64 /* normal endstate */
#define CHECK2 128
#define CHECK2 128 /* status bits for remote ref check */
#define CHECK3 256 /* status bits for atomic jump check */
#define Nhash 255 /* slots in symbol hash-table */
@ -216,18 +243,24 @@ typedef Lextok *Lexptr;
#define SOMETHINGBIG 65536
#define RATHERSMALL 512
#define MAXSCOPESZ 1024
#ifndef max
#define max(a,b) (((a)<(b)) ? (b) : (a))
#define max(a,b) (((a)<(b)) ? (b) : (a))
#endif
enum { INIV, PUTV, LOGV }; /* for pangen[14].c */
#ifdef PC
#define MFLAGS "wb"
#else
#define MFLAGS "w"
#endif
/***** prototype definitions *****/
Element *eval_sub(Element *);
Element *get_lab(Lextok *, int);
Element *huntele(Element *, int, int);
Element *huntele(Element *, unsigned int, int);
Element *huntstart(Element *);
Element *mk_skip(void);
Element *target(Element *);
Lextok *do_unless(Lextok *, Lextok *);
@ -238,8 +271,9 @@ Lextok *nn(Lextok *, int, Lextok *, Lextok *);
Lextok *rem_lab(Symbol *, Lextok *, Symbol *);
Lextok *rem_var(Symbol *, Lextok *, Symbol *, Lextok *);
Lextok *tail_add(Lextok *, Lextok *);
Lextok *return_statement(Lextok *);
ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *);
ProcList *ready(Symbol *, Lextok *, Sequence *, int, Lextok *, enum btypes);
SeqList *seqlist(Sequence *, SeqList *);
Sequence *close_seq(int);
@ -250,7 +284,8 @@ Symbol *has_lab(Element *, int);
Symbol *lookup(char *);
Symbol *prep_inline(Symbol *, Lextok *);
char *emalloc(int);
char *put_inline(FILE *, char *);
char *emalloc(size_t);
long Rand(void);
int any_oper(Lextok *, int);
@ -258,6 +293,7 @@ int any_undo(Lextok *);
int c_add_sv(FILE *);
int cast_val(int, int, int);
int checkvar(Symbol *, int);
int check_track(Lextok *);
int Cnt_flds(Lextok *);
int cnt_mpars(Lextok *);
int complete_rendez(void);
@ -274,12 +310,14 @@ int has_typ(Lextok *, int);
int in_bound(Symbol *, int);
int interprint(FILE *, Lextok *);
int printm(FILE *, Lextok *);
int is_inline(void);
int ismtype(char *);
int isproctype(char *);
int isutype(char *);
int Lval_struct(Lextok *, Symbol *, int, int);
int main(int, char **);
int pc_value(Lextok *);
int pid_is_claim(int);
int proper_enabler(Lextok *);
int putcode(FILE *, Sequence *, Element *, int, int, int);
int q_is_sync(Lextok *);
@ -298,7 +336,6 @@ int Sym_typ(Lextok *);
int tl_main(int, char *[]);
int Width_set(int *, int, Lextok *);
int yyparse(void);
int yywrap(void);
int yylex(void);
void AST_track(Lextok *, int);
@ -309,7 +346,6 @@ void c_state(Symbol *, Symbol *, Symbol *);
void c_add_def(FILE *);
void c_add_loc(FILE *, char *);
void c_add_locinit(FILE *, int, char *);
void c_add_use(FILE *);
void c_chandump(FILE *);
void c_preview(void);
void c_struct(FILE *, char *, Symbol *);
@ -321,6 +357,7 @@ void check_param_count(int, Lextok *);
void checkrun(Symbol *, int);
void comment(FILE *, Lextok *, int);
void cross_dsteps(Lextok *, Lextok *);
void disambiguate(void);
void doq(Symbol *, int, RunList *);
void dotag(FILE *, char *);
void do_locinits(FILE *);
@ -344,20 +381,22 @@ void genunio(void);
void ini_struct(Symbol *);
void loose_ends(void);
void make_atomic(Sequence *, int);
void mark_last(void);
void match_trail(void);
void no_side_effects(char *);
void nochan_manip(Lextok *, Lextok *, int);
void non_fatal(char *, char *);
void ntimes(FILE *, int, int, char *c[]);
void ntimes(FILE *, int, int, const char *c[]);
void open_seq(int);
void p_talk(Element *, int);
void pickup_inline(Symbol *, Lextok *);
void pickup_inline(Symbol *, Lextok *, Lextok *);
void plunk_c_decls(FILE *);
void plunk_c_fcts(FILE *);
void plunk_expr(FILE *, char *);
void plunk_inline(FILE *, char *, int);
void plunk_inline(FILE *, char *, int, int);
void prehint(Symbol *);
void preruse(FILE *, Lextok *);
void pretty_print(void);
void prune_opts(Lextok *);
void pstext(int, char *);
void pushbreak(void);
@ -383,17 +422,23 @@ void start_claim(int);
void struct_name(Lextok *, Symbol *, int, char *);
void symdump(void);
void symvar(Symbol *);
void sync_product(void);
void trackchanuse(Lextok *, Lextok *, int);
void trackvar(Lextok *, Lextok *);
void trackrun(Lextok *);
void trapwonly(Lextok *, char *); /* spin.y and main.c */
void trapwonly(Lextok * /* , char * */); /* spin.y and main.c */
void typ2c(Symbol *);
void typ_ck(int, int, char *);
void undostmnt(Lextok *, int);
void unrem_Seq(void);
void unskip(int);
void varcheck(Element *, Element *);
void whoruns(int);
void wrapup(int);
void yyerror(char *, ...);
extern int unlink(const char *);
#define TMP_FILE1 "._s_p_i_n_"
#define TMP_FILE2 "._n_i_p_s_"
#endif

615
sys/src/cmd/spin/spin.y
View File

@ -1,47 +1,69 @@
/***** spin: spin.y *****/
/* 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 */
/*
* 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 "spin.h"
#include <sys/types.h>
#ifndef PC
#include <unistd.h>
#endif
#include <stdarg.h>
#define YYDEBUG 0
#define YYMAXDEPTH 20000 /* default is 10000 */
#define YYDEBUG 0
#define Stop nn(ZN,'@',ZN,ZN)
#define PART0 "place initialized declaration of "
#define PART1 "place initialized chan decl of "
#define PART2 " at start of proctype "
static Lextok *ltl_to_string(Lextok *);
extern Symbol *context, *owner;
extern int u_sync, u_async, dumptab;
extern short has_sorted, has_random, has_enabled, has_pcvalue, has_np;
extern short has_code, has_state, has_io;
extern Lextok *for_body(Lextok *, int);
extern void for_setup(Lextok *, Lextok *, Lextok *);
extern Lextok *for_index(Lextok *, Lextok *);
extern Lextok *sel_index(Lextok *, Lextok *, Lextok *);
extern void keep_track_off(Lextok *);
extern void safe_break(void);
extern void restore_break(void);
extern int u_sync, u_async, dumptab, scope_level;
extern int initialization_ok;
extern short has_sorted, has_random, has_enabled, has_pcvalue, has_np, has_priority;
extern short has_code, has_state, has_ltl, has_io;
extern void count_runs(Lextok *);
extern void no_internals(Lextok *);
extern void any_runs(Lextok *);
extern void explain(int);
extern void ltl_list(char *, char *);
extern void validref(Lextok *, Lextok *);
extern void sanity_check(Lextok *);
extern char yytext[];
int Mpars = 0; /* max nr of message parameters */
int runsafe = 1; /* 1 if all run stmnts are in init */
int nclaims = 0; /* nr of never claims */
int ltl_mode = 0; /* set when parsing an ltl formula */
int Expand_Ok = 0, realread = 1, IArgs = 0, NamesNotAdded = 0;
int in_for = 0, in_seq = 0, par_cnt = 0;
int dont_simplify = 0;
char *claimproc = (char *) 0;
char *eventmap = (char *) 0;
static int Embedded = 0, inEventMap = 0, has_ini = 0;
static char *ltl_name;
static int Embedded = 0, inEventMap = 0, has_ini = 0;
%}
%token ASSERT PRINT PRINTM
%token ASSERT PRINT PRINTM PREPROC
%token C_CODE C_DECL C_EXPR C_STATE C_TRACK
%token RUN LEN ENABLED EVAL PC_VAL
%token TYPEDEF MTYPE INLINE LABEL OF
%token GOTO BREAK ELSE SEMI
%token IF FI DO OD SEP
%token RUN LEN ENABLED SET_P GET_P EVAL PC_VAL
%token TYPEDEF MTYPE INLINE RETURN LABEL OF
%token GOTO BREAK ELSE SEMI ARROW
%token IF FI DO OD FOR SELECT IN SEP DOTDOT
%token ATOMIC NON_ATOMIC D_STEP UNLESS
%token TIMEOUT NONPROGRESS
%token ACTIVE PROCTYPE D_PROCTYPE
@ -50,12 +72,16 @@ static int Embedded = 0, inEventMap = 0, has_ini = 0;
%token FULL EMPTY NFULL NEMPTY
%token CONST TYPE XU /* val */
%token NAME UNAME PNAME INAME /* sym */
%token STRING CLAIM TRACE INIT /* sym */
%token STRING CLAIM TRACE INIT LTL /* sym */
%right ASGN
%left SND O_SND RCV R_RCV /* SND doubles as boolean negation */
%left IMPLIES EQUIV /* ltl */
%left OR
%left AND
%left ALWAYS EVENTUALLY /* ltl */
%left UNTIL WEAK_UNTIL RELEASE /* ltl */
%right NEXT /* ltl */
%left '|'
%left '^'
%left '&'
@ -81,17 +107,25 @@ units : unit
unit : proc /* proctype { } */
| init /* init { } */
| claim /* never claim */
| ltl /* ltl formula */
| events /* event assertions */
| one_decl /* variables, chans */
| utype /* user defined types */
| c_fcts /* c functions etc. */
| ns /* named sequence */
| SEMI /* optional separator */
| semi /* optional separator */
| error
;
l_par : '(' { par_cnt++; }
;
r_par : ')' { par_cnt--; }
;
proc : inst /* optional instantiator */
proctype NAME {
proctype NAME {
setptype($3, PROCTYPE, ZN);
setpname($3);
context = $3->sym;
@ -99,20 +133,29 @@ proc : inst /* optional instantiator */
Expand_Ok++; /* expand struct names in decl */
has_ini = 0;
}
'(' decl ')' { Expand_Ok--;
l_par decl r_par { Expand_Ok--;
if (has_ini)
fatal("initializer in parameter list", (char *) 0);
}
Opt_priority
Opt_enabler
body { ProcList *rl;
rl = ready($3->sym, $6, $11->sq, $2->val, $10);
if ($1 != ZN && $1->val > 0)
{ int j;
rl = ready($3->sym, $6, $11->sq, $2->val, $10, A_PROC);
for (j = 0; j < $1->val; j++)
runnable(rl, $9?$9->val:1, 1);
{ runnable(rl, $9?$9->val:1, 1);
announce(":root:");
}
if (dumptab) $3->sym->ini = $1;
} else
{ rl = ready($3->sym, $6, $11->sq, $2->val, $10, P_PROC);
}
if (rl && has_ini == 1) /* global initializations, unsafe */
{ /* printf("proctype %s has initialized data\n",
$3->sym->name);
*/
rl->unsafe = 1;
}
context = ZS;
}
@ -124,7 +167,7 @@ proctype: PROCTYPE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 0; }
inst : /* empty */ { $$ = ZN; }
| ACTIVE { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
| ACTIVE '[' CONST ']' {
| ACTIVE '[' const_expr ']' {
$$ = nn(ZN,CONST,ZN,ZN); $$->val = $3->val;
if ($3->val > 255)
non_fatal("max nr of processes is 255\n", "");
@ -133,10 +176,10 @@ inst : /* empty */ { $$ = ZN; }
$$ = nn(ZN,CONST,ZN,ZN);
$$->val = 0;
if (!$3->sym->type)
non_fatal("undeclared variable %s",
fatal("undeclared variable %s",
$3->sym->name);
else if ($3->sym->ini->ntyp != CONST)
non_fatal("need constant initializer for %s\n",
fatal("need constant initializer for %s\n",
$3->sym->name);
else
$$->val = $3->sym->ini->val;
@ -146,41 +189,84 @@ inst : /* empty */ { $$ = ZN; }
init : INIT { context = $1->sym; }
Opt_priority
body { ProcList *rl;
rl = ready(context, ZN, $4->sq, 0, ZN);
rl = ready(context, ZN, $4->sq, 0, ZN, I_PROC);
runnable(rl, $3?$3->val:1, 1);
announce(":root:");
context = ZS;
}
;
claim : CLAIM { context = $1->sym;
if (claimproc)
non_fatal("claim %s redefined", claimproc);
ltl : LTL optname2 { ltl_mode = 1; ltl_name = $2->sym->name; }
ltl_body { if ($4) ltl_list($2->sym->name, $4->sym->name);
ltl_mode = 0; has_ltl = 1;
}
;
ltl_body: '{' full_expr OS '}' { $$ = ltl_to_string($2); }
| error { $$ = NULL; }
;
claim : CLAIM optname { if ($2 != ZN)
{ $1->sym = $2->sym; /* new 5.3.0 */
}
nclaims++;
context = $1->sym;
if (claimproc && !strcmp(claimproc, $1->sym->name))
{ fatal("claim %s redefined", claimproc);
}
claimproc = $1->sym->name;
}
body { (void) ready($1->sym, ZN, $3->sq, 0, ZN);
body { (void) ready($1->sym, ZN, $4->sq, 0, ZN, N_CLAIM);
context = ZS;
}
;
optname : /* empty */ { char tb[32];
memset(tb, 0, 32);
sprintf(tb, "never_%d", nclaims);
$$ = nn(ZN, NAME, ZN, ZN);
$$->sym = lookup(tb);
}
| NAME { $$ = $1; }
;
optname2 : /* empty */ { char tb[32]; static int nltl = 0;
memset(tb, 0, 32);
sprintf(tb, "ltl_%d", nltl++);
$$ = nn(ZN, NAME, ZN, ZN);
$$->sym = lookup(tb);
}
| NAME { $$ = $1; }
;
events : TRACE { context = $1->sym;
if (eventmap)
non_fatal("trace %s redefined", eventmap);
eventmap = $1->sym->name;
inEventMap++;
}
body { (void) ready($1->sym, ZN, $3->sq, 0, ZN);
body {
if (strcmp($1->sym->name, ":trace:") == 0)
{ (void) ready($1->sym, ZN, $3->sq, 0, ZN, E_TRACE);
} else
{ (void) ready($1->sym, ZN, $3->sq, 0, ZN, N_TRACE);
}
context = ZS;
inEventMap--;
}
;
utype : TYPEDEF NAME { if (context)
fatal("typedef %s must be global",
$2->sym->name);
utype : TYPEDEF NAME '{' { if (context)
{ fatal("typedef %s must be global",
$2->sym->name);
}
owner = $2->sym;
in_seq = $1->ln;
}
decl_lst '}' { setuname($5);
owner = ZS;
in_seq = 0;
}
'{' decl_lst '}' { setuname($5); owner = ZS; }
;
nm : NAME { $$ = $1; }
@ -190,8 +276,8 @@ nm : NAME { $$ = $1; }
}
;
ns : INLINE nm '(' { NamesNotAdded++; }
args ')' { prep_inline($2->sym, $5);
ns : INLINE nm l_par { NamesNotAdded++; }
args r_par { prep_inline($2->sym, $5);
NamesNotAdded--;
}
;
@ -227,6 +313,8 @@ ccode : C_CODE { Symbol *s;
NamesNotAdded--;
$$ = nn(ZN, C_CODE, ZN, ZN);
$$->sym = s;
$$->ln = $1->ln;
$$->fn = $1->fn;
has_code = 1;
}
| C_DECL { Symbol *s;
@ -236,23 +324,37 @@ ccode : C_CODE { Symbol *s;
s->type = CODE_DECL;
$$ = nn(ZN, C_CODE, ZN, ZN);
$$->sym = s;
$$->ln = $1->ln;
$$->fn = $1->fn;
has_code = 1;
}
;
cexpr : C_EXPR { Symbol *s;
NamesNotAdded++;
s = prep_inline(ZS, ZN);
/* if context is 0 this was inside an ltl formula
mark the last inline added to seqnames */
if (!context)
{ mark_last();
}
NamesNotAdded--;
$$ = nn(ZN, C_EXPR, ZN, ZN);
$$->sym = s;
$$->ln = $1->ln;
$$->fn = $1->fn;
no_side_effects(s->name);
has_code = 1;
}
;
body : '{' { open_seq(1); }
body : '{' { open_seq(1); in_seq = $1->ln; }
sequence OS { add_seq(Stop); }
'}' { $$->sq = close_seq(0); }
'}' { $$->sq = close_seq(0); in_seq = 0;
if (scope_level != 0)
{ non_fatal("missing '}' ?", 0);
scope_level = 0;
}
}
;
sequence: step { if ($1) add_seq($1); }
@ -264,7 +366,11 @@ step : one_decl { $$ = ZN; }
| NAME ':' one_decl { fatal("label preceding declaration,", (char *)0); }
| NAME ':' XU { fatal("label predecing xr/xs claim,", 0); }
| stmnt { $$ = $1; }
| stmnt UNLESS stmnt { $$ = do_unless($1, $3); }
| stmnt UNLESS { if ($1->ntyp == DO) { safe_break(); } }
stmnt { if ($1->ntyp == DO) { restore_break(); }
$$ = do_unless($1, $4);
}
| error { printf("Not a Step\n"); }
;
vis : /* empty */ { $$ = ZN; }
@ -277,7 +383,9 @@ asgn: /* empty */
| ASGN
;
one_decl: vis TYPE var_list { setptype($3, $2->val, $1); $$ = $3; }
one_decl: vis TYPE var_list { setptype($3, $2->val, $1);
$$ = $3;
}
| vis UNAME var_list { setutype($3, $2->sym, $1);
$$ = expand($3, Expand_Ok);
}
@ -310,26 +418,76 @@ var_list: ivar { $$ = nn($1, TYPE, ZN, ZN); }
| ivar ',' var_list { $$ = nn($1, TYPE, ZN, $3); }
;
c_list : CONST { $1->ntyp = CONST; $$ = $1; }
| CONST ',' c_list { $1->ntyp = CONST; $$ = nn($1, ',', $1, $3); }
;
ivar : vardcl { $$ = $1;
$1->sym->ini = nn(ZN,CONST,ZN,ZN);
$1->sym->ini->val = 0;
if (!initialization_ok)
{ Lextok *zx, *xz;
zx = nn(ZN, NAME, ZN, ZN);
zx->sym = $1->sym;
xz = nn(zx, ASGN, zx, $1->sym->ini);
keep_track_off(xz);
/* make sure zx doesnt turn out to be a STRUCT later */
add_seq(xz);
}
}
| vardcl ASGN expr { $1->sym->ini = $3; $$ = $1;
trackvar($1,$3); has_ini = 1;
| vardcl ASGN '{' c_list '}' {
if (!$1->sym->isarray)
fatal("%s must be an array", $1->sym->name);
$$ = $1;
$1->sym->ini = $4;
has_ini = 1;
$1->sym->hidden |= (4|8); /* conservative */
if (!initialization_ok)
{ Lextok *zx = nn(ZN, NAME, ZN, ZN);
zx->sym = $1->sym;
add_seq(nn(zx, ASGN, zx, $4));
}
}
| vardcl ASGN expr { $$ = $1;
$1->sym->ini = $3;
if ($3->ntyp == CONST
|| ($3->ntyp == NAME && $3->sym->context))
{ has_ini = 2; /* local init */
} else
{ has_ini = 1; /* possibly global */
}
trackvar($1, $3);
if (any_oper($3, RUN))
{ fatal("cannot use 'run' in var init, saw", (char *) 0);
}
nochan_manip($1, $3, 0);
no_internals($1);
if (!initialization_ok)
{ Lextok *zx = nn(ZN, NAME, ZN, ZN);
zx->sym = $1->sym;
add_seq(nn(zx, ASGN, zx, $3));
}
}
| vardcl ASGN ch_init { $1->sym->ini = $3;
$$ = $1; has_ini = 1;
if (!initialization_ok)
{ non_fatal(PART1 "'%s'" PART2, $1->sym->name);
}
}
;
ch_init : '[' CONST ']' OF
'{' typ_list '}' { if ($2->val) u_async++;
else u_sync++;
ch_init : '[' const_expr ']' OF
'{' typ_list '}' { if ($2->val)
u_async++;
else
u_sync++;
{ int i = cnt_mpars($6);
Mpars = max(Mpars, i);
}
$$ = nn(ZN, CHAN, ZN, $6);
$$->val = $2->val;
$$->ln = $1->ln;
$$->fn = $1->fn;
}
;
@ -342,13 +500,33 @@ vardcl : NAME { $1->sym->nel = 1; $$ = $1; }
}
$1->sym->nel = 1; $$ = $1;
}
| NAME '[' CONST ']' { $1->sym->nel = $3->val; $$ = $1; }
| NAME '[' const_expr ']' { $1->sym->nel = $3->val; $1->sym->isarray = 1; $$ = $1; }
| NAME '[' NAME ']' { /* make an exception for an initialized scalars */
$$ = nn(ZN, CONST, ZN, ZN);
fprintf(stderr, "spin: %s:%d, warning: '%s' in array bound ",
$1->fn->name, $1->ln, $3->sym->name);
if ($3->sym->ini->val > 0)
{ fprintf(stderr, "evaluated as %d\n", $3->sym->ini->val);
$$->val = $3->sym->ini->val;
} else
{ fprintf(stderr, "evaluated as 8 by default (to avoid zero)\n");
$$->val = 8;
}
$1->sym->nel = $$->val;
$1->sym->isarray = 1;
$$ = $1;
}
;
varref : cmpnd { $$ = mk_explicit($1, Expand_Ok, NAME); }
;
pfld : NAME { $$ = nn($1, NAME, ZN, ZN); }
pfld : NAME { $$ = nn($1, NAME, ZN, ZN);
if ($1->sym->isarray && !in_for)
{ non_fatal("missing array index for '%s'",
$1->sym->name);
}
}
| NAME { owner = ZS; }
'[' expr ']' { $$ = nn($1, NAME, $4, ZN); }
;
@ -363,7 +541,7 @@ cmpnd : pfld { Embedded++;
Embedded--;
if (!Embedded && !NamesNotAdded
&& !$1->sym->type)
non_fatal("undeclared variable: %s",
fatal("undeclared variable: %s",
$1->sym->name);
if ($3) validref($1, $3->lft);
owner = ZS;
@ -374,13 +552,21 @@ sfld : /* empty */ { $$ = ZN; }
| '.' cmpnd %prec DOT { $$ = nn(ZN, '.', $2, ZN); }
;
stmnt : Special { $$ = $1; }
| Stmnt { $$ = $1;
if (inEventMap)
non_fatal("not an event", (char *)0);
stmnt : Special { $$ = $1; initialization_ok = 0; }
| Stmnt { $$ = $1; initialization_ok = 0;
if (inEventMap) non_fatal("not an event", (char *)0);
}
;
for_pre : FOR l_par { in_for = 1; }
varref { trapwonly($4 /*, "for" */);
pushbreak(); /* moved up */
$$ = $4;
}
;
for_post: '{' sequence OS '}' ;
Special : varref RCV { Expand_Ok++; }
rargs { Expand_Ok--; has_io++;
$$ = nn($1, 'r', $1, $4);
@ -392,13 +578,30 @@ Special : varref RCV { Expand_Ok++; }
$$->val=0; trackchanuse($4, ZN, 'S');
any_runs($4);
}
| for_pre ':' expr DOTDOT expr r_par {
for_setup($1, $3, $5); in_for = 0;
}
for_post { $$ = for_body($1, 1);
}
| for_pre IN varref r_par { $$ = for_index($1, $3); in_for = 0;
}
for_post { $$ = for_body($5, 1);
}
| SELECT l_par varref ':' expr DOTDOT expr r_par {
trapwonly($3 /*, "select" */);
$$ = sel_index($3, $5, $7);
}
| IF options FI { $$ = nn($1, IF, ZN, ZN);
$$->sl = $2->sl;
$$->ln = $1->ln;
$$->fn = $1->fn;
prune_opts($$);
}
| DO { pushbreak(); }
options OD { $$ = nn($1, DO, ZN, ZN);
$$->sl = $3->sl;
$$->ln = $1->ln;
$$->fn = $1->fn;
prune_opts($$);
}
| BREAK { $$ = nn(ZN, GOTO, ZN, ZN);
@ -420,9 +623,22 @@ Special : varref RCV { Expand_Ok++; }
}
$1->sym->type = LABEL;
}
| NAME ':' { $$ = nn($1, ':',ZN,ZN);
if ($1->sym->type != 0
&& $1->sym->type != LABEL) {
non_fatal("bad label-name %s",
$1->sym->name);
}
$$->lft = nn(ZN, 'c', nn(ZN,CONST,ZN,ZN), ZN);
$$->lft->lft->val = 1; /* skip */
$1->sym->type = LABEL;
}
| error { $$ = nn(ZN, 'c', nn(ZN,CONST,ZN,ZN), ZN);
$$->lft->val = 1; /* skip */
}
;
Stmnt : varref ASGN expr { $$ = nn($1, ASGN, $1, $3);
Stmnt : varref ASGN full_expr { $$ = nn($1, ASGN, $1, $3);
trackvar($1, $3);
nochan_manip($1, $3, 0);
no_internals($1);
@ -443,10 +659,11 @@ Stmnt : varref ASGN expr { $$ = nn($1, ASGN, $1, $3);
if ($1->sym->type == CHAN)
fatal("arithmetic on chan id's", (char *)0);
}
| PRINT '(' STRING { realread = 0; }
prargs ')' { $$ = nn($3, PRINT, $5, ZN); realread = 1; }
| PRINTM '(' varref ')' { $$ = nn(ZN, PRINTM, $3, ZN); }
| PRINTM '(' CONST ')' { $$ = nn(ZN, PRINTM, $3, ZN); }
| SET_P l_par two_args r_par { $$ = nn(ZN, SET_P, $3, ZN); has_priority++; }
| PRINT l_par STRING { realread = 0; }
prargs r_par { $$ = nn($3, PRINT, $5, ZN); realread = 1; }
| PRINTM l_par varref r_par { $$ = nn(ZN, PRINTM, $3, ZN); }
| PRINTM l_par CONST r_par { $$ = nn(ZN, PRINTM, $3, ZN); }
| ASSERT full_expr { $$ = nn(ZN, ASSERT, $2, ZN); AST_track($2, 0); }
| ccode { $$ = $1; }
| varref R_RCV { Expand_Ok++; }
@ -480,21 +697,40 @@ Stmnt : varref ASGN expr { $$ = nn($1, ASGN, $1, $3);
| ATOMIC '{' { open_seq(0); }
sequence OS '}' { $$ = nn($1, ATOMIC, ZN, ZN);
$$->sl = seqlist(close_seq(3), 0);
make_atomic($$->sl->this, 0);
$$->ln = $1->ln;
$$->fn = $1->fn;
make_atomic($$->sl->this, 0);
}
| D_STEP '{' { open_seq(0); rem_Seq(); }
| D_STEP '{' { open_seq(0);
rem_Seq();
}
sequence OS '}' { $$ = nn($1, D_STEP, ZN, ZN);
$$->sl = seqlist(close_seq(4), 0);
$$->ln = $1->ln;
$$->fn = $1->fn;
make_atomic($$->sl->this, D_ATOM);
unrem_Seq();
}
| '{' { open_seq(0); }
sequence OS '}' { $$ = nn(ZN, NON_ATOMIC, ZN, ZN);
$$->sl = seqlist(close_seq(5), 0);
$$->ln = $1->ln;
$$->fn = $1->fn;
}
| INAME { IArgs++; }
'(' args ')' { pickup_inline($1->sym, $4); IArgs--; }
l_par args r_par { initialization_ok = 0;
pickup_inline($1->sym, $4, ZN);
IArgs--;
}
Stmnt { $$ = $7; }
| varref ASGN INAME { IArgs++; }
l_par args r_par { initialization_ok = 0;
pickup_inline($3->sym, $6, $1);
IArgs--;
}
Stmnt { $$ = $9; }
| RETURN full_expr { $$ = return_statement($2); }
;
options : option { $$->sl = seqlist($1->sq, 0); }
@ -503,22 +739,39 @@ options : option { $$->sl = seqlist($1->sq, 0); }
option : SEP { open_seq(0); }
sequence OS { $$ = nn(ZN,0,ZN,ZN);
$$->sq = close_seq(6); }
$$->sq = close_seq(6);
$$->ln = $1->ln;
$$->fn = $1->fn;
}
;
OS : /* empty */
| SEMI { /* redundant semi at end of sequence */ }
| semi { /* redundant semi at end of sequence */ }
;
MS : SEMI { /* at least one semi-colon */ }
| MS SEMI { /* but more are okay too */ }
semi : SEMI
| ARROW
;
MS : semi { /* at least one semi-colon */ }
| MS semi { /* but more are okay too */ }
;
aname : NAME { $$ = $1; }
| PNAME { $$ = $1; }
;
expr : '(' expr ')' { $$ = $2; }
const_expr: CONST { $$ = $1; }
| '-' const_expr %prec UMIN { $$ = $2; $$->val = -($2->val); }
| l_par const_expr r_par { $$ = $2; }
| const_expr '+' const_expr { $$ = $1; $$->val = $1->val + $3->val; }
| const_expr '-' const_expr { $$ = $1; $$->val = $1->val - $3->val; }
| const_expr '*' const_expr { $$ = $1; $$->val = $1->val * $3->val; }
| const_expr '/' const_expr { $$ = $1; $$->val = $1->val / $3->val; }
| const_expr '%' const_expr { $$ = $1; $$->val = $1->val % $3->val; }
;
expr : l_par expr r_par { $$ = $2; }
| expr '+' expr { $$ = nn(ZN, '+', $1, $3); }
| expr '-' expr { $$ = nn(ZN, '-', $1, $3); }
| expr '*' expr { $$ = nn(ZN, '*', $1, $3); }
@ -541,28 +794,25 @@ expr : '(' expr ')' { $$ = $2; }
| '-' expr %prec UMIN { $$ = nn(ZN, UMIN, $2, ZN); }
| SND expr %prec NEG { $$ = nn(ZN, '!', $2, ZN); }
| '(' expr SEMI expr ':' expr ')' {
| l_par expr ARROW expr ':' expr r_par {
$$ = nn(ZN, OR, $4, $6);
$$ = nn(ZN, '?', $2, $$);
}
| RUN aname { Expand_Ok++;
if (!context)
fatal("used 'run' outside proctype",
fatal("used 'run' outside proctype",
(char *) 0);
if (strcmp(context->name, ":init:") != 0)
runsafe = 0;
}
'(' args ')'
l_par args r_par
Opt_priority { Expand_Ok--;
$$ = nn($2, RUN, $5, ZN);
$$->val = ($7) ? $7->val : 1;
$$->val = ($7) ? $7->val : 0;
trackchanuse($5, $2, 'A'); trackrun($$);
}
| LEN '(' varref ')' { $$ = nn($3, LEN, $3, ZN); }
| ENABLED '(' expr ')' { $$ = nn(ZN, ENABLED, $3, ZN);
has_enabled++;
}
| LEN l_par varref r_par { $$ = nn($3, LEN, $3, ZN); }
| ENABLED l_par expr r_par { $$ = nn(ZN, ENABLED, $3, ZN); has_enabled++; }
| GET_P l_par expr r_par { $$ = nn(ZN, GET_P, $3, ZN); has_priority++; }
| varref RCV { Expand_Ok++; }
'[' rargs ']' { Expand_Ok--; has_io++;
$$ = nn($1, 'R', $1, $5);
@ -572,7 +822,7 @@ expr : '(' expr ')' { $$ = $2; }
$$ = nn($1, 'R', $1, $5);
$$->val = has_random = 1;
}
| varref { $$ = $1; trapwonly($1, "varref"); }
| varref { $$ = $1; trapwonly($1 /*, "varref" */); }
| cexpr { $$ = $1; }
| CONST { $$ = nn(ZN,CONST,ZN,ZN);
$$->ismtyp = $1->ismtyp;
@ -582,7 +832,7 @@ expr : '(' expr ')' { $$ = $2; }
| NONPROGRESS { $$ = nn(ZN,NONPROGRESS, ZN, ZN);
has_np++;
}
| PC_VAL '(' expr ')' { $$ = nn(ZN, PC_VAL, $3, ZN);
| PC_VAL l_par expr r_par { $$ = nn(ZN, PC_VAL, $3, ZN);
has_pcvalue++;
}
| PNAME '[' expr ']' '@' NAME
@ -591,18 +841,51 @@ expr : '(' expr ')' { $$ = $2; }
{ $$ = rem_var($1->sym, $3, $6->sym, $6->lft); }
| PNAME '@' NAME { $$ = rem_lab($1->sym, ZN, $3->sym); }
| PNAME ':' pfld { $$ = rem_var($1->sym, ZN, $3->sym, $3->lft); }
| ltl_expr { $$ = $1; /* sanity_check($1); */ }
;
Opt_priority: /* none */ { $$ = ZN; }
| PRIORITY CONST { $$ = $2; }
| PRIORITY CONST { $$ = $2; has_priority++; }
;
full_expr: expr { $$ = $1; }
| Expr { $$ = $1; }
| Expr { $$ = $1; }
;
ltl_expr: expr UNTIL expr { $$ = nn(ZN, UNTIL, $1, $3); }
| expr RELEASE expr { $$ = nn(ZN, RELEASE, $1, $3); }
| expr WEAK_UNTIL expr { $$ = nn(ZN, ALWAYS, $1, ZN);
$$ = nn(ZN, OR, $$, nn(ZN, UNTIL, $1, $3));
}
| expr IMPLIES expr {
$$ = nn(ZN, '!', $1, ZN);
$$ = nn(ZN, OR, $$, $3);
}
| expr EQUIV expr { $$ = nn(ZN, EQUIV, $1, $3); }
| NEXT expr %prec NEG { $$ = nn(ZN, NEXT, $2, ZN); }
| ALWAYS expr %prec NEG { $$ = nn(ZN, ALWAYS,$2, ZN); }
| EVENTUALLY expr %prec NEG { $$ = nn(ZN, EVENTUALLY, $2, ZN); }
;
/* an Expr cannot be negated - to protect Probe expressions */
Expr : Probe { $$ = $1; }
| l_par Expr r_par { $$ = $2; }
| Expr AND Expr { $$ = nn(ZN, AND, $1, $3); }
| Expr AND expr { $$ = nn(ZN, AND, $1, $3); }
| expr AND Expr { $$ = nn(ZN, AND, $1, $3); }
| Expr OR Expr { $$ = nn(ZN, OR, $1, $3); }
| Expr OR expr { $$ = nn(ZN, OR, $1, $3); }
| expr OR Expr { $$ = nn(ZN, OR, $1, $3); }
;
Probe : FULL l_par varref r_par { $$ = nn($3, FULL, $3, ZN); }
| NFULL l_par varref r_par { $$ = nn($3, NFULL, $3, ZN); }
| EMPTY l_par varref r_par { $$ = nn($3, EMPTY, $3, ZN); }
| NEMPTY l_par varref r_par { $$ = nn($3,NEMPTY, $3, ZN); }
;
Opt_enabler: /* none */ { $$ = ZN; }
| PROVIDED '(' full_expr ')' { if (!proper_enabler($3))
| PROVIDED l_par full_expr r_par { if (!proper_enabler($3))
{ non_fatal("invalid PROVIDED clause",
(char *)0);
$$ = ZN;
@ -615,23 +898,6 @@ Opt_enabler: /* none */ { $$ = ZN; }
}
;
/* an Expr cannot be negated - to protect Probe expressions */
Expr : Probe { $$ = $1; }
| '(' Expr ')' { $$ = $2; }
| Expr AND Expr { $$ = nn(ZN, AND, $1, $3); }
| Expr AND expr { $$ = nn(ZN, AND, $1, $3); }
| Expr OR Expr { $$ = nn(ZN, OR, $1, $3); }
| Expr OR expr { $$ = nn(ZN, OR, $1, $3); }
| expr AND Expr { $$ = nn(ZN, AND, $1, $3); }
| expr OR Expr { $$ = nn(ZN, OR, $1, $3); }
;
Probe : FULL '(' varref ')' { $$ = nn($3, FULL, $3, ZN); }
| NFULL '(' varref ')' { $$ = nn($3, NFULL, $3, ZN); }
| EMPTY '(' varref ')' { $$ = nn($3, EMPTY, $3, ZN); }
| NEMPTY '(' varref ')' { $$ = nn($3,NEMPTY, $3, ZN); }
;
basetype: TYPE { $$->sym = ZS;
$$->val = $1->val;
if ($$->val == UNSIGNED)
@ -647,6 +913,9 @@ typ_list: basetype { $$ = nn($1, $1->val, ZN, ZN); }
| basetype ',' typ_list { $$ = nn($1, $1->val, ZN, $3); }
;
two_args: expr ',' expr { $$ = nn(ZN, ',', $1, $3); }
;
args : /* empty */ { $$ = ZN; }
| arg { $$ = $1; }
;
@ -656,7 +925,7 @@ prargs : /* empty */ { $$ = ZN; }
;
margs : arg { $$ = $1; }
| expr '(' arg ')' { if ($1->ntyp == ',')
| expr l_par arg r_par { if ($1->ntyp == ',')
$$ = tail_add($1, $3);
else
$$ = nn(ZN, ',', $1, $3);
@ -676,9 +945,9 @@ arg : expr { if ($1->ntyp == ',')
;
rarg : varref { $$ = $1; trackvar($1, $1);
trapwonly($1, "rarg"); }
| EVAL '(' expr ')' { $$ = nn(ZN,EVAL,$3,ZN);
trapwonly($1, "eval rarg"); }
trapwonly($1 /*, "rarg" */); }
| EVAL l_par expr r_par { $$ = nn(ZN,EVAL,$3,ZN);
trapwonly($1 /*, "eval rarg" */); }
| CONST { $$ = nn(ZN,CONST,ZN,ZN);
$$->ismtyp = $1->ismtyp;
$$->val = $1->val;
@ -698,12 +967,12 @@ rargs : rarg { if ($1->ntyp == ',')
else
$$ = nn(ZN, ',', $1, $3);
}
| rarg '(' rargs ')' { if ($1->ntyp == ',')
| rarg l_par rargs r_par { if ($1->ntyp == ',')
$$ = tail_add($1, $3);
else
$$ = nn(ZN, ',', $1, $3);
}
| '(' rargs ')' { $$ = $2; }
| l_par rargs r_par { $$ = $2; }
;
nlst : NAME { $$ = nn($1, NAME, ZN, ZN);
@ -715,6 +984,138 @@ nlst : NAME { $$ = nn($1, NAME, ZN, ZN);
;
%%
#define binop(n, sop) fprintf(fd, "("); recursive(fd, n->lft); \
fprintf(fd, ") %s (", sop); recursive(fd, n->rgt); \
fprintf(fd, ")");
#define unop(n, sop) fprintf(fd, "%s (", sop); recursive(fd, n->lft); \
fprintf(fd, ")");
static void
recursive(FILE *fd, Lextok *n)
{
if (n)
switch (n->ntyp) {
case NEXT:
unop(n, "X");
break;
case ALWAYS:
unop(n, "[]");
break;
case EVENTUALLY:
unop(n, "<>");
break;
case '!':
unop(n, "!");
break;
case UNTIL:
binop(n, "U");
break;
case WEAK_UNTIL:
binop(n, "W");
break;
case RELEASE: /* see http://en.wikipedia.org/wiki/Linear_temporal_logic */
binop(n, "V");
break;
case OR:
binop(n, "||");
break;
case AND:
binop(n, "&&");
break;
case IMPLIES:
binop(n, "->");
break;
case EQUIV:
binop(n, "<->");
break;
case C_EXPR:
fprintf(fd, "c_expr { %s }", put_inline(fd, n->sym->name));
break;
default:
comment(fd, n, 0);
break;
}
}
static Lextok *
ltl_to_string(Lextok *n)
{ Lextok *m = nn(ZN, 0, ZN, ZN);
char *retval;
char ltl_formula[2048];
FILE *tf = fopen(TMP_FILE1, "w+"); /* tmpfile() fails on Windows 7 */
/* convert the parsed ltl to a string
by writing into a file, using existing functions,
and then passing it to the existing interface for
conversion into a never claim
(this means parsing everything twice, which is
a little redundant, but adds only miniscule overhead)
*/
if (!tf)
{ fatal("cannot create temporary file", (char *) 0);
}
dont_simplify = 1;
recursive(tf, n);
dont_simplify = 0;
(void) fseek(tf, 0L, SEEK_SET);
memset(ltl_formula, 0, sizeof(ltl_formula));
retval = fgets(ltl_formula, sizeof(ltl_formula), tf);
fclose(tf);
(void) unlink(TMP_FILE1);
if (!retval)
{ printf("%p\n", retval);
fatal("could not translate ltl ltl_formula", 0);
}
if (1) printf("ltl %s: %s\n", ltl_name, ltl_formula);
m->sym = lookup(ltl_formula);
return m;
}
int
is_temporal(int t)
{
return (t == EVENTUALLY || t == ALWAYS || t == UNTIL
|| t == WEAK_UNTIL || t == RELEASE);
}
int
is_boolean(int t)
{
return (t == AND || t == OR || t == IMPLIES || t == EQUIV);
}
#if 0
/* flags correct formula like: ltl { true U (true U true) } */
void
sanity_check(Lextok *t) /* check proper embedding of ltl_expr */
{
if (!t) return;
sanity_check(t->lft);
sanity_check(t->rgt);
if (t->lft && t->rgt)
{ if (!is_boolean(t->ntyp)
&& (is_temporal(t->lft->ntyp)
|| is_temporal(t->rgt->ntyp)))
{ printf("spin: attempt to apply '");
explain(t->ntyp);
printf("' to '");
explain(t->lft->ntyp);
printf("' and '");
explain(t->rgt->ntyp);
printf("'\n");
/* non_fatal("missing parentheses?", (char *)0); */
} }
}
#endif
void
yyerror(char *fmt, ...)
{

908
sys/src/cmd/spin/spinlex.c
View File

File diff suppressed because it is too large Load Diff

76
sys/src/cmd/spin/structs.c
View File

@ -1,13 +1,10 @@
/***** spin: structs.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 */
/*
* 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 "spin.h"
#include "y.tab.h"
@ -19,7 +16,7 @@ typedef struct UType {
} UType;
extern Symbol *Fname;
extern int lineno, depth, Expand_Ok;
extern int lineno, depth, Expand_Ok, has_hidden, in_for;
Symbol *owner;
@ -33,14 +30,16 @@ void
setuname(Lextok *n)
{ UType *tmp;
if (!owner)
fatal("illegal reference inside typedef", (char *) 0);
for (tmp = Unames; tmp; tmp = tmp->nxt)
if (!strcmp(owner->name, tmp->nm->name))
{ non_fatal("typename %s was defined before",
tmp->nm->name);
return;
}
if (!owner) fatal("illegal reference inside typedef",
(char *) 0);
tmp = (UType *) emalloc(sizeof(UType));
tmp->nm = owner;
tmp->cn = n;
@ -102,21 +101,22 @@ setutype(Lextok *p, Symbol *t, Lextok *vis) /* user-defined types */
{ lineno = n->ln;
Fname = n->fn;
if (n->sym->type)
non_fatal("redeclaration of '%s'", n->sym->name);
fatal("redeclaration of '%s'", n->sym->name);
if (n->sym->nbits > 0)
non_fatal("(%s) only an unsigned can have width-field",
n->sym->name);
non_fatal("(%s) only an unsigned can have width-field",
n->sym->name);
if (Expand_Ok)
n->sym->hidden |= (4|8|16); /* formal par */
if (vis)
{ if (strncmp(vis->sym->name, ":hide:", 6) == 0)
n->sym->hidden |= 1;
else if (strncmp(vis->sym->name, ":show:", 6) == 0)
{ if (strncmp(vis->sym->name, ":hide:", (size_t) 6) == 0)
{ n->sym->hidden |= 1;
has_hidden++;
} else if (strncmp(vis->sym->name, ":show:", (size_t) 6) == 0)
n->sym->hidden |= 2;
else if (strncmp(vis->sym->name, ":local:", 7) == 0)
else if (strncmp(vis->sym->name, ":local:", (size_t) 7) == 0)
n->sym->hidden |= 64;
}
n->sym->type = STRUCT; /* classification */
@ -196,6 +196,7 @@ Rval_struct(Lextok *n, Symbol *v, int xinit) /* n varref, v valref */
fatal("non-zero 'rgt' on non-structure", 0);
ix = eval(tmp->lft);
/* printf("%d: ix: %d (%d) %d\n", depth, ix, tl->nel, tl->val[ix]); */
if (ix >= tl->nel || ix < 0)
fatal("indexing error \'%s\'", tl->name);
@ -222,10 +223,12 @@ Lval_struct(Lextok *n, Symbol *v, int xinit, int a) /* a = assigned value */
fatal("indexing error \'%s\'", tl->name);
if (tl->nbits > 0)
a = (a & ((1<<tl->nbits)-1));
tl->val[ix] = a;
tl->setat = depth;
a = (a & ((1<<tl->nbits)-1));
if (a != tl->val[ix])
{ tl->val[ix] = a;
tl->setat = depth;
}
return 1;
}
@ -246,7 +249,7 @@ is_lst:
for (fp = n; fp; fp = fp->rgt)
for (tl = fp->lft; tl; tl = tl->rgt)
{ if (tl->sym->type == STRUCT)
{ if (tl->sym->nel != 1)
{ if (tl->sym->nel > 1 || tl->sym->isarray)
fatal("array of structures in param list, %s",
tl->sym->name);
cnt += Cnt_flds(tl->sym->Slst);
@ -266,9 +269,9 @@ Sym_typ(Lextok *t)
return s->type;
if (!t->rgt
|| !t->rgt->ntyp == '.'
|| t->rgt->ntyp != '.' /* gh: had ! in wrong place */
|| !t->rgt->lft)
return STRUCT; /* not a field reference */
return STRUCT; /* not a field reference */
return Sym_typ(t->rgt->lft);
}
@ -315,6 +318,7 @@ cpnn(Lextok *s, int L, int R, int S)
if (!s) return ZN;
d = (Lextok *) emalloc(sizeof(Lextok));
d->uiid = s->uiid;
d->ntyp = s->ntyp;
d->val = s->val;
d->ln = s->ln;
@ -353,7 +357,7 @@ full_name(FILE *fd, Lextok *n, Symbol *v, int xinit)
goto out;
}
fprintf(fd, ".%s", tl->name);
out: if (tmp->sym->nel > 1)
out: if (tmp->sym->nel > 1 || tmp->sym->isarray == 1)
{ fprintf(fd, "[%d]", eval(tmp->lft));
hiddenarrays = 1;
}
@ -391,7 +395,7 @@ struct_name(Lextok *n, Symbol *v, int xinit, char *buf)
}
sprintf(lbuf, ".%s", tl->name);
strcat(buf, lbuf);
if (tmp->sym->nel > 1)
if (tmp->sym->nel > 1 || tmp->sym->isarray == 1)
{ sprintf(lbuf, "[%d]", eval(tmp->lft));
strcat(buf, lbuf);
}
@ -405,10 +409,10 @@ walk2_struct(char *s, Symbol *z)
extern void Done_case(char *, Symbol *);
ini_struct(z);
if (z->nel == 1)
if (z->nel == 1 && z->isarray == 0)
sprintf(eprefix, "%s%s.", s, z->name);
for (ix = 0; ix < z->nel; ix++)
{ if (z->nel > 1)
{ if (z->nel > 1 || z->isarray == 1)
sprintf(eprefix, "%s%s[%d].", s, z->name, ix);
for (fp = z->Sval[ix]; fp; fp = fp->rgt)
for (tl = fp->lft; tl; tl = tl->rgt)
@ -426,10 +430,10 @@ walk_struct(FILE *ofd, int dowhat, char *s, Symbol *z, char *a, char *b, char *c
int ix;
ini_struct(z);
if (z->nel == 1)
if (z->nel == 1 && z->isarray == 0)
sprintf(eprefix, "%s%s.", s, z->name);
for (ix = 0; ix < z->nel; ix++)
{ if (z->nel > 1)
{ if (z->nel > 1 || z->isarray == 1)
sprintf(eprefix, "%s%s[%d].", s, z->name, ix);
for (fp = z->Sval[ix]; fp; fp = fp->rgt)
for (tl = fp->lft; tl; tl = tl->rgt)
@ -443,7 +447,7 @@ walk_struct(FILE *ofd, int dowhat, char *s, Symbol *z, char *a, char *b, char *c
void
c_struct(FILE *fd, char *ipref, Symbol *z)
{ Lextok *fp, *tl;
char pref[256], eprefix[256];
char pref[256], eprefix[300];
int ix;
ini_struct(z);
@ -452,7 +456,7 @@ c_struct(FILE *fd, char *ipref, Symbol *z)
for (fp = z->Sval[ix]; fp; fp = fp->rgt)
for (tl = fp->lft; tl; tl = tl->rgt)
{ strcpy(eprefix, ipref);
if (z->nel > 1)
if (z->nel > 1 || z->isarray == 1)
{ /* insert index before last '.' */
eprefix[strlen(eprefix)-1] = '\0';
sprintf(pref, "[ %d ].", ix);
@ -476,7 +480,7 @@ dump_struct(Symbol *z, char *prefix, RunList *r)
ini_struct(z);
for (ix = 0; ix < z->nel; ix++)
{ if (z->nel > 1)
{ if (z->nel > 1 || z->isarray == 1)
sprintf(eprefix, "%s[%d]", prefix, ix);
else
strcpy(eprefix, prefix);
@ -484,7 +488,7 @@ dump_struct(Symbol *z, char *prefix, RunList *r)
for (fp = z->Sval[ix]; fp; fp = fp->rgt)
for (tl = fp->lft; tl; tl = tl->rgt)
{ if (tl->sym->type == STRUCT)
{ char pref[256];
{ char pref[300];
strcpy(pref, eprefix);
strcat(pref, ".");
strcat(pref, tl->sym->name);
@ -498,7 +502,7 @@ dump_struct(Symbol *z, char *prefix, RunList *r)
if (r)
printf("%s(%d):", r->n->name, r->pid);
printf("%s.%s", eprefix, tl->sym->name);
if (tl->sym->nel > 1)
if (tl->sym->nel > 1 || tl->sym->isarray == 1)
printf("[%d]", jx);
printf(" = ");
sr_mesg(stdout, tl->sym->val[jx],
@ -579,9 +583,11 @@ mk_explicit(Lextok *n, int Ok, int Ntyp)
int i, cnt; extern int IArgs;
if (n->sym->type != STRUCT
|| in_for
|| is_explicit(n))
return n;
if (n->rgt
&& n->rgt->ntyp == '.'
&& n->rgt->lft

159
sys/src/cmd/spin/sym.c
View File

@ -1,25 +1,27 @@
/***** spin: sym.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 */
/*
* 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 "spin.h"
#include "y.tab.h"
extern Symbol *Fname, *owner;
extern int lineno, depth, verbose, NamesNotAdded, deadvar;
extern int has_hidden, m_loss, old_scope_rules;
extern short has_xu;
extern char CurScope[MAXSCOPESZ];
Symbol *context = ZS;
Ordered *all_names = (Ordered *)0;
int Nid = 0;
Lextok *Mtype = (Lextok *) 0;
Lextok *runstmnts = ZN;
static Ordered *last_name = (Ordered *)0;
static Symbol *symtab[Nhash+1];
@ -31,12 +33,12 @@ samename(Symbol *a, Symbol *b)
return !strcmp(a->name, b->name);
}
int
hash(char *s)
{ int h=0;
unsigned int
hash(const char *s)
{ unsigned int h = 0;
while (*s)
{ h += *s++;
{ h += (unsigned int) *s++;
h <<= 1;
if (h&(Nhash+1))
h |= 1;
@ -44,31 +46,89 @@ hash(char *s)
return h&Nhash;
}
void
disambiguate(void)
{ Ordered *walk;
Symbol *sp;
char *n, *m;
if (old_scope_rules)
return;
/* prepend the scope_prefix to the names */
for (walk = all_names; walk; walk = walk->next)
{ sp = walk->entry;
if (sp->type != 0
&& sp->type != LABEL
&& strlen((const char *)sp->bscp) > 1)
{ if (sp->context)
{ m = (char *) emalloc(strlen((const char *)sp->bscp) + 1);
sprintf(m, "_%d_", sp->context->sc);
if (strcmp((const char *) m, (const char *) sp->bscp) == 0)
{ continue;
/* 6.2.0: only prepend scope for inner-blocks,
not for top-level locals within a proctype
this means that you can no longer use the same name
for a global and a (top-level) local variable
*/
} }
n = (char *) emalloc(strlen((const char *)sp->name)
+ strlen((const char *)sp->bscp) + 1);
sprintf(n, "%s%s", sp->bscp, sp->name);
sp->name = n; /* discard the old memory */
} }
}
Symbol *
lookup(char *s)
{ Symbol *sp; Ordered *no;
int h = hash(s);
unsigned int h = hash(s);
for (sp = symtab[h]; sp; sp = sp->next)
if (strcmp(sp->name, s) == 0
&& samename(sp->context, context)
&& samename(sp->owner, owner))
return sp; /* found */
if (old_scope_rules)
{ /* same scope - global refering to global or local to local */
for (sp = symtab[h]; sp; sp = sp->next)
{ if (strcmp(sp->name, s) == 0
&& samename(sp->context, context)
&& samename(sp->owner, owner))
{ return sp; /* found */
} }
} else
{ /* added 6.0.0: more traditional, scope rule */
for (sp = symtab[h]; sp; sp = sp->next)
{ if (strcmp(sp->name, s) == 0
&& samename(sp->context, context)
&& (strcmp((const char *)sp->bscp, CurScope) == 0
|| strncmp((const char *)sp->bscp, CurScope, strlen((const char *)sp->bscp)) == 0)
&& samename(sp->owner, owner))
{
if (!samename(sp->owner, owner))
{ printf("spin: different container %s\n", sp->name);
printf(" old: %s\n", sp->owner?sp->owner->name:"--");
printf(" new: %s\n", owner?owner->name:"--");
/* alldone(1); */
}
return sp; /* found */
} } }
if (context) /* in proctype */
if (context) /* in proctype, refers to global */
for (sp = symtab[h]; sp; sp = sp->next)
if (strcmp(sp->name, s) == 0
{ if (strcmp(sp->name, s) == 0
&& !sp->context
&& samename(sp->owner, owner))
return sp; /* global */
{ return sp; /* global */
} }
sp = (Symbol *) emalloc(sizeof(Symbol));
sp->name = (char *) emalloc((int) strlen(s) + 1);
sp->name = (char *) emalloc(strlen(s) + 1);
strcpy(sp->name, s);
sp->nel = 1;
sp->setat = depth;
sp->context = context;
sp->owner = owner; /* if fld in struct */
sp->bscp = (unsigned char *) emalloc(strlen((const char *)CurScope)+1);
strcpy((char *)sp->bscp, CurScope);
if (NamesNotAdded == 0)
{ sp->next = symtab[h];
@ -109,8 +169,6 @@ trackvar(Lextok *n, Lextok *m)
}
}
Lextok *runstmnts = ZN;
void
trackrun(Lextok *n)
{
@ -151,11 +209,11 @@ checkrun(Symbol *parnm, int posno)
strcpy(buf2, (!(res&4))?"bit":"byte");
sputtype(buf, parnm->type);
i = (int) strlen(buf);
while (buf[--i] == ' ') buf[i] = '\0';
if (strcmp(buf, buf2) == 0) return;
while (i > 0 && buf[--i] == ' ') buf[i] = '\0';
if (i == 0 || strcmp(buf, buf2) == 0) return;
prehint(parnm);
printf("proctype %s, '%s %s' could be declared",
parnm->context->name, buf, parnm->name);
parnm->context?parnm->context->name:"", buf, parnm->name);
printf(" '%s %s'\n", buf2, parnm->name);
}
}
@ -178,9 +236,9 @@ setptype(Lextok *n, int t, Lextok *vis) /* predefined types */
while (n)
{ if (n->sym->type && !(n->sym->hidden&32))
{ lineno = n->ln; Fname = n->fn;
non_fatal("redeclaration of '%s'", n->sym->name);
lineno = oln;
{ lineno = n->ln; Fname = n->fn;
fatal("redeclaration of '%s'", n->sym->name);
lineno = oln;
}
n->sym->type = (short) t;
@ -201,14 +259,15 @@ setptype(Lextok *n, int t, Lextok *vis) /* predefined types */
n->sym->name);
}
if (vis)
{ if (strncmp(vis->sym->name, ":hide:", 6) == 0)
{ if (strncmp(vis->sym->name, ":hide:", (size_t) 6) == 0)
{ n->sym->hidden |= 1;
has_hidden++;
if (t == BIT)
fatal("bit variable (%s) cannot be hidden",
n->sym->name);
} else if (strncmp(vis->sym->name, ":show:", 6) == 0)
} else if (strncmp(vis->sym->name, ":show:", (size_t) 6) == 0)
{ n->sym->hidden |= 2;
} else if (strncmp(vis->sym->name, ":local:", 7) == 0)
} else if (strncmp(vis->sym->name, ":local:", (size_t) 7) == 0)
{ n->sym->hidden |= 64;
}
}
@ -268,7 +327,13 @@ void
setxus(Lextok *p, int t)
{ Lextok *m, *n;
has_xu = 1;
has_xu = 1;
if (m_loss && t == XS)
{ printf("spin: %s:%d, warning, xs tag not compatible with -m (message loss)\n",
(p->fn != NULL) ? p->fn->name : "stdin", p->ln);
}
if (!context)
{ lineno = p->ln;
Fname = p->fn;
@ -276,6 +341,7 @@ setxus(Lextok *p, int t)
}
for (m = p; m; m = m->rgt)
{ Lextok *Xu_new = (Lextok *) emalloc(sizeof(Lextok));
Xu_new->uiid = p->uiid;
Xu_new->val = t;
Xu_new->lft = m->lft;
Xu_new->sym = context;
@ -297,8 +363,6 @@ setxus(Lextok *p, int t)
}
}
Lextok *Mtype = (Lextok *) 0;
void
setmtype(Lextok *m)
{ Lextok *n;
@ -332,7 +396,7 @@ setmtype(Lextok *m)
}
lineno = oln;
if (cnt > 256)
fatal("too many mtype elements (>255)", (char *)0);
fatal("too many mtype elements (>255)", (char *)0);
}
int
@ -389,11 +453,11 @@ symvar(Symbol *sp)
printf("\t");
if (sp->owner) printf("%s.", sp->owner->name);
printf("%s", sp->name);
if (sp->nel > 1) printf("[%d]", sp->nel);
if (sp->nel > 1 || sp->isarray == 1) printf("[%d]", sp->nel);
if (sp->type == CHAN)
printf("\t%d", (sp->ini)?sp->ini->val:0);
else if (sp->type == STRUCT) /* Frank Weil, 2.9.8 */
else if (sp->type == STRUCT && sp->Snm != NULL) /* Frank Weil, 2.9.8 */
printf("\t%s", sp->Snm->name);
else
printf("\t%d", eval(sp->ini));
@ -408,8 +472,13 @@ symvar(Symbol *sp)
if (sp->Nid < 0) /* formal parameter */
printf("\t<parameter %d>", -(sp->Nid));
else if (sp->type == MTYPE)
printf("\t<constant>");
else if (sp->isarray)
printf("\t<array>");
else
printf("\t<variable>");
if (sp->type == CHAN && sp->ini)
{ int i;
for (m = sp->ini->rgt, i = 0; m; m = m->rgt)
@ -423,6 +492,11 @@ symvar(Symbol *sp)
if (m->rgt) printf("\t");
}
}
if (!old_scope_rules)
{ printf("\t{scope %s}", sp->bscp);
}
printf("\n");
}
@ -440,11 +514,10 @@ chname(Symbol *sp)
if (sp->context) printf("%s-", sp->context->name);
if (sp->owner) printf("%s.", sp->owner->name);
printf("%s", sp->name);
if (sp->nel > 1) printf("[%d]", sp->nel);
if (sp->nel > 1 || sp->isarray == 1) printf("[%d]", sp->nel);
printf("\t");
}
static struct X {
int typ; char *nm;
} xx[] = {
@ -521,14 +594,14 @@ chanaccess(void)
if (!(verbose&32) || has_code) continue;
printf("spin: warning, %s, ", Fname->name);
printf("spin: %s:0, warning, ", Fname->name);
sputtype(buf, walk->entry->type);
if (walk->entry->context)
printf("proctype %s",
walk->entry->context->name);
else
printf("global");
printf(", '%s%s' variable is never used\n",
printf(", '%s%s' variable is never used (other than in print stmnts)\n",
buf, walk->entry->name);
} }
}

29
sys/src/cmd/spin/tl.h
View File

@ -1,16 +1,13 @@
/***** tl_spin: tl.h *****/
/* Copyright (c) 1995-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 */
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
/*
* 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
*
* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
*/
#include <stdio.h>
#include <string.h>
@ -66,6 +63,7 @@ enum {
#ifdef NXT
, NEXT /* 269 */
#endif
, CEXPR /* 270 */
};
Node *Canonical(Node *);
@ -82,11 +80,12 @@ Symbol *tl_lookup(char *);
Symbol *getsym(Symbol *);
Symbol *DoDump(Node *);
char *emalloc(int); /* in main.c */
extern char *emalloc(size_t); /* in main.c */
extern unsigned int hash(const char *); /* in sym.c */
int anywhere(int, Node *, Node *);
int dump_cond(Node *, Node *, int);
int hash(char *); /* in sym.c */
int isalnum_(int); /* in spinlex.c */
int isequal(Node *, Node *);
int tl_Getchar(void);
@ -100,6 +99,10 @@ void exit(int);
void Fatal(char *, char *);
void fatal(char *, char *);
void fsm_print(void);
void ini_buchi(void);
void ini_cache(void);
void ini_rewrt(void);
void ini_trans(void);
void releasenode(int, Node *);
void tfree(void *);
void tl_explain(int);

56
sys/src/cmd/spin/tl_buchi.c
View File

@ -1,20 +1,18 @@
/***** tl_spin: tl_buchi.c *****/
/* Copyright (c) 1995-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 */
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
/*
* 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
*
* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
*/
#include "tl.h"
extern int tl_verbose, tl_clutter, Total, Max_Red;
extern char *claim_name;
FILE *tl_out; /* if standalone: = stdout; */
@ -38,6 +36,13 @@ typedef struct State {
static State *never = (State *) 0;
static int hitsall;
void
ini_buchi(void)
{
never = (State *) 0;
hitsall = 0;
}
static int
sametrans(Transition *s, Transition *t)
{
@ -58,6 +63,7 @@ Prune(Node *p)
#ifdef NXT
case NEXT:
#endif
case CEXPR:
return p;
case OR:
p->lft = Prune(p->lft);
@ -545,10 +551,22 @@ rev_trans(Transition *t) /* print transitions in reverse order... */
rev_trans(t->nxt);
if (t->redundant && !tl_verbose) return;
fprintf(tl_out, "\t:: (");
if (dump_cond(t->cond, t->cond, 1))
fprintf(tl_out, "1");
fprintf(tl_out, ") -> goto %s\n", t->name->name);
if (strcmp(t->name->name, "accept_all") == 0) /* 6.2.4 */
{ /* not d_step because there may be remote refs */
fprintf(tl_out, "\t:: atomic { (");
if (dump_cond(t->cond, t->cond, 1))
fprintf(tl_out, "1");
fprintf(tl_out, ") -> assert(!(");
if (dump_cond(t->cond, t->cond, 1))
fprintf(tl_out, "1");
fprintf(tl_out, ")) }\n");
} else
{ fprintf(tl_out, "\t:: (");
if (dump_cond(t->cond, t->cond, 1))
fprintf(tl_out, "1");
fprintf(tl_out, ") -> goto %s\n", t->name->name);
}
tcnt++;
}
@ -570,11 +588,11 @@ printstate(State *b)
&& Max_Red == 0)
fprintf(tl_out, "T0%s:\n", &(b->name->name[6]));
fprintf(tl_out, "\tif\n");
fprintf(tl_out, "\tdo\n");
tcnt = 0;
rev_trans(b->trans);
if (!tcnt) fprintf(tl_out, "\t:: false\n");
fprintf(tl_out, "\tfi;\n");
fprintf(tl_out, "\tod;\n");
Total++;
}
@ -626,13 +644,13 @@ fsm_print(void)
if (tl_clutter) clutter();
b = findstate("T0_init");
if (Max_Red == 0)
if (b && (Max_Red == 0))
b->accepting = 1;
mergestates(0);
b = findstate("T0_init");
fprintf(tl_out, "never { /* ");
fprintf(tl_out, "never %s { /* ", claim_name?claim_name:"");
put_uform();
fprintf(tl_out, " */\n");

35
sys/src/cmd/spin/tl_cache.c
View File

@ -1,16 +1,13 @@
/***** tl_spin: tl_cache.c *****/
/* Copyright (c) 1995-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 */
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
/*
* 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
*
* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
*/
#include "tl.h"
@ -24,9 +21,18 @@ typedef struct Cache {
static Cache *stored = (Cache *) 0;
static unsigned long Caches, CacheHits;
static int ismatch(Node *, Node *);
static int ismatch(Node *, Node *);
static int sameform(Node *, Node *);
extern void fatal(char *, char *);
int sameform(Node *, Node *);
void
ini_cache(void)
{
stored = (Cache *) 0;
Caches = 0;
CacheHits = 0;
}
#if 0
void
@ -182,7 +188,7 @@ sametrees(int ntyp, Node *a, Node *b)
return all_lfts(ntyp, b, a);
}
int /* a better isequal() */
static int /* a better isequal() */
sameform(Node *a, Node *b)
{
if (!a && !b) return 1;
@ -206,6 +212,7 @@ sameform(Node *a, Node *b)
#ifdef NXT
case NEXT:
#endif
case CEXPR:
return sameform(a->lft, b->lft);
case U_OPER:
case V_OPER:

150
sys/src/cmd/spin/tl_lex.c
View File

@ -1,16 +1,13 @@
/***** tl_spin: tl_lex.c *****/
/* Copyright (c) 1995-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 */
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
/*
* 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
*
* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
*/
#include <stdlib.h>
#include <ctype.h>
@ -18,6 +15,7 @@
static Symbol *symtab[Nhash+1];
static int tl_lex(void);
extern int tl_peek(int);
extern YYSTYPE tl_yylval;
extern char yytext[];
@ -26,11 +24,19 @@ extern char yytext[];
static void
tl_getword(int first, int (*tst)(int))
{ int i=0; char c;
{ int i=0; int c;
yytext[i++] = (char ) first;
while (tst(c = tl_Getchar()))
yytext[i++] = c;
c = tl_Getchar();
while (c != -1 && tst(c))
{ yytext[i++] = (char) c;
c = tl_Getchar();
}
/* while (tst(c = tl_Getchar()))
* yytext[i++] = c;
*/
yytext[i] = '\0';
tl_UnGetchar();
}
@ -54,11 +60,85 @@ int
tl_yylex(void)
{ int c = tl_lex();
#if 0
printf("c = %d\n", c);
printf("c = %c (%d)\n", c, c);
#endif
return c;
}
static int
is_predicate(int z)
{ char c, c_prev = z;
char want = (z == '{') ? '}' : ')';
int i = 0, j, nesting = 0;
char peek_buf[512];
c = tl_peek(i++); /* look ahead without changing position */
while ((c != want || nesting > 0) && c != -1 && i < 2047)
{ if (islower((int) c) || c == '_')
{ peek_buf[0] = c;
j = 1;
while (j < (int) sizeof(peek_buf)
&& (isalnum((int)(c = tl_peek(i))) || c == '_'))
{ peek_buf[j++] = c;
i++;
}
c = 0; /* make sure we don't match on z or want on the peekahead */
if (j >= (int) sizeof(peek_buf))
{ peek_buf[j-1] = '\0';
fatal("name '%s' in ltl formula too long", peek_buf);
}
peek_buf[j] = '\0';
if (strcmp(peek_buf, "always") == 0
|| strcmp(peek_buf, "equivalent") == 0
|| strcmp(peek_buf, "eventually") == 0
|| strcmp(peek_buf, "until") == 0
|| strcmp(peek_buf, "next") == 0
|| strcmp(peek_buf, "c_expr") == 0)
{ return 0;
}
} else
{ int c_nxt = tl_peek(i);
if (((c == 'U' || c == 'V' || c == 'X')
&& !isalnum_(c_prev)
&& (c_nxt == -1 || !isalnum_(c_nxt)))
|| (c == '<' && c_nxt == '>')
|| (c == '<' && c_nxt == '-')
|| (c == '-' && c_nxt == '>')
|| (c == '[' && c_nxt == ']'))
{ return 0;
} }
if (c == z)
{ nesting++;
}
if (c == want)
{ nesting--;
}
c_prev = c;
c = tl_peek(i++);
}
return 1;
}
static void
read_upto_closing(int z)
{ char c, want = (z == '{') ? '}' : ')';
int i = 0, nesting = 0;
c = tl_Getchar();
while ((c != want || nesting > 0) && c != -1 && i < 2047) /* yytext is 2048 */
{ yytext[i++] = c;
if (c == z)
{ nesting++;
}
if (c == want)
{ nesting--;
}
c = tl_Getchar();
}
yytext[i] = '\0';
}
static int
tl_lex(void)
{ int c;
@ -74,6 +154,20 @@ tl_lex(void)
} while (c == ' '); /* '\t' is removed in tl_main.c */
if (c == '{' || c == '(') /* new 6.0.0 */
{ if (is_predicate(c))
{ read_upto_closing(c);
tl_yylval = tl_nn(PREDICATE,ZN,ZN);
if (!tl_yylval)
{ fatal("unexpected error 4", (char *) 0);
}
tl_yylval->sym = tl_lookup(yytext);
return PREDICATE;
} }
if (c == '}')
{ tl_yyerror("unexpected '}'");
}
if (islower(c))
{ tl_getword(c, isalnum_);
if (strcmp("true", yytext) == 0)
@ -82,10 +176,34 @@ tl_lex(void)
if (strcmp("false", yytext) == 0)
{ Token(FALSE);
}
if (strcmp("always", yytext) == 0)
{ Token(ALWAYS);
}
if (strcmp("eventually", yytext) == 0)
{ Token(EVENTUALLY);
}
if (strcmp("until", yytext) == 0)
{ Token(U_OPER);
}
#ifdef NXT
if (strcmp("next", yytext) == 0)
{ Token(NEXT);
}
#endif
if (strcmp("c_expr", yytext) == 0)
{ Token(CEXPR);
}
if (strcmp("not", yytext) == 0)
{ Token(NOT);
}
tl_yylval = tl_nn(PREDICATE,ZN,ZN);
if (!tl_yylval)
{ fatal("unexpected error 5", (char *) 0);
}
tl_yylval->sym = tl_lookup(yytext);
return PREDICATE;
}
if (c == '<')
{ c = tl_Getchar();
if (c == '>')
@ -124,7 +242,7 @@ tl_lex(void)
Symbol *
tl_lookup(char *s)
{ Symbol *sp;
int h = hash(s);
unsigned int h = hash(s);
for (sp = symtab[h]; sp; sp = sp->next)
if (strcmp(sp->name, s) == 0)

95
sys/src/cmd/spin/tl_main.c
View File

@ -1,16 +1,13 @@
/***** tl_spin: tl_main.c *****/
/* Copyright (c) 1995-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 */
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
/*
* 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
*
* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
*/
#include "tl.h"
@ -21,7 +18,10 @@ int tl_errs = 0;
int tl_verbose = 0;
int tl_terse = 0;
int tl_clutter = 0;
int state_cnt = 0;
unsigned long All_Mem = 0;
char *claim_name;
static char uform[4096];
static int hasuform=0, cnt=0;
@ -38,6 +38,15 @@ tl_Getchar(void)
return -1;
}
int
tl_peek(int n)
{
if (cnt+n < hasuform)
{ return uform[cnt+n];
}
return -1;
}
void
tl_balanced(void)
{ int i;
@ -45,10 +54,21 @@ tl_balanced(void)
for (i = 0; i < hasuform; i++)
{ if (uform[i] == '(')
{ k++;
{ if (i > 0
&& ((uform[i-1] == '"' && uform[i+1] == '"')
|| (uform[i-1] == '\'' && uform[i+1] == '\'')))
{ continue;
}
k++;
} else if (uform[i] == ')')
{ k--;
{ if (i > 0
&& ((uform[i-1] == '"' && uform[i+1] == '"')
|| (uform[i-1] == '\'' && uform[i+1] == '\'')))
{ continue;
}
k--;
} }
if (k != 0)
{ tl_errs++;
tl_yyerror("parentheses not balanced");
@ -79,18 +99,40 @@ tl_stats(void)
int
tl_main(int argc, char *argv[])
{ int i;
extern int verbose, xspin;
tl_verbose = verbose;
tl_clutter = 1-xspin; /* use -X -f to turn off uncluttering */
extern int xspin, s_trail;
tl_verbose = 0; /* was: tl_verbose = verbose; */
if (xspin && s_trail)
{ tl_clutter = 1;
/* generating claims for a replay should
be done the same as when generating the
pan.c that produced the error-trail */
} else
{ tl_clutter = 1-xspin; /* use -X -f to turn off uncluttering */
}
newstates = 0;
state_cnt = 0;
tl_errs = 0;
tl_terse = 0;
All_Mem = 0;
memset(uform, 0, sizeof(uform));
hasuform=0;
cnt=0;
claim_name = (char *) 0;
ini_buchi();
ini_cache();
ini_rewrt();
ini_trans();
while (argc > 1 && argv[1][0] == '-')
{ switch (argv[1][1]) {
{
switch (argv[1][1]) {
case 'd': newstates = 1; /* debugging mode */
break;
case 'f': argc--; argv++;
for (i = 0; i < argv[1][i]; i++)
for (i = 0; argv[1][i]; i++)
{ if (argv[1][i] == '\t'
|| argv[1][i] == '\"'
|| argv[1][i] == '\n')
argv[1][i] = ' ';
}
@ -101,6 +143,10 @@ tl_main(int argc, char *argv[])
break;
case 'n': tl_terse = 1;
break;
case 'c': argc--; argv++;
claim_name = (char *) emalloc(strlen(argv[1])+1);
strcpy(claim_name, argv[1]);
break;
default : printf("spin -f: saw '-%c'\n", argv[1][1]);
goto nogood;
}
@ -162,6 +208,12 @@ dump(Node *n)
case PREDICATE:
fprintf(tl_out, "(%s)", n->sym->name);
break;
case CEXPR:
fprintf(tl_out, "c_expr");
fprintf(tl_out, " {");
dump(n->lft);
fprintf(tl_out, "}");
break;
case -1:
fprintf(tl_out, " D ");
break;
@ -189,6 +241,7 @@ tl_explain(int n)
#ifdef NXT
case NEXT: printf("X"); break;
#endif
case CEXPR: printf("c_expr"); break;
case TRUE: printf("true"); break;
case FALSE: printf("false"); break;
case ';': printf("end of formula"); break;
@ -202,10 +255,14 @@ tl_non_fatal(char *s1, char *s2)
int i;
printf("tl_spin: ");
#if 1
printf(s1, s2); /* prevent a compiler warning */
#else
if (s2)
printf(s1, s2);
else
printf(s1);
#endif
if (tl_yychar != -1 && tl_yychar != 0)
{ printf(", saw '");
tl_explain(tl_yychar);

19
sys/src/cmd/spin/tl_mem.c
View File

@ -1,16 +1,13 @@
/***** tl_spin: tl_mem.c *****/
/* Copyright (c) 1995-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 */
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
/*
* 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
*
* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
*/
#include "tl.h"

36
sys/src/cmd/spin/tl_parse.c
View File

@ -1,16 +1,13 @@
/***** tl_spin: tl_parse.c *****/
/* Copyright (c) 1995-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 */
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
/*
* 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
*
* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
*/
#include "tl.h"
@ -44,11 +41,13 @@ tl_factor(void)
ptr = tl_yylval;
tl_yychar = tl_yylex();
ptr->lft = tl_factor();
if (!ptr->lft)
{ fatal("malformed expression", (char *) 0);
}
ptr = push_negation(ptr);
break;
case ALWAYS:
tl_yychar = tl_yylex();
ptr = tl_factor();
#ifndef NO_OPT
if (ptr->ntyp == FALSE
@ -73,6 +72,14 @@ tl_factor(void)
ptr = tl_nn(NEXT, ptr, ZN);
break;
#endif
case CEXPR:
tl_yychar = tl_yylex();
ptr = tl_factor();
if (ptr->ntyp != PREDICATE)
{ tl_yyerror("expected {...} after c_expr");
}
ptr = tl_nn(CEXPR, ptr, ZN);
break;
case EVENTUALLY:
tl_yychar = tl_yylex();
@ -385,7 +392,10 @@ tl_formula(void)
void
tl_parse(void)
{ Node *n = tl_formula();
{ Node *n;
/* tl_verbose = 1; */
n = tl_formula();
if (tl_verbose)
{ printf("formula: ");
dump(n);

33
sys/src/cmd/spin/tl_rewrt.c
View File

@ -1,16 +1,13 @@
/***** tl_spin: tl_rewrt.c *****/
/* Copyright (c) 1995-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 */
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
/*
* 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
*
* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
*/
#include "tl.h"
@ -18,6 +15,12 @@ extern int tl_verbose;
static Node *can = ZN;
void
ini_rewrt(void)
{
can = ZN;
}
Node *
right_linked(Node *n)
{
@ -137,6 +140,9 @@ addcan(int tok, Node *n)
}
s = DoDump(N);
if (!s)
{ fatal("unexpected error 6", (char *) 0);
}
if (can->ntyp != tok) /* only one element in list so far */
{ ptr = &can;
goto insert;
@ -146,7 +152,10 @@ addcan(int tok, Node *n)
prev = ZN;
for (m = can; m->ntyp == tok && m->rgt; prev = m, m = m->rgt)
{ t = DoDump(m->lft);
cmp = strcmp(s->name, t->name);
if (t != ZS)
cmp = strcmp(s->name, t->name);
else
cmp = 0;
if (cmp == 0) /* duplicate */
return;
if (cmp < 0)

77
sys/src/cmd/spin/tl_trans.c
View File

@ -1,21 +1,18 @@
/***** tl_spin: tl_trans.c *****/
/* Copyright (c) 1995-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 */
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
/*
* 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
*
* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
*/
#include "tl.h"
extern FILE *tl_out;
extern int tl_errs, tl_verbose, tl_terse, newstates;
extern int tl_errs, tl_verbose, tl_terse, newstates, state_cnt;
int Stack_mx=0, Max_Red=0, Total=0;
@ -23,7 +20,7 @@ static Mapping *Mapped = (Mapping *) 0;
static Graph *Nodes_Set = (Graph *) 0;
static Graph *Nodes_Stack = (Graph *) 0;
static char dumpbuf[2048];
static char dumpbuf[4096];
static int Red_cnt = 0;
static int Lab_cnt = 0;
static int Base = 0;
@ -51,6 +48,24 @@ static void ng(Symbol *, Symbol *, Node *, Node *, Node *);
static void push_stack(Graph *);
static void sdump(Node *);
void
ini_trans(void)
{
Stack_mx = 0;
Max_Red = 0;
Total = 0;
Mapped = (Mapping *) 0;
Nodes_Set = (Graph *) 0;
Nodes_Stack = (Graph *) 0;
memset(dumpbuf, 0, sizeof(dumpbuf));
Red_cnt = 0;
Lab_cnt = 0;
Base = 0;
Stack_sz = 0;
}
static void
dump_graph(Graph *g)
{ Node *n1;
@ -101,9 +116,8 @@ pop_stack(void)
static char *
newname(void)
{ static int cnt = 0;
static char buf[32];
sprintf(buf, "S%d", cnt++);
{ static char buf[32];
sprintf(buf, "S%d", state_cnt++);
return buf;
}
@ -132,6 +146,8 @@ static void
mk_grn(Node *n)
{ Graph *p;
if (!n) return;
n = right_linked(n);
more:
for (p = Nodes_Set; p; p = p->nxt)
@ -152,6 +168,8 @@ static void
mk_red(Node *n)
{ Graph *p;
if (!n) return;
n = right_linked(n);
for (p = Nodes_Set; p; p = p->nxt)
{ if (p->outgoing
@ -240,6 +258,15 @@ dump_cond(Node *pp, Node *r, int first)
q = dupnode(pp);
q = rewrite(q);
if (q->ntyp == CEXPR)
{ if (!frst) fprintf(tl_out, " && ");
fprintf(tl_out, "c_expr { ");
dump_cond(q->lft, r, 1);
fprintf(tl_out, " } ");
frst = 0;
return frst;
}
if (q->ntyp == PREDICATE
|| q->ntyp == NOT
#ifndef NXT
@ -342,7 +369,7 @@ static void
fsm_trans(Graph *p, int count, char *curnm)
{ Graph *r;
Symbol *s;
char prefix[128], nwnm[128];
char prefix[128], nwnm[256];
if (!p->outgoing)
addtrans(p, curnm, False, "accept_all");
@ -452,9 +479,11 @@ fixinit(Node *orig)
ng(tl_lookup("init"), ZS, ZN, ZN, ZN);
p1 = pop_stack();
p1->nxt = Nodes_Set;
p1->Other = p1->Old = orig;
Nodes_Set = p1;
if (p1)
{ p1->nxt = Nodes_Set;
p1->Other = p1->Old = orig;
Nodes_Set = p1;
}
for (g = Nodes_Set; g; g = g->nxt)
{ for (q1 = g->incoming; q1; q1 = q2)
@ -532,6 +561,10 @@ common1: sdump(n->lft);
case NEXT: strcat(dumpbuf, "X");
goto common1;
#endif
case CEXPR: strcat(dumpbuf, "c_expr {");
sdump(n->lft);
strcat(dumpbuf, "}");
break;
case NOT: strcat(dumpbuf, "!");
goto common1;
case TRUE: strcat(dumpbuf, "T");
@ -718,10 +751,13 @@ out:
break;
case PREDICATE:
case NOT:
case CEXPR:
if (can_release) releasenode(1, now);
push_stack(g);
break;
case V_OPER:
Assert(now->rgt != ZN, now->ntyp);
Assert(now->lft != ZN, now->ntyp);
Assert(now->rgt->nxt == ZN, now->ntyp);
Assert(now->lft->nxt == ZN, now->ntyp);
n1 = now->rgt;
@ -759,6 +795,7 @@ out:
#ifdef NXT
case NEXT:
Assert(now->lft != ZN, now->ntyp);
nx = dupnode(now->lft);
nx->nxt = g->Next;
g->Next = nx;

120
sys/src/cmd/spin/vars.c
View File

@ -1,13 +1,10 @@
/***** spin: vars.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 */
/*
* 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 "spin.h"
#include "y.tab.h"
@ -17,7 +14,7 @@ extern RunList *X, *LastX;
extern Symbol *Fname;
extern char Buf[];
extern int lineno, depth, verbose, xspin, limited_vis;
extern int analyze, jumpsteps, nproc, nstop, columns;
extern int analyze, jumpsteps, nproc, nstop, columns, old_priority_rules;
extern short no_arrays, Have_claim;
extern void sr_mesg(FILE *, int, int);
extern void sr_buf(int, int);
@ -42,22 +39,54 @@ getval(Lextok *sn)
{ if (!X) return 0;
return X->pid - Have_claim;
}
if (strcmp(s->name, "_priority") == 0)
{ if (!X) return 0;
if (old_priority_rules)
{ non_fatal("cannot refer to _priority with -o6", (char *) 0);
return 1;
}
return X->priority;
}
if (strcmp(s->name, "_nr_pr") == 0)
return nproc-nstop; /* new 3.3.10 */
{ return nproc-nstop; /* new 3.3.10 */
}
if (s->context && s->type)
return getlocal(sn);
{ return getlocal(sn);
}
if (!s->type) /* not declared locally */
{ s = lookup(s->name); /* try global */
sn->sym = s; /* fix it */
}
return getglobal(sn);
}
int
setval(Lextok *v, int n)
{
if (strcmp(v->sym->name, "_last") == 0
|| strcmp(v->sym->name, "_p") == 0
|| strcmp(v->sym->name, "_pid") == 0
|| strcmp(v->sym->name, "_nr_qs") == 0
|| strcmp(v->sym->name, "_nr_pr") == 0)
{ non_fatal("illegal assignment to %s", v->sym->name);
}
if (strcmp(v->sym->name, "_priority") == 0)
{ if (old_priority_rules)
{ non_fatal("cannot refer to _priority with -o6", (char *) 0);
return 1;
}
if (!X)
{ non_fatal("no context for _priority", (char *) 0);
return 1;
}
X->priority = n;
}
if (v->sym->context && v->sym->type)
return setlocal(v, n);
if (!v->sym->type)
@ -90,6 +119,7 @@ int
checkvar(Symbol *s, int n)
{ int i, oln = lineno; /* calls on eval() change it */
Symbol *ofnm = Fname;
Lextok *z, *y;
if (!in_bound(s, n))
return 0;
@ -101,15 +131,23 @@ checkvar(Symbol *s, int n)
/* not a STRUCT */
if (s->val == (int *) 0) /* uninitialized */
{ s->val = (int *) emalloc(s->nel*sizeof(int));
z = s->ini;
for (i = 0; i < s->nel; i++)
{ if (s->type != CHAN)
{ rm_selfrefs(s, s->ini);
s->val[i] = eval(s->ini);
{ if (z && z->ntyp == ',')
{ y = z->lft;
z = z->rgt;
} else
{ y = z;
}
if (s->type != CHAN)
{ rm_selfrefs(s, y);
s->val[i] = eval(y);
} else if (!analyze)
s->val[i] = qmake(s);
} }
{ s->val[i] = qmake(s);
} } }
lineno = oln;
Fname = ofnm;
return 1;
}
@ -118,14 +156,16 @@ getglobal(Lextok *sn)
{ Symbol *s = sn->sym;
int i, n = eval(sn->lft);
if (s->type == 0 && X && (i = find_lab(s, X->n, 0)))
if (s->type == 0 && X && (i = find_lab(s, X->n, 0))) /* getglobal */
{ printf("findlab through getglobal on %s\n", s->name);
return i; /* can this happen? */
}
if (s->type == STRUCT)
return Rval_struct(sn, s, 1); /* 1 = check init */
{ return Rval_struct(sn, s, 1); /* 1 = check init */
}
if (checkvar(s, n))
return cast_val(s->type, s->val[n], s->nbits);
{ return cast_val(s->type, s->val[n], s->nbits);
}
return 0;
}
@ -145,23 +185,26 @@ cast_val(int t, int v, int w)
}
if (v != i+s+ (int) u)
{ char buf[32]; sprintf(buf, "%d->%d (%d)", v, i+s+u, t);
{ char buf[64]; sprintf(buf, "%d->%d (%d)", v, i+s+(int)u, t);
non_fatal("value (%s) truncated in assignment", buf);
}
return (int)(i+s+u);
return (int)(i+s+(int)u);
}
static int
setglobal(Lextok *v, int m)
{
if (v->sym->type == STRUCT)
(void) Lval_struct(v, v->sym, 1, m);
else
{ (void) Lval_struct(v, v->sym, 1, m);
} else
{ int n = eval(v->lft);
if (checkvar(v->sym, n))
{ v->sym->val[n] = cast_val(v->sym->type, m, v->sym->nbits);
v->sym->setat = depth;
} }
{ int oval = v->sym->val[n];
int nval = cast_val(v->sym->type, m, v->sym->nbits);
v->sym->val[n] = nval;
if (oval != nval)
{ v->sym->setat = depth;
} } }
return 1;
}
@ -215,7 +258,12 @@ dumpglobals(void)
continue;
if (sp->type == STRUCT)
{ dump_struct(sp, sp->name, 0);
{ if ((verbose&4) && !(verbose&64)
&& (sp->setat < depth
&& jumpsteps != depth))
{ continue;
}
dump_struct(sp, sp->name, 0);
continue;
}
for (j = 0; j < sp->nel; j++)
@ -227,13 +275,15 @@ dumpglobals(void)
if ((verbose&4) && !(verbose&64)
&& (sp->setat < depth
&& jumpsteps != depth))
continue;
{ continue;
}
dummy->sym = sp;
dummy->lft->val = j;
/* in case of cast_val warnings, do this first: */
prefetch = getglobal(dummy);
printf("\t\t%s", sp->name);
if (sp->nel > 1) printf("[%d]", j);
if (sp->nel > 1 || sp->isarray) printf("[%d]", j);
printf(" = ");
sr_mesg(stdout, prefetch,
sp->type == MTYPE);
@ -249,7 +299,7 @@ dumpglobals(void)
}
sr_buf(prefetch, sp->type == MTYPE);
if (sp->colnr == 0)
{ sp->colnr = maxcolnr;
{ sp->colnr = (unsigned char) maxcolnr;
maxcolnr = 1+(maxcolnr%10);
}
colpos = nproc+sp->colnr-1;
@ -266,7 +316,7 @@ dumpglobals(void)
depth, colpos);
printf("(state 0)\t[printf('MSC: globvar\\\\n')]\n");
printf("\t\t%s", sp->name);
if (sp->nel > 1) printf("[%d]", j);
if (sp->nel > 1 || sp->isarray) printf("[%d]", j);
printf(" = %s\n", Buf);
} } }
}
@ -303,8 +353,8 @@ dumplocal(RunList *r)
dummy->lft->val = i;
printf("\t\t%s(%d):%s",
r->n->name, r->pid, z->name);
if (z->nel > 1) printf("[%d]", i);
r->n->name, r->pid - Have_claim, z->name);
if (z->nel > 1 || z->isarray) printf("[%d]", i);
printf(" = ");
sr_mesg(stdout, getval(dummy), z->type == MTYPE);
printf("\n");
@ -321,7 +371,7 @@ dumplocal(RunList *r)
}
sr_buf(getval(dummy), z->type==MTYPE);
if (z->colnr == 0)
{ z->colnr = maxcolnr;
{ z->colnr = (unsigned char) maxcolnr;
maxcolnr = 1+(maxcolnr%10);
}
colpos = nproc+z->colnr-1;
@ -341,7 +391,7 @@ dumplocal(RunList *r)
printf("(state 0)\t[printf('MSC: locvar\\\\n')]\n");
printf("\t\t%s(%d):%s",
r->n->name, r->pid, z->name);
if (z->nel > 1) printf("[%d]", i);
if (z->nel > 1 || z->isarray) printf("[%d]", i);
printf(" = %s\n", Buf);
} } }
}

10
sys/src/cmd/spin/version.h
View File

@ -1 +1,9 @@
#define Version "Spin Version 4.3.0 -- 22 June 2007"
/***** spin: version.h *****/
/*
* 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
*/
#define SpinVersion "Spin Version 6.4.7 -- 19 August 2017"