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

[Artem Dergachev via Phabricator via cfe-commits]

NoQ created this revision.
NoQ added reviewers: dcoughlin, xazax.hun, a_sidorin, rnkovacs, mikhail.ramalho, Szelethus, baloghadamsoftware, Charusso, alexfh.
Herald added subscribers: cfe-commits, jdoerfert, dkrupp, donat.nagy, a.sidorin, szepet.
Herald added a project: clang.

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 `UnknownVal`s, 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.


Repository:
  rC Clang

https://reviews.llvm.org/D59857

Files:
  clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
  clang/test/Analysis/logical-ops.c


Index: clang/test/Analysis/logical-ops.c
===================================================================
--- clang/test/Analysis/logical-ops.c
+++ clang/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 @@
   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;
+}
Index: clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
+++ clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
@@ -627,6 +627,21 @@
 
 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 @@
     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;


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D59857.192390.patch
Type: text/x-patch
Size: 3217 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20190327/904ab8d6/attachment-0001.bin>