Merge pull request diffblue#538 from diffblue/smowton/cleanup/goto-binary-save-routine

Cleanup: separate GOTO binary postprocessing from saving

Author: smowton

src/taint-analysis/taint_security_scanner.cpp

@@ -180,9 +180,7 @@ bool taint_do_security_scan(
        "INSTRUMENTER")
         .native(),
       statistics,
-      logger,
-      config.is_html_dump_of_instrumented_program_enabled(),
-      config.is_string_refinement_enabled());
+      logger);
     instrumentation_driver.run(
       config.use_data_flow_insensitive_instrumentation());
 

src/taint-instrumenter/instrumentation_driver.cpp

@@ -6,10 +6,13 @@
 
 #include <algorithm>
 #include <fstream>
+
+#include <goto-programs/goto_statistics.h>
+#include <goto-programs/write_goto_binary.h>
 #include <summaries/summary_dump.h>
 #include <taint-instrumenter/instrumentation_driver.h>
 #include <taint-instrumenter/instrumentation_props.h>
-#include <taint-instrumenter/instrumented_goto_binary_builder.h>
+#include <taint-instrumenter/postprocess_instrumented_goto_model.h>
 #include <taint-instrumenter/instrumenter.h>
 #include <taint-instrumenter/search_for_rule_applications.h>
 #include <util/file_util.h>
@@ -24,24 +27,117 @@ taint_instrumentation_drivert::taint_instrumentation_drivert(
   const boost::filesystem::path &results_dir,
   const boost::filesystem::path &temp_dir,
   taint_statisticst &statistics,
-  messaget &logger,
-  const bool perform_html_dump,
-  const bool string_refinement_enabled)
+  messaget &logger)
   : program(program),
     summaries(summaries),
     tokens_propagation_graph(tokens_propagation_graph),
     // , timeout(timeout)
     results_dir(results_dir),
     temp_dir(temp_dir),
     statistics(statistics),
-    logger(logger),
-    perform_html_dump(perform_html_dump),
-    string_refinement_enabled(string_refinement_enabled)
+    logger(logger)
 {
   boost::filesystem::create_directory(this->results_dir);
   boost::filesystem::create_directory(this->temp_dir);
 }
 
