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

Fix comparison opcodes and minor errors in proof scripts.

Browse Source
This commit is contained in:
Daniel Kirchner 2019-06-14 16:57:57 +02:00
parent 4aa0c9e079
commit 5718072e10
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) X = BitVec('X', n_bits)
Y = BitVec('Y', n_bits) Y = BitVec('Y', n_bits)
# Constants
ONE = BitVecVal(1, n_bits)
# Non optimized result # Non optimized result
nonopt = DIV(X, SHL(Y, ONE)) nonopt = DIV(X, SHL(Y, 1))
# Optimized result # Optimized result
opt = SHR(Y, X) 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) X = BitVec('X', n_bits)
Y = BitVec('Y', n_bits) Y = BitVec('Y', n_bits)
# Constants
ONE = BitVecVal(1, n_bits)
# Requirements # Requirements
# Non optimized result # Non optimized result
nonopt_1 = MUL(X, SHL(Y, ONE)) nonopt_1 = MUL(X, SHL(Y, 1))
nonopt_2 = MUL(SHL(X, ONE), Y) nonopt_2 = MUL(SHL(X, 1), Y)
# Optimized result # Optimized result
opt_1 = SHL(Y, X) 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))) Mask = SHL(B, SHR(A, Int2BV(IntVal(-1), n_bits)))
opt = If( opt = If(
UGT(A, B), UGT(A, B),
AND(SHR(a - b, x), Mask), AND(SHR(A - B, X), Mask),
If( If(
UGT(B, A), UGT(B, A),
AND(SHL(B - A, X), Mask), 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) return If(y == 0, 0, x % y)
def LT(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): 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): def SLT(x, y):
return x < y return If(x < y, BitVecVal(1, x.size()), BitVecVal(0, x.size()))
def SGT(x, y): 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): def AND(x, y):
return x & y return x & y