tuple_handler.h

Go to the documentation of this file.

#ifndef ESBMC_PYTHON_TUPLE_HANDLER_H
#define ESBMC_PYTHON_TUPLE_HANDLER_H
 
#include <python-frontend/python_converter.h>
#include <util/irep/type.h>
#include <util/irep/expr.h>
#include <nlohmann/json.hpp>
#include <string>
 
class python_converter;
class type_handler;

class tuple_handler
{
public:
  static constexpr size_t tuple_str_member_size = 16;

  tuple_handler(python_converter &converter, type_handler &type_handler);

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

  exprt handle_tuple_subscript(
    const exprt &array,
    const nlohmann::json &slice,
    const nlohmann::json &element);

  bool is_tuple_type(const typet &type) const;

  void handle_tuple_unpacking(
    const nlohmann::json &ast_node,
    const nlohmann::json &target,
    exprt &rhs,
    codet &target_block);

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

  exprt prepare_rhs_for_unpacking(
    const nlohmann::json &ast_node,
    exprt &rhs,
    codet &target_block);

  exprt handle_tuple_membership(
    const exprt &lhs,
    const exprt &rhs,
    bool invert,
    const nlohmann::json &element);

  struct_typet
  create_tuple_struct_type(const std::vector<typet> &element_types) const;

  exprt get_tuple_element(
    const exprt &array,
    const struct_typet &tuple_type,
    size_t idx) const;

  exprt coerce_to_tuple_type(
    const exprt &value,
    const typet &target,
    const locationt &loc,
    codet &target_block);
 
private:
  std::string build_tuple_tag(const std::vector<typet> &element_types) const;

  exprt pad_string_element(const exprt &elem) const;

  size_t starred_target_index(const nlohmann::json &targets) const;

  symbolt &unpack_target_symbol(
    const nlohmann::json &name_node,
    const typet &type,
    codet &target_block);
 
  typet unpack_target_type(const exprt &rhs, const typet &member_type) const;

  void assign_unpacked_element(
    const exprt &target,
    const exprt &member_access,
    const locationt &loc,
    codet &target_block);

  void assign_starred_elements(
    const nlohmann::json &ast_node,
    const nlohmann::json &star_value,
    const exprt &rhs,
    size_t first,
    size_t count,
    codet &target_block);

  exprt copy_str_to_member(
    const exprt &str,
    const array_typet &member_type,
    const locationt &loc,
    codet &target_block);

  typet tuple_member_type_from_annotation(const nlohmann::json &node);
 
  python_converter &converter_;
  type_handler &type_handler_;
};
 
#endif // ESBMC_PYTHON_TUPLE_HANDLER_H