sys/src/cmd/spin/dstep.c

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