[clang] [analyzer] `canReasonAbout` does not support `nonloc::LazyCompoundVal` (PR #87521)

Andrew V. Teylu via cfe-commits cfe-commits at lists.llvm.org
Thu Apr 4 23:27:52 PDT 2024


https://github.com/aytey updated https://github.com/llvm/llvm-project/pull/87521

>From 1f70839ea1607f151c9f7eb390fcb974b32a54ca Mon Sep 17 00:00:00 2001
From: "Andrew V. Teylu" <andrew.teylu at vector.com>
Date: Wed, 3 Apr 2024 17:18:08 +0100
Subject: [PATCH 1/3] [analyzer] `canReasonAbout` does not support
 `nonloc::LazyCompoundVal`

This PR makes two modifications to the {Simple, Range} constraint managers:

* `nonloc::LazyCompoundVal` is now explicitly not able to be reasoned about; and

* When we have something that cannot be reasoned about, we return an unmodified state (and do not attempt to simplify)

For the added test-case, testing under `main` will either hit an `llvm_unreachable` (or go off the rails for other reasons). After this change, the test-case passes successfully.

The change stating "Non-integer types are not supported" for `nonloc::LazyCompoundVal` follows the same logic inside of `RangedConstraintManager::assumeSymUnsupported`. However, when a `nonloc::LazyCompoundVal`, we don't want to call `RangedConstraintManager::assumeSymUnsupported` because this will attempt to work with the `Sym` or `State` in a way that isn't compatible with a `nonloc::LazyCompoundVal`.
---
 .../Core/RangeConstraintManager.cpp             |  4 ++++
 .../Core/SimpleConstraintManager.cpp            | 10 +++++++---
 clang/test/Analysis/non_loc_compound.cpp        | 17 +++++++++++++++++
 3 files changed, 28 insertions(+), 3 deletions(-)
 create mode 100644 clang/test/Analysis/non_loc_compound.cpp

diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index c6f87b45ab887a..1f3e5711bcc71c 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -2836,6 +2836,10 @@ bool RangeConstraintManager::canReasonAbout(SVal X) const {
     return false;
   }
 
+  // Non-integer types are not supported.
+  if (X.getAs<nonloc::LazyCompoundVal>())
+    return false;
+
   return true;
 }
 
diff --git a/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index 8ca2cdb9d3ab7a..b84a68ab93ef90 100644
--- a/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -57,10 +57,14 @@ ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
   // We cannot reason about SymSymExprs, and can only reason about some
   // SymIntExprs.
   if (!canReasonAbout(Cond)) {
-    // Just add the constraint to the expression without trying to simplify.
     SymbolRef Sym = Cond.getAsSymbol();
-    assert(Sym);
-    return assumeSymUnsupported(State, Sym, Assumption);
+    if (Sym) {
+      // this will simplify the symbol, so only call this if we have a
+      // symbol.
+      return assumeSymUnsupported(State, Sym, Assumption);
+    } else {
+      return State;
+    }
   }
 
   switch (Cond.getKind()) {
diff --git a/clang/test/Analysis/non_loc_compound.cpp b/clang/test/Analysis/non_loc_compound.cpp
new file mode 100644
index 00000000000000..b76ecb8d56635c
--- /dev/null
+++ b/clang/test/Analysis/non_loc_compound.cpp
@@ -0,0 +1,17 @@
+// REQUIRES: crash-recovery, asserts
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=alpha.cplusplus.InvalidatedIterator \
+// RUN:   -analyzer-config aggressive-binary-operation-simplification=true \
+// RUN:   2>&1
+
+struct node {};
+struct prop : node {};
+struct bitvec : node {
+  prop operator==(bitvec) { return prop(); }
+  bitvec extend(); // { return *this; }
+};
+void convert() {
+  bitvec input;
+  bitvec output(input.extend());
+  output == input;
+}

>From 9f552209d9ce9bbddca247a46f79b331388908bf Mon Sep 17 00:00:00 2001
From: "Andrew V. Teylu" <andrew.teylu at vector.com>
Date: Wed, 3 Apr 2024 17:18:08 +0100
Subject: [PATCH 2/3] [analyzer] `canReasonAbout` does not support
 `nonloc::LazyCompoundVal`

This PR makes two modifications to the {Simple, Range} constraint managers:

* `nonloc::LazyCompoundVal` is now explicitly not able to be reasoned about; and

* When we have something that cannot be reasoned about, we return an unmodified state (and do not attempt to simplify)

For the added test-case, testing under `main` will either hit an `llvm_unreachable` (or go off the rails for other reasons). After this change, the test-case passes successfully.

The change stating "Non-integer types are not supported" for `nonloc::LazyCompoundVal` follows the same logic inside of `RangedConstraintManager::assumeSymUnsupported`. However, when a `nonloc::LazyCompoundVal`, we don't want to call `RangedConstraintManager::assumeSymUnsupported` because this will attempt to work with the `Sym` or `State` in a way that isn't compatible with a `nonloc::LazyCompoundVal`.
---
 .../Core/RangeConstraintManager.cpp             |  4 ++++
 .../Core/SimpleConstraintManager.cpp            | 10 +++++++---
 clang/test/Analysis/non_loc_compound.cpp        | 17 +++++++++++++++++
 3 files changed, 28 insertions(+), 3 deletions(-)
 create mode 100644 clang/test/Analysis/non_loc_compound.cpp

diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index c6f87b45ab887a..1f3e5711bcc71c 100644
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -2836,6 +2836,10 @@ bool RangeConstraintManager::canReasonAbout(SVal X) const {
     return false;
   }
 
+  // Non-integer types are not supported.
+  if (X.getAs<nonloc::LazyCompoundVal>())
+    return false;
+
   return true;
 }
 
