Merge pull request #8531 from ethereum/smt_sort_provider

[SMTChecker] Add SortProvider

libsolidity/CMakeLists.txt

@@ -100,6 +100,8 @@ set(sources
 	formal/SMTPortfolio.cpp
 	formal/SMTPortfolio.h
 	formal/SolverInterface.h
+	formal/Sorts.cpp
+	formal/Sorts.h
 	formal/SSAVariable.cpp
 	formal/SSAVariable.h
 	formal/SymbolicTypes.cpp

libsolidity/formal/CHC.cpp

@@ -79,10 +79,9 @@ void CHC::analyze(SourceUnit const& _source)
 
 	resetSourceAnalysis();
 
-	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
 	auto genesisSort = make_shared<smt::FunctionSort>(
 		vector<smt::SortPointer>(),
-		boolSort
+		smt::SortProvider::boolSort
 	);
 	m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis");
 	addRule(genesis(), "genesis");
@@ -131,12 +130,9 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 	clearIndices(&_contract);
 
-
-	// TODO create static instances for Bool/Int sorts in SolverInterface.
-	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
 	auto errorFunctionSort = make_shared<smt::FunctionSort>(
 		vector<smt::SortPointer>(),
-		boolSort
+		smt::SortProvider::boolSort
 	);
 
 	string suffix = _contract.name() + "_" + to_string(_contract.id());
@@ -664,29 +660,25 @@ vector<smt::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
 
 smt::SortPointer CHC::constructorSort()
 {
-	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
-	auto intSort = make_shared<smt::Sort>(smt::Kind::Int);
 	return make_shared<smt::FunctionSort>(
-		vector<smt::SortPointer>{intSort} + m_stateSorts,
+		vector<smt::SortPointer>{smt::SortProvider::intSort} + m_stateSorts,
-		boolSort
+		smt::SortProvider::boolSort
 	);
 }
 
 smt::SortPointer CHC::interfaceSort()
 {
-	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
 	return make_shared<smt::FunctionSort>(
 		m_stateSorts,
-		boolSort
+		smt::SortProvider::boolSort
 	);
 }
 
 smt::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
 {
-	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
 	return make_shared<smt::FunctionSort>(
 		stateSorts(_contract),
-		boolSort
+		smt::SortProvider::boolSort
 	);
 }
 
@@ -703,8 +695,6 @@ smt::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
 /// - 1 set of output variables
 smt::SortPointer CHC::sort(FunctionDefinition const& _function)
 {
-	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
-	auto intSort = make_shared<smt::Sort>(smt::Kind::Int);
 	vector<smt::SortPointer> inputSorts;
 	for (auto const& var: _function.parameters())
 		inputSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
@@ -712,8 +702,8 @@ smt::SortPointer CHC::sort(FunctionDefinition const& _function)
 	for (auto const& var: _function.returnParameters())
 		outputSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
 	return make_shared<smt::FunctionSort>(
-		vector<smt::SortPointer>{intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts,
+		vector<smt::SortPointer>{smt::SortProvider::intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts,
-		boolSort
+		smt::SortProvider::boolSort
 	);
 }
 
@@ -725,13 +715,12 @@ smt::SortPointer CHC::sort(ASTNode const* _node)
 	auto fSort = dynamic_pointer_cast<smt::FunctionSort>(sort(*m_currentFunction));
 	solAssert(fSort, "");
 
-	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
 	vector<smt::SortPointer> varSorts;
 	for (auto const& var: m_currentFunction->localVariables())
 		varSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
 	return make_shared<smt::FunctionSort>(
 		fSort->domain + varSorts,
-		boolSort
+		smt::SortProvider::boolSort
 	);
 }
 
@@ -740,16 +729,14 @@ smt::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractD
 	auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
 	auto sorts = stateSorts(_contract);
 
-	auto boolSort = make_shared<smt::Sort>(smt::Kind::Bool);
-	auto intSort = make_shared<smt::Sort>(smt::Kind::Int);
 	vector<smt::SortPointer> inputSorts, outputSorts;
 	for (auto const& var: _function.parameters())
 		inputSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
 	for (auto const& var: _function.returnParameters())
 		outputSorts.push_back(smt::smtSortAbstractFunction(*var->type()));
 	return make_shared<smt::FunctionSort>(
-		vector<smt::SortPointer>{intSort} + sorts + inputSorts + sorts + outputSorts,
+		vector<smt::SortPointer>{smt::SortProvider::intSort} + sorts + inputSorts + sorts + outputSorts,
-		boolSort
+		smt::SortProvider::boolSort
 	);
 }
 

libsolidity/formal/EncodingContext.cpp

@@ -28,8 +28,8 @@ EncodingContext::EncodingContext():
 	m_thisAddress(make_unique<SymbolicAddressVariable>("this", *this))
 {
 	auto sort = make_shared<ArraySort>(
-		make_shared<Sort>(Kind::Int),
+		SortProvider::intSort,
-		make_shared<Sort>(Kind::Int)
+		SortProvider::intSort
 	);
 	m_balances = make_unique<SymbolicVariable>(sort, "balances", *this);
 }

libsolidity/formal/SolverInterface.h

@@ -17,6 +17,8 @@
 
 #pragma once
 
+#include <libsolidity/formal/Sorts.h>
+
 #include <libsolidity/ast/Types.h>
 #include <libsolidity/interface/ReadFile.h>
 #include <liblangutil/Exceptions.h>
@@ -52,94 +54,6 @@ enum class CheckResult
 	SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR
 };
 
