1 /***** spin: main.c *****/ 2 3 /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */ 4 /* 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.att.com */ 12 13 #include "spin.h" 14 #include <signal.h> 15 #include <stdlib.h> 16 #include <unistd.h> 17 #include "y.tab.h" 18 19 extern int DstepStart, lineno; 20 extern FILE *yyin; 21 22 Symbol *Fname, *oFname; 23 24 int verbose = 0; 25 int analyze = 0; 26 int s_trail = 0; 27 int m_loss = 0; 28 int dumptab = 0; 29 int nr_errs = 0; 30 int dataflow = 0; 31 int has_remote = 0; 32 int Interactive = 0; 33 int Ntimeouts = 0; /* counts those used in never claim */ 34 int Etimeouts = 0; /* counts those used in program */ 35 int xspin = 0; /* set when used with xspin interface */ 36 37 void 38 main(int argc, char *argv[]) 39 { Symbol *s; 40 int T = (int) time((long *)0); 41 42 while (argc > 1 && argv[1][0] == '-') 43 { switch (argv[1][1]) { 44 case 'a': analyze = 1; break; 45 case 'd': dumptab = 1; break; 46 case 'D': dataflow++; break; 47 case 'g': verbose += 1; break; 48 case 'i': Interactive = 1; break; 49 case 'l': verbose += 2; break; 50 case 'm': m_loss = 1; break; 51 case 'n': T = atoi(&argv[1][2]); break; 52 case 'p': verbose += 4; break; 53 case 'r': verbose += 8; break; 54 case 's': verbose += 16; break; 55 case 't': s_trail = 1; break; 56 case 'v': verbose += 32; break; 57 case 'V': printf("%s\n", Version); exit(0); 58 case 'X': xspin = 1; 59 signal(SIGPIPE, exit); /* not posix compliant... */ 60 break; 61 default : printf("use: spin [-option] ... [-option] file\n"); 62 printf("\t-a produce an analyzer\n"); 63 printf("\t-d produce symbol-table information\n"); 64 printf("\t-D write/write dataflow\n"); 65 printf("\t-D -D read/write dataflow\n"); 66 printf("\t-g print all global variables\n"); 67 printf("\t-i interactive (random simulation)\n"); 68 printf("\t-l print all local variables\n"); 69 printf("\t-m lose msgs sent to full queues\n"); 70 printf("\t-nN seed for random nr generator\n"); 71 printf("\t-p print all statements\n"); 72 printf("\t-r print receive events\n"); 73 printf("\t-s print send events\n"); 74 printf("\t-v verbose, more warnings\n"); 75 printf("\t-t follow a simulation trail\n"); 76 printf("\t-V print version number and exit\n"); 77 exit(1); 78 } 79 argc--, argv++; 80 } 81 if (argc > 1) 82 { char outfile[32], cmd[128]; 83 extern char *tmpnam(char *); 84 (void) tmpnam(outfile); 85 86 /* on some systems: "/usr/ccs/lib/cpp" */ 87 sprintf(cmd, "/bin/cpp %s > %s", argv[1], outfile); 88 if (system((const char *)cmd)) 89 { (void) unlink((const char *)outfile); 90 exit(1); 91 } else if (!(yyin = fopen(outfile, "r"))) 92 { printf("cannot open %s\n", outfile); 93 exit(1); 94 } 95 (void) unlink((const char *)outfile); 96 oFname = Fname = lookup(argv[1]); 97 if (oFname->name[0] == '\"') 98 { int i = strlen(oFname->name); 99 oFname->name[i-1] = '\0'; 100 oFname = lookup(&oFname->name[1]); 101 } 102 } else 103 Fname = lookup("<stdin>"); 104 Srand(T); /* defined in run.c */ 105 s = lookup("_p"); s->type = PREDEF; 106 s = lookup("_pid"); s->type = PREDEF; 107 s = lookup("_last"); s->type = PREDEF; 108 yyparse(); 109 exit(nr_errs); 110 } 111 112 int 113 yywrap(void) /* dummy routine */ 114 { 115 return 1; 116 } 117 118 void 119 non_fatal(char *s1, char *s2) 120 { extern int yychar; extern char yytext[]; 121 122 printf("spin: line %3d %s: ", lineno, Fname->name); 123 if (s2) 124 printf(s1, s2); 125 else 126 printf(s1); 127 if (yychar != -1 && yychar != 0) 128 { printf(" saw '"); 129 explain(yychar); 130 printf("'"); 131 } 132 if (yytext && strlen(yytext)>1) 133 printf(" near '%s'", yytext); 134 printf("\n"); fflush(stdout); 135 nr_errs++; 136 } 137 138 void 139 fatal(char *s1, char *s2) 140 { 141 non_fatal(s1, s2); 142 exit(1); 143 } 144 145 char * 146 emalloc(int n) 147 { char *tmp; 148 149 if (!(tmp = (char *) malloc(n))) 150 fatal("not enough memory", (char *)0); 151 memset(tmp, 0, n); 152 return tmp; 153 } 154 155 Lextok * 156 nn(Lextok *s, int t, Lextok *ll, Lextok *rl) 157 { Lextok *n = (Lextok *) emalloc(sizeof(Lextok)); 158 extern char *claimproc; 159 extern Symbol *context; 160 161 n->ntyp = t; 162 if (s && s->fn) 163 { n->ln = s->ln; 164 n->fn = s->fn; 165 } else if (rl && rl->fn) 166 { n->ln = rl->ln; 167 n->fn = rl->fn; 168 } else if (ll && ll->fn) 169 { n->ln = ll->ln; 170 n->fn = ll->fn; 171 } else 172 { n->ln = lineno; 173 n->fn = Fname; 174 } 175 if (s) n->sym = s->sym; 176 n->lft = ll; 177 n->rgt = rl; 178 n->indstep = DstepStart; 179 180 if (t == TIMEOUT) Etimeouts++; 181 182 if (!context) 183 return n; 184 if (context->name == claimproc) 185 { switch (t) { 186 case ASGN: case 'r': case 's': 187 non_fatal("never claim has side-effect",(char *)0); 188 break; 189 case TIMEOUT: 190 /* never claim polls timeout */ 191 Ntimeouts++; Etimeouts--; 192 break; 193 case LEN: case EMPTY: case FULL: 194 case 'R': case NFULL: case NEMPTY: 195 /* status bumped to non-exclusive */ 196 if (n->sym) n->sym->xu |= XX; 197 break; 198 default: 199 break; 200 } 201 } else if (t == ENABLED) 202 fatal("using enabled() outside never-claim",(char *)0); 203 /* this affects how enabled is implemented in run.c */ 204 205 return n; 206 } 207 208 Lextok * 209 rem_lab(Symbol *a, Lextok *b, Symbol *c) 210 { Lextok *tmp1, *tmp2, *tmp3; 211 212 has_remote++; 213 fix_dest(c, a); /* in case target is jump */ 214 tmp1 = nn(ZN, '?', b, ZN); tmp1->sym = a; 215 tmp1 = nn(ZN, 'p', tmp1, ZN); 216 tmp1->sym = lookup("_p"); 217 tmp2 = nn(ZN, NAME, ZN, ZN); tmp2->sym = a; 218 tmp3 = nn(ZN, 'q', tmp2, ZN); tmp3->sym = c; 219 return nn(ZN, EQ, tmp1, tmp3); 220 } 221 222 char Operator[] = "operator: "; 223 char Keyword[] = "keyword: "; 224 char Function[] = "function-name: "; 225 226 void 227 explain(int n) 228 { 229 switch (n) { 230 default: if (n > 0 && n < 256) 231 printf("%c' = '", n); 232 printf("%d", n); 233 break; 234 case '\b': printf("\\b"); break; 235 case '\t': printf("\\t"); break; 236 case '\f': printf("\\f"); break; 237 case '\n': printf("\\n"); break; 238 case '\r': printf("\\r"); break; 239 case 'c': printf("condition"); break; 240 case 's': printf("send"); break; 241 case 'r': printf("recv"); break; 242 case '@': printf("delproc"); break; 243 case '?': printf("(x->y:z)"); break; 244 case ACTIVE: printf("%sactive", Keyword); break; 245 case AND: printf("%s&&", Operator); break; 246 case ASGN: printf("%s=", Operator); break; 247 case ASSERT: printf("%sassert", Function); break; 248 case ATOMIC: printf("%satomic", Keyword); break; 249 case BREAK: printf("%sbreak", Keyword); break; 250 case CLAIM: printf("%snever", Keyword); break; 251 case CONST: printf("a constant"); break; 252 case DECR: printf("%s--", Operator); break; 253 case D_STEP: printf("%sd_step", Keyword); break; 254 case DO: printf("%sdo", Keyword); break; 255 case DOT: printf("."); break; 256 case ELSE: printf("%selse", Keyword); break; 257 case EMPTY: printf("%sempty", Function); break; 258 case ENABLED: printf("%senabled", Function); break; 259 case EQ: printf("%s==", Operator); break; 260 case FI: printf("%sfi", Keyword); break; 261 case FULL: printf("%sfull", Function); break; 262 case GE: printf("%s>=", Operator); break; 263 case GOTO: printf("%sgoto", Keyword); break; 264 case GT: printf("%s>", Operator); break; 265 case IF: printf("%sif", Keyword); break; 266 case INCR: printf("%s++", Operator); break; 267 case INIT: printf("%sinit", Keyword); break; 268 case LABEL: printf("a label-name"); break; 269 case LE: printf("%s<=", Operator); break; 270 case LEN: printf("%slen", Function); break; 271 case LSHIFT: printf("%s<<", Operator); break; 272 case LT: printf("%s<", Operator); break; 273 case MTYPE: printf("%smtype", Keyword); break; 274 case NAME: printf("an identifier"); break; 275 case NE: printf("%s!=", Operator); break; 276 case NEG: printf("%s! (not)", Operator); break; 277 case NEMPTY: printf("%snempty", Function); break; 278 case NFULL: printf("%snfull", Function); break; 279 case NON_ATOMIC: printf("sub-sequence"); break; 280 case OD: printf("%sod", Keyword); break; 281 case OF: printf("%sof", Keyword); break; 282 case OR: printf("%s||", Operator); break; 283 case O_SND: printf("%s!!", Operator); break; 284 case PC_VAL: printf("%spc_value", Function); break; 285 case PNAME: printf("process name"); break; 286 case PRINT: printf("%sprintf", Function); break; 287 case PROCTYPE: printf("%sproctype", Keyword); break; 288 case RCV: printf("%s?", Operator); break; 289 case R_RCV: printf("%s??", Operator); break; 290 case RSHIFT: printf("%s>>", Operator); break; 291 case RUN: printf("%srun", Operator); break; 292 case SEP: printf("token: ::"); break; 293 case SEMI: printf(";"); break; 294 case SND: printf("%s!", Operator); break; 295 case STRING: printf("a string"); break; 296 case TIMEOUT: printf("%stimeout", Keyword); break; 297 case TYPE: printf("data typename"); break; 298 case TYPEDEF: printf("%stypedef", Keyword); break; 299 case XU: printf("%sx[rs]", Keyword); break; 300 case UMIN: printf("%s- (unary minus)", Operator); break; 301 case UNAME: printf("a typename"); break; 302 case UNLESS: printf("%sunless", Keyword); break; 303 } 304 } 305 306 static int IsAsgn = 0, OrIsAsgn = 0; 307 static Element *Same; 308 309 int 310 used_here(Symbol *s, Lextok *n) 311 { extern Symbol *context; 312 int res = 0; 313 314 if (!n) return 0; 315 #ifdef DEBUG 316 { int oln; Symbol *ofn; 317 printf(" used_here %s -- ", context->name); 318 oln = lineno; ofn = Fname; 319 comment(stdout, n, 0); 320 lineno = oln; Fname = ofn; 321 printf(" -- %d:%s\n", n->ln,n->fn->name); 322 } 323 #endif 324 if (n->sym == s) res = (IsAsgn || n->ntyp == ASGN)?2:1; 325 if (n->ntyp == ASGN) 326 res |= used_here(s, n->lft->lft); 327 else 328 res |= used_here(s, n->lft); 329 if (n->ntyp == 'r') 330 IsAsgn = 1; 331 res |= used_here(s, n->rgt); 332 if (n->ntyp == 'r') 333 IsAsgn = 0; 334 return res; 335 } 336 337 int 338 used_later(Symbol *s, Element *t) 339 { extern Symbol *context; 340 int res = 0; 341 342 if (!t || !s) 343 return 0; 344 if (t->status&CHECK2) 345 { 346 #ifdef DEBUG 347 printf("\t%d used_later: done before\n", t->Seqno); 348 #endif 349 return (t->Seqno == Same->Seqno) ? 4 : 0; 350 } 351 352 t->status |= CHECK2; 353 354 #ifdef DEBUG 355 { int oln; Symbol *ofn; 356 printf("\t%d %u ->%d %u used_later %s -- ", 357 t->seqno, 358 t, (t->nxt)?t->nxt->seqno:-1, 359 t->nxt, context->name); 360 oln = lineno; ofn = Fname; 361 comment(stdout, t->n, 0); 362 lineno = oln; Fname = ofn; 363 printf(" -- %d:%s\n", t->n->ln, t->n->fn->name); 364 } 365 #endif 366 if (t->n->ntyp == GOTO) 367 { Element *j = target(t); 368 #ifdef DEBUG 369 printf("\t\tjump to %d\n", j?j->Seqno:-1); 370 #endif 371 res |= used_later(s, j); 372 goto done; 373 } 374 375 if (t->n->sl && ! t->sub) /* d_step or (non-) atomic */ 376 { SeqList *f; 377 for (f = t->n->sl; f; f = f->nxt) 378 { f->this->last->nxt = t->nxt; 379 #ifdef DEBUG 380 printf("\tPatch2 %d->%d (%d)\n", 381 f->this->last->seqno, t->nxt?t->nxt->seqno:-1, t->n->ntyp); 382 #endif 383 res |= used_later(s, f->this->frst); 384 } 385 } else if (t->sub) /* IF or DO */ 386 { SeqList *f; 387 for (f = t->sub; f; f = f->nxt) 388 res |= used_later(s, f->this->frst); 389 } else 390 { res |= used_here(s, t->n); 391 } 392 if (!(res&3)) res |= used_later(s, t->nxt); 393 done: 394 t->status &= ~CHECK2; 395 return res; 396 } 397 398 void 399 varused(Lextok *t, Element *u, int isread) 400 { int res = 0; 401 402 if (!t || !t->sym) return; 403 if (dataflow == 1 && isread) return; 404 405 res = used_later(t->sym, u); 406 407 if ((res&1) 408 || (isread && res&4)) 409 return; /* followed by at least one read */ 410 411 printf("%s:%3d: ", 412 Same->n->fn->name, 413 Same->n->ln); 414 if (t->sym->owner) printf("%s.", t->sym->owner->name); 415 printf("%s -- (%s)", 416 t->sym->name, 417 (isread)?"read":"write"); 418 419 if (!res) { printf(" none"); printf("\n");exit(0); } 420 if (res&2) printf(" write"); 421 if (res&4) printf(" same"); 422 printf("\n"); 423 424 } 425 426 void 427 varprobe(Element *parent, Lextok *n, Element *q) 428 { 429 if (!n) return; 430 431 Same = parent; 432 433 /* can't deal with globals, structs, or arrays */ 434 if (n->sym 435 && n->sym->context 436 && n->sym->nel == 1 437 && n->sym->type != STRUCT 438 && n->ntyp != PRINT) 439 varused(n, q, (!OrIsAsgn && n->ntyp != ASGN)); 440 441 if (n->ntyp == ASGN) 442 varprobe(parent, n->lft->lft, q); 443 else 444 varprobe(parent, n->lft, q); 445 446 if (n->ntyp == 'r') 447 OrIsAsgn = 1; 448 449 varprobe(parent, n->rgt, q); 450 451 if (n->ntyp == 'r') 452 OrIsAsgn = 0; 453 } 454 455 #if 0 456 #define walkprog varcheck 457 #else 458 #define Varcheck varcheck 459 #endif 460 461 void 462 Varcheck(Element *e, Element *nx) 463 { SeqList *f; extern Symbol *context; 464 465 if (!dataflow || !e || e->status&CHECK1) 466 return; 467 #ifdef DEBUG 468 { int oln; Symbol *ofn; 469 printf("%s:%d -- ", context->name, e->Seqno); 470 oln = lineno; ofn = Fname; 471 comment(stdout, e->n, 0); 472 lineno = oln; Fname = ofn; 473 printf(" -- %d:%s\n", e->n->ln, e->n->fn->name); 474 } 475 #endif 476 e->status |= CHECK1; 477 478 if (e->n->ntyp == GOTO) 479 { Element *ef = target(e); 480 if (ef) varcheck(ef, ef->nxt); 481 goto done; 482 } else if (e->n->sl && !e->sub) /* d_step or (non)-atomic */ 483 { for (f = e->n->sl; f; f = f->nxt) 484 { f->this->last->nxt = nx; 485 #ifdef DEBUG 486 printf("\tPatch1 %d->%d\n", 487 f->this->last->seqno, nx?nx->seqno:-1); 488 varcheck(f->this->frst, nx); 489 #endif 490 f->this->last->nxt = 0; 491 } 492 } else if (e->sub && e->n->ntyp == IF) /* if */ 493 { for (f = e->sub; f; f = f->nxt) 494 varcheck(f->this->frst, nx); 495 } else if (e->sub && e->n->ntyp == DO) /* do */ 496 { for (f = e->sub; f; f = f->nxt) 497 varcheck(f->this->frst, e); 498 } else 499 { varprobe(e, e->n, e->nxt); 500 } 501 { Element *ef = huntele(e->nxt, e->status); 502 if (ef) varcheck(ef, ef->nxt); 503 } 504 done: 505 /* e->status &= ~CHECK1 */ ; 506 } 507 508 void 509 nested(int n) 510 { int i; 511 for (i = 0; i < n; i++) 512 printf("\t"); 513 } 514 515 void 516 walkprog(Element *e, Element *nx) 517 { SeqList *f; extern Symbol *context; 518 static int Nest=0; int oln; 519 520 if (!dataflow) return; 521 if (!e) 522 { nested(Nest); 523 printf("nil\n"); 524 return; 525 } 526 527 nested(Nest); 528 printf("%4d,%4d, %s:%d(%u) -- ", 529 e->status, lineno, 530 context->name, e->Seqno, e); 531 oln = lineno; 532 comment(stdout, e->n, 0); 533 lineno = oln; 534 printf(" -- %d:%s\n", e->n->ln, e->n->fn->name); 535 536 if (e->status&CHECK1) 537 { nested(Nest); 538 printf("seenbefore\n"); 539 return; 540 } 541 542 e->status |= CHECK1; 543 544 if (e->n->ntyp == GOTO) 545 { Element *ef = target(e); 546 if (ef) walkprog(ef, ef->nxt); 547 } else if (e->n->sl && !e->sub) /* ATOMIC, NON_ATOMIC, D_STEP */ 548 { int cnt; 549 550 for (f = e->n->sl, cnt=1; f; f = f->nxt, cnt++) 551 { Nest++; 552 nested(Nest); 553 printf("---a>%d:\n", cnt); 554 #ifdef DEBUG 555 printf("\tPatch0 %d->%d\n", 556 f->this->last->seqno, nx?nx->seqno:-1); 557 f->this->last->nxt = nx; 558 walkprog(f->this->frst, nx); 559 #endif 560 /* f->this->last->nxt = 0; */ 561 Nest--; 562 } 563 } else if (e->sub && e->n->ntyp == IF) 564 { int cnt; 565 for (f = e->sub, cnt=1; f; f = f->nxt, cnt++) 566 { Nest++; 567 nested(Nest); 568 printf("---s>%d:\n", cnt); 569 walkprog(f->this->frst, nx); 570 Nest--; 571 } 572 } else if (e->sub && e->n->ntyp == DO) 573 { int cnt; 574 for (f = e->sub, cnt=1; f; f = f->nxt, cnt++) 575 { Nest++; 576 nested(Nest); 577 printf("---s>%d:\n", cnt); 578 walkprog(f->this->frst, e); 579 Nest--; 580 } 581 } 582 { Element *ef = huntele(e->nxt, e->status); 583 if (ef) walkprog(ef, ef->nxt); 584 } 585 e->status &= ~CHECK1; 586 } 587