Merge pull request #1 from ethereum/develop

Update

Changelog.md

@@ -9,6 +9,12 @@ Compiler Features:
 
 
 Bugfixes:
+ * Yul / Inline Assembly Parser: Disallow trailing commas in function call arguments.
+
+
+Build System:
+ * Attempt to use stock Z3 cmake files to find Z3 and only fall back to manual discovery.
+ * Generate a cmake error for gcc versions older than 5.0.
 
 
 

cmake/EthCompilerSettings.cmake

@@ -41,11 +41,11 @@ if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MA
 	# Additional GCC-specific compiler settings.
 	if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")
 
-		# Check that we've got GCC 4.7 or newer.
+		# Check that we've got GCC 5.0 or newer.
 		execute_process(
 			COMMAND ${CMAKE_CXX_COMPILER} -dumpversion OUTPUT_VARIABLE GCC_VERSION)
-		if (NOT (GCC_VERSION VERSION_GREATER 4.7 OR GCC_VERSION VERSION_EQUAL 4.7))
+		if (NOT (GCC_VERSION VERSION_GREATER 5.0 OR GCC_VERSION VERSION_EQUAL 5.0))
-			message(FATAL_ERROR "${PROJECT_NAME} requires g++ 4.7 or greater.")
+			message(FATAL_ERROR "${PROJECT_NAME} requires g++ 5.0 or greater.")
 		endif ()
 
 	# Additional Clang-specific compiler settings.

cmake/FindZ3.cmake

@@ -1,29 +1,45 @@
 if (USE_Z3)
-    find_path(Z3_INCLUDE_DIR NAMES z3++.h PATH_SUFFIXES z3)
+    # Save and clear Z3_FIND_VERSION, since the
-    find_library(Z3_LIBRARY NAMES z3)
+    # Z3 config module cannot handle version requirements.
-    find_program(Z3_EXECUTABLE z3 PATH_SUFFIXES bin)
+    set(Z3_FIND_VERSION_ORIG ${Z3_FIND_VERSION})
-
+    set(Z3_FIND_VERSION)
-    if(Z3_INCLUDE_DIR AND Z3_LIBRARY AND Z3_EXECUTABLE)
+    # Try to find Z3 using its stock cmake files.
-        execute_process (COMMAND ${Z3_EXECUTABLE} -version
+    find_package(Z3 QUIET CONFIG)
-            OUTPUT_VARIABLE libz3_version_str
+    # Restore Z3_FIND_VERSION for find_package_handle_standard_args.
-            ERROR_QUIET
+    set(Z3_FIND_VERSION ${Z3_FIND_VERSION_ORIG})
-            OUTPUT_STRIP_TRAILING_WHITESPACE)
+    set(Z3_FIND_VERSION_ORIG)
-
-        string(REGEX REPLACE "^Z3 version ([0-9.]+).*" "\\1"
-               Z3_VERSION_STRING "${libz3_version_str}")
-        unset(libz3_version_str)
-    endif()
-    mark_as_advanced(Z3_VERSION_STRING z3_DIR)
 
     include(FindPackageHandleStandardArgs)
-    find_package_handle_standard_args(Z3
-        REQUIRED_VARS Z3_LIBRARY Z3_INCLUDE_DIR
-        VERSION_VAR Z3_VERSION_STRING)
 
-    if (NOT TARGET Z3::Z3)
+    if (Z3_FOUND)
-        add_library(Z3::Z3 UNKNOWN IMPORTED)
+        set(Z3_VERSION ${Z3_VERSION_STRING})
-        set_property(TARGET Z3::Z3 PROPERTY IMPORTED_LOCATION ${Z3_LIBRARY})
+        find_package_handle_standard_args(Z3 CONFIG_MODE)
-        set_property(TARGET Z3::Z3 PROPERTY INTERFACE_INCLUDE_DIRECTORIES ${Z3_INCLUDE_DIR})
+    else()
+        find_path(Z3_INCLUDE_DIR NAMES z3++.h PATH_SUFFIXES z3)
+        find_library(Z3_LIBRARY NAMES z3)
+        find_program(Z3_EXECUTABLE z3 PATH_SUFFIXES bin)
+
+        if(Z3_INCLUDE_DIR AND Z3_LIBRARY AND Z3_EXECUTABLE)
+            execute_process (COMMAND ${Z3_EXECUTABLE} -version
+                OUTPUT_VARIABLE libz3_version_str
+                ERROR_QUIET
+                OUTPUT_STRIP_TRAILING_WHITESPACE)
+
+            string(REGEX REPLACE "^Z3 version ([0-9.]+).*" "\\1"
+                   Z3_VERSION_STRING "${libz3_version_str}")
+            unset(libz3_version_str)
+        endif()
+        mark_as_advanced(Z3_VERSION_STRING z3_DIR)
+
+        find_package_handle_standard_args(Z3
+            REQUIRED_VARS Z3_LIBRARY Z3_INCLUDE_DIR
+            VERSION_VAR Z3_VERSION_STRING)
+
+        if (NOT TARGET z3::libz3)
+            add_library(z3::libz3 UNKNOWN IMPORTED)
+            set_property(TARGET z3::libz3 PROPERTY IMPORTED_LOCATION ${Z3_LIBRARY})
+            set_property(TARGET z3::libz3 PROPERTY INTERFACE_INCLUDE_DIRECTORIES ${Z3_INCLUDE_DIR})
+        endif()
     endif()
 else()
     set(Z3_FOUND FALSE)

