[analyzer] Sink false [[assume]] execution paths

[steakhal]

This PR splits the existing modeling of builtin assume from the BuiltinFunctionChecker.

We just sink the execution path if we are about to leave the assume expression with a false assumption.
Assumptions with side-effects are skipped, and ignored. Their values are "UnknownVal" anyway.

[llvmbot]

@llvm/pr-subscribers-clang

@llvm/pr-subscribers-clang-static-analyzer-1

Author: Balazs Benics (steakhal)

Changes

This PR splits the existing modeling of builtin assume from the BuiltinFunctionChecker.

We just sink the execution path if we are about to leave the assume expression with a false assumption.
Assumptions with side-effects are skipped, and ignored. Their values are "UnknownVal" anyway.

---

Full diff: https://github.com/llvm/llvm-project/pull/130418.diff

7 Files Affected:

• (modified) clang/include/clang/StaticAnalyzer/Checkers/Checkers.td (+5-1)
• (added) clang/lib/StaticAnalyzer/Checkers/AssumeModeling.cpp (+88)
• (modified) clang/lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp (+23-21)
• (modified) clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt (+1)
• (modified) clang/test/Analysis/analyzer-enabled-checkers.c (+1)
• (modified) clang/test/Analysis/cxx23-assume-attribute.cpp (+6-12)
• (modified) clang/test/Analysis/std-c-library-functions-arg-enabled-checkers.c (+1)

diff --git a/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td b/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
index c8895db914d13..07f5c0cf81d76 100644
--- a/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
+++ b/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
@@ -385,7 +385,7 @@ def TrustReturnsNonnullChecker : Checker<"TrustReturnsNonnull">,
 } // end "apiModeling"
 
 //===----------------------------------------------------------------------===//
-// Evaluate "builtin" functions.
+// Evaluate "builtin" functions and assumptions.
 //===----------------------------------------------------------------------===//
 
 let ParentPackage = CoreBuiltin in {
@@ -399,6 +399,10 @@ def BuiltinFunctionChecker : Checker<"BuiltinFunctions">,
   HelpText<"Evaluate compiler builtin functions (e.g., alloca())">,
   Documentation<NotDocumented>;
 
+def AssumeModeling : Checker<"AssumeModeling">,
+  HelpText<"Model compiler builtin assume functions and the assume attribute">,
+  Documentation<NotDocumented>;
+
 } // end "core.builtin"
 
 //===----------------------------------------------------------------------===//
diff --git a/clang/lib/StaticAnalyzer/Checkers/AssumeModeling.cpp b/clang/lib/StaticAnalyzer/Checkers/AssumeModeling.cpp
new file mode 100644
index 0000000000000..ca7dcec1d7ab4
--- /dev/null
+++ b/clang/lib/StaticAnalyzer/Checkers/AssumeModeling.cpp
@@ -0,0 +1,88 @@
+//=== AssumeModeling.cpp ----------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This checker evaluates the builting assume functions.
+// This checker also sinks execution paths leaving [[assume]] attributes with
+// false assumptions.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/AST/AttrIterator.h"
+#include "clang/Basic/Builtins.h"
+#include "clang/StaticAnalyzer/Checkers/BuiltinCheckerRegistration.h"
+#include "clang/StaticAnalyzer/Core/Checker.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
+#include "llvm/ADT/STLExtras.h"
+
+using namespace clang;
+using namespace ento;
+
+namespace {
+class AssumeModelingChecker
+    : public Checker<eval::Call, check::PostStmt<AttributedStmt>> {
+public:
+  void checkPostStmt(const AttributedStmt *A, CheckerContext &C) const;
+  bool evalCall(const CallEvent &Call, CheckerContext &C) const;
+};
+} // namespace
+
+void AssumeModelingChecker::checkPostStmt(const AttributedStmt *A,
+                                          CheckerContext &C) const {
+  if (!hasSpecificAttr<CXXAssumeAttr>(A->getAttrs()))
+    return;
+
+  for (const auto *Attr : getSpecificAttrs<CXXAssumeAttr>(A->getAttrs())) {
+    SVal AssumptionVal = C.getSVal(Attr->getAssumption());
+
+    // The assumption is not evaluated at all if it had sideffects; skip them.
+    if (AssumptionVal.isUnknown())
+      continue;
+
+    const auto *Assumption = AssumptionVal.getAsInteger();
+    assert(Assumption && "We should know the exact outcome of an assume expr");
+    if (Assumption && Assumption->isZero()) {
+      C.addSink();
+    }
+  }
+}
+
+bool AssumeModelingChecker::evalCall(const CallEvent &Call,
+                                     CheckerContext &C) const {
+  ProgramStateRef state = C.getState();
+  const auto *FD = dyn_cast_or_null<FunctionDecl>(Call.getDecl());
+  if (!FD)
+    return false;
+
+  if (!llvm::is_contained({Builtin::BI__builtin_assume, Builtin::BI__assume},
+                          FD->getBuiltinID())) {
+    return false;
+  }
+
+  assert(Call.getNumArgs() > 0);
+  SVal Arg = Call.getArgSVal(0);
+  if (Arg.isUndef())
+    return true; // Return true to model purity.
+
+  state = state->assume(Arg.castAs<DefinedOrUnknownSVal>(), true);
+  // FIXME: do we want to warn here? Not right now. The most reports might
+  // come from infeasible paths, thus being false positives.
+  if (!state) {
+    C.addSink();
+    return true;
+  }
+
+  C.addTransition(state);
+  return true;
+}
+
+void ento::registerAssumeModeling(CheckerManager &Mgr) {
+  Mgr.registerChecker<AssumeModelingChecker>();
+}
+
+bool ento::shouldRegisterAssumeModeling(const CheckerManager &) { return true; }
diff --git a/clang/lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp b/clang/lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
index cfdd3c9faa360..fc4725868ad0e 100644
--- a/clang/lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
@@ -14,6 +14,7 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include "clang/AST/AttrIterator.h"
 #include "clang/Basic/Builtins.h"
 #include "clang/StaticAnalyzer/Checkers/BuiltinCheckerRegistration.h"
 #include "clang/StaticAnalyzer/Checkers/Taint.h"
