From 8e4cd7f487b13417a7b3ec542857a3e96632b5cc Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Sat, 12 May 2018 18:27:00 +0200 Subject: [PATCH] Use only one _try constraint call. Cleans up this method. Also add non zero checks to initial constraint (multiplication) --- mythril/analysis/modules/integer.py | 17 ++--------------- 1 file changed, 2 insertions(+), 15 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index 310ad650..25c639e9 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -74,7 +74,7 @@ def _check_integer_overflow(statespace, state, node): expr = op1 * op0 # Check satisfiable - constraint = Or(ULT(expr, op0), ULT(expr, op1)) + constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0)) model = _try_constraints(node.constraints, [constraint]) if model is None: @@ -106,20 +106,7 @@ def _verify_integer_overflow(statespace, node, expr, state, model, constraint, o if len(interesting_usages) == 0: return False - model0, model1 = None, None - - if type(op0) is not int: - op0_value = int(str(model.eval(op0, model_completion=True))) - model0 = _try_constraints(node.constraints, [op0 != op0_value]) - - if type(op1) is not int: - op1_value = int(str(model.eval(op1, model_completion=True))) - model1 = _try_constraints(node.constraints, [op1 != op1_value]) - - if model0 is None and model1 is None: - return False - - return True + return _try_constraints(node.constraints, [Not(constraint)]) is not None def _try_constraints(constraints, new_constraints):