0b55f123 |
1 | /***** spin: run.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 <stdlib.h> |
13 | #include "spin.h" |
14 | #include "y.tab.h" |
15 | |
16 | extern RunList *X, *run; |
17 | extern Symbol *Fname; |
18 | extern Element *LastStep; |
19 | extern int Rvous, lineno, Tval, interactive, MadeChoice; |
20 | extern int TstOnly, verbose, s_trail, xspin, jumpsteps, depth; |
21 | extern int nproc, nstop, no_print, like_java; |
22 | |
23 | static long Seed = 1; |
24 | static int E_Check = 0, Escape_Check = 0; |
25 | |
26 | static int eval_sync(Element *); |
27 | static int pc_enabled(Lextok *n); |
28 | extern void sr_buf(int, int); |
29 | |
30 | void |
31 | Srand(unsigned int s) |
32 | { Seed = s; |
33 | } |
34 | |
35 | long |
36 | Rand(void) |
37 | { /* CACM 31(10), Oct 1988 */ |
38 | Seed = 16807*(Seed%127773) - 2836*(Seed/127773); |
39 | if (Seed <= 0) Seed += 2147483647; |
40 | return Seed; |
41 | } |
42 | |
43 | Element * |
44 | rev_escape(SeqList *e) |
45 | { Element *r; |
46 | |
47 | if (!e) |
48 | return (Element *) 0; |
49 | |
50 | if ((r = rev_escape(e->nxt)) != ZE) /* reversed order */ |
51 | return r; |
52 | |
53 | return eval_sub(e->this->frst); |
54 | } |
55 | |
56 | Element * |
57 | eval_sub(Element *e) |
58 | { Element *f, *g; |
59 | SeqList *z; |
60 | int i, j, k; |
61 | |
62 | if (!e || !e->n) |
63 | return ZE; |
64 | #ifdef DEBUG |
65 | printf("\n\teval_sub(%d %s: line %d) ", |
66 | e->Seqno, e->esc?"+esc":"", e->n?e->n->ln:0); |
67 | comment(stdout, e->n, 0); |
68 | printf("\n"); |
69 | #endif |
70 | if (e->n->ntyp == GOTO) |
71 | { if (Rvous) return ZE; |
72 | LastStep = e; |
73 | f = get_lab(e->n, 1); |
74 | cross_dsteps(e->n, f->n); |
75 | return f; |
76 | } |
77 | if (e->n->ntyp == UNLESS) |
78 | { /* escapes were distributed into sequence */ |
79 | return eval_sub(e->sub->this->frst); |
80 | } else if (e->sub) /* true for IF, DO, and UNLESS */ |
81 | { Element *has_else = ZE; |
82 | Element *bas_else = ZE; |
83 | int nr_else = 0, nr_choices = 0; |
84 | |
85 | if (interactive |
86 | && !MadeChoice && !E_Check |
87 | && !Escape_Check |
88 | && !(e->status&(D_ATOM)) |
89 | && depth >= jumpsteps) |
90 | { printf("Select stmnt ("); |
91 | whoruns(0); printf(")\n"); |
92 | if (nproc-nstop > 1) |
93 | printf("\tchoice 0: other process\n"); |
94 | } |
95 | for (z = e->sub, j=0; z; z = z->nxt) |
96 | { j++; |
97 | if (interactive |
98 | && !MadeChoice && !E_Check |
99 | && !Escape_Check |
100 | && !(e->status&(D_ATOM)) |
101 | && depth >= jumpsteps |
102 | && z->this->frst |
103 | && (xspin || (verbose&32) || Enabled0(z->this->frst))) |
104 | { if (z->this->frst->n->ntyp == ELSE) |
105 | { has_else = (Rvous)?ZE:z->this->frst->nxt; |
106 | nr_else = j; |
107 | continue; |
108 | } |
109 | printf("\tchoice %d: ", j); |
110 | #if 0 |
111 | if (z->this->frst->n) |
112 | printf("line %d, ", z->this->frst->n->ln); |
113 | #endif |
114 | if (!Enabled0(z->this->frst)) |
115 | printf("unexecutable, "); |
116 | else |
117 | nr_choices++; |
118 | comment(stdout, z->this->frst->n, 0); |
119 | printf("\n"); |
120 | } } |
121 | |
122 | if (nr_choices == 0 && has_else) |
123 | printf("\tchoice %d: (else)\n", nr_else); |
124 | |
125 | if (interactive && depth >= jumpsteps |
126 | && !Escape_Check |
127 | && !(e->status&(D_ATOM)) |
128 | && !E_Check) |
129 | { if (!MadeChoice) |
130 | { char buf[256]; |
131 | if (xspin) |
132 | printf("Make Selection %d\n\n", j); |
133 | else |
134 | printf("Select [0-%d]: ", j); |
135 | fflush(stdout); |
136 | scanf("%64s", buf); |
137 | if (isdigit(buf[0])) |
138 | k = atoi(buf); |
139 | else |
140 | { if (buf[0] == 'q') |
141 | alldone(0); |
142 | k = -1; |
143 | } |
144 | } else |
145 | { k = MadeChoice; |
146 | MadeChoice = 0; |
147 | } |
148 | if (k < 1 || k > j) |
149 | { if (k != 0) printf("\tchoice outside range\n"); |
150 | return ZE; |
151 | } |
152 | k--; |
153 | } else |
154 | { if (e->n && e->n->indstep >= 0) |
155 | k = 0; /* select 1st executable guard */ |
156 | else |
157 | k = Rand()%j; /* nondeterminism */ |
158 | } |
159 | has_else = ZE; |
160 | bas_else = ZE; |
161 | for (i = 0, z = e->sub; i < j+k; i++) |
162 | { if (z->this->frst |
163 | && z->this->frst->n->ntyp == ELSE) |
164 | { bas_else = z->this->frst; |
165 | has_else = (Rvous)?ZE:bas_else->nxt; |
166 | if (!interactive || depth < jumpsteps |
167 | || Escape_Check |
168 | || (e->status&(D_ATOM))) |
169 | { z = (z->nxt)?z->nxt:e->sub; |
170 | continue; |
171 | } |
172 | } |
173 | if (z->this->frst |
174 | && ((z->this->frst->n->ntyp == ATOMIC |
175 | || z->this->frst->n->ntyp == D_STEP) |
176 | && z->this->frst->n->sl->this->frst->n->ntyp == ELSE)) |
177 | { bas_else = z->this->frst->n->sl->this->frst; |
178 | has_else = (Rvous)?ZE:bas_else->nxt; |
179 | if (!interactive || depth < jumpsteps |
180 | || Escape_Check |
181 | || (e->status&(D_ATOM))) |
182 | { z = (z->nxt)?z->nxt:e->sub; |
183 | continue; |
184 | } |
185 | } |
186 | if (i >= k) |
187 | { if ((f = eval_sub(z->this->frst)) != ZE) |
188 | return f; |
189 | else if (interactive && depth >= jumpsteps |
190 | && !(e->status&(D_ATOM))) |
191 | { if (!E_Check && !Escape_Check) |
192 | printf("\tunexecutable\n"); |
193 | return ZE; |
194 | } } |
195 | z = (z->nxt)?z->nxt:e->sub; |
196 | } |
197 | LastStep = bas_else; |
198 | return has_else; |
199 | } else |
200 | { if (e->n->ntyp == ATOMIC |
201 | || e->n->ntyp == D_STEP) |
202 | { f = e->n->sl->this->frst; |
203 | g = e->n->sl->this->last; |
204 | g->nxt = e->nxt; |
205 | if (!(g = eval_sub(f))) /* atomic guard */ |
206 | return ZE; |
207 | return g; |
208 | } else if (e->n->ntyp == NON_ATOMIC) |
209 | { f = e->n->sl->this->frst; |
210 | g = e->n->sl->this->last; |
211 | g->nxt = e->nxt; /* close it */ |
212 | return eval_sub(f); |
213 | } else if (e->n->ntyp == '.') |
214 | { if (!Rvous) return e->nxt; |
215 | return eval_sub(e->nxt); |
216 | } else |
217 | { SeqList *x; |
218 | if (!(e->status & (D_ATOM)) |
219 | && e->esc && verbose&32) |
220 | { printf("Stmnt ["); |
221 | comment(stdout, e->n, 0); |
222 | printf("] has escape(s): "); |
223 | for (x = e->esc; x; x = x->nxt) |
224 | { printf("["); |
225 | g = x->this->frst; |
226 | if (g->n->ntyp == ATOMIC |
227 | || g->n->ntyp == NON_ATOMIC) |
228 | g = g->n->sl->this->frst; |
229 | comment(stdout, g->n, 0); |
230 | printf("] "); |
231 | } |
232 | printf("\n"); |
233 | } |
234 | #if 0 |
235 | if (!(e->status & D_ATOM)) /* escapes don't reach inside d_steps */ |
236 | /* 4.2.4: only the guard of a d_step can have an escape */ |
237 | #endif |
238 | { Escape_Check++; |
239 | if (like_java) |
240 | { if ((g = rev_escape(e->esc)) != ZE) |
241 | { if (verbose&4) |
242 | printf("\tEscape taken\n"); |
243 | Escape_Check--; |
244 | return g; |
245 | } |
246 | } else |
247 | { for (x = e->esc; x; x = x->nxt) |
248 | { if ((g = eval_sub(x->this->frst)) != ZE) |
249 | { if (verbose&4) |
250 | printf("\tEscape taken\n"); |
251 | Escape_Check--; |
252 | return g; |
253 | } } } |
254 | Escape_Check--; |
255 | } |
256 | |
257 | switch (e->n->ntyp) { |
258 | case TIMEOUT: case RUN: |
259 | case PRINT: case PRINTM: |
260 | case C_CODE: case C_EXPR: |
261 | case ASGN: case ASSERT: |
262 | case 's': case 'r': case 'c': |
263 | /* toplevel statements only */ |
264 | LastStep = e; |
265 | default: |
266 | break; |
267 | } |
268 | if (Rvous) |
269 | { |
270 | return (eval_sync(e))?e->nxt:ZE; |
271 | } |
272 | return (eval(e->n))?e->nxt:ZE; |
273 | } |
274 | } |
275 | return ZE; /* not reached */ |
276 | } |
277 | |
278 | static int |
279 | eval_sync(Element *e) |
280 | { /* allow only synchronous receives |
281 | and related node types */ |
282 | Lextok *now = (e)?e->n:ZN; |
283 | |
284 | if (!now |
285 | || now->ntyp != 'r' |
286 | || now->val >= 2 /* no rv with a poll */ |
287 | || !q_is_sync(now)) |
288 | { |
289 | return 0; |
290 | } |
291 | |
292 | LastStep = e; |
293 | return eval(now); |
294 | } |
295 | |
296 | static int |
297 | assign(Lextok *now) |
298 | { int t; |
299 | |
300 | if (TstOnly) return 1; |
301 | |
302 | switch (now->rgt->ntyp) { |
303 | case FULL: case NFULL: |
304 | case EMPTY: case NEMPTY: |
305 | case RUN: case LEN: |
306 | t = BYTE; |
307 | break; |
308 | default: |
309 | t = Sym_typ(now->rgt); |
310 | break; |
311 | } |
312 | typ_ck(Sym_typ(now->lft), t, "assignment"); |
313 | return setval(now->lft, eval(now->rgt)); |
314 | } |
315 | |
316 | static int |
317 | nonprogress(void) /* np_ */ |
318 | { RunList *r; |
319 | |
320 | for (r = run; r; r = r->nxt) |
321 | { if (has_lab(r->pc, 4)) /* 4=progress */ |
322 | return 0; |
323 | } |
324 | return 1; |
325 | } |
326 | |
327 | int |
328 | eval(Lextok *now) |
329 | { |
330 | if (now) { |
331 | lineno = now->ln; |
332 | Fname = now->fn; |
333 | #ifdef DEBUG |
334 | printf("eval "); |
335 | comment(stdout, now, 0); |
336 | printf("\n"); |
337 | #endif |
338 | switch (now->ntyp) { |
339 | case CONST: return now->val; |
340 | case '!': return !eval(now->lft); |
341 | case UMIN: return -eval(now->lft); |
342 | case '~': return ~eval(now->lft); |
343 | |
344 | case '/': return (eval(now->lft) / eval(now->rgt)); |
345 | case '*': return (eval(now->lft) * eval(now->rgt)); |
346 | case '-': return (eval(now->lft) - eval(now->rgt)); |
347 | case '+': return (eval(now->lft) + eval(now->rgt)); |
348 | case '%': return (eval(now->lft) % eval(now->rgt)); |
349 | case LT: return (eval(now->lft) < eval(now->rgt)); |
350 | case GT: return (eval(now->lft) > eval(now->rgt)); |
351 | case '&': return (eval(now->lft) & eval(now->rgt)); |
352 | case '^': return (eval(now->lft) ^ eval(now->rgt)); |
353 | case '|': return (eval(now->lft) | eval(now->rgt)); |
354 | case LE: return (eval(now->lft) <= eval(now->rgt)); |
355 | case GE: return (eval(now->lft) >= eval(now->rgt)); |
356 | case NE: return (eval(now->lft) != eval(now->rgt)); |
357 | case EQ: return (eval(now->lft) == eval(now->rgt)); |
358 | case OR: return (eval(now->lft) || eval(now->rgt)); |
359 | case AND: return (eval(now->lft) && eval(now->rgt)); |
360 | case LSHIFT: return (eval(now->lft) << eval(now->rgt)); |
361 | case RSHIFT: return (eval(now->lft) >> eval(now->rgt)); |
362 | case '?': return (eval(now->lft) ? eval(now->rgt->lft) |
363 | : eval(now->rgt->rgt)); |
364 | |
365 | case 'p': return remotevar(now); /* _p for remote reference */ |
366 | case 'q': return remotelab(now); |
367 | case 'R': return qrecv(now, 0); /* test only */ |
368 | case LEN: return qlen(now); |
369 | case FULL: return (qfull(now)); |
370 | case EMPTY: return (qlen(now)==0); |
371 | case NFULL: return (!qfull(now)); |
372 | case NEMPTY: return (qlen(now)>0); |
373 | case ENABLED: if (s_trail) return 1; |
374 | return pc_enabled(now->lft); |
375 | case EVAL: return eval(now->lft); |
376 | case PC_VAL: return pc_value(now->lft); |
377 | case NONPROGRESS: return nonprogress(); |
378 | case NAME: return getval(now); |
379 | |
380 | case TIMEOUT: return Tval; |
381 | case RUN: return TstOnly?1:enable(now); |
382 | |
383 | case 's': return qsend(now); /* send */ |
384 | case 'r': return qrecv(now, 1); /* receive or poll */ |
385 | case 'c': return eval(now->lft); /* condition */ |
386 | case PRINT: return TstOnly?1:interprint(stdout, now); |
387 | case PRINTM: return TstOnly?1:printm(stdout, now); |
388 | case ASGN: return assign(now); |
389 | |
390 | case C_CODE: printf("%s:\t", now->sym->name); |
391 | plunk_inline(stdout, now->sym->name, 0); |
392 | return 1; /* uninterpreted */ |
393 | |
394 | case C_EXPR: printf("%s:\t", now->sym->name); |
395 | plunk_expr(stdout, now->sym->name); |
396 | printf("\n"); |
397 | return 1; /* uninterpreted */ |
398 | |
399 | case ASSERT: if (TstOnly || eval(now->lft)) return 1; |
400 | non_fatal("assertion violated", (char *) 0); |
401 | printf("spin: text of failed assertion: assert("); |
402 | comment(stdout, now->lft, 0); |
403 | printf(")\n"); |
404 | if (s_trail && !xspin) return 1; |
405 | wrapup(1); /* doesn't return */ |
406 | |
407 | case IF: case DO: case BREAK: case UNLESS: /* compound */ |
408 | case '.': return 1; /* return label for compound */ |
409 | case '@': return 0; /* stop state */ |
410 | case ELSE: return 1; /* only hit here in guided trails */ |
411 | default : printf("spin: bad node type %d (run)\n", now->ntyp); |
412 | if (s_trail) printf("spin: trail file doesn't match spec?\n"); |
413 | fatal("aborting", 0); |
414 | }} |
415 | return 0; |
416 | } |
417 | |
418 | int |
419 | printm(FILE *fd, Lextok *n) |
420 | { extern char Buf[]; |
421 | int j; |
422 | |
423 | Buf[0] = '\0'; |
424 | if (!no_print) |
425 | if (!s_trail || depth >= jumpsteps) { |
426 | if (n->lft->ismtyp) |
427 | j = n->lft->val; |
428 | else |
429 | j = eval(n->lft); |
430 | sr_buf(j, 1); |
431 | dotag(fd, Buf); |
432 | } |
433 | return 1; |
434 | } |
435 | |
436 | int |
437 | interprint(FILE *fd, Lextok *n) |
438 | { Lextok *tmp = n->lft; |
439 | char c, *s = n->sym->name; |
440 | int i, j; char lbuf[512]; /* matches value in sr_buf() */ |
441 | extern char Buf[]; /* global, size 4096 */ |
442 | char tBuf[4096]; /* match size of global Buf[] */ |
443 | |
444 | Buf[0] = '\0'; |
445 | if (!no_print) |
446 | if (!s_trail || depth >= jumpsteps) { |
447 | for (i = 0; i < (int) strlen(s); i++) |
448 | switch (s[i]) { |
449 | case '\"': break; /* ignore */ |
450 | case '\\': |
451 | switch(s[++i]) { |
452 | case 't': strcat(Buf, "\t"); break; |
453 | case 'n': strcat(Buf, "\n"); break; |
454 | default: goto onechar; |
455 | } |
456 | break; |
457 | case '%': |
458 | if ((c = s[++i]) == '%') |
459 | { strcat(Buf, "%"); /* literal */ |
460 | break; |
461 | } |
462 | if (!tmp) |
463 | { non_fatal("too few print args %s", s); |
464 | break; |
465 | } |
466 | j = eval(tmp->lft); |
467 | tmp = tmp->rgt; |
468 | switch(c) { |
469 | case 'c': sprintf(lbuf, "%c", j); break; |
470 | case 'd': sprintf(lbuf, "%d", j); break; |
471 | |
472 | case 'e': strcpy(tBuf, Buf); /* event name */ |
473 | Buf[0] = '\0'; |
474 | sr_buf(j, 1); |
475 | strcpy(lbuf, Buf); |
476 | strcpy(Buf, tBuf); |
477 | break; |
478 | |
479 | case 'o': sprintf(lbuf, "%o", j); break; |
480 | case 'u': sprintf(lbuf, "%u", (unsigned) j); break; |
481 | case 'x': sprintf(lbuf, "%x", j); break; |
482 | default: non_fatal("bad print cmd: '%s'", &s[i-1]); |
483 | lbuf[0] = '\0'; break; |
484 | } |
485 | goto append; |
486 | default: |
487 | onechar: lbuf[0] = s[i]; lbuf[1] = '\0'; |
488 | append: strcat(Buf, lbuf); |
489 | break; |
490 | } |
491 | dotag(fd, Buf); |
492 | } |
493 | if (strlen(Buf) >= 4096) fatal("printf string too long", 0); |
494 | return 1; |
495 | } |
496 | |
497 | static int |
498 | Enabled1(Lextok *n) |
499 | { int i; int v = verbose; |
500 | |
501 | if (n) |
502 | switch (n->ntyp) { |
503 | case 'c': |
504 | if (has_typ(n->lft, RUN)) |
505 | return 1; /* conservative */ |
506 | /* else fall through */ |
507 | default: /* side-effect free */ |
508 | verbose = 0; |
509 | E_Check++; |
510 | i = eval(n); |
511 | E_Check--; |
512 | verbose = v; |
513 | return i; |
514 | |
515 | case C_CODE: case C_EXPR: |
516 | case PRINT: case PRINTM: |
517 | case ASGN: case ASSERT: |
518 | return 1; |
519 | |
520 | case 's': |
521 | if (q_is_sync(n)) |
522 | { if (Rvous) return 0; |
523 | TstOnly = 1; verbose = 0; |
524 | E_Check++; |
525 | i = eval(n); |
526 | E_Check--; |
527 | TstOnly = 0; verbose = v; |
528 | return i; |
529 | } |
530 | return (!qfull(n)); |
531 | case 'r': |
532 | if (q_is_sync(n)) |
533 | return 0; /* it's never a user-choice */ |
534 | n->ntyp = 'R'; verbose = 0; |
535 | E_Check++; |
536 | i = eval(n); |
537 | E_Check--; |
538 | n->ntyp = 'r'; verbose = v; |
539 | return i; |
540 | } |
541 | return 0; |
542 | } |
543 | |
544 | int |
545 | Enabled0(Element *e) |
546 | { SeqList *z; |
547 | |
548 | if (!e || !e->n) |
549 | return 0; |
550 | |
551 | switch (e->n->ntyp) { |
552 | case '@': |
553 | return X->pid == (nproc-nstop-1); |
554 | case '.': |
555 | return 1; |
556 | case GOTO: |
557 | if (Rvous) return 0; |
558 | return 1; |
559 | case UNLESS: |
560 | return Enabled0(e->sub->this->frst); |
561 | case ATOMIC: |
562 | case D_STEP: |
563 | case NON_ATOMIC: |
564 | return Enabled0(e->n->sl->this->frst); |
565 | } |
566 | if (e->sub) /* true for IF, DO, and UNLESS */ |
567 | { for (z = e->sub; z; z = z->nxt) |
568 | if (Enabled0(z->this->frst)) |
569 | return 1; |
570 | return 0; |
571 | } |
572 | for (z = e->esc; z; z = z->nxt) |
573 | { if (Enabled0(z->this->frst)) |
574 | return 1; |
575 | } |
576 | #if 0 |
577 | printf("enabled1 "); |
578 | comment(stdout, e->n, 0); |
579 | printf(" ==> %s\n", Enabled1(e->n)?"yes":"nope"); |
580 | #endif |
581 | return Enabled1(e->n); |
582 | } |
583 | |
584 | int |
585 | pc_enabled(Lextok *n) |
586 | { int i = nproc - nstop; |
587 | int pid = eval(n); |
588 | int result = 0; |
589 | RunList *Y, *oX; |
590 | |
591 | if (pid == X->pid) |
592 | fatal("used: enabled(pid=thisproc) [%s]", X->n->name); |
593 | |
594 | for (Y = run; Y; Y = Y->nxt) |
595 | if (--i == pid) |
596 | { oX = X; X = Y; |
597 | result = Enabled0(Y->pc); |
598 | X = oX; |
599 | break; |
600 | } |
601 | return result; |
602 | } |