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