python_annotation.h

Go to the documentation of this file.

#pragma once
 
#include <python-frontend/dynamic_type/literal_divergence.h>
#include <python-frontend/json_utils.h>
#include <python-frontend/module/global_scope.h>
#include <python-frontend/module/module_manager.h>
#include <python-frontend/module/module.h>
#include <python-frontend/numpy/numpy_random.h>
#include <python-frontend/python_converter.h>
#include <python-frontend/type/type_utils.h>
#include <python-frontend/python_annotation/annotation_intrinsics.h>
#include <python-frontend/python_annotation/annotation_parser.h>
#include <python-frontend/python_annotation/annotation_utils.h>
#include <python-frontend/python_annotation/function_values.h>
#include <util/message/message.h>
 
#include <map>
#include <set>
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <utility>
 
// `InferResult`, `builtin_functions` and the pure-helper utilities
// (`has_annotation`, `has_return_none`, `get_type_from_json`,
// `get_base_var_name`, `invert_substrings`,
// `infer_type_from_default_arg_shape`) were moved to the
// `python_annotation_intrinsics` and `python_annotation_utils`
// modules. The using declarations below preserve the unqualified
// names so existing call sites inside the .inl files remain byte-
// identical except, for `builtin_functions`, the trailing parens
// (`builtin_functions.find(...)` -> `builtin_functions().find(...)`).
using python_annotation_intrinsics::builtin_functions;
using python_annotation_parser::find_function_recursive;
using python_annotation_parser::find_lambda_in_body;
using python_annotation_utils::get_base_var_name;
using python_annotation_utils::get_type_from_json;
using python_annotation_utils::has_annotation;
using python_annotation_utils::has_return_none;
using python_annotation_utils::infer_type_from_default_arg_shape;
using python_annotation_utils::InferResult;
using python_annotation_utils::invert_substrings;
 
// Python-frontend annotation pass. Walks the JSON AST produced by
// `parser.py` and decorates every assignment, parameter, and return
// site with an inferred type so the downstream converter sees a
// fully-typed program. Method definitions are split across .inl
// files in python_annotation/ and are `#include`d at the bottom of
// this header. The class shape, member layout, and template
// parameter are unchanged from the pre-split version — this header
// is a thin facade over the .inl files.
template <class Json>
class python_annotation
{
public:
  python_annotation(Json &ast, global_scope &gs)
    : ast_(ast),
      gs_(gs),
      current_func(nullptr),
      parent_func(nullptr),
      current_line_(0)
  {
    python_filename_ = ast_["filename"].template get<std::string>();
    if (ast_.contains("ast_output_dir"))
      module_manager_ =
        module_manager::create(ast_["ast_output_dir"], python_filename_);
  }
 
  // Entry points exercised by callers outside python_annotation.h.
  bool preprocess_constructor_calls(Json &node);
  void preprocess_method_calls(const Json &node);
  void preprocess_receiver_method_calls();
  bool is_instance_call(const Json &func) const;
  Json *class_method(const std::string &cls, const Json &method);
  static const std::string &unresolved_arg_type()
  {
    static const std::string s = "<unresolved>";
    return s;
  }

  bool preprocess_function_calls(Json &root);
  std::string
  promote_to_float_operand(const Json &stmt, const std::string &type);
  bool annotate_from_call_sites(
    Json &root,
    Json &param,
    const std::pair<std::string, size_t> &key,
    std::set<std::string> types,
    const std::set<std::string> &top_level_funcs);
  void collect_function_call_arg_types(
    Json &node,
    std::map<std::pair<std::string, size_t>, std::set<std::string>>
      &param_types,
    const std::set<std::string> &top_level_funcs,
    std::set<std::pair<std::string, size_t>> &dynamically_typed_params);
  void add_type_annotation();
  void add_type_annotation(const std::string &func_name);
 
