Give up parsing generic method signature with bound

Bounds on generic type variables are not currently parsed. Previously
we were assuming a bound of java.lang.Object. This caused inconsistent
types in goto programs. When we find a bounded type variable in a
function signature we now give up on trying to parse the generic types
and fall back to using the descriptor, which knows about the bounds
and gives us type consistency. The problem still occurs when the bounded
type variable is defined in a class signature.

Author: Owen Jones

jbmc/src/java_bytecode/java_types.cpp

@@ -462,6 +462,18 @@ typet java_type_from_string(
         throw unsupported_java_class_signature_exceptiont(
           "Failed to find generic signature closing delimiter");
       }
+
+      // If there are any bounds between '<' and '>' then we cannot currently
+      // parse them, so we give up. This only happens when parsing the
+      // signature, so we'll fall back to the result of parsing the
+      // descriptor, which will respect the bounds correctly.
+      const size_t colon_pos = src.find(':');
+      if(colon_pos != std::string::npos && colon_pos < closing_generic)
+      {
+        throw unsupported_java_class_signature_exceptiont(
+          "Cannot currently parse bounds on generic types");
+      }
+
       const typet &method_type=java_type_from_string(
         src.substr(closing_generic+1, std::string::npos), class_name_prefix);
 

jbmc/unit/java_bytecode/java_bytecode_parse_generics/BoundedGenericInnerClasses$BoundedInner.class

@@ -8,6 +8,9 @@ class Inner<E>
   class BoundedInner<NUM extends java.lang.Number>
   {
     NUM elem;
+
+    public void f(NUM x) {
+    }
   }
 
   BoundedInner<Integer> belem;

jbmc/unit/java_bytecode/java_bytecode_parse_generics/BoundedGenericInnerClasses$DoubleBoundedInner.class

@@ -17,6 +17,11 @@ public static <T extends Interface_Implementation> void processUpperBoundClass(G
 
   }
 
+  public static <T extends java.lang.Number> void processUpperBoundClass2(T x)
+  {
+
+  }
+
   public static <T extends Interface_Implementation & Interface> void processDoubleUpperBoundClass(Generic<T> x)
   {
 

jbmc/unit/java_bytecode/java_bytecode_parse_generics/BoundedGenericInnerClasses$TwoElementInner.class

@@ -68,6 +68,24 @@ SCENARIO(
             to_struct_type(class_symbol.type), "elem");
         require_type::require_java_generic_parameter(
           elem.type(), boundedinner_name + "::NUM");
+
+        std::string method_name =
+          boundedinner_name + ".f:(Ljava/lang/Number;)V";
+        REQUIRE(new_symbol_table.has_symbol(method_name));
+        THEN("The method parameter type should respect its bound")
+        {
+          const symbolt &method_symbol =
+            new_symbol_table.lookup_ref(method_name);
+          const code_typet &method_type =
+            require_type::require_code(method_symbol.type);
+          const code_typet::parametert &param =
+            require_type::require_parameter(method_type, "x");
+          require_type::require_java_generic_parameter(
+            param.type(), boundedinner_name + "::NUM");
+
+          // TODO: the bounds are not parsed yet; extend tests when fixed -
+          // issue TG-1286
+        }
       }
     }
   }