Merge pull request #5251 from ethereum/smt_refactor_expr_types

[SMTChecker] Refactor expressions to use SymbolicVariable

4 files changed, 62 insertions, 79 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 671c2049..e5648eb3 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -458,6 +458,12 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 	{
 		// 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()))
+	{
+		if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
+			return;
+		createExpr(_identifier);
+	}
 	else if (isSupportedType(_identifier.annotation().type->category()))
 	{
 		if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
@@ -469,25 +475,15 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 				"Assertion checker does not yet support the type of this variable."
 			);
 	}
-	else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
-	{
-		if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
-			return;
-		createExpr(_identifier);
-	}
 }
 
 void SMTChecker::endVisit(Literal const& _literal)
 {
 	Type const& type = *_literal.annotation().type;
-	if (type.category() == Type::Category::Integer || type.category() == Type::Category::Address || type.category() == Type::Category::RationalNumber)
-	{
-		if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type))
-			solAssert(!rational->isFractional(), "");
+	if (isNumber(type.category()))
 
 		defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
-	}
-	else if (type.category() == Type::Category::Bool)
+	else if (isBool(type.category()))
 		defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
 	else
 		m_errorReporter.warning(
@@ -917,13 +913,10 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 	if (hasVariable(_varDecl))
 		return true;
 	auto const& type = _varDecl.type();
-	if (isSupportedType(type->category()))
-	{
-		solAssert(m_variables.count(&_varDecl) == 0, "");
-		m_variables.emplace(&_varDecl, newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface));
-		return true;
-	}
-	else
+	solAssert(m_variables.count(&_varDecl) == 0, "");
+	auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface);
+	m_variables.emplace(&_varDecl, result.second);
+	if (result.first)
 	{
 		m_errorReporter.warning(
 			_varDecl.location(),
@@ -931,6 +924,7 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 		);
 		return false;
 	}
+	return true;
 }
 
 string SMTChecker::uniqueSymbol(Expression const& _expr)
@@ -980,7 +974,7 @@ smt::Expression SMTChecker::expr(Expression const& _e)
 		m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
 		createExpr(_e);
 	}
-	return prev(m_expressions.upper_bound(&_e))->second;
+	return m_expressions.at(&_e)->currentValue();
 }
 
 bool SMTChecker::hasExpr(Expression const& _e) const
@@ -996,33 +990,17 @@ bool SMTChecker::hasVariable(VariableDeclaration const& _var) const
 void SMTChecker::createExpr(Expression const& _e)
 {
 	solAssert(_e.annotation().type, "");
-	string exprSymbol = uniqueSymbol(_e) + "_" + to_string(m_expressions.count(&_e));
-	switch (_e.annotation().type->category())
-	{
-	case Type::Category::RationalNumber:
+	if (hasExpr(_e))
+		m_expressions.at(&_e)->increaseIndex();
+	else
 	{
-		if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
-			solAssert(!rational->isFractional(), "");
-		m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
-		break;
-	}
-	case Type::Category::Address:
-	case Type::Category::Integer:
-		m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
-		break;
-	case Type::Category::Bool:
-		m_expressions.emplace(&_e, m_interface->newBool(exprSymbol));
-		break;
-	case Type::Category::Function:
-		// This should be replaced by a `non-deterministic` type in the future.
-		m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
-		break;
-	default:
-		m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol));
-		m_errorReporter.warning(
-			_e.location(),
-			"Assertion checker does not yet implement this type."
-		);
+		auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface);
+		m_expressions.emplace(&_e, result.second);
+		if (result.first)
+			m_errorReporter.warning(
+				_e.location(),
+				"Assertion checker does not yet implement this type."
+			);
 	}
 }
 
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 0b078556..f66693d2 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -25,7 +25,6 @@
 
 #include <libsolidity/interface/ReadFile.h>
 
-#include <map>
 #include <unordered_map>
 #include <string>
 #include <vector>
@@ -186,7 +185,7 @@ private:
 	bool m_loopExecutionHappened = false;
 	/// An Expression may have multiple smt::Expression due to
 	/// repeated calls to the same function.
