1 /***** spin: pangen4.c *****/
2
3 /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
4 /* All Rights Reserved. This software is for educational purposes only. */
5 /* No guarantee whatsoever is expressed or implied by the distribution of */
6 /* this code. Permission is given to distribute this code provided that */
7 /* this introductory message is not removed and no monies are exchanged. */
8 /* Software written by Gerard J. Holzmann. For tool documentation see: */
9 /* http://spinroot.com/ */
10 /* Send all bug-reports and/or questions to: bugs@spinroot.com */
11
12 #include "spin.h"
13 #include "y.tab.h"
14
15 extern FILE *tc, *tb;
16 extern Queue *qtab;
17 extern Symbol *Fname;
18 extern int lineno, m_loss, Pid, eventmapnr, multi_oval;
19 extern short nocast, has_provided, has_sorted;
20 extern char *R13[], *R14[], *R15[];
21
22 static void check_proc(Lextok *, int);
23
24 void
undostmnt(Lextok * now,int m)25 undostmnt(Lextok *now, int m)
26 { Lextok *v;
27 int i, j;
28
29 if (!now)
30 { fprintf(tb, "0");
31 return;
32 }
33 lineno = now->ln;
34 Fname = now->fn;
35 switch (now->ntyp) {
36 case CONST: case '!': case UMIN:
37 case '~': case '/': case '*':
38 case '-': case '+': case '%':
39 case LT: case GT: case '&':
40 case '|': case LE: case GE:
41 case NE: case EQ: case OR:
42 case AND: case LSHIFT: case RSHIFT:
43 case TIMEOUT: case LEN: case NAME:
44 case FULL: case EMPTY: case 'R':
45 case NFULL: case NEMPTY: case ENABLED:
46 case '?': case PC_VAL: case '^':
47 case C_EXPR:
48 case NONPROGRESS:
49 putstmnt(tb, now, m);
50 break;
51
52 case RUN:
53 fprintf(tb, "delproc(0, now._nr_pr-1)");
54 break;
55
56 case 's':
57 if (Pid == eventmapnr) break;
58
59 if (m_loss)
60 fprintf(tb, "if (_m == 2) ");
61 putname(tb, "_m = unsend(", now->lft, m, ")");
62 break;
63
64 case 'r':
65 if (Pid == eventmapnr) break;
66
67 for (v = now->rgt, i=j=0; v; v = v->rgt, i++)
68 if (v->lft->ntyp != CONST
69 && v->lft->ntyp != EVAL)
70 j++;
71 if (j == 0 && now->val >= 2)
72 break; /* poll without side-effect */
73
74 { int ii = 0, jj;
75
76 for (v = now->rgt; v; v = v->rgt)
77 if ((v->lft->ntyp != CONST
78 && v->lft->ntyp != EVAL))
79 ii++; /* nr of things bupped */
80 if (now->val == 1)
81 { ii++;
82 jj = multi_oval - ii - 1;
83 fprintf(tb, "XX = trpt->bup.oval");
84 if (multi_oval > 0)
85 { fprintf(tb, "s[%d]", jj);
86 jj++;
87 }
88 fprintf(tb, ";\n\t\t");
89 } else
90 { fprintf(tb, "XX = 1;\n\t\t");
91 jj = multi_oval - ii - 1;
92 }
93
94 if (now->val < 2) /* not for channel poll */
95 for (v = now->rgt, i = 0; v; v = v->rgt, i++)
96 { switch(v->lft->ntyp) {
97 case CONST:
98 case EVAL:
99 fprintf(tb, "unrecv");
100 putname(tb, "(", now->lft, m, ", XX-1, ");
101 fprintf(tb, "%d, ", i);
102 if (v->lft->ntyp == EVAL)
103 undostmnt(v->lft->lft, m);
104 else
105 undostmnt(v->lft, m);
106 fprintf(tb, ", %d);\n\t\t", (i==0)?1:0);
107 break;
108 default:
109 fprintf(tb, "unrecv");
110 putname(tb, "(", now->lft, m, ", XX-1, ");
111 fprintf(tb, "%d, ", i);
112 if (v->lft->sym
113 && !strcmp(v->lft->sym->name, "_"))
114 { fprintf(tb, "trpt->bup.oval");
115 if (multi_oval > 0)
116 fprintf(tb, "s[%d]", jj);
117 } else
118 putstmnt(tb, v->lft, m);
119
120 fprintf(tb, ", %d);\n\t\t", (i==0)?1:0);
121 if (multi_oval > 0)
122 jj++;
123 break;
124 } }
125 jj = multi_oval - ii - 1;
126
127 if (now->val == 1 && multi_oval > 0)
128 jj++; /* new 3.4.0 */
129
130 for (v = now->rgt, i = 0; v; v = v->rgt, i++)
131 { switch(v->lft->ntyp) {
132 case CONST:
133 case EVAL:
134 break;
135 default:
136 if (!v->lft->sym
137 || strcmp(v->lft->sym->name, "_") != 0)
138 { nocast=1; putstmnt(tb,v->lft,m);
139 nocast=0; fprintf(tb, " = trpt->bup.oval");
140 if (multi_oval > 0)
141 fprintf(tb, "s[%d]", jj);
142 fprintf(tb, ";\n\t\t");
143 }
144 if (multi_oval > 0)
145 jj++;
146 break;
147 } }
148 multi_oval -= ii;
149 }
150 break;
151
152 case '@':
153 fprintf(tb, "p_restor(II);\n\t\t");
154 break;
155
156 case ASGN:
157 nocast=1; putstmnt(tb,now->lft,m);
158 nocast=0; fprintf(tb, " = trpt->bup.oval");
159 if (multi_oval > 0)
160 { multi_oval--;
161 fprintf(tb, "s[%d]", multi_oval-1);
162 }
163 check_proc(now->rgt, m);
164 break;
165
166 case 'c':
167 check_proc(now->lft, m);
168 break;
169
170 case '.':
171 case GOTO:
172 case ELSE:
173 case BREAK:
174 break;
175
176 case C_CODE:
177 fprintf(tb, "sv_restor();\n");
178 break;
179
180 case ASSERT:
181 case PRINT:
182 check_proc(now, m);
183 break;
184 case PRINTM:
185 break;
186
187 default:
188 printf("spin: bad node type %d (.b)\n", now->ntyp);
189 alldone(1);
190 }
191 }
192
193 int
any_undo(Lextok * now)194 any_undo(Lextok *now)
195 { /* is there anything to undo on a return move? */
196 if (!now) return 1;
197 switch (now->ntyp) {
198 case 'c': return any_oper(now->lft, RUN);
199 case ASSERT:
200 case PRINT: return any_oper(now, RUN);
201
202 case PRINTM:
203 case '.':
204 case GOTO:
205 case ELSE:
206 case BREAK: return 0;
207 default: return 1;
208 }
209 }
210
211 int
any_oper(Lextok * now,int oper)212 any_oper(Lextok *now, int oper)
213 { /* check if an expression contains oper operator */
214 if (!now) return 0;
215 if (now->ntyp == oper)
216 return 1;
217 return (any_oper(now->lft, oper) || any_oper(now->rgt, oper));
218 }
219
220 static void
check_proc(Lextok * now,int m)221 check_proc(Lextok *now, int m)
222 {
223 if (!now)
224 return;
225 if (now->ntyp == '@' || now->ntyp == RUN)
226 { fprintf(tb, ";\n\t\t");
227 undostmnt(now, m);
228 }
229 check_proc(now->lft, m);
230 check_proc(now->rgt, m);
231 }
232
233 void
genunio(void)234 genunio(void)
235 { char buf1[256];
236 Queue *q; int i;
237
238 ntimes(tc, 0, 1, R13);
239 for (q = qtab; q; q = q->nxt)
240 { fprintf(tc, "\tcase %d:\n", q->qid);
241
242 if (has_sorted)
243 { sprintf(buf1, "((Q%d *)z)->contents", q->qid);
244 fprintf(tc, "#ifdef HAS_SORTED\n");
245 fprintf(tc, "\t\tj = trpt->ipt;\n"); /* ipt was bup.oval */
246 fprintf(tc, "#endif\n");
247 fprintf(tc, "\t\tfor (k = j; k < ((Q%d *)z)->Qlen; k++)\n",
248 q->qid);
249 fprintf(tc, "\t\t{\n");
250 for (i = 0; i < q->nflds; i++)
251 fprintf(tc, "\t\t\t%s[k].fld%d = %s[k+1].fld%d;\n",
252 buf1, i, buf1, i);
253 fprintf(tc, "\t\t}\n");
254 fprintf(tc, "\t\tj = ((Q0 *)z)->Qlen;\n");
255 }
256
257 sprintf(buf1, "((Q%d *)z)->contents[j].fld", q->qid);
258 for (i = 0; i < q->nflds; i++)
259 fprintf(tc, "\t\t%s%d = 0;\n", buf1, i);
260 if (q->nslots==0)
261 { /* check if rendezvous succeeded, 1 level down */
262 fprintf(tc, "\t\t_m = (trpt+1)->o_m;\n");
263 fprintf(tc, "\t\tif (_m) (trpt-1)->o_pm |= 1;\n");
264 fprintf(tc, "\t\tUnBlock;\n");
265 } else
266 fprintf(tc, "\t\t_m = trpt->o_m;\n");
267
268 fprintf(tc, "\t\tbreak;\n");
269 }
270 ntimes(tc, 0, 1, R14);
271 for (q = qtab; q; q = q->nxt)
272 { sprintf(buf1, "((Q%d *)z)->contents", q->qid);
273 fprintf(tc, " case %d:\n", q->qid);
274 if (q->nslots == 0)
275 fprintf(tc, "\t\tif (strt) boq = from+1;\n");
276 else if (q->nslots > 1) /* shift */
277 { fprintf(tc, "\t\tif (strt && slot<%d)\n",
278 q->nslots-1);
279 fprintf(tc, "\t\t{\tfor (j--; j>=slot; j--)\n");
280 fprintf(tc, "\t\t\t{");
281 for (i = 0; i < q->nflds; i++)
282 { fprintf(tc, "\t%s[j+1].fld%d =\n\t\t\t",
283 buf1, i);
284 fprintf(tc, "\t%s[j].fld%d;\n\t\t\t",
285 buf1, i);
286 }
287 fprintf(tc, "}\n\t\t}\n");
288 }
289 strcat(buf1, "[slot].fld");
290 fprintf(tc, "\t\tif (strt) {\n");
291 for (i = 0; i < q->nflds; i++)
292 fprintf(tc, "\t\t\t%s%d = 0;\n", buf1, i);
293 fprintf(tc, "\t\t}\n");
294 if (q->nflds == 1) /* set */
295 fprintf(tc, "\t\tif (fld == 0) %s0 = fldvar;\n",
296 buf1);
297 else
298 { fprintf(tc, "\t\tswitch (fld) {\n");
299 for (i = 0; i < q->nflds; i++)
300 { fprintf(tc, "\t\tcase %d:\t%s", i, buf1);
301 fprintf(tc, "%d = fldvar; break;\n", i);
302 }
303 fprintf(tc, "\t\t}\n");
304 }
305 fprintf(tc, "\t\tbreak;\n");
306 }
307 ntimes(tc, 0, 1, R15);
308 }
309
310 extern void explain(int);
311
312 int
proper_enabler(Lextok * n)313 proper_enabler(Lextok *n)
314 {
315 if (!n) return 1;
316 switch (n->ntyp) {
317 case NEMPTY: case FULL:
318 case NFULL: case EMPTY:
319 case LEN: case 'R':
320 case NAME:
321 has_provided = 1;
322 if (strcmp(n->sym->name, "_pid") == 0)
323 return 1;
324 return (!(n->sym->context));
325
326 case C_EXPR:
327 case CONST:
328 case TIMEOUT:
329 has_provided = 1;
330 return 1;
331
332 case ENABLED: case PC_VAL:
333 return proper_enabler(n->lft);
334
335 case '!': case UMIN: case '~':
336 return proper_enabler(n->lft);
337
338 case '/': case '*': case '-': case '+':
339 case '%': case LT: case GT: case '&': case '^':
340 case '|': case LE: case GE: case NE: case '?':
341 case EQ: case OR: case AND: case LSHIFT:
342 case RSHIFT: case 'c':
343 return proper_enabler(n->lft) && proper_enabler(n->rgt);
344 default:
345 break;
346 }
347 printf("spin: saw ");
348 explain(n->ntyp);
349 printf("\n");
350 return 0;
351 }
352