python_converter.h

Go to the documentation of this file.

#pragma once
 
#include <array>
#include <deque>
#include <functional>
#include <nlohmann/json.hpp>
#include <python-frontend/math/complex_handler.h>
#include <python-frontend/function_call/cache.h>
#include <python-frontend/module/global_scope.h>
#include <python-frontend/python-dict/python_dict_handler.h>
#include <python-frontend/dynamic_type/dynamic_type_handler.h>
#include <python-frontend/dynamic_type/literal_divergence.h>
#include <python-frontend/math/python_math.h>
#include <python-frontend/numpy/numpy_nditer.h>
#include <python-frontend/string/string_handler.h>
#include <python-frontend/type/element_type_registry.h>
#include <python-frontend/type/type_handler.h>
#include <python-frontend/type/type_utils.h>
#include <python-frontend/set/python_set.h>
#include <util/symtab/context.h>
#include <util/symtab/namespace.h>
#include <util/irep/std_code.h>
#include <util/symtab/symbol_generator.h>
#include <functional>
#include <map>
#include <optional>
#include <set>
#include <tuple>
#include <unordered_map>
#include <unordered_set>
#include <utility>
#include <vector>
 
class codet;
class struct_typet;
class function_id;
class symbol_id;
class function_call_expr;
class type_handler;
class string_builder;
class module_locator;
class tuple_handler;
class python_typechecking;
class python_class_builder;
class python_lambda;
class python_exception_handler;
class get_expr_depth_guard;
 
// Defined in converter_stmt.cpp; shared with numpy_call_expr.cpp so both can
// verify a Name/Attribute receiver actually resolves to the imported numpy
// module before treating a call as a numpy constructor/method.
bool is_imported_numpy_module_alias(
  const nlohmann::json &ast,
  const std::string &name);
 
// One `Call` node together with the name of the function whose body it
// textually appears in (empty for a module-level call). Declared here (Impl
// in converter_funcdef.cpp) so python_converter can cache the whole-AST scan
// that finds these instead of every caller re-walking the AST itself.
struct numpy_param_call_site
{
  const nlohmann::json *call;
  std::string enclosing_function;
};

class python_converter
{
public:
  python_converter(
    contextt &_context,
    const nlohmann::json *ast,
    const global_scope &gs,
    const std::vector<nlohmann::json> *extra_asts = nullptr);
 
  ~python_converter();
 
  void convert();
 
  // Accessors for handlers
  void set_converting_rhs(bool value)
  {
    is_converting_rhs = value;
  }
  void set_current_lhs(exprt *value)
  {
    current_lhs = value;
  }
  void set_current_func_name(const std::string &name)
  {
    current_func_name_ = name;
  }
  void set_current_element_type(const typet &type)
  {
    current_element_type = type;
  }
  symbolt *add_symbol_and_get_ptr(symbolt &symbol)
  {
    return symbol_table_.move_symbol_to_context(symbol);
  }
 
  exprt create_lhs_expression(
    const nlohmann::json &target,
    symbolt *lhs_symbol,
    const locationt &location);
 
  const std::string &get_current_func_name() const
  {
    return current_func_name_;
  }
  const nlohmann::json &get_ast_json() const
  {
    return *ast_json;
  }

  symbolt *contract_return_value_symbol(
    const std::string &var_name,
    const nlohmann::json &element);
 
  exprt get_expr(const nlohmann::json &element);

  exprt handle_tuple_operations(
    const std::string &op,
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &element);
 
  std::string get_op(const std::string &op, const typet &type) const;
  typet get_callable_type(
    const nlohmann::json &annotation,
    const nlohmann::json &stmt);
  typet returned_function_type(const nlohmann::json &function_node);
  typet named_return_type(
    const std::string &name,
    const nlohmann::json &return_node,
    const nlohmann::json &function_node);
  typet named_callee_type(const std::string &name);
  std::optional<code_typet> returned_function(const nlohmann::json &callee);
  std::optional<exprt> call_returned_function(const nlohmann::json &element);
  void convert_lambda_call(
    const nlohmann::json &element,
    side_effect_expr_function_callt &call);
  const symbolt *
  lambda_copy_for_call(const nlohmann::json &call, const symbolt &var);
  bool call_lambda_copy(
    const nlohmann::json &element,
    const symbolt &var,
    side_effect_expr_function_callt &call,
    const code_typet *&callee_type);
  std::optional<exprt> call_property_value(const nlohmann::json &element);
  bool may_be_callable(const typet &type);
  exprt not_callable_function(
    const typet &function,
    const typet &value,
    const locationt &location);
  void decay_function_choice(exprt &then, exprt &else_expr);
 
  typet get_type_from_annotation(
    const nlohmann::json &annotation_node,
    const nlohmann::json &element);

  typet get_optional_type(const nlohmann::json &slice);
  typet optional_container_type(const nlohmann::json &slice);
 
  string_builder &get_string_builder();
 
  python_dict_handler *get_dict_handler()
  {
    return dict_handler_;
  }
 
  python_exception_handler &get_exception_handler()
  {
    return *exception_handler_;
  }
 
  const python_exception_handler &get_exception_handler() const
  {
    return *exception_handler_;
  }
 
  python_math &get_math_handler()
  {
    return math_handler_;
  }
 
  complex_handler &get_complex_handler()
  {
    return complex_handler_;
  }
 
  string_handler &get_string_handler()
  {
    return string_handler_;
  }
 
  tuple_handler &get_tuple_handler() const
  {
    return *tuple_handler_;
  }
 
  const nlohmann::json &ast() const
  {
    return *ast_json;
  }
 
  contextt &symbol_table() const
  {
    return symbol_table_;
  }
 
  type_handler &get_type_handler()
  {
    return type_handler_;
  }
 
  element_type_registry &get_element_type_registry()
  {
    return element_type_registry_;
  }
 
  const element_type_registry &get_element_type_registry() const
  {
    return element_type_registry_;
  }

  void mark_list_call_escaped(const std::string &id)
  {
    call_escaped_lists_.insert(id);
  }
 
  bool is_list_call_escaped(const std::string &id) const
  {
    return call_escaped_lists_.find(id) != call_escaped_lists_.end();
  }

  void outlive_scope(const std::string &id);

  void defer_check(std::function<void()> check)
  {
    deferred_checks_.push_back(std::move(check));
  }
 
  bool type_assertions_enabled() const;
 
  const std::string &python_file() const
  {
    return current_python_file;
  }
 
  const std::string &main_python_filename() const
  {
    return main_python_file;
  }
 
  const std::string &current_function_name() const
  {
    return current_func_name_;
  }
 
  const std::string &current_classname() const
  {
    return current_class_name_;
  }

  std::string current_ast_scope() const;
 
  const namespacet &name_space() const
  {
    return ns;
  }
 
  function_call_cache &get_function_call_cache()
  {
    return function_call_cache_;
  }
 
  const function_call_cache &get_function_call_cache() const
  {
    return function_call_cache_;
  }
 
  void add_symbol(const symbolt s)
  {
    symbol_table_.add(s);
  }
 
  void add_instruction(const exprt &expr)
  {
    if (current_block)
      current_block->copy_to_operands(expr);
  }
 
  // Converts `ast_node` (an Assign statement) into GOTO and appends it to
  // current_block, the same way any real source-level assignment is
  // converted -- for a caller (numpy argument hoisting) that only has
  // add_instruction's implicit current_block, not a codet& of its own to
  // pass to get_var_assign directly. False when there is no current block to
  // emit into (e.g. converting outside statement context).
  bool emit_statement_into_current_block(const nlohmann::json &ast_node)
  {
    if (!current_block || !safe_to_emit_side_effecting_statement())
      return false;
    // get_var_assign always leaves current_lhs pointing at its own target
    // (or null) when it returns, clobbering whatever an enclosing
    // assignment's own RHS conversion had it pointing at -- e.g. a call
    // argument hoisted into a temp mid-conversion (hoist_call_argument_
    // into_temp) would otherwise silently erase the outer assignment's
    // ability to retype its own target from the freshly computed RHS
    // (retype_current_lhs_and_return and friends), leaving a stale
    // static-annotator guess in place. Save and restore around the nested
    // statement so it only ever affects its own target.
    exprt *outer_lhs = current_lhs;
    bool outer_is_converting_rhs = is_converting_rhs;
    bool outer_is_converting_lhs = is_converting_lhs;
    const nlohmann::json *outer_store_target = lhs_store_target_;
    typet outer_element_type = current_element_type;
    get_var_assign(ast_node, *current_block);
    current_lhs = outer_lhs;
    is_converting_rhs = outer_is_converting_rhs;
    is_converting_lhs = outer_is_converting_lhs;
    lhs_store_target_ = outer_store_target;
    current_element_type = outer_element_type;
    return true;
  }
 
  // True where a side-effecting statement (e.g. a hoisted temporary
  // assignment) is safe to plant into current_block without being evaluated
  // an extra time or leaking into a specification -- the same guard
  // needs_zero_division_guard applies before hoisting a side-effecting
  // divisor: not a lambda body at its definition (operands still unbound),
  // not the discarded type-probe pass of an assignment RHS (which runs the
  // real conversion again right after), and not inside a contract clause
  // (which must not plant a statement into the enclosing block at all).
  bool safe_to_emit_side_effecting_statement() const
  {
    return !converting_lambda_body_ && !in_rhs_type_probe_ &&
           !in_contract_clause_;
  }
 
  // A runtime guard emitted into current_block runs once, unconditionally,
  // ahead of the enclosing statement; that is wrong for an expression Python
  // evaluates conditionally or repeatedly (an and/or tail, a while test).
  bool can_emit_runtime_guard() const
  {
    return current_block && safe_to_emit_side_effecting_statement() &&
           !in_lazy_operand_;
  }
 
  // A raise lowers to a jump to the function's end, which every later state
  // then merges with, so a guard that only replaces an operational-model
  // assert is planted only where an enclosing `try` can catch it.
  bool can_emit_catchable_guard() const
  {
    return try_body_depth_ > 0 && can_emit_runtime_guard();
  }

  void capture_lambda_free_variables(
    const nlohmann::json &lambda_node,
    const std::string &lambda_id,
    const locationt &location);
 
  // Hoists @p operand into a temporary when it carries a side effect, so a
  // guard and its use evaluate it once.
  exprt hoist_side_effecting_operand(
    const exprt &operand,
    const nlohmann::json &element,
    const std::string &prefix);

  void guard_attribute_on_none(
    const exprt &base,
    const std::string &attr_name,
    const nlohmann::json &element,
    bool is_self = false);
 
  codet get_compound_store(
    const exprt &lhs,
    const exprt &rhs,
    const locationt &location);
  void emit_guarded_raise(
    const exprt &cond,
    const std::string &exception,
    const std::string &message,
    const locationt &location);
 
  exprt handle_tuple_add(
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &element);
 
  // `tuple + list` or `list + tuple`: raises TypeError unless the list was
  // built by tuple(x) (#8777), in which case the result is that tuple
  // concatenated with the other one.
  exprt concat_tuple_with_list(
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &element);
 
  // Raises OverflowError (infinity) or ValueError (NaN) before a float
  // @p operand is converted to int, and with @p reject_none TypeError for a
  // pointer @p operand that is None; returns the operand to convert.
  exprt guard_nonfinite_float_to_int(
    exprt operand,
    const nlohmann::json &element,
    bool reject_none = false);
 
  // Raises TypeError with @p message before a None-typed @p operand of
  // float() is converted, when it holds None.
  exprt guard_none_conversion(
    exprt operand,
    const std::string &message,
    const nlohmann::json &element);
 
  exprt fit_numpy_integer_store(
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &value);
 
  void update_symbol(const exprt &expr) const;
 
  symbolt *find_symbol(const std::string &symbol_id) const;
 
  bool is_imported_module(const std::string &module_name) const;
  nlohmann::json callable_function_stubs() const;
  bool is_retyped(const irep_idt &id) const
  {
    return retype_aliases_.count(id.as_string()) > 0;
  }

  struct scope_bindings
  {
    bool by_import = false;
    bool by_other = false;
    bool declared_outer = false;
  };

  static scope_bindings
  module_scope_bindings(const nlohmann::json &module, const std::string &name);
  static std::optional<bool> binding_is_import(
    const nlohmann::json &module,
    const scope_bindings &global,
    const nlohmann::json *function,
    bool in_class,
    bool in_order,
    const std::string &name,
    const nlohmann::json &use);
  bool name_shadows_module(
    const nlohmann::json &receiver,
    const nlohmann::json &use) const;
  bool is_module_receiver(
    const std::string &module_name,
    const nlohmann::json &receiver,
    const nlohmann::json &use) const;
  std::string current_module_name() const;
 
  const std::string
  get_imported_module_path(const std::string &module_name) const
  {
    if (imported_modules.find(module_name) != imported_modules.end())
      return imported_modules.at(module_name);
 
    return {};
  }
 
  symbolt create_symbol(
    const std::string &module,
    const std::string &name,
    const std::string &id,
    const locationt &location,
    const typet &type) const;
 
  // Register a ``void name(void)`` C intrinsic in the Python symbol
  // table if not already present. Used for ESBMC built-ins whose bodies
  // live in the C library (cprover_library) but whose call sites are
  // synthesised by the Python frontend (atomic_begin/end, yield, the
  // pthread main hooks, __pyt_*); the C-style ``c:@F@<name>`` id is
  // needed so c2goto's linker resolves the call to the library body.
  void ensure_void_void_intrinsic(
    const std::string &name,
    const locationt &location);
 
