12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717817918018118218318418518618718818919019119219319419519619719819920020120220320420520620720820921021121221321421521621721821922022122222322422522622722822923023123223323423523623723823924024124224324424524624724824925025125225325425525625725825926026126226326426526626726826927027127227327427527627727827928028128228328428528628728828929029129229329429529629729829930030130230330430530630730830931031131231331431531631731831932032132232332432532632732832933033133233333433533633733833934034134234334434534634734834935035135235335435535635735835936036136236336436536636736836937037137237337437537637737837938038138238338438538638738838939039139239339439539639739839940040140240340440540640740840941041141241341441541641741841942042142242342442542642742842943043143243343443543643743843944044144244344444544644744844945045145245345445545645745845946046146246346446546646746846947047147247347447547647747847948048148248348448548648748848949049149249349449549649749849950050150250350450550650750850951051151251351451551651751851952052152252352452552652752852953053153253353453553653753853954054154254354454554654754854955055155255355455555655755855956056156256356456556656756856957057157257357457557657757857958058158258358458558658758858959059159259359459559659759859960060160260360460560660760860961061161261361461561661761861962062162262362462562662762862963063163263363463563663763863964064164264364464564664764864965065165265365465565665765865966066166266366466566666766866967067167267367467567667767867968068168268368468568668768868969069169269369469569669769869970070170270370470570670770870971071171271371471571671771871972072172272372472572672772872973073173273373473573673773873974074174274374474574674774874975075175275375475575675775875976076176276376476576676776876977077177277377477577677777877978078178278378478578678778878979079179279379479579679779879980080180280380480580680780880981081181281381481581681781881982082182282382482582682782882983083183283383483583683783883984084184284384484584684784884985085185285385485585685785885986086186286386486586686786886987087187287387487587687787887988088188288388488588688788888989089189289389489589689789889990090190290390490590690790890991091191291391491591691791891992092192292392492592692792892993093193293393493593693793893994094194294394494594694794894995095195295395495595695795895996096196296396496596696796896997097197297397497597697797897998098198298398498598698798898999099199299399499599699799899910001001100210031004100510061007100810091010101110121013101410151016101710181019102010211022102310241025 |
- /***** spin: sched.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 <stdlib.h>
- #include "spin.h"
- #include "y.tab.h"
- extern int verbose, s_trail, analyze, no_wrapup;
- extern char *claimproc, *eventmap, Buf[];
- extern Ordered *all_names;
- extern Symbol *Fname, *context;
- extern int lineno, nr_errs, dumptab, xspin, jumpsteps, columns;
- extern int u_sync, Elcnt, interactive, TstOnly, cutoff;
- extern short has_enabled;
- extern int limited_vis;
- RunList *X = (RunList *) 0;
- RunList *run = (RunList *) 0;
- RunList *LastX = (RunList *) 0; /* previous executing proc */
- ProcList *rdy = (ProcList *) 0;
- Element *LastStep = ZE;
- int nproc=0, nstop=0, Tval=0;
- int Rvous=0, depth=0, nrRdy=0, MadeChoice;
- short Have_claim=0, Skip_claim=0;
- static int Priority_Sum = 0;
- static void setlocals(RunList *);
- static void setparams(RunList *, ProcList *, Lextok *);
- static void talk(RunList *);
- void
- runnable(ProcList *p, int weight, int noparams)
- { RunList *r = (RunList *) emalloc(sizeof(RunList));
- r->n = p->n;
- r->tn = p->tn;
- r->pid = nproc++ - nstop + Skip_claim;
- if ((verbose&4) || (verbose&32))
- printf("Starting %s with pid %d\n", p->n->name, r->pid);
- if (!p->s)
- fatal("parsing error, no sequence %s", p->n?p->n->name:"--");
- r->pc = huntele(p->s->frst, p->s->frst->status, -1);
- r->ps = p->s;
- if (p->s->last)
- p->s->last->status |= ENDSTATE; /* normal end state */
- r->nxt = run;
- r->prov = p->prov;
- r->priority = weight;
- if (noparams) setlocals(r);
- Priority_Sum += weight;
- run = r;
- }
- ProcList *
- ready(Symbol *n, Lextok *p, Sequence *s, int det, Lextok *prov)
- /* n=name, p=formals, s=body det=deterministic prov=provided */
- { ProcList *r = (ProcList *) emalloc(sizeof(ProcList));
- Lextok *fp, *fpt; int j; extern int Npars;
- r->n = n;
- r->p = p;
- r->s = s;
- r->prov = prov;
- r->tn = nrRdy++;
- r->det = (short) det;
- r->nxt = rdy;
- rdy = r;
- for (fp = p, j = 0; fp; fp = fp->rgt)
- for (fpt = fp->lft; fpt; fpt = fpt->rgt)
- j++; /* count # of parameters */
- Npars = max(Npars, j);
- return rdy;
- }
- int
- find_maxel(Symbol *s)
- { ProcList *p;
- for (p = rdy; p; p = p->nxt)
- if (p->n == s)
- return p->s->maxel++;
- return Elcnt++;
- }
- static void
- formdump(void)
- { ProcList *p;
- Lextok *f, *t;
- int cnt;
- for (p = rdy; p; p = p->nxt)
- { if (!p->p) continue;
- cnt = -1;
- for (f = p->p; f; f = f->rgt) /* types */
- for (t = f->lft; t; t = t->rgt) /* formals */
- { if (t->ntyp != ',')
- t->sym->Nid = cnt--; /* overload Nid */
- else
- t->lft->sym->Nid = cnt--;
- }
- }
- }
- void
- announce(char *w)
- {
- if (columns)
- { extern char Buf[];
- extern int firstrow;
- firstrow = 1;
- if (columns == 2)
- { sprintf(Buf, "%d:%s",
- run->pid - Have_claim, run->n->name);
- pstext(run->pid - Have_claim, Buf);
- } else
- printf("proc %d = %s\n",
- run->pid - Have_claim, run->n->name);
- return;
- }
- if (dumptab
- || analyze
- || s_trail
- || !(verbose&4))
- return;
- if (w)
- printf(" 0: proc - (%s) ", w);
- else
- whoruns(1);
- printf("creates proc %2d (%s)",
- run->pid - Have_claim,
- run->n->name);
- if (run->priority > 1)
- printf(" priority %d", run->priority);
- printf("\n");
- }
- #ifndef MAXP
- #define MAXP 255 /* matches max nr of processes in verifier */
- #endif
- int
- enable(Lextok *m)
- { ProcList *p;
- Symbol *s = m->sym; /* proctype name */
- Lextok *n = m->lft; /* actual parameters */
- if (m->val < 1) m->val = 1; /* minimum priority */
- for (p = rdy; p; p = p->nxt)
- if (strcmp(s->name, p->n->name) == 0)
- { if (nproc-nstop >= MAXP)
- { printf("spin: too many processes (%d max)\n", MAXP);
- break;
- }
- runnable(p, m->val, 0);
- announce((char *) 0);
- setparams(run, p, n);
- setlocals(run); /* after setparams */
- return run->pid - Have_claim + Skip_claim; /* effective simu pid */
- }
- return 0; /* process not found */
- }
- void
- check_param_count(int i, Lextok *m)
- { ProcList *p;
- Symbol *s = m->sym; /* proctype name */
- Lextok *f, *t; /* formal pars */
- int cnt = 0;
- for (p = rdy; p; p = p->nxt)
- { if (strcmp(s->name, p->n->name) == 0)
- { if (m->lft) /* actual param list */
- { lineno = m->lft->ln;
- Fname = m->lft->fn;
- }
- for (f = p->p; f; f = f->rgt) /* one type at a time */
- for (t = f->lft; t; t = t->rgt) /* count formal params */
- { cnt++;
- }
- if (i != cnt)
- { printf("spin: saw %d parameters, expected %d\n", i, cnt);
- non_fatal("wrong number of parameters", "");
- }
- break;
- } }
- }
- void
- start_claim(int n)
- { ProcList *p;
- RunList *r, *q = (RunList *) 0;
- for (p = rdy; p; p = p->nxt)
- if (p->tn == n
- && strcmp(p->n->name, ":never:") == 0)
- { runnable(p, 1, 1);
- goto found;
- }
- printf("spin: couldn't find claim (ignored)\n");
- Skip_claim = 1;
- goto done;
- found:
- /* move claim to far end of runlist, and reassign it pid 0 */
- if (columns == 2)
- { depth = 0;
- pstext(0, "0::never:");
- for (r = run; r; r = r->nxt)
- { if (!strcmp(r->n->name, ":never:"))
- continue;
- sprintf(Buf, "%d:%s",
- r->pid+1, r->n->name);
- pstext(r->pid+1, Buf);
- } }
- if (run->pid == 0) return; /* it is the first process started */
- q = run; run = run->nxt;
- q->pid = 0; q->nxt = (RunList *) 0; /* remove */
- done:
- Have_claim = 1;
- for (r = run; r; r = r->nxt)
- { r->pid = r->pid+Have_claim; /* adjust */
- if (!r->nxt)
- { r->nxt = q;
- break;
- } }
- }
- int
- f_pid(char *n)
- { RunList *r;
- int rval = -1;
- for (r = run; r; r = r->nxt)
- if (strcmp(n, r->n->name) == 0)
- { if (rval >= 0)
- { printf("spin: remote ref to proctype %s, ", n);
- printf("has more than one match: %d and %d\n",
- rval, r->pid);
- } else
- rval = r->pid;
- }
- return rval;
- }
- void
- wrapup(int fini)
- {
- limited_vis = 0;
- if (columns)
- { extern void putpostlude(void);
- if (columns == 2) putpostlude();
- if (!no_wrapup)
- printf("-------------\nfinal state:\n-------------\n");
- }
- if (no_wrapup)
- goto short_cut;
- if (nproc != nstop)
- { int ov = verbose;
- printf("#processes: %d\n", nproc-nstop - Have_claim + Skip_claim);
- verbose &= ~4;
- dumpglobals();
- verbose = ov;
- verbose &= ~1; /* no more globals */
- verbose |= 32; /* add process states */
- for (X = run; X; X = X->nxt)
- talk(X);
- verbose = ov; /* restore */
- }
- printf("%d process%s created\n",
- nproc - Have_claim + Skip_claim,
- (xspin || nproc!=1)?"es":"");
- short_cut:
- if (xspin) alldone(0); /* avoid an abort from xspin */
- if (fini) alldone(1);
- }
- static char is_blocked[256];
- static int
- p_blocked(int p)
- { int i, j;
- is_blocked[p%256] = 1;
- for (i = j = 0; i < nproc - nstop; i++)
- j += is_blocked[i];
- if (j >= nproc - nstop)
- { memset(is_blocked, 0, 256);
- return 1;
- }
- return 0;
- }
- static Element *
- silent_moves(Element *e)
- { Element *f;
- if (e->n)
- switch (e->n->ntyp) {
- case GOTO:
- if (Rvous) break;
- f = get_lab(e->n, 1);
- cross_dsteps(e->n, f->n);
- return f; /* guard against goto cycles */
- case UNLESS:
- return silent_moves(e->sub->this->frst);
- case NON_ATOMIC:
- case ATOMIC:
- case D_STEP:
- e->n->sl->this->last->nxt = e->nxt;
- return silent_moves(e->n->sl->this->frst);
- case '.':
- return silent_moves(e->nxt);
- }
- return e;
- }
- static RunList *
- pickproc(RunList *Y)
- { SeqList *z; Element *has_else;
- short Choices[256];
- int j, k, nr_else = 0;
- if (nproc <= nstop+1)
- { X = run;
- return NULL;
- }
- if (!interactive || depth < jumpsteps)
- { /* was: j = (int) Rand()%(nproc-nstop); */
- if (Priority_Sum < nproc-nstop)
- fatal("cannot happen - weights", (char *)0);
- j = (int) Rand()%Priority_Sum;
- while (j - X->priority >= 0)
- { j -= X->priority;
- Y = X;
- X = X->nxt;
- if (!X) { Y = NULL; X = run; }
- }
- } else
- { int only_choice = -1;
- int no_choice = 0, proc_no_ch, proc_k;
- Tval = 0; /* new 4.2.6 */
- try_again: printf("Select a statement\n");
- try_more: for (X = run, k = 1; X; X = X->nxt)
- { if (X->pid > 255) break;
- Choices[X->pid] = (short) k;
- if (!X->pc
- || (X->prov && !eval(X->prov)))
- { if (X == run)
- Choices[X->pid] = 0;
- continue;
- }
- X->pc = silent_moves(X->pc);
- if (!X->pc->sub && X->pc->n)
- { int unex;
- unex = !Enabled0(X->pc);
- if (unex)
- no_choice++;
- else
- only_choice = k;
- if (!xspin && unex && !(verbose&32))
- { k++;
- continue;
- }
- printf("\tchoice %d: ", k++);
- p_talk(X->pc, 0);
- if (unex)
- printf(" unexecutable,");
- printf(" [");
- comment(stdout, X->pc->n, 0);
- if (X->pc->esc) printf(" + Escape");
- printf("]\n");
- } else {
- has_else = ZE;
- proc_no_ch = no_choice;
- proc_k = k;
- for (z = X->pc->sub, j=0; z; z = z->nxt)
- { Element *y = silent_moves(z->this->frst);
- int unex;
- if (!y) continue;
- if (y->n->ntyp == ELSE)
- { has_else = (Rvous)?ZE:y;
- nr_else = k++;
- continue;
- }
- unex = !Enabled0(y);
- if (unex)
- no_choice++;
- else
- only_choice = k;
- if (!xspin && unex && !(verbose&32))
- { k++;
- continue;
- }
- printf("\tchoice %d: ", k++);
- p_talk(X->pc, 0);
- if (unex)
- printf(" unexecutable,");
- printf(" [");
- comment(stdout, y->n, 0);
- printf("]\n");
- }
- if (has_else)
- { if (no_choice-proc_no_ch >= (k-proc_k)-1)
- { only_choice = nr_else;
- printf("\tchoice %d: ", nr_else);
- p_talk(X->pc, 0);
- printf(" [else]\n");
- } else
- { no_choice++;
- printf("\tchoice %d: ", nr_else);
- p_talk(X->pc, 0);
- printf(" unexecutable, [else]\n");
- } }
- } }
- X = run;
- if (k - no_choice < 2 && Tval == 0)
- { Tval = 1;
- no_choice = 0; only_choice = -1;
- goto try_more;
- }
- if (xspin)
- printf("Make Selection %d\n\n", k-1);
- else
- { if (k - no_choice < 2)
- { printf("no executable choices\n");
- alldone(0);
- }
- printf("Select [1-%d]: ", k-1);
- }
- if (!xspin && k - no_choice == 2)
- { printf("%d\n", only_choice);
- j = only_choice;
- } else
- { char buf[256];
- fflush(stdout);
- scanf("%s", buf);
- j = -1;
- if (isdigit(buf[0]))
- j = atoi(buf);
- else
- { if (buf[0] == 'q')
- alldone(0);
- }
- if (j < 1 || j >= k)
- { printf("\tchoice is outside range\n");
- goto try_again;
- } }
- MadeChoice = 0;
- Y = NULL;
- for (X = run; X; Y = X, X = X->nxt)
- { if (!X->nxt
- || X->nxt->pid > 255
- || j < Choices[X->nxt->pid])
- {
- MadeChoice = 1+j-Choices[X->pid];
- break;
- } }
- }
- return Y;
- }
- void
- sched(void)
- { Element *e;
- RunList *Y = NULL; /* previous process in run queue */
- RunList *oX;
- int go, notbeyond = 0;
- #ifdef PC
- int bufmax = 100;
- #endif
- if (dumptab)
- { formdump();
- symdump();
- dumplabels();
- return;
- }
- if (has_enabled && u_sync > 0)
- { printf("spin: error, cannot use 'enabled()' in ");
- printf("models with synchronous channels.\n");
- nr_errs++;
- }
- if (analyze)
- { gensrc();
- return;
- } else if (s_trail)
- { match_trail();
- return;
- }
- if (claimproc)
- printf("warning: never claim not used in random simulation\n");
- if (eventmap)
- printf("warning: trace assertion not used in random simulation\n");
- X = run;
- Y = pickproc(Y);
- while (X)
- { context = X->n;
- if (X->pc && X->pc->n)
- { lineno = X->pc->n->ln;
- Fname = X->pc->n->fn;
- }
- if (cutoff > 0 && depth >= cutoff)
- { printf("-------------\n");
- printf("depth-limit (-u%d steps) reached\n", cutoff);
- break;
- }
- #ifdef PC
- if (xspin && !interactive && --bufmax <= 0)
- { int c; /* avoid buffer overflow on pc's */
- printf("spin: type return to proceed\n");
- fflush(stdout);
- c = getc(stdin);
- if (c == 'q') wrapup(0);
- bufmax = 100;
- }
- #endif
- depth++; LastStep = ZE;
- oX = X; /* a rendezvous could change it */
- go = 1;
- if (X && X->prov && X->pc
- && !(X->pc->status & D_ATOM)
- && !eval(X->prov))
- { if (!xspin && ((verbose&32) || (verbose&4)))
- { p_talk(X->pc, 1);
- printf("\t<<Not Enabled>>\n");
- }
- go = 0;
- }
- if (go && (e = eval_sub(X->pc)))
- { if (depth >= jumpsteps
- && ((verbose&32) || (verbose&4)))
- { if (X == oX)
- if (!(e->status & D_ATOM) || (verbose&32)) /* no talking in d_steps */
- { p_talk(X->pc, 1);
- printf(" [");
- if (!LastStep) LastStep = X->pc;
- comment(stdout, LastStep->n, 0);
- printf("]\n");
- }
- if (verbose&1) dumpglobals();
- if (verbose&2) dumplocal(X);
- if (!(e->status & D_ATOM))
- if (xspin)
- printf("\n");
- }
- if (oX != X)
- { e = silent_moves(e);
- notbeyond = 0;
- }
- oX->pc = e; LastX = X;
- if (!interactive) Tval = 0;
- memset(is_blocked, 0, 256);
- if (X->pc && (X->pc->status & (ATOM|L_ATOM))
- && (notbeyond == 0 || oX != X))
- { if ((X->pc->status & L_ATOM))
- notbeyond = 1;
- continue; /* no process switch */
- }
- } else
- { depth--;
- if (oX->pc->status & D_ATOM)
- non_fatal("stmnt in d_step blocks", (char *)0);
- if (X->pc->n->ntyp == '@'
- && X->pid == (nproc-nstop-1))
- { if (X != run && Y != NULL)
- Y->nxt = X->nxt;
- else
- run = X->nxt;
- nstop++;
- Priority_Sum -= X->priority;
- if (verbose&4)
- { whoruns(1);
- dotag(stdout, "terminates\n");
- }
- LastX = X;
- if (!interactive) Tval = 0;
- if (nproc == nstop) break;
- memset(is_blocked, 0, 256);
- /* proc X is no longer in runlist */
- X = (X->nxt) ? X->nxt : run;
- } else
- { if (p_blocked(X->pid))
- { if (Tval) break;
- Tval = 1;
- if (depth >= jumpsteps)
- { oX = X;
- X = (RunList *) 0; /* to suppress indent */
- dotag(stdout, "timeout\n");
- X = oX;
- } } } }
- Y = pickproc(X);
- notbeyond = 0;
- }
- context = ZS;
- wrapup(0);
- }
- int
- complete_rendez(void)
- { RunList *orun = X, *tmp;
- Element *s_was = LastStep;
- Element *e;
- int j, ointer = interactive;
- if (s_trail)
- return 1;
- if (orun->pc->status & D_ATOM)
- fatal("rv-attempt in d_step sequence", (char *)0);
- Rvous = 1;
- interactive = 0;
- j = (int) Rand()%Priority_Sum; /* randomize start point */
- X = run;
- while (j - X->priority >= 0)
- { j -= X->priority;
- X = X->nxt;
- if (!X) X = run;
- }
- for (j = nproc - nstop; j > 0; j--)
- { if (X != orun
- && (!X->prov || eval(X->prov))
- && (e = eval_sub(X->pc)))
- { if (TstOnly)
- { X = orun;
- Rvous = 0;
- goto out;
- }
- if ((verbose&32) || (verbose&4))
- { tmp = orun; orun = X; X = tmp;
- if (!s_was) s_was = X->pc;
- p_talk(s_was, 1);
- printf(" [");
- comment(stdout, s_was->n, 0);
- printf("]\n");
- tmp = orun; orun = X; X = tmp;
- if (!LastStep) LastStep = X->pc;
- p_talk(LastStep, 1);
- printf(" [");
- comment(stdout, LastStep->n, 0);
- printf("]\n");
- }
- Rvous = 0; /* before silent_moves */
- X->pc = silent_moves(e);
- out: interactive = ointer;
- return 1;
- }
- X = X->nxt;
- if (!X) X = run;
- }
- Rvous = 0;
- X = orun;
- interactive = ointer;
- return 0;
- }
- /***** Runtime - Local Variables *****/
- static void
- addsymbol(RunList *r, Symbol *s)
- { Symbol *t;
- int i;
- for (t = r->symtab; t; t = t->next)
- if (strcmp(t->name, s->name) == 0)
- return; /* it's already there */
- t = (Symbol *) emalloc(sizeof(Symbol));
- t->name = s->name;
- t->type = s->type;
- t->hidden = s->hidden;
- t->nbits = s->nbits;
- t->nel = s->nel;
- t->ini = s->ini;
- t->setat = depth;
- t->context = r->n;
- if (s->type != STRUCT)
- { if (s->val) /* if already initialized, copy info */
- { t->val = (int *) emalloc(s->nel*sizeof(int));
- for (i = 0; i < s->nel; i++)
- t->val[i] = s->val[i];
- } else
- (void) checkvar(t, 0); /* initialize it */
- } else
- { if (s->Sval)
- fatal("saw preinitialized struct %s", s->name);
- t->Slst = s->Slst;
- t->Snm = s->Snm;
- t->owner = s->owner;
- /* t->context = r->n; */
- }
- t->next = r->symtab; /* add it */
- r->symtab = t;
- }
- static void
- setlocals(RunList *r)
- { Ordered *walk;
- Symbol *sp;
- RunList *oX = X;
- X = r;
- for (walk = all_names; walk; walk = walk->next)
- { sp = walk->entry;
- if (sp
- && sp->context
- && strcmp(sp->context->name, r->n->name) == 0
- && sp->Nid >= 0
- && (sp->type == UNSIGNED
- || sp->type == BIT
- || sp->type == MTYPE
- || sp->type == BYTE
- || sp->type == CHAN
- || sp->type == SHORT
- || sp->type == INT
- || sp->type == STRUCT))
- { if (!findloc(sp))
- non_fatal("setlocals: cannot happen '%s'",
- sp->name);
- }
- }
- X = oX;
- }
- static void
- oneparam(RunList *r, Lextok *t, Lextok *a, ProcList *p)
- { int k; int at, ft;
- RunList *oX = X;
- if (!a)
- fatal("missing actual parameters: '%s'", p->n->name);
- if (t->sym->nel != 1)
- fatal("array in parameter list, %s", t->sym->name);
- k = eval(a->lft);
- at = Sym_typ(a->lft);
- X = r; /* switch context */
- ft = Sym_typ(t);
- if (at != ft && (at == CHAN || ft == CHAN))
- { char buf[128], tag1[64], tag2[64];
- (void) sputtype(tag1, ft);
- (void) sputtype(tag2, at);
- sprintf(buf, "type-clash in params of %s(..), (%s<-> %s)",
- p->n->name, tag1, tag2);
- non_fatal("%s", buf);
- }
- t->ntyp = NAME;
- addsymbol(r, t->sym);
- (void) setval(t, k);
-
- X = oX;
- }
- static void
- setparams(RunList *r, ProcList *p, Lextok *q)
- { Lextok *f, *a; /* formal and actual pars */
- Lextok *t; /* list of pars of 1 type */
- if (q)
- { lineno = q->ln;
- Fname = q->fn;
- }
- for (f = p->p, a = q; f; f = f->rgt) /* one type at a time */
- for (t = f->lft; t; t = t->rgt, a = (a)?a->rgt:a)
- { if (t->ntyp != ',')
- oneparam(r, t, a, p); /* plain var */
- else
- oneparam(r, t->lft, a, p); /* expanded struct */
- }
- }
- Symbol *
- findloc(Symbol *s)
- { Symbol *r;
- if (!X)
- { /* fatal("error, cannot eval '%s' (no proc)", s->name); */
- return ZS;
- }
- for (r = X->symtab; r; r = r->next)
- if (strcmp(r->name, s->name) == 0)
- break;
- if (!r)
- { addsymbol(X, s);
- r = X->symtab;
- }
- return r;
- }
- int
- in_bound(Symbol *r, int n)
- {
- if (!r) return 0;
- if (n >= r->nel || n < 0)
- { printf("spin: indexing %s[%d] - size is %d\n",
- r->name, n, r->nel);
- non_fatal("indexing array \'%s\'", r->name);
- return 0;
- }
- return 1;
- }
- int
- getlocal(Lextok *sn)
- { Symbol *r, *s = sn->sym;
- int n = eval(sn->lft);
- r = findloc(s);
- if (r && r->type == STRUCT)
- return Rval_struct(sn, r, 1); /* 1 = check init */
- if (in_bound(r, n))
- return cast_val(r->type, r->val[n], r->nbits);
- return 0;
- }
- int
- setlocal(Lextok *p, int m)
- { Symbol *r = findloc(p->sym);
- int n = eval(p->lft);
- if (in_bound(r, n))
- { if (r->type == STRUCT)
- (void) Lval_struct(p, r, 1, m); /* 1 = check init */
- else
- {
- #if 0
- if (r->nbits > 0)
- m = (m & ((1<<r->nbits)-1));
- r->val[n] = m;
- #else
- r->val[n] = cast_val(r->type, m, r->nbits);
- #endif
- r->setat = depth;
- } }
- return 1;
- }
- void
- whoruns(int lnr)
- { if (!X) return;
- if (lnr) printf("%3d: ", depth);
- printf("proc ");
- if (Have_claim && X->pid == 0)
- printf(" -");
- else
- printf("%2d", X->pid - Have_claim);
- printf(" (%s) ", X->n->name);
- }
- static void
- talk(RunList *r)
- {
- if ((verbose&32) || (verbose&4))
- { p_talk(r->pc, 1);
- printf("\n");
- if (verbose&1) dumpglobals();
- if (verbose&2) dumplocal(r);
- }
- }
- void
- p_talk(Element *e, int lnr)
- { static int lastnever = -1;
- int newnever = -1;
- if (e && e->n)
- newnever = e->n->ln;
- if (Have_claim && X && X->pid == 0
- && lastnever != newnever && e)
- { if (xspin)
- { printf("MSC: ~G line %d\n", newnever);
- #if 0
- printf("%3d: proc - (NEVER) line %d \"never\" ",
- depth, newnever);
- printf("(state 0)\t[printf('MSC: never\\\\n')]\n");
- } else
- { printf("%3d: proc - (NEVER) line %d \"never\"\n",
- depth, newnever);
- #endif
- }
- lastnever = newnever;
- }
- whoruns(lnr);
- if (e)
- { printf("line %3d %s (state %d)",
- e->n?e->n->ln:-1,
- e->n?e->n->fn->name:"-",
- e->seqno);
- if (!xspin
- && ((e->status&ENDSTATE) || has_lab(e, 2))) /* 2=end */
- { printf(" <valid end state>");
- }
- }
- }
- int
- remotelab(Lextok *n)
- { int i;
- lineno = n->ln;
- Fname = n->fn;
- if (n->sym->type != 0 && n->sym->type != LABEL)
- { printf("spin: error, type: %d\n", n->sym->type);
- fatal("not a labelname: '%s'", n->sym->name);
- }
- if (n->indstep >= 0)
- { fatal("remote ref to label '%s' inside d_step",
- n->sym->name);
- }
- if ((i = find_lab(n->sym, n->lft->sym, 1)) == 0)
- fatal("unknown labelname: %s", n->sym->name);
- return i;
- }
- int
- remotevar(Lextok *n)
- { int prno, i, added=0;
- RunList *Y, *oX;
- Lextok *onl;
- Symbol *os;
- lineno = n->ln;
- Fname = n->fn;
- if (!n->lft->lft)
- prno = f_pid(n->lft->sym->name);
- else
- { prno = eval(n->lft->lft); /* pid - can cause recursive call */
- #if 0
- if (n->lft->lft->ntyp == CONST) /* user-guessed pid */
- #endif
- { prno += Have_claim;
- added = Have_claim;
- } }
- if (prno < 0)
- return 0; /* non-existing process */
- #if 0
- i = nproc - nstop;
- for (Y = run; Y; Y = Y->nxt)
- { --i;
- printf(" %s: i=%d, prno=%d, ->pid=%d\n", Y->n->name, i, prno, Y->pid);
- }
- #endif
- i = nproc - nstop;
- for (Y = run; Y; Y = Y->nxt)
- if (--i == prno)
- { if (strcmp(Y->n->name, n->lft->sym->name) != 0)
- { printf("spin: remote reference error on '%s[%d]'\n",
- n->lft->sym->name, prno-added);
- non_fatal("refers to wrong proctype '%s'", Y->n->name);
- }
- if (strcmp(n->sym->name, "_p") == 0)
- { if (Y->pc)
- return Y->pc->seqno;
- /* harmless, can only happen with -t */
- return 0;
- }
- #if 1
- /* new 4.0 allow remote variables */
- oX = X;
- X = Y;
- onl = n->lft;
- n->lft = n->rgt;
- os = n->sym;
- n->sym = findloc(n->sym);
- i = getval(n);
- n->sym = os;
- n->lft = onl;
- X = oX;
- return i;
- #else
- break;
- #endif
- }
- printf("remote ref: %s[%d] ", n->lft->sym->name, prno-added);
- non_fatal("%s not found", n->sym->name);
- printf("have only:\n");
- i = nproc - nstop - 1;
- for (Y = run; Y; Y = Y->nxt, i--)
- if (!strcmp(Y->n->name, n->lft->sym->name))
- printf("\t%d\t%s\n", i, Y->n->name);
- return 0;
- }
|