-enum class Kind
-{
-	Int,
-	Bool,
-	Function,
-	Array,
-	Sort
-};
-
-struct Sort
-{
-	Sort(Kind _kind):
-		kind(_kind) {}
-	virtual ~Sort() = default;
-	virtual bool operator==(Sort const& _other) const { return kind == _other.kind; }
-
-	Kind const kind;
-};
-using SortPointer = std::shared_ptr<Sort>;
-
-struct FunctionSort: public Sort
-{
-	FunctionSort(std::vector<SortPointer> _domain, SortPointer _codomain):
-		Sort(Kind::Function), domain(std::move(_domain)), codomain(std::move(_codomain)) {}
-	bool operator==(Sort const& _other) const override
-	{
-		if (!Sort::operator==(_other))
-			return false;
-		auto _otherFunction = dynamic_cast<FunctionSort const*>(&_other);
-		solAssert(_otherFunction, "");
-		if (domain.size() != _otherFunction->domain.size())
-			return false;
-		if (!std::equal(
-			domain.begin(),
-			domain.end(),
-			_otherFunction->domain.begin(),
-			[&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
-		))
-			return false;
-		solAssert(codomain, "");
-		solAssert(_otherFunction->codomain, "");
-		return *codomain == *_otherFunction->codomain;
-	}
-
-	std::vector<SortPointer> domain;
-	SortPointer codomain;
-};
-
-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)) {}
-	bool operator==(Sort const& _other) const override
-	{
-		if (!Sort::operator==(_other))
-			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;
-	}
-
-	SortPointer domain;
-	SortPointer range;
-};
-
-struct SortSort: public Sort
-{
-	SortSort(SortPointer _inner): Sort(Kind::Sort), inner(std::move(_inner)) {}
-	bool operator==(Sort const& _other) const override
-	{
-		if (!Sort::operator==(_other))
-			return false;
-		auto _otherSort = dynamic_cast<SortSort const*>(&_other);
-		solAssert(_otherSort, "");
-		solAssert(_otherSort->inner, "");
-		solAssert(inner, "");
-		return *inner == *_otherSort->inner;
-	}
-
-	SortPointer inner;
-};
-
 // Forward declaration.
 SortPointer smtSort(Type const& _type);
 

libsolidity/formal/Sorts.cpp

@@ -0,0 +1,29 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+
+#include <libsolidity/formal/Sorts.h>
+
+using namespace std;
+
+namespace solidity::frontend::smt
+{
+
+shared_ptr<Sort> const SortProvider::boolSort{make_shared<Sort>(Kind::Bool)};
+shared_ptr<Sort> const SortProvider::intSort{make_shared<Sort>(Kind::Int)};
+
+}

libsolidity/formal/Sorts.h

