Import sources from 2011-03-30 iso image

1 files changed, 328 insertions, 0 deletions

diff --git a/sys/src/cmd/spin/tl_cache.c b/sys/src/cmd/spin/tl_cache.c
new file mode 100755
index 000000000..fc902dcb0
--- /dev/null
+++ b/sys/src/cmd/spin/tl_cache.c
@@ -0,0 +1,328 @@
+/***** 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 *);
+
+#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;
+}