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

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

clang/lib/StaticAnalyzer/Checkers/AssumeModeling.cpp

@@ -0,0 +1,86 @@
+//=== AssumeModeling.cpp --------------------------------------------------===//
+//
+// 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);
+  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

@@ -23,7 +23,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;
@@ -288,25 +287,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

@@ -8,6 +8,7 @@ add_clang_library(clangStaticAnalyzerCheckers
   AnalysisOrderChecker.cpp
   AnalyzerStatsChecker.cpp
   ArrayBoundChecker.cpp
+  AssumeModeling.cpp
   BasicObjCFoundationChecks.cpp
   BitwiseShiftChecker.cpp
   BlockInCriticalSectionChecker.cpp

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

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

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