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