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;
}