  exprt make_char_array_expr(
    const std::vector<unsigned char> &string_literal,
    const typet &t);

  exprt make_class_object(const std::string &name);

  exprt class_value(const std::string &name);
  exprt as_class_value(const exprt &e);
  exprt compare_class_values(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs);
  bool binds_runtime_class(const nlohmann::json &ast_node, const exprt &rhs);
  bool settle_target_type(
    symbolt *lhs_symbol,
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &ast_node);

  ExpressionType expression_type(const nlohmann::json &element) const;

  exprt class_mro_tuple(const nlohmann::json &element);
 
  static bool is_class_object(const exprt &expr)
  {
    return expr.is_constant() && expr.type().is_array() &&
           !expr.get("value").empty();
  }
 
  exprt get_literal(const nlohmann::json &element);
 
  locationt get_location_from_decl(const nlohmann::json &element) const;
 
  void copy_location_fields_from_decl(
    const nlohmann::json &from,
    nlohmann::json &to) const;
 
  exprt handle_string_comparison(
    const std::string &op,
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &element);
 
  bool scalar_order(
    exprt a,
    exprt b,
    const nlohmann::json &element,
    expr2tc &lt,
    expr2tc &eq);
 
  size_t unordered_tuple_component(
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &element);
 
  void raise_on_unordered_tie(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs,
    size_t unordered,
    const expr2tc &prefix_eq,
    const nlohmann::json &element);
 
  python_typechecking &get_typechecker();
  const python_typechecking &get_typechecker() const;

  bool enter_contract_clause(bool entering)
  {
    return std::exchange(in_contract_clause_, in_contract_clause_ || entering);
  }
  void restore_contract_clause(bool saved)
  {
    in_contract_clause_ = saved;
  }
  bool in_contract_clause() const
  {
    return in_contract_clause_;
  }
  size_t current_block_statement_count() const
  {
    return current_block ? current_block->operands().size() : 0;
  }

  const std::string *class_object_name(const irep_idt &id) const
  {
    auto it = class_object_names_.find(id);
    return it == class_object_names_.end() ? nullptr : &it->second;
  }
 
private:
  // Hoists @p operand once and plants @p emit_guards over its value where the
  // operand is evaluated, also inside an and/or tail or a while test.
  exprt guard_operand(
    exprt operand,
    const nlohmann::json &element,
    const std::string &prefix,
    const std::function<void(const expr2tc &, const locationt &)> &emit_guards);
 
  friend class bounded_math;
  friend class complex_handler;
  friend class function_call_expr;
  friend class numpy_call_expr;
  friend class numpy_random;
  friend class numpy_nditer;
  friend class function_call_builder;
  friend class type_handler;
  friend class python_list;
  friend class string_handler;
  friend class tuple_handler;
  friend class dynamic_type_handler;
  friend class python_typechecking;
  friend class python_class_builder;
  friend class python_dict_handler;
  friend class python_set;
  friend class python_exception_handler;
  friend class get_expr_depth_guard;
  friend class python_converter_test_access;
 
  template <typename Func>
  decltype(auto) with_ast(const nlohmann::json *new_ast, Func &&f)
  {
    const nlohmann::json *old_ast = ast_json;
    ast_json = new_ast;
    auto result = f();
    ast_json = old_ast;
    return result;
  }
 
  void load_c_intrisics(code_blockt &block);
 
  void get_var_assign(const nlohmann::json &ast_node, codet &target_block);
 
  void preregister_global_variables(const nlohmann::json &ast_body);

  std::string annotated_optional_class(const nlohmann::json &annotation) const;
 
  typet
  resolve_variable_type(const std::string &var_name, const locationt &loc);
 
  void get_compound_assign(const nlohmann::json &ast_node, codet &target_block);

  symbolt *find_symbol_in_enclosing_scopes(const std::string &name);
 
  symbolt *resolve_subscript_base_symbol(
    const nlohmann::json &target,
    const std::string &name,
    symbolt *found);

  void mark_augassign_list_escaped(const exprt &lhs, const exprt &rhs);
 
  void
  get_return_statements(const nlohmann::json &ast_node, codet &target_block);
  void get_return_with_conditional_spelling(
    const nlohmann::json &ast_node,
    codet &target_block);
 
  void get_function_definition(const nlohmann::json &function_node);

  exprt dispatch_mismatched_callees(
    const exprt &callee,
    const nlohmann::json &call,
    const side_effect_expr_function_callt &call_expr);
 
  exprt get_function_body_or_unsupported(const nlohmann::json &function_node);

  static exprt hoist_local_declarations(exprt body);
 
  bool function_may_be_called(const nlohmann::json &function_node) const;
 
  void
  get_class_definition(const nlohmann::json &class_node, codet &target_block);
 
  exprt get_unary_operator_expr(const nlohmann::json &element);

  exprt get_named_expr(const nlohmann::json &element);

  static bool contains_named_expr(const nlohmann::json &node);

  static bool contains_nested_scope_named_expr(const nlohmann::json &node);
 
  exprt get_binary_operator_expr(const nlohmann::json &element);
  std::optional<exprt> try_bound_method_compare(const nlohmann::json &element);
  std::optional<std::pair<exprt, std::string>>
  bound_method_operand(const nlohmann::json &operand);
  exprt get_binary_operator_expr(
    const nlohmann::json &element,
    const nlohmann::json &left,
    const nlohmann::json &right,
    const std::string &op,
    exprt &lhs,
    exprt &rhs);
  exprt
  keep_operand_calls(const exprt &result, const exprt &lhs, const exprt &rhs);

  exprt checked_erased_int(
    exprt operand,
    const nlohmann::json &node,
    const nlohmann::json &element);
  exprt get_right_operand_expr(
    const nlohmann::json &element,
    const nlohmann::json &right,
    const exprt &lhs);
  exprt build_division_guarded_binop(
    const std::string &op,
    exprt lhs,
    exprt rhs,
    const nlohmann::json &element);
  exprt build_arithmetic_binop(
    const std::string &op,
    exprt lhs,
    exprt rhs,
    const nlohmann::json &element);
  std::vector<typet>
  percent_arg_types(const nlohmann::json &right, const exprt &rhs) const;
  exprt get_fstring_in_order(const nlohmann::json &joined);
  exprt get_percent_format_expr(
    const nlohmann::json &left,
    const std::vector<nlohmann::json> &args,
    const std::map<std::string, nlohmann::json> &mapping,
    const std::vector<typet> &arg_types);

  std::string get_python_type_category(const typet &t) const;
 
  bool is_bytes_literal(const nlohmann::json &element);
 
  // V.3: build the `is` identity equality in IREP2 (shared by the `is` and
  // `is not` paths); the public wrappers back-migrate once at the legacy seam.
  expr2tc build_is_equality(
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right);
 
  exprt get_binary_operator_expr_for_is(
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right);
 
  exprt get_negated_is_expr(
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right);
 
  exprt get_resolved_value(const exprt &expr);
 
  exprt get_function_constant_return(const exprt &func_value);
 
  exprt resolve_function_call(const exprt &func_expr, const exprt &args_expr);
 
  exprt get_lambda_expr(
    const nlohmann::json &element,
    const std::vector<std::optional<typet>> &argument_types = {});
 
  codet convert_expression_to_code(exprt &expr);
 
  std::string remove_quotes_from_type_string(const std::string &type_string);
 
  bool function_has_missing_return_paths(const nlohmann::json &function_node);
 
  bool function_is_generator(const nlohmann::json &function_node);
 
  exprt materialize_list_function_call(
    const exprt &expr,
    const nlohmann::json &element,
    codet &target_block);
 
  std::optional<typet> call_dict_value_type(const nlohmann::json &call);
 
  symbolt create_return_temp_variable(
    const typet &return_type,
    const locationt &location,
    const std::string &func_name);
 
  // Stage 1 object-model migration (#3067): copy a constructed class *value*
  // onto a fresh non-expiring `__ESBMC_new_object` heap object and return the
  // pointer to it, so a `-> Cls` function can hand back a `Cls*` reference that
  // survives its frame. `current_func_return_type_` must be the migrated
  // pointer type. Used by both return paths in get_return_statements.
  exprt box_value_on_heap(
    const exprt &value,
    const locationt &location,
    codet &target_block);
 
  // Same, but boxing behind an explicit pointer type instead of
  // `current_func_return_type_` (e.g. `char (*)[N]` for a local string
  // array whose bytes must survive the frame, #5571).
  exprt box_value_on_heap(
    const exprt &value,
    const locationt &location,
    codet &target_block,
    const typet &ptr_type);
 
  void register_instance_attribute(
    const std::string &symbol_id,
    const std::string &attr_name,
    const std::string &var_name,
    const std::string &class_tag);

  void reject_maybe_unset_instance_attr(
    bool instance_written,
    const symbolt &symbol,
    const std::string &var_name,
    const std::string &attr_name,
    const std::string &obj_type_name);
 
  bool is_instance_attribute(
    const std::string &symbol_id,
    const std::string &attr_name,
    const std::string &var_name,
    const std::string &class_tag);
 
  exprt create_member_expression(
    const symbolt &symbol,
    const std::string &attr_name,
    const typet &attr_type);
 
  typet clean_attribute_type(const typet &attr_type);
 
  std::string create_normalized_self_key(const std::string &class_tag);
 
  std::string extract_class_name_from_tag(const std::string &tag_name);

  symbolt *find_class_attribute_symbol(
    const std::string &class_name,
    const std::string &attr_name);

  std::vector<dynamic_type_detail::numeric_bindingt> scope_numeric_bindings(
    const std::string &name,
    int before,
    bool include_later) const;
 
  void reject_inexact_number_join(
    const nlohmann::json &element,
    const exprt &expr) const;
 
  // The class name `t` names, or empty when it is neither a struct nor a
  // `tag-<Class>` symbol reference.
  std::string class_name_of(const typet &t);
 
  // True iff `t` denotes a user-defined Python class struct — either the struct
  // itself or a `symbol_typet("tag-<Class>")` reference to it (robust to
  // whether the struct has been built yet). Excludes the list/dict/object model
  // structs.
  bool is_user_class_struct_type(const typet &t);
 
  // True iff `t` is a user class the object model migrates to the heap and
  // stores in a container as a `Class*`. A reserved `__ESBMC` name opts out:
  // the push and read paths must agree on which classes stay inline, so both
  // gate on this one predicate (#7685).
  bool is_heap_migrated_class_type(const typet &t);
 
  // True iff `t` is a pointer to a user-defined class struct (a migrated
  // `Class*` instance). Used to gate the object-model migration's
  // None-keeps-Class* and dunder-dispatch-through-pointer paths to real
  // classes.
  bool is_user_class_pointer(const typet &t);
 
  // Widen a symbol rebound from a non-class placeholder (None, Any, a bare
  // scalar) to a class-pointer binding. Only those types are widened: a
  // struct-shaped one may already back an expression built elsewhere.
  void retype_placeholder_to_class(symbolt &sym, const typet &new_type);
 
  exprt resolve_identity_function_call(
    const exprt &func_expr,
    const exprt &args_expr);
 
  bool is_identity_function(
    const exprt &func_value,
    const std::string &func_identifier);
 
  exprt handle_none_comparison(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs);

  exprt handle_none_operand(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs);
 
  void raise_on_optional_none(
    const std::string &op,
    const exprt &lhs_none,
    const exprt &rhs_none,
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &element);

  exprt try_lower_slice_member_is_none(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs);
 
  symbolt &create_tmp_symbol(
    const nlohmann::json &element,
    const std::string var_name,
    const typet &symbol_type,
    const exprt &symbol_value);

  symbolt &create_tmp_symbol(
    const locationt &location,
    const std::string var_name,
    const typet &symbol_type,
    const exprt &symbol_value);
 
  exprt get_logical_operator_expr(const nlohmann::json &element);
 
  exprt get_boolop_operand(
    const nlohmann::json &operand,
    std::vector<code_blockt> &effects);
 
  exprt lower_short_circuit_boolop(
    const exprt &logical_expr,
    const std::vector<code_blockt> &effects,
    const std::function<exprt(const exprt &)> &truthy,
    const nlohmann::json &element);
 
  exprt emit_guarded_boolop(
    const exprt &logical_expr,
    const std::vector<code_blockt> &effects,
    const std::function<exprt(const exprt &)> &truthy,
    const locationt &location);

  exprt get_flat_boolop_test(
    const nlohmann::json &test_node,
    const std::function<exprt(const exprt &, const nlohmann::json &)> &to_bool);
 
  exprt get_conditional_stm(const nlohmann::json &ast_node);

  bool rewrite_divergent_conditional_assign(
    const nlohmann::json &ast_node,
    codet &target_block);
 
  std::string instantiated_class(const nlohmann::json &value) const;
 
  bool ternary_needs_if_spelling(const nlohmann::json &ifexp) const;
  void reject_divergent_attribute_classes(
    const nlohmann::json &target,
    const nlohmann::json &ifexp) const;
 
  bool is_coverage_mode() const;
 
  bool is_assert_fold_disabled() const;
 
  bool is_pytest_generation_mode() const;
 
  bool is_model_file(const nlohmann::json &node) const;

  bool is_program_file(const std::string &file) const;
 
  exprt get_function_call(const nlohmann::json &ast_block);
  exprt get_call_expr(const nlohmann::json &element);

