Merge pull request #5388 from ethereum/smt_mapping

[SMTChecker] Support for mapping

7 files changed, 178 insertions, 16 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index dc14f4c2..bfbd6caf 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -60,8 +60,7 @@ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _
 bool SMTChecker::visit(ContractDefinition const& _contract)
 {
 	for (auto _var : _contract.stateVariables())
-		if (_var->type()->isValueType())
-			createVariable(*_var);
+		createVariable(*_var);
 	return true;
 }
 
@@ -94,9 +93,10 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 		m_uninterpretedTerms.clear();
 		resetStateVariables();
 		initializeLocalVariables(_function);
+		m_loopExecutionHappened = false;
+		m_arrayAssignmentHappened = false;
 	}
 
-	m_loopExecutionHappened = false;
 	return true;
 }
 
@@ -271,6 +271,11 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 		assignment(decl, _assignment.rightHandSide(), _assignment.location());
 		defineExpr(_assignment, expr(_assignment.rightHandSide()));
 	}
+	else if (dynamic_cast<IndexAccess const*>(&_assignment.leftHandSide()))
+	{
+		arrayIndexAssignment(_assignment);
+		defineExpr(_assignment, expr(_assignment.rightHandSide()));
+	}
 	else
 		m_errorReporter.warning(
 			_assignment.location(),
@@ -459,6 +464,13 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 		m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
 
+void SMTChecker::eraseArrayKnowledge()
+{
+	for (auto const& var: m_variables)
+		if (var.first->annotation().type->category() == Type::Category::Mapping)
+			newValue(*var.first);
+}
+
 void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 {
 	FunctionDefinition const* _funDef = nullptr;
@@ -532,7 +544,7 @@ void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
 	for (auto const& arg: _funCall.arguments())
 		smtArguments.push_back(expr(*arg));
 	defineExpr(_funCall, (*m_expressions.at(&_funCall.expression()))(smtArguments));
-	m_uninterpretedTerms.push_back(&_funCall);
+	m_uninterpretedTerms.insert(&_funCall);
 	setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_interface);
 }
 
@@ -638,6 +650,74 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
 	return true;
 }
 
