Merge pull request diffblue#29 from diffblue/smowton/feature/pretty_print_evs

External value set pretty-printer

Author: smowton

src/driver/sec_driver_parse_options.cpp

@@ -58,6 +58,8 @@ Author: Chris Smowton, [email protected]
 
 #include <taint-analysis/taint_security_scanner.h>
 
+#include <pointer-analysis/evs_pretty_printer.h>
+
 #include "sec_driver_parse_options.h"
 
 #include <fstream>
@@ -193,6 +195,7 @@ int sec_driver_parse_optionst::doit()
            << config.this_operating_system() << eom;
 
   register_languages();
+  register_evs_pretty_printer();
 
   goto_model.set_message_handler(get_message_handler());
 

src/pointer-analysis/Makefile

@@ -1,5 +1,5 @@
 
-SRC = local_value_set_analysis.cpp local_value_set.cpp
+SRC = local_value_set_analysis.cpp local_value_set.cpp evs_pretty_printer.cpp
 
 INCLUDES= -I .. -I ../../cbmc/src
 

src/pointer-analysis/evs_pretty_printer.cpp

@@ -0,0 +1,54 @@
+
+#include "evs_pretty_printer.h"
+#include <pointer-analysis/external_value_set_expr.h>
+#include <langapi/language_util.h>
+
+#include <sstream>
+
+std::string evs_pretty_printert::convert(const exprt &src)
+{
+  if(src.id()==ID_external_value_set)
+  {
+    std::ostringstream result;
+    result << "EXT_VAL_SET(";
+    bool first=true;
+    forall_operands(it, src)
+    {
+      if(!first)
+        result << ", ";
+      else
+        first=false;
+      result << top_pretty_printer->convert(*it);
+    }
+    result << ")";
+    if(src.get_bool("modified"))
+      result << "<maybe-modified>";
+    result << " ["
+           << top_pretty_printer->convert(src.type())
+           << ']';
+    return result.str();
+  }
+  else if(src.id()==ID_access_path_entry)
+  {
+    std::ostringstream result;
+    result << "{ " << src.get(ID_access_path_label) << ", " <<
+      src.get(ID_access_path_function) << ", " <<
+      src.get(ID_access_path_loc);
+    const auto &decl_type=to_access_path_entry(src).declared_on_type();
+    if(decl_type.id()==ID_struct)
+      result << " (decl-on-type " << to_struct_type(decl_type).get_tag() << ") }";
+    return result.str();
+  }
+
+  return baset::convert(src);
+}
+
+void register_evs_pretty_printer()
+{
+  register_global_pretty_printer(
+    [](const namespacet &ns)
+    {
+      return std::unique_ptr<pretty_printert>(new evs_pretty_printert(ns));
+    }
+  );
+}

src/pointer-analysis/evs_pretty_printer.h

@@ -0,0 +1,22 @@
+#ifndef SECURITY_SCANNER_POINTER_ANALYSIS_EVS_PRETTY_PRINTER
+#define SECURITY_SCANNER_POINTER_ANALYSIS_EVS_PRETTY_PRINTER
+
+#include <langapi/pretty_printer.h>
+#include <util/namespace.h>
+
+class evs_pretty_printert:public pretty_printert
+{
+public:
+  evs_pretty_printert(const namespacet &ns):
+    ns(ns)
+  {}
+
+  std::string convert(const exprt &) override;
+ protected:
+  typedef pretty_printert baset;
+  const namespacet &ns;
+};
+
+void register_evs_pretty_printer();
+
+#endif