[PATCH] D159355: [clang][dataflow] Unsoundly treat "Unknown" as "Equivalent" in widening.

[Yitzhak Mandelbaum via Phabricator via cfe-commits]

ymandel created this revision.
ymandel added reviewers: xazax.hun, gribozavr2, mboehme.
Herald added a subscriber: martong.
Herald added a reviewer: NoQ.
Herald added a project: All.
ymandel requested review of this revision.
Herald added a project: clang.

This change makes widening act the same as equivalence checking. When the
analysis does not provide an answer regarding the equivalence of two distinct
values, the framework treats them as equivalent. This is an unsound choice that
enables convergence.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D159355

Files:
  clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
  clang/unittests/Analysis/FlowSensitive/TransferTest.cpp


Index: clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
@@ -3843,10 +3843,7 @@
       }
     }
   )cc";
-  // FIXME: Implement pointer value widening to make analysis converge.
-  ASSERT_THAT_ERROR(
-      checkDataflowWithNoopAnalysis(Code),
-      llvm::FailedWithMessage("maximum number of iterations reached"));
+  ASSERT_THAT_ERROR(checkDataflowWithNoopAnalysis(Code), llvm::Succeeded());
 }
 
 TEST(TransferTest, LoopDereferencingChangingRecordPointerConverges) {
@@ -3868,10 +3865,7 @@
       }
     }
   )cc";
-  // FIXME: Implement pointer value widening to make analysis converge.
-  ASSERT_THAT_ERROR(
-      checkDataflowWithNoopAnalysis(Code),
-      llvm::FailedWithMessage("maximum number of iterations reached"));
+  ASSERT_THAT_ERROR(checkDataflowWithNoopAnalysis(Code), llvm::Succeeded());
 }
 
 TEST(TransferTest, DoesNotCrashOnUnionThisExpr) {
Index: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -22,10 +22,8 @@
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/MapVector.h"
 #include "llvm/ADT/STLExtras.h"
-#include "llvm/Support/Casting.h"
 #include "llvm/Support/ErrorHandling.h"
 #include <cassert>
-#include <memory>
 #include <utility>
 
 namespace clang {
@@ -50,6 +48,23 @@
   return Result;
 }
 
+// Whether to consider equivalent two values with an unknown relation.
+//
+// FIXME: this function is a hook that enable unsoundness in support of
+// convergence. Once we have widening support for the reference/pointer and
+// struct built-in models, this should be unconditionally `false` (and inlined
+// as such at its call sites)
+static bool equateUnknownValues(Value::Kind K) {
+  switch (K) {
+  case Value::Kind::Integer:
+  case Value::Kind::Pointer:
+  case Value::Kind::Record:
+    return true;
+  default:
+    return false;
+  }
+}
+
 static bool compareDistinctValues(QualType Type, Value &Val1,
                                   const Environment &Env1, Value &Val2,
                                   const Environment &Env2,
@@ -66,18 +81,7 @@
   case ComparisonResult::Different:
     return false;
   case ComparisonResult::Unknown:
-    switch (Val1.getKind()) {
-    case Value::Kind::Integer:
-    case Value::Kind::Pointer:
-    case Value::Kind::Record:
-      // FIXME: this choice intentionally introduces unsoundness to allow
-      // for convergence. Once we have widening support for the
-      // reference/pointer and struct built-in models, this should be
-      // `false`.
-      return true;
-    default:
-      return false;
-    }
+    return equateUnknownValues(Val1.getKind());
   }
   llvm_unreachable("All cases covered in switch");
 }
@@ -167,8 +171,7 @@
   if (auto *W = Model.widen(Type, Prev, PrevEnv, Current, CurrentEnv))
     return *W;
 
-  // Default of widening is a no-op: leave the current value unchanged.
-  return Current;
+  return equateUnknownValues(Prev.getKind()) ? Prev : Current;
 }
 
 // Returns whether the values in `Map1` and `Map2` compare equal for those


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D159355.555350.patch
Type: text/x-patch
Size: 3359 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20230901/4555bb89/attachment.bin>