sys/src/cmd/spin/vars.c

   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[32]; 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                 {       v->sym->val[n] = cast_val(v->sym->type, m, v->sym->nbits);
 163                         v->sym->setat = depth;
 164         }       }
 165         return 1;
 166 }
 167
 168 void
 169 dumpclaims(FILE *fd, int pid, char *s)
 170 {       extern Lextok *Xu_List; extern int Pid;
 171         extern short terse;
 172         Lextok *m; int cnt = 0; int oPid = Pid;
 173
 174         for (m = Xu_List; m; m = m->rgt)
 175                 if (strcmp(m->sym->name, s) == 0)
 176                 {       cnt=1;
 177                         break;
 178                 }
 179         if (cnt == 0) return;
 180
 181         Pid = pid;
 182         fprintf(fd, "#ifndef XUSAFE\n");
 183         for (m = Xu_List; m; m = m->rgt)
 184         {       if (strcmp(m->sym->name, s) != 0)
 185                         continue;
 186                 no_arrays = 1;
 187                 putname(fd, "\t\tsetq_claim(", m->lft, 0, "");
 188                 no_arrays = 0;
 189                 fprintf(fd, ", %d, ", m->val);
 190                 terse = 1;
 191                 putname(fd, "\"", m->lft, 0, "\", h, ");
 192                 terse = 0;
 193                 fprintf(fd, "\"%s\");\n", s);
 194         }
 195         fprintf(fd, "#endif\n");
 196         Pid = oPid;
 197 }
 198
 199 void
 200 dumpglobals(void)
 201 {       Ordered *walk;
 202         static Lextok *dummy = ZN;
 203         Symbol *sp;
 204         int j;
 205
 206         if (!dummy)
 207                 dummy = nn(ZN, NAME, nn(ZN,CONST,ZN,ZN), ZN);
 208
 209         for (walk = all_names; walk; walk = walk->next)
 210         {       sp = walk->entry;
 211                 if (!sp->type || sp->context || sp->owner
 212                 ||  sp->type == PROCTYPE  || sp->type == PREDEF
 213                 ||  sp->type == CODE_FRAG || sp->type == CODE_DECL
 214                 ||  (sp->type == MTYPE && ismtype(sp->name)))
 215                         continue;
 216
 217                 if (sp->type == STRUCT)
 218                 {       dump_struct(sp, sp->name, 0);
 219                         continue;
 220                 }
 221                 for (j = 0; j < sp->nel; j++)
 222                 {       int prefetch;
 223                         if (sp->type == CHAN)
 224                         {       doq(sp, j, 0);
 225                                 continue;
 226                         }
 227                         if ((verbose&4) && !(verbose&64)
 228                         &&  (sp->setat < depth
 229                         &&   jumpsteps != depth))
 230                                 continue;
 231                         dummy->sym = sp;
 232                         dummy->lft->val = j;
 233                         /* in case of cast_val warnings, do this first: */
 234                         prefetch = getglobal(dummy);
 235                         printf("\t\t%s", sp->name);
 236                         if (sp->nel > 1) printf("[%d]", j);
 237                         printf(" = ");
 238                         sr_mesg(stdout, prefetch,
 239                                 sp->type == MTYPE);
 240                         printf("\n");
 241                         if (limited_vis && (sp->hidden&2))
 242                         {       int colpos;
 243                                 Buf[0] = '\0';
 244                                 if (!xspin)
 245                                 {       if (columns == 2)
 246                                         sprintf(Buf, "~G%s = ", sp->name);
 247                                         else
 248                                         sprintf(Buf, "%s = ", sp->name);
 249                                 }
 250                                 sr_buf(prefetch, sp->type == MTYPE);
 251                                 if (sp->colnr == 0)
 252                                 {       sp->colnr = maxcolnr;
 253                                         maxcolnr = 1+(maxcolnr%10);
 254                                 }
 255                                 colpos = nproc+sp->colnr-1;
 256                                 if (columns == 2)
 257                                 {       pstext(colpos, Buf);
 258                                         continue;
 259                                 }
 260                                 if (!xspin)
 261                                 {       printf("\t\t%s\n", Buf);
 262                                         continue;
 263                                 }
 264                                 printf("MSC: ~G %s %s\n", sp->name, Buf);
 265                                 printf("%3d:\tproc %3d (TRACK) line   1 \"var\" ",
 266                                         depth, colpos);
 267                                 printf("(state 0)\t[printf('MSC: globvar\\\\n')]\n");
 268                                 printf("\t\t%s", sp->name);
 269                                 if (sp->nel > 1) printf("[%d]", j);
 270                                 printf(" = %s\n", Buf);
 271         }       }       }
 272 }
 273
 274 void
 275 dumplocal(RunList *r)
 276 {       static Lextok *dummy = ZN;
 277         Symbol *z, *s;
 278         int i;
 279
 280         if (!r) return;
 281
 282         s = r->symtab;
 283
 284         if (!dummy)
 285                 dummy = nn(ZN, NAME, nn(ZN,CONST,ZN,ZN), ZN);
 286
 287         for (z = s; z; z = z->next)
 288         {       if (z->type == STRUCT)
 289                 {       dump_struct(z, z->name, r);
 290                         continue;
 291                 }
 292                 for (i = 0; i < z->nel; i++)
 293                 {       if (z->type == CHAN)
 294                         {       doq(z, i, r);
 295                                 continue;
 296                         }
 297                         if ((verbose&4) && !(verbose&64)
 298                         &&  (z->setat < depth
 299                         &&   jumpsteps != depth))
 300                                 continue;
 301
 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), z->type == MTYPE);
 310                         printf("\n");
 311                         if (limited_vis && (z->hidden&2))
 312                         {       int colpos;
 313                                 Buf[0] = '\0';
 314                                 if (!xspin)
 315                                 {       if (columns == 2)
 316                                         sprintf(Buf, "~G%s(%d):%s = ",
 317                                         r->n->name, r->pid, z->name);
 318                                         else
 319                                         sprintf(Buf, "%s(%d):%s = ",
 320                                         r->n->name, r->pid, z->name);
 321                                 }
 322                                 sr_buf(getval(dummy), z->type==MTYPE);
 323                                 if (z->colnr == 0)
 324                                 {       z->colnr = maxcolnr;
 325                                         maxcolnr = 1+(maxcolnr%10);
 326                                 }
 327                                 colpos = nproc+z->colnr-1;
 328                                 if (columns == 2)
 329                                 {       pstext(colpos, Buf);
 330                                         continue;
 331                                 }
 332                                 if (!xspin)
 333                                 {       printf("\t\t%s\n", Buf);
 334                                         continue;
 335                                 }
 336                                 printf("MSC: ~G %s(%d):%s %s\n",
 337                                         r->n->name, r->pid, z->name, Buf);
 338
 339                                 printf("%3d:\tproc %3d (TRACK) line   1 \"var\" ",
 340                                         depth, colpos);
 341                                 printf("(state 0)\t[printf('MSC: locvar\\\\n')]\n");
 342                                 printf("\t\t%s(%d):%s",
 343                                         r->n->name, r->pid, z->name);
 344                                 if (z->nel > 1) printf("[%d]", i);
 345                                 printf(" = %s\n", Buf);
 346         }       }       }
 347 }