uno_fcts.c

C程序漏洞检查

		if (p)
		{	q = strchr(p+1, '(');	/* has () */
		} else
		{	c = '\'';		/* single quotes? */
			p = strchr(m->label, c);
			if (!p) return 0;	/* give up */
			q = strchr(p+1, '(');
		}

		if (!q)
		{	q = strchr(p+1, c);	/* no (), find closing quote */
			took = c;
		}
	
		r = &(n->label[2]);
		if (r) s = strchr(r+1, ' ');

		f2d_assert((int) (p && q && r && s && q > p+1), "bad fct_call() arg");

		*q = *s = '\0';
		t = (strcmp(p+1, r) == 0);
		*q = took; *s = ' ';	/* restore */
		if (t) return 1;
	}
	return 0;
}

static void
unselect(void)
{	Var *v;

	if (stack)
	for (v = stack->sels; v; v = v->nxt)
		v->sel = 0;

	if (debug) printf("UnSeLecting\n");
}

void
set_select(char *name, char *loc, int stat)
{	Var *v;

	for (v = stack->sels; v; v = v->nxt)
		if (strcmp(v->s, name) == 0)
		{	v->sel  |= 1;
			v->stat |= stat;
			if (debug) printf("	>Select old '%s' - stat %d\n", v->s, v->stat);
			return;
		}
	v = new_var(name);
	v->loc = new_str(loc);
	v->sel = 1;
	if (debug) printf("	>Select new '%s', stat %d\n", v->s, stat);
	v->stat = stat;
	v->nxt = stack->sels;
	stack->sels = v;
}

int
mark_select(int x)
{	Var *v;
	int cnt = 0;

	for (v = stack->sels; v; v = v->nxt)
		if (v->sel)
		{	v->mark = x;
			cnt++;
			if (debug) printf("\tset mark %s to %d\n", v->s, x);
		}
	return cnt;
}

static void
list_sel(void)
{	Var *v;

	for (v = stack->sels; v; v = v->nxt)
		if (v->sel)
		printf("%3d:\t\tvars: %s (%s), mark %d, selection %d\n",
			depth, v->s, v->loc, v->mark, v->sel);
}

static int
has_sel_match(Label *n, int match, int dont)
{	char *r, *s;
	int typ = 0;

	if (strlen(n->label) <= 2
	||  n->label[1] != ' ')
		return 0;

	switch (n->label[0]) {
	case 'G':
		if (!(match & (DECL|DEF)) || (dont & (DECL|DEF))) return 0;
		typ = DECL|DEF;
		break;
	case 'D':
		if (!(match & DEF) || (dont & DEF)) return 0;
		typ = DEF;
		break;
	case 'U':
		if (!(match & USE) || (dont & USE)) return 0;
		typ = USE;
		break;
	case 'R':
		if (!(match & DEREF) || (dont & DEREF)) return 0;
		typ = DEREF;
		break;
	default:
		return 0;
	}

	r = &(n->label[2]);
	s = strchr(r+1, ' ');

	if (!(r && s && s > r)) fprintf(stderr, "bad label: '%s' -- %u %u\n", n->label, r, s);
	f2d_assert((int) (r && s && s > r), "bad sel match");
	*s = '\0';
	set_select(r, s+1, typ); /* r = name, s+1 = location */
	*s = ' ';	/* restore */

	return 1;
}

static int
has_ref_match(int mark, int match, int dont)
{	Var *v;
	int hasmatch = 0;

	if (debug)
	for (v = stack->sels; v; v = v->nxt)
		printf("\tSel: '%s', stat %d, mark %d -- looking for mark %d, +%d -%d\n",
			v->s, v->stat, v->mark, mark, match, dont);

	for (v = stack->sels; v; v = v->nxt)
		if (v->sel == 1
		&&  v->mark == mark
		&& (v->stat & match)
		&& !(v->stat & dont))
		{	hasmatch = 1;
			break;
		}

	if (hasmatch)
	for (v = stack->sels; v; v = v->nxt)
		if (v->sel == 1
		&& (v->mark != mark
		|| !(v->stat & match)
		||  (v->stat & dont)))
			v->sel = 0;

	return hasmatch;
}

static void
notyet(Label *m, char *s)
{
	fflush(stdout);
	fprintf(stderr, "uno:global: unhandled type of label '%s' (%s)\n", m->label, s);
	exit(1);
}

