2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 University of Virginia,
4 ** Massachusetts Institute of Technology
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.
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.
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.
20 ** For information on splint: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
28 # include "splintMacros.nf"
31 /*@constant int ATINVALID; @*/
35 aliasTable_canAliasAux (aliasTable p_s, sRef p_sr, int p_lim) /*@*/ ;
37 aliasTable_aliasedByLimit (aliasTable p_s, sRef p_sr, int p_lim) /*@*/ ;
39 aliasTable_aliasedByAux (aliasTable p_s, sRef p_sr, int p_lim) /*@*/ ;
44 return (aliasTable_undefined);
47 static /*@only@*/ /*@notnull@*/ aliasTable
48 aliasTable_newEmpty (void)
50 aliasTable s = (aliasTable) dmalloc (sizeof (*s));
53 s->nspace = aliasTableBASESIZE;
54 s->keys = (sRef *) dmalloc (sizeof (*s->keys) * aliasTableBASESIZE);
55 s->values = (sRefSet *) dmalloc (sizeof (*s->values) * aliasTableBASESIZE);
61 aliasTable_grow (/*@notnull@*/ aliasTable s)
64 o_sRefSet *oldvalues = s->values;
65 sRef *oldkeys = s->keys;
67 s->nspace += aliasTableBASESIZE;
69 s->values = (sRefSet *) dmalloc (sizeof (*s->values)
70 * (s->nelements + s->nspace));
71 s->keys = (sRef *) dmalloc (sizeof (*s->keys) * (s->nelements + aliasTableBASESIZE));
73 if (s->keys == (sRef *) 0 || s->values == (sRefSet *)0)
75 llfatalerror (cstring_makeLiteral ("aliasTable_grow: out of memory!"));
78 for (i = 0; i < s->nelements; i++)
80 s->values[i] = oldvalues[i];
81 s->keys[i] = oldkeys[i];
88 static int aliasTable_lookupRefs (/*@notnull@*/ aliasTable s, sRef sr)
93 for (i = 0; i < aliasTable_size (s); i++)
95 if (sRef_same (sr, s->keys[i]))
105 ** sr aliases al (and anything al aliases!)
109 aliasTable_addMustAlias (/*@returned@*/ aliasTable s,
110 /*@exposed@*/ sRef sr,
111 /*@exposed@*/ sRef al)
116 llassert (NOALIAS (sr, al));
118 DPRINTF (("Adding alias: %s / %s", sRef_unparseFull (sr),
119 sRef_unparseFull (al)));
121 if (aliasTable_isUndefined (s))
123 s = aliasTable_newEmpty ();
128 ind = aliasTable_lookupRefs (s, sr);
131 ss = aliasTable_canAlias (s, al);
132 DPRINTF (("Previous aliases: %s", sRefSet_unparse (ss)));
134 if (ind == ATINVALID)
136 if (s->nspace <= 0) {
141 s->keys[s->nelements] = sr;
142 s->values[s->nelements] = sRefSet_single (al);
148 s->values[ind] = sRefSet_insert (s->values[ind], al);
151 s->values[ind] = sRefSet_unionExcept (s->values[ind], ss, s->keys[ind]);
152 DPRINTF (("New aliases: %s", sRefSet_unparse (s->values[ind])));
159 aliasTable_addSet (/*@returned@*/ aliasTable s,
160 /*@exposed@*/ sRef key, /*@only@*/ sRefSet value)
162 if (!sRefSet_isEmpty (value))
164 if (aliasTable_isUndefined (s))
166 s = aliasTable_newEmpty ();
177 s->keys[s->nelements] = key;
178 s->values[s->nelements] = value;
183 sRefSet_free (value);
190 ** When aliases are cleared:
192 ** o remove all entries for sr
193 ** o replace all aliases for things which alias sr with sr's aliases
195 ** Clear aliases for sr; if sr is a direct param reference, clear its aliases too.
198 static void aliasTable_clearAliasesAux (/*@notnull@*/ aliasTable p_s, sRef p_sr)
201 void aliasTable_clearAliases (aliasTable s, sRef sr)
203 if (aliasTable_isUndefined (s))
209 sRef rb = sRef_getRootBase (sr);
212 if (!sRef_isCvar (sr) && sRef_isLocalVar (rb))
214 int ind = aliasTable_lookupRefs (s, rb);
216 if (ind != ATINVALID)
218 sRefSet al = s->values[ind];
221 sRefSet_realElements (al, el)
224 if (sRef_isParam (el))
226 if (sRef_sameName (el, rb))
228 sRef fb = sRef_fixBase (sr, el);
230 aliasTable_clearAliasesAux (s, fb);
233 } end_sRefSet_realElements ;
237 aliasTable_clearAliasesAux (s, sr);
242 void aliasTable_clearAliasesAux (/*@notnull@*/ aliasTable s, sRef sr)
246 for (i = 0; i < s->nelements; i++)
248 sRef key = s->keys[i];
250 if (sRef_includedBy (key, sr))
252 sRefSet_clear (s->values[i]);
256 (void) sRefSet_deleteBase (s->values[i], sr);
262 ** returns set of all sRefs that must alias sr (but are different from sr)
265 static /*@only@*/ sRefSet aliasTable_aliasedByAux (aliasTable s, sRef sr, int lim)
267 static bool hadWarning = FALSE;
268 sRefSet res = sRefSet_undefined;
271 llassert (!sRef_isConj (sr));
274 if (aliasTable_isUndefined (s) || lim >= ALIASSEARCHLIMIT)
276 if (lim >= ALIASSEARCHLIMIT && !hadWarning)
279 (message ("Alias search limit exceeded, checking %q. "
280 "This either means there is a variable with at least "
281 "%d indirections, or there is a bug in Splint.",
288 return sRefSet_undefined;
294 if (sRef_isPointer (sr))
296 abl = aliasTable_aliasedByLimit (s, sRef_getBase (sr), lim);
297 res = sRefSet_addIndirection (abl);
299 else if (sRef_isAddress (sr))
301 abl = aliasTable_aliasedByLimit (s, sRef_getBase (sr), lim);
302 res = sRefSet_removeIndirection (abl);
304 else if (sRef_isField (sr))
306 abl = aliasTable_aliasedByLimit (s, sRef_getBase (sr), lim);
307 res = sRefSet_accessField (abl, sRef_getField (sr));
309 else if (sRef_isArrayFetch (sr))
311 abl = aliasTable_aliasedByLimit (s, sRef_getBase (sr), lim);
313 if (sRef_isIndexKnown (sr))
315 int idx = sRef_getIndex (sr);
317 res = sRefSet_fetchKnown (abl, idx);
321 res = sRefSet_fetchUnknown (abl);
326 abl = sRefSet_undefined;
332 for (i = 0; i < s->nelements; i++)
334 sRef elem = s->keys[i];
336 if (!sRef_same (sr, elem)) /* was sameName */
339 sRefSet_realElements (s->values[i], current)
342 if (sRef_similar (sr, current))
344 res = sRefSet_insert (res, sRef_fixOuterRef (elem));
345 /*@innerbreak@*/ break;
347 } end_sRefSet_realElements;
354 static /*@only@*/ sRefSet aliasTable_aliasedByLimit (aliasTable s, sRef sr, int lim)
359 if (sRef_isConj (sr))
361 res = sRefSet_unionFree (aliasTable_aliasedByLimit (s, sRef_getConjA (sr), lim),
362 aliasTable_aliasedByLimit (s, sRef_getConjB (sr), lim));
366 res = aliasTable_aliasedByAux (s, sr, lim + 1);
372 /*@only@*/ sRefSet aliasTable_aliasedBy (aliasTable s, sRef sr)
374 if (sRef_isConj (sr))
376 return (sRefSet_unionFree (aliasTable_aliasedBy (s, sRef_getConjA (sr)),
377 aliasTable_aliasedBy (s, sRef_getConjB (sr))));
380 return (aliasTable_aliasedByAux (s, sr, 0));
383 /*@only@*/ sRefSet aliasTable_canAlias (aliasTable s, sRef sr)
388 if (sRef_isConj (sr))
390 res = sRefSet_unionFree (aliasTable_canAlias (s, sRef_getConjA (sr)),
391 aliasTable_canAlias (s, sRef_getConjB (sr)));
395 res = aliasTable_canAliasAux (s, sr, 0);
402 ** need to limit the depth of aliasing searches
405 static /*@only@*/ sRefSet aliasTable_canAliasLimit (aliasTable s, sRef sr, int lim)
409 if (sRef_isConj (sr))
411 sRefSet a = aliasTable_canAliasLimit (s, sRef_getConjA (sr), lim);
412 sRefSet b = aliasTable_canAliasLimit (s, sRef_getConjB (sr), lim);
414 res = sRefSet_unionFree (a, b);
418 res = aliasTable_canAliasAux (s, sr, lim + 1);
424 static /*@only@*/ sRefSet
425 aliasTable_canAliasAux (aliasTable s, sRef sr, int lim)
427 static bool hadWarning = FALSE;
428 llassert (!sRef_isConj (sr));
431 if (aliasTable_isUndefined (s) || lim >= ALIASSEARCHLIMIT)
433 if (lim >= ALIASSEARCHLIMIT && !hadWarning)
436 (message ("Alias search limit exceeded, checking %q. "
437 "This either means there is a variable with at least "
438 "%d indirections, or there is a bug in Splint.",
445 return sRefSet_undefined;
449 int ind = aliasTable_lookupRefs (s, sr);
451 if (sRef_isPointer (sr) || sRef_isAddress (sr) || sRef_isField (sr)
452 || sRef_isArrayFetch (sr))
454 sRef base = sRef_getBase (sr);
455 sRefSet tmp = aliasTable_canAliasLimit (s, base, lim);
458 if (sRef_isPointer (sr))
460 ret = sRefSet_addIndirection (tmp);
462 else if (sRef_isAddress (sr))
464 ret = sRefSet_removeIndirection (tmp);
466 else if (sRef_isField (sr))
468 ret = sRefSet_accessField (tmp, sRef_getField (sr));
470 else if (sRef_isArrayFetch (sr))
472 if (sRef_isIndexKnown (sr))
474 ret = sRefSet_fetchKnown (tmp, sRef_getIndex (sr));
478 ret = sRefSet_fetchUnknown (tmp);
486 if (ind != ATINVALID)
488 ret = sRefSet_union (ret, s->values[ind]);
495 if (ind == ATINVALID) return sRefSet_undefined;
497 return sRefSet_newCopy (s->values[ind]);
501 aliasTable aliasTable_copy (aliasTable s)
503 if (aliasTable_isEmpty (s))
505 return aliasTable_undefined;
509 aliasTable t = (aliasTable) dmalloc (sizeof (*s));
512 t->nelements = s->nelements;
514 t->keys = (sRef *) dmalloc (sizeof (*s->keys) * s->nelements);
515 t->values = (sRefSet *) dmalloc (sizeof (*s->values) * t->nelements);
517 for (i = 0; i < s->nelements; i++)
519 t->keys[i] = s->keys[i];
520 t->values[i] = sRefSet_newCopy (s->values[i]);
528 aliasTable_levelPrune (aliasTable s, int lexlevel)
532 if (aliasTable_isEmpty (s))
539 int backcount = s->nelements - 1;
541 for (i = 0; i <= backcount; i++)
543 sRef key = s->keys[i];
545 if (sRef_lexLevel (key) > lexlevel)
548 for (j = backcount; j > i; j--)
554 if (sRef_lexLevel (s->keys[j]) <= lexlevel)
556 s->keys[i] = s->keys[j];
557 s->values[i] = s->values[j];
558 sRefSet_levelPrune (s->values[i], lexlevel);
559 /*@innerbreak@*/ break;
567 sRefSet_levelPrune (s->values[i], lexlevel);
576 ** like level union, but know that t2 was executed after t1. So if
577 ** t1 has x -> { a, b } and t2 has x -> { a }, then result has x -> { a }.
579 ** NOTE: t2 is "only".
582 aliasTable aliasTable_levelUnionSeq (/*@returned@*/ aliasTable t1,
583 /*@only@*/ aliasTable t2, int level)
585 if (aliasTable_isUndefined (t2))
590 if (aliasTable_isUndefined (t1))
592 t1 = aliasTable_newEmpty ();
596 aliasTable_levelPrune (t1, level);
599 aliasTable_elements (t2, key, value)
601 if (sRef_lexLevel (key) <= level)
603 int ind = aliasTable_lookupRefs (t1, key);
605 sRefSet_levelPrune (value, level);
607 if (ind == ATINVALID)
609 /* okay, t2 is killed */
610 /*@-exposetrans@*/ /*@-dependenttrans@*/
611 t1 = aliasTable_addSet (t1, key, value);
612 /*@=exposetrans@*/ /*@=dependenttrans@*/
616 sRefSet_free (t1->values[ind]);
618 /*@-dependenttrans@*/ /* okay, t2 is killed */
619 t1->values[ind] = value;
620 /*@=dependenttrans@*/
625 /*@-exposetrans@*/ /*@-dependenttrans@*/
626 sRefSet_free (value);
627 /*@=exposetrans@*/ /*@=dependenttrans@*/
630 } end_aliasTable_elements;
640 aliasTable_levelUnion (/*@returned@*/ aliasTable t1, aliasTable t2, int level)
642 if (aliasTable_isUndefined (t1))
644 if (aliasTable_isUndefined (t2))
650 t1 = aliasTable_newEmpty ();
655 aliasTable_levelPrune (t1, level);
658 aliasTable_elements (t2, key, cvalue)
660 sRefSet value = sRefSet_newCopy (cvalue);
662 if (sRef_lexLevel (key) <= level)
664 sRefSet_levelPrune (value, level);
666 if (sRefSet_size (value) > 0)
668 int ind = aliasTable_lookupRefs (t1, key);
670 if (ind == ATINVALID)
672 t1 = aliasTable_addSet (t1, key, value);
676 t1->values[ind] = sRefSet_union (t1->values[ind], value);
677 sRefSet_free (value);
682 sRefSet_free (value);
687 sRefSet_free (value);
689 } end_aliasTable_elements;
694 aliasTable aliasTable_levelUnionNew (aliasTable t1, aliasTable t2, int level)
696 aliasTable ret = aliasTable_levelUnion (aliasTable_copy (t1), t2, level);
702 aliasTable_unparse (aliasTable s)
704 cstring st = cstring_undefined;
706 if (aliasTable_isUndefined (s)) return (cstring_makeLiteral ("<NULL>"));
708 aliasTable_elements (s, key, value)
710 st = message ("%q\t%q -> %q\n", st, sRef_unparseFull (key),
711 sRefSet_unparseFull (value));
712 } end_aliasTable_elements;
722 aliasTable_fixSrefs (aliasTable s)
726 if (aliasTable_isUndefined (s)) return;
728 for (i = 0; i < s->nelements; i++)
730 sRef old = s->keys[i];
732 if (sRef_isLocalVar (old))
734 s->keys[i] = uentry_getSref (sRef_getUentry (old));
737 sRefSet_fixSrefs (s->values[i]);
742 aliasTable_free (/*@only@*/ aliasTable s)
746 if (aliasTable_isUndefined (s)) return;
748 for (i = 0; i < s->nelements; i++)
750 sRefSet_free (s->values[i]);
759 aliasTable_checkGlobs (aliasTable t)
761 aliasTable_elements (t, key, value)
763 sRef root = sRef_getRootBase (key);
765 if (sRef_isAliasCheckedGlobal (root))
767 sRefSet_realElements (value, sr)
769 root = sRef_getRootBase (sr);
771 if (((sRef_isAliasCheckedGlobal (root)
772 && !(sRef_similar (root, key)))
773 || sRef_isAnyParam (root))
774 && !sRef_isExposed (root))
776 if (sRef_isAliasCheckedGlobal (key))
778 if (!(sRef_isShared (key)
779 && sRef_isShared (root)))
784 ("Function returns with %q variable %q aliasing %q %q",
785 cstring_makeLiteral (sRef_isRealGlobal (key)
786 ? "global" : "file static"),
788 cstring_makeLiteral (sRef_isAnyParam (root)
789 ? "parameter" : "global"),
796 } end_sRefSet_realElements;
798 else if (sRef_isAnyParam (key) || sRef_isAnyParam (root))
800 sRefSet_realElements (value, sr)
802 root = sRef_getRootBase (sr);
804 if (sRef_isAliasCheckedGlobal (root)
805 && !sRef_isExposed (root)
806 && !sRef_isDead (key)
807 && !sRef_isShared (root))
811 message ("Function returns with parameter %q aliasing %q %q",
813 cstring_makeLiteral (sRef_isRealGlobal (root)
814 ? "global" : "file static"),
818 } end_sRefSet_realElements;
824 } end_aliasTable_elements;
830 ** For debugging only
833 void aliasTable_checkValid (aliasTable t)
835 aliasTable_elements (t, key, value)
837 sRef_checkCompletelyReasonable (key);
839 sRefSet_elements (value, sr)
841 sRef_checkCompletelyReasonable (sr);
842 } end_sRefSet_elements ;
843 } end_aliasTable_elements ;