Subversion Repositories planix.SVN

Rev

Details | Last modification | View Log | RSS feed

Rev Author Line No. Line
2 - 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 
}