flow.c

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

/***** spin: flow.c *****/

/* Copyright (c) 1989-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]            */

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

extern Symbol	*Fname;
extern int	nr_errs, lineno, verbose;
extern short	has_unless, has_badelse;

Element *Al_El = ZE;
Label	*labtab = (Label *) 0;
int	Unique=0, Elcnt=0, DstepStart = -1;

static Lbreak	*breakstack = (Lbreak *) 0;
static Lextok	*innermost;
static SeqList	*cur_s = (SeqList *) 0;
static int	break_id=0;

static Element	*if_seq(Lextok *);
static Element	*new_el(Lextok *);
static Element	*unless_seq(Lextok *);
static void	add_el(Element *, Sequence *);
static void	attach_escape(Sequence *, Sequence *);
static void	mov_lab(Symbol *, Element *, Element *);
static void	walk_atomic(Element *, Element *, int);

void
open_seq(int top)
{	SeqList *t;
	Sequence *s = (Sequence *) emalloc(sizeof(Sequence));

	t = seqlist(s, cur_s);
	cur_s = t;
	if (top) Elcnt = 1;
}

void
rem_Seq(void)
{
	DstepStart = Unique;
}

void
unrem_Seq(void)
{
	DstepStart = -1;
}

static int
Rjumpslocal(Element *q, Element *stop)
{	Element *lb, *f;
	SeqList *h;

	/* allow no jumps out of a d_step sequence */
	for (f = q; f && f != stop; f = f->nxt)
	{	if (f && f->n && f->n->ntyp == GOTO)
		{	lb = get_lab(f->n, 0);
			if (!lb || lb->Seqno < DstepStart)
			{	lineno = f->n->ln;
				Fname = f->n->fn;
				return 0;
		}	}
		for (h = f->sub; h; h = h->nxt)
		{	if (!Rjumpslocal(h->this->frst, h->this->last))
				return 0;
	
	}	}
	return 1;
}

void
cross_dsteps(Lextok *a, Lextok *b)
{
	if (a && b
	&&  a->indstep != b->indstep)
	{	lineno = a->ln;
		Fname  = a->fn;
		fatal("jump into d_step sequence", (char *) 0);
	}
}

int
is_skip(Lextok *n)
{
	return (n->ntyp == PRINT
	||	n->ntyp == PRINTM
	||	(n->ntyp == 'c'
		&& n->lft
		&& n->lft->ntyp == CONST
		&& n->lft->val  == 1));
}

void
check_sequence(Sequence *s)
{	Element *e, *le = ZE;
	Lextok *n;
	int cnt = 0;

	for (e = s->frst; e; le = e, e = e->nxt)
	{	n = e->n;
		if (is_skip(n) && !has_lab(e, 0))
		{	cnt++;
			if (cnt > 1
			&&  n->ntyp != PRINT
			&&  n->ntyp != PRINTM)
			{	if (verbose&32)
					printf("spin: line %d %s, redundant skip\n",
						n->ln, n->fn->name);
				if (e != s->frst
				&&  e != s->last
				&&  e != s->extent)
				{	e->status |= DONE;	/* not unreachable */
					le->nxt = e->nxt;	/* remove it */
					e = le;
				}
			}
		} else
			cnt = 0;
	}
}

void
prune_opts(Lextok *n)
{	SeqList *l;
	extern Symbol *context;
	extern char *claimproc;

	if (!n
	|| (context && claimproc && strcmp(context->name, claimproc) == 0))
		return;

	for (l = n->sl; l; l = l->nxt)	/* find sequences of unlabeled skips */
		check_sequence(l->this);
}

Sequence *
close_seq(int nottop)
{	Sequence *s = cur_s->this;
	Symbol *z;

	if (nottop > 0 && (z = has_lab(s->frst, 0)))
	{	printf("error: (%s:%d) label %s placed incorrectly\n",
			(s->frst->n)?s->frst->n->fn->name:"-",
			(s->frst->n)?s->frst->n->ln:0,
			z->name);
		switch (nottop) {
		case 1:
			printf("=====> stmnt unless Label: stmnt\n");
			printf("sorry, cannot jump to the guard of an\n");
			printf("escape (it is not a unique state)\n");
			break;
		case 2:
			printf("=====> instead of  ");
			printf("\"Label: stmnt unless stmnt\"\n");
			printf("=====> always use  ");
			printf("\"Label: { stmnt unless stmnt }\"\n");
			break;
		case 3:
			printf("=====> instead of  ");
			printf("\"atomic { Label: statement ... }\"\n");
			printf("=====> always use  ");
			printf("\"Label: atomic { statement ... }\"\n");
			break;
		case 4:
			printf("=====> instead of  ");
			printf("\"d_step { Label: statement ... }\"\n");
			printf("=====> always use  ");
			printf("\"Label: d_step { statement ... }\"\n");
			break;
		case 5:
			printf("=====> instead of  ");
			printf("\"{ Label: statement ... }\"\n");
			printf("=====> always use  ");
			printf("\"Label: { statement ... }\"\n");
			break;
		case 6:
			printf("=====>instead of\n");
			printf("	do (or if)\n");
			printf("	:: ...\n");
			printf("	:: Label: statement\n");
			printf("	od (of fi)\n");
			printf("=====>always use\n");
			printf("Label:	do (or if)\n");
			printf("	:: ...\n");
			printf("	:: statement\n");
			printf("	od (or fi)\n");
			break;
		case 7:
			printf("cannot happen - labels\n");
			break;
		}
		alldone(1);
	}

	if (nottop == 4
	&& !Rjumpslocal(s->frst, s->last))
		fatal("non_local jump in d_step sequence", (char *) 0);

	cur_s = cur_s->nxt;
	s->maxel = Elcnt;
	s->extent = s->last;
	if (!s->last)
		fatal("sequence must have at least one statement", (char *) 0);
	return s;
}

