xref: /plan9-contrib/sys/src/cmd/spin/spinlex.c (revision de2caf28f9ba1a56e70be94a699435d36eb50311) 
1 /***** spin: spinlex.c *****/
2 
3 /*
4  * This file is part of the public release of Spin. It is subject to the
5  * terms in the LICENSE file that is included in this source directory.
6  * Tool documentation is available at http://spinroot.com
7  */
8 
9 #include <stdlib.h>
10 #include <assert.h>
11 #include <errno.h>
12 #include <ctype.h>
13 #include "spin.h"
14 #include "y.tab.h"
15 
16 #define MAXINL	16	/* max recursion depth inline fcts */
17 #define MAXPAR	32	/* max params to an inline call */
18 #define MAXLEN	512	/* max len of an actual parameter text */
19 
20 typedef struct IType {
21 	Symbol *nm;		/* name of the type */
22 	Lextok *cn;		/* contents */
23 	Lextok *params;		/* formal pars if any */
24 	Lextok *rval;		/* variable to assign return value, if any */
25 	char   **anms;		/* literal text for actual pars */
26 	char   *prec;		/* precondition for c_code or c_expr */
27 	int    uiid;		/* unique inline id */
28 	int    is_expr;		/* c_expr in an ltl formula */
29 	int    dln, cln;	/* def and call linenr */
30 	Symbol *dfn, *cfn;	/* def and call filename */
31 	struct IType *nxt;	/* linked list */
32 } IType;
33 
34 typedef struct C_Added {
35 	Symbol *s;
36 	Symbol *t;
37 	Symbol *ival;
38 	Symbol *fnm;
39 	int	lno;
40 	struct C_Added *nxt;
41 } C_Added;
42 
43 extern RunList	*X_lst;
44 extern ProcList	*ready;
45 extern Symbol	*Fname, *oFname;
46 extern Symbol	*context, *owner;
47 extern YYSTYPE	yylval;
48 extern short	has_last, has_code, has_priority;
49 extern int	verbose, IArgs, hastrack, separate, in_for;
50 extern int	implied_semis, ltl_mode, in_seq, par_cnt;
51 
52 short	has_stack = 0;
53 int	lineno  = 1;
54 int	scope_seq[128], scope_level = 0;
55 char	CurScope[MAXSCOPESZ];
56 char	yytext[2048];
57 FILE	*yyin, *yyout;
58 
59 static C_Added	*c_added, *c_tracked;
60 static IType	*Inline_stub[MAXINL];
61 static char	*ReDiRect;
62 static char	*Inliner[MAXINL], IArg_cont[MAXPAR][MAXLEN];
63 static unsigned char	in_comment=0;
64 static int	IArgno = 0, Inlining = -1;
65 static int	check_name(char *);
66 static int	last_token = 0;
67 
68 #define ValToken(x, y)	{ if (in_comment) goto again; \
69 			yylval = nn(ZN,0,ZN,ZN); \
70 			yylval->val = x; \
71 			last_token = y; \
72 			return y; \
73 			}
74 
75 #define SymToken(x, y)	{ if (in_comment) goto again; \
76 			yylval = nn(ZN,0,ZN,ZN); \
77 			yylval->sym = x; \
78 			last_token = y; \
79 			return y; \
80 			}
81 
82 static int  getinline(void);
83 static void uninline(void);
84 
85 static int PushBack;
86 static int PushedBack;
87 static char pushedback[4096];
88 
89 static void
push_back(char * s)90 push_back(char *s)
91 {
92 	if (PushedBack + strlen(s) > 4094)
93 	{	fatal("select statement too large", 0);
94 	}
95 	strcat(pushedback, s);
96 	PushedBack += strlen(s);
97 }
98 
99 static int
Getchar(void)100 Getchar(void)
101 {	int c;
102 
103 	if (PushedBack > 0 && PushBack < PushedBack)
104 	{	c = pushedback[PushBack++];
105 		if (PushBack == PushedBack)
106 		{	pushedback[0] = '\0';
107 			PushBack = PushedBack = 0;
108 		}
109 		return c;	/* expanded select statement */
110 	}
111 	if (Inlining<0)
112 	{	do {	c = getc(yyin);
113 		} while (c == 0);	// ignore null chars
114 		// eventually there will always be an EOF
115 	} else
116 	{	c = getinline();
117 	}
118 #if 0
119 	if (0)
120 	{	printf("<%c:%d>[%d] ", c, c, Inlining);
121 	} else
122 	{	printf("%c", c);
123 	}
124 #endif
125 	return c;
126 }
127 
128 static void
Ungetch(int c)129 Ungetch(int c)
130 {
131 	if (PushedBack > 0 && PushBack > 0)
132 	{	PushBack--;
133 		return;
134 	}
135 
136 	if (Inlining<0)
137 	{	ungetc(c,yyin);
138 	} else
139 	{	uninline();
140 	}
141 	if (0)
142 	{	printf("\n<bs{%d}bs>\n", c);
143 	}
144 }
145 
146 static int
notdollar(int c)147 notdollar(int c)
148 {	return (c != '$' && c != '\n');
149 }
150 
151 static int
notquote(int c)152 notquote(int c)
153 {	return (c != '\"' && c != '\n');
154 }
155 
156 int
isalnum_(int c)157 isalnum_(int c)
158 {	return (isalnum(c) || c == '_');
159 }
160 
161 static int
isalpha_(int c)162 isalpha_(int c)
163 {	return isalpha(c);	/* could be macro */
164 }
165 
166 static int
isdigit_(int c)167 isdigit_(int c)
168 {	return isdigit(c);	/* could be macro */
169 }
170 
171 static void
getword(int first,int (* tst)(int))172 getword(int first, int (*tst)(int))
173 {	int i=0, c;
174 
175 	yytext[i++]= (char) first;
176 	while (tst(c = Getchar()))
177 	{	if (c == EOF)
178 		{	break;
179 		}
180 		yytext[i++] = (char) c;
181 		if (c == '\\')
182 		{	c = Getchar();
183 			yytext[i++] = (char) c;	/* no tst */
184 	}	}
185 	yytext[i] = '\0';
186 
187 	Ungetch(c);
188 }
189 
190 static int
follow(int tok,int ifyes,int ifno)191 follow(int tok, int ifyes, int ifno)
192 {	int c;
193 
194 	if ((c = Getchar()) == tok)
195 	{	return ifyes;
196 	}
197 	Ungetch(c);
198 
199 	return ifno;
200 }
201 
202 static IType *seqnames;
203 
204 static void
def_inline(Symbol * s,int ln,char * ptr,char * prc,Lextok * nms)205 def_inline(Symbol *s, int ln, char *ptr, char *prc, Lextok *nms)
206 {	IType *tmp;
207 	int  cnt = 0;
208 	char *nw = (char *) emalloc(strlen(ptr)+1);
209 	strcpy(nw, ptr);
210 
211 	for (tmp = seqnames; tmp; cnt++, tmp = tmp->nxt)
212 		if (!strcmp(s->name, tmp->nm->name))
213 		{	non_fatal("procedure name %s redefined",
214 				tmp->nm->name);
215 			tmp->cn = (Lextok *) nw;
216 			tmp->params = nms;
217 			tmp->dln = ln;
218 			tmp->dfn = Fname;
219 			return;
220 		}
221 	tmp = (IType *) emalloc(sizeof(IType));
222 	tmp->nm = s;
223 	tmp->cn = (Lextok *) nw;
224 	tmp->params = nms;
225 	if (strlen(prc) > 0)
226 	{	tmp->prec = (char *) emalloc(strlen(prc)+1);
227 		strcpy(tmp->prec, prc);
228 	}
229 	tmp->dln = ln;
230 	tmp->dfn = Fname;
231 	tmp->uiid = cnt+1;	/* so that 0 means: not an inline */
232 	tmp->nxt = seqnames;
233 	seqnames = tmp;
234 }
235 
236 void
gencodetable(FILE * fd)237 gencodetable(FILE *fd)
238 {	IType *tmp;
239 	char *q;
240 	int cnt;
241 
242 	if (separate == 2) return;
243 
244 	fprintf(fd, "struct {\n");
245 	fprintf(fd, "	char *c; char *t;\n");
246 	fprintf(fd, "} code_lookup[] = {\n");
247 
248 	if (has_code)
249 	for (tmp = seqnames; tmp; tmp = tmp->nxt)
250 		if (tmp->nm->type == CODE_FRAG
251 		||  tmp->nm->type == CODE_DECL)
252 		{	fprintf(fd, "\t{ \"%s\", ",
253 				tmp->nm->name);
254 			q = (char *) tmp->cn;
255 
256 			while (*q == '\n' || *q == '\r' || *q == '\\')
257 				q++;
258 
259 			fprintf(fd, "\"");
260 			cnt = 0;
261 			while (*q && cnt < 1024) /* pangen1.h allows 2048 */
262 			{	switch (*q) {
263 				case '"':
264 					fprintf(fd, "\\\"");
265 					break;
266 				case '%':
267 					fprintf(fd, "%%");
268 					break;
269 				case '\n':
270 					fprintf(fd, "\\n");
271 					break;
272 				default:
273 					putc(*q, fd);
274 					break;
275 				}
276 				q++; cnt++;
277 			}
278 			if (*q) fprintf(fd, "...");
279 			fprintf(fd, "\"");
280 			fprintf(fd, " },\n");
281 		}
282 
283 	fprintf(fd, "	{ (char *) 0, \"\" }\n");
284 	fprintf(fd, "};\n");
285 }
286 
287 static int
iseqname(char * t)288 iseqname(char *t)
289 {	IType *tmp;
290 
291 	for (tmp = seqnames; tmp; tmp = tmp->nxt)
292 	{	if (!strcmp(t, tmp->nm->name))
293 			return 1;
294 	}
295 	return 0;
296 }
297 
298 Lextok *
return_statement(Lextok * n)299 return_statement(Lextok *n)
300 {
301 	if (Inline_stub[Inlining]->rval)
302 	{	Lextok *g = nn(ZN, NAME, ZN, ZN);
303 		Lextok *h = Inline_stub[Inlining]->rval;
304 		g->sym = lookup("rv_");
305 		return nn(h, ASGN, h, n);
306 	} else
307 	{	fatal("return statement outside inline", (char *) 0);
308 	}
309 	return ZN;
310 }
311 
312 static int
getinline(void)313 getinline(void)
314 {	int c;
315 
316 	if (ReDiRect)
317 	{	c = *ReDiRect++;
318 		if (c == '\0')
319 		{	ReDiRect = (char *) 0;
320 			c = *Inliner[Inlining]++;
321 		}
322 	} else
323 	{
324 		c = *Inliner[Inlining]++;
325 	}
326 
327 	if (c == '\0')
328 	{
329 		lineno = Inline_stub[Inlining]->cln;
330 		Fname  = Inline_stub[Inlining]->cfn;
331 		Inlining--;
332 
333 #if 0
334 		if (verbose&32)
335 		printf("spin: %s:%d, done inlining %s\n",
336 			Fname, lineno, Inline_stub[Inlining+1]->nm->name);
337 #endif
338 		return Getchar();
339 	}
340 	return c;
341 }
342 
343 static void
uninline(void)344 uninline(void)
345 {
346 	if (ReDiRect)
347 		ReDiRect--;
348 	else
349 		Inliner[Inlining]--;
350 }
351 
352 int
is_inline(void)353 is_inline(void)
354 {
355 	if (Inlining < 0)
356 		return 0;	/* i.e., not an inline */
357 	if (Inline_stub[Inlining] == NULL)
358 		fatal("unexpected, inline_stub not set", 0);
359 	return Inline_stub[Inlining]->uiid;
360 }
361 
362 IType *
find_inline(char * s)363 find_inline(char *s)
364 {	IType *tmp;
365 
366 	for (tmp = seqnames; tmp; tmp = tmp->nxt)
367 		if (!strcmp(s, tmp->nm->name))
368 			break;
369 	if (!tmp)
370 		fatal("cannot happen, missing inline def %s", s);
371 
372 	return tmp;
373 }
374 
375 void
c_state(Symbol * s,Symbol * t,Symbol * ival)376 c_state(Symbol *s, Symbol *t, Symbol *ival)	/* name, scope, ival */
377 {	C_Added *r;
378 
379 	r = (C_Added *) emalloc(sizeof(C_Added));
380 	r->s = s;	/* pointer to a data object */
381 	r->t = t;	/* size of object, or "global", or "local proctype_name"  */
382 	r->ival = ival;
383 	r->lno = lineno;
384 	r->fnm = Fname;
385 	r->nxt = c_added;
386 
387 	if(strncmp(r->s->name, "\"unsigned unsigned", 18) == 0)
388 	{	int i;
389 		for (i = 10; i < 18; i++)
390 		{	r->s->name[i] = ' ';
391 		}
392 	/*	printf("corrected <%s>\n", r->s->name);	*/
393 	}
394 	c_added = r;
395 }
396 
397 void
c_track(Symbol * s,Symbol * t,Symbol * stackonly)398 c_track(Symbol *s, Symbol *t, Symbol *stackonly)	/* name, size */
399 {	C_Added *r;
400 
401 	r = (C_Added *) emalloc(sizeof(C_Added));
402 	r->s = s;
403 	r->t = t;
404 	r->ival = stackonly;	/* abuse of name */
405 	r->nxt = c_tracked;
406 	r->fnm = Fname;
407 	r->lno = lineno;
408 	c_tracked = r;
409 
410 	if (stackonly != ZS)
411 	{	if (strcmp(stackonly->name, "\"Matched\"") == 0)
412 			r->ival = ZS;	/* the default */
413 		else if (strcmp(stackonly->name, "\"UnMatched\"") != 0
414 		     &&  strcmp(stackonly->name, "\"unMatched\"") != 0
415 		     &&  strcmp(stackonly->name, "\"StackOnly\"") != 0)
416 			non_fatal("expecting '[Un]Matched', saw %s", stackonly->name);
417 		else
418 			has_stack = 1;	/* unmatched stack */
419 	}
420 }
421 
422 char *
skip_white(char * p)423 skip_white(char *p)
424 {
425 	if (p != NULL)
426 	{	while (*p == ' ' || *p == '\t')
427 			p++;
428 	} else
429 	{	fatal("bad format - 1", (char *) 0);
430 	}
431 	return p;
432 }
433 
434 char *
skip_nonwhite(char * p)435 skip_nonwhite(char *p)
436 {
437 	if (p != NULL)
438 	{	while (*p != ' ' && *p != '\t')
439 			p++;
440 	} else
441 	{	fatal("bad format - 2", (char *) 0);
442 	}
443 	return p;
444 }
445 
446 static char *
jump_etc(C_Added * r)447 jump_etc(C_Added *r)
448 {	char *op = r->s->name;
449 	char *p = op;
450 	char *q = (char *) 0;
451 	int oln = lineno;
452 	Symbol *ofnm = Fname;
453 
454 	/* try to get the type separated from the name */
455 	lineno = r->lno;
456 	Fname  = r->fnm;
457 
458 	p = skip_white(p);	/* initial white space */
459 
460 	if (strncmp(p, "enum", strlen("enum")) == 0) /* special case: a two-part typename */
461 	{	p += strlen("enum")+1;
462 		p = skip_white(p);
463 	}
464 	if (strncmp(p, "unsigned", strlen("unsigned")) == 0) /* possibly a two-part typename */
465 	{	p += strlen("unsigned")+1;
466 		q = p = skip_white(p);
467 	}
468 	p = skip_nonwhite(p);	/* type name */
469 	p = skip_white(p);	/* white space */
470 	while (*p == '*') p++;	/* decorations */
471 	p = skip_white(p);	/* white space */
472 
473 	if (*p == '\0')
474 	{	if (q)
475 		{	p = q;	/* unsigned with implied 'int' */
476 		} else
477 		{	fatal("c_state format (%s)", op);
478 	}	}
479 
480 	if (strchr(p, '[')
481 	&& (!r->ival
482 	||  !r->ival->name
483 	||  !strchr(r->ival->name, '{')))	/* was !strchr(p, '{')) */
484 	{	non_fatal("array initialization error, c_state (%s)", p);
485 		p = (char *) 0;
486 	}
487 
488 	lineno = oln;
489 	Fname = ofnm;
490 
491 	return p;
492 }
493 
494 void
c_add_globinit(FILE * fd)495 c_add_globinit(FILE *fd)
496 {	C_Added *r;
497 	char *p, *q;
498 
499 	fprintf(fd, "void\nglobinit(void)\n{\n");
500 	for (r = c_added; r; r = r->nxt)
501 	{	if (r->ival == ZS)
502 			continue;
503 
504 		if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0)
505 		{	for (q = r->ival->name; *q; q++)
506 			{	if (*q == '\"')
507 					*q = ' ';
508 				if (*q == '\\')
509 					*q++ = ' '; /* skip over the next */
510 			}
511 			p = jump_etc(r);	/* e.g., "int **q" */
512 			if (p)
513 			fprintf(fd, "	now.%s = %s;\n", p, r->ival->name);
514 
515 		} else
516 		if (strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0)
517 		{	for (q = r->ival->name; *q; q++)
518 			{	if (*q == '\"')
519 					*q = ' ';
520 				if (*q == '\\')
521 					*q++ = ' '; /* skip over the next */
522 			}
523 			p = jump_etc(r);	/* e.g., "int **q" */
524 			if (p)
525 			fprintf(fd, "	%s = %s;\n", p, r->ival->name);	/* no now. prefix */
526 
527 	}	}
528 	fprintf(fd, "}\n");
529 }
530 
531 void
c_add_locinit(FILE * fd,int tpnr,char * pnm)532 c_add_locinit(FILE *fd, int tpnr, char *pnm)
533 {	C_Added *r;
534 	char *p, *q, *s;
535 	int frst = 1;
536 
537 	fprintf(fd, "void\nlocinit%d(int h)\n{\n", tpnr);
538 	for (r = c_added; r; r = r->nxt)
539 		if (r->ival != ZS
540 		&&  strncmp(r->t->name, " Local", strlen(" Local")) == 0)
541 		{	for (q = r->ival->name; *q; q++)
542 				if (*q == '\"')
543 					*q = ' ';
544 			p = jump_etc(r);	/* e.g., "int **q" */
545 
546 			q = r->t->name + strlen(" Local");
547 			while (*q == ' ' || *q == '\t')
548 				q++;			/* process name */
549 
550 			s = (char *) emalloc(strlen(q)+1);
551 			strcpy(s, q);
552 
553 			q = &s[strlen(s)-1];
554 			while (*q == ' ' || *q == '\t')
555 				*q-- = '\0';
556 
557 			if (strcmp(pnm, s) != 0)
558 				continue;
559 
560 			if (frst)
561 			{	fprintf(fd, "\tuchar *_this = pptr(h);\n");
562 				frst = 0;
563 			}
564 
565 			if (p)
566 			{	fprintf(fd, "\t\t((P%d *)_this)->%s = %s;\n",
567 					tpnr, p, r->ival->name);
568 			}
569 		}
570 	fprintf(fd, "}\n");
571 }
572 
573 /* tracking:
574 	1. for non-global and non-local c_state decls: add up all the sizes in c_added
575 	2. add a global char array of that size into now
576 	3. generate a routine that memcpy's the required values into that array
577 	4. generate a call to that routine
578  */
579 
580 void
c_preview(void)581 c_preview(void)
582 {	C_Added *r;
583 
584 	hastrack = 0;
585 	if (c_tracked)
586 		hastrack = 1;
587 	else
588 	for (r = c_added; r; r = r->nxt)
589 		if (strncmp(r->t->name, " Global ", strlen(" Global ")) != 0
590 		&&  strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) != 0
591 		&&  strncmp(r->t->name, " Local",  strlen(" Local"))  != 0)
592 		{	hastrack = 1;	/* c_state variant now obsolete */
593 			break;
594 		}
595 }
596 
597 int
c_add_sv(FILE * fd)598 c_add_sv(FILE *fd)	/* 1+2 -- called in pangen1.c */
599 {	C_Added *r;
600 	int cnt = 0;
601 
602 	if (!c_added && !c_tracked) return 0;
603 
604 	for (r = c_added; r; r = r->nxt)	/* pickup global decls */
605 		if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0)
606 			fprintf(fd, "	%s;\n", r->s->name);
607 
608 	for (r = c_added; r; r = r->nxt)
609 		if (strncmp(r->t->name, " Global ", strlen(" Global ")) != 0
610 		&&  strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) != 0
611 		&&  strncmp(r->t->name, " Local",  strlen(" Local"))  != 0)
612 		{	cnt++;	/* obsolete use */
613 		}
614 
615 	for (r = c_tracked; r; r = r->nxt)
616 		cnt++;		/* preferred use */
617 
618 	if (cnt == 0) return 0;
619 
620 	cnt = 0;
621 	fprintf(fd, "	uchar c_state[");
622 	for (r = c_added; r; r = r->nxt)
623 		if (strncmp(r->t->name, " Global ", strlen(" Global ")) != 0
624 		&&  strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) != 0
625 		&&  strncmp(r->t->name, " Local",  strlen(" Local"))  != 0)
626 		{	fprintf(fd, "%ssizeof(%s)",
627 				(cnt==0)?"":"+", r->t->name);
628 			cnt++;
629 		}
630 
631 	for (r = c_tracked; r; r = r->nxt)
632 	{	if (r->ival != ZS) continue;
633 
634 		fprintf(fd, "%s%s",
635 			(cnt==0)?"":"+", r->t->name);
636 		cnt++;
637 	}
638 
639 	if (cnt == 0) fprintf(fd, "4");	/* now redundant */
640 	fprintf(fd, "];\n");
641 	return 1;
642 }
643 
644 void
c_stack_size(FILE * fd)645 c_stack_size(FILE *fd)
646 {	C_Added *r;
647 	int cnt = 0;
648 
649 	for (r = c_tracked; r; r = r->nxt)
650 		if (r->ival != ZS)
651 		{	fprintf(fd, "%s%s",
652 				(cnt==0)?"":"+", r->t->name);
653 			cnt++;
654 		}
655 	if (cnt == 0)
656 	{	fprintf(fd, "WS");
657 	}
658 }
659 
660 void
c_add_stack(FILE * fd)661 c_add_stack(FILE *fd)
662 {	C_Added *r;
663 	int cnt = 0;
664 
665 	if ((!c_added && !c_tracked) || !has_stack)
666 	{	return;
667 	}
668 
669 	for (r = c_tracked; r; r = r->nxt)
670 		if (r->ival != ZS)
671 		{	cnt++;
672 		}
673 
674 	if (cnt > 0)
675 	{	fprintf(fd, "	uchar c_stack[StackSize];\n");
676 	}
677 }
678 
679 void
c_add_hidden(FILE * fd)680 c_add_hidden(FILE *fd)
681 {	C_Added *r;
682 
683 	for (r = c_added; r; r = r->nxt)	/* pickup hidden decls */
684 		if (strncmp(r->t->name, "\"Hidden\"", strlen("\"Hidden\"")) == 0)
685 		{	r->s->name[strlen(r->s->name)-1] = ' ';
686 			fprintf(fd, "%s;	/* Hidden */\n", &r->s->name[1]);
687 			r->s->name[strlen(r->s->name)-1] = '"';
688 		}
689 	/* called before c_add_def - quotes are still there */
690 }
691 
692 void
c_add_loc(FILE * fd,char * s)693 c_add_loc(FILE *fd, char *s)	/* state vector entries for proctype s */
694 {	C_Added *r;
695 	static char buf[1024];
696 	char *p;
697 
698 	if (!c_added) return;
699 
700 	strcpy(buf, s);
701 	strcat(buf, " ");
702 	for (r = c_added; r; r = r->nxt)	/* pickup local decls */
703 	{	if (strncmp(r->t->name, " Local", strlen(" Local")) == 0)
704 		{	p = r->t->name + strlen(" Local");
705 fprintf(fd, "/* XXX p=<%s>, s=<%s>, buf=<%s> r->s->name=<%s>XXX */\n", p, s, buf, r->s->name);
706 			while (*p == ' ' || *p == '\t')
707 			{	p++;
708 			}
709 			if (strcmp(p, buf) == 0
710 			||  (strncmp(p, "init", 4) == 0 && strncmp(buf, ":init:", 6) == 0))
711 			{	fprintf(fd, "	%s;\n", r->s->name);
712 	}	}	}
713 }
714 void
c_add_def(FILE * fd)715 c_add_def(FILE *fd)	/* 3 - called in plunk_c_fcts() */
716 {	C_Added *r;
717 
718 	fprintf(fd, "#if defined(C_States) && (HAS_TRACK==1)\n");
719 	for (r = c_added; r; r = r->nxt)
720 	{	r->s->name[strlen(r->s->name)-1] = ' ';
721 		r->s->name[0] = ' '; /* remove the "s */
722 
723 		r->t->name[strlen(r->t->name)-1] = ' ';
724 		r->t->name[0] = ' ';
725 
726 		if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0
727 		||  strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0
728 		||  strncmp(r->t->name, " Local",  strlen(" Local"))  == 0)
729 			continue;
730 
731 		if (strchr(r->s->name, '&'))
732 			fatal("dereferencing state object: %s", r->s->name);
733 
734 		fprintf(fd, "extern %s %s;\n", r->t->name, r->s->name);
735 	}
736 	for (r = c_tracked; r; r = r->nxt)
737 	{	r->s->name[strlen(r->s->name)-1] = ' ';
738 		r->s->name[0] = ' '; /* remove " */
739 
740 		r->t->name[strlen(r->t->name)-1] = ' ';
741 		r->t->name[0] = ' ';
742 	}
743 
744 	if (separate == 2)
745 	{	fprintf(fd, "#endif\n");
746 		return;
747 	}
748 
749 	if (has_stack)
750 	{	fprintf(fd, "int cpu_printf(const char *, ...);\n");
751 		fprintf(fd, "void\nc_stack(uchar *p_t_r)\n{\n");
752 		fprintf(fd, "#ifdef VERBOSE\n");
753 		fprintf(fd, "	cpu_printf(\"c_stack %%u\\n\", p_t_r);\n");
754 		fprintf(fd, "#endif\n");
755 		for (r = c_tracked; r; r = r->nxt)
756 		{	if (r->ival == ZS) continue;
757 
758 			fprintf(fd, "\tif(%s)\n", r->s->name);
759 			fprintf(fd, "\t\tmemcpy(p_t_r, %s, %s);\n",
760 				r->s->name, r->t->name);
761 			fprintf(fd, "\telse\n");
762 			fprintf(fd, "\t\tmemset(p_t_r, 0, %s);\n",
763 				r->t->name);
764 			fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
765 		}
766 		fprintf(fd, "}\n\n");
767 	}
768 
769 	fprintf(fd, "void\nc_update(uchar *p_t_r)\n{\n");
770 	fprintf(fd, "#ifdef VERBOSE\n");
771 	fprintf(fd, "	printf(\"c_update %%p\\n\", p_t_r);\n");
772 	fprintf(fd, "#endif\n");
773 	for (r = c_added; r; r = r->nxt)
774 	{	if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0
775 		||  strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0
776 		||  strncmp(r->t->name, " Local",  strlen(" Local"))  == 0)
777 			continue;
778 
779 		fprintf(fd, "\tmemcpy(p_t_r, &%s, sizeof(%s));\n",
780 			r->s->name, r->t->name);
781 		fprintf(fd, "\tp_t_r += sizeof(%s);\n", r->t->name);
782 	}
783 
784 	for (r = c_tracked; r; r = r->nxt)
785 	{	if (r->ival) continue;
786 
787 		fprintf(fd, "\tif(%s)\n", r->s->name);
788 		fprintf(fd, "\t\tmemcpy(p_t_r, %s, %s);\n",
789 			r->s->name, r->t->name);
790 		fprintf(fd, "\telse\n");
791 		fprintf(fd, "\t\tmemset(p_t_r, 0, %s);\n",
792 			r->t->name);
793 		fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
794 	}
795 
796 	fprintf(fd, "}\n");
797 
798 	if (has_stack)
799 	{	fprintf(fd, "void\nc_unstack(uchar *p_t_r)\n{\n");
800 		fprintf(fd, "#ifdef VERBOSE\n");
801 		fprintf(fd, "	cpu_printf(\"c_unstack %%u\\n\", p_t_r);\n");
802 		fprintf(fd, "#endif\n");
803 		for (r = c_tracked; r; r = r->nxt)
804 		{	if (r->ival == ZS) continue;
805 
806 			fprintf(fd, "\tif(%s)\n", r->s->name);
807 			fprintf(fd, "\t\tmemcpy(%s, p_t_r, %s);\n",
808 				r->s->name, r->t->name);
809 			fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
810 		}
811 		fprintf(fd, "}\n");
812 	}
813 
814 	fprintf(fd, "void\nc_revert(uchar *p_t_r)\n{\n");
815 	fprintf(fd, "#ifdef VERBOSE\n");
816 	fprintf(fd, "	printf(\"c_revert %%p\\n\", p_t_r);\n");
817 	fprintf(fd, "#endif\n");
818 	for (r = c_added; r; r = r->nxt)
819 	{	if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0
820 		||  strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0
821 		||  strncmp(r->t->name, " Local",  strlen(" Local"))  == 0)
822 			continue;
823 
824 		fprintf(fd, "\tmemcpy(&%s, p_t_r, sizeof(%s));\n",
825 			r->s->name, r->t->name);
826 		fprintf(fd, "\tp_t_r += sizeof(%s);\n", r->t->name);
827 	}
828 	for (r = c_tracked; r; r = r->nxt)
829 	{	if (r->ival != ZS) continue;
830 
831 		fprintf(fd, "\tif(%s)\n", r->s->name);
832 		fprintf(fd, "\t\tmemcpy(%s, p_t_r, %s);\n",
833 			r->s->name, r->t->name);
834 		fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
835 	}
836 
837 	fprintf(fd, "}\n");
838 	fprintf(fd, "#endif\n");
839 }
840 
841 void
plunk_reverse(FILE * fd,IType * p,int matchthis)842 plunk_reverse(FILE *fd, IType *p, int matchthis)
843 {	char *y, *z;
844 
845 	if (!p) return;
846 	plunk_reverse(fd, p->nxt, matchthis);
847 
848 	if (!p->nm->context
849 	&&   p->nm->type == matchthis
850 	&&   p->is_expr == 0)
851 	{	fprintf(fd, "\n/* start of %s */\n", p->nm->name);
852 		z = (char *) p->cn;
853 		while (*z == '\n' || *z == '\r' || *z == '\\')
854 		{	z++;
855 		}
856 		/* e.g.: \#include "..." */
857 
858 		y = z;
859 		while ((y = strstr(y, "\\#")) != NULL)
860 		{	*y = '\n'; y++;
861 		}
862 
863 		fprintf(fd, "%s\n", z);
864 		fprintf(fd, "\n/* end of %s */\n", p->nm->name);
865 	}
866 }
867 
868 void
plunk_c_decls(FILE * fd)869 plunk_c_decls(FILE *fd)
870 {
871 	plunk_reverse(fd, seqnames, CODE_DECL);
872 }
873 
874 void
plunk_c_fcts(FILE * fd)875 plunk_c_fcts(FILE *fd)
876 {
877 	if (separate == 2 && hastrack)
878 	{	c_add_def(fd);
879 		return;
880 	}
881 
882 	c_add_hidden(fd);
883 	plunk_reverse(fd, seqnames, CODE_FRAG);
884 
885 	if (c_added || c_tracked)	/* enables calls to c_revert and c_update */
886 		fprintf(fd, "#define C_States	1\n");
887 	else
888 		fprintf(fd, "#undef C_States\n");
889 
890 	if (hastrack)
891 		c_add_def(fd);
892 
893 	c_add_globinit(fd);
894 	do_locinits(fd);
895 }
896 
897 static void
check_inline(IType * tmp)898 check_inline(IType *tmp)
899 {	char buf[128];
900 	ProcList *p;
901 
902 	if (!X_lst) return;
903 
904 	for (p = ready; p; p = p->nxt)
905 	{	if (strcmp(p->n->name, X_lst->n->name) == 0)
906 			continue;
907 		sprintf(buf, "P%s->", p->n->name);
908 		if (strstr((char *)tmp->cn, buf))
909 		{	printf("spin: in proctype %s, ref to object in proctype %s\n",
910 				X_lst->n->name, p->n->name);
911 			fatal("invalid variable ref in '%s'", tmp->nm->name);
912 	}	}
913 }
914 
915 extern short terse;
916 extern short nocast;
917 
918 void
plunk_expr(FILE * fd,char * s)919 plunk_expr(FILE *fd, char *s)
920 {	IType *tmp;
921 	char *q;
922 
923 	tmp = find_inline(s);
924 	check_inline(tmp);
925 
926 	if (terse && nocast)
927 	{	for (q = (char *) tmp->cn; q && *q != '\0'; q++)
928 		{	fflush(fd);
929 			if (*q == '"')
930 			{	fprintf(fd, "\\");
931 			}
932 			fprintf(fd, "%c", *q);
933 		}
934 	} else
935 	{	fprintf(fd, "%s", (char *) tmp->cn);
936 	}
937 }
938 
939 void
preruse(FILE * fd,Lextok * n)940 preruse(FILE *fd, Lextok *n)	/* check a condition for c_expr with preconditions */
941 {	IType *tmp;
942 
943 	if (!n) return;
944 	if (n->ntyp == C_EXPR)
945 	{	tmp = find_inline(n->sym->name);
946 		if (tmp->prec)
947 		{	fprintf(fd, "if (!(%s)) { if (!readtrail) { depth++; ", tmp->prec);
948 			fprintf(fd, "trpt++; trpt->pr = II; trpt->o_t = t; trpt->st = tt; ");
949 			fprintf(fd, "uerror(\"c_expr line %d precondition false: %s\"); continue;",
950 				tmp->dln, tmp->prec);
951 			fprintf(fd, " } else { printf(\"pan: precondition false: %s\\n\"); ",
952 				tmp->prec);
953 			fprintf(fd, "_m = 3; goto P999; } } \n\t\t");
954 		}
955 	} else
956 	{	preruse(fd, n->rgt);
957 		preruse(fd, n->lft);
958 	}
959 }
960 
961 int
glob_inline(char * s)962 glob_inline(char *s)
963 {	IType *tmp;
964 	char *bdy;
965 
966 	tmp = find_inline(s);
967 	bdy = (char *) tmp->cn;
968 	return (strstr(bdy, "now.")		/* global ref or   */
969 	||      strchr(bdy, '(') > bdy);	/* possible C-function call */
970 }
971 
972 char *
put_inline(FILE * fd,char * s)973 put_inline(FILE *fd, char *s)
974 {	IType *tmp;
975 
976 	tmp = find_inline(s);
977 	check_inline(tmp);
978 	return (char *) tmp->cn;
979 }
980 
981 void
mark_last(void)982 mark_last(void)
983 {
984 	if (seqnames)
985 	{	seqnames->is_expr = 1;
986 	}
987 }
988 
989 void
plunk_inline(FILE * fd,char * s,int how,int gencode)990 plunk_inline(FILE *fd, char *s, int how, int gencode)	/* c_code with precondition */
991 {	IType *tmp;
992 
993 	tmp = find_inline(s);
994 	check_inline(tmp);
995 
996 	fprintf(fd, "{ ");
997 	if (how && tmp->prec)
998 	{	fprintf(fd, "if (!(%s)) { if (!readtrail) {",
999 			tmp->prec);
1000 		fprintf(fd, " uerror(\"c_code line %d precondition false: %s\"); continue; ",
1001 			tmp->dln,
1002 			tmp->prec);
1003 		fprintf(fd, "} else { ");
1004 		fprintf(fd, "printf(\"pan: precondition false: %s\\n\"); _m = 3; goto P999; } } ",
1005 			tmp->prec);
1006 	}
1007 
1008 	if (!gencode)	/* not in d_step */
1009 	{	fprintf(fd, "\n\t\tsv_save();");
1010 	}
1011 
1012 	fprintf(fd, "%s", (char *) tmp->cn);
1013 	fprintf(fd, " }\n");
1014 }
1015 
1016 int
side_scan(char * t,char * pat)1017 side_scan(char *t, char *pat)
1018 {	char *r = strstr(t, pat);
1019 	return (r
1020 		&& *(r-1) != '"'
1021 		&& *(r-1) != '\'');
1022 }
1023 
1024 void
no_side_effects(char * s)1025 no_side_effects(char *s)
1026 {	IType *tmp;
1027 	char *t;
1028 	char *z;
1029 
1030 	/* could still defeat this check via hidden
1031 	 * side effects in function calls,
1032 	 * but this will catch at least some cases
1033 	 */
1034 
1035 	tmp = find_inline(s);
1036 	t = (char *) tmp->cn;
1037 	while (t && *t == ' ')
1038 	{	t++;
1039 	}
1040 
1041 	z = strchr(t, '(');
1042 	if (z
1043 	&&  z > t
1044 	&&  isalnum((int) *(z-1))
1045 	&&  strncmp(t, "spin_mutex_free(", strlen("spin_mutex_free(")) != 0)
1046 	{	goto bad;	/* fct call */
1047 	}
1048 
1049 	if (side_scan(t, ";")
1050 	||  side_scan(t, "++")
1051 	||  side_scan(t, "--"))
1052 	{
1053 bad:		lineno = tmp->dln;
1054 		Fname = tmp->dfn;
1055 		non_fatal("c_expr %s has side-effects", s);
1056 		return;
1057 	}
1058 	while ((t = strchr(t, '=')) != NULL)
1059 	{	if (*(t-1) == '!'
1060 		||  *(t-1) == '>'
1061 		||  *(t-1) == '<'
1062 		||  *(t-1) == '"'
1063 		||  *(t-1) == '\'')
1064 		{	t += 2;
1065 			continue;
1066 		}
1067 		t++;
1068 		if (*t != '=')
1069 			goto bad;
1070 		t++;
1071 	}
1072 }
1073 
1074 void
pickup_inline(Symbol * t,Lextok * apars,Lextok * rval)1075 pickup_inline(Symbol *t, Lextok *apars, Lextok *rval)
1076 {	IType *tmp; Lextok *p, *q; int j;
1077 
1078 	tmp = find_inline(t->name);
1079 
1080 	if (++Inlining >= MAXINL)
1081 		fatal("inlines nested too deeply", 0);
1082 	tmp->cln = lineno;	/* remember calling point */
1083 	tmp->cfn = Fname;	/* and filename */
1084 	tmp->rval = rval;
1085 
1086 	for (p = apars, q = tmp->params, j = 0; p && q; p = p->rgt, q = q->rgt)
1087 		j++; /* count them */
1088 	if (p || q)
1089 		fatal("wrong nr of params on call of '%s'", t->name);
1090 
1091 	tmp->anms  = (char **) emalloc(j * sizeof(char *));
1092 	for (p = apars, j = 0; p; p = p->rgt, j++)
1093 	{	tmp->anms[j] = (char *) emalloc(strlen(IArg_cont[j])+1);
1094 		strcpy(tmp->anms[j], IArg_cont[j]);
1095 	}
1096 
1097 	lineno = tmp->dln;	/* linenr of def */
1098 	Fname = tmp->dfn;	/* filename of same */
1099 	Inliner[Inlining] = (char *)tmp->cn;
1100 	Inline_stub[Inlining] = tmp;
1101 #if 0
1102 	if (verbose&32)
1103 	printf("spin: %s:%d, inlining '%s' (from %s:%d)\n",
1104 		tmp->cfn->name, tmp->cln, t->name, tmp->dfn->name, tmp->dln);
1105 #endif
1106 	for (j = 0; j < Inlining; j++)
1107 	{	if (Inline_stub[j] == Inline_stub[Inlining])
1108 		{	fatal("cyclic inline attempt on: %s", t->name);
1109 	}	}
1110 	last_token = SEMI;	/* avoid insertion of extra semi */
1111 }
1112 
1113 extern int pp_mode;
1114 
1115 static void
do_directive(int first)1116 do_directive(int first)
1117 {	int c = first;	/* handles lines starting with pound */
1118 
1119 	getword(c, isalpha_);
1120 
1121 	if (strcmp(yytext, "#ident") == 0)
1122 		goto done;
1123 
1124 	if ((c = Getchar()) != ' ')
1125 		fatal("malformed preprocessor directive - # .", 0);
1126 
1127 	if (!isdigit_(c = Getchar()))
1128 		fatal("malformed preprocessor directive - # .lineno", 0);
1129 
1130 	getword(c, isdigit_);
1131 	lineno = atoi(yytext);	/* pickup the line number */
1132 
1133 	if ((c = Getchar()) == '\n')
1134 		return;	/* no filename */
1135 
1136 	if (c != ' ')
1137 		fatal("malformed preprocessor directive - .fname", 0);
1138 
1139 	if ((c = Getchar()) != '\"')
1140 	{	printf("got %c, expected \" -- lineno %d\n", c, lineno);
1141 		fatal("malformed preprocessor directive - .fname (%s)", yytext);
1142 	}
1143 
1144 	getword(Getchar(), notquote);	/* was getword(c, notquote); */
1145 	if (Getchar() != '\"')
1146 		fatal("malformed preprocessor directive - fname.", 0);
1147 
1148 	/* strcat(yytext, "\""); */
1149 	Fname = lookup(yytext);
1150 done:
1151 	while (Getchar() != '\n')
1152 		;
1153 }
1154 
1155 void
precondition(char * q)1156 precondition(char *q)
1157 {	int c, nest = 1;
1158 
1159 	for (;;)
1160 	{	c = Getchar();
1161 		*q++ = c;
1162 		switch (c) {
1163 		case '\n':
1164 			lineno++;
1165 			break;
1166 		case '[':
1167 			nest++;
1168 			break;
1169 		case ']':
1170 			if (--nest <= 0)
1171 			{	*--q = '\0';
1172 				return;
1173 			}
1174 			break;
1175 		}
1176 	}
1177 	fatal("cannot happen", (char *) 0); /* unreachable */
1178 }
1179 
1180 
1181 Symbol *
prep_inline(Symbol * s,Lextok * nms)1182 prep_inline(Symbol *s, Lextok *nms)
1183 {	int c, nest = 1, dln, firstchar, cnr;
1184 	char *p;
1185 	Lextok *t;
1186 	static char Buf1[SOMETHINGBIG], Buf2[RATHERSMALL];
1187 	static int c_code = 1;
1188 
1189 	for (t = nms; t; t = t->rgt)
1190 		if (t->lft)
1191 		{	if (t->lft->ntyp != NAME)
1192 			fatal("bad param to inline %s", s?s->name:"--");
1193 			t->lft->sym->hidden |= 32;
1194 		}
1195 
1196 	if (!s)	/* C_Code fragment */
1197 	{	s = (Symbol *) emalloc(sizeof(Symbol));
1198 		s->name = (char *) emalloc(strlen("c_code")+26);
1199 		sprintf(s->name, "c_code%d", c_code++);
1200 		s->context = context;
1201 		s->type = CODE_FRAG;
1202 	} else
1203 	{	s->type = PREDEF;
1204 	}
1205 
1206 	p = &Buf1[0];
1207 	Buf2[0] = '\0';
1208 	for (;;)
1209 	{	c = Getchar();
1210 		switch (c) {
1211 		case '[':
1212 			if (s->type != CODE_FRAG)
1213 				goto bad;
1214 			precondition(&Buf2[0]);	/* e.g., c_code [p] { r = p-r; } */
1215 			continue;
1216 		case '{':
1217 			break;
1218 		case '\n':
1219 			lineno++;
1220 			/* fall through */
1221 		case ' ': case '\t': case '\f': case '\r':
1222 			continue;
1223 		default :
1224 			 printf("spin: saw char '%c'\n", c);
1225 bad:			 fatal("bad inline: %s", s->name);
1226 		}
1227 		break;
1228 	}
1229 	dln = lineno;
1230 	if (s->type == CODE_FRAG)
1231 	{	if (verbose&32)
1232 		{	sprintf(Buf1, "\t/* line %d %s */\n\t\t",
1233 				lineno, Fname->name);
1234 		} else
1235 		{	strcpy(Buf1, "");
1236 		}
1237 	} else
1238 	{	sprintf(Buf1, "\n#line %d \"%s\"\n{", lineno, Fname->name);
1239 	}
1240 	p += strlen(Buf1);
1241 	firstchar = 1;
1242 
1243 	cnr = 1; /* not zero */
1244 more:
1245 	c = Getchar();
1246 	*p++ = (char) c;
1247 	if (p - Buf1 >= SOMETHINGBIG)
1248 		fatal("inline text too long", 0);
1249 	switch (c) {
1250 	case '\n':
1251 		lineno++;
1252 		cnr = 0;
1253 		break;
1254 	case '{':
1255 		cnr++;
1256 		nest++;
1257 		break;
1258 	case '}':
1259 		cnr++;
1260 		if (--nest <= 0)
1261 		{	*p = '\0';
1262 			if (s->type == CODE_FRAG)
1263 			{	*--p = '\0';	/* remove trailing '}' */
1264 			}
1265 			def_inline(s, dln, &Buf1[0], &Buf2[0], nms);
1266 			if (firstchar)
1267 			{	printf("%3d: %s, warning: empty inline definition (%s)\n",
1268 					dln, Fname->name, s->name);
1269 			}
1270 			return s;	/* normal return */
1271 		}
1272 		break;
1273 	case '#':
1274 		if (cnr == 0)
1275 		{	p--;
1276 			do_directive(c); /* reads to newline */
1277 		} else
1278 		{	firstchar = 0;
1279 			cnr++;
1280 		}
1281 		break;
1282 	case '\t':
1283 	case ' ':
1284 	case '\f':
1285 		cnr++;
1286 		break;
1287 	case '"':
1288 		do {
1289 			c = Getchar();
1290 			*p++ = (char) c;
1291 			if (c == '\\')
1292 			{	*p++ = (char) Getchar();
1293 			}
1294 			if (p - Buf1 >= SOMETHINGBIG)
1295 			{	fatal("inline text too long", 0);
1296 			}
1297 		} while (c != '"');	/* end of string */
1298 		/* *p = '\0'; */
1299 		break;
1300 	case '\'':
1301 		c = Getchar();
1302 		*p++ = (char) c;
1303 		if (c == '\\')
1304 		{	*p++ = (char) Getchar();
1305 		}
1306 		c = Getchar();
1307 		*p++ = (char) c;
1308 		assert(c == '\'');
1309 		break;
1310 	default:
1311 		firstchar = 0;
1312 		cnr++;
1313 		break;
1314 	}
1315 	goto more;
1316 }
1317 
1318 static void
set_cur_scope(void)1319 set_cur_scope(void)
1320 {	int i;
1321 	char tmpbuf[256];
1322 
1323 	strcpy(CurScope, "_");
1324 
1325 	if (context)
1326 	for (i = 0; i < scope_level; i++)
1327 	{	sprintf(tmpbuf, "%d_", scope_seq[i]);
1328 		strcat(CurScope, tmpbuf);
1329 	}
1330 }
1331 
1332 static int
pre_proc(void)1333 pre_proc(void)
1334 {	char b[512];
1335 	int c, i = 0;
1336 
1337 	b[i++] = '#';
1338 	while ((c = Getchar()) != '\n' && c != EOF)
1339 	{	b[i++] = (char) c;
1340 	}
1341 	b[i] = '\0';
1342 	yylval = nn(ZN, 0, ZN, ZN);
1343 	yylval->sym = lookup(b);
1344 	return PREPROC;
1345 }
1346 
1347 static int specials[] = {
1348 	'}', ')', ']',
1349 	OD, FI, ELSE, BREAK,
1350 	C_CODE, C_EXPR, C_DECL,
1351 	NAME, CONST, INCR, DECR, 0
1352 };
1353 
1354 int
follows_token(int c)1355 follows_token(int c)
1356 {	int i;
1357 
1358 	for (i = 0; specials[i]; i++)
1359 	{	if (c == specials[i])
1360 		{	return 1;
1361 	}	}
1362 	return 0;
1363 }
1364 #define DEFER_LTL
1365 #ifdef DEFER_LTL
1366 /* defer ltl formula to the end of the spec
1367  * no matter where they appear in the original
1368  */
1369 
1370 static int deferred = 0;
1371 static FILE *defer_fd;
1372 
1373 int
get_deferred(void)1374 get_deferred(void)
1375 {
1376 	if (!defer_fd)
1377 	{	return 0;	/* nothing was deferred */
1378 	}
1379 	fclose(defer_fd);
1380 
1381 	defer_fd = fopen(TMP_FILE2, "r");
1382 	if (!defer_fd)
1383 	{	non_fatal("cannot retrieve deferred ltl formula", (char *) 0);
1384 		return 0;
1385 	}
1386 	fclose(yyin);
1387 	yyin = defer_fd;
1388 	return 1;
1389 }
1390 
1391 void
zap_deferred(void)1392 zap_deferred(void)
1393 {
1394 	(void) unlink(TMP_FILE2);
1395 }
1396 
1397 int
put_deferred(void)1398 put_deferred(void)
1399 {	int c, cnt;
1400 	if (!defer_fd)
1401 	{	defer_fd = fopen(TMP_FILE2, "w+");
1402 		if (!defer_fd)
1403 		{	non_fatal("cannot defer ltl expansion", (char *) 0);
1404 			return 0;
1405 	}	}
1406 	fprintf(defer_fd, "ltl ");
1407 	cnt = 0;
1408 	while ((c = getc(yyin)) != EOF)
1409 	{	if (c == '{')
1410 		{	cnt++;
1411 		}
1412 		if (c == '}')
1413 		{	cnt--;
1414 			if (cnt == 0)
1415 			{	break;
1416 		}	}
1417 		fprintf(defer_fd, "%c", c);
1418 	}
1419 	fprintf(defer_fd, "}\n");
1420 	fflush(defer_fd);
1421 	return 1;
1422 }
1423 #endif
1424 
1425 #define EXPAND_SELECT
1426 #ifdef EXPAND_SELECT
1427 static char tmp_hold[256];
1428 static int  tmp_has;
1429 
1430 void
new_select(void)1431 new_select(void)
1432 {	tmp_hold[0] = '\0';
1433 	tmp_has = 0;
1434 }
1435 
1436 static int
scan_to(int stop,int (* tst)(int),char * buf,int bufsz)1437 scan_to(int stop, int (*tst)(int), char *buf, int bufsz)
1438 {	int c, i = 0;
1439 
1440 	do {	c = Getchar();
1441 		if (tmp_has < sizeof(tmp_hold))
1442 		{	tmp_hold[tmp_has++] = c;
1443 		}
1444 		if (c == '\n')
1445 		{	lineno++;
1446 		} else if (buf && i < bufsz-1)
1447 		{	buf[i++] = c;
1448 		} else if (buf && i >= bufsz-1)
1449 		{	buf[bufsz-1] = '\0';
1450 			fatal("name too long", buf);
1451 		}
1452 		if (tst && !tst(c) && c != ' ' && c != '\t')
1453 		{	break;
1454 		}
1455 	} while (c != stop && c != EOF);
1456 
1457 	if (buf)
1458 	{	if (i <= 0)
1459 		{	fatal("input error", (char *) 0);
1460 		}
1461 		buf[i-1] = '\0';
1462 	}
1463 
1464 	if (c != stop)
1465 	{	if (0)
1466 		{	printf("saw: '%c', expected '%c'\n", c, stop);
1467 		}
1468 		if (tmp_has < sizeof(tmp_hold))
1469 		{	tmp_hold[tmp_has] = '\0';
1470 			push_back(tmp_hold);
1471 			if (0)
1472 			{	printf("pushed back: <'%s'>\n", tmp_hold);
1473 			}
1474 			return 0; /* internal expansion fails */
1475 		} else
1476 		{	fatal("expecting select ( name : constant .. constant )", 0);
1477 	}	}
1478 	return 1;		/* success */
1479 }
1480 #endif
1481 
1482 int
lex(void)1483 lex(void)
1484 {	int c;
1485 again:
1486 	c = Getchar();
1487 /* more: */
1488 	yytext[0] = (char) c;
1489 	yytext[1] = '\0';
1490 	switch (c) {
1491 	case EOF:
1492 #ifdef DEFER_LTL
1493 		if (!deferred)
1494 		{	deferred = 1;
1495 			if (get_deferred())
1496 			{	goto again;
1497 			}
1498 		} else
1499 		{	zap_deferred();
1500 		}
1501 #endif
1502 		return c;
1503 	case '\n':		/* newline */
1504 		lineno++;
1505 		/* make most semi-colons optional */
1506 		if (implied_semis
1507 	/*	&&  context	*/
1508 		&&  in_seq
1509 		&&  par_cnt == 0
1510 		&&  follows_token(last_token))
1511 		{	if (last_token == '}')
1512 			{	do {	c = Getchar();
1513 					if (c == '\n')
1514 					{	lineno++;
1515 					}
1516 				} while (c == ' ' || c == '\t' ||
1517 					 c == '\f' || c == '\n' ||
1518 					 c == '\r');
1519 				Ungetch(c);
1520 				if (0) printf("%d: saw %d\n", lineno, c);
1521 				if (c == 'u') /* first letter of UNLESS */
1522 				{	goto again;
1523 			}	}
1524 			if (0)
1525 			{	printf("insert ; line %d, last_token %d in_seq %d\n",
1526 				 lineno-1, last_token, in_seq);
1527 			}
1528 			ValToken(1, SEMI);
1529 		}
1530 		/* else fall thru */
1531 	case '\r':		/* carriage return */
1532 		goto again;
1533 
1534 	case  ' ': case '\t': case '\f':	/* white space */
1535 		goto again;
1536 
1537 	case '#':		/* preprocessor directive */
1538 		if (in_comment) goto again;
1539 		if (pp_mode)
1540 		{	last_token = PREPROC;
1541 			return pre_proc();
1542 		}
1543 		do_directive(c);
1544 		goto again;
1545 
1546 	case '\"':
1547 		getword(c, notquote);
1548 		if (Getchar() != '\"')
1549 			fatal("string not terminated", yytext);
1550 		strcat(yytext, "\"");
1551 		SymToken(lookup(yytext), STRING)
1552 
1553 	case '$':
1554 		getword('\"', notdollar);
1555 		if (Getchar() != '$')
1556 			fatal("ltl definition not terminated", yytext);
1557 		strcat(yytext, "\"");
1558 		SymToken(lookup(yytext), STRING)
1559 
1560 	case '\'':	/* new 3.0.9 */
1561 		c = Getchar();
1562 		if (c == '\\')
1563 		{	c = Getchar();
1564 			if (c == 'n') c = '\n';
1565 			else if (c == 'r') c = '\r';
1566 			else if (c == 't') c = '\t';
1567 			else if (c == 'f') c = '\f';
1568 		}
1569 		if (Getchar() != '\'' && !in_comment)
1570 			fatal("character quote missing: %s", yytext);
1571 		ValToken(c, CONST)
1572 
1573 	default:
1574 		break;
1575 	}
1576 
1577 	if (isdigit_(c))
1578 	{	long int nr;
1579 		getword(c, isdigit_);
1580 		errno = 0;
1581 		nr = strtol(yytext, NULL, 10);
1582 		if (errno != 0)
1583 		{	fprintf(stderr, "spin: value out of range: '%s' read as '%d'\n",
1584 				yytext, (int) nr);
1585 		}
1586 		ValToken((int)nr, CONST)
1587 	}
1588 
1589 	if (isalpha_(c) || c == '_')
1590 	{	getword(c, isalnum_);
1591 		if (!in_comment)
1592 		{	c = check_name(yytext);
1593 
1594 /* replace timeout with (timeout) */
1595 			if (c == TIMEOUT
1596 			&&  Inlining < 0
1597 			&&  last_token != '(')
1598 			{	push_back("timeout)");
1599 				last_token = '(';
1600 				return '(';
1601 			}
1602 /* end */
1603 
1604 #ifdef EXPAND_SELECT
1605 			if (c == SELECT && Inlining < 0)
1606 			{	char name[64], from[32], upto[32];
1607 				int i, a, b;
1608 				new_select();
1609 				if (!scan_to('(', 0, 0, 0)
1610 				||  !scan_to(':', isalnum, name, sizeof(name))
1611 				||  !scan_to('.', isdigit, from, sizeof(from))
1612 				||  !scan_to('.', 0, 0, 0)
1613 				||  !scan_to(')', isdigit, upto, sizeof(upto)))
1614 				{	goto not_expanded;
1615 				}
1616 				a = atoi(from);
1617 				b = atoi(upto);
1618 				if (0)
1619 				{	printf("Select %s from %d to %d\n",
1620 						name, a, b);
1621 				}
1622 				if (a > b)
1623 				{	non_fatal("bad range in select statement", 0);
1624 					goto again;
1625 				}
1626 				if (b - a <= 32)
1627 				{	push_back("if ");
1628 					for (i = a; i <= b; i++)
1629 					{	char buf[256];
1630 						push_back(":: ");
1631 						sprintf(buf, "%s = %d ",
1632 							name, i);
1633 						push_back(buf);
1634 					}
1635 					push_back("fi ");
1636 				} else
1637 				{	char buf[256];
1638 					sprintf(buf, "%s = %d; do ",
1639 						name, a);
1640 					push_back(buf);
1641 					sprintf(buf, ":: (%s < %d) -> %s++ ",
1642 						name, b, name);
1643 					push_back(buf);
1644 					push_back(":: break od; ");
1645 				}
1646 				goto again;
1647 			}
1648 not_expanded:
1649 #endif
1650 
1651 #ifdef DEFER_LTL
1652 			if (c == LTL && !deferred)
1653 			{	if (put_deferred())
1654 				{	goto again;
1655 			}	}
1656 #endif
1657 			if (c)
1658 			{	last_token = c;
1659 				return c;
1660 			}
1661 			/* else fall through */
1662 		}
1663 		goto again;
1664 	}
1665 
1666 	if (ltl_mode)
1667 	{	switch (c) {
1668 		case '-': c = follow('>', IMPLIES,    '-'); break;
1669 		case '[': c = follow(']', ALWAYS,     '['); break;
1670 		case '<': c = follow('>', EVENTUALLY, '<');
1671 			  if (c == '<')
1672 			  {	c = Getchar();
1673 				if (c == '-')
1674 				{	c = follow('>', EQUIV, '-');
1675 					if (c == '-')
1676 					{	Ungetch(c);
1677 						c = '<';
1678 					}
1679 				} else
1680 				{	Ungetch(c);
1681 					c = '<';
1682 			  }	}
1683 		default:  break;
1684 	}	}
1685 
1686 	switch (c) {
1687 	case '/': c = follow('*', 0, '/');
1688 		  if (!c) { in_comment = 1; goto again; }
1689 		  break;
1690 	case '*': c = follow('/', 0, '*');
1691 		  if (!c) { in_comment = 0; goto again; }
1692 		  break;
1693 	case ':': c = follow(':', SEP, ':'); break;
1694 	case '-': c = follow('>', ARROW, follow('-', DECR, '-')); break;
1695 	case '+': c = follow('+', INCR, '+'); break;
1696 	case '<': c = follow('<', LSHIFT, follow('=', LE, LT)); break;
1697 	case '>': c = follow('>', RSHIFT, follow('=', GE, GT)); break;
1698 	case '=': c = follow('=', EQ, ASGN); break;
1699 	case '!': c = follow('=', NE, follow('!', O_SND, SND)); break;
1700 	case '?': c = follow('?', R_RCV, RCV); break;
1701 	case '&': c = follow('&', AND, '&'); break;
1702 	case '|': c = follow('|', OR, '|'); break;
1703 	case ';': c = SEMI; break;
1704 	case '.': c = follow('.', DOTDOT, '.'); break;
1705 	case '{': scope_seq[scope_level++]++; set_cur_scope(); break;
1706 	case '}': scope_level--; set_cur_scope(); break;
1707 	default : break;
1708 	}
1709 	ValToken(0, c)
1710 }
1711 
1712 static struct {
1713 	char *s;	int tok;
1714 } LTL_syms[] = {
1715 	/* [], <>, ->, and <-> are intercepted in lex() */
1716 	{ "U",		UNTIL   },
1717 	{ "V",		RELEASE },
1718 	{ "W",		WEAK_UNTIL },
1719 	{ "X",		NEXT    },
1720 	{ "always",	ALWAYS  },
1721 	{ "eventually",	EVENTUALLY },
1722 	{ "until",	UNTIL   },
1723 	{ "stronguntil",UNTIL   },
1724 	{ "weakuntil",	WEAK_UNTIL   },
1725 	{ "release",	RELEASE },
1726 	{ "next",	NEXT    },
1727 	{ "implies",	IMPLIES },
1728 	{ "equivalent",	EQUIV   },
1729 	{ 0, 		0       },
1730 };
1731 
1732 static struct {
1733 	char *s;	int tok;	int val;	char *sym;
1734 } Names[] = {
1735 	{"active",	ACTIVE,		0,		0},
1736 	{"assert",	ASSERT,		0,		0},
1737 	{"atomic",	ATOMIC,		0,		0},
1738 	{"bit",		TYPE,		BIT,		0},
1739 	{"bool",	TYPE,		BIT,		0},
1740 	{"break",	BREAK,		0,		0},
1741 	{"byte",	TYPE,		BYTE,		0},
1742 	{"c_code",	C_CODE,		0,		0},
1743 	{"c_decl",	C_DECL,		0,		0},
1744 	{"c_expr",	C_EXPR,		0,		0},
1745 	{"c_state",	C_STATE,	0,		0},
1746 	{"c_track",	C_TRACK,	0,		0},
1747 	{"D_proctype",	D_PROCTYPE,	0,		0},
1748 	{"do",		DO,		0,		0},
1749 	{"chan",	TYPE,		CHAN,		0},
1750 	{"else", 	ELSE,		0,		0},
1751 	{"empty",	EMPTY,		0,		0},
1752 	{"enabled",	ENABLED,	0,		0},
1753 	{"eval",	EVAL,		0,		0},
1754 	{"false",	CONST,		0,		0},
1755 	{"fi",		FI,		0,		0},
1756 	{"for",		FOR,		0,		0},
1757 	{"full",	FULL,		0,		0},
1758 	{"get_priority", GET_P,		0,		0},
1759 	{"goto",	GOTO,		0,		0},
1760 	{"hidden",	HIDDEN,		0,		":hide:"},
1761 	{"if",		IF,		0,		0},
1762 	{"in",		IN,		0,		0},
1763 	{"init",	INIT,		0,		":init:"},
1764 	{"inline",	INLINE,		0,		0},
1765 	{"int",		TYPE,		INT,		0},
1766 	{"len",		LEN,		0,		0},
1767 	{"local",	ISLOCAL,	0,		":local:"},
1768 	{"ltl",		LTL,		0,		":ltl:"},
1769 	{"mtype",	TYPE,		MTYPE,		0},
1770 	{"nempty",	NEMPTY,		0,		0},
1771 	{"never",	CLAIM,		0,		":never:"},
1772 	{"nfull",	NFULL,		0,		0},
1773 	{"notrace",	TRACE,		0,		":notrace:"},
1774 	{"np_",		NONPROGRESS,	0,		0},
1775 	{"od",		OD,		0,		0},
1776 	{"of",		OF,		0,		0},
1777 	{"pc_value",	PC_VAL,		0,		0},
1778 	{"pid",		TYPE,		BYTE,		0},
1779 	{"printf",	PRINT,		0,		0},
1780 	{"printm",	PRINTM,		0,		0},
1781 	{"priority",	PRIORITY,	0,		0},
1782 	{"proctype",	PROCTYPE,	0,		0},
1783 	{"provided",	PROVIDED,	0,		0},
1784 	{"return",	RETURN,		0,		0},
1785 	{"run",		RUN,		0,		0},
1786 	{"d_step",	D_STEP,		0,		0},
1787 	{"select",	SELECT,		0,		0},
1788 	{"set_priority", SET_P,		0,		0},
1789 	{"short",	TYPE,		SHORT,		0},
1790 	{"skip",	CONST,		1,		0},
1791 	{"timeout",	TIMEOUT,	0,		0},
1792 	{"trace",	TRACE,		0,		":trace:"},
1793 	{"true",	CONST,		1,		0},
1794 	{"show",	SHOW,		0,		":show:"},
1795 	{"typedef",	TYPEDEF,	0,		0},
1796 	{"unless",	UNLESS,		0,		0},
1797 	{"unsigned",	TYPE,		UNSIGNED,	0},
1798 	{"xr",		XU,		XR,		0},
1799 	{"xs",		XU,		XS,		0},
1800 	{0, 		0,		0,		0},
1801 };
1802 
1803 static int
check_name(char * s)1804 check_name(char *s)
1805 {	int i;
1806 
1807 	yylval = nn(ZN, 0, ZN, ZN);
1808 
1809 	if (ltl_mode)
1810 	{	for (i = 0; LTL_syms[i].s; i++)
1811 		{	if (strcmp(s, LTL_syms[i].s) == 0)
1812 			{	return LTL_syms[i].tok;
1813 	}	}	}
1814 
1815 	for (i = 0; Names[i].s; i++)
1816 	{	if (strcmp(s, Names[i].s) == 0)
1817 		{	yylval->val = Names[i].val;
1818 			if (Names[i].sym)
1819 				yylval->sym = lookup(Names[i].sym);
1820 			if (Names[i].tok == IN && !in_for)
1821 			{	continue;
1822 			}
1823 			return Names[i].tok;
1824 	}	}
1825 
1826 	if ((yylval->val = ismtype(s)) != 0)
1827 	{	yylval->ismtyp = 1;
1828 		yylval->sym = (Symbol *) emalloc(sizeof(Symbol));
1829 		yylval->sym->name = (char *) emalloc(strlen(s)+1);
1830 		strcpy(yylval->sym->name, s);
1831 		return CONST;
1832 	}
1833 
1834 	if (strcmp(s, "_last") == 0)
1835 		has_last++;
1836 
1837 	if (strcmp(s, "_priority") == 0)
1838 		has_priority++;
1839 
1840 	if (Inlining >= 0 && !ReDiRect)
1841 	{	Lextok *tt, *t = Inline_stub[Inlining]->params;
1842 
1843 		for (i = 0; t; t = t->rgt, i++)				/* formal pars */
1844 		 if (!strcmp(s, t->lft->sym->name)			/* varname matches formal */
1845 		 &&   strcmp(s, Inline_stub[Inlining]->anms[i]) != 0)	/* actual pars */
1846 		 {
1847 #if 0
1848 			if (verbose&32)
1849 			printf("\tline %d, replace %s in call of '%s' with %s\n",
1850 				lineno, s,
1851 				Inline_stub[Inlining]->nm->name,
1852 				Inline_stub[Inlining]->anms[i]);
1853 #endif
1854 			for (tt = Inline_stub[Inlining]->params; tt; tt = tt->rgt)
1855 				if (!strcmp(Inline_stub[Inlining]->anms[i],
1856 					tt->lft->sym->name))
1857 				{	/* would be cyclic if not caught */
1858 					printf("spin: %s:%d replacement value: %s\n",
1859 						oFname->name?oFname->name:"--", lineno, tt->lft->sym->name);
1860 					fatal("formal par of %s contains replacement value",
1861 						Inline_stub[Inlining]->nm->name);
1862 					yylval->ntyp = tt->lft->ntyp;
1863 					yylval->sym = lookup(tt->lft->sym->name);
1864 					return NAME;
1865 				}
1866 
1867 			/* check for occurrence of param as field of struct */
1868 			{ char *ptr = Inline_stub[Inlining]->anms[i];
1869 				char *optr = ptr;
1870 				while ((ptr = strstr(ptr, s)) != NULL)
1871 				{	if ((ptr > optr && *(ptr-1) == '.')
1872 					||  *(ptr+strlen(s)) == '.')
1873 					{	fatal("formal par of %s used in structure name",
1874 						Inline_stub[Inlining]->nm->name);
1875 					}
1876 					ptr++;
1877 			}	}
1878 			ReDiRect = Inline_stub[Inlining]->anms[i];
1879 			return 0;
1880 	}	 }
1881 
1882 	yylval->sym = lookup(s);	/* symbol table */
1883 	if (isutype(s))
1884 		return UNAME;
1885 	if (isproctype(s))
1886 		return PNAME;
1887 	if (iseqname(s))
1888 		return INAME;
1889 
1890 	return NAME;
1891 }
1892 
1893 int
yylex(void)1894 yylex(void)
1895 {	static int last = 0;
1896 	static int hold = 0;
1897 	int c;
1898 	/*
1899 	 * repair two common syntax mistakes with
1900 	 * semi-colons before or after a '}'
1901 	 */
1902 	if (hold)
1903 	{	c = hold;
1904 		hold = 0;
1905 		last_token = c;
1906 	} else
1907 	{	c = lex();
1908 		if (last == ELSE
1909 		&&  c != SEMI
1910 		&&  c != ARROW
1911 		&&  c != FI)
1912 		{	hold = c;
1913 			last = 0;
1914 			last_token = SEMI;
1915 			return SEMI;
1916 		}
1917 		if (last == '}'
1918 		&&  c != PROCTYPE
1919 		&&  c != INIT
1920 		&&  c != CLAIM
1921 		&&  c != SEP
1922 		&&  c != FI
1923 		&&  c != OD
1924 		&&  c != '}'
1925 		&&  c != UNLESS
1926 		&&  c != SEMI
1927 		&&  c != ARROW
1928 		&&  c != EOF)
1929 		{	hold = c;
1930 			last = 0;
1931 			last_token = SEMI;
1932 			return SEMI;	/* insert ';' */
1933 		}
1934 		if (c == SEMI || c == ARROW)
1935 		{	/* if context, we're not in a typedef
1936 			 * because they're global.
1937 			 * if owner, we're at the end of a ref
1938 			 * to a struct field -- prevent that the
1939 			 * lookahead is interpreted as a field of
1940 			 * the same struct...
1941 			 */
1942 			if (context) owner = ZS;
1943 			hold = lex();	/* look ahead */
1944 			if (hold == '}'
1945 			||  hold == ARROW
1946 			||  hold == SEMI)
1947 			{	c = hold; /* omit ';' */
1948 				hold = 0;
1949 			}
1950 		}
1951 	}
1952 	last = c;
1953 
1954 	if (IArgs)
1955 	{	static int IArg_nst = 0;
1956 
1957 		if (strcmp(yytext, ",") == 0)
1958 		{	IArg_cont[++IArgno][0] = '\0';
1959 		} else if (strcmp(yytext, "(") == 0)
1960 		{	if (IArg_nst++ == 0)
1961 			{	IArgno = 0;
1962 				IArg_cont[0][0] = '\0';
1963 			} else
1964 			{	assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
1965 				strcat(IArg_cont[IArgno], yytext);
1966 			}
1967 		} else if (strcmp(yytext, ")") == 0)
1968 		{	if (--IArg_nst > 0)
1969 			{	assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
1970 				strcat(IArg_cont[IArgno], yytext);
1971 			}
1972 		} else if (c == CONST && yytext[0] == '\'')
1973 		{	sprintf(yytext, "'%c'", yylval->val);
1974 			assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
1975 			strcat(IArg_cont[IArgno], yytext);
1976 		} else if (c == CONST)
1977 		{	sprintf(yytext, "%d", yylval->val);
1978 			assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
1979 			strcat(IArg_cont[IArgno], yytext);
1980 		} else
1981 		{
1982 			switch (c) {
1983 			case ARROW:	strcpy(yytext, "->"); break; /* NEW */
1984 			case SEP:	strcpy(yytext, "::"); break;
1985 			case SEMI:	strcpy(yytext, ";"); break;
1986 			case DECR:	strcpy(yytext, "--"); break;
1987 			case INCR: 	strcpy(yytext, "++"); break;
1988 			case LSHIFT:	strcpy(yytext, "<<"); break;
1989 			case RSHIFT:	strcpy(yytext, ">>"); break;
1990 			case LE:	strcpy(yytext, "<="); break;
1991 			case LT:	strcpy(yytext, "<"); break;
1992 			case GE:	strcpy(yytext, ">="); break;
1993 			case GT:	strcpy(yytext, ">"); break;
1994 			case EQ:	strcpy(yytext, "=="); break;
1995 			case ASGN:	strcpy(yytext, "="); break;
1996 			case NE:	strcpy(yytext, "!="); break;
1997 			case R_RCV:	strcpy(yytext, "??"); break;
1998 			case RCV:	strcpy(yytext, "?"); break;
1999 			case O_SND:	strcpy(yytext, "!!"); break;
2000 			case SND:	strcpy(yytext, "!"); break;
2001 			case AND: 	strcpy(yytext, "&&"); break;
2002 			case OR:	strcpy(yytext, "||"); break;
2003 			}
2004 			assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
2005 			strcat(IArg_cont[IArgno], yytext);
2006 		}
2007 	}
2008 	return c;
2009 }
2010