docs/style-guide.rst

@@ -757,20 +757,26 @@ No::
 
     pragma solidity >=0.4.0 <0.7.0;
 
+
     // Base contracts just to make this compile
     contract B {
         constructor(uint) public {
         }
     }
+
+
     contract C {
         constructor(uint, uint) public {
         }
     }
+
+
     contract D {
         constructor(uint) public {
         }
     }
 
+
     contract A is B, C, D {
         uint x;
 
@@ -778,12 +784,12 @@ No::
         B(param1)
         C(param2, param3)
         D(param4)
-        public
+        public {
-        {
             x = param5;
         }
     }
 
+
     contract X is B, C, D {
         uint x;
 
@@ -792,10 +798,11 @@ No::
             C(param2, param3)
             D(param4)
             public {
-            x = param5;
+                x = param5;
-        }
+            }
     }
 
+
 When declaring short functions with a single statement, it is permissible to do it on a single line.
 
 Permissible::
@@ -973,27 +980,32 @@ Yes::
 
     pragma solidity >=0.4.0 <0.7.0;
 
+
     // Owned.sol
     contract Owned {
-         address public owner;
+        address public owner;
 
-         constructor() public {
+        constructor() public {
-             owner = msg.sender;
+            owner = msg.sender;
-         }
+        }
 
-         modifier onlyOwner {
+        modifier onlyOwner {
-             require(msg.sender == owner);
+            require(msg.sender == owner);
-             _;
+            _;
-         }
+        }
 
-         function transferOwnership(address newOwner) public onlyOwner {
+        function transferOwnership(address newOwner) public onlyOwner {
-             owner = newOwner;
+            owner = newOwner;
-         }
+        }
     }
 
-    // Congress.sol
+and in ``Congress.sol``::
+
+    pragma solidity >=0.4.0 <0.7.0;
+
     import "./Owned.sol";
 
+
     contract Congress is Owned, TokenRecipient {
         //...
     }
@@ -1002,32 +1014,34 @@ No::
 
     pragma solidity >=0.4.0 <0.7.0;
 
+
     // owned.sol
     contract owned {
-         address public owner;
+        address public owner;
 
-         constructor() public {
+        constructor() public {
-             owner = msg.sender;
+            owner = msg.sender;
-         }
+        }
 
-         modifier onlyOwner {
+        modifier onlyOwner {
-             require(msg.sender == owner);
+            require(msg.sender == owner);
-             _;
+            _;
-         }
+        }
 
-         function transferOwnership(address newOwner) public onlyOwner {
+        function transferOwnership(address newOwner) public onlyOwner {
-             owner = newOwner;
+            owner = newOwner;
-         }
+        }
     }
 
-    // Congress.sol
+and in ``Congress.sol``::
+
     import "./owned.sol";
 
+
     contract Congress is owned, tokenRecipient {
         //...
     }
 
-
 Struct Names
 ==========================
 
@@ -1104,6 +1118,7 @@ added looks like the one below::
 
     pragma solidity >=0.4.0 <0.7.0;
 
