uno_generic.c

C程序漏洞检查！

				}
w = 6;
				goto unknown;			/* cannot tell */
			}
		}
	}
	if (!anyhits) goto unknown;

	if (debug)
	{	fprintf(stderr, "+preknown (want=%d) <%s>:\n", want, x_stmnt(m));
		if (s) fprintf(stderr, "	-- symbol %s -- v=%d\n", s->sm->nme->str, v);
		if (g) fprintf(stderr, " -- step <%s>\n", x_stmnt(g->e));
		if (g) fprintf(stderr, " -- cond <%s>\n", x_stmnt(g->c));
	}
	return 1;
unknown:
	if (debug)
	{	fprintf(stderr, "-preknown (want=%d) <%s> -- w=%d:\n", want, x_stmnt(m), w);
		if (s) fprintf(stderr, "	-- symbol %s -- v=%d\n", s->sm->nme->str, v);
		if (g) fprintf(stderr, " -- step <%s>\n", x_stmnt(g->e));
		if (g) fprintf(stderr, " -- cond <%s>\n", x_stmnt(g->c));
	}
	return 0;
}
static int
known_zero(treenode *m, int unused1, int unused2)
{	int r = known_details(m, 1);
	if (debug) fprintf(stderr, ">>knowzero returns %d\n", r);
	return r;
}
static int
known_nonzero(treenode *m, int unused1, int unused2)
{	int r = known_details(m, -1);
	if (debug) fprintf(stderr, ">>know_nonzero returns %d\n", r);
	return r;
}


static void
do_nothing(treenode *m, int x, int y)
{
	return;
}

static void
list_select(treenode *n, int x, int y)	/* x and y not used */
{	SymRef *s;
	SymList *r;
	int cnt = 0;

	if (n)
		printf("uno: %s:%d: symbols (*=selected):\n",
			n->hdr.fnm, n->hdr.line);
	else
		printf("uno: symbols (*=selected):\n");

	for (s = gen_stack->symrefs; s; s = s->nxt)
		{	printf("	%3d%s:\t%s [",
				++cnt,
				(s->status & SELECTED)?"*":"",
				s->sm->nme->str);
			dflow_mark(stdout, s->status);
			printf("]	(stack - mark %d)\n", s->s_val);
		}

	if (n && n->hdr.defuse)
	for (r = n->hdr.defuse->other; r; r = r->nxt)
		{	printf("	%3d%s:	%s [",
				++cnt,
				r->selected?"*":"",
				r->sm->nme->str);
			dflow_mark(stdout, r->mark);
			printf("]	(stmnt)\n");
		}
}

static void
sym_add(treenode *m, int allow, int forbid)
{	SymRef *s;
	SymList *r;
	treenode *n;

	n = (m && m->hdr.type == TN_IF) ? ((if_node *)m)->cond : m;
	if (!n || !n->hdr.defuse)
	{	if (debug) printf("	symadd - nothing to add\n");
		return;
	}

	for (r = n->hdr.defuse->other; r; r = r->nxt)
	{	if (debug) printf("\tsymadd sees %s mark %d, looking for %d & !%d\n",
			r->sm->nme->str, r->mark, allow, forbid);

		if ((r->mark & allow) && !(r->mark & forbid))
		{	for (s = gen_stack->symrefs; s; s = s->nxt)
				if (strcmp(s->sm->nme->str, r->sm->nme->str) == 0
				&&  s->status == r->mark)
				{	if (debug) printf("\tsymadd %s - already there\n",
						s->sm->nme->str);
					break;
				}
			if (!s)
			{	s = uno_getref(r->sm);
				s->nxt = gen_stack->symrefs;
				s->status = r->mark;
				s->n = n;
				gen_stack->symrefs = s;
				if (debug) printf("\tadded %s (line %d)\n",
					s->sm->nme->str, s->n?s->n->hdr.line:-1);
		}	}
	}
	if (debug) printf("\tsymadd - done\n");
}

static void
sym_del(treenode *m, int allow, int forbid)
{	SymRef *s, *os;
	SymList *r;
	treenode *n;

	n = (m && m->hdr.type == TN_IF) ? ((if_node *)m)->cond : m;

	if (n && n->hdr.defuse)
	for (r = n->hdr.defuse->other; r; r = r->nxt)
	{	if ((r->mark & allow) && !(r->mark & forbid))
		{	os = (SymRef *) 0;
again:			for (s = gen_stack->symrefs; s; os = s, s = s->nxt)
			{	if (strcmp(s->sm->nme->str, r->sm->nme->str) == 0
				&&  (s->status & allow)
				&& !(s->status & forbid))
				{	if (!os)
						gen_stack->symrefs = s->nxt;
					else
						os->nxt = s->nxt;

					if (debug) printf("\tdeleted %s\n",
						s->sm->nme->str);

					goto again;
	}	}	}	}
}

