diff --git a/jbmc/regression/jbmc-strings/CProverStringToString/Main.class b/jbmc/regression/jbmc-strings/CProverStringToString/Main.class new file mode 100644 index 00000000000..50cbf1cb632 Binary files /dev/null and b/jbmc/regression/jbmc-strings/CProverStringToString/Main.class differ diff --git a/jbmc/regression/jbmc-strings/CProverStringToString/Main.java b/jbmc/regression/jbmc-strings/CProverStringToString/Main.java new file mode 100644 index 00000000000..b6a1ccc40d5 --- /dev/null +++ b/jbmc/regression/jbmc-strings/CProverStringToString/Main.java @@ -0,0 +1,132 @@ +import org.cprover.CProverString; + +class Main { + public void testIntSuccess(int choice) { + int i; + String r; + + switch (choice) { + case 0: + i = 0; + r = "0"; + break; + case 1: + i = 1; + r = "1"; + break; + case 2: + i = -1; + r = "-1"; + break; + case 3: + i = Integer.MIN_VALUE; + r = "-2147483648"; + case 4: + i = Integer.MAX_VALUE; + r = "2147483647"; + default: + return; + } + + String s = CProverString.toString(i); + assert s.equals(r); + } + + public void testIntFailure() { + String s = CProverString.toString(123); + assert s.equals("0"); + } + + public void testLongSuccess(int choice) { + long l; + String r; + + switch (choice) { + case 0: + l = 0L; + r = "0"; + break; + case 1: + l = 1L; + r = "1"; + break; + case 2: + l = -1L; + r = "-1"; + break; + case 3: + l = Long.MIN_VALUE; + ; + r = "-9223372036854775808"; + break; + case 4: + l = Long.MAX_VALUE; + r = "9223372036854775807"; + break; + default: + return; + } + + String s = CProverString.toString(l); + assert s.equals(r); + } + + public void testLongFailure() { + String s = CProverString.toString(9223372036854775807L); + assert s.equals("0"); + } + + public void testFloatSuccess(int choice) { + float f; + String r; + + switch (choice) { + case 0: + f = 0F; + r = "0.0"; + break; + case 1: + f = 1F; + r = "1.0"; + break; + case 2: + f = -1F; + r = "-1.0"; + break; + case 3: + f = 1.1F; + r = "1.1"; + break; + case 4: + f = Float.MAX_VALUE; + r = "3.4028235E38"; + break; + case 5: + f = Float.MIN_VALUE; + r = "1.4E-45"; + break; + case 6: + f = Float.POSITIVE_INFINITY; + r = "Infinity"; + break; + case 7: + f = Float.NEGATIVE_INFINITY; + r = "-Infinity"; + break; + case 8: + f = Float.NaN; + r = "NaN"; + break; + default: + return; + } + + String s = CProverString.toString(f); + assert s.equals(r); + } + + public void testFloatFailure() { + String s = CProverString.toString(1.1F); + assert s.equals("0"); + } +} diff --git a/jbmc/regression/jbmc-strings/CProverStringToString/test_float_fail.desc b/jbmc/regression/jbmc-strings/CProverStringToString/test_float_fail.desc new file mode 100644 index 00000000000..9dd65313c34 --- /dev/null +++ b/jbmc/regression/jbmc-strings/CProverStringToString/test_float_fail.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.testFloatFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/CProverStringToString/test_float_success.desc b/jbmc/regression/jbmc-strings/CProverStringToString/test_float_success.desc new file mode 100644 index 00000000000..568920275e2 --- /dev/null +++ b/jbmc/regression/jbmc-strings/CProverStringToString/test_float_success.desc @@ -0,0 +1,8 @@ +KNOWNBUG +Main.class +--function Main.testFloatSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/CProverStringToString/test_int_fail.desc b/jbmc/regression/jbmc-strings/CProverStringToString/test_int_fail.desc new file mode 100644 index 00000000000..33c9a2324b0 --- /dev/null +++ b/jbmc/regression/jbmc-strings/CProverStringToString/test_int_fail.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.testIntFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/CProverStringToString/test_int_success.desc b/jbmc/regression/jbmc-strings/CProverStringToString/test_int_success.desc new file mode 100644 index 00000000000..6f0de1c4c30 --- /dev/null +++ b/jbmc/regression/jbmc-strings/CProverStringToString/test_int_success.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.testIntSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/CProverStringToString/test_long_fail.desc b/jbmc/regression/jbmc-strings/CProverStringToString/test_long_fail.desc new file mode 100644 index 00000000000..bd3ef8fdc3b --- /dev/null +++ b/jbmc/regression/jbmc-strings/CProverStringToString/test_long_fail.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.testLongFailure --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/CProverStringToString/test_long_success.desc b/jbmc/regression/jbmc-strings/CProverStringToString/test_long_success.desc new file mode 100644 index 00000000000..c5f8638bea7 --- /dev/null +++ b/jbmc/regression/jbmc-strings/CProverStringToString/test_long_success.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.testLongSuccess --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/CharToString/Test.class b/jbmc/regression/jbmc-strings/CharToString/Test.class new file mode 100644 index 00000000000..7fec9c176a2 Binary files /dev/null and b/jbmc/regression/jbmc-strings/CharToString/Test.class differ diff --git a/jbmc/regression/jbmc-strings/CharToString/Test.java b/jbmc/regression/jbmc-strings/CharToString/Test.java new file mode 100644 index 00000000000..5a2e68f2ba1 --- /dev/null +++ b/jbmc/regression/jbmc-strings/CharToString/Test.java @@ -0,0 +1,13 @@ +public class Test { + public void test1() { + char c = '\uFFFF'; + String s = String.valueOf(c); + assert s.equals("\uFFFF"); + } + + public void test2() { + char c = '\uFFFE'; + String s = String.valueOf(c); + assert s.equals("\uFFFE"); + } +} diff --git a/jbmc/regression/jbmc-strings/CharToString/test1.desc b/jbmc/regression/jbmc-strings/CharToString/test1.desc new file mode 100644 index 00000000000..bb497ca3c1b --- /dev/null +++ b/jbmc/regression/jbmc-strings/CharToString/test1.desc @@ -0,0 +1,6 @@ +KNOWNBUG +Test.class +--function Test.test1 --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/CharToString/test2.desc b/jbmc/regression/jbmc-strings/CharToString/test2.desc new file mode 100644 index 00000000000..44a22109795 --- /dev/null +++ b/jbmc/regression/jbmc-strings/CharToString/test2.desc @@ -0,0 +1,6 @@ +CORE +Test.class +--function Test.test2 --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/cprover/CProverString.class b/jbmc/regression/jbmc-strings/cprover/CProverString.class index 8eb78d4aaa4..7ba84c9259a 100644 Binary files a/jbmc/regression/jbmc-strings/cprover/CProverString.class and b/jbmc/regression/jbmc-strings/cprover/CProverString.class differ diff --git a/jbmc/regression/jbmc-strings/cprover/CProverString.java b/jbmc/regression/jbmc-strings/cprover/CProverString.java index 0603aac5dc6..bf84a5b24d9 100644 --- a/jbmc/regression/jbmc-strings/cprover/CProverString.java +++ b/jbmc/regression/jbmc-strings/cprover/CProverString.java @@ -147,4 +147,12 @@ public static StringBuffer insert( StringBuffer sb, int offset, long l) { return sb.insert(offset, l); } + + public static String toString(int i) { return String.valueOf(i); } + + public static String toString(long l) { return String.valueOf(l); } + + public static String toString(float f) { return String.valueOf(f); } + + public static String toString(double d) { return String.valueOf((float)d); } } diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index bf8fbcaaca9..a1a629d6ed0 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1475,6 +1475,93 @@ void java_string_library_preprocesst::initialize_conversion_table() // Methods that are not supported here should ultimately have Java models // provided for them in the class-path. + // CProverString library + cprover_equivalent_to_java_assign_and_return_function + ["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/" + "lang/CharSequence;II)" + "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func; + // CProverString.charAt differs from the Java String.charAt in that no + // exception is raised for the out of bounds case. + cprover_equivalent_to_java_function + ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"] = + ID_cprover_string_char_at_func; + cprover_equivalent_to_java_function + ["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] = + ID_cprover_string_char_at_func; + cprover_equivalent_to_java_function + ["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] = + ID_cprover_string_code_point_at_func; + cprover_equivalent_to_java_function + ["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] = + ID_cprover_string_code_point_before_func; + cprover_equivalent_to_java_function + ["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] = + ID_cprover_string_code_point_count_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/" + "lang/StringBuffer;"] = ID_cprover_string_delete_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::org.cprover.CProverString.delete:(Ljava/lang/" + "StringBuilder;II)Ljava/lang/StringBuilder;"] = + ID_cprover_string_delete_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/" + "StringBufferI)Ljava/lang/StringBuffer;"] = + ID_cprover_string_delete_char_at_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/" + "StringBuilder;I)Ljava/lang/StringBuilder;"] = + ID_cprover_string_delete_char_at_func; + + std::string format_signature = "java::org.cprover.CProverString.format:("; + for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i) + format_signature += "Ljava/lang/String;"; + format_signature += ")Ljava/lang/String;"; + cprover_equivalent_to_java_string_returning_function[format_signature] = + ID_cprover_string_format_func; + + cprover_equivalent_to_java_assign_and_return_function + ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/" + "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func; + cprover_equivalent_to_java_function + ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/" + "String;II)I"] = ID_cprover_string_offset_by_code_point_func; + cprover_equivalent_to_java_assign_function + ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] = + ID_cprover_string_char_set_func; + cprover_equivalent_to_java_assign_function + ["java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] = + ID_cprover_string_set_length_func; + cprover_equivalent_to_java_string_returning_function + ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/" + "lang/CharSequence;"] = ID_cprover_string_substring_func; + // CProverString.substring differs from the Java String.substring in that no + // exception is raised for the out of bounds case. + cprover_equivalent_to_java_string_returning_function + ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)" + "Ljava/lang/String;"] = ID_cprover_string_substring_func; + cprover_equivalent_to_java_string_returning_function + ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)" + "Ljava/lang/String;"] = ID_cprover_string_substring_func; + cprover_equivalent_to_java_string_returning_function + ["java::org.cprover.CProverString.substring:(Ljava/Lang/" + "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func; + cprover_equivalent_to_java_string_returning_function + ["java::org.cprover.CProverString.toString:(I)Ljava/lang/String;"] = + ID_cprover_string_of_int_func; + cprover_equivalent_to_java_string_returning_function + ["java::org.cprover.CProverString.toString:(J)Ljava/lang/String;"] = + ID_cprover_string_of_long_func; + conversion_table + ["java::org.cprover.CProverString.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); + // String library conversion_table["java::java.lang.String.:(Ljava/lang/String;)V"] = std::bind( @@ -1496,20 +1583,6 @@ void java_string_library_preprocesst::initialize_conversion_table() ["java::java.lang.String.:()V"]= ID_cprover_string_empty_string_func; - // CProverString.charAt differs from the Java String.charAt in that no - // exception is raised for the out of bounds case. - cprover_equivalent_to_java_function - ["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]= - ID_cprover_string_char_at_func; - cprover_equivalent_to_java_function - ["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] = - ID_cprover_string_code_point_at_func; - cprover_equivalent_to_java_function - ["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] = - ID_cprover_string_code_point_before_func; - cprover_equivalent_to_java_function - ["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] = - ID_cprover_string_code_point_count_func; cprover_equivalent_to_java_function ["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]= ID_cprover_string_compare_to_func; @@ -1526,13 +1599,6 @@ void java_string_library_preprocesst::initialize_conversion_table() ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]= ID_cprover_string_equals_ignore_case_func; - std::string format_signature = "java::org.cprover.CProverString.format:("; - for(std::size_t i = 0; i < MAX_FORMAT_ARGS + 1; ++i) - format_signature += "Ljava/lang/String;"; - format_signature += ")Ljava/lang/String;"; - cprover_equivalent_to_java_string_returning_function[format_signature] = - ID_cprover_string_format_func; - cprover_equivalent_to_java_function ["java::java.lang.String.indexOf:(I)I"]= ID_cprover_string_index_of_func; @@ -1567,9 +1633,6 @@ void java_string_library_preprocesst::initialize_conversion_table() std::placeholders::_2, std::placeholders::_3, std::placeholders::_4); - cprover_equivalent_to_java_function - ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/" - "String;II)I"] = ID_cprover_string_offset_by_code_point_func; cprover_equivalent_to_java_string_returning_function ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]= ID_cprover_string_replace_func; @@ -1582,19 +1645,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_function ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]= ID_cprover_string_startswith_func; - cprover_equivalent_to_java_string_returning_function - ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/" - "lang/CharSequence;"] = ID_cprover_string_substring_func; - // CProverString.substring differs from the Java String.substring in that no - // exception is raised for the out of bounds case. - cprover_equivalent_to_java_string_returning_function - ["java::org.cprover.CProverString.substring:(Ljava/lang/String;II)" - "Ljava/lang/String;"]= - ID_cprover_string_substring_func; - cprover_equivalent_to_java_string_returning_function - ["java::org.cprover.CProverString.substring:(Ljava/lang/String;I)" - "Ljava/lang/String;"]= - ID_cprover_string_substring_func; cprover_equivalent_to_java_string_returning_function ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]= ID_cprover_string_to_lower_case_func; @@ -1649,10 +1699,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]= ID_cprover_string_concat_char_func; - cprover_equivalent_to_java_assign_and_return_function - ["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/" - "lang/CharSequence;II)" - "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func; cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)" "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func; @@ -1675,17 +1721,6 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_function ["java::java.lang.StringBuilder.codePointCount:(II)I"]= ID_cprover_string_code_point_count_func; - cprover_equivalent_to_java_assign_and_return_function - ["java::org.cprover.CProverString.delete:(Ljava/lang/" - "StringBuilder;II)Ljava/lang/StringBuilder;"] = - ID_cprover_string_delete_func; - cprover_equivalent_to_java_assign_and_return_function - ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/" - "StringBuilder;I)Ljava/lang/StringBuilder;"] = - ID_cprover_string_delete_char_at_func; - cprover_equivalent_to_java_assign_and_return_function - ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/" - "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func; conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind( &java_string_library_preprocesst::make_string_length_code, this, @@ -1744,9 +1779,6 @@ void java_string_library_preprocesst::initialize_conversion_table() ["java::java.lang.StringBuffer.appendCodePoint:(I)" "Ljava/lang/StringBuffer;"]= ID_cprover_string_concat_code_point_func; - cprover_equivalent_to_java_function - ["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] = - ID_cprover_string_char_at_func; cprover_equivalent_to_java_function ["java::java.lang.StringBuffer.codePointAt:(I)I"]= ID_cprover_string_code_point_at_func; @@ -1756,28 +1788,12 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_function ["java::java.lang.StringBuffer.codePointCount:(II)I"]= ID_cprover_string_code_point_count_func; - cprover_equivalent_to_java_assign_and_return_function - ["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/" - "lang/StringBuffer;"] = ID_cprover_string_delete_func; - cprover_equivalent_to_java_assign_and_return_function - ["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/" - "StringBufferI)Ljava/lang/StringBuffer;"] = - ID_cprover_string_delete_char_at_func; conversion_table ["java::java.lang.StringBuffer.length:()I"]= conversion_table["java::java.lang.String.length:()I"]; - cprover_equivalent_to_java_assign_function - ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] = - ID_cprover_string_char_set_func; - cprover_equivalent_to_java_assign_function - ["java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] = - ID_cprover_string_set_length_func; cprover_equivalent_to_java_string_returning_function ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]= ID_cprover_string_substring_func; - cprover_equivalent_to_java_string_returning_function - ["java::org.cprover.CProverString.substring:(Ljava/Lang/" - "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func; conversion_table ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind( &java_string_library_preprocesst::make_copy_string_code,