Subversion Repositories planix.SVN

Rev

Rev 2 | Details | Compare with Previous | Last modification | View Log | RSS feed

Rev Author Line No. Line
2 - 1 
/***** spin: flow.c *****/
2 
 
3 
/* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     */
4 
/* All Rights Reserved.  This software is for educational purposes only.  */
5 
/* No guarantee whatsoever is expressed or implied by the distribution of */
6 
/* this code.  Permission is given to distribute this code provided that  */
7 
/* this introductory message is not removed and no monies are exchanged.  */
8 
/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
9 
/*             http://spinroot.com/                                       */
10 
/* Send all bug-reports and/or questions to: bugs@spinroot.com            */
11 
 
12 
#include "spin.h"
13 
#include "y.tab.h"
14 
 
15 
extern Symbol	*Fname;
16 
extern int	nr_errs, lineno, verbose, in_for;
17 
extern short	has_unless, has_badelse, has_xu;
18 
extern char CurScope[MAXSCOPESZ];
19 
 
20 
Element *Al_El = ZE;
21 
Label	*labtab = (Label *) 0;
22 
int	Unique = 0, Elcnt = 0, DstepStart = -1;
23 
int	initialization_ok = 1;
24 
 
25 
static Lbreak	*breakstack = (Lbreak *) 0;
26 
static Lextok	*innermost;
27 
static SeqList	*cur_s = (SeqList *) 0;
28 
static int	break_id=0;
29 
 
30 
static Element	*if_seq(Lextok *);
31 
static Element	*new_el(Lextok *);
32 
static Element	*unless_seq(Lextok *);
33 
static void	add_el(Element *, Sequence *);
34 
static void	attach_escape(Sequence *, Sequence *);
35 
static void	mov_lab(Symbol *, Element *, Element *);
36 
static void	walk_atomic(Element *, Element *, int);
37 
 
38 
void
39 
open_seq(int top)
40 
{	SeqList *t;
41 
	Sequence *s = (Sequence *) emalloc(sizeof(Sequence));
42 
 
43 
	t = seqlist(s, cur_s);
44 
	cur_s = t;
45 
	if (top)
46 
	{	Elcnt = 1;
47 
		initialization_ok = 1;
48 
	}
49 
}
50 
 
51 
void
52 
rem_Seq(void)
53 
{
54 
	DstepStart = Unique;
55 
}
56 
 
57 
void
58 
unrem_Seq(void)
59 
{
60 
	DstepStart = -1;
61 
}
62 
 
63 
static int
64 
Rjumpslocal(Element *q, Element *stop)
65 
{	Element *lb, *f;
66 
	SeqList *h;
67 
 
68 
	/* allow no jumps out of a d_step sequence */
69 
	for (f = q; f && f != stop; f = f->nxt)
70 
	{	if (f && f->n && f->n->ntyp == GOTO)
71 
		{	lb = get_lab(f->n, 0);
72 
			if (!lb || lb->Seqno < DstepStart)
73 
			{	lineno = f->n->ln;
74 
				Fname = f->n->fn;
75 
				return 0;
76 
		}	}
77 
		for (h = f->sub; h; h = h->nxt)
78 
		{	if (!Rjumpslocal(h->this->frst, h->this->last))
79 
				return 0;
80 
 
81 
	}	}
82 
	return 1;
83 
}
84 
 
85 
void
86 
cross_dsteps(Lextok *a, Lextok *b)
87 
{
88 
	if (a && b
89 
	&&  a->indstep != b->indstep)
90 
	{	lineno = a->ln;
91 
		Fname  = a->fn;
92 
		fatal("jump into d_step sequence", (char *) 0);
93 
	}
94 
}
95 
 
96 
int
97 
is_skip(Lextok *n)
98 
{
99 
	return (n->ntyp == PRINT
100 
	||	n->ntyp == PRINTM
101 
	||	(n->ntyp == 'c'
102 
		&& n->lft
103 
		&& n->lft->ntyp == CONST
104 
		&& n->lft->val  == 1));
105 
}
106 
 
107 
void
108 
check_sequence(Sequence *s)
109 
{	Element *e, *le = ZE;
110 
	Lextok *n;
111 
	int cnt = 0;
112 
 
113 
	for (e = s->frst; e; le = e, e = e->nxt)
114 
	{	n = e->n;
115 
		if (is_skip(n) && !has_lab(e, 0))
116 
		{	cnt++;
117 
			if (cnt > 1
118 
			&&  n->ntyp != PRINT
119 
			&&  n->ntyp != PRINTM)
120 
			{	if (verbose&32)
121 
					printf("spin: %s:%d, redundant skip\n",
122 
						n->fn->name, n->ln);
123 
				if (e != s->frst
124 
				&&  e != s->last
125 
				&&  e != s->extent)
126 
				{	e->status |= DONE;	/* not unreachable */
127 
					le->nxt = e->nxt;	/* remove it */
128 
					e = le;
129 
				}
130 
			}
131 
		} else
132 
			cnt = 0;
133 
	}
134 
}
135 
 
