From e3652627fdd27e1949785c871614915d75974ac3 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Sun, 10 Nov 2019 18:58:29 +0100 Subject: [PATCH] [SMTChecker] Fix ICE in CHC when function used as argument --- Changelog.md | 1 + libsolidity/formal/CHC.cpp | 22 +++++++++--- libsolidity/formal/CHC.h | 6 ++-- libsolidity/formal/SMTEncoder.cpp | 6 ++-- libsolidity/formal/SymbolicTypes.cpp | 24 ++++++++++++- libsolidity/formal/SymbolicVariables.cpp | 34 ++++++++++++++++--- libsolidity/formal/SymbolicVariables.h | 32 +++++++++++++++-- .../typecast/function_type_to_address.sol | 10 ++++++ ...unction_type_to_function_type_external.sol | 8 +++++ ...unction_type_to_function_type_internal.sol | 13 +++++++ .../types/function_type_as_argument.sol | 5 +++ .../types/function_type_call.sol | 13 +++++++ .../types/function_type_members.sol | 11 ++++++ .../types/function_type_nested.sol | 22 ++++++++++++ .../types/function_type_nested_return.sol | 27 +++++++++++++++ 15 files changed, 215 insertions(+), 19 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/typecast/function_type_to_address.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_external.sol create mode 100644 test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol create mode 100644 test/libsolidity/smtCheckerTests/types/function_type_as_argument.sol create mode 100644 test/libsolidity/smtCheckerTests/types/function_type_call.sol create mode 100644 test/libsolidity/smtCheckerTests/types/function_type_members.sol create mode 100644 test/libsolidity/smtCheckerTests/types/function_type_nested.sol create mode 100644 test/libsolidity/smtCheckerTests/types/function_type_nested_return.sol diff --git a/Changelog.md b/Changelog.md index c47a0dc1a..6064d9a82 100644 --- a/Changelog.md +++ b/Changelog.md @@ -17,6 +17,7 @@ Bugfixes: * Code Generator: Fixed a faulty assert that would wrongly trigger for array sizes exceeding unsigned integer * Type Checker: Treat magic variables as unknown identifiers in inline assembly * SMTChecker: Fix internal error when accessing indices of fixed bytes. + * SMTChecker: Fix internal error when using function pointers as arguments. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 22d70a5aa..a917faf82 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -508,7 +508,13 @@ smt::SortPointer CHC::sort(FunctionDefinition const& _function) auto boolSort = make_shared(smt::Kind::Bool); vector varSorts; for (auto const& var: _function.parameters() + _function.returnParameters()) - varSorts.push_back(smt::smtSort(*var->type())); + { + // SMT solvers do not support function types as arguments. + if (var->type()->category() == Type::Category::Function) + varSorts.push_back(make_shared(smt::Kind::Int)); + else + varSorts.push_back(smt::smtSort(*var->type())); + } return make_shared( m_stateSorts + varSorts, boolSort @@ -526,7 +532,13 @@ smt::SortPointer CHC::sort(ASTNode const* _node) auto boolSort = make_shared(smt::Kind::Bool); vector varSorts; for (auto const& var: m_currentFunction->localVariables()) - varSorts.push_back(smt::smtSort(*var->type())); + { + // SMT solvers do not support function types as arguments. + if (var->type()->category() == Type::Category::Function) + varSorts.push_back(make_shared(smt::Kind::Int)); + else + varSorts.push_back(smt::smtSort(*var->type())); + } return make_shared( fSort->domain + varSorts, boolSort @@ -540,7 +552,7 @@ unique_ptr CHC::createSymbolicBlock(smt::SortPoin _name, m_context ); - m_interface->registerRelation(block->currentValue()); + m_interface->registerRelation(block->currentFunctionValue()); return block; } @@ -572,7 +584,7 @@ smt::Expression CHC::error() smt::Expression CHC::error(unsigned _idx) { - return m_errorPredicate->valueAtIndex(_idx)({}); + return m_errorPredicate->functionValueAtIndex(_idx)({}); } unique_ptr CHC::createBlock(ASTNode const* _node, string const& _prefix) @@ -589,7 +601,7 @@ void CHC::createErrorBlock() { solAssert(m_errorPredicate, ""); m_errorPredicate->increaseIndex(); - m_interface->registerRelation(m_errorPredicate->currentValue()); + m_interface->registerRelation(m_errorPredicate->currentFunctionValue()); } void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints) diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 965da2d79..a9fb9f2b7 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -154,15 +154,15 @@ private: //@{ /// Constructor predicate. /// Default constructor sets state vars to 0. - std::unique_ptr m_constructorPredicate; + std::unique_ptr m_constructorPredicate; /// Artificial Interface predicate. /// Single entry block for all functions. - std::unique_ptr m_interfacePredicate; + std::unique_ptr m_interfacePredicate; /// Artificial Error predicate. /// Single error block for all assertions. - std::unique_ptr m_errorPredicate; + std::unique_ptr m_errorPredicate; //@} /// Variables. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index c55f2a52f..12d8c3cc8 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -594,10 +594,10 @@ void SMTEncoder::endVisit(Identifier const& _identifier) { // Will be translated as part of the node that requested the lvalue. } - else if (_identifier.annotation().type->category() == Type::Category::Function) - visitFunctionIdentifier(_identifier); else if (auto decl = identifierToVariable(_identifier)) defineExpr(_identifier, currentValue(*decl)); + else if (_identifier.annotation().type->category() == Type::Category::Function) + visitFunctionIdentifier(_identifier); else if (_identifier.name() == "now") defineGlobalVariable(_identifier.name(), _identifier); else if (_identifier.name() == "this") @@ -1343,7 +1343,7 @@ void SMTEncoder::createExpr(Expression const& _e) void SMTEncoder::defineExpr(Expression const& _e, smt::Expression _value) { createExpr(_e); - solAssert(smt::smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported"); + solAssert(_value.sort->kind != smt::Kind::Function, "Equality operator applied to type that is not fully supported"); m_context.addAssertion(expr(_e) == _value); } diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index ab23b8712..591158a25 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -19,6 +19,7 @@ #include #include +#include #include using namespace std; @@ -139,7 +140,28 @@ pair> newSymbolicVariable( else if (isBool(_type.category())) var = make_shared(type, _uniqueName, _context); else if (isFunction(_type.category())) - var = make_shared(type, _uniqueName, _context); + { + auto const& fType = dynamic_cast(type); + auto const& paramsIn = fType->parameterTypes(); + auto const& paramsOut = fType->returnParameterTypes(); + auto findFunctionParam = [&](auto&& params) { + return find_if( + begin(params), + end(params), + [&](TypePointer _paramType) { return _paramType->category() == solidity::Type::Category::Function; } + ); + }; + if ( + findFunctionParam(paramsIn) != end(paramsIn) || + findFunctionParam(paramsOut) != end(paramsOut) + ) + { + abstract = true; + var = make_shared(TypeProvider::uint256(), type, _uniqueName, _context); + } + else + var = make_shared(type, _uniqueName, _context); + } else if (isInteger(_type.category())) var = make_shared(type, type, _uniqueName, _context); else if (isFixedBytes(_type.category())) diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 3190cc6c6..3a814ec7d 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -19,7 +19,6 @@ #include #include -#include using namespace std; using namespace dev; @@ -153,16 +152,38 @@ SymbolicFunctionVariable::SymbolicFunctionVariable( solAssert(m_sort->kind == Kind::Function, ""); } -void SymbolicFunctionVariable::resetDeclaration() +Expression SymbolicFunctionVariable::currentValue(solidity::TypePointer const& _targetType) const { - m_declaration = m_context.newVariable(currentName(), m_sort); + return m_abstract.currentValue(_targetType); +} + +Expression SymbolicFunctionVariable::currentFunctionValue() const +{ + return m_declaration; +} + +Expression SymbolicFunctionVariable::valueAtIndex(int _index) const +{ + return m_abstract.valueAtIndex(_index); +} + +Expression SymbolicFunctionVariable::functionValueAtIndex(int _index) const +{ + return SymbolicVariable::valueAtIndex(_index); +} + +Expression SymbolicFunctionVariable::resetIndex() +{ + SymbolicVariable::resetIndex(); + return m_abstract.resetIndex(); } Expression SymbolicFunctionVariable::increaseIndex() { ++(*m_ssa); resetDeclaration(); - return currentValue(); + m_abstract.increaseIndex(); + return m_abstract.currentValue(); } Expression SymbolicFunctionVariable::operator()(vector _arguments) const @@ -170,6 +191,11 @@ Expression SymbolicFunctionVariable::operator()(vector _arguments) c return m_declaration(_arguments); } +void SymbolicFunctionVariable::resetDeclaration() +{ + m_declaration = m_context.newVariable(currentName(), m_sort); +} + SymbolicMappingVariable::SymbolicMappingVariable( solidity::TypePointer _type, string _uniqueName, diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index c65a26326..9ae637490 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -20,6 +20,7 @@ #include #include #include +#include #include namespace dev @@ -138,7 +139,12 @@ public: }; /** - * Specialization of SymbolicVariable for FunctionType + * Specialization of SymbolicVariable for FunctionType. + * Besides containing a symbolic function declaration, + * it also has an integer used as abstraction. + * By default, the abstract representation is used when + * values are requested, and the function declaration is + * used when operator() is applied over arguments. */ class SymbolicFunctionVariable: public SymbolicVariable { @@ -154,8 +160,20 @@ public: EncodingContext& _context ); - Expression increaseIndex(); - Expression operator()(std::vector _arguments) const; + Expression currentValue(solidity::TypePointer const& _targetType = TypePointer{}) const override; + + // Explicit request the function declaration. + Expression currentFunctionValue() const; + + Expression valueAtIndex(int _index) const override; + + // Explicit request the function declaration. + Expression functionValueAtIndex(int _index) const; + + Expression resetIndex() override; + Expression increaseIndex() override; + + Expression operator()(std::vector _arguments) const override; private: /// Creates a new function declaration. @@ -163,6 +181,14 @@ private: /// Stores the current function declaration. Expression m_declaration; + + /// Abstract representation. + SymbolicIntVariable m_abstract{ + TypeProvider::uint256(), + TypeProvider::uint256(), + m_uniqueName + "_abstract", + m_context + }; }; /** diff --git a/test/libsolidity/smtCheckerTests/typecast/function_type_to_address.sol b/test/libsolidity/smtCheckerTests/typecast/function_type_to_address.sol new file mode 100644 index 000000000..c0b7d109d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/function_type_to_address.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract C { + function f(address a, function(uint) external g) internal pure { + address b = address(g); + assert(a == b); + } +} +// ---- +// Warning: (128-138): Type conversion is not yet fully supported and might yield false positives. +// Warning: (142-156): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_external.sol b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_external.sol new file mode 100644 index 000000000..799852592 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_external.sol @@ -0,0 +1,8 @@ +pragma experimental SMTChecker; +contract C { + function f(function(uint) external returns (uint) g, function(uint) external returns (uint) h) public { + assert(g(2) == h(2)); + } +} +// ---- +// Warning: (155-175): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol new file mode 100644 index 000000000..1657a95c6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_internal.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + function f(function(uint) returns (uint) g, function(uint) returns (uint) h) internal { + assert(g(2) == h(2)); + assert(g == h); + } +} +// ---- +// Warning: (146-150): Assertion checker does not yet implement this type of function call. +// Warning: (154-158): Assertion checker does not yet implement this type of function call. +// Warning: (170-176): Assertion checker does not yet implement the type function (uint256) returns (uint256) for comparisons +// Warning: (139-159): Assertion violation happens here +// Warning: (163-177): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/function_type_as_argument.sol b/test/libsolidity/smtCheckerTests/types/function_type_as_argument.sol new file mode 100644 index 000000000..0ba33e408 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/function_type_as_argument.sol @@ -0,0 +1,5 @@ +pragma experimental SMTChecker; +contract C { + function f(function(uint) external g) public { + } +} diff --git a/test/libsolidity/smtCheckerTests/types/function_type_call.sol b/test/libsolidity/smtCheckerTests/types/function_type_call.sol new file mode 100644 index 000000000..90a80dd9e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/function_type_call.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + function(uint) m_g; + function f(function(uint) internal g) internal { + g(2); + } + function h() public { + f(m_g); + } +} +// ---- +// Warning: (121-125): Assertion checker does not yet implement this type of function call. +// Warning: (121-125): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/function_type_members.sol b/test/libsolidity/smtCheckerTests/types/function_type_members.sol new file mode 100644 index 000000000..2296fa798 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/function_type_members.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; +contract C { + function f(function(uint) external payable g) internal { + g.selector; + g.gas(2).value(3)(4); + } +} +// ---- +// Warning: (108-118): Assertion checker does not yet support this expression. +// Warning: (122-130): Assertion checker does not yet implement this type of function call. +// Warning: (122-139): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/function_type_nested.sol b/test/libsolidity/smtCheckerTests/types/function_type_nested.sol new file mode 100644 index 000000000..5eb637315 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/function_type_nested.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; +contract C { + function(uint) m_g; + function f1(function(uint) internal g1) internal { + g1(2); + } + function f2(function(function(uint) internal) internal g2) internal { + g2(m_g); + } + function h() public { + f2(f1); + } +} +// ---- +// Warning: (123-128): Assertion checker does not yet implement this type of function call. +// Warning: (152-197): Assertion checker does not yet support the type of this variable. +// Warning: (212-214): Assertion checker does not yet implement type function (function (uint256)) +// Warning: (212-219): Assertion checker does not yet implement this type of function call. +// Warning: (255-257): Internal error: Expression undefined for SMT solver. +// Warning: (255-257): Assertion checker does not yet implement type function (function (uint256)) +// Warning: (212-214): Assertion checker does not yet implement type function (function (uint256)) +// Warning: (212-219): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/function_type_nested_return.sol b/test/libsolidity/smtCheckerTests/types/function_type_nested_return.sol new file mode 100644 index 000000000..2e974fef8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/function_type_nested_return.sol @@ -0,0 +1,27 @@ +pragma experimental SMTChecker; +contract C { + function(uint) m_g; + function r() internal view returns (function(uint)) { + return m_g; + } + function f1(function(uint) internal g1) internal { + g1(2); + } + function f2(function(function(uint) internal) internal g2) internal { + g2(r()); + } + function h() public { + f2(f1); + } +} +// ---- +// Warning: (195-200): Assertion checker does not yet implement this type of function call. +// Warning: (224-269): Assertion checker does not yet support the type of this variable. +// Warning: (284-286): Assertion checker does not yet implement type function (function (uint256)) +// Warning: (287-288): Assertion checker does not yet support this global variable. +// Warning: (284-291): Assertion checker does not yet implement this type of function call. +// Warning: (327-329): Internal error: Expression undefined for SMT solver. +// Warning: (327-329): Assertion checker does not yet implement type function (function (uint256)) +// Warning: (284-286): Assertion checker does not yet implement type function (function (uint256)) +// Warning: (287-288): Assertion checker does not yet support this global variable. +// Warning: (284-291): Assertion checker does not yet implement this type of function call.