1 /***** spin: run.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 extern Symbol *Fname; 17 extern Element *LastStep; 18 extern int Rvous, lineno, Tval, Interactive, SubChoice; 19 extern int TstOnly, verbose, s_trail, xspin; 20 21 static long Seed=1; 22 23 void 24 Srand(unsigned int s) 25 { Seed = s; 26 } 27 28 long 29 Rand(void) 30 { /* CACM 31(10), Oct 1988 */ 31 Seed = 16807*(Seed%127773) - 2836*(Seed/127773); 32 if (Seed <= 0) Seed += 2147483647; 33 return Seed; 34 } 35 36 Element * 37 eval_sub(Element *e) 38 { Element *f, *g; 39 SeqList *z; 40 int i, j, k; 41 42 if (!e->n) 43 return ZE; 44 #ifdef DEBUG 45 printf("eval_sub(%d) ", e->Seqno); 46 comment(stdout, e->n, 0); 47 printf("\n"); 48 #endif 49 if (e->n->ntyp == GOTO) 50 { if (Rvous) return ZE; 51 f = get_lab(e->n, 1); 52 cross_dsteps(e->n, f->n); 53 return f; 54 } 55 if (e->n->ntyp == UNLESS) 56 { /* escapes were distributed into sequence */ 57 return eval_sub(e->sub->this->frst); 58 } else if (e->sub) /* true for IF, DO, and UNLESS */ 59 { Element *has_else = ZE; 60 61 if (Interactive && !SubChoice) 62 { printf("Select stmnt ("); 63 whoruns(0); printf(")\n"); 64 printf("\tchoice 0: other process\n"); 65 } 66 for (z = e->sub, j=0; z; z = z->nxt) 67 { j++; 68 if (Interactive 69 && !SubChoice 70 && z->this->frst 71 && (xspin || Enabled0(z->this->frst))) 72 { printf("\tchoice %d: ", j); 73 if (!Enabled0(z->this->frst)) 74 printf("unexecutable, "); 75 comment(stdout, z->this->frst->n, 0); 76 printf("\n"); 77 } } 78 if (Interactive) 79 { if (!SubChoice) 80 { if (xspin) 81 printf("Make Selection %d\n\n", j); 82 else 83 printf("Select [0-%d]: ", j); 84 fflush(stdout); 85 scanf("%d", &k); 86 } else 87 { k = SubChoice; 88 SubChoice = 0; 89 } 90 if (k < 1 || k > j) 91 { printf("\tchoice outside range\n"); 92 return ZE; 93 } 94 k--; 95 } else 96 k = Rand()%j; /* nondeterminism */ 97 for (i = 0, z = e->sub; i < j+k; i++) 98 { if (z->this->frst 99 && z->this->frst->n->ntyp == ELSE) 100 { has_else = z->this->frst->nxt; 101 if (!Interactive) 102 { z = (z->nxt)?z->nxt:e->sub; 103 continue; 104 } } 105 if (i >= k) 106 { if (f = eval_sub(z->this->frst)) 107 return f; 108 else if (Interactive) 109 { printf("\tunexecutable\n"); 110 return ZE; 111 } } 112 z = (z->nxt)?z->nxt:e->sub; 113 } 114 LastStep = z->this->frst; 115 return has_else; 116 } else 117 { if (e->n->ntyp == ATOMIC 118 || e->n->ntyp == D_STEP) 119 { f = e->n->sl->this->frst; 120 g = e->n->sl->this->last; 121 g->nxt = e->nxt; 122 if (!(g = eval_sub(f))) /* atomic guard */ 123 return ZE; 124 /* new implementation of atomic sequences */ 125 return g; 126 } else if (e->n->ntyp == NON_ATOMIC) 127 { f = e->n->sl->this->frst; 128 g = e->n->sl->this->last; 129 g->nxt = e->nxt; /* close it */ 130 return eval_sub(f); 131 } else if (Rvous) 132 { if (eval_sync(e)) 133 return e->nxt; 134 } else if (e->n->ntyp == '.') 135 { return e->nxt; 136 } else 137 { SeqList *x; 138 if (e->esc && verbose&32) 139 { printf("Statement ["); 140 comment(stdout, e->n, 0); 141 printf("] - can be escaped by\n"); 142 for (x = e->esc; x; x = x->nxt) 143 { printf("\t["); 144 comment(stdout, x->this->frst->n, 0); 145 printf("]\n"); 146 } } 147 for (x = e->esc; x; x = x->nxt) 148 { if (g = eval_sub(x->this->frst)) 149 { if (verbose&4) 150 printf("\tEscape taken\n"); 151 return g; 152 } } 153 switch (e->n->ntyp) { 154 case TIMEOUT: case RUN: 155 case PRINT: case ASGN: case ASSERT: 156 case 's': case 'r': case 'c': 157 /* toplevel statements only */ 158 LastStep = e; 159 default: 160 break; 161 } 162 return (eval(e->n))?e->nxt:ZE; 163 } 164 } 165 return ZE; 166 } 167 168 int 169 eval_sync(Element *e) 170 { /* allow only synchronous receives 171 /* and related node types */ 172 Lextok *now = (e)?e->n:ZN; 173 174 if (!now 175 || now->ntyp != 'r' 176 || !q_is_sync(now)) 177 return 0; 178 179 LastStep = e; 180 return eval(now); 181 } 182 183 int 184 assign(Lextok *now) 185 { int t; 186 187 if (TstOnly) return 1; 188 189 switch (now->rgt->ntyp) { 190 case FULL: case NFULL: 191 case EMPTY: case NEMPTY: 192 case RUN: case LEN: 193 t = BYTE; 194 break; 195 default: 196 t = Sym_typ(now->rgt); 197 break; 198 } 199 typ_ck(Sym_typ(now->lft), t, "assignment"); 200 return setval(now->lft, eval(now->rgt)); 201 } 202 203 int 204 eval(Lextok *now) 205 { 206 if (now) { 207 lineno = now->ln; 208 Fname = now->fn; 209 #ifdef DEBUG 210 printf("eval "); 211 comment(stdout, now, 0); 212 printf("\n"); 213 #endif 214 switch (now->ntyp) { 215 case CONST: return now->val; 216 case '!': return !eval(now->lft); 217 case UMIN: return -eval(now->lft); 218 case '~': return ~eval(now->lft); 219 220 case '/': return (eval(now->lft) / eval(now->rgt)); 221 case '*': return (eval(now->lft) * eval(now->rgt)); 222 case '-': return (eval(now->lft) - eval(now->rgt)); 223 case '+': return (eval(now->lft) + eval(now->rgt)); 224 case '%': return (eval(now->lft) % eval(now->rgt)); 225 case LT: return (eval(now->lft) < eval(now->rgt)); 226 case GT: return (eval(now->lft) > eval(now->rgt)); 227 case '&': return (eval(now->lft) & eval(now->rgt)); 228 case '|': return (eval(now->lft) | eval(now->rgt)); 229 case LE: return (eval(now->lft) <= eval(now->rgt)); 230 case GE: return (eval(now->lft) >= eval(now->rgt)); 231 case NE: return (eval(now->lft) != eval(now->rgt)); 232 case EQ: return (eval(now->lft) == eval(now->rgt)); 233 case OR: return (eval(now->lft) || eval(now->rgt)); 234 case AND: return (eval(now->lft) && eval(now->rgt)); 235 case LSHIFT: return (eval(now->lft) << eval(now->rgt)); 236 case RSHIFT: return (eval(now->lft) >> eval(now->rgt)); 237 case '?': return (eval(now->lft) ? eval(now->rgt->lft) 238 : eval(now->rgt->rgt)); 239 240 case 'p': return remotevar(now); /* only _p allowed */ 241 case 'q': return remotelab(now); 242 case 'R': return qrecv(now, 0); /* test only */ 243 case LEN: return qlen(now); 244 case FULL: return (qfull(now)); 245 case EMPTY: return (qlen(now)==0); 246 case NFULL: return (!qfull(now)); 247 case NEMPTY: return (qlen(now)>0); 248 case ENABLED: return 1; /* can only be hit with -t option*/ 249 case PC_VAL: return pc_value(now->lft); 250 case NAME: return getval(now); 251 252 case TIMEOUT: return Tval; 253 case RUN: return TstOnly?1:enable(now->sym, now->lft); 254 255 case 's': return qsend(now); /* send */ 256 case 'r': return qrecv(now, 1); /* full-receive */ 257 case 'c': return eval(now->lft); /* condition */ 258 case PRINT: return TstOnly?1:interprint(now); 259 case ASGN: return assign(now); 260 case ASSERT: if (TstOnly || eval(now->lft)) return 1; 261 non_fatal("assertion violated", (char *) 0); 262 if (s_trail) return 1; /* else */ 263 wrapup(1); /* doesn't return */ 264 265 case IF: case DO: case BREAK: case UNLESS: /* compound structure */ 266 case '.': return 1; /* return label for compound */ 267 case '@': return 0; /* stop state */ 268 case ELSE: return 1; /* only hit here in guided trails */ 269 default : printf("spin: bad node type %d (run)\n", now->ntyp); 270 fatal("aborting", 0); 271 }} 272 return 0; 273 } 274 275 int 276 interprint(Lextok *n) 277 { Lextok *tmp = n->lft; 278 char c, *s = n->sym->name; 279 int i, j; 280 281 for (i = 0; i < strlen(s); i++) 282 switch (s[i]) { 283 default: putchar(s[i]); break; 284 case '\"': break; /* ignore */ 285 case '\\': 286 switch(s[++i]) { 287 case 't': putchar('\t'); break; 288 case 'n': putchar('\n'); break; 289 default: putchar(s[i]); break; 290 } 291 break; 292 case '%': 293 if ((c = s[++i]) == '%') 294 { putchar('%'); /* literal */ 295 break; 296 } 297 if (!tmp) 298 { non_fatal("too few print args %s", s); 299 break; 300 } 301 j = eval(tmp->lft); 302 tmp = tmp->rgt; 303 switch(c) { 304 case 'c': printf("%c", j); break; 305 case 'd': printf("%d", j); break; 306 case 'o': printf("%o", j); break; 307 case 'u': printf("%u", (unsigned) j); break; 308 case 'x': printf("%x", j); break; 309 default: non_fatal("unrecognized print cmd: '%s'", &s[i-1]); 310 break; 311 } 312 break; 313 } 314 fflush(stdout); 315 return 1; 316 } 317 318 /* new */ 319 320 int 321 Enabled1(Lextok *n) 322 { int i; int v = verbose; 323 324 if (n) 325 switch (n->ntyp) { 326 default: /* side-effect free */ 327 verbose = 0; 328 i = eval(n); 329 verbose = v; 330 return i; 331 332 case PRINT: case ASGN: 333 case ASSERT: case RUN: 334 return 1; 335 336 case 's': /* guesses for rv */ 337 if (q_is_sync(n)) return !Rvous; 338 return (!qfull(n)); 339 case 'r': /* guesses for rv */ 340 if (q_is_sync(n)) return Rvous; 341 n->ntyp = 'R'; verbose = 0; 342 i = eval(n); 343 n->ntyp = 'r'; verbose = v; 344 return i; 345 } 346 return 0; 347 } 348 349 int 350 Enabled0(Element *e) 351 { SeqList *z; 352 353 if (!e || !e->n) 354 return 0; 355 356 switch (e->n->ntyp) { 357 case '.': 358 return 1; 359 case GOTO: 360 if (Rvous) return 0; 361 return 1; 362 case UNLESS: 363 return Enabled0(e->sub->this->frst); 364 case ATOMIC: 365 case D_STEP: 366 case NON_ATOMIC: 367 return Enabled0(e->n->sl->this->frst); 368 } 369 if (e->sub) /* true for IF, DO, and UNLESS */ 370 { for (z = e->sub; z; z = z->nxt) 371 if (Enabled0(z->this->frst)) 372 return 1; 373 return 0; 374 } 375 for (z = e->esc; z; z = z->nxt) 376 { if (Enabled0(z->this->frst)) 377 return 1; 378 } 379 return Enabled1(e->n); 380 } 381