Add solver timeout

pull/23/head
Bernhard Mueller 7 years ago
parent 1ce6fbb588
commit 247648df7a
  1. 2
      mythril/analysis/modules/unchecked_suicide.py
  2. 1
      mythril/analysis/solver.py
  3. 9
      mythril/analysis/symbolic.py

@ -57,7 +57,7 @@ def execute(statespace):
for s in statespace.sstors[index]: for s in statespace.sstors[index]:
if s.tainted: if s.tainted:
can_write = Trues can_write = True
issue.description += "\nThere is a check on storage index " + str(index) + ". This storage index can be written to by calling the function '" + s.node.function_name + "'." issue.description += "\nThere is a check on storage index " + str(index) + ". This storage index can be written to by calling the function '" + s.node.function_name + "'."
break break

@ -3,6 +3,7 @@ from mythril.exceptions import UnsatError
def get_model(constraints): def get_model(constraints):
s = Solver() s = Solver()
s.set("timeout", 2000)
for constraint in constraints: for constraint in constraints:
s.add(constraint) s.add(constraint)

@ -69,19 +69,22 @@ class StateSpace:
def sstor_analysis(self): def sstor_analysis(self):
logging.debug("Analyzing storage operations...") logging.info("Analyzing storage operations...")
for index in self.sstors: for index in self.sstors:
for s in self.sstors[index]: for s in self.sstors[index]:
# For now we simply 'taint' every storage location that is reachable without any constraint on msg.sender # For now we simply 'taint' every storage location that is reachable without any constraint on msg.sender
taint = True
for constraint in s.node.constraints: for constraint in s.node.constraints:
logging.debug("Constraint: " + str(constraint)) # logging.debug("Constraint: " + str(constraint))
if ("caller" in str(constraint)): if ("caller" in str(constraint)):
s.tainted = False taint = False
break break
if taint:
try: try:
solver.get_model(s.node.constraints) solver.get_model(s.node.constraints)
s.tainted = True s.tainted = True

Loading…
Cancel
Save