Merge pull request diffblue#209 from diffblue/smowton/feature/lvsa_json_dump

Add LVSA domain JSON dump support

Author: smowton

cbmc/src/analyses/static_analysis.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 #include <memory>
 
+#include <util/json_irep.h>
 #include <util/std_expr.h>
 #include <util/std_code.h>
 
@@ -110,6 +111,34 @@ void static_analysis_baset::output(
   }
 }
 
+jsont static_analysis_baset::output_json(
+  const goto_programt &goto_program,
+  const irep_idt &identifier) const
+{
+  json_arrayt retval;
+  json_irept irep_converter(true);
+
+  forall_goto_program_instructions(i_it, goto_program)
+  {
+    json_objectt instruction_object;
+    instruction_object["location_number"]=
+      json_numbert(std::to_string(i_it->location_number));
+    instruction_object["source_location"]=
+      irep_converter.convert_from_irep(i_it->source_location);
+    instruction_object["code"]=
+      irep_converter.convert_from_irep(i_it->code);
+    {
+      std::ostringstream pretty_type;
+      pretty_type << i_it->type;
+      instruction_object["instruction_type"]=json_stringt(pretty_type.str());
+    }
+    instruction_object["state"]=get_state(i_it).output_json(ns);
+    retval.push_back(instruction_object);
+  }
+
+  return retval;
+}
+
 void static_analysis_baset::generate_states(
   const goto_functionst &goto_functions)
 {

cbmc/src/analyses/static_analysis.h

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 #include <unordered_set>
 
+#include <util/json.h>
 #include <util/make_unique.h>
 
 #include <goto-programs/goto_functions.h>
@@ -67,6 +68,11 @@ class domain_baset
   {
   }
 
+  virtual jsont output_json(const namespacet &ns) const
+  {
+    return json_stringt("");
+  }
+
   typedef std::unordered_set<exprt, irep_hash> expr_sett;
 
   // will go away
@@ -157,6 +163,11 @@ class static_analysis_baset
     output(goto_program, "", out);
   }
 
+  jsont output_json(const goto_programt &goto_program) const
+  {
+    return output_json(goto_program, "");
+  }
+
   virtual bool has_location(locationt l) const=0;
 
   void insert(locationt l)
@@ -183,6 +194,10 @@ class static_analysis_baset
     const irep_idt &identifier,
     std::ostream &out) const;
 
+  virtual jsont output_json(
+    const goto_programt &goto_program,
+    const irep_idt &identifier) const;
+
   typedef std::map<unsigned, locationt> working_sett;
 
   locationt get_next(working_sett &working_set);

cbmc/src/pointer-analysis/value_set.cpp

@@ -20,6 +20,7 @@
 #include <util/arith_tools.h>
 #include <util/pointer_offset_size.h>
 #include <util/cprover_prefix.h>
+#include <util/json_irep.h>
 
 #include <util/c_types.h>
 
@@ -192,6 +193,33 @@ void value_sett::output(
   }
 }
 
+jsont value_sett::output_json(const namespacet &) const
+{
+  json_arrayt retval;
+  json_irept irep_converter(true);
+
+  for(const auto &name_values : values)
+  {
+    json_objectt json_entry;
+
+    json_entry["id"]=json_stringt(id2string(name_values.second.identifier));
+    json_entry["suffix"]=json_stringt(id2string(name_values.second.suffix));
+
+    json_arrayt vals;
+    for(const auto &obj_entry : name_values.second.object_map.read())
+    {
+      vals.push_back(
+        irep_converter.convert_from_irep(object_numbering[obj_entry.first]));
+    }
+
+    json_entry["values"]=vals;
+
+    retval.push_back(json_entry);
+  }
+
+  return retval;
+}
+
 exprt value_sett::to_expr(const object_map_dt::value_type &it) const
 {
   const exprt &object=object_numbering[it.first];

cbmc/src/pointer-analysis/value_set.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <set>
 
+#include <util/json.h>
 #include <util/mp_arith.h>
 #include <util/reference_counting.h>
 
@@ -206,6 +207,8 @@ class value_sett
     const namespacet &ns,
     std::ostream &out) const;
 
