[clang] [analyzer][Z3][NFCI] Simplify getExpr* functions by taking a RetTy reference (PR #180801)
via cfe-commits
cfe-commits at lists.llvm.org
Tue Feb 10 10:26:40 PST 2026
llvmbot wrote:
<!--LLVM PR SUMMARY COMMENT-->
@llvm/pr-subscribers-clang-static-analyzer-1
Author: Balázs Benics (steakhal)
<details>
<summary>Changes</summary>
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
---
Full diff: https://github.com/llvm/llvm-project/pull/180801.diff
2 Files Affected:
- (modified) clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (+2-2)
- (modified) clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h (+35-38)
``````````diff
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());
``````````
</details>
https://github.com/llvm/llvm-project/pull/180801
More information about the cfe-commits
mailing list