1 /***** spin: spinlex.c *****/ 2 3 /* Copyright (c) 1991,1995 by AT&T Corporation. All Rights Reserved. */ 4 /* This software is for educational purposes only. */ 5 /* Permission is given to distribute this code provided that this intro- */ 6 /* ductory message is not removed and no monies are exchanged. */ 7 /* No guarantee is expressed or implied by the distribution of this code. */ 8 /* Software written by Gerard J. Holzmann as part of the book: */ 9 /* `Design and Validation of Computer Protocols,' ISBN 0-13-539925-4, */ 10 /* Prentice Hall, Englewood Cliffs, NJ, 07632. */ 11 /* Send bug-reports and/or questions to: gerard@research.att.com */ 12 13 #include "spin.h" 14 #include "y.tab.h" 15 16 int lineno=1; 17 unsigned char in_comment=0; 18 char yytext[512]; 19 FILE *yyin = {stdin}; 20 FILE *yyout = {stdout}; 21 22 extern Symbol *Fname; 23 extern YYSTYPE yylval; 24 extern int has_last; 25 26 extern int isdigit(int); 27 extern int isalpha(int); 28 extern int isalnum(int); 29 30 #define Token(y) { yylval = nn(ZN,0,ZN,ZN); \ 31 if (!in_comment) return y; else goto again; } 32 33 #define ValToken(x, y) { yylval = nn(ZN,0,ZN,ZN); yylval->val = x; \ 34 if (!in_comment) return y; else goto again; } 35 36 #define SymToken(x, y) { yylval = nn(ZN,0,ZN,ZN); yylval->sym = x; \ 37 if (!in_comment) return y; else goto again; } 38 39 #define Getchar() getc(yyin) 40 #define Ungetch(c) ungetc(c, yyin) 41 42 int 43 notquote(int c) 44 { return (c != '\"' && c != '\n'); 45 } 46 47 int 48 isalnum_(int c) 49 { return (isalnum(c) || c == '_'); 50 } 51 52 void 53 getword(int first, int (*tst)(int)) 54 { int i=0; char c; 55 56 yytext[i++]= first; 57 while (tst(c = Getchar())) 58 yytext[i++] = c; 59 yytext[i] = '\0'; 60 Ungetch(c); 61 } 62 63 int 64 follow(int tok, int ifyes, int ifno) 65 { int c; 66 67 if ((c = Getchar()) == tok) 68 return ifyes; 69 Ungetch(c); 70 71 return ifno; 72 } 73 74 int 75 lex(void) 76 { int c; 77 78 again: 79 c = Getchar(); 80 yytext[0] = c; 81 yytext[1] = '\0'; 82 switch (c) { 83 case '\n': /* newline */ 84 lineno++; 85 goto again; 86 87 case ' ': case '\t': /* white space */ 88 goto again; 89 90 case '#': /* preprocessor directive */ 91 getword(c, isalpha); 92 if (Getchar() != ' ') 93 fatal("malformed preprocessor directive - # .", 0); 94 if (!isdigit(c = Getchar())) 95 fatal("malformed preprocessor directive - # .lineno", 0); 96 getword(c, isdigit); 97 lineno = atoi(yytext); /* removed -1 */ 98 c = Getchar(); 99 if (c == '\n') goto again; /* no filename */ 100 101 if (c != ' ') 102 fatal("malformed preprocessor directive - .fname", 0); 103 if ((c = Getchar()) != '\"') 104 fatal("malformed preprocessor directive - .fname", 0); 105 getword(c, notquote); 106 if (Getchar() != '\"') 107 fatal("malformed preprocessor directive - fname.", 0); 108 strcat(yytext, "\""); 109 Fname = lookup(yytext); 110 while (Getchar() != '\n') 111 ; 112 goto again; 113 114 case '\"': 115 getword(c, notquote); 116 if (Getchar() != '\"') 117 fatal("string not terminated", yytext); 118 strcat(yytext, "\""); 119 SymToken(lookup(yytext), STRING); 120 121 default: 122 break; 123 } 124 125 if (isdigit(c)) 126 { getword(c, isdigit); 127 ValToken(atoi(yytext), CONST); 128 } 129 130 if (isalpha(c) || c == '_') 131 { getword(c, isalnum_); 132 if (!in_comment) 133 return check_name(yytext); 134 else goto again; 135 } 136 137 switch (c) { 138 case '/': c = follow('*', 0, '/'); 139 if (!c) { in_comment = 1; goto again; } 140 break; 141 case '*': c = follow('/', 0, '*'); 142 if (!c) { in_comment = 0; goto again; } 143 break; 144 case ':': c = follow(':', SEP, ':'); break; 145 case '-': c = follow('>', SEMI, follow('-', DECR, '-')); break; 146 case '+': c = follow('+', INCR, '+'); break; 147 case '<': c = follow('<', LSHIFT, follow('=', LE, LT)); break; 148 case '>': c = follow('>', RSHIFT, follow('=', GE, GT)); break; 149 case '=': c = follow('=', EQ, ASGN); break; 150 case '!': c = follow('=', NE, follow('!', O_SND, SND)); break; 151 case '?': c = follow('?', R_RCV, RCV); break; 152 case '&': c = follow('&', AND, '&'); break; 153 case '|': c = follow('|', OR, '|'); break; 154 case ';': c = SEMI; break; 155 default : break; 156 } 157 Token(c); 158 } 159 160 static struct { 161 char *s; int tok; int val; char *sym; 162 } Names[] = { 163 "active", ACTIVE, 0, 0, 164 "assert", ASSERT, 0, 0, 165 "atomic", ATOMIC, 0, 0, 166 "bit", TYPE, BIT, 0, 167 "bool", TYPE, BIT, 0, 168 "break", BREAK, 0, 0, 169 "byte", TYPE, BYTE, 0, 170 "do", DO, 0, 0, 171 "chan", TYPE, CHAN, 0, 172 "else", ELSE, 0, 0, 173 "empty", EMPTY, 0, 0, 174 "enabled", ENABLED, 0, 0, 175 "fi", FI, 0, 0, 176 "full", FULL, 0, 0, 177 "goto", GOTO, 0, 0, 178 "hidden", HIDDEN, 0, 0, 179 "if", IF, 0, 0, 180 "init", INIT, 0, ":init:", 181 "int", TYPE, INT, 0, 182 "len", LEN, 0, 0, 183 "mtype", MTYPE, 0, 0, 184 "nempty", NEMPTY, 0, 0, 185 "never", CLAIM, 0, ":never:", 186 "nfull", NFULL, 0, 0, 187 "od", OD, 0, 0, 188 "of", OF, 0, 0, 189 "pc_value", PC_VAL, 0, 0, 190 "printf", PRINT, 0, 0, 191 "proctype", PROCTYPE, 0, 0, 192 "run", RUN, 0, 0, 193 "d_step", D_STEP, 0, 0, 194 "short", TYPE, SHORT, 0, 195 "skip", CONST, 1, 0, 196 "timeout", TIMEOUT, 0, 0, 197 "typedef", TYPEDEF, 0, 0, 198 "unless", UNLESS, 0, 0, 199 "xr", XU, XR, 0, 200 "xs", XU, XS, 0, 201 0, 0, 0, 0, 202 }; 203 204 int 205 check_name(char *s) 206 { register int i; 207 208 yylval = nn(ZN, 0, ZN, ZN); 209 for (i = 0; Names[i].s; i++) 210 if (strcmp(s, Names[i].s) == 0) 211 { yylval->val = Names[i].val; 212 if (Names[i].sym) 213 yylval->sym = lookup(Names[i].sym); 214 return Names[i].tok; 215 } 216 217 if (yylval->val = ismtype(s)) 218 { yylval->ismtyp = 1; 219 return CONST; 220 } 221 222 if (strcmp(s, "_last") == 0) 223 has_last++; 224 225 yylval->sym = lookup(s); /* symbol table */ 226 227 if (isutype(s)) 228 return UNAME; 229 if (isproctype(s)) 230 return PNAME; 231 232 return NAME; 233 } 234 235 int 236 yylex(void) 237 { static int last = 0; 238 static int hold = 0; 239 int c; 240 241 /* 242 * repair two common syntax mistakes with 243 * semi-colons before or after a '}' 244 */ 245 246 if (hold) 247 { c = hold; 248 hold = 0; 249 } else 250 { c = lex(); 251 if (last == ELSE 252 && c != SEMI 253 && c != FI) 254 { hold = c; 255 last = 0; 256 return SEMI; 257 } 258 if (last == '}' 259 && c != PROCTYPE 260 && c != INIT 261 && c != CLAIM 262 && c != SEP 263 && c != FI 264 && c != OD 265 && c != '}' 266 && c != UNLESS 267 && c != SEMI 268 && c != EOF) 269 { hold = c; 270 last = 0; 271 return SEMI; /* insert ';' */ 272 } 273 if (c == SEMI) 274 { extern Symbol *context, *owner; 275 /* if context, we're not in a typedef 276 * because they're global. 277 * if owner, we're at the end of a ref 278 * to a struct field -- prevent that the 279 * lookahead is interpreted as a field of 280 * the same struct... 281 */ 282 if (context) owner = ZS; 283 hold = lex(); /* look ahead */ 284 if (hold == '}' 285 || hold == SEMI) 286 { c = hold; /* omit ';' */ 287 hold = 0; 288 } 289 } 290 } 291 last = c; 292 return c; 293 } 294