From 6c7527ac9001ebff7839ab2533e08fa66296a4f9 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 26 Apr 2019 14:57:29 +0200 Subject: [PATCH] [SMTChecker] Support tuple type declaration --- Changelog.md | 1 + libsolidity/formal/SMTChecker.cpp | 38 +++++++++++++++---- libsolidity/formal/SymbolicTypes.cpp | 10 ++++- libsolidity/formal/SymbolicTypes.h | 1 + libsolidity/formal/SymbolicVariables.cpp | 18 +++++++++ libsolidity/formal/SymbolicVariables.h | 23 +++++++++++ .../functions/functions_identity_as_tuple.sol | 1 - .../functions_identity_as_tuple_fail.sol | 1 - .../types/address_transfer.sol | 1 - .../types/address_transfer_2.sol | 2 - .../types/address_transfer_insufficient.sol | 2 - .../smtCheckerTests/types/array_literal_1.sol | 2 +- .../types/tuple_assignment_compound.sol | 13 +++++++ 13 files changed, 97 insertions(+), 16 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/types/tuple_assignment_compound.sol diff --git a/Changelog.md b/Changelog.md index 1b400ffc7..51bb3548b 100644 --- a/Changelog.md +++ b/Changelog.md @@ -5,6 +5,7 @@ Language Features: Compiler Features: * SMTChecker: Support inherited state variables. + * SMTChecker: Support tuple declarations. Bugfixes: diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 46c392958..6a6e108f6 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -383,17 +383,41 @@ void SMTChecker::endVisit(Assignment const& _assignment) void SMTChecker::endVisit(TupleExpression const& _tuple) { - if ( - _tuple.isInlineArray() || - _tuple.components().size() != 1 || - !isSupportedType(_tuple.components()[0]->annotation().type->category()) - ) + if (_tuple.isInlineArray()) m_errorReporter.warning( _tuple.location(), - "Assertion checker does not yet implement tuples and inline arrays." + "Assertion checker does not yet implement inline arrays." ); + else if (_tuple.annotation().type->category() == Type::Category::Tuple) + { + createExpr(_tuple); + vector> components; + for (auto const& component: _tuple.components()) + if (component) + { + if (auto varDecl = identifierToVariable(*component)) + components.push_back(m_variables[varDecl]); + else + { + solAssert(knownExpr(*component), ""); + components.push_back(m_expressions[component.get()]); + } + } + else + components.push_back(nullptr); + solAssert(components.size() == _tuple.components().size(), ""); + auto const& symbTuple = dynamic_pointer_cast(m_expressions[&_tuple]); + solAssert(symbTuple, ""); + symbTuple->setComponents(move(components)); + } else - defineExpr(_tuple, expr(*_tuple.components()[0])); + { + /// Parenthesized expressions are also TupleExpression regardless their type. + auto const& components = _tuple.components(); + solAssert(components.size() == 1, ""); + if (isSupportedType(components.front()->annotation().type->category())) + defineExpr(_tuple, expr(*components.front())); + } } void SMTChecker::addOverflowTarget( diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 268d4aedc..175637735 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -99,7 +99,8 @@ bool dev::solidity::isSupportedType(Type::Category _category) return isNumber(_category) || isBool(_category) || isMapping(_category) || - isArray(_category); + isArray(_category) || + isTuple(_category); } bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category) @@ -151,6 +152,8 @@ pair> dev::solidity::newSymbolicVariable( var = make_shared(type, _uniqueName, _solver); else if (isArray(_type.category())) var = make_shared(type, _uniqueName, _solver); + else if (isTuple(_type.category())) + var = make_shared(type, _uniqueName, _solver); else solAssert(false, ""); return make_pair(abstract, var); @@ -226,6 +229,11 @@ bool dev::solidity::isArray(Type::Category _category) return _category == Type::Category::Array; } +bool dev::solidity::isTuple(Type::Category _category) +{ + return _category == Type::Category::Tuple; +} + smt::Expression dev::solidity::minValue(IntegerType const& _type) { return smt::Expression(_type.minValue()); diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index f487ae430..e9132a819 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -51,6 +51,7 @@ bool isBool(Type::Category _category); bool isFunction(Type::Category _category); bool isMapping(Type::Category _category); bool isArray(Type::Category _category); +bool isTuple(Type::Category _category); /// Returns a new symbolic variable, according to _type. /// Also returns whether the type is abstract or not, diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index cccaa61a0..cad64fc48 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -173,3 +173,21 @@ SymbolicEnumVariable::SymbolicEnumVariable( { solAssert(isEnum(m_type->category()), ""); } + +SymbolicTupleVariable::SymbolicTupleVariable( + TypePointer _type, + string _uniqueName, + smt::SolverInterface& _interface +): + SymbolicVariable(move(_type), move(_uniqueName), _interface) +{ + 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); +} diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 0c65a34a6..3da4bbbb1 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -187,5 +187,28 @@ public: ); }; +/** + * Specialization of SymbolicVariable for Tuple + */ +class SymbolicTupleVariable: public SymbolicVariable +{ +public: + SymbolicTupleVariable( + TypePointer _type, + std::string _uniqueName, + smt::SolverInterface& _interface + ); + + std::vector> const& components() + { + return m_components; + } + + void setComponents(std::vector> _components); + +private: + std::vector> m_components; +}; + } } diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol index 2ecff63e1..3793f4116 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol @@ -12,4 +12,3 @@ contract C } // ---- -// Warning: (153-156): Assertion checker does not yet implement tuples and inline arrays. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol index a9bde9e48..e3c805947 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol @@ -12,5 +12,4 @@ contract C } // ---- -// Warning: (153-156): Assertion checker does not yet implement tuples and inline arrays. // Warning: (163-176): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer.sol b/test/libsolidity/smtCheckerTests/types/address_transfer.sol index 08a5244c3..80abfbc38 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer.sol @@ -12,5 +12,4 @@ contract C } // ---- // Warning: (131-146): Insufficient funds happens here -// Warning: (131-146): Assertion checker does not yet implement this type. // Warning: (195-219): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol index d2f9e6939..a83ed00ad 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol @@ -15,7 +15,5 @@ contract C } // ---- // Warning: (217-232): Insufficient funds happens here -// Warning: (217-232): Assertion checker does not yet implement this type. // Warning: (236-251): Insufficient funds happens here -// Warning: (236-251): Assertion checker does not yet implement this type. // Warning: (295-324): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol index d3bfbe302..d0df06e22 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol @@ -12,7 +12,5 @@ contract C } // ---- // Warning: (134-149): Insufficient funds happens here -// Warning: (134-149): Assertion checker does not yet implement this type. // Warning: (153-169): Insufficient funds happens here -// Warning: (153-169): Assertion checker does not yet implement this type. // Warning: (213-237): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_1.sol b/test/libsolidity/smtCheckerTests/types/array_literal_1.sol index 5c0d31b5b..0380f673c 100644 --- a/test/libsolidity/smtCheckerTests/types/array_literal_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_literal_1.sol @@ -8,5 +8,5 @@ contract C } // ---- // Warning: (76-96): Unused local variable. -// Warning: (99-114): Assertion checker does not yet implement tuples and inline arrays. +// Warning: (99-114): Assertion checker does not yet implement inline arrays. // Warning: (99-114): Internal error: Expression undefined for SMT solver. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_assignment_compound.sol b/test/libsolidity/smtCheckerTests/types/tuple_assignment_compound.sol new file mode 100644 index 000000000..68b4f9d68 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/tuple_assignment_compound.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + uint a = 1; + uint b = 3; + a += ((((b)))); + assert(a == 3); + } +} +// ---- +// Warning: (122-136): Assertion violation happens here