trunk/verif/Spin/Src5.1.6/flow.c

   1 /***** spin: flow.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 "spin.h"
  13 #include "y.tab.h"
  14
  15 extern Symbol   *Fname;
  16 extern int      nr_errs, lineno, verbose;
  17 extern short    has_unless, has_badelse;
  18
  19 Element *Al_El = ZE;
  20 Label   *labtab = (Label *) 0;
  21 int     Unique=0, Elcnt=0, DstepStart = -1;
  22
  23 static Lbreak   *breakstack = (Lbreak *) 0;
  24 static Lextok   *innermost;
  25 static SeqList  *cur_s = (SeqList *) 0;
  26 static int      break_id=0;
  27
  28 static Element  *if_seq(Lextok *);
  29 static Element  *new_el(Lextok *);
  30 static Element  *unless_seq(Lextok *);
  31 static void     add_el(Element *, Sequence *);
  32 static void     attach_escape(Sequence *, Sequence *);
  33 static void     mov_lab(Symbol *, Element *, Element *);
  34 static void     walk_atomic(Element *, Element *, int);
  35
  36 void
  37 open_seq(int top)
  38 {       SeqList *t;
  39         Sequence *s = (Sequence *) emalloc(sizeof(Sequence));
  40
  41         t = seqlist(s, cur_s);
  42         cur_s = t;
  43         if (top) Elcnt = 1;
  44 }
  45
  46 void
  47 rem_Seq(void)
  48 {
  49         DstepStart = Unique;
  50 }
  51
  52 void
  53 unrem_Seq(void)
  54 {
  55         DstepStart = -1;
  56 }
  57
  58 static int
  59 Rjumpslocal(Element *q, Element *stop)
  60 {       Element *lb, *f;
  61         SeqList *h;
  62
  63         /* allow no jumps out of a d_step sequence */
  64         for (f = q; f && f != stop; f = f->nxt)
  65         {       if (f && f->n && f->n->ntyp == GOTO)
  66                 {       lb = get_lab(f->n, 0);
  67                         if (!lb || lb->Seqno < DstepStart)
  68                         {       lineno = f->n->ln;
  69                                 Fname = f->n->fn;
  70                                 return 0;
  71                 }       }
  72                 for (h = f->sub; h; h = h->nxt)
  73                 {       if (!Rjumpslocal(h->this->frst, h->this->last))
  74                                 return 0;
  75
  76         }       }
  77         return 1;
  78 }
  79
  80 void
  81 cross_dsteps(Lextok *a, Lextok *b)
  82 {
  83         if (a && b
  84         &&  a->indstep != b->indstep)
  85         {       lineno = a->ln;
  86                 Fname  = a->fn;
  87                 fatal("jump into d_step sequence", (char *) 0);
  88         }
  89 }
  90
  91 int
  92 is_skip(Lextok *n)
  93 {
  94         return (n->ntyp == PRINT
  95         ||      n->ntyp == PRINTM
  96         ||      (n->ntyp == 'c'
  97                 && n->lft
  98                 && n->lft->ntyp == CONST
  99                 && n->lft->val  == 1));
 100 }
 101
 102 void
 103 check_sequence(Sequence *s)
 104 {       Element *e, *le = ZE;
 105         Lextok *n;
 106         int cnt = 0;
 107
 108         for (e = s->frst; e; le = e, e = e->nxt)
 109         {       n = e->n;
 110                 if (is_skip(n) && !has_lab(e, 0))
 111                 {       cnt++;
 112                         if (cnt > 1
 113                         &&  n->ntyp != PRINT
 114                         &&  n->ntyp != PRINTM)
 115                         {       if (verbose&32)
 116                                         printf("spin: line %d %s, redundant skip\n",
 117                                                 n->ln, n->fn->name);
 118                                 if (e != s->frst
 119                                 &&  e != s->last
 120                                 &&  e != s->extent)
 121                                 {       e->status |= DONE;      /* not unreachable */
 122                                         le->nxt = e->nxt;       /* remove it */
 123                                         e = le;
 124                                 }
 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 void
 313 loose_ends(void)        /* properly tie-up ends of sub-sequences */
 314 {       Element *e, *f;
 315
 316         for (e = Al_El; e; e = e->Nxt)
 317         {       if (!e->n
 318                 ||  !e->nxt)
 319                         continue;
 320                 switch (e->n->ntyp) {
 321                 case ATOMIC:
 322                 case NON_ATOMIC:
 323                 case D_STEP:
 324                         f = e->nxt;
 325                         while (f && f->n->ntyp == '.')
 326                                 f = f->nxt;
 327                         if (0) printf("link %d, {%d .. %d} -> %d (ntyp=%d) was %d\n",
 328                                 e->seqno,
 329                                 e->n->sl->this->frst->seqno,
 330                                 e->n->sl->this->last->seqno,
 331                                 f?f->seqno:-1, f?f->n->ntyp:-1,
 332                                 e->n->sl->this->last->nxt?e->n->sl->this->last->nxt->seqno:-1);
 333                         if (!e->n->sl->this->last->nxt)
 334                                 e->n->sl->this->last->nxt = f;
 335                         else
 336                         {       if (e->n->sl->this->last->nxt->n->ntyp != GOTO)
 337                                 {       if (!f || e->n->sl->this->last->nxt->seqno != f->seqno)
 338                                         non_fatal("unexpected: loose ends", (char *)0);
 339                                 } else
 340                                         e->n->sl->this->last = e->n->sl->this->last->nxt;
 341                                 /*
 342                                  * fix_dest can push a goto into the nxt position
 343                                  * in that case the goto wins and f is not needed
 344                                  * but the last fields needs adjusting
 345                                  */
 346                         }
 347                         break;
 348         }       }
 349 }
 350
 351 static Element *
 352 if_seq(Lextok *n)
 353 {       int     tok = n->ntyp;
 354         SeqList *s  = n->sl;
 355         Element *e  = new_el(ZN);
 356         Element *t  = new_el(nn(ZN,'.',ZN,ZN)); /* target */
 357         SeqList *z, *prev_z = (SeqList *) 0;
 358         SeqList *move_else  = (SeqList *) 0;    /* to end of optionlist */
 359         int     ref_chans = 0;
 360
 361         for (z = s; z; z = z->nxt)
 362         {       if (!z->this->frst)
 363                         continue;
 364                 if (z->this->frst->n->ntyp == ELSE)
 365                 {       if (move_else)
 366                                 fatal("duplicate `else'", (char *) 0);
 367                         if (z->nxt)     /* is not already at the end */
 368                         {       move_else = z;
 369                                 if (prev_z)
 370                                         prev_z->nxt = z->nxt;
 371                                 else
 372                                         s = n->sl = z->nxt;
 373                                 continue;
 374                         }
 375                 } else
 376                         ref_chans |= has_chanref(z->this->frst->n);
 377                 prev_z = z;
 378         }
 379         if (move_else)
 380         {       move_else->nxt = (SeqList *) 0;
 381                 /* if there is no prev, then else was at the end */
 382                 if (!prev_z) fatal("cannot happen - if_seq", (char *) 0);
 383                 prev_z->nxt = move_else;
 384                 prev_z = move_else;
 385         }
 386         if (prev_z
 387         &&  ref_chans
 388         &&  prev_z->this->frst->n->ntyp == ELSE)
 389         {       prev_z->this->frst->n->val = 1;
 390                 has_badelse++;
 391                 non_fatal("dubious use of 'else' combined with i/o,",
 392                         (char *)0);
 393                 nr_errs--;
 394         }
 395
 396         e->n = nn(n, tok, ZN, ZN);
 397         e->n->sl = s;                   /* preserve as info only */
 398         e->sub = s;
 399         for (z = s; z; prev_z = z, z = z->nxt)
 400                 add_el(t, z->this);     /* append target */
 401         if (tok == DO)
 402         {       add_el(t, cur_s->this); /* target upfront */
 403                 t = new_el(nn(n, BREAK, ZN, ZN)); /* break target */
 404                 set_lab(break_dest(), t);       /* new exit  */
 405                 breakstack = breakstack->nxt;   /* pop stack */
 406         }
 407         add_el(e, cur_s->this);
 408         add_el(t, cur_s->this);
 409         return e;                       /* destination node for label */
 410 }
 411
 412 static void
 413 escape_el(Element *f, Sequence *e)
 414 {       SeqList *z;
 415
 416         for (z = f->esc; z; z = z->nxt)
 417                 if (z->this == e)
 418                         return; /* already there */
 419
 420         /* cover the lower-level escapes of this state */
 421         for (z = f->esc; z; z = z->nxt)
 422                 attach_escape(z->this, e);
 423
 424         /* now attach escape to the state itself */
 425
 426         f->esc = seqlist(e, f->esc);    /* in lifo order... */
 427 #ifdef DEBUG
 428         printf("attach %d (", e->frst->Seqno);
 429         comment(stdout, e->frst->n, 0);
 430         printf(")       to %d (", f->Seqno);
 431         comment(stdout, f->n, 0);
 432         printf(")\n");
 433 #endif
 434         switch (f->n->ntyp) {
 435         case UNLESS:
 436                 attach_escape(f->sub->this, e);
 437                 break;
 438         case IF:
 439         case DO:
 440                 for (z = f->sub; z; z = z->nxt)
 441                         attach_escape(z->this, e);
 442                 break;
 443         case D_STEP:
 444                 /* attach only to the guard stmnt */
 445                 escape_el(f->n->sl->this->frst, e);
 446                 break;
 447         case ATOMIC:
 448         case NON_ATOMIC:
 449                 /* attach to all stmnts */
 450                 attach_escape(f->n->sl->this, e);
 451                 break;
 452         }
 453 }
 454
 455 static void
 456 attach_escape(Sequence *n, Sequence *e)
 457 {       Element *f;
 458
 459         for (f = n->frst; f; f = f->nxt)
 460         {       escape_el(f, e);
 461                 if (f == n->extent)
 462                         break;
 463         }
 464 }
 465
 466 static Element *
 467 unless_seq(Lextok *n)
 468 {       SeqList *s  = n->sl;
 469         Element *e  = new_el(ZN);
 470         Element *t  = new_el(nn(ZN,'.',ZN,ZN)); /* target */
 471         SeqList *z;
 472
 473         e->n = nn(n, UNLESS, ZN, ZN);
 474         e->n->sl = s;                   /* info only */
 475         e->sub = s;
 476
 477         /* need 2 sequences: normal execution and escape */
 478         if (!s || !s->nxt || s->nxt->nxt)
 479                 fatal("unexpected unless structure", (char *)0);
 480
 481         /* append the target state to both */
 482         for (z = s; z; z = z->nxt)
 483                 add_el(t, z->this);
 484
 485         /* attach escapes to all states in normal sequence */
 486         attach_escape(s->this, s->nxt->this);
 487
 488         add_el(e, cur_s->this);
 489         add_el(t, cur_s->this);
 490 #ifdef DEBUG
 491         printf("unless element (%d,%d):\n", e->Seqno, t->Seqno);
 492         for (z = s; z; z = z->nxt)
 493         {       Element *x; printf("\t%d,%d,%d :: ",
 494                 z->this->frst->Seqno,
 495                 z->this->extent->Seqno,
 496                 z->this->last->Seqno);
 497                 for (x = z->this->frst; x; x = x->nxt)
 498                         printf("(%d)", x->Seqno);
 499                 printf("\n");
 500         }
 501 #endif
 502         return e;
 503 }
 504
 505 Element *
 506 mk_skip(void)
 507 {       Lextok  *t = nn(ZN, CONST, ZN, ZN);
 508         t->val = 1;
 509         return new_el(nn(ZN, 'c', t, ZN));
 510 }
 511
 512 static void
 513 add_el(Element *e, Sequence *s)
 514 {
 515         if (e->n->ntyp == GOTO)
 516         {       Symbol *z = has_lab(e, (1|2|4));
 517                 if (z)
 518                 {       Element *y; /* insert a skip */
 519                         y = mk_skip();
 520                         mov_lab(z, e, y); /* inherit label */
 521                         add_el(y, s);
 522         }       }
 523 #ifdef DEBUG
 524         printf("add_el %d after %d -- ",
 525         e->Seqno, (s->last)?s->last->Seqno:-1);
 526         comment(stdout, e->n, 0);
 527         printf("\n");
 528 #endif
 529         if (!s->frst)
 530                 s->frst = e;
 531         else
 532                 s->last->nxt = e;
 533         s->last = e;
 534 }
 535
 536 static Element *
 537 colons(Lextok *n)
 538 {
 539         if (!n)
 540                 return ZE;
 541         if (n->ntyp == ':')
 542         {       Element *e = colons(n->lft);
 543                 set_lab(n->sym, e);
 544                 return e;
 545         }
 546         innermost = n;
 547         return new_el(n);
 548 }
 549
 550 void
 551 add_seq(Lextok *n)
 552 {       Element *e;
 553
 554         if (!n) return;
 555         innermost = n;
 556         e = colons(n);
 557         if (innermost->ntyp != IF
 558         &&  innermost->ntyp != DO
 559         &&  innermost->ntyp != UNLESS)
 560                 add_el(e, cur_s->this);
 561 }
 562
 563 void
 564 set_lab(Symbol *s, Element *e)
 565 {       Label *l; extern Symbol *context;
 566
 567         if (!s) return;
 568         for (l = labtab; l; l = l->nxt)
 569                 if (l->s == s && l->c == context)
 570                 {       non_fatal("label %s redeclared", s->name);
 571                         break;
 572                 }
 573         l = (Label *) emalloc(sizeof(Label));
 574         l->s = s;
 575         l->c = context;
 576         l->e = e;
 577         l->nxt = labtab;
 578         labtab = l;
 579 }
 580
 581 Element *
 582 get_lab(Lextok *n, int md)
 583 {       Label *l;
 584         Symbol *s = n->sym;
 585
 586         for (l = labtab; l; l = l->nxt)
 587                 if (s == l->s)
 588                         return (l->e);
 589
 590         lineno = n->ln;
 591         Fname = n->fn;
 592         if (md) fatal("undefined label %s", s->name);
 593         return ZE;
 594 }
 595
 596 Symbol *
 597 has_lab(Element *e, int special)
 598 {       Label *l;
 599
 600         for (l = labtab; l; l = l->nxt)
 601         {       if (e != l->e)
 602                         continue;
 603                 if (special == 0
 604                 ||  ((special&1) && !strncmp(l->s->name, "accept", 6))
 605                 ||  ((special&2) && !strncmp(l->s->name, "end", 3))
 606                 ||  ((special&4) && !strncmp(l->s->name, "progress", 8)))
 607                         return (l->s);
 608         }
 609         return ZS;
 610 }
 611
 612 static void
 613 mov_lab(Symbol *z, Element *e, Element *y)
 614 {       Label *l;
 615
 616         for (l = labtab; l; l = l->nxt)
 617                 if (e == l->e)
 618                 {       l->e = y;
 619                         return;
 620                 }
 621         if (e->n)
 622         {       lineno = e->n->ln;
 623                 Fname  = e->n->fn;
 624         }
 625         fatal("cannot happen - mov_lab %s", z->name);
 626 }
 627
 628 void
 629 fix_dest(Symbol *c, Symbol *a)          /* c:label name, a:proctype name */
 630 {       Label *l; extern Symbol *context;
 631
 632 #if 0
 633         printf("ref to label '%s' in proctype '%s', search:\n",
 634                 c->name, a->name);
 635         for (l = labtab; l; l = l->nxt)
 636                 printf("        %s in   %s\n", l->s->name, l->c->name);
 637 #endif
 638
 639         for (l = labtab; l; l = l->nxt)
 640         {       if (strcmp(c->name, l->s->name) == 0
 641                 &&  strcmp(a->name, l->c->name) == 0)   /* ? */
 642                         break;
 643         }
 644         if (!l)
 645         {       printf("spin: label '%s' (proctype %s)\n", c->name, a->name);
 646                 non_fatal("unknown label '%s'", c->name);
 647                 if (context == a)
 648                 printf("spin: cannot remote ref a label inside the same proctype\n");
 649                 return;
 650         }
 651         if (!l->e || !l->e->n)
 652                 fatal("fix_dest error (%s)", c->name);
 653         if (l->e->n->ntyp == GOTO)
 654         {       Element *y = (Element *) emalloc(sizeof(Element));
 655                 int     keep_ln = l->e->n->ln;
 656                 Symbol  *keep_fn = l->e->n->fn;
 657
 658                 /* insert skip - or target is optimized away */
 659                 y->n = l->e->n;           /* copy of the goto   */
 660                 y->seqno = find_maxel(a); /* unique seqno within proc */
 661                 y->nxt = l->e->nxt;
 662                 y->Seqno = Unique++; y->Nxt = Al_El; Al_El = y;
 663
 664                 /* turn the original element+seqno into a skip */
 665                 l->e->n = nn(ZN, 'c', nn(ZN, CONST, ZN, ZN), ZN);
 666                 l->e->n->ln = l->e->n->lft->ln = keep_ln;
 667                 l->e->n->fn = l->e->n->lft->fn = keep_fn;
 668                 l->e->n->lft->val = 1;
 669                 l->e->nxt = y;          /* append the goto  */
 670         }
 671         l->e->status |= CHECK2; /* treat as if global */
 672         if (l->e->status & (ATOM | L_ATOM | D_ATOM))
 673         {       non_fatal("cannot reference label inside atomic or d_step (%s)",
 674                         c->name);
 675         }
 676 }
 677
 678 int
 679 find_lab(Symbol *s, Symbol *c, int markit)
 680 {       Label *l;
 681
 682         for (l = labtab; l; l = l->nxt)
 683         {       if (strcmp(s->name, l->s->name) == 0
 684                 &&  strcmp(c->name, l->c->name) == 0)
 685                 {       l->visible |= markit;
 686                         return (l->e->seqno);
 687         }       }
 688         return 0;
 689 }
 690
 691 void
 692 pushbreak(void)
 693 {       Lbreak *r = (Lbreak *) emalloc(sizeof(Lbreak));
 694         Symbol *l;
 695         char buf[64];
 696
 697         sprintf(buf, ":b%d", break_id++);
 698         l = lookup(buf);
 699         r->l = l;
 700         r->nxt = breakstack;
 701         breakstack = r;
 702 }
 703
 704 Symbol *
 705 break_dest(void)
 706 {
 707         if (!breakstack)
 708                 fatal("misplaced break statement", (char *)0);
 709         return breakstack->l;
 710 }
 711
 712 void
 713 make_atomic(Sequence *s, int added)
 714 {       Element *f;
 715
 716         walk_atomic(s->frst, s->last, added);
 717
 718         f = s->last;
 719         switch (f->n->ntyp) {   /* is last step basic stmnt or sequence ? */
 720         case NON_ATOMIC:
 721         case ATOMIC:
 722                 /* redo and search for the last step of that sequence */
 723                 make_atomic(f->n->sl->this, added);
 724                 break;
 725
 726         case UNLESS:
 727                 /* escapes are folded into main sequence */
 728                 make_atomic(f->sub->this, added);
 729                 break;
 730
 731         default:
 732                 f->status &= ~ATOM;
 733                 f->status |= L_ATOM;
 734                 break;
 735         }
 736 }
 737
 738 static void
 739 walk_atomic(Element *a, Element *b, int added)
 740 {       Element *f; Symbol *ofn; int oln;
 741         SeqList *h;
 742
 743         ofn = Fname;
 744         oln = lineno;
 745         for (f = a; ; f = f->nxt)
 746         {       f->status |= (ATOM|added);
 747                 switch (f->n->ntyp) {
 748                 case ATOMIC:
 749                         if (verbose&32)
 750                           printf("spin: warning, line %3d %s, atomic inside %s (ignored)\n",
 751                           f->n->ln, f->n->fn->name, (added)?"d_step":"atomic");
 752                         goto mknonat;
 753                 case D_STEP:
 754                         if (!(verbose&32))
 755                         {       if (added) goto mknonat;
 756                                 break;
 757                         }
 758                         printf("spin: warning, line %3d %s, d_step inside ",
 759                          f->n->ln, f->n->fn->name);
 760                         if (added)
 761                         {       printf("d_step (ignored)\n");
 762                                 goto mknonat;
 763                         }
 764                         printf("atomic\n");
 765                         break;
 766                 case NON_ATOMIC:
 767 mknonat:                f->n->ntyp = NON_ATOMIC; /* can jump here */
 768                         h = f->n->sl;
 769                         walk_atomic(h->this->frst, h->this->last, added);
 770                         break;
 771                 case UNLESS:
 772                         if (added)
 773                         { printf("spin: error, line %3d %s, unless in d_step (ignored)\n",
 774                                  f->n->ln, f->n->fn->name);
 775                         }
 776                 }
 777                 for (h = f->sub; h; h = h->nxt)
 778                         walk_atomic(h->this->frst, h->this->last, added);
 779                 if (f == b)
 780                         break;
 781         }
 782         Fname = ofn;
 783         lineno = oln;
 784 }
 785
 786 void
 787 dumplabels(void)
 788 {       Label *l;
 789
 790         for (l = labtab; l; l = l->nxt)
 791                 if (l->c != 0 && l->s->name[0] != ':')
 792                 printf("label   %s      %d      <%s>\n",
 793                 l->s->name, l->e->seqno, l->c->name);
 794 }