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