uno_lts.c

C程序漏洞检查

/***** uno: uno_lts.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 <stdarg.h>
#include <ctype.h>
#include "prnttree.h"
#include "token.h"
#include "gram.h"
#include "symtab.h"
#include "uno_lts.h"

/* Names used in user-code inside C procedure specifying the property */
extern char	*property;
extern int	localonly, lintlike, usecheck, gui;

int *testcase;
int x_testcase;

static int	debug = 0;

static DfStack	*dfs_frame;
static DfStack	*dfstack;
static DfStack	*safe_stack;

static FILE	*fd_uno;

       Graphs	*curgraph;	/* set during uno checking */
static Graphs	*find_graph(char *);
static Graphs	*glob_decls;
static Graphs	*graph;		/* all graphs - last created first */
static Graphs	*freegraph;

static LNode	*lnodes;	/* label nodes in cfg */

static PathCond *pathcond;
static PathCond *pathfree;

static Stack	*eol;		/* end of loop */
static Stack	*fol;		/* free frames */
static Stack	*sol;		/* start of loop */

typedef struct Gst Gst;

struct Gst {
	Graphs	*gnm;
	Gst	*nxt;
};

static Gst *grst;	/* fcts that contain calls of other fcts via ptrs */
static Gst *frst;	/* fcts that can be called via a ptr */

static SymExt	*freesymext;
static SymRef	*freesymref;
static Trans	*freetrans;
static State	*freestate;
static State	*NS = (State *) 0;		/* no state */
static State	*lts_dowhile(State *, treenode *);
static State	*lts_for(State *, for_node *);
static State	*lts_if (State *, if_node *);
static State	*lts_node(State *, treenode *);
static State	*lts_switch(State *, treenode *);
static State	*lts_tree(State *, treenode *);
static State	*lts_while(State *, treenode *);
static symentry_t	*mksym(char *, treenode *);
       void	debug_node(treenode *, int, char *);
static int	simple_zero(symentry_t *, treenode *);
static int	simple_nonzero(symentry_t *, treenode *);
extern void	dflow_mark(FILE *, int);

static SwStack	*stck;		/* to detect goto cycles */
static SwStack	*swol;		/* switch structures */

static SymRef	*dfs_free;
static SymRef	*globs;		/* list of global objects being tracked */
static SymRef	*globuse;	/* list of unused global objects */

extern char	cur_in[];

static int	checkpathcond(symentry_t *, treenode *, int);
static int	is_static_fct;
static int	not_a_prototype;
static int	sawdefault;	/* xtract.c has its own copy */

static treenode	*mk_label_node(leafnode *, treenode *n, char *);
static treenode *mk_goto_node(leafnode *);
static Graphs	*new_graph(treenode *, char *);
static SymRef	*add_gstack(symentry_t *, treenode *, int);
static PathCond *getpathframe(void);

static void	dfs_uno(State *);
static void	putpathcond(symentry_t *);
static void	attach_nut(char *, symentry_t *, treenode *);

extern int	has_node_type(treenode *, int);
extern void	dump_defuse(DefUse *, FILE *);
extern int	v_reported(treenode *);
extern void	dfs_bound(State *, treenode *, treenode *, State *);
extern void	explain_bound(char *, ArBound *, treenode *);
extern void	gen_stats(void);
extern void	dfs_generic(State *);

int	depth = 0;
State	*uno_prop;

void
uno_assert(int cond, char *s)
{
	if (!cond)
	{	fprintf(stderr, "uno: %s\n", s);
		exit(1);
	}
}

int
uno_ignore(symentry_t *sm)
{	/* filter out std library fcts and data objects */
	return (sm
	&&  strncmp(sm->fn, "/usr/include", strlen("/usr/include")) == 0);
}

