0b55f123 |
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 |
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 |
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 |
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 |
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 | return 1; |
114 | } |
115 | |
116 | static int |
117 | getglobal(Lextok *sn) |
118 | { Symbol *s = sn->sym; |
119 | int i, n = eval(sn->lft); |
120 | |
121 | if (s->type == 0 && X && (i = find_lab(s, X->n, 0))) |
122 | { printf("findlab through getglobal on %s\n", s->name); |
123 | return i; /* can this happen? */ |
124 | } |
125 | if (s->type == STRUCT) |
126 | return Rval_struct(sn, s, 1); /* 1 = check init */ |
127 | if (checkvar(s, n)) |
128 | return cast_val(s->type, s->val[n], s->nbits); |
129 | return 0; |
130 | } |
131 | |
132 | int |
133 | cast_val(int t, int v, int w) |
134 | { int i=0; short s=0; unsigned int u=0; |
135 | |
136 | if (t == PREDEF || t == INT || t == CHAN) i = v; /* predef means _ */ |
137 | else if (t == SHORT) s = (short) v; |
138 | else if (t == BYTE || t == MTYPE) u = (unsigned char)v; |
139 | else if (t == BIT) u = (unsigned char)(v&1); |
140 | else if (t == UNSIGNED) |
141 | { if (w == 0) |
142 | fatal("cannot happen, cast_val", (char *)0); |
143 | /* u = (unsigned)(v& ((1<<w)-1)); problem when w=32 */ |
144 | u = (unsigned)(v& (~0u>>(8*sizeof(unsigned)-w))); /* doug */ |
145 | } |
146 | |
147 | if (v != i+s+ (int) u) |
148 | { char buf[64]; sprintf(buf, "%d->%d (%d)", v, i+s+u, t); |
149 | non_fatal("value (%s) truncated in assignment", buf); |
150 | } |
151 | return (int)(i+s+u); |
152 | } |
153 | |
154 | static int |
155 | setglobal(Lextok *v, int m) |
156 | { |
157 | if (v->sym->type == STRUCT) |
158 | (void) Lval_struct(v, v->sym, 1, m); |
159 | else |
160 | { int n = eval(v->lft); |
161 | if (checkvar(v->sym, n)) |
162 | { int oval = v->sym->val[n]; |
163 | int nval = cast_val(v->sym->type, m, v->sym->nbits); |
164 | v->sym->val[n] = nval; |
165 | if (oval != nval) |
166 | { v->sym->setat = depth; |
167 | } } } |
168 | return 1; |
169 | } |
170 | |
171 | void |
172 | dumpclaims(FILE *fd, int pid, char *s) |
173 | { extern Lextok *Xu_List; extern int Pid; |
174 | extern short terse; |
175 | Lextok *m; int cnt = 0; int oPid = Pid; |
176 | |
177 | for (m = Xu_List; m; m = m->rgt) |
178 | if (strcmp(m->sym->name, s) == 0) |
179 | { cnt=1; |
180 | break; |
181 | } |
182 | if (cnt == 0) return; |
183 | |
184 | Pid = pid; |
185 | fprintf(fd, "#ifndef XUSAFE\n"); |
186 | for (m = Xu_List; m; m = m->rgt) |
187 | { if (strcmp(m->sym->name, s) != 0) |
188 | continue; |
189 | no_arrays = 1; |
190 | putname(fd, "\t\tsetq_claim(", m->lft, 0, ""); |
191 | no_arrays = 0; |
192 | fprintf(fd, ", %d, ", m->val); |
193 | terse = 1; |
194 | putname(fd, "\"", m->lft, 0, "\", h, "); |
195 | terse = 0; |
196 | fprintf(fd, "\"%s\");\n", s); |
197 | } |
198 | fprintf(fd, "#endif\n"); |
199 | Pid = oPid; |
200 | } |
201 | |
202 | void |
203 | dumpglobals(void) |
204 | { Ordered *walk; |
205 | static Lextok *dummy = ZN; |
206 | Symbol *sp; |
207 | int j; |
208 | |
209 | if (!dummy) |
210 | dummy = nn(ZN, NAME, nn(ZN,CONST,ZN,ZN), ZN); |
211 | |
212 | for (walk = all_names; walk; walk = walk->next) |
213 | { sp = walk->entry; |
214 | if (!sp->type || sp->context || sp->owner |
215 | || sp->type == PROCTYPE || sp->type == PREDEF |
216 | || sp->type == CODE_FRAG || sp->type == CODE_DECL |
217 | || (sp->type == MTYPE && ismtype(sp->name))) |
218 | continue; |
219 | |
220 | if (sp->type == STRUCT) |
221 | { if ((verbose&4) && !(verbose&64) |
222 | && (sp->setat < depth |
223 | && jumpsteps != depth)) |
224 | { continue; |
225 | } |
226 | dump_struct(sp, sp->name, 0); |
227 | continue; |
228 | } |
229 | for (j = 0; j < sp->nel; j++) |
230 | { int prefetch; |
231 | if (sp->type == CHAN) |
232 | { doq(sp, j, 0); |
233 | continue; |
234 | } |
235 | if ((verbose&4) && !(verbose&64) |
236 | && (sp->setat < depth |
237 | && jumpsteps != depth)) |
238 | { continue; |
239 | } |
240 | |
241 | dummy->sym = sp; |
242 | dummy->lft->val = j; |
243 | /* in case of cast_val warnings, do this first: */ |
244 | prefetch = getglobal(dummy); |
245 | printf("\t\t%s", sp->name); |
246 | if (sp->nel > 1) printf("[%d]", j); |
247 | printf(" = "); |
248 | sr_mesg(stdout, prefetch, |
249 | sp->type == MTYPE); |
250 | printf("\n"); |
251 | if (limited_vis && (sp->hidden&2)) |
252 | { int colpos; |
253 | Buf[0] = '\0'; |
254 | if (!xspin) |
255 | { if (columns == 2) |
256 | sprintf(Buf, "~G%s = ", sp->name); |
257 | else |
258 | sprintf(Buf, "%s = ", sp->name); |
259 | } |
260 | sr_buf(prefetch, sp->type == MTYPE); |
261 | if (sp->colnr == 0) |
262 | { sp->colnr = maxcolnr; |
263 | maxcolnr = 1+(maxcolnr%10); |
264 | } |
265 | colpos = nproc+sp->colnr-1; |
266 | if (columns == 2) |
267 | { pstext(colpos, Buf); |
268 | continue; |
269 | } |
270 | if (!xspin) |
271 | { printf("\t\t%s\n", Buf); |
272 | continue; |
273 | } |
274 | printf("MSC: ~G %s %s\n", sp->name, Buf); |
275 | printf("%3d:\tproc %3d (TRACK) line 1 \"var\" ", |
276 | depth, colpos); |
277 | printf("(state 0)\t[printf('MSC: globvar\\\\n')]\n"); |
278 | printf("\t\t%s", sp->name); |
279 | if (sp->nel > 1) printf("[%d]", j); |
280 | printf(" = %s\n", Buf); |
281 | } } } |
282 | } |
283 | |
284 | void |
285 | dumplocal(RunList *r) |
286 | { static Lextok *dummy = ZN; |
287 | Symbol *z, *s; |
288 | int i; |
289 | |
290 | if (!r) return; |
291 | |
292 | s = r->symtab; |
293 | |
294 | if (!dummy) |
295 | dummy = nn(ZN, NAME, nn(ZN,CONST,ZN,ZN), ZN); |
296 | |
297 | for (z = s; z; z = z->next) |
298 | { if (z->type == STRUCT) |
299 | { dump_struct(z, z->name, r); |
300 | continue; |
301 | } |
302 | for (i = 0; i < z->nel; i++) |
303 | { if (z->type == CHAN) |
304 | { doq(z, i, r); |
305 | continue; |
306 | } |
307 | if ((verbose&4) && !(verbose&64) |
308 | && (z->setat < depth |
309 | && jumpsteps != depth)) |
310 | continue; |
311 | |
312 | dummy->sym = z; |
313 | dummy->lft->val = i; |
314 | |
315 | printf("\t\t%s(%d):%s", |
316 | r->n->name, r->pid, z->name); |
317 | if (z->nel > 1) printf("[%d]", i); |
318 | printf(" = "); |
319 | sr_mesg(stdout, getval(dummy), z->type == MTYPE); |
320 | printf("\n"); |
321 | if (limited_vis && (z->hidden&2)) |
322 | { int colpos; |
323 | Buf[0] = '\0'; |
324 | if (!xspin) |
325 | { if (columns == 2) |
326 | sprintf(Buf, "~G%s(%d):%s = ", |
327 | r->n->name, r->pid, z->name); |
328 | else |
329 | sprintf(Buf, "%s(%d):%s = ", |
330 | r->n->name, r->pid, z->name); |
331 | } |
332 | sr_buf(getval(dummy), z->type==MTYPE); |
333 | if (z->colnr == 0) |
334 | { z->colnr = maxcolnr; |
335 | maxcolnr = 1+(maxcolnr%10); |
336 | } |
337 | colpos = nproc+z->colnr-1; |
338 | if (columns == 2) |
339 | { pstext(colpos, Buf); |
340 | continue; |
341 | } |
342 | if (!xspin) |
343 | { printf("\t\t%s\n", Buf); |
344 | continue; |
345 | } |
346 | printf("MSC: ~G %s(%d):%s %s\n", |
347 | r->n->name, r->pid, z->name, Buf); |
348 | |
349 | printf("%3d:\tproc %3d (TRACK) line 1 \"var\" ", |
350 | depth, colpos); |
351 | printf("(state 0)\t[printf('MSC: locvar\\\\n')]\n"); |
352 | printf("\t\t%s(%d):%s", |
353 | r->n->name, r->pid, z->name); |
354 | if (z->nel > 1) printf("[%d]", i); |
355 | printf(" = %s\n", Buf); |
356 | } } } |
357 | } |