dynamic_type_handler.h

Go to the documentation of this file.

#pragma once
 
#include <util/irep/type.h>
#include <util/irep/expr.h>
#include <util/irep/std_code.h>
#include <util/irep/location.h>
#include <util/symtab/symbol.h>
#include <python-frontend/symbol_id.h>
#include <nlohmann/json.hpp>
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <vector>
 
class python_converter;
class type_handler;
 
class dynamic_type_handler
{
public:
  dynamic_type_handler(python_converter &converter, type_handler &type_handler);

  std::unordered_set<std::string>
  detect_dynamic_type_names(const nlohmann::json &if_node) const;

  void declare_dynamic_type_names(
    const std::unordered_set<std::string> &dynamic_type_names,
    const nlohmann::json &ast_node);

  bool is_tagged(const std::string &name) const;

  std::string tagged_symbol_id(const std::string &name) const;

  symbol_id bound_symbol_id(const std::string &name) const;

  bool tagged_binop_result_may_be_tagged(const std::string &op) const;

  void assign(
    const exprt &rhs,
    const locationt &location,
    const std::string &name,
    codet &target_block);

  void resolve_read(symbolt *&symbol) const;

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

  exprt handle_arithmetic(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs,
    const locationt &location);

  void guard_type_error(
    const std::string &op,
    const exprt &lhs,
    const exprt &rhs,
    const locationt &location);

  exprt build_neg_tagged(const exprt &tagged, const locationt &location);

  exprt build_isinstance_check(
    const exprt &tagged,
    const std::string &type_name,
    bool type_is_user_class) const;

  exprt build_truthiness(const exprt &tagged);

  bool detect_dynamic_return_type(const nlohmann::json &function_node) const;

  bool parameter_call_returns_tagged(const nlohmann::json &call) const;

  bool scope_assigns_divergent_literal_types(
    const std::string &name,
    const nlohmann::json &scope_body,
    const nlohmann::json &module_body = nlohmann::json()) const;

  exprt build_tagged_value(
    const exprt &value,
    const locationt &location,
    codet &target_block);

  exprt build_numeric_conversion(
    const exprt &tagged,
    const typet &result_type,
    const locationt &location);

  void refuse_float_tag_operation(const exprt &lhs, const exprt &rhs) const;

  [[noreturn]] void refuse_tagged_argument() const;

  void assign_tagged_object(
    const exprt &rhs,
    const locationt &location,
    const std::string &name,
    codet &target_block);

  class scope_guard
  {
  public:
    scope_guard(
      dynamic_type_handler &handler,
      const std::unordered_set<std::string> &dynamic_type_names);
    ~scope_guard();
 
  private:
    dynamic_type_handler &handler_;
    std::unordered_set<std::string> added_;
  };
 
private:
  std::vector<codet> build_tag_field_assigns(
    symbolt &tag_symbol,
    const exprt &rhs,
    const locationt &location);

  symbolt *find_tag_symbol(const std::string &name) const;

  bool joins_divergent_kinds(
    const std::string &name,
    std::unordered_set<std::string> &kinds,
    bool keeps_value) const;

  exprt build_literal_compare_call(
    const std::string &num_func_name,
    const std::string &str_func_name,
    const exprt &tagged,
    const exprt &literal);
 
  exprt build_eq_literal(const exprt &tagged, const exprt &literal);
  exprt build_ordered_literal(
    const std::string &op,
    const exprt &tagged,
    const exprt &literal);
  exprt
  build_ordered_obj(const std::string &op, const exprt &lhs, const exprt &rhs);
  exprt build_add_literal(
    const exprt &tagged,
    const exprt &literal,
    bool tagged_is_left);
  exprt build_sub_literal(
    const exprt &tagged,
    const exprt &literal,
    bool tagged_is_left);
  exprt build_div_literal(
    const exprt &tagged,
    const exprt &literal,
    bool tagged_is_left,
    const locationt &location);
  exprt build_add_tagged(const exprt &lhs, const exprt &rhs);
  exprt build_sub_tagged(const exprt &lhs, const exprt &rhs);
  exprt build_div_tagged(
    const exprt &lhs,
    const exprt &rhs,
    const locationt &location);

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

  void guard_zero_division(
    const exprt &divisor,
    const exprt &type_ok,
    const locationt &location);
 
  python_converter &converter_;
  type_handler &type_handler_;
 
  // Names of variables flagged as needing the tagged-object representation
  // for the duration of converting one if/else's branches.
  std::unordered_set<std::string> tagged_names_;
 
  // Original symbol id -> tagged-object symbol id, for a variable that
  // already had a native-typed symbol when it was flagged. Unlike the
  // straight-line retype heuristic's alias, never reverted: the whole
  // point is surviving the join.
  std::unordered_map<std::string, std::string> aliases_;
};