Merge pull request diffblue#228 from diffblue/feature/dump_of_goto_stats_of_slicing_tasks

SEC-41 : Adding a use of statistics of GOTO program in security-analyser.

Author: marek-trtik

src/taint-slicer/slicing_tasks_builder.cpp

@@ -14,6 +14,7 @@
 #include <goto-programs/write_goto_binary.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_statistics.h>
 #include <java_bytecode/java_entry_point.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
@@ -324,7 +325,55 @@ std::pair<taint_slicing_taskt,std::string> build_slicing_task(
     if(fail)
       fail_message="Not available.";
     else
-      return {{props.get_root(),sink_locations,pathname},""};
+    {
+      // Before return we compute and same basic statistics of the saved
+      // GOTO program (i.e. the slicing task). These statistics will later
+      // be used by the Python driver script to compare them with similar
+      // statistics from the full slicer (implemented in goto-instrument)
+      // in order to get the efficiency of the slicing.
+
+      const std::string out_json_file_pathname=
+        fileutl_remove_extension(pathname) + ".stats.json";
+
+      // We start with safety check related to the file to be written.
+      bool can_write_stats=true;
+      if(fileutl_is_directory(out_json_file_pathname))
+      {
+        logger->error()
+          << "The path-name '"
+          << out_json_file_pathname
+          << "' for the statistics JSON output is actually an existing "
+          << "directory."
+          << messaget::eom;
+        can_write_stats=false;
+      }
+      if(fileutl_parse_extension_in_pathname(out_json_file_pathname)!=".json")
+      {
+        logger->error()
+          << "The file of the path-name '" << out_json_file_pathname
+          << "' for the statistics JSON output does not have '.json' extension."
+          << messaget::eom;
+        can_write_stats=false;
+      }
+      if(can_write_stats)
+      {
+        // And let's compute and save the statistics.
+        goto_statisticst stats;
+        stats.extend(goto_model);
+        std::ofstream ofile(out_json_file_pathname);
+        if(!ofile)
+        {
+          logger->error()
+            << "Failed to open the JSON file '" << out_json_file_pathname
+            << "' for writing. The statistic of the GOTO program won't be "
+            << "available."
+            << messaget::eom;
+        }
+        else
+          ofile << to_json(stats);
+      }
+      return {{props.get_root(), sink_locations, pathname}, ""};
+    }
   }
   catch(const std::exception &e)
   {