1 /***** spin: flow.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 "spin.h" 14 #ifdef PC 15 #include "y_tab.h" 16 #else 17 #include "y.tab.h" 18 #endif 19 20 extern Symbol *Fname; 21 extern int nr_errs, lineno, verbose; 22 extern short has_unless, has_badelse; 23 24 Element *Al_El = ZE; 25 Label *labtab = (Label *) 0; 26 int Unique=0, Elcnt=0, DstepStart = -1; 27 28 static Lbreak *breakstack = (Lbreak *) 0; 29 static Lextok *innermost; 30 static SeqList *cur_s = (SeqList *) 0; 31 static int break_id=0; 32 33 static Element *if_seq(Lextok *); 34 static Element *new_el(Lextok *); 35 static Element *unless_seq(Lextok *); 36 static void add_el(Element *, Sequence *); 37 static void attach_escape(Sequence *, Sequence *); 38 static void mov_lab(Symbol *, Element *, Element *); 39 static void walk_atomic(Element *, Element *, int); 40 41 void 42 open_seq(int top) 43 { SeqList *t; 44 Sequence *s = (Sequence *) emalloc(sizeof(Sequence)); 45 46 t = seqlist(s, cur_s); 47 cur_s = t; 48 if (top) Elcnt = 1; 49 } 50 51 void 52 rem_Seq(void) 53 { 54 DstepStart = Unique; 55 } 56 57 void 58 unrem_Seq(void) 59 { 60 DstepStart = -1; 61 } 62 63 static int 64 Rjumpslocal(Element *q, Element *stop) 65 { Element *lb, *f; 66 SeqList *h; 67 68 /* allow no jumps out of a d_step sequence */ 69 for (f = q; f && f != stop; f = f->nxt) 70 { if (f && f->n && f->n->ntyp == GOTO) 71 { lb = get_lab(f->n, 0); 72 if (!lb || lb->Seqno < DstepStart) 73 { lineno = f->n->ln; 74 Fname = f->n->fn; 75 return 0; 76 } } 77 for (h = f->sub; h; h = h->nxt) 78 { if (!Rjumpslocal(h->this->frst, h->this->last)) 79 return 0; 80 81 } } 82 return 1; 83 } 84 85 void 86 cross_dsteps(Lextok *a, Lextok *b) 87 { 88 if (a && b 89 && a->indstep != b->indstep) 90 { lineno = a->ln; 91 Fname = a->fn; 92 fatal("jump into d_step sequence", (char *) 0); 93 } 94 } 95 96 int 97 is_skip(Lextok *n) 98 { 99 return (n->ntyp == PRINT 100 || (n->ntyp == 'c' 101 && n->lft 102 && n->lft->ntyp == CONST 103 && n->lft->val == 1)); 104 } 105 106 void 107 check_sequence(Sequence *s) 108 { Element *e, *le = ZE; 109 Lextok *n; 110 int cnt = 0; 111 112 for (e = s->frst; e; le = e, e = e->nxt) 113 { n = e->n; 114 if (is_skip(n) && !has_lab(e, 0)) 115 { cnt++; 116 if (cnt > 1 && n->ntyp != PRINT) 117 { if (verbose&32) 118 printf("spin: line %d %s, redundant skip\n", 119 n->ln, n->fn->name); 120 if (le) 121 { e->status |= DONE; /* not unreachable */ 122 le->nxt = e->nxt; /* remove it */ 123 e = le; 124 } /* else, can't happen */ 125 } 126 } else 127 cnt = 0; 128 } 129 } 130 131 void 132 prune_opts(Lextok *n) 133 { SeqList *l; 134 extern Symbol *context; 135 extern char *claimproc; 136 137 if (!n 138 || (context && claimproc && strcmp(context->name, claimproc) == 0)) 139 return; 140 141 for (l = n->sl; l; l = l->nxt) /* find sequences of unlabeled skips */ 142 check_sequence(l->this); 143 } 144 145 Sequence * 146 close_seq(int nottop) 147 { Sequence *s = cur_s->this; 148 Symbol *z; 149 150 if (nottop > 0 && (z = has_lab(s->frst, 0))) 151 { printf("error: (%s:%d) label %s placed incorrectly\n", 152 (s->frst->n)?s->frst->n->fn->name:"-", 153 (s->frst->n)?s->frst->n->ln:0, 154 z->name); 155 switch (nottop) { 156 case 1: 157 printf("=====> stmnt unless Label: stmnt\n"); 158 printf("sorry, cannot jump to the guard of an\n"); 159 printf("escape (it is not a unique state)\n"); 160 break; 161 case 2: 162 printf("=====> instead of "); 163 printf("\"Label: stmnt unless stmnt\"\n"); 164 printf("=====> always use "); 165 printf("\"Label: { stmnt unless stmnt }\"\n"); 166 break; 167 case 3: 168 printf("=====> instead of "); 169 printf("\"atomic { Label: statement ... }\"\n"); 170 printf("=====> always use "); 171 printf("\"Label: atomic { statement ... }\"\n"); 172 break; 173 case 4: 174 printf("=====> instead of "); 175 printf("\"d_step { Label: statement ... }\"\n"); 176 printf("=====> always use "); 177 printf("\"Label: d_step { statement ... }\"\n"); 178 break; 179 case 5: 180 printf("=====> instead of "); 181 printf("\"{ Label: statement ... }\"\n"); 182 printf("=====> always use "); 183 printf("\"Label: { statement ... }\"\n"); 184 break; 185 case 6: 186 printf("=====>instead of\n"); 187 printf(" do (or if)\n"); 188 printf(" :: ...\n"); 189 printf(" :: Label: statement\n"); 190 printf(" od (of fi)\n"); 191 printf("=====>always use\n"); 192 printf("Label: do (or if)\n"); 193 printf(" :: ...\n"); 194 printf(" :: statement\n"); 195 printf(" od (or fi)\n"); 196 break; 197 case 7: 198 printf("cannot happen - labels\n"); 199 break; 200 } 201 alldone(1); 202 } 203 204 if (nottop == 4 205 && !Rjumpslocal(s->frst, s->last)) 206 fatal("non_local jump in d_step sequence", (char *) 0); 207 208 cur_s = cur_s->nxt; 209 s->maxel = Elcnt; 210 s->extent = s->last; 211 if (!s->last) 212 fatal("sequence must have at least one statement", (char *) 0); 213 return s; 214 } 215 216 Lextok * 217 do_unless(Lextok *No, Lextok *Es) 218 { SeqList *Sl; 219 Lextok *Re = nn(ZN, UNLESS, ZN, ZN); 220 Re->ln = No->ln; 221 Re->fn = No->fn; 222 223 has_unless++; 224 if (Es->ntyp == NON_ATOMIC) 225 Sl = Es->sl; 226 else 227 { open_seq(0); add_seq(Es); 228 Sl = seqlist(close_seq(1), 0); 229 } 230 231 if (No->ntyp == NON_ATOMIC) 232 { No->sl->nxt = Sl; 233 Sl = No->sl; 234 } else if (No->ntyp == ':' 235 && (No->lft->ntyp == NON_ATOMIC 236 || No->lft->ntyp == ATOMIC 237 || No->lft->ntyp == D_STEP)) 238 { 239 int tok = No->lft->ntyp; 240 241 No->lft->sl->nxt = Sl; 242 Re->sl = No->lft->sl; 243 244 open_seq(0); add_seq(Re); 245 Re = nn(ZN, tok, ZN, ZN); 246 Re->sl = seqlist(close_seq(7), 0); 247 Re->ln = No->ln; 248 Re->fn = No->fn; 249 250 Re = nn(No, ':', Re, ZN); /* lift label */ 251 Re->ln = No->ln; 252 Re->fn = No->fn; 253 return Re; 254 } else 255 { open_seq(0); add_seq(No); 256 Sl = seqlist(close_seq(2), Sl); 257 } 258 259 Re->sl = Sl; 260 return Re; 261 } 262 263 SeqList * 264 seqlist(Sequence *s, SeqList *r) 265 { SeqList *t = (SeqList *) emalloc(sizeof(SeqList)); 266 267 t->this = s; 268 t->nxt = r; 269 return t; 270 } 271 272 static Element * 273 new_el(Lextok *n) 274 { Element *m; 275 276 if (n) 277 { if (n->ntyp == IF || n->ntyp == DO) 278 return if_seq(n); 279 if (n->ntyp == UNLESS) 280 return unless_seq(n); 281 } 282 m = (Element *) emalloc(sizeof(Element)); 283 m->n = n; 284 m->seqno = Elcnt++; 285 m->Seqno = Unique++; 286 m->Nxt = Al_El; Al_El = m; 287 return m; 288 } 289 290 static int 291 has_chanref(Lextok *n) 292 { 293 if (!n) return 0; 294 295 switch (n->ntyp) { 296 case 's': case 'r': 297 #if 0 298 case 'R': case LEN: 299 #endif 300 case FULL: case NFULL: 301 case EMPTY: case NEMPTY: 302 return 1; 303 default: 304 break; 305 } 306 if (has_chanref(n->lft)) 307 return 1; 308 309 return has_chanref(n->rgt); 310 } 311 312 static Element * 313 if_seq(Lextok *n) 314 { int tok = n->ntyp; 315 SeqList *s = n->sl; 316 Element *e = new_el(ZN); 317 Element *t = new_el(nn(ZN,'.',ZN,ZN)); /* target */ 318 SeqList *z, *prev_z = (SeqList *) 0; 319 SeqList *move_else = (SeqList *) 0; /* to end of optionlist */ 320 int ref_chans = 0; 321 322 for (z = s; z; z = z->nxt) 323 { if (!z->this->frst) 324 continue; 325 if (z->this->frst->n->ntyp == ELSE) 326 { if (move_else) 327 fatal("duplicate `else'", (char *) 0); 328 if (z->nxt) /* is not already at the end */ 329 { move_else = z; 330 if (prev_z) 331 prev_z->nxt = z->nxt; 332 else 333 s = n->sl = z->nxt; 334 continue; 335 } 336 } else 337 ref_chans |= has_chanref(z->this->frst->n); 338 prev_z = z; 339 } 340 if (move_else) 341 { move_else->nxt = (SeqList *) 0; 342 /* if there is no prev, then else was at the end */ 343 if (!prev_z) fatal("cannot happen - if_seq", (char *) 0); 344 prev_z->nxt = move_else; 345 prev_z = move_else; 346 } 347 if (prev_z 348 && ref_chans 349 && prev_z->this->frst->n->ntyp == ELSE) 350 { prev_z->this->frst->n->val = 1; 351 has_badelse++; 352 non_fatal("dubious use of 'else' combined with i/o,", 353 (char *)0); 354 nr_errs--; 355 } 356 357 e->n = nn(n, tok, ZN, ZN); 358 e->n->sl = s; /* preserve as info only */ 359 e->sub = s; 360 for (z = s; z; prev_z = z, z = z->nxt) 361 add_el(t, z->this); /* append target */ 362 if (tok == DO) 363 { add_el(t, cur_s->this); /* target upfront */ 364 t = new_el(nn(n, BREAK, ZN, ZN)); /* break target */ 365 set_lab(break_dest(), t); /* new exit */ 366 breakstack = breakstack->nxt; /* pop stack */ 367 } 368 add_el(e, cur_s->this); 369 add_el(t, cur_s->this); 370 return e; /* destination node for label */ 371 } 372 373 static void 374 escape_el(Element *f, Sequence *e) 375 { SeqList *z; 376 377 for (z = f->esc; z; z = z->nxt) 378 if (z->this == e) 379 return; /* already there */ 380 381 /* cover the lower-level escapes of this state */ 382 for (z = f->esc; z; z = z->nxt) 383 attach_escape(z->this, e); 384 385 /* now attach escape to the state itself */ 386 387 f->esc = seqlist(e, f->esc); /* in lifo order... */ 388 #ifdef DEBUG 389 printf("attach %d (", e->frst->Seqno); 390 comment(stdout, e->frst->n, 0); 391 printf(") to %d (", f->Seqno); 392 comment(stdout, f->n, 0); 393 printf(")\n"); 394 #endif 395 switch (f->n->ntyp) { 396 case UNLESS: 397 attach_escape(f->sub->this, e); 398 break; 399 case IF: 400 case DO: 401 for (z = f->sub; z; z = z->nxt) 402 attach_escape(z->this, e); 403 break; 404 case D_STEP: 405 /* attach only to the guard stmnt */ 406 escape_el(f->n->sl->this->frst, e); 407 break; 408 case ATOMIC: 409 case NON_ATOMIC: 410 /* attach to all stmnts */ 411 attach_escape(f->n->sl->this, e); 412 break; 413 } 414 } 415 416 static void 417 attach_escape(Sequence *n, Sequence *e) 418 { Element *f; 419 420 for (f = n->frst; f; f = f->nxt) 421 { escape_el(f, e); 422 if (f == n->extent) 423 break; 424 } 425 } 426 427 static Element * 428 unless_seq(Lextok *n) 429 { SeqList *s = n->sl; 430 Element *e = new_el(ZN); 431 Element *t = new_el(nn(ZN,'.',ZN,ZN)); /* target */ 432 SeqList *z; 433 434 e->n = nn(n, UNLESS, ZN, ZN); 435 e->n->sl = s; /* info only */ 436 e->sub = s; 437 438 /* need 2 sequences: normal execution and escape */ 439 if (!s || !s->nxt || s->nxt->nxt) 440 fatal("unexpected unless structure", (char *)0); 441 442 /* append the target state to both */ 443 for (z = s; z; z = z->nxt) 444 add_el(t, z->this); 445 446 /* attach escapes to all states in normal sequence */ 447 attach_escape(s->this, s->nxt->this); 448 449 add_el(e, cur_s->this); 450 add_el(t, cur_s->this); 451 #ifdef DEBUG 452 printf("unless element (%d,%d):\n", e->Seqno, t->Seqno); 453 for (z = s; z; z = z->nxt) 454 { Element *x; printf("\t%d,%d,%d :: ", 455 z->this->frst->Seqno, 456 z->this->extent->Seqno, 457 z->this->last->Seqno); 458 for (x = z->this->frst; x; x = x->nxt) 459 printf("(%d)", x->Seqno); 460 printf("\n"); 461 } 462 #endif 463 return e; 464 } 465 466 Element * 467 mk_skip(void) 468 { Lextok *t = nn(ZN, CONST, ZN, ZN); 469 t->val = 1; 470 return new_el(nn(ZN, 'c', t, ZN)); 471 } 472 473 static void 474 add_el(Element *e, Sequence *s) 475 { 476 if (e->n->ntyp == GOTO) 477 { Symbol *z = has_lab(e, (1|2|4)); 478 if (z) 479 { Element *y; /* insert a skip */ 480 y = mk_skip(); 481 mov_lab(z, e, y); /* inherit label */ 482 add_el(y, s); 483 } } 484 #ifdef DEBUG 485 printf("add_el %d after %d -- ", 486 e->Seqno, (s->last)?s->last->Seqno:-1); 487 comment(stdout, e->n, 0); 488 printf("\n"); 489 #endif 490 if (!s->frst) 491 s->frst = e; 492 else 493 s->last->nxt = e; 494 s->last = e; 495 } 496 497 static Element * 498 colons(Lextok *n) 499 { 500 if (!n) 501 return ZE; 502 if (n->ntyp == ':') 503 { Element *e = colons(n->lft); 504 set_lab(n->sym, e); 505 return e; 506 } 507 innermost = n; 508 return new_el(n); 509 } 510 511 void 512 add_seq(Lextok *n) 513 { Element *e; 514 515 if (!n) return; 516 innermost = n; 517 e = colons(n); 518 if (innermost->ntyp != IF 519 && innermost->ntyp != DO 520 && innermost->ntyp != UNLESS) 521 add_el(e, cur_s->this); 522 } 523 524 void 525 set_lab(Symbol *s, Element *e) 526 { Label *l; extern Symbol *context; 527 528 if (!s) return; 529 for (l = labtab; l; l = l->nxt) 530 if (l->s == s && l->c == context) 531 { non_fatal("label %s redeclared", s->name); 532 break; 533 } 534 l = (Label *) emalloc(sizeof(Label)); 535 l->s = s; 536 l->c = context; 537 l->e = e; 538 l->nxt = labtab; 539 labtab = l; 540 } 541 542 Element * 543 get_lab(Lextok *n, int md) 544 { Label *l; 545 Symbol *s = n->sym; 546 547 for (l = labtab; l; l = l->nxt) 548 if (s == l->s) 549 return (l->e); 550 lineno = n->ln; 551 Fname = n->fn; 552 if (md) fatal("undefined label %s", s->name); 553 return ZE; 554 } 555 556 Symbol * 557 has_lab(Element *e, int special) 558 { Label *l; 559 560 for (l = labtab; l; l = l->nxt) 561 { if (e != l->e) 562 continue; 563 if (special == 0 564 || ((special&1) && !strncmp(l->s->name, "accept", 6)) 565 || ((special&2) && !strncmp(l->s->name, "end", 3)) 566 || ((special&4) && !strncmp(l->s->name, "progress", 8))) 567 return (l->s); 568 } 569 return ZS; 570 } 571 572 static void 573 mov_lab(Symbol *z, Element *e, Element *y) 574 { Label *l; 575 576 for (l = labtab; l; l = l->nxt) 577 if (e == l->e) 578 { l->e = y; 579 return; 580 } 581 if (e->n) 582 { lineno = e->n->ln; 583 Fname = e->n->fn; 584 } 585 fatal("cannot happen - mov_lab %s", z->name); 586 } 587 588 void 589 fix_dest(Symbol *c, Symbol *a) /* label, proctype */ 590 { Label *l; extern Symbol *context; 591 592 for (l = labtab; l; l = l->nxt) 593 { if (strcmp(c->name, l->s->name) == 0 594 && strcmp(a->name, l->c->name) == 0) 595 break; 596 } 597 if (!l) 598 { printf("spin: label '%s' (proctype %s)\n", c->name, a->name); 599 non_fatal("unknown label '%s'", c->name); 600 if (context == a) 601 printf("spin: cannot remote ref a label inside the same proctype\n"); 602 return; 603 } 604 if (!l->e || !l->e->n) 605 fatal("fix_dest error (%s)", c->name); 606 if (l->e->n->ntyp == GOTO) 607 { Element *y = (Element *) emalloc(sizeof(Element)); 608 int keep_ln = l->e->n->ln; 609 Symbol *keep_fn = l->e->n->fn; 610 611 /* insert skip - or target is optimized away */ 612 y->n = l->e->n; /* copy of the goto */ 613 y->seqno = find_maxel(a); /* unique seqno within proc */ 614 y->nxt = l->e->nxt; 615 y->Seqno = Unique++; y->Nxt = Al_El; Al_El = y; 616 617 /* turn the original element+seqno into a skip */ 618 l->e->n = nn(ZN, 'c', nn(ZN, CONST, ZN, ZN), ZN); 619 l->e->n->ln = l->e->n->lft->ln = keep_ln; 620 l->e->n->fn = l->e->n->lft->fn = keep_fn; 621 l->e->n->lft->val = 1; 622 l->e->nxt = y; /* append the goto */ 623 } 624 l->e->status |= CHECK2; /* treat as if global */ 625 } 626 627 int 628 find_lab(Symbol *s, Symbol *c, int markit) 629 { Label *l; 630 631 for (l = labtab; l; l = l->nxt) 632 { if (strcmp(s->name, l->s->name) == 0 633 && strcmp(c->name, l->c->name) == 0) 634 { l->visible |= markit; 635 return (l->e->seqno); 636 } } 637 return 0; 638 } 639 640 void 641 pushbreak(void) 642 { Lbreak *r = (Lbreak *) emalloc(sizeof(Lbreak)); 643 Symbol *l; 644 char buf[64]; 645 646 sprintf(buf, ":b%d", break_id++); 647 l = lookup(buf); 648 r->l = l; 649 r->nxt = breakstack; 650 breakstack = r; 651 } 652 653 Symbol * 654 break_dest(void) 655 { 656 if (!breakstack) 657 fatal("misplaced break statement", (char *)0); 658 return breakstack->l; 659 } 660 661 void 662 make_atomic(Sequence *s, int added) 663 { 664 walk_atomic(s->frst, s->last, added); 665 s->last->status &= ~ATOM; 666 s->last->status |= L_ATOM; 667 } 668 669 static void 670 walk_atomic(Element *a, Element *b, int added) 671 { Element *f; Symbol *ofn; int oln; 672 SeqList *h; 673 674 ofn = Fname; 675 oln = lineno; 676 for (f = a; ; f = f->nxt) 677 { f->status |= (ATOM|added); 678 switch (f->n->ntyp) { 679 case ATOMIC: 680 if (verbose&32) 681 printf("spin: warning, line %3d %s, atomic inside %s (ignored)\n", 682 f->n->ln, f->n->fn->name, (added)?"d_step":"atomic"); 683 goto mknonat; 684 case D_STEP: 685 if (!(verbose&32)) 686 { if (added) goto mknonat; 687 break; 688 } 689 printf("spin: warning, line %3d %s, d_step inside ", 690 f->n->ln, f->n->fn->name); 691 if (added) 692 { printf("d_step (ignored)\n"); 693 goto mknonat; 694 } 695 printf("atomic\n"); 696 break; 697 case NON_ATOMIC: 698 mknonat: f->n->ntyp = NON_ATOMIC; /* can jump here */ 699 h = f->n->sl; 700 walk_atomic(h->this->frst, h->this->last, added); 701 break; 702 } 703 for (h = f->sub; h; h = h->nxt) 704 walk_atomic(h->this->frst, h->this->last, added); 705 if (f == b) 706 break; 707 } 708 Fname = ofn; 709 lineno = oln; 710 } 711 712 void 713 dumplabels(void) 714 { Label *l; 715 716 for (l = labtab; l; l = l->nxt) 717 if (l->c != 0 && l->s->name[0] != ':') 718 printf("label %s %d <%s>\n", 719 l->s->name, l->e->seqno, l->c->name); 720 } 721