cprover
java_bytecode_parse_tree.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
10 
11 #include <algorithm>
12 #include <ostream>
13 
14 #include <util/symbol_table.h>
15 #include <util/namespace.h>
16 
17 #include <langapi/language_util.h>
18 
19 #include "expr2java.h"
20 
21 void java_bytecode_parse_treet::output(std::ostream &out) const
22 {
23  parsed_class.output(out);
24 
25  out << "Class references:\n";
26  for(class_refst::const_iterator it=class_refs.begin();
27  it!=class_refs.end();
28  it++)
29  out << " " << *it << '\n';
30 }
31 
32 void java_bytecode_parse_treet::classt::output(std::ostream &out) const
33 {
34  for(const auto &annotation : annotations)
35  {
36  annotation.output(out);
37  out << '\n';
38  }
39 
40  out << "class " << name;
41  if(!extends.empty())
42  out << " extends " << extends;
43  out << " {" << '\n';
44 
45  for(fieldst::const_iterator
46  it=fields.begin();
47  it!=fields.end();
48  it++)
49  {
50  it->output(out);
51  }
52 
53  out << '\n';
54 
55  for(methodst::const_iterator
56  it=methods.begin();
57  it!=methods.end();
58  it++)
59  {
60  it->output(out);
61  }
62 
63  out << '}' << '\n';
64  out << '\n';
65 }
66 
68 {
69  symbol_tablet symbol_table;
70  namespacet ns(symbol_table);
71 
72  out << '@' << type2java(type, ns);
73 
74  if(!element_value_pairs.empty())
75  {
76  out << '(';
77 
78  bool first=true;
79  for(const auto &element_value_pair : element_value_pairs)
80  {
81  if(first)
82  first=false;
83  else
84  out << ", ";
85  element_value_pair.output(out);
86  }
87 
88  out << ')';
89  }
90 }
91 
93  std::ostream &out) const
94 {
95  symbol_tablet symbol_table;
96  namespacet ns(symbol_table);
97 
98  out << '"' << element_name << '"' << '=';
99  out << expr2java(value, ns);
100 }
101 
110  const annotationst &annotations,
111  const irep_idt &annotation_type_name)
112 {
113  const auto annotation_it = std::find_if(
114  annotations.begin(),
115  annotations.end(),
116  [&annotation_type_name](const annotationt &annotation) {
117  if(annotation.type.id() != ID_pointer)
118  return false;
119  const typet &type = annotation.type.subtype();
120  return type.id() == ID_symbol &&
121  to_symbol_type(type).get_identifier() == annotation_type_name;
122  });
123  if(annotation_it == annotations.end())
124  return {};
125  return *annotation_it;
126 }
127 
128 void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
129 {
130  symbol_tablet symbol_table;
131  namespacet ns(symbol_table);
132 
133  for(const auto &annotation : annotations)
134  {
135  out << " ";
136  annotation.output(out);
137  out << '\n';
138  }
139 
140  out << " ";
141 
142  if(is_public)
143  out << "public ";
144 
145  if(is_protected)
146  out << "protected ";
147 
148  if(is_private)
149  out << "private ";
150 
151  if(is_static)
152  out << "static ";
153 
154  if(is_final)
155  out << "final ";
156 
157  if(is_native)
158  out << "native ";
159 
160  if(is_synchronized)
161  out << "synchronized ";
162 
163  out << name;
164  out << " : " << descriptor;
165 
166  out << '\n';
167 
168  out << " {" << '\n';
169 
170  for(const auto &i : instructions)
171  {
172  if(!i.source_location.get_line().empty())
173  out << " // " << i.source_location << '\n';
174 
175  out << " " << i.address << ": ";
176  out << i.statement;
177 
178  for(std::vector<exprt>::const_iterator
179  a_it=i.args.begin(); a_it!=i.args.end(); a_it++)
180  {
181  if(a_it!=i.args.begin())
182  out << ',';
183  #if 0
184  out << ' ' << from_expr(*a_it);
185  #else
186  out << ' ' << expr2java(*a_it, ns);
187  #endif
188  }
189 
190  out << '\n';
191  }
192 
193  out << " }" << '\n';
194 
195  out << '\n';
196 
197  out << " Locals:\n";
198  for(const auto &v : local_variable_table)
199  {
200  out << " " << v.index << ": " << v.name << ' '
201  << v.descriptor << '\n';
202  }
203 
204  out << '\n';
205 }
206 
207 void java_bytecode_parse_treet::fieldt::output(std::ostream &out) const
208 {
209  for(const auto &annotation : annotations)
210  {
211  out << " ";
212  annotation.output(out);
213  out << '\n';
214  }
215 
216  out << " ";
217 
218  if(is_public)
219  out << "public ";
220 
221  if(is_static)
222  out << "static ";
223 
224  out << name;
225  out << " : " << descriptor << ';';
226 
227  out << '\n';
228 }
The type of an expression.
Definition: type.h:22
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:462
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
virtual void output(std::ostream &out) const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
std::vector< annotationt > annotationst
const irep_idt & id() const
Definition: irep.h:189
nonstd::optional< T > optionalt
Definition: optional.h:35
The symbol table.
Definition: symbol_table.h:19
void output(std::ostream &out) const
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Author: Diffblue Ltd.
void output(std::ostream &out) const
virtual void output(std::ostream &out) const
const typet & subtype() const
Definition: type.h:33
bool empty() const
Definition: dstring.h:61
const irep_idt & get_identifier() const
Definition: std_types.h:123
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:455