https://github.com/rdevshp updated https://github.com/llvm/llvm-project/pull/210525
>From 8face7c8dcf8daed79d53d520a072b87fdd3c28c Mon Sep 17 00:00:00 2001 From: rdevshp <[email protected]> Date: Sat, 18 Jul 2026 16:05:37 +0000 Subject: [PATCH 1/3] [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 <[email protected]> Date: Sat, 18 Jul 2026 17:44:32 +0000 Subject: [PATCH 2/3] 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 <[email protected]> Date: Sat, 18 Jul 2026 17:48:28 +0000 Subject: [PATCH 3/3] 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; } _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
