Skip to content

Commit 47dd1fb

Browse files
committed
Restrict new clinit_wrapper calls to enum types
Calling clinit_wrapper on all nondet-initialized types has a noticeable impact on performance, so for now we are only doing this for enums, and we will re-evaluate the behavior for other types in the future.
1 parent c9e46ae commit 47dd1fb

File tree

2 files changed

+21
-7
lines changed

2 files changed

+21
-7
lines changed

jbmc/src/java_bytecode/ci_lazy_methods.cpp

+10-3
Original file line numberDiff line numberDiff line change
@@ -381,9 +381,16 @@ void ci_lazy_methodst::initialize_instantiated_classes(
381381
{
382382
if(param.type().id()==ID_pointer)
383383
{
384-
const pointer_typet &original_pointer=to_pointer_type(param.type());
385-
add_clinit_call_for_pointer_type(
386-
original_pointer, ns.get_symbol_table(), needed_lazy_methods);
384+
const pointer_typet &original_pointer = to_pointer_type(param.type());
385+
const auto &original_type =
386+
to_java_class_type(ns.follow(original_pointer.subtype()));
387+
// Special case for enums. We may want to generalise this, see TG-4689
388+
// and the comment in java_object_factoryt::gen_nondet_pointer_init.
389+
if(original_type.get_base("java::java.lang.Enum"))
390+
{
391+
add_clinit_call_for_pointer_type(
392+
original_pointer, ns.get_symbol_table(), needed_lazy_methods);
393+
}
387394
needed_lazy_methods.add_all_needed_classes(original_pointer);
388395
}
389396
}

jbmc/src/java_bytecode/java_object_factory.cpp

+11-4
Original file line numberDiff line numberDiff line change
@@ -785,15 +785,22 @@ void java_object_factoryt::gen_nondet_pointer_init(
785785
// (This can currently happen for some cases of #exception_value)
786786
bool must_be_null = subtype == empty_typet();
787787

788-
// If we may be about to initialize a non-null object, always run the
788+
// If we may be about to initialize a non-null enum type, always run the
789789
// clinit_wrapper of its class first.
790+
// TODO: TG-4689 we may want to do this for all types, not just enums, as
791+
// described in the Java language specification:
792+
// https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.7
793+
// https://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4.1
794+
// But we would have to put this behavior behind an option as it would have an
795+
// impact on running times.
790796
// Note that it would be more consistent with the behaviour of the JVM to only
791797
// run clinit_wrapper if we are about to initialize an object of which we know
792798
// for sure that it is not null on any following branch. However, adding this
793-
// case in gen_nondet_struct_init would slow symex down too much.
794-
if(!must_be_null)
799+
// case in gen_nondet_struct_init would slow symex down too much, so if we
800+
// decide to do this for all types, we should do it here.
801+
const java_class_typet &class_type = to_java_class_type(subtype);
802+
if(class_type.get_base("java::java.lang.Enum") && !must_be_null)
795803
{
796-
const java_class_typet &class_type = to_java_class_type(subtype);
797804
const irep_idt &class_name = class_type.get_name();
798805
const irep_idt class_clinit = clinit_wrapper_name(class_name);
799806
gen_method_call_if_present(assignments, expr, class_clinit);

0 commit comments

Comments
 (0)