123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912913914915916917918919920921922923924925926927928929930931932933934935936937938939940941942943944945946947948949950951952953954955956957958959960961962963964965966967968969970971972973974975976977978979980981982983984985986987988989990991992993994995996997998999100010011002100310041005100610071008100910101011101210131014101510161017101810191020102110221023102410251026102710281029103010311032103310341035103610371038103910401041104210431044104510461047104810491050105110521053105410551056105710581059106010611062106310641065106610671068106910701071107210731074107510761077107810791080108110821083108410851086108710881089109010911092109310941095109610971098109911001101110211031104110511061107110811091110111111121113111411151116111711181119112011211122112311241125112611271128112911301131113211331134113511361137113811391140114111421143114411451146114711481149115011511152115311541155115611571158115911601161116211631164116511661167116811691170117111721173117411751176117711781179118011811182118311841185118611871188118911901191119211931194119511961197119811991200120112021203120412051206120712081209121012111212121312141215121612171218121912201221122212231224122512261227122812291230123112321233123412351236123712381239124012411242124312441245124612471248124912501251125212531254125512561257125812591260126112621263126412651266126712681269127012711272127312741275127612771278127912801281128212831284128512861287128812891290129112921293129412951296129712981299130013011302130313041305130613071308130913101311131213131314131513161317131813191320132113221323132413251326132713281329133013311332133313341335133613371338133913401341134213431344134513461347134813491350135113521353135413551356135713581359136013611362136313641365136613671368136913701371137213731374137513761377137813791380138113821383138413851386138713881389139013911392139313941395139613971398139914001401140214031404140514061407140814091410141114121413141414151416141714181419142014211422142314241425142614271428142914301431143214331434143514361437143814391440144114421443144414451446144714481449145014511452145314541455145614571458145914601461146214631464146514661467146814691470147114721473147414751476147714781479148014811482148314841485148614871488148914901491149214931494149514961497149814991500150115021503150415051506150715081509151015111512151315141515151615171518151915201521152215231524152515261527152815291530153115321533153415351536153715381539154015411542154315441545154615471548154915501551155215531554155515561557155815591560156115621563156415651566156715681569157015711572157315741575157615771578157915801581158215831584158515861587158815891590159115921593159415951596159715981599160016011602160316041605160616071608160916101611161216131614161516161617161816191620162116221623162416251626162716281629163016311632163316341635163616371638163916401641164216431644164516461647164816491650165116521653165416551656165716581659166016611662166316641665166616671668166916701671167216731674167516761677167816791680168116821683168416851686168716881689169016911692169316941695169616971698169917001701170217031704170517061707170817091710171117121713171417151716171717181719172017211722172317241725172617271728172917301731173217331734173517361737173817391740174117421743174417451746174717481749175017511752175317541755175617571758175917601761176217631764176517661767176817691770177117721773177417751776177717781779178017811782178317841785178617871788178917901791179217931794179517961797179817991800180118021803180418051806180718081809181018111812181318141815181618171818181918201821182218231824182518261827182818291830183118321833183418351836183718381839184018411842184318441845184618471848184918501851185218531854185518561857185818591860186118621863186418651866186718681869187018711872187318741875187618771878187918801881188218831884188518861887188818891890189118921893189418951896189718981899190019011902190319041905190619071908190919101911191219131914191519161917191819191920192119221923192419251926192719281929193019311932193319341935193619371938193919401941194219431944194519461947194819491950195119521953195419551956195719581959196019611962196319641965196619671968196919701971197219731974197519761977197819791980198119821983198419851986198719881989199019911992199319941995199619971998199920002001200220032004200520062007200820092010201120122013201420152016201720182019202020212022202320242025202620272028202920302031203220332034203520362037203820392040204120422043204420452046204720482049205020512052205320542055205620572058205920602061206220632064206520662067206820692070207120722073207420752076207720782079208020812082208320842085208620872088208920902091209220932094209520962097209820992100210121022103210421052106210721082109211021112112211321142115211621172118211921202121212221232124212521262127212821292130213121322133213421352136213721382139214021412142214321442145214621472148214921502151215221532154215521562157215821592160216121622163216421652166216721682169217021712172217321742175217621772178217921802181218221832184218521862187218821892190219121922193219421952196219721982199220022012202220322042205220622072208220922102211221222132214221522162217221822192220222122222223222422252226222722282229223022312232223322342235223622372238223922402241224222432244224522462247224822492250225122522253225422552256225722582259226022612262226322642265226622672268226922702271227222732274227522762277227822792280228122822283228422852286228722882289229022912292229322942295229622972298229923002301230223032304230523062307230823092310231123122313231423152316231723182319232023212322232323242325232623272328232923302331233223332334233523362337233823392340234123422343234423452346234723482349235023512352 |
- /***** spin: pangen6.c *****/
- /* Copyright (c) 2000-2003 by Lucent Technologies, Bell Laboratories. */
- /* All Rights Reserved. This software is for educational purposes only. */
- /* No guarantee whatsoever is expressed or implied by the distribution of */
- /* this code. Permission is given to distribute this code provided that */
- /* this introductory message is not removed and no monies are exchanged. */
- /* Software written by Gerard J. Holzmann. For tool documentation see: */
- /* http://spinroot.com/ */
- /* Send all bug-reports and/or questions to: bugs@spinroot.com */
- /* Abstract syntax tree analysis / slicing (spin option -A) */
- /* AST_store stores the fsms's for each proctype */
- /* AST_track keeps track of variables used in properties */
- /* AST_slice starts the slicing algorithm */
- /* it first collects more info and then calls */
- /* AST_criteria to process the slice criteria */
- #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 FSM_state no_state;
- 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)
- 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 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)
- 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 a = AST_nrpar(cl->s);
- int b = AST_nrpar(t->step->n);
- if (a != b) /* matching nrs of params */
- continue;
- a = AST_ord(cl->s, cl->n);
- b = AST_ord(t->step->n, u->n);
- if (a != b) /* 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 (strcmp(a->p->n->name, ":never:") != 0
- && strcmp(a->p->n->name, ":trace:") != 0
- && strcmp(a->p->n->name, ":notrace:") != 0)
- 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 (strcmp(a->p->n->name, ":never:") == 0
- || strcmp(a->p->n->name, ":trace:") == 0
- || strcmp(a->p->n->name, ":notrace:") == 0
- || strcmp(a->p->n->name, ":init:") == 0)
- { 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(" line %3d %s (state %d)",
- e->n?e->n->ln:-1,
- e->n?e->n->fn->name:"-",
- 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: error: DEF and USE of same var in rcv stmnt: ");
- 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 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)
- AST_track(now->lft, USE|code); /* index */
- 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 ");
- 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 ");
- 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 (strcmp(a->p->n->name, ":never:") != 0
- && strcmp(a->p->n->name, ":trace:") != 0
- && strcmp(a->p->n->name, ":notrace:") != 0)
- AST_ctrl(a);
- }
- static void
- AST_prelabel(void)
- { AST *a;
- FSM_state *f;
- FSM_trans *t;
- for (a = ast; a; a = a->nxt)
- { if (strcmp(a->p->n->name, ":never:") != 0
- && strcmp(a->p->n->name, ":trace:") != 0
- && strcmp(a->p->n->name, ":notrace:") != 0)
- 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)
- { non_fatal("no slice criteria (or no claim) specified",
- (char *) 0);
- 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 (strcmp(p->n->name, ":never:") != 0
- && strcmp(p->n->name, ":trace:") != 0
- && strcmp(p->n->name, ":notrace:") != 0)
- { 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 (strcmp(a->p->n->name, ":never:") == 0
- || strcmp(a->p->n->name, ":trace:") == 0
- || strcmp(a->p->n->name, ":notrace:") == 0
- || strcmp(a->p->n->name, ":init:") == 0)
- continue; /* have 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 (strcmp(a->p->n->name, ":never:") != 0
- && strcmp(a->p->n->name, ":trace:") != 0
- && strcmp(a->p->n->name, ":notrace:") != 0) /* claim 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;
- 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;
- 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;
- 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<<i); /* clear tail */
- for (cnt = 0; cnt < a->nstates; cnt++)
- if (!fsm_tbl[cnt]->seen)
- { i = cnt / BPW;
- j = cnt % BPW;
- f->dom[i] &= ~(1<<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;
- 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;
- #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 */
- } }
- }
|