]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /*;-*-C-*-; |
11db3170 | 2 | ** Splint - annotation-assisted static program checker |
c59f5181 | 3 | ** Copyright (C) 1994-2003 University of Virginia, |
11db3170 | 4 | ** Massachusetts Institute of Technology |
885824d3 | 5 | ** |
11db3170 | 6 | ** This program is free software; you can redistribute it and/or modify it |
7 | ** under the terms of the GNU General Public License as published by the | |
8 | ** Free Software Foundation; either version 2 of the License, or (at your | |
9 | ** option) any later version. | |
10 | ** | |
11 | ** This program is distributed in the hope that it will be useful, but | |
12 | ** WITHOUT ANY WARRANTY; without even the implied warranty of | |
13 | ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU | |
14 | ** General Public License for more details. | |
15 | ** | |
16 | ** The GNU General Public License is available from http://www.gnu.org/ or | |
17 | ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, | |
18 | ** MA 02111-1307, USA. | |
885824d3 | 19 | ** |
1b8ae690 | 20 | ** For information on splint: splint@cs.virginia.edu |
21 | ** To report a bug: splint-bug@cs.virginia.edu | |
11db3170 | 22 | ** For more information: http://www.splint.org |
885824d3 | 23 | */ |
24 | /* | |
11db3170 | 25 | ** signature.y |
885824d3 | 26 | ** |
11db3170 | 27 | ** Grammar for parsing LSL signatures. |
885824d3 | 28 | ** |
11db3170 | 29 | ** Original author: Yang Meng Tan, Massachusetts Institute of Technology |
885824d3 | 30 | */ |
31 | ||
32 | %{ | |
33 | ||
885824d3 | 34 | # include <stdio.h> |
1b8ae690 | 35 | # include "splintMacros.nf" |
b73d1009 | 36 | # include "basic.h" |
885824d3 | 37 | # include "lslparse.h" |
38 | # include "signature.h" | |
39 | ||
4dd72714 | 40 | static void lslerror (char *); |
41 | extern int lsllex (); | |
42 | ||
885824d3 | 43 | /*@dependent@*/ /*@null@*/ lslOp importedlslOp; |
44 | ||
45 | /*@-noparams@*/ /* Can't list params since YYSTYPE isn't defined yet. */ | |
46 | static void yyprint (/*FILE *p_file, int p_type, YYSTYPE p_value */); | |
47 | /*@=noparams@*/ | |
48 | ||
49 | # define YYPRINT(file, type, value) yyprint (file, type, value) | |
50 | ||
51 | # define YYDEBUG 1 | |
52 | ||
60eced23 | 53 | /*@-redef@*/ |
54 | /*@-readonlytrans@*/ | |
55 | /*@-nullassign@*/ | |
885824d3 | 56 | |
57 | %} | |
58 | ||
59 | %pure_parser | |
60 | ||
61 | /* CONVENTIONS: Reserved words are in ALL CAPS (plus markerSym) | |
62 | Characters appearing in the grammar are reserved: | |
63 | % ( ) , : \ */ | |
64 | ||
65 | /* Changes made | |
66 | - added LBRACKET stuff in OpForm (missing in LSL) | |
67 | - dif from LCL: open vs openSym, close vs closeSym | |
68 | - yylval vs yylval.tok | |
69 | */ | |
70 | ||
71 | %union { | |
72 | ltoken ltok; /* a leaf is also an ltoken */ | |
73 | unsigned int count; | |
74 | /*@only@*/ ltokenList ltokenList; | |
75 | /*@only@*/ opFormNode opform; | |
76 | /*@owned@*/ sigNode signature; | |
77 | /*@only@*/ nameNode name; | |
78 | /*@owned@*/ lslOp operator; | |
79 | /*@only@*/ lslOpList operators; | |
60eced23 | 80 | /*@-redef@*/ /*@-matchfields@*/ |
81 | } | |
82 | /*@=redef@*/ /*@=matchfields@*/ | |
885824d3 | 83 | |
84 | %token <ltok> LST_SIMPLEID | |
85 | %token <ltok> LST_LOGICALOP /* \implies, \and, \not, \or */ | |
86 | %token <ltok> LST_EQOP /* \eq, \neq, ==, != */ | |
87 | %token <ltok> LST_SIMPLEOP /* opSym - reserved */ | |
88 | %token <ltok> LST_MAPSYM /* LSL's -> */ | |
89 | /* FIELDMAPSYM = "\\field_arrow", only for LCL symtable import */ | |
90 | %token <ltok> LST_FIELDMAPSYM /* LCL's struct field operator -> */ | |
91 | %token <ltok> LST_MARKERSYM /* \marker, __ */ | |
92 | %token <ltok> LST_ifTOKEN LST_thenTOKEN LST_elseTOKEN | |
93 | /* different from LSL: separate LBRACKET from openSym and | |
94 | RBRACKET from closeSym */ | |
95 | %token <ltok> LST_LBRACKET LST_RBRACKET | |
96 | %token <ltok> LST_SELECTSYM /* \select or . */ | |
97 | %token <ltok> LST_SEPSYM LST_OPENSYM LST_CLOSESYM | |
98 | %token <ltok> LST_COLON /* : */ | |
99 | %token <ltok> LST_COMMA /* , */ | |
100 | %token <ltok> LST_EOL LST_COMMENTSYM LST_WHITESPACE | |
101 | ||
102 | %token LST_WHITESPACE | |
103 | %token LST_QUANTIFIERSYM | |
104 | %token LST_EQUATIONSYM | |
105 | %token LST_EQSEPSYM | |
106 | %token LST_COMPOSESYM | |
107 | %token LST_LPAR | |
108 | %token LST_RPAR | |
109 | %token LST_assertsTOKEN | |
110 | %token LST_assumesTOKEN | |
111 | %token LST_byTOKEN | |
112 | %token LST_convertsTOKEN | |
113 | %token LST_enumerationTOKEN | |
114 | %token LST_equationsTOKEN | |
115 | %token LST_exemptingTOKEN | |
116 | %token LST_forTOKEN | |
117 | %token LST_generatedTOKEN | |
118 | %token LST_impliesTOKEN | |
119 | %token LST_includesTOKEN | |
120 | %token LST_introducesTOKEN | |
121 | %token LST_ofTOKEN | |
122 | %token LST_partitionedTOKEN | |
123 | %token LST_traitTOKEN | |
124 | %token LST_tupleTOKEN | |
125 | %token LST_unionTOKEN | |
126 | %token LST_BADTOKEN | |
127 | ||
128 | %type <ltok> anyOp separator sortId opId | |
129 | %type <count> middle placeList | |
130 | %type <ltokenList> domain sortList | |
131 | %type <opform> opForm | |
132 | %type <signature> signature | |
133 | %type <name> name | |
134 | %type <operator> operator | |
135 | %type <operators> operatorList top | |
136 | ||
137 | %% | |
138 | ||
139 | top: operatorList { lslOpList_free ($1); } | |
2f2892c2 | 140 | ; |
885824d3 | 141 | |
142 | operatorList: operator | |
143 | { lslOpList x = lslOpList_new (); | |
144 | g_importedlslOp = $1; | |
145 | lslOpList_add (x, $1); | |
146 | $$ = x; } | |
147 | | operatorList operator | |
148 | { lslOpList_add ($1, $2); | |
149 | $$ = $1; } | |
2f2892c2 | 150 | ; |
885824d3 | 151 | |
152 | operator: name LST_COLON signature | |
153 | { $$ = makelslOpNode ($1, $3); } | |
154 | /* The next production is never used in the output of lsl -syms | |
155 | | name | |
156 | { $$ = makelslOpNode ($1, (sigNode)0); } */ | |
2f2892c2 | 157 | ; |
885824d3 | 158 | |
159 | name: opId /* check for the case of if_then_else */ | |
160 | { $$ = makeNameNodeId ($1); } | |
161 | | opForm | |
162 | { $$ = makeNameNodeForm ($1); } | |
2f2892c2 | 163 | ; |
885824d3 | 164 | |
165 | opForm | |
166 | : LST_ifTOKEN LST_MARKERSYM LST_thenTOKEN LST_MARKERSYM LST_elseTOKEN LST_MARKERSYM | |
167 | { $$ = makeOpFormNode ($1, OPF_IF, opFormUnion_createMiddle (0), ltoken_undefined); } | |
168 | | anyOp | |
169 | { $$ = makeOpFormNode ($1, OPF_ANYOP, opFormUnion_createAnyOp ($1), ltoken_undefined); } | |
170 | | LST_MARKERSYM anyOp | |
171 | { $$ = makeOpFormNode ($1, OPF_MANYOP, opFormUnion_createAnyOp ($2), ltoken_undefined); } | |
172 | | anyOp LST_MARKERSYM | |
173 | { $$ = makeOpFormNode ($1, OPF_ANYOPM, opFormUnion_createAnyOp ($1), ltoken_undefined); } | |
174 | | LST_MARKERSYM anyOp LST_MARKERSYM | |
175 | { $$ = makeOpFormNode ($1, OPF_MANYOPM, opFormUnion_createAnyOp ($2), ltoken_undefined); } | |
176 | | LST_OPENSYM middle LST_CLOSESYM | |
177 | { $$ = makeOpFormNode ($1, OPF_MIDDLE, opFormUnion_createMiddle ($2), $3); } | |
178 | | LST_MARKERSYM LST_OPENSYM middle LST_CLOSESYM | |
179 | { $$ = makeOpFormNode ($2, OPF_MMIDDLE, opFormUnion_createMiddle ($3), $4); } | |
180 | | LST_OPENSYM middle LST_CLOSESYM LST_MARKERSYM | |
181 | { $$ = makeOpFormNode ($1, OPF_MIDDLEM, opFormUnion_createMiddle ($2), $3); } | |
182 | | LST_MARKERSYM LST_OPENSYM middle LST_CLOSESYM LST_MARKERSYM | |
183 | { $$ = makeOpFormNode ($2, OPF_MMIDDLEM, | |
184 | opFormUnion_createMiddle ($3), $4); } | |
185 | | LST_LBRACKET middle LST_RBRACKET | |
186 | { $$ = makeOpFormNode ($1, OPF_BMIDDLE, | |
187 | opFormUnion_createMiddle ($2), $3); } | |
188 | | LST_MARKERSYM LST_LBRACKET middle LST_RBRACKET | |
189 | { $$ = makeOpFormNode ($2, OPF_BMMIDDLE, | |
190 | opFormUnion_createMiddle ($3), $4); } | |
191 | | LST_LBRACKET middle LST_RBRACKET LST_MARKERSYM | |
192 | { $$ = makeOpFormNode ($1, OPF_BMIDDLEM, | |
193 | opFormUnion_createMiddle ($2), $3); } | |
194 | | LST_MARKERSYM LST_LBRACKET middle LST_RBRACKET LST_MARKERSYM | |
195 | { $$ = makeOpFormNode ($2, OPF_BMMIDDLEM, | |
196 | opFormUnion_createMiddle ($3), $4); } | |
197 | | LST_SELECTSYM LST_SIMPLEID | |
198 | { $$ = makeOpFormNode ($1, OPF_SELECT, | |
199 | opFormUnion_createAnyOp ($2), ltoken_undefined); } | |
200 | | LST_MARKERSYM LST_SELECTSYM LST_SIMPLEID | |
201 | { $$ = makeOpFormNode ($1, OPF_MSELECT, | |
202 | opFormUnion_createAnyOp ($3), ltoken_undefined); } | |
203 | /* not in LSL, need FILEDMAPSYM to distinguish it from MAPSYM */ | |
204 | /* LST_FIELDMAPSYM = "\\field_arrow", only for LCL symtable import */ | |
205 | | LST_MARKERSYM LST_FIELDMAPSYM LST_SIMPLEID | |
206 | { $$ = makeOpFormNode ($1, OPF_MMAP, | |
207 | opFormUnion_createAnyOp ($3), ltoken_undefined); } | |
2f2892c2 | 208 | ; |
885824d3 | 209 | |
210 | anyOp: LST_SIMPLEOP | |
211 | { $$ = $1; } | |
212 | | LST_LOGICALOP | |
213 | { $$ = $1; } | |
214 | | LST_EQOP | |
215 | { $$ = $1; } | |
2f2892c2 | 216 | ; |
885824d3 | 217 | |
218 | middle: /* empty */ | |
219 | { $$ = 0; } | |
220 | | placeList | |
221 | { $$ = $1; } | |
2f2892c2 | 222 | ; |
885824d3 | 223 | |
224 | placeList: LST_MARKERSYM | |
225 | { $$ = 1; } | |
226 | | placeList separator LST_MARKERSYM | |
227 | { $$ = $1 + 1; } | |
2f2892c2 | 228 | ; |
885824d3 | 229 | |
230 | separator: LST_COMMA | |
231 | { $$ = $1; } | |
232 | | LST_SEPSYM | |
233 | { $$ = $1; } | |
2f2892c2 | 234 | ; |
885824d3 | 235 | |
236 | signature: domain LST_MAPSYM sortId | |
237 | { $$ = makesigNode ($2, $1, $3); } | |
2f2892c2 | 238 | ; |
885824d3 | 239 | |
240 | domain: /* empty */ | |
241 | { $$ = ltokenList_new (); } | |
242 | | sortList | |
243 | { $$ = $1; } | |
2f2892c2 | 244 | ; |
885824d3 | 245 | |
246 | sortList: sortId | |
247 | { $$ = ltokenList_singleton ($1); } | |
248 | | sortList LST_COMMA sortId | |
249 | { $$ = ltokenList_push ($1, $3); } | |
2f2892c2 | 250 | ; |
885824d3 | 251 | |
252 | sortId: LST_SIMPLEID | |
253 | { | |
254 | $$ = $1; | |
255 | ltoken_setText ($$, processTraitSortId (ltoken_getText ($1))); | |
256 | } | |
2f2892c2 | 257 | ; |
885824d3 | 258 | |
259 | opId: LST_SIMPLEID | |
260 | { $$ = $1; } | |
2f2892c2 | 261 | ; |
262 | ||
885824d3 | 263 | %% |
264 | ||
265 | # include "bison.reset" | |
266 | ||
267 | extern char *yytext; | |
268 | ||
269 | void lslerror (char *s) | |
270 | { | |
a0a162cd | 271 | llfatalbug |
272 | (cstring_makeLiteral | |
28bf4b0b | 273 | ("There has been a problem in the parser with LSL signatures. This is believed to result " |
1b8ae690 | 274 | "from a problem with bison v. 1.25. Please try rebuidling Splint " |
28bf4b0b | 275 | "using the pre-compiled grammar files by commenting out the " |
276 | "BISON= line in the top-level Makefile.")); | |
885824d3 | 277 | } |
278 | ||
279 | static void yyprint (FILE *file, int type, YYSTYPE value) | |
280 | { | |
281 | fprintf (file, " (%u:%u type: %d; text: %s) ", | |
282 | ltoken_getLine (value.ltok), | |
283 | ltoken_getCol (value.ltok), | |
284 | type, | |
285 | ltoken_getRawTextChars (value.ltok)); | |
286 | } | |
287 | ||
288 | extern void PrintToken (ltoken tok) { | |
289 | char *codStr; | |
290 | ||
291 | switch (ltoken_getCode (tok)) | |
292 | { | |
293 | case NOTTOKEN: codStr = "*** NOTTOKEN ***"; break; | |
294 | case LST_QUANTIFIERSYM: codStr = "QUANTIFIERSYM"; break; | |
295 | case LST_LOGICALOP: codStr = "LOGICALOP: "; break; | |
296 | case LST_SELECTSYM: codStr = "LST_SELECTSYM"; break; | |
297 | case LST_OPENSYM: codStr = "LST_OPENSYM"; break; | |
298 | case LST_SEPSYM: codStr = "SEPSYM"; break; | |
299 | case LST_CLOSESYM: codStr = "LST_CLOSESYM"; break; | |
300 | case LST_SIMPLEID: codStr = "LST_SIMPLEID"; break; | |
301 | case LST_MAPSYM: codStr = "MAPSYM"; break; | |
302 | case LST_MARKERSYM: codStr = "LST_MARKERSYM"; break; | |
303 | case LST_COMMENTSYM: codStr = "COMMENTSYM"; break; | |
304 | case LST_SIMPLEOP: codStr = "SIMPLEOP"; break; | |
305 | case LST_COLON: codStr = "LST_COLON"; break; | |
306 | case LST_COMMA: codStr = "COMMA"; break; | |
307 | case LST_LBRACKET: codStr = "LST_LBRACKET"; break; | |
308 | case LST_LPAR: codStr = "LST_LPAR"; break; | |
309 | case LST_RBRACKET: codStr = "LST_RBRACKET"; break; | |
310 | case LST_RPAR: codStr = "LST_RPAR"; break; | |
311 | case LST_EQOP: codStr = "LST_EQOP"; break; | |
312 | case LST_WHITESPACE: codStr = "WHITESPACE,"; break; | |
313 | case LST_EOL: codStr = "LST_EOL"; break; | |
314 | case LST_elseTOKEN: codStr = "elseTOKEN"; break; | |
315 | case LST_ifTOKEN: codStr = "ifTOKEN"; break; | |
316 | case LST_thenTOKEN: codStr = "thenTOKEN"; break; | |
317 | case LST_BADTOKEN: codStr = "*** BADTOKEN ***"; break; | |
318 | case LEOFTOKEN: /* can't reach LEOFTOKEN easily */ | |
319 | codStr = "LEOFTOKEN"; break; | |
320 | default: | |
321 | codStr = "*** invalid token code ***"; | |
322 | break; | |
323 | } /* end switch */ | |
324 | ||
325 | /* only used for debugging */ | |
326 | printf ("%u:%u: Token Code (%u): %s", | |
327 | ltoken_getLine (tok), ltoken_getCol (tok), | |
328 | ltoken_getCode (tok), codStr); | |
329 | if (ltoken_getRawText (tok) != 0) | |
330 | { | |
331 | printf (", Token String (%lu): %s\n", | |
332 | ltoken_getRawText (tok), ltoken_getRawTextChars (tok)); | |
333 | } | |
334 | else printf ("\n"); | |
335 | } | |
336 | ||
337 | ||
338 | ||
339 |