ref: d1cebf608b05e45b148108ac6c16ae94f6862097
dir: /sys/src/cmd/spin/pangen6.c/
/***** spin: pangen6.c *****/ /* * This file is part of the public release of Spin. It is subject to the * terms in the LICENSE file that is included in this source directory. * Tool documentation is available at http://spinroot.com */ #include "spin.h" #include "y.tab.h" extern Ordered *all_names; extern FSM_use *use_free; extern FSM_state **fsm_tbl; extern FSM_state *fsm; extern int verbose, o_max; static FSM_trans *cur_t; static FSM_trans *expl_par; static FSM_trans *expl_var; static FSM_trans *explicit; extern void rel_use(FSM_use *); #define ulong unsigned long typedef struct Pair { FSM_state *h; int b; struct Pair *nxt; } Pair; typedef struct AST { ProcList *p; /* proctype decl */ int i_st; /* start state */ int nstates, nwords; int relevant; Pair *pairs; /* entry and exit nodes of proper subgraphs */ FSM_state *fsm; /* proctype body */ struct AST *nxt; /* linked list */ } AST; typedef struct RPN { /* relevant proctype names */ Symbol *rn; struct RPN *nxt; } RPN; typedef struct ALIAS { /* channel aliasing info */ Lextok *cnm; /* this chan */ int origin; /* debugging - origin of the alias */ struct ALIAS *alias; /* can be an alias for these other chans */ struct ALIAS *nxt; /* linked list */ } ALIAS; typedef struct ChanList { Lextok *s; /* containing stmnt */ Lextok *n; /* point of reference - could be struct */ struct ChanList *nxt; /* linked list */ } ChanList; /* a chan alias can be created in one of three ways: assignement to chan name a = b -- a is now an alias for b passing chan name as parameter in run run x(b) -- proctype x(chan a) passing chan name through channel x!b -- x?a */ #define USE 1 #define DEF 2 #define DEREF_DEF 4 #define DEREF_USE 8 static AST *ast; static ALIAS *chalcur; static ALIAS *chalias; static ChanList *chanlist; static Slicer *slicer; static Slicer *rel_vars; /* all relevant variables */ static int AST_Changes; static int AST_Round; static RPN *rpn; static int in_recv = 0; static int AST_mutual(Lextok *, Lextok *, int); static void AST_dominant(void); static void AST_hidden(void); static void AST_setcur(Lextok *); static void check_slice(Lextok *, int); static void curtail(AST *); static void def_use(Lextok *, int); static void name_AST_track(Lextok *, int); static void show_expl(void); static int AST_isini(Lextok *n) /* is this an initialized channel */ { Symbol *s; if (!n || !n->sym) return 0; s = n->sym; if (s->type == CHAN) return (s->ini->ntyp == CHAN); /* freshly instantiated */ if (s->type == STRUCT && n->rgt) return AST_isini(n->rgt->lft); return 0; } static void AST_var(Lextok *n, Symbol *s, int toplevel) { if (!s) return; if (toplevel) { if (s->context && s->type) printf(":%s:L:", s->context->name); else printf("G:"); } printf("%s", s->name); /* array indices ignored */ if (s->type == STRUCT && n && n->rgt && n->rgt->lft) { printf(":"); AST_var(n->rgt->lft, n->rgt->lft->sym, 0); } } static void name_def_indices(Lextok *n, int code) { if (!n || !n->sym) return; if (n->sym->nel > 1 || n->sym->isarray) def_use(n->lft, code); /* process the index */ if (n->sym->type == STRUCT /* and possible deeper ones */ && n->rgt) name_def_indices(n->rgt->lft, code); } static void name_def_use(Lextok *n, int code) { FSM_use *u; if (!n) return; if ((code&USE) && cur_t->step && cur_t->step->n) { switch (cur_t->step->n->ntyp) { case 'c': /* possible predicate abstraction? */ n->sym->colnr |= 2; /* yes */ break; default: n->sym->colnr |= 1; /* no */ break; } } for (u = cur_t->Val[0]; u; u = u->nxt) if (AST_mutual(n, u->n, 1) && u->special == code) return; if (use_free) { u = use_free; use_free = use_free->nxt; } else u = (FSM_use *) emalloc(sizeof(FSM_use)); u->n = n; u->special = code; u->nxt = cur_t->Val[0]; cur_t->Val[0] = u; name_def_indices(n, USE|(code&(~DEF))); /* not def, but perhaps deref */ } static void def_use(Lextok *now, int code) { Lextok *v; if (now) switch (now->ntyp) { case '!': case UMIN: case '~': case 'c': case ENABLED: case SET_P: case GET_P: case ASSERT: case EVAL: def_use(now->lft, USE|code); break; case LEN: case FULL: case EMPTY: case NFULL: case NEMPTY: def_use(now->lft, DEREF_USE|USE|code); break; case '/': case '*': case '-': case '+': case '%': case '&': case '^': case '|': case LE: case GE: case GT: case LT: case NE: case EQ: case OR: case AND: case LSHIFT: case RSHIFT: def_use(now->lft, USE|code); def_use(now->rgt, USE|code); break; case ASGN: def_use(now->lft, DEF|code); def_use(now->rgt, USE|code); break; case TYPE: /* name in parameter list */ name_def_use(now, code); break; case NAME: name_def_use(now, code); break; case RUN: name_def_use(now, USE); /* procname - not really needed */ for (v = now->lft; v; v = v->rgt) def_use(v->lft, USE); /* params */ break; case 's': def_use(now->lft, DEREF_DEF|DEREF_USE|USE|code); for (v = now->rgt; v; v = v->rgt) def_use(v->lft, USE|code); break; case 'r': def_use(now->lft, DEREF_DEF|DEREF_USE|USE|code); for (v = now->rgt; v; v = v->rgt) { if (v->lft->ntyp == EVAL) def_use(v->lft, code); /* will add USE */ else if (v->lft->ntyp != CONST) def_use(v->lft, DEF|code); } break; case 'R': def_use(now->lft, DEREF_USE|USE|code); for (v = now->rgt; v; v = v->rgt) { if (v->lft->ntyp == EVAL) def_use(v->lft, code); /* will add USE */ } break; case '?': def_use(now->lft, USE|code); if (now->rgt) { def_use(now->rgt->lft, code); def_use(now->rgt->rgt, code); } break; case PRINT: for (v = now->lft; v; v = v->rgt) def_use(v->lft, USE|code); break; case PRINTM: def_use(now->lft, USE); break; case CONST: case ELSE: /* ? */ case NONPROGRESS: case PC_VAL: case 'p': case 'q': break; case '.': case GOTO: case BREAK: case '@': case D_STEP: case ATOMIC: case NON_ATOMIC: case IF: case DO: case UNLESS: case TIMEOUT: case C_CODE: case C_EXPR: default: break; } } static int AST_add_alias(Lextok *n, int nr) { ALIAS *ca; int res; for (ca = chalcur->alias; ca; ca = ca->nxt) if (AST_mutual(ca->cnm, n, 1)) { res = (ca->origin&nr); ca->origin |= nr; /* 1, 2, or 4 - run, asgn, or rcv */ return (res == 0); /* 0 if already there with same origin */ } ca = (ALIAS *) emalloc(sizeof(ALIAS)); ca->cnm = n; ca->origin = nr; ca->nxt = chalcur->alias; chalcur->alias = ca; return 1; } static void AST_run_alias(char *pn, char *s, Lextok *t, int parno) { Lextok *v; int cnt; if (!t) return; if (t->ntyp == RUN) { if (strcmp(t->sym->name, s) == 0) for (v = t->lft, cnt = 1; v; v = v->rgt, cnt++) if (cnt == parno) { AST_add_alias(v->lft, 1); /* RUN */ break; } } else { AST_run_alias(pn, s, t->lft, parno); AST_run_alias(pn, s, t->rgt, parno); } } static void AST_findrun(char *s, int parno) { FSM_state *f; FSM_trans *t; AST *a; for (a = ast; a; a = a->nxt) /* automata */ for (f = a->fsm; f; f = f->nxt) /* control states */ for (t = f->t; t; t = t->nxt) /* transitions */ { if (t->step) AST_run_alias(a->p->n->name, s, t->step->n, parno); } } static void AST_par_chans(ProcList *p) /* find local chan's init'd to chan passed as param */ { Ordered *walk; Symbol *sp; for (walk = all_names; walk; walk = walk->next) { sp = walk->entry; if (sp && sp->context && strcmp(sp->context->name, p->n->name) == 0 && sp->Nid >= 0 /* not itself a param */ && sp->type == CHAN && sp->ini->ntyp == NAME) /* != CONST and != CHAN */ { Lextok *x = nn(ZN, 0, ZN, ZN); x->sym = sp; AST_setcur(x); AST_add_alias(sp->ini, 2); /* ASGN */ } } } static void AST_para(ProcList *p) { Lextok *f, *t, *c; int cnt = 0; AST_par_chans(p); for (f = p->p; f; f = f->rgt) /* list of types */ for (t = f->lft; t; t = t->rgt) { if (t->ntyp != ',') c = t; else c = t->lft; /* expanded struct */ cnt++; if (Sym_typ(c) == CHAN) { ALIAS *na = (ALIAS *) emalloc(sizeof(ALIAS)); na->cnm = c; na->nxt = chalias; chalcur = chalias = na; #if 0 printf("%s -- (par) -- ", p->n->name); AST_var(c, c->sym, 1); printf(" => <<"); #endif AST_findrun(p->n->name, cnt); #if 0 printf(">>\n"); #endif } } } static void AST_haschan(Lextok *c) { if (!c) return; if (Sym_typ(c) == CHAN) { AST_add_alias(c, 2); /* ASGN */ #if 0 printf("<<"); AST_var(c, c->sym, 1); printf(">>\n"); #endif } else { AST_haschan(c->rgt); AST_haschan(c->lft); } } static int AST_nrpar(Lextok *n) /* 's' or 'r' */ { Lextok *m; int j = 0; for (m = n->rgt; m; m = m->rgt) j++; return j; } static int AST_ord(Lextok *n, Lextok *s) { Lextok *m; int j = 0; for (m = n->rgt; m; m = m->rgt) { j++; if (s->sym == m->lft->sym) return j; } return 0; } #if 0 static void AST_ownership(Symbol *s) { if (!s) return; printf("%s:", s->name); AST_ownership(s->owner); } #endif static int AST_mutual(Lextok *a, Lextok *b, int toplevel) { Symbol *as, *bs; if (!a && !b) return 1; if (!a || !b) return 0; as = a->sym; bs = b->sym; if (!as || !bs) return 0; if (toplevel && as->context != bs->context) return 0; if (as->type != bs->type) return 0; if (strcmp(as->name, bs->name) != 0) return 0; if (as->type == STRUCT && a->rgt && b->rgt) /* we know that a and b are not null */ return AST_mutual(a->rgt->lft, b->rgt->lft, 0); return 1; } static void AST_setcur(Lextok *n) /* set chalcur */ { ALIAS *ca; for (ca = chalias; ca; ca = ca->nxt) if (AST_mutual(ca->cnm, n, 1)) /* if same chan */ { chalcur = ca; return; } ca = (ALIAS *) emalloc(sizeof(ALIAS)); ca->cnm = n; ca->nxt = chalias; chalcur = chalias = ca; } static void AST_other(AST *a) /* check chan params in asgns and recvs */ { FSM_state *f; FSM_trans *t; FSM_use *u; ChanList *cl; for (f = a->fsm; f; f = f->nxt) /* control states */ for (t = f->t; t; t = t->nxt) /* transitions */ for (u = t->Val[0]; u; u = u->nxt) /* def/use info */ if (Sym_typ(u->n) == CHAN && (u->special&DEF)) /* def of chan-name */ { AST_setcur(u->n); switch (t->step->n->ntyp) { case ASGN: AST_haschan(t->step->n->rgt); break; case 'r': /* guess sends where name may originate */ for (cl = chanlist; cl; cl = cl->nxt) /* all sends */ { int aa = AST_nrpar(cl->s); int bb = AST_nrpar(t->step->n); if (aa != bb) /* matching nrs of params */ continue; aa = AST_ord(cl->s, cl->n); bb = AST_ord(t->step->n, u->n); if (aa != bb) /* same position in parlist */ continue; AST_add_alias(cl->n, 4); /* RCV assume possible match */ } break; default: printf("type = %d\n", t->step->n->ntyp); non_fatal("unexpected chan def type", (char *) 0); break; } } } static void AST_aliases(void) { ALIAS *na, *ca; for (na = chalias; na; na = na->nxt) { printf("\npossible aliases of "); AST_var(na->cnm, na->cnm->sym, 1); printf("\n\t"); for (ca = na->alias; ca; ca = ca->nxt) { if (!ca->cnm->sym) printf("no valid name "); else AST_var(ca->cnm, ca->cnm->sym, 1); printf("<"); if (ca->origin & 1) printf("RUN "); if (ca->origin & 2) printf("ASGN "); if (ca->origin & 4) printf("RCV "); printf("[%s]", AST_isini(ca->cnm)?"Initzd":"Name"); printf(">"); if (ca->nxt) printf(", "); } printf("\n"); } printf("\n"); } static void AST_indirect(FSM_use *uin, FSM_trans *t, char *cause, char *pn) { FSM_use *u; /* this is a newly discovered relevant statement */ /* all vars it uses to contribute to its DEF are new criteria */ if (!(t->relevant&1)) AST_Changes++; t->round = AST_Round; t->relevant = 1; if ((verbose&32) && t->step) { printf("\tDR %s [[ ", pn); comment(stdout, t->step->n, 0); printf("]]\n\t\tfully relevant %s", cause); if (uin) { printf(" due to "); AST_var(uin->n, uin->n->sym, 1); } printf("\n"); } for (u = t->Val[0]; u; u = u->nxt) if (u != uin && (u->special&(USE|DEREF_USE))) { if (verbose&32) { printf("\t\t\tuses(%d): ", u->special); AST_var(u->n, u->n->sym, 1); printf("\n"); } name_AST_track(u->n, u->special); /* add to slice criteria */ } } static void def_relevant(char *pn, FSM_trans *t, Lextok *n, int ischan) { FSM_use *u; ALIAS *na, *ca; int chanref; /* look for all DEF's of n * mark those stmnts relevant * mark all var USEs in those stmnts as criteria */ if (n->ntyp != ELSE) for (u = t->Val[0]; u; u = u->nxt) { chanref = (Sym_typ(u->n) == CHAN); if (ischan != chanref /* no possible match */ || !(u->special&(DEF|DEREF_DEF))) /* not a def */ continue; if (AST_mutual(u->n, n, 1)) { AST_indirect(u, t, "(exact match)", pn); continue; } if (chanref) for (na = chalias; na; na = na->nxt) { if (!AST_mutual(u->n, na->cnm, 1)) continue; for (ca = na->alias; ca; ca = ca->nxt) if (AST_mutual(ca->cnm, n, 1) && AST_isini(ca->cnm)) { AST_indirect(u, t, "(alias match)", pn); break; } if (ca) break; } } } static void AST_relevant(Lextok *n) { AST *a; FSM_state *f; FSM_trans *t; int ischan; /* look for all DEF's of n * mark those stmnts relevant * mark all var USEs in those stmnts as criteria */ if (!n) return; ischan = (Sym_typ(n) == CHAN); if (verbose&32) { printf("<<ast_relevant (ntyp=%d) ", n->ntyp); AST_var(n, n->sym, 1); printf(">>\n"); } for (t = expl_par; t; t = t->nxt) /* param assignments */ { if (!(t->relevant&1)) def_relevant(":params:", t, n, ischan); } for (t = expl_var; t; t = t->nxt) { if (!(t->relevant&1)) /* var inits */ def_relevant(":vars:", t, n, ischan); } for (a = ast; a; a = a->nxt) /* all other stmnts */ { if (a->p->b != N_CLAIM && a->p->b != E_TRACE && a->p->b != N_TRACE) for (f = a->fsm; f; f = f->nxt) for (t = f->t; t; t = t->nxt) { if (!(t->relevant&1)) def_relevant(a->p->n->name, t, n, ischan); } } } static int AST_relpar(char *s) { FSM_trans *t, *T; FSM_use *u; for (T = expl_par; T; T = (T == expl_par)?expl_var: (FSM_trans *) 0) for (t = T; t; t = t->nxt) { if (t->relevant&1) for (u = t->Val[0]; u; u = u->nxt) { if (u->n->sym->type && u->n->sym->context && strcmp(u->n->sym->context->name, s) == 0) { if (verbose&32) { printf("proctype %s relevant, due to symbol ", s); AST_var(u->n, u->n->sym, 1); printf("\n"); } return 1; } } } return 0; } static void AST_dorelevant(void) { AST *a; RPN *r; for (r = rpn; r; r = r->nxt) { for (a = ast; a; a = a->nxt) if (strcmp(a->p->n->name, r->rn->name) == 0) { a->relevant |= 1; break; } if (!a) fatal("cannot find proctype %s", r->rn->name); } } static void AST_procisrelevant(Symbol *s) { RPN *r; for (r = rpn; r; r = r->nxt) if (strcmp(r->rn->name, s->name) == 0) return; r = (RPN *) emalloc(sizeof(RPN)); r->rn = s; r->nxt = rpn; rpn = r; } static int AST_proc_isrel(char *s) { AST *a; for (a = ast; a; a = a->nxt) if (strcmp(a->p->n->name, s) == 0) return (a->relevant&1); non_fatal("cannot happen, missing proc in ast", (char *) 0); return 0; } static int AST_scoutrun(Lextok *t) { if (!t) return 0; if (t->ntyp == RUN) return AST_proc_isrel(t->sym->name); return (AST_scoutrun(t->lft) || AST_scoutrun(t->rgt)); } static void AST_tagruns(void) { AST *a; FSM_state *f; FSM_trans *t; /* if any stmnt inside a proctype is relevant * or any parameter passed in a run * then so are all the run statements on that proctype */ for (a = ast; a; a = a->nxt) { if (a->p->b == N_CLAIM || a->p->b == I_PROC || a->p->b == E_TRACE || a->p->b == N_TRACE) { a->relevant |= 1; /* the proctype is relevant */ continue; } if (AST_relpar(a->p->n->name)) a->relevant |= 1; else { for (f = a->fsm; f; f = f->nxt) for (t = f->t; t; t = t->nxt) if (t->relevant) goto yes; yes: if (f) a->relevant |= 1; } } for (a = ast; a; a = a->nxt) for (f = a->fsm; f; f = f->nxt) for (t = f->t; t; t = t->nxt) if (t->step && AST_scoutrun(t->step->n)) { AST_indirect((FSM_use *)0, t, ":run:", a->p->n->name); /* BUT, not all actual params are relevant */ } } static void AST_report(AST *a, Element *e) /* ALSO deduce irrelevant vars */ { if (!(a->relevant&2)) { a->relevant |= 2; printf("spin: redundant in proctype %s (for given property):\n", a->p->n->name); } printf(" %s:%d (state %d)", e->n?e->n->fn->name:"-", e->n?e->n->ln:-1, e->seqno); printf(" ["); comment(stdout, e->n, 0); printf("]\n"); } static int AST_always(Lextok *n) { if (!n) return 0; if (n->ntyp == '@' /* -end */ || n->ntyp == 'p') /* remote reference */ return 1; return AST_always(n->lft) || AST_always(n->rgt); } static void AST_edge_dump(AST *a, FSM_state *f) { FSM_trans *t; FSM_use *u; for (t = f->t; t; t = t->nxt) /* edges */ { if (t->step && AST_always(t->step->n)) t->relevant |= 1; /* always relevant */ if (verbose&32) { switch (t->relevant) { case 0: printf(" "); break; case 1: printf("*%3d ", t->round); break; case 2: printf("+%3d ", t->round); break; case 3: printf("#%3d ", t->round); break; default: printf("? "); break; } printf("%d\t->\t%d\t", f->from, t->to); if (t->step) comment(stdout, t->step->n, 0); else printf("Unless"); for (u = t->Val[0]; u; u = u->nxt) { printf(" <"); AST_var(u->n, u->n->sym, 1); printf(":%d>", u->special); } printf("\n"); } else { if (t->relevant) continue; if (t->step) switch(t->step->n->ntyp) { case ASGN: case 's': case 'r': case 'c': if (t->step->n->lft->ntyp != CONST) AST_report(a, t->step); break; case PRINT: /* don't report */ case PRINTM: case ASSERT: case C_CODE: case C_EXPR: default: break; } } } } static void AST_dfs(AST *a, int s, int vis) { FSM_state *f; FSM_trans *t; f = fsm_tbl[s]; if (f->seen) return; f->seen = 1; if (vis) AST_edge_dump(a, f); for (t = f->t; t; t = t->nxt) AST_dfs(a, t->to, vis); } static void AST_dump(AST *a) { FSM_state *f; for (f = a->fsm; f; f = f->nxt) { f->seen = 0; fsm_tbl[f->from] = f; } if (verbose&32) printf("AST_START %s from %d\n", a->p->n->name, a->i_st); AST_dfs(a, a->i_st, 1); } static void AST_sends(AST *a) { FSM_state *f; FSM_trans *t; FSM_use *u; ChanList *cl; for (f = a->fsm; f; f = f->nxt) /* control states */ for (t = f->t; t; t = t->nxt) /* transitions */ { if (t->step && t->step->n && t->step->n->ntyp == 's') for (u = t->Val[0]; u; u = u->nxt) { if (Sym_typ(u->n) == CHAN && ((u->special&USE) && !(u->special&DEREF_USE))) { #if 0 printf("%s -- (%d->%d) -- ", a->p->n->name, f->from, t->to); AST_var(u->n, u->n->sym, 1); printf(" -> chanlist\n"); #endif cl = (ChanList *) emalloc(sizeof(ChanList)); cl->s = t->step->n; cl->n = u->n; cl->nxt = chanlist; chanlist = cl; } } } } static ALIAS * AST_alfind(Lextok *n) { ALIAS *na; for (na = chalias; na; na = na->nxt) if (AST_mutual(na->cnm, n, 1)) return na; return (ALIAS *) 0; } static void AST_trans(void) { ALIAS *na, *ca, *da, *ea; int nchanges; do { nchanges = 0; for (na = chalias; na; na = na->nxt) { chalcur = na; for (ca = na->alias; ca; ca = ca->nxt) { da = AST_alfind(ca->cnm); if (da) for (ea = da->alias; ea; ea = ea->nxt) { nchanges += AST_add_alias(ea->cnm, ea->origin|ca->origin); } } } } while (nchanges > 0); chalcur = (ALIAS *) 0; } static void AST_def_use(AST *a) { FSM_state *f; FSM_trans *t; for (f = a->fsm; f; f = f->nxt) /* control states */ for (t = f->t; t; t = t->nxt) /* all edges */ { cur_t = t; rel_use(t->Val[0]); /* redo Val; doesn't cover structs */ rel_use(t->Val[1]); t->Val[0] = t->Val[1] = (FSM_use *) 0; if (!t->step) continue; def_use(t->step->n, 0); /* def/use info, including structs */ } cur_t = (FSM_trans *) 0; } static void name_AST_track(Lextok *n, int code) { extern int nr_errs; #if 0 printf("AST_name: "); AST_var(n, n->sym, 1); printf(" -- %d\n", code); #endif if (in_recv && (code&DEF) && (code&USE)) { printf("spin: %s:%d, error: DEF and USE of same var in rcv stmnt: ", n->fn->name, n->ln); AST_var(n, n->sym, 1); printf(" -- %d\n", code); nr_errs++; } check_slice(n, code); } void AST_track(Lextok *now, int code) /* called from main.c */ { Lextok *v; extern int export_ast; if (!export_ast) return; if (now) switch (now->ntyp) { case LEN: case FULL: case EMPTY: case NFULL: case NEMPTY: AST_track(now->lft, DEREF_USE|USE|code); break; case '/': case '*': case '-': case '+': case '%': case '&': case '^': case '|': case LE: case GE: case GT: case LT: case NE: case EQ: case OR: case AND: case LSHIFT: case RSHIFT: AST_track(now->rgt, USE|code); /* fall through */ case '!': case UMIN: case '~': case 'c': case ENABLED: case SET_P: case GET_P: case ASSERT: AST_track(now->lft, USE|code); break; case EVAL: AST_track(now->lft, USE|(code&(~DEF))); break; case NAME: name_AST_track(now, code); if (now->sym->nel > 1 || now->sym->isarray) AST_track(now->lft, USE); /* index, was USE|code */ break; case 'R': AST_track(now->lft, DEREF_USE|USE|code); for (v = now->rgt; v; v = v->rgt) AST_track(v->lft, code); /* a deeper eval can add USE */ break; case '?': AST_track(now->lft, USE|code); if (now->rgt) { AST_track(now->rgt->lft, code); AST_track(now->rgt->rgt, code); } break; /* added for control deps: */ case TYPE: name_AST_track(now, code); break; case ASGN: AST_track(now->lft, DEF|code); AST_track(now->rgt, USE|code); break; case RUN: name_AST_track(now, USE); for (v = now->lft; v; v = v->rgt) AST_track(v->lft, USE|code); break; case 's': AST_track(now->lft, DEREF_DEF|DEREF_USE|USE|code); for (v = now->rgt; v; v = v->rgt) AST_track(v->lft, USE|code); break; case 'r': AST_track(now->lft, DEREF_DEF|DEREF_USE|USE|code); for (v = now->rgt; v; v = v->rgt) { in_recv++; AST_track(v->lft, DEF|code); in_recv--; } break; case PRINT: for (v = now->lft; v; v = v->rgt) AST_track(v->lft, USE|code); break; case PRINTM: AST_track(now->lft, USE); break; /* end add */ case 'p': #if 0 'p' -sym-> _p / '?' -sym-> a (proctype) / b (pid expr) #endif AST_track(now->lft->lft, USE|code); AST_procisrelevant(now->lft->sym); break; case CONST: case ELSE: case NONPROGRESS: case PC_VAL: case 'q': break; case '.': case GOTO: case BREAK: case '@': case D_STEP: case ATOMIC: case NON_ATOMIC: case IF: case DO: case UNLESS: case TIMEOUT: case C_CODE: case C_EXPR: break; default: printf("AST_track, NOT EXPECTED ntyp: %d\n", now->ntyp); break; } } static int AST_dump_rel(void) { Slicer *rv; Ordered *walk; char buf[64]; int banner=0; if (verbose&32) { printf("Relevant variables:\n"); for (rv = rel_vars; rv; rv = rv->nxt) { printf("\t"); AST_var(rv->n, rv->n->sym, 1); printf("\n"); } return 1; } for (rv = rel_vars; rv; rv = rv->nxt) rv->n->sym->setat = 1; /* mark it */ for (walk = all_names; walk; walk = walk->next) { Symbol *s; s = walk->entry; if (!s->setat && (s->type != MTYPE || s->ini->ntyp != CONST) && s->type != STRUCT /* report only fields */ && s->type != PROCTYPE && !s->owner && sputtype(buf, s->type)) { if (!banner) { banner = 1; printf("spin: redundant vars (for given property):\n"); } printf("\t"); symvar(s); } } return banner; } static void AST_suggestions(void) { Symbol *s; Ordered *walk; FSM_state *f; FSM_trans *t; AST *a; int banner=0; int talked=0; for (walk = all_names; walk; walk = walk->next) { s = walk->entry; if (s->colnr == 2 /* only used in conditionals */ && (s->type == BYTE || s->type == SHORT || s->type == INT || s->type == MTYPE)) { if (!banner) { banner = 1; printf("spin: consider using predicate"); printf(" abstraction to replace:\n"); } printf("\t"); symvar(s); } } /* look for source and sink processes */ for (a = ast; a; a = a->nxt) /* automata */ { banner = 0; for (f = a->fsm; f; f = f->nxt) /* control states */ for (t = f->t; t; t = t->nxt) /* transitions */ { if (t->step) switch (t->step->n->ntyp) { case 's': banner |= 1; break; case 'r': banner |= 2; break; case '.': case D_STEP: case ATOMIC: case NON_ATOMIC: case IF: case DO: case UNLESS: case '@': case GOTO: case BREAK: case PRINT: case PRINTM: case ASSERT: case C_CODE: case C_EXPR: break; default: banner |= 4; goto no_good; } } no_good: if (banner == 1 || banner == 2) { printf("spin: proctype %s defines a %s process\n", a->p->n->name, banner==1?"source":"sink"); talked |= banner; } else if (banner == 3) { printf("spin: proctype %s mimics a buffer\n", a->p->n->name); talked |= 4; } } if (talked&1) { printf("\tto reduce complexity, consider merging the code of\n"); printf("\teach source process into the code of its target\n"); } if (talked&2) { printf("\tto reduce complexity, consider merging the code of\n"); printf("\teach sink process into the code of its source\n"); } if (talked&4) printf("\tto reduce complexity, avoid buffer processes\n"); } static void AST_preserve(void) { Slicer *sc, *nx, *rv; for (sc = slicer; sc; sc = nx) { if (!sc->used) break; /* done */ nx = sc->nxt; for (rv = rel_vars; rv; rv = rv->nxt) if (AST_mutual(sc->n, rv->n, 1)) break; if (!rv) /* not already there */ { sc->nxt = rel_vars; rel_vars = sc; } } slicer = sc; } static void check_slice(Lextok *n, int code) { Slicer *sc; for (sc = slicer; sc; sc = sc->nxt) if (AST_mutual(sc->n, n, 1) && sc->code == code) return; /* already there */ sc = (Slicer *) emalloc(sizeof(Slicer)); sc->n = n; sc->code = code; sc->used = 0; sc->nxt = slicer; slicer = sc; } static void AST_data_dep(void) { Slicer *sc; /* mark all def-relevant transitions */ for (sc = slicer; sc; sc = sc->nxt) { sc->used = 1; if (verbose&32) { printf("spin: slice criterion "); AST_var(sc->n, sc->n->sym, 1); printf(" type=%d\n", Sym_typ(sc->n)); } AST_relevant(sc->n); } AST_tagruns(); /* mark 'run's relevant if target proctype is relevant */ } static int AST_blockable(AST *a, int s) { FSM_state *f; FSM_trans *t; f = fsm_tbl[s]; for (t = f->t; t; t = t->nxt) { if (t->relevant&2) return 1; if (t->step && t->step->n) switch (t->step->n->ntyp) { case IF: case DO: case ATOMIC: case NON_ATOMIC: case D_STEP: if (AST_blockable(a, t->to)) { t->round = AST_Round; t->relevant |= 2; return 1; } /* else fall through */ default: break; } else if (AST_blockable(a, t->to)) /* Unless */ { t->round = AST_Round; t->relevant |= 2; return 1; } } return 0; } static void AST_spread(AST *a, int s) { FSM_state *f; FSM_trans *t; f = fsm_tbl[s]; for (t = f->t; t; t = t->nxt) { if (t->relevant&2) continue; if (t->step && t->step->n) switch (t->step->n->ntyp) { case IF: case DO: case ATOMIC: case NON_ATOMIC: case D_STEP: AST_spread(a, t->to); /* fall thru */ default: t->round = AST_Round; t->relevant |= 2; break; } else /* Unless */ { AST_spread(a, t->to); t->round = AST_Round; t->relevant |= 2; } } } static int AST_notrelevant(Lextok *n) { Slicer *s; for (s = rel_vars; s; s = s->nxt) if (AST_mutual(s->n, n, 1)) return 0; for (s = slicer; s; s = s->nxt) if (AST_mutual(s->n, n, 1)) return 0; return 1; } static int AST_withchan(Lextok *n) { if (!n) return 0; if (Sym_typ(n) == CHAN) return 1; return AST_withchan(n->lft) || AST_withchan(n->rgt); } static int AST_suspect(FSM_trans *t) { FSM_use *u; /* check for possible overkill */ if (!t || !t->step || !AST_withchan(t->step->n)) return 0; for (u = t->Val[0]; u; u = u->nxt) if (AST_notrelevant(u->n)) return 1; return 0; } static void AST_shouldconsider(AST *a, int s) { FSM_state *f; FSM_trans *t; f = fsm_tbl[s]; for (t = f->t; t; t = t->nxt) { if (t->step && t->step->n) switch (t->step->n->ntyp) { case IF: case DO: case ATOMIC: case NON_ATOMIC: case D_STEP: AST_shouldconsider(a, t->to); break; default: AST_track(t->step->n, 0); /* AST_track is called here for a blockable stmnt from which a relevant stmnmt was shown to be reachable for a condition this makes all USEs relevant but for a channel operation it only makes the executability relevant -- in those cases, parameters that aren't already relevant may be replaceable with arbitrary tokens */ if (AST_suspect(t)) { printf("spin: possibly redundant parameters in: "); comment(stdout, t->step->n, 0); printf("\n"); } break; } else /* an Unless */ AST_shouldconsider(a, t->to); } } static int FSM_critical(AST *a, int s) { FSM_state *f; FSM_trans *t; /* is a 1-relevant stmnt reachable from this state? */ f = fsm_tbl[s]; if (f->seen) goto done; f->seen = 1; f->cr = 0; for (t = f->t; t; t = t->nxt) if ((t->relevant&1) || FSM_critical(a, t->to)) { f->cr = 1; if (verbose&32) { printf("\t\t\t\tcritical(%d) ", t->relevant); comment(stdout, t->step->n, 0); printf("\n"); } break; } #if 0 else { if (verbose&32) { printf("\t\t\t\tnot-crit "); comment(stdout, t->step->n, 0); printf("\n"); } } #endif done: return f->cr; } static void AST_ctrl(AST *a) { FSM_state *f; FSM_trans *t; int hit; /* add all blockable transitions * from which relevant transitions can be reached */ if (verbose&32) printf("CTL -- %s\n", a->p->n->name); /* 1 : mark all blockable edges */ for (f = a->fsm; f; f = f->nxt) { if (!(f->scratch&2)) /* not part of irrelevant subgraph */ for (t = f->t; t; t = t->nxt) { if (t->step && t->step->n) switch (t->step->n->ntyp) { case 'r': case 's': case 'c': case ELSE: t->round = AST_Round; t->relevant |= 2; /* mark for next phases */ if (verbose&32) { printf("\tpremark "); comment(stdout, t->step->n, 0); printf("\n"); } break; default: break; } } } /* 2: keep only 2-marked stmnts from which 1-marked stmnts can be reached */ for (f = a->fsm; f; f = f->nxt) { fsm_tbl[f->from] = f; f->seen = 0; /* used in dfs from FSM_critical */ } for (f = a->fsm; f; f = f->nxt) { if (!FSM_critical(a, f->from)) for (t = f->t; t; t = t->nxt) if (t->relevant&2) { t->relevant &= ~2; /* clear mark */ if (verbose&32) { printf("\t\tnomark "); if (t->step && t->step->n) comment(stdout, t->step->n, 0); printf("\n"); } } } /* 3 : lift marks across IF/DO etc. */ for (f = a->fsm; f; f = f->nxt) { hit = 0; for (t = f->t; t; t = t->nxt) { if (t->step && t->step->n) switch (t->step->n->ntyp) { case IF: case DO: case ATOMIC: case NON_ATOMIC: case D_STEP: if (AST_blockable(a, t->to)) hit = 1; break; default: break; } else if (AST_blockable(a, t->to)) /* Unless */ hit = 1; if (hit) break; } if (hit) /* at least one outgoing trans can block */ for (t = f->t; t; t = t->nxt) { t->round = AST_Round; t->relevant |= 2; /* lift */ if (verbose&32) { printf("\t\t\tliftmark "); if (t->step && t->step->n) comment(stdout, t->step->n, 0); printf("\n"); } AST_spread(a, t->to); /* and spread to all guards */ } } /* 4: nodes with 2-marked out-edges contribute new slice criteria */ for (f = a->fsm; f; f = f->nxt) for (t = f->t; t; t = t->nxt) if (t->relevant&2) { AST_shouldconsider(a, f->from); break; /* inner loop */ } } static void AST_control_dep(void) { AST *a; for (a = ast; a; a = a->nxt) { if (a->p->b != N_CLAIM && a->p->b != E_TRACE && a->p->b != N_TRACE) { AST_ctrl(a); } } } static void AST_prelabel(void) { AST *a; FSM_state *f; FSM_trans *t; for (a = ast; a; a = a->nxt) { if (a->p->b != N_CLAIM && a->p->b != E_TRACE && a->p->b != N_TRACE) for (f = a->fsm; f; f = f->nxt) for (t = f->t; t; t = t->nxt) { if (t->step && t->step->n && t->step->n->ntyp == ASSERT ) { t->relevant |= 1; } } } } static void AST_criteria(void) { /* * remote labels are handled separately -- by making * sure they are not pruned away during optimization */ AST_Changes = 1; /* to get started */ for (AST_Round = 1; slicer && AST_Changes; AST_Round++) { AST_Changes = 0; AST_data_dep(); AST_preserve(); /* moves processed vars from slicer to rel_vars */ AST_dominant(); /* mark data-irrelevant subgraphs */ AST_control_dep(); /* can add data deps, which add control deps */ if (verbose&32) printf("\n\nROUND %d -- changes %d\n", AST_Round, AST_Changes); } } static void AST_alias_analysis(void) /* aliasing of promela channels */ { AST *a; for (a = ast; a; a = a->nxt) AST_sends(a); /* collect chan-names that are send across chans */ for (a = ast; a; a = a->nxt) AST_para(a->p); /* aliasing of chans thru proctype parameters */ for (a = ast; a; a = a->nxt) AST_other(a); /* chan params in asgns and recvs */ AST_trans(); /* transitive closure of alias table */ if (verbose&32) AST_aliases(); /* show channel aliasing info */ } void AST_slice(void) { AST *a; int spurious = 0; if (!slicer) { printf("spin: warning: no slice criteria found (no assertions and no claim)\n"); spurious = 1; } AST_dorelevant(); /* mark procs refered to in remote refs */ for (a = ast; a; a = a->nxt) AST_def_use(a); /* compute standard def/use information */ AST_hidden(); /* parameter passing and local var inits */ AST_alias_analysis(); /* channel alias analysis */ AST_prelabel(); /* mark all 'assert(...)' stmnts as relevant */ AST_criteria(); /* process the slice criteria from * asserts and from the never claim */ if (!spurious || (verbose&32)) { spurious = 1; for (a = ast; a; a = a->nxt) { AST_dump(a); /* marked up result */ if (a->relevant&2) /* it printed something */ spurious = 0; } if (!AST_dump_rel() /* relevant variables */ && spurious) printf("spin: no redundancies found (for given property)\n"); } AST_suggestions(); if (verbose&32) show_expl(); } void AST_store(ProcList *p, int start_state) { AST *n_ast; if (p->b != N_CLAIM && p->b != E_TRACE && p->b != N_TRACE) { n_ast = (AST *) emalloc(sizeof(AST)); n_ast->p = p; n_ast->i_st = start_state; n_ast->relevant = 0; n_ast->fsm = fsm; n_ast->nxt = ast; ast = n_ast; } fsm = (FSM_state *) 0; /* hide it from FSM_DEL */ } static void AST_add_explicit(Lextok *d, Lextok *u) { FSM_trans *e = (FSM_trans *) emalloc(sizeof(FSM_trans)); e->to = 0; /* or start_state ? */ e->relevant = 0; /* to be determined */ e->step = (Element *) 0; /* left blank */ e->Val[0] = e->Val[1] = (FSM_use *) 0; cur_t = e; def_use(u, USE); def_use(d, DEF); cur_t = (FSM_trans *) 0; e->nxt = explicit; explicit = e; } static void AST_fp1(char *s, Lextok *t, Lextok *f, int parno) { Lextok *v; int cnt; if (!t) return; if (t->ntyp == RUN) { if (strcmp(t->sym->name, s) == 0) for (v = t->lft, cnt = 1; v; v = v->rgt, cnt++) if (cnt == parno) { AST_add_explicit(f, v->lft); break; } } else { AST_fp1(s, t->lft, f, parno); AST_fp1(s, t->rgt, f, parno); } } static void AST_mk1(char *s, Lextok *c, int parno) { AST *a; FSM_state *f; FSM_trans *t; /* concoct an extra FSM_trans *t with the asgn of * formal par c to matching actual pars made explicit */ for (a = ast; a; a = a->nxt) /* automata */ for (f = a->fsm; f; f = f->nxt) /* control states */ for (t = f->t; t; t = t->nxt) /* transitions */ { if (t->step) AST_fp1(s, t->step->n, c, parno); } } static void AST_par_init(void) /* parameter passing -- hidden assignments */ { AST *a; Lextok *f, *t, *c; int cnt; for (a = ast; a; a = a->nxt) { if (a->p->b == N_CLAIM || a->p->b == I_PROC || a->p->b == E_TRACE || a->p->b == N_TRACE) { continue; /* has no params */ } cnt = 0; for (f = a->p->p; f; f = f->rgt) /* types */ for (t = f->lft; t; t = t->rgt) /* formals */ { cnt++; /* formal par count */ c = (t->ntyp != ',')? t : t->lft; /* the formal parameter */ AST_mk1(a->p->n->name, c, cnt); /* all matching run statements */ } } } static void AST_var_init(void) /* initialized vars (not chans) - hidden assignments */ { Ordered *walk; Lextok *x; Symbol *sp; AST *a; for (walk = all_names; walk; walk = walk->next) { sp = walk->entry; if (sp && !sp->context /* globals */ && sp->type != PROCTYPE && sp->ini && (sp->type != MTYPE || sp->ini->ntyp != CONST) /* not mtype defs */ && sp->ini->ntyp != CHAN) { x = nn(ZN, TYPE, ZN, ZN); x->sym = sp; AST_add_explicit(x, sp->ini); } } for (a = ast; a; a = a->nxt) { if (a->p->b != N_CLAIM && a->p->b != E_TRACE && a->p->b != N_TRACE) /* has no locals */ for (walk = all_names; walk; walk = walk->next) { sp = walk->entry; if (sp && sp->context && strcmp(sp->context->name, a->p->n->name) == 0 && sp->Nid >= 0 /* not a param */ && sp->type != LABEL && sp->ini && sp->ini->ntyp != CHAN) { x = nn(ZN, TYPE, ZN, ZN); x->sym = sp; AST_add_explicit(x, sp->ini); } } } } static void show_expl(void) { FSM_trans *t, *T; FSM_use *u; printf("\nExplicit List:\n"); for (T = expl_par; T; T = (T == expl_par)?expl_var: (FSM_trans *) 0) { for (t = T; t; t = t->nxt) { if (!t->Val[0]) continue; printf("%s", t->relevant?"*":" "); printf("%3d", t->round); for (u = t->Val[0]; u; u = u->nxt) { printf("\t<"); AST_var(u->n, u->n->sym, 1); printf(":%d>, ", u->special); } printf("\n"); } printf("==\n"); } printf("End\n"); } static void AST_hidden(void) /* reveal all hidden assignments */ { AST_par_init(); expl_par = explicit; explicit = (FSM_trans *) 0; AST_var_init(); expl_var = explicit; explicit = (FSM_trans *) 0; } #define BPW (8*sizeof(ulong)) /* bits per word */ static int bad_scratch(FSM_state *f, int upto) { FSM_trans *t; #if 0 1. all internal branch-points have else-s 2. all non-branchpoints have non-blocking out-edge 3. all internal edges are non-relevant subgraphs like this need NOT contribute control-dependencies #endif if (!f->seen || (f->scratch&4)) return 0; if (f->scratch&8) return 1; f->scratch |= 4; if (verbose&32) printf("X[%d:%d:%d] ", f->from, upto, f->scratch); if (f->scratch&1) { if (verbose&32) printf("\tbad scratch: %d\n", f->from); bad: f->scratch &= ~4; /* f->scratch |= 8; wrong */ return 1; } if (f->from != upto) for (t = f->t; t; t = t->nxt) if (bad_scratch(fsm_tbl[t->to], upto)) goto bad; return 0; } static void mark_subgraph(FSM_state *f, int upto) { FSM_trans *t; if (f->from == upto || !f->seen || (f->scratch&2)) return; f->scratch |= 2; for (t = f->t; t; t = t->nxt) mark_subgraph(fsm_tbl[t->to], upto); } static void AST_pair(AST *a, FSM_state *h, int y) { Pair *p; for (p = a->pairs; p; p = p->nxt) if (p->h == h && p->b == y) return; p = (Pair *) emalloc(sizeof(Pair)); p->h = h; p->b = y; p->nxt = a->pairs; a->pairs = p; } static void AST_checkpairs(AST *a) { Pair *p; for (p = a->pairs; p; p = p->nxt) { if (verbose&32) printf(" inspect pair %d %d\n", p->b, p->h->from); if (!bad_scratch(p->h, p->b)) /* subgraph is clean */ { if (verbose&32) printf("subgraph: %d .. %d\n", p->b, p->h->from); mark_subgraph(p->h, p->b); } } } static void subgraph(AST *a, FSM_state *f, int out) { FSM_state *h; int i, j; ulong *g; #if 0 reverse dominance suggests that this is a possible entry and exit node for a proper subgraph #endif h = fsm_tbl[out]; i = f->from / BPW; j = f->from % BPW; /* assert(j <= 32); else lshift undefined? */ g = h->mod; if (verbose&32) printf("possible pair %d %d -- %d\n", f->from, h->from, (g[i]&(1<<j))?1:0); if (g[i]&(1<<j)) /* also a forward dominance pair */ AST_pair(a, h, f->from); /* record this pair */ } static void act_dom(AST *a) { FSM_state *f; FSM_trans *t; int i, j, cnt; for (f = a->fsm; f; f = f->nxt) { if (!f->seen) continue; #if 0 f->from is the exit-node of a proper subgraph, with the dominator its entry-node, if: a. this node has more than 1 reachable predecessor b. the dominator has more than 1 reachable successor (need reachability - in case of reverse dominance) d. the dominator is reachable, and not equal to this node #endif for (t = f->p, i = 0; t; t = t->nxt) { i += fsm_tbl[t->to]->seen; } if (i <= 1) { continue; /* a. */ } for (cnt = 1; cnt < a->nstates; cnt++) /* 0 is endstate */ { if (cnt == f->from || !fsm_tbl[cnt]->seen) { continue; /* c. */ } i = cnt / BPW; j = cnt % BPW; /* assert(j <= 32); */ if (!(f->dom[i]&(1<<j))) { continue; } for (t = fsm_tbl[cnt]->t, i = 0; t; t = t->nxt) { i += fsm_tbl[t->to]->seen; } if (i <= 1) { continue; /* b. */ } if (f->mod) /* final check in 2nd phase */ { subgraph(a, f, cnt); /* possible entry-exit pair */ } } } } static void reachability(AST *a) { FSM_state *f; for (f = a->fsm; f; f = f->nxt) f->seen = 0; /* clear */ AST_dfs(a, a->i_st, 0); /* mark 'seen' */ } static int see_else(FSM_state *f) { FSM_trans *t; for (t = f->t; t; t = t->nxt) { if (t->step && t->step->n) switch (t->step->n->ntyp) { case ELSE: return 1; case IF: case DO: case ATOMIC: case NON_ATOMIC: case D_STEP: if (see_else(fsm_tbl[t->to])) return 1; default: break; } } return 0; } static int is_guard(FSM_state *f) { FSM_state *g; FSM_trans *t; for (t = f->p; t; t = t->nxt) { g = fsm_tbl[t->to]; if (!g->seen) continue; if (t->step && t->step->n) switch(t->step->n->ntyp) { case IF: case DO: return 1; case ATOMIC: case NON_ATOMIC: case D_STEP: if (is_guard(g)) return 1; default: break; } } return 0; } static void curtail(AST *a) { FSM_state *f, *g; FSM_trans *t; int i, haselse, isrel, blocking; #if 0 mark nodes that do not satisfy these requirements: 1. all internal branch-points have else-s 2. all non-branchpoints have non-blocking out-edge 3. all internal edges are non-data-relevant #endif if (verbose&32) printf("Curtail %s:\n", a->p->n->name); for (f = a->fsm; f; f = f->nxt) { if (!f->seen || (f->scratch&(1|2))) continue; isrel = haselse = i = blocking = 0; for (t = f->t; t; t = t->nxt) { g = fsm_tbl[t->to]; isrel |= (t->relevant&1); /* data relevant */ i += g->seen; if (t->step && t->step->n) { switch (t->step->n->ntyp) { case IF: case DO: haselse |= see_else(g); break; case 'c': case 's': case 'r': blocking = 1; break; } } } #if 0 if (verbose&32) printf("prescratch %d -- %d %d %d %d -- %d\n", f->from, i, isrel, blocking, haselse, is_guard(f)); #endif if (isrel /* 3. */ || (i == 1 && blocking) /* 2. */ || (i > 1 && !haselse)) /* 1. */ { if (!is_guard(f)) { f->scratch |= 1; if (verbose&32) printf("scratch %d -- %d %d %d %d\n", f->from, i, isrel, blocking, haselse); } } } } static void init_dom(AST *a) { FSM_state *f; int i, j, cnt; #if 0 (1) D(s0) = {s0} (2) for s in S - {s0} do D(s) = S #endif for (f = a->fsm; f; f = f->nxt) { if (!f->seen) continue; f->dom = (ulong *) emalloc(a->nwords * sizeof(ulong)); if (f->from == a->i_st) { i = a->i_st / BPW; j = a->i_st % BPW; /* assert(j <= 32); */ f->dom[i] = (1<<j); /* (1) */ } else /* (2) */ { for (i = 0; i < a->nwords; i++) { f->dom[i] = (ulong) ~0; /* all 1's */ } if (a->nstates % BPW) for (i = (a->nstates % BPW); i < (int) BPW; i++) { f->dom[a->nwords-1] &= ~(1<< ((ulong) i)); /* clear tail */ } for (cnt = 0; cnt < a->nstates; cnt++) { if (!fsm_tbl[cnt]->seen) { i = cnt / BPW; j = cnt % BPW; /* assert(j <= 32); */ f->dom[i] &= ~(1<< ((ulong) j)); } } } } } static int dom_perculate(AST *a, FSM_state *f) { static ulong *ndom = (ulong *) 0; static int on = 0; int i, j, cnt = 0; FSM_state *g; FSM_trans *t; if (on < a->nwords) { on = a->nwords; ndom = (ulong *) emalloc(on * sizeof(ulong)); } for (i = 0; i < a->nwords; i++) ndom[i] = (ulong) ~0; for (t = f->p; t; t = t->nxt) /* all reachable predecessors */ { g = fsm_tbl[t->to]; if (g->seen) for (i = 0; i < a->nwords; i++) ndom[i] &= g->dom[i]; /* (5b) */ } i = f->from / BPW; j = f->from % BPW; /* assert(j <= 32); */ ndom[i] |= (1<<j); /* (5a) */ for (i = 0; i < a->nwords; i++) if (f->dom[i] != ndom[i]) { cnt++; f->dom[i] = ndom[i]; } return cnt; } static void dom_forward(AST *a) { FSM_state *f; int cnt; init_dom(a); /* (1,2) */ do { cnt = 0; for (f = a->fsm; f; f = f->nxt) { if (f->seen && f->from != a->i_st) /* (4) */ cnt += dom_perculate(a, f); /* (5) */ } } while (cnt); /* (3) */ dom_perculate(a, fsm_tbl[a->i_st]); } static void AST_dominant(void) { FSM_state *f; FSM_trans *t; AST *a; int oi; static FSM_state no_state; #if 0 find dominators Aho, Sethi, & Ullman, Compilers - principles, techniques, and tools Addison-Wesley, 1986, p.671. (1) D(s0) = {s0} (2) for s in S - {s0} do D(s) = S (3) while any D(s) changes do (4) for s in S - {s0} do (5) D(s) = {s} union with intersection of all D(p) where p are the immediate predecessors of s the purpose is to find proper subgraphs (one entry node, one exit node) #endif if (AST_Round == 1) /* computed once, reused in every round */ for (a = ast; a; a = a->nxt) { a->nstates = 0; for (f = a->fsm; f; f = f->nxt) { a->nstates++; /* count */ fsm_tbl[f->from] = f; /* fast lookup */ f->scratch = 0; /* clear scratch marks */ } for (oi = 0; oi < a->nstates; oi++) if (!fsm_tbl[oi]) fsm_tbl[oi] = &no_state; a->nwords = (a->nstates + BPW - 1) / BPW; /* round up */ if (verbose&32) { printf("%s (%d): ", a->p->n->name, a->i_st); printf("states=%d (max %d), words = %d, bpw %d, overflow %d\n", a->nstates, o_max, a->nwords, (int) BPW, (int) (a->nstates % BPW)); } reachability(a); dom_forward(a); /* forward dominance relation */ curtail(a); /* mark ineligible edges */ for (f = a->fsm; f; f = f->nxt) { t = f->p; f->p = f->t; f->t = t; /* invert edges */ f->mod = f->dom; f->dom = (ulong *) 0; } oi = a->i_st; if (fsm_tbl[0]->seen) /* end-state reachable - else leave it */ a->i_st = 0; /* becomes initial state */ dom_forward(a); /* reverse dominance -- don't redo reachability! */ act_dom(a); /* mark proper subgraphs, if any */ AST_checkpairs(a); /* selectively place 2 scratch-marks */ for (f = a->fsm; f; f = f->nxt) { t = f->p; f->p = f->t; f->t = t; /* restore */ } a->i_st = oi; /* restore */ } else for (a = ast; a; a = a->nxt) { for (f = a->fsm; f; f = f->nxt) { fsm_tbl[f->from] = f; f->scratch &= 1; /* preserve 1-marks */ } for (oi = 0; oi < a->nstates; oi++) if (!fsm_tbl[oi]) fsm_tbl[oi] = &no_state; curtail(a); /* mark ineligible edges */ for (f = a->fsm; f; f = f->nxt) { t = f->p; f->p = f->t; f->t = t; /* invert edges */ } AST_checkpairs(a); /* recompute 2-marks */ for (f = a->fsm; f; f = f->nxt) { t = f->p; f->p = f->t; f->t = t; /* restore */ } } }