spinlex.c

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

	getword(c, isdigit_);
	lineno = atoi(yytext);	/* pickup the line number */

	if ((c = Getchar()) == '\n')
		return;	/* no filename */

	if (c != ' ')
		fatal("malformed preprocessor directive - .fname", 0);

	if ((c = Getchar()) != '\"')
		fatal("malformed preprocessor directive - .fname", 0);

	getword(c, notquote);
	if (Getchar() != '\"')
		fatal("malformed preprocessor directive - fname.", 0);

	strcat(yytext, "\"");
	Fname = lookup(yytext);
done:
	while (Getchar() != '\n')
		;
}

void
precondition(char *q)
{	int c, nest = 1;

	for (;;)
	{	c = Getchar();
		*q++ = c;
		switch (c) {
		case '\n':
			lineno++;
			break;
		case '[':
			nest++;
			break;
		case ']':
			if (--nest <= 0)
			{	*--q = '\0';
				return;
			}
			break;
		}
	}
	fatal("cannot happen", (char *) 0); /* unreachable */
}


Symbol *
prep_inline(Symbol *s, Lextok *nms)
{	int c, nest = 1, dln, firstchar, cnr;
	char *p;
	Lextok *t;
	static char Buf1[SOMETHINGBIG], Buf2[RATHERSMALL];
	static int c_code = 1;

	for (t = nms; t; t = t->rgt)
		if (t->lft)
		{	if (t->lft->ntyp != NAME)
			fatal("bad param to inline %s", s?s->name:"--");
			t->lft->sym->hidden |= 32;
		}

	if (!s)	/* C_Code fragment */
	{	s = (Symbol *) emalloc(sizeof(Symbol));
		s->name = (char *) emalloc(strlen("c_code")+26);
		sprintf(s->name, "c_code%d", c_code++);
		s->context = context;
		s->type = CODE_FRAG;
	} else
		s->type = PREDEF;

	p = &Buf1[0];
	Buf2[0] = '\0';
	for (;;)
	{	c = Getchar();
		switch (c) {
		case '[':
			if (s->type != CODE_FRAG)
				goto bad;
			precondition(&Buf2[0]);	/* e.g., c_code [p] { r = p-r; } */
			continue;
		case '{':
			break;
		case '\n':
			lineno++;
			/* fall through */
		case ' ': case '\t': case '\f': case '\r':
			continue;
		default :
			 printf("spin: saw char '%c'\n", c);
bad:			 fatal("bad inline: %s", s->name);
		}
		break;
	}
	dln = lineno;
	if (s->type == CODE_FRAG)
	{	if (verbose&32)
			sprintf(Buf1, "\t/* line %d %s */\n\t\t",
				lineno, Fname->name);
		else
			strcpy(Buf1, "");
	} else
		sprintf(Buf1, "\n#line %d %s\n{", lineno, Fname->name);
	p += strlen(Buf1);
	firstchar = 1;

	cnr = 1; /* not zero */
more:
	*p++ = c = Getchar();
	if (p - Buf1 >= SOMETHINGBIG)
		fatal("inline text too long", 0);
	switch (c) {
	case '\n':
		lineno++;
		cnr = 0;
		break;
	case '{':
		cnr++;
		nest++;
		break;
	case '}':
		cnr++;
		if (--nest <= 0)
		{	*p = '\0';
			if (s->type == CODE_FRAG)
				*--p = '\0';	/* remove trailing '}' */	
			def_inline(s, dln, &Buf1[0], &Buf2[0], nms);
			if (firstchar)
				printf("%3d: %s, warning: empty inline definition (%s)\n",
					dln, Fname->name, s->name);
			return s;	/* normal return */
		}
		break;
	case '#':
		if (cnr == 0)
		{	p--;
			do_directive(c); /* reads to newline */
			break;
		} /* else fall through */
	default:
		firstchar = 0;
	case '\t':
	case ' ':
	case '\f':
		cnr++;
		break;
	}
	goto more;
}

