string_handler.h

Go to the documentation of this file.

#ifndef PYTHON_FRONTEND_STRING_HANDLER_H
#define PYTHON_FRONTEND_STRING_HANDLER_H
 
#include <util/irep/expr.h>
#include <util/irep/std_types.h>
#include <util/arith/arith_tools.h>
#include <util/lang/c_types.h>
#include <util/symtab/context.h>
#include <util/message/message.h>
#include <nlohmann/json.hpp>
#include <optional>
#include <string>
#include <unordered_map>
#include <vector>
 
// Forward declarations
class python_converter;
class type_handler;
class string_builder;

class string_handler
{
public:
  string_handler(
    python_converter &converter,
    contextt &symbol_table,
    type_handler &type_handler,
    string_builder *str_builder);
 
  void set_string_builder(string_builder *sb)
  {
    string_builder_ = sb;
  }
 
  // String size and conversion operations

  BigInt get_string_size(const exprt &expr);

  exprt convert_to_string(const exprt &expr);

  static std::string fstring_repr_of_constant(const nlohmann::json &operand);

  exprt build_fstring_conversion(
    const nlohmann::json &value,
    int conversion,
    const exprt &operand,
    const locationt &location);

  exprt build_repr(const exprt &value, const locationt &location);

  exprt format_fstring_part(const nlohmann::json &value);
 
  exprt build_nondet_string_fallback(const locationt &location);

  exprt build_nondet_string(const locationt &location);

  static int nondet_str_buffer_size();

  std::string extract_string_from_array_operands(const exprt &array_expr) const;

  void ensure_string_array(exprt &expr);

  exprt ensure_null_terminated_string(exprt &e);
 
  // Format string operations

  std::string process_format_spec(const nlohmann::json &format_spec);

  exprt
  apply_format_specification(const exprt &expr, const std::string &format);

  exprt format_runtime_value(const exprt &expr, const std::string &format);

  exprt get_fstring_expr(const nlohmann::json &element);
 
  // String concatenation operations

  exprt handle_string_concatenation(
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right);

  exprt handle_string_concatenation_with_promotion(
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right);
 
  // String comparison operations

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

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

  exprt create_char_comparison_expr(
    const std::string &op,
    const exprt &lhs_char_value,
    const exprt &rhs_char_value,
    const exprt &lhs_source,
    const exprt &rhs_source) const;

  exprt handle_string_repetition(exprt &lhs, exprt &rhs);

  exprt handle_string_operations(
    const std::string &op,
    exprt &lhs,
    exprt &rhs,
    const nlohmann::json &left,
    const nlohmann::json &right,
    const nlohmann::json &element);
 
  // String joining operations

  exprt handle_str_join(const nlohmann::json &call_json);
  exprt join_unfoldable_iterable(
    const exprt &separator,
    const nlohmann::json &call_json);

  exprt convert_join_items(
    const nlohmann::json &elements,
    std::vector<exprt> &elem_exprs);

  exprt handle_string_attribute_call(const nlohmann::json &call_json);

  exprt read_tagged_str_receiver(
    const exprt &receiver,
    const std::string &method,
    const nlohmann::json &call_json);

  exprt try_handle_len_string_fast_path(
    const nlohmann::json &call_json,
    const exprt &arg_expr);
  exprt char_array_type_length(const exprt &arg_expr) const;
 
  // String method operations

  exprt handle_string_startswith(
    const exprt &string_obj,
    const exprt &prefix_arg,
    const locationt &location);

  exprt handle_string_endswith(
    const exprt &string_obj,
    const exprt &suffix_arg,
    const locationt &location);

  exprt handle_startswith_endswith_with_pos(
    const exprt &string_obj,
    const nlohmann::json &args,
    python_converter &converter,
    const locationt &location,
    bool is_suffix);

  exprt build_affix_tuple_match(
    const exprt &string_obj,
    const exprt &affix_tuple,
    const locationt &location,
    bool is_suffix);

