ADDMOD and MULMOD fixes (#1531)

* ADDMOD and MULMOD tests * ADDMOD and MULMOD tests * Not mod256 arith
trailofbits · Oct 2, 2019 · 1ec9032 · 1ec9032
1 parent 5bde1b5
commit 1ec9032
Show file tree

Hide file tree

Showing 2 changed files with 112 additions and 2 deletions.
diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py
@@ -1414,15 +1414,17 @@ def SMOD(self, a, b):
     def ADDMOD(self, a, b, c):
         """Modulo addition operation"""
         try:
-            result = Operators.ITEBV(256, c == 0, 0, (a + b) % c)
+            result = Operators.EXTRACT(self.safe_add(a, b) % Operators.ZEXTEND(c, 512), 0, 256)
+            result = Operators.ITEBV(256, c == 0, 0, result)
         except ZeroDivisionError:
             result = 0
         return result
 
     def MULMOD(self, a, b, c):
         """Modulo addition operation"""
         try:
-            result = Operators.ITEBV(256, c == 0, 0, (a * b) % c)
+            result = Operators.EXTRACT(self.safe_mul(a, b) % Operators.ZEXTEND(c, 512), 0, 256)
+            result = Operators.ITEBV(256, c == 0, 0, result)
         except ZeroDivisionError:
             result = 0
         return result

diff --git a/tests/ethereum/test_regressions.py b/tests/ethereum/test_regressions.py
@@ -245,6 +245,114 @@ def test_1102(self):
     def test_705(self):
         self._simple_cli_run("705.sol")
 
+    def test_addmod(self):
+        """
+        (declare-fun BV () (_ BitVec 256))
+        (declare-fun BV_2 () (_ BitVec 256))
+        (declare-fun BV_1 () (_ BitVec 256))
+        (declare-fun a_1 () (_ BitVec 256))(assert (= a_1 (bvmul BV BV_1)))
+        (declare-fun a_2 () (_ BitVec 512))(assert (= a_2 ((_ zero_extend 256) BV)))
+        (declare-fun a_3 () (_ BitVec 512))(assert (= a_3 ((_ zero_extend 256) BV_1)))
+        (declare-fun a_4 () (_ BitVec 512))(assert (= a_4 (bvmul a_2 a_3)))
+        (declare-fun a_5 () (_ BitVec 512))(assert (= a_5 ((_ zero_extend 256) BV_2)))
+        (declare-fun a_6 () (_ BitVec 512))(assert (= a_6 (bvsmod a_4 a_5)))
+        (declare-fun a_7 () (_ BitVec 256))(assert (= a_7 ((_ extract 255 0) a_6)))
+        (declare-fun a_8 () (_ BitVec 256))(assert (= a_8 (bvsmod a_1 BV_2)))
+        (declare-fun a_9 () Bool)(assert (= a_9 (= a_7 a_8)))
+        (assert (not a_9))
+
+        (check-sat)
+        """
+        from manticore.platforms import evm
+        from manticore.core.smtlib import ConstraintSet, Z3Solver, Operators
+
+        constraints = ConstraintSet()
+
+        address = 0x41414141414141414141
+        data = b""
+        caller = 0x42424242424242424242
+        value = 0
+        bytecode = ""
+        vm = evm.EVM(constraints, address, data, caller, value, bytecode)
+
+        self.assertEqual(vm.ADDMOD(12323, 2343, 20), 6)
+        self.assertEqual(vm.ADDMOD(12323, 2343, 0), 0)
+
+        A, B, C = (
+            0x780000002090309A004201626B1400041D318000000200008A0080089C042DA7,
+            0xF000000740403F7007C012807BED003BE2CE800000060000FFFFBFF7E4087033,
+            0x338000080FFFFF64AAAACFFCF7DBFA408000000000000270120000001E7C2ACF,
+        )
+        self.assertEqual(
+            vm.ADDMOD(A, B, C),
+            23067954172474524581131069693479689311231082562138745684554374357070230297856,
+        )
+        a, b, c = (
+            constraints.new_bitvec(256),
+            constraints.new_bitvec(256),
+            constraints.new_bitvec(256),
+        )
+        constraints.add(a == A)
+        constraints.add(b == B)
+        constraints.add(c == C)
+        result = vm.ADDMOD(a, b, c)
+        # 0x32ffffd700d073ae080133f517d922bd000000000007f1611e003fffc9239d00
+        self.assertEqual(
+            Z3Solver.instance().get_all_values(constraints, result),
+            [0x32FFFFD700D073AE080133F517D922BD000000000007F1611E003FFFC9239D00],
+        )
+
+    def test_mulmod(self):
+        """
+        (declare-fun BV () (_ BitVec 256))
+        (declare-fun BV_2 () (_ BitVec 256))
+        (declare-fun BV_1 () (_ BitVec 256))
+        (declare-fun a_1 () (_ BitVec 256))(assert (= a_1 (bvmul BV BV_1)))
+        (declare-fun a_2 () (_ BitVec 512))(assert (= a_2 ((_ zero_extend 256) BV)))
+        (declare-fun a_3 () (_ BitVec 512))(assert (= a_3 ((_ zero_extend 256) BV_1)))
+        (declare-fun a_4 () (_ BitVec 512))(assert (= a_4 (bvmul a_2 a_3)))
+        (declare-fun a_5 () (_ BitVec 512))(assert (= a_5 ((_ zero_extend 256) BV_2)))
+        (declare-fun a_6 () (_ BitVec 512))(assert (= a_6 (bvsmod a_4 a_5)))
+        (declare-fun a_7 () (_ BitVec 256))(assert (= a_7 ((_ extract 255 0) a_6)))
+        (declare-fun a_8 () (_ BitVec 256))(assert (= a_8 (bvsmod a_1 BV_2)))
+        (declare-fun a_9 () Bool)(assert (= a_9 (= a_7 a_8)))
+        (assert (not a_9))
+
+        (check-sat)
+        """
+        from manticore.platforms import evm
+        from manticore.core.smtlib import ConstraintSet, Z3Solver, Operators
+
+        constraints = ConstraintSet()
+
+        address = 0x41414141414141414141
+        data = b""
+        caller = 0x42424242424242424242
+        value = 0
+        bytecode = ""
+        vm = evm.EVM(constraints, address, data, caller, value, bytecode)
+
+        self.assertEqual(vm.MULMOD(12323, 2343, 20), 9)
+        self.assertEqual(vm.MULMOD(12323, 2343, 0), 0)
+
+        A, B, C = (
+            110427941548649020598956093796432407239217743554726184882600387580788736,
+            1048576,
+            4194319,
+        )
+        self.assertEqual(vm.MULMOD(A, B, C), 2423129)
+        a, b, c = (
+            constraints.new_bitvec(256),
+            constraints.new_bitvec(256),
+            constraints.new_bitvec(256),
+        )
+        constraints.add(a == A)
+        constraints.add(b == B)
+        constraints.add(c == C)
+        result = vm.MULMOD(a, b, c)
+        # 0x8000000000000000000000000000000000000000000000000000000082000011
+        self.assertEqual(Z3Solver.instance().get_all_values(constraints, result), [2423129])
+
 
 if __name__ == "__main__":
     unittest.main()