Merge pull request diffblue#123 from trtikm/cleanup/move-dump-into-taint_sett

Implemented proper dump of taint sets

Author: NathanJPhillips

src/goto-analyzer/taint_cond.h

@@ -9,6 +9,7 @@
 #include <boost/optional.hpp>
 #include <string>
 #include <util/json.h>
+#include <util/dumper.h>
 
 
 /*******************************************************************\
@@ -34,13 +35,15 @@ class taint_condt
 
   //taint_sett substitute_for_variable(taint_variablet variable, taint_sett substitution);
 
-  boost::optional<taint_condt> recondition(taint_tokent condition2, taint_tokent result2)
+  boost::optional<taint_condt> recondition(taint_tokent condition2, taint_tokent result2) const
   {
     if (result == condition2)
       return taint_condt(subject, condition, result2);
     return boost::none;
   }
 
+  dumper dump(const taint_tokent::named_tokenst &named_tokens) const;
+
   size_t get_hash() const
   {
     std::size_t seed = 0;

src/goto-analyzer/taint_rules.cpp

@@ -9,7 +9,7 @@
 
 boost::optional<tainted_locationt> tainted_locationt::load(
   const jsont &json,
-  named_tokenst &tokens,
+  taint_tokent::named_tokenst &tokens,
   message_handlert &message_handler)
 {
   messaget msg(message_handler);

src/goto-analyzer/taint_rules.h

@@ -15,10 +15,6 @@
 #include <string>
 #include <memory>
 #include <boost/optional.hpp>
-#include <boost/bimap.hpp>
-
-
-typedef boost::bimap<std::string, taint_tokent> named_tokenst;
 
 
 /*******************************************************************\
@@ -62,7 +58,7 @@ struct tainted_locationt
 public:
   static boost::optional<tainted_locationt> load(
     const jsont & json,
-    named_tokenst &tokens,
+    taint_tokent::named_tokenst &tokens,
     message_handlert &message_handler);
 
   boost::optional<tainted_locationt> applied(
@@ -170,7 +166,7 @@ class taint_sink_rulet
 class taint_rulest
 {
 private:
-  named_tokenst named_tokens;
+  taint_tokent::named_tokenst named_tokens;
   std::map<irep_idt, std::shared_ptr<taint_propogation_rulet>> propogation_rules;
   std::map<irep_idt, std::shared_ptr<taint_sanitizer_rulet>> sanitizer_rules;
   std::map<irep_idt, std::shared_ptr<taint_sink_rulet>> sink_rules;

src/goto-analyzer/taint_set.h

@@ -5,6 +5,7 @@
 #include "taint_cond.h"
 #include <string>
 #include <util/json.h>
+#include <util/dumper.h>
 
 
 /*******************************************************************\
@@ -73,6 +74,8 @@ class taint_sett
   static taint_sett from_json(const jsont& js);
   json_objectt to_json() const;
 
+  dumper dump(const taint_tokent::named_tokenst &named_tokens) const;
+
   //[[deprecated("External code should not access internal properties")]]
   const taint_variable_sett& get_vars() const { return variables; }
 

src/goto-analyzer/taint_summary.cpp

@@ -571,19 +571,19 @@ static void  build_summary_from_computed_domain(
       {
         msg.debug() << "o ";
         taint_dump_lvalue_in_html(lval, ns, msg.debug());
-        msg.debug() << " &rarr; ";
-        taint_dump_as_html(it->second, taint_variable_to_specification_symbol_name_mapt() /*TODO*/, msg.debug());
-        msg.debug() << "\n";
+        msg.debug() << " &rarr; "
+          << it->second.dump(taint_tokent::named_tokenst() /*TODO*/)
+          << "\n";
       }
     }
     else
       if(message_handler.get_verbosity()>=messaget::M_DEBUG)
       {
         msg.debug() << "o !! EXCLUDING !! : ";
         taint_dump_lvalue_in_html(lval, ns, msg.debug());
-        msg.debug() << " &rarr; ";
-        taint_dump_as_html(it->second, taint_variable_to_specification_symbol_name_mapt() /*TODO*/, msg.debug());
-        msg.debug() << "\n";
+        msg.debug() << " &rarr; "
+          << it->second.dump(taint_tokent::named_tokenst() /*TODO*/)
+          << "\n";
       }
   }
 

src/goto-analyzer/taint_summary_dump.cpp

@@ -14,45 +14,66 @@ It provides a dump of computed taint summary in HTML format.
 
 #include <goto-analyzer/taint_summary_dump.h>
 #include <util/msgstream.h>
+#include <util/string_join.h>
 #include <memory>
 #include <map>
 #include <sstream>
 #include <iostream>
 #include <iomanip>
 #include <cassert>
