From 5b5e853ea0a1ddbe9be93e29a6477d12039535dc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= Date: Sat, 28 Jan 2023 03:20:43 +0100 Subject: [PATCH] Warn about missing user-defined operator support in SMTChecker --- libsolidity/formal/SMTEncoder.cpp | 34 ++++++++++++++++++++++++++++--- 1 file changed, 31 insertions(+), 3 deletions(-) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 5c4fc5ded..e8598392f 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -449,11 +449,25 @@ void SMTEncoder::endVisit(UnaryOperation const& _op) if (_op.annotation().type->category() == Type::Category::RationalNumber) return; - if (TokenTraits::isBitOp(_op.getOperator())) + if (TokenTraits::isBitOp(_op.getOperator()) && !*_op.annotation().userDefinedFunction) return bitwiseNotOperation(_op); createExpr(_op); + // User-defined operators are essentially function calls. + if (*_op.annotation().userDefinedFunction) + { + // TODO: Implement user-defined operators properly. + m_errorReporter.warning( + 6156_error, + _op.location(), + "User-defined operators are not yet supported by SMTChecker. "s + + "This invocation of operator " + TokenTraits::friendlyName(_op.getOperator()) + + " has been ignored, which may lead to incorrect results." + ); + return; + } + auto const* subExpr = innermostTuple(_op.subExpression()); auto type = _op.annotation().type; switch (_op.getOperator()) @@ -524,7 +538,7 @@ bool SMTEncoder::visit(BinaryOperation const& _op) { if (shortcutRationalNumber(_op)) return false; - if (TokenTraits::isBooleanOp(_op.getOperator())) + if (TokenTraits::isBooleanOp(_op.getOperator()) && !*_op.annotation().userDefinedFunction) { booleanOperation(_op); return false; @@ -537,11 +551,25 @@ void SMTEncoder::endVisit(BinaryOperation const& _op) /// If _op is const evaluated the RationalNumber shortcut was taken. if (isConstant(_op)) return; - if (TokenTraits::isBooleanOp(_op.getOperator())) + if (TokenTraits::isBooleanOp(_op.getOperator()) && !*_op.annotation().userDefinedFunction) return; createExpr(_op); + // User-defined operators are essentially function calls. + if (*_op.annotation().userDefinedFunction) + { + // TODO: Implement user-defined operators properly. + m_errorReporter.warning( + 6756_error, + _op.location(), + "User-defined operators are not yet supported by SMTChecker. "s + + "This invocation of operator " + TokenTraits::friendlyName(_op.getOperator()) + + " has been ignored, which may lead to incorrect results." + ); + return; + } + if (TokenTraits::isArithmeticOp(_op.getOperator())) arithmeticOperation(_op); else if (TokenTraits::isCompareOp(_op.getOperator()))