136 
void
137 
prune_opts(Lextok *n)
138 
{	SeqList *l;
139 
	extern Symbol *context;
140 
	extern char *claimproc;
141 
 
142 
	if (!n
143 
	|| (context && claimproc && strcmp(context->name, claimproc) == 0))
144 
		return;
145 
 
146 
	for (l = n->sl; l; l = l->nxt)	/* find sequences of unlabeled skips */
147 
		check_sequence(l->this);
148 
}
149 
 
150 
Sequence *
151 
close_seq(int nottop)
152 
{	Sequence *s = cur_s->this;
153 
	Symbol *z;
154 
 
155 
	if (nottop == 0)	/* end of proctype body */
156 
	{	initialization_ok = 1;
157 
	}
158 
 
159 
	if (nottop > 0 && (z = has_lab(s->frst, 0)))
160 
	{	printf("error: (%s:%d) label %s placed incorrectly\n",
161 
			(s->frst->n)?s->frst->n->fn->name:"-",
162 
			(s->frst->n)?s->frst->n->ln:0,
163 
			z->name);
164 
		switch (nottop) {
165 
		case 1:
166 
			printf("=====> stmnt unless Label: stmnt\n");
167 
			printf("sorry, cannot jump to the guard of an\n");
168 
			printf("escape (it is not a unique state)\n");
169 
			break;
170 
		case 2:
171 
			printf("=====> instead of  ");
172 
			printf("\"Label: stmnt unless stmnt\"\n");
173 
			printf("=====> always use  ");
174 
			printf("\"Label: { stmnt unless stmnt }\"\n");
175 
			break;
176 
		case 3:
177 
			printf("=====> instead of  ");
178 
			printf("\"atomic { Label: statement ... }\"\n");
179 
			printf("=====> always use  ");
180 
			printf("\"Label: atomic { statement ... }\"\n");
181 
			break;
182 
		case 4:
183 
			printf("=====> instead of  ");
184 
			printf("\"d_step { Label: statement ... }\"\n");
185 
			printf("=====> always use  ");
186 
			printf("\"Label: d_step { statement ... }\"\n");
187 
			break;
188 
		case 5:
189 
			printf("=====> instead of  ");
190 
			printf("\"{ Label: statement ... }\"\n");
191 
			printf("=====> always use  ");
192 
			printf("\"Label: { statement ... }\"\n");
193 
			break;
194 
		case 6:
195 
			printf("=====>instead of\n");
196 
			printf("	do (or if)\n");
197 
			printf("	:: ...\n");
198 
			printf("	:: Label: statement\n");
199 
			printf("	od (of fi)\n");
200 
			printf("=====>always use\n");
201 
			printf("Label:	do (or if)\n");
202 
			printf("	:: ...\n");
203 
			printf("	:: statement\n");
204 
			printf("	od (or fi)\n");
205 
			break;
206 
		case 7:
207 
			printf("cannot happen - labels\n");
208 
			break;
209 
		}
210 
		alldone(1);
211 
	}
212 
 
213 
	if (nottop == 4
214 
	&& !Rjumpslocal(s->frst, s->last))
215 
		fatal("non_local jump in d_step sequence", (char *) 0);
216 
 
217 
	cur_s = cur_s->nxt;
218 
	s->maxel = Elcnt;
219 
	s->extent = s->last;
220 
	if (!s->last)
221 
		fatal("sequence must have at least one statement", (char *) 0);
222 
	return s;
223 
}
224 
 
225 
Lextok *
226 
do_unless(Lextok *No, Lextok *Es)
227 
{	SeqList *Sl;
228 
	Lextok *Re = nn(ZN, UNLESS, ZN, ZN);
229 
	Re->ln = No->ln;
230 
	Re->fn = No->fn;
231 
 
232 
	has_unless++;
233 
	if (Es->ntyp == NON_ATOMIC)
234 
		Sl = Es->sl;
235 
	else
236 
	{	open_seq(0); add_seq(Es);
237 
		Sl = seqlist(close_seq(1), 0);
238 
	}
239 
 
240 
	if (No->ntyp == NON_ATOMIC)
241 
	{	No->sl->nxt = Sl;
242 
		Sl = No->sl;
243 
	} else	if (No->ntyp == ':'
244 
		&& (No->lft->ntyp == NON_ATOMIC
245 
		||  No->lft->ntyp == ATOMIC
246 
		||  No->lft->ntyp == D_STEP))
247 
	{
248 
		int tok = No->lft->ntyp;
249 
 
250 
		No->lft->sl->nxt = Sl;
251 
		Re->sl = No->lft->sl;
252 
 
253 
		open_seq(0); add_seq(Re);
254 
		Re = nn(ZN, tok, ZN, ZN);
255 
		Re->sl = seqlist(close_seq(7), 0);
256 
		Re->ln = No->ln;
257 
		Re->fn = No->fn;
258 
 
259 
		Re = nn(No, ':', Re, ZN);	/* lift label */
260 
		Re->ln = No->ln;
261 
		Re->fn = No->fn;
262 
		return Re;
263 
	} else
264 
	{	open_seq(0); add_seq(No);
265 
		Sl = seqlist(close_seq(2), Sl);
266 
	}
267 
 
268 
	Re->sl = Sl;
269 
	return Re;
270 
}
271 
 
