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