type_utils.h

Go to the documentation of this file.

#pragma once
 
#include <util/lang/c_types.h>
#include <util/irep/expr.h>
#include <util/irep/std_types.h>
#include <util/expr/expr_util.h>
#include <util/irep/type.h>
#include <python-frontend/type/type_handler.h>
 
#include <nlohmann/json.hpp>
 
#include <cctype>
#include <map>
#include <set>
#include <string>
 
enum class StatementType
{
  VARIABLE_ASSIGN,
  COMPOUND_ASSIGN,
  FUNC_DEFINITION,
  IF_STATEMENT,
  WHILE_STATEMENT,
  FOR_STATEMENT,
  EXPR,
  RETURN,
  ASSERT,
  CLASS_DEFINITION,
  PASS,
  IMPORT,
  BREAK,
  CONTINUE,
  RAISE,
  UNKNOWN,
  GLOBAL,
  NONLOCAL,
  TRY,
  EXCEPTHANDLER,
  DELETE_STATEMENT
};
 
enum class ExpressionType
{
  BINARY_OPERATION,
  UNARY_OPERATION,
  FUNC_CALL,
  IF_EXPR,
  LOGICAL_OPERATION,
  LITERAL,
  SUBSCRIPT,
  VARIABLE_REF,
  LIST,
  UNKNOWN,
  FSTRING,
  TUPLE,
  SLICE,
  CLASS_MRO
};
 
struct TypeFlags
{
  bool has_float = false;
  bool has_int = false;
  bool has_bool = false;
  bool has_none = false;
  bool has_other = false;
};
 
class type_utils
{
public:
  static const irep_idt &
  argument_identifier(const code_typet::argumentt &argument)
  {
    return argument.get_identifier().empty() ? argument.identifier()
                                             : argument.get_identifier();
  }
 
  static bool is_builtin_type(const std::string &name)
  {
    return (
      name == "int" || name == "float" || name == "bool" || name == "str" ||
      name == "chr" || name == "hex" || name == "oct" || name == "bin" ||
      name == "ord" || name == "tuple" || name == "list" || name == "dict" ||
      name == "set" || name == "frozenset" || name == "bytes" ||
      name == "bytearray" || name == "range" || name == "complex" ||
      name == "type" || name == "object" || name == "abs" || name == "None" ||
      name == "divmod" || name == "slice");
  }

  static bool is_str_only_method(const std::string &name)
  {
    static const std::set<std::string> str_only_methods = {
      "capitalize",   "casefold",     "center",    "count",     "encode",
      "endswith",     "expandtabs",   "find",      "format",    "format_map",
      "index",        "isalnum",      "isalpha",   "isascii",   "isdecimal",
      "isdigit",      "isidentifier", "islower",   "isnumeric", "isprintable",
      "isspace",      "istitle",      "isupper",   "join",      "ljust",
      "lower",        "lstrip",       "maketrans", "partition", "removeprefix",
      "removesuffix", "replace",      "rfind",     "rindex",    "rjust",
      "rpartition",   "rsplit",       "rstrip",    "split",     "splitlines",
      "startswith",   "strip",        "swapcase",  "title",     "translate",
      "upper",        "zfill"};
    return str_only_methods.count(name) > 0;
  }
 
  static bool is_consensus_type(const std::string &name)
  {
    return (
      name == "uint64" || name == "uint256" || name == "Epoch" ||
      name == "Gwei" || name == "BLSFieldElement" || name == "Slot" ||
      name == "GeneralizedIndex");
  }

  static bool is_typeddict(const std::string &name)
  {
    return name == "TypedDict";
  }
 
  static bool is_consensus_func(const std::string &name)
  {
    return consensus_func_to_type().find(name) !=
           consensus_func_to_type().end();
  }
 
  static std::string get_type_from_consensus_func(const std::string &name)
  {
    if (!is_consensus_func(name))
      return std::string();
    return consensus_func_to_type().at(name);
  }

  static bool is_nondet_collection_builder(const std::string &name)
  {
    return name.rfind("_nondet_list_", 0) == 0 ||
           (name.rfind("_nondet_dict_", 0) == 0 && name != "_nondet_dict_size");
  }
 
