pangen2.c

对软件进行可达性测试的软件

		if (n->sym->context
		|| (n->sym->hidden&64)
		||  strcmp(n->sym->name, "_pid") == 0
		||  strcmp(n->sym->name, "_") == 0)
			return 0;
		return 1;

	case RUN:
		return proc_is_safe(n);

	case C_CODE: case C_EXPR:
		return glob_inline(n->sym->name);

	case ENABLED: case PC_VAL: case NONPROGRESS:
	case 'p': case 'q':
	case TIMEOUT:
		return 1;

	/* 	@ was 1 (global) since 2.8.5
		in 3.0 it is considered local and
		conditionally safe, provided:
			II is the youngest process
			and nrprocs < MAXPROCS
	*/
	case '@': return 0;

	case '!': case UMIN: case '~': case ASSERT:
		return has_global(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': case ASGN:
		return has_global(n->lft) || has_global(n->rgt);

	case PRINT:
		for (v = n->lft; v; v = v->rgt)
			if (has_global(v->lft)) return 1;
		return 0;
	case PRINTM:
		return has_global(n->lft);
	}
	return 0;
}

static void
Bailout(FILE *fd, char *str)
{
	if (!GenCode)
		fprintf(fd, "continue%s", str);
	else if (IsGuard)
		fprintf(fd, "%s%s", NextLab[Level], str);
	else
		fprintf(fd, "Uerror(\"block in step seq\")%s", str);
}

#define cat0(x)   	putstmnt(fd,now->lft,m); fprintf(fd, x); \
			putstmnt(fd,now->rgt,m)
#define cat1(x)		fprintf(fd,"("); cat0(x); fprintf(fd,")")
#define cat2(x,y)  	fprintf(fd,x); putstmnt(fd,y,m)
#define cat3(x,y,z)	fprintf(fd,x); putstmnt(fd,y,m); fprintf(fd,z)

