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)