json_goto_trace.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Traces of GOTO Programs
 
Author: Daniel Kroening
 
  Date: November 2005
 
\*******************************************************************/
 
 
#include "json_goto_trace.h"
 
#include <util/invariant.h>
#include <util/namespace.h>
#include <util/simplify_expr.h>
#include <util/symbol.h>
 
#include <langapi/language_util.h>
 
#include "goto_trace.h"
#include "json_expr.h"
 
void convert_assert(
  json_objectt &json_failure,
  const conversion_dependenciest &conversion_dependencies)
{
  const goto_trace_stept &step = conversion_dependencies.step;
  const jsont &location = conversion_dependencies.location;
 
  json_failure["stepType"] = json_stringt("failure");
  json_failure["hidden"] = jsont::json_boolean(step.hidden);
  json_failure["internal"] = jsont::json_boolean(step.internal);
  json_failure["thread"] = json_numbert(std::to_string(step.thread_nr));
  json_failure["reason"] = json_stringt(step.comment);
  json_failure["property"] = json_stringt(step.property_id);
 
  if(!location.is_null())
    json_failure["sourceLocation"] = location;
}
 
void convert_decl(
  json_objectt &json_assignment,
  const conversion_dependenciest &conversion_dependencies,
  const trace_optionst &trace_options)
{
  const goto_trace_stept &step = conversion_dependencies.step;
  const jsont &json_location = conversion_dependencies.location;
  const namespacet &ns = conversion_dependencies.ns;
 
  auto lhs_object=step.get_lhs_object();
 
  irep_idt identifier =
    lhs_object.has_value()?lhs_object->get_identifier():irep_idt();
 
  json_assignment["stepType"] = json_stringt("assignment");
 
  if(!json_location.is_null())
    json_assignment["sourceLocation"] = json_location;
 
  std::string value_string, type_string, full_lhs_string;
  json_objectt full_lhs_value;
 
  DATA_INVARIANT(
    step.full_lhs.is_not_nil(), "full_lhs in assignment must not be nil");
  exprt simplified = simplify_expr(step.full_lhs, ns);
 
  if(trace_options.json_full_lhs)
  {
    class comment_base_name_visitort : public expr_visitort
    {
    private:
      const namespacet &ns;
 
    public:
      explicit comment_base_name_visitort(const namespacet &ns) : ns(ns)
      {
      }
 
      void operator()(exprt &expr) override
      {
        if(expr.id() == ID_symbol)
        {
          const symbolt &symbol = ns.lookup(to_symbol_expr(expr));
 
          if(expr.find(ID_C_base_name).is_not_nil())
            INVARIANT(
              expr.find(ID_C_base_name).id() == symbol.base_name,
              "base_name comment does not match symbol's base_name");
          else
            expr.add(ID_C_base_name, irept(symbol.base_name));
        }
      }
    };
    comment_base_name_visitort comment_base_name_visitor(ns);
    simplified.visit(comment_base_name_visitor);
  }
 
  full_lhs_string = from_expr(ns, identifier, simplified);
 
  const symbolt *symbol;
  irep_idt base_name, display_name;
 
  DATA_INVARIANT(
    step.full_lhs_value.is_not_nil(),
    "full_lhs_value in assignment must not be nil");
 
  if(!ns.lookup(identifier, symbol))
  {
    base_name = symbol->base_name;
    display_name = symbol->display_name();
    if(type_string.empty())
      type_string = from_type(ns, identifier, symbol->type);
 
    json_assignment["mode"] = json_stringt(symbol->mode);
    const exprt simplified_expr = simplify_expr(step.full_lhs_value, ns);
 
    full_lhs_value = json(simplified_expr, ns, symbol->mode);
  }
  else
  {
    full_lhs_value = json(step.full_lhs_value, ns, ID_unknown);
  }
 
  json_assignment["value"] = full_lhs_value;
  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["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
      ? "actual-parameter"
      : "variable");
}
 
void convert_output(
  json_objectt &json_output,
  const conversion_dependenciest &conversion_dependencies)
{
  const goto_trace_stept &step = conversion_dependencies.step;
  const jsont &location = conversion_dependencies.location;
  const namespacet &ns = conversion_dependencies.ns;
 
  json_output["stepType"] = json_stringt("output");
  json_output["hidden"] = jsont::json_boolean(step.hidden);
  json_output["internal"] = jsont::json_boolean(step.internal);
  json_output["thread"] = json_numbert(std::to_string(step.thread_nr));
  json_output["outputID"] = json_stringt(step.io_id);
 
  // Recovering the mode from the function
  irep_idt mode;
  const symbolt *function_name;
  if(ns.lookup(step.function_id, function_name))
    // Failed to find symbol
    mode = ID_unknown;
  else
    mode = function_name->mode;
  json_output["mode"] = json_stringt(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(!location.is_null())
    json_output["sourceLocation"] = location;
}
 
void convert_input(
  json_objectt &json_input,
  const conversion_dependenciest &conversion_dependencies)
{
  const goto_trace_stept &step = conversion_dependencies.step;
  const jsont &location = conversion_dependencies.location;
  const namespacet &ns = conversion_dependencies.ns;
 
  json_input["stepType"] = json_stringt("input");
  json_input["hidden"] = jsont::json_boolean(step.hidden);
  json_input["internal"] = jsont::json_boolean(step.internal);
  json_input["thread"] = json_numbert(std::to_string(step.thread_nr));
  json_input["inputID"] = json_stringt(step.io_id);
 
  // Recovering the mode from the function
  irep_idt mode;
  const symbolt *function_name;
  if(ns.lookup(step.function_id, function_name))
    // Failed to find symbol
    mode = ID_unknown;
  else
    mode = function_name->mode;
  json_input["mode"] = json_stringt(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(!location.is_null())
    json_input["sourceLocation"] = location;
}
 
void convert_return(
  json_objectt &json_call_return,
  const conversion_dependenciest &conversion_dependencies)
{
  const goto_trace_stept &step = conversion_dependencies.step;
  const jsont &location = conversion_dependencies.location;
  const namespacet &ns = conversion_dependencies.ns;
 
  std::string tag = (step.type == goto_trace_stept::typet::FUNCTION_CALL)
                      ? "function-call"
                      : "function-return";
 
  json_call_return["stepType"] = json_stringt(tag);
  json_call_return["hidden"] = jsont::json_boolean(step.hidden);
  json_call_return["internal"] = jsont::json_boolean(step.internal);
  json_call_return["thread"] = json_numbert(std::to_string(step.thread_nr));
 
  const irep_idt &function_identifier = step.called_function;
 
  const symbolt &symbol = ns.lookup(function_identifier);
  json_call_return["function"] =
    json_objectt({{"displayName", json_stringt(symbol.display_name())},
                  {"identifier", json_stringt(function_identifier)},
                  {"sourceLocation", json(symbol.location)}});
 
  if(!location.is_null())
    json_call_return["sourceLocation"] = location;
}
 
void convert_default(
  json_objectt &json_location_only,
  const default_trace_stept &default_step)
{
  json_location_only["stepType"] =
    json_stringt(default_step_name(default_step.kind));
  json_location_only["hidden"] = jsont::json_boolean(default_step.hidden);
  json_location_only["thread"] =
    json_numbert(std::to_string(default_step.thread_number));
  json_location_only["sourceLocation"] = json(default_step.location);
}