/***** 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 *); voidini_cache(void){	stored = (Cache *) 0;	Caches = 0;	CacheHits = 0;} #if 0voidcache_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);} voidcache_stats(void){	printf("cache stores     : %9ld\n", Caches);	printf("cache hits       : %9ld\n", CacheHits);} voidreleasenode(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;} intone_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);} intall_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);} intsametrees(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;} intisequal(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 intismatch(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;} intany_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);} intany_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);} intany_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);} intanywhere(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;}