static void
sym_del_name(treenode *m, int allow, int forbid)
{	SymRef *s, *os;
	SymList *r;
	treenode *n;

	n = (m && m->hdr.type == TN_IF) ? ((if_node *)m)->cond : m;

	if (n && n->hdr.defuse)
	for (r = n->hdr.defuse->other; r; r = r->nxt)
	{	if ((r->mark & allow) && !(r->mark & forbid))
		{	os = (SymRef *) 0;
again:			for (s = gen_stack->symrefs; s; os = s, s = s->nxt)
			{	if (strcmp(s->sm->nme->str, r->sm->nme->str) == 0)
				{	if (!os)
						gen_stack->symrefs = s->nxt;
					else
						os->nxt = s->nxt;

					if (debug) printf("\tdeleted %s\n",
						s->sm->nme->str);

					goto again;
	}	}	}	}
}

static int
on_track(treenode *m, int allow, int forbid)
{	SymRef *s;
	SymList *r;
	treenode *n;

	n = (m && m->hdr.type == TN_IF) ? ((if_node *)m)->cond : m;

	if (n && n->hdr.defuse)
	for (r = n->hdr.defuse->other; r; r = r->nxt)
		if ((r->mark & allow) && !(r->mark & forbid))
		{	for (s = gen_stack->symrefs; s; s = s->nxt)
			{	if (strcmp(s->sm->nme->str, r->sm->nme->str) == 0
				&&  (s->status & allow)
				&& !(s->status & forbid))
				{	if (m != s->n)
						witness = s->n;
					if (debug) printf("\tsym present %s (line %d)\n",
						r->sm->nme->str, s->n?s->n->hdr.line:-1);
					return 1;
		}	}	}

	if (debug)
	{	printf("on_track: no matching syms\n");
		if (n && n->hdr.defuse)
		for (r = n->hdr.defuse->other; r; r = r->nxt)
			printf("\tdefuse have %s %d\n", r->sm->nme->str, r->mark);
		for (s = gen_stack->symrefs; s; s = s->nxt)
			printf("\tgenstack have %s %d\n", s->sm->nme->str, s->status);
	}
	return 0;
}

static int
match_track(treenode *m, int allow, int forbid)
{	SymRef *s;
	SymList *r;
	treenode *n;	/* var with allow and !forbid on defuse - that is also on_track? */

	n = (m && m->hdr.type == TN_IF) ? ((if_node *)m)->cond : m;

	if (n && n->hdr.defuse)
	for (r = n->hdr.defuse->other; r; r = r->nxt)
		if ((r->mark & allow) && !(r->mark & forbid))
		{	for (s = gen_stack->symrefs; s; s = s->nxt)
			{	if (strcmp(s->sm->nme->str, r->sm->nme->str) == 0)
				{	if (m != s->n)
						witness = s->n;
					if (debug) printf("\tsym matched %s (line %d)\n",
						r->sm->nme->str, s->n?s->n->hdr.line:-1);
					return 1;
		}	}	}

	if (debug) printf("match_track: no matching syms\n");
	return 0;
}

static int
any_track(treenode *m, int allow, int forbid)
{	SymRef *s;

	for (s = gen_stack->symrefs; s; s = s->nxt)
	{	if ((s->status & allow)
		&& !(s->status & forbid))
		{	if (m != s->n)
				witness = s->n;
			if (debug) printf("\tanytrack sym present %s (line %d)\n",
				s->sm->nme->str, s->n?s->n->hdr.line:-1);
			return 1;
	}	}

	if (debug) printf("any_track: no matching syms\n");
	return 0;
}

static struct Cmd {
	const char *cmd;
	void (*fn)(treenode *, int, int);
} cmds[] = {
	{ Add_track,	sym_add },
	{ Del_track,	sym_del },
	{ Del_name,	sym_del_name },
	{ Skip_name,	do_nothing },
	{ List_select,	list_select },
	{ Update,	sym_update },
	{ Unmark,	sym_unmark }
	/* adjust size of hit_cmds when adding more */
};

