================
@@ -270,8 +274,14 @@ class SMTConv {
QualType ToTy, uint64_t ToBitWidth,
QualType FromTy,
uint64_t FromBitWidth) {
- if ((FromTy.getAtomicUnqualifiedType()->isIntegralOrEnumerationType() &&
- ToTy.getAtomicUnqualifiedType()->isIntegralOrEnumerationType()) ||
+ FromTy = getSymbolicValueType(FromTy);
+ ToTy = getSymbolicValueType(ToTy);
+
+ if (FromTy == ToTy && FromBitWidth == ToBitWidth)
+ return Exp;
----------------
rdevshp wrote:
The callers to fromCast are
1. SMTConf.h:354 getCastExpr
```
return fromCast(Solver, Exp, ToTy, SMTConv::getSMTBitWidth(Ctx, ToTy),
FromTy, SMTConv::getSMTBitWidth(Ctx, FromTy));
```
If FromTy and ToTy are both Bool, the early return in fromCast would apply.
2. SMTConv.h:520 the fromCast call in
```
std::optional<llvm::SMTExprRef>
getSymExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
QualType &RetTy, bool *hasComparison)
```
```
OperandExp = fromCast(Solver, OperandExp.value(), RetTy,
Ctx.getTypeSize(RetTy), OperandTy, 1);
```
This call is gated by OperandTy != RetTy, both of which are canonicalized, so
it can't be the case that both types are Bool for this fromCast call.
3. SMTConv.h:669:
```
SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>(
Solver, Ctx, LHS, LTy, RHS, RTy);
```
In this call, doIntTypeConversion would promote the Bool type, so it also can't
be the case that fromCast is called with both FromTy/ToTy types to be Bool.
4. SMTConv.h: 675:
```
SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(
Solver, Ctx, LHS, LTy, RHS, RTy);
```
It can't be the case that both LTy and RTy is Bool because it requires
LTy->isRealFloatingType() || RTy->isRealFloatingType().
5. SMTConf.h: 691:
```
if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
(LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
(LTy->isReferenceType() ^ RTy->isReferenceType())) {
if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
LTy->isReferenceType()) {
LHS = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
LTy = RTy;
} else {
RHS = fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
RTy = LTy;
}
}
```
The condition in this case requires at least one non-Bool type, so this is not
affected.
https://github.com/llvm/llvm-project/pull/212050
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