272 
SeqList *
273 
seqlist(Sequence *s, SeqList *r)
274 
{	SeqList *t = (SeqList *) emalloc(sizeof(SeqList));
275 
 
276 
	t->this = s;
277 
	t->nxt = r;
278 
	return t;
279 
}
280 
 
281 
static Element *
282 
new_el(Lextok *n)
283 
{	Element *m;
284 
 
285 
	if (n)
286 
	{	if (n->ntyp == IF || n->ntyp == DO)
287 
			return if_seq(n);
288 
		if (n->ntyp == UNLESS)
289 
			return unless_seq(n);
290 
	}
291 
	m = (Element *) emalloc(sizeof(Element));
292 
	m->n = n;
293 
	m->seqno = Elcnt++;
294 
	m->Seqno = Unique++;
295 
	m->Nxt = Al_El; Al_El = m;
296 
	return m;
297 
}
298 
 
299 
static int
300 
has_chanref(Lextok *n)
301 
{
302 
	if (!n) return 0;
303 
 
304 
	switch (n->ntyp) {
305 
	case 's':	case 'r':
306 
#if 0
307 
	case 'R':	case LEN:
308 
#endif
309 
	case FULL:	case NFULL:
310 
	case EMPTY:	case NEMPTY:
311 
		return 1;
312 
	default:
313 
		break;
314 
	}
315 
	if (has_chanref(n->lft))
316 
		return 1;
317 
 
318 
	return has_chanref(n->rgt);
319 
}
320 
 
321 
void
322 
loose_ends(void)	/* properly tie-up ends of sub-sequences */
323 
{	Element *e, *f;
324 
 
325 
	for (e = Al_El; e; e = e->Nxt)
326 
	{	if (!e->n
327 
		||  !e->nxt)
328 
			continue;
329 
		switch (e->n->ntyp) {
330 
		case ATOMIC:
331 
		case NON_ATOMIC:
332 
		case D_STEP:
333 
			f = e->nxt;
334 
			while (f && f->n->ntyp == '.')
335 
				f = f->nxt;
336 
			if (0) printf("link %d, {%d .. %d} -> %d (ntyp=%d) was %d\n",
337 
				e->seqno,
338 
				e->n->sl->this->frst->seqno,
339 
				e->n->sl->this->last->seqno,
340 
				f?f->seqno:-1, f?f->n->ntyp:-1,
341 
				e->n->sl->this->last->nxt?e->n->sl->this->last->nxt->seqno:-1);
342 
			if (!e->n->sl->this->last->nxt)
343 
				e->n->sl->this->last->nxt = f;
344 
			else
345 
			{	if (e->n->sl->this->last->nxt->n->ntyp != GOTO)
346 
				{	if (!f || e->n->sl->this->last->nxt->seqno != f->seqno)
347 
					non_fatal("unexpected: loose ends", (char *)0);
348 
				} else
349 
					e->n->sl->this->last = e->n->sl->this->last->nxt;
350 
				/*
351 
				 * fix_dest can push a goto into the nxt position
352 
				 * in that case the goto wins and f is not needed
353 
				 * but the last fields needs adjusting
354 
				 */
355 
			}
356 
			break;
357 
	}	}
358 
}
359 
 
360 
static Element *
361 
if_seq(Lextok *n)
362 
{	int	tok = n->ntyp;
363 
	SeqList	*s  = n->sl;
364 
	Element	*e  = new_el(ZN);
365 
	Element	*t  = new_el(nn(ZN,'.',ZN,ZN)); /* target */
366 
	SeqList	*z, *prev_z = (SeqList *) 0;
367 
	SeqList *move_else  = (SeqList *) 0;	/* to end of optionlist */
368 
	int	ref_chans = 0;
369 
 
370 
	for (z = s; z; z = z->nxt)
371 
	{	if (!z->this->frst)
372 
			continue;
373 
		if (z->this->frst->n->ntyp == ELSE)
374 
		{	if (move_else)
375 
				fatal("duplicate `else'", (char *) 0);
376 
			if (z->nxt)	/* is not already at the end */
377 
			{	move_else = z;
378 
				if (prev_z)
379 
					prev_z->nxt = z->nxt;
380 
				else
381 
					s = n->sl = z->nxt;
382 
				continue;
383 
			}
384 
		} else
385 
			ref_chans |= has_chanref(z->this->frst->n);
386 
		prev_z = z;
387 
	}
388 
	if (move_else)
389 
	{	move_else->nxt = (SeqList *) 0;
390 
		/* if there is no prev, then else was at the end */
391 
		if (!prev_z) fatal("cannot happen - if_seq", (char *) 0);
392 
		prev_z->nxt = move_else;
393 
		prev_z = move_else;
394 
	}
395 
	if (prev_z
396 
	&&  ref_chans
397 
	&&  prev_z->this->frst->n->ntyp == ELSE)
398 
	{	prev_z->this->frst->n->val = 1;
399 
		has_badelse++;
400 
		if (has_xu)
401 
		{	fatal("invalid use of 'else' combined with i/o and xr/xs assertions,",
402 
				(char *)0);
403 
		} else
404 
		{	non_fatal("dubious use of 'else' combined with i/o,",
405 
				(char *)0);
406 
		}
407 
		nr_errs--;
408 
	}
409 
 
410 
	e->n = nn(n, tok, ZN, ZN);
411 
	e->n->sl = s;			/* preserve as info only */
412 
	e->sub = s;
413 
	for (z = s; z; prev_z = z, z = z->nxt)
414 
		add_el(t, z->this);	/* append target */
415 
	if (tok == DO)
416 
	{	add_el(t, cur_s->this); /* target upfront */
417 
		t = new_el(nn(n, BREAK, ZN, ZN)); /* break target */
418 
		set_lab(break_dest(), t);	/* new exit  */
419 
		breakstack = breakstack->nxt;	/* pop stack */
420 
	}
421 
	add_el(e, cur_s->this);
422 
	add_el(t, cur_s->this);
423 
	return e;			/* destination node for label */
424 
}
425 
 
