]>
Commit | Line | Data |
---|---|---|
616915dd | 1 | /* |
11db3170 | 2 | ** Splint - annotation-assisted static program checker |
c59f5181 | 3 | ** Copyright (C) 1994-2003 University of Virginia, |
616915dd | 4 | ** Massachusetts Institute of Technology |
5 | ** | |
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. | |
19 | ** | |
155af98d | 20 | ** For information on splint: info@splint.org |
21 | ** To report a bug: splint-bug@splint.org | |
11db3170 | 22 | ** For more information: http://www.splint.org |
616915dd | 23 | */ |
24 | /* | |
25 | ** lslparse.c | |
26 | ** | |
27 | ** Module for calling LSL checker. | |
28 | ** | |
29 | ** AUTHOR: | |
30 | ** Yang Meng Tan, | |
31 | ** Massachusetts Institute of Technology | |
32 | */ | |
33 | ||
1b8ae690 | 34 | # include "splintMacros.nf" |
616915dd | 35 | # include "llbasic.h" |
36 | # include "lclscan.h" | |
37 | # include "signature.h" | |
38 | # include "signature2.h" | |
39 | # include "scan.h" | |
40 | # include "scanline.h" | |
41 | # include "syntable.h" | |
42 | # include "tokentable.h" | |
43 | # include "lslinit.h" | |
44 | # include "lslparse.h" | |
45 | # include "llmain.h" | |
46 | ||
47 | /*@+ignorequals@*/ | |
48 | ||
49 | /*@dependent@*/ /*@null@*/ lslOp g_importedlslOp = NULL; | |
50 | bool g_lslParsingTraits = FALSE; | |
51 | ||
28bf4b0b | 52 | static void invokeLSL (cstring p_infile, cstring p_outfile, bool p_deletep); |
616915dd | 53 | |
54 | int | |
55 | parseSignatures (cstring infile) | |
56 | { | |
28bf4b0b | 57 | inputStream sourceFile; |
616915dd | 58 | ltoken *id = (ltoken *) dmalloc (sizeof (*id)); |
59 | int status = 0; | |
60 | ||
61 | /* parse traits */ | |
28bf4b0b | 62 | *id = LSLInsertToken (LST_SIMPLEID, lsymbol_fromString (infile), 0, FALSE); |
63 | ltoken_setFileName (*id, infile); | |
616915dd | 64 | ltoken_setLine (*id, 0); |
65 | ltoken_setCol (*id, 0); | |
66 | ||
28bf4b0b | 67 | sourceFile = inputStream_create (infile, cstring_undefined, FALSE); |
616915dd | 68 | |
28bf4b0b | 69 | if (!inputStream_getPath (context_getLarchPath (), sourceFile)) |
616915dd | 70 | { |
71 | lclplainerror | |
72 | (message ("LSL signature parsing: can't find file %s containing trait", | |
28bf4b0b | 73 | inputStream_fileName (sourceFile))); |
616915dd | 74 | status = 1; |
75 | ||
76 | sfree (id); | |
28bf4b0b | 77 | inputStream_free (sourceFile); |
616915dd | 78 | return status; |
79 | } | |
80 | ||
28bf4b0b | 81 | if (!inputStream_open (sourceFile)) |
616915dd | 82 | { |
83 | lclplainerror | |
84 | (cstring_makeLiteral ("LSL parsing: can't open file containing trait")); | |
85 | status = 2; | |
86 | sfree (id); | |
28bf4b0b | 87 | inputStream_free (sourceFile); |
616915dd | 88 | |
89 | return status; | |
90 | } | |
91 | ||
92 | lsldebug = 0; | |
93 | g_lslParsingTraits = TRUE; | |
94 | LSLScanReset (sourceFile); | |
95 | LSLReportEolTokens (FALSE); | |
96 | ||
97 | status = lslparse (); | |
98 | ||
99 | /* symtable_dump (symtab, stdout, TRUE); */ | |
100 | g_lslParsingTraits = FALSE; | |
101 | ||
28bf4b0b | 102 | (void) inputStream_close (sourceFile); |
103 | inputStream_free (sourceFile); | |
616915dd | 104 | |
105 | sfree (id); | |
106 | ||
107 | ||
108 | return status; | |
109 | } | |
110 | ||
111 | /*@only@*/ lslOp | |
28bf4b0b | 112 | parseOpLine (cstring fname, cstring line) |
616915dd | 113 | { |
28bf4b0b | 114 | inputStream sourceFile; |
616915dd | 115 | bool status; |
116 | ||
28bf4b0b | 117 | sourceFile = inputStream_fromString (fname, line); |
616915dd | 118 | |
28bf4b0b | 119 | if (check (inputStream_open (sourceFile))) |
616915dd | 120 | { |
121 | LSLScanReset (sourceFile); | |
122 | LSLReportEolTokens (FALSE); /* 0 by default, lslParsingTraits = 0; */ | |
123 | ||
124 | /* | |
125 | ** lsl parsing and importing .lcs files are expected to be mutually | |
126 | ** exclusive. | |
127 | ** | |
128 | ** lslparse sets importedlslOp | |
129 | */ | |
130 | ||
131 | status = (lslparse () != 0); | |
132 | ||
133 | if (status) | |
134 | { | |
28bf4b0b | 135 | lclplainfatalerror (message ("Error in parsing line: %s", line)); |
616915dd | 136 | } |
137 | ||
28bf4b0b | 138 | (void) inputStream_close (sourceFile); |
616915dd | 139 | } |
140 | ||
28bf4b0b | 141 | inputStream_free (sourceFile); |
616915dd | 142 | |
143 | llassert (g_importedlslOp != NULL); | |
144 | return (lslOp_copy (g_importedlslOp)); | |
145 | } | |
146 | ||
147 | lsymbol | |
148 | processTraitSortId (lsymbol sortid) | |
149 | { | |
150 | lsymbol out = lsymbol_sortFromType (g_symtab, sortid); | |
151 | if (out == sortid) | |
152 | { /* may be a new sort */ | |
153 | (void) sort_fromLsymbol (sortid); | |
154 | } | |
155 | return out; | |
156 | } | |
157 | ||
158 | /* formerly from check.c module */ | |
159 | ||
160 | static /*@only@*/ cstring | |
161 | printTypeName2 (typeNameNode n) | |
162 | { | |
163 | cstring s = cstring_undefined; | |
164 | sortNode sn; | |
165 | lsymbol lclSort; | |
166 | ltoken err; | |
167 | ||
168 | if (n != (typeNameNode) 0) | |
169 | { | |
170 | if (n->isTypeName) | |
171 | { | |
172 | /* does not process opForm renaming, pass on to LSL | |
173 | and hope that it works for now. */ | |
174 | typeNamePack p = n->typename; | |
175 | ||
176 | llassert (p != NULL); | |
177 | ||
178 | /* get the LCL type, assume LCL type has already been mentioned. */ | |
179 | lclSort = lclTypeSpecNode2sort (p->type); | |
180 | lclSort = sort_getUnderlying (lclSort); | |
181 | /* lclsource = LCLSLScanSource (); */ | |
182 | if (!sort_isValidSort (lclSort)) | |
183 | { | |
184 | err = lclTypeSpecNode_errorToken (p->type); | |
28bf4b0b | 185 | /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (err)); */ |
616915dd | 186 | lclerror (err, message ("Unrecognized type in uses: %q", |
187 | typeNameNode_unparse (n))); | |
188 | } | |
189 | else | |
190 | { | |
191 | /* | |
192 | ** Below is necessary because this is one place where an LCL mutable | |
193 | ** type name is mapped directly into its value sort, not obj sort. | |
194 | ** Allows us to support only one qualifying "obj", rather | |
195 | ** than "val" as well. | |
196 | */ | |
197 | ||
198 | lclSort = typeExpr2ptrSort (lclSort, p->abst); | |
199 | lclSort = sort_makeVal (lclSort); | |
200 | ||
201 | /* | |
202 | ** Check that lclSort is not a HOFSort ... | |
203 | ** Propagation of HOFSort should stop here. | |
204 | */ | |
205 | ||
206 | if (sort_isHOFSortKind (lclSort)) | |
207 | { | |
208 | err = lclTypeSpecNode_errorToken (p->type); | |
209 | ||
210 | lclfatalerror | |
211 | (err, | |
212 | cstring_makeLiteral | |
213 | ("LCL uses cannot handle higher-order types")); | |
214 | } | |
215 | if (p->isObj) | |
216 | lclSort = sort_makeObj (lclSort); | |
217 | ||
218 | /* if (!p->isObj) { | |
219 | lclSort = sort_makeVal (lclSort); | |
220 | } */ | |
221 | ||
222 | sn = sort_lookup (lclSort); | |
28bf4b0b | 223 | s = cstring_copy (cstring_fromChars (lsymbol_toChars (sn->name))); |
616915dd | 224 | /* s = string_paste (s, AbstDeclaratorNode_unparse (p->abst)); */ |
225 | } | |
226 | } | |
227 | else | |
228 | { | |
229 | /* s = OpFormNode_unparse (n->opform); */ | |
230 | if (n->opform != 0) | |
231 | { | |
232 | lclfatalerror | |
233 | (n->opform->tok, | |
234 | cstring_makeLiteral ("Attempt to rename operator with uses: " | |
235 | "use LSL includes renaming facility")); | |
236 | } | |
237 | else | |
238 | { | |
239 | BADEXIT; | |
240 | } | |
241 | } | |
242 | } | |
243 | return s; | |
244 | } | |
245 | ||
246 | static /*@only@*/ cstring | |
247 | replaceNode_unparseAlt (replaceNode x) | |
248 | { | |
249 | cstring s = cstring_undefined; | |
250 | ||
251 | if (x != (replaceNode) 0) | |
252 | { | |
253 | s = printTypeName2 (x->typename); | |
254 | s = cstring_concatChars (s, " for "); | |
255 | ||
256 | if (x->isCType) | |
257 | { | |
258 | s = cstring_concatFree1 (s, ltoken_unparse (x->content.ctype)); | |
259 | } | |
260 | else | |
261 | { | |
262 | s = cstring_concatFree (s, nameNode_unparse (x->content.renamesortname.name)); | |
263 | s = cstring_concatFree (s, | |
264 | sigNode_unparse (x->content.renamesortname.signature)); | |
265 | } | |
266 | } | |
267 | ||
268 | return s; | |
269 | } | |
270 | ||
271 | static /*@only@*/ cstring | |
272 | replaceNodeList_unparseAlt (replaceNodeList x) | |
273 | { | |
274 | cstring s = cstring_undefined; | |
275 | bool first = TRUE; | |
276 | ||
277 | replaceNodeList_elements (x, i) | |
278 | { | |
279 | if (first) | |
280 | { | |
281 | s = replaceNode_unparseAlt (i); | |
282 | first = FALSE; | |
283 | } | |
284 | else | |
285 | { | |
286 | s = message ("%q, %q", s, replaceNode_unparseAlt (i)); | |
287 | } | |
288 | } end_replaceNodeList_elements; | |
289 | ||
290 | return s; | |
291 | } | |
292 | ||
293 | static /*@only@*/ cstring | |
294 | printNameList2 (typeNameNodeList x) | |
295 | { | |
296 | /* printing a list of typeNameNode's, not nameNode's */ | |
297 | bool first = TRUE; | |
298 | cstring s = cstring_undefined; | |
299 | ||
300 | typeNameNodeList_elements (x, i) | |
301 | { | |
302 | if (first) | |
303 | { | |
304 | s = printTypeName2 (i); | |
305 | first = FALSE; | |
306 | } | |
307 | else | |
308 | { | |
309 | s = message ("%q, %q", s, printTypeName2 (i)); | |
310 | } | |
311 | } end_typeNameNodeList_elements; | |
312 | ||
313 | return s; | |
314 | } | |
315 | ||
316 | static /*@only@*/ cstring | |
317 | printRenamingNode2 (renamingNode x) | |
318 | { | |
319 | cstring s = cstring_undefined; | |
320 | ||
321 | if (x != (renamingNode) 0) | |
322 | { | |
323 | if (x->is_replace) | |
324 | { | |
325 | replaceNodeList r = x->content.replace; | |
326 | s = replaceNodeList_unparseAlt (r); | |
327 | } | |
328 | else | |
329 | { | |
330 | nameAndReplaceNode n = x->content.name; | |
331 | bool printComma = TRUE; | |
332 | if (typeNameNodeList_size (n->namelist) == 0) | |
333 | { | |
334 | printComma = FALSE; | |
335 | } | |
336 | s = printNameList2 (n->namelist); | |
337 | if (printComma) | |
338 | if (replaceNodeList_isDefined (n->replacelist) && | |
339 | replaceNodeList_size (n->replacelist) != 0) | |
340 | { | |
341 | s = cstring_appendChar (s, ','); | |
342 | s = cstring_appendChar (s, ' '); | |
343 | } | |
344 | s = cstring_concatFree (s, replaceNodeList_unparseAlt (n->replacelist)); | |
345 | } | |
346 | } | |
347 | return s; | |
348 | } | |
349 | ||
350 | static /*@only@*/ cstring | |
28bf4b0b | 351 | printTraitRefList2 (traitRefNodeList x) /*@*/ |
616915dd | 352 | { |
353 | cstring s = cstring_undefined; | |
354 | ||
355 | traitRefNodeList_elements (x, i) | |
356 | { | |
357 | s = message ("%qincludes (%q)", s, printRawLeaves2 (i->traitid)); | |
358 | ||
359 | if (i->rename != 0) | |
360 | { | |
361 | s = message ("%q(%q)", s, printRenamingNode2 (i->rename)); | |
362 | } | |
28bf4b0b | 363 | |
616915dd | 364 | s = message ("%q\n", s); |
365 | } end_traitRefNodeList_elements; | |
366 | ||
367 | return s; | |
368 | } | |
369 | ||
370 | void | |
28bf4b0b | 371 | callLSL (/*@unused@*/ cstring specfile, /*@only@*/ cstring text) |
616915dd | 372 | { |
373 | /* specfile is the name of the LCL file that contains "uses" | |
374 | Create an intermediate file named | |
375 | specfile_<TEMP_LSL_SUFFIX>.<TEMP_LSL_IN_SUFFIX>. | |
376 | put text in the file, run lsl on it and direct | |
377 | output to specfile_<TEMP_LSL_SUFFIX>.<TEMP_LSL_OUT_SUFFIX>. | |
378 | specfile can be a full pathname. | |
379 | Note: LSL does not support traitnames that are pathnames, only | |
380 | symbols. | |
381 | */ | |
382 | ||
28bf4b0b | 383 | cstring infile; |
384 | cstring outfile; | |
385 | cstring nopath; | |
386 | cstring noext; | |
616915dd | 387 | FILE *inptr; |
388 | ||
4dd72714 | 389 | infile = fileTable_fileName (fileTable_addltemp (context_fileTable ())); |
d5047b91 | 390 | inptr = fileTable_createFile (context_fileTable (), infile); |
616915dd | 391 | |
392 | if (inptr == NULL) | |
393 | { | |
394 | /* fopen fails */ | |
395 | llfatalerror (message ("Unable to write intermediate file: %s", | |
28bf4b0b | 396 | infile)); |
616915dd | 397 | } |
398 | ||
28bf4b0b | 399 | nopath = fileLib_removePath (infile); |
400 | noext = fileLib_removeAnyExtension (nopath); | |
401 | ||
402 | fprintf (inptr, "%s : trait\n", cstring_toCharsSafe (noext)); | |
616915dd | 403 | |
28bf4b0b | 404 | cstring_free (noext); |
405 | cstring_free (nopath); | |
616915dd | 406 | |
28bf4b0b | 407 | fprintf (inptr, "%s", cstring_toCharsSafe (text)); |
dfd82dce | 408 | check (fileTable_closeFile (context_fileTable (), inptr)); |
616915dd | 409 | |
410 | /* the default is to delete the input file */ | |
411 | ||
4dd72714 | 412 | outfile = fileTable_fileName (fileTable_addltemp (context_fileTable ())); |
616915dd | 413 | invokeLSL (infile, outfile, context_getFlag (FLG_KEEP)); |
28bf4b0b | 414 | cstring_free (text); |
616915dd | 415 | } |
416 | ||
28bf4b0b | 417 | static void invokeLSL (cstring infile, cstring outfile, bool deletep) |
616915dd | 418 | { |
419 | /* run lsl on infile and leave result in outfile */ | |
420 | FILE *outptr; | |
421 | filestatus status; | |
422 | int callstatus; | |
423 | cstring call; | |
28bf4b0b | 424 | cstring returnPath = cstring_undefined; |
616915dd | 425 | |
426 | /* | |
427 | ** Ensures that outfile can be written into, should find a better | |
428 | ** way to do this. | |
429 | */ | |
430 | ||
d5047b91 | 431 | outptr = fileTable_createFile (context_fileTable (), outfile); |
616915dd | 432 | |
433 | if (outptr == NULL) | |
434 | { | |
435 | /* fopen fails */ | |
436 | llfatalerror (message ("Unable to write intermediate file: %s", | |
28bf4b0b | 437 | outfile)); |
616915dd | 438 | } |
439 | ||
dfd82dce | 440 | check (fileTable_closeFile (context_fileTable (), outptr)); |
616915dd | 441 | |
442 | /* set call to the right command */ | |
28bf4b0b | 443 | status = osd_getExePath (cstring_makeLiteralTemp ("PATH"), |
444 | cstring_makeLiteralTemp ("lsl"), | |
445 | &returnPath); | |
616915dd | 446 | |
447 | ||
448 | if (status == OSD_FILEFOUND) | |
449 | { | |
28bf4b0b | 450 | call = message ("%s -syms %s > %s", returnPath, infile, outfile); |
616915dd | 451 | |
452 | /* before calling, make sure old file is removed */ | |
453 | (void) osd_unlink (outfile); | |
454 | ||
28bf4b0b | 455 | callstatus = osd_system (call); |
616915dd | 456 | |
457 | cstring_free (call); | |
458 | ||
459 | if (callstatus != CALL_SUCCESS) | |
460 | { | |
461 | /* | |
462 | ** lsl errors: call lsl again without -syms, sending output to stdout | |
463 | */ | |
28bf4b0b | 464 | cstring syscal = message ("%s %s", returnPath, infile); |
465 | (void) osd_system (syscal); | |
616915dd | 466 | cstring_free (syscal); |
467 | ||
468 | llfatalerror (cstring_makeLiteral ("LSL trait used contains errors.")); | |
469 | } | |
470 | else | |
471 | { /* ok, go ahead */ | |
472 | /* Now parse the LSL output and store info in symbol table */ | |
28bf4b0b | 473 | callstatus = parseSignatures (cstring_copy (outfile)); |
616915dd | 474 | |
475 | if (callstatus == 0) | |
476 | { | |
477 | /* all went well */ | |
478 | if (!context_getFlag (FLG_KEEP)) | |
479 | { | |
480 | /* delete temporary files */ | |
481 | if (deletep) | |
482 | { | |
483 | (void) osd_unlink (infile); | |
484 | } | |
485 | ||
486 | (void) osd_unlink (outfile); | |
487 | } | |
488 | } | |
489 | } | |
490 | } | |
491 | else if (status == OSD_FILENOTFOUND) | |
492 | { | |
493 | llfatalerror | |
494 | (cstring_makeLiteral ("Cannot find LSL checker: check your command search path.")); | |
495 | } | |
496 | else /* must be (status == OSD_PATHTOOLONG) */ | |
497 | { | |
498 | lclfatalbug ("invokeLSL: lsl plus directory from search path is too long"); | |
499 | } | |
500 | } | |
501 | ||
502 | /* callLSL ("MySet", "includes Set (CC for C, EE for E)"); */ | |
503 | ||
504 | void | |
505 | readlsignatures (interfaceNode n) | |
506 | { | |
507 | /* assume n->kind = usesKIND */ | |
28bf4b0b | 508 | callLSL (g_currentSpec, printTraitRefList2 (n->content.uses)); |
616915dd | 509 | } |