https://github.com/steakhal created https://github.com/llvm/llvm-project/pull/180801
Let me start by: This is some ancient code and was never really uphold to the greatest quality standards. It turns out the `RetTy` was almost always provided, and in the cases when it wasn't, we could just pass a dummy and discard the result. Probably the APIs could be refactored, but I decided not to. The code mostly works, let's not stir up the mud. Addresses https://github.com/llvm/llvm-project/pull/168034#discussion_r2785236941 From e2c3def9f1841c4b8cdc966aba9a20b69d2d29ed Mon Sep 17 00:00:00 2001 From: Balazs Benics <[email protected]> Date: Tue, 10 Feb 2026 19:20:52 +0100 Subject: [PATCH] [analyzer][Z3][NFCI] Simplify getExpr* functions by taking a RetTy reference Let me start by: This is some ancient code and was never really uphold to the greatest quality standards. It turns out the `RetTy` was almost always provided, and in the cases when it wasn't, we could just pass a dummy and discard the result. Probably the APIs could be refactored, but I decided not to. The code mostly works, let's not stir up the mud. Addresses https://github.com/llvm/llvm-project/pull/168034#discussion_r2785236941 --- .../Core/PathSensitive/SMTConstraintManager.h | 4 +- .../Core/PathSensitive/SMTConv.h | 73 +++++++++---------- 2 files changed, 37 insertions(+), 40 deletions(-) diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index 3105dfa4dae55..7ea6d4ee3b72e 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -53,7 +53,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { bool hasComparison; llvm::SMTExprRef Exp = - SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); + SMTConv::getExpr(Solver, Ctx, Sym, RetTy, &hasComparison); // Create zero comparison for implicit boolean cast, with reversed // assumption @@ -89,7 +89,7 @@ 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 VarExp = SMTConv::getExpr(Solver, Ctx, Sym, RetTy); llvm::SMTExprRef Exp = SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true); diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h index b0673b62efffe..c8c7a1ac7cc45 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h @@ -348,29 +348,26 @@ class SMTConv { getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &LHS, QualType LTy, BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, - QualType RTy, QualType *RetTy) { + 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. - if (RetTy) { - // 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)) { - *RetTy = Ctx.BoolTy; - } else { - *RetTy = LTy; - } + // 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)) { + RetTy = Ctx.BoolTy; + } else { + RetTy = LTy; + } // If the two operands are pointers and the operation is a subtraction, // the result is of type ptrdiff_t, which is signed if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) { - *RetTy = Ctx.getPointerDiffType(); + RetTy = Ctx.getPointerDiffType(); } - } return LTy->isRealFloatingType() ? fromFloatBinOp(Solver, NewLHS, Op, NewRHS) @@ -384,13 +381,13 @@ class SMTConv { ASTContext &Ctx, const BinarySymExpr *BSE, bool *hasComparison, - QualType *RetTy) { + QualType &RetTy) { QualType LTy, RTy; BinaryOperator::Opcode Op = BSE->getOpcode(); if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) { llvm::SMTExprRef LHS = - getSymExpr(Solver, Ctx, SIE->getLHS(), <y, hasComparison); + getSymExpr(Solver, Ctx, SIE->getLHS(), LTy, hasComparison); llvm::APSInt NewRInt; std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS()); llvm::SMTExprRef RHS = @@ -404,15 +401,15 @@ class SMTConv { llvm::SMTExprRef LHS = Solver->mkBitvector(NewLInt, NewLInt.getBitWidth()); llvm::SMTExprRef RHS = - getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison); + getSymExpr(Solver, Ctx, ISE->getRHS(), RTy, hasComparison); return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); } if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) { llvm::SMTExprRef LHS = - getSymExpr(Solver, Ctx, SSM->getLHS(), <y, hasComparison); + getSymExpr(Solver, Ctx, SSM->getLHS(), LTy, hasComparison); llvm::SMTExprRef RHS = - getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison); + getSymExpr(Solver, Ctx, SSM->getRHS(), RTy, hasComparison); return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); } @@ -423,22 +420,20 @@ class SMTConv { // Sets the hasComparison and RetTy parameters. See getExpr(). static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, - QualType *RetTy, + QualType &RetTy, bool *hasComparison) { if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) { - if (RetTy) - *RetTy = Sym->getType(); + RetTy = Sym->getType(); return fromData(Solver, Ctx, SD); } if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) { - if (RetTy) - *RetTy = Sym->getType(); + RetTy = Sym->getType(); QualType FromTy; llvm::SMTExprRef Exp = - getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison); + getSymExpr(Solver, Ctx, SC->getOperand(), FromTy, hasComparison); // Casting an expression with a comparison invalidates it. Note that this // must occur after the recursive call above. @@ -449,22 +444,21 @@ class SMTConv { } if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) { - if (RetTy) - *RetTy = Sym->getType(); + RetTy = Sym->getType(); QualType OperandTy; llvm::SMTExprRef OperandExp = - getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison); + getSymExpr(Solver, Ctx, USE->getOperand(), OperandTy, hasComparison); // 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. // E.g. -(5 && a) - if (OperandTy == Ctx.BoolTy && OperandTy != *RetTy && - (*RetTy)->isIntegerType()) { - OperandExp = fromCast(Solver, OperandExp, (*RetTy), - Ctx.getTypeSize(*RetTy), OperandTy, 1); - OperandTy = (*RetTy); + if (OperandTy == Ctx.BoolTy && OperandTy != RetTy && + RetTy->isIntegerType()) { + OperandExp = fromCast(Solver, OperandExp, RetTy, Ctx.getTypeSize(RetTy), + OperandTy, 1); + OperandTy = RetTy; } llvm::SMTExprRef UnaryExp = @@ -502,7 +496,7 @@ class SMTConv { // promotions and casts. static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, - QualType *RetTy = nullptr, + QualType &RetTy, bool *hasComparison = nullptr) { if (hasComparison) { *hasComparison = false; @@ -554,12 +548,14 @@ class SMTConv { // Convert symbol QualType SymTy; - llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy); + llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, SymTy); // Construct single (in)equality - if (From == To) + if (From == To) { + QualType UnusedRetTy; return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE, - FromExp, FromTy, /*RetTy=*/nullptr); + FromExp, FromTy, /*RetTy=*/UnusedRetTy); + } QualType ToTy; llvm::APSInt NewToInt; @@ -569,12 +565,13 @@ class SMTConv { assert(FromTy == ToTy && "Range values have different types!"); // 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=*/nullptr); + FromTy, /*RetTy=*/UnusedRetTy); llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy, - /*RetTy=*/nullptr); + /*RetTy=*/UnusedRetTy); return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS, SymTy->isSignedIntegerOrEnumerationType()); _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
