[analyzer] Widen loops: Augment assignment note when values invalidated at the start of a loop

clang/include/clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h

@@ -290,6 +290,10 @@ class ExprEngine {
   /// This tag applies to a node created after removeDead.
   static const ProgramPointTag *cleanupNodeTag();
 
+  /// A tag to track when loop widening occurs.
+  /// This tag applies to a node created after getWidenedLoopState.
+  static const ProgramPointTag *loopWideningNodeTag();
+
   /// processCFGElement - Called by CoreEngine. Used to generate new successor
   ///  nodes by processing the 'effects' of a CFG element.
   void processCFGElement(const CFGElement E, ExplodedNode *Pred,

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

@@ -1353,6 +1353,49 @@ static void showBRDefaultDiagnostics(llvm::raw_svector_ostream &OS,
     OS << " to ";
     SI.Dest->printPretty(OS);
   }
+
+  // If the value was part of a loop widening node and its value was
+  // invalidated (i.e. replaced with a conjured symbol) then let the user know
+  // that it was due to loop widening.
+  if (SI.StoreSite && SI.Dest &&
+      SI.StoreSite->getLocation().getTag() ==
+          ExprEngine::loopWideningNodeTag()) {
+
+    // TODO: Is it always the case that there's only one predecessor?
+    assert(SI.StoreSite->hasSinglePred() &&
+           "more than one predecessor found, this needs to be handled...");
+    if (const ExplodedNode *previous = SI.StoreSite->getFirstPred()) {
+      // Was the associated memory region for this variable changed from
+      // non-Symbolic to Symbolic because of invalidation?
+      // TODO: Better yet, if there was simply a way to know if a given
+      // SVal / MemRegion was invalidated as part of the current state,
+      // then that should be more robust than what's going on here.
+      // Could we somehow make use of "RegionChanges" /
+      // "runCheckersForRegionChanges" and the ExplicitRegions parameter.
+      // Still need to somehow know when a particular Global
+      // Variable is invalidated. I have not found this to be possible with
+      // "RegionChanges" unless I'm missing something...
+      const ProgramState *lastState = previous->getState().get();
+      const SVal &lastSVal = lastState->getSVal(SI.Dest);
+      const SymbolRef valueSymbol = SI.Value.getAsSymbol(true);
+      const SymbolRef lastSymbol = lastSVal.getAsSymbol(true);
+
+      bool isNowSymbolic = false;
+      if (valueSymbol) {
+        if (!lastSymbol) {
+          // Last state did not have a symbol for SI.Value in current state.
+          // Probably (?) invalidated.
+          isNowSymbolic = true;
+        } else {
+          // If the symbol types differ, then there was likely invalidation
+          isNowSymbolic = valueSymbol->getKind() != lastSymbol->getKind();
+        }
+      }
+
+      if (isNowSymbolic)
+        OS << " (invalidation as part of widen-loops made this symbolic here)";
+    }
+  }
 }
 
 static bool isTrivialCopyOrMoveCtor(const CXXConstructExpr *CE) {

clang/lib/StaticAnalyzer/Core/ExprEngine.cpp

@@ -1109,6 +1109,11 @@ const ProgramPointTag *ExprEngine::cleanupNodeTag() {
   return &cleanupTag;
 }
 
+const ProgramPointTag *ExprEngine::loopWideningNodeTag() {
+  static SimpleProgramPointTag loopWideningTag(TagProviderName, "Widen Loop");
+  return &loopWideningTag;
+}
+
 void ExprEngine::ProcessStmt(const Stmt *currStmt, ExplodedNode *Pred) {
   // Reclaim any unnecessary nodes in the ExplodedGraph.
   G.reclaimRecentlyAllocatedNodes();
@@ -2546,7 +2551,7 @@ void ExprEngine::processCFGBlockEntrance(const BlockEdge &L,
     const LocationContext *LCtx = Pred->getLocationContext();
     ProgramStateRef WidenedState =
         getWidenedLoopState(Pred->getState(), LCtx, BlockCount, Term);
-    nodeBuilder.generateNode(WidenedState, Pred);
+    nodeBuilder.generateNode(WidenedState, Pred, loopWideningNodeTag());
     return;
   }
 

clang/test/Analysis/loop-widening-notes.cpp

@@ -9,7 +9,7 @@ int test_for_bug_25609() {
     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,        // expected-note {{Value assigned to 'p_a' (invalidation as part of widen-loops made this symbolic here)}}
        i < flag_a;
        ++i) {}
 
@@ -23,7 +23,7 @@ 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@-1 {{Value assigned to 'num' (invalidation as part of widen-loops made this symbolic here)}}
                          // expected-note@-2 {{Loop condition is false. Execution continues on line 30}}
     num = flag_b;
   }
@@ -45,7 +45,7 @@ int do_while_analyzer_output() {
   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'}}
+  } while (flag_c-- > 0); //expected-note {{Value assigned to 'num' (invalidation as part of widen-loops made this symbolic here)}}
   int local = 0;
   if (num == 0)       // expected-note {{Assuming 'num' is equal to 0}} 
                       // expected-note@-1 {{Taking true branch}}
@@ -59,7 +59,7 @@ 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'}}
+       new int(10),  // expected-note {{Value assigned to 'num' (invalidation as part of widen-loops made this symbolic here)}}
        i < flag_d;
        ++i) {         
     ++num;
@@ -73,7 +73,7 @@ int test_for_loop() {
 
 int test_for_range_loop() {
   int arr[10] = {0};
-  for(auto x : arr) { // expected-note {{Assigning value}} 
+  for(auto x : arr) { // expected-note {{Assigning value (invalidation as part of widen-loops made this symbolic here)}}
     ++x;
   }
   if (arr[0] == 0)   // expected-note {{Assuming the condition is true}} 

clang/test/Analysis/loop-widening.cpp

@@ -16,7 +16,7 @@ void fn1() {
 
   for (;;) { // expected-note{{Loop condition is true.  Entering loop body}}
              // expected-note@-1{{Loop condition is true.  Entering loop body}}
-             // expected-note@-2{{Value assigned to 'b'}}
+             // expected-note@-2{{Value assigned to 'b' (invalidation as part of widen-loops made this symbolic here)}}
              // no crash during bug report construction
 
     g = !b;     // expected-note{{Assuming 'b' is null}}