Secure your code as it's written. Use Snyk Code to scan source code in minutes - no build needed - and fix issues immediately.
def _try_constraints(constraints, new_constraints):
"""Tries new constraints.
:param constraints:
:param new_constraints:
:return Model if satisfiable otherwise None
"""
_constraints = copy.deepcopy(constraints)
for constraint in new_constraints:
_constraints.append(copy.deepcopy(constraint))
try:
model = solver.get_model(_constraints)
return model
except UnsatError:
return None
def _is_precompile_call(global_state: GlobalState):
to = global_state.mstate.stack[-2] # type: BitVec
constraints = copy(global_state.world_state.constraints)
constraints += [
Or(
to < symbol_factory.BitVecVal(1, 256),
to > symbol_factory.BitVecVal(PRECOMPILE_COUNT, 256),
)
]
try:
solver.get_model(constraints)
return False
except UnsatError:
return True
for dependency in dependencies:
# Is there a known read operation along this path that matches a write in the previous transaction?
try:
solver.get_model((location == dependency,))
return True
except UnsatError:
continue
# Has the *currently executed* path been influenced by a write operation in the previous transaction?
for dependency in annotation.storage_loaded:
try:
solver.get_model((location == dependency,))
return True
except UnsatError:
continue
return False
constraints = copy(global_state.mstate.constraints)
solver.get_model(
constraints
+ [
UGT(gas, symbol_factory.BitVecVal(2300, 256)),
Or(
to > symbol_factory.BitVecVal(16, 256),
to == symbol_factory.BitVecVal(0, 256),
),
]
)
# Check whether we can also set the callee address
try:
constraints += [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF]
solver.get_model(constraints)
global_state.annotate(StateChangeCallsAnnotation(global_state, True))
except UnsatError:
global_state.annotate(StateChangeCallsAnnotation(global_state, False))
except UnsatError:
pass
def _can_change(self, constraints, variable):
"""Checks if the variable can change given some constraints.
:param constraints:
:param variable:
:return:
"""
_constraints = copy.deepcopy(constraints)
try:
model = solver.get_model(_constraints)
except UnsatError:
return False
try:
initial_value = int(str(model.eval(variable, model_completion=True)))
return (
self._try_constraints(constraints, [variable != initial_value])
is not None
)
except AttributeError:
return False
:param storage_write_cache
"""
storage_write_cache = annotation.get_storage_write_cache(self.iteration - 1)
# Skip "pure" paths that don't have any dependencies.
if address not in self.sloads_on_path:
return False
# Execute the path if there are state modifications along it that *could* be relevant
if address in self.storage_accessed_global:
for location in self.sstores_on_path:
try:
solver.get_model((location == address,))
return True
except UnsatError:
continue
dependencies = self.sloads_on_path[address]
# Execute the path if there's any dependency on state modified in the previous transaction
for location in storage_write_cache:
for dependency in dependencies:
# Is there a known read operation along this path that matches a write in the previous transaction?
try:
solver.get_model((location == dependency,))
def concretize_ite_storage(self, global_state):
sender = global_state.environment.sender
models_tuple = []
sat = False
for actor in ACTOR_ADDRESSES:
try:
models_tuple.append(
(
get_model(
constraints=global_state.mstate.constraints
+ [sender == actor]
),
sender == actor,
)
)
sat = True
except UnsatError:
models_tuple.append((None, sender == actor))
import random, sha3
calldata_cond = True
for account in global_state.world_state.accounts.values():
for key in account.storage._ite_region.itedict:
if (
isinstance(key, BitVecFunc)
elif opcode == "BLOCKHASH":
param = state.mstate.stack[-1]
try:
constraint = [
ULT(param, state.environment.block_number),
ULT(
state.environment.block_number,
symbol_factory.BitVecVal(2 ** 255, 256),
),
]
# Why the second constraint? Because without it Z3 returns a solution where param overflows.
solver.get_model(state.mstate.constraints + constraint)
state.annotate(OldBlockNumberUsedAnnotation(constraint))
except UnsatError:
pass
else:
# we're in post hook
opcode = state.environment.code.instruction_list[state.mstate.pc - 1][
"opcode"
]
if opcode == "BLOCKHASH":
# if we're in the post hook of a BLOCKHASH op, check if an old block number was used to create it.
annotations = cast(
def _add_external_call(global_state: GlobalState) -> None:
gas = global_state.mstate.stack[-1]
to = global_state.mstate.stack[-2]
try:
constraints = copy(global_state.mstate.constraints)
solver.get_model(
constraints
+ [
UGT(gas, symbol_factory.BitVecVal(2300, 256)),
Or(
to > symbol_factory.BitVecVal(16, 256),
to == symbol_factory.BitVecVal(0, 256),
),
]
)
# Check whether we can also set the callee address
try:
constraints += [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF]
solver.get_model(constraints)
global_state.annotate(StateChangeCallsAnnotation(global_state, True))