uno_generic.c

C程序漏洞检查！

		if (strlen(nm) > 0
		&&  strcmp(nm, r->sm->nme->str) != 0)
			continue;

		switch (which) {
		case 1:	/* select */
			if ((r->mark & allow)
			&& !(r->mark & forbid))
			{	r->selected = 1;
				nonempty = 1;
			}
			break;

		case 2:	/* unselect */
			if (r->selected)
			{	if ((r->mark & allow)
				&& !(r->mark & forbid))
					r->selected = 0;
				else
					nonempty = 1;
			}
			break;
	}	}

	return nonempty;
}

static int
sel_args(treenode *e, treenode *n, int which)	/* 1:select(name,with,without), 2:unselect() */
{	treenode *f, *g;
	int val1, val2;

	/*	   TN_FUNC_CALL:e
		      /    \
		     /      \
		TN_IDENT  TN_EXPR_LIST:f
		   /          /         \
		select       /       TN_INT:val2
	                    /
	           TN_EXPR_LIST:g
	                  /      \
		 TN_STRING       TN_INT:val1
	      or TN_IDENT:MATCH:arg1
	 */
		if (!e->rnode
		||   e->rnode->hdr.type != TN_EXPR_LIST)
			goto bad1;
	f = e->rnode;
		if (!f->lnode
		||   f->lnode->hdr.type != TN_EXPR_LIST)
			goto bad1;
	g = f->lnode;
		if (!g->lnode || !g->rnode)
			goto bad1;
	nogood = 0;
	val1 = eval_const_expr(g->rnode, n);
	val2 = eval_const_expr(f->rnode, n);
	if (nogood || g->lnode->hdr.type != TN_STRING)
	{
bad1:		err_path++;
		fprintf(stderr, "\t\t%s:%d: error in '%s'\n",
			n?n->hdr.fnm:"--", n?n->hdr.line:0, x_stmnt(e));
		exit(1);
	}

	user_name = ((leafnode *)g->lnode)->data.str;

	if (debug)
	printf(">>saw %s(%s,%d,%d)\n", x_stmnt(e), user_name, val1, val2);

	return dosel(n, user_name, val1, val2, which);
}

static int
doref(treenode *m, int allow, int forbid)	/* refine -- unselect nonmatches */
{	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)
	{	if (debug)
		printf(">> refine/unselect saw: %s mark=%d\n",
			r->sm->nme->str, r->mark);

		if (r->selected)
		{	if (!(r->mark & allow)
			||   (r->mark & forbid))
				r->selected = 0;
			else
				nonempty = 1;
	}	}

	return nonempty;
}

static int
ref_args(treenode *e, treenode *n)	/* 1: refine(with,without), 2: unselect(with,without) */
{	treenode *f;
	int val1, val2;

	/*	   TN_FUNC_CALL:e
		      /    \
		     /      \
		TN_IDENT  TN_EXPR_LIST:f
		   /          /         \
		refine       /       TN_INT:val2
		     TN_INT:val1
	 */
		if (!e->rnode
		||   e->rnode->hdr.type != TN_EXPR_LIST)
			goto bad1;
	f = e->rnode;
		if (!f->lnode || !f->rnode)
			goto bad1;
	nogood = 0;
	val1 = eval_const_expr(f->lnode, n);
	val2 = eval_const_expr(f->rnode, n);
	if (nogood)
	{
bad1:		err_path++;
		fprintf(stderr, "\t\t%s:%d: error in '%s'\n",
			n?n->hdr.fnm:"--", n?n->hdr.line:0, x_stmnt(e));
		exit(1);
	}

	if (debug)
	printf(">>saw %s(%s,%d,%d,%d)\n", x_stmnt(e), user_name, user_val, val1, val2);

	return doref(n, val1, val2);
}

