Add full JSON-structured output for value-set analysis

Author: smowton

src/analyses/static_analysis.cpp

@@ -132,11 +132,7 @@ jsont static_analysis_baset::output_json(
       pretty_type << i_it->type;
       instruction_object["instruction_type"]=json_stringt(pretty_type.str());
     }
-    {
-      std::ostringstream state_text;
-      get_state(i_it).output(ns, state_text);
-      instruction_object["state"]=json_stringt(state_text.str());
-    }
+    instruction_object["state"]=get_state(i_it).output_json(ns);
     retval.push_back(instruction_object);
   }
 

src/analyses/static_analysis.h

@@ -68,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

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];

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

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)
     {