| 1 | /***** spin: pangen5.c *****/ |
| 2 | |
| 3 | /* Copyright (c) 1999-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 | typedef struct BuildStack { |
| 16 | FSM_trans *t; |
| 17 | struct BuildStack *nxt; |
| 18 | } BuildStack; |
| 19 | |
| 20 | extern ProcList *rdy; |
| 21 | extern int verbose, eventmapnr, claimnr, rvopt, export_ast, u_sync; |
| 22 | extern Element *Al_El; |
| 23 | |
| 24 | static FSM_state *fsm_free; |
| 25 | static FSM_trans *trans_free; |
| 26 | static BuildStack *bs, *bf; |
| 27 | static int max_st_id; |
| 28 | static int cur_st_id; |
| 29 | int o_max; |
| 30 | FSM_state *fsm; |
| 31 | FSM_state **fsm_tbl; |
| 32 | FSM_use *use_free; |
| 33 | |
| 34 | static void ana_seq(Sequence *); |
| 35 | static void ana_stmnt(FSM_trans *, Lextok *, int); |
| 36 | |
| 37 | extern void AST_slice(void); |
| 38 | extern void AST_store(ProcList *, int); |
| 39 | extern int has_global(Lextok *); |
| 40 | extern void exit(int); |
| 41 | |
| 42 | static void |
| 43 | fsm_table(void) |
| 44 | { FSM_state *f; |
| 45 | max_st_id += 2; |
| 46 | /* fprintf(stderr, "omax %d, max=%d\n", o_max, max_st_id); */ |
| 47 | if (o_max < max_st_id) |
| 48 | { o_max = max_st_id; |
| 49 | fsm_tbl = (FSM_state **) emalloc(max_st_id * sizeof(FSM_state *)); |
| 50 | } else |
| 51 | memset((char *)fsm_tbl, 0, max_st_id * sizeof(FSM_state *)); |
| 52 | cur_st_id = max_st_id; |
| 53 | max_st_id = 0; |
| 54 | |
| 55 | for (f = fsm; f; f = f->nxt) |
| 56 | fsm_tbl[f->from] = f; |
| 57 | } |
| 58 | |
| 59 | static int |
| 60 | FSM_DFS(int from, FSM_use *u) |
| 61 | { FSM_state *f; |
| 62 | FSM_trans *t; |
| 63 | FSM_use *v; |
| 64 | int n; |
| 65 | |
| 66 | if (from == 0) |
| 67 | return 1; |
| 68 | |
| 69 | f = fsm_tbl[from]; |
| 70 | |
| 71 | if (!f) |
| 72 | { printf("cannot find state %d\n", from); |
| 73 | fatal("fsm_dfs: cannot happen\n", (char *) 0); |
| 74 | } |
| 75 | |
| 76 | if (f->seen) |
| 77 | return 1; |
| 78 | f->seen = 1; |
| 79 | |
| 80 | for (t = f->t; t; t = t->nxt) |
| 81 | { |
| 82 | for (n = 0; n < 2; n++) |
| 83 | for (v = t->Val[n]; v; v = v->nxt) |
| 84 | if (u->var == v->var) |
| 85 | return n; /* a read or write */ |
| 86 | |
| 87 | if (!FSM_DFS(t->to, u)) |
| 88 | return 0; |
| 89 | } |
| 90 | return 1; |
| 91 | } |
| 92 | |
| 93 | static void |
| 94 | new_dfs(void) |
| 95 | { int i; |
| 96 | |
| 97 | for (i = 0; i < cur_st_id; i++) |
| 98 | if (fsm_tbl[i]) |
| 99 | fsm_tbl[i]->seen = 0; |
| 100 | } |
| 101 | |
| 102 | static int |
| 103 | good_dead(Element *e, FSM_use *u) |
| 104 | { |
| 105 | switch (u->special) { |
| 106 | case 2: /* ok if it's a receive */ |
| 107 | if (e->n->ntyp == ASGN |
| 108 | && e->n->rgt->ntyp == CONST |
| 109 | && e->n->rgt->val == 0) |
| 110 | return 0; |
| 111 | break; |
| 112 | case 1: /* must be able to use oval */ |
| 113 | if (e->n->ntyp != 'c' |
| 114 | && e->n->ntyp != 'r') |
| 115 | return 0; /* can't really happen */ |
| 116 | break; |
| 117 | } |
| 118 | return 1; |
| 119 | } |
| 120 | |
| 121 | #if 0 |
| 122 | static int howdeep = 0; |
| 123 | #endif |
| 124 | |
| 125 | static int |
| 126 | eligible(FSM_trans *v) |
| 127 | { Element *el = ZE; |
| 128 | Lextok *lt = ZN; |
| 129 | |
| 130 | if (v) el = v->step; |
| 131 | if (el) lt = v->step->n; |
| 132 | |
| 133 | if (!lt /* dead end */ |
| 134 | || v->nxt /* has alternatives */ |
| 135 | || el->esc /* has an escape */ |
| 136 | || (el->status&CHECK2) /* remotely referenced */ |
| 137 | || lt->ntyp == ATOMIC |
| 138 | || lt->ntyp == NON_ATOMIC /* used for inlines -- should be able to handle this */ |
| 139 | || lt->ntyp == IF |
| 140 | || lt->ntyp == C_CODE |
| 141 | || lt->ntyp == C_EXPR |
| 142 | || has_lab(el, 0) /* any label at all */ |
| 143 | |
| 144 | || lt->ntyp == DO |
| 145 | || lt->ntyp == UNLESS |
| 146 | || lt->ntyp == D_STEP |
| 147 | || lt->ntyp == ELSE |
| 148 | || lt->ntyp == '@' |
| 149 | || lt->ntyp == 'c' |
| 150 | || lt->ntyp == 'r' |
| 151 | || lt->ntyp == 's') |
| 152 | return 0; |
| 153 | |
| 154 | if (!(el->status&(2|4))) /* not atomic */ |
| 155 | { int unsafe = (el->status&I_GLOB)?1:has_global(el->n); |
| 156 | if (unsafe) |
| 157 | return 0; |
| 158 | } |
| 159 | |
| 160 | return 1; |
| 161 | } |
| 162 | |
| 163 | static int |
| 164 | canfill_in(FSM_trans *v) |
| 165 | { Element *el = v->step; |
| 166 | Lextok *lt = v->step->n; |
| 167 | |
| 168 | if (!lt /* dead end */ |
| 169 | || v->nxt /* has alternatives */ |
| 170 | || el->esc /* has an escape */ |
| 171 | || (el->status&CHECK2)) /* remotely referenced */ |
| 172 | return 0; |
| 173 | |
| 174 | if (!(el->status&(2|4)) /* not atomic */ |
| 175 | && ((el->status&I_GLOB) |
| 176 | || has_global(el->n))) /* and not safe */ |
| 177 | return 0; |
| 178 | |
| 179 | return 1; |
| 180 | } |
| 181 | |
| 182 | static int |
| 183 | pushbuild(FSM_trans *v) |
| 184 | { BuildStack *b; |
| 185 | |
| 186 | for (b = bs; b; b = b->nxt) |
| 187 | if (b->t == v) |
| 188 | return 0; |
| 189 | if (bf) |
| 190 | { b = bf; |
| 191 | bf = bf->nxt; |
| 192 | } else |
| 193 | b = (BuildStack *) emalloc(sizeof(BuildStack)); |
| 194 | b->t = v; |
| 195 | b->nxt = bs; |
| 196 | bs = b; |
| 197 | return 1; |
| 198 | } |
| 199 | |
| 200 | static void |
| 201 | popbuild(void) |
| 202 | { BuildStack *f; |
| 203 | if (!bs) |
| 204 | fatal("cannot happen, popbuild", (char *) 0); |
| 205 | f = bs; |
| 206 | bs = bs->nxt; |
| 207 | f->nxt = bf; |
| 208 | bf = f; /* freelist */ |
| 209 | } |
| 210 | |
| 211 | static int |
| 212 | build_step(FSM_trans *v) |
| 213 | { FSM_state *f; |
| 214 | Element *el; |
| 215 | #if 0 |
| 216 | Lextok *lt = ZN; |
| 217 | #endif |
| 218 | int st; |
| 219 | int r; |
| 220 | |
| 221 | if (!v) return -1; |
| 222 | |
| 223 | el = v->step; |
| 224 | st = v->to; |
| 225 | |
| 226 | if (!el) return -1; |
| 227 | |
| 228 | if (v->step->merge) |
| 229 | return v->step->merge; /* already done */ |
| 230 | |
| 231 | if (!eligible(v)) /* non-blocking */ |
| 232 | return -1; |
| 233 | |
| 234 | if (!pushbuild(v)) /* cycle detected */ |
| 235 | return -1; /* break cycle */ |
| 236 | |
| 237 | f = fsm_tbl[st]; |
| 238 | #if 0 |
| 239 | lt = v->step->n; |
| 240 | if (verbose&32) |
| 241 | { if (++howdeep == 1) |
| 242 | printf("spin: %s, line %3d, merge:\n", |
| 243 | lt->fn->name, |
| 244 | lt->ln); |
| 245 | printf("\t[%d] <seqno %d>\t", howdeep, el->seqno); |
| 246 | comment(stdout, lt, 0); |
| 247 | printf(";\n"); |
| 248 | } |
| 249 | #endif |
| 250 | r = build_step(f->t); |
| 251 | v->step->merge = (r == -1) ? st : r; |
| 252 | #if 0 |
| 253 | if (verbose&32) |
| 254 | { printf(" merge value: %d (st=%d,r=%d, line %d)\n", |
| 255 | v->step->merge, st, r, el->n->ln); |
| 256 | howdeep--; |
| 257 | } |
| 258 | #endif |
| 259 | popbuild(); |
| 260 | |
| 261 | return v->step->merge; |
| 262 | } |
| 263 | |
| 264 | static void |
| 265 | FSM_MERGER(/* char *pname */ void) /* find candidates for safely merging steps */ |
| 266 | { FSM_state *f, *g; |
| 267 | FSM_trans *t; |
| 268 | Lextok *lt; |
| 269 | |
| 270 | for (f = fsm; f; f = f->nxt) /* all states */ |
| 271 | for (t = f->t; t; t = t->nxt) /* all edges */ |
| 272 | { if (!t->step) continue; /* happens with 'unless' */ |
| 273 | |
| 274 | t->step->merge_in = f->in; /* ?? */ |
| 275 | |
| 276 | if (t->step->merge) |
| 277 | continue; |
| 278 | lt = t->step->n; |
| 279 | |
| 280 | if (lt->ntyp == 'c' |
| 281 | || lt->ntyp == 'r' |
| 282 | || lt->ntyp == 's') /* blocking stmnts */ |
| 283 | continue; /* handled in 2nd scan */ |
| 284 | |
| 285 | if (!eligible(t)) |
| 286 | continue; |
| 287 | |
| 288 | g = fsm_tbl[t->to]; |
| 289 | if (!g || !eligible(g->t)) |
| 290 | { |
| 291 | #define SINGLES |
| 292 | #ifdef SINGLES |
| 293 | t->step->merge_single = t->to; |
| 294 | #if 0 |
| 295 | if ((verbose&32)) |
| 296 | { printf("spin: %s, line %3d, merge_single:\n\t<seqno %d>\t", |
| 297 | t->step->n->fn->name, |
| 298 | t->step->n->ln, |
| 299 | t->step->seqno); |
| 300 | comment(stdout, t->step->n, 0); |
| 301 | printf(";\n"); |
| 302 | } |
| 303 | #endif |
| 304 | #endif |
| 305 | /* t is an isolated eligible step: |
| 306 | * |
| 307 | * a merge_start can connect to a proper |
| 308 | * merge chain or to a merge_single |
| 309 | * a merge chain can be preceded by |
| 310 | * a merge_start, but not by a merge_single |
| 311 | */ |
| 312 | |
| 313 | continue; |
| 314 | } |
| 315 | |
| 316 | (void) build_step(t); |
| 317 | } |
| 318 | |
| 319 | /* 2nd scan -- find possible merge_starts */ |
| 320 | |
| 321 | for (f = fsm; f; f = f->nxt) /* all states */ |
| 322 | for (t = f->t; t; t = t->nxt) /* all edges */ |
| 323 | { if (!t->step || t->step->merge) |
| 324 | continue; |
| 325 | |
| 326 | lt = t->step->n; |
| 327 | #if 0 |
| 328 | 4.1.3: |
| 329 | an rv send operation inside an atomic, *loses* atomicity |
| 330 | when executed |
| 331 | and should therefore never be merged with a subsequent |
| 332 | statement within the atomic sequence |
| 333 | the same is not true for non-rv send operations |
| 334 | #endif |
| 335 | |
| 336 | if (lt->ntyp == 'c' /* potentially blocking stmnts */ |
| 337 | || lt->ntyp == 'r' |
| 338 | || (lt->ntyp == 's' && u_sync == 0)) /* added !u_sync in 4.1.3 */ |
| 339 | { if (!canfill_in(t)) /* atomic, non-global, etc. */ |
| 340 | continue; |
| 341 | |
| 342 | g = fsm_tbl[t->to]; |
| 343 | if (!g || !g->t || !g->t->step) |
| 344 | continue; |
| 345 | if (g->t->step->merge) |
| 346 | t->step->merge_start = g->t->step->merge; |
| 347 | #ifdef SINGLES |
| 348 | else if (g->t->step->merge_single) |
| 349 | t->step->merge_start = g->t->step->merge_single; |
| 350 | #endif |
| 351 | #if 0 |
| 352 | if ((verbose&32) |
| 353 | && t->step->merge_start) |
| 354 | { printf("spin: %s, line %3d, merge_START:\n\t<seqno %d>\t", |
| 355 | lt->fn->name, |
| 356 | lt->ln, |
| 357 | t->step->seqno); |
| 358 | comment(stdout, lt, 0); |
| 359 | printf(";\n"); |
| 360 | } |
| 361 | #endif |
| 362 | } |
| 363 | } |
| 364 | } |
| 365 | |
| 366 | static void |
| 367 | FSM_ANA(void) |
| 368 | { FSM_state *f; |
| 369 | FSM_trans *t; |
| 370 | FSM_use *u, *v, *w; |
| 371 | int n; |
| 372 | |
| 373 | for (f = fsm; f; f = f->nxt) /* all states */ |
| 374 | for (t = f->t; t; t = t->nxt) /* all edges */ |
| 375 | for (n = 0; n < 2; n++) /* reads and writes */ |
| 376 | for (u = t->Val[n]; u; u = u->nxt) |
| 377 | { if (!u->var->context /* global */ |
| 378 | || u->var->type == CHAN |
| 379 | || u->var->type == STRUCT) |
| 380 | continue; |
| 381 | new_dfs(); |
| 382 | if (FSM_DFS(t->to, u)) /* cannot hit read before hitting write */ |
| 383 | u->special = n+1; /* means, reset to 0 after use */ |
| 384 | } |
| 385 | |
| 386 | if (!export_ast) |
| 387 | for (f = fsm; f; f = f->nxt) |
| 388 | for (t = f->t; t; t = t->nxt) |
| 389 | for (n = 0; n < 2; n++) |
| 390 | for (u = t->Val[n], w = (FSM_use *) 0; u; ) |
| 391 | { if (u->special) |
| 392 | { v = u->nxt; |
| 393 | if (!w) /* remove from list */ |
| 394 | t->Val[n] = v; |
| 395 | else |
| 396 | w->nxt = v; |
| 397 | #if q |
| 398 | if (verbose&32) |
| 399 | { printf("%s : %3d: %d -> %d \t", |
| 400 | t->step->n->fn->name, |
| 401 | t->step->n->ln, |
| 402 | f->from, |
| 403 | t->to); |
| 404 | comment(stdout, t->step->n, 0); |
| 405 | printf("\t%c%d: %s\n", n==0?'R':'L', |
| 406 | u->special, u->var->name); |
| 407 | } |
| 408 | #endif |
| 409 | if (good_dead(t->step, u)) |
| 410 | { u->nxt = t->step->dead; /* insert into dead */ |
| 411 | t->step->dead = u; |
| 412 | } |
| 413 | u = v; |
| 414 | } else |
| 415 | { w = u; |
| 416 | u = u->nxt; |
| 417 | } } |
| 418 | } |
| 419 | |
| 420 | void |
| 421 | rel_use(FSM_use *u) |
| 422 | { |
| 423 | if (!u) return; |
| 424 | rel_use(u->nxt); |
| 425 | u->var = (Symbol *) 0; |
| 426 | u->special = 0; |
| 427 | u->nxt = use_free; |
| 428 | use_free = u; |
| 429 | } |
| 430 | |
| 431 | static void |
| 432 | rel_trans(FSM_trans *t) |
| 433 | { |
| 434 | if (!t) return; |
| 435 | rel_trans(t->nxt); |
| 436 | rel_use(t->Val[0]); |
| 437 | rel_use(t->Val[1]); |
| 438 | t->Val[0] = t->Val[1] = (FSM_use *) 0; |
| 439 | t->nxt = trans_free; |
| 440 | trans_free = t; |
| 441 | } |
| 442 | |
| 443 | static void |
| 444 | rel_state(FSM_state *f) |
| 445 | { |
| 446 | if (!f) return; |
| 447 | rel_state(f->nxt); |
| 448 | rel_trans(f->t); |
| 449 | f->t = (FSM_trans *) 0; |
| 450 | f->nxt = fsm_free; |
| 451 | fsm_free = f; |
| 452 | } |
| 453 | |
| 454 | static void |
| 455 | FSM_DEL(void) |
| 456 | { |
| 457 | rel_state(fsm); |
| 458 | fsm = (FSM_state *) 0; |
| 459 | } |
| 460 | |
| 461 | static FSM_state * |
| 462 | mkstate(int s) |
| 463 | { FSM_state *f; |
| 464 | |
| 465 | /* fsm_tbl isn't allocated yet */ |
| 466 | for (f = fsm; f; f = f->nxt) |
| 467 | if (f->from == s) |
| 468 | break; |
| 469 | if (!f) |
| 470 | { if (fsm_free) |
| 471 | { f = fsm_free; |
| 472 | memset(f, 0, sizeof(FSM_state)); |
| 473 | fsm_free = fsm_free->nxt; |
| 474 | } else |
| 475 | f = (FSM_state *) emalloc(sizeof(FSM_state)); |
| 476 | f->from = s; |
| 477 | f->t = (FSM_trans *) 0; |
| 478 | f->nxt = fsm; |
| 479 | fsm = f; |
| 480 | if (s > max_st_id) |
| 481 | max_st_id = s; |
| 482 | } |
| 483 | return f; |
| 484 | } |
| 485 | |
| 486 | static FSM_trans * |
| 487 | get_trans(int to) |
| 488 | { FSM_trans *t; |
| 489 | |
| 490 | if (trans_free) |
| 491 | { t = trans_free; |
| 492 | memset(t, 0, sizeof(FSM_trans)); |
| 493 | trans_free = trans_free->nxt; |
| 494 | } else |
| 495 | t = (FSM_trans *) emalloc(sizeof(FSM_trans)); |
| 496 | |
| 497 | t->to = to; |
| 498 | return t; |
| 499 | } |
| 500 | |
| 501 | static void |
| 502 | FSM_EDGE(int from, int to, Element *e) |
| 503 | { FSM_state *f; |
| 504 | FSM_trans *t; |
| 505 | |
| 506 | f = mkstate(from); /* find it or else make it */ |
| 507 | t = get_trans(to); |
| 508 | |
| 509 | t->step = e; |
| 510 | t->nxt = f->t; |
| 511 | f->t = t; |
| 512 | |
| 513 | f = mkstate(to); |
| 514 | f->in++; |
| 515 | |
| 516 | if (export_ast) |
| 517 | { t = get_trans(from); |
| 518 | t->step = e; |
| 519 | t->nxt = f->p; /* from is a predecessor of to */ |
| 520 | f->p = t; |
| 521 | } |
| 522 | |
| 523 | if (t->step) |
| 524 | ana_stmnt(t, t->step->n, 0); |
| 525 | } |
| 526 | |
| 527 | #define LVAL 1 |
| 528 | #define RVAL 0 |
| 529 | |
| 530 | static void |
| 531 | ana_var(FSM_trans *t, Lextok *now, int usage) |
| 532 | { FSM_use *u, *v; |
| 533 | |
| 534 | if (!t || !now || !now->sym) |
| 535 | return; |
| 536 | |
| 537 | if (now->sym->name[0] == '_' |
| 538 | && (strcmp(now->sym->name, "_") == 0 |
| 539 | || strcmp(now->sym->name, "_pid") == 0 |
| 540 | || strcmp(now->sym->name, "_last") == 0)) |
| 541 | return; |
| 542 | |
| 543 | v = t->Val[usage]; |
| 544 | for (u = v; u; u = u->nxt) |
| 545 | if (u->var == now->sym) |
| 546 | return; /* it's already there */ |
| 547 | |
| 548 | if (!now->lft) |
| 549 | { /* not for array vars -- it's hard to tell statically |
| 550 | if the index would, at runtime, evaluate to the |
| 551 | same values at lval and rval references |
| 552 | */ |
| 553 | if (use_free) |
| 554 | { u = use_free; |
| 555 | use_free = use_free->nxt; |
| 556 | } else |
| 557 | u = (FSM_use *) emalloc(sizeof(FSM_use)); |
| 558 | |
| 559 | u->var = now->sym; |
| 560 | u->nxt = t->Val[usage]; |
| 561 | t->Val[usage] = u; |
| 562 | } else |
| 563 | ana_stmnt(t, now->lft, RVAL); /* index */ |
| 564 | |
| 565 | if (now->sym->type == STRUCT |
| 566 | && now->rgt |
| 567 | && now->rgt->lft) |
| 568 | ana_var(t, now->rgt->lft, usage); |
| 569 | } |
| 570 | |
| 571 | static void |
| 572 | ana_stmnt(FSM_trans *t, Lextok *now, int usage) |
| 573 | { Lextok *v; |
| 574 | |
| 575 | if (!t || !now) return; |
| 576 | |
| 577 | switch (now->ntyp) { |
| 578 | case '.': |
| 579 | case BREAK: |
| 580 | case GOTO: |
| 581 | case CONST: |
| 582 | case TIMEOUT: |
| 583 | case NONPROGRESS: |
| 584 | case ELSE: |
| 585 | case '@': |
| 586 | case 'q': |
| 587 | case IF: |
| 588 | case DO: |
| 589 | case ATOMIC: |
| 590 | case NON_ATOMIC: |
| 591 | case D_STEP: |
| 592 | case C_CODE: |
| 593 | case C_EXPR: |
| 594 | break; |
| 595 | |
| 596 | case '!': |
| 597 | case UMIN: |
| 598 | case '~': |
| 599 | case ENABLED: |
| 600 | case PC_VAL: |
| 601 | case LEN: |
| 602 | case FULL: |
| 603 | case EMPTY: |
| 604 | case NFULL: |
| 605 | case NEMPTY: |
| 606 | case ASSERT: |
| 607 | case 'c': |
| 608 | ana_stmnt(t, now->lft, RVAL); |
| 609 | break; |
| 610 | |
| 611 | case '/': |
| 612 | case '*': |
| 613 | case '-': |
| 614 | case '+': |
| 615 | case '%': |
| 616 | case '&': |
| 617 | case '^': |
| 618 | case '|': |
| 619 | case LT: |
| 620 | case GT: |
| 621 | case LE: |
| 622 | case GE: |
| 623 | case NE: |
| 624 | case EQ: |
| 625 | case OR: |
| 626 | case AND: |
| 627 | case LSHIFT: |
| 628 | case RSHIFT: |
| 629 | ana_stmnt(t, now->lft, RVAL); |
| 630 | ana_stmnt(t, now->rgt, RVAL); |
| 631 | break; |
| 632 | |
| 633 | case ASGN: |
| 634 | ana_stmnt(t, now->lft, LVAL); |
| 635 | ana_stmnt(t, now->rgt, RVAL); |
| 636 | break; |
| 637 | |
| 638 | case PRINT: |
| 639 | case RUN: |
| 640 | for (v = now->lft; v; v = v->rgt) |
| 641 | ana_stmnt(t, v->lft, RVAL); |
| 642 | break; |
| 643 | |
| 644 | case PRINTM: |
| 645 | if (now->lft && !now->lft->ismtyp) |
| 646 | ana_stmnt(t, now->lft, RVAL); |
| 647 | break; |
| 648 | |
| 649 | case 's': |
| 650 | ana_stmnt(t, now->lft, RVAL); |
| 651 | for (v = now->rgt; v; v = v->rgt) |
| 652 | ana_stmnt(t, v->lft, RVAL); |
| 653 | break; |
| 654 | |
| 655 | case 'R': |
| 656 | case 'r': |
| 657 | ana_stmnt(t, now->lft, RVAL); |
| 658 | for (v = now->rgt; v; v = v->rgt) |
| 659 | { if (v->lft->ntyp == EVAL) |
| 660 | ana_stmnt(t, v->lft->lft, RVAL); |
| 661 | else |
| 662 | if (v->lft->ntyp != CONST |
| 663 | && now->ntyp != 'R') /* was v->lft->ntyp */ |
| 664 | ana_stmnt(t, v->lft, LVAL); |
| 665 | } |
| 666 | break; |
| 667 | |
| 668 | case '?': |
| 669 | ana_stmnt(t, now->lft, RVAL); |
| 670 | if (now->rgt) |
| 671 | { ana_stmnt(t, now->rgt->lft, RVAL); |
| 672 | ana_stmnt(t, now->rgt->rgt, RVAL); |
| 673 | } |
| 674 | break; |
| 675 | |
| 676 | case NAME: |
| 677 | ana_var(t, now, usage); |
| 678 | break; |
| 679 | |
| 680 | case 'p': /* remote ref */ |
| 681 | ana_stmnt(t, now->lft->lft, RVAL); /* process id */ |
| 682 | ana_var(t, now, RVAL); |
| 683 | ana_var(t, now->rgt, RVAL); |
| 684 | break; |
| 685 | |
| 686 | default: |
| 687 | printf("spin: bad node type %d line %d (ana_stmnt)\n", now->ntyp, now->ln); |
| 688 | fatal("aborting", (char *) 0); |
| 689 | } |
| 690 | } |
| 691 | |
| 692 | void |
| 693 | ana_src(int dataflow, int merger) /* called from main.c and guided.c */ |
| 694 | { ProcList *p; |
| 695 | Element *e; |
| 696 | #if 0 |
| 697 | int counter = 1; |
| 698 | #endif |
| 699 | for (p = rdy; p; p = p->nxt) |
| 700 | { if (p->tn == eventmapnr |
| 701 | || p->tn == claimnr) |
| 702 | continue; |
| 703 | |
| 704 | ana_seq(p->s); |
| 705 | fsm_table(); |
| 706 | |
| 707 | e = p->s->frst; |
| 708 | #if 0 |
| 709 | if (dataflow || merger) |
| 710 | { printf("spin: %d, optimizing '%s'", |
| 711 | counter++, p->n->name); |
| 712 | fflush(stdout); |
| 713 | } |
| 714 | #endif |
| 715 | if (dataflow) |
| 716 | { FSM_ANA(); |
| 717 | } |
| 718 | if (merger) |
| 719 | { FSM_MERGER(/* p->n->name */); |
| 720 | huntele(e, e->status, -1)->merge_in = 1; /* start-state */ |
| 721 | #if 0 |
| 722 | printf("\n"); |
| 723 | #endif |
| 724 | } |
| 725 | if (export_ast) |
| 726 | AST_store(p, huntele(e, e->status, -1)->seqno); |
| 727 | |
| 728 | FSM_DEL(); |
| 729 | } |
| 730 | for (e = Al_El; e; e = e->Nxt) |
| 731 | { |
| 732 | if (!(e->status&DONE) && (verbose&32)) |
| 733 | { printf("unreachable code: "); |
| 734 | printf("%s, line %3d: ", |
| 735 | e->n->fn->name, e->n->ln); |
| 736 | comment(stdout, e->n, 0); |
| 737 | printf("\n"); |
| 738 | } |
| 739 | e->status &= ~DONE; |
| 740 | } |
| 741 | if (export_ast) |
| 742 | { AST_slice(); |
| 743 | exit(0); |
| 744 | } |
| 745 | } |
| 746 | |
| 747 | void |
| 748 | spit_recvs(FILE *f1, FILE *f2) /* called from pangen2.c */ |
| 749 | { Element *e; |
| 750 | Sequence *s; |
| 751 | extern int Unique; |
| 752 | |
| 753 | fprintf(f1, "unsigned char Is_Recv[%d];\n", Unique); |
| 754 | |
| 755 | fprintf(f2, "void\nset_recvs(void)\n{\n"); |
| 756 | for (e = Al_El; e; e = e->Nxt) |
| 757 | { if (!e->n) continue; |
| 758 | |
| 759 | switch (e->n->ntyp) { |
| 760 | case 'r': |
| 761 | markit: fprintf(f2, "\tIs_Recv[%d] = 1;\n", e->Seqno); |
| 762 | break; |
| 763 | case D_STEP: |
| 764 | s = e->n->sl->this; |
| 765 | switch (s->frst->n->ntyp) { |
| 766 | case DO: |
| 767 | fatal("unexpected: do at start of d_step", (char *) 0); |
| 768 | case IF: /* conservative: fall through */ |
| 769 | case 'r': goto markit; |
| 770 | } |
| 771 | break; |
| 772 | } |
| 773 | } |
| 774 | fprintf(f2, "}\n"); |
| 775 | |
| 776 | if (rvopt) |
| 777 | { |
| 778 | fprintf(f2, "int\nno_recvs(int me)\n{\n"); |
| 779 | fprintf(f2, " int h; uchar ot; short tt;\n"); |
| 780 | fprintf(f2, " Trans *t;\n"); |
| 781 | fprintf(f2, " for (h = BASE; h < (int) now._nr_pr; h++)\n"); |
| 782 | fprintf(f2, " { if (h == me) continue;\n"); |
| 783 | fprintf(f2, " tt = (short) ((P0 *)pptr(h))->_p;\n"); |
| 784 | fprintf(f2, " ot = (uchar) ((P0 *)pptr(h))->_t;\n"); |
| 785 | fprintf(f2, " for (t = trans[ot][tt]; t; t = t->nxt)\n"); |
| 786 | fprintf(f2, " if (Is_Recv[t->t_id]) return 0;\n"); |
| 787 | fprintf(f2, " }\n"); |
| 788 | fprintf(f2, " return 1;\n"); |
| 789 | fprintf(f2, "}\n"); |
| 790 | } |
| 791 | } |
| 792 | |
| 793 | static void |
| 794 | ana_seq(Sequence *s) |
| 795 | { SeqList *h; |
| 796 | Sequence *t; |
| 797 | Element *e, *g; |
| 798 | int From, To; |
| 799 | |
| 800 | for (e = s->frst; e; e = e->nxt) |
| 801 | { if (e->status & DONE) |
| 802 | goto checklast; |
| 803 | |
| 804 | e->status |= DONE; |
| 805 | |
| 806 | From = e->seqno; |
| 807 | |
| 808 | if (e->n->ntyp == UNLESS) |
| 809 | ana_seq(e->sub->this); |
| 810 | else if (e->sub) |
| 811 | { for (h = e->sub; h; h = h->nxt) |
| 812 | { g = huntstart(h->this->frst); |
| 813 | To = g->seqno; |
| 814 | |
| 815 | if (g->n->ntyp != 'c' |
| 816 | || g->n->lft->ntyp != CONST |
| 817 | || g->n->lft->val != 0 |
| 818 | || g->esc) |
| 819 | FSM_EDGE(From, To, e); |
| 820 | /* else it's a dead link */ |
| 821 | } |
| 822 | for (h = e->sub; h; h = h->nxt) |
| 823 | ana_seq(h->this); |
| 824 | } else if (e->n->ntyp == ATOMIC |
| 825 | || e->n->ntyp == D_STEP |
| 826 | || e->n->ntyp == NON_ATOMIC) |
| 827 | { |
| 828 | t = e->n->sl->this; |
| 829 | g = huntstart(t->frst); |
| 830 | t->last->nxt = e->nxt; |
| 831 | To = g->seqno; |
| 832 | FSM_EDGE(From, To, e); |
| 833 | |
| 834 | ana_seq(t); |
| 835 | } else |
| 836 | { if (e->n->ntyp == GOTO) |
| 837 | { g = get_lab(e->n, 1); |
| 838 | g = huntele(g, e->status, -1); |
| 839 | To = g->seqno; |
| 840 | } else if (e->nxt) |
| 841 | { g = huntele(e->nxt, e->status, -1); |
| 842 | To = g->seqno; |
| 843 | } else |
| 844 | To = 0; |
| 845 | |
| 846 | FSM_EDGE(From, To, e); |
| 847 | |
| 848 | if (e->esc |
| 849 | && e->n->ntyp != GOTO |
| 850 | && e->n->ntyp != '.') |
| 851 | for (h = e->esc; h; h = h->nxt) |
| 852 | { g = huntstart(h->this->frst); |
| 853 | To = g->seqno; |
| 854 | FSM_EDGE(From, To, ZE); |
| 855 | ana_seq(h->this); |
| 856 | } |
| 857 | } |
| 858 | |
| 859 | checklast: if (e == s->last) |
| 860 | break; |
| 861 | } |
| 862 | } |