Skip to content
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

Java generic bounded types in method signatures #2232

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
12 changes: 12 additions & 0 deletions jbmc/src/java_bytecode/java_types.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand Down
Binary file not shown.
Binary file not shown.
Binary file not shown.
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,9 @@ class Inner<E>
class BoundedInner<NUM extends java.lang.Number>
{
NUM elem;

public void f(NUM x) {
}
}

BoundedInner<Integer> belem;
Expand Down
Binary file not shown.
Original file line number Diff line number Diff line change
Expand Up @@ -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)
{

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
}
}
}
Expand Down
Loading