<br><br><div class="gmail_quote">2010/10/25 Marcin Świderski <span dir="ltr"><<a href="mailto:marcin.sfider@gmail.com">marcin.sfider@gmail.com</a>></span><br><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<div class="gmail_quote">2010/10/25 Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com" target="_blank">kremenek@apple.com</a>></span></div><div class="gmail_quote"><div><div></div><div class="h5"><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<div bgcolor="#FFFFFF"><div><div></div><div><div><span>On Oct 24, 2010, at 10:29 PM, Zhongxing Xu <<a href="mailto:xuzhongxing@gmail.com" target="_blank">xuzhongxing@gmail.com</a>> wrote:</span></div><div>
<br></div><div></div><blockquote type="cite"><div><br><br><div class="gmail_quote">On Mon, Oct 25, 2010 at 1:19 PM, Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com" target="_blank"></a><a href="mailto:kremenek@apple.com" target="_blank">kremenek@apple.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<div style="word-wrap: break-word;"><div><div></div><div><br><div><div>On Oct 24, 2010, at 9:52 PM, Zhongxing Xu wrote:</div><br><blockquote type="cite"><br><br><div class="gmail_quote">On Mon, Oct 25, 2010 at 12:24 PM, Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com" target="_blank"></a><a href="mailto:kremenek@apple.com" target="_blank">kremenek@apple.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<div bgcolor="#FFFFFF"><div><div></div><div><div><span>On Oct 24, 2010, at 7:57 PM, Zhongxing Xu <<a href="mailto:xuzhongxing@gmail.com" target="_blank"></a><a href="mailto:xuzhongxing@gmail.com" target="_blank">xuzhongxing@gmail.com</a>> wrote:</span><br>
</div><div>
<br></div><div></div><blockquote type="cite"><div><br><br><div class="gmail_quote">On Mon, Oct 25, 2010 at 2:13 AM, Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com" target="_blank"></a><a href="mailto:kremenek@apple.com" target="_blank"></a><a href="mailto:kremenek@apple.com" target="_blank">kremenek@apple.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<div bgcolor="#FFFFFF"><div><div></div><div><div><span>On Oct 22, 2010, at 10:41 PM, Zhongxing Xu <<a href="mailto:xuzhongxing@gmail.com" target="_blank"></a><a href="mailto:xuzhongxing@gmail.com" target="_blank"></a><a href="mailto:xuzhongxing@gmail.com" target="_blank">xuzhongxing@gmail.com</a>> wrote:</span></div>
<div>
<br></div><div></div><blockquote type="cite"><div><br><br><div class="gmail_quote">2010/10/23 Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com" target="_blank"></a><a href="mailto:kremenek@apple.com" target="_blank"></a><a href="mailto:kremenek@apple.com" target="_blank"></a><a href="mailto:kremenek@apple.com" target="_blank">kremenek@apple.com</a>></span><br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<div>On Oct 17, 2010, at 3:06 PM, Marcin Świderski wrote:<br>
<br>
</div><div>> Blocks structure that is constructed is fine, but I don't know what to use for terminator of block initiating the branch and for first element in block closing the branch (I didn't check this yet, but I think that it could be used during backward analysis). Could I use fake if/else statement for this? Similar solution is used to make every declaration into separate statement.<br>
<br>
</div>What we could do is generalize terminators in the same way we did with CFGElements. Right now terminators are Stmt*, but they could be something like CFGTerminator, which could discriminate between regular terminators and those used for blocks guarding destructor calls. The CFGTerminator for those blocks could essentially be the same Stmt* as the terminator guarding the block with the constructor, but with a special bit indicating it is for the matching destructor(s). The nice thing about this approach is that it naturally ties the two blocks together, they can share the same condition values, etc.</blockquote>
</div><br>We need a way to convey the branch information to the second logical op used as terminator. At first we bind logical op to a UndefinedVal which indicates which branch is taken. Then the logical op is bound to its real value. At the second terminator where the logical op appears, we still need the taken branch information to decide which branch to take.<br>
</div></blockquote><br></div></div><div>Indeed. After thinking about this some more, we can't just keep a reference the original block-level expression that represented the branch condition and hope that is enough. That expression's SVal should still be in the Environment (since it would still be live), and we could use it a second time when deciding the branch. That only works, however, if we only took a single branch (not both of them) and the SVal didn't reference any symbolic values (which depend on state). Thus recording the branch taken seems to be the most accurate and simplest approach.</div>
<div><br></div><div>We could possibly insert this information into the Environment (possibly using some bit mangling for the Stmt* key value), have the data value represent the branch taken, and then have the liveness of that entry be the same as the liveness of the original condition expression.</div>
<div><br></div><div>For example, in A || B, the expression 'A' is used to determine the first branch. For that, we have a block-level expression (a Stmt*) which serves as a condition for the terminator '||'. That value gets inserted into the Environment as part of regular evaluation, and stays live until after we are done with evaluating the '||' terminator (LiveVariables analysis does this for us). In addition, we could insert another entry whose key is similar to the one for the block-level expression but instead has a bit twiddled (e.g., we take the Stmt* for 'A', which represents the condition value used for the first branch, and then bit-mangle it). We could use that to record what branch we took, and keep that entry around as long as the original block-level expression (e.g., the Stmt* for 'A') would stay in the Environment. That value's lifetime would get extended by having a special CFGTerminator that referenced that block-level expression and represented the terminator for jumping to the block with the destructor calls. We then consult the branch value when choosing what block to jump to for the destructors.</div>
</div></blockquote><div><br></div><div>That means we need to modify the dataflow solver since the Terminator does not participate the dataflow computation for now, right? <br></div></div></div></blockquote></div></div></div>
</blockquote><div><br>Sorry, I didn't get this clear. I am concerning the liveness computation. We need to keep the bit-mangled Stmt* for 'A' alive until the second logical op as terminator. Since it is only referenced by this terminator, we need to modify the dataflow solver to consider terminators when doing the computation.</div>
</div></blockquote><br></div></div></div><div>Ah, I see. DataflowSolver already calls 'VisitTerminator', and LiveVariables.cpp already checks the terminator as part of the liveness computation. I don't think we'd really need to do much more other than educate LiveVariables.cpp about the new terminators. The DataflowSolver itself wouldn't need to be changed.</div>
</div></blockquote></div><br>I see. And we also need to insert the bit-mangled Stmt * into the CFGBlock, otherwise it won't appear in the LiveVariables. So we need to create a new kind of CFGElement, say, BranchMarker?<br>
</div></blockquote><br></div></div><div>I don't immediately see a need to do that. Since <span>LiveVariables is a reverse dataflow analysis, the bit-mangled Stmt* can get inserted (as "live") when we visit the terminator. It can then get removed when we visit the original Stmt* (which by definition dominates the point where we'd consult the bit-mangled Stmt*). I don't see a need to add a special BranchMarker. Is there a case that I'm missing?</span></div>
</div></blockquote><div><br></div></div></div><div>I'm currently getting to know the path-sensitive engine and don't yet understand why do we need to handle this in LiveVariables analysis. As I scanned through the code the symbol liveness is managed with the use of SymbolReaper which, I think, doesn't get in touch with any LiveVariables instance.</div>
</div></blockquote><div><br>SymbolReaper references LiveVariables through LocationContext.<br> </div><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<div class="gmail_quote">
<div><br></div><div>I see I did rush a little with CFGTerminator change (I wanted to close the destructors generation in CFG), but as I understand the bit marking terminator as being used for branching destructors calls will suffice.</div>
</div>
</blockquote></div><br>