Merge pull request #11349 from ethereum/create-solver-class-from-reasoning-based-simplifier

Create solver class from reasoning based simplifier

libyul/CMakeLists.txt

@@ -166,6 +166,8 @@ add_library(yul
 	optimiser/RedundantAssignEliminator.h
 	optimiser/Rematerialiser.cpp
 	optimiser/Rematerialiser.h
+	optimiser/SMTSolver.cpp
+	optimiser/SMTSolver.h
 	optimiser/SSAReverser.cpp
 	optimiser/SSAReverser.h
 	optimiser/SSATransform.cpp

libyul/optimiser/ReasoningBasedSimplifier.cpp

@@ -16,8 +16,8 @@
 */
 
 #include <libyul/optimiser/ReasoningBasedSimplifier.h>
+#include <libyul/optimiser/SMTSolver.h>
 
-#include <libyul/optimiser/OptimizerUtilities.h>
 #include <libyul/optimiser/SSAValueTracker.h>
 #include <libyul/optimiser/Semantics.h>
 #include <libyul/AST.h>
@@ -56,14 +56,7 @@ std::optional<string> ReasoningBasedSimplifier::invalidInCurrentEnvironment()
 
 void ReasoningBasedSimplifier::operator()(VariableDeclaration& _varDecl)
 {
-	if (_varDecl.variables.size() != 1 || !_varDecl.value)
+	SMTSolver::encodeVariableDeclaration(_varDecl);
-		return;
-	YulString varName = _varDecl.variables.front().name;
-	if (!m_ssaVariables.count(varName))
-		return;
-	bool const inserted = m_variables.insert({varName, m_solver->newVariable("yul_" + varName.str(), defaultSort())}).second;
-	yulAssert(inserted, "");
-	m_solver->addAssertion(m_variables.at(varName) == encodeExpression(*_varDecl.value));
 }
 
 void ReasoningBasedSimplifier::operator()(If& _if)
@@ -111,37 +104,11 @@ ReasoningBasedSimplifier::ReasoningBasedSimplifier(
 	Dialect const& _dialect,
 	set<YulString> const& _ssaVariables
 ):
-	m_dialect(_dialect),
+	SMTSolver(_ssaVariables, _dialect),
-	m_ssaVariables(_ssaVariables),
+	m_dialect(_dialect)
-	m_solver(make_unique<smtutil::SMTPortfolio>())
 {
 }
 
-smtutil::Expression ReasoningBasedSimplifier::encodeExpression(yul::Expression const& _expression)
-{
-	return std::visit(GenericVisitor{
-		[&](FunctionCall const& _functionCall)
-		{
-			if (auto instruction = toEVMInstruction(m_dialect, _functionCall.functionName.name))
-				return encodeEVMBuiltin(*instruction, _functionCall.arguments);
-			return newRestrictedVariable();
-		},
-		[&](Identifier const& _identifier)
-		{
-			if (
-				m_ssaVariables.count(_identifier.name) &&
-				m_variables.count(_identifier.name)
-			)
-				return m_variables.at(_identifier.name);
-			else
-				return newRestrictedVariable();
-		},
-		[&](Literal const& _literal)
-		{
-			return literalValue(_literal);
-		}
-	}, _expression);
-}
 
 smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
 	evmasm::Instruction _instruction,
@@ -172,10 +139,10 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
 			constantValue(0),
 			// No `wrap()` needed here, because -2**255 / -1 results
 			// in 2**255 which is "converted" to its two's complement
-			// representation 2**255 in `signedToUnsigned`
+			// representation 2**255 in `signedToTwosComplement`
-			signedToUnsigned(smtutil::signedDivisionEVM(
+			signedToTwosComplement(smtutil::signedDivisionEVM(
-				unsignedToSigned(arguments.at(0)),
+				twosComplementToSigned(arguments.at(0)),
-				unsignedToSigned(arguments.at(1))
+				twosComplementToSigned(arguments.at(1))
 			))
 		);
 	case evmasm::Instruction::MOD:
@@ -188,19 +155,19 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
 		return smtutil::Expression::ite(
 			arguments.at(1) == constantValue(0),
 			constantValue(0),
-			signedToUnsigned(signedModuloEVM(
+			signedToTwosComplement(signedModuloEVM(
-				unsignedToSigned(arguments.at(0)),
+				twosComplementToSigned(arguments.at(0)),
-				unsignedToSigned(arguments.at(1))
+				twosComplementToSigned(arguments.at(1))
 			))
 		);
 	case evmasm::Instruction::LT:
 		return booleanValue(arguments.at(0) < arguments.at(1));
 	case evmasm::Instruction::SLT:
-		return booleanValue(unsignedToSigned(arguments.at(0)) < unsignedToSigned(arguments.at(1)));
+		return booleanValue(twosComplementToSigned(arguments.at(0)) < twosComplementToSigned(arguments.at(1)));
 	case evmasm::Instruction::GT:
 		return booleanValue(arguments.at(0) > arguments.at(1));
 	case evmasm::Instruction::SGT:
-		return booleanValue(unsignedToSigned(arguments.at(0)) > unsignedToSigned(arguments.at(1)));
+		return booleanValue(twosComplementToSigned(arguments.at(0)) > twosComplementToSigned(arguments.at(1)));
 	case evmasm::Instruction::EQ:
 		return booleanValue(arguments.at(0) == arguments.at(1));
 	case evmasm::Instruction::ISZERO:
@@ -259,76 +226,3 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
 	}
 	return newRestrictedVariable();
 }
-
-smtutil::Expression ReasoningBasedSimplifier::int2bv(smtutil::Expression _arg) const
-{
-	return smtutil::Expression::int2bv(std::move(_arg), 256);
-}
-
-smtutil::Expression ReasoningBasedSimplifier::bv2int(smtutil::Expression _arg) const
-{
-	return smtutil::Expression::bv2int(std::move(_arg));
-}
-
-smtutil::Expression ReasoningBasedSimplifier::newVariable()
-{
-	return m_solver->newVariable(uniqueName(), defaultSort());
-}
-
-smtutil::Expression ReasoningBasedSimplifier::newRestrictedVariable()
-{
-	smtutil::Expression var = newVariable();
-	m_solver->addAssertion(0 <= var && var < smtutil::Expression(bigint(1) << 256));
-	return var;
-}
-
-string ReasoningBasedSimplifier::uniqueName()
-{
-	return "expr_" + to_string(m_varCounter++);
-}
-
-shared_ptr<Sort> ReasoningBasedSimplifier::defaultSort() const
-{
-	return SortProvider::intSort();
-}
-
-smtutil::Expression ReasoningBasedSimplifier::booleanValue(smtutil::Expression _value) const
-{
-	return smtutil::Expression::ite(_value, constantValue(1), constantValue(0));
-}
-
-smtutil::Expression ReasoningBasedSimplifier::constantValue(size_t _value) const
-{
-	return _value;
-}
-
-smtutil::Expression ReasoningBasedSimplifier::literalValue(Literal const& _literal) const
-{
-	return smtutil::Expression(valueOfLiteral(_literal));
-}
-
-smtutil::Expression ReasoningBasedSimplifier::unsignedToSigned(smtutil::Expression _value)
-{
-	return smtutil::Expression::ite(
-		_value < smtutil::Expression(bigint(1) << 255),
-		_value,
-		_value - smtutil::Expression(bigint(1) << 256)
-	);
-}
-
-smtutil::Expression ReasoningBasedSimplifier::signedToUnsigned(smtutil::Expression _value)
-{
-	return smtutil::Expression::ite(
-		_value >= 0,
-		_value,
-		_value + smtutil::Expression(bigint(1) << 256)
-	);
-}
-
-smtutil::Expression ReasoningBasedSimplifier::wrap(smtutil::Expression _value)
-{
-	smtutil::Expression rest = newRestrictedVariable();
-	smtutil::Expression multiplier = newVariable();
-	m_solver->addAssertion(_value == multiplier * smtutil::Expression(bigint(1) << 256) + rest);
-	return rest;
-}

libyul/optimiser/ReasoningBasedSimplifier.h

@@ -16,6 +16,7 @@
 */
 #pragma once
 
+#include <libyul/optimiser/SMTSolver.h>
 #include <libyul/optimiser/ASTWalker.h>
 #include <libyul/optimiser/OptimiserStep.h>
 #include <libyul/Dialect.h>
@@ -46,7 +47,7 @@ namespace solidity::yul
  *
  * Prerequisite: Disambiguator, SSATransform.
  */
-class ReasoningBasedSimplifier: public ASTModifier
+class ReasoningBasedSimplifier: public ASTModifier, SMTSolver
 {
 public:
 	static constexpr char const* name{"ReasoningBasedSimplifier"};
@@ -63,36 +64,12 @@ private:
 		std::set<YulString> const& _ssaVariables
 	);
 
-	smtutil::Expression encodeExpression(
+	smtutil::Expression encodeEVMBuiltin(
-		Expression const& _expression
-	);
-
-	virtual smtutil::Expression encodeEVMBuiltin(
 		evmasm::Instruction _instruction,
 		std::vector<Expression> const& _arguments
-	);
+	) override;
-
-	smtutil::Expression int2bv(smtutil::Expression _arg) const;
-	smtutil::Expression bv2int(smtutil::Expression _arg) const;
-
-	smtutil::Expression newVariable();
-	virtual smtutil::Expression newRestrictedVariable();
-	std::string uniqueName();
-
-	virtual std::shared_ptr<smtutil::Sort> defaultSort() const;
-	virtual smtutil::Expression booleanValue(smtutil::Expression _value) const;
-	virtual smtutil::Expression constantValue(size_t _value) const;
-	virtual smtutil::Expression literalValue(Literal const& _literal) const;
-	virtual smtutil::Expression unsignedToSigned(smtutil::Expression _value);
-	virtual smtutil::Expression signedToUnsigned(smtutil::Expression _value);
-	virtual smtutil::Expression wrap(smtutil::Expression _value);
 
 	Dialect const& m_dialect;
-	std::set<YulString> const& m_ssaVariables;
-	std::unique_ptr<smtutil::SolverInterface> m_solver;
-	std::map<YulString, smtutil::Expression> m_variables;
-
-	size_t m_varCounter = 0;
 };
 
 }

