xref: /plan9/sys/src/cmd/spin/run.c (revision 00d970127b9d44d2b22f4f656717a212dec1f1d2)
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