@@ -23,7 +24,6 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CheckerContext.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CheckerHelpers.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/DynamicExtent.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 
 using namespace clang;
@@ -91,8 +91,29 @@ QualType getOverflowBuiltinResultType(const CallEvent &Call, CheckerContext &C,
   }
 }
 
-class BuiltinFunctionChecker : public Checker<eval::Call> {
+class BuiltinFunctionChecker
+    : public Checker<eval::Call, check::PostStmt<AttributedStmt>> {
 public:
+  void checkPostStmt(const AttributedStmt *A, CheckerContext &C) const {
+    if (!hasSpecificAttr<CXXAssumeAttr>(A->getAttrs()))
+      return;
+
+    for (const auto *Attr : getSpecificAttrs<CXXAssumeAttr>(A->getAttrs())) {
+      SVal AssumptionVal = C.getSVal(Attr->getAssumption());
+
+      // The assumption is not evaluated at all if it had sideffects; skip them.
+      if (AssumptionVal.isUnknown())
+        continue;
+
+      const auto *Assumption = AssumptionVal.getAsInteger();
+      assert(Assumption &&
+             "We should know the exact outcome of an assume expr");
+      if (Assumption && Assumption->isZero()) {
+        C.addSink();
+      }
+    }
+  }
+
   bool evalCall(const CallEvent &Call, CheckerContext &C) const;
   void handleOverflowBuiltin(const CallEvent &Call, CheckerContext &C,
                              BinaryOperator::Opcode Op,
@@ -288,25 +309,6 @@ bool BuiltinFunctionChecker::evalCall(const CallEvent &Call,
     handleOverflowBuiltin(Call, C, BO_Add,
                           getOverflowBuiltinResultType(Call, C, BI));
     return true;
-  case Builtin::BI__builtin_assume:
-  case Builtin::BI__assume: {
-    assert (Call.getNumArgs() > 0);
-    SVal Arg = Call.getArgSVal(0);
-    if (Arg.isUndef())
-      return true; // Return true to model purity.
-
-    state = state->assume(Arg.castAs<DefinedOrUnknownSVal>(), true);
-    // FIXME: do we want to warn here? Not right now. The most reports might
-    // come from infeasible paths, thus being false positives.
-    if (!state) {
-      C.generateSink(C.getState(), C.getPredecessor());
-      return true;
-    }
-
-    C.addTransition(state);
-    return true;
-  }
-
   case Builtin::BI__builtin_unpredictable:
   case Builtin::BI__builtin_expect:
   case Builtin::BI__builtin_expect_with_probability:
diff --git a/clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt b/clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt
index 5910043440987..bafab8b19ee87 100644
--- a/clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt
+++ b/clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt
@@ -8,6 +8,7 @@ add_clang_library(clangStaticAnalyzerCheckers
   AnalysisOrderChecker.cpp
   AnalyzerStatsChecker.cpp
   ArrayBoundChecker.cpp
+  AssumeModeling.cpp
   BasicObjCFoundationChecks.cpp
   BitwiseShiftChecker.cpp
   BlockInCriticalSectionChecker.cpp
diff --git a/clang/test/Analysis/analyzer-enabled-checkers.c b/clang/test/Analysis/analyzer-enabled-checkers.c
index c70aeb21ab045..e5d0acb84a039 100644
--- a/clang/test/Analysis/analyzer-enabled-checkers.c
+++ b/clang/test/Analysis/analyzer-enabled-checkers.c
@@ -24,6 +24,7 @@
 // CHECK-NEXT: core.StackAddressEscape
 // CHECK-NEXT: core.UndefinedBinaryOperatorResult
 // CHECK-NEXT: core.VLASize
+// CHECK-NEXT: core.builtin.AssumeModeling
 // CHECK-NEXT: core.builtin.BuiltinFunctions
 // CHECK-NEXT: core.builtin.NoReturnFunctions
 // CHECK-NEXT: core.uninitialized.ArraySubscript
diff --git a/clang/test/Analysis/cxx23-assume-attribute.cpp b/clang/test/Analysis/cxx23-assume-attribute.cpp
index ee049af9f13aa..86e7662cd2af9 100644
--- a/clang/test/Analysis/cxx23-assume-attribute.cpp
+++ b/clang/test/Analysis/cxx23-assume-attribute.cpp
@@ -1,6 +1,7 @@
 // RUN: %clang_analyze_cc1 -std=c++23 -triple x86_64-pc-linux-gnu \
 // RUN:   -analyzer-checker=core,debug.ExprInspection -verify %s
 
+void clang_analyzer_warnIfReached();
 template <typename T> void clang_analyzer_dump(T);
 template <typename T> void clang_analyzer_value(T);
 
@@ -27,33 +28,22 @@ int ternary_in_builtin_assume(int a, int b) {
 
 // From: https://github.com/llvm/llvm-project/pull/116462#issuecomment-2517853226
 int ternary_in_assume(int a, int b) {
-  // FIXME notes
-  // Currently, if this test is run without the core.builtin.Builtin checker, the above function with the __builtin_assume behaves identically to the following test
-  // i.e. calls to `clang_analyzer_dump` result in "extraneous"  prints of the SVal(s) `reg<int b> ...`
-  // as opposed to 4 or 10
-  // which likely implies the Program State(s) did not get narrowed.
-  // A new checker is likely needed to be implemented to properly handle the expressions within `[[assume]]` to eliminate the states where `b` is not narrowed.
-
   [[assume(a > 10 ? b == 4 : b == 10)]];
   clang_analyzer_value(a);
   // expected-warning@-1 {{[-2147483648, 10]}}
   // expected-warning@-2 {{[11, 2147483647]}}
 
   clang_analyzer_dump(b); // expected-warning {{4}} expected-warning {{10}}
-  // expected-warning-re@-1 {{reg_${{[0-9]+}}<int b>}} FIXME: We shouldn't have this dump.
 
   if (a > 20) {
     clang_analyzer_dump(b + 100); // expected-warning {{104}}
-    // expected-warning-re@-1 {{(reg_${{[0-9]+}}<int b>) + 100}} FIXME: We shouldn't have this dump.
     return 2;
   }
   if (a > 10) {
     clang_analyzer_dump(b + 200); // expected-warning {{204}}
-    // expected-warning-re@-1 {{(reg_${{[0-9]+}}<int b>) + 200}} FIXME: We shouldn't have this dump.
     return 1;
   }
   clang_analyzer_dump(b + 300); // expected-warning {{310}}
-  // expected-warning-re@-1 {{(reg_${{[0-9]+}}<int b>) + 300}} FIXME: We shouldn't have this dump.
   return 0;
 }
 
@@ -70,8 +60,12 @@ int assume_and_fallthrough_at_the_same_attrstmt(int a, int b) {
       return b;
     }
   }
+
   // This code should be unreachable.
+  clang_analyzer_warnIfReached(); // expected-warning {{REACHABLE}}
+
   [[assume(false)]]; // This should definitely make it so.
-  clang_analyzer_dump(33); // expected-warning {{33 S32b}}
+  clang_analyzer_warnIfReached(); // no-warning
+
   return 0;
 }
diff --git a/clang/test/Analysis/std-c-library-functions-arg-enabled-checkers.c b/clang/test/Analysis/std-c-library-functions-arg-enabled-checkers.c
index faf0a8f19d919..d2900c6a42fff 100644
--- a/clang/test/Analysis/std-c-library-functions-arg-enabled-checkers.c
+++ b/clang/test/Analysis/std-c-library-functions-arg-enabled-checkers.c
@@ -32,6 +32,7 @@
 // CHECK-NEXT: core.StackAddressEscape
 // CHECK-NEXT: core.UndefinedBinaryOperatorResult
 // CHECK-NEXT: core.VLASize
+// CHECK-NEXT: core.builtin.AssumeModeling
 // CHECK-NEXT: core.builtin.BuiltinFunctions
 // CHECK-NEXT: core.builtin.NoReturnFunctions
 // CHECK-NEXT: core.uninitialized.ArraySubscript

[steakhal]

This patch should conclude the assume attribute modeling. After this, we would have some basic support for them.

[Xazax-hun]

I have one question once that is resolved the rest looks good to me.