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