Better concretize and calldataload

manticore/core/smtlib/visitors.py

@@ -786,7 +786,7 @@ def to_constant(expression):
 
 @lru_cache(maxsize=128, typed=True)
 def simplify(expression):
-    # expression = constant_folder(expression)
+    expression = constant_folder(expression)
     expression = arithmetic_simplify(expression)
     return expression
 

manticore/ethereum/abi.py

@@ -253,6 +253,7 @@ def _deserialize(ty, buf, offset=0):
         elif ty[0] in ("array"):
             result = []
             dyn_offset = ABI._deserialize_int(buf[offset : offset + 32])
+            dyn_offset = to_constant(dyn_offset)
             rep = ty[1]
             ty_size = ABI._type_size(ty[2])
             if rep is None:

manticore/ethereum/detectors.py

@@ -75,7 +75,6 @@ def add_finding(self, state, address, pc, finding, at_init, constraint=True):
         self.get_findings(state).append((address, pc, finding, at_init, constraint))
         with self.locked_global_findings() as gf:
             gf.append((address, pc, finding, at_init))
-
         # Fixme for ever broken logger
         logger.warning(finding)
 

manticore/ethereum/manticore.py

@@ -1502,6 +1502,9 @@ def generate_testcase(self, state, message="", only_if=None, name="user"):
         if len(local_findings):
             with testcase.open_stream("findings") as findings:
                 for address, pc, finding, at_init, constraint in local_findings:
+                    if not state.can_be_true(constraint):
+                        continue
+                    state.constrain(constraint)
                     findings.write("- %s -\n" % finding)
                     write_findings(findings, "  ", address, pc, at_init)
                     md = self.get_metadata(address)

manticore/platforms/evm.py

@@ -78,6 +78,11 @@ def globalsha3(data):
     default=1024 * 1024,
     description="Max calldata offset to explore with. Iff offset or size in a calldata related instruction are symbolic it will be constrained to this constant",
 )
+consts.add(
+    "calldata_max_size",
+    default = 64,
+    description="Max calldata size to explore in each CALLDATACOPY. Iff size in a calldata related instruction are symbolic it will be constrained to be less than this constant. -1 means free(only use when gas is being tracked)",
+)
 
 # Auxiliary constants and functions
 TT256 = 2 ** 256
@@ -142,14 +147,17 @@ def __init__(
         self.gas = gas
         self.set_result(result, return_data)
 
-    def concretize(self, state):
-        conc_caller = state.solve_one(self.caller)
-        conc_address = state.solve_one(self.address)
-        conc_value = state.solve_one(self.value)
-        conc_gas = state.solve_one(self.gas)
-        conc_data = state.solve_one(self.data)
-        conc_return_data = state.solve_one(self.return_data)
-
+    def concretize(self, state, constrain=False):
+        """
+        :param state: a manticore state
+        :param bool constrain: If True, constrain expr to concretized value
+        """
+        conc_caller = state.solve_one(self.caller, constrain=constrain)
+        conc_address = state.solve_one(self.address, constrain=constrain)
+        conc_value = state.solve_one(self.value, constrain=constrain)
+        conc_gas = state.solve_one(self.gas, constrain=constrain)
+        conc_data = state.solve_one(self.data, constrain=constrain)
+        conc_return_data = state.solve_one(self.return_data, constrain=constrain)
         return Transaction(
             self.sort,
             conc_address,
@@ -160,7 +168,7 @@ def concretize(self, state):
             conc_gas,
             depth=self.depth,
             result=self.result,
-            return_data=bytearray(conc_return_data),
+            return_data=conc_return_data,
         )
 
     def to_dict(self, mevm):
@@ -556,8 +564,8 @@ def wrapper(*args, **kwargs):
                         "the value might not be tracked properly (This may affect detectors)"
                     )
                 logger.info(
-                    f"Concretizing instruction {args[0].world.current_vm.instruction} argument {arg} by {policy}"
-                )
+                    f"Concretizing instruction {args[0].world.current_vm.instruction} argument {arg} by {policy}")
+
                 raise ConcretizeArgument(index, policy=policy)
             return func(*args, **kwargs)
 
@@ -834,7 +842,7 @@ def _get_memfee(self, address, size=1):
         return Operators.ITEBV(512, size == 0, 0, Operators.ITEBV(512, flag, memfee, 0))
 
     def _allocate(self, address, size=1):
-        address_c = Operators.UDIV(Operators.ZEXTEND(address, 512) + size + 31, 32) * 32
+        address_c = Operators.UDIV(self.safe_add(address, size, 31), 32) * 32
         self._allocated = Operators.ITEBV(
             512, Operators.UGT(address_c, self._allocated), address_c, self.allocated
         )
