diff --git a/tests/laser/smt/bitvecfunc_test.py b/tests/laser/smt/bitvecfunc_test.py deleted file mode 100644 index 37217c73..00000000 --- a/tests/laser/smt/bitvecfunc_test.py +++ /dev/null @@ -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