Skip to content

Commit 3b3fee3

Browse files
authored
Revert "TG-374 Feature/java support generics"
1 parent 0e14431 commit 3b3fee3

21 files changed

+49
-1015
lines changed

regression/cbmc-java/enum1/test.desc

+1-3
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
enum1.class
33
--java-unwind-enum-static --unwind 3
44
^VERIFICATION SUCCESSFUL$
@@ -7,5 +7,3 @@ enum1.class
77
^Unwinding loop java::enum1.<clinit>:\(\)V.0 iteration 5 \(6 max\) file enum1.java line 6 function java::enum1.<clinit>:\(\)V bytecode-index 78 thread 0$
88
--
99
^warning: ignoring
10-
--
11-
cf. https://diffblue.atlassian.net/browse/TG-611
+2-4
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,8 @@
1-
KNOWNBUG
1+
CORE
22
iterator2.class
3-
--cover location --unwind 3 --function iterator2.f
3+
--cover location --unwind 3 --function iterator2.f
44
^EXIT=0$
55
^SIGNAL=0$
66
^.*SATISFIED$
77
--
88
^warning: ignoring
9-
--
10-
https://diffblue.atlassian.net/browse/TG-610
+1-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
1-
KNOWNBUG
1+
CORE
22
DetectSplitPackagesTask.class
33
--show-symbol-table
44
^EXIT=0$
55
^SIGNAL=0$
66
--
77
--
8-
cf. https://diffblue.atlassian.net/browse/TG-610

src/java_bytecode/ci_lazy_methods.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ bool ci_lazy_methodst::operator()(
7979
{
8080
const irep_idt methodid="java::"+id2string(classname)+"."+
8181
id2string(method.name)+":"+
82-
id2string(method.descriptor);
82+
id2string(method.signature);
8383
method_worklist2.push_back(methodid);
8484
}
8585
}
@@ -505,3 +505,4 @@ irep_idt ci_lazy_methodst::get_virtual_method_target(
505505
else
506506
return irep_idt();
507507
}
508+

src/java_bytecode/java_bytecode_convert_class.cpp

+2-63
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ Author: Daniel Kroening, [email protected]
2121
#include "java_bytecode_language.h"
2222
#include "java_utils.h"
2323

24-
#include <util/c_types.h>
2524
#include <util/arith_tools.h>
2625
#include <util/namespace.h>
2726
#include <util/std_expr.h>
@@ -102,25 +101,6 @@ void java_bytecode_convert_classt::convert(const classt &c)
102101
}
103102

104103
java_class_typet class_type;
105-
if(c.signature.has_value())
106-
{
107-
java_generics_class_typet generic_class_type;
108-
#ifdef DEBUG
109-
std::cout << "INFO: found generic class signature "
110-
<< c.signature.value()
111-
<< " in parsed class "
112-
<< c.name << "\n";
113-
#endif
114-
for(auto t : java_generic_type_from_string(
115-
id2string(c.name),
116-
c.signature.value()))
117-
{
118-
generic_class_type.generic_types()
119-
.push_back(to_java_generic_parameter(t));
120-
}
121-
122-
class_type=generic_class_type;
123-
}
124104

