Add support for generating the dependency graph to goto-analyze, including dot format.

Author: martin

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -227,6 +227,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"))
@@ -244,6 +245,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);
@@ -298,6 +304,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")) 
@@ -307,10 +314,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);
+  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("non-null") ||
+	options.get_bool_option("dependence-graph")))
   {
     status() << "Domain defaults to --constants" << eom;
     options.set_option("constants", true);
@@ -661,11 +671,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, martin.brain@cs.ox.ac.uk
 
 #include <analyses/interval_domain.h>
 #include <analyses/constant_propagator.h>
+#include <analyses/dependence_graph.h>
 
 #include "static_show_domain.h"
 
@@ -37,6 +38,7 @@ bool static_show_domain(
   std::ostream &out)
 {
   ai_baset *domain = NULL;
+  namespacet ns(goto_model.symbol_table);
 
   if (options.get_bool_option("flow-sensitive"))
   {
@@ -48,7 +50,10 @@ bool static_show_domain(
 
     //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("concurrent"))
   {
@@ -75,10 +80,18 @@ 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);
+
+    d->output_dot(out);
+  }
   else
     domain->output(goto_model, out);