uno_generic.c

C程序漏洞检查！

/***** uno: uno_generic.c *****/

/* Copyright (c) 2000-2003 by Lucent Technologies - Bell Laboratories     */
/* All Rights Reserved.  This software is for educational purposes only.  */
/* Permission is given to distribute this code provided that this intro-  */
/* ductory message is not removed and no monies are exchanged.            */
/* No guarantee is expressed or implied by the distribution of this code. */
/* Software written by Gerard J. Holzmann based on the public domain      */
/* ANSI-C parser Ctree Version 0.14 from Shaun Flisakowski                */

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "gram.h"
#include "symtab.h"
#include "uno_lts.h"

static int	debug = 0;

typedef struct GenStack GenStack;

struct GenStack {
	SymRef	*symrefs;
	int	uno_state;
	treenode *e, *c;
	GenStack *nxt;
};

static GenStack	*gen_stack = (GenStack *) 0;
static GenStack	*gen_free = (GenStack *) 0;
static treenode *witness = (treenode *) 0;
static int	ruledout = 0;

extern State	*uno_prop;
extern Graphs	*curgraph;

static int	steps = 0;
static int	path_ends = 0;
static int	ErrCnt = 0;
extern int	depth, Verbose;
extern int	nogood, picky, allerrs;
int		err_path;

/* Names used in user-code inside C procedure specifying the property */
const char *property  = "uno_check";	/* name of prop, specified as C procedure in src */
const char *errname   = "error";	/* name of error procedure */
const char *callname  = "fct_call";	/* name of procedure used to check for fcts called */
const char *endname   = "path_ends";	/* name of procedure used to check for end-state */
const char *selname   = "select";
const char *refname   = "refine";
const char *matchname = "match";
const char *markedname = "marked";
const char *excname   = "unselect";

/* variables that can be set within the property */
const char *statename = "uno_state";	/* to refer to the state of the prop automaton */
const char *s_name    = "s_name";	/* to refer to target symbol name */
const char *s_val     = "s_mark";	/* to refer to target symbol state_value */

char	*user_name;	/* remembers a user-defined symbol name - for use in select() */
int	user_val;	/* remembers a user-defined state value - for use in select() */

/* dealing with symbols: */
#define Add_track	"add_track"
#define List_select	"list"
#define Skip_name	"no_error"
#define Del_track	"del_track"
#define Del_name	"del_name"
#define On_track	"on_track"
#define Any_track	"any_track"
#define Match_track	"match_track"
#define Known_zero	"known_zero"
#define Known_nonzero	"known_nonzero"
#define Update		"mark"
#define Unmark		"unmark"

extern void	uno_assert(int, char *);
extern int	v_reported(treenode *);
extern SymRef	*rev_release(SymRef *);
extern SymRef	*uno_getref(symentry_t *);
extern int	eval_const_expr(treenode *, treenode *);
extern void	dflow_mark(FILE *, int);
extern int	v_matched(treenode *);
extern void	dump_defuse(DefUse *, FILE *);
extern int	snap_add(State *, SymRef *);
extern int	infeasible(treenode *, treenode *);

static int
has_ident(treenode *n, char *s)
{
	if (!n) return 0;

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

	if (n->hdr.which != LEAF_T)
		switch (n->hdr.type) {
		case TN_SWITCH:
		case TN_WHILE:
		case TN_DOWHILE:
			return has_ident(n->lnode, s);
		default:
			return has_ident(n->lnode, s) || has_ident(n->rnode, s);
		}
	return 0;
}

static int
err_matched(GenStack *g)
{
	if (!g) return 0;

	return err_matched(g->nxt)
	|| (witness
	&&  witness == g->e
	&&  v_matched(g->e));
}

static void
err_reversed(GenStack *g)
{
	if (!g) return;

	err_reversed(g->nxt);
#if 0
	if (!debug && witness)
	{	if (g->e != witness)
			return;
		if (v_reported(g->e))
		{	fprintf(stderr, "\t--:\t%s:%d: <%s> matches an earlier case\n",
				g->e->hdr.fnm,
				g->e->hdr.line,
				x_stmnt(g->e));
			return;
		}
	}
	witness = ZT;
#endif

	if (g->e
	&&  g->e->hdr.type != TN_SWITCH
	&&  g->e->hdr.type != TN_WHILE
	&&  g->e->hdr.type != TN_DOWHILE)
	{
		if (g->e == witness) printf("*");
		if (g->c) printf("C");

		printf("\t%d:\t%s:%d: <%s>",
			steps++,
			g->e->hdr.fnm,
			g->e->hdr.line,
			x_stmnt(g->e));
		if (g->c)
			printf(" == <%s>", x_stmnt(g->c));

		if (debug) dump_defuse(g->e->hdr.defuse, stdout);
		printf(";\n");
	}
}

static int
same_expr(treenode *a, treenode *b)
{	leafnode *n, *m;

	if (!a && b) return 0;
	if (a && !b) return 0;
	if (a == b)  return 1;

	if (a->hdr.tok != b->hdr.tok
	||  a->hdr.which != b->hdr.which
	||  a->hdr.type != b->hdr.type)
		return 0;

	if (a->hdr.which == LEAF_T)
	{	n = (leafnode *) a;
		m = (leafnode *) b;

		switch (a->hdr.type) {
		case TN_INT:
			return n->data.ival == m->data.ival;
		case TN_REAL:
			return n->data.dval == m->data.dval;
		case TN_STRING:
			return n->data.sval->str == m->data.sval->str;
		case TN_IDENT:
			return (strcmp(n->data.sval->str, m->data.sval->str) == 0);
		case TN_TYPE:
			if (a->hdr.tok == TYPEDEF_NAME)
				return n->data.sval->str == m->data.sval->str;
			return (a->hdr.tok != b->hdr.tok);
		default:
			fprintf(stderr, "uno: %s:%d: %s:%d: cannot happen, same_expr: %s\n",
				a->hdr.fnm, a->hdr.line,
				b->hdr.fnm, b->hdr.line,
				name_of_node(a->hdr.type));
			exit(1);
		}
	}

	return same_expr(a->lnode, b->lnode)
	&&     same_expr(a->rnode, b->rnode);
}

static treenode *
path_not_feasible(void)
{	GenStack *f, *g;
	char *s, *t;
	SymList *x, *y;

	for (g = gen_stack; g; g = g->nxt)
	{	if (!g->c
		||   g->c->hdr.tok != IDENT)	/* not a conditional */
			continue;

		s = ((leafnode *)g->c)->data.sval->str;

		if (strcmp(s, "_false_") != 0
		&&  strcmp(s, "_true_")  != 0)
			continue;		/* not simple */

		for (f = g->nxt; f; f = f->nxt)
		{
#if 1
			/* if a symbol with USE in g->e appears with DEF in f->e
			   then the condition could well change in value
			 */

			if (f->e->hdr.defuse && g->e->hdr.defuse)
			for (x = f->e->hdr.defuse->other; x; x = x->nxt)
			{	if ((x->mark & DEF) && !(x->mark & (REF0|REF1)))
				for (y = g->e->hdr.defuse->other; y; y = y->nxt)
					if (strcmp(x->sm->nme->str, y->sm->nme->str) == 0
					&&  (y->mark & USE))
					{	if (debug)
						{	fprintf(stderr, "consistency check on %s\t",
								x_stmnt(g->e));
							fprintf(stderr, "voided by asgn in %s\n",
								x_stmnt(f->e));
						}
						goto done;
			}		}
#endif
			if (!same_expr(f->e, g->e)
			|| !f->c
			||  f->c->hdr.tok != IDENT)
				continue;

			t = ((leafnode *)f->c)->data.sval->str;
			if (strcmp(t, "_false_") != 0
			&&  strcmp(t, "_true_")  != 0)
				continue;	/* not simple */

			if (strcmp(s, t) != 0)	/* found contradiction */
			{	ruledout++;
				if (Verbose)
				{	printf("(Infeasible path)\n");
					return (treenode *) 0;
				}
				return g->e;
		}	}
done:		;
	}
	return (treenode *) 0;
}