  exprt get_len_on_class_instance(const nlohmann::json &element);
  static bool is_pure_read(const nlohmann::json &node);
  exprt
  get_len_on_list_element(const nlohmann::json &arg, const locationt &location);
  static exprt list_element_type_id(const exprt &value);
  std::size_t count_user_classes();
  exprt checked_len_result(const exprt &len_call, const locationt &location);
 
  // len(v) where v is a pointer-backed numpy view (ADR-NP-003 etapa 2, 1-D
  // slice views). Split out of get_function_call() to keep that already
  // large function's own decision count from growing further; see
  // converter_funcall.cpp for the full rationale.
  std::optional<exprt>
  try_get_numpy_pointer_view_len(const nlohmann::json &element);
  std::optional<exprt>
  try_get_numpy_named_pointer_view_len(const nlohmann::json &arg) const;
  std::optional<exprt> try_get_numpy_subscript_pointer_view_len(
    const nlohmann::json &arg,
    const nlohmann::json &element);
 
  // v.shape / v.ndim where v is a pointer-backed numpy view (ADR-NP-003
  // etapa 2, 1-D slice views): unwrapping the pointer only reaches the
  // scalar element type, not a shape, so the view's own tracked logical
  // length is used instead. Split out of get_expr() to keep that already
  // large function's own decision count from growing further; see
  // converter_expr.cpp for the full rationale. Returns std::nullopt for
  // any other attribute or an untracked symbol, so the caller falls
  // through to the existing array/list handling.
  std::optional<exprt> try_get_numpy_pointer_view_shape_attr(
    const symbolt &symbol,
    const std::string &attr_name);
 
  // v.shape / v.ndim / v.size where v is a 2-D+ numpy array parameter: its
  // full logical shape is tracked in numpy_param_shapes_ (populated by
  // register_function_argument before the C-ABI row-pointer decay erases the
  // outer dimension). Mirrors try_get_numpy_pointer_view_shape_attr's split
  // reasoning. Returns std::nullopt for any other attribute or an untracked
  // symbol, so the caller falls through to the existing array/list handling.
  std::optional<exprt> try_get_numpy_param_shape_attr(
    const symbolt &symbol,
    const std::string &attr_name);
 
  // Tries try_get_numpy_pointer_view_shape_attr then
  // try_get_numpy_param_shape_attr, so get_expr's own Attribute dispatch
  // needs a single `if` for both tracked-shape sources instead of growing
  // its own decision count by one per source.
  std::optional<exprt>
  try_get_numpy_shape_attr(const symbolt &symbol, const std::string &attr_name);
 
  std::optional<std::vector<std::size_t>>
  tracked_numpy_shape_from_name(const std::string &name) const;
 
  std::optional<std::vector<std::size_t>>
  numpy_shape_from_indexed_decl(const std::string &name) const;
 
  exprt numpy_shape_attr_expr(
    const std::vector<std::size_t> &shape,
    const std::string &attr_name);
 
  std::optional<std::vector<std::size_t>>
  get_numpy_constructor_shape(const nlohmann::json &node) const;
 
  std::optional<exprt> try_get_numpy_value_shape_attr(
    const exprt &base_expr,
    const nlohmann::json &base_node,
    const std::string &attr_name);
 
  std::optional<exprt>
  try_get_numpy_shape_subscript(const nlohmann::json &element) const;
 
  std::optional<exprt> try_get_numpy_tracked_value_shape_attr(
    const exprt &base_expr,
    const nlohmann::json &base_node,
    const std::string &attr_name);
 
  void reject_numpy_shape_attr_on_nonobject_call_result(
    const exprt &base_expr,
    const nlohmann::json &base_node,
    const std::string &attr_name);
 
  bool should_reject_numpy_shape_attr_on_symbol(
    const symbolt &symbol,
    const std::string &attr_name);
 
  std::optional<exprt> try_get_numpy_bool_mask_rows_shape_attr(
    const exprt &base_expr,
    const typet &base_type,
    const std::string &attr_name);
 
  exprt get_block(
    const nlohmann::json &ast_block,
    bool is_function_body = false,
    bool is_loop_body = false);
 
  exprt get_static_array(const nlohmann::json &arr, const typet &shape);
 
  void adjust_statement_types(exprt &lhs, exprt &rhs) const;
 
  symbol_id create_symbol_id() const;

  void find_entry_function(
    const std::string &target,
    nlohmann::json &node,
    std::string &owning_class) const;
 
  symbol_id create_symbol_id(const std::string &filename) const;
 
  void promote_int_to_float(exprt &op, const typet &target_type) const;
 
  void handle_float_division(exprt &lhs, exprt &rhs, exprt &bin_expr) const;
 
  exprt get_tuple_expr(const nlohmann::json &element);

  exprt build_slice_object(const nlohmann::json &slice_node);

  exprt build_slice_from_args(
    const nlohmann::json &args,
    const nlohmann::json &source_node);
 
  std::pair<exprt, exprt>
  resolve_comparison_operands_internal(const exprt &lhs, const exprt &rhs);
 
  bool
  has_unsupported_side_effects_internal(const exprt &lhs, const exprt &rhs);
 
  TypeFlags infer_types_from_returns(const nlohmann::json &function_body);
 
  void process_function_arguments(
    const nlohmann::json &function_node,
    code_typet &type,
    const symbol_id &id,
    const locationt &location);
 
  // Records a numpy array parameter's pre-decay shape (when 2-D+) and its
  // tracked-array-symbol status once its arg_id is known. Split out of
  // register_function_argument to keep that function's own decision count
  // down -- both conditions live in here instead of as two more `if`s there.
  void track_numpy_param(
    const std::string &arg_id,
    const std::optional<std::vector<std::size_t>> &numpy_param_full_shape,
    bool numpy_array_param,
    const typet &array_type);
 
  // A numpy array parameter decays to a pointer; element-wise arithmetic
  // reads it back through its pre-decay array type.
  exprt numpy_param_as_array(const exprt &operand) const;
  exprt snapshot_left_operand(
    const nlohmann::json &left,
    const exprt &lhs,
    const nlohmann::json &right);
  bool may_rebind_left(
    const nlohmann::json &left,
    const exprt &lhs,
    const nlohmann::json &right) const;
  bool calls_user_code(const nlohmann::json &node) const;
  exprt
  materialize_numpy_arithmetic(const nlohmann::json &node, const exprt &value);
  std::optional<std::vector<std::size_t>>
  numpy_param_shape(const std::string &symbol_id) const;
 
  size_t register_function_argument(
    const nlohmann::json &element,
    code_typet &type,
    const symbol_id &id,
    const locationt &location,
    bool is_keyword_only);

  code_blockt create_capture_cells(
    const nlohmann::json &function_node,
    const symbol_id &id,
    const locationt &location);
 
  code_blockt bind_capture_cells(
    const std::set<std::string> &free_names,
    const std::string &enclosing_scope,
    const std::string &func_id,
    const locationt &location);

  code_blockt pending_captures_;

  const nlohmann::json *enclosing_function_node_ = nullptr;

  bool try_infer_numpy_param_type(
    const std::string &func_name,
    size_t param_index,
    typet &out,
    std::set<std::string> &visiting) const;
 
  // A call-site argument that resolves to a numpy array's element type: a
  // literal `np.array([...])` call (is_numpy_array_literal_call), or a
  // `Call` to a user function whose body unconditionally returns one
  // (numpy_array_literal_return in converter_funcdef.cpp). nullopt for
  // anything else. Replaces try_infer_numpy_param_type's own former
  // is_numpy_array_literal_call() check one-for-one (same call count there)
  // instead of adding a second, separate dispatch branch for the `Call`
  // case, to keep that function's own decision count down.
  std::optional<typet> try_infer_numpy_array_arg_type(
    const nlohmann::json &arg,
    const nlohmann::json &module_body) const;

  bool try_infer_dynamic_param_type(
    const std::string &callee,
    const std::string &param_name,
    size_t param_index) const;
 
  typet ctor_param_attr_type(
    const std::vector<const nlohmann::json *> &module_bodies,
    const std::string &class_name,
    const std::string &param_name,
    int param_idx) const;
 
  void reject_one_sided_tagged_store(const exprt &lhs, const exprt &rhs) const;

  bool infer_bytes_param_size_from_call_sites(
    const std::string &func_name,
    size_t param_index,
    long long &out_size) const;
  bool infer_bytes_param_size_from_call_sites(
    const std::string &func_name,
    size_t param_index,
    long long &out_size,
    std::set<std::string> &visiting) const;

  std::optional<long long> resolve_forwarded_bytes_param_size(
    const nlohmann::json &arg,
    const nlohmann::json &module_body,
    const std::string &enclosing_function,
    std::set<std::string> &visiting) const;

  std::optional<long long> resolve_bytes_call_site_arg_size(
    const std::string &enclosing_function,
    const nlohmann::json &call,
    size_t param_index,
    const nlohmann::json &module_body,
    std::set<std::string> &visiting) const;

  std::optional<typet> try_infer_bytes_param_size(
    const std::string &arg_name,
    const typet &arg_type,
    const symbol_id &id,
    size_t param_index) const;
 
  void validate_return_paths(
    const nlohmann::json &function_node,
    const code_typet &type,
    exprt &function_body);
 
  exprt compare_constants_internal(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs);
 
  exprt handle_indexed_comparison_internal(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs);
 
  exprt handle_type_mismatches(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs);
 
  typet
  any_attribute_type(const nlohmann::json &stmt, const std::string &attr_name);
  void get_attributes_from_self(
    const nlohmann::json &func_node,
    struct_typet &clazz);
 
  // Infer the static type of `class_name.attr_name` by scanning non-None
  // assignments to that attribute — both `self.attr = <rhs>` within the
  // class's own methods and `<var>.attr = <rhs>` at module scope where
  // `<var>` was assigned `class_name(...)`. Returns nil if no useful
  // information is found (caller falls back to any_type()).
  typet infer_attr_type_from_usage(
    const std::string &class_name,
    const std::string &attr_name);
 
  // The entry module, every imported module and the current one, each once.
  std::vector<const nlohmann::json *> reachable_module_bodies() const;
 
  // None when every write to an attribute named `attr_name` stores None, and
  // Optional[T] when they store None and literals of one scalar type T.
  // any_type() for any other write or a setattr call.
  typet none_attribute_type(const std::string &attr_name) const;
 
  bool held_by_reference(
    bool rhs_is_aliased_name,
    const std::string &attr_name,
    const typet &type,
    const std::string &annotated_type) const;
 
  // Attributes stored None that none_attribute_type could not type: those
  // whose every write is a plain store carry a None flag per instance, the
  // others are refused in arithmetic.
  mutable std::set<std::string> untyped_none_attributes_;
  mutable std::set<std::string> none_flagged_attributes_;
 
  void add_none_flag_component(
    struct_typet &clazz,
    const std::string &attr_name) const;
  exprt none_flag_of_attribute(const exprt &operand) const;
  void guard_none_attribute_operands(
    const std::string &op,
    const nlohmann::json &left,
    const nlohmann::json &right,
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &element);
  void set_none_flag(
    const exprt &lhs,
    const nlohmann::json &ast_node,
    codet &target_block) const;

  typet infer_tuple_struct_from_value(
    const nlohmann::json &value_node,
    const std::unordered_map<std::string, nlohmann::json> &param_annotations);
 
  exprt get_return_from_func(const char *func_symbol_id);
 
  void create_builtin_symbols();
 
  bool import_module_into_block(
    const nlohmann::json &import_node,
    module_locator &locator,
    code_blockt &code);
 
  bool import_one_module(
    const nlohmann::json &import_node,
    module_locator &locator,
    code_blockt &code);
 
  std::vector<const nlohmann::json *>
  import_nodes(std::deque<nlohmann::json> &submodules) const;
 
  std::string module_source_file(
    const std::string &module,
    const module_locator &locator) const;

  std::vector<nlohmann::json> submodule_imports(
    const nlohmann::json &import_node,
    const module_locator &locator) const;

  void register_import_alias(
    const nlohmann::json &import_node,
    const std::string &module_file);

  void convert_module_imports(code_blockt &all_imports_block);

  void convert_extra_translation_unit(
    const nlohmann::json &extra_ast,
    code_blockt &init_code,
    code_blockt &combined_user_code);
 
  nlohmann::json build_dunder_call(
    const nlohmann::json &object,
    const std::string &dunder_name,
    const nlohmann::json &args,
    const nlohmann::json &source_node) const;

  exprt store_call_result(
    exprt call_expr,
    const locationt &location,
    const std::string &temp_prefix,
    codet *block = nullptr);
 
  void process_module_imports(
    const nlohmann::json &module_ast,
    module_locator &locator,
    code_blockt &accumulated_code);

  void pre_collect_module_asts(
    const nlohmann::json &module_ast,
    module_locator &locator);
  void pre_collect_import(const nlohmann::json &node, module_locator &locator);
 
  symbolt *find_function_in_base_classes(
    const std::string &class_name,
    const std::string &symbol_id,
    std::string method_name,
    bool is_ctor) const;

  symbolt *find_function_in_imported_base_classes(
    const std::string &class_name,
    const std::string &method_name,
    bool is_ctor) const;

  std::pair<const nlohmann::json *, std::string>
  find_imported_class_module(const std::string &class_name) const;

  symbolt *find_method_in_imported_base(
    const nlohmann::json &base_class_node,
    const std::string &base_class,
    const std::string &method_name,
    bool is_ctor) const;

  symbolt *find_method_in_model_base(
    const std::string &base_class,
    const std::string &sym_id) const;

