Optimize byte-after-shr for shift amounts that are not multiples of 8.

This commit is contained in:
chriseth
2020-08-04 12:16:23 +02:00
parent f079efe28c
commit a3a9630d8b
3 changed files with 11 additions and 7 deletions
+1 -4
View File
@@ -3,7 +3,7 @@ from opcodes import *
"""
byte(A, shr(B, X))
given B % 8 == 0 && A < n_bits/8 && B <= n_bits && A < B / 8
given A < B / 8
->
0
"""
@@ -22,9 +22,6 @@ 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)