Subversion Repositories planix.SVN

/***** tl_spin: tl_cache.c *****/

/* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories.     */

/* All Rights Reserved.  This software is for educational purposes only.  */

/* No guarantee whatsoever is expressed or implied by the distribution of */

/* this code.  Permission is given to distribute this code provided that  */

/* this introductory message is not removed and no monies are exchanged.  */

/* Software written by Gerard J. Holzmann.  For tool documentation see:   */

/*             http://spinroot.com/                                       */

/* Send all bug-reports and/or questions to: bugs@spinroot.com            */

/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */

/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.   */

#include "tl.h"

typedef struct Cache {

	Node *before;

	Node *after;

	int same;

	struct Cache *nxt;

} Cache;

static Cache	*stored = (Cache *) 0;

static unsigned long	Caches, CacheHits;

static int	ismatch(Node *, Node *);

extern void fatal(char *, char *);

int	sameform(Node *, Node *);

void

ini_cache(void)

{

	stored = (Cache *) 0;

	Caches = 0;

	CacheHits = 0;

}

#if 0

void

cache_dump(void)

{	Cache *d; int nr=0;

	printf("\nCACHE DUMP:\n");

	for (d = stored; d; d = d->nxt, nr++)

	{	if (d->same) continue;

		printf("B%3d: ", nr); dump(d->before); printf("\n");

		printf("A%3d: ", nr); dump(d->after); printf("\n");

	}

	printf("============\n");

}

#endif

Node *

in_cache(Node *n)

{	Cache *d; int nr=0;

	for (d = stored; d; d = d->nxt, nr++)

		if (isequal(d->before, n))

		{	CacheHits++;

			if (d->same && ismatch(n, d->before)) return n;

			return dupnode(d->after);

		}

	return ZN;

}

Node *

cached(Node *n)

{	Cache *d;

	Node *m;

	if (!n) return n;

	if ((m = in_cache(n)) != ZN)

		return m;

	Caches++;

	d = (Cache *) tl_emalloc(sizeof(Cache));

	d->before = dupnode(n);

	d->after  = Canonical(n); /* n is released */

	if (ismatch(d->before, d->after))

	{	d->same = 1;

		releasenode(1, d->after);

		d->after = d->before;

	}

	d->nxt = stored;

	stored = d;

	return dupnode(d->after);

}

void

cache_stats(void)

{

	printf("cache stores     : %9ld\n", Caches);

	printf("cache hits       : %9ld\n", CacheHits);

}

void

releasenode(int all_levels, Node *n)

{

	if (!n) return;

	if (all_levels)

	{	releasenode(1, n->lft);

		n->lft = ZN;

		releasenode(1, n->rgt);

		n->rgt = ZN;

	}

	tfree((void *) n);

}

Node *

tl_nn(int t, Node *ll, Node *rl)

{	Node *n = (Node *) tl_emalloc(sizeof(Node));

	n->ntyp = (short) t;

	n->lft  = ll;

	n->rgt  = rl;

	return n;

}

Node *

getnode(Node *p)

{	Node *n;

	if (!p) return p;

	n =  (Node *) tl_emalloc(sizeof(Node));

	n->ntyp = p->ntyp;

	n->sym  = p->sym; /* same name */

	n->lft  = p->lft;

	n->rgt  = p->rgt;

	return n;

}

Node *

dupnode(Node *n)

{	Node *d;

	if (!n) return n;

	d = getnode(n);

	d->lft = dupnode(n->lft);

	d->rgt = dupnode(n->rgt);

	return d;

}

int

one_lft(int ntyp, Node *x, Node *in)

{

	if (!x)  return 1;

	if (!in) return 0;

	if (sameform(x, in))

		return 1;

	if (in->ntyp != ntyp)

		return 0;

	if (one_lft(ntyp, x, in->lft))

		return 1;

	return one_lft(ntyp, x, in->rgt);

}

int

all_lfts(int ntyp, Node *from, Node *in)

{

	if (!from) return 1;

	if (from->ntyp != ntyp)

		return one_lft(ntyp, from, in);

	if (!one_lft(ntyp, from->lft, in))

		return 0;

	return all_lfts(ntyp, from->rgt, in);

}

int

sametrees(int ntyp, Node *a, Node *b)

{	/* toplevel is an AND or OR */

	/* both trees are right-linked, but the leafs */

	/* can be in different places in the two trees */

	if (!all_lfts(ntyp, a, b))

		return 0;

	return all_lfts(ntyp, b, a);

}

int	/* a better isequal() */

sameform(Node *a, Node *b)

{

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

	if (!a || !b) return 0;

	if (a->ntyp != b->ntyp) return 0;

	if (a->sym

	&&  b->sym

	&&  strcmp(a->sym->name, b->sym->name) != 0)

		return 0;

	switch (a->ntyp) {

	case TRUE:

	case FALSE:

		return 1;

	case PREDICATE:

		if (!a->sym || !b->sym) fatal("sameform...", (char *) 0);

		return !strcmp(a->sym->name, b->sym->name);

	case NOT:

#ifdef NXT

	case NEXT:

#endif

		return sameform(a->lft, b->lft);

	case U_OPER:

	case V_OPER:

		if (!sameform(a->lft, b->lft))

			return 0;

		if (!sameform(a->rgt, b->rgt))

			return 0;

		return 1;

	case AND:

	case OR:	/* the hard case */

		return sametrees(a->ntyp, a, b);

	default:

		printf("type: %d\n", a->ntyp);

		fatal("cannot happen, sameform", (char *) 0);

	}

	return 0;

}

int

isequal(Node *a, Node *b)

{

	if (!a && !b)

		return 1;

	if (!a || !b)

	{	if (!a)

		{	if (b->ntyp == TRUE)

				return 1;

		} else

		{	if (a->ntyp == TRUE)

				return 1;

		}

		return 0;

	}

	if (a->ntyp != b->ntyp)

		return 0;

	if (a->sym

	&&  b->sym

	&&  strcmp(a->sym->name, b->sym->name) != 0)

		return 0;

	if (isequal(a->lft, b->lft)

	&&  isequal(a->rgt, b->rgt))

		return 1;

	return sameform(a, b);

}

static int

ismatch(Node *a, Node *b)

{

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

	if (!a || !b) return 0;

	if (a->ntyp != b->ntyp) return 0;

	if (a->sym

	&&  b->sym

	&&  strcmp(a->sym->name, b->sym->name) != 0)

		return 0;

	if (ismatch(a->lft, b->lft)

	&&  ismatch(a->rgt, b->rgt))

		return 1;

	return 0;

}

int

any_term(Node *srch, Node *in)

{

	if (!in) return 0;

	if (in->ntyp == AND)

		return	any_term(srch, in->lft) ||

			any_term(srch, in->rgt);

	return isequal(in, srch);

}

int

any_and(Node *srch, Node *in)

{

	if (!in) return 0;

	if (srch->ntyp == AND)

		return	any_and(srch->lft, in) &&

			any_and(srch->rgt, in);

	return any_term(srch, in);

}

int

any_lor(Node *srch, Node *in)

{

	if (!in) return 0;

	if (in->ntyp == OR)

		return	any_lor(srch, in->lft) ||

			any_lor(srch, in->rgt);

	return isequal(in, srch);

}

int

anywhere(int tok, Node *srch, Node *in)

{

	if (!in) return 0;

	switch (tok) {

	case AND:	return any_and(srch, in);

	case  OR:	return any_lor(srch, in);

	case   0:	return any_term(srch, in);

	}

	fatal("cannot happen, anywhere", (char *) 0);

	return 0;

}