[PATCH] D53076: [analyzer] Enhance ConditionBRVisitor to write out more information

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In https://reviews.llvm.org/D53076#1276315, @Charusso wrote:

> In https://reviews.llvm.org/D53076#1276277, @NoQ wrote:
>
> > I mean, the idea of checking constraints instead of matching program points is generally good, but the example i gave above suggests that there's a bug somewhere.
>
>
> I think it is an unimplemented feature which appear like 1:500 time, but we will see.


The original behavior is perfectly consistent with my understanding of Static Analyzer's reports that i've been reading continuously for years. There might have been a few places where assumption is made but isn't highlighted, but the opposite has never happened, and also the opposite is more confusing to the user because it demonstrates an explicit text that the user has to trust. So i think that one way or another, the new behavior is a regression from the original behavior on an on-by-default functionality on some test cases, and we should not commit this patch until this regression is debugged and fixed.

I highlight a few more test cases that i believe have regressed in inline comments.



================
Comment at: test/Analysis/MisusedMovedObject.cpp:187
     A a;
-    if (i == 1) { // expected-note {{Taking false branch}} expected-note {{Taking false branch}}
+    if (i == 1) { // expected-note {{Assuming 'i' is not equal to 1}} expected-note {{Taking false branch}}
+      // expected-note at -1 {{Assuming 'i' is not equal to 1}} expected-note at -1 {{Taking false branch}}
----------------
These assumptions were already made on the previous branches. There should be no extra assumptions here.


================
Comment at: test/Analysis/MisusedMovedObject.cpp:221
     }
-    if (i > 5) { // expected-note {{Taking true branch}}
+    if (i > 5) { // expected-note {{Assuming 'i' is > 5}} expected-note {{Taking true branch}}
       a.foo();   // expected-warning {{Method call on a 'moved-from' object 'a'}} expected-note {{Method call on a 'moved-from' object 'a'}}
----------------
We have assumed that `i` is `>= 10` on the previous branch. It imples that `i` is greater than `5`, so no additional assumption is being made here.


================
Comment at: test/Analysis/NewDelete-path-notes.cpp:10
   if (p)
-    // expected-note at -1 {{Taking true branch}}
+    // expected-note at -1 {{Assuming 'p' is non-null}}
+    // expected-note at -2 {{Taking true branch}}
----------------
Static Analyzer knows that the standard operator new never returns null. Therefore no assumption is being made here.


================
Comment at: test/Analysis/diagnostics/macros.cpp:33
 void testDoubleMacro(double d) {
-  if (d == DBL_MAX) { // expected-note {{Taking true branch}}
+  if (d == DBL_MAX) { // expected-note {{Assuming 'd' is equal to DBL_MAX}}
+                      // expected-note at -1 {{Taking true branch}}
----------------
This one's good. Static Analyzer doesn't understand floats, so this branch is indeed non-trivial. There should indeed be an assuming... piece here.


================
Comment at: test/Analysis/diagnostics/no-store-func-path-notes.cpp:23
   int initialize(int *p, int param) {
-    if (param) { //expected-note{{Taking false branch}}
+    if (param) { // expected-note{{Assuming 'param' is 0}}
+                 // expected-note at -1{{Taking false branch}}
----------------
This method is called from `use()` with `param` equal to concrete 0. It is not analyzed as a top-level function. There is no assumption made here, like in most other places in this file.


================
Comment at: test/Analysis/diagnostics/no-store-func-path-notes.m:13
 - (int)initVar:(int *)var param:(int)param {
-  if (param) { // expected-note{{Taking false branch}}
+  if (param) { // expected-note{{Assuming 'param' is 0}}
+               // expected-note at -1{{Taking false branch}}
----------------
This method is called from `foo()` with `param` equal to concrete `0`. It is not analyzed as a top-level function. There is no assumption made here.


================
Comment at: test/Analysis/diagnostics/no-store-func-path-notes.m:26
                                     //expected-note at -1{{Returning from 'initVar:param:'}}
-  if (out)                          // expected-note{{Taking true branch}}
+  if (out)                          // expected-note{{Assuming 'out' is not equal to 0}}
+                                    // expected-note at -1{{Taking true branch}}
----------------
`-initVar` returns concrete `0` when called with these parameters. There is no assumption being made here.


================
Comment at: test/Analysis/diagnostics/no-store-func-path-notes.m:34
 int initializer1(int *p, int x) {
-  if (x) { // expected-note{{Taking false branch}}
+  if (x) { // expected-note{{Assuming 'x' is 0}}
+           // expected-note at -1{{Taking false branch}}
----------------
This function is called from `inifFromBlock()` with `x` equal to concrete `0`. It is not analyzed as a top-level function. Therefore, no assumption is being made here.


================
Comment at: test/Analysis/inline-plist.c:46
   if (p == 0) {
-    // expected-note at -1 {{Taking true branch}}
+    // expected-note at -1 {{Assuming 'p' is equal to null}}
+    // expected-note at -2 {{Taking true branch}}
----------------
The condition `!!p` above being assumed to false ensures that `p` is equal to `null` here. We are not assuming it again here.


================
Comment at: test/Analysis/uninit-vals.m:167
   testObj->origin = makePoint(0.0, 0.0);
-  if (testObj->size > 0) { ; } // expected-note{{Taking false branch}}
+  if (testObj->size > 0) { ; } // expected-note{{Assuming the condition is false}}
+                               // expected-note at -1{{Taking false branch}}
----------------
These are pretty weird. As far as i understand the test, these should be there. But i'm suddenly unable to debug why were they not shown before, because there's either something wrong with exploded graph dumps or with the exploded graph itself; it appears to be missing an edge right after `size > 0` is assumed. I'll look more into those.


https://reviews.llvm.org/D53076