https://github.com/vabridgers updated
https://github.com/llvm/llvm-project/pull/143310
>From 66fbfd292123136e87528d710db6aeeceed3cce2 Mon Sep 17 00:00:00 2001
From: Vince Bridgers <vince.a.bridg...@ericsson.com>
Date: Sun, 8 Jun 2025 15:48:04 +0200
Subject: [PATCH 1/6] [analyzer] Correct SMT Layer for _BitInt cases
refutations
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Since _BitInt was added later, SMT did not comprehend getting
a type by bitwidth that's not a power of 2. 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&)
---
.../Core/PathSensitive/SMTConv.h | 27 ++++++++++++++++---
clang/test/Analysis/bitint-z3.c | 23 ++++++++++++++++
2 files changed, 47 insertions(+), 3 deletions(-)
create mode 100644 clang/test/Analysis/bitint-z3.c
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 580b49a38dc72..50c29a3a7f781 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,42 @@ class SMTConv {
// TODO: Refactor to put elsewhere
static inline QualType getAPSIntType(ASTContext &Ctx,
const llvm::APSInt &Int) {
- return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
+ QualType Ty = Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
+ // If Ty is Null, could be because the original type was a _BitInt.
+ // Get the bit size and round up to next power of 2, max char size
+ if (Ty.isNull()) {
+ unsigned CharTypeSize = Ctx.getTypeSize(Ctx.CharTy);
+ unsigned pow2DestWidth =
+ std::max(llvm::bit_ceil(Int.getBitWidth()), CharTypeSize);
+ Ty = Ctx.getIntTypeForBitwidth(pow2DestWidth, Int.isSigned());
+ }
+ return Ty;
+ }
+
+ 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/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]}}
+}
>From 94db43307c6e173c9eae7eb5b1fde49a53c9086d Mon Sep 17 00:00:00 2001
From: einvbri <vince.a.bridg...@ericsson.com>
Date: Tue, 10 Jun 2025 19:47:03 +0200
Subject: [PATCH 2/6] Address review comments
---
.../StaticAnalyzer/Core/PathSensitive/SMTConv.h | 14 +++++++-------
1 file changed, 7 insertions(+), 7 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 50c29a3a7f781..8d0a82cb0984b 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -577,16 +577,16 @@ class SMTConv {
// Get the bit size and round up to next power of 2, max char size
if (Ty.isNull()) {
unsigned CharTypeSize = Ctx.getTypeSize(Ctx.CharTy);
- unsigned pow2DestWidth =
+ unsigned Pow2DestWidth =
std::max(llvm::bit_ceil(Int.getBitWidth()), CharTypeSize);
- Ty = Ctx.getIntTypeForBitwidth(pow2DestWidth, Int.isSigned());
+ Ty = Ctx.getIntTypeForBitwidth(Pow2DestWidth, Int.isSigned());
}
return Ty;
}
- static inline bool IsPower2(unsigned bits) {
- return bits > 0 && (bits & (bits - 1)) == 0;
- }
+ // 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>
@@ -601,8 +601,8 @@ class SMTConv {
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);
+ } else if (!llvm::isPowerOf2_32(APSIntBitwidth) &&
+ !getAPSIntType(Ctx, Int).isNull()) {
NewInt = Int.extend(Ctx.getTypeSize(Ty));
} else
NewInt = Int;
>From fa9760917b69b06ab9bee6b5e4878e64cae751f2 Mon Sep 17 00:00:00 2001
From: einvbri <vince.a.bridg...@ericsson.com>
Date: Tue, 10 Jun 2025 22:01:54 +0200
Subject: [PATCH 3/6] Really address the review comments I missed the first
time
:)
---
.../clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h | 7 +------
1 file changed, 1 insertion(+), 6 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 8d0a82cb0984b..3238f56a8bb3a 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -584,10 +584,6 @@ class SMTConv {
return Ty;
}
- // 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) {
@@ -601,8 +597,7 @@ class SMTConv {
if (APSIntBitwidth == 1 && Ty.isNull()) {
NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
Ty = getAPSIntType(Ctx, NewInt);
- } else if (!llvm::isPowerOf2_32(APSIntBitwidth) &&
- !getAPSIntType(Ctx, Int).isNull()) {
+ } else if (!llvm::isPowerOf2_32(APSIntBitwidth) && !Ty.isNull()) {
NewInt = Int.extend(Ctx.getTypeSize(Ty));
} else
NewInt = Int;
>From 6d3e79bf1b7feda1795cbf33c87acd0246f4a990 Mon Sep 17 00:00:00 2001
From: einvbri <vince.a.bridg...@ericsson.com>
Date: Wed, 11 Jun 2025 12:48:56 +0200
Subject: [PATCH 4/6] Address latest round of comments, rebase to latest
origin/main
---
.../Core/PathSensitive/SMTConv.h | 30 +++++++++----------
clang/test/Analysis/bitint-z3.c | 23 +++++++-------
2 files changed, 25 insertions(+), 28 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 3238f56a8bb3a..e3f4dc13d54a0 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -572,15 +572,16 @@ class SMTConv {
// TODO: Refactor to put elsewhere
static inline QualType getAPSIntType(ASTContext &Ctx,
const llvm::APSInt &Int) {
- QualType Ty = Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
+ QualType Ty;
+ if (!(Ty = Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned()))
+ .isNull())
+ return Ty;
// If Ty is Null, could be because the original type was a _BitInt.
// Get the bit size and round up to next power of 2, max char size
- if (Ty.isNull()) {
- unsigned CharTypeSize = Ctx.getTypeSize(Ctx.CharTy);
- unsigned Pow2DestWidth =
- std::max(llvm::bit_ceil(Int.getBitWidth()), CharTypeSize);
- Ty = Ctx.getIntTypeForBitwidth(Pow2DestWidth, Int.isSigned());
- }
+ unsigned CharTypeSize = Ctx.getTypeSize(Ctx.CharTy);
+ unsigned Pow2DestWidth =
+ std::max(llvm::bit_ceil(Int.getBitWidth()), CharTypeSize);
+ Ty = Ctx.getIntTypeForBitwidth(Pow2DestWidth, Int.isSigned());
return Ty;
}
@@ -594,15 +595,12 @@ class SMTConv {
// 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()) {
- NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
- Ty = getAPSIntType(Ctx, NewInt);
- } else if (!llvm::isPowerOf2_32(APSIntBitwidth) && !Ty.isNull()) {
- NewInt = Int.extend(Ctx.getTypeSize(Ty));
- } else
- NewInt = Int;
-
- return std::make_pair(NewInt, Ty);
+ if (APSIntBitwidth == 1 && Ty.isNull())
+ return {Int.extend(Ctx.getTypeSize(Ctx.BoolTy)),
+ getAPSIntType(Ctx, NewInt)};
+ if (!llvm::isPowerOf2_32(APSIntBitwidth) && !Ty.isNull())
+ return {Int.extend(Ctx.getTypeSize(Ty)), Ty};
+ return {Int, 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
index d50c93acdf117..8bb97ca968f11 100644
--- a/clang/test/Analysis/bitint-z3.c
+++ b/clang/test/Analysis/bitint-z3.c
@@ -1,23 +1,22 @@
-// 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
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -w \
+// RUN: -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.
+// Previously these tests were crashing because the SMTConv layer did not
+// comprehend the _BitInt types.
-_BitInt(35) a;
-int b;
-void c() {
+void clang_analyzer_warnIfReached();
+
+void c(int b, _BitInt(35) a) {
int d;
if (a)
b = d; // expected-warning{{Assigned value is uninitialized
[core.uninitialized.Assign]}}
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
}
-int *d;
-_BitInt(3) e;
-void f() {
+void f(int *d, _BitInt(3) e) {
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]}}
+ e ?: 0;
+ clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
}
>From c3fa58f25fb41b5a39a8d0c22c433b6c913941c2 Mon Sep 17 00:00:00 2001
From: einvbri <vince.a.bridg...@ericsson.com>
Date: Wed, 11 Jun 2025 15:09:45 +0200
Subject: [PATCH 5/6] Address next round of comments
---
.../StaticAnalyzer/Core/PathSensitive/SMTConv.h | 14 ++++++++------
1 file changed, 8 insertions(+), 6 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index e3f4dc13d54a0..6ed569eaa0a49 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -577,12 +577,14 @@ class SMTConv {
.isNull())
return Ty;
// If Ty is Null, could be because the original type was a _BitInt.
- // Get the bit size and round up to next power of 2, max char size
+ // 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);
- Ty = Ctx.getIntTypeForBitwidth(Pow2DestWidth, Int.isSigned());
- return Ty;
+ return Ctx.getIntTypeForBitwidth(Pow2DestWidth, Int.isSigned());
+ // Ty = Ctx.getIntTypeForBitwidth(Pow2DestWidth, Int.isSigned());
+ // return Ty;
}
// Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
@@ -598,9 +600,9 @@ class SMTConv {
if (APSIntBitwidth == 1 && Ty.isNull())
return {Int.extend(Ctx.getTypeSize(Ctx.BoolTy)),
getAPSIntType(Ctx, NewInt)};
- if (!llvm::isPowerOf2_32(APSIntBitwidth) && !Ty.isNull())
- return {Int.extend(Ctx.getTypeSize(Ty)), Ty};
- return {Int, Ty};
+ 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.
>From 86809d7315aaadcf1458778404d27c8861e7ccb0 Mon Sep 17 00:00:00 2001
From: einvbri <vince.a.bridg...@ericsson.com>
Date: Wed, 11 Jun 2025 15:47:19 +0200
Subject: [PATCH 6/6] address next round of comments
---
.../clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h | 7 ++-----
clang/test/Analysis/bitint-z3.c | 4 ++--
2 files changed, 4 insertions(+), 7 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 6ed569eaa0a49..69d1743842312 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -572,9 +572,8 @@ class SMTConv {
// TODO: Refactor to put elsewhere
static inline QualType getAPSIntType(ASTContext &Ctx,
const llvm::APSInt &Int) {
- QualType Ty;
- if (!(Ty = Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned()))
- .isNull())
+ 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
@@ -583,8 +582,6 @@ class SMTConv {
unsigned Pow2DestWidth =
std::max(llvm::bit_ceil(Int.getBitWidth()), CharTypeSize);
return Ctx.getIntTypeForBitwidth(Pow2DestWidth, Int.isSigned());
- // Ty = Ctx.getIntTypeForBitwidth(Pow2DestWidth, Int.isSigned());
- // return Ty;
}
// Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
diff --git a/clang/test/Analysis/bitint-z3.c b/clang/test/Analysis/bitint-z3.c
index 8bb97ca968f11..4cb97f9de8299 100644
--- a/clang/test/Analysis/bitint-z3.c
+++ b/clang/test/Analysis/bitint-z3.c
@@ -8,9 +8,9 @@
void clang_analyzer_warnIfReached();
void c(int b, _BitInt(35) a) {
- int d;
+ int d = 0;
if (a)
- b = d; // expected-warning{{Assigned value is uninitialized
[core.uninitialized.Assign]}}
+ b = d;
clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
}
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
