CBMC
json_irep.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Util
4 
5 Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "json_irep.h"
13 
14 #include "exception_utils.h"
15 #include "irep.h"
16 #include "json.h"
17 
22 json_irept::json_irept(bool _include_comments):
23  include_comments(_include_comments)
24 {
25 }
26 
32 {
33  json_objectt irep_object;
34 
35  irep_object["id"] = json_stringt(irep.id_string());
36 
37  convert_sub_tree("sub", irep.get_sub(), irep_object);
38  convert_named_sub_tree("namedSub", irep.get_named_sub(), irep_object);
39 
40  return irep_object;
41 }
42 
49 
51  const std::string &sub_tree_id,
52  const irept::subt &sub_trees,
53  json_objectt &parent) const
54 {
55  if(!sub_trees.empty())
56  {
57  json_arrayt sub_objects;
58  for(const irept &sub_tree : sub_trees)
59  {
60  json_objectt sub_object=convert_from_irep(sub_tree);
61  sub_objects.push_back(sub_object);
62  }
63  parent[sub_tree_id]=sub_objects;
64  }
65 }
66 
75  const std::string &sub_tree_id,
76  const irept::named_subt &sub_trees,
77  json_objectt &parent) const
78 {
79  if(!sub_trees.empty())
80  {
81  json_objectt sub_objects;
82  for(const auto &sub_tree : sub_trees)
83  if(include_comments || !irept::is_comment(sub_tree.first))
84  {
85  json_objectt sub_object = convert_from_irep(sub_tree.second);
86  sub_objects[id2string(sub_tree.first)] = sub_object;
87  }
88  parent[sub_tree_id]=sub_objects;
89  }
90 }
91 
96 {
97  if(!in.is_object())
98  {
100  "irep JSON representation must be an object");
101  }
102 
103  const json_objectt &json_object = to_json_object(in);
104 
105  irept out;
106 
107  {
108  const auto it = json_object.find("id");
109 
110  if(it != json_object.end())
111  {
112  out.id(it->second.value);
113  }
114  }
115 
116  {
117  const auto it = json_object.find("sub");
118 
119  if(it != json_object.end())
120  {
121  for(const auto &sub : to_json_array(it->second))
122  out.get_sub().push_back(convert_from_json(sub));
123  }
124  }
125 
126  {
127  const auto it = json_object.find("namedSub");
128 
129  if(it != json_object.end())
130  {
131  for(const auto &named_sub : to_json_object(it->second))
132  out.add(named_sub.first) = convert_from_json(named_sub.second);
133  }
134  }
135 
136  return out;
137 }
138 
140 {
141  json_objectt result;
142 
143  if(!location.get_working_directory().empty())
144  result["workingDirectory"] = json_stringt(location.get_working_directory());
145 
146  if(!location.get_file().empty())
147  result["file"] = json_stringt(location.get_file());
148 
149  if(!location.get_line().empty())
150  result["line"] = json_stringt(location.get_line());
151 
152  if(!location.get_column().empty())
153  result["column"] = json_stringt(location.get_column());
154 
155  if(!location.get_function().empty())
156  result["function"] = json_stringt(location.get_function());
157 
158  if(!location.get_java_bytecode_index().empty())
159  result["bytecodeIndex"] = json_stringt(location.get_java_bytecode_index());
160 
161  return result;
162 }
exception_utils.h
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:55
json_irept::include_comments
bool include_comments
Definition: json_irep.h:38
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition: exception_utils.h:79
json_objectt::find
iterator find(const std::string &key)
Definition: json.h:356
source_locationt::get_column
const irep_idt & get_column() const
Definition: source_location.h:50
sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::named_subt
typename dt::named_subt named_subt
Definition: irep.h:161
to_json_array
json_arrayt & to_json_array(jsont &json)
Definition: json.h:426
jsont
Definition: json.h:26
json_irep.h
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:45
json_arrayt
Definition: json.h:164
json_objectt
Definition: json.h:299
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
irept::get_named_sub
named_subt & get_named_sub()
Definition: irep.h:458
irept::id_string
const std::string & id_string() const
Definition: irep.h:399
irept::id
const irep_idt & id() const
Definition: irep.h:396
dstringt::empty
bool empty() const
Definition: dstring.h:88
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:31
sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::subt
typename dt::subt subt
Definition: irep.h:160
json_irept::convert_named_sub_tree
void convert_named_sub_tree(const std::string &sub_tree_id, const irept::named_subt &sub_trees, json_objectt &parent) const
To convert to JSON from a map of ireps that are in a named subtree.
Definition: json_irep.cpp:74
source_locationt
Definition: source_location.h:18
json_irept::convert_sub_tree
void convert_sub_tree(const std::string &sub_tree_id, const irept::subt &sub_trees, json_objectt &parent) const
To convert to JSON from a list of ireps that are in an unlabelled subtree.
Definition: json_irep.cpp:50
source_locationt::get_java_bytecode_index
const irep_idt & get_java_bytecode_index() const
Definition: source_location.h:80
json_objectt::end
iterator end()
Definition: json.h:386
irept::add
irept & add(const irep_idt &name)
Definition: irep.cpp:116
to_json_object
json_objectt & to_json_object(jsont &json)
Definition: json.h:444
json_irept::json_irept
json_irept(bool include_comments)
To convert to JSON from an irep structure by recursively generating JSON for the different sub trees.
Definition: json_irep.cpp:22
irept::get_sub
subt & get_sub()
Definition: irep.h:456
json.h
json
json_objectt json(const source_locationt &location)
Definition: json_irep.cpp:139
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:35
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:359
jsont::is_object
bool is_object() const
Definition: json.h:56
source_locationt::get_working_directory
const irep_idt & get_working_directory() const
Definition: source_location.h:40
irept::is_comment
static bool is_comment(const irep_idt &name)
Definition: irep.h:468
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
irep.h
json_irept::convert_from_json
irept convert_from_json(const jsont &) const
Deserialize a JSON irep representation.
Definition: json_irep.cpp:95
json_stringt
Definition: json.h:269