Merge pull request #10683 from ethereum/optSubEq

Optimize iszero(sub(x, y)) to eq(x, y).
This commit is contained in:
Harikrishnan Mulackal 2021-01-06 12:22:54 +01:00 committed by GitHub
commit 3cb48b8c60
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 45 additions and 0 deletions

View File

@ -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.

View File

@ -365,6 +365,11 @@ std::vector<SimplificationRule<Pattern>> simplificationRuleListPart6(
[=]() -> Pattern { return Builtins::EQ(X, Y); }
});
rules.push_back({
Builtins::ISZERO(Builtins::SUB(X, Y)),
[=]() -> Pattern { return Builtins::EQ(X, Y); }
});
return rules;
}

23
test/formal/eq_sub.py Normal file
View File

@ -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)

View File

@ -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) }
// }