Don't constraint calldata_size.

palkeo · Mar 25, 2019 · 0b9e694 · 0b9e694
1 parent 4afbe91
commit 0b9e694
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 7 deletions.
diff --git a/pakala/env.py b/pakala/env.py
@@ -77,7 +77,7 @@ def extra_constraints(self):
                 yield getattr(self, name) <= max_
 
     def solution_string(self, solver):
-        calldata_size = solver.min(self.calldata_size)
+        calldata_size = max(solver.min(self.calldata_size), self.calldata.size())
         solution = {
             "calldata": "{0:0{1}x}".format(
                 solver.min(self.calldata.read(0, calldata_size)), calldata_size * 2

diff --git a/pakala/sm.py b/pakala/sm.py
@@ -40,10 +40,10 @@
 BVV_1 = bvv(1)
 
 # interesting values aligned to classic parameters.
-CALLDATALOAD_INDEX_FUZZ = [0, 32, 64] + [4, 36, 68, 100, 136]
-CALLDATACOPY_SIZE_FUZZ = list(range(9)) + [16, 32, 64]
-RETURNDATACOPY_SIZE_FUZZ = [0, 32]
-EXP_EXPONENT_FUZZ = [min, max]
+CALLDATALOAD_INDEX_FUZZ = set(range(0, 32*3, 32)) | set(range(4, 32*5, 32))
+CALLDATACOPY_SIZE_FUZZ = set(range(9)) | {0, 32} | {4, 34, 4 + 32 * 16}
+RETURNDATACOPY_SIZE_FUZZ = {0, 32}
+EXP_EXPONENT_FUZZ = {min, max}
 
 
 class MultipleSolutionsError(ValueError):
@@ -459,7 +459,6 @@ def solution(variable):
                     state.stack_push(index)  # restore the stack
                     self.add_for_fuzzing(state, index, CALLDATALOAD_INDEX_FUZZ)
                     return False
-                state.solver.add(state.env.calldata_size >= index_sol + 32)
                 state.stack_push(state.env.calldata.read(index_sol, 32))
             elif op == opcode_values.CALLDATASIZE:
                 state.stack_push(state.env.calldata_size)
@@ -477,7 +476,6 @@ def solution(variable):
                     self.add_for_fuzzing(old_state, size, CALLDATACOPY_SIZE_FUZZ)
                     return False
                 state.memory.copy_from(state.env.calldata, mstart, dstart, size)
-                state.solver.add(state.env.calldata_size >= dstart + size)
             elif op == opcode_values.CODESIZE:
                 state.stack_push(bvv(len(self.code)))
             elif op == opcode_values.EXTCODESIZE: