[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 <[email protected]>

Author: vabridgers

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.

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}}
+}