flow.c 23 KB

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