  // Register an additional AST whose multi-axis subscript usages must be
  // considered when inferring `__getitem__` / `__setitem__` key tuple
  // types. Used when annotating an imported module to make the importing
  // module's call sites visible (GitHub #4545). The caller retains
  // ownership; @p ast must outlive this annotator.
  void add_extra_subscript_inference_source(const Json &ast);
 
private:
  Json *
  class_init(const std::string &class_name, unsigned depth, bool &inherited);
  std::map<Json *, std::set<std::string>> inherited_init_args_;
  // Implementations live in annotation_conversion.inl unless noted.
 
  // ----- AST lookup and walk helpers -----
  Json find_var_node_for_inference(const std::string &var_name);
  // Whether an empty-list append argument resolves to a *direct* integer
  // scalar (literal, int-annotated name, or name bound to a plain int
  // source) rather than through a container/object indirection. See the
  // call site in infer_type (issue #3239 / jpl_1 regression).
  bool append_arg_is_plain_int(const Json &arg);
  const Json
  find_annotated_assign(const std::string &node_name, const Json &body);
  Json
  match_unpacking_assignment(const Json &elem, const std::string &node_name);
  Json find_receiver_decl(const std::string &obj);
  std::vector<Json>
  find_function_calls(const std::string &func_name, const Json &body);
  void find_function_calls_recursive(
    const std::string &func_name,
    const Json &node,
    std::vector<Json> &calls);
  void get_global_elements(const Json &node);
 
  // ----- type inspectors -----
  std::string get_current_func_name();
  bool is_rebound_in_scope(const std::string &var_name);
  unsigned arg_type_depth_ = 0;
  std::string get_type_from_constant(const Json &element);
  std::string get_type_from_lhs(const std::string &id, const Json &body);
  std::string get_list_subtype(const Json &list);
  std::string get_list_type_from_literal(const Json &list_arg);
  std::string subscript_annotation_type(const Json &annotation);
  std::string
  container_literal_type(const std::string &base_type, const Json &value);
  std::string list_concat_type(const Json &binop);
  // Recover a `list[T]` type for a name bound to an *empty* list literal by
  // inspecting the first `<var_name>.append(arg)` in the enclosing scope.
  // Comprehensions lower to `tmp = []; tmp.append(elt)`, so the element type
  // is lost through the empty literal; without recovery a parameter bound to
  // the list is typed bare `list` and element reads are mis-modelled as nested
  // lists (issue #5022). Returns "" when no append is found or the element
  // type does not resolve concretely (then the caller keeps the bare list).
  std::string recover_list_type_from_appends(const std::string &var_name);
  std::string bare_list_subscript_type(
    const Json &var_node,
    const std::string &var_name,
    bool is_slice);
  std::string homogeneous_literal_subscript_type(
    const Json &var_node,
    const std::string &var_name,
    bool is_slice);
  std::string
  refine_any_from_value(const std::string &annotated, const Json &var_node);
  std::string get_object_name(const Json &call, const std::string &prefix);
  std::string get_string_method_return_type(const std::string &method) const;
  bool extract_type_info(
    const Json &annotation,
    std::string &base_type,
    std::string &element_type);
  std::string infer_dict_value_type(const Json &var_node);
  std::string resolve_subscript_type(
    const Json &subscript_node,
    const Json &body,
    bool nested = false);
 
  // The type of `f(...)[i]` read from f's `list[T]` return annotation, or "Any"
  // when the subscript's base is not such a call.
  std::string subscript_type_from_call(const Json &subscript_node);
 
  // The type every element of the literal in `[a, b, ...][i]` shares, or "Any".
  std::string subscript_type_from_list_literal(const Json &subscript_node);
  bool
  is_imported_name_in_body(const std::string &name, const Json &stmts) const;
  bool is_imported_name(const std::string &name) const;
  std::string infer_unpacked_element_type(const Json &rhs, size_t index);
  std::string resolve_object_class_name(const std::string &obj);
  std::string match_literal_argument(
    const Json &call_node,
    std::vector<Json> overloads) const;
  std::string resolve_overload_return_type(
    const std::string &func_name,
    const Json &call_node) const;
 
