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