cerc-io/solidity
10
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 #11765 from ethereum/fix_byte_formal

Browse Source 
Fix implementation of BYTE
This commit is contained in:
chriseth 2021-08-09 20:38:08 +02:00 committed by GitHub
commit 74c804d87d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 23 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
test/formal/byte_big.py Normal file
View File

@ -0,0 +1,18 @@
from rule import Rule
from opcodes import *
"""
byte(A, X) -> 0
given A >= WordSize / 8
"""
rule = Rule()
n_bits = 256
# Input vars
X = BitVec('X', n_bits)
A = BitVec('A', n_bits)
rule.require(A >= n_bits / 8)
rule.check(BYTE(A, X), 0)

6
test/formal/opcodes.py
View File

@ -59,4 +59,8 @@ def SAR(x, y):
def BYTE(i, x): def BYTE(i, x):
bit = (i + 1) * 8 bit = (i + 1) * 8
return If(UGT(bit, x.size()), BitVecVal(0, x.size()), (LShR(x, (x.size() - bit))) & 0xff) return If(
UGT(i, x.size() / 8 - 1),
BitVecVal(0, x.size()),
(LShR(x, (x.size() - bit))) & 0xff
)