[clang][analyzer] Correct SMT Layer for _BitInt cases refutations

[vabridgers]

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

clang::ento::SMTConv::fromBinOp(std::shared_ptr&, 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&)

[llvmbot]

@llvm/pr-subscribers-clang-static-analyzer-1

@llvm/pr-subscribers-clang

Author: None (vabridgers)

Changes

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

---

Full diff: https://github.com/llvm/llvm-project/pull/143310.diff

3 Files Affected:

• (modified) clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h (+12-2)
• (modified) clang/lib/AST/ASTContext.cpp (+7-2)
• (added) clang/test/Analysis/bitint-z3.c (+23)

diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 580b49a38dc72..2a41202d46440 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -573,20 +573,30 @@ class SMTConv {
     return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
   }
 
+  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/lib/AST/ASTContext.cpp b/clang/lib/AST/ASTContext.cpp
index 45f9602856840..094264813a8b3 100644
--- a/clang/lib/AST/ASTContext.cpp
+++ b/clang/lib/AST/ASTContext.cpp
@@ -13209,9 +13209,14 @@ size_t ASTContext::getSideTableAllocatedMemory() const {
 /// Returns empty type if there is no appropriate target types.
 QualType ASTContext::getIntTypeForBitwidth(unsigned DestWidth,
                                            unsigned Signed) const {
-  TargetInfo::IntType Ty = getTargetInfo().getIntTypeByWidth(DestWidth, Signed);
+  // round up to next power of 2 for _BitInt cases
+  unsigned pow2DestWidth = llvm::bit_ceil(DestWidth);
+  //if (pow2DestWidth == 4) pow2DestWidth = 8;
+  if (pow2DestWidth < 8) pow2DestWidth = 8;
+
+  TargetInfo::IntType Ty = getTargetInfo().getIntTypeByWidth(pow2DestWidth, Signed);
   CanQualType QualTy = getFromTargetType(Ty);
-  if (!QualTy && DestWidth == 128)
+  if (!QualTy && pow2DestWidth == 128)
     return Signed ? Int128Ty : UnsignedInt128Ty;
   return QualTy;
 }
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]}}
+}

[github-actions]

✅ With the latest revision this PR passed the C/C++ code formatter.

[vabridgers]

Looks like the ASTContext change is impacting other LITs and is an incorrect approach for those reasons. Please have a look regardless and comment on different ways to address if appropriate. I'm thinking the real fix needs to be in the SMT layer, detecting a _BitInt type and "doing the right thing". Thank you!

[steakhal]

Before I'd continue my review, I'd like a bit more context about the crash.
So we ended up with different "sorts", but I feel like that is because we don't capture implicit conversions that would play the role of widening or matching the operands type like standard arithmetic conversions and promotion rules would dictate.

I also looked at the test cases and it wasn't apparent where exactly it crashed, and why we need a stack address escape diag to trigger it. My best bet would be that we need some diag to trigger refutation, but then we could use a clang_analyzer_warnIfReached I think to convey this.

Could you tell us a bit more about this crash? And I we have not touched any related parts for ages now, how did you discover this now? Did you improve your fuzzer to cover more patterns?

[vabridgers]

Hi @steakhal , thanks for the response and questions. We started seeing these crashes when a new type was added to the front end, called _BitInt. _BitInt is a type allowing developers to define integers with a specific number of bits. We initially saw these rarely, and only in certain test cases since we really do not use _BitInt (at least not yet), so we improved our fuzzer to make use of _BitInt and drive these cases much more frequently. We try to make use of Z3 refutation to reduce our false positives, this case seems to be on the long tail of issues we know about. We've found and fixed a handful of issues related to the exotic features of our target - such as unusual address spaces and bitwidths. In retrospect, we know CSA (much less SMT) was not tested thoroughly across these conditions, so we continue to uncover dark corners here and there.

For both problems, the control flow ends up in fixAPSInt from different points in SMT - for example, from fromBinOp or getRangeExpr. fixAPSInt is given an APSInt and asked to infer the type from the width of APSInt (by calling getAPSIntType). In both of the test cases the bit width cannot be used to infer a type because the bitwidths of 3 and 35 in those test cases specifically cause Ctx.getIntTypeForBitwidth to return a NULL type. This is unexpected which led to a crash in doTypeConversion because both LTy and RTy are expected to be non NULL (an assertion caught this).

Once the type was inferred correctly, that corrected the crash in doTypeConversion, but left us with the crash in fromBinOp. The type widths needed to be adjusted also in addition to returning a correctly inferred type.

I hope this explains. I can provide more details if needed. Thanks for looking at this!

[steakhal]

Hi @steakhal , thanks for the response and questions. We started seeing these crashes when [...] so we continue to uncover dark corners here and there.

Yes, I knew this.

For both problems, the control flow ends up in fixAPSInt from different points in SMT - for example, from fromBinOp or getRangeExpr. fixAPSInt is given an APSInt and asked to infer the type from the width of APSInt (by calling getAPSIntType). In both of the test cases the bit width cannot be used to infer a type because the bitwidths of 3 and 35 in those test cases specifically cause Ctx.getIntTypeForBitwidth to return a NULL type.
This is unexpected which led to a crash in doTypeConversion because both LTy and RTy are expected to be non NULL (an assertion caught this).

I see now. This wasn't apparent form the patch.

Once the type was inferred correctly, that corrected the crash in doTypeConversion, but left us with the crash in fromBinOp. The type widths needed to be adjusted also in addition to returning a correctly inferred type.
I hope this explains. I can provide more details if needed. Thanks for looking at this!

I don't think I have more questions just yet. I'll have a look at the patch with having these in mind.

[NagyDonat]

The approach of the commit seems to be good. If the tests are passing with this commit, while they were crashing without it, then I don't see any significant obstacles.

I added a few nitpicks in inline comments, please have a look at them.

[vabridgers]

Thanks for the comments @NagyDonat , I think all comments have been resolved. Best

[vabridgers]

Sorry I missed those changes @NagyDonat , I think all has been resolved. Thanks so much for the comments. Best

[vabridgers]

Thanks @NagyDonat and @steakhal for the useful comments. I think all have been resolved at this point. If I've missed something I'll address. Best.

[NagyDonat]

Thanks for the updates! I added a few more style nitpicks, but overall LGTM.

[vabridgers]

Thanks for the improvement suggestions @NagyDonat and @steakhal. I've resolved all comments for now and patiently await your next round or LGTM. Best!

[vabridgers]

Thanks for the catching the unresolved issues. I think they're all resolved at this point. Please let me know otherwise.

[NagyDonat]

LGTM but wait for the opinion of @steakhal as well.

(By the way, after tweaking the testcase, did you check that it would still crash without the improvements of the commit?)