static int
err_report(char *m, treenode *e)
{	GenStack *g;
	treenode *x;

	x = path_not_feasible();

	if ((!debug && x)
	||  err_matched(gen_stack))
	{	if (debug)
		fprintf(stderr, "err_report suppressed 1 x=%d\n", x);
		return 0;
	}

	if ((!allerrs && v_reported(e))
	|| (witness == e && picky))
	{	if (debug)
		fprintf(stderr, "err_report suppressed 2\n");
		return 0;
	}

	if (picky)
	{	int cnt = 0;
		for (g = gen_stack; g; g = g->nxt)
			if (g->c)
				cnt++;
		if (cnt >= picky)
		{	if (debug)
			fprintf(stderr, "err_report suppressed 3 (cnt %d, picky %d)\n",
				cnt, picky);
			return 0;	/* no paths with >= picky conditionals */
	}	}

	ErrCnt++;

	printf("uno: %d: %s() '%s'%s",
		ErrCnt, curgraph->fctnm, m,
		(witness && witness == e)? " (in cyclic path)":"");
	if (x)
	printf(" (fails consistency check on %s)", x_stmnt(x));
	printf("\n");

	steps = 1;
	err_path = 1;
	err_reversed(gen_stack);
	err_path = 0;
	printf("\n");

	if (0) abort();

	return 1;
}

static int
gen_push(State *s)
{	GenStack *g;
	SymRef *r, *t;
	int any_added = 0;

	if (gen_free)
	{	g = gen_free;
		gen_free = gen_free->nxt;
	} else
		g = (GenStack *) emalloc(sizeof(GenStack));

	if (gen_stack)
	{	g->uno_state = gen_stack->uno_state;	/* copy state-bits */

		for (r = gen_stack->symrefs; r; r = r->nxt)
		{	if (snap_add(s, r))		/* not tracked from s before */
				any_added = 1;

			t = uno_getref(r->sm);
			t->status = r->status;
			t->s_val = r->s_val;
			t->n = r->n;
			t->nxt = g->symrefs;
			g->symrefs = t;
	}	}

	g->nxt = gen_stack;
	gen_stack = g;

	return any_added;
}

static void
gen_pop(GenStack *g)
{
	g->symrefs = rev_release(g->symrefs);
	g->uno_state = 0;

	uno_assert((int) gen_stack, "gen_stack error");

	gen_stack = gen_stack->nxt;	/* pop stack */
	g->nxt = gen_free;
	gen_free = g;
}

static int
basiczero(treenode *n)	/* 1 = zero, -1 = nonzero, 0 = don't know */
{
	if (n->hdr.type == TN_IDENT
	||  n->hdr.type == TN_ASSIGN
	||  n->hdr.type == TN_FUNC_CALL)
		return -1;		/* implicit ZERO_TEST - nonzero if true */

	if (n->hdr.type != TN_EXPR)
	{	if (debug) printf("basiczero: not an expr\n");
		return 0;		/* don't know */
	}

	if (n->hdr.tok == NOT
	&&  (n->rnode->hdr.type == TN_IDENT
	||   n->rnode->hdr.type == TN_ASSIGN))
		return 1;		/* implicit NONZERO_TEST - zero if true */

	if (n->hdr.tok == EQUAL)
	{	if ((n->rnode->hdr.type == TN_INT
		&&   ((leafnode *)n->rnode)->data.ival == 0)
		||  (n->lnode->hdr.type == TN_INT
		&&   ((leafnode *)n->lnode)->data.ival == 0))
			return 1;	/* explicit ZERO_TEST - zero if true */

		if (debug) printf("basiczero: equal fail\n");
		return 0;		/* don't know */
	}
	if (n->hdr.tok == NOT_EQ)
	{	if ((n->rnode->hdr.type == TN_INT
		&&   ((leafnode *)n->rnode)->data.ival == 0)
		||  (n->lnode->hdr.type == TN_INT
		&&  ((leafnode *)n->lnode)->data.ival == 0))
			return -1;	/* explicit NONZERO_TEST - nonzero if true */
		if (debug) printf("basiczero: not_equal fail\n");
		return 0;		/* don't know */
	}

	if (debug) printf("basiczero: other fail\n");
	return 0;
}

