[clang] [analyzer] Fix unary/binary op support for SMT symbolic execution (PR #205078)
via cfe-commits
cfe-commits at lists.llvm.org
Tue Jun 30 01:20:49 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 01/11] [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 02/11] 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 03/11] 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 04/11] 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 05/11] 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 06/11] 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 07/11] 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());
}
>From 9444bed9ad4a0ab9b85566631caba32b9720fe9d Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Mon, 29 Jun 2026 16:19:32 +0000
Subject: [PATCH 08/11] return empty std::optional instead in
BasicValueFacotry::evalAPSInt for unsupported operator opcodes
---
clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp b/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
index 7cf118c85ec9a..d1a4ef65528b3 100644
--- a/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
@@ -246,7 +246,7 @@ std::optional<APSIntPtr> BasicValueFactory::evalAPSInt(UnaryOperator::Opcode Op,
const llvm::APSInt &V1) {
switch (Op) {
default:
- llvm_unreachable("Invalid Opcode.");
+ return std::nullopt;
case UO_Minus:
return getValue(-V1);
@@ -261,7 +261,7 @@ BasicValueFactory::evalAPSInt(BinaryOperator::Opcode Op, const llvm::APSInt &V1,
const llvm::APSInt &V2) {
switch (Op) {
default:
- llvm_unreachable("Invalid Opcode.");
+ return std::nullopt;
case BO_Mul:
return getValue(V1 * V2);
>From f7d3eb69098e339f2ef1e4fc8098e9176fda6d92 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Mon, 29 Jun 2026 16:21:47 +0000
Subject: [PATCH 09/11] Apply clang-format
---
.../clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 00720185ab6e7..605e4e856f15d 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -357,10 +357,10 @@ class SMTConv {
if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
Ty->isBlockPointerType() || Ty->isReferenceType()) {
- return fromBinOp(
- Solver, Exp, BO_NE,
- Solver->mkBitvector(llvm::APSInt::getUnsigned(0), Ctx.getTypeSize(Ty)),
- Ty->isSignedIntegerOrEnumerationType());
+ return fromBinOp(Solver, Exp, BO_NE,
+ Solver->mkBitvector(llvm::APSInt::getUnsigned(0),
+ Ctx.getTypeSize(Ty)),
+ Ty->isSignedIntegerOrEnumerationType());
}
llvm_unreachable("Unsupported type for boolean conversion!");
>From 810fd6d054f33e7956682f1465cacc1ae7070e46 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Tue, 30 Jun 2026 07:48:15 +0000
Subject: [PATCH 10/11] SMT solver: return std::optional for
convertToBoolExpr/getBinExpr/getSymBinExpr/getSymExpr/getExpr/getRangeExpr
---
.../Core/PathSensitive/SMTConstraintManager.h | 33 +++--
.../Core/PathSensitive/SMTConv.h | 133 ++++++++++--------
.../Core/Z3CrosscheckVisitor.cpp | 24 +++-
3 files changed, 117 insertions(+), 73 deletions(-)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index d32a7f244dae6..ce47994971217 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -52,17 +52,20 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
QualType RetTy;
bool hasComparison;
- llvm::SMTExprRef Exp =
+ std::optional<llvm::SMTExprRef> Exp =
SMTConv::getExpr(Solver, Ctx, Sym, RetTy, &hasComparison);
-
+ if (!Exp) {
+ return assumeSymUnsupported(State, Sym, Assumption);
+ }
// Create zero comparison for implicit boolean cast, with reversed
// assumption
if (!hasComparison && !RetTy->isBooleanType())
return assumeExpr(
State, Sym,
- SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
+ SMTConv::getZeroExpr(Solver, Ctx, Exp.value(), RetTy, !Assumption));
- return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
+ return assumeExpr(State, Sym,
+ Assumption ? Exp.value() : Solver->mkNot(Exp.value()));
}
ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
@@ -70,8 +73,12 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
const llvm::APSInt &To,
bool InRange) override {
ASTContext &Ctx = getBasicVals().getContext();
- return assumeExpr(
- State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
+ std::optional<llvm::SMTExprRef> Expr =
+ SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange);
+ if (!Expr) {
+ return assumeSymUnsupported(State, Sym, false);
+ }
+ return assumeExpr(State, Sym, Expr.value());
}
ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
@@ -89,13 +96,17 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
QualType RetTy;
// The expression may be casted, so we cannot call getZ3DataExpr() directly
- llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, RetTy);
- llvm::SMTExprRef Exp =
- SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
+ std::optional<llvm::SMTExprRef> VarExp =
+ SMTConv::getExpr(Solver, Ctx, Sym, RetTy);
+ if (!VarExp) {
+ return ConditionTruthVal();
+ }
+ llvm::SMTExprRef Exp = SMTConv::getZeroExpr(Solver, Ctx, VarExp.value(),
+ RetTy, /*Assumption=*/true);
// Negate the constraint
- llvm::SMTExprRef NotExp =
- SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
+ llvm::SMTExprRef NotExp = SMTConv::getZeroExpr(Solver, Ctx, VarExp.value(),
+ RetTy, /*Assumption=*/false);
ConditionTruthVal isSat = checkModel(State, Sym, Exp);
ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 605e4e856f15d..6f7ba47532cfa 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -342,10 +342,9 @@ class SMTConv {
Ctx.getTypeSize(FromTy));
}
- static inline llvm::SMTExprRef convertToBoolExpr(llvm::SMTSolverRef &Solver,
- ASTContext &Ctx,
- const llvm::SMTExprRef &Exp,
- QualType Ty) {
+ static inline std::optional<llvm::SMTExprRef>
+ convertToBoolExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
+ const llvm::SMTExprRef &Exp, QualType Ty) {
if (Ty->isBooleanType())
return Exp;
@@ -362,13 +361,13 @@ class SMTConv {
Ctx.getTypeSize(Ty)),
Ty->isSignedIntegerOrEnumerationType());
}
-
- llvm_unreachable("Unsupported type for boolean conversion!");
+ assert(false && "Unsupported type for boolean conversion!");
+ return std::nullopt;
}
// Wrapper to generate SMTSolverRef from unpacked binary symbolic
// expression. Sets the RetTy parameter. See getSMTSolverRef().
- static inline llvm::SMTExprRef
+ static inline std::optional<llvm::SMTExprRef>
getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
const llvm::SMTExprRef &LHS, QualType LTy,
BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS,
@@ -385,8 +384,13 @@ class SMTConv {
RetTy = Ctx.BoolTy;
} else if (BinaryOperator::isLogicalOp(Op)) {
RetTy = Ctx.BoolTy;
- NewLHS = convertToBoolExpr(Solver, Ctx, LHS, LTy);
- NewRHS = convertToBoolExpr(Solver, Ctx, RHS, RTy);
+ auto LHSOpt = convertToBoolExpr(Solver, Ctx, LHS, LTy);
+ auto RHSOpt = convertToBoolExpr(Solver, Ctx, RHS, RTy);
+ if (!LHSOpt || !RHSOpt) {
+ return std::nullopt;
+ }
+ NewLHS = LHSOpt.value();
+ NewRHS = RHSOpt.value();
return fromBinOp(Solver, NewLHS, Op, NewRHS, false);
} else {
doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
@@ -407,22 +411,24 @@ class SMTConv {
// Wrapper to generate SMTSolverRef from BinarySymExpr.
// Sets the hasComparison and RetTy parameters. See getSMTSolverRef().
- static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver,
- ASTContext &Ctx,
- const BinarySymExpr *BSE,
- bool *hasComparison,
- QualType &RetTy) {
+ static inline std::optional<llvm::SMTExprRef>
+ getSymBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
+ const BinarySymExpr *BSE, bool *hasComparison,
+ QualType &RetTy) {
QualType LTy, RTy;
BinaryOperator::Opcode Op = BSE->getOpcode();
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
- llvm::SMTExprRef LHS =
+ std::optional<llvm::SMTExprRef> LHS =
getSymExpr(Solver, Ctx, SIE->getLHS(), LTy, hasComparison);
+ if (!LHS) {
+ return std::nullopt;
+ }
llvm::APSInt NewRInt;
std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
llvm::SMTExprRef RHS =
Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
- return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
+ return getBinExpr(Solver, Ctx, LHS.value(), LTy, Op, RHS, RTy, RetTy);
}
if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
@@ -430,28 +436,35 @@ class SMTConv {
std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
llvm::SMTExprRef LHS =
Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
- llvm::SMTExprRef RHS =
+ std::optional<llvm::SMTExprRef> RHS =
getSymExpr(Solver, Ctx, ISE->getRHS(), RTy, hasComparison);
- return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
+ if (!RHS) {
+ return std::nullopt;
+ }
+ return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS.value(), RTy, RetTy);
}
if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
- llvm::SMTExprRef LHS =
+ std::optional<llvm::SMTExprRef> LHS =
getSymExpr(Solver, Ctx, SSM->getLHS(), LTy, hasComparison);
- llvm::SMTExprRef RHS =
+ std::optional<llvm::SMTExprRef> RHS =
getSymExpr(Solver, Ctx, SSM->getRHS(), RTy, hasComparison);
- return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
+ if (!LHS || !RHS) {
+ return std::nullopt;
+ }
+ return getBinExpr(Solver, Ctx, LHS.value(), LTy, Op, RHS.value(), RTy,
+ RetTy);
}
- llvm_unreachable("Unsupported BinarySymExpr type!");
+ assert(false && "Unsupported BinarySymExpr type!");
+ return std::nullopt;
}
// Recursive implementation to unpack and generate symbolic expression.
// Sets the hasComparison and RetTy parameters. See getExpr().
- static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
- ASTContext &Ctx, SymbolRef Sym,
- QualType &RetTy,
- bool *hasComparison) {
+ static inline std::optional<llvm::SMTExprRef>
+ getSymExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
+ QualType &RetTy, bool *hasComparison) {
if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
RetTy = Sym->getType();
@@ -462,24 +475,28 @@ class SMTConv {
RetTy = Sym->getType();
QualType FromTy;
- llvm::SMTExprRef Exp =
+ std::optional<llvm::SMTExprRef> Exp =
getSymExpr(Solver, Ctx, SC->getOperand(), FromTy, hasComparison);
-
+ if (!Exp) {
+ return std::nullopt;
+ }
// Casting an expression with a comparison invalidates it. Note that this
// must occur after the recursive call above.
// e.g. (signed char) (x > 0)
if (hasComparison)
*hasComparison = false;
- return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
+ return getCastExpr(Solver, Ctx, Exp.value(), FromTy, Sym->getType());
}
if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
RetTy = Sym->getType();
QualType OperandTy;
- llvm::SMTExprRef OperandExp =
+ std::optional<llvm::SMTExprRef> OperandExp =
getSymExpr(Solver, Ctx, USE->getOperand(), OperandTy, hasComparison);
-
+ if (!OperandExp) {
+ return std::nullopt;
+ }
// When the operand is a bool expr, but the operator is an integeral
// operator, casting the bool expr to the integer before creating the
// unary operator.
@@ -490,15 +507,15 @@ class SMTConv {
if (hasComparison)
*hasComparison = false;
- OperandExp = fromCast(Solver, OperandExp, RetTy, Ctx.getTypeSize(RetTy),
- OperandTy, 1);
+ OperandExp = fromCast(Solver, OperandExp.value(), RetTy,
+ Ctx.getTypeSize(RetTy), OperandTy, 1);
OperandTy = RetTy;
}
llvm::SMTExprRef UnaryExp =
OperandTy->isRealFloatingType()
- ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp)
- : fromUnOp(Solver, USE->getOpcode(), OperandExp);
+ ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp.value())
+ : fromUnOp(Solver, USE->getOpcode(), OperandExp.value());
// Currently, without the `support-symbolic-integer-casts=true` option,
// we do not emit `SymbolCast`s for implicit casts.
@@ -513,25 +530,24 @@ class SMTConv {
}
if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
- llvm::SMTExprRef Exp =
+ std::optional<llvm::SMTExprRef> Exp =
getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
// Set the hasComparison parameter, in post-order traversal order.
if (hasComparison)
*hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
return Exp;
}
-
- llvm_unreachable("Unsupported SymbolRef type!");
+ assert(false && "Unsupported SymbolRef type!");
+ return std::nullopt;
}
// Generate an SMTSolverRef that represents the given symbolic expression.
// Sets the hasComparison parameter if the expression has a comparison
// operator. Sets the RetTy parameter to the final return type after
// promotions and casts.
- static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,
- ASTContext &Ctx, SymbolRef Sym,
- QualType &RetTy,
- bool *hasComparison = nullptr) {
+ static inline std::optional<llvm::SMTExprRef>
+ getExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
+ QualType &RetTy, bool *hasComparison = nullptr) {
if (hasComparison) {
*hasComparison = false;
}
@@ -570,7 +586,7 @@ class SMTConv {
// Wrapper to generate SMTSolverRef from a range. If From == To, an
// equality will be created instead.
- static inline llvm::SMTExprRef
+ static inline std::optional<llvm::SMTExprRef>
getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) {
// Convert lower bound
@@ -582,13 +598,16 @@ class SMTConv {
// Convert symbol
QualType SymTy;
- llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, SymTy);
-
+ std::optional<llvm::SMTExprRef> Exp = getExpr(Solver, Ctx, Sym, SymTy);
+ if (!Exp) {
+ return std::nullopt;
+ }
// Construct single (in)equality
if (From == To) {
QualType UnusedRetTy;
- return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
- FromExp, FromTy, /*RetTy=*/UnusedRetTy);
+ return getBinExpr(Solver, Ctx, Exp.value(), SymTy,
+ InRange ? BO_EQ : BO_NE, FromExp, FromTy,
+ /*RetTy=*/UnusedRetTy);
}
QualType ToTy;
@@ -600,15 +619,17 @@ class SMTConv {
// Construct two (in)equalities, and a logical and/or
QualType UnusedRetTy;
- llvm::SMTExprRef LHS =
- getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
- FromTy, /*RetTy=*/UnusedRetTy);
- llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
- InRange ? BO_LE : BO_GT, ToExp, ToTy,
- /*RetTy=*/UnusedRetTy);
-
- return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
- SymTy->isSignedIntegerOrEnumerationType());
+ std::optional<llvm::SMTExprRef> LHS =
+ getBinExpr(Solver, Ctx, Exp.value(), SymTy, InRange ? BO_GE : BO_LT,
+ FromExp, FromTy, /*RetTy=*/UnusedRetTy);
+ std::optional<llvm::SMTExprRef> RHS = getBinExpr(
+ Solver, Ctx, Exp.value(), SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
+ /*RetTy=*/UnusedRetTy);
+ if (!LHS || !RHS) {
+ return std::nullopt;
+ }
+ return fromBinOp(Solver, LHS.value(), InRange ? BO_LAnd : BO_LOr,
+ RHS.value(), SymTy->isSignedIntegerOrEnumerationType());
}
// Recover the QualType of an APSInt.
diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
index f965bfb590d80..30bb82a4a5c6c 100644
--- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
+++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
@@ -75,16 +75,28 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
for (const auto &[Sym, Range] : Constraints) {
auto RangeIt = Range.begin();
- llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
+ std::optional<llvm::SMTExprRef> SMTConstraintsOpt = SMTConv::getRangeExpr(
RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
/*InRange=*/true);
+ if (!SMTConstraintsOpt) {
+ continue;
+ }
+ auto SMTConstraints = SMTConstraintsOpt.value();
+ bool ShouldAddConstraint = true;
while ((++RangeIt) != Range.end()) {
- SMTConstraints = RefutationSolver->mkOr(
- SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
- RangeIt->From(), RangeIt->To(),
- /*InRange=*/true));
+ std::optional<llvm::SMTExprRef> ConstraintOpt = SMTConv::getRangeExpr(
+ RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
+ /*InRange=*/true);
+ if (!ConstraintOpt) {
+ ShouldAddConstraint = false;
+ break;
+ }
+ SMTConstraints =
+ RefutationSolver->mkOr(SMTConstraints, ConstraintOpt.value());
+ }
+ if (ShouldAddConstraint) {
+ RefutationSolver->addConstraint(SMTConstraints);
}
- RefutationSolver->addConstraint(SMTConstraints);
}
auto GetUsedRLimit = [](const llvm::SMTSolverRef &Solver) {
>From db996444684d139b41c260a447a857014245cf52 Mon Sep 17 00:00:00 2001
From: rdevshp <rdevshp at gmail.com>
Date: Tue, 30 Jun 2026 08:20:11 +0000
Subject: [PATCH 11/11] Add assert to BasicValueFactory::evalAPSInt
---
clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp | 2 ++
1 file changed, 2 insertions(+)
diff --git a/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp b/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
index d1a4ef65528b3..b86f0e8309dc7 100644
--- a/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BasicValueFactory.cpp
@@ -246,6 +246,7 @@ std::optional<APSIntPtr> BasicValueFactory::evalAPSInt(UnaryOperator::Opcode Op,
const llvm::APSInt &V1) {
switch (Op) {
default:
+ assert(false && "Invalid Opcode.");
return std::nullopt;
case UO_Minus:
@@ -261,6 +262,7 @@ BasicValueFactory::evalAPSInt(BinaryOperator::Opcode Op, const llvm::APSInt &V1,
const llvm::APSInt &V2) {
switch (Op) {
default:
+ assert(false && "Invalid Opcode.");
return std::nullopt;
case BO_Mul:
More information about the cfe-commits
mailing list