1219b2ee8SDavid du Colombier /***** spin: pangen4.c *****/
2219b2ee8SDavid du Colombier
3312a1df1SDavid du Colombier /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
47dd7cddfSDavid du Colombier /* All Rights Reserved. This software is for educational purposes only. */
5312a1df1SDavid du Colombier /* No guarantee whatsoever is expressed or implied by the distribution of */
6312a1df1SDavid du Colombier /* this code. Permission is given to distribute this code provided that */
7312a1df1SDavid du Colombier /* this introductory message is not removed and no monies are exchanged. */
8312a1df1SDavid du Colombier /* Software written by Gerard J. Holzmann. For tool documentation see: */
9312a1df1SDavid du Colombier /* http://spinroot.com/ */
10312a1df1SDavid du Colombier /* Send all bug-reports and/or questions to: bugs@spinroot.com */
11219b2ee8SDavid du Colombier
12219b2ee8SDavid du Colombier #include "spin.h"
13219b2ee8SDavid du Colombier #include "y.tab.h"
14219b2ee8SDavid du Colombier
15219b2ee8SDavid du Colombier extern FILE *tc, *tb;
16219b2ee8SDavid du Colombier extern Queue *qtab;
17219b2ee8SDavid du Colombier extern Symbol *Fname;
18312a1df1SDavid du Colombier extern int lineno, m_loss, Pid, eventmapnr, multi_oval;
19312a1df1SDavid du Colombier extern short nocast, has_provided, has_sorted;
20219b2ee8SDavid du Colombier extern char *R13[], *R14[], *R15[];
21219b2ee8SDavid du Colombier
227dd7cddfSDavid du Colombier static void check_proc(Lextok *, int);
237dd7cddfSDavid du Colombier
24219b2ee8SDavid du Colombier void
undostmnt(Lextok * now,int m)25219b2ee8SDavid du Colombier undostmnt(Lextok *now, int m)
26219b2ee8SDavid du Colombier { Lextok *v;
277dd7cddfSDavid du Colombier int i, j;
28219b2ee8SDavid du Colombier
29219b2ee8SDavid du Colombier if (!now)
30219b2ee8SDavid du Colombier { fprintf(tb, "0");
31219b2ee8SDavid du Colombier return;
32219b2ee8SDavid du Colombier }
33219b2ee8SDavid du Colombier lineno = now->ln;
34219b2ee8SDavid du Colombier Fname = now->fn;
35219b2ee8SDavid du Colombier switch (now->ntyp) {
36219b2ee8SDavid du Colombier case CONST: case '!': case UMIN:
37219b2ee8SDavid du Colombier case '~': case '/': case '*':
38219b2ee8SDavid du Colombier case '-': case '+': case '%':
39219b2ee8SDavid du Colombier case LT: case GT: case '&':
40219b2ee8SDavid du Colombier case '|': case LE: case GE:
41219b2ee8SDavid du Colombier case NE: case EQ: case OR:
42219b2ee8SDavid du Colombier case AND: case LSHIFT: case RSHIFT:
43219b2ee8SDavid du Colombier case TIMEOUT: case LEN: case NAME:
44219b2ee8SDavid du Colombier case FULL: case EMPTY: case 'R':
45219b2ee8SDavid du Colombier case NFULL: case NEMPTY: case ENABLED:
467dd7cddfSDavid du Colombier case '?': case PC_VAL: case '^':
47312a1df1SDavid du Colombier case C_EXPR:
487dd7cddfSDavid du Colombier case NONPROGRESS:
49219b2ee8SDavid du Colombier putstmnt(tb, now, m);
50219b2ee8SDavid du Colombier break;
517dd7cddfSDavid du Colombier
527dd7cddfSDavid du Colombier case RUN:
537dd7cddfSDavid du Colombier fprintf(tb, "delproc(0, now._nr_pr-1)");
54219b2ee8SDavid du Colombier break;
557dd7cddfSDavid du Colombier
567dd7cddfSDavid du Colombier case 's':
577dd7cddfSDavid du Colombier if (Pid == eventmapnr) break;
587dd7cddfSDavid du Colombier
597dd7cddfSDavid du Colombier if (m_loss)
60312a1df1SDavid du Colombier fprintf(tb, "if (_m == 2) ");
61312a1df1SDavid du Colombier putname(tb, "_m = unsend(", now->lft, m, ")");
62219b2ee8SDavid du Colombier break;
637dd7cddfSDavid du Colombier
647dd7cddfSDavid du Colombier case 'r':
657dd7cddfSDavid du Colombier if (Pid == eventmapnr) break;
667dd7cddfSDavid du Colombier
677dd7cddfSDavid du Colombier for (v = now->rgt, i=j=0; v; v = v->rgt, i++)
687dd7cddfSDavid du Colombier if (v->lft->ntyp != CONST
697dd7cddfSDavid du Colombier && v->lft->ntyp != EVAL)
70219b2ee8SDavid du Colombier j++;
717dd7cddfSDavid du Colombier if (j == 0 && now->val >= 2)
727dd7cddfSDavid du Colombier break; /* poll without side-effect */
737dd7cddfSDavid du Colombier
747dd7cddfSDavid du Colombier { int ii = 0, jj;
757dd7cddfSDavid du Colombier
767dd7cddfSDavid du Colombier for (v = now->rgt; v; v = v->rgt)
777dd7cddfSDavid du Colombier if ((v->lft->ntyp != CONST
787dd7cddfSDavid du Colombier && v->lft->ntyp != EVAL))
797dd7cddfSDavid du Colombier ii++; /* nr of things bupped */
807dd7cddfSDavid du Colombier if (now->val == 1)
817dd7cddfSDavid du Colombier { ii++;
827dd7cddfSDavid du Colombier jj = multi_oval - ii - 1;
837dd7cddfSDavid du Colombier fprintf(tb, "XX = trpt->bup.oval");
847dd7cddfSDavid du Colombier if (multi_oval > 0)
857dd7cddfSDavid du Colombier { fprintf(tb, "s[%d]", jj);
867dd7cddfSDavid du Colombier jj++;
877dd7cddfSDavid du Colombier }
887dd7cddfSDavid du Colombier fprintf(tb, ";\n\t\t");
89219b2ee8SDavid du Colombier } else
907dd7cddfSDavid du Colombier { fprintf(tb, "XX = 1;\n\t\t");
917dd7cddfSDavid du Colombier jj = multi_oval - ii - 1;
927dd7cddfSDavid du Colombier }
937dd7cddfSDavid du Colombier
947dd7cddfSDavid du Colombier if (now->val < 2) /* not for channel poll */
95219b2ee8SDavid du Colombier for (v = now->rgt, i = 0; v; v = v->rgt, i++)
967dd7cddfSDavid du Colombier { switch(v->lft->ntyp) {
977dd7cddfSDavid du Colombier case CONST:
987dd7cddfSDavid du Colombier case EVAL:
997dd7cddfSDavid du Colombier fprintf(tb, "unrecv");
1007dd7cddfSDavid du Colombier putname(tb, "(", now->lft, m, ", XX-1, ");
101219b2ee8SDavid du Colombier fprintf(tb, "%d, ", i);
1027dd7cddfSDavid du Colombier if (v->lft->ntyp == EVAL)
1037dd7cddfSDavid du Colombier undostmnt(v->lft->lft, m);
1047dd7cddfSDavid du Colombier else
105219b2ee8SDavid du Colombier undostmnt(v->lft, m);
106219b2ee8SDavid du Colombier fprintf(tb, ", %d);\n\t\t", (i==0)?1:0);
1077dd7cddfSDavid du Colombier break;
1087dd7cddfSDavid du Colombier default:
1097dd7cddfSDavid du Colombier fprintf(tb, "unrecv");
1107dd7cddfSDavid du Colombier putname(tb, "(", now->lft, m, ", XX-1, ");
1117dd7cddfSDavid du Colombier fprintf(tb, "%d, ", i);
1127dd7cddfSDavid du Colombier if (v->lft->sym
1137dd7cddfSDavid du Colombier && !strcmp(v->lft->sym->name, "_"))
1147dd7cddfSDavid du Colombier { fprintf(tb, "trpt->bup.oval");
1157dd7cddfSDavid du Colombier if (multi_oval > 0)
1167dd7cddfSDavid du Colombier fprintf(tb, "s[%d]", jj);
1177dd7cddfSDavid du Colombier } else
1187dd7cddfSDavid du Colombier putstmnt(tb, v->lft, m);
1197dd7cddfSDavid du Colombier
1207dd7cddfSDavid du Colombier fprintf(tb, ", %d);\n\t\t", (i==0)?1:0);
1217dd7cddfSDavid du Colombier if (multi_oval > 0)
1227dd7cddfSDavid du Colombier jj++;
1237dd7cddfSDavid du Colombier break;
1247dd7cddfSDavid du Colombier } }
1257dd7cddfSDavid du Colombier jj = multi_oval - ii - 1;
126312a1df1SDavid du Colombier
127312a1df1SDavid du Colombier if (now->val == 1 && multi_oval > 0)
128312a1df1SDavid du Colombier jj++; /* new 3.4.0 */
129312a1df1SDavid du Colombier
1307dd7cddfSDavid du Colombier for (v = now->rgt, i = 0; v; v = v->rgt, i++)
1317dd7cddfSDavid du Colombier { switch(v->lft->ntyp) {
1327dd7cddfSDavid du Colombier case CONST:
1337dd7cddfSDavid du Colombier case EVAL:
1347dd7cddfSDavid du Colombier break;
1357dd7cddfSDavid du Colombier default:
1367dd7cddfSDavid du Colombier if (!v->lft->sym
1377dd7cddfSDavid du Colombier || strcmp(v->lft->sym->name, "_") != 0)
1387dd7cddfSDavid du Colombier { nocast=1; putstmnt(tb,v->lft,m);
1397dd7cddfSDavid du Colombier nocast=0; fprintf(tb, " = trpt->bup.oval");
1407dd7cddfSDavid du Colombier if (multi_oval > 0)
1417dd7cddfSDavid du Colombier fprintf(tb, "s[%d]", jj);
1427dd7cddfSDavid du Colombier fprintf(tb, ";\n\t\t");
143219b2ee8SDavid du Colombier }
1447dd7cddfSDavid du Colombier if (multi_oval > 0)
1457dd7cddfSDavid du Colombier jj++;
1467dd7cddfSDavid du Colombier break;
1477dd7cddfSDavid du Colombier } }
1487dd7cddfSDavid du Colombier multi_oval -= ii;
149219b2ee8SDavid du Colombier }
150219b2ee8SDavid du Colombier break;
1517dd7cddfSDavid du Colombier
1527dd7cddfSDavid du Colombier case '@':
1537dd7cddfSDavid du Colombier fprintf(tb, "p_restor(II);\n\t\t");
154219b2ee8SDavid du Colombier break;
1557dd7cddfSDavid du Colombier
1567dd7cddfSDavid du Colombier case ASGN:
1577dd7cddfSDavid du Colombier nocast=1; putstmnt(tb,now->lft,m);
1587dd7cddfSDavid du Colombier nocast=0; fprintf(tb, " = trpt->bup.oval");
1597dd7cddfSDavid du Colombier if (multi_oval > 0)
1607dd7cddfSDavid du Colombier { multi_oval--;
1617dd7cddfSDavid du Colombier fprintf(tb, "s[%d]", multi_oval-1);
1627dd7cddfSDavid du Colombier }
163219b2ee8SDavid du Colombier check_proc(now->rgt, m);
164219b2ee8SDavid du Colombier break;
1657dd7cddfSDavid du Colombier
1667dd7cddfSDavid du Colombier case 'c':
1677dd7cddfSDavid du Colombier check_proc(now->lft, m);
168219b2ee8SDavid du Colombier break;
1697dd7cddfSDavid du Colombier
170219b2ee8SDavid du Colombier case '.':
171219b2ee8SDavid du Colombier case GOTO:
172219b2ee8SDavid du Colombier case ELSE:
1737dd7cddfSDavid du Colombier case BREAK:
174219b2ee8SDavid du Colombier break;
1757dd7cddfSDavid du Colombier
176312a1df1SDavid du Colombier case C_CODE:
177312a1df1SDavid du Colombier fprintf(tb, "sv_restor();\n");
178312a1df1SDavid du Colombier break;
179312a1df1SDavid du Colombier
1807dd7cddfSDavid du Colombier case ASSERT:
1817dd7cddfSDavid du Colombier case PRINT:
1827dd7cddfSDavid du Colombier check_proc(now, m);
1837dd7cddfSDavid du Colombier break;
184312a1df1SDavid du Colombier case PRINTM:
185312a1df1SDavid du Colombier break;
1867dd7cddfSDavid du Colombier
1877dd7cddfSDavid du Colombier default:
1887dd7cddfSDavid du Colombier printf("spin: bad node type %d (.b)\n", now->ntyp);
1897dd7cddfSDavid du Colombier alldone(1);
190219b2ee8SDavid du Colombier }
191219b2ee8SDavid du Colombier }
192219b2ee8SDavid du Colombier
193219b2ee8SDavid du Colombier int
any_undo(Lextok * now)194219b2ee8SDavid du Colombier any_undo(Lextok *now)
195219b2ee8SDavid du Colombier { /* is there anything to undo on a return move? */
196219b2ee8SDavid du Colombier if (!now) return 1;
197219b2ee8SDavid du Colombier switch (now->ntyp) {
198219b2ee8SDavid du Colombier case 'c': return any_oper(now->lft, RUN);
199219b2ee8SDavid du Colombier case ASSERT:
200219b2ee8SDavid du Colombier case PRINT: return any_oper(now, RUN);
201219b2ee8SDavid du Colombier
202312a1df1SDavid du Colombier case PRINTM:
203219b2ee8SDavid du Colombier case '.':
204219b2ee8SDavid du Colombier case GOTO:
205219b2ee8SDavid du Colombier case ELSE:
206219b2ee8SDavid du Colombier case BREAK: return 0;
207219b2ee8SDavid du Colombier default: return 1;
208219b2ee8SDavid du Colombier }
209219b2ee8SDavid du Colombier }
210219b2ee8SDavid du Colombier
211219b2ee8SDavid du Colombier int
any_oper(Lextok * now,int oper)212219b2ee8SDavid du Colombier any_oper(Lextok *now, int oper)
213219b2ee8SDavid du Colombier { /* check if an expression contains oper operator */
214219b2ee8SDavid du Colombier if (!now) return 0;
215219b2ee8SDavid du Colombier if (now->ntyp == oper)
216219b2ee8SDavid du Colombier return 1;
217219b2ee8SDavid du Colombier return (any_oper(now->lft, oper) || any_oper(now->rgt, oper));
218219b2ee8SDavid du Colombier }
219219b2ee8SDavid du Colombier
2207dd7cddfSDavid du Colombier static void
check_proc(Lextok * now,int m)221219b2ee8SDavid du Colombier check_proc(Lextok *now, int m)
222219b2ee8SDavid du Colombier {
223219b2ee8SDavid du Colombier if (!now)
224219b2ee8SDavid du Colombier return;
225219b2ee8SDavid du Colombier if (now->ntyp == '@' || now->ntyp == RUN)
226219b2ee8SDavid du Colombier { fprintf(tb, ";\n\t\t");
227219b2ee8SDavid du Colombier undostmnt(now, m);
228219b2ee8SDavid du Colombier }
229219b2ee8SDavid du Colombier check_proc(now->lft, m);
230219b2ee8SDavid du Colombier check_proc(now->rgt, m);
231219b2ee8SDavid du Colombier }
232219b2ee8SDavid du Colombier
233219b2ee8SDavid du Colombier void
genunio(void)234219b2ee8SDavid du Colombier genunio(void)
2357dd7cddfSDavid du Colombier { char buf1[256];
2367dd7cddfSDavid du Colombier Queue *q; int i;
237219b2ee8SDavid du Colombier
238219b2ee8SDavid du Colombier ntimes(tc, 0, 1, R13);
239219b2ee8SDavid du Colombier for (q = qtab; q; q = q->nxt)
240219b2ee8SDavid du Colombier { fprintf(tc, "\tcase %d:\n", q->qid);
241219b2ee8SDavid du Colombier
242219b2ee8SDavid du Colombier if (has_sorted)
243219b2ee8SDavid du Colombier { sprintf(buf1, "((Q%d *)z)->contents", q->qid);
244312a1df1SDavid du Colombier fprintf(tc, "#ifdef HAS_SORTED\n");
245312a1df1SDavid du Colombier fprintf(tc, "\t\tj = trpt->ipt;\n"); /* ipt was bup.oval */
246312a1df1SDavid du Colombier fprintf(tc, "#endif\n");
2477dd7cddfSDavid du Colombier fprintf(tc, "\t\tfor (k = j; k < ((Q%d *)z)->Qlen; k++)\n",
2487dd7cddfSDavid du Colombier q->qid);
249219b2ee8SDavid du Colombier fprintf(tc, "\t\t{\n");
250219b2ee8SDavid du Colombier for (i = 0; i < q->nflds; i++)
251219b2ee8SDavid du Colombier fprintf(tc, "\t\t\t%s[k].fld%d = %s[k+1].fld%d;\n",
252219b2ee8SDavid du Colombier buf1, i, buf1, i);
253219b2ee8SDavid du Colombier fprintf(tc, "\t\t}\n");
254219b2ee8SDavid du Colombier fprintf(tc, "\t\tj = ((Q0 *)z)->Qlen;\n");
255219b2ee8SDavid du Colombier }
256219b2ee8SDavid du Colombier
257219b2ee8SDavid du Colombier sprintf(buf1, "((Q%d *)z)->contents[j].fld", q->qid);
258219b2ee8SDavid du Colombier for (i = 0; i < q->nflds; i++)
259219b2ee8SDavid du Colombier fprintf(tc, "\t\t%s%d = 0;\n", buf1, i);
260219b2ee8SDavid du Colombier if (q->nslots==0)
261219b2ee8SDavid du Colombier { /* check if rendezvous succeeded, 1 level down */
262312a1df1SDavid du Colombier fprintf(tc, "\t\t_m = (trpt+1)->o_m;\n");
263312a1df1SDavid du Colombier fprintf(tc, "\t\tif (_m) (trpt-1)->o_pm |= 1;\n");
264219b2ee8SDavid du Colombier fprintf(tc, "\t\tUnBlock;\n");
265219b2ee8SDavid du Colombier } else
266312a1df1SDavid du Colombier fprintf(tc, "\t\t_m = trpt->o_m;\n");
2677dd7cddfSDavid du Colombier
268219b2ee8SDavid du Colombier fprintf(tc, "\t\tbreak;\n");
269219b2ee8SDavid du Colombier }
270219b2ee8SDavid du Colombier ntimes(tc, 0, 1, R14);
271219b2ee8SDavid du Colombier for (q = qtab; q; q = q->nxt)
272219b2ee8SDavid du Colombier { sprintf(buf1, "((Q%d *)z)->contents", q->qid);
273219b2ee8SDavid du Colombier fprintf(tc, " case %d:\n", q->qid);
274219b2ee8SDavid du Colombier if (q->nslots == 0)
275219b2ee8SDavid du Colombier fprintf(tc, "\t\tif (strt) boq = from+1;\n");
276219b2ee8SDavid du Colombier else if (q->nslots > 1) /* shift */
277219b2ee8SDavid du Colombier { fprintf(tc, "\t\tif (strt && slot<%d)\n",
278219b2ee8SDavid du Colombier q->nslots-1);
279219b2ee8SDavid du Colombier fprintf(tc, "\t\t{\tfor (j--; j>=slot; j--)\n");
280219b2ee8SDavid du Colombier fprintf(tc, "\t\t\t{");
281219b2ee8SDavid du Colombier for (i = 0; i < q->nflds; i++)
282219b2ee8SDavid du Colombier { fprintf(tc, "\t%s[j+1].fld%d =\n\t\t\t",
283219b2ee8SDavid du Colombier buf1, i);
284219b2ee8SDavid du Colombier fprintf(tc, "\t%s[j].fld%d;\n\t\t\t",
285219b2ee8SDavid du Colombier buf1, i);
286219b2ee8SDavid du Colombier }
287219b2ee8SDavid du Colombier fprintf(tc, "}\n\t\t}\n");
288219b2ee8SDavid du Colombier }
289219b2ee8SDavid du Colombier strcat(buf1, "[slot].fld");
290219b2ee8SDavid du Colombier fprintf(tc, "\t\tif (strt) {\n");
291219b2ee8SDavid du Colombier for (i = 0; i < q->nflds; i++)
292219b2ee8SDavid du Colombier fprintf(tc, "\t\t\t%s%d = 0;\n", buf1, i);
293219b2ee8SDavid du Colombier fprintf(tc, "\t\t}\n");
294219b2ee8SDavid du Colombier if (q->nflds == 1) /* set */
295219b2ee8SDavid du Colombier fprintf(tc, "\t\tif (fld == 0) %s0 = fldvar;\n",
296219b2ee8SDavid du Colombier buf1);
297219b2ee8SDavid du Colombier else
298219b2ee8SDavid du Colombier { fprintf(tc, "\t\tswitch (fld) {\n");
299219b2ee8SDavid du Colombier for (i = 0; i < q->nflds; i++)
300219b2ee8SDavid du Colombier { fprintf(tc, "\t\tcase %d:\t%s", i, buf1);
301219b2ee8SDavid du Colombier fprintf(tc, "%d = fldvar; break;\n", i);
302219b2ee8SDavid du Colombier }
303219b2ee8SDavid du Colombier fprintf(tc, "\t\t}\n");
304219b2ee8SDavid du Colombier }
305219b2ee8SDavid du Colombier fprintf(tc, "\t\tbreak;\n");
306219b2ee8SDavid du Colombier }
307219b2ee8SDavid du Colombier ntimes(tc, 0, 1, R15);
308219b2ee8SDavid du Colombier }
3097dd7cddfSDavid du Colombier
310*00d97012SDavid du Colombier extern void explain(int);
311*00d97012SDavid du Colombier
3127dd7cddfSDavid du Colombier int
proper_enabler(Lextok * n)3137dd7cddfSDavid du Colombier proper_enabler(Lextok *n)
3147dd7cddfSDavid du Colombier {
3157dd7cddfSDavid du Colombier if (!n) return 1;
3167dd7cddfSDavid du Colombier switch (n->ntyp) {
3177dd7cddfSDavid du Colombier case NEMPTY: case FULL:
3187dd7cddfSDavid du Colombier case NFULL: case EMPTY:
3197dd7cddfSDavid du Colombier case LEN: case 'R':
3207dd7cddfSDavid du Colombier case NAME:
3217dd7cddfSDavid du Colombier has_provided = 1;
3227dd7cddfSDavid du Colombier if (strcmp(n->sym->name, "_pid") == 0)
3237dd7cddfSDavid du Colombier return 1;
3247dd7cddfSDavid du Colombier return (!(n->sym->context));
3257dd7cddfSDavid du Colombier
326*00d97012SDavid du Colombier case C_EXPR:
327*00d97012SDavid du Colombier case CONST:
328*00d97012SDavid du Colombier case TIMEOUT:
3297dd7cddfSDavid du Colombier has_provided = 1;
3307dd7cddfSDavid du Colombier return 1;
3317dd7cddfSDavid du Colombier
3327dd7cddfSDavid du Colombier case ENABLED: case PC_VAL:
3337dd7cddfSDavid du Colombier return proper_enabler(n->lft);
3347dd7cddfSDavid du Colombier
3357dd7cddfSDavid du Colombier case '!': case UMIN: case '~':
3367dd7cddfSDavid du Colombier return proper_enabler(n->lft);
3377dd7cddfSDavid du Colombier
3387dd7cddfSDavid du Colombier case '/': case '*': case '-': case '+':
3397dd7cddfSDavid du Colombier case '%': case LT: case GT: case '&': case '^':
3407dd7cddfSDavid du Colombier case '|': case LE: case GE: case NE: case '?':
3417dd7cddfSDavid du Colombier case EQ: case OR: case AND: case LSHIFT:
3427dd7cddfSDavid du Colombier case RSHIFT: case 'c':
3437dd7cddfSDavid du Colombier return proper_enabler(n->lft) && proper_enabler(n->rgt);
3447dd7cddfSDavid du Colombier default:
3457dd7cddfSDavid du Colombier break;
3467dd7cddfSDavid du Colombier }
347*00d97012SDavid du Colombier printf("spin: saw ");
348*00d97012SDavid du Colombier explain(n->ntyp);
349*00d97012SDavid du Colombier printf("\n");
3507dd7cddfSDavid du Colombier return 0;
3517dd7cddfSDavid du Colombier }
352