add parameter for depth of recursive objects

The original implementation could enter an infinite loop for recursive objects,
this patch adds a maximal recursion depth to prevent this and at the same time
to allow for having non-null object members.

Author: Matthias Güdemann

src/cbmc/cbmc_parse_options.cpp

@@ -1156,6 +1156,8 @@ void cbmc_parse_optionst::help()
     " --classpath dir/jar          set the classpath\n"
     " --main-class class-name      set the name of the main class\n"
     // NOLINTNEXTLINE(whitespace/line_length)
+    "--java-max-recursion-depth    max recursion depth for nondet init of recursive objects\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
     " --java-max-vla-length        limit the length of user-code-created arrays\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --java-cp-include-files      regexp or JSON list of files to load (with '@' prefix)\n"

src/cbmc/cbmc_parse_options.h

@@ -56,6 +56,7 @@ class optionst;
   "(graphml-witness):" \
   "(java-max-vla-length):(java-unwind-enum-static)" \
   "(java-cp-include-files):" \
+  "(java-max-recursion-depth):" \
   "(localize-faults)(localize-faults-method):" \
   "(lazy-methods)" \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)

src/java_bytecode/java_bytecode_language.cpp

@@ -48,6 +48,9 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   if(cmd.isset("java-max-input-array-length"))
     max_nondet_array_length=
       std::stoi(cmd.get_value("java-max-input-array-length"));
+  if(cmd.isset("java-max-recursion-depth"))
+    max_recursion_depth=
+      std::stoi(cmd.get_value("java-max-recursion-depth"));
   if(cmd.isset("java-max-vla-length"))
     max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length"));
   if(cmd.isset("lazy-methods-context-sensitive"))
@@ -791,7 +794,8 @@ bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
       main_class,
       get_message_handler(),
       assume_inputs_non_null,
