sys/src/cmd/spin/dstep.c

   1 /***** spin: dstep.c *****/
   2
   3 /*
   4  * This file is part of the public release of Spin. It is subject to the
   5  * terms in the LICENSE file that is included in this source directory.
   6  * Tool documentation is available at http://spinroot.com
   7  */
   8
   9 #include <assert.h>
  10 #include "spin.h"
  11 #include "y.tab.h"
  12
  13 #define MAXDSTEP        2048    /* was 512 */
  14
  15 char    *NextLab[64];   /* must match value in pangen2.c:41 */
  16 int     Level=0, GenCode=0, IsGuard=0, TestOnly=0;
  17
  18 static int      Tj=0, Jt=0, LastGoto=0;
  19 static int      Tojump[MAXDSTEP], Jumpto[MAXDSTEP], Special[MAXDSTEP];
  20 static void     putCode(FILE *, Element *, Element *, Element *, int);
  21
  22 extern int      Pid, separate, OkBreak;
  23
  24 static void
  25 Sourced(int n, int special)
  26 {       int i;
  27         for (i = 0; i < Tj; i++)
  28                 if (Tojump[i] == n)
  29                         return;
  30         if (Tj >= MAXDSTEP)
  31                 fatal("d_step sequence too long", (char *)0);
  32         Special[Tj] = special;
  33         Tojump[Tj++] = n;
  34 }
  35
  36 static void
  37 Dested(int n)
  38 {       int i;
  39         for (i = 0; i < Tj; i++)
  40                 if (Tojump[i] == n)
  41                         return;
  42         for (i = 0; i < Jt; i++)
  43                 if (Jumpto[i] == n)
  44                         return;
  45         if (Jt >= MAXDSTEP)
  46                 fatal("d_step sequence too long", (char *)0);
  47         Jumpto[Jt++] = n;
  48         LastGoto = 1;
  49 }
  50
  51 static void
  52 Mopup(FILE *fd)
  53 {       int i, j;
  54
  55         for (i = 0; i < Jt; i++)
  56         {       for (j = 0; j < Tj; j++)
  57                         if (Tojump[j] == Jumpto[i])
  58                                 break;
  59                 if (j == Tj)
  60                 {       char buf[16];
  61                         if (Jumpto[i] == OkBreak)
  62                         {       if (!LastGoto)
  63                                 fprintf(fd, "S_%.3d_0:  /* break-dest */\n",
  64                                         OkBreak);
  65                         } else {
  66                                 sprintf(buf, "S_%.3d_0", Jumpto[i]);
  67                                 non_fatal("goto %s breaks from d_step seq", buf);
  68         }       }       }
  69         for (j = 0; j < Tj; j++)
  70         {       for (i = 0; i < Jt; i++)
  71                         if (Tojump[j] == Jumpto[i])
  72                                 break;
  73 #ifdef DEBUG
  74                 if (i == Jt && !Special[i])
  75                         fprintf(fd, "\t\t/* no goto's to S_%.3d_0 */\n",
  76                         Tojump[j]);
  77 #endif
  78         }
  79         for (j = i = 0; j < Tj; j++)
  80                 if (Special[j])
  81                 {       if (i >= MAXDSTEP)
  82                         {       fatal("cannot happen (dstep.c)", (char *)0);
  83                         }
  84                         Tojump[i] = Tojump[j];
  85                         Special[i] = 2;
  86                         i++;
  87                 }
  88         Tj = i; /* keep only the global exit-labels */
  89         Jt = 0;
  90 }
  91
  92 static int
  93 FirstTime(int n)
  94 {       int i;
  95         for (i = 0; i < Tj; i++)
  96                 if (Tojump[i] == n)
  97                         return (Special[i] <= 1);
  98         return 1;
  99 }
 100
 101 static void
 102 illegal(Element *e, char *str)
 103 {
 104         printf("illegal operator in 'd_step:' '");
 105         comment(stdout, e->n, 0);
 106         printf("'\n");
 107         fatal("'%s'", str);
 108 }
 109
 110 static void
 111 filterbad(Element *e)
 112 {
 113         switch (e->n->ntyp) {
 114         case ASSERT:
 115         case PRINT:
 116         case 'c':
 117                 /* run cannot be completely undone
 118                  * with sv_save-sv_restor
 119                  */
 120                 if (any_oper(e->n->lft, RUN))
 121                         illegal(e, "run operator in d_step");
 122
 123                 /* remote refs inside d_step sequences
 124                  * would be okay, but they cannot always
 125                  * be interpreted by the simulator the
 126                  * same as by the verifier (e.g., for an
 127                  * error trail)
 128                  */
 129                 if (any_oper(e->n->lft, 'p'))
 130                         illegal(e, "remote reference in d_step");
 131                 break;
 132         case '@':
 133                 illegal(e, "process termination");
 134                 break;
 135         case D_STEP:
 136                 illegal(e, "nested d_step sequence");
 137                 break;
 138         case ATOMIC:
 139                 illegal(e, "nested atomic sequence");
 140                 break;
 141         default:
 142                 break;
 143         }
 144 }
 145
 146 static int
 147 CollectGuards(FILE *fd, Element *e, int inh)
 148 {       SeqList *h; Element *ee;
 149
 150         for (h = e->sub; h; h = h->nxt)
 151         {       ee = huntstart(h->this->frst);
 152                 filterbad(ee);
 153                 switch (ee->n->ntyp) {
 154                 case NON_ATOMIC:
 155                         inh += CollectGuards(fd, ee->n->sl->this->frst, inh);
 156                         break;
 157                 case  IF:
 158                         inh += CollectGuards(fd, ee, inh);
 159                         break;
 160                 case '.':
 161                         if (ee->nxt->n->ntyp == DO)
 162                                 inh += CollectGuards(fd, ee->nxt, inh);
 163                         break;
 164                 case ELSE:
 165                         if (inh++ > 0) fprintf(fd, " || ");
 166 /* 4.2.5 */             if (!pid_is_claim(Pid))
 167                                 fprintf(fd, "(boq == -1 /* else */)");
 168                         else
 169                                 fprintf(fd, "(1 /* else */)");
 170                         break;
 171                 case 'R':
 172                         if (inh++ > 0) fprintf(fd, " || ");
 173                         fprintf(fd, "("); TestOnly=1;
 174                         putstmnt(fd, ee->n, ee->seqno);
 175                         fprintf(fd, ")"); TestOnly=0;
 176                         break;
 177                 case 'r':
 178                         if (inh++ > 0) fprintf(fd, " || ");
 179                         fprintf(fd, "("); TestOnly=1;
 180                         putstmnt(fd, ee->n, ee->seqno);
 181                         fprintf(fd, ")"); TestOnly=0;
 182                         break;
 183                 case 's':
 184                         if (inh++ > 0) fprintf(fd, " || ");
 185                         fprintf(fd, "("); TestOnly=1;
 186 /* 4.2.1 */             if (!pid_is_claim(Pid)) fprintf(fd, "(boq == -1) && ");
 187                         putstmnt(fd, ee->n, ee->seqno);
 188                         fprintf(fd, ")"); TestOnly=0;
 189                         break;
 190                 case 'c':
 191                         if (inh++ > 0) fprintf(fd, " || ");
 192                         fprintf(fd, "("); TestOnly=1;
 193                         if (!pid_is_claim(Pid))
 194                                 fprintf(fd, "(boq == -1 && ");
 195                         putstmnt(fd, ee->n->lft, e->seqno);
 196                         if (!pid_is_claim(Pid))
 197                                 fprintf(fd, ")");
 198                         fprintf(fd, ")"); TestOnly=0;
 199                         break;
 200         }       }
 201         return inh;
 202 }
 203
 204 int
 205 putcode(FILE *fd, Sequence *s, Element *nxt, int justguards, int ln, int seqno)
 206 {       int isg=0;
 207         static char buf[64];
 208
 209         NextLab[0] = "continue";
 210         filterbad(s->frst);
 211
 212         switch (s->frst->n->ntyp) {
 213         case UNLESS:
 214                 non_fatal("'unless' inside d_step - ignored", (char *) 0);
 215                 return putcode(fd, s->frst->n->sl->this, nxt, 0, ln, seqno);
 216         case NON_ATOMIC:
 217                 (void) putcode(fd, s->frst->n->sl->this, ZE, 1, ln, seqno);
 218                 if (justguards) return 0;       /* 6.2.5 */
 219                 break;
 220         case IF:
 221                 fprintf(fd, "if (!(");
 222                 if (!CollectGuards(fd, s->frst, 0))     /* what about boq? */
 223                         fprintf(fd, "1");
 224                 fprintf(fd, "))\n\t\t\tcontinue;");
 225                 isg = 1;
 226                 break;
 227         case '.':
 228                 if (s->frst->nxt->n->ntyp == DO)
 229                 {       fprintf(fd, "if (!(");
 230                         if (!CollectGuards(fd, s->frst->nxt, 0))
 231                                 fprintf(fd, "1");
 232                         fprintf(fd, "))\n\t\t\tcontinue;");
 233                         isg = 1;
 234                 }
 235                 break;
 236         case 'R': /* <- can't really happen (it's part of a 'c') */
 237                 fprintf(fd, "if (!("); TestOnly=1;
 238                 putstmnt(fd, s->frst->n, s->frst->seqno);
 239                 fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
 240                 break;
 241         case 'r':
 242                 fprintf(fd, "if (!("); TestOnly=1;
 243                 putstmnt(fd, s->frst->n, s->frst->seqno);
 244                 fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
 245                 break;
 246         case 's':
 247                 fprintf(fd, "if (");
 248 #if 1
 249 /* 4.2.1 */     if (!pid_is_claim(Pid)) fprintf(fd, "(boq != -1) || ");
 250 #endif
 251                 fprintf(fd, "!("); TestOnly=1;
 252                 putstmnt(fd, s->frst->n, s->frst->seqno);
 253                 fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
 254                 break;
 255         case 'c':
 256                 fprintf(fd, "if (!(");
 257                 if (!pid_is_claim(Pid)) fprintf(fd, "boq == -1 && ");
 258                 TestOnly=1;
 259                 putstmnt(fd, s->frst->n->lft, s->frst->seqno);
 260                 fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
 261                 break;
 262         case ELSE:
 263                 fprintf(fd, "if (boq != -1 || (");
 264                 if (separate != 2) fprintf(fd, "trpt->");
 265                 fprintf(fd, "o_pm&1))\n\t\t\tcontinue;");
 266                 {       extern FILE *th;
 267                         fprintf(th, "#ifndef ELSE_IN_GUARD\n");
 268                         fprintf(th, "   #define ELSE_IN_GUARD\n");
 269                         fprintf(th, "#endif\n");
 270                 }
 271                 break;
 272         case ASGN:      /* new 3.0.8 */
 273                 fprintf(fd, "IfNotBlocked");
 274                 break;
 275         default:
 276                 fprintf(fd, "/* default %d */\n\t\t", s->frst->n->ntyp);
 277         }
 278
 279         /* 6.2.5 : before TstOnly */
 280         fprintf(fd, "\n\n\t\treached[%d][%d] = 1;\n\t\t", Pid, seqno);
 281         fprintf(fd, "reached[%d][t->st] = 1;\n\t\t", Pid); /* next state */
 282         fprintf(fd, "reached[%d][tt] = 1;\n", Pid);     /* current state */
 283
 284         /* 6.2.5 : before sv_save() */
 285         if (s->frst->n->ntyp != NON_ATOMIC)
 286         fprintf(fd, "\n\t\tif (TstOnly) return 1;\n"); /* if called from enabled() */
 287
 288         if (justguards) return 0;
 289
 290         fprintf(fd, "\n\t\tsv_save();\n\t\t");
 291         sprintf(buf, "Uerror(\"block in d_step seq, line %d\")", ln);
 292         NextLab[0] = buf;
 293         putCode(fd, s->frst, s->extent, nxt, isg);
 294
 295         if (nxt)
 296         {       extern Symbol *Fname;
 297                 extern int lineno;
 298
 299                 if (FirstTime(nxt->Seqno)
 300                 && (!(nxt->status & DONE2) || !(nxt->status & D_ATOM)))
 301                 {       fprintf(fd, "S_%.3d_0: /* 1 */\n", nxt->Seqno);
 302                         nxt->status |= DONE2;
 303                         LastGoto = 0;
 304                 }
 305                 Sourced(nxt->Seqno, 1);
 306                 lineno = ln;
 307                 Fname = nxt->n->fn;
 308                 Mopup(fd);
 309         }
 310         unskip(s->frst->seqno);
 311         return LastGoto;
 312 }
 313
 314 static void
 315 putCode(FILE *fd, Element *f, Element *last, Element *next, int isguard)
 316 {       Element *e, *N;
 317         SeqList *h; int i;
 318         char NextOpt[64];
 319         static int bno = 0;
 320
 321         for (e = f; e; e = e->nxt)
 322         {       if (e->status & DONE2)
 323                         continue;
 324                 e->status |= DONE2;
 325
 326                 if (!(e->status & D_ATOM))
 327                 {       if (!LastGoto)
 328                         {       fprintf(fd, "\t\tgoto S_%.3d_0;\n",
 329                                         e->Seqno);
 330                                 Dested(e->Seqno);
 331                         }
 332                         break;
 333                 }
 334                 fprintf(fd, "S_%.3d_0: /* 2 */\n", e->Seqno);
 335                 LastGoto = 0;
 336                 Sourced(e->Seqno, 0);
 337
 338                 if (!e->sub)
 339                 {       filterbad(e);
 340                         switch (e->n->ntyp) {
 341                         case NON_ATOMIC:
 342                                 h = e->n->sl;
 343                                 putCode(fd, h->this->frst,
 344                                         h->this->extent, e->nxt, 0);
 345                                 break;
 346                         case BREAK:
 347                                 if (LastGoto) break;
 348                                 if (e->nxt)
 349                                 {       i = target( huntele(e->nxt,
 350                                                 e->status, -1))->Seqno;
 351                                         fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
 352                                         fprintf(fd, "/* 'break' */\n");
 353                                         Dested(i);
 354                                 } else
 355                                 {       if (next)
 356                                         {       fprintf(fd, "\t\tgoto S_%.3d_0;",
 357                                                         next->Seqno);
 358                                                 fprintf(fd, " /* NEXT */\n");
 359                                                 Dested(next->Seqno);
 360                                         } else
 361                                         fatal("cannot interpret d_step", 0);
 362                                 }
 363                                 break;
 364                         case GOTO:
 365                                 if (LastGoto) break;
 366                                 i = huntele( get_lab(e->n,1),
 367                                         e->status, -1)->Seqno;
 368                                 fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
 369                                 fprintf(fd, "/* 'goto' */\n");
 370                                 Dested(i);
 371                                 break;
 372                         case '.':
 373                                 if (LastGoto) break;
 374                                 if (e->nxt && (e->nxt->status & DONE2))
 375                                 {       i = e->nxt->Seqno;
 376                                         fprintf(fd, "\t\tgoto S_%.3d_0;", i);
 377                                         fprintf(fd, " /* '.' */\n");
 378                                         Dested(i);
 379                                 }
 380                                 break;
 381                         default:
 382                                 putskip(e->seqno);
 383                                 GenCode = 1; IsGuard = isguard;
 384                                 fprintf(fd, "\t\t");
 385                                 putstmnt(fd, e->n, e->seqno);
 386                                 fprintf(fd, ";\n");
 387                                 GenCode = IsGuard = isguard = LastGoto = 0;
 388                                 break;
 389                         }
 390                         i = e->nxt?e->nxt->Seqno:0;
 391                         if (e->nxt && (e->nxt->status & DONE2) && !LastGoto)
 392                         {       fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
 393                                 fprintf(fd, "/* ';' */\n");
 394                                 Dested(i);
 395                                 break;
 396                         }
 397                 } else
 398                 {       for (h = e->sub, i=1; h; h = h->nxt, i++)
 399                         {       sprintf(NextOpt, "goto S_%.3d_%d",
 400                                         e->Seqno, i);
 401                                 NextLab[++Level] = NextOpt;
 402                                 N = (e->n && e->n->ntyp == DO) ? e : e->nxt;
 403                                 putCode(fd, h->this->frst,
 404                                         h->this->extent, N, 1);
 405                                 Level--;
 406                                 fprintf(fd, "%s: /* 3 */\n", &NextOpt[5]);
 407                                 LastGoto = 0;
 408                         }
 409                         if (!LastGoto)
 410                         {       fprintf(fd, "\t\tUerror(\"blocking sel ");
 411                                 fprintf(fd, "in d_step (nr.%d, near line %d)\");\n",
 412                                 bno++, (e->n)?e->n->ln:0);
 413                                 LastGoto = 0;
 414                         }
 415                 }
 416                 if (e == last)
 417                 {       if (!LastGoto && next)
 418                         {       fprintf(fd, "\t\tgoto S_%.3d_0;\n",
 419                                         next->Seqno);
 420                                 Dested(next->Seqno);
 421                         }
 422                         break;
 423         }       }
 424 }