Blame | Last modification | View Log | RSS feed
/***** 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 */
#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;
static Ordered *last_name = (Ordered *)0;
static Symbol *symtab[Nhash+1];
static Lextok *runstmnts = ZN;
static 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;
}
void
disambiguate(void)
{ Ordered *walk;
Symbol *sp;
if (old_scope_rules)
return;
/* if the same name appears in two different scopes,
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)
{ char *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; /* discord the old memory */
} }
}
Symbol *
lookup(char *s)
{ Symbol *sp; Ordered *no;
int h = hash(s);
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, refers to global */
for (sp = symtab[h]; sp; sp = sp->next)
{ if (strcmp(sp->name, s) == 0
&& !sp->context
&& samename(sp->owner, owner))
{ return sp; /* global */
} }
sp = (Symbol *) emalloc(sizeof(Symbol));
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];
symtab[h] = sp;
no = (Ordered *) emalloc(sizeof(Ordered));
no->entry = sp;
if (!last_name)
last_name = all_names = no;
else
{ last_name->next = no;
last_name = no;
} }
return sp;
}
void
trackvar(Lextok *n, Lextok *m)
{ Symbol *sp = n->sym;
if (!sp) return; /* a structure list */
switch (m->ntyp) {
case NAME:
if (m->sym->type != BIT)
{ sp->hidden |= 4;
if (m->sym->type != BYTE)
sp->hidden |= 8;
}
break;
case CONST:
if (m->val != 0 && m->val != 1)
sp->hidden |= 4;
if (m->val < 0 || m->val > 256)
sp->hidden |= 8; /* ditto byte-equiv */
break;
default: /* unknown */
sp->hidden |= (4|8); /* not known bit-equiv */
}
}
void
trackrun(Lextok *n)
{
runstmnts = nn(ZN, 0, n, runstmnts);
}
void
checkrun(Symbol *parnm, int posno)
{ Lextok *n, *now, *v; int i, m;
int res = 0; char buf[16], buf2[16];
for (n = runstmnts; n; n = n->rgt)
{ now = n->lft;
if (now->sym != parnm->context)
continue;
for (v = now->lft, i = 0; v; v = v->rgt, i++)
if (i == posno)
{ m = v->lft->ntyp;
if (m == CONST)
{ m = v->lft->val;
if (m != 0 && m != 1)
res |= 4;
if (m < 0 || m > 256)
res |= 8;
} else if (m == NAME)
{ m = v->lft->sym->type;
if (m != BIT)
{ res |= 4;
if (m != BYTE)
res |= 8;
}
} else
res |= (4|8); /* unknown */
break;
} }
if (!(res&4) || !(res&8))
{ if (!(verbose&32)) return;
strcpy(buf2, (!(res&4))?"bit":"byte");
sputtype(buf, parnm->type);
i = (int) strlen(buf);
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?parnm->context->name:"", buf, parnm->name);
printf(" '%s %s'\n", buf2, parnm->name);
}
}
void
trackchanuse(Lextok *m, Lextok *w, int t)
{ Lextok *n = m; int cnt = 1;
while (n)
{ if (n->lft
&& n->lft->sym
&& n->lft->sym->type == CHAN)
setaccess(n->lft->sym, w?w->sym:ZS, cnt, t);
n = n->rgt; cnt++;
}
}
void
setptype(Lextok *n, int t, Lextok *vis) /* predefined types */
{ int oln = lineno, cnt = 1; extern int Expand_Ok;
while (n)
{ if (n->sym->type && !(n->sym->hidden&32))
{ lineno = n->ln; Fname = n->fn;
fatal("redeclaration of '%s'", n->sym->name);
lineno = oln;
}
n->sym->type = (short) t;
if (Expand_Ok)
{ n->sym->hidden |= (4|8|16); /* formal par */
if (t == CHAN)
setaccess(n->sym, ZS, cnt, 'F');
}
if (t == UNSIGNED)
{ if (n->sym->nbits < 0 || n->sym->nbits >= 32)
fatal("(%s) has invalid width-field", n->sym->name);
if (n->sym->nbits == 0)
{ n->sym->nbits = 16;
non_fatal("unsigned without width-field", 0);
}
} else if (n->sym->nbits > 0)
{ non_fatal("(%s) only an unsigned can have width-field",
n->sym->name);
}
if (vis)
{ 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:", (size_t) 6) == 0)
{ n->sym->hidden |= 2;
} else if (strncmp(vis->sym->name, ":local:", (size_t) 7) == 0)
{ n->sym->hidden |= 64;
}
}
if (t == CHAN)
n->sym->Nid = ++Nid;
else
{ n->sym->Nid = 0;
if (n->sym->ini
&& n->sym->ini->ntyp == CHAN)
{ Fname = n->fn;
lineno = n->ln;
fatal("chan initializer for non-channel %s",
n->sym->name);
}
}
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; cnt++;
}
}
static 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;
}
}
static 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 (m_loss && t == XS)
{ printf("spin: warning, %s:%d, 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;
fatal("non-local x[rs] assertion", (char *)0);
}
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;
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;
}
}
}
void
setmtype(Lextok *m)
{ Lextok *n;
int cnt, oln = lineno;
if (m) { lineno = m->ln; Fname = m->fn; }
if (!Mtype)
Mtype = m;
else
{ for (n = Mtype; n->rgt; n = n->rgt)
;
n->rgt = m; /* concatenate */
}
for (n = Mtype, cnt = 1; n; n = n->rgt, cnt++) /* 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 */
if (n->lft->sym->type != MTYPE)
{ n->lft->sym->hidden |= 128; /* is used */
n->lft->sym->type = MTYPE;
n->lft->sym->ini = nn(ZN,CONST,ZN,ZN);
n->lft->sym->ini->val = cnt;
} else if (n->lft->sym->ini->val != cnt)
non_fatal("name %s appears twice in mtype declaration",
n->lft->sym->name);
}
lineno = oln;
if (cnt > 256)
fatal("too many mtype elements (>255)", (char *)0);
}
int
ismtype(char *str) /* name to number */
{ 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 UNSIGNED: strcpy(foo, "unsigned "); break;
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;
}
static int
puttype(int m)
{ char buf[128];
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 || 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 && sp->Snm != NULL) /* Frank Weil, 2.9.8 */
printf("\t%s", sp->Snm->name);
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 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)
i++;
printf("\t%d\t", i);
for (m = sp->ini->rgt; m; m = m->rgt)
{ if (m->ntyp == STRUCT)
printf("struct %s", m->sym->name);
else
(void) puttype(m->ntyp);
if (m->rgt) printf("\t");
}
}
if (1) printf("\t{scope %s}", sp->bscp);
printf("\n");
}
void
symdump(void)
{ Ordered *walk;
for (walk = all_names; walk; walk = walk->next)
symvar(walk->entry);
}
void
chname(Symbol *sp)
{ printf("chan ");
if (sp->context) printf("%s-", sp->context->name);
if (sp->owner) printf("%s.", sp->owner->name);
printf("%s", sp->name);
if (sp->nel > 1 || sp->isarray == 1) printf("[%d]", sp->nel);
printf("\t");
}
static struct X {
int typ; char *nm;
} xx[] = {
{ 'A', "exported as run parameter" },
{ 'F', "imported as proctype parameter" },
{ 'L', "used as l-value in asgnmnt" },
{ 'V', "used as r-value in asgnmnt" },
{ 'P', "polled in receive stmnt" },
{ 'R', "used as parameter in receive stmnt" },
{ 'S', "used as parameter in send stmnt" },
{ 'r', "received from" },
{ 's', "sent to" },
};
static void
chan_check(Symbol *sp)
{ Access *a; int i, b=0, d;
if (verbose&1) goto report; /* -C -g */
for (a = sp->access; a; a = a->lnk)
if (a->typ == 'r')
b |= 1;
else if (a->typ == 's')
b |= 2;
if (b == 3 || (sp->hidden&16)) /* balanced or formal par */
return;
report:
chname(sp);
for (i = d = 0; i < (int) (sizeof(xx)/sizeof(struct X)); i++)
{ b = 0;
for (a = sp->access; a; a = a->lnk)
if (a->typ == xx[i].typ) b++;
if (b == 0) continue; d++;
printf("\n\t%s by: ", xx[i].nm);
for (a = sp->access; a; a = a->lnk)
if (a->typ == xx[i].typ)
{ printf("%s", a->who->name);
if (a->what) printf(" to %s", a->what->name);
if (a->cnt) printf(" par %d", a->cnt);
if (--b > 0) printf(", ");
}
}
printf("%s\n", (!d)?"\n\tnever used under this name":"");
}
void
chanaccess(void)
{ Ordered *walk;
char buf[128];
extern int Caccess, separate;
extern short has_code;
for (walk = all_names; walk; walk = walk->next)
{ if (!walk->entry->owner)
switch (walk->entry->type) {
case CHAN:
if (Caccess) chan_check(walk->entry);
break;
case MTYPE:
case BIT:
case BYTE:
case SHORT:
case INT:
case UNSIGNED:
if ((walk->entry->hidden&128)) /* was: 32 */
continue;
if (!separate
&& !walk->entry->context
&& !has_code
&& deadvar)
walk->entry->hidden |= 1; /* auto-hide */
if (!(verbose&32) || has_code) continue;
printf("spin: warning, %s, ", 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",
buf, walk->entry->name);
} }
}