Merge pull request diffblue#2678 from romainbrenguier/feature/extend-builtin-functions-part3

romainbrenguier · web-flow · commit 318474ff3772 · 2018-08-07T06:38:13.000+01:00
Eval function for string_to_lower/upper_case builtin functions
diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/Test.class b/jbmc/regression/jbmc-strings/StringToLowerCase/Test.class
diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/Test.java b/jbmc/regression/jbmc-strings/StringToLowerCase/Test.java
@@ -0,0 +1,50 @@
+public class Test {
+    public String det()
+    {
+        StringBuilder builder = new StringBuilder();
+        builder.append("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ".toLowerCase());
+        builder.append("abcdeghijklmnopfrstuqwxyzABCDvFGHIJKLMENOPQRSTUVWXYZ".toLowerCase());
+        builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toLowerCase());
+        builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toLowerCase());
+        builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toLowerCase());
+        return builder.toString();
+    }
+
+    public String nonDet(String s)
+    {
+        if(s.length() < 20)
+            return "Short string";
+        if(!s.startsWith("A"))
+            return "String not starting with A";
+
+        StringBuilder builder = new StringBuilder();
+        builder.append(s.toLowerCase());
+        builder.append(s.toLowerCase());
+        builder.append(":");
+        builder.append(s);
+        builder.append(":");
+        builder.append(s.toLowerCase());
+        builder.append(s.toLowerCase());
+        return builder.toString();
+    }
+
+    public String withDependency(String s, boolean b)
+    {
+        // Filter
+        if(s == null || s.length() < 20)
+            return "Short string";
+        if(!s.endsWith("A"))
+            return "String not ending with A";
+
+        // Act
+        String result = s + s.toLowerCase();
+
+        // Assert
+        if(b) {
+            assert(result.endsWith("a"));
+        } else {
+            assert(!result.endsWith("a"));
+        }
+        return result;
+    }
+}
diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc b/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc
@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.withDependency  --verbosity 10 --max-nondet-string-length 10000
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 44 .*: SUCCESS
+assertion at file Test.java line 46 .*: FAILURE
+--
+--
+Check that when there are dependencies, axioms are adde correctly.
diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc b/jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc
@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.det  --verbosity 10 --cover location
+^EXIT=0$
+^SIGNAL=0$
+coverage.* file Test.java line 9 .*: SATISFIED
+--
+adding lemma .*nondet_infinite_array
+--
+Check that using the string dependence informations, no lemma involving arrays is added
diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc b/jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc
@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.nonDet  --verbosity 10 --cover location --max-nondet-string-length 1000
+^EXIT=0$
+^SIGNAL=0$
+coverage.* file Test.java line 27 .*: SATISFIED
+--
+adding lemma .*nondet_infinite_array
+--
+Check that using the string dependence informations, no lemma involving arrays is added
diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/Test.class b/jbmc/regression/jbmc-strings/StringToUpperCase/Test.class
diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/Test.java b/jbmc/regression/jbmc-strings/StringToUpperCase/Test.java
@@ -0,0 +1,50 @@
+public class Test {
+    public String det()
+    {
+        StringBuilder builder = new StringBuilder();
+        builder.append("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ".toLowerCase());
+        builder.append("abcdeghijklmnopfrstuqwxyzABCDvFGHIJKLMENOPQRSTUVWXYZ".toUpperCase());
+        builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toUpperCase());
+        builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toUpperCase());
+        builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toUpperCase());
+        return builder.toString();
+    }
+
+    public String nonDet(String s)
+    {
+        if(s.length() < 20)
+            return "Short string";
+        if(!s.startsWith("a"))
+            return "String not starting with a";
+
+        StringBuilder builder = new StringBuilder();
+        builder.append(s.toUpperCase());
+        builder.append(s.toUpperCase());
+        builder.append(":");
+        builder.append(s);
+        builder.append(":");
+        builder.append(s.toUpperCase());
+        builder.append(s.toUpperCase());
+        return builder.toString();
+    }
+
+    public String withDependency(String s, boolean b)
+    {
+        // Filter
+        if(s == null || s.length() < 20)
+            return "Short string";
+        if(!s.endsWith("a"))
+            return "String not ending with a";
+
+        // Act
+        String result = s + s.toUpperCase();
+
+        // Assert
+        if(b) {
+            assert(result.endsWith("A"));
+        } else {
+            assert(!result.endsWith("A"));
+        }
+        return result;
+    }
+}
diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc b/jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc
@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.withDependency --verbosity 10 --max-nondet-string-length 10000
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 44 .*: SUCCESS
+assertion at file Test.java line 46 .*: FAILURE
+--
+--
+Check that when there are dependencies, axioms are added correctly.
diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc b/jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc
@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.det  --verbosity 10 --cover location
+^EXIT=0$
+^SIGNAL=0$
+coverage.* file Test.java line 9 .*: SATISFIED
+--
+adding lemma .*nondet_infinite_array
+--
+Check that using the string dependence informations, no lemma involving arrays is added
diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc b/jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc
@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.nonDet  --verbosity 10 --cover location --max-nondet-string-length 1000
+^EXIT=0$
+^SIGNAL=0$
+coverage.* file Test.java line 27 .*: SATISFIED
+--
+adding lemma .*nondet_infinite_array
+--
+Check that using the string dependence informations, no lemma involving arrays is added
diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/refinement/string_builtin_function.cpp
@@ -8,7 +8,9 @@
 
 #include "string_constraint_generator.h"
 
