sys/src/cmd/spin/tl_lex.c

   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
  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
  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
  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
  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
 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
 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 *
 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 *
 261 getsym(Symbol *s)
 262 {       Symbol *n = (Symbol *) tl_emalloc(sizeof(Symbol));
 263
 264         n->name = s->name;
 265         return n;
 266 }