Merge pull request #1235 from romainbrenguier/feature/string-max-input-length#948

Joel Allred · web-flow · commit bc309878a6ab · 2017-09-18T14:29:02.000+01:00
String max input length option
diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.class b/regression/strings-smoke-tests/max_input_length/MemberTest.class
diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.desc b/regression/strings-smoke-tests/max_input_length/MemberTest.desc
@@ -0,0 +1,7 @@
+CORE
+MemberTest.class
+--refine-strings --string-max-length 29 --java-assume-inputs-non-null
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/regression/strings-smoke-tests/max_input_length/MemberTest.java b/regression/strings-smoke-tests/max_input_length/MemberTest.java
@@ -0,0 +1,9 @@
+public class MemberTest {
+    String foo;
+    public void main() {
+        // Causes this function to be ignored if string-max-length is
+        // less than 40
+        String t = new String("0123456789012345678901234567890123456789");
+        assert foo != null && foo.length() < 30;
+    }
+}
diff --git a/regression/strings-smoke-tests/max_input_length/Test.class b/regression/strings-smoke-tests/max_input_length/Test.class
diff --git a/regression/strings-smoke-tests/max_input_length/Test.java b/regression/strings-smoke-tests/max_input_length/Test.java
@@ -0,0 +1,11 @@
+public class Test {
+    public static void main(String s) {
+	// This prevent anything from happening if string-max-length is smaller
+	// than 40
+	String t = new String("0123456789012345678901234567890123456789");
+	if (s.length() >= 30)
+	    // This should not happen when string-max-input length is smaller
+	    // than 30
+	    assert false;
+    }
+}
diff --git a/regression/strings-smoke-tests/max_input_length/test.desc b/regression/strings-smoke-tests/max_input_length/test.desc
@@ -0,0 +1,7 @@
+CORE
+Test.class
+--refine-strings --string-max-length 30
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/regression/strings-smoke-tests/max_input_length/test1.desc b/regression/strings-smoke-tests/max_input_length/test1.desc
@@ -0,0 +1,7 @@
+CORE
+Test.class
+--refine-strings --string-max-length 45  --string-max-input-length 31
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
diff --git a/regression/strings-smoke-tests/max_input_length/test2.desc b/regression/strings-smoke-tests/max_input_length/test2.desc
@@ -0,0 +1,7 @@
+CORE
+Test.class
+--refine-strings --string-max-length 45 --string-max-input-length 20
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -793,11 +793,16 @@ bool cbmc_parse_optionst::process_goto_program(
     // Similar removal of java nondet statements:
     // TODO Should really get this from java_bytecode_language somehow, but we
     // don't have an instance of that here.
-    const size_t max_nondet_array_length=
+    object_factory_parameterst factory_params;
+    factory_params.max_nondet_array_length=
       cmdline.isset("java-max-input-array-length")
         ? std::stoul(cmdline.get_value("java-max-input-array-length"))
         : MAX_NONDET_ARRAY_LENGTH_DEFAULT;
-    const size_t max_nondet_tree_depth=
+    factory_params.max_nondet_string_length=
+      cmdline.isset("string-max-input-length")
+        ? std::stoul(cmdline.get_value("string-max-input-length"))
+        : MAX_NONDET_STRING_LENGTH;
+    factory_params.max_nondet_tree_depth=
       cmdline.isset("java-max-input-tree-depth")
         ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
         : MAX_NONDET_TREE_DEPTH;
@@ -807,8 +812,7 @@ bool cbmc_parse_optionst::process_goto_program(
     convert_nondet(
       goto_model,
       get_message_handler(),
-      max_nondet_array_length,
-      max_nondet_tree_depth);
+      factory_params);
 
     // add generic checks
     status() << "Generic Property Instrumentation" << eom;
@@ -1067,7 +1071,8 @@ void cbmc_parse_optionst::help()
     " --refine-strings             use string refinement (experimental)\n"
     " --string-non-empty           add constraint that strings are non empty (experimental)\n" // NOLINT(*)
     " --string-printable           add constraint that strings are printable (experimental)\n" // NOLINT(*)
-    " --string-max-length          add constraint on the length of strings (experimental)\n" // NOLINT(*)
+    " --string-max-length          add constraint on the length of strings\n" // NOLINT(*)
+    " --string-max-input-length    add constraint on the length of input strings\n" // NOLINT(*)
     " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)
     " --arrays-uf-always           always turn arrays into uninterpreted functions\n" // NOLINT(*)
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
@@ -48,6 +48,7 @@ class optionst;
   "(string-non-empty)" \
   "(string-printable)" \
   "(string-max-length):" \
+  "(string-max-input-length):" \
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-loops)" \
diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp
@@ -34,8 +34,7 @@ static goto_programt::targett insert_nondet_init_code(
   const goto_programt::targett &target,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  size_t max_nondet_array_length,
-  size_t max_nondet_tree_depth)
+  const object_factory_parameterst &object_factory_parameters)
 {
   // Return if the instruction isn't an assignment
   const auto next_instr=std::next(target);
@@ -91,8 +90,7 @@ static goto_programt::targett insert_nondet_init_code(
     true,
     allocation_typet::DYNAMIC,
     nullable,
-    max_nondet_array_length,
-    max_nondet_tree_depth,
+    object_factory_parameters,
     update_in_placet::NO_UPDATE_IN_PLACE);
 
   // Convert this code into goto instructions
@@ -117,8 +115,7 @@ void convert_nondet(
   goto_programt &goto_program,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  size_t max_nondet_array_length,
-  size_t max_nondet_tree_depth)
+  const object_factory_parameterst &object_factory_parameters)
 {
   for(auto instruction_iterator=goto_program.instructions.begin(),
         end=goto_program.instructions.end();
@@ -129,26 +126,23 @@ void convert_nondet(
       instruction_iterator,
       symbol_table,
       message_handler,
-      max_nondet_array_length,
-      max_nondet_tree_depth);
+      object_factory_parameters);
   }
 }
 
 void convert_nondet(
   goto_functionst &goto_functions,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  size_t max_nondet_array_length,
-  size_t max_nondet_tree_depth)
+  const object_factory_parameterst &object_factory_parameters)
 {
   for(auto &goto_program : goto_functions.function_map)
   {
     convert_nondet(
       goto_program.second.body,
       symbol_table,
       message_handler,
-      max_nondet_array_length,
-      max_nondet_tree_depth);
+      object_factory_parameters);
   }
 
   goto_functions.compute_location_numbers();
