1 /***** spin: vars.c *****/ 2 3 /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */ 4 /* 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.att.com */ 12 13 #include "spin.h" 14 #include "y.tab.h" 15 16 extern RunList *X, *LastX; 17 extern Symbol *Fname; 18 extern int lineno, depth, verbose, xspin, Have_claim, no_arrays; 19 20 int 21 getval(Lextok *sn) 22 { Symbol *s = sn->sym; 23 24 if (strcmp(s->name, "_last") == 0) 25 return (LastX)?LastX->pid:0; 26 if (strcmp(s->name, "_p") == 0) 27 return (X && X->pc)?X->pc->seqno:0; 28 if (strcmp(s->name, "_pid") == 0) 29 { if (!X) return 0; 30 if (Have_claim 31 && Have_claim >= X->pid) 32 return X->pid - 1; 33 return X->pid; 34 35 } 36 if (s->context && s->type) 37 return getlocal(sn); 38 39 if (!s->type) /* not declared locally */ 40 { s = lookup(s->name); /* try global */ 41 sn->sym = s; /* fix it */ 42 } 43 44 return getglobal(sn); 45 } 46 47 int 48 setval(Lextok *v, int n) 49 { 50 if (v->sym->context && v->sym->type) 51 return setlocal(v, n); 52 if (!v->sym->type) 53 v->sym = lookup(v->sym->name); 54 return setglobal(v, n); 55 } 56 57 int 58 checkvar(Symbol *s, int n) 59 { int i; 60 61 if (n >= s->nel || n < 0) 62 { non_fatal("array indexing error, '%s'", s->name); 63 return 0; 64 } 65 66 if (s->type == 0) 67 { non_fatal("undecl var '%s' (assuming int)", s->name); 68 s->type = INT; 69 } 70 /* it cannot be a STRUCT */ 71 if (s->val == (int *) 0) /* uninitialized */ 72 { s->val = (int *) emalloc(s->nel*sizeof(int)); 73 for (i = 0; i < s->nel; i++) 74 { if (s->type != CHAN) 75 s->val[i] = eval(s->ini); 76 else 77 s->val[i] = qmake(s); 78 } } 79 return 1; 80 } 81 82 int 83 getglobal(Lextok *sn) 84 { Symbol *s = sn->sym; 85 int n = eval(sn->lft); 86 int i; 87 88 if (s->type == 0 && X && (i = find_lab(s, X->n))) 89 { printf("findlab through getglobal on %s\n", s->name); 90 return i; /* can this happen? */ 91 } 92 if (s->type == STRUCT) 93 return Rval_struct(sn, s, 1); /* 1 = check init */ 94 if (checkvar(s, n)) 95 return cast_val(s->type, s->val[n]); 96 return 0; 97 } 98 99 int 100 cast_val(int t, int v) 101 { int i=0; short s=0; unsigned char u=0; 102 103 if (t == INT || t == CHAN) i = v; 104 else if (t == SHORT) s = (short) v; 105 else if (t == BYTE || t == MTYPE) u = (unsigned char)v; 106 else if (t == BIT) u = (unsigned char)(v&1); 107 108 if (v != i+s+u) 109 { char buf[32]; sprintf(buf, "%d->%d (%d)", v, i+s+u, t); 110 non_fatal("value (%s) truncated in assignment", buf); 111 } 112 return (int)(i+s+u); 113 } 114 115 int 116 setglobal(Lextok *v, int m) 117 { 118 if (v->sym->type == STRUCT) 119 (void) Lval_struct(v, v->sym, 1, m); 120 else 121 { int n = eval(v->lft); 122 if (checkvar(v->sym, n)) 123 { v->sym->val[n] = m; 124 v->sym->setat = depth; 125 } } 126 return 1; 127 } 128 129 void 130 dumpclaims(FILE *fd, int pid, char *s) 131 { extern Lextok *Xu_List; extern int terse, Pid; 132 Lextok *m; int cnt = 0; int oPid = Pid; 133 134 for (m = Xu_List; m; m = m->rgt) 135 if (strcmp(m->sym->name, s) == 0) 136 { cnt=1; 137 break; 138 } 139 if (cnt == 0) return; 140 141 Pid = pid; 142 fprintf(fd, "#ifndef XUSAFE\n"); 143 for (m = Xu_List; m; m = m->rgt) 144 { if (strcmp(m->sym->name, s) != 0) 145 continue; 146 no_arrays = 1; 147 putname(fd, "\t\tsetq_claim(", m->lft, 0, ""); 148 no_arrays = 0; 149 fprintf(fd, ", %d, ", m->val); 150 terse = 1; 151 putname(fd, "\"", m->lft, 0, "\", h, "); 152 terse = 0; 153 fprintf(fd, "\"%s\");\n", s); 154 } 155 fprintf(fd, "#endif\n"); 156 Pid = oPid; 157 } 158 159 void 160 dumpglobals(void) 161 { extern Symbol *symtab[Nhash+1]; 162 Lextok *dummy; 163 Symbol *sp; 164 int i, j; 165 166 for (i = 0; i <= Nhash; i++) 167 for (sp = symtab[i]; sp; sp = sp->next) 168 { if (!sp->type || sp->context || sp->owner 169 || sp->type == PROCTYPE || sp->type == PREDEF) 170 continue; 171 if (sp->type == STRUCT) 172 dump_struct(sp, sp->name, 0); 173 else 174 for (j = 0; j < sp->nel; j++) 175 { if (sp->type == CHAN) 176 { doq(sp, j, 0); 177 continue; 178 } else 179 { if (xspin > 0 180 && (verbose&4) 181 && sp->setat < depth) 182 continue; 183 184 dummy = nn(ZN, NAME, 185 nn(ZN,CONST,ZN,ZN), ZN); 186 dummy->sym = sp; 187 dummy->lft->val = j; 188 printf("\t\t%s", sp->name); 189 if (sp->nel > 1) printf("[%d]", j); 190 printf(" = %d\n", getglobal(dummy)); 191 } } } 192 } 193 194 void 195 dumplocal(RunList *r) 196 { Lextok *dummy; 197 Symbol *z, *s = r->symtab; 198 int i; 199 200 for (z = s; z; z = z->next) 201 { if (z->type == STRUCT) 202 dump_struct(z, z->name, r); 203 else 204 for (i = 0; i < z->nel; i++) 205 { if (z->type == CHAN) 206 doq(z, i, r); 207 else 208 { 209 if (xspin > 0 210 && (verbose&4) 211 && z->setat < depth) 212 continue; 213 dummy = nn(ZN, NAME, 214 nn(ZN,CONST,ZN,ZN), ZN); 215 dummy->sym = z; 216 dummy->lft->val = i; 217 printf("\t\t%s(%d):%s", 218 r->n->name, r->pid, z->name); 219 if (z->nel > 1) printf("[%d]", i); 220 printf(" = %d\n", getval(dummy)); 221 } } } 222 } 223