[lttv.git] / trunk / verif / Spin / Src5.1.6 / pangen4.c

/***** spin: pangen4.c *****/

/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     */
/* All Rights Reserved.  This software is for educational purposes only.  */
/* No guarantee whatsoever is expressed or implied by the distribution of */
/* this code.  Permission is given to distribute this code provided that  */
/* this introductory message is not removed and no monies are exchanged.  */
/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
/*             http://spinroot.com/                                       */
/* Send all bug-reports and/or questions to: bugs@spinroot.com            */

#include "spin.h"
#include "y.tab.h"

extern FILE	*tc, *tb;
extern Queue	*qtab;
extern Symbol	*Fname;
extern int	lineno, m_loss, Pid, eventmapnr, multi_oval;
extern short	nocast, has_provided, has_sorted;
extern char	*R13[], *R14[], *R15[];

static void	check_proc(Lextok *, int);

void
undostmnt(Lextok *now, int m)
{	Lextok *v;
	int i, j;

	if (!now)
	{	fprintf(tb, "0");
		return;
	}
	lineno = now->ln;
	Fname  = now->fn;
	switch (now->ntyp) {
	case CONST:	case '!':	case UMIN:
	case '~':	case '/':	case '*':
	case '-':	case '+':	case '%':
	case LT:	case GT:	case '&':
	case '|':	case LE:	case GE:
	case NE:	case EQ:	case OR:
	case AND:	case LSHIFT:	case RSHIFT:
	case TIMEOUT:	case LEN:	case NAME:
	case FULL:	case EMPTY:	case 'R':
	case NFULL:	case NEMPTY:	case ENABLED:
	case '?':	case PC_VAL:	case '^':
	case C_EXPR:
	case NONPROGRESS:
		putstmnt(tb, now, m);
		break;

	case RUN:
		fprintf(tb, "delproc(0, now._nr_pr-1)");
		break;

	case 's':
		if (Pid == eventmapnr) break;

		if (m_loss)
			fprintf(tb, "if (_m == 2) ");
		putname(tb, "_m = unsend(", now->lft, m, ")");
		break;

	case 'r':
		if (Pid == eventmapnr) break;

		for (v = now->rgt, i=j=0; v; v = v->rgt, i++)
			if (v->lft->ntyp != CONST
			&&  v->lft->ntyp != EVAL)
				j++;
		if (j == 0 && now->val >= 2)
			break;	/* poll without side-effect */

		{	int ii = 0, jj;

			for (v = now->rgt; v; v = v->rgt)
				if ((v->lft->ntyp != CONST
				&&   v->lft->ntyp != EVAL))
					ii++;	/* nr of things bupped */
			if (now->val == 1)
			{	ii++;
				jj = multi_oval - ii - 1;
				fprintf(tb, "XX = trpt->bup.oval");
				if (multi_oval > 0)
				{	fprintf(tb, "s[%d]", jj);
					jj++;
				}
				fprintf(tb, ";\n\t\t");
			} else
			{	fprintf(tb, "XX = 1;\n\t\t");
				jj = multi_oval - ii - 1;
			}

			if (now->val < 2)	/* not for channel poll */
			for (v = now->rgt, i = 0; v; v = v->rgt, i++)
			{	switch(v->lft->ntyp) {
				case CONST:
				case EVAL:
					fprintf(tb, "unrecv");
					putname(tb, "(", now->lft, m, ", XX-1, ");
					fprintf(tb, "%d, ", i);
					if (v->lft->ntyp == EVAL)
						undostmnt(v->lft->lft, m);
					else
						undostmnt(v->lft, m);
					fprintf(tb, ", %d);\n\t\t", (i==0)?1:0);
					break;
				default:
					fprintf(tb, "unrecv");
					putname(tb, "(", now->lft, m, ", XX-1, ");
					fprintf(tb, "%d, ", i);
					if (v->lft->sym
					&& !strcmp(v->lft->sym->name, "_"))
					{	fprintf(tb, "trpt->bup.oval");
						if (multi_oval > 0)
							fprintf(tb, "s[%d]", jj);
					} else
						putstmnt(tb, v->lft, m);

					fprintf(tb, ", %d);\n\t\t", (i==0)?1:0);
					if (multi_oval > 0)
						jj++;
					break;
			}	}
			jj = multi_oval - ii - 1;

			if (now->val == 1 && multi_oval > 0)
				jj++;	/* new 3.4.0 */

			for (v = now->rgt, i = 0; v; v = v->rgt, i++)
			{	switch(v->lft->ntyp) {
				case CONST:
				case EVAL:
					break;
				default:
					if (!v->lft->sym
					||  strcmp(v->lft->sym->name, "_") != 0)
					{	nocast=1; putstmnt(tb,v->lft,m);
						nocast=0; fprintf(tb, " = trpt->bup.oval");
						if (multi_oval > 0)
							fprintf(tb, "s[%d]", jj);
						fprintf(tb, ";\n\t\t");
					}
					if (multi_oval > 0)
						jj++;
					break;
			}	}
			multi_oval -= ii;
		}
		break;

	case '@':
		fprintf(tb, "p_restor(II);\n\t\t");
		break;

	case ASGN:
		nocast=1; putstmnt(tb,now->lft,m);
		nocast=0; fprintf(tb, " = trpt->bup.oval");
		if (multi_oval > 0)
		{	multi_oval--;
			fprintf(tb, "s[%d]", multi_oval-1);
		}
		check_proc(now->rgt, m);
		break;

	case 'c':
		check_proc(now->lft, m);
		break;

	case '.':
	case GOTO:
	case ELSE:
	case BREAK:
		break;

	case C_CODE:
		fprintf(tb, "sv_restor();\n");
		break;

	case ASSERT:
	case PRINT:
		check_proc(now, m);
		break;
	case PRINTM:
		break;

	default:
		printf("spin: bad node type %d (.b)\n", now->ntyp);
		alldone(1);
	}
}

