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