1*219b2ee8SDavid du Colombier /***** spin: sym.c *****/ 2*219b2ee8SDavid du Colombier 3*219b2ee8SDavid du Colombier /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */ 4*219b2ee8SDavid du Colombier /* This software is for educational purposes only. */ 5*219b2ee8SDavid du Colombier /* Permission is given to distribute this code provided that this intro- */ 6*219b2ee8SDavid du Colombier /* ductory message is not removed and no monies are exchanged. */ 7*219b2ee8SDavid du Colombier /* No guarantee is expressed or implied by the distribution of this code. */ 8*219b2ee8SDavid du Colombier /* Software written by Gerard J. Holzmann as part of the book: */ 9*219b2ee8SDavid du Colombier /* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4, */ 10*219b2ee8SDavid du Colombier /* Prentice Hall, Englewood Cliffs, NJ, 07632. */ 11*219b2ee8SDavid du Colombier /* Send bug-reports and/or questions to: gerard@research.att.com */ 12*219b2ee8SDavid du Colombier 13*219b2ee8SDavid du Colombier #include "spin.h" 14*219b2ee8SDavid du Colombier #include "y.tab.h" 15*219b2ee8SDavid du Colombier 16*219b2ee8SDavid du Colombier extern Symbol *Fname, *owner; 17*219b2ee8SDavid du Colombier extern int lineno, has_xu, depth; 18*219b2ee8SDavid du Colombier 19*219b2ee8SDavid du Colombier Symbol *symtab[Nhash+1]; 20*219b2ee8SDavid du Colombier Symbol *context = ZS; 21*219b2ee8SDavid du Colombier int Nid = 0; 22*219b2ee8SDavid du Colombier 23*219b2ee8SDavid du Colombier int 24*219b2ee8SDavid du Colombier samename(Symbol *a, Symbol *b) 25*219b2ee8SDavid du Colombier { 26*219b2ee8SDavid du Colombier if (!a && !b) return 1; 27*219b2ee8SDavid du Colombier if (!a || !b) return 0; 28*219b2ee8SDavid du Colombier return !strcmp(a->name, b->name); 29*219b2ee8SDavid du Colombier } 30*219b2ee8SDavid du Colombier 31*219b2ee8SDavid du Colombier int 32*219b2ee8SDavid du Colombier hash(char *s) 33*219b2ee8SDavid du Colombier { int h=0; 34*219b2ee8SDavid du Colombier 35*219b2ee8SDavid du Colombier while (*s) 36*219b2ee8SDavid du Colombier { h += *s++; 37*219b2ee8SDavid du Colombier h <<= 1; 38*219b2ee8SDavid du Colombier if (h&(Nhash+1)) 39*219b2ee8SDavid du Colombier h |= 1; 40*219b2ee8SDavid du Colombier } 41*219b2ee8SDavid du Colombier return h&Nhash; 42*219b2ee8SDavid du Colombier } 43*219b2ee8SDavid du Colombier 44*219b2ee8SDavid du Colombier Symbol * 45*219b2ee8SDavid du Colombier lookup(char *s) 46*219b2ee8SDavid du Colombier { Symbol *sp; 47*219b2ee8SDavid du Colombier int h=hash(s); 48*219b2ee8SDavid du Colombier 49*219b2ee8SDavid du Colombier for (sp = symtab[h]; sp; sp = sp->next) 50*219b2ee8SDavid du Colombier if (strcmp(sp->name, s) == 0 51*219b2ee8SDavid du Colombier && samename(sp->context, context) 52*219b2ee8SDavid du Colombier && samename(sp->owner, owner)) 53*219b2ee8SDavid du Colombier return sp; /* found */ 54*219b2ee8SDavid du Colombier 55*219b2ee8SDavid du Colombier if (context) /* local scope */ 56*219b2ee8SDavid du Colombier for (sp = symtab[h]; sp; sp = sp->next) 57*219b2ee8SDavid du Colombier if (strcmp(sp->name, s) == 0 58*219b2ee8SDavid du Colombier && !sp->context 59*219b2ee8SDavid du Colombier && samename(sp->owner, owner)) 60*219b2ee8SDavid du Colombier return sp; /* global reference */ 61*219b2ee8SDavid du Colombier 62*219b2ee8SDavid du Colombier sp = (Symbol *) emalloc(sizeof(Symbol)); /* add */ 63*219b2ee8SDavid du Colombier sp->name = (char *) emalloc(strlen(s) + 1); 64*219b2ee8SDavid du Colombier strcpy(sp->name, s); 65*219b2ee8SDavid du Colombier sp->nel = 1; 66*219b2ee8SDavid du Colombier sp->setat = depth; 67*219b2ee8SDavid du Colombier sp->context = context; 68*219b2ee8SDavid du Colombier sp->owner = owner; /* if fld in struct */ 69*219b2ee8SDavid du Colombier sp->next = symtab[h]; 70*219b2ee8SDavid du Colombier symtab[h] = sp; 71*219b2ee8SDavid du Colombier 72*219b2ee8SDavid du Colombier return sp; 73*219b2ee8SDavid du Colombier } 74*219b2ee8SDavid du Colombier 75*219b2ee8SDavid du Colombier void 76*219b2ee8SDavid du Colombier setptype(Lextok *n, int t, Lextok *vis) /* predefined types */ 77*219b2ee8SDavid du Colombier { int oln = lineno; 78*219b2ee8SDavid du Colombier while (n) 79*219b2ee8SDavid du Colombier { if (n->sym->type) 80*219b2ee8SDavid du Colombier { lineno = n->ln; Fname = n->fn; 81*219b2ee8SDavid du Colombier non_fatal("redeclaration of '%s'", n->sym->name); 82*219b2ee8SDavid du Colombier lineno = oln; 83*219b2ee8SDavid du Colombier } 84*219b2ee8SDavid du Colombier n->sym->type = t; 85*219b2ee8SDavid du Colombier if (vis) 86*219b2ee8SDavid du Colombier n->sym->hidden = 1; 87*219b2ee8SDavid du Colombier if (t == CHAN) 88*219b2ee8SDavid du Colombier n->sym->Nid = ++Nid; 89*219b2ee8SDavid du Colombier else 90*219b2ee8SDavid du Colombier n->sym->Nid = 0; 91*219b2ee8SDavid du Colombier if (n->sym->nel <= 0) 92*219b2ee8SDavid du Colombier { lineno = n->ln; Fname = n->fn; 93*219b2ee8SDavid du Colombier non_fatal("bad array size for '%s'", n->sym->name); 94*219b2ee8SDavid du Colombier lineno = oln; 95*219b2ee8SDavid du Colombier } 96*219b2ee8SDavid du Colombier n = n->rgt; 97*219b2ee8SDavid du Colombier } 98*219b2ee8SDavid du Colombier } 99*219b2ee8SDavid du Colombier 100*219b2ee8SDavid du Colombier void 101*219b2ee8SDavid du Colombier setonexu(Symbol *sp, int t) 102*219b2ee8SDavid du Colombier { 103*219b2ee8SDavid du Colombier sp->xu |= t; 104*219b2ee8SDavid du Colombier if (t == XR || t == XS) 105*219b2ee8SDavid du Colombier { if (sp->xup[t-1] 106*219b2ee8SDavid du Colombier && strcmp(sp->xup[t-1]->name, context->name)) 107*219b2ee8SDavid du Colombier { printf("error: x[rs] claims from %s and %s\n", 108*219b2ee8SDavid du Colombier sp->xup[t-1]->name, context->name); 109*219b2ee8SDavid du Colombier non_fatal("conflicting claims on chan '%s'", 110*219b2ee8SDavid du Colombier sp->name); 111*219b2ee8SDavid du Colombier } 112*219b2ee8SDavid du Colombier sp->xup[t-1] = context; 113*219b2ee8SDavid du Colombier } 114*219b2ee8SDavid du Colombier } 115*219b2ee8SDavid du Colombier 116*219b2ee8SDavid du Colombier void 117*219b2ee8SDavid du Colombier setallxu(Lextok *n, int t) 118*219b2ee8SDavid du Colombier { Lextok *fp, *tl; 119*219b2ee8SDavid du Colombier 120*219b2ee8SDavid du Colombier for (fp = n; fp; fp = fp->rgt) 121*219b2ee8SDavid du Colombier for (tl = fp->lft; tl; tl = tl->rgt) 122*219b2ee8SDavid du Colombier { if (tl->sym->type == STRUCT) 123*219b2ee8SDavid du Colombier setallxu(tl->sym->Slst, t); 124*219b2ee8SDavid du Colombier else if (tl->sym->type == CHAN) 125*219b2ee8SDavid du Colombier setonexu(tl->sym, t); 126*219b2ee8SDavid du Colombier } 127*219b2ee8SDavid du Colombier } 128*219b2ee8SDavid du Colombier 129*219b2ee8SDavid du Colombier Lextok *Xu_List = (Lextok *) 0; 130*219b2ee8SDavid du Colombier 131*219b2ee8SDavid du Colombier void 132*219b2ee8SDavid du Colombier setxus(Lextok *p, int t) 133*219b2ee8SDavid du Colombier { Lextok *m, *n; 134*219b2ee8SDavid du Colombier 135*219b2ee8SDavid du Colombier has_xu = 1; 136*219b2ee8SDavid du Colombier if (!context) 137*219b2ee8SDavid du Colombier { lineno = p->ln; 138*219b2ee8SDavid du Colombier Fname = p->fn; 139*219b2ee8SDavid du Colombier non_fatal("non-local x[rs] assertion", (char *)0); 140*219b2ee8SDavid du Colombier } 141*219b2ee8SDavid du Colombier for (m = p; m; m = m->rgt) 142*219b2ee8SDavid du Colombier { Lextok *Xu_new = (Lextok *) emalloc(sizeof(Lextok)); 143*219b2ee8SDavid du Colombier Xu_new->val = t; 144*219b2ee8SDavid du Colombier Xu_new->lft = m->lft; 145*219b2ee8SDavid du Colombier Xu_new->sym = context; 146*219b2ee8SDavid du Colombier Xu_new->rgt = Xu_List; 147*219b2ee8SDavid du Colombier Xu_List = Xu_new; 148*219b2ee8SDavid du Colombier 149*219b2ee8SDavid du Colombier n = m->lft; 150*219b2ee8SDavid du Colombier if (n->sym->type == STRUCT) 151*219b2ee8SDavid du Colombier setallxu(n->sym->Slst, t); 152*219b2ee8SDavid du Colombier else if (n->sym->type == CHAN) 153*219b2ee8SDavid du Colombier setonexu(n->sym, t); 154*219b2ee8SDavid du Colombier else 155*219b2ee8SDavid du Colombier { int oln = lineno; 156*219b2ee8SDavid du Colombier lineno = n->ln; Fname = n->fn; 157*219b2ee8SDavid du Colombier non_fatal("xr or xs of non-chan '%s'", 158*219b2ee8SDavid du Colombier n->sym->name); 159*219b2ee8SDavid du Colombier lineno = oln; 160*219b2ee8SDavid du Colombier } 161*219b2ee8SDavid du Colombier } 162*219b2ee8SDavid du Colombier } 163*219b2ee8SDavid du Colombier 164*219b2ee8SDavid du Colombier Lextok *Mtype = (Lextok *) 0; 165*219b2ee8SDavid du Colombier 166*219b2ee8SDavid du Colombier void 167*219b2ee8SDavid du Colombier setmtype(Lextok *m) 168*219b2ee8SDavid du Colombier { Lextok *n = m; 169*219b2ee8SDavid du Colombier int oln = lineno; 170*219b2ee8SDavid du Colombier int cnt = 1; 171*219b2ee8SDavid du Colombier 172*219b2ee8SDavid du Colombier if (n) 173*219b2ee8SDavid du Colombier { lineno = n->ln; Fname = n->fn; 174*219b2ee8SDavid du Colombier } 175*219b2ee8SDavid du Colombier 176*219b2ee8SDavid du Colombier if (Mtype) 177*219b2ee8SDavid du Colombier non_fatal("mtype redeclared", (char *)0); 178*219b2ee8SDavid du Colombier 179*219b2ee8SDavid du Colombier Mtype = n; 180*219b2ee8SDavid du Colombier 181*219b2ee8SDavid du Colombier while (n) /* syntax check */ 182*219b2ee8SDavid du Colombier { if (!n->lft || !n->lft->sym 183*219b2ee8SDavid du Colombier || (n->lft->ntyp != NAME) 184*219b2ee8SDavid du Colombier || n->lft->lft) /* indexed variable */ 185*219b2ee8SDavid du Colombier fatal("bad mtype definition", (char *)0); 186*219b2ee8SDavid du Colombier 187*219b2ee8SDavid du Colombier /* label the name */ 188*219b2ee8SDavid du Colombier n->lft->sym->type = MTYPE; 189*219b2ee8SDavid du Colombier n->lft->sym->ini = nn(ZN,CONST,ZN,ZN); 190*219b2ee8SDavid du Colombier n->lft->sym->ini->val = cnt; 191*219b2ee8SDavid du Colombier n = n->rgt; 192*219b2ee8SDavid du Colombier cnt++; 193*219b2ee8SDavid du Colombier } 194*219b2ee8SDavid du Colombier lineno = oln; 195*219b2ee8SDavid du Colombier } 196*219b2ee8SDavid du Colombier 197*219b2ee8SDavid du Colombier int 198*219b2ee8SDavid du Colombier ismtype(char *str) 199*219b2ee8SDavid du Colombier { Lextok *n; 200*219b2ee8SDavid du Colombier int cnt = 1; 201*219b2ee8SDavid du Colombier 202*219b2ee8SDavid du Colombier for (n = Mtype; n; n = n->rgt) 203*219b2ee8SDavid du Colombier { if (strcmp(str, n->lft->sym->name) == 0) 204*219b2ee8SDavid du Colombier return cnt; 205*219b2ee8SDavid du Colombier cnt++; 206*219b2ee8SDavid du Colombier } 207*219b2ee8SDavid du Colombier return 0; 208*219b2ee8SDavid du Colombier } 209*219b2ee8SDavid du Colombier 210*219b2ee8SDavid du Colombier int 211*219b2ee8SDavid du Colombier sputtype(char *foo, int m) 212*219b2ee8SDavid du Colombier { 213*219b2ee8SDavid du Colombier switch (m) { 214*219b2ee8SDavid du Colombier case BIT: strcpy(foo, "bit "); break; 215*219b2ee8SDavid du Colombier case BYTE: strcpy(foo, "byte "); break; 216*219b2ee8SDavid du Colombier case CHAN: strcpy(foo, "chan "); break; 217*219b2ee8SDavid du Colombier case SHORT: strcpy(foo, "short "); break; 218*219b2ee8SDavid du Colombier case INT: strcpy(foo, "int "); break; 219*219b2ee8SDavid du Colombier case MTYPE: strcpy(foo, "mtype "); break; 220*219b2ee8SDavid du Colombier case STRUCT: strcpy(foo, "struct"); break; 221*219b2ee8SDavid du Colombier case PROCTYPE: strcpy(foo, "proctype"); break; 222*219b2ee8SDavid du Colombier case LABEL: strcpy(foo, "label "); return 0; 223*219b2ee8SDavid du Colombier default: strcpy(foo, "value "); return 0; 224*219b2ee8SDavid du Colombier } 225*219b2ee8SDavid du Colombier return 1; 226*219b2ee8SDavid du Colombier } 227*219b2ee8SDavid du Colombier 228*219b2ee8SDavid du Colombier 229*219b2ee8SDavid du Colombier int 230*219b2ee8SDavid du Colombier puttype(int m) 231*219b2ee8SDavid du Colombier { char buf[32]; 232*219b2ee8SDavid du Colombier 233*219b2ee8SDavid du Colombier if (sputtype(buf, m)) 234*219b2ee8SDavid du Colombier { printf("%s", buf); 235*219b2ee8SDavid du Colombier return 1; 236*219b2ee8SDavid du Colombier } 237*219b2ee8SDavid du Colombier return 0; 238*219b2ee8SDavid du Colombier } 239*219b2ee8SDavid du Colombier 240*219b2ee8SDavid du Colombier void 241*219b2ee8SDavid du Colombier symvar(Symbol *sp) 242*219b2ee8SDavid du Colombier { Lextok *m; 243*219b2ee8SDavid du Colombier 244*219b2ee8SDavid du Colombier if (!puttype(sp->type)) 245*219b2ee8SDavid du Colombier return; 246*219b2ee8SDavid du Colombier 247*219b2ee8SDavid du Colombier printf("\t"); 248*219b2ee8SDavid du Colombier if (sp->owner) printf("%s.", sp->owner->name); 249*219b2ee8SDavid du Colombier printf("%s", sp->name); 250*219b2ee8SDavid du Colombier if (sp->nel > 1) printf("[%d]", sp->nel); 251*219b2ee8SDavid du Colombier 252*219b2ee8SDavid du Colombier if (sp->type == CHAN) 253*219b2ee8SDavid du Colombier printf("\t%d", (sp->ini)?sp->ini->val:0); 254*219b2ee8SDavid du Colombier else 255*219b2ee8SDavid du Colombier printf("\t%d", eval(sp->ini)); 256*219b2ee8SDavid du Colombier 257*219b2ee8SDavid du Colombier if (sp->owner) 258*219b2ee8SDavid du Colombier printf("\t<struct-field>"); 259*219b2ee8SDavid du Colombier else 260*219b2ee8SDavid du Colombier if (!sp->context) 261*219b2ee8SDavid du Colombier printf("\t<global>"); 262*219b2ee8SDavid du Colombier else 263*219b2ee8SDavid du Colombier printf("\t<%s>", sp->context->name); 264*219b2ee8SDavid du Colombier 265*219b2ee8SDavid du Colombier if (sp->Nid < 0) /* formal parameter */ 266*219b2ee8SDavid du Colombier printf("\t<parameter %d>", -(sp->Nid)); 267*219b2ee8SDavid du Colombier else 268*219b2ee8SDavid du Colombier printf("\t<variable>"); 269*219b2ee8SDavid du Colombier if (sp->type == CHAN && sp->ini) 270*219b2ee8SDavid du Colombier { int i; 271*219b2ee8SDavid du Colombier for (m = sp->ini->rgt, i = 0; m; m = m->rgt) 272*219b2ee8SDavid du Colombier i++; 273*219b2ee8SDavid du Colombier printf("\t%d\t", i); 274*219b2ee8SDavid du Colombier for (m = sp->ini->rgt; m; m = m->rgt) 275*219b2ee8SDavid du Colombier { (void) puttype(m->ntyp); 276*219b2ee8SDavid du Colombier if (m->rgt) printf("\t"); 277*219b2ee8SDavid du Colombier } 278*219b2ee8SDavid du Colombier } 279*219b2ee8SDavid du Colombier printf("\n"); 280*219b2ee8SDavid du Colombier } 281*219b2ee8SDavid du Colombier 282*219b2ee8SDavid du Colombier void 283*219b2ee8SDavid du Colombier symdump(void) 284*219b2ee8SDavid du Colombier { Symbol *sp; 285*219b2ee8SDavid du Colombier int i; 286*219b2ee8SDavid du Colombier 287*219b2ee8SDavid du Colombier for (i = 0; i <= Nhash; i++) 288*219b2ee8SDavid du Colombier for (sp = symtab[i]; sp; sp = sp->next) 289*219b2ee8SDavid du Colombier symvar(sp); 290*219b2ee8SDavid du Colombier } 291