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[12]; 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 } 412