Merge pull request #5065 from danpoe/refactor/remove-string-operations-handled-by-models

danpoe · web-flow · commit 57de946bd15c · 2019-09-12T12:15:34.000+01:00
Remove string operations handled by models from string solver
diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library
@@ -1 +1 @@
-Subproject commit ccf0abbed92bf9d5c7ef9ad8efbc45a81e147393
+Subproject commit b5459581cb894990c47712af7f1216d5f4cf9cd2
diff --git a/jbmc/regression/jbmc-strings/StringValueOf01/test.desc b/jbmc/regression/jbmc-strings/StringValueOf01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringValueOf01.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/StringValueOf02/test.desc b/jbmc/regression/jbmc-strings/StringValueOf02/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf02.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/StringValueOf03/test.desc b/jbmc/regression/jbmc-strings/StringValueOf03/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf03.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/StringValueOf04/test.desc b/jbmc/regression/jbmc-strings/StringValueOf04/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf04.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/StringValueOf05/test.desc b/jbmc/regression/jbmc-strings/StringValueOf05/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf05.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/StringValueOf06/test.desc b/jbmc/regression/jbmc-strings/StringValueOf06/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf06.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/StringValueOf07/test.desc b/jbmc/regression/jbmc-strings/StringValueOf07/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf07.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 8 .* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/StringValueOf08/test.desc b/jbmc/regression/jbmc-strings/StringValueOf08/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf08.class
---max-nondet-string-length 100
+--max-nondet-string-length 100 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/StringValueOf09/test.desc b/jbmc/regression/jbmc-strings/StringValueOf09/test.desc
@@ -1,6 +1,6 @@
-CORE
+KNOWNBUG
 StringValueOf09.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/jbmc/regression/jbmc-strings/StringValueOf10/test.desc b/jbmc/regression/jbmc-strings/StringValueOf10/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringValueOf10.class
---max-nondet-string-length 1000
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.checkWithDependency --depth 10000
+--function Test.checkWithDependency --depth 10000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 63 .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.checkDet
+--function Test.checkDet --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 26 .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc
@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.checkNonDet
+--function Test.checkNonDet --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 55 .*: FAILURE
diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc
@@ -1,6 +1,6 @@
 CORE
 Main.class
---function Main.main
+--function Main.main --max-nondet-string-length 10000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1669,26 +1669,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.String.trim:()Ljava/lang/String;"]=
       ID_cprover_string_trim_func;
-  cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]=
-      ID_cprover_string_of_bool_func;
-  cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.String.valueOf:(C)Ljava/lang/String;"]=
-      ID_cprover_string_of_char_func;
-  conversion_table["java::java.lang.String.valueOf:(F)Ljava/lang/String;"] =
-    std::bind(
-      &java_string_library_preprocesst::make_float_to_string_code,
-      this,
-      std::placeholders::_1,
-      std::placeholders::_2,
-      std::placeholders::_3,
-      std::placeholders::_4);
-  cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.String.valueOf:(I)Ljava/lang/String;"]=
-      ID_cprover_string_of_int_func;
-  cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.String.valueOf:(J)Ljava/lang/String;"]=
-      ID_cprover_string_of_long_func;
 
   // StringBuilder library
   conversion_table
@@ -1827,14 +1807,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
       conversion_table["java::java.lang.String.length:()I"];
 
   // Other libraries
-  conversion_table["java::java.lang.Float.toString:(F)Ljava/lang/String;"] =
-    std::bind(
-      &java_string_library_preprocesst::make_float_to_string_code,
-      this,
-      std::placeholders::_1,
-      std::placeholders::_2,
-      std::placeholders::_3,
-      std::placeholders::_4);
   cprover_equivalent_to_java_function
     ["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
       ID_cprover_string_parse_int_func;
@@ -1850,18 +1822,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
       ID_cprover_string_of_int_hex_func;
-  cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.Integer.toString:(I)Ljava/lang/String;"]=
-      ID_cprover_string_of_int_func;
-  cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.Integer.toString:(II)Ljava/lang/String;"]=
-      ID_cprover_string_of_int_func;
-  cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.Long.toString:(J)Ljava/lang/String;"]=
-      ID_cprover_string_of_int_func;
-  cprover_equivalent_to_java_string_returning_function
-    ["java::java.lang.Long.toString:(JI)Ljava/lang/String;"]=
-      ID_cprover_string_of_int_func;
   conversion_table["java::org.cprover.CProver.classIdentifier:("
                    "Ljava/lang/Object;)Ljava/lang/String;"] =
     std::bind(
diff --git a/src/solvers/README.md b/src/solvers/README.md
@@ -499,9 +499,6 @@ This is described in more detail \link string_builtin_functiont here. \endlink
   * `cprover_string_of_float_scientific_notation` :
     \copybrief string_constraint_generatort::add_axioms_from_float_scientific_notation
     \link string_constraint_generatort::add_axioms_from_float_scientific_notation More... \endlink
-  * `cprover_string_of_char` :
-    \copybrief string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f)
-    \link string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) More... \endlink
   * `cprover_string_parse_int` :
     \copybrief string_constraint_generatort::add_axioms_for_parse_int
     \link string_constraint_generatort::add_axioms_for_parse_int More... \endlink
@@ -530,8 +527,6 @@ This is described in more detail \link string_builtin_functiont here. \endlink
   * `cprover_string_delete_char_at` : A call to
     `cprover_string_delete_char_at(s, i)` would be the same thing as
     `cprover_string_delete(s, i, i+1)`.
-  * `cprover_string_of_bool` :
-    Language dependent, should be implemented in the models.
   * `cprover_string_copy` : Same as `cprover_string_substring(s, 0)`.
   * `cprover_string_of_int_hex` : Same as `cprover_string_of_int(s, 16)`.
   * `cprover_string_of_double` : Same as `cprover_string_of_float`.
diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp
@@ -273,10 +273,6 @@ string_constraint_generatort::add_axioms_for_function_application(
     return add_axioms_from_double(expr);
   else if(id == ID_cprover_string_of_long_func)
     return add_axioms_from_long(expr);
-  else if(id == ID_cprover_string_of_bool_func)
-    return add_axioms_from_bool(expr);
-  else if(id == ID_cprover_string_of_char_func)
-    return add_axioms_from_char(expr);
   else if(id == ID_cprover_string_set_length_func)
     return add_axioms_for_set_length(expr);
   else if(id == ID_cprover_string_delete_func)
diff --git a/src/solvers/strings/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp
@@ -55,21 +55,6 @@ string_constraint_generatort::add_axioms_from_long(
     return add_axioms_for_string_of_int(res, f.arguments()[2], 0);
 }
 
-/// Add axioms corresponding to the String.valueOf(Z) java function.
-/// \deprecated This is Java specific and should be implemented in Java instead
-/// \param f: function application with a Boolean argument
-/// \return a new string expression
-DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
-std::pair<exprt, string_constraintst>
-string_constraint_generatort::add_axioms_from_bool(
-  const function_application_exprt &f)
-{
-  PRECONDITION(f.arguments().size() == 3);
-  const array_string_exprt res =
-    array_pool.find(f.arguments()[1], f.arguments()[0]);
-  return add_axioms_from_bool(res, f.arguments()[2]);
-}
-
 /// Add axioms stating that the returned string equals "true" when the Boolean
 /// expression is true and "false" when it is false.
 /// \deprecated This is Java specific and should be implemented in Java instead
@@ -281,44 +266,6 @@ string_constraint_generatort::add_axioms_from_int_hex(
   return add_axioms_from_int_hex(res, f.arguments()[2]);
 }
 
-/// Conversion from char to string
-///
-// NOLINTNEXTLINE
-/// \copybrief add_axioms_from_char(const array_string_exprt &res, const exprt &c)
-// NOLINTNEXTLINE
-/// \link add_axioms_from_char(const array_string_exprt &res, const exprt &c)
-///   (More...) \endlink
-/// \param f: function application with arguments integer `|res|`, character
-///   pointer `&res[0]` and character `c`
-/// \return code 0 on success
-std::pair<exprt, string_constraintst>
-string_constraint_generatort::add_axioms_from_char(
-  const function_application_exprt &f)
-{
-  PRECONDITION(f.arguments().size() == 3);
-  const array_string_exprt res =
-    array_pool.find(f.arguments()[1], f.arguments()[0]);
-  return add_axioms_from_char(res, f.arguments()[2]);
-}
-
-/// Add axiom stating that string `res` has length 1 and the character
-/// it contains equals `c`.
-///
-/// This axiom is: \f$ |{\tt res}| = 1 \land {\tt res}[0] = {\tt c} \f$.
-/// \param res: array of characters expression
-/// \param c: character expression
-/// \return code 0 on success
-std::pair<exprt, string_constraintst>
-string_constraint_generatort::add_axioms_from_char(
-  const array_string_exprt &res,
-  const exprt &c)
-{
-  string_constraintst constraints;
-  constraints.existential = {and_exprt(
-    equal_exprt(res[0], c), equal_to(array_pool.get_or_create_length(res), 1))};
-  return {from_integer(0, get_return_code_type()), std::move(constraints)};
-}
-
 /// Add axioms making the return value true if the given string is a correct
 /// number in the given radix
 /// \param str: string expression
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
@@ -619,11 +619,9 @@ IREP_ID_ONE(cprover_string_length_func)
 IREP_ID_ONE(cprover_string_of_int_func)
 IREP_ID_ONE(cprover_string_of_int_hex_func)
 IREP_ID_ONE(cprover_string_of_long_func)
-IREP_ID_ONE(cprover_string_of_bool_func)
 IREP_ID_ONE(cprover_string_of_float_func)
 IREP_ID_ONE(cprover_string_of_float_scientific_notation_func)
 IREP_ID_ONE(cprover_string_of_double_func)
-IREP_ID_ONE(cprover_string_of_char_func)
 IREP_ID_ONE(cprover_string_parse_int_func)
 IREP_ID_ONE(cprover_string_replace_func)
 IREP_ID_ONE(cprover_string_set_length_func)
