[SMTChecker] Use SymbolicFunctionVariable for uninterpreted functions

4 files changed, 133 insertions, 85 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 17dc11ac..dc14f4c2 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -90,8 +90,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 		m_interface->reset();
 		m_pathConditions.clear();
 		m_expressions.clear();
-		m_specialVariables.clear();
-		m_uninterpretedFunctions.clear();
+		m_globalContext.clear();
 		m_uninterpretedTerms.clear();
 		resetStateVariables();
 		initializeLocalVariables(_function);
@@ -268,16 +267,9 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 	else if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_assignment.leftHandSide()))
 	{
 		VariableDeclaration const& decl = dynamic_cast<VariableDeclaration const&>(*identifier->annotation().referencedDeclaration);
-		if (knownVariable(decl))
-		{
-			assignment(decl, _assignment.rightHandSide(), _assignment.location());
-			defineExpr(_assignment, expr(_assignment.rightHandSide()));
-		}
-		else
-			m_errorReporter.warning(
-				_assignment.location(),
-				"Assertion checker does not yet implement such assignments."
-			);
+		solAssert(knownVariable(decl), "");
+		assignment(decl, _assignment.rightHandSide(), _assignment.location());
+		defineExpr(_assignment, expr(_assignment.rightHandSide()));
 	}
 	else
 		m_errorReporter.warning(
@@ -288,7 +280,11 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 
 void SMTChecker::endVisit(TupleExpression const& _tuple)
 {
-	if (_tuple.isInlineArray() || _tuple.components().size() != 1)
+	if (
+		_tuple.isInlineArray() ||
+		_tuple.components().size() != 1 ||
+		!isSupportedType(_tuple.components()[0]->annotation().type->category())
+	)
 		m_errorReporter.warning(
 			_tuple.location(),
 			"Assertion checker does not yet implement tuples and inline arrays."
@@ -399,18 +395,30 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 
 	std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
-	if (funType.kind() == FunctionType::Kind::Assert)
+	switch (funType.kind())
+	{
+	case FunctionType::Kind::Assert:
 		visitAssert(_funCall);
-	else if (funType.kind() == FunctionType::Kind::Require)
+		break;
+	case FunctionType::Kind::Require:
 		visitRequire(_funCall);
-	else if (funType.kind() == FunctionType::Kind::GasLeft)
+		break;
+	case FunctionType::Kind::GasLeft:
 		visitGasLeft(_funCall);
-	else if (funType.kind() == FunctionType::Kind::BlockHash)
-		visitBlockHash(_funCall);
-	else if (funType.kind() == FunctionType::Kind::Internal)
+		break;
+	case FunctionType::Kind::Internal:
 		inlineFunctionCall(_funCall);
-	else
-	{
+		break;
+	case FunctionType::Kind::KECCAK256:
+	case FunctionType::Kind::ECRecover:
+	case FunctionType::Kind::SHA256:
+	case FunctionType::Kind::RIPEMD160:
+	case FunctionType::Kind::BlockHash:
+	case FunctionType::Kind::AddMod:
+	case FunctionType::Kind::MulMod:
+		abstractFunctionCall(_funCall);
+		break;
+	default:
 		m_errorReporter.warning(
 			_funCall.location(),
 			"Assertion checker does not yet implement this type of function call."
@@ -442,8 +450,8 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 	string gasLeft = "gasleft()";
 	// We increase the variable index since gasleft changes
 	// inside a tx.
-	defineSpecialVariable(gasLeft, _funCall, true);
-	auto const& symbolicVar = m_specialVariables.at(gasLeft);
+	defineGlobalVariable(gasLeft, _funCall, true);
+	auto const& symbolicVar = m_globalContext.at(gasLeft);
 	unsigned index = symbolicVar->index();
 	// We set the current value to unknown anyway to add type constraints.
 	setUnknownValue(*symbolicVar);
@@ -451,21 +459,6 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 		m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
 
-void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
-{
-	string blockHash = "blockhash";
-	auto const& arguments = _funCall.arguments();
-	solAssert(arguments.size() == 1, "");
-	smt::SortPointer paramSort = smtSort(*arguments.at(0)->annotation().type);
-	smt::SortPointer returnSort = smtSort(*_funCall.annotation().type);
-	defineUninterpretedFunction(
-		blockHash,
-		make_shared<smt::FunctionSort>(vector<smt::SortPointer>{paramSort}, returnSort)
-	);
-	defineExpr(_funCall, m_uninterpretedFunctions.at(blockHash)({expr(*arguments.at(0))}));
-	m_uninterpretedTerms.push_back(&_funCall);
-}
-
 void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 {
 	FunctionDefinition const* _funDef = nullptr;
@@ -533,29 +526,32 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
 	}
 }
 
+void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
+{
+	vector<smt::Expression> smtArguments;
+	for (auto const& arg: _funCall.arguments())
+		smtArguments.push_back(expr(*arg));
+	defineExpr(_funCall, (*m_expressions.at(&_funCall.expression()))(smtArguments));
+	m_uninterpretedTerms.push_back(&_funCall);
+	setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_interface);
+}
+
 void SMTChecker::endVisit(Identifier const& _identifier)
 {
 	if (_identifier.annotation().lValueRequested)
 	{
 		// Will be translated as part of the node that requested the lvalue.
 	}
-	else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
+	else if (dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
 	{
-		if (
-			fun->kind() == FunctionType::Kind::Assert ||
-			fun->kind() == FunctionType::Kind::Require ||
-			fun->kind() == FunctionType::Kind::GasLeft ||
-			fun->kind() == FunctionType::Kind::BlockHash
-		)
-			return;
-		createExpr(_identifier);
+		visitFunctionIdentifier(_identifier);
 	}
 	else if (isSupportedType(_identifier.annotation().type->category()))
 	{
 		if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
 			defineExpr(_identifier, currentValue(*decl));
 		else if (_identifier.name() == "now")
-			defineSpecialVariable(_identifier.name(), _identifier);
+			defineGlobalVariable(_identifier.name(), _identifier);
 		else
 			// TODO: handle MagicVariableDeclaration here
 			m_errorReporter.warning(
@@ -565,6 +561,20 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 	}
 }
 
+void SMTChecker::visitFunctionIdentifier(Identifier const& _identifier)
+{
+	auto const& fType = dynamic_cast<FunctionType const&>(*_identifier.annotation().type);
+	if (fType.returnParameterTypes().size() > 1)
+	{
+		m_errorReporter.warning(
+			_identifier.location(),
+			"Assertion checker does not yet support functions with more than one return parameter."
+		);
+	}
+	defineGlobalFunction(fType.richIdentifier(), _identifier);
+	m_expressions.emplace(&_identifier, m_globalContext.at(fType.richIdentifier()));
+}
+
 void SMTChecker::endVisit(Literal const& _literal)
 {
 	Type const& type = *_literal.annotation().type;
@@ -616,7 +626,7 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
 				_memberAccess.location(),
 				"Assertion checker does not yet support this expression."
 			);
-		defineSpecialVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
+		defineGlobalVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
 		return false;
 	}
 	else
@@ -628,30 +638,39 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
 	return true;
 }
 
-void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
+void SMTChecker::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
 {
-	if (!knownSpecialVariable(_name))
+	if (!knownGlobalSymbol(_name))
 	{
 		auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
-		m_specialVariables.emplace(_name, result.second);
+		m_globalContext.emplace(_name, result.second);
 		setUnknownValue(*result.second);
 		if (result.first)
 			m_errorReporter.warning(
 				_expr.location(),
-				"Assertion checker does not yet support this special variable."
+				"Assertion checker does not yet support this global variable."
 			);
 	}
 	else if (_increaseIndex)
-		m_specialVariables.at(_name)->increaseIndex();
+		m_globalContext.at(_name)->increaseIndex();
 	// The default behavior is not to increase the index since
-	// most of the special values stay the same throughout a tx.
-	defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
+	// most of the global values stay the same throughout a tx.
+	if (isSupportedType(_expr.annotation().type->category()))
+		defineExpr(_expr, m_globalContext.at(_name)->currentValue());
 }
 
-void SMTChecker::defineUninterpretedFunction(string const& _name, smt::SortPointer _sort)
+void SMTChecker::defineGlobalFunction(string const& _name, Expression const& _expr)
 {
-	if (!m_uninterpretedFunctions.count(_name))
-		m_uninterpretedFunctions.emplace(_name, m_interface->newVariable(_name, _sort));
+	if (!knownGlobalSymbol(_name))
+	{
+		auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface);
+		m_globalContext.emplace(_name, result.second);
+		if (result.first)
+			m_errorReporter.warning(
+				_expr.location(),
+				"Assertion checker does not yet support the type of this function."
+			);
+	}
 }
 
 void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
@@ -831,10 +850,13 @@ void SMTChecker::checkCondition(
 			expressionsToEvaluate.emplace_back(currentValue(*var.first));
 			expressionNames.push_back(var.first->name());
 		}
-		for (auto const& var: m_specialVariables)
+		for (auto const& var: m_globalContext)
 		{
-			expressionsToEvaluate.emplace_back(var.second->currentValue());
-			expressionNames.push_back(var.first);
+			if (smtKind(var.second->type()->category()) != smt::Kind::Function)
+			{
+				expressionsToEvaluate.emplace_back(var.second->currentValue());
+				expressionNames.push_back(var.first);
+			}
 		}
 		for (auto const& uf: m_uninterpretedTerms)
 		{
@@ -1147,9 +1169,9 @@ bool SMTChecker::knownExpr(Expression const& _e) const
 	return m_expressions.count(&_e);
 }
 
-bool SMTChecker::knownSpecialVariable(string const& _var) const
+bool SMTChecker::knownGlobalSymbol(string const& _var) const
 {
-	return m_specialVariables.count(_var);
+	return m_globalContext.count(_var);
 }
 
 void SMTChecker::createExpr(Expression const& _e)
@@ -1172,6 +1194,7 @@ void SMTChecker::createExpr(Expression const& _e)
 void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
 {
 	createExpr(_e);
+	solAssert(isSupportedType(*_e.annotation().type), "Equality operator applied to type that is not fully supported");
 	m_interface->addAssertion(expr(_e) == _value);
 }
 
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 34724848..9f8c04ab 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -84,16 +84,18 @@ private:
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 
-	void visitAssert(FunctionCall const&);
-	void visitRequire(FunctionCall const&);
-	void visitGasLeft(FunctionCall const&);
-	void visitBlockHash(FunctionCall const&);
+	void visitAssert(FunctionCall const& _funCall);
+	void visitRequire(FunctionCall const& _funCall);
+	void visitGasLeft(FunctionCall const& _funCall);
 	/// Visits the FunctionDefinition of the called function
 	/// if available and inlines the return value.
-	void inlineFunctionCall(FunctionCall const&);
+	void inlineFunctionCall(FunctionCall const& _funCall);
+	/// Creates an uninterpreted function call.
+	void abstractFunctionCall(FunctionCall const& _funCall);
+	void visitFunctionIdentifier(Identifier const& _identifier);
 
-	void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
-	void defineUninterpretedFunction(std::string const& _name, smt::SortPointer _sort);
+	void defineGlobalVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
+	void defineGlobalFunction(std::string const& _name, Expression const& _expr);
 
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
@@ -176,8 +178,8 @@ private:
 	/// Creates the expression and sets its value.
 	void defineExpr(Expression const& _e, smt::Expression _value);
 
-	/// Checks if special variable was seen.
-	bool knownSpecialVariable(std::string const& _var) const;
+	/// Checks if special variable or function was seen.
+	bool knownGlobalSymbol(std::string const& _var) const;
 
 	/// Adds a new path condition
 	void pushPathCondition(smt::Expression const& _e);
@@ -205,9 +207,7 @@ private:
 	/// 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_specialVariables;
-	/// Stores the declaration of an Uninterpreted Function.
-	std::unordered_map<std::string, smt::Expression> m_uninterpretedFunctions;
+	std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_globalContext;
 	/// Stores the instances of an Uninterpreted Function applied to arguments.
 	/// Used to retrieve models.
 	std::vector<Expression const*> m_uninterpretedTerms;
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index c297c807..3cfaa271 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -38,15 +38,25 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type)
 		solAssert(fType, "");
 		vector<smt::SortPointer> parameterSorts = smtSort(fType->parameterTypes());
 		auto returnTypes = fType->returnParameterTypes();
-		// TODO remove this when we support tuples.
-		solAssert(returnTypes.size() == 1, "");
-		smt::SortPointer returnSort = smtSort(*returnTypes.at(0));
+		smt::SortPointer returnSort;
+		// TODO change this when we support tuples.
+		if (returnTypes.size() == 0)
+			// We cannot declare functions without a return sort, so we use the smallest.
+			returnSort = make_shared<smt::Sort>(smt::Kind::Bool);
+		else if (returnTypes.size() > 1)
+			// Abstract sort.
+			returnSort = make_shared<smt::Sort>(smt::Kind::Int);
+		else
+			returnSort = smtSort(*returnTypes.at(0));
 		return make_shared<smt::FunctionSort>(parameterSorts, returnSort);
 	}
 	case smt::Kind::Array:
 	{
 		solUnimplementedAssert(false, "Invalid type");
 	}
+	default:
+		// Abstract case.
+		return make_shared<smt::Sort>(smt::Kind::Int);
 	}
 	solAssert(false, "Invalid type");
 }