+void SMTChecker::endVisit(IndexAccess const& _indexAccess)
+{
+	shared_ptr<SymbolicVariable> array;
+	if (auto const& id = dynamic_cast<Identifier const*>(&_indexAccess.baseExpression()))
+	{
+		auto const& varDecl = dynamic_cast<VariableDeclaration const&>(*id->annotation().referencedDeclaration);
+		solAssert(knownVariable(varDecl), "");
+		array = m_variables[&varDecl];
+	}
+	else if (auto const& innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
+	{
+		solAssert(knownExpr(*innerAccess), "");
+		array = m_expressions[innerAccess];
+	}
+	else
+	{
+		m_errorReporter.warning(
+			_indexAccess.location(),
+			"Assertion checker does not yet implement this expression."
+		);
+		return;
+	}
+
+	solAssert(array, "");
+	defineExpr(_indexAccess, smt::Expression::select(
+		array->currentValue(),
+		expr(*_indexAccess.indexExpression())
+	));
+	setSymbolicUnknownValue(
+		expr(_indexAccess),
+		_indexAccess.annotation().type,
+		*m_interface
+	);
+	m_uninterpretedTerms.insert(&_indexAccess);
+}
+
+void SMTChecker::arrayAssignment()
+{
+	m_arrayAssignmentHappened = true;
+	eraseArrayKnowledge();
+}
+
+void SMTChecker::arrayIndexAssignment(Assignment const& _assignment)
+{
+	auto const& indexAccess = dynamic_cast<IndexAccess const&>(_assignment.leftHandSide());
+	if (auto const& id = dynamic_cast<Identifier const*>(&indexAccess.baseExpression()))
+	{
+		auto const& varDecl = dynamic_cast<VariableDeclaration const&>(*id->annotation().referencedDeclaration);
+		solAssert(knownVariable(varDecl), "");
+		smt::Expression store = smt::Expression::store(
+			m_variables[&varDecl]->currentValue(),
+			expr(*indexAccess.indexExpression()),
+			expr(_assignment.rightHandSide())
+		);
+		m_interface->addAssertion(newValue(varDecl) == store);
+	}
+	else if (dynamic_cast<IndexAccess const*>(&indexAccess.baseExpression()))
+		m_errorReporter.warning(
+			indexAccess.location(),
+			"Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays."
+		);
+	else
+		m_errorReporter.warning(
+			_assignment.location(),
+			"Assertion checker does not yet implement this expression."
+		);
+}
+
 void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
 {
 	if (!knownGlobalSymbol(_name))
@@ -803,6 +883,8 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio
 		checkUnderOverflow(_value, *intType, _location);
 	else if (dynamic_cast<AddressType const*>(type.get()))
 		checkUnderOverflow(_value, IntegerType(160), _location);
+	else if (dynamic_cast<MappingType const*>(type.get()))
+		arrayAssignment();
 	m_interface->addAssertion(newValue(_variable) == _value);
 }
 
@@ -847,12 +929,19 @@ void SMTChecker::checkCondition(
 		}
 		for (auto const& var: m_variables)
 		{
-			expressionsToEvaluate.emplace_back(currentValue(*var.first));
-			expressionNames.push_back(var.first->name());
+			if (var.first->type()->isValueType())
+			{
+				expressionsToEvaluate.emplace_back(currentValue(*var.first));
+				expressionNames.push_back(var.first->name());
+			}
 		}
 		for (auto const& var: m_globalContext)
 		{
-			if (smtKind(var.second->type()->category()) != smt::Kind::Function)
+			auto const& type = var.second->type();
+			if (
+				type->isValueType() &&
+				smtKind(type->category()) != smt::Kind::Function
+			)
 			{
 				expressionsToEvaluate.emplace_back(var.second->currentValue());
 				expressionNames.push_back(var.first);
@@ -860,8 +949,11 @@ void SMTChecker::checkCondition(
 		}
 		for (auto const& uf: m_uninterpretedTerms)
 		{
-			expressionsToEvaluate.emplace_back(expr(*uf));
-			expressionNames.push_back(m_scanner->sourceAt(uf->location()));
+			if (uf->annotation().type->isValueType())
+			{
+				expressionsToEvaluate.emplace_back(expr(*uf));
+				expressionNames.push_back(m_scanner->sourceAt(uf->location()));
+			}
 		}
 	}
 	smt::CheckResult result;
@@ -873,6 +965,12 @@ void SMTChecker::checkCondition(
 		loopComment =
 			"\nNote that some information is erased after the execution of loops.\n"
 			"You can re-introduce information using require().";
+	if (m_arrayAssignmentHappened)
+		loopComment +=
+			"\nNote that array aliasing is not supported,"
+			" therefore all mapping information is erased after"
+			" a mapping local variable/parameter is assigned.\n"
+			"You can re-introduce information using require().";
 
 	switch (result)
 	{
@@ -1006,7 +1104,11 @@ void SMTChecker::initializeFunctionCallParameters(FunctionDefinition const& _fun
 	solAssert(funParams.size() == _callArgs.size(), "");
 	for (unsigned i = 0; i < funParams.size(); ++i)
 		if (createVariable(*funParams[i]))
+		{
 			m_interface->addAssertion(_callArgs[i] == newValue(*funParams[i]));
+			if (funParams[i]->annotation().type->category() == Type::Category::Mapping)
+				m_arrayAssignmentHappened = true;
+		}
 
 	for (auto const& variable: _function.localVariables())
 		if (createVariable(*variable))
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 9f8c04ab..c749cbc3 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -79,6 +79,7 @@ private:
 	void endVisit(Literal const& _node) override;
 	void endVisit(Return const& _node) override;
 	bool visit(MemberAccess const& _node) override;
+	void endVisit(IndexAccess const& _node) override;
 
 	void arithmeticOperation(BinaryOperation const& _op);
 	void compareOperation(BinaryOperation const& _op);
@@ -96,6 +97,14 @@ private:
 
 	void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
 	void defineGlobalFunction(std::string const& _name, Expression const& _expr);
+	/// Handles the side effects of assignment
+	/// to variable of some SMT array type
+	/// while aliasing is not supported.
+	void arrayAssignment();
+	/// Handles assignment to SMT array index.
+	void arrayIndexAssignment(Assignment const& _assignment);
+	/// Erases information about SMT arrays.
+	void eraseArrayKnowledge();
 
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
@@ -203,14 +212,16 @@ private:
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::shared_ptr<VariableUsage> m_variableUsage;
 	bool m_loopExecutionHappened = false;
+	bool m_arrayAssignmentHappened = false;
 	/// An Expression may have multiple smt::Expression due to
 	/// repeated calls to the same function.
 	std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
 	std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
 	std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_globalContext;
 	/// Stores the instances of an Uninterpreted Function applied to arguments.
+	/// These may be direct application of UFs or Array index access.
 	/// Used to retrieve models.
-	std::vector<Expression const*> m_uninterpretedTerms;
+	std::set<Expression const*> m_uninterpretedTerms;
 	std::vector<smt::Expression> m_pathConditions;
 	langutil::ErrorReporter& m_errorReporter;
 	std::shared_ptr<langutil::Scanner> m_scanner;
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 4a4b3fb1..03920dd6 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -80,6 +80,8 @@ struct FunctionSort: public Sort
 			[&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
 		))
 			return false;
+		solAssert(codomain, "");
+		solAssert(_otherFunction->codomain, "");
 		return *codomain == *_otherFunction->codomain;
 	}
 
@@ -99,6 +101,10 @@ struct ArraySort: public Sort
 			return false;
 		auto _otherArray = dynamic_cast<ArraySort const*>(&_other);
 		solAssert(_otherArray, "");
+		solAssert(_otherArray->domain, "");
+		solAssert(_otherArray->range, "");
+		solAssert(domain, "");
+		solAssert(range, "");
 		return *domain == *_otherArray->domain && *range == *_otherArray->range;
 	}
 
@@ -161,8 +167,9 @@ public:
 	static Expression select(Expression _array, Expression _index)
 	{
 		solAssert(_array.sort->kind == Kind::Array, "");
-		auto const& arraySort = dynamic_cast<ArraySort const*>(_array.sort.get());
+		std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
 		solAssert(arraySort, "");
+		solAssert(_index.sort, "");
 		solAssert(*arraySort->domain == *_index.sort, "");
 		return Expression(
 			"select",
@@ -176,14 +183,16 @@ public:
 	static Expression store(Expression _array, Expression _index, Expression _element)
 	{
 		solAssert(_array.sort->kind == Kind::Array, "");
-		auto const& arraySort = dynamic_cast<ArraySort const*>(_array.sort.get());
+		std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
 		solAssert(arraySort, "");
+		solAssert(_index.sort, "");
+		solAssert(_element.sort, "");
 		solAssert(*arraySort->domain == *_index.sort, "");
 		solAssert(*arraySort->range == *_element.sort, "");
 		return Expression(
 			"store",
 			std::vector<Expression>{std::move(_array), std::move(_index), std::move(_element)},
-			_array.sort
+			arraySort
 		);
 	}
 
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 3cfaa271..583f7b09 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -52,13 +52,19 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type)
 	}
 	case smt::Kind::Array:
 	{
-		solUnimplementedAssert(false, "Invalid type");
+		if (isMapping(_type.category()))
+		{
+			auto mapType = dynamic_cast<MappingType const*>(&_type);
+			solAssert(mapType, "");
+			return make_shared<smt::ArraySort>(smtSort(*mapType->keyType()), smtSort(*mapType->valueType()));
+		}
+		// TODO Solidity array
+		return make_shared<smt::Sort>(smt::Kind::Int);
 	}
 	default:
 		// Abstract case.
 		return make_shared<smt::Sort>(smt::Kind::Int);
 	}
-	solAssert(false, "Invalid type");
 }
 
 vector<smt::SortPointer> dev::solidity::smtSort(vector<TypePointer> const& _types)
