mirror of https://github.com/ConsenSys/mythril
Nikhil Parasaram
5 years ago
commit
f74f7602cd
@ -0,0 +1,81 @@ |
||||
"""This module contains the detection code for Arbitrary jumps.""" |
||||
import logging |
||||
from mythril.analysis.solver import get_transaction_sequence, UnsatError |
||||
from mythril.analysis.modules.base import DetectionModule, Issue |
||||
from mythril.analysis.swc_data import ARBITRARY_JUMP |
||||
from mythril.laser.ethereum.state.global_state import GlobalState |
||||
|
||||
log = logging.getLogger(__name__) |
||||
|
||||
DESCRIPTION = """ |
||||
|
||||
Search for any writes to an arbitrary storage slot |
||||
""" |
||||
|
||||
|
||||
class ArbitraryJump(DetectionModule): |
||||
"""This module searches for JUMPs to an arbitrary instruction.""" |
||||
|
||||
def __init__(self): |
||||
"""""" |
||||
super().__init__( |
||||
name="Jump to an arbitrary line", |
||||
swc_id=ARBITRARY_JUMP, |
||||
description=DESCRIPTION, |
||||
entrypoint="callback", |
||||
pre_hooks=["JUMP", "JUMPI"], |
||||
) |
||||
|
||||
def reset_module(self): |
||||
""" |
||||
Resets the module by clearing everything |
||||
:return: |
||||
""" |
||||
super().reset_module() |
||||
|
||||
def _execute(self, state: GlobalState) -> None: |
||||
""" |
||||
|
||||
:param state: |
||||
:return: |
||||
""" |
||||
if state.get_current_instruction()["address"] in self.cache: |
||||
return |
||||
self.issues.extend(self._analyze_state(state)) |
||||
|
||||
@staticmethod |
||||
def _analyze_state(state): |
||||
""" |
||||
|
||||
:param state: |
||||
:return: |
||||
""" |
||||
|
||||
jump_dest = state.mstate.stack[-1] |
||||
if jump_dest.symbolic is False: |
||||
return [] |
||||
# Most probably the jump destination can have multiple locations in these circumstances |
||||
try: |
||||
transaction_sequence = get_transaction_sequence( |
||||
state, state.mstate.constraints |
||||
) |
||||
except UnsatError: |
||||
return [] |
||||
issue = Issue( |
||||
contract=state.environment.active_account.contract_name, |
||||
function_name=state.environment.active_function_name, |
||||
address=state.get_current_instruction()["address"], |
||||
swc_id=ARBITRARY_JUMP, |
||||
title="Jump to an arbitrary instruction", |
||||
severity="Medium", |
||||
bytecode=state.environment.code.bytecode, |
||||
description_head="The caller can jump to any point in the code.", |
||||
description_tail="This can lead to unintended consequences." |
||||
"Please avoid using low level code as much as possible", |
||||
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
||||
transaction_sequence=transaction_sequence, |
||||
) |
||||
return [issue] |
||||
|
||||
|
||||
detector = ArbitraryJump() |
||||
@ -1,137 +0,0 @@ |
||||
"""This module contains the detection code SWC-128 - DOS with block gas limit.""" |
||||
|
||||
import logging |
||||
from typing import Dict, cast, List |
||||
|
||||
from mythril.analysis.swc_data import DOS_WITH_BLOCK_GAS_LIMIT |
||||
from mythril.analysis.report import Issue |
||||
from mythril.analysis.modules.base import DetectionModule |
||||
from mythril.analysis.solver import get_transaction_sequence, UnsatError |
||||
from mythril.analysis.analysis_args import analysis_args |
||||
from mythril.laser.ethereum.state.global_state import GlobalState |
||||
from mythril.laser.ethereum.state.annotation import StateAnnotation |
||||
from mythril.laser.ethereum import util |
||||
from copy import copy |
||||
|
||||
log = logging.getLogger(__name__) |
||||
|
||||
|
||||
class VisitsAnnotation(StateAnnotation): |
||||
"""State annotation that stores the addresses of state-modifying operations""" |
||||
|
||||
def __init__(self) -> None: |
||||
self.loop_start = None # type: int |
||||
self.jump_targets = {} # type: Dict[int, int] |
||||
|
||||
def __copy__(self): |
||||
result = VisitsAnnotation() |
||||
|
||||
result.loop_start = self.loop_start |
||||
result.jump_targets = copy(self.jump_targets) |
||||
return result |
||||
|
||||
|
||||
class DosModule(DetectionModule): |
||||
"""This module consists of a makeshift loop detector that annotates the state with |
||||
a list of byte ranges likely to be loops. If a CALL or SSTORE detection is found in |
||||
one of the ranges it creates a low-severity issue. This is not super precise but |
||||
good enough to identify places that warrant a closer look. Checking the loop condition |
||||
would be a possible improvement. |
||||
""" |
||||
|
||||
def __init__(self) -> None: |
||||
"""""" |
||||
super().__init__( |
||||
name="DOS", |
||||
swc_id=DOS_WITH_BLOCK_GAS_LIMIT, |
||||
description="Check for DOS", |
||||
entrypoint="callback", |
||||
pre_hooks=["JUMP", "JUMPI", "CALL", "SSTORE"], |
||||
) |
||||
|
||||
def _execute(self, state: GlobalState) -> None: |
||||
|
||||
""" |
||||
:param state: |
||||
:return: |
||||
""" |
||||
issues = self._analyze_state(state) |
||||
self.issues.extend(issues) |
||||
|
||||
def _analyze_state(self, state: GlobalState) -> List[Issue]: |
||||
""" |
||||
:param state: the current state |
||||
:return: returns the issues for that corresponding state |
||||
""" |
||||
|
||||
opcode = state.get_current_instruction()["opcode"] |
||||
address = state.get_current_instruction()["address"] |
||||
|
||||
annotations = cast( |
||||
List[VisitsAnnotation], list(state.get_annotations(VisitsAnnotation)) |
||||
) |
||||
|
||||
if len(annotations) == 0: |
||||
annotation = VisitsAnnotation() |
||||
state.annotate(annotation) |
||||
else: |
||||
annotation = annotations[0] |
||||
|
||||
if opcode in ["JUMP", "JUMPI"]: |
||||
|
||||
if annotation.loop_start is not None: |
||||
return [] |
||||
try: |
||||
target = util.get_concrete_int(state.mstate.stack[-1]) |
||||
except TypeError: |
||||
log.debug("Symbolic target encountered in dos module") |
||||
return [] |
||||
if target in annotation.jump_targets: |
||||
annotation.jump_targets[target] += 1 |
||||
else: |
||||
annotation.jump_targets[target] = 1 |
||||
|
||||
if annotation.jump_targets[target] > min(2, analysis_args.loop_bound - 1): |
||||
annotation.loop_start = address |
||||
|
||||
elif annotation.loop_start is not None: |
||||
|
||||
if opcode == "CALL": |
||||
operation = "A message call" |
||||
else: |
||||
operation = "A storage modification" |
||||
|
||||
description_head = ( |
||||
"Potential denial-of-service if block gas limit is reached." |
||||
) |
||||
description_tail = "{} is executed in a loop. Be aware that the transaction may fail to execute if the loop is unbounded and the necessary gas exceeds the block gas limit.".format( |
||||
operation |
||||
) |
||||
|
||||
try: |
||||
transaction_sequence = get_transaction_sequence( |
||||
state, state.mstate.constraints |
||||
) |
||||
except UnsatError: |
||||
return [] |
||||
|
||||
issue = Issue( |
||||
contract=state.environment.active_account.contract_name, |
||||
function_name=state.environment.active_function_name, |
||||
address=annotation.loop_start, |
||||
swc_id=DOS_WITH_BLOCK_GAS_LIMIT, |
||||
bytecode=state.environment.code.bytecode, |
||||
title="Potential denial-of-service if block gas limit is reached", |
||||
severity="Low", |
||||
description_head=description_head, |
||||
description_tail=description_tail, |
||||
gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), |
||||
transaction_sequence=transaction_sequence, |
||||
) |
||||
|
||||
return [issue] |
||||
|
||||
return [] |
||||
|
||||
|
||||
detector = DosModule() |
||||
@ -1,297 +0,0 @@ |
||||
import operator |
||||
from itertools import product |
||||
from typing import Optional, Union, cast, Callable, List |
||||
import z3 |
||||
|
||||
from mythril.laser.smt.bitvec import BitVec, Annotations, _padded_operation |
||||
from mythril.laser.smt.bool import Or, Bool, And |
||||
|
||||
|
||||
def _arithmetic_helper( |
||||
a: "BitVecFunc", b: Union[BitVec, int], operation: Callable |
||||
) -> "BitVecFunc": |
||||
""" |
||||
Helper function for arithmetic operations on BitVecFuncs. |
||||
|
||||
:param a: The BitVecFunc to perform the operation on. |
||||
:param b: A BitVec or int to perform the operation on. |
||||
:param operation: The arithmetic operation to perform. |
||||
:return: The resulting BitVecFunc |
||||
""" |
||||
if isinstance(b, int): |
||||
b = BitVec(z3.BitVecVal(b, a.size())) |
||||
|
||||
raw = operation(a.raw, b.raw) |
||||
union = a.annotations.union(b.annotations) |
||||
|
||||
if isinstance(b, BitVecFunc): |
||||
return BitVecFunc( |
||||
raw=raw, |
||||
func_name="Hybrid", |
||||
input_=BitVec(z3.BitVec("", 256), annotations=union), |
||||
nested_functions=a.nested_functions + b.nested_functions + [a, b], |
||||
) |
||||
|
||||
return BitVecFunc( |
||||
raw=raw, |
||||
func_name=a.func_name, |
||||
input_=a.input_, |
||||
annotations=union, |
||||
nested_functions=a.nested_functions + [a], |
||||
) |
||||
|
||||
|
||||
def _comparison_helper( |
||||
a: "BitVecFunc", |
||||
b: Union[BitVec, int], |
||||
operation: Callable, |
||||
default_value: bool, |
||||
inputs_equal: bool, |
||||
) -> Bool: |
||||
""" |
||||
Helper function for comparison operations with BitVecFuncs. |
||||
|
||||
:param a: The BitVecFunc to compare. |
||||
:param b: A BitVec or int to compare to. |
||||
:param operation: The comparison operation to perform. |
||||
:return: The resulting Bool |
||||
""" |
||||
# Is there some hack for gt/lt comparisons? |
||||
if isinstance(b, int): |
||||
b = BitVec(z3.BitVecVal(b, a.size())) |
||||
union = a.annotations.union(b.annotations) |
||||
|
||||
if not a.symbolic and not b.symbolic: |
||||
if operation == z3.UGT: |
||||
operation = operator.gt |
||||
if operation == z3.ULT: |
||||
operation = operator.lt |
||||
return Bool(z3.BoolVal(operation(a.value, b.value)), annotations=union) |
||||
if ( |
||||
not isinstance(b, BitVecFunc) |
||||
or not a.func_name |
||||
or not a.input_ |
||||
or not a.func_name == b.func_name |
||||
or str(operation) not in ("<built-in function eq>", "<built-in function ne>") |
||||
): |
||||
return Bool(z3.BoolVal(default_value), annotations=union) |
||||
|
||||
condition = True |
||||
for a_nest, b_nest in product(a.nested_functions, b.nested_functions): |
||||
if a_nest.func_name != b_nest.func_name: |
||||
continue |
||||
if a_nest.func_name == "Hybrid": |
||||
continue |
||||
# a.input (eq/neq) b.input ==> a == b |
||||
if inputs_equal: |
||||
condition = z3.And( |
||||
condition, |
||||
z3.Or( |
||||
z3.Not((a_nest.input_ == b_nest.input_).raw), |
||||
(a_nest.raw == b_nest.raw), |
||||
), |
||||
z3.Or( |
||||
z3.Not((a_nest.raw == b_nest.raw)), |
||||
(a_nest.input_ == b_nest.input_).raw, |
||||
), |
||||
) |
||||
else: |
||||
condition = z3.And( |
||||
condition, |
||||
z3.Or( |
||||
z3.Not((a_nest.input_ != b_nest.input_).raw), |
||||
(a_nest.raw == b_nest.raw), |
||||
), |
||||
z3.Or( |
||||
z3.Not((a_nest.raw == b_nest.raw)), |
||||
(a_nest.input_ != b_nest.input_).raw, |
||||
), |
||||
) |
||||
|
||||
return And( |
||||
Bool( |
||||
cast(z3.BoolRef, _padded_operation(a.raw, b.raw, operation)), |
||||
annotations=union, |
||||
), |
||||
Bool(condition) if b.nested_functions else Bool(True), |
||||
a.input_ == b.input_ if inputs_equal else a.input_ != b.input_, |
||||
) |
||||
|
||||
|
||||
class BitVecFunc(BitVec): |
||||
"""A bit vector function symbol. Used in place of functions like sha3.""" |
||||
|
||||
def __init__( |
||||
self, |
||||
raw: z3.BitVecRef, |
||||
func_name: Optional[str], |
||||
input_: "BitVec" = None, |
||||
annotations: Optional[Annotations] = None, |
||||
nested_functions: Optional[List["BitVecFunc"]] = None, |
||||
): |
||||
""" |
||||
|
||||
:param raw: The raw bit vector symbol |
||||
:param func_name: The function name. e.g. sha3 |
||||
:param input: The input to the functions |
||||
:param annotations: The annotations the BitVecFunc should start with |
||||
""" |
||||
|
||||
self.func_name = func_name |
||||
self.input_ = input_ |
||||
self.nested_functions = nested_functions or [] |
||||
self.nested_functions = list(dict.fromkeys(self.nested_functions)) |
||||
if isinstance(input_, BitVecFunc): |
||||
self.nested_functions.extend(input_.nested_functions) |
||||
super().__init__(raw, annotations) |
||||
|
||||
def __add__(self, other: Union[int, "BitVec"]) -> "BitVecFunc": |
||||
"""Create an addition expression. |
||||
|
||||
:param other: The int or BitVec to add to this BitVecFunc |
||||
:return: The resulting BitVecFunc |
||||
""" |
||||
return _arithmetic_helper(self, other, operator.add) |
||||
|
||||
def __sub__(self, other: Union[int, "BitVec"]) -> "BitVecFunc": |
||||
"""Create a subtraction expression. |
||||
|
||||
:param other: The int or BitVec to subtract from this BitVecFunc |
||||
:return: The resulting BitVecFunc |
||||
""" |
||||
return _arithmetic_helper(self, other, operator.sub) |
||||
|
||||
def __mul__(self, other: "BitVec") -> "BitVecFunc": |
||||
"""Create a multiplication expression. |
||||
|
||||
:param other: The int or BitVec to multiply to this BitVecFunc |
||||
:return: The resulting BitVecFunc |
||||
""" |
||||
return _arithmetic_helper(self, other, operator.mul) |
||||
|
||||
def __truediv__(self, other: "BitVec") -> "BitVecFunc": |
||||
"""Create a signed division expression. |
||||
|
||||
:param other: The int or BitVec to divide this BitVecFunc by |
||||
:return: The resulting BitVecFunc |
||||
""" |
||||
return _arithmetic_helper(self, other, operator.truediv) |
||||
|
||||
def __and__(self, other: Union[int, "BitVec"]) -> "BitVecFunc": |
||||
"""Create an and expression. |
||||
|
||||
:param other: The int or BitVec to and with this BitVecFunc |
||||
:return: The resulting BitVecFunc |
||||
""" |
||||
return _arithmetic_helper(self, other, operator.and_) |
||||
|
||||
def __or__(self, other: Union[int, "BitVec"]) -> "BitVecFunc": |
||||
"""Create an or expression. |
||||
|
||||
:param other: The int or BitVec to or with this BitVecFunc |
||||
:return: The resulting BitVecFunc |
||||
""" |
||||
if not isinstance(other, BitVec): |
||||
other = BitVec(z3.BitVecVal(other, self.size())) |
||||
return _arithmetic_helper(self, other, operator.or_) |
||||
|
||||
def __xor__(self, other: Union[int, "BitVec"]) -> "BitVecFunc": |
||||
"""Create a xor expression. |
||||
|
||||
:param other: The int or BitVec to xor with this BitVecFunc |
||||
:return: The resulting BitVecFunc |
||||
""" |
||||
if not isinstance(other, BitVec): |
||||
other = BitVec(z3.BitVecVal(other, self.size())) |
||||
return _arithmetic_helper(self, other, operator.xor) |
||||
|
||||
def __lt__(self, other: Union[int, "BitVec"]) -> Bool: |
||||
"""Create a signed less than expression. |
||||
|
||||
:param other: The int or BitVec to compare to this BitVecFunc |
||||
:return: The resulting Bool |
||||
""" |
||||
if not isinstance(other, BitVec): |
||||
other = BitVec(z3.BitVecVal(other, self.size())) |
||||
return _comparison_helper( |
||||
self, other, operator.lt, default_value=False, inputs_equal=False |
||||
) |
||||
|
||||
def __gt__(self, other: Union[int, "BitVec"]) -> Bool: |
||||
"""Create a signed greater than expression. |
||||
|
||||
:param other: The int or BitVec to compare to this BitVecFunc |
||||
:return: The resulting Bool |
||||
""" |
||||
if not isinstance(other, BitVec): |
||||
other = BitVec(z3.BitVecVal(other, self.size())) |
||||
return _comparison_helper( |
||||
self, other, operator.gt, default_value=False, inputs_equal=False |
||||
) |
||||
|
||||
def __le__(self, other: Union[int, "BitVec"]) -> Bool: |
||||
"""Create a signed less than or equal to expression. |
||||
|
||||
:param other: The int or BitVec to compare to this BitVecFunc |
||||
:return: The resulting Bool |
||||
""" |
||||
if not isinstance(other, BitVec): |
||||
other = BitVec(z3.BitVecVal(other, self.size())) |
||||
return Or(self < other, self == other) |
||||
|
||||
def __ge__(self, other: Union[int, "BitVec"]) -> Bool: |
||||
"""Create a signed greater than or equal to expression. |
||||
|
||||
:param other: The int or BitVec to compare to this BitVecFunc |
||||
:return: The resulting Bool |
||||
""" |
||||
if not isinstance(other, BitVec): |
||||
other = BitVec(z3.BitVecVal(other, self.size())) |
||||
return Or(self > other, self == other) |
||||
|
||||
# MYPY: fix complains about overriding __eq__ |
||||
def __eq__(self, other: Union[int, "BitVec"]) -> Bool: # type: ignore |
||||
"""Create an equality expression. |
||||
|
||||
:param other: The int or BitVec to compare to this BitVecFunc |
||||
:return: The resulting Bool |
||||
""" |
||||
|
||||
if not isinstance(other, BitVec): |
||||
other = BitVec(z3.BitVecVal(other, self.size())) |
||||
|
||||
return _comparison_helper( |
||||
self, other, operator.eq, default_value=False, inputs_equal=True |
||||
) |
||||
|
||||
# MYPY: fix complains about overriding __ne__ |
||||
def __ne__(self, other: Union[int, "BitVec"]) -> Bool: # type: ignore |
||||
"""Create an inequality expression. |
||||
|
||||
:param other: The int or BitVec to compare to this BitVecFunc |
||||
:return: The resulting Bool |
||||
""" |
||||
if not isinstance(other, BitVec): |
||||
other = BitVec(z3.BitVecVal(other, self.size())) |
||||
return _comparison_helper( |
||||
self, other, operator.ne, default_value=True, inputs_equal=False |
||||
) |
||||
|
||||
def __lshift__(self, other: Union[int, "BitVec"]) -> "BitVec": |
||||
""" |
||||
Left shift operation |
||||
:param other: The int or BitVec to shift on |
||||
:return The resulting left shifted output |
||||
""" |
||||
return _arithmetic_helper(self, other, operator.lshift) |
||||
|
||||
def __rshift__(self, other: Union[int, "BitVec"]) -> "BitVec": |
||||
""" |
||||
Right shift operation |
||||
:param other: The int or BitVec to shift on |
||||
:return The resulting right shifted output: |
||||
""" |
||||
return _arithmetic_helper(self, other, operator.rshift) |
||||
|
||||
def __hash__(self) -> int: |
||||
return self.raw.__hash__() |
||||
@ -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 |
||||
Loading…
Reference in new issue