1 /***** spin: flow.c *****/
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 */
16 extern int nr_errs, lineno, verbose;
17 extern short has_unless, has_badelse;
20 Label *labtab = (Label *) 0;
21 int Unique=0, Elcnt=0, DstepStart = -1;
23 static Lbreak *breakstack = (Lbreak *) 0;
24 static Lextok *innermost;
25 static SeqList *cur_s = (SeqList *) 0;
26 static int break_id=0;
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);
39 Sequence *s = (Sequence *) emalloc(sizeof(Sequence));
41 t = seqlist(s, cur_s);
59 Rjumpslocal(Element *q, Element *stop)
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)
72 for (h = f->sub; h; h = h->nxt)
73 { if (!Rjumpslocal(h->this->frst, h->this->last))
81 cross_dsteps(Lextok *a, Lextok *b)
84 && a->indstep != b->indstep)
87 fatal("jump into d_step sequence", (char *) 0);
94 return (n->ntyp == PRINT
98 && n->lft->ntyp == CONST
99 && n->lft->val == 1));
103 check_sequence(Sequence *s)
104 { Element *e, *le = ZE;
108 for (e = s->frst; e; le = e, e = e->nxt)
110 if (is_skip(n) && !has_lab(e, 0))
114 && n->ntyp != PRINTM)
116 printf("spin: line %d %s, redundant skip\n",
121 { e->status |= DONE; /* not unreachable */
122 le->nxt = e->nxt; /* remove it */
132 prune_opts(Lextok *n)
134 extern Symbol *context;
135 extern char *claimproc;
138 || (context && claimproc && strcmp(context->name, claimproc) == 0))
141 for (l = n->sl; l; l = l->nxt) /* find sequences of unlabeled skips */
142 check_sequence(l->this);
146 close_seq(int nottop)
147 { Sequence *s = cur_s->this;
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,
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");
162 printf("=====> instead of ");
163 printf("\"Label: stmnt unless stmnt\"\n");
164 printf("=====> always use ");
165 printf("\"Label: { stmnt unless stmnt }\"\n");
168 printf("=====> instead of ");
169 printf("\"atomic { Label: statement ... }\"\n");
170 printf("=====> always use ");
171 printf("\"Label: atomic { statement ... }\"\n");
174 printf("=====> instead of ");
175 printf("\"d_step { Label: statement ... }\"\n");
176 printf("=====> always use ");
177 printf("\"Label: d_step { statement ... }\"\n");
180 printf("=====> instead of ");
181 printf("\"{ Label: statement ... }\"\n");
182 printf("=====> always use ");
183 printf("\"Label: { statement ... }\"\n");
186 printf("=====>instead of\n");
187 printf(" do (or if)\n");
189 printf(" :: Label: statement\n");
190 printf(" od (of fi)\n");
191 printf("=====>always use\n");
192 printf("Label: do (or if)\n");
194 printf(" :: statement\n");
195 printf(" od (or fi)\n");
198 printf("cannot happen - labels\n");
205 && !Rjumpslocal(s->frst, s->last))
206 fatal("non_local jump in d_step sequence", (char *) 0);
212 fatal("sequence must have at least one statement", (char *) 0);
217 do_unless(Lextok *No, Lextok *Es)
219 Lextok *Re = nn(ZN, UNLESS, ZN, ZN);
224 if (Es->ntyp == NON_ATOMIC)
227 { open_seq(0); add_seq(Es);
228 Sl = seqlist(close_seq(1), 0);
231 if (No->ntyp == NON_ATOMIC)
234 } else if (No->ntyp == ':'
235 && (No->lft->ntyp == NON_ATOMIC
236 || No->lft->ntyp == ATOMIC
237 || No->lft->ntyp == D_STEP))
239 int tok = No->lft->ntyp;
241 No->lft->sl->nxt = Sl;
242 Re->sl = No->lft->sl;
244 open_seq(0); add_seq(Re);
245 Re = nn(ZN, tok, ZN, ZN);
246 Re->sl = seqlist(close_seq(7), 0);
250 Re = nn(No, ':', Re, ZN); /* lift label */
255 { open_seq(0); add_seq(No);
256 Sl = seqlist(close_seq(2), Sl);
264 seqlist(Sequence *s, SeqList *r)
265 { SeqList *t = (SeqList *) emalloc(sizeof(SeqList));
277 { if (n->ntyp == IF || n->ntyp == DO)
279 if (n->ntyp == UNLESS)
280 return unless_seq(n);
282 m = (Element *) emalloc(sizeof(Element));
286 m->Nxt = Al_El; Al_El = m;
291 has_chanref(Lextok *n)
300 case FULL: case NFULL:
301 case EMPTY: case NEMPTY:
306 if (has_chanref(n->lft))
309 return has_chanref(n->rgt);
313 loose_ends(void) /* properly tie-up ends of sub-sequences */
316 for (e = Al_El; e; e = e->Nxt)
320 switch (e->n->ntyp) {
325 while (f && f->n->ntyp == '.')
327 if (0) printf("link %d, {%d .. %d} -> %d (ntyp=%d) was %d\n",
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;
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);
340 e->n->sl->this->last = e->n->sl->this->last->nxt;
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
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 */
361 for (z = s; z; z = z->nxt)
362 { if (!z->this->frst)
364 if (z->this->frst->n->ntyp == ELSE)
366 fatal("duplicate `else'", (char *) 0);
367 if (z->nxt) /* is not already at the end */
370 prev_z->nxt = z->nxt;
376 ref_chans |= has_chanref(z->this->frst->n);
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;
388 && prev_z->this->frst->n->ntyp == ELSE)
389 { prev_z->this->frst->n->val = 1;
391 non_fatal("dubious use of 'else' combined with i/o,",
396 e->n = nn(n, tok, ZN, ZN);
397 e->n->sl = s; /* preserve as info only */
399 for (z = s; z; prev_z = z, z = z->nxt)
400 add_el(t, z->this); /* append target */
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 */
407 add_el(e, cur_s->this);
408 add_el(t, cur_s->this);
409 return e; /* destination node for label */
413 escape_el(Element *f, Sequence *e)
416 for (z = f->esc; z; z = z->nxt)
418 return; /* already there */
420 /* cover the lower-level escapes of this state */
421 for (z = f->esc; z; z = z->nxt)
422 attach_escape(z->this, e);
424 /* now attach escape to the state itself */
426 f->esc = seqlist(e, f->esc); /* in lifo order... */
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);
434 switch (f->n->ntyp) {
436 attach_escape(f->sub->this, e);
440 for (z = f->sub; z; z = z->nxt)
441 attach_escape(z->this, e);
444 /* attach only to the guard stmnt */
445 escape_el(f->n->sl->this->frst, e);
449 /* attach to all stmnts */
450 attach_escape(f->n->sl->this, e);
456 attach_escape(Sequence *n, Sequence *e)
459 for (f = n->frst; f; f = f->nxt)
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 */
473 e->n = nn(n, UNLESS, ZN, ZN);
474 e->n->sl = s; /* info only */
477 /* need 2 sequences: normal execution and escape */
478 if (!s || !s->nxt || s->nxt->nxt)
479 fatal("unexpected unless structure", (char *)0);
481 /* append the target state to both */
482 for (z = s; z; z = z->nxt)
485 /* attach escapes to all states in normal sequence */
486 attach_escape(s->this, s->nxt->this);
488 add_el(e, cur_s->this);
489 add_el(t, cur_s->this);
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);
507 { Lextok *t = nn(ZN, CONST, ZN, ZN);
509 return new_el(nn(ZN, 'c', t, ZN));
513 add_el(Element *e, Sequence *s)
515 if (e->n->ntyp == GOTO)
516 { Symbol *z = has_lab(e, (1|2|4));
518 { Element *y; /* insert a skip */
520 mov_lab(z, e, y); /* inherit label */
524 printf("add_el %d after %d -- ",
525 e->Seqno, (s->last)?s->last->Seqno:-1);
526 comment(stdout, e->n, 0);
542 { Element *e = colons(n->lft);
557 if (innermost->ntyp != IF
558 && innermost->ntyp != DO
559 && innermost->ntyp != UNLESS)
560 add_el(e, cur_s->this);
564 set_lab(Symbol *s, Element *e)
565 { Label *l; extern Symbol *context;
568 for (l = labtab; l; l = l->nxt)
569 if (l->s == s && l->c == context)
570 { non_fatal("label %s redeclared", s->name);
573 l = (Label *) emalloc(sizeof(Label));
582 get_lab(Lextok *n, int md)
586 for (l = labtab; l; l = l->nxt)
592 if (md) fatal("undefined label %s", s->name);
597 has_lab(Element *e, int special)
600 for (l = labtab; l; l = l->nxt)
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)))
613 mov_lab(Symbol *z, Element *e, Element *y)
616 for (l = labtab; l; l = l->nxt)
625 fatal("cannot happen - mov_lab %s", z->name);
629 fix_dest(Symbol *c, Symbol *a) /* c:label name, a:proctype name */
630 { Label *l; extern Symbol *context;
633 printf("ref to label '%s' in proctype '%s', search:\n",
635 for (l = labtab; l; l = l->nxt)
636 printf(" %s in %s\n", l->s->name, l->c->name);
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) /* ? */
645 { printf("spin: label '%s' (proctype %s)\n", c->name, a->name);
646 non_fatal("unknown label '%s'", c->name);
648 printf("spin: cannot remote ref a label inside the same proctype\n");
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;
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 */
662 y->Seqno = Unique++; y->Nxt = Al_El; Al_El = y;
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 */
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)",
679 find_lab(Symbol *s, Symbol *c, int markit)
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);
693 { Lbreak *r = (Lbreak *) emalloc(sizeof(Lbreak));
697 sprintf(buf, ":b%d", break_id++);
708 fatal("misplaced break statement", (char *)0);
709 return breakstack->l;
713 make_atomic(Sequence *s, int added)
716 walk_atomic(s->frst, s->last, added);
719 switch (f->n->ntyp) { /* is last step basic stmnt or sequence ? */
722 /* redo and search for the last step of that sequence */
723 make_atomic(f->n->sl->this, added);
727 /* escapes are folded into main sequence */
728 make_atomic(f->sub->this, added);
739 walk_atomic(Element *a, Element *b, int added)
740 { Element *f; Symbol *ofn; int oln;
745 for (f = a; ; f = f->nxt)
746 { f->status |= (ATOM|added);
747 switch (f->n->ntyp) {
750 printf("spin: warning, line %3d %s, atomic inside %s (ignored)\n",
751 f->n->ln, f->n->fn->name, (added)?"d_step":"atomic");
755 { if (added) goto mknonat;
758 printf("spin: warning, line %3d %s, d_step inside ",
759 f->n->ln, f->n->fn->name);
761 { printf("d_step (ignored)\n");
767 mknonat: f->n->ntyp = NON_ATOMIC; /* can jump here */
769 walk_atomic(h->this->frst, h->this->last, added);
773 { printf("spin: error, line %3d %s, unless in d_step (ignored)\n",
774 f->n->ln, f->n->fn->name);
777 for (h = f->sub; h; h = h->nxt)
778 walk_atomic(h->this->frst, h->this->last, added);
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);