How to use the mythril.laser.smt.Extract function in mythril

if key.size() == 512:
                ex_key = Extract(511, 256, key)
            else:
                ex_key = key
            potential_values = concrete_values
            key.potential_values = []
            for i, val in enumerate(potential_values):
                key.potential_values.append(
                    (val, And(models[i][1], BitVec(key.raw) == val))
                )

            return key.potential_values
        if key.size() == 512:
            val = simplify(Extract(511, 256, key))
            concrete_vals = self._traverse_concretise(val, models)
            vals2 = self._traverse_concretise(Extract(255, 0, key), models)
            key.potential_values = []
            i = 0
            for val1, val2 in zip(concrete_vals, vals2):
                if val2 and val1:
                    c_val = Concat(val1[0], val2[0])
                    condition = And(
                        models[i][1], BitVec(key.raw) == c_val, val1[1], val2[1]
                    )
                    key.potential_values.append((c_val, condition))
                else:
                    key.potential_values.append((None, None))

        if isinstance(key.input_, BitVec) or (
            isinstance(key.input_, BitVecFunc) and key.input_.func_name == "sha3"
        ):
            self._traverse_concretise(key.input_, models)

def _sanitize(input_: BitVec) -> BitVec:
        if input_.potential_values:
            input_ = input_.potential_values
        if input_.size() == 512:
            return input_
        if input_.size() > 512:
            return Extract(511, 0, input_)
        else:
            return Concat(symbol_factory.BitVecVal(0, 512 - input_.size()), input_)

models[i][1], BitVec(key.raw) == c_val, val1[1], val2[1]
                    )
                    key.potential_values.append((c_val, condition))
                else:
                    key.potential_values.append((None, None))

        if isinstance(key.input_, BitVec) or (
            isinstance(key.input_, BitVecFunc) and key.input_.func_name == "sha3"
        ):
            self._traverse_concretise(key.input_, models)

        if isinstance(key, BitVecFunc):
            if key.size() == 512:
                p1 = Extract(511, 256, key)
                if not isinstance(p1, BitVecFunc):
                    p1 = Extract(255, 0, key)
                p1 = [
                    (self.calc_sha3(val[0], p1.input_.size()), val[1])
                    for val in p1.input_.potential_values
                ]
                key.potential_values = []
                for i, val in enumerate(p1):
                    if val[0]:
                        c_val = Concat(val[0], Extract(255, 0, key))
                        condition = And(models[i][1], val[1], BitVec(key.raw) == c_val)
                        key.potential_values.append((c_val, condition))
                    else:
                        key.potential_values.append((None, None))
            else:
                key.potential_values = []
                for i, val in enumerate(key.input_.potential_values):
                    if val[0]:

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),
                        256,
                    )
                    pseudo_input = symbol_factory.BitVecVal(pseudo_input, 256)
                    calldata_cond = And(
                        calldata_cond,
                        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
                    if not is_true(simplify(Extract(511, 256, key.input_).potential_input_cond != calldata_cond)):
                        print(key.input_, Extract(511, 256, key.input_).concat_args)
                    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(
                    (
                        get_model(
                            constraints=global_state.mstate.constraints
                            + [sender == actor, calldata_cond]
                        ),
                        And(calldata_cond, sender == actor),
                    )
                )
                sat = True
            except UnsatError:
                models_tuple.append((None, And(calldata_cond, sender == actor)))

and isinstance(key.input_, BitVec)
                    and key.input_.symbolic
                    and key.input_.size() == 512
                ):
                    pseudo_input = random.randint(0, 2 ** 256 - 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),
                        256,
                    )
                    pseudo_input = symbol_factory.BitVecVal(pseudo_input, 256)
                    calldata_cond = And(
                        calldata_cond,
                        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
                    if not is_true(simplify(Extract(511, 256, key.input_).potential_input_cond != calldata_cond)):
                        print(key.input_, Extract(511, 256, key.input_).concat_args)
                    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(
                    (
                        get_model(
                            constraints=global_state.mstate.constraints
                            + [sender == actor, calldata_cond]
                        ),
                        And(calldata_cond, sender == actor),

c_val = Concat(val1[0], val2[0])
                    condition = And(
                        models[i][1], BitVec(key.raw) == c_val, val1[1], val2[1]
                    )
                    key.potential_values.append((c_val, condition))
                else:
                    key.potential_values.append((None, None))

        if isinstance(key.input_, BitVec) or (
            isinstance(key.input_, BitVecFunc) and key.input_.func_name == "sha3"
        ):
            self._traverse_concretise(key.input_, models)

        if isinstance(key, BitVecFunc):
            if key.size() == 512:
                p1 = Extract(511, 256, key)
                if not isinstance(p1, BitVecFunc):
                    p1 = Extract(255, 0, key)
                p1 = [
                    (self.calc_sha3(val[0], p1.input_.size()), val[1])
                    for val in p1.input_.potential_values
                ]
                key.potential_values = []
                for i, val in enumerate(p1):
                    if val[0]:
                        c_val = Concat(val[0], Extract(255, 0, key))
                        condition = And(models[i][1], val[1], BitVec(key.raw) == c_val)
                        key.potential_values.append((c_val, condition))
                    else:
                        key.potential_values.append((None, None))
            else:
                key.potential_values = []

:param global_state:
        :return:
        """
        mstate = global_state.mstate
        op0, op1 = mstate.stack.pop(), mstate.stack.pop()
        if not isinstance(op1, Expression):
            op1 = symbol_factory.BitVecVal(op1, 256)
        try:
            index = util.get_concrete_int(op0)
            offset = (31 - index) * 8
            if offset >= 0:
                result = simplify(
                    Concat(
                        symbol_factory.BitVecVal(0, 248),
                        Extract(offset + 7, offset, op1),
                    )
                )  # type: Union[int, Expression]
            else:
                result = 0
        except TypeError:
            log.debug("BYTE: Unsupported symbolic byte offset")
            result = global_state.new_bitvec(
                str(simplify(op1)) + "[" + str(simplify(op0)) + "]", 256
            )

        mstate.stack.append(result)
        return [global_state]