  // ----- core inference dispatchers -----
  std::string get_argument_type(const Json &arg);
  std::string get_dict_literal_type(const Json &dict_value);
  std::string get_call_type(const Json &arg);
  std::string get_attribute_type(const Json &arg);
  std::string class_attribute_type(
    const std::string &cls,
    const std::string &attr,
    bool constructed_only = false);
  std::string self_attribute_type(const Json &node);
  std::string get_operand_type(const Json &node);
  std::string get_builtin_call_type(const Json &call);
  // Type of a builtin call whose result depends on its argument (abs, hash),
  // or empty for any other call.
  std::string arg_dependent_call_type(const Json &call);
  std::string list_copy_type(const std::string &func_name, const Json &call);
  std::string dict_view_list_type(const Json &call);
  std::string get_type_from_binary_expr(const Json &stmt, const Json &body);
  bool is_array_operand(const Json &operand, const Json &body);
  std::string operand_annotation_type(const Json &decl);
  std::string get_type_from_rhs_variable(const Json &element, const Json &body);
  bool holds_callable_value(const std::string &name) const;
  std::string get_type_from_call(const Json &element);
  std::optional<std::string> get_type_from_literal_method(const Json &call);
  std::string get_type_from_method(const Json &call);
  std::string get_type_from_call_or_random(const Json &element);
  InferResult infer_type_from_ifexp(
    const Json &ifexp_node,
    const Json &body,
    std::string &inferred_type);
  std::optional<std::pair<Json, std::string>>
  function_signature(const function_values::candidate &function);
  std::string
  function_value_return_type(const Json &value, const Json *call = nullptr);
  InferResult
  infer_type(const Json &stmt, const Json &body, std::string &inferred_type);
  // True for a `np.<ctor>(...)` call node (module or aliased), where <ctor>
  // is one of the array-shape constructors whose numpy.py signature is a
  // generic `list[float]` the converter later replaces with a concrete
  // array type. Scopes infer_type's Attribute-Call branch decline to
  // exactly the calls that can hit the array_return_local_* gap.
  bool is_numpy_array_ctor_call(const Json &call_value) const;
  // True when the function currently being annotated (current_func) returns
  // `name` directly as its own trailing statement -- `return name`, or
  // identically through both arms of a trailing if/else. Mirrors
  // get_function_definition's local_var_numpy_array_return on the converter
  // side, at the granularity infer_type's decline needs (it only has to
  // know whether the name being assigned right now is the one at risk, not
  // reconstruct the whole pattern).
  bool current_func_returns_name_directly(const std::string &name) const;
  std::string
  get_function_return_type(const std::string &func_name, const Json &ast);
  std::string infer_lambda_return_type(const Json &lambda_elem) const;
  // Sets *divergent when branches return incompatible types.
  std::string infer_from_return_statements(
    const Json &body,
    const std::string &func_name,
    bool *divergent = nullptr);
  // The type a parameter's default value implies, or empty.
  std::string infer_type_from_parameter_default(
    const Json &function_element,
    size_t param_index,
    size_t param_count);
  // Return type of a FunctionDef @p member: its declared `-> T` (or `->
  // T[...]`) annotation, else the type inferred from its return statements,
  // else "Any".
  std::string
  method_return_type(const Json &member, const std::string &class_name);
  // Type inferred from the return statements of @p member, a method of
  // @p class_name, resolving names in the method's own scope, or empty.
  std::string
  infer_method_return_type(const Json &member, const std::string &class_name);
  void collect_return_types(
    const Json &body,
    const std::string &func_name,
    std::set<std::string> &types);
  // True if @p node (a return-value expression subtree) contains a direct call
  // to @p func_name. Used to skip self-recursive returns during return-type
  // inference so they don't re-enter the analysis (stack overflow).
  static bool
  expr_calls_function(const Json &node, const std::string &func_name);
  // True if the arithmetic expression @p node has an attribute read among its
  // operands, at any depth.
  static bool arithmetic_reads_attribute(const Json &node);
 
