pangen6.c

这是一个同样来自贝尔实验室的和UNIX有着渊源的操作系统, 其简洁的设计和实现易于我们学习和理解

/***** spin: pangen6.c *****/

/* Copyright (c) 2000-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: [e-mail]            */

/* Abstract syntax tree analysis / slicing (spin option -A) */
/* AST_store stores the fsms's for each proctype            */
/* AST_track keeps track of variables used in properties    */
/* AST_slice starts the slicing algorithm                   */
/*      it first collects more info and then calls          */
/*      AST_criteria to process the slice criteria          */

#include "spin.h"
#ifdef PC
#include "y_tab.h"
#else
#include "y.tab.h"
#endif

extern Ordered	 *all_names;
extern FSM_use   *use_free;
extern FSM_state **fsm_tbl;
extern FSM_state *fsm;
extern int	 verbose, o_max;

static FSM_trans *cur_t;
static FSM_trans *expl_par;
static FSM_trans *expl_var;
static FSM_trans *explicit;

extern void rel_use(FSM_use *);

#define ulong	unsigned long

typedef struct Pair {
	FSM_state	*h;
	int		b;
	struct Pair	*nxt;
} Pair;

typedef struct AST {
	ProcList *p;		/* proctype decl */
	int	i_st;		/* start state */
	int	nstates, nwords;
	int	relevant;
	Pair	*pairs;		/* entry and exit nodes of proper subgraphs */
	FSM_state *fsm;		/* proctype body */
	struct AST *nxt;	/* linked list */
} AST;

typedef struct RPN {		/* relevant proctype names */
	Symbol	*rn;
	struct RPN *nxt;
} RPN;

typedef struct ALIAS {		/* channel aliasing info */
	Lextok	*cnm;		/* this chan */
	int	origin;		/* debugging - origin of the alias */
	struct ALIAS	*alias;	/* can be an alias for these other chans */
	struct ALIAS	*nxt;	/* linked list */
} ALIAS;

typedef struct ChanList {
	Lextok *s;		/* containing stmnt */
	Lextok *n;		/* point of reference - could be struct */
	struct ChanList *nxt;	/* linked list */
} ChanList;

/* a chan alias can be created in one of three ways:
	assignement to chan name
		a = b -- a is now an alias for b
	passing chan name as parameter in run
		run x(b) -- proctype x(chan a)
	passing chan name through channel
		x!b -- x?a
 */

#define USE		1
#define DEF		2
#define DEREF_DEF	4
#define DEREF_USE	8

static AST	*ast;
static ALIAS	*chalcur;
static ALIAS	*chalias;
static ChanList	*chanlist;
static Slicer	*slicer;
static Slicer	*rel_vars;	/* all relevant variables */
static int	AST_Changes;
static int	AST_Round;
static FSM_state no_state;
static RPN	*rpn;
static int	in_recv = 0;

static int	AST_mutual(Lextok *, Lextok *, int);
static void	AST_dominant(void);
static void	AST_hidden(void);
static void	AST_setcur(Lextok *);
static void	check_slice(Lextok *, int);
static void	curtail(AST *);
static void	def_use(Lextok *, int);
static void	name_AST_track(Lextok *, int);
static void	show_expl(void);

static int
AST_isini(Lextok *n)	/* is this an initialized channel */
{	Symbol *s;

	if (!n || !n->sym) return 0;

	s = n->sym;

	if (s->type == CHAN)
		return (s->ini->ntyp == CHAN); /* freshly instantiated */

	if (s->type == STRUCT && n->rgt)
		return AST_isini(n->rgt->lft);

	return 0;
}

static void
AST_var(Lextok *n, Symbol *s, int toplevel)
{
	if (!s) return;

	if (toplevel)
	{	if (s->context && s->type)
			printf(":%s:L:", s->context->name);
		else
			printf("G:");
	}
	printf("%s", s->name); /* array indices ignored */

	if (s->type == STRUCT && n && n->rgt && n->rgt->lft)
	{	printf(":");
		AST_var(n->rgt->lft, n->rgt->lft->sym, 0);
	}
}

