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