Merge pull request diffblue#91 from diffblue/marek/enabling_slicer_PR

Enabling slicer.

Author: marek-trtik

src/Makefile

@@ -1,10 +1,12 @@
-DIRS = driver pointer-analysis summaries taint-analysis util
+DIRS = driver pointer-analysis summaries taint-analysis taint-slicer util
 
 all: driver.dir
 
-pointer-analysis.dir summaries.dir taint-analysis.dir: cbmc.dir
+pointer-analysis.dir summaries.dir taint-analysis.dir taint-slicer.dir: cbmc.dir
 
-driver.dir: cbmc.dir pointer-analysis.dir summaries.dir taint-analysis.dir util.dir
+driver.dir: cbmc.dir pointer-analysis.dir summaries.dir taint-analysis.dir \
+            taint-slicer.dir util.dir \
+            # No more directories
 
 # building for a particular directory
 
@@ -17,7 +19,8 @@ $(patsubst %, %.dir, $(DIRS)):
 cbmc.dir:
 	$(MAKE) $(MAKEARGS) -C ../cbmc/src \
     languages linking.dir big-int.dir goto-programs.dir analyses.dir \
-    pointer-analysis.dir langapi.dir json.dir assembler.dir util.dir miniz.dir
+    pointer-analysis.dir langapi.dir json.dir assembler.dir util.dir miniz.dir \
+    goto-instrument.dir cbmc.dir symex.dir
 
 # generate source files
 

src/driver/Makefile

@@ -17,6 +17,7 @@ OBJ += ../../cbmc/src/ansi-c/ansi-c$(LIBEXT) \
       ../pointer-analysis/sec_pointer_analysis$(LIBEXT) \
       ../taint-analysis/sec_taint_analysis$(LIBEXT) \
       ../util/sec_util$(LIBEXT) \
+      ../taint-slicer/taint-slicer$(LIBEXT) \
       # No more library files
 
 INCLUDES= -I .. \

src/taint-analysis/taint_security_scanner.cpp

@@ -22,11 +22,14 @@ The root module of the security scanner (a.k.a. the taint analyser).
 #include "taint_tokens_propagation_graph.h"
 #include "taint_summary_dump.h"
 #include "taint_statistics_dump.h"
+#include <taint-slicer/slicer.h>
 #include <util/config.h>
 #include <util/msgstream.h>
 #include <util/json_map_serializer.h>
 #include "taint_serializer_traits.h"
 #include <memory>
+#include <chrono> // NOLINT(*) : Google has its own time library.
+                  //             So they suppress chrono.
 
 
 bool taint_do_security_scan(
@@ -39,6 +42,9 @@ bool taint_do_security_scan(
   {
     logger.status() << "Starting the security scanner." << messaget::eom;
 
+    const std::chrono::high_resolution_clock::time_point start_time=
+      std::chrono::high_resolution_clock::now();
+
     taint_statisticst statistics;
 
     logger.status() << "Loading config files." << messaget::eom;
@@ -150,6 +156,51 @@ bool taint_do_security_scan(
       &statistics,
       &logger);
 
+    const float consumed_time_after_summarising=
+      std::chrono::duration<float>(
+        std::chrono::high_resolution_clock::now() - start_time).count();
+    if(config.get_timeout_in_seconds() > consumed_time_after_summarising)
+    {
+      const auto remaining_timeout=
+        config.get_timeout_in_seconds() - consumed_time_after_summarising;
+
+      logger.status()
+        << "Starting slicer on the analysed GOTO program (timeout="
+        << std::fixed << std::setprecision(1)
+        << remaining_timeout
+        << "s)." << messaget::eom;
+
+      taint_slicert slicer(
+        &program,
+        &numbering,
+        &named_tokens,
+        &taint_summaries,
+        tokens_propagation_graph_ptr.get(),
+        remaining_timeout,
+        config.get_slicer_root_directory(),
+        fileutl_concatenate_file_paths(
+          config.get_temp_root_directory(),
+          "SLICER"),
+        &statistics,
+        &logger);
+      slicer.compute_slice();
+    }
+
+    if(config.is_html_dump_of_program_slice_enabled())
+    {
+      logger.status()
+        << "Saving tokens propagation graph (see '"
+        << fileutl_concatenate_file_paths(
+             config.get_slicer_root_directory(),
+             "tokens_propagation_graph.svg")
+        << "')." << messaget::eom;
+      taint_dump_as_svg(
+        *tokens_propagation_graph_ptr,
+        fileutl_concatenate_file_paths(
+          config.get_slicer_root_directory(),
+          "tokens_propagation_graph.svg"));
+    }
+
     if(config.is_html_dump_of_summaries_enabled())
     {
       statistics.begin_dump_of_taint_html_summaries();

src/taint-analysis/taint_summary_dump.cpp

@@ -395,21 +395,21 @@ bool taint_functions_for_dumping_taint_summary_in_htmlt::
             bool first_and=true;
             for(const auto& set : props.get_sink_conditions())
             {
-              if(!first_and)
+              if(first_and)
+                first_and=false;
+              else
                 ostr << " and ";
               if(props.get_sink_conditions().size()>1U && set.size()>1U)
                 ostr << " ( ";
-              bool first_or=true;
-              for(const auto& cond : set)
-              {
-                if(!first_or)
-                  ostr << " or ";
-                ostr << html_encoding() << cond.dump(named_tokens);
-                first_or=false;
-              }
+              const taint_tokent::named_tokenst * const named_tokens_ptr=
+                  &named_tokens;
+              ostr << html_encoding()
+                   << join(set | boost::adaptors::transformed(
+                        [named_tokens_ptr](const taint_subject_conditiont &cond)
+                        { return cond.dump(*named_tokens_ptr); }),
+                        std::string(" or "));
               if(props.get_sink_conditions().size()>1U && set.size()>1U)
                 ostr << " ) ";
-              first_and=false;
             }
             ostr << ".";
           }

src/taint-analysis/taint_tokens_propagation_graph.cpp

@@ -209,7 +209,13 @@ std::ostream &taint_to_dot(
        << "  node [fontsize=12];\n\n";
   for(const taint_tokent::namet &token : graph.get_tokens())
     ostr << "  \"" << token
-         << "\" [shape="
+         << "\" [label=\""
+         << (token == taint_tokens_propagation_grapht::get_source_token() ?
+               taint_tokens_propagation_grapht::get_source_token().name :
+             token == taint_tokens_propagation_grapht::get_sink_token() ?
+               taint_tokens_propagation_grapht::get_sink_token().name :
+               (msgstream() << token).get())
+         << "\", shape="
          << (token==graph.get_source_token() ? "octagon" :
             (token==graph.get_sink_token()   ? "doubleoctagon" :
                                                "ellipse"))

src/taint-slicer/slicer.cpp

@@ -41,7 +41,7 @@ taint_slicert::taint_slicert(
   , named_tokens(named_tokens)
   , summaries(summaries)
   , tokens_propagation_graph(tokens_propagation_graph)
-  , timeout(timeout)
+  // , timeout(timeout)
   , results_dir(results_dir)
   , temp_dir(temp_dir)
   , statistics(statistics)

src/taint-slicer/slicer.h

@@ -73,7 +73,7 @@ class taint_slicert
   const taint_tokent::named_tokenst *named_tokens;
   const taint_summaryt::dbt * const summaries;
   const taint_tokens_propagation_grapht *tokens_propagation_graph;
-  float timeout;
+  // float timeout;
   std::string results_dir;
   std::string temp_dir;
   taint_statisticst *statistics;