static void
name_def_indices(Lextok *n, int code)
{
	if (!n || !n->sym) return;

	if (n->sym->nel != 1)
		def_use(n->lft, code);		/* process the index */

	if (n->sym->type == STRUCT		/* and possible deeper ones */
	&&  n->rgt)
		name_def_indices(n->rgt->lft, code);
}

static void
name_def_use(Lextok *n, int code)
{	FSM_use *u;

	if (!n) return;

	if ((code&USE)
	&&  cur_t->step
	&&  cur_t->step->n)
	{	switch (cur_t->step->n->ntyp) {
		case 'c': /* possible predicate abstraction? */
			n->sym->colnr |= 2; /* yes */
			break;
		default:
			n->sym->colnr |= 1; /* no  */
			break;
		}
	}

	for (u = cur_t->Val[0]; u; u = u->nxt)
		if (AST_mutual(n, u->n, 1)
		&&  u->special == code)
			return;

	if (use_free)
	{	u = use_free;
		use_free = use_free->nxt;
	} else
		u = (FSM_use *) emalloc(sizeof(FSM_use));
	
	u->n = n;
	u->special = code;
	u->nxt = cur_t->Val[0];
	cur_t->Val[0] = u;

	name_def_indices(n, USE|(code&(~DEF)));	/* not def, but perhaps deref */
}

static void
def_use(Lextok *now, int code)
{	Lextok *v;

	if (now)
	switch (now->ntyp) {
	case '!':	
	case UMIN:	
	case '~':
	case 'c':
	case ENABLED:
	case ASSERT:
	case EVAL:
		def_use(now->lft, USE|code);
		break;

	case LEN:
	case FULL:
	case EMPTY:
	case NFULL:
	case NEMPTY:
		def_use(now->lft, DEREF_USE|USE|code);
		break;

	case '/':
	case '*':
	case '-':
	case '+':
	case '%':
	case '&':
	case '^':
	case '|':
	case LE:
	case GE:
	case GT:
	case LT:
	case NE:
	case EQ:
	case OR:
	case AND:
	case LSHIFT:
	case RSHIFT:
		def_use(now->lft, USE|code);
		def_use(now->rgt, USE|code); 
		break;

	case ASGN:
		def_use(now->lft, DEF|code);
		def_use(now->rgt, USE|code);
		break;

	case TYPE:	/* name in parameter list */
		name_def_use(now, code);
		break;

	case NAME:
		name_def_use(now, code);
		break;

	case RUN:
		name_def_use(now, USE);			/* procname - not really needed */
		for (v = now->lft; v; v = v->rgt)
			def_use(v->lft, USE);		/* params */
		break;

	case 's':
		def_use(now->lft, DEREF_DEF|DEREF_USE|USE|code);
		for (v = now->rgt; v; v = v->rgt)
			def_use(v->lft, USE|code);
		break;

	case 'r':
		def_use(now->lft, DEREF_DEF|DEREF_USE|USE|code);
		for (v = now->rgt; v; v = v->rgt)
		{	if (v->lft->ntyp == EVAL)
				def_use(v->lft, code);	/* will add USE */
			else if (v->lft->ntyp != CONST)
				def_use(v->lft, DEF|code);
		}
		break;

	case 'R':
		def_use(now->lft, DEREF_USE|USE|code);
		for (v = now->rgt; v; v = v->rgt)
		{	if (v->lft->ntyp == EVAL)
				def_use(v->lft, code); /* will add USE */
		}
		break;

	case '?':
		def_use(now->lft, USE|code);
		if (now->rgt)
		{	def_use(now->rgt->lft, code);
			def_use(now->rgt->rgt, code);
		}
		break;	

	case PRINT:
		for (v = now->lft; v; v = v->rgt)
			def_use(v->lft, USE|code);
		break;

	case PRINTM:
		def_use(now->lft, USE);
		break;

	case CONST:
	case ELSE:	/* ? */
	case NONPROGRESS:
	case PC_VAL:
	case   'p':
	case   'q':
		break;

	case   '.':
	case  GOTO:
	case BREAK:
	case   '@':
	case D_STEP:
	case ATOMIC:
	case NON_ATOMIC:
	case IF:
	case DO:
	case UNLESS:
	case TIMEOUT:
	case C_CODE:
	case C_EXPR:
	default:
		break;
	}
}