  static bool is_python_model_func(const std::string &name)
  {
    return (
      name == "ESBMC_range_next_" || name == "ESBMC_range_has_next_" ||
      name == "bit_length" || name == "conjugate" || name == "from_bytes" ||
      name == "to_bytes" || name == "randint" || name == "random" ||
      name == "all" || is_nondet_collection_builder(name));
  }
 
  static bool is_python_exceptions(const std::string &name)
  {
    static const std::unordered_set<std::string> exceptions = {
      "BaseException",     "Exception",
      "ValueError",        "TypeError",
      "AttributeError",    "IndexError",
      "KeyError",          "ZeroDivisionError",
      "OverflowError",     "AssertionError",
      "NameError",         "OSError",
      "FileNotFoundError", "FileExistsError",
      "PermissionError",   "NotImplementedError",
      "ImportError",       "ModuleNotFoundError",
      "RuntimeError",      "StopIteration",
      "EOFError",          "UnboundLocalError",
      "ArithmeticError",   "FloatingPointError",
      "LookupError"};
    return exceptions.count(name) != 0;
  }
 
  static bool is_c_model_func(const std::string &func_name)
  {
    return func_name == "ceil" || func_name == "floor" || func_name == "fabs" ||
           func_name == "sin" || func_name == "cos" || func_name == "exp" ||
           func_name == "fmod" || func_name == "sqrt" || func_name == "fmin" ||
           func_name == "fmax" || func_name == "trunc" ||
           func_name == "round" || func_name == "copysign" ||
           func_name == "arctan" || func_name == "arccos" ||
           func_name == "dot" || func_name == "add" ||
           func_name == "subtract" || func_name == "multiply" ||
           func_name == "divide" || func_name == "transpose" ||
           func_name == "det" || func_name == "matmul" || func_name == "pow" ||
           func_name == "log" || func_name == "pow_by_squaring" ||
           func_name == "log2" || func_name == "log1p_taylor" ||
           func_name == "ldexp" || func_name == "__ESBMC_sin" ||
           func_name == "__ESBMC_cos" || func_name == "__ESBMC_sqrt" ||
           func_name == "__ESBMC_exp" || func_name == "__ESBMC_log";
  }
 
  static bool is_ordered_comparison(const std::string &op)
  {
    return op == "Lt" || op == "Gt" || op == "LtE" || op == "GtE";
  }
 
  static bool is_relational_op(const std::string &op)
  {
    return (
      op == "Eq" || op == "Lt" || op == "LtE" || op == "NotEq" || op == "Gt" ||
      op == "GtE" || op == "And" || op == "Or");
  }
 
  // Encapsulated accessors for the irep string attributes the Python
  // frontend attaches to legacy typet nodes. These attributes are read by
  // shared/downstream passes — "#cpp_type" by clang_cpp_adjust, the C/C++
  // pretty-printers and goto2c; "#member_name" by the shared clang-cpp pass
  // — so they must stay on the legacy node at the migrate seam. Funnelling
  // every raw .set/.get("#…") through one seam each is the Phase 4.1
  // hardening step of the IREP2 migration (docs/roadmap/irep2-migration.md Part
  // IV, F-P5 / §15). Keep the keys and values byte-identical: this is a
  // behaviour-preserving relocation, not a semantic change.
  static void set_cpp_type(typet &t, const irep_idt &value)
  {
    t.cpp_type(value);
  }
 
  static irep_idt get_cpp_type(const typet &t)
  {
    return t.cpp_type();
  }
 
  static void set_member_name(typet &t, const irep_idt &value)
  {
    t.member_name(value);
  }
 
  static void remove_member_name(typet &t)
  {
    t.remove_member_name();
  }
 
  // A scalar T whose `Optional[T]` is the Optional<T> struct, not a T*.
  static bool is_optional_scalar(const typet &t)
  {
    return t == long_long_int_type() || t == long_long_uint_type() ||
           t == double_type() || t == bool_type();
  }
 
