Merge pull request diffblue#2052 from romainbrenguier/bugfix/default-axioms2#TG-2138

[TG-2138] Stop adding default axioms in string solver

Author: Daniel Kroening

regression/jbmc-strings/long_string/Test.class

@@ -30,7 +30,9 @@ public static void checkAbort(String s, String t) {
         String u = s.concat(t);
 
         // Filter out
-        if(u.length() < 67_108_864)
+        // 67_108_864 corresponds to the maximum length for which the solver
+        // will concretize the string.
+        if(u.length() <= 67_108_864)
             return;
         if(CProverString.charAt(u, 2_000_000) != 'b')
             return;

regression/jbmc-strings/long_string/Test.java

@@ -1,9 +1,10 @@
 CORE
 Test.class
---refine-strings --function Test.checkAbort
-^EXIT=6$
+--refine-strings --function Test.checkAbort --trace
+^EXIT=10$
 ^SIGNAL=0$
+dynamic_object[0-9]*=\(assignment removed\)
 --
 --
-This tests should abort, because concretizing a string of the required
-length may take to much memory.
+This tests that the object does not appear in the trace, because concretizing
+a string of the required length may take too much memory.

regression/jbmc-strings/long_string/test_abort.desc

@@ -0,0 +1,44 @@
+public class IntegerTests {
+
+    public static Boolean testMyGenSet(Integer key) {
+        if (key == null) return null;
+        MyGenSet<Integer> ms = new MyGenSet<>();
+        ms.array[0] = 101;
+        if (ms.contains(key)) return true;
+        return false;
+    }
+
+    public static Boolean testMySet(Integer key) {
+        if (key == null) return null;
+        MySet ms = new MySet();
+        ms.array[0] = 101;
+        if (ms.contains(key)) return true;
+        return false;
+    }
+
+}
+
+class MyGenSet<E> {
+    E[] array;
+    @SuppressWarnings("unchecked")
+    MyGenSet() {
+        array = (E[]) new Object[1];
+    }
+    boolean contains(E o) {
+        if (o.equals(array[0]))
+            return true;
+        return false;
+    }
+}
+
+class MySet {
+    Integer[] array;
+    MySet() {
+        array = new Integer[1];
+    }
+    boolean contains(Integer o) {
+        if (o.equals(array[0]))
+            return true;
+        return false;
+    }
+}

regression/jbmc-strings/max-length-generic-array/IntegerTests.class

@@ -0,0 +1,19 @@
+CORE
+IntegerTests.class
+-refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMySet --cover location
+^EXIT=0$
+^SIGNAL=0$
+coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 1 .* SATISFIED
+coverage.* line 12 function java::IntegerTests.testMySet.* bytecode-index 3 .* SATISFIED
+coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 4 .* SATISFIED
+coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 6 .* SATISFIED
+coverage.* line 13 function java::IntegerTests.testMySet.* bytecode-index 7 .* SATISFIED
+coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 12 .* SATISFIED
+coverage.* line 14 function java::IntegerTests.testMySet.* bytecode-index 13 .* SATISFIED
+coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 16 .* SATISFIED
+coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 17 .* SATISFIED
+coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 21 .* SATISFIED
+coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 19 .* SATISFIED
+coverage.* line 15 function java::IntegerTests.testMySet.* bytecode-index 20 .* SATISFIED
+coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 22 .* SATISFIED
+coverage.* line 16 function java::IntegerTests.testMySet.* bytecode-index 23 .* SATISFIED

regression/jbmc-strings/max-length-generic-array/IntegerTests.java

@@ -0,0 +1,20 @@
+CORE
+IntegerTests.class
+-refine-strings --string-max-length 100 IntegerTests.class --function IntegerTests.testMyGenSet --cover location
+^EXIT=0$
+^SIGNAL=0$
+coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 1 .* SATISFIED
+coverage.* line 4 function java::IntegerTests.testMyGenSet.* bytecode-index 3 .* SATISFIED
+coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 4 .* SATISFIED
+coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 6 .* SATISFIED
+coverage.* line 5 function java::IntegerTests.testMyGenSet.* bytecode-index 7 .* SATISFIED
+coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 10 .* SATISFIED
+coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 13 .* SATISFIED
+coverage.* line 6 function java::IntegerTests.testMyGenSet.* bytecode-index 14 .* SATISFIED
+coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 17 .* SATISFIED
+coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 18 .* SATISFIED
+coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 22 .* SATISFIED
+coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 20 .* SATISFIED
+coverage.* line 7 function java::IntegerTests.testMyGenSet.* bytecode-index 21 .* SATISFIED
+coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 23 .* SATISFIED
+coverage.* line 8 function java::IntegerTests.testMyGenSet.* bytecode-index 24 .* SATISFIED

regression/jbmc-strings/max-length-generic-array/MyGenSet.class

@@ -0,0 +1,37 @@
+public class Test {
+
+    static void checkMaxInputLength(String arg1, String arg2) {
+        // Filter
+        if (arg1 == null || arg2 == null)
+            return;
+
+        // The validity of this depends on string-max-input-length
+        assert arg1.length() + arg2.length() < 1_000_000;
+    }
+
+    static void checkMaxLength(String arg1, String arg2) {
+        // Filter
+        if (arg1 == null || arg2 == null)
+            return;
+
+        if(arg1.length() + arg2.length() < 4_001)
+            return;
+
+        // Act
+        String s = arg1.concat(arg2);
+
+        // When string-max-length is smaller than 4_000 this will
+        // always be the case
+        assert org.cprover.CProverString.charAt(s, 4_000) == '?';
+    }
+
+    static void main(String argv[]) {
+        // Filter
+        if (argv.length < 2)
+            return;
+
+        // Act
+        checkMaxInputLength(argv[0], argv[1]);
+        checkMaxLength(argv[0], argv[1]);
+    }
+}

regression/jbmc-strings/max-length-generic-array/MySet.class

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --verbosity 10 --string-max-input-length 499999 --function Test.checkMaxInputLength
+^EXIT=0$
+^SIGNAL=0$
+assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: SUCCESS

regression/jbmc-strings/max-length-generic-array/test.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --verbosity 10 --string-max-input-length 500000 --function Test.checkMaxInputLength
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: FAILURE

regression/jbmc-strings/max-length-generic-array/test_gen.desc

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--refine-strings --verbosity 10 --string-max-length 4001 --function Test.checkMaxLength
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: FAILURE

regression/jbmc-strings/max-length/Test.class

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --verbosity 10 --string-max-length 4000 --function Test.checkMaxLength
+^SIGNAL=0$
+--
+^EXIT=0$
+assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: SUCCESS
+--
+The solver may give an ERROR because the value of string-max-length is too
+small to give an answer about the assertion.
+So we just check that the answer is not success.

regression/jbmc-strings/max-length/Test.java

@@ -999,8 +999,9 @@ void cbmc_parse_optionst::help()
     " --refine                     use refinement procedure (experimental)\n"
     " --refine-strings             use string refinement (experimental)\n"
     " --string-printable           add constraint that strings are printable (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(*)
+    " --string-max-length          add constraint on the length of strings"
+    "                              (deprecated: use string-max-input-length instead)\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(*)

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

@@ -177,7 +177,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
   info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
   info.ui=ui;
   if(options.get_bool_option("string-max-length"))
-    info.string_max_length=options.get_signed_int_option("string-max-length");
+    info.max_string_length = options.get_signed_int_option("string-max-length");
   info.trace=options.get_bool_option("trace");
   if(options.get_bool_option("max-node-refinement"))
     info.max_node_refinement=

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

@@ -55,6 +55,10 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   if(cmd.isset("string-max-input-length"))
     object_factory_parameters.max_nondet_string_length=
       std::stoi(cmd.get_value("string-max-input-length"));
+  else if(cmd.isset("string-max-length"))
+    object_factory_parameters.max_nondet_string_length =
+      std::stoi(cmd.get_value("string-max-length"));
+
   object_factory_parameters.string_printable = cmd.isset("string-printable");
   if(cmd.isset("java-max-vla-length"))
     max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length"));

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

@@ -878,7 +878,7 @@ codet java_string_library_preprocesst::code_assign_string_expr_to_java_string(
 /// \param symbol_table: symbol table
 /// \param [out] code: code block that gets appended the following code:
 /// ~~~~~~~~~~~~~~~~~~~~~~
-/// lhs.length=rhs->length
+/// lhs.length = rhs==null ? 0 : rhs->length
 /// lhs.data=rhs->data
 /// ~~~~~~~~~~~~~~~~~~~~~~
 void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
@@ -899,8 +899,13 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
 
   const dereference_exprt deref = checked_dereference(rhs, deref_type);
 
-  // Fields of the string object
-  const exprt rhs_length = get_length(deref, symbol_table);
+  // Although we should not reach this code if rhs is null, the association
+  // `pointer -> length` is added to the solver anyway, so we have to make sure
+  // the length is set to something reasonable.
+  const auto rhs_length = if_exprt(
+    equal_exprt(rhs, null_pointer_exprt(to_pointer_type(rhs.type()))),
+    from_integer(0, lhs.length().type()),
+    get_length(deref, symbol_table));
 
   // Assignments
   code.add(code_assignt(lhs.length(), rhs_length), loc);

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

@@ -94,14 +94,7 @@ class string_constraint_generatort final
   // Used by format function
   class format_specifiert;
 
-  /// Arguments pack for the string_constraint_generator constructor
-  struct infot
-  {
-    /// Max length of non-deterministic strings
-    size_t string_max_length=std::numeric_limits<size_t>::max();
-  };
-
-  string_constraint_generatort(const infot& info, const namespacet& ns);
+  explicit string_constraint_generatort(const namespacet &ns);
 
   /// Axioms are of three kinds: universally quantified string constraint,
   /// not contains string constraints and simple formulas.
@@ -181,10 +174,9 @@ class string_constraint_generatort final
 
   static constant_exprt constant_char(int i, const typet &char_type);
 
-  array_string_exprt
+  const array_string_exprt &
   char_array_of_pointer(const exprt &pointer, const exprt &length);
 
-  void add_default_axioms(const array_string_exprt &s);
   exprt axiom_for_is_positive_index(const exprt &x);
 
   void add_constraint_on_characters(
@@ -402,7 +394,6 @@ class string_constraint_generatort final
 
   // MEMBERS
 public:
-  const size_t max_string_length;
   // Used to store information about witnesses for not_contains constraints
   std::map<string_not_contains_constraintt, symbol_exprt> witness;
 private:

src/cbmc/cbmc_parse_options.cpp

@@ -28,10 +28,8 @@ Author: Romain Brenguier, [email protected]
 #include <util/string_constant.h>
 #include <util/deprecate.h>
 
-string_constraint_generatort::string_constraint_generatort(
-  const string_constraint_generatort::infot &info,
-  const namespacet &ns)
-  : array_pool(fresh_symbol), max_string_length(info.string_max_length), ns(ns)
+string_constraint_generatort::string_constraint_generatort(const namespacet &ns)
+  : array_pool(fresh_symbol), ns(ns)
 {
 }
 
@@ -172,7 +170,6 @@ array_string_exprt string_constraint_generatort::fresh_string(
   symbol_exprt content = fresh_symbol("string_content", array_type);
   array_string_exprt str = to_array_string_expr(content);
   created_strings.insert(str);
-  add_default_axioms(str);
   return str;
 }
 
@@ -279,7 +276,7 @@ exprt string_constraint_generatort::associate_array_to_pointer(
 
   const exprt &pointer_expr = f.arguments()[1];
   array_pool.insert(pointer_expr, array_expr);
-  add_default_axioms(to_array_string_expr(array_expr));
+  created_strings.emplace(to_array_string_expr(array_expr));
   return from_integer(0, f.type());
 }
 
@@ -319,27 +316,6 @@ void string_constraint_generatort::clear_constraints()
   not_contains_constraints.clear();
 }
 
-/// adds standard axioms about the length of the string and its content: * its
-/// length should be positive * it should not exceed max_string_length * if
-/// force_printable_characters is true then all characters should belong to the
-/// range of ASCII characters between ' ' and '~'
-/// \param s: a string expression
-/// \return a string expression that is linked to the argument through axioms
-///   that are added to the list
-void string_constraint_generatort::add_default_axioms(
-  const array_string_exprt &s)
-{
-  // If `s` was already added we do nothing.
-  if(!created_strings.insert(s).second)
-    return;
-
-  const exprt index_zero = from_integer(0, s.length().type());
-  lemmas.push_back(s.axiom_for_length_ge(index_zero));
-
-  if(max_string_length!=std::numeric_limits<size_t>::max())
-    lemmas.push_back(s.axiom_for_length_le(max_string_length));
-}
-
 /// Add constraint on characters of a string.
 ///
 /// This constraint is
@@ -409,14 +385,13 @@ array_string_exprt array_poolt::find(const exprt &pointer, const exprt &length)
 }
 
 /// Adds creates a new array if it does not already exists
-/// \todo This should be replaced by associate_char_array_to_char_pointer
-array_string_exprt string_constraint_generatort::char_array_of_pointer(
+/// \todo This should be replaced
+/// by array_poolt.make_char_array_for_char_pointer
+const array_string_exprt &string_constraint_generatort::char_array_of_pointer(
   const exprt &pointer,
   const exprt &length)
 {
-  const array_string_exprt array = array_pool.find(pointer, length);
-  add_default_axioms(array);
-  return array;
+  return *created_strings.insert(array_pool.find(pointer, length)).first;
 }
 
 array_string_exprt array_poolt::find(const refined_string_exprt &str)