From ee674ff803d7f309fd5b296ce51f4d0c47a0d7a2 Mon Sep 17 00:00:00 2001 From: Haozhong Zhang Date: Wed, 31 Oct 2018 11:30:30 +0800 Subject: [PATCH] analysis/integer: fix the overflow check of bit vector multiplication Differently than the bit vector addition, an overflowed bit vector multiplication does not necessarily result in a value less than any of its operands (e.g., the multiplication of two 8-bit vectors 0x7 and 4 produces 0xC). Fix this issue by using Z3 BVMulNoOverflow in the overflow check of bit vector multiplication. --- mythril/analysis/modules/integer.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index df0d8988..709d2c2e 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -72,11 +72,12 @@ def _check_integer_overflow(statespace, state, node): # Formulate expression if instruction["opcode"] == "ADD": expr = op0 + op1 + constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0)) else: expr = op1 * op0 + constraint = Not(BVMulNoOverflow(op0, op1, signed=False)) # Check satisfiable - constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0)) model = _try_constraints(node.constraints, [constraint]) if model is None: