verif/Spin/Src5.1.6/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 || !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;
  73                 f = get_lab(e->n, 1);
  74                 cross_dsteps(e->n, f->n);
  75                 return f;
  76         }
  77         if (e->n->ntyp == UNLESS)
  78         {       /* escapes were distributed into sequence */
  79                 return eval_sub(e->sub->this->frst);
  80         } else if (e->sub)      /* true for IF, DO, and UNLESS */
  81         {       Element *has_else = ZE;
  82                 Element *bas_else = ZE;
  83                 int nr_else = 0, nr_choices = 0;
  84
  85                 if (interactive
  86                 && !MadeChoice && !E_Check
  87                 && !Escape_Check
  88                 && !(e->status&(D_ATOM))
  89                 && depth >= jumpsteps)
  90                 {       printf("Select stmnt (");
  91                         whoruns(0); printf(")\n");
  92                         if (nproc-nstop > 1)
  93                         printf("\tchoice 0: other process\n");
  94                 }
  95                 for (z = e->sub, j=0; z; z = z->nxt)
  96                 {       j++;
  97                         if (interactive
  98                         && !MadeChoice && !E_Check
  99                         && !Escape_Check
 100                         && !(e->status&(D_ATOM))
 101                         && depth >= jumpsteps
 102                         && z->this->frst
 103                         && (xspin || (verbose&32) || Enabled0(z->this->frst)))
 104                         {       if (z->this->frst->n->ntyp == ELSE)
 105                                 {       has_else = (Rvous)?ZE:z->this->frst->nxt;
 106                                         nr_else = j;
 107                                         continue;
 108                                 }
 109                                 printf("\tchoice %d: ", j);
 110 #if 0
 111                                 if (z->this->frst->n)
 112                                         printf("line %d, ", z->this->frst->n->ln);
 113 #endif
 114                                 if (!Enabled0(z->this->frst))
 115                                         printf("unexecutable, ");
 116                                 else
 117                                         nr_choices++;
 118                                 comment(stdout, z->this->frst->n, 0);
 119                                 printf("\n");
 120                 }       }
 121
 122                 if (nr_choices == 0 && has_else)
 123                         printf("\tchoice %d: (else)\n", nr_else);
 124
 125                 if (interactive && depth >= jumpsteps
 126                 && !Escape_Check
 127                 && !(e->status&(D_ATOM))
 128                 && !E_Check)
 129                 {       if (!MadeChoice)
 130                         {       char buf[256];
 131                                 if (xspin)
 132                                         printf("Make Selection %d\n\n", j);
 133                                 else
 134                                         printf("Select [0-%d]: ", j);
 135                                 fflush(stdout);
 136                                 scanf("%64s", buf);
 137                                 if (isdigit(buf[0]))
 138                                         k = atoi(buf);
 139                                 else
 140                                 {       if (buf[0] == 'q')
 141                                                 alldone(0);
 142                                         k = -1;
 143                                 }
 144                         } else
 145                         {       k = MadeChoice;
 146                                 MadeChoice = 0;
 147                         }
 148                         if (k < 1 || k > j)
 149                         {       if (k != 0) printf("\tchoice outside range\n");
 150                                 return ZE;
 151                         }
 152                         k--;
 153                 } else
 154                 {       if (e->n && e->n->indstep >= 0)
 155                                 k = 0;  /* select 1st executable guard */
 156                         else
 157                                 k = Rand()%j;   /* nondeterminism */
 158                 }
 159                 has_else = ZE;
 160                 bas_else = ZE;
 161                 for (i = 0, z = e->sub; i < j+k; i++)
 162                 {       if (z->this->frst
 163                         &&  z->this->frst->n->ntyp == ELSE)
 164                         {       bas_else = z->this->frst;
 165                                 has_else = (Rvous)?ZE:bas_else->nxt;
 166                                 if (!interactive || depth < jumpsteps
 167                                 || Escape_Check
 168                                 || (e->status&(D_ATOM)))
 169                                 {       z = (z->nxt)?z->nxt:e->sub;
 170                                         continue;
 171                                 }
 172                         }
 173                         if (z->this->frst
 174                         &&  ((z->this->frst->n->ntyp == ATOMIC
 175                           ||  z->this->frst->n->ntyp == D_STEP)
 176                           &&  z->this->frst->n->sl->this->frst->n->ntyp == ELSE))
 177                         {       bas_else = z->this->frst->n->sl->this->frst;
 178                                 has_else = (Rvous)?ZE:bas_else->nxt;
 179                                 if (!interactive || depth < jumpsteps
 180                                 || Escape_Check
 181                                 || (e->status&(D_ATOM)))
 182                                 {       z = (z->nxt)?z->nxt:e->sub;
 183                                         continue;
 184                                 }
 185                         }
 186                         if (i >= k)
 187                         {       if ((f = eval_sub(z->this->frst)) != ZE)
 188                                         return f;
 189                                 else if (interactive && depth >= jumpsteps
 190                                 && !(e->status&(D_ATOM)))
 191                                 {       if (!E_Check && !Escape_Check)
 192                                                 printf("\tunexecutable\n");
 193                                         return ZE;
 194                         }       }
 195                         z = (z->nxt)?z->nxt:e->sub;
 196                 }
 197                 LastStep = bas_else;
 198                 return has_else;
 199         } else
 200         {       if (e->n->ntyp == ATOMIC
 201                 ||  e->n->ntyp == D_STEP)
 202                 {       f = e->n->sl->this->frst;
 203                         g = e->n->sl->this->last;
 204                         g->nxt = e->nxt;
 205                         if (!(g = eval_sub(f))) /* atomic guard */
 206                                 return ZE;
 207                         return g;
 208                 } else if (e->n->ntyp == NON_ATOMIC)
 209                 {       f = e->n->sl->this->frst;
 210                         g = e->n->sl->this->last;
 211                         g->nxt = e->nxt;                /* close it */
 212                         return eval_sub(f);
 213                 } else if (e->n->ntyp == '.')
 214                 {       if (!Rvous) return e->nxt;
 215                         return eval_sub(e->nxt);
 216                 } else
 217                 {       SeqList *x;
 218                         if (!(e->status & (D_ATOM))
 219                         &&  e->esc && verbose&32)
 220                         {       printf("Stmnt [");
 221                                 comment(stdout, e->n, 0);
 222                                 printf("] has escape(s): ");
 223                                 for (x = e->esc; x; x = x->nxt)
 224                                 {       printf("[");
 225                                         g = x->this->frst;
 226                                         if (g->n->ntyp == ATOMIC
 227                                         ||  g->n->ntyp == NON_ATOMIC)
 228                                                 g = g->n->sl->this->frst;
 229                                         comment(stdout, g->n, 0);
 230                                         printf("] ");
 231                                 }
 232                                 printf("\n");
 233                         }
 234 #if 0
 235                         if (!(e->status & D_ATOM))      /* escapes don't reach inside d_steps */
 236                         /* 4.2.4: only the guard of a d_step can have an escape */
 237 #endif
 238                         {       Escape_Check++;
 239                                 if (like_java)
 240                                 {       if ((g = rev_escape(e->esc)) != ZE)
 241                                         {       if (verbose&4)
 242                                                         printf("\tEscape taken\n");
 243                                                 Escape_Check--;
 244                                                 return g;
 245                                         }
 246                                 } else
 247                                 {       for (x = e->esc; x; x = x->nxt)
 248                                         {       if ((g = eval_sub(x->this->frst)) != ZE)
 249                                                 {       if (verbose&4)
 250                                                                 printf("\tEscape taken\n");
 251                                                         Escape_Check--;
 252                                                         return g;
 253                                 }       }       }
 254                                 Escape_Check--;
 255                         }
 256
 257                         switch (e->n->ntyp) {
 258                         case TIMEOUT: case RUN:
 259                         case PRINT: case PRINTM:
 260                         case C_CODE: case C_EXPR:
 261                         case ASGN: case ASSERT:
 262                         case 's': case 'r': case 'c':
 263                                 /* toplevel statements only */
 264                                 LastStep = e;
 265                         default:
 266                                 break;
 267                         }
 268                         if (Rvous)
 269                         {
 270                                 return (eval_sync(e))?e->nxt:ZE;
 271                         }
 272                         return (eval(e->n))?e->nxt:ZE;
 273                 }
 274         }
 275         return ZE; /* not reached */
 276 }
 277
 278 static int
 279 eval_sync(Element *e)
 280 {       /* allow only synchronous receives
 281            and related node types    */
 282         Lextok *now = (e)?e->n:ZN;
 283
 284         if (!now
 285         ||  now->ntyp != 'r'
 286         ||  now->val >= 2       /* no rv with a poll */
 287         ||  !q_is_sync(now))
 288         {
 289                 return 0;
 290         }
 291
 292         LastStep = e;
 293         return eval(now);
 294 }
 295
 296 static int
 297 assign(Lextok *now)
 298 {       int t;
 299
 300         if (TstOnly) return 1;
 301
 302         switch (now->rgt->ntyp) {
 303         case FULL:      case NFULL:
 304         case EMPTY:     case NEMPTY:
 305         case RUN:       case LEN:
 306                 t = BYTE;
 307                 break;
 308         default:
 309                 t = Sym_typ(now->rgt);
 310                 break;
 311         }
 312         typ_ck(Sym_typ(now->lft), t, "assignment");
 313         return setval(now->lft, eval(now->rgt));
 314 }
 315
 316 static int
 317 nonprogress(void)       /* np_ */
 318 {       RunList *r;
 319
 320         for (r = run; r; r = r->nxt)
 321         {       if (has_lab(r->pc, 4))  /* 4=progress */
 322                         return 0;
 323         }
 324         return 1;
 325 }
 326
 327 int
 328 eval(Lextok *now)
 329 {
 330         if (now) {
 331         lineno = now->ln;
 332         Fname  = now->fn;
 333 #ifdef DEBUG
 334         printf("eval ");
 335         comment(stdout, now, 0);
 336         printf("\n");
 337 #endif
 338         switch (now->ntyp) {
 339         case CONST: return now->val;
 340         case   '!': return !eval(now->lft);
 341         case  UMIN: return -eval(now->lft);
 342         case   '~': return ~eval(now->lft);
 343
 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   '%': return (eval(now->lft) % eval(now->rgt));
 349         case    LT: return (eval(now->lft) <  eval(now->rgt));
 350         case    GT: 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   '|': return (eval(now->lft) |  eval(now->rgt));
 354         case    LE: return (eval(now->lft) <= eval(now->rgt));
 355         case    GE: return (eval(now->lft) >= eval(now->rgt));
 356         case    NE: return (eval(now->lft) != eval(now->rgt));
 357         case    EQ: return (eval(now->lft) == eval(now->rgt));
 358         case    OR: return (eval(now->lft) || eval(now->rgt));
 359         case   AND: return (eval(now->lft) && eval(now->rgt));
 360         case LSHIFT: return (eval(now->lft) << eval(now->rgt));
 361         case RSHIFT: return (eval(now->lft) >> eval(now->rgt));
 362         case   '?': return (eval(now->lft) ? eval(now->rgt->lft)
 363                                            : eval(now->rgt->rgt));
 364
 365         case     'p': return remotevar(now);    /* _p for remote reference */
 366         case     'q': return remotelab(now);
 367         case     'R': return qrecv(now, 0);     /* test only    */
 368         case     LEN: return qlen(now);
 369         case    FULL: return (qfull(now));
 370         case   EMPTY: return (qlen(now)==0);
 371         case   NFULL: return (!qfull(now));
 372         case  NEMPTY: return (qlen(now)>0);
 373         case ENABLED: if (s_trail) return 1;
 374                       return pc_enabled(now->lft);
 375         case    EVAL: return eval(now->lft);
 376         case  PC_VAL: return pc_value(now->lft);
 377         case NONPROGRESS: return nonprogress();
 378         case    NAME: return getval(now);
 379
 380         case TIMEOUT: return Tval;
 381         case     RUN: return TstOnly?1:enable(now);
 382
 383         case   's': return qsend(now);          /* send         */
 384         case   'r': return qrecv(now, 1);       /* receive or poll */
 385         case   'c': return eval(now->lft);      /* condition    */
 386         case PRINT: return TstOnly?1:interprint(stdout, now);
 387         case PRINTM: return TstOnly?1:printm(stdout, now);
 388         case  ASGN: return assign(now);
 389
 390         case C_CODE: printf("%s:\t", now->sym->name);
 391                      plunk_inline(stdout, now->sym->name, 0);
 392                      return 1; /* uninterpreted */
 393
 394         case C_EXPR: printf("%s:\t", now->sym->name);
 395                      plunk_expr(stdout, now->sym->name);
 396                      printf("\n");
 397                      return 1; /* uninterpreted */
 398
 399         case ASSERT: if (TstOnly || eval(now->lft)) return 1;
 400                      non_fatal("assertion violated", (char *) 0);
 401                         printf("spin: text of failed assertion: assert(");
 402                         comment(stdout, now->lft, 0);
 403                         printf(")\n");
 404                      if (s_trail && !xspin) return 1;
 405                      wrapup(1); /* doesn't return */
 406
 407         case  IF: case DO: case BREAK: case UNLESS:     /* compound */
 408         case   '.': return 1;   /* return label for compound */
 409         case   '@': return 0;   /* stop state */
 410         case  ELSE: return 1;   /* only hit here in guided trails */
 411         default   : printf("spin: bad node type %d (run)\n", now->ntyp);
 412                     if (s_trail) printf("spin: trail file doesn't match spec?\n");
 413                     fatal("aborting", 0);
 414         }}
 415         return 0;
 416 }
 417
 418 int
 419 printm(FILE *fd, Lextok *n)
 420 {       extern char Buf[];
 421         int j;
 422
 423         Buf[0] = '\0';
 424         if (!no_print)
 425         if (!s_trail || depth >= jumpsteps) {
 426                 if (n->lft->ismtyp)
 427                         j = n->lft->val;
 428                 else
 429                         j = eval(n->lft);
 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]; /* matches value in sr_buf() */
 441         extern char Buf[];      /* global, size 4096 */
 442         char tBuf[4096];        /* match size of global Buf[] */
 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 }