cprover
json_goto_trace.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Traces of GOTO Programs
4 
5 Author: Daniel Kroening
6 
7 Date: November 2005
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
15 #define CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
16 
17 #include "goto_trace.h"
18 #include "structured_trace_util.h"
19 
20 #include <algorithm>
21 #include <util/invariant.h>
22 #include <util/json.h>
23 #include <util/json_irep.h>
24 #include <util/json_stream.h>
25 
29 typedef struct
30 {
31  const jsont &location;
33  const namespacet &ns;
35 
43 void convert_assert(
44  json_objectt &json_failure,
45  const conversion_dependenciest &conversion_dependencies);
46 
56 void convert_decl(
57  json_objectt &json_assignment,
58  const conversion_dependenciest &conversion_dependencies,
59  const trace_optionst &trace_options);
60 
68 void convert_output(
69  json_objectt &json_output,
70  const conversion_dependenciest &conversion_dependencies);
71 
79 void convert_input(
80  json_objectt &json_input,
81  const conversion_dependenciest &conversion_dependencies);
82 
90 void convert_return(
91  json_objectt &json_call_return,
92  const conversion_dependenciest &conversion_dependencies);
93 
101 void convert_default(
102  json_objectt &json_location_only,
104 
115 template <typename json_arrayT>
116 void convert(
117  const namespacet &ns,
118  const goto_tracet &goto_trace,
119  json_arrayT &dest_array,
121 {
122  source_locationt previous_source_location;
123 
124  for(const auto &step : goto_trace.steps)
125  {
126  const source_locationt &source_location = step.pc->source_location;
127 
128  jsont json_location;
129 
130  source_location.is_not_nil() && !source_location.get_file().empty()
131  ? json_location = json(source_location)
132  : json_location = json_nullt();
133 
134  // NOLINTNEXTLINE(whitespace/braces)
135  conversion_dependenciest conversion_dependencies = {
136  json_location, step, ns};
137 
138  switch(step.type)
139  {
141  if(!step.cond_value)
142  {
143  json_objectt &json_failure = dest_array.push_back().make_object();
144  convert_assert(json_failure, conversion_dependencies);
145  }
146  break;
147 
150  {
151  json_objectt &json_assignment = dest_array.push_back().make_object();
152  convert_decl(json_assignment, conversion_dependencies, trace_options);
153  }
154  break;
155 
157  {
158  json_objectt &json_output = dest_array.push_back().make_object();
159  convert_output(json_output, conversion_dependencies);
160  }
161  break;
162 
164  {
165  json_objectt &json_input = dest_array.push_back().make_object();
166  convert_input(json_input, conversion_dependencies);
167  }
168  break;
169 
172  {
173  json_objectt &json_call_return = dest_array.push_back().make_object();
174  convert_return(json_call_return, conversion_dependencies);
175  }
176  break;
177 
190  const auto default_step = ::default_step(step, previous_source_location);
191  if(default_step)
192  {
193  json_objectt &json_location_only = dest_array.push_back().make_object();
194  convert_default(json_location_only, *default_step);
195  }
196  break;
197  }
198 
199  if(source_location.is_not_nil() && !source_location.get_file().empty())
200  previous_source_location = source_location;
201  }
202 }
203 
204 #endif // CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
default_step
optionalt< default_trace_stept > default_step(const goto_trace_stept &step, const source_locationt &previous_source_location)
Definition: structured_trace_util.cpp:39
convert_assert
void convert_assert(json_objectt &json_failure, const conversion_dependenciest &conversion_dependencies)
Convert an ASSERT goto_trace step.
Definition: json_goto_trace.cpp:32
goto_trace_stept::typet::LOCATION
@ LOCATION
goto_trace_stept::typet::ASSUME
@ ASSUME
json_stream.h
invariant.h
goto_tracet::steps
stepst steps
Definition: goto_trace.h:174
convert_return
void convert_return(json_objectt &json_call_return, const conversion_dependenciest &conversion_dependencies)
Convert a FUNCTION_RETURN goto_trace step.
Definition: json_goto_trace.cpp:250
goto_trace_stept
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
jsont::make_object
json_objectt & make_object()
Definition: json.h:438
jsont
Definition: json.h:27
json_irep.h
Util.
json_objectt
Definition: json.h:300
goto_trace.h
Traces of GOTO Programs.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
convert_decl
void convert_decl(json_objectt &json_assignment, const conversion_dependenciest &conversion_dependencies, const trace_optionst &trace_options)
Convert a DECL goto_trace step.
Definition: json_goto_trace.cpp:59
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
goto_trace_stept::typet::DECL
@ DECL
goto_trace_stept::typet::ASSERT
@ ASSERT
goto_trace_stept::typet::NONE
@ NONE
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
convert_default
void convert_default(json_objectt &json_location_only, const default_trace_stept &default_step)
Convert all other types of steps not already handled by the other conversion functions.
Definition: json_goto_trace.cpp:279
goto_trace_stept::typet::ASSIGNMENT
@ ASSIGNMENT
conversion_dependenciest::step
const goto_trace_stept & step
Definition: json_goto_trace.h:32
conversion_dependenciest
This is structure is here to facilitate passing arguments to the conversion functions.
Definition: json_goto_trace.h:30
dstringt::empty
bool empty() const
Definition: dstring.h:88
goto_trace_stept::typet::INPUT
@ INPUT
goto_trace_stept::typet::ATOMIC_END
@ ATOMIC_END
goto_trace_stept::typet::SPAWN
@ SPAWN
conversion_dependenciest::ns
const namespacet & ns
Definition: json_goto_trace.h:33
source_locationt
Definition: source_location.h:20
convert_output
void convert_output(json_objectt &json_output, const conversion_dependenciest &conversion_dependencies)
Convert an OUTPUT goto_trace step.
Definition: json_goto_trace.cpp:166
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
default_trace_stept
Definition: structured_trace_util.h:41
goto_trace_stept::typet::GOTO
@ GOTO
convert_input
void convert_input(json_objectt &json_input, const conversion_dependenciest &conversion_dependencies)
Convert an INPUT goto_trace step.
Definition: json_goto_trace.cpp:208
trace_optionst
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:215
trace_optionst::default_options
static const trace_optionst default_options
Definition: goto_trace.h:232
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
json.h
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
conversion_dependenciest::location
const jsont & location
Definition: json_goto_trace.h:31
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
convert
void convert(const namespacet &ns, const goto_tracet &goto_trace, json_arrayT &dest_array, trace_optionst trace_options=trace_optionst::default_options)
Templated version of the conversion method.
Definition: json_goto_trace.h:116
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
structured_trace_util.h
Utilities for printing location info steps in the trace in a format agnostic way.
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
json_nullt
Definition: json.h:415
goto_trace_stept::typet::DEAD
@ DEAD
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT