expr_inferrer.py 文件源码

def infer_subscript(node, context, solver):
    """Infer expressions like: x[1], x["a"], x[1:2], x[1:].
    Where x may be: a list, dict, tuple, str

    Attributes:
        node: the subscript node to be inferred
    """

    indexed_type = infer(node.value, context, solver)

    if isinstance(node.slice, ast.Index):
        index_type = infer(node.slice.value, context, solver)
        result_type = solver.new_z3_const("index")
        solver.add(axioms.index(indexed_type, index_type, result_type, solver.z3_types),
                   fail_message="Indexing in line {}".format(node.lineno))
        return result_type
    else:  # Slicing
        # Some slicing may contain 'None' bounds, ex: a[1:], a[::]. Make Int the default type.
        lower_type = upper_type = step_type = solver.z3_types.int
        if node.slice.lower:
            lower_type = infer(node.slice.lower, context, solver)
        if node.slice.upper:
            upper_type = infer(node.slice.upper, context, solver)
        if node.slice.step:
            step_type = infer(node.slice.step, context, solver)

        result_type = solver.new_z3_const("slice")

        solver.add(axioms.slicing(lower_type, upper_type, step_type, indexed_type, result_type, solver.z3_types),
                   fail_message="Slicing in line {}".format(node.lineno))
        return result_type