<div>Hi Ted,<br><br>Thank you very much for your reply. It solved many problems that confusing me.<br><br>Sorry for the misuse of the APIs and data structures. My intention of last mail is to show what i am trying to do by code without changing the Engine and the checker visit mechanism.<br>
<br>If you don't mention "taint analysis" in your email, i didn't realize that yet. Yes, i think it's some sort of taint analysis.</div>
<div>IMO, some key points in this 'taint' analysis are:</div>
<blockquote dir="ltr" style="MARGIN-RIGHT: 0px">
<div>source: return values from all the CallExpr.</div>
<div>sanitizer: the condition in a BranchCondition.</div>
<div>sink: when we handle RemoveDeadSymbols?(according to your mail)</div></blockquote>
<div dir="ltr">And as you point, the 'taint' propagation ruls is the most important thing. So i think this analysis is more or less different from the traditional taint analysis.</div>
<div dir="ltr"> </div>
<div dir="ltr">More comments inline.</div>
<div> </div>
<div class="gmail_quote">2011/3/15 Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com" target="_blank">kremenek@apple.com</a>></span><br>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div>
<div>On Mar 9, 2011, at 10:28 PM, ียภฺ wrote:</div><br></div>
<blockquote type="cite"><span style="WORD-SPACING: 0px; FONT: medium Helvetica; TEXT-TRANSFORM: none; TEXT-INDENT: 0px; WHITE-SPACE: normal; LETTER-SPACING: normal; BORDER-COLLAPSE: separate">Hi clang,<br><br>
<div>Sorry for this late reply.<br><br>I reimplement UncheckedReturnChecker, here are some key points and some problems confusing me.<br></div></span></blockquote>
<div><br></div>
<div>Hi Lei,</div>
<div><br></div>
<div>Thanks for continuing to push forward on this. Comments inline.</div>
<div>
<div><br></div>
<blockquote type="cite"><span style="WORD-SPACING: 0px; FONT: medium Helvetica; TEXT-TRANSFORM: none; TEXT-INDENT: 0px; WHITE-SPACE: normal; LETTER-SPACING: normal; BORDER-COLLAPSE: separate">
<ol>
<li>Instead of the original syntactic approach, i track the symbolic values in BinaryOperator & UnaryOperator. It means every BinaryOperator & UnaryOperator will have a symbol to record the callexprs in subExpr. (So i create many Conjured Symbol to do this, is this all alright?)</li>
</ol></span></blockquote></div>
<div>I don't think this is quite the right approach, although your patch raises some interesting questions. In principal, you shouldn't need to create any new conjured symbols at all. Conjured symbols represent values to be tracked by the analyzer. Conceptually, your checker only tracks meta-data associated with symbols. However, what you are trying to do is a form of "taint" analysis, which may require introducing more symbols.</div>
</div></div></blockquote>
<div><br>If i should not create conjured symbols, which symbol should i use.<br> <br></div>
<div></div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div></div>
<div>A few specific comments:</div>
<div><br></div>
<div>
<div>
<div>+ // Once we encounter a call expr, set the initial state to Unchecked.</div></div>
<div>+ if (SymbolRef Sym = V.getAsSymbol()) {</div>
<div>+ llvm::DenseSet<StateRef> *CRStates = new llvm::DenseSet<StateRef>();</div>
<div>+ CheckedReturnSet CRSet = CheckedReturnSet(CE, *CRStates);</div>
<div>+ CRSet.addState(CheckedReturnState::getUnchecked(CE));</div>
<div>+ state = state->set<CheckedReturnSetState>(Sym, CRSet);</div>
<div>+ C.addTransition(state);</div>
<div>+ }</div>
<div><br></div>
<div>
<div>DenseMaps should never be used as data stored by a GRState. DenseMaps are not immutable, and your checker will now allocate a ton of memory and leak like crazy. For data to be tracked for a given GRState, you must use immutable data structures such as ImmutableMap. The reason is two fold:</div>
<div><br></div>
<div>1) ImmutableMaps can be reused in multiple instances of GRState, and we can compare (using pointer equality) if two ImmutableMaps are equivalent. This allows us to do state caching, and also merge paths when two ExplodedNodes have the same ProgramPoint and GRState.</div>
<div><br></div>
<div>2) All memory associated with the ImmutableMaps (particularly those managed by the GDM) are region allocated and destroyed. Such memory is allocated efficiently. Using DenseMaps for per-GRState involves malloc()'ing a bunch of memory that just gets leaked. That's really inefficient, and algorithmically not correct.</div>
</div></div></div></div></blockquote>
<div><br>Errr, sorry about that.<br> </div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div>
<div>
<div> </div></div></div></div></div></blockquote>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div>
<div>
<div></div>
<div>Instead, I'd expect to see something like:</div>
<div><br></div>
<div>if (SymbolRef sym = V.getAsSymbol()) {</div>
<div> state = state->add<CheckedReturnState>(sym, CheckedReturnState::getUnchecked(CE))</div>
<div> C.addTransition(state);</div>
<div>}</div>
<div><br></div>
<div>That's a lot less code and doesn't allocate a ton of (mutable) memory. Id then replace CheckedReturnState with some like the following:</div>
<div><br></div>
<div>enum CheckReturnStateKind { Unchecked, Checked };</div>
<div>
<div>typedef llvm::ImmutableMap<SymbolRef, CheckReturnStateKind > CheckedReturnState;</div>
<div>namespace clang { namespace ento {</div>
<div> template<><br> struct GRStateTrait<CheckReturnState > : public GRStatePartialTrait< CheckedReturnState > {<br> static void* GDMIndex() { static int index = 0; return &index; }<br> };</div>
<div>}}</div>
<div><br></div>
<div>That reduces about 60 lines of code to 8, and then allows you to use CheckedReturnState as I illustrated above. After reading through more of your code, I realize that this doesn't quite match up with your algorithm, so let's continue to discuss the algorithmic design and see how it matches up with the static analyzer APIs we have.</div>
<div><br></div>
<div>Now let's look at checkPostStmt(BinaryOperator*):</div>
<div><br></div>
<div>I think I see what you are trying to do. Essentially:</div>
<div><br></div>
<div>a) the checker tracks symbols returned from function calls</div>
<div><br></div>
<div>b) binary/unary operations can create new values that are *derived* from symbols we are tracking. When those new values are checked, we want to treat the original symbols as tracked, so we need a way to track that a value is derived from another.</div>
<div><br></div>
<div>c) What are the "checked" propagation rules? For example:</div>
<div><br></div>
<div> x = foo(); // new symbol</div>
<div> y = bar(); // new symbol</div>
<div> z = x + y; // new symbol, based on the symbolic values in 'x' and 'y'</div>
<div> if (z) ...</div>
<div><br></div>
<div>Algorithmically, at 'if (z)', should the values in 'x' and 'y' be considered checked? I'm not certain. I think it really depends on your analysis and the "taint" propagation rules.</div>
</div></div></div></div></div></blockquote>
<div><br>IMO, 'x' and 'y' should be considered checked. But there is no evidence, so i think the 'taint' propagation rules needs to much more study and test.<br> </div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div>
<div>
<div>
<div> </div></div></div></div></div></div></blockquote>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div>
<div>
<div>
<div></div>
<div>My gut feeling is that (b) should be managed by the analyzer engine, not a specific checker. The reason is that many checkers may wish to do taint analysis (a general term for these kinds of problems), and track how a symbolic value "morphs" into other values. (c) seems to be the purview of a specific checker.</div>
<div><br></div>
<div>So here is how I'd expect the checker to be written:</div>
<div><br></div>
<div>I) The core analysis engine provides a few key APIs for doing taint analysis that can be used by specific checkers. Specifically:</div>
<div><br></div>
<div>a) CheckerContext provides an API for a checker to indicate that it wants to start tracking the "taint" state of a given function return value. Operationally, this would do the following:</div>
<div><br></div>
<div>- If the return value is a symbol, the analysis engine adds that symbol to a list of symbols to be tracked for taint analysis.</div>
<div>- If the return value is not a symbol, the analysis engine conjures a new symbol, constraints that symbol to have the value returned from the function call, and then adds that symbol to a list of symbols to be tracked for taint analysis</div>
<div><br></div>
<div>b) When the analysis engine evaluates unary or binary operations (that can create new values derived from symbols), it checks if any of the operands are tainted symbols. If so, it does one of the following:</div>
<div><br></div>
<div>- If the new value for that expression is a symbol, the analysis engine records that that new symbol was "derived" via taint analysis from the tracked tainted symbol.</div>
<div>- If the new value for that expression is not a symbol, the analysis engine creates a new symbol, constrains that symbol to be equal to the value computed for that expression, and then uses that new symbol as the value of the expression. It then records that the new symbol was "derived" via taint analysis from the tracked tainted symbol."</div>
<div><br></div>
<div>We can have some variations here, but with this first cut essentially the checker would need no additional code to do the taint propagation. It would be done entirely by the analysis engine. This causes your checkPostStmt(BinaryOperator*) and checkPostStmt(UnaryOperator*) to completely vanish.</div>
<div><br></div>
<div>c) The analysis engine provides APIs to query if a symbol is tainted, and walk the tree of symbols from which it inherits its "tainted" classification.</div></div></div></div></div></div></blockquote>
<div> </div>
<div>How the Engine works depends on how we define the propagation rules. If we wanna make checkPostStmt(BinaryOperator *) and checkPostStmt(UnaryOperator *) to completely vanish, we must implement those rules in the engine. But we may have different propagation rules, like traditional one and what we have in UncheckedReturnChecker. Should all this rules work in the engine? Or maybe we need have some callback for propagation?</div>
<div> </div>
<div></div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div>
<div>
<div>
<div> </div></div></div></div></div></div></blockquote>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div>
<div>
<div>
<div></div>
<div>II) Using the APIs above, the checker would consist of two parts:</div>
<div><br></div>
<div>- Use API (a) in checkPostStmt(CallExpr). The checker would get the symbol returned by the API, and set it to the "Unchecked" state (per my example code above).</div>
<div>- Use API (c) in checkBranchCondition(). If the condition evaluates to a tainted symbol, we can explore the tree of symbols from which it derives it taint status and mark all symbols in that tree as being "checked".</div>
<div><br></div>
<div>The nice thing about this approach is that your checker is just in the business of tracking basic typestate, and (ideally) does minimal work to propagate the taint propagation (which can really only be done well in the analysis engine itself).</div>
</div></div></div></div></div></blockquote>
<div> </div>
<div>Yes, i think this is the right apprach.</div>
<div>Thank you very much for pointing this. I knew something wrong with my patch, but i couldn't tell it. So i didn't go any further, and wrote last mail for help.</div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div>
<blockquote type="cite">
<ol start="2">
<li>I create a global DenseMap<const CallExpr*, CheckedReturnState*> to store whether a callexpr is checked or not.</li></ol></blockquote></div>
<div>This probably isn't the right approach, because we really want to shy away from global state. It also makes a bunch of assumptions that might not be true. For example, it assumes that functions are analyzed independently and that we do no inter-procedural analysis. While that's what we mostly do right now, that isn't an invariant.</div>
<div><br></div>
<div>For example, consider the case where we do basic inter-procedural analysis where we "inline" function calls. That is, when we see a function call, we continuing creating the ExplodedGraph by tracing into the called function, and then when we return from that function we continue analyzing the original function. We then have one analysis pass, and the "global" state is associated with analyzing all of those functions. What happens if the called function is the same function we are already analyzing? E.g., we are analyzing foo(), and foo() calls itself. This will cause the counts to be all messed up, as they will conflate two calls. Is this what we want? Maybe, but it should be a deliberate decision, not an accident. Further, Checker objects now exist for the entirety of </div>
</div></div></blockquote>
<div> </div>
<div>Yes, you are right. I forget about this.</div>
<div> </div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div>analyzing ALL functions in a translation unit. This means that they are reused by multiple GRExprEngine instances. This means that such global state really is a problem, as it is shared between multiple analysis runs.</div>
</div></div></blockquote>
<div> </div>
<div>Errr, I didn't make this clear. IMO, this global DenseMap<const CallExpr*, CheckedReturnState*> is used by the whole translation unit. All the CheckedReturnStates in different GRExprEngine instances are record here, and do the statistica count after all the function handled.</div>
<div>However, using a global state like this is indeed wierd. And i will move on as you suggested.</div>
<div> </div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div><br></div>
<div>Instead, I suggest we decompose things as follows:</div>
<div><br></div>
<div>- Provide a way to associate checker-specific state with a LocationContext. A LocationContext can encapsulate the current "stack frame", and thus provides the "local" but "global" analysis state you are looking for.</div>
<div>- Using the "local" state I suggested, Incrementally build up the statistical counting as needed. We only need to update the counts in two places:</div>
<div><br></div>
<div>a) in checkBranchCondition(), when we transition a tracked symbol to the "checked" state, we can increment the checked count for that symbol.</div>
<div>b) when we handle RemoveDeadSymbols and a symbol is in the "unchecked" state, we increment the unchecked count for that symbol.</div>
<div><br></div>
<div>We keep statistical counts for each LocationContext (or rather, StackFrameContext), and then do the post-analysis based on that.</div></div></div></blockquote>
<div> </div>
<div>OK, this souds much better than what i did, and i need to read more code about LocationContext.</div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div>
<blockquote type="cite">
<ol start="3">
<li>This patch didn't consider the deal with the escaped symbol.</li></ol></blockquote>
<div><br></div></div>
<div>We can handle this in a variety of ways. We can add a new checker callback when symbols escape, and then have the Checker respond accordingly.</div>
<div><br>
<blockquote type="cite">
<ol start="4">
<li>The bugreport is very simple now...<br></li></ol></blockquote></div>
<div>That's fine. That's polish.</div>
<div><br>
<blockquote type="cite">
<ol start="5">
<li>This checker seems much slower than other...</li></ol></blockquote></div>
<div>There are a couple reasons for this. First, you are malloc'ing a ton of objects. malloc() is really slow, and your checker now leaks like crazy. All checker state should be allocated using the BumpPtrAllocator associated with GRStateManager. Second, a semantic approach is inherently slower than a syntactic one, but far more general and thorough. Third, because of the way you are tracking checker state, you have forced the static analyzer to be worst-case exponential. There will be no state caching as there is no way to merge isomorphic states because of the freshly created DenseMaps.</div>
</div></div></blockquote>
<div> </div>
<div>Thank you for pointing these out.</div>
<div> </div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div>
<div>
<div><br></div>
<blockquote type="cite">After all, there are many work should be done. I write this mail to ask whether this direction is right or not.</blockquote><br></div></div>
<div>After writing my comments above, I realized this really is a big project, not just a new checker. To do it semantically, we need a bunch of new infrastructure that currently doesn't exist. I see two options:</div>
<div><br></div>
<div>a) We forge ahead on such infrastructure (for taint propagation in the analysis engine). I can work with you to gradually make this happen, but this will take time. Once that's in place, we use that new infrastructure to implement your checker using that infrastructure (or we do this in tandem).</div>
<div>b) We go (for now) with your original "syntactic" version of the checker, and fix the issues that would be common to both the semantic and syntactic versions.</div>
<div><br></div>
<div>I think we should do both. The good thing about (b) is that it establishes a baseline. That baseline allows us to write tests, etc. It also allows you to not commit staying involved beyond where your interest or time peaks out. With (a), we can keep (b) around as an entirely separate implementation, and gradually make progress on (a) until we feel it is good enough to replace (b).</div>
<div><br></div>
<div>I know this is a lot of data, and I feel I probably explained a few things very poorly. At a high level, I think to do your checker "right" we need to add a bunch of infrastructure to the core analysis engine that doesn't exist. Once that infrastructure exists, however, I think the checker itself should be fairly simple.</div>
<div><br></div>
<div>Thoughts? Comments? How would you like to proceed?</div></div></blockquote>
<div> </div>
<div>I think option(a) is what i want. But to implement it, i need to study the the taint analysis theory and find out the propagation rules we should establish for this checker. And i can't guarantee the time spent on it.</div>
<div>So as you said, we go with (b) first, and then gradually make (a) happen.</div>
<div> </div>
<div>I will go back the with the original "syntactic" version of the checker, and see what i can do about (a) meanwhile.</div>
<div> </div>
<div>What you say?</div>
<div> </div>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
<div style="WORD-WRAP: break-word">
<div><br></div>
<div>Cheers,</div>
<div>Ted</div></div></blockquote></div><br><br clear="all"><br>-- <br>Best regards!<br><br>Lei Zhang<br>