From d46da8e53c880cf44ff7d4c431c41bf1844debb3 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 22 Dec 2020 15:08:37 +0100 Subject: [PATCH] Optimize iszero(sub(x, y)) to eq(x, y). --- libevmasm/RuleList.h | 5 ++++ test/formal/eq_sub.py | 23 +++++++++++++++++++ .../expressionSimplifier/sub_eq.yul | 16 +++++++++++++ 3 files changed, 44 insertions(+) create mode 100644 test/formal/eq_sub.py create mode 100644 test/libyul/yulOptimizerTests/expressionSimplifier/sub_eq.yul diff --git a/libevmasm/RuleList.h b/libevmasm/RuleList.h index 8943c662b..c324514ec 100644 --- a/libevmasm/RuleList.h +++ b/libevmasm/RuleList.h @@ -365,6 +365,11 @@ std::vector> simplificationRuleListPart6( [=]() -> Pattern { return Builtins::EQ(X, Y); } }); + rules.push_back({ + Builtins::ISZERO(Builtins::SUB(X, Y)), + [=]() -> Pattern { return Builtins::EQ(X, Y); } + }); + return rules; } diff --git a/test/formal/eq_sub.py b/test/formal/eq_sub.py new file mode 100644 index 000000000..bf7518acf --- /dev/null +++ b/test/formal/eq_sub.py @@ -0,0 +1,23 @@ +from rule import Rule +from opcodes import * + +""" +Rule: +ISZERO(SUB(X, Y)) -> EQ(X, Y) +""" + +rule = Rule() + +n_bits = 256 + +# Input vars +X = BitVec('X', n_bits) +Y = BitVec('Y', n_bits) + +# Non optimized result +nonopt = ISZERO(SUB(X, Y)) + +# Optimized result +opt = EQ(X, Y) + +rule.check(nonopt, opt) diff --git a/test/libyul/yulOptimizerTests/expressionSimplifier/sub_eq.yul b/test/libyul/yulOptimizerTests/expressionSimplifier/sub_eq.yul new file mode 100644 index 000000000..5380c1905 --- /dev/null +++ b/test/libyul/yulOptimizerTests/expressionSimplifier/sub_eq.yul @@ -0,0 +1,16 @@ +{ + let a := calldataload(0) + let b := calldataload(0x20) + let x := sub(a, b) + if gt(x, 0) { + sstore(0, 1) + } +} +// ---- +// step: expressionSimplifier +// +// { +// let _1 := 0 +// let a := calldataload(_1) +// if iszero(eq(a, calldataload(0x20))) { sstore(_1, 1) } +// }