  exprt
  handle_string_isdigit(const exprt &string_obj, const locationt &location);

  exprt
  handle_string_isalpha(const exprt &string_obj, const locationt &location);

  exprt handle_string_isspace(const exprt &str_expr, const locationt &location);

  exprt handle_char_isspace(const exprt &char_expr, const locationt &location);

  exprt handle_string_lstrip(
    const exprt &str_expr,
    const exprt &chars_arg,
    const locationt &location);

  exprt handle_string_strip(
    const exprt &str_expr,
    const exprt &chars_arg,
    const locationt &location);

  exprt handle_string_rstrip(
    const exprt &str_expr,
    const exprt &chars_arg,
    const locationt &location);

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

  exprt
  handle_string_islower(const exprt &string_obj, const locationt &location);

  exprt handle_string_lower(const exprt &string_obj, const locationt &location);

  exprt handle_string_upper(const exprt &string_obj, const locationt &location);
  exprt handle_string_find(
    const exprt &string_obj,
    const exprt &find_arg,
    const locationt &location);

  exprt handle_string_find_range(
    const exprt &string_obj,
    const exprt &find_arg,
    const exprt &start_arg,
    const exprt &end_arg,
    const locationt &location);

  exprt handle_string_index(
    const nlohmann::json &call,
    const exprt &string_obj,
    const exprt &find_arg,
    const locationt &location);

  exprt handle_string_index_range(
    const nlohmann::json &call,
    const exprt &string_obj,
    const exprt &find_arg,
    const exprt &start_arg,
    const exprt &end_arg,
    const locationt &location);

  exprt handle_string_rfind(
    const exprt &string_obj,
    const exprt &find_arg,
    const locationt &location);

  exprt handle_string_rfind_range(
    const exprt &string_obj,
    const exprt &find_arg,
    const exprt &start_arg,
    const exprt &end_arg,
    const locationt &location);

  exprt handle_string_rindex(
    const nlohmann::json &call,
    const exprt &string_obj,
    const exprt &find_arg,
    const locationt &location);

  exprt handle_string_rindex_range(
    const nlohmann::json &call,
    const exprt &string_obj,
    const exprt &find_arg,
    const exprt &start_arg,
    const exprt &end_arg,
    const locationt &location);

  exprt handle_string_replace(
    const exprt &string_obj,
    const exprt &old_arg,
    const exprt &new_arg,
    const exprt &count_arg,
    const locationt &location);

  exprt
  handle_string_capitalize(const exprt &string_obj, const locationt &location);

  exprt handle_string_title(const exprt &string_obj, const locationt &location);

  exprt
  handle_string_swapcase(const exprt &string_obj, const locationt &location);

  exprt
  handle_string_casefold(const exprt &string_obj, const locationt &location);

  exprt handle_string_count(
    const exprt &string_obj,
    const exprt &sub_arg,
    const exprt &start_arg,
    const exprt &end_arg,
    const locationt &location);

  exprt handle_string_removeprefix(
    const exprt &string_obj,
    const exprt &prefix_arg,
    const locationt &location);

  exprt handle_string_removesuffix(
    const exprt &string_obj,
    const exprt &suffix_arg,
    const locationt &location);

  exprt handle_string_splitlines(
    const nlohmann::json &call,
    const exprt &string_obj,
    const locationt &location,
    bool keepends = false);

  exprt handle_string_format(
    const nlohmann::json &call,
    const exprt &string_obj,
    const locationt &location);

  exprt handle_string_partition(
    const exprt &string_obj,
    const exprt &sep_arg,
    const locationt &location);

  exprt handle_string_rpartition(
    const exprt &string_obj,
    const exprt &sep_arg,
    const locationt &location);

  exprt build_partition_tuple(
    const exprt &string_obj,
    const exprt &sep_arg,
    const locationt &location,
    bool from_right);