125105
class_type.set_tag(c.name);
126106
class_type.set(ID_base_name, c.name);
@@ -194,7 +174,7 @@ void java_bytecode_convert_classt::convert(const classt &c)
194174
const irep_idt method_identifier=
195175
id2string(qualified_classname)+
196176
"."+id2string(method.name)+
197-
":"+method.descriptor;
177+
":"+method.signature;
198178
// Always run the lazy pre-stage, as it symbol-table
199179
// registers the function.
200180
debug() << "Adding symbol: method '" << method_identifier << "'" << eom;
@@ -215,48 +195,7 @@ void java_bytecode_convert_classt::convert(
215195
symbolt &class_symbol,
216196
const fieldt &f)
217197
{
218-
typet field_type;
219-
if(f.signature.has_value())
220-
{
221-
field_type=java_type_from_string(
222-
f.signature.value(),
223-
id2string(class_symbol.name));
224-
225-
/// this is for a free type variable, e.g., a field of the form `T f;`
226-
if(is_java_generic_parameter(field_type))
227-
{
228-
#ifdef DEBUG
229-
std::cout << "fieldtype: generic "
230-
<< to_java_generic_parameter(field_type).type_variable()
231-
.get_identifier()
232-
<< " name " << f.name << "\n";
233-
#endif
234-
}
235-
236-
/// this is for a field that holds a generic type, wither with instantiated
237-
/// or with free type variables, e.g., `List<T> l;` or `List<Integer> l;`
238-
else if(is_java_generic_type(field_type))
239-
{
240-
java_generic_typet &with_gen_type=
241-
to_java_generic_type(field_type);
242-
#ifdef DEBUG
243-
std::cout << "fieldtype: generic container type "
244-
<< std::to_string(with_gen_type.generic_type_variables().size())
245-
<< " type " << with_gen_type.id()
246-
<< " name " << f.name
247-
<< " subtype id " << with_gen_type.subtype().id() << "\n";
248-
#endif
249-
field_type=with_gen_type;
250-
}
251-
252-
/// This case is not possible, a field is either a non-instantiated type
253-
/// variable or a generics container type.
254-
INVARIANT(
255-
!is_java_generic_inst_parameter(field_type),
256-
"Cannot be an instantiated type variable here.");
257-
}
258-
else
259-
field_type=java_type_from_string(f.descriptor);
198+
typet field_type=java_type_from_string(f.signature);
260199

261200
// is this a static field?
262201
if(f.is_static)

src/java_bytecode/java_bytecode_convert_method.cpp

+4-25
Original file line numberDiff line numberDiff line change
@@ -252,7 +252,7 @@ const exprt java_bytecode_convert_methodt::variable(
252252
/// method conversion just yet. The caller should call
253253
/// java_bytecode_convert_method later to give the symbol/method a body.
254254
/// \par parameters: `class_symbol`: class this method belongs to
255-
/// `method_identifier`: fully qualified method name, including type descriptor
255+
/// `method_identifier`: fully qualified method name, including type signature
256256
/// (e.g. "x.y.z.f:(I)")
257257
/// `m`: parsed method object to convert
258258
/// `symbol_table`: global symbol table (will be modified)
@@ -263,19 +263,7 @@ void java_bytecode_convert_method_lazy(
263263
symbol_tablet &symbol_table)
264264
{
265265
symbolt method_symbol;
266-
typet member_type;
267-
if(m.signature.has_value())
268-
{
269-
#ifdef DEBUG
270-
std::cout << "method " << m.name
271-
<< " has signature " << m.signature.value() << "\n";
272-
#endif
273-
member_type=java_type_from_string(
274-
m.signature.value(),
275-
id2string(class_symbol.name));
276-
}
277-
else
278-
member_type=java_type_from_string(m.descriptor);
266+
typet member_type=java_type_from_string(m.signature);
279267

280268
method_symbol.name=method_identifier;
281269
method_symbol.base_name=m.base_name;
@@ -329,7 +317,7 @@ void java_bytecode_convert_methodt::convert(
329317
// to retrieve the symbol (constructed by java_bytecode_convert_method_lazy)
330318
// associated to the method
331319
const irep_idt method_identifier=
332-
id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.descriptor;
320+
id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.signature;
333321
method_id=method_identifier;
334322

335323
const auto &old_sym=symbol_table.lookup(method_identifier);
@@ -362,16 +350,7 @@ void java_bytecode_convert_methodt::convert(
362350
// Construct a fully qualified name for the parameter v,
363351
// e.g. my.package.ClassName.myMethodName:(II)I::anIntParam, and then a
364352
// symbol_exprt with the parameter and its type
365-
typet t;
366-
if(v.signature.has_value())
367-
{
368-
t=java_type_from_string(
369-
v.signature.value(),
370-
id2string(class_symbol.name));
371-
}
372-
else
373-
t=java_type_from_string(v.descriptor);
374-
353+
typet t=java_type_from_string(v.signature);
375354
std::ostringstream id_oss;
376355
id_oss << method_id << "::" << v.name;
377356
irep_idt identifier(id_oss.str());

src/java_bytecode/java_bytecode_parse_tree.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@ void java_bytecode_parse_treet::classt::swap(
2828
std::swap(other.is_public, is_public);
2929
std::swap(other.is_protected, is_protected);
3030
std::swap(other.is_private, is_private);
31-
std::swap(other.signature, signature);
3231
other.implements.swap(implements);
3332
other.fields.swap(fields);
3433
other.methods.swap(methods);
@@ -152,7 +151,7 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
152151
out << "synchronized ";
153152

154153
out << name;
155-
out << " : " << descriptor;
154+
out << " : " << signature;
156155

157156
out << '\n';
158157

@@ -189,7 +188,7 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
189188
for(const auto &v : local_variable_table)
190189
{
191190
out << " " << v.index << ": " << v.name << ' '
192-
<< v.descriptor << '\n';
191+
<< v.signature << '\n';
193192
}
194193

195194
out << '\n';
@@ -213,7 +212,7 @@ void java_bytecode_parse_treet::fieldt::output(std::ostream &out) const
213212
out << "static ";
214213

215214
out << name;
216-
out << " : " << descriptor << ';';
215+
out << " : " << signature << ';';
217216

218217
out << '\n';
219218
}

src/java_bytecode/java_bytecode_parse_tree.h

+5-8
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
1212

1313
#include <set>
1414

15-
#include <util/optional.h>
1615
#include <util/std_code.h>
1716
#include <util/std_types.h>
1817

@@ -55,17 +54,16 @@ class java_bytecode_parse_treet
5554
class membert
5655
{
5756
public:
58-
std::string descriptor;
59-
optionalt<std::string> signature;
57+
std::string signature;
6058
irep_idt name;
6159
bool is_public, is_protected, is_private, is_static, is_final;
6260
annotationst annotations;
6361

6462
virtual void output(std::ostream &out) const = 0;
6563

6664
membert():
67-
is_public(false), is_protected(false),
68-
is_private(false), is_static(false), is_final(false)
65+
is_public(false), is_protected(false), is_private(false),
66+
is_static(false), is_final(false)
6967
{
7068
}
7169
};
@@ -102,8 +100,7 @@ class java_bytecode_parse_treet
102100
{
103101
public:
104102
irep_idt name;
105-
std::string descriptor;
106-
optionalt<std::string> signature;
103+
std::string signature;
107104
std::size_t index;
108105
std::size_t start_pc;
109106
std::size_t length;
@@ -177,7 +174,7 @@ class java_bytecode_parse_treet
177174

178175
typedef std::list<irep_idt> implementst;
179176
implementst implements;
180-
optionalt<std::string> signature;
177+
181178
typedef std::list<fieldt> fieldst;
182179
typedef std::list<methodt> methodst;
183180
fieldst fields;

0 commit comments

Comments
 (0)