Skip to content

Revert "TG-374 Feature/java support generics" #1411

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Sep 21, 2017
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 1 addition & 3 deletions regression/cbmc-java/enum1/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
CORE
enum1.class
--java-unwind-enum-static --unwind 3
^VERIFICATION SUCCESSFUL$
Expand All @@ -7,5 +7,3 @@ enum1.class
^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$
--
^warning: ignoring
--
cf. https://diffblue.atlassian.net/browse/TG-611
6 changes: 2 additions & 4 deletions regression/cbmc-java/iterator2/test.desc
Original file line number Diff line number Diff line change
@@ -1,10 +1,8 @@
KNOWNBUG
CORE
iterator2.class
--cover location --unwind 3 --function iterator2.f
--cover location --unwind 3 --function iterator2.f
^EXIT=0$
^SIGNAL=0$
^.*SATISFIED$
--
^warning: ignoring
--
https://diffblue.atlassian.net/browse/TG-610
3 changes: 1 addition & 2 deletions regression/cbmc-java/lvt-groovy/test.desc
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@
KNOWNBUG
CORE
DetectSplitPackagesTask.class
--show-symbol-table
^EXIT=0$
^SIGNAL=0$
--
--
cf. https://diffblue.atlassian.net/browse/TG-610
3 changes: 2 additions & 1 deletion src/java_bytecode/ci_lazy_methods.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ bool ci_lazy_methodst::operator()(
{
const irep_idt methodid="java::"+id2string(classname)+"."+
id2string(method.name)+":"+
id2string(method.descriptor);
id2string(method.signature);
method_worklist2.push_back(methodid);
}
}
Expand Down Expand Up @@ -505,3 +505,4 @@ irep_idt ci_lazy_methodst::get_virtual_method_target(
else
return irep_idt();
}

65 changes: 2 additions & 63 deletions src/java_bytecode/java_bytecode_convert_class.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@ Author: Daniel Kroening, [email protected]
#include "java_bytecode_language.h"
#include "java_utils.h"

#include <util/c_types.h>
#include <util/arith_tools.h>
#include <util/namespace.h>
#include <util/std_expr.h>
Expand Down Expand Up @@ -102,25 +101,6 @@ void java_bytecode_convert_classt::convert(const classt &c)
}

java_class_typet class_type;
if(c.signature.has_value())
{
java_generics_class_typet generic_class_type;
#ifdef DEBUG
std::cout << "INFO: found generic class signature "
<< c.signature.value()
<< " in parsed class "
<< c.name << "\n";
#endif
for(auto t : java_generic_type_from_string(
id2string(c.name),
c.signature.value()))
{
generic_class_type.generic_types()
.push_back(to_java_generic_parameter(t));
}

class_type=generic_class_type;
}