static struct Fct {
	const char *cmd;
	int (*fn)(treenode *, int, int);
} evals[] = {
	{ On_track,	on_track },
	{ Any_track,	any_track },
	{ Match_track,	match_track },
	{ Known_zero,   known_zero },
	{ Known_nonzero, known_nonzero }
	/* adjust size of hit_fcts when adding more */
};

int hit_cmds[8];
int hit_fcts[8];	/* room for 8 fcts */

static void
prop_reached(State *s)
{	Trans *t;

	if (!s || !s->n) return;

	if (!s->visited
	&&  !strstr(s->n->hdr.fnm, " after "))
		printf("uno: %s:%d: not reached\n",
			s->n->hdr.fnm, s->n->hdr.line);

	s->visited = 1;	/* prevent duplicate reports */

	for (t = s->succ; t && t->branch; t = t->nxt)
		prop_reached(t->branch);
}

void
gen_stats(void)
{	int i;
	int cnt;

	for (i = cnt = 0; i < 5; i++)
		if (hit_cmds[i])
			cnt++;
	if (cnt)
	{	printf("uno: commands in property executed\n");
		for (i = 0; i < 5; i++)
			if (hit_cmds[i])
			printf("\t%d\t%s\n", hit_cmds[i], cmds[i].cmd);
	}
	for (i = cnt = 0; i < 5; i++)
		if (hit_cmds[i])
			cnt++;
	if (cnt)
	{	printf("uno: fcts in property executed\n");
		for (i = 0; i < 3; i++)
			if (hit_fcts[i])
			printf("\t%d\t%s\n", hit_fcts[i], evals[i].cmd);
	}

	prop_reached(uno_prop);

	if (ruledout)
	printf("uno: %3d errorpaths generated, but ruled out as infeasible\n",
		ruledout);
}

static void
exec_fct(treenode *n, treenode *m)
{	SymRef *s;
	leafnode *leaf;
	int i, val1, val2;

	if (!n) return;

	if (n->lnode->hdr.type != TN_IDENT)
	{	err_path++;
		printf("exec_fct:\n\t%s:%d: expect ident for fctname, got %s in %s\n",
			n->hdr.fnm,
			n->hdr.line,
			name_of_node(n->lnode->hdr.type),
			x_stmnt(n));
		exit(1);
	}

	leaf = (leafnode *) n->lnode;

	for (i = 0; i < sizeof(cmds)/sizeof(struct Cmd); i++)
		if (strcmp(leaf->data.sval->str, cmds[i].cmd) == 0)
		{
			if (strcmp(leaf->data.sval->str, Skip_name) == 0
			||  strcmp(leaf->data.sval->str, List_select) == 0)
			{	if (debug)
				printf("\tsaw: %s\n", leaf->data.sval->str);

				if (n->rnode
				&&  n->rnode->hdr.type == TN_STRING)
					printf("%s(\"%s\")\n",
						leaf->data.sval->str,
						((leafnode *) n->rnode)->data.str);

				hit_cmds[i]++;
				cmds[i].fn(m, 0, 0);
				return;
			}

			if (strcmp(leaf->data.sval->str, Unmark) == 0)
			{	nogood = val1 = val2 = 0;
				goto doit;	/* 'unmark()' means 'mark(0)' */
			}

			if (strcmp(cmds[i].cmd, Update) == 0)	/* one arg */
			{	nogood = val2 = 0;
				val1 = eval_const_expr(n->rnode, m);
				if (nogood)
				{	fprintf(stderr, "uno: expecting mark(const)\n");
					exit(1);
				}
				goto doit;
			}

			if (!n->rnode
			||   n->rnode->hdr.type != TN_EXPR_LIST)
			{
bad:				fprintf(stderr, "uno: expecting %s(const_expr, const_expr), saw %s(%s)\n",
					cmds[i].cmd, cmds[i].cmd,
					n->rnode?name_of_node(n->rnode->hdr.type):"");
				exit(1);
			}
			nogood = 0;
			val1 = eval_const_expr(n->rnode->lnode, m);
			val2 = eval_const_expr(n->rnode->rnode, m);
			if (nogood) goto bad;

doit:			cmds[i].fn(m, val1, val2);
			hit_cmds[i]++;

	if (debug)
			{	printf("\tgen_stack %s(", cmds[i].cmd);
				if (i < 2) dflow_mark(stdout, val1); else printf("%d", val1);
				printf(", ");
				if (i < 2) dflow_mark(stdout, val2); else printf("%d", val2);
				printf(") <%s>:\n", x_stmnt(m));
				for (s = gen_stack->symrefs; s; s = s->nxt)
				{	printf("\t%s\t(", s->sm->nme->str);
					dflow_mark(stdout, (s->status & ANY));
					printf(")\n");
				}
			}
			return;
		}

	if (strcmp(leaf->data.sval->str, errname) != 0
	||  n->rnode->hdr.type != TN_STRING)
	{	printf("\t\texpect '%s(\"...\")', saw '%s(%s)'\n",
			errname, leaf->data.sval->str,
			name_of_node(n->rnode->hdr.type));
		exit(1);
	}

	leaf = (leafnode *) n->rnode;

	if (debug) printf("<<%s>>\n", leaf->data.str);
	if (err_report(leaf->data.str, m))
	{	fflush(stdout);
		fflush(stderr);
		if (0) exit(1);
	}
	witness = ZT;
}

