Revert "TG-374 Feature/java support generics"

regression/cbmc-java/enum1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 enum1.class
 --java-unwind-enum-static --unwind 3
 ^VERIFICATION SUCCESSFUL$
@@ -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

regression/cbmc-java/iterator2/test.desc

@@ -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

regression/cbmc-java/lvt-groovy/test.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 DetectSplitPackagesTask.class
 --show-symbol-table
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
-cf. https://diffblue.atlassian.net/browse/TG-610

src/java_bytecode/ci_lazy_methods.cpp

@@ -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);
       }
     }
@@ -505,3 +505,4 @@ irep_idt ci_lazy_methodst::get_virtual_method_target(
   else
     return irep_idt();
 }
+

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -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>
@@ -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);
@@ -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;
@@ -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)

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -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)
@@ -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;
@@ -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);
@@ -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());

src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -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);
@@ -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';
 
@@ -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';
@@ -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';
 }

src/java_bytecode/java_bytecode_parse_tree.h

@@ -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>
 
@@ -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)
     {
     }
   };
@@ -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;
@@ -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;