1 /***** spin: vars.c *****/ 2 3 /* Copyright (c) 1991-2000 by Lucent Technologies - Bell Laboratories */ 4 /* All Rights Reserved. This software is for educational purposes only. */ 5 /* Permission is given to distribute this code provided that this intro- */ 6 /* ductory message is not removed and no monies are exchanged. */ 7 /* No guarantee is expressed or implied by the distribution of this code. */ 8 /* Software written by Gerard J. Holzmann as part of the book: */ 9 /* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4, */ 10 /* Prentice Hall, Englewood Cliffs, NJ, 07632. */ 11 /* Send bug-reports and/or questions to: gerard@research.bell-labs.com */ 12 13 #include "spin.h" 14 #ifdef PC 15 #include "y_tab.h" 16 #else 17 #include "y.tab.h" 18 #endif 19 20 extern Ordered *all_names; 21 extern RunList *X, *LastX; 22 extern Symbol *Fname; 23 extern char Buf[]; 24 extern int lineno, depth, verbose, xspin, limited_vis; 25 extern int analyze, jumpsteps, nproc, nstop, columns; 26 extern short no_arrays, Have_claim, Skip_claim; 27 extern void sr_mesg(FILE *, int, int); 28 extern void sr_buf(int, int); 29 30 static int getglobal(Lextok *); 31 static int setglobal(Lextok *, int); 32 static int maxcolnr = 1; 33 34 int 35 getval(Lextok *sn) 36 { Symbol *s = sn->sym; 37 38 if (strcmp(s->name, "_") == 0) 39 { non_fatal("attempt to read value of '_'", 0); 40 return 0; 41 } 42 if (strcmp(s->name, "_last") == 0) 43 return (LastX)?LastX->pid:0; 44 if (strcmp(s->name, "_p") == 0) 45 return (X && X->pc)?X->pc->seqno:0; 46 if (strcmp(s->name, "_pid") == 0) 47 { if (!X) return 0; 48 return X->pid - Have_claim; 49 } 50 if (strcmp(s->name, "_nr_pr") == 0) 51 return nproc-nstop; /* new 3.3.10 */ 52 53 if (s->context && s->type) 54 return getlocal(sn); 55 56 if (!s->type) /* not declared locally */ 57 { s = lookup(s->name); /* try global */ 58 sn->sym = s; /* fix it */ 59 } 60 return getglobal(sn); 61 } 62 63 int 64 setval(Lextok *v, int n) 65 { 66 if (v->sym->context && v->sym->type) 67 return setlocal(v, n); 68 if (!v->sym->type) 69 v->sym = lookup(v->sym->name); 70 return setglobal(v, n); 71 } 72 73 void 74 rm_selfrefs(Symbol *s, Lextok *i) 75 { 76 if (!i) return; 77 78 if (i->ntyp == NAME 79 && strcmp(i->sym->name, s->name) == 0 80 && ( (!i->sym->context && !s->context) 81 || ( i->sym->context && s->context 82 && strcmp(i->sym->context->name, s->context->name) == 0))) 83 { lineno = i->ln; 84 Fname = i->fn; 85 non_fatal("self-reference initializing '%s'", s->name); 86 i->ntyp = CONST; 87 i->val = 0; 88 } else 89 { rm_selfrefs(s, i->lft); 90 rm_selfrefs(s, i->rgt); 91 } 92 } 93 94 int 95 checkvar(Symbol *s, int n) 96 { int i, oln = lineno; /* calls on eval() change it */ 97 Symbol *ofnm = Fname; 98 99 if (n >= s->nel || n < 0) 100 { printf("spin: indexing %s[%d] - size is %d\n", 101 s->name, n, s->nel); 102 non_fatal("indexing array \'%s\'", s->name); 103 return 0; 104 } 105 if (s->type == 0) 106 { non_fatal("undecl var %s (assuming int)", s->name); 107 s->type = INT; 108 } 109 /* not a STRUCT */ 110 if (s->val == (int *) 0) /* uninitialized */ 111 { s->val = (int *) emalloc(s->nel*sizeof(int)); 112 for (i = 0; i < s->nel; i++) 113 { if (s->type != CHAN) 114 { rm_selfrefs(s, s->ini); 115 s->val[i] = eval(s->ini); 116 } else if (!analyze) 117 s->val[i] = qmake(s); 118 } } 119 lineno = oln; 120 Fname = ofnm; 121 return 1; 122 } 123 124 static int 125 getglobal(Lextok *sn) 126 { Symbol *s = sn->sym; 127 int i, n = eval(sn->lft); 128 129 if (s->type == 0 && X && (i = find_lab(s, X->n, 0))) 130 { printf("findlab through getglobal on %s\n", s->name); 131 return i; /* can this happen? */ 132 } 133 if (s->type == STRUCT) 134 return Rval_struct(sn, s, 1); /* 1 = check init */ 135 if (checkvar(s, n)) 136 return cast_val(s->type, s->val[n], s->nbits); 137 return 0; 138 } 139 140 int 141 cast_val(int t, int v, int w) 142 { int i=0; short s=0; unsigned char u=0; 143 144 if (t == INT || t == CHAN) i = v; 145 else if (t == SHORT) s = (short) v; 146 else if (t == BYTE || t == MTYPE) u = (unsigned char)v; 147 else if (t == BIT) u = (unsigned char)(v&1); 148 else if (t == UNSIGNED) 149 { if (w == 0) 150 fatal("cannot happen, cast_val", (char *)0); 151 u = (unsigned char)(v& ((1<<w)-1)); 152 } 153 154 if (v != i+s+u) 155 { char buf[32]; sprintf(buf, "%d->%d (%d)", v, i+s+u, t); 156 non_fatal("value (%s) truncated in assignment", buf); 157 } 158 return (int)(i+s+u); 159 } 160 161 static int 162 setglobal(Lextok *v, int m) 163 { 164 if (v->sym->type == STRUCT) 165 (void) Lval_struct(v, v->sym, 1, m); 166 else 167 { int n = eval(v->lft); 168 if (checkvar(v->sym, n)) 169 { if (v->sym->nbits > 0) 170 m = (m & ((1<<v->sym->nbits)-1)); 171 v->sym->val[n] = m; 172 v->sym->setat = depth; 173 } } 174 return 1; 175 } 176 177 void 178 dumpclaims(FILE *fd, int pid, char *s) 179 { extern Lextok *Xu_List; extern int Pid; 180 extern short terse; 181 Lextok *m; int cnt = 0; int oPid = Pid; 182 183 for (m = Xu_List; m; m = m->rgt) 184 if (strcmp(m->sym->name, s) == 0) 185 { cnt=1; 186 break; 187 } 188 if (cnt == 0) return; 189 190 Pid = pid; 191 fprintf(fd, "#ifndef XUSAFE\n"); 192 for (m = Xu_List; m; m = m->rgt) 193 { if (strcmp(m->sym->name, s) != 0) 194 continue; 195 no_arrays = 1; 196 putname(fd, "\t\tsetq_claim(", m->lft, 0, ""); 197 no_arrays = 0; 198 fprintf(fd, ", %d, ", m->val); 199 terse = 1; 200 putname(fd, "\"", m->lft, 0, "\", h, "); 201 terse = 0; 202 fprintf(fd, "\"%s\");\n", s); 203 } 204 fprintf(fd, "#endif\n"); 205 Pid = oPid; 206 } 207 208 void 209 dumpglobals(void) 210 { Ordered *walk; 211 Lextok *dummy; 212 Symbol *sp; 213 int j; 214 215 for (walk = all_names; walk; walk = walk->next) 216 { sp = walk->entry; 217 if (!sp->type || sp->context || sp->owner 218 || sp->type == PROCTYPE || sp->type == PREDEF 219 || (sp->type == MTYPE && ismtype(sp->name))) 220 continue; 221 222 if (sp->type == STRUCT) 223 { dump_struct(sp, sp->name, 0); 224 continue; 225 } 226 for (j = 0; j < sp->nel; j++) 227 { int prefetch; 228 if (sp->type == CHAN) 229 { doq(sp, j, 0); 230 continue; 231 } 232 if ((verbose&4) && !(verbose&64) 233 && (sp->setat < depth 234 && jumpsteps != depth)) 235 continue; 236 dummy = nn(ZN, NAME, nn(ZN,CONST,ZN,ZN), ZN); 237 dummy->sym = sp; 238 dummy->lft->val = j; 239 /* in case of cast_val warnings, do this first: */ 240 prefetch = getglobal(dummy); 241 printf("\t\t%s", sp->name); 242 if (sp->nel > 1) printf("[%d]", j); 243 printf(" = "); 244 sr_mesg(stdout, prefetch, 245 sp->type == MTYPE); 246 printf("\n"); 247 if (limited_vis && (sp->hidden&2)) 248 { int colpos; 249 Buf[0] = '\0'; 250 if (!xspin) 251 { if (columns == 2) 252 sprintf(Buf, "~G%s = ", sp->name); 253 else 254 sprintf(Buf, "%s = ", sp->name); 255 } 256 sr_buf(prefetch, sp->type == MTYPE); 257 if (sp->colnr == 0) 258 { sp->colnr = maxcolnr; 259 maxcolnr = 1+(maxcolnr%10); 260 } 261 colpos = nproc+sp->colnr-1; 262 if (columns == 2) 263 { pstext(colpos, Buf); 264 continue; 265 } 266 if (!xspin) 267 { printf("\t\t%s\n", Buf); 268 continue; 269 } 270 printf("MSC: ~G %s %s\n", sp->name, Buf); 271 printf("%3d:\tproc %3d (TRACK) line 1 \"var\" ", 272 depth, colpos); 273 printf("(state 0)\t[printf('MSC: globvar\\\\n')]\n"); 274 printf("\t\t%s", sp->name); 275 if (sp->nel > 1) printf("[%d]", j); 276 printf(" = %s\n", Buf); 277 } } } 278 } 279 280 void 281 dumplocal(RunList *r) 282 { Lextok *dummy; 283 Symbol *z, *s = r->symtab; 284 int i; 285 286 for (z = s; z; z = z->next) 287 { if (z->type == STRUCT) 288 { dump_struct(z, z->name, r); 289 continue; 290 } 291 for (i = 0; i < z->nel; i++) 292 { if (z->type == CHAN) 293 { doq(z, i, r); 294 continue; 295 } 296 if ((verbose&4) && !(verbose&64) 297 && (z->setat < depth 298 && jumpsteps != depth)) 299 continue; 300 301 dummy = nn(ZN, NAME, nn(ZN,CONST,ZN,ZN), ZN); 302 dummy->sym = z; 303 dummy->lft->val = i; 304 305 printf("\t\t%s(%d):%s", 306 r->n->name, r->pid, z->name); 307 if (z->nel > 1) printf("[%d]", i); 308 printf(" = "); 309 sr_mesg(stdout, getval(dummy), 310 z->type == MTYPE); 311 printf("\n"); 312 if (limited_vis && (z->hidden&2)) 313 { int colpos; 314 Buf[0] = '\0'; 315 if (!xspin) 316 { if (columns == 2) 317 sprintf(Buf, "~G%s(%d):%s = ", 318 r->n->name, r->pid, z->name); 319 else 320 sprintf(Buf, "%s(%d):%s = ", 321 r->n->name, r->pid, z->name); 322 } 323 sr_buf(getval(dummy), z->type==MTYPE); 324 if (z->colnr == 0) 325 { z->colnr = maxcolnr; 326 maxcolnr = 1+(maxcolnr%10); 327 } 328 colpos = nproc+z->colnr-1; 329 if (columns == 2) 330 { pstext(colpos, Buf); 331 continue; 332 } 333 if (!xspin) 334 { printf("\t\t%s\n", Buf); 335 continue; 336 } 337 printf("MSC: ~G %s(%d):%s %s\n", 338 r->n->name, r->pid, z->name, Buf); 339 340 printf("%3d:\tproc %3d (TRACK) line 1 \"var\" ", 341 depth, colpos); 342 printf("(state 0)\t[printf('MSC: locvar\\\\n')]\n"); 343 printf("\t\t%s(%d):%s", 344 r->n->name, r->pid, z->name); 345 if (z->nel > 1) printf("[%d]", i); 346 printf(" = %s\n", Buf); 347 } } } 348 } 349