Hi Ted,
<br> <br>I think statistical checker is some different from the checkers we have.
<br><br>IMO, when doing statistical check, the static analyzer should not work in the "whole-program-analysis" mode, but in the "textual" statistic mode.
<br><br>In this mode, we treat every top level functiondecl (also the inline function) has a body as a cell. Then we do symbolic execution in every cell to check CheckedReturn state for calls (i.e, a call to foo()), and textually count a function decl's (i.e, foo()) CheckedReturn state from all the occurrences (calls).
<br><br>So we need a new action to activate this "textual" mode, and in this mode the inline IPA should be deactivated (i think the function summary IPA also works). Then every cell will have only one LocationContext, right?
<br> <br>Here is a example to make it clearer.
<br> <br>int f1();
<br> <br>int main() {
<br> f2();
<br> f3();
<br>}
<br> <br>void f2() {
<br> f1();
<br>}
<br> <br>void f3() {
<br> f2();
<br> if (f1())
<br> return;
<br>}
<br> <br>There are two "textual" calls to f1(), the one in f3() is checked and the one in f2() is unchecked. But if we do the check in WPA Mode(IMO, as viewed from "execute"), there are 3 calls to f1(), one of them is checked and the other two are not.
<br> <br>We should do it in the "textual" way, right?<br><br>What you say about this?<br><br><div class="gmail_quote">2011/4/12 Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com">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;">Lei,<br>
<br>
Just to make this a little clearer, suppose we had:<br>
<br>
unsigned factorial(unsigned n) {<br>
if (n == 0)<br>
return 1;<br>
return n * factorial(n - 1);<br>
}<br>
<br>
Currently when we analyze this function, we create only one LocationContext. However, one way to do IPA is to due inlining of function calls. In this case, we might create a second LocationContext during the first recursive call to factorial. If we wanted to further inline, we might create a second LocationContext, etc., each one capturing the "context" of the recursive call and simulating an abstract stack frame (obviously bounding the amount of LocationContexts we create).<br>
<div><div></div><div class="h5"><br>
On Apr 11, 2011, at 10:53 AM, Ted Kremenek wrote:<br>
<br>
> I thought about this some more, and using the LocationContext might be a reasonable place to put checker-specific data that represents "global" information (i.e not specific to a GRState) but also limited in scope (i.e. the data is limited to the scope of analyzing a given *call* to a function). Once we support analysis inlining, it will be possible for multiple LocationContext objects to be around at the once for the same function. Are the statistics you are interested in specific to a given LocationContext?<br>
><br>
> On Apr 11, 2011, at 10:19 AM, Ted Kremenek <<a href="mailto:kremenek@apple.com">kremenek@apple.com</a>> wrote:<br>
><br>
>> Hi Lei,<br>
>><br>
>> LocationContext should not contain any checker-specific data. It is only intended to model context-sensitivity (i.e., it simulates an abstract stack frame, or "location" in an abstract call chain).<br>
>><br>
>> What are you trying to do?<br>
>><br>
>> Ted<br>
>><br>
>> On Apr 10, 2011, at 8:26 PM, ียภฺ wrote:<br>
>><br>
>>> Hi Clang,<br>
>>><br>
>>> This patch add a DenseMap to record the CheckedReturn count for a functiondecl(fielddecl, vardecl as function pointer) in LocationContext.<br>
>>><br>
>>> ImmutableMap seems not alright here, is DenseMap ok?<br>
>>><br>
>>> And how to make it checker-specific?<br>
>>><br>
>>> This patch is preparation for statistical UncheckedRenturn checker.<br>
>>> I'll appreciate it if there are any advice about this patch.<br>
>>><br>
>>> --<br>
>>> Best regards!<br>
>>><br>
>>> Lei Zhang<br>
>>> <CRResultMap.patch>_______________________________________________<br>
>>> cfe-commits mailing list<br>
>>> <a href="mailto:cfe-commits@cs.uiuc.edu">cfe-commits@cs.uiuc.edu</a><br>
>>> <a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits</a><br>
>><br>
>><br>
>> _______________________________________________<br>
>> cfe-commits mailing list<br>
>> <a href="mailto:cfe-commits@cs.uiuc.edu">cfe-commits@cs.uiuc.edu</a><br>
>> <a href="http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits</a><br>
<br>
</div></div></blockquote></div><br><br clear="all"><br>-- <br>Best regards!<br><br>Lei Zhang<br>