class_type.set_tag(c.name);
class_type.set(ID_base_name, c.name);
Expand Down Expand Up @@ -194,7 +174,7 @@ void java_bytecode_convert_classt::convert(const classt &c)
const irep_idt method_identifier=
id2string(qualified_classname)+
"."+id2string(method.name)+
":"+method.descriptor;
":"+method.signature;
// Always run the lazy pre-stage, as it symbol-table
// registers the function.
debug() << "Adding symbol: method '" << method_identifier << "'" << eom;
Expand All @@ -215,48 +195,7 @@ void java_bytecode_convert_classt::convert(
symbolt &class_symbol,
const fieldt &f)
{
typet field_type;
if(f.signature.has_value())
{
field_type=java_type_from_string(
f.signature.value(),
id2string(class_symbol.name));

/// this is for a free type variable, e.g., a field of the form `T f;`
if(is_java_generic_parameter(field_type))
{
#ifdef DEBUG
std::cout << "fieldtype: generic "
<< to_java_generic_parameter(field_type).type_variable()
.get_identifier()
<< " name " << f.name << "\n";
#endif
}

/// this is for a field that holds a generic type, wither with instantiated
/// or with free type variables, e.g., `List<T> l;` or `List<Integer> l;`
else if(is_java_generic_type(field_type))
{
java_generic_typet &with_gen_type=
to_java_generic_type(field_type);
#ifdef DEBUG
std::cout << "fieldtype: generic container type "
<< std::to_string(with_gen_type.generic_type_variables().size())
<< " type " << with_gen_type.id()
<< " name " << f.name
<< " subtype id " << with_gen_type.subtype().id() << "\n";
#endif
field_type=with_gen_type;
}

/// This case is not possible, a field is either a non-instantiated type
/// variable or a generics container type.
INVARIANT(
!is_java_generic_inst_parameter(field_type),
"Cannot be an instantiated type variable here.");
}
else
field_type=java_type_from_string(f.descriptor);
typet field_type=java_type_from_string(f.signature);

// is this a static field?
if(f.is_static)
Expand Down
29 changes: 4 additions & 25 deletions src/java_bytecode/java_bytecode_convert_method.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -252,7 +252,7 @@ const exprt java_bytecode_convert_methodt::variable(
/// method conversion just yet. The caller should call
/// java_bytecode_convert_method later to give the symbol/method a body.
/// \par parameters: `class_symbol`: class this method belongs to
/// `method_identifier`: fully qualified method name, including type descriptor
/// `method_identifier`: fully qualified method name, including type signature
/// (e.g. "x.y.z.f:(I)")
/// `m`: parsed method object to convert
/// `symbol_table`: global symbol table (will be modified)
Expand All @@ -263,19 +263,7 @@ void java_bytecode_convert_method_lazy(
symbol_tablet &symbol_table)
{
symbolt method_symbol;
typet member_type;
if(m.signature.has_value())
{
#ifdef DEBUG
std::cout << "method " << m.name
<< " has signature " << m.signature.value() << "\n";
#endif
member_type=java_type_from_string(
m.signature.value(),
id2string(class_symbol.name));
}
else
member_type=java_type_from_string(m.descriptor);
typet member_type=java_type_from_string(m.signature);

method_symbol.name=method_identifier;
method_symbol.base_name=m.base_name;
Expand Down Expand Up @@ -329,7 +317,7 @@ void java_bytecode_convert_methodt::convert(
// to retrieve the symbol (constructed by java_bytecode_convert_method_lazy)
// associated to the method
const irep_idt method_identifier=
id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.descriptor;
id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.signature;
method_id=method_identifier;

const auto &old_sym=symbol_table.lookup(method_identifier);
Expand Down Expand Up @@ -362,16 +350,7 @@ void java_bytecode_convert_methodt::convert(
// Construct a fully qualified name for the parameter v,
// e.g. my.package.ClassName.myMethodName:(II)I::anIntParam, and then a
// symbol_exprt with the parameter and its type
typet t;
if(v.signature.has_value())
{
t=java_type_from_string(
v.signature.value(),
id2string(class_symbol.name));
}
else
t=java_type_from_string(v.descriptor);

typet t=java_type_from_string(v.signature);
std::ostringstream id_oss;
id_oss << method_id << "::" << v.name;
irep_idt identifier(id_oss.str());
Expand Down
7 changes: 3 additions & 4 deletions src/java_bytecode/java_bytecode_parse_tree.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@ void java_bytecode_parse_treet::classt::swap(
std::swap(other.is_public, is_public);
std::swap(other.is_protected, is_protected);
std::swap(other.is_private, is_private);
std::swap(other.signature, signature);
other.implements.swap(implements);
other.fields.swap(fields);
other.methods.swap(methods);
Expand Down Expand Up @@ -152,7 +151,7 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
out << "synchronized ";

out << name;
out << " : " << descriptor;
out << " : " << signature;

out << '\n';

Expand Down Expand Up @@ -189,7 +188,7 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
for(const auto &v : local_variable_table)
{
out << " " << v.index << ": " << v.name << ' '
<< v.descriptor << '\n';
<< v.signature << '\n';
}

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

out << name;
out << " : " << descriptor << ';';
out << " : " << signature << ';';

out << '\n';
}
13 changes: 5 additions & 8 deletions src/java_bytecode/java_bytecode_parse_tree.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]

#include <set>

#include <util/optional.h>
#include <util/std_code.h>
#include <util/std_types.h>

Expand Down Expand Up @@ -55,17 +54,16 @@ class java_bytecode_parse_treet
class membert
{
public:
std::string descriptor;
optionalt<std::string> signature;
std::string signature;
irep_idt name;
bool is_public, is_protected, is_private, is_static, is_final;
annotationst annotations;

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

membert():
is_public(false), is_protected(false),
is_private(false), is_static(false), is_final(false)
is_public(false), is_protected(false), is_private(false),
is_static(false), is_final(false)
{
}
};
Expand Down Expand Up @@ -102,8 +100,7 @@ class java_bytecode_parse_treet
{
public:
irep_idt name;
std::string descriptor;
optionalt<std::string> signature;
std::string signature;
std::size_t index;
std::size_t start_pc;
std::size_t length;
Expand Down Expand Up @@ -177,7 +174,7 @@ class java_bytecode_parse_treet

typedef std::list<irep_idt> implementst;
implementst implements;
optionalt<std::string> signature;

typedef std::list<fieldt> fieldst;
typedef std::list<methodt> methodst;
fieldst fields;
Expand Down
Loading