libyul/optimiser/SMTSolver.cpp

@@ -0,0 +1,160 @@
+/*
+	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 <libyul/optimiser/SMTSolver.h>
+#include <libyul/optimiser/OptimizerUtilities.h>
+
+#include <libyul/AST.h>
+#include <libyul/Utilities.h>
+
+#include <libsolutil/Visitor.h>
+#include <libsolutil/CommonData.h>
+
+#include <libsmtutil/SMTPortfolio.h>
+#include <libsmtutil/Helpers.h>
+
+using namespace solidity::yul;
+using namespace solidity::util;
+using namespace solidity::smtutil;
+using namespace solidity;
+using namespace std;
+
+SMTSolver::SMTSolver(set<YulString> const& _ssaVariables, Dialect const& _dialect):
+	m_ssaVariables(_ssaVariables),
+	m_solver(make_unique<smtutil::SMTPortfolio>()),
+	m_dialect(_dialect)
+{ }
+
+smtutil::Expression SMTSolver::encodeExpression(Expression const& _expression)
+{
+	return std::visit(GenericVisitor{
+		[&](FunctionCall const& _functionCall)
+		{
+			if (auto instruction = toEVMInstruction(m_dialect, _functionCall.functionName.name))
+				return encodeEVMBuiltin(*instruction, _functionCall.arguments);
+
+			return newRestrictedVariable();
+		},
+		[&](Identifier const& _identifier)
+		{
+			if (
+				m_ssaVariables.count(_identifier.name) &&
+				m_variables.count(_identifier.name)
+			)
+				return m_variables.at(_identifier.name);
+			else
+				return newRestrictedVariable();
+		},
+		[&](Literal const& _literal)
+		{
+			return literalValue(_literal);
+		}
+	}, _expression);
+}
+
+smtutil::Expression SMTSolver::int2bv(smtutil::Expression _arg)
+{
+	return smtutil::Expression::int2bv(std::move(_arg), 256);
+}
+
+smtutil::Expression SMTSolver::bv2int(smtutil::Expression _arg)
+{
+	return smtutil::Expression::bv2int(std::move(_arg));
+}
+
+smtutil::Expression SMTSolver::newVariable()
+{
+	return m_solver->newVariable(uniqueName(), defaultSort());
+}
+
+smtutil::Expression SMTSolver::newRestrictedVariable(bigint _maxValue)
+{
+	smtutil::Expression var = newVariable();
+	m_solver->addAssertion(0 <= var && var <= smtutil::Expression(_maxValue));
+	return var;
+}
+
+string SMTSolver::uniqueName()
+{
+	return "expr_" + to_string(m_varCounter++);
+}
+
+shared_ptr<Sort> SMTSolver::defaultSort() const
+{
+	return SortProvider::intSort();
+}
+
+smtutil::Expression SMTSolver::booleanValue(smtutil::Expression _value)
+{
+	return smtutil::Expression::ite(_value, constantValue(1), constantValue(0));
+}
+
+smtutil::Expression SMTSolver::constantValue(bigint _value)
+{
+	return _value;
+}
+
+smtutil::Expression SMTSolver::literalValue(Literal const& _literal)
+{
+	return smtutil::Expression(valueOfLiteral(_literal));
+}
+
+smtutil::Expression SMTSolver::twosComplementToSigned(smtutil::Expression _value)
+{
+	return smtutil::Expression::ite(
+		_value < smtutil::Expression(bigint(1) << 255),
+		_value,
+		_value - smtutil::Expression(bigint(1) << 256)
+	);
+}
+
+smtutil::Expression SMTSolver::signedToTwosComplement(smtutil::Expression _value)
+{
+	return smtutil::Expression::ite(
+		_value >= 0,
+		_value,
+		_value + smtutil::Expression(bigint(1) << 256)
+	);
+}
+
+smtutil::Expression SMTSolver::wrap(smtutil::Expression _value)
+{
+	smtutil::Expression rest = newRestrictedVariable();
+	smtutil::Expression multiplier = newVariable();
+	m_solver->addAssertion(_value == multiplier * smtutil::Expression(bigint(1) << 256) + rest);
+	return rest;
+}
+
+void SMTSolver::encodeVariableDeclaration(VariableDeclaration const& _varDecl)
+{
+	if (
+		_varDecl.variables.size() == 1 &&
+		_varDecl.value &&
+		m_ssaVariables.count(_varDecl.variables.front().name)
+	)
+	{
+		YulString const& variableName = _varDecl.variables.front().name;
+		bool const inserted = m_variables.insert({
+			variableName,
+			m_solver->newVariable("yul_" + variableName.str(), defaultSort())
+		}).second;
+		yulAssert(inserted, "");
+		m_solver->addAssertion(
+			m_variables.at(variableName) == encodeExpression(*_varDecl.value)
+		);
+	}
+}

libyul/optimiser/SMTSolver.h

@@ -0,0 +1,92 @@
+/*
+	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 <libyul/AST.h>
+#include <libyul/Dialect.h>
+#include <libyul/Exceptions.h>
+
+// because of instruction
+#include <libyul/backends/evm/EVMDialect.h>
+
+#include <libsmtutil/SolverInterface.h>
+
+#include <memory>
+
+namespace solidity::smtutil
+{
+
+class SolverInterface;
+class Expression;
+struct Sort;
+
+}
+
+namespace solidity::yul
+{
+
+/**
+ * Base class for SMT based optimization steps.
+ *
+ * Works best when used with AST in SSA form.
+ */
+class SMTSolver
+{
+protected:
+	SMTSolver(
+		std::set<YulString> const& _ssaVariables,
+		Dialect const& _dialect
+	);
+
+	/// Helper function that encodes VariableDeclaration
+	void encodeVariableDeclaration(VariableDeclaration const& _varDecl);
+
+	/// The encoding for a builtin. The type of encoding determines what we are
+	/// solving for.
+	virtual smtutil::Expression encodeEVMBuiltin(
+		evmasm::Instruction _instruction,
+		std::vector<Expression> const& _arguments
+	) = 0;
+
+	smtutil::Expression encodeExpression(Expression const& _expression);
+
+	static smtutil::Expression int2bv(smtutil::Expression _arg);
+	static smtutil::Expression bv2int(smtutil::Expression _arg);
+
+	smtutil::Expression newVariable();
+	virtual smtutil::Expression newRestrictedVariable(bigint _maxValue = (bigint(1) << 256) - 1);
+	std::string uniqueName();
+
+	virtual std::shared_ptr<smtutil::Sort> defaultSort() const;
+	static smtutil::Expression booleanValue(smtutil::Expression _value);
+	static smtutil::Expression constantValue(bigint _value);
+	static smtutil::Expression literalValue(Literal const& _literal);
+	static smtutil::Expression twosComplementToSigned(smtutil::Expression _value);
+	static smtutil::Expression signedToTwosComplement(smtutil::Expression _value);
+	smtutil::Expression wrap(smtutil::Expression _value);
+
+	std::set<YulString> const& m_ssaVariables;
+	std::unique_ptr<smtutil::SolverInterface> m_solver;
+	std::map<YulString, smtutil::Expression> m_variables;
+
+	Dialect const& m_dialect;
+
+private:
+	size_t m_varCounter = 0;
+};
+
+}