@@ -1213,7 +1221,11 @@ def setstate(state, value):
             raise Concretize(
                 "Concretize PC", expression=expression, setstate=setstate, policy="ALL"
             )
-        # print(self)
+        #if self._checkpoint_data is None:
+        #    print(self)
+        #else:
+        #    print ("back from a fork")
+        #import pdb; pdb.set_trace()
         try:
             # import time
             # limbo = 0.0
@@ -1334,10 +1346,12 @@ def _store(self, offset, value, size=1):
                 "did_evm_write_memory", offset + i, Operators.EXTRACT(value, (size - i - 1) * 8, 8)
             )
 
-    def safe_add(self, a, b):
+    def safe_add(self, a, b, *args):
         a = Operators.ZEXTEND(a, 512)
         b = Operators.ZEXTEND(b, 512)
         result = a + b
+        if len(args) > 0:
+            result = self.safe_add(result, *args)
         return result
 
     def safe_mul(self, a, b):
@@ -1597,22 +1611,18 @@ def CALLVALUE(self):
     def CALLDATALOAD(self, offset):
         """Get input data of current environment"""
         # calldata_overflow = const.calldata_overflow
-        # calldata_underflow = const.calldata_underflow
         calldata_overflow = None  # 32
-        calldata_underflow = None  # 32
-        # if const.calldata_overlap:
         if calldata_overflow is not None:
-            self.constraints.add(offset + 32 <= len(self.data) + calldata_overflow)
+            self.constraints.add(self.safe_add(offset, 32) <= len(self.data) + calldata_overflow)
         if calldata_underflow is not None:
-            self.constraints.add(offset >= -calldata_underflow)
 
         self._use_calldata(offset, 32)
 
         data_length = len(self.data)
         bytes = []
         for i in range(32):
             try:
-                c = simplify(Operators.ITEBV(8, offset + i < data_length, self.data[offset + i], 0))
+                c = simplify(Operators.ITEBV(8, Operators.ULT(self.safe_add(offset, i), data_length), self.data[offset + i], 0))
             except IndexError:
                 # offset + i is concrete and outside data
                 c = 0
@@ -1636,17 +1646,14 @@ def CALLDATACOPY_gas(self, mem_offset, data_offset, size):
         memfee = self._get_memfee(mem_offset, size)
         return self.safe_add(copyfee, memfee)
 
-    @concretized_args(size="SAMPLED")
+    #@concretized_args(size="SAMPLED")
     def CALLDATACOPY(self, mem_offset, data_offset, size):
         """Copy input data in current environment to memory"""
         # calldata_overflow = const.calldata_overflow
         # calldata_underflow = const.calldata_underflow
         calldata_overflow = None  # 32
-        calldata_underflow = None  # 32
-        # if const.calldata_overlap:
-        if calldata_underflow is not None:
-            self.constraints.add(data_offset + size <= len(self.data) + calldata_overflow)
-            self.constraints.add(data_offset >= -calldata_underflow)
+        if calldata_overflow is not None:
+            self.constraints.add(Operators.ULT( self.safe_add(data_offset, size), len(self.data) + calldata_overflow))
 
         self._use_calldata(data_offset, size)
         self._allocate(mem_offset, size)
@@ -1658,6 +1665,9 @@ def CALLDATACOPY(self, mem_offset, data_offset, size):
                 raise NotEnoughGas()
             self.constraints.add(cond)
 
+        if consts.calldata_max_size >= 0:
+            self.constraints.add(Operators.ULE(size, consts.calldata_max_size))
+
         max_size = size
         if issymbolic(max_size):
             max_size = Z3Solver.instance().max(self.constraints, size)
@@ -1677,7 +1687,7 @@ def CALLDATACOPY(self, mem_offset, data_offset, size):
             try:
                 c1 = Operators.ITEBV(
                     8,
-                    data_offset + i < len(self.data),
+                    Operators.ULT(self.safe_add(data_offset, i), len(self.data)),
                     Operators.ORD(self.data[data_offset + i]),
                     0,
                 )
@@ -2202,7 +2212,7 @@ def __str__(self):
         gas = self.gas
         if issymbolic(gas):
             gas = simplify(gas)
-            result.append(f"Gas: {translate_to_smtlib(gas)} {gas.taint}")
+            result.append(f"Gas: {translate_to_smtlib(gas)[:20]} {gas.taint}")
         else:
             result.append(f"Gas: {gas}")