https://github.com/rdevshp created
https://github.com/llvm/llvm-project/pull/205078
SMT symbolic execution:
the patch fixes unary op support, convert 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.
This PR allows C functions like
```
int f(int x, int y) {
if (~(x && y))
return 0;
return 1;
}
```
to be analyzed with `-cc1 -analyze -analyzer-checker=core
-analyzer-constraints=z3`
Assisted-by: Codex
>From 98ab54c13884a6968563561a9963f1131dc53287 Mon Sep 17 00:00:00 2001
From: rdevshp <[email protected]>
Date: Mon, 22 Jun 2026 08:24:48 +0000
Subject: [PATCH] [analyzer] Fix unary/binary op support for SMT symbolic
execution
SMT symbolic execution: the patch fixes unary op support, convert
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 | 15 +++++--
.../Core/PathSensitive/SMTConv.h | 39 ++++++++++++++++++-
.../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..fcaf86cc5ac92 100644
---
a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++
b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -171,6 +171,16 @@ 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 +291,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..539c59b1f1920 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,11 @@ 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..c4fe27d2751af 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) {
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
