From f73fb726aff0284f3de18204f23b502f94475c5d Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 11 May 2020 19:56:29 +0200 Subject: [PATCH 1/5] Reasoning based optimizer. --- libsmtutil/CMakeLists.txt | 1 + libsmtutil/Helpers.h | 58 +++ libsolidity/formal/SMTEncoder.cpp | 7 +- libyul/CMakeLists.txt | 5 +- libyul/Dialect.cpp | 9 + libyul/Dialect.h | 1 + libyul/optimiser/ReasoningBasedSimplifier.cpp | 330 ++++++++++++++++++ libyul/optimiser/ReasoningBasedSimplifier.h | 97 +++++ .../semanticTests/arithmetics/signed_mod.sol | 14 + test/libyul/YulOptimizerTest.cpp | 6 + .../reasoningBasedSimplifier/addmod.yul | 31 ++ .../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 | 8 + 23 files changed, 825 insertions(+), 6 deletions(-) create mode 100644 libsmtutil/Helpers.h create mode 100644 libyul/optimiser/ReasoningBasedSimplifier.cpp create mode 100644 libyul/optimiser/ReasoningBasedSimplifier.h create mode 100644 test/libsolidity/semanticTests/arithmetics/signed_mod.sol create mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul create mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith.yul create mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_movable.yul create mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/arith_non_movable.yul create mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulcheck.yul create mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/mulmod.yul create mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/negative_rounding.yul create mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/nested.yul create mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/signed_division.yul create mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smod.yul create mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/smoke.yul create mode 100644 test/libyul/yulOptimizerTests/reasoningBasedSimplifier/wrapping.yul 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; } From 2d7e28769a38da0fd7e470a2f1597f33d47132a0 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 10 Sep 2020 16:16:11 +0200 Subject: [PATCH 2/5] Skip smt optimizer tests if smt is disabled. --- test/libyul/YulOptimizerTest.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/test/libyul/YulOptimizerTest.cpp b/test/libyul/YulOptimizerTest.cpp index 30a8aed5d..cdcfd4fc2 100644 --- a/test/libyul/YulOptimizerTest.cpp +++ b/test/libyul/YulOptimizerTest.cpp @@ -103,6 +103,9 @@ 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) + m_shouldRun = false; + m_source = m_reader.source(); auto dialectName = m_reader.stringSetting("dialect", "evm"); From 9bcc2f1713663d9cd64399d132f4d95ead603ada Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 10 Sep 2020 16:18:57 +0200 Subject: [PATCH 3/5] Make ReasoningBasedSimplifier available as step. --- libyul/optimiser/Suite.cpp | 3 +++ test/tools/yulopti.cpp | 9 +-------- test/yulPhaser/Chromosome.cpp | 2 +- 3 files changed, 5 insertions(+), 9 deletions(-) diff --git a/libyul/optimiser/Suite.cpp b/libyul/optimiser/Suite.cpp index 1625e60c5..4f52c8fe8 100644 --- a/libyul/optimiser/Suite.cpp +++ b/libyul/optimiser/Suite.cpp @@ -41,6 +41,7 @@ #include #include #include +#include #include #include #include @@ -184,6 +185,7 @@ map> const& OptimiserSuite::allSteps() LoopInvariantCodeMotion, NameSimplifier, RedundantAssignEliminator, + ReasoningBasedSimplifier, Rematerialiser, SSAReverser, SSATransform, @@ -221,6 +223,7 @@ map const& OptimiserSuite::stepNameToAbbreviationMap() {LoadResolver::name, 'L'}, {LoopInvariantCodeMotion::name, 'M'}, {NameSimplifier::name, 'N'}, + {ReasoningBasedSimplifier::name, 'R'}, {RedundantAssignEliminator::name, 'r'}, {Rematerialiser::name, 'm'}, {SSAReverser::name, 'V'}, diff --git a/test/tools/yulopti.cpp b/test/tools/yulopti.cpp index 409951e42..a15c426dc 100644 --- a/test/tools/yulopti.cpp +++ b/test/tools/yulopti.cpp @@ -158,8 +158,7 @@ public: map const& extraOptions = { {'#', "quit"}, {',', "VarNameCleaner"}, - {';', "StackCompressor"}, - {'R', "ReasoningBasedSimplifier"} + {';', "StackCompressor"} }; printUsageBanner(abbreviationMap, extraOptions, 4); @@ -192,12 +191,6 @@ public: StackCompressor::run(m_dialect, obj, true, 16); break; } - case 'R': - { - ReasoningBasedSimplifier::run(context, *m_ast); - break; - } - default: cerr << "Unknown option." << endl; } diff --git a/test/yulPhaser/Chromosome.cpp b/test/yulPhaser/Chromosome.cpp index 4d0592e9a..1f66398be 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) == "flcCUnDvejsxIOoighTLMNrmVatpud"); + BOOST_TEST(toString(chromosome) == "flcCUnDvejsxIOoighTLMNRrmVatpud"); } BOOST_AUTO_TEST_CASE(optimisationSteps_should_translate_chromosomes_genes_to_optimisation_step_names) From bfd3ab23e29f813eb9d4968b8a2186313162255b Mon Sep 17 00:00:00 2001 From: chriseth Date: Fri, 11 Sep 2020 13:39:11 +0200 Subject: [PATCH 4/5] Disallow optimizer steps that require SMT if none is available. --- libyul/optimiser/OptimiserStep.h | 25 +++++++++++++++++++ libyul/optimiser/ReasoningBasedSimplifier.cpp | 9 +++++++ libyul/optimiser/ReasoningBasedSimplifier.h | 1 + libyul/optimiser/Suite.cpp | 9 +++++++ 4 files changed, 44 insertions(+) diff --git a/libyul/optimiser/OptimiserStep.h b/libyul/optimiser/OptimiserStep.h index 3da161957..70ed098a8 100644 --- a/libyul/optimiser/OptimiserStep.h +++ b/libyul/optimiser/OptimiserStep.h @@ -20,6 +20,7 @@ #include +#include #include #include @@ -49,17 +50,41 @@ struct OptimiserStep virtual ~OptimiserStep() = default; virtual void run(OptimiserStepContext&, Block&) const = 0; + /// @returns non-nullopt if the step cannot be run, for example because it requires + /// an SMT solver to be loaded, but none is available. In that case, the string + /// contains a human-readable reason. + virtual std::optional invalidInCurrentEnvironment() const = 0; std::string name; }; template struct OptimiserStepInstance: public OptimiserStep { +private: + template + struct HasInvalidInCurrentEnvironmentMethod + { + private: + template static auto test(int) -> decltype(U::invalidInCurrentEnvironment(), std::true_type()); + template static std::false_type test(...); + + public: + static constexpr bool value = decltype(test(0))::value; + }; + +public: OptimiserStepInstance(): OptimiserStep{Step::name} {} void run(OptimiserStepContext& _context, Block& _ast) const override { Step::run(_context, _ast); } + std::optional invalidInCurrentEnvironment() const override + { + if constexpr (HasInvalidInCurrentEnvironmentMethod::value) + return Step::invalidInCurrentEnvironment(); + else + return std::nullopt; + }; }; diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp index 7d22e335c..90c3916c2 100644 --- a/libyul/optimiser/ReasoningBasedSimplifier.cpp +++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp @@ -46,6 +46,15 @@ void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _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) { if (_varDecl.variables.size() != 1 || !_varDecl.value) diff --git a/libyul/optimiser/ReasoningBasedSimplifier.h b/libyul/optimiser/ReasoningBasedSimplifier.h index 904828bfc..18fcf3583 100644 --- a/libyul/optimiser/ReasoningBasedSimplifier.h +++ b/libyul/optimiser/ReasoningBasedSimplifier.h @@ -51,6 +51,7 @@ class ReasoningBasedSimplifier: public ASTModifier 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; diff --git a/libyul/optimiser/Suite.cpp b/libyul/optimiser/Suite.cpp index 4f52c8fe8..98683b453 100644 --- a/libyul/optimiser/Suite.cpp +++ b/libyul/optimiser/Suite.cpp @@ -269,6 +269,7 @@ void OptimiserSuite::validateSequence(string const& _stepAbbreviations) insideLoop = false; break; default: + { yulAssert( string(NonStepAbbreviations).find(abbreviation) == string::npos, "Unhandled syntactic element in the abbreviation sequence" @@ -278,6 +279,14 @@ void OptimiserSuite::validateSequence(string const& _stepAbbreviations) OptimizerException, "'"s + abbreviation + "' is not a valid step abbreviation" ); + optional invalid = allSteps().at(stepAbbreviationToNameMap().at(abbreviation))->invalidInCurrentEnvironment(); + assertThrow( + !invalid.has_value(), + OptimizerException, + "'"s + abbreviation + "' is invalid in the current environment: " + *invalid + ); + + } } assertThrow(!insideLoop, OptimizerException, "Unbalanced brackets"); } From e527ac88f7ed6c5387cef130c4dee878133c9896 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 14 Sep 2020 16:56:45 +0200 Subject: [PATCH 5/5] Documentation. --- docs/yul.rst | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/docs/yul.rst b/docs/yul.rst index c7c7fdb33..281cb8d63 100644 --- a/docs/yul.rst +++ b/docs/yul.rst @@ -1110,6 +1110,7 @@ Abbreviation Full name ``L`` ``LoadResolver`` ``M`` ``LoopInvariantCodeMotion`` ``r`` ``RedundantAssignEliminator`` +``R`` ``ReasoningBasedSimplifier`` - highly experimental ``m`` ``Rematerialiser`` ``V`` ``SSAReverser`` ``a`` ``SSATransform`` @@ -1121,6 +1122,10 @@ 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! .. _erc20yul: