From e7d50f3c608c8a7fee9e431c54c02b67dee3d55a Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 29 Oct 2021 10:33:27 +0100 Subject: [PATCH] Fix issue with integer arthimetic (#1541) --- mythril/analysis/module/modules/integer.py | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/mythril/analysis/module/modules/integer.py b/mythril/analysis/module/modules/integer.py index d042061f..459eb6e2 100644 --- a/mythril/analysis/module/modules/integer.py +++ b/mythril/analysis/module/modules/integer.py @@ -161,25 +161,22 @@ class IntegerArithmetics(DetectionModule): def _handle_exp(self, state): op0, op1 = self._get_args(state) + + if op1.value == 0 or op0.value < 2: + return if op0.symbolic and op1.symbolic: constraint = And( op1 > symbol_factory.BitVecVal(256, 256), op0 > symbol_factory.BitVecVal(1, 256), ) - elif op1.symbolic: - if op0.value < 2: - return - constraint = op1 >= symbol_factory.BitVecVal( - ceil(256 / log2(op0.value)), 256 - ) elif op0.symbolic: - if op1.value == 0: - return constraint = op0 >= symbol_factory.BitVecVal( 2 ** ceil(256 / op1.value), 256 ) else: - constraint = op0.value ** op1.value >= 2 ** 256 + constraint = op1 >= symbol_factory.BitVecVal( + ceil(256 / log2(op0.value)), 256 + ) annotation = OverUnderflowAnnotation(state, "exponentiation", constraint) op0.annotate(annotation)