fixcompilation

Author: peterschrammel

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -93,7 +93,6 @@ static goto_programt::targett insert_nondet_init_code(
     source_loc,
     true,
     allocation_typet::DYNAMIC,
-    nullable,
     object_factory_parameters,
     update_in_placet::NO_UPDATE_IN_PLACE);
 

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -59,50 +59,13 @@ Author: Daniel Kroening, [email protected]
   "                                  the purpose of lazy method loading\n"                       /* NOLINT(*) */ \
   "                                  A '.*' wildcard is allowed to specify all class members\n"
 
-#define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
-#define MAX_NONDET_STRING_LENGTH std::numeric_limits<std::int32_t>::max()
-#define MAX_NONDET_TREE_DEPTH 5
-#define MAX_NONNULL_TREE_DEPTH 0
-
 class symbolt;
 
 enum lazy_methods_modet
 {
   LAZY_METHODS_MODE_EAGER,
   LAZY_METHODS_MODE_CONTEXT_INSENSITIVE,
-  LAZY_METHODS_MODE_CONTEXT_SENSITIVE
-};
-
-struct object_factory_parameterst final
-{
-  /// Maximum value for the non-deterministically-chosen length of an array.
-  size_t max_nondet_array_length=MAX_NONDET_ARRAY_LENGTH_DEFAULT;
-
-  /// Maximum value for the non-deterministically-chosen length of a string.
-  size_t max_nondet_string_length=MAX_NONDET_STRING_LENGTH;
-
-  /// Maximum depth for object hierarchy on input.
-  /// Used to prevent object factory to loop infinitely during the
-  /// generation of code that allocates/initializes data structures of recursive
-  /// data types or unbounded depth. We bound the maximum number of times we
-  /// dereference a pointer using a 'depth counter'. We set a pointer to null if
-  /// such depth becomes >= than this maximum value.
-  size_t max_nondet_tree_depth=MAX_NONDET_TREE_DEPTH;
-
-  /// To force a certain depth of non-null objects.
-  /// The default is that objects are 'maybe null' up to the nondet tree depth.
-  /// Examples:
-  /// * max_nondet_tree_depth=0, max_nonnull_tree_depth irrelevant
-  ///   pointer initialized to null
-  /// * max_nondet_tree_depth=n, max_nonnull_tree_depth=0
-  ///   pointer and children up to depth n maybe-null, beyond n null
-  /// * max_nondet_tree_depth=n >=m, max_nonnull_tree_depth=m
-  ///   pointer and children up to depth m initialized to non-null,
-  ///   children up to n maybe-null, beyond n null
-  size_t max_nonnull_tree_depth=MAX_NONNULL_TREE_DEPTH;
-
-  /// Force string content to be ASCII printable characters when set to true.
-  bool string_printable = false;
+  LAZY_METHODS_MODE_EXTERNAL_DRIVER
 };
 
 class java_bytecode_languaget:public languaget

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -192,7 +192,6 @@ exprt::operandst java_build_arguments(
     if(is_main)
       parameters.max_nonnull_tree_depth = 2;
 
-    object_factory_parameterst parameters = object_factory_parameters;
     parameters.function_id = goto_functionst::entry_point();
 
     // generate code to allocate and non-deterministicaly initialize the

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -833,11 +833,9 @@ void java_object_factoryt::gen_nondet_pointer_init(
   // and asign to `expr` the address of such object
   code_blockt non_null_inst;
 
-  bool string_init_failed = false;
   // Note string-type-specific initialization might fail, e.g. if java.lang.CharSequence does not
   // have the expected fields (typically this happens if --refine-strings was not passed). In this
   // case we fall back to normal pointer target init.
-
   bool string_init_succeeded = false;
 
   if(java_string_library_preprocesst::implements_java_char_sequence_pointer(
@@ -869,10 +867,6 @@ void java_object_factoryt::gen_nondet_pointer_init(
 
   bool allow_null = depth > object_factory_parameters.max_nonnull_tree_depth;
 
-  // Determine whether the pointer can be null. In particular the pointers
-  // inside the java.lang.Class class shall not be null
-  const bool not_null = allow_nul || class_identifier == "java.lang.Class";
-
   // Alternatively, if this is a void* we *must* initialise with null:
   // (This can currently happen for some cases of #exception_value)
   // Also, if the String model is not loaded then we can only

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -786,14 +786,19 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body(
   {
     const symbol_exprt new_global_symbol =
       symbol_table.lookup_ref(it->second).symbol_expr();
+
+    parameters.max_nonnull_tree_depth =
+      is_non_null_library_global(it->second) ?
+      object_factory_parameters.max_nonnull_tree_depth + 1 :
+      object_factory_parameters.max_nonnull_tree_depth;
+
     gen_nondet_init(
       new_global_symbol,
       static_init_body,
       symbol_table,
       source_locationt(),
       false,
       allocation_typet::DYNAMIC,
-      !is_non_null_library_global(it->second),
       parameters,
       pointer_type_selector,
       update_in_placet::NO_UPDATE_IN_PLACE);

jbmc/src/java_bytecode/object_factory_parameters.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
 #define MAX_NONDET_STRING_LENGTH std::numeric_limits<std::int32_t>::max()
 #define MAX_NONDET_TREE_DEPTH 5
+#define MAX_NONNULL_TREE_DEPTH 0
 
 struct object_factory_parameterst final
 {
@@ -34,6 +35,18 @@ struct object_factory_parameterst final
   /// such depth becomes >= than this maximum value.
   size_t max_nondet_tree_depth=MAX_NONDET_TREE_DEPTH;
 
+  /// To force a certain depth of non-null objects.
+  /// The default is that objects are 'maybe null' up to the nondet tree depth.
+  /// Examples:
+  /// * max_nondet_tree_depth=0, max_nonnull_tree_depth irrelevant
+  ///   pointer initialized to null
+  /// * max_nondet_tree_depth=n, max_nonnull_tree_depth=0
+  ///   pointer and children up to depth n maybe-null, beyond n null
+  /// * max_nondet_tree_depth=n >=m, max_nonnull_tree_depth=m
+  ///   pointer and children up to depth m initialized to non-null,
+  ///   children up to n maybe-null, beyond n null
+  size_t max_nonnull_tree_depth=MAX_NONNULL_TREE_DEPTH;
+
   /// Force string content to be ASCII printable characters when set to true.
   bool string_printable = false;
 

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -106,6 +106,10 @@ void java_simple_method_stubst::create_method_stub_at(
   if(is_constructor)
     to_init = dereference_exprt(to_init, expected_base);
 
+  object_factory_parameterst parameters = object_factory_parameters;
+  if(assume_non_null)
+    parameters.max_nonnull_tree_depth++;
+
   // Generate new instructions.
   code_blockt new_instructions;
   gen_nondet_init(
@@ -115,8 +119,7 @@ void java_simple_method_stubst::create_method_stub_at(
     loc,
     is_constructor,
     allocation_typet::DYNAMIC,
-    !assume_non_null,
-    object_factory_parameters,
+    parameters,
     update_in_place ? update_in_placet::MUST_UPDATE_IN_PLACE
                     : update_in_placet::NO_UPDATE_IN_PLACE);
 
@@ -189,15 +192,18 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
       const exprt &to_return = to_return_symbol.symbol_expr();
       if(to_return_symbol.type.id() != ID_pointer)
       {
+        object_factory_parameterst parameters = object_factory_parameters;
+        if(assume_non_null)
+          parameters.max_nonnull_tree_depth++;
+
         gen_nondet_init(
           to_return,
           new_instructions,
           symbol_table,
           source_locationt(),
           false,
           allocation_typet::LOCAL, // Irrelevant as type is primitive
-          !assume_non_null,
-          object_factory_parameters,
+          parameters,
           update_in_placet::NO_UPDATE_IN_PLACE);
       }
       else