diff --git a/Changelog.md b/Changelog.md index 00719ac7a..d182257f1 100644 --- a/Changelog.md +++ b/Changelog.md @@ -8,6 +8,7 @@ Compiler Features: * SMTChecker: Support inherited state variables. * SMTChecker: Support tuples and function calls with multiple return values. * SMTChecker: Support ``delete``. + * SMTChecker: Inline external function calls to ``this``. * Assembler: Encode the compiler version in the deployed bytecode. diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index d70aa188a..7009efebb 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -666,8 +666,6 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) visitGasLeft(_funCall); break; case FunctionType::Kind::Internal: - inlineFunctionCall(_funCall); - break; case FunctionType::Kind::External: case FunctionType::Kind::DelegateCall: case FunctionType::Kind::BareCall: @@ -675,9 +673,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) case FunctionType::Kind::BareDelegateCall: case FunctionType::Kind::BareStaticCall: case FunctionType::Kind::Creation: - m_externalFunctionCallHappened = true; - resetStateVariables(); - resetStorageReferences(); + internalOrExternalFunctionCall(_funCall); break; case FunctionType::Kind::KECCAK256: case FunctionType::Kind::ECRecover: @@ -805,6 +801,25 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) } } +void SMTChecker::internalOrExternalFunctionCall(FunctionCall const& _funCall) +{ + auto funDef = inlinedFunctionCallToDefinition(_funCall); + auto const& funType = dynamic_cast(*_funCall.expression().annotation().type); + if (funDef) + inlineFunctionCall(_funCall); + else if (funType.kind() == FunctionType::Kind::Internal) + m_errorReporter.warning( + _funCall.location(), + "Assertion checker does not yet implement this type of function call." + ); + else + { + m_externalFunctionCallHappened = true; + resetStateVariables(); + resetStorageReferences(); + } +} + void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall) { vector smtArguments; @@ -1931,7 +1946,21 @@ FunctionDefinition const* SMTChecker::inlinedFunctionCallToDefinition(FunctionCa return nullptr; FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); - if (funType.kind() != FunctionType::Kind::Internal) + if (funType.kind() == FunctionType::Kind::External) + { + auto memberAccess = dynamic_cast(&_funCall.expression()); + auto identifier = memberAccess ? + dynamic_cast(&memberAccess->expression()) : + nullptr; + if (!( + identifier && + identifier->name() == "this" && + identifier->annotation().referencedDeclaration && + dynamic_cast(identifier->annotation().referencedDeclaration) + )) + return nullptr; + } + else if (funType.kind() != FunctionType::Kind::Internal) return nullptr; FunctionDefinition const* funDef = nullptr; diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index d83fc9232..8c0f03ab3 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -115,6 +115,9 @@ private: void inlineFunctionCall(FunctionCall const& _funCall); /// Creates an uninterpreted function call. void abstractFunctionCall(FunctionCall const& _funCall); + /// Inlines if the function call is internal or external to `this`. + /// Erases knowledge about state variables if external. + void internalOrExternalFunctionCall(FunctionCall const& _funCall); void visitFunctionIdentifier(Identifier const& _identifier); /// Encodes a modifier or function body according to the modifier diff --git a/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol b/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol index 0ceb3b46c..ee4504287 100644 --- a/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol +++ b/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol @@ -9,4 +9,5 @@ contract C { } } // ---- +// Warning: (99-107): Assertion checker does not support recursive function calls. // Warning: (141-144): Assertion checker does not support recursive function calls. diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call.sol new file mode 100644 index 000000000..d7762fbea --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/this_external_call.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + function f(uint y) public { + x = y; + } + function g(uint y) public { + require(y < 1000); + this.f(y); + assert(x < 1000); + } +} diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol new file mode 100644 index 000000000..4226bd68a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + function f(uint y) public returns (uint) { + x = y; + return x; + } + function g(uint y) public { + require(y < 1000); + uint z = this.f(y); + assert(z < 1000); + } +} diff --git a/test/libsolidity/smtCheckerTests/functions/this_fake.sol b/test/libsolidity/smtCheckerTests/functions/this_fake.sol new file mode 100644 index 000000000..3a7511a54 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/this_fake.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; + +contract C +{ + uint public x; + C c; + function f(C _c) public { + c = _c; + } + function g() public { + C this = c; + x = 0; + this.h(); + // State knowledge is erased. + // Function call is not inlined. + assert(x == 0); + } + function h() public { + x = 2; + } +} +// ---- +// Warning: (160-166): This declaration shadows a builtin symbol. +// Warning: (268-282): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/this_state.sol b/test/libsolidity/smtCheckerTests/functions/this_state.sol new file mode 100644 index 000000000..6af349473 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/this_state.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C +{ + uint public x; + function g() public { + x = 0; + this.h(); + // Function call is inlined. + assert(x == 2); + } + function h() public { + x = 2; + } +}