diff --git a/libsmtutil/CMakeLists.txt b/libsmtutil/CMakeLists.txt index 62b52f5c6..8c8b3677d 100644 --- a/libsmtutil/CMakeLists.txt +++ b/libsmtutil/CMakeLists.txt @@ -9,6 +9,7 @@ set(sources SolverInterface.h Sorts.cpp Sorts.h + Helpers.h ) if (${Z3_FOUND}) diff --git a/libsmtutil/Helpers.h b/libsmtutil/Helpers.h new file mode 100644 index 000000000..fa6081b16 --- /dev/null +++ b/libsmtutil/Helpers.h @@ -0,0 +1,58 @@ +/* + 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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#pragma once + +#include + +namespace solidity::smtutil +{ + +/// Signed division in SMTLIB2 rounds differently than EVM. +/// This does not check for division by zero! +inline Expression signedDivision(Expression _left, Expression _right) +{ + return Expression::ite( + _left >= 0, + Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))), + Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right)) + ); +} + +inline Expression abs(Expression _value) +{ + return Expression::ite(_value >= 0, _value, 0 - _value); +} + +/// Signed modulo in SMTLIB2 behaves differently with regards +/// to the sign than EVM. +/// This does not check for modulo by zero! +inline Expression signedModulo(Expression _left, Expression _right) +{ + return Expression::ite( + _left >= 0, + _left % _right, + Expression::ite( + (_left % _right) == 0, + 0, + (_left % _right) - abs(_right) + ) + ); +} + +} diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index e2a35a0d8..f8a8893bd 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -23,6 +23,7 @@ #include #include +#include #include #include @@ -1497,11 +1498,7 @@ smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Exp { // Signed division in SMTLIB2 rounds differently for negative division. if (_type.isSigned()) - return (smtutil::Expression::ite( - _left >= 0, - smtutil::Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))), - smtutil::Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right)) - )); + return signedDivision(_left, _right); else return _left / _right; } diff --git a/libyul/CMakeLists.txt b/libyul/CMakeLists.txt index bb385c755..bbc52d8f2 100644 --- a/libyul/CMakeLists.txt +++ b/libyul/CMakeLists.txt @@ -132,6 +132,8 @@ add_library(yul optimiser/OptimiserStep.h optimiser/OptimizerUtilities.cpp optimiser/OptimizerUtilities.h + optimiser/ReasoningBasedSimplifier.cpp + optimiser/ReasoningBasedSimplifier.h optimiser/RedundantAssignEliminator.cpp optimiser/RedundantAssignEliminator.h optimiser/Rematerialiser.cpp @@ -168,4 +170,5 @@ add_library(yul optimiser/VarNameCleaner.cpp optimiser/VarNameCleaner.h ) -target_link_libraries(yul PUBLIC evmasm solutil langutil) + +target_link_libraries(yul PUBLIC evmasm solutil langutil smtutil) \ No newline at end of file diff --git a/libyul/Dialect.cpp b/libyul/Dialect.cpp index 1003c8e44..6c498ce4c 100644 --- a/libyul/Dialect.cpp +++ b/libyul/Dialect.cpp @@ -33,6 +33,15 @@ Literal Dialect::zeroLiteralForType(solidity::yul::YulString _type) const return {SourceLocation{}, LiteralKind::Number, "0"_yulstring, _type}; } + +Literal Dialect::trueLiteral() const +{ + if (boolType != defaultType) + return {SourceLocation{}, LiteralKind::Boolean, "true"_yulstring, boolType}; + else + return {SourceLocation{}, LiteralKind::Number, "1"_yulstring, defaultType}; +} + bool Dialect::validTypeForLiteral(LiteralKind _kind, YulString, YulString _type) const { if (_kind == LiteralKind::Boolean) diff --git a/libyul/Dialect.h b/libyul/Dialect.h index 6634d6cfd..d47c09659 100644 --- a/libyul/Dialect.h +++ b/libyul/Dialect.h @@ -77,6 +77,7 @@ struct Dialect: boost::noncopyable virtual bool validTypeForLiteral(LiteralKind _kind, YulString _value, YulString _type) const; virtual Literal zeroLiteralForType(YulString _type) const; + virtual Literal trueLiteral() const; virtual std::set fixedFunctionNames() const { return {}; } diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp new file mode 100644 index 000000000..7d22e335c --- /dev/null +++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp @@ -0,0 +1,330 @@ +/* + 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 +#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); +} + +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)); +} + +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.location = locationOf(*_if.condition); + _if.condition = make_unique(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.location = locationOf(*_if.condition); + _if.condition = make_unique(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 +): + m_dialect(_dialect), + m_ssaVariables(_ssaVariables), + m_solver(make_unique()) +{ +} + +smtutil::Expression ReasoningBasedSimplifier::encodeExpression(yul::Expression const& _expression) +{ + return std::visit(GenericVisitor{ + [&](FunctionCall const& _functionCall) + { + if (auto const* dialect = dynamic_cast(&m_dialect)) + if (auto const* builtin = dialect->builtin(_functionCall.functionName.name)) + if (builtin->instruction) + return encodeEVMBuiltin(*builtin->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, + 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 `signedToUnsigned` + signedToUnsigned(smtutil::signedDivision( + unsignedToSigned(arguments.at(0)), + unsignedToSigned(arguments.at(1)) + )) + ); + break; + 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), + signedToUnsigned(signedModulo( + unsignedToSigned(arguments.at(0)), + unsignedToSigned(arguments.at(1)) + )) + ); + break; + 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))); + 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))); + 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(); +} + +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 new file mode 100644 index 000000000..904828bfc --- /dev/null +++ b/libyul/optimiser/ReasoningBasedSimplifier.h @@ -0,0 +1,97 @@ +/* + 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 + +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 +{ +public: + static constexpr char const* name{"ReasoningBasedSimplifier"}; + static void run(OptimiserStepContext& _context, Block& _ast); + + 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 encodeExpression( + Expression const& _expression + ); + + virtual 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); + + 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/test/libsolidity/semanticTests/arithmetics/signed_mod.sol b/test/libsolidity/semanticTests/arithmetics/signed_mod.sol new file mode 100644 index 000000000..a992bd0be --- /dev/null +++ b/test/libsolidity/semanticTests/arithmetics/signed_mod.sol @@ -0,0 +1,14 @@ +contract C { + function f(int a, int b) public pure returns (int) { + return a % b; + } +} + +// ==== +// compileViaYul: also +// ---- +// f(int256,int256): 7, 5 -> 2 +// f(int256,int256): 7, -5 -> 2 +// f(int256,int256): -7, 5 -> -2 +// f(int256,int256): -7, 5 -> -2 +// f(int256,int256): -5, -5 -> 0 diff --git a/test/libyul/YulOptimizerTest.cpp b/test/libyul/YulOptimizerTest.cpp index 18576384d..30a8aed5d 100644 --- a/test/libyul/YulOptimizerTest.cpp +++ b/test/libyul/YulOptimizerTest.cpp @@ -53,6 +53,7 @@ #include #include #include +#include #include #include #include @@ -320,6 +321,11 @@ TestCase::TestResult YulOptimizerTest::run(ostream& _stream, string const& _line LiteralRematerialiser::run(*m_context, *m_object->code); StructuralSimplifier::run(*m_context, *m_object->code); } + else if (m_optimizerStep == "reasoningBasedSimplifier") + { + disambiguate(); + ReasoningBasedSimplifier::run(*m_context, *m_object->code); + } else if (m_optimizerStep == "equivalentFunctionCombiner") { disambiguate(); diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul new file mode 100644 index 000000000..88c60a0ee --- /dev/null +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul @@ -0,0 +1,31 @@ +{ + let x := calldataload(0) + let y := calldataload(32) + let z := calldataload(64) + let result := addmod(x, y, z) + + // should be zero + if gt(result, z) { sstore(0, 1) } + + // addmod is equal to mod of sum for small numbers + if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { + if eq(result, mod(add(x, y), z)) { sstore(0, 9) } + } + + // but not in general + if and(and(gt(x, sub(0, 5)), gt(y, sub(0, 2))), eq(z, 3)) { + if eq(result, mod(add(x, y), z)) { sstore(0, 5) } + } +} +// ---- +// step: reasoningBasedSimplifier +// +// { +// let x := calldataload(0) +// let y := calldataload(32) +// let z := calldataload(64) +// let result := addmod(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)), gt(y, sub(0, 2))), eq(z, 3)) { if 0 { } } +// } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul new file mode 100644 index 000000000..7ff930766 --- /dev/null +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul @@ -0,0 +1,13 @@ +{ + 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 new file mode 100644 index 000000000..2080a678c --- /dev/null +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_movable.yul @@ -0,0 +1,19 @@ +{ + 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 new file mode 100644 index 000000000..ed50224d0 --- /dev/null +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_non_movable.yul @@ -0,0 +1,23 @@ +{ + 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 new file mode 100644 index 000000000..31a342339 --- /dev/null +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul @@ -0,0 +1,32 @@ +{ + 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 new file mode 100644 index 000000000..f5226acf7 --- /dev/null +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul @@ -0,0 +1,31 @@ +{ + 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 new file mode 100644 index 000000000..6e4b3f5ed --- /dev/null +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul @@ -0,0 +1,16 @@ +{ + 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 new file mode 100644 index 000000000..d7002c99b --- /dev/null +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul @@ -0,0 +1,26 @@ +{ + 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 new file mode 100644 index 000000000..1e409079e --- /dev/null +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul @@ -0,0 +1,31 @@ +{ + 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 new file mode 100644 index 000000000..12f04c857 --- /dev/null +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul @@ -0,0 +1,53 @@ +{ + // 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 new file mode 100644 index 000000000..6f860dc13 --- /dev/null +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smoke.yul @@ -0,0 +1,5 @@ +{ } +// ---- +// step: reasoningBasedSimplifier +// +// { } diff --git a/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul new file mode 100644 index 000000000..69f5c6769 --- /dev/null +++ b/test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul @@ -0,0 +1,15 @@ +{ + 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 e4605d10f..409951e42 100644 --- a/test/tools/yulopti.cpp +++ b/test/tools/yulopti.cpp @@ -36,6 +36,7 @@ #include #include #include +#include #include @@ -158,6 +159,7 @@ public: {'#', "quit"}, {',', "VarNameCleaner"}, {';', "StackCompressor"}, + {'R', "ReasoningBasedSimplifier"} }; printUsageBanner(abbreviationMap, extraOptions, 4); @@ -190,6 +192,12 @@ public: StackCompressor::run(m_dialect, obj, true, 16); break; } + case 'R': + { + ReasoningBasedSimplifier::run(context, *m_ast); + break; + } + default: cerr << "Unknown option." << endl; }