Skip to content

Commit e6218f8

Browse files
committed
Always run clinit_wrapper before nondet object init
This is more consistent with the behaviour of the JDK (the Java language specification says that static initializers should be run on object initialization), and a necessary requirement to access enum constants.
1 parent 01c47fb commit e6218f8

File tree

1 file changed

+45
-15
lines changed

1 file changed

+45
-15
lines changed

jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 45 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -141,6 +141,11 @@ class java_object_factoryt
141141
allocation_typet alloc_type,
142142
const pointer_typet &substitute_pointer_type,
143143
size_t depth);
144+
145+
void gen_method_call(
146+
code_blockt &assignments,
147+
const exprt &instance_expr,
148+
const irep_idt &method_name);
144149
};
145150

146151
/// Generates code for allocating a dynamic object. This is used in
@@ -756,6 +761,24 @@ void java_object_factoryt::gen_nondet_pointer_init(
756761
}
757762
}
758763

764+
// If this is a void* we *must* initialise with null:
765+
// (This can currently happen for some cases of #exception_value)
766+
bool must_be_null = subtype == empty_typet();
767+
768+
// If we may be about to initialize a non-null object, always run the
769+
// clinit_wrapper of its class first.
770+
// Note that it would be more consistent with the behaviour of the JVM to only
771+
// run clinit_wrapper if we are about to initialize an object of which we know
772+
// for sure that it is not null on any following branch. However, adding this
773+
// case in gen_nondet_struct_init would slow symex down too much.
774+
if(!must_be_null)
775+
{
776+
const java_class_typet &class_type = to_java_class_type(subtype);
777+
const irep_idt &class_name = class_type.get_name();
778+
const irep_idt class_clinit = clinit_wrapper_name(class_name);
779+
gen_method_call(assignments, expr, class_clinit);
780+
}
781+
759782
code_blockt new_object_assignments;
760783
code_blockt update_in_place_assignments;
761784

@@ -800,10 +823,6 @@ void java_object_factoryt::gen_nondet_pointer_init(
800823
const bool allow_null =
801824
depth > object_factory_parameters.max_nonnull_tree_depth;
802825

803-
// Alternatively, if this is a void* we *must* initialise with null:
804-
// (This can currently happen for some cases of #exception_value)
805-
bool must_be_null = subtype == empty_typet();
806-
807826
if(must_be_null)
808827
{
809828
// Add the following code to assignments:
@@ -1066,17 +1085,7 @@ void java_object_factoryt::gen_nondet_struct_init(
10661085

10671086
const irep_idt init_method_name =
10681087
"java::" + id2string(struct_tag) + ".cproverNondetInitialize:()V";
1069-
1070-
if(const auto func = symbol_table.lookup(init_method_name))
1071-
{
1072-
const code_typet &type = to_code_type(func->type);
1073-
code_function_callt fun_call;
1074-
fun_call.function() = func->symbol_expr();
1075-
if(type.has_this())
1076-
fun_call.arguments().push_back(address_of_exprt(expr));
1077-
1078-
assignments.add(fun_call);
1079-
}
1088+
gen_method_call(assignments, expr, init_method_name);
10801089
}
10811090

10821091
/// Initializes a primitive-typed or reference-typed object tree rooted at
@@ -1599,3 +1608,24 @@ void gen_nondet_init(
15991608
pointer_type_selector,
16001609
update_in_place);
16011610
}
1611+
1612+
/// Adds a call for the given method to the end of `assignments`.
1613+
/// \param assignments: A code block that the method call will be appended to.
1614+
/// \param instance_expr: The instance to call the method on. This argument is
1615+
/// ignored if the method is static.
1616+
/// \param method_name: The name of the method to be called.
1617+
void java_object_factoryt::gen_method_call(
1618+
code_blockt &assignments,
1619+
const exprt &instance_expr,
1620+
const irep_idt &method_name)
1621+
{
1622+
if(const auto func = symbol_table.lookup(method_name))
1623+
{
1624+
const code_typet &type = to_code_type(func->type);
1625+
code_function_callt fun_call;
1626+
fun_call.function() = func->symbol_expr();
1627+
if(type.has_this())
1628+
fun_call.arguments().push_back(address_of_exprt(instance_expr));
1629+
assignments.add(fun_call);
1630+
}
1631+
}

0 commit comments

Comments
 (0)