dot.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Dump Goto-Program as DOT Graph
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#include "dot.h"
 
#include <sstream>
 
#include <goto-programs/goto_model.h>
 
#include <langapi/language_util.h>
 
#define DOTGRAPHSETTINGS  "color=black;" \
                          "orientation=portrait;" \
                          "fontsize=20;"\
                          "compound=true;"\
                          "size=\"30,40\";"\
                          "ratio=compress;"
 
class dott
{
public:
  explicit dott(
    const goto_modelt &_goto_model):
    goto_model(_goto_model),
    subgraphscount(0)
  {
  }
 
  void output(std::ostream &out);
 
protected:
  const goto_modelt &goto_model;
 
  unsigned subgraphscount;
 
  std::list<std::pair<std::string, exprt>> function_calls;
  std::list<exprt> clusters;
 
  void
  write_dot_subgraph(std::ostream &, const irep_idt &, const goto_programt &);
 
  void do_dot_function_calls(std::ostream &);
 
  std::string &escape(std::string &str);
 
  void write_edge(std::ostream &,
                  const goto_programt::instructiont &,
                  const goto_programt::instructiont &,
                  const std::string &);
 
  void find_next(
    const goto_programt::instructionst &,
    const goto_programt::const_targett &,
    std::set<goto_programt::const_targett, goto_programt::target_less_than> &,
    std::set<goto_programt::const_targett, goto_programt::target_less_than> &);
};
 
void dott::write_dot_subgraph(
  std::ostream &out,
  const irep_idt &function_id,
  const goto_programt &goto_program)
{
  clusters.push_back(exprt("cluster"));
  clusters.back().set("name", function_id);
  clusters.back().set("nr", subgraphscount);
 
  out << "subgraph \"cluster_" << function_id << "\" {\n";
  out << "label=\"" << function_id << "\";\n";
 
  const goto_programt::instructionst &instructions =
    goto_program.instructions;
 
  if(instructions.empty())
  {
    out << "Node_" << subgraphscount << "_0 " <<
      "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
  }
  else
  {
    const namespacet ns(goto_model.symbol_table);
 
    std::set<goto_programt::const_targett, goto_programt::target_less_than>
      seen;
    goto_programt::const_targetst worklist;
    worklist.push_back(instructions.begin());
 
    while(!worklist.empty())
    {
      goto_programt::const_targett it=worklist.front();
      worklist.pop_front();
 
      if(it==instructions.end() ||
         seen.find(it)!=seen.end()) continue;
 
      std::stringstream tmp;
      if(it->is_goto())
      {
        if(it->condition().is_true())
          tmp.str("Goto");
        else
        {
          std::string t = from_expr(ns, function_id, it->condition());
          while(t[ t.size()-1 ]=='\n')
            t = t.substr(0, t.size()-1);
          tmp << escape(t) << "?";
        }
      }
      else if(it->is_assume())
      {
        std::string t = from_expr(ns, function_id, it->condition());
        while(t[ t.size()-1 ]=='\n')
          t = t.substr(0, t.size()-1);
        tmp << "Assume\\n(" << escape(t) << ")";
      }
      else if(it->is_assert())
      {
        std::string t = from_expr(ns, function_id, it->condition());
        while(t[ t.size()-1 ]=='\n')
          t = t.substr(0, t.size()-1);
        tmp << "Assert\\n(" << escape(t) << ")";
      }
      else if(it->is_skip())
        tmp.str("Skip");
      else if(it->is_end_function())
        tmp.str("End of Function");
      else if(it->is_location())
        tmp.str("Location");
      else if(it->is_dead())
        tmp.str("Dead");
      else if(it->is_atomic_begin())
        tmp.str("Atomic Begin");
      else if(it->is_atomic_end())
        tmp.str("Atomic End");
      else if(it->is_function_call())
      {
        const code_function_callt function_call(
          it->call_lhs(), it->call_function(), it->call_arguments());
        std::string t = from_expr(ns, function_id, function_call);
        while(t[ t.size()-1 ]=='\n')
          t = t.substr(0, t.size()-1);
        tmp.str(escape(t));
 
        std::stringstream ss;
        ss << "Node_" << subgraphscount << "_" << it->location_number;
        function_calls.push_back(
          std::pair<std::string, exprt>(ss.str(), it->call_function()));
      }
      else if(
        it->is_assign() || it->is_decl() || it->is_set_return_value() ||
        it->is_other())
      {
        std::string t = from_expr(ns, function_id, it->code());
        while(t[ t.size()-1 ]=='\n')
          t = t.substr(0, t.size()-1);
        tmp.str(escape(t));
      }
      else if(it->is_start_thread())
        tmp.str("Start of Thread");
      else if(it->is_end_thread())
        tmp.str("End of Thread");
      else if(it->is_throw())
        tmp.str("THROW");
      else if(it->is_catch())
        tmp.str("CATCH");
      else
        tmp.str("UNKNOWN");
 
      out << "Node_" << subgraphscount << "_" << it->location_number;
      out << " [shape=";
      if(it->is_goto() && !it->condition().is_constant())
        out << "diamond";
      else
        out <<"Mrecord";
      out << ",fontsize=22,label=\"";
      out << tmp.str();
      out << "\"];\n";
 
      std::set<goto_programt::const_targett, goto_programt::target_less_than>
        tres;
      std::set<goto_programt::const_targett, goto_programt::target_less_than>
        fres;
      find_next(instructions, it, tres, fres);
 
      std::string tlabel;
      std::string flabel;
      if(!fres.empty() && !tres.empty())
      {
        tlabel = "true";
        flabel = "false";
      }
 
      typedef std::
        set<goto_programt::const_targett, goto_programt::target_less_than>
          t;
 
      for(t::iterator trit=tres.begin();
           trit!=tres.end();
           trit++)
        write_edge(out, *it, **trit, tlabel);
      for(t::iterator frit=fres.begin();
          frit!=fres.end();
          frit++)
        write_edge(out, *it, **frit, flabel);
 
      seen.insert(it);
      const auto temp=goto_program.get_successors(it);
      worklist.insert(worklist.end(), temp.begin(), temp.end());
    }
  }
 
  out << "}\n";
  subgraphscount++;
}
 