static int
known_nz(void)
{	Var *v;
	BSym *s;

	for (v = stack->sels; v; v = v->nxt)
	{	if (v->sel == 1)
		{	if (debug) printf("	is %s known_nonzero? ", v->s);
			for (s = stack->knz; s; s = s->nxt)
				if (strcmp(v->s, s->s) == 0)
				{	if (debug) printf("yes!\n");
					break;
				}
			if (!s)
			{	if (debug)
				{	printf("no!\n");
					for (s = stack->knz; s; s = s->nxt)
						printf("	knownonzero: %s\n", s->s);
				}
				return 0;
			}
		}
	}
	if (debug) printf("all selected vars known nonzero\n");
	return 1;
}

static int
take_action(Label *m)
{	char *p, *q;
	Label *lb;
	int x, y;
	char c = '\"';

	if (strncmp(m->label, "error(", strlen("error(")) == 0)
	{	p = strchr(m->label, c);
		if (p)
		{	q = strchr(p+1, c);
		} else
		{	c = '\'';
			p = strchr(m->label, c);
			if (!p) return 0;
			q = strchr(p+1, c);
		}
		*q = '\0';
		f2d_assert((int) (p && q && q > p+1), "bad error() arg");

		if (n_reported(stack))
			goto shortcut;

		printf("uno:#%d: %s", ErrCnt++, p+1);
		if (stack->move)
		for (lb = stack->move->to->lab; lb; lb = lb->nxt)
			if (strlen(lb->label) > 0)
				printf(": [%s]", lb->label);
		printf("\n");

		if (print_fnm(rstack, "in fct"))
		print_rstack(rstack->nxt, "called from");

		if (debug) list_sel();

		if (longtrace)
		{	printf("Trace Detail (length %d):\n", depth);
			tabs = 0;
			print_stack(stack, depth);
			printf("\n");
		}
shortcut:		*q = c;
		if (debug) printf("	STOP '%s'\n", m->label);
		if (debug) exit(0);
		return 0;	/* i.e., stop search along this path */
	}

	if (strncmp(m->label, "mark(", strlen("mark(")) == 0)
	{	x = strlen("mark(");
		if (!isdigit(m->label[x])) notyet(m, "arg to mark()");
		x = atoi(&(m->label[x]));
		y = mark_select(x);
		if (debug) printf("	mark '%d' [cnt=%d]\n", x, y);
		return 1;
	}
	if (strncmp(m->label, "unmark()", strlen("unmark()")) == 0)
	{	y = mark_select(0);
		if (debug) printf("	unmark [cnt=%d]\n", y);
		return 1;
	}
	if (strncmp(m->label, "list()", strlen("list()")) == 0)
	{	list_sel();
		if (debug) printf("	list\n");
		return 1;
	}
	if (strncmp(m->label, "no_error()", strlen("no_error()")) == 0)
	{	p = strchr(m->label, c);
		if (p)
		{	q = strchr(p+1, c);
			*q = '\0';
			f2d_assert((int) (p && q && q > p+1), "bad no_error() arg");
			printf("%s", p+1);
			*q = c;
		} else
		{	c = '\'';
			p = strchr(m->label, c);
			if (!p) return 0;
			q = strchr(p+1, c);
			*q = '\0';
			f2d_assert((int) (p && q && q > p+1), "bad no_error() arg");
			printf("%s", p+1);
			*q = c;
		}
		if (debug) printf("	no_error\n");
		return 1;
	}

	/* other types of stmnts, e.g., uno_state++, uno_state--, uno_state = N */
	if (strncmp(m->label, "uno_state--", strlen("uno_state--")) == 0)
		stack->uno_state--;
	else if (strncmp(m->label, "uno_state++", strlen("uno_state++")) == 0)
		stack->uno_state++;
	else if (strncmp(m->label, "uno_state=", strlen("uno_state=")) == 0
	     && isdigit(m->label[strlen("uno_state=")]))
		stack->uno_state = atoi(&(m->label[strlen("uno_state=")]));
	else
		notyet(m, "expecting uno_state = N");

	if (debug) printf("\taction '%s'\n", m->label);
	return 1;
}

