Optimize combination of byte and shl.

This commit is contained in:
chriseth
2020-07-08 20:26:46 +02:00
parent ecc4bf2464
commit 59f4989966
8 changed files with 155 additions and 1 deletions
+29
View File
@@ -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)
+30
View File
@@ -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)
+30
View File
@@ -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)
+4
View File
@@ -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)
@@ -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