+  jsont output_json(const namespacet &) const;
+
   valuest values;
 
   // true = added something new

cbmc/src/pointer-analysis/value_set_domain.h

@@ -30,34 +30,39 @@ class value_set_domaint:public domain_baset
     return value_set.make_union(other.value_set);
   }
 
-  virtual void output(
+  void output(
     const namespacet &ns,
-    std::ostream &out) const
+    std::ostream &out) const override
   {
     value_set.output(ns, out);
   }
 
-  virtual void initialize(
+  jsont output_json(const namespacet &ns) const override
+  {
+    return value_set.output_json(ns);
+  }
+
+  void initialize(
     const namespacet &ns,
-    locationt l)
+    locationt l) override
   {
     value_set.clear();
     value_set.location_number=l->location_number;
     value_set.function=l->function;
   }
 
-  virtual void get_reference_set(
+  void get_reference_set(
     const namespacet &ns,
     const exprt &expr,
-    value_setst::valuest &dest)
+    value_setst::valuest &dest) override
   {
     value_set.get_reference_set(expr, dest, ns);
   }
 
-  virtual void transform(
+  void transform(
     const namespacet &ns,
     locationt from_l,
-    locationt to_l)
+    locationt to_l) override
   {
     switch(from_l->type)
     {

cbmc/src/util/ui_message.h

@@ -12,6 +12,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "message.h"
 
+#define UI_MESSAGE_OPTIONS \
+  "(json-ui)" \
+  "(xml-ui)" \
+  // End of options
+
 class ui_message_handlert:public message_handlert
 {
 public:

src/driver/sec_driver_parse_options.cpp

@@ -201,6 +201,7 @@ int sec_driver_parse_optionst::doit()
       get_inverted_topological_order(call_graph,goto_model.goto_functions,process_order);
       size_t total_funcs=process_order.size();
       size_t processed=0;
+      json_objectt json_function_descriptions;
       for(const auto& fname : process_order)
       {
         ++processed;
@@ -217,12 +218,37 @@ int sec_driver_parse_optionst::doit()
         value_set_analysis(gf.body);
         if(cmdline.isset("show-value-sets"))
         {
-          status() << "*** function " << fname << eom;
-          value_set_analysis.output(gf.body, std::cout);
+          switch(get_ui())
+          {
+            case ui_message_handlert::uit::PLAIN:
+            {
+              status() << "*** function " << fname << '\n';
+              value_set_analysis.output(gf.body, status());
+              status() << eom;
+              break;
+            }
+            case ui_message_handlert::uit::JSON_UI:
+            {
+              json_function_descriptions[id2string(fname)]=
+                value_set_analysis.output_json(gf.body);
+              break;
+            }
+          default:
+            INVARIANT(false, "LVSA summary dump: UI type not handled");
+          }
         }
         if(dbpath.size()!=0)
           value_set_analysis.save_summary(gf.body);
       }
+
+      if(cmdline.isset("show-value-sets") &&
+         get_ui()==ui_message_handlert::uit::JSON_UI)
+      {
+        json_objectt dump_message;
+        dump_message["messageType"]=json_stringt("LVSA-ALL-FUNCTIONS-DUMP");
+        dump_message["functions"]=json_function_descriptions;
+        status() << dump_message << eom;
+      }
     }
     return 0;
   }

src/driver/sec_driver_parse_options.h

@@ -39,6 +39,7 @@ class optionst;
   "(local-value-set-analysis)(show-value-sets)(lvsa-function):" \
   "(security-scanner):" \
   "(rebuild-taint-cache)" \
+  UI_MESSAGE_OPTIONS \
   // End of options
 
 

src/pointer-analysis/local_value_set.h

@@ -7,6 +7,7 @@
 #define SECURITY_SCANNER_POINTER_ANALYSIS_LOCAL_VALUE_SET_H
 
 #include <pointer-analysis/value_set.h>
+#include <util/json.h>
 #include "external_value_set_expr.h"
 
 class local_value_sett:public value_sett