string_builder.h

Go to the documentation of this file.

#pragma once
 
#include <util/irep/expr.h>
#include <util/irep/type.h>
#include <nlohmann/json.hpp>
#include <vector>
#include <string>
#include <cstdint>
 
// Forward declaration
class python_converter;
class type_handler;
class contextt;
class string_handler;

class string_builder
{
public:
  explicit string_builder(python_converter &converter, string_handler *handler);

  exprt make_null_terminator();

  exprt make_char_constant(unsigned char ch);

  std::vector<exprt> extract_string_chars(
    const exprt &expr,
    const nlohmann::json &json_node = nlohmann::json());

  exprt build_null_terminated_string(const std::vector<exprt> &chars);

  exprt build_string_literal(const std::string &str);

  exprt build_byte_string(const std::vector<uint8_t> &bytes);

  exprt ensure_null_terminated_string(exprt &e);

  exprt concatenate_strings(
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &left = nlohmann::json(),
    const nlohmann::json &right = nlohmann::json());
 
  exprt handle_string_repetition(exprt &lhs, exprt &rhs);

  exprt build_raw_byte_array(const std::vector<uint8_t> &bytes);
 
  exprt concatenate_strings_via_c_function(
    const exprt &lhs,
    const exprt &rhs,
    const nlohmann::json &left);

  exprt build_runtime_str_conversion_call(
    const std::string &fn_name,
    const typet &arg_type,
    const exprt &arg);

  exprt
  build_runtime_str_join_call(const exprt &separator, const exprt &list_expr);
 
private:
  python_converter &converter_;
  string_handler *str_handler_;
  contextt &get_symbol_table() const;
  type_handler &get_type_handler();
};