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.bridg...@ericsson.com>
Date: Sun, 8 Jun 2025 15:48:04 +0200
Subject: [PATCH] [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]}}
+}
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