426 
static void
427 
escape_el(Element *f, Sequence *e)
428 
{	SeqList *z;
429 
 
430 
	for (z = f->esc; z; z = z->nxt)
431 
		if (z->this == e)
432 
			return;	/* already there */
433 
 
434 
	/* cover the lower-level escapes of this state */
435 
	for (z = f->esc; z; z = z->nxt)
436 
		attach_escape(z->this, e);
437 
 
438 
	/* now attach escape to the state itself */
439 
 
440 
	f->esc = seqlist(e, f->esc);	/* in lifo order... */
441 
#ifdef DEBUG
442 
	printf("attach %d (", e->frst->Seqno);
443 
	comment(stdout, e->frst->n, 0);
444 
	printf(")	to %d (", f->Seqno);
445 
	comment(stdout, f->n, 0);
446 
	printf(")\n");
447 
#endif
448 
	switch (f->n->ntyp) {
449 
	case UNLESS:
450 
		attach_escape(f->sub->this, e);
451 
		break;
452 
	case IF:
453 
	case DO:
454 
		for (z = f->sub; z; z = z->nxt)
455 
			attach_escape(z->this, e);
456 
		break;
457 
	case D_STEP:
458 
		/* attach only to the guard stmnt */
459 
		escape_el(f->n->sl->this->frst, e);
460 
		break;
461 
	case ATOMIC:
462 
	case NON_ATOMIC:
463 
		/* attach to all stmnts */
464 
		attach_escape(f->n->sl->this, e);
465 
		break;
466 
	}
467 
}
468 
 
469 
static void
470 
attach_escape(Sequence *n, Sequence *e)
471 
{	Element *f;
472 
 
473 
	for (f = n->frst; f; f = f->nxt)
474 
	{	escape_el(f, e);
475 
		if (f == n->extent)
476 
			break;
477 
	}
478 
}
479 
 
480 
static Element *
481 
unless_seq(Lextok *n)
482 
{	SeqList	*s  = n->sl;
483 
	Element	*e  = new_el(ZN);
484 
	Element	*t  = new_el(nn(ZN,'.',ZN,ZN)); /* target */
485 
	SeqList	*z;
486 
 
487 
	e->n = nn(n, UNLESS, ZN, ZN);
488 
	e->n->sl = s;			/* info only */
489 
	e->sub = s;
490 
 
491 
	/* need 2 sequences: normal execution and escape */
492 
	if (!s || !s->nxt || s->nxt->nxt)
493 
		fatal("unexpected unless structure", (char *)0);
494 
 
495 
	/* append the target state to both */
496 
	for (z = s; z; z = z->nxt)
497 
		add_el(t, z->this);
498 
 
499 
	/* attach escapes to all states in normal sequence */
500 
	attach_escape(s->this, s->nxt->this);
501 
 
502 
	add_el(e, cur_s->this);
503 
	add_el(t, cur_s->this);
504 
#ifdef DEBUG
505 
	printf("unless element (%d,%d):\n", e->Seqno, t->Seqno);
506 
	for (z = s; z; z = z->nxt)
507 
	{	Element *x; printf("\t%d,%d,%d :: ",
508 
		z->this->frst->Seqno,
509 
		z->this->extent->Seqno,
510 
		z->this->last->Seqno);
511 
		for (x = z->this->frst; x; x = x->nxt)
512 
			printf("(%d)", x->Seqno);
513 
		printf("\n");
514 
	}
515 
#endif
516 
	return e;
517 
}
518 
 
519 
Element *
520 
mk_skip(void)
521 
{	Lextok  *t = nn(ZN, CONST, ZN, ZN);
522 
	t->val = 1;
523 
	return new_el(nn(ZN, 'c', t, ZN));
524 
}
525 
 
526 
static void
527 
add_el(Element *e, Sequence *s)
528 
{
529 
	if (e->n->ntyp == GOTO)
530 
	{	Symbol *z = has_lab(e, (1|2|4));
531 
		if (z)
532 
		{	Element *y; /* insert a skip */
533 
			y = mk_skip();
534 
			mov_lab(z, e, y); /* inherit label */
535 
			add_el(y, s);
536 
	}	}
537 
#ifdef DEBUG
538 
	printf("add_el %d after %d -- ",
539 
	e->Seqno, (s->last)?s->last->Seqno:-1);
540 
	comment(stdout, e->n, 0);
541 
	printf("\n");
542 
#endif
543 
	if (!s->frst)
544 
		s->frst = e;
545 
	else
546 
		s->last->nxt = e;
547 
	s->last = e;
548 
}
549 
 
