Generalize allow_null to max_nonnull_tree_depth

allow_null only considered the immediate pointer,
but did not allow forcing sub-objects to be
non-null. This is required for example to
ensure the array elements of the argument to
the main() function to be non-null.
The depth argument starts from 1 now to allow
the immediate pointer to be maybe null when
max_nonnull_tree_depth is 0.

Author: peterschrammel

src/goto-programs/convert_nondet.cpp

@@ -34,7 +34,7 @@ static goto_programt::targett insert_nondet_init_code(
   const goto_programt::targett &target,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters)
+  object_factory_parameterst object_factory_parameters)
 {
   // Return if the instruction isn't an assignment
   const auto next_instr=std::next(target);
@@ -73,7 +73,8 @@ static goto_programt::targett insert_nondet_init_code(
   }
 
   // Check whether the nondet object may be null
-  const auto nullable=to_side_effect_expr_nondet(side_effect).get_nullable();
+  if(!to_side_effect_expr_nondet(side_effect).get_nullable())
+    object_factory_parameters.max_nonnull_tree_depth = 1;
   // Get the symbol to nondet-init
   const auto source_loc=target->source_location;
 
@@ -89,7 +90,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);
 

src/java_bytecode/java_entry_point.cpp

@@ -120,15 +120,18 @@ static void java_static_lifetime_init(
           if(allow_null && is_non_null_library_global(nameid))
             allow_null = false;
         }
+        object_factory_parameterst parameters = object_factory_parameters;
+        if(!allow_null)
+          parameters.max_nonnull_tree_depth = 1;
+
         gen_nondet_init(
           sym.symbol_expr(),
           code_block,
           symbol_table,
           source_location,
           false,
           allocation_typet::GLOBAL,
-          allow_null,
-          object_factory_parameters,
+          parameters,
           pointer_type_selector,
           update_in_placet::NO_UPDATE_IN_PLACE);
       }
@@ -202,22 +205,21 @@ exprt::operandst java_build_arguments(
     // be null
     bool is_this=(param_number==0) && parameters[param_number].get_this();
 
-    bool allow_null=
-      !assume_init_pointers_not_null && !is_main && !is_this;
+    object_factory_parameterst parameters = object_factory_parameters;
+    if(assume_init_pointers_not_null || is_main || is_this)
+      parameters.max_nonnull_tree_depth = 1;
 
     // generate code to allocate and non-deterministicaly initialize the
     // argument
-    main_arguments[param_number]=
-      object_factory(
-        p.type(),
-        base_name,
-        init_code,
-        allow_null,
-        symbol_table,
-        object_factory_parameters,
-        allocation_typet::LOCAL,
-        function.location,
-        pointer_type_selector);
+    main_arguments[param_number] = object_factory(
+      p.type(),
+      base_name,
+      init_code,
+      symbol_table,
+      parameters,
+      allocation_typet::LOCAL,
+      function.location,
+      pointer_type_selector);
 
     // record as an input
     codet input(ID_input);

src/java_bytecode/java_object_factory.cpp

@@ -133,7 +133,6 @@ class java_object_factoryt
     allocation_typet alloc_type,
     bool override_,
     const typet &override_type,
-    bool allow_null,
     size_t depth,
     update_in_placet);
 
@@ -144,7 +143,6 @@ class java_object_factoryt
     const irep_idt &class_identifier,
     allocation_typet alloc_type,
     const pointer_typet &pointer_type,
-    bool allow_null,
     size_t depth,
     const update_in_placet &update_in_place);
 
@@ -441,7 +439,6 @@ void java_object_factoryt::gen_pointer_target_init(
       alloc_type,
       false,   // override
       typet(), // override type immaterial
-      true,    // allow_null always enabled in sub-objects
       depth+1,
       update_in_place);
   }
