pangen4.c 8.4 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360
  1. /*
  2. * This file is part of the UCB release of Plan 9. It is subject to the license
  3. * terms in the LICENSE file found in the top-level directory of this
  4. * distribution and at http://akaros.cs.berkeley.edu/files/Plan9License. No
  5. * part of the UCB release of Plan 9, including this file, may be copied,
  6. * modified, propagated, or distributed except according to the terms contained
  7. * in the LICENSE file.
  8. */
  9. /***** spin: pangen4.c *****/
  10. /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
  11. /* All Rights Reserved. This software is for educational purposes only. */
  12. /* No guarantee whatsoever is expressed or implied by the distribution of */
  13. /* this code. Permission is given to distribute this code provided that */
  14. /* this introductory message is not removed and no monies are exchanged. */
  15. /* Software written by Gerard J. Holzmann. For tool documentation see: */
  16. /* http://spinroot.com/ */
  17. /* Send all bug-reports and/or questions to: bugs@spinroot.com */
  18. #include "spin.h"
  19. #include "y.tab.h"
  20. extern FILE *tc, *tb;
  21. extern Queue *qtab;
  22. extern Symbol *Fname;
  23. extern int lineno, m_loss, Pid, eventmapnr, multi_oval;
  24. extern int16_t nocast, has_provided, has_sorted;
  25. extern char *R13[], *R14[], *R15[];
  26. static void check_proc(Lextok *, int);
  27. void
  28. undostmnt(Lextok *now, int m)
  29. { Lextok *v;
  30. int i, j;
  31. if (!now)
  32. { fprintf(tb, "0");
  33. return;
  34. }
  35. lineno = now->ln;
  36. Fname = now->fn;
  37. switch (now->ntyp) {
  38. case CONST: case '!': case UMIN:
  39. case '~': case '/': case '*':
  40. case '-': case '+': case '%':
  41. case LT: case GT: case '&':
  42. case '|': case LE: case GE:
  43. case NE: case EQ: case OR:
  44. case AND: case LSHIFT: case RSHIFT:
  45. case TIMEOUT: case LEN: case NAME:
  46. case FULL: case EMPTY: case 'R':
  47. case NFULL: case NEMPTY: case ENABLED:
  48. case '?': case PC_VAL: case '^':
  49. case C_EXPR:
  50. case NONPROGRESS:
  51. putstmnt(tb, now, m);
  52. break;
  53. case RUN:
  54. fprintf(tb, "delproc(0, now._nr_pr-1)");
  55. break;
  56. case 's':
  57. if (Pid == eventmapnr) break;
  58. if (m_loss)
  59. fprintf(tb, "if (_m == 2) ");
  60. putname(tb, "_m = unsend(", now->lft, m, ")");
  61. break;
  62. case 'r':
  63. if (Pid == eventmapnr) break;
  64. for (v = now->rgt, i=j=0; v; v = v->rgt, i++)
  65. if (v->lft->ntyp != CONST
  66. && v->lft->ntyp != EVAL)
  67. j++;
  68. if (j == 0 && now->val >= 2)
  69. break; /* poll without side-effect */
  70. { int ii = 0, jj;
  71. for (v = now->rgt; v; v = v->rgt)
  72. if ((v->lft->ntyp != CONST
  73. && v->lft->ntyp != EVAL))
  74. ii++; /* nr of things bupped */
  75. if (now->val == 1)
  76. { ii++;
  77. jj = multi_oval - ii - 1;
  78. fprintf(tb, "XX = trpt->bup.oval");
  79. if (multi_oval > 0)
  80. { fprintf(tb, "s[%d]", jj);
  81. jj++;
  82. }
  83. fprintf(tb, ";\n\t\t");
  84. } else
  85. { fprintf(tb, "XX = 1;\n\t\t");
  86. jj = multi_oval - ii - 1;
  87. }
  88. if (now->val < 2) /* not for channel poll */
  89. for (v = now->rgt, i = 0; v; v = v->rgt, i++)
  90. { switch(v->lft->ntyp) {
  91. case CONST:
  92. case EVAL:
  93. fprintf(tb, "unrecv");
  94. putname(tb, "(", now->lft, m, ", XX-1, ");
  95. fprintf(tb, "%d, ", i);
  96. if (v->lft->ntyp == EVAL)
  97. undostmnt(v->lft->lft, m);
  98. else
  99. undostmnt(v->lft, m);
  100. fprintf(tb, ", %d);\n\t\t", (i==0)?1:0);
  101. break;
  102. default:
  103. fprintf(tb, "unrecv");
  104. putname(tb, "(", now->lft, m, ", XX-1, ");
  105. fprintf(tb, "%d, ", i);
  106. if (v->lft->sym
  107. && !strcmp(v->lft->sym->name, "_"))
  108. { fprintf(tb, "trpt->bup.oval");
  109. if (multi_oval > 0)
  110. fprintf(tb, "s[%d]", jj);
  111. } else
  112. putstmnt(tb, v->lft, m);
  113. fprintf(tb, ", %d);\n\t\t", (i==0)?1:0);
  114. if (multi_oval > 0)
  115. jj++;
  116. break;
  117. } }
  118. jj = multi_oval - ii - 1;
  119. if (now->val == 1 && multi_oval > 0)
  120. jj++; /* new 3.4.0 */
  121. for (v = now->rgt, i = 0; v; v = v->rgt, i++)
  122. { switch(v->lft->ntyp) {
  123. case CONST:
  124. case EVAL:
  125. break;
  126. default:
  127. if (!v->lft->sym
  128. || strcmp(v->lft->sym->name, "_") != 0)
  129. { nocast=1; putstmnt(tb,v->lft,m);
  130. nocast=0; fprintf(tb, " = trpt->bup.oval");
  131. if (multi_oval > 0)
  132. fprintf(tb, "s[%d]", jj);
  133. fprintf(tb, ";\n\t\t");
  134. }
  135. if (multi_oval > 0)
  136. jj++;
  137. break;
  138. } }
  139. multi_oval -= ii;
  140. }
  141. break;
  142. case '@':
  143. fprintf(tb, "p_restor(II);\n\t\t");
  144. break;
  145. case ASGN:
  146. nocast=1; putstmnt(tb,now->lft,m);
  147. nocast=0; fprintf(tb, " = trpt->bup.oval");
  148. if (multi_oval > 0)
  149. { multi_oval--;
  150. fprintf(tb, "s[%d]", multi_oval-1);
  151. }
  152. check_proc(now->rgt, m);
  153. break;
  154. case 'c':
  155. check_proc(now->lft, m);
  156. break;
  157. case '.':
  158. case GOTO:
  159. case ELSE:
  160. case BREAK:
  161. break;
  162. case C_CODE:
  163. fprintf(tb, "sv_restor();\n");
  164. break;
  165. case ASSERT:
  166. case PRINT:
  167. check_proc(now, m);
  168. break;
  169. case PRINTM:
  170. break;
  171. default:
  172. printf("spin: bad node type %d (.b)\n", now->ntyp);
  173. alldone(1);
  174. }
  175. }
  176. int
  177. any_undo(Lextok *now)
  178. { /* is there anything to undo on a return move? */
  179. if (!now) return 1;
  180. switch (now->ntyp) {
  181. case 'c': return any_oper(now->lft, RUN);
  182. case ASSERT:
  183. case PRINT: return any_oper(now, RUN);
  184. case PRINTM:
  185. case '.':
  186. case GOTO:
  187. case ELSE:
  188. case BREAK: return 0;
  189. default: return 1;
  190. }
  191. }
  192. int
  193. any_oper(Lextok *now, int oper)
  194. { /* check if an expression contains oper operator */
  195. if (!now) return 0;
  196. if (now->ntyp == oper)
  197. return 1;
  198. return (any_oper(now->lft, oper) || any_oper(now->rgt, oper));
  199. }
  200. static void
  201. check_proc(Lextok *now, int m)
  202. {
  203. if (!now)
  204. return;
  205. if (now->ntyp == '@' || now->ntyp == RUN)
  206. { fprintf(tb, ";\n\t\t");
  207. undostmnt(now, m);
  208. }
  209. check_proc(now->lft, m);
  210. check_proc(now->rgt, m);
  211. }
  212. void
  213. genunio(void)
  214. { char buf1[256];
  215. Queue *q; int i;
  216. ntimes(tc, 0, 1, R13);
  217. for (q = qtab; q; q = q->nxt)
  218. { fprintf(tc, "\tcase %d:\n", q->qid);
  219. if (has_sorted)
  220. { sprintf(buf1, "((Q%d *)z)->contents", q->qid);
  221. fprintf(tc, "#ifdef HAS_SORTED\n");
  222. fprintf(tc, "\t\tj = trpt->ipt;\n"); /* ipt was bup.oval */
  223. fprintf(tc, "#endif\n");
  224. fprintf(tc, "\t\tfor (k = j; k < ((Q%d *)z)->Qlen; k++)\n",
  225. q->qid);
  226. fprintf(tc, "\t\t{\n");
  227. for (i = 0; i < q->nflds; i++)
  228. fprintf(tc, "\t\t\t%s[k].fld%d = %s[k+1].fld%d;\n",
  229. buf1, i, buf1, i);
  230. fprintf(tc, "\t\t}\n");
  231. fprintf(tc, "\t\tj = ((Q0 *)z)->Qlen;\n");
  232. }
  233. sprintf(buf1, "((Q%d *)z)->contents[j].fld", q->qid);
  234. for (i = 0; i < q->nflds; i++)
  235. fprintf(tc, "\t\t%s%d = 0;\n", buf1, i);
  236. if (q->nslots==0)
  237. { /* check if rendezvous succeeded, 1 level down */
  238. fprintf(tc, "\t\t_m = (trpt+1)->o_m;\n");
  239. fprintf(tc, "\t\tif (_m) (trpt-1)->o_pm |= 1;\n");
  240. fprintf(tc, "\t\tUnBlock;\n");
  241. } else
  242. fprintf(tc, "\t\t_m = trpt->o_m;\n");
  243. fprintf(tc, "\t\tbreak;\n");
  244. }
  245. ntimes(tc, 0, 1, R14);
  246. for (q = qtab; q; q = q->nxt)
  247. { sprintf(buf1, "((Q%d *)z)->contents", q->qid);
  248. fprintf(tc, " case %d:\n", q->qid);
  249. if (q->nslots == 0)
  250. fprintf(tc, "\t\tif (strt) boq = from+1;\n");
  251. else if (q->nslots > 1) /* shift */
  252. { fprintf(tc, "\t\tif (strt && slot<%d)\n",
  253. q->nslots-1);
  254. fprintf(tc, "\t\t{\tfor (j--; j>=slot; j--)\n");
  255. fprintf(tc, "\t\t\t{");
  256. for (i = 0; i < q->nflds; i++)
  257. { fprintf(tc, "\t%s[j+1].fld%d =\n\t\t\t",
  258. buf1, i);
  259. fprintf(tc, "\t%s[j].fld%d;\n\t\t\t",
  260. buf1, i);
  261. }
  262. fprintf(tc, "}\n\t\t}\n");
  263. }
  264. strcat(buf1, "[slot].fld");
  265. fprintf(tc, "\t\tif (strt) {\n");
  266. for (i = 0; i < q->nflds; i++)
  267. fprintf(tc, "\t\t\t%s%d = 0;\n", buf1, i);
  268. fprintf(tc, "\t\t}\n");
  269. if (q->nflds == 1) /* set */
  270. fprintf(tc, "\t\tif (fld == 0) %s0 = fldvar;\n",
  271. buf1);
  272. else
  273. { fprintf(tc, "\t\tswitch (fld) {\n");
  274. for (i = 0; i < q->nflds; i++)
  275. { fprintf(tc, "\t\tcase %d:\t%s", i, buf1);
  276. fprintf(tc, "%d = fldvar; break;\n", i);
  277. }
  278. fprintf(tc, "\t\t}\n");
  279. }
  280. fprintf(tc, "\t\tbreak;\n");
  281. }
  282. ntimes(tc, 0, 1, R15);
  283. }
  284. extern void explain(int);
  285. int
  286. proper_enabler(Lextok *n)
  287. {
  288. if (!n) return 1;
  289. switch (n->ntyp) {
  290. case NEMPTY: case FULL:
  291. case NFULL: case EMPTY:
  292. case LEN: case 'R':
  293. case NAME:
  294. has_provided = 1;
  295. if (strcmp(n->sym->name, "_pid") == 0)
  296. return 1;
  297. return (!(n->sym->context));
  298. case C_EXPR:
  299. case CONST:
  300. case TIMEOUT:
  301. has_provided = 1;
  302. return 1;
  303. case ENABLED: case PC_VAL:
  304. return proper_enabler(n->lft);
  305. case '!': case UMIN: case '~':
  306. return proper_enabler(n->lft);
  307. case '/': case '*': case '-': case '+':
  308. case '%': case LT: case GT: case '&': case '^':
  309. case '|': case LE: case GE: case NE: case '?':
  310. case EQ: case OR: case AND: case LSHIFT:
  311. case RSHIFT: case 'c':
  312. return proper_enabler(n->lft) && proper_enabler(n->rgt);
  313. default:
  314. break;
  315. }
  316. printf("spin: saw ");
  317. explain(n->ntyp);
  318. printf("\n");
  319. return 0;
  320. }