-/// Get the valuation of the string, given a valuation
+/// Given a function `get_value` which gives a valuation to expressions, attempt
+/// to find the current value of the array `a`. If the valuation of some
+/// characters are missing, then return an empty optional.
 static optionalt<std::vector<mp_integer>> eval_string(
   const array_string_exprt &a,
   const std::function<exprt(const exprt &)> &get_value);
@@ -187,6 +189,51 @@ exprt string_set_char_builtin_functiont::length_constraint() const
     equal_exprt(return_code, return_value));
 }
 
+static bool eval_is_upper_case(const mp_integer &c)
+{
+  // Characters between 'A' and 'Z' are upper-case
+  // Characters between 0xc0 (latin capital A with grave)
+  // and 0xd6 (latin capital O with diaeresis) are upper-case
+  // Characters between 0xd8 (latin capital O with stroke)
+  // and 0xde (latin capital thorn) are upper-case
+  return ('A' <= c && c <= 'Z') || (0xc0 <= c && c <= 0xd6) ||
+         (0xd8 <= c && c <= 0xde);
+}
+
+optionalt<exprt> string_to_lower_case_builtin_functiont::eval(
+  const std::function<exprt(const exprt &)> &get_value) const
+{
+  auto input_opt = eval_string(input, get_value);
+  if(!input_opt)
+    return {};
+  for(mp_integer &c : input_opt.value())
+  {
+    if(eval_is_upper_case(c))
+      c += 0x20;
+  }
+  const auto length =
+    from_integer(input_opt.value().size(), result.length().type());
+  const array_typet type(result.type().subtype(), length);
+  return make_string(input_opt.value(), type);
+}
+
+optionalt<exprt> string_to_upper_case_builtin_functiont::eval(
+  const std::function<exprt(const exprt &)> &get_value) const
+{
+  auto input_opt = eval_string(input, get_value);
+  if(!input_opt)
+    return {};
+  for(mp_integer &c : input_opt.value())
+  {
+    if(eval_is_upper_case(c - 0x20))
+      c -= 0x20;
+  }
+  const auto length =
+    from_integer(input_opt.value().size(), result.length().type());
+  const array_typet type(result.type().subtype(), length);
+  return make_string(input_opt.value(), type);
+}
+
 std::vector<mp_integer> string_insertion_builtin_functiont::eval(
   const std::vector<mp_integer> &input1_value,
   const std::vector<mp_integer> &input2_value,
diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h
@@ -30,6 +30,10 @@ class string_builtin_functiont
     return {};
   }
 
+  /// Given a function `get_value` which gives a valuation to expressions,
+  /// attempt to find the result of the builtin function.
+  /// If not enough information can be gathered from `get_value`, return an
+  /// empty optional.
   virtual optionalt<exprt>
   eval(const std::function<exprt(const exprt &)> &get_value) const = 0;
 
@@ -177,6 +181,72 @@ class string_set_char_builtin_functiont
   exprt length_constraint() const override;
 };
 
