From 3be826f39d33786902d793a7376f13846e088a7e Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 6 Aug 2018 16:50:31 +0100 Subject: [PATCH 1/9] Add some documentation to java_object_factory Add a high-level overview of the recursive algorithm in the file. --- jbmc/src/java_bytecode/java_object_factory.cpp | 4 ++-- jbmc/src/java_bytecode/java_object_factory.h | 9 ++++++--- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 2760a9936bb..4693eb0c745 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -974,7 +974,7 @@ void java_object_factoryt::gen_nondet_struct_init( // Should we write the whole object? // * Not if this is a sub-structure (a superclass object), as our caller will // have done this already - // * Not if the object has already been initialised by our caller, in whic + // * Not if the object has already been initialised by our caller, in which // case they will set `skip_classid` // * Not if we're re-initializing an existing object (i.e. update_in_place) @@ -1094,7 +1094,7 @@ void java_object_factoryt::gen_nondet_struct_init( } } -/// Initializes a primitive-typed or referece-typed object tree rooted at +/// Initializes a primitive-typed or reference-typed object tree rooted at /// `expr`, allocating child objects as necessary and nondet-initializing their /// members, or if MUST_UPDATE_IN_PLACE is set, re-initializing /// already-allocated objects. diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h index d174d4e4ae2..acde2f165fe 100644 --- a/jbmc/src/java_bytecode/java_object_factory.h +++ b/jbmc/src/java_bytecode/java_object_factory.h @@ -19,8 +19,9 @@ Author: Daniel Kroening, kroening@kroening.com /// that are called but for which we don't have a body (overapproximating the /// return value and possibly side effects). /// -/// The two main APIs are \ref gen_nondet_init() and \ref object_factory(), at -/// the bottom of the file. Their purpose is very similar. A call to +/// The two main APIs are \ref gen_nondet_init() and \ref object_factory() +/// (which calls gen_nondet_init()), at the bottom of the file. +/// A call to /// /// gen_nondet_init(expr, code, ..., update_in_place) /// @@ -28,7 +29,9 @@ Author: Daniel Kroening, kroening@kroening.com /// non-deterministically initialize the `expr` (which is expected to be an /// l-value exprt) with a primitive or reference value of type equal to or /// compatible with `expr.type()` -- see documentation for the argument -/// `pointer_type_selector` for additional details. +/// `pointer_type_selector` for additional details. gen_nondet_init() is the +/// starting point of a recursive algorithm, and most other functions in this +/// file are different (recursive or base) cases depending on the type of expr. /// /// The code generated mainly depends on the parameter `update_in_place`. Assume /// that `expr` is a reference to an object (in our IR, that means a pointer to From 07d1e446fbc6e820d73b6fc1adc77d507ff885ca Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 6 Aug 2018 19:34:24 +0100 Subject: [PATCH 2/9] 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. --- .../src/java_bytecode/java_object_factory.cpp | 61 ++++++++++++++----- 1 file changed, 46 insertions(+), 15 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 4693eb0c745..5522fc4e723 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -148,6 +148,11 @@ class java_object_factoryt const pointer_typet &substitute_pointer_type, size_t depth, const source_locationt &location); + + void gen_method_call_if_present( + code_blockt &assignments, + const exprt &instance_expr, + const irep_idt &method_name); }; /// Generates code for allocating a dynamic object. This is used in @@ -764,6 +769,24 @@ void java_object_factoryt::gen_nondet_pointer_init( } } + // If this is a void* we *must* initialise with null: + // (This can currently happen for some cases of #exception_value) + bool must_be_null = subtype == empty_typet(); + + // If we may be about to initialize a non-null object, always run the + // clinit_wrapper of its class first. + // Note that it would be more consistent with the behaviour of the JVM to only + // run clinit_wrapper if we are about to initialize an object of which we know + // for sure that it is not null on any following branch. However, adding this + // case in gen_nondet_struct_init would slow symex down too much. + if(!must_be_null) + { + const java_class_typet &class_type = to_java_class_type(subtype); + const irep_idt &class_name = class_type.get_name(); + const irep_idt class_clinit = clinit_wrapper_name(class_name); + gen_method_call_if_present(assignments, expr, class_clinit); + } + code_blockt new_object_assignments; code_blockt update_in_place_assignments; @@ -810,10 +833,6 @@ void java_object_factoryt::gen_nondet_pointer_init( const bool allow_null = depth > object_factory_parameters.max_nonnull_tree_depth; - // Alternatively, if this is a void* we *must* initialise with null: - // (This can currently happen for some cases of #exception_value) - bool must_be_null = subtype == empty_typet(); - if(must_be_null) { // Add the following code to assignments: @@ -1081,17 +1100,7 @@ void java_object_factoryt::gen_nondet_struct_init( const irep_idt init_method_name = "java::" + id2string(struct_tag) + ".cproverNondetInitialize:()V"; - - if(const auto func = symbol_table.lookup(init_method_name)) - { - const java_method_typet &type = to_java_method_type(func->type); - code_function_callt fun_call; - fun_call.function() = func->symbol_expr(); - if(type.has_this()) - fun_call.arguments().push_back(address_of_exprt(expr)); - - assignments.add(fun_call); - } + gen_method_call_if_present(assignments, expr, init_method_name); } /// Initializes a primitive-typed or reference-typed object tree rooted at @@ -1619,3 +1628,25 @@ void gen_nondet_init( pointer_type_selector, update_in_place); } + +/// Adds a call for the given method to the end of `assignments` if the method +/// exists in the symbol table. Does nothing if the method does not exist. +/// \param assignments: A code block that the method call will be appended to. +/// \param instance_expr: The instance to call the method on. This argument is +/// ignored if the method is static. +/// \param method_name: The name of the method to be called. +void java_object_factoryt::gen_method_call_if_present( + code_blockt &assignments, + const exprt &instance_expr, + const irep_idt &method_name) +{ + if(const auto func = symbol_table.lookup(method_name)) + { + const java_method_typet &type = to_java_method_type(func->type); + code_function_callt fun_call; + fun_call.function() = func->symbol_expr(); + if(type.has_this()) + fun_call.arguments().push_back(address_of_exprt(instance_expr)); + assignments.add(fun_call); + } +} From 6c84caa1cc583a4a75654cf2dfa226bd4d5f8db2 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Thu, 9 Aug 2018 12:43:59 +0100 Subject: [PATCH 3/9] Refactor logic for generating a nondet int --- .../src/java_bytecode/java_object_factory.cpp | 98 +++++++++++++------ 1 file changed, 66 insertions(+), 32 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 5522fc4e723..564ca42be9b 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -149,6 +149,13 @@ class java_object_factoryt size_t depth, const source_locationt &location); + const symbol_exprt gen_nondet_int_init( + code_blockt &assignments, + const std::string &basename_prefix, + const exprt &min_length_expr, + const exprt &max_length_expr, + const source_locationt &location); + void gen_method_call_if_present( code_blockt &assignments, const exprt &instance_expr, @@ -1218,6 +1225,60 @@ void java_object_factoryt::gen_nondet_init( } } +/// Nondeterministically initializes an int i in the range min <= i <= max, +/// where min is the integer represented by `min_value_expr` and max is the +/// integer represented by `max_value_expr`. +/// \param [out] assignments: A code block that the initializing assignments +/// will be appended to. +/// \param basename_prefix: Used for naming the newly created symbol. +/// \param min_value_expr: Represents the minimum value for the integer. +/// \param max_value_expr: Represents the maximum value for the integer. +/// \param location: Source location associated with nondet-initialization. +/// \return A symbol expression for the resulting integer. +const symbol_exprt java_object_factoryt::gen_nondet_int_init( + code_blockt &assignments, + const std::string &basename_prefix, + const exprt &min_value_expr, + const exprt &max_value_expr, + const source_locationt &location) +{ + PRECONDITION(min_value_expr.type() == max_value_expr.type()); + // Allocate a new symbol for the int + const symbolt &int_symbol = get_fresh_aux_symbol( + min_value_expr.type(), + id2string(object_factory_parameters.function_id), + basename_prefix, + loc, + ID_java, + symbol_table); + symbols_created.push_back(&int_symbol); + const auto &int_symbol_expr = int_symbol.symbol_expr(); + + // Nondet-initialize it + gen_nondet_init( + assignments, + int_symbol_expr, + false, // is_sub + irep_idt(), + false, // skip_classid + allocation_typet::LOCAL, // immaterial, type is primitive + false, // override + typet(), // override type is immaterial + 0, // depth is immaterial, always non-null + update_in_placet::NO_UPDATE_IN_PLACE, + location); + + // Insert assumptions to bound its value + const auto min_assume_expr = + binary_relation_exprt(int_symbol_expr, ID_ge, min_value_expr); + const auto max_assume_expr = + binary_relation_exprt(int_symbol_expr, ID_le, max_value_expr); + assignments.add(code_assumet(min_assume_expr)); + assignments.add(code_assumet(max_assume_expr)); + + return int_symbol_expr; +} + /// Allocates a fresh array and emits an assignment writing to \p lhs the /// address of the new array. Single-use at the moment, but useful to keep as a /// separate function for downstream branches. @@ -1238,46 +1299,19 @@ void java_object_factoryt::allocate_nondet_length_array( const typet &element_type, const source_locationt &location) { - symbolt &length_sym = get_fresh_aux_symbol( - java_int_type(), - id2string(object_factory_parameters.function_id), - "nondet_array_length", - loc, - ID_java, - symbol_table); - symbols_created.push_back(&length_sym); - const auto &length_sym_expr=length_sym.symbol_expr(); - - // Initialize array with some undetermined length: - gen_nondet_init( + const auto &length_sym_expr = gen_nondet_int_init( assignments, - length_sym_expr, - false, // is_sub - irep_idt(), - false, // skip_classid - allocation_typet::LOCAL, // immaterial, type is primitive - false, // override - typet(), // override type is immaterial - 0, // depth is immaterial, always non-null - update_in_placet::NO_UPDATE_IN_PLACE, + "nondet_array_length", + from_integer(0, java_int_type()), + max_length_expr, location); - // Insert assumptions to bound its length: - binary_relation_exprt - assume1(length_sym_expr, ID_ge, from_integer(0, java_int_type())); - binary_relation_exprt - assume2(length_sym_expr, ID_le, max_length_expr); - code_assumet assume_inst1(assume1); - code_assumet assume_inst2(assume2); - assignments.move_to_operands(assume_inst1); - assignments.move_to_operands(assume_inst2); - side_effect_exprt java_new_array(ID_java_new_array, lhs.type(), loc); java_new_array.copy_to_operands(length_sym_expr); java_new_array.set(ID_length_upper_bound, max_length_expr); java_new_array.type().subtype().set(ID_element_type, element_type); code_assignt assign(lhs, java_new_array); - assign.add_source_location()=loc; + assign.add_source_location() = loc; assignments.copy_to_operands(assign); } From 6ecf4f912e8ee8a98bf0d214755958e01af23536 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Thu, 9 Aug 2018 13:37:10 +0100 Subject: [PATCH 4/9] Nondet-init enums by assigning them to a constant Rather than nondet-initializing each field (String name and int ordinal) of an enum, we assign it to be equal to one of the constant values stored in the $VALUES array of the corresponding type. --- .../src/java_bytecode/java_object_factory.cpp | 142 +++++++++++------- 1 file changed, 90 insertions(+), 52 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 564ca42be9b..251348a948d 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -394,65 +394,103 @@ void java_object_factoryt::gen_pointer_target_init( update_in_placet update_in_place, const source_locationt &location) { - PRECONDITION(expr.type().id()==ID_pointer); - PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE); + PRECONDITION(expr.type().id() == ID_pointer); + PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE); - if(target_type.id()==ID_struct && - has_prefix( - id2string(to_struct_type(target_type).get_tag()), - "java::array[")) - { - gen_nondet_array_init( - assignments, expr, depth + 1, update_in_place, location); - } - else + if(target_type.id() == ID_struct) { - // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we - // initialize the fields of the object pointed by `expr`; if in - // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it - // (return value of `allocate_object`), emit a statement of the form - // ` := address-of()` and recursively initialize such new - // object. - exprt target; - if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE) + const auto &target_class_type = to_java_class_type(target_type); + if(has_prefix(id2string(target_class_type.get_tag()), "java::array[")) { - target=allocate_object( - assignments, - expr, - target_type, - alloc_type); - INVARIANT( - target.type().id()==ID_pointer, - "Pointer-typed expression expected"); + gen_nondet_array_init( + assignments, expr, depth + 1, update_in_place, location); + return; } - else + if(target_class_type.get_base("java::java.lang.Enum")) { - target=expr; - } + // We nondet-initialize enums to be equal to one of the constants defined + // for their type: + // int i = nondet(int) + // assume(0 < = i < $VALUES.length) + // expr = $VALUES[i] + // where $VALUES is a variable generated by the Java compiler that stores + // the array that is returned by Enum.values(). + + const irep_idt &class_name = target_class_type.get_name(); + const irep_idt values_name = id2string(class_name) + ".$VALUES"; + INVARIANT( + ns.get_symbol_table().has_symbol(values_name), + "The $VALUES array (populated by clinit_wrapper) should be in the " + "symbol table"); + const symbolt &values = ns.lookup(values_name); + + // Access members (length and data) of $VALUES array + dereference_exprt deref_expr(values.symbol_expr()); + const auto &deref_struct_type = + to_struct_type(ns.follow(deref_expr.type())); + PRECONDITION(is_valid_java_array(deref_struct_type)); + const auto &comps = deref_struct_type.components(); + const member_exprt length_expr(deref_expr, "length", comps[1].type()); + const member_exprt enum_array_expr = + member_exprt(deref_expr, "data", comps[2].type()); + + const symbol_exprt &index_expr = gen_nondet_int_init( + assignments, + "enum_index_init", + from_integer(0, java_int_type()), + minus_exprt(length_expr, from_integer(1, java_int_type())), + location); - // we dereference the pointer and initialize the resulting object using a - // recursive call - exprt init_expr; - if(target.id()==ID_address_of) - init_expr=target.op0(); - else - { - init_expr= - dereference_exprt(target, target.type().subtype()); + // Generate statement using pointer arithmetic to access array element: + // expr = (expr.type())*(enum_array_expr + index_expr); + plus_exprt plus(enum_array_expr, index_expr); + const dereference_exprt arraycellref( + plus, enum_array_expr.type().subtype()); + code_assignt enum_assign(expr, typecast_exprt(arraycellref, expr.type())); + assignments.add(enum_assign); + return; } - gen_nondet_init( - assignments, - init_expr, - false, // is_sub - "", // class_identifier - false, // skip_classid - alloc_type, - false, - typet(), - depth + 1, - update_in_place, - location); } + + // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we + // initialize the fields of the object pointed by `expr`; if in + // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it + // (return value of `allocate_object`), emit a statement of the form + // ` := address-of()` and recursively initialize such new + // object. + exprt target; + if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE) + { + target = allocate_object(assignments, expr, target_type, alloc_type); + INVARIANT( + target.type().id() == ID_pointer, "Pointer-typed expression expected"); + } + else + { + target = expr; + } + + // we dereference the pointer and initialize the resulting object using a + // recursive call + exprt init_expr; + if(target.id() == ID_address_of) + init_expr = target.op0(); + else + { + init_expr = dereference_exprt(target, target.type().subtype()); + } + gen_nondet_init( + assignments, + init_expr, + false, // is_sub + "", // class_identifier + false, // skip_classid + alloc_type, + false, // override + typet(), // override type immaterial + depth + 1, + update_in_place, + location); } /// Recursion-set entry owner class. If a recursion-set entry is added @@ -1258,7 +1296,7 @@ const symbol_exprt java_object_factoryt::gen_nondet_int_init( gen_nondet_init( assignments, int_symbol_expr, - false, // is_sub + false, // is_sub irep_idt(), false, // skip_classid allocation_typet::LOCAL, // immaterial, type is primitive From 5542c54d08404e5d9f54273452895986b213ae7b Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Fri, 10 Aug 2018 18:13:34 +0100 Subject: [PATCH 5/9] Move nondet enum initialization to new function --- .../src/java_bytecode/java_object_factory.cpp | 92 +++++++++++-------- 1 file changed, 52 insertions(+), 40 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 251348a948d..4836734800d 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -107,6 +107,12 @@ class java_object_factoryt update_in_placet, const source_locationt &location); + void gen_nondet_enum_init( + code_blockt &assignments, + const exprt &expr, + const java_class_typet &java_class_type, + const source_locationt &location); + void gen_nondet_init( code_blockt &assignments, const exprt &expr, @@ -408,46 +414,7 @@ void java_object_factoryt::gen_pointer_target_init( } if(target_class_type.get_base("java::java.lang.Enum")) { - // We nondet-initialize enums to be equal to one of the constants defined - // for their type: - // int i = nondet(int) - // assume(0 < = i < $VALUES.length) - // expr = $VALUES[i] - // where $VALUES is a variable generated by the Java compiler that stores - // the array that is returned by Enum.values(). - - const irep_idt &class_name = target_class_type.get_name(); - const irep_idt values_name = id2string(class_name) + ".$VALUES"; - INVARIANT( - ns.get_symbol_table().has_symbol(values_name), - "The $VALUES array (populated by clinit_wrapper) should be in the " - "symbol table"); - const symbolt &values = ns.lookup(values_name); - - // Access members (length and data) of $VALUES array - dereference_exprt deref_expr(values.symbol_expr()); - const auto &deref_struct_type = - to_struct_type(ns.follow(deref_expr.type())); - PRECONDITION(is_valid_java_array(deref_struct_type)); - const auto &comps = deref_struct_type.components(); - const member_exprt length_expr(deref_expr, "length", comps[1].type()); - const member_exprt enum_array_expr = - member_exprt(deref_expr, "data", comps[2].type()); - - const symbol_exprt &index_expr = gen_nondet_int_init( - assignments, - "enum_index_init", - from_integer(0, java_int_type()), - minus_exprt(length_expr, from_integer(1, java_int_type())), - location); - - // Generate statement using pointer arithmetic to access array element: - // expr = (expr.type())*(enum_array_expr + index_expr); - plus_exprt plus(enum_array_expr, index_expr); - const dereference_exprt arraycellref( - plus, enum_array_expr.type().subtype()); - code_assignt enum_assign(expr, typecast_exprt(arraycellref, expr.type())); - assignments.add(enum_assign); + gen_nondet_enum_init(assignments, expr, target_class_type, location); return; } } @@ -1492,6 +1459,51 @@ void java_object_factoryt::gen_nondet_array_init( assignments.move_to_operands(init_done_label); } +/// We nondet-initialize enums to be equal to one of the constants defined +/// for their type: +/// int i = nondet(int); +/// assume(0 < = i < $VALUES.length); +/// expr = $VALUES[i]; +/// where $VALUES is a variable generated by the Java compiler that stores +/// the array that is returned by Enum.values(). +void java_object_factoryt::gen_nondet_enum_init( + code_blockt &assignments, + const exprt &expr, + const java_class_typet &java_class_type, + const source_locationt &location) +{ + const irep_idt &class_name = java_class_type.get_name(); + const irep_idt values_name = id2string(class_name) + ".$VALUES"; + INVARIANT( + ns.get_symbol_table().has_symbol(values_name), + "The $VALUES array (populated by clinit_wrapper) should be in the " + "symbol table"); + const symbolt &values = ns.lookup(values_name); + + // Access members (length and data) of $VALUES array + dereference_exprt deref_expr(values.symbol_expr()); + const auto &deref_struct_type = to_struct_type(ns.follow(deref_expr.type())); + PRECONDITION(is_valid_java_array(deref_struct_type)); + const auto &comps = deref_struct_type.components(); + const member_exprt length_expr(deref_expr, "length", comps[1].type()); + const member_exprt enum_array_expr = + member_exprt(deref_expr, "data", comps[2].type()); + + const symbol_exprt &index_expr = gen_nondet_int_init( + assignments, + "enum_index_init", + from_integer(0, java_int_type()), + minus_exprt(length_expr, from_integer(1, java_int_type())), + location); + + // Generate statement using pointer arithmetic to access array element: + // expr = (expr.type())*(enum_array_expr + index_expr); + plus_exprt plus(enum_array_expr, index_expr); + const dereference_exprt arraycellref(plus); + code_assignt enum_assign(expr, typecast_exprt(arraycellref, expr.type())); + assignments.add(enum_assign); +} + /// Add code_declt instructions to `init_code` for every non-static symbol /// in `symbols_created` /// \param symbols_created: list of symbols From 3e32140d6fda727855de093529abc67e66bbb9b9 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Tue, 31 Jul 2018 17:03:19 +0100 Subject: [PATCH 6/9] CI lazy methods: load clinit for all param types We load static initializers for all types of parameters of the entry function(s). This is necessary for the new nondet-initialization of enums, and also consistent with the Java language specification, which says that static initializers should be run on object initialization. --- jbmc/src/java_bytecode/ci_lazy_methods.cpp | 25 ++++++++++++++++++++++ jbmc/src/java_bytecode/ci_lazy_methods.h | 5 +++++ 2 files changed, 30 insertions(+) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index dd7a161e303..05373710b09 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -382,6 +382,8 @@ void ci_lazy_methodst::initialize_instantiated_classes( if(param.type().id()==ID_pointer) { const pointer_typet &original_pointer=to_pointer_type(param.type()); + add_clinit_call_for_pointer_type( + original_pointer, ns.get_symbol_table(), needed_lazy_methods); needed_lazy_methods.add_all_needed_classes(original_pointer); } } @@ -399,6 +401,29 @@ void ci_lazy_methodst::initialize_instantiated_classes( needed_lazy_methods.add_needed_class("java::" + id2string(id)); } +/// Helper function for `initialize_instantiated_classes`. +/// For a given pointer_typet that is being noted as needed in +/// `needed_lazy_methods`, notes that its static initializer is also needed. +/// This applies the same logic to the class of `pointer_type` that +/// `java_bytecode_convert_methodt::get_clinit_call` applies e.g. to classes +/// whose constructor we call in a method body. This duplication is unavoidable +/// due to the fact that ci_lazy_methods essentially has to go through the same +/// logic as __CPROVER_start in its initial setup. +/// \param pointer_type: The given pointer_typet +/// \param symbol_table: Used to look up occurrences of static initializers +/// \param [out] needed_lazy_methods: Gets notified of any static initializers +/// that need to be loaded +void ci_lazy_methodst::add_clinit_call_for_pointer_type( + const pointer_typet &pointer_type, + const symbol_tablet &symbol_table, + ci_lazy_methods_neededt &needed_lazy_methods) +{ + const irep_idt &pointer_id = + to_symbol_type(pointer_type.subtype()).get_identifier(); + const irep_idt &clinit_wrapper = clinit_wrapper_name(pointer_id); + if(symbol_table.symbols.count(clinit_wrapper)) + needed_lazy_methods.add_needed_method(clinit_wrapper); +} /// Get places where virtual functions are called. /// \param e: expression tree to search diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.h b/jbmc/src/java_bytecode/ci_lazy_methods.h index f90d2186a8e..905258f1c4d 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.h +++ b/jbmc/src/java_bytecode/ci_lazy_methods.h @@ -120,6 +120,11 @@ class ci_lazy_methodst:public messaget const namespacet &ns, ci_lazy_methods_neededt &needed_lazy_methods); + void add_clinit_call_for_pointer_type( + const pointer_typet &pointer_type, + const symbol_tablet &symbol_table, + ci_lazy_methods_neededt &needed_lazy_methods); + void gather_virtual_callsites( const exprt &e, std::unordered_set &result); From 03e3877830ba5acef5e8e07d46ebd39ef171108b Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Thu, 9 Aug 2018 15:14:29 +0100 Subject: [PATCH 7/9] Add tests for nondet initialization of enums The tests check that for a nondeterministic non-null enum, any of the constants of its type can be chosen, and nothing other than these constants. --- .../regression/jbmc/NondetEnumArg/Color.class | Bin 0 -> 800 bytes jbmc/regression/jbmc/NondetEnumArg/Color.java | 5 ++ .../jbmc/NondetEnumArg/NondetEnumArg.class | Bin 0 -> 1549 bytes .../jbmc/NondetEnumArg/NondetEnumArg.java | 46 ++++++++++++++++++ .../NondetEnumArg/test_some_constant.desc | 10 ++++ .../test_specific_constant1.desc | 7 +++ .../test_specific_constant2.desc | 7 +++ .../test_specific_constant3.desc | 7 +++ 8 files changed, 82 insertions(+) create mode 100644 jbmc/regression/jbmc/NondetEnumArg/Color.class create mode 100644 jbmc/regression/jbmc/NondetEnumArg/Color.java create mode 100644 jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.class create mode 100644 jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.java create mode 100644 jbmc/regression/jbmc/NondetEnumArg/test_some_constant.desc create mode 100644 jbmc/regression/jbmc/NondetEnumArg/test_specific_constant1.desc create mode 100644 jbmc/regression/jbmc/NondetEnumArg/test_specific_constant2.desc create mode 100644 jbmc/regression/jbmc/NondetEnumArg/test_specific_constant3.desc diff --git a/jbmc/regression/jbmc/NondetEnumArg/Color.class b/jbmc/regression/jbmc/NondetEnumArg/Color.class new file mode 100644 index 0000000000000000000000000000000000000000..5fc329a12dd4d7c143e62f9e22715f6818584af6 GIT binary patch literal 800 zcmZuu?@!ZE6g{u)*6z{$piXoHMG>VP$~2KrTL?I-F z+w+rjB7Zb$&B3M{_?NY{`+}aQL~pC@)`S9pJc*E=bO4pQ5H1iX;5L@PaEGEb^5WwY zuy0Ty80Ba$Sk+C#&_f{pxwkPVi8az|0-1a0ll%ga*q7h8|3#W zqu@RatdhMF6_7~r?frz-vvlNMehu3 a*3OcY3W}trPUj73rQoXh13Z)>*8T#fV2(2Y literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/NondetEnumArg/Color.java b/jbmc/regression/jbmc/NondetEnumArg/Color.java new file mode 100644 index 00000000000..0fd41d395d0 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumArg/Color.java @@ -0,0 +1,5 @@ +public enum Color { + RED, + GREEN, + BLUE +} diff --git a/jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.class b/jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.class new file mode 100644 index 0000000000000000000000000000000000000000..b4af0ffd3c87f4084703fcbce6eb51f1d534b123 GIT binary patch literal 1549 zcmb`GTTj$L9L3M=--e2lcy7@Q7{A{<$irVyQ}ZRS6i&bpgZkD~@YdnM_=yP-UnBJr!AZ zd|8RCGlZbQ4_tbm`@!PA0Yqn?Y8FQ+2-Q2@yZM&kQ}C(hHzD3BA@(;#YTSYY=;2dI ze;@&k&-MIQXz$)5v4#!~TR$OrZxh;={08){)CP=~IH<-ONT=4(&SA?M4DB_vdx|l#K#~Lr4R|>r_ zxE<1%qOTH6JmB}|Y|sm|;T7A|OLZ?=^nHis#CME|_};Ht(HFJiEej+mei*hQb@Oi=?BmD8dz^5?~owl>#S!04-)&| Date: Mon, 13 Aug 2018 17:40:54 +0100 Subject: [PATCH 8/9] Temporarily remove new UNREACHABLE statements These really should be unreachable, but some company code needs to be changed for this first. A ticket number has been added as a reminder. --- src/goto-symex/symex_builtin_functions.cpp | 3 ++- src/goto-symex/symex_catch.cpp | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 07104728643..f23726cd88a 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -505,7 +505,8 @@ void goto_symext::symex_fkt( statet &, const code_function_callt &) { - UNREACHABLE; + // TODO: uncomment this line when TG-4667 is done + // UNREACHABLE; #if 0 exprt new_fc(ID_function, fc.type()); diff --git a/src/goto-symex/symex_catch.cpp b/src/goto-symex/symex_catch.cpp index a5440bb3c90..33b0317f61e 100644 --- a/src/goto-symex/symex_catch.cpp +++ b/src/goto-symex/symex_catch.cpp @@ -13,7 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com void goto_symext::symex_catch(statet &) { - UNREACHABLE; + // TODO: uncomment this line when TG-4667 is done + // UNREACHABLE; // there are two variants: 'push' and 'pop' #if 0 From 5ca6cd2e3a754b8bc4c7c205825a5d2fabec018a Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Tue, 14 Aug 2018 11:50:30 +0100 Subject: [PATCH 9/9] 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. --- jbmc/src/java_bytecode/ci_lazy_methods.cpp | 14 ++++++++--- .../src/java_bytecode/java_object_factory.cpp | 25 +++++++++++++------ 2 files changed, 29 insertions(+), 10 deletions(-) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 05373710b09..414b2a51ad0 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -381,9 +381,17 @@ void ci_lazy_methodst::initialize_instantiated_classes( { if(param.type().id()==ID_pointer) { - const pointer_typet &original_pointer=to_pointer_type(param.type()); - add_clinit_call_for_pointer_type( - original_pointer, ns.get_symbol_table(), needed_lazy_methods); + const pointer_typet &original_pointer = to_pointer_type(param.type()); + const auto &original_type = ns.follow(original_pointer.subtype()); + // Special case for enums. We may want to generalise this, see TG-4689 + // and the comment in java_object_factoryt::gen_nondet_pointer_init. + if( + can_cast_type(original_type) && + to_java_class_type(original_type).get_base("java::java.lang.Enum")) + { + add_clinit_call_for_pointer_type( + original_pointer, ns.get_symbol_table(), needed_lazy_methods); + } needed_lazy_methods.add_all_needed_classes(original_pointer); } } diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 4836734800d..e29b5d5832c 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -785,18 +785,29 @@ void java_object_factoryt::gen_nondet_pointer_init( // (This can currently happen for some cases of #exception_value) bool must_be_null = subtype == empty_typet(); - // If we may be about to initialize a non-null object, always run the + // If we may be about to initialize a non-null enum type, always run the // clinit_wrapper of its class first. + // TODO: TG-4689 we may want to do this for all types, not just enums, as + // described in the Java language specification: + // https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.7 + // https://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4.1 + // But we would have to put this behavior behind an option as it would have an + // impact on running times. // Note that it would be more consistent with the behaviour of the JVM to only // run clinit_wrapper if we are about to initialize an object of which we know // for sure that it is not null on any following branch. However, adding this - // case in gen_nondet_struct_init would slow symex down too much. - if(!must_be_null) + // case in gen_nondet_struct_init would slow symex down too much, so if we + // decide to do this for all types, we should do it here. + // Note also that this logic is mirrored in + // ci_lazy_methodst::initialize_instantiated_classes. + if(const auto class_type = type_try_dynamic_cast(subtype)) { - const java_class_typet &class_type = to_java_class_type(subtype); - const irep_idt &class_name = class_type.get_name(); - const irep_idt class_clinit = clinit_wrapper_name(class_name); - gen_method_call_if_present(assignments, expr, class_clinit); + if(class_type->get_base("java::java.lang.Enum") && !must_be_null) + { + const irep_idt &class_name = class_type->get_name(); + const irep_idt class_clinit = clinit_wrapper_name(class_name); + gen_method_call_if_present(assignments, expr, class_clinit); + } } code_blockt new_object_assignments;