123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857 |
- /***** spin: pangen5.c *****/
- /* Copyright (c) 1999-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 */
- #include "spin.h"
- #include "y.tab.h"
- typedef struct BuildStack {
- FSM_trans *t;
- struct BuildStack *nxt;
- } BuildStack;
- extern ProcList *rdy;
- extern int verbose, eventmapnr, claimnr, rvopt, export_ast, u_sync;
- extern Element *Al_El;
- static FSM_state *fsm_free;
- static FSM_trans *trans_free;
- static BuildStack *bs, *bf;
- static int max_st_id;
- static int cur_st_id;
- int o_max;
- FSM_state *fsm;
- FSM_state **fsm_tbl;
- FSM_use *use_free;
- static void ana_seq(Sequence *);
- static void ana_stmnt(FSM_trans *, Lextok *, int);
- extern void AST_slice(void);
- extern void AST_store(ProcList *, int);
- extern int has_global(Lextok *);
- extern void exit(int);
- static void
- fsm_table(void)
- { FSM_state *f;
- max_st_id += 2;
- /* fprintf(stderr, "omax %d, max=%d\n", o_max, max_st_id); */
- if (o_max < max_st_id)
- { o_max = max_st_id;
- fsm_tbl = (FSM_state **) emalloc(max_st_id * sizeof(FSM_state *));
- } else
- memset((char *)fsm_tbl, 0, max_st_id * sizeof(FSM_state *));
- cur_st_id = max_st_id;
- max_st_id = 0;
- for (f = fsm; f; f = f->nxt)
- fsm_tbl[f->from] = f;
- }
- static int
- FSM_DFS(int from, FSM_use *u)
- { FSM_state *f;
- FSM_trans *t;
- FSM_use *v;
- int n;
- if (from == 0)
- return 1;
- f = fsm_tbl[from];
- if (!f)
- { printf("cannot find state %d\n", from);
- fatal("fsm_dfs: cannot happen\n", (char *) 0);
- }
- if (f->seen)
- return 1;
- f->seen = 1;
- for (t = f->t; t; t = t->nxt)
- {
- for (n = 0; n < 2; n++)
- for (v = t->Val[n]; v; v = v->nxt)
- if (u->var == v->var)
- return n; /* a read or write */
- if (!FSM_DFS(t->to, u))
- return 0;
- }
- return 1;
- }
- static void
- new_dfs(void)
- { int i;
- for (i = 0; i < cur_st_id; i++)
- if (fsm_tbl[i])
- fsm_tbl[i]->seen = 0;
- }
- static int
- good_dead(Element *e, FSM_use *u)
- {
- switch (u->special) {
- case 2: /* ok if it's a receive */
- if (e->n->ntyp == ASGN
- && e->n->rgt->ntyp == CONST
- && e->n->rgt->val == 0)
- return 0;
- break;
- case 1: /* must be able to use oval */
- if (e->n->ntyp != 'c'
- && e->n->ntyp != 'r')
- return 0; /* can't really happen */
- break;
- }
- return 1;
- }
- #if 0
- static int howdeep = 0;
- #endif
- static int
- eligible(FSM_trans *v)
- { Element *el = ZE;
- Lextok *lt = ZN;
- if (v) el = v->step;
- if (el) lt = v->step->n;
- if (!lt /* dead end */
- || v->nxt /* has alternatives */
- || el->esc /* has an escape */
- || (el->status&CHECK2) /* remotely referenced */
- || lt->ntyp == ATOMIC
- || lt->ntyp == NON_ATOMIC /* used for inlines -- should be able to handle this */
- || lt->ntyp == IF
- || lt->ntyp == C_CODE
- || lt->ntyp == C_EXPR
- || has_lab(el, 0) /* any label at all */
- || lt->ntyp == DO
- || lt->ntyp == UNLESS
- || lt->ntyp == D_STEP
- || lt->ntyp == ELSE
- || lt->ntyp == '@'
- || lt->ntyp == 'c'
- || lt->ntyp == 'r'
- || lt->ntyp == 's')
- return 0;
- if (!(el->status&(2|4))) /* not atomic */
- { int unsafe = (el->status&I_GLOB)?1:has_global(el->n);
- if (unsafe)
- return 0;
- }
- return 1;
- }
- static int
- canfill_in(FSM_trans *v)
- { Element *el = v->step;
- Lextok *lt = v->step->n;
- if (!lt /* dead end */
- || v->nxt /* has alternatives */
- || el->esc /* has an escape */
- || (el->status&CHECK2)) /* remotely referenced */
- return 0;
- if (!(el->status&(2|4)) /* not atomic */
- && ((el->status&I_GLOB)
- || has_global(el->n))) /* and not safe */
- return 0;
- return 1;
- }
- static int
- pushbuild(FSM_trans *v)
- { BuildStack *b;
- for (b = bs; b; b = b->nxt)
- if (b->t == v)
- return 0;
- if (bf)
- { b = bf;
- bf = bf->nxt;
- } else
- b = (BuildStack *) emalloc(sizeof(BuildStack));
- b->t = v;
- b->nxt = bs;
- bs = b;
- return 1;
- }
- static void
- popbuild(void)
- { BuildStack *f;
- if (!bs)
- fatal("cannot happen, popbuild", (char *) 0);
- f = bs;
- bs = bs->nxt;
- f->nxt = bf;
- bf = f; /* freelist */
- }
- static int
- build_step(FSM_trans *v)
- { FSM_state *f;
- Element *el = v->step;
- #if 0
- Lextok *lt = ZN;
- #endif
- int st = v->to;
- int r;
- if (!el) return -1;
- if (v->step->merge)
- return v->step->merge; /* already done */
- if (!eligible(v)) /* non-blocking */
- return -1;
- if (!pushbuild(v)) /* cycle detected */
- return -1; /* break cycle */
- f = fsm_tbl[st];
- #if 0
- lt = v->step->n;
- if (verbose&32)
- { if (++howdeep == 1)
- printf("spin: %s, line %3d, merge:\n",
- lt->fn->name,
- lt->ln);
- printf("\t[%d] <seqno %d>\t", howdeep, el->seqno);
- comment(stdout, lt, 0);
- printf(";\n");
- }
- #endif
- r = build_step(f->t);
- v->step->merge = (r == -1) ? st : r;
- #if 0
- if (verbose&32)
- { printf(" merge value: %d (st=%d,r=%d, line %d)\n",
- v->step->merge, st, r, el->n->ln);
- howdeep--;
- }
- #endif
- popbuild();
- return v->step->merge;
- }
- static void
- FSM_MERGER(char *pname_unused) /* find candidates for safely merging steps */
- { FSM_state *f, *g;
- FSM_trans *t;
- Lextok *lt;
- for (f = fsm; f; f = f->nxt) /* all states */
- for (t = f->t; t; t = t->nxt) /* all edges */
- { if (!t->step) continue; /* happens with 'unless' */
- t->step->merge_in = f->in; /* ?? */
- if (t->step->merge)
- continue;
- lt = t->step->n;
- if (lt->ntyp == 'c'
- || lt->ntyp == 'r'
- || lt->ntyp == 's') /* blocking stmnts */
- continue; /* handled in 2nd scan */
- if (!eligible(t))
- continue;
- g = fsm_tbl[t->to];
- if (!eligible(g->t))
- {
- #define SINGLES
- #ifdef SINGLES
- t->step->merge_single = t->to;
- #if 0
- if ((verbose&32))
- { printf("spin: %s, line %3d, merge_single:\n\t<seqno %d>\t",
- t->step->n->fn->name,
- t->step->n->ln,
- t->step->seqno);
- comment(stdout, t->step->n, 0);
- printf(";\n");
- }
- #endif
- #endif
- /* t is an isolated eligible step:
- *
- * a merge_start can connect to a proper
- * merge chain or to a merge_single
- * a merge chain can be preceded by
- * a merge_start, but not by a merge_single
- */
- continue;
- }
- (void) build_step(t);
- }
- /* 2nd scan -- find possible merge_starts */
- for (f = fsm; f; f = f->nxt) /* all states */
- for (t = f->t; t; t = t->nxt) /* all edges */
- { if (!t->step || t->step->merge)
- continue;
- lt = t->step->n;
- #if 0
- 4.1.3:
- an rv send operation inside an atomic, *loses* atomicity
- when executed
- and should therefore never be merged with a subsequent
- statement within the atomic sequence
- the same is not true for non-rv send operations
- #endif
- if (lt->ntyp == 'c' /* potentially blocking stmnts */
- || lt->ntyp == 'r'
- || (lt->ntyp == 's' && u_sync == 0)) /* added !u_sync in 4.1.3 */
- { if (!canfill_in(t)) /* atomic, non-global, etc. */
- continue;
- g = fsm_tbl[t->to];
- if (!g || !g->t || !g->t->step)
- continue;
- if (g->t->step->merge)
- t->step->merge_start = g->t->step->merge;
- #ifdef SINGLES
- else if (g->t->step->merge_single)
- t->step->merge_start = g->t->step->merge_single;
- #endif
- #if 0
- if ((verbose&32)
- && t->step->merge_start)
- { printf("spin: %s, line %3d, merge_START:\n\t<seqno %d>\t",
- lt->fn->name,
- lt->ln,
- t->step->seqno);
- comment(stdout, lt, 0);
- printf(";\n");
- }
- #endif
- }
- }
- }
- static void
- FSM_ANA(void)
- { FSM_state *f;
- FSM_trans *t;
- FSM_use *u, *v, *w;
- int n;
- for (f = fsm; f; f = f->nxt) /* all states */
- for (t = f->t; t; t = t->nxt) /* all edges */
- for (n = 0; n < 2; n++) /* reads and writes */
- for (u = t->Val[n]; u; u = u->nxt)
- { if (!u->var->context /* global */
- || u->var->type == CHAN
- || u->var->type == STRUCT)
- continue;
- new_dfs();
- if (FSM_DFS(t->to, u)) /* cannot hit read before hitting write */
- u->special = n+1; /* means, reset to 0 after use */
- }
- if (!export_ast)
- for (f = fsm; f; f = f->nxt)
- for (t = f->t; t; t = t->nxt)
- for (n = 0; n < 2; n++)
- for (u = t->Val[n], w = (FSM_use *) 0; u; )
- { if (u->special)
- { v = u->nxt;
- if (!w) /* remove from list */
- t->Val[n] = v;
- else
- w->nxt = v;
- #if q
- if (verbose&32)
- { printf("%s : %3d: %d -> %d \t",
- t->step->n->fn->name,
- t->step->n->ln,
- f->from,
- t->to);
- comment(stdout, t->step->n, 0);
- printf("\t%c%d: %s\n", n==0?'R':'L',
- u->special, u->var->name);
- }
- #endif
- if (good_dead(t->step, u))
- { u->nxt = t->step->dead; /* insert into dead */
- t->step->dead = u;
- }
- u = v;
- } else
- { w = u;
- u = u->nxt;
- } }
- }
- void
- rel_use(FSM_use *u)
- {
- if (!u) return;
- rel_use(u->nxt);
- u->var = (Symbol *) 0;
- u->special = 0;
- u->nxt = use_free;
- use_free = u;
- }
- static void
- rel_trans(FSM_trans *t)
- {
- if (!t) return;
- rel_trans(t->nxt);
- rel_use(t->Val[0]);
- rel_use(t->Val[1]);
- t->Val[0] = t->Val[1] = (FSM_use *) 0;
- t->nxt = trans_free;
- trans_free = t;
- }
- static void
- rel_state(FSM_state *f)
- {
- if (!f) return;
- rel_state(f->nxt);
- rel_trans(f->t);
- f->t = (FSM_trans *) 0;
- f->nxt = fsm_free;
- fsm_free = f;
- }
- static void
- FSM_DEL(void)
- {
- rel_state(fsm);
- fsm = (FSM_state *) 0;
- }
- static FSM_state *
- mkstate(int s)
- { FSM_state *f;
- /* fsm_tbl isn't allocated yet */
- for (f = fsm; f; f = f->nxt)
- if (f->from == s)
- break;
- if (!f)
- { if (fsm_free)
- { f = fsm_free;
- memset(f, 0, sizeof(FSM_state));
- fsm_free = fsm_free->nxt;
- } else
- f = (FSM_state *) emalloc(sizeof(FSM_state));
- f->from = s;
- f->t = (FSM_trans *) 0;
- f->nxt = fsm;
- fsm = f;
- if (s > max_st_id)
- max_st_id = s;
- }
- return f;
- }
- static FSM_trans *
- get_trans(int to)
- { FSM_trans *t;
- if (trans_free)
- { t = trans_free;
- memset(t, 0, sizeof(FSM_trans));
- trans_free = trans_free->nxt;
- } else
- t = (FSM_trans *) emalloc(sizeof(FSM_trans));
- t->to = to;
- return t;
- }
- static void
- FSM_EDGE(int from, int to, Element *e)
- { FSM_state *f;
- FSM_trans *t;
- f = mkstate(from); /* find it or else make it */
- t = get_trans(to);
- t->step = e;
- t->nxt = f->t;
- f->t = t;
- f = mkstate(to);
- f->in++;
- if (export_ast)
- { t = get_trans(from);
- t->step = e;
- t->nxt = f->p; /* from is a predecessor of to */
- f->p = t;
- }
- if (t->step)
- ana_stmnt(t, t->step->n, 0);
- }
- #define LVAL 1
- #define RVAL 0
- static void
- ana_var(FSM_trans *t, Lextok *now, int usage)
- { FSM_use *u, *v;
- if (!t || !now || !now->sym)
- return;
- if (now->sym->name[0] == '_'
- && (strcmp(now->sym->name, "_") == 0
- || strcmp(now->sym->name, "_pid") == 0
- || strcmp(now->sym->name, "_last") == 0))
- return;
- v = t->Val[usage];
- for (u = v; u; u = u->nxt)
- if (u->var == now->sym)
- return; /* it's already there */
- if (!now->lft)
- { /* not for array vars -- it's hard to tell statically
- if the index would, at runtime, evaluate to the
- same values at lval and rval references
- */
- if (use_free)
- { u = use_free;
- use_free = use_free->nxt;
- } else
- u = (FSM_use *) emalloc(sizeof(FSM_use));
-
- u->var = now->sym;
- u->nxt = t->Val[usage];
- t->Val[usage] = u;
- } else
- ana_stmnt(t, now->lft, RVAL); /* index */
- if (now->sym->type == STRUCT
- && now->rgt
- && now->rgt->lft)
- ana_var(t, now->rgt->lft, usage);
- }
- static void
- ana_stmnt(FSM_trans *t, Lextok *now, int usage)
- { Lextok *v;
- if (!t || !now) return;
- switch (now->ntyp) {
- case '.':
- case BREAK:
- case GOTO:
- case CONST:
- case TIMEOUT:
- case NONPROGRESS:
- case ELSE:
- case '@':
- case 'q':
- case IF:
- case DO:
- case ATOMIC:
- case NON_ATOMIC:
- case D_STEP:
- case C_CODE:
- case C_EXPR:
- break;
- case '!':
- case UMIN:
- case '~':
- case ENABLED:
- case PC_VAL:
- case LEN:
- case FULL:
- case EMPTY:
- case NFULL:
- case NEMPTY:
- case ASSERT:
- case 'c':
- ana_stmnt(t, now->lft, RVAL);
- break;
- case '/':
- case '*':
- case '-':
- case '+':
- case '%':
- case '&':
- case '^':
- case '|':
- case LT:
- case GT:
- case LE:
- case GE:
- case NE:
- case EQ:
- case OR:
- case AND:
- case LSHIFT:
- case RSHIFT:
- ana_stmnt(t, now->lft, RVAL);
- ana_stmnt(t, now->rgt, RVAL);
- break;
- case ASGN:
- ana_stmnt(t, now->lft, LVAL);
- ana_stmnt(t, now->rgt, RVAL);
- break;
- case PRINT:
- case RUN:
- for (v = now->lft; v; v = v->rgt)
- ana_stmnt(t, v->lft, RVAL);
- break;
- case PRINTM:
- if (now->lft && !now->lft->ismtyp)
- ana_stmnt(t, now->lft, RVAL);
- break;
- case 's':
- ana_stmnt(t, now->lft, RVAL);
- for (v = now->rgt; v; v = v->rgt)
- ana_stmnt(t, v->lft, RVAL);
- break;
- case 'R':
- case 'r':
- ana_stmnt(t, now->lft, RVAL);
- for (v = now->rgt; v; v = v->rgt)
- { if (v->lft->ntyp == EVAL)
- ana_stmnt(t, v->lft->lft, RVAL);
- else
- if (v->lft->ntyp != CONST
- && now->ntyp != 'R') /* was v->lft->ntyp */
- ana_stmnt(t, v->lft, LVAL);
- }
- break;
- case '?':
- ana_stmnt(t, now->lft, RVAL);
- if (now->rgt)
- { ana_stmnt(t, now->rgt->lft, RVAL);
- ana_stmnt(t, now->rgt->rgt, RVAL);
- }
- break;
- case NAME:
- ana_var(t, now, usage);
- break;
- case 'p': /* remote ref */
- ana_stmnt(t, now->lft->lft, RVAL); /* process id */
- ana_var(t, now, RVAL);
- ana_var(t, now->rgt, RVAL);
- break;
- default:
- printf("spin: bad node type %d line %d (ana_stmnt)\n", now->ntyp, now->ln);
- fatal("aborting", (char *) 0);
- }
- }
- void
- ana_src(int dataflow, int merger) /* called from main.c and guided.c */
- { ProcList *p;
- Element *e;
- #if 0
- int counter = 1;
- #endif
- for (p = rdy; p; p = p->nxt)
- { if (p->tn == eventmapnr
- || p->tn == claimnr)
- continue;
- ana_seq(p->s);
- fsm_table();
- e = p->s->frst;
- #if 0
- if (dataflow || merger)
- { printf("spin: %d, optimizing '%s'",
- counter++, p->n->name);
- fflush(stdout);
- }
- #endif
- if (dataflow)
- { FSM_ANA();
- }
- if (merger)
- { FSM_MERGER(p->n->name);
- huntele(e, e->status, -1)->merge_in = 1; /* start-state */
- #if 0
- printf("\n");
- #endif
- }
- if (export_ast)
- AST_store(p, huntele(e, e->status, -1)->seqno);
- FSM_DEL();
- }
- for (e = Al_El; e; e = e->Nxt)
- {
- if (!(e->status&DONE) && (verbose&32))
- { printf("unreachable code: ");
- printf("%s, line %3d: ",
- e->n->fn->name, e->n->ln);
- comment(stdout, e->n, 0);
- printf("\n");
- }
- e->status &= ~DONE;
- }
- if (export_ast)
- { AST_slice();
- exit(0);
- }
- }
- void
- spit_recvs(FILE *f1, FILE *f2) /* called from pangen2.c */
- { Element *e;
- Sequence *s;
- extern int Unique;
- fprintf(f1, "unsigned char Is_Recv[%d];\n", Unique);
- fprintf(f2, "void\nset_recvs(void)\n{\n");
- for (e = Al_El; e; e = e->Nxt)
- { if (!e->n) continue;
- switch (e->n->ntyp) {
- case 'r':
- markit: fprintf(f2, "\tIs_Recv[%d] = 1;\n", e->Seqno);
- break;
- case D_STEP:
- s = e->n->sl->this;
- switch (s->frst->n->ntyp) {
- case DO:
- fatal("unexpected: do at start of d_step", (char *) 0);
- case IF: /* conservative: fall through */
- case 'r': goto markit;
- }
- break;
- }
- }
- fprintf(f2, "}\n");
- if (rvopt)
- {
- fprintf(f2, "int\nno_recvs(int me)\n{\n");
- fprintf(f2, " int h; uchar ot; short tt;\n");
- fprintf(f2, " Trans *t;\n");
- fprintf(f2, " for (h = BASE; h < (int) now._nr_pr; h++)\n");
- fprintf(f2, " { if (h == me) continue;\n");
- fprintf(f2, " tt = (short) ((P0 *)pptr(h))->_p;\n");
- fprintf(f2, " ot = (uchar) ((P0 *)pptr(h))->_t;\n");
- fprintf(f2, " for (t = trans[ot][tt]; t; t = t->nxt)\n");
- fprintf(f2, " if (Is_Recv[t->t_id]) return 0;\n");
- fprintf(f2, " }\n");
- fprintf(f2, " return 1;\n");
- fprintf(f2, "}\n");
- }
- }
- static void
- ana_seq(Sequence *s)
- { SeqList *h;
- Sequence *t;
- Element *e, *g;
- int From, To;
- for (e = s->frst; e; e = e->nxt)
- { if (e->status & DONE)
- goto checklast;
- e->status |= DONE;
- From = e->seqno;
- if (e->n->ntyp == UNLESS)
- ana_seq(e->sub->this);
- else if (e->sub)
- { for (h = e->sub; h; h = h->nxt)
- { g = huntstart(h->this->frst);
- To = g->seqno;
- if (g->n->ntyp != 'c'
- || g->n->lft->ntyp != CONST
- || g->n->lft->val != 0
- || g->esc)
- FSM_EDGE(From, To, e);
- /* else it's a dead link */
- }
- for (h = e->sub; h; h = h->nxt)
- ana_seq(h->this);
- } else if (e->n->ntyp == ATOMIC
- || e->n->ntyp == D_STEP
- || e->n->ntyp == NON_ATOMIC)
- {
- t = e->n->sl->this;
- g = huntstart(t->frst);
- t->last->nxt = e->nxt;
- To = g->seqno;
- FSM_EDGE(From, To, e);
- ana_seq(t);
- } else
- { if (e->n->ntyp == GOTO)
- { g = get_lab(e->n, 1);
- g = huntele(g, e->status, -1);
- To = g->seqno;
- } else if (e->nxt)
- { g = huntele(e->nxt, e->status, -1);
- To = g->seqno;
- } else
- To = 0;
- FSM_EDGE(From, To, e);
- if (e->esc
- && e->n->ntyp != GOTO
- && e->n->ntyp != '.')
- for (h = e->esc; h; h = h->nxt)
- { g = huntstart(h->this->frst);
- To = g->seqno;
- FSM_EDGE(From, To, ZE);
- ana_seq(h->this);
- }
- }
- checklast: if (e == s->last)
- break;
- }
- }
|