Merge branch 'develop' of https://github.com/ethereum/solidity into develop

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.

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 = '(' ( Parameter (',' Parameter)* )? ')'
-ParameterList =        '(' ( TypeName            Identifier? (',' TypeName            Identifier?)* )? ')'
+Parameter = TypeName StorageLocation? Identifier?
-TypeNameList =         '(' ( TypeName (',' TypeName )* )? ')'
+
+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 )*
+FunctionTypeName = 'function' FunctionTypeParameterList ( 'internal' | 'external' | StateMutability )*
-                   ( 'returns' TypeNameList )?
+                   ( 'returns' FunctionTypeParameterList )?
 StorageLocation = 'memory' | 'storage'
 StateMutability = 'pure' | 'constant' | 'view' | 'payable'
 

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.
 

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(

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<Declaration const*> 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<Declaration const*> _variables)
 	}
 }
 
+void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse)
+{
+	set<Declaration const*> 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<IntegerType const*>(_varDecl.type().get()))

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.
+	/// Maps a variable to an SSA index.
-	// @param _condition if present, asserts that this condition is true within the branch.
+	using VariableSequenceCounters = std::map<Declaration const*, int>;
-	void visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
+
-	void visitBranch(Statement const& _statement, smt::Expression _condition);
+	/// 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<Declaration const*> _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<Declaration const*> 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<Declaration const*, int>;
-
 	/// 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)

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<SourceLocation>(" <<
+			_repetitions <<
+			", SourceLocation(" <<
+			_loc.start <<
+			", " <<
+			_loc.end <<
+			", make_shared<string>(\"" <<
+			*_loc.sourceName <<
+			"\"))) +" << endl;
+	};
+
+	vector<SourceLocation> 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<SourceLocation> const& _locations)
 {
 	BOOST_CHECK_EQUAL(_items.size(), _locations.size());
 	for (size_t i = 0; i < min(_items.size(), _locations.size()); ++i)
 	{
-		BOOST_CHECK_MESSAGE(
+		if (_items[i].location() != _locations[i])
-			_items[i].location() == _locations[i],
+		{
-			"Location mismatch for assembly item " + to_string(i) + ". Found: " +
+			BOOST_CHECK_MESSAGE(false, "Location mismatch for item " + to_string(i) + ". Found the following locations:");
-					(_items[i].location().sourceName ? *_items[i].location().sourceName + ":" : "(null source name)") +
+			printAssemblyLocations(_items);
-					to_string(_items[i].location().start) + "-" +
+			return;
-					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));
 	}
 }
 
+
 } // end anonymous namespace
 
 BOOST_AUTO_TEST_SUITE(Assembly)

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");
+	CHECK_SUCCESS_NO_WARNINGS(text);
-	// Clear also works on the else branch
+	// 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");
+	CHECK_SUCCESS_NO_WARNINGS(text);
-	// Variable is not cleared, if it is only read.
+	// 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 {