1 /***** spin: pangen5.c *****/
3 /* Copyright (c) 1999-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 */
15 typedef struct BuildStack
{
17 struct BuildStack
*nxt
;
21 extern int verbose
, eventmapnr
, claimnr
, rvopt
, export_ast
, u_sync
;
22 extern Element
*Al_El
;
24 static FSM_state
*fsm_free
;
25 static FSM_trans
*trans_free
;
26 static BuildStack
*bs
, *bf
;
34 static void ana_seq(Sequence
*);
35 static void ana_stmnt(FSM_trans
*, Lextok
*, int);
37 extern void AST_slice(void);
38 extern void AST_store(ProcList
*, int);
39 extern int has_global(Lextok
*);
40 extern void exit(int);
46 /* fprintf(stderr, "omax %d, max=%d\n", o_max, max_st_id); */
47 if (o_max
< max_st_id
)
49 fsm_tbl
= (FSM_state
**) emalloc(max_st_id
* sizeof(FSM_state
*));
51 memset((char *)fsm_tbl
, 0, max_st_id
* sizeof(FSM_state
*));
52 cur_st_id
= max_st_id
;
55 for (f
= fsm
; f
; f
= f
->nxt
)
60 FSM_DFS(int from
, FSM_use
*u
)
72 { printf("cannot find state %d\n", from
);
73 fatal("fsm_dfs: cannot happen\n", (char *) 0);
80 for (t
= f
->t
; t
; t
= t
->nxt
)
82 for (n
= 0; n
< 2; n
++)
83 for (v
= t
->Val
[n
]; v
; v
= v
->nxt
)
85 return n
; /* a read or write */
87 if (!FSM_DFS(t
->to
, u
))
97 for (i
= 0; i
< cur_st_id
; i
++)
103 good_dead(Element
*e
, FSM_use
*u
)
105 switch (u
->special
) {
106 case 2: /* ok if it's a receive */
107 if (e
->n
->ntyp
== ASGN
108 && e
->n
->rgt
->ntyp
== CONST
109 && e
->n
->rgt
->val
== 0)
112 case 1: /* must be able to use oval */
113 if (e
->n
->ntyp
!= 'c'
114 && e
->n
->ntyp
!= 'r')
115 return 0; /* can't really happen */
122 static int howdeep
= 0;
126 eligible(FSM_trans
*v
)
131 if (el
) lt
= v
->step
->n
;
133 if (!lt
/* dead end */
134 || v
->nxt
/* has alternatives */
135 || el
->esc
/* has an escape */
136 || (el
->status
&CHECK2
) /* remotely referenced */
137 || lt
->ntyp
== ATOMIC
138 || lt
->ntyp
== NON_ATOMIC
/* used for inlines -- should be able to handle this */
140 || lt
->ntyp
== C_CODE
141 || lt
->ntyp
== C_EXPR
142 || has_lab(el
, 0) /* any label at all */
145 || lt
->ntyp
== UNLESS
146 || lt
->ntyp
== D_STEP
154 if (!(el
->status
&(2|4))) /* not atomic */
155 { int unsafe
= (el
->status
&I_GLOB
)?1:has_global(el
->n
);
164 canfill_in(FSM_trans
*v
)
165 { Element
*el
= v
->step
;
166 Lextok
*lt
= v
->step
->n
;
168 if (!lt
/* dead end */
169 || v
->nxt
/* has alternatives */
170 || el
->esc
/* has an escape */
171 || (el
->status
&CHECK2
)) /* remotely referenced */
174 if (!(el
->status
&(2|4)) /* not atomic */
175 && ((el
->status
&I_GLOB
)
176 || has_global(el
->n
))) /* and not safe */
183 pushbuild(FSM_trans
*v
)
186 for (b
= bs
; b
; b
= b
->nxt
)
193 b
= (BuildStack
*) emalloc(sizeof(BuildStack
));
204 fatal("cannot happen, popbuild", (char *) 0);
208 bf
= f
; /* freelist */
212 build_step(FSM_trans
*v
)
229 return v
->step
->merge
; /* already done */
231 if (!eligible(v
)) /* non-blocking */
234 if (!pushbuild(v
)) /* cycle detected */
235 return -1; /* break cycle */
241 { if (++howdeep
== 1)
242 printf("spin: %s, line %3d, merge:\n",
245 printf("\t[%d] <seqno %d>\t", howdeep
, el
->seqno
);
246 comment(stdout
, lt
, 0);
250 r
= build_step(f
->t
);
251 v
->step
->merge
= (r
== -1) ? st
: r
;
254 { printf(" merge value: %d (st=%d,r=%d, line %d)\n",
255 v
->step
->merge
, st
, r
, el
->n
->ln
);
261 return v
->step
->merge
;
265 FSM_MERGER(/* char *pname */ void) /* find candidates for safely merging steps */
270 for (f
= fsm
; f
; f
= f
->nxt
) /* all states */
271 for (t
= f
->t
; t
; t
= t
->nxt
) /* all edges */
272 { if (!t
->step
) continue; /* happens with 'unless' */
274 t
->step
->merge_in
= f
->in
; /* ?? */
282 || lt
->ntyp
== 's') /* blocking stmnts */
283 continue; /* handled in 2nd scan */
289 if (!g
|| !eligible(g
->t
))
293 t
->step
->merge_single
= t
->to
;
296 { printf("spin: %s, line %3d, merge_single:\n\t<seqno %d>\t",
297 t
->step
->n
->fn
->name
,
300 comment(stdout
, t
->step
->n
, 0);
305 /* t is an isolated eligible step:
307 * a merge_start can connect to a proper
308 * merge chain or to a merge_single
309 * a merge chain can be preceded by
310 * a merge_start, but not by a merge_single
316 (void) build_step(t
);
319 /* 2nd scan -- find possible merge_starts */
321 for (f
= fsm
; f
; f
= f
->nxt
) /* all states */
322 for (t
= f
->t
; t
; t
= t
->nxt
) /* all edges */
323 { if (!t
->step
|| t
->step
->merge
)
329 an rv send operation inside an atomic
, *loses
* atomicity
331 and should therefore never be merged with a subsequent
332 statement within the atomic sequence
333 the same is
not true for non
-rv send operations
336 if (lt
->ntyp
== 'c' /* potentially blocking stmnts */
338 || (lt
->ntyp
== 's' && u_sync
== 0)) /* added !u_sync in 4.1.3 */
339 { if (!canfill_in(t
)) /* atomic, non-global, etc. */
343 if (!g
|| !g
->t
|| !g
->t
->step
)
345 if (g
->t
->step
->merge
)
346 t
->step
->merge_start
= g
->t
->step
->merge
;
348 else if (g
->t
->step
->merge_single
)
349 t
->step
->merge_start
= g
->t
->step
->merge_single
;
353 && t
->step
->merge_start
)
354 { printf("spin: %s, line %3d, merge_START:\n\t<seqno %d>\t",
358 comment(stdout
, lt
, 0);
373 for (f
= fsm
; f
; f
= f
->nxt
) /* all states */
374 for (t
= f
->t
; t
; t
= t
->nxt
) /* all edges */
375 for (n
= 0; n
< 2; n
++) /* reads and writes */
376 for (u
= t
->Val
[n
]; u
; u
= u
->nxt
)
377 { if (!u
->var
->context
/* global */
378 || u
->var
->type
== CHAN
379 || u
->var
->type
== STRUCT
)
382 if (FSM_DFS(t
->to
, u
)) /* cannot hit read before hitting write */
383 u
->special
= n
+1; /* means, reset to 0 after use */
387 for (f
= fsm
; f
; f
= f
->nxt
)
388 for (t
= f
->t
; t
; t
= t
->nxt
)
389 for (n
= 0; n
< 2; n
++)
390 for (u
= t
->Val
[n
], w
= (FSM_use
*) 0; u
; )
393 if (!w
) /* remove from list */
399 { printf("%s : %3d: %d -> %d \t",
400 t
->step
->n
->fn
->name
,
404 comment(stdout
, t
->step
->n
, 0);
405 printf("\t%c%d: %s\n", n
==0?'R':'L',
406 u
->special
, u
->var
->name
);
409 if (good_dead(t
->step
, u
))
410 { u
->nxt
= t
->step
->dead
; /* insert into dead */
425 u
->var
= (Symbol
*) 0;
432 rel_trans(FSM_trans
*t
)
438 t
->Val
[0] = t
->Val
[1] = (FSM_use
*) 0;
444 rel_state(FSM_state
*f
)
449 f
->t
= (FSM_trans
*) 0;
458 fsm
= (FSM_state
*) 0;
465 /* fsm_tbl isn't allocated yet */
466 for (f
= fsm
; f
; f
= f
->nxt
)
472 memset(f
, 0, sizeof(FSM_state
));
473 fsm_free
= fsm_free
->nxt
;
475 f
= (FSM_state
*) emalloc(sizeof(FSM_state
));
477 f
->t
= (FSM_trans
*) 0;
492 memset(t
, 0, sizeof(FSM_trans
));
493 trans_free
= trans_free
->nxt
;
495 t
= (FSM_trans
*) emalloc(sizeof(FSM_trans
));
502 FSM_EDGE(int from
, int to
, Element
*e
)
506 f
= mkstate(from
); /* find it or else make it */
517 { t
= get_trans(from
);
519 t
->nxt
= f
->p
; /* from is a predecessor of to */
524 ana_stmnt(t
, t
->step
->n
, 0);
531 ana_var(FSM_trans
*t
, Lextok
*now
, int usage
)
534 if (!t
|| !now
|| !now
->sym
)
537 if (now
->sym
->name
[0] == '_'
538 && (strcmp(now
->sym
->name
, "_") == 0
539 || strcmp(now
->sym
->name
, "_pid") == 0
540 || strcmp(now
->sym
->name
, "_last") == 0))
544 for (u
= v
; u
; u
= u
->nxt
)
545 if (u
->var
== now
->sym
)
546 return; /* it's already there */
549 { /* not for array vars -- it's hard to tell statically
550 if the index would, at runtime, evaluate to the
551 same values at lval and rval references
555 use_free
= use_free
->nxt
;
557 u
= (FSM_use
*) emalloc(sizeof(FSM_use
));
560 u
->nxt
= t
->Val
[usage
];
563 ana_stmnt(t
, now
->lft
, RVAL
); /* index */
565 if (now
->sym
->type
== STRUCT
568 ana_var(t
, now
->rgt
->lft
, usage
);
572 ana_stmnt(FSM_trans
*t
, Lextok
*now
, int usage
)
575 if (!t
|| !now
) return;
608 ana_stmnt(t
, now
->lft
, RVAL
);
629 ana_stmnt(t
, now
->lft
, RVAL
);
630 ana_stmnt(t
, now
->rgt
, RVAL
);
634 ana_stmnt(t
, now
->lft
, LVAL
);
635 ana_stmnt(t
, now
->rgt
, RVAL
);
640 for (v
= now
->lft
; v
; v
= v
->rgt
)
641 ana_stmnt(t
, v
->lft
, RVAL
);
645 if (now
->lft
&& !now
->lft
->ismtyp
)
646 ana_stmnt(t
, now
->lft
, RVAL
);
650 ana_stmnt(t
, now
->lft
, RVAL
);
651 for (v
= now
->rgt
; v
; v
= v
->rgt
)
652 ana_stmnt(t
, v
->lft
, RVAL
);
657 ana_stmnt(t
, now
->lft
, RVAL
);
658 for (v
= now
->rgt
; v
; v
= v
->rgt
)
659 { if (v
->lft
->ntyp
== EVAL
)
660 ana_stmnt(t
, v
->lft
->lft
, RVAL
);
662 if (v
->lft
->ntyp
!= CONST
663 && now
->ntyp
!= 'R') /* was v->lft->ntyp */
664 ana_stmnt(t
, v
->lft
, LVAL
);
669 ana_stmnt(t
, now
->lft
, RVAL
);
671 { ana_stmnt(t
, now
->rgt
->lft
, RVAL
);
672 ana_stmnt(t
, now
->rgt
->rgt
, RVAL
);
677 ana_var(t
, now
, usage
);
680 case 'p': /* remote ref */
681 ana_stmnt(t
, now
->lft
->lft
, RVAL
); /* process id */
682 ana_var(t
, now
, RVAL
);
683 ana_var(t
, now
->rgt
, RVAL
);
687 printf("spin: bad node type %d line %d (ana_stmnt)\n", now
->ntyp
, now
->ln
);
688 fatal("aborting", (char *) 0);
693 ana_src(int dataflow
, int merger
) /* called from main.c and guided.c */
699 for (p
= rdy
; p
; p
= p
->nxt
)
700 { if (p
->tn
== eventmapnr
709 if (dataflow
|| merger
)
710 { printf("spin: %d, optimizing '%s'",
711 counter
++, p
->n
->name
);
719 { FSM_MERGER(/* p->n->name */);
720 huntele(e
, e
->status
, -1)->merge_in
= 1; /* start-state */
726 AST_store(p
, huntele(e
, e
->status
, -1)->seqno
);
730 for (e
= Al_El
; e
; e
= e
->Nxt
)
732 if (!(e
->status
&DONE
) && (verbose
&32))
733 { printf("unreachable code: ");
734 printf("%s, line %3d: ",
735 e
->n
->fn
->name
, e
->n
->ln
);
736 comment(stdout
, e
->n
, 0);
748 spit_recvs(FILE *f1
, FILE *f2
) /* called from pangen2.c */
753 fprintf(f1
, "unsigned char Is_Recv[%d];\n", Unique
);
755 fprintf(f2
, "void\nset_recvs(void)\n{\n");
756 for (e
= Al_El
; e
; e
= e
->Nxt
)
757 { if (!e
->n
) continue;
759 switch (e
->n
->ntyp
) {
761 markit
: fprintf(f2
, "\tIs_Recv[%d] = 1;\n", e
->Seqno
);
765 switch (s
->frst
->n
->ntyp
) {
767 fatal("unexpected: do at start of d_step", (char *) 0);
768 case IF
: /* conservative: fall through */
769 case 'r': goto markit
;
778 fprintf(f2
, "int\nno_recvs(int me)\n{\n");
779 fprintf(f2
, " int h; uchar ot; short tt;\n");
780 fprintf(f2
, " Trans *t;\n");
781 fprintf(f2
, " for (h = BASE; h < (int) now._nr_pr; h++)\n");
782 fprintf(f2
, " { if (h == me) continue;\n");
783 fprintf(f2
, " tt = (short) ((P0 *)pptr(h))->_p;\n");
784 fprintf(f2
, " ot = (uchar) ((P0 *)pptr(h))->_t;\n");
785 fprintf(f2
, " for (t = trans[ot][tt]; t; t = t->nxt)\n");
786 fprintf(f2
, " if (Is_Recv[t->t_id]) return 0;\n");
788 fprintf(f2
, " return 1;\n");
800 for (e
= s
->frst
; e
; e
= e
->nxt
)
801 { if (e
->status
& DONE
)
808 if (e
->n
->ntyp
== UNLESS
)
809 ana_seq(e
->sub
->this);
811 { for (h
= e
->sub
; h
; h
= h
->nxt
)
812 { g
= huntstart(h
->this->frst
);
815 if (g
->n
->ntyp
!= 'c'
816 || g
->n
->lft
->ntyp
!= CONST
817 || g
->n
->lft
->val
!= 0
819 FSM_EDGE(From
, To
, e
);
820 /* else it's a dead link */
822 for (h
= e
->sub
; h
; h
= h
->nxt
)
824 } else if (e
->n
->ntyp
== ATOMIC
825 || e
->n
->ntyp
== D_STEP
826 || e
->n
->ntyp
== NON_ATOMIC
)
829 g
= huntstart(t
->frst
);
830 t
->last
->nxt
= e
->nxt
;
832 FSM_EDGE(From
, To
, e
);
836 { if (e
->n
->ntyp
== GOTO
)
837 { g
= get_lab(e
->n
, 1);
838 g
= huntele(g
, e
->status
, -1);
841 { g
= huntele(e
->nxt
, e
->status
, -1);
846 FSM_EDGE(From
, To
, e
);
849 && e
->n
->ntyp
!= GOTO
850 && e
->n
->ntyp
!= '.')
851 for (h
= e
->esc
; h
; h
= h
->nxt
)
852 { g
= huntstart(h
->this->frst
);
854 FSM_EDGE(From
, To
, ZE
);
859 checklast
: if (e
== s
->last
)