[clang] [analyzer] Model [[assume]] attributes without side-effects (PR #120572)
Balazs Benics via cfe-commits
cfe-commits at lists.llvm.org
Thu Dec 19 04:52:29 PST 2024
https://github.com/steakhal created https://github.com/llvm/llvm-project/pull/120572
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
>From 097d7feb474e7eca884730dc8eebbb8b1bdef2e1 Mon Sep 17 00:00:00 2001
From: Balazs Benics <benicsbalazs at gmail.com>
Date: Thu, 19 Dec 2024 13:45:58 +0100
Subject: [PATCH] [analyzer] Model [[assume]] attributes without side-ffects
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
---
clang/docs/ReleaseNotes.rst | 2 +
.../clang/StaticAnalyzer/Checkers/Checkers.td | 6 +-
.../Checkers/AssumeModeling.cpp | 88 +++++++++++++++++++
.../Checkers/BuiltinFunctionChecker.cpp | 44 +++++-----
.../StaticAnalyzer/Checkers/CMakeLists.txt | 1 +
.../test/Analysis/analyzer-enabled-checkers.c | 1 +
.../test/Analysis/cxx23-assume-attribute.cpp | 11 ---
...c-library-functions-arg-enabled-checkers.c | 1 +
8 files changed, 121 insertions(+), 33 deletions(-)
create mode 100644 clang/lib/StaticAnalyzer/Checkers/AssumeModeling.cpp
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 at -1 {{[-2147483648, 10]}}
// expected-warning at -2 {{[11, 2147483647]}}
clang_analyzer_dump(b); // expected-warning {{4}} expected-warning {{10}}
- // expected-warning-re at -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 at -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 at -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 at -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
More information about the cfe-commits
mailing list