From be065a1243324fb7ae937f23369746007cb9717f Mon Sep 17 00:00:00 2001 From: Federico Bond Date: Sun, 24 Dec 2017 04:43:53 -0300 Subject: [PATCH 1/6] grammar.txt: Add optional storage location to parameters --- docs/grammar.txt | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/docs/grammar.txt b/docs/grammar.txt index ce3fd3ad5..e700c9465 100644 --- a/docs/grammar.txt +++ b/docs/grammar.txt @@ -27,14 +27,19 @@ ModifierInvocation = Identifier ( '(' ExpressionList? ')' )? FunctionDefinition = 'function' Identifier? ParameterList ( ModifierInvocation | StateMutability | 'external' | 'public' | 'internal' | 'private' )* ( 'returns' ParameterList )? ( ';' | Block ) -EventDefinition = 'event' Identifier IndexedParameterList 'anonymous'? ';' +EventDefinition = 'event' Identifier EventParameterList 'anonymous'? ';' EnumValue = Identifier EnumDefinition = 'enum' Identifier '{' EnumValue? (',' EnumValue)* '}' -IndexedParameterList = '(' ( TypeName 'indexed'? Identifier? (',' TypeName 'indexed'? Identifier?)* )? ')' -ParameterList = '(' ( TypeName Identifier? (',' TypeName Identifier?)* )? ')' -TypeNameList = '(' ( TypeName (',' TypeName )* )? ')' +ParameterList = '(' ( Parameter (',' Parameter)* )? ')' +Parameter = TypeName StorageLocation? Identifier? + +EventParameterList = '(' ( EventParameter (',' EventParameter )* )? ')' +EventParameter = TypeName 'indexed'? Identifier? + +FunctionTypeParameterList = '(' ( FunctionTypeParameter (',' FunctionTypeParameter )* )? ')' +FunctionTypeParameter = TypeName StorageLocation? // semantic restriction: mappings and structs (recursively) containing mappings // are not allowed in argument lists @@ -50,8 +55,8 @@ UserDefinedTypeName = Identifier ( '.' Identifier )* Mapping = 'mapping' '(' ElementaryTypeName '=>' TypeName ')' ArrayTypeName = TypeName '[' Expression? ']' -FunctionTypeName = 'function' TypeNameList ( 'internal' | 'external' | StateMutability )* - ( 'returns' TypeNameList )? +FunctionTypeName = 'function' FunctionTypeParameterList ( 'internal' | 'external' | StateMutability )* + ( 'returns' FunctionTypeParameterList )? StorageLocation = 'memory' | 'storage' StateMutability = 'pure' | 'constant' | 'view' | 'payable' From 00692a4ff66551ae99920380cc4e43de377e63c7 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 4 Jan 2018 14:24:19 +0100 Subject: [PATCH 2/6] Reset source location after using inline assembly. --- libsolidity/codegen/CompilerContext.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/libsolidity/codegen/CompilerContext.cpp b/libsolidity/codegen/CompilerContext.cpp index ce9c3b7f6..ab10d7dd0 100644 --- a/libsolidity/codegen/CompilerContext.cpp +++ b/libsolidity/codegen/CompilerContext.cpp @@ -347,6 +347,9 @@ void CompilerContext::appendInlineAssembly( solAssert(errorReporter.errors().empty(), "Failed to analyze inline assembly block."); assembly::CodeGenerator::assemble(*parserResult, analysisInfo, *m_asm, identifierAccess, _system); + + // Reset the source location to the one of the node (instead of the CODEGEN source location) + updateSourceLocation(); } FunctionDefinition const& CompilerContext::resolveVirtualFunction( From 7f4cf00f1b6a41c1fd409dbca329d7bc17f4fd56 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 4 Jan 2018 14:24:35 +0100 Subject: [PATCH 3/6] Provide easy way to update source location expectation. --- test/libsolidity/Assembly.cpp | 54 +++++++++++++++++++++++++++++------ 1 file changed, 45 insertions(+), 9 deletions(-) diff --git a/test/libsolidity/Assembly.cpp b/test/libsolidity/Assembly.cpp index 358d3c720..59af6d412 100644 --- a/test/libsolidity/Assembly.cpp +++ b/test/libsolidity/Assembly.cpp @@ -86,23 +86,59 @@ eth::AssemblyItems compileContract(const string& _sourceCode) return AssemblyItems(); } +void printAssemblyLocations(AssemblyItems const& _items) +{ + auto printRepeated = [](SourceLocation const& _loc, size_t _repetitions) + { + cout << + "\t\tvector(" << + _repetitions << + ", SourceLocation(" << + _loc.start << + ", " << + _loc.end << + ", make_shared(\"" << + *_loc.sourceName << + "\"))) +" << endl; + }; + + vector locations; + for (auto const& item: _items) + locations.push_back(item.location()); + size_t repetitions = 0; + SourceLocation const* previousLoc = nullptr; + for (size_t i = 0; i < locations.size(); ++i) + { + SourceLocation& loc = locations[i]; + if (previousLoc && *previousLoc == loc) + repetitions++; + else + { + if (previousLoc) + printRepeated(*previousLoc, repetitions); + previousLoc = &loc; + repetitions = 1; + } + } + if (previousLoc) + printRepeated(*previousLoc, repetitions); +} + void checkAssemblyLocations(AssemblyItems const& _items, vector const& _locations) { BOOST_CHECK_EQUAL(_items.size(), _locations.size()); for (size_t i = 0; i < min(_items.size(), _locations.size()); ++i) { - BOOST_CHECK_MESSAGE( - _items[i].location() == _locations[i], - "Location mismatch for assembly item " + to_string(i) + ". Found: " + - (_items[i].location().sourceName ? *_items[i].location().sourceName + ":" : "(null source name)") + - to_string(_items[i].location().start) + "-" + - to_string(_items[i].location().end) + ", expected: " + - (_locations[i].sourceName ? *_locations[i].sourceName + ":" : "(null source name)") + - to_string(_locations[i].start) + "-" + - to_string(_locations[i].end)); + if (_items[i].location() != _locations[i]) + { + BOOST_CHECK_MESSAGE(false, "Location mismatch for item " + to_string(i) + ". Found the following locations:"); + printAssemblyLocations(_items); + return; + } } } + } // end anonymous namespace BOOST_AUTO_TEST_SUITE(Assembly) From 6a9a4e2bb860e7e1c8bd832b251dc6877912c233 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 4 Jan 2018 17:19:45 +0100 Subject: [PATCH 4/6] Explain the difference to inline assembly. --- docs/julia.rst | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/docs/julia.rst b/docs/julia.rst index 309e6b369..9e961a9dd 100644 --- a/docs/julia.rst +++ b/docs/julia.rst @@ -14,6 +14,13 @@ It can already be used for "inline assembly" inside Solidity and future versions of the Solidity compiler will even use JULIA as intermediate language. It should also be easy to build high-level optimizer stages for JULIA. +.. note:: + + Note that the flavour used for "inline assembly" does not have types + (everything is ``u256``) and the built-in functions are identical + to the EVM opcodes. Please resort to the inline assembly documentation + for details. + The core components of JULIA are functions, blocks, variables, literals, for-loops, if-statements, switch-statements, expressions and assignments to variables. From d0abc5359b24a27376cc1a4ba8d0b35e7ca036d2 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 18 Dec 2017 19:43:15 +0100 Subject: [PATCH 5/6] [SMTChecker] Variables are merged after branches (ite variables) --- libsolidity/formal/SMTChecker.cpp | 32 ++++++++++++++++----- libsolidity/formal/SMTChecker.h | 18 ++++++++---- test/libsolidity/SMTChecker.cpp | 47 +++++++++++++++++++++++++------ 3 files changed, 76 insertions(+), 21 deletions(-) diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index a85297956..a64024b36 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -91,15 +91,16 @@ bool SMTChecker::visit(IfStatement const& _node) checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE."); - visitBranch(_node.trueStatement(), expr(_node.condition())); + auto countersEndFalse = m_currentSequenceCounter; + auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition())); vector touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement()); if (_node.falseStatement()) { - visitBranch(*_node.falseStatement(), !expr(_node.condition())); + countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition())); touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement()); } - resetVariables(touchedVariables); + mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse); return false; } @@ -506,12 +507,12 @@ void SMTChecker::assignment(Declaration const& _variable, smt::Expression const& m_interface->addAssertion(newValue(_variable) == _value); } -void SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition) +SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition) { - visitBranch(_statement, &_condition); + return visitBranch(_statement, &_condition); } -void SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition) +SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition) { VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter; @@ -522,7 +523,8 @@ void SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* popPathCondition(); m_conditionalExecutionHappened = true; - m_currentSequenceCounter = sequenceCountersStart; + std::swap(sequenceCountersStart, m_currentSequenceCounter); + return sequenceCountersStart; } void SMTChecker::checkCondition( @@ -702,6 +704,22 @@ void SMTChecker::resetVariables(vector _variables) } } +void SMTChecker::mergeVariables(vector const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse) +{ + set uniqueVars(_variables.begin(), _variables.end()); + for (auto const* decl: uniqueVars) + { + int trueCounter = _countersEndTrue.at(decl); + int falseCounter = _countersEndFalse.at(decl); + solAssert(trueCounter != falseCounter, ""); + m_interface->addAssertion(newValue(*decl) == smt::Expression::ite( + _condition, + valueAtSequence(*decl, trueCounter), + valueAtSequence(*decl, falseCounter)) + ); + } +} + bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { if (dynamic_cast(_varDecl.type().get())) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index d4c2cf6f0..b57f0f96b 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -75,10 +75,14 @@ private: void assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location); void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location); - // Visits the branch given by the statement, pushes and pops the SMT checker. - // @param _condition if present, asserts that this condition is true within the branch. - void visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr); - void visitBranch(Statement const& _statement, smt::Expression _condition); + /// Maps a variable to an SSA index. + using VariableSequenceCounters = std::map; + + /// Visits the branch given by the statement, pushes and pops the current path conditions. + /// @param _condition if present, asserts that this condition is true within the branch. + /// @returns the variable sequence counter after visiting the branch. + VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr); + VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression _condition); /// Check that a condition can be satisfied. void checkCondition( @@ -106,6 +110,10 @@ private: void initializeLocalVariables(FunctionDefinition const& _function); void resetVariables(std::vector _variables); + /// Given two different branches and the touched variables, + /// merge the touched variables into after-branch ite variables + /// using the branch condition as guard. + void mergeVariables(std::vector const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse); /// Tries to create an uninitialized variable and returns true on success. /// This fails if the type is not supported. bool createVariable(VariableDeclaration const& _varDecl); @@ -134,8 +142,6 @@ private: static smt::Expression minValue(IntegerType const& _t); static smt::Expression maxValue(IntegerType const& _t); - using VariableSequenceCounters = std::map; - /// Returns the expression corresponding to the AST node. Throws if the expression does not exist. smt::Expression expr(Expression const& _e); /// Creates the expression (value can be arbitrary) diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 3a65aa433..2a1609cc4 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -168,9 +168,9 @@ BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars) CHECK_SUCCESS_NO_WARNINGS(text); } -BOOST_AUTO_TEST_CASE(branches_clear_variables) +BOOST_AUTO_TEST_CASE(branches_merge_variables) { - // Only clears accessed variables + // Branch does not touch variable a string text = R"( contract C { function f(uint x) public pure { @@ -182,7 +182,7 @@ BOOST_AUTO_TEST_CASE(branches_clear_variables) } )"; CHECK_SUCCESS_NO_WARNINGS(text); - // It is just a plain clear and will not combine branches. + // Positive branch touches variable a, but assertion should still hold. text = R"( contract C { function f(uint x) public pure { @@ -194,8 +194,8 @@ BOOST_AUTO_TEST_CASE(branches_clear_variables) } } )"; - CHECK_WARNING(text, "Assertion violation happens here"); - // Clear also works on the else branch + CHECK_SUCCESS_NO_WARNINGS(text); + // Negative branch touches variable a, but assertion should still hold. text = R"( contract C { function f(uint x) public pure { @@ -208,8 +208,8 @@ BOOST_AUTO_TEST_CASE(branches_clear_variables) } } )"; - CHECK_WARNING(text, "Assertion violation happens here"); - // Variable is not cleared, if it is only read. + CHECK_SUCCESS_NO_WARNINGS(text); + // Variable is not merged, if it is only read. text = R"( contract C { function f(uint x) public pure { @@ -224,6 +224,36 @@ BOOST_AUTO_TEST_CASE(branches_clear_variables) } )"; CHECK_SUCCESS_NO_WARNINGS(text); + // Variable is reset in both branches + text = R"( + contract C { + function f(uint x) public pure { + uint a = 2; + if (x > 10) { + a = 3; + } else { + a = 3; + } + assert(a == 3); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); + // Variable is reset in both branches + text = R"( + contract C { + function f(uint x) public pure { + uint a = 2; + if (x > 10) { + a = 3; + } else { + a = 4; + } + assert(a >= 3); + } + } + )"; + CHECK_SUCCESS_NO_WARNINGS(text); } BOOST_AUTO_TEST_CASE(branches_assert_condition) @@ -262,7 +292,7 @@ BOOST_AUTO_TEST_CASE(branches_assert_condition) CHECK_SUCCESS_NO_WARNINGS(text); } -BOOST_AUTO_TEST_CASE(ways_to_clear_variables) +BOOST_AUTO_TEST_CASE(ways_to_merge_variables) { string text = R"( contract C { @@ -275,6 +305,7 @@ BOOST_AUTO_TEST_CASE(ways_to_clear_variables) } } )"; + CHECK_WARNING(text, "Assertion violation happens here"); text = R"( contract C { function f(uint x) public pure { From e27418cb3369c8b7fa3f18ef63425ea2918b7cee Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 4 Jan 2018 21:23:56 +0100 Subject: [PATCH 6/6] [SMTChecker] Added feature line to Changelog --- Changelog.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Changelog.md b/Changelog.md index 13c8118f9..bfaeeb27a 100644 --- a/Changelog.md +++ b/Changelog.md @@ -3,6 +3,8 @@ Features: * Limit the number of warnings raised for creating abstract contracts. * Inline Assembly: Issue warning for using jump labels (already existed for jump instructions). + * SMT Checker: If-else branch conditions are taken into account in the SMT encoding of the program + variables. Bugfixes: * Parser: Disallow event declarations with no parameter list.