generic_parameter_specialization_map.h

Go to the documentation of this file.

 
#ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_H
#define CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_H
 
#include <stack>
#include <vector>
 
#include <util/string_utils.h>
 
#include "expr2java.h"
#include "java_types.h"

class generic_parameter_specialization_mapt
{
private:
  struct container_paramt
  {
    std::size_t container_index;
    std::size_t param_index;
  };

  std::unordered_map<irep_idt, container_paramt> param_to_container;
  std::vector<std::stack<std::vector<reference_typet>>>
    container_to_specializations;
 
public:
  std::size_t insert(
    const std::vector<java_generic_parametert> &parameters,
    std::vector<reference_typet> types);

  void pop(std::size_t container_index);

  std::optional<reference_typet> pop(const irep_idt &parameter_name);

  struct printert
  {
    const generic_parameter_specialization_mapt &map;
    const namespacet &ns;
 
    printert(
      const generic_parameter_specialization_mapt &map,
      const namespacet &ns)
      : map(map), ns(ns)
    {
    }
  };
 
  template <typename ostreamt>
  friend ostreamt &operator<<(ostreamt &stm, const printert &map);
};

template <typename ostreamt>
ostreamt &operator<<(
  ostreamt &stm,
  const generic_parameter_specialization_mapt::printert &map)
{
  if(map.map.container_to_specializations.empty())
    stm << "empty map";
  else
    stm << "map:\n";
  std::vector<std::vector<irep_idt>> container_to_params(
    map.map.container_to_specializations.size());
  for(const auto &elt : map.map.param_to_container)
  {
    std::vector<irep_idt> &params =
      container_to_params[elt.second.container_index];
    if(params.size() < elt.second.param_index + 1)
      params.resize(elt.second.param_index + 1);
    params[elt.second.param_index] = elt.first;
  }
  const namespacet &ns = map.ns;
  for(std::size_t index = 0; index < container_to_params.size(); ++index)
  {
    stm << "<";
    join_strings(
      stm,
      container_to_params.at(index).begin(),
      container_to_params.at(index).end(),
      ", ");
    stm << ">: ";
    std::stack<std::vector<reference_typet>> stack =
      map.map.container_to_specializations.at(index);
    while(!stack.empty())
    {
      stm << "<";
      join_strings(
        stm,
        stack.top().begin(),
        stack.top().end(),
        ", ",
        [&ns](const reference_typet &pointer_type) {
          if(is_java_generic_parameter(pointer_type))
          {
            return id2string(
              to_java_generic_parameter(pointer_type).get_name());
          }
          else
            return type2java(pointer_type, ns);
        });
      stm << ">, ";
      stack.pop();
    }
    stm << "\n";
  }
  return stm;
}
 
#endif // CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_H