@@ -716,11 +713,6 @@ static bool add_nondet_string_pointer_initialization(
 ///   others.
 /// \param alloc_type:
 ///   Allocation type (global, local or dynamic)
-/// \param allow_null:
-///   true iff the the non-det initialization code is allowed to set null as a
-///   value to the pointer \p expr; note that the current value of allow_null is
-///   _not_ inherited by subsequent recursive calls; those will always be
-///   authorized to assign null to a pointer
 /// \param depth:
 ///   Number of times that a pointer has been dereferenced from the root of the
 ///   object tree that we are initializing.
@@ -737,7 +729,6 @@ void java_object_factoryt::gen_nondet_pointer_init(
   const irep_idt &class_identifier,
   allocation_typet alloc_type,
   const pointer_typet &pointer_type,
-  bool allow_null,
   size_t depth,
   const update_in_placet &update_in_place)
 {
@@ -858,7 +849,9 @@ void java_object_factoryt::gen_nondet_pointer_init(
 
   // 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_null || class_identifier == "java.lang.Class";
+  const bool not_null =
+    depth <= object_factory_parameters.max_nonnull_tree_depth ||
+    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)
@@ -958,7 +951,6 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
     alloc_type,
     false,   // override
     typet(), // override_type
-    true,    // allow_null
     depth,
     update_in_placet::NO_UPDATE_IN_PLACE);
 
@@ -1067,7 +1059,6 @@ void java_object_factoryt::gen_nondet_struct_init(
         alloc_type,
         false,   // override
         typet(), // override_type
-        true,    // allow_null always true for sub-objects
         depth,
         substruct_in_place);
     }
