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 } 603