sym.c 12 KB

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