pangen4.c 7.9 KB

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