550 
static Element *
551 
colons(Lextok *n)
552 
{
553 
	if (!n)
554 
		return ZE;
555 
	if (n->ntyp == ':')
556 
	{	Element *e = colons(n->lft);
557 
		set_lab(n->sym, e);
558 
		return e;
559 
	}
560 
	innermost = n;
561 
	return new_el(n);
562 
}
563 
 
564 
void
565 
add_seq(Lextok *n)
566 
{	Element *e;
567 
 
568 
	if (!n) return;
569 
	innermost = n;
570 
	e = colons(n);
571 
	if (innermost->ntyp != IF
572 
	&&  innermost->ntyp != DO
573 
	&&  innermost->ntyp != UNLESS)
574 
		add_el(e, cur_s->this);
575 
}
576 
 
577 
void
578 
show_lab(void)
579 
{	Label *l;
580 
	for (l = labtab; l; l = l->nxt)
581 
		printf("label %s\n", l->s->name);
582 
}
583 
 
584 
void
585 
set_lab(Symbol *s, Element *e)
586 
{	Label *l; extern Symbol *context;
587 
	int cur_uiid = is_inline();
588 
 
589 
	if (!s) return;
590 
 
591 
	for (l = labtab; l; l = l->nxt)
592 
	{	if (strcmp(l->s->name, s->name) == 0
593 
		&&  l->c == context
594 
		&&  l->uiid == cur_uiid)
595 
		{	non_fatal("label %s redeclared", s->name);
596 
			break;
597 
	}	}
598 
 
599 
	l = (Label *) emalloc(sizeof(Label));
600 
	l->s = s;
601 
	l->c = context;
602 
	l->e = e;
603 
	l->uiid = cur_uiid;
604 
	l->nxt = labtab;
605 
	labtab = l;
606 
}
607 
 
608 
static Label *
609 
get_labspec(Lextok *n)
610 
{	Symbol *s = n->sym;
611 
	Label *l, *anymatch = (Label *) 0;
612 
	int cur_uiid = n->uiid;
613 
	/*
614 
	 * try to find a label with the same uiid
615 
	 * but if it doesn't exist, return any other
616 
	 * that is defined within the same scope
617 
	 */
618 
	for (l = labtab; l; l = l->nxt)
619 
	{	if (strcmp(s->name, l->s->name) == 0
620 
		&&  s->context == l->s->context)
621 
		{	anymatch = l;
622 
			if (cur_uiid == l->uiid) /* best match */
623 
			{	return l;
624 
	}	}	}
625 
 
626 
	return anymatch; /* likely to be 0 */
627 
}
628 
 
629 
Element *
630 
get_lab(Lextok *n, int md)
631 
{	Label *l = get_labspec(n);
632 
 
633 
	if (l != (Label *) 0)
634 
	{	return (l->e);
635 
	}
636 
 
637 
	if (md)
638 
	{	lineno = n->ln;
639 
		Fname  = n->fn;
640 
		fatal("undefined label %s", n->sym->name);
641 
	}
642 
 
643 
	return ZE;
644 
}
645 
 
646 
Symbol *
647 
has_lab(Element *e, int special)
648 
{	Label *l;
649 
 
650 
	for (l = labtab; l; l = l->nxt)
651 
	{	if (e != l->e)
652 
			continue;
653 
		if (special == 0
654 
		||  ((special&1) && !strncmp(l->s->name, "accept", 6))
655 
		||  ((special&2) && !strncmp(l->s->name, "end", 3))
656 
		||  ((special&4) && !strncmp(l->s->name, "progress", 8)))
657 
			return (l->s);
658 
	}
659 
	return ZS;
660 
}
661 
 
662 
static void
663 
mov_lab(Symbol *z, Element *e, Element *y)
664 
{	Label *l;
665 
 
666 
	for (l = labtab; l; l = l->nxt)
667 
		if (e == l->e)
668 
		{	l->e = y;
669 
			return;
670 
		}
671 
	if (e->n)
672 
	{	lineno = e->n->ln;
673 
		Fname  = e->n->fn;
674 
	}
675 
	fatal("cannot happen - mov_lab %s", z->name);
676 
}
677 
 