+static void save_goto_binary(
+  goto_modelt &instrumented_goto_model,
+  const boost::filesystem::path &binary_path,
+  messaget &logger)
+{
+  logger.status() << "  Saving the goto model as goto binary to disk."
+                  << messaget::eom;
+
+  // Finally save the constructed goto_model on the disc as GOTO binary.
+  const bool fail = write_goto_binary(
+    binary_path.native(), instrumented_goto_model, logger.get_message_handler());
+  INVARIANT(!fail, "write_goto_binary should always succeed");
+
+  logger.status() << "  Saving statistics of the saved the goto program."
+                  << messaget::eom;
+
+  // We compute and save basic statistics of the saved
+  // GOTO program (i.e. the GOTO binary). 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.
+
+  auto out_json_file_pathname = binary_path;
+  out_json_file_pathname.replace_extension("stats.json");
+
+  // We start with safety check related to the file to be written.
+  bool can_write_stats = true;
+  if(boost::filesystem::is_directory(out_json_file_pathname))
+  {
+    logger.error()
+      << "The path-name '" << out_json_file_pathname.native()
+      << "' for the statistics JSON output is actually an existing "
+      << "directory." << messaget::eom;
+    can_write_stats = false;
+  }
+  if(can_write_stats)
+  {
+    // And let's compute and save the statistics.
+    goto_statisticst stats;
+    stats.extend(instrumented_goto_model);
+    std::ofstream ofile(out_json_file_pathname.native());
+    if(!ofile)
+    {
+      logger.error()
+        << "Failed to open the JSON file '"
+        << out_json_file_pathname.native()
+        << "' for writing. The statistic of the GOTO program won't be "
+        << "available." << messaget::eom;
+    }
+    else
+      ofile << to_json(stats);
+  }
+}
+
+static void save_goto_binary_description(
+  const taint_instrumentation_propst &props,
+  const boost::filesystem::path &output_path,
+  const boost::filesystem::path &goto_binary_path)
+{
+  // Now we collect sink locations. This is necessary in subsequent phases
+  // of the whole analysis. Namely, for recognition which error traces should
+  // be considered and which discarded.
+
+  json_objectt binary_description;
+  binary_description["goto_binary_file"] =
+    json_stringt(goto_binary_path.native());
+
+  json_arrayt jsinks;
+  typedef std::tuple<irep_idt, irep_idt, irep_idt> sink_loct;
+  std::set<sink_loct> seen_sinks;
+
+  for(const auto loc_id : props.get_sinks())
+  {
+    const auto &loc = props.get_location_props()
+      .at(loc_id)
+      .get_instruction_id()
+      ->source_location;
+
+    if(seen_sinks.insert(
+         sink_loct{loc.get_file(), loc.get_function(), loc.get_line()}).second)
+    {
+      json_objectt jloc;
+      jloc["file"] = json_stringt(id2string(loc.get_file()));
+      jloc["function"] = json_stringt(id2string(loc.get_function()));
+      jloc["line"] = json_numbert(id2string(loc.get_line()));
+
+      jsinks.push_back(jloc);
+    }
+  }
+
+  binary_description["sinks"] = jsinks;
+
+  std::ofstream ostr(output_path.native());
+  ostr << binary_description;
+}
+
+
 void taint_instrumentation_drivert::run(
   const bool use_data_flow_insensitive_instrumentation)
 {
@@ -108,33 +204,29 @@ void taint_instrumentation_drivert::run(
   statistics.end_instrumenter();
   statistics.begin_instrumented_goto_binary_build();
 
-  logger.status() << "  Starting the builder of the instrumented GOTO binary."
+  logger.status() << "  Post-processing the instrumented model"
                   << messaget::eom;
 
-  const std::pair<taint_instrumented_goto_binary_infot, std::string>
-    task_valid = build_instrumented_goto_binary(
-      instrumentation_props,
-      instrumenter,
-      results_dir,
-      instrumented_goto_model,
-      program,
-      statistics,
-      logger,
-      perform_html_dump,
-      string_refinement_enabled);
-  if(task_valid.second.empty())
-  {
-    logger.status() << "  Saving info JSON file about the saved GOTO binary."
-                    << messaget::eom;
+  postprocess_instrumented_goto_model(
+    instrumentation_props,
+    instrumenter,
+    instrumented_goto_model,
+    program,
+    logger);
 
-    json_objectt jtask;
-    dump_as_json(task_valid.first, jtask);
-    std::ofstream ostr(
-      (results_dir / "instrumented_goto_program.json").native());
-    ostr << jtask;
-  }
-  else
-    logger.status() << task_valid.second << messaget::eom;
+  logger.status() << "  Saving the instrumented model"
+                  << messaget::eom;
+
+  const auto binary_path = results_dir / "instrumented_goto_program.gbf";
+  save_goto_binary(instrumented_goto_model, binary_path, logger);
+
+  logger.status() << "  Saving info JSON file about the saved GOTO binary."
+                  << messaget::eom;
+
+  const auto binary_description_path =
+    results_dir / "instrumented_goto_program.json";
+  save_goto_binary_description(
+    instrumentation_props, binary_description_path, binary_path);
 
   statistics.end_instrumented_goto_binary_build();
 }

src/taint-instrumenter/instrumentation_driver.h

@@ -29,9 +29,7 @@ class taint_instrumentation_drivert
     const boost::filesystem::path &results_dir,
     const boost::filesystem::path &temp_dir,
     taint_statisticst &statistics,
-    messaget &logger,
-    const bool perform_html_dump,
-    const bool string_refinement_enabled);
+    messaget &logger);
 
   /// The method computes an instrumented GOTO program (referenced in the member
   /// `program`) The original GOTO program is NOT modified.
@@ -60,8 +58,6 @@ class taint_instrumentation_drivert
   boost::filesystem::path temp_dir;
   taint_statisticst &statistics;
   messaget &logger;
-  bool perform_html_dump;
-  bool string_refinement_enabled;
 };
 
 #endif