@@ -0,0 +1,125 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <liblangutil/Exceptions.h>
+#include <libsolutil/Common.h>
+#include <libsolutil/Exceptions.h>
+
+#include <memory>
+#include <vector>
+
+namespace solidity::frontend::smt
+{
+
+enum class Kind
+{
+	Int,
+	Bool,
+	Function,
+	Array,
+	Sort
+};
+
+struct Sort
+{
+	Sort(Kind _kind):
+		kind(_kind) {}
+	virtual ~Sort() = default;
+	virtual bool operator==(Sort const& _other) const { return kind == _other.kind; }
+
+	Kind const kind;
+};
+using SortPointer = std::shared_ptr<Sort>;
+
+struct FunctionSort: public Sort
+{
+	FunctionSort(std::vector<SortPointer> _domain, SortPointer _codomain):
+		Sort(Kind::Function), domain(std::move(_domain)), codomain(std::move(_codomain)) {}
+	bool operator==(Sort const& _other) const override
+	{
+		if (!Sort::operator==(_other))
+			return false;
+		auto _otherFunction = dynamic_cast<FunctionSort const*>(&_other);
+		solAssert(_otherFunction, "");
+		if (domain.size() != _otherFunction->domain.size())
+			return false;
+		if (!std::equal(
+			domain.begin(),
+			domain.end(),
+			_otherFunction->domain.begin(),
+			[&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
+		))
+			return false;
+		solAssert(codomain, "");
+		solAssert(_otherFunction->codomain, "");
+		return *codomain == *_otherFunction->codomain;
+	}
+
+	std::vector<SortPointer> domain;
+	SortPointer codomain;
+};
+
+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)) {}
+	bool operator==(Sort const& _other) const override
+	{
+		if (!Sort::operator==(_other))
+			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;
+	}
+
+	SortPointer domain;
+	SortPointer range;
+};
+
+struct SortSort: public Sort
+{
+	SortSort(SortPointer _inner): Sort(Kind::Sort), inner(std::move(_inner)) {}
+	bool operator==(Sort const& _other) const override
+	{
+		if (!Sort::operator==(_other))
+			return false;
+		auto _otherSort = dynamic_cast<SortSort const*>(&_other);
+		solAssert(_otherSort, "");
+		solAssert(_otherSort->inner, "");
+		solAssert(inner, "");
+		return *inner == *_otherSort->inner;
+	}
+
+	SortPointer inner;
+};
+
+/** Frequently used sorts.*/
+struct SortProvider
+{
+	static std::shared_ptr<Sort> const boolSort;
+	static std::shared_ptr<Sort> const intSort;
+};
+
+}

libsolidity/formal/SymbolicTypes.cpp

@@ -32,9 +32,9 @@ SortPointer smtSort(frontend::Type const& _type)
 	switch (smtKind(_type.category()))
 	{
 	case Kind::Int:
-		return make_shared<Sort>(Kind::Int);
+		return SortProvider::intSort;
 	case Kind::Bool:
-		return make_shared<Sort>(Kind::Bool);
+		return SortProvider::boolSort;
 	case Kind::Function:
 	{
 		auto fType = dynamic_cast<frontend::FunctionType const*>(&_type);
@@ -45,10 +45,10 @@ SortPointer smtSort(frontend::Type const& _type)
 		// 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<Sort>(Kind::Bool);
+			returnSort = SortProvider::boolSort;
 		else if (returnTypes.size() > 1)
 			// Abstract sort.
-			returnSort = make_shared<Sort>(Kind::Int);
+			returnSort = SortProvider::intSort;
 		else
 			returnSort = smtSort(*returnTypes.front());
 		return make_shared<FunctionSort>(parameterSorts, returnSort);
@@ -65,20 +65,19 @@ SortPointer smtSort(frontend::Type const& _type)
 		{
 			auto stringLitType = dynamic_cast<frontend::StringLiteralType const*>(&_type);
 			solAssert(stringLitType, "");
-			auto intSort = make_shared<Sort>(Kind::Int);
+			return make_shared<ArraySort>(SortProvider::intSort, SortProvider::intSort);
-			return make_shared<ArraySort>(intSort, intSort);
 		}
 		else
 		{
 			solAssert(isArray(_type.category()), "");
 			auto arrayType = dynamic_cast<frontend::ArrayType const*>(&_type);
 			solAssert(arrayType, "");
-			return make_shared<ArraySort>(make_shared<Sort>(Kind::Int), smtSortAbstractFunction(*arrayType->baseType()));
+			return make_shared<ArraySort>(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType()));
 		}
 	}
 	default:
 		// Abstract case.
-		return make_shared<Sort>(Kind::Int);
+		return SortProvider::intSort;
 	}
 }
 
@@ -93,7 +92,7 @@ vector<SortPointer> smtSort(vector<frontend::TypePointer> const& _types)
 SortPointer smtSortAbstractFunction(frontend::Type const& _type)
 {
 	if (isFunction(_type.category()))
-		return make_shared<Sort>(Kind::Int);
+		return SortProvider::intSort;
 	return smtSort(_type);
 }