python_dict_handler.h

Go to the documentation of this file.

 
#ifndef PYTHON_DICT_HANDLER_H
#define PYTHON_DICT_HANDLER_H
 
#include <python-frontend/symbol_id.h>
#include <python-frontend/type/element_type_registry.h>
 
#include <util/irep/std_types.h>
#include <util/irep/std_code.h>
#include <util/irep/expr.h>
#include <nlohmann/json.hpp>
 
#include <optional>
#include <string>
#include <unordered_map>
 
class python_converter;
class type_handler;
class contextt;
class symbolt;

class python_dict_handler
{
public:
  python_dict_handler(
    python_converter &converter,
    contextt &symbol_table,
    type_handler &type_handler);

  bool is_dict_literal(const nlohmann::json &element) const;

  exprt get_dict_literal(const nlohmann::json &element);
 
  exprt get_dict_comprehension(const nlohmann::json &element);
 
  // Build a dict comprehension whose iterable is range(...) with a
  // non-constant bound by iterating a counter (the range element value)
  // instead of materialising range into a backing list. See #5222.
  exprt build_range_dict_comprehension(
    const nlohmann::json &element,
    const nlohmann::json &generator,
    symbolt &dict_sym);

  exprt create_dict_from_literal(
    const nlohmann::json &element,
    const exprt &target_symbol);

  void
  create_empty_dict(const nlohmann::json &element, const exprt &target_symbol);

  exprt create_dict_with_unpacking(
    const nlohmann::json &element,
    const exprt &target_symbol);

  exprt handle_dict_subscript(
    const exprt &dict_expr,
    const nlohmann::json &slice_node,
    const typet &expected_type = typet(),
    bool check_type = false);

  void check_value_type(
    bool enabled,
    const exprt &obj,
    const typet &type,
    const locationt &location);

  void handle_dict_subscript_assign(
    const exprt &dict_expr,
    const exprt &key_expr,
    const exprt &value,
    const locationt &location,
    const nlohmann::json &node,
    codet &target_block);

  exprt handle_dict_membership(
    const exprt &key_expr,
    const exprt &dict_expr,
    bool negated);

  void handle_dict_delete(
    const exprt &dict_expr,
    const nlohmann::json &slice_node,
    codet &target_block);

  bool is_dict_type(const typet &type) const;

  bool holds_dict_lists(const typet &type) const;

  struct_typet get_dict_struct_type();

  void resolve_dict_subscript_types(
    const nlohmann::json &left,
    const nlohmann::json &right,
    exprt &lhs,
    exprt &rhs);
 
  bool is_retypable_subscript(const nlohmann::json &node);

  typet
  get_dict_value_type_from_annotation(const nlohmann::json &annotation_node);

  typet get_popitem_tuple_type(const exprt &dict_expr);

  exprt
  handle_dict_popitem(const exprt &dict_expr, const nlohmann::json &call_node);

  typet resolve_expected_type_for_dict_subscript(const exprt &dict_expr);

  exprt read_struct_value(const exprt &obj_value, const typet &type);

  typet literal_value_type_hint;
  typet literal_value_type(const exprt &target);

  typet recorded_tuple_value_type(const exprt &dict_expr) const;

  bool reads_value_as_tagged(
    const exprt &dict_expr,
    const nlohmann::json &slice_node,
    const element_type_registry::entries &entries);
 
  char annotated_value_kind(const exprt &dict_expr);

  typet uniform_list_dict_value_type(const std::string &list_id) const;

  bool handle_subscript_assignment_check(
    python_converter &converter,
    const nlohmann::json &ast_node,
    const nlohmann::json &target,
    codet &target_block);

  bool handle_literal_assignment_check(
    python_converter &converter,
    const nlohmann::json &ast_node,
    const exprt &lhs);

  bool handle_unannotated_literal_check(
    python_converter &converter,
    const nlohmann::json &ast_node,
    const nlohmann::json &target,
    const symbol_id &sid);

  exprt
  handle_dict_get(const exprt &dict_expr, const nlohmann::json &call_node);

  exprt handle_dict_setdefault(
    const exprt &dict_expr,
    const nlohmann::json &call_node);

  exprt
  handle_dict_pop(const exprt &dict_expr, const nlohmann::json &call_node);

  static bool is_value_returning_method(const std::string &method_name);

  std::string
  materialize_tuple_key(exprt &key_expr, const nlohmann::json &element);

  static const std::string &
  get_internal_list_id(const std::string &dict_sym_id, bool keys)
  {
    static const std::string empty;
    auto &m = keys ? dict_keys_list_id_ : dict_vals_list_id_;
    auto it = m.find(dict_sym_id);
    return it != m.end() ? it->second : empty;
  }

  exprt
  handle_dict_update(const exprt &dict_expr, const nlohmann::json &call_node);
 
  exprt bind_dict_source(const exprt &source, const nlohmann::json &node);

  void copy_dict_entries(
    const exprt &dict_expr,
    const exprt &source,
    const nlohmann::json &call_node);

  exprt handle_dict_union(
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &element);

  exprt
  handle_dict_copy(const exprt &dict_expr, const nlohmann::json &call_node);

  exprt
  handle_dict_clear(const exprt &dict_expr, const nlohmann::json &call_node);

  exprt handle_dict_fromkeys(const nlohmann::json &call_node);

  exprt handle_dict_constructor(const nlohmann::json &call_node);

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

  std::optional<bool> try_constant_fold_eq(
    const nlohmann::json &lhs,
    const nlohmann::json &rhs) const;
 
private:
  python_converter &converter_;

  contextt &symbol_table_;

  type_handler &type_handler_;

  static std::unordered_map<std::string, std::string> dict_keys_list_id_;

  static std::unordered_map<std::string, std::string> dict_vals_list_id_;

  typet
  get_dict_key_type_from_annotation(const nlohmann::json &annotation_node);

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

  static size_t generate_nested_dict_type_hash(const typet &dict_type);

  exprt safe_cast_to_dict_pointer(
    const nlohmann::json &node,
    const exprt &obj_value,
    const typet &target_ptr_type,
    const locationt &location);

  void store_nested_dict_value(
    const nlohmann::json &element,
    const symbolt &values_list,
    const exprt &value_expr,
    const locationt &location);

  void store_dict_value_by_pointer(
    const nlohmann::json &node,
    const exprt &value,
    const exprt &values_member,
    const exprt &index,
    const locationt &location,
    codet &target_block,
    code_function_callt &set_call,
    code_function_callt &push_call);

  exprt retrieve_nested_dict_value(
    const nlohmann::json &slice_node,
    const exprt &obj_value,
    const typet &expected_type,
    const locationt &location);

  std::string generate_unique_dict_name(
    const nlohmann::json &element,
    const locationt &location) const;
};
 
#endif // PYTHON_DICT_HANDLER_H