+
     /// @author The Solidity Team
     /// @title A simple storage example
     contract SimpleStorage {
@@ -1126,4 +1141,4 @@ added looks like the one below::
 
 It is recommended that Solidity contracts are fully annontated using `NatSpec <natspec>`_ for all public interfaces (everything in the ABI).
 
-Please see the section about `NatSpec <natspec>`_ for a detailed explanation.
+Please see the section about `NatSpec <natspec>`_ for a detailed explanation.

docs/types/value-types.rst

@@ -625,100 +625,116 @@ Example that shows how to use the members::
 
     pragma solidity >=0.4.16 <0.7.0;
 
+
     contract Example {
-      function f() public payable returns (bytes4) {
+        function f() public payable returns (bytes4) {
-        return this.f.selector;
+            return this.f.selector;
-      }
+        }
-      function g() public {
+
-        this.f.gas(10).value(800)();
+        function g() public {
-      }
+            this.f.gas(10).value(800)();
+        }
     }
 
 Example that shows how to use internal function types::
 
     pragma solidity >=0.4.16 <0.7.0;
 
+
     library ArrayUtils {
-      // internal functions can be used in internal library functions because
+        // internal functions can be used in internal library functions because
-      // they will be part of the same code context
+        // they will be part of the same code context
-      function map(uint[] memory self, function (uint) pure returns (uint) f)
+        function map(uint[] memory self, function (uint) pure returns (uint) f)
-        internal
+            internal
-        pure
+            pure
-        returns (uint[] memory r)
+            returns (uint[] memory r)
-      {
+        {
-        r = new uint[](self.length);
+            r = new uint[](self.length);
-        for (uint i = 0; i < self.length; i++) {
+            for (uint i = 0; i < self.length; i++) {
-          r[i] = f(self[i]);
+                r[i] = f(self[i]);
+            }
         }
-      }
+
-      function reduce(
+        function reduce(
-        uint[] memory self,
+            uint[] memory self,
-        function (uint, uint) pure returns (uint) f
+            function (uint, uint) pure returns (uint) f
-      )
+        )
-        internal
+            internal
-        pure
+            pure
-        returns (uint r)
+            returns (uint r)
-      {
+        {
-        r = self[0];
+            r = self[0];
-        for (uint i = 1; i < self.length; i++) {
+            for (uint i = 1; i < self.length; i++) {
-          r = f(r, self[i]);
+                r = f(r, self[i]);
+            }
         }
-      }
+
-      function range(uint length) internal pure returns (uint[] memory r) {
+        function range(uint length) internal pure returns (uint[] memory r) {
-        r = new uint[](length);
+            r = new uint[](length);
-        for (uint i = 0; i < r.length; i++) {
+            for (uint i = 0; i < r.length; i++) {
-          r[i] = i;
+                r[i] = i;
+            }
         }
-      }
     }
 
+
     contract Pyramid {
-      using ArrayUtils for *;
+        using ArrayUtils for *;
-      function pyramid(uint l) public pure returns (uint) {
+
-        return ArrayUtils.range(l).map(square).reduce(sum);
+        function pyramid(uint l) public pure returns (uint) {
-      }
+            return ArrayUtils.range(l).map(square).reduce(sum);
-      function square(uint x) internal pure returns (uint) {
+        }
-        return x * x;
+
-      }
+        function square(uint x) internal pure returns (uint) {
-      function sum(uint x, uint y) internal pure returns (uint) {
+            return x * x;
-        return x + y;
+        }
-      }
+
+        function sum(uint x, uint y) internal pure returns (uint) {
+            return x + y;
+        }
     }
 
 Another example that uses external function types::
 
     pragma solidity >=0.4.22 <0.7.0;
 
+
     contract Oracle {
-      struct Request {
+        struct Request {
-        bytes data;
+            bytes data;
-        function(uint) external callback;
+            function(uint) external callback;
-      }
+        }
-      Request[] requests;
+
-      event NewRequest(uint);
+        Request[] private requests;
-      function query(bytes memory data, function(uint) external callback) public {
+        event NewRequest(uint);
-        requests.push(Request(data, callback));
+
-        emit NewRequest(requests.length - 1);
+        function query(bytes memory data, function(uint) external callback) public {
-      }
+            requests.push(Request(data, callback));
-      function reply(uint requestID, uint response) public {
+            emit NewRequest(requests.length - 1);
-        // Here goes the check that the reply comes from a trusted source
+        }
-        requests[requestID].callback(response);
+
-      }
+        function reply(uint requestID, uint response) public {
+            // Here goes the check that the reply comes from a trusted source
+            requests[requestID].callback(response);
+        }
     }
 
+
     contract OracleUser {
-      Oracle constant oracle = Oracle(0x1234567); // known contract
+        Oracle constant private ORACLE_CONST = Oracle(0x1234567); // known contract
-      uint exchangeRate;
+        uint private exchangeRate;
-      function buySomething() public {
+
-        oracle.query("USD", this.oracleResponse);
+        function buySomething() public {
-      }
+            ORACLE_CONST.query("USD", this.oracleResponse);
-      function oracleResponse(uint response) public {
+        }
-        require(
+
-            msg.sender == address(oracle),
+        function oracleResponse(uint response) public {
-            "Only oracle can call this."
+            require(
-        );
+                msg.sender == address(ORACLE_CONST),
-        exchangeRate = response;
+                "Only oracle can call this."
-      }
+            );
+            exchangeRate = response;
+        }
     }
 
 .. note::

libsolidity/CMakeLists.txt

@@ -140,7 +140,7 @@ add_library(solidity ${sources} ${z3_SRCS} ${cvc4_SRCS})
 target_link_libraries(solidity PUBLIC yul evmasm langutil devcore ${Boost_FILESYSTEM_LIBRARY} ${Boost_SYSTEM_LIBRARY})
 
 if (${Z3_FOUND})
-  target_link_libraries(solidity PUBLIC Z3::Z3)
+  target_link_libraries(solidity PUBLIC z3::libz3)
 endif()
 
 if (${CVC4_FOUND})

libsolidity/codegen/ir/IRGeneratorForStatements.cpp

@@ -550,13 +550,14 @@ void IRGeneratorForStatements::endVisit(FunctionCall const& _functionCall)
 		solAssert(arguments.size() > 0, "Expected at least one parameter for require/assert");
 		solAssert(arguments.size() <= 2, "Expected no more than two parameters for require/assert");
 
+		Type const* messageArgumentType = arguments.size() > 1 ? arguments[1]->annotation().type : nullptr;
 		string requireOrAssertFunction = m_utils.requireOrAssertFunction(
 			functionType->kind() == FunctionType::Kind::Assert,
-			arguments.size() > 1 ? arguments[1]->annotation().type : nullptr
+			messageArgumentType
 		);
 
 		m_code << move(requireOrAssertFunction) << "(" << m_context.variable(*arguments[0]);
-		if (arguments.size() > 1)
+		if (messageArgumentType && messageArgumentType->sizeOnStack() > 0)
 			m_code << ", " << m_context.variable(*arguments[1]);
 		m_code << ")\n";
 

libsolidity/formal/CVC4Interface.cpp

@@ -132,8 +132,14 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 		else if (n == "false")
 			return m_context.mkConst(false);
 		else
-			// We assume it is an integer...
+			try
-			return m_context.mkConst(CVC4::Rational(n));
+			{
+				return m_context.mkConst(CVC4::Rational(n));
+			}
+			catch (...)
+			{
+				solAssert(false, "");
+			}
 	}
 
 	solAssert(_expr.hasCorrectArity(), "");
@@ -145,6 +151,8 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 		return arguments[0].andExpr(arguments[1]);
 	else if (n == "or")
 		return arguments[0].orExpr(arguments[1]);
+	else if (n == "implies")
+		return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]);
 	else if (n == "=")
 		return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]);
 	else if (n == "<")