-      max_nondet_array_length));
+      max_nondet_array_length,
+      max_recursion_depth));
 }
 
 /*******************************************************************\

src/java_bytecode/java_bytecode_language.h

@@ -56,7 +56,8 @@ class java_bytecode_languaget:public languaget
   virtual ~java_bytecode_languaget();
   java_bytecode_languaget():
     max_nondet_array_length(MAX_NONDET_ARRAY_LENGTH_DEFAULT),
-    max_user_array_length(0)
+    max_user_array_length(0),
+    max_recursion_depth(0)
     {}
 
   bool from_expr(
@@ -106,6 +107,7 @@ class java_bytecode_languaget:public languaget
   lazy_methods_modet lazy_methods_mode;
   bool string_refinement_enabled;
   std::string java_cp_include_files;
+  size_t max_recursion_depth;       // maximal depth for recursive objects
 };
 
 languaget *new_java_bytecode_language();

src/java_bytecode/java_entry_point.cpp

@@ -102,7 +102,8 @@ bool java_static_lifetime_init(
   const source_locationt &source_location,
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
-  unsigned max_nondet_array_length)
+  size_t max_nondet_array_length,
+  size_t max_recursive_depth)
 {
   symbolt &initialize_symbol=symbol_table.lookup(INITIALIZE);
   code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
@@ -141,6 +142,7 @@ bool java_static_lifetime_init(
           allow_null,
           symbol_table,
           max_nondet_array_length,
+          max_recursive_depth,
           source_location,
           message_handler);
         code_assignt assignment(sym.symbol_expr(), newsym);
@@ -194,7 +196,8 @@ exprt::operandst java_build_arguments(
   code_blockt &init_code,
   symbol_tablet &symbol_table,
   bool assume_init_pointers_not_null,
-  unsigned max_nondet_array_length,
+  size_t max_nondet_array_length,
+  size_t max_recursive_depth,
   message_handlert &message_handler)
 {
   const code_typet::parameterst &parameters=
@@ -233,6 +236,7 @@ exprt::operandst java_build_arguments(
         allow_null,
         symbol_table,
         max_nondet_array_length,
+        max_recursive_depth,
         function.location,
         message_handler);
 
@@ -517,7 +521,8 @@ bool java_entry_point(
   const irep_idt &main_class,
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
-  size_t max_nondet_array_length)
+  size_t max_nondet_array_length,
+  size_t max_recursive_depth)
 {
   // check if the entry point is already there
   if(symbol_table.symbols.find(goto_functionst::entry_point())!=
@@ -541,7 +546,8 @@ bool java_entry_point(
        symbol.location,
        message_handler,
        assume_init_pointers_not_null,
-       max_nondet_array_length))
+       max_nondet_array_length,
+       max_recursive_depth))
     return true;
 
   code_blockt init_code;
@@ -598,6 +604,7 @@ bool java_entry_point(
       symbol_table,
       assume_init_pointers_not_null,
       max_nondet_array_length,
+      max_recursive_depth,
       message_handler);
   call_main.arguments()=main_arguments;
 

src/java_bytecode/java_entry_point.h

@@ -16,7 +16,8 @@ bool java_entry_point(
   const irep_idt &main_class,
   class message_handlert &message_handler,
   bool assume_init_pointers_not_null,
-  size_t max_nondet_array_length);
+  size_t max_nondet_array_length,
+  size_t max_recursive_depth);
 
 typedef struct
 {

src/java_bytecode/java_object_factory.cpp

@@ -42,6 +42,8 @@ class java_object_factoryt:public messaget
   std::set<irep_idt> recursion_set;
   bool assume_non_null;
   size_t max_nondet_array_length;
+  size_t recursion_depth;
+  size_t max_recursion_depth;
   symbol_tablet &symbol_table;
   message_handlert &message_handler;
   namespacet ns;
@@ -51,11 +53,14 @@ class java_object_factoryt:public messaget
     code_blockt &_init_code,
     bool _assume_non_null,
     size_t _max_nondet_array_length,
+    size_t _max_recursion_depth,
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler):
     init_code(_init_code),
     assume_non_null(_assume_non_null),
     max_nondet_array_length(_max_nondet_array_length),
+    recursion_depth(0),
+    max_recursion_depth(_max_recursion_depth),
     symbol_table(_symbol_table),
     message_handler(_message_handler),
     ns(_symbol_table)
@@ -189,20 +194,23 @@ void java_object_factoryt::gen_nondet_init(
     {
       const struct_typet &struct_type=to_struct_type(subtype);
       const irep_idt struct_tag=struct_type.get_tag();
-      // set to null if found in recursion set and not a sub-type
-      if(recursion_set.find(struct_tag)!=recursion_set.end() &&
-         struct_tag==class_identifier)
+      // set to null if found in recursion set and recursion depth allows it
+      if(recursion_set.find(struct_tag)!=recursion_set.end())
       {
-        // make null
-        null_pointer_exprt null_pointer_expr(pointer_type);
-        code_assignt code(expr, null_pointer_expr);
-        code.add_source_location()=loc;
-        init_code.copy_to_operands(code);
-
-        return;
+        if(recursion_depth<max_recursion_depth)
+          recursion_depth++;
+        else
+        {
+          recursion_depth=0;
+          // make null
+          null_pointer_exprt null_pointer_expr(pointer_type);
+          code_assignt code(expr, null_pointer_expr);
+          code.add_source_location()=loc;
+          init_code.copy_to_operands(code);
+          return;
+        }
       }
     }
-
     code_labelt set_null_label;
     code_labelt init_done_label;
 
@@ -483,12 +491,14 @@ void gen_nondet_init(
   bool create_dyn_objs,
   bool assume_non_null,
   message_handlert &message_handler,
-  size_t max_nondet_array_length)
+  size_t max_nondet_array_length,
+  size_t max_recursion_depth)
 {
   java_object_factoryt state(
     init_code,
     assume_non_null,
     max_nondet_array_length,
+    max_recursion_depth,
     symbol_table,
     message_handler);
   state.gen_nondet_init(
@@ -567,6 +577,7 @@ exprt object_factory(
   bool allow_null,
   symbol_tablet &symbol_table,
   size_t max_nondet_array_length,
+  size_t max_recursion_depth,
   const source_locationt &loc,
   message_handlert &message_handler)
 {
@@ -588,7 +599,8 @@ exprt object_factory(
       false,
       !allow_null,
       message_handler,
-      max_nondet_array_length);
+      max_nondet_array_length,
+      max_recursion_depth);
 
     return object;
   }

src/java_bytecode/java_object_factory.h

@@ -19,6 +19,7 @@ exprt object_factory(
   bool allow_null,
   symbol_tablet &symbol_table,
   size_t max_nondet_array_length,
+  size_t max_recursion_depth,
   const source_locationt &,
   message_handlert &message_handler);
 
@@ -31,7 +32,8 @@ void gen_nondet_init(
   bool create_dynamic_objects,
   bool assume_non_null,
   message_handlert &message_handler,
-  size_t max_nondet_array_length=5);
+  size_t max_nondet_array_length,
+  size_t max_recursion_depth);
 
 
 exprt get_nondet_bool(const typet &);