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