1 /***** spin: dstep.c *****/ 2 3 /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */ 4 /* 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.att.com */ 12 13 #include "spin.h" 14 #include "y.tab.h" 15 16 char *NextLab[64]; 17 int Level=0, GenCode=0, IsGuard=0, TestOnly=0; 18 int Tj=0, Jt=0, LastGoto=0; 19 int Tojump[512], Jumpto[512], Special[512]; 20 21 void 22 Sourced(int n, int special) 23 { int i; 24 for (i = 0; i < Tj; i++) 25 if (Tojump[i] == n) 26 return; 27 Special[Tj] = special; 28 Tojump[Tj++] = n; 29 } 30 31 void 32 Dested(int n) 33 { int i; 34 35 LastGoto = 1; 36 for (i = 0; i < Tj; i++) 37 if (Tojump[i] == n) 38 return; 39 for (i = 0; i < Jt; i++) 40 if (Jumpto[i] == n) 41 return; 42 Jumpto[Jt++] = n; 43 } 44 45 void 46 Mopup(FILE *fd) 47 { int i, j; 48 for (i = 0; i < Jt; i++) 49 { for (j = 0; j < Tj; j++) 50 { if (Tojump[j] == Jumpto[i]) 51 break; 52 } 53 if (j == Tj) 54 { char buf[12]; 55 sprintf(buf, "S_%.3d_0", Jumpto[i]); 56 non_fatal("goto %s breaks from d_step seq", buf); 57 } } 58 for (j = 0; j < Tj; j++) 59 { for (i = 0; i < Jt; i++) 60 { if (Tojump[j] == Jumpto[i]) 61 break; 62 } 63 #ifdef DEBUG 64 if (i == Jt && !Special[i]) 65 { fprintf(fd, "\t\t/* >>no goto's for S_%.3d_0<< */\n", 66 Tojump[j]); 67 } 68 #endif 69 } 70 for (j = i = 0; j < Tj; j++) 71 { if (Special[j]) 72 { Tojump[i] = Tojump[j]; 73 Special[i] = 2; 74 i++; 75 } } 76 Tj = i; /* keep only the global exit-labels */ 77 Jt = 0; 78 } 79 80 int 81 FirstTime(int n) 82 { int i; 83 for (i = 0; i < Tj; i++) 84 if (Tojump[i] == n) 85 return (Special[i] <= 1); 86 return 1; 87 } 88 89 void 90 illegal(Element *e, char *str) 91 { 92 printf("illegal operator in 'step:' '"); 93 comment(stdout, e->n, 0); 94 printf("'\n"); 95 fatal("saw %s", str); 96 } 97 98 void 99 filterbad(Element *e) 100 { 101 switch (e->n->ntyp) { 102 case ASSERT: 103 case PRINT: 104 case 'c': 105 /* run cannot be completely undone 106 * with sv_save-sv_restor 107 */ 108 if (any_oper(e->n->lft, RUN)) 109 illegal(e, "run operator"); 110 break; 111 case '@': 112 illegal(e, "process termination"); 113 break; 114 case D_STEP: 115 illegal(e, "nested d_step sequence"); 116 break; 117 case ATOMIC: 118 illegal(e, "nested atomic sequence"); 119 break; 120 default: 121 break; 122 } 123 } 124 125 int 126 CollectGuards(FILE *fd, Element *e, int inh) 127 { SeqList *h; Element *ee; 128 129 for (h = e->sub; h; h = h->nxt) 130 { ee = huntstart(h->this->frst); 131 filterbad(ee); 132 switch (ee->n->ntyp) { 133 case IF: 134 inh += CollectGuards(fd, ee, inh); 135 break; 136 case '.': 137 if (ee->nxt->n->ntyp == DO) 138 inh += CollectGuards(fd, ee->nxt, inh); 139 break; 140 case ELSE: 141 if (inh++ > 0) fprintf(fd, " || "); 142 fprintf(fd, "(1 /* else */)"); 143 break; 144 case 'c': 145 if (inh++ > 0) fprintf(fd, " || "); 146 fprintf(fd, "("); TestOnly=1; 147 putstmnt(fd, ee->n->lft, e->seqno); 148 fprintf(fd, ")"); TestOnly=0; 149 break; 150 } 151 } 152 return inh; 153 } 154 155 int 156 putcode(FILE *fd, Sequence *s, Element *nxt, int justguards) 157 { int isg=0; 158 159 NextLab[0] = "continue"; 160 161 filterbad(s->frst); 162 163 switch (s->frst->n->ntyp) { 164 case UNLESS: 165 non_fatal("'unless' inside d_step - ignored", (char *) 0); 166 return putcode(fd, s->frst->n->sl->this, nxt, 0); 167 case NON_ATOMIC: 168 (void) putcode(fd, s->frst->n->sl->this, ZE, 1); 169 break; 170 case IF: 171 fprintf(fd, "if (!("); 172 if (!CollectGuards(fd, s->frst, 0)) 173 fprintf(fd, "1"); 174 fprintf(fd, "))\n\t\t\tcontinue;"); 175 isg = 1; 176 break; 177 case '.': 178 if (s->frst->nxt->n->ntyp == DO) 179 { fprintf(fd, "if (!("); 180 if (!CollectGuards(fd, s->frst->nxt, 0)) 181 fprintf(fd, "1"); 182 fprintf(fd, "))\n\t\t\tcontinue;"); 183 isg = 1; 184 } 185 break; 186 case 'R': 187 case 'r': 188 case 's': 189 fprintf(fd, "if (!("); TestOnly=1; 190 putstmnt(fd, s->frst->n, s->frst->seqno); 191 fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0; 192 break; 193 case 'c': 194 fprintf(fd, "if (!("); TestOnly=1; 195 putstmnt(fd, s->frst->n->lft, s->frst->seqno); 196 fprintf(fd, "))\n\t\t\tcontinue;"); TestOnly=0; 197 break; 198 } 199 if (justguards) return 0; 200 201 fprintf(fd, "\n#if defined(FULLSTACK) && defined(NOCOMP)\n"); 202 fprintf(fd, "\t\tif (t->atom&2)\n"); 203 fprintf(fd, "#endif\n"); 204 fprintf(fd, "\t\tsv_save((char *)&now);\n"); 205 putCode(fd, s->frst, s->extent, nxt, isg); 206 207 if (nxt) 208 { if (FirstTime(nxt->Seqno) 209 && (!(nxt->status & DONE2) || !(nxt->status & D_ATOM))) 210 { fprintf(fd, "S_%.3d_0: /* 1 */\n", nxt->Seqno); 211 nxt->status |= DONE2; 212 LastGoto = 0; 213 } 214 Sourced(nxt->Seqno, 1); 215 Mopup(fd); 216 } 217 unskip(s->frst->seqno); 218 return LastGoto; 219 } 220 221 void 222 putCode(FILE *fd, Element *f, Element *last, Element *next, int isguard) 223 { Element *e, *N; 224 SeqList *h; int i; 225 char NextOpt[32]; 226 227 for (e = f; e; e = e->nxt) 228 { if (e->status & DONE2) 229 continue; 230 e->status |= DONE2; 231 232 if (!(e->status & D_ATOM)) 233 { if (!LastGoto) 234 { fprintf(fd, "\t\tgoto S_%.3d_0;\n", e->Seqno); 235 Dested(e->Seqno); 236 } 237 break; 238 } 239 fprintf(fd, "S_%.3d_0: /* 2 */\n", e->Seqno); 240 Sourced(e->Seqno, 0); 241 242 if (!e->sub) 243 { filterbad(e); 244 switch (e->n->ntyp) { 245 case NON_ATOMIC: 246 h = e->n->sl; 247 putCode(fd, h->this->frst, h->this->extent, e->nxt, 0); 248 break; 249 case BREAK: 250 if (LastGoto) break; 251 i = target(huntele(e->nxt, e->status))->Seqno; 252 fprintf(fd, "\t\tgoto S_%.3d_0; /* 'break' */\n", i); 253 Dested(i); 254 break; 255 case GOTO: 256 if (LastGoto) break; 257 i = huntele(get_lab(e->n,1), e->status)->Seqno; 258 fprintf(fd, "\t\tgoto S_%.3d_0; /* 'goto' */\n", i); 259 Dested(i); 260 break; 261 case '.': 262 if (LastGoto) break; 263 if (e->nxt->status & DONE2) 264 { i = e->nxt?e->nxt->Seqno:0; 265 fprintf(fd, "\t\tgoto S_%.3d_0; /* '.' */\n", i); 266 Dested(i); 267 } 268 break; 269 default: 270 putskip(e->seqno); 271 GenCode = 1; IsGuard = isguard; 272 fprintf(fd, "\t\t"); 273 putstmnt(fd, e->n, e->seqno); 274 fprintf(fd, ";\n"); 275 GenCode = IsGuard = isguard = LastGoto = 0; 276 if (e->n->ntyp == ELSE) 277 LastGoto = 1; 278 break; 279 } 280 i = e->nxt?e->nxt->Seqno:0; 281 if (e->nxt && e->nxt->status & DONE2 && !LastGoto) 282 { fprintf(fd, "\t\tgoto S_%.3d_0; /* ';' */\n", i); 283 Dested(i); 284 break; 285 } 286 } else 287 { for (h = e->sub, i=1; h; h = h->nxt, i++) 288 { sprintf(NextOpt, "goto S_%.3d_%d", e->Seqno, i); 289 NextLab[++Level] = NextOpt; 290 N = (e->n->ntyp == DO) ? e : e->nxt; 291 putCode(fd, h->this->frst, h->this->extent, N, 1); 292 Level--; 293 fprintf(fd, "%s: /* 3 */\n", &NextOpt[5]); 294 } 295 if (!LastGoto) 296 { fprintf(fd, "\t\tUerror(\"blocking sel in d_step\");\n"); 297 LastGoto = 0; 298 } 299 } 300 if (e == last) 301 { if (!LastGoto && next) 302 { fprintf(fd, "\t\tgoto S_%.3d_0;\n", next->Seqno); 303 Dested(next->Seqno); 304 } 305 break; 306 } } 307 } 308