[clang] [clang][analyzer] Correct SMT Layer for _BitInt cases refutations (PR #143310)
via cfe-commits
cfe-commits at lists.llvm.org
Tue Jun 10 10:49:19 PDT 2025
https://github.com/vabridgers updated https://github.com/llvm/llvm-project/pull/143310
>From 4065ca6418831aba48e1d3147f67fa5bd01b7438 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] [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, SMT did not comprehend getting
a type by bitwidth that's not a power of 2. 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 | 27 ++++++++++++++++---
clang/test/Analysis/bitint-z3.c | 23 ++++++++++++++++
2 files changed, 47 insertions(+), 3 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..50c29a3a7f781 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -18,6 +18,8 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
#include "llvm/Support/SMTAPI.h"
+#include <algorithm>
+
namespace clang {
namespace ento {
@@ -570,23 +572,42 @@ class SMTConv {
// TODO: Refactor to put elsewhere
static inline QualType getAPSIntType(ASTContext &Ctx,
const llvm::APSInt &Int) {
- return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
+ QualType Ty = Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
+ // If Ty is Null, could be because the original type was a _BitInt.
+ // Get the bit size and round up to next power of 2, max char size
+ if (Ty.isNull()) {
+ unsigned CharTypeSize = Ctx.getTypeSize(Ctx.CharTy);
+ unsigned pow2DestWidth =
+ std::max(llvm::bit_ceil(Int.getBitWidth()), CharTypeSize);
+ Ty = Ctx.getIntTypeForBitwidth(pow2DestWidth, Int.isSigned());
+ }
+ return Ty;
+ }
+
+ 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/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 e1456623471769926fd00a4287a74b2112cf0320 Mon Sep 17 00:00:00 2001
From: einvbri <vince.a.bridgers at ericsson.com>
Date: Tue, 10 Jun 2025 19:47:03 +0200
Subject: [PATCH 2/2] Address review comments
---
.../StaticAnalyzer/Core/PathSensitive/SMTConv.h | 14 +++++++-------
1 file changed, 7 insertions(+), 7 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 50c29a3a7f781..8d0a82cb0984b 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -577,16 +577,16 @@ class SMTConv {
// Get the bit size and round up to next power of 2, max char size
if (Ty.isNull()) {
unsigned CharTypeSize = Ctx.getTypeSize(Ctx.CharTy);
- unsigned pow2DestWidth =
+ unsigned Pow2DestWidth =
std::max(llvm::bit_ceil(Int.getBitWidth()), CharTypeSize);
- Ty = Ctx.getIntTypeForBitwidth(pow2DestWidth, Int.isSigned());
+ Ty = Ctx.getIntTypeForBitwidth(Pow2DestWidth, Int.isSigned());
}
return Ty;
}
- static inline bool IsPower2(unsigned bits) {
- return bits > 0 && (bits & (bits - 1)) == 0;
- }
+ // 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>
@@ -601,8 +601,8 @@ 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()) {
- Ty = getAPSIntType(Ctx, Int);
+ } else if (!llvm::isPowerOf2_32(APSIntBitwidth) &&
+ !getAPSIntType(Ctx, Int).isNull()) {
NewInt = Int.extend(Ctx.getTypeSize(Ty));
} else
NewInt = Int;
More information about the cfe-commits
mailing list