A *very* fast method to evaluate symbolic jump targets if they are a) concrete targets, or b) targets coming
        from jump tables.

        :param state:   A SimState instance.
        :param ip:      The AST of the instruction pointer to evaluate.
        :param limit:   The maximum number of concrete IPs.
        :return:        A list of conditions and the corresponding concrete IPs, or None which indicates fallback is
                        necessary.
        :rtype:         list or None

def _eval_target_jumptable(state, ip, limit):
        """
        A *very* fast method to evaluate symbolic jump targets if they are a) concrete targets, or b) targets coming
        from jump tables.

        :param state:   A SimState instance.
        :param ip:      The AST of the instruction pointer to evaluate.
        :param limit:   The maximum number of concrete IPs.
        :return:        A list of conditions and the corresponding concrete IPs, or None which indicates fallback is
                        necessary.
        :rtype:         list or None
        """

        if ip.symbolic is False:
            return [ (claripy.ast.bool.true, ip) ]  # concrete

        # Detect whether ip is in the form of "if a == 1 then addr_0 else if a == 2 then addr_1 else ..."
        cond_and_targets = [ ]  # tuple of (condition, target)

        ip_ = ip
        # Handle the outer Reverse
        outer_reverse = False
        if ip_.op == "Reverse":
            ip_ = ip_.args[0]
            outer_reverse = True

        fallback = False
        target_variable = None
        concretes = set()
        reached_sentinel = False

        for cond, target in claripy.reverse_ite_cases(ip_):
            # We must fully unpack the entire AST to make sure it indeed complies with the form above
            if reached_sentinel:
                # We should not have any other value beyond the sentinel - maybe one of the possible targets happens to
                # be the same as the sentinel value?
                fallback = True
                break

            if target.symbolic is False and state.solver.eval(target) == DUMMY_SYMBOLIC_READ_VALUE:
                # Ignore the dummy value, which acts as the sentinel of this ITE tree
                reached_sentinel = True
                continue

            if cond.op != "__eq__":
                # We only support equivalence right now. Fallback
                fallback = True
                break

            if cond.args[0].symbolic is True and cond.args[1].symbolic is False:
                variable, value = cond.args
            elif cond.args[0].symbolic is False and cond.args[1].symbolic is True:
                value, variable = cond.args
            else:
                # Cannot determine variable and value. Fallback
                fallback = True
                break

            if target_variable is None:
                target_variable = variable
            elif target_variable is not variable:
                # it's checking a different variable. Fallback
                fallback = True
                break

            # Make sure the conditions are mutually exclusive
            value_concrete = state.solver.eval(value)
            if value_concrete in concretes:
                # oops... the conditions are not mutually exclusive
                fallback = True
                break
            concretes.add(value_concrete)

            if target.symbolic is True:
                # Cannot handle symbolic targets. Fallback
                fallback = True
                break

            cond_and_targets.append((cond, target if not outer_reverse else state.solver.Reverse(target)))

        if reached_sentinel is False:
            # huh?
            fallback = True

        if fallback:
            return None
        else:
            return cond_and_targets[ : limit]