diff --git a/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index 8ca2cdb9d3ab7a..b84a68ab93ef90 100644
--- a/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -57,10 +57,14 @@ ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
   // We cannot reason about SymSymExprs, and can only reason about some
   // SymIntExprs.
   if (!canReasonAbout(Cond)) {
-    // Just add the constraint to the expression without trying to simplify.
     SymbolRef Sym = Cond.getAsSymbol();
-    assert(Sym);
-    return assumeSymUnsupported(State, Sym, Assumption);
+    if (Sym) {
+      // this will simplify the symbol, so only call this if we have a
+      // symbol.
+      return assumeSymUnsupported(State, Sym, Assumption);
+    } else {
+      return State;
+    }
   }
 
   switch (Cond.getKind()) {
diff --git a/clang/test/Analysis/non_loc_compound.cpp b/clang/test/Analysis/non_loc_compound.cpp
new file mode 100644
index 00000000000000..b76ecb8d56635c
--- /dev/null
+++ b/clang/test/Analysis/non_loc_compound.cpp
@@ -0,0 +1,17 @@
+// REQUIRES: crash-recovery, asserts
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=alpha.cplusplus.InvalidatedIterator \
+// RUN:   -analyzer-config aggressive-binary-operation-simplification=true \
+// RUN:   2>&1
+
+struct node {};
+struct prop : node {};
+struct bitvec : node {
+  prop operator==(bitvec) { return prop(); }
+  bitvec extend(); // { return *this; }
+};
+void convert() {
+  bitvec input;
+  bitvec output(input.extend());
+  output == input;
+}

>From f96dcf1b327a55fde0edd0c12e3120c82d563455 Mon Sep 17 00:00:00 2001
From: "Andrew V. Teylu" <andrew.teylu at vector.com>
Date: Fri, 5 Apr 2024 07:27:41 +0100
Subject: [PATCH 3/3] Remove 'REQUIRES' line

---
 clang/test/Analysis/non_loc_compound.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/clang/test/Analysis/non_loc_compound.cpp b/clang/test/Analysis/non_loc_compound.cpp
index b76ecb8d56635c..9b7b50e6fd8c9c 100644
--- a/clang/test/Analysis/non_loc_compound.cpp
+++ b/clang/test/Analysis/non_loc_compound.cpp
@@ -1,4 +1,3 @@
-// REQUIRES: crash-recovery, asserts
 // RUN: %clang_analyze_cc1 %s \
 // RUN:   -analyzer-checker=alpha.cplusplus.InvalidatedIterator \
 // RUN:   -analyzer-config aggressive-binary-operation-simplification=true \



More information about the cfe-commits mailing list