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