From 29041c8101d13a5e4372e9c2b94e83a5e254d66e Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Tue, 27 Jun 2023 17:42:06 +0200 Subject: [PATCH] Remove ReasoningBasedSimplifier from libyul Due to a design decision to move away from a bundled SMT solver, ReasoningBasedSimplifier in its current form cannot be use any longer. This is a necessary step to allow a unified way to call solvers using only SMTLIB interface. Since this optimization pass has always been marked as highly experimental and never turned on by default, it should be OK to remove it. --- Changelog.md | 1 + docs/internals/optimizer.rst | 21 -- libyul/CMakeLists.txt | 4 - libyul/optimiser/ReasoningBasedSimplifier.cpp | 228 ------------------ libyul/optimiser/ReasoningBasedSimplifier.h | 75 ------ libyul/optimiser/SMTSolver.cpp | 160 ------------ libyul/optimiser/SMTSolver.h | 92 ------- libyul/optimiser/Suite.cpp | 3 - test/libyul/YulOptimizerTest.cpp | 7 - test/libyul/YulOptimizerTestCommon.cpp | 8 +- .../reasoningBasedSimplifier/arith.yul | 13 - .../arith_movable.yul | 19 -- .../arith_non_movable.yul | 23 -- .../reasoningBasedSimplifier/mulcheck.yul | 32 --- .../reasoningBasedSimplifier/mulmod.yul | 31 --- .../negative_rounding.yul | 16 -- .../reasoningBasedSimplifier/nested.yul | 26 -- .../signed_division.yul | 31 --- .../reasoningBasedSimplifier/smod.yul | 53 ---- .../reasoningBasedSimplifier/smoke.yul | 5 - .../reasoningBasedSimplifier/wrapping.yul | 15 -- test/tools/yulopti.cpp | 1 - test/yulPhaser/Chromosome.cpp | 2 +- 23 files changed, 3 insertions(+), 863 deletions(-) delete mode 100644 libyul/optimiser/ReasoningBasedSimplifier.cpp delete mode 100644 libyul/optimiser/ReasoningBasedSimplifier.h delete mode 100644 libyul/optimiser/SMTSolver.cpp delete mode 100644 libyul/optimiser/SMTSolver.h delete mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul delete mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_movable.yul delete mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_non_movable.yul delete mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul delete mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul delete mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul delete mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul delete mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul delete mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul delete mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smoke.yul delete mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul diff --git a/Changelog.md b/Changelog.md index 69bd02624..2ddf6647e 100644 --- a/Changelog.md +++ b/Changelog.md @@ -12,6 +12,7 @@ Compiler Features: * SMTChecker: Add ``--model-checker-print-query`` CLI option and ``settings.modelChecker.printQuery`` JSON option to output the SMTChecker queries in the SMTLIB2 format. This requires using `smtlib2` solver only. * Standard JSON Interface: Add ``ast`` file-level output for Yul input. * Standard JSON Interface: Add ``irAst`` and ``irOptimizedAst`` contract-level outputs for Solidity input, providing AST in compact JSON format for IR and optimized IR. + * Yul Optimizer: Remove experimental `ReasoningBasedSimplifier` optimization step. * Yul Optimizer: Stack-to-memory mover is now enabled by default whenever possible for via IR code generation and pure Yul compilation. diff --git a/docs/internals/optimizer.rst b/docs/internals/optimizer.rst index d3df1b600..cd4624a1a 100644 --- a/docs/internals/optimizer.rst +++ b/docs/internals/optimizer.rst @@ -316,7 +316,6 @@ Abbreviation Full name ``L`` :ref:`load-resolver` ``M`` :ref:`loop-invariant-code-motion` ``r`` :ref:`redundant-assign-eliminator` -``R`` :ref:`reasoning-based-simplifier` - highly experimental ``m`` :ref:`rematerialiser` ``V`` :ref:`SSA-reverser` ``a`` :ref:`SSA-transform` @@ -330,10 +329,6 @@ Abbreviation Full name Some steps depend on properties ensured by ``BlockFlattener``, ``FunctionGrouper``, ``ForLoopInitRewriter``. For this reason the Yul optimizer always applies them before applying any steps supplied by the user. -The ReasoningBasedSimplifier is an optimizer step that is currently not enabled -in the default set of steps. It uses an SMT solver to simplify arithmetic expressions -and boolean conditions. It has not received thorough testing or validation yet and can produce -non-reproducible results, so please use with care! Selecting Optimizations ----------------------- @@ -863,22 +858,6 @@ Works best if the code is in SSA form. Prerequisite: Disambiguator, ForLoopInitRewriter. -.. _reasoning-based-simplifier: - -ReasoningBasedSimplifier -^^^^^^^^^^^^^^^^^^^^^^^^ - -This optimizer uses SMT solvers to check whether ``if`` conditions are constant. - -- If ``constraints AND condition`` is UNSAT, the condition is never true and the whole body can be removed. -- If ``constraints AND NOT condition`` is UNSAT, the condition is always true and can be replaced by ``1``. - -The simplifications above can only be applied if the condition is movable. - -It is only effective on the EVM dialect, but safe to use on other dialects. - -Prerequisite: Disambiguator, SSATransform. - Statement-Scale Simplifications ------------------------------- diff --git a/libyul/CMakeLists.txt b/libyul/CMakeLists.txt index 2cf02f838..0bb98e467 100644 --- a/libyul/CMakeLists.txt +++ b/libyul/CMakeLists.txt @@ -143,8 +143,6 @@ add_library(yul optimiser/OptimiserStep.h optimiser/OptimizerUtilities.cpp optimiser/OptimizerUtilities.h - optimiser/ReasoningBasedSimplifier.cpp - optimiser/ReasoningBasedSimplifier.h optimiser/UnusedAssignEliminator.cpp optimiser/UnusedAssignEliminator.h optimiser/UnusedStoreBase.cpp @@ -153,8 +151,6 @@ add_library(yul optimiser/UnusedStoreEliminator.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 deleted file mode 100644 index 24882d84e..000000000 --- a/libyul/optimiser/ReasoningBasedSimplifier.cpp +++ /dev/null @@ -1,228 +0,0 @@ -/* - 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 - -#include - -#include - -#include -#include - -using namespace std; -using namespace solidity; -using namespace solidity::util; -using namespace solidity::yul; -using namespace solidity::smtutil; - -void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _ast) -{ - set ssaVars = SSAValueTracker::ssaVariables(_ast); - ReasoningBasedSimplifier{_context.dialect, ssaVars}(_ast); -} - -std::optional ReasoningBasedSimplifier::invalidInCurrentEnvironment() -{ - // SMTLib2 interface is always available, but we would like to have synchronous answers. - if (smtutil::SMTPortfolio{}.solvers() <= 1) - return string{"No SMT solvers available."}; - else - return nullopt; -} - -void ReasoningBasedSimplifier::operator()(VariableDeclaration& _varDecl) -{ - SMTSolver::encodeVariableDeclaration(_varDecl); -} - -void ReasoningBasedSimplifier::operator()(If& _if) -{ - if (!SideEffectsCollector{m_dialect, *_if.condition}.movable()) - return; - - smtutil::Expression condition = encodeExpression(*_if.condition); - m_solver->push(); - m_solver->addAssertion(condition == constantValue(0)); - CheckResult result = m_solver->check({}).first; - m_solver->pop(); - if (result == CheckResult::UNSATISFIABLE) - { - Literal trueCondition = m_dialect.trueLiteral(); - trueCondition.debugData = debugDataOf(*_if.condition); - _if.condition = make_unique(std::move(trueCondition)); - } - else - { - m_solver->push(); - m_solver->addAssertion(condition != constantValue(0)); - CheckResult result2 = m_solver->check({}).first; - m_solver->pop(); - if (result2 == CheckResult::UNSATISFIABLE) - { - Literal falseCondition = m_dialect.zeroLiteralForType(m_dialect.boolType); - falseCondition.debugData = debugDataOf(*_if.condition); - _if.condition = make_unique(std::move(falseCondition)); - _if.body = yul::Block{}; - // Nothing left to be done. - return; - } - } - - m_solver->push(); - m_solver->addAssertion(condition != constantValue(0)); - - ASTModifier::operator()(_if.body); - - m_solver->pop(); -} - -ReasoningBasedSimplifier::ReasoningBasedSimplifier( - Dialect const& _dialect, - set const& _ssaVariables -): - SMTSolver(_ssaVariables, _dialect), - m_dialect(_dialect) -{ -} - - -smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin( - evmasm::Instruction _instruction, - vector const& _arguments -) -{ - vector arguments = applyMap( - _arguments, - [this](yul::Expression const& _expr) { return encodeExpression(_expr); } - ); - switch (_instruction) - { - case evmasm::Instruction::ADD: - return wrap(arguments.at(0) + arguments.at(1)); - case evmasm::Instruction::MUL: - return wrap(arguments.at(0) * arguments.at(1)); - case evmasm::Instruction::SUB: - return wrap(arguments.at(0) - arguments.at(1)); - case evmasm::Instruction::DIV: - return smtutil::Expression::ite( - arguments.at(1) == constantValue(0), - constantValue(0), - arguments.at(0) / arguments.at(1) - ); - case evmasm::Instruction::SDIV: - return smtutil::Expression::ite( - arguments.at(1) == constantValue(0), - 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 `signedToTwosComplement` - signedToTwosComplement(smtutil::signedDivisionEVM( - twosComplementToSigned(arguments.at(0)), - twosComplementToSigned(arguments.at(1)) - )) - ); - case evmasm::Instruction::MOD: - return smtutil::Expression::ite( - arguments.at(1) == constantValue(0), - constantValue(0), - arguments.at(0) % arguments.at(1) - ); - case evmasm::Instruction::SMOD: - return smtutil::Expression::ite( - arguments.at(1) == constantValue(0), - constantValue(0), - 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(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(twosComplementToSigned(arguments.at(0)) > twosComplementToSigned(arguments.at(1))); - case evmasm::Instruction::EQ: - return booleanValue(arguments.at(0) == arguments.at(1)); - case evmasm::Instruction::ISZERO: - return booleanValue(arguments.at(0) == constantValue(0)); - case evmasm::Instruction::AND: - return smtutil::Expression::ite( - (arguments.at(0) == 0 || arguments.at(0) == 1) && - (arguments.at(1) == 0 || arguments.at(1) == 1), - booleanValue(arguments.at(0) == 1 && arguments.at(1) == 1), - bv2int(int2bv(arguments.at(0)) & int2bv(arguments.at(1))) - ); - case evmasm::Instruction::OR: - return smtutil::Expression::ite( - (arguments.at(0) == 0 || arguments.at(0) == 1) && - (arguments.at(1) == 0 || arguments.at(1) == 1), - booleanValue(arguments.at(0) == 1 || arguments.at(1) == 1), - bv2int(int2bv(arguments.at(0)) | int2bv(arguments.at(1))) - ); - case evmasm::Instruction::XOR: - return bv2int(int2bv(arguments.at(0)) ^ int2bv(arguments.at(1))); - case evmasm::Instruction::NOT: - return smtutil::Expression(u256(-1)) - arguments.at(0); - case evmasm::Instruction::SHL: - return smtutil::Expression::ite( - arguments.at(0) > 255, - constantValue(0), - bv2int(int2bv(arguments.at(1)) << int2bv(arguments.at(0))) - ); - case evmasm::Instruction::SHR: - return smtutil::Expression::ite( - arguments.at(0) > 255, - constantValue(0), - bv2int(int2bv(arguments.at(1)) >> int2bv(arguments.at(0))) - ); - case evmasm::Instruction::SAR: - return smtutil::Expression::ite( - arguments.at(0) > 255, - constantValue(0), - bv2int(smtutil::Expression::ashr(int2bv(arguments.at(1)), int2bv(arguments.at(0)))) - ); - case evmasm::Instruction::ADDMOD: - return smtutil::Expression::ite( - arguments.at(2) == constantValue(0), - constantValue(0), - (arguments.at(0) + arguments.at(1)) % arguments.at(2) - ); - case evmasm::Instruction::MULMOD: - return smtutil::Expression::ite( - arguments.at(2) == constantValue(0), - constantValue(0), - (arguments.at(0) * arguments.at(1)) % arguments.at(2) - ); - // TODO SIGNEXTEND - default: - break; - } - return newRestrictedVariable(); -} diff --git a/libyul/optimiser/ReasoningBasedSimplifier.h b/libyul/optimiser/ReasoningBasedSimplifier.h deleted file mode 100644 index c458a36d0..000000000 --- a/libyul/optimiser/ReasoningBasedSimplifier.h +++ /dev/null @@ -1,75 +0,0 @@ -/* - 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 -#include - -// because of instruction -#include - -#include - -namespace solidity::smtutil -{ -class SolverInterface; -class Expression; -struct Sort; -} - -namespace solidity::yul -{ - -/** - * Reasoning-based simplifier. - * This optimizer uses SMT solvers to check whether `if` conditions are constant. - * - If `constraints AND condition` is UNSAT, the condition is never true and the whole body can be removed. - * - If `constraints AND NOT condition` is UNSAT, the condition is always true and can be replaced by `1`. - * The simplifications above can only be applied if the condition is movable. - * - * It is only effective on the EVM dialect, but safe to use on other dialects. - * - * Prerequisite: Disambiguator, SSATransform. - */ -class ReasoningBasedSimplifier: public ASTModifier, SMTSolver -{ -public: - static constexpr char const* name{"ReasoningBasedSimplifier"}; - static void run(OptimiserStepContext& _context, Block& _ast); - static std::optional invalidInCurrentEnvironment(); - - using ASTModifier::operator(); - void operator()(VariableDeclaration& _varDecl) override; - void operator()(If& _if) override; - -private: - explicit ReasoningBasedSimplifier( - Dialect const& _dialect, - std::set const& _ssaVariables - ); - - smtutil::Expression encodeEVMBuiltin( - evmasm::Instruction _instruction, - std::vector const& _arguments - ) override; - - Dialect const& m_dialect; -}; - -} diff --git a/libyul/optimiser/SMTSolver.cpp b/libyul/optimiser/SMTSolver.cpp deleted file mode 100644 index c0c6bcb5e..000000000 --- a/libyul/optimiser/SMTSolver.cpp +++ /dev/null @@ -1,160 +0,0 @@ -/* - 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 deleted file mode 100644 index d92a84c1d..000000000 --- a/libyul/optimiser/SMTSolver.h +++ /dev/null @@ -1,92 +0,0 @@ -/* - 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; -}; - -} diff --git a/libyul/optimiser/Suite.cpp b/libyul/optimiser/Suite.cpp index e29112b01..bd966e5d3 100644 --- a/libyul/optimiser/Suite.cpp +++ b/libyul/optimiser/Suite.cpp @@ -43,7 +43,6 @@ #include #include #include -#include #include #include #include @@ -272,7 +271,6 @@ map> const& OptimiserSuite::allSteps() LoopInvariantCodeMotion, UnusedAssignEliminator, UnusedStoreEliminator, - ReasoningBasedSimplifier, Rematerialiser, SSAReverser, SSATransform, @@ -312,7 +310,6 @@ map const& OptimiserSuite::stepNameToAbbreviationMap() {LiteralRematerialiser::name, 'T'}, {LoadResolver::name, 'L'}, {LoopInvariantCodeMotion::name, 'M'}, - {ReasoningBasedSimplifier::name, 'R'}, {UnusedAssignEliminator::name, 'r'}, {UnusedStoreEliminator::name, 'S'}, {Rematerialiser::name, 'm'}, diff --git a/test/libyul/YulOptimizerTest.cpp b/test/libyul/YulOptimizerTest.cpp index 6404fa7c6..b50bcb38e 100644 --- a/test/libyul/YulOptimizerTest.cpp +++ b/test/libyul/YulOptimizerTest.cpp @@ -24,7 +24,6 @@ #include #include -#include #include #include @@ -53,12 +52,6 @@ YulOptimizerTest::YulOptimizerTest(string const& _filename): BOOST_THROW_EXCEPTION(runtime_error("Filename path has to contain a directory: \"" + _filename + "\".")); m_optimizerStep = std::prev(std::prev(path.end()))->string(); - if (m_optimizerStep == "reasoningBasedSimplifier" && ( - solidity::test::CommonOptions::get().disableSMT || - ReasoningBasedSimplifier::invalidInCurrentEnvironment() - )) - m_shouldRun = false; - m_source = m_reader.source(); auto dialectName = m_reader.stringSetting("dialect", "evm"); diff --git a/test/libyul/YulOptimizerTestCommon.cpp b/test/libyul/YulOptimizerTestCommon.cpp index 48c7ea403..ed29f339c 100644 --- a/test/libyul/YulOptimizerTestCommon.cpp +++ b/test/libyul/YulOptimizerTestCommon.cpp @@ -49,7 +49,6 @@ #include #include #include -#include #include #include #include @@ -289,10 +288,6 @@ YulOptimizerTestCommon::YulOptimizerTestCommon( LiteralRematerialiser::run(*m_context, *m_ast); StructuralSimplifier::run(*m_context, *m_ast); }}, - {"reasoningBasedSimplifier", [&]() { - disambiguate(); - ReasoningBasedSimplifier::run(*m_context, *m_object->code); - }}, {"equivalentFunctionCombiner", [&]() { disambiguate(); ForLoopInitRewriter::run(*m_context, *m_ast); @@ -424,8 +419,7 @@ string YulOptimizerTestCommon::randomOptimiserStep(unsigned _seed) // it can sometimes drain memory. if ( optimiserStep == "mainFunction" || - optimiserStep == "wordSizeTransform" || - optimiserStep == "reasoningBasedSimplifier" + optimiserStep == "wordSizeTransform" ) // "Fullsuite" is fuzzed roughly four times more frequently than // other steps because of the filtering in place above. diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul deleted file mode 100644 index 7ff930766..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul +++ /dev/null @@ -1,13 +0,0 @@ -{ - let x := 7 - let y := 8 - if eq(add(x, y), 15) { } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// let x := 7 -// let y := 8 -// if 1 { } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_movable.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_movable.yul deleted file mode 100644 index 2080a678c..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_movable.yul +++ /dev/null @@ -1,19 +0,0 @@ -{ - function f() -> z - { - z := 15 - } - let x := 7 - let y := 8 - if eq(add(x, y), f()) { } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// function f() -> z -// { z := 15 } -// let x := 7 -// let y := 8 -// if eq(add(x, y), f()) { } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_non_movable.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_non_movable.yul deleted file mode 100644 index ed50224d0..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_non_movable.yul +++ /dev/null @@ -1,23 +0,0 @@ -{ - function f() -> z - { - sstore(1, 15) - z := 15 - } - let x := 7 - let y := 8 - if eq(add(x, y), f()) { } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// function f() -> z -// { -// sstore(1, 15) -// z := 15 -// } -// let x := 7 -// let y := 8 -// if eq(add(x, y), f()) { } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul deleted file mode 100644 index 31a342339..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul +++ /dev/null @@ -1,32 +0,0 @@ -{ - let vloc_x := calldataload(0) - let vloc_y := calldataload(1) - if lt(vloc_x, shl(100, 1)) { - if lt(vloc_y, shl(100, 1)) { - if iszero(and(iszero(iszero(vloc_x)), gt(vloc_y, div(not(0), vloc_x)))) { - let vloc := mul(vloc_x, vloc_y) - sstore(0, vloc) - } - } - } -} -// ==== -// EVMVersion: >=constantinople -// ---- -// step: reasoningBasedSimplifier -// -// { -// let vloc_x := calldataload(0) -// let vloc_y := calldataload(1) -// if lt(vloc_x, shl(100, 1)) -// { -// if lt(vloc_y, shl(100, 1)) -// { -// if 1 -// { -// let vloc := mul(vloc_x, vloc_y) -// sstore(0, vloc) -// } -// } -// } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul deleted file mode 100644 index f5226acf7..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul +++ /dev/null @@ -1,31 +0,0 @@ -{ - let x := calldataload(0) - let y := calldataload(32) - let z := calldataload(64) - let result := mulmod(x, y, z) - - // should be zero - if gt(result, z) { sstore(0, 1) } - - // mulmod is equal to mod of product for small numbers - if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { - if eq(result, mod(mul(x, y), z)) { sstore(0, 9) } - } - - // but not in general - if and(and(gt(x, sub(0, 5)), eq(y, 2)), eq(z, 3)) { - if eq(result, mod(mul(x, y), z)) { sstore(0, 5) } - } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// let x := calldataload(0) -// let y := calldataload(32) -// let z := calldataload(64) -// let result := mulmod(x, y, z) -// if 0 { } -// if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { if 1 { sstore(0, 9) } } -// if and(and(gt(x, sub(0, 5)), eq(y, 2)), eq(z, 3)) { if 0 { } } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul deleted file mode 100644 index 6e4b3f5ed..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul +++ /dev/null @@ -1,16 +0,0 @@ -{ - let x := sub(0, 7) - let y := 2 - // (-7)/2 == -3 on the evm - if iszero(add(sdiv(x, y), 3)) { } - if iszero(add(sdiv(x, y), 4)) { } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// let x := sub(0, 7) -// let y := 2 -// if 1 { } -// if 0 { } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul deleted file mode 100644 index d7002c99b..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul +++ /dev/null @@ -1,26 +0,0 @@ -{ - let x := calldataload(2) - let t := lt(x, 20) - if t { - if lt(x, 21) { } - if lt(x, 20) { } - if lt(x, 19) { } - if gt(x, 20) { } - if iszero(gt(x, 20)) { } - } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// let x := calldataload(2) -// let t := lt(x, 20) -// if t -// { -// if 1 { } -// if 1 { } -// if lt(x, 19) { } -// if 0 { } -// if 1 { } -// } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul deleted file mode 100644 index 1e409079e..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul +++ /dev/null @@ -1,31 +0,0 @@ -{ - let y := calldataload(0) - let t := calldataload(32) - - if sgt(sub(y, 1), y) { - // y - 1 > y, i.e. y is the most negative value - if eq(sdiv(y, sub(0, 1)), y) { - // should be true: y / -1 == y - sstore(0, 7) - } - if iszero(eq(y, t)) { - // t is not the most negative value - if eq(sdiv(t, sub(0, 1)), sub(0, t)) { - // should be true: t / -1 = 0 - t - sstore(1, 7) - } - } - } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// let y := calldataload(0) -// let t := calldataload(32) -// if sgt(sub(y, 1), y) -// { -// if 1 { sstore(0, 7) } -// if iszero(eq(y, t)) { if 1 { sstore(1, 7) } } -// } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul deleted file mode 100644 index 12f04c857..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul +++ /dev/null @@ -1,53 +0,0 @@ -{ - // 7 % 5 == 2 - // 7 % -5 == 2 - // -7 % 5 == -2 - // -7 % -5 == -2 - // -5 % -5 == 0 - let x := calldataload(0) - let y := calldataload(32) - let result := smod(x, y) - if eq(x, 7) { - if eq(y, 5) { - if eq(result, 2) { sstore(0, 7)} - } - if eq(y, sub(0, 5)) { - if eq(result, 2) { sstore(0, 7)} - } - } - if eq(x, sub(0, 7)) { - if eq(y, 5) { - if eq(result, sub(0, 2)) { sstore(0, 7)} - } - if eq(y, sub(0, 5)) { - if eq(result, sub(0, 2)) { sstore(0, 7)} - } - } - if eq(x, sub(0, 5)) { - if eq(y, sub(0, 5)) { - if eq(result, 0) { sstore(0, 7)} - } - } -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// let x := calldataload(0) -// let y := calldataload(32) -// let result := smod(x, y) -// if eq(x, 7) -// { -// if eq(y, 5) { if 1 { sstore(0, 7) } } -// if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } } -// } -// if eq(x, sub(0, 7)) -// { -// if eq(y, 5) { if 1 { sstore(0, 7) } } -// if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } } -// } -// if eq(x, sub(0, 5)) -// { -// if eq(y, sub(0, 5)) { if 1 { sstore(0, 7) } } -// } -// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smoke.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smoke.yul deleted file mode 100644 index 6f860dc13..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smoke.yul +++ /dev/null @@ -1,5 +0,0 @@ -{ } -// ---- -// step: reasoningBasedSimplifier -// -// { } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul deleted file mode 100644 index 69f5c6769..000000000 --- a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul +++ /dev/null @@ -1,15 +0,0 @@ -{ - let x := 7 - let y := 8 - if gt(sub(x, y), 20) { } - if eq(sub(x, y), 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) {} -} -// ---- -// step: reasoningBasedSimplifier -// -// { -// let x := 7 -// let y := 8 -// if 1 { } -// if 1 { } -// } diff --git a/test/tools/yulopti.cpp b/test/tools/yulopti.cpp index ad98ab9be..20491afe1 100644 --- a/test/tools/yulopti.cpp +++ b/test/tools/yulopti.cpp @@ -37,7 +37,6 @@ #include #include #include -#include #include diff --git a/test/yulPhaser/Chromosome.cpp b/test/yulPhaser/Chromosome.cpp index 90e278f42..1d12bf18c 100644 --- a/test/yulPhaser/Chromosome.cpp +++ b/test/yulPhaser/Chromosome.cpp @@ -138,7 +138,7 @@ BOOST_AUTO_TEST_CASE(output_operator_should_create_concise_and_unambiguous_strin BOOST_TEST(chromosome.length() == allSteps.size()); BOOST_TEST(chromosome.optimisationSteps() == allSteps); - BOOST_TEST(toString(chromosome) == "flcCUnDEvejsxIOoighFTLMRmVatrpuSd"); + BOOST_TEST(toString(chromosome) == "flcCUnDEvejsxIOoighFTLMmVatrpuSd"); } BOOST_AUTO_TEST_CASE(optimisationSteps_should_translate_chromosomes_genes_to_optimisation_step_names)