String solver: support bounded-length intermediate strings

.gitignore

@@ -60,8 +60,7 @@ regression/**/tests-*.log
 regression/**/*.goto-cc-saved
 regression/**/*.gb
 regression/**/*.smt2
-jbmc/regression/**/tests.log
-jbmc/regression/**/tests-symex-driven-loading.log
+jbmc/regression/**/*.log
 
 # regression/coverage file
 /regression/coverage_**

jbmc/regression/jbmc-strings/CMakeLists.txt

@@ -2,6 +2,13 @@ add_test_pl_tests(
     "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
 )
 
+add_test_pl_profile(
+    "jbmc-strings-fixed-size-arrays"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity"
+    "-C;-s;fixed-size-strings;-X;limited-size-strings-expected-failure"
+    "CORE"
+)
+
 add_test_pl_profile(
     "jbmc-strings-symex-driven-lazy-loading"
     "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"

jbmc/regression/jbmc-strings/Makefile

@@ -4,18 +4,22 @@ include ../../src/config.inc
 
 test:
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity" -X limited-size-strings-expected-failure -s fixed-size-strings
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 testfuture:
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity" -CF -X limited-size-strings-expected-failure -s fixed-size-strings
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
 
 testall:
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity" -CFTK -X limited-size-strings-expected-failure -s fixed-size-strings
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity" -X limited-size-strings-expected-failure -s fixed-size-strings
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:

jbmc/regression/jbmc-strings/StringContains03/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.check
 ^EXIT=10$

jbmc/regression/jbmc-strings/StringIndexOf/test.desc

@@ -1,6 +1,9 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.check --unwind 4 --max-nondet-string-length 3 --java-assume-inputs-non-null
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
+--
+--
+Actually works fine with limited size strings, just takes a very long time.

jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.det 
 ^EXIT=10$

jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.nonDet  --max-nondet-string-length 1000
 ^EXIT=10$

jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc

@@ -8,3 +8,4 @@ assertion at file Test.java line 50 .*: FAILURE
 --
 --
 Check that when there are dependencies, axioms are added correctly.
+

jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.det
 ^EXIT=10$

jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.nonDet --max-nondet-string-length 1000
 ^EXIT=10$

jbmc/regression/jbmc-strings/long_string/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.check --max-nondet-string-length 2000000
 ^EXIT=10$

jbmc/regression/jbmc-strings/long_string/test_abort.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.checkAbort --trace --max-nondet-string-length 100000000
 ^EXIT=10$

jbmc/regression/jbmc-strings/max-length/test2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --max-nondet-string-length 500000 --function Test.checkMaxInputLength
 ^EXIT=10$

jbmc/regression/jbmc-strings/max-length/test3.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --max-nondet-string-length 4001 --function Test.checkMaxLength
 ^EXIT=10$

jbmc/regression/jbmc-strings/max-length/test4.desc

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --max-nondet-string-length 4000 --function Test.checkMaxLength
 ^SIGNAL=0$

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

@@ -1,4 +1,4 @@
-CORE
+CORE limited-size-strings-expected-failure
 Test
 --function Test.checkMinLength --string-non-empty --max-nondet-string-length 2147483647
 ^EXIT=10$

jbmc/regression/strings-smoke-tests/CMakeLists.txt

@@ -2,6 +2,13 @@ add_test_pl_tests(
     "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
 )
 
+add_test_pl_profile(
+    "strings-smoke-tests-fixed-size-arrays"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity"
+    "-C;-s;fixed-size-strings;-X;limited-size-strings-expected-failure"
+    "CORE"
+)
+
 add_test_pl_profile(
     "strings-smoke-tests-symex-driven-lazy-loading"
     "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"

jbmc/regression/strings-smoke-tests/Makefile

@@ -4,18 +4,22 @@ include ../../src/config.inc
 
 test:
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity" -X limited-size-strings-expected-failure -s fixed-size-strings
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 testfuture:
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity" -CF -X limited-size-strings-expected-failure -s fixed-size-strings
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
 
 testall:
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity" -CFTK -X limited-size-strings-expected-failure -s fixed-size-strings
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
 
 tests.log: ../$(CPROVER_DIR)/regression/test.pl
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
+	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --max-intermediate-string-length 100 --use-fixed-size-arrays-for-bounded-strings --no-array-field-sensitivity" -X limited-size-strings-expected-failure -s fixed-size-strings
 	@../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
 
 show:

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -261,6 +261,16 @@ java_bytecode_language_optionst::java_bytecode_language_optionst(
 void java_bytecode_languaget::set_language_options(const optionst &options)
 {
   object_factory_parameters.set(options);
+  if(options.is_set("max-intermediate-string-length"))
+  {
+    string_preprocess.set_max_intermediate_string_length(
+      options.get_unsigned_int_option("max-intermediate-string-length"));
+  }
+  if(options.is_set("use-fixed-size-arrays-for-bounded-strings"))
+  {
+    string_preprocess.set_use_fixed_size_arrays_for_bounded_strings(true);
+  }
+
   language_options = java_bytecode_language_optionst{options, *this};
   const auto &new_points = build_extra_entry_points(options);
   language_options->extra_methods.insert(

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -327,6 +327,9 @@ static irep_idt integer_interval_to_string(const integer_intervalt &interval)
 ///   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 use_fixed_size_array_for_bounded_string: if true, allocate a fixed
+//    size array when  max_nondet_string_length is set and reasonably small
+//    (currently hard-coded to 256 chars)
 /// \param loc: location in the source
 /// \param function_id: function ID to associate with auxiliary variables
 /// \param symbol_table: the symbol table
@@ -362,6 +365,7 @@ void initialize_nondet_string_fields(
   code_blockt &code,
   const std::size_t &min_nondet_string_length,
   const std::size_t &max_nondet_string_length,
+  const bool use_fixed_size_array_for_bounded_string,
   const source_locationt &loc,
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
@@ -413,8 +417,13 @@ void initialize_nondet_string_fields(
       code_assumet(binary_relation_exprt(length_expr, ID_le, max_length)));
   }
 
-  const exprt data_expr =
-    make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
+  const exprt data_expr = make_nondet_char_array(
+    symbol_table,
+    loc,
+    function_id,
+    code,
+    use_fixed_size_array_for_bounded_string ? max_nondet_string_length
+                                            : optionalt<size_t>{});
   struct_expr.operands()[struct_type.component_number("length")] = length_expr;
 
   const address_of_exprt array_pointer(
@@ -832,6 +841,7 @@ void java_object_factoryt::gen_nondet_struct_init(
         assignments,
         object_factory_parameters.min_nondet_string_length,
         object_factory_parameters.max_nondet_string_length,
+        object_factory_parameters.use_fixed_size_arrays_for_bounded_strings,
         location,
         object_factory_parameters.function_id,
         symbol_table,

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -17,6 +17,7 @@ Date:   April 2017
 ///   java.lang.StringBuilder, java.lang.StringBuffer.
 
 #include <goto-programs/class_identifier.h>
+#include <solvers/strings/max_concrete_char_array.h>
 #include <util/allocate_objects.h>
 #include <util/arith_tools.h>
 #include <util/c_types.h>
@@ -493,8 +494,21 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   const side_effect_expr_nondett nondet_length(str.length().type(), loc);
   code.add(code_assignt(str.length(), nondet_length), loc);
 
-  const exprt nondet_array_expr =
-    make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
+  const exprt nondet_array_expr = make_nondet_char_array(
+    symbol_table,
+    loc,
+    function_id,
+    code,
+    use_fixed_size_arrays_for_bounded_strings ? max_intermediate_string_length
+                                              : optionalt<size_t>{});
+
+  if(max_intermediate_string_length)
+  {
+    code.add(code_assumet(binary_relation_exprt(
+      str.length(),
+      ID_le,
+      from_integer(*max_intermediate_string_length, java_int_type()))));
+  }
 
   const address_of_exprt array_pointer(
     index_exprt(nondet_array_expr, from_integer(0, java_int_type())));
@@ -576,23 +590,26 @@ codet java_string_library_preprocesst::code_return_function_application(
     make_function_application(function_id, arguments, type, symbol_table));
 }
 
-/// Declare a fresh symbol of type array of character with infinite size.
+/// Declare a fresh symbol of type array of characters suitable for a string
+/// of the given maximum length
 /// \param symbol_table: the symbol table
 /// \param loc: source location
 /// \param function_id: name of the function containing the array
 /// \param [out] code: code block where the declaration gets added
+/// \param max_length: maximum string length
 /// \return created symbol expression
-exprt make_nondet_infinite_char_array(
+exprt make_nondet_char_array(
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
   const irep_idt &function_id,
-  code_blockt &code)
+  code_blockt &code,
+  optionalt<std::size_t> max_length)
 {
-  const array_typet array_type(
-    java_char_type(), infinity_exprt(java_int_type()));
+  const array_typet array_type =
+    make_char_array_type(java_char_type(), java_int_type(), max_length);
   const symbolt data_sym = fresh_java_symbol(
     pointer_type(array_type),
-    "nondet_infinite_array_pointer",
+    "nondet_array_pointer",
     loc,
     function_id,
     symbol_table);

jbmc/src/java_bytecode/java_string_library_preprocess.h

@@ -44,6 +44,15 @@ class java_string_library_preprocesst:public messaget
 
   void initialize_known_type_table();
   void initialize_conversion_table();
+  void set_max_intermediate_string_length(
+    optionalt<std::size_t> max_intermediate_string_length_)
+  {
+    this->max_intermediate_string_length = max_intermediate_string_length_;
+  }
+  void set_use_fixed_size_arrays_for_bounded_strings(bool value)
+  {
+    use_fixed_size_arrays_for_bounded_strings = value;
+  }
 
   bool implements_function(const irep_idt &function_id) const;
   void get_all_function_names(std::unordered_set<irep_idt> &methods) const;
@@ -145,6 +154,13 @@ class java_string_library_preprocesst:public messaget
   // A set tells us what java types should be considered as string objects
   std::unordered_set<irep_idt> string_types;
 
+  // Maximum length enforced on freshly-allocated strings
+  optionalt<std::size_t> max_intermediate_string_length;
+
+  // If true, allocate fixed-size arrays to hold small (currently hard-coded
+  // to 256 chars) bounded strings
+  bool use_fixed_size_arrays_for_bounded_strings = false;
+
   code_blockt make_float_to_string_code(
     const java_method_typet &type,
     const source_locationt &loc,
@@ -309,11 +325,12 @@ class java_string_library_preprocesst:public messaget
     symbol_table_baset &symbol_table);
 };
 
-exprt make_nondet_infinite_char_array(
+exprt make_nondet_char_array(
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
   const irep_idt &function_id,
-  code_blockt &code);
+  code_blockt &code,
+  optionalt<std::size_t> max_length);
 
 void add_pointer_to_array_association(
   const exprt &pointer,

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -299,6 +299,16 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("refine-arithmetic", true);
   }
 
+  if(cmdline.isset("max-intermediate-string-length"))
+  {
+    options.set_option(
+      "max-intermediate-string-length",
+      cmdline.get_value("max-intermediate-string-length"));
+  }
+
+  if(cmdline.isset("use-fixed-size-arrays-for-bounded-strings"))
+    options.set_option("use-fixed-size-arrays-for-bounded-strings", true);
+
   if(cmdline.isset("no-refine-strings"))
     options.set_option("refine-strings", false);
 
@@ -457,6 +467,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("show-goto-symex-steps"))
     options.set_option("show-goto-symex-steps", true);
+
+  if(!string_solver_options_valid(options, log))
+    exit(CPROVER_EXIT_USAGE_ERROR);
 }
 
 /// invoke main modules

jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

@@ -89,20 +89,20 @@ SCENARIO(
           "tmp_object_factory = NONDET(int);",
           CPROVER_PREFIX "assume(tmp_object_factory >= 0);",
           CPROVER_PREFIX "assume(tmp_object_factory <= 20);",
-          "char (*nondet_infinite_array_pointer)[INFINITY()];",
-          "nondet_infinite_array_pointer = "
+          "char (*nondet_array_pointer)[INFINITY()];",
+          "nondet_array_pointer = "
             "ALLOCATE(char [INFINITY()], INFINITY(), false);",
-          "*nondet_infinite_array_pointer = NONDET(char [INFINITY()]);",
+          "*nondet_array_pointer = NONDET(char [INFINITY()]);",
           "int return_array;",
           "return_array = cprover_associate_array_to_pointer_func"
-            "(*nondet_infinite_array_pointer, *nondet_infinite_array_pointer);",
+            "(*nondet_array_pointer, *nondet_array_pointer);",
           "int return_array;",
           "return_array = cprover_associate_length_to_array_func"
-            "(*nondet_infinite_array_pointer, tmp_object_factory);",
+            "(*nondet_array_pointer, tmp_object_factory);",
           "arg = { [email protected]={ .@class_identifier"
             "=\"java::java.lang.String\" },"
             " .length=tmp_object_factory, "
-            ".data=*nondet_infinite_array_pointer };"};
+            ".data=*nondet_array_pointer };"};
         // clang-format on
 
         for(std::size_t i = 0;