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
open_seq(int top)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
rem_Seq(void)52 rem_Seq(void)
53 {
54 DstepStart = Unique;
55 }
56
57 void
unrem_Seq(void)58 unrem_Seq(void)
59 {
60 DstepStart = -1;
61 }
62
63 static int
Rjumpslocal(Element * q,Element * stop)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
cross_dsteps(Lextok * a,Lextok * b)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
is_skip(Lextok * n)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
check_sequence(Sequence * s)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
prune_opts(Lextok * n)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 *
close_seq(int nottop)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 *
do_unless(Lextok * No,Lextok * Es)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 *
seqlist(Sequence * s,SeqList * r)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 *
new_el(Lextok * n)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
has_chanref(Lextok * n)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
loose_ends(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 *
if_seq(Lextok * n)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
escape_el(Element * f,Sequence * e)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
attach_escape(Sequence * n,Sequence * e)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 *
unless_seq(Lextok * n)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 *
mk_skip(void)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
add_el(Element * e,Sequence * s)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 *
colons(Lextok * n)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
add_seq(Lextok * n)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
show_lab(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
set_lab(Symbol * s,Element * e)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 *
get_labspec(Lextok * n)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 *
get_lab(Lextok * n,int md)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 *
has_lab(Element * e,int special)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
mov_lab(Symbol * z,Element * e,Element * y)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
fix_dest(Symbol * c,Symbol * a)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
find_lab(Symbol * s,Symbol * c,int markit)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
pushbreak(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 *
break_dest(void)755 break_dest(void)
756 {
757 if (!breakstack)
758 fatal("misplaced break statement", (char *)0);
759 return breakstack->l;
760 }
761
762 void
make_atomic(Sequence * s,int added)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
match_struct(Symbol * s,Symbol * t)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
valid_name(Lextok * a3,Lextok * a5,Lextok * a8,char * tp)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
for_setup(Lextok * a3,Lextok * a5,Lextok * a8)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 *
for_index(Lextok * a3,Lextok * a5)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 *
for_body(Lextok * a3,int with_else)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 *
sel_index(Lextok * a3,Lextok * a5,Lextok * a7)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
walk_atomic(Element * a,Element * b,int added)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
dumplabels(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 }
1070