<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">
<div>Hi Jordan,</div>
<div><br>
</div>
<div>Thanks for your answer. My comments below.</div>
<div><br>
</div>
<div>-- Mathieu</div>
<div><br>
</div>
<div>On May 7, 2013, at 6:52 PM, Jordan Rose <<a href="mailto:jordan_rose@apple.com">jordan_rose@apple.com</a>> wrote:</div>
<div><br class="Apple-interchange-newline">
<blockquote type="cite">
<div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">
<div>Hi, Mathieu...sorry for the delay. There's no reason why a new checker wouldn't be able to check new kinds of annotations, but the annotations it supports today are the same attributes provided by the Clang compiler. Now, we can always add attributes to
the compiler, but that's not something we usually want to do lightly.</div>
</div>
</blockquote>
Excellent. Sure!</div>
<div><br>
<blockquote type="cite">
<div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">
<div>Anna, Ted, and I have kicked around the idea of a more generic 'analyzer_annotate' attribute, which could make one-off analyzer language extensions cheaper, but we didn't quite finish designing it. Does this sound like the sort of thing you're asking about?
This would require modifying Clang's attribute parser to support this generic attribute and provide convenient access to its possible fields for any checkers.</div>
</div>
</blockquote>
<div>Yes this is totally what I am interested in.</div>
<div><br>
</div>
<div>Ideally (some of) these custom attributes should be attachable to types so that we can annotate structures in depth and share annotations between function declarations.</div>
<div><br>
</div>
<div>See example below.</div>
<div><br>
</div>
<blockquote type="cite">
<div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">
<div>(Meanwhile, we've hacked some things together using the existing string-only 'annotate' attribute; see IvarInvalidationChecker. You could use this to prototype your checker if you didn't want to work on the general attribute problem just yet.)</div>
<div><br>
</div>
<div>In this particular case, something else we've thought of is an attribute that stipulates that a function return value is always non-null, and another requiring that the result is checked. These also haven't been fully designed yet (are they inherited?
do they piggyback on existing attributes like 'nonnull', or do they get their own syntax?).</div>
</div>
</blockquote>
<div><br>
</div>
<div>
<div>As far as semantics is concerned, a solution that comes to my mind is to hack the usual 4-value lattice with a 5th "magic" value duplicating the "absurd" state. This 5-th value would propagate but otherwise would not be produced by unification.</div>
<div><br>
</div>
<div> nullable (check required)</div>
<div> / \</div>
<div> / \</div>
<div> null nonnull </div>
<div> \ / </div>
<div> \ / </div>
<div> absurd (unreachable)</div>
<div> magic (don't care) <-- actually the default in the absence of annotation</div>
<div><br>
</div>
<div>// merging values from possible paths</div>
<div>union(null, nonnull) = nullable // one of the path explicitly null-ed the value, we can't feed a function requiring a nonnull value anymore </div>
<div>union(magic, null) = null // idem</div>
<div>
<div>
<div>union(magic, nonnull) = nonnull // ignore the magic value and pretend we know it is nonnull (strange but I could not find any problematic example)</div>
<div></div>
</div>
<div><br>
</div>
<div>// unifying values</div>
<div>intersection(null, nonnull) = absurd // cut the path</div>
<div>intersection(magic, nonnull) = magic // continue to ignore this runtime value</div>
</div>
<div></div>
</div>
<div><br>
</div>
<div><br>
</div>
<div>Here is one motivating example using this vocabulary as type annotations.</div>
<div>
<div><font face="Courier New"><br>
</font></div>
<div><font face="Courier New">struct list;</font></div>
<div><font face="Courier New">typedef struct list __nullable__ list_t; // activate null-value checking</font></div>
<div><font face="Courier New"><br>
</font></div>
<div><font face="Courier New">struct list {</font></div>
<div><font face="Courier New"> int key;</font></div>
<div><font face="Courier New"> struct blob value</font></div>
<div><font face="Courier New"> list_t next; // here as well</font></div>
<div><font face="Courier New">};</font></div>
<div><font face="Courier New"><br>
</font></div>
<div><font face="Courier New">int buggy_length(list_t l) {</font></div>
<div><font face="Courier New"> int x = 1;</font></div>
<div><font face="Courier New"> while(l -> next) { // boom</font></div>
<div><font face="Courier New"><span class="Apple-tab-span" style="white-space: pre; "></span>x++;</font></div>
<div><font face="Courier New"><span class="Apple-tab-span" style="white-space: pre; "></span>l = l -> next;</font></div>
<div><font face="Courier New"> }</font></div>
<div><font face="Courier New"> return x;</font></div>
<div><font face="Courier New">}</font></div>
<div><font face="Courier New"><br>
</font></div>
<div><font face="Courier New">list_t buggy_next(struct list st) {</font></div>
<div><font face="Courier New"> return st.next; // re-boom</font></div>
<div><font face="Courier New">}</font></div>
<div><font face="Courier New"><br>
</font></div>
<div><font face="Courier New">int find(list_t l, int value, struct blob *__nonnull__ result) {</font></div>
<div><span style="font-family: 'Courier New'; ">// some code to find a node in the list and write it to *result</span></div>
<div><span style="font-family: 'Courier New'; ">}</span></div>
<div><br>
</div>
</div>
<blockquote type="cite">
<div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">
<div><br>
</div>
<div>Jordan</div>
<div><br>
</div>
<br>
<div>
<div>On May 6, 2013, at 19:20 , Mathieu Baudet <<a href="mailto:mathieubaudet@fb.com">mathieubaudet@fb.com</a>> wrote:</div>
<br class="Apple-interchange-newline">
<blockquote type="cite">
<div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">
Hi list,
<div><br>
</div>
<div>Is anyone in the position to offer some insight on the question (below) about possibly using Clang analyzer for more "contract-based" null-pointer analyses?</div>
<div>
<div><br>
</div>
<div>--</div>
<div>Mathieu</div>
<div><br>
</div>
<div>On May 2, 2013, at 5:43 PM, Mathieu Baudet <<a href="mailto:mathieubaudet@fb.com">mathieubaudet@fb.com</a>> wrote:
<div><br class="Apple-interchange-newline">
<blockquote type="cite">
<div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">
<div>On a slightly different topic, has anyone ever considered using the core of clang-analyzer to bring more fine-grained annotations to life, in the spirit of Findbugs for Java?</div>
<div> <a href="https://urldefense.proofpoint.com/v1/url?u=http://findbugs.sourceforge.net/manual/annotations.html&k=ZVNjlDMF0FElm4dQtryO4A%3D%3D%0A&r=DySJRSwIPwJgrlWcFuOjhjgW2TvEV7mDN%2BhK5RWHkOA%3D%0A&m=ypYa%2F2cxjWXNEkgs%2FMXwdm19awfhaGyd7usPqi6NrAM%3D%0A&s=f29d699397d55f1f8ce0aabb8ddfcb0bb175bac5c0dda1abab8010ed7d7b013b">http://findbugs.sourceforge.net/manual/annotations.html</a></div>
<div><br>
</div>
<div>From this page</div>
<div> <a href="https://urldefense.proofpoint.com/v1/url?u=http://clang-analyzer.llvm.org/annotations.html&k=ZVNjlDMF0FElm4dQtryO4A%3D%3D%0A&r=DySJRSwIPwJgrlWcFuOjhjgW2TvEV7mDN%2BhK5RWHkOA%3D%0A&m=ypYa%2F2cxjWXNEkgs%2FMXwdm19awfhaGyd7usPqi6NrAM%3D%0A&s=97860c12802ff0270af264614dece9dc213d5dd424f3939c3e62a26656303d7b">http://clang-analyzer.llvm.org/annotations.html</a></div>
<div>I understand that we can already attach attributes to various syntactic elements (not sure exactly which ones yet, though).</div>
<div><br>
</div>
<div>Is there any reason to believe that this project would require more than just writing a new checker?</div>
<div><br>
</div>
<div>-- Mathieu</div>
<br>
<div>
<div>On May 2, 2013, at 1:33 PM, Jordan Rose <<a href="mailto:jordan_rose@apple.com">jordan_rose@apple.com</a>> wrote:</div>
<br class="Apple-interchange-newline">
<blockquote type="cite">
<div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">
<div>Hi, Mathieu. You've run into one of the analyzer's haziest features: false positive suppression based on return values. To put it simply, if there's a null pointer dereference, and it turns out the null pointer came from an inlined function, we suppress
the warning.</div>
<div><br>
</div>
<div>Why? Well, for better or for worse the analyzer does not have perfect information. Consider an example like this:</div>
<div><br>
</div>
<div>
<div><span class="Apple-tab-span" style="white-space:pre"></span>targetMap[targetName]->process(input);</div>
<br>
</div>
<div>Seems harmless, right? Well, what does the map's operator[] look like?</div>
<div><br>
</div>
<div><span class="Apple-tab-span" style="white-space:pre"></span>Target *getItem(StringRef name) {</div>
<div><span class="Apple-tab-span" style="white-space:pre"></span>if (map contains a target for name)</div>
<div><span class="Apple-tab-span" style="white-space:pre"></span>return it</div>
<div><span class="Apple-tab-span" style="white-space:pre"></span>return NULL;</div>
<div><span class="Apple-tab-span" style="white-space:pre"></span>}</div>
<div><br>
</div>
<div>Most likely, the analyzer doesn't have perfect knowledge about the contents of the map, so it assumes both branches can be taken—which is totally reasonable! However, the caller could very well have some extra knowledge: the targetName is checked at the
beginning of the program, and so the map lookup will never fail at this point.</div>
<div><br>
</div>
<div>Usually, the response to this sort of bug is to add an assertion, but in this case you wouldn't be able to do that without introducing a temporary variable and breaking apart the original expression.</div>
<div><br>
</div>
<div>When we first turned on C++ inlining, this sort of example resulting in hundreds of false posiitves on the LLVM code base. It did find some true positives, such as unchecked calls to dyn_cast, but in general it was just not compatible with the way people
write code. A lot of times, generic functions have to handle error cases that the caller
<i>knows</i> won't happen, but would find annoying or difficult to actually assert() about. We've found that a lot of these cases correspond to a null value being returned, which is
<i>entirely</i> a heuristic.</div>
<div><br>
</div>
<div>The false positive suppression heuristics can definitely be improved, but in general false negatives are better for the analyzer than false positives. The former reduces bugs caught and confidence in the tool, but the latter results in people turning off
a checker wholesale or not running the analyzer at all.</div>
<div><br>
</div>
<div>Anyway, thanks for the report, and if you come up with any "counter-suppression" ideas, please send them to the list!</div>
<div><br>
</div>
<div>Jordan</div>
<div><br>
</div>
<br>
<div>
<div>On May 1, 2013, at 22:16 , Mathieu Baudet <<a href="mailto:mathieubaudet@fb.com">mathieubaudet@fb.com</a>> wrote:</div>
<br class="Apple-interchange-newline">
<blockquote type="cite">Hi,<br>
<br>
As I was testing NonNullParamChecker this afternoon, I ran into this troubling example:<br>
<br>
// --------- example 1 ------------<br>
void *getNull() {<br>
return 0;<br>
}<br>
<br>
void check(void *p) __attribute__(( nonnull ));<br>
void check(void *p) {<br>
}<br>
<br>
int main(int argc, char **argv) {<br>
void *p = getNull();<br>
check(p);<br>
return 0;<br>
}<br>
// --------------------------------<br>
<br>
This code gives no warning on the versions of clang that I could test:<br>
- Apple LLVM version 4.2 (clang-425.0.28) (based on LLVM 3.2svn)<br>
- clang version 3.3 (trunk 180768)<br>
- clang version 3.3 (trunk 180907) (llvm/trunk 180768)<br>
<br>
To get an error one I have to replace p = getNull() by p = 0.<br>
<br>
First I was tempted to think it was just a limitation of the core analyzer, but<br>
1) I obtain an error with a similar example where the nonnull attribute is replaced by a division by zero (see example 2 at the end)<br>
<br>
2) I debugged the file NonNullParamChecker.cpp : I am very new to this codebase but it seems that a report is actually emitted (lines 119-139). Then it never shows up for some reason...<br>
<br>
Is this a bug? If not, how can we improve this checker?<br>
<br>
Thanks!<br>
--<br>
Mathieu<br>
<br>
<br>
// --------- example 2 -----------<br>
int getX() {<br>
return 0;<br>
}<br>
<br>
void check(int p) {<br>
1 / p;<br>
}<br>
<br>
int main(int argc, char **argv) {<br>
int x = getX();<br>
check(x);<br>
return 0;<br>
}<br>
<br>
<br>
_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@cs.uiuc.edu">cfe-dev@cs.uiuc.edu</a><br>
<a href="https://urldefense.proofpoint.com/v1/url?u=http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev&k=ZVNjlDMF0FElm4dQtryO4A%3D%3D%0A&r=DySJRSwIPwJgrlWcFuOjhjgW2TvEV7mDN%2BhK5RWHkOA%3D%0A&m=ypYa%2F2cxjWXNEkgs%2FMXwdm19awfhaGyd7usPqi6NrAM%3D%0A&s=d7644f203409e1f01227fb4d7e7fc52597cdb92028884d1660354a5cf4aef9de">http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev</a><br>
</blockquote>
</div>
<br>
</div>
</blockquote>
</div>
<br>
</div>
</blockquote>
</div>
<br>
</div>
</div>
</div>
</blockquote>
</div>
<br>
</div>
</blockquote>
</div>
<br>
</body>
</html>