Merge pull request diffblue#1427 from LAJW/feature/string-replace-single-character-strings

String.replace for single-character strings TG-810

Author: smowton

src/java_bytecode/java_string_library_preprocess.cpp

@@ -1944,6 +1944,9 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
       ID_cprover_string_replace_func;
+  cprover_equivalent_to_java_string_returning_function
+    ["java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]= // NOLINT
+      ID_cprover_string_replace_func;
   cprover_equivalent_to_java_function
     ["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
       ID_cprover_string_startswith_func;

src/solvers/refinement/expr_cast.h

@@ -0,0 +1,71 @@
+/*******************************************************************\
+
+Module: exprt conversion functions
+
+Author: Diffblue ltd. All Rights Reserved
+
+\*******************************************************************/
+
+/// \file
+/// Abstraction Refinement Loop
+
+#ifndef CPROVER_SOLVERS_REFINEMENT_EXPR_CAST_H
+#define CPROVER_SOLVERS_REFINEMENT_EXPR_CAST_H
+
+#include <util/optional.h>
+
+/// Convert exprt to a specific type. Remove empty optional if
+/// conversion cannot be performed
+/// Generic case doesn't exist, specialize for different types accordingly
+/// TODO: this should go to util
+template<typename T>
+struct expr_cast_implt final { };
+
+template<>
+struct expr_cast_implt<mp_integer> final
+{
+  optionalt<mp_integer> operator()(const exprt &expr) const
+  {
+    mp_integer out;
+    if(to_integer(expr, out))
+      return {};
+    return out;
+  }
+};
+
+template<>
+struct expr_cast_implt<std::size_t> final
+{
+  optionalt<std::size_t> operator()(const exprt &expr) const
+  {
+    if(const auto tmp=expr_cast_implt<mp_integer>()(expr))
+      if(tmp->is_long() && *tmp>=0)
+        return tmp->to_long();
+    return {};
+  }
+};
+
+template<>
+struct expr_cast_implt<string_exprt> final
+{
+  optionalt<string_exprt> operator()(const exprt &expr) const
+  {
+    if(is_refined_string_type(expr.type()))
+      return to_string_expr(expr);
+    return {};
+  }
+};
+
+template<typename T>
+optionalt<T> expr_cast(const exprt& expr)
+{ return expr_cast_implt<T>()(expr); }
+
+template<typename T>
+T expr_cast_v(const exprt &expr)
+{
+  const auto maybe=expr_cast<T>(expr);
+  INVARIANT(maybe, "Bad conversion");
+  return *maybe;
+}
+
+#endif // CPROVER_SOLVERS_REFINEMENT_EXPR_CAST_H

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -13,6 +13,7 @@ Author: Romain Brenguier, [email protected]
 
 #include <solvers/refinement/string_refinement_invariant.h>
 #include <solvers/refinement/string_constraint_generator.h>
+#include "expr_cast.h"
 
 /// add axioms to say that the returned string expression `res` has length `k`
 /// and characters at position `i` in `res` are equal to the character at
@@ -359,38 +360,70 @@ string_exprt string_constraint_generatort::add_axioms_for_char_set(
   return res;
 }
 
-/// add axioms corresponding to the String.replace java function
-/// \par parameters: function application with three arguments, the first is a
-///   string,
-/// the second and the third are characters
+/// Convert two expressions to pair of chars
+/// If both expressions are characters, return pair of them
+/// If both expressions are 1-length strings, return first character of each
+/// Otherwise return empty optional
+/// \param expr1 First expression
+/// \param expr2 Second expression
+/// \return Optional pair of two expressions
+static optionalt<std::pair<exprt, exprt>> to_char_pair(
+  exprt expr1, exprt expr2)
+{
+  if((expr1.type().id()==ID_unsignedbv
+      || expr1.type().id()==ID_char)
+     && (expr2.type().id()==ID_char
+         || expr2.type().id()==ID_unsignedbv))
+    return std::make_pair(expr1, expr2);
+  const auto expr1_str=to_string_expr(expr1);
+  const auto expr2_str=to_string_expr(expr2);
+  const auto expr1_length=expr_cast<size_t>(expr1_str.length());
+  const auto expr2_length=expr_cast<size_t>(expr2_str.length());
+  if(expr1_length && expr2_length && *expr1_length==1 && *expr2_length==1)
+    return std::make_pair(exprt(expr1_str[0]), exprt(expr2_str[0]));
+  return { };
+}
+
+/// Add axioms corresponding to the String.replace java function
+/// Only supports String.replace(char, char) and
+/// String.replace(String, String) for single-character strings
+/// Returns original string in every other case (that behaviour is to
+/// be fixed in the future)
+/// \param f function application with three arguments, the first is a
+/// string, the second and the third are either pair of characters or
+/// a pair of strings
 /// \return a new string expression
 string_exprt string_constraint_generatort::add_axioms_for_replace(
   const function_application_exprt &f)
 {
   string_exprt str=get_string_expr(args(f, 3)[0]);
   const refined_string_typet &ref_type=to_refined_string_type(str.type());
-  const exprt &old_char=args(f, 3)[1];
-  const exprt &new_char=args(f, 3)[2];
-  string_exprt res=fresh_string(ref_type);
-
-  // We add axioms:
-  // a1 : |res| = |str|
-  // a2 : forall qvar, 0<=qvar<|res|,
-  //    str[qvar]=oldChar => res[qvar]=newChar
-  //    !str[qvar]=oldChar => res[qvar]=str[qvar]
-
-  m_axioms.push_back(res.axiom_for_has_same_length_as(str));
-
-  symbol_exprt qvar=fresh_univ_index("QA_replace", ref_type.get_index_type());
-  implies_exprt case1(
-    equal_exprt(str[qvar], old_char),
-    equal_exprt(res[qvar], new_char));
-  implies_exprt case2(
-    not_exprt(equal_exprt(str[qvar], old_char)),
-    equal_exprt(res[qvar], str[qvar]));
-  string_constraintt a2(qvar, res.length(), and_exprt(case1, case2));
-  m_axioms.push_back(a2);
-  return res;
+  if(const auto maybe_chars=to_char_pair(args(f, 3)[1], args(f, 3)[2]))
+  {
+    const auto old_char=maybe_chars->first;
+    const auto new_char=maybe_chars->second;
+    string_exprt res=fresh_string(ref_type);
+
+    // We add axioms:
+    // a1 : |res| = |str|
+    // a2 : forall qvar, 0<=qvar<|res|,
+    //    str[qvar]=oldChar => res[qvar]=newChar
+    //    !str[qvar]=oldChar => res[qvar]=str[qvar]
+
+    m_axioms.push_back(res.axiom_for_has_same_length_as(str));
+
+    symbol_exprt qvar=fresh_univ_index("QA_replace", ref_type.get_index_type());
+    implies_exprt case1(
+      equal_exprt(str[qvar], old_char),
+      equal_exprt(res[qvar], new_char));
+    implies_exprt case2(
+      not_exprt(equal_exprt(str[qvar], old_char)),
+      equal_exprt(res[qvar], str[qvar]));
+    string_constraintt a2(qvar, res.length(), and_exprt(case1, case2));
+    m_axioms.push_back(a2);
+    return res;
+  }
+  return str;
 }
 
 /// add axioms corresponding to the StringBuilder.deleteCharAt java function

src/solvers/refinement/string_refinement.cpp

@@ -26,6 +26,7 @@ Author: Alberto Griggio, [email protected]
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/string_constraint_instantiation.h>
 #include <java_bytecode/java_types.h>
+#include "expr_cast.h"
 
 static exprt substitute_array_with_expr(const exprt &expr, const exprt &index);
 
@@ -95,63 +96,6 @@ static exprt get_array(
   const std::function<exprt(const exprt &)> &super_get,
   const exprt &arr);
 
-/// Convert exprt to a specific type. Throw bad_cast if conversion
-/// cannot be performed
-/// Generic case doesn't exist, specialize for different types accordingly
-/// TODO: this should go to util
-
-// Tag dispatching struct
-
-template<typename T>
-struct expr_cast_implt final { };
-
-template<>
-struct expr_cast_implt<mp_integer> final
-{
-  optionalt<mp_integer> operator()(const exprt &expr) const
-  {
-    mp_integer out;
-    if(to_integer(expr, out))
-      return {};
-    return out;
-  }
-};
-
-template<>
-struct expr_cast_implt<std::size_t> final
-{
-  optionalt<std::size_t> operator()(const exprt &expr) const
-  {
-    if(const auto tmp=expr_cast_implt<mp_integer>()(expr))
-      if(tmp->is_long() && *tmp>=0)
-        return tmp->to_long();
-    return {};
-  }
-};
-
-template<>
-struct expr_cast_implt<string_exprt> final
-{
-  optionalt<string_exprt> operator()(const exprt &expr) const
-  {
-    if(is_refined_string_type(expr.type()))
-      return to_string_expr(expr);
-    return {};
-  }
-};
-
-template<typename T>
-optionalt<T> expr_cast(const exprt& expr)
-{ return expr_cast_implt<T>()(expr); }
-
-template<typename T>
-T expr_cast_v(const exprt &expr)
-{
-  const auto maybe=expr_cast<T>(expr);
-  INVARIANT(maybe, "Bad conversion");
-  return *maybe;
-}
-
 /// Convert index-value map to a vector of values. If a value for an
 /// index is not defined, set it to the value referenced by the next higher
 /// index. The length of the resulting vector is the key of the map's