+#include <boost/range/adaptor/transformed.hpp>
 
 void taint_dump_lvalue_in_html(
-    taint_lvaluet const&  lvalue,
-    namespacet const&  ns,
-    std::ostream&  ostr
-    )
+  taint_lvaluet const&  lvalue,
+  namespacet const&  ns,
+  std::ostream &ostr)
 {
   dump_access_path_in_html(lvalue,ns,ostr);
 }
 
-void taint_dump_as_html(
-    taint_sett const& taint,
-    taint_variable_to_specification_symbol_name_mapt const&
-        taint_spec_names,
-    std::ostream&  ostr
-    )
+dumper taint_sett::dump(const taint_tokent::named_tokenst &named_tokens) const
 {
-  if (taint.is_bottom())
-    ostr << "&#8869;";
-  else
-  {
-    bool first = true;
-    for (auto const&  symbol : taint.get_vars())
+  return (dumper)
+    [this, &named_tokens] (std::ostream &ostr)
     {
-       ostr << (first ? "" : " <b>&#x2210;</b> ");
-       auto const  name_it = taint_spec_names.find(symbol);
-       if (name_it != taint_spec_names.cend())
-         ostr << name_it->second;
-       else
-        ostr << "T" << symbol;
-       first = false;
-    }
-  }
+      if (is_bottom())
+      {
+        ostr << "\u22A5";
+        return;
+      }
+      std::string set_separator(" \u222A "),
+        set_element_separator(", ");
+      if(!tokens.empty() || !variables.empty())
+      {
+        ostr << "{ " << join(
+          tokens
+            | boost::adaptors::transformed([&named_tokens] (taint_tokent token)
+              { return token.get_name(named_tokens); }),
+          set_element_separator);
+        if(!tokens.empty())
+          ostr << set_element_separator;
+        ostr << join(variables, set_element_separator) << " }";
+        if(!conditionals.empty())
+          ostr << set_separator;
+      }
+      ostr << join(
+        conditionals
+          | boost::adaptors::transformed([&named_tokens] (taint_condt conditional)
+            { return conditional.dump(named_tokens); }),
+        set_separator);
+    };
+}
+
+dumper taint_condt::dump(const taint_tokent::named_tokenst &named_tokens) const
+{
+  return (dumper)
+    [this, &named_tokens] (std::ostream &ostr)
+    {
+      ostr
+        << "(" << condition.get_name(named_tokens)
+        << " \u2208 " << subject
+        << " \u2192 " << result.get_name(named_tokens) << ")";
+    };
 }
 
 void lvalues_to_taint_dump_as_html(
@@ -77,13 +98,13 @@ void lvalues_to_taint_dump_as_html(
     ostr << "    <table>\n";
     for (auto const&  elem : order)
     {
-      ostr << "      <tr>\n";
-      ostr << "        <td>" << elem.first << "</td>\n";
-      ostr << "        <td>";
-      taint_dump_as_html(lvalue_to_taint_map.at(elem.second),
-                                taint_spec_names,ostr);
-      ostr << "</td>\n";
-      ostr << "      </tr>\n";
+      ostr
+        << "      <tr>\n"
+        << "        <td>" << elem.first << "</td>\n"
+        << "        <td>"
+        << lvalue_to_taint_map.at(elem.second).dump(taint_tokent::named_tokenst() /*TODO: Use taint_spec_names*/)
+        << "</td>\n"
+        << "      </tr>\n";
     }
     ostr << "    </table>\n";
   }
@@ -113,13 +134,13 @@ void numbered_lvalues_to_taint_dump_as_html(
     ostr << "    <table>\n";
     for (auto const&  elem : order)
     {
-      ostr << "      <tr>\n";
-      ostr << "        <td>" << elem.first << "</td>\n";
-      ostr << "        <td>";
-      taint_dump_as_html(lvalue_to_taint_map.at(elem.second),
-                                taint_spec_names,ostr);
-      ostr << "</td>\n";
-      ostr << "      </tr>\n";
+      ostr
+        << "      <tr>\n"
+        << "        <td>" << elem.first << "</td>\n"
+        << "        <td>"
+        << lvalue_to_taint_map.at(elem.second).dump(taint_tokent::named_tokenst() /*TODO: Use taint_spec_names*/)
+        << "</td>\n"
+        << "      </tr>\n";
     }
     ostr << "    </table>\n";
   }
@@ -177,7 +198,7 @@ void numbered_lvalues_to_taint_changes_dump_as_html(
     ostr << "        <td>";
     auto findit=lvalue_to_taint_map.find(elem.second);
     if(findit!=lvalue_to_taint_map.end())
-      taint_dump_as_html(findit->second,taint_spec_names,ostr);
+      ostr << findit->second.dump(taint_tokent::named_tokenst() /*TODO: Use taint_spec_names*/);
     ostr << "</td>\n";
     ostr << "      </tr>\n";
   }
@@ -218,13 +239,12 @@ std::string taint_object_summary_dump_as_html(
     }
     for (auto const&  elem : order)
     {
-      ostr << "  <tr>\n";
-      ostr << "        <td>" << elem.first << "</td>\n";
-      ostr << "    <td>";
-      taint_dump_as_html(summary->input().at(elem.second),
-                                taint_spec_names,ostr);
-      ostr <<"</td>\n";
-      ostr << "  </tr>\n";
+      ostr << "  <tr>\n"
+        << "        <td>" << elem.first << "</td>\n"
+        << "    <td>"
+        << summary->input().at(elem.second).dump(taint_tokent::named_tokenst() /*TODO: Use taint_spec_names*/)
+        << "</td>\n"
+        << "  </tr>\n";
     }
   }
   ostr << "</table>\n";
