Add output_json to the dependence_graph abstract domain.

Author: martin

src/analyses/dependence_graph.cpp

@@ -11,6 +11,8 @@ Date: August 2013
 
 #include <cassert>
 
+#include <util/json.h>
+
 #include "goto_rw.h"
 
 #include "dependence_graph.h"
@@ -329,6 +331,54 @@ void dep_graph_domaint::output(
   }
 }
 
+/*******************************************************************\
+
+Function: dep_graph_domaint::output_json
+
+  Inputs: The abstract interpreter and the namespace.
+
+ Outputs: The domain, formatted as a JSON object.
+
+ Purpose: Outputs the current value of the domain.
+
+\*******************************************************************/
+
+
+jsont dep_graph_domaint::output_json(
+  const ai_baset &ai,
+  const namespacet &ns) const
+{
+  json_arrayt graph;
+
+  for(dep_graph_domaint::depst::const_iterator cdi=control_deps.begin();
+      cdi!=control_deps.end();
+      ++cdi)
+  {
+    json_objectt &link=graph.push_back().make_object();
+    link["location_number"]=
+      json_numbert(std::to_string((*cdi)->location_number));
+    link["source_location"]=
+      json_stringt((*cdi)->source_location.as_string());
+    link["type"]=json_stringt("control");
+  }
+
+  for(dep_graph_domaint::depst::const_iterator ddi=data_deps.begin();
+      ddi!=data_deps.end();
+      ++ddi)
+  {
+    json_objectt &link=graph.push_back().make_object();
+    link["location_number"]=
+      json_numbert(std::to_string((*ddi)->location_number));
+    link["source_location"]=
+      json_stringt((*ddi)->source_location.as_string());
+    link["type"]=json_stringt("data");
+  }
+
+  return graph;
+}
+
+
+
 /*******************************************************************\
 
 Function: dependence_grapht::add_dep

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -179,6 +179,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   options.set_option("text", false);
   options.set_option("json", false);
   options.set_option("xml", false);
+  options.set_option("dot", false);
   options.set_option("outfile", "-");
 
   if(cmdline.isset("text"))
@@ -196,6 +197,11 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("xml", true);
     options.set_option("outfile", cmdline.get_value("xml"));
   }
+  else if (cmdline.isset("dot"))
+  {
+    options.set_option("dot", true);
+    options.set_option("outfile", cmdline.get_value("dot"));
+  }
   else
   {
     options.set_option("text", true);
@@ -250,6 +256,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   options.set_option("constants", false);
   options.set_option("intervals", false);
   options.set_option("non-null", false);
+  options.set_option("dependence-graph", false);
 
   if(cmdline.isset("intervals") ||
      cmdline.isset("show-intervals"))
@@ -259,10 +266,13 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("non-null", true);
   else if(cmdline.isset("constants"))
     options.set_option("constants", true);
-
-  if(!(options.get_bool_option("constants")  ||
-     options.get_bool_option("intervals")  ||
-     options.get_bool_option("non-null")))
+  else if (cmdline.isset("dependence-graph"))
+    options.set_option("dependence-graph", true);
+    
+  if (!(options.get_bool_option("constants")  ||
+        options.get_bool_option("intervals")  ||
+        options.get_bool_option("non-null") ||
+        options.get_bool_option("dependence-graph")))
   {
     status() << "Domain defaults to --constants" << eom;
     options.set_option("constants", true);
@@ -616,11 +626,13 @@ void goto_analyzer_parse_optionst::help()
     " --constants                  constant abstraction\n"
     " --intervals                  interval abstraction\n"
     " --non-null                   non-null abstraction\n"
+    " --dependence-graph           dependency relation between instructions\n"
     "\n"
     "Output options:\n"
     " --text file_name             output results in plain text to given file\n"
     " --json file_name             output results in JSON format to given file\n"
     " --xml file_name              output results in XML format to given file\n"
+    " --dot file_name              output results in DOT format to given file\n"
     "\n"
     "Other analyses:\n"
     " --taint file_name            perform taint analysis using rules in given file\n"

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -33,12 +33,13 @@ class optionst;
   "(gcc)(arch):" \
   "(taint):(show-taint)" \
   "(show-local-may-alias)" \
-  "(json):(xml):(text):" \
+  "(json):(xml):(text):(dot):" \
   "(unreachable-instructions)" \
   "(intervals)(show-intervals)" \
   "(non-null)(show-non-null)" \
   "(constants)" \
-  "(show)(verify)(simplify):" \
+  "(dependence-graph)" \
+  "(show)(verify)(simplify):"			\
   "(flow-sensitive)(concurrent)"
 
 class goto_analyzer_parse_optionst:

src/goto-analyzer/static_show_domain.cpp

@@ -14,6 +14,7 @@ Author: Martin Brain, [email protected]
 
 #include <analyses/interval_domain.h>
 #include <analyses/constant_propagator.h>
+#include <analyses/dependence_graph.h>
 
 #include "static_show_domain.h"
 
@@ -36,18 +37,23 @@ bool static_show_domain(
   message_handlert &message_handler,
   std::ostream &out)
 {
-  ai_baset *domain=NULL;
-
+  ai_baset *domain = NULL;
+  namespacet ns(goto_model.symbol_table);
+  
   if(options.get_bool_option("flow-sensitive"))
   {
     if(options.get_bool_option("constants"))
-      domain=new ait<constant_propagator_domaint>();
+      domain = new ait<constant_propagator_domaint>();
 
     else if(options.get_bool_option("intervals"))
-      domain=new ait<interval_domaint>();
+      domain = new ait<interval_domaint>();
+
+    //else if(options.get_bool_option("non-null"))
+    //  domain = new ait<non_null_domaint>();
+
+    else if(options.get_bool_option("dependence-graph"))
+      domain = new dependence_grapht(ns);
 
-    // else if(options.get_bool_option("non-null"))
-    //   domain=new ait<non_null_domaint>();
   }
   else if(options.get_bool_option("concurrent"))
   {
@@ -75,10 +81,20 @@ bool static_show_domain(
   // status() << "Performing analysis" << eom;
   (*domain)(goto_model);
 
+
   if(options.get_bool_option("json"))
     out << domain->output_json(goto_model);
   else if(options.get_bool_option("xml"))
     out << domain->output_xml(goto_model);
+  else if(options.get_bool_option("dot") && options.get_bool_option("dependence-graph"))
+  {
+    dependence_grapht *d = dynamic_cast<dependence_grapht*>(domain);
+    assert(d != NULL);
+
+    out << "digraph g {\n";
+    d->output_dot(out);
+    out << "}\n";
+  }
   else
     domain->output(goto_model, out);