r357325 - [analyzer] PR37501: Disable assertion for logical op short circuit evaluation.

[Artem Dergachev via cfe-commits]

Author: dergachev
Date: Fri Mar 29 15:43:34 2019
New Revision: 357325

URL: http://llvm.org/viewvc/llvm-project?rev=357325&view=rev
Log:
[analyzer] PR37501: Disable assertion for logical op short circuit evaluation.

The transfer function for the CFG element that represents a logical operation
computes the value of the operation and does nothing else. The element
appears after all the short circuit decisions were made, so they don't need
to be made again at this point.

Because our expression evaluation is imprecise, it is often hard to
discriminate between:

  (1) we don't know the value of the RHS because we failed to evaluate it

and

  (2) we don't know the value of the RHS because it didn't need to be evaluated.

This is hard because it depends on our knowledge about the value of the LHS
(eg., if LHS is true, then RHS in (LHS || RHS) doesn't need to be computed)
but LHS itself may have been evaluated imprecisely and we don't know whether
it is true or not. Additionally, the Analyzer wouldn't necessarily even remember
what the value of the LHS was because theoretically it's not really necessary
to know it for any future evaluations.

In order to work around these issues, the transfer function for logical
operations consists in looking at the ExplodedGraph we've constructed so far
in order to figure out from which CFG direction did we arrive here.
Such post-factum backtracking that doesn't involve looking up LHS and RHS values
is usually possible. However sometimes it fails because when we deduplicate
exploded nodes with the same program point and the same program state we may end
up in a situation when we reached the same program point from two or more
different directions.

By removing the assertion, we admit that the procedure indeed sometimes fails to
work. When it fails, we also admit that we don't know the value of the logical
operator.

Differential Revision: https://reviews.llvm.org/D59857

Modified:
    cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp
    cfe/trunk/test/Analysis/logical-ops.c

Modified: cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp?rev=357325&r1=357324&r2=357325&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp Fri Mar 29 15:43:34 2019
@@ -627,6 +627,21 @@ void ExprEngine::VisitDeclStmt(const Dec
 
 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);
 
@@ -648,10 +663,20 @@ void ExprEngine::VisitLogicalExpr(const
     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;

Modified: cfe/trunk/test/Analysis/logical-ops.c
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/logical-ops.c?rev=357325&r1=357324&r2=357325&view=diff
==============================================================================
--- cfe/trunk/test/Analysis/logical-ops.c (original)
+++ cfe/trunk/test/Analysis/logical-ops.c Fri Mar 29 15:43:34 2019
@@ -1,4 +1,5 @@
-// 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);
 
@@ -33,7 +34,21 @@ int between(char *x) {
   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;
+}