<div dir="ltr"><div dir="ltr">Hi!<div><br></div><div>This is a very interesting problem, and I'm excited to see that there is real desire for such a feature.<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 3 Oct 2019 at 06:15, Алексеев Кирилл via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</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><br></div><div><br></div><div><div><div>I need to find loop at first and then to find all definitions of variables in loop control expression, and definitions of some related variables used in rhs of previous definitions.<br></div><div><div>For example program: </div><div><br></div><div>foo2(int start, int end){</div><div> for (int i=start; i<end; i++){</div><div> …//memory copy loop</div><div> }</div><div>}</div><div><br></div><div>foo1(int b)</div><div> if(…){</div><div> c = 5;</div><div> }</div><div>else c = 10;</div><div> a = b + c;</div><div> foo2(a, b)</div><div>}</div><div><br></div><div>I need to find loop at first and then (backward) definitions:</div><div>a) start = foo2 param (a)</div><div>b) a = b + c</div><div>c) b = …</div><div>d1) c = 5</div><div>d2) c = 10</div><div><br></div><div> I.e. is it exist a pointer to previous node(s) of current node of ExplodedGraph?</div></div></div></div></blockquote><div><br></div><div>Sure, but mind that nodes in the ExplodedGraph may have several predecessors. After the analysis is concluded (and the entire graph is built), the analyzer will create linear bugpaths from the ExplodedGraph, which describe a specific path from the root to a bug node. At this stage, nodes in the bugpath only have a single predecessor (unless its the root), but the bugpath isn't available to the checkers, only visitors and BugReporter itself.</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><div><div><div>Also is it possible to find with Clang SA checkers' API input data that allow to reach some basic block? I want to find constraints on input data that allow to reach particular definitions of variables. Yes, it is over all paths, but not using simple meet operator.</div></div></div></div></blockquote><div><br></div><div>To me it seems like the algorithm known as "Reaching definitions" may be the answer to your problem. The drawback is that we have not implemented this algorithm for C++ (but its in the works! <a href="https://reviews.llvm.org/D64991">https://reviews.llvm.org/D64991</a>). Once it is complete however, it still won't be interprocedural, so arguing across function boundaries will require some trickery.</div><div><br></div><div>The class described in this patch will calculate reaching definitions to a variable within a function, and after some discussion on the mailing list we think that it would be possible to combine the information gathered by the analyzer (most importantly, the resolution of parameter passing) to make it semi-interprocedural.</div><div><br></div><div>The answer to your question is "no", but its not that far from being a part of the API.</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><div><div><div>So it seemed for me that ExplodedGraph is the best choice.</div></div></div></div></blockquote><div> <br></div><div>It is very difficult to argue across the entire ExplodedGraph. The thing that is most challanging to overcome is proving that one path of execution is related to another.</div><div><br></div><div>Suppose you have to analyze the following program:</div><div><font face="monospace"><br></font></div><div><font face="monospace">void f(int a, int b) {</font></div><div><font face="monospace"> if (coin())</font></div><div><font face="monospace"> blackmagic(&a, &b);</font></div><div><font face="monospace"> </font></div><div><font face="monospace"> for (int i = a; i < b; ++b) { ... }</font></div><div><font face="monospace">}</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">Suppose that the function blackmagic() halts symbolic execution somewhere due to the analyzer's budget depleting or containing code that the analyzer can't model (like inline assembly). There is no guarantee that if coin() returns true, symbolic execution would ever reach the loop, and even if it did, it might just be the case that we don't know the internals of blackmagic().</font></div><div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">That said, it would amazing if we had the infrastructure to traverse and argue about the entirety of the ExplodedGraph, but I fear its far in the distance for now.</font></div><div><br></div><div>I hope this helped, please follow up if you still have questions!</div><div><br></div><div>Cheers,</div><div>Husi</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><br></div><div></div><div><br></div>_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
<a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" rel="noreferrer" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br>
</blockquote></div></div>