static int
lex(void)
{	int c;

again:
	c = Getchar();
	yytext[0] = (char) c;
	yytext[1] = '\0';
	switch (c) {
	case '\n':		/* newline */
		lineno++;
	case '\r':		/* carriage return */
		goto again;

	case  ' ': case '\t': case '\f':	/* white space */
		goto again;

	case '#':		/* preprocessor directive */
		if (in_comment) goto again;
		do_directive(c);
		goto again;

	case '\"':
		getword(c, notquote);
		if (Getchar() != '\"')
			fatal("string not terminated", yytext);
		strcat(yytext, "\"");
		SymToken(lookup(yytext), STRING)

	case '\'':	/* new 3.0.9 */
		c = Getchar();
		if (c == '\\')
		{	c = Getchar();
			if (c == 'n') c = '\n';
			else if (c == 'r') c = '\r';
			else if (c == 't') c = '\t';
			else if (c == 'f') c = '\f';
		}
		if (Getchar() != '\'' && !in_comment)
			fatal("character quote missing: %s", yytext);
		ValToken(c, CONST)

	default:
		break;
	}

	if (isdigit_(c))
	{	getword(c, isdigit_);
		ValToken(atoi(yytext), CONST)
	}

	if (isalpha_(c) || c == '_')
	{	getword(c, isalnum_);
		if (!in_comment)
		{	c = check_name(yytext);
			if (c) return c;
			/* else fall through */
		}
		goto again;
	}

	switch (c) {
	case '/': c = follow('*', 0, '/');
		  if (!c) { in_comment = 1; goto again; }
		  break;
	case '*': c = follow('/', 0, '*');
		  if (!c) { in_comment = 0; goto again; }
		  break;
	case ':': c = follow(':', SEP, ':'); break;
	case '-': c = follow('>', SEMI, follow('-', DECR, '-')); break;
	case '+': c = follow('+', INCR, '+'); break;
	case '<': c = follow('<', LSHIFT, follow('=', LE, LT)); break;
	case '>': c = follow('>', RSHIFT, follow('=', GE, GT)); break;
	case '=': c = follow('=', EQ, ASGN); break;
	case '!': c = follow('=', NE, follow('!', O_SND, SND)); break;
	case '?': c = follow('?', R_RCV, RCV); break;
	case '&': c = follow('&', AND, '&'); break;
	case '|': c = follow('|', OR, '|'); break;
	case ';': c = SEMI; break;
	default : break;
	}
	Token(c)
}

static struct {
	char *s;	int tok;	int val;	char *sym;
} Names[] = {
	{"active",	ACTIVE,		0,		0},
	{"assert",	ASSERT,		0,		0},
	{"atomic",	ATOMIC,		0,		0},
	{"bit",		TYPE,		BIT,		0},
	{"bool",	TYPE,		BIT,		0},
	{"break",	BREAK,		0,		0},
	{"byte",	TYPE,		BYTE,		0},
	{"c_code",	C_CODE,		0,		0},
	{"c_decl",	C_DECL,		0,		0},
	{"c_expr",	C_EXPR,		0,		0},
	{"c_state",	C_STATE,	0,		0},
	{"c_track",	C_TRACK,	0,		0},
	{"D_proctype",	D_PROCTYPE,	0,		0},
	{"do",		DO,		0,		0},
	{"chan",	TYPE,		CHAN,		0},
	{"else", 	ELSE,		0,		0},
	{"empty",	EMPTY,		0,		0},
	{"enabled",	ENABLED,	0,		0},
	{"eval",	EVAL,		0,		0},
	{"false",	CONST,		0,		0},
	{"fi",		FI,		0,		0},
	{"full",	FULL,		0,		0},
	{"goto",	GOTO,		0,		0},
	{"hidden",	HIDDEN,		0,		":hide:"},
	{"if",		IF,		0,		0},
	{"init",	INIT,		0,		":init:"},
	{"int",		TYPE,		INT,		0},
	{"len",		LEN,		0,		0},
	{"local",	ISLOCAL,	0,		":local:"},
	{"mtype",	TYPE,		MTYPE,		0},
	{"nempty",	NEMPTY,		0,		0},
	{"never",	CLAIM,		0,		":never:"},
	{"nfull",	NFULL,		0,		0},
	{"notrace",	TRACE,		0,		":notrace:"},
	{"np_",		NONPROGRESS,	0,		0},
	{"od",		OD,		0,		0},
	{"of",		OF,		0,		0},
	{"pc_value",	PC_VAL,		0,		0},
	{"pid",		TYPE,		BYTE,		0},
	{"printf",	PRINT,		0,		0},
	{"printm",	PRINTM,		0,		0},
	{"priority",	PRIORITY,	0,		0},
	{"proctype",	PROCTYPE,	0,		0},
	{"provided",	PROVIDED,	0,		0},
	{"run",		RUN,		0,		0},
	{"d_step",	D_STEP,		0,		0},
	{"inline",	INLINE,		0,		0},
	{"short",	TYPE,		SHORT,		0},
	{"skip",	CONST,		1,		0},
	{"timeout",	TIMEOUT,	0,		0},
	{"trace",	TRACE,		0,		":trace:"},
	{"true",	CONST,		1,		0},
	{"show",	SHOW,		0,		":show:"},
	{"typedef",	TYPEDEF,	0,		0},
	{"unless",	UNLESS,		0,		0},
	{"unsigned",	TYPE,		UNSIGNED,	0},
	{"xr",		XU,		XR,		0},
	{"xs",		XU,		XS,		0},
	{0, 		0,		0,		0},
};