@@ -159,13 +153,11 @@ void convert_nondet(
 void convert_nondet(
   goto_modelt &goto_model,
   message_handlert &message_handler,
-  size_t max_nondet_array_length,
-  size_t max_nondet_tree_depth)
+  const object_factory_parameterst& object_factory_parameters)
 {
   convert_nondet(
     goto_model.goto_functions,
     goto_model.symbol_table,
     message_handler,
-    max_nondet_array_length,
-    max_nondet_tree_depth);
+    object_factory_parameters);
 }
diff --git a/src/goto-programs/convert_nondet.h b/src/goto-programs/convert_nondet.h
@@ -18,26 +18,24 @@ class goto_functionst;
 class symbol_tablet;
 class goto_modelt;
 class message_handlert;
+struct object_factory_parameterst;
 
 /// Replace calls to nondet library functions with an internal nondet
 /// representation.
 /// \param goto_functions: The set of goto programs to modify.
 /// \param symbol_table: The symbol table to query/update.
 /// \param message_handler: For error logging.
-/// \param max_nondet_array_length: The maximum length of any new arrays.
-/// \param max_nondet_tree_depth: Maximum depth for object hierarchy on input
-///   parameterers.
+/// \param object_factory_parameters: Parameters for the generation of nondet
+///   objects.
 void convert_nondet(
   goto_functionst &,
   symbol_tablet &,
   message_handlert &,
-  std::size_t max_nondet_array_length,
-  std::size_t max_nondet_tree_depth);
+  const object_factory_parameterst &object_factory_parameters);
 
 void convert_nondet(
   goto_modelt &,
   message_handlert &,
-  std::size_t max_nondet_array_length,
-  std::size_t max_nondet_tree_depth);
+  const object_factory_parameterst &object_factory_parameters);
 
 #endif
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
@@ -42,11 +42,14 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   string_refinement_enabled=cmd.isset("refine-strings");
   throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions");
   if(cmd.isset("java-max-input-array-length"))
-    max_nondet_array_length=
+    object_factory_parameters.max_nondet_array_length=
       std::stoi(cmd.get_value("java-max-input-array-length"));
   if(cmd.isset("java-max-input-tree-depth"))
-    max_nondet_tree_depth=
+    object_factory_parameters.max_nondet_tree_depth=
       std::stoi(cmd.get_value("java-max-input-tree-depth"));
+  if(cmd.isset("string-max-input-length"))
+    object_factory_parameters.max_nondet_string_length=
+      std::stoi(cmd.get_value("string-max-input-length"));
   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"))
