https://github.com/rdevshp updated https://github.com/llvm/llvm-project/pull/205078
>From b1d7b51bd8c3af7f61244c0d2f49bbe0bb9f159f 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, 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) { _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