678 
void
679 
fix_dest(Symbol *c, Symbol *a)		/* c:label name, a:proctype name */
680 
{	Label *l; extern Symbol *context;
681 
 
682 
#if 0
683 
	printf("ref to label '%s' in proctype '%s', search:\n",
684 
		c->name, a->name);
685 
	for (l = labtab; l; l = l->nxt)
686 
		printf("	%s in	%s\n", l->s->name, l->c->name);
687 
#endif
688 
 
689 
	for (l = labtab; l; l = l->nxt)
690 
	{	if (strcmp(c->name, l->s->name) == 0
691 
		&&  strcmp(a->name, l->c->name) == 0)	/* ? */
692 
			break;
693 
	}
694 
	if (!l)
695 
	{	printf("spin: label '%s' (proctype %s)\n", c->name, a->name);
696 
		non_fatal("unknown label '%s'", c->name);
697 
		if (context == a)
698 
		printf("spin: cannot remote ref a label inside the same proctype\n");
699 
		return;
700 
	}
701 
	if (!l->e || !l->e->n)
702 
		fatal("fix_dest error (%s)", c->name);
703 
	if (l->e->n->ntyp == GOTO)
704 
	{	Element	*y = (Element *) emalloc(sizeof(Element));
705 
		int	keep_ln = l->e->n->ln;
706 
		Symbol	*keep_fn = l->e->n->fn;
707 
 
708 
		/* insert skip - or target is optimized away */
709 
		y->n = l->e->n;		  /* copy of the goto   */
710 
		y->seqno = find_maxel(a); /* unique seqno within proc */
711 
		y->nxt = l->e->nxt;
712 
		y->Seqno = Unique++; y->Nxt = Al_El; Al_El = y;
713 
 
714 
		/* turn the original element+seqno into a skip */
715 
		l->e->n = nn(ZN, 'c', nn(ZN, CONST, ZN, ZN), ZN);
716 
		l->e->n->ln = l->e->n->lft->ln = keep_ln;
717 
		l->e->n->fn = l->e->n->lft->fn = keep_fn;
718 
		l->e->n->lft->val = 1;
719 
		l->e->nxt = y;		/* append the goto  */
720 
	}
721 
	l->e->status |= CHECK2;	/* treat as if global */
722 
	if (l->e->status & (ATOM | L_ATOM | D_ATOM))
723 
	{	non_fatal("cannot reference label inside atomic or d_step (%s)",
724 
			c->name);
725 
	}
726 
}
727 
 
728 
int
729 
find_lab(Symbol *s, Symbol *c, int markit)
730 
{	Label *l;
731 
 
732 
	for (l = labtab; l; l = l->nxt)
733 
	{	if (strcmp(s->name, l->s->name) == 0
734 
		&&  strcmp(c->name, l->c->name) == 0)
735 
		{	l->visible |= markit;
736 
			return (l->e->seqno);
737 
	}	}
738 
	return 0;
739 
}
740 
 
741 
void
742 
pushbreak(void)
743 
{	Lbreak *r = (Lbreak *) emalloc(sizeof(Lbreak));
744 
	Symbol *l;
745 
	char buf[64];
746 
 
747 
	sprintf(buf, ":b%d", break_id++);
748 
	l = lookup(buf);
749 
	r->l = l;
750 
	r->nxt = breakstack;
751 
	breakstack = r;
752 
}
753 
 
754 
Symbol *
755 
break_dest(void)
756 
{
757 
	if (!breakstack)
758 
		fatal("misplaced break statement", (char *)0);
759 
	return breakstack->l;
760 
}
761 
 
762 
void
763 
make_atomic(Sequence *s, int added)
764 
{	Element *f;
765 
 
766 
	walk_atomic(s->frst, s->last, added);
767 
 
768 
	f = s->last;
769 
	switch (f->n->ntyp) {	/* is last step basic stmnt or sequence ? */
770 
	case NON_ATOMIC:
771 
	case ATOMIC:
772 
		/* redo and search for the last step of that sequence */
773 
		make_atomic(f->n->sl->this, added);
774 
		break;
775 
 
776 
	case UNLESS:
777 
		/* escapes are folded into main sequence */
778 
		make_atomic(f->sub->this, added);
779 
		break;
780 
 
781 
	default:
782 
		f->status &= ~ATOM;
783 
		f->status |= L_ATOM;
784 
		break;
785 
	}
786 
}
787 
 
788 
#if 0
789 
static int depth = 0;
790 
void dump_sym(Symbol *, char *);
791 
 
792 
void
793 
dump_lex(Lextok *t, char *s)
794 
{	int i;
795 
 
796 
	depth++;
797 
	printf(s);
798 
	for (i = 0; i < depth; i++)
799 
		printf("\t");
800 
	explain(t->ntyp);
801 
	if (t->ntyp == NAME) printf(" %s ", t->sym->name);
802 
	if (t->ntyp == CONST) printf(" %d ", t->val);
803 
	if (t->ntyp == STRUCT)
804 
	{	dump_sym(t->sym, "\n:Z:");
805 
	}
806 
	if (t->lft)
807 
	{	dump_lex(t->lft, "\nL");
808 
	}
809 
	if (t->rgt)
810 
	{	dump_lex(t->rgt, "\nR");
811 
	}
812 
	depth--;
813 
}
814 
void
815 
dump_sym(Symbol *z, char *s)
816 
{	int i;
817 
	char txt[64];
818 
	depth++;
819 
	printf(s);
820 
	for (i = 0; i < depth; i++)
821 
		printf("\t");
822 
 
823 
	if (z->type == CHAN)
824 
	{	if (z->ini && z->ini->rgt && z->ini->rgt->sym)
825 
		{	// dump_sym(z->ini->rgt->sym, "\n:I:"); /* could also be longer list */
826 
			if (z->ini->rgt->rgt
827 
			|| !z->ini->rgt->sym)
828 
			fatal("chan %s in for should have only one field (a typedef)", z->name);
829 
			printf(" -- %s %p -- ", z->ini->rgt->sym->name, z->ini->rgt->sym);
830 
		}
831 
	} else if (z->type == STRUCT)
832 
	{	if (z->Snm)
833 
			printf(" == %s %p == ", z->Snm->name, z->Snm);
834 
		else
835 
		{	if (z->Slst)
836 
				dump_lex(z->Slst, "\n:X:");
837 
			if (z->ini)
838 
				dump_lex(z->ini, "\n:I:");
839 
		}
840 
	}
841 
	depth--;
842 
 
843 
}
844 
#endif
845 
 
