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(const auto &class_ref : class_refs)
27  out << " " << class_ref << '\n';
28 }
29 
30 void java_bytecode_parse_treet::classt::output(std::ostream &out) const
31 {
32  for(const auto &annotation : annotations)
33  {
34  annotation.output(out);
35  out << '\n';
36  }
37 
38  out << "class " << name;
39  if(!super_class.empty())
40  out << " extends " << super_class;
41  out << " {" << '\n';
42 
43  for(const auto &field : fields)
44  field.output(out);
45 
46  out << '\n';
47 
48  for(const auto &method : methods)
49  method.output(out);
50 
51  out << '}' << '\n';
52  out << '\n';
53 }
54 
56 {
57  symbol_tablet symbol_table;
58  namespacet ns(symbol_table);
59 
60  out << '@' << type2java(type, ns);
61 
62  if(!element_value_pairs.empty())
63  {
64  out << '(';
65 
66  bool first=true;
67  for(const auto &element_value_pair : element_value_pairs)
68  {
69  if(first)
70  first=false;
71  else
72  out << ", ";
73  element_value_pair.output(out);
74  }
75 
76  out << ')';
77  }
78 }
79 
81  std::ostream &out) const
82 {
83  symbol_tablet symbol_table;
84  namespacet ns(symbol_table);
85 
86  out << '"' << element_name << '"' << '=';
87  out << expr2java(value, ns);
88 }
89 
98  const annotationst &annotations,
99  const irep_idt &annotation_type_name)
100 {
101  const auto annotation_it = std::find_if(
102  annotations.begin(),
103  annotations.end(),
104  [&annotation_type_name](const annotationt &annotation) {
105  if(annotation.type.id() != ID_pointer)
106  return false;
107  const typet &type = annotation.type.subtype();
108  return type.id() == ID_struct_tag &&
109  to_struct_tag_type(type).get_identifier() == annotation_type_name;
110  });
111  if(annotation_it == annotations.end())
112  return {};
113  return *annotation_it;
114 }
115 
116 void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
117 {
118  symbol_tablet symbol_table;
119  namespacet ns(symbol_table);
120 
121  for(const auto &annotation : annotations)
122  {
123  out << " ";
124  annotation.output(out);
125  out << '\n';
126  }
127 
128  out << " ";
129 
130  if(is_public)
131  out << "public ";
132 
133  if(is_protected)
134  out << "protected ";
135 
136  if(is_private)
137  out << "private ";
138 
139  if(is_static)
140  out << "static ";
141 
142  if(is_final)
143  out << "final ";
144 
145  if(is_native)
146  out << "native ";
147 
148  if(is_synchronized)
149  out << "synchronized ";
150 
151  out << name;
152  out << " : " << descriptor;
153 
154  out << '\n';
155 
156  out << " {" << '\n';
157 
158  for(const auto &i : instructions)
159  {
160  if(!i.source_location.get_line().empty())
161  out << " // " << i.source_location << '\n';
162 
163  out << " " << i.address << ": ";
164  out << bytecode_info[i.bytecode].mnemonic;
165 
166  bool first = true;
167  for(const auto &arg : i.args)
168  {
169  if(first)
170  first = false;
171  else
172  out << ',';
173 #if 0
174  out << ' ' << from_expr(arg);
175 #else
176  out << ' ' << expr2java(arg, ns);
177 #endif
178  }
179 
180  out << '\n';
181  }
182 
183  out << " }" << '\n';
184 
185  out << '\n';
186 
187  out << " Locals:\n";
188  for(const auto &v : local_variable_table)
189  {
190  out << " " << v.index << ": " << v.name << ' '
191  << v.descriptor << '\n';
192  }
193 
194  out << '\n';
195 }
196 
197 void java_bytecode_parse_treet::fieldt::output(std::ostream &out) const
198 {
199  for(const auto &annotation : annotations)
200  {
201  out << " ";
202  annotation.output(out);
203  out << '\n';
204  }
205 
206  out << " ";
207 
208  if(is_public)
209  out << "public ";
210 
211  if(is_static)
212  out << "static ";
213 
214  out << name;
215  out << " : " << descriptor << ';';
216 
217  out << '\n';
218 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
bytecode_infot::mnemonic
const char * mnemonic
Definition: bytecode_info.h:46
java_bytecode_parse_treet::annotationt::output
void output(std::ostream &) const
Definition: java_bytecode_parse_tree.cpp:55
java_bytecode_parse_treet::annotationt::element_value_pairt::output
void output(std::ostream &) const
Definition: java_bytecode_parse_tree.cpp:80
java_bytecode_parse_treet::annotationst
std::vector< annotationt > annotationst
Definition: java_bytecode_parse_tree.h:50
java_bytecode_parse_treet::find_annotation
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
Definition: java_bytecode_parse_tree.cpp:97
java_bytecode_parse_treet::fieldt::output
void output(std::ostream &out) const
Definition: java_bytecode_parse_tree.cpp:197
namespace.h
java_bytecode_parse_treet::classt::annotations
annotationst annotations
Definition: java_bytecode_parse_tree.h:282
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
java_bytecode_parse_treet::annotationt
Definition: java_bytecode_parse_tree.h:34
java_bytecode_parse_treet::methodt::output
void output(std::ostream &out) const
Definition: java_bytecode_parse_tree.cpp:116
language_util.h
java_bytecode_parse_treet::classt::name
irep_idt name
Definition: java_bytecode_parse_tree.h:213
java_bytecode_parse_tree.h
java_bytecode_parse_treet::classt::output
void output(std::ostream &out) const
Definition: java_bytecode_parse_tree.cpp:30
java_bytecode_parse_treet::class_refs
class_refst class_refs
Definition: java_bytecode_parse_tree.h:317
dstringt::empty
bool empty() const
Definition: dstring.h:88
java_bytecode_parse_treet::output
void output(std::ostream &out) const
Definition: java_bytecode_parse_tree.cpp:21
java_bytecode_parse_treet::classt::methods
methodst methods
Definition: java_bytecode_parse_tree.h:281
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_bytecode_parse_treet::classt::fields
fieldst fields
Definition: java_bytecode_parse_tree.h:280
java_bytecode_parse_treet::parsed_class
classt parsed_class
Definition: java_bytecode_parse_tree.h:311
type2java
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:462
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:455
expr2java.h
symbol_table.h
Author: Diffblue Ltd.
bytecode_info
struct bytecode_infot const bytecode_info[]
Definition: bytecode_info.cpp:16
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
java_bytecode_parse_treet::classt::super_class
irep_idt super_class
Definition: java_bytecode_parse_tree.h:213