Json output through languaget interface

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

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

@@ -18,7 +18,6 @@ Author: Daniel Kroening, [email protected]
 #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);
             }
           }

src/cbmc/show_vcc.cpp

@@ -18,7 +18,6 @@ Author: Daniel Kroening, [email protected]
 #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())

src/goto-analyzer/static_simplifier.cpp

@@ -6,16 +6,15 @@ Author: Martin Brain, [email protected]
 
 \*******************************************************************/
 
+#include "static_simplifier.h"
+
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unreachable.h>
 #include <goto-programs/write_goto_binary.h>
 
 #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.

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-instrument/unwind.h

@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_GOTO_INSTRUMENT_UNWIND_H
 
 #include <util/json.h>
-#include <util/json_expr.h>
 #include <goto-programs/goto_model.h>
 
 class goto_modelt;

src/goto-programs/goto_inline_class.h

@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/message.h>
 #include <util/json.h>
-#include <util/json_expr.h>
 
 #include "goto_functions.h"
 

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;

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)

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.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>

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;

src/goto-programs/show_properties.cpp

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [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>
 
@@ -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));

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 \