Call expr/type to json via languaget

Author: peterschrammel

src/analyses/dependence_graph.cpp

@@ -272,6 +272,7 @@ jsont dep_graph_domaint::output_json(
   const namespacet &ns) const
 {
   json_arrayt graph;
+  json_exprt json;
 
   for(const auto &cd : control_deps)
   {

src/cbmc/bmc_cover.cpp

@@ -359,7 +359,8 @@ bool bmc_covert::operator()()
         json_result["description"] = json_stringt(goal.description);
 
         if(goal.source_location.is_not_nil())
-          json_result["sourceLocation"] = json(goal.source_location);
+          json_result["sourceLocation"] = json(
+            bmc.ns, goal.source_location.get_function(), goal.source_location);
       }
       json_result["totalGoals"]=json_numbert(std::to_string(goal_map.size()));
       json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered));
@@ -384,8 +385,8 @@ bool bmc_covert::operator()()
               json_objectt json_input;
               json_input["id"]=json_stringt(id2string(step.io_id));
               if(step.io_args.size()==1)
-                json_input["value"]=
-                  json(step.io_args.front(), bmc.ns, ID_unknown);
+                json_input["value"] =
+                  json(bmc.ns, step.pc->function, step.io_args.front());
               json_test.push_back(json_input);
             }
           }

src/cbmc/show_vcc.cpp

@@ -97,7 +97,8 @@ void bmct::show_vcc_json(std::ostream &out)
 
     const source_locationt &source_location=s_it->source.pc->source_location;
     if(source_location.is_not_nil())
-      object["sourceLocation"]=json(source_location);
+      object["sourceLocation"] =
+        json(ns, s_it->source.pc->function, source_location);
 
     const std::string &s=s_it->comment;
     if(!s.empty())

src/goto-analyzer/static_verifier.cpp

@@ -11,8 +11,8 @@ Author: Martin Brain, [email protected]
 #include <util/xml.h>
 #include <util/xml_expr.h>
 #include <util/json.h>
-#include <util/json_expr.h>
 
+#include <langapi/language_util.h>
 
 /// Runs the analyzer and then prints out the domain
 /// \param goto_model: the program analyzed
@@ -78,7 +78,7 @@ bool static_verifier(
           ++unknown;
         }
 
-        j["sourceLocation"]=json(i_it->source_location);
+        j["sourceLocation"] = json(ns, i_it->function, i_it->source_location);
       }
     }
     m.status() << "Writing JSON report" << messaget::eom;

src/goto-analyzer/unreachable_instructions.cpp

@@ -16,10 +16,11 @@ Date: April 2016
 #include <sstream>
 
 #include <util/json.h>
-#include <util/json_expr.h>
 #include <util/file_util.h>
 #include <util/xml.h>
 
+#include <langapi/language_util.h>
+
 #include <analyses/cfg_dominators.h>
 
 #include <goto-programs/goto_model.h>
@@ -157,7 +158,7 @@ static void add_to_json(
     // print info for file actually with full path
     json_objectt &i_entry=dead_ins.push_back().make_object();
     const source_locationt &l=it->second->source_location;
-    i_entry["sourceLocation"]=json(l);
+    i_entry["sourceLocation"] = json(ns, it->second->function, l);
     i_entry["statement"]=json_stringt(s);
   }
 }

src/goto-diff/goto_diff_base.cpp

@@ -13,9 +13,10 @@ Author: Peter Schrammel
 
 #include <goto-programs/show_properties.h>
 
-#include <util/json_expr.h>
 #include <util/options.h>
 
+#include <langapi/language_util.h>
+
 /// Output diff result
 void goto_difft::output_functions() const
 {
@@ -136,7 +137,7 @@ void goto_difft::convert_function_json(
   const symbolt &symbol = ns.lookup(function_name);
 
   result["name"] = json_stringt(id2string(function_name));
-  result["sourceLocation"] = json(symbol.location);
+  result["sourceLocation"] = json(ns, function_name, symbol.location);
 
   if(options.get_bool_option("show-properties"))
   {

src/goto-programs/json_goto_trace.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening
 #include <util/simplify_expr.h>
 #include <util/json_irep.h>
 #include <langapi/language_util.h>
+#include <langapi/mode.h>
 
 /// Convert an ASSERT goto_trace step.
 /// \param [out] json_failure: The JSON object that
@@ -123,30 +124,18 @@ void convert_decl(
 
   full_lhs_string = from_expr(ns, identifier, simplified);
 
-  const symbolt *symbol;
   irep_idt base_name, display_name;
 
-  if(!ns.lookup(identifier, symbol))
-  {
-    base_name = symbol->base_name;
-    display_name = symbol->display_name();
-    if(type_string == "")
-      type_string = from_type(ns, identifier, symbol->type);
-
-    json_assignment["mode"] = json_stringt(id2string(symbol->mode));
-    exprt simplified = simplify_expr(step.full_lhs_value, ns);
+  const symbolt *symbol;
+  bool not_found = ns.lookup(identifier, symbol);
+  CHECK_RETURN(!not_found);
+  base_name = symbol->base_name;
+  display_name = symbol->display_name();
 
-    full_lhs_value = json(simplified, ns, symbol->mode);
-  }
-  else
-  {
-    DATA_INVARIANT(
-      step.full_lhs_value.is_not_nil(),
-      "full_lhs_value in assignment must not be nil");
-    full_lhs_value = json(step.full_lhs_value, ns, ID_unknown);
-  }
+  json_assignment["mode"] = json_stringt(id2string(symbol->mode));
 
-  json_assignment["value"] = full_lhs_value;
+  const exprt value_simplified = simplify_expr(step.full_lhs_value, ns);
+  json_assignment["value"] = json(ns, identifier, value_simplified);
   json_assignment["lhs"] = json_stringt(full_lhs_string);
   if(trace_options.json_full_lhs)
   {
@@ -186,20 +175,17 @@ void convert_output(
   json_output["outputID"] = json_stringt(id2string(step.io_id));
 
   // Recovering the mode from the function
-  irep_idt mode;
-  const symbolt *function_name;
-  if(ns.lookup(source_location.get_function(), function_name))
-    // Failed to find symbol
-    mode = ID_unknown;
-  else
-    mode = function_name->mode;
+  const irep_idt mode =
+    get_mode_from_identifier(ns, source_location.get_function());
   json_output["mode"] = json_stringt(id2string(mode));
   json_arrayt &json_values = json_output["values"].make_array();
 
   for(const auto &arg : step.io_args)
   {
-    arg.is_nil() ? json_values.push_back(json_stringt(""))
-                 : json_values.push_back(json(arg, ns, mode));
+    if(arg.is_nil())
+      json_values.push_back(json_stringt(""));
+    else
+      json_values.push_back(json(ns, source_location.get_function(), arg));
   }
 
   if(!location.is_null())
@@ -229,20 +215,17 @@ void convert_input(
   json_input["inputID"] = json_stringt(id2string(step.io_id));
 
   // Recovering the mode from the function
-  irep_idt mode;
-  const symbolt *function_name;
-  if(ns.lookup(source_location.get_function(), function_name))
-    // Failed to find symbol
-    mode = ID_unknown;
-  else
-    mode = function_name->mode;
+  const irep_idt mode =
+    get_mode_from_identifier(ns, source_location.get_function());
   json_input["mode"] = json_stringt(id2string(mode));
   json_arrayt &json_values = json_input["values"].make_array();
 
   for(const auto &arg : step.io_args)
   {
-    arg.is_nil() ? json_values.push_back(json_stringt(""))
-                 : json_values.push_back(json(arg, ns, mode));
+    if(arg.is_nil())
+      json_values.push_back(json_stringt(""));
+    else
+      json_values.push_back(json(ns, source_location.get_function(), arg));
   }
 
   if(!location.is_null())
@@ -277,7 +260,7 @@ void convert_return(
   json_objectt &json_function = json_call_return["function"].make_object();
   json_function["displayName"] = json_stringt(id2string(symbol.display_name()));
   json_function["identifier"] = json_stringt(id2string(step.identifier));
-  json_function["sourceLocation"] = json(symbol.location);
+  json_function["sourceLocation"] = json(ns, step.identifier, symbol.location);
 
   if(!location.is_null())
     json_call_return["sourceLocation"] = location;

src/goto-programs/json_goto_trace.h

@@ -21,6 +21,9 @@ Date: November 2005
 #include <util/json_expr.h>
 #include <util/invariant.h>
 
+#include <langapi/mode.h>
+#include <langapi/language_util.h>
+
 /// This is structure is here to facilitate
 /// passing arguments to the conversion
 /// functions.
@@ -127,8 +130,10 @@ void convert(
 
     jsont json_location;
 
-    source_location.is_not_nil() && !source_location.get_file().empty()
-      ? json_location = json(source_location)
+    source_location.is_not_nil() && !source_location.get_file().empty() &&
+        !source_location.get_function().empty()
+      ? json_location =
+          json(ns, source_location.get_function(), source_location)
       : json_location = json_nullt();
 
     // NOLINTNEXTLINE(whitespace/braces)

src/goto-programs/loop_ids.cpp

@@ -87,7 +87,7 @@ void show_loop_ids_json(
 
       json_objectt &loop=loops.push_back().make_object();
       loop["name"]=json_stringt(id);
-      loop["sourceLocation"]=json(it->source_location);
+      loop["sourceLocation"] = json_exprt()(it->source_location);
     }
   }
 }
@@ -110,6 +110,7 @@ void show_loop_ids(
       forall_goto_functions(it, goto_functions)
         show_loop_ids_json(ui, it->second.body, loops);
 
+      // TODO: this needs clean up
       std::cout << ",\n" << json_result;
       break;
   }

src/goto-programs/show_goto_functions_json.cpp

@@ -75,8 +75,8 @@ json_objectt show_goto_functions_jsont::convert(
 
         if(instruction.code.source_location().is_not_nil())
         {
-          instruction_entry["sourceLocation"]=
-            json(instruction.code.source_location());
+          instruction_entry["sourceLocation"] =
+            json(ns, instruction.function, instruction.code.source_location());
         }
 
         std::ostringstream instruction_builder;

src/goto-programs/show_properties.cpp

@@ -137,7 +137,7 @@ void convert_properties_json(
       json_property["coveredLines"]=
         json_stringt(
           id2string(source_location.get_basic_block_covered_lines()));
-    json_property["sourceLocation"]=json(source_location);
+    json_property["sourceLocation"] = json(ns, identifier, source_location);
     json_property["description"]=json_stringt(id2string(description));
     json_property["expression"]=
       json_stringt(from_expr(ns, identifier, ins.guard));

src/java_bytecode/Makefile

@@ -20,6 +20,7 @@ SRC = bytecode_info.cpp \
       java_class_loader_limit.cpp \
       java_enum_static_init_unwind_handler.cpp \
       java_entry_point.cpp \
+      java_json_expr.cpp \
       java_local_variable_table.cpp \
       java_object_factory.cpp \
       java_pointer_casts.cpp \

src/java_bytecode/java_bytecode_language.cpp

@@ -34,6 +34,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_static_initializers.h"
 #include "java_utils.h"
 #include <java_bytecode/ci_lazy_methods.h>
+#include "java_json_expr.h"
 
 #include "expr2java.h"
 
@@ -1087,6 +1088,24 @@ bool java_bytecode_languaget::to_expr(
   return true; // fail for now
 }
 
+json_objectt
+java_bytecode_languaget::json(const exprt &expr, const namespacet &ns)
+{
+  return java_json_exprt()(expr, ns);
+}
+
+json_objectt
+java_bytecode_languaget::json(const typet &type, const namespacet &ns)
+{
+  return java_json_exprt()(type, ns);
+}
+
+json_objectt
+java_bytecode_languaget::json(const source_locationt &source_location)
+{
+  return java_json_exprt()(source_location);
+}
+
 java_bytecode_languaget::~java_bytecode_languaget()
 {
 }

src/java_bytecode/java_bytecode_language.h

@@ -127,6 +127,12 @@ class java_bytecode_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
+  json_objectt json(const exprt &, const namespacet &) override;
+
+  json_objectt json(const typet &, const namespacet &) override;
+
+  json_objectt json(const source_locationt &) override;
+
   std::unique_ptr<languaget> new_language() override
   { return util_make_unique<java_bytecode_languaget>(); }
 

src/java_bytecode/java_json_expr.cpp

@@ -0,0 +1,53 @@
+/*******************************************************************\
+
+Module: Expressions in JSON for Java
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Expressions in JSON for Java
+
+#include "java_json_expr.h"
+
+#include <util/std_expr.h>
+
+#include <langapi/language.h>
+
+/// Output a Java source location in json.
+/// \param location: a source location
+/// \return a json object
+json_objectt java_json_exprt::operator()(const source_locationt &location)
+{
+  json_objectt result = json_exprt()(location);
+
+  if(!location.get_java_bytecode_index().empty())
+    result["bytecodeIndex"] =
+      json_stringt(id2string(location.get_java_bytecode_index()));
+
+  return result;
+}
+
+/// Output a Java constant expression as a string.
+/// \param ns: a namespace
+/// \param expr: a constant expression
+/// \return a string
+std::string
+java_json_exprt::from_constant(const namespacet &ns, const constant_exprt &expr)
+{
+  std::string result;
+  language->from_expr(expr, result, ns);
+  return result;
+}
+
+/// Output a Java type as a string.
+/// \param ns: a namespace
+/// \param type: an type
+/// \return a string
+std::string java_json_exprt::from_type(const namespacet &ns, const typet &type)
+{
+  std::string result;
+  language->from_type(type, result, ns);
+  return result;
+}