[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

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@357325 91177308-0d34-0410-b5e6-96231b3b80d8

diff --git a/lib/StaticAnalyzer/Core/ExprEngineC.cpp b/lib/StaticAnalyzer/Core/ExprEngineC.cpp
index 11a3befcb1d99bca7b5f12def838f21ccc9c6441..df78b49130ceeac94aa981992bad36fb1004bc63 100644 (file)
--- a/lib/StaticAnalyzer/Core/ExprEngineC.cpp
+++ b/lib/StaticAnalyzer/Core/ExprEngineC.cpp
@@ -627,6 +627,21 @@ void ExprEngine::VisitDeclStmt(const DeclStmt *DS, ExplodedNode *Pred,
 
 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 BinaryOperator* B, ExplodedNode *Pred,
     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;

diff --git a/test/Analysis/logical-ops.c b/test/Analysis/logical-ops.c
index f839b1bf22bd690c642ac603780c5cb3dff43f58..c9ab7fcbe0214e4146e1f8e4fd02c83f83a09ac9 100644 (file)
--- a/test/Analysis/logical-ops.c
+++ b/test/Analysis/logical-ops.c
@@ -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;
+}