diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.class new file mode 100644 index 00000000000..2564e1c2fa8 Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.java new file mode 100644 index 00000000000..9c25e16e1d8 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/Main.java @@ -0,0 +1,8 @@ +public class Main { + public void test() { + String s1 = "abc"; + String s2 = "xyz"; + String s3 = s1 + s2; + assert s3.equals("abcxyz"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc new file mode 100644 index 00000000000..b945ed1593a --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test --property "java::Main.test:()V.assertion.1" --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/Main.class new file mode 100644 index 00000000000..a8de14739ad Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/Main.java new file mode 100644 index 00000000000..da507dec82d --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/Main.java @@ -0,0 +1,15 @@ +public class Main { + public void test1() { + String s1 = "abc"; + String s2 = "xyz"; + String s3 = s1 + s2; + assert s3.length() == 7; + } + + public void test2() { + String s1 = "abc"; + String s2 = "xyz"; + String s3 = s1 + s2; + assert s3.startsWith("abcdefg"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/test1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/test1.desc new file mode 100644 index 00000000000..fe36f6f408a --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/test1.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.test1 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/test2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/test2.desc new file mode 100644 index 00000000000..edb9bfbeb0d --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation05-VerificationFailure/test2.desc @@ -0,0 +1,8 @@ +CORE +Main.class +--function Main.test2 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.class new file mode 100644 index 00000000000..db71618d67d Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.java new file mode 100644 index 00000000000..28ea730c884 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/Main.java @@ -0,0 +1,9 @@ +public class Main { + public void test() { + String s1 = "ディフ"; + String s2 = "ブルー"; + String s3 = s1 + s2; + assert s3.length() == 6; + assert s3.startsWith("ディフブルー"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc new file mode 100644 index 00000000000..936f1a33c06 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.class new file mode 100644 index 00000000000..9a004221735 Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.java new file mode 100644 index 00000000000..44fe0e729f4 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/Main.java @@ -0,0 +1,9 @@ +public class Main { + public void test() { + String s1 = "\t"; + String s2 = "\\"; + String s3 = s1 + s2; + assert s3.length() == 2; + assert s3.startsWith("\t\\"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/test.desc new file mode 100644 index 00000000000..936f1a33c06 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.class b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.class new file mode 100644 index 00000000000..9e0e12cde7b Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.java b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.java new file mode 100644 index 00000000000..4a6ea40f518 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/Main.java @@ -0,0 +1,9 @@ +public class Main { + public void test() { + StringBuilder sb = new StringBuilder("abc"); + sb.append("xyz"); + String s = sb.toString(); + assert s.length() == 6; + assert s.startsWith("abcxyz"); + } +} diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/test.desc b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/test.desc new file mode 100644 index 00000000000..936f1a33c06 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation1/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.class b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.class new file mode 100644 index 00000000000..0385c410ad7 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.java b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.java new file mode 100644 index 00000000000..9f86462847a --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/Main.java @@ -0,0 +1,25 @@ +public class Main { + public void test1() { + StringBuilder sb1 = new StringBuilder("abc"); + String s2 = ""; + sb1.append(s2); + assert sb1.length() == 3; + assert sb1.toString().startsWith("abc"); + } + + public void test2() { + StringBuilder sb1 = new StringBuilder(); + String s2 = "abc"; + sb1.append(s2); + assert sb1.length() == 3; + assert sb1.toString().startsWith("abc"); + } + + public void test3() { + StringBuilder sb1 = new StringBuilder(); + String s2 = ""; + sb1.append(s2); + assert sb1.length() == 0; + assert sb1.toString().startsWith(""); + } +} diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test1.desc b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test1.desc new file mode 100644 index 00000000000..5d4cb5560c8 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test1.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test1 --property "java::Main.test1:()V.assertion.1" --property "java::Main.test1:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test2.desc b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test2.desc new file mode 100644 index 00000000000..92d3a8b0dab --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test2.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test2 --property "java::Main.test2:()V.assertion.1" --property "java::Main.test2:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test3.desc b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test3.desc new file mode 100644 index 00000000000..1b80407d635 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation2/test3.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test3 --property "java::Main.test3:()V.assertion.1" --property "java::Main.test3:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.class b/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.class new file mode 100644 index 00000000000..4c786819c8c Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.java b/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.java new file mode 100644 index 00000000000..f5f01c587fd --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/Main.java @@ -0,0 +1,8 @@ +public class Main { + public void test() { + StringBuilder sb = new StringBuilder(); + String s = sb.toString(); + assert s.isEmpty(); + assert s.length() == 0; + } +} diff --git a/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/test.desc b/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/test.desc new file mode 100644 index 00000000000..27a6bb0db9b --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderDefaultConstructorConstantEvaluation/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.class b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.class new file mode 100644 index 00000000000..971beaf6f32 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.java b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.java new file mode 100644 index 00000000000..09e47b60040 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/Main.java @@ -0,0 +1,9 @@ +public class Main { + public void test() { + String s1 = "abc"; + String s2 = "xyz"; + String s3 = s1 + s2; + assert s3.length() == 6; + assert s3.startsWith("abcxyz"); + } +} diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/test.desc b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/test.desc new file mode 100644 index 00000000000..936f1a33c06 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation1/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.class b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.class new file mode 100644 index 00000000000..f08a81099b2 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.java b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.java new file mode 100644 index 00000000000..2085a053a50 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/Main.java @@ -0,0 +1,25 @@ +public class Main { + public void test1() { + String s1 = "abc"; + String s2 = ""; + String s3 = s1 + s2; + assert s3.length() == 3; + assert s3.startsWith("abc"); + } + + public void test2() { + String s1 = ""; + String s2 = "abc"; + String s3 = s1 + s2; + assert s3.length() == 3; + assert s3.startsWith("abc"); + } + + public void test3() { + String s1 = ""; + String s2 = ""; + String s3 = s1 + s2; + assert s3.length() == 0; + assert s3.startsWith(""); + } +} diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test1.desc b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test1.desc new file mode 100644 index 00000000000..5d4cb5560c8 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test1.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test1 --property "java::Main.test1:()V.assertion.1" --property "java::Main.test1:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test2.desc b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test2.desc new file mode 100644 index 00000000000..92d3a8b0dab --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test2.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test2 --property "java::Main.test2:()V.assertion.1" --property "java::Main.test2:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test3.desc b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test3.desc new file mode 100644 index 00000000000..1b80407d635 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation2/test3.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test3 --property "java::Main.test3:()V.assertion.1" --property "java::Main.test3:()V.assertion.2" +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/Main.class b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/Main.class new file mode 100644 index 00000000000..2e4b51f8205 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/Main.java b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/Main.java new file mode 100644 index 00000000000..4d9adae3c64 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/Main.java @@ -0,0 +1,10 @@ +public class Main { + public void test1(String s1) { + String s2 = "abc"; + assert (s1 + s2).startsWith("abc"); + } + + public void test2(String s) { assert ("" + s).startsWith("abc"); } + + public void test3(String s) { assert (s + s).startsWith("abc"); } +} diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/test1.desc b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/test1.desc new file mode 100644 index 00000000000..4aceb3941ab --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/test1.desc @@ -0,0 +1,11 @@ +CORE symex-driven-lazy-loading-expected-failure +Main.class +--function Main.test1 --property "java::Main.test1:(Ljava/lang/String;)V.assertion.1" +^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that constant propagation does not happen, since a constant +result cannot be determined from the arguments to `+`. diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/test2.desc b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/test2.desc new file mode 100644 index 00000000000..ab6bff95a99 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/test2.desc @@ -0,0 +1,11 @@ +CORE symex-driven-lazy-loading-expected-failure +Main.class +--function Main.test2 --property "java::Main.test2:(Ljava/lang/String;)V.assertion.1" +^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that constant propagation does not happen, since a constant +result cannot be determined from the arguments to `+`. diff --git a/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/test3.desc b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/test3.desc new file mode 100644 index 00000000000..2483252332e --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation3/test3.desc @@ -0,0 +1,11 @@ +CORE symex-driven-lazy-loading-expected-failure +Main.class +--function Main.test3 --property "java::Main.test3:(Ljava/lang/String;)V.assertion.1" +^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that constant propagation does not happen, since a constant +result cannot be determined from the arguments to `+`. diff --git a/jbmc/regression/jbmc-strings/StringDefaultConstructorConstantEvaluation/Main.class b/jbmc/regression/jbmc-strings/StringDefaultConstructorConstantEvaluation/Main.class new file mode 100644 index 00000000000..3552c3f18f4 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringDefaultConstructorConstantEvaluation/Main.class differ diff --git a/jbmc/regression/jbmc-strings/StringDefaultConstructorConstantEvaluation/Main.java b/jbmc/regression/jbmc-strings/StringDefaultConstructorConstantEvaluation/Main.java new file mode 100644 index 00000000000..3ae54da747d --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringDefaultConstructorConstantEvaluation/Main.java @@ -0,0 +1,7 @@ +public class Main { + public void test() { + String s = new String(); + assert s.isEmpty(); + assert s.startsWith(""); + } +} diff --git a/jbmc/regression/jbmc-strings/StringDefaultConstructorConstantEvaluation/test.desc b/jbmc/regression/jbmc-strings/StringDefaultConstructorConstantEvaluation/test.desc new file mode 100644 index 00000000000..27a6bb0db9b --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringDefaultConstructorConstantEvaluation/test.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.test +^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp index 0a95e7d19ac..f4595e89d76 100644 --- a/jbmc/src/java_bytecode/java_string_literals.cpp +++ b/jbmc/src/java_bytecode/java_string_literals.cpp @@ -15,34 +15,12 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include #include +#include #include #include #include -/// Replace non-alphanumeric characters with `_xx` escapes, where xx are hex -/// digits. Underscores are replaced by `__`. -/// \param to_escape: string to escape -/// \return string with non-alphanumeric characters escaped -static std::string escape_non_alnum(const std::string &to_escape) -{ - std::ostringstream escaped; - for(auto &ch : to_escape) - { - if(ch=='_') - escaped << "__"; - else if(isalnum(ch)) - escaped << ch; - else - escaped << '_' - << std::hex - << std::setfill('0') - << std::setw(2) - << (unsigned int)ch; - } - return escaped.str(); -} - /// Convert UCS-2 or UTF-16 to an array expression. /// \par parameters: `in`: wide string to convert /// \return Returns a Java char array containing the same wchars. diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index 37800249436..171aca2a2ab 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -14,9 +14,18 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr_skeleton.h" #include "symex_assign.h" +#include +#include #include +#include +#include +#include #include #include +#include +#include + +#include unsigned goto_symext::dynamic_counter=0; @@ -87,8 +96,294 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code) if(state.source.pc->source_location.get_hide()) assignment_type = symex_targett::assignment_typet::HIDDEN; + symex_assignt symex_assign{ + state, assignment_type, ns, symex_config, target}; + + // Try to constant propagate potential side effects of the assignment, when + // simplification is turned on and there is one thread only. Constant + // propagation is only sound for sequential code as here we do not take into + // account potential writes from other threads when propagating the values. + if(symex_config.simplify_opt && state.threads.size() <= 1) + { + if(constant_propagate_assignment_with_side_effects( + state, symex_assign, lhs, rhs)) + return; + } + exprt::operandst lhs_if_then_else_conditions; - symex_assignt{state, assignment_type, ns, symex_config, target}.assign_rec( + symex_assign.assign_rec( lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions); } } + +/// Maps the given array expression containing constant characters to a string +/// containing only alphanumeric characters +/// +/// \param char_array: array_exprt containing characters represented by +/// expressions of kind constant_exprt and type unsignedbv_typet or +/// signedbv_typet +/// \return a string containing only alphanumeric characters +static std::string get_alnum_string(const array_exprt &char_array) +{ + const auto &ibv_type = + to_integer_bitvector_type(to_array_type(char_array.type()).subtype()); + + const std::size_t n_bits = ibv_type.get_width(); + CHECK_RETURN(n_bits % 8 == 0); + + static_assert(CHAR_BIT == 8, "bitwidth of char assumed to be 8"); + + const std::size_t n_chars = n_bits / 8; + + INVARIANT( + sizeof(std::size_t) >= n_chars, + "size_t shall be large enough to represent a character"); + + std::string result; + + for(const auto &c : char_array.operands()) + { + const std::size_t c_val = numeric_cast_v(to_constant_expr(c)); + + for(std::size_t i = 0; i < n_chars; i++) + { + const char c_chunk = static_cast((c_val >> (i * 8)) & 0xff); + result.push_back(c_chunk); + } + } + + return escape_non_alnum(result); +} + +bool goto_symext::constant_propagate_assignment_with_side_effects( + statet &state, + symex_assignt &symex_assign, + const exprt &lhs, + const exprt &rhs) +{ + if(rhs.id() == ID_function_application) + { + const function_application_exprt &f_l1 = to_function_application_expr(rhs); + + if(f_l1.function().id() == ID_symbol) + { + const irep_idt &func_id = + to_symbol_expr(f_l1.function()).get_identifier(); + + if(func_id == ID_cprover_string_concat_func) + { + return constant_propagate_string_concat(state, symex_assign, f_l1); + } + else if(func_id == ID_cprover_string_empty_string_func) + { + // constant propagating the empty string always succeeds as it does + // not depend on potentially non-constant inputs + constant_propagate_empty_string(state, symex_assign, f_l1); + return true; + } + } + } + + return false; +} + +void goto_symext::assign_string_constant( + statet &state, + symex_assignt &symex_assign, + const ssa_exprt &length, + const constant_exprt &new_length, + const ssa_exprt &char_array, + const array_exprt &new_char_array) +{ + // assign length of string + symex_assign.assign_symbol(length, expr_skeletont{}, new_length, {}); + + const std::string aux_symbol_name = + get_alnum_string(new_char_array) + "_constant_char_array"; + + const bool string_constant_exists = + state.symbol_table.has_symbol(aux_symbol_name); + + const symbolt &aux_symbol = + string_constant_exists + ? state.symbol_table.lookup_ref(aux_symbol_name) + : get_new_string_data_symbol( + state, symex_assign, aux_symbol_name, char_array, new_char_array); + + INVARIANT( + aux_symbol.value == new_char_array, + "symbol shall have value derived from char array content"); + + const address_of_exprt string_data( + index_exprt(aux_symbol.symbol_expr(), from_integer(0, index_type()))); + + symex_assign.assign_symbol(char_array, expr_skeletont{}, string_data, {}); + + if(!string_constant_exists) + { + associate_array_to_pointer( + state, symex_assign, new_char_array, string_data); + } +} + +const symbolt &goto_symext::get_new_string_data_symbol( + statet &state, + symex_assignt &symex_assign, + const std::string &aux_symbol_name, + const ssa_exprt &char_array, + const array_exprt &new_char_array) +{ + array_typet new_char_array_type = new_char_array.type(); + new_char_array_type.set(ID_C_constant, true); + + symbolt &new_aux_symbol = get_fresh_aux_symbol( + new_char_array_type, + "", + aux_symbol_name, + source_locationt(), + ns.lookup(to_symbol_expr(char_array.get_original_expr())).mode, + ns, + state.symbol_table); + + CHECK_RETURN(new_aux_symbol.is_state_var); + CHECK_RETURN(new_aux_symbol.is_lvalue); + + new_aux_symbol.is_static_lifetime = true; + new_aux_symbol.is_file_local = false; + new_aux_symbol.is_thread_local = false; + + new_aux_symbol.value = new_char_array; + + const exprt arr = state.rename(new_aux_symbol.symbol_expr(), ns).get(); + + symex_assign.assign_symbol( + to_ssa_expr(arr).get_l1_object(), expr_skeletont{}, new_char_array, {}); + + return new_aux_symbol; +} + +void goto_symext::associate_array_to_pointer( + statet &state, + symex_assignt &symex_assign, + const array_exprt &new_char_array, + const address_of_exprt &string_data) +{ + const symbolt &function_symbol = + ns.lookup(ID_cprover_associate_array_to_pointer_func); + + const function_application_exprt array_to_pointer_app{ + function_symbol.symbol_expr(), {new_char_array, string_data}}; + + const symbolt &return_symbol = get_fresh_aux_symbol( + to_mathematical_function_type(function_symbol.type).codomain(), + "", + "return_value", + source_locationt(), + function_symbol.mode, + ns, + state.symbol_table); + + const ssa_exprt ssa_expr(return_symbol.symbol_expr()); + + symex_assign.assign_symbol( + ssa_expr, expr_skeletont{}, array_to_pointer_app, {}); +} + +optionalt> +goto_symext::try_evaluate_constant_string( + const statet &state, + const exprt &content) +{ + if(content.id() != ID_symbol) + { + return {}; + } + + const auto s_pointer_opt = + state.propagation.find(to_symbol_expr(content).get_identifier()); + + if(!s_pointer_opt) + { + return {}; + } + + return try_get_string_data_array(s_pointer_opt->get(), ns); +} + +void goto_symext::constant_propagate_empty_string( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1) +{ + const auto &f_type = to_mathematical_function_type(f_l1.function().type()); + const auto &length_type = f_type.domain().at(0); + const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype(); + + const constant_exprt length = from_integer(0, length_type); + + const array_typet char_array_type(char_type, length); + + DATA_INVARIANT( + f_l1.arguments().size() == 2, + "empty string primitive takes two output arguments"); + + const array_exprt char_array({}, char_array_type); + + assign_string_constant( + state, + symex_assign, + to_ssa_expr(f_l1.arguments().at(0)), + length, + to_ssa_expr(f_l1.arguments().at(1)), + char_array); +} + +bool goto_symext::constant_propagate_string_concat( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1) +{ + const auto &f_type = to_mathematical_function_type(f_l1.function().type()); + const auto &length_type = f_type.domain().at(0); + const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype(); + + const refined_string_exprt &s1 = to_string_expr(f_l1.arguments().at(2)); + const auto s1_data_opt = try_evaluate_constant_string(state, s1.content()); + + if(!s1_data_opt) + return false; + + const array_exprt &s1_data = s1_data_opt->get(); + + const refined_string_exprt &s2 = to_string_expr(f_l1.arguments().at(3)); + const auto s2_data_opt = try_evaluate_constant_string(state, s2.content()); + + if(!s2_data_opt) + return false; + + const array_exprt &s2_data = s2_data_opt->get(); + + const std::size_t new_size = + s1_data.operands().size() + s2_data.operands().size(); + + const constant_exprt new_char_array_length = + from_integer(new_size, length_type); + + const array_typet new_char_array_type(char_type, new_char_array_length); + + exprt::operandst operands(s1_data.operands()); + operands.insert( + operands.end(), s2_data.operands().begin(), s2_data.operands().end()); + + const array_exprt new_char_array(std::move(operands), new_char_array_type); + + assign_string_constant( + state, + symex_assign, + to_ssa_expr(f_l1.arguments().at(0)), + new_char_array_length, + to_ssa_expr(f_l1.arguments().at(1)), + new_char_array); + + return true; +} diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 2896720c127..de1942a02cb 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "path_storage.h" class byte_extract_exprt; +class function_application_exprt; class typet; class code_typet; class symbol_tablet; @@ -33,6 +34,7 @@ class symbol_exprt; class member_exprt; class namespacet; class side_effect_exprt; +class symex_assignt; class typecast_exprt; /// Configuration used for a symbolic execution @@ -528,6 +530,103 @@ class goto_symext /// \param code: The assignment to execute void symex_assign(statet &state, const code_assignt &code); + /// Attempt to constant propagate side effects of the assignment (if any) + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param lhs: lhs of the assignment + /// \param rhs: rhs of the assignment + /// \return true if the operation could be evaluated to a constant string, + /// false otherwise + bool constant_propagate_assignment_with_side_effects( + statet &state, + symex_assignt &symex_assign, + const exprt &lhs, + const exprt &rhs); + + /// Create an empty string constant + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param f_l1: application of function ID_cprover_string_empty_string_func + /// with l1 renaming applied + void constant_propagate_empty_string( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1); + + /// Attempt to constant propagate string concatenation + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param f_l1: application of function ID_cprover_string_concat_func with + /// l1 renaming applied + /// \return true if the operation could be evaluated to a constant string, + /// false otherwise + bool constant_propagate_string_concat( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1); + + /// Assign constant string length and string data given by a char array to + /// given ssa variables + /// + /// A new symbol is created (if not yet existing) in the symbol table to hold + /// the string data given by `new_char_array`. The name of the symbol is + /// derived from the contents of `new_char_array` (e.g., if the array contains + /// "abc", the symbol will be named "abc_constant_char_array"). Then, the + /// expression `&sym[0]` is assigned to `char_array` (assuming `sym` denotes + /// the symbol holding the string data given by `new_char_array`. + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param length: ssa variable to assign the constant string length to + /// \param new_length: value to assign to `length` + /// \param char_array: ssa variable to assign the constant string data to + /// \param new_char_array: constant char array which gives the string data to + /// assign to `char_array` + void assign_string_constant( + statet &state, + symex_assignt &symex_assign, + const ssa_exprt &length, + const constant_exprt &new_length, + const ssa_exprt &char_array, + const array_exprt &new_char_array); + + /// Installs a new symbol in the symbol table to represent the given + /// character array, and assigns the character array to the symbol + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param aux_symbol_name: name of the symbol to create + /// \param char_array: ssa variable to which to assign a pointer to the symbol + /// \param new_char_array: new character array to assign to the symbol + const symbolt &get_new_string_data_symbol( + statet &state, + symex_assignt &symex_assign, + const std::string &aux_symbol_name, + const ssa_exprt &char_array, + const array_exprt &new_char_array); + + /// Generate array to pointer association primitive + /// + /// Executes an assignment `return_value = f(new_char_array, string_data)`, + /// with `new_char_array` being the character array to associate with pointer + /// `string_data` + /// + /// \param state: goto symex state + /// \param symex_assign: object handling symbol assignments + /// \param new_char_array: character array to associate with pointer + /// \param string_data: pointer to associate with character array + void associate_array_to_pointer( + statet &state, + symex_assignt &symex_assign, + const array_exprt &new_char_array, + const address_of_exprt &string_data); + + optionalt> + try_evaluate_constant_string(const statet &state, const exprt &content); + // havocs the given object void havoc_rec(statet &state, const guardt &guard, const exprt &dest); diff --git a/src/solvers/strings/array_pool.cpp b/src/solvers/strings/array_pool.cpp index e454175e555..5289a5f8f9c 100644 --- a/src/solvers/strings/array_pool.cpp +++ b/src/solvers/strings/array_pool.cpp @@ -162,7 +162,10 @@ void array_poolt::insert( INVARIANT( it_bool.second, "should not associate two arrays to the same pointer"); - attempt_assign_length_from_type(array_expr, length_of_array, fresh_symbol); + if(length_of_array.find(array_expr) == length_of_array.end()) + { + attempt_assign_length_from_type(array_expr, length_of_array, fresh_symbol); + } } /// Return a map mapping all array_string_exprt of the array_pool to their diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 7c35a624052..d94c3565a8a 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -64,11 +64,6 @@ struct simplify_expr_cachet simplify_expr_cachet simplify_expr_cache; #endif -static optionalt> -try_get_string_data_array( - const refined_string_exprt &s, - const namespacet &ns); - simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr) { if(expr.op().is_constant()) @@ -163,14 +158,14 @@ static simplify_exprt::resultt<> simplify_string_endswith( const namespacet &ns) { const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0)); - const auto s1_data_opt = try_get_string_data_array(s1, ns); + const auto s1_data_opt = try_get_string_data_array(s1.content(), ns); if(!s1_data_opt) return simplify_exprt::unchanged(expr); const array_exprt &s1_data = s1_data_opt->get(); const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1)); - const auto s2_data_opt = try_get_string_data_array(s2, ns); + const auto s2_data_opt = try_get_string_data_array(s2.content(), ns); if(!s2_data_opt) return simplify_exprt::unchanged(expr); @@ -219,13 +214,13 @@ static simplify_exprt::resultt<> simplify_string_compare_to( const namespacet &ns) { const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0)); - const auto s1_data_opt = try_get_string_data_array(s1, ns); + const auto s1_data_opt = try_get_string_data_array(s1.content(), ns); if(!s1_data_opt) return simplify_exprt::unchanged(expr); const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1)); - const auto s2_data_opt = try_get_string_data_array(s2, ns); + const auto s2_data_opt = try_get_string_data_array(s2.content(), ns); if(!s2_data_opt) return simplify_exprt::unchanged(expr); @@ -290,7 +285,7 @@ static simplify_exprt::resultt<> simplify_string_index_of( const refined_string_exprt &s1 = to_string_expr(expr.arguments().at(0)); - const auto s1_data_opt = try_get_string_data_array(s1, ns); + const auto s1_data_opt = try_get_string_data_array(s1.content(), ns); if(!s1_data_opt) { @@ -315,7 +310,7 @@ static simplify_exprt::resultt<> simplify_string_index_of( const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1)); - const auto s2_data_opt = try_get_string_data_array(s2, ns); + const auto s2_data_opt = try_get_string_data_array(s2.content(), ns); if(!s2_data_opt) { @@ -384,7 +379,7 @@ static simplify_exprt::resultt<> simplify_string_char_at( const refined_string_exprt &s = to_string_expr(expr.arguments().at(0)); - const auto char_seq_opt = try_get_string_data_array(s, ns); + const auto char_seq_opt = try_get_string_data_array(s.content(), ns); if(!char_seq_opt) { @@ -425,7 +420,8 @@ static simplify_exprt::resultt<> simplify_string_startswith( auto &first_argument = to_string_expr(expr.arguments().at(0)); auto &second_argument = to_string_expr(expr.arguments().at(1)); - const auto first_value_opt = try_get_string_data_array(first_argument, ns); + const auto first_value_opt = + try_get_string_data_array(first_argument.content(), ns); if(!first_value_opt) { @@ -434,7 +430,8 @@ static simplify_exprt::resultt<> simplify_string_startswith( const array_exprt &first_value = first_value_opt->get(); - const auto second_value_opt = try_get_string_data_array(second_argument, ns); + const auto second_value_opt = + try_get_string_data_array(second_argument.content(), ns); if(!second_value_opt) { @@ -1670,36 +1667,22 @@ optionalt simplify_exprt::expr2bits( return {}; } -/// Get char sequence from refined string expression -/// -/// If `s.content()` is of the form `&id[e]`, where `id` is an array-typed -/// symbol expression (and `e` is any expression), return the value of the -/// symbol `id` (as given by the `value` field of the symbol in the namespace -/// `ns`); otherwise return an empty optional. -/// -/// \param s: refined string expression -/// \param ns: namespace -/// \return array expression representing the char sequence which forms the -/// content of the refined string expression, empty optional if the content -/// cannot be determined -static optionalt> - try_get_string_data_array( - const refined_string_exprt &s, - const namespacet &ns) +optionalt> +try_get_string_data_array(const exprt &content, const namespacet &ns) { - if(s.content().id() != ID_address_of) + if(content.id() != ID_address_of) { return {}; } - const auto &content = to_address_of_expr(s.content()); + const auto &array_pointer = to_address_of_expr(content); - if(content.object().id() != ID_index) + if(array_pointer.object().id() != ID_index) { return {}; } - const auto &array_start = to_index_expr(content.object()); + const auto &array_start = to_index_expr(array_pointer.object()); if(array_start.array().id() != ID_symbol || array_start.array().type().id() != ID_array) diff --git a/src/util/simplify_expr.h b/src/util/simplify_expr.h index 3f34c0486dd..7035720ab21 100644 --- a/src/util/simplify_expr.h +++ b/src/util/simplify_expr.h @@ -10,8 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_SIMPLIFY_EXPR_H #define CPROVER_UTIL_SIMPLIFY_EXPR_H +class array_exprt; class exprt; class namespacet; +class refined_string_exprt; + +#include // // simplify an expression @@ -27,4 +31,19 @@ bool simplify( // this is the preferred interface exprt simplify_expr(exprt src, const namespacet &ns); +/// Get char sequence from content field of a refined string expression +/// +/// If `content` is of the form `&id[e]`, where `id` is an array-typed symbol +/// expression (and `e` is any expression), return the value of the symbol `id` +/// (as given by the `value` field of the symbol in the namespace `ns`); +/// otherwise return an empty optional. +/// +/// \param content: content field of a refined string expression +/// \param ns: namespace +/// \return array expression representing the char sequence which forms the +/// content of the refined string expression, empty optional if the content +/// cannot be determined +optionalt> +try_get_string_data_array(const exprt &content, const namespacet &ns); + #endif // CPROVER_UTIL_SIMPLIFY_EXPR_H diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp index 68333a414a6..c76ce9820db 100644 --- a/src/util/string_utils.cpp +++ b/src/util/string_utils.cpp @@ -10,9 +10,10 @@ Author: Daniel Poetzl #include "exception_utils.h" #include "invariant.h" +#include #include #include -#include +#include /// Remove all whitespace characters from either end of a string. Whitespace /// in the middle of the string is left unchanged @@ -159,3 +160,19 @@ std::string escape(const std::string &s) return result; } + +std::string escape_non_alnum(const std::string &to_escape) +{ + std::ostringstream escaped; + for(auto &ch : to_escape) + { + if(ch == '_') + escaped << "__"; + else if(isalnum(ch)) + escaped << ch; + else + escaped << '_' << std::hex << std::setfill('0') << std::setw(2) + << (unsigned int)ch; + } + return escaped.str(); +} diff --git a/src/util/string_utils.h b/src/util/string_utils.h index 504c2f3f2b0..278e48b2c71 100644 --- a/src/util/string_utils.h +++ b/src/util/string_utils.h @@ -96,4 +96,10 @@ join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter) /// programming language. std::string escape(const std::string &); +/// Replace non-alphanumeric characters with `_xx` escapes, where xx are hex +/// digits. Underscores are replaced by `__`. +/// \param to_escape: string to escape +/// \return string with non-alphanumeric characters escaped +std::string escape_non_alnum(const std::string &to_escape); + #endif