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