[clang] [analyzer] Fix unary/binary op support for SMT symbolic execution (PR #205078)
via cfe-commits
cfe-commits at lists.llvm.org
Mon Jun 29 08:46:52 PDT 2026
https://github.com/rdevshp updated https://github.com/llvm/llvm-project/pull/205078
>From b1d7b51bd8c3af7f61244c0d2f49bbe0bb9f159f Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Mon, 22 Jun 2026 08:24:48 +0000
Subject: [PATCH 1/7] [analyzer] Fix unary/binary op support for SMT symbolic
execution
SMT symbolic execution: the patch fixes unary op support, converts
operands of logical operators to boolean in getBinExpr, and clears
the hasComparison flag in getSymExpr when a boolean operand is
converted to a non-bool integer
Assisted-by: Codex
---
.../Core/PathSensitive/BasicValueFactory.h | 3 ++
.../Core/PathSensitive/SMTConstraintManager.h | 14 +++++--
.../Core/PathSensitive/SMTConv.h | 40 ++++++++++++++++++-
.../StaticAnalyzer/Core/BasicValueFactory.cpp | 14 +++++++
4 files changed, 66 insertions(+), 5 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
index ef04f9c485e88..38eaabf74dd34 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
@@ -265,6 +265,9 @@ class BasicValueFactory {
accumCXXBase(llvm::iterator_range<CastExpr::path_const_iterator> PathRange,
const nonloc::PointerToMember &PTM, const clang::CastKind &kind);
+ std::optional<APSIntPtr> evalAPSInt(UnaryOperator::Opcode Op,
+ const llvm::APSInt &V1);
+
std::optional<APSIntPtr> evalAPSInt(BinaryOperator::Opcode Op,
const llvm::APSInt &V1,
const llvm::APSInt &V2);
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index 7ea6d4ee3b72e..ac93c8bbf3724 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -171,6 +171,15 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
return BVF.Convert(SC->getType(), *Value).get();
}
+ if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
+ SymbolRef Operand = USE->getOperand();
+ const llvm::APSInt *Value;
+ if (!(Value = getSymVal(State, Operand)))
+ return nullptr;
+ std::optional<APSIntPtr> Res = BVF.evalAPSInt(USE->getOpcode(), *Value);
+ return Res ? Res.value().get() : nullptr;
+ }
+
if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
const llvm::APSInt *LHS, *RHS;
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
@@ -281,9 +290,8 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
- // UnarySymExpr support is not yet implemented in the Z3 wrapper.
- if (isa<UnarySymExpr>(Sym)) {
- return false;
+ if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
+ return canReasonAbout(SVB.makeSymbolVal(USE->getOperand()));
}
if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index c8c7a1ac7cc45..5fda18df409a3 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -342,6 +342,30 @@ class SMTConv {
Ctx.getTypeSize(FromTy));
}
+ static inline llvm::SMTExprRef convertToBoolExpr(llvm::SMTSolverRef &Solver,
+ ASTContext &Ctx,
+ const llvm::SMTExprRef &Exp,
+ QualType Ty) {
+ if (Ty->isBooleanType())
+ return Exp;
+
+ if (Ty->isRealFloatingType()) {
+ llvm::APFloat Zero =
+ llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
+ return fromFloatBinOp(Solver, Exp, BO_NE, Solver->mkFloat(Zero));
+ }
+
+ if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
+ Ty->isBlockPointerType() || Ty->isReferenceType()) {
+ return fromBinOp(
+ Solver, Exp, BO_NE,
+ Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
+ Ty->isSignedIntegerOrEnumerationType());
+ }
+
+ llvm_unreachable("Unsupported type for boolean conversion!");
+ }
+
// Wrapper to generate SMTSolverRef from unpacked binary symbolic
// expression. Sets the RetTy parameter. See getSMTSolverRef().
static inline llvm::SMTExprRef
@@ -351,15 +375,21 @@ class SMTConv {
QualType RTy, QualType &RetTy) {
llvm::SMTExprRef NewLHS = LHS;
llvm::SMTExprRef NewRHS = RHS;
- doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
// Update the return type parameter if the output type has changed.
// A boolean result can be represented as an integer type in C/C++, but at
// this point we only care about the SMT sorts. Set it as a boolean type
// to avoid subsequent SMT errors.
- if (BinaryOperator::isComparisonOp(Op) || BinaryOperator::isLogicalOp(Op)) {
+ if (BinaryOperator::isComparisonOp(Op)) {
+ doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
RetTy = Ctx.BoolTy;
+ } else if (BinaryOperator::isLogicalOp(Op)) {
+ RetTy = Ctx.BoolTy;
+ NewLHS = convertToBoolExpr(Solver, Ctx, LHS, LTy);
+ NewRHS = convertToBoolExpr(Solver, Ctx, RHS, RTy);
+ return fromBinOp(Solver, NewLHS, Op, NewRHS, false);
} else {
+ doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
RetTy = LTy;
}
@@ -456,6 +486,12 @@ class SMTConv {
// E.g. -(5 && a)
if (OperandTy == Ctx.BoolTy && OperandTy != RetTy &&
RetTy->isIntegerType()) {
+
+ // Converting an expression from bool to a non-bool integer invalidates
+ // it
+ if (hasComparison)
+ *hasComparison = false;
+
OperandExp = fromCast(Solver, OperandExp, RetTy, Ctx.getTypeSize(RetTy),
OperandTy, 1);
OperandTy = RetTy;
diff --git a/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp b/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
index c905ee6bc9fc9..7cf118c85ec9a 100644
--- a/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
@@ -242,6 +242,20 @@ const PointerToMemberData *BasicValueFactory::accumCXXBase(
return getPointerToMemberData(ND, BaseSpecList);
}
+std::optional<APSIntPtr> BasicValueFactory::evalAPSInt(UnaryOperator::Opcode Op,
+ const llvm::APSInt &V1) {
+ switch (Op) {
+ default:
+ llvm_unreachable("Invalid Opcode.");
+
+ case UO_Minus:
+ return getValue(-V1);
+
+ case UO_Not:
+ return getValue(~V1);
+ }
+}
+
std::optional<APSIntPtr>
BasicValueFactory::evalAPSInt(BinaryOperator::Opcode Op, const llvm::APSInt &V1,
const llvm::APSInt &V2) {
>From 436dfac9aad30942d2aeba6e9fb80ab656a3b480 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Wed, 24 Jun 2026 15:17:15 +0000
Subject: [PATCH 2/7] Add test cases for unary/binary SMT symbolic execution
---
clang/test/Analysis/z3/z3-logicalexpr-eval.c | 13 +++++++++++++
clang/test/Analysis/z3/z3-unarysymexpr.c | 6 ++++++
2 files changed, 19 insertions(+)
create mode 100644 clang/test/Analysis/z3/z3-logicalexpr-eval.c
diff --git a/clang/test/Analysis/z3/z3-logicalexpr-eval.c b/clang/test/Analysis/z3/z3-logicalexpr-eval.c
new file mode 100644
index 0000000000000..65290f6d2140a
--- /dev/null
+++ b/clang/test/Analysis/z3/z3-logicalexpr-eval.c
@@ -0,0 +1,13 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection \
+// RUN: -analyzer-constraints=z3 -verify %s
+// REQUIRES: z3
+
+void clang_analyzer_eval(int);
+
+void unary_not_logical_result(int x, int y) {
+ clang_analyzer_eval(~(x && y) != 0); // expected-warning{{TRUE}}
+}
+
+void unary_minus_logical_result(int x, int y) {
+ clang_analyzer_eval(-(x && y) <= 0); // expected-warning{{TRUE}}
+}
\ No newline at end of file
diff --git a/clang/test/Analysis/z3/z3-unarysymexpr.c b/clang/test/Analysis/z3/z3-unarysymexpr.c
index efe558c3146e8..2196f5188d851 100644
--- a/clang/test/Analysis/z3/z3-unarysymexpr.c
+++ b/clang/test/Analysis/z3/z3-unarysymexpr.c
@@ -60,3 +60,9 @@ long z3_crash3(long a) {
}
return 0;
}
+
+// Previously Z3 analysis crashed in this case, validate
+// that this no longer happens.
+int unary_operand_in_binary_op(int size, int mask) {
+ return size & ~mask;
+}
\ No newline at end of file
>From 60b39e671072c676a0fec662dd6934322d248460 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Wed, 24 Jun 2026 15:21:58 +0000
Subject: [PATCH 3/7] Add new lines at the end of the new testcases
---
clang/test/Analysis/z3/z3-logicalexpr-eval.c | 2 +-
clang/test/Analysis/z3/z3-unarysymexpr.c | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/clang/test/Analysis/z3/z3-logicalexpr-eval.c b/clang/test/Analysis/z3/z3-logicalexpr-eval.c
index 65290f6d2140a..2f2fb2e94b7d5 100644
--- a/clang/test/Analysis/z3/z3-logicalexpr-eval.c
+++ b/clang/test/Analysis/z3/z3-logicalexpr-eval.c
@@ -10,4 +10,4 @@ void unary_not_logical_result(int x, int y) {
void unary_minus_logical_result(int x, int y) {
clang_analyzer_eval(-(x && y) <= 0); // expected-warning{{TRUE}}
-}
\ No newline at end of file
+}
diff --git a/clang/test/Analysis/z3/z3-unarysymexpr.c b/clang/test/Analysis/z3/z3-unarysymexpr.c
index 2196f5188d851..e365ecfa655b0 100644
--- a/clang/test/Analysis/z3/z3-unarysymexpr.c
+++ b/clang/test/Analysis/z3/z3-unarysymexpr.c
@@ -65,4 +65,4 @@ long z3_crash3(long a) {
// that this no longer happens.
int unary_operand_in_binary_op(int size, int mask) {
return size & ~mask;
-}
\ No newline at end of file
+}
>From 81dcdefbe3e1356bf781ea815653cd9fce4c7cb2 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Mon, 29 Jun 2026 12:10:58 +0000
Subject: [PATCH 4/7] Remove hasComparison invalidation comment in getSymExpr
---
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h | 2 --
1 file changed, 2 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 5fda18df409a3..5d3ce58fced2a 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -487,8 +487,6 @@ class SMTConv {
if (OperandTy == Ctx.BoolTy && OperandTy != RetTy &&
RetTy->isIntegerType()) {
- // Converting an expression from bool to a non-bool integer invalidates
- // it
if (hasComparison)
*hasComparison = false;
>From 666f02dde023df406a8fd52002a0e8cf3815244d Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Mon, 29 Jun 2026 15:02:07 +0000
Subject: [PATCH 5/7] add GH issue reference to z3-unarysymexpr.c
unary_operand_in_binary_op test case
---
clang/test/Analysis/z3/z3-unarysymexpr.c | 1 +
1 file changed, 1 insertion(+)
diff --git a/clang/test/Analysis/z3/z3-unarysymexpr.c b/clang/test/Analysis/z3/z3-unarysymexpr.c
index e365ecfa655b0..b66b0ad0586aa 100644
--- a/clang/test/Analysis/z3/z3-unarysymexpr.c
+++ b/clang/test/Analysis/z3/z3-unarysymexpr.c
@@ -63,6 +63,7 @@ long z3_crash3(long a) {
// Previously Z3 analysis crashed in this case, validate
// that this no longer happens.
+// no-crash: GH #205037
int unary_operand_in_binary_op(int size, int mask) {
return size & ~mask;
}
>From 9329bc378f3d2c8d4e7e162bc97709db49cd789f Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Mon, 29 Jun 2026 15:08:16 +0000
Subject: [PATCH 6/7] Apply reviewer suggestion
---
.../StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index ac93c8bbf3724..d32a7f244dae6 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -290,7 +290,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
- if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
+ if (const auto *USE = dyn_cast<UnarySymExpr>(Sym)) {
return canReasonAbout(SVB.makeSymbolVal(USE->getOperand()));
}
>From f6fab2ae8c1ce8094e07e1e8f62c780cb6822a29 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Mon, 29 Jun 2026 15:45:13 +0000
Subject: [PATCH 7/7] use llvm::APSInt::getUnsigned(0) to construct APSInt 0
instead in SMTConv.h convertToBoolExpr
---
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 5d3ce58fced2a..00720185ab6e7 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -359,7 +359,7 @@ class SMTConv {
Ty->isBlockPointerType() || Ty->isReferenceType()) {
return fromBinOp(
Solver, Exp, BO_NE,
- Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
+ Solver->mkBitvector(llvm::APSInt::getUnsigned(0), Ctx.getTypeSize(Ty)),
Ty->isSignedIntegerOrEnumerationType());
}
More information about the cfe-commits
mailing list