diff --git a/Changelog.md b/Changelog.md index 21d3ee43c..2c8314750 100644 --- a/Changelog.md +++ b/Changelog.md @@ -4,6 +4,7 @@ Language Features: * Possibility to use ``catch Panic(uint code)`` to catch a panic failure from an external call. Compiler Features: + * Optimizer: Add rule to replace ``iszero(sub(x,y))`` by ``eq(x,y)``. * Parser: Report meaningful error if parsing a version pragma failed. * SMTChecker: Support ABI functions as uninterpreted functions. * SMTChecker: Use checked arithmetic by default and support ``unchecked`` blocks. 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/iszero_sub_to_eq.yul b/test/libyul/yulOptimizerTests/expressionSimplifier/iszero_sub_to_eq.yul new file mode 100644 index 000000000..7efa54b02 --- /dev/null +++ b/test/libyul/yulOptimizerTests/expressionSimplifier/iszero_sub_to_eq.yul @@ -0,0 +1,16 @@ +{ + let a := calldataload(0) + let b := calldataload(0x20) + let x := sub(a, b) + if iszero(x) { + sstore(0, 1) + } +} +// ---- +// step: expressionSimplifier +// +// { +// let _1 := 0 +// let a := calldataload(_1) +// if eq(a, calldataload(0x20)) { sstore(_1, 1) } +// }