  // The Optional<T> struct type_handler::build_optional_type makes.
  static bool is_optional_struct(const typet &t)
  {
    return t.is_struct() &&
           to_struct_type(t).tag().as_string().starts_with("tag-Optional_");
  }
 
  // Optional[str]: a pointer to an unsized char array, NULL for None.
  static bool is_optional_str_pointer(const typet &t)
  {
    return t.is_pointer() && t.subtype().is_array() &&
           t.subtype().subtype() == char_type() &&
           to_array_type(t.subtype()).size().is_zero();
  }
 
  static bool is_char_type(const typet &t)
  {
    return (t.is_signedbv() || t.is_unsignedbv()) && get_cpp_type(t) == "char";
  }
 
  // Distinguishes a `bytes` value from a numpy-style numeric array, so `+`
  // routes to concatenation only for the former. Both share the same legacy
  // `array of long_long_int_type` representation here
  // (type_handler::get_typet's "bytes" branch).
  static bool is_bytes_array(const typet &t)
  {
    return t.is_array() && get_cpp_type(t) == "bytes";
  }
 
  static bool is_float_vs_char(const exprt &a, const exprt &b)
  {
    const auto &type_a = a.type();
    const auto &type_b = b.type();
    return (type_a.is_floatbv() && is_char_type(type_b)) ||
           (type_b.is_floatbv() && is_char_type(type_a));
  }
 
  static std::string remove_quotes(const std::string &str)
  {
    if (str.length() < 2)
      return str;
 
    // Check for single quotes
    if (str.front() == '\'' && str.back() == '\'')
      return str.substr(1, str.length() - 2);
 
    // Check for double quotes
    if (str.front() == '"' && str.back() == '"')
      return str.substr(1, str.length() - 2);
 
    // No quotes found, return original string
    return str;
  }
 
  // Select widest type from flags based on hierarchy: float > int > bool
  static typet
  select_widest_type(const TypeFlags &flags, const typet &default_type)
  {
    // A member outside the float/int/bool hierarchy has no place in it, so
    // widening would pick a scalar for a union that is not one (#7872).
    if (flags.has_other)
      return default_type;
 
    if (flags.has_float)
      return double_type();
    if (flags.has_int)
      return long_long_int_type();
    if (flags.has_bool)
      return bool_type();
 
    return default_type;
  }
 
  // Extract type flags from Union annotation slice
  static TypeFlags extract_union_types(const nlohmann::json &slice)
  {
    TypeFlags flags;
 
    if (slice["_type"] == "Tuple" && slice.contains("elts"))
    {
      for (const auto &elem : slice["elts"])
        update_type_flags_from_node(elem, flags);
    }
 
    return flags;
  }
 
  // Extract type flags from PEP 604 union syntax: int | bool
  static TypeFlags extract_binop_union_types(const nlohmann::json &binop_node)
  {
    TypeFlags flags;
 
    // Extract from left operand. `|` is left-associative, so a chained union
    // nests on the left: `int | bool | float` is
    // BinOp(BinOp(int, bool), float).
    if (binop_node.contains("left"))
    {
      const auto &left = binop_node["left"];
      if (left["_type"] == "BinOp")
        merge_type_flags(flags, extract_binop_union_types(left));
      else
        update_type_flags_from_node(left, flags);
    }
 
    // Extract from right operand (may be nested BinOp for chained unions)
    if (binop_node.contains("right"))
    {
      const auto &right = binop_node["right"];
      if (right["_type"] == "BinOp")
      {
        // Recursively handle chained unions: int | bool | float
        TypeFlags right_flags = extract_binop_union_types(right);
        merge_type_flags(flags, right_flags);
      }
      else
        update_type_flags_from_node(right, flags);
    }
 
    return flags;
  }
 
  // Whether an annotation spells a union with None (`T | None`,
  // `Union[T, None]`).
  static bool annotation_admits_none(const nlohmann::json &ann)
  {
    if (!ann.is_object())
      return false;
    if (ann.value("_type", "") == "BinOp")
      return type_utils::extract_binop_union_types(ann).has_none;
    if (
      ann.value("_type", "") != "Subscript" ||
      ann["value"].value("id", "") != "Union")
      return false;
    const nlohmann::json &slice = ann["slice"];
    for (const auto &elt : slice.value("elts", nlohmann::json::array()))
      if (elt.value("_type", "") == "Constant" && elt["value"].is_null())
        return true;
    return false;
  }
 
