[Analyzer] Fix Bug 25609 - Assertion UNREACHABLE: 'Unexpected ProgramPoint' with widen-loops=true

[MTC]

Summary

In the original design of the analyzer, it is assumed that the BlockEntrance doesn't create a new binding on the Store, But this assumption isn't true when 'widen-loops' sets true.

Regards,

Henry Wong

[MTC]

This comment was removed by MTC.

[MTC]

Sorry, remove irrelevant code updates.

[NoQ]

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

651–652 ↗

(On Diff #112892)

This is user-facing text, and users shouldn't know about conjured symbols, and "max" shouldn't be shortened, and i'm not sure what else. I'd probably suggest something along the lines of "Contents of <...> are wiped", but this is still not good enough.

Also could you add a test that displays this note? I.e. with -analyzer-output=text.

[MTC]

Add the test file and modify the description in the analyzer output.

[MTC]

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

651–652 ↗

(On Diff #112892)

Thanks for your review.

You are right, whether this information should be displayed to the user is a question worth discussing.

[szepet]

Hello MTC,

Thanks for working on this! I planned to add a change like this in D36690 but it worths an individual patch (did not know it was a reported bug).
Just some thoughts:

• I think the current display information is ambiguous. If I did not know the code then I would not understand what this stands for. (That is just my opinon.) I think Artem's "Contents of <...> are wiped" idea is better but I would go with something like this: "Invalidated previously known information on <...>". (Maybe remove the word 'previously' if its too long.) It still can be weird for the user that why this happened but at least in case of a false positive he/she can see that why this was even considered by the analyzer.
• Right now there is a "race condition" between your patch and D36690. So in order to avoid "conflicts" I'd ask you to add some variable changing effect to the body of the loop. For example in the last test case the variable 'num' is the one which you use to show the effect of widening. In this case a line like num++ or num = i would ensure that the more precise widening invalidates it as well. Other thing is that handling loops which contains pointer operation or nested loops will be a little bit more conservative, so you these will not be widened like now. (However, test_for_bug_25609()) still should be valid.
• Please upload the diff with context (git flag: -U99999) since it is really helpful for the review.
• +1 inline comment below.

lib/StaticAnalyzer/Core/PathDiagnostic.cpp

694 ↗

(On Diff #112969)

I think it would be more correct to use the location what is used in case of the BlockEdge. (So on the entranced block terminator condition.) The reason is because the BlockEntrance display message will be displayed before the message of the BlockEdge (since it is an "earlier" node in the ExplodedGraph). So it would result that if check these notes in a viewer then the earlier note would belong to the later location which could be confusing.

[MTC]

Hi peter,

Thank you very much for your help.

• I think the current display information is ambiguous. If I did not know the code then I would not understand what this stands for. (That is just my opinon.) I think Artem's "Contents of <...> are wiped" idea is better but I would go with something like this: "Invalidated previously known information on <...>". (Maybe remove the word 'previously' if its too long.) It still can be weird for the user that why this happened but at least in case of a false positive he/she can see that why this was even considered by the analyzer.

Yes, that's the problem. The information displayed to the user should be clear, but not difficult to understand.

• Right now there is a "race condition" between your patch and D36690. So in order to avoid "conflicts" I'd ask you to add some variable changing effect to the body of the loop. For example in the last test case the variable 'num' is the one which you use to show the effect of widening. In this case a line like num++ or num = i would ensure that the more precise widening invalidates it as well. Other thing is that handling loops which contains pointer operation or nested loops will be a little bit more conservative, so you these will not be widened like now. (However, test_for_bug_25609()) still should be valid.

I'll update the test file，:D.

• Please upload the diff with context (git flag: -U99999) since it is really helpful for the review.

About ‘git diff’, that's my mistake, and I'll add this option next time. Thank you very much for pointing it out!

• +1 inline comment below.

[MTC]

(1) Modify the description of the bug report
(2) Update loop-widening-notes.c
(3) PathDiagnosticLocation::create() - Use the location of TerminatorCondition.

[MTC]

lib/StaticAnalyzer/Core/PathDiagnostic.cpp

694 ↗

(On Diff #112969)

Yes, it would be better to use the location of the TerminatorCondition :D.

[szepet]

Thanks for the update!
It looks good to me! (Probably somebody else (most likely NoQ) will have some additional comment but I think it's great!)

[xazax.hun]

LGTM!

[zaks.anna]

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

651–652 ↗

(On Diff #112892)

I am not convinced that we need to print this information to the user. The problem here is that it leaks internal implementation details about the analyzer. The users should not know about "loop limits" and "invalidation" and most of the users would not even know what this means. I can see how this is useful to the analyzer developers for debugging the analyzer, but not to the end user.

[xazax.hun]

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

651–652 ↗

(On Diff #112892)

While we might not want to expose this to the user this can be really useful to understand what the analyzer is doing when we debugging a false positive finding. Maybe it would be worth to introduce a developer mode or verbose mode for those purposes. What do you think?

[zaks.anna]

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

651–652 ↗

(On Diff #112892)

I'd be fine with that in theory, though the downside is that it would pollute the code a bit. One trick that's often used to better understand a report when debugging is to remove the path note pruning (by passing a flag). I am not sure if that approach can be extended for this case. Ex: maybe we could have special markers on the notes saying that they are for debug purposes only and have the pruning remove them.

By the way, is this change related to the other change from this patch?

[xazax.hun]

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

651–652 ↗

(On Diff #112892)

I agree that we should just commit this without the message to fix the assert. The "debug message" could be addressed in a separate patch.

[MTC]

The message about invalidate variable values is temporarily not printed. This work can be done with separate patch.

[MTC]

Split the long "expected" line into multiple lines.

[MTC]

ping?

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

651–652 ↗

(On Diff #112892)

Thank you for your review!
Agree with you, and Artem also recommends not exposing too much internal implementation to the user.

651–652 ↗

(On Diff #112892)

Thank you, Gábor!
That's a good point. I think this idea requires a little bit of work to be done, and it should be done by someone more familiar with BugReport or PathDiagnostic, :).

651–652 ↗

(On Diff #112892)

Thanks, anna!
The output here is just to make it better for the user to figure out what's going on here. Delete the output information does not affect the other part, but the output information is changed from "Reach the maximum loop limit. Invalidate the value of 'num'" becomes the original output information "value assigned to 'p'".

651–652 ↗

(On Diff #112892)

Done!

[MTC]

ping?

[xazax.hun]

LGTM! But wait for @dcoughlin, @zaks.anna , or @NoQ before commit.

[dcoughlin]

lib/StaticAnalyzer/Core/PathDiagnostic.cpp

694 ↗

(On Diff #112969)

Thanks for looking into fixing this.

I don't think using the terminator condition of the entered block is the right thing to do. The terminator is at the *end* of a basic block and this program point represents the entrance to the block. I think it is better to use the location corresponding to the first element in in the entered block.

[MTC]

Update diff, use the SourceLocation of the first element of the entered block as the argument of PathDiagnosticLocation.

[MTC]

lib/StaticAnalyzer/Core/PathDiagnostic.cpp

694 ↗

(On Diff #112969)

Thank you, dcoughlin!

I have updated the diff. The first element kind I can think of is only Stmt and NewAllocator. I don't know if it's enough?

[dcoughlin]

lib/StaticAnalyzer/Core/PathDiagnostic.cpp

695 ↗

(On Diff #123783)

You can use getAs<> in the if guard condition to make this more concise:

if (auto StmtElt = BlockFront.getAs<CFGStmt>()) {
  return PathDiagnosticLocation(StmtElt->getStmt()->getLocStart(), SMng);
}

694 ↗

(On Diff #112969)

It would be good to add an llvm_unreachable() assertion expressing this expectation so that we'll get an assertion failure if this turns out not to be enough. (Or if we add a new CFGElement kind in the future).

[MTC]

1.Use the getAs<> in the if condition.
2.Add an "Unexpected ProgramPoint" assertion to make this patch more complete.

[dcoughlin]

LGTM, but as noted inline you should update the new llvm_unreachable() to have a more descriptive error message.

Do you have commit access or do you need someone to commit this for you?

lib/StaticAnalyzer/Core/PathDiagnostic.cpp

701 ↗

(On Diff #124248)

This assertion should probably say something like "Unexpected CFG element at front of block".

[MTC]

Update the llvm_unreachable's description of the BlockEntrance-branch from "Unexpected ProgramPoint" to "Unexpected CFG element at front of block".

[MTC]

Hi dcoughlin,

Thank you very much for your help. I have no commit access and hope someone can commit it on my behalf. Thanks a lot!

cfe/trunk/lib/StaticAnalyzer/Core/PathDiagnostic.cpp

PathDiagnosticLocation::create(const ProgramPoint& P,
   } else if (Optional<CallEnter> CE = P.getAs<CallEnter>()) {
     return getLocationForCaller(CE->getCalleeContext(),
                                 CE->getLocationContext(),
                                 SMng);
   } else if (Optional<CallExitEnd> CEE = P.getAs<CallExitEnd>()) {
     return getLocationForCaller(CEE->getCalleeContext(),
                                 CEE->getLocationContext(),
                                 SMng);
+  } else if (Optional<BlockEntrance> BE = P.getAs<BlockEntrance>()) {
+    CFGElement BlockFront = BE->getBlock()->front();
+    if (auto StmtElt = BlockFront.getAs<CFGStmt>()) {
+      return PathDiagnosticLocation(StmtElt->getStmt()->getLocStart(), SMng);
+    } else if (auto NewAllocElt = BlockFront.getAs<CFGNewAllocator>()) {
+      return PathDiagnosticLocation(
+          NewAllocElt->getAllocatorExpr()->getLocStart(), SMng);
+    }
+    llvm_unreachable("Unexpected CFG element at front of block");
   } else {
     llvm_unreachable("Unexpected ProgramPoint");
   }
 
   return PathDiagnosticLocation(S, SMng, P.getLocationContext());
 }
 
 static const LocationContext *

cfe/trunk/test/Analysis/loop-widening-notes.cpp

+// RUN: %clang_analyze_cc1 -analyzer-checker=core,alpha -analyzer-max-loop 2 -analyzer-config widen-loops=true -analyzer-output=text -verify %s
+
+int *p_a;
+int bar();
+int flag_a;
+int test_for_bug_25609() {
+  if (p_a == 0) // expected-note {{Assuming 'p_a' is equal to null}} 
+                // expected-note@-1 {{Taking true branch}}
+    bar();
+  for (int i = 0;  // expected-note {{Loop condition is true.  Entering loop body}}                    
+                   // expected-note@-1 {{Loop condition is false. Execution continues on line 16}}
+       ++i,        // expected-note {{Value assigned to 'p_a'}} 
+       i < flag_a;
+       ++i) {}
+                                      
+  *p_a = 25609; // no-crash expected-warning {{Dereference of null pointer (loaded from variable 'p_a')}}
+                // expected-note@-1 {{Dereference of null pointer (loaded from variable 'p_a')}}
+  return *p_a;
+}
+
+int flag_b;
+int while_analyzer_output() {
+  flag_b = 100;
+  int num = 10;
+  while (flag_b-- > 0) { // expected-note {{Loop condition is true.  Entering loop body}} 
+                         // expected-note@-1 {{Value assigned to 'num'}} 
+                         // expected-note@-2 {{Loop condition is false. Execution continues on line 30}}
+    num = flag_b;
+  }
+  if (num < 0) // expected-note {{Assuming 'num' is >= 0}} 
+               // expected-note@-1 {{Taking false branch}}
+    flag_b = 0;
+  else if (num >= 1) // expected-note {{Assuming 'num' is < 1}} 
+                     // expected-note@-1 {{Taking false branch}}
+    flag_b = 50;
+  else
+    flag_b = 100;
+  return flag_b / num; // no-crash expected-warning {{Division by zero}} 
+                       // expected-note@-1 {{Division by zero}}
+}
+
+int flag_c;
+int do_while_analyzer_output() {
+  int num = 10;
+  do {   // expected-note {{Loop condition is true. Execution continues on line 47}} 
+         // expected-note@-1 {{Loop condition is false.  Exiting loop}}
+    num--;
+  } while (flag_c-- > 0); //expected-note {{Value assigned to 'num'}}
+  int local = 0;
+  if (num == 0)       // expected-note {{Assuming 'num' is equal to 0}} 
+                      // expected-note@-1 {{Taking true branch}}
+    local = 10 / num; // no-crash expected-warning {{Division by zero}}
+                      // expected-note@-1 {{Division by zero}}
+  return local;
+}
+
+int flag_d;
+int test_for_loop() {
+  int num = 10;
+  for (int i = 0;    // expected-note {{Loop condition is true.  Entering loop body}} 
+                     // expected-note@-1 {{Loop condition is false. Execution continues on line 67}}
+       new int(10),  // expected-note {{Value assigned to 'num'}}
+       i < flag_d;
+       ++i) {         
+    ++num;
+  }
+  if (num == 0) // expected-note {{Assuming 'num' is equal to 0}} 
+                // expected-note@-1 {{Taking true branch}}
+    flag_d += 10;
+  return flag_d / num; // no-crash expected-warning {{Division by zero}} 
+                       // expected-note@-1 {{Division by zero}}
+}