From 39b23420ec93d7e0f72ef53dea103c9bc3af9c8e Mon Sep 17 00:00:00 2001 From: hrkrshnn Date: Thu, 6 May 2021 11:22:35 +0200 Subject: [PATCH] Extracted the class SMT Solver from ReasoningBasedSimplifier --- libyul/CMakeLists.txt | 2 + libyul/optimiser/ReasoningBasedSimplifier.cpp | 132 ++------------- libyul/optimiser/ReasoningBasedSimplifier.h | 31 +--- libyul/optimiser/SMTSolver.cpp | 160 ++++++++++++++++++ libyul/optimiser/SMTSolver.h | 92 ++++++++++ 5 files changed, 271 insertions(+), 146 deletions(-) create mode 100644 libyul/optimiser/SMTSolver.cpp create mode 100644 libyul/optimiser/SMTSolver.h diff --git a/libyul/CMakeLists.txt b/libyul/CMakeLists.txt index 77d09706a..80c83ebc2 100644 --- a/libyul/CMakeLists.txt +++ b/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 diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp index e75ca3cf5..96924a06d 100644 --- a/libyul/optimiser/ReasoningBasedSimplifier.cpp +++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp @@ -16,8 +16,8 @@ */ #include +#include -#include #include #include #include @@ -56,14 +56,7 @@ std::optional ReasoningBasedSimplifier::invalidInCurrentEnvironment() void ReasoningBasedSimplifier::operator()(VariableDeclaration& _varDecl) { - if (_varDecl.variables.size() != 1 || !_varDecl.value) - 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)); + SMTSolver::encodeVariableDeclaration(_varDecl); } void ReasoningBasedSimplifier::operator()(If& _if) @@ -111,37 +104,11 @@ ReasoningBasedSimplifier::ReasoningBasedSimplifier( Dialect const& _dialect, set const& _ssaVariables ): - m_dialect(_dialect), - m_ssaVariables(_ssaVariables), - m_solver(make_unique()) + SMTSolver(_ssaVariables, _dialect), + m_dialect(_dialect) { } -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` - signedToUnsigned(smtutil::signedDivisionEVM( - unsignedToSigned(arguments.at(0)), - unsignedToSigned(arguments.at(1)) + // representation 2**255 in `signedToTwosComplement` + signedToTwosComplement(smtutil::signedDivisionEVM( + twosComplementToSigned(arguments.at(0)), + 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( - unsignedToSigned(arguments.at(0)), - unsignedToSigned(arguments.at(1)) + signedToTwosComplement(signedModuloEVM( + twosComplementToSigned(arguments.at(0)), + 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 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; -} diff --git a/libyul/optimiser/ReasoningBasedSimplifier.h b/libyul/optimiser/ReasoningBasedSimplifier.h index 18fcf3583..c458a36d0 100644 --- a/libyul/optimiser/ReasoningBasedSimplifier.h +++ b/libyul/optimiser/ReasoningBasedSimplifier.h @@ -16,6 +16,7 @@ */ #pragma once +#include #include #include #include @@ -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 const& _ssaVariables ); - smtutil::Expression encodeExpression( - Expression const& _expression - ); - - virtual smtutil::Expression encodeEVMBuiltin( + smtutil::Expression encodeEVMBuiltin( evmasm::Instruction _instruction, std::vector const& _arguments - ); - - 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 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); + ) override; Dialect const& m_dialect; - std::set const& m_ssaVariables; - std::unique_ptr m_solver; - std::map m_variables; - - size_t m_varCounter = 0; }; } diff --git a/libyul/optimiser/SMTSolver.cpp b/libyul/optimiser/SMTSolver.cpp new file mode 100644 index 000000000..c0c6bcb5e --- /dev/null +++ b/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 . +*/ + +#include +#include + +#include +#include + +#include +#include + +#include +#include + +using namespace solidity::yul; +using namespace solidity::util; +using namespace solidity::smtutil; +using namespace solidity; +using namespace std; + +SMTSolver::SMTSolver(set const& _ssaVariables, Dialect const& _dialect): + m_ssaVariables(_ssaVariables), + m_solver(make_unique()), + 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 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) + ); + } +} diff --git a/libyul/optimiser/SMTSolver.h b/libyul/optimiser/SMTSolver.h new file mode 100644 index 000000000..d92a84c1d --- /dev/null +++ b/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 . +*/ +#pragma once + +#include +#include +#include + +// because of instruction +#include + +#include + +#include + +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 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 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 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 const& m_ssaVariables; + std::unique_ptr m_solver; + std::map m_variables; + + Dialect const& m_dialect; + +private: + size_t m_varCounter = 0; +}; + +}