diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.class new file mode 100644 index 00000000000..7e72b920b4e Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.java new file mode 100644 index 00000000000..aa05e11b84c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/Main.java @@ -0,0 +1,31 @@ +public class Main { + public void contains() { + String str = "abcde"; + assert str.contains("cd"); + } + + public void doesntContain() { + String str = "abcde"; + assert !str.contains("cda"); + } + + public void noprop(String str) { + assert str.contains("cd"); + } + + public void nondetArg(String str) { + assert "dave".contains(str); + } + + public void noPi() { + assert !"dave".contains("π"); + } + + public void pi() { + assert "dave_loves_π".contains("π"); + } + + public void alphanumeric() { + assert "ad672naksd3".contains("72n"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/alphanumeric.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/alphanumeric.desc new file mode 100644 index 00000000000..bdedcbc0df6 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/alphanumeric.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.alphanumeric --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/ConstantEvaluationContains/contains.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/contains.desc new file mode 100644 index 00000000000..78ec5d2688f --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/contains.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.contains --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/ConstantEvaluationContains/doesntContain.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/doesntContain.desc new file mode 100644 index 00000000000..68996343768 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/doesntContain.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.doesntContain --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/ConstantEvaluationContains/noPi.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noPi.desc new file mode 100644 index 00000000000..ea3b279c50c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noPi.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noPi --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/ConstantEvaluationContains/nondetArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc new file mode 100644 index 00000000000..93db2edb075 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/nondetArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nondetArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc new file mode 100644 index 00000000000..27e95eab525 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/noprop.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationContains/pi.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/pi.desc new file mode 100644 index 00000000000..42cc4811a28 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationContains/pi.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.pi --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/ConstantEvaluationEqualsIgnoreCase/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.class new file mode 100644 index 00000000000..c45d60b5ae2 Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.java new file mode 100644 index 00000000000..71ba6076a14 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/Main.java @@ -0,0 +1,49 @@ +public class Main { + public void equals() { + assert "abc".equalsIgnoreCase("ABC"); + } + + public void notEqual() { + assert !"abce".equalsIgnoreCase("ABC"); + } + + public void noprop(String val) { + assert val.equalsIgnoreCase("ABC"); + } + + public void longEquals() { + assert !"abce".equalsIgnoreCase("qwertyuiops"); + } + + public void shortEquals() { + assert !"abce".equalsIgnoreCase("BF"); + } + + public void nondetString(String str) { + assert !str.equalsIgnoreCase("dave"); + } + + public void nondetArg(String str) { + assert !"dave".equalsIgnoreCase(str); + } + + public void pi() { + assert !"π".equalsIgnoreCase("dave"); + } + + public void nonAlpha() { + assert "^£&$1!".equalsIgnoreCase("^£&$1!"); + } + + public void empty() { + assert "".equalsIgnoreCase(""); + } + + public void emptyThis() { + assert !"".equalsIgnoreCase("dave"); + } + + public void emptyArg() { + assert !"dave".equalsIgnoreCase(""); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/empty.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/empty.desc new file mode 100644 index 00000000000..15b1a57602c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/empty.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.empty --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/ConstantEvaluationEqualsIgnoreCase/emptyArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/emptyArg.desc new file mode 100644 index 00000000000..279e22eb4bd --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/emptyArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.emptyArg --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/ConstantEvaluationEqualsIgnoreCase/emptyThis.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/emptyThis.desc new file mode 100644 index 00000000000..7e85f448edb --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/emptyThis.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.emptyThis --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/ConstantEvaluationEqualsIgnoreCase/equals.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/equals.desc new file mode 100644 index 00000000000..c33e7b70399 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/equals.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.equals --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/ConstantEvaluationEqualsIgnoreCase/longEquals.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/longEquals.desc new file mode 100644 index 00000000000..28c88ee03d8 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/longEquals.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.longEquals --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/ConstantEvaluationEqualsIgnoreCase/nonAlpha.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nonAlpha.desc new file mode 100644 index 00000000000..49684c9e415 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nonAlpha.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nonAlpha --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetArg.desc new file mode 100644 index 00000000000..93db2edb075 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nondetArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetString.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetString.desc new file mode 100644 index 00000000000..a59296a5206 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/nondetString.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nondetString --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/noprop.desc new file mode 100644 index 00000000000..27e95eab525 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/noprop.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/notEqual.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/notEqual.desc new file mode 100644 index 00000000000..f6941d4447c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/notEqual.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.notEqual --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/ConstantEvaluationEqualsIgnoreCase/pi.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/pi.desc new file mode 100644 index 00000000000..6e626865b5d --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/pi.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.pi --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/shortEquals.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/shortEquals.desc new file mode 100644 index 00000000000..b0a227bbcd1 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEqualsIgnoreCase/shortEquals.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.shortEquals --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/ConstantEvaluationLastIndexOf/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/Main.class new file mode 100644 index 00000000000..61aea99c2ce Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/Main.java new file mode 100644 index 00000000000..bcc2b402c98 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/Main.java @@ -0,0 +1,26 @@ +public class Main { + public void lastIndexOf() { + String str = "abcabcabc"; + assert str.lastIndexOf("b") == 7; + } + + public void noIndex() { + String str = "abcabcabc"; + assert str.lastIndexOf("g") == -1; + } + + public void noprop(String str) { + assert str.lastIndexOf("b") == 7; + } + + public void subsetIndex() { + String str = "abcabcabc"; + assert str.lastIndexOf("b", 5) == 4; + } + + public void subsetNoIndex() { + String str = "abcabcabc"; + assert str.lastIndexOf("c", 1) == -1; + } +} + diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/lastIndexOf.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/lastIndexOf.desc new file mode 100644 index 00000000000..b6dec1fb8b7 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/lastIndexOf.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.lastIndexOf --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/ConstantEvaluationLastIndexOf/noIndex.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/noIndex.desc new file mode 100644 index 00000000000..270d141eb1d --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/noIndex.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noIndex --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/ConstantEvaluationLastIndexOf/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/noprop.desc new file mode 100644 index 00000000000..27e95eab525 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/noprop.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/subsetIndex.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/subsetIndex.desc new file mode 100644 index 00000000000..bf927192f16 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/subsetIndex.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.subsetIndex --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/ConstantEvaluationLastIndexOf/subsetNoIndex.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/subsetNoIndex.desc new file mode 100644 index 00000000000..92e35fbb27a --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationLastIndexOf/subsetNoIndex.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.subsetNoIndex --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/ConstantEvaluationReplace/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/Main.class new file mode 100644 index 00000000000..bdc0dee456f Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/Main.java new file mode 100644 index 00000000000..c729566cc1d --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/Main.java @@ -0,0 +1,90 @@ +public class Main { + public void replace() { + String str = "abded"; + str = str.replace('d', 'c'); + assert str.equals("abcec"); + } + + public void notEqualsReplace() { + String str = "abded"; + str = str.replace('d', 'c'); + assert !str.equals("abdec"); + } + + public void noReplace() { + String str = "abcde"; + str = str.replace('z', 'c'); + assert str.equals("abcde"); + } + + public void randomCharReplace(char b) { + String str = "abcde"; + str = str.replace('a', b); + assert str.equals("abcde"); + } + + public void randomCharsReplace(char a, char b) { + String str = "abcde"; + str = str.replace(a, b); + assert str.equals("abcde"); + } + + public void nopropReplace(String str) { + str = str.replace('d', 'c'); + assert str.equals("abcec"); + } + + public void stringReplace() { + String str = "abded"; + str = str.replace("d", "c"); + assert str.equals("abcec"); + } + + public void stringNoReplace() { + String str = "abded"; + str = str.replace("f", "c"); + assert str.equals("abded"); + } + + public void stringSmallerReplace() { + String str = "abded"; + str = str.replace("ab", "f"); + assert str.equals("fded"); + } + + public void stringLargerReplace() { + String str = "abded"; + str = str.replace("ab", "fghj"); + assert str.equals("fghjded"); + } + + public void stringMultiReplace() { + String str = "abcdab"; + str = str.replace("ab", "gh"); + assert str.equals("ghcdgh"); + } + + public void stringMultiSmallerReplace() { + String str = "abcdabcd"; + str = str.replace("ab", "z"); + assert str.equals("zcdzcd"); + } + + public void stringMultiLargerReplace() { + String str = "abcdabcd"; + str = str.replace("ab", "zack"); + assert str.equals("zackcdzackcd"); + } + + public void stringFullReplace() { + String str = "abcde"; + str = str.replace("abcde", "ttttt"); + assert str.equals("ttttt"); + } + + public void fullReplace() { + String str = "aaaa"; + str = str.replace('a', 'f'); + assert str.equals("ffff"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/fullReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/fullReplace.desc new file mode 100644 index 00000000000..aadde598aca --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/fullReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.fullReplace --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/ConstantEvaluationReplace/noReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/noReplace.desc new file mode 100644 index 00000000000..633674aef01 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/noReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noReplace --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/ConstantEvaluationReplace/nopropReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/nopropReplace.desc new file mode 100644 index 00000000000..a8f4547b764 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/nopropReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nopropReplace --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/notEqualsReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/notEqualsReplace.desc new file mode 100644 index 00000000000..f139b7e758e --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/notEqualsReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.notEqualsReplace --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/ConstantEvaluationReplace/randomCharReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/randomCharReplace.desc new file mode 100644 index 00000000000..c0ab4f17e7a --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/randomCharReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.randomCharReplace --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/randomCharsReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/randomCharsReplace.desc new file mode 100644 index 00000000000..b58a843ea2e --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/randomCharsReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.randomCharsReplace --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/replace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/replace.desc new file mode 100644 index 00000000000..dd08b815ba7 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/replace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.replace --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/ConstantEvaluationReplace/stringFullReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringFullReplace.desc new file mode 100644 index 00000000000..2101010f54d --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringFullReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.stringFullReplace --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/ConstantEvaluationReplace/stringLargerReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringLargerReplace.desc new file mode 100644 index 00000000000..01f8ce31b9f --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringLargerReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.stringLargerReplace --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/ConstantEvaluationReplace/stringMultiLargerReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringMultiLargerReplace.desc new file mode 100644 index 00000000000..fbdce11d4d5 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringMultiLargerReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.stringMultiLargerReplace --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/ConstantEvaluationReplace/stringMultiReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringMultiReplace.desc new file mode 100644 index 00000000000..50b5ec97b90 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringMultiReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.stringMultiReplace --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/ConstantEvaluationReplace/stringMultiSmallerReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringMultiSmallerReplace.desc new file mode 100644 index 00000000000..92c4ba76c58 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringMultiSmallerReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.stringMultiSmallerReplace --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/ConstantEvaluationReplace/stringNoReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringNoReplace.desc new file mode 100644 index 00000000000..45da3ab26a4 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringNoReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.stringNoReplace --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/ConstantEvaluationReplace/stringReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringReplace.desc new file mode 100644 index 00000000000..c83231fa8f0 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.stringReplace --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/ConstantEvaluationReplace/stringSmallerReplace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringSmallerReplace.desc new file mode 100644 index 00000000000..5fc63dd6be0 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationReplace/stringSmallerReplace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.stringSmallerReplace --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/ConstantEvaluationToLowerCase/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/Main.class new file mode 100644 index 00000000000..65b208f272d Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/Main.java new file mode 100644 index 00000000000..60ad536fd09 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/Main.java @@ -0,0 +1,43 @@ +public class Main { + public void toLower() { + String str = "ABCDE"; + str = str.toLowerCase(); + assert str.equals("abcde"); + } + + public void noLower() { + String str = "ABCDE"; + str = str.toLowerCase(); + assert !str.equals("abcdE"); + } + + public void noprop(String str) { + str = str.toLowerCase(); + assert str.equals("ABCDE"); + } + + public void nondetArg(String str) { + str = "dave".toLowerCase(); + assert !str.equals(str); + } + + public void pi() { + assert "π".toLowerCase().equals("π"); + } + + public void nonAlpha() { + assert "^£&$1!".toLowerCase().equals("^£&$1!"); + } + + public void empty() { + assert "".toLowerCase().equals(""); + } + + public void emptyThis() { + assert !"".toLowerCase().equals("dave"); + } + + public void emptyArg() { + assert !"dave".toLowerCase().equals(""); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/empty.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/empty.desc new file mode 100644 index 00000000000..15b1a57602c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/empty.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.empty --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/ConstantEvaluationToLowerCase/emptyArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/emptyArg.desc new file mode 100644 index 00000000000..279e22eb4bd --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/emptyArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.emptyArg --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/ConstantEvaluationToLowerCase/emptyThis.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/emptyThis.desc new file mode 100644 index 00000000000..7e85f448edb --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/emptyThis.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.emptyThis --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/ConstantEvaluationToLowerCase/noLower.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noLower.desc new file mode 100644 index 00000000000..9fdcf0d49e2 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noLower.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noLower --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/ConstantEvaluationToLowerCase/nonAlpha.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nonAlpha.desc new file mode 100644 index 00000000000..49684c9e415 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nonAlpha.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nonAlpha --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nondetArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nondetArg.desc new file mode 100644 index 00000000000..93db2edb075 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nondetArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nondetArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noprop.desc new file mode 100644 index 00000000000..27e95eab525 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/noprop.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/pi.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/pi.desc new file mode 100644 index 00000000000..cbed1f44433 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/pi.desc @@ -0,0 +1,13 @@ +CORE +Main.class +--function Main.pi --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This is technically wrong (as pi has an uppercase) but our current implementation +only constant props things within the 0 - 128 range due to the tolower/toupper methods +currently being used. If this ever changes to be a true all-character case change, +just modify the test. \ No newline at end of file diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/toLower.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/toLower.desc new file mode 100644 index 00000000000..0a218afeeb9 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/toLower.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.toLower --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/ConstantEvaluationToUpperCase/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/Main.class new file mode 100644 index 00000000000..ca120cd04d5 Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/Main.java new file mode 100644 index 00000000000..c33e55278c1 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/Main.java @@ -0,0 +1,43 @@ +public class Main { + public void toUpper() { + String str = "abcde"; + str = str.toUpperCase(); + assert str.equals("ABCDE"); + } + + public void noUpper() { + String str = "abcde"; + str = str.toUpperCase(); + assert !str.equals("ABCDe"); + } + + public void noprop(String str) { + str = str.toUpperCase(); + assert str.equals("ABCDE"); + } + + public void nondetArg(String str) { + str = "dave".toUpperCase(); + assert !str.equals(str); + } + + public void pi() { + assert "π".toUpperCase().equals("π"); + } + + public void nonAlpha() { + assert "^£&$1!".toUpperCase().equals("^£&$1!"); + } + + public void empty() { + assert "".toLowerCase().equals(""); + } + + public void emptyThis() { + assert !"".toUpperCase().equals("dave"); + } + + public void emptyArg() { + assert !"dave".toUpperCase().equals(""); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/empty.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/empty.desc new file mode 100644 index 00000000000..15b1a57602c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/empty.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.empty --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/ConstantEvaluationToUpperCase/emptyArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/emptyArg.desc new file mode 100644 index 00000000000..279e22eb4bd --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/emptyArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.emptyArg --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/ConstantEvaluationToUpperCase/emptyThis.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/emptyThis.desc new file mode 100644 index 00000000000..7e85f448edb --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/emptyThis.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.emptyThis --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/ConstantEvaluationToUpperCase/noUpper.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noUpper.desc new file mode 100644 index 00000000000..128636cf876 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noUpper.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noUpper --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/ConstantEvaluationToUpperCase/nonAlpha.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nonAlpha.desc new file mode 100644 index 00000000000..49684c9e415 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nonAlpha.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nonAlpha --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nondetArg.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nondetArg.desc new file mode 100644 index 00000000000..93db2edb075 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nondetArg.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.nondetArg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noprop.desc new file mode 100644 index 00000000000..27e95eab525 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/noprop.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/pi.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/pi.desc new file mode 100644 index 00000000000..cbed1f44433 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/pi.desc @@ -0,0 +1,13 @@ +CORE +Main.class +--function Main.pi --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This is technically wrong (as pi has an uppercase) but our current implementation +only constant props things within the 0 - 128 range due to the tolower/toupper methods +currently being used. If this ever changes to be a true all-character case change, +just modify the test. \ No newline at end of file diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/toUpper.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/toUpper.desc new file mode 100644 index 00000000000..151488ea8b1 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/toUpper.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.toUpper --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/ConstantEvaluationTrim/Main.class b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class new file mode 100644 index 00000000000..5c80d03b77f Binary files /dev/null and b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class differ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.java b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.java new file mode 100644 index 00000000000..922bb6da298 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.java @@ -0,0 +1,50 @@ +public class Main { + public void trim() { + String str = " abc "; + str = str.trim(); + assert str.equals("abc"); + } + + public void noTrim() { + String str = " abc "; + str = str.trim(); + assert !str.equals(" abc "); + } + + public void trimLeft() { + String str = " abc"; + str = str.trim(); + assert str.equals("abc"); + } + + public void trimRight() { + String str = "abc "; + str = str.trim(); + assert str.equals("abc"); + } + + public void noprop(String str) { + str = str.trim(); + assert str.equals("abc"); + } + + public void empty() { + String str = "".trim(); + assert str.equals(""); + } + + public void tab() { + String str = " ".trim(); + assert str.equals(""); + } + + public void linebreak() { + String str = "\n".trim(); + assert str.equals(""); + } + + public void middleWhitespace() { + String str = " hello dave ".trim(); + assert str.equals("hello dave"); + } +} diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/empty.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/empty.desc new file mode 100644 index 00000000000..15b1a57602c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/empty.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.empty --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/ConstantEvaluationTrim/linebreak.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/linebreak.desc new file mode 100644 index 00000000000..15b1a57602c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/linebreak.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.empty --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/ConstantEvaluationTrim/middleWhitespace.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/middleWhitespace.desc new file mode 100644 index 00000000000..746e5615c44 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/middleWhitespace.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.middleWhitespace --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/ConstantEvaluationTrim/noTrim.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/noTrim.desc new file mode 100644 index 00000000000..6ec540a6fbc --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/noTrim.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noTrim --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/ConstantEvaluationTrim/noprop.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/noprop.desc new file mode 100644 index 00000000000..27e95eab525 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/noprop.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/tab.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/tab.desc new file mode 100644 index 00000000000..15b1a57602c --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/tab.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.empty --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/ConstantEvaluationTrim/trim.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/trim.desc new file mode 100644 index 00000000000..c4959541902 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/trim.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.trim --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/ConstantEvaluationTrim/trimLeft.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/trimLeft.desc new file mode 100644 index 00000000000..03d390d2752 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/trimLeft.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.trimLeft --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/ConstantEvaluationTrim/trimRight.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/trimRight.desc new file mode 100644 index 00000000000..c6805d6e500 --- /dev/null +++ b/jbmc/regression/jbmc-strings/ConstantEvaluationTrim/trimRight.desc @@ -0,0 +1,9 @@ +CORE +Main.class +--function Main.trimRight --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/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index 49226caefda..491b475deb5 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -207,6 +207,22 @@ bool goto_symext::constant_propagate_assignment_with_side_effects( { return constant_propagate_set_char_at(state, symex_assign, f_l1); } + else if(func_id == ID_cprover_string_trim_func) + { + return constant_propagate_trim(state, symex_assign, f_l1); + } + else if(func_id == ID_cprover_string_to_lower_case_func) + { + return constant_propagate_case_change(state, symex_assign, f_l1, false); + } + else if(func_id == ID_cprover_string_to_upper_case_func) + { + return constant_propagate_case_change(state, symex_assign, f_l1, true); + } + else if(func_id == ID_cprover_string_replace_func) + { + return constant_propagate_replace(state, symex_assign, f_l1); + } } } @@ -922,3 +938,225 @@ bool goto_symext::constant_propagate_set_char_at( return true; } + +bool goto_symext::constant_propagate_case_change( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1, + bool to_upper) +{ + 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 &s = to_string_expr(f_l1.arguments().at(2)); + const auto s_data_opt = try_evaluate_constant_string(state, s.content()); + + if(!s_data_opt) + return false; + + array_exprt string_data = s_data_opt->get(); + + auto &operands = string_data.operands(); + for(auto &operand : operands) + { + auto &constant_value = to_constant_expr(operand); + auto character = numeric_cast_v(constant_value); + + // Can't guarantee matches against non-ASCII characters. + if(character >= 128) + return false; + + if(isalpha(character)) + { + if(to_upper) + { + if(islower(character)) + constant_value = + from_integer(toupper(character), constant_value.type()); + } + else + { + if(isupper(character)) + constant_value = + from_integer(tolower(character), constant_value.type()); + } + } + } + + const constant_exprt new_char_array_length = + from_integer(operands.size(), length_type); + + const array_typet new_char_array_type(char_type, new_char_array_length); + 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; +} + +bool goto_symext::constant_propagate_replace( + 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 &s = to_string_expr(f_l1.arguments().at(2)); + const auto s_data_opt = try_evaluate_constant_string(state, s.content()); + + if(!s_data_opt) + return false; + + auto &new_data = f_l1.arguments().at(4); + auto &old_data = f_l1.arguments().at(3); + + array_exprt characters_to_find(s_data_opt->get().type()); + array_exprt characters_to_replace(s_data_opt->get().type()); + + // Two main ways to perform a replace: characters or strings. + bool is_single_character = new_data.type().id() == ID_unsignedbv && + old_data.type().id() == ID_unsignedbv; + if(is_single_character) + { + const auto new_char_pointer = try_evaluate_constant(state, new_data); + const auto old_char_pointer = try_evaluate_constant(state, old_data); + + if(!new_char_pointer || !old_char_pointer) + { + return {}; + } + + characters_to_find.operands().emplace_back(old_char_pointer->get()); + characters_to_replace.operands().emplace_back(new_char_pointer->get()); + } + else + { + auto &new_char_array = to_string_expr(new_data); + auto &old_char_array = to_string_expr(old_data); + + const auto new_char_array_opt = + try_evaluate_constant_string(state, new_char_array.content()); + + const auto old_char_array_opt = + try_evaluate_constant_string(state, old_char_array.content()); + + if(!new_char_array_opt || !old_char_array_opt) + { + return {}; + } + + characters_to_find = old_char_array_opt->get(); + characters_to_replace = new_char_array_opt->get(); + } + + // Copy data, then do initial search for a replace sequence. + array_exprt existing_data = s_data_opt->get(); + auto found_pattern = std::search( + existing_data.operands().begin(), + existing_data.operands().end(), + characters_to_find.operands().begin(), + characters_to_find.operands().end()); + + // If we've found a match, proceed to perform a replace on all instances. + while(found_pattern != existing_data.operands().end()) + { + // Find the difference between our first/last match iterator. + auto match_end = found_pattern + characters_to_find.operands().size(); + + // Erase them. + found_pattern = existing_data.operands().erase(found_pattern, match_end); + + // Insert our replacement characters, then move the iterator to the end of + // our new sequence. + found_pattern = existing_data.operands().insert( + found_pattern, + characters_to_replace.operands().begin(), + characters_to_replace.operands().end()) + + characters_to_replace.operands().size(); + + // Then search from there for any additional matches. + found_pattern = std::search( + found_pattern, + existing_data.operands().end(), + characters_to_find.operands().begin(), + characters_to_find.operands().end()); + } + + const constant_exprt new_char_array_length = + from_integer(existing_data.operands().size(), length_type); + + const array_typet new_char_array_type(char_type, new_char_array_length); + const array_exprt new_char_array( + std::move(existing_data.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; +} + +bool goto_symext::constant_propagate_trim( + 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 &s = to_string_expr(f_l1.arguments().at(2)); + const auto s_data_opt = try_evaluate_constant_string(state, s.content()); + + if(!s_data_opt) + return false; + + auto is_not_whitespace = [](const exprt &expr) { + auto character = numeric_cast_v(to_constant_expr(expr)); + return character > ' '; + }; + + // Note the points where a trim would trim too. + auto &operands = s_data_opt->get().operands(); + auto end_iter = + std::find_if(operands.rbegin(), operands.rend(), is_not_whitespace); + auto start_iter = + std::find_if(operands.begin(), operands.end(), is_not_whitespace); + + // Then copy in the string with leading/trailing whitespace removed. + // Note: if start_iter == operands.end it means the entire string is + // whitespace, so we'll trim it to be empty anyway. + exprt::operandst new_operands; + if(start_iter != operands.end()) + new_operands = exprt::operandst{start_iter, end_iter.base()}; + + const constant_exprt new_char_array_length = + from_integer(new_operands.size(), length_type); + + const array_typet new_char_array_type(char_type, new_char_array_length); + const array_exprt new_char_array( + std::move(new_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 6f320a01658..316f9530b76 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -657,6 +657,25 @@ class goto_symext symex_assignt &symex_assign, const function_application_exprt &f_l1); + /// Attempt to constant propagate trim operations. + bool constant_propagate_trim( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1); + + /// Attempt to constant propagate case changes, both upper and lower. + bool constant_propagate_case_change( + statet &state, + symex_assignt &symex_assign, + const function_application_exprt &f_l1, + bool to_upper); + + /// Attempt to constant proagate character replacement. + bool constant_propagate_replace( + 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 /// diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 0abfde728e3..8b3665df30b 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -180,6 +180,48 @@ static simplify_exprt::resultt<> simplify_string_endswith( return from_integer(res ? 1 : 0, expr.type()); } +/// Simplify String.contains function when arguments are constant +static simplify_exprt::resultt<> simplify_string_contains( + const function_application_exprt &expr, + const namespacet &ns) +{ + // We want to get both arguments of any starts-with comparison, and + // trace them back to the actual string instance. All variables on the + // way must be constant for us to be sure this will work. + 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.content(), ns); + + if(!first_value_opt) + { + return simplify_exprt::unchanged(expr); + } + + const array_exprt &first_value = first_value_opt->get(); + + const auto second_value_opt = + try_get_string_data_array(second_argument.content(), ns); + + if(!second_value_opt) + { + return simplify_exprt::unchanged(expr); + } + + const array_exprt &second_value = second_value_opt->get(); + + // Is our 'contains' array directly contained in our target. + const bool includes = + std::search( + first_value.operands().begin(), + first_value.operands().end(), + second_value.operands().begin(), + second_value.operands().end()) != first_value.operands().end(); + + return from_integer(includes ? 1 : 0, expr.type()); +} + /// Simplify String.isEmpty function when arguments are constant /// \param expr: the expression to simplify /// \param ns: namespace @@ -256,10 +298,12 @@ static simplify_exprt::resultt<> simplify_string_compare_to( /// /// \param expr: the expression to simplify /// \param ns: namespace +/// \param search_from_end: return the last instead of the first index /// \return: the modified expression or an unchanged expression static simplify_exprt::resultt<> simplify_string_index_of( const function_application_exprt &expr, - const namespacet &ns) + const namespacet &ns, + const bool search_from_end) { std::size_t starting_index = 0; @@ -294,21 +338,19 @@ static simplify_exprt::resultt<> simplify_string_index_of( const array_exprt &s1_data = s1_data_opt->get(); - if(starting_index >= s1_data.operands().size()) + const auto search_string_size = s1_data.operands().size(); + if(starting_index >= search_string_size) { return from_integer(-1, expr.type()); } - // Iterator pointing to the character in the first string at which the second - // string or character was found - exprt::operandst::const_iterator it; - + unsigned long starting_offset = + starting_index > 0 ? (search_string_size - 1) - starting_index : 0; if(can_cast_expr(expr.arguments().at(1))) { // Second argument is a string - const refined_string_exprt &s2 = - to_string_expr(expr.arguments().at(1)); + const refined_string_exprt &s2 = to_string_expr(expr.arguments().at(1)); const auto s2_data_opt = try_get_string_data_array(s2.content(), ns); @@ -319,11 +361,41 @@ static simplify_exprt::resultt<> simplify_string_index_of( const array_exprt &s2_data = s2_data_opt->get(); - it = std::search( - std::next(s1_data.operands().begin(), starting_index), - s1_data.operands().end(), - s2_data.operands().begin(), - s2_data.operands().end()); + // Searching for empty string is a special case and is simply the + // "always found at the first searched position. This needs to take into + // account starting position and if you're starting from the beginning or + // end. + if(s2_data.operands().empty()) + return from_integer( + search_from_end + ? starting_index > 0 ? starting_index : search_string_size + : 0, + expr.type()); + + if(search_from_end) + { + auto end = std::prev(s1_data.operands().end(), starting_offset); + auto it = std::find_end( + s1_data.operands().begin(), + end, + s2_data.operands().begin(), + s2_data.operands().end()); + if(it != end) + return from_integer( + std::distance(s1_data.operands().begin(), it), expr.type()); + } + else + { + auto it = std::search( + std::next(s1_data.operands().begin(), starting_index), + s1_data.operands().end(), + s2_data.operands().begin(), + s2_data.operands().end()); + + if(it != s1_data.operands().end()) + return from_integer( + std::distance(s1_data.operands().begin(), it), expr.type()); + } } else if(expr.arguments().at(1).id() == ID_constant) { @@ -332,33 +404,40 @@ static simplify_exprt::resultt<> simplify_string_index_of( const constant_exprt &c1 = to_constant_expr(expr.arguments().at(1)); const auto c1_val = numeric_cast_v(c1); - auto pred = [&](const exprt &c2) - { + auto pred = [&](const exprt &c2) { const auto c2_val = numeric_cast_v(to_constant_expr(c2)); return c1_val == c2_val; }; - it = std::find_if( - std::next(s1_data.operands().begin(), starting_index), - s1_data.operands().end(), - pred); + if(search_from_end) + { + auto it = std::find_if( + std::next(s1_data.operands().rbegin(), starting_offset), + s1_data.operands().rend(), + pred); + if(it != s1_data.operands().rend()) + return from_integer( + std::distance(s1_data.operands().begin(), it.base() - 1), + expr.type()); + } + else + { + auto it = std::find_if( + std::next(s1_data.operands().begin(), starting_index), + s1_data.operands().end(), + pred); + if(it != s1_data.operands().end()) + return from_integer( + std::distance(s1_data.operands().begin(), it), expr.type()); + } } else { return simplify_exprt::unchanged(expr); } - if(it == s1_data.operands().end()) - { - return from_integer(-1, expr.type()); - } - else - { - const std::size_t idx = std::distance(s1_data.operands().begin(), it); - - return from_integer(idx, expr.type()); - } + return from_integer(-1, expr.type()); } /// Simplify String.charAt function when arguments are constant @@ -405,6 +484,75 @@ static simplify_exprt::resultt<> simplify_string_char_at( return c; } +/// Take the passed-in constant string array and lower-case every character. +static bool lower_case_string_expression(array_exprt &string_data) +{ + auto &operands = string_data.operands(); + for(auto &operand : operands) + { + auto &constant_value = to_constant_expr(operand); + auto character = numeric_cast_v(constant_value); + + // Can't guarantee matches against non-ASCII characters. + if(character >= 128) + return false; + + if(isalpha(character)) + { + if(isupper(character)) + constant_value = + from_integer(tolower(character), constant_value.type()); + } + } + + return true; +} + +/// Simplify String.equalsIgnorecase function when arguments are constant +/// +/// \param expr: the expression to simplify +/// \param ns: namespace +/// \return: the modified expression or an unchanged expression +static simplify_exprt::resultt<> simplify_string_equals_ignore_case( + const function_application_exprt &expr, + const namespacet &ns) +{ + // We want to get both arguments of any starts-with comparison, and + // trace them back to the actual string instance. All variables on the + // way must be constant for us to be sure this will work. + 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.content(), ns); + + if(!first_value_opt) + { + return simplify_exprt::unchanged(expr); + } + + array_exprt first_value = first_value_opt->get(); + + const auto second_value_opt = + try_get_string_data_array(second_argument.content(), ns); + + if(!second_value_opt) + { + return simplify_exprt::unchanged(expr); + } + + array_exprt second_value = second_value_opt->get(); + + // Just lower-case both expressions. + if( + !lower_case_string_expression(first_value) || + !lower_case_string_expression(second_value)) + return simplify_exprt::unchanged(expr); + + bool is_equal = first_value == second_value; + return from_integer(is_equal ? 1 : 0, expr.type()); +} + /// Simplify String.startsWith function when arguments are constant /// /// \param expr: the expression to simplify @@ -504,12 +652,24 @@ simplify_exprt::resultt<> simplify_exprt::simplify_function_application( } else if(func_id == ID_cprover_string_index_of_func) { - return simplify_string_index_of(expr, ns); + return simplify_string_index_of(expr, ns, false); } else if(func_id == ID_cprover_string_char_at_func) { return simplify_string_char_at(expr, ns); } + else if(func_id == ID_cprover_string_contains_func) + { + return simplify_string_contains(expr, ns); + } + else if(func_id == ID_cprover_string_last_index_of_func) + { + return simplify_string_index_of(expr, ns, true); + } + else if(func_id == ID_cprover_string_equals_ignore_case_func) + { + return simplify_string_equals_ignore_case(expr, ns); + } return unchanged(expr); }