1 /***** spin: pangen6.c *****/
3 /* Copyright (c) 2000-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 */
12 /* Abstract syntax tree analysis / slicing (spin option -A) */
13 /* AST_store stores the fsms's for each proctype */
14 /* AST_track keeps track of variables used in properties */
15 /* AST_slice starts the slicing algorithm */
16 /* it first collects more info and then calls */
17 /* AST_criteria to process the slice criteria */
22 extern Ordered
*all_names
;
23 extern FSM_use
*use_free
;
24 extern FSM_state
**fsm_tbl
;
25 extern FSM_state
*fsm
;
26 extern int verbose
, o_max
;
28 static FSM_trans
*cur_t
;
29 static FSM_trans
*expl_par
;
30 static FSM_trans
*expl_var
;
31 static FSM_trans
*explicit;
33 extern void rel_use(FSM_use
*);
35 #define ulong unsigned long
44 ProcList
*p
; /* proctype decl */
45 int i_st
; /* start state */
48 Pair
*pairs
; /* entry and exit nodes of proper subgraphs */
49 FSM_state
*fsm
; /* proctype body */
50 struct AST
*nxt
; /* linked list */
53 typedef struct RPN
{ /* relevant proctype names */
58 typedef struct ALIAS
{ /* channel aliasing info */
59 Lextok
*cnm
; /* this chan */
60 int origin
; /* debugging - origin of the alias */
61 struct ALIAS
*alias
; /* can be an alias for these other chans */
62 struct ALIAS
*nxt
; /* linked list */
65 typedef struct ChanList
{
66 Lextok
*s
; /* containing stmnt */
67 Lextok
*n
; /* point of reference - could be struct */
68 struct ChanList
*nxt
; /* linked list */
71 /* a chan alias can be created in one of three ways:
72 assignement to chan name
73 a = b -- a is now an alias for b
74 passing chan name as parameter in run
75 run x(b) -- proctype x(chan a)
76 passing chan name through channel
86 static ALIAS
*chalcur
;
87 static ALIAS
*chalias
;
88 static ChanList
*chanlist
;
89 static Slicer
*slicer
;
90 static Slicer
*rel_vars
; /* all relevant variables */
91 static int AST_Changes
;
94 static int in_recv
= 0;
96 static int AST_mutual(Lextok
*, Lextok
*, int);
97 static void AST_dominant(void);
98 static void AST_hidden(void);
99 static void AST_setcur(Lextok
*);
100 static void check_slice(Lextok
*, int);
101 static void curtail(AST
*);
102 static void def_use(Lextok
*, int);
103 static void name_AST_track(Lextok
*, int);
104 static void show_expl(void);
107 AST_isini(Lextok
*n
) /* is this an initialized channel */
110 if (!n
|| !n
->sym
) return 0;
115 return (s
->ini
->ntyp
== CHAN
); /* freshly instantiated */
117 if (s
->type
== STRUCT
&& n
->rgt
)
118 return AST_isini(n
->rgt
->lft
);
124 AST_var(Lextok
*n
, Symbol
*s
, int toplevel
)
129 { if (s
->context
&& s
->type
)
130 printf(":%s:L:", s
->context
->name
);
134 printf("%s", s
->name
); /* array indices ignored */
136 if (s
->type
== STRUCT
&& n
&& n
->rgt
&& n
->rgt
->lft
)
138 AST_var(n
->rgt
->lft
, n
->rgt
->lft
->sym
, 0);
143 name_def_indices(Lextok
*n
, int code
)
145 if (!n
|| !n
->sym
) return;
147 if (n
->sym
->nel
!= 1)
148 def_use(n
->lft
, code
); /* process the index */
150 if (n
->sym
->type
== STRUCT
/* and possible deeper ones */
152 name_def_indices(n
->rgt
->lft
, code
);
156 name_def_use(Lextok
*n
, int code
)
164 { switch (cur_t
->step
->n
->ntyp
) {
165 case 'c': /* possible predicate abstraction? */
166 n
->sym
->colnr
|= 2; /* yes */
169 n
->sym
->colnr
|= 1; /* no */
174 for (u
= cur_t
->Val
[0]; u
; u
= u
->nxt
)
175 if (AST_mutual(n
, u
->n
, 1)
176 && u
->special
== code
)
181 use_free
= use_free
->nxt
;
183 u
= (FSM_use
*) emalloc(sizeof(FSM_use
));
187 u
->nxt
= cur_t
->Val
[0];
190 name_def_indices(n
, USE
|(code
&(~DEF
))); /* not def, but perhaps deref */
194 def_use(Lextok
*now
, int code
)
206 def_use(now
->lft
, USE
|code
);
214 def_use(now
->lft
, DEREF_USE
|USE
|code
);
235 def_use(now
->lft
, USE
|code
);
236 def_use(now
->rgt
, USE
|code
);
240 def_use(now
->lft
, DEF
|code
);
241 def_use(now
->rgt
, USE
|code
);
244 case TYPE
: /* name in parameter list */
245 name_def_use(now
, code
);
249 name_def_use(now
, code
);
253 name_def_use(now
, USE
); /* procname - not really needed */
254 for (v
= now
->lft
; v
; v
= v
->rgt
)
255 def_use(v
->lft
, USE
); /* params */
259 def_use(now
->lft
, DEREF_DEF
|DEREF_USE
|USE
|code
);
260 for (v
= now
->rgt
; v
; v
= v
->rgt
)
261 def_use(v
->lft
, USE
|code
);
265 def_use(now
->lft
, DEREF_DEF
|DEREF_USE
|USE
|code
);
266 for (v
= now
->rgt
; v
; v
= v
->rgt
)
267 { if (v
->lft
->ntyp
== EVAL
)
268 def_use(v
->lft
, code
); /* will add USE */
269 else if (v
->lft
->ntyp
!= CONST
)
270 def_use(v
->lft
, DEF
|code
);
275 def_use(now
->lft
, DEREF_USE
|USE
|code
);
276 for (v
= now
->rgt
; v
; v
= v
->rgt
)
277 { if (v
->lft
->ntyp
== EVAL
)
278 def_use(v
->lft
, code
); /* will add USE */
283 def_use(now
->lft
, USE
|code
);
285 { def_use(now
->rgt
->lft
, code
);
286 def_use(now
->rgt
->rgt
, code
);
291 for (v
= now
->lft
; v
; v
= v
->rgt
)
292 def_use(v
->lft
, USE
|code
);
296 def_use(now
->lft
, USE
);
326 AST_add_alias(Lextok
*n
, int nr
)
330 for (ca
= chalcur
->alias
; ca
; ca
= ca
->nxt
)
331 if (AST_mutual(ca
->cnm
, n
, 1))
332 { res
= (ca
->origin
&nr
);
333 ca
->origin
|= nr
; /* 1, 2, or 4 - run, asgn, or rcv */
334 return (res
== 0); /* 0 if already there with same origin */
337 ca
= (ALIAS
*) emalloc(sizeof(ALIAS
));
340 ca
->nxt
= chalcur
->alias
;
346 AST_run_alias(char *pn
, char *s
, Lextok
*t
, int parno
)
353 { if (strcmp(t
->sym
->name
, s
) == 0)
354 for (v
= t
->lft
, cnt
= 1; v
; v
= v
->rgt
, cnt
++)
356 { AST_add_alias(v
->lft
, 1); /* RUN */
360 { AST_run_alias(pn
, s
, t
->lft
, parno
);
361 AST_run_alias(pn
, s
, t
->rgt
, parno
);
366 AST_findrun(char *s
, int parno
)
371 for (a
= ast
; a
; a
= a
->nxt
) /* automata */
372 for (f
= a
->fsm
; f
; f
= f
->nxt
) /* control states */
373 for (t
= f
->t
; t
; t
= t
->nxt
) /* transitions */
375 AST_run_alias(a
->p
->n
->name
, s
, t
->step
->n
, parno
);
380 AST_par_chans(ProcList
*p
) /* find local chan's init'd to chan passed as param */
384 for (walk
= all_names
; walk
; walk
= walk
->next
)
388 && strcmp(sp
->context
->name
, p
->n
->name
) == 0
389 && sp
->Nid
>= 0 /* not itself a param */
391 && sp
->ini
->ntyp
== NAME
) /* != CONST and != CHAN */
392 { Lextok
*x
= nn(ZN
, 0, ZN
, ZN
);
395 AST_add_alias(sp
->ini
, 2); /* ASGN */
400 AST_para(ProcList
*p
)
406 for (f
= p
->p
; f
; f
= f
->rgt
) /* list of types */
407 for (t
= f
->lft
; t
; t
= t
->rgt
)
408 { if (t
->ntyp
!= ',')
411 c
= t
->lft
; /* expanded struct */
414 if (Sym_typ(c
) == CHAN
)
415 { ALIAS
*na
= (ALIAS
*) emalloc(sizeof(ALIAS
));
419 chalcur
= chalias
= na
;
421 printf("%s -- (par) -- ", p
->n
->name
);
422 AST_var(c
, c
->sym
, 1);
425 AST_findrun(p
->n
->name
, cnt
);
434 AST_haschan(Lextok
*c
)
437 if (Sym_typ(c
) == CHAN
)
438 { AST_add_alias(c
, 2); /* ASGN */
441 AST_var(c
, c
->sym
, 1);
445 { AST_haschan(c
->rgt
);
451 AST_nrpar(Lextok
*n
) /* 's' or 'r' */
455 for (m
= n
->rgt
; m
; m
= m
->rgt
)
461 AST_ord(Lextok
*n
, Lextok
*s
)
465 for (m
= n
->rgt
; m
; m
= m
->rgt
)
467 if (s
->sym
== m
->lft
->sym
)
475 AST_ownership(Symbol
*s
)
478 printf("%s:", s
->name
);
479 AST_ownership(s
->owner
);
484 AST_mutual(Lextok
*a
, Lextok
*b
, int toplevel
)
487 if (!a
&& !b
) return 1;
489 if (!a
|| !b
) return 0;
494 if (!as
|| !bs
) return 0;
496 if (toplevel
&& as
->context
!= bs
->context
)
499 if (as
->type
!= bs
->type
)
502 if (strcmp(as
->name
, bs
->name
) != 0)
505 if (as
->type
== STRUCT
&& a
->rgt
&& b
->rgt
) /* we know that a and b are not null */
506 return AST_mutual(a
->rgt
->lft
, b
->rgt
->lft
, 0);
512 AST_setcur(Lextok
*n
) /* set chalcur */
515 for (ca
= chalias
; ca
; ca
= ca
->nxt
)
516 if (AST_mutual(ca
->cnm
, n
, 1)) /* if same chan */
521 ca
= (ALIAS
*) emalloc(sizeof(ALIAS
));
524 chalcur
= chalias
= ca
;
528 AST_other(AST
*a
) /* check chan params in asgns and recvs */
534 for (f
= a
->fsm
; f
; f
= f
->nxt
) /* control states */
535 for (t
= f
->t
; t
; t
= t
->nxt
) /* transitions */
536 for (u
= t
->Val
[0]; u
; u
= u
->nxt
) /* def/use info */
537 if (Sym_typ(u
->n
) == CHAN
538 && (u
->special
&DEF
)) /* def of chan-name */
540 switch (t
->step
->n
->ntyp
) {
542 AST_haschan(t
->step
->n
->rgt
);
545 /* guess sends where name may originate */
546 for (cl
= chanlist
; cl
; cl
= cl
->nxt
) /* all sends */
547 { int aa
= AST_nrpar(cl
->s
);
548 int bb
= AST_nrpar(t
->step
->n
);
549 if (aa
!= bb
) /* matching nrs of params */
552 aa
= AST_ord(cl
->s
, cl
->n
);
553 bb
= AST_ord(t
->step
->n
, u
->n
);
554 if (aa
!= bb
) /* same position in parlist */
557 AST_add_alias(cl
->n
, 4); /* RCV assume possible match */
561 printf("type = %d\n", t
->step
->n
->ntyp
);
562 non_fatal("unexpected chan def type", (char *) 0);
571 for (na
= chalias
; na
; na
= na
->nxt
)
572 { printf("\npossible aliases of ");
573 AST_var(na
->cnm
, na
->cnm
->sym
, 1);
575 for (ca
= na
->alias
; ca
; ca
= ca
->nxt
)
577 printf("no valid name ");
579 AST_var(ca
->cnm
, ca
->cnm
->sym
, 1);
581 if (ca
->origin
& 1) printf("RUN ");
582 if (ca
->origin
& 2) printf("ASGN ");
583 if (ca
->origin
& 4) printf("RCV ");
584 printf("[%s]", AST_isini(ca
->cnm
)?"Initzd":"Name");
586 if (ca
->nxt
) printf(", ");
594 AST_indirect(FSM_use
*uin
, FSM_trans
*t
, char *cause
, char *pn
)
597 /* this is a newly discovered relevant statement */
598 /* all vars it uses to contribute to its DEF are new criteria */
600 if (!(t
->relevant
&1)) AST_Changes
++;
602 t
->round
= AST_Round
;
605 if ((verbose
&32) && t
->step
)
606 { printf("\tDR %s [[ ", pn
);
607 comment(stdout
, t
->step
->n
, 0);
608 printf("]]\n\t\tfully relevant %s", cause
);
609 if (uin
) { printf(" due to "); AST_var(uin
->n
, uin
->n
->sym
, 1); }
612 for (u
= t
->Val
[0]; u
; u
= u
->nxt
)
614 && (u
->special
&(USE
|DEREF_USE
)))
616 { printf("\t\t\tuses(%d): ", u
->special
);
617 AST_var(u
->n
, u
->n
->sym
, 1);
620 name_AST_track(u
->n
, u
->special
); /* add to slice criteria */
625 def_relevant(char *pn
, FSM_trans
*t
, Lextok
*n
, int ischan
)
630 /* look for all DEF's of n
631 * mark those stmnts relevant
632 * mark all var USEs in those stmnts as criteria
636 for (u
= t
->Val
[0]; u
; u
= u
->nxt
)
637 { chanref
= (Sym_typ(u
->n
) == CHAN
);
639 if (ischan
!= chanref
/* no possible match */
640 || !(u
->special
&(DEF
|DEREF_DEF
))) /* not a def */
643 if (AST_mutual(u
->n
, n
, 1))
644 { AST_indirect(u
, t
, "(exact match)", pn
);
649 for (na
= chalias
; na
; na
= na
->nxt
)
650 { if (!AST_mutual(u
->n
, na
->cnm
, 1))
652 for (ca
= na
->alias
; ca
; ca
= ca
->nxt
)
653 if (AST_mutual(ca
->cnm
, n
, 1)
654 && AST_isini(ca
->cnm
))
655 { AST_indirect(u
, t
, "(alias match)", pn
);
663 AST_relevant(Lextok
*n
)
669 /* look for all DEF's of n
670 * mark those stmnts relevant
671 * mark all var USEs in those stmnts as criteria
675 ischan
= (Sym_typ(n
) == CHAN
);
678 { printf("<<ast_relevant (ntyp=%d) ", n
->ntyp
);
679 AST_var(n
, n
->sym
, 1);
683 for (t
= expl_par
; t
; t
= t
->nxt
) /* param assignments */
684 { if (!(t
->relevant
&1))
685 def_relevant(":params:", t
, n
, ischan
);
688 for (t
= expl_var
; t
; t
= t
->nxt
)
689 { if (!(t
->relevant
&1)) /* var inits */
690 def_relevant(":vars:", t
, n
, ischan
);
693 for (a
= ast
; a
; a
= a
->nxt
) /* all other stmnts */
694 { if (strcmp(a
->p
->n
->name
, ":never:") != 0
695 && strcmp(a
->p
->n
->name
, ":trace:") != 0
696 && strcmp(a
->p
->n
->name
, ":notrace:") != 0)
697 for (f
= a
->fsm
; f
; f
= f
->nxt
)
698 for (t
= f
->t
; t
; t
= t
->nxt
)
699 { if (!(t
->relevant
&1))
700 def_relevant(a
->p
->n
->name
, t
, n
, ischan
);
709 for (T
= expl_par
; T
; T
= (T
== expl_par
)?expl_var
: (FSM_trans
*) 0)
710 for (t
= T
; t
; t
= t
->nxt
)
712 for (u
= t
->Val
[0]; u
; u
= u
->nxt
)
713 { if (u
->n
->sym
->type
714 && u
->n
->sym
->context
715 && strcmp(u
->n
->sym
->context
->name
, s
) == 0)
718 { printf("proctype %s relevant, due to symbol ", s
);
719 AST_var(u
->n
, u
->n
->sym
, 1);
732 for (r
= rpn
; r
; r
= r
->nxt
)
733 { for (a
= ast
; a
; a
= a
->nxt
)
734 if (strcmp(a
->p
->n
->name
, r
->rn
->name
) == 0)
739 fatal("cannot find proctype %s", r
->rn
->name
);
744 AST_procisrelevant(Symbol
*s
)
746 for (r
= rpn
; r
; r
= r
->nxt
)
747 if (strcmp(r
->rn
->name
, s
->name
) == 0)
749 r
= (RPN
*) emalloc(sizeof(RPN
));
756 AST_proc_isrel(char *s
)
759 for (a
= ast
; a
; a
= a
->nxt
)
760 if (strcmp(a
->p
->n
->name
, s
) == 0)
761 return (a
->relevant
&1);
762 non_fatal("cannot happen, missing proc in ast", (char *) 0);
767 AST_scoutrun(Lextok
*t
)
772 return AST_proc_isrel(t
->sym
->name
);
773 return (AST_scoutrun(t
->lft
) || AST_scoutrun(t
->rgt
));
782 /* if any stmnt inside a proctype is relevant
783 * or any parameter passed in a run
784 * then so are all the run statements on that proctype
787 for (a
= ast
; a
; a
= a
->nxt
)
788 { if (strcmp(a
->p
->n
->name
, ":never:") == 0
789 || strcmp(a
->p
->n
->name
, ":trace:") == 0
790 || strcmp(a
->p
->n
->name
, ":notrace:") == 0
791 || strcmp(a
->p
->n
->name
, ":init:") == 0)
792 { a
->relevant
|= 1; /* the proctype is relevant */
795 if (AST_relpar(a
->p
->n
->name
))
798 { for (f
= a
->fsm
; f
; f
= f
->nxt
)
799 for (t
= f
->t
; t
; t
= t
->nxt
)
807 for (a
= ast
; a
; a
= a
->nxt
)
808 for (f
= a
->fsm
; f
; f
= f
->nxt
)
809 for (t
= f
->t
; t
; t
= t
->nxt
)
811 && AST_scoutrun(t
->step
->n
))
812 { AST_indirect((FSM_use
*)0, t
, ":run:", a
->p
->n
->name
);
813 /* BUT, not all actual params are relevant */
818 AST_report(AST
*a
, Element
*e
) /* ALSO deduce irrelevant vars */
820 if (!(a
->relevant
&2))
822 printf("spin: redundant in proctype %s (for given property):\n",
825 printf(" line %3d %s (state %d)",
827 e
->n
?e
->n
->fn
->name
:"-",
830 comment(stdout
, e
->n
, 0);
835 AST_always(Lextok
*n
)
839 if (n
->ntyp
== '@' /* -end */
840 || n
->ntyp
== 'p') /* remote reference */
842 return AST_always(n
->lft
) || AST_always(n
->rgt
);
846 AST_edge_dump(AST
*a
, FSM_state
*f
)
850 for (t
= f
->t
; t
; t
= t
->nxt
) /* edges */
852 if (t
->step
&& AST_always(t
->step
->n
))
853 t
->relevant
|= 1; /* always relevant */
856 { switch (t
->relevant
) {
857 case 0: printf(" "); break;
858 case 1: printf("*%3d ", t
->round
); break;
859 case 2: printf("+%3d ", t
->round
); break;
860 case 3: printf("#%3d ", t
->round
); break;
861 default: printf("? "); break;
864 printf("%d\t->\t%d\t", f
->from
, t
->to
);
866 comment(stdout
, t
->step
->n
, 0);
870 for (u
= t
->Val
[0]; u
; u
= u
->nxt
)
872 AST_var(u
->n
, u
->n
->sym
, 1);
873 printf(":%d>", u
->special
);
881 switch(t
->step
->n
->ntyp
) {
886 if (t
->step
->n
->lft
->ntyp
!= CONST
)
887 AST_report(a
, t
->step
);
890 case PRINT
: /* don't report */
901 AST_dfs(AST
*a
, int s
, int vis
)
909 if (vis
) AST_edge_dump(a
, f
);
911 for (t
= f
->t
; t
; t
= t
->nxt
)
912 AST_dfs(a
, t
->to
, vis
);
919 for (f
= a
->fsm
; f
; f
= f
->nxt
)
921 fsm_tbl
[f
->from
] = f
;
925 printf("AST_START %s from %d\n", a
->p
->n
->name
, a
->i_st
);
927 AST_dfs(a
, a
->i_st
, 1);
937 for (f
= a
->fsm
; f
; f
= f
->nxt
) /* control states */
938 for (t
= f
->t
; t
; t
= t
->nxt
) /* transitions */
941 && t
->step
->n
->ntyp
== 's')
942 for (u
= t
->Val
[0]; u
; u
= u
->nxt
)
943 { if (Sym_typ(u
->n
) == CHAN
944 && ((u
->special
&USE
) && !(u
->special
&DEREF_USE
)))
947 printf("%s -- (%d->%d) -- ",
948 a
->p
->n
->name
, f
->from
, t
->to
);
949 AST_var(u
->n
, u
->n
->sym
, 1);
950 printf(" -> chanlist\n");
952 cl
= (ChanList
*) emalloc(sizeof(ChanList
));
960 AST_alfind(Lextok
*n
)
963 for (na
= chalias
; na
; na
= na
->nxt
)
964 if (AST_mutual(na
->cnm
, n
, 1))
971 { ALIAS
*na
, *ca
, *da
, *ea
;
976 for (na
= chalias
; na
; na
= na
->nxt
)
978 for (ca
= na
->alias
; ca
; ca
= ca
->nxt
)
979 { da
= AST_alfind(ca
->cnm
);
981 for (ea
= da
->alias
; ea
; ea
= ea
->nxt
)
982 { nchanges
+= AST_add_alias(ea
->cnm
,
983 ea
->origin
|ca
->origin
);
985 } while (nchanges
> 0);
987 chalcur
= (ALIAS
*) 0;
995 for (f
= a
->fsm
; f
; f
= f
->nxt
) /* control states */
996 for (t
= f
->t
; t
; t
= t
->nxt
) /* all edges */
998 rel_use(t
->Val
[0]); /* redo Val; doesn't cover structs */
1000 t
->Val
[0] = t
->Val
[1] = (FSM_use
*) 0;
1002 if (!t
->step
) continue;
1004 def_use(t
->step
->n
, 0); /* def/use info, including structs */
1006 cur_t
= (FSM_trans
*) 0;
1010 name_AST_track(Lextok
*n
, int code
)
1011 { extern int nr_errs
;
1013 printf("AST_name: ");
1014 AST_var(n
, n
->sym
, 1);
1015 printf(" -- %d\n", code
);
1017 if (in_recv
&& (code
&DEF
) && (code
&USE
))
1018 { printf("spin: error: DEF and USE of same var in rcv stmnt: ");
1019 AST_var(n
, n
->sym
, 1);
1020 printf(" -- %d\n", code
);
1023 check_slice(n
, code
);
1027 AST_track(Lextok
*now
, int code
) /* called from main.c */
1028 { Lextok
*v
; extern int export_ast
;
1030 if (!export_ast
) return;
1033 switch (now
->ntyp
) {
1039 AST_track(now
->lft
, DEREF_USE
|USE
|code
);
1060 AST_track(now
->rgt
, USE
|code
);
1068 AST_track(now
->lft
, USE
|code
);
1072 AST_track(now
->lft
, USE
|(code
&(~DEF
)));
1076 name_AST_track(now
, code
);
1077 if (now
->sym
->nel
!= 1)
1078 AST_track(now
->lft
, USE
|code
); /* index */
1082 AST_track(now
->lft
, DEREF_USE
|USE
|code
);
1083 for (v
= now
->rgt
; v
; v
= v
->rgt
)
1084 AST_track(v
->lft
, code
); /* a deeper eval can add USE */
1088 AST_track(now
->lft
, USE
|code
);
1090 { AST_track(now
->rgt
->lft
, code
);
1091 AST_track(now
->rgt
->rgt
, code
);
1095 /* added for control deps: */
1097 name_AST_track(now
, code
);
1100 AST_track(now
->lft
, DEF
|code
);
1101 AST_track(now
->rgt
, USE
|code
);
1104 name_AST_track(now
, USE
);
1105 for (v
= now
->lft
; v
; v
= v
->rgt
)
1106 AST_track(v
->lft
, USE
|code
);
1109 AST_track(now
->lft
, DEREF_DEF
|DEREF_USE
|USE
|code
);
1110 for (v
= now
->rgt
; v
; v
= v
->rgt
)
1111 AST_track(v
->lft
, USE
|code
);
1114 AST_track(now
->lft
, DEREF_DEF
|DEREF_USE
|USE
|code
);
1115 for (v
= now
->rgt
; v
; v
= v
->rgt
)
1117 AST_track(v
->lft
, DEF
|code
);
1122 for (v
= now
->lft
; v
; v
= v
->rgt
)
1123 AST_track(v
->lft
, USE
|code
);
1126 AST_track(now
->lft
, USE
);
1133 '?' -sym
-> a (proctype
)
1137 AST_track(now
->lft
->lft
, USE
|code
);
1138 AST_procisrelevant(now
->lft
->sym
);
1164 printf("AST_track, NOT EXPECTED ntyp: %d\n", now
->ntyp
);
1177 { printf("Relevant variables:\n");
1178 for (rv
= rel_vars
; rv
; rv
= rv
->nxt
)
1180 AST_var(rv
->n
, rv
->n
->sym
, 1);
1185 for (rv
= rel_vars
; rv
; rv
= rv
->nxt
)
1186 rv
->n
->sym
->setat
= 1; /* mark it */
1188 for (walk
= all_names
; walk
; walk
= walk
->next
)
1192 && (s
->type
!= MTYPE
|| s
->ini
->ntyp
!= CONST
)
1193 && s
->type
!= STRUCT
/* report only fields */
1194 && s
->type
!= PROCTYPE
1196 && sputtype(buf
, s
->type
))
1199 printf("spin: redundant vars (for given property):\n");
1208 AST_suggestions(void)
1217 for (walk
= all_names
; walk
; walk
= walk
->next
)
1219 if (s
->colnr
== 2 /* only used in conditionals */
1223 || s
->type
== MTYPE
))
1226 printf("spin: consider using predicate");
1227 printf(" abstraction to replace:\n");
1233 /* look for source and sink processes */
1235 for (a
= ast
; a
; a
= a
->nxt
) /* automata */
1237 for (f
= a
->fsm
; f
; f
= f
->nxt
) /* control states */
1238 for (t
= f
->t
; t
; t
= t
->nxt
) /* transitions */
1240 switch (t
->step
->n
->ntyp
) {
1268 no_good
: if (banner
== 1 || banner
== 2)
1269 { printf("spin: proctype %s defines a %s process\n",
1271 banner
==1?"source":"sink");
1273 } else if (banner
== 3)
1274 { printf("spin: proctype %s mimics a buffer\n",
1280 { printf("\tto reduce complexity, consider merging the code of\n");
1281 printf("\teach source process into the code of its target\n");
1284 { printf("\tto reduce complexity, consider merging the code of\n");
1285 printf("\teach sink process into the code of its source\n");
1288 printf("\tto reduce complexity, avoid buffer processes\n");
1293 { Slicer
*sc
, *nx
, *rv
;
1295 for (sc
= slicer
; sc
; sc
= nx
)
1301 for (rv
= rel_vars
; rv
; rv
= rv
->nxt
)
1302 if (AST_mutual(sc
->n
, rv
->n
, 1))
1305 if (!rv
) /* not already there */
1306 { sc
->nxt
= rel_vars
;
1313 check_slice(Lextok
*n
, int code
)
1316 for (sc
= slicer
; sc
; sc
= sc
->nxt
)
1317 if (AST_mutual(sc
->n
, n
, 1)
1318 && sc
->code
== code
)
1319 return; /* already there */
1321 sc
= (Slicer
*) emalloc(sizeof(Slicer
));
1334 /* mark all def-relevant transitions */
1335 for (sc
= slicer
; sc
; sc
= sc
->nxt
)
1338 { printf("spin: slice criterion ");
1339 AST_var(sc
->n
, sc
->n
->sym
, 1);
1340 printf(" type=%d\n", Sym_typ(sc
->n
));
1342 AST_relevant(sc
->n
);
1344 AST_tagruns(); /* mark 'run's relevant if target proctype is relevant */
1348 AST_blockable(AST
*a
, int s
)
1354 for (t
= f
->t
; t
; t
= t
->nxt
)
1355 { if (t
->relevant
&2)
1358 if (t
->step
&& t
->step
->n
)
1359 switch (t
->step
->n
->ntyp
) {
1365 if (AST_blockable(a
, t
->to
))
1366 { t
->round
= AST_Round
;
1370 /* else fall through */
1374 else if (AST_blockable(a
, t
->to
)) /* Unless */
1375 { t
->round
= AST_Round
;
1384 AST_spread(AST
*a
, int s
)
1390 for (t
= f
->t
; t
; t
= t
->nxt
)
1391 { if (t
->relevant
&2)
1394 if (t
->step
&& t
->step
->n
)
1395 switch (t
->step
->n
->ntyp
) {
1401 AST_spread(a
, t
->to
);
1404 t
->round
= AST_Round
;
1409 { AST_spread(a
, t
->to
);
1410 t
->round
= AST_Round
;
1417 AST_notrelevant(Lextok
*n
)
1420 for (s
= rel_vars
; s
; s
= s
->nxt
)
1421 if (AST_mutual(s
->n
, n
, 1))
1423 for (s
= slicer
; s
; s
= s
->nxt
)
1424 if (AST_mutual(s
->n
, n
, 1))
1430 AST_withchan(Lextok
*n
)
1433 if (Sym_typ(n
) == CHAN
)
1435 return AST_withchan(n
->lft
) || AST_withchan(n
->rgt
);
1439 AST_suspect(FSM_trans
*t
)
1441 /* check for possible overkill */
1442 if (!t
|| !t
->step
|| !AST_withchan(t
->step
->n
))
1444 for (u
= t
->Val
[0]; u
; u
= u
->nxt
)
1445 if (AST_notrelevant(u
->n
))
1451 AST_shouldconsider(AST
*a
, int s
)
1456 for (t
= f
->t
; t
; t
= t
->nxt
)
1457 { if (t
->step
&& t
->step
->n
)
1458 switch (t
->step
->n
->ntyp
) {
1464 AST_shouldconsider(a
, t
->to
);
1467 AST_track(t
->step
->n
, 0);
1469 AST_track is called here for a blockable stmnt from which
1470 a relevant stmnmt was shown to be reachable
1471 for a condition this makes all USEs relevant
1472 but for a channel operation it only makes the executability
1473 relevant -- in those cases, parameters that aren't already
1474 relevant may be replaceable with arbitrary tokens
1477 { printf("spin: possibly redundant parameters in: ");
1478 comment(stdout
, t
->step
->n
, 0);
1483 else /* an Unless */
1484 AST_shouldconsider(a
, t
->to
);
1489 FSM_critical(AST
*a
, int s
)
1493 /* is a 1-relevant stmnt reachable from this state? */
1500 for (t
= f
->t
; t
; t
= t
->nxt
)
1502 || FSM_critical(a
, t
->to
))
1506 { printf("\t\t\t\tcritical(%d) ", t
->relevant
);
1507 comment(stdout
, t
->step
->n
, 0);
1515 { printf("\t\t\t\tnot-crit ");
1516 comment(stdout
, t
->step
->n
, 0);
1531 /* add all blockable transitions
1532 * from which relevant transitions can be reached
1535 printf("CTL -- %s\n", a
->p
->n
->name
);
1537 /* 1 : mark all blockable edges */
1538 for (f
= a
->fsm
; f
; f
= f
->nxt
)
1539 { if (!(f
->scratch
&2)) /* not part of irrelevant subgraph */
1540 for (t
= f
->t
; t
; t
= t
->nxt
)
1541 { if (t
->step
&& t
->step
->n
)
1542 switch (t
->step
->n
->ntyp
) {
1547 t
->round
= AST_Round
;
1548 t
->relevant
|= 2; /* mark for next phases */
1550 { printf("\tpremark ");
1551 comment(stdout
, t
->step
->n
, 0);
1559 /* 2: keep only 2-marked stmnts from which 1-marked stmnts can be reached */
1560 for (f
= a
->fsm
; f
; f
= f
->nxt
)
1561 { fsm_tbl
[f
->from
] = f
;
1562 f
->seen
= 0; /* used in dfs from FSM_critical */
1564 for (f
= a
->fsm
; f
; f
= f
->nxt
)
1565 { if (!FSM_critical(a
, f
->from
))
1566 for (t
= f
->t
; t
; t
= t
->nxt
)
1568 { t
->relevant
&= ~2; /* clear mark */
1570 { printf("\t\tnomark ");
1571 if (t
->step
&& t
->step
->n
)
1572 comment(stdout
, t
->step
->n
, 0);
1576 /* 3 : lift marks across IF/DO etc. */
1577 for (f
= a
->fsm
; f
; f
= f
->nxt
)
1579 for (t
= f
->t
; t
; t
= t
->nxt
)
1580 { if (t
->step
&& t
->step
->n
)
1581 switch (t
->step
->n
->ntyp
) {
1587 if (AST_blockable(a
, t
->to
))
1593 else if (AST_blockable(a
, t
->to
)) /* Unless */
1598 if (hit
) /* at least one outgoing trans can block */
1599 for (t
= f
->t
; t
; t
= t
->nxt
)
1600 { t
->round
= AST_Round
;
1601 t
->relevant
|= 2; /* lift */
1603 { printf("\t\t\tliftmark ");
1604 if (t
->step
&& t
->step
->n
)
1605 comment(stdout
, t
->step
->n
, 0);
1608 AST_spread(a
, t
->to
); /* and spread to all guards */
1611 /* 4: nodes with 2-marked out-edges contribute new slice criteria */
1612 for (f
= a
->fsm
; f
; f
= f
->nxt
)
1613 for (t
= f
->t
; t
; t
= t
->nxt
)
1615 { AST_shouldconsider(a
, f
->from
);
1616 break; /* inner loop */
1621 AST_control_dep(void)
1624 for (a
= ast
; a
; a
= a
->nxt
)
1625 if (strcmp(a
->p
->n
->name
, ":never:") != 0
1626 && strcmp(a
->p
->n
->name
, ":trace:") != 0
1627 && strcmp(a
->p
->n
->name
, ":notrace:") != 0)
1637 for (a
= ast
; a
; a
= a
->nxt
)
1638 { if (strcmp(a
->p
->n
->name
, ":never:") != 0
1639 && strcmp(a
->p
->n
->name
, ":trace:") != 0
1640 && strcmp(a
->p
->n
->name
, ":notrace:") != 0)
1641 for (f
= a
->fsm
; f
; f
= f
->nxt
)
1642 for (t
= f
->t
; t
; t
= t
->nxt
)
1645 && t
->step
->n
->ntyp
== ASSERT
1654 * remote labels are handled separately -- by making
1655 * sure they are not pruned away during optimization
1657 AST_Changes
= 1; /* to get started */
1658 for (AST_Round
= 1; slicer
&& AST_Changes
; AST_Round
++)
1661 AST_preserve(); /* moves processed vars from slicer to rel_vars */
1662 AST_dominant(); /* mark data-irrelevant subgraphs */
1663 AST_control_dep(); /* can add data deps, which add control deps */
1666 printf("\n\nROUND %d -- changes %d\n",
1667 AST_Round
, AST_Changes
);
1672 AST_alias_analysis(void) /* aliasing of promela channels */
1675 for (a
= ast
; a
; a
= a
->nxt
)
1676 AST_sends(a
); /* collect chan-names that are send across chans */
1678 for (a
= ast
; a
; a
= a
->nxt
)
1679 AST_para(a
->p
); /* aliasing of chans thru proctype parameters */
1681 for (a
= ast
; a
; a
= a
->nxt
)
1682 AST_other(a
); /* chan params in asgns and recvs */
1684 AST_trans(); /* transitive closure of alias table */
1687 AST_aliases(); /* show channel aliasing info */
1696 { non_fatal("no slice criteria (or no claim) specified",
1700 AST_dorelevant(); /* mark procs refered to in remote refs */
1702 for (a
= ast
; a
; a
= a
->nxt
)
1703 AST_def_use(a
); /* compute standard def/use information */
1705 AST_hidden(); /* parameter passing and local var inits */
1707 AST_alias_analysis(); /* channel alias analysis */
1709 AST_prelabel(); /* mark all 'assert(...)' stmnts as relevant */
1710 AST_criteria(); /* process the slice criteria from
1711 * asserts and from the never claim
1713 if (!spurious
|| (verbose
&32))
1715 for (a
= ast
; a
; a
= a
->nxt
)
1716 { AST_dump(a
); /* marked up result */
1717 if (a
->relevant
&2) /* it printed something */
1720 if (!AST_dump_rel() /* relevant variables */
1722 printf("spin: no redundancies found (for given property)\n");
1731 AST_store(ProcList
*p
, int start_state
)
1734 if (strcmp(p
->n
->name
, ":never:") != 0
1735 && strcmp(p
->n
->name
, ":trace:") != 0
1736 && strcmp(p
->n
->name
, ":notrace:") != 0)
1737 { n_ast
= (AST
*) emalloc(sizeof(AST
));
1739 n_ast
->i_st
= start_state
;
1740 n_ast
->relevant
= 0;
1745 fsm
= (FSM_state
*) 0; /* hide it from FSM_DEL */
1749 AST_add_explicit(Lextok
*d
, Lextok
*u
)
1750 { FSM_trans
*e
= (FSM_trans
*) emalloc(sizeof(FSM_trans
));
1752 e
->to
= 0; /* or start_state ? */
1753 e
->relevant
= 0; /* to be determined */
1754 e
->step
= (Element
*) 0; /* left blank */
1755 e
->Val
[0] = e
->Val
[1] = (FSM_use
*) 0;
1762 cur_t
= (FSM_trans
*) 0;
1769 AST_fp1(char *s
, Lextok
*t
, Lextok
*f
, int parno
)
1776 { if (strcmp(t
->sym
->name
, s
) == 0)
1777 for (v
= t
->lft
, cnt
= 1; v
; v
= v
->rgt
, cnt
++)
1779 { AST_add_explicit(f
, v
->lft
);
1783 { AST_fp1(s
, t
->lft
, f
, parno
);
1784 AST_fp1(s
, t
->rgt
, f
, parno
);
1789 AST_mk1(char *s
, Lextok
*c
, int parno
)
1794 /* concoct an extra FSM_trans *t with the asgn of
1795 * formal par c to matching actual pars made explicit
1798 for (a
= ast
; a
; a
= a
->nxt
) /* automata */
1799 for (f
= a
->fsm
; f
; f
= f
->nxt
) /* control states */
1800 for (t
= f
->t
; t
; t
= t
->nxt
) /* transitions */
1802 AST_fp1(s
, t
->step
->n
, c
, parno
);
1807 AST_par_init(void) /* parameter passing -- hidden assignments */
1812 for (a
= ast
; a
; a
= a
->nxt
)
1813 { if (strcmp(a
->p
->n
->name
, ":never:") == 0
1814 || strcmp(a
->p
->n
->name
, ":trace:") == 0
1815 || strcmp(a
->p
->n
->name
, ":notrace:") == 0
1816 || strcmp(a
->p
->n
->name
, ":init:") == 0)
1817 continue; /* have no params */
1820 for (f
= a
->p
->p
; f
; f
= f
->rgt
) /* types */
1821 for (t
= f
->lft
; t
; t
= t
->rgt
) /* formals */
1822 { cnt
++; /* formal par count */
1823 c
= (t
->ntyp
!= ',')? t
: t
->lft
; /* the formal parameter */
1824 AST_mk1(a
->p
->n
->name
, c
, cnt
); /* all matching run statements */
1829 AST_var_init(void) /* initialized vars (not chans) - hidden assignments */
1835 for (walk
= all_names
; walk
; walk
= walk
->next
)
1838 && !sp
->context
/* globals */
1839 && sp
->type
!= PROCTYPE
1841 && (sp
->type
!= MTYPE
|| sp
->ini
->ntyp
!= CONST
) /* not mtype defs */
1842 && sp
->ini
->ntyp
!= CHAN
)
1843 { x
= nn(ZN
, TYPE
, ZN
, ZN
);
1845 AST_add_explicit(x
, sp
->ini
);
1848 for (a
= ast
; a
; a
= a
->nxt
)
1849 { if (strcmp(a
->p
->n
->name
, ":never:") != 0
1850 && strcmp(a
->p
->n
->name
, ":trace:") != 0
1851 && strcmp(a
->p
->n
->name
, ":notrace:") != 0) /* claim has no locals */
1852 for (walk
= all_names
; walk
; walk
= walk
->next
)
1856 && strcmp(sp
->context
->name
, a
->p
->n
->name
) == 0
1857 && sp
->Nid
>= 0 /* not a param */
1858 && sp
->type
!= LABEL
1860 && sp
->ini
->ntyp
!= CHAN
)
1861 { x
= nn(ZN
, TYPE
, ZN
, ZN
);
1863 AST_add_explicit(x
, sp
->ini
);
1872 printf("\nExplicit List:\n");
1873 for (T
= expl_par
; T
; T
= (T
== expl_par
)?expl_var
: (FSM_trans
*) 0)
1874 { for (t
= T
; t
; t
= t
->nxt
)
1875 { if (!t
->Val
[0]) continue;
1876 printf("%s", t
->relevant
?"*":" ");
1877 printf("%3d", t
->round
);
1878 for (u
= t
->Val
[0]; u
; u
= u
->nxt
)
1880 AST_var(u
->n
, u
->n
->sym
, 1);
1881 printf(":%d>, ", u
->special
);
1891 AST_hidden(void) /* reveal all hidden assignments */
1894 expl_par
= explicit;
1895 explicit = (FSM_trans
*) 0;
1898 expl_var
= explicit;
1899 explicit = (FSM_trans
*) 0;
1902 #define BPW (8*sizeof(ulong)) /* bits per word */
1905 bad_scratch(FSM_state
*f
, int upto
)
1908 1. all internal branch
-points have
else-s
1909 2. all non
-branchpoints have non
-blocking out
-edge
1910 3. all internal edges are non
-relevant
1911 subgraphs like
this need NOT contribute control
-dependencies
1923 if (verbose
&32) printf("X[%d:%d:%d] ", f
->from
, upto
, f
->scratch
);
1927 printf("\tbad scratch: %d\n", f
->from
);
1928 bad
: f
->scratch
&= ~4;
1929 /* f->scratch |= 8; wrong */
1933 if (f
->from
!= upto
)
1934 for (t
= f
->t
; t
; t
= t
->nxt
)
1935 if (bad_scratch(fsm_tbl
[t
->to
], upto
))
1942 mark_subgraph(FSM_state
*f
, int upto
)
1952 for (t
= f
->t
; t
; t
= t
->nxt
)
1953 mark_subgraph(fsm_tbl
[t
->to
], upto
);
1957 AST_pair(AST
*a
, FSM_state
*h
, int y
)
1960 for (p
= a
->pairs
; p
; p
= p
->nxt
)
1965 p
= (Pair
*) emalloc(sizeof(Pair
));
1973 AST_checkpairs(AST
*a
)
1976 for (p
= a
->pairs
; p
; p
= p
->nxt
)
1978 printf(" inspect pair %d %d\n", p
->b
, p
->h
->from
);
1979 if (!bad_scratch(p
->h
, p
->b
)) /* subgraph is clean */
1981 printf("subgraph: %d .. %d\n", p
->b
, p
->h
->from
);
1982 mark_subgraph(p
->h
, p
->b
);
1988 subgraph(AST
*a
, FSM_state
*f
, int out
)
1993 reverse dominance suggests that
this is a possible
1994 entry
and exit node
for a proper subgraph
2003 printf("possible pair %d %d -- %d\n",
2004 f
->from
, h
->from
, (g
[i
]&(1<<j
))?1:0);
2006 if (g
[i
]&(1<<j
)) /* also a forward dominance pair */
2007 AST_pair(a
, h
, f
->from
); /* record this pair */
2016 for (f
= a
->fsm
; f
; f
= f
->nxt
)
2017 { if (!f
->seen
) continue;
2019 f
->from is the exit
-node of a proper subgraph
, with
2020 the dominator its entry
-node
, if:
2021 a
. this node has more than
1 reachable predecessor
2022 b
. the dominator has more than
1 reachable successor
2023 (need reachability
- in
case of reverse dominance
)
2024 d
. the dominator is reachable
, and not equal to
this node
2026 for (t
= f
->p
, i
= 0; t
; t
= t
->nxt
)
2027 i
+= fsm_tbl
[t
->to
]->seen
;
2028 if (i
<= 1) continue; /* a. */
2030 for (cnt
= 1; cnt
< a
->nstates
; cnt
++) /* 0 is endstate */
2031 { if (cnt
== f
->from
2032 || !fsm_tbl
[cnt
]->seen
)
2037 if (!(f
->dom
[i
]&(1<<j
)))
2040 for (t
= fsm_tbl
[cnt
]->t
, i
= 0; t
; t
= t
->nxt
)
2041 i
+= fsm_tbl
[t
->to
]->seen
;
2045 if (f
->mod
) /* final check in 2nd phase */
2046 subgraph(a
, f
, cnt
); /* possible entry-exit pair */
2052 reachability(AST
*a
)
2055 for (f
= a
->fsm
; f
; f
= f
->nxt
)
2056 f
->seen
= 0; /* clear */
2057 AST_dfs(a
, a
->i_st
, 0); /* mark 'seen' */
2061 see_else(FSM_state
*f
)
2064 for (t
= f
->t
; t
; t
= t
->nxt
)
2067 switch (t
->step
->n
->ntyp
) {
2075 if (see_else(fsm_tbl
[t
->to
]))
2085 is_guard(FSM_state
*f
)
2089 for (t
= f
->p
; t
; t
= t
->nxt
)
2090 { g
= fsm_tbl
[t
->to
];
2096 switch(t
->step
->n
->ntyp
) {
2116 int i
, haselse
, isrel
, blocking
;
2118 mark nodes that
do not satisfy these requirements
:
2119 1. all internal branch
-points have
else-s
2120 2. all non
-branchpoints have non
-blocking out
-edge
2121 3. all internal edges are non
-data
-relevant
2124 printf("Curtail %s:\n", a
->p
->n
->name
);
2126 for (f
= a
->fsm
; f
; f
= f
->nxt
)
2128 || (f
->scratch
&(1|2)))
2131 isrel
= haselse
= i
= blocking
= 0;
2133 for (t
= f
->t
; t
; t
= t
->nxt
)
2134 { g
= fsm_tbl
[t
->to
];
2136 isrel
|= (t
->relevant
&1); /* data relevant */
2141 { switch (t
->step
->n
->ntyp
) {
2144 haselse
|= see_else(g
);
2154 printf("prescratch %d -- %d %d %d %d -- %d\n",
2155 f
->from
, i
, isrel
, blocking
, haselse
, is_guard(f
));
2158 || (i
== 1 && blocking
) /* 2. */
2159 || (i
> 1 && !haselse
)) /* 1. */
2163 printf("scratch %d -- %d %d %d %d\n",
2164 f
->from
, i
, isrel
, blocking
, haselse
);
2176 (2) for s in S
- {s0
} do D(s
) = S
2179 for (f
= a
->fsm
; f
; f
= f
->nxt
)
2180 { if (!f
->seen
) continue;
2183 emalloc(a
->nwords
* sizeof(ulong
));
2185 if (f
->from
== a
->i_st
)
2186 { i
= a
->i_st
/ BPW
;
2188 f
->dom
[i
] = (1<<j
); /* (1) */
2190 { for (i
= 0; i
< a
->nwords
; i
++)
2191 f
->dom
[i
] = (ulong
) ~0; /* all 1's */
2193 if (a
->nstates
% BPW
)
2194 for (i
= (a
->nstates
% BPW
); i
< (int) BPW
; i
++)
2195 f
->dom
[a
->nwords
-1] &= ~(1<<i
); /* clear tail */
2197 for (cnt
= 0; cnt
< a
->nstates
; cnt
++)
2198 if (!fsm_tbl
[cnt
]->seen
)
2201 f
->dom
[i
] &= ~(1<<j
);
2206 dom_perculate(AST
*a
, FSM_state
*f
)
2207 { static ulong
*ndom
= (ulong
*) 0;
2216 emalloc(on
* sizeof(ulong
));
2219 for (i
= 0; i
< a
->nwords
; i
++)
2220 ndom
[i
] = (ulong
) ~0;
2222 for (t
= f
->p
; t
; t
= t
->nxt
) /* all reachable predecessors */
2223 { g
= fsm_tbl
[t
->to
];
2225 for (i
= 0; i
< a
->nwords
; i
++)
2226 ndom
[i
] &= g
->dom
[i
]; /* (5b) */
2231 ndom
[i
] |= (1<<j
); /* (5a) */
2233 for (i
= 0; i
< a
->nwords
; i
++)
2234 if (f
->dom
[i
] != ndom
[i
])
2236 f
->dom
[i
] = ndom
[i
];
2247 init_dom(a
); /* (1,2) */
2250 for (f
= a
->fsm
; f
; f
= f
->nxt
)
2252 && f
->from
!= a
->i_st
) /* (4) */
2253 cnt
+= dom_perculate(a
, f
); /* (5) */
2255 } while (cnt
); /* (3) */
2256 dom_perculate(a
, fsm_tbl
[a
->i_st
]);
2265 static FSM_state no_state
;
2268 Aho
, Sethi
, & Ullman
, Compilers
- principles
, techniques
, and tools
2269 Addison
-Wesley
, 1986, p
.671.
2272 (2) for s in S
- {s0
} do D(s
) = S
2274 (3) while any
D(s
) changes
do
2275 (4) for s in S
- {s0
} do
2276 (5) D(s
) = {s
} union with intersection of all
D(p
)
2277 where p are the immediate predecessors of s
2279 the purpose is to find proper subgraphs
2280 (one entry node
, one exit node
)
2282 if (AST_Round
== 1) /* computed once, reused in every round */
2283 for (a
= ast
; a
; a
= a
->nxt
)
2285 for (f
= a
->fsm
; f
; f
= f
->nxt
)
2286 { a
->nstates
++; /* count */
2287 fsm_tbl
[f
->from
] = f
; /* fast lookup */
2288 f
->scratch
= 0; /* clear scratch marks */
2290 for (oi
= 0; oi
< a
->nstates
; oi
++)
2292 fsm_tbl
[oi
] = &no_state
;
2294 a
->nwords
= (a
->nstates
+ BPW
- 1) / BPW
; /* round up */
2297 { printf("%s (%d): ", a
->p
->n
->name
, a
->i_st
);
2298 printf("states=%d (max %d), words = %d, bpw %d, overflow %d\n",
2299 a
->nstates
, o_max
, a
->nwords
,
2300 (int) BPW
, (int) (a
->nstates
% BPW
));
2304 dom_forward(a
); /* forward dominance relation */
2306 curtail(a
); /* mark ineligible edges */
2307 for (f
= a
->fsm
; f
; f
= f
->nxt
)
2310 f
->t
= t
; /* invert edges */
2313 f
->dom
= (ulong
*) 0;
2316 if (fsm_tbl
[0]->seen
) /* end-state reachable - else leave it */
2317 a
->i_st
= 0; /* becomes initial state */
2319 dom_forward(a
); /* reverse dominance -- don't redo reachability! */
2320 act_dom(a
); /* mark proper subgraphs, if any */
2321 AST_checkpairs(a
); /* selectively place 2 scratch-marks */
2323 for (f
= a
->fsm
; f
; f
= f
->nxt
)
2326 f
->t
= t
; /* restore */
2328 a
->i_st
= oi
; /* restore */
2330 for (a
= ast
; a
; a
= a
->nxt
)
2331 { for (f
= a
->fsm
; f
; f
= f
->nxt
)
2332 { fsm_tbl
[f
->from
] = f
;
2333 f
->scratch
&= 1; /* preserve 1-marks */
2335 for (oi
= 0; oi
< a
->nstates
; oi
++)
2337 fsm_tbl
[oi
] = &no_state
;
2339 curtail(a
); /* mark ineligible edges */
2341 for (f
= a
->fsm
; f
; f
= f
->nxt
)
2344 f
->t
= t
; /* invert edges */
2347 AST_checkpairs(a
); /* recompute 2-marks */
2349 for (f
= a
->fsm
; f
; f
= f
->nxt
)
2352 f
->t
= t
; /* restore */