sys/src/cmd/spin/run.c

   1 /***** spin: run.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 <stdlib.h>
  13 #include "spin.h"
  14 #include "y.tab.h"
  15
  16 extern RunList  *X, *run;
  17 extern Symbol   *Fname;
  18 extern Element  *LastStep;
  19 extern int      Rvous, lineno, Tval, interactive, MadeChoice;
  20 extern int      TstOnly, verbose, s_trail, xspin, jumpsteps, depth;
  21 extern int      nproc, nstop, no_print, like_java;
  22
  23 static long     Seed = 1;
  24 static int      E_Check = 0, Escape_Check = 0;
  25
  26 static int      eval_sync(Element *);
  27 static int      pc_enabled(Lextok *n);
  28 extern void     sr_buf(int, int);
  29
  30 void
  31 Srand(unsigned int s)
  32 {       Seed = s;
  33 }
  34
  35 long
  36 Rand(void)
  37 {       /* CACM 31(10), Oct 1988 */
  38         Seed = 16807*(Seed%127773) - 2836*(Seed/127773);
  39         if (Seed <= 0) Seed += 2147483647;
  40         return Seed;
  41 }
  42
  43 Element *
  44 rev_escape(SeqList *e)
  45 {       Element *r;
  46
  47         if (!e)
  48                 return (Element *) 0;
  49
  50         if ((r = rev_escape(e->nxt)) != ZE) /* reversed order */
  51                 return r;
  52
  53         return eval_sub(e->this->frst);
  54 }
  55
  56 Element *
  57 eval_sub(Element *e)
  58 {       Element *f, *g;
  59         SeqList *z;
  60         int i, j, k;
  61
  62         if (!e->n)
  63                 return ZE;
  64 #ifdef DEBUG
  65         printf("\n\teval_sub(%d %s: line %d) ",
  66                 e->Seqno, e->esc?"+esc":"", e->n?e->n->ln:0);
  67         comment(stdout, e->n, 0);
  68         printf("\n");
  69 #endif
  70         if (e->n->ntyp == GOTO)
  71         {       if (Rvous) return ZE;
  72                 LastStep = e; f = get_lab(e->n, 1);
  73                 cross_dsteps(e->n, f->n);
  74                 return f;
  75         }
  76         if (e->n->ntyp == UNLESS)
  77         {       /* escapes were distributed into sequence */
  78                 return eval_sub(e->sub->this->frst);
  79         } else if (e->sub)      /* true for IF, DO, and UNLESS */
  80         {       Element *has_else = ZE;
  81                 Element *bas_else = ZE;
  82                 int nr_else = 0, nr_choices = 0;
  83
  84                 if (interactive
  85                 && !MadeChoice && !E_Check
  86                 && !Escape_Check
  87                 && !(e->status&(D_ATOM))
  88                 && depth >= jumpsteps)
  89                 {       printf("Select stmnt (");
  90                         whoruns(0); printf(")\n");
  91                         if (nproc-nstop > 1)
  92                         printf("\tchoice 0: other process\n");
  93                 }
  94                 for (z = e->sub, j=0; z; z = z->nxt)
  95                 {       j++;
  96                         if (interactive
  97                         && !MadeChoice && !E_Check
  98                         && !Escape_Check
  99                         && !(e->status&(D_ATOM))
 100                         && depth >= jumpsteps
 101                         && z->this->frst
 102                         && (xspin || (verbose&32) || Enabled0(z->this->frst)))
 103                         {       if (z->this->frst->n->ntyp == ELSE)
 104                                 {       has_else = (Rvous)?ZE:z->this->frst->nxt;
 105                                         nr_else = j;
 106                                         continue;
 107                                 }
 108                                 printf("\tchoice %d: ", j);
 109 #if 0
 110                                 if (z->this->frst->n)
 111                                         printf("line %d, ", z->this->frst->n->ln);
 112 #endif
 113                                 if (!Enabled0(z->this->frst))
 114                                         printf("unexecutable, ");
 115                                 else
 116                                         nr_choices++;
 117                                 comment(stdout, z->this->frst->n, 0);
 118                                 printf("\n");
 119                 }       }
 120
 121                 if (nr_choices == 0 && has_else)
 122                         printf("\tchoice %d: (else)\n", nr_else);
 123
 124                 if (interactive && depth >= jumpsteps
 125                 && !Escape_Check
 126                 && !(e->status&(D_ATOM))
 127                 && !E_Check)
 128                 {       if (!MadeChoice)
 129                         {       char buf[256];
 130                                 if (xspin)
 131                                         printf("Make Selection %d\n\n", j);
 132                                 else
 133                                         printf("Select [0-%d]: ", j);
 134                                 fflush(stdout);
 135                                 scanf("%s", buf);
 136                                 if (isdigit(buf[0]))
 137                                         k = atoi(buf);
 138                                 else
 139                                 {       if (buf[0] == 'q')
 140                                                 alldone(0);
 141                                         k = -1;
 142                                 }
 143                         } else
 144                         {       k = MadeChoice;
 145                                 MadeChoice = 0;
 146                         }
 147                         if (k < 1 || k > j)
 148                         {       if (k != 0) printf("\tchoice outside range\n");
 149                                 return ZE;
 150                         }
 151                         k--;
 152                 } else
 153                 {       if (e->n && e->n->indstep >= 0)
 154                                 k = 0;  /* select 1st executable guard */
 155                         else
 156                                 k = Rand()%j;   /* nondeterminism */
 157                 }
 158                 has_else = ZE;
 159                 bas_else = ZE;
 160                 for (i = 0, z = e->sub; i < j+k; i++)
 161                 {       if (z->this->frst
 162                         &&  z->this->frst->n->ntyp == ELSE)
 163                         {       bas_else = z->this->frst;
 164                                 has_else = (Rvous)?ZE:bas_else->nxt;
 165                                 if (!interactive || depth < jumpsteps
 166                                 || Escape_Check
 167                                 || (e->status&(D_ATOM)))
 168                                 {       z = (z->nxt)?z->nxt:e->sub;
 169                                         continue;
 170                                 }
 171                         }
 172                         if (z->this->frst
 173                         &&  ((z->this->frst->n->ntyp == ATOMIC
 174                           ||  z->this->frst->n->ntyp == D_STEP)
 175                           &&  z->this->frst->n->sl->this->frst->n->ntyp == ELSE))
 176                         {       bas_else = z->this->frst->n->sl->this->frst;
 177                                 has_else = (Rvous)?ZE:bas_else->nxt;
 178                                 if (!interactive || depth < jumpsteps
 179                                 || Escape_Check
 180                                 || (e->status&(D_ATOM)))
 181                                 {       z = (z->nxt)?z->nxt:e->sub;
 182                                         continue;
 183                                 }
 184                         }
 185                         if (i >= k)
 186                         {       if ((f = eval_sub(z->this->frst)) != ZE)
 187                                         return f;
 188                                 else if (interactive && depth >= jumpsteps
 189                                 && !(e->status&(D_ATOM)))
 190                                 {       if (!E_Check && !Escape_Check)
 191                                                 printf("\tunexecutable\n");
 192                                         return ZE;
 193                         }       }
 194                         z = (z->nxt)?z->nxt:e->sub;
 195                 }
 196                 LastStep = bas_else;
 197                 return has_else;
 198         } else
 199         {       if (e->n->ntyp == ATOMIC
 200                 ||  e->n->ntyp == D_STEP)
 201                 {       f = e->n->sl->this->frst;
 202                         g = e->n->sl->this->last;
 203                         g->nxt = e->nxt;
 204                         if (!(g = eval_sub(f))) /* atomic guard */
 205                                 return ZE;
 206                         return g;
 207                 } else if (e->n->ntyp == NON_ATOMIC)
 208                 {       f = e->n->sl->this->frst;
 209                         g = e->n->sl->this->last;
 210                         g->nxt = e->nxt;                /* close it */
 211                         return eval_sub(f);
 212                 } else if (e->n->ntyp == '.')
 213                 {       if (!Rvous) return e->nxt;
 214                         return eval_sub(e->nxt);
 215                 } else
 216                 {       SeqList *x;
 217                         if (!(e->status & (D_ATOM))
 218                         &&  e->esc && verbose&32)
 219                         {       printf("Stmnt [");
 220                                 comment(stdout, e->n, 0);
 221                                 printf("] has escape(s): ");
 222                                 for (x = e->esc; x; x = x->nxt)
 223                                 {       printf("[");
 224                                         g = x->this->frst;
 225                                         if (g->n->ntyp == ATOMIC
 226                                         ||  g->n->ntyp == NON_ATOMIC)
 227                                                 g = g->n->sl->this->frst;
 228                                         comment(stdout, g->n, 0);
 229                                         printf("] ");
 230                                 }
 231                                 printf("\n");
 232                         }
 233 #if 0
 234                         if (!(e->status & D_ATOM))      /* escapes don't reach inside d_steps */
 235                         /* 4.2.4: only the guard of a d_step can have an escape */
 236 #endif
 237                         {       Escape_Check++;
 238                                 if (like_java)
 239                                 {       if ((g = rev_escape(e->esc)) != ZE)
 240                                         {       if (verbose&4)
 241                                                         printf("\tEscape taken\n");
 242                                                 Escape_Check--;
 243                                                 return g;
 244                                         }
 245                                 } else
 246                                 {       for (x = e->esc; x; x = x->nxt)
 247                                         {       if ((g = eval_sub(x->this->frst)) != ZE)
 248                                                 {       if (verbose&4)
 249                                                                 printf("\tEscape taken\n");
 250                                                         Escape_Check--;
 251                                                         return g;
 252                                 }       }       }
 253                                 Escape_Check--;
 254                         }
 255
 256                         switch (e->n->ntyp) {
 257                         case TIMEOUT: case RUN:
 258                         case PRINT: case PRINTM:
 259                         case C_CODE: case C_EXPR:
 260                         case ASGN: case ASSERT:
 261                         case 's': case 'r': case 'c':
 262                                 /* toplevel statements only */
 263                                 LastStep = e;
 264                         default:
 265                                 break;
 266                         }
 267                         if (Rvous)
 268                         {
 269                                 return (eval_sync(e))?e->nxt:ZE;
 270                         }
 271                         return (eval(e->n))?e->nxt:ZE;
 272                 }
 273         }
 274         return ZE; /* not reached */
 275 }
 276
 277 static int
 278 eval_sync(Element *e)
 279 {       /* allow only synchronous receives
 280            and related node types    */
 281         Lextok *now = (e)?e->n:ZN;
 282
 283         if (!now
 284         ||  now->ntyp != 'r'
 285         ||  now->val >= 2       /* no rv with a poll */
 286         ||  !q_is_sync(now))
 287         {
 288                 return 0;
 289         }
 290
 291         LastStep = e;
 292         return eval(now);
 293 }
 294
 295 static int
 296 assign(Lextok *now)
 297 {       int t;
 298
 299         if (TstOnly) return 1;
 300
 301         switch (now->rgt->ntyp) {
 302         case FULL:      case NFULL:
 303         case EMPTY:     case NEMPTY:
 304         case RUN:       case LEN:
 305                 t = BYTE;
 306                 break;
 307         default:
 308                 t = Sym_typ(now->rgt);
 309                 break;
 310         }
 311         typ_ck(Sym_typ(now->lft), t, "assignment");
 312         return setval(now->lft, eval(now->rgt));
 313 }
 314
 315 static int
 316 nonprogress(void)       /* np_ */
 317 {       RunList *r;
 318
 319         for (r = run; r; r = r->nxt)
 320         {       if (has_lab(r->pc, 4))  /* 4=progress */
 321                         return 0;
 322         }
 323         return 1;
 324 }
 325
 326 int
 327 eval(Lextok *now)
 328 {
 329         if (now) {
 330         lineno = now->ln;
 331         Fname  = now->fn;
 332 #ifdef DEBUG
 333         printf("eval ");
 334         comment(stdout, now, 0);
 335         printf("\n");
 336 #endif
 337         switch (now->ntyp) {
 338         case CONST: return now->val;
 339         case   '!': return !eval(now->lft);
 340         case  UMIN: return -eval(now->lft);
 341         case   '~': return ~eval(now->lft);
 342
 343         case   '/': return (eval(now->lft) / eval(now->rgt));
 344         case   '*': return (eval(now->lft) * eval(now->rgt));
 345         case   '-': return (eval(now->lft) - eval(now->rgt));
 346         case   '+': return (eval(now->lft) + eval(now->rgt));
 347         case   '%': return (eval(now->lft) % eval(now->rgt));
 348         case    LT: return (eval(now->lft) <  eval(now->rgt));
 349         case    GT: return (eval(now->lft) >  eval(now->rgt));
 350         case   '&': return (eval(now->lft) &  eval(now->rgt));
 351         case   '^': return (eval(now->lft) ^  eval(now->rgt));
 352         case   '|': return (eval(now->lft) |  eval(now->rgt));
 353         case    LE: return (eval(now->lft) <= eval(now->rgt));
 354         case    GE: return (eval(now->lft) >= eval(now->rgt));
 355         case    NE: return (eval(now->lft) != eval(now->rgt));
 356         case    EQ: return (eval(now->lft) == eval(now->rgt));
 357         case    OR: return (eval(now->lft) || eval(now->rgt));
 358         case   AND: return (eval(now->lft) && eval(now->rgt));
 359         case LSHIFT: return (eval(now->lft) << eval(now->rgt));
 360         case RSHIFT: return (eval(now->lft) >> eval(now->rgt));
 361         case   '?': return (eval(now->lft) ? eval(now->rgt->lft)
 362                                            : eval(now->rgt->rgt));
 363
 364         case     'p': return remotevar(now);    /* _p for remote reference */
 365         case     'q': return remotelab(now);
 366         case     'R': return qrecv(now, 0);     /* test only    */
 367         case     LEN: return qlen(now);
 368         case    FULL: return (qfull(now));
 369         case   EMPTY: return (qlen(now)==0);
 370         case   NFULL: return (!qfull(now));
 371         case  NEMPTY: return (qlen(now)>0);
 372         case ENABLED: if (s_trail) return 1;
 373                       return pc_enabled(now->lft);
 374         case    EVAL: return eval(now->lft);
 375         case  PC_VAL: return pc_value(now->lft);
 376         case NONPROGRESS: return nonprogress();
 377         case    NAME: return getval(now);
 378
 379         case TIMEOUT: return Tval;
 380         case     RUN: return TstOnly?1:enable(now);
 381
 382         case   's': return qsend(now);          /* send         */
 383         case   'r': return qrecv(now, 1);       /* receive or poll */
 384         case   'c': return eval(now->lft);      /* condition    */
 385         case PRINT: return TstOnly?1:interprint(stdout, now);
 386         case PRINTM: return TstOnly?1:printm(stdout, now);
 387         case  ASGN: return assign(now);
 388
 389         case C_CODE: printf("%s:\t", now->sym->name);
 390                      plunk_inline(stdout, now->sym->name, 0);
 391                      return 1; /* uninterpreted */
 392
 393         case C_EXPR: printf("%s:\t", now->sym->name);
 394                      plunk_expr(stdout, now->sym->name);
 395                      printf("\n");
 396                      return 1; /* uninterpreted */
 397
 398         case ASSERT: if (TstOnly || eval(now->lft)) return 1;
 399                      non_fatal("assertion violated", (char *) 0);
 400                         printf("spin: text of failed assertion: assert(");
 401                         comment(stdout, now->lft, 0);
 402                         printf(")\n");
 403                      if (s_trail && !xspin) return 1;
 404                      wrapup(1); /* doesn't return */
 405
 406         case  IF: case DO: case BREAK: case UNLESS:     /* compound */
 407         case   '.': return 1;   /* return label for compound */
 408         case   '@': return 0;   /* stop state */
 409         case  ELSE: return 1;   /* only hit here in guided trails */
 410         default   : printf("spin: bad node type %d (run)\n", now->ntyp);
 411                     if (s_trail) printf("spin: trail file doesn't match spec?\n");
 412                     fatal("aborting", 0);
 413         }}
 414         return 0;
 415 }
 416
 417 int
 418 printm(FILE *fd, Lextok *n)
 419 {       extern char Buf[];
 420         int j;
 421
 422         Buf[0] = '\0';
 423         if (!no_print)
 424         if (!s_trail || depth >= jumpsteps) {
 425                 if (n->lft->ismtyp)
 426                         j = n->lft->val;
 427                 else
 428                         j = eval(n->lft);
 429                 Buf[0] = '\0';
 430                 sr_buf(j, 1);
 431                 dotag(fd, Buf);
 432         }
 433         return 1;
 434 }
 435
 436 int
 437 interprint(FILE *fd, Lextok *n)
 438 {       Lextok *tmp = n->lft;
 439         char c, *s = n->sym->name;
 440         int i, j; char lbuf[512];
 441         extern char Buf[];
 442         char tBuf[4096];
 443
 444         Buf[0] = '\0';
 445         if (!no_print)
 446         if (!s_trail || depth >= jumpsteps) {
 447         for (i = 0; i < (int) strlen(s); i++)
 448                 switch (s[i]) {
 449                 case '\"': break; /* ignore */
 450                 case '\\':
 451                          switch(s[++i]) {
 452                          case 't': strcat(Buf, "\t"); break;
 453                          case 'n': strcat(Buf, "\n"); break;
 454                          default:  goto onechar;
 455                          }
 456                          break;
 457                 case  '%':
 458                          if ((c = s[++i]) == '%')
 459                          {      strcat(Buf, "%"); /* literal */
 460                                 break;
 461                          }
 462                          if (!tmp)
 463                          {      non_fatal("too few print args %s", s);
 464                                 break;
 465                          }
 466                          j = eval(tmp->lft);
 467                          tmp = tmp->rgt;
 468                          switch(c) {
 469                          case 'c': sprintf(lbuf, "%c", j); break;
 470                          case 'd': sprintf(lbuf, "%d", j); break;
 471
 472                          case 'e': strcpy(tBuf, Buf);   /* event name */
 473                                    Buf[0] = '\0';
 474                                    sr_buf(j, 1);
 475                                    strcpy(lbuf, Buf);
 476                                    strcpy(Buf, tBuf);
 477                                    break;
 478
 479                          case 'o': sprintf(lbuf, "%o", j); break;
 480                          case 'u': sprintf(lbuf, "%u", (unsigned) j); break;
 481                          case 'x': sprintf(lbuf, "%x", j); break;
 482                          default:  non_fatal("bad print cmd: '%s'", &s[i-1]);
 483                                    lbuf[0] = '\0'; break;
 484                          }
 485                          goto append;
 486                 default:
 487 onechar:                 lbuf[0] = s[i]; lbuf[1] = '\0';
 488 append:                  strcat(Buf, lbuf);
 489                          break;
 490                 }
 491                 dotag(fd, Buf);
 492         }
 493         if (strlen(Buf) > 4096) fatal("printf string too long", 0);
 494         return 1;
 495 }
 496
 497 static int
 498 Enabled1(Lextok *n)
 499 {       int i; int v = verbose;
 500
 501         if (n)
 502         switch (n->ntyp) {
 503         case 'c':
 504                 if (has_typ(n->lft, RUN))
 505                         return 1;       /* conservative */
 506                 /* else fall through */
 507         default:        /* side-effect free */
 508                 verbose = 0;
 509                 E_Check++;
 510                 i = eval(n);
 511                 E_Check--;
 512                 verbose = v;
 513                 return i;
 514
 515         case C_CODE: case C_EXPR:
 516         case PRINT: case PRINTM:
 517         case   ASGN: case ASSERT:
 518                 return 1;
 519
 520         case 's':
 521                 if (q_is_sync(n))
 522                 {       if (Rvous) return 0;
 523                         TstOnly = 1; verbose = 0;
 524                         E_Check++;
 525                         i = eval(n);
 526                         E_Check--;
 527                         TstOnly = 0; verbose = v;
 528                         return i;
 529                 }
 530                 return (!qfull(n));
 531         case 'r':
 532                 if (q_is_sync(n))
 533                         return 0;       /* it's never a user-choice */
 534                 n->ntyp = 'R'; verbose = 0;
 535                 E_Check++;
 536                 i = eval(n);
 537                 E_Check--;
 538                 n->ntyp = 'r'; verbose = v;
 539                 return i;
 540         }
 541         return 0;
 542 }
 543
 544 int
 545 Enabled0(Element *e)
 546 {       SeqList *z;
 547
 548         if (!e || !e->n)
 549                 return 0;
 550
 551         switch (e->n->ntyp) {
 552         case '@':
 553                 return X->pid == (nproc-nstop-1);
 554         case '.':
 555                 return 1;
 556         case GOTO:
 557                 if (Rvous) return 0;
 558                 return 1;
 559         case UNLESS:
 560                 return Enabled0(e->sub->this->frst);
 561         case ATOMIC:
 562         case D_STEP:
 563         case NON_ATOMIC:
 564                 return Enabled0(e->n->sl->this->frst);
 565         }
 566         if (e->sub)     /* true for IF, DO, and UNLESS */
 567         {       for (z = e->sub; z; z = z->nxt)
 568                         if (Enabled0(z->this->frst))
 569                                 return 1;
 570                 return 0;
 571         }
 572         for (z = e->esc; z; z = z->nxt)
 573         {       if (Enabled0(z->this->frst))
 574                         return 1;
 575         }
 576 #if 0
 577         printf("enabled1 ");
 578         comment(stdout, e->n, 0);
 579         printf(" ==> %s\n", Enabled1(e->n)?"yes":"nope");
 580 #endif
 581         return Enabled1(e->n);
 582 }
 583
 584 int
 585 pc_enabled(Lextok *n)
 586 {       int i = nproc - nstop;
 587         int pid = eval(n);
 588         int result = 0;
 589         RunList *Y, *oX;
 590
 591         if (pid == X->pid)
 592                 fatal("used: enabled(pid=thisproc) [%s]", X->n->name);
 593
 594         for (Y = run; Y; Y = Y->nxt)
 595                 if (--i == pid)
 596                 {       oX = X; X = Y;
 597                         result = Enabled0(Y->pc);
 598                         X = oX;
 599                         break;
 600                 }
 601         return result;
 602 }