Merge pull request #5478 from ethereum/smt_refactor_sort_patch3

[SMTChecker] Add ArraySort and array operations

5 files changed, 76 insertions, 2 deletions

diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index cff1717f..de5e4430 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -164,6 +164,10 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 		return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
 	else if (n == "/")
 		return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);
+	else if (n == "select")
+		return m_context.mkExpr(CVC4::kind::SELECT, arguments[0], arguments[1]);
+	else if (n == "store")
+		return m_context.mkExpr(CVC4::kind::STORE, arguments[0], arguments[1], arguments[2]);
 	// Cannot reach here.
 	solAssert(false, "");
 	return arguments[0];
@@ -182,6 +186,11 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
 		FunctionSort const& fSort = dynamic_cast<FunctionSort const&>(_sort);
 		return m_context.mkFunctionType(cvc4Sort(fSort.domain), cvc4Sort(*fSort.codomain));
 	}
+	case Kind::Array:
+	{
+		auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
+		return m_context.mkArrayType(cvc4Sort(*arraySort.domain), cvc4Sort(*arraySort.range));
+	}
 	default:
 		break;
 	}
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index bb85860f..55c72cfc 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -144,6 +144,11 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 		return "Int";
 	case Kind::Bool:
 		return "Bool";
+	case Kind::Array:
+	{
+		auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
+		return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')';
+	}
 	default:
 		solAssert(false, "Invalid SMT sort");
 	}
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 551ef8e9..17e6904c 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -46,7 +46,8 @@ enum class Kind
 {
 	Int,
 	Bool,
-	Function
+	Function,
+	Array
 };
 
 struct Sort
@@ -79,6 +80,20 @@ struct FunctionSort: public Sort
 	}
 };
 
+struct ArraySort: public Sort
+{
+	/// _domain is the sort of the indices
+	/// _range is the sort of the values
+	ArraySort(SortPointer _domain, SortPointer _range):
+		Sort(Kind::Array), domain(std::move(_domain)), range(std::move(_range)) {}
+	SortPointer domain;
+	SortPointer range;
+	bool operator==(ArraySort const& _other) const
+	{
+		return Sort::operator==(_other) && *domain == *_other.domain && *range == *_other.range;
+	}
+};
+
 /// C++ representation of an SMTLIB2 expression.
 class Expression
 {
@@ -109,7 +124,9 @@ public:
 			{"+", 2},
 			{"-", 2},
 			{"*", 2},
-			{"/", 2}
+			{"/", 2},
+			{"select", 2},
+			{"store", 3}
 		};
 		return operatorsArity.count(name) && operatorsArity.at(name) == arguments.size();
 	}
@@ -127,6 +144,36 @@ public:
 		return !std::move(_a) || std::move(_b);
 	}
 
+	/// select is the SMT representation of an array index access.
+	static Expression select(Expression _array, Expression _index)
+	{
+		solAssert(_array.sort->kind == Kind::Array, "");
+		auto const& arraySort = dynamic_cast<ArraySort const*>(_array.sort.get());
+		solAssert(arraySort, "");
+		solAssert(*arraySort->domain == *_index.sort, "");
+		return Expression(
+			"select",
+			std::vector<Expression>{std::move(_array), std::move(_index)},
+			arraySort->range
+		);
+	}
+
+	/// store is the SMT representation of an assignment to array index.
+	/// The function is pure and returns the modified array.
+	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());
+		solAssert(arraySort, "");
+		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
+		);
+	}
+
 	friend Expression operator!(Expression _a)
 	{
 		return Expression("not", std::move(_a), Kind::Bool);
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 2d0107c5..a12ab142 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -43,6 +43,10 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type)
 		smt::SortPointer returnSort = smtSort(*returnTypes.at(0));
 		return make_shared<smt::FunctionSort>(parameterSorts, returnSort);
 	}
+	case smt::Kind::Array:
+	{
+		solUnimplementedAssert(false, "Invalid type");
+	}
 	}
 	solAssert(false, "Invalid type");
 }
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 162b0c23..cb01dc61 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -163,6 +163,10 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 		return arguments[0] * arguments[1];
 	else if (n == "/")
 		return arguments[0] / arguments[1];
+	else if (n == "select")
+		return z3::select(arguments[0], arguments[1]);
+	else if (n == "store")
+		return z3::store(arguments[0], arguments[1], arguments[2]);
 	// Cannot reach here.
 	solAssert(false, "");
 	return arguments[0];
@@ -176,6 +180,11 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort)
 		return m_context.bool_sort();
 	case Kind::Int:
 		return m_context.int_sort();
+	case Kind::Array:
+	{
+		auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
+		return m_context.array_sort(z3Sort(*arraySort.domain), z3Sort(*arraySort.range));
+	}
 	default:
 		break;
 	}