+/// Converting each uppercase character of Basic Latin and Latin-1 supplement
+/// to the corresponding lowercase character.
+class string_to_lower_case_builtin_functiont
+  : public string_transformation_builtin_functiont
+{
+public:
+  string_to_lower_case_builtin_functiont(
+    const exprt &return_code,
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool)
+    : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
+  {
+  }
+
+  optionalt<exprt>
+  eval(const std::function<exprt(const exprt &)> &get_value) const override;
+
+  std::string name() const override
+  {
+    return "to_lower_case";
+  }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    return generator.add_axioms_for_to_lower_case(result, input);
+  };
+
+  exprt length_constraint() const override
+  {
+    return equal_exprt(result.length(), input.length());
+  };
+};
+
+/// Converting each lowercase character of Basic Latin and Latin-1 supplement
+/// to the corresponding uppercase character.
+class string_to_upper_case_builtin_functiont
+  : public string_transformation_builtin_functiont
+{
+public:
+  string_to_upper_case_builtin_functiont(
+    const exprt &return_code,
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool)
+    : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
+  {
+  }
+
+  optionalt<exprt>
+  eval(const std::function<exprt(const exprt &)> &get_value) const override;
+
+  std::string name() const override
+  {
+    return "to_upper_case";
+  }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    return generator.add_axioms_for_to_upper_case(result, input);
+  };
+
+  exprt length_constraint() const override
+  {
+    return equal_exprt(result.length(), input.length());
+  };
+};
+
 /// String inserting a string into another one
 class string_insertion_builtin_functiont : public string_builtin_functiont
 {
diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
@@ -175,6 +175,12 @@ class string_constraint_generatort final
     const array_string_exprt &str,
     const exprt &position,
     const exprt &character);
+  exprt add_axioms_for_to_lower_case(
+    const array_string_exprt &res,
+    const array_string_exprt &str);
+  exprt add_axioms_for_to_upper_case(
+    const array_string_exprt &res,
+    const array_string_exprt &expr);
 
 private:
   symbol_exprt fresh_boolean(const irep_idt &prefix);
@@ -335,9 +341,6 @@ class string_constraint_generatort final
   exprt add_axioms_for_substring(const function_application_exprt &f);
   exprt add_axioms_for_to_lower_case(const function_application_exprt &f);
   exprt add_axioms_for_to_upper_case(const function_application_exprt &f);
-  exprt add_axioms_for_to_upper_case(
-    const array_string_exprt &res,
-    const array_string_exprt &expr);
   exprt add_axioms_for_trim(const function_application_exprt &f);
 
   exprt add_axioms_for_code_point(
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -456,10 +456,6 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
     res=add_axioms_for_compare_to(expr);
   else if(id==ID_cprover_string_literal_func)
     res=add_axioms_from_literal(expr);
-  else if(id==ID_cprover_string_concat_func)
-    res=add_axioms_for_concat(expr);
-  else if(id==ID_cprover_string_concat_char_func)
-    res=add_axioms_for_concat_char(expr);
   else if(id==ID_cprover_string_concat_code_point_func)
     res=add_axioms_for_concat_code_point(expr);
   else if(id==ID_cprover_string_insert_func)
@@ -480,18 +476,10 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
     res=add_axioms_for_substring(expr);
   else if(id==ID_cprover_string_trim_func)
     res=add_axioms_for_trim(expr);
-  else if(id==ID_cprover_string_to_lower_case_func)
-    res=add_axioms_for_to_lower_case(expr);
-  else if(id==ID_cprover_string_to_upper_case_func)
-    res=add_axioms_for_to_upper_case(expr);
-  else if(id==ID_cprover_string_char_set_func)
-    res=add_axioms_for_char_set(expr);
   else if(id==ID_cprover_string_empty_string_func)
     res=add_axioms_for_empty_string(expr);
   else if(id==ID_cprover_string_copy_func)
     res=add_axioms_for_copy(expr);
-  else if(id==ID_cprover_string_of_int_func)
-    res=add_axioms_from_int(expr);
   else if(id==ID_cprover_string_of_int_hex_func)
     res=add_axioms_from_int_hex(expr);
   else if(id==ID_cprover_string_of_float_func)
diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp
diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