  const scope_bindings &module_bindings(const std::string &name) const;
  mutable std::
    map<std::pair<const nlohmann::json *, std::string>, scope_bindings>
      module_bindings_memo_;
  using mro_memo =
    std::map<std::string, std::optional<std::vector<std::string>>>;

  std::optional<std::vector<std::string>>
  class_mro(const std::string &class_name) const;
  std::optional<std::vector<std::string>>
  class_mro(const std::string &class_name, mro_memo &memo) const;
  static std::optional<std::vector<std::string>>
  c3_merge(std::vector<std::vector<std::string>> seqs);
  const nlohmann::json *sole_binding(
    const std::string &name,
    const std::string &statement = "ClassDef") const;
  const nlohmann::json *sole_method_def(
    const std::string &class_name,
    const std::string &method) const;
  bool overridden_below(
    const std::string &class_name,
    const std::string &method) const;

  struct attribute_functions
  {
    bool bound;
    std::vector<std::string> ids;
  };
  const attribute_functions *function_attribute(const std::string &attr);
  static bool same_signature(const code_typet &a, const code_typet &b);
  void collect_attribute_stores(
    const nlohmann::json &node,
    const std::string &owner,
    const nlohmann::json *method);
  void record_function_store(
    const std::string &attr,
    const std::pair<bool, std::string> &stored);
  std::set<std::string> subclasses(const std::string &class_name) const;
  std::optional<std::pair<bool, std::string>> stored_function(
    const nlohmann::json &target,
    const nlohmann::json &value,
    const std::string &owner,
    const nlohmann::json *method) const;
  std::optional<std::string>
  bound_method_id(const std::string &owner, const std::string &m) const;
  bool try_bound_method_store(const nlohmann::json &ast_node, codet &block);
  bool try_dedicated_assign(const nlohmann::json &ast_node, codet &block);
  bool try_numpy_nditer_assign(const nlohmann::json &ast_node);
  const nlohmann::json *
  numpy_slice_copy_source(const nlohmann::json &value) const;
  bool try_numpy_slice_copy_assign(const nlohmann::json &ast_node);
  std::optional<exprt> get_intercepted_expr(const nlohmann::json &element);
  void reject_bound_method_read(const nlohmann::json &element);
  exprt get_class_dunder_attribute(const nlohmann::json &element);
  exprt get_class_attribute(const nlohmann::json &element);
  exprt get_class_name(const nlohmann::json &value);
  exprt
  get_module_member(const std::string &var_name, const nlohmann::json &element);
  void reject_method_value(const std::string &class_name, const std::string &m)
    const;
  std::map<
    const nlohmann::json *,
    std::optional<std::map<std::string, std::optional<attribute_functions>>>>
    attribute_functions_;
  bool class_binds_name(const std::string &class_name, const std::string &name)
    const;
 
  symbolt *find_imported_symbol(const std::string &symbol_id) const;
  symbolt *find_symbol_through_module(const std::string &sym_id) const;
  symbolt *find_nested_function_symbol(const std::string &name) const;
  symbolt *find_symbol_in_global_scope(const std::string &symbol_id) const;
  symbolt *find_model_symbol(const std::string &sym_id) const;
  void collect_model_namespaces();
  void build_models_block(code_blockt &models_block, bool models_precompiled);
 
  void copy_instance_attributes(
    const std::string &src_obj_id,
    const std::string &target_obj_id);
 
  void update_instance_from_self(
    const std::string &class_name,
    const std::string &func_name,
    const std::string &obj_symbol_id);
 
  void refuse_misaligned_self_calls() const;
  void refuse_misaligned_self_call(
    const code_function_callt &call,
    const namespacet &ns) const;
 
  size_t get_type_size(const nlohmann::json &ast_node);
 
  void append_models_from_directory(
    std::list<std::string> &file_list,
    const std::string &dir_path);
 
  typet nullable_dict_pointee(const typet &t) const;
  bool keeps_pointer_type_on_none(const typet &t);
  void guard_none_container(
    exprt &rhs,
    typet &rhs_type,
    const nlohmann::json &element);
  void guard_none_typed_container(
    const std::string &op,
    exprt &rhs,
    const nlohmann::json &element);
  exprt handle_membership_operator(
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &element,
    bool invert);
  exprt range_membership(const exprt &x, const nlohmann::json &element);
  exprt
  list_or_range_contains(exprt &lhs, exprt &rhs, const nlohmann::json &element);

  typet get_union_type_from_annotation(
    const nlohmann::json &annotation_node,
    const nlohmann::json &element);
 
  typet narrow_union_to_member(const std::string &member_name);
 
  std::string extract_non_none_type(const nlohmann::json &annotation_node);
 
  void
  get_delete_statement(const nlohmann::json &ast_node, codet &target_block);
 
  // =========================================================================
  // Helper methods for get_var_assign
  // =========================================================================
 
  std::pair<std::string, typet>
  extract_type_info(const nlohmann::json &ast_node);

  void upgrade_param_type_from_default(
    code_typet::argumentt &param_arg,
    const exprt &default_expr);

  void refine_any_param_to_list(
    code_typet::argumentt &param_arg,
    const nlohmann::json &body,
    const std::string &func_name,
    size_t param_index);

  bool param_is_list_like(
    const std::string &param_name,
    const nlohmann::json &body,
    const std::string &func_name,
    size_t param_index,
    typet &elem_type) const;
 
  bool called_only_with_flat_list_displays(
    const std::string &func_name,
    size_t param_index) const;

  void refine_any_param_from_elements(
    code_typet::argumentt &param_arg,
    const std::string &func_name,
    size_t param_index);

  void seed_list_param_element_type(
    const nlohmann::json &element,
    const symbol_id &id,
    const std::string &arg_id,
    size_t param_index);

  bool seed_mixed_call_site_elements(
    const std::string &param_id,
    const std::string &func_name,
    size_t param_index);
  bool infer_list_elem_type_from_call_sites(
    const std::string &func_name,
    size_t param_index,
    typet &out) const;
  bool param_keeps_positions(
    const std::string &func_name,
    size_t param_index,
    bool any_index = false) const;
  bool param_elements(
    const nlohmann::json &arg,
    const std::string &enclosing_function,
    std::vector<nlohmann::json> &out,
    bool &direct,
    unsigned depth) const;
  bool call_site_list_literals(
    const std::string &func_name,
    size_t param_index,
    std::vector<nlohmann::json> &out,
    bool &direct,
    unsigned depth) const;
  bool literal_element_kinds(
    const std::vector<nlohmann::json> &literals,
    std::vector<std::vector<typet>> &kinds) const;
  bool record_literal_positions(
    const std::string &id,
    const std::vector<nlohmann::json> &literals,
    const std::vector<typet> &kinds);
  bool record_literal_elements(
    const std::string &id,
    const std::vector<nlohmann::json> &literals,
    bool positional);
  bool mixes_str_and_number(
    const std::string &probe,
    const std::vector<typet> &kinds);
 
  void handle_array_unpacking(
    const nlohmann::json &ast_node,
    const nlohmann::json &target,
    exprt &rhs,
    codet &target_block);

  bool
  try_tagged_var_assign(const nlohmann::json &ast_node, codet &target_block);

  bool module_scope_rhs_needs_type_probe(const nlohmann::json &ast_node);

  symbolt *mint_retyped_symbol(
    const symbolt &orig,
    const std::string &alias_key,
    const typet &new_type,
    const locationt &location,
    const symbol_id &sid,
    codet &target_block);
 
  void handle_list_literal_unpacking(
    const nlohmann::json &ast_node,
    const nlohmann::json &target,
    codet &target_block);
 
  void set_assigned_value(symbolt &symbol, const exprt &rhs);
  void retype_resized_str(symbolt &symbol, exprt &lhs, exprt &rhs);
  bool store_optional_str(symbolt *lhs_symbol, const exprt &lhs, exprt &rhs);

  bool annotation_yields_to_rhs(
    const nlohmann::json &ast_node,
    const exprt &rhs) const;
 
  void handle_assignment_type_adjustments(
    symbolt *lhs_symbol,
    exprt &lhs,
    exprt &rhs,
    const std::string &lhs_type,
    const nlohmann::json &ast_node,
    bool is_ctor_call);
 
  std::string element_kind(const std::string &id) const;
  bool element_kinds_differ(const std::string &a, const std::string &b) const;
  void propagate_list_type_info(
    const exprt &lhs,
    const exprt &rhs,
    symbolt *lhs_symbol);

  void propagate_dict_member_list_type_info(
    const exprt &rhs,
    const std::string &lhs_identifier);
 
  // =========================================================================
  // Dictionary assignment helper methods
  // =========================================================================

  exprt get_rhs_with_dict_resolution(
    const nlohmann::json &ast_node,
    const typet &target_type);
 
  // =========================================================================
  // Type inference helper methods
  // =========================================================================

  std::string infer_type_from_any_annotation(
    const nlohmann::json &ast_node,
    const std::string &lhs_type);

  typet resolve_any_subscript_array_type(
    const nlohmann::json &ast_node,
    const typet &current_type);
 
  typet resolve_call_argument_array_type(
    const nlohmann::json &ast_node,
    const typet &current_type);

  typet resolve_numpy_reducer_call_array_type(
    const nlohmann::json &ast_node,
    const typet &current_type);

  const code_typet *
  lambda_call_callee(const nlohmann::json &call, const symbolt &var);
  typet resolve_lambda_call_result_type(
    const nlohmann::json &ast_node,
    const typet &current_type);
  // The array type of element-wise arithmetic the annotator typed as a list.
  typet resolve_numpy_arithmetic_type(
    const nlohmann::json &ast_node,
    const exprt &rhs,
    const typet &current_type) const;
 
  std::string resolve_name_symbol_id(const std::string &name) const;
  exprt
  once_bound_exponent(const nlohmann::json &right, const exprt &rhs) const;
  symbolt *find_enclosing_scope_symbol(symbol_id sid) const;
  symbolt *find_global_symbol(const symbol_id &sid);
  bool global_has_type(const std::string &name, const std::string &type) const;
  exprt
  module_function_expr(const std::string &name, const nlohmann::json &element);
  void track_unbound_global(
    const std::string &id,
    const nlohmann::json &binding,
    const typet &type);
  void guard_unbound_global(
    const std::string &id,
    const std::string &name,
    const nlohmann::json &element);
  void mark_global_bound(const nlohmann::json &stmt, code_blockt &block);
  typet forward_function_return_type(const std::string &name, const exprt &fn);
  exprt get_default_expr(const nlohmann::json &node);
 
  std::string root_name_from_subscript(const nlohmann::json &node) const;
 
  bool is_basic_numpy_view_subscript(const nlohmann::json &node) const;
 
  // is_basic_numpy_view_subscript(), excluding `.shape[i]`: that indexes the
  // plain int tuple `.shape` returns, never the array's own data, so it must
  // never be tracked as a numpy view/alias (root_name_from_subscript drills
  // through any Attribute to its base Name, so without this exclusion
  // `shape_0 = a.shape[0]` would register shape_0 as a view copy of `a`
  // itself). A wrapper, not a change to is_basic_numpy_view_subscript
  // itself, to keep that already-large function's own decision count as-is.
  bool is_tracked_numpy_view_subscript(const nlohmann::json &node) const;
 
  // True for a transpose()/reshape()/ravel()/diagonal() Attribute-call node
  // (module or method form), independent of whether its root array name can
  // be resolved. Shared by is_numpy_view_copy_expr and
  // root_name_from_numpy_view_copy_expr so the view_functions set and the
  // Call/Attribute shape check live in one place.
  bool is_numpy_view_copy_call_node(const nlohmann::json &node) const;
 
  bool is_numpy_array_constructor_expr(const nlohmann::json &node) const;
 
  // The last direct assignment to `name` in `block[0..end)`, following into
  // both arms of a trailing if/else (nullptr unless both arms agree it's a
  // numpy array constructor call). Shared by block_assigns_numpy_array_to
  // and reject_incompatible_numpy_local_return_branches so both walk the
  // same "what did this name last bind to" search -- one only needs to know
  // whether it resolved, the other needs the value node itself to compare
  // shapes between branches.
  const nlohmann::json *find_numpy_ctor_value_assigned_to(
    const nlohmann::json &block,
    std::size_t end,
    const std::string &name) const;
 
  // True when `block[0..end)` ends (directly, or through both arms of a
  // trailing if/else) in an assignment binding `name` from a numpy array
  // constructor call. Shared by local_var_numpy_array_return's straight-line
  // and branching cases so both walk the same "what did this name last bind
  // to" search.
  bool block_assigns_numpy_array_to(
    const nlohmann::json &block,
    std::size_t end,
    const std::string &name) const;
 
