Computation of dependency graph for strings [TG-2605]

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/solvers/Makefile

@@ -179,6 +179,7 @@ SRC = $(BOOLEFORCE_SRC) \
       refinement/refine_arithmetic.cpp \
       refinement/refine_arrays.cpp \
       refinement/string_refinement.cpp \
+      refinement/string_refinement_util.cpp \
       refinement/string_constraint_generator_code_points.cpp \
       refinement/string_constraint_generator_comparison.cpp \
       refinement/string_constraint_generator_concat.cpp \

src/solvers/refinement/string_constraint_generator.h

@@ -27,6 +27,62 @@ Author: Romain Brenguier, [email protected]
 #include <util/constexpr.def>
 #include <solvers/refinement/string_constraint.h>
 
+/// Generation of fresh symbols of a given type
+class symbol_generatort final
+{
+public:
+  symbol_exprt
+  operator()(const irep_idt &prefix, const typet &type = bool_typet());
+
+private:
+  unsigned symbol_count = 0;
+};
+
+/// Correspondance between arrays and pointers string representations
+class array_poolt final
+{
+public:
+  explicit array_poolt(symbol_generatort &symbol_generator)
+    : fresh_symbol(symbol_generator)
+  {
+  }
+
+  const std::unordered_map<exprt, array_string_exprt, irep_hash> &
+  get_arrays_of_pointers() const
+  {
+    return arrays_of_pointers;
+  }
+
+  exprt get_length(const array_string_exprt &s) const;
+
+  void insert(const exprt &pointer_expr, array_string_exprt &array);
+
+  array_string_exprt find(const exprt &pointer, const exprt &length);
+
+  array_string_exprt find(const refined_string_exprt &str);
+
+  /// Converts a struct containing a length and pointer to an array.
+  /// This allows to get a string expression from arguments of a string
+  /// builtion function, because string arguments in these function calls
+  /// are given as a struct containing a length and pointer to an array.
+  array_string_exprt of_argument(const exprt &arg);
+
+private:
+  // associate arrays to char pointers
+  std::unordered_map<exprt, array_string_exprt, irep_hash> arrays_of_pointers;
+
+  // associate length to arrays of infinite size
+  std::unordered_map<array_string_exprt, symbol_exprt, irep_hash>
+    length_of_array;
+
+  // generates fresh symbols
+  symbol_generatort &fresh_symbol;
+
+  array_string_exprt make_char_array_for_char_pointer(
+    const exprt &char_pointer,
+    const typet &char_array_type);
+};
+
 class string_constraint_generatort final
 {
 public:
@@ -69,22 +125,22 @@ class string_constraint_generatort final
     return index_exprt(witness.at(c), univ_val);
   }
 
-  symbol_exprt fresh_symbol(
-    const irep_idt &prefix, const typet &type=bool_typet());
-  symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type);
-
-
   exprt add_axioms_for_function_application(
     const function_application_exprt &expr);
 
+  symbol_generatort fresh_symbol;
+
+  symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type);
+
   symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type);
 
-  const std::map<exprt, array_string_exprt> &get_arrays_of_pointers() const
-  {
-    return arrays_of_pointers_;
-  }
+  array_poolt array_pool;
 
-  exprt get_length_of_string_array(const array_string_exprt &s) const;
+  /// Associate array to pointer, and array to length
+  /// \return an expression if the given function application is one of
+  ///   associate pointer and associate length
+  optionalt<exprt>
+  make_array_pointer_association(const function_application_exprt &expr);
 
   // Type used by primitives to signal errors
   const signedbv_typet get_return_code_type()
@@ -99,9 +155,6 @@ class string_constraint_generatort final
   array_string_exprt get_string_expr(const exprt &expr);
   plus_exprt plus_exprt_with_overflow_check(const exprt &op1, const exprt &op2);
 
-  array_string_exprt associate_char_array_to_char_pointer(
-    const exprt &char_pointer,
-    const typet &char_array_type);
 
   static constant_exprt constant_char(int i, const typet &char_type);
 
@@ -349,7 +402,6 @@ class string_constraint_generatort final
   std::map<string_not_contains_constraintt, symbol_exprt> witness;
 private:
   std::set<array_string_exprt> created_strings;
-  unsigned symbol_count=0;
   const messaget message;
 
   std::vector<exprt> lemmas;
@@ -364,12 +416,6 @@ class string_constraint_generatort final
 
   // Pool used for the intern method
   std::map<array_string_exprt, symbol_exprt> intern_of_string;
-
-  // associate arrays to char pointers
-  std::map<exprt, array_string_exprt> arrays_of_pointers_;
-
-  // associate length to arrays of infinite size
-  std::map<array_string_exprt, symbol_exprt> length_of_array_;
 };
 
 exprt is_digit_with_radix(