vars.c 8.8 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367
  1. /*
  2. * This file is part of the UCB release of Plan 9. It is subject to the license
  3. * terms in the LICENSE file found in the top-level directory of this
  4. * distribution and at http://akaros.cs.berkeley.edu/files/Plan9License. No
  5. * part of the UCB release of Plan 9, including this file, may be copied,
  6. * modified, propagated, or distributed except according to the terms contained
  7. * in the LICENSE file.
  8. */
  9. /***** spin: vars.c *****/
  10. /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
  11. /* All Rights Reserved. This software is for educational purposes only. */
  12. /* No guarantee whatsoever is expressed or implied by the distribution of */
  13. /* this code. Permission is given to distribute this code provided that */
  14. /* this introductory message is not removed and no monies are exchanged. */
  15. /* Software written by Gerard J. Holzmann. For tool documentation see: */
  16. /* http://spinroot.com/ */
  17. /* Send all bug-reports and/or questions to: bugs@spinroot.com */
  18. #include "spin.h"
  19. #include "y.tab.h"
  20. extern Ordered *all_names;
  21. extern RunList *X, *LastX;
  22. extern Symbol *Fname;
  23. extern char Buf[];
  24. extern int lineno, depth, verbose, xspin, limited_vis;
  25. extern int analyze, jumpsteps, nproc, nstop, columns;
  26. extern int16_t no_arrays, Have_claim;
  27. extern void sr_mesg(FILE *, int, int);
  28. extern void sr_buf(int, int);
  29. static int getglobal(Lextok *);
  30. static int setglobal(Lextok *, int);
  31. static int maxcolnr = 1;
  32. int
  33. getval(Lextok *sn)
  34. { Symbol *s = sn->sym;
  35. if (strcmp(s->name, "_") == 0)
  36. { non_fatal("attempt to read value of '_'", 0);
  37. return 0;
  38. }
  39. if (strcmp(s->name, "_last") == 0)
  40. return (LastX)?LastX->pid:0;
  41. if (strcmp(s->name, "_p") == 0)
  42. return (X && X->pc)?X->pc->seqno:0;
  43. if (strcmp(s->name, "_pid") == 0)
  44. { if (!X) return 0;
  45. return X->pid - Have_claim;
  46. }
  47. if (strcmp(s->name, "_nr_pr") == 0)
  48. return nproc-nstop; /* new 3.3.10 */
  49. if (s->context && s->type)
  50. return getlocal(sn);
  51. if (!s->type) /* not declared locally */
  52. { s = lookup(s->name); /* try global */
  53. sn->sym = s; /* fix it */
  54. }
  55. return getglobal(sn);
  56. }
  57. int
  58. setval(Lextok *v, int n)
  59. {
  60. if (v->sym->context && v->sym->type)
  61. return setlocal(v, n);
  62. if (!v->sym->type)
  63. v->sym = lookup(v->sym->name);
  64. return setglobal(v, n);
  65. }
  66. void
  67. rm_selfrefs(Symbol *s, Lextok *i)
  68. {
  69. if (!i) return;
  70. if (i->ntyp == NAME
  71. && strcmp(i->sym->name, s->name) == 0
  72. && ( (!i->sym->context && !s->context)
  73. || ( i->sym->context && s->context
  74. && strcmp(i->sym->context->name, s->context->name) == 0)))
  75. { lineno = i->ln;
  76. Fname = i->fn;
  77. non_fatal("self-reference initializing '%s'", s->name);
  78. i->ntyp = CONST;
  79. i->val = 0;
  80. } else
  81. { rm_selfrefs(s, i->lft);
  82. rm_selfrefs(s, i->rgt);
  83. }
  84. }
  85. int
  86. checkvar(Symbol *s, int n)
  87. { int i, oln = lineno; /* calls on eval() change it */
  88. Symbol *ofnm = Fname;
  89. if (!in_bound(s, n))
  90. return 0;
  91. if (s->type == 0)
  92. { non_fatal("undecl var %s (assuming int)", s->name);
  93. s->type = INT;
  94. }
  95. /* not a STRUCT */
  96. if (s->val == (int *) 0) /* uninitialized */
  97. { s->val = (int *) emalloc(s->nel*sizeof(int));
  98. for (i = 0; i < s->nel; i++)
  99. { if (s->type != CHAN)
  100. { rm_selfrefs(s, s->ini);
  101. s->val[i] = eval(s->ini);
  102. } else if (!analyze)
  103. s->val[i] = qmake(s);
  104. } }
  105. lineno = oln;
  106. Fname = ofnm;
  107. return 1;
  108. }
  109. static int
  110. getglobal(Lextok *sn)
  111. { Symbol *s = sn->sym;
  112. int i, n = eval(sn->lft);
  113. if (s->type == 0 && X && (i = find_lab(s, X->n, 0)))
  114. { printf("findlab through getglobal on %s\n", s->name);
  115. return i; /* can this happen? */
  116. }
  117. if (s->type == STRUCT)
  118. return Rval_struct(sn, s, 1); /* 1 = check init */
  119. if (checkvar(s, n))
  120. return cast_val(s->type, s->val[n], s->nbits);
  121. return 0;
  122. }
  123. int
  124. cast_val(int t, int v, int w)
  125. { int i=0; int16_t s=0; unsigned int u=0;
  126. if (t == PREDEF || t == INT || t == CHAN) i = v; /* predef means _ */
  127. else if (t == SHORT) s = (int16_t) v;
  128. else if (t == BYTE || t == MTYPE) u = (unsigned char)v;
  129. else if (t == BIT) u = (unsigned char)(v&1);
  130. else if (t == UNSIGNED)
  131. { if (w == 0)
  132. fatal("cannot happen, cast_val", (char *)0);
  133. /* u = (unsigned)(v& ((1<<w)-1)); problem when w=32 */
  134. u = (unsigned)(v& (~0u>>(8*sizeof(unsigned)-w))); /* doug */
  135. }
  136. if (v != i+s+ (int) u)
  137. { char buf[64]; sprintf(buf, "%d->%d (%d)", v, i+s+u, t);
  138. non_fatal("value (%s) truncated in assignment", buf);
  139. }
  140. return (int)(i+s+u);
  141. }
  142. static int
  143. setglobal(Lextok *v, int m)
  144. {
  145. if (v->sym->type == STRUCT)
  146. (void) Lval_struct(v, v->sym, 1, m);
  147. else
  148. { int n = eval(v->lft);
  149. if (checkvar(v->sym, n))
  150. { int oval = v->sym->val[n];
  151. int nval = cast_val(v->sym->type, m, v->sym->nbits);
  152. v->sym->val[n] = nval;
  153. if (oval != nval)
  154. { v->sym->setat = depth;
  155. } } }
  156. return 1;
  157. }
  158. void
  159. dumpclaims(FILE *fd, int pid, char *s)
  160. { extern Lextok *Xu_List; extern int Pid;
  161. extern int16_t terse;
  162. Lextok *m; int cnt = 0; int oPid = Pid;
  163. for (m = Xu_List; m; m = m->rgt)
  164. if (strcmp(m->sym->name, s) == 0)
  165. { cnt=1;
  166. break;
  167. }
  168. if (cnt == 0) return;
  169. Pid = pid;
  170. fprintf(fd, "#ifndef XUSAFE\n");
  171. for (m = Xu_List; m; m = m->rgt)
  172. { if (strcmp(m->sym->name, s) != 0)
  173. continue;
  174. no_arrays = 1;
  175. putname(fd, "\t\tsetq_claim(", m->lft, 0, "");
  176. no_arrays = 0;
  177. fprintf(fd, ", %d, ", m->val);
  178. terse = 1;
  179. putname(fd, "\"", m->lft, 0, "\", h, ");
  180. terse = 0;
  181. fprintf(fd, "\"%s\");\n", s);
  182. }
  183. fprintf(fd, "#endif\n");
  184. Pid = oPid;
  185. }
  186. void
  187. dumpglobals(void)
  188. { Ordered *walk;
  189. static Lextok *dummy = ZN;
  190. Symbol *sp;
  191. int j;
  192. if (!dummy)
  193. dummy = nn(ZN, NAME, nn(ZN,CONST,ZN,ZN), ZN);
  194. for (walk = all_names; walk; walk = walk->next)
  195. { sp = walk->entry;
  196. if (!sp->type || sp->context || sp->owner
  197. || sp->type == PROCTYPE || sp->type == PREDEF
  198. || sp->type == CODE_FRAG || sp->type == CODE_DECL
  199. || (sp->type == MTYPE && ismtype(sp->name)))
  200. continue;
  201. if (sp->type == STRUCT)
  202. { if ((verbose&4) && !(verbose&64)
  203. && (sp->setat < depth
  204. && jumpsteps != depth))
  205. { continue;
  206. }
  207. dump_struct(sp, sp->name, 0);
  208. continue;
  209. }
  210. for (j = 0; j < sp->nel; j++)
  211. { int prefetch;
  212. if (sp->type == CHAN)
  213. { doq(sp, j, 0);
  214. continue;
  215. }
  216. if ((verbose&4) && !(verbose&64)
  217. && (sp->setat < depth
  218. && jumpsteps != depth))
  219. { continue;
  220. }
  221. dummy->sym = sp;
  222. dummy->lft->val = j;
  223. /* in case of cast_val warnings, do this first: */
  224. prefetch = getglobal(dummy);
  225. printf("\t\t%s", sp->name);
  226. if (sp->nel > 1 || sp->isarray) printf("[%d]", j);
  227. printf(" = ");
  228. sr_mesg(stdout, prefetch,
  229. sp->type == MTYPE);
  230. printf("\n");
  231. if (limited_vis && (sp->hidden&2))
  232. { int colpos;
  233. Buf[0] = '\0';
  234. if (!xspin)
  235. { if (columns == 2)
  236. sprintf(Buf, "~G%s = ", sp->name);
  237. else
  238. sprintf(Buf, "%s = ", sp->name);
  239. }
  240. sr_buf(prefetch, sp->type == MTYPE);
  241. if (sp->colnr == 0)
  242. { sp->colnr = maxcolnr;
  243. maxcolnr = 1+(maxcolnr%10);
  244. }
  245. colpos = nproc+sp->colnr-1;
  246. if (columns == 2)
  247. { pstext(colpos, Buf);
  248. continue;
  249. }
  250. if (!xspin)
  251. { printf("\t\t%s\n", Buf);
  252. continue;
  253. }
  254. printf("MSC: ~G %s %s\n", sp->name, Buf);
  255. printf("%3d:\tproc %3d (TRACK) line 1 \"var\" ",
  256. depth, colpos);
  257. printf("(state 0)\t[printf('MSC: globvar\\\\n')]\n");
  258. printf("\t\t%s", sp->name);
  259. if (sp->nel > 1 || sp->isarray) printf("[%d]", j);
  260. printf(" = %s\n", Buf);
  261. } } }
  262. }
  263. void
  264. dumplocal(RunList *r)
  265. { static Lextok *dummy = ZN;
  266. Symbol *z, *s;
  267. int i;
  268. if (!r) return;
  269. s = r->symtab;
  270. if (!dummy)
  271. dummy = nn(ZN, NAME, nn(ZN,CONST,ZN,ZN), ZN);
  272. for (z = s; z; z = z->next)
  273. { if (z->type == STRUCT)
  274. { dump_struct(z, z->name, r);
  275. continue;
  276. }
  277. for (i = 0; i < z->nel; i++)
  278. { if (z->type == CHAN)
  279. { doq(z, i, r);
  280. continue;
  281. }
  282. if ((verbose&4) && !(verbose&64)
  283. && (z->setat < depth
  284. && jumpsteps != depth))
  285. continue;
  286. dummy->sym = z;
  287. dummy->lft->val = i;
  288. printf("\t\t%s(%d):%s",
  289. r->n->name, r->pid - Have_claim, z->name);
  290. if (z->nel > 1 || z->isarray) printf("[%d]", i);
  291. printf(" = ");
  292. sr_mesg(stdout, getval(dummy), z->type == MTYPE);
  293. printf("\n");
  294. if (limited_vis && (z->hidden&2))
  295. { int colpos;
  296. Buf[0] = '\0';
  297. if (!xspin)
  298. { if (columns == 2)
  299. sprintf(Buf, "~G%s(%d):%s = ",
  300. r->n->name, r->pid, z->name);
  301. else
  302. sprintf(Buf, "%s(%d):%s = ",
  303. r->n->name, r->pid, z->name);
  304. }
  305. sr_buf(getval(dummy), z->type==MTYPE);
  306. if (z->colnr == 0)
  307. { z->colnr = maxcolnr;
  308. maxcolnr = 1+(maxcolnr%10);
  309. }
  310. colpos = nproc+z->colnr-1;
  311. if (columns == 2)
  312. { pstext(colpos, Buf);
  313. continue;
  314. }
  315. if (!xspin)
  316. { printf("\t\t%s\n", Buf);
  317. continue;
  318. }
  319. printf("MSC: ~G %s(%d):%s %s\n",
  320. r->n->name, r->pid, z->name, Buf);
  321. printf("%3d:\tproc %3d (TRACK) line 1 \"var\" ",
  322. depth, colpos);
  323. printf("(state 0)\t[printf('MSC: locvar\\\\n')]\n");
  324. printf("\t\t%s(%d):%s",
  325. r->n->name, r->pid, z->name);
  326. if (z->nel > 1 || z->isarray) printf("[%d]", i);
  327. printf(" = %s\n", Buf);
  328. } } }
  329. }