static int
AST_add_alias(Lextok *n, int nr)
{	ALIAS *ca;
	int res;

	for (ca = chalcur->alias; ca; ca = ca->nxt)
		if (AST_mutual(ca->cnm, n, 1))
		{	res = (ca->origin&nr);
			ca->origin |= nr;	/* 1, 2, or 4 - run, asgn, or rcv */
			return (res == 0);	/* 0 if already there with same origin */
		}

	ca = (ALIAS *) emalloc(sizeof(ALIAS));
	ca->cnm = n;
	ca->origin = nr;
	ca->nxt = chalcur->alias;
	chalcur->alias = ca;
	return 1;
}

static void
AST_run_alias(char *pn, char *s, Lextok *t, int parno)
{	Lextok *v;
	int cnt;

	if (!t) return;

	if (t->ntyp == RUN)
	{	if (strcmp(t->sym->name, s) == 0)
		for (v = t->lft, cnt = 1; v; v = v->rgt, cnt++)
			if (cnt == parno)
			{	AST_add_alias(v->lft, 1); /* RUN */
				break;
			}
	} else
	{	AST_run_alias(pn, s, t->lft, parno);
		AST_run_alias(pn, s, t->rgt, parno);
	}
}

static void
AST_findrun(char *s, int parno)
{	FSM_state *f;
	FSM_trans *t;
	AST *a;

	for (a = ast; a; a = a->nxt)		/* automata       */
	for (f = a->fsm; f; f = f->nxt)		/* control states */
	for (t = f->t; t; t = t->nxt)		/* transitions    */
	{	if (t->step)
		AST_run_alias(a->p->n->name, s, t->step->n, parno);
	}
}

static void
AST_par_chans(ProcList *p)	/* find local chan's init'd to chan passed as param */
{	Ordered	*walk;
	Symbol	*sp;

	for (walk = all_names; walk; walk = walk->next)
	{	sp = walk->entry;
		if (sp
		&&  sp->context
		&&  strcmp(sp->context->name, p->n->name) == 0
		&&  sp->Nid >= 0	/* not itself a param */
		&&  sp->type == CHAN
		&&  sp->ini->ntyp == NAME)	/* != CONST and != CHAN */
		{	Lextok *x = nn(ZN, 0, ZN, ZN);
			x->sym = sp;
			AST_setcur(x);
			AST_add_alias(sp->ini, 2);	/* ASGN */
	}	}
}

static void
AST_para(ProcList *p)
{	Lextok *f, *t, *c;
	int cnt = 0;

	AST_par_chans(p);

	for (f = p->p; f; f = f->rgt) 		/* list of types */
	for (t = f->lft; t; t = t->rgt)
	{	if (t->ntyp != ',')
			c = t;
		else
			c = t->lft;	/* expanded struct */

		cnt++;
		if (Sym_typ(c) == CHAN)
		{	ALIAS *na = (ALIAS *) emalloc(sizeof(ALIAS));

			na->cnm = c;
			na->nxt = chalias;
			chalcur = chalias = na;
#if 0
			printf("%s -- (par) -- ", p->n->name);
			AST_var(c, c->sym, 1);
			printf(" => <<");
#endif
			AST_findrun(p->n->name, cnt);
#if 0
			printf(">>\n");
#endif
		}
	}
}