libsolidity/formal/SMTChecker.cpp

@@ -34,10 +34,10 @@ using namespace langutil;
 using namespace dev::solidity;
 
 SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
-	m_interface(make_unique<smt::SMTPortfolio>(_smtlib2Responses)),
+	m_interface(_smtlib2Responses),
 	m_errorReporterReference(_errorReporter),
 	m_errorReporter(m_smtErrors),
-	m_context(*m_interface)
+	m_context(m_interface)
 {
 #if defined (HAVE_Z3) || defined (HAVE_CVC4)
 	if (!_smtlib2Responses.empty())
@@ -52,15 +52,18 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _
 
 void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
 {
-	m_scanner = _scanner;
+	if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
-	if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
+		return;
-		_source.accept(*this);
 
-	solAssert(m_interface->solvers() > 0, "");
+	m_scanner = _scanner;
+
+	_source.accept(*this);
+
+	solAssert(m_interface.solvers() > 0, "");
 	// If this check is true, Z3 and CVC4 are not available
 	// and the query answers were not provided, since SMTPortfolio
 	// guarantees that SmtLib2Interface is the first solver.
-	if (!m_interface->unhandledQueries().empty() && m_interface->solvers() == 1)
+	if (!m_interface.unhandledQueries().empty() && m_interface.solvers() == 1)
 	{
 		if (!m_noSolverWarning)
 		{
@@ -106,7 +109,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 	// Not visited by a function call
 	if (m_callStack.empty())
 	{
-		m_interface->reset();
+		m_interface.reset();
 		m_context.reset();
 		m_pathConditions.clear();
 		m_callStack.clear();
@@ -302,13 +305,13 @@ bool SMTChecker::visit(ForStatement const& _node)
 			checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
 	}
 
-	m_interface->push();
+	m_interface.push();
 	if (_node.condition())
-		m_interface->addAssertion(expr(*_node.condition()));
+		m_interface.addAssertion(expr(*_node.condition()));
 	_node.body().accept(*this);
 	if (_node.loopExpression())
 		_node.loopExpression()->accept(*this);
-	m_interface->pop();
+	m_interface.pop();
 
 	auto indicesAfterLoop = copyVariableIndices();
 	// We reset the execution to before the loop
@@ -693,7 +696,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 		solAssert(value, "");
 
 		smt::Expression thisBalance = m_context.balance();
-		setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_interface);
+		setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_interface);
 		checkCondition(thisBalance < expr(*value), _funCall.location(), "Insufficient funds", "address(this).balance", &thisBalance);
 
 		m_context.transfer(m_context.thisAddress(), expr(address), expr(*value));
@@ -737,7 +740,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 	// We set the current value to unknown anyway to add type constraints.
 	m_context.setUnknownValue(*symbolicVar);
 	if (index > 0)
-		m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
+		m_interface.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
 
 void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
@@ -819,7 +822,7 @@ void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
 		smtArguments.push_back(expr(*arg));
 	defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments));
 	m_uninterpretedTerms.insert(&_funCall);
-	setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_interface);
+	setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, m_interface);
 }
 
 void SMTChecker::endVisit(Identifier const& _identifier)
@@ -911,7 +914,7 @@ void SMTChecker::endVisit(Literal const& _literal)
 			auto stringType = TypeProvider::stringMemory();
 			auto stringLit = dynamic_cast<StringLiteralType const*>(_literal.annotation().type);
 			solAssert(stringLit, "");
-			auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface);
+			auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), m_interface);
 			m_context.createExpression(_literal, result.second);
 		}
 		m_errorReporter.warning(
@@ -936,10 +939,10 @@ void SMTChecker::endVisit(Return const& _return)
 			solAssert(components.size() == returnParams.size(), "");
 			for (unsigned i = 0; i < returnParams.size(); ++i)
 				if (components.at(i))
-					m_interface->addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i)));
+					m_interface.addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i)));
 		}
 		else if (returnParams.size() == 1)
-			m_interface->addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
+			m_interface.addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front()));
 	}
 }
 
