From 59f4989966ead898cc2a048a73361d6c996a8320 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 4 Jun 2020 11:11:53 +0200 Subject: [PATCH] Optimize combination of byte and shl. --- .gitignore | 2 +- Changelog.md | 3 ++ libevmasm/RuleList.h | 14 ++++++ test/formal/combine_byte_shl.py | 29 ++++++++++++ test/formal/combine_byte_shr_1.py | 30 +++++++++++++ test/formal/combine_byte_shr_2.py | 30 +++++++++++++ test/formal/opcodes.py | 4 ++ .../semanticTests/optimizer/shift_bytes.sol | 44 +++++++++++++++++++ 8 files changed, 155 insertions(+), 1 deletion(-) create mode 100644 test/formal/combine_byte_shl.py create mode 100644 test/formal/combine_byte_shr_1.py create mode 100644 test/formal/combine_byte_shr_2.py create mode 100644 test/libsolidity/semanticTests/optimizer/shift_bytes.sol diff --git a/.gitignore b/.gitignore index f6eeba75f..67e450759 100644 --- a/.gitignore +++ b/.gitignore @@ -35,7 +35,7 @@ build/ build*/ emscripten_build/ docs/_build -docs/utils/__pycache__ +__pycache__ docs/utils/*.pyc /deps/downloads/ deps/install diff --git a/Changelog.md b/Changelog.md index 9795ecb51..7b0a87a9a 100644 --- a/Changelog.md +++ b/Changelog.md @@ -6,6 +6,9 @@ Compiler Features: Bugfixes: * Type Checker: Fix overload resolution in combination with ``{value: ...}``. +Compiler Features: + * Optimizer: Add rule to remove shifts inside the byte opcode. + ### 0.6.11 (2020-07-07) diff --git a/libevmasm/RuleList.h b/libevmasm/RuleList.h index e29141b49..9442524b1 100644 --- a/libevmasm/RuleList.h +++ b/libevmasm/RuleList.h @@ -571,6 +571,20 @@ std::vector> simplificationRuleListPart7( feasibilityFunction }); + rules.push_back({ + Builtins::BYTE(A, Builtins::SHL(B, X)), + [=]() -> Pattern { return Builtins::BYTE(A.d() + B.d() / 8, X); }, + false, + [=] { return B.d() % 8 == 0 && A.d() <= 32 && B.d() <= 256; } + }); + + rules.push_back({ + Builtins::BYTE(A, Builtins::SHR(B, X)), + [=]() -> Pattern { return A.d() < B.d() / 8 ? Word(0) : Builtins::BYTE(A.d() - B.d() / 8, X); }, + false, + [=] { return B.d() % 8 == 0 && A.d() < Pattern::WordSize / 8 && B.d() <= Pattern::WordSize; } + }); + return rules; } diff --git a/test/formal/combine_byte_shl.py b/test/formal/combine_byte_shl.py new file mode 100644 index 000000000..e2a6034ff --- /dev/null +++ b/test/formal/combine_byte_shl.py @@ -0,0 +1,29 @@ +from rule import Rule +from opcodes import * + +""" +byte(A, shl(B, X)) +given B % 8 == 0 && A <= 32 && B <= 256 +-> +byte(A + B / 8, X) +""" + +rule = Rule() + +n_bits = 256 + +# Input vars +X = BitVec('X', n_bits) +A = BitVec('A', n_bits) +B = BitVec('B', n_bits) + +# Non optimized result +nonopt = BYTE(A, SHL(B, X)) +# Optimized result +opt = BYTE(A + B / 8, X) + +rule.require(B % 8 == 0) +rule.require(ULE(A, 32)) +rule.require(ULE(B, 256)) + +rule.check(nonopt, opt) diff --git a/test/formal/combine_byte_shr_1.py b/test/formal/combine_byte_shr_1.py new file mode 100644 index 000000000..4938e73f7 --- /dev/null +++ b/test/formal/combine_byte_shr_1.py @@ -0,0 +1,30 @@ +from rule import Rule +from opcodes import * + +""" +byte(A, shr(B, X)) +given B % 8 == 0 && A < n_bits/8 && B <= n_bits && A >= B / 8 +-> +byte(A - B / 8, X) +""" + +rule = Rule() + +n_bits = 256 + +# Input vars +X = BitVec('X', n_bits) +A = BitVec('A', n_bits) +B = BitVec('B', n_bits) + +# Non optimized result +nonopt = BYTE(A, SHR(B, X)) +# Optimized result +opt = BYTE(A - B / 8, X) + +rule.require(B % 8 == 0) +rule.require(ULT(A, n_bits/8)) +rule.require(ULE(B, n_bits)) +rule.require(UGE(A, DIV(B,8))) + +rule.check(nonopt, opt) diff --git a/test/formal/combine_byte_shr_2.py b/test/formal/combine_byte_shr_2.py new file mode 100644 index 000000000..d74114e85 --- /dev/null +++ b/test/formal/combine_byte_shr_2.py @@ -0,0 +1,30 @@ +from rule import Rule +from opcodes import * + +""" +byte(A, shr(B, X)) +given B % 8 == 0 && A < n_bits/8 && B <= n_bits && A < B / 8 +-> +0 +""" + +rule = Rule() + +n_bits = 256 + +# Input vars +X = BitVec('X', n_bits) +A = BitVec('A', n_bits) +B = BitVec('B', n_bits) + +# Non optimized result +nonopt = BYTE(A, SHR(B, X)) +# Optimized result +opt = 0 + +rule.require(B % 8 == 0) +rule.require(ULT(A, n_bits/8)) +rule.require(ULE(B, n_bits)) +rule.require(ULT(A, DIV(B,8))) + +rule.check(nonopt, opt) diff --git a/test/formal/opcodes.py b/test/formal/opcodes.py index 589bd9520..24d53484b 100644 --- a/test/formal/opcodes.py +++ b/test/formal/opcodes.py @@ -56,3 +56,7 @@ def SHR(x, y): def SAR(x, y): return y >> x + +def BYTE(i, x): + bit = (i + 1) * 8 + return If(UGT(bit, x.size()), BitVecVal(0, x.size()), (LShR(x, (x.size() - bit))) & 0xff) diff --git a/test/libsolidity/semanticTests/optimizer/shift_bytes.sol b/test/libsolidity/semanticTests/optimizer/shift_bytes.sol new file mode 100644 index 000000000..5a85160f9 --- /dev/null +++ b/test/libsolidity/semanticTests/optimizer/shift_bytes.sol @@ -0,0 +1,44 @@ +// This tests the optimizer rule +// byte(A, shl(B, X)) +// -> +// byte(A + B / 8, X) +// given A <= 32 && B % 8 == 0 && B <= 256 +// +// and the respective rule about shr +contract C { + function f(uint a) public returns (uint, uint, uint) { + uint x = a << (256 - 8); + assembly { + x := byte(0, x) + } + uint y = a << 8; + assembly { + y := byte(30, y) + } + uint z = a << 16; + assembly { + z := byte(1, z) + } + return (x, y, z); + } + function g(uint a) public returns (uint, uint, uint) { + uint x = a >> (256 - 16); + assembly { + x := byte(31, x) + } + uint y = a >> 8; + assembly { + y := byte(4, y) + } + uint z = a >> 16; + assembly { + z := byte(7, z) + } + return (x, y, z); + } +} +// ==== +// compileViaYul: also +// ---- +// f(uint256): 0x0102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f -> 0x1f, 0x1f, 3 +// g(uint256): 0x0102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f -> 1, 3, 5