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

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. (#GH100762)
+
 - 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.

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"
 
 //===----------------------------------------------------------------------===//

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; }

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:

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

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

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;
 }

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