cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #6943 from ethereum/opcodeFix

Browse Source 
Fix comparison opcodes and minor errors in proof scripts.
This commit is contained in:
Daniel Kirchner 2019-06-14 17:45:34 +02:00 committed by GitHub
commit e78500a199
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 11 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
test/formal/combine_div_shl_one_32.py
View File

@ -15,11 +15,8 @@ n_bits = 32
X = BitVec('X', n_bits)
Y = BitVec('Y', n_bits)
# Constants
ONE = BitVecVal(1, n_bits)
# Non optimized result
nonopt = DIV(X, SHL(Y, ONE))
nonopt = DIV(X, SHL(Y, 1))
# Optimized result
opt = SHR(Y, X)

7
test/formal/combine_mul_shl_one_64.py
View File

@ -16,14 +16,11 @@ n_bits = 64
X = BitVec('X', n_bits)
Y = BitVec('Y', n_bits)
# Constants
ONE = BitVecVal(1, n_bits)
# Requirements
# Non optimized result
nonopt_1 = MUL(X, SHL(Y, ONE))
nonopt_2 = MUL(SHL(X, ONE), Y)
nonopt_1 = MUL(X, SHL(Y, 1))
nonopt_2 = MUL(SHL(X, 1), Y)
# Optimized result
opt_1 = SHL(Y, X)

2
test/formal/combine_shr_shl_by_constant_64.py
View File

@ -33,7 +33,7 @@ nonopt = SHL(B, SHR(A, X))
Mask = SHL(B, SHR(A, Int2BV(IntVal(-1), n_bits)))
opt = If(
UGT(A, B),
AND(SHR(a - b, x), Mask),
AND(SHR(A - B, X), Mask),
If(
UGT(B, A),
AND(SHL(B - A, X), Mask),

11
test/formal/opcodes.py
View File

@ -22,16 +22,19 @@ def SMOD(x, y):
return If(y == 0, 0, x % y)
def LT(x, y):
return ULT(x, y)
return If(ULT(x, y), BitVecVal(1, x.size()), BitVecVal(0, x.size()))
def GT(x, y):
return UGT(x, y)
return If(UGT(x, y), BitVecVal(1, x.size()), BitVecVal(0, x.size()))
def SLT(x, y):
return x < y
return If(x < y, BitVecVal(1, x.size()), BitVecVal(0, x.size()))
def SGT(x, y):
return x > y
return If(x > y, BitVecVal(1, x.size()), BitVecVal(0, x.size()))
def ISZERO(x):
return If(x == 0, BitVecVal(1, x.size()), BitVecVal(0, x.size()))
def AND(x, y):
return x & y