static int
act_cond(Label *m, int t)	/* match or non_zero -- conditionals indep of sys labels */
{	int ret = 0;
	int x, y, z;
	int truth = t;

	if (strncmp(m->label, "!match(", strlen("!match(")) == 0)
	{	truth = (truth == 1) ? -1 : 1;
		x = strlen("!match(,");
		goto n_ref;
	}
	if (strncmp(m->label, "!known_nonzero()", strlen("!known_nonzero()")) == 0)
	{	truth = (truth == 1) ? -1 : 1;
		goto n_nz;
	}

	if (strncmp(m->label, "match(", strlen("match(")) == 0)
	{	x = strlen("match(");		/* match(mark, domatch, nomatch) */
n_ref:		if (!isdigit(m->label[x])
		||  sscanf(&(m->label[x]), "%d,%d,%d", &z, &x, &y) != 3)
			notyet(m, "args to match");

		if ((x|y) & ~(DEF|USE|DEREF))	/* only D, U, or R marks matter */
			notyet(m, "2nd or 3rd arg to match");

		ret = has_ref_match(z, x, y);
		if (truth == -1) ret = 1 - ret;

		if (debug) printf("ac: %s -- returns %d\n", m->label, ret);
	} else if (strncmp(m->label, "known_nonzero()", strlen("known_nonzero()")) == 0)
	{
n_nz:		ret = known_nz();
		if (truth == -1) ret = 1 - ret;

		if (debug) printf("ac: %s -- returns %d\n", m->label, ret);
	}

	return ret;
}

static int
act_select(Label *n, Label *m, int t)
{	char *p;
	int ret = 0;
	int x, y;
	int truth = t;

	/*
	 *  n = sys  -- e.g. "C nm file line -- R x file line"
	 *  m = prop -- e.g. "ftc_call('nm') -- select('x', DEREF, NONE)"
	 */

	if (strncmp(m->label, "!fct_call(", strlen("!fct_call(")) == 0)
	{	truth = (truth == 1) ? -1 : 1;
		goto n_fct;
	}
	if (strncmp(m->label, "!select(", strlen("!select(")) == 0)
	{	truth = (truth == 1) ? -1 : 1;
		x = strlen("select('',");
		goto n_sel;
	}
	if (strncmp(m->label, "!(uno_state", strlen("!(uno_state")) == 0)
	{	truth = (truth == 1) ? -1 : 1;
		p = &(m->label[strlen("!(uno_state")]);
		goto n_uno;
	}

	if (strncmp(m->label, "fct_call(", strlen("fct_call(")) == 0)
	{
n_fct:		if (has_fct_match(n, m))
		{	if (debug)
			printf("\tfct match '%s' <-> '%s' (want %d)\n",
				n->label, m->label, truth);

			if (truth ==  1) return 1;
			if (truth == -1) return 0;
			return 1;	/* fct_call as stmnt, matching */
		} else
		{	if (truth ==  1) return 0;
			if (truth == -1) return 1;
			return 0;	/* fct_call as stmnt, not matching */
	}	}

	if (strncmp(m->label, "select(", strlen("select(")) == 0)
	{	/* 4 args:  name, domatch, nomatch, mark */
		/* name must be '' for now */
		x = strlen("select('',");
n_sel:
		if (!strstr(m->label, "('',")
		||  !isdigit(m->label[x])
		||  sscanf(&(m->label[x]), "%d,%d", &x, &y) != 2)
			notyet(m, "args to select");
		if ((x|y) & ~(DEF|USE|DEREF))	/* only D, U, or R marks matter */
			notyet(m, "2nd or 3rd arg to select");

		ret = has_sel_match(n, x, y);
		if (truth == -1) ret = 1 - ret;

		if (debug) printf("lm: %s <-> %s -- returns %d\n", n->label, m->label, ret);
		return ret;
	}

	if (strncmp(m->label, "(uno_state", strlen("(uno_state")) == 0)
	{	p = &(m->label[strlen("(uno_state")]);
n_uno:		switch (*p) {
		case '!':
			if (*(p+1) != '=' || !isdigit(*(p+2))) notyet(m, "operator");
			ret = (stack->uno_state != atoi(p+2));
			break;
		case '=':
			if (*(p+1) != '=' || !isdigit(*(p+2))) notyet(m, "operator");
			ret = (stack->uno_state == atoi(p+2));
			break;
		case '>':
			if (*(p+1) == '=')
			{	if (!isdigit(*(p+2))) notyet(m, "operator");
				ret = (stack->uno_state >= atoi(p+2));
			} else
			{	if (!isdigit(*(p+1))) notyet(m, "operator");
				ret = (stack->uno_state > atoi(p+1));
			}
			break;
		case '<':
			if (*(p+1) == '=')
			{	if (!isdigit(*(p+2))) notyet(m, "operator");
				ret = (stack->uno_state <= atoi(p+2));
			} else
			{	if (!isdigit(*(p+1))) notyet(m, "operator");
				ret = (stack->uno_state < atoi(p+1));
			}
			break;
		default:
			notyet(m, "operator");
		}
		if (truth == -1) ret = 1 - ret;

		if (debug)
		printf("\tcmd '%s' == %d\n", m->label, ret);
		return ret;
	}
	notyet(m, "unrecnogized command");
	return ret;
}

