json_goto_trace.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Traces of GOTO Programs
 
Author: Daniel Kroening
 
Date: November 2005
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
#define CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
 
#include "goto_trace.h"
#include "structured_trace_util.h"
 
#include <util/json.h>
#include <util/json_irep.h>

typedef struct
{
  const jsont &location;
  const goto_trace_stept &step;
  const namespacet &ns;
} conversion_dependenciest;

void convert_assert(
  json_objectt &json_failure,
  const conversion_dependenciest &conversion_dependencies);

void convert_decl(
  json_objectt &json_assignment,
  const conversion_dependenciest &conversion_dependencies,
  const trace_optionst &trace_options);

void convert_output(
  json_objectt &json_output,
  const conversion_dependenciest &conversion_dependencies);

void convert_input(
  json_objectt &json_input,
  const conversion_dependenciest &conversion_dependencies);

void convert_return(
  json_objectt &json_call_return,
  const conversion_dependenciest &conversion_dependencies);

void convert_default(
  json_objectt &json_location_only,
  const default_trace_stept &default_step);

template <typename json_arrayT>
void convert(
  const namespacet &ns,
  const goto_tracet &goto_trace,
  json_arrayT &dest_array,
  trace_optionst trace_options = trace_optionst::default_options)
{
  source_locationt previous_source_location;
 
  for(const auto &step : goto_trace.steps)
  {
    const source_locationt &source_location = step.pc->source_location();
 
    jsont json_location;
 
    source_location.is_not_nil() && !source_location.get_file().empty()
      ? json_location = json(source_location)
      : json_location = json_nullt();
 
    // NOLINTNEXTLINE(whitespace/braces)
    conversion_dependenciest conversion_dependencies = {
      json_location, step, ns};
 
    switch(step.type)
    {
    case goto_trace_stept::typet::ASSERT:
      if(!step.cond_value)
      {
        json_objectt &json_failure = dest_array.push_back().make_object();
        convert_assert(json_failure, conversion_dependencies);
      }
      break;
 
    case goto_trace_stept::typet::ASSIGNMENT:
    case goto_trace_stept::typet::DECL:
    {
      json_objectt &json_assignment = dest_array.push_back().make_object();
      convert_decl(json_assignment, conversion_dependencies, trace_options);
    }
    break;
 
    case goto_trace_stept::typet::OUTPUT:
    {
      json_objectt &json_output = dest_array.push_back().make_object();
      convert_output(json_output, conversion_dependencies);
    }
    break;
 
    case goto_trace_stept::typet::INPUT:
    {
      json_objectt &json_input = dest_array.push_back().make_object();
      convert_input(json_input, conversion_dependencies);
    }
    break;
 
    case goto_trace_stept::typet::FUNCTION_CALL:
    case goto_trace_stept::typet::FUNCTION_RETURN:
    {
      json_objectt &json_call_return = dest_array.push_back().make_object();
      convert_return(json_call_return, conversion_dependencies);
    }
    break;
 
    case goto_trace_stept::typet::ATOMIC_BEGIN:
    case goto_trace_stept::typet::ATOMIC_END:
    case goto_trace_stept::typet::DEAD:
    case goto_trace_stept::typet::LOCATION:
    case goto_trace_stept::typet::GOTO:
    case goto_trace_stept::typet::ASSUME:
    case goto_trace_stept::typet::MEMORY_BARRIER:
    case goto_trace_stept::typet::SPAWN:
    case goto_trace_stept::typet::SHARED_READ:
    case goto_trace_stept::typet::SHARED_WRITE:
    case goto_trace_stept::typet::CONSTRAINT:
    case goto_trace_stept::typet::NONE:
      const auto default_step = ::default_step(step, previous_source_location);
      if(default_step)
      {
        json_objectt &json_location_only = dest_array.push_back().make_object();
        convert_default(json_location_only, *default_step);
      }
      break;
    }
 
    if(source_location.is_not_nil() && !source_location.get_file().empty())
      previous_source_location = source_location;
  }
}
 
#endif // CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H