int
any_undo(Lextok *now)
{	/* is there anything to undo on a return move? */
	if (!now) return 1;
	switch (now->ntyp) {
	case 'c':	return any_oper(now->lft, RUN);
	case ASSERT:
	case PRINT:	return any_oper(now, RUN);

	case PRINTM:
	case   '.':
	case  GOTO:
	case  ELSE:
	case BREAK:	return 0;
	default:	return 1;
	}
}

int
any_oper(Lextok *now, int oper)
{	/* check if an expression contains oper operator */
	if (!now) return 0;
	if (now->ntyp == oper)
		return 1;
	return (any_oper(now->lft, oper) || any_oper(now->rgt, oper));
}

static void
check_proc(Lextok *now, int m)
{
	if (!now)
		return;
	if (now->ntyp == '@' || now->ntyp == RUN)
	{	fprintf(tb, ";\n\t\t");
		undostmnt(now, m);
	}
	check_proc(now->lft, m);
	check_proc(now->rgt, m);
}

void
genunio(void)
{	char buf1[256];
	Queue *q; int i;

	ntimes(tc, 0, 1, R13);
	for (q = qtab; q; q = q->nxt)
	{	fprintf(tc, "\tcase %d:\n", q->qid);

		if (has_sorted)
		{	sprintf(buf1, "((Q%d *)z)->contents", q->qid);
			fprintf(tc, "#ifdef HAS_SORTED\n");
			fprintf(tc, "\t\tj = trpt->ipt;\n");	/* ipt was bup.oval */
			fprintf(tc, "#endif\n");
			fprintf(tc, "\t\tfor (k = j; k < ((Q%d *)z)->Qlen; k++)\n",
				q->qid);
			fprintf(tc, "\t\t{\n");
			for (i = 0; i < q->nflds; i++)
			fprintf(tc, "\t\t\t%s[k].fld%d = %s[k+1].fld%d;\n",
				buf1, i, buf1, i);
			fprintf(tc, "\t\t}\n");
			fprintf(tc, "\t\tj = ((Q0 *)z)->Qlen;\n");
		}

		sprintf(buf1, "((Q%d *)z)->contents[j].fld", q->qid);
		for (i = 0; i < q->nflds; i++)
			fprintf(tc, "\t\t%s%d = 0;\n", buf1, i);
		if (q->nslots==0)
		{	/* check if rendezvous succeeded, 1 level down */
			fprintf(tc, "\t\t_m = (trpt+1)->o_m;\n");
			fprintf(tc, "\t\tif (_m) (trpt-1)->o_pm |= 1;\n");
			fprintf(tc, "\t\tUnBlock;\n");
		} else
			fprintf(tc, "\t\t_m = trpt->o_m;\n");

		fprintf(tc, "\t\tbreak;\n");
	}
	ntimes(tc, 0, 1, R14);
	for (q = qtab; q; q = q->nxt)
	{	sprintf(buf1, "((Q%d *)z)->contents", q->qid);
		fprintf(tc, "	case %d:\n", q->qid);
		if (q->nslots == 0)
			fprintf(tc, "\t\tif (strt) boq = from+1;\n");
		else if (q->nslots > 1)	/* shift */
		{	fprintf(tc, "\t\tif (strt && slot<%d)\n",
							q->nslots-1);
			fprintf(tc, "\t\t{\tfor (j--; j>=slot; j--)\n");
			fprintf(tc, "\t\t\t{");
			for (i = 0; i < q->nflds; i++)
			{	fprintf(tc, "\t%s[j+1].fld%d =\n\t\t\t",
							buf1, i);
				fprintf(tc, "\t%s[j].fld%d;\n\t\t\t",
							buf1, i);
			}
			fprintf(tc, "}\n\t\t}\n");
		}
		strcat(buf1, "[slot].fld");
		fprintf(tc, "\t\tif (strt) {\n");
		for (i = 0; i < q->nflds; i++)
			fprintf(tc, "\t\t\t%s%d = 0;\n", buf1, i);
		fprintf(tc, "\t\t}\n");
		if (q->nflds == 1)	/* set */
			fprintf(tc, "\t\tif (fld == 0) %s0 = fldvar;\n",
							buf1);
		else
		{	fprintf(tc, "\t\tswitch (fld) {\n");
			for (i = 0; i < q->nflds; i++)
			{	fprintf(tc, "\t\tcase %d:\t%s", i, buf1);
				fprintf(tc, "%d = fldvar; break;\n", i);
			}
			fprintf(tc, "\t\t}\n");
		}
		fprintf(tc, "\t\tbreak;\n");
	}
	ntimes(tc, 0, 1, R15);
}

extern void explain(int);

int
proper_enabler(Lextok *n)
{
	if (!n) return 1;
	switch (n->ntyp) {
	case NEMPTY:	case FULL:
	case NFULL:	case EMPTY:
	case LEN:	case 'R':
	case NAME:
		has_provided = 1;
		if (strcmp(n->sym->name, "_pid") == 0)
			return 1;
		return (!(n->sym->context));

	case C_EXPR:
	case CONST:
	case TIMEOUT:
		has_provided = 1;
		return 1;

	case ENABLED:	case PC_VAL:
		return proper_enabler(n->lft);

	case '!': case UMIN: case '~':
		return proper_enabler(n->lft);

	case '/': case '*': case '-': case '+':
	case '%': case LT:  case GT: case '&': case '^':
	case '|': case LE:  case GE:  case NE: case '?':
	case EQ:  case OR:  case AND: case LSHIFT:
	case RSHIFT: case 'c':
		return proper_enabler(n->lft) && proper_enabler(n->rgt);
	default:
		break;
	}
	printf("spin: saw ");
	explain(n->ntyp);
	printf("\n");
	return 0;
}
Commit	Line	Data
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	}