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
]))
97 DPRINTF (("sRef match: %s / %s",
98 sRef_unparseFull (sr
),
99 sRef_unparseFull (s
->keys
[i
])));
108 ** sr aliases al (and anything al aliases!)
112 aliasTable_addMustAlias (/*@returned@*/ aliasTable s
,
113 /*@exposed@*/ sRef sr
,
114 /*@exposed@*/ sRef al
)
119 llassert (NOALIAS (sr
, al
));
121 DPRINTF (("Adding alias: %s / %s", sRef_unparseFull (sr
),
122 sRef_unparseFull (al
)));
124 if (aliasTable_isUndefined (s
))
126 s
= aliasTable_newEmpty ();
131 ind
= aliasTable_lookupRefs (s
, sr
);
134 ss
= aliasTable_canAlias (s
, al
);
135 DPRINTF (("Previous aliases: %s", sRefSet_unparse (ss
)));
137 if (ind
== ATINVALID
)
139 if (s
->nspace
<= 0) {
144 s
->keys
[s
->nelements
] = sr
;
145 s
->values
[s
->nelements
] = sRefSet_single (al
);
151 s
->values
[ind
] = sRefSet_insert (s
->values
[ind
], al
);
154 s
->values
[ind
] = sRefSet_unionExcept (s
->values
[ind
], ss
, s
->keys
[ind
]);
155 DPRINTF (("New aliases: %s", sRefSet_unparse (s
->values
[ind
])));
162 aliasTable_addSet (/*@returned@*/ aliasTable s
,
163 /*@exposed@*/ sRef key
, /*@only@*/ sRefSet value
)
165 if (!sRefSet_isEmpty (value
))
167 if (aliasTable_isUndefined (s
))
169 s
= aliasTable_newEmpty ();
180 s
->keys
[s
->nelements
] = key
;
181 s
->values
[s
->nelements
] = value
;
186 sRefSet_free (value
);
193 ** When aliases are cleared:
195 ** o remove all entries for sr
196 ** o replace all aliases for things which alias sr with sr's aliases
198 ** Clear aliases for sr; if sr is a direct param reference, clear its aliases too.
201 static void aliasTable_clearAliasesAux (/*@notnull@*/ aliasTable p_s
, sRef p_sr
)
204 void aliasTable_clearAliases (aliasTable s
, sRef sr
)
206 if (aliasTable_isUndefined (s
))
212 sRef rb
= sRef_getRootBase (sr
);
215 if (!sRef_isCvar (sr
) && sRef_isLocalVar (rb
))
217 int ind
= aliasTable_lookupRefs (s
, rb
);
219 if (ind
!= ATINVALID
)
221 sRefSet al
= s
->values
[ind
];
224 sRefSet_realElements (al
, el
)
227 if (sRef_isParam (el
))
229 if (sRef_sameName (el
, rb
))
231 sRef fb
= sRef_fixBase (sr
, el
);
233 aliasTable_clearAliasesAux (s
, fb
);
236 } end_sRefSet_realElements
;
240 aliasTable_clearAliasesAux (s
, sr
);
245 void aliasTable_clearAliasesAux (/*@notnull@*/ aliasTable s
, sRef sr
)
249 for (i
= 0; i
< s
->nelements
; i
++)
251 sRef key
= s
->keys
[i
];
253 if (sRef_includedBy (key
, sr
))
255 sRefSet_clear (s
->values
[i
]);
259 (void) sRefSet_deleteBase (s
->values
[i
], sr
);
265 ** returns set of all sRefs that must alias sr (but are different from sr)
268 static /*@only@*/ sRefSet
aliasTable_aliasedByAux (aliasTable s
, sRef sr
, int lim
)
270 static bool hadWarning
= FALSE
;
271 sRefSet res
= sRefSet_undefined
;
274 llassert (!sRef_isConj (sr
));
277 if (aliasTable_isUndefined (s
) || lim
>= ALIASSEARCHLIMIT
)
279 if (lim
>= ALIASSEARCHLIMIT
&& !hadWarning
)
282 (message ("Alias search limit exceeded, checking %q. "
283 "This either means there is a variable with at least "
284 "%d indirections, or there is a bug in Splint.",
291 return sRefSet_undefined
;
297 if (sRef_isPointer (sr
))
299 abl
= aliasTable_aliasedByLimit (s
, sRef_getBase (sr
), lim
);
300 res
= sRefSet_addIndirection (abl
);
302 else if (sRef_isAddress (sr
))
304 abl
= aliasTable_aliasedByLimit (s
, sRef_getBase (sr
), lim
);
305 res
= sRefSet_removeIndirection (abl
);
307 else if (sRef_isField (sr
))
309 abl
= aliasTable_aliasedByLimit (s
, sRef_getBase (sr
), lim
);
310 res
= sRefSet_accessField (abl
, sRef_getField (sr
));
312 else if (sRef_isArrayFetch (sr
))
314 abl
= aliasTable_aliasedByLimit (s
, sRef_getBase (sr
), lim
);
316 if (sRef_isIndexKnown (sr
))
318 int idx
= sRef_getIndex (sr
);
320 res
= sRefSet_fetchKnown (abl
, idx
);
324 res
= sRefSet_fetchUnknown (abl
);
329 abl
= sRefSet_undefined
;
335 for (i
= 0; i
< s
->nelements
; i
++)
337 sRef elem
= s
->keys
[i
];
339 if (!sRef_same (sr
, elem
)) /* was sameName */
342 sRefSet_realElements (s
->values
[i
], current
)
345 if (sRef_similar (sr
, current
))
347 res
= sRefSet_insert (res
, sRef_fixOuterRef (elem
));
348 /*@innerbreak@*/ break;
350 } end_sRefSet_realElements
;
357 static /*@only@*/ sRefSet
aliasTable_aliasedByLimit (aliasTable s
, sRef sr
, int lim
)
362 if (sRef_isConj (sr
))
364 res
= sRefSet_unionFree (aliasTable_aliasedByLimit (s
, sRef_getConjA (sr
), lim
),
365 aliasTable_aliasedByLimit (s
, sRef_getConjB (sr
), lim
));
369 res
= aliasTable_aliasedByAux (s
, sr
, lim
+ 1);
375 /*@only@*/ sRefSet
aliasTable_aliasedBy (aliasTable s
, sRef sr
)
377 if (sRef_isConj (sr
))
379 return (sRefSet_unionFree (aliasTable_aliasedBy (s
, sRef_getConjA (sr
)),
380 aliasTable_aliasedBy (s
, sRef_getConjB (sr
))));
383 return (aliasTable_aliasedByAux (s
, sr
, 0));
386 /*@only@*/ sRefSet
aliasTable_canAlias (aliasTable s
, sRef sr
)
390 if (sRef_isConj (sr
))
392 res
= sRefSet_unionFree (aliasTable_canAlias (s
, sRef_getConjA (sr
)),
393 aliasTable_canAlias (s
, sRef_getConjB (sr
)));
397 res
= aliasTable_canAliasAux (s
, sr
, 0);
404 ** need to limit the depth of aliasing searches
407 static /*@only@*/ sRefSet
aliasTable_canAliasLimit (aliasTable s
, sRef sr
, int lim
)
411 if (sRef_isConj (sr
))
413 sRefSet a
= aliasTable_canAliasLimit (s
, sRef_getConjA (sr
), lim
);
414 sRefSet b
= aliasTable_canAliasLimit (s
, sRef_getConjB (sr
), lim
);
416 res
= sRefSet_unionFree (a
, b
);
420 res
= aliasTable_canAliasAux (s
, sr
, lim
+ 1);
426 static /*@only@*/ sRefSet
427 aliasTable_canAliasAux (aliasTable s
, sRef sr
, int lim
)
429 static bool hadWarning
= FALSE
;
430 llassert (!sRef_isConj (sr
));
433 if (aliasTable_isUndefined (s
) || lim
>= ALIASSEARCHLIMIT
)
435 if (lim
>= ALIASSEARCHLIMIT
&& !hadWarning
)
438 (message ("Alias search limit exceeded, checking %q. "
439 "This either means there is a variable with at least "
440 "%d indirections, or there is a bug in Splint.",
447 return sRefSet_undefined
;
451 int ind
= aliasTable_lookupRefs (s
, sr
);
453 if (sRef_isPointer (sr
) || sRef_isAddress (sr
) || sRef_isField (sr
)
454 || sRef_isArrayFetch (sr
))
456 sRef base
= sRef_getBase (sr
);
457 sRefSet tmp
= aliasTable_canAliasLimit (s
, base
, lim
);
460 if (sRef_isPointer (sr
))
462 ret
= sRefSet_addIndirection (tmp
);
464 else if (sRef_isAddress (sr
))
466 ret
= sRefSet_removeIndirection (tmp
);
468 else if (sRef_isField (sr
))
470 ret
= sRefSet_accessField (tmp
, sRef_getField (sr
));
472 else if (sRef_isArrayFetch (sr
))
474 if (sRef_isIndexKnown (sr
))
476 ret
= sRefSet_fetchKnown (tmp
, sRef_getIndex (sr
));
480 ret
= sRefSet_fetchUnknown (tmp
);
486 ret
= sRefSet_undefined
;
489 if (ind
!= ATINVALID
)
491 ret
= sRefSet_union (ret
, s
->values
[ind
]);
498 if (ind
== ATINVALID
) return sRefSet_undefined
;
500 return sRefSet_newCopy (s
->values
[ind
]);
504 aliasTable
aliasTable_copy (aliasTable s
)
506 if (aliasTable_isEmpty (s
))
508 return aliasTable_undefined
;
512 aliasTable t
= (aliasTable
) dmalloc (sizeof (*s
));
515 t
->nelements
= s
->nelements
;
517 t
->keys
= (sRef
*) dmalloc (sizeof (*s
->keys
) * s
->nelements
);
518 t
->values
= (sRefSet
*) dmalloc (sizeof (*s
->values
) * t
->nelements
);
520 for (i
= 0; i
< s
->nelements
; i
++)
522 t
->keys
[i
] = s
->keys
[i
];
523 t
->values
[i
] = sRefSet_newCopy (s
->values
[i
]);
531 aliasTable_levelPrune (aliasTable s
, int lexlevel
)
535 if (aliasTable_isEmpty (s
))
542 int backcount
= s
->nelements
- 1;
544 for (i
= 0; i
<= backcount
; i
++)
546 sRef key
= s
->keys
[i
];
548 if (sRef_lexLevel (key
) > lexlevel
)
551 for (j
= backcount
; j
> i
; j
--)
557 if (sRef_lexLevel (s
->keys
[j
]) <= lexlevel
)
559 s
->keys
[i
] = s
->keys
[j
];
560 s
->values
[i
] = s
->values
[j
];
561 sRefSet_levelPrune (s
->values
[i
], lexlevel
);
562 /*@innerbreak@*/ break;
570 sRefSet_levelPrune (s
->values
[i
], lexlevel
);
579 ** like level union, but know that t2 was executed after t1. So if
580 ** t1 has x -> { a, b } and t2 has x -> { a }, then result has x -> { a }.
582 ** NOTE: t2 is "only".
585 aliasTable
aliasTable_levelUnionSeq (/*@returned@*/ aliasTable t1
,
586 /*@only@*/ aliasTable t2
, int level
)
588 if (aliasTable_isUndefined (t2
))
593 if (aliasTable_isUndefined (t1
))
595 t1
= aliasTable_newEmpty ();
599 aliasTable_levelPrune (t1
, level
);
602 aliasTable_elements (t2
, key
, value
)
604 if (sRef_lexLevel (key
) <= level
)
606 int ind
= aliasTable_lookupRefs (t1
, key
);
608 sRefSet_levelPrune (value
, level
);
610 if (ind
== ATINVALID
)
612 /* okay, t2 is killed */
613 /*@-exposetrans@*/ /*@-dependenttrans@*/
614 t1
= aliasTable_addSet (t1
, key
, value
);
615 /*@=exposetrans@*/ /*@=dependenttrans@*/
619 sRefSet_free (t1
->values
[ind
]);
621 /*@-dependenttrans@*/ /* okay, t2 is killed */
622 t1
->values
[ind
] = value
;
623 /*@=dependenttrans@*/
628 /*@-exposetrans@*/ /*@-dependenttrans@*/
629 sRefSet_free (value
);
630 /*@=exposetrans@*/ /*@=dependenttrans@*/
633 } end_aliasTable_elements
;
643 aliasTable_levelUnion (/*@returned@*/ aliasTable t1
, aliasTable t2
, int level
)
645 if (aliasTable_isUndefined (t1
))
647 if (aliasTable_isUndefined (t2
))
653 t1
= aliasTable_newEmpty ();
658 aliasTable_levelPrune (t1
, level
);
661 aliasTable_elements (t2
, key
, cvalue
)
663 sRefSet value
= sRefSet_newCopy (cvalue
);
665 if (sRef_lexLevel (key
) <= level
)
667 sRefSet_levelPrune (value
, level
);
669 if (sRefSet_size (value
) > 0)
671 int ind
= aliasTable_lookupRefs (t1
, key
);
673 if (ind
== ATINVALID
)
675 t1
= aliasTable_addSet (t1
, key
, value
);
679 t1
->values
[ind
] = sRefSet_union (t1
->values
[ind
], value
);
680 sRefSet_free (value
);
685 sRefSet_free (value
);
690 sRefSet_free (value
);
692 } end_aliasTable_elements
;
697 aliasTable
aliasTable_levelUnionNew (aliasTable t1
, aliasTable t2
, int level
)
699 aliasTable ret
= aliasTable_levelUnion (aliasTable_copy (t1
), t2
, level
);
705 aliasTable_unparse (aliasTable s
)
707 cstring st
= cstring_undefined
;
709 if (aliasTable_isUndefined (s
)) return (cstring_makeLiteral ("<NULL>"));
711 aliasTable_elements (s
, key
, value
)
713 st
= message ("%q\t%q -> %q\n", st
, sRef_unparseFull (key
),
714 sRefSet_unparseFull (value
));
715 } end_aliasTable_elements
;
725 aliasTable_fixSrefs (aliasTable s
)
729 if (aliasTable_isUndefined (s
)) return;
731 for (i
= 0; i
< s
->nelements
; i
++)
733 sRef old
= s
->keys
[i
];
735 if (sRef_isLocalVar (old
))
737 s
->keys
[i
] = uentry_getSref (sRef_getUentry (old
));
740 sRefSet_fixSrefs (s
->values
[i
]);
745 aliasTable_free (/*@only@*/ aliasTable s
)
749 if (aliasTable_isUndefined (s
)) return;
751 for (i
= 0; i
< s
->nelements
; i
++)
753 sRefSet_free (s
->values
[i
]);
762 aliasTable_checkGlobs (aliasTable t
)
764 aliasTable_elements (t
, key
, value
)
766 sRef root
= sRef_getRootBase (key
);
768 if (sRef_isAliasCheckedGlobal (root
))
770 sRefSet_realElements (value
, sr
)
772 root
= sRef_getRootBase (sr
);
774 if (((sRef_isAliasCheckedGlobal (root
)
775 && !(sRef_similar (root
, key
)))
776 || sRef_isAnyParam (root
))
777 && !sRef_isExposed (root
))
779 if (sRef_isAliasCheckedGlobal (key
))
781 if (!(sRef_isShared (key
)
782 && sRef_isShared (root
)))
787 ("Function returns with %q variable %q aliasing %q %q",
788 cstring_makeLiteral (sRef_isRealGlobal (key
)
789 ? "global" : "file static"),
791 cstring_makeLiteral (sRef_isAnyParam (root
)
792 ? "parameter" : "global"),
799 } end_sRefSet_realElements
;
801 else if (sRef_isAnyParam (key
) || sRef_isAnyParam (root
))
803 sRefSet_realElements (value
, sr
)
805 root
= sRef_getRootBase (sr
);
807 if (sRef_isAliasCheckedGlobal (root
)
808 && !sRef_isExposed (root
)
809 && !sRef_isDead (key
)
810 && !sRef_isShared (root
))
814 message ("Function returns with parameter %q aliasing %q %q",
816 cstring_makeLiteral (sRef_isRealGlobal (root
)
817 ? "global" : "file static"),
821 } end_sRefSet_realElements
;
827 } end_aliasTable_elements
;
833 ** For debugging only
836 void aliasTable_checkValid (aliasTable t
)
838 aliasTable_elements (t
, key
, value
)
840 sRef_checkCompletelyReasonable (key
);
842 sRefSet_elements (value
, sr
)
844 sRef_checkCompletelyReasonable (sr
);
845 } end_sRefSet_elements
;
846 } end_aliasTable_elements
;