846 
int
847 
match_struct(Symbol *s, Symbol *t)
848 
{
849 
	if (!t
850 
	||  !t->ini
851 
	||  !t->ini->rgt
852 
	||  !t->ini->rgt->sym
853 
	||   t->ini->rgt->rgt)
854 
	{	fatal("chan %s in for should have only one field (a typedef)", t->name);
855 
	}
856 
	/* we already know that s is a STRUCT */
857 
	if (0)
858 
	{	printf("index type %s %p ==\n", s->Snm->name, s->Snm);
859 
		printf("chan type  %s %p --\n\n", t->ini->rgt->sym->name, t->ini->rgt->sym);
860 
	}
861 
 
862 
	return (s->Snm == t->ini->rgt->sym);
863 
}
864 
 
865 
void
866 
valid_name(Lextok *a3, Lextok *a5, Lextok *a8, char *tp)
867 
{
868 
	if (a3->ntyp != NAME)
869 
	{	fatal("%s ( .name : from .. to ) { ... }", tp);
870 
	}
871 
	if (a3->sym->type == CHAN
872 
	||  a3->sym->type == STRUCT
873 
	||  a3->sym->isarray != 0)
874 
	{	fatal("bad index in for-construct %s", a3->sym->name);
875 
	}
876 
	if (a5->ntyp == CONST && a8->ntyp == CONST && a5->val > a8->val)
877 
	{	non_fatal("start value for %s exceeds end-value", a3->sym->name);
878 
	}
879 
}
880 
 
881 
void
882 
for_setup(Lextok *a3, Lextok *a5, Lextok *a8)
883 
{	/* for ( a3 : a5 .. a8 ) */
884 
 
885 
	valid_name(a3, a5, a8, "for");
886 
	/* a5->ntyp = a8->ntyp = CONST; */
887 
	add_seq(nn(a3, ASGN, a3, a5));	/* start value */
888 
	open_seq(0);
889 
	add_seq(nn(ZN, 'c', nn(a3, LE, a3, a8), ZN));	/* condition */
890 
}
891 
 
892 
Lextok *
893 
for_index(Lextok *a3, Lextok *a5)
894 
{	Lextok *z0, *z1, *z2, *z3;
895 
	Symbol *tmp_cnt;
896 
	char tmp_nm[MAXSCOPESZ];
897 
	/* for ( a3 in a5 ) { ... } */
898 
 
899 
	if (a3->ntyp != NAME)
900 
	{	fatal("for ( .name in name ) { ... }", (char *) 0);
901 
	}
902 
 
903 
	if (a5->ntyp != NAME)
904 
	{	fatal("for ( %s in .name ) { ... }", a3->sym->name);
905 
	}
906 
 
907 
	if (a3->sym->type == STRUCT)
908 
	{	if (a5->sym->type != CHAN)
909 
		{	fatal("for ( %s in .channel_name ) { ... }",
910 
				a3->sym->name);
911 
		}
912 
		z0 = a5->sym->ini;
913 
		if (!z0
914 
		|| z0->val <= 0
915 
		|| z0->rgt->ntyp != STRUCT
916 
		|| z0->rgt->rgt != NULL)
917 
		{	fatal("bad channel type %s in for", a5->sym->name);
918 
		}
919 
 
920 
		if (!match_struct(a3->sym, a5->sym))
921 
		{	fatal("type of %s does not match chan", a3->sym->name);
922 
		}
923 
 
924 
		z1 = nn(ZN, CONST, ZN, ZN); z1->val = 0;
925 
		z2 = nn(a5, LEN, a5, ZN);
926 
 
927 
		sprintf(tmp_nm, "_f0r_t3mp%s", CurScope); /* make sure it's unique */
928 
		tmp_cnt = lookup(tmp_nm);
929 
		if (z0->val > 255)			/* check nr of slots, i.e. max length */
930 
		{	tmp_cnt->type = SHORT;	/* should be rare */
931 
		} else
932 
		{	tmp_cnt->type = BYTE;
933 
		}
934 
		z3 = nn(ZN, NAME, ZN, ZN);
935 
		z3->sym = tmp_cnt;
936 
 
937 
		add_seq(nn(z3, ASGN, z3, z1));	/* start value 0 */
938 
 
939 
		open_seq(0);
940 
 
941 
		add_seq(nn(ZN, 'c', nn(z3, LT, z3, z2), ZN));	/* condition */
942 
 
943 
		/* retrieve  message from the right slot -- for now: rotate contents */
944 
		in_for = 0;
945 
		add_seq(nn(a5, 'r', a5, expand(a3, 1)));	/* receive */
946 
		add_seq(nn(a5, 's', a5, expand(a3, 1)));	/* put back in to rotate */
947 
		in_for = 1;
948 
		return z3;
949 
	} else
950 
	{	if (a5->sym->isarray == 0
951 
		||  a5->sym->nel <= 0)
952 
		{	fatal("bad arrayname %s", a5->sym->name);
953 
		}
954 
		z1 = nn(ZN, CONST, ZN, ZN); z1->val = 0;
955 
		z2 = nn(ZN, CONST, ZN, ZN); z2->val = a5->sym->nel - 1;
956 
		for_setup(a3, z1, z2);
957 
		return a3;
958 
	}
959 
}
960 
 