  // True when `func_def`'s only top-level statement is `return <Name>`, and
  // that Name was last bound (directly, or identically on both arms of an
  // if/else) by a numpy array constructor call. get_function_definition
  // checks this before its own return-type dispatch: the static annotator's
  // pre-pass already resolved such a Name's own `np.zeros(...)`-shaped
  // assignment through the numpy operational model's declared signature
  // (`list[float]`) and wrote that bogus annotation into
  // `function_node["returns"]` ahead of real conversion -- locking the
  // function's return type to a generic PyListObject* before the body (which
  // actually returns a concrete array) is ever converted. A direct
  // `return np.zeros(...)` never hits this: static inference only chases a
  // Name-based callee, not np.zeros's Attribute-based one, so it leaves the
  // return type empty and the existing GOTO-scan fallback already types it
  // correctly. Treating the local-var case the same way here (by having the
  // caller skip the annotation-driven dispatch entirely) reaches that same
  // already-correct fallback instead of duplicating it.
  bool local_var_numpy_array_return(const nlohmann::json &func_def) const;
  // `return np.array(...) * 2`: the annotator types element-wise arithmetic
  // over a constructor as a list, so it takes the same fallback.
  bool numpy_arithmetic_return(const nlohmann::json &func_def) const;
  bool is_numpy_param_operand(
    const nlohmann::json &node,
    const nlohmann::json &func_def) const;
  bool is_numpy_arithmetic_node(
    const nlohmann::json &node,
    const nlohmann::json &func_def) const;
  bool is_numpy_arithmetic_value(
    const nlohmann::json &node,
    const nlohmann::json &func_def) const;
  bool is_numpy_arithmetic_binding(
    const nlohmann::json &node,
    const nlohmann::json &func_def) const;
  bool call_passes_numpy_array(const nlohmann::json &call_node) const;
 
  // The `returns` node get_function_definition's own dispatch should use:
  // null when local_var_numpy_array_return applies, function_node["returns"]
  // otherwise. Split out to keep the ternary this needs out of
  // get_function_definition's own decision count.
  const nlohmann::json &
  resolve_return_annotation_node(const nlohmann::json &function_node) const;
 
  // Throws an explicit TypeError when local_var_numpy_array_return's
  // trailing if/else binds the returned name from a numpy array constructor
  // call with a different literal shape argument on each arm -- e.g.
  // np.zeros(3) on one branch, np.zeros((2, 2)) on the other. Left
  // unchecked, converting the branch merge with two different concrete
  // array types crashes value_sett::assign's type-compatibility assertion
  // instead of rejecting cleanly (ADR-NP principle 3).
  void reject_incompatible_numpy_local_return_branches(
    const nlohmann::json &func_def) const;
 
  // True when `func_name`'s own body reads `param_name`'s `.shape`/`.ndim`/
  // `.size`/`.T`, or passes it to `numpy.transpose`/`numpy.sort`/
  // `numpy.argsort`, *and* some call site feeds the `param_index`-th
  // argument from a module-level numpy array constructor call whose shape
  // argument is not a literal (e.g. `np.ones(n)` for a variable `n`).
  // register_function_argument uses this to reject such a parameter with an
  // explicit diagnostic instead of leaving it untyped, which previously
  // surfaced as a generic runtime AttributeError the first time the callee
  // touched one of those. Deliberately excludes `len()`, which already
  // resolves soundly for a symbolic-shape parameter through a different
  // path.
  bool numpy_param_call_site_has_symbolic_shape(
    const std::string &func_name,
    size_t param_index,
    const std::string &param_name) const;
 
  // Every `Call` node in the AST, computed once and reused:
  // register_function_argument calls numpy_param_call_site_has_symbolic_shape
  // once per parameter, and each call previously re-walked the entire AST from
  // scratch.
  const std::vector<numpy_param_call_site> &numpy_call_sites() const;
  mutable std::vector<numpy_param_call_site> numpy_call_sites_cache_;
  mutable bool numpy_call_sites_cached_ = false;
 
  // True when some top-level statement in `module_body` binds `arg_name` to
  // a numpy array constructor call with a non-literal shape. Split out of
  // numpy_param_call_site_has_symbolic_shape to keep that function's own
  // decision count down.
  bool module_level_symbolic_ctor_binding(
    const nlohmann::json &module_body,
    const std::string &arg_name) const;
 
  // Throws when `numpy_array_param` is false and some call site feeds this
  // parameter from a numpy array constructor call with a non-literal shape.
  // Split out of register_function_argument to keep the `if` this check
  // needs out of that function's own decision count.
  void reject_if_symbolic_shape_param(
    bool numpy_array_param,
    const typet &arg_type,
    const std::string &func_name,
    size_t param_index,
    const std::string &arg_name) const;
 
  // `y = identity(x)`/`y = make()`: a call to a locally-defined function that
  // itself returns a numpy array is never an is_numpy_array_constructor_expr
  // (that only recognises a literal `np.<ctor>(...)` shape). lhs's own type
  // already reflects the array-return fix by the time update_numpy_array_
  // binding runs, so trust it instead of duplicating that resolution here.
  // Split out of update_numpy_array_binding to keep its own decision count
  // from growing further.
  bool is_numpy_arithmetic_result(
    const nlohmann::json &rhs_node,
    const exprt &lhs) const;
  bool is_array_returning_call_expr(
    const nlohmann::json &rhs_node,
    const exprt &lhs) const;
 
  bool is_numpy_view_copy_expr(const nlohmann::json &node) const;
 
  std::string
  root_name_from_numpy_view_copy_expr(const nlohmann::json &node) const;
 
  bool contains_tracked_numpy_view_name(const nlohmann::json &node);
 
  bool is_tracked_numpy_view_name_node(const nlohmann::json &node);
 
  bool is_basic_numpy_view_subscript_escape(const nlohmann::json &node);
  exprt probe_expr(const nlohmann::json &node);
  std::optional<typet>
  literal_numpy_array_type(const nlohmann::json &call) const;
  nlohmann::json bind_numpy_constructor_argument(const nlohmann::json &arg);
 
  bool contains_tracked_numpy_view_object(const nlohmann::json &node);
 
  void reject_numpy_view_mutating_method_call(const nlohmann::json &node);

  std::string numpy_view_storage_root(const std::string &id) const;
  bool is_numpy_storage_escaped(const nlohmann::json &name) const;
  bool is_closed_return_expression(
    const nlohmann::json &value,
    const nlohmann::json &params) const;
  std::optional<nlohmann::json>
  simple_call_return_value(const nlohmann::json &call) const;
  std::optional<nlohmann::json>
  fold_numpy_view_call(const nlohmann::json &call);
  void
  get_folded_var_assign(const nlohmann::json &ast_node, codet &target_block);
  void reject_or_defer_numpy_view_return(
    const nlohmann::json &ast_node,
    codet &target_block);
  bool bind_numpy_pointer_view_alias(
    const exprt &lhs,
    const std::string &lhs_id,
    const std::string &rhs_id);
  void reject_multi_path_numpy_view_return(const nlohmann::json &call);
  bool numpy_subscript_yields_view(const nlohmann::json &node) const;
  bool holds_numpy_view(const nlohmann::json &node) const;
  bool is_numpy_module_call(const nlohmann::json &node) const;
  bool is_numpy_view_value(const nlohmann::json &node) const;
  void reject_numpy_view_comprehension(const nlohmann::json &node) const;
  void check_numpy_view_statement(const nlohmann::json &statement) const;
  void reject_unfoldable_numpy_view_call(const nlohmann::json &call);
  bool reject_or_defer_numpy_view_name_return(
    const nlohmann::json &ast_node,
    codet &target_block);
  nlohmann::json current_user_function_node() const;
  bool is_numpy_module_param(const std::string &root_name) const;
  bool is_copied_numpy_view_local(const std::string &name) const;
  bool is_scalar_read_of_numpy_view_param(
    const exprt &lhs,
    const std::string &storage_id) const;
  code_blockt *while_condition_block(
    const nlohmann::json &ast_node,
    code_blockt &cond_prelude);
  void reject_live_numpy_view_copies_of(const nlohmann::json &args);
  bool passes_numpy_view(const nlohmann::json &arg);
  bool is_scalar_numpy_view_call(const nlohmann::json &call);
  bool passes_unnamed_numpy_view_argument(const nlohmann::json &call);
  bool contains_unnamed_numpy_view_argument(const nlohmann::json &node);
  const nlohmann::json &hoist_unnamed_numpy_view_arguments(
    const nlohmann::json &statement,
    nlohmann::json &rewritten,
    codet &target_block);
  nlohmann::json bind_numpy_view_temporary(
    const nlohmann::json &statement,
    const nlohmann::json &value,
    const std::string &prefix,
    codet &target_block);
  bool hoist_numpy_view_arguments(
    const std::string &key,
    nlohmann::json &rewritten,
    codet &target_block);
  bool needs_numpy_view_call_binding(const nlohmann::json &node);
  std::string numpy_view_callee_name(const symbol_id &function) const;
  std::optional<std::pair<std::string, std::size_t>>
  numpy_view_method_callee(const nlohmann::json &call) const;
  bool binds_every_numpy_view_argument(const nlohmann::json &call);
  bool names_python_builtin(const std::string &name) const;
  bool consumes_numpy_view_as_list(const nlohmann::json &node) const;
  bool is_builtin_over_numpy_view(const nlohmann::json &node) const;
  symbolt *find_symbol_in_import(
    const nlohmann::json &obj,
    const std::string &symbol_id,
    const std::string &lookup_name) const;
  symbolt *find_symbol_in_module(
    const std::string &symbol_id,
    const std::string &module_file,
    const std::string &lookup_name,
    const std::string &name) const;
  bool import_hides_builtin(
    const nlohmann::json &import,
    const std::string &symbol_id,
    const std::string &name) const;
  bool needs_fresh_retype_slot(
    const exprt &lhs,
    const exprt &rhs,
    const std::string &lhs_id) const;
  bool is_numpy_array_to_view_rebind(
    const exprt &lhs,
    const exprt &rhs,
    const std::string &lhs_id) const;
  std::string pointee_class(const typet &type) const;
  void retype_for_class_rebind(
    const nlohmann::json &target,
    const nlohmann::json &ast_node,
    bool is_ctor_call,
    const symbol_id &sid,
    const locationt &location,
    symbolt *&lhs_symbol,
    exprt &lhs,
    codet &target_block);
  void
  reject_numpy_array_retype(const symbolt &symbol, const typet &type) const;
  bool needs_fresh_numpy_array_slot(
    const exprt &lhs,
    const exprt &rhs,
    const std::string &lhs_id) const;
  bool is_numpy_array_reshape_rebind(
    const exprt &lhs,
    const exprt &rhs,
    const std::string &lhs_id) const;
  bool passes_numpy_view_anywhere(const nlohmann::json &call);
  bool is_handled_numpy_view_call(const nlohmann::json &call);
  bool is_attribute_store_of_numpy_view(
    const nlohmann::json &target,
    const nlohmann::json &value);
  bool call_needs_view_argument_hoist(const nlohmann::json &call);
  bool takes_numpy_view_argument(const nlohmann::json &call, std::size_t index);
  bool is_rank1_numpy_view(const nlohmann::json &node) const;
  bool is_rank1_numpy_array_name(const nlohmann::json &node) const;
  void reject_builtin_over_complex_array(const nlohmann::json &node) const;
  bool is_foldable_constant_index(const exprt &expr) const;
  bool adapt_numpy_view_builtin_arguments(nlohmann::json &node);
  std::optional<nlohmann::json>
  inline_numpy_view_lambda_call(const nlohmann::json &call);
  bool is_inlined_numpy_view_lambda(const nlohmann::json &statement);
  std::optional<bool> bind_lambda_arguments(
    const nlohmann::json &signature,
    const nlohmann::json &args,
    std::map<std::string, nlohmann::json> &values) const;
  std::set<std::string> numpy_inlined_lambdas_;
  const nlohmann::json &adapt_numpy_view_builtin_calls(
    const nlohmann::json &statement,
    nlohmann::json &rewritten);
  bool split_conditional_numpy_view_assignment(
    const nlohmann::json &statement,
    nlohmann::json &rewritten);
  bool needs_numpy_view_hoist(const nlohmann::json &node);
  bool freeze_numpy_view_operand(
    const nlohmann::json::json_pointer &path,
    nlohmann::json &rewritten,
    codet &target_block);
  bool hoist_first_evaluated_numpy_view_call(
    const nlohmann::json::json_pointer &path,
    bool skip,
    nlohmann::json &rewritten,
    codet &target_block);
  std::size_t numpy_view_arg_count_ = 0;
  bool returns_bound_numpy_view_param(const nlohmann::json &func_node);
  const nlohmann::json *
  returned_numpy_view_argument(const nlohmann::json &call);
  bool try_bind_returned_numpy_view_param(
    const nlohmann::json &ast_node,
    codet &target_block);
  const nlohmann::json *numpy_discarded_call_ = nullptr;
  void reject_numpy_view_argument_use(const nlohmann::json &call);
  void reject_numpy_view_method_call(const nlohmann::json &func) const;
  void reject_numpy_view_callee(const nlohmann::json &call);
  void reject_inline_runtime_numpy_slice(const nlohmann::json &call) const;
  void reject_numpy_view_container_store(const nlohmann::json &ast_node);
  bool is_numpy_view_syntax(
    const nlohmann::json &value,
    const std::string &scope,
    std::size_t depth) const;
  bool is_numpy_storage_syntax(
    const nlohmann::json &value,
    const std::string &scope,
    std::size_t depth) const;
  bool is_fold_only_numpy_function(const nlohmann::json &function_node);
  void get_unfolded_function_definition(const nlohmann::json &function_node);
  void track_numpy_view_call_escape(const nlohmann::json &call);
  void reject_escaped_numpy_view_read(const nlohmann::json &node) const;
  void reject_escaped_numpy_view_write(const nlohmann::json &target) const;
  void reject_escaped_numpy_view_use(const nlohmann::json &statement) const;
 
  void reject_numpy_view_identity_query(const nlohmann::json &node);
 
  void reject_copied_numpy_view_in_container(
    const nlohmann::json &ast_node,
    const std::set<std::string> &container_types);
 