@@ -1117,9 +1108,6 @@ void java_object_factoryt::gen_nondet_struct_init(
 ///   If true, initialize with `override_type` instead of `expr.type()`. Used at
 ///   the moment for reference arrays, which are implemented as void* arrays but
 ///   should be init'd as their true type with appropriate casts.
-/// \param allow_null:
-///   True iff the the non-det initialization code is allowed to set null as a
-///   value to a pointer.
 /// \param depth:
 ///   Number of times that a pointer has been dereferenced from the root of the
 ///   object tree that we are initializing.
@@ -1139,7 +1127,6 @@ void java_object_factoryt::gen_nondet_init(
   allocation_typet alloc_type,
   bool override_,
   const typet &override_type,
-  bool allow_null,
   size_t depth,
   update_in_placet update_in_place)
 {
@@ -1157,7 +1144,6 @@ void java_object_factoryt::gen_nondet_init(
       class_identifier,
       alloc_type,
       pointer_type,
-      allow_null,
       depth,
       update_in_place);
   }
@@ -1220,14 +1206,13 @@ void java_object_factoryt::allocate_nondet_length_array(
   gen_nondet_init(
     assignments,
     length_sym_expr,
-    false,   // is_sub
+    false, // is_sub
     irep_idt(),
-    false,   // skip_classid
+    false,                   // skip_classid
     allocation_typet::LOCAL, // immaterial, type is primitive
-    false,   // override
-    typet(), // override type is immaterial
-    false,   // allow_null
-    0,       // depth is immaterial
+    false,                   // override
+    typet(),                 // override type is immaterial
+    0,                       // depth is immaterial, always non-null
     update_in_placet::NO_UPDATE_IN_PLACE);
 
   // Insert assumptions to bound its length:
@@ -1374,7 +1359,6 @@ void java_object_factoryt::gen_nondet_array_init(
     allocation_typet::DYNAMIC,
     true,  // override
     element_type,
-    true,  // allow_null
     depth,
     child_update_in_place);
 
@@ -1424,7 +1408,6 @@ exprt object_factory(
   const typet &type,
   const irep_idt base_name,
   code_blockt &init_code,
-  bool allow_null,
   symbol_table_baset &symbol_table,
   const object_factory_parameterst &parameters,
   allocation_typet alloc_type,
@@ -1460,14 +1443,13 @@ exprt object_factory(
   state.gen_nondet_init(
     assignments,
     object,
-    false,   // is_sub
-    "",      // class_identifier
-    false,   // skip_classid
+    false, // is_sub
+    "",    // class_identifier
+    false, // skip_classid
     alloc_type,
     false,   // override
     typet(), // override_type is immaterial
-    allow_null,
-    0,       // initial depth
+    1,       // initial depth
     update_in_placet::NO_UPDATE_IN_PLACE);
 
   declare_created_symbols(symbols_created, loc, init_code);
@@ -1498,13 +1480,6 @@ exprt object_factory(
 /// \param alloc_type:
 ///   Allocate new objects as global objects (GLOBAL) or as local variables
 ///   (LOCAL) or using malloc (DYNAMIC).
-/// \param allow_null:
-///   When \p expr is a pointer, the non-det initializing code will
-///   unconditionally set \p expr to a non-null object iff \p allow_null is
-///   true. Note that other references down the object hierarchy *can* be null
-///   when \p allow_null is false (as this parameter is not inherited by
-///   subsequent recursive calls).  Has no effect when \p expr is not
-///   pointer-typed.
 /// \param object_factory_parameters:
 ///   Parameters for the generation of non deterministic objects.
 /// \param pointer_type_selector:
@@ -1525,7 +1500,6 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  bool allow_null,
   const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   update_in_placet update_in_place)
@@ -1542,14 +1516,13 @@ void gen_nondet_init(
   state.gen_nondet_init(
     assignments,
     expr,
-    false,   // is_sub
-    "",      // class_identifier
+    false, // is_sub
+    "",    // class_identifier
     skip_classid,
     alloc_type,
     false,   // override
     typet(), // override_type is immaterial
-    allow_null,
-    0,       // initial depth
+    1,       // initial depth
     update_in_place);
 
   declare_created_symbols(symbols_created, loc, init_code);
@@ -1562,7 +1535,6 @@ exprt object_factory(
   const typet &type,
   const irep_idt base_name,
   code_blockt &init_code,
-  bool allow_null,
   symbol_tablet &symbol_table,
   const object_factory_parameterst &object_factory_parameters,
   allocation_typet alloc_type,
@@ -1573,7 +1545,6 @@ exprt object_factory(
     type,
     base_name,
     init_code,
-    allow_null,
     symbol_table,
     object_factory_parameters,
     alloc_type,
@@ -1589,7 +1560,6 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  bool allow_null,
   const object_factory_parameterst &object_factory_parameters,
   update_in_placet update_in_place)
 {
@@ -1601,7 +1571,6 @@ void gen_nondet_init(
     loc,
     skip_classid,
     alloc_type,
-    allow_null,
     object_factory_parameters,
     pointer_type_selector,
     update_in_place);

src/java_bytecode/java_object_factory.h

@@ -90,7 +90,6 @@ exprt object_factory(
   const typet &type,
   const irep_idt base_name,
   code_blockt &init_code,
-  bool allow_null,
   symbol_table_baset &symbol_table,
   const object_factory_parameterst &parameters,
   allocation_typet alloc_type,
@@ -101,7 +100,6 @@ exprt object_factory(
   const typet &type,
   const irep_idt base_name,
   code_blockt &init_code,
-  bool allow_null,
   symbol_tablet &symbol_table,
   const object_factory_parameterst &object_factory_parameters,
   allocation_typet alloc_type,
@@ -121,7 +119,6 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  bool allow_null,
   const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   update_in_placet update_in_place);
@@ -133,7 +130,6 @@ void gen_nondet_init(
   const source_locationt &loc,
   bool skip_classid,
   allocation_typet alloc_type,
-  bool allow_null,
   const object_factory_parameterst &object_factory_parameters,
   update_in_placet update_in_place);
 

src/java_bytecode/java_static_initializers.cpp

@@ -373,15 +373,17 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body(
   {
     const symbol_exprt new_global_symbol =
       symbol_table.lookup_ref(it->second).symbol_expr();
+    object_factory_parameterst parameters = object_factory_parameters;
+    if(is_non_null_library_global(it->second))
+      parameters.max_nonnull_tree_depth = 1;
     gen_nondet_init(
       new_global_symbol,
       static_init_body,
       symbol_table,
       source_locationt(),
       false,
       allocation_typet::DYNAMIC,
-      !is_non_null_library_global(it->second),
-      object_factory_parameters,
+      parameters,
       pointer_type_selector,
       update_in_placet::NO_UPDATE_IN_PLACE);
   }

src/java_bytecode/object_factory_parameters.h

@@ -15,6 +15,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
 {
@@ -32,6 +33,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;
 };