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_irep.h>
18 #include <util/cprover_prefix.h>
19 #include <util/prefix.h>
20 
21 #include <langapi/language_util.h>
22 
23 #include "goto_functions.h"
24 #include "goto_model.h"
25 
30  const namespacet &_ns,
31  bool _list_only)
32  : ns(_ns), list_only(_list_only)
33 {}
34 
39  const goto_functionst &goto_functions)
40 {
41  json_arrayt json_functions;
42  const json_irept no_comments_irep_converter(false);
43 
44  const auto sorted = goto_functions.sorted();
45 
46  for(const auto &function_entry : sorted)
47  {
48  const irep_idt &function_name = function_entry->first;
49  const goto_functionst::goto_functiont &function = function_entry->second;
50 
51  json_objectt &json_function=
52  json_functions.push_back(jsont()).make_object();
53  json_function["name"] = json_stringt(function_name);
54  json_function["isBodyAvailable"]=
55  jsont::json_boolean(function.body_available());
56  bool is_internal=
57  has_prefix(id2string(function_name), CPROVER_PREFIX) ||
58  has_prefix(id2string(function_name), "java::array[") ||
59  has_prefix(id2string(function_name), "java::org.cprover") ||
60  has_prefix(id2string(function_name), "java::java");
61  json_function["isInternal"]=jsont::json_boolean(is_internal);
62 
63  if(list_only)
64  continue;
65 
66  if(function.body_available())
67  {
68  json_arrayt json_instruction_array=json_arrayt();
69 
70  for(const goto_programt::instructiont &instruction :
71  function.body.instructions)
72  {
73  json_objectt instruction_entry{
74  {"instructionId", json_stringt(instruction.to_string())}};
75 
76  if(instruction.code.source_location().is_not_nil())
77  {
78  instruction_entry["sourceLocation"]=
79  json(instruction.code.source_location());
80  }
81 
82  std::ostringstream instruction_builder;
83  function.body.output_instruction(
84  ns, function_name, instruction_builder, instruction);
85 
86  instruction_entry["instruction"]=
87  json_stringt(instruction_builder.str());
88 
89  if(!instruction.code.operands().empty())
90  {
91  json_arrayt operand_array;
92  for(const exprt &operand : instruction.code.operands())
93  {
94  json_objectt operand_object=
95  no_comments_irep_converter.convert_from_irep(
96  operand);
97  operand_array.push_back(operand_object);
98  }
99  instruction_entry["operands"] = std::move(operand_array);
100  }
101 
102  if(!instruction.guard.is_true())
103  {
104  json_objectt guard_object=
105  no_comments_irep_converter.convert_from_irep(
106  instruction.guard);
107 
108  instruction_entry["guard"] = std::move(guard_object);
109  }
110 
111  json_instruction_array.push_back(std::move(instruction_entry));
112  }
113 
114  json_function["instructions"] = std::move(json_instruction_array);
115  }
116  }
117 
118  return json_objectt({{"functions", json_functions}});
119 }
120 
129  const goto_functionst &goto_functions,
130  std::ostream &out,
131  bool append)
132 {
133  if(append)
134  {
135  out << ",\n";
136  }
137  out << convert(goto_functions);
138 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
show_goto_functions_jsont::show_goto_functions_jsont
show_goto_functions_jsont(const namespacet &_ns, bool _list_only=false)
For outputting the GOTO program in a readable JSON format.
Definition: show_goto_functions_json.cpp:29
show_goto_functions_json.h
Goto Program.
goto_programt::instructiont::to_string
std::string to_string() const
Definition: goto_program.h:549
show_goto_functions_jsont::ns
const namespacet & ns
Definition: show_goto_functions_json.h:32
prefix.h
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
jsont::make_object
json_objectt & make_object()
Definition: json.h:438
jsont
Definition: json.h:27
json_irep.h
Util.
json_arrayt
Definition: json.h:165
json_objectt
Definition: json.h:300
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
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
language_util.h
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
show_goto_functions_jsont::convert
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...
Definition: show_goto_functions_json.cpp:38
show_goto_functions_jsont::operator()
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...
Definition: show_goto_functions_json.cpp:128
json_irept::convert_from_irep
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
cprover_prefix.h
show_goto_functions_jsont::list_only
bool list_only
Definition: show_goto_functions_json.h:33
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_programt::instructiont::guard
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
Definition: goto_program.h:276
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functions.h
Goto Programs with Functions.
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
json_irept
Definition: json_irep.h:21
exprt::operands
operandst & operands()
Definition: expr.h:95
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
goto_functionst::sorted
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
Definition: goto_functions.cpp:62
jsont::json_boolean
static jsont json_boolean(bool value)
Definition: json.h:97
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
json_stringt
Definition: json.h:270