961 
Lextok *
962 
for_body(Lextok *a3, int with_else)
963 
{	Lextok *t1, *t2, *t0, *rv;
964 
 
965 
	rv = nn(ZN, CONST, ZN, ZN); rv->val = 1;
966 
	rv = nn(ZN,  '+', a3, rv);
967 
	rv = nn(a3, ASGN, a3, rv);
968 
	add_seq(rv);	/* initial increment */
969 
 
970 
	pushbreak();
971 
 
972 
	/* completed loop body, main sequence */
973 
	t1 = nn(ZN, 0, ZN, ZN);
974 
	t1->sq = close_seq(8);
975 
 
976 
	open_seq(0);		/* add else -> break sequence */
977 
	if (with_else)
978 
	{	add_seq(nn(ZN, ELSE, ZN, ZN));
979 
	}
980 
	t2 = nn(ZN, GOTO, ZN, ZN);
981 
	t2->sym = break_dest();
982 
	add_seq(t2);
983 
	t2 = nn(ZN, 0, ZN, ZN);
984 
	t2->sq = close_seq(9);
985 
 
986 
	t0 = nn(ZN, 0, ZN, ZN);
987 
	t0->sl = seqlist(t2->sq, seqlist(t1->sq, 0));
988 
 
989 
	rv = nn(ZN, DO, ZN, ZN);
990 
	rv->sl = t0->sl;
991 
	return rv;
992 
}
993 
 
994 
Lextok *
995 
sel_index(Lextok *a3, Lextok *a5, Lextok *a7)
996 
{	/* select ( a3 : a5 .. a7 ) */
997 
 
998 
	valid_name(a3, a5, a7, "select");
999 
	/* a5->ntyp = a7->ntyp = CONST; */
1000 
 
1001 
	add_seq(nn(a3, ASGN, a3, a5));	/* start value */
1002 
	open_seq(0);
1003 
	add_seq(nn(ZN, 'c', nn(a3, LT, a3, a7), ZN));	/* condition */
1004 
 
1005 
	return for_body(a3, 0);	/* no else, just a non-deterministic break */
1006 
}
1007 
 
1008 
static void
1009 
walk_atomic(Element *a, Element *b, int added)
1010 
{	Element *f; Symbol *ofn; int oln;
1011 
	SeqList *h;
1012 
 
1013 
	ofn = Fname;
1014 
	oln = lineno;
1015 
	for (f = a; ; f = f->nxt)
1016 
	{	f->status |= (ATOM|added);
1017 
		switch (f->n->ntyp) {
1018 
		case ATOMIC:
1019 
			if (verbose&32)
1020 
			  printf("spin: warning, %s:%d, atomic inside %s (ignored)\n",
1021 
			  f->n->fn->name, f->n->ln, (added)?"d_step":"atomic");
1022 
			goto mknonat;
1023 
		case D_STEP:
1024 
			if (!(verbose&32))
1025 
			{	if (added) goto mknonat;
1026 
				break;
1027 
			}
1028 
			printf("spin: warning, %s:%d, d_step inside ",
1029 
			 f->n->fn->name, f->n->ln);
1030 
			if (added)
1031 
			{	printf("d_step (ignored)\n");
1032 
				goto mknonat;
1033 
			}
1034 
			printf("atomic\n");
1035 
			break;
1036 
		case NON_ATOMIC:
1037 
mknonat:		f->n->ntyp = NON_ATOMIC; /* can jump here */
1038 
			h = f->n->sl;
1039 
			walk_atomic(h->this->frst, h->this->last, added);
1040 
			break;
1041 
		case UNLESS:
1042 
			if (added)
1043 
			{ printf("spin: error, %s:%d, unless in d_step (ignored)\n",
1044 
			 	 f->n->fn->name, f->n->ln);
1045 
			}
1046 
		}
1047 
		for (h = f->sub; h; h = h->nxt)
1048 
			walk_atomic(h->this->frst, h->this->last, added);
1049 
		if (f == b)
1050 
			break;
1051 
	}
1052 
	Fname = ofn;
1053 
	lineno = oln;
1054 
}
1055 
 
1056 
void
1057 
dumplabels(void)
1058 
{	Label *l;
1059 
 
1060 
	for (l = labtab; l; l = l->nxt)
1061 
		if (l->c != 0 && l->s->name[0] != ':')
1062 
		{	printf("label	%s	%d	",
1063 
				l->s->name, l->e->seqno);
1064 
			if (l->uiid == 0)
1065 
				printf("<%s>\n", l->c->name);
1066 
			else
1067 
				printf("<%s i%d>\n", l->c->name, l->uiid);
1068 
		}
1069 
}