static void
addtostack(char *s)	/* info on var known to be nonzero */
{	char *p;
	BSym *r;

	p = strchr(s, ' ');
	if (!p)
	{	fprintf(stderr, "bad label: %s\n", s);
		return;
	}
	*p = '\0'; /* p now points to location */
	r = new_sym(s);
	r->nxt = stack->knz;
	stack->knz = r;
	*p = ' ';	/* restore */
	if (debug) printf("KnownNonZero var: '%s'\n", s);
}

static int
eval_prop(Node *sys, Node *prop)
{	Arc	*b;
	Label	*n, *m;
	int	nzs = 0, truth, x;

	if (!prop) return 1;			/* reached end of prop */

	for (n = sys->lab; n; n = n->nxt)	/* is this a knz inserted state? */
		if (strncmp(n->label, "N ", strlen("N ")) == 0)
		{	addtostack(&n->label[2]);
			nzs = 1;
		}
	if (nzs) return 1;

#if 0
	the only possible labels, so far, are:
	condnts:	select, fct_call	<- true/false arcs, dependent on sys
	condnts:	match, known_nonzero	<- true/false arcs, independent of sys
	actions:	error, no_error, mark	<- single label and independent of sys
#endif

	for (b = prop->succ; b; b = b->nxt)	/* all edges to succ states of prop */
	for (m = b->lab; m; m = m->nxt)		/* all tags on those states */
	{
		if (debug) printf("	>proplabel '%s'\n", m->label);

		if (strstr(m->label, "||")
		||  strstr(m->label, "&&"))
			notyet(m, "composite expr");

		if (strstr(m->label, "== _true") != NULL)
			truth = 1;	/* true branch */
		else if (strstr(m->label, "== _false") != NULL)
			truth = -1;	/* false branch */
		else if (strstr(m->label, " == ") != NULL)
			notyet(m, "case switch");
		else
		{	/* action: error, no_error, mark */
			if (!take_action(m))	/* independent of sys labels */
				return 0;	/* error - do not proceed */
			x = 1;			/* no_error, mark */
			goto down;
		}
		if (strstr(m->label, "match(")
		||  strstr(m->label, "known_nonzero("))
			x = act_cond(m, truth);	/* eval independent of sys labs */
		else
		{	x = 0;
			if (strstr(m->label, "select("))
				unselect();			/* new selection erases old */
			for (n = sys->lab; n; n = n->nxt)	/* tags on current system state */
				x += act_select(n, m, truth);	/* collect info from all matches */
			/* unless 'notyet' is declared as an exit fct, uno
			   will not be able to tell that 'truth' was initialized
			 */
		}
down:		if (x)
		{	if (debug) printf("	>down in prop\n");
			eval_prop(sys, b->to);
			if (debug) printf("	>up in prop\n");
		}
	}

	if (debug) printf("uno:global: end of property\n");
	return 1;	/* reached the end */
}

