cprover
show_goto_functions_json.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Program
4 
5 Author: Thomas Kiley
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <iostream>
15 
16 #include <util/json_irep.h>
17 #include <util/cprover_prefix.h>
18 #include <util/prefix.h>
19 
20 #include "goto_functions.h"
21 
26  const namespacet &_ns,
27  bool _list_only)
28  : ns(_ns), list_only(_list_only)
29 {}
30 
35  const goto_functionst &goto_functions)
36 {
37  json_arrayt json_functions;
38  const json_irept no_comments_irep_converter(false);
39 
40  const auto sorted = goto_functions.sorted();
41 
42  for(const auto &function_entry : sorted)
43  {
44  const irep_idt &function_name = function_entry->first;
45  const goto_functionst::goto_functiont &function = function_entry->second;
46 
47  json_objectt &json_function=
48  json_functions.push_back(jsont()).make_object();
49  json_function["name"] = json_stringt(function_name);
50  json_function["isBodyAvailable"]=
51  jsont::json_boolean(function.body_available());
52  bool is_internal=
53  has_prefix(id2string(function_name), CPROVER_PREFIX) ||
54  has_prefix(id2string(function_name), "java::array[") ||
55  has_prefix(id2string(function_name), "java::org.cprover") ||
56  has_prefix(id2string(function_name), "java::java");
57  json_function["isInternal"]=jsont::json_boolean(is_internal);
58 
59  if(list_only)
60  continue;
61 
62  if(function.body_available())
63  {
64  json_arrayt json_instruction_array=json_arrayt();
65 
66  for(const goto_programt::instructiont &instruction :
67  function.body.instructions)
68  {
69  json_objectt instruction_entry{
70  {"instructionId", json_stringt(instruction.to_string())}};
71 
72  if(instruction.get_code().source_location().is_not_nil())
73  {
74  instruction_entry["sourceLocation"] =
75  json(instruction.get_code().source_location());
76  }
77 
78  std::ostringstream instruction_builder;
79  function.body.output_instruction(
80  ns, function_name, instruction_builder, instruction);
81 
82  instruction_entry["instruction"]=
83  json_stringt(instruction_builder.str());
84 
85  if(!instruction.get_code().operands().empty())
86  {
87  json_arrayt operand_array;
88  for(const exprt &operand : instruction.get_code().operands())
89  {
90  json_objectt operand_object=
91  no_comments_irep_converter.convert_from_irep(
92  operand);
93  operand_array.push_back(operand_object);
94  }
95  instruction_entry["operands"] = std::move(operand_array);
96  }
97 
98  if(instruction.has_condition())
99  {
100  json_objectt guard_object =
101  no_comments_irep_converter.convert_from_irep(
102  instruction.condition());
103 
104  instruction_entry["guard"] = std::move(guard_object);
105  }
106 
107  json_instruction_array.push_back(std::move(instruction_entry));
108  }
109 
110  json_function["instructions"] = std::move(json_instruction_array);
111  }
112  }
113 
114  return json_objectt({{"functions", json_functions}});
115 }
116 
125  const goto_functionst &goto_functions,
126  std::ostream &out,
127  bool append)
128 {
129  if(append)
130  {
131  out << ",\n";
132  }
133  out << convert(goto_functions);
134 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
const source_locationt & source_location() const
Definition: expr.h:230
operandst & operands()
Definition: expr.h:92
A collection of goto functions.
::goto_functiont goto_functiont
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const exprt & condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:382
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:360
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
std::string to_string() const
Definition: goto_program.h:562
bool is_not_nil() const
Definition: irep.h:380
jsont & push_back(const jsont &json)
Definition: json.h:212
json_objectt convert_from_irep(const irept &) const
To convert to JSON from an irep structure by recursively generating JSON for the different sub trees.
Definition: json_irep.cpp:31
Definition: json.h:27
json_objectt & make_object()
Definition: json.h:438
static jsont json_boolean(bool value)
Definition: json.h:97
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
void operator()(const goto_functionst &goto_functions, std::ostream &out, bool append=true)
Print the json object generated by show_goto_functions_jsont::show_goto_functions to the provided str...
json_objectt convert(const goto_functionst &goto_functions)
Walks through all of the functions in the program and returns a JSON object representing all their fu...
show_goto_functions_jsont(const namespacet &_ns, bool _list_only=false)
For outputting the GOTO program in a readable JSON format.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:117