@@ -981,7 +984,7 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
 		if (_memberAccess.memberName() == "balance")
 		{
 			defineExpr(_memberAccess, m_context.balance(expr(_memberAccess.expression())));
-			setSymbolicUnknownValue(*m_context.expression(_memberAccess), *m_interface);
+			setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_interface);
 			m_uninterpretedTerms.insert(&_memberAccess);
 			return false;
 		}
@@ -1028,7 +1031,7 @@ void SMTChecker::endVisit(IndexAccess const& _indexAccess)
 	setSymbolicUnknownValue(
 		expr(_indexAccess),
 		_indexAccess.annotation().type,
-		*m_interface
+		m_interface
 	);
 	m_uninterpretedTerms.insert(&_indexAccess);
 }
@@ -1080,7 +1083,7 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 			expr(*indexAccess.indexExpression()),
 			_rightHandSide
 		);
-		m_interface->addAssertion(m_context.newValue(*varDecl) == store);
+		m_interface.addAssertion(m_context.newValue(*varDecl) == store);
 		// Update the SMT select value after the assignment,
 		// necessary for sound models.
 		defineExpr(indexAccess, smt::Expression::select(
@@ -1211,7 +1214,7 @@ smt::Expression SMTChecker::arithmeticOperation(
 	if (_op == Token::Div || _op == Token::Mod)
 	{
 		checkCondition(_right == 0, _location, "Division by zero", "<result>", &_right);
-		m_interface->addAssertion(_right != 0);
+		m_interface.addAssertion(_right != 0);
 	}
 
 	addOverflowTarget(
@@ -1393,7 +1396,7 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio
 		addOverflowTarget(OverflowTarget::Type::All, TypeProvider::uint(160), _value, _location);
 	else if (type->category() == Type::Category::Mapping)
 		arrayAssignment();
-	m_interface->addAssertion(m_context.newValue(_variable) == _value);
+	m_interface.addAssertion(m_context.newValue(_variable) == _value);
 }
 
 SMTChecker::VariableIndices SMTChecker::visitBranch(ASTNode const* _statement, smt::Expression _condition)
@@ -1422,7 +1425,7 @@ void SMTChecker::checkCondition(
 	smt::Expression const* _additionalValue
 )
 {
-	m_interface->push();
+	m_interface.push();
 	addPathConjoinedExpression(_condition);
 
 	vector<smt::Expression> expressionsToEvaluate;
@@ -1534,7 +1537,7 @@ void SMTChecker::checkCondition(
 		m_errorReporter.warning(_location, "Error trying to invoke SMT solver.");
 		break;
 	}
-	m_interface->pop();
+	m_interface.pop();
 }
 
 void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string const& _description)
@@ -1543,15 +1546,15 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co
 	if (dynamic_cast<Literal const*>(&_condition))
 		return;
 
-	m_interface->push();
+	m_interface.push();
 	addPathConjoinedExpression(expr(_condition));
 	auto positiveResult = checkSatisfiable();
-	m_interface->pop();
+	m_interface.pop();
 
-	m_interface->push();
+	m_interface.push();
 	addPathConjoinedExpression(!expr(_condition));
 	auto negatedResult = checkSatisfiable();
-	m_interface->pop();
+	m_interface.pop();
 
 	if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
 		m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver.");
@@ -1596,7 +1599,7 @@ SMTChecker::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _exp
 	vector<string> values;
 	try
 	{
-		tie(result, values) = m_interface->check(_expressionsToEvaluate);
+		tie(result, values) = m_interface.check(_expressionsToEvaluate);
 	}
 	catch (smt::SolverError const& _e)
 	{
@@ -1632,7 +1635,7 @@ void SMTChecker::initializeFunctionCallParameters(CallableDeclaration const& _fu
 	for (unsigned i = 0; i < funParams.size(); ++i)
 		if (createVariable(*funParams[i]))
 		{
-			m_interface->addAssertion(_callArgs[i] == m_context.newValue(*funParams[i]));
+			m_interface.addAssertion(_callArgs[i] == m_context.newValue(*funParams[i]));
 			if (funParams[i]->annotation().type->category() == Type::Category::Mapping)
 				m_arrayAssignmentHappened = true;
 		}
@@ -1698,7 +1701,7 @@ void SMTChecker::mergeVariables(set<VariableDeclaration const*> const& _variable
 		int trueIndex = _indicesEndTrue.at(decl);
 		int falseIndex = _indicesEndFalse.at(decl);
 		solAssert(trueIndex != falseIndex, "");
-		m_interface->addAssertion(m_context.newValue(*decl) == smt::Expression::ite(
+		m_interface.addAssertion(m_context.newValue(*decl) == smt::Expression::ite(
 			_condition,
 			valueAtIndex(*decl, trueIndex),
 			valueAtIndex(*decl, falseIndex))
@@ -1758,7 +1761,7 @@ void SMTChecker::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");
-	m_interface->addAssertion(expr(_e) == _value);
+	m_interface.addAssertion(expr(_e) == _value);
 }
 
 void SMTChecker::popPathCondition()
@@ -1807,12 +1810,12 @@ void SMTChecker::pushCallStack(CallStackEntry _entry)
 
 void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e)
 {
-	m_interface->addAssertion(currentPathConditions() && _e);
+	m_interface.addAssertion(currentPathConditions() && _e);
 }
 
 void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
 {
-	m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
+	m_interface.addAssertion(smt::Expression::implies(currentPathConditions(), _e));
 }
 
 bool SMTChecker::isRootFunction()

libsolidity/formal/SMTChecker.h

@@ -19,7 +19,7 @@
 
 
 #include <libsolidity/formal/EncodingContext.h>
-#include <libsolidity/formal/SolverInterface.h>
+#include <libsolidity/formal/SMTPortfolio.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 #include <libsolidity/formal/VariableUsage.h>
 
@@ -53,7 +53,7 @@ public:
 	/// This is used if the SMT solver is not directly linked into this binary.
 	/// @returns a list of inputs to the SMT solver that were not part of the argument to
 	/// the constructor.
-	std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
+	std::vector<std::string> unhandledQueries() { return m_interface.unhandledQueries(); }
 
 	/// @returns the FunctionDefinition of a called function if possible and should inline,
 	/// otherwise nullptr.
@@ -91,6 +91,10 @@ private:
 	void endVisit(IndexAccess const& _node) override;
 	bool visit(InlineAssembly const& _node) override;
 
+	smt::Expression assertions() { return m_interface.assertions(); }
+	void push() { m_interface.push(); }
+	void pop() { m_interface.pop(); }
+
 	/// Do not visit subtree if node is a RationalNumber.
 	/// Symbolic _expr is the rational literal.
 	bool shortcutRationalNumber(Expression const& _expr);
@@ -270,7 +274,7 @@ private:
 	/// @returns the VariableDeclaration referenced by an Identifier or nullptr.
 	VariableDeclaration const* identifierToVariable(Expression const& _expr);
 
-	std::unique_ptr<smt::SolverInterface> m_interface;
+	smt::SMTPortfolio m_interface;
 	smt::VariableUsage m_variableUsage;
 	bool m_loopExecutionHappened = false;
 	bool m_arrayAssignmentHappened = false;

libsolidity/formal/SMTPortfolio.cpp

@@ -43,18 +43,21 @@ SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
 
 void SMTPortfolio::reset()
 {
+	m_assertions.clear();
 	for (auto const& s: m_solvers)
 		s->reset();
 }
 
 void SMTPortfolio::push()
 {
+	m_assertions.push_back(Expression(true));
 	for (auto const& s: m_solvers)
 		s->push();
 }
 
 void SMTPortfolio::pop()
 {
+	m_assertions.pop_back();
 	for (auto const& s: m_solvers)
 		s->pop();
 }
@@ -67,10 +70,23 @@ void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort)
 
 void SMTPortfolio::addAssertion(Expression const& _expr)
 {
+	if (m_assertions.empty())
+		m_assertions.push_back(_expr);
+	else
+		m_assertions.back() = _expr && move(m_assertions.back());
+
 	for (auto const& s: m_solvers)
 		s->addAssertion(_expr);
 }
 
+Expression SMTPortfolio::assertions()
+{
+	if (m_assertions.empty())
+		return Expression(true);
+
+	return m_assertions.back();
+}
+
 /*
  * Broadcasts the SMT query to all solvers and returns a single result.
  * This comment explains how this result is decided.

libsolidity/formal/SMTPortfolio.h

@@ -52,6 +52,9 @@ public:
 	void declareVariable(std::string const&, Sort const&) override;
 
 	void addAssertion(Expression const& _expr) override;
+
+	Expression assertions();
+
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
 
 	std::vector<std::string> unhandledQueries() override;
@@ -60,6 +63,8 @@ private:
 	static bool solverAnswered(CheckResult result);
 
 	std::vector<std::unique_ptr<smt::SolverInterface>> m_solvers;
+
+	std::vector<Expression> m_assertions;
 };
 
 }

libsolidity/formal/SolverInterface.h

@@ -133,6 +133,7 @@ public:
 			{"not", 1},
 			{"and", 2},
 			{"or", 2},
+			{"implies", 2},
 			{"=", 2},
 			{"<", 2},
 			{"<=", 2},
@@ -160,7 +161,12 @@ public:
 
 	static Expression implies(Expression _a, Expression _b)
 	{
-		return !std::move(_a) || std::move(_b);
+		return Expression(
+			"implies",
+			std::move(_a),
+			std::move(_b),
+			Kind::Bool
+		);
 	}
 
 	/// select is the SMT representation of an array index access.

libsolidity/formal/Z3Interface.cpp

@@ -131,8 +131,14 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 		else if (n == "false")
 			return m_context.bool_val(false);
 		else
-			// We assume it is an integer...
+			try
-			return m_context.int_val(n.c_str());
+			{
+				return m_context.int_val(n.c_str());
+			}
+			catch (...)
+			{
+				solAssert(false, "");
+			}
 	}
 
 	solAssert(_expr.hasCorrectArity(), "");
@@ -144,6 +150,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 		return arguments[0] && arguments[1];
 	else if (n == "or")
 		return arguments[0] || arguments[1];
+	else if (n == "implies")
+		return z3::implies(arguments[0], arguments[1]);
 	else if (n == "=")
 		return arguments[0] == arguments[1];
 	else if (n == "<")

libyul/AsmParser.cpp

@@ -609,12 +609,14 @@ Expression Parser::parseCall(Parser::ElementaryOperation&& _initialOp)
 		else
 			ret = std::move(boost::get<FunctionCall>(_initialOp));
 		expectToken(Token::LParen);
-		while (currentToken() != Token::RParen)
+		if (currentToken() != Token::RParen)
 		{
 			ret.arguments.emplace_back(parseExpression());
-			if (currentToken() == Token::RParen)
+			while (currentToken() != Token::RParen)
-				break;
+			{
-			expectToken(Token::Comma);
+				expectToken(Token::Comma);
+				ret.arguments.emplace_back(parseExpression());
+			}
 		}
 		ret.location.end = endPosition();
 		expectToken(Token::RParen);

libyul/AsmPrinter.cpp

@@ -266,7 +266,7 @@ string AsmPrinter::formatTypedName(TypedName _variable) const
 
 string AsmPrinter::appendTypeName(YulString _type) const
 {
-	if (m_yul)
+	if (m_yul && !_type.empty())
 		return ":" + _type.str();
 	return "";
 }

test/libsolidity/SemanticTest.cpp

@@ -46,8 +46,18 @@ SemanticTest::SemanticTest(string const& _filename, string const& _ipcPath, lang
 	m_source = parseSourceAndSettings(file);
 	if (m_settings.count("compileViaYul"))
 	{
-		m_validatedSettings["compileViaYul"] = m_settings["compileViaYul"];
+		if (m_settings["compileViaYul"] == "also")
-		m_compileViaYul = true;
+		{
+			m_validatedSettings["compileViaYul"] = m_settings["compileViaYul"];
+			m_runWithYul = true;
+			m_runWithoutYul = true;
+		}
+		else
+		{
+			m_validatedSettings["compileViaYul"] = "only";
+			m_runWithYul = true;
+			m_runWithoutYul = false;
+		}
 		m_settings.erase("compileViaYul");
 	}
 	parseExpectations(file);
@@ -55,68 +65,84 @@ SemanticTest::SemanticTest(string const& _filename, string const& _ipcPath, lang
 
 TestCase::TestResult SemanticTest::run(ostream& _stream, string const& _linePrefix, bool _formatted)
 {
-
+	for(bool compileViaYul: set<bool>{!m_runWithoutYul, m_runWithYul})
-
-	bool success = true;
-	for (auto& test: m_tests)
-		test.reset();
-
-	for (auto& test: m_tests)
 	{
-		if (&test == &m_tests.front())
+		bool success = true;
-			if (test.call().isConstructor)
+
-				deploy("", 0, test.call().arguments.rawBytes());
+		m_compileViaYul = compileViaYul;
+		if (compileViaYul)
+			AnsiColorized(_stream, _formatted, {BOLD, CYAN}) << _linePrefix << "Running via Yul:" << endl;
+
+		for (auto& test: m_tests)
+			test.reset();
+
+		for (auto& test: m_tests)
+		{
+			if (&test == &m_tests.front())
+				if (test.call().isConstructor)
+					deploy("", 0, test.call().arguments.rawBytes());
+				else
+					soltestAssert(deploy("", 0, bytes()), "Failed to deploy contract.");
 			else
-				soltestAssert(deploy("", 0, bytes()), "Failed to deploy contract.");
+				soltestAssert(!test.call().isConstructor, "Constructor has to be the first function call.");
-		else
-			soltestAssert(!test.call().isConstructor, "Constructor has to be the first function call.");
 
-		if (test.call().isConstructor)
+			if (test.call().isConstructor)
-		{
+			{
-			if (m_transactionSuccessful == test.call().expectations.failure)
+				if (m_transactionSuccessful == test.call().expectations.failure)
-				success = false;
+					success = false;
 
-			test.setFailure(!m_transactionSuccessful);
+				test.setFailure(!m_transactionSuccessful);
-			test.setRawBytes(bytes());
+				test.setRawBytes(bytes());
+			}
+			else
+			{
+				bytes output = callContractFunctionWithValueNoEncoding(
+					test.call().signature,
+					test.call().value,
+					test.call().arguments.rawBytes()
+				);
+
+				if ((m_transactionSuccessful == test.call().expectations.failure) || (output != test.call().expectations.rawBytes()))
+					success = false;
+
+				test.setFailure(!m_transactionSuccessful);
+				test.setRawBytes(std::move(output));
+				test.setContractABI(m_compiler.contractABI(m_compiler.lastContractName()));
+			}
 		}
-		else
+
+		if (!success)
 		{
-			bytes output = callContractFunctionWithValueNoEncoding(
+			AnsiColorized(_stream, _formatted, {BOLD, CYAN}) << _linePrefix << "Expected result:" << endl;
-				test.call().signature,
+			for (auto const& test: m_tests)
-				test.call().value,
+			{
-				test.call().arguments.rawBytes()
+				ErrorReporter errorReporter;
-			);
+				_stream << test.format(errorReporter, _linePrefix, false, _formatted) << endl;
-
+				_stream << errorReporter.format(_linePrefix, _formatted);
-			if ((m_transactionSuccessful == test.call().expectations.failure) || (output != test.call().expectations.rawBytes()))
+			}
-				success = false;
+			_stream << endl;
-
+			AnsiColorized(_stream, _formatted, {BOLD, CYAN}) << _linePrefix << "Obtained result:" << endl;
-			test.setFailure(!m_transactionSuccessful);
+			for (auto const& test: m_tests)
-			test.setRawBytes(std::move(output));
+			{
-			test.setContractABI(m_compiler.contractABI(m_compiler.lastContractName()));
+				ErrorReporter errorReporter;
+				_stream << test.format(errorReporter, _linePrefix, true, _formatted) << endl;
+				_stream << errorReporter.format(_linePrefix, _formatted);
+			}
+			AnsiColorized(_stream, _formatted, {BOLD, RED}) << _linePrefix << endl << _linePrefix
+				<< "Attention: Updates on the test will apply the detected format displayed." << endl;
+			if (compileViaYul && m_runWithoutYul)
+			{
+				_stream << _linePrefix << endl << _linePrefix;
+				AnsiColorized(_stream, _formatted, {RED_BACKGROUND}) << "Note that the test passed without Yul.";
+				_stream << endl;
+			}
+			else if (!compileViaYul && m_runWithYul)
+				AnsiColorized(_stream, _formatted, {BOLD, YELLOW}) << _linePrefix << endl << _linePrefix
+					<< "Note that the test also has to pass via Yul." << endl;
+			return TestResult::Failure;
 		}
 	}
 
-	if (!success)
-	{
-		AnsiColorized(_stream, _formatted, {BOLD, CYAN}) << _linePrefix << "Expected result:" << endl;
-		for (auto const& test: m_tests)
-		{
-			ErrorReporter errorReporter;
-			_stream << test.format(errorReporter, _linePrefix, false, _formatted) << endl;
-			_stream << errorReporter.format(_linePrefix, _formatted);
-		}
-		_stream << endl;
-		AnsiColorized(_stream, _formatted, {BOLD, CYAN}) << _linePrefix << "Obtained result:" << endl;
-		for (auto const& test: m_tests)
-		{
-			ErrorReporter errorReporter;
-			_stream << test.format(errorReporter, _linePrefix, true, _formatted) << endl;
-			_stream << errorReporter.format(_linePrefix, _formatted);
-		}
-		AnsiColorized(_stream, _formatted, {BOLD, RED}) << _linePrefix << endl << _linePrefix
-			<< "Attention: Updates on the test will apply the detected format displayed." << endl;
-		return TestResult::Failure;
-	}
 	return TestResult::Success;
 }
 

test/libsolidity/SemanticTest.h

@@ -65,6 +65,8 @@ public:
 private:
 	std::string m_source;
 	std::vector<TestFunctionCall> m_tests;
+	bool m_runWithYul = false;
+	bool m_runWithoutYul = true;
 };
 
 }

test/libsolidity/smtCheckerTestsJSON/multi.json

@@ -3,8 +3,8 @@
 	{
 		"smtlib2responses":
 		{
-			"0x092d52dc5c2b54c1909592f7b3c8efedfd87afc0223ce421a24a1cc7905006b4": "sat\n((|EVALEXPR_0| 1))\n",
+			"0x0a0e9583fd983e7ce82e96bd95f7c0eb831e2dd3ce3364035e30bf1d22823b34": "sat\n((|EVALEXPR_0| 1))\n",
-			"0x8faacfc008b6f2278b5927ff22d76832956dfb46b3c21a64fab96583c241b88f": "unsat\n",
+			"0x15353582486fb1dac47801edbb366ae40a59ef0191ebe7c09ca32bdabecc2f1a": "unsat\n",
 			"0xa66d08de30c873ca7d0e7e9e426f278640e0ee463a1aed2e4e80baee916b6869": "sat\n((|EVALEXPR_0| 0))\n"
 		}
 	}

test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_beginning.sol

@@ -3,10 +3,9 @@ contract C {
     assembly {
       function f(a, b) {}
       f()
-      f(1,)
       f(,1)
     }
   }
 }
 // ----
-// ParserError: (113-114): Literal, identifier or instruction expected.
+// ParserError: (101-102): Literal, identifier or instruction expected.

test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_end.sol

@@ -0,0 +1,11 @@
+contract C {
+  function f() public pure {
+    assembly {
+      function f(a, b) {}
+      f()
+      f(1,)
+    }
+  }
+}
+// ----
+// ParserError: (103-104): Literal, identifier or instruction expected.

test/libsolidity/syntaxTests/inlineAssembly/invalid/empty_fun_arg_middle.sol

@@ -0,0 +1,10 @@
+contract C {
+  function f() public pure {
+    assembly {
+      function f(a, b, c) {}
+      f(1,,1)
+    }
+  }
+}
+// ----
+// ParserError: (96-97): Literal, identifier or instruction expected.