<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div>On Aug 9, 2010, at 7:17 PM, Zhongxing Xu wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><span class="Apple-style-span" style="border-collapse: separate; font-family: Helvetica; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; font-size: medium; ">I'm inclined to Jordy's original proposal that Checkers should be able<br>to control some symbols that only they know what the symbol means,<br>when the symbol dies.<br></span></blockquote><div><br></div><div>My point was that the checker shouldn't have to do anything special to extend the lifetime of a symbol. For symbols that annotate MemRegions, the lifetime of the symbol is inherently bound to the lifetime of the MemRegion. It seems far more natural to me, more efficient, and far less error prone to have SymbolManager::isLive() understand that the lifetime of one symbol is tied to another (declaratively) then having the checker doing something ad hoc on the side.</div><br><blockquote type="cite"><span class="Apple-style-span" style="border-collapse: separate; font-family: Helvetica; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; font-size: medium; "><br>The benefit is that symbols still remains what it is: a representation<br>of a value generated somewhere, and immutable. The checker could<br>generate a symbol to represent what it thinks representing the length<br>of the string, and next time when it change its mind, it can generate<br>a new symbol, and mark the old one dead. This seems very natural to<br>me. And it won't pollute the state with unnecessary symbols, because<br>it knows exactly when the symbol is live and dead.<br><br>On Tue, Aug 10, 2010 at 1:15 AM, Ted Kremenek <<a href="mailto:kremenek@apple.com">kremenek@apple.com</a>> wrote:<br><blockquote type="cite">Hi Jordy,<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">I have mixed feelings about adding this, and I think this needs strong justification. Why is it needed? What symbols do we need to keep around that aren't related to live regions, or the values bound to live regions? Right now symbols can indicate that they are derived from other symbols (or are related to regions), and their liveness is extended if they thing they derive from is also live. If a symbol is no longer live, why do we need to continue tracking state?<br></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">My concern about adding this is that it artificially will extend the lifetime of symbols, causing the GRState to accumulate extra state that defeats state caching. The current set of checkers already do a bad job of removing stale data from the GDM for dead symbols.<br></blockquote><br>Why? Checkers get informed by callback EvalDeadSymbols().</span></blockquote><br></div><div>That requires Checkers being good citizens and implement that callback. The only Checkers that should need to implement that callback are ones that do something special (e.g., leak detection checkers) when a symbol is no longer live. The more we can move to a place where the management of symbols is more declarative than imperative then the performance problems involved with artificially keeping track of a symbol longer than necessary just get defined away.</div></body></html>