diff --git a/Changelog.md b/Changelog.md index 9ecd036e1..201d792ed 100644 --- a/Changelog.md +++ b/Changelog.md @@ -7,6 +7,7 @@ Compiler Features: Bugfixes: + * SMTChecker: Fix internal error when using ``abi.decode``. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 98d6519fb..5fd364f8b 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -208,17 +208,14 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl) solAssert(symbTuple, ""); auto const& components = symbTuple->components(); auto const& declarations = _varDecl.declarations(); - if (!components.empty()) - { - solAssert(components.size() == declarations.size(), ""); - for (unsigned i = 0; i < declarations.size(); ++i) - if ( - components.at(i) && - declarations.at(i) && - m_context.knownVariable(*declarations.at(i)) - ) - assignment(*declarations.at(i), components.at(i)->currentValue(declarations.at(i)->type())); - } + solAssert(components.size() == declarations.size(), ""); + for (unsigned i = 0; i < declarations.size(); ++i) + if ( + components.at(i) && + declarations.at(i) && + m_context.knownVariable(*declarations.at(i)) + ) + assignment(*declarations.at(i), components.at(i)->currentValue(declarations.at(i)->type())); } } else if (m_context.knownVariable(*_varDecl.declarations().front())) @@ -320,24 +317,23 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple) { auto const& symbTuple = dynamic_pointer_cast(m_context.expression(_tuple)); solAssert(symbTuple, ""); - if (symbTuple->components().empty()) + auto const& symbComponents = symbTuple->components(); + auto const& tupleComponents = _tuple.components(); + solAssert(symbComponents.size() == _tuple.components().size(), ""); + for (unsigned i = 0; i < symbComponents.size(); ++i) { - vector> components; - for (auto const& component: _tuple.components()) - if (component) - { - if (auto varDecl = identifierToVariable(*component)) - components.push_back(m_context.variable(*varDecl)); - else - { - solAssert(m_context.knownExpression(*component), ""); - components.push_back(m_context.expression(*component)); - } - } + auto sComponent = symbComponents.at(i); + auto tComponent = tupleComponents.at(i); + if (sComponent && tComponent) + { + if (auto varDecl = identifierToVariable(*tComponent)) + m_context.addAssertion(sComponent->currentValue() == currentValue(*varDecl)); else - components.push_back(nullptr); - solAssert(components.size() == _tuple.components().size(), ""); - symbTuple->setComponents(move(components)); + { + solAssert(m_context.knownExpression(*tComponent), ""); + m_context.addAssertion(sComponent->currentValue() == expr(*tComponent)); + } + } } } else @@ -609,12 +605,22 @@ void SMTEncoder::endVisit(Identifier const& _identifier) defineExpr(_identifier, m_context.thisAddress()); m_uninterpretedTerms.insert(&_identifier); } - else if (smt::isSupportedType(_identifier.annotation().type->category())) - // TODO: handle MagicVariableDeclaration here - m_errorReporter.warning( - _identifier.location(), - "Assertion checker does not yet support the type of this variable." - ); + else if ( + _identifier.annotation().type->category() != Type::Category::Modifier + ) + createExpr(_identifier); +} + +void SMTEncoder::endVisit(ElementaryTypeNameExpression const& _typeName) +{ + auto const& typeType = dynamic_cast(*_typeName.annotation().type); + auto result = smt::newSymbolicVariable( + *TypeProvider::uint256(), + typeType.actualType()->toString(false), + m_context + ); + solAssert(!result.first && result.second, ""); + m_context.createExpression(_typeName, result.second); } void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall) @@ -1503,15 +1509,18 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) { auto const& symbTuple = dynamic_pointer_cast(m_context.expression(_funCall)); solAssert(symbTuple, ""); - if (symbTuple->components().empty()) + auto const& symbComponents = symbTuple->components(); + solAssert(symbComponents.size() == returnParams.size(), ""); + for (unsigned i = 0; i < symbComponents.size(); ++i) { - vector> components; - for (auto param: returnParams) + auto sComponent = symbComponents.at(i); + auto param = returnParams.at(i); + solAssert(param, ""); + if (sComponent) { solAssert(m_context.knownVariable(*param), ""); - components.push_back(m_context.variable(*param)); + m_context.addAssertion(sComponent->currentValue() == currentValue(*param)); } - symbTuple->setComponents(move(components)); } } else if (returnParams.size() == 1) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 37a7cea24..4f8c5ac8c 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -27,6 +27,7 @@ #include #include +#include #include #include #include @@ -82,6 +83,7 @@ protected: void endVisit(BinaryOperation const& _node) override; void endVisit(FunctionCall const& _node) override; void endVisit(Identifier const& _node) override; + void endVisit(ElementaryTypeNameExpression const& _node) override; void endVisit(Literal const& _node) override; void endVisit(Return const& _node) override; bool visit(MemberAccess const& _node) override; diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 3a814ec7d..d0163d381 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -248,12 +248,16 @@ SymbolicTupleVariable::SymbolicTupleVariable( SymbolicVariable(_type, _type, move(_uniqueName), _context) { solAssert(isTuple(m_type->category()), ""); -} - -void SymbolicTupleVariable::setComponents(vector> _components) -{ - solAssert(m_components.empty(), ""); - auto const& tupleType = dynamic_cast(m_type); - solAssert(_components.size() == tupleType->components().size(), ""); - m_components = move(_components); + auto const& tupleType = dynamic_cast(*m_type); + auto const& componentsTypes = tupleType.components(); + for (unsigned i = 0; i < componentsTypes.size(); ++i) + if (componentsTypes.at(i)) + { + string componentName = m_uniqueName + "_component_" + to_string(i); + auto result = smt::newSymbolicVariable(*componentsTypes.at(i), componentName, m_context); + solAssert(result.second, ""); + m_components.emplace_back(move(result.second)); + } + else + m_components.emplace_back(nullptr); } diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 9ae637490..4d9fcc2f7 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -250,8 +250,6 @@ public: return m_components; } - void setComponents(std::vector> _components); - private: std::vector> m_components; }; diff --git a/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol b/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol index e4d8f4cfe..955d5fd1e 100644 --- a/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol +++ b/test/libsolidity/smtCheckerTests/complex/MerkleProof.sol @@ -35,6 +35,8 @@ library MerkleProof { // ---- // Warning: (755-767): Assertion checker does not yet support this expression. +// Warning: (988-991): Assertion checker does not yet implement type abi // Warning: (988-1032): Assertion checker does not yet implement this type of function call. +// Warning: (1175-1178): Assertion checker does not yet implement type abi // Warning: (1175-1219): Assertion checker does not yet implement this type of function call. // Warning: (755-767): Assertion checker does not yet support this expression. diff --git a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol index 6db44a5ef..43bd10cf7 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol @@ -83,7 +83,7 @@ contract InternalCall { // Warning: (1144-1206): Function state mutability can be restricted to pure // Warning: (1212-1274): Function state mutability can be restricted to pure // Warning: (1280-1342): Function state mutability can be restricted to pure +// Warning: (771-774): Assertion checker does not yet implement type abi // Warning: (782-813): Type conversion is not yet fully supported and might yield false positives. // Warning: (771-814): Assertion checker does not yet implement this type of function call. -// Warning: (825-830): Assertion checker does not yet support the type of this variable. // Warning: (1403-1408): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol b/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol index f6c6f89c2..33cf71e81 100644 --- a/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol +++ b/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol @@ -9,5 +9,6 @@ contract C { // ---- // Warning: (133-143): Unused local variable. // Warning: (133-143): Assertion checker does not yet support the type of this variable. +// Warning: (146-147): Assertion checker does not yet implement type type(struct C.A storage pointer) // Warning: (146-163): Assertion checker does not yet implement type struct C.A memory // Warning: (146-163): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol b/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol index 8c3ef4aff..bed409b90 100644 --- a/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol +++ b/test/libsolidity/smtCheckerTests/functions/abi_encode_functions.sol @@ -6,5 +6,7 @@ contract C { } // ---- // Warning: (31-64): Experimental features are turned on. Do not use experimental features on live deployments. +// Warning: (162-165): Assertion checker does not yet implement type abi // Warning: (162-176): Assertion checker does not yet implement this type of function call. +// Warning: (178-181): Assertion checker does not yet implement type abi // Warning: (178-203): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol index 2ceb9e607..85387017b 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_library_1.sol @@ -16,3 +16,5 @@ contract C assert(y < 10000); } } +// ---- +// Warning: (228-229): Assertion checker does not yet implement type type(library L) diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol index 324197004..5eda70213 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_library_1_fail.sol @@ -17,4 +17,5 @@ contract C } } // ---- +// Warning: (228-229): Assertion checker does not yet implement type type(library L) // Warning: (245-261): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol new file mode 100644 index 000000000..e469f06ba --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +pragma experimental "ABIEncoderV2"; + +contract C { + struct S { uint x; uint[] b; } + function f() public pure returns (S memory, bytes memory) { + return abi.decode("abc", (S, bytes)); + } +} +// ---- +// Warning: (32-67): Experimental features are turned on. Do not use experimental features on live deployments. +// Warning: (151-159): Assertion checker does not yet support the type of this variable. +// Warning: (188-191): Assertion checker does not yet implement type abi +// Warning: (207-208): Assertion checker does not yet implement type type(struct C.S storage pointer) +// Warning: (188-217): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol new file mode 100644 index 000000000..cf86e8e78 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_memory_v2_value_types.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; +pragma experimental "ABIEncoderV2"; + +contract C { + function f() public pure { + (uint x1, bool b1) = abi.decode("abc", (uint, bool)); + (uint x2, bool b2) = abi.decode("abc", (uint, bool)); + // False positive until abi.* are implemented as uninterpreted functions. + assert(x1 == x2); + } +} +// ---- +// Warning: (32-67): Experimental features are turned on. Do not use experimental features on live deployments. +// Warning: (125-132): Unused local variable. +// Warning: (183-190): Unused local variable. +// Warning: (136-139): Assertion checker does not yet implement type abi +// Warning: (136-167): Assertion checker does not yet implement this type of function call. +// Warning: (194-197): Assertion checker does not yet implement type abi +// Warning: (194-225): Assertion checker does not yet implement this type of function call. +// Warning: (303-319): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol new file mode 100644 index 000000000..c06577e0f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; +contract C { + function f() public pure { + (uint a1, bytes32 b1, C c1) = abi.decode("abc", (uint, bytes32, C)); + (uint a2, bytes32 b2, C c2) = abi.decode("abc", (uint, bytes32, C)); + // False positive until abi.* are implemented as uninterpreted functions. + assert(a1 == a2); + assert(a1 != a2); + } + +} +// ---- +// Warning: (88-98): Unused local variable. +// Warning: (100-104): Unused local variable. +// Warning: (161-171): Unused local variable. +// Warning: (173-177): Unused local variable. +// Warning: (108-111): Assertion checker does not yet implement type abi +// Warning: (142-143): Assertion checker does not yet implement type type(contract C) +// Warning: (108-145): Assertion checker does not yet implement this type of function call. +// Warning: (181-184): Assertion checker does not yet implement type abi +// Warning: (215-216): Assertion checker does not yet implement type type(contract C) +// Warning: (181-218): Assertion checker does not yet implement this type of function call. +// Warning: (296-312): Assertion violation happens here +// Warning: (315-331): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol b/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol index 44c252868..33a7d972b 100644 --- a/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol +++ b/test/libsolidity/smtCheckerTests/typecast/enum_from_uint.sol @@ -10,5 +10,6 @@ contract C } } // ---- +// Warning: (132-133): Assertion checker does not yet implement type type(enum C.D) // Warning: (132-136): Type conversion is not yet fully supported and might yield false positives. // Warning: (140-160): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_call.sol b/test/libsolidity/smtCheckerTests/types/address_call.sol index d6d165591..da87778e6 100644 --- a/test/libsolidity/smtCheckerTests/types/address_call.sol +++ b/test/libsolidity/smtCheckerTests/types/address_call.sol @@ -20,3 +20,6 @@ contract C // ---- // Warning: (224-240): Unused local variable. // Warning: (260-275): Assertion violation happens here +// Warning: (279-293): Assertion violation happens here +// Warning: (297-316): Assertion violation happens here +// Warning: (320-344): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol b/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol index 06925a66b..b9d3bcaea 100644 --- a/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol +++ b/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol @@ -20,3 +20,6 @@ contract C // ---- // Warning: (224-240): Unused local variable. // Warning: (268-283): Assertion violation happens here +// Warning: (287-301): Assertion violation happens here +// Warning: (305-324): Assertion violation happens here +// Warning: (328-352): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol index 529ce7ac0..32e4cbb9a 100644 --- a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol +++ b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol @@ -20,3 +20,6 @@ contract C // ---- // Warning: (224-240): Unused local variable. // Warning: (266-281): Assertion violation happens here +// Warning: (285-299): Assertion violation happens here +// Warning: (303-322): Assertion violation happens here +// Warning: (326-350): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct_1.sol b/test/libsolidity/smtCheckerTests/types/struct_1.sol index 38aa311a6..89c10c73c 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_1.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_1.sol @@ -17,8 +17,10 @@ contract C // Warning: (157-170): Unused local variable. // Warning: (157-170): Assertion checker does not yet support the type of this variable. // Warning: (139-146): Assertion checker does not yet implement type struct C.S storage ref +// Warning: (149-150): Assertion checker does not yet implement type type(struct C.S storage pointer) // Warning: (149-153): Assertion checker does not yet implement type struct C.S memory // Warning: (149-153): Assertion checker does not yet implement this expression. // Warning: (139-153): Assertion checker does not yet implement type struct C.S storage ref +// Warning: (173-174): Assertion checker does not yet implement type type(struct C.S storage pointer) // Warning: (173-177): Assertion checker does not yet implement type struct C.S memory // Warning: (173-177): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol b/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol index 99db33948..1a266aaa7 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_return_branch.sol @@ -15,9 +15,11 @@ contract C { } // ---- // Warning: (112-120): Assertion checker does not yet support the type of this variable. +// Warning: (137-138): Assertion checker does not yet implement type type(struct C.S storage pointer) // Warning: (137-141): Assertion checker does not yet implement type struct C.S memory // Warning: (137-141): Assertion checker does not yet implement this expression. // Warning: (193-203): Assertion checker does not yet support the type of this variable. +// Warning: (137-138): Assertion checker does not yet implement type type(struct C.S storage pointer) // Warning: (137-141): Assertion checker does not yet implement type struct C.S memory // Warning: (137-141): Assertion checker does not yet implement this expression. // Warning: (227-228): Assertion checker does not yet implement type struct C.S memory