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