diff --git a/src/Makefile b/src/Makefile
index d28a2bdc976..d570dbb641a 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -25,8 +25,6 @@ languages: util.dir langapi.dir \
            cpp.dir ansi-c.dir xmllang.dir assembler.dir java_bytecode.dir \
            jsil.dir
 
-solvers.dir: util.dir langapi.dir
-
 goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
                      goto-symex.dir linking.dir analyses.dir solvers.dir \
                      json.dir
diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
index dd9a770d837..3aa90133198 100644
--- a/src/analyses/dependence_graph.cpp
+++ b/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)
   {
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
index 72d64a184a5..76cbc7d5d79 100644
--- a/src/cbmc/bmc_cover.cpp
+++ b/src/cbmc/bmc_cover.cpp
@@ -18,7 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/xml_expr.h>
 #include <util/json.h>
 #include <util/json_stream.h>
-#include <util/json_expr.h>
 
 #include <solvers/prop/cover_goals.h>
 #include <solvers/prop/literal_expr.h>
@@ -359,7 +358,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 +384,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);
             }
           }
diff --git a/src/cbmc/show_vcc.cpp b/src/cbmc/show_vcc.cpp
index 6a5b051cff9..1ab4fae60c0 100644
--- a/src/cbmc/show_vcc.cpp
+++ b/src/cbmc/show_vcc.cpp
@@ -18,7 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language_util.h>
 
 #include <util/json.h>
-#include <util/json_expr.h>
 
 void bmct::show_vcc_plain(std::ostream &out)
 {
@@ -97,7 +96,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())
diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp
index 9e6ffa57822..aa0d2ad476a 100644
--- a/src/goto-analyzer/static_simplifier.cpp
+++ b/src/goto-analyzer/static_simplifier.cpp
@@ -6,6 +6,8 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 
 \*******************************************************************/
 
+#include "static_simplifier.h"
+
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unreachable.h>
 #include <goto-programs/write_goto_binary.h>
@@ -13,9 +15,6 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 #include <util/xml.h>
 #include <util/xml_expr.h>
 #include <util/json.h>
-#include <util/json_expr.h>
-
-#include "static_simplifier.h"
 
 
 /// Simplifies the program using the information in the abstract domain.
diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp
index 660d20bd37e..daa28ca898c 100644
--- a/src/goto-analyzer/static_verifier.cpp
+++ b/src/goto-analyzer/static_verifier.cpp
@@ -11,8 +11,8 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 #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;
diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp
index 0e783baaba5..7ca7312901c 100644
--- a/src/goto-analyzer/unreachable_instructions.cpp
+++ b/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);
   }
 }
diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp
index db3b925d702..9ae2e957df1 100644
--- a/src/goto-diff/goto_diff_base.cpp
+++ b/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"))
   {
diff --git a/src/goto-instrument/unwind.h b/src/goto-instrument/unwind.h
index 072c6f54267..0ba4719d845 100644
--- a/src/goto-instrument/unwind.h
+++ b/src/goto-instrument/unwind.h
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_GOTO_INSTRUMENT_UNWIND_H
 
 #include <util/json.h>
-#include <util/json_expr.h>
 #include <goto-programs/goto_model.h>
 
 class goto_modelt;
diff --git a/src/goto-programs/goto_inline_class.h b/src/goto-programs/goto_inline_class.h
index eea4a63eba4..6adaa313329 100644
--- a/src/goto-programs/goto_inline_class.h
+++ b/src/goto-programs/goto_inline_class.h
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/message.h>
 #include <util/json.h>
-#include <util/json_expr.h>
 
 #include "goto_functions.h"
 
diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp
index 1095a3ad281..bbd785e103a 100644
--- a/src/goto-programs/json_goto_trace.cpp
+++ b/src/goto-programs/json_goto_trace.cpp
@@ -14,7 +14,6 @@ Author: Daniel Kroening
 #include "json_goto_trace.h"
 #include "goto_trace.h"
 
-#include <util/json_expr.h>
 #include <util/json.h>
 #include <util/json_stream.h>
 #include <util/arith_tools.h>
@@ -23,6 +22,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 +123,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 +174,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 +214,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 +259,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;
diff --git a/src/goto-programs/json_goto_trace.h b/src/goto-programs/json_goto_trace.h
index 820de78ee78..464bf315fdd 100644
--- a/src/goto-programs/json_goto_trace.h
+++ b/src/goto-programs/json_goto_trace.h
@@ -18,9 +18,11 @@ Date: November 2005
 
 #include <util/json.h>
 #include <util/json_stream.h>
-#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 +129,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)
diff --git a/src/goto-programs/loop_ids.cpp b/src/goto-programs/loop_ids.cpp
index 86deb73eb43..4f1a6afce6e 100644
--- a/src/goto-programs/loop_ids.cpp
+++ b/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;
   }
diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp
index 4180e38c719..f17868048e1 100644
--- a/src/goto-programs/show_goto_functions.cpp
+++ b/src/goto-programs/show_goto_functions.cpp
@@ -15,7 +15,6 @@ Author: Peter Schrammel
 
 #include <util/xml.h>
 #include <util/json.h>
-#include <util/json_expr.h>
 #include <util/xml_expr.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
diff --git a/src/goto-programs/show_goto_functions_json.cpp b/src/goto-programs/show_goto_functions_json.cpp
index bfedc6250c2..e836f4bc148 100644
--- a/src/goto-programs/show_goto_functions_json.cpp
+++ b/src/goto-programs/show_goto_functions_json.cpp
@@ -14,7 +14,6 @@ Author: Thomas Kiley
 #include <iostream>
 #include <sstream>
 
-#include <util/json_expr.h>
 #include <util/json_irep.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
@@ -75,8 +74,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;
diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp
index 6df2f69bf33..1bc28d5a7d2 100644
--- a/src/goto-programs/show_properties.cpp
+++ b/src/goto-programs/show_properties.cpp
@@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/xml.h>
 #include <util/xml_expr.h>
 #include <util/json.h>
-#include <util/json_expr.h>
 
 #include <langapi/language_util.h>
 
@@ -137,7 +136,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));
diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile
index cf6d7a5cc9d..c80fcf6ba2c 100644
--- a/src/java_bytecode/Makefile
+++ b/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 \
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 0de42e59ebc..97ba9893dde 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -34,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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()
 {
 }
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index 47d5fb69d82..db5190cda83 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/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>(); }
 
diff --git a/src/java_bytecode/java_json_expr.cpp b/src/java_bytecode/java_json_expr.cpp
new file mode 100644
index 00000000000..ff28c04b6c6
--- /dev/null
+++ b/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;
+}
diff --git a/src/java_bytecode/java_json_expr.h b/src/java_bytecode/java_json_expr.h
new file mode 100644
index 00000000000..b6294070249
--- /dev/null
+++ b/src/java_bytecode/java_json_expr.h
@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+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 <util/json_expr.h>
+
+#include <langapi/mode.h>
+
+class java_json_exprt : public json_exprt
+{
+public:
+  json_objectt operator()(const exprt &expr, const namespacet &ns) override
+  {
+    return json_exprt::operator()(expr, ns);
+  }
+
+  json_objectt operator()(const typet &type, const namespacet &ns) override
+  {
+    return json_exprt::operator()(type, ns);
+  }
+
+  json_objectt operator()(const source_locationt &) override;
+
+protected:
+  std::unique_ptr<languaget> language = get_language_from_mode(ID_java);
+  std::string
+  from_constant(const namespacet &ns, const constant_exprt &) override;
+  std::string from_type(const namespacet &ns, const typet &) override;
+};
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_JSON_EXPR_H
diff --git a/src/langapi/language.cpp b/src/langapi/language.cpp
index 443062dce08..61deab3b2a3 100644
--- a/src/langapi/language.cpp
+++ b/src/langapi/language.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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,21 @@ bool languaget::from_type(
   return false;
 }
 
