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

8 files changed, 144 insertions, 36 deletions

diff --git a/Changelog.md b/Changelog.md
index 13c8118f..bfaeeb27 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.
diff --git a/docs/grammar.txt b/docs/grammar.txt
index ce3fd3ad..e700c946 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'
 
diff --git a/docs/julia.rst b/docs/julia.rst
index 309e6b36..9e961a9d 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.
 
diff --git a/libsolidity/codegen/CompilerContext.cpp b/libsolidity/codegen/CompilerContext.cpp
index ce9c3b7f..ab10d7dd 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(
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index a8529795..a64024b3 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<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()))
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index d4c2cf6f..b57f0f96 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<Declaration const*, int>;
+
+	/// 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)
diff --git a/test/libsolidity/Assembly.cpp b/test/libsolidity/Assembly.cpp
index 358d3c72..59af6d41 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<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(
-			_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)
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index 3a65aa43..2a1609cc 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 {