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() functio 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_bytecode_language.h

@@ -59,13 +59,50 @@ 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_EXTERNAL_DRIVER
+  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;
 };
 
 class java_bytecode_languaget:public languaget

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,8 +205,9 @@ 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
@@ -212,9 +216,8 @@ exprt::operandst java_build_arguments(
         p.type(),
         base_name,
         init_code,
-        allow_null,
         symbol_table,
-        object_factory_parameters,
+        parameters,
         allocation_typet::LOCAL,
         function.location,
         pointer_type_selector);

src/java_bytecode/java_object_factory.cpp

@@ -144,7 +144,6 @@ class java_object_factoryt
     allocation_typet alloc_type,
     bool override_,
     const typet &override_type,
-    bool allow_null,
     size_t depth,
     update_in_placet);
 
@@ -155,7 +154,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);
 
@@ -452,7 +450,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);
   }
@@ -727,11 +724,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.
@@ -748,7 +740,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)
 {
@@ -870,7 +861,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)
@@ -970,7 +963,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);
 
@@ -1079,7 +1071,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);
     }
@@ -1129,9 +1120,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.
@@ -1151,7 +1139,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)
 {
@@ -1178,7 +1165,6 @@ void java_object_factoryt::gen_nondet_init(
       class_identifier,
       alloc_type,
       pointer_type,
-      allow_null,
       depth,
       update_in_place);
   }
@@ -1262,8 +1248,7 @@ void java_object_factoryt::allocate_nondet_length_array(
     allocation_typet::LOCAL, // immaterial, type is primitive
     false,   // override
     typet(), // override type is immaterial
-    false,   // allow_null
-    0,       // depth is immaterial
+    0,       // depth is immaterial, always non-null
     update_in_placet::NO_UPDATE_IN_PLACE);
 
   // Insert assumptions to bound its length:
@@ -1410,7 +1395,6 @@ void java_object_factoryt::gen_nondet_array_init(
     allocation_typet::DYNAMIC,
     true,  // override
     element_type,
-    true,  // allow_null
     depth,
     child_update_in_place);
 
@@ -1460,7 +1444,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,
@@ -1502,8 +1485,7 @@ exprt object_factory(
     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);
@@ -1534,13 +1516,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:
@@ -1561,7 +1536,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)
@@ -1584,8 +1558,7 @@ void gen_nondet_init(
     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);
@@ -1598,7 +1571,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,
@@ -1609,7 +1581,6 @@ exprt object_factory(
     type,
     base_name,
     init_code,
-    allow_null,
     symbol_table,
     object_factory_parameters,
     alloc_type,
@@ -1625,7 +1596,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)
 {
@@ -1637,7 +1607,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);