@@ -125,8 +128,7 @@ bool java_bytecode_languaget::generate_start_function(
     symbol_table,
     get_message_handler(),
     assume_inputs_non_null,
-    max_nondet_array_length,
-    max_nondet_tree_depth,
+    object_factory_parameters,
     *pointer_type_selector);
 }
 
@@ -402,8 +404,7 @@ bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
       main_class,
       get_message_handler(),
       assume_inputs_non_null,
-      max_nondet_array_length,
-      max_nondet_tree_depth,
+      object_factory_parameters,
       get_pointer_type_selector());
 }
 
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
@@ -48,6 +48,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "                                  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
 
 class symbolt;
@@ -59,6 +60,23 @@ enum lazy_methods_modet
   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;
+};
+
 typedef std::pair<
           const symbolt *,
           const java_bytecode_parse_treet::methodt *>
@@ -95,8 +113,7 @@ class java_bytecode_languaget:public languaget
   java_bytecode_languaget(
     std::unique_ptr<select_pointer_typet> pointer_type_selector):
       assume_inputs_non_null(false),
-      max_nondet_array_length(MAX_NONDET_ARRAY_LENGTH_DEFAULT),
-      max_nondet_tree_depth(MAX_NONDET_TREE_DEPTH),
+      object_factory_parameters(),
       max_user_array_length(0),
       lazy_methods_mode(lazy_methods_modet::LAZY_METHODS_MODE_EAGER),
       string_refinement_enabled(false),
@@ -149,8 +166,7 @@ class java_bytecode_languaget:public languaget
   std::vector<irep_idt> main_jar_classes;
   java_class_loadert java_class_loader;
   bool assume_inputs_non_null;      // assume inputs variables to be non-null
-  size_t max_nondet_array_length;   // maximal length for non-det array creation
-  size_t max_nondet_tree_depth;     // maximal depth for object tree in non-det creation
+  object_factory_parameterst object_factory_parameters;
   size_t max_user_array_length;     // max size for user code created arrays
   lazy_methodst lazy_methods;
   lazy_methods_modet lazy_methods_mode;
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
@@ -90,8 +90,7 @@ void java_static_lifetime_init(
   symbol_tablet &symbol_table,
   const source_locationt &source_location,
   bool assume_init_pointers_not_null,
-  unsigned max_nondet_array_length,
-  unsigned max_nondet_tree_depth,
+  const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   symbolt &initialize_symbol=symbol_table.lookup(INITIALIZE);
@@ -132,8 +131,7 @@ void java_static_lifetime_init(
           code_block,
           allow_null,
           symbol_table,
-          max_nondet_array_length,
-          max_nondet_tree_depth,
+          object_factory_parameters,
           allocation_typet::GLOBAL,
           source_location,
           pointer_type_selector);
@@ -164,8 +162,7 @@ exprt::operandst java_build_arguments(
   code_blockt &init_code,
   symbol_tablet &symbol_table,
   bool assume_init_pointers_not_null,
-  size_t max_nondet_array_length,
-  size_t max_nondet_tree_depth,
+  object_factory_parameterst object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   const code_typet::parameterst &parameters=
@@ -221,8 +218,7 @@ exprt::operandst java_build_arguments(
         init_code,
         allow_null,
         symbol_table,
-        max_nondet_array_length,
-        max_nondet_tree_depth,
+        object_factory_parameters,
         allocation_typet::LOCAL,
         function.location,
         pointer_type_selector);
@@ -481,8 +477,7 @@ 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_tree_depth,
+  const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   // check if the entry point is already there
@@ -506,17 +501,15 @@ bool java_entry_point(
     symbol_table,
     symbol.location,
     assume_init_pointers_not_null,
-    max_nondet_array_length,
-    max_nondet_tree_depth,
+    object_factory_parameters,
     pointer_type_selector);
 
   return generate_java_start_function(
     symbol,
     symbol_table,
     message_handler,
     assume_init_pointers_not_null,
-    max_nondet_array_length,
-    max_nondet_tree_depth,
+    object_factory_parameters,
     pointer_type_selector);
 }
 
@@ -538,8 +531,7 @@ bool generate_java_start_function(
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   bool assume_init_pointers_not_null,
-  size_t max_nondet_array_length,
-  size_t max_nondet_tree_depth,
+  const object_factory_parameterst& object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
   messaget message(message_handler);
@@ -618,8 +610,7 @@ bool generate_java_start_function(
       init_code,
       symbol_table,
       assume_init_pointers_not_null,
-      max_nondet_array_length,
-      max_nondet_tree_depth,
+      object_factory_parameters,
       pointer_type_selector);
   call_main.arguments()=main_arguments;
 
diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h
