| 1114 | } |
| 1115 | |
| 1116 | void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall) |
| 1117 | { |
| 1118 | solAssert(*_funCall.annotation().kind == FunctionCallKind::TypeConversion, ""); |
| 1119 | solAssert(_funCall.arguments().size() == 1, ""); |
| 1120 | |
| 1121 | auto argument = _funCall.arguments().front(); |
| 1122 | auto const argType = argument->annotation().type; |
| 1123 | auto const funCallType = _funCall.annotation().type; |
| 1124 | |
| 1125 | auto symbArg = expr(*argument, funCallType); |
| 1126 | |
| 1127 | if (smt::isStringLiteral(*argType) && smt::isFixedBytes(*funCallType)) |
| 1128 | { |
| 1129 | defineExpr(_funCall, symbArg); |
| 1130 | return; |
| 1131 | } |
| 1132 | |
| 1133 | ArrayType const* arrayType = dynamic_cast<ArrayType const*>(argType); |
| 1134 | if (auto sliceType = dynamic_cast<ArraySliceType const*>(argType)) |
| 1135 | arrayType = &sliceType->arrayType(); |
| 1136 | |
| 1137 | if (arrayType && arrayType->isByteArrayOrString() && smt::isFixedBytes(*funCallType)) |
| 1138 | { |
| 1139 | auto array = std::dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*argument)); |
| 1140 | bytesToFixedBytesAssertions(*array, _funCall); |
| 1141 | return; |
| 1142 | } |
| 1143 | |
| 1144 | // TODO Simplify this whole thing for 0.8.0 where weird casts are disallowed. |
| 1145 | |
| 1146 | unsigned argSize = argType->storageBytes(); |
| 1147 | unsigned castSize = funCallType->storageBytes(); |
| 1148 | bool castIsSigned = smt::isNumber(*funCallType) && smt::isSigned(funCallType); |
| 1149 | bool argIsSigned = smt::isNumber(*argType) && smt::isSigned(argType); |
| 1150 | std::optional<smtutil::Expression> symbMin; |
| 1151 | std::optional<smtutil::Expression> symbMax; |
| 1152 | if (smt::isNumber(*funCallType)) |
| 1153 | { |
| 1154 | symbMin = smt::minValue(funCallType); |
| 1155 | symbMax = smt::maxValue(funCallType); |
| 1156 | } |
| 1157 | if (argSize == castSize) |
| 1158 | { |
| 1159 | // If sizes are the same, it's possible that the signs are different. |
| 1160 | if (smt::isNumber(*funCallType) && smt::isNumber(*argType)) |
| 1161 | { |
| 1162 | // castIsSigned && !argIsSigned => might overflow if arg > castType.max |
| 1163 | // !castIsSigned && argIsSigned => might underflow if arg < castType.min |
| 1164 | // !castIsSigned && !argIsSigned => ok |
| 1165 | // castIsSigned && argIsSigned => ok |
| 1166 | |
| 1167 | if (castIsSigned && !argIsSigned) |
| 1168 | { |
| 1169 | auto wrap = smtutil::Expression::ite( |
| 1170 | symbArg > *symbMax, |
| 1171 | symbArg - (*symbMax - *symbMin + 1), |
| 1172 | symbArg |
| 1173 | ); |
nothing calls this directly
no test coverage detected