0b55f123 |
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 |
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 |
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 |
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 |
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 |
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 |
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 | } |