  static bool is_integer_type(const typet &type)
  {
    return type.is_signedbv() || type.is_unsignedbv();
  }

  static bool is_numpy_string_array(const typet &type)
  {
    if (!type.is_array() || !type.subtype().is_array())
      return false;
    return type.subtype().subtype() == char_type() ||
           is_numpy_string_array(type.subtype());
  }

  static typet array_scalar_type(const typet &type)
  {
    typet scalar = type;
    while (scalar.is_array())
      scalar = scalar.subtype();
    return scalar;
  }

  static bool is_numpy_complex_array(const typet &type)
  {
    return type.is_array() && is_complex_type(array_scalar_type(type));
  }
 
  static bool is_string_type(const typet &type)
  {
    // String types are represented as arrays or pointers to char
    if (type.is_array() && type.subtype() == char_type())
      return true;
 
    if (type.is_pointer())
    {
      const typet &subtype = type.subtype();
      // Direct pointer to char: char*
      if (subtype == char_type())
        return true;
      // Pointer to char array: char(*)[N] (string literals)
      if (subtype.is_array() && subtype.subtype() == char_type())
        return true;
    }
 
    return false;
  }
 
  static bool is_dict_subscript(const nlohmann::json &element)
  {
    return element.contains("_type") && element["_type"] == "Subscript" &&
           element.contains("value");
  }
 
  static inline bool is_type_identifier(const std::string &name)
  {
    static const std::unordered_set<std::string> type_identifiers = {
      "int",
      "float",
      "str",
      "bool",
      "bytes",
      "list",
      "set",
      "tuple",
      "type",
      "object",
      "complex",
      "frozenset",
      "NoneType"};
    return type_identifiers.find(name) != type_identifiers.end();
  }

  static bool strip_pep515_underscores(const std::string &s, std::string &out)
  {
    out.clear();
    out.reserve(s.size());
    for (std::size_t i = 0; i < s.size(); i++)
    {
      if (s[i] != '_')
      {
        out.push_back(s[i]);
        continue;
      }
      const bool between_digits =
        i > 0 && i + 1 < s.size() &&
        isdigit(static_cast<unsigned char>(s[i - 1])) &&
        isdigit(static_cast<unsigned char>(s[i + 1]));
      if (!between_digits)
        return false;
    }
    return true;
  }
 
private:
  static void
  update_type_flags_from_node(const nlohmann::json &node, TypeFlags &flags)
  {
    if (node["_type"] == "Name" && node.contains("id"))
    {
      const std::string type_str = node["id"].get<std::string>();
      if (type_str == "float")
        flags.has_float = true;
      else if (type_str == "int")
        flags.has_int = true;
      else if (type_str == "bool")
        flags.has_bool = true;
      else if (type_str == "None" || type_str == "NoneType")
        flags.has_none = true;
      else
        flags.has_other = true;
    }
    else if (
      node["_type"] == "Constant" && node.contains("value") &&
      node["value"].is_null())
    {
      flags.has_none = true;
    }
    else
      flags.has_other = true;
  }
 
  static void merge_type_flags(TypeFlags &dest, const TypeFlags &src)
  {
    dest.has_float = dest.has_float || src.has_float;
    dest.has_int = dest.has_int || src.has_int;
    dest.has_bool = dest.has_bool || src.has_bool;
    dest.has_none = dest.has_none || src.has_none;
    dest.has_other = dest.has_other || src.has_other;
  }
 
  static const std::map<std::string, std::string> &consensus_func_to_type()
  {
    // hash() -> bytes (Bytes32), matching models/consensus.py's real
    // signature -- not the real Python builtin's int.
    static const std::map<std::string, std::string> func_to_type = {
      {"hash", "bytes"}};
    return func_to_type;
  }
};