void dott::do_dot_function_calls(
  std::ostream &out)
{
  for(const auto &call : function_calls)
  {
    std::list<exprt>::const_iterator cit=clusters.begin();
    for( ; cit!=clusters.end(); cit++)
      if(cit->get("name") == call.second.get(ID_identifier))
        break;
 
    if(cit!=clusters.end())
    {
      out << call.first
          << " -> "
             "Node_"
          << cit->get("nr") << "_0"
          << " [lhead=\"cluster_" << call.second.get(ID_identifier) << "\","
          << "color=blue];\n";
    }
    else
    {
      out << "subgraph \"cluster_" << call.second.get(ID_identifier)
          << "\" {\n";
      out << "rank=sink;\n";
      out << "label=\"" << call.second.get(ID_identifier) << "\";\n";
      out << "Node_" << subgraphscount << "_0 " <<
        "[shape=Mrecord,fontsize=22,label=\"?\"];\n";
      out << "}\n";
      clusters.push_back(exprt("cluster"));
      clusters.back().set("name", call.second.get(ID_identifier));
      clusters.back().set("nr", subgraphscount);
      out << call.first
          << " -> "
             "Node_"
          << subgraphscount << "_0"
          << " [lhead=\"cluster_" << call.second.get("identifier") << "\","
          << "color=blue];\n";
      subgraphscount++;
    }
  }
}
 
void dott::output(std::ostream &out)
{
  out << "digraph G {\n";
  out << DOTGRAPHSETTINGS << '\n';
 
  for(const auto &gf_entry : goto_model.goto_functions.function_map)
  {
    if(gf_entry.second.body_available())
      write_dot_subgraph(out, gf_entry.first, gf_entry.second.body);
  }
 
  do_dot_function_calls(out);
 
  out << "}\n";
}
 
std::string &dott::escape(std::string &str)
{
  for(std::string::size_type i=0; i<str.size(); i++)
  {
    if(str[i]=='\n')
    {
      str[i] = 'n';
      str.insert(i, "\\");
    }
    else if(str[i]=='\"' ||
            str[i]=='|' ||
            str[i]=='\\' ||
            str[i]=='>' ||
            str[i]=='<' ||
            str[i]=='{' ||
            str[i]=='}')
    {
      str.insert(i, "\\");
      i++;
    }
  }
 
  return str;
}
 
void dott::find_next(
  const goto_programt::instructionst &instructions,
  const goto_programt::const_targett &it,
  std::set<goto_programt::const_targett, goto_programt::target_less_than> &tres,
  std::set<goto_programt::const_targett, goto_programt::target_less_than> &fres)
{
  if(it->is_goto() && !it->condition().is_false())
  {
    for(const auto &target : it->targets)
      tres.insert(target);
  }
 
  if(it->is_goto() && it->condition().is_true())
    return;
 
  goto_programt::const_targett next = it; next++;
  if(next!=instructions.end())
    fres.insert(next);
}
 
void dott::write_edge(
  std::ostream &out,
  const goto_programt::instructiont &from,
  const goto_programt::instructiont &to,
  const std::string &label)
{
  out << "Node_" << subgraphscount << "_" << from.location_number;
  out << " -> ";
  out << "Node_" << subgraphscount << "_" << to.location_number << " ";
  if(!label.empty())
  {
    out << "[fontsize=20,label=\"" << label << "\"";
    if(from.is_backwards_goto() && from.location_number > to.location_number)
      out << ",color=red";
    out << "]";
  }
  out << ";\n";
}
 
void dot(const goto_modelt &src, std::ostream &out)
{
  dott dot(src);
  dot.output(out);
}