| 1 | /***** spin: dstep.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 | #define MAXDSTEP 1024 /* was 512 */ |
| 16 | |
| 17 | char *NextLab[64]; |
| 18 | int Level=0, GenCode=0, IsGuard=0, TestOnly=0; |
| 19 | |
| 20 | static int Tj=0, Jt=0, LastGoto=0; |
| 21 | static int Tojump[MAXDSTEP], Jumpto[MAXDSTEP], Special[MAXDSTEP]; |
| 22 | static void putCode(FILE *, Element *, Element *, Element *, int); |
| 23 | |
| 24 | extern int Pid, claimnr, separate, OkBreak; |
| 25 | |
| 26 | static void |
| 27 | Sourced(int n, int special) |
| 28 | { int i; |
| 29 | for (i = 0; i < Tj; i++) |
| 30 | if (Tojump[i] == n) |
| 31 | return; |
| 32 | if (Tj >= MAXDSTEP) |
| 33 | fatal("d_step sequence too long", (char *)0); |
| 34 | Special[Tj] = special; |
| 35 | Tojump[Tj++] = n; |
| 36 | } |
| 37 | |
| 38 | static void |
| 39 | Dested(int n) |
| 40 | { int i; |
| 41 | for (i = 0; i < Tj; i++) |
| 42 | if (Tojump[i] == n) |
| 43 | return; |
| 44 | for (i = 0; i < Jt; i++) |
| 45 | if (Jumpto[i] == n) |
| 46 | return; |
| 47 | if (Jt >= MAXDSTEP) |
| 48 | fatal("d_step sequence too long", (char *)0); |
| 49 | Jumpto[Jt++] = n; |
| 50 | LastGoto = 1; |
| 51 | } |
| 52 | |
| 53 | static void |
| 54 | Mopup(FILE *fd) |
| 55 | { int i, j; |
| 56 | |
| 57 | for (i = 0; i < Jt; i++) |
| 58 | { for (j = 0; j < Tj; j++) |
| 59 | if (Tojump[j] == Jumpto[i]) |
| 60 | break; |
| 61 | if (j == Tj) |
| 62 | { char buf[16]; |
| 63 | if (Jumpto[i] == OkBreak) |
| 64 | { if (!LastGoto) |
| 65 | fprintf(fd, "S_%.3d_0: /* break-dest */\n", |
| 66 | OkBreak); |
| 67 | } else { |
| 68 | sprintf(buf, "S_%.3d_0", Jumpto[i]); |
| 69 | non_fatal("goto %s breaks from d_step seq", buf); |
| 70 | } } } |
| 71 | for (j = 0; j < Tj; j++) |
| 72 | { for (i = 0; i < Jt; i++) |
| 73 | if (Tojump[j] == Jumpto[i]) |
| 74 | break; |
| 75 | #ifdef DEBUG |
| 76 | if (i == Jt && !Special[i]) |
| 77 | fprintf(fd, "\t\t/* no goto's to S_%.3d_0 */\n", |
| 78 | Tojump[j]); |
| 79 | #endif |
| 80 | } |
| 81 | for (j = i = 0; j < Tj; j++) |
| 82 | if (Special[j]) |
| 83 | { Tojump[i] = Tojump[j]; |
| 84 | Special[i] = 2; |
| 85 | if (i >= MAXDSTEP) |
| 86 | fatal("cannot happen (dstep.c)", (char *)0); |
| 87 | i++; |
| 88 | } |
| 89 | Tj = i; /* keep only the global exit-labels */ |
| 90 | Jt = 0; |
| 91 | } |
| 92 | |
| 93 | static int |
| 94 | FirstTime(int n) |
| 95 | { int i; |
| 96 | for (i = 0; i < Tj; i++) |
| 97 | if (Tojump[i] == n) |
| 98 | return (Special[i] <= 1); |
| 99 | return 1; |
| 100 | } |
| 101 | |
| 102 | static void |
| 103 | illegal(Element *e, char *str) |
| 104 | { |
| 105 | printf("illegal operator in 'd_step:' '"); |
| 106 | comment(stdout, e->n, 0); |
| 107 | printf("'\n"); |
| 108 | fatal("'%s'", str); |
| 109 | } |
| 110 | |
| 111 | static void |
| 112 | filterbad(Element *e) |
| 113 | { |
| 114 | switch (e->n->ntyp) { |
| 115 | case ASSERT: |
| 116 | case PRINT: |
| 117 | case 'c': |
| 118 | /* run cannot be completely undone |
| 119 | * with sv_save-sv_restor |
| 120 | */ |
| 121 | if (any_oper(e->n->lft, RUN)) |
| 122 | illegal(e, "run operator in d_step"); |
| 123 | |
| 124 | /* remote refs inside d_step sequences |
| 125 | * would be okay, but they cannot always |
| 126 | * be interpreted by the simulator the |
| 127 | * same as by the verifier (e.g., for an |
| 128 | * error trail) |
| 129 | */ |
| 130 | if (any_oper(e->n->lft, 'p')) |
| 131 | illegal(e, "remote reference in d_step"); |
| 132 | break; |
| 133 | case '@': |
| 134 | illegal(e, "process termination"); |
| 135 | break; |
| 136 | case D_STEP: |
| 137 | illegal(e, "nested d_step sequence"); |
| 138 | break; |
| 139 | case ATOMIC: |
| 140 | illegal(e, "nested atomic sequence"); |
| 141 | break; |
| 142 | default: |
| 143 | break; |
| 144 | } |
| 145 | } |
| 146 | |
| 147 | static int |
| 148 | CollectGuards(FILE *fd, Element *e, int inh) |
| 149 | { SeqList *h; Element *ee; |
| 150 | |
| 151 | for (h = e->sub; h; h = h->nxt) |
| 152 | { ee = huntstart(h->this->frst); |
| 153 | filterbad(ee); |
| 154 | switch (ee->n->ntyp) { |
| 155 | case NON_ATOMIC: |
| 156 | inh += CollectGuards(fd, ee->n->sl->this->frst, inh); |
| 157 | break; |
| 158 | case IF: |
| 159 | inh += CollectGuards(fd, ee, inh); |
| 160 | break; |
| 161 | case '.': |
| 162 | if (ee->nxt->n->ntyp == DO) |
| 163 | inh += CollectGuards(fd, ee->nxt, inh); |
| 164 | break; |
| 165 | case ELSE: |
| 166 | if (inh++ > 0) fprintf(fd, " || "); |
| 167 | /* 4.2.5 */ if (Pid != claimnr) |
| 168 | fprintf(fd, "(boq == -1 /* else */)"); |
| 169 | else |
| 170 | fprintf(fd, "(1 /* else */)"); |
| 171 | break; |
| 172 | case 'R': |
| 173 | if (inh++ > 0) fprintf(fd, " || "); |
| 174 | fprintf(fd, "("); TestOnly=1; |
| 175 | putstmnt(fd, ee->n, ee->seqno); |
| 176 | fprintf(fd, ")"); TestOnly=0; |
| 177 | break; |
| 178 | case 'r': |
| 179 | if (inh++ > 0) fprintf(fd, " || "); |
| 180 | fprintf(fd, "("); TestOnly=1; |
| 181 | putstmnt(fd, ee->n, ee->seqno); |
| 182 | fprintf(fd, ")"); TestOnly=0; |
| 183 | break; |
| 184 | case 's': |
| 185 | if (inh++ > 0) fprintf(fd, " || "); |
| 186 | fprintf(fd, "("); TestOnly=1; |
| 187 | /* 4.2.1 */ if (Pid != claimnr) fprintf(fd, "(boq == -1) && "); |
| 188 | putstmnt(fd, ee->n, ee->seqno); |
| 189 | fprintf(fd, ")"); TestOnly=0; |
| 190 | break; |
| 191 | case 'c': |
| 192 | if (inh++ > 0) fprintf(fd, " || "); |
| 193 | fprintf(fd, "("); TestOnly=1; |
| 194 | if (Pid != claimnr) |
| 195 | fprintf(fd, "(boq == -1 && "); |
| 196 | putstmnt(fd, ee->n->lft, e->seqno); |
| 197 | if (Pid != claimnr) |
| 198 | fprintf(fd, ")"); |
| 199 | fprintf(fd, ")"); TestOnly=0; |
| 200 | break; |
| 201 | } } |
| 202 | return inh; |
| 203 | } |
| 204 | |
| 205 | int |
| 206 | putcode(FILE *fd, Sequence *s, Element *nxt, int justguards, int ln, int seqno) |
| 207 | { int isg=0; char buf[64]; |
| 208 | |
| 209 | NextLab[0] = "continue"; |
| 210 | filterbad(s->frst); |
| 211 | |
| 212 | switch (s->frst->n->ntyp) { |
| 213 | case UNLESS: |
| 214 | non_fatal("'unless' inside d_step - ignored", (char *) 0); |
| 215 | return putcode(fd, s->frst->n->sl->this, nxt, 0, ln, seqno); |
| 216 | case NON_ATOMIC: |
| 217 | (void) putcode(fd, s->frst->n->sl->this, ZE, 1, ln, seqno); |
| 218 | break; |
| 219 | case IF: |
| 220 | fprintf(fd, "if (!("); |
| 221 | if (!CollectGuards(fd, s->frst, 0)) /* what about boq? */ |
| 222 | fprintf(fd, "1"); |
| 223 | fprintf(fd, "))\n\t\t\tcontinue;"); |
| 224 | isg = 1; |
| 225 | break; |
| 226 | case '.': |
| 227 | if (s->frst->nxt->n->ntyp == DO) |
| 228 | { fprintf(fd, "if (!("); |
| 229 | if (!CollectGuards(fd, s->frst->nxt, 0)) |
| 230 | fprintf(fd, "1"); |
| 231 | fprintf(fd, "))\n\t\t\tcontinue;"); |
| 232 | isg = 1; |
| 233 | } |
| 234 | break; |
| 235 | case 'R': /* <- can't really happen (it's part of a 'c') */ |
| 236 | fprintf(fd, "if (!("); TestOnly=1; |
| 237 | putstmnt(fd, s->frst->n, s->frst->seqno); |
| 238 | fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0; |
| 239 | break; |
| 240 | case 'r': |
| 241 | fprintf(fd, "if (!("); TestOnly=1; |
| 242 | putstmnt(fd, s->frst->n, s->frst->seqno); |
| 243 | fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0; |
| 244 | break; |
| 245 | case 's': |
| 246 | fprintf(fd, "if ("); |
| 247 | #if 1 |
| 248 | /* 4.2.1 */ if (Pid != claimnr) fprintf(fd, "(boq != -1) || "); |
| 249 | #endif |
| 250 | fprintf(fd, "!("); TestOnly=1; |
| 251 | putstmnt(fd, s->frst->n, s->frst->seqno); |
| 252 | fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0; |
| 253 | break; |
| 254 | case 'c': |
| 255 | fprintf(fd, "if (!("); |
| 256 | if (Pid != claimnr) fprintf(fd, "boq == -1 && "); |
| 257 | TestOnly=1; |
| 258 | putstmnt(fd, s->frst->n->lft, s->frst->seqno); |
| 259 | fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0; |
| 260 | break; |
| 261 | case ELSE: |
| 262 | fprintf(fd, "if (boq != -1 || ("); |
| 263 | if (separate != 2) fprintf(fd, "trpt->"); |
| 264 | fprintf(fd, "o_pm&1))\n\t\t\tcontinue;"); |
| 265 | break; |
| 266 | case ASGN: /* new 3.0.8 */ |
| 267 | fprintf(fd, "IfNotBlocked"); |
| 268 | break; |
| 269 | } |
| 270 | if (justguards) return 0; |
| 271 | |
| 272 | fprintf(fd, "\n\t\tsv_save();\n\t\t"); |
| 273 | #if 1 |
| 274 | fprintf(fd, "reached[%d][%d] = 1;\n\t\t", Pid, seqno); |
| 275 | fprintf(fd, "reached[%d][t->st] = 1;\n\t\t", Pid); /* true next state */ |
| 276 | fprintf(fd, "reached[%d][tt] = 1;\n", Pid); /* true current state */ |
| 277 | #endif |
| 278 | sprintf(buf, "Uerror(\"block in d_step seq, line %d\")", ln); |
| 279 | NextLab[0] = buf; |
| 280 | putCode(fd, s->frst, s->extent, nxt, isg); |
| 281 | |
| 282 | if (nxt) |
| 283 | { extern Symbol *Fname; |
| 284 | extern int lineno; |
| 285 | |
| 286 | if (FirstTime(nxt->Seqno) |
| 287 | && (!(nxt->status & DONE2) || !(nxt->status & D_ATOM))) |
| 288 | { fprintf(fd, "S_%.3d_0: /* 1 */\n", nxt->Seqno); |
| 289 | nxt->status |= DONE2; |
| 290 | LastGoto = 0; |
| 291 | } |
| 292 | Sourced(nxt->Seqno, 1); |
| 293 | lineno = ln; |
| 294 | Fname = nxt->n->fn; |
| 295 | Mopup(fd); |
| 296 | } |
| 297 | unskip(s->frst->seqno); |
| 298 | return LastGoto; |
| 299 | } |
| 300 | |
| 301 | static void |
| 302 | putCode(FILE *fd, Element *f, Element *last, Element *next, int isguard) |
| 303 | { Element *e, *N; |
| 304 | SeqList *h; int i; |
| 305 | char NextOpt[64]; |
| 306 | static int bno = 0; |
| 307 | |
| 308 | for (e = f; e; e = e->nxt) |
| 309 | { if (e->status & DONE2) |
| 310 | continue; |
| 311 | e->status |= DONE2; |
| 312 | |
| 313 | if (!(e->status & D_ATOM)) |
| 314 | { if (!LastGoto) |
| 315 | { fprintf(fd, "\t\tgoto S_%.3d_0;\n", |
| 316 | e->Seqno); |
| 317 | Dested(e->Seqno); |
| 318 | } |
| 319 | break; |
| 320 | } |
| 321 | fprintf(fd, "S_%.3d_0: /* 2 */\n", e->Seqno); |
| 322 | LastGoto = 0; |
| 323 | Sourced(e->Seqno, 0); |
| 324 | |
| 325 | if (!e->sub) |
| 326 | { filterbad(e); |
| 327 | switch (e->n->ntyp) { |
| 328 | case NON_ATOMIC: |
| 329 | h = e->n->sl; |
| 330 | putCode(fd, h->this->frst, |
| 331 | h->this->extent, e->nxt, 0); |
| 332 | break; |
| 333 | case BREAK: |
| 334 | if (LastGoto) break; |
| 335 | if (e->nxt) |
| 336 | { i = target( huntele(e->nxt, |
| 337 | e->status, -1))->Seqno; |
| 338 | fprintf(fd, "\t\tgoto S_%.3d_0; ", i); |
| 339 | fprintf(fd, "/* 'break' */\n"); |
| 340 | Dested(i); |
| 341 | } else |
| 342 | { if (next) |
| 343 | { fprintf(fd, "\t\tgoto S_%.3d_0;", |
| 344 | next->Seqno); |
| 345 | fprintf(fd, " /* NEXT */\n"); |
| 346 | Dested(next->Seqno); |
| 347 | } else |
| 348 | fatal("cannot interpret d_step", 0); |
| 349 | } |
| 350 | break; |
| 351 | case GOTO: |
| 352 | if (LastGoto) break; |
| 353 | i = huntele( get_lab(e->n,1), |
| 354 | e->status, -1)->Seqno; |
| 355 | fprintf(fd, "\t\tgoto S_%.3d_0; ", i); |
| 356 | fprintf(fd, "/* 'goto' */\n"); |
| 357 | Dested(i); |
| 358 | break; |
| 359 | case '.': |
| 360 | if (LastGoto) break; |
| 361 | if (e->nxt && (e->nxt->status & DONE2)) |
| 362 | { i = e->nxt?e->nxt->Seqno:0; |
| 363 | fprintf(fd, "\t\tgoto S_%.3d_0;", i); |
| 364 | fprintf(fd, " /* '.' */\n"); |
| 365 | Dested(i); |
| 366 | } |
| 367 | break; |
| 368 | default: |
| 369 | putskip(e->seqno); |
| 370 | GenCode = 1; IsGuard = isguard; |
| 371 | fprintf(fd, "\t\t"); |
| 372 | putstmnt(fd, e->n, e->seqno); |
| 373 | fprintf(fd, ";\n"); |
| 374 | GenCode = IsGuard = isguard = LastGoto = 0; |
| 375 | break; |
| 376 | } |
| 377 | i = e->nxt?e->nxt->Seqno:0; |
| 378 | if (e->nxt && e->nxt->status & DONE2 && !LastGoto) |
| 379 | { fprintf(fd, "\t\tgoto S_%.3d_0; ", i); |
| 380 | fprintf(fd, "/* ';' */\n"); |
| 381 | Dested(i); |
| 382 | break; |
| 383 | } |
| 384 | } else |
| 385 | { for (h = e->sub, i=1; h; h = h->nxt, i++) |
| 386 | { sprintf(NextOpt, "goto S_%.3d_%d", |
| 387 | e->Seqno, i); |
| 388 | NextLab[++Level] = NextOpt; |
| 389 | N = (e->n && e->n->ntyp == DO) ? e : e->nxt; |
| 390 | putCode(fd, h->this->frst, |
| 391 | h->this->extent, N, 1); |
| 392 | Level--; |
| 393 | fprintf(fd, "%s: /* 3 */\n", &NextOpt[5]); |
| 394 | LastGoto = 0; |
| 395 | } |
| 396 | if (!LastGoto) |
| 397 | { fprintf(fd, "\t\tUerror(\"blocking sel "); |
| 398 | fprintf(fd, "in d_step (nr.%d, near line %d)\");\n", |
| 399 | bno++, (e->n)?e->n->ln:0); |
| 400 | LastGoto = 0; |
| 401 | } |
| 402 | } |
| 403 | if (e == last) |
| 404 | { if (!LastGoto && next) |
| 405 | { fprintf(fd, "\t\tgoto S_%.3d_0;\n", |
| 406 | next->Seqno); |
| 407 | Dested(next->Seqno); |
| 408 | } |
| 409 | break; |
| 410 | } } |
| 411 | } |