static int
domatch(treenode *n, int mark, int allow, int forbid, int which)	/* 1: match, 2: marked */
{	SymRef *s;
	SymList *r;
	int nonempty = 0;

	/* select names in dfstack that match selection in defuse */

	if (!n || !n->hdr.defuse)
		return 0;

	if (debug)
	printf("domatch mark=%d, allow=%d, forbid=%d, which=%d\n",
		mark, allow, forbid, which);

	for (s = gen_stack->symrefs; s; s = s->nxt)
	{	if (debug)
		printf(">> stack: %s s_val=%d status=%d\n",
			s->sm->nme->str, s->s_val, s->status);

		if (s->s_val == mark
		&&  (s->status & allow)
		&& !(s->status & forbid))
		{	if (which == 2)	/* marked */
			{	if (s->s_val == mark
				&&  (s->status & allow)
				&& !(s->status & forbid))
				{	s->status |= SELECTED;
					if (debug) printf("	YES marked\n");
					nonempty = 1;
				}
			} else		/* match */
			{	for (r = n->hdr.defuse->other; r; r = r->nxt)
					if (r->selected
					&&  strcmp(r->sm->nme->str, s->sm->nme->str) == 0)
					{	s->status |= SELECTED;
						nonempty = 1;
						if (debug) printf("	YES matched\n");
						break;
		}	}		}
	}
	return nonempty;
}

static int
match_args(treenode *e, treenode *n, int which)	/* 1:match(mark,with,without) 2:marked(x,with,without) */
{	treenode *f, *g;
	int val1, val2, mark;

	/*	   TN_FUNC_CALL:e
		      /    \
		     /      \
		TN_IDENT  TN_EXPR_LIST:f
		   /          /         \
		match        /       TN_INT:val2
	           TN_EXPR_LIST:g
	                  /      \
		  TN_INT:mark    TN_INT:val1
	 */
		if (!e->rnode
		||   e->rnode->hdr.type != TN_EXPR_LIST)
			goto bad1;
	f = e->rnode;
		if (!f->lnode
		||   f->lnode->hdr.type != TN_EXPR_LIST)
			goto bad1;
	g = f->lnode;
		if (!g->lnode || !g->rnode)
			goto bad1;
	nogood = 0;
	val1 = eval_const_expr(g->rnode, n);
	val2 = eval_const_expr(f->rnode, n);
	mark = eval_const_expr(g->lnode, n);
	if (nogood)
	{
bad1:		err_path++;
		fprintf(stderr, "\t\t%s:%d: error in '%s'\n",
			n?n->hdr.fnm:"--", n?n->hdr.line:0, x_stmnt(e));
		exit(1);
	}

	if (debug)
	{	err_path++;
		printf("%3d>>saw %s(%s,%d,%d)\n", depth, x_stmnt(e), user_name, val1, val2);
		err_path--;
	}
	return domatch(n, mark, val1, val2, which);
}

int
eval_fct(treenode *e, treenode *n)
{	leafnode *leaf;
	int i, val1, val2;

	if (!e) return 0;

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

	leaf = (leafnode *) e->lnode;
	if (strcmp(leaf->data.sval->str, endname) == 0)
		return path_ends;

	if (strcmp(leaf->data.sval->str, callname) == 0)
	{	if (e->rnode
		&&  e->rnode->hdr.type == TN_STRING)
		{	leaf = (leafnode *) e->rnode;

			if (debug) printf("saw %s(%s)\n", callname, leaf->data.str);

			return has_ident(n, leaf->data.str);
		}
		goto bad1;
	}

	if (strcmp(leaf->data.sval->str, selname) == 0)
		return sel_args(e, n, 1);

	if (strcmp(leaf->data.sval->str, refname) == 0)
		return ref_args(e, n);

	if (strcmp(leaf->data.sval->str, excname) == 0)
		return sel_args(e, n, 2);

	if (strcmp(leaf->data.sval->str, matchname) == 0)
		return match_args(e, n, 1);

	if (strcmp(leaf->data.sval->str, markedname) == 0)
		return match_args(e, n, 2);

	for (i = 0; i < sizeof(evals)/sizeof(struct Cmd); i++)
		if (strcmp(leaf->data.sval->str, evals[i].cmd) == 0)
		{
			val1 = val2 = 0;	/* set defaults */
			nogood = 0;

			if (strncmp(evals[i].cmd, "known_", strlen("known_")) == 0)
				goto doit;	/* no args */

			/* everything else has two args */

			if (!e->rnode
			||   e->rnode->hdr.type != TN_EXPR_LIST)
			{
bad2:				fprintf(stderr, "uno: bad fct args %s(%s)\n",
					evals[i].cmd, x_stmnt(e->rnode));
				exit(1);
			}

			val1 = eval_const_expr(e->rnode->lnode, n);
			val2 = eval_const_expr(e->rnode->rnode, n);
doit:			if (nogood) goto bad2;

			hit_fcts[i]++;
			if (debug) printf("saw %s(%d,%d)\n", evals[i].cmd, val1, val2);
			return evals[i].fn(n, val1, val2);
		}
	goto bad1;
}