@@ -245,13 +265,12 @@ std::string taint_object_summary_dump_as_html(
     }
     for (auto const&  elem : order)
     {
-      ostr << "  <tr>\n";
-      ostr << "        <td>" << elem.first << "</td>\n";
-      ostr << "    <td>";
-      taint_dump_as_html(summary->output().at(elem.second),
-                                taint_spec_names,ostr);
-      ostr <<"</td>\n";
-      ostr << "  </tr>\n";
+      ostr << "  <tr>\n"
+        << "        <td>" << elem.first << "</td>\n"
+        << "    <td>"
+        << summary->output().at(elem.second).dump(taint_tokent::named_tokenst() /*TODO: Use taint_spec_names*/)
+        << "</td>\n"
+        << "  </tr>\n";
     }
   }
   ostr << "</table>\n";

src/goto-analyzer/taint_summary_dump.h

@@ -52,26 +52,6 @@ void  taint_dump_lvalue_in_html(
  Purpose:
 
 
-\*******************************************************************/
-void taint_dump_as_html(
-    taint_sett const& taint,
-    taint_variable_to_specification_symbol_name_mapt const&
-        taint_spec_names,
-    std::ostream&  ostr
-    );
-
-
-/*******************************************************************\
-
-Function:
-
-  Inputs: See purpose
-
- Outputs: See purpose
-
- Purpose:
-
-
 \*******************************************************************/
 void lvalues_to_taint_dump_as_html(
     lvalue_to_taint_mapt const&  lvalue_to_taint_map,

src/goto-analyzer/taint_token.cpp

@@ -12,8 +12,3 @@ taint_tokent taint_tokent::fresh()
   static uint64_t last_id = 0;
   return taint_tokent(++last_id);
 }
-
-std::string taint_tokent::to_string() const
-{
-  return std::to_string(id);
-}

src/goto-analyzer/taint_token.h

@@ -7,19 +7,32 @@
 #else
 # include <set>
 #endif
+#include <boost/bimap.hpp>
 
 
 // An identifier for a concrete "taint state" of propagation from a source
 // to a sink.
 class taint_tokent : public id_as_struct<uint64_t>
 {
+public:
+  typedef boost::bimap<std::string, taint_tokent> named_tokenst;
+
 private:
   taint_tokent(uint64_t id);
 
 public:
   static taint_tokent fresh();
 
-  std::string to_string() const;
+  std::string get_name(named_tokenst names) const
+  {
+    return names.right.at(*this);
+  }
+
+  friend std::ostream& operator<<(
+    std::ostream &ostr, const taint_tokent& token)
+  {
+    return ostr << "T" << static_cast<const id_as_struct<uint64_t> &>(token);
+  }
 };
 
 namespace std

src/goto-analyzer/taint_trace_dump_html.cpp

@@ -114,18 +114,13 @@ void taint_trace_dump_as_html(
             taint_spec_names,
             ostr
             );
-      ostr << "    </td>\n"
-              "    <td>\n";
-      taint_dump_as_html(
-          element.get_taint(),
-          taint_spec_names,
-          ostr
-          );
-      ostr << "    </td>\n"
-              "    <td>" << to_html_text(element.get_message())
-           << "</td>\n"
-              "    <td>"
-              ;
+      ostr
+        << "    </td>\n"
+          "    <td>\n"
+        << element.get_taint().dump(taint_tokent::named_tokenst() /*TODO: use taint_spec_names*/)
+        << "    </td>\n"
+          "    <td>" << to_html_text(element.get_message()) << "</td>\n"
+          "    <td>";
       if (element.get_line() != 0UL)
         ostr << element.get_line();
       else