[TG-2138] Remove default axioms for strings in string solver

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

@@ -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/test.desc

@@ -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/test_gen.desc

@@ -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/Test.java

@@ -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/test1.desc

@@ -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/test2.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/test3.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/test4.desc

@@ -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/strings-smoke-tests/java_format2/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --verbosity 10 --string-max-length 20
+--refine-strings --verbosity 10 --string-max-input-length 20
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$

regression/strings-smoke-tests/max_input_length/MemberTest.desc

@@ -1,8 +1,8 @@
 CORE
 MemberTest.class
---refine-strings --verbosity 10 --string-max-length 29 --java-assume-inputs-non-null --function MemberTest.main
-^EXIT=0$
+--refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 31 --function MemberTest.main
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 --
 non equal types

regression/strings-smoke-tests/max_input_length/MemberTest.java

@@ -1,9 +1,17 @@
 public class MemberTest {
     String foo;
+
     public void main() {
-        // Causes this function to be ignored if string-max-length is
-        // less than 40
+        if (foo == null)
+          return;
+
+        // This would prevent anything from happening if we were to add a
+        // constraints on strings being smaller than 40
         String t = new String("0123456789012345678901234567890123456789");
-        assert foo != null && foo.length() < 30;
+
+        if (foo.length() >= 30)
+            // This should not happen when string-max-input length is smaller
+            // than 30
+            assert false;
     }
 }

regression/strings-smoke-tests/max_input_length/MemberTest2.desc

@@ -0,0 +1,8 @@
+CORE
+MemberTest.class
+--refine-strings --verbosity 10 --string-max-length 45 --string-max-input-length 20 --function MemberTest.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+non equal types

regression/strings-smoke-tests/max_input_length/Test.java

@@ -1,8 +1,8 @@
 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");
+        // This prevent anything from happening if we were to add a constraints on strings
+        // being 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

src/cbmc/cbmc_solvers.cpp

@@ -176,8 +176,10 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
   info.prop=prop.get();
   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_bool_option("string-max-length")
+      ? options.get_unsigned_int_option("string-max-length")
+      : DEFAULT_MAX_STRING_LENGTH;
   info.trace=options.get_bool_option("trace");
   if(options.get_bool_option("max-node-refinement"))
     info.max_node_refinement=

src/java_bytecode/java_bytecode_language.cpp

@@ -56,6 +56,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"));

src/solvers/refinement/string_constraint_generator.h

@@ -37,14 +37,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.
@@ -108,7 +101,6 @@ class string_constraint_generatort final
   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(
@@ -344,7 +336,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/solvers/refinement/string_constraint_generator_main.cpp

@@ -28,11 +28,8 @@ Author: Romain Brenguier, [email protected]
 #include <util/ssa_expr.h>
 #include <util/string_constant.h>
 
-string_constraint_generatort::string_constraint_generatort(
-  const string_constraint_generatort::infot &info,
-  const namespacet &ns)
-  : max_string_length(info.string_max_length),
-    ns(ns)
+string_constraint_generatort::string_constraint_generatort(const namespacet &ns)
+  : ns(ns)
 {
 }
 
@@ -181,7 +178,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;
 }
 
@@ -249,7 +245,7 @@ string_constraint_generatort::associate_char_array_to_char_pointer(
   auto insert_result =
     arrays_of_pointers_.insert(std::make_pair(char_pointer, array_sym));
   array_string_exprt result = to_array_string_expr(insert_result.first->second);
-  add_default_axioms(result);
+  created_strings.insert(result);
   return result;
 }
 
@@ -287,7 +283,7 @@ exprt string_constraint_generatort::associate_array_to_pointer(
     arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr));
   INVARIANT(
     it_bool.second, "should not associate two arrays to the same pointer");
-  add_default_axioms(to_array_string_expr(array_expr));
+  created_strings.emplace(to_array_string_expr(array_expr));
   return from_integer(0, f.type());
 }
 
@@ -320,27 +316,6 @@ string_constraint_generatort::get_string_expr(const exprt &expr)
   return char_array_of_pointer(str.content(), str.length());
 }
 
-/// 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