  nlohmann::json
  get_ravel_receiver_node(const nlohmann::json &ravel_call) const;
  bool is_numpy_ravel_receiver(const nlohmann::json &ravel_call) const;
  nlohmann::json
  flat_subscript_receiver_node(const nlohmann::json &subscript_node) const;
  bool try_handle_flat_index_assignment(
    const nlohmann::json &ast_node,
    const nlohmann::json &target,
    codet &target_block);
  std::optional<exprt> try_build_flat_index_read(const nlohmann::json &element);
 
  // ExpressionType::SUBSCRIPT's handler, split out of get_expr into its own
  // function plus these sub-dispatch helpers -- each phase of a[...]'s
  // handling (base resolution, dict/tuple pointer unwrap, and one dispatch
  // per index shape: tuple, dict, bool-mask-rows, multi-axis tuple, fancy
  // list, bool-mask variable, __getitem__) is independently a return early
  // or fall-through step, so extracting them keeps every one individually
  // simple instead of one function accumulating get_expr's own decision
  // count as ADR-NP-003 etapa 2 adds more index shapes.
  exprt handle_subscript_expr(const nlohmann::json &element);
  std::optional<exprt>
  resolve_subscript_base(const nlohmann::json &element, exprt &array);
  std::optional<exprt> try_fold_constant_string_slice(
    const nlohmann::json &element,
    const exprt &array);
  void unwrap_subscript_base_types(
    exprt &array,
    typet &array_type,
    typet &array_type_for_dict,
    bool &array_is_dict_pointer,
    const nlohmann::json &element);
  std::optional<exprt> try_dispatch_tuple_subscript(
    const exprt &array,
    const typet &array_type,
    const nlohmann::json &slice,
    const nlohmann::json &element);
  std::optional<exprt> try_dispatch_dict_subscript(
    exprt &array,
    const typet &array_type_for_dict,
    bool array_is_dict_pointer,
    const nlohmann::json &element);
  bool subscript_targets_list_model(
    const typet &array_type,
    const typet &list_type) const;
  std::optional<exprt> try_dispatch_multidim_tuple_index(
    const exprt &array,
    const typet &array_type,
    const nlohmann::json &slice,
    const nlohmann::json &element,
    bool tuple_index_targets_list_model,
    const typet &list_type);
  std::optional<exprt> try_dispatch_multidim_tuple_axes(
    const exprt &array,
    const nlohmann::json &element,
    const std::vector<nlohmann::json> &idx_nodes);
  std::optional<exprt> try_dispatch_chained_axis_index(
    const exprt &array,
    const nlohmann::json &element,
    const std::vector<nlohmann::json> &idx_nodes,
    const typet &list_type);
  std::optional<exprt> try_dispatch_fancy_list_index(
    const exprt &array,
    const nlohmann::json &slice,
    const nlohmann::json &element,
    bool tuple_index_targets_list_model);
  std::optional<exprt> try_dispatch_bool_mask_variable_index(
    const exprt &array,
    const typet &array_type,
    const nlohmann::json &slice,
    const nlohmann::json &element,
    bool tuple_index_targets_list_model);
  std::optional<exprt> try_dispatch_fancy_index_via_list_variable(
    const exprt &array,
    const nlohmann::json &slice,
    const nlohmann::json &element);
  std::optional<exprt> try_dispatch_dunder_getitem(
    const nlohmann::json &element,
    const nlohmann::json &slice);
  void reject_scalar_subscript(
    const typet &array_type,
    const nlohmann::json &element) const;
 
  std::optional<nlohmann::json>
  select_return_value_for_call(const nlohmann::json &call_node) const;
 
  nlohmann::json substitute_call_arguments(
    const nlohmann::json &node,
    const nlohmann::json &call_node) const;
 
  bool return_value_uses_call_argument(
    const nlohmann::json &return_value,
    const nlohmann::json &call_node) const;
 
  // return <call>(<param>, ...), e.g. `def transposed(a): return
  // np.transpose(a)`: true when every Name the call expression references is
  // either one of `params` or an imported module alias. Split out of
  // return_value_uses_call_argument to keep that function's own decision
  // count down.
  bool return_call_only_references_params_or_modules(
    const nlohmann::json &return_value,
    const nlohmann::json &params) const;
 
  void reject_unsafe_numpy_view_target(const nlohmann::json &target);
  void reject_unsafe_numpy_view_write_to(const std::string &root_id);
 
  void reject_numpy_view_slice_assignment(const nlohmann::json &target);

  bool reject_immutable_item_assignment(
    const typet &container_type,
    codet &target_block);
 
  void record_numpy_view_copy(const exprt &lhs, const nlohmann::json &rhs_node);
  std::string numpy_view_source_of(const std::string &storage_id) const;
 
  bool is_tracked_numpy_view_id(const std::string &symbol_id) const;
 
  void reject_nonconstant_numpy_view_write(const nlohmann::json &target) const;
 
  std::optional<std::vector<nlohmann::json>>
  build_numpy_nditer_logical_elements(const nlohmann::json &arg) const;
 
  std::optional<std::pair<std::vector<std::size_t>, std::vector<exprt>>>
  build_numpy_descriptor_materialized_elements(
    const nlohmann::json &arg,
    const std::string &unsupported_rank_error);
 
  std::optional<std::vector<std::size_t>>
  get_empty_numpy_literal_slice_shape(const nlohmann::json &arg) const;
 
  std::optional<exprt> build_numpy_descriptor_materialized_list(
    const nlohmann::json &arg,
    bool nested);

  bool numpy_result_is_fresh_copy_ = false;
  bool numpy_result_is_view_ = false;

  bool is_numpy_param_slice(const nlohmann::json &subscript) const;

  exprt hoist_numpy_element(const exprt &element);

  exprt materialize_numpy_elements(
    const nlohmann::json &location_node,
    const std::vector<std::size_t> &shape,
    const std::vector<exprt> &elems,
    const typet &elem_type);

  std::optional<exprt> build_numpy_descriptor_materialized_array(
    const nlohmann::json &arg,
    const std::vector<std::size_t> *reshape_to = nullptr);
 
  std::optional<std::vector<std::size_t>>
  get_numpy_nditer_logical_shape(const std::string &root_id) const;
 
  std::optional<typet>
  get_numpy_descriptor_element_type(const std::string &root_id) const;
 
  bool is_numpy_readonly_view_arg(const nlohmann::json &arg) const;
 
  void clear_numpy_view_copy(const exprt &lhs);
 
  void
  update_numpy_array_binding(const exprt &lhs, const nlohmann::json &rhs_node);
 
  bool update_numpy_array_binding_from_name(
    const exprt &lhs,
    const std::string &lhs_id,
    const nlohmann::json &rhs_node,
    bool unconditional_assignment);
 
  bool preserve_conditional_numpy_alias_shape(
    const std::string &lhs_id,
    const std::string &rhs_id,
    bool unconditional_assignment);
 
  void copy_numpy_alias_shape_state(
    const std::string &lhs_id,
    const std::string &rhs_id);
 
  void reject_conditional_numpy_alias_rebind(
    const exprt &lhs,
    const nlohmann::json &rhs_node) const;
 
  bool record_numpy_view_copy_from_returned_argument(
    const exprt &lhs,
    const std::string &lhs_id,
    const nlohmann::json &rhs_node);
 
  void clear_numpy_array_storage_aliases_for(const std::string &symbol_id);
 
  void bind_numpy_array_storage_alias(
    const std::string &lhs_id,
    const std::string &rhs_id);
 
  symbolt *resolve_numpy_array_storage_alias(symbolt *symbol) const;
 
  std::string
  resolve_numpy_array_storage_alias_id(const std::string &symbol_id) const;

  std::vector<std::string> numpy_views_of(const std::string &rebound_id) const;
 
  bool keep_numpy_result_view(const std::string &lhs_id);
  bool is_readonly_numpy_view_expr(const nlohmann::json &node) const;
 
  void record_numpy_constructor_binding(
    const exprt &lhs,
    const std::string &lhs_id,
    const nlohmann::json &rhs_node,
    bool unconditional_assignment);
 
  void detach_numpy_pointer_views_of(
    const std::string &rebound_id,
    const locationt &location,
    codet &target_block);

  void detach_numpy_pointer_view(
    const std::string &view_id,
    const locationt &location,
    codet &target_block);

  void share_numpy_storage_snapshot(
    const std::string &storage_id,
    const std::vector<std::string> &view_ids,
    const locationt &location,
    codet &target_block,
    const std::string &heir_id = "");
  std::vector<std::string>
  numpy_storage_aliases_of(const std::string &rebound_id) const;
  std::string hand_numpy_storage_to_alias(
    const std::string &rebound_id,
    const locationt &location,
    codet &target_block);
 
  bool should_rebuild_cached_numpy_row_subscript_rhs(
    const nlohmann::json &rhs_node) const;
 
  bool is_tracked_2d_numpy_array_symbol(const std::string &source_id) const;
 
  std::optional<nlohmann::json>
  rewrite_numpy_method_call_node(const nlohmann::json &call_node) const;
  bool is_numpy_subscript_reducer_receiver(
    const nlohmann::json &method_base,
    const std::string &method_name) const;
 
  // get_var_assign's RHS preprocessing step: rewrites `a.T` into
  // `np.transpose(a)` (numpy's own Attribute-shaped transpose sugar, with
  // no method-call node to reach rewrite_numpy_method_call_node through),
  // or else defers to rewrite_numpy_method_call_node for any other numpy
  // method-call RHS. Split out to keep get_var_assign's own decision count
  // from growing as more special-cased RHS rewrites land there.
  nlohmann::json rewrite_assign_rhs_node(const nlohmann::json &ast_node) const;
  nlohmann::json numpy_transpose_base(const nlohmann::json &node) const;
 
  // Classifies a Call node as a numpy method call: (is_a_method_call,
  // method_name, method_base, is_a_supported_copy_method,
  // is_a_supported_dispatch_rewrite_method). Split out of
  // rewrite_numpy_method_call_node() to keep that function's own decision
  // count low.
  std::tuple<bool, std::string, nlohmann::json, bool, bool>
  classify_numpy_method_call(const nlohmann::json &call_node) const;
 
  bool
  method_base_is_imported_module(const std::string &method_base_name) const;
 
  bool
  method_base_is_tracked_numpy_array(const std::string &method_base_name) const;
 
  // Builds the np.<method_name>(method_base, ...original args...) rewrite of
  // a recognized numpy method call.
  nlohmann::json build_numpy_method_rewrite_node(
    const nlohmann::json &call_node,
    const std::string &method_name,
    const nlohmann::json &method_base) const;
 
  // =========================================================================
  // Unpacking helper methods
  // =========================================================================

  bool handle_unpacking_assignment(
    const nlohmann::json &ast_node,
    const nlohmann::json &target,
    codet &target_block);
 
  bool unpack_record_is_trusted(const nlohmann::json &value) const;

  void unpack_nested_target(
    const nlohmann::json &ast_node,
    const nlohmann::json &target,
    const exprt &value,
    codet &target_block);
 
  exprt hold_tuple_member_list(
    const nlohmann::json &ast_node,
    const exprt &value,
    codet &target_block);

  void desugar_unpacking_with_lvalue_targets(
    const nlohmann::json &ast_node,
    const nlohmann::json &target,
    codet &target_block);
 
  // =========================================================================
  // Symbol creation helper methods
  // =========================================================================

  symbolt *create_symbol_for_unannotated_assign(
    const nlohmann::json &ast_node,
    const nlohmann::json &target,
    const symbol_id &sid,
    bool is_global);

  bool is_global_variable(const symbol_id &sid) const;

  void declare_nonlocal(const nlohmann::json &element);

  void redirect_nonlocal(symbol_id &sid) const;

  std::string extract_target_name(const nlohmann::json &target) const;
 
  // =========================================================================
  // RHS processing helper methods
  // =========================================================================

  static const nlohmann::json *
  reordering_builtin_arg(const nlohmann::json &ast_node);
 
  void copy_elem_types_from_reordering_builtin(
    const nlohmann::json &ast_node,
    const std::string &lhs_id);

  std::string user_class_of(const typet &type);
  void reject_attribute_added_on_some_paths(
    const std::string &receiver,
    const std::string &class_name,
    const std::string &attr) const;
  void reject_attribute_scalar_change(const exprt &lhs, const exprt &rhs);
  void reject_attribute_class_change(
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &ast_node,
    bool is_ctor_call);
  void widen_int_target_for_float_call(
    exprt &lhs,
    const exprt &rhs,
    bool is_ctor_call);
  void handle_function_call_rhs(
    const nlohmann::json &ast_node,
    symbolt *lhs_symbol,
    exprt &lhs,
    exprt &rhs,
    const locationt &location,
    bool is_ctor_call,
    codet &target_block);
 
  void wrap_call_result_in_optional(
    const nlohmann::json &ast_node,
    const exprt &lhs,
    exprt &rhs,
    const locationt &location,
    codet &target_block);

  exprt handle_string_literal_rhs(
    const nlohmann::json &ast_node,
    const std::string &lhs_type,
    const exprt &rhs);
 
  // =========================================================================
  // Helper methods for binary operator expression handling
  // =========================================================================

  exprt handle_type_identity_check(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right);

  exprt handle_type_comparison(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right);
 
  exprt erased_type_argument(const nlohmann::json &node);

  static constexpr const char *unknown_class_name = "<unknown class>";