@@ -65,13 +75,21 @@ smt::Kind dev::solidity::smtKind(Type::Category _category)
 		return smt::Kind::Int;
 	else if (isBool(_category))
 		return smt::Kind::Bool;
-	solAssert(false, "Invalid type");
+	else if (isFunction(_category))
+		return smt::Kind::Function;
+	// Abstract case.
+	return smt::Kind::Int;
 }
 
 bool dev::solidity::isSupportedType(Type::Category _category)
 {
 	return isNumber(_category) ||
-		isBool(_category) ||
+		isBool(_category);
+}
+
+bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category)
+{
+	return isSupportedType(_category) ||
 		isFunction(_category);
 }
 
@@ -84,7 +102,7 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
 	bool abstract = false;
 	shared_ptr<SymbolicVariable> var;
 	TypePointer type = _type.shared_from_this();
-	if (!isSupportedType(_type))
+	if (!isSupportedTypeDeclaration(_type))
 	{
 		abstract = true;
 		var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
@@ -92,7 +110,7 @@ pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
 	else if (isBool(_type.category()))
 		var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _solver);
 	else if (isFunction(_type.category()))
-		var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver);
+		var = make_shared<SymbolicFunctionVariable>(type, _uniqueName, _solver);
 	else if (isInteger(_type.category()))
 		var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver);
 	else if (isFixedBytes(_type.category()))
@@ -122,6 +140,11 @@ bool dev::solidity::isSupportedType(Type const& _type)
 	return isSupportedType(_type.category());
 }
 
+bool dev::solidity::isSupportedTypeDeclaration(Type const& _type)
+{
+	return isSupportedTypeDeclaration(_type.category());
+}
+
 bool dev::solidity::isInteger(Type::Category _category)
 {
 	return _category == Type::Category::Integer;
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 984653b3..2c568f5b 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -34,10 +34,12 @@ std::vector<smt::SortPointer> smtSort(std::vector<TypePointer> const& _types);
 /// Returns the SMT kind that models the Solidity type type category _category.
 smt::Kind smtKind(Type::Category _category);
 
-/// So far int, bool and address are supported.
-/// Returns true if type is supported.
+/// Returns true if type is fully supported (declaration and operations).
 bool isSupportedType(Type::Category _category);
 bool isSupportedType(Type const& _type);
+/// Returns true if type is partially supported (declaration).
+bool isSupportedTypeDeclaration(Type::Category _category);
+bool isSupportedTypeDeclaration(Type const& _type);
 
 bool isInteger(Type::Category _category);
 bool isRational(Type::Category _category);