static int
eval_step(treenode *e, treenode *v, treenode *n)
{	leafnode *leaf;
	int val, arg1_val = -1;

	uno_assert(e && v, "bad call to eval_step");

	if (debug)
	{	printf("\teval %s <%s> ",
			name_of_node(e->hdr.type),
			x_stmnt(e));
		printf(":: %s <%s>\n",
			name_of_node(v->hdr.type),
			x_stmnt(v));
	}
	switch (e->hdr.type) {
	case TN_IDENT:
		leaf = (leafnode *) e;
		if (strcmp(leaf->data.sval->str, statename) != 0)
		{	printf("\t\texpected '%s', saw %s\n",
				statename, leaf->data.sval->str);
			exit(1);
		}
		arg1_val = gen_stack->uno_state;
		if (debug) printf("\t\targ1 %s (==%d)\n",
				leaf->data.sval->str, arg1_val);
		break;

	case TN_FUNC_CALL:
		arg1_val = eval_fct(e, n);
		break;

	case TN_EXPR:
		nogood = 0;
		arg1_val = eval_const_expr(e, n);
		if (nogood)
		{	printf("\t\tbad expression (%s == ?), saw %s <%s>\n",
				statename, name_of_node(e->hdr.type), x_stmnt(e));
			exit(1);
		} else
		{	if (debug) printf("\t\targ1 = %d\n", arg1_val);
		}
		break;
	default:
		printf("\t\targ1 expecting func_call or ident, saw %s <%s>\n",
			name_of_node(e->hdr.type), x_stmnt(e));
		exit(1);
	}

	switch (v->hdr.type) {
	case TN_IDENT:
		leaf = (leafnode *) v;

		if (debug) printf("\t\targ2 = %s\n", leaf->data.sval->str);

		if (strcmp(leaf->data.sval->str, "_true_") == 0)
		{	if (arg1_val) goto yes; else goto no;
		} else if (strcmp(leaf->data.sval->str, "_false_") == 0)
		{	if (arg1_val) goto no; else goto yes;
		} else if (strcmp(leaf->data.sval->str, statename) == 0)
		{	if (arg1_val == gen_stack->uno_state) goto yes;
			goto no;
		}
		printf("\t\texpected true, false, or %s, saw %s\n",
			statename, leaf->data.sval->str);			
		break;

	case TN_EXPR:
		nogood = 0;
		val = eval_const_expr(v, n);
		if (!nogood)
		{	if (debug) printf("\t\targ2 = %d\n", val);
			if (arg1_val == val) goto yes;
			goto no;
		}
		printf("\t\tbad expression arg2 = ?, saw <%s>\n", x_stmnt(v));
		break;
	default:
		printf("\t\targ2 expecting expr or ident, saw %s\n",
			name_of_node(v->hdr.type));
		break;
	}

	if (debug) printf("Don't Know\n");
	exit(1);
yes:
	if (debug) printf("Yes\n");
	return 1;
no:
	if (debug) printf("No\n");
	return 0;
}