static int
check_name(char *s)
{	int i;

	yylval = nn(ZN, 0, ZN, ZN);
	for (i = 0; Names[i].s; i++)
		if (strcmp(s, Names[i].s) == 0)
		{	yylval->val = Names[i].val;
			if (Names[i].sym)
				yylval->sym = lookup(Names[i].sym);
			return Names[i].tok;
		}

	if ((yylval->val = ismtype(s)) != 0)
	{	yylval->ismtyp = 1;
		return CONST;
	}

	if (strcmp(s, "_last") == 0)
		has_last++;

	if (Inlining >= 0 && !ReDiRect)
	{	Lextok *tt, *t = Inline_stub[Inlining]->params;

		for (i = 0; t; t = t->rgt, i++)				/* formal pars */
		 if (!strcmp(s, t->lft->sym->name)			/* varname matches formal */
		 &&   strcmp(s, Inline_stub[Inlining]->anms[i]) != 0)	/* actual pars */
		 {
#if 0
			if (verbose&32)
			printf("\tline %d, replace %s in call of '%s' with %s\n",
				lineno, s,
				Inline_stub[Inlining]->nm->name,
				Inline_stub[Inlining]->anms[i]);
#endif
			
			for (tt = Inline_stub[Inlining]->params; tt; tt = tt->rgt)
				if (!strcmp(Inline_stub[Inlining]->anms[i],
					tt->lft->sym->name))
				{	/* would be cyclic if not caught */
					printf("spin: line %d replacement value: %s\n",
						lineno, tt->lft->sym->name);
					fatal("formal par of %s matches replacement value",
						Inline_stub[Inlining]->nm->name);
					yylval->ntyp = tt->lft->ntyp;
					yylval->sym = lookup(tt->lft->sym->name);
					return NAME;
				}
			ReDiRect = Inline_stub[Inlining]->anms[i];
			return 0;
	}	 }

	yylval->sym = lookup(s);	/* symbol table */
	if (isutype(s))
		return UNAME;
	if (isproctype(s))
		return PNAME;
	if (iseqname(s))
		return INAME;

	return NAME;
}

int
yylex(void)
{	static int last = 0;
	static int hold = 0;
	int c;
	/*
	 * repair two common syntax mistakes with
	 * semi-colons before or after a '}'
	 */
	if (hold)
	{	c = hold;
		hold = 0;
	} else
	{	c = lex();
		if (last == ELSE
		&&  c != SEMI
		&&  c != FI)
		{	hold = c;
			last = 0;
			return SEMI;
		}
		if (last == '}'
		&&  c != PROCTYPE
		&&  c != INIT
		&&  c != CLAIM
		&&  c != SEP
		&&  c != FI
		&&  c != OD
		&&  c != '}'
		&&  c != UNLESS
		&&  c != SEMI
		&&  c != EOF)
		{	hold = c;
			last = 0;
			return SEMI;	/* insert ';' */
		}
		if (c == SEMI)
		{	/* if context, we're not in a typedef
			 * because they're global.
			 * if owner, we're at the end of a ref
			 * to a struct field -- prevent that the
			 * lookahead is interpreted as a field of
			 * the same struct...
			 */
			if (context) owner = ZS;
			hold = lex();	/* look ahead */
			if (hold == '}'
			||  hold == SEMI)
			{	c = hold; /* omit ';' */
				hold = 0;
			}
		}
	}
	last = c;

	if (IArgs)
	{	static int IArg_nst = 0;

		if (strcmp(yytext, ",") == 0)
		{	IArg_cont[++IArgno][0] = '\0';
		} else if (strcmp(yytext, "(") == 0)
		{	if (IArg_nst++ == 0)
			{	IArgno = 0;
				IArg_cont[0][0] = '\0';
			} else
				strcat(IArg_cont[IArgno], yytext);
		} else if (strcmp(yytext, ")") == 0)
		{	if (--IArg_nst > 0)
				strcat(IArg_cont[IArgno], yytext);
		} else if (c == CONST && yytext[0] == '\'')
		{	sprintf(yytext, "'%c'", yylval->val);
			strcat(IArg_cont[IArgno], yytext);
		} else
		{
			switch (c) {
			case SEP:	strcpy(yytext, "::"); break;
			case SEMI:	strcpy(yytext, ";"); break;
			case DECR:	strcpy(yytext, "--"); break;
			case INCR: 	strcpy(yytext, "++"); break;
			case LSHIFT:	strcpy(yytext, "<<"); break;
			case RSHIFT:	strcpy(yytext, ">>"); break;
			case LE:	strcpy(yytext, "<="); break;
			case LT:	strcpy(yytext, "<"); break;
			case GE:	strcpy(yytext, ">="); break;
			case GT:	strcpy(yytext, ">"); break;
			case EQ:	strcpy(yytext, "=="); break;
			case ASGN:	strcpy(yytext, "="); break;
			case NE:	strcpy(yytext, "!="); break;
			case R_RCV:	strcpy(yytext, "??"); break;
			case RCV:	strcpy(yytext, "?"); break;
			case O_SND:	strcpy(yytext, "!!"); break;
			case SND:	strcpy(yytext, "!"); break;
			case AND: 	strcpy(yytext, "&&"); break;
			case OR:	strcpy(yytext, "||"); break;
			}
			strcat(IArg_cont[IArgno], yytext);
		}
	}

	return c;
}