void
uno_warn(char *msg, treenode *n, symentry_t *s)
{	char *str;

	uno_assert(curgraph && s, "bad input to uno_warn");

	if (strcmp(msg, "variable never used (evaluated)") == 0)
	{	if (n)
			str = x_stmnt(n);
		else
			str = "(declaration)";

		fprintf(stdout, "uno: ");

		if (n)	fprintf(stdout, "%s:%d:", n->hdr.fnm, n->hdr.line);
		else if (s) fprintf(stdout, "%s:%d", s->fn, s->ln);

		fprintf(stdout, "\tin fct %s, %s '%s' ",
			curgraph->fctnm, msg, s->nme->str);

	} else if (n && n->hdr.type != TN_EMPTY)
	{
		fprintf(stdout, "uno: in fct %s, %s '%s'",
			curgraph->fctnm, msg, s->nme->str);

		fprintf(stdout, "\n     statement  : %s:%d: ",
			n->hdr.fnm, n->hdr.line);

		if (n->hdr.type != TN_IF)
		{	str = x_stmnt(n);
			if (!str || strlen(str) == 0)
				str = "<stmnt>";
			fprintf(stdout, "%s", str);	/* src of offending stmnt */
		} else
		{	str = x_stmnt(((if_node *)n)->cond);
			if (!str || strlen(str) == 0)
				str = "<cond>";
			fprintf(stdout, "%s", str);	/* src of offending stmnt */
		}

		if (n->hdr.line != s->ln)		/* if different from above */
			fprintf(stdout, "\n     declaration: %s:%d: %s",
				s->fn, s->ln, x_stmnt(s->node)); /* decl src */
	} else
	{	fprintf(stdout, "uno: in fct %s, %s '%s'", curgraph->fctnm, msg, s->nme->str);
	}

	fprintf(stdout, "\n");
}

static State *
create_state(Graphs *g)
{	State *s;

	if (freestate)
	{	s = freestate;
		freestate = s->all;
		memset(s, 0, sizeof(State));
	} else
		s = (State *) emalloc(sizeof(State));

	s->all = g->all;
	g->all = s;
	return s;
}

static void
lts_push_switch(State *st)
{	SwStack *s;

	s = (SwStack *) emalloc(sizeof(SwStack));
	s->s = st;
	s->nxt = swol;
	swol = s;
}

static State *
lts_top_switch(treenode *n)
{
	if (!swol && n) printf("uno: %s:%d error\n", n->hdr.fnm, n->hdr.line);
	uno_assert((int) swol, "switch stack (top)");
	return swol->s;		/* uno cannot tell that swol will be nonzero */
}

static void
lts_pop_switch(void)
{
	uno_assert((int) swol, "switch stack (pop)");
	swol = swol->nxt;
}

static Stack *
lts_new_stack(void)
{	Stack *f;

	if (!fol)
		return (Stack *) emalloc(sizeof(Stack));

	f = fol;
	fol = fol->nxt;
	f->nxt = (Stack *) 0;
	return f;
}

static void
lts_push_start(treenode *n)
{	Stack *f;

	f = lts_new_stack();
	f->n = n;
	f->nxt = sol;
	sol = f;
}

static void
lts_push_end(treenode *n)
{	Stack *f;

	f = lts_new_stack();
	f->status = 1;
	f->n = n;
	f->nxt = eol;
	eol = f;
}

static int
has_fctcalls(DefUse *d)
{	SymList *s;

	if (d)
	for (s = d->other; s; s = s->nxt)
		if (s->mark & FCALL)
			return 1;
	return 0;
}

static void
saw_break(void)
{
	if (eol) eol->status = 1;
}

Stack *fallthru;

