Merge pull request #7745 from ethereum/develop

Merge develop into develop_060

libsolidity/formal/SMTEncoder.cpp

@@ -209,17 +209,14 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
 			solAssert(symbTuple, "");
 			auto const& components = symbTuple->components();
 			auto const& declarations = _varDecl.declarations();
-			if (!components.empty())
-			{
-				solAssert(components.size() == declarations.size(), "");
-				for (unsigned i = 0; i < declarations.size(); ++i)
-					if (
-						components.at(i) &&
-						declarations.at(i) &&
-						m_context.knownVariable(*declarations.at(i))
-					)
-						assignment(*declarations.at(i), components.at(i)->currentValue(declarations.at(i)->type()));
-			}
+			solAssert(components.size() == declarations.size(), "");
+			for (unsigned i = 0; i < declarations.size(); ++i)
+				if (
+					components.at(i) &&
+					declarations.at(i) &&
+					m_context.knownVariable(*declarations.at(i))
+				)
+					assignment(*declarations.at(i), components.at(i)->currentValue(declarations.at(i)->type()));
 		}
 	}
 	else if (m_context.knownVariable(*_varDecl.declarations().front()))
@@ -321,24 +318,23 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 	{
 		auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_tuple));
 		solAssert(symbTuple, "");
-		if (symbTuple->components().empty())
+		auto const& symbComponents = symbTuple->components();
+		auto const& tupleComponents = _tuple.components();
+		solAssert(symbComponents.size() == _tuple.components().size(), "");
+		for (unsigned i = 0; i < symbComponents.size(); ++i)
 		{
-			vector<shared_ptr<smt::SymbolicVariable>> components;
-			for (auto const& component: _tuple.components())
-				if (component)
-				{
-					if (auto varDecl = identifierToVariable(*component))
-						components.push_back(m_context.variable(*varDecl));
-					else
-					{
-						solAssert(m_context.knownExpression(*component), "");
-						components.push_back(m_context.expression(*component));
-					}
-				}
+			auto sComponent = symbComponents.at(i);
+			auto tComponent = tupleComponents.at(i);
+			if (sComponent && tComponent)
+			{
+				if (auto varDecl = identifierToVariable(*tComponent))
+					m_context.addAssertion(sComponent->currentValue() == currentValue(*varDecl));
 				else
-					components.push_back(nullptr);
-			solAssert(components.size() == _tuple.components().size(), "");
-			symbTuple->setComponents(move(components));
+				{
+					solAssert(m_context.knownExpression(*tComponent), "");
+					m_context.addAssertion(sComponent->currentValue() == expr(*tComponent));
+				}
+			}
 		}
 	}
 	else
@@ -610,12 +606,22 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
 		defineExpr(_identifier, m_context.thisAddress());
 		m_uninterpretedTerms.insert(&_identifier);
 	}
-	else if (smt::isSupportedType(_identifier.annotation().type->category()))
-		// TODO: handle MagicVariableDeclaration here
-		m_errorReporter.warning(
-			_identifier.location(),
-			"Assertion checker does not yet support the type of this variable."
-		);
+	else if (
+		_identifier.annotation().type->category() != Type::Category::Modifier
+	)
+		createExpr(_identifier);
+}
+
+void SMTEncoder::endVisit(ElementaryTypeNameExpression const& _typeName)
+{
+	auto const& typeType = dynamic_cast<TypeType const&>(*_typeName.annotation().type);
+	auto result = smt::newSymbolicVariable(
+		*TypeProvider::uint256(),
+		typeType.actualType()->toString(false),
+		m_context
+	);
+	solAssert(!result.first && result.second, "");
+	m_context.createExpression(_typeName, result.second);
 }
 
 void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
@@ -1513,15 +1519,18 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
 	{
 		auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
 		solAssert(symbTuple, "");
-		if (symbTuple->components().empty())
+		auto const& symbComponents = symbTuple->components();
+		solAssert(symbComponents.size() == returnParams.size(), "");
+		for (unsigned i = 0; i < symbComponents.size(); ++i)
 		{
-			vector<shared_ptr<smt::SymbolicVariable>> components;
-			for (auto param: returnParams)
+			auto sComponent = symbComponents.at(i);
+			auto param = returnParams.at(i);
+			solAssert(param, "");
+			if (sComponent)
 			{
 				solAssert(m_context.knownVariable(*param), "");
-				components.push_back(m_context.variable(*param));
+				m_context.addAssertion(sComponent->currentValue() == currentValue(*param));
 			}
-			symbTuple->setComponents(move(components));
 		}
 	}
 	else if (returnParams.size() == 1)

libsolidity/formal/SMTEncoder.h

@@ -27,6 +27,7 @@
 #include <libsolidity/formal/SymbolicVariables.h>
 #include <libsolidity/formal/VariableUsage.h>
 
+#include <libsolidity/ast/AST.h>
 #include <libsolidity/ast/ASTVisitor.h>
 #include <libsolidity/interface/ReadFile.h>
 #include <liblangutil/ErrorReporter.h>
@@ -82,6 +83,7 @@ protected:
 	void endVisit(BinaryOperation const& _node) override;
 	void endVisit(FunctionCall const& _node) override;
 	void endVisit(Identifier const& _node) override;
+	void endVisit(ElementaryTypeNameExpression const& _node) override;
 	void endVisit(Literal const& _node) override;
 	void endVisit(Return const& _node) override;
 	bool visit(MemberAccess const& _node) override;

libsolidity/formal/SymbolicVariables.cpp

@@ -248,12 +248,16 @@ SymbolicTupleVariable::SymbolicTupleVariable(
 	SymbolicVariable(_type, _type, move(_uniqueName), _context)
 {
 	solAssert(isTuple(m_type->category()), "");
-}
-
-void SymbolicTupleVariable::setComponents(vector<shared_ptr<SymbolicVariable>> _components)
-{
-	solAssert(m_components.empty(), "");
-	auto const& tupleType = dynamic_cast<solidity::TupleType const*>(m_type);
-	solAssert(_components.size() == tupleType->components().size(), "");
-	m_components = move(_components);
+	auto const& tupleType = dynamic_cast<TupleType const&>(*m_type);
+	auto const& componentsTypes = tupleType.components();
+	for (unsigned i = 0; i < componentsTypes.size(); ++i)
+		if (componentsTypes.at(i))
+		{
+			string componentName = m_uniqueName + "_component_" + to_string(i);
+			auto result = smt::newSymbolicVariable(*componentsTypes.at(i), componentName, m_context);
+			solAssert(result.second, "");
+			m_components.emplace_back(move(result.second));
+		}
+		else
+			m_components.emplace_back(nullptr);
 }

libsolidity/formal/SymbolicVariables.h

@@ -250,8 +250,6 @@ public:
 		return m_components;
 	}
 
-	void setComponents(std::vector<std::shared_ptr<SymbolicVariable>> _components);
-
 private:
 	std::vector<std::shared_ptr<SymbolicVariable>> m_components;
 };