  // ----- annotation-node constructors (annotation_expr.inl) -----
  Json create_name_annotation(
    const std::string &type_id,
    int lineno,
    int col_offset,
    int end_lineno,
    int end_col_offset);
  Json create_subscript_annotation(
    const std::string &base_type,
    const std::string &element_type,
    int lineno,
    int col_offset,
    int end_lineno);
  // Build a `tuple[t0, t1, ...]` Subscript annotation node. Used by the
  // parameter-inference pass to specialise bare `tuple` annotations once
  // the element types have been recovered from call sites (GitHub #4515).
  Json create_tuple_subscript_annotation(
    const std::vector<std::string> &elem_types,
    int lineno,
    int col_offset,
    int end_lineno);
  Json create_annotation_from_type(
    const std::string &inferred_type,
    int lineno,
    int col_offset,
    int end_lineno);
  void update_assignment_node(Json &element, const std::string &inferred_type);
  void add_parameter_annotation(Json &param, const std::string &type);
  void update_end_col_offset(Json &ast);
 
  // ----- class inheritance and specialisation (annotation_symbolic.inl) -----
  bool are_all_user_classes(const std::vector<std::string> &types) const;
  bool are_specializable_types(const std::vector<std::string> &types) const;
  bool is_specialization_pending(
    const std::string &func_name,
    size_t param_index,
    const std::vector<std::string> &types) const;
  std::string build_specialized_function_name(
    const std::string &base_name,
    const std::string &class_name) const;
  std::string
  resolve_name_assigned_class(const std::string &name, const Json &node);
  void rewrite_specialized_calls(
    const std::string &original_name,
    size_t param_index,
    const std::unordered_map<std::string, std::string> &specialized_names,
    Json &node);
  void apply_pending_specializations();
  // Returns the ancestors of a class (including itself) in BFS order via
  // "bases". Handles multiple inheritance and cycle-safe (visited guard).
  // "object" is intentionally excluded — it has no ESBMC IR representation.
  std::vector<std::string> get_class_ancestors(const std::string &class_name);
  // Returns the lowest common ancestor of two user-defined class types,
  // or "" when none exists.
  std::string
  find_common_ancestor(const std::string &type_a, const std::string &type_b);
 
  // ----- per-class subscript-key tuple inference -----
  std::vector<std::string>
  infer_subscript_key_tuple_types(const std::string &class_name);
  void collect_class_instance_map(
    const Json &ast,
    std::unordered_map<std::string, std::string> &out) const;
  template <typename Visitor>
  void visit_class_tuple_subscripts(
    const Json &node,
    const std::string &class_name,
    const std::unordered_map<std::string, std::string> &var_to_class,
    Visitor &&visit,
    const Json *enclosing_func = nullptr);
  std::string resolve_name_in_enclosing_func(
    const std::string &name,
    const Json &enclosing_func);
  std::string resolve_wildcard_import_func(const std::string &func_name);
  bool reads_import(const std::string &name, const Json &use) const;
  std::string
  resolve_expr_in_enclosing_func(const Json &elt, const Json &enclosing_func);
  std::vector<std::string> infer_tuple_element_types(
    const Json &elts,
    const Json *enclosing_func = nullptr);
 
