Merge pull request #4781 from danpoe/feature/simplify-expression-index-of

danpoe · web-flow · commit 16f63e8c4548 · 2019-07-11T13:11:02.000+01:00
[TG-8284] Expression simplification for indexOf()
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/Main.class b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/Main.class
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/Main.java
@@ -0,0 +1,13 @@
+public class Main {
+    public void constantIndexOf() {
+        String s1 = "abcabc";
+        String s2 = "bc";
+        assert s1.indexOf(s2) == 1;
+        assert s1.indexOf(s2, -10) == 1;
+        assert s1.indexOf("") == 0;
+        assert s1.indexOf(s2, 3) == 4;
+        assert s1.indexOf("cd") == -1;
+        assert s1.indexOf(s2, 10) == -1;
+        assert s1.indexOf("", 10) == -1;
+    }
+}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/test.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation1/test.desc
@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/Main.class b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/Main.class
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/Main.java
@@ -0,0 +1,10 @@
+public class Main {
+    public void constantIndexOf() {
+        String s1 = "abcabc";
+        assert s1.indexOf('b') == 1;
+        assert s1.indexOf('b', -10) == 1;
+        assert s1.indexOf('b', 3) == 4;
+        assert s1.indexOf('d') == -1;
+        assert s1.indexOf('b', 10) == -1;
+    }
+}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/test.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation2/test.desc
@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/Main.class b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/Main.class
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/Main.java
@@ -0,0 +1,6 @@
+public class Main {
+    public void constantIndexOf(String arg) {
+        String s1 = "abcabc";
+        assert s1.indexOf(arg, 10) == -1;
+    }
+}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/test.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation3/test.desc
@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;)V.assertion.1"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/Main.class b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/Main.class
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/Main.java b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/Main.java
@@ -0,0 +1,23 @@
+public class Main {
+    public void constantIndexOf(String s, char c, int i) {
+
+        String s1 = "abcabc";
+        String s2 = "bc";
+
+        assert s1.indexOf(c) == 1;
+        assert s1.indexOf(s) == 1;
+        assert s1.indexOf(c, 1) == 1;
+        assert s1.indexOf(s, 1) == 1;
+
+        assert s.indexOf('a') == 1;
+        assert s.indexOf(s1) == 1;
+        assert s.indexOf('a', 1) == 1;
+        assert s.indexOf(s1, 1) == 1;
+
+        assert s1.indexOf(s, -10) == 1;
+        assert s1.indexOf(c, -10) == 1;
+
+        assert s1.indexOf(s2, i) == 1;
+        assert s1.indexOf('a', i) == 1;
+    }
+}
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test1.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test1.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.1" --show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test10.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test10.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.10" --show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test11.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test11.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.11" --show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test12.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test12.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.12" --show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test2.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test2.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.2" --show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test3.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test3.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.3" --show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test4.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test4.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.4" --show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test5.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test5.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.5" --show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test6.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test6.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.6" --show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test7.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test7.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.7" --show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test8.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test8.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.8" --show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test9.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation4/test9.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.9" --show-vcc
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
@@ -262,6 +262,115 @@ static simplify_exprt::resultt<> simplify_string_compare_to(
     first_shorter ? char1 - char2 : char2 - char1, expr.type());
 }
 
+/// Simplify String.indexOf function when arguments are constant
+///
+/// \param expr: the expression to simplify
+/// \param ns: namespace
+/// \return: the modified expression or an unchanged expression
+static simplify_exprt::resultt<> simplify_string_index_of(
+  const function_application_exprt &expr,
+  const namespacet &ns)
+{
+  std::size_t starting_index = 0;
+
+  // Determine starting index for the comparison (if given)
+  if(expr.arguments().size() == 3)
+  {
+    auto &starting_index_expr = expr.arguments().at(2);
+
+    if(starting_index_expr.id() != ID_constant)
+    {
+      return simplify_exprt::unchanged(expr);
+    }
+
+    const mp_integer idx =
+      numeric_cast_v<mp_integer>(to_constant_expr(starting_index_expr));
+
+    // Negative indices are treated like 0
+    if(idx > 0)
+    {
+      starting_index = numeric_cast_v<std::size_t>(idx);
+    }
+  }
+
+  const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0));
+
+  const auto s1_data_opt = try_get_string_data_array(s1, ns);
+
+  if(!s1_data_opt)
+  {
+    return simplify_exprt::unchanged(expr);
+  }
+
+  const array_exprt &s1_data = s1_data_opt->get();
+
+  if(starting_index >= s1_data.operands().size())
+  {
+    return from_integer(-1, expr.type());
+  }
+
+  // Iterator pointing to the character in the first string at which the second
+  // string or character was found
+  exprt::operandst::const_iterator it;
+
+  if(can_cast_expr<refined_string_exprt>(expr.arguments().at(1)))
+  {
+    // Second argument is a string
+
+    const refined_string_exprt &s2 =
+      to_string_expr(expr.arguments().at(1));
+
+    const auto s2_data_opt = try_get_string_data_array(s2, ns);
+
+    if(!s2_data_opt)
+    {
+      return simplify_exprt::unchanged(expr);
+    }
+
+    const array_exprt &s2_data = s2_data_opt->get();
+
+    it = std::search(
+      std::next(s1_data.operands().begin(), starting_index),
+      s1_data.operands().end(),
+      s2_data.operands().begin(),
+      s2_data.operands().end());
+  }
+  else if(expr.arguments().at(1).id() == ID_constant)
+  {
+    // Second argument is a constant character
+
+    const constant_exprt &c1 = to_constant_expr(expr.arguments().at(1));
+    const auto c1_val = numeric_cast_v<mp_integer>(c1);
+
+    auto pred = [&](const exprt &c2)
+    {
+      const auto c2_val = numeric_cast_v<mp_integer>(to_constant_expr(c2));
+
+      return c1_val == c2_val;
+    };
+
+    it = std::find_if(
+      std::next(s1_data.operands().begin(), starting_index),
+      s1_data.operands().end(),
+      pred);
+  }
+  else
+  {
+    return simplify_exprt::unchanged(expr);
+  }
+
+  if(it == s1_data.operands().end())
+  {
+    return from_integer(-1, expr.type());
+  }
+  else
+  {
+    const std::size_t idx = std::distance(s1_data.operands().begin(), it);
+
+    return from_integer(idx, expr.type());
+  }
+}
+
 simplify_exprt::resultt<> simplify_exprt::simplify_function_application(
   const function_application_exprt &expr)
 {
@@ -345,6 +454,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_function_application(
   {
     return simplify_string_compare_to(expr, ns);
   }
+  else if(func_id == ID_cprover_string_index_of_func)
+  {
+    return simplify_string_index_of(expr, ns);
+  }
   else if(func_id == ID_cprover_string_char_at_func)
   {
     if(expr.arguments().at(1).id() != ID_constant)
diff --git a/src/util/string_expr.h b/src/util/string_expr.h
@@ -173,7 +173,8 @@ inline const refined_string_exprt &to_string_expr(const exprt &expr)
 template <>
 inline bool can_cast_expr<refined_string_exprt>(const exprt &base)
 {
-  return base.id() == ID_struct && base.operands().size() == 2;
+  return base.id() == ID_struct && base.operands().size() == 2 &&
+    is_refined_string_type(base.type());
 }
 
 inline void validate_expr(const refined_string_exprt &x)
