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

/* Copyright (c) 1991 by AT&T Bell Telephone Laboratories, Inc.
 * All Rights Reserved. This software is for educational purposes only.
 * No part of this source code may be reproduced in any form
 * without explicit written permission from the copyright owner.
 * This software was written by Gerard J. Holzmann, as part of the book
 * ``Design and Validation of Computer Protocols,'' ISBN 0-13-539925-4,
 * Prentice Hall, Englewood Cliffs, NJ, 07632.
 * Send bug-reports to: gerard@research.att.com
 */

#include "spin.h"
#include "y.tab.h"

Label	*labtab = (Label *) 0;
Lbreak	*breakstack = (Lbreak *) 0;
SeqList	*cur_s = (SeqList *) 0;
int	Elcnt, break_id=0;

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

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

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

	if (s->frst == s->last)
	{	if ((z = has_lab(s->frst))
		&& (strncmp(z->name, "progress", 8) == 0
		||  strncmp(z->name, "accept", 6) == 0
		||  strncmp(z->name, "end", 3) == 0))
		{	Element *y =	/* insert a skip */
			new_el(nn((Symbol *)0, s->frst->n->nval, 'c',
				nn((Symbol *)0, 1, CONST, (Node *)0,
				(Node *)0), (Node *)0));
			if (s->frst->n->ntyp == GOTO
			||  s->frst->n->ntyp == BREAK)
			{	s->frst = y;
				y->nxt = s->last;
			} else
			{	mov_lab(z, s->frst, y);
				s->frst->nxt = y;
				s->last = y;
	}	}	}
	cur_s = cur_s->nxt;
	return s;
}

SeqList *
seqlist(s, r)
	Sequence *s;
	SeqList *r;
{
	SeqList *t = (SeqList *) emalloc(sizeof(SeqList));
	t->this = s;
	t->nxt = r;
	return t;
}

Element *
new_el(n)
	Node *n;
{
	Element *m;

	if (n && (n->ntyp == IF || n->ntyp == DO))
		return if_seq(n->seql, n->ntyp, n->nval);
	m = (Element *) emalloc(sizeof(Element));
	m->n = n;
	m->seqno = Elcnt++;
	return m;
}

Element *
if_seq(s, tok, lnno)
	SeqList *s;
{
	Element *e = new_el((Node *) 0);
	Element *t = new_el(nn((Symbol *) 0, lnno, '.', 
			(Node *)0, (Node *)0)); /* target */
	SeqList *z;

	e->n = nn((Symbol *)0, lnno, tok, (Node *)0, (Node *)0);
	e->sub = s;
	for (z = s; z; z = z->nxt)
		add_el(t, z->this);
	if (tok == DO)
	{	add_el(t, cur_s->this);
		t = new_el(nn((Symbol *)0, lnno, BREAK, (Node *)0, (Node *)0));
		set_lab(break_dest(), t);
		breakstack = breakstack->nxt;	/* pop stack */
	}
	add_el(e, cur_s->this);
	add_el(t, cur_s->this);
	return e;	/* destination node for label */
}

void
add_el(e, s)
	Element *e;
	Sequence *s;
{
	if (e->n->ntyp == GOTO)
	{	Symbol *z;
		if ((z = has_lab(e))
		&& (strncmp(z->name, "progress", 8) == 0
		||  strncmp(z->name, "accept", 6) == 0
		||  strncmp(z->name, "end", 3) == 0))
		{	Element *y =	/* insert a skip */
			new_el(nn((Symbol *)0, e->n->nval, 'c',
				nn((Symbol *)0, 1, CONST, (Node *)0,
					(Node *)0), (Node *)0));
			mov_lab(z, e, y); /* gets its label */
			add_el(y, s);
	}	}
	if (!s->frst)
		s->frst = e;
	else
		s->last->nxt = e;
	s->last = e;
}

Node	*innermost;

Element *
colons(n)
	Node *n;
{
	if (!n)
		return (Element *) 0;
	if (n->ntyp == ':')
	{	Element *e = colons(n->lft);
		set_lab(n->nsym, e);
		return e;
	}
	innermost = n;
	return new_el(n);
}

void
add_seq(n)
	Node *n;
{
	Element *e;
	if (!n) return;
	innermost = n;
	e = colons(n);
	if (innermost->ntyp != IF && innermost->ntyp != DO)
		add_el(e, cur_s->this);
}


void
set_lab(s, e)
	Symbol *s;
	Element *e;
{
	Label *l; extern Symbol *context;
	if (!s) return;
	l = (Label *) emalloc(sizeof(Label));
	l->s = s;
	l->c = context;
	l->e = e;
	l->nxt = labtab;
	labtab = l;
}

Element *
get_lab(s)
	Symbol *s;
{
	Label *l;
	for (l = labtab; l; l = l->nxt)
		if (s == l->s)
			return (l->e);
	fatal("undefined label %s", s->name);
}

Symbol *
has_lab(e)
	Element *e;
{
	Label *l;
	for (l = labtab; l; l = l->nxt)
		if (e == l->e)
			return (l->s);
	return (Symbol *) 0;
}

void
mov_lab(z, e, y)
	Symbol *z;
	Element *e, *y;
{
	Label *l;
	for (l = labtab; l; l = l->nxt)
		if (e == l->e)
		{	l->e = y;
			return;
		}
	fatal("cannot happen - mov_lab %s", z->name);
}

find_lab(s, c)
	Symbol *s, *c;
{
	Label *l;
	for (l = labtab; l; l = l->nxt)
	{	if (strcmp(s->name, l->s->name) == 0
		&&  strcmp(c->name, l->c->name) == 0)
			return (l->e->seqno);
	}
	return 0;
}

void
pushbreak()
{	Lbreak *r = (Lbreak *) emalloc(sizeof(Lbreak));
	Symbol *l;
	char buf[32];

	sprintf(buf, ":b%d", break_id++);
	l = lookup(buf);
	r->l = l;
	r->nxt = breakstack;
	breakstack = r;
}

Symbol *
break_dest()
{	if (!breakstack)
		fatal("misplaced break statement", (char *)0);
	return breakstack->l;
}

void
make_atomic(s)
	Sequence *s;
{
	walk_atomic(s->frst, s->last);
	s->last->status &= ~ATOM;
	s->last->status |= L_ATOM;
}

void
walk_atomic(a, b)
	Element *a, *b;
{
	Element *f;
	SeqList *h;
	for (f = a; ; f = f->nxt)
	{	f->status |= ATOM;
		for (h = f->sub; h; h = h->nxt)
			walk_atomic(h->this->frst, h->this->last);
		if (f == b)
			break;
	}
}