class_hierarchy.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Class Hierarchy
 
Author: Daniel Kroening
 
Date: April 2016
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H
#define CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H
 
#include <iosfwd>
#include <map>
#include <unordered_map>
 
#include <util/graph.h>
#include <util/irep.h>
 
#define OPT_SHOW_CLASS_HIERARCHY \
  "(show-class-hierarchy)"
 
#define HELP_SHOW_CLASS_HIERARCHY                                              \
  " {y--show-class-hierarchy} \t show the class hierarchy\n"
 
class symbol_table_baset;
class json_stream_arrayt;
class ui_message_handlert;
 
class class_hierarchyt
{
public:
  typedef std::vector<irep_idt> idst;
 
  class entryt
  {
  public:
    idst parents, children;
    bool is_abstract;
  };
 
  typedef std::map<irep_idt, entryt> class_mapt;
  class_mapt class_map;
 
  void operator()(const symbol_table_baset &);
 
  class_hierarchyt() = default;
  explicit class_hierarchyt(const symbol_table_baset &symbol_table)
  {
    (*this)(symbol_table);
  }
  class_hierarchyt(const class_hierarchyt &) = delete;
  class_hierarchyt &operator=(const class_hierarchyt &) = delete;
 
  // transitively gets all children
  idst get_children_trans(const irep_idt &id) const
  {
    idst result;
    get_children_trans_rec(id, result);
    return result;
  }
 
  // transitively gets all parents
  idst get_parents_trans(const irep_idt &id) const
  {
    idst result;
    get_parents_trans_rec(id, result);
    return result;
  }
 
  void output(std::ostream &, bool children_only) const;
  void output_dot(std::ostream &) const;
  void output(json_stream_arrayt &, bool children_only) const;
 
protected:
  void get_children_trans_rec(const irep_idt &, idst &) const;
  void get_parents_trans_rec(const irep_idt &, idst &) const;
};
 
class class_hierarchy_graph_nodet : public graph_nodet<empty_edget>
{
public:
  irep_idt class_identifier;
};
 
class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
{
public:
  typedef std::vector<irep_idt> idst;
 
  typedef std::unordered_map<irep_idt, node_indext> nodes_by_namet;
 
  void populate(const symbol_table_baset &);
 
  const nodes_by_namet &get_nodes_by_class_identifier() const
  {
    return nodes_by_name;
  }
 
  idst get_direct_children(const irep_idt &c) const;
 
  idst get_children_trans(const irep_idt &c) const;
 
  idst get_parents_trans(const irep_idt &c) const;
 
private:
  nodes_by_namet nodes_by_name;
 
  idst ids_from_indices(const std::vector<node_indext> &nodes) const;
 
  idst get_other_reachable_ids(const irep_idt &c, bool forwards) const;
};
 
void show_class_hierarchy(
  const class_hierarchyt &hierarchy,
  ui_message_handlert &message_handler,
  bool children_only = false);
 
#endif // CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H