Skip to content

Commit 63e0a3e

Browse files
author
thk123
committed
Wrote an irep to JSON converter
Use this converter in the show_goto_functions_json to provide more information.
1 parent ecca997 commit 63e0a3e

File tree

4 files changed

+182
-1
lines changed

4 files changed

+182
-1
lines changed

src/goto-programs/show_goto_functions_json.cpp

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Author: Thomas Kiley
1010
#include <sstream>
1111

1212
#include <util/json_expr.h>
13+
#include <util/json_irep.h>
1314
#include <util/cprover_prefix.h>
1415
#include <util/prefix.h>
1516

@@ -54,6 +55,7 @@ json_objectt show_goto_functions_jsont::get_goto_functions(
5455
const goto_functionst &goto_functions)
5556
{
5657
json_arrayt json_functions;
58+
const json_irept no_comments_irep_converter(false);
5759
for(const auto &function_entry : goto_functions.function_map)
5860
{
5961
const irep_idt &function_name=function_entry.first;
@@ -93,6 +95,16 @@ json_objectt show_goto_functions_jsont::get_goto_functions(
9395
instruction_entry["instruction"]=
9496
json_stringt(instruction_builder.str());
9597

98+
json_arrayt operand_array;
99+
for(const exprt &operand : instruction.code.operands())
100+
{
101+
json_objectt operand_object;
102+
no_comments_irep_converter.convert_from_irep(operand, operand_object);
103+
operand_array.push_back(operand_object);
104+
}
105+
106+
instruction_entry["operands"]=operand_array;
107+
96108
json_instruction_array.push_back(instruction_entry);
97109
}
98110

src/util/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \
2121
bv_arithmetic.cpp tempdir.cpp tempfile.cpp timer.cpp unicode.cpp \
2222
irep_ids.cpp byte_operators.cpp string2int.cpp file_util.cpp \
2323
memory_info.cpp pipe_stream.cpp irep_hash.cpp endianness_map.cpp \
24-
ssa_expr.cpp json_expr.cpp \
24+
ssa_expr.cpp json_irep.cpp json_expr.cpp \
2525
string_utils.cpp
2626

2727
INCLUDES= -I ..

src/util/json_irep.cpp

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
/*******************************************************************\
2+
3+
Module: Util
4+
5+
Author: Thomas Kiley, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "irep.h"
10+
#include "json.h"
11+
#include "json_irep.h"
12+
13+
/*******************************************************************\
14+
15+
Function: json_irept::json_irept
16+
17+
Inputs:
18+
include_comments - when generating the JSON, should the comments
19+
sub tree be included.
20+
21+
Outputs:
22+
23+
Purpose: To convert to JSON from an irep structure by recurssively
24+
generating JSON for the different sub trees.
25+
26+
\*******************************************************************/
27+
28+
json_irept::json_irept(bool include_comments):
29+
include_comments(include_comments)
30+
{}
31+
32+
/*******************************************************************\
33+
34+
Function: json_irept::convert_from_irep
35+
36+
Inputs:
37+
irep - The irep structure to turn into json
38+
json - The json object to be filled up.
39+
40+
Outputs:
41+
42+
Purpose: To convert to JSON from an irep structure by recurssively
43+
generating JSON for the different sub trees.
44+
45+
\*******************************************************************/
46+
47+
void json_irept::convert_from_irep(const irept &irep, jsont &json) const
48+
{
49+
json_objectt &irep_object=json.make_object();
50+
if(irep.id()!=ID_nil)
51+
irep_object["id"]=json_stringt(irep.id_string());
52+
53+
convert_sub_tree("sub", irep.get_sub(), irep_object);
54+
convert_named_sub_tree("named_sub", irep.get_named_sub(), irep_object);
55+
if(include_comments)
56+
{
57+
convert_named_sub_tree("comment", irep.get_comments(), irep_object);
58+
}
59+
}
60+
61+
/*******************************************************************\
62+
63+
Function: json_irept::convert_sub_tree
64+
65+
Inputs:
66+
sub_tree_id - the name to give the subtree in the parent object
67+
sub_trees - the list of subtrees to parse
68+
parent - the parent JSON object who should be added to
69+
70+
Outputs:
71+
72+
Purpose: To convert to JSON from a list of ireps that are in an
73+
unlabelled subtree. The parent JSON object will get a key
74+
called sub_tree_id and the value shall be an array of JSON
75+
objects generated from each of the sub trees
76+
77+
\*******************************************************************/
78+
79+
void json_irept::convert_sub_tree(
80+
const std::string &sub_tree_id,
81+
const irept::subt &sub_trees,
82+
json_objectt &parent) const
83+
{
84+
if(sub_trees.size()>0)
85+
{
86+
json_arrayt sub_objects;
87+
for(const irept &sub_tree : sub_trees)
88+
{
89+
json_objectt sub_object;
90+
convert_from_irep(sub_tree, sub_object);
91+
sub_objects.push_back(sub_object);
92+
}
93+
parent[sub_tree_id]=sub_objects;
94+
}
95+
}
96+
97+
/*******************************************************************\
98+
99+
Function: json_irept::convert_named_sub_tree
100+
101+
Inputs:
102+
sub_tree_id - the name to give the subtree in the parent object
103+
sub_trees - the map of subtrees to parse
104+
parent - the parent JSON object who should be added to
105+
106+
Outputs:
107+
108+
Purpose: To convert to JSON from a map of ireps that are in a
109+
named subtree. The parent JSON object will get a key
110+
called sub_tree_id and the value shall be a JSON object
111+
whose keys shall be the name of the sub tree and the value
112+
will be the object generated from the sub tree.
113+
114+
\*******************************************************************/
115+
116+
void json_irept::convert_named_sub_tree(
117+
const std::string &sub_tree_id,
118+
const irept::named_subt &sub_trees,
119+
json_objectt &parent) const
120+
{
121+
if(sub_trees.size()>0)
122+
{
123+
json_objectt sub_objects;
124+
for(const auto &sub_tree : sub_trees)
125+
{
126+
json_objectt sub_object;
127+
convert_from_irep(sub_tree.second, sub_object);
128+
sub_objects[id2string(sub_tree.first)]=sub_object;
129+
}
130+
parent[sub_tree_id]=sub_objects;
131+
}
132+
}
133+

src/util/json_irep.h

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
/*******************************************************************\
2+
3+
Module: Util
4+
5+
Author: Thomas Kiley, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_UTIL_JSON_IREP_H
10+
#define CPROVER_UTIL_JSON_IREP_H
11+
12+
#include <util/irep.h>
13+
class jsont;
14+
class json_objectt;
15+
16+
class json_irept
17+
{
18+
public:
19+
explicit json_irept(bool include_comments);
20+
void convert_from_irep(const irept &irep, jsont &json) const;
21+
22+
private:
23+
void convert_sub_tree(
24+
const std::string &sub_tree_id,
25+
const irept::subt &sub_trees,
26+
json_objectt &parent) const;
27+
28+
void convert_named_sub_tree(
29+
const std::string &sub_tree_id,
30+
const irept::named_subt &sub_trees,
31+
json_objectt &parent) const;
32+
33+
bool include_comments;
34+
};
35+
36+
#endif // CPROVER_UTIL_JSON_IREP_H

0 commit comments

Comments
 (0)