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

[via cfe-commits]

llvmbot wrote:


<!--LLVM PR SUMMARY COMMENT-->

@llvm/pr-subscribers-clang

Author: None (vabridgers)

<details>
<summary>Changes</summary>

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 
&amp;,
     const llvm::SMTExprRef &amp;, const BinaryOperator::Opcode, const 
llvm::SMTExprRef &amp;, bool):
     Assertion `*Solver-&gt;getSort(LHS) == *Solver-&gt;getSort(RHS) &amp;&amp; 
"AST's must have the same sort!"' failed.
 ...
 #<!-- -->9 &lt;address&gt; 
clang::ento::SMTConv::fromBinOp(std::shared_ptr&lt;llvm::SMTSolver&gt;&amp;,
     llvm::SMTExpr const* const&amp;, clang::BinaryOperatorKind, llvm::SMTExpr 
const* const&amp;,
     bool) SMTConstraintManager.cpp
     clang::ASTContext&amp;, llvm::SMTExpr const* const&amp;, clang::QualType,
     clang::BinaryOperatorKind, llvm::SMTExpr const* const&amp;, 
clang::QualType,
     clang::QualType*) SMTConstraintManager.cpp
     clang::ASTContext&amp;, clang::ento::SymExpr const*, llvm::APSInt 
const&amp;,
     llvm::APSInt const&amp;, bool) SMTConstraintManager.cpp
     clang::ento::ExplodedNode const*, clang::ento::PathSensitiveBugReport&amp;)

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

``````````

</details>


https://github.com/llvm/llvm-project/pull/143310
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits