[clang] [clang][analyzer] Correct SMT Layer for _BitInt cases refutations (PR #143310)
via cfe-commits
cfe-commits at lists.llvm.org
Sun Jun 8 09:38:44 PDT 2025
https://github.com/vabridgers updated https://github.com/llvm/llvm-project/pull/143310
>From 4b86a568caa5e18b66e3e76825d4db6db195dfd5 Mon Sep 17 00:00:00 2001
From: Vince Bridgers <vince.a.bridgers at ericsson.com>
Date: Sun, 8 Jun 2025 15:48:04 +0200
Subject: [PATCH 1/2] [clang][analyzer] Correct SMT Layer for _BitInt cases
refutations
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Since _BitInt was added later, ASTContext did not comprehend getting
a type by bitwidth that's not a power of 2, and the SMT layer also
did not comprehend this. This led to unexpected crashes using Z3
refutation during randomized testing. The assertion and redacted and
summarized crash stack is shown here.
clang: ../../clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:103:
static llvm::SMTExprRef clang::ento::SMTConv::fromBinOp(llvm::SMTSolverRef &,
const llvm::SMTExprRef &, const BinaryOperator::Opcode, const llvm::SMTExprRef &, bool):
Assertion `*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must have the same sort!"' failed.
...
#9 <address> clang::ento::SMTConv::fromBinOp(std::shared_ptr<llvm::SMTSolver>&,
llvm::SMTExpr const* const&, clang::BinaryOperatorKind, llvm::SMTExpr const* const&,
bool) SMTConstraintManager.cpp
clang::ASTContext&, llvm::SMTExpr const* const&, clang::QualType,
clang::BinaryOperatorKind, llvm::SMTExpr const* const&, clang::QualType,
clang::QualType*) SMTConstraintManager.cpp
clang::ASTContext&, clang::ento::SymExpr const*, llvm::APSInt const&,
llvm::APSInt const&, bool) SMTConstraintManager.cpp
clang::ento::ExplodedNode const*, clang::ento::PathSensitiveBugReport&)
---
.../Core/PathSensitive/SMTConv.h | 14 +++++++++--
clang/lib/AST/ASTContext.cpp | 9 ++++++--
clang/test/Analysis/bitint-z3.c | 23 +++++++++++++++++++
3 files changed, 42 insertions(+), 4 deletions(-)
create mode 100644 clang/test/Analysis/bitint-z3.c
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 580b49a38dc72..2a41202d46440 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -573,20 +573,30 @@ class SMTConv {
return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
}
+ static inline bool IsPower2(unsigned bits) {
+ return bits > 0 && (bits & (bits-1)) == 0;
+ }
+
// Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
static inline std::pair<llvm::APSInt, QualType>
fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int) {
llvm::APSInt NewInt;
+ unsigned APSIntBitwidth = Int.getBitWidth();
+ QualType Ty = getAPSIntType(Ctx, Int);
// FIXME: This should be a cast from a 1-bit integer type to a boolean type,
// but the former is not available in Clang. Instead, extend the APSInt
// directly.
- if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) {
+ if (APSIntBitwidth == 1 && Ty.isNull()) {
NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
+ Ty = getAPSIntType(Ctx, NewInt);
+ } else if ( !IsPower2(APSIntBitwidth) && !getAPSIntType(Ctx, Int).isNull()) {
+ Ty = getAPSIntType(Ctx, Int);
+ NewInt = Int.extend( Ctx.getTypeSize(Ty));
} else
NewInt = Int;
- return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
+ return std::make_pair(NewInt, Ty);
}
// Perform implicit type conversion on binary symbolic expressions.
diff --git a/clang/lib/AST/ASTContext.cpp b/clang/lib/AST/ASTContext.cpp
index 45f9602856840..094264813a8b3 100644
--- a/clang/lib/AST/ASTContext.cpp
+++ b/clang/lib/AST/ASTContext.cpp
@@ -13209,9 +13209,14 @@ size_t ASTContext::getSideTableAllocatedMemory() const {
/// Returns empty type if there is no appropriate target types.
QualType ASTContext::getIntTypeForBitwidth(unsigned DestWidth,
unsigned Signed) const {
- TargetInfo::IntType Ty = getTargetInfo().getIntTypeByWidth(DestWidth, Signed);
+ // round up to next power of 2 for _BitInt cases
+ unsigned pow2DestWidth = llvm::bit_ceil(DestWidth);
+ //if (pow2DestWidth == 4) pow2DestWidth = 8;
+ if (pow2DestWidth < 8) pow2DestWidth = 8;
+
+ TargetInfo::IntType Ty = getTargetInfo().getIntTypeByWidth(pow2DestWidth, Signed);
CanQualType QualTy = getFromTargetType(Ty);
- if (!QualTy && DestWidth == 128)
+ if (!QualTy && pow2DestWidth == 128)
return Signed ? Int128Ty : UnsignedInt128Ty;
return QualTy;
}
diff --git a/clang/test/Analysis/bitint-z3.c b/clang/test/Analysis/bitint-z3.c
new file mode 100644
index 0000000000000..d50c93acdf117
--- /dev/null
+++ b/clang/test/Analysis/bitint-z3.c
@@ -0,0 +1,23 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core -w -DNO_CROSSCHECK -verify %s
+// RUN: %clang_cc1 -analyze -analyzer-checker=core -w -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+// The SMTConv layer did not comprehend _BitInt types (because this was an
+// evolved feature) and was crashing due to needed updates in 2 places.
+// Analysis is expected to find these cases using _BitInt without crashing.
+
+_BitInt(35) a;
+int b;
+void c() {
+ int d;
+ if (a)
+ b = d; // expected-warning{{Assigned value is uninitialized [core.uninitialized.Assign]}}
+}
+
+int *d;
+_BitInt(3) e;
+void f() {
+ int g;
+ d = &g;
+ e ?: 0; // expected-warning{{Address of stack memory associated with local variable 'g' is still referred to by the global variable 'd' upon returning to the caller. This will be a dangling reference [core.StackAddressEscape]}}
+}
>From 8b2238f4c7fa282785464daf15a3a08c8db3fd19 Mon Sep 17 00:00:00 2001
From: einvbri <vince.a.bridgers at ericsson.com>
Date: Sun, 8 Jun 2025 18:36:56 +0200
Subject: [PATCH 2/2] [clang][analyzer] Correct SMT Layer for _BitInt cases
refutations
Correct clang-format issues
---
.../clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h | 6 +++---
clang/lib/AST/ASTContext.cpp | 8 +++++---
2 files changed, 8 insertions(+), 6 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 2a41202d46440..f2ae6f0e9b48a 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -574,7 +574,7 @@ class SMTConv {
}
static inline bool IsPower2(unsigned bits) {
- return bits > 0 && (bits & (bits-1)) == 0;
+ return bits > 0 && (bits & (bits - 1)) == 0;
}
// Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
@@ -590,9 +590,9 @@ class SMTConv {
if (APSIntBitwidth == 1 && Ty.isNull()) {
NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
Ty = getAPSIntType(Ctx, NewInt);
- } else if ( !IsPower2(APSIntBitwidth) && !getAPSIntType(Ctx, Int).isNull()) {
+ } else if (!IsPower2(APSIntBitwidth) && !getAPSIntType(Ctx, Int).isNull()) {
Ty = getAPSIntType(Ctx, Int);
- NewInt = Int.extend( Ctx.getTypeSize(Ty));
+ NewInt = Int.extend(Ctx.getTypeSize(Ty));
} else
NewInt = Int;
diff --git a/clang/lib/AST/ASTContext.cpp b/clang/lib/AST/ASTContext.cpp
index 094264813a8b3..4f0849647c542 100644
--- a/clang/lib/AST/ASTContext.cpp
+++ b/clang/lib/AST/ASTContext.cpp
@@ -13211,10 +13211,12 @@ QualType ASTContext::getIntTypeForBitwidth(unsigned DestWidth,
unsigned Signed) const {
// round up to next power of 2 for _BitInt cases
unsigned pow2DestWidth = llvm::bit_ceil(DestWidth);
- //if (pow2DestWidth == 4) pow2DestWidth = 8;
- if (pow2DestWidth < 8) pow2DestWidth = 8;
+ // if (pow2DestWidth == 4) pow2DestWidth = 8;
+ if (pow2DestWidth < 8)
+ pow2DestWidth = 8;
- TargetInfo::IntType Ty = getTargetInfo().getIntTypeByWidth(pow2DestWidth, Signed);
+ TargetInfo::IntType Ty =
+ getTargetInfo().getIntTypeByWidth(pow2DestWidth, Signed);
CanQualType QualTy = getFromTargetType(Ty);
if (!QualTy && pow2DestWidth == 128)
return Signed ? Int128Ty : UnsignedInt128Ty;
More information about the cfe-commits
mailing list