/***** spin: pangen5.c *****/ /* Copyright (c) 1999-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            */ #include "spin.h"#include "y.tab.h" typedef struct BuildStack {	FSM_trans *t;	struct BuildStack *nxt;} BuildStack; extern ProcList	*rdy;extern int verbose, eventmapnr, claimnr, rvopt, export_ast, u_sync;extern Element *Al_El; static FSM_state *fsm_free;static FSM_trans *trans_free;static BuildStack *bs, *bf;static int max_st_id;static int cur_st_id;int o_max;FSM_state *fsm;FSM_state **fsm_tbl;FSM_use   *use_free; static void ana_seq(Sequence *);static void ana_stmnt(FSM_trans *, Lextok *, int); extern void AST_slice(void);extern void AST_store(ProcList *, int);extern int  has_global(Lextok *);extern void exit(int); static voidfsm_table(void){	FSM_state *f;	max_st_id += 2;	/* fprintf(stderr, "omax %d, max=%d\n", o_max, max_st_id); */	if (o_max < max_st_id)	{	o_max = max_st_id;		fsm_tbl = (FSM_state **) emalloc(max_st_id * sizeof(FSM_state *));	} else		memset((char *)fsm_tbl, 0, max_st_id * sizeof(FSM_state *));	cur_st_id = max_st_id;	max_st_id = 0; 	for (f = fsm; f; f = f->nxt)		fsm_tbl[f->from] = f;} static intFSM_DFS(int from, FSM_use *u){	FSM_state *f;	FSM_trans *t;	FSM_use *v;	int n; 	if (from == 0)		return 1; 	f = fsm_tbl[from]; 	if (!f)	{	printf("cannot find state %d\n", from);		fatal("fsm_dfs: cannot happen\n", (char *) 0);	} 	if (f->seen)		return 1;	f->seen = 1; 	for (t = f->t; t; t = t->nxt)	{		for (n = 0; n < 2; n++)		for (v = t->Val[n]; v; v = v->nxt)			if (u->var == v->var)				return n;	/* a read or write */ 		if (!FSM_DFS(t->to, u))			return 0;	}	return 1;} static voidnew_dfs(void){	int i; 	for (i = 0; i < cur_st_id; i++)		if (fsm_tbl[i])			fsm_tbl[i]->seen = 0;} static intgood_dead(Element *e, FSM_use *u){	switch (u->special) {	case 2:	/* ok if it's a receive */		if (e->n->ntyp == ASGN		&&  e->n->rgt->ntyp == CONST		&&  e->n->rgt->val == 0)			return 0;		break;	case 1:	/* must be able to use oval */		if (e->n->ntyp != 'c'		&&  e->n->ntyp != 'r')			return 0;	/* can't really happen */		break;	}	return 1;} #if 0static int howdeep = 0;#endif static inteligible(FSM_trans *v){	Element	*el = ZE;	Lextok	*lt = ZN; 	if (v) el = v->step;	if (el) lt = v->step->n; 	if (!lt				/* dead end */	||  v->nxt			/* has alternatives */	||  el->esc			/* has an escape */	||  (el->status&CHECK2)		/* remotely referenced */	||  lt->ntyp == ATOMIC	||  lt->ntyp == NON_ATOMIC	/* used for inlines -- should be able to handle this */	||  lt->ntyp == IF	||  lt->ntyp == C_CODE	||  lt->ntyp == C_EXPR	||  has_lab(el, 0)		/* any label at all */ 	||  lt->ntyp == DO	||  lt->ntyp == UNLESS	||  lt->ntyp == D_STEP	||  lt->ntyp == ELSE	||  lt->ntyp == '@'	||  lt->ntyp == 'c'	||  lt->ntyp == 'r'	||  lt->ntyp == 's')		return 0; 	if (!(el->status&(2|4)))	/* not atomic */	{	int unsafe = (el->status&I_GLOB)?1:has_global(el->n);		if (unsafe)			return 0;	} 	return 1;} static intcanfill_in(FSM_trans *v){	Element	*el = v->step;	Lextok	*lt = v->step->n; 	if (!lt				/* dead end */	||  v->nxt			/* has alternatives */	||  el->esc			/* has an escape */	||  (el->status&CHECK2))	/* remotely referenced */		return 0; 	if (!(el->status&(2|4))		/* not atomic */	&&  ((el->status&I_GLOB)	||   has_global(el->n)))	/* and not safe */		return 0; 	return 1;} static intpushbuild(FSM_trans *v){	BuildStack *b; 	for (b = bs; b; b = b->nxt)		if (b->t == v)			return 0;	if (bf)	{	b = bf;		bf = bf->nxt;	} else		b = (BuildStack *) emalloc(sizeof(BuildStack));	b->t = v;	b->nxt = bs;	bs = b;	return 1;} static voidpopbuild(void){	BuildStack *f;	if (!bs)		fatal("cannot happen, popbuild", (char *) 0);	f = bs;	bs = bs->nxt;	f->nxt = bf;	bf = f;				/* freelist */} static intbuild_step(FSM_trans *v){	FSM_state *f;	Element	*el;#if 0	Lextok	*lt = ZN;#endif	int	st;	int	r; 	if (!v) return -1; 	el = v->step;	st = v->to; 	if (!el) return -1; 	if (v->step->merge)		return v->step->merge;	/* already done */ 	if (!eligible(v))		/* non-blocking */		return -1; 	if (!pushbuild(v))		/* cycle detected */		return -1;		/* break cycle */ 	f = fsm_tbl[st];#if 0	lt = v->step->n;	if (verbose&32)	{	if (++howdeep == 1)			printf("spin: %s:%d, merge:\n", lt->fn->name, lt->ln);		printf("\t[%d] <seqno %d>\t", howdeep, el->seqno);		comment(stdout, lt, 0);		printf(";\n");	}#endif	r = build_step(f->t);	v->step->merge = (r == -1) ? st : r;#if 0	if (verbose&32)	{	printf("	merge value: %d (st=%d,r=%d, line %d)\n",			v->step->merge, st, r, el->n->ln);		howdeep--;	}#endif	popbuild(); 	return v->step->merge;} static voidFSM_MERGER(/* char *pname */ void)	/* find candidates for safely merging steps */{	FSM_state *f, *g;	FSM_trans *t;	Lextok	*lt; 	for (f = fsm; f; f = f->nxt)		/* all states */	for (t = f->t; t; t = t->nxt)		/* all edges */	{	if (!t->step) continue;		/* happens with 'unless' */ 		t->step->merge_in = f->in;	/* ?? */ 		if (t->step->merge)			continue;		lt = t->step->n; 		if (lt->ntyp == 'c'		||  lt->ntyp == 'r'		||  lt->ntyp == 's')	/* blocking stmnts */			continue;	/* handled in 2nd scan */ 		if (!eligible(t))			continue; 		g = fsm_tbl[t->to];		if (!g || !eligible(g->t))		{#define SINGLES#ifdef SINGLES			t->step->merge_single = t->to;#if 0			if ((verbose&32))			{	printf("spin: %s:%d, merge_single:\n\t<seqno %d>\t",					t->step->n->fn->name,					t->step->n->ln,					t->step->seqno);				comment(stdout, t->step->n, 0);				printf(";\n");			}#endif#endif			/* t is an isolated eligible step:			 *			 * a merge_start can connect to a proper			 * merge chain or to a merge_single			 * a merge chain can be preceded by			 * a merge_start, but not by a merge_single			 */ 			continue;		} 		(void) build_step(t);	} 	/* 2nd scan -- find possible merge_starts */ 	for (f = fsm; f; f = f->nxt)		/* all states */	for (t = f->t; t; t = t->nxt)		/* all edges */	{	if (!t->step || t->step->merge)			continue; 		lt = t->step->n;#if 0	4.1.3:	an rv send operation inside an atomic, *loses* atomicity	when executed	and should therefore never be merged with a subsequent	statement within the atomic sequence	the same is not true for non-rv send operations#endif 		if (lt->ntyp == 'c'	/* potentially blocking stmnts */		||  lt->ntyp == 'r'		||  (lt->ntyp == 's' && u_sync == 0))	/* added !u_sync in 4.1.3 */		{	if (!canfill_in(t))		/* atomic, non-global, etc. */				continue; 			g = fsm_tbl[t->to];			if (!g || !g->t || !g->t->step)				continue;			if (g->t->step->merge)				t->step->merge_start = g->t->step->merge;#ifdef SINGLES			else if (g->t->step->merge_single)				t->step->merge_start = g->t->step->merge_single;#endif#if 0			if ((verbose&32)			&& t->step->merge_start)			{	printf("spin: %s:%d, merge_START:\n\t<seqno %d>\t",						lt->fn->name, lt->ln,						t->step->seqno);				comment(stdout, lt, 0);				printf(";\n");			}#endif		}	}} static voidFSM_ANA(void){	FSM_state *f;	FSM_trans *t;	FSM_use *u, *v, *w;	int n; 	for (f = fsm; f; f = f->nxt)		/* all states */	for (t = f->t; t; t = t->nxt)		/* all edges */	for (n = 0; n < 2; n++)			/* reads and writes */	for (u = t->Val[n]; u; u = u->nxt)	{	if (!u->var->context	/* global */		||   u->var->type == CHAN		||   u->var->type == STRUCT)			continue;		new_dfs();		if (FSM_DFS(t->to, u))	/* cannot hit read before hitting write */			u->special = n+1;	/* means, reset to 0 after use */	} 	if (!export_ast)	for (f = fsm; f; f = f->nxt)	for (t = f->t; t; t = t->nxt)	for (n = 0; n < 2; n++)	for (u = t->Val[n], w = (FSM_use *) 0; u; )	{	if (u->special)		{	v = u->nxt;			if (!w)			/* remove from list */				t->Val[n] = v;			else				w->nxt = v;#if q			if (verbose&32)			{	printf("%s : %3d:  %d -> %d \t",					t->step->n->fn->name,					t->step->n->ln,					f->from,					t->to);				comment(stdout, t->step->n, 0);				printf("\t%c%d: %s\n", n==0?'R':'L',					u->special, u->var->name);			}#endif			if (good_dead(t->step, u))			{	u->nxt = t->step->dead;	/* insert into dead */				t->step->dead = u;			}			u = v;		} else		{	w = u;			u = u->nxt;	}	}} voidrel_use(FSM_use *u){	if (!u) return;	rel_use(u->nxt);	u->var = (Symbol *) 0;	u->special = 0;	u->nxt = use_free;	use_free = u;} static voidrel_trans(FSM_trans *t){	if (!t) return;	rel_trans(t->nxt);	rel_use(t->Val[0]);	rel_use(t->Val[1]);	t->Val[0] = t->Val[1] = (FSM_use *) 0;	t->nxt = trans_free;	trans_free = t;} static voidrel_state(FSM_state *f){	if (!f) return;	rel_state(f->nxt);	rel_trans(f->t);	f->t = (FSM_trans *) 0;	f->nxt = fsm_free;	fsm_free = f;} static voidFSM_DEL(void){	rel_state(fsm);	fsm = (FSM_state *) 0;} static FSM_state *mkstate(int s){	FSM_state *f; 	/* fsm_tbl isn't allocated yet */	for (f = fsm; f; f = f->nxt)		if (f->from == s)			break;	if (!f)	{	if (fsm_free)		{	f = fsm_free;			memset(f, 0, sizeof(FSM_state));			fsm_free = fsm_free->nxt;		} else			f = (FSM_state *) emalloc(sizeof(FSM_state));		f->from = s;		f->t = (FSM_trans *) 0;		f->nxt = fsm;		fsm = f;		if (s > max_st_id)			max_st_id = s;	}	return f;} static FSM_trans *get_trans(int to){	FSM_trans *t; 	if (trans_free)	{	t = trans_free;		memset(t, 0, sizeof(FSM_trans));		trans_free = trans_free->nxt;	} else		t = (FSM_trans *) emalloc(sizeof(FSM_trans)); 	t->to = to;	return t;} static voidFSM_EDGE(int from, int to, Element *e){	FSM_state *f;

Lines 1–500 of 856. Load more