mirror of https://github.com/ConsenSys/mythril
blockchainethereumsmart-contractssoliditysecurityprogram-analysissecurity-analysissymbolic-execution
You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
145 lines
3.3 KiB
145 lines
3.3 KiB
from mythril.laser.smt.solver.independence_solver import (
|
|
_get_expr_variables,
|
|
DependenceBucket,
|
|
DependenceMap,
|
|
IndependenceSolver,
|
|
)
|
|
from mythril.laser.smt import symbol_factory
|
|
|
|
import z3
|
|
|
|
|
|
def test_get_expr_variables():
|
|
# Arrange
|
|
x = z3.Bool("x")
|
|
y = z3.BitVec("y", 256)
|
|
z = z3.BitVec("z", 256)
|
|
b = z3.BitVec("b", 256)
|
|
expression = z3.If(x, y, z + b)
|
|
|
|
# Act
|
|
variables = list(map(str, _get_expr_variables(expression)))
|
|
|
|
# Assert
|
|
assert str(x) in variables
|
|
assert str(y) in variables
|
|
assert str(z) in variables
|
|
assert str(b) in variables
|
|
|
|
|
|
def test_get_expr_variables_num():
|
|
# Arrange
|
|
b = z3.BitVec("b", 256)
|
|
expression = b + z3.BitVecVal(2, 256)
|
|
|
|
# Act
|
|
variables = _get_expr_variables(expression)
|
|
|
|
# Assert
|
|
assert [b] == variables
|
|
|
|
|
|
def test_create_bucket():
|
|
# Arrange
|
|
x = z3.Bool("x")
|
|
|
|
# Act
|
|
bucket = DependenceBucket([x], [x])
|
|
|
|
# Assert
|
|
assert [x] == bucket.variables
|
|
assert [x] == bucket.conditions
|
|
|
|
|
|
def test_dependence_map():
|
|
# Arrange
|
|
x = z3.BitVec("x", 256)
|
|
y = z3.BitVec("y", 256)
|
|
z = z3.BitVec("z", 256)
|
|
a = z3.BitVec("a", 256)
|
|
b = z3.BitVec("b", 256)
|
|
|
|
conditions = [x > y, y == z, a == b]
|
|
|
|
dependence_map = DependenceMap()
|
|
|
|
# Act
|
|
for condition in conditions:
|
|
dependence_map.add_condition(condition)
|
|
|
|
# Assert
|
|
assert 2 == len(dependence_map.buckets)
|
|
|
|
assert x in dependence_map.buckets[0].variables
|
|
assert y in dependence_map.buckets[0].variables
|
|
assert z in dependence_map.buckets[0].variables
|
|
assert len(set(dependence_map.buckets[0].variables)) == 3
|
|
|
|
assert conditions[0] in dependence_map.buckets[0].conditions
|
|
assert conditions[1] in dependence_map.buckets[0].conditions
|
|
|
|
assert a in dependence_map.buckets[1].variables
|
|
assert b in dependence_map.buckets[1].variables
|
|
assert len(set(dependence_map.buckets[1].variables)) == 2
|
|
|
|
assert conditions[2] in dependence_map.buckets[1].conditions
|
|
|
|
|
|
def test_Independence_solver_unsat():
|
|
# Arrange
|
|
x = symbol_factory.BitVecSym("x", 256)
|
|
y = symbol_factory.BitVecSym("y", 256)
|
|
z = symbol_factory.BitVecSym("z", 256)
|
|
a = symbol_factory.BitVecSym("a", 256)
|
|
b = symbol_factory.BitVecSym("b", 256)
|
|
|
|
conditions = [x > y, y == z, y != z, a == b]
|
|
|
|
solver = IndependenceSolver()
|
|
|
|
# Act
|
|
solver.add(*conditions)
|
|
result = solver.check()
|
|
|
|
# Assert
|
|
assert z3.unsat == result
|
|
|
|
|
|
def test_independence_solver_unsat_in_second_bucket():
|
|
# Arrange
|
|
x = symbol_factory.BitVecSym("x", 256)
|
|
y = symbol_factory.BitVecSym("y", 256)
|
|
z = symbol_factory.BitVecSym("z", 256)
|
|
a = symbol_factory.BitVecSym("a", 256)
|
|
b = symbol_factory.BitVecSym("b", 256)
|
|
|
|
conditions = [x > y, y == z, a == b, a != b]
|
|
|
|
solver = IndependenceSolver()
|
|
|
|
# Act
|
|
solver.add(*conditions)
|
|
result = solver.check()
|
|
|
|
# Assert
|
|
assert z3.unsat == result
|
|
|
|
|
|
def test_independence_solver_sat():
|
|
# Arrange
|
|
x = symbol_factory.BitVecSym("x", 256)
|
|
y = symbol_factory.BitVecSym("y", 256)
|
|
z = symbol_factory.BitVecSym("z", 256)
|
|
a = symbol_factory.BitVecSym("a", 256)
|
|
b = symbol_factory.BitVecSym("b", 256)
|
|
|
|
conditions = [x > y, y == z, a == b]
|
|
|
|
solver = IndependenceSolver()
|
|
|
|
# Act
|
|
solver.add(*conditions)
|
|
result = solver.check()
|
|
|
|
# Assert
|
|
assert z3.sat == result
|
|
|