[clang] [llvm] [analyzer] Fix _BitInt support & casting behavior for Z3 symbolic execution (PR #210525)
via cfe-commits
cfe-commits at lists.llvm.org
Sun Jul 19 02:28:20 PDT 2026
https://github.com/rdevshp updated https://github.com/llvm/llvm-project/pull/210525
>From 8face7c8dcf8daed79d53d520a072b87fdd3c28c Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Sat, 18 Jul 2026 16:05:37 +0000
Subject: [PATCH 1/4] [analyzer] Fix _BitInt support & casting behavior for Z3
symbolic execution
Forces symbolic cast to be enabled for
z3 symbolic execution, and switches away from
Ctx.getTypeSize for getting the bit width of
integral types.
Assisted-by: Codex
---
.../StaticAnalyzer/Core/AnalyzerOptions.h | 5 ++
.../Core/PathSensitive/SMTConstraintManager.h | 2 +-
.../Core/PathSensitive/SMTConv.h | 55 ++++++-------------
clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp | 8 +--
clang/lib/StaticAnalyzer/Core/SValBuilder.cpp | 2 +-
clang/test/Analysis/z3/z3-bitint-arithmetic.c | 36 ++++++++++++
clang/test/Analysis/z3/z3-logicalexpr-eval.c | 4 ++
llvm/lib/Support/Z3Solver.cpp | 15 ++---
8 files changed, 72 insertions(+), 55 deletions(-)
create mode 100644 clang/test/Analysis/z3/z3-bitint-arithmetic.c
diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
index f0fa68008fc4d..f136f7beda3a5 100644
--- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
+++ b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
@@ -391,6 +391,11 @@ class AnalyzerOptions {
ExplorationStrategyKind getExplorationStrategy() const;
CTUPhase1InliningKind getCTUPhase1Inlining() const;
+ bool analyzerSymbolicIntegerCasts() const {
+ return ShouldSupportSymbolicIntegerCasts ||
+ AnalysisConstraintsOpt == Z3ConstraintsModel;
+ }
+
/// Returns the inter-procedural analysis mode.
IPAKind getIPAMode() const;
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index 88902aeddb96e..14c8411f24a1b 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -128,7 +128,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
QualType Ty = Sym->getType();
assert(!Ty->isRealFloatingType());
- llvm::APSInt Value(Ctx.getTypeSize(Ty),
+ llvm::APSInt Value(SMTConv::getSMTBitWidth(Ctx, Ty),
!Ty->isSignedIntegerOrEnumerationType());
// TODO: this should call checkModel so we can use the cache, however,
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index a494177372b6e..4ba0483dc0380 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -25,6 +25,12 @@ namespace ento {
class SMTConv {
public:
+ static inline uint64_t getSMTBitWidth(ASTContext &Ctx, QualType Ty) {
+ if (Ty->isIntegralOrEnumerationType())
+ return Ctx.getIntWidth(Ty);
+ return Ctx.getTypeSize(Ty);
+ }
+
// Returns an appropriate sort, given a QualType and it's bit width.
static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver,
const QualType &Ty, unsigned BitWidth) {
@@ -325,7 +331,7 @@ class SMTConv {
fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym) {
const SymbolID ID = Sym->getSymbolID();
const QualType Ty = Sym->getType();
- const uint64_t BitWidth = Ctx.getTypeSize(Ty);
+ const uint64_t BitWidth = SMTConv::getSMTBitWidth(Ctx, Ty);
llvm::SmallString<16> Str;
llvm::raw_svector_ostream OS(Str);
@@ -338,8 +344,8 @@ class SMTConv {
ASTContext &Ctx,
const llvm::SMTExprRef &Exp,
QualType FromTy, QualType ToTy) {
- return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
- Ctx.getTypeSize(FromTy));
+ return fromCast(Solver, Exp, ToTy, SMTConv::getSMTBitWidth(Ctx, ToTy),
+ FromTy, SMTConv::getSMTBitWidth(Ctx, FromTy));
}
static inline std::optional<llvm::SMTExprRef>
@@ -358,7 +364,7 @@ class SMTConv {
Ty->isBlockPointerType() || Ty->isReferenceType())
return fromBinOp(Solver, Exp, BO_NE,
Solver->mkBitvector(llvm::APSInt::getUnsigned(0),
- Ctx.getTypeSize(Ty)),
+ SMTConv::getSMTBitWidth(Ctx, Ty)),
Ty->isSignedIntegerOrEnumerationType());
assert(false && "Unsupported type for boolean conversion!");
return std::nullopt;
@@ -568,10 +574,10 @@ class SMTConv {
if (Ty->isBooleanType())
return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
- return fromBinOp(
- Solver, Exp, Assumption ? BO_EQ : BO_NE,
- Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
- isSigned);
+ return fromBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
+ Solver->mkBitvector(llvm::APSInt("0"),
+ SMTConv::getSMTBitWidth(Ctx, Ty)),
+ isSigned);
}
llvm_unreachable("Unsupported type for zero value!");
@@ -627,38 +633,13 @@ class SMTConv {
// TODO: Refactor to put elsewhere
static inline QualType getAPSIntType(ASTContext &Ctx,
const llvm::APSInt &Int) {
- const QualType Ty =
- Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
- if (!Ty.isNull())
- return Ty;
- // If Ty is Null, could be because the original type was a _BitInt.
- // Get the size of the _BitInt type (expressed in bits) and round it up to
- // the next power of 2 that is at least the bit size of 'char' (usually 8).
- unsigned CharTypeSize = Ctx.getTypeSize(Ctx.CharTy);
- unsigned Pow2DestWidth =
- std::max(llvm::bit_ceil(Int.getBitWidth()), CharTypeSize);
- return Ctx.getIntTypeForBitwidth(Pow2DestWidth, Int.isSigned());
+ return Ctx.getBitIntType(Int.isUnsigned(), Int.getBitWidth());
}
// 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 (APSIntBitwidth == 1 && Ty.isNull())
- return {Int.extend(Ctx.getTypeSize(Ctx.BoolTy)),
- getAPSIntType(Ctx, NewInt)};
- else if (APSIntBitwidth == 1 && !Ty.isNull())
- return {Int.extend(Ctx.getTypeSize(getAPSIntType(Ctx, Int))),
- getAPSIntType(Ctx, NewInt)};
- if (llvm::isPowerOf2_32(APSIntBitwidth) || Ty.isNull())
- return {Int, Ty};
- return {Int.extend(Ctx.getTypeSize(Ty)), Ty};
+ return {Int, getAPSIntType(Ctx, Int)};
}
// Perform implicit type conversion on binary symbolic expressions.
@@ -744,8 +725,8 @@ class SMTConv {
static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver,
ASTContext &Ctx, T &LHS, QualType <y,
T &RHS, QualType &RTy) {
- uint64_t LBitWidth = Ctx.getTypeSize(LTy);
- uint64_t RBitWidth = Ctx.getTypeSize(RTy);
+ uint64_t LBitWidth = SMTConv::getSMTBitWidth(Ctx, LTy);
+ uint64_t RBitWidth = SMTConv::getSMTBitWidth(Ctx, RTy);
assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
// Always perform integer promotion before checking type equality.
diff --git a/clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp b/clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
index 33c31fe10782a..ab36295f53f85 100644
--- a/clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
+++ b/clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp
@@ -411,7 +411,7 @@ void ExprEngine::VisitCast(const CastExpr *CastE, const Expr *Ex,
case CK_IntegralCast: {
// Delegate to SValBuilder to process.
SVal V = state->getSVal(Ex, SF);
- if (AMgr.options.ShouldSupportSymbolicIntegerCasts)
+ if (AMgr.options.analyzerSymbolicIntegerCasts())
V = svalBuilder.evalCast(V, T, ExTy);
else
V = svalBuilder.evalIntegralCast(state, V, T, ExTy);
@@ -729,10 +729,8 @@ void ExprEngine::VisitLogicalExpr(const BinaryOperator* B, ExplodedNode *Pred,
// We evaluate "RHSVal != 0" expression which result in 0 if the value is
// known to be false, 1 if the value is known to be true and a new symbol
// when the assumption is unknown.
- nonloc::ConcreteInt Zero(getBasicVals().getValue(0, B->getType()));
- X = evalBinOp(N->getState(), BO_NE,
- svalBuilder.evalCast(RHSVal, B->getType(), RHS->getType()),
- Zero, B->getType());
+ X = evalBinOp(N->getState(), BO_NE, RHSVal,
+ svalBuilder.makeZeroVal(RHS->getType()), B->getType());
}
}
Bldr.generateNode(B, Pred, state->BindExpr(B, Pred->getStackFrame(), X));
diff --git a/clang/lib/StaticAnalyzer/Core/SValBuilder.cpp b/clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
index e816cb2aec4d3..57c97b2852445 100644
--- a/clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
+++ b/clang/lib/StaticAnalyzer/Core/SValBuilder.cpp
@@ -977,7 +977,7 @@ class EvalCastVisitor : public SValVisitor<EvalCastVisitor, SVal> {
.getAnalyzerOptions();
// If appropriate option is disabled, ignore the cast.
// NOTE: ShouldSupportSymbolicIntegerCasts is `false` by default.
- if (!Opts.ShouldSupportSymbolicIntegerCasts)
+ if (!Opts.analyzerSymbolicIntegerCasts())
return V;
return simplifySymbolCast(V, CastTy);
}
diff --git a/clang/test/Analysis/z3/z3-bitint-arithmetic.c b/clang/test/Analysis/z3/z3-bitint-arithmetic.c
new file mode 100644
index 0000000000000..e3d3084cc2b5c
--- /dev/null
+++ b/clang/test/Analysis/z3/z3-bitint-arithmetic.c
@@ -0,0 +1,36 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN: -analyzer-constraints=unsupported-z3 -verify %s
+// REQUIRES: z3
+
+void clang_analyzer_eval(int);
+
+void unsigned_bitint_8_wrap_equivalence(unsigned _BitInt(8) x) {
+ clang_analyzer_eval( // expected-warning{{TRUE}}
+ (x + (unsigned _BitInt(8))1 == 0) ==
+ (x == (unsigned _BitInt(8))255));
+}
+
+void unsigned_bitint_35_wrap_equivalence(unsigned _BitInt(35) x) {
+ clang_analyzer_eval( // expected-warning{{TRUE}}
+ (x + 1 == 0) ==
+ (x == (unsigned _BitInt(35))0x7ffffffffULL));
+}
+
+void unsigned_bitint_63_wrap_equivalence(unsigned _BitInt(63) x) {
+ // Addition wraps modulo 2^63, so these two conditions are equivalent.
+ clang_analyzer_eval( // expected-warning{{TRUE}}
+ (x + 1 == 0) ==
+ (x == (unsigned _BitInt(63))0x7fffffffffffffffULL));
+}
+
+void unsigned_bitint_256_wrap_equivalence(unsigned _BitInt(256) x) {
+ clang_analyzer_eval( // expected-warning{{TRUE}}
+ (x + 1 == 0) ==
+ (x == ~(unsigned _BitInt(256))0));
+}
+
+void unsigned_bitint_widening_cast(unsigned _BitInt(35) x) {
+ clang_analyzer_eval( // expected-warning{{TRUE}}
+ (unsigned _BitInt(63))x <=
+ (unsigned _BitInt(63))0x7ffffffffULL);
+}
diff --git a/clang/test/Analysis/z3/z3-logicalexpr-eval.c b/clang/test/Analysis/z3/z3-logicalexpr-eval.c
index 3f21d08bd98b8..dd9e44a5a2483 100644
--- a/clang/test/Analysis/z3/z3-logicalexpr-eval.c
+++ b/clang/test/Analysis/z3/z3-logicalexpr-eval.c
@@ -11,3 +11,7 @@ void unary_not_logical_result(int x, int y) {
void unary_minus_logical_result(int x, int y) {
clang_analyzer_eval(-(x && y) <= 0); // expected-warning{{TRUE}}
}
+
+void wide_bitint_logical_truth_value(unsigned _BitInt(63) x) {
+ clang_analyzer_eval((1 && x) == (x != 0)); // expected-warning{{TRUE}}
+}
diff --git a/llvm/lib/Support/Z3Solver.cpp b/llvm/lib/Support/Z3Solver.cpp
index 664da8eacd323..f96c666c6c222 100644
--- a/llvm/lib/Support/Z3Solver.cpp
+++ b/llvm/lib/Support/Z3Solver.cpp
@@ -825,19 +825,12 @@ class Z3Solver : public SMTSolver {
}
// FIXME: This function is also used to retrieve floating-point values,
- // which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything
- // between 1 and 64 bits long, which is the reason we have this weird
- // guard. In the future, we need proper calls in the backend to retrieve
+ // which can be 16, 32, 64 or 128 bits long. Bitvectors can be arbitrarily
+ // long. In the future, we need proper calls in the backend to retrieve
// floating-points and its special values (NaN, +/-infinity, +/-zero),
// then we can drop this weird condition.
- if (Sort->getBitvectorSortSize() <= 64 ||
- Sort->getBitvectorSortSize() == 128) {
- Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
- return true;
- }
-
- assert(false && "Bitwidth not supported!");
- return false;
+ Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
+ return true;
}
if (Sort->isBooleanSort()) {
>From e4720bddf3b8535d0ac6e3d32585ad5b12d9e896 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Sat, 18 Jul 2026 17:44:32 +0000
Subject: [PATCH 2/4] reword comment
---
llvm/lib/Support/Z3Solver.cpp | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/llvm/lib/Support/Z3Solver.cpp b/llvm/lib/Support/Z3Solver.cpp
index f96c666c6c222..3db7013b4ce6a 100644
--- a/llvm/lib/Support/Z3Solver.cpp
+++ b/llvm/lib/Support/Z3Solver.cpp
@@ -827,8 +827,7 @@ class Z3Solver : public SMTSolver {
// FIXME: This function is also used to retrieve floating-point values,
// which can be 16, 32, 64 or 128 bits long. Bitvectors can be arbitrarily
// long. In the future, we need proper calls in the backend to retrieve
- // floating-points and its special values (NaN, +/-infinity, +/-zero),
- // then we can drop this weird condition.
+ // floating-points and its special values (NaN, +/-infinity, +/-zero).
Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
return true;
}
>From d01f53901f13f5108c2b9b481e092b5c1f544cc4 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Sat, 18 Jul 2026 17:48:28 +0000
Subject: [PATCH 3/4] reword comment
---
llvm/lib/Support/Z3Solver.cpp | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/llvm/lib/Support/Z3Solver.cpp b/llvm/lib/Support/Z3Solver.cpp
index 3db7013b4ce6a..12357b4fa5380 100644
--- a/llvm/lib/Support/Z3Solver.cpp
+++ b/llvm/lib/Support/Z3Solver.cpp
@@ -825,9 +825,9 @@ class Z3Solver : public SMTSolver {
}
// FIXME: This function is also used to retrieve floating-point values,
- // which can be 16, 32, 64 or 128 bits long. Bitvectors can be arbitrarily
- // long. In the future, we need proper calls in the backend to retrieve
- // floating-points and its special values (NaN, +/-infinity, +/-zero).
+ // which can be 16, 32, 64 or 128 bits long. In the future, we need proper
+ // calls in the backend to retrieve floating-points and its special values
+ // (NaN, +/-infinity, +/-zero).
Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
return true;
}
>From 533563012a80543644c0d38fec7901edf06fd827 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Sun, 19 Jul 2026 09:26:41 +0000
Subject: [PATCH 4/4] add regression test for the default range solver
---
clang/test/Analysis/logical-ops.c | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/clang/test/Analysis/logical-ops.c b/clang/test/Analysis/logical-ops.c
index be68569fcd8e5..eb202fdaace8d 100644
--- a/clang/test/Analysis/logical-ops.c
+++ b/clang/test/Analysis/logical-ops.c
@@ -52,3 +52,7 @@ void ambiguous_backtrack_2(int x) {
global_a = x >= 2 ? 1 : x;
global_b == x && 9 || 2;
}
+
+void wide_bitint_logical_truth_value(unsigned _BitInt(63) x) {
+ clang_analyzer_eval((1 && x) == (x != 0)); // expected-warning{{TRUE}}
+}
More information about the cfe-commits
mailing list