[clang] ec8d68b - [clang][analyzer] Correct SMT Layer for _BitInt cases refutations (#143310)

[via cfe-commits]

Author: vabridgers
Date: 2025-06-11T11:25:24-05:00
New Revision: ec8d68b59f82423e5a6bf452e33ee8c5f64b0edc

URL: https://github.com/llvm/llvm-project/commit/ec8d68b59f82423e5a6bf452e33ee8c5f64b0edc
DIFF: https://github.com/llvm/llvm-project/commit/ec8d68b59f82423e5a6bf452e33ee8c5f64b0edc.diff

LOG: [clang][analyzer] Correct SMT Layer for _BitInt cases refutations (#143310)

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.
 ...
<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&)

---------

Co-authored-by: Vince Bridgers <vince.a.bridgers at ericsson.com>

Added: 
    clang/test/Analysis/bitint-z3.c

Modified: 
    clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 580b49a38dc72..70a7953918ace 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,35 @@ class SMTConv {
   // TODO: Refactor to put elsewhere
   static inline QualType getAPSIntType(ASTContext &Ctx,
                                        const llvm::APSInt &Int) {
-    return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
+    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());
   }
 
   // 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()) {
-      NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
-    } else
-      NewInt = Int;
-
-    return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
+    if (APSIntBitwidth == 1 && Ty.isNull())
+      return {Int.extend(Ctx.getTypeSize(Ctx.BoolTy)),
+              getAPSIntType(Ctx, NewInt)};
+    if (llvm::isPowerOf2_32(APSIntBitwidth) || Ty.isNull())
+      return {Int, Ty};
+    return {Int.extend(Ctx.getTypeSize(Ty)), 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..4cb97f9de8299
--- /dev/null
+++ b/clang/test/Analysis/bitint-z3.c
@@ -0,0 +1,22 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -w \
+// RUN:   -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+// Previously these tests were crashing because the SMTConv layer did not
+// comprehend the _BitInt types.
+
+void clang_analyzer_warnIfReached();
+
+void c(int b, _BitInt(35) a) {
+  int d = 0;
+  if (a)
+    b = d;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}
+
+void f(int *d, _BitInt(3) e) {
+  int g;
+  d = &g;
+  e ?: 0;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+}