  // ----- function-call collection and parameter-type inference -----
  std::vector<std::string> collect_parameter_types_from_calls(
    size_t param_index,
    const std::vector<Json> &function_calls);
  std::vector<std::string> infer_tuple_param_types_from_calls(
    size_t param_index,
    const std::vector<Json> &function_calls);
  std::string infer_parameter_type_from_calls(
    size_t param_index,
    const std::vector<Json> &function_calls);
  struct caller_scopet
  {
    std::string root;
    std::string ctx;
    std::string class_prefix;
    bool in_lambda = false;
  };
  std::string caller_arg_type(const Json &arg, const caller_scopet &scope);
  void collect_caller_arg_types(
    const std::string &callee,
    size_t index,
    const Json &node,
    const caller_scopet &scope,
    std::vector<std::string> &types);
  std::vector<std::string> caller_arg_types(
    const std::string &func_name,
    size_t index,
    const Json &search_context);
  std::string infer_parameter_type_at_call_sites(
    const std::string &func_name,
    size_t param_index,
    const std::vector<Json> &function_calls,
    const Json &search_context);
  bool specializable_at_call_sites(
    const std::string &func_name,
    size_t param_index,
    std::vector<std::string> &call_types,
    const Json &search_context);
  void infer_parameter_types(Json &function_element);
 
  // ----- top-level orchestration entry points -----
  void annotate_global_scope();
  void annotate_function(Json &function_element);
  void annotate_class(Json &class_element);
  void infer_loop_variable_types(Json &while_stmt, bool synthesized_only);
  Json list_element_annotation(const Json &iter_node);
  Json self_attr_list_element(const std::string &attr);
  void annotate_branch_blocks(Json &element);
  void add_annotation(Json &body);
  std::string widen_to_optional_scalar(
    const Json &element,
    const std::string &inferred_type);
  std::string optional_scalar_of(const std::string &name, const Json &scope);
  std::string returned_optional_scalar(const Json &function, const Json &body);
  void collect_name_stores(
    const std::string &name,
    const Json &body,
    std::vector<const Json *> &stores);
 
  // ----- state -----
  Json &ast_;
  global_scope &gs_;
  std::shared_ptr<module_manager> module_manager_;
  Json *current_func;
  Json
    *parent_func; // Track parent function for nested function scope resolution
  int current_line_;
  std::string python_filename_;
  bool filter_global_elements_ = false;
  // True only while add_type_annotation(func_name) (the --function
  // entry-point pass over the *main* module) is running, so add_annotation's
  // bare-call forward-reference scan is scoped to that module. The scan
  // searches only the current ast_, so applying it while annotating an
  // *imported* module (e.g. an OM calling another OM's helper) would throw
  // on any name that module itself imports (github #5937).
  bool annotating_function_entry_point_ = false;
  std::vector<Json> referenced_global_elements;
  std::set<std::string> functions_in_analysis_;
  // Functions whose recursive-branch inference is itself running. A second
  // re-entry means the self-reference is indirect (the returned name's binding
  // calls the function), which the return-expression scan cannot see.
  std::set<std::string> functions_reentered_;
  std::set<std::string> resolving_rhs_vars_;
  // Per (scope, name): the Optional[T] annotation of a name stored None and
  // one scalar type T, decided before any of its stores is annotated.
  std::map<std::pair<const Json *, std::string>, std::string>
    optional_scalar_names_;
  std::string current_func_name_context_;
  std::string current_class_name_;
  struct pending_specializationt
  {
    std::string function_name;
    size_t param_index;
    std::vector<std::string> class_types;
  };
  std::vector<pending_specializationt> pending_specializations_;
  void retype_builtin_copy(
    Json &fn,
    const pending_specializationt &spec,
    const std::string &type,
    const std::vector<Json> &calls);
  std::vector<const Json *> extra_subscript_inference_asts_;
};
 
// Out-of-class template member definitions. These files are part of
// this header and must not be included independently — the
// definitions need the `python_annotation<Json>` class layout above.
#include <python-frontend/python_annotation/annotation_conversion.inl>
#include <python-frontend/python_annotation/annotation_expr.inl>
#include <python-frontend/python_annotation/annotation_symbolic.inl>