From 7e3dbc6ff528cebe6db64bbc495a984785fd4a4a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 3 Nov 2026 16:36:08 +0000 Subject: [PATCH 1/5] JBMC: initialise class literals after all other static symbols java_static_lifetime_init initialises static symbols in alphabetical order. For a class literal (Foo@class_model) it emits a call to java.lang.Class.cproverInitializeClassLiteral of the models library. That method may access static fields, which runs static initializers. Static fields, and the flags that record whether a static initializer has run, are zero-initialised in the same alphabetical pass. Thus, for example, java::Test$A@class_model was initialised before java::java.lang.Class's static fields and its clinit_already_run flag: the effects of the class literal's initialisation on static state were undone, and the static initializer of java.lang.Class ran again later. Initialise class literals only once all other static symbols (and any symbols that their initialisation creates) have been initialised. With the current models library nothing changes: its cproverInitializeClassLiteral does not access static fields, and all JBMC regression tests pass. A model of Class.forName that keeps the unique Class object of each class in a static data structure, including the class literals, requires this change. The new regression test uses its own model of java.lang.Class, whose cproverInitializeClassLiteral counts the initialised class literals in a static field of another class. Without this change, that count is 0 when the entry point runs. Co-authored-by: Kiro --- .../jbmc/class-literals-static-state/pom.xml | 37 +++++++++++++++++++ .../src/main/java/Test.java | 13 +++++++ .../src/main/java/java/lang/Class.java | 25 +++++++++++++ .../regression/ClassLiteralCounter.java | 6 +++ .../class-literals-static-state/test.desc | 14 +++++++ jbmc/regression/jbmc/pom.xml | 1 + jbmc/src/java_bytecode/java_entry_point.cpp | 24 +++++++++++- 7 files changed, 119 insertions(+), 1 deletion(-) create mode 100644 jbmc/regression/jbmc/class-literals-static-state/pom.xml create mode 100644 jbmc/regression/jbmc/class-literals-static-state/src/main/java/Test.java create mode 100644 jbmc/regression/jbmc/class-literals-static-state/src/main/java/java/lang/Class.java create mode 100644 jbmc/regression/jbmc/class-literals-static-state/src/main/java/org/cprover/regression/ClassLiteralCounter.java create mode 100644 jbmc/regression/jbmc/class-literals-static-state/test.desc diff --git a/jbmc/regression/jbmc/class-literals-static-state/pom.xml b/jbmc/regression/jbmc/class-literals-static-state/pom.xml new file mode 100644 index 000000000000..2986c14740c7 --- /dev/null +++ b/jbmc/regression/jbmc/class-literals-static-state/pom.xml @@ -0,0 +1,37 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.class-literals-static-state + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/class-literals-static-state/src/main/java/Test.java b/jbmc/regression/jbmc/class-literals-static-state/src/main/java/Test.java new file mode 100644 index 000000000000..d62037dca9b2 --- /dev/null +++ b/jbmc/regression/jbmc/class-literals-static-state/src/main/java/Test.java @@ -0,0 +1,13 @@ +public class Test { + static class A {} + + static class B {} + + public static void main() { + Class a = A.class; + Class b = B.class; + assert a != b; + // at least the class literals of A and B have been initialised + assert org.cprover.regression.ClassLiteralCounter.count[0] >= 2; + } +} diff --git a/jbmc/regression/jbmc/class-literals-static-state/src/main/java/java/lang/Class.java b/jbmc/regression/jbmc/class-literals-static-state/src/main/java/java/lang/Class.java new file mode 100644 index 000000000000..b5d5120a81eb --- /dev/null +++ b/jbmc/regression/jbmc/class-literals-static-state/src/main/java/java/lang/Class.java @@ -0,0 +1,25 @@ +package java.lang; + +public class Class { + + private String name; + + @org.cprover.MustNotThrow + public void cproverInitializeClassLiteral( + String name, + boolean isAnnotation, + boolean isArray, + boolean isInterface, + boolean isSynthetic, + boolean isLocalClass, + boolean isMemberClass, + boolean isEnum) { + this.name = name; + // a static field of another class, which must not be reset afterwards + org.cprover.regression.ClassLiteralCounter.count[0]++; + } + + public String getName() { return name; } + + public boolean desiredAssertionStatus() { return true; } +} diff --git a/jbmc/regression/jbmc/class-literals-static-state/src/main/java/org/cprover/regression/ClassLiteralCounter.java b/jbmc/regression/jbmc/class-literals-static-state/src/main/java/org/cprover/regression/ClassLiteralCounter.java new file mode 100644 index 000000000000..d81f2af34fc8 --- /dev/null +++ b/jbmc/regression/jbmc/class-literals-static-state/src/main/java/org/cprover/regression/ClassLiteralCounter.java @@ -0,0 +1,6 @@ +package org.cprover.regression; + +public class ClassLiteralCounter { + // Number of class literals that have been initialised + public static final int[] count = new int[1]; +} diff --git a/jbmc/regression/jbmc/class-literals-static-state/test.desc b/jbmc/regression/jbmc/class-literals-static-state/test.desc new file mode 100644 index 000000000000..3cc69197acbb --- /dev/null +++ b/jbmc/regression/jbmc/class-literals-static-state/test.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.main -cp target/classes +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +JBMC initialises class literals by calling cproverInitializeClassLiteral of the +model of java.lang.Class. Its effects on static fields must persist: class +literals must thus only be initialised once all other static symbols +(including the static fields of java.lang.Class and the flag recording whether +its static initializer has run) have been initialised. diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 0dff8aa4ddb2..55d0fa07d73f 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -69,6 +69,7 @@ char1 class-fields class-literals + class-literals-static-state class-loading-annotations class_hierarchy Class_method1 diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index fa074554c8e5..8ac95439cca4 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -265,17 +265,39 @@ void java_static_lifetime_init( for(const auto &entry : symbol_table.symbols) symbol_names.insert(id2string(entry.first)); + // Class literals are initialised by calling a method of the model of + // java.lang.Class, which may access static fields and thus run static + // initializers. Initialise class literals only once all other static symbols + // have been initialised: otherwise, zero-initialising a static field, or the + // flag that records whether a static initializer has run, may undo the + // effects of that method. + std::set class_literals; + bool class_literal_phase = false; std::set additional_symbols; - while(!symbol_names.empty() || !additional_symbols.empty()) + while(true) { if(!additional_symbols.empty()) symbol_names.swap(additional_symbols); + else if(symbol_names.empty()) + { + if(class_literal_phase || class_literals.empty()) + break; + class_literal_phase = true; + symbol_names.swap(class_literals); + } for(const auto &symbol_name : symbol_names) { const symbolt &sym = symbol_table.lookup_ref(symbol_name); if(should_init_symbol(sym)) { + if( + !class_literal_phase && + get_class_literal_initializer(sym, symbol_table) != nullptr) + { + class_literals.insert(symbol_name); + continue; + } auto new_symbols = init_symbol( sym, code_block, From 9ec6be2be70800d91a013fc9bed84a6faf21211b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 3 Nov 2026 20:29:18 +0000 Subject: [PATCH 2/5] JBMC: make Object.getClass return the unique Class object of each class In the JVM, each class has exactly one java.lang.Class object, so that a.getClass() == b.getClass() holds if and only if a and b have the same runtime type, and a.getClass() == A.class if and only if a has type A. Code relies on this, e.g., in equals methods and in Enum.compareTo. JBMC used the Object.getClass model of the models library, which calls Class.forName with the name of the runtime type. Implementing Class objects that are unique per name in the models library requires a lookup by name, which compares strings using the string solver: with a list of all Class objects, a program that calls getClass on objects of 10 different classes took 81 seconds, and with 20 classes did not finish within 7 minutes. An if-then-else chain over all classes in JBMC itself scales linearly, but makes every program that calls getClass initialise the class literals of all of the about 130 classes that are loaded. Instead, add a synthetic method C.getClass, which overrides Object.getClass and returns the class literal of C, for each class C that can have instances. Virtual method dispatch then selects the override of the runtime type, which symbolic execution resolves without involving the string solver. This is compatible with both kinds of lazy loading, as only the method symbols are created up front: context-insensitive lazy loading only converts the overrides of classes that it finds to be instantiated, and symex-driven lazy loading converts the ones that symbolic execution reaches. Class literals must exist before __CPROVER_initialize is generated, so create one for each class up front. If the program does not refer to a class literal, it is not initialised in __CPROVER_initialize, but on the first call of the class's getClass override, using CProver.classIdentifier for the name (as no new String literals can be created at that point). Initialising the class literals of all classes in __CPROVER_initialize would increase the size of the program expression for a trivial program from 37348 to 53079 steps with symex-driven lazy loading, which does not remove unused globals; with this change, it is 37540 steps. For the benchmark described above, verification now takes 0.33 seconds with 10 classes and 1.3 seconds with 40 classes. All JBMC regression tests pass; the sum of per-test times was 1003 and 1027 seconds in two runs, compared with 1003 seconds without this change. Co-authored-by: Kiro --- .../jbmc/get-class/classLiteral.desc | 11 + .../jbmc/get-class/differentClass.desc | 11 + jbmc/regression/jbmc/get-class/mustFail.desc | 11 + .../jbmc/get-class/noClassLiteral.desc | 11 + jbmc/regression/jbmc/get-class/pom.xml | 37 +++ jbmc/regression/jbmc/get-class/sameClass.desc | 11 + .../jbmc/get-class/src/main/java/Test.java | 60 +++++ jbmc/regression/jbmc/pom.xml | 1 + .../java_bytecode/java_bytecode_language.cpp | 243 ++++++++++++++++++ .../src/java_bytecode/synthetic_methods_map.h | 6 +- 10 files changed, 401 insertions(+), 1 deletion(-) create mode 100644 jbmc/regression/jbmc/get-class/classLiteral.desc create mode 100644 jbmc/regression/jbmc/get-class/differentClass.desc create mode 100644 jbmc/regression/jbmc/get-class/mustFail.desc create mode 100644 jbmc/regression/jbmc/get-class/noClassLiteral.desc create mode 100644 jbmc/regression/jbmc/get-class/pom.xml create mode 100644 jbmc/regression/jbmc/get-class/sameClass.desc create mode 100644 jbmc/regression/jbmc/get-class/src/main/java/Test.java diff --git a/jbmc/regression/jbmc/get-class/classLiteral.desc b/jbmc/regression/jbmc/get-class/classLiteral.desc new file mode 100644 index 000000000000..a2e67e7d5cb9 --- /dev/null +++ b/jbmc/regression/jbmc/get-class/classLiteral.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.classLiteral -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the unique java.lang.Class object of the runtime +type of the receiver, which is also the class literal of that type. diff --git a/jbmc/regression/jbmc/get-class/differentClass.desc b/jbmc/regression/jbmc/get-class/differentClass.desc new file mode 100644 index 000000000000..28826e0bf159 --- /dev/null +++ b/jbmc/regression/jbmc/get-class/differentClass.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.differentClass -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the unique java.lang.Class object of the runtime +type of the receiver, which is also the class literal of that type. diff --git a/jbmc/regression/jbmc/get-class/mustFail.desc b/jbmc/regression/jbmc/get-class/mustFail.desc new file mode 100644 index 000000000000..0b8e1d907e7a --- /dev/null +++ b/jbmc/regression/jbmc/get-class/mustFail.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.mustFail -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 58 .*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +Objects of different runtime types have different Class objects. diff --git a/jbmc/regression/jbmc/get-class/noClassLiteral.desc b/jbmc/regression/jbmc/get-class/noClassLiteral.desc new file mode 100644 index 000000000000..ee1426260e14 --- /dev/null +++ b/jbmc/regression/jbmc/get-class/noClassLiteral.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.noClassLiteral -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the unique java.lang.Class object of the runtime +type of the receiver, which is also the class literal of that type. diff --git a/jbmc/regression/jbmc/get-class/pom.xml b/jbmc/regression/jbmc/get-class/pom.xml new file mode 100644 index 000000000000..ebf9a029ee4d --- /dev/null +++ b/jbmc/regression/jbmc/get-class/pom.xml @@ -0,0 +1,37 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.get-class + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/get-class/sameClass.desc b/jbmc/regression/jbmc/get-class/sameClass.desc new file mode 100644 index 000000000000..be50905e6ef0 --- /dev/null +++ b/jbmc/regression/jbmc/get-class/sameClass.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.sameClass -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the unique java.lang.Class object of the runtime +type of the receiver, which is also the class literal of that type. diff --git a/jbmc/regression/jbmc/get-class/src/main/java/Test.java b/jbmc/regression/jbmc/get-class/src/main/java/Test.java new file mode 100644 index 000000000000..d844f80d7eab --- /dev/null +++ b/jbmc/regression/jbmc/get-class/src/main/java/Test.java @@ -0,0 +1,60 @@ +public class Test { + static class A { + int x; + + A(int x) { + this.x = x; + } + + @Override + public boolean equals(Object o) { + // a common idiom, which requires Class objects to be unique + if(o == null || getClass() != o.getClass()) + return false; + return x == ((A)o).x; + } + } + + static class B extends A { + B(int x) { + super(x); + } + } + + // no class literal of C appears in this program + static class C { + } + + public static void sameClass(int i) { + A a1 = new A(i); + A a2 = new A(i); + assert a1.getClass() == a2.getClass(); + assert a1.equals(a2); + } + + public static void classLiteral() { + A a = new A(1); + assert a.getClass() == A.class; + assert a.getClass() != B.class; + } + + public static void differentClass(int i) { + A a = new A(i); + B b = new B(i); + assert a.getClass() != b.getClass(); + assert !a.equals(b); + } + + public static void noClassLiteral() { + Object c1 = new C(); + Object c2 = new C(); + assert c1.getClass() == c2.getClass(); + assert c1.getClass().getName().equals("Test$C"); + } + + public static void mustFail(int i) { + A a = new A(i); + B b = new B(i); + assert a.getClass() == b.getClass(); + } +} diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 55d0fa07d73f..c86b414d0f38 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -164,6 +164,7 @@ function3 function4 generic_base_type + get-class generic_class_bound1 generic_function_parameter generic_static_field diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index b982ff625b00..1fbd9ee08e6f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -18,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -791,6 +793,241 @@ static void create_stub_global_symbols( } } +/// Name of the global flag that records whether the class literal of +/// \p class_id, which \ref create_get_class_methods created, has been +/// initialised. +static irep_idt lazy_class_literal_initialized_name(const irep_idt &class_id) +{ + return id2string(class_id) + "@class_model_initialized"; +} + +static const irep_idt &object_get_class_name() +{ + static const irep_idt name = + "java::java.lang.Object.getClass:()Ljava/lang/Class;"; + return name; +} + +/// For each class that can have instances, add a method `getClass` that +/// overrides java.lang.Object.getClass and returns the class's class literal +/// (see \ref get_class_method_body). Only the symbols are created here, the +/// bodies are generated when the methods are converted, so that this is +/// compatible with lazy loading: context-insensitive lazy loading only converts +/// the overrides of classes that are instantiated, and symex-driven lazy +/// loading converts those of the runtime types that symbolic execution +/// encounters. The class literals are created up front, as all of them must +/// exist before __CPROVER_initialize is generated. +/// \param symbol_table: global symbol table +/// \param synthetic_methods: synthetic method map, to which the methods are +/// added +static void create_get_class_methods( + symbol_table_baset &symbol_table, + synthetic_methods_mapt &synthetic_methods) +{ + const symbolt *object_get_class = + symbol_table.lookup(object_get_class_name()); + if(object_get_class == nullptr || object_get_class->value.is_not_nil()) + return; + + // Careful not to add to the symbol table while iterating over it + std::vector class_ids; + for(const auto &entry : symbol_table) + { + const symbolt &symbol = entry.second; + if( + !symbol.is_type || symbol.mode != ID_java || + !can_cast_type(symbol.type) || + symbol.name == "java::java.lang.Object" || is_java_array_tag(symbol.name)) + { + continue; + } + const java_class_typet &class_type = to_java_class_type(symbol.type); + if(class_type.get_interface() || class_type.get_abstract()) + continue; + class_ids.push_back(symbol.name); + } + + const java_method_typet &object_get_class_type = + to_java_method_type(object_get_class->type); + for(const irep_idt &class_id : class_ids) + { + const irep_idt method_id = + id2string(class_id) + ".getClass:()Ljava/lang/Class;"; + if(symbol_table.has_symbol(method_id)) + continue; + + // If the program does not refer to the class literal, create one that is + // only initialised once getClass is first called for this class (see + // get_class_method_body): initialising the class literals of all classes + // in __CPROVER_initialize would be expensive with symex-driven lazy + // loading, which does not remove unused globals. + const irep_idt literal_id = id2string(class_id) + JAVA_CLASS_MODEL_SUFFIX; + if(!symbol_table.has_symbol(literal_id)) + { + get_or_create_class_literal_symbol(class_id, symbol_table); + symbol_table.get_writeable_ref(literal_id) + .type.set(ID_C_no_initialization_required, true); + + symbolt initialized_symbol{ + lazy_class_literal_initialized_name(class_id), + java_boolean_type(), + ID_java}; + initialized_symbol.base_name = + id2string(initialized_symbol.name).substr(6); + initialized_symbol.is_lvalue = true; + initialized_symbol.is_state_var = true; + initialized_symbol.is_static_lifetime = true; + initialized_symbol.value = from_integer(0, java_boolean_type()); + symbol_table.add(initialized_symbol); + } + + java_method_typet method_type = object_get_class_type; + method_type.set_is_final(true); + auto &this_param = method_type.parameters().front(); + this_param.type() = java_reference_type(struct_tag_typet{class_id}); + this_param.set_base_name("this"); + this_param.set_identifier(id2string(method_id) + "::this"); + + symbolt method_symbol{method_id, method_type, ID_java}; + method_symbol.base_name = "getClass"; + method_symbol.pretty_name = id2string(class_id).substr(6) + ".getClass()"; + set_declaring_class(method_symbol, class_id); + symbol_table.add(method_symbol); + synthetic_methods[method_id] = synthetic_method_typet::GET_CLASS; + } +} + +/// Body of an override of java.lang.Object.getClass created by +/// \ref create_get_class_methods for class C: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// return &C@class_model; +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// If the program does not refer to the class literal, so that +/// __CPROVER_initialize does not initialise it, the class literal is +/// initialised on the first call instead, in the same way as +/// java_static_lifetime_init does, except that the name is obtained via +/// CProver.classIdentifier, as no new String literals can be created at this +/// point: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// if(!C@class_model_initialized) +/// { +/// C@class_model_initialized = true; +/// C@class_model = { zero-initialised object of type java.lang.Class }; +/// C@class_model.cproverInitializeClassLiteral( +/// CProver.classIdentifier(this), ...); +/// } +/// return &C@class_model; +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// \param function_id: name of the method +/// \param symbol_table: global symbol table +/// \param message_handler: message handler +/// \return code of the method +static codet get_class_method_body( + const irep_idt &function_id, + symbol_table_baset &symbol_table, + message_handlert &message_handler) +{ + const symbolt &symbol = symbol_table.lookup_ref(function_id); + const java_method_typet &method_type = to_java_method_type(symbol.type); + for(const auto ¶meter : method_type.parameters()) + { + parameter_symbolt parameter_symbol; + parameter_symbol.name = parameter.get_identifier(); + parameter_symbol.base_name = parameter.get_base_name(); + parameter_symbol.mode = ID_java; + parameter_symbol.type = parameter.type(); + symbol_table.add(parameter_symbol); + } + + const auto class_id = declaring_class(symbol); + INVARIANT(class_id.has_value(), "getClass override must have a class"); + const symbol_exprt class_literal = + symbol_table.lookup_ref(id2string(*class_id) + JAVA_CLASS_MODEL_SUFFIX) + .symbol_expr(); + const source_locationt &loc = symbol.location; + + code_blockt code; + + const symbolt *initialized = + symbol_table.lookup(lazy_class_literal_initialized_name(*class_id)); + const symbolt *initializer = + symbol_table.lookup(get_java_class_literal_initializer_signature()); + if(initialized != nullptr && initializer != nullptr) + { + code_blockt init; + init.add(code_frontend_assignt{ + initialized->symbol_expr(), from_integer(1, java_boolean_type())}); + + const namespacet ns{symbol_table}; + auto zero_object = zero_initializer(class_literal.type(), loc, ns); + if(!zero_object.has_value()) + { + messaget log{message_handler}; + log.error() << "failed to zero-initialize " << class_literal.identifier() + << messaget::eom; + throw 0; + } + set_class_identifier( + to_struct_expr(*zero_object), + ns, + to_struct_tag_type(class_literal.type())); + init.add(code_frontend_assignt{class_literal, *zero_object}); + + const java_method_typet &initializer_type = + to_java_method_type(initializer->type); + const typet &string_type = initializer_type.parameters()[1].type(); + exprt name = null_pointer_exprt{to_pointer_type(string_type)}; + const symbolt *class_identifier = symbol_table.lookup( + "java::org.cprover.CProver.classIdentifier:" + "(Ljava/lang/Object;)Ljava/lang/String;"); + if(class_identifier != nullptr) + { + const symbolt &name_symbol = fresh_java_symbol( + string_type, "class_name", loc, function_id, symbol_table); + init.add(code_frontend_declt{name_symbol.symbol_expr()}); + const java_method_typet &class_identifier_type = + to_java_method_type(class_identifier->type); + init.add(code_function_callt{ + name_symbol.symbol_expr(), + class_identifier->symbol_expr(), + {typecast_exprt::conditional_cast( + symbol_exprt{ + method_type.parameters()[0].get_identifier(), + method_type.parameters()[0].type()}, + class_identifier_type.parameters()[0].type())}}); + name = name_symbol.symbol_expr(); + } + + const java_class_typet &class_type = + to_java_class_type(symbol_table.lookup_ref(*class_id).type); + auto constant_bool = [](bool b) + { return from_integer(b ? 1 : 0, java_boolean_type()); }; + const side_effect_expr_nondett nondet_bool{java_boolean_type(), loc}; + // Argument order is: name, isAnnotation, isArray, isInterface, + // isSynthetic, isLocalClass, isMemberClass, isEnum + init.add(code_function_callt{ + initializer->symbol_expr(), + {address_of_exprt{class_literal}, + name, + constant_bool(class_type.get_is_annotation()), + constant_bool(false), + constant_bool(class_type.get_interface()), + constant_bool(class_type.get_synthetic()), + nondet_bool, + nondet_bool, + constant_bool(class_type.get_is_enumeration())}}); + + code.add(code_ifthenelset{ + equal_exprt{ + initialized->symbol_expr(), from_integer(0, java_boolean_type())}, + init}); + } + + code.add(code_frontend_returnt{typecast_exprt::conditional_cast( + address_of_exprt{class_literal}, method_type.return_type())}); + return std::move(code); +} + bool java_bytecode_languaget::typecheck( symbol_table_baset &symbol_table, const std::string &, @@ -936,6 +1173,8 @@ bool java_bytecode_languaget::typecheck( } } + create_get_class_methods(symbol_table, synthetic_methods); + messaget log(message_handler); log.status() << "Java: added " << (symbol_table.symbols.size() - before_constant_globals_size) @@ -1437,6 +1676,10 @@ bool java_bytecode_languaget::convert_single_method_code( writable_symbol.value = invokedynamic_synthetic_method( function_id, symbol_table, message_handler); break; + case synthetic_method_typet::GET_CLASS: + writable_symbol.value = + get_class_method_body(function_id, symbol_table, message_handler); + break; case synthetic_method_typet::CREATE_ARRAY_WITH_TYPE: { INVARIANT( diff --git a/jbmc/src/java_bytecode/synthetic_methods_map.h b/jbmc/src/java_bytecode/synthetic_methods_map.h index bfe203cfadee..27d430f190b5 100644 --- a/jbmc/src/java_bytecode/synthetic_methods_map.h +++ b/jbmc/src/java_bytecode/synthetic_methods_map.h @@ -49,7 +49,11 @@ enum class synthetic_method_typet INVOKEDYNAMIC_METHOD, /// Our internal implementation of CProver.createArrayWithType, which needs to /// access internal type-id fields - CREATE_ARRAY_WITH_TYPE + CREATE_ARRAY_WITH_TYPE, + /// An override of java.lang.Object.getClass in a class C, which returns the + /// class literal of C. Virtual method dispatch then makes getClass return + /// the unique java.lang.Class object of the runtime type of the receiver. + GET_CLASS }; /// Maps method names on to a synthetic method kind. From 879f7c5c46aa841f3c9628d3a9783920b3bead9d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 4 Nov 2026 16:48:12 +0000 Subject: [PATCH 3/5] JBMC: let the models provide Class objects for getClass If the program does not refer to the class literal of a class C, the override of getClass for C initialises C's class literal on its first call. A model of Class.forName that returns unique Class objects cannot find that class literal before then, so a call of Class.forName("C") before the first call of getClass for C creates a second Class object for C: Class.forName("C") == new C().getClass() did not hold. Instead, obtain the Class object of such a class from the method cproverGetClassObject of the model of java.lang.Class, if it exists, on the first call of getClass for C, and store it in a global. The model can then return the Class object that forName created for C, if any. cproverGetClassObject takes the same arguments as cproverInitializeClassLiteral, so that the model can record whether C is an enum etc. With models that do not have cproverGetClassObject, the class literal is initialised as before. If the model of java.lang.Class has neither cproverGetClassObject nor cproverInitializeClassLiteral, the class literal is now initialised by __CPROVER_initialize as before this series, rather than not at all. The new regression test get-class-for-name uses its own model of java.lang.Class with such a cproverGetClassObject method. It also covers programs that first call getClass for a class on only one branch: the model must not add an object that might already be in one of its lists, as symbolic execution would then consider cyclic lists and could not bound the loops over them. Co-authored-by: Kiro --- .../jbmc/get-class-for-name/classLiteral.desc | 14 + .../jbmc/get-class-for-name/enumFlag.desc | 14 + .../get-class-for-name/firstCallOnBranch.desc | 14 + .../forNameThenGetClass.desc | 14 + .../getClassThenForName.desc | 14 + .../jbmc/get-class-for-name/mustFail.desc | 11 + .../get-class-for-name/objectReceiver.desc | 12 + .../jbmc/get-class-for-name/pom.xml | 37 +++ .../src/main/java/Test.java | 56 ++++ .../src/main/java/java/lang/Class.java | 74 +++++ .../jbmc/get-class-for-name/twoClasses.desc | 14 + jbmc/regression/jbmc/pom.xml | 1 + .../java_bytecode/java_bytecode_language.cpp | 271 +++++++++++------- 13 files changed, 449 insertions(+), 97 deletions(-) create mode 100644 jbmc/regression/jbmc/get-class-for-name/classLiteral.desc create mode 100644 jbmc/regression/jbmc/get-class-for-name/enumFlag.desc create mode 100644 jbmc/regression/jbmc/get-class-for-name/firstCallOnBranch.desc create mode 100644 jbmc/regression/jbmc/get-class-for-name/forNameThenGetClass.desc create mode 100644 jbmc/regression/jbmc/get-class-for-name/getClassThenForName.desc create mode 100644 jbmc/regression/jbmc/get-class-for-name/mustFail.desc create mode 100644 jbmc/regression/jbmc/get-class-for-name/objectReceiver.desc create mode 100644 jbmc/regression/jbmc/get-class-for-name/pom.xml create mode 100644 jbmc/regression/jbmc/get-class-for-name/src/main/java/Test.java create mode 100644 jbmc/regression/jbmc/get-class-for-name/src/main/java/java/lang/Class.java create mode 100644 jbmc/regression/jbmc/get-class-for-name/twoClasses.desc diff --git a/jbmc/regression/jbmc/get-class-for-name/classLiteral.desc b/jbmc/regression/jbmc/get-class-for-name/classLiteral.desc new file mode 100644 index 000000000000..02c3223b3990 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/classLiteral.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.classLiteral -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the same java.lang.Class object as +Class.forName, also for classes whose class literal the program does not +refer to, irrespective of which of the two is called first. JBMC obtains the +Class object of such a class from cproverGetClassObject of the model of +java.lang.Class on the first call of getClass for that class. diff --git a/jbmc/regression/jbmc/get-class-for-name/enumFlag.desc b/jbmc/regression/jbmc/get-class-for-name/enumFlag.desc new file mode 100644 index 000000000000..f27df42beda2 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/enumFlag.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.enumFlag -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the same java.lang.Class object as +Class.forName, also for classes whose class literal the program does not +refer to, irrespective of which of the two is called first. JBMC obtains the +Class object of such a class from cproverGetClassObject of the model of +java.lang.Class on the first call of getClass for that class. diff --git a/jbmc/regression/jbmc/get-class-for-name/firstCallOnBranch.desc b/jbmc/regression/jbmc/get-class-for-name/firstCallOnBranch.desc new file mode 100644 index 000000000000..3c3acc296ff6 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/firstCallOnBranch.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.firstCallOnBranch -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the same java.lang.Class object as +Class.forName, also for classes whose class literal the program does not +refer to, irrespective of which of the two is called first. JBMC obtains the +Class object of such a class from cproverGetClassObject of the model of +java.lang.Class on the first call of getClass for that class. diff --git a/jbmc/regression/jbmc/get-class-for-name/forNameThenGetClass.desc b/jbmc/regression/jbmc/get-class-for-name/forNameThenGetClass.desc new file mode 100644 index 000000000000..03e7c8bd3765 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/forNameThenGetClass.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.forNameThenGetClass -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the same java.lang.Class object as +Class.forName, also for classes whose class literal the program does not +refer to, irrespective of which of the two is called first. JBMC obtains the +Class object of such a class from cproverGetClassObject of the model of +java.lang.Class on the first call of getClass for that class. diff --git a/jbmc/regression/jbmc/get-class-for-name/getClassThenForName.desc b/jbmc/regression/jbmc/get-class-for-name/getClassThenForName.desc new file mode 100644 index 000000000000..83df332a74b7 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/getClassThenForName.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.getClassThenForName -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the same java.lang.Class object as +Class.forName, also for classes whose class literal the program does not +refer to, irrespective of which of the two is called first. JBMC obtains the +Class object of such a class from cproverGetClassObject of the model of +java.lang.Class on the first call of getClass for that class. diff --git a/jbmc/regression/jbmc/get-class-for-name/mustFail.desc b/jbmc/regression/jbmc/get-class-for-name/mustFail.desc new file mode 100644 index 000000000000..bfe980189104 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/mustFail.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.mustFail -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=10$ +^SIGNAL=0$ +^\[java::Test\.mustFail:\(\)V\.assertion\.1\] line 54 .*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +The Class objects of different classes must be distinct. diff --git a/jbmc/regression/jbmc/get-class-for-name/objectReceiver.desc b/jbmc/regression/jbmc/get-class-for-name/objectReceiver.desc new file mode 100644 index 000000000000..a17c99453cc9 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/objectReceiver.desc @@ -0,0 +1,12 @@ +CORE +Test +--function Test.objectReceiver -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Objects whose runtime type is java.lang.Object use the model of +Object.getClass, which calls Class.forName; their Class object must be the +class literal of java.lang.Object, and differ from those of other classes. diff --git a/jbmc/regression/jbmc/get-class-for-name/pom.xml b/jbmc/regression/jbmc/get-class-for-name/pom.xml new file mode 100644 index 000000000000..438b42ada37f --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/pom.xml @@ -0,0 +1,37 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.get-class-for-name + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + org.cprover.util + cprover-api + + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + diff --git a/jbmc/regression/jbmc/get-class-for-name/src/main/java/Test.java b/jbmc/regression/jbmc/get-class-for-name/src/main/java/Test.java new file mode 100644 index 000000000000..ac807b139cad --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/src/main/java/Test.java @@ -0,0 +1,56 @@ +public class Test { + static class A {} + static class B {} + static class C {} + enum E { X } + + public static void forNameThenGetClass() { + Class c = Class.forName("Test$A"); + assert new A().getClass() == c; + assert Class.forName("Test$A") == c; + } + + public static void getClassThenForName() { + Class c = new A().getClass(); + assert Class.forName("Test$A") == c; + } + + public static void classLiteral() { + assert Class.forName("Test$C") == C.class; + assert new C().getClass() == C.class; + } + + public static void twoClasses() { + Class a = Class.forName("Test$A"); + Class b = Class.forName("Test$B"); + assert new B().getClass() == b; + assert new A().getClass() == a; + assert a != b; + } + + public static void firstCallOnBranch(boolean nondet) { + if (nondet) + new A().getClass(); + Class c = new A().getClass(); + assert Class.forName("Test$A") == c; + } + + public static void enumFlag() { + Class c = Class.forName("Test$E"); + assert E.X.getClass() == c; + assert c.isEnum(); + } + + public static void objectReceiver() { + Object o = new Object(); + assert o.getClass() == Object.class; + assert new Object().getClass() == o.getClass(); + Object a = new A(); + assert a.getClass() != o.getClass(); + } + + public static void mustFail() { + Class c = Class.forName("Test$A"); + assert new B().getClass() == c; + } +} diff --git a/jbmc/regression/jbmc/get-class-for-name/src/main/java/java/lang/Class.java b/jbmc/regression/jbmc/get-class-for-name/src/main/java/java/lang/Class.java new file mode 100644 index 000000000000..7bc5a9cf95c8 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/src/main/java/java/lang/Class.java @@ -0,0 +1,74 @@ +package java.lang; + +// A minimal model of java.lang.Class with unique Class objects per name, which +// provides cproverGetClassObject for JBMC's implementation of getClass. +public class Class { + private String name; + private boolean cproverIsEnum; + private Class cproverNextClass; + + // Class literals that JBMC initialises in __CPROVER_initialize + private static final Class[] literals = new Class[1]; + // Class objects created by forName or cproverGetClassObject + private static final Class[] others = new Class[1]; + + public String getName() { return name; } + public boolean isEnum() { return cproverIsEnum; } + public boolean desiredAssertionStatus() { return true; } + + private static Class findOther(String name) { + for (Class c = others[0]; c != null; c = c.cproverNextClass) + if (name.equals(c.name)) + return c; + return null; + } + + private static Class newOther(String name) { + Class c = new Class<>(); + c.name = name; + c.cproverNextClass = others[0]; + others[0] = c; + return c; + } + + public static Class forName(String name) { + for (Class c = literals[0]; c != null; c = c.cproverNextClass) + if (name.equals(c.name)) + return c; + Class c = findOther(name); + return c != null ? c : newOther(name); + } + + @org.cprover.MustNotThrow + public void cproverInitializeClassLiteral( + String name, + boolean isAnnotation, + boolean isArray, + boolean isInterface, + boolean isSynthetic, + boolean isLocalClass, + boolean isMemberClass, + boolean isEnum) { + this.name = name; + this.cproverIsEnum = isEnum; + cproverNextClass = literals[0]; + literals[0] = this; + } + + @org.cprover.MustNotThrow + private static Class cproverGetClassObject( + String name, + boolean isAnnotation, + boolean isArray, + boolean isInterface, + boolean isSynthetic, + boolean isLocalClass, + boolean isMemberClass, + boolean isEnum) { + Class c = findOther(name); + if (c == null) + c = newOther(name); + c.cproverIsEnum = isEnum; + return c; + } +} diff --git a/jbmc/regression/jbmc/get-class-for-name/twoClasses.desc b/jbmc/regression/jbmc/get-class-for-name/twoClasses.desc new file mode 100644 index 000000000000..cb0305aabf50 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/twoClasses.desc @@ -0,0 +1,14 @@ +CORE +Test +--function Test.twoClasses -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Object.getClass must return the same java.lang.Class object as +Class.forName, also for classes whose class literal the program does not +refer to, irrespective of which of the two is called first. JBMC obtains the +Class object of such a class from cproverGetClassObject of the model of +java.lang.Class on the first call of getClass for that class. diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index c86b414d0f38..02a7931292bc 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -165,6 +165,7 @@ function4 generic_base_type get-class + get-class-for-name generic_class_bound1 generic_function_parameter generic_static_field diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 1fbd9ee08e6f..b803a1192581 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -793,12 +793,26 @@ static void create_stub_global_symbols( } } -/// Name of the global flag that records whether the class literal of -/// \p class_id, which \ref create_get_class_methods created, has been -/// initialised. -static irep_idt lazy_class_literal_initialized_name(const irep_idt &class_id) +/// Name of the global that \ref get_class_method_body uses to store the +/// java.lang.Class object of \p class_id if the program does not refer to +/// its class literal. It is null until getClass is first called on an object +/// of that class. +static irep_idt lazy_class_object_name(const irep_idt &class_id) { - return id2string(class_id) + "@class_model_initialized"; + return id2string(class_id) + "@class_object"; +} + +/// Signature of the method of the model of java.lang.Class that returns the +/// Class object of a class whose class literal the program does not refer +/// to. It takes the same arguments as cproverInitializeClassLiteral, and +/// returns the Class object that Class.forName created for this class, if +/// any, and a new one otherwise. +static const irep_idt &class_object_factory_signature() +{ + static const irep_idt signature = + "java::java.lang.Class.cproverGetClassObject:" + "(Ljava/lang/String;ZZZZZZZ)Ljava/lang/Class;"; + return signature; } static const irep_idt &object_get_class_name() @@ -809,14 +823,14 @@ static const irep_idt &object_get_class_name() } /// For each class that can have instances, add a method `getClass` that -/// overrides java.lang.Object.getClass and returns the class's class literal +/// overrides java.lang.Object.getClass and returns the class's Class object /// (see \ref get_class_method_body). Only the symbols are created here, the /// bodies are generated when the methods are converted, so that this is /// compatible with lazy loading: context-insensitive lazy loading only converts /// the overrides of classes that are instantiated, and symex-driven lazy /// loading converts those of the runtime types that symbolic execution -/// encounters. The class literals are created up front, as all of them must -/// exist before __CPROVER_initialize is generated. +/// encounters. Any symbols that the bodies use are created up front, as all +/// globals must exist before __CPROVER_initialize is generated. /// \param symbol_table: global symbol table /// \param synthetic_methods: synthetic method map, to which the methods are /// added @@ -829,6 +843,11 @@ static void create_get_class_methods( if(object_get_class == nullptr || object_get_class->value.is_not_nil()) return; + const bool have_class_object_factory = + symbol_table.has_symbol(class_object_factory_signature()); + const bool have_class_literal_initializer = + symbol_table.has_symbol(get_java_class_literal_initializer_signature()); + // Careful not to add to the symbol table while iterating over it std::vector class_ids; for(const auto &entry : symbol_table) @@ -856,30 +875,37 @@ static void create_get_class_methods( if(symbol_table.has_symbol(method_id)) continue; - // If the program does not refer to the class literal, create one that is - // only initialised once getClass is first called for this class (see - // get_class_method_body): initialising the class literals of all classes - // in __CPROVER_initialize would be expensive with symex-driven lazy - // loading, which does not remove unused globals. + // If the program does not refer to the class literal, the Class object + // is only created or initialised once getClass is first called for this + // class (see get_class_method_body): initialising the class literals of + // all classes in __CPROVER_initialize would be expensive with + // symex-driven lazy loading, which does not remove unused globals. const irep_idt literal_id = id2string(class_id) + JAVA_CLASS_MODEL_SUFFIX; - if(!symbol_table.has_symbol(literal_id)) + if( + !symbol_table.has_symbol(literal_id) && + (have_class_object_factory || have_class_literal_initializer)) { - get_or_create_class_literal_symbol(class_id, symbol_table); - symbol_table.get_writeable_ref(literal_id) - .type.set(ID_C_no_initialization_required, true); - - symbolt initialized_symbol{ - lazy_class_literal_initialized_name(class_id), - java_boolean_type(), - ID_java}; - initialized_symbol.base_name = - id2string(initialized_symbol.name).substr(6); - initialized_symbol.is_lvalue = true; - initialized_symbol.is_state_var = true; - initialized_symbol.is_static_lifetime = true; - initialized_symbol.value = from_integer(0, java_boolean_type()); - symbol_table.add(initialized_symbol); + if(!have_class_object_factory) + { + get_or_create_class_literal_symbol(class_id, symbol_table); + symbol_table.get_writeable_ref(literal_id) + .type.set(ID_C_no_initialization_required, true); + } + + const typet &class_reference_type = object_get_class_type.return_type(); + symbolt class_object_symbol{ + lazy_class_object_name(class_id), class_reference_type, ID_java}; + class_object_symbol.base_name = + id2string(class_object_symbol.name).substr(6); + class_object_symbol.is_lvalue = true; + class_object_symbol.is_state_var = true; + class_object_symbol.is_static_lifetime = true; + class_object_symbol.value = + null_pointer_exprt{to_pointer_type(class_reference_type)}; + symbol_table.add(class_object_symbol); } + else + get_or_create_class_literal_symbol(class_id, symbol_table); java_method_typet method_type = object_get_class_type; method_type.set_is_final(true); @@ -898,25 +924,35 @@ static void create_get_class_methods( } /// Body of an override of java.lang.Object.getClass created by -/// \ref create_get_class_methods for class C: +/// \ref create_get_class_methods for class C. If the program refers to the +/// class literal of C, which __CPROVER_initialize then initialises, or the +/// model of java.lang.Class has neither cproverGetClassObject nor +/// cproverInitializeClassLiteral: /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ /// return &C@class_model; /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -/// If the program does not refer to the class literal, so that -/// __CPROVER_initialize does not initialise it, the class literal is -/// initialised on the first call instead, in the same way as -/// java_static_lifetime_init does, except that the name is obtained via -/// CProver.classIdentifier, as no new String literals can be created at this -/// point: +/// Otherwise, the Class object is obtained on the first call from the model +/// of java.lang.Class, which returns the object that Class.forName created +/// for C, if any. The name is obtained via CProver.classIdentifier, as no new +/// String literals can be created at this point: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// if(C@class_object == null) +/// C@class_object = Class.cproverGetClassObject( +/// CProver.classIdentifier(this), ...); +/// return C@class_object; +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// With a model of java.lang.Class that does not have cproverGetClassObject, +/// the class literal is initialised instead, in the same way as +/// java_static_lifetime_init does: /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -/// if(!C@class_model_initialized) +/// if(C@class_object == null) /// { -/// C@class_model_initialized = true; /// C@class_model = { zero-initialised object of type java.lang.Class }; /// C@class_model.cproverInitializeClassLiteral( /// CProver.classIdentifier(this), ...); +/// C@class_object = &C@class_model; /// } -/// return &C@class_model; +/// return C@class_object; /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ /// \param function_id: name of the method /// \param symbol_table: global symbol table @@ -941,23 +977,100 @@ static codet get_class_method_body( const auto class_id = declaring_class(symbol); INVARIANT(class_id.has_value(), "getClass override must have a class"); - const symbol_exprt class_literal = - symbol_table.lookup_ref(id2string(*class_id) + JAVA_CLASS_MODEL_SUFFIX) - .symbol_expr(); const source_locationt &loc = symbol.location; + const irep_idt literal_id = id2string(*class_id) + JAVA_CLASS_MODEL_SUFFIX; code_blockt code; - const symbolt *initialized = - symbol_table.lookup(lazy_class_literal_initialized_name(*class_id)); + const symbolt *class_object = + symbol_table.lookup(lazy_class_object_name(*class_id)); + if(class_object == nullptr) + { + code.add(code_frontend_returnt{typecast_exprt::conditional_cast( + address_of_exprt{symbol_table.lookup_ref(literal_id).symbol_expr()}, + method_type.return_type())}); + return std::move(code); + } + + const symbolt *factory = + symbol_table.lookup(class_object_factory_signature()); const symbolt *initializer = symbol_table.lookup(get_java_class_literal_initializer_signature()); - if(initialized != nullptr && initializer != nullptr) + INVARIANT( + factory != nullptr || initializer != nullptr, + "create_get_class_methods only creates " + id2string(class_object->name) + + " if the model of java.lang.Class can initialise it"); + const java_method_typet &callee_type = + to_java_method_type((factory != nullptr ? factory : initializer)->type); + // cproverGetClassObject is static, cproverInitializeClassLiteral takes the + // class literal as its first argument + const typet &string_type = + callee_type.parameters()[factory != nullptr ? 0 : 1].type(); + + code_blockt init; + + exprt name = null_pointer_exprt{to_pointer_type(string_type)}; + const symbolt *class_identifier = symbol_table.lookup( + "java::org.cprover.CProver.classIdentifier:" + "(Ljava/lang/Object;)Ljava/lang/String;"); + if(class_identifier != nullptr) { - code_blockt init; - init.add(code_frontend_assignt{ - initialized->symbol_expr(), from_integer(1, java_boolean_type())}); + const symbolt &name_symbol = fresh_java_symbol( + string_type, "class_name", loc, function_id, symbol_table); + init.add(code_frontend_declt{name_symbol.symbol_expr()}); + const java_method_typet &class_identifier_type = + to_java_method_type(class_identifier->type); + init.add(code_function_callt{ + name_symbol.symbol_expr(), + class_identifier->symbol_expr(), + {typecast_exprt::conditional_cast( + symbol_exprt{ + method_type.parameters()[0].get_identifier(), + method_type.parameters()[0].type()}, + class_identifier_type.parameters()[0].type())}}); + name = name_symbol.symbol_expr(); + } + const java_class_typet &class_type = + to_java_class_type(symbol_table.lookup_ref(*class_id).type); + auto constant_bool = [](bool b) + { return from_integer(b ? 1 : 0, java_boolean_type()); }; + const side_effect_expr_nondett nondet_bool{java_boolean_type(), loc}; + // Argument order is: name, isAnnotation, isArray, isInterface, + // isSynthetic, isLocalClass, isMemberClass, isEnum + exprt::operandst arguments{ + name, + constant_bool(class_type.get_is_annotation()), + constant_bool(false), + constant_bool(class_type.get_interface()), + constant_bool(class_type.get_synthetic()), + nondet_bool, + nondet_bool, + constant_bool(class_type.get_is_enumeration())}; + + const symbol_exprt class_object_expr = class_object->symbol_expr(); + if(factory != nullptr) + { + const symbolt &result_symbol = fresh_java_symbol( + callee_type.return_type(), + "class_object", + loc, + function_id, + symbol_table); + init.add(code_frontend_declt{result_symbol.symbol_expr()}); + init.add(code_function_callt{ + result_symbol.symbol_expr(), + factory->symbol_expr(), + std::move(arguments)}); + init.add(code_frontend_assignt{ + class_object_expr, + typecast_exprt::conditional_cast( + result_symbol.symbol_expr(), class_object_expr.type())}); + } + else + { + const symbol_exprt class_literal = + symbol_table.lookup_ref(literal_id).symbol_expr(); const namespacet ns{symbol_table}; auto zero_object = zero_initializer(class_literal.type(), loc, ns); if(!zero_object.has_value()) @@ -973,58 +1086,22 @@ static codet get_class_method_body( to_struct_tag_type(class_literal.type())); init.add(code_frontend_assignt{class_literal, *zero_object}); - const java_method_typet &initializer_type = - to_java_method_type(initializer->type); - const typet &string_type = initializer_type.parameters()[1].type(); - exprt name = null_pointer_exprt{to_pointer_type(string_type)}; - const symbolt *class_identifier = symbol_table.lookup( - "java::org.cprover.CProver.classIdentifier:" - "(Ljava/lang/Object;)Ljava/lang/String;"); - if(class_identifier != nullptr) - { - const symbolt &name_symbol = fresh_java_symbol( - string_type, "class_name", loc, function_id, symbol_table); - init.add(code_frontend_declt{name_symbol.symbol_expr()}); - const java_method_typet &class_identifier_type = - to_java_method_type(class_identifier->type); - init.add(code_function_callt{ - name_symbol.symbol_expr(), - class_identifier->symbol_expr(), - {typecast_exprt::conditional_cast( - symbol_exprt{ - method_type.parameters()[0].get_identifier(), - method_type.parameters()[0].type()}, - class_identifier_type.parameters()[0].type())}}); - name = name_symbol.symbol_expr(); - } - - const java_class_typet &class_type = - to_java_class_type(symbol_table.lookup_ref(*class_id).type); - auto constant_bool = [](bool b) - { return from_integer(b ? 1 : 0, java_boolean_type()); }; - const side_effect_expr_nondett nondet_bool{java_boolean_type(), loc}; - // Argument order is: name, isAnnotation, isArray, isInterface, - // isSynthetic, isLocalClass, isMemberClass, isEnum - init.add(code_function_callt{ - initializer->symbol_expr(), - {address_of_exprt{class_literal}, - name, - constant_bool(class_type.get_is_annotation()), - constant_bool(false), - constant_bool(class_type.get_interface()), - constant_bool(class_type.get_synthetic()), - nondet_bool, - nondet_bool, - constant_bool(class_type.get_is_enumeration())}}); - - code.add(code_ifthenelset{ - equal_exprt{ - initialized->symbol_expr(), from_integer(0, java_boolean_type())}, - init}); + arguments.insert(arguments.begin(), address_of_exprt{class_literal}); + init.add( + code_function_callt{initializer->symbol_expr(), std::move(arguments)}); + init.add(code_frontend_assignt{ + class_object_expr, + typecast_exprt::conditional_cast( + address_of_exprt{class_literal}, class_object_expr.type())}); } + code.add(code_ifthenelset{ + equal_exprt{ + class_object_expr, + null_pointer_exprt{to_pointer_type(class_object_expr.type())}}, + std::move(init)}); code.add(code_frontend_returnt{typecast_exprt::conditional_cast( - address_of_exprt{class_literal}, method_type.return_type())}); + class_object_expr, method_type.return_type())}); return std::move(code); } From e9224560beafdf94a69187868f81442f96e9509a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 4 Nov 2026 18:05:44 +0000 Subject: [PATCH 4/5] JBMC: bind super.getClass() calls dynamically Object.getClass is final, so that super.getClass() returns the Class object of the runtime type of the receiver, just like getClass(). javac compiles super.getClass() to invokespecial java/lang/Object.getClass, but other compilers may name the superclass, e.g. invokespecial A.getClass in a subclass B of A. JBMC binds invokespecial calls statically, so that such a call reached the getClass override of A that JBMC now creates, and returned the Class object of A instead of B. Bind invokespecial calls of getClass:()Ljava/lang/Class; dynamically instead, so that they reach the override of the runtime type. This also applies to javac's form, which thus no longer goes through the model of Object.getClass. The new regression test get-class-invokespecial uses Jasmin to create such an invokespecial instruction; it fails without this change. Co-authored-by: Kiro --- .../jbmc/get-class-invokespecial/pom.xml | 34 ++++++++++++++ .../get-class-invokespecial/src/main/java/A.j | 8 ++++ .../get-class-invokespecial/src/main/java/B.j | 47 +++++++++++++++++++ .../jbmc/get-class-invokespecial/test.desc | 13 +++++ jbmc/regression/jbmc/pom.xml | 1 + .../java_bytecode_convert_method.cpp | 15 +++++- 6 files changed, 116 insertions(+), 2 deletions(-) create mode 100644 jbmc/regression/jbmc/get-class-invokespecial/pom.xml create mode 100644 jbmc/regression/jbmc/get-class-invokespecial/src/main/java/A.j create mode 100644 jbmc/regression/jbmc/get-class-invokespecial/src/main/java/B.j create mode 100644 jbmc/regression/jbmc/get-class-invokespecial/test.desc diff --git a/jbmc/regression/jbmc/get-class-invokespecial/pom.xml b/jbmc/regression/jbmc/get-class-invokespecial/pom.xml new file mode 100644 index 000000000000..ee9cfaad48cc --- /dev/null +++ b/jbmc/regression/jbmc/get-class-invokespecial/pom.xml @@ -0,0 +1,34 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.get-class-invokespecial + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + com.github.abextm + jasmin-maven-plugin + + + + + diff --git a/jbmc/regression/jbmc/get-class-invokespecial/src/main/java/A.j b/jbmc/regression/jbmc/get-class-invokespecial/src/main/java/A.j new file mode 100644 index 000000000000..ba3dc5596fbe --- /dev/null +++ b/jbmc/regression/jbmc/get-class-invokespecial/src/main/java/A.j @@ -0,0 +1,8 @@ +.class public A +.super java/lang/Object + +.method public ()V + aload_0 + invokespecial java/lang/Object/()V + return +.end method diff --git a/jbmc/regression/jbmc/get-class-invokespecial/src/main/java/B.j b/jbmc/regression/jbmc/get-class-invokespecial/src/main/java/B.j new file mode 100644 index 000000000000..c979f3836cb5 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-invokespecial/src/main/java/B.j @@ -0,0 +1,47 @@ +.class public B +.super A + +.method public ()V + aload_0 + invokespecial A/()V + return +.end method + +.method public viaSuper()Ljava/lang/Class; + .limit stack 1 + .limit locals 1 + aload_0 + invokespecial A/getClass()Ljava/lang/Class; + areturn +.end method + +; assert new B().viaSuper() == new B().getClass(); +; assert new B().viaSuper() != new A().getClass(); +.method public static test()V + .limit stack 3 + .limit locals 0 + new B + dup + invokespecial B/()V + invokevirtual B/viaSuper()Ljava/lang/Class; + new B + dup + invokespecial B/()V + invokevirtual java/lang/Object/getClass()Ljava/lang/Class; + if_acmpne fail + new B + dup + invokespecial B/()V + invokevirtual B/viaSuper()Ljava/lang/Class; + new A + dup + invokespecial A/()V + invokevirtual java/lang/Object/getClass()Ljava/lang/Class; + if_acmpeq fail + return +fail: + new java/lang/AssertionError + dup + invokespecial java/lang/AssertionError/()V + athrow +.end method diff --git a/jbmc/regression/jbmc/get-class-invokespecial/test.desc b/jbmc/regression/jbmc/get-class-invokespecial/test.desc new file mode 100644 index 000000000000..cd8a40477083 --- /dev/null +++ b/jbmc/regression/jbmc/get-class-invokespecial/test.desc @@ -0,0 +1,13 @@ +CORE +B +--function B.test -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +super.getClass() must return the Class object of the runtime type of the +receiver, as Object.getClass is final. javac emits invokespecial +java/lang/Object/getClass for super.getClass(), but other compilers may name +the superclass (here: A) instead, which must not bind to A's getClass override. diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml index 02a7931292bc..bca53c21d261 100644 --- a/jbmc/regression/jbmc/pom.xml +++ b/jbmc/regression/jbmc/pom.xml @@ -166,6 +166,7 @@ generic_base_type get-class get-class-for-name + get-class-invokespecial generic_class_bound1 generic_function_parameter generic_static_field diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index a6e650389dc0..66e75806f614 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2236,8 +2236,19 @@ void java_bytecode_convert_methodt::convert_invoke( exprt::operandst &results) { const bool use_this(statement != "invokestatic"); + // Object.getClass is final, so that getClass always returns the Class object + // of the runtime type of the receiver, also when called via invokespecial + // (super.getClass()). Bind such calls dynamically, so that they reach the + // override of the runtime type that java_bytecode_languaget creates, rather + // than that of the class that invokespecial names (javac names + // java.lang.Object, other compilers may name the superclass). + const bool is_get_class_call = + statement == "invokespecial" && + class_method_descriptor.mangled_method_name() == + "getClass:()Ljava/lang/Class;"; const bool is_virtual( - statement == "invokevirtual" || statement == "invokeinterface"); + statement == "invokevirtual" || statement == "invokeinterface" || + is_get_class_call); const irep_idt &invoked_method_id = class_method_descriptor.get_identifier(); INVARIANT( @@ -2292,7 +2303,7 @@ void java_bytecode_convert_methodt::convert_invoke( needed_lazy_methods->add_needed_class(class_id); method_type.set_is_constructor(); } - else + else if(!is_get_class_call) method_type.set(ID_java_super_method_call, true); } } From 4c8c3bdc986f9bff0db921cfe775e1cf8d109bd4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 4 Nov 2026 18:18:54 +0000 Subject: [PATCH 5/5] JBMC: obtain lazily created Class objects thread-safely With --java-threading, two threads could both find that the Class object of a class whose class literal the program does not refer to has not been obtained yet, and both call cproverGetClassObject, or one thread could see the Class object before it was initialised. With --java-threading, use the protocol of the thread-safe static initializer wrappers instead: in an atomic section, a thread waits (via an assumption) while another thread obtains the Class object, and claims the task if no thread has done so yet; once done, it records completion in another atomic section. Obtaining the Class object does not call getClass for the same class, so that, unlike for static initializers, recursive initialisation by the same thread need not be handled. Without --java-threading, the code is unchanged. The new test get-class-for-name/threading.desc runs one of the existing cases with --java-threading. In a program in which two threads call getClass for the same class, JBMC did not report a violation of uniqueness either before or after this change, with --unwind 2 taking about 335 seconds in both cases, which is too long for a regression test. Co-authored-by: Kiro --- .../jbmc/get-class-for-name/threading.desc | 11 +++ .../java_bytecode/java_bytecode_language.cpp | 99 +++++++++++++++++-- 2 files changed, 101 insertions(+), 9 deletions(-) create mode 100644 jbmc/regression/jbmc/get-class-for-name/threading.desc diff --git a/jbmc/regression/jbmc/get-class-for-name/threading.desc b/jbmc/regression/jbmc/get-class-for-name/threading.desc new file mode 100644 index 000000000000..447cc55507ea --- /dev/null +++ b/jbmc/regression/jbmc/get-class-for-name/threading.desc @@ -0,0 +1,11 @@ +CORE +Test +--function Test.forNameThenGetClass --java-threading -cp `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +With --java-threading, getClass obtains the Class object using the same +protocol as the thread-safe static initializer wrappers. diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index b803a1192581..22efba9e67cb 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -802,6 +802,14 @@ static irep_idt lazy_class_object_name(const irep_idt &class_id) return id2string(class_id) + "@class_object"; } +/// Name of the global that, with --java-threading, records whether a thread +/// has started (1) or completed (2) obtaining the Class object stored in +/// \ref lazy_class_object_name. +static irep_idt lazy_class_object_state_name(const irep_idt &class_id) +{ + return id2string(class_id) + "@class_object_state"; +} + /// Signature of the method of the model of java.lang.Class that returns the /// Class object of a class whose class literal the program does not refer /// to. It takes the same arguments as cproverInitializeClassLiteral, and @@ -834,9 +842,11 @@ static const irep_idt &object_get_class_name() /// \param symbol_table: global symbol table /// \param synthetic_methods: synthetic method map, to which the methods are /// added +/// \param threading_support: true if --java-threading was given static void create_get_class_methods( symbol_table_baset &symbol_table, - synthetic_methods_mapt &synthetic_methods) + synthetic_methods_mapt &synthetic_methods, + bool threading_support) { const symbolt *object_get_class = symbol_table.lookup(object_get_class_name()); @@ -903,6 +913,18 @@ static void create_get_class_methods( class_object_symbol.value = null_pointer_exprt{to_pointer_type(class_reference_type)}; symbol_table.add(class_object_symbol); + + if(threading_support) + { + symbolt state_symbol{ + lazy_class_object_state_name(class_id), java_int_type(), ID_java}; + state_symbol.base_name = id2string(state_symbol.name).substr(6); + state_symbol.is_lvalue = true; + state_symbol.is_state_var = true; + state_symbol.is_static_lifetime = true; + state_symbol.value = from_integer(0, java_int_type()); + symbol_table.add(state_symbol); + } } else get_or_create_class_literal_symbol(class_id, symbol_table); @@ -941,6 +963,28 @@ static void create_get_class_methods( /// CProver.classIdentifier(this), ...); /// return C@class_object; /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// With --java-threading, only one thread obtains the Class object, and other +/// threads wait for it to complete, as in the thread-safe static initializer +/// wrappers (see get_thread_safe_clinit_wrapper_body): +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// ATOMIC_BEGIN +/// assume(C@class_object_state != 1); +/// must_init = C@class_object_state == 0; +/// if(must_init) +/// C@class_object_state = 1; +/// ATOMIC_END +/// if(must_init) +/// { +/// C@class_object = Class.cproverGetClassObject(...); +/// ATOMIC_BEGIN +/// C@class_object_state = 2; +/// ATOMIC_END +/// } +/// return C@class_object; +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// Obtaining the Class object does not call getClass for C, so that this does +/// not need to handle recursive initialisation as the static initializer +/// wrappers do. /// With a model of java.lang.Class that does not have cproverGetClassObject, /// the class literal is initialised instead, in the same way as /// java_static_lifetime_init does: @@ -956,11 +1000,13 @@ static void create_get_class_methods( /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ /// \param function_id: name of the method /// \param symbol_table: global symbol table +/// \param threading_support: true if --java-threading was given /// \param message_handler: message handler /// \return code of the method static codet get_class_method_body( const irep_idt &function_id, symbol_table_baset &symbol_table, + bool threading_support, message_handlert &message_handler) { const symbolt &symbol = symbol_table.lookup_ref(function_id); @@ -1095,11 +1141,42 @@ static codet get_class_method_body( address_of_exprt{class_literal}, class_object_expr.type())}); } - code.add(code_ifthenelset{ - equal_exprt{ - class_object_expr, - null_pointer_exprt{to_pointer_type(class_object_expr.type())}}, - std::move(init)}); + const symbolt *state = + symbol_table.lookup(lazy_class_object_state_name(*class_id)); + if(threading_support && state != nullptr) + { + const symbol_exprt state_expr = state->symbol_expr(); + auto state_value = [](int value) + { return from_integer(value, java_int_type()); }; + const symbolt &must_init = fresh_java_symbol( + java_boolean_type(), "must_init", loc, function_id, symbol_table); + const symbol_exprt must_init_expr = must_init.symbol_expr(); + code.add(code_frontend_declt{must_init_expr}); + code.add(codet{ID_atomic_begin}); + code.add(code_assumet{notequal_exprt{state_expr, state_value(1)}}); + code.add(code_frontend_assignt{ + must_init_expr, + typecast_exprt{ + equal_exprt{state_expr, state_value(0)}, java_boolean_type()}}); + code.add(code_ifthenelset{ + equal_exprt{state_expr, state_value(0)}, + code_frontend_assignt{state_expr, state_value(1)}}); + code.add(codet{ID_atomic_end}); + init.add(codet{ID_atomic_begin}); + init.add(code_frontend_assignt{state_expr, state_value(2)}); + init.add(codet{ID_atomic_end}); + code.add(code_ifthenelset{ + notequal_exprt{must_init_expr, from_integer(0, java_boolean_type())}, + std::move(init)}); + } + else + { + code.add(code_ifthenelset{ + equal_exprt{ + class_object_expr, + null_pointer_exprt{to_pointer_type(class_object_expr.type())}}, + std::move(init)}); + } code.add(code_frontend_returnt{typecast_exprt::conditional_cast( class_object_expr, method_type.return_type())}); return std::move(code); @@ -1250,7 +1327,8 @@ bool java_bytecode_languaget::typecheck( } } - create_get_class_methods(symbol_table, synthetic_methods); + create_get_class_methods( + symbol_table, synthetic_methods, language_options->threading_support); messaget log(message_handler); log.status() << "Java: added " @@ -1754,8 +1832,11 @@ bool java_bytecode_languaget::convert_single_method_code( function_id, symbol_table, message_handler); break; case synthetic_method_typet::GET_CLASS: - writable_symbol.value = - get_class_method_body(function_id, symbol_table, message_handler); + writable_symbol.value = get_class_method_body( + function_id, + symbol_table, + language_options->threading_support, + message_handler); break; case synthetic_method_typet::CREATE_ARRAY_WITH_TYPE: {