  exprt handle_erased_type_comparison(
    const std::string &op,
    const nlohmann::json &left,
    const nlohmann::json &right);

  std::optional<std::string>
  class_identity_operand(const nlohmann::json &node, const exprt &expr) const;

  exprt handle_tagged_scalar_binop(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right,
    const nlohmann::json &element);

  exprt handle_dict_bitwise(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &element);
 
  exprt
  build_emptiness_check(const exprt &value, const nlohmann::json &element);

  static void convert_function_call_to_side_effect(exprt &expr);

  void convert_function_calls_to_side_effects(exprt &lhs, exprt &rhs);

  exprt handle_chained_comparisons_logic(
    const nlohmann::json &element,
    exprt &bin_expr);

  std::pair<exprt, exprt> chained_pair_operands(
    const nlohmann::json &element,
    size_t i,
    exprt &first_pair,
    exprt &reuse);

  exprt bind_chained_comparator(
    const exprt &operand,
    const nlohmann::json &element,
    exprt &reuse);

  exprt bind_operand_read_twice(
    const exprt &operand,
    const nlohmann::json &element,
    exprt &reread);

  bool handle_none_check_setup(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs);

  exprt numpy_array_arithmetic(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs,
    const locationt &location);
  void
  guard_negative_exponents(const exprt &exponents, const locationt &location);
  exprt numpy_elementwise(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs,
    const typet &type);
  exprt raise_in_expression(
    const std::string &exception,
    const std::string &message,
    const typet &type);
  void reject_unmodelled_array_arithmetic(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &element);
  exprt
  numpy_float_remainder(const exprt &x, const exprt &y, const typet &type);
  exprt numpy_element_op(
    const std::string &op,
    const exprt &x,
    const exprt &y,
    const typet &type);
  exprt handle_array_operations(
    const std::string &op,
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right,
    const nlohmann::json &element);

  exprt build_bytes_concat(const exprt &lhs, const exprt &rhs);
 
  // A right operand of list + that is never a list: a scalar, a str, or a
  // tuple outside `+=` (which extends the list).
  bool is_definite_non_list_addend(
    const typet &type,
    const nlohmann::json &element) const;

  exprt handle_list_operations(
    const std::string &op,
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right,
    const nlohmann::json &element);

  exprt handle_relational_type_mismatches(
    const std::string &op,
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &element);

  exprt handle_string_binary_operations(
    const std::string &op,
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right,
    const nlohmann::json &element);

  exprt str_pointer_add_error(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right);

  exprt build_binary_expression(const std::string &op, exprt &lhs, exprt &rhs);

  typet infer_return_type_from_body(const nlohmann::json &body);
 
  // =========================================================================
  // String method helpers
  // =========================================================================
 
  exprt handle_string_type_mismatch(
    const exprt &lhs,
    const exprt &rhs,
    const std::string &op);
 
  void process_forward_reference(
    const nlohmann::json &annotation,
    codet &target_block);
 
  // Build the class a `tag-<Name>` symbol type refers to when it is defined
  // later in the module, so the type can be followed.
  void build_forward_class(const typet &type);
 
  // =========================================================================
  // Optional type helpers
  // =========================================================================

  typet optional_return_type(
    const nlohmann::json &function_node,
    const typet &declared);
  exprt wrap_in_optional(const exprt &value, const typet &optional_type);
  exprt wrap_if_optional(const exprt &value, const typet &type)
  {
    return type_utils::is_optional_struct(type) ? wrap_in_optional(value, type)
                                                : value;
  }
  exprt wrap_stored_if_optional(const exprt &value, const typet &type);
  typet optional_ternary_type(exprt &then, exprt &else_expr, bool then_is_none);
  exprt get_return_value(const nlohmann::json &value);
  typet subscript_annotation_type(
    const std::string &base,
    const nlohmann::json &var_node);
 
  // =========================================================================
  // Enum support helpers
  // =========================================================================

  exprt make_enum_member_struct_expr(
    const symbolt &int_sym,
    const std::string &class_name,
    const std::string &member_name);
 
  void adopt_tagged_element(symbolt *lhs_symbol, exprt &lhs, const exprt &rhs);
 
  void adopt_array_type(symbolt &lhs_symbol, exprt &lhs, exprt &rhs);

  exprt materialize_optional(const exprt &expr, const nlohmann::json &element);
  exprt check_float_fits_int_return(
    const nlohmann::json &ast_node,
    const exprt &value,
    codet &target_block);
  static exprt string_literal_address(const exprt &array);
  void
  decay_string_literal_returns(exprt &node, const typet &return_type) const;
  exprt coerce_optional_return(
    const exprt &value,
    const locationt &location,
    codet &target_block);
  exprt narrow_optional_return(
    const exprt &value,
    const locationt &location,
    codet &target_block);
  exprt resolve_optional_operands(
    const std::string &op,
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &element,
    bool is_none_check);
  exprt unwrap_optional_if_needed(
    const exprt &expr,
    const nlohmann::json &element = nlohmann::json());
 
  // =========================================================================
  // Dunder method dispatch for user-defined struct types
  // =========================================================================
 
  static std::string op_to_dunder(const std::string &op);
  static std::string op_to_rdunder(const std::string &op);
  exprt apply_bool_dunder(exprt cond, const locationt &location);

  exprt fold_tagged_identity(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right);

  exprt tagged_truthiness(exprt value, const nlohmann::json &node);

  exprt handle_tagged_unary_operator(
    const std::string &op,
    const exprt &operand,
    const nlohmann::json &element);

  void refuse_tagged_boolop_operand(const exprt &operand) const;

  exprt apply_string_truthiness(const exprt &str, const locationt &location);

  exprt apply_bool_dunder_for_not(
    const std::string &op,
    exprt operand,
    const locationt &location);
 
  symbolt *find_dunder_method(
    const std::string &class_name,
    const std::string &dunder_name);

  std::string instance_class_name(const nlohmann::json &value_node);

  bool is_class_instance(const nlohmann::json &value_node);
  bool has_dunder_method(
    const nlohmann::json &value_node,
    const std::string &dunder_name);
  exprt dispatch_dunder_operator(
    const std::string &op,
    exprt &lhs,
    exprt &rhs,
    const locationt &loc);
  exprt dispatch_unary_dunder_operator(
    const std::string &op,
    exprt &operand,
    const locationt &loc);
 
  // =========================================================================
  // Member variables
  // =========================================================================
 
  contextt &symbol_table_;
  const nlohmann::json *ast_json;
  const nlohmann::json *entry_ast_;
  const std::vector<nlohmann::json> *extra_asts_;
  const global_scope &global_scope_;
  type_handler type_handler_;
  element_type_registry element_type_registry_;
  std::vector<std::function<void()>> deferred_checks_;
  string_builder *string_builder_;
  symbol_generator sym_generator_;
 
  namespacet ns;
  typet current_element_type;
  typet current_func_return_type_;
  bool current_func_annotated_int_ = false;
  typet ternary_return_target_;
  std::string main_python_file;
  std::string current_python_file;
  size_t not_callable_count_ = 0;
  nlohmann::json imported_module_json;
  std::string current_func_name_;
  std::string current_class_name_;
  std::size_t get_expr_depth_ = 0;
  code_blockt *current_block;
  exprt *current_lhs;
  std::array<const nlohmann::json *, 2> type_compared_operands_{};
  string_handler string_handler_;
  python_math math_handler_;
  complex_handler complex_handler_;
  dynamic_type_handler dynamic_type_handler_;
  tuple_handler *tuple_handler_;
  python_dict_handler *dict_handler_;
  python_typechecking *typechecker_ = nullptr;
  python_lambda *lambda_handler_;
  python_exception_handler *exception_handler_;
 
  bool is_converting_lhs = false;
  bool is_converting_rhs = false;
 
  // The assignment target node currently being converted, or null. Reads
  // nested inside a target -- the index in `xs[idx[0]] = v`, the base in
  // `xs[0][1] = v` -- are converted with is_converting_lhs set too, so only
  // node identity picks out the slot actually being stored to.
  const nlohmann::json *lhs_store_target_ = nullptr;

  bool is_store_target(const nlohmann::json &node) const
  {
    return is_converting_lhs && lhs_store_target_ == &node;
  }
  // The ZeroDivisionError guard (and its divisor hoist) must be emitted only
  // where the division is really code-generated in its execution context.
  // Keep it inside a lambda body converted at its definition (the enclosing
  // block is still current) and suppress it during the discarded type-probe
  // pass of an assignment RHS (which would otherwise emit the guard twice as
  // dead code and evaluate a side-effecting divisor an extra time).
  bool converting_defaults_ = false;
  bool converting_lambda_body_ = false;
  std::map<std::string, irep_idt> lambda_copies_;
  bool in_rhs_type_probe_ = false;
  // Set while probe_expr() evaluates a node only to inspect its result.
  bool in_scratch_probe_ = false;
  // A clause is a specification, not code: converting one must not plant a
  // statement into the enclosing block. The guard did, so annotating a file
  // changed its verification result with contracts switched off, and a `//` in
  // a loop invariant raised inside the loop body. C emits nothing from a
  // clause either.
  bool in_contract_clause_ = false;
  bool in_lazy_operand_ = false;
  // Number of try bodies enclosing the statement being converted.
  unsigned try_body_depth_ = 0;
  // The test of the assert statement being converted; see
  // lower_short_circuit_boolop.
  const nlohmann::json *asserted_test_ = nullptr;
 
  bool needs_zero_division_guard(const std::string &op, const exprt &rhs) const;
  // Set by resolve_any_subscript_array_type when it adopts an array type for
  // an Any-annotated `row = a[i]`-style assignment. The RHS in that case is a
  // raw index/slice expression rather than an already-materialized array
  // symbol, and the backend rejects a single whole-array-to-whole-array
  // code_assignt between those (Z3 sort mismatch) -- get_var_assign's final
  // store must copy it element by element instead.
  bool any_subscript_array_needs_copy_ = false;
  // An array-type probe may already have built this exprt while resolving the
  // RHS's real type. get_var_assign's RHS fetch reuses it instead of converting
  // the same RHS AST node a second time (which would duplicate any temporaries/
  // instructions the probe emitted, e.g. for fancy/mask/column selection).
  exprt cached_any_subscript_rhs_;
  bool has_cached_any_subscript_rhs_ = false;
  std::set<std::string> numpy_array_symbols_;
  std::unordered_map<irep_idt, std::string, irep_id_hash> class_object_names_;
  std::map<std::string, int> class_ids_;

