1 /***** spin: sym.c *****/
2
3 /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
4 /* All Rights Reserved. This software is for educational purposes only. */
5 /* No guarantee whatsoever is expressed or implied by the distribution of */
6 /* this code. Permission is given to distribute this code provided that */
7 /* this introductory message is not removed and no monies are exchanged. */
8 /* Software written by Gerard J. Holzmann. For tool documentation see: */
9 /* http://spinroot.com/ */
10 /* Send all bug-reports and/or questions to: bugs@spinroot.com */
11
12 #include "spin.h"
13 #include "y.tab.h"
14
15 extern Symbol *Fname, *owner;
16 extern int lineno, depth, verbose, NamesNotAdded, deadvar;
17 extern int has_hidden, m_loss, old_scope_rules;
18 extern short has_xu;
19 extern char CurScope[MAXSCOPESZ];
20
21 Symbol *context = ZS;
22 Ordered *all_names = (Ordered *)0;
23 int Nid = 0;
24
25 Lextok *Mtype = (Lextok *) 0;
26
27 static Ordered *last_name = (Ordered *)0;
28 static Symbol *symtab[Nhash+1];
29 static Lextok *runstmnts = ZN;
30
31 static int
samename(Symbol * a,Symbol * b)32 samename(Symbol *a, Symbol *b)
33 {
34 if (!a && !b) return 1;
35 if (!a || !b) return 0;
36 return !strcmp(a->name, b->name);
37 }
38
39 int
hash(char * s)40 hash(char *s)
41 { int h=0;
42
43 while (*s)
44 { h += *s++;
45 h <<= 1;
46 if (h&(Nhash+1))
47 h |= 1;
48 }
49 return h&Nhash;
50 }
51
52 void
disambiguate(void)53 disambiguate(void)
54 { Ordered *walk;
55 Symbol *sp;
56
57 if (old_scope_rules)
58 return;
59
60 /* if the same name appears in two different scopes,
61 prepend the scope_prefix to the names */
62
63 for (walk = all_names; walk; walk = walk->next)
64 { sp = walk->entry;
65 if (sp->type != 0
66 && sp->type != LABEL
67 && strlen((const char *)sp->bscp) > 1)
68 { char *n = (char *) emalloc(strlen((const char *)sp->name)
69 + strlen((const char *)sp->bscp) + 1);
70 sprintf(n, "%s%s", sp->bscp, sp->name);
71 sp->name = n; /* discord the old memory */
72 } }
73 }
74
75 Symbol *
lookup(char * s)76 lookup(char *s)
77 { Symbol *sp; Ordered *no;
78 int h = hash(s);
79
80 if (old_scope_rules)
81 { /* same scope - global refering to global or local to local */
82 for (sp = symtab[h]; sp; sp = sp->next)
83 { if (strcmp(sp->name, s) == 0
84 && samename(sp->context, context)
85 && samename(sp->owner, owner))
86 { return sp; /* found */
87 } }
88 } else
89 { /* added 6.0.0: more traditional, scope rule */
90 for (sp = symtab[h]; sp; sp = sp->next)
91 { if (strcmp(sp->name, s) == 0
92 && samename(sp->context, context)
93 && (strcmp((const char *)sp->bscp, CurScope) == 0
94 || strncmp((const char *)sp->bscp, CurScope, strlen((const char *)sp->bscp)) == 0)
95 && samename(sp->owner, owner))
96 {
97 if (!samename(sp->owner, owner))
98 { printf("spin: different container %s\n", sp->name);
99 printf(" old: %s\n", sp->owner?sp->owner->name:"--");
100 printf(" new: %s\n", owner?owner->name:"--");
101 /* alldone(1); */
102 }
103 return sp; /* found */
104 } } }
105
106 if (context) /* in proctype, refers to global */
107 for (sp = symtab[h]; sp; sp = sp->next)
108 { if (strcmp(sp->name, s) == 0
109 && !sp->context
110 && samename(sp->owner, owner))
111 { return sp; /* global */
112 } }
113
114 sp = (Symbol *) emalloc(sizeof(Symbol));
115 sp->name = (char *) emalloc(strlen(s) + 1);
116 strcpy(sp->name, s);
117 sp->nel = 1;
118 sp->setat = depth;
119 sp->context = context;
120 sp->owner = owner; /* if fld in struct */
121 sp->bscp = (unsigned char *) emalloc(strlen((const char *)CurScope)+1);
122 strcpy((char *)sp->bscp, CurScope);
123
124 if (NamesNotAdded == 0)
125 { sp->next = symtab[h];
126 symtab[h] = sp;
127 no = (Ordered *) emalloc(sizeof(Ordered));
128 no->entry = sp;
129 if (!last_name)
130 last_name = all_names = no;
131 else
132 { last_name->next = no;
133 last_name = no;
134 } }
135
136 return sp;
137 }
138
139 void
trackvar(Lextok * n,Lextok * m)140 trackvar(Lextok *n, Lextok *m)
141 { Symbol *sp = n->sym;
142
143 if (!sp) return; /* a structure list */
144 switch (m->ntyp) {
145 case NAME:
146 if (m->sym->type != BIT)
147 { sp->hidden |= 4;
148 if (m->sym->type != BYTE)
149 sp->hidden |= 8;
150 }
151 break;
152 case CONST:
153 if (m->val != 0 && m->val != 1)
154 sp->hidden |= 4;
155 if (m->val < 0 || m->val > 256)
156 sp->hidden |= 8; /* ditto byte-equiv */
157 break;
158 default: /* unknown */
159 sp->hidden |= (4|8); /* not known bit-equiv */
160 }
161 }
162
163 void
trackrun(Lextok * n)164 trackrun(Lextok *n)
165 {
166 runstmnts = nn(ZN, 0, n, runstmnts);
167 }
168
169 void
checkrun(Symbol * parnm,int posno)170 checkrun(Symbol *parnm, int posno)
171 { Lextok *n, *now, *v; int i, m;
172 int res = 0; char buf[16], buf2[16];
173
174 for (n = runstmnts; n; n = n->rgt)
175 { now = n->lft;
176 if (now->sym != parnm->context)
177 continue;
178 for (v = now->lft, i = 0; v; v = v->rgt, i++)
179 if (i == posno)
180 { m = v->lft->ntyp;
181 if (m == CONST)
182 { m = v->lft->val;
183 if (m != 0 && m != 1)
184 res |= 4;
185 if (m < 0 || m > 256)
186 res |= 8;
187 } else if (m == NAME)
188 { m = v->lft->sym->type;
189 if (m != BIT)
190 { res |= 4;
191 if (m != BYTE)
192 res |= 8;
193 }
194 } else
195 res |= (4|8); /* unknown */
196 break;
197 } }
198 if (!(res&4) || !(res&8))
199 { if (!(verbose&32)) return;
200 strcpy(buf2, (!(res&4))?"bit":"byte");
201 sputtype(buf, parnm->type);
202 i = (int) strlen(buf);
203 while (i > 0 && buf[--i] == ' ') buf[i] = '\0';
204 if (i == 0 || strcmp(buf, buf2) == 0) return;
205 prehint(parnm);
206 printf("proctype %s, '%s %s' could be declared",
207 parnm->context?parnm->context->name:"", buf, parnm->name);
208 printf(" '%s %s'\n", buf2, parnm->name);
209 }
210 }
211
212 void
trackchanuse(Lextok * m,Lextok * w,int t)213 trackchanuse(Lextok *m, Lextok *w, int t)
214 { Lextok *n = m; int cnt = 1;
215 while (n)
216 { if (n->lft
217 && n->lft->sym
218 && n->lft->sym->type == CHAN)
219 setaccess(n->lft->sym, w?w->sym:ZS, cnt, t);
220 n = n->rgt; cnt++;
221 }
222 }
223
224 void
setptype(Lextok * n,int t,Lextok * vis)225 setptype(Lextok *n, int t, Lextok *vis) /* predefined types */
226 { int oln = lineno, cnt = 1; extern int Expand_Ok;
227
228 while (n)
229 { if (n->sym->type && !(n->sym->hidden&32))
230 { lineno = n->ln; Fname = n->fn;
231 fatal("redeclaration of '%s'", n->sym->name);
232 lineno = oln;
233 }
234 n->sym->type = (short) t;
235
236 if (Expand_Ok)
237 { n->sym->hidden |= (4|8|16); /* formal par */
238 if (t == CHAN)
239 setaccess(n->sym, ZS, cnt, 'F');
240 }
241 if (t == UNSIGNED)
242 { if (n->sym->nbits < 0 || n->sym->nbits >= 32)
243 fatal("(%s) has invalid width-field", n->sym->name);
244 if (n->sym->nbits == 0)
245 { n->sym->nbits = 16;
246 non_fatal("unsigned without width-field", 0);
247 }
248 } else if (n->sym->nbits > 0)
249 { non_fatal("(%s) only an unsigned can have width-field",
250 n->sym->name);
251 }
252 if (vis)
253 { if (strncmp(vis->sym->name, ":hide:", (size_t) 6) == 0)
254 { n->sym->hidden |= 1;
255 has_hidden++;
256 if (t == BIT)
257 fatal("bit variable (%s) cannot be hidden",
258 n->sym->name);
259 } else if (strncmp(vis->sym->name, ":show:", (size_t) 6) == 0)
260 { n->sym->hidden |= 2;
261 } else if (strncmp(vis->sym->name, ":local:", (size_t) 7) == 0)
262 { n->sym->hidden |= 64;
263 }
264 }
265 if (t == CHAN)
266 n->sym->Nid = ++Nid;
267 else
268 { n->sym->Nid = 0;
269 if (n->sym->ini
270 && n->sym->ini->ntyp == CHAN)
271 { Fname = n->fn;
272 lineno = n->ln;
273 fatal("chan initializer for non-channel %s",
274 n->sym->name);
275 }
276 }
277 if (n->sym->nel <= 0)
278 { lineno = n->ln; Fname = n->fn;
279 non_fatal("bad array size for '%s'", n->sym->name);
280 lineno = oln;
281 }
282 n = n->rgt; cnt++;
283 }
284 }
285
286 static void
setonexu(Symbol * sp,int t)287 setonexu(Symbol *sp, int t)
288 {
289 sp->xu |= t;
290 if (t == XR || t == XS)
291 { if (sp->xup[t-1]
292 && strcmp(sp->xup[t-1]->name, context->name))
293 { printf("error: x[rs] claims from %s and %s\n",
294 sp->xup[t-1]->name, context->name);
295 non_fatal("conflicting claims on chan '%s'",
296 sp->name);
297 }
298 sp->xup[t-1] = context;
299 }
300 }
301
302 static void
setallxu(Lextok * n,int t)303 setallxu(Lextok *n, int t)
304 { Lextok *fp, *tl;
305
306 for (fp = n; fp; fp = fp->rgt)
307 for (tl = fp->lft; tl; tl = tl->rgt)
308 { if (tl->sym->type == STRUCT)
309 setallxu(tl->sym->Slst, t);
310 else if (tl->sym->type == CHAN)
311 setonexu(tl->sym, t);
312 }
313 }
314
315 Lextok *Xu_List = (Lextok *) 0;
316
317 void
setxus(Lextok * p,int t)318 setxus(Lextok *p, int t)
319 { Lextok *m, *n;
320
321 has_xu = 1;
322
323 if (m_loss && t == XS)
324 { printf("spin: warning, %s:%d, xs tag not compatible with -m (message loss)\n",
325 (p->fn != NULL) ? p->fn->name : "stdin", p->ln);
326 }
327
328 if (!context)
329 { lineno = p->ln;
330 Fname = p->fn;
331 fatal("non-local x[rs] assertion", (char *)0);
332 }
333 for (m = p; m; m = m->rgt)
334 { Lextok *Xu_new = (Lextok *) emalloc(sizeof(Lextok));
335 Xu_new->uiid = p->uiid;
336 Xu_new->val = t;
337 Xu_new->lft = m->lft;
338 Xu_new->sym = context;
339 Xu_new->rgt = Xu_List;
340 Xu_List = Xu_new;
341
342 n = m->lft;
343 if (n->sym->type == STRUCT)
344 setallxu(n->sym->Slst, t);
345 else if (n->sym->type == CHAN)
346 setonexu(n->sym, t);
347 else
348 { int oln = lineno;
349 lineno = n->ln; Fname = n->fn;
350 non_fatal("xr or xs of non-chan '%s'",
351 n->sym->name);
352 lineno = oln;
353 }
354 }
355 }
356
357 void
setmtype(Lextok * m)358 setmtype(Lextok *m)
359 { Lextok *n;
360 int cnt, oln = lineno;
361
362 if (m) { lineno = m->ln; Fname = m->fn; }
363
364 if (!Mtype)
365 Mtype = m;
366 else
367 { for (n = Mtype; n->rgt; n = n->rgt)
368 ;
369 n->rgt = m; /* concatenate */
370 }
371
372 for (n = Mtype, cnt = 1; n; n = n->rgt, cnt++) /* syntax check */
373 { if (!n->lft || !n->lft->sym
374 || n->lft->ntyp != NAME
375 || n->lft->lft) /* indexed variable */
376 fatal("bad mtype definition", (char *)0);
377
378 /* label the name */
379 if (n->lft->sym->type != MTYPE)
380 { n->lft->sym->hidden |= 128; /* is used */
381 n->lft->sym->type = MTYPE;
382 n->lft->sym->ini = nn(ZN,CONST,ZN,ZN);
383 n->lft->sym->ini->val = cnt;
384 } else if (n->lft->sym->ini->val != cnt)
385 non_fatal("name %s appears twice in mtype declaration",
386 n->lft->sym->name);
387 }
388 lineno = oln;
389 if (cnt > 256)
390 fatal("too many mtype elements (>255)", (char *)0);
391 }
392
393 int
ismtype(char * str)394 ismtype(char *str) /* name to number */
395 { Lextok *n;
396 int cnt = 1;
397
398 for (n = Mtype; n; n = n->rgt)
399 { if (strcmp(str, n->lft->sym->name) == 0)
400 return cnt;
401 cnt++;
402 }
403 return 0;
404 }
405
406 int
sputtype(char * foo,int m)407 sputtype(char *foo, int m)
408 {
409 switch (m) {
410 case UNSIGNED: strcpy(foo, "unsigned "); break;
411 case BIT: strcpy(foo, "bit "); break;
412 case BYTE: strcpy(foo, "byte "); break;
413 case CHAN: strcpy(foo, "chan "); break;
414 case SHORT: strcpy(foo, "short "); break;
415 case INT: strcpy(foo, "int "); break;
416 case MTYPE: strcpy(foo, "mtype "); break;
417 case STRUCT: strcpy(foo, "struct"); break;
418 case PROCTYPE: strcpy(foo, "proctype"); break;
419 case LABEL: strcpy(foo, "label "); return 0;
420 default: strcpy(foo, "value "); return 0;
421 }
422 return 1;
423 }
424
425
426 static int
puttype(int m)427 puttype(int m)
428 { char buf[128];
429
430 if (sputtype(buf, m))
431 { printf("%s", buf);
432 return 1;
433 }
434 return 0;
435 }
436
437 void
symvar(Symbol * sp)438 symvar(Symbol *sp)
439 { Lextok *m;
440
441 if (!puttype(sp->type))
442 return;
443
444 printf("\t");
445 if (sp->owner) printf("%s.", sp->owner->name);
446 printf("%s", sp->name);
447 if (sp->nel > 1 || sp->isarray == 1) printf("[%d]", sp->nel);
448
449 if (sp->type == CHAN)
450 printf("\t%d", (sp->ini)?sp->ini->val:0);
451 else if (sp->type == STRUCT && sp->Snm != NULL) /* Frank Weil, 2.9.8 */
452 printf("\t%s", sp->Snm->name);
453 else
454 printf("\t%d", eval(sp->ini));
455
456 if (sp->owner)
457 printf("\t<:struct-field:>");
458 else
459 if (!sp->context)
460 printf("\t<:global:>");
461 else
462 printf("\t<%s>", sp->context->name);
463
464 if (sp->Nid < 0) /* formal parameter */
465 printf("\t<parameter %d>", -(sp->Nid));
466 else if (sp->type == MTYPE)
467 printf("\t<constant>");
468 else if (sp->isarray)
469 printf("\t<array>");
470 else
471 printf("\t<variable>");
472
473 if (sp->type == CHAN && sp->ini)
474 { int i;
475 for (m = sp->ini->rgt, i = 0; m; m = m->rgt)
476 i++;
477 printf("\t%d\t", i);
478 for (m = sp->ini->rgt; m; m = m->rgt)
479 { if (m->ntyp == STRUCT)
480 printf("struct %s", m->sym->name);
481 else
482 (void) puttype(m->ntyp);
483 if (m->rgt) printf("\t");
484 }
485 }
486
487 if (1) printf("\t{scope %s}", sp->bscp);
488
489 printf("\n");
490 }
491
492 void
symdump(void)493 symdump(void)
494 { Ordered *walk;
495
496 for (walk = all_names; walk; walk = walk->next)
497 symvar(walk->entry);
498 }
499
500 void
chname(Symbol * sp)501 chname(Symbol *sp)
502 { printf("chan ");
503 if (sp->context) printf("%s-", sp->context->name);
504 if (sp->owner) printf("%s.", sp->owner->name);
505 printf("%s", sp->name);
506 if (sp->nel > 1 || sp->isarray == 1) printf("[%d]", sp->nel);
507 printf("\t");
508 }
509
510 static struct X {
511 int typ; char *nm;
512 } xx[] = {
513 { 'A', "exported as run parameter" },
514 { 'F', "imported as proctype parameter" },
515 { 'L', "used as l-value in asgnmnt" },
516 { 'V', "used as r-value in asgnmnt" },
517 { 'P', "polled in receive stmnt" },
518 { 'R', "used as parameter in receive stmnt" },
519 { 'S', "used as parameter in send stmnt" },
520 { 'r', "received from" },
521 { 's', "sent to" },
522 };
523
524 static void
chan_check(Symbol * sp)525 chan_check(Symbol *sp)
526 { Access *a; int i, b=0, d;
527
528 if (verbose&1) goto report; /* -C -g */
529
530 for (a = sp->access; a; a = a->lnk)
531 if (a->typ == 'r')
532 b |= 1;
533 else if (a->typ == 's')
534 b |= 2;
535 if (b == 3 || (sp->hidden&16)) /* balanced or formal par */
536 return;
537 report:
538 chname(sp);
539 for (i = d = 0; i < (int) (sizeof(xx)/sizeof(struct X)); i++)
540 { b = 0;
541 for (a = sp->access; a; a = a->lnk)
542 if (a->typ == xx[i].typ) b++;
543 if (b == 0) continue; d++;
544 printf("\n\t%s by: ", xx[i].nm);
545 for (a = sp->access; a; a = a->lnk)
546 if (a->typ == xx[i].typ)
547 { printf("%s", a->who->name);
548 if (a->what) printf(" to %s", a->what->name);
549 if (a->cnt) printf(" par %d", a->cnt);
550 if (--b > 0) printf(", ");
551 }
552 }
553 printf("%s\n", (!d)?"\n\tnever used under this name":"");
554 }
555
556 void
chanaccess(void)557 chanaccess(void)
558 { Ordered *walk;
559 char buf[128];
560 extern int Caccess, separate;
561 extern short has_code;
562
563 for (walk = all_names; walk; walk = walk->next)
564 { if (!walk->entry->owner)
565 switch (walk->entry->type) {
566 case CHAN:
567 if (Caccess) chan_check(walk->entry);
568 break;
569 case MTYPE:
570 case BIT:
571 case BYTE:
572 case SHORT:
573 case INT:
574 case UNSIGNED:
575 if ((walk->entry->hidden&128)) /* was: 32 */
576 continue;
577
578 if (!separate
579 && !walk->entry->context
580 && !has_code
581 && deadvar)
582 walk->entry->hidden |= 1; /* auto-hide */
583
584 if (!(verbose&32) || has_code) continue;
585
586 printf("spin: warning, %s, ", Fname->name);
587 sputtype(buf, walk->entry->type);
588 if (walk->entry->context)
589 printf("proctype %s",
590 walk->entry->context->name);
591 else
592 printf("global");
593 printf(", '%s%s' variable is never used\n",
594 buf, walk->entry->name);
595 } }
596 }
597