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 01/10] [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 02/10] 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 <[email protected]> Date: Wed, 24 Jun 2026 15:21:58 +0000 Subject: [PATCH 03/10] 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 <[email protected]> Date: Mon, 29 Jun 2026 12:10:58 +0000 Subject: [PATCH 04/10] 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 <[email protected]> Date: Mon, 29 Jun 2026 15:02:07 +0000 Subject: [PATCH 05/10] 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 <[email protected]> Date: Mon, 29 Jun 2026 15:08:16 +0000 Subject: [PATCH 06/10] 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 <[email protected]> Date: Mon, 29 Jun 2026 15:45:13 +0000 Subject: [PATCH 07/10] 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 <[email protected]> Date: Mon, 29 Jun 2026 16:19:32 +0000 Subject: [PATCH 08/10] 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 <[email protected]> Date: Mon, 29 Jun 2026 16:21:47 +0000 Subject: [PATCH 09/10] 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 <[email protected]> Date: Tue, 30 Jun 2026 07:48:15 +0000 Subject: [PATCH 10/10] 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) { _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
