Subversion Repositories planix.SVN

Rev

Details | Last modification | View Log | RSS feed

Rev Author Line No. Line
2 - 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 
 
114 
	return 1;
115 
}
116 
 
117 
static int
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
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
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
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
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
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 
}