]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* ;-*-C-*-; |
1b8ae690 | 2 | ** Splint - annotation-assisted static program checker |
3 | ** Copyright (C) 1994-2002 University of Virginia, | |
4 | ** Massachusetts Institute of Technology | |
885824d3 | 5 | ** |
1b8ae690 | 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 | ** |
155af98d | 20 | ** For information on splint: info@splint.org |
21 | ** To report a bug: splint-bug@splint.org | |
1b8ae690 | 22 | ** For more information: http://www.splint.org |
885824d3 | 23 | */ |
24 | /* | |
25 | ** cttable.i | |
26 | ** | |
27 | ** NOTE: This is not a stand-alone source file, but is included in ctype.c. | |
28 | ** (This is necessary becuase there is no other way in C to have a | |
29 | ** hidden scope, besides at the file level.) | |
30 | */ | |
31 | ||
32 | /*@access ctype@*/ | |
33 | ||
34 | /* | |
35 | ** type definitions and forward declarations in ctbase.i | |
36 | */ | |
37 | ||
38 | static void | |
39 | ctentry_free (/*@only@*/ ctentry c) | |
40 | { | |
41 | ctbase_free (c->ctbase); | |
42 | cstring_free (c->unparse); | |
43 | sfree (c); | |
44 | } | |
45 | ||
46 | static void cttable_reset (void) | |
47 | /*@globals cttab@*/ | |
48 | /*@modifies cttab@*/ | |
49 | { | |
50 | if (cttab.entries != NULL) | |
51 | { | |
52 | int i; | |
53 | ||
54 | for (i = 0; i < cttab.size; i++) | |
55 | { | |
86d93ed3 | 56 | /*drl bee: si*/ ctentry_free (cttab.entries[i]); |
885824d3 | 57 | } |
58 | ||
59 | /*@-compdestroy@*/ | |
60 | sfree (cttab.entries); | |
61 | /*@=compdestroy@*/ | |
62 | ||
63 | cttab.entries = NULL; | |
64 | } | |
65 | ||
66 | cttab.size = 0 ; | |
67 | cttab.nspace = 0 ; | |
68 | } | |
69 | ||
885824d3 | 70 | static ctentry |
71 | ctentry_makeNew (ctkind ctk, /*@only@*/ ctbase c) | |
72 | { | |
73 | ||
74 | return (ctentry_make (ctk, c, ctype_dne, ctype_dne, ctype_dne, cstring_undefined)); | |
75 | } | |
76 | ||
77 | static /*@only@*/ ctentry | |
78 | ctentry_make (ctkind ctk, | |
79 | /*@keep@*/ ctbase c, ctype base, | |
80 | ctype ptr, ctype array, | |
81 | /*@keep@*/ cstring unparse) /*@*/ | |
82 | { | |
83 | ctentry cte = (ctentry) dmalloc (sizeof (*cte)); | |
84 | cte->kind = ctk; | |
85 | cte->ctbase = c; | |
86 | cte->base = base; | |
87 | cte->ptr = ptr; | |
88 | cte->array = array; | |
89 | cte->unparse = unparse; | |
90 | return cte; | |
91 | } | |
92 | ||
93 | static cstring | |
94 | ctentry_unparse (ctentry c) | |
95 | { | |
96 | return (message | |
97 | ("%20s [%d] [%d] [%d]", | |
98 | (cstring_isDefined (c->unparse) ? c->unparse : cstring_makeLiteral ("<no name>")), | |
99 | c->base, | |
100 | c->ptr, | |
101 | c->array)); | |
102 | } | |
103 | ||
104 | static bool | |
105 | ctentry_isInteresting (ctentry c) | |
106 | { | |
107 | return (cstring_isNonEmpty (c->unparse)); | |
108 | } | |
109 | ||
110 | static /*@only@*/ cstring | |
111 | ctentry_dump (ctentry c) | |
112 | { | |
a0a162cd | 113 | DPRINTF (("Dumping: %s", ctentry_unparse (c))); |
114 | ||
885824d3 | 115 | if (c->ptr == ctype_dne |
116 | && c->array == ctype_dne | |
117 | && c->base == ctype_dne) | |
118 | { | |
119 | return (message ("%d %q&", | |
120 | ctkind_toInt (c->kind), | |
121 | ctbase_dump (c->ctbase))); | |
122 | } | |
123 | else if (c->base == ctype_undefined | |
124 | && c->array == ctype_dne) | |
125 | { | |
126 | if (c->ptr == ctype_dne) | |
127 | { | |
128 | return (message ("%d %q!", | |
129 | ctkind_toInt (c->kind), | |
130 | ctbase_dump (c->ctbase))); | |
131 | } | |
132 | else | |
133 | { | |
134 | return (message ("%d %q^%d", | |
135 | ctkind_toInt (c->kind), | |
136 | ctbase_dump (c->ctbase), | |
137 | c->ptr)); | |
138 | } | |
139 | } | |
140 | else if (c->ptr == ctype_dne | |
141 | && c->array == ctype_dne) | |
142 | { | |
143 | return (message ("%d %q%d&", | |
144 | ctkind_toInt (c->kind), | |
145 | ctbase_dump (c->ctbase), | |
146 | c->base)); | |
147 | } | |
148 | else | |
149 | { | |
150 | return (message ("%d %q%d %d %d", | |
151 | ctkind_toInt (c->kind), | |
152 | ctbase_dump (c->ctbase), | |
153 | c->base, c->ptr, c->array)); | |
154 | } | |
155 | } | |
156 | ||
157 | ||
158 | static /*@only@*/ ctentry | |
86d93ed3 | 159 | ctentry_undump (/*@dependent@*/ char *s) /*@requires maxRead(s) >= 2 @*/ |
885824d3 | 160 | { |
161 | int base, ptr, array; | |
162 | ctkind kind; | |
163 | ctbase ct; | |
164 | ||
28bf4b0b | 165 | kind = ctkind_fromInt (reader_getInt (&s)); |
885824d3 | 166 | ct = ctbase_undump (&s); |
167 | ||
28bf4b0b | 168 | if (reader_optCheckChar (&s, '&')) |
885824d3 | 169 | { |
170 | base = ctype_dne; | |
171 | ptr = ctype_dne; | |
172 | array = ctype_dne; | |
173 | } | |
28bf4b0b | 174 | else if (reader_optCheckChar (&s, '!')) |
885824d3 | 175 | { |
176 | base = ctype_undefined; | |
177 | ptr = ctype_dne; | |
178 | array = ctype_dne; | |
179 | } | |
28bf4b0b | 180 | else if (reader_optCheckChar (&s, '^')) |
885824d3 | 181 | { |
182 | base = ctype_undefined; | |
28bf4b0b | 183 | ptr = reader_getInt (&s); |
885824d3 | 184 | array = ctype_dne; |
185 | } | |
186 | else | |
187 | { | |
28bf4b0b | 188 | base = reader_getInt (&s); |
885824d3 | 189 | |
28bf4b0b | 190 | if (reader_optCheckChar (&s, '&')) |
885824d3 | 191 | { |
192 | ptr = ctype_dne; | |
193 | array = ctype_dne; | |
194 | } | |
195 | else | |
196 | { | |
28bf4b0b | 197 | ptr = reader_getInt (&s); |
198 | array = reader_getInt (&s); | |
885824d3 | 199 | } |
200 | } | |
201 | ||
202 | /* can't unparse w/o typeTable */ | |
203 | return (ctentry_make (kind, ct, base, ptr, array, cstring_undefined)); | |
204 | } | |
205 | ||
206 | static /*@observer@*/ cstring | |
207 | ctentry_doUnparse (ctentry c) /*@modifies c@*/ | |
208 | { | |
209 | if (cstring_isDefined (c->unparse)) | |
210 | { | |
211 | return (c->unparse); | |
212 | } | |
213 | else | |
214 | { | |
215 | cstring s = ctbase_unparse (c->ctbase); | |
216 | ||
217 | if (!cstring_isEmpty (s) && !cstring_containsChar (s, '<')) | |
218 | { | |
219 | c->unparse = s; | |
220 | } | |
221 | else | |
222 | { | |
223 | cstring_markOwned (s); | |
224 | } | |
225 | ||
226 | return (s); | |
227 | } | |
228 | } | |
229 | ||
230 | static /*@observer@*/ cstring | |
231 | ctentry_doUnparseDeep (ctentry c) | |
232 | { | |
233 | if (cstring_isDefined (c->unparse)) | |
234 | { | |
235 | return (c->unparse); | |
236 | } | |
237 | else | |
238 | { | |
239 | c->unparse = ctbase_unparseDeep (c->ctbase); | |
240 | return (c->unparse); | |
241 | } | |
242 | } | |
243 | ||
244 | /* | |
245 | ** cttable operations | |
246 | */ | |
247 | ||
248 | static /*@only@*/ cstring | |
249 | cttable_unparse (void) | |
250 | { | |
251 | int i; | |
252 | cstring s = cstring_undefined; | |
253 | ||
254 | /*@access ctbase@*/ | |
255 | for (i = 0; i < cttab.size; i++) | |
256 | { | |
86d93ed3 | 257 | /*drl bee: si*/ ctentry cte = cttab.entries[i]; |
885824d3 | 258 | if (ctentry_isInteresting (cte)) |
259 | { | |
260 | if (ctbase_isUA (cte->ctbase)) | |
261 | { | |
262 | s = message ("%s%d\t%q [%d]\n", s, i, ctentry_unparse (cttab.entries[i]), | |
263 | cte->ctbase->contents.tid); | |
264 | } | |
265 | else | |
266 | { | |
267 | s = message ("%s%d\t%q\n", s, i, ctentry_unparse (cttab.entries[i])); | |
268 | } | |
269 | } | |
270 | } | |
271 | /*@noaccess ctbase@*/ | |
272 | return (s); | |
273 | } | |
274 | ||
275 | void | |
276 | cttable_print (void) | |
277 | { | |
278 | int i; | |
279 | ||
280 | /*@access ctbase@*/ | |
281 | for (i = 0; i < cttab.size; i++) | |
282 | { | |
86d93ed3 | 283 | /*drl bee: si*/ ctentry cte = cttab.entries[i]; |
885824d3 | 284 | |
28bf4b0b | 285 | if (TRUE) /* ctentry_isInteresting (cte)) */ |
885824d3 | 286 | { |
287 | if (ctbase_isUA (cte->ctbase)) | |
288 | { | |
289 | fprintf (g_msgstream, "%3d: %s [%d]\n", i, | |
290 | cstring_toCharsSafe (ctentry_doUnparse (cttab.entries[i])), | |
291 | cte->ctbase->contents.tid); | |
292 | } | |
293 | else | |
294 | { | |
295 | fprintf (g_msgstream, "%3d: %s\n", i, | |
296 | cstring_toCharsSafe (ctentry_doUnparse (cttab.entries[i]))); | |
297 | } | |
298 | } | |
299 | else | |
300 | { | |
301 | /* fprintf (g_msgstream, "%3d: <no name>\n", i); */ | |
302 | } | |
303 | } | |
304 | /*@noaccess ctbase@*/ | |
305 | } | |
306 | ||
307 | /* | |
308 | ** cttable_dump | |
309 | ** | |
310 | ** Output cttable for dump file | |
311 | */ | |
312 | ||
313 | static void | |
314 | cttable_dump (FILE *fout) | |
315 | { | |
316 | bool showdots = FALSE; | |
317 | int showdotstride = 0; | |
318 | int i; | |
319 | ||
320 | if (context_getFlag (FLG_SHOWSCAN) && cttab.size > 5000) | |
321 | { | |
322 | fprintf (g_msgstream, " >\n"); /* end dumping to */ | |
323 | fprintf (g_msgstream, "< Dumping type table (%d types) ", cttab.size); | |
324 | showdotstride = cttab.size / 5; | |
325 | showdots = TRUE; | |
326 | } | |
327 | ||
28bf4b0b | 328 | /* |
329 | DPRINTF (("Dumping cttable: ")); | |
330 | cttable_print (); | |
331 | */ | |
332 | ||
885824d3 | 333 | for (i = 0; i < cttab.size; i++) |
334 | { | |
335 | cstring s; | |
336 | ||
86d93ed3 | 337 | /*drl bee: si*/ s = ctentry_dump (cttab.entries[i]); |
28bf4b0b | 338 | DPRINTF (("[%d] = %s", i, ctentry_unparse (cttab.entries[i]))); |
885824d3 | 339 | llassert (cstring_length (s) < MAX_DUMP_LINE_LENGTH); |
340 | fputline (fout, cstring_toCharsSafe (s)); | |
341 | cstring_free (s); | |
342 | ||
343 | if (showdots && (i != 0 && ((i - 1) % showdotstride == 0))) | |
344 | { | |
345 | (void) fflush (g_msgstream); | |
346 | fprintf (stderr, "."); | |
347 | (void) fflush (stderr); | |
348 | } | |
349 | } | |
350 | ||
351 | if (showdots) | |
352 | { | |
353 | fprintf (stderr, " >\n< Continuing dump "); | |
354 | } | |
355 | ||
a0a162cd | 356 | } |
885824d3 | 357 | |
358 | /* | |
359 | ** load cttable from init file | |
360 | */ | |
361 | ||
362 | static void cttable_load (FILE *f) | |
363 | /*@globals cttab @*/ | |
364 | /*@modifies cttab, f @*/ | |
365 | { | |
366 | char *s = mstring_create (MAX_DUMP_LINE_LENGTH); | |
367 | ctentry cte; | |
368 | ||
369 | cttable_reset (); | |
370 | ||
28bf4b0b | 371 | /* |
372 | DPRINTF (("Loading cttable: ")); | |
373 | cttable_print (); | |
374 | */ | |
375 | ||
376 | while (reader_readLine (f, s, MAX_DUMP_LINE_LENGTH) != NULL && *s == ';') | |
885824d3 | 377 | { |
378 | ; | |
379 | } | |
380 | ||
381 | if (mstring_length (s) == (MAX_DUMP_LINE_LENGTH - 1)) | |
382 | { | |
383 | llbug (message ("Library line too long: %s\n", cstring_fromChars (s))); | |
384 | } | |
385 | ||
386 | while (s != NULL && *s != ';' && *s != '\0') | |
387 | { | |
388 | ctype ct; | |
389 | ||
86d93ed3 | 390 | /*drl bee: tcf*/ cte = ctentry_undump (s); |
885824d3 | 391 | ct = cttable_addFull (cte); |
392 | ||
28bf4b0b | 393 | DPRINTF (("Type: %d: %s", ct, ctype_unparse (ct))); |
394 | ||
885824d3 | 395 | if (ctbase_isConj (cte->ctbase) |
28bf4b0b | 396 | && !(ctbase_isExplicitConj (cte->ctbase))) |
885824d3 | 397 | { |
398 | ctype_recordConj (ct); | |
399 | } | |
400 | ||
28bf4b0b | 401 | (void) reader_readLine (f, s, MAX_DUMP_LINE_LENGTH); |
885824d3 | 402 | } |
403 | ||
404 | sfree (s); | |
28bf4b0b | 405 | |
406 | /* | |
407 | DPRINTF (("Done loading cttable: ")); | |
408 | cttable_print (); | |
409 | */ | |
410 | } | |
885824d3 | 411 | |
412 | /* | |
413 | ** cttable_init | |
414 | ** | |
415 | ** fill up the cttable with basic types, and first order derivations. | |
416 | ** this is done without using our constructors for efficiency reasons | |
417 | ** (probably bogus) | |
418 | ** | |
419 | */ | |
420 | ||
421 | /*@access cprim@*/ | |
422 | static void cttable_init (void) | |
423 | /*@globals cttab@*/ /*@modifies cttab@*/ | |
424 | { | |
425 | ctkind i; | |
426 | cprim j; | |
427 | ctbase ct = ctbase_undefined; | |
428 | ||
429 | llassert (cttab.size == 0); | |
430 | ||
431 | /* do for plain, pointer, arrayof */ | |
432 | for (i = CTK_PLAIN; i <= CTK_ARRAY; i++) | |
433 | { | |
434 | for (j = CTX_UNKNOWN; j <= CTX_LAST; j++) | |
435 | { | |
436 | if (i == CTK_PLAIN) | |
437 | { | |
438 | if (j == CTX_BOOL) | |
439 | { | |
440 | ct = ctbase_createBool (); /* why different? */ | |
441 | } | |
442 | else if (j == CTX_UNKNOWN) | |
443 | { | |
444 | ct = ctbase_createUnknown (); | |
445 | } | |
446 | else | |
447 | { | |
448 | ct = ctbase_createPrim ((cprim)j); | |
449 | } | |
450 | ||
451 | (void) cttable_addFull | |
452 | (ctentry_make (CTK_PLAIN, | |
453 | ct, ctype_undefined, | |
454 | j + CTK_PREDEFINED, j + CTK_PREDEFINED2, | |
455 | ctbase_unparse (ct))); | |
456 | } | |
457 | else | |
458 | { | |
459 | switch (i) | |
460 | { | |
461 | case CTK_PTR: | |
462 | ct = ctbase_makePointer (j); | |
463 | /*@switchbreak@*/ break; | |
464 | case CTK_ARRAY: | |
465 | ct = ctbase_makeArray (j); | |
466 | /*@switchbreak@*/ break; | |
467 | default: | |
468 | llbugexitlit ("cttable_init: base case"); | |
469 | } | |
470 | ||
471 | (void) cttable_addDerived (i, ct, j); | |
472 | } | |
473 | } | |
474 | } | |
475 | ||
476 | /**** reserve a slot for userBool ****/ | |
477 | (void) cttable_addFull (ctentry_make (CTK_INVALID, ctbase_undefined, | |
478 | ctype_undefined, ctype_dne, ctype_dne, | |
479 | cstring_undefined)); | |
480 | } | |
481 | ||
482 | /*@noaccess cprim@*/ | |
483 | ||
484 | static void | |
485 | cttable_grow () | |
486 | { | |
487 | int i; | |
488 | o_ctentry *newentries ; | |
489 | ||
490 | cttab.nspace = CTK_BASESIZE; | |
491 | newentries = (ctentry *) dmalloc (sizeof (*newentries) * (cttab.size + cttab.nspace)); | |
492 | ||
493 | if (newentries == NULL) | |
494 | { | |
495 | llfatalerror (message ("cttable_grow: out of memory. Size: %d", | |
496 | cttab.size)); | |
497 | } | |
498 | ||
499 | for (i = 0; i < cttab.size; i++) | |
500 | { | |
86d93ed3 | 501 | /*drl bee: dm*/ /*drl bee: si*/ newentries[i] = cttab.entries[i]; |
885824d3 | 502 | } |
503 | ||
504 | /*@-compdestroy@*/ | |
505 | sfree (cttab.entries); | |
506 | /*@=compdestroy@*/ | |
507 | ||
508 | cttab.entries = newentries; | |
509 | /*@-compdef@*/ | |
510 | } /*@=compdef@*/ | |
511 | ||
512 | static ctype | |
513 | cttable_addDerived (ctkind ctk, /*@keep@*/ ctbase cnew, ctype base) | |
514 | { | |
515 | if (cttab.nspace == 0) | |
516 | cttable_grow (); | |
517 | ||
86d93ed3 | 518 | /*drl bee: si*/ cttab.entries[cttab.size] = |
885824d3 | 519 | ctentry_make (ctk, cnew, base, ctype_dne, ctype_dne, cstring_undefined); |
520 | ||
521 | cttab.nspace--; | |
522 | ||
523 | return (cttab.size++); | |
524 | } | |
525 | ||
526 | static ctype | |
28bf4b0b | 527 | cttable_addComplex (/*@only@*/ ctbase cnew) |
885824d3 | 528 | /*@modifies cttab; @*/ |
529 | { | |
28bf4b0b | 530 | /*@access ctbase@*/ |
885824d3 | 531 | if (cnew->type != CT_FCN && cnew->type != CT_EXPFCN) |
532 | { | |
533 | ctype i; | |
534 | int ctstop = cttable_lastIndex () - DEFAULT_OPTLEVEL; | |
535 | ||
536 | if (ctstop < LAST_PREDEFINED) | |
537 | { | |
538 | ctstop = LAST_PREDEFINED; | |
539 | } | |
540 | ||
541 | for (i = cttable_lastIndex (); i >= ctstop; i--) /* better to go from back... */ | |
542 | { | |
543 | ctbase ctb; | |
544 | ||
885824d3 | 545 | ctb = ctype_getCtbase (i); |
28bf4b0b | 546 | |
547 | /*@i32 is this optimization really worthwhile??? */ | |
885824d3 | 548 | |
549 | if (ctbase_isDefined (ctb) && ctbase_equivStrict (cnew, ctb)) | |
550 | { | |
a0a162cd | 551 | DPRINTF (("EQUIV!! %s / %s", |
552 | ctbase_unparse (cnew), | |
553 | ctbase_unparse (ctb))); | |
28bf4b0b | 554 | |
885824d3 | 555 | ctbase_free (cnew); |
885824d3 | 556 | return i; |
557 | } | |
558 | } | |
559 | } | |
560 | ||
561 | if (cttab.nspace == 0) | |
562 | cttable_grow (); | |
563 | ||
86d93ed3 | 564 | /*drl bee: si*/ cttab.entries[cttab.size] = ctentry_make (CTK_COMPLEX, cnew, ctype_undefined, |
885824d3 | 565 | ctype_dne, ctype_dne, |
566 | cstring_undefined); | |
567 | cttab.nspace--; | |
568 | ||
569 | return (cttab.size++); | |
28bf4b0b | 570 | /*@noaccess ctbase@*/ |
885824d3 | 571 | } |
572 | ||
573 | static ctype | |
574 | cttable_addFull (ctentry cnew) | |
575 | { | |
576 | if (cttab.nspace == 0) | |
577 | { | |
578 | cttable_grow (); | |
579 | } | |
580 | ||
86d93ed3 | 581 | /*drl bee: si*/ cttab.entries[cttab.size] = cnew; |
885824d3 | 582 | cttab.nspace--; |
583 | ||
584 | return (cttab.size++); | |
585 | } | |
586 | ||
587 | static ctype | |
588 | cttable_addFullSafe (/*@only@*/ ctentry cnew) | |
589 | { | |
590 | int i; | |
591 | ctbase cnewbase = cnew->ctbase; | |
592 | ||
593 | llassert (ctbase_isDefined (cnewbase)); | |
594 | ||
595 | for (i = cttable_lastIndex (); i >= CT_FIRST; i--) | |
596 | { | |
597 | ctbase ctb = ctype_getCtbase (i); | |
598 | ||
599 | if (ctbase_isDefined (ctb) | |
600 | && ctbase_equiv (cnewbase, ctype_getCtbaseSafe (i))) | |
601 | { | |
602 | ctentry_free (cnew); | |
603 | return i; | |
604 | } | |
605 | } | |
606 | ||
607 | if (cttab.nspace == 0) | |
608 | cttable_grow (); | |
609 | ||
86d93ed3 | 610 | /*drl bee: si*/ cttab.entries[cttab.size] = cnew; |
885824d3 | 611 | |
612 | cttab.nspace--; | |
613 | ||
614 | return (cttab.size++); | |
615 | } | |
616 |