static int
do_oper(treenode *m, int sign)
{	treenode *n;

	/* either --x (rnode) or x-- (lnode) */
	/* executed as stmnt, net effect the same */

	if (m->rnode) n = m->rnode; else n = m->lnode;

	if (!n
	||   n->hdr.type != TN_IDENT
	||  strcmp(((leafnode *) n)->data.sval->str, statename) != 0)
		return 0;

	gen_stack->uno_state += sign;

	return 1;
}

static void
exec_step(treenode *n, treenode *m)
{	leafnode *leaf;

	switch (n->hdr.type) {
	case TN_FUNC_DECL:
	case TN_DECL:
	case TN_LABEL:
		break;

	case TN_FUNC_CALL:
		exec_fct(n, m);
		break;

	case TN_ASSIGN:
		if (n->lnode->hdr.type == TN_IDENT)
		{	leaf = (leafnode *) n->lnode;
			if (strcmp(leaf->data.sval->str, statename) == 0)
			{	nogood = 0;
				gen_stack->uno_state = eval_const_expr(n->rnode, m);
				if (nogood) goto bad;
			} else if (strcmp(leaf->data.sval->str, s_name) == 0)
			{	if (n->rnode->hdr.type == TN_STRING)
					user_name = ((leafnode *)n->rnode)->data.str;
				else if (n->rnode->hdr.type == TN_IDENT
				&& strcmp(((leafnode *)n->rnode)->data.sval->str, "MATCH") == 0)
					user_name = "_M_A_T_C_H_";
				else goto bad;
			} else if (strcmp(leaf->data.sval->str, s_val) == 0)
			{	nogood = 0;
				user_val = eval_const_expr(n->rnode, m);
				if (nogood) goto bad;
			}
		} else
		{
bad:			err_path++;
			printf("unrecognized assignment <%s>\n",
				x_stmnt(n->rnode));
			exit(1);
		}
		break;

	case TN_EXPR:	/* i++, i-- */
		switch (n->hdr.tok) {
		case INCR:
			if (!do_oper(n, 1)) goto bad;
			break;
		case DECR:
			if (!do_oper(n, -1)) goto bad;
			break;
		default:
			goto nogood;
		}
		break;

	default:
nogood:		err_path++;
		printf("\texec: unknown stmnt type '%s' <%s>\n",
			name_of_node(n->hdr.type),
			x_stmnt(n));
		if (n->lnode) printf("\t\tL = %s\n", name_of_node(n->lnode->hdr.type));
		if (n->rnode) printf("\t\tR = %s\n", name_of_node(n->rnode->hdr.type));
		exit(1);
	}
}

int
get_state_val(void)
{
	if (!gen_stack)
	{	nogood = 1;
		return 0;
	}
	return gen_stack->uno_state;
}

static int
dosel(treenode *m, char *nm, int allow, int forbid, int which)	/* 1:select, 2:unselect */
{	SymRef *s;
	SymList *r;
	treenode *n;
	int nonempty = 0;

	n = (m && m->hdr.type == TN_IF) ? ((if_node *)m)->cond : m;

	if (n && n->hdr.defuse)
	for (r = n->hdr.defuse->other; r; r = r->nxt)
		r->selected = 0;
	if (gen_stack)
	for (s = gen_stack->symrefs; s; s = s->nxt)
		s->status &= ~SELECTED;

	if (n && n->hdr.defuse)
	for (r = n->hdr.defuse->other; r; r = r->nxt)
	{	if (debug)
		printf(">> select saw: %s mark=%d\n",
			r->sm->nme->str, r->mark);