static void
AST_haschan(Lextok *c)
{
	if (!c) return;
	if (Sym_typ(c) == CHAN)
	{	AST_add_alias(c, 2);	/* ASGN */
#if 0
		printf("<<");
		AST_var(c, c->sym, 1);
		printf(">>\n");
#endif
	} else
	{	AST_haschan(c->rgt);
		AST_haschan(c->lft);
	}
}

static int
AST_nrpar(Lextok *n) /* 's' or 'r' */
{	Lextok *m;
	int j = 0;

	for (m = n->rgt; m; m = m->rgt)
		j++;
	return j;
}

static int
AST_ord(Lextok *n, Lextok *s)
{	Lextok *m;
	int j = 0;

	for (m = n->rgt; m; m = m->rgt)
	{	j++;
		if (s->sym == m->lft->sym)
			return j;
	}
	return 0;
}

#if 0
static void
AST_ownership(Symbol *s)
{
	if (!s) return;
	printf("%s:", s->name);
	AST_ownership(s->owner);
}
#endif

static int
AST_mutual(Lextok *a, Lextok *b, int toplevel)
{	Symbol *as, *bs;

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

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

	as = a->sym;
	bs = b->sym;

	if (!as || !bs) return 0;

	if (toplevel && as->context != bs->context)
		return 0;

	if (as->type != bs->type)
		return 0;

	if (strcmp(as->name, bs->name) != 0)
		return 0;

	if (as->type == STRUCT
	&&  a && a->rgt && b && b->rgt)
		return AST_mutual(a->rgt->lft, b->rgt->lft, 0);

	return 1;
}

static void
AST_setcur(Lextok *n)	/* set chalcur */
{	ALIAS *ca;

	for (ca = chalias; ca; ca = ca->nxt)
		if (AST_mutual(ca->cnm, n, 1))	/* if same chan */
		{	chalcur = ca;
			return;
		}

	ca = (ALIAS *) emalloc(sizeof(ALIAS));
	ca->cnm = n;
	ca->nxt = chalias;
	chalcur = chalias = ca;
}

static void
AST_other(AST *a)	/* check chan params in asgns and recvs */
{	FSM_state *f;
	FSM_trans *t;
	FSM_use *u;
	ChanList *cl;

	for (f = a->fsm; f; f = f->nxt)		/* control states */
	for (t = f->t; t; t = t->nxt)		/* transitions    */
	for (u = t->Val[0]; u; u = u->nxt)	/* def/use info   */
		if (Sym_typ(u->n) == CHAN
		&&  (u->special&DEF))		/* def of chan-name  */
		{	AST_setcur(u->n);
			switch (t->step->n->ntyp) {
			case ASGN:
				AST_haschan(t->step->n->rgt);
				break;
			case 'r':
				/* guess sends where name may originate */
				for (cl = chanlist; cl; cl = cl->nxt)	/* all sends */
				{	int a = AST_nrpar(cl->s);
					int b = AST_nrpar(t->step->n);
					if (a != b)	/* matching nrs of params */
						continue;

					a = AST_ord(cl->s, cl->n);
					b = AST_ord(t->step->n, u->n);
					if (a != b)	/* same position in parlist */
						continue;

					AST_add_alias(cl->n, 4); /* RCV assume possible match */
				}
				break;
			default:
				printf("type = %d\n", t->step->n->ntyp);
				non_fatal("unexpected chan def type", (char *) 0);
				break;
		}	}
}

static void
AST_aliases(void)
{	ALIAS *na, *ca;

	for (na = chalias; na; na = na->nxt)
	{	printf("\npossible aliases of ");
		AST_var(na->cnm, na->cnm->sym, 1);
		printf("\n\t");
		for (ca = na->alias; ca; ca = ca->nxt)
		{	if (!ca->cnm->sym)
				printf("no valid name ");
			else
				AST_var(ca->cnm, ca->cnm->sym, 1);
			printf("<");
			if (ca->origin & 1) printf("RUN ");
			if (ca->origin & 2) printf("ASGN ");
			if (ca->origin & 4) printf("RCV ");
			printf("[%s]", AST_isini(ca->cnm)?"Initzd":"Name");