Merge pull request #2909 from romainbrenguier/bugfix/string-non-empty

Fix --string-non-empty option

Author: romainbrenguier

jbmc/regression/jbmc-strings/string-non-empty-option/Test.class

@@ -0,0 +1,22 @@
+public class Test {
+
+    static void checkMinLength(String arg1, String arg2, int nondet) {
+        // Filter
+        if (arg1 == null || arg2 == null)
+            return;
+
+        // The validity of the following assertion depends on
+        // whether --string-non-empty is used
+        if(nondet == 0) {
+            assert arg1.length() > 0;
+        } else if(nondet == 1) {
+            assert arg2.length() > 0;
+        } else if(nondet == 2) {
+            // For this assertion to be valid, also need to limit the length of
+            // strings because overflows could cause the sum to be negative.
+            assert arg1.length() + arg2.length() > 1;
+        } else {
+            assert arg1.length() > 1;
+        }
+    }
+}

jbmc/regression/jbmc-strings/string-non-empty-option/Test.java

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.checkMinLength
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 11 function java::Test.checkMinLength.*: FAILURE
+assertion.* line 13 function java::Test.checkMinLength.*: FAILURE
+assertion.* line 17 function java::Test.checkMinLength.*: FAILURE
+assertion.* line 19 function java::Test.checkMinLength.*: FAILURE

jbmc/regression/jbmc-strings/string-non-empty-option/test.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.checkMinLength --string-non-empty
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 11 function java::Test.checkMinLength.*: SUCCESS
+assertion.* line 13 function java::Test.checkMinLength.*: SUCCESS
+assertion.* line 17 function java::Test.checkMinLength.*: FAILURE
+assertion.* line 19 function java::Test.checkMinLength.*: FAILURE

jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.checkMinLength --string-non-empty --max-nondet-string-length 100000
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 11 function java::Test.checkMinLength.*: SUCCESS
+assertion.* line 13 function java::Test.checkMinLength.*: SUCCESS
+assertion.* line 17 function java::Test.checkMinLength.*: SUCCESS
+assertion.* line 19 function java::Test.checkMinLength.*: FAILURE

jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty_no_overflow.desc

@@ -68,6 +68,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
     object_factory_parameters.max_nondet_string_length =
       safe_string2size_t(cmd.get_value("max-nondet-string-length"));
   }
+  if(cmd.isset("string-non-empty"))
+    object_factory_parameters.min_nondet_string_length = 1;
 
   object_factory_parameters.string_printable = cmd.isset("string-printable");
   if(cmd.isset("java-max-vla-length"))

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -538,6 +538,7 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
 /// \param struct_expr [out]: struct that we may initialize
 /// \param code: block to add pre-requisite declarations (e.g. to allocate a
 ///   data array)
+/// \param min_nondet_string_length: minimum length of strings to initialize
 /// \param max_nondet_string_length: maximum length of strings to initialize
 /// \param loc: location in the source
 /// \param function_id: function ID to associate with auxiliary variables
@@ -573,6 +574,7 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
 bool initialize_nondet_string_fields(
   struct_exprt &struct_expr,
   code_blockt &code,
+  const std::size_t &min_nondet_string_length,
   const std::size_t &max_nondet_string_length,
   const source_locationt &loc,
   const irep_idt &function_id,
@@ -627,11 +629,10 @@ bool initialize_nondet_string_fields(
   code.add(code_declt(length_expr));
   code.add(code_assignt(length_expr, nondet_length));
 
-  // assume (length_expr >= 0);
-  code.add(
-    code_assumet(
-      binary_relation_exprt(
-        length_expr, ID_ge, from_integer(0, java_int_type()))));
+  // assume (length_expr >= min_nondet_string_length);
+  const exprt min_length =
+    from_integer(min_nondet_string_length, java_int_type());
+  code.add(code_assumet(binary_relation_exprt(length_expr, ID_ge, min_length)));
 
   // assume (length_expr <= max_input_length)
   if(max_nondet_string_length <= max_value(length_expr.type()))
@@ -1044,15 +1045,15 @@ void java_object_factoryt::gen_nondet_struct_init(
     // If the initialised type is a special-cased String type (one with length
     // and data fields introduced by string-library preprocessing), initialise
     // those fields with nondet values:
-    skip_special_string_fields =
-      initialize_nondet_string_fields(
-        to_struct_expr(initial_object),
-        assignments,
-        object_factory_parameters.max_nondet_string_length,
-        loc,
-        object_factory_parameters.function_id,
-        symbol_table,
-        object_factory_parameters.string_printable);
+    skip_special_string_fields = initialize_nondet_string_fields(
+      to_struct_expr(initial_object),
+      assignments,
+      object_factory_parameters.min_nondet_string_length,
+      object_factory_parameters.max_nondet_string_length,
+      loc,
+      object_factory_parameters.function_id,
+      symbol_table,
+      object_factory_parameters.string_printable);
 
     assignments.copy_to_operands(
       code_assignt(expr, initial_object));

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -28,6 +28,9 @@ struct object_factory_parameterst final
   /// Maximum value for the non-deterministically-chosen length of a string.
   size_t max_nondet_string_length=MAX_NONDET_STRING_LENGTH;
 
+  /// Minimum value for the non-deterministically-chosen length of a string.
+  size_t min_nondet_string_length = 0;
+
   /// 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

jbmc/src/java_bytecode/object_factory_parameters.h

@@ -33,11 +33,13 @@ Author: Alberto Griggio, [email protected]
 #define OPT_STRING_REFINEMENT \
   "(no-refine-strings)" \
   "(string-printable)" \
+  "(string-non-empty)" \
   "(max-nondet-string-length):"
 
 #define HELP_STRING_REFINEMENT \
   " --no-refine-strings          turn off string refinement\n" \
   " --string-printable           restrict to printable strings (experimental)\n" /* NOLINT(*) */ \
+  " --string-non-empty           restrict to non-empty strings (experimental)\n" /* NOLINT(*) */ \
   " --max-nondet-string-length n bound the length of nondet (e.g. input) strings\n" /* NOLINT(*) */
 
 // The integration of the string solver into CBMC is incomplete. Therefore,