diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 45 |
1 files changed, 44 insertions, 1 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 35c1e2f1..38715289 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -386,7 +386,7 @@ void SMTChecker::endVisit(BinaryOperation const& _op) void SMTChecker::endVisit(FunctionCall const& _funCall) { solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, ""); - if (_funCall.annotation().kind != FunctionCallKind::FunctionCall) + if (_funCall.annotation().kind == FunctionCallKind::StructConstructorCall) { m_errorReporter.warning( _funCall.location(), @@ -395,6 +395,12 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) return; } + if (_funCall.annotation().kind == FunctionCallKind::TypeConversion) + { + visitTypeConversion(_funCall); + return; + } + FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type); std::vector<ASTPointer<Expression const>> const args = _funCall.arguments(); @@ -571,6 +577,43 @@ void SMTChecker::endVisit(Identifier const& _identifier) } } +void SMTChecker::visitTypeConversion(FunctionCall const& _funCall) +{ + solAssert(_funCall.annotation().kind == FunctionCallKind::TypeConversion, ""); + solAssert(_funCall.arguments().size() == 1, ""); + auto argument = _funCall.arguments().at(0); + unsigned argSize = argument->annotation().type->storageBytes(); + unsigned castSize = _funCall.annotation().type->storageBytes(); + if (argSize == castSize) + defineExpr(_funCall, expr(*argument)); + else + { + createExpr(_funCall); + setUnknownValue(*m_expressions.at(&_funCall)); + auto const& funCallCategory = _funCall.annotation().type->category(); + // TODO: truncating and bytesX needs a different approach because of right padding. + if (funCallCategory == Type::Category::Integer || funCallCategory == Type::Category::Address) + { + if (argSize < castSize) + defineExpr(_funCall, expr(*argument)); + else + { + auto const& intType = dynamic_cast<IntegerType const&>(*m_expressions.at(&_funCall)->type()); + defineExpr(_funCall, smt::Expression::ite( + expr(*argument) >= minValue(intType) && expr(*argument) <= maxValue(intType), + expr(*argument), + expr(_funCall) + )); + } + } + + m_errorReporter.warning( + _funCall.location(), + "Type conversion is not yet fully supported and might yield false positives." + ); + } +} + void SMTChecker::visitFunctionIdentifier(Identifier const& _identifier) { auto const& fType = dynamic_cast<FunctionType const&>(*_identifier.annotation().type); |