diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | docs/solidity-by-example.rst | 7 | ||||
| -rw-r--r-- | docs/utils/SolidityLexer.py | 10 | ||||
| -rw-r--r-- | libevmasm/JumpdestRemover.cpp | 4 | ||||
| -rw-r--r-- | libsolidity/formal/SMTLib2Interface.cpp | 11 | ||||
| -rw-r--r-- | libsolidity/formal/SMTLib2Interface.h | 8 | ||||
| -rw-r--r-- | libsolidity/formal/SolverInterface.h | 72 | ||||
| -rw-r--r-- | test/libsolidity/SolidityNameAndTypeResolution.cpp | 34 |
8 files changed, 69 insertions, 78 deletions
@@ -34,6 +34,7 @@ prerelease.txt build/ docs/_build docs/utils/__pycache__ +docs/utils/*.pyc # vim stuff *.swp diff --git a/docs/solidity-by-example.rst b/docs/solidity-by-example.rst index 59ab7962..9489665e 100644 --- a/docs/solidity-by-example.rst +++ b/docs/solidity-by-example.rst @@ -492,7 +492,7 @@ high or low invalid bids. if (amount > 0) { // It is important to set this to zero because the recipient // can call this function again as part of the receiving call - // before `send` returns (see the remark above about + // before `transfer` returns (see the remark above about // conditions -> effects -> interaction). pendingReturns[msg.sender] = 0; @@ -508,12 +508,11 @@ high or low invalid bids. require(!ended); AuctionEnded(highestBidder, highestBid); ended = true; - // We send all the money we have, because some - // of the refunds might have failed. - beneficiary.transfer(this.balance); + beneficiary.transfer(highestBid); } } + .. index:: purchase, remote purchase, escrow ******************** diff --git a/docs/utils/SolidityLexer.py b/docs/utils/SolidityLexer.py index a828146f..50f51cf4 100644 --- a/docs/utils/SolidityLexer.py +++ b/docs/utils/SolidityLexer.py @@ -56,7 +56,7 @@ class SolidityLexer(RegexLexer): (r'[})\].]', Punctuation), (r'(anonymous|as|assembly|break|constant|continue|do|delete|else|external|for|hex|if|' r'indexed|internal|import|is|mapping|memory|new|payable|public|pragma|' - r'private|return|returns|storage|super|this|throw|using|while)\b', Keyword, 'slashstartsregex'), + r'private|pure|return|returns|storage|super|this|throw|using|view|while)\b', Keyword, 'slashstartsregex'), (r'(var|function|event|modifier|struct|enum|contract|library|interface)\b', Keyword.Declaration, 'slashstartsregex'), (r'(bytes|string|address|uint|int|bool|byte|' + '|'.join( @@ -67,15 +67,15 @@ class SolidityLexer(RegexLexer): ['fixed%dx%d' % ((i), (j + 8)) for i in range(0, 256, 8) for j in range(0, 256 - i, 8)] ) + r')\b', Keyword.Type, 'slashstartsregex'), (r'(wei|szabo|finney|ether|seconds|minutes|hours|days|weeks|years)\b', Keyword.Type, 'slashstartsregex'), - (r'(abstract|after|case|catch|default|final|in|inline|interface|let|match|' - r'null|of|pure|relocatable|static|switch|try|type|typeof|view)\b', Keyword.Reserved), + (r'(abstract|after|case|catch|default|final|in|inline|let|match|' + r'null|of|relocatable|static|switch|try|type|typeof)\b', Keyword.Reserved), (r'(true|false)\b', Keyword.Constant), (r'(block|msg|tx|now|suicide|selfdestruct|addmod|mulmod|sha3|keccak256|log[0-4]|' r'sha256|ecrecover|ripemd160|assert|revert|require)', Name.Builtin), (r'[$a-zA-Z_][a-zA-Z0-9_]*', Name.Other), - (r'[0-9][0-9]*\.[0-9]+([eE][0-9]+)?[fd]?', Number.Float), + (r'[0-9][0-9]*\.[0-9]+([eE][0-9]+)?', Number.Float), (r'0x[0-9a-fA-F]+', Number.Hex), - (r'[0-9]+', Number.Integer), + (r'[0-9]+([eE][0-9]+)?', Number.Integer), (r'"(\\\\|\\"|[^"])*"', String.Double), (r"'(\\\\|\\'|[^'])*'", String.Single), ] diff --git a/libevmasm/JumpdestRemover.cpp b/libevmasm/JumpdestRemover.cpp index b6016798..60493a99 100644 --- a/libevmasm/JumpdestRemover.cpp +++ b/libevmasm/JumpdestRemover.cpp @@ -21,8 +21,6 @@ #include "JumpdestRemover.h" -#include <libsolidity/interface/Exceptions.h> - #include <libevmasm/AssemblyItem.h> using namespace std; @@ -45,7 +43,7 @@ bool JumpdestRemover::optimise(set<size_t> const& _tagsReferencedFromOutside) if (_item.type() != Tag) return false; auto asmIdAndTag = _item.splitForeignPushTag(); - solAssert(asmIdAndTag.first == size_t(-1), "Sub-assembly tag used as label."); + assertThrow(asmIdAndTag.first == size_t(-1), OptimizerException, "Sub-assembly tag used as label."); size_t tag = asmIdAndTag.second; return !references.count(tag); } diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index c627057a..0e00665a 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -64,8 +64,6 @@ void SMTLib2Interface::pop() Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain) { - solAssert(!m_variables.count(_name), ""); - m_variables[_name] = SMTVariableType::Function; write( "(declare-fun |" + _name + @@ -80,16 +78,12 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom Expression SMTLib2Interface::newInteger(string _name) { - solAssert(!m_variables.count(_name), ""); - m_variables[_name] = SMTVariableType::Integer; write("(declare-const |" + _name + "| Int)"); return SolverInterface::newInteger(move(_name)); } Expression SMTLib2Interface::newBool(string _name) { - solAssert(!m_variables.count(_name), ""); - m_variables[_name] = SMTVariableType::Bool; write("(declare-const |" + _name + "| Bool)"); return SolverInterface::newBool(std::move(_name)); } @@ -151,9 +145,8 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _ for (size_t i = 0; i < _expressionsToEvaluate.size(); i++) { auto const& e = _expressionsToEvaluate.at(i); - solAssert(m_variables.count(e.name), ""); - solAssert(m_variables[e.name] == SMTVariableType::Integer, ""); - command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n"; + solAssert(e.sort == Sort::Int || e.sort == Sort::Bool, "Invalid sort for expression to evaluate."); + command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + "\n"; command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n"; } command += "(check-sat)\n"; diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index e827449f..63188acd 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -68,14 +68,6 @@ private: ReadCallback::Callback m_queryCallback; std::vector<std::string> m_accumulatedOutput; - - enum class SMTVariableType { - Function, - Integer, - Bool - }; - - std::map<std::string,SMTVariableType> m_variables; }; } diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index a69d19d5..c9adf863 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -44,7 +44,9 @@ enum class CheckResult enum class Sort { - Int, Bool + Int, + Bool, + IntIntFun // Function of one Int returning a single Int }; /// C++ representation of an SMTLIB2 expression. @@ -52,10 +54,10 @@ class Expression { friend class SolverInterface; public: - explicit Expression(bool _v): name(_v ? "true" : "false") {} - Expression(size_t _number): name(std::to_string(_number)) {} - Expression(u256 const& _number): name(_number.str()) {} - Expression(bigint const& _number): name(_number.str()) {} + explicit Expression(bool _v): name(_v ? "true" : "false"), sort(Sort::Bool) {} + Expression(size_t _number): name(std::to_string(_number)), sort(Sort::Int) {} + Expression(u256 const& _number): name(_number.str()), sort(Sort::Int) {} + Expression(bigint const& _number): name(_number.str()), sort(Sort::Int) {} Expression(Expression const&) = default; Expression(Expression&&) = default; @@ -64,26 +66,27 @@ public: static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue) { + solAssert(_trueValue.sort == _falseValue.sort, ""); return Expression("ite", std::vector<Expression>{ std::move(_condition), std::move(_trueValue), std::move(_falseValue) - }); + }, _trueValue.sort); } friend Expression operator!(Expression _a) { - return Expression("not", std::move(_a)); + return Expression("not", std::move(_a), Sort::Bool); } friend Expression operator&&(Expression _a, Expression _b) { - return Expression("and", std::move(_a), std::move(_b)); + return Expression("and", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator||(Expression _a, Expression _b) { - return Expression("or", std::move(_a), std::move(_b)); + return Expression("or", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator==(Expression _a, Expression _b) { - return Expression("=", std::move(_a), std::move(_b)); + return Expression("=", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator!=(Expression _a, Expression _b) { @@ -91,52 +94,56 @@ public: } friend Expression operator<(Expression _a, Expression _b) { - return Expression("<", std::move(_a), std::move(_b)); + return Expression("<", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator<=(Expression _a, Expression _b) { - return Expression("<=", std::move(_a), std::move(_b)); + return Expression("<=", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator>(Expression _a, Expression _b) { - return Expression(">", std::move(_a), std::move(_b)); + return Expression(">", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator>=(Expression _a, Expression _b) { - return Expression(">=", std::move(_a), std::move(_b)); + return Expression(">=", std::move(_a), std::move(_b), Sort::Bool); } friend Expression operator+(Expression _a, Expression _b) { - return Expression("+", std::move(_a), std::move(_b)); + return Expression("+", std::move(_a), std::move(_b), Sort::Int); } friend Expression operator-(Expression _a, Expression _b) { - return Expression("-", std::move(_a), std::move(_b)); + return Expression("-", std::move(_a), std::move(_b), Sort::Int); } friend Expression operator*(Expression _a, Expression _b) { - return Expression("*", std::move(_a), std::move(_b)); + return Expression("*", std::move(_a), std::move(_b), Sort::Int); } Expression operator()(Expression _a) const { - solAssert(arguments.empty(), "Attempted function application to non-function."); - return Expression(name, _a); + solAssert( + sort == Sort::IntIntFun && arguments.empty(), + "Attempted function application to non-function." + ); + return Expression(name, _a, Sort::Int); } std::string const name; std::vector<Expression> const arguments; + Sort sort; private: /// Manual constructor, should only be used by SolverInterface and this class itself. - Expression(std::string _name, std::vector<Expression> _arguments): - name(std::move(_name)), arguments(std::move(_arguments)) {} - - explicit Expression(std::string _name): - Expression(std::move(_name), std::vector<Expression>{}) {} - Expression(std::string _name, Expression _arg): - Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}) {} - Expression(std::string _name, Expression _arg1, Expression _arg2): - Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}) {} + Expression(std::string _name, std::vector<Expression> _arguments, Sort _sort): + name(std::move(_name)), arguments(std::move(_arguments)), sort(_sort) {} + + explicit Expression(std::string _name, Sort _sort): + Expression(std::move(_name), std::vector<Expression>{}, _sort) {} + Expression(std::string _name, Expression _arg, Sort _sort): + Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}, _sort) {} + Expression(std::string _name, Expression _arg1, Expression _arg2, Sort _sort): + Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}, _sort) {} }; DEV_SIMPLE_EXCEPTION(SolverError); @@ -149,20 +156,21 @@ public: virtual void push() = 0; virtual void pop() = 0; - virtual Expression newFunction(std::string _name, Sort /*_domain*/, Sort /*_codomain*/) + virtual Expression newFunction(std::string _name, Sort _domain, Sort _codomain) { + solAssert(_domain == Sort::Int && _codomain == Sort::Int, "Function sort not supported."); // Subclasses should do something here - return Expression(std::move(_name), {}); + return Expression(std::move(_name), {}, Sort::IntIntFun); } virtual Expression newInteger(std::string _name) { // Subclasses should do something here - return Expression(std::move(_name), {}); + return Expression(std::move(_name), {}, Sort::Int); } virtual Expression newBool(std::string _name) { // Subclasses should do something here - return Expression(std::move(_name), {}); + return Expression(std::move(_name), {}, Sort::Bool); } virtual void addAssertion(Expression const& _expr) = 0; diff --git a/test/libsolidity/SolidityNameAndTypeResolution.cpp b/test/libsolidity/SolidityNameAndTypeResolution.cpp index 73c1660e..97d359e8 100644 --- a/test/libsolidity/SolidityNameAndTypeResolution.cpp +++ b/test/libsolidity/SolidityNameAndTypeResolution.cpp @@ -1038,7 +1038,7 @@ BOOST_AUTO_TEST_CASE(function_modifier_double_invocation) modifier mod(uint a) { if (a > 0) _; } } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(base_constructor_double_invocation) @@ -1392,7 +1392,7 @@ BOOST_AUTO_TEST_CASE(events_with_same_name) event A(uint i); } )"; - BOOST_CHECK(success(text)); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(events_with_same_name_unnamed_arguments) @@ -4033,7 +4033,7 @@ BOOST_AUTO_TEST_CASE(varM_disqualified_as_keyword) } } )"; - BOOST_CHECK(!success(text)); + CHECK_ERROR(text, DeclarationError, "Identifier not found or not unique."); } BOOST_AUTO_TEST_CASE(modifier_is_not_a_valid_typename) @@ -4074,7 +4074,7 @@ BOOST_AUTO_TEST_CASE(long_uint_variable_fails) } } )"; - BOOST_CHECK(!success(text)); + CHECK_ERROR(text, DeclarationError, "Identifier not found or not unique."); } BOOST_AUTO_TEST_CASE(bytes10abc_is_identifier) @@ -4113,7 +4113,7 @@ BOOST_AUTO_TEST_CASE(library_functions_do_not_have_value) } } )"; - BOOST_CHECK(!success(text)); + CHECK_ERROR(text, TypeError, "Member \"value\" not found or not visible after argument-dependent lookup in function ()"); } BOOST_AUTO_TEST_CASE(invalid_fixed_types_0x7_mxn) @@ -5690,7 +5690,7 @@ BOOST_AUTO_TEST_CASE(constructible_internal_constructor) function D() public { } } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(return_structs) @@ -5703,7 +5703,7 @@ BOOST_AUTO_TEST_CASE(return_structs) } } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(return_recursive_structs) @@ -5753,7 +5753,7 @@ BOOST_AUTO_TEST_CASE(address_checksum_type_deduction) } } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(invalid_address_checksum) @@ -5896,7 +5896,7 @@ BOOST_AUTO_TEST_CASE(interface) interface I { } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(interface_constructor) @@ -5917,7 +5917,7 @@ BOOST_AUTO_TEST_CASE(interface_functions) function f(); } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(interface_function_bodies) @@ -5939,7 +5939,7 @@ BOOST_AUTO_TEST_CASE(interface_function_external) function f() external; } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(interface_function_public) @@ -5980,7 +5980,7 @@ BOOST_AUTO_TEST_CASE(interface_events) event E(); } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(interface_inheritance) @@ -6023,7 +6023,7 @@ BOOST_AUTO_TEST_CASE(interface_function_parameters) function f(uint a) public returns (bool); } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(interface_enums) @@ -6047,7 +6047,7 @@ BOOST_AUTO_TEST_CASE(using_interface) } } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(using_interface_complex) @@ -6064,7 +6064,7 @@ BOOST_AUTO_TEST_CASE(using_interface_complex) } } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(warn_about_throw) @@ -6123,7 +6123,7 @@ BOOST_AUTO_TEST_CASE(pure_statement_check_for_regular_for_loop) } } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(warn_multiple_storage_storage_copies) @@ -6239,7 +6239,7 @@ BOOST_AUTO_TEST_CASE(warn_unused_function_parameter) } } )"; - success(text); + CHECK_SUCCESS(text); } BOOST_AUTO_TEST_CASE(warn_unused_return_parameter) |