+json_objectt languaget::json(const exprt &expr, const namespacet &ns)
+{
+  return json_exprt()(expr, ns);
+}
+
+json_objectt languaget::json(const typet &type, const namespacet &ns)
+{
+  return json_exprt()(type, ns);
+}
+
+json_objectt languaget::json(const source_locationt &source_location)
+{
+  return json_exprt()(source_location);
+}
+
 bool languaget::type_to_name(
   const typet &type,
   std::string &name,
diff --git a/src/langapi/language.h b/src/langapi/language.h
index 9e35daa17c9..f868cc9e6e6 100644
--- a/src/langapi/language.h
+++ b/src/langapi/language.h
@@ -134,6 +134,24 @@ class languaget:public messaget
     std::string &code,
     const namespacet &ns);
 
+  /// Formats the given expression as a JSON object in a language-specific way
+  /// \param expr: the expression to format
+  /// \param ns: a namespace
+  /// \return the JSON object
+  virtual json_objectt json(const exprt &, const namespacet &);
+
+  /// Formats the given type as a JSON object in a language-specific way
+  /// \param type: the type to format
+  /// \param ns: a namespace
+  /// \return the JSON object
+  virtual json_objectt json(const typet &, const namespacet &);
+
+  /// Formats the given source location as a JSON object
+  ///   in a language-specific way
+  /// \param source_location: the source location to format
+  /// \return the JSON object
+  virtual json_objectt json(const source_locationt &);
+
   /// Encodes the given type in a language-specific way
   /// \param type: the type to encode
   /// \param name: the encoded type
diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp
index 87c51c9877f..6ad2755d375 100644
--- a/src/langapi/language_util.cpp
+++ b/src/langapi/language_util.cpp
@@ -17,6 +17,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "language.h"
 #include "mode.h"
 
