[analyzer] Sink execution if the assumption of [[assume]] is false

[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.

Depends on #116462

[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.

Depends on #116462

---

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

8 Files Affected:

• (modified) clang/docs/ReleaseNotes.rst (+2)
• (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 (-11)
• (modified) clang/test/Analysis/std-c-library-functions-arg-enabled-checkers.c (+1)

diff --git a/clang/docs/ReleaseNotes.rst b/clang/docs/ReleaseNotes.rst
index 5f91ff90634036..2f7f0c8a2affb5 100644
--- a/clang/docs/ReleaseNotes.rst
+++ b/clang/docs/ReleaseNotes.rst
@@ -1092,6 +1092,8 @@ New features
 
 - Now CSA models `__builtin_*_overflow` functions. (#GH102602)
 
+- Now CSA models `[[assume]]` attributes that have no side-effects. (#GH-TODO)
+
 - MallocChecker now checks for ``ownership_returns(class, idx)`` and ``ownership_takes(class, idx)``
   attributes with class names different from "malloc". Clang static analyzer now reports an error
   if class of allocation and deallocation function mismatches.
diff --git a/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td b/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
index b34e940682fc5e..c38219d1105848 100644
--- a/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
+++ b/clang/include/clang/StaticAnalyzer/Checkers/Checkers.td
@@ -380,7 +380,7 @@ def TrustReturnsNonnullChecker : Checker<"TrustReturnsNonnull">,
 } // end "apiModeling"
 
 //===----------------------------------------------------------------------===//
-// Evaluate "builtin" functions.
+// Evaluate "builtin" functions and assumptions.
 //===----------------------------------------------------------------------===//
 
 let ParentPackage = CoreBuiltin in {
@@ -394,6 +394,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 00000000000000..ca7dcec1d7ab4b
--- /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 cfdd3c9faa360a..fc4725868ad0ef 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 fcbe8b864b6e41..ba629fa6c6cbec 100644
--- a/clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt
+++ b/clang/lib/StaticAnalyzer/Checkers/CMakeLists.txt
@@ -9,6 +9,7 @@ add_clang_library(clangStaticAnalyzerCheckers
   AnalyzerStatsChecker.cpp
   ArrayBoundChecker.cpp
   ArrayBoundCheckerV2.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 160e35c77462d1..6e014a632cc029 100644
--- a/clang/test/Analysis/analyzer-enabled-checkers.c
+++ b/clang/test/Analysis/analyzer-enabled-checkers.c
@@ -23,6 +23,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 defcdeec282f61..31ce346c4119a7 100644
--- a/clang/test/Analysis/cxx23-assume-attribute.cpp
+++ b/clang/test/Analysis/cxx23-assume-attribute.cpp
@@ -27,32 +27,21 @@ 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;
 }
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 0910f030b0f072..1ea4af6c5064e4 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
@@ -31,6 +31,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