static void
check_prop(Arc	*in)
{	Stack	*os;
	BFct	*f;
	Label	*n;
	Arc	*a;
	Node	*sys;
	int	hit;

	if (!in || !in->to)
	{	end_of_path();	/* find continuations in callstack */
		return;
	}

	sys = in->to;

	if (same_state(in))
	{	if (debug)
		printf("\tREVISIT nid %d state_bits %d - callpt %d\n",
			sys->nid,
			sys->vis->uno_state,	/* bit mask */
			(rstack && rstack->n)?rstack->n->nid:-1);
		return;
	}

	depth++;

	if (debug)
	printf("%3d: [%d, %d] callpt %d -- %s\n", depth, sys->nid,
		stack->uno_state,
		(rstack && rstack->n)?rstack->n->nid:-1,
		(sys && sys->lab)?sys->lab->label:"--");

	if (debug) printf("%3d: evalprop starts (%u)\n", depth, prop_start);

	if (!eval_prop(sys, prop_start))		/* complains on errors */
		goto done;

	if (debug) printf("%3d: evalprop ended\n", depth);

	hit = 0;
	for (n = sys->lab; n; n = n->nxt)		/* check tags on current state */
	{	f = fct_in_lab(n->label);		/* to find all fct calls */
		if (f && !f->visited)			/* effect not already in call chain */
		{	if (debug) printf("%3d:\tCALL to %s [%d]\n", depth, f->fnm, sys->nid);
			do_fct_call(f, sys);
			if (debug) printf("%3d:\tUN_CALL %s [%d]\n", depth, f->fnm, sys->nid);
			hit++;	/* continuation is explored on return from fct */
	}	}
	if (hit) goto done;

	if (!sys->succ) end_of_path();

	for (a = sys->succ; a; a = a->nxt)		/* explore all next states */
	{	if (debug) { printf("%3d:\tDOWN\n", depth); list_sel(); }
		check_prop(a);	/* are explored */
		if (debug) { printf("%3d:\tUP\n", depth); list_sel(); }
	}
done:
	depth--;
	os = stack;
	stack->sels = rev_release(stack->sels);
	stack->knz  = rev_symrel(stack->knz);
	stack = stack->nxt;
	os->nxt = free_stack;
	free_stack = os;
}

void
run_check(void)
{	BFct *f;

	if (!fcts) return;

	stack = &init;
	ini_prop();
	add_glob_defs();

	f = find_function("_global_");	/* start execution with global defs */
	if (f)
	{	if (debug) printf("	CHECK %s\n", f->fnm);
		do_fct_call(f, (Node *) 0);
	} else
		printf("uno:global: internal error, no _global_\n");
	if (verbose)
	printf("uno:global: %d scenarios reported in property check\n", ErrCnt-1);
}

void
handle_fct(char *p_in)
{	static BFct *f;
	static Arc *a;
	int id;
	char *t;
	char p[512];

	if (strlen(p_in) >= 512)
	{	fprintf(stderr, "uno:global: very long fct name <%s>\n", p_in);
		exit(1);
	}
	strcpy(p, p_in);	/* p_in could be a constant string */

	t = strchr(p, '\r');
	if (t) *t = '\0';
	t = strchr(p, '\n');
	if (t) *t = '\0';

	if (0) { printf("'%s' (%d)\n", p, strlen(p)); fflush(stdout); }

	if (p)
	switch (*p) {
	case ':':	/* reminder of fct name - already created */
		t = strchr(p+2, '\t');
		if (!t) goto bad1;
		*t = '\0';
		f = find_function(p+2);
		if (!f)
		{
bad1:			fprintf(stderr, "uno:global: fct reminder invalid '%s'\n", p);
			exit(1);
		}
		*t = '\t';
		oid = 0;
		break;

	case '{':
		if (sscanf(p, "{%d}", &id) != 1)
bad:			fprintf(stderr, "uno:global: bad fct delimiter: '%s'\n", p);
		else
			a = add_arc(f, oid, id);	/* uno can't tell that f was initialized */
		break;

	case '<':
		if (sscanf(p, "<%d>", &id) != 1)
			goto bad;
		else
			oid = id;
		break;

	case '>':
		if (sscanf(p, ">%d>", &id) != 1)
			goto bad;
		else
		{	a = add_arc(f, oid, id);
			oid = id;
		}
		break;

	case '[':
		t = strrchr(p, ']');
		if (!t) goto bad;
		*t = '\0';
		if (t > p+1)
		{	if (!a)
			{	fprintf(stderr, "uno:global: zero arc error\n");
				exit(1);
			}
			add_label(f, a, p+1);
		}
		*t = ']';
		break;
	}
}