TheDude
/
mythril
mirror of https://github.com/ConsenSys/mythril
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Add the BitWise instructions

Browse Source
pull/963/head
Nikhil Parasaram 6 years ago
parent e2e86aa1be
commit 7cc9a3de8f
7 changed files with 468 additions and 0 deletions
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Show Stats Download Patch File Download Diff File
  1. 8
      mythril/laser/ethereum/gas.py
  2. 42
      mythril/laser/ethereum/instructions.py
  3. 1
      mythril/laser/smt/__init__.py
  4. 21
      mythril/laser/smt/bitvec.py
  5. 148
      tests/instructions/sar_test.py
  6. 123
      tests/instructions/shl_test.py
  7. 125
      tests/instructions/shr_test.py

8
mythril/laser/ethereum/gas.py
Unescape View File

@ -62,6 +62,9 @@ OPCODE_GAS = {
"XOR": (3, 3),
"NOT": (3, 3),
"BYTE": (3, 3),
"SHL": (3, 3),
"SHR": (3, 3),
"SAR": (3, 3),
"SHA3": (
30,
30 + 6 * 8,
@ -80,6 +83,7 @@ OPCODE_GAS = {
"GASPRICE": (2, 2),
"EXTCODESIZE": (700, 700),
"EXTCODECOPY": (700, 700 + 3 * 768), # https://ethereum.stackexchange.com/a/47556
"EXTCODEHASH": (400, 400),
"RETURNDATASIZE": (2, 2),
"RETURNDATACOPY": (3, 3),
"BLOCKHASH": (20, 20),
@ -176,6 +180,10 @@ OPCODE_GAS = {
"LOG3": (4 * 375, 4 * 375 + 8 * 32),
"LOG4": (5 * 375, 5 * 375 + 8 * 32),
"CREATE": (32000, 32000),
"CREATE2": (
32000,
32000,
), # TODO: The gas value is dynamic, to be done while implementing create2
"CALL": (700, 700 + 9000 + 25000),
"NATIVE_COST": calculate_native_gas,
"CALLCODE": (700, 700 + 9000 + 25000),

42
mythril/laser/ethereum/instructions.py
Unescape View File

@ -26,6 +26,7 @@ from mythril.laser.smt import (
Bool,
Or,
Not,
LShR,
)
from mythril.laser.smt import symbol_factory
@ -464,6 +465,33 @@ class Instruction:
global_state.mstate.stack.append(0 if s1 == 0 else URem(s0, s1))
return [global_state]
@StateTransition()
def shl_(self, global_state: GlobalState) -> List[GlobalState]:
shift, value = (
util.pop_bitvec(global_state.mstate),
util.pop_bitvec(global_state.mstate),
)
global_state.mstate.stack.append(value << shift)
return [global_state]
@StateTransition()
def shr_(self, global_state: GlobalState) -> List[GlobalState]:
shift, value = (
util.pop_bitvec(global_state.mstate),
util.pop_bitvec(global_state.mstate),
)
global_state.mstate.stack.append(LShR(value, shift))
return [global_state]
@StateTransition()
def sar_(self, global_state: GlobalState) -> List[GlobalState]:
shift, value = (
util.pop_bitvec(global_state.mstate),
util.pop_bitvec(global_state.mstate),
)
global_state.mstate.stack.append(value >> shift)
return [global_state]
@StateTransition()
def smod_(self, global_state: GlobalState) -> List[GlobalState]:
"""
@ -1082,6 +1110,20 @@ class Instruction:
return [global_state]
@StateTransition
def extcodehash_(self, global_state: GlobalState) -> List[GlobalState]:
"""
:param global_state:
:return: List of global states possible, list of size 1 in this case
"""
# TODO: To be implemented
address = global_state.mstate.stack.pop()
global_state.mstate.stack.append(
global_state.new_bitvec("extcodehash_{}".format(str(address)), 256)
)
return [global_state]
@StateTransition()
def extcodecopy_(self, global_state: GlobalState) -> List[GlobalState]:
"""

1
mythril/laser/smt/__init__.py
Unescape View File

@ -13,6 +13,7 @@ from mythril.laser.smt.bitvec import (
BVAddNoOverflow,
BVMulNoOverflow,
BVSubNoUnderflow,
LShR,
)
from mythril.laser.smt.bitvecfunc import BitVecFunc
from mythril.laser.smt.expression import Expression, simplify

21
mythril/laser/smt/bitvec.py
Unescape View File

@ -211,6 +211,22 @@ class BitVec(Expression[z3.BitVecRef]):
# MYPY: fix complaints due to z3 overriding __eq__
return Bool(cast(z3.BoolRef, self.raw != other.raw), annotations=union)
def __lshift__(self, other: Union[int, "BitVec"]) -> "BitVec":
if not isinstance(other, BitVec):
return BitVec(
self.raw << other, annotations=self.annotations
)
union = self.annotations + other.annotations
return BitVec(self.raw << other.raw, annotations=union)
def __rshift__(self, other: Union[int, "BitVec"]) -> "BitVec":
if not isinstance(other, BitVec):
return BitVec(
self.raw >> other, annotations=self.annotations
)
union = self.annotations + other.annotations
return BitVec(self.raw >> other.raw, annotations=union)
def _comparison_helper(
a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool
@ -254,6 +270,11 @@ def _arithmetic_helper(a: BitVec, b: BitVec, operation: Callable) -> BitVec:
return BitVec(raw, annotations=union)
def LShR(a, b):
union = a.annotations + b.annotations
return BitVec(z3.LShR(a.raw, b.raw), annotations=union)
def If(a: Union[Bool, bool], b: Union[BitVec, int], c: Union[BitVec, int]) -> BitVec:
"""Create an if-then-else expression.

148
tests/instructions/sar_test.py
Unescape View File

@ -0,0 +1,148 @@
import pytest
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.ethereum.state.environment import Environment
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.state.machine_state import MachineState
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.instructions import Instruction
from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction
from mythril.laser.smt import symbol_factory, simplify
def get_state():
active_account = Account("0x0", code=Disassembly("60606040"))
environment = Environment(active_account, None, None, None, None, None)
state = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
state.transaction_stack.append(
(MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
)
return state
BVV = symbol_factory.BitVecVal
BV = symbol_factory.BitVecSym
test_data = (
([BVV(-1, 256), BVV(1, 256)], BVV(-1, 256)),
([BVV(23, 256), BVV(257, 256)], BVV(0, 256)),
([BVV(23, 256), BVV(30, 256)], BVV(23 >> 30, 256)),
([BVV(-10, 256), BVV(10, 256)], BVV(-1, 256)),
([BV("a", 256), BV("b", 256)], BV("a", 256) >> BV("b", 256)),
)
@pytest.mark.parametrize("inputs,output", test_data)
def test_sar(inputs, output):
# Arrange
state = get_state()
state.mstate.stack = inputs
instruction = Instruction("sar", dynamic_loader=None)
# Act
new_state = instruction.evaluate(state)[0]
# Assert
assert simplify(new_state.mstate.stack[-1]) == output
@pytest.mark.parametrize(
# Test cases from https://github.com/ethereum/EIPs/blob/master/EIPS/eip-145.md#sar-arithmetic-shift-right
"val1, val2, expected ",
(
(
"0x0000000000000000000000000000000000000000000000000000000000000001",
"0x00",
"0x0000000000000000000000000000000000000000000000000000000000000001",
),
(
"0x0000000000000000000000000000000000000000000000000000000000000001",
"0x01",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
(
"0x8000000000000000000000000000000000000000000000000000000000000000",
"0x01",
"0xc000000000000000000000000000000000000000000000000000000000000000",
),
(
"0x8000000000000000000000000000000000000000000000000000000000000000",
"0xff",
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
),
(
"0x8000000000000000000000000000000000000000000000000000000000000000",
"0x0100",
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
),
(
"0x8000000000000000000000000000000000000000000000000000000000000000",
"0x0101",
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
),
(
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0x00",
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
),
(
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0x01",
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
),
(
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0xff",
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
),
(
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0x0100",
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
),
(
"0x0000000000000000000000000000000000000000000000000000000000000000",
"0x01",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
(
"0x4000000000000000000000000000000000000000000000000000000000000000",
"0xfe",
"0x0000000000000000000000000000000000000000000000000000000000000001",
),
(
"0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0xf8",
"0x000000000000000000000000000000000000000000000000000000000000007f",
),
(
"0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0xfe",
"0x0000000000000000000000000000000000000000000000000000000000000001",
),
(
"0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0xff",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
(
"0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0x0100",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
),
)
def test_concrete_sar(val1, val2, expected):
# Arrange
state = get_state()
state.mstate.stack = [BVV(int(val1, 16), 256), BVV(int(val2, 16), 256)]
expected = BVV(int(expected, 16), 256)
instruction = Instruction("sar", dynamic_loader=None)
# Act
new_state = instruction.evaluate(state)[0]
# Assert
assert simplify(new_state.mstate.stack[-1]) == expected

123
tests/instructions/shl_test.py
Unescape View File

@ -0,0 +1,123 @@
import pytest
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.ethereum.state.environment import Environment
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.state.machine_state import MachineState
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.instructions import Instruction
from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction
from mythril.laser.smt import symbol_factory, simplify
def get_state():
active_account = Account("0x0", code=Disassembly("60606040"))
environment = Environment(active_account, None, None, None, None, None)
state = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
state.transaction_stack.append(
(MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
)
return state
BVV = symbol_factory.BitVecVal
BV = symbol_factory.BitVecSym
test_data = (
([BVV(2, 256), BVV(2, 256)], BVV(8, 256)),
([BVV(23, 256), BVV(257, 256)], BVV(0, 256)),
([BVV(23, 256), BVV(30, 256)], BVV(23 * (1 << 30), 256)),
([BV("a", 256), BVV(270, 256)], 0),
([BV("a", 256), BV("b", 256)], BV("a", 256) << BV("b", 256)),
)
@pytest.mark.parametrize("inputs,output,", test_data)
def test_shl(inputs, output):
# Arrange
state = get_state()
state.mstate.stack = inputs
instruction = Instruction("shl", dynamic_loader=None)
# Act
new_state = instruction.evaluate(state)[0]
# Assert
assert simplify(new_state.mstate.stack[-1]) == output
@pytest.mark.parametrize(
# Testcases from https://github.com/ethereum/EIPs/blob/master/EIPS/eip-145.md#shl-shift-left
"val1, val2, expected",
(
(
"0x0000000000000000000000000000000000000000000000000000000000000001",
"0x00",
"0x0000000000000000000000000000000000000000000000000000000000000001",
),
(
"0x0000000000000000000000000000000000000000000000000000000000000001",
"0x01",
"0x0000000000000000000000000000000000000000000000000000000000000002",
),
(
"0x0000000000000000000000000000000000000000000000000000000000000001",
"0xff",
"0x8000000000000000000000000000000000000000000000000000000000000000",
),
(
"0x0000000000000000000000000000000000000000000000000000000000000001",
"0x0100",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
(
"0x0000000000000000000000000000000000000000000000000000000000000001",
"0x0101",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
(
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0x00",
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
),
(
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0x01",
"0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe",
),
(
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0xff",
"0x8000000000000000000000000000000000000000000000000000000000000000",
),
(
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0x0100",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
(
"0x0000000000000000000000000000000000000000000000000000000000000000",
"0x01",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
(
"0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0x01",
"0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe",
),
),
)
def test_concrete_shl(val1, val2, expected):
# Arrange
state = get_state()
state.mstate.stack = [BVV(int(val1, 16), 256), BVV(int(val2, 16), 256)]
expected = BVV(int(expected, 16), 256)
instruction = Instruction("shl", dynamic_loader=None)
# Act
new_state = instruction.evaluate(state)[0]
# Assert
assert simplify(new_state.mstate.stack[-1]) == expected

125
tests/instructions/shr_test.py
Unescape View File

@ -0,0 +1,125 @@
import pytest
from mythril.disassembler.disassembly import Disassembly
from mythril.laser.ethereum.state.environment import Environment
from mythril.laser.ethereum.state.account import Account
from mythril.laser.ethereum.state.machine_state import MachineState
from mythril.laser.ethereum.state.global_state import GlobalState
from mythril.laser.ethereum.state.world_state import WorldState
from mythril.laser.ethereum.instructions import Instruction
from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction
from mythril.laser.smt import symbol_factory, simplify, LShR
def get_state():
active_account = Account("0x0", code=Disassembly("60606040"))
environment = Environment(active_account, None, None, None, None, None)
state = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
state.transaction_stack.append(
(MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
)
return state
BVV = symbol_factory.BitVecVal
BV = symbol_factory.BitVecSym
test_data = (
([BVV(33, 256), BVV(4, 256)], BVV(2, 256)),
([BVV(1 << 100, 256), BVV(257, 256)], BVV(0, 256)),
([BVV(23233, 256), BVV(10, 256)], BVV(23233 // (1 << 10), 256)),
([BV("a", 256), BVV(270, 256)], 0),
(
[BV("a", 256), BV("b", 256)],
LShR(BV("a", 256), BV("b", 256)),
), # Current approximate specs
)
@pytest.mark.parametrize("inputs,output,", test_data)
def test_shr(inputs, output):
# Arrange
state = get_state()
state.mstate.stack = inputs
instruction = Instruction("shr", dynamic_loader=None)
# Act
new_state = instruction.evaluate(state)[0]
# Assert
assert simplify(new_state.mstate.stack[-1]) == output
@pytest.mark.parametrize(
# Cases: https://github.com/ethereum/EIPs/blob/master/EIPS/eip-145.md#shr-logical-shift-right
"val1, val2, expected",
(
(
"0x0000000000000000000000000000000000000000000000000000000000000001",
"0x00",
"0x0000000000000000000000000000000000000000000000000000000000000001",
),
(
"0x0000000000000000000000000000000000000000000000000000000000000001",
"0x01",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
(
"0x8000000000000000000000000000000000000000000000000000000000000000",
"0x01",
"0x4000000000000000000000000000000000000000000000000000000000000000",
),
(
"0x8000000000000000000000000000000000000000000000000000000000000000",
"0xff",
"0x0000000000000000000000000000000000000000000000000000000000000001",
),
(
"0x8000000000000000000000000000000000000000000000000000000000000000",
"0x0100",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
(
"0x8000000000000000000000000000000000000000000000000000000000000000",
"0x0101",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
(
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0x00",
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
),
(
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0x01",
"0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
),
(
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0xff",
"0x0000000000000000000000000000000000000000000000000000000000000001",
),
(
"0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
"0x0100",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
(
"0x0000000000000000000000000000000000000000000000000000000000000000",
"0x01",
"0x0000000000000000000000000000000000000000000000000000000000000000",
),
),
)
def test_concrete_shr(val1, val2, expected):
state = get_state()
state.mstate.stack = [BVV(int(val1, 16), 256), BVV(int(val2, 16), 256)]
expected = BVV(int(expected, 16), 256)
instruction = Instruction("shr", dynamic_loader=None)
# Act
new_state = instruction.evaluate(state)[0]
# Assert
assert simplify(new_state.mstate.stack[-1]) == expected
Write Preview
Loading…
Cancel
Save