1 /***** spin: vars.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 Ordered *all_names;
16 extern RunList *X, *LastX;
17 extern Symbol *Fname;
18 extern char Buf[];
19 extern int lineno, depth, verbose, xspin, limited_vis;
20 extern int analyze, jumpsteps, nproc, nstop, columns;
21 extern short no_arrays, Have_claim;
22 extern void sr_mesg(FILE *, int, int);
23 extern void sr_buf(int, int);
24
25 static int getglobal(Lextok *);
26 static int setglobal(Lextok *, int);
27 static int maxcolnr = 1;
28
29 int
getval(Lextok * sn)30 getval(Lextok *sn)
31 { Symbol *s = sn->sym;
32
33 if (strcmp(s->name, "_") == 0)
34 { non_fatal("attempt to read value of '_'", 0);
35 return 0;
36 }
37 if (strcmp(s->name, "_last") == 0)
38 return (LastX)?LastX->pid:0;
39 if (strcmp(s->name, "_p") == 0)
40 return (X && X->pc)?X->pc->seqno:0;
41 if (strcmp(s->name, "_pid") == 0)
42 { if (!X) return 0;
43 return X->pid - Have_claim;
44 }
45 if (strcmp(s->name, "_nr_pr") == 0)
46 return nproc-nstop; /* new 3.3.10 */
47
48 if (s->context && s->type)
49 return getlocal(sn);
50
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
58 int
setval(Lextok * v,int n)59 setval(Lextok *v, int n)
60 {
61 if (v->sym->context && v->sym->type)
62 return setlocal(v, n);
63 if (!v->sym->type)
64 v->sym = lookup(v->sym->name);
65 return setglobal(v, n);
66 }
67
68 void
rm_selfrefs(Symbol * s,Lextok * i)69 rm_selfrefs(Symbol *s, Lextok *i)
70 {
71 if (!i) return;
72
73 if (i->ntyp == NAME
74 && strcmp(i->sym->name, s->name) == 0
75 && ( (!i->sym->context && !s->context)
76 || ( i->sym->context && s->context
77 && strcmp(i->sym->context->name, s->context->name) == 0)))
78 { lineno = i->ln;
79 Fname = i->fn;
80 non_fatal("self-reference initializing '%s'", s->name);
81 i->ntyp = CONST;
82 i->val = 0;
83 } else
84 { rm_selfrefs(s, i->lft);
85 rm_selfrefs(s, i->rgt);
86 }
87 }
88
89 int
checkvar(Symbol * s,int n)90 checkvar(Symbol *s, int n)
91 { int i, oln = lineno; /* calls on eval() change it */
92 Symbol *ofnm = Fname;
93
94 if (!in_bound(s, n))
95 return 0;
96
97 if (s->type == 0)
98 { non_fatal("undecl var %s (assuming int)", s->name);
99 s->type = INT;
100 }
101 /* not a STRUCT */
102 if (s->val == (int *) 0) /* uninitialized */
103 { s->val = (int *) emalloc(s->nel*sizeof(int));
104 for (i = 0; i < s->nel; i++)
105 { if (s->type != CHAN)
106 { rm_selfrefs(s, s->ini);
107 s->val[i] = eval(s->ini);
108 } else if (!analyze)
109 s->val[i] = qmake(s);
110 } }
111 lineno = oln;
112 Fname = ofnm;
113
114 return 1;
115 }
116
117 static int
getglobal(Lextok * sn)118 getglobal(Lextok *sn)
119 { Symbol *s = sn->sym;
120 int i, n = eval(sn->lft);
121
122 if (s->type == 0 && X && (i = find_lab(s, X->n, 0)))
123 { printf("findlab through getglobal on %s\n", s->name);
124 return i; /* can this happen? */
125 }
126 if (s->type == STRUCT)
127 return Rval_struct(sn, s, 1); /* 1 = check init */
128 if (checkvar(s, n))
129 return cast_val(s->type, s->val[n], s->nbits);
130 return 0;
131 }
132
133 int
cast_val(int t,int v,int w)134 cast_val(int t, int v, int w)
135 { int i=0; short s=0; unsigned int u=0;
136
137 if (t == PREDEF || t == INT || t == CHAN) i = v; /* predef means _ */
138 else if (t == SHORT) s = (short) v;
139 else if (t == BYTE || t == MTYPE) u = (unsigned char)v;
140 else if (t == BIT) u = (unsigned char)(v&1);
141 else if (t == UNSIGNED)
142 { if (w == 0)
143 fatal("cannot happen, cast_val", (char *)0);
144 /* u = (unsigned)(v& ((1<<w)-1)); problem when w=32 */
145 u = (unsigned)(v& (~0u>>(8*sizeof(unsigned)-w))); /* doug */
146 }
147
148 if (v != i+s+ (int) u)
149 { char buf[64]; sprintf(buf, "%d->%d (%d)", v, i+s+u, t);
150 non_fatal("value (%s) truncated in assignment", buf);
151 }
152 return (int)(i+s+u);
153 }
154
155 static int
setglobal(Lextok * v,int m)156 setglobal(Lextok *v, int m)
157 {
158 if (v->sym->type == STRUCT)
159 (void) Lval_struct(v, v->sym, 1, m);
160 else
161 { int n = eval(v->lft);
162 if (checkvar(v->sym, n))
163 { int oval = v->sym->val[n];
164 int nval = cast_val(v->sym->type, m, v->sym->nbits);
165 v->sym->val[n] = nval;
166 if (oval != nval)
167 { v->sym->setat = depth;
168 } } }
169 return 1;
170 }
171
172 void
dumpclaims(FILE * fd,int pid,char * s)173 dumpclaims(FILE *fd, int pid, char *s)
174 { extern Lextok *Xu_List; extern int Pid;
175 extern short terse;
176 Lextok *m; int cnt = 0; int oPid = Pid;
177
178 for (m = Xu_List; m; m = m->rgt)
179 if (strcmp(m->sym->name, s) == 0)
180 { cnt=1;
181 break;
182 }
183 if (cnt == 0) return;
184
185 Pid = pid;
186 fprintf(fd, "#ifndef XUSAFE\n");
187 for (m = Xu_List; m; m = m->rgt)
188 { if (strcmp(m->sym->name, s) != 0)
189 continue;
190 no_arrays = 1;
191 putname(fd, "\t\tsetq_claim(", m->lft, 0, "");
192 no_arrays = 0;
193 fprintf(fd, ", %d, ", m->val);
194 terse = 1;
195 putname(fd, "\"", m->lft, 0, "\", h, ");
196 terse = 0;
197 fprintf(fd, "\"%s\");\n", s);
198 }
199 fprintf(fd, "#endif\n");
200 Pid = oPid;
201 }
202
203 void
dumpglobals(void)204 dumpglobals(void)
205 { Ordered *walk;
206 static Lextok *dummy = ZN;
207 Symbol *sp;
208 int j;
209
210 if (!dummy)
211 dummy = nn(ZN, NAME, nn(ZN,CONST,ZN,ZN), ZN);
212
213 for (walk = all_names; walk; walk = walk->next)
214 { sp = walk->entry;
215 if (!sp->type || sp->context || sp->owner
216 || sp->type == PROCTYPE || sp->type == PREDEF
217 || sp->type == CODE_FRAG || sp->type == CODE_DECL
218 || (sp->type == MTYPE && ismtype(sp->name)))
219 continue;
220
221 if (sp->type == STRUCT)
222 { if ((verbose&4) && !(verbose&64)
223 && (sp->setat < depth
224 && jumpsteps != depth))
225 { continue;
226 }
227 dump_struct(sp, sp->name, 0);
228 continue;
229 }
230 for (j = 0; j < sp->nel; j++)
231 { int prefetch;
232 if (sp->type == CHAN)
233 { doq(sp, j, 0);
234 continue;
235 }
236 if ((verbose&4) && !(verbose&64)
237 && (sp->setat < depth
238 && jumpsteps != depth))
239 { continue;
240 }
241
242 dummy->sym = sp;
243 dummy->lft->val = j;
244 /* in case of cast_val warnings, do this first: */
245 prefetch = getglobal(dummy);
246 printf("\t\t%s", sp->name);
247 if (sp->nel > 1 || sp->isarray) printf("[%d]", j);
248 printf(" = ");
249 sr_mesg(stdout, prefetch,
250 sp->type == MTYPE);
251 printf("\n");
252 if (limited_vis && (sp->hidden&2))
253 { int colpos;
254 Buf[0] = '\0';
255 if (!xspin)
256 { if (columns == 2)
257 sprintf(Buf, "~G%s = ", sp->name);
258 else
259 sprintf(Buf, "%s = ", sp->name);
260 }
261 sr_buf(prefetch, sp->type == MTYPE);
262 if (sp->colnr == 0)
263 { sp->colnr = maxcolnr;
264 maxcolnr = 1+(maxcolnr%10);
265 }
266 colpos = nproc+sp->colnr-1;
267 if (columns == 2)
268 { pstext(colpos, Buf);
269 continue;
270 }
271 if (!xspin)
272 { printf("\t\t%s\n", Buf);
273 continue;
274 }
275 printf("MSC: ~G %s %s\n", sp->name, Buf);
276 printf("%3d:\tproc %3d (TRACK) line 1 \"var\" ",
277 depth, colpos);
278 printf("(state 0)\t[printf('MSC: globvar\\\\n')]\n");
279 printf("\t\t%s", sp->name);
280 if (sp->nel > 1 || sp->isarray) printf("[%d]", j);
281 printf(" = %s\n", Buf);
282 } } }
283 }
284
285 void
dumplocal(RunList * r)286 dumplocal(RunList *r)
287 { static Lextok *dummy = ZN;
288 Symbol *z, *s;
289 int i;
290
291 if (!r) return;
292
293 s = r->symtab;
294
295 if (!dummy)
296 dummy = nn(ZN, NAME, nn(ZN,CONST,ZN,ZN), ZN);
297
298 for (z = s; z; z = z->next)
299 { if (z->type == STRUCT)
300 { dump_struct(z, z->name, r);
301 continue;
302 }
303 for (i = 0; i < z->nel; i++)
304 { if (z->type == CHAN)
305 { doq(z, i, r);
306 continue;
307 }
308 if ((verbose&4) && !(verbose&64)
309 && (z->setat < depth
310 && jumpsteps != depth))
311 continue;
312
313 dummy->sym = z;
314 dummy->lft->val = i;
315
316 printf("\t\t%s(%d):%s",
317 r->n->name, r->pid - Have_claim, z->name);
318 if (z->nel > 1 || z->isarray) printf("[%d]", i);
319 printf(" = ");
320 sr_mesg(stdout, getval(dummy), z->type == MTYPE);
321 printf("\n");
322 if (limited_vis && (z->hidden&2))
323 { int colpos;
324 Buf[0] = '\0';
325 if (!xspin)
326 { if (columns == 2)
327 sprintf(Buf, "~G%s(%d):%s = ",
328 r->n->name, r->pid, z->name);
329 else
330 sprintf(Buf, "%s(%d):%s = ",
331 r->n->name, r->pid, z->name);
332 }
333 sr_buf(getval(dummy), z->type==MTYPE);
334 if (z->colnr == 0)
335 { z->colnr = maxcolnr;
336 maxcolnr = 1+(maxcolnr%10);
337 }
338 colpos = nproc+z->colnr-1;
339 if (columns == 2)
340 { pstext(colpos, Buf);
341 continue;
342 }
343 if (!xspin)
344 { printf("\t\t%s\n", Buf);
345 continue;
346 }
347 printf("MSC: ~G %s(%d):%s %s\n",
348 r->n->name, r->pid, z->name, Buf);
349
350 printf("%3d:\tproc %3d (TRACK) line 1 \"var\" ",
351 depth, colpos);
352 printf("(state 0)\t[printf('MSC: locvar\\\\n')]\n");
353 printf("\t\t%s(%d):%s",
354 r->n->name, r->pid, z->name);
355 if (z->nel > 1 || z->isarray) printf("[%d]", i);
356 printf(" = %s\n", Buf);
357 } } }
358 }
359