From 8c5f5c7db09a565e8b1c897cbd5d5f2160e6c8bd Mon Sep 17 00:00:00 2001 From: Daniel Lupu Date: Mon, 2 May 2022 00:10:37 +0300 Subject: [PATCH 1/4] add rules for mod(mul(X, Y), A) & mod(add(X, Y), A) --- libevmasm/RuleList.h | 20 ++++++++++++++++++- .../combine_add_and_mod_constant.yul | 13 ++++++++++++ .../combine_mul_and_mod_constant.yul | 13 ++++++++++++ 3 files changed, 45 insertions(+), 1 deletion(-) create mode 100644 test/libyul/yulOptimizerTests/expressionSimplifier/combine_add_and_mod_constant.yul create mode 100644 test/libyul/yulOptimizerTests/expressionSimplifier/combine_mul_and_mod_constant.yul diff --git a/libevmasm/RuleList.h b/libevmasm/RuleList.h index ec0970e65..1ed101455 100644 --- a/libevmasm/RuleList.h +++ b/libevmasm/RuleList.h @@ -279,7 +279,7 @@ std::vector> simplificationRuleListPart5( Pattern B, Pattern, Pattern X, - Pattern + Pattern Y ) { using Word = typename Pattern::Word; @@ -287,6 +287,24 @@ std::vector> simplificationRuleListPart5( std::vector> rules; + // Replace MOD(MUL(X, Y), A) with MULMOD(X, Y, A) iff A=2**N + rules.push_back({ + Builtins::MOD(Builtins::MUL(X, Y), A), + [=]() -> Pattern { return Builtins::MULMOD(X, Y, A); }, + [=] { + return A.d() > 0 && ((A.d() & (A.d() - 1)) == 0); + } + }); + + // Replace MOD(ADD(X, Y), A) with ADDMOD(X, Y, A) iff A=2**N + rules.push_back({ + Builtins::MOD(Builtins::ADD(X, Y), A), + [=]() -> Pattern { return Builtins::ADDMOD(X, Y, A); }, + [=] { + return A.d() > 0 && ((A.d() & (A.d() - 1)) == 0); + } + }); + // Replace MOD X, with AND X, - 1 for (size_t i = 0; i < Pattern::WordSize; ++i) { diff --git a/test/libyul/yulOptimizerTests/expressionSimplifier/combine_add_and_mod_constant.yul b/test/libyul/yulOptimizerTests/expressionSimplifier/combine_add_and_mod_constant.yul new file mode 100644 index 000000000..f462486ea --- /dev/null +++ b/test/libyul/yulOptimizerTests/expressionSimplifier/combine_add_and_mod_constant.yul @@ -0,0 +1,13 @@ +{ + mstore(0, mod(add(mload(0), mload(1)), 32)) +} +// ---- +// step: expressionSimplifier +// +// { +// { +// let _3 := mload(1) +// let _4 := 0 +// mstore(_4, addmod(mload(_4), _3, 32)) +// } +// } diff --git a/test/libyul/yulOptimizerTests/expressionSimplifier/combine_mul_and_mod_constant.yul b/test/libyul/yulOptimizerTests/expressionSimplifier/combine_mul_and_mod_constant.yul new file mode 100644 index 000000000..93edb5319 --- /dev/null +++ b/test/libyul/yulOptimizerTests/expressionSimplifier/combine_mul_and_mod_constant.yul @@ -0,0 +1,13 @@ +{ + mstore(0, mod(mul(mload(0), mload(1)), 32)) +} +// ---- +// step: expressionSimplifier +// +// { +// { +// let _3 := mload(1) +// let _4 := 0 +// mstore(_4, mulmod(mload(_4), _3, 32)) +// } +// } From d1e382f2a883f2df8b67e0332c986b0801cd7a34 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Wed, 8 Jun 2022 18:07:55 +0200 Subject: [PATCH 2/4] Python Z3 proofs of the rules. --- test/formal/mod_add_to_addmod.py | 31 +++++++++++++++++++++++++++++++ test/formal/mod_mul_to_mulmod.py | 31 +++++++++++++++++++++++++++++++ test/formal/opcodes.py | 8 +++++++- 3 files changed, 69 insertions(+), 1 deletion(-) create mode 100644 test/formal/mod_add_to_addmod.py create mode 100644 test/formal/mod_mul_to_mulmod.py diff --git a/test/formal/mod_add_to_addmod.py b/test/formal/mod_add_to_addmod.py new file mode 100644 index 000000000..60093b7fe --- /dev/null +++ b/test/formal/mod_add_to_addmod.py @@ -0,0 +1,31 @@ +from opcodes import MOD, ADD, ADDMOD +from rule import Rule +from z3 import BitVec + +""" +Rule: +MOD(ADD(X, Y), A) -> ADDMOD(X, Y, A) +given + A > 0 + A & (A - 1) == 0 +""" + +rule = Rule() + +n_bits = 32 + +# Input vars +X = BitVec('X', n_bits) +Y = BitVec('Y', n_bits) +A = BitVec('A', n_bits) + +# Non optimized result +nonopt = MOD(ADD(X, Y), A) + +# Optimized result +opt = ADDMOD(X, Y, A) + +rule.require(A > 0) +rule.require(((A & (A - 1)) == 0)) + +rule.check(nonopt, opt) diff --git a/test/formal/mod_mul_to_mulmod.py b/test/formal/mod_mul_to_mulmod.py new file mode 100644 index 000000000..812f341ea --- /dev/null +++ b/test/formal/mod_mul_to_mulmod.py @@ -0,0 +1,31 @@ +from opcodes import MOD, MUL, MULMOD +from rule import Rule +from z3 import BitVec + +""" +Rule: +MOD(MUL(X, Y), A) -> MULMOD(X, Y, A) +given + A > 0 + A & (A - 1) == 0 +""" + +rule = Rule() + +n_bits = 8 + +# Input vars +X = BitVec('X', n_bits) +Y = BitVec('Y', n_bits) +A = BitVec('A', n_bits) + +# Non optimized result +nonopt = MOD(MUL(X, Y), A) + +# Optimized result +opt = MULMOD(X, Y, A) + +rule.require(A > 0) +rule.require(((A & (A - 1)) == 0)) + +rule.check(nonopt, opt) diff --git a/test/formal/opcodes.py b/test/formal/opcodes.py index 103e57a14..e091e7847 100644 --- a/test/formal/opcodes.py +++ b/test/formal/opcodes.py @@ -1,4 +1,4 @@ -from z3 import BitVecVal, BV2Int, If, LShR, UDiv, ULT, UGT, URem +from z3 import BitVecVal, BV2Int, If, LShR, UDiv, ULT, UGT, URem, ZeroExt, Extract def ADD(x, y): return x + y @@ -18,6 +18,12 @@ def SDIV(x, y): def MOD(x, y): return If(y == 0, 0, URem(x, y)) +def MULMOD(x, y, m): + return If(m == 0, 0, Extract(x.size() - 1, 0, URem(ZeroExt(x.size(), x) * ZeroExt(x.size(), y), ZeroExt(m.size(), m)))) + +def ADDMOD(x, y, m): + return If(m == 0, 0, Extract(x.size() - 1, 0, URem(ZeroExt(1, x) + ZeroExt(1, y), ZeroExt(1, m)))) + def SMOD(x, y): return If(y == 0, 0, x % y) From b99f85ec65e0353051ff2efd4145aeb479950c51 Mon Sep 17 00:00:00 2001 From: Daniel Lupu Date: Sat, 11 Jun 2022 13:43:55 +0300 Subject: [PATCH 3/4] Only apply rules for yul optimizer --- libevmasm/RuleList.h | 39 ++++++++++++++++++++++----------------- 1 file changed, 22 insertions(+), 17 deletions(-) diff --git a/libevmasm/RuleList.h b/libevmasm/RuleList.h index 1ed101455..9b20d0f8b 100644 --- a/libevmasm/RuleList.h +++ b/libevmasm/RuleList.h @@ -275,6 +275,7 @@ std::vector> simplificationRuleListPart4_5( template std::vector> simplificationRuleListPart5( + bool _forYulOptimizer, Pattern A, Pattern B, Pattern, @@ -287,23 +288,27 @@ std::vector> simplificationRuleListPart5( std::vector> rules; - // Replace MOD(MUL(X, Y), A) with MULMOD(X, Y, A) iff A=2**N - rules.push_back({ - Builtins::MOD(Builtins::MUL(X, Y), A), - [=]() -> Pattern { return Builtins::MULMOD(X, Y, A); }, - [=] { - return A.d() > 0 && ((A.d() & (A.d() - 1)) == 0); - } - }); + // The libevmasm optimizer does not support rules resulting in opcodes with more than two arguments. + if (_forYulOptimizer) + { + // Replace MOD(MUL(X, Y), A) with MULMOD(X, Y, A) iff A=2**N + rules.push_back({ + Builtins::MOD(Builtins::MUL(X, Y), A), + [=]() -> Pattern { return Builtins::MULMOD(X, Y, A); }, + [=] { + return A.d() > 0 && ((A.d() & (A.d() - 1)) == 0); + } + }); - // Replace MOD(ADD(X, Y), A) with ADDMOD(X, Y, A) iff A=2**N - rules.push_back({ - Builtins::MOD(Builtins::ADD(X, Y), A), - [=]() -> Pattern { return Builtins::ADDMOD(X, Y, A); }, - [=] { - return A.d() > 0 && ((A.d() & (A.d() - 1)) == 0); - } - }); + // Replace MOD(ADD(X, Y), A) with ADDMOD(X, Y, A) iff A=2**N + rules.push_back({ + Builtins::MOD(Builtins::ADD(X, Y), A), + [=]() -> Pattern { return Builtins::ADDMOD(X, Y, A); }, + [=] { + return A.d() > 0 && ((A.d() & (A.d() - 1)) == 0); + } + }); + } // Replace MOD X, with AND X, - 1 for (size_t i = 0; i < Pattern::WordSize; ++i) @@ -816,7 +821,7 @@ std::vector> simplificationRuleList( rules += simplificationRuleListPart3(A, B, C, W, X); rules += simplificationRuleListPart4(A, B, C, W, X); rules += simplificationRuleListPart4_5(A, B, C, W, X); - rules += simplificationRuleListPart5(A, B, C, W, X); + rules += simplificationRuleListPart5(_evmVersion.has_value(), A, B, C, W, X); rules += simplificationRuleListPart6(A, B, C, W, X); rules += simplificationRuleListPart7(A, B, C, W, X); rules += simplificationRuleListPart8(A, B, C, W, X); From 8498fdf1d4978fc1759985f4921382d637a96e36 Mon Sep 17 00:00:00 2001 From: Daniel Lupu Date: Wed, 15 Jun 2022 23:27:40 +0300 Subject: [PATCH 4/4] Add changelog entries --- Changelog.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Changelog.md b/Changelog.md index 6bc2f8af4..ee03bffa2 100644 --- a/Changelog.md +++ b/Changelog.md @@ -6,6 +6,8 @@ Language Features: Compiler Features: * TypeChecker: Support using library constants in initializers of other constants. * Yul IR Code Generation: Improved copy routines for arrays with packed storage layout. + * Yul Optimizer: Add rule to convert `mod(mul(X, Y), A)` into `mulmod(X, Y, A)`, if `A` is a power of two. + * Yul Optimizer: Add rule to convert `mod(add(X, Y), A)` into `addmod(X, Y, A)`, if `A` is a power of two. Bugfixes: