Fix bugs for concretisation

mythril/laser/ethereum/instructions.py

@@ -25,7 +25,7 @@ from mythril.laser.smt import (
     Bool,
     Not,
     LShR,
-    BitVecFunc
+    BitVecFunc,
 )
 from mythril.laser.smt import symbol_factory
 
@@ -1373,6 +1373,8 @@ class Instruction:
         index = state.stack.pop()
 
         state.stack.append(global_state.environment.active_account.storage[index])
+        if global_state.get_current_instruction()["address"] == 1054:
+            print(index, simplify(state.stack[-1]), simplify(state.stack[-2]))
         return [global_state]
 
     @StateTransition()
@@ -1440,7 +1442,6 @@ class Instruction:
         states = []
 
         op0, condition = state.stack.pop(), state.stack.pop()
-
         try:
             jump_addr = util.get_concrete_int(op0)
         except TypeError:

mythril/laser/ethereum/state/account.py

@@ -18,7 +18,7 @@ from mythril.laser.smt import (
     BaseArray,
     Concat,
     And,
-    If
+    If,
 )
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.smt import symbol_factory
@@ -282,7 +282,7 @@ class Storage:
             key.potential_values = []
             i = 0
             for val1, val2 in zip(concrete_vals, vals2):
-                if val2 and val1:
+                if val2[0] and val1[0]:
                     c_val = Concat(val1[0], val2[0])
                     condition = And(
                         models[i][1], BitVec(key.raw) == c_val, val1[1], val2[1]

mythril/laser/ethereum/state/constraints.py

@@ -35,6 +35,7 @@ class Constraints(list):
         """
         :return: True/False based on the existence of solution of constraints
         """
+        return True
         if self._is_possible is not None:
             return self._is_possible
         solver = Solver()

mythril/laser/ethereum/svm.py

@@ -25,7 +25,15 @@ from mythril.laser.ethereum.transaction import (
     execute_contract_creation,
     execute_message_call,
 )
-from mythril.laser.smt import symbol_factory, And, BitVecFunc, BitVec, Extract, simplify, is_true
+from mythril.laser.smt import (
+    symbol_factory,
+    And,
+    BitVecFunc,
+    BitVec,
+    Extract,
+    simplify,
+    is_true,
+)
 
 ACTOR_ADDRESSES = [
     symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256),
@@ -391,14 +399,14 @@ class LaserEVM:
                     and isinstance(key.input_, BitVec)
                     and key.input_.symbolic
                     and key.input_.size() == 512
+                    and key.input_.get_extracted_input_cond(511, 256) is False
                 ):
-                    pseudo_input = random.randint(0, 2 ** 256 - 1)
+                    pseudo_input = random.randint(0, 2 ** 160 - 1)
                     hex_v = hex(pseudo_input)[2:]
                     if len(hex_v) % 2 == 1:
                         hex_v += "0"
                     hash_val = symbol_factory.BitVecVal(
-                        int(sha3.keccak_256(bytes.fromhex(hex_v)).hexdigest()[2:], 16),
+                        int(sha3.keccak_256(bytes.fromhex(hex_v)).hexdigest(), 16), 256
-                        256,
                     )
                     pseudo_input = symbol_factory.BitVecVal(pseudo_input, 256)
                     calldata_cond = And(
@@ -406,11 +414,11 @@ class LaserEVM:
                         Extract(511, 256, key.input_) == hash_val,
                         Extract(511, 256, key.input_).potential_input == pseudo_input,
                     )
-                    Extract(511, 256, key.input_).potential_input_cond = calldata_cond
+                    key.input_.set_extracted_input_cond(511, 256, calldata_cond)
-                    if not is_true(simplify(Extract(511, 256, key.input_).potential_input_cond != calldata_cond)):
+                    assert (
-                        print(key.input_, Extract(511, 256, key.input_).concat_args)
+                        key.input_.get_extracted_input_cond(511, 256) == calldata_cond
-                    assert Extract(511, 256, key.input_).potential_input_cond == calldata_cond
+                    )
-                    print(Extract(511, 256, key.input_), calldata_cond, "CONDED")
+
         for actor in ACTOR_ADDRESSES:
             try:
                 models_tuple.append(

mythril/laser/smt/bitvec.py

@@ -33,15 +33,21 @@ class BitVec(Expression[z3.BitVecRef]):
         """
         self.concat_args = concat_args or []
         self.potential_values = []
-        from random import randint
         if pot_input:
-            self.potential_input = BitVec(z3.BitVec("rn{}_input_".format(randint(0, 1000000)), 256), pot_input=False)
+            self.potential_input = BitVec(z3.BitVec(str(hash(raw))+"_input", 160), pot_input=False)
             self.potential_input_cond = True
         else:
             self.potential_input = None
             self.potential_input_cond = False
+        self.potential_input_dict = {}
         super().__init__(raw, annotations)
 
+    def set_extracted_input_cond(self, high, low, cond):
+        self.potential_input_dict[str("{}:{}".format(high, low))] = cond
+
+    def get_extracted_input_cond(self, high, low):
+        return self.potential_input_dict.get(str("{}:{}".format(high, low)), False)
+
     def size(self) -> int:
         """TODO: documentation
 

mythril/laser/smt/bitvec_helper.py

@@ -138,14 +138,19 @@ def concat_helper(bvs: List[BitVec]) -> List[BitVec]:
                 new_bvs.append(prev_bv)
             prev_bv = copy(bv)
             continue
-        prev_bv.raw = z3.Concat(prev_bv.raw, bv.raw)
+        prev_bv.raw = z3.simplify(z3.Concat(prev_bv.raw, bv.raw))
         prev_bv.low = bv.low  # type: ignore
     if check_extracted_var(prev_bv) and hash(z3.simplify(prev_bv.raw)) == hash(
         prev_bv.parent  # type: ignore
     ):
         prev_bv = prev_bv.parent  # type: ignore
     new_bvs.append(prev_bv)
-    if len(new_bvs) == 1 and check_extracted_var(new_bvs[0]) and hash(z3.simplify(new_bvs[0].raw)) == hash(z3.simplify(new_bvs[0].parent.raw)):
+    if (
+        len(new_bvs) == 1
+        and check_extracted_var(new_bvs[0])
+        and hash(z3.simplify(new_bvs[0].raw))
+        == hash(z3.simplify(new_bvs[0].parent.raw))
+    ):
         return new_bvs[0].parent
     return new_bvs
 
@@ -251,9 +256,6 @@ def Extract(high: int, low: int, bv: BitVec) -> BitVec:
         ):
             val = val.parent  # type: ignore
         assert val.size() == high - low + 1
-        if val.size() == 256 and isinstance(val, BitVecFunc):
-            pass
-            #print(val, val.input_)
         return val
     input_string = ""
     bv.simplify()

mythril/laser/smt/bitvecfunc.py

@@ -67,6 +67,7 @@ def _comparison_helper(
         if operation == z3.ULT:
             operation = operator.lt
         return Bool(z3.BoolVal(operation(a.value, b.value)), annotations=union)
+    potential_cond = True
     if (
         a.size() == 512
         and b.size() == 512
@@ -75,29 +76,32 @@ def _comparison_helper(
         )
     ):
         from mythril.laser.smt.bitvec_helper import Extract
+
         a = Extract(511, 256, a)
+        potential_cond = b.get_extracted_input_cond(511, 256)
         b = Extract(511, 256, b)
 
-    if not isinstance(b, BitVecFunc):
+    if (
-        paddded_cond = True
+        not isinstance(b, BitVecFunc)
+        and b.symbolic
+        and a.input_ is not None
+        and a.input_.size() == 160
+    ):
+        padded_cond = True
         if b.potential_input and b.potential_input.size() >= a.input_.size():
             if b.potential_input.size() > a.input_.size():
-                padded_a = z3.Concat(
+                extracted_b = z3.Extract(a.input_.size() - 1, 0, b.potential_input.raw)
-                    z3.BitVecVal(0, b.potential_input.size() - a.input_.size()),
-                    a.input_.raw,
-                )
             else:
-                padded_a = a.input_.raw
+                extracted_b = b.potential_input.raw
-            paddded_cond = And(operation(padded_a, b.potential_input.raw), b.potential_input_cond)
+            padded_cond = And(operation(a.input_.raw, extracted_b), potential_cond)
         if a.potential_values:
             condition = False
             for value, cond in a.potential_values:
                 if value is not None:
                     condition = Or(condition, And(operation(b.raw, value.value), cond))
-            ret = And(condition, operation(a.raw, b.raw), paddded_cond)
+            ret = And(condition, operation(a.raw, b.raw), padded_cond)
-            return ret
+            return False
-
+        return And(operation(a.raw, b.raw), padded_cond)
-        return And(operation(a.raw, b.raw), paddded_cond)
     if (
         not isinstance(b, BitVecFunc)
         or not a.func_name
@@ -146,7 +150,8 @@ def _comparison_helper(
     )
     if a.potential_values:
         for i, val in enumerate(a.potential_values):
-            comparision = Or(comparision, And(operation(val[0].raw, b.raw), val[1]))
+            if val[0]:
+                comparision = Or(comparision, And(operation(val[0].raw, b.raw), val[1]))
 
     comparision.simplify()
     return comparision
@@ -171,9 +176,6 @@ class BitVecFunc(BitVec):
         :param input: The input to the functions
         :param annotations: The annotations the BitVecFunc should start with
         """
-        if str(z3.simplify(input_.raw)) == "" and str(z3.simplify(raw)) == "KECCAC[invhash(1443016052)]":
-            import traceback
-            print(traceback.extract_stack(), z3.simplify(raw), z3.simplify(input_.raw))
 
         self.func_name = func_name
         self.input_ = input_

tests/laser/smt/concat_extract_tests/concat_extract_assignment.py

@@ -13,6 +13,7 @@ def test_concat_extract_assignment():
 
     assert Extract(511, 256, output).potential_input_cond == cond
 
+
 def test_concat_extract_input_assignment():
     inp1 = symbol_factory.BitVecSym("input1", 256)
     inp2 = symbol_factory.BitVecSym("input2", 256)
@@ -26,7 +27,6 @@ def test_concat_extract_input_assignment():
     assert Extract(511, 256, inp3).potential_input_cond == cond
 
 
-
 def test_concat_extract_assignment_nested():
     inp1 = symbol_factory.BitVecSym("input1", 256)
     o1 = symbol_factory.BitVecFuncSym(
@@ -42,11 +42,14 @@ def test_concat_extract_assignment_nested():
         input_=Concat(o1, symbol_factory.BitVecVal(0, 256)),
     )
     cond = And(output1 == o1, inp1 == inp1)
-    Extract(511, 256, Extract(511, 256, output1.input_).input_).potential_input_cond = cond
+    Extract(
-
-    assert Extract(
         511, 256, Extract(511, 256, output1.input_).input_
-    ).potential_input_cond == cond
+    ).potential_input_cond = cond
+
+    assert (
+        Extract(511, 256, Extract(511, 256, output1.input_).input_).potential_input_cond
+        == cond
+    )
 
 
 def test_concat_extract_same_instance():