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 } 359