<div dir="ltr"><div dir="ltr"></div>I enhanced the sketch greatly.<div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 11 Jun 2019 at 04:19, Artem Dergachev <<a href="mailto:noqnoqneo@gmail.com">noqnoqneo@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF">
Hmm, what do you mean by this line?:<br>
<br>
trackExpressionValue(N, RHS of assignment, Report)<br>
<br>
Like, how does the existing visitor infrastructure behave when the
statement is, by construction, never appears in the bug path? It
doesn't even have a value to track, as it never appeared in the
Environment.<br></div></blockquote><div><br></div><div>Well the thinking was that there's no need for that as TrackControlDependecy only needs a CFG to track conditions. Now, obviously, the actual tracking of the right hand side of the assignment wouldn't be possible, but that could be a plus: I think tracking too much hypothetical "this could have prevented the bug, but ultimately did not" events could litter the bug report.</div><div><br></div><div>I changed this in the sketch.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div bgcolor="#FFFFFF">
P.S. I just realized that this discussion would probably be messy to
read later through archives, as old revisions of the google doc are
no longer available.<br></div></blockquote><div><br></div><div>Good point. Here's a copy-paste from the document:<br><br><span id="gmail-docs-internal-guid-77b057a5-7fff-45fb-dd99-3a51871294fc"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:Arial;color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">The following slicing algorithm, which is heavily tailored for the Clang Static Analyzer, somewhat redefines the goal of slicing: traditionally, we’d gather a set of relevant variables, which would initially be the variables in the slicing criterion, and expand it if we find a variable relevant to any variable within the set. Along this, we’d also calculate a set of relevant statements, which is a subset of the program, either executable on it’s own or not.</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><b style="font-weight:normal" id="gmail-docs-internal-guid-ed1ab866-7fff-93b2-8ac7-cfcb0bcd2057"><br></b></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:Arial;color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">My approach is vastly different: the reason behind this is the function called trackExpressionValue. In a nutshell, trackExpressionValue tracks a variable, and adds notes at where the tracked variable was written, alongside the path that leads there, essentially gathering the set of relevant statements. Teaching it to discover variables immediate relevant to the tracked variable, we could (in theory) calculate the set of relevant variables transitively: if X is tracked, and A would be added to the set because of X, and B would be added because of A, tracking X would trigger tracking A, and that would trigger tracking B.</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><b style="font-weight:normal"><br></b></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:Arial;color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">Our starting point (slicing criterion) is the ExplodedNode and CFGBlock where report originates from, and the variable that was initially tracked.</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">function insertIfLastWrite(CFG, SetOfLastWrites : set of CFGBlocks,</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> NewBlock : CFGBlock)</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> for each W block in SetOfLastWrites do</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> if NewBlock post dominates W then</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> SetOfLastWrites -= W</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> SetOfLastWrites += NewBlock </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> else if W post dominates B then</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> break</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> fi</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> od</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> if no elements post dominate B or vise versa then</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> SetOfLastWrites += NewBlock</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> fi</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><b style="font-weight:normal"><br></b></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">// Traverses N’s CFG to discover branches that are not a part of the</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">// bug path. Returns true if it discovers a write to X that is</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">// inevitable.</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">function conditionTracker(N : ExplodedNode, X : variable,</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> OriginB : CFGBlock, Report : BugReport)</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> SetOfLastWrites = {} : set of CFGBlocks</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><b style="font-weight:normal"><br></b></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> for all B blocks in N->getCFG() in order do</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> if there is no path from B to OriginB then</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> continue</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> fi</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><b style="font-weight:normal"><br></b></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> for all E elements in B in order do</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> if E writes X then</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> insertIfLastWrite(N->getCFG(), SetOfLastWrites, B)</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> continue</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> fi</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><b style="font-weight:normal"><br></b></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> if E is a function call to F and the analyzer inlined F then</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> ParamSet := set of F's parameters to which</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> X is passed to as a non-const reference</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> NC := N's predecessor that is F's CallEnter</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> </span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> for all NewX variables in ParamSet do</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> if conditionTracker(NC, NewX, F’s exit block, Report) then</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> insertIfLastWrite(N->getCFG(), SetOfLastWrites, B)</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> fi</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> od</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> // X is global/static, or a field and F is a method, etc...</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> if F would have access to X regardless then</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> if conditionTracker(NC, NewX, F’s exit block, Report) then</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> insertIfLastWrite(N->getCFG(), SetOfLastWrites, B)</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> fi</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> fi</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> continue</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> fi</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><b style="font-weight:normal"><br></b></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> od</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> od</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><b style="font-weight:normal"><br></b></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> for all W blocks in SetOfLastWrites do</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> if W is not a part of the bug path then</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> track control dependencies of W</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> fi</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> // Otherwise, let regular visitors handle it.</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> od</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><b style="font-weight:normal"><br></b></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> if any of the blocks in SetOfLastWrites is in the bug path</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> return true</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> fi</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:"Courier New";color:rgb(34,34,34);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap"> return false</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><br class="gmail-Apple-interchange-newline"></p></span></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div bgcolor="#FFFFFF">
<div class="gmail-m_7315061547291713812moz-cite-prefix">On 6/10/19 6:46 PM, Kristóf Umann
wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">I rewrote my sketch algorithm that showcases how I
imagine this to work.
<div><br>
</div>
<div><a href="https://docs.google.com/document/d/1Lx867o3meyQsj0WKOSWMdosSBdw2MUq1aIxyPJM6iLU/edit" target="_blank">https://docs.google.com/document/d/1Lx867o3meyQsj0WKOSWMdosSBdw2MUq1aIxyPJM6iLU/edit</a><br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Mon, 10 Jun 2019 at 20:03,
Kristóf Umann <<a href="mailto:dkszelethus@gmail.com" target="_blank">dkszelethus@gmail.com</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div dir="ltr">
<div dir="ltr"><br>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Mon, 10 Jun 2019 at
05:03, Artem Dergachev <<a href="mailto:noqnoqneo@gmail.com" target="_blank">noqnoqneo@gmail.com</a>>
wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF"> The problem we're solving is
*entirely* about inter-procedural analysis. Like, as
long as there are no inlined calls on the path (and
therefore no pruning is being done), then there's no
problem at all: the user can easily see that the value
is untouched by direct observation.<br>
</div>
</blockquote>
<div><br>
</div>
<div>I have explained myself poorly. I intend to implement
an <i>intraprocedural</i> slicing, but that would work
<i>interprocedurally</i> by resolving function calls
with the help of the analyzer. This is important,
because for the by-the-book interprocedural slicing
you'd need a system dependence graph. Now, if a function
isn't inlined, we need to do this on our own. I see a
couple unknowns here (how deep do we explore such
functions? how to we resolve non-trivial parameter
passing? are we sure that tracking expressions here is
actually meaningful?) but I think tackling simple cases
is achievable.</div>
<div> </div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF"> In this sense i find the lack of
note in example 2 completely non-problematic (as long
as control dependency tracking lands). It's not a
problem that the user isn't told that bar() could have
initialized 'x', because the user already knows that
bar() is not even called in the first place.<br>
</div>
</blockquote>
<div><br>
</div>
<div>Would you agree that tracking flag however would be
good?</div>
<div> </div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF"> However, there may be a
combination of category 1 and category 2 that is much
more interesting: what if main() unconditionally calls
foo() that conditionally calls bar() that
unconditionally initializes the value? Eg.:<br>
<br>
void bar(int *x) {<br>
*x = 1; // the interesting event that doesn't
happen<br>
}<br>
<br>
void foo(int *x) {<br>
if (rand()) // control dependency of the
interesting event<br>
bar(x);<br>
}<br>
<br>
int main() {<br>
int x;<br>
foo(&x);<br>
use(x); // use of uninitialized value<br>
}<br>
<br>
In this case it is essential to highlight the path
within foo() so that to explain how it fails to call
bar().</div>
</blockquote>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF">
<div class="gmail-m_7315061547291713812gmail-m_7630018529613555819m_3899269156412793041gmail-m_-8359532103913902229moz-cite-prefix">On
09.06.2019 17:50, Kristóf Umann wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">I gave this some thought, and
realized that we could divide the
"should-not-have-happened" cases into 2
categories:<br>
<br>
<div>1. The unexplored block is within a function
that the analyzer visited.</div>
<div>2. The unexplored block lies within a
function that the analyzer didn't even visit.</div>
<div><br>
</div>
<div>For example:<br>
<br>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">01 int flag;</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">02 bool coin();</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">03 </span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">04 void foo() {</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">05 flag = coin();</span><span style="color:rgb(0,0,0);font-family:"Courier New";font-size:12px;white-space:pre-wrap"> // no note, but there should be one</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">06 }</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">07</span></p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">08 void bar(int &i) {</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">09 if (flag) // assumed false</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">10 i = new int;</span></p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">11 }</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">12 </span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">13 int main() {</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">14 int *x = 0; // x initialized to 0</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">15 flag = 1;</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">16 foo();</span><span style="color:rgb(0,0,0);font-family:"Courier New";font-size:12px;white-space:pre-wrap"> // no note, but there should be one</span></p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">17 bar(x);</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">18 foo(); // no note, but there should be one</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">19 </span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">20 if (flag) // assumed true</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">21 *x = 5; // warn</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">22 }</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><br>
</p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt">Observe
the subtle difference that on line 17,
function bar is called, and the first branch
lies in that function. This is definitely a
"category 1" case, since the analyzer inlined
and visited <font face="courier new,
monospace">bar()</font>, but again, failed
the realize the importance of flag due to not
visiting line 10, and makes no mention of line
16 in the bugreport.</p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">
01 int flag;</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">02 bool coin();</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">03 </span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">04 void foo() {</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">05 flag = coin();</span><span style="color:rgb(0,0,0);font-family:"Courier New";font-size:12px;white-space:pre-wrap"> // no note, but there should be one</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">06 }</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">07</span></p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">08 void bar(int &i) {</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">09 i = new int;</span></p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">10 }</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">11 </span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">12 int main() {</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">13 int *x = 0; // x initialized to 0</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">14 flag = 1;</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">15 foo();</span><span style="color:rgb(0,0,0);font-family:"Courier New";font-size:12px;white-space:pre-wrap"> // no note, but there should be one</span></p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><font face="Courier New" color="#000000"><span style="font-size:12px;white-space:pre-wrap">16 if (flag) // assumed false</span></font></p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">17 bar(x);</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">18 foo(); // no note, but there should be one</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">19 </span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">20 if (flag) // assumed true</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">21 *x = 5; // warn</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">22 }</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><br>
</p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt">In
this example, the if statement stays, but the
assignment to x is now found in bar(). In this
case, the analyzer didn't explore <font face="courier new, monospace">bar(),</font>
so it's a "category 2" case.</p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><br>
</p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt">Now,
the reason why these categories are important
is that if the analyzer actually explored a
function, it solves the problem of parameters:
for the example shown for "category 1", we can
simply ask the analyzer whether <font face="courier new, monospace">x</font> in
function <font face="courier new, monospace">main()</font>
is the same as <font face="courier new,
monospace">i</font> in function <font face="courier new, monospace">bar()</font>.
This is, as stated in my previous letter, far
more difficult for "category 2" cases.</p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><br>
</p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt">I
think when I'm finished with the
"must-have-happened" cases, I could start
enhancing NoStoreFuncVisitor to gather
conditions possibly worth tracking for
"category 1" cases, see whether an
intraprocedural slicing algorithm makes sense,
could worry about resolving parameters for the
other case one when I get there.</p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><br>
</p>
<p style="line-height:1.38;margin-top:0pt;margin-bottom:0pt">Any
thoughts on this approach? :)</p>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Sat, 8 Jun
2019 at 01:59, Kristóf Umann <<a href="mailto:dkszelethus@gmail.com" target="_blank">dkszelethus@gmail.com</a>>
wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div dir="ltr">Hi!<br>
<br>
I'm currently working on a GSoC project that
aims to improve the description we provide for
bug reports the Static Analyzer emits.<br>
<br>
<div>We divided the problem (that the
bugreports didn't explain how the bug came
about very well) into two parts:</div>
<div><br>
</div>
<div>1. The information is available in the
bug path (basically parts of the code the
analyzer actually explored on that
particular path of execution). We refer to
these as the "must-have-happened" case.</div>
<div>2. The information isn't available,
possibly not even in the ExplodedGraph
(parts of the program the analyzer explored
on all paths of execution). We call this the
"should-not-have-happened" case.</div>
<div><br>
</div>
<div><span id="gmail-m_7315061547291713812gmail-m_7630018529613555819m_3899269156412793041gmail-m_-8359532103913902229gmail-m_-840552459534237689gmail-docs-internal-guid-832b5cb3-7fff-3777-21ce-4e1d0c7bc76e">
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">01 int flag;</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">02 bool coin();</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">03 </span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">04 void foo() {</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">05 flag = coin();</span><span style="color:rgb(0,0,0);font-family:"Courier New";font-size:12px;white-space:pre-wrap"> // no note, but there should be one</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">06 }</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">07 </span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">08 int main() {</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">09 int *x = 0; // x initialized to 0</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">10 flag = 1;</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">11 foo();</span><span style="color:rgb(0,0,0);font-family:"Courier New";font-size:12px;white-space:pre-wrap"> // no note, but there should be one</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">12 if (flag) // assumed false</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">13 x = new int;</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">14 foo(); // no note, but there should be one</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">15 </span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">16 if (flag) // assumed true</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">17 *x = 5; // warn</span></p>
<p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:9pt;font-family:"Courier New";color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">18 }</span></p>
</span><br class="gmail-m_7315061547291713812gmail-m_7630018529613555819m_3899269156412793041gmail-m_-8359532103913902229gmail-m_-840552459534237689gmail-Apple-interchange-newline">
</div>
<div>The first branch is a good example for
the "should-not-have-happened" case: the bug
path doesn't contain line 13, so we don't
really know whether the condition on line 12
is a big deal, which in this case it is
(unlike if it only guarded a print of some
sort)</div>
<div><br>
</div>
<div>The second branch is a good example for
the "must-have-happened" case: we know that
the condition on line 16 is very important.</div>
<div><br>
</div>
<div>I like to think that I made a very decent
progress on the first part, as it's
objectively a lot simpler. A great addition
to the analyzer is that it now understands
(at least, when my patches land) control
dependencies in the CFG. With that, we can
figure out that flag's value on line 16 is
crucial, so we track it, resulting in notes
being added on line 14, and on line 5,
explaining that flag's value changed.</div>
<div><br>
</div>
<div>However, we are very unsure about how to
tackle the second part on the project. I
gave this a lot of thought, we had a couple
meetings in private, and I'd like to share
where I am with this.</div>
<div><br>
</div>
<div>My project proposed to implement a static
backward program slicing algorithm which
would definitely be amazing, but seems to be
an unrealistic approach. Basically, any
slicing algorithm that is interprocedural
would require a system dependence graph,
something we just simply don't have, not
even for LLVM.</div>
<div><br>
</div>
<div>Whenever pointer semantics are in the
picture, we have a really hard time: it's
something that is super difficult to reason
about without symbolic execution, and it
would probably be a good idea not to tackle
such cases until we come up with something
clever (maybe the pset calculation Gábor
Horváth is working on?). We should, however,
being able to handle reference parameters.</div>
<div><br>
</div>
<div>So then, what's the goal exactly?</div>
<div><br>
</div>
<div>We'd like to teach the analyzer that some
code blocks (even in other functions) could
have written the variable that is
responsible for the bug (x, in the included
example), and is very important to the bug
report. We could use this information to
track variables similarly to the
"must-have-happened" case: track conditions
that prevented the write from happening.</div>
<div><br>
</div>
<div>To the specifics. I think it's reasonable
to implement an <i>intraprocedural</i> slicing
algorithm. For the included example, I think
we should be able to discover the potential
write to x on line 9. We don't need anything
we already don't have to achieve this.</div>
<div><br>
</div>
<div>Reasoning across function boundaries
could be achieved by inlining functions (as
I understand it, simply insert the
function's CFGBlocks), but there are big
unknowns in this.</div>
<div><br>
</div>
<div>So my question is, do you think such
inlining is possible? If not, should I just
create a primitive variable-to-parameter
mapping? Is there something else on the
table?</div>
<div><br>
</div>
<div>Cheers!<br>
Kristóf Umann</div>
</div>
</blockquote>
</div>
</blockquote>
<br>
</div>
</blockquote>
</div>
</div>
</blockquote>
</div>
</blockquote>
<br>
</div>
</blockquote></div></div></div>