[analyzer] PR37501: Disable the assertion for reverse-engineering logical op short circuits.

[NoQ]

Summary

Replace the incorrect assertion with a lot of swearing in comments. This should take care of these rare crashes such as https://bugs.llvm.org/show_bug.cgi?id=37501 and the minimal fallback behavior i added should hopefully be better than just dropping the assertion (instead of picking a path for backtracking at random, we admit that we don't know the value). The idea behind the original implementation is elegant, but it doesn't really work.

I did try to replace the logic with trying to evaluate logical operators as if they were regular operators: take the LHS value, take the RHS value, apply math. It's not easy because it requires tweaking liveness analysis to make sure that all the necessary values are alive; i couldn't immediately fix all the failres on tests. Even if i did get it working, i suspect that this is also a dead end, because we have these "unknown value" things. Even if the values of the operands were too complicated to compute and evaluated to UnknownVals, we can still obtain the correct value of the logical operator via backtracking ("we're at this point in our execution path, therefore the LHS must have been assumed to be true"), but not via math ("whoops, the LHS is unknown").

We could combine both techniques (backtracking and math, use one when the other fails), but that's an overkill for such a rare problem, so i decided to just remove the assertion.

The truly reliable solution in our situation would be to set a flag in the program state whenever we're doing a short circuit operation, and consume it in VisitLogicalExpr. But that also requires making sure we don't mess up with all those CFG cornercases, so i decided to leave it as an exercise for the future generations of Static Analyzer developers.

[Charusso]

There is no connection with my reverse-engineering reverted patch: https://reviews.llvm.org/D57410?id=184992 ? It evaluates the left and the right side and may it could help.

[alexfh]

LG

lib/StaticAnalyzer/Core/ExprEngineC.cpp

for (ExplodedNodeSet::iterator I = dstPreVisit.begin(), E = dstPreVisit.end();
     }
   }
 
   getCheckerManager().runCheckersForPostStmt(Dst, B.getResults(), DS, *this);
 }
 
 void ExprEngine::VisitLogicalExpr(const BinaryOperator* B, ExplodedNode *Pred,
                                   ExplodedNodeSet &Dst) {
+  // This method acts upon CFG elements for logical operators && and ||
+  // and attaches the value (true or false) to them as expressions.
+  // It doesn't produce any state splits.
+  // If we made it that far, we're past the point when we modeled the short
+  // circuit. It means that we should have precise knowledge about whether
+  // we've short-circuited. If we did, we already know the value we need to
+  // bind. If we didn't, the value of the RHS (casted to the boolean type)
+  // is the answer.
+  // Currently this method tries to figure out whether we've short-circuited
+  // by looking at the ExplodedGraph. This method is imperfect because there
+  // could inevitably have been merges that would have resulted in multiple
+  // potential path traversal histories. We bail out when we fail.
+  // Due to this ambiguity, a more reliable solution would have been to
+  // track the short circuit operation history path-sensitively until
+  // we evaluate the respective logical operator.
   assert(B->getOpcode() == BO_LAnd ||
          B->getOpcode() == BO_LOr);
 
   StmtNodeBuilder Bldr(Pred, Dst, *currBldrCtx);
   ProgramStateRef state = Pred->getState();
 
   if (B->getType()->isVectorType()) {
     // FIXME: We do not model vector arithmetic yet. When adding support for
     // that, note that the CFG-based reasoning below does not apply, because
     // logical operators on vectors are not short-circuit. Currently they are
     // modeled as short-circuit in Clang CFG but this is incorrect.
     // Do not set the value for the expression. It'd be UnknownVal by default.
     Bldr.generateNode(B, Pred, state);
     return;
   }
 
   ExplodedNode *N = Pred;
   while (!N->getLocation().getAs<BlockEntrance>()) {
     ProgramPoint P = N->getLocation();
     assert(P.getAs<PreStmt>()|| P.getAs<PreStmtPurgeDeadSymbols>());
     (void) P;
-    assert(N->pred_size() == 1);
+    if (N->pred_size() != 1) {
+      // We failed to track back where we came from.
+      Bldr.generateNode(B, Pred, state);
+      return;
+    }
     N = *N->pred_begin();
   }
-  assert(N->pred_size() == 1);
+
+  if (N->pred_size() != 1) {
+    // We failed to track back where we came from.
+    Bldr.generateNode(B, Pred, state);
+    return;
+  }
+
   N = *N->pred_begin();
   BlockEdge BE = N->getLocation().castAs<BlockEdge>();
   SVal X;
 
   // Determine the value of the expression by introspecting how we
   // got this location in the CFG.  This requires looking at the previous
   // block we were in and what kind of control-flow transfer was involved.
   const CFGBlock *SrcBlock = BE.getSrc();

test/Analysis/logical-ops.c

-// RUN: %clang_analyze_cc1 -Wno-pointer-bool-conversion -analyzer-checker=core,debug.ExprInspection -verify -analyzer-config eagerly-assume=false %s
+// RUN: %clang_analyze_cc1 -w -analyzer-checker=core,debug.ExprInspection\
+// RUN:                    -analyzer-config eagerly-assume=false -verify %s
 
 void clang_analyzer_eval(int);
 
 void testAnd(int i, int *p) {
   int *nullP = 0;
   int *knownP = &i;
   clang_analyzer_eval((knownP && knownP) == 1); // expected-warning{{TRUE}}
   clang_analyzer_eval((knownP && nullP) == 0); // expected-warning{{TRUE}}

 
 // These crashed the analyzer at some point.
 int between(char *x) {
   extern char start[];
   extern char end[];
   return x >= start && x < end;
 }
 
-int undef(void) {} // expected-warning{{control reaches end of non-void function}}
+int undef(void) {}
 void useUndef(void) { 0 || undef(); }
 
 void testPointer(void) { (void) (1 && testPointer && 0); }
+
+char *global_ap, *global_bp, *global_cp;
+void ambiguous_backtrack_1() {
+  for (;;) {
+    (global_bp - global_ap ? global_cp[global_bp - global_ap] : 0) || 1;
+    global_bp++;
+  }
+}
+
+int global_a, global_b;
+void ambiguous_backtrack_2(int x) {
+  global_a = x >= 2 ? 1 : x;
+  global_b == x && 9 || 2;
+}