  exprt handle_string_isalnum(
    const exprt &string_obj,
    [[maybe_unused]] const locationt &location);

  exprt handle_string_isupper(
    const exprt &string_obj,
    [[maybe_unused]] const locationt &location);

  exprt handle_string_isnumeric(
    const exprt &string_obj,
    [[maybe_unused]] const locationt &location);

  exprt handle_string_isidentifier(
    const exprt &string_obj,
    [[maybe_unused]] const locationt &location);

  exprt handle_string_center(
    const exprt &string_obj,
    const exprt &width_arg,
    const exprt &fill_arg,
    const locationt &location);

  exprt handle_string_ljust(
    const exprt &string_obj,
    const exprt &width_arg,
    const exprt &fill_arg,
    const locationt &location);

  exprt handle_string_rjust(
    const exprt &string_obj,
    const exprt &width_arg,
    const exprt &fill_arg,
    const locationt &location);

  exprt handle_string_zfill(
    const exprt &string_obj,
    const exprt &width_arg,
    const locationt &location);

  exprt handle_string_expandtabs(
    const exprt &string_obj,
    const exprt &tabsize_arg,
    const locationt &location);

  exprt handle_string_format_map(
    const nlohmann::json &call,
    const exprt &string_obj,
    const locationt &location);

  static bool extract_constant_string(
    const nlohmann::json &node,
    python_converter &converter,
    std::string &out);
 
  // Utility methods

  bool is_zero_length_array(const exprt &expr);

  exprt get_array_base_address(const exprt &arr);

  exprt handle_string_to_int(
    const exprt &string_obj,
    const exprt &base_arg,
    const locationt &location);

  exprt handle_string_to_int_base10(
    const exprt &string_obj,
    const locationt &location);

  exprt handle_int_conversion(const exprt &arg, const locationt &location);

  exprt handle_int_conversion_with_base(
    const exprt &arg,
    const exprt &base,
    const locationt &location);

  exprt
  handle_string_to_float(const exprt &string_obj, const locationt &location);

  exprt
  handle_string_is_float(const exprt &string_obj, const locationt &location);

  exprt
  handle_chr_conversion(const exprt &codepoint_arg, const locationt &location);

  exprt
  handle_ord_conversion(const exprt &string_obj, const locationt &location);
 
private:
  python_converter &converter_;
  contextt &symbol_table_;
  type_handler &type_handler_;
  string_builder *string_builder_;
  std::unordered_map<std::string, symbolt *> symbol_cache_;
  std::unordered_map<std::string, int> assignment_count_cache_;
  std::unordered_map<std::string, bool> assignment_has_augassign_cache_;
  std::unordered_map<std::string, nlohmann::json> var_value_cache_;
  std::string len_cache_scope_id_;
 
  // Helper methods for internal use
  bool try_extract_const_string_expr(const exprt &expr, std::string &out);

  exprt make_char_array_expr(
    const std::vector<unsigned char> &chars,
    const typet &type);

  exprt char_to_string(const exprt &expr);
 
  exprt constant_to_string(const exprt &expr);
 
  exprt build_string_index_result(
    const nlohmann::json &call,
    const exprt &find_expr,
    const locationt &location);

  std::string ensure_string_function_symbol(const std::string &function_name);
 
  symbolt *find_cached_symbol(const std::string &symbol_id);
  const symbolt *find_foldable_symbol(const std::string &symbol_id);
  exprt symbol_to_string(const exprt &expr);
  symbolt *find_cached_c_function_symbol(const std::string &symbol_id);
  exprt try_len_fast_path_from_constant_arg(
    const nlohmann::json &arg_json,
    const exprt &arg_expr);
  exprt try_len_fast_path_from_name_arg(const nlohmann::json &arg_json);

  std::string float_to_string(
    const std::string &float_bits,
    std::size_t width,
    int precision);
 
public:
  static std::string cpython_float_str(double d);
};
 
#endif // PYTHON_FRONTEND_STRING_HANDLER_H