show_goto_functions_json.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Goto Program
 
Author: Thomas Kiley
 
\*******************************************************************/

 
#include "show_goto_functions_json.h"
 
#include <util/cprover_prefix.h>
#include <util/json_irep.h>
 
#include "goto_functions.h"

show_goto_functions_jsont::show_goto_functions_jsont(bool _list_only)
  : list_only(_list_only)
{}

json_objectt show_goto_functions_jsont::convert(
  const goto_functionst &goto_functions)
{
  json_arrayt json_functions;
  const json_irept no_comments_irep_converter(false);
 
  const auto sorted = goto_functions.sorted();
 
  for(const auto &function_entry : sorted)
  {
    const irep_idt &function_name = function_entry->first;
    const goto_functionst::goto_functiont &function = function_entry->second;
 
    json_objectt &json_function=
      json_functions.push_back(jsont()).make_object();
    json_function["name"] = json_stringt(function_name);
    json_function["isBodyAvailable"]=
      jsont::json_boolean(function.body_available());
    bool is_internal = function_name.starts_with(CPROVER_PREFIX) ||
                       function_name.starts_with("java::array[") ||
                       function_name.starts_with("java::org.cprover") ||
                       function_name.starts_with("java::java");
    json_function["isInternal"]=jsont::json_boolean(is_internal);
    json_function["isHidden"] = jsont::json_boolean(function.is_hidden());
    auto json_parameter_id_range =
      make_range(
        function.parameter_identifiers.begin(),
        function.parameter_identifiers.end())
        .map([](const irep_idt &id) { return json_stringt{id}; });
    json_function["parameterIdentifiers"] = json_arrayt{
      json_parameter_id_range.begin(), json_parameter_id_range.end()};
 
    if(list_only)
      continue;
 
    if(function.body_available())
    {
      json_arrayt json_instruction_array=json_arrayt();
 
      for(const goto_programt::instructiont &instruction :
        function.body.instructions)
      {
        json_objectt instruction_entry{
          {"instructionId", json_stringt(instruction.to_string())},
          {"locationNumber",
           json_numbert{std::to_string(instruction.location_number)}}};
 
        if(instruction.source_location().is_not_nil())
        {
          instruction_entry["sourceLocation"] =
            json(instruction.source_location());
        }
 
        std::ostringstream instruction_builder;
        instruction.output(instruction_builder);
 
        instruction_entry["instruction"]=
          json_stringt(instruction_builder.str());
 
        if(instruction.code().is_not_nil())
        {
          json_objectt code_object =
            no_comments_irep_converter.convert_from_irep(instruction.code());
 
          instruction_entry["code"] = std::move(code_object);
        }
 
        if(instruction.has_condition())
        {
          json_objectt guard_object =
            no_comments_irep_converter.convert_from_irep(
              instruction.condition());
 
          instruction_entry["guard"] = std::move(guard_object);
        }
 
        if(!instruction.targets.empty())
        {
          auto json_target_range =
            make_range(instruction.targets.begin(), instruction.targets.end())
              .map(
                [](const goto_programt::targett &target) {
                  return json_numbert{std::to_string(target->location_number)};
                });
          instruction_entry["targets"] =
            json_arrayt{json_target_range.begin(), json_target_range.end()};
        }
 
        if(!instruction.labels.empty())
        {
          auto json_label_range =
            make_range(instruction.labels.begin(), instruction.labels.end())
              .map([](const irep_idt &id) { return json_stringt{id}; });
          instruction_entry["labels"] =
            json_arrayt{json_label_range.begin(), json_label_range.end()};
        }
 
        json_instruction_array.push_back(std::move(instruction_entry));
      }
 
      json_function["instructions"] = std::move(json_instruction_array);
    }
  }
 
  return json_objectt({{"functions", json_functions}});
}

void show_goto_functions_jsont::operator()(
  const goto_functionst &goto_functions,
  std::ostream &out,
  bool append)
{
  if(append)
  {
    out << ",\n";
  }
  out << convert(goto_functions);
}