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
);
This page took 0.06253 seconds and 5 git commands to generate.