1 /***** spin: pangen4.c *****/
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 */
18 extern int lineno
, m_loss
, Pid
, eventmapnr
, multi_oval
;
19 extern short nocast
, has_provided
, has_sorted
;
20 extern char *R13
[], *R14
[], *R15
[];
22 static void check_proc(Lextok
*, int);
25 undostmnt(Lextok
*now
, int m
)
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 '^':
53 fprintf(tb
, "delproc(0, now._nr_pr-1)");
57 if (Pid
== eventmapnr
) break;
60 fprintf(tb
, "if (_m == 2) ");
61 putname(tb
, "_m = unsend(", now
->lft
, m
, ")");
65 if (Pid
== eventmapnr
) break;
67 for (v
= now
->rgt
, i
=j
=0; v
; v
= v
->rgt
, i
++)
68 if (v
->lft
->ntyp
!= CONST
69 && v
->lft
->ntyp
!= EVAL
)
71 if (j
== 0 && now
->val
>= 2)
72 break; /* poll without side-effect */
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 */
82 jj
= multi_oval
- ii
- 1;
83 fprintf(tb
, "XX = trpt->bup.oval");
85 { fprintf(tb
, "s[%d]", jj
);
88 fprintf(tb
, ";\n\t\t");
90 { fprintf(tb
, "XX = 1;\n\t\t");
91 jj
= multi_oval
- ii
- 1;
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
) {
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
);
105 undostmnt(v
->lft
, m
);
106 fprintf(tb
, ", %d);\n\t\t", (i
==0)?1:0);
109 fprintf(tb
, "unrecv");
110 putname(tb
, "(", now
->lft
, m
, ", XX-1, ");
111 fprintf(tb
, "%d, ", i
);
113 && !strcmp(v
->lft
->sym
->name
, "_"))
114 { fprintf(tb
, "trpt->bup.oval");
116 fprintf(tb
, "s[%d]", jj
);
118 putstmnt(tb
, v
->lft
, m
);
120 fprintf(tb
, ", %d);\n\t\t", (i
==0)?1:0);
125 jj
= multi_oval
- ii
- 1;
127 if (now
->val
== 1 && multi_oval
> 0)
128 jj
++; /* new 3.4.0 */
130 for (v
= now
->rgt
, i
= 0; v
; v
= v
->rgt
, i
++)
131 { switch(v
->lft
->ntyp
) {
137 || strcmp(v
->lft
->sym
->name
, "_") != 0)
138 { nocast
=1; putstmnt(tb
,v
->lft
,m
);
139 nocast
=0; fprintf(tb
, " = trpt->bup.oval");
141 fprintf(tb
, "s[%d]", jj
);
142 fprintf(tb
, ";\n\t\t");
153 fprintf(tb
, "p_restor(II);\n\t\t");
157 nocast
=1; putstmnt(tb
,now
->lft
,m
);
158 nocast
=0; fprintf(tb
, " = trpt->bup.oval");
161 fprintf(tb
, "s[%d]", multi_oval
-1);
163 check_proc(now
->rgt
, m
);
167 check_proc(now
->lft
, m
);
177 fprintf(tb
, "sv_restor();\n");
188 printf("spin: bad node type %d (.b)\n", now
->ntyp
);
194 any_undo(Lextok
*now
)
195 { /* is there anything to undo on a return move? */
198 case 'c': return any_oper(now
->lft
, RUN
);
200 case PRINT
: return any_oper(now
, RUN
);
206 case BREAK
: return 0;
212 any_oper(Lextok
*now
, int oper
)
213 { /* check if an expression contains oper operator */
215 if (now
->ntyp
== oper
)
217 return (any_oper(now
->lft
, oper
) || any_oper(now
->rgt
, oper
));
221 check_proc(Lextok
*now
, int m
)
225 if (now
->ntyp
== '@' || now
->ntyp
== RUN
)
226 { fprintf(tb
, ";\n\t\t");
229 check_proc(now
->lft
, m
);
230 check_proc(now
->rgt
, m
);
238 ntimes(tc
, 0, 1, R13
);
239 for (q
= qtab
; q
; q
= q
->nxt
)
240 { fprintf(tc
, "\tcase %d:\n", q
->qid
);
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",
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",
253 fprintf(tc
, "\t\t}\n");
254 fprintf(tc
, "\t\tj = ((Q0 *)z)->Qlen;\n");
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
);
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");
266 fprintf(tc
, "\t\t_m = trpt->o_m;\n");
268 fprintf(tc
, "\t\tbreak;\n");
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
);
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",
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",
284 fprintf(tc
, "\t%s[j].fld%d;\n\t\t\t",
287 fprintf(tc
, "}\n\t\t}\n");
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",
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
);
303 fprintf(tc
, "\t\t}\n");
305 fprintf(tc
, "\t\tbreak;\n");
307 ntimes(tc
, 0, 1, R15
);
310 extern void explain(int);
313 proper_enabler(Lextok
*n
)
317 case NEMPTY
: case FULL
:
318 case NFULL
: case EMPTY
:
322 if (strcmp(n
->sym
->name
, "_pid") == 0)
324 return (!(n
->sym
->context
));
332 case ENABLED
: case PC_VAL
:
333 return proper_enabler(n
->lft
);
335 case '!': case UMIN
: case '~':
336 return proper_enabler(n
->lft
);
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
);
347 printf("spin: saw ");
This page took 0.03869 seconds and 4 git commands to generate.