static void
show_fall(void)
{	Stack *f;
	int cnt = 0;
	Stack *lst = (Stack *) 0;
	char *s, *t;

	if (!fallthru) return;

	for (f = fallthru; f; lst = f, f = f->nxt)
		if (lst && lst->n->hdr.line == f->n->hdr.line + 1)
		{	f->status = 1;
			lst->status = 1;
		}

	for (f = fallthru; f; lst = f, f = f->nxt)
		if (f->status == 0)
			cnt++;

	if (cnt == 0) return;

	fprintf(stdout, "uno: fallthroughs in switch stmnt:");
	for (f = fallthru; f; f = f->nxt)
	{
		if (f->status != 0) continue;

		s = x_stmnt(f->n);
		if (strlen(s) > 0)
		{	t = strchr(s, ':');
			if (t) *t = '\0';
		}
#if 0
		if ((cnt++ % 3) == 0 || gui == 1)
#endif
			fprintf(stdout, "\n");
		fprintf(stdout, "\t%s:%d:",
			f->n->hdr.fnm, f->n->hdr.line);
		if (strlen(s) > 0)
			fprintf(stdout, " <%s>", s);
	}
	fprintf(stdout, "\n");
}

static void
want_break(treenode *n)
{	Stack *f;
	uno_assert((int) eol, "case outside switch");

	if (lintlike && !eol->status)	/* uno cannot tell that eol is nonzero */
	{	if (fol)
		{	f = fol;
			fol = fol->nxt;
			memset(f, 0, sizeof(Stack));
		} else
			f = (Stack *) emalloc(sizeof(Stack));
		f->n = n;
		f->nxt = fallthru;
		fallthru = f;
	}
	eol->status = 0;
}

static Stack *
rel_sframe(Stack *f)
{
	if (f)
	{	rel_sframe(f->nxt);
		f->nxt = fol;
		fol = f;
	}
	return (Stack *) 0;
}

static void
lts_pop_start(void)
{	Stack *f;

	uno_assert((int) sol, "start stack underflow");
	f = sol;
	sol = sol->nxt;

	f->nxt = fol;
	fol = f;
}

static void
lts_pop_end(void)
{	Stack *f;

	uno_assert((int) eol, "end stack underflow");

	f = eol;
	eol = eol->nxt;

	f->nxt = fol;
	fol = f;
}

static treenode *
lts_top_start(void)
{
	uno_assert((int) sol, "start stack (top)");
	return sol->n;		/* uno cannot tell that sol will be nonzero */
}

static treenode *
lts_top_end(void)
{
	uno_assert((int) eol, "end stack (top)");
	eol->status = 1;	/* uno cannot tell that eol will be nonzero */
	return eol->n;
}

static LNode *freelabels;

static LNode *
rel_label(LNode *n)
{
	if (n)
	{	rel_label(n->nxt);
		n->nxt = freelabels;
		freelabels = n;
	}
	return (LNode *) 0;
}

static void
record_label(treenode *s, State *n)	/* associate symentry with state in cfg */
{	LNode *ln;
	leafnode *x = (leafnode *) s;

	uno_assert((int) (x && n), "bad call to record_label");

	if (freelabels)
	{	ln = freelabels;
		freelabels = ln->nxt;
		memset(ln, 0, sizeof(LNode));
	} else
		ln = (LNode *) emalloc(sizeof(LNode));
	ln->s = x->data.sval->str;
	ln->f = curgraph?curgraph->fctnm:"_noname_";
	ln->n = n;
	ln->nxt = lnodes;
	lnodes = ln;
}

static State *
lts_label_find(char *s)
{	LNode *ln;

	uno_assert((int) s, "bad call to lts_label_find");

	for (ln = lnodes; ln; ln = ln->nxt)
		if (ln->s == s
		&&  ln->f == curgraph->fctnm)
		{	if (0)
			fprintf(stderr, "label match %s (N%u)\n", s, ln->n->n);
			return ln->n;
		}

	fprintf(stderr, "error: label %s not defined\n", s);
	return NS;
}

