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 #include <sstream>
16 
17 #include <util/json_expr.h>
18 #include <util/json_irep.h>
19 #include <util/cprover_prefix.h>
20 #include <util/prefix.h>
21 
22 #include <langapi/language_util.h>
23 
24 #include "goto_functions.h"
25 #include "goto_model.h"
26 
31  const namespacet &_ns,
32  bool _list_only)
33  : ns(_ns), list_only(_list_only)
34 {}
35 
40  const goto_functionst &goto_functions)
41 {
42  json_arrayt json_functions;
43  const json_irept no_comments_irep_converter(false);
44 
45  const auto sorted = goto_functions.sorted();
46 
47  for(const auto &function_entry : sorted)
48  {
49  const irep_idt &function_name = function_entry->first;
50  const goto_functionst::goto_functiont &function = function_entry->second;
51 
52  json_objectt &json_function=
53  json_functions.push_back(jsont()).make_object();
54  json_function["name"] = json_stringt(function_name);
55  json_function["isBodyAvailable"]=
56  jsont::json_boolean(function.body_available());
57  bool is_internal=
58  has_prefix(id2string(function_name), CPROVER_PREFIX) ||
59  has_prefix(id2string(function_name), "java::array[") ||
60  has_prefix(id2string(function_name), "java::org.cprover") ||
61  has_prefix(id2string(function_name), "java::java");
62  json_function["isInternal"]=jsont::json_boolean(is_internal);
63 
64  if(list_only)
65  continue;
66 
67  if(function.body_available())
68  {
69  json_arrayt json_instruction_array=json_arrayt();
70 
71  for(const goto_programt::instructiont &instruction :
72  function.body.instructions)
73  {
74  json_objectt instruction_entry=json_objectt();
75 
76  instruction_entry["instructionId"]=
77  json_stringt(instruction.to_string());
78 
79  if(instruction.code.source_location().is_not_nil())
80  {
81  instruction_entry["sourceLocation"]=
82  json(instruction.code.source_location());
83  }
84 
85  std::ostringstream instruction_builder;
86  function.body.output_instruction(
87  ns, function_name, instruction_builder, instruction);
88 
89  instruction_entry["instruction"]=
90  json_stringt(instruction_builder.str());
91 
92  if(!instruction.code.operands().empty())
93  {
94  json_arrayt operand_array;
95  for(const exprt &operand : instruction.code.operands())
96  {
97  json_objectt operand_object=
98  no_comments_irep_converter.convert_from_irep(
99  operand);
100  operand_array.push_back(operand_object);
101  }
102  instruction_entry["operands"]=operand_array;
103  }
104 
105  if(!instruction.guard.is_true())
106  {
107  json_objectt guard_object=
108  no_comments_irep_converter.convert_from_irep(
109  instruction.guard);
110 
111  instruction_entry["guard"]=guard_object;
112  }
113 
114  json_instruction_array.push_back(instruction_entry);
115  }
116 
117  json_function["instructions"]=json_instruction_array;
118  }
119  }
120 
121  json_objectt json_result;
122  json_result["functions"]=json_functions;
123 
124  return json_result;
125 }
126 
135  const goto_functionst &goto_functions,
136  std::ostream &out,
137  bool append)
138 {
139  if(append)
140  {
141  out << ",\n";
142  }
143  out << convert(goto_functions);
144 }
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
std::string to_string() const
Definition: goto_program.h:391
#define CPROVER_PREFIX
Goto Programs with Functions.
Definition: json.h:23
static jsont json_boolean(bool value)
Definition: json.h:85
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
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...
show_goto_functions_jsont(const namespacet &_ns, bool _list_only=false)
For outputting the GOTO program in a readable JSON format.
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
jsont & push_back(const jsont &json)
Definition: json.h:163
Symbol Table + CFG.
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...
Expressions in JSON.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:33
Base class for all expressions.
Definition: expr.h:54
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
const source_locationt & source_location() const
Definition: expr.h:228
json_objectt & make_object()
Definition: json.h:290
operandst & operands()
Definition: expr.h:78
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87