]>
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 | ||
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); } | |
140 | ||
141 | operatorList: operator | |
142 | { lslOpList x = lslOpList_new (); | |
143 | g_importedlslOp = $1; | |
144 | lslOpList_add (x, $1); | |
145 | $$ = x; } | |
146 | | operatorList operator | |
147 | { lslOpList_add ($1, $2); | |
148 | $$ = $1; } | |
149 | ||
150 | operator: name LST_COLON signature | |
151 | { $$ = makelslOpNode ($1, $3); } | |
152 | /* The next production is never used in the output of lsl -syms | |
153 | | name | |
154 | { $$ = makelslOpNode ($1, (sigNode)0); } */ | |
155 | ||
156 | name: opId /* check for the case of if_then_else */ | |
157 | { $$ = makeNameNodeId ($1); } | |
158 | | opForm | |
159 | { $$ = makeNameNodeForm ($1); } | |
160 | ||
161 | opForm | |
162 | : LST_ifTOKEN LST_MARKERSYM LST_thenTOKEN LST_MARKERSYM LST_elseTOKEN LST_MARKERSYM | |
163 | { $$ = makeOpFormNode ($1, OPF_IF, opFormUnion_createMiddle (0), ltoken_undefined); } | |
164 | | anyOp | |
165 | { $$ = makeOpFormNode ($1, OPF_ANYOP, opFormUnion_createAnyOp ($1), ltoken_undefined); } | |
166 | | LST_MARKERSYM anyOp | |
167 | { $$ = makeOpFormNode ($1, OPF_MANYOP, opFormUnion_createAnyOp ($2), ltoken_undefined); } | |
168 | | anyOp LST_MARKERSYM | |
169 | { $$ = makeOpFormNode ($1, OPF_ANYOPM, opFormUnion_createAnyOp ($1), ltoken_undefined); } | |
170 | | LST_MARKERSYM anyOp LST_MARKERSYM | |
171 | { $$ = makeOpFormNode ($1, OPF_MANYOPM, opFormUnion_createAnyOp ($2), ltoken_undefined); } | |
172 | | LST_OPENSYM middle LST_CLOSESYM | |
173 | { $$ = makeOpFormNode ($1, OPF_MIDDLE, opFormUnion_createMiddle ($2), $3); } | |
174 | | LST_MARKERSYM LST_OPENSYM middle LST_CLOSESYM | |
175 | { $$ = makeOpFormNode ($2, OPF_MMIDDLE, opFormUnion_createMiddle ($3), $4); } | |
176 | | LST_OPENSYM middle LST_CLOSESYM LST_MARKERSYM | |
177 | { $$ = makeOpFormNode ($1, OPF_MIDDLEM, opFormUnion_createMiddle ($2), $3); } | |
178 | | LST_MARKERSYM LST_OPENSYM middle LST_CLOSESYM LST_MARKERSYM | |
179 | { $$ = makeOpFormNode ($2, OPF_MMIDDLEM, | |
180 | opFormUnion_createMiddle ($3), $4); } | |
181 | | LST_LBRACKET middle LST_RBRACKET | |
182 | { $$ = makeOpFormNode ($1, OPF_BMIDDLE, | |
183 | opFormUnion_createMiddle ($2), $3); } | |
184 | | LST_MARKERSYM LST_LBRACKET middle LST_RBRACKET | |
185 | { $$ = makeOpFormNode ($2, OPF_BMMIDDLE, | |
186 | opFormUnion_createMiddle ($3), $4); } | |
187 | | LST_LBRACKET middle LST_RBRACKET LST_MARKERSYM | |
188 | { $$ = makeOpFormNode ($1, OPF_BMIDDLEM, | |
189 | opFormUnion_createMiddle ($2), $3); } | |
190 | | LST_MARKERSYM LST_LBRACKET middle LST_RBRACKET LST_MARKERSYM | |
191 | { $$ = makeOpFormNode ($2, OPF_BMMIDDLEM, | |
192 | opFormUnion_createMiddle ($3), $4); } | |
193 | | LST_SELECTSYM LST_SIMPLEID | |
194 | { $$ = makeOpFormNode ($1, OPF_SELECT, | |
195 | opFormUnion_createAnyOp ($2), ltoken_undefined); } | |
196 | | LST_MARKERSYM LST_SELECTSYM LST_SIMPLEID | |
197 | { $$ = makeOpFormNode ($1, OPF_MSELECT, | |
198 | opFormUnion_createAnyOp ($3), ltoken_undefined); } | |
199 | /* not in LSL, need FILEDMAPSYM to distinguish it from MAPSYM */ | |
200 | /* LST_FIELDMAPSYM = "\\field_arrow", only for LCL symtable import */ | |
201 | | LST_MARKERSYM LST_FIELDMAPSYM LST_SIMPLEID | |
202 | { $$ = makeOpFormNode ($1, OPF_MMAP, | |
203 | opFormUnion_createAnyOp ($3), ltoken_undefined); } | |
204 | ||
205 | ||
206 | anyOp: LST_SIMPLEOP | |
207 | { $$ = $1; } | |
208 | | LST_LOGICALOP | |
209 | { $$ = $1; } | |
210 | | LST_EQOP | |
211 | { $$ = $1; } | |
212 | ||
213 | middle: /* empty */ | |
214 | { $$ = 0; } | |
215 | | placeList | |
216 | { $$ = $1; } | |
217 | ||
218 | placeList: LST_MARKERSYM | |
219 | { $$ = 1; } | |
220 | | placeList separator LST_MARKERSYM | |
221 | { $$ = $1 + 1; } | |
222 | ||
223 | separator: LST_COMMA | |
224 | { $$ = $1; } | |
225 | | LST_SEPSYM | |
226 | { $$ = $1; } | |
227 | ||
228 | signature: domain LST_MAPSYM sortId | |
229 | { $$ = makesigNode ($2, $1, $3); } | |
230 | ||
231 | domain: /* empty */ | |
232 | { $$ = ltokenList_new (); } | |
233 | | sortList | |
234 | { $$ = $1; } | |
235 | ||
236 | sortList: sortId | |
237 | { $$ = ltokenList_singleton ($1); } | |
238 | | sortList LST_COMMA sortId | |
239 | { $$ = ltokenList_push ($1, $3); } | |
240 | ||
241 | sortId: LST_SIMPLEID | |
242 | { | |
243 | $$ = $1; | |
244 | ltoken_setText ($$, processTraitSortId (ltoken_getText ($1))); | |
245 | } | |
246 | ||
247 | opId: LST_SIMPLEID | |
248 | { $$ = $1; } | |
249 | %% | |
250 | ||
251 | # include "bison.reset" | |
252 | ||
253 | extern char *yytext; | |
254 | ||
255 | void lslerror (char *s) | |
256 | { | |
a0a162cd | 257 | llfatalbug |
258 | (cstring_makeLiteral | |
28bf4b0b | 259 | ("There has been a problem in the parser with LSL signatures. This is believed to result " |
1b8ae690 | 260 | "from a problem with bison v. 1.25. Please try rebuidling Splint " |
28bf4b0b | 261 | "using the pre-compiled grammar files by commenting out the " |
262 | "BISON= line in the top-level Makefile.")); | |
885824d3 | 263 | } |
264 | ||
265 | static void yyprint (FILE *file, int type, YYSTYPE value) | |
266 | { | |
267 | fprintf (file, " (%u:%u type: %d; text: %s) ", | |
268 | ltoken_getLine (value.ltok), | |
269 | ltoken_getCol (value.ltok), | |
270 | type, | |
271 | ltoken_getRawTextChars (value.ltok)); | |
272 | } | |
273 | ||
274 | extern void PrintToken (ltoken tok) { | |
275 | char *codStr; | |
276 | ||
277 | switch (ltoken_getCode (tok)) | |
278 | { | |
279 | case NOTTOKEN: codStr = "*** NOTTOKEN ***"; break; | |
280 | case LST_QUANTIFIERSYM: codStr = "QUANTIFIERSYM"; break; | |
281 | case LST_LOGICALOP: codStr = "LOGICALOP: "; break; | |
282 | case LST_SELECTSYM: codStr = "LST_SELECTSYM"; break; | |
283 | case LST_OPENSYM: codStr = "LST_OPENSYM"; break; | |
284 | case LST_SEPSYM: codStr = "SEPSYM"; break; | |
285 | case LST_CLOSESYM: codStr = "LST_CLOSESYM"; break; | |
286 | case LST_SIMPLEID: codStr = "LST_SIMPLEID"; break; | |
287 | case LST_MAPSYM: codStr = "MAPSYM"; break; | |
288 | case LST_MARKERSYM: codStr = "LST_MARKERSYM"; break; | |
289 | case LST_COMMENTSYM: codStr = "COMMENTSYM"; break; | |
290 | case LST_SIMPLEOP: codStr = "SIMPLEOP"; break; | |
291 | case LST_COLON: codStr = "LST_COLON"; break; | |
292 | case LST_COMMA: codStr = "COMMA"; break; | |
293 | case LST_LBRACKET: codStr = "LST_LBRACKET"; break; | |
294 | case LST_LPAR: codStr = "LST_LPAR"; break; | |
295 | case LST_RBRACKET: codStr = "LST_RBRACKET"; break; | |
296 | case LST_RPAR: codStr = "LST_RPAR"; break; | |
297 | case LST_EQOP: codStr = "LST_EQOP"; break; | |
298 | case LST_WHITESPACE: codStr = "WHITESPACE,"; break; | |
299 | case LST_EOL: codStr = "LST_EOL"; break; | |
300 | case LST_elseTOKEN: codStr = "elseTOKEN"; break; | |
301 | case LST_ifTOKEN: codStr = "ifTOKEN"; break; | |
302 | case LST_thenTOKEN: codStr = "thenTOKEN"; break; | |
303 | case LST_BADTOKEN: codStr = "*** BADTOKEN ***"; break; | |
304 | case LEOFTOKEN: /* can't reach LEOFTOKEN easily */ | |
305 | codStr = "LEOFTOKEN"; break; | |
306 | default: | |
307 | codStr = "*** invalid token code ***"; | |
308 | break; | |
309 | } /* end switch */ | |
310 | ||
311 | /* only used for debugging */ | |
312 | printf ("%u:%u: Token Code (%u): %s", | |
313 | ltoken_getLine (tok), ltoken_getCol (tok), | |
314 | ltoken_getCode (tok), codStr); | |
315 | if (ltoken_getRawText (tok) != 0) | |
316 | { | |
317 | printf (", Token String (%lu): %s\n", | |
318 | ltoken_getRawText (tok), ltoken_getRawTextChars (tok)); | |
319 | } | |
320 | else printf ("\n"); | |
321 | } | |
322 | ||
323 | ||
324 | ||
325 |