static State *
lts_redirect(State *s)
{	State *st = s;
	leafnode *ln;
	SwStack *frame;

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

	for (frame = stck; frame; frame = frame->nxt)
		if (frame->s == s)
		{	fprintf(stderr, "uno: %s:%d: goto cycle\n",
				s->n->hdr.fnm,
				s->n->hdr.line);
			return s;
		}

	frame = (SwStack *) emalloc(sizeof(SwStack));
	frame->s = s;
	frame->nxt = stck;
	stck = frame;
	
	if (s->n->hdr.which == NODE_T)
	{	switch (s->n->hdr.type) {
		case TN_JUMP:
			if (s->n->hdr.tok == RETURN)
				break;
			if (ln = (leafnode *) s->n->lnode)	/* assign */
			{	st = lts_label_find(ln->data.sval->str);
				if (!st) st = s;
			}
			break;

		case TN_BLOCK:
		case TN_STEMNT:
		case TN_LABEL:	/* skip fillers, if unique successor */
			if (!s->succ)	/* not yet set, but already known to be unique */
				st = s->nxt;
			else if (!s->succ->nxt)
				st = s->succ->branch;

			if (!st) st = s;
			break;
	}	}

	if (st != s)
		st = lts_redirect(st);

	stck = stck->nxt;	/* pop frame stack */

	return st;
}

SymRef *
rev_release(SymRef *r)	/* release a list of symrefs */
{
	if (r)
	{	rev_release(r->nxt);
		r->nxt = dfs_free;
		dfs_free = r;
	}
	return (SymRef *) 0;
}

static void
cfg_unvisit(State *t)
{	State *s;

	for (s = t; s; s = s->all)
	{	s->visited = 0;
		s->snapshot = rev_release(s->snapshot);
	}
}

typedef struct EX	EX;
struct EX {
	char	*f;
	EX	*nxt;
};
EX *exs;

void
custom_exit(char *s)
{	EX *nx;

	nx = (EX *) emalloc(sizeof(EX));
	nx->f = (char *) emalloc(strlen(s)+1);
	strcpy(nx->f, s);
	nx->nxt = exs;
	exs = nx;
}

static int
no_return(char *s)
{	EX *nx;

	for (nx = exs; nx; nx = nx->nxt)
		if (strcmp(nx->f, s) == 0)
			return 1;
	return 0;
}

static Trans *
get_trans(void)
{	Trans *t;

	if (freetrans)
	{	t = freetrans;
		freetrans = t->nxt;
		memset(t, 0, sizeof(Trans));
	} else
		t = (Trans *) emalloc(sizeof(Trans));
	return t;
}

static void
prep_graph(Graphs *g)
{	State *s;
	Trans *t;
	int cnt;

	curgraph = g;

	for (s = g->all; s; s = s->all)
	{	s->visited = 0;
		if (!s->succ)
		{	if (s->n)
			{	if (s->n->hdr.tok == RETURN)
					continue;

				if (s->n->hdr.type == TN_FUNC_CALL
				&&  s->n->lnode->hdr.type == TN_IDENT
				&&  no_return(((leafnode *)s->n->lnode)->data.sval->str))
					continue;
			}

			if (s->n
			&&  s->n->hdr.tok != GOTO
			&&  s->n->hdr.tok != COLON
			&& !s->nxt
			&&  strcmp(s->n->hdr.fnm, "-1") != 0)
			{	g->status |= 2;	/* no value returned */

				if (0) printf("no value returned at %s:%d: -- %s = %d\n",
					s->n->hdr.fnm, s->n->hdr.line,
					toksym(s->n->hdr.tok,0),
					s->n->hdr.tok);
				if (debug)
				printf("prepgraph %s adds 2 <%d:%d> %s:%d\n",
					g->fctnm,
					s->n->hdr.type,
					s->n->hdr.tok,
					s->n->hdr.fnm,
					s->n->hdr.line);
			}

			t = get_trans();
			t->branch = lts_redirect(s->nxt);
			t->nxt = (Trans *) 0;
			s->succ = t;
		} else
		{	cnt = 0;
			for (t = s->succ; t; t = t->nxt)
			{	t->branch = lts_redirect(t->branch);
				cnt++;
			}