  bool unpack_record_trusted_ = false;
  std::unordered_map<std::string, std::string> numpy_view_copy_sources_;
  std::unordered_map<std::string, std::string> numpy_array_storage_aliases_;
  // A pointer-backed numpy view's logical shape (ADR-NP-003 etapa 2 scalar
  // strided views: 1-D unit-stride slices, 2-D row views, column views,
  // stepped/reversed 1-D slices, diagonal views, ravel/.flat). `length` is
  // the number of logical elements: __ESBMC_get_object_size on the pointer
  // reports the base object's remaining size from that offset, not this
  // (which may be shorter -- e.g. an empty view still points at a valid
  // position), so len() looks the value up here instead for a tracked view
  // symbol. `stride` is the step, in elements, between consecutive logical
  // indices (1 for unit-stride slices and row views, num_cols for column
  // views, num_cols+1 for the main diagonal, an explicit step for a
  // stepped slice). `readonly` rejects writing through the view (the
  // diagonal view NumPy itself treats as read-only); false for every other
  // kind. See list_access.cpp's handle_range_slice/handle_index_access and
  // converter_funcall.cpp's len() dispatch.
  struct numpy_scalar_pointer_view_infot
  {
    std::size_t length;
    long long stride;
    bool readonly;
    std::vector<std::size_t> shape;
    std::string source_id;
    // The other storages a view bound to different arrays on different
    // paths may point at.
    std::set<std::string> other_sources;
    // Per-axis element strides of an N-D view over a scalar pointer; empty
    // for a contiguous view (typed pointer to rows) or a legacy 1-D view.
    std::vector<long long> strides;
    // Runtime extents and strides, as the ids of the signed 64-bit temporaries
    // holding them ("" for an axis whose value is a constant). Parallel to
    // shape/strides, whose entries are placeholders for a runtime axis.
    std::vector<std::string> shape_symbols;
    std::vector<std::string> stride_symbols;
    bool is_symbolic() const
    {
      for (const std::string &id : shape_symbols)
        if (!id.empty())
          return true;
      for (const std::string &id : stride_symbols)
        if (!id.empty())
          return true;
      return false;
    }
  };
  std::unordered_map<std::string, numpy_scalar_pointer_view_infot>
    numpy_pointer_view_info_;
  std::map<std::string, numpy_nditer_state> numpy_nditers_;
  std::map<std::string, numpy_nditer_item> numpy_nditer_items_;
  nlohmann::json current_nditer_call_;
  std::string current_nditer_state_;
  unsigned nditer_counter_ = 0;
  std::vector<exprt> prebuilt_exprs_;
  const numpy_scalar_pointer_view_infot *
  find_numpy_pointer_view_info(const std::string &name) const;
  // Scans call sites of `func_name` for subscript view arguments at
  // `param_index`; returns the common elem type and view info when all sites
  // agree; returns false on conflict or when no analyzable view site exists.
  bool try_infer_numpy_view_param(
    const std::string &func_name,
    std::size_t param_index,
    typet &out_elem_type,
    numpy_scalar_pointer_view_infot &out_info) const;
  bool try_infer_numpy_view_param(
    const std::string &func_name,
    std::size_t param_index,
    typet &out_elem_type,
    numpy_scalar_pointer_view_infot &out_info,
    std::set<std::string> &visiting) const;
  std::optional<typet> numpy_literal_array_type(
    const std::string &arr_name,
    const std::string &function,
    int line,
    unsigned depth = 0) const;
  std::optional<typet> numpy_filled_array_type(
    const nlohmann::json &value,
    const std::string &function) const;
  std::optional<typet> numpy_arange_array_type(
    const nlohmann::json &value,
    const std::string &function) const;
  exprt list_argument_expr(const nlohmann::json &arg);
  typet returned_function_return_type(const nlohmann::json &call);
  typet stored_function_return_type(const nlohmann::json &value);
  std::optional<typet>
  dict_function_return_type(const nlohmann::json &container);
  bool dict_values(
    const nlohmann::json &container,
    std::vector<nlohmann::json> &out);
  typet subscript_call_return_type(
    const exprt &func_ptr,
    const nlohmann::json &func_node);
  std::optional<std::vector<std::size_t>>
  numpy_filled_array_shape(const nlohmann::json &value) const;
  const std::optional<std::pair<typet, numpy_scalar_pointer_view_infot>> &
  inferred_numpy_view_param(
    const std::string &func_name,
    std::size_t param_index);
  bool is_bound_numpy_view_param(
    const std::string &func_name,
    std::size_t param_index);
  void reject_numpy_view_argument_type_mismatch(const nlohmann::json &call);
  std::map<
    std::string,
    std::optional<std::pair<typet, numpy_scalar_pointer_view_infot>>>
    numpy_view_param_layouts_;
  // Parameters whose conversion has decided whether they bind a view, and
  // what callers converted before that were told.
  std::set<std::string> numpy_view_params_decided_;
  std::map<std::string, bool> numpy_view_params_assumed_;
  static std::optional<numpy_scalar_pointer_view_infot>
  slice_view_info(std::size_t length, const nlohmann::json &slice_node);
  static std::optional<numpy_scalar_pointer_view_infot> row_slice_view_info(
    std::size_t rows,
    std::size_t cols,
    const nlohmann::json &slice_node);
  static std::optional<numpy_scalar_pointer_view_infot> column_view_info(
    std::size_t rows,
    std::size_t cols,
    const nlohmann::json &slice_node);
  static std::optional<numpy_scalar_pointer_view_infot>
  view_info_from_subscript(
    const std::vector<std::size_t> &src_shape,
    const nlohmann::json &slice_node);
  static numpy_scalar_pointer_view_infot
  runtime_view_info(std::size_t rank = 1);
  static std::optional<numpy_scalar_pointer_view_infot>
  slice_or_runtime_view_info(
    std::size_t length,
    const nlohmann::json &slice_node);
  static std::optional<std::pair<typet, numpy_scalar_pointer_view_infot>>
  merge_view_layouts(
    const std::pair<typet, numpy_scalar_pointer_view_infot> &a,
    const std::pair<typet, numpy_scalar_pointer_view_infot> &b);
  // Symbol ids holding the extent and stride of each axis of a view whose
  // layout is read at run time.
  struct numpy_runtime_view_layoutt
  {
    std::vector<std::string> extents;
    std::vector<std::string> strides;
  };
  // Keyed like numpy_view_params_: the statics every caller writes, and the
  // parameter symbol with the callee's own copies.
  std::map<std::string, numpy_runtime_view_layoutt> numpy_runtime_view_statics_;
  std::map<std::string, std::pair<std::string, numpy_runtime_view_layoutt>>
    numpy_runtime_view_locals_;
  const nlohmann::json *numpy_runtime_bound_call_ = nullptr;
  const numpy_runtime_view_layoutt &
  runtime_numpy_view_statics(const std::string &key, std::size_t rank);
  void declare_runtime_numpy_view_param(
    numpy_scalar_pointer_view_infot &info,
    const std::string &arg_id,
    const std::string &key);
  void prepend_runtime_numpy_view_prologue(
    const std::string &function_id,
    exprt &function_body);
  void bind_runtime_numpy_view_arguments(
    const nlohmann::json &statement,
    codet &target_block);
  void store_runtime_numpy_view_layout(
    const nlohmann::json &call,
    const std::string &func_name,
    std::size_t param_index,
    codet &target_block);
  std::string numpy_view_callee_of(const nlohmann::json &call);
  std::vector<std::size_t>
  runtime_numpy_view_params(const std::string &func_name);
  void reject_unbound_runtime_numpy_view_call(const nlohmann::json &call);
  static bool same_view_layout(
    const std::pair<typet, numpy_scalar_pointer_view_infot> &a,
    const std::pair<typet, numpy_scalar_pointer_view_infot> &b);
  static std::optional<numpy_scalar_pointer_view_infot> subview_info(
    const numpy_scalar_pointer_view_infot &parent,
    const nlohmann::json &slice_node);
  std::optional<std::pair<typet, numpy_scalar_pointer_view_infot>>
  infer_diagonal_view_layout(
    const nlohmann::json &call,
    const std::string &function) const;
  std::optional<std::pair<typet, numpy_scalar_pointer_view_infot>>
  infer_branch_bound_view_layout(
    const nlohmann::json &node,
    const std::string &function,
    std::set<std::string> &visiting,
    unsigned depth) const;
  std::optional<std::pair<typet, numpy_scalar_pointer_view_infot>>
  infer_numpy_view_layout(
    const nlohmann::json &node,
    const std::string &function,
    std::set<std::string> &visiting,
    unsigned depth = 0) const;
  std::optional<numpy_scalar_pointer_view_infot> infer_numpy_view_param_type(
    const std::string &func_name,
    std::size_t param_index,
    const std::string &arg_name,
    bool numpy_array_param,
    typet &arg_type) const;
  void register_numpy_view_param(
    const std::optional<numpy_scalar_pointer_view_infot> &view_param,
    const std::string &arg_id,
    const std::string &func_name,
    std::size_t param_index);
  // Runtime length of the named view when its extent is not a constant.
  std::optional<exprt>
  symbolic_numpy_view_length(const std::string &name) const;
  // Axis `axis` extent / stride of a view as signed 64-bit expressions.
  exprt numpy_view_extent(
    const numpy_scalar_pointer_view_infot &info,
    std::size_t axis) const;
  exprt numpy_view_stride(
    const numpy_scalar_pointer_view_infot &info,
    std::size_t axis) const;
  // Consumers that need a constant length/stride reject a symbolic view.
  static void
  reject_symbolic_numpy_view(const numpy_scalar_pointer_view_infot &info);

  struct strided_copy_axis
  {
    exprt extent;
    exprt stride;
  };

  void emit_strided_copy(
    codet &block,
    const exprt &dst,
    const exprt &src,
    const exprt &offset,
    const std::vector<strided_copy_axis> &axes,
    const locationt &location);

  std::string snapshot_symbolic_numpy_view(
    const exprt &old_ptr,
    numpy_scalar_pointer_view_infot &info,
    const locationt &location,
    codet &target_block);
  void reject_numpy_view_rebind() const;
  bool accepts_numpy_view_binding(
    const std::string &lhs_id,
    const numpy_scalar_pointer_view_infot &candidate,
    const typet &view_ptr_type,
    const exprt &source);
  bool can_merge_numpy_view_layouts(const std::string &view_id) const;
  const numpy_runtime_view_layoutt &
  numpy_view_layout_vars(const std::string &view_id, std::size_t rank);
  void record_numpy_view_layout(
    const std::string &view_id,
    const std::string &storage_id);
  void merge_numpy_view_binding(const std::string &view_id, bool same_kind);
  static bool same_numpy_view_kind(
    const numpy_scalar_pointer_view_infot &a,
    const numpy_scalar_pointer_view_infot &b);
  // Layout variables of each view name, the function-local ones among them,
  // and the names whose metadata reads them.
  std::map<std::string, numpy_runtime_view_layoutt> numpy_view_layout_vars_;
  std::vector<std::string> numpy_view_layout_locals_;
  std::set<std::string> numpy_merged_views_;
  std::map<std::string, std::set<std::string>> numpy_view_other_sources_;
  std::set<std::string> numpy_view_storage_roots(const std::string &id) const;
  unsigned numpy_loop_depth_ = 0;
  // Conditional expressions being converted; their arms run on one path only.
  unsigned conditional_expr_depth_ = 0;
  // Converting an and/or operand into the block of effects it owns.
  bool in_operand_effects_block_ = false;
  std::vector<exprt> read_strided_view_elements(
    const exprt &base,
    const std::vector<long long> &strides,
    const std::vector<std::size_t> &shape);
  std::vector<exprt> read_contiguous_view_elements(
    exprt base,
    std::size_t count,
    long long stride,
    const std::vector<std::size_t> &shape);
  std::string snapshot_constant_numpy_view(
    const symbolt &view_symbol,
    numpy_scalar_pointer_view_infot &info,
    const locationt &location,
    codet &target_block);
  struct numpy_view_containert
  {
    std::vector<std::string> elements;
    std::map<std::string, std::size_t> keys;
    bool is_dict = false;
  };
  std::unordered_map<std::string, numpy_view_containert> numpy_view_containers_;
  std::size_t numpy_view_container_count_ = 0;
  const numpy_view_containert *
  find_numpy_view_container(const nlohmann::json &node) const;
  std::string numpy_view_container_element(
    const numpy_view_containert &container,
    const nlohmann::json &slice) const;
  std::optional<nlohmann::json>
  resolve_numpy_view_container_use(const nlohmann::json &node) const;
  nlohmann::json
  rewrite_numpy_view_container_reads(const nlohmann::json &node) const;
  const nlohmann::json &resolve_numpy_view_containers(
    const nlohmann::json &statement,
    nlohmann::json &rewritten) const;
  bool try_bind_numpy_view_container(
    const nlohmann::json &ast_node,
    codet &target_block);
  std::unordered_set<std::string> numpy_view_return_functions_;
  std::unordered_set<std::string> numpy_fold_only_functions_;
  std::unordered_set<std::string> numpy_escaped_storage_;
  std::unordered_set<std::string> numpy_readonly_arrays_;
  std::vector<std::string> model_namespaces_;
  // A 2-D+ numpy array parameter's full logical shape, keyed by the
  // parameter's own symbol id. register_function_argument decays such a
  // parameter to a pointer to its row type for the C ABI (gen_pointer_type
  // over arg_type.subtype()), which is what the backend needs but erases the
  // outer dimension from the parameter's own type -- unwrapping the pointer
  // recovers only the row shape, not the row count. `.shape`/`.ndim`/`.size`
  // and the array-consuming numpy calls (transpose, sort/argsort/
  // searchsorted, reducers) read the pre-decay shape from here instead.
  std::unordered_map<std::string, std::vector<std::size_t>> numpy_param_shapes_;
  std::unordered_map<std::string, typet> numpy_param_array_types_;
  std::unordered_set<std::string> numpy_ambiguous_shape_symbols_;
  // List parameters mixing strings and numbers whose call sites agree on
  // each position's type, so a constant index reads that type (#8670).
  std::unordered_set<std::string> positional_list_params_;
  // Keys are "func_name#param_index" for parameters that receive numpy views
  // and have registered view metadata in numpy_pointer_view_info_.
  std::set<std::string> numpy_view_params_;
  std::unordered_set<std::string> numpy_view_param_symbols_;
  bool is_loading_models = false;
  bool is_importing_module = false;
  bool base_ctor_called = false;
  bool build_static_lists = false;
  typet numpy_element_type;

  std::set<std::string> call_escaped_lists_;

  std::map<std::string, std::set<std::string>> instance_attr_map;
  std::map<std::string, std::set<std::string>> certain_instance_attrs_;
  std::unordered_map<std::string, std::string> imported_modules;

  std::map<std::string, nlohmann::json> module_ast_pool_;
  std::unordered_map<std::string, std::string> input_str_to_len_sym_;

  std::unordered_map<std::string, std::string> retype_aliases_;
  symbolt *follow_retype_alias(symbolt *symbol) const;
  symbolt *retype_store_symbol(
    const nlohmann::json &target,
    const exprt &lhs,
    symbolt *lhs_symbol);

  std::unordered_map<std::string, std::pair<std::string, typet>>
    unbound_global_flags_;
  std::unordered_map<std::string, std::string> unmodelled_base_classes_;
  std::unordered_set<std::string> str_valued_symbols_;
  std::unordered_set<std::string> str_assigned_symbols_;
  std::unordered_set<std::string> out_of_scope_locals_;
  void end_block_scope(const code_blockt &block);

  std::unordered_map<std::string, std::string> flow_class_map_;

  std::string flow_lvalue_path(const nlohmann::json &node) const;

  std::string flow_rhs_class(const nlohmann::json &rhs) const;

  std::string alias_rhs_class(const nlohmann::json &rhs);

  std::string call_return_class(const nlohmann::json &rhs) const;

  unsigned block_nesting_ = 0;

  unsigned function_body_depth_ = 0;

  unsigned loop_body_depth_ = 0;
 
  function_call_cache function_call_cache_;
 
  std::vector<std::string> global_declarations;
  std::map<std::string, std::string> nonlocal_scopes_;
  std::vector<std::string> local_loads;
  bool is_right = false;
  std::vector<std::string> scope_stack_;
 
  exprt extract_type_from_boolean_op(const exprt &bool_op);
};