+/// Formats the given expression according to the given identifier's language
+/// \param ns: a namespace
+/// \param identifier: an identifier whose symbol's mode determines the language
+/// \param expr: the expression to format
+/// \return the formatted expression
 std::string from_expr(
   const namespacet &ns,
   const irep_idt &identifier,
@@ -30,6 +35,11 @@ std::string from_expr(
   return result;
 }
 
+/// Formats the given type according to the given identifier's language
+/// \param ns: a namespace
+/// \param identifier: an identifier whose symbol's mode determines the language
+/// \param type: the type to format
+/// \return the formatted type
 std::string from_type(
   const namespacet &ns,
   const irep_idt &identifier,
@@ -43,6 +53,40 @@ std::string from_type(
   return result;
 }
 
+/// Formats the given expression as a JSON object, according to the given
+///   identifier's language
+/// \param ns: a namespace
+/// \param identifier: an identifier whose symbol's mode determines the language
+/// \param expr: the expression to format
+/// \return the JSON object
+json_objectt
+json(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
+{
+  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
+
+  std::string result;
+  return p->json(expr, ns);
+}
+
+/// Formats the given type as a JSON object, according to the given
+///   identifier's language
+/// \param ns: a namespace
+/// \param identifier: an identifier whose symbol's mode determines the language
+/// \param type: the type to format
+/// \return the JSON object
+json_objectt
+json(const namespacet &ns, const irep_idt &identifier, const typet &type)
+{
+  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
+
+  return p->json(type, ns);
+}
+
+/// Encodes the given type according to the given identifier's language
+/// \param ns: a namespace
+/// \param identifier: an identifier whose symbol's mode determines the language
+/// \param type: the type to encode
+/// \return the encoded type
 std::string type_to_name(
   const namespacet &ns,
   const irep_idt &identifier,
@@ -56,18 +100,30 @@ std::string type_to_name(
   return result;
 }
 
+/// Formats the given expression according to the default language
+/// \param expr: the expression to format
+/// \return the formatted expression
 std::string from_expr(const exprt &expr)
 {
   symbol_tablet symbol_table;
   return from_expr(namespacet(symbol_table), "", expr);
 }
 
+/// Formats the given type according to the default language
+/// \param type: the type to format
+/// \return the formatted type
 std::string from_type(const typet &type)
 {
   symbol_tablet symbol_table;
   return from_type(namespacet(symbol_table), "", type);
 }
 
+/// Parses the given string into an expression according to the given
+///   identifier's language
+/// \param ns: a namespace
+/// \param identifier: an identifier whose symbol's mode determines the language
+/// \param src: the string to parse
+/// \return the parsed expression
 exprt to_expr(
   const namespacet &ns,
   const irep_idt &identifier,
@@ -88,8 +144,27 @@ exprt to_expr(
   return expr;
 }
 
+/// Encodes the given type according to the default language
+/// \param type: the type to encode
+/// \return the encoded type
 std::string type_to_name(const typet &type)
 {
   symbol_tablet symbol_table;
   return type_to_name(namespacet(symbol_table), "", type);
 }
+
+/// Formats the given source location as a JSON object, according to the given
+///   identifier's language
+/// \param ns: a namespace
+/// \param identifier: an identifier whose symbol's mode determines the language
+/// \param source_location: the source location to format
+/// \return the JSON object
+json_objectt json(
+  const namespacet &ns,
+  const irep_idt &identifier,
+  const source_locationt &source_location)
+{
+  std::unique_ptr<languaget> p(get_language_from_identifier(ns, identifier));
+
+  return p->json(source_location);
+}
diff --git a/src/langapi/language_util.h b/src/langapi/language_util.h
index 9893aea4b68..423e5ee7583 100644
--- a/src/langapi/language_util.h
+++ b/src/langapi/language_util.h
@@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 class exprt;
 class namespacet;
 class typet;
+class json_objectt;
+class source_locationt;
 
 std::string from_expr(
   const namespacet &ns,
@@ -23,6 +25,9 @@ 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,
@@ -30,6 +35,9 @@ std::string from_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,
@@ -42,4 +50,9 @@ std::string type_to_name(
 
 std::string type_to_name(const typet &type);
 
+json_objectt json(
+  const namespacet &ns,
+  const irep_idt &identifier,
+  const source_locationt &source_location);
+
 #endif // CPROVER_LANGAPI_LANGUAGE_UTIL_H
diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index 2256e0ee977..102a8ba0de1 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -227,5 +227,5 @@ solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB)
 	$(LINKLIB) $(LIBSOLVER)
 
 smt2_solver$(EXEEXT): $(OBJ) smt2/smt2_solver$(OBJEXT) \
-	../util/util$(LIBEXT) ../langapi/langapi$(LIBEXT) ../big-int/big-int$(LIBEXT) $(SOLVER_LIB)
+	../util/util$(LIBEXT) ../big-int/big-int$(LIBEXT) $(SOLVER_LIB)
 	$(LINKBIN) $(LIBSOLVER)
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 055eabc7891..19e7810aba2 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -3,4 +3,4 @@ add_library(util ${sources})
 
 generic_includes(util)
 
-target_link_libraries(util big-int langapi)
+target_link_libraries(util big-int)
diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp
index aa8b63a0dc7..228decd24b9 100644
--- a/src/util/json_expr.cpp
+++ b/src/util/json_expr.cpp
@@ -21,11 +21,13 @@ Author: Peter Schrammel
 #include "config.h"
 #include "identifier.h"
 #include "invariant.h"
-
-#include <langapi/mode.h>
-#include <langapi/language.h>
+#include "format.h"
+#include "format_type.h"
+#include "format_expr.h"
+#include "format_constant.h"
 
 #include <memory>
+#include <sstream>
 
 static exprt simplify_json_expr(
   const exprt &src,
@@ -80,7 +82,7 @@ static exprt simplify_json_expr(
   return src;
 }
 
-json_objectt json(const source_locationt &location)
+json_objectt json_exprt::operator()(const source_locationt &location)
 {
   json_objectt result;
 
@@ -100,27 +102,17 @@ json_objectt json(const source_locationt &location)
   if(!location.get_function().empty())
     result["function"]=json_stringt(id2string(location.get_function()));
 
-  if(!location.get_java_bytecode_index().empty())
-    result["bytecodeIndex"]=
-      json_stringt(id2string(location.get_java_bytecode_index()));
-
   return result;
 }
 
 /// Output a CBMC type in json.
-/// The `mode` argument is used to correctly report types.
 /// \param type: a type
 /// \param ns: a namespace
-/// \param mode: language in which the code was written; for now ID_C and
-///   ID_java are supported
 /// \return a json object
-json_objectt json(
-  const typet &type,
-  const namespacet &ns,
-  const irep_idt &mode)
+json_objectt json_exprt::operator()(const typet &type, const namespacet &ns)
 {
   if(type.id()==ID_symbol)
-    return json(ns.follow(type), ns, mode);
+    return (*this)(ns.follow(type), ns);
 
   json_objectt result;
 
@@ -156,7 +148,7 @@ json_objectt json(
   else if(type.id()==ID_c_enum_tag)
   {
     // we return the base type
-    return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns, mode);
+    return (*this)(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns);
   }
   else if(type.id()==ID_fixedbv)
   {
@@ -167,7 +159,7 @@ json_objectt json(
   else if(type.id()==ID_pointer)
   {
     result["name"]=json_stringt("pointer");
-    result["subtype"]=json(type.subtype(), ns, mode);
+    result["subtype"] = (*this)(type.subtype(), ns);
   }
   else if(type.id()==ID_bool)
   {
@@ -176,13 +168,13 @@ json_objectt json(
   else if(type.id()==ID_array)
   {
     result["name"]=json_stringt("array");
-    result["subtype"]=json(type.subtype(), ns, mode);
+    result["subtype"] = (*this)(type.subtype(), ns);
   }
   else if(type.id()==ID_vector)
   {
     result["name"]=json_stringt("vector");
-    result["subtype"]=json(type.subtype(), ns, mode);
-    result["size"]=json(to_vector_type(type).size(), ns, mode);
+    result["subtype"] = (*this)(type.subtype(), ns);
+    result["size"] = (*this)(to_vector_type(type).size(), ns);
   }
   else if(type.id()==ID_struct)
   {
@@ -194,7 +186,7 @@ json_objectt json(
     {
       json_objectt &e=members.push_back().make_object();
       e["name"]=json_stringt(id2string(component.get_name()));
-      e["type"]=json(component.type(), ns, mode);
+      e["type"] = (*this)(component.type(), ns);
     }
   }
   else if(type.id()==ID_union)
@@ -207,7 +199,7 @@ json_objectt json(
     {
       json_objectt &e=members.push_back().make_object();
       e["name"]=json_stringt(id2string(component.get_name()));
-      e["type"]=json(component.type(), ns, mode);
+      e["type"] = (*this)(component.type(), ns);
     }
   }
   else
@@ -216,17 +208,24 @@ json_objectt json(
   return result;
 }
 
+std::string
+json_exprt::from_constant(const namespacet &ns, const constant_exprt &expr)
+{
+  return format_constantt()(expr);
+}
+
+std::string json_exprt::from_type(const namespacet &ns, const typet &type)
+{
+  std::stringstream ss;
+  ss << format(ns.follow(type));
+  return ss.str();
+}
+
 /// Output a CBMC expression in json.
-/// The mode is used to correctly report types.
 /// \param expr: an expression
 /// \param ns: a namespace
-/// \param mode: language in which the code was written; for now ID_C and
-///   ID_java are supported
 /// \return a json object
-json_objectt json(
-  const exprt &expr,
-  const namespacet &ns,
-  const irep_idt &mode)
+json_objectt json_exprt::operator()(const exprt &expr, const namespacet &ns)
 {
   json_objectt result;
 
@@ -234,28 +233,14 @@ json_objectt json(
 
   if(expr.id()==ID_constant)
   {
-    std::unique_ptr<languaget> lang;
-    if(mode==ID_unknown)
-      lang=std::unique_ptr<languaget>(get_default_language());
-    else
-    {
-      lang=std::unique_ptr<languaget>(get_language_from_mode(mode));
-      if(!lang)
-        lang=std::unique_ptr<languaget>(get_default_language());
-    }
-
     const typet &underlying_type=
       type.id()==ID_c_bit_field?type.subtype():
       type;
 
-    std::string type_string;
-    bool error=lang->from_type(underlying_type, type_string, ns);
-    CHECK_RETURN(!error);
-
-    std::string value_string;
-    lang->from_expr(expr, value_string, ns);
-
+    std::string type_string = from_type(ns, underlying_type);
     const constant_exprt &constant_expr=to_constant_expr(expr);
+    std::string value_string = from_constant(ns, constant_expr);
+
     if(type.id()==ID_unsignedbv ||
        type.id()==ID_signedbv ||
        type.id()==ID_c_bit_field)
@@ -281,7 +266,7 @@ json_objectt json(
       constant_exprt tmp;
       tmp.type()=ns.follow_tag(to_c_enum_tag_type(type));
       tmp.set_value(to_constant_expr(expr).get_value());
-      return json(tmp, ns, mode);
+      result = (*this)(tmp, ns);
     }
     else if(type.id()==ID_bv)
     {
@@ -359,7 +344,7 @@ json_objectt json(
     {
       json_objectt &e=elements.push_back().make_object();
       e["index"]=json_numbert(std::to_string(index));
-      e["value"]=json(*it, ns, mode);
+      e["value"] = (*this)(*it, ns);
       index++;
     }
   }
@@ -380,7 +365,7 @@ json_objectt json(
       for(std::size_t m=0; m<expr.operands().size(); m++)
       {
         json_objectt &e=members.push_back().make_object();
-        e["value"]=json(expr.operands()[m], ns, mode);
+        e["value"] = (*this)(expr.operands()[m], ns);
         e["name"]=json_stringt(id2string(components[m].get_name()));
       }
     }
@@ -391,7 +376,7 @@ json_objectt json(
 
     const union_exprt &union_expr=to_union_expr(expr);
     json_objectt &e=result["member"].make_object();
-    e["value"]=json(union_expr.op(), ns, mode);
+    e["value"] = (*this)(union_expr.op(), ns);
     e["name"]=json_stringt(id2string(union_expr.get_component_name()));
   }
   else
diff --git a/src/util/json_expr.h b/src/util/json_expr.h
index cc082020cdc..2bbe9a09458 100644
--- a/src/util/json_expr.h
+++ b/src/util/json_expr.h
@@ -18,18 +18,21 @@ Author: Peter Schrammel
 class source_locationt;
 class typet;
 class exprt;
+class constant_exprt;
 class namespacet;
 
-json_objectt json(
-  const exprt &,
-  const namespacet &,
-  const irep_idt &mode);
+class json_exprt
+{
+public:
+  virtual json_objectt operator()(const exprt &, const namespacet &);
 
-json_objectt json(
-  const typet &,
-  const namespacet &,
-  const irep_idt &mode);
+  virtual json_objectt operator()(const typet &, const namespacet &);
 
-json_objectt json(const source_locationt &);
+  virtual json_objectt operator()(const source_locationt &);
+
+protected:
+  virtual std::string from_constant(const namespacet &, const constant_exprt &);
+  virtual std::string from_type(const namespacet &, const typet &);
+};
 
 #endif // CPROVER_UTIL_JSON_EXPR_H
diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp
index 83c5473fe78..06e47186f92 100644
--- a/src/util/ui_message.cpp
+++ b/src/util/ui_message.cpp
@@ -287,7 +287,10 @@ void ui_message_handlert::json_ui_msg(
 
   if(location.is_not_nil() &&
      !location.get_file().empty())
-    result["sourceLocation"] = json(location);
+  {
+    // Note: this output is not language-specific
+    result["sourceLocation"] = json_exprt()(location);
+  }
 
   result["messageType"] = json_stringt(type);
   result["messageText"] = json_stringt(msg1);