@@ -77,6 +83,8 @@ smt::Kind dev::solidity::smtKind(Type::Category _category)
 		return smt::Kind::Bool;
 	else if (isFunction(_category))
 		return smt::Kind::Function;
+	else if (isMapping(_category))
+		return smt::Kind::Array;
 	// Abstract case.
 	return smt::Kind::Int;
 }
@@ -84,7 +92,8 @@ smt::Kind dev::solidity::smtKind(Type::Category _category)
 bool dev::solidity::isSupportedType(Type::Category _category)
 {
 	return isNumber(_category) ||
-		isBool(_category);
+		isBool(_category) ||
+		isMapping(_category);
 }
 
 bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category)
@@ -130,6 +139,8 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
 		else
 			var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
 	}
+	else if (isMapping(_type.category()))
+		var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _solver);
 	else
 		solAssert(false, "");
 	return make_pair(abstract, var);
@@ -183,6 +194,11 @@ bool dev::solidity::isFunction(Type::Category _category)
 	return _category == Type::Category::Function;
 }
 
+bool dev::solidity::isMapping(Type::Category _category)
+{
+	return _category == Type::Category::Mapping;
+}
+
 smt::Expression dev::solidity::minValue(IntegerType const& _type)
 {
 	return smt::Expression(_type.minValue());
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 2c568f5b..66552b27 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -48,6 +48,7 @@ bool isAddress(Type::Category _category);
 bool isNumber(Type::Category _category);
 bool isBool(Type::Category _category);
 bool isFunction(Type::Category _category);
+bool isMapping(Type::Category _category);
 
 /// Returns a new symbolic variable, according to _type.
 /// Also returns whether the type is abstract or not,
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index 997635af..f7eeb3bd 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -127,3 +127,13 @@ smt::Expression SymbolicFunctionVariable::operator()(vector<smt::Expression> _ar
 {
 	return m_declaration(_arguments);
 }
+
+SymbolicMappingVariable::SymbolicMappingVariable(
+	TypePointer _type,
+	string const& _uniqueName,
+	smt::SolverInterface& _interface
+):
+	SymbolicVariable(move(_type), _uniqueName, _interface)
+{
+	solAssert(isMapping(m_type->category()), "");
+}
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index 6754ee07..f7a65a4e 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -143,5 +143,18 @@ private:
 	smt::Expression m_declaration;
 };
 
+/**
+ * Specialization of SymbolicVariable for Mapping
+ */
+class SymbolicMappingVariable: public SymbolicVariable
+{
+public:
+	SymbolicMappingVariable(
+		TypePointer _type,
+		std::string const& _uniqueName,
+		smt::SolverInterface& _interface
+	);
+};
+
 }
 }