-	std::multimap<Expression const*, smt::Expression> m_expressions;
+	std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
 	std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 2d993865..d47869db 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -30,27 +30,44 @@ using namespace dev::solidity;
 
 bool dev::solidity::isSupportedType(Type::Category _category)
 {
-	return isInteger(_category) ||
-		isAddress(_category) ||
-		isBool(_category);
+	return isNumber(_category) ||
+		isBool(_category) ||
+		isFunction(_category);
 }
 
-shared_ptr<SymbolicVariable> dev::solidity::newSymbolicVariable(
+pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable(
 	Type const& _type,
 	std::string const& _uniqueName,
 	smt::SolverInterface& _solver
 )
 {
+	bool abstract = false;
+	shared_ptr<SymbolicVariable> var;
 	if (!isSupportedType(_type))
-		return nullptr;
-	if (isBool(_type.category()))
-		return make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver);
+	{
+		abstract = true;
+		var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
+	}
+	else if (isBool(_type.category()))
+		var = make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver);
+	else if (isFunction(_type.category()))
+		var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
 	else if (isInteger(_type.category()))
-		return make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
+		var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
 	else if (isAddress(_type.category()))
-		return make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver);
+		var = make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver);
+	else if (isRational(_type.category()))
+	{
+		auto rational = dynamic_cast<RationalNumberType const*>(&_type);
+		solAssert(rational, "");
+		if (rational->isFractional())
+			var = make_shared<SymbolicIntVariable>(IntegerType{256}, _uniqueName, _solver);
+		else
+			var = make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
+	}
 	else
 		solAssert(false, "");
+	return make_pair(abstract, var);
 }
 
 bool dev::solidity::isSupportedType(Type const& _type)
@@ -63,9 +80,9 @@ bool dev::solidity::isInteger(Type::Category _category)
 	return _category == Type::Category::Integer;
 }
 
-bool dev::solidity::isInteger(Type const& _type)
+bool dev::solidity::isRational(Type::Category _category)
 {
-	return isInteger(_type.category());
+	return _category == Type::Category::RationalNumber;
 }
 
 bool dev::solidity::isAddress(Type::Category _category)
@@ -73,30 +90,21 @@ bool dev::solidity::isAddress(Type::Category _category)
 	return _category == Type::Category::Address;
 }
 
-bool dev::solidity::isAddress(Type const& _type)
-{
-	return isAddress(_type.category());
-}
-
 bool dev::solidity::isNumber(Type::Category _category)
 {
 	return isInteger(_category) ||
+		isRational(_category) ||
 		isAddress(_category);
 }
 
-bool dev::solidity::isNumber(Type const& _type)
-{
-	return isNumber(_type.category());
-}
-
 bool dev::solidity::isBool(Type::Category _category)
 {
 	return _category == Type::Category::Bool;
 }
 
-bool dev::solidity::isBool(Type const& _type)
+bool dev::solidity::isFunction(Type::Category _category)
 {
-	return isBool(_type.category());
+	return _category == Type::Category::Function;
 }
 
 smt::Expression dev::solidity::minValue(IntegerType const& _type)
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 77822fed..0887fa41 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -34,18 +34,16 @@ bool isSupportedType(Type::Category _category);
 bool isSupportedType(Type const& _type);
 
 bool isInteger(Type::Category _category);
-bool isInteger(Type const& _type);
-
+bool isRational(Type::Category _category);
 bool isAddress(Type::Category _category);
-bool isAddress(Type const& _type);
-
 bool isNumber(Type::Category _category);
-bool isNumber(Type const& _type);
-
 bool isBool(Type::Category _category);
-bool isBool(Type const& _type);
+bool isFunction(Type::Category _category);
 
-std::shared_ptr<SymbolicVariable> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver);
+/// Returns a new symbolic variable, according to _type.
+/// Also returns whether the type is abstract or not,
+/// which is true for unsupported types.
+std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver);
 
 smt::Expression minValue(IntegerType const& _type);
 smt::Expression maxValue(IntegerType const& _type);