xref: /plan9-contrib/sys/src/cmd/spin/tl_cache.c (revision de2caf28f9ba1a56e70be94a699435d36eb50311)
17dd7cddfSDavid du Colombier /***** tl_spin: tl_cache.c *****/
27dd7cddfSDavid du Colombier 
3*de2caf28SDavid du Colombier /*
4*de2caf28SDavid du Colombier  * This file is part of the public release of Spin. It is subject to the
5*de2caf28SDavid du Colombier  * terms in the LICENSE file that is included in this source directory.
6*de2caf28SDavid du Colombier  * Tool documentation is available at http://spinroot.com
7*de2caf28SDavid du Colombier  *
8*de2caf28SDavid du Colombier  * Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
9*de2caf28SDavid du Colombier  * presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
10*de2caf28SDavid du Colombier  */
117dd7cddfSDavid du Colombier 
127dd7cddfSDavid du Colombier #include "tl.h"
137dd7cddfSDavid du Colombier 
147dd7cddfSDavid du Colombier typedef struct Cache {
157dd7cddfSDavid du Colombier 	Node *before;
167dd7cddfSDavid du Colombier 	Node *after;
177dd7cddfSDavid du Colombier 	int same;
187dd7cddfSDavid du Colombier 	struct Cache *nxt;
197dd7cddfSDavid du Colombier } Cache;
207dd7cddfSDavid du Colombier 
217dd7cddfSDavid du Colombier static Cache	*stored = (Cache *) 0;
227dd7cddfSDavid du Colombier static unsigned long	Caches, CacheHits;
237dd7cddfSDavid du Colombier 
247dd7cddfSDavid du Colombier static int ismatch(Node *, Node *);
25*de2caf28SDavid du Colombier static int sameform(Node *, Node *);
26*de2caf28SDavid du Colombier 
277dd7cddfSDavid du Colombier extern void fatal(char *, char *);
287dd7cddfSDavid du Colombier 
2900d97012SDavid du Colombier void
ini_cache(void)3000d97012SDavid du Colombier ini_cache(void)
3100d97012SDavid du Colombier {
3200d97012SDavid du Colombier 	stored = (Cache *) 0;
3300d97012SDavid du Colombier 	Caches = 0;
3400d97012SDavid du Colombier 	CacheHits = 0;
3500d97012SDavid du Colombier }
3600d97012SDavid du Colombier 
37312a1df1SDavid du Colombier #if 0
387dd7cddfSDavid du Colombier void
397dd7cddfSDavid du Colombier cache_dump(void)
407dd7cddfSDavid du Colombier {	Cache *d; int nr=0;
417dd7cddfSDavid du Colombier 
427dd7cddfSDavid du Colombier 	printf("\nCACHE DUMP:\n");
437dd7cddfSDavid du Colombier 	for (d = stored; d; d = d->nxt, nr++)
447dd7cddfSDavid du Colombier 	{	if (d->same) continue;
457dd7cddfSDavid du Colombier 		printf("B%3d: ", nr); dump(d->before); printf("\n");
467dd7cddfSDavid du Colombier 		printf("A%3d: ", nr); dump(d->after); printf("\n");
477dd7cddfSDavid du Colombier 	}
487dd7cddfSDavid du Colombier 	printf("============\n");
497dd7cddfSDavid du Colombier }
50312a1df1SDavid du Colombier #endif
517dd7cddfSDavid du Colombier 
527dd7cddfSDavid du Colombier Node *
in_cache(Node * n)537dd7cddfSDavid du Colombier in_cache(Node *n)
547dd7cddfSDavid du Colombier {	Cache *d; int nr=0;
557dd7cddfSDavid du Colombier 
567dd7cddfSDavid du Colombier 	for (d = stored; d; d = d->nxt, nr++)
577dd7cddfSDavid du Colombier 		if (isequal(d->before, n))
587dd7cddfSDavid du Colombier 		{	CacheHits++;
597dd7cddfSDavid du Colombier 			if (d->same && ismatch(n, d->before)) return n;
607dd7cddfSDavid du Colombier 			return dupnode(d->after);
617dd7cddfSDavid du Colombier 		}
627dd7cddfSDavid du Colombier 	return ZN;
637dd7cddfSDavid du Colombier }
647dd7cddfSDavid du Colombier 
657dd7cddfSDavid du Colombier Node *
cached(Node * n)667dd7cddfSDavid du Colombier cached(Node *n)
677dd7cddfSDavid du Colombier {	Cache *d;
687dd7cddfSDavid du Colombier 	Node *m;
697dd7cddfSDavid du Colombier 
707dd7cddfSDavid du Colombier 	if (!n) return n;
71312a1df1SDavid du Colombier 	if ((m = in_cache(n)) != ZN)
727dd7cddfSDavid du Colombier 		return m;
737dd7cddfSDavid du Colombier 
747dd7cddfSDavid du Colombier 	Caches++;
757dd7cddfSDavid du Colombier 	d = (Cache *) tl_emalloc(sizeof(Cache));
767dd7cddfSDavid du Colombier 	d->before = dupnode(n);
777dd7cddfSDavid du Colombier 	d->after  = Canonical(n); /* n is released */
787dd7cddfSDavid du Colombier 
797dd7cddfSDavid du Colombier 	if (ismatch(d->before, d->after))
807dd7cddfSDavid du Colombier 	{	d->same = 1;
817dd7cddfSDavid du Colombier 		releasenode(1, d->after);
827dd7cddfSDavid du Colombier 		d->after = d->before;
837dd7cddfSDavid du Colombier 	}
847dd7cddfSDavid du Colombier 	d->nxt = stored;
857dd7cddfSDavid du Colombier 	stored = d;
867dd7cddfSDavid du Colombier 	return dupnode(d->after);
877dd7cddfSDavid du Colombier }
887dd7cddfSDavid du Colombier 
897dd7cddfSDavid du Colombier void
cache_stats(void)907dd7cddfSDavid du Colombier cache_stats(void)
917dd7cddfSDavid du Colombier {
927dd7cddfSDavid du Colombier 	printf("cache stores     : %9ld\n", Caches);
937dd7cddfSDavid du Colombier 	printf("cache hits       : %9ld\n", CacheHits);
947dd7cddfSDavid du Colombier }
957dd7cddfSDavid du Colombier 
967dd7cddfSDavid du Colombier void
releasenode(int all_levels,Node * n)977dd7cddfSDavid du Colombier releasenode(int all_levels, Node *n)
987dd7cddfSDavid du Colombier {
997dd7cddfSDavid du Colombier 	if (!n) return;
1007dd7cddfSDavid du Colombier 
1017dd7cddfSDavid du Colombier 	if (all_levels)
1027dd7cddfSDavid du Colombier 	{	releasenode(1, n->lft);
1037dd7cddfSDavid du Colombier 		n->lft = ZN;
1047dd7cddfSDavid du Colombier 		releasenode(1, n->rgt);
1057dd7cddfSDavid du Colombier 		n->rgt = ZN;
1067dd7cddfSDavid du Colombier 	}
1077dd7cddfSDavid du Colombier 	tfree((void *) n);
1087dd7cddfSDavid du Colombier }
1097dd7cddfSDavid du Colombier 
1107dd7cddfSDavid du Colombier Node *
tl_nn(int t,Node * ll,Node * rl)1117dd7cddfSDavid du Colombier tl_nn(int t, Node *ll, Node *rl)
1127dd7cddfSDavid du Colombier {	Node *n = (Node *) tl_emalloc(sizeof(Node));
1137dd7cddfSDavid du Colombier 
1147dd7cddfSDavid du Colombier 	n->ntyp = (short) t;
1157dd7cddfSDavid du Colombier 	n->lft  = ll;
1167dd7cddfSDavid du Colombier 	n->rgt  = rl;
1177dd7cddfSDavid du Colombier 
1187dd7cddfSDavid du Colombier 	return n;
1197dd7cddfSDavid du Colombier }
1207dd7cddfSDavid du Colombier 
1217dd7cddfSDavid du Colombier Node *
getnode(Node * p)1227dd7cddfSDavid du Colombier getnode(Node *p)
1237dd7cddfSDavid du Colombier {	Node *n;
1247dd7cddfSDavid du Colombier 
1257dd7cddfSDavid du Colombier 	if (!p) return p;
1267dd7cddfSDavid du Colombier 
1277dd7cddfSDavid du Colombier 	n =  (Node *) tl_emalloc(sizeof(Node));
1287dd7cddfSDavid du Colombier 	n->ntyp = p->ntyp;
1297dd7cddfSDavid du Colombier 	n->sym  = p->sym; /* same name */
1307dd7cddfSDavid du Colombier 	n->lft  = p->lft;
1317dd7cddfSDavid du Colombier 	n->rgt  = p->rgt;
1327dd7cddfSDavid du Colombier 
1337dd7cddfSDavid du Colombier 	return n;
1347dd7cddfSDavid du Colombier }
1357dd7cddfSDavid du Colombier 
1367dd7cddfSDavid du Colombier Node *
dupnode(Node * n)1377dd7cddfSDavid du Colombier dupnode(Node *n)
1387dd7cddfSDavid du Colombier {	Node *d;
1397dd7cddfSDavid du Colombier 
1407dd7cddfSDavid du Colombier 	if (!n) return n;
1417dd7cddfSDavid du Colombier 	d = getnode(n);
1427dd7cddfSDavid du Colombier 	d->lft = dupnode(n->lft);
1437dd7cddfSDavid du Colombier 	d->rgt = dupnode(n->rgt);
1447dd7cddfSDavid du Colombier 	return d;
1457dd7cddfSDavid du Colombier }
1467dd7cddfSDavid du Colombier 
1477dd7cddfSDavid du Colombier int
one_lft(int ntyp,Node * x,Node * in)1487dd7cddfSDavid du Colombier one_lft(int ntyp, Node *x, Node *in)
1497dd7cddfSDavid du Colombier {
1507dd7cddfSDavid du Colombier 	if (!x)  return 1;
1517dd7cddfSDavid du Colombier 	if (!in) return 0;
1527dd7cddfSDavid du Colombier 
1537dd7cddfSDavid du Colombier 	if (sameform(x, in))
1547dd7cddfSDavid du Colombier 		return 1;
1557dd7cddfSDavid du Colombier 
1567dd7cddfSDavid du Colombier 	if (in->ntyp != ntyp)
1577dd7cddfSDavid du Colombier 		return 0;
1587dd7cddfSDavid du Colombier 
1597dd7cddfSDavid du Colombier 	if (one_lft(ntyp, x, in->lft))
1607dd7cddfSDavid du Colombier 		return 1;
1617dd7cddfSDavid du Colombier 
1627dd7cddfSDavid du Colombier 	return one_lft(ntyp, x, in->rgt);
1637dd7cddfSDavid du Colombier }
1647dd7cddfSDavid du Colombier 
1657dd7cddfSDavid du Colombier int
all_lfts(int ntyp,Node * from,Node * in)1667dd7cddfSDavid du Colombier all_lfts(int ntyp, Node *from, Node *in)
1677dd7cddfSDavid du Colombier {
1687dd7cddfSDavid du Colombier 	if (!from) return 1;
1697dd7cddfSDavid du Colombier 
1707dd7cddfSDavid du Colombier 	if (from->ntyp != ntyp)
1717dd7cddfSDavid du Colombier 		return one_lft(ntyp, from, in);
1727dd7cddfSDavid du Colombier 
1737dd7cddfSDavid du Colombier 	if (!one_lft(ntyp, from->lft, in))
1747dd7cddfSDavid du Colombier 		return 0;
1757dd7cddfSDavid du Colombier 
1767dd7cddfSDavid du Colombier 	return all_lfts(ntyp, from->rgt, in);
1777dd7cddfSDavid du Colombier }
1787dd7cddfSDavid du Colombier 
1797dd7cddfSDavid du Colombier int
sametrees(int ntyp,Node * a,Node * b)1807dd7cddfSDavid du Colombier sametrees(int ntyp, Node *a, Node *b)
1817dd7cddfSDavid du Colombier {	/* toplevel is an AND or OR */
1827dd7cddfSDavid du Colombier 	/* both trees are right-linked, but the leafs */
1837dd7cddfSDavid du Colombier 	/* can be in different places in the two trees */
1847dd7cddfSDavid du Colombier 
1857dd7cddfSDavid du Colombier 	if (!all_lfts(ntyp, a, b))
1867dd7cddfSDavid du Colombier 		return 0;
1877dd7cddfSDavid du Colombier 
1887dd7cddfSDavid du Colombier 	return all_lfts(ntyp, b, a);
1897dd7cddfSDavid du Colombier }
1907dd7cddfSDavid du Colombier 
191*de2caf28SDavid du Colombier static int	/* a better isequal() */
sameform(Node * a,Node * b)1927dd7cddfSDavid du Colombier sameform(Node *a, Node *b)
1937dd7cddfSDavid du Colombier {
1947dd7cddfSDavid du Colombier 	if (!a && !b) return 1;
1957dd7cddfSDavid du Colombier 	if (!a || !b) return 0;
1967dd7cddfSDavid du Colombier 	if (a->ntyp != b->ntyp) return 0;
1977dd7cddfSDavid du Colombier 
1987dd7cddfSDavid du Colombier 	if (a->sym
1997dd7cddfSDavid du Colombier 	&&  b->sym
2007dd7cddfSDavid du Colombier 	&&  strcmp(a->sym->name, b->sym->name) != 0)
2017dd7cddfSDavid du Colombier 		return 0;
2027dd7cddfSDavid du Colombier 
2037dd7cddfSDavid du Colombier 	switch (a->ntyp) {
2047dd7cddfSDavid du Colombier 	case TRUE:
2057dd7cddfSDavid du Colombier 	case FALSE:
2067dd7cddfSDavid du Colombier 		return 1;
2077dd7cddfSDavid du Colombier 	case PREDICATE:
2087dd7cddfSDavid du Colombier 		if (!a->sym || !b->sym) fatal("sameform...", (char *) 0);
2097dd7cddfSDavid du Colombier 		return !strcmp(a->sym->name, b->sym->name);
2107dd7cddfSDavid du Colombier 
2117dd7cddfSDavid du Colombier 	case NOT:
2127dd7cddfSDavid du Colombier #ifdef NXT
2137dd7cddfSDavid du Colombier 	case NEXT:
2147dd7cddfSDavid du Colombier #endif
215*de2caf28SDavid du Colombier 	case CEXPR:
2167dd7cddfSDavid du Colombier 		return sameform(a->lft, b->lft);
2177dd7cddfSDavid du Colombier 	case U_OPER:
2187dd7cddfSDavid du Colombier 	case V_OPER:
2197dd7cddfSDavid du Colombier 		if (!sameform(a->lft, b->lft))
2207dd7cddfSDavid du Colombier 			return 0;
2217dd7cddfSDavid du Colombier 		if (!sameform(a->rgt, b->rgt))
2227dd7cddfSDavid du Colombier 			return 0;
2237dd7cddfSDavid du Colombier 		return 1;
2247dd7cddfSDavid du Colombier 
2257dd7cddfSDavid du Colombier 	case AND:
2267dd7cddfSDavid du Colombier 	case OR:	/* the hard case */
2277dd7cddfSDavid du Colombier 		return sametrees(a->ntyp, a, b);
2287dd7cddfSDavid du Colombier 
2297dd7cddfSDavid du Colombier 	default:
2307dd7cddfSDavid du Colombier 		printf("type: %d\n", a->ntyp);
2317dd7cddfSDavid du Colombier 		fatal("cannot happen, sameform", (char *) 0);
2327dd7cddfSDavid du Colombier 	}
2337dd7cddfSDavid du Colombier 
2347dd7cddfSDavid du Colombier 	return 0;
2357dd7cddfSDavid du Colombier }
2367dd7cddfSDavid du Colombier 
2377dd7cddfSDavid du Colombier int
isequal(Node * a,Node * b)2387dd7cddfSDavid du Colombier isequal(Node *a, Node *b)
2397dd7cddfSDavid du Colombier {
2407dd7cddfSDavid du Colombier 	if (!a && !b)
2417dd7cddfSDavid du Colombier 		return 1;
2427dd7cddfSDavid du Colombier 
2437dd7cddfSDavid du Colombier 	if (!a || !b)
2447dd7cddfSDavid du Colombier 	{	if (!a)
2457dd7cddfSDavid du Colombier 		{	if (b->ntyp == TRUE)
2467dd7cddfSDavid du Colombier 				return 1;
2477dd7cddfSDavid du Colombier 		} else
2487dd7cddfSDavid du Colombier 		{	if (a->ntyp == TRUE)
2497dd7cddfSDavid du Colombier 				return 1;
2507dd7cddfSDavid du Colombier 		}
2517dd7cddfSDavid du Colombier 		return 0;
2527dd7cddfSDavid du Colombier 	}
2537dd7cddfSDavid du Colombier 	if (a->ntyp != b->ntyp)
2547dd7cddfSDavid du Colombier 		return 0;
2557dd7cddfSDavid du Colombier 
2567dd7cddfSDavid du Colombier 	if (a->sym
2577dd7cddfSDavid du Colombier 	&&  b->sym
2587dd7cddfSDavid du Colombier 	&&  strcmp(a->sym->name, b->sym->name) != 0)
2597dd7cddfSDavid du Colombier 		return 0;
2607dd7cddfSDavid du Colombier 
2617dd7cddfSDavid du Colombier 	if (isequal(a->lft, b->lft)
2627dd7cddfSDavid du Colombier 	&&  isequal(a->rgt, b->rgt))
2637dd7cddfSDavid du Colombier 		return 1;
2647dd7cddfSDavid du Colombier 
2657dd7cddfSDavid du Colombier 	return sameform(a, b);
2667dd7cddfSDavid du Colombier }
2677dd7cddfSDavid du Colombier 
2687dd7cddfSDavid du Colombier static int
ismatch(Node * a,Node * b)2697dd7cddfSDavid du Colombier ismatch(Node *a, Node *b)
2707dd7cddfSDavid du Colombier {
2717dd7cddfSDavid du Colombier 	if (!a && !b) return 1;
2727dd7cddfSDavid du Colombier 	if (!a || !b) return 0;
2737dd7cddfSDavid du Colombier 	if (a->ntyp != b->ntyp) return 0;
2747dd7cddfSDavid du Colombier 
2757dd7cddfSDavid du Colombier 	if (a->sym
2767dd7cddfSDavid du Colombier 	&&  b->sym
2777dd7cddfSDavid du Colombier 	&&  strcmp(a->sym->name, b->sym->name) != 0)
2787dd7cddfSDavid du Colombier 		return 0;
2797dd7cddfSDavid du Colombier 
2807dd7cddfSDavid du Colombier 	if (ismatch(a->lft, b->lft)
2817dd7cddfSDavid du Colombier 	&&  ismatch(a->rgt, b->rgt))
2827dd7cddfSDavid du Colombier 		return 1;
2837dd7cddfSDavid du Colombier 
2847dd7cddfSDavid du Colombier 	return 0;
2857dd7cddfSDavid du Colombier }
2867dd7cddfSDavid du Colombier 
2877dd7cddfSDavid du Colombier int
any_term(Node * srch,Node * in)2887dd7cddfSDavid du Colombier any_term(Node *srch, Node *in)
2897dd7cddfSDavid du Colombier {
2907dd7cddfSDavid du Colombier 	if (!in) return 0;
2917dd7cddfSDavid du Colombier 
2927dd7cddfSDavid du Colombier 	if (in->ntyp == AND)
2937dd7cddfSDavid du Colombier 		return	any_term(srch, in->lft) ||
2947dd7cddfSDavid du Colombier 			any_term(srch, in->rgt);
2957dd7cddfSDavid du Colombier 
2967dd7cddfSDavid du Colombier 	return isequal(in, srch);
2977dd7cddfSDavid du Colombier }
2987dd7cddfSDavid du Colombier 
2997dd7cddfSDavid du Colombier int
any_and(Node * srch,Node * in)3007dd7cddfSDavid du Colombier any_and(Node *srch, Node *in)
3017dd7cddfSDavid du Colombier {
3027dd7cddfSDavid du Colombier 	if (!in) return 0;
3037dd7cddfSDavid du Colombier 
3047dd7cddfSDavid du Colombier 	if (srch->ntyp == AND)
3057dd7cddfSDavid du Colombier 		return	any_and(srch->lft, in) &&
3067dd7cddfSDavid du Colombier 			any_and(srch->rgt, in);
3077dd7cddfSDavid du Colombier 
3087dd7cddfSDavid du Colombier 	return any_term(srch, in);
3097dd7cddfSDavid du Colombier }
3107dd7cddfSDavid du Colombier 
3117dd7cddfSDavid du Colombier int
any_lor(Node * srch,Node * in)3127dd7cddfSDavid du Colombier any_lor(Node *srch, Node *in)
3137dd7cddfSDavid du Colombier {
3147dd7cddfSDavid du Colombier 	if (!in) return 0;
3157dd7cddfSDavid du Colombier 
3167dd7cddfSDavid du Colombier 	if (in->ntyp == OR)
3177dd7cddfSDavid du Colombier 		return	any_lor(srch, in->lft) ||
3187dd7cddfSDavid du Colombier 			any_lor(srch, in->rgt);
3197dd7cddfSDavid du Colombier 
3207dd7cddfSDavid du Colombier 	return isequal(in, srch);
3217dd7cddfSDavid du Colombier }
3227dd7cddfSDavid du Colombier 
3237dd7cddfSDavid du Colombier int
anywhere(int tok,Node * srch,Node * in)3247dd7cddfSDavid du Colombier anywhere(int tok, Node *srch, Node *in)
3257dd7cddfSDavid du Colombier {
3267dd7cddfSDavid du Colombier 	if (!in) return 0;
3277dd7cddfSDavid du Colombier 
3287dd7cddfSDavid du Colombier 	switch (tok) {
3297dd7cddfSDavid du Colombier 	case AND:	return any_and(srch, in);
3307dd7cddfSDavid du Colombier 	case  OR:	return any_lor(srch, in);
3317dd7cddfSDavid du Colombier 	case   0:	return any_term(srch, in);
3327dd7cddfSDavid du Colombier 	}
3337dd7cddfSDavid du Colombier 	fatal("cannot happen, anywhere", (char *) 0);
3347dd7cddfSDavid du Colombier 	return 0;
3357dd7cddfSDavid du Colombier }
336