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

Bye Bye bitvecfunc tests

Browse Source
remove/dos
Nikhil Parasaram 5 years ago
parent a9f6d20f20
commit 9f2b2f759e
1 changed files with 0 additions and 237 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. 237
      tests/laser/smt/bitvecfunc_test.py

237
tests/laser/smt/bitvecfunc_test.py
Unescape View File

@ -1,237 +0,0 @@
from mythril.laser.smt import Solver, symbol_factory, UGT, UGE, ULT, ULE
import z3
import pytest
import operator
@pytest.mark.parametrize(
"operation,expected",
[
(operator.add, z3.unsat),
(operator.sub, z3.unsat),
(operator.and_, z3.sat),
(operator.or_, z3.sat),
(operator.xor, z3.unsat),
],
)
def test_bitvecfunc_arithmetic(operation, expected):
# Arrange
s = Solver()
input_ = symbol_factory.BitVecVal(1, 8)
bvf = symbol_factory.BitVecFuncSym("bvf", "sha3", 256, input_=input_)
x = symbol_factory.BitVecSym("x", 256)
y = symbol_factory.BitVecSym("y", 256)
# Act
s.add(x != y)
s.add(operation(bvf, x) == operation(y, bvf))
# Assert
assert s.check() == expected
@pytest.mark.parametrize(
"operation,expected",
[
(operator.eq, z3.sat),
(operator.ne, z3.unsat),
(operator.lt, z3.unsat),
(operator.le, z3.sat),
(operator.gt, z3.unsat),
(operator.ge, z3.sat),
(UGT, z3.unsat),
(UGE, z3.sat),
(ULT, z3.unsat),
(ULE, z3.sat),
],
)
def test_bitvecfunc_bitvecfunc_comparison(operation, expected):
# Arrange
s = Solver()
input1 = symbol_factory.BitVecSym("input1", 256)
input2 = symbol_factory.BitVecSym("input2", 256)
bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=input2)
# Act
s.add(operation(bvf1, bvf2))
s.add(input1 == input2)
# Assert
assert s.check() == expected
def test_bitvecfunc_bitvecfuncval_comparison():
# Arrange
s = Solver()
input1 = symbol_factory.BitVecSym("input1", 256)
input2 = symbol_factory.BitVecVal(1337, 256)
bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
bvf2 = symbol_factory.BitVecFuncVal(12345678910, "sha3", 256, input_=input2)
# Act
s.add(bvf1 == bvf2)
# Assert
assert s.check() == z3.sat
assert s.model().eval(input2.raw) == 1337
def test_bitvecfunc_nested_comparison():
# arrange
s = Solver()
input1 = symbol_factory.BitVecSym("input1", 256)
input2 = symbol_factory.BitVecSym("input2", 256)
bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1)
bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3)
# Act
s.add(input1 == input2)
s.add(bvf2 == bvf4)
# Assert
assert s.check() == z3.sat
def test_bitvecfunc_unequal_nested_comparison():
# arrange
s = Solver()
input1 = symbol_factory.BitVecSym("input1", 256)
input2 = symbol_factory.BitVecSym("input2", 256)
bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1)
bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3)
# Act
s.add(input1 != input2)
s.add(bvf2 == bvf4)
# Assert
assert s.check() == z3.unsat
def test_bitvecfunc_ext_nested_comparison():
# arrange
s = Solver()
input1 = symbol_factory.BitVecSym("input1", 256)
input2 = symbol_factory.BitVecSym("input2", 256)
input3 = symbol_factory.BitVecSym("input3", 256)
input4 = symbol_factory.BitVecSym("input4", 256)
bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1 + input3)
bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3 + input4)
# Act
s.add(input1 == input2)
s.add(input3 == input4)
s.add(bvf2 == bvf4)
# Assert
assert s.check() == z3.sat
def test_bitvecfunc_ext_unequal_nested_comparison():
# Arrange
s = Solver()
input1 = symbol_factory.BitVecSym("input1", 256)
input2 = symbol_factory.BitVecSym("input2", 256)
input3 = symbol_factory.BitVecSym("input3", 256)
input4 = symbol_factory.BitVecSym("input4", 256)
bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1 + input3)
bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3 + input4)
# Act
s.add(input1 == input2)
s.add(input3 != input4)
s.add(bvf2 == bvf4)
# Assert
assert s.check() == z3.unsat
def test_bitvecfunc_ext_unequal_nested_comparison_f():
# Arrange
s = Solver()
input1 = symbol_factory.BitVecSym("input1", 256)
input2 = symbol_factory.BitVecSym("input2", 256)
input3 = symbol_factory.BitVecSym("input3", 256)
input4 = symbol_factory.BitVecSym("input4", 256)
bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1 + input3)
bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3 + input4)
# Act
s.add(input1 != input2)
s.add(input3 == input4)
s.add(bvf2 == bvf4)
# Assert
assert s.check() == z3.unsat
def test_bitvecfunc_find_input():
# Arrange
s = Solver()
input1 = symbol_factory.BitVecSym("input1", 256)
input2 = symbol_factory.BitVecSym("input2", 256)
bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
bvf2 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
# Act
s.add(input1 == symbol_factory.BitVecVal(1, 256))
s.add(bvf1 == bvf2)
# Assert
assert s.check() == z3.sat
assert s.model()[input2.raw] == 1
def test_bitvecfunc_nested_find_input():
# Arrange
s = Solver()
input1 = symbol_factory.BitVecSym("input1", 256)
input2 = symbol_factory.BitVecSym("input2", 256)
bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1)
bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3)
# Act
s.add(input1 == symbol_factory.BitVecVal(123, 256))
s.add(bvf2 == bvf4)
# Assert
assert s.check() == z3.sat
assert s.model()[input2.raw] == 123
Write Preview
Loading…
Cancel
Save