1 /***** spin: spinlex.c *****/
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 */
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 */
20 typedef struct IType
{
21 Symbol
*nm
; /* name of the type */
22 Lextok
*cn
; /* contents */
23 Lextok
*params
; /* formal pars if any */
24 char **anms
; /* literal text for actual pars */
25 char *prec
; /* precondition for c_code or c_expr */
26 int dln
, cln
; /* def and call linenr */
27 Symbol
*dfn
, *cfn
; /* def and call filename */
28 struct IType
*nxt
; /* linked list */
31 typedef struct C_Added
{
41 extern Symbol
*context
, *owner
;
42 extern YYSTYPE yylval
;
43 extern short has_last
, has_code
;
44 extern int verbose
, IArgs
, hastrack
, separate
;
51 static C_Added
*c_added
, *c_tracked
;
52 static IType
*Inline_stub
[MAXINL
];
53 static char *ReDiRect
;
54 static char *Inliner
[MAXINL
], IArg_cont
[MAXPAR
][MAXLEN
];
55 static unsigned char in_comment
=0;
56 static int IArgno
= 0, Inlining
= -1;
57 static int check_name(char *);
60 #define Token(y) { if (in_comment) goto again; \
61 yylval = nn(ZN,0,ZN,ZN); return y; }
63 #define ValToken(x, y) { if (in_comment) goto again; \
64 yylval = nn(ZN,0,ZN,ZN); yylval->val = x; return y; }
66 #define SymToken(x, y) { if (in_comment) goto again; \
67 yylval = nn(ZN,0,ZN,ZN); yylval->sym = x; return y; }
69 #define Token(y) { yylval = nn(ZN,0,ZN,ZN); \
70 if (!in_comment) return y; else goto again; }
72 #define ValToken(x, y) { yylval = nn(ZN,0,ZN,ZN); yylval->val = x; \
73 if (!in_comment) return y; else goto again; }
75 #define SymToken(x, y) { yylval = nn(ZN,0,ZN,ZN); yylval->sym = x; \
76 if (!in_comment) return y; else goto again; }
79 static int getinline(void);
80 static void uninline(void);
83 #define Getchar() ((Inlining<0)?getc(yyin):getinline())
84 #define Ungetch(c) {if (Inlining<0) ungetc(c,yyin); else uninline(); }
96 { printf("<%c:%d>[%d] ", c
, c
, Inlining
);
116 { return (c
!= '\"' && c
!= '\n');
121 { return (isalnum(c
) || c
== '_');
126 { return isalpha(c
); /* could be macro */
131 { return isdigit(c
); /* could be macro */
135 getword(int first
, int (*tst
)(int))
138 yytext
[i
++]= (char) first
;
139 while (tst(c
= Getchar()))
140 { yytext
[i
++] = (char) c
;
143 yytext
[i
++] = (char) c
; /* no tst */
150 follow(int tok
, int ifyes
, int ifno
)
153 if ((c
= Getchar()) == tok
)
160 static IType
*seqnames
;
163 def_inline(Symbol
*s
, int ln
, char *ptr
, char *prc
, Lextok
*nms
)
165 char *nw
= (char *) emalloc(strlen(ptr
)+1);
168 for (tmp
= seqnames
; tmp
; tmp
= tmp
->nxt
)
169 if (!strcmp(s
->name
, tmp
->nm
->name
))
170 { non_fatal("procedure name %s redefined",
172 tmp
->cn
= (Lextok
*) nw
;
178 tmp
= (IType
*) emalloc(sizeof(IType
));
180 tmp
->cn
= (Lextok
*) nw
;
183 { tmp
->prec
= (char *) emalloc(strlen(prc
)+1);
184 strcpy(tmp
->prec
, prc
);
193 gencodetable(FILE *fd
)
198 if (separate
== 2) return;
200 fprintf(fd
, "struct {\n");
201 fprintf(fd
, " char *c; char *t;\n");
202 fprintf(fd
, "} code_lookup[] = {\n");
205 for (tmp
= seqnames
; tmp
; tmp
= tmp
->nxt
)
206 if (tmp
->nm
->type
== CODE_FRAG
207 || tmp
->nm
->type
== CODE_DECL
)
208 { fprintf(fd
, "\t{ \"%s\", ",
210 q
= (char *) tmp
->cn
;
212 while (*q
== '\n' || *q
== '\r' || *q
== '\\')
217 while (*q
&& cnt
< 1024) /* pangen1.h allows 2048 */
234 if (*q
) fprintf(fd
, "...");
236 fprintf(fd
, " },\n");
239 fprintf(fd
, " { (char *) 0, \"\" }\n");
247 for (tmp
= seqnames
; tmp
; tmp
= tmp
->nxt
)
248 { if (!strcmp(t
, tmp
->nm
->name
))
261 { ReDiRect
= (char *) 0;
262 c
= *Inliner
[Inlining
]++;
265 c
= *Inliner
[Inlining
]++;
268 { lineno
= Inline_stub
[Inlining
]->cln
;
269 Fname
= Inline_stub
[Inlining
]->cfn
;
273 printf("spin: line %d, done inlining %s\n",
274 lineno
, Inline_stub
[Inlining
+1]->nm
->name
);
294 for (tmp
= seqnames
; tmp
; tmp
= tmp
->nxt
)
295 if (!strcmp(s
, tmp
->nm
->name
))
298 fatal("cannot happen, missing inline def %s", s
);
304 c_state(Symbol
*s
, Symbol
*t
, Symbol
*ival
) /* name, scope, ival */
307 r
= (C_Added
*) emalloc(sizeof(C_Added
));
308 r
->s
= s
; /* pointer to a data object */
309 r
->t
= t
; /* size of object, or "global", or "local proctype_name" */
316 c_track(Symbol
*s
, Symbol
*t
, Symbol
*stackonly
) /* name, size */
319 r
= (C_Added
*) emalloc(sizeof(C_Added
));
322 r
->ival
= stackonly
; /* abuse of name */
327 { if (strcmp(stackonly
->name
, "\"Matched\"") == 0)
328 r
->ival
= ZS
; /* the default */
329 else if (strcmp(stackonly
->name
, "\"UnMatched\"") != 0
330 && strcmp(stackonly
->name
, "\"unMatched\"") != 0
331 && strcmp(stackonly
->name
, "\"StackOnly\"") != 0)
332 non_fatal("expecting '[Un]Matched', saw %s", stackonly
->name
);
334 has_stack
= 1; /* unmatched stack */
342 /* kludgy - try to get the type separated from the name */
344 while (*p
== ' ' || *p
== '\t')
345 p
++; /* initial white space */
346 while (*p
!= ' ' && *p
!= '\t')
348 while (*p
== ' ' || *p
== '\t')
349 p
++; /* white space */
351 p
++; /* decorations */
352 while (*p
== ' ' || *p
== '\t')
353 p
++; /* white space */
356 fatal("c_state format (%s)", op
);
360 { non_fatal("array initialization error, c_state (%s)", p
);
368 c_add_globinit(FILE *fd
)
372 fprintf(fd
, "void\nglobinit(void)\n{\n");
373 for (r
= c_added
; r
; r
= r
->nxt
)
377 if (strncmp(r
->t
->name
, " Global ", strlen(" Global ")) == 0)
378 { for (q
= r
->ival
->name
; *q
; q
++)
382 *q
++ = ' '; /* skip over the next */
384 p
= jump_etc(r
->s
->name
); /* e.g., "int **q" */
386 fprintf(fd
, " now.%s = %s;\n", p
, r
->ival
->name
);
389 if (strncmp(r
->t
->name
, " Hidden ", strlen(" Hidden ")) == 0)
390 { for (q
= r
->ival
->name
; *q
; q
++)
394 *q
++ = ' '; /* skip over the next */
396 p
= jump_etc(r
->s
->name
); /* e.g., "int **q" */
398 fprintf(fd
, " %s = %s;\n", p
, r
->ival
->name
); /* no now. prefix */
405 c_add_locinit(FILE *fd
, int tpnr
, char *pnm
)
410 fprintf(fd
, "void\nlocinit%d(int h)\n{\n", tpnr
);
411 for (r
= c_added
; r
; r
= r
->nxt
)
413 && strncmp(r
->t
->name
, " Local", strlen(" Local")) == 0)
414 { for (q
= r
->ival
->name
; *q
; q
++)
418 p
= jump_etc(r
->s
->name
); /* e.g., "int **q" */
420 q
= r
->t
->name
+ strlen(" Local");
421 while (*q
== ' ' || *q
== '\t')
422 q
++; /* process name */
424 s
= (char *) emalloc(strlen(q
)+1);
428 while (*q
== ' ' || *q
== '\t')
431 if (strcmp(pnm
, s
) != 0)
435 { fprintf(fd
, "\tuchar *this = pptr(h);\n");
440 fprintf(fd
, " ((P%d *)this)->%s = %s;\n",
441 tpnr
, p
, r
->ival
->name
);
448 1. for non-global and non-local c_state decls: add up all the sizes in c_added
449 2. add a global char array of that size into now
450 3. generate a routine that memcpy's the required values into that array
451 4. generate a call to that routine
462 for (r
= c_added
; r
; r
= r
->nxt
)
463 if (strncmp(r
->t
->name
, " Global ", strlen(" Global ")) != 0
464 && strncmp(r
->t
->name
, " Hidden ", strlen(" Hidden ")) != 0
465 && strncmp(r
->t
->name
, " Local", strlen(" Local")) != 0)
466 { hastrack
= 1; /* c_state variant now obsolete */
472 c_add_sv(FILE *fd
) /* 1+2 -- called in pangen1.c */
476 if (!c_added
&& !c_tracked
) return 0;
478 for (r
= c_added
; r
; r
= r
->nxt
) /* pickup global decls */
479 if (strncmp(r
->t
->name
, " Global ", strlen(" Global ")) == 0)
480 fprintf(fd
, " %s;\n", r
->s
->name
);
482 for (r
= c_added
; r
; r
= r
->nxt
)
483 if (strncmp(r
->t
->name
, " Global ", strlen(" Global ")) != 0
484 && strncmp(r
->t
->name
, " Hidden ", strlen(" Hidden ")) != 0
485 && strncmp(r
->t
->name
, " Local", strlen(" Local")) != 0)
486 { cnt
++; /* obsolete use */
489 for (r
= c_tracked
; r
; r
= r
->nxt
)
490 cnt
++; /* preferred use */
492 if (cnt
== 0) return 0;
495 fprintf(fd
, " uchar c_state[");
496 for (r
= c_added
; r
; r
= r
->nxt
)
497 if (strncmp(r
->t
->name
, " Global ", strlen(" Global ")) != 0
498 && strncmp(r
->t
->name
, " Hidden ", strlen(" Hidden ")) != 0
499 && strncmp(r
->t
->name
, " Local", strlen(" Local")) != 0)
500 { fprintf(fd
, "%ssizeof(%s)",
501 (cnt
==0)?"":"+", r
->t
->name
);
505 for (r
= c_tracked
; r
; r
= r
->nxt
)
506 { if (r
->ival
!= ZS
) continue;
509 (cnt
==0)?"":"+", r
->t
->name
);
513 if (cnt
== 0) fprintf(fd
, "4"); /* now redundant */
519 c_stack_size(FILE *fd
)
523 for (r
= c_tracked
; r
; r
= r
->nxt
)
525 { fprintf(fd
, "%s%s",
526 (cnt
==0)?"":"+", r
->t
->name
);
535 c_add_stack(FILE *fd
)
539 if ((!c_added
&& !c_tracked
) || !has_stack
)
543 for (r
= c_tracked
; r
; r
= r
->nxt
)
549 { fprintf(fd
, " uchar c_stack[StackSize];\n");
554 c_add_hidden(FILE *fd
)
557 for (r
= c_added
; r
; r
= r
->nxt
) /* pickup hidden decls */
558 if (strncmp(r
->t
->name
, "\"Hidden\"", strlen("\"Hidden\"")) == 0)
559 { r
->s
->name
[strlen(r
->s
->name
)-1] = ' ';
560 fprintf(fd
, "%s; /* Hidden */\n", &r
->s
->name
[1]);
561 r
->s
->name
[strlen(r
->s
->name
)-1] = '"';
563 /* called before c_add_def - quotes are still there */
567 c_add_loc(FILE *fd
, char *s
) /* state vector entries for proctype s */
569 static char buf
[1024];
572 if (!c_added
) return;
576 for (r
= c_added
; r
; r
= r
->nxt
) /* pickup local decls */
577 if (strncmp(r
->t
->name
, " Local", strlen(" Local")) == 0)
578 { p
= r
->t
->name
+ strlen(" Local");
579 while (*p
== ' ' || *p
== '\t')
581 if (strcmp(p
, buf
) == 0)
582 fprintf(fd
, " %s;\n", r
->s
->name
);
586 c_add_def(FILE *fd
) /* 3 - called in plunk_c_fcts() */
589 fprintf(fd
, "#if defined(C_States) && defined(HAS_TRACK)\n");
590 for (r
= c_added
; r
; r
= r
->nxt
)
591 { r
->s
->name
[strlen(r
->s
->name
)-1] = ' ';
592 r
->s
->name
[0] = ' '; /* remove the "s */
594 r
->t
->name
[strlen(r
->t
->name
)-1] = ' ';
597 if (strncmp(r
->t
->name
, " Global ", strlen(" Global ")) == 0
598 || strncmp(r
->t
->name
, " Hidden ", strlen(" Hidden ")) == 0
599 || strncmp(r
->t
->name
, " Local", strlen(" Local")) == 0)
602 if (strchr(r
->s
->name
, '&'))
603 fatal("dereferencing state object: %s", r
->s
->name
);
605 fprintf(fd
, "extern %s %s;\n", r
->t
->name
, r
->s
->name
);
607 for (r
= c_tracked
; r
; r
= r
->nxt
)
608 { r
->s
->name
[strlen(r
->s
->name
)-1] = ' ';
609 r
->s
->name
[0] = ' '; /* remove " */
611 r
->t
->name
[strlen(r
->t
->name
)-1] = ' ';
616 { fprintf(fd
, "#endif\n");
621 { fprintf(fd
, "int cpu_printf(const char *, ...);\n");
622 fprintf(fd
, "void\nc_stack(uchar *p_t_r)\n{\n");
623 fprintf(fd
, "#ifdef VERBOSE\n");
624 fprintf(fd
, " cpu_printf(\"c_stack %%u\\n\", p_t_r);\n");
625 fprintf(fd
, "#endif\n");
626 for (r
= c_tracked
; r
; r
= r
->nxt
)
627 { if (r
->ival
== ZS
) continue;
629 fprintf(fd
, "\tif(%s)\n", r
->s
->name
);
630 fprintf(fd
, "\t\tmemcpy(p_t_r, %s, %s);\n",
631 r
->s
->name
, r
->t
->name
);
632 fprintf(fd
, "\telse\n");
633 fprintf(fd
, "\t\tmemset(p_t_r, 0, %s);\n",
635 fprintf(fd
, "\tp_t_r += %s;\n", r
->t
->name
);
637 fprintf(fd
, "}\n\n");
640 fprintf(fd
, "void\nc_update(uchar *p_t_r)\n{\n");
641 fprintf(fd
, "#ifdef VERBOSE\n");
642 fprintf(fd
, " printf(\"c_update %%u\\n\", p_t_r);\n");
643 fprintf(fd
, "#endif\n");
644 for (r
= c_added
; r
; r
= r
->nxt
)
645 { if (strncmp(r
->t
->name
, " Global ", strlen(" Global ")) == 0
646 || strncmp(r
->t
->name
, " Hidden ", strlen(" Hidden ")) == 0
647 || strncmp(r
->t
->name
, " Local", strlen(" Local")) == 0)
650 fprintf(fd
, "\tmemcpy(p_t_r, &%s, sizeof(%s));\n",
651 r
->s
->name
, r
->t
->name
);
652 fprintf(fd
, "\tp_t_r += sizeof(%s);\n", r
->t
->name
);
655 for (r
= c_tracked
; r
; r
= r
->nxt
)
656 { if (r
->ival
) continue;
658 fprintf(fd
, "\tif(%s)\n", r
->s
->name
);
659 fprintf(fd
, "\t\tmemcpy(p_t_r, %s, %s);\n",
660 r
->s
->name
, r
->t
->name
);
661 fprintf(fd
, "\telse\n");
662 fprintf(fd
, "\t\tmemset(p_t_r, 0, %s);\n",
664 fprintf(fd
, "\tp_t_r += %s;\n", r
->t
->name
);
670 { fprintf(fd
, "void\nc_unstack(uchar *p_t_r)\n{\n");
671 fprintf(fd
, "#ifdef VERBOSE\n");
672 fprintf(fd
, " cpu_printf(\"c_unstack %%u\\n\", p_t_r);\n");
673 fprintf(fd
, "#endif\n");
674 for (r
= c_tracked
; r
; r
= r
->nxt
)
675 { if (r
->ival
== ZS
) continue;
677 fprintf(fd
, "\tif(%s)\n", r
->s
->name
);
678 fprintf(fd
, "\t\tmemcpy(%s, p_t_r, %s);\n",
679 r
->s
->name
, r
->t
->name
);
680 fprintf(fd
, "\tp_t_r += %s;\n", r
->t
->name
);
685 fprintf(fd
, "void\nc_revert(uchar *p_t_r)\n{\n");
686 fprintf(fd
, "#ifdef VERBOSE\n");
687 fprintf(fd
, " printf(\"c_revert %%u\\n\", p_t_r);\n");
688 fprintf(fd
, "#endif\n");
689 for (r
= c_added
; r
; r
= r
->nxt
)
690 { if (strncmp(r
->t
->name
, " Global ", strlen(" Global ")) == 0
691 || strncmp(r
->t
->name
, " Hidden ", strlen(" Hidden ")) == 0
692 || strncmp(r
->t
->name
, " Local", strlen(" Local")) == 0)
695 fprintf(fd
, "\tmemcpy(&%s, p_t_r, sizeof(%s));\n",
696 r
->s
->name
, r
->t
->name
);
697 fprintf(fd
, "\tp_t_r += sizeof(%s);\n", r
->t
->name
);
699 for (r
= c_tracked
; r
; r
= r
->nxt
)
700 { if (r
->ival
!= ZS
) continue;
702 fprintf(fd
, "\tif(%s)\n", r
->s
->name
);
703 fprintf(fd
, "\t\tmemcpy(%s, p_t_r, %s);\n",
704 r
->s
->name
, r
->t
->name
);
705 fprintf(fd
, "\tp_t_r += %s;\n", r
->t
->name
);
709 fprintf(fd
, "#endif\n");
713 plunk_reverse(FILE *fd
, IType
*p
, int matchthis
)
717 plunk_reverse(fd
, p
->nxt
, matchthis
);
720 && p
->nm
->type
== matchthis
)
721 { fprintf(fd
, "\n/* start of %s */\n", p
->nm
->name
);
723 while (*z
== '\n' || *z
== '\r' || *z
== '\\')
725 /* e.g.: \#include "..." */
728 while ((y
= strstr(y
, "\\#")) != NULL
)
732 fprintf(fd
, "%s\n", z
);
733 fprintf(fd
, "\n/* end of %s */\n", p
->nm
->name
);
738 plunk_c_decls(FILE *fd
)
740 plunk_reverse(fd
, seqnames
, CODE_DECL
);
744 plunk_c_fcts(FILE *fd
)
746 if (separate
== 2 && hastrack
)
752 plunk_reverse(fd
, seqnames
, CODE_FRAG
);
754 if (c_added
|| c_tracked
) /* enables calls to c_revert and c_update */
755 fprintf(fd
, "#define C_States 1\n");
757 fprintf(fd
, "#undef C_States\n");
767 check_inline(IType
*tmp
)
773 for (p
= rdy
; p
; p
= p
->nxt
)
774 { if (strcmp(p
->n
->name
, X
->n
->name
) == 0)
776 sprintf(buf
, "P%s->", p
->n
->name
);
777 if (strstr((char *)tmp
->cn
, buf
))
778 { printf("spin: in proctype %s, ref to object in proctype %s\n",
779 X
->n
->name
, p
->n
->name
);
780 fatal("invalid variable ref in '%s'", tmp
->nm
->name
);
785 plunk_expr(FILE *fd
, char *s
)
788 tmp
= find_inline(s
);
791 fprintf(fd
, "%s", (char *) tmp
->cn
);
795 preruse(FILE *fd
, Lextok
*n
) /* check a condition for c_expr with preconditions */
799 if (n
->ntyp
== C_EXPR
)
800 { tmp
= find_inline(n
->sym
->name
);
802 { fprintf(fd
, "if (!(%s)) { if (!readtrail) { depth++; ", tmp
->prec
);
803 fprintf(fd
, "trpt++; trpt->pr = II; trpt->o_t = t;");
804 fprintf(fd
, "trpt->st = tt; Uerror(\"%s\"); } ", tmp
->prec
);
805 fprintf(fd
, "else { printf(\"pan: precondition false: %s\\n\"); ", tmp
->prec
);
806 fprintf(fd
, "_m = 3; goto P999; } } \n\t\t");
809 { preruse(fd
, n
->rgt
);
819 tmp
= find_inline(s
);
820 bdy
= (char *) tmp
->cn
;
821 return (strstr(bdy
, "now.") /* global ref or */
822 || strchr(bdy
, '(') > bdy
); /* possible C-function call */
826 plunk_inline(FILE *fd
, char *s
, int how
) /* c_code with precondition */
829 tmp
= find_inline(s
);
833 if (how
&& tmp
->prec
)
834 { fprintf(fd
, "if (!(%s)) { if (!readtrail) { depth++; ", tmp
->prec
);
835 fprintf(fd
, "trpt++; trpt->pr = II; trpt->o_t = t;");
836 fprintf(fd
, "trpt->st = tt; Uerror(\"%s\"); } ", tmp
->prec
);
837 fprintf(fd
, "else { printf(\"pan: precondition false: %s\\n\"); ", tmp
->prec
);
838 fprintf(fd
, "_m = 3; goto P999; } } ");
840 fprintf(fd
, "%s", (char *) tmp
->cn
);
845 no_side_effects(char *s
)
849 /* could still defeat this check via hidden
850 * side effects in function calls,
851 * but this will catch at least some cases
854 tmp
= find_inline(s
);
855 t
= (char *) tmp
->cn
;
861 bad
: lineno
= tmp
->dln
;
863 non_fatal("c_expr %s has side-effects", s
);
866 while ((t
= strchr(t
, '=')) != NULL
)
881 pickup_inline(Symbol
*t
, Lextok
*apars
)
882 { IType
*tmp
; Lextok
*p
, *q
; int j
;
884 tmp
= find_inline(t
->name
);
886 if (++Inlining
>= MAXINL
)
887 fatal("inline fcts too deeply nested", 0);
888 tmp
->cln
= lineno
; /* remember calling point */
889 tmp
->cfn
= Fname
; /* and filename */
891 for (p
= apars
, q
= tmp
->params
, j
= 0; p
&& q
; p
= p
->rgt
, q
= q
->rgt
)
892 j
++; /* count them */
894 fatal("wrong nr of params on call of '%s'", t
->name
);
896 tmp
->anms
= (char **) emalloc(j
* sizeof(char *));
897 for (p
= apars
, j
= 0; p
; p
= p
->rgt
, j
++)
898 { tmp
->anms
[j
] = (char *) emalloc(strlen(IArg_cont
[j
])+1);
899 strcpy(tmp
->anms
[j
], IArg_cont
[j
]);
902 lineno
= tmp
->dln
; /* linenr of def */
903 Fname
= tmp
->dfn
; /* filename of same */
904 Inliner
[Inlining
] = (char *)tmp
->cn
;
905 Inline_stub
[Inlining
] = tmp
;
908 printf("spin: line %d, file %s, inlining '%s' (from line %d, file %s)\n",
909 tmp
->cln
, tmp
->cfn
->name
, t
->name
, tmp
->dln
, tmp
->dfn
->name
);
911 for (j
= 0; j
< Inlining
; j
++)
912 if (Inline_stub
[j
] == Inline_stub
[Inlining
])
913 fatal("cyclic inline attempt on: %s", t
->name
);
917 do_directive(int first
)
918 { int c
= first
; /* handles lines starting with pound */
920 getword(c
, isalpha_
);
922 if (strcmp(yytext
, "#ident") == 0)
925 if ((c
= Getchar()) != ' ')
926 fatal("malformed preprocessor directive - # .", 0);
928 if (!isdigit_(c
= Getchar()))
929 fatal("malformed preprocessor directive - # .lineno", 0);
931 getword(c
, isdigit_
);
932 lineno
= atoi(yytext
); /* pickup the line number */
934 if ((c
= Getchar()) == '\n')
935 return; /* no filename */
938 fatal("malformed preprocessor directive - .fname", 0);
940 if ((c
= Getchar()) != '\"')
941 fatal("malformed preprocessor directive - .fname", 0);
943 getword(c
, notquote
);
944 if (Getchar() != '\"')
945 fatal("malformed preprocessor directive - fname.", 0);
947 strcat(yytext
, "\"");
948 Fname
= lookup(yytext
);
950 while (Getchar() != '\n')
955 precondition(char *q
)
976 fatal("cannot happen", (char *) 0); /* unreachable */
981 prep_inline(Symbol
*s
, Lextok
*nms
)
982 { int c
, nest
= 1, dln
, firstchar
, cnr
;
985 static char Buf1
[SOMETHINGBIG
], Buf2
[RATHERSMALL
];
986 static int c_code
= 1;
988 for (t
= nms
; t
; t
= t
->rgt
)
990 { if (t
->lft
->ntyp
!= NAME
)
991 fatal("bad param to inline %s", s
?s
->name
:"--");
992 t
->lft
->sym
->hidden
|= 32;
995 if (!s
) /* C_Code fragment */
996 { s
= (Symbol
*) emalloc(sizeof(Symbol
));
997 s
->name
= (char *) emalloc(strlen("c_code")+26);
998 sprintf(s
->name
, "c_code%d", c_code
++);
999 s
->context
= context
;
1000 s
->type
= CODE_FRAG
;
1010 if (s
->type
!= CODE_FRAG
)
1012 precondition(&Buf2
[0]); /* e.g., c_code [p] { r = p-r; } */
1019 case ' ': case '\t': case '\f': case '\r':
1022 printf("spin: saw char '%c'\n", c
);
1023 bad
: fatal("bad inline: %s", s
->name
);
1028 if (s
->type
== CODE_FRAG
)
1030 sprintf(Buf1
, "\t/* line %d %s */\n\t\t",
1031 lineno
, Fname
->name
);
1035 sprintf(Buf1
, "\n#line %d %s\n{", lineno
, Fname
->name
);
1039 cnr
= 1; /* not zero */
1041 *p
++ = c
= Getchar();
1042 if (p
- Buf1
>= SOMETHINGBIG
)
1043 fatal("inline text too long", 0);
1057 if (s
->type
== CODE_FRAG
)
1058 *--p
= '\0'; /* remove trailing '}' */
1059 def_inline(s
, dln
, &Buf1
[0], &Buf2
[0], nms
);
1061 printf("%3d: %s, warning: empty inline definition (%s)\n",
1062 dln
, Fname
->name
, s
->name
);
1063 return s
; /* normal return */
1069 do_directive(c
); /* reads to newline */
1071 } /* else fall through */
1089 yytext
[0] = (char) c
;
1092 case '\n': /* newline */
1094 case '\r': /* carriage return */
1097 case ' ': case '\t': case '\f': /* white space */
1100 case '#': /* preprocessor directive */
1101 if (in_comment
) goto again
;
1106 getword(c
, notquote
);
1107 if (Getchar() != '\"')
1108 fatal("string not terminated", yytext
);
1109 strcat(yytext
, "\"");
1110 SymToken(lookup(yytext
), STRING
)
1112 case '\'': /* new 3.0.9 */
1116 if (c
== 'n') c
= '\n';
1117 else if (c
== 'r') c
= '\r';
1118 else if (c
== 't') c
= '\t';
1119 else if (c
== 'f') c
= '\f';
1121 if (Getchar() != '\'' && !in_comment
)
1122 fatal("character quote missing: %s", yytext
);
1130 { getword(c
, isdigit_
);
1131 ValToken(atoi(yytext
), CONST
)
1134 if (isalpha_(c
) || c
== '_')
1135 { getword(c
, isalnum_
);
1137 { c
= check_name(yytext
);
1139 /* else fall through */
1145 case '/': c
= follow('*', 0, '/');
1146 if (!c
) { in_comment
= 1; goto again
; }
1148 case '*': c
= follow('/', 0, '*');
1149 if (!c
) { in_comment
= 0; goto again
; }
1151 case ':': c
= follow(':', SEP
, ':'); break;
1152 case '-': c
= follow('>', SEMI
, follow('-', DECR
, '-')); break;
1153 case '+': c
= follow('+', INCR
, '+'); break;
1154 case '<': c
= follow('<', LSHIFT
, follow('=', LE
, LT
)); break;
1155 case '>': c
= follow('>', RSHIFT
, follow('=', GE
, GT
)); break;
1156 case '=': c
= follow('=', EQ
, ASGN
); break;
1157 case '!': c
= follow('=', NE
, follow('!', O_SND
, SND
)); break;
1158 case '?': c
= follow('?', R_RCV
, RCV
); break;
1159 case '&': c
= follow('&', AND
, '&'); break;
1160 case '|': c
= follow('|', OR
, '|'); break;
1161 case ';': c
= SEMI
; break;
1168 char *s
; int tok
; int val
; char *sym
;
1170 {"active", ACTIVE
, 0, 0},
1171 {"assert", ASSERT
, 0, 0},
1172 {"atomic", ATOMIC
, 0, 0},
1173 {"bit", TYPE
, BIT
, 0},
1174 {"bool", TYPE
, BIT
, 0},
1175 {"break", BREAK
, 0, 0},
1176 {"byte", TYPE
, BYTE
, 0},
1177 {"c_code", C_CODE
, 0, 0},
1178 {"c_decl", C_DECL
, 0, 0},
1179 {"c_expr", C_EXPR
, 0, 0},
1180 {"c_state", C_STATE
, 0, 0},
1181 {"c_track", C_TRACK
, 0, 0},
1182 {"D_proctype", D_PROCTYPE
, 0, 0},
1184 {"chan", TYPE
, CHAN
, 0},
1185 {"else", ELSE
, 0, 0},
1186 {"empty", EMPTY
, 0, 0},
1187 {"enabled", ENABLED
, 0, 0},
1188 {"eval", EVAL
, 0, 0},
1189 {"false", CONST
, 0, 0},
1191 {"full", FULL
, 0, 0},
1192 {"goto", GOTO
, 0, 0},
1193 {"hidden", HIDDEN
, 0, ":hide:"},
1195 {"init", INIT
, 0, ":init:"},
1196 {"int", TYPE
, INT
, 0},
1198 {"local", ISLOCAL
, 0, ":local:"},
1199 {"mtype", TYPE
, MTYPE
, 0},
1200 {"nempty", NEMPTY
, 0, 0},
1201 {"never", CLAIM
, 0, ":never:"},
1202 {"nfull", NFULL
, 0, 0},
1203 {"notrace", TRACE
, 0, ":notrace:"},
1204 {"np_", NONPROGRESS
, 0, 0},
1207 {"pc_value", PC_VAL
, 0, 0},
1208 {"pid", TYPE
, BYTE
, 0},
1209 {"printf", PRINT
, 0, 0},
1210 {"printm", PRINTM
, 0, 0},
1211 {"priority", PRIORITY
, 0, 0},
1212 {"proctype", PROCTYPE
, 0, 0},
1213 {"provided", PROVIDED
, 0, 0},
1215 {"d_step", D_STEP
, 0, 0},
1216 {"inline", INLINE
, 0, 0},
1217 {"short", TYPE
, SHORT
, 0},
1218 {"skip", CONST
, 1, 0},
1219 {"timeout", TIMEOUT
, 0, 0},
1220 {"trace", TRACE
, 0, ":trace:"},
1221 {"true", CONST
, 1, 0},
1222 {"show", SHOW
, 0, ":show:"},
1223 {"typedef", TYPEDEF
, 0, 0},
1224 {"unless", UNLESS
, 0, 0},
1225 {"unsigned", TYPE
, UNSIGNED
, 0},
1235 yylval
= nn(ZN
, 0, ZN
, ZN
);
1236 for (i
= 0; Names
[i
].s
; i
++)
1237 if (strcmp(s
, Names
[i
].s
) == 0)
1238 { yylval
->val
= Names
[i
].val
;
1240 yylval
->sym
= lookup(Names
[i
].sym
);
1241 return Names
[i
].tok
;
1244 if ((yylval
->val
= ismtype(s
)) != 0)
1245 { yylval
->ismtyp
= 1;
1249 if (strcmp(s
, "_last") == 0)
1252 if (Inlining
>= 0 && !ReDiRect
)
1253 { Lextok
*tt
, *t
= Inline_stub
[Inlining
]->params
;
1255 for (i
= 0; t
; t
= t
->rgt
, i
++) /* formal pars */
1256 if (!strcmp(s
, t
->lft
->sym
->name
) /* varname matches formal */
1257 && strcmp(s
, Inline_stub
[Inlining
]->anms
[i
]) != 0) /* actual pars */
1261 printf("\tline %d, replace %s in call of '%s' with %s\n",
1263 Inline_stub
[Inlining
]->nm
->name
,
1264 Inline_stub
[Inlining
]->anms
[i
]);
1266 for (tt
= Inline_stub
[Inlining
]->params
; tt
; tt
= tt
->rgt
)
1267 if (!strcmp(Inline_stub
[Inlining
]->anms
[i
],
1268 tt
->lft
->sym
->name
))
1269 { /* would be cyclic if not caught */
1270 printf("spin: line %d replacement value: %s\n",
1271 lineno
, tt
->lft
->sym
->name
);
1272 wrong
: fatal("formal par of %s contains replacement value",
1273 Inline_stub
[Inlining
]->nm
->name
);
1274 yylval
->ntyp
= tt
->lft
->ntyp
;
1275 yylval
->sym
= lookup(tt
->lft
->sym
->name
);
1279 /* check for occurrence of param as field of struct */
1280 { char *ptr
= Inline_stub
[Inlining
]->anms
[i
];
1281 while ((ptr
= strstr(ptr
, s
)) != NULL
)
1282 { if (*(ptr
-1) == '.'
1283 || *(ptr
+strlen(s
)) == '.')
1288 ReDiRect
= Inline_stub
[Inlining
]->anms
[i
];
1292 yylval
->sym
= lookup(s
); /* symbol table */
1305 { static int last
= 0;
1306 static int hold
= 0;
1309 * repair two common syntax mistakes with
1310 * semi-colons before or after a '}'
1337 return SEMI
; /* insert ';' */
1340 { /* if context, we're not in a typedef
1341 * because they're global.
1342 * if owner, we're at the end of a ref
1343 * to a struct field -- prevent that the
1344 * lookahead is interpreted as a field of
1345 * the same struct...
1347 if (context
) owner
= ZS
;
1348 hold
= lex(); /* look ahead */
1351 { c
= hold
; /* omit ';' */
1359 { static int IArg_nst
= 0;
1361 if (strcmp(yytext
, ",") == 0)
1362 { IArg_cont
[++IArgno
][0] = '\0';
1363 } else if (strcmp(yytext
, "(") == 0)
1364 { if (IArg_nst
++ == 0)
1366 IArg_cont
[0][0] = '\0';
1368 strcat(IArg_cont
[IArgno
], yytext
);
1369 } else if (strcmp(yytext
, ")") == 0)
1370 { if (--IArg_nst
> 0)
1371 strcat(IArg_cont
[IArgno
], yytext
);
1372 } else if (c
== CONST
&& yytext
[0] == '\'')
1373 { sprintf(yytext
, "'%c'", yylval
->val
);
1374 strcat(IArg_cont
[IArgno
], yytext
);
1375 } else if (c
== CONST
)
1376 { sprintf(yytext
, "%d", yylval
->val
);
1377 strcat(IArg_cont
[IArgno
], yytext
);
1381 case SEP
: strcpy(yytext
, "::"); break;
1382 case SEMI
: strcpy(yytext
, ";"); break;
1383 case DECR
: strcpy(yytext
, "--"); break;
1384 case INCR
: strcpy(yytext
, "++"); break;
1385 case LSHIFT
: strcpy(yytext
, "<<"); break;
1386 case RSHIFT
: strcpy(yytext
, ">>"); break;
1387 case LE
: strcpy(yytext
, "<="); break;
1388 case LT
: strcpy(yytext
, "<"); break;
1389 case GE
: strcpy(yytext
, ">="); break;
1390 case GT
: strcpy(yytext
, ">"); break;
1391 case EQ
: strcpy(yytext
, "=="); break;
1392 case ASGN
: strcpy(yytext
, "="); break;
1393 case NE
: strcpy(yytext
, "!="); break;
1394 case R_RCV
: strcpy(yytext
, "??"); break;
1395 case RCV
: strcpy(yytext
, "?"); break;
1396 case O_SND
: strcpy(yytext
, "!!"); break;
1397 case SND
: strcpy(yytext
, "!"); break;
1398 case AND
: strcpy(yytext
, "&&"); break;
1399 case OR
: strcpy(yytext
, "||"); break;
1401 strcat(IArg_cont
[IArgno
], yytext
);
This page took 0.073172 seconds and 4 git commands to generate.