Lextok *
do_unless(Lextok *No, Lextok *Es)
{	SeqList *Sl;
	Lextok *Re = nn(ZN, UNLESS, ZN, ZN);
	Re->ln = No->ln;
	Re->fn = No->fn;

	has_unless++;
	if (Es->ntyp == NON_ATOMIC)
		Sl = Es->sl;
	else
	{	open_seq(0); add_seq(Es);
		Sl = seqlist(close_seq(1), 0);
	}

	if (No->ntyp == NON_ATOMIC)
	{	No->sl->nxt = Sl;
		Sl = No->sl;
	} else	if (No->ntyp == ':'
		&& (No->lft->ntyp == NON_ATOMIC
		||  No->lft->ntyp == ATOMIC
		||  No->lft->ntyp == D_STEP))
	{
		int tok = No->lft->ntyp;

		No->lft->sl->nxt = Sl;
		Re->sl = No->lft->sl;

		open_seq(0); add_seq(Re);
		Re = nn(ZN, tok, ZN, ZN);
		Re->sl = seqlist(close_seq(7), 0);
		Re->ln = No->ln;
		Re->fn = No->fn;

		Re = nn(No, ':', Re, ZN);	/* lift label */
		Re->ln = No->ln;
		Re->fn = No->fn;
		return Re;
	} else
	{	open_seq(0); add_seq(No);
		Sl = seqlist(close_seq(2), Sl);
	}

	Re->sl = Sl;
	return Re;
}

SeqList *
seqlist(Sequence *s, SeqList *r)
{	SeqList *t = (SeqList *) emalloc(sizeof(SeqList));

	t->this = s;
	t->nxt = r;
	return t;
}

static Element *
new_el(Lextok *n)
{	Element *m;

	if (n)
	{	if (n->ntyp == IF || n->ntyp == DO)
			return if_seq(n);
		if (n->ntyp == UNLESS)
			return unless_seq(n);
	}
	m = (Element *) emalloc(sizeof(Element));
	m->n = n;
	m->seqno = Elcnt++;
	m->Seqno = Unique++;
	m->Nxt = Al_El; Al_El = m;
	return m;
}

static int
has_chanref(Lextok *n)
{
	if (!n) return 0;

	switch (n->ntyp) {
	case 's':	case 'r':
#if 0
	case 'R':	case LEN:
#endif
	case FULL:	case NFULL:
	case EMPTY:	case NEMPTY:
		return 1;
	default:
		break;
	}
	if (has_chanref(n->lft))
		return 1;

	return has_chanref(n->rgt);
}

void
loose_ends(void)	/* properly tie-up ends of sub-sequences */
{	Element *e, *f;

	for (e = Al_El; e; e = e->Nxt)
	{	if (!e->n
		||  !e->nxt)
			continue;
		switch (e->n->ntyp) {
		case ATOMIC:
		case NON_ATOMIC:
		case D_STEP:
			f = e->nxt;
			while (f && f->n->ntyp == '.')
				f = f->nxt;
			if (0) printf("link %d, {%d .. %d} -> %d (ntyp=%d) was %d\n",
				e->seqno,
				e->n->sl->this->frst->seqno,
				e->n->sl->this->last->seqno,
				f?f->seqno:-1, f?f->n->ntyp:-1,
				e->n->sl->this->last->nxt?e->n->sl->this->last->nxt->seqno:-1);
			if (!e->n->sl->this->last->nxt)
				e->n->sl->this->last->nxt = f;
			else
			{	if (e->n->sl->this->last->nxt->n->ntyp != GOTO)
				{	if (!f || e->n->sl->this->last->nxt->seqno != f->seqno)
					non_fatal("unexpected: loose ends", (char *)0);
				} else
					e->n->sl->this->last = e->n->sl->this->last->nxt;
				/*
				 * fix_dest can push a goto into the nxt position
				 * in that case the goto wins and f is not needed
				 * but the last fields needs adjusting
				 */
			}
			break;
	}	}
}

static Element *
if_seq(Lextok *n)
{	int	tok = n->ntyp;
	SeqList	*s  = n->sl;
	Element	*e  = new_el(ZN);
	Element	*t  = new_el(nn(ZN,'.',ZN,ZN)); /* target */
	SeqList	*z, *prev_z = (SeqList *) 0;
	SeqList *move_else  = (SeqList *) 0;	/* to end of optionlist */
	int	ref_chans = 0;

	for (z = s; z; z = z->nxt)
	{	if (!z->this->frst)
			continue;
		if (z->this->frst->n->ntyp == ELSE)
		{	if (move_else)
				fatal("duplicate `else'", (char *) 0);
			if (z->nxt)	/* is not already at the end */
			{	move_else = z;
				if (prev_z)
					prev_z->nxt = z->nxt;
				else
					s = n->sl = z->nxt;
				continue;
			}
		} else
			ref_chans |= has_chanref(z->this->frst->n);
		prev_z = z;
	}
	if (move_else)
	{	move_else->nxt = (SeqList *) 0;
		/* if there is no prev, then else was at the end */
		if (!prev_z) fatal("cannot happen - if_seq", (char *) 0);
		prev_z->nxt = move_else;
		prev_z = move_else;
	}
	if (prev_z
	&&  ref_chans
	&&  prev_z->this->frst->n->ntyp == ELSE)
	{	prev_z->this->frst->n->val = 1;
		has_badelse++;
		non_fatal("dubious use of 'else' combined with i/o,",
			(char *)0);
		nr_errs--;
	}

	e->n = nn(n, tok, ZN, ZN);