1 /***** tl_spin: tl_lex.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 * Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
9 * presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
10 */
11
12 #include <stdlib.h>
13 #include <ctype.h>
14 #include "tl.h"
15
16 static Symbol *symtab[Nhash+1];
17 static int tl_lex(void);
18 extern int tl_peek(int);
19
20 extern YYSTYPE tl_yylval;
21 extern char yytext[];
22
23 #define Token(y) tl_yylval = tl_nn(y,ZN,ZN); return y
24
25 static void
tl_getword(int first,int (* tst)(int))26 tl_getword(int first, int (*tst)(int))
27 { int i=0; int c;
28
29 yytext[i++] = (char ) first;
30
31 c = tl_Getchar();
32 while (c != -1 && tst(c))
33 { yytext[i++] = (char) c;
34 c = tl_Getchar();
35 }
36
37 /* while (tst(c = tl_Getchar()))
38 * yytext[i++] = c;
39 */
40 yytext[i] = '\0';
41 tl_UnGetchar();
42 }
43
44 static int
tl_follow(int tok,int ifyes,int ifno)45 tl_follow(int tok, int ifyes, int ifno)
46 { int c;
47 char buf[32];
48 extern int tl_yychar;
49
50 if ((c = tl_Getchar()) == tok)
51 return ifyes;
52 tl_UnGetchar();
53 tl_yychar = c;
54 sprintf(buf, "expected '%c'", tok);
55 tl_yyerror(buf); /* no return from here */
56 return ifno;
57 }
58
59 int
tl_yylex(void)60 tl_yylex(void)
61 { int c = tl_lex();
62 #if 0
63 printf("c = %c (%d)\n", c, c);
64 #endif
65 return c;
66 }
67
68 static int
is_predicate(int z)69 is_predicate(int z)
70 { char c, c_prev = z;
71 char want = (z == '{') ? '}' : ')';
72 int i = 0, j, nesting = 0;
73 char peek_buf[512];
74
75 c = tl_peek(i++); /* look ahead without changing position */
76 while ((c != want || nesting > 0) && c != -1 && i < 2047)
77 { if (islower((int) c) || c == '_')
78 { peek_buf[0] = c;
79 j = 1;
80 while (j < (int) sizeof(peek_buf)
81 && (isalnum((int)(c = tl_peek(i))) || c == '_'))
82 { peek_buf[j++] = c;
83 i++;
84 }
85 c = 0; /* make sure we don't match on z or want on the peekahead */
86 if (j >= (int) sizeof(peek_buf))
87 { peek_buf[j-1] = '\0';
88 fatal("name '%s' in ltl formula too long", peek_buf);
89 }
90 peek_buf[j] = '\0';
91 if (strcmp(peek_buf, "always") == 0
92 || strcmp(peek_buf, "equivalent") == 0
93 || strcmp(peek_buf, "eventually") == 0
94 || strcmp(peek_buf, "until") == 0
95 || strcmp(peek_buf, "next") == 0
96 || strcmp(peek_buf, "c_expr") == 0)
97 { return 0;
98 }
99 } else
100 { int c_nxt = tl_peek(i);
101 if (((c == 'U' || c == 'V' || c == 'X')
102 && !isalnum_(c_prev)
103 && (c_nxt == -1 || !isalnum_(c_nxt)))
104 || (c == '<' && c_nxt == '>')
105 || (c == '<' && c_nxt == '-')
106 || (c == '-' && c_nxt == '>')
107 || (c == '[' && c_nxt == ']'))
108 { return 0;
109 } }
110
111 if (c == z)
112 { nesting++;
113 }
114 if (c == want)
115 { nesting--;
116 }
117 c_prev = c;
118 c = tl_peek(i++);
119 }
120 return 1;
121 }
122
123 static void
read_upto_closing(int z)124 read_upto_closing(int z)
125 { char c, want = (z == '{') ? '}' : ')';
126 int i = 0, nesting = 0;
127
128 c = tl_Getchar();
129 while ((c != want || nesting > 0) && c != -1 && i < 2047) /* yytext is 2048 */
130 { yytext[i++] = c;
131 if (c == z)
132 { nesting++;
133 }
134 if (c == want)
135 { nesting--;
136 }
137 c = tl_Getchar();
138 }
139 yytext[i] = '\0';
140 }
141
142 static int
tl_lex(void)143 tl_lex(void)
144 { int c;
145
146 do {
147 c = tl_Getchar();
148 yytext[0] = (char ) c;
149 yytext[1] = '\0';
150
151 if (c <= 0)
152 { Token(';');
153 }
154
155 } while (c == ' '); /* '\t' is removed in tl_main.c */
156
157 if (c == '{' || c == '(') /* new 6.0.0 */
158 { if (is_predicate(c))
159 { read_upto_closing(c);
160 tl_yylval = tl_nn(PREDICATE,ZN,ZN);
161 if (!tl_yylval)
162 { fatal("unexpected error 4", (char *) 0);
163 }
164 tl_yylval->sym = tl_lookup(yytext);
165 return PREDICATE;
166 } }
167
168 if (c == '}')
169 { tl_yyerror("unexpected '}'");
170 }
171 if (islower(c))
172 { tl_getword(c, isalnum_);
173 if (strcmp("true", yytext) == 0)
174 { Token(TRUE);
175 }
176 if (strcmp("false", yytext) == 0)
177 { Token(FALSE);
178 }
179 if (strcmp("always", yytext) == 0)
180 { Token(ALWAYS);
181 }
182 if (strcmp("eventually", yytext) == 0)
183 { Token(EVENTUALLY);
184 }
185 if (strcmp("until", yytext) == 0)
186 { Token(U_OPER);
187 }
188 #ifdef NXT
189 if (strcmp("next", yytext) == 0)
190 { Token(NEXT);
191 }
192 #endif
193 if (strcmp("c_expr", yytext) == 0)
194 { Token(CEXPR);
195 }
196 if (strcmp("not", yytext) == 0)
197 { Token(NOT);
198 }
199 tl_yylval = tl_nn(PREDICATE,ZN,ZN);
200 if (!tl_yylval)
201 { fatal("unexpected error 5", (char *) 0);
202 }
203 tl_yylval->sym = tl_lookup(yytext);
204 return PREDICATE;
205 }
206
207 if (c == '<')
208 { c = tl_Getchar();
209 if (c == '>')
210 { Token(EVENTUALLY);
211 }
212 if (c != '-')
213 { tl_UnGetchar();
214 tl_yyerror("expected '<>' or '<->'");
215 }
216 c = tl_Getchar();
217 if (c == '>')
218 { Token(EQUIV);
219 }
220 tl_UnGetchar();
221 tl_yyerror("expected '<->'");
222 }
223
224 switch (c) {
225 case '/' : c = tl_follow('\\', AND, '/'); break;
226 case '\\': c = tl_follow('/', OR, '\\'); break;
227 case '&' : c = tl_follow('&', AND, '&'); break;
228 case '|' : c = tl_follow('|', OR, '|'); break;
229 case '[' : c = tl_follow(']', ALWAYS, '['); break;
230 case '-' : c = tl_follow('>', IMPLIES, '-'); break;
231 case '!' : c = NOT; break;
232 case 'U' : c = U_OPER; break;
233 case 'V' : c = V_OPER; break;
234 #ifdef NXT
235 case 'X' : c = NEXT; break;
236 #endif
237 default : break;
238 }
239 Token(c);
240 }
241
242 Symbol *
tl_lookup(char * s)243 tl_lookup(char *s)
244 { Symbol *sp;
245 unsigned int h = hash(s);
246
247 for (sp = symtab[h]; sp; sp = sp->next)
248 if (strcmp(sp->name, s) == 0)
249 return sp;
250
251 sp = (Symbol *) tl_emalloc(sizeof(Symbol));
252 sp->name = (char *) tl_emalloc((int) strlen(s) + 1);
253 strcpy(sp->name, s);
254 sp->next = symtab[h];
255 symtab[h] = sp;
256
257 return sp;
258 }
259
260 Symbol *
getsym(Symbol * s)261 getsym(Symbol *s)
262 { Symbol *n = (Symbol *) tl_emalloc(sizeof(Symbol));
263
264 n->name = s->name;
265 return n;
266 }
267