static State *
exec_lastfirst(State *s, Trans *t, treenode *e, treenode *n)
{	State *x;

	if (!t || !t->branch)
	{	if (debug>1) printf("\t(%d) lastfirst. no branch\n", s->n->hdr.line);
		return ZS;
	}

	if (x = exec_lastfirst(s, t->nxt, e, n))	/* assign x */
	{	if (debug>1) printf("\t(%d) lastfirst. gottcha\n", s->n->hdr.line);
		return x;
	}

	if (e && !eval_step(e, t->cond, n))
	{	if (debug>1) printf("\t(%d) lastfirst. fail eval\n", s->n->hdr.line);
		return ZS;
	}

	if (debug>1) printf("\t(%d) lastfirst. pass eval\n", s->n->hdr.line);

	return t->branch;
}

static void
exec_prop(State *s, treenode *n)
{	treenode *exp = ZT;
	State *ns = ZS;

	if (!s) return;

	if (debug) printf("exec_prop %s:%d: %s <%s>\n",
			s->n->hdr.fnm,
			s->n->hdr.line,
			name_of_node(s->n->hdr.type),
			x_stmnt(s->n));

	s->visited = 1;	/* to determine effective coverage of property */

	if (s->iscond && s->n)
	{	exp = (s->n->hdr.type == TN_IF) ? ((if_node *)s->n)->cond : s->n;
		ns = exec_lastfirst(s, s->succ, exp, n);	/* eval_step(exp) */
	} else
	{	exec_step(s->n, n);
		if (s->succ) ns = s->succ->branch;
	}

	exec_prop(ns, n);
}

void
dfs_generic(State *s)
{	GenStack *g;
	Trans *t;
	SymRef *r;
	treenode *exp = ZT;
	int any_added = 0;

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

	depth++;

	if (debug)
	{	printf("%3d: dfs %s:%d: <%s>\t",
			depth,
			s->n->hdr.fnm,
			s->n->hdr.line,
			x_stmnt(s->n));
		if (s->n->hdr.type == TN_IF)
			dump_defuse(((if_node *)s->n)->cond->hdr.defuse, stdout);
		else
			dump_defuse(s->n->hdr.defuse, stdout);
		printf("\n");
		if (gen_stack)
		for (r = gen_stack->symrefs; r; r = r->nxt)
			printf("\tGenStack %s %d\n", r->sm->nme->str, r->status);

	}

	if (s->iscond && s->n)
	exp = (s->n->hdr.type == TN_IF) ? ((if_node *)s->n)->cond : s->n;

	any_added = gen_push(s);	/* checks symrefs to state snapshot -- updates snapshot*/
	g = gen_stack;
	g->e = exp?exp:s->n;

	path_ends = !(s->succ && s->succ->branch);

	user_val = 0;
	user_name = "";
	exec_prop(uno_prop, g->e);	/* can modify uno_state/symrefs */

	if (g->uno_state >= sizeof(unsigned long)*8)
	{	fprintf(stderr, "uno: too many states in property (max %d)\n",
			sizeof(unsigned long)*8 - 1);
		exit(1);
	}

	if (debug)
		printf("\t%s = %d (stack) %d (state-bits)\n",
			statename,
			g->uno_state,
			s->uno_state);

	if (any_added == 0 && (s->uno_state & (1 << g->uno_state)))
	{	if (s->visited)
		{	if (debug) printf("\told\n");
			goto pop;
		} else
		{	if (debug) printf("\tnew\n");
		}
	} else
	{	if (debug)
			printf("\t%s\n", s->visited?"revisit":"new");
	}
	s->uno_state |= (1<<g->uno_state);	/* updates uno_state snapshot */
	s->visited = 1;

	for (t = s->succ; t && t->branch; t = t->nxt)
		if (!infeasible(exp, t->cond))	/* e.g. 0 == _true_ */
		{	g->c = t->cond;
			dfs_generic(t->branch);
		}

pop:	gen_pop(g);

	if (debug)
	{	printf("%3d: dfs up\n", depth);
		if (gen_stack)
		for (r = gen_stack->symrefs; r; r = r->nxt)
			printf("\tGenStack %s %d\n", r->sm->nme->str, r->status);
	}
	
	depth--;
}

void
gen_reset(void)
{
	gen_stack = (GenStack *) 0;
	witness = (treenode *) 0;
	ruledout = 0;
}