void
putstmnt(FILE *fd, Lextok *now, int m)
{	Lextok *v;
	int i, j;

	if (!now) { fprintf(fd, "0"); return; }
	lineno = now->ln;
	Fname  = now->fn;

	switch (now->ntyp) {
	case CONST:	fprintf(fd, "%d", now->val); break;
	case '!':	cat3(" !(", now->lft, ")"); break;
	case UMIN:	cat3(" -(", now->lft, ")"); break;
	case '~':	cat3(" ~(", now->lft, ")"); break;

	case '/':	cat1("/");  break;
	case '*':	cat1("*");  break;
	case '-':	cat1("-");  break;
	case '+':	cat1("+");  break;
	case '%':	cat1("%%"); break;
	case '&':	cat1("&");  break;
	case '^':	cat1("^");  break;
	case '|':	cat1("|");  break;
	case LT:	cat1("<");  break;
	case GT:	cat1(">");  break;
	case LE:	cat1("<="); break;
	case GE:	cat1(">="); break;
	case NE:	cat1("!="); break;
	case EQ:	cat1("=="); break;
	case OR:	cat1("||"); break;
	case AND:	cat1("&&"); break;
	case LSHIFT:	cat1("<<"); break;
	case RSHIFT:	cat1(">>"); break;

	case TIMEOUT:
		if (separate == 2)
			fprintf(fd, "((tau)&1)");
		else
			fprintf(fd, "((trpt->tau)&1)");
		if (GenCode)
		 printf("spin: line %3d, warning: 'timeout' in d_step sequence\n",
			lineno);
		/* is okay as a guard */
		break;

	case RUN:
		if (now->sym == NULL)
			Fatal("internal error pangen2.c", (char *) 0);
		if (claimproc
		&&  strcmp(now->sym->name, claimproc) == 0)
			fatal("claim %s, (not runnable)", claimproc);
		if (eventmap
		&&  strcmp(now->sym->name, eventmap) == 0)
			fatal("eventmap %s, (not runnable)", eventmap);

		if (GenCode)
		  fatal("'run' in d_step sequence (use atomic)",
			(char *)0);

		fprintf(fd,"addproc(%d", fproc(now->sym->name));
		for (v = now->lft, i = 0; v; v = v->rgt, i++)
		{	cat2(", ", v->lft);
		}
		check_param_count(i, now);

		if (i > Npars)
		{	/* printf("\t%d parameters used, max %d expected\n", i, Npars); */
			fatal("too many parameters in run %s(...)", now->sym->name);
		}
		for ( ; i < Npars; i++)
			fprintf(fd, ", 0");
		fprintf(fd, ")");
		break;

	case ENABLED:
		cat3("enabled(II, ", now->lft, ")");
		break;

	case NONPROGRESS:
		/* o_pm&4=progress, tau&128=claim stutter */
		if (separate == 2)
		fprintf(fd, "(!(o_pm&4) && !(tau&128))");
		else
		fprintf(fd, "(!(trpt->o_pm&4) && !(trpt->tau&128))");
		break;

	case PC_VAL:
		cat3("((P0 *) Pptr(", now->lft, "+BASE))->_p");
		break;

	case LEN:
		if (!terse && !TestOnly && has_xu)
		{	fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
			putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
			putname(fd, "q_R_check(", now->lft, m, "");
			fprintf(fd, ", II)) &&\n\t\t");
			putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
			putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
			fprintf(fd, "\n#endif\n\t\t");
		}
		putname(fd, "q_len(", now->lft, m, ")");
		break;

	case FULL:
		if (!terse && !TestOnly && has_xu)
		{	fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
			putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
			putname(fd, "q_R_check(", now->lft, m, "");
			fprintf(fd, ", II)) &&\n\t\t");
			putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
			putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
			fprintf(fd, "\n#endif\n\t\t");
		}
		putname(fd, "q_full(", now->lft, m, ")");
		break;

	case EMPTY:
		if (!terse && !TestOnly && has_xu)
		{	fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
			putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
			putname(fd, "q_R_check(", now->lft, m, "");
			fprintf(fd, ", II)) &&\n\t\t");
			putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
			putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
			fprintf(fd, "\n#endif\n\t\t");
		}
		putname(fd, "(q_len(", now->lft, m, ")==0)");
		break;

	case NFULL:
		if (!terse && !TestOnly && has_xu)
		{	fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
			putname(fd, "(!(q_claim[", now->lft, m, "]&2) || ");
			putname(fd, "q_S_check(", now->lft, m, ", II)) &&");
			fprintf(fd, "\n#endif\n\t\t");
		}
		putname(fd, "(!q_full(", now->lft, m, "))");
		break;

	case NEMPTY:
		if (!terse && !TestOnly && has_xu)
		{	fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
			putname(fd, "(!(q_claim[", now->lft, m, "]&1) || ");
			putname(fd, "q_R_check(", now->lft, m, ", II)) &&");
			fprintf(fd, "\n#endif\n\t\t");
		}
		putname(fd, "(q_len(", now->lft, m, ")>0)");
		break;

	case 's':
		if (Pid == eventmapnr)
		{	fprintf(fd, "if ((ot == EVENT_TRACE && _tp != 's') ");
			putname(fd, "|| _qid+1 != ", now->lft, m, "");
			for (v = now->rgt, i=0; v; v = v->rgt, i++)
			{	if (v->lft->ntyp != CONST
				&&  v->lft->ntyp != EVAL)
					continue;
				fprintf(fd, " \\\n\t\t|| qrecv(");
				putname(fd, "", now->lft, m, ", ");
				putname(fd, "q_len(", now->lft, m, ")-1, ");
				fprintf(fd, "%d, 0) != ", i);
				if (v->lft->ntyp == CONST)
					putstmnt(fd, v->lft, m);
				else /* EVAL */
					putstmnt(fd, v->lft->lft, m);
			}
			fprintf(fd, ")\n");
			fprintf(fd, "\t\t	continue");
			putname(th, " || (x_y3_ == ", now->lft, m, ")");
			break;
		}
		if (TestOnly)
		{	if (m_loss)
				fprintf(fd, "1");
			else
				putname(fd, "!q_full(", now->lft, m, ")");
			break;
		}
		if (has_xu)
		{	fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
			putname(fd, "if (q_claim[", now->lft, m, "]&2) ");
			putname(fd, "q_S_check(", now->lft, m, ", II);");
			fprintf(fd, "\n#endif\n\t\t");
		}
		fprintf(fd, "if (q_%s",
			(u_sync > 0 && u_async == 0)?"len":"full");
		putname(fd, "(", now->lft, m, "))\n");

		if (m_loss)
			fprintf(fd, "\t\t{ nlost++; delta_m = 1; } else {");
		else
		{	fprintf(fd, "\t\t\t");
			Bailout(fd, ";");
		}

		if (has_enabled)
			fprintf(fd, "\n\t\tif (TstOnly) return 1;");

		if (u_sync && !u_async && rvopt)
			fprintf(fd, "\n\n\t\tif (no_recvs(II)) continue;\n");

		fprintf(fd, "\n#ifdef HAS_CODE\n");
		fprintf(fd, "\t\tif (readtrail && gui) {\n");
		fprintf(fd, "\t\t\tchar simtmp[32];\n");
		putname(fd, "\t\t\tsprintf(simvals, \"%%d!\", ", now->lft, m, ");\n");
		_isok++;
		for (v = now->rgt, i = 0; v; v = v->rgt, i++)
		{	cat3("\t\tsprintf(simtmp, \"%%d\", ", v->lft, "); strcat(simvals, simtmp);");
			if (v->rgt)
			fprintf(fd, "\t\tstrcat(simvals, \",\");\n");
		}
		_isok--;
		fprintf(fd, "\t\t}\n");
		fprintf(fd, "#endif\n\t\t");

		putname(fd, "\n\t\tqsend(", now->lft, m, "");
		fprintf(fd, ", %d", now->val);
		for (v = now->rgt, i = 0; v; v = v->rgt, i++)
		{	cat2(", ", v->lft);
		}
		if (i > Mpars)
		{	terse++;
			putname(stdout, "channel name: ", now->lft, m, "\n");
			terse--;
			printf("	%d msg parameters sent, %d expected\n", i, Mpars);
			fatal("too many pars in send", "");
		}
		for (j = i; i < Mpars; i++)
			fprintf(fd, ", 0");
		fprintf(fd, ", %d)", j);
		if (u_sync)
		{	fprintf(fd, ";\n\t\t");
			if (u_async)
			  putname(fd, "if (q_zero(", now->lft, m, ")) ");
			putname(fd, "{ boq = ", now->lft, m, "");
			if (GenCode)
			  fprintf(fd, "; Uerror(\"rv-attempt in d_step\")");
			fprintf(fd, "; }");
		}
		if (m_loss)
			fprintf(fd, ";\n\t\t}\n\t\t"); /* end of m_loss else */
		break;

	case 'r':
		if (Pid == eventmapnr)
		{	fprintf(fd, "if ((ot == EVENT_TRACE && _tp != 'r') ");
			putname(fd, "|| _qid+1 != ", now->lft, m, "");
			for (v = now->rgt, i=0; v; v = v->rgt, i++)
			{	if (v->lft->ntyp != CONST
				&&  v->lft->ntyp != EVAL)
					continue;
				fprintf(fd, " \\\n\t\t|| qrecv(");
				putname(fd, "", now->lft, m, ", ");
				fprintf(fd, "0, %d, 0) != ", i);
				if (v->lft->ntyp == CONST)
					putstmnt(fd, v->lft, m);
				else /* EVAL */
					putstmnt(fd, v->lft->lft, m);
			}
			fprintf(fd, ")\n");
			fprintf(fd, "\t\t	continue");

			putname(tc, " || (x_y3_ == ", now->lft, m, ")");

			break;
		}
		if (TestOnly)
		{	fprintf(fd, "((");
			if (u_sync) fprintf(fd, "(boq == -1 && ");

			putname(fd, "q_len(", now->lft, m, ")");

			if (u_sync && now->val <= 1)
			{ putname(fd, ") || (boq == ",  now->lft,m," && ");
			  putname(fd, "q_zero(", now->lft,m,"))");
			}

			fprintf(fd, ")");
			if (now->val == 0 || now->val == 2)
			{	for (v = now->rgt, i=j=0; v; v = v->rgt, i++)
				{ if (v->lft->ntyp == CONST)
				  { cat3("\n\t\t&& (", v->lft, " == ");
				    putname(fd, "qrecv(", now->lft, m, ", ");
				    fprintf(fd, "0, %d, 0))", i);
				  } else if (v->lft->ntyp == EVAL)
				  { cat3("\n\t\t&& (", v->lft->lft, " == ");
				    putname(fd, "qrecv(", now->lft, m, ", ");
				    fprintf(fd, "0, %d, 0))", i);
				  } else
				  {	j++; continue;
				  }
				}
			} else
			{	fprintf(fd, "\n\t\t&& Q_has(");
				putname(fd, "", now->lft, m, "");
				for (v = now->rgt, i=0; v; v = v->rgt, i++)
				{	if (v->lft->ntyp == CONST)
					{	fprintf(fd, ", 1, ");
						putstmnt(fd, v->lft, m);
					} else if (v->lft->ntyp == EVAL)
					{	fprintf(fd, ", 1, ");
						putstmnt(fd, v->lft->lft, m);
					} else
					{	fprintf(fd, ", 0, 0");
				}	}
				for ( ; i < Mpars; i++)
					fprintf(fd, ", 0, 0");
				fprintf(fd, ")");
			}
			fprintf(fd, ")");
			break;
		}
		if (has_xu)
		{	fprintf(fd, "\n#ifndef XUSAFE\n\t\t");
			putname(fd, "if (q_claim[", now->lft, m, "]&1) ");
			putname(fd, "q_R_check(", now->lft, m, ", II);");
			fprintf(fd, "\n#endif\n\t\t");
		}
		if (u_sync)
		{	if (now->val >= 2)
			{	if (u_async)
				{ fprintf(fd, "if (");
				  putname(fd, "q_zero(", now->lft,m,"))");
				  fprintf(fd, "\n\t\t{\t");
				}
				fprintf(fd, "uerror(\"polling ");
				fprintf(fd, "rv chan\");\n\t\t");
				if (u_async)
				  fprintf(fd, "	continue;\n\t\t}\n\t\t");
				fprintf(fd, "IfNotBlocked\n\t\t");
			} else
			{	fprintf(fd, "if (");
				if (u_async == 0)
				  putname(fd, "boq != ", now->lft,m,") ");
				else
				{ putname(fd, "q_zero(", now->lft,m,"))");
				  fprintf(fd, "\n\t\t{\tif (boq != ");
				  putname(fd, "",  now->lft,m,") ");
				  Bailout(fd, ";\n\t\t} else\n\t\t");
				  fprintf(fd, "{\tif (boq != -1) ");
				}
				Bailout(fd, ";\n\t\t");
				if (u_async)
					fprintf(fd, "}\n\t\t");
		}	}
		putname(fd, "if (q_len(", now->lft, m, ") == 0) ");
		Bailout(fd, "");

		for (v = now->rgt, j=0; v; v = v->rgt)
		{	if (v->lft->ntyp != CONST
			&&  v->lft->ntyp != EVAL)
				j++;	/* count settables */
		}
		fprintf(fd, ";\n\n\t\tXX=1");
/* test */	if (now->val == 0 || now->val == 2)
		{	for (v = now->rgt, i=0; v; v = v->rgt, i++)
			{	if (v->lft->ntyp == CONST)
				{ fprintf(fd, ";\n\t\t");
				  cat3("if (", v->lft, " != ");
				  putname(fd, "qrecv(", now->lft, m, ", ");
				  fprintf(fd, "0, %d, 0)) ", i);
				  Bailout(fd, "");
				} else if (v->lft->ntyp == EVAL)
				{ fprintf(fd, ";\n\t\t");
				  cat3("if (", v->lft->lft, " != ");
				  putname(fd, "qrecv(", now->lft, m, ", ");
				  fprintf(fd, "0, %d, 0)) ", i);
				  Bailout(fd, "");
			}	}
		} else	/* random receive: val 1 or 3 */
		{	fprintf(fd, ";\n\t\tif (!(XX = Q_has(");
			putname(fd, "", now->lft, m, "");
			for (v = now->rgt, i=0; v; v = v->rgt, i++)
			{	if (v->lft->ntyp == CONST)
				{	fprintf(fd, ", 1, ");
					putstmnt(fd, v->lft, m);
				} else if (v->lft->ntyp == EVAL)
				{	fprintf(fd, ", 1, ");
					putstmnt(fd, v->lft->lft, m);
				} else
				{	fprintf(fd, ", 0, 0");
			}	}
			for ( ; i < Mpars; i++)
				fprintf(fd, ", 0, 0");
			fprintf(fd, "))) ");
			Bailout(fd, "");
			fprintf(fd, ";\n\t\t");
			if (multi_oval)
			{	check_needed();
				fprintf(fd, "(trpt+1)->bup.ovals[%d] = ",
					multi_oval-1);
				multi_oval++;
			} else
				fprintf(fd, "(trpt+1)->bup.oval = ");
			fprintf(fd, "XX");
		}

		if (has_enabled)
			fprintf(fd, ";\n\t\tif (TstOnly) return 1");

		if (j == 0 && now->val >= 2)
		{	fprintf(fd, ";\n\t\t");
			break;	/* poll without side-effect */
		}

		if (!GenCode)
		{	int jj = 0;
			fprintf(fd, ";\n\t\t");
			/* no variables modified */
			if (j == 0 && now->val == 0)
			{	fprintf(fd, "if (q_flds[((Q0 *)qptr(");
				putname(fd, "", now->lft, m, "-1))->_t]");
				fprintf(fd, " != %d)\n\t", i);
				fprintf(fd, "\t\tUerror(\"wrong nr of msg fields in rcv\");\n\t\t");
			}

			for (v = now->rgt; v; v = v->rgt)
				if ((v->lft->ntyp != CONST
				&&   v->lft->ntyp != EVAL))
					jj++;	/* nr of vars needing bup */

			if (jj)
			for (v = now->rgt, i = 0; v; v = v->rgt, i++)
			{	char tempbuf[64];

				if ((v->lft->ntyp == CONST
				||   v->lft->ntyp == EVAL))
					continue;

				if (multi_oval)
				{	check_needed();
					sprintf(tempbuf, "(trpt+1)->bup.ovals[%d] = ",
						multi_oval-1);
					multi_oval++;
				} else
					sprintf(tempbuf, "(trpt+1)->bup.oval = ");

				if (v->lft->sym && !strcmp(v->lft->sym->name, "_"))
				{	fprintf(fd, tempbuf);
					putname(fd, "qrecv(", now->lft, m, "");
					fprintf(fd, ", XX-1, %d, 0);\n\t\t", i);
				} else
				{	_isok++;
					cat3(tempbuf, v->lft, ";\n\t\t"