/***** spin: sym.c *****/ /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. *//* This software is for educational purposes only. *//* Permission is given to distribute this code provided that this intro- *//* ductory message is not removed and no monies are exchanged. *//* No guarantee is expressed or implied by the distribution of this code. *//* Software written by Gerard J. Holzmann as part of the book: *//* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4, *//* Prentice Hall, Englewood Cliffs, NJ, 07632. *//* Send bug-reports and/or questions to: gerard@research.att.com */ #include "spin.h"#include "y.tab.h" extern Symbol *Fname, *owner;extern int lineno, has_xu, depth; Symbol *symtab[Nhash+1];Symbol *context = ZS;int Nid = 0; intsamename(Symbol *a, Symbol *b){ if (!a && !b) return 1; if (!a || !b) return 0; return !strcmp(a->name, b->name);} inthash(char *s){ int h=0; while (*s) { h += *s++; h <<= 1; if (h&(Nhash+1)) h |= 1; } return h&Nhash;} Symbol *lookup(char *s){ Symbol *sp; 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 (context) /* local scope */ for (sp = symtab[h]; sp; sp = sp->next) if (strcmp(sp->name, s) == 0 && !sp->context && samename(sp->owner, owner)) return sp; /* global reference */ sp = (Symbol *) emalloc(sizeof(Symbol)); /* add */ 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->next = symtab[h]; symtab[h] = sp; return sp;} voidsetptype(Lextok *n, int t, Lextok *vis) /* predefined types */{ int oln = lineno; while (n) { if (n->sym->type) { lineno = n->ln; Fname = n->fn; non_fatal("redeclaration of '%s'", n->sym->name); lineno = oln; } n->sym->type = t; if (vis) n->sym->hidden = 1; if (t == CHAN) n->sym->Nid = ++Nid; else n->sym->Nid = 0; if (n->sym->nel <= 0) { lineno = n->ln; Fname = n->fn; non_fatal("bad array size for '%s'", n->sym->name); lineno = oln; } n = n->rgt; }} voidsetonexu(Symbol *sp, int t){ sp->xu |= t; if (t == XR || t == XS) { if (sp->xup[t-1] && strcmp(sp->xup[t-1]->name, context->name)) { printf("error: x[rs] claims from %s and %s\n", sp->xup[t-1]->name, context->name); non_fatal("conflicting claims on chan '%s'", sp->name); } sp->xup[t-1] = context; }} voidsetallxu(Lextok *n, int t){ Lextok *fp, *tl; for (fp = n; fp; fp = fp->rgt) for (tl = fp->lft; tl; tl = tl->rgt) { if (tl->sym->type == STRUCT) setallxu(tl->sym->Slst, t); else if (tl->sym->type == CHAN) setonexu(tl->sym, t); }} Lextok *Xu_List = (Lextok *) 0; voidsetxus(Lextok *p, int t){ Lextok *m, *n; has_xu = 1; if (!context) { lineno = p->ln; Fname = p->fn; non_fatal("non-local x[rs] assertion", (char *)0); } for (m = p; m; m = m->rgt) { Lextok *Xu_new = (Lextok *) emalloc(sizeof(Lextok)); Xu_new->val = t; Xu_new->lft = m->lft; Xu_new->sym = context; Xu_new->rgt = Xu_List; Xu_List = Xu_new; n = m->lft; if (n->sym->type == STRUCT) setallxu(n->sym->Slst, t); else if (n->sym->type == CHAN) setonexu(n->sym, t); else { int oln = lineno; lineno = n->ln; Fname = n->fn; non_fatal("xr or xs of non-chan '%s'", n->sym->name); lineno = oln; } }} Lextok *Mtype = (Lextok *) 0; voidsetmtype(Lextok *m){ Lextok *n = m; int oln = lineno; int cnt = 1; if (n) { lineno = n->ln; Fname = n->fn; } if (Mtype) non_fatal("mtype redeclared", (char *)0); Mtype = n; while (n) /* syntax check */ { if (!n->lft || !n->lft->sym || (n->lft->ntyp != NAME) || n->lft->lft) /* indexed variable */ fatal("bad mtype definition", (char *)0); /* label the name */ n->lft->sym->type = MTYPE; n->lft->sym->ini = nn(ZN,CONST,ZN,ZN); n->lft->sym->ini->val = cnt; n = n->rgt; cnt++; } lineno = oln;} intismtype(char *str){ Lextok *n; int cnt = 1; for (n = Mtype; n; n = n->rgt) { if (strcmp(str, n->lft->sym->name) == 0) return cnt; cnt++; } return 0;} intsputtype(char *foo, int m){ switch (m) { case BIT: strcpy(foo, "bit "); break; case BYTE: strcpy(foo, "byte "); break; case CHAN: strcpy(foo, "chan "); break; case SHORT: strcpy(foo, "short "); break; case INT: strcpy(foo, "int "); break; case MTYPE: strcpy(foo, "mtype "); break; case STRUCT: strcpy(foo, "struct"); break; case PROCTYPE: strcpy(foo, "proctype"); break; case LABEL: strcpy(foo, "label "); return 0; default: strcpy(foo, "value "); return 0; } return 1;} intputtype(int m){ char buf[32]; if (sputtype(buf, m)) { printf("%s", buf); return 1; } return 0;} voidsymvar(Symbol *sp){ Lextok *m; if (!puttype(sp->type)) return; printf("\t"); if (sp->owner) printf("%s.", sp->owner->name); printf("%s", sp->name); if (sp->nel > 1) printf("[%d]", sp->nel); if (sp->type == CHAN) printf("\t%d", (sp->ini)?sp->ini->val:0); else printf("\t%d", eval(sp->ini)); if (sp->owner) printf("\t<struct-field>"); else if (!sp->context) printf("\t<global>"); else printf("\t<%s>", sp->context->name); if (sp->Nid < 0) /* formal parameter */ printf("\t<parameter %d>", -(sp->Nid)); else printf("\t<variable>"); if (sp->type == CHAN && sp->ini) { int i; for (m = sp->ini->rgt, i = 0; m; m = m->rgt) i++; printf("\t%d\t", i); for (m = sp->ini->rgt; m; m = m->rgt) { (void) puttype(m->ntyp); if (m->rgt) printf("\t"); } } printf("\n");} voidsymdump(void){ Symbol *sp; int i; for (i = 0; i <= Nhash; i++) for (sp = symtab[i]; sp; sp = sp->next) symvar(sp);}
/***** spin: sym.c *****/
/* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */
/* This software is for educational purposes only. */
/* Permission is given to distribute this code provided that this intro- */
/* ductory message is not removed and no monies are exchanged. */
/* No guarantee is expressed or implied by the distribution of this code. */
/* Software written by Gerard J. Holzmann as part of the book: */
/* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4, */
/* Prentice Hall, Englewood Cliffs, NJ, 07632. */
/* Send bug-reports and/or questions to: gerard@research.att.com */
#include "spin.h"
#include "y.tab.h"
extern Symbol *Fname, *owner;
extern int lineno, has_xu, depth;
Symbol *symtab[Nhash+1];
Symbol *context = ZS;
int Nid = 0;
int
samename(Symbol *a, Symbol *b)
{
if (!a && !b) return 1;
if (!a || !b) return 0;
return !strcmp(a->name, b->name);
}
int
hash(char *s)
{ int h=0;
while (*s)
{ h += *s++;
h <<= 1;
if (h&(Nhash+1))
h |= 1;
}
return h&Nhash;
}
Symbol *
lookup(char *s)
{ Symbol *sp;
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 (context) /* local scope */
for (sp = symtab[h]; sp; sp = sp->next)
if (strcmp(sp->name, s) == 0
&& !sp->context
&& samename(sp->owner, owner))
return sp; /* global reference */
sp = (Symbol *) emalloc(sizeof(Symbol)); /* add */
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->next = symtab[h];
symtab[h] = sp;
return sp;
}
void
setptype(Lextok *n, int t, Lextok *vis) /* predefined types */
{ int oln = lineno;
while (n)
{ if (n->sym->type)
{ lineno = n->ln; Fname = n->fn;
non_fatal("redeclaration of '%s'", n->sym->name);
lineno = oln;
}
n->sym->type = t;
if (vis)
n->sym->hidden = 1;
if (t == CHAN)
n->sym->Nid = ++Nid;
else
n->sym->Nid = 0;
if (n->sym->nel <= 0)
{ lineno = n->ln; Fname = n->fn;
non_fatal("bad array size for '%s'", n->sym->name);
lineno = oln;
}
n = n->rgt;
}
}
void
setonexu(Symbol *sp, int t)
{
sp->xu |= t;
if (t == XR || t == XS)
{ if (sp->xup[t-1]
&& strcmp(sp->xup[t-1]->name, context->name))
{ printf("error: x[rs] claims from %s and %s\n",
sp->xup[t-1]->name, context->name);
non_fatal("conflicting claims on chan '%s'",
sp->name);
}
sp->xup[t-1] = context;
}
}
void
setallxu(Lextok *n, int t)
{ Lextok *fp, *tl;
for (fp = n; fp; fp = fp->rgt)
for (tl = fp->lft; tl; tl = tl->rgt)
{ if (tl->sym->type == STRUCT)
setallxu(tl->sym->Slst, t);
else if (tl->sym->type == CHAN)
setonexu(tl->sym, t);
}
}
Lextok *Xu_List = (Lextok *) 0;
void
setxus(Lextok *p, int t)
{ Lextok *m, *n;
has_xu = 1;
if (!context)
{ lineno = p->ln;
Fname = p->fn;
non_fatal("non-local x[rs] assertion", (char *)0);
}
for (m = p; m; m = m->rgt)
{ Lextok *Xu_new = (Lextok *) emalloc(sizeof(Lextok));
Xu_new->val = t;
Xu_new->lft = m->lft;
Xu_new->sym = context;
Xu_new->rgt = Xu_List;
Xu_List = Xu_new;
n = m->lft;
if (n->sym->type == STRUCT)
setallxu(n->sym->Slst, t);
else if (n->sym->type == CHAN)
setonexu(n->sym, t);
else
{ int oln = lineno;
lineno = n->ln; Fname = n->fn;
non_fatal("xr or xs of non-chan '%s'",
n->sym->name);
lineno = oln;
}
}
}
Lextok *Mtype = (Lextok *) 0;
void
setmtype(Lextok *m)
{ Lextok *n = m;
int oln = lineno;
int cnt = 1;
if (n)
{ lineno = n->ln; Fname = n->fn;
}
if (Mtype)
non_fatal("mtype redeclared", (char *)0);
Mtype = n;
while (n) /* syntax check */
{ if (!n->lft || !n->lft->sym
|| (n->lft->ntyp != NAME)
|| n->lft->lft) /* indexed variable */
fatal("bad mtype definition", (char *)0);
/* label the name */
n->lft->sym->type = MTYPE;
n->lft->sym->ini = nn(ZN,CONST,ZN,ZN);
n->lft->sym->ini->val = cnt;
n = n->rgt;
cnt++;
}
lineno = oln;
}
int
ismtype(char *str)
{ Lextok *n;
int cnt = 1;
for (n = Mtype; n; n = n->rgt)
{ if (strcmp(str, n->lft->sym->name) == 0)
return cnt;
cnt++;
}
return 0;
}
int
sputtype(char *foo, int m)
{
switch (m) {
case BIT: strcpy(foo, "bit "); break;
case BYTE: strcpy(foo, "byte "); break;
case CHAN: strcpy(foo, "chan "); break;
case SHORT: strcpy(foo, "short "); break;
case INT: strcpy(foo, "int "); break;
case MTYPE: strcpy(foo, "mtype "); break;
case STRUCT: strcpy(foo, "struct"); break;
case PROCTYPE: strcpy(foo, "proctype"); break;
case LABEL: strcpy(foo, "label "); return 0;
default: strcpy(foo, "value "); return 0;
}
return 1;
}
int
puttype(int m)
{ char buf[32];
if (sputtype(buf, m))
{ printf("%s", buf);
return 1;
}
return 0;
}
void
symvar(Symbol *sp)
{ Lextok *m;
if (!puttype(sp->type))
return;
printf("\t");
if (sp->owner) printf("%s.", sp->owner->name);
printf("%s", sp->name);
if (sp->nel > 1) printf("[%d]", sp->nel);
if (sp->type == CHAN)
printf("\t%d", (sp->ini)?sp->ini->val:0);
else
printf("\t%d", eval(sp->ini));
if (sp->owner)
printf("\t<struct-field>");
else
if (!sp->context)
printf("\t<global>");
else
printf("\t<%s>", sp->context->name);
if (sp->Nid < 0) /* formal parameter */
printf("\t<parameter %d>", -(sp->Nid));
else
printf("\t<variable>");
if (sp->type == CHAN && sp->ini)
{ int i;
for (m = sp->ini->rgt, i = 0; m; m = m->rgt)
i++;
printf("\t%d\t", i);
for (m = sp->ini->rgt; m; m = m->rgt)
{ (void) puttype(m->ntyp);
if (m->rgt) printf("\t");
}
}
printf("\n");
}
void
symdump(void)
{ Symbol *sp;
int i;
for (i = 0; i <= Nhash; i++)
for (sp = symtab[i]; sp; sp = sp->next)
symvar(sp);
}