static void
sym_unmark(treenode *m, int unused1, int unused2)
{	SymRef *s, *os = (SymRef *) 0;

	for (s = gen_stack->symrefs; s; s = s->nxt)
		if (s->status & SELECTED)
		{	if (!os)
				gen_stack->symrefs = s->nxt;
			else
				os->nxt = s->nxt;

			if (debug) fprintf(stderr, "\tdeleted %s (line %d)\n",
				s->sm->nme->str, s->n?s->n->hdr.line:-1);
		} else
			os = s;
}

static void
sym_update(treenode *m, int val, int unused2)
{	SymRef *s;
	SymList *r;
	treenode *n;

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

	/* if any items on the stack were selected
	 * then a match() operations was executed
	 * which voids the select bits in defuse
	 */
	for (s = gen_stack->symrefs; s; s = s->nxt)
		if (s->status & SELECTED)
			goto after;

	if (n && n->hdr.defuse)
	for (r = n->hdr.defuse->other; r; r = r->nxt)
		if (r->selected)
		{	s = uno_getref(r->sm);
			s->nxt = gen_stack->symrefs;
			s->status = r->mark | SELECTED;
			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);
		}

	for (s = gen_stack->symrefs; s; s = s->nxt)
		if (s->status & SELECTED)
		{	if (debug)
			printf("\tmarked %s = %d (line %d)\n",
				s->sm->nme->str, val, s->n?s->n->hdr.line:-1);
after:			s->s_val = val;
		}
}

static int
known_details(treenode *m, int want)
{	SymRef *s, *t;
	SymList *r;
	GenStack *g = (GenStack *) 0;
	int v = -2;
	int w = 0;
	int anyhits;
#if 0
	for each symbol selected on dfs_stack
	search path backwards for USE of symbol in conditionals
	and determine if this renders its zero-ness known
#endif

	anyhits = 0;
	for (s = gen_stack->symrefs; s; s = s->nxt)
	{
		if (debug)
		fprintf(stderr, "stack: %s -- selected: %d\n", s->sm->nme->str, s->status & SELECTED);

		if (s->status & SELECTED)
		for (g = gen_stack->nxt; g; g = g->nxt)
		{
w = 1;
			/* should still appear in symrefs */
			for (t = g->symrefs; t; t = t->nxt)
				if (t->sm == s->sm)
					break;
			if (!t) goto unknown;
w = 2;
			r = (SymList *) 0;
			if (g->e->hdr.defuse && g->c)
			for (r = g->e->hdr.defuse->other; r; r = r->nxt)
				if (strcmp(r->sm->nme->str, s->sm->nme->str) == 0
				&& ((r->mark & USEafterdef)	/* test after assign */
				||  (r->mark & USE)))		/* straight test */
					break;
w = 3;
			if (r)
			{	anyhits = 1;
				v = basiczero(g->e);		/* 1=known zero, -1=nonzero */
				if (v == 0) goto unknown;	/* i.e., value unknown */
w = 4;
				if (strcmp(((leafnode *)g->c)->data.sval->str, "_true_") == 0)
				{	if (v == want)
					{
	if (debug)
	printf("want=%d, v=%d, known because of: %s == true\n",
		want, v, x_stmnt(g->e));
#if 0
                       v ==  0  -> false (unknown value)
	(want ==  1 && v ==  1) && _true_ -> true  (KNOWN ZERO)
	(want == -1 && v == -1) && _true_ -> true  KNOWN NONZERO

	 want ==  1 && v == -1) && _true_ -> false (not known zero)
	 want == -1 && v ==  1  && _true_ -> false (not knwon nonzero)
#endif
						break;		/* this symbol known zero */
					} else
						goto unknown;	/* unknown or nonzero */
				}
w = 5;
				if (strcmp(((leafnode *)g->c)->data.sval->str, "_false_") == 0)
				{	if (v == -want)		/* known nonzero */
					{
	if (debug)
	printf("want=%d, v=%d, known because of: %s == false\n",
		want, v, x_stmnt(g->e));
#if 0
	 want ==  1 && v == -1) && _false_ -> true (known zero)
	 want == -1 && v ==  1  && _false_ -> true (known nonzero)

	(want ==  1 && v ==  1) && _false_ -> false  (KNOWN ZERO)
	(want == -1 && v == -1) && _false_ -> false  KNOWN NONZERO
#endif
						break;
					} else
						goto unknown;	/* unknown or not zero */