Call expr/type to json via languaget

Author: peterschrammel

src/cbmc/bmc_cover.cpp

@@ -385,7 +385,7 @@ bool bmc_covert::operator()()
               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(bmc.ns, step.pc->function, step.io_args.front());
               json_test.push_back(json_input);
             }
           }

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
@@ -128,34 +129,25 @@ void convert_decl(
 
   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);
+    base_name=symbol->base_name;
+    display_name=symbol->display_name();
+    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);
-
-    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;
-  json_assignment["lhs"] = json_stringt(full_lhs_string);
+  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)
   {
     // Not language specific, still mangled, fully-qualified name of lhs
-    json_assignment["rawLhs"] = json_irept(true).convert_from_irep(simplified);
+    json_assignment["rawLhs"] =
+      json_irept(true).convert_from_irep(simplified);
   }
-  json_assignment["hidden"] = jsont::json_boolean(step.hidden);
-  json_assignment["internal"] = jsont::json_boolean(step.internal);
-  json_assignment["thread"] = json_numbert(std::to_string(step.thread_nr));
+  json_assignment["hidden"]=jsont::json_boolean(step.hidden);
+  json_assignment["internal"]=jsont::json_boolean(step.internal);
+  json_assignment["thread"]=json_numbert(std::to_string(step.thread_nr));
 
   json_assignment["assignmentType"] = json_stringt(
     step.assignment_type == goto_trace_stept::assignment_typet::ACTUAL_PARAMETER
@@ -186,20 +178,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;
-  json_output["mode"] = json_stringt(id2string(mode));
-  json_arrayt &json_values = json_output["values"].make_array();
+  const irep_idt mode =
+    get_mode_from_identifier(ns.get_symbol_table(), 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 +218,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;
-  json_input["mode"] = json_stringt(id2string(mode));
-  json_arrayt &json_values = json_input["values"].make_array();
+  const irep_idt mode =
+    get_mode_from_identifier(ns.get_symbol_table(), 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())

src/java_bytecode/java_json_expr.cpp

@@ -0,0 +1,49 @@
+/*******************************************************************\
+
+Module: Expressions in JSON for Java
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Expressions in JSON for Java
+
+#include "java_json_expr.h"
+
+#include <util/json_expr.h>
+
+/// Output a Java source location in json.
+/// \param location: a source location
+/// \return a json object
+json_objectt java_json(const source_locationt &location)
+{
+  json_objectt result = json(source_location);
+
+  if(!location.get_java_bytecode_index().empty())
+    result["bytecodeIndex"]=
+      json_stringt(id2string(location.get_java_bytecode_index()));
+
+  return result;
+}
+
+/// Output a Java expression in json.
+/// \param expr: an expression
+/// \param ns: a namespace
+/// \return a json object
+json_objectt java_json(
+  const exprt &expr,
+  const namespacet &ns)
+{
+  if(expr.id()==ID_constant)
+  {
+    json_objectt result;
+    json(result, ns, to_constant_expr(expr), type,
+         [](const namespacet &ns, const exprt &expr) { return from_expr(ns, ID_java, expr); },
+         [](const namespacet &ns, const typet &type) { return from_type(ns, ID_java, type); });
+    return result;
+  }
+
+  return json(expr, ns);
+}
+}

src/java_bytecode/java_json_expr.h

@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+Module: Expressions in JSON for Java
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Expressions in JSON for Java
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_JSON_EXPR_H
+#define CPROVER_JAVA_BYTECODE_JAVA_JSON_EXPR_H
+
+#include "json.h"
+#include "irep.h"
+
+class source_locationt;
+class typet;
+class exprt;
+class namespacet;
+
+json_objectt java_json(
+  const exprt &,
+  const namespacet &);
+
+json_objectt java_json(
+  const typet &,
+  const namespacet &);
+
+json_objectt java_json(const source_locationt &);
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_JSON_EXPR_H

src/langapi/language.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "language.h"
 
 #include <util/expr.h>
+#include <util/json_expr.h>
 #include <util/symbol.h>
 #include <util/symbol_table.h>
 #include <util/prefix.h>
@@ -52,6 +53,25 @@ bool languaget::from_type(
   return false;
 }
 
+json_objectt languaget::json(
+  const exprt &expr,
+  const namespacet &ns)
+{
+  return ::json(expr, ns);
+}
+
+json_objectt languaget::json(
+  const typet &type,
+  const namespacet &ns)
+{
+  return ::json(type, ns);
+}
+
+json_objectt languaget::json(const source_locationt &source_location)
+{
+  return ::json(source_location);
+}
+
 bool languaget::type_to_name(
   const typet &type,
   std::string &name,

src/langapi/language.h

@@ -31,6 +31,7 @@ class exprt;
 class namespacet;
 class typet;
 class cmdlinet;
+class json_objectt;
 
 #define OPT_FUNCTIONS \
   "(function):"
@@ -126,6 +127,16 @@ class languaget:public messaget
     std::string &code,
     const namespacet &ns);
 
+  virtual json_objectt json(
+    const exprt &,
+    const namespacet &);
+
+  virtual json_objectt json(
+    const typet &,
+    const namespacet &);
+
+  virtual json_objectt json(const source_locationt &);
+
   virtual bool type_to_name(
     const typet &type,
     std::string &name,

src/langapi/language_util.cpp

@@ -45,6 +45,29 @@ std::string from_type(
   return result;
 }
 
+json_objectt json(
+  const namespacet &ns,
+  const irep_idt &identifier,
+  const exprt &expr)
+{
+  std::unique_ptr<languaget> p(
+    get_language_from_identifier(ns.get_symbol_table(), identifier));
+
+  std::string result;
+  return p->json(expr, ns);
+}
+
+json_objectt json(
+  const namespacet &ns,
+  const irep_idt &identifier,
+  const typet &type)
+{
+  std::unique_ptr<languaget> p(
+    get_language_from_identifier(ns.get_symbol_table(), identifier));
+
+  return p->json(type, ns);
+}
+
 std::string type_to_name(
   const namespacet &ns,
   const irep_idt &identifier,

src/langapi/language_util.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 class exprt;
 class namespacet;
 class typet;
+class json_objectt;
 
 std::string from_expr(
   const namespacet &ns,
@@ -23,13 +24,23 @@ std::string from_expr(
 
 std::string from_expr(const exprt &expr);
 
+json_objectt json(
+  const namespacet &ns,
+  const irep_idt &identifier,
+  const exprt &expr);
+
 std::string from_type(
   const namespacet &ns,
   const irep_idt &identifier,
   const typet &type);
 
 std::string from_type(const typet &type);
 
+json_objectt json(
+  const namespacet &ns,
+  const irep_idt &identifier,
+  const typet &type);
+
 exprt to_expr(
   const namespacet &ns,
   const irep_idt &identifier,