123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412 |
- /***** spin: dstep.c *****/
- /* Copyright (c) 1989-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"
- #ifdef PC
- #include "y_tab.h"
- #else
- #include "y.tab.h"
- #endif
- #define MAXDSTEP 1024 /* was 512 */
- char *NextLab[64];
- int Level=0, GenCode=0, IsGuard=0, TestOnly=0;
- static int Tj=0, Jt=0, LastGoto=0;
- static int Tojump[MAXDSTEP], Jumpto[MAXDSTEP], Special[MAXDSTEP];
- static void putCode(FILE *, Element *, Element *, Element *, int);
- extern int Pid, claimnr, separate, OkBreak;
- static void
- Sourced(int n, int special)
- { int i;
- for (i = 0; i < Tj; i++)
- if (Tojump[i] == n)
- return;
- if (Tj >= MAXDSTEP)
- fatal("d_step sequence too long", (char *)0);
- Special[Tj] = special;
- Tojump[Tj++] = n;
- }
- static void
- Dested(int n)
- { int i;
- for (i = 0; i < Tj; i++)
- if (Tojump[i] == n)
- return;
- for (i = 0; i < Jt; i++)
- if (Jumpto[i] == n)
- return;
- if (Jt >= MAXDSTEP)
- fatal("d_step sequence too long", (char *)0);
- Jumpto[Jt++] = n;
- LastGoto = 1;
- }
- static void
- Mopup(FILE *fd)
- { int i, j;
- for (i = 0; i < Jt; i++)
- { for (j = 0; j < Tj; j++)
- if (Tojump[j] == Jumpto[i])
- break;
- if (j == Tj)
- { char buf[12];
- if (Jumpto[i] == OkBreak)
- { if (!LastGoto)
- fprintf(fd, "S_%.3d_0: /* break-dest */\n",
- OkBreak);
- } else {
- sprintf(buf, "S_%.3d_0", Jumpto[i]);
- non_fatal("goto %s breaks from d_step seq", buf);
- } } }
- for (j = 0; j < Tj; j++)
- { for (i = 0; i < Jt; i++)
- if (Tojump[j] == Jumpto[i])
- break;
- #ifdef DEBUG
- if (i == Jt && !Special[i])
- fprintf(fd, "\t\t/* no goto's to S_%.3d_0 */\n",
- Tojump[j]);
- #endif
- }
- for (j = i = 0; j < Tj; j++)
- if (Special[j])
- { Tojump[i] = Tojump[j];
- Special[i] = 2;
- if (i >= MAXDSTEP)
- fatal("cannot happen (dstep.c)", (char *)0);
- i++;
- }
- Tj = i; /* keep only the global exit-labels */
- Jt = 0;
- }
- static int
- FirstTime(int n)
- { int i;
- for (i = 0; i < Tj; i++)
- if (Tojump[i] == n)
- return (Special[i] <= 1);
- return 1;
- }
- static void
- illegal(Element *e, char *str)
- {
- printf("illegal operator in 'd_step:' '");
- comment(stdout, e->n, 0);
- printf("'\n");
- fatal("'%s'", str);
- }
- static void
- filterbad(Element *e)
- {
- switch (e->n->ntyp) {
- case ASSERT:
- case PRINT:
- case 'c':
- /* run cannot be completely undone
- * with sv_save-sv_restor
- */
- if (any_oper(e->n->lft, RUN))
- illegal(e, "run operator in d_step");
- /* remote refs inside d_step sequences
- * would be okay, but they cannot always
- * be interpreted by the simulator the
- * same as by the verifier (e.g., for an
- * error trail)
- */
- if (any_oper(e->n->lft, 'p'))
- illegal(e, "remote reference in d_step");
- break;
- case '@':
- illegal(e, "process termination");
- break;
- case D_STEP:
- illegal(e, "nested d_step sequence");
- break;
- case ATOMIC:
- illegal(e, "nested atomic sequence");
- break;
- default:
- break;
- }
- }
- static int
- CollectGuards(FILE *fd, Element *e, int inh)
- { SeqList *h; Element *ee;
- for (h = e->sub; h; h = h->nxt)
- { ee = huntstart(h->this->frst);
- filterbad(ee);
- switch (ee->n->ntyp) {
- case NON_ATOMIC:
- inh += CollectGuards(fd, ee->n->sl->this->frst, inh);
- break;
- case IF:
- inh += CollectGuards(fd, ee, inh);
- break;
- case '.':
- if (ee->nxt->n->ntyp == DO)
- inh += CollectGuards(fd, ee->nxt, inh);
- break;
- case ELSE:
- if (inh++ > 0) fprintf(fd, " || ");
- fprintf(fd, "(1 /* else */)");
- break;
- case 'R':
- if (inh++ > 0) fprintf(fd, " || ");
- fprintf(fd, "("); TestOnly=1;
- putstmnt(fd, ee->n, ee->seqno);
- fprintf(fd, ")"); TestOnly=0;
- break;
- case 'r':
- if (inh++ > 0) fprintf(fd, " || ");
- fprintf(fd, "("); TestOnly=1;
- putstmnt(fd, ee->n, ee->seqno);
- fprintf(fd, ")"); TestOnly=0;
- break;
- case 's':
- if (inh++ > 0) fprintf(fd, " || ");
- fprintf(fd, "("); TestOnly=1;
- /* 4.2.1 */ if (Pid != claimnr) fprintf(fd, "(boq == -1) && ");
- putstmnt(fd, ee->n, ee->seqno);
- fprintf(fd, ")"); TestOnly=0;
- break;
- case 'c':
- if (inh++ > 0) fprintf(fd, " || ");
- fprintf(fd, "("); TestOnly=1;
- if (Pid != claimnr)
- fprintf(fd, "(boq == -1 && ");
- putstmnt(fd, ee->n->lft, e->seqno);
- if (Pid != claimnr)
- fprintf(fd, ")");
- fprintf(fd, ")"); TestOnly=0;
- break;
- } }
- return inh;
- }
- int
- putcode(FILE *fd, Sequence *s, Element *nxt, int justguards, int ln, int seqno)
- { int isg=0; char buf[64];
- NextLab[0] = "continue";
- filterbad(s->frst);
- switch (s->frst->n->ntyp) {
- case UNLESS:
- non_fatal("'unless' inside d_step - ignored", (char *) 0);
- return putcode(fd, s->frst->n->sl->this, nxt, 0, ln, seqno);
- case NON_ATOMIC:
- (void) putcode(fd, s->frst->n->sl->this, ZE, 1, ln, seqno);
- break;
- case IF:
- fprintf(fd, "if (!(");
- if (!CollectGuards(fd, s->frst, 0)) /* what about boq? */
- fprintf(fd, "1");
- fprintf(fd, "))\n\t\t\tcontinue;");
- isg = 1;
- break;
- case '.':
- if (s->frst->nxt->n->ntyp == DO)
- { fprintf(fd, "if (!(");
- if (!CollectGuards(fd, s->frst->nxt, 0))
- fprintf(fd, "1");
- fprintf(fd, "))\n\t\t\tcontinue;");
- isg = 1;
- }
- break;
- case 'R': /* <- can't really happen (it's part of a 'c') */
- fprintf(fd, "if (!("); TestOnly=1;
- putstmnt(fd, s->frst->n, s->frst->seqno);
- fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
- break;
- case 'r':
- fprintf(fd, "if (!("); TestOnly=1;
- putstmnt(fd, s->frst->n, s->frst->seqno);
- fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
- break;
- case 's':
- fprintf(fd, "if (");
- #if 1
- /* 4.2.1 */ if (Pid != claimnr) fprintf(fd, "(boq != -1) || ");
- #endif
- fprintf(fd, "!("); TestOnly=1;
- putstmnt(fd, s->frst->n, s->frst->seqno);
- fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
- break;
- case 'c':
- fprintf(fd, "if (!(");
- if (Pid != claimnr) fprintf(fd, "boq == -1 && ");
- TestOnly=1;
- putstmnt(fd, s->frst->n->lft, s->frst->seqno);
- fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0;
- break;
- case ELSE:
- fprintf(fd, "if (boq != -1 || (");
- if (separate != 2) fprintf(fd, "trpt->");
- fprintf(fd, "o_pm&1))\n\t\t\tcontinue;");
- break;
- case ASGN: /* new 3.0.8 */
- fprintf(fd, "IfNotBlocked");
- break;
- }
- if (justguards) return 0;
- fprintf(fd, "\n\t\tsv_save();\n\t\t");
- #if 1
- fprintf(fd, "reached[%d][%d] = 1;\n\t\t", Pid, seqno);
- fprintf(fd, "reached[%d][t->st] = 1;\n\t\t", Pid); /* true next state */
- fprintf(fd, "reached[%d][tt] = 1;\n", Pid); /* true current state */
- #endif
- sprintf(buf, "Uerror(\"block in d_step seq, line %d\")", ln);
- NextLab[0] = buf;
- putCode(fd, s->frst, s->extent, nxt, isg);
- if (nxt)
- { extern Symbol *Fname;
- extern int lineno;
- if (FirstTime(nxt->Seqno)
- && (!(nxt->status & DONE2) || !(nxt->status & D_ATOM)))
- { fprintf(fd, "S_%.3d_0: /* 1 */\n", nxt->Seqno);
- nxt->status |= DONE2;
- LastGoto = 0;
- }
- Sourced(nxt->Seqno, 1);
- lineno = ln;
- Fname = nxt->n->fn;
- Mopup(fd);
- }
- unskip(s->frst->seqno);
- return LastGoto;
- }
- static void
- putCode(FILE *fd, Element *f, Element *last, Element *next, int isguard)
- { Element *e, *N;
- SeqList *h; int i;
- char NextOpt[64];
- static int bno = 0;
- for (e = f; e; e = e->nxt)
- { if (e->status & DONE2)
- continue;
- e->status |= DONE2;
- if (!(e->status & D_ATOM))
- { if (!LastGoto)
- { fprintf(fd, "\t\tgoto S_%.3d_0;\n",
- e->Seqno);
- Dested(e->Seqno);
- }
- break;
- }
- fprintf(fd, "S_%.3d_0: /* 2 */\n", e->Seqno);
- LastGoto = 0;
- Sourced(e->Seqno, 0);
- if (!e->sub)
- { filterbad(e);
- switch (e->n->ntyp) {
- case NON_ATOMIC:
- h = e->n->sl;
- putCode(fd, h->this->frst,
- h->this->extent, e->nxt, 0);
- break;
- case BREAK:
- if (LastGoto) break;
- if (e->nxt)
- { i = target( huntele(e->nxt,
- e->status, -1))->Seqno;
- fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
- fprintf(fd, "/* 'break' */\n");
- Dested(i);
- } else
- { if (next)
- { fprintf(fd, "\t\tgoto S_%.3d_0;",
- next->Seqno);
- fprintf(fd, " /* NEXT */\n");
- Dested(next->Seqno);
- } else
- fatal("cannot interpret d_step", 0);
- }
- break;
- case GOTO:
- if (LastGoto) break;
- i = huntele( get_lab(e->n,1),
- e->status, -1)->Seqno;
- fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
- fprintf(fd, "/* 'goto' */\n");
- Dested(i);
- break;
- case '.':
- if (LastGoto) break;
- if (e->nxt && (e->nxt->status & DONE2))
- { i = e->nxt?e->nxt->Seqno:0;
- fprintf(fd, "\t\tgoto S_%.3d_0;", i);
- fprintf(fd, " /* '.' */\n");
- Dested(i);
- }
- break;
- default:
- putskip(e->seqno);
- GenCode = 1; IsGuard = isguard;
- fprintf(fd, "\t\t");
- putstmnt(fd, e->n, e->seqno);
- fprintf(fd, ";\n");
- GenCode = IsGuard = isguard = LastGoto = 0;
- break;
- }
- i = e->nxt?e->nxt->Seqno:0;
- if (e->nxt && e->nxt->status & DONE2 && !LastGoto)
- { fprintf(fd, "\t\tgoto S_%.3d_0; ", i);
- fprintf(fd, "/* ';' */\n");
- Dested(i);
- break;
- }
- } else
- { for (h = e->sub, i=1; h; h = h->nxt, i++)
- { sprintf(NextOpt, "goto S_%.3d_%d",
- e->Seqno, i);
- NextLab[++Level] = NextOpt;
- N = (e->n->ntyp == DO) ? e : e->nxt;
- putCode(fd, h->this->frst,
- h->this->extent, N, 1);
- Level--;
- fprintf(fd, "%s: /* 3 */\n", &NextOpt[5]);
- LastGoto = 0;
- }
- if (!LastGoto)
- { fprintf(fd, "\t\tUerror(\"blocking sel ");
- fprintf(fd, "in d_step (nr.%d, near line %d)\");\n",
- bno++, (e->n)?e->n->ln:0);
- LastGoto = 0;
- }
- }
- if (e == last)
- { if (!LastGoto && next)
- { fprintf(fd, "\t\tgoto S_%.3d_0;\n",
- next->Seqno);
- Dested(next->Seqno);
- }
- break;
- } }
- }
|