From 78eb37d2596c9416b3fac9881414bf7e9c524de8 Mon Sep 17 00:00:00 2001 From: Pawel Gebal Date: Tue, 8 Aug 2023 17:48:38 +0200 Subject: [PATCH 1/4] Support user defined operators in SMT --- Changelog.md | 1 + libsolidity/ast/AST.h | 3 + libsolidity/formal/BMC.cpp | 62 ++++++-- libsolidity/formal/BMC.h | 8 ++ libsolidity/formal/CHC.cpp | 136 +++++++++++++----- libsolidity/formal/CHC.h | 18 ++- libsolidity/formal/SMTEncoder.cpp | 58 +++----- libsolidity/formal/SMTEncoder.h | 9 +- .../user_defined_division_same_as_builtin.sol | 6 +- ...ed_division_with_safe_division_by_zero.sol | 2 +- .../user_defined_operations_on_constants.sol | 76 +++------- ...r_defined_operations_on_constants_fail.sol | 27 +--- ...rator_matches_equivalent_function_call.sol | 98 +++++-------- .../userDefined/user_defined_overflow.sol | 8 +- 14 files changed, 267 insertions(+), 245 deletions(-) diff --git a/Changelog.md b/Changelog.md index 57175dcc79d3..9c64ba690eea 100644 --- a/Changelog.md +++ b/Changelog.md @@ -8,6 +8,7 @@ Compiler Features: * Commandline Interface: Add ``--no-import-callback`` option that prevents the compiler from loading source files not given explicitly on the CLI or in Standard JSON input. * Commandline Interface: Use proper severity and coloring also for error messages produced outside of the compilation pipeline. * Parser: Remove the experimental error recovery mode (``--error-recovery`` / ``settings.parserErrorRecovery``). + * SMTChecker: Support user-defined operators. * Yul Optimizer: If ``PUSH0`` is supported, favor zero literals over storing zero values in variables. * Yul Optimizer: Run the ``Rematerializer`` and ``UnusedPruner`` steps at the end of the default clean-up sequence. diff --git a/libsolidity/ast/AST.h b/libsolidity/ast/AST.h index ca23b0d61975..d651df33bebc 100644 --- a/libsolidity/ast/AST.h +++ b/libsolidity/ast/AST.h @@ -2111,6 +2111,7 @@ class UnaryOperation: public Expression Token getOperator() const { return m_operator; } bool isPrefixOperation() const { return m_isPrefix; } Expression const& subExpression() const { return *m_subExpression; } + ASTPointer const& argument() const { return m_subExpression; } FunctionType const* userDefinedFunctionType() const; @@ -2145,6 +2146,8 @@ class BinaryOperation: public Expression Expression const& leftExpression() const { return *m_left; } Expression const& rightExpression() const { return *m_right; } + ASTPointer leftArgument() const { return m_left; } + ASTPointer rightArgument() const { return m_right; } Token getOperator() const { return m_operator; } FunctionType const* userDefinedFunctionType() const; diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index dede97cc036e..d8f30368812f 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -551,6 +551,15 @@ void BMC::endVisit(UnaryOperation const& _op) { SMTEncoder::endVisit(_op); + // User-defined operators are essentially function calls. + if (auto funDef = *_op.annotation().userDefinedFunction) + { + std::vector> arguments; + arguments.push_back(_op.argument()); + inlineFunctionCall(funDef, _op, &_op, _op.userDefinedFunctionType(), arguments); + return; + } + if ( _op.annotation().type->category() == Type::Category::RationalNumber || _op.annotation().type->category() == Type::Category::FixedPoint @@ -565,6 +574,19 @@ void BMC::endVisit(UnaryOperation const& _op) ); } +void BMC::endVisit(BinaryOperation const& _op) +{ + SMTEncoder::endVisit(_op); + + if (auto funDef = *_op.annotation().userDefinedFunction) + { + std::vector> arguments; + arguments.push_back(_op.leftArgument()); + arguments.push_back(_op.rightArgument()); + inlineFunctionCall(funDef, _op, &_op, _op.userDefinedFunctionType(), arguments); + } +} + void BMC::endVisit(FunctionCall const& _funCall) { auto functionCallKind = *_funCall.annotation().kind; @@ -674,15 +696,21 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall) SMTEncoder::visitAddMulMod(_funCall); } -void BMC::inlineFunctionCall(FunctionCall const& _funCall) +void BMC::inlineFunctionCall( + FunctionDefinition const* _funDef, + Expression const& _callStackExpr, + Expression const* _calledExpr, + FunctionType const* _funType, + std::vector> const& _arguments +) { - solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), ""); - auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); - solAssert(funDef, ""); + solAssert(_funDef, ""); + solAssert(_funType, ""); + solAssert(_calledExpr, ""); - if (visitedFunction(funDef)) + if (visitedFunction(_funDef)) { - auto const& returnParams = funDef->returnParameters(); + auto const& returnParams = _funDef->returnParameters(); for (auto param: returnParams) { m_context.newValue(*param); @@ -691,19 +719,31 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall) } else { - initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall, m_currentContract)); + initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef, _calledExpr, _funType, _arguments)); // The reason why we need to pushCallStack here instead of visit(FunctionDefinition) - // is that there we don't have `_funCall`. - pushCallStack({funDef, &_funCall}); + // is that there we don't have `_callStackExpr`. + pushCallStack({_funDef, &_callStackExpr}); pushPathCondition(currentPathConditions()); auto oldChecked = std::exchange(m_checked, true); - funDef->accept(*this); + _funDef->accept(*this); m_checked = oldChecked; popPathCondition(); } - createReturnedExpressions(_funCall, m_currentContract); + createReturnedExpressions(_funDef, _callStackExpr); +} + +void BMC::inlineFunctionCall(FunctionCall const& _funCall) +{ + solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), ""); + + auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); + Expression const* calledExpr = &_funCall.expression(); + auto funType = dynamic_cast(calledExpr->annotation().type); + std::vector> arguments = _funCall.sortedArguments(); + + inlineFunctionCall(funDef, _funCall, calledExpr, funType, arguments); } void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall) diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index dfd4169e2998..4aceadeea60f 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -97,6 +97,7 @@ class BMC: public SMTEncoder bool visit(WhileStatement const& _node) override; bool visit(ForStatement const& _node) override; void endVisit(UnaryOperation const& _node) override; + void endVisit(BinaryOperation const& _node) override; void endVisit(FunctionCall const& _node) override; void endVisit(Return const& _node) override; bool visit(TryStatement const& _node) override; @@ -113,6 +114,13 @@ class BMC: public SMTEncoder /// Visits the FunctionDefinition of the called function /// if available and inlines the return value. void inlineFunctionCall(FunctionCall const& _funCall); + void inlineFunctionCall( + FunctionDefinition const* _funDef, + Expression const& _callStackExpr, + Expression const* _calledExpr, + FunctionType const* _funType, + std::vector> const& _arguments + ); /// Inlines if the function call is internal or external to `this`. /// Erases knowledge about state variables if external. void internalOrExternalFunctionCall(FunctionCall const& _funCall); diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index a803f87d0a1c..bf19090f561e 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -543,6 +543,35 @@ void CHC::endVisit(ForStatement const& _for) m_scopes.pop_back(); } +void CHC::endVisit(UnaryOperation const& _op) +{ + SMTEncoder::endVisit(_op); + + if (auto funDef = *_op.annotation().userDefinedFunction) + { + std::vector> arguments; + arguments.push_back(_op.argument()); + internalFunctionCall(funDef, &_op, _op.userDefinedFunctionType(), arguments, state().thisAddress()); + + createReturnedExpressions(funDef, _op); + } +} + +void CHC::endVisit(BinaryOperation const& _op) +{ + SMTEncoder::endVisit(_op); + + if (auto funDef = *_op.annotation().userDefinedFunction) + { + std::vector> arguments; + arguments.push_back(_op.leftArgument()); + arguments.push_back(_op.rightArgument()); + internalFunctionCall(funDef, &_op, _op.userDefinedFunctionType(), arguments, state().thisAddress()); + + createReturnedExpressions(funDef, _op); + } +} + void CHC::endVisit(FunctionCall const& _funCall) { auto functionCallKind = *_funCall.annotation().kind; @@ -593,8 +622,8 @@ void CHC::endVisit(FunctionCall const& _funCall) break; } - - createReturnedExpressions(_funCall, m_currentContract); + auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); + createReturnedExpressions(funDef, _funCall); } void CHC::endVisit(Break const& _break) @@ -820,20 +849,27 @@ void CHC::visitDeployment(FunctionCall const& _funCall) defineExpr(_funCall, newAddr); } -void CHC::internalFunctionCall(FunctionCall const& _funCall) +void CHC::internalFunctionCall( + FunctionDefinition const* _funDef, + Expression const* _calledExpr, + FunctionType const* _funType, + std::vector> const& _arguments, + smtutil::Expression _contractAddressValue +) { solAssert(m_currentContract, ""); + solAssert(_calledExpr, ""); + solAssert(_funType, ""); - auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); - if (function) + if (_funDef) { if (m_currentFunction && !m_currentFunction->isConstructor()) - m_callGraph[m_currentFunction].insert(function); + m_callGraph[m_currentFunction].insert(_funDef); else - m_callGraph[m_currentContract].insert(function); + m_callGraph[m_currentContract].insert(_funDef); } - m_context.addAssertion(predicate(_funCall)); + m_context.addAssertion(predicate(_funDef, _calledExpr, _funType, _arguments, _contractAddressValue)); solAssert(m_errorDest, ""); connectBlocks( @@ -845,6 +881,37 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall) m_context.addAssertion(errorFlag().increaseIndex() == 0); } +void CHC::internalFunctionCall(FunctionCall const& _funCall) +{ + solAssert(m_currentContract, ""); + + auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); + if (funDef) + { + if (m_currentFunction && !m_currentFunction->isConstructor()) + m_callGraph[m_currentFunction].insert(funDef); + else + m_callGraph[m_currentContract].insert(funDef); + } + + Expression const* calledExpr = &_funCall.expression(); + auto funType = dynamic_cast(calledExpr->annotation().type); + std::vector> arguments = _funCall.sortedArguments(); + + auto contractAddressValue = [this](FunctionCall const& _f) { + auto [callExpr, callOptions] = functionCallExpression(_f); + + FunctionType const& funType = dynamic_cast(*callExpr->annotation().type); + if (funType.kind() == FunctionType::Kind::Internal) + return state().thisAddress(); + if (MemberAccess const* callBase = dynamic_cast(callExpr)) + return expr(callBase->expression()); + solAssert(false, "Unreachable!"); + }; + + internalFunctionCall(funDef, calledExpr, funType, arguments, contractAddressValue(_funCall)); +} + void CHC::addNondetCalls(ContractDefinition const& _contract) { for (auto var: _contract.stateVariables()) @@ -1028,7 +1095,7 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall) state().readStateVars(*function->annotation().contract, contractAddressValue(_funCall)); } - smtutil::Expression pred = predicate(_funCall); + smtutil::Expression pred = predicate(function, callExpr, &funType, _funCall.sortedArguments(), calledAddress); auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(*function); m_context.addAssertion(pred && txConstraints); @@ -1264,6 +1331,12 @@ std::set CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot return verificationTargetsIds; } +bool CHC::usesStaticCall(FunctionDefinition const* _funDef, FunctionType const* _funType) +{ + auto kind = _funType->kind(); + return (_funDef && (_funDef->stateMutability() == StateMutability::Pure || _funDef->stateMutability() == StateMutability::View)) || kind == FunctionType::Kind::BareStaticCall; +} + bool CHC::usesStaticCall(FunctionCall const& _funCall) { FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); @@ -1733,40 +1806,35 @@ smtutil::Expression CHC::predicate(Predicate const& _block) solAssert(false, ""); } -smtutil::Expression CHC::predicate(FunctionCall const& _funCall) +smtutil::Expression CHC::predicate( + FunctionDefinition const* _funDef, + Expression const* _calledExpr, + FunctionType const* _funType, + std::vector> _arguments, + smtutil::Expression _contractAddressValue +) { - FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); - auto kind = funType.kind(); + solAssert(_calledExpr, ""); + solAssert(_funType, ""); + auto kind = _funType->kind(); solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); - - solAssert(m_currentContract, ""); - auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); - if (!function) + if (!_funDef) return smtutil::Expression(true); - auto contractAddressValue = [this](FunctionCall const& _f) { - auto [callExpr, callOptions] = functionCallExpression(_f); - - FunctionType const& funType = dynamic_cast(*callExpr->annotation().type); - if (funType.kind() == FunctionType::Kind::Internal) - return state().thisAddress(); - if (MemberAccess const* callBase = dynamic_cast(callExpr)) - return expr(callBase->expression()); - solAssert(false, "Unreachable!"); - }; errorFlag().increaseIndex(); - std::vector args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()}; - auto const* contract = function->annotation().contract; + std::vector args{errorFlag().currentValue(), _contractAddressValue, state().abi(), state().crypto(), state().tx(), state().state()}; + + auto const* contract = _funDef->annotation().contract; auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; - solAssert(kind != FunctionType::Kind::Internal || function->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), ""); + solAssert(kind != FunctionType::Kind::Internal || _funDef->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), ""); if (kind == FunctionType::Kind::Internal) contract = m_currentContract; args += currentStateVariables(*contract); - args += symbolicArguments(_funCall, contract); - if (!usesStaticCall(_funCall)) + args += symbolicArguments(_funDef, _calledExpr, _funType, _arguments); + if (!usesStaticCall(_funDef, _funType)) { state().newState(); for (auto const& var: stateVariablesIncludingInheritedAndPrivate(*contract)) @@ -1775,7 +1843,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) args += std::vector{state().state()}; args += currentStateVariables(*contract); - for (auto var: function->parameters() + function->returnParameters()) + for (auto var: _funDef->parameters() + _funDef->returnParameters()) { if (m_context.knownVariable(*var)) m_context.variable(*var)->increaseIndex(); @@ -1784,10 +1852,10 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) args.push_back(currentValue(*var)); } - Predicate const& summary = *m_summaries.at(contract).at(function); + Predicate const& summary = *m_summaries.at(contract).at(_funDef); auto from = smt::function(summary, contract, m_context); Predicate const& callPredicate = *createSummaryBlock( - *function, + *_funDef, *contract, kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted ); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 27bdaebf2264..57bf8073846b 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -111,6 +111,8 @@ class CHC: public SMTEncoder bool visit(ForStatement const&) override; void endVisit(ForStatement const&) override; void endVisit(FunctionCall const& _node) override; + void endVisit(BinaryOperation const& _op) override; + void endVisit(UnaryOperation const& _op) override; void endVisit(Break const& _node) override; void endVisit(Continue const& _node) override; void endVisit(IndexRangeAccess const& _node) override; @@ -127,6 +129,13 @@ class CHC: public SMTEncoder void visitAddMulMod(FunctionCall const& _funCall) override; void visitDeployment(FunctionCall const& _funCall); void internalFunctionCall(FunctionCall const& _funCall); + void internalFunctionCall( + FunctionDefinition const* _funDef, + Expression const* _calledExpr, + FunctionType const* _funType, + std::vector> const& _arguments, + smtutil::Expression _contractAddressValue + ); void externalFunctionCall(FunctionCall const& _funCall); void externalFunctionCallToTrustedCode(FunctionCall const& _funCall); void addNondetCalls(ContractDefinition const& _contract); @@ -152,6 +161,7 @@ class CHC: public SMTEncoder void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override; void setCurrentBlock(Predicate const& _block); std::set transactionVerificationTargetsIds(ASTNode const* _txRoot); + bool usesStaticCall(FunctionDefinition const* _funDef, FunctionType const* _funType); bool usesStaticCall(FunctionCall const& _funCall); //@} @@ -246,7 +256,13 @@ class CHC: public SMTEncoder /// @returns a predicate application after checking the predicate's type. smtutil::Expression predicate(Predicate const& _block); /// @returns the summary predicate for the called function. - smtutil::Expression predicate(FunctionCall const& _funCall); + smtutil::Expression predicate( + FunctionDefinition const* _funDef, + Expression const* _calledExpr, + FunctionType const* _funType, + std::vector> _arguments, + smtutil::Expression _contractAddressValue + ); /// @returns a predicate that defines a contract initializer for _contract in the context of _contractContext. smtutil::Expression initializer(ContractDefinition const& _contract, ContractDefinition const& _contractContext); /// @returns a predicate that defines a constructor summary. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index d985e359effe..abb47fdd3b7c 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -459,17 +459,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op) // User-defined operators are essentially function calls. if (*_op.annotation().userDefinedFunction) - { - // TODO: Implement user-defined operators properly. - m_unsupportedErrors.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; @@ -561,17 +551,7 @@ void SMTEncoder::endVisit(BinaryOperation const& _op) // User-defined operators are essentially function calls. if (*_op.annotation().userDefinedFunction) - { - // TODO: Implement user-defined operators properly. - m_unsupportedErrors.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); @@ -3141,47 +3121,45 @@ std::set SMTEncoder::sourceDependencies return sources; } -void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract) +void SMTEncoder::createReturnedExpressions(FunctionDefinition const* _funDef, Expression const& _callStackExpr) { - auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract); - if (!funDef) + if (!_funDef) return; - auto const& returnParams = funDef->returnParameters(); + auto const& returnParams = _funDef->returnParameters(); for (auto param: returnParams) createVariable(*param); auto returnValues = applyMap(returnParams, [this](auto const& param) -> std::optional { solAssert(param && m_context.knownVariable(*param), ""); return currentValue(*param); }); - defineExpr(_funCall, returnValues); + defineExpr(_callStackExpr, returnValues); } -std::vector SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract) +std::vector SMTEncoder::symbolicArguments( + FunctionDefinition const* _funDef, + Expression const* _calledExpr, + FunctionType const* _funType, + std::vector> const& _arguments) { - auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract); - solAssert(funDef, ""); + solAssert(_funDef, ""); + solAssert(_funType, ""); std::vector args; - Expression const* calledExpr = &_funCall.expression(); - auto funType = dynamic_cast(calledExpr->annotation().type); - solAssert(funType, ""); - - std::vector> arguments = _funCall.sortedArguments(); - auto functionParams = funDef->parameters(); + auto functionParams = _funDef->parameters(); unsigned firstParam = 0; - if (funType->hasBoundFirstArgument()) + if (_funType->hasBoundFirstArgument()) { - calledExpr = innermostTuple(*calledExpr); - auto const& attachedFunction = dynamic_cast(calledExpr); + _calledExpr = innermostTuple(*_calledExpr); + auto const& attachedFunction = dynamic_cast(_calledExpr); solAssert(attachedFunction, ""); args.push_back(expr(attachedFunction->expression(), functionParams.front()->type())); firstParam = 1; } - solAssert((arguments.size() + firstParam) == functionParams.size(), ""); - for (unsigned i = 0; i < arguments.size(); ++i) - args.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type())); + solAssert((_arguments.size() + firstParam) == functionParams.size(), ""); + for (unsigned i = 0; i < _arguments.size(); ++i) + args.push_back(expr(*_arguments.at(i), functionParams.at(i + firstParam)->type())); return args; } diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 726f16ef6bc9..e88a2400e6a9 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -403,12 +403,17 @@ class SMTEncoder: public ASTConstVisitor /// Creates symbolic expressions for the returned values /// and set them as the components of the symbolic tuple. - void createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract); + void createReturnedExpressions(FunctionDefinition const* _funDef, Expression const& _calledExpr); /// @returns the symbolic arguments for a function call, /// taking into account attached functions and /// type conversion. - std::vector symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract); + std::vector symbolicArguments( + FunctionDefinition const* _funDef, + Expression const* _calledExpr, + FunctionType const* _funType, + std::vector> const& _arguments + ); smtutil::Expression constantExpr(Expression const& _expr, VariableDeclaration const& _var); diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_same_as_builtin.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_same_as_builtin.sol index 20889af057c8..1e94e41d4a62 100644 --- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_same_as_builtin.sol +++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_same_as_builtin.sol @@ -2,15 +2,15 @@ type U is uint; using {div as /} for U global; function div(U x, U y) pure returns (U) { - return U.wrap(U.unwrap(x) / U.unwrap(y)); + return U.wrap(U.unwrap(x) / U.unwrap(y)); // detects division by zero } contract C { function f(U x, U y) public pure returns (U) { - return x / y; // FIXME: should detect div by zero + return x / y; // reports division by zero in the implementation } } // ==== // SMTEngine: all // ---- -// Warning 6756: (218-223): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results. +// Warning 4281: (108-133): CHC: Division by zero happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_with_safe_division_by_zero.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_with_safe_division_by_zero.sol index edc4d2a9791c..8f8e6c53c411 100644 --- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_with_safe_division_by_zero.sol +++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_with_safe_division_by_zero.sol @@ -16,4 +16,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6756: (271-276): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants.sol index 10ec6a199320..c39360b656d2 100644 --- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants.sol +++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants.sol @@ -33,72 +33,32 @@ contract C { I16 constant FOUR = I16.wrap(4); function testBitwise() public pure { - assert(ONE | TWO == THREE); // FIXME: should hold - assert(ONE & THREE == ZERO); // FIXME: should hold - assert(TWO ^ TWO == ZERO); // FIXME: should hold - assert(~ONE == MINUS_TWO); // FIXME: should hold + assert(ONE | TWO == THREE); + assert(ONE & THREE == ONE); + assert(TWO ^ TWO == ZERO); + assert(~ONE == MINUS_TWO); } function testArithmetic() public pure { - assert(TWO + TWO == FOUR); // FIXME: should hold - assert(TWO - TWO == ZERO); // FIXME: should hold - assert(-TWO == MINUS_TWO); // FIXME: should hold - assert(TWO * TWO == FOUR); // FIXME: should hold - assert(TWO / TWO == ONE); // FIXME: should hold - assert(TWO % TWO == ZERO); // FIXME: should hold + assert(TWO + TWO == FOUR); + assert(TWO - TWO == ZERO); + assert(-TWO == MINUS_TWO); + assert(TWO * TWO == FOUR); + assert(TWO / TWO == ONE); + assert(TWO % TWO == ZERO); } function testComparison() public pure { - assert(TWO == TWO); // FIXME: should hold - assert(!(TWO != TWO)); // FIXME: should hold - assert(!(TWO < TWO)); // FIXME: should hold - assert(!(TWO > TWO)); // FIXME: should hold - assert(TWO <= TWO); // FIXME: should hold - assert(TWO >= TWO); // FIXME: should hold + assert(TWO == TWO); + assert(!(TWO != TWO)); + assert(!(TWO < TWO)); + assert(!(TWO > TWO)); + assert(TWO <= TWO); + assert(TWO >= TWO); } } // ==== // SMTEngine: all // ---- -// Warning 6756: (2019-2028): User-defined operators are not yet supported by SMTChecker. This invocation of operator | has been ignored, which may lead to incorrect results. -// Warning 6756: (2019-2037): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2077-2088): User-defined operators are not yet supported by SMTChecker. This invocation of operator & has been ignored, which may lead to incorrect results. -// Warning 6756: (2077-2096): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2136-2145): User-defined operators are not yet supported by SMTChecker. This invocation of operator ^ has been ignored, which may lead to incorrect results. -// Warning 6756: (2136-2153): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6156: (2193-2197): User-defined operators are not yet supported by SMTChecker. This invocation of operator ~ has been ignored, which may lead to incorrect results. -// Warning 6756: (2193-2210): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2301-2310): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results. -// Warning 6756: (2301-2318): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2358-2367): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results. -// Warning 6756: (2358-2375): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6156: (2415-2419): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results. -// Warning 6756: (2415-2432): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2472-2481): User-defined operators are not yet supported by SMTChecker. This invocation of operator * has been ignored, which may lead to incorrect results. -// Warning 6756: (2472-2489): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2529-2538): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results. -// Warning 6756: (2529-2545): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2585-2594): User-defined operators are not yet supported by SMTChecker. This invocation of operator % has been ignored, which may lead to incorrect results. -// Warning 6756: (2585-2602): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2693-2703): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2745-2755): User-defined operators are not yet supported by SMTChecker. This invocation of operator != has been ignored, which may lead to incorrect results. -// Warning 6756: (2798-2807): User-defined operators are not yet supported by SMTChecker. This invocation of operator < has been ignored, which may lead to incorrect results. -// Warning 6756: (2850-2859): User-defined operators are not yet supported by SMTChecker. This invocation of operator > has been ignored, which may lead to incorrect results. -// Warning 6756: (2900-2910): User-defined operators are not yet supported by SMTChecker. This invocation of operator <= has been ignored, which may lead to incorrect results. -// Warning 6756: (2950-2960): User-defined operators are not yet supported by SMTChecker. This invocation of operator >= has been ignored, which may lead to incorrect results. -// Warning 6328: (2012-2038): CHC: Assertion violation happens here. -// Warning 6328: (2070-2097): CHC: Assertion violation happens here. -// Warning 6328: (2129-2154): CHC: Assertion violation happens here. -// Warning 6328: (2186-2211): CHC: Assertion violation happens here. -// Warning 6328: (2294-2319): CHC: Assertion violation happens here. -// Warning 6328: (2351-2376): CHC: Assertion violation happens here. -// Warning 6328: (2408-2433): CHC: Assertion violation happens here. -// Warning 6328: (2465-2490): CHC: Assertion violation happens here. -// Warning 6328: (2522-2546): CHC: Assertion violation happens here. -// Warning 6328: (2578-2603): CHC: Assertion violation happens here. -// Warning 6328: (2686-2704): CHC: Assertion violation happens here. -// Warning 6328: (2736-2757): CHC: Assertion violation happens here. -// Warning 6328: (2789-2809): CHC: Assertion violation happens here. -// Warning 6328: (2841-2861): CHC: Assertion violation happens here. -// Warning 6328: (2893-2911): CHC: Assertion violation happens here. -// Warning 6328: (2943-2961): CHC: Assertion violation happens here. +// Info 1391: CHC: 21 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. + diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants_fail.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants_fail.sol index c30bb21c1da5..25674513c0de 100644 --- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants_fail.sol +++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants_fail.sol @@ -60,32 +60,6 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6756: (2019-2028): User-defined operators are not yet supported by SMTChecker. This invocation of operator | has been ignored, which may lead to incorrect results. -// Warning 6756: (2019-2036): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2069-2080): User-defined operators are not yet supported by SMTChecker. This invocation of operator & has been ignored, which may lead to incorrect results. -// Warning 6756: (2069-2088): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2121-2130): User-defined operators are not yet supported by SMTChecker. This invocation of operator ^ has been ignored, which may lead to incorrect results. -// Warning 6756: (2121-2138): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6156: (2171-2175): User-defined operators are not yet supported by SMTChecker. This invocation of operator ~ has been ignored, which may lead to incorrect results. -// Warning 6756: (2171-2183): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2267-2278): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results. -// Warning 6756: (2267-2286): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2319-2328): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results. -// Warning 6756: (2319-2336): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6156: (2369-2373): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results. -// Warning 6756: (2369-2381): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2414-2425): User-defined operators are not yet supported by SMTChecker. This invocation of operator * has been ignored, which may lead to incorrect results. -// Warning 6756: (2414-2433): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2466-2475): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results. -// Warning 6756: (2466-2483): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2516-2525): User-defined operators are not yet supported by SMTChecker. This invocation of operator % has been ignored, which may lead to incorrect results. -// Warning 6756: (2516-2533): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2619-2629): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2663-2673): User-defined operators are not yet supported by SMTChecker. This invocation of operator != has been ignored, which may lead to incorrect results. -// Warning 6756: (2706-2715): User-defined operators are not yet supported by SMTChecker. This invocation of operator < has been ignored, which may lead to incorrect results. -// Warning 6756: (2748-2757): User-defined operators are not yet supported by SMTChecker. This invocation of operator > has been ignored, which may lead to incorrect results. -// Warning 6756: (2792-2802): User-defined operators are not yet supported by SMTChecker. This invocation of operator <= has been ignored, which may lead to incorrect results. -// Warning 6756: (2838-2848): User-defined operators are not yet supported by SMTChecker. This invocation of operator >= has been ignored, which may lead to incorrect results. // Warning 6328: (2012-2037): CHC: Assertion violation happens here. // Warning 6328: (2062-2089): CHC: Assertion violation happens here. // Warning 6328: (2114-2139): CHC: Assertion violation happens here. @@ -102,3 +76,4 @@ contract C { // Warning 6328: (2741-2758): CHC: Assertion violation happens here. // Warning 6328: (2783-2804): CHC: Assertion violation happens here. // Warning 6328: (2829-2850): CHC: Assertion violation happens here. +// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol index 9d09e2f296ee..a6cad9580f72 100644 --- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol +++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol @@ -17,6 +17,7 @@ function mul(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) * function div(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) / I16.unwrap(y)); } function mod(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) % I16.unwrap(y)); } + function eq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) == I16.unwrap(y); } function noteq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) != I16.unwrap(y); } function lt(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) < I16.unwrap(y); } @@ -26,81 +27,48 @@ function geq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) >= I16.unw contract C { function testBitwise(I16 x, I16 y) public pure { - assert(x | y == bitor(x, y)); // FIXME: should hold - assert(x & y == bitand(x, y)); // FIXME: should hold - assert(x ^ y == bitxor(x, y)); // FIXME: should hold - assert(~x == bitnot(x)); // FIXME: should hold + assert(x | y == bitor(x, y)); // should hold + assert(x & y == bitand(x, y)); // should hold + assert(x ^ y == bitxor(x, y)); // should hold + assert(~x == bitnot(x)); // should hold } function testArithmetic(I16 x, I16 y) public pure { - assert(x + y == add(x, y)); // FIXME: should hold - assert(x - y == sub(x, y)); // FIXME: should hold - assert(-x == unsub(x)); // FIXME: should hold - assert(x * y == mul(x, y)); // FIXME: should hold - assert(x / y == div(x, y)); // FIXME: should hold - assert(x % y == mod(x, y)); // FIXME: should hold + assert(x + y == add(x, y)); + assert(x - y == sub(x, y)); + assert(-x == unsub(x)); + assert(x * y == mul(x, y)); + assert(x / y == div(x, y)); + assert(x % y == mod(x, y)); } function testComparison(I16 x, I16 y) public pure { - assert((x == y) == eq(x, y)); // FIXME: should hold - assert((x != y) == noteq(x, y)); // FIXME: should hold - assert((x < y) == lt(x, y)); // FIXME: should hold - assert((x > y) == gt(x, y)); // FIXME: should hold - assert((x <= y) == leq(x, y)); // FIXME: should hold - assert((x >= y) == geq(x, y)); // FIXME: should hold + assert((x == y) == eq(x, y)); // should hold + assert((x != y) == noteq(x, y)); // should hold + assert((x < y) == lt(x, y)); // should hold + assert((x > y) == gt(x, y)); // should hold + assert((x <= y) == leq(x, y)); // should hold + assert((x >= y) == geq(x, y)); // should hold } } // ==== // SMTEngine: all +// SMTIgnoreOS: macos // ---- -// Warning 6756: (1803-1808): User-defined operators are not yet supported by SMTChecker. This invocation of operator | has been ignored, which may lead to incorrect results. -// Warning 6756: (1803-1823): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (1863-1868): User-defined operators are not yet supported by SMTChecker. This invocation of operator & has been ignored, which may lead to incorrect results. -// Warning 6756: (1863-1884): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (1924-1929): User-defined operators are not yet supported by SMTChecker. This invocation of operator ^ has been ignored, which may lead to incorrect results. -// Warning 6756: (1924-1945): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6156: (1985-1987): User-defined operators are not yet supported by SMTChecker. This invocation of operator ~ has been ignored, which may lead to incorrect results. -// Warning 6756: (1985-2000): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2103-2108): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results. -// Warning 6756: (2103-2121): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2161-2166): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results. -// Warning 6756: (2161-2179): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6156: (2219-2221): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results. -// Warning 6756: (2219-2233): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2273-2278): User-defined operators are not yet supported by SMTChecker. This invocation of operator * has been ignored, which may lead to incorrect results. -// Warning 6756: (2273-2291): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2331-2336): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results. -// Warning 6756: (2331-2349): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2389-2394): User-defined operators are not yet supported by SMTChecker. This invocation of operator % has been ignored, which may lead to incorrect results. -// Warning 6756: (2389-2407): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2511-2517): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results. -// Warning 6756: (2571-2577): User-defined operators are not yet supported by SMTChecker. This invocation of operator != has been ignored, which may lead to incorrect results. -// Warning 6756: (2634-2639): User-defined operators are not yet supported by SMTChecker. This invocation of operator < has been ignored, which may lead to incorrect results. -// Warning 6756: (2693-2698): User-defined operators are not yet supported by SMTChecker. This invocation of operator > has been ignored, which may lead to incorrect results. -// Warning 6756: (2752-2758): User-defined operators are not yet supported by SMTChecker. This invocation of operator <= has been ignored, which may lead to incorrect results. -// Warning 6756: (2813-2819): User-defined operators are not yet supported by SMTChecker. This invocation of operator >= has been ignored, which may lead to incorrect results. -// Warning 3944: (679-708): CHC: Underflow (resulting value less than -32768) happens here. -// Warning 4984: (679-708): CHC: Overflow (resulting value larger than 32767) happens here. +// Warning 3944: (679-708): CHC: Underflow (resulting value less than -32768) might happen here. +// Warning 4984: (679-708): CHC: Overflow (resulting value larger than 32767) might happen here. // Warning 3944: (777-806): CHC: Underflow (resulting value less than -32768) happens here. -// Warning 4984: (777-806): CHC: Overflow (resulting value larger than 32767) happens here. -// Warning 3944: (953-982): CHC: Underflow (resulting value less than -32768) happens here. -// Warning 4984: (953-982): CHC: Overflow (resulting value larger than 32767) happens here. -// Warning 4281: (1051-1080): CHC: Division by zero happens here. +// Warning 4984: (777-806): CHC: Overflow (resulting value larger than 32767) might happen here. +// Warning 3944: (953-982): CHC: Underflow (resulting value less than -32768) might happen here. +// Warning 4984: (953-982): CHC: Overflow (resulting value larger than 32767) might happen here. +// Warning 4984: (1051-1080): CHC: Overflow (resulting value larger than 32767) might happen here. +// Warning 4281: (1051-1080): CHC: Division by zero might happen here. // Warning 4281: (1149-1178): CHC: Division by zero happens here. -// Warning 6328: (1796-1824): CHC: Assertion violation happens here. -// Warning 6328: (1856-1885): CHC: Assertion violation happens here. -// Warning 6328: (1917-1946): CHC: Assertion violation happens here. -// Warning 6328: (1978-2001): CHC: Assertion violation happens here. -// Warning 6328: (2096-2122): CHC: Assertion violation happens here. -// Warning 6328: (2154-2180): CHC: Assertion violation happens here. -// Warning 6328: (2212-2234): CHC: Assertion violation happens here. -// Warning 6328: (2266-2292): CHC: Assertion violation happens here. -// Warning 6328: (2324-2350): CHC: Assertion violation happens here. -// Warning 6328: (2382-2408): CHC: Assertion violation happens here. -// Warning 6328: (2503-2531): CHC: Assertion violation happens here. -// Warning 6328: (2563-2594): CHC: Assertion violation happens here. -// Warning 6328: (2626-2653): CHC: Assertion violation happens here. -// Warning 6328: (2685-2712): CHC: Assertion violation happens here. -// Warning 6328: (2744-2773): CHC: Assertion violation happens here. -// Warning 6328: (2805-2834): CHC: Assertion violation happens here. -// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 6328: (2105-2131): CHC: Assertion violation might happen here. +// Warning 6328: (2141-2163): CHC: Assertion violation might happen here. +// Warning 6328: (2209-2235): CHC: Assertion violation might happen here. +// Warning 6328: (2245-2271): CHC: Assertion violation might happen here. +// Info 1391: CHC: 12 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Warning 3046: (1051-1080): BMC: Division by zero happens here. +// Warning 7812: (2245-2271): BMC: Assertion violation might happen here. +// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_overflow.sol b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_overflow.sol index 21ed55c1c23a..8211325276fd 100644 --- a/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_overflow.sol +++ b/test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_overflow.sol @@ -2,14 +2,14 @@ type U8 is uint8; using {add as +} for U8 global; function add(U8 x, U8 y) pure returns (U8) { - return U8.wrap(U8.unwrap(x) + U8.unwrap(y)); // FIXME: should detect possible overflow here + return U8.wrap(U8.unwrap(x) + U8.unwrap(y)); // overflow detected } contract C { - U8 x = U8.wrap(254); + U8 x = U8.wrap(255); function inc() public { - x = x + U8.wrap(1); // FIXME: should detect possible overflow here + x = x + U8.wrap(1); } function check() view public { @@ -20,5 +20,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6756: (274-288): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results. +// Warning 4984: (115-142): CHC: Overflow (resulting value larger than 255) happens here. // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. From 13c2d62146ba7330cce6146c3029d06f6f5c0dee Mon Sep 17 00:00:00 2001 From: Pawel Gebal Date: Fri, 6 Oct 2023 12:16:02 +0200 Subject: [PATCH 2/4] apply CR changes --- libsolidity/ast/AST.h | 3 --- libsolidity/formal/BMC.cpp | 45 ++++++++++++++++++------------- libsolidity/formal/BMC.h | 5 ++-- libsolidity/formal/CHC.cpp | 28 ++++++++++++------- libsolidity/formal/CHC.h | 4 +-- libsolidity/formal/SMTEncoder.cpp | 24 +++++++---------- libsolidity/formal/SMTEncoder.h | 7 +++-- 7 files changed, 62 insertions(+), 54 deletions(-) diff --git a/libsolidity/ast/AST.h b/libsolidity/ast/AST.h index d651df33bebc..ca23b0d61975 100644 --- a/libsolidity/ast/AST.h +++ b/libsolidity/ast/AST.h @@ -2111,7 +2111,6 @@ class UnaryOperation: public Expression Token getOperator() const { return m_operator; } bool isPrefixOperation() const { return m_isPrefix; } Expression const& subExpression() const { return *m_subExpression; } - ASTPointer const& argument() const { return m_subExpression; } FunctionType const* userDefinedFunctionType() const; @@ -2146,8 +2145,6 @@ class BinaryOperation: public Expression Expression const& leftExpression() const { return *m_left; } Expression const& rightExpression() const { return *m_right; } - ASTPointer leftArgument() const { return m_left; } - ASTPointer rightArgument() const { return m_right; } Token getOperator() const { return m_operator; } FunctionType const* userDefinedFunctionType() const; diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index d8f30368812f..87c819987903 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -554,9 +554,11 @@ void BMC::endVisit(UnaryOperation const& _op) // User-defined operators are essentially function calls. if (auto funDef = *_op.annotation().userDefinedFunction) { - std::vector> arguments; - arguments.push_back(_op.argument()); - inlineFunctionCall(funDef, _op, &_op, _op.userDefinedFunctionType(), arguments); + std::vector arguments; + arguments.push_back(&_op.subExpression()); + // pushCallStack and defineExpr inside createReturnedExpression should be called on the expression + // in case of a user-defined operator call + inlineFunctionCall(funDef, _op, std::nullopt, arguments); return; } @@ -580,10 +582,13 @@ void BMC::endVisit(BinaryOperation const& _op) if (auto funDef = *_op.annotation().userDefinedFunction) { - std::vector> arguments; - arguments.push_back(_op.leftArgument()); - arguments.push_back(_op.rightArgument()); - inlineFunctionCall(funDef, _op, &_op, _op.userDefinedFunctionType(), arguments); + std::vector arguments; + arguments.push_back(&_op.leftExpression()); + arguments.push_back(&_op.rightExpression()); + + // pushCallStack and defineExpr inside createReturnedExpression should be called on the expression + // in case of a user-defined operator call + inlineFunctionCall(funDef, _op, std::nullopt, arguments); } } @@ -699,14 +704,11 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall) void BMC::inlineFunctionCall( FunctionDefinition const* _funDef, Expression const& _callStackExpr, - Expression const* _calledExpr, - FunctionType const* _funType, - std::vector> const& _arguments + std::optional _calledExpr, + std::vector const& _arguments ) { solAssert(_funDef, ""); - solAssert(_funType, ""); - solAssert(_calledExpr, ""); if (visitedFunction(_funDef)) { @@ -719,7 +721,7 @@ void BMC::inlineFunctionCall( } else { - initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef, _calledExpr, _funType, _arguments)); + initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef->parameters(), _calledExpr, _arguments)); // The reason why we need to pushCallStack here instead of visit(FunctionDefinition) // is that there we don't have `_callStackExpr`. @@ -739,11 +741,18 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall) solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), ""); auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); - Expression const* calledExpr = &_funCall.expression(); - auto funType = dynamic_cast(calledExpr->annotation().type); - std::vector> arguments = _funCall.sortedArguments(); - - inlineFunctionCall(funDef, _funCall, calledExpr, funType, arguments); + Expression const* expr = &_funCall.expression(); + auto funType = dynamic_cast(expr->annotation().type); + std::optional calledExpr = + funType->hasBoundFirstArgument() ? std::make_optional(expr) : std::nullopt; + + std::vector arguments; + for (auto& arg: _funCall.sortedArguments()) + arguments.push_back(&(*arg)); + + // pushCallStack and defineExpr inside createReturnedExpression should be called + // on the FunctionCall object for the normal function call case + inlineFunctionCall(funDef, _funCall, calledExpr, arguments); } void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall) diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 4aceadeea60f..9daa1683721c 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -117,9 +117,8 @@ class BMC: public SMTEncoder void inlineFunctionCall( FunctionDefinition const* _funDef, Expression const& _callStackExpr, - Expression const* _calledExpr, - FunctionType const* _funType, - std::vector> const& _arguments + std::optional _calledExpr, + std::vector const& _arguments ); /// Inlines if the function call is internal or external to `this`. /// Erases knowledge about state variables if external. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index bf19090f561e..930ca9b67544 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -549,8 +549,8 @@ void CHC::endVisit(UnaryOperation const& _op) if (auto funDef = *_op.annotation().userDefinedFunction) { - std::vector> arguments; - arguments.push_back(_op.argument()); + std::vector arguments; + arguments.push_back(&_op.subExpression()); internalFunctionCall(funDef, &_op, _op.userDefinedFunctionType(), arguments, state().thisAddress()); createReturnedExpressions(funDef, _op); @@ -563,9 +563,9 @@ void CHC::endVisit(BinaryOperation const& _op) if (auto funDef = *_op.annotation().userDefinedFunction) { - std::vector> arguments; - arguments.push_back(_op.leftArgument()); - arguments.push_back(_op.rightArgument()); + std::vector arguments; + arguments.push_back(&_op.leftExpression()); + arguments.push_back(&_op.rightExpression()); internalFunctionCall(funDef, &_op, _op.userDefinedFunctionType(), arguments, state().thisAddress()); createReturnedExpressions(funDef, _op); @@ -853,7 +853,7 @@ void CHC::internalFunctionCall( FunctionDefinition const* _funDef, Expression const* _calledExpr, FunctionType const* _funType, - std::vector> const& _arguments, + std::vector const& _arguments, smtutil::Expression _contractAddressValue ) { @@ -896,7 +896,6 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall) Expression const* calledExpr = &_funCall.expression(); auto funType = dynamic_cast(calledExpr->annotation().type); - std::vector> arguments = _funCall.sortedArguments(); auto contractAddressValue = [this](FunctionCall const& _f) { auto [callExpr, callOptions] = functionCallExpression(_f); @@ -909,6 +908,9 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall) solAssert(false, "Unreachable!"); }; + std::vector arguments; + for (auto& arg: _funCall.sortedArguments()) + arguments.push_back(&(*arg)); internalFunctionCall(funDef, calledExpr, funType, arguments, contractAddressValue(_funCall)); } @@ -1095,7 +1097,10 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall) state().readStateVars(*function->annotation().contract, contractAddressValue(_funCall)); } - smtutil::Expression pred = predicate(function, callExpr, &funType, _funCall.sortedArguments(), calledAddress); + std::vector arguments; + for (auto& arg: _funCall.sortedArguments()) + arguments.push_back(&(*arg)); + smtutil::Expression pred = predicate(function, callExpr, &funType, arguments, calledAddress); auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(*function); m_context.addAssertion(pred && txConstraints); @@ -1810,7 +1815,7 @@ smtutil::Expression CHC::predicate( FunctionDefinition const* _funDef, Expression const* _calledExpr, FunctionType const* _funType, - std::vector> _arguments, + std::vector _arguments, smtutil::Expression _contractAddressValue ) { @@ -1833,7 +1838,10 @@ smtutil::Expression CHC::predicate( contract = m_currentContract; args += currentStateVariables(*contract); - args += symbolicArguments(_funDef, _calledExpr, _funType, _arguments); + + std::optional calledExpr = + _funType->hasBoundFirstArgument() ? std::make_optional(_calledExpr) : std::nullopt; + args += symbolicArguments(_funDef->parameters(), calledExpr, _arguments); if (!usesStaticCall(_funDef, _funType)) { state().newState(); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 57bf8073846b..7f25d8a19e8d 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -133,7 +133,7 @@ class CHC: public SMTEncoder FunctionDefinition const* _funDef, Expression const* _calledExpr, FunctionType const* _funType, - std::vector> const& _arguments, + std::vector const& _arguments, smtutil::Expression _contractAddressValue ); void externalFunctionCall(FunctionCall const& _funCall); @@ -260,7 +260,7 @@ class CHC: public SMTEncoder FunctionDefinition const* _funDef, Expression const* _calledExpr, FunctionType const* _funType, - std::vector> _arguments, + std::vector _arguments, smtutil::Expression _contractAddressValue ); /// @returns a predicate that defines a contract initializer for _contract in the context of _contractContext. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index abb47fdd3b7c..34258397b864 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -3137,29 +3137,25 @@ void SMTEncoder::createReturnedExpressions(FunctionDefinition const* _funDef, Ex } std::vector SMTEncoder::symbolicArguments( - FunctionDefinition const* _funDef, - Expression const* _calledExpr, - FunctionType const* _funType, - std::vector> const& _arguments) + std::vector> const& _funParameters, + std::optional _calledExpr, + std::vector const& _arguments) { - solAssert(_funDef, ""); - solAssert(_funType, ""); - std::vector args; - auto functionParams = _funDef->parameters(); unsigned firstParam = 0; - if (_funType->hasBoundFirstArgument()) + if (_calledExpr) { - _calledExpr = innermostTuple(*_calledExpr); - auto const& attachedFunction = dynamic_cast(_calledExpr); + Expression const* calledExpr = innermostTuple(*_calledExpr.value()); + auto const& attachedFunction = dynamic_cast(calledExpr); solAssert(attachedFunction, ""); - args.push_back(expr(attachedFunction->expression(), functionParams.front()->type())); + args.push_back(expr(attachedFunction->expression(), _funParameters.front()->type())); firstParam = 1; } - solAssert((_arguments.size() + firstParam) == functionParams.size(), ""); + solAssert((_arguments.size() + firstParam) == _funParameters.size(), ""); + for (unsigned i = 0; i < _arguments.size(); ++i) - args.push_back(expr(*_arguments.at(i), functionParams.at(i + firstParam)->type())); + args.push_back(expr(*_arguments.at(i), _funParameters.at(i + firstParam)->type())); return args; } diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index e88a2400e6a9..4e2b8112ba48 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -409,10 +409,9 @@ class SMTEncoder: public ASTConstVisitor /// taking into account attached functions and /// type conversion. std::vector symbolicArguments( - FunctionDefinition const* _funDef, - Expression const* _calledExpr, - FunctionType const* _funType, - std::vector> const& _arguments + std::vector> const& _funParameters, + std::optional _calledExpr, + std::vector const& _arguments ); smtutil::Expression constantExpr(Expression const& _expr, VariableDeclaration const& _var); From 353dbdde8a31c7a1d1dc35ff1bbf310707251fa2 Mon Sep 17 00:00:00 2001 From: Pawel Gebal Date: Thu, 19 Oct 2023 16:26:30 +0200 Subject: [PATCH 3/4] refactor: rename calledExpr to boundArgumentCall --- libsolidity/formal/BMC.cpp | 8 ++++---- libsolidity/formal/CHC.cpp | 22 ++++++++++------------ libsolidity/formal/CHC.h | 4 ++-- libsolidity/formal/SMTEncoder.cpp | 9 +++++---- libsolidity/formal/SMTEncoder.h | 4 ++-- 5 files changed, 23 insertions(+), 24 deletions(-) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 87c819987903..b16182af8c88 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -704,7 +704,7 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall) void BMC::inlineFunctionCall( FunctionDefinition const* _funDef, Expression const& _callStackExpr, - std::optional _calledExpr, + std::optional _boundArgumentCall, std::vector const& _arguments ) { @@ -721,7 +721,7 @@ void BMC::inlineFunctionCall( } else { - initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef->parameters(), _calledExpr, _arguments)); + initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef->parameters(), _arguments, _boundArgumentCall)); // The reason why we need to pushCallStack here instead of visit(FunctionDefinition) // is that there we don't have `_callStackExpr`. @@ -743,7 +743,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall) auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); Expression const* expr = &_funCall.expression(); auto funType = dynamic_cast(expr->annotation().type); - std::optional calledExpr = + std::optional boundArgumentCall = funType->hasBoundFirstArgument() ? std::make_optional(expr) : std::nullopt; std::vector arguments; @@ -752,7 +752,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall) // pushCallStack and defineExpr inside createReturnedExpression should be called // on the FunctionCall object for the normal function call case - inlineFunctionCall(funDef, _funCall, calledExpr, arguments); + inlineFunctionCall(funDef, _funCall, boundArgumentCall, arguments); } void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall) diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 930ca9b67544..09a9af8ffe30 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -551,7 +551,7 @@ void CHC::endVisit(UnaryOperation const& _op) { std::vector arguments; arguments.push_back(&_op.subExpression()); - internalFunctionCall(funDef, &_op, _op.userDefinedFunctionType(), arguments, state().thisAddress()); + internalFunctionCall(funDef, std::nullopt, _op.userDefinedFunctionType(), arguments, state().thisAddress()); createReturnedExpressions(funDef, _op); } @@ -566,7 +566,7 @@ void CHC::endVisit(BinaryOperation const& _op) std::vector arguments; arguments.push_back(&_op.leftExpression()); arguments.push_back(&_op.rightExpression()); - internalFunctionCall(funDef, &_op, _op.userDefinedFunctionType(), arguments, state().thisAddress()); + internalFunctionCall(funDef, std::nullopt, _op.userDefinedFunctionType(), arguments, state().thisAddress()); createReturnedExpressions(funDef, _op); } @@ -851,14 +851,13 @@ void CHC::visitDeployment(FunctionCall const& _funCall) void CHC::internalFunctionCall( FunctionDefinition const* _funDef, - Expression const* _calledExpr, + std::optional _boundArgumentCall, FunctionType const* _funType, std::vector const& _arguments, smtutil::Expression _contractAddressValue ) { solAssert(m_currentContract, ""); - solAssert(_calledExpr, ""); solAssert(_funType, ""); if (_funDef) @@ -869,7 +868,7 @@ void CHC::internalFunctionCall( m_callGraph[m_currentContract].insert(_funDef); } - m_context.addAssertion(predicate(_funDef, _calledExpr, _funType, _arguments, _contractAddressValue)); + m_context.addAssertion(predicate(_funDef, _boundArgumentCall, _funType, _arguments, _contractAddressValue)); solAssert(m_errorDest, ""); connectBlocks( @@ -911,7 +910,10 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall) std::vector arguments; for (auto& arg: _funCall.sortedArguments()) arguments.push_back(&(*arg)); - internalFunctionCall(funDef, calledExpr, funType, arguments, contractAddressValue(_funCall)); + + std::optional boundArgumentCall = + funType->hasBoundFirstArgument() ? std::make_optional(calledExpr) : std::nullopt; + internalFunctionCall(funDef, boundArgumentCall, funType, arguments, contractAddressValue(_funCall)); } void CHC::addNondetCalls(ContractDefinition const& _contract) @@ -1813,13 +1815,12 @@ smtutil::Expression CHC::predicate(Predicate const& _block) smtutil::Expression CHC::predicate( FunctionDefinition const* _funDef, - Expression const* _calledExpr, + std::optional _boundArgumentCall, FunctionType const* _funType, std::vector _arguments, smtutil::Expression _contractAddressValue ) { - solAssert(_calledExpr, ""); solAssert(_funType, ""); auto kind = _funType->kind(); solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); @@ -1838,10 +1839,7 @@ smtutil::Expression CHC::predicate( contract = m_currentContract; args += currentStateVariables(*contract); - - std::optional calledExpr = - _funType->hasBoundFirstArgument() ? std::make_optional(_calledExpr) : std::nullopt; - args += symbolicArguments(_funDef->parameters(), calledExpr, _arguments); + args += symbolicArguments(_funDef->parameters(), _arguments, _boundArgumentCall); if (!usesStaticCall(_funDef, _funType)) { state().newState(); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 7f25d8a19e8d..fe7387bd3568 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -131,7 +131,7 @@ class CHC: public SMTEncoder void internalFunctionCall(FunctionCall const& _funCall); void internalFunctionCall( FunctionDefinition const* _funDef, - Expression const* _calledExpr, + std::optional _boundArgumentCall, FunctionType const* _funType, std::vector const& _arguments, smtutil::Expression _contractAddressValue @@ -258,7 +258,7 @@ class CHC: public SMTEncoder /// @returns the summary predicate for the called function. smtutil::Expression predicate( FunctionDefinition const* _funDef, - Expression const* _calledExpr, + std::optional _boundArgumentCall, FunctionType const* _funType, std::vector _arguments, smtutil::Expression _contractAddressValue diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 34258397b864..ae3a06869d19 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -3138,14 +3138,15 @@ void SMTEncoder::createReturnedExpressions(FunctionDefinition const* _funDef, Ex std::vector SMTEncoder::symbolicArguments( std::vector> const& _funParameters, - std::optional _calledExpr, - std::vector const& _arguments) + std::vector const& _arguments, + std::optional _boundArgumentCall +) { std::vector args; unsigned firstParam = 0; - if (_calledExpr) + if (_boundArgumentCall) { - Expression const* calledExpr = innermostTuple(*_calledExpr.value()); + Expression const* calledExpr = innermostTuple(*_boundArgumentCall.value()); auto const& attachedFunction = dynamic_cast(calledExpr); solAssert(attachedFunction, ""); args.push_back(expr(attachedFunction->expression(), _funParameters.front()->type())); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 4e2b8112ba48..69010fb1cf54 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -410,8 +410,8 @@ class SMTEncoder: public ASTConstVisitor /// type conversion. std::vector symbolicArguments( std::vector> const& _funParameters, - std::optional _calledExpr, - std::vector const& _arguments + std::vector const& _arguments, + std::optional _calledExpr ); smtutil::Expression constantExpr(Expression const& _expr, VariableDeclaration const& _var); From da7c00e1e5f64293d5283cd5fe1a39391ad17966 Mon Sep 17 00:00:00 2001 From: Pawel Gebal Date: Fri, 20 Oct 2023 16:39:51 +0200 Subject: [PATCH 4/4] fix test error --- libsolidity/formal/CHC.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 09a9af8ffe30..3cd1524599df 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -1102,7 +1102,7 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall) std::vector arguments; for (auto& arg: _funCall.sortedArguments()) arguments.push_back(&(*arg)); - smtutil::Expression pred = predicate(function, callExpr, &funType, arguments, calledAddress); + smtutil::Expression pred = predicate(function, std::nullopt, &funType, arguments, calledAddress); auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(*function); m_context.addAssertion(pred && txConstraints);