Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix for returndatasize #1612

Merged
merged 15 commits into from
Mar 5, 2020
Prev Previous commit
Next Next commit
CC
  • Loading branch information
feliam committed Feb 4, 2020
commit 939e0a10a6ffa711e8df92b60e4b655002698c16
2 changes: 1 addition & 1 deletion manticore/core/smtlib/solver.py
Original file line number Diff line number Diff line change
Expand Up @@ -401,7 +401,7 @@ def _pop(self):
"""Recall the last pushed constraint store and state."""
self._send("(pop 1)")

def can_be_true(self, constraints:ConstraintSet, expression=True):
def can_be_true(self, constraints: ConstraintSet, expression=True):
"""Check if two potentially symbolic values can be equal"""
if isinstance(expression, bool):
if not expression:
Expand Down
2 changes: 2 additions & 0 deletions manticore/ethereum/cli.py
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@
consts = config.get_group("cli")
consts.add("profile", default=False, description="Enable worker profiling mode")
consts.add("explore_balance", default=False, description="Explore states in which only the balance was changed")


def get_detectors_classes():
return [
DetectInvalid,
Expand Down
8 changes: 2 additions & 6 deletions manticore/ethereum/manticore.py
Original file line number Diff line number Diff line change
Expand Up @@ -405,7 +405,6 @@ def __init__(self, workspace_url: str = None, policy: str = "random"):
elif consts.sha3 is consts.sha3.fake:
self.subscribe("on_symbolic_function", self._on_unsound_symbolication)


self._accounts: Dict[str, EVMContract] = dict()
self._serializer = PickleSerializer()

Expand Down Expand Up @@ -583,8 +582,7 @@ def solidity_create_contract(
f"Can't create solidity contract with balance ({balance}) "
f"different than 0 because the contract's constructor is not payable."
)
elif Z3Solver.instance().can_be_true(self.constraints, Operators.UGE(self.world.get_balance(
owner.address), balance)):
elif Z3Solver.instance().can_be_true(self.constraints, Operators.UGE(self.world.get_balance(owner.address), balance)):
self.constraints.add(Operators.UGE(self.world.get_balance(owner.address), balance))
elif Z3Solver.instance().can_be_true(self.constraints, self.world.get_balance(owner.address) < balance):
raise EthereumError(
Expand Down Expand Up @@ -1137,7 +1135,6 @@ def _on_concretize(self, state, func, data, result):

result.append(y_concrete)


def _on_unsound_symbolication(self, state, func, data, result):
"""Apply the function symbolic unfriendly func to data
state: a manticore state
Expand All @@ -1162,7 +1159,7 @@ def _on_unsound_symbolication(self, state, func, data, result):
try:
value = func(data)
except Exception as e:
pass #function is unknown
pass # function is unknown

#Value is known. Let's add it to our concrete database
if value is not None:
Expand Down Expand Up @@ -1240,7 +1237,6 @@ def make_cond(state, table):
# Ok all functions had a match for current state
return state.can_be_true(True)


def fix_unsound_symbolication_sound(self, state):
""" This method goes through all the applied symbolic functions and tries
to find a concrete matching set of pairs
Expand Down
5 changes: 3 additions & 2 deletions manticore/platforms/evm.py
Original file line number Diff line number Diff line change
Expand Up @@ -54,13 +54,14 @@
# ignore: Ignore gas. Do not account for it. Do not OOG.
consts = config.get_group("evm")



def globalsha3(data):
return int(sha3.keccak_256(data).hexdigest(), 16)


def globalfakesha3(data):
return None


consts.add(
"oog",
default="complete",
Expand Down