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 1/2] [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 <[email protected]> Date: Wed, 24 Jun 2026 15:17:15 +0000 Subject: [PATCH 2/2] 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 _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
