291983dd7078c2d939e7d4f26929b2764ea9574d
1 /***** spin: vars.c *****/
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 */
15 extern Ordered
*all_names
;
16 extern RunList
*X
, *LastX
;
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);
25 static int getglobal(Lextok
*);
26 static int setglobal(Lextok
*, int);
27 static int maxcolnr
= 1;
31 { Symbol
*s
= sn
->sym
;
33 if (strcmp(s
->name
, "_") == 0)
34 { non_fatal("attempt to read value of '_'", 0);
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)
43 return X
->pid
- Have_claim
;
45 if (strcmp(s
->name
, "_nr_pr") == 0)
46 return nproc
-nstop
; /* new 3.3.10 */
48 if (s
->context
&& s
->type
)
51 if (!s
->type
) /* not declared locally */
52 { s
= lookup(s
->name
); /* try global */
53 sn
->sym
= s
; /* fix it */
59 setval(Lextok
*v
, int n
)
61 if (v
->sym
->context
&& v
->sym
->type
)
62 return setlocal(v
, n
);
64 v
->sym
= lookup(v
->sym
->name
);
65 return setglobal(v
, n
);
69 rm_selfrefs(Symbol
*s
, Lextok
*i
)
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)))
80 non_fatal("self-reference initializing '%s'", s
->name
);
84 { rm_selfrefs(s
, i
->lft
);
85 rm_selfrefs(s
, i
->rgt
);
90 checkvar(Symbol
*s
, int n
)
91 { int i
, oln
= lineno
; /* calls on eval() change it */
98 { non_fatal("undecl var %s (assuming int)", s
->name
);
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
);
109 s
->val
[i
] = qmake(s
);
117 getglobal(Lextok
*sn
)
118 { Symbol
*s
= sn
->sym
;
119 int i
, n
= eval(sn
->lft
);
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? */
125 if (s
->type
== STRUCT
)
126 return Rval_struct(sn
, s
, 1); /* 1 = check init */
128 return cast_val(s
->type
, s
->val
[n
], s
->nbits
);
133 cast_val(int t
, int v
, int w
)
134 { int i
=0; short s
=0; unsigned int u
=0;
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
)
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 */
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
);
155 setglobal(Lextok
*v
, int m
)
157 if (v
->sym
->type
== STRUCT
)
158 (void) Lval_struct(v
, v
->sym
, 1, m
);
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
;
166 { v
->sym
->setat
= depth
;
172 dumpclaims(FILE *fd
, int pid
, char *s
)
173 { extern Lextok
*Xu_List
; extern int Pid
;
175 Lextok
*m
; int cnt
= 0; int oPid
= Pid
;
177 for (m
= Xu_List
; m
; m
= m
->rgt
)
178 if (strcmp(m
->sym
->name
, s
) == 0)
182 if (cnt
== 0) return;
185 fprintf(fd
, "#ifndef XUSAFE\n");
186 for (m
= Xu_List
; m
; m
= m
->rgt
)
187 { if (strcmp(m
->sym
->name
, s
) != 0)
190 putname(fd
, "\t\tsetq_claim(", m
->lft
, 0, "");
192 fprintf(fd
, ", %d, ", m
->val
);
194 putname(fd
, "\"", m
->lft
, 0, "\", h, ");
196 fprintf(fd
, "\"%s\");\n", s
);
198 fprintf(fd
, "#endif\n");
205 static Lextok
*dummy
= ZN
;
210 dummy
= nn(ZN
, NAME
, nn(ZN
,CONST
,ZN
,ZN
), ZN
);
212 for (walk
= all_names
; walk
; walk
= walk
->next
)
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
)))
220 if (sp
->type
== STRUCT
)
221 { if ((verbose
&4) && !(verbose
&64)
222 && (sp
->setat
< depth
223 && jumpsteps
!= depth
))
226 dump_struct(sp
, sp
->name
, 0);
229 for (j
= 0; j
< sp
->nel
; j
++)
231 if (sp
->type
== CHAN
)
235 if ((verbose
&4) && !(verbose
&64)
236 && (sp
->setat
< depth
237 && jumpsteps
!= depth
))
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
);
248 sr_mesg(stdout
, prefetch
,
251 if (limited_vis
&& (sp
->hidden
&2))
256 sprintf(Buf
, "~G%s = ", sp
->name
);
258 sprintf(Buf
, "%s = ", sp
->name
);
260 sr_buf(prefetch
, sp
->type
== MTYPE
);
262 { sp
->colnr
= maxcolnr
;
263 maxcolnr
= 1+(maxcolnr
%10);
265 colpos
= nproc
+sp
->colnr
-1;
267 { pstext(colpos
, Buf
);
271 { printf("\t\t%s\n", Buf
);
274 printf("MSC: ~G %s %s\n", sp
->name
, Buf
);
275 printf("%3d:\tproc %3d (TRACK) line 1 \"var\" ",
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
);
285 dumplocal(RunList
*r
)
286 { static Lextok
*dummy
= ZN
;
295 dummy
= nn(ZN
, NAME
, nn(ZN
,CONST
,ZN
,ZN
), ZN
);
297 for (z
= s
; z
; z
= z
->next
)
298 { if (z
->type
== STRUCT
)
299 { dump_struct(z
, z
->name
, r
);
302 for (i
= 0; i
< z
->nel
; i
++)
303 { if (z
->type
== CHAN
)
307 if ((verbose
&4) && !(verbose
&64)
309 && jumpsteps
!= depth
))
315 printf("\t\t%s(%d):%s",
316 r
->n
->name
, r
->pid
, z
->name
);
317 if (z
->nel
> 1) printf("[%d]", i
);
319 sr_mesg(stdout
, getval(dummy
), z
->type
== MTYPE
);
321 if (limited_vis
&& (z
->hidden
&2))
326 sprintf(Buf
, "~G%s(%d):%s = ",
327 r
->n
->name
, r
->pid
, z
->name
);
329 sprintf(Buf
, "%s(%d):%s = ",
330 r
->n
->name
, r
->pid
, z
->name
);
332 sr_buf(getval(dummy
), z
->type
==MTYPE
);
334 { z
->colnr
= maxcolnr
;
335 maxcolnr
= 1+(maxcolnr
%10);
337 colpos
= nproc
+z
->colnr
-1;
339 { pstext(colpos
, Buf
);
343 { printf("\t\t%s\n", Buf
);
346 printf("MSC: ~G %s(%d):%s %s\n",
347 r
->n
->name
, r
->pid
, z
->name
, Buf
);
349 printf("%3d:\tproc %3d (TRACK) line 1 \"var\" ",
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
);
This page took 0.038668 seconds and 3 git commands to generate.