diff --git a/.travis.yml b/.travis.yml index 6af73e31878..e8e19bc01ea 100644 --- a/.travis.yml +++ b/.travis.yml @@ -47,4 +47,4 @@ script: make -C src minisat2-download && make -C src CXX=$COMPILER CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare" -j2 && env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test && - make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 aa-symex.dir cegis.dir clobber.dir memory-models.dir musketeer.dir + make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir diff --git a/regression/cbmc-java/assume1/Assume1.class b/regression/cbmc-java/assume1/Assume1.class new file mode 100644 index 00000000000..b9a49bc9971 Binary files /dev/null and b/regression/cbmc-java/assume1/Assume1.class differ diff --git a/regression/cbmc-java/assume1/Assume1.java b/regression/cbmc-java/assume1/Assume1.java new file mode 100644 index 00000000000..4de0afd025b --- /dev/null +++ b/regression/cbmc-java/assume1/Assume1.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class Assume1 +{ + static void foo(int x) + { + CProver.assume(x>3); + assert x>0; + } +} diff --git a/regression/cbmc-java/assume1/test.desc b/regression/cbmc-java/assume1/test.desc new file mode 100644 index 00000000000..1f80a1c1e86 --- /dev/null +++ b/regression/cbmc-java/assume1/test.desc @@ -0,0 +1,8 @@ +CORE +Assume1.class +--function Assume1.foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/assume2/Assume2.class b/regression/cbmc-java/assume2/Assume2.class new file mode 100644 index 00000000000..36e09875d7d Binary files /dev/null and b/regression/cbmc-java/assume2/Assume2.class differ diff --git a/regression/cbmc-java/assume2/Assume2.java b/regression/cbmc-java/assume2/Assume2.java new file mode 100644 index 00000000000..6991167bfb8 --- /dev/null +++ b/regression/cbmc-java/assume2/Assume2.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class Assume2 +{ + static void foo(int x) + { + CProver.assume(x>3); + assert x>4; + } +} diff --git a/regression/cbmc-java/assume2/test.desc b/regression/cbmc-java/assume2/test.desc new file mode 100644 index 00000000000..35a954116f8 --- /dev/null +++ b/regression/cbmc-java/assume2/test.desc @@ -0,0 +1,8 @@ +CORE +Assume2.class +--function Assume2.foo +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/assume3/Assume3.class b/regression/cbmc-java/assume3/Assume3.class new file mode 100644 index 00000000000..916ad4065fb Binary files /dev/null and b/regression/cbmc-java/assume3/Assume3.class differ diff --git a/regression/cbmc-java/assume3/Assume3.java b/regression/cbmc-java/assume3/Assume3.java new file mode 100644 index 00000000000..895deee9ca0 --- /dev/null +++ b/regression/cbmc-java/assume3/Assume3.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class Assume3 +{ + public static void main(String[] args) + { + CProver.assume(false); + assert false; + } +} diff --git a/regression/cbmc-java/assume3/test.desc b/regression/cbmc-java/assume3/test.desc new file mode 100644 index 00000000000..0ad8c00399f --- /dev/null +++ b/regression/cbmc-java/assume3/test.desc @@ -0,0 +1,8 @@ +CORE +Assume3.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/covered1/covered1.class b/regression/cbmc-java/covered1/covered1.class new file mode 100644 index 00000000000..7cb91496b7d Binary files /dev/null and b/regression/cbmc-java/covered1/covered1.class differ diff --git a/regression/cbmc-java/covered1/covered1.java b/regression/cbmc-java/covered1/covered1.java new file mode 100644 index 00000000000..018e65336a6 --- /dev/null +++ b/regression/cbmc-java/covered1/covered1.java @@ -0,0 +1,37 @@ +public class covered1 +{ + // this is a variable + int x=1; + //these are two, one line off the first + int y=2; + int z=3; + //this is part of static init + static int z0=0; + + //another non-static + int a; + int b; + static boolean odd; + + static + { + odd=(z0+1)%2==0; + } + + covered1(int a, int b) + { + this.a=a*b; + this.b=a+b; + if(this.a==a) + z0++; + else + odd=!odd; + } + // at the back + int z1=2; + int z2=3; + int z3=4; + // + static int z4=5; + int z5=5; +} diff --git a/regression/cbmc-java/covered1/test.desc b/regression/cbmc-java/covered1/test.desc new file mode 100644 index 00000000000..32af766bdb7 --- /dev/null +++ b/regression/cbmc-java/covered1/test.desc @@ -0,0 +1,19 @@ +CORE +covered1.class +--cover location --json-ui --show-properties +^EXIT=0$ +^SIGNAL=0$ +.*\"coveredLines\": \"22\",$ +.*\"coveredLines\": \"4,6,7,23-25,31-33,36\",$ +.*\"coveredLines\": \"26\",$ +.*\"coveredLines\": \"28\",$ +.*\"coveredLines\": \"28\",$ +.*\"coveredLines\": \"28\",$ +.*\"coveredLines\": \"28\",$ +.*\"coveredLines\": \"29\",$ +.*\"coveredLines\": \"9,18\",$ +.*\"coveredLines\": \"18\",$ +.*\"coveredLines\": \"18\",$ +.*\"coveredLines\": \"18,35\",$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/lazyloading1/A.class b/regression/cbmc-java/lazyloading1/A.class new file mode 100644 index 00000000000..d6a62ca1ce4 Binary files /dev/null and b/regression/cbmc-java/lazyloading1/A.class differ diff --git a/regression/cbmc-java/lazyloading1/B.class b/regression/cbmc-java/lazyloading1/B.class new file mode 100644 index 00000000000..2d693bf7383 Binary files /dev/null and b/regression/cbmc-java/lazyloading1/B.class differ diff --git a/regression/cbmc-java/lazyloading1/test.class b/regression/cbmc-java/lazyloading1/test.class new file mode 100644 index 00000000000..25d52a223f4 Binary files /dev/null and b/regression/cbmc-java/lazyloading1/test.class differ diff --git a/regression/cbmc-java/lazyloading1/test.desc b/regression/cbmc-java/lazyloading1/test.desc new file mode 100644 index 00000000000..c0011248128 --- /dev/null +++ b/regression/cbmc-java/lazyloading1/test.desc @@ -0,0 +1,8 @@ +CORE +test.class +--lazy-methods --verbosity 10 --function test.main +^EXIT=0$ +^SIGNAL=0$ +elaborate java::A\.f:\(\)V +-- +elaborate java::B\.g:\(\)V diff --git a/regression/cbmc-java/lazyloading1/test.java b/regression/cbmc-java/lazyloading1/test.java new file mode 100644 index 00000000000..e0686d8c4d0 --- /dev/null +++ b/regression/cbmc-java/lazyloading1/test.java @@ -0,0 +1,21 @@ +// The most basic lazy loading test: A::f is directly called, B::g should be unreachable + +public class test +{ + A a; + B b; + public static void main() + { + A.f(); + } +} + +class A +{ + public static void f() {} +} + +class B +{ + public static void g() {} +} diff --git a/regression/cbmc-java/lazyloading2/A.class b/regression/cbmc-java/lazyloading2/A.class new file mode 100644 index 00000000000..6d789cdb6ec Binary files /dev/null and b/regression/cbmc-java/lazyloading2/A.class differ diff --git a/regression/cbmc-java/lazyloading2/B.class b/regression/cbmc-java/lazyloading2/B.class new file mode 100644 index 00000000000..d9cf49c418f Binary files /dev/null and b/regression/cbmc-java/lazyloading2/B.class differ diff --git a/regression/cbmc-java/lazyloading2/test.class b/regression/cbmc-java/lazyloading2/test.class new file mode 100644 index 00000000000..054809ef0f6 Binary files /dev/null and b/regression/cbmc-java/lazyloading2/test.class differ diff --git a/regression/cbmc-java/lazyloading2/test.desc b/regression/cbmc-java/lazyloading2/test.desc new file mode 100644 index 00000000000..c0011248128 --- /dev/null +++ b/regression/cbmc-java/lazyloading2/test.desc @@ -0,0 +1,8 @@ +CORE +test.class +--lazy-methods --verbosity 10 --function test.main +^EXIT=0$ +^SIGNAL=0$ +elaborate java::A\.f:\(\)V +-- +elaborate java::B\.g:\(\)V diff --git a/regression/cbmc-java/lazyloading2/test.java b/regression/cbmc-java/lazyloading2/test.java new file mode 100644 index 00000000000..b53bae71fa4 --- /dev/null +++ b/regression/cbmc-java/lazyloading2/test.java @@ -0,0 +1,23 @@ +// This test checks that because A is instantiated in main and B is not, +// A::f is reachable and B::g is not + +public class test +{ + A a; + B b; + public static void main() + { + A a = new A(); + a.f(); + } +} + +class A +{ + public void f() {} +} + +class B +{ + public void g() {} +} diff --git a/regression/cbmc-java/lazyloading3/A.class b/regression/cbmc-java/lazyloading3/A.class new file mode 100644 index 00000000000..affb565d625 Binary files /dev/null and b/regression/cbmc-java/lazyloading3/A.class differ diff --git a/regression/cbmc-java/lazyloading3/B.class b/regression/cbmc-java/lazyloading3/B.class new file mode 100644 index 00000000000..9a4ab54d369 Binary files /dev/null and b/regression/cbmc-java/lazyloading3/B.class differ diff --git a/regression/cbmc-java/lazyloading3/C.class b/regression/cbmc-java/lazyloading3/C.class new file mode 100644 index 00000000000..c249e24ace4 Binary files /dev/null and b/regression/cbmc-java/lazyloading3/C.class differ diff --git a/regression/cbmc-java/lazyloading3/D.class b/regression/cbmc-java/lazyloading3/D.class new file mode 100644 index 00000000000..7e16bd6527d Binary files /dev/null and b/regression/cbmc-java/lazyloading3/D.class differ diff --git a/regression/cbmc-java/lazyloading3/test.class b/regression/cbmc-java/lazyloading3/test.class new file mode 100644 index 00000000000..8e470f64650 Binary files /dev/null and b/regression/cbmc-java/lazyloading3/test.class differ diff --git a/regression/cbmc-java/lazyloading3/test.desc b/regression/cbmc-java/lazyloading3/test.desc new file mode 100644 index 00000000000..c0011248128 --- /dev/null +++ b/regression/cbmc-java/lazyloading3/test.desc @@ -0,0 +1,8 @@ +CORE +test.class +--lazy-methods --verbosity 10 --function test.main +^EXIT=0$ +^SIGNAL=0$ +elaborate java::A\.f:\(\)V +-- +elaborate java::B\.g:\(\)V diff --git a/regression/cbmc-java/lazyloading3/test.java b/regression/cbmc-java/lazyloading3/test.java new file mode 100644 index 00000000000..6d3129d1261 --- /dev/null +++ b/regression/cbmc-java/lazyloading3/test.java @@ -0,0 +1,30 @@ +// This test checks that because `main` has a parameter of type C, which has a field of type A, +// A::f is considered reachable, but B::g is not. + +public class test +{ + public static void main(C c) + { + c.a.f(); + } +} + +class A +{ + public void f() {} +} + +class B +{ + public void g() {} +} + +class C +{ + A a; +} + +class D +{ + B b; +} diff --git a/regression/failed-tests-printer.pl b/regression/failed-tests-printer.pl index 832ba2d2c64..40767185d5c 100755 --- a/regression/failed-tests-printer.pl +++ b/regression/failed-tests-printer.pl @@ -4,23 +4,25 @@ open LOG,") { chomp; if (/^Test '(.+)'/) { $current_test = $1; - $ignore = 0; - } elsif (1 == $ignore) { - next; + $printed_this_test = 0; } elsif (/\[FAILED\]\s*$/) { - $ignore = 1; - print "Failed test: $current_test\n"; - my $outf = `sed -n '2p' $current_test/test.desc`; - $outf =~ s/\..*$/.out/; - system("cat $current_test/$outf"); - print "\n\n"; + if(0 == $printed_this_test) { + $printed_this_test = 1; + print "\n\n"; + print "Failed test: $current_test\n"; + my $outf = `sed -n '2p' $current_test/test.desc`; + $outf =~ s/\..*$/.out/; + system("cat $current_test/$outf"); + print "\n\nFailed test.desc lines:\n"; + } + print "$_\n"; } } diff --git a/regression/strings/RegexMatches01/RegexMatches01.class b/regression/strings/RegexMatches01/RegexMatches01.class new file mode 100644 index 00000000000..4006de70b28 Binary files /dev/null and b/regression/strings/RegexMatches01/RegexMatches01.class differ diff --git a/regression/strings/RegexMatches01/RegexMatches01.java b/regression/strings/RegexMatches01/RegexMatches01.java new file mode 100644 index 00000000000..79e05c1432d --- /dev/null +++ b/regression/strings/RegexMatches01/RegexMatches01.java @@ -0,0 +1,25 @@ +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +public class RegexMatches01 +{ + public static void main(String[] args) + { + Pattern expression = + Pattern.compile("W.*\\d[0-35-9]-\\d\\d-\\d\\d"); + + String string1 = "XXXX's Birthday is 05-12-75\n" + + "YYYY's Birthday is 11-04-68\n" + + "ZZZZ's Birthday is 04-28-73\n" + + "WWWW's Birthday is 12-17-77"; + + Matcher matcher = expression.matcher(string1); + + while (matcher.find()) + { + System.out.println(matcher.group()); + String tmp=matcher.group(); + assert tmp.equals("WWWW's Birthday is 12-17-77"); + } + } +} diff --git a/regression/strings/RegexMatches01/test.desc b/regression/strings/RegexMatches01/test.desc new file mode 100644 index 00000000000..45cc542b352 --- /dev/null +++ b/regression/strings/RegexMatches01/test.desc @@ -0,0 +1,8 @@ +FUTURE +RegexMatches01.class +--string-refine --unwind 100 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/RegexMatches02/RegexMatches02.class b/regression/strings/RegexMatches02/RegexMatches02.class new file mode 100644 index 00000000000..d696c5eb047 Binary files /dev/null and b/regression/strings/RegexMatches02/RegexMatches02.class differ diff --git a/regression/strings/RegexMatches02/RegexMatches02.java b/regression/strings/RegexMatches02/RegexMatches02.java new file mode 100644 index 00000000000..634774832c1 --- /dev/null +++ b/regression/strings/RegexMatches02/RegexMatches02.java @@ -0,0 +1,25 @@ +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +public class RegexMatches02 +{ + public static void main(String[] args) + { + Pattern expression = + Pattern.compile("W.*\\d[0-35-9]-\\d\\d-\\d\\d"); + + String string1 = "XXXX's Birthday is 05-12-75\n" + + "YYYY's Birthday is 11-04-68\n" + + "ZZZZ's Birthday is 04-28-73\n" + + "WWWW's Birthday is 12-17-77"; + + Matcher matcher = expression.matcher(string1); + + while (matcher.find()) + { + System.out.println(matcher.group()); + String tmp=matcher.group(); + assert tmp.equals("WWWWW's Birthday is 12-17-77"); + } + } +} diff --git a/regression/strings/RegexMatches02/test.desc b/regression/strings/RegexMatches02/test.desc new file mode 100644 index 00000000000..92d72ae941e --- /dev/null +++ b/regression/strings/RegexMatches02/test.desc @@ -0,0 +1,8 @@ +FUTURE +RegexMatches02.class +--string-refine --unwind 100 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/RegexSubstitution01/RegexSubstitution01.class b/regression/strings/RegexSubstitution01/RegexSubstitution01.class new file mode 100644 index 00000000000..fe4106df4e8 Binary files /dev/null and b/regression/strings/RegexSubstitution01/RegexSubstitution01.class differ diff --git a/regression/strings/RegexSubstitution01/RegexSubstitution01.java b/regression/strings/RegexSubstitution01/RegexSubstitution01.java new file mode 100644 index 00000000000..06b9e7aaa10 --- /dev/null +++ b/regression/strings/RegexSubstitution01/RegexSubstitution01.java @@ -0,0 +1,39 @@ +import java.util.Arrays; + +public class RegexSubstitution01 +{ + public static void main(String[] args) + { + String firstString = "DiffBlue ***"; + String secondString = "Automatic Test Case Generation"; + + firstString = firstString.replaceAll("\\*", "^"); + + assert firstString.equals("DiffBlue ^^^"); + + secondString = secondString.replaceAll("Automatic", "Automated"); + + System.out.printf( + "\"Automatic\" substituted for \"Automated\": %s\n", secondString); + secondString.equals("Automated Test Case Generation"); + + System.out.printf("Every word replaced by \"word\": %s\n\n", + firstString.replaceAll("\\w+", "word")); + + System.out.printf("Original String 2: %s\n", secondString); + secondString.equals("Automated Test Case Generation"); + + for (int i = 0; i < 3; i++) + secondString = secondString.replaceFirst("\\A", "automated"); + + assert secondString.equals("automatedautomatedautomatedAutomated Test Case Generation"); + + System.out.print("String split at commas: "); + String[] results = secondString.split(" \\s*"); + System.out.println(Arrays.toString(results)); + assert results[0].equals("automatedautomatedautomatedAutomated"); + assert results[1].equals("Test"); + assert results[2].equals("Case"); + assert results[3].equals("Generation"); + } +} diff --git a/regression/strings/RegexSubstitution01/test.desc b/regression/strings/RegexSubstitution01/test.desc new file mode 100644 index 00000000000..bc7ed3648f3 --- /dev/null +++ b/regression/strings/RegexSubstitution01/test.desc @@ -0,0 +1,8 @@ +FUTURE +RegexSubstitution01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/RegexSubstitution02/RegexSubstitution02.class b/regression/strings/RegexSubstitution02/RegexSubstitution02.class new file mode 100644 index 00000000000..834c403b3b2 Binary files /dev/null and b/regression/strings/RegexSubstitution02/RegexSubstitution02.class differ diff --git a/regression/strings/RegexSubstitution02/RegexSubstitution02.java b/regression/strings/RegexSubstitution02/RegexSubstitution02.java new file mode 100644 index 00000000000..476c0921553 --- /dev/null +++ b/regression/strings/RegexSubstitution02/RegexSubstitution02.java @@ -0,0 +1,32 @@ +import java.util.Arrays; + +public class RegexSubstitution02 +{ + public static void main(String[] args) + { + String firstString = "DiffBlue ***"; + String secondString = "Automatic Test Case Generation"; + + firstString = firstString.replaceAll("\\*", "^"); + + secondString = secondString.replaceAll("Automatic", "Automated"); + + System.out.printf( + "\"Automatic\" substituted for \"Automated\": %s\n", secondString); + secondString.equals("Automated Test Case Generation"); + + System.out.printf("Every word replaced by \"word\": %s\n\n", + firstString.replaceAll("\\w+", "word")); + + System.out.printf("Original String 2: %s\n", secondString); + secondString.equals("Automated Test Case Generation"); + + for (int i = 0; i < 3; i++) + secondString = secondString.replaceFirst("\\A", "automated"); + + System.out.print("String split at commas: "); + String[] results = secondString.split(" \\s*"); + System.out.println(Arrays.toString(results)); + assert results[0].equals("automatedautomatedautomatedaAutomated"); + } +} diff --git a/regression/strings/RegexSubstitution02/test.desc b/regression/strings/RegexSubstitution02/test.desc new file mode 100644 index 00000000000..eb2c03599a1 --- /dev/null +++ b/regression/strings/RegexSubstitution02/test.desc @@ -0,0 +1,8 @@ +FUTURE +RegexSubstitution02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/RegexSubstitution03/RegexSubstitution03.class b/regression/strings/RegexSubstitution03/RegexSubstitution03.class new file mode 100644 index 00000000000..fa382774918 Binary files /dev/null and b/regression/strings/RegexSubstitution03/RegexSubstitution03.class differ diff --git a/regression/strings/RegexSubstitution03/RegexSubstitution03.java b/regression/strings/RegexSubstitution03/RegexSubstitution03.java new file mode 100644 index 00000000000..9ea91639e2c --- /dev/null +++ b/regression/strings/RegexSubstitution03/RegexSubstitution03.java @@ -0,0 +1,33 @@ +import java.util.Arrays; + +public class RegexSubstitution03 +{ + public static void main(String[] args) + { + String firstString = "DiffBlue ***"; + String secondString = "Automatic Test Case Generation"; + + firstString = firstString.replaceAll("\\*", "^"); + + assert firstString.equals("DiffBlue ^^^"); + + secondString = secondString.replaceAll("Automatic", "Automated"); + + System.out.printf( + "\"Automatic\" substituted for \"Automated\": %s\n", secondString); + secondString.equals("Automated Test Case Generation"); + + System.out.printf("Every word replaced by \"word\": %s\n\n", + firstString.replaceAll("\\w+", "word")); + + System.out.printf("Original String 2: %s\n", secondString); + secondString.equals("Automated Test Case Generation"); + + for (int i = 0; i < 3; i++) + secondString = secondString.replaceFirst("\\A", "automated"); + + System.out.print("String split at commas: "); + String[] results = secondString.split(" \\s*"); + System.out.println(Arrays.toString(results)); + } +} diff --git a/regression/strings/RegexSubstitution03/test.desc b/regression/strings/RegexSubstitution03/test.desc new file mode 100644 index 00000000000..20da1478b1a --- /dev/null +++ b/regression/strings/RegexSubstitution03/test.desc @@ -0,0 +1,8 @@ +FUTURE +RegexSubstitution03.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StaticCharMethods01/StaticCharMethods01.class b/regression/strings/StaticCharMethods01/StaticCharMethods01.class new file mode 100644 index 00000000000..9236c2521e1 Binary files /dev/null and b/regression/strings/StaticCharMethods01/StaticCharMethods01.class differ diff --git a/regression/strings/StaticCharMethods01/StaticCharMethods01.java b/regression/strings/StaticCharMethods01/StaticCharMethods01.java new file mode 100644 index 00000000000..d8e2f9d261b --- /dev/null +++ b/regression/strings/StaticCharMethods01/StaticCharMethods01.java @@ -0,0 +1,16 @@ +public class StaticCharMethods01 +{ + public static void main(String[] args) + { + char c = 0; + assert Character.isDefined(c)==true; + assert Character.isDigit(c)==false; + assert Character.isJavaIdentifierStart(c)==false; + assert Character.isJavaIdentifierPart(c)==true; + assert Character.isLetter(c)==false; + assert Character.isLetterOrDigit(c)==false; + assert Character.isLowerCase(c)==false; + assert Character.isUpperCase(c)==false; + assert Character.toUpperCase(c)==Character.toLowerCase(c); + } +} diff --git a/regression/strings/StaticCharMethods01/test.desc b/regression/strings/StaticCharMethods01/test.desc new file mode 100644 index 00000000000..4b633e92bcf --- /dev/null +++ b/regression/strings/StaticCharMethods01/test.desc @@ -0,0 +1,8 @@ +FUTURE +StaticCharMethods01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StaticCharMethods02/StaticCharMethods02.class b/regression/strings/StaticCharMethods02/StaticCharMethods02.class new file mode 100644 index 00000000000..78ad3dbdc77 Binary files /dev/null and b/regression/strings/StaticCharMethods02/StaticCharMethods02.class differ diff --git a/regression/strings/StaticCharMethods02/StaticCharMethods02.java b/regression/strings/StaticCharMethods02/StaticCharMethods02.java new file mode 100644 index 00000000000..658186e9603 --- /dev/null +++ b/regression/strings/StaticCharMethods02/StaticCharMethods02.java @@ -0,0 +1,8 @@ +public class StaticCharMethods02 +{ + public static void main(String[] args) + { + char c = 0; + assert Character.toUpperCase(c)!=Character.toLowerCase(c); + } +} diff --git a/regression/strings/StaticCharMethods02/test.desc b/regression/strings/StaticCharMethods02/test.desc new file mode 100644 index 00000000000..496814588a7 --- /dev/null +++ b/regression/strings/StaticCharMethods02/test.desc @@ -0,0 +1,8 @@ +FUTURE +StaticCharMethods02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StaticCharMethods03/StaticCharMethods03.class b/regression/strings/StaticCharMethods03/StaticCharMethods03.class new file mode 100644 index 00000000000..264331b2fbe Binary files /dev/null and b/regression/strings/StaticCharMethods03/StaticCharMethods03.class differ diff --git a/regression/strings/StaticCharMethods03/StaticCharMethods03.java b/regression/strings/StaticCharMethods03/StaticCharMethods03.java new file mode 100644 index 00000000000..abc29073402 --- /dev/null +++ b/regression/strings/StaticCharMethods03/StaticCharMethods03.java @@ -0,0 +1,8 @@ +public class StaticCharMethods03 +{ + public static void main(String[] args) + { + char c = 0; + assert Character.isDefined(c)==false; + } +} diff --git a/regression/strings/StaticCharMethods03/test.desc b/regression/strings/StaticCharMethods03/test.desc new file mode 100644 index 00000000000..d48bf57dbba --- /dev/null +++ b/regression/strings/StaticCharMethods03/test.desc @@ -0,0 +1,8 @@ +FUTURE +StaticCharMethods03.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StaticCharMethods04/StaticCharMethods04.class b/regression/strings/StaticCharMethods04/StaticCharMethods04.class new file mode 100644 index 00000000000..6966a3cc557 Binary files /dev/null and b/regression/strings/StaticCharMethods04/StaticCharMethods04.class differ diff --git a/regression/strings/StaticCharMethods04/StaticCharMethods04.java b/regression/strings/StaticCharMethods04/StaticCharMethods04.java new file mode 100644 index 00000000000..70fa2be2f36 --- /dev/null +++ b/regression/strings/StaticCharMethods04/StaticCharMethods04.java @@ -0,0 +1,8 @@ +public class StaticCharMethods04 +{ + public static void main(String[] args) + { + char c = 0; + assert Character.isLetter(c)==true; + } +} diff --git a/regression/strings/StaticCharMethods04/test.desc b/regression/strings/StaticCharMethods04/test.desc new file mode 100644 index 00000000000..93eebbae1da --- /dev/null +++ b/regression/strings/StaticCharMethods04/test.desc @@ -0,0 +1,8 @@ +FUTURE +StaticCharMethods04.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StaticCharMethods05/StaticCharMethods05.class b/regression/strings/StaticCharMethods05/StaticCharMethods05.class new file mode 100644 index 00000000000..c58f3d328af Binary files /dev/null and b/regression/strings/StaticCharMethods05/StaticCharMethods05.class differ diff --git a/regression/strings/StaticCharMethods05/StaticCharMethods05.java b/regression/strings/StaticCharMethods05/StaticCharMethods05.java new file mode 100644 index 00000000000..cffbed129b4 --- /dev/null +++ b/regression/strings/StaticCharMethods05/StaticCharMethods05.java @@ -0,0 +1,33 @@ +import java.util.Scanner; + +public class StaticCharMethods05 +{ + public static void main(String[] args) + { + Scanner scanner = new Scanner(System.in); + + int radix = scanner.nextInt(); + + int choice = scanner.nextInt() % 3; + assert choice>=0 && choice<3; + + switch (choice) + { + case 1: // convert digit to character + System.out.println("Enter a digit:"); + int digit = scanner.nextInt(); + System.out.printf("Convert digit to character: %s\n", + Character.forDigit(digit, radix)); + char tmp=Character.forDigit(digit, radix); + assert tmp=='t'; + break; + + case 2: // convert character to digit + System.out.println("Enter a character:"); + char character = scanner.next().charAt(0); + System.out.printf("Convert character to digit: %s\n", + Character.digit(character, radix)); + break; + } + } +} diff --git a/regression/strings/StaticCharMethods05/test.desc b/regression/strings/StaticCharMethods05/test.desc new file mode 100644 index 00000000000..e009650a853 --- /dev/null +++ b/regression/strings/StaticCharMethods05/test.desc @@ -0,0 +1,8 @@ +FUTURE +StaticCharMethods05.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StaticCharMethods06/StaticCharMethods06.class b/regression/strings/StaticCharMethods06/StaticCharMethods06.class new file mode 100644 index 00000000000..10f416854e6 Binary files /dev/null and b/regression/strings/StaticCharMethods06/StaticCharMethods06.class differ diff --git a/regression/strings/StaticCharMethods06/StaticCharMethods06.java b/regression/strings/StaticCharMethods06/StaticCharMethods06.java new file mode 100644 index 00000000000..ca8ff1604ac --- /dev/null +++ b/regression/strings/StaticCharMethods06/StaticCharMethods06.java @@ -0,0 +1,19 @@ +public class StaticCharMethods06 +{ + public static void main(String[] args) + { + Character c1 = 'A'; + Character c2 = 'A'; + + if (c1.equals(c2)) + { + System.out.println("c1 and c2 are equal\n"); + assert true; + } + else + { + System.out.println("c1 and c2 are not equal\n"); + assert false; + } + } +} diff --git a/regression/strings/StaticCharMethods06/test.desc b/regression/strings/StaticCharMethods06/test.desc new file mode 100644 index 00000000000..6f351b2c7cf --- /dev/null +++ b/regression/strings/StaticCharMethods06/test.desc @@ -0,0 +1,8 @@ +FUTURE +StaticCharMethods06.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderAppend01/StringBuilderAppend01.class b/regression/strings/StringBuilderAppend01/StringBuilderAppend01.class new file mode 100644 index 00000000000..b6202d6fc9a Binary files /dev/null and b/regression/strings/StringBuilderAppend01/StringBuilderAppend01.class differ diff --git a/regression/strings/StringBuilderAppend01/StringBuilderAppend01.java b/regression/strings/StringBuilderAppend01/StringBuilderAppend01.java new file mode 100644 index 00000000000..26e164c02c9 --- /dev/null +++ b/regression/strings/StringBuilderAppend01/StringBuilderAppend01.java @@ -0,0 +1,43 @@ +public class StringBuilderAppend01 +{ + public static void main(String[] args) + { + Object objectRef = "diffblue"; + String string = "test"; + char[] charArray = {'v', 'e', 'r', 'i', 'f', 'i', 'c', 'a', 't', 'i', 'o', 'n'}; + boolean booleanValue = true; + char characterValue = 'Z'; + int integerValue = 7; + long longValue = 10000000000L; + float floatValue = 2.5f; + double doubleValue = 33.333; + + StringBuilder lastBuffer = new StringBuilder("last buffer"); + StringBuilder buffer = new StringBuilder(); + + buffer.append(objectRef) + .append("%n") + .append(string) + .append("%n") + .append(charArray) + .append("%n") + .append(charArray, 0, 3) + .append("%n") + .append(booleanValue) + .append("%n") + .append(characterValue) + .append("%n") + .append(integerValue) + .append("%n") + .append(longValue) + .append("%n") + .append(floatValue) + .append("%n") + .append(doubleValue) + .append("%n") + .append(lastBuffer); + + String tmp=buffer.toString(); + assert tmp.equals("diffblue%ntest%nverification%nver%ntrue%nZ%n7%n10000000000%n2.5%n33.333%nlast buffer"); + } +} diff --git a/regression/strings/StringBuilderAppend01/test.desc b/regression/strings/StringBuilderAppend01/test.desc new file mode 100644 index 00000000000..f1f89b629be --- /dev/null +++ b/regression/strings/StringBuilderAppend01/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderAppend01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderAppend02/StringBuilderAppend02.class b/regression/strings/StringBuilderAppend02/StringBuilderAppend02.class new file mode 100644 index 00000000000..bf07da6a613 Binary files /dev/null and b/regression/strings/StringBuilderAppend02/StringBuilderAppend02.class differ diff --git a/regression/strings/StringBuilderAppend02/StringBuilderAppend02.java b/regression/strings/StringBuilderAppend02/StringBuilderAppend02.java new file mode 100644 index 00000000000..98e0e189c6f --- /dev/null +++ b/regression/strings/StringBuilderAppend02/StringBuilderAppend02.java @@ -0,0 +1,43 @@ +public class StringBuilderAppend02 +{ + public static void main(String[] args) + { + Object objectRef = "diffblue"; + String string = "test"; + char[] charArray = {'v', 'e', 'r', 'i', 'f', 'i', 'c', 'a', 't', 'i', 'o', 'n'}; + boolean booleanValue = true; + char characterValue = 'Z'; + int integerValue = 7; + long longValue = 10000000000L; + float floatValue = 2.5f; + double doubleValue = 33.333; + + StringBuilder lastBuffer = new StringBuilder("last buffer"); + StringBuilder buffer = new StringBuilder(); + + buffer.append(objectRef) + .append("%n") + .append(string) + .append("%n") + .append(charArray) + .append("%n") + .append(charArray, 0, 3) + .append("%n") + .append(booleanValue) + .append("%n") + .append(characterValue) + .append("%n") + .append(integerValue) + .append("%n") + .append(longValue) + .append("%n") + .append(floatValue) + .append("%n") + .append(doubleValue) + .append("%n") + .append(lastBuffer); + + String tmp=buffer.toString(); + assert tmp.equals("diffblue%ntest%nverification%nver%ntrue%n%Z%n7%n10000000000%n2.5%n33.333%nlast buffer"); + } +} diff --git a/regression/strings/StringBuilderAppend02/test.desc b/regression/strings/StringBuilderAppend02/test.desc new file mode 100644 index 00000000000..4ff9da595b5 --- /dev/null +++ b/regression/strings/StringBuilderAppend02/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderAppend02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderCapLen01/StringBuilderCapLen01.class b/regression/strings/StringBuilderCapLen01/StringBuilderCapLen01.class new file mode 100644 index 00000000000..caf6da81f4b Binary files /dev/null and b/regression/strings/StringBuilderCapLen01/StringBuilderCapLen01.class differ diff --git a/regression/strings/StringBuilderCapLen01/StringBuilderCapLen01.java b/regression/strings/StringBuilderCapLen01/StringBuilderCapLen01.java new file mode 100644 index 00000000000..fb9d6e0b0f5 --- /dev/null +++ b/regression/strings/StringBuilderCapLen01/StringBuilderCapLen01.java @@ -0,0 +1,18 @@ +public class StringBuilderCapLen01 +{ + public static void main(String[] args) + { + StringBuilder buffer = new StringBuilder("Diffblue is leader in automatic test case generation"); + + assert buffer.toString().equals("Diffblue is leader in automatic test case generation"); + assert buffer.length()==52; + assert buffer.capacity()==68; + + buffer.ensureCapacity(75); + assert buffer.capacity()==138; + + buffer.setLength(8); + assert buffer.length()==8; + assert buffer.toString().equals("Diffblue"); + } +} diff --git a/regression/strings/StringBuilderCapLen01/test.desc b/regression/strings/StringBuilderCapLen01/test.desc new file mode 100644 index 00000000000..05516f08da2 --- /dev/null +++ b/regression/strings/StringBuilderCapLen01/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderCapLen01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderCapLen02/StringBuilderCapLen02.class b/regression/strings/StringBuilderCapLen02/StringBuilderCapLen02.class new file mode 100644 index 00000000000..ec6949a763f Binary files /dev/null and b/regression/strings/StringBuilderCapLen02/StringBuilderCapLen02.class differ diff --git a/regression/strings/StringBuilderCapLen02/StringBuilderCapLen02.java b/regression/strings/StringBuilderCapLen02/StringBuilderCapLen02.java new file mode 100644 index 00000000000..5397130cde4 --- /dev/null +++ b/regression/strings/StringBuilderCapLen02/StringBuilderCapLen02.java @@ -0,0 +1,8 @@ +public class StringBuilderCapLen02 +{ + public static void main(String[] args) + { + StringBuilder buffer = new StringBuilder("Diffblue is leader in automatic test case generation"); + assert buffer.toString().equals("Diffblue is leader in automatic test case generation"); + } +} diff --git a/regression/strings/StringBuilderCapLen02/test.desc b/regression/strings/StringBuilderCapLen02/test.desc new file mode 100644 index 00000000000..cf2a98acf6d --- /dev/null +++ b/regression/strings/StringBuilderCapLen02/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderCapLen02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderCapLen03/StringBuilderCapLen03.class b/regression/strings/StringBuilderCapLen03/StringBuilderCapLen03.class new file mode 100644 index 00000000000..a14ea26291a Binary files /dev/null and b/regression/strings/StringBuilderCapLen03/StringBuilderCapLen03.class differ diff --git a/regression/strings/StringBuilderCapLen03/StringBuilderCapLen03.java b/regression/strings/StringBuilderCapLen03/StringBuilderCapLen03.java new file mode 100644 index 00000000000..86ac16fcdf6 --- /dev/null +++ b/regression/strings/StringBuilderCapLen03/StringBuilderCapLen03.java @@ -0,0 +1,8 @@ +public class StringBuilderCapLen03 +{ + public static void main(String[] args) + { + StringBuilder buffer = new StringBuilder("Diffblue is leader in automatic test case generation"); + assert buffer.length()==51; + } +} diff --git a/regression/strings/StringBuilderCapLen03/test.desc b/regression/strings/StringBuilderCapLen03/test.desc new file mode 100644 index 00000000000..7095d79fe5f --- /dev/null +++ b/regression/strings/StringBuilderCapLen03/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderCapLen03.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderCapLen04/StringBuilderCapLen04.class b/regression/strings/StringBuilderCapLen04/StringBuilderCapLen04.class new file mode 100644 index 00000000000..7350cb80672 Binary files /dev/null and b/regression/strings/StringBuilderCapLen04/StringBuilderCapLen04.class differ diff --git a/regression/strings/StringBuilderCapLen04/StringBuilderCapLen04.java b/regression/strings/StringBuilderCapLen04/StringBuilderCapLen04.java new file mode 100644 index 00000000000..0ee0492b7bb --- /dev/null +++ b/regression/strings/StringBuilderCapLen04/StringBuilderCapLen04.java @@ -0,0 +1,8 @@ +public class StringBuilderCapLen04 +{ + public static void main(String[] args) + { + StringBuilder buffer = new StringBuilder("Diffblue is leader in automatic test case generation"); + assert buffer.capacity()==69; + } +} diff --git a/regression/strings/StringBuilderCapLen04/test.desc b/regression/strings/StringBuilderCapLen04/test.desc new file mode 100644 index 00000000000..ce51066e789 --- /dev/null +++ b/regression/strings/StringBuilderCapLen04/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderCapLen04.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderChars01/StringBuilderChars01.class b/regression/strings/StringBuilderChars01/StringBuilderChars01.class new file mode 100644 index 00000000000..f2645ec7774 Binary files /dev/null and b/regression/strings/StringBuilderChars01/StringBuilderChars01.class differ diff --git a/regression/strings/StringBuilderChars01/StringBuilderChars01.java b/regression/strings/StringBuilderChars01/StringBuilderChars01.java new file mode 100644 index 00000000000..10265254980 --- /dev/null +++ b/regression/strings/StringBuilderChars01/StringBuilderChars01.java @@ -0,0 +1,28 @@ +public class StringBuilderChars01 +{ + public static void main(String[] args) + { + StringBuilder buffer = new StringBuilder("DiffBlue Limited"); + + assert buffer.toString().equals("DiffBlue Limited"); + assert buffer.charAt(0)!=buffer.charAt(4); + + char[] charArray = new char[buffer.length()]; + buffer.getChars(0, buffer.length(), charArray, 0); + + int i=0; + for (char character : charArray) + { + System.out.print(character); + assert character==buffer.charAt(i); + ++i; + } + + buffer.setCharAt(0, 'H'); + buffer.setCharAt(6, 'T'); + assert buffer.toString().equals("HiffBlTe Limited"); + + buffer.reverse(); + assert buffer.toString().equals("detimiL eTlBffiH"); + } +} diff --git a/regression/strings/StringBuilderChars01/test.desc b/regression/strings/StringBuilderChars01/test.desc new file mode 100644 index 00000000000..41dfe54abeb --- /dev/null +++ b/regression/strings/StringBuilderChars01/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderChars01.class +--string-refine --unwind 100 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderChars02/StringBuilderChars02.class b/regression/strings/StringBuilderChars02/StringBuilderChars02.class new file mode 100644 index 00000000000..bcfdcce9aa6 Binary files /dev/null and b/regression/strings/StringBuilderChars02/StringBuilderChars02.class differ diff --git a/regression/strings/StringBuilderChars02/StringBuilderChars02.java b/regression/strings/StringBuilderChars02/StringBuilderChars02.java new file mode 100644 index 00000000000..c5a2bb276f3 --- /dev/null +++ b/regression/strings/StringBuilderChars02/StringBuilderChars02.java @@ -0,0 +1,8 @@ +public class StringBuilderChars02 +{ + public static void main(String[] args) + { + StringBuilder buffer = new StringBuilder("DiffBlue Limited"); + assert buffer.toString().equals("DiffBlue Limitted"); + } +} diff --git a/regression/strings/StringBuilderChars02/test.desc b/regression/strings/StringBuilderChars02/test.desc new file mode 100644 index 00000000000..3a6bde6ef78 --- /dev/null +++ b/regression/strings/StringBuilderChars02/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderChars02.class +--string-refine --unwind 100 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderChars03/StringBuilderChars03.class b/regression/strings/StringBuilderChars03/StringBuilderChars03.class new file mode 100644 index 00000000000..d124e87d092 Binary files /dev/null and b/regression/strings/StringBuilderChars03/StringBuilderChars03.class differ diff --git a/regression/strings/StringBuilderChars03/StringBuilderChars03.java b/regression/strings/StringBuilderChars03/StringBuilderChars03.java new file mode 100644 index 00000000000..f226901e113 --- /dev/null +++ b/regression/strings/StringBuilderChars03/StringBuilderChars03.java @@ -0,0 +1,8 @@ +public class StringBuilderChars03 +{ + public static void main(String[] args) + { + StringBuilder buffer = new StringBuilder("DiffBlue Limited"); + assert buffer.charAt(0)==buffer.charAt(4); + } +} diff --git a/regression/strings/StringBuilderChars03/test.desc b/regression/strings/StringBuilderChars03/test.desc new file mode 100644 index 00000000000..12f20189434 --- /dev/null +++ b/regression/strings/StringBuilderChars03/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderChars03.class +--string-refine --unwind 100 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderChars04/StringBuilderChars04.class b/regression/strings/StringBuilderChars04/StringBuilderChars04.class new file mode 100644 index 00000000000..41be0e00683 Binary files /dev/null and b/regression/strings/StringBuilderChars04/StringBuilderChars04.class differ diff --git a/regression/strings/StringBuilderChars04/StringBuilderChars04.java b/regression/strings/StringBuilderChars04/StringBuilderChars04.java new file mode 100644 index 00000000000..039c0079c42 --- /dev/null +++ b/regression/strings/StringBuilderChars04/StringBuilderChars04.java @@ -0,0 +1,18 @@ +public class StringBuilderChars04 +{ + public static void main(String[] args) + { + StringBuilder buffer = new StringBuilder("DiffBlue Limited"); + + char[] charArray = new char[buffer.length()]; + buffer.getChars(0, buffer.length(), charArray, 0); + + int i=0; + for (char character : charArray) + { + System.out.print(character); + assert character!=buffer.charAt(i); + ++i; + } + } +} diff --git a/regression/strings/StringBuilderChars04/test.desc b/regression/strings/StringBuilderChars04/test.desc new file mode 100644 index 00000000000..a2658cf2fe4 --- /dev/null +++ b/regression/strings/StringBuilderChars04/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderChars04.class +--string-refine --unwind 100 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderChars05/StringBuilderChars05.class b/regression/strings/StringBuilderChars05/StringBuilderChars05.class new file mode 100644 index 00000000000..25d758c6d62 Binary files /dev/null and b/regression/strings/StringBuilderChars05/StringBuilderChars05.class differ diff --git a/regression/strings/StringBuilderChars05/StringBuilderChars05.java b/regression/strings/StringBuilderChars05/StringBuilderChars05.java new file mode 100644 index 00000000000..120871f8a9d --- /dev/null +++ b/regression/strings/StringBuilderChars05/StringBuilderChars05.java @@ -0,0 +1,10 @@ +public class StringBuilderChars05 +{ + public static void main(String[] args) + { + StringBuilder buffer = new StringBuilder("DiffBlue Limited"); + buffer.setCharAt(0, 'H'); + buffer.setCharAt(6, 'T'); + assert buffer.toString().equals("HiffBllTe Limited"); + } +} diff --git a/regression/strings/StringBuilderChars05/test.desc b/regression/strings/StringBuilderChars05/test.desc new file mode 100644 index 00000000000..2bcbdbab934 --- /dev/null +++ b/regression/strings/StringBuilderChars05/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderChars05.class +--string-refine --unwind 100 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderChars06/StringBuilderChars06.class b/regression/strings/StringBuilderChars06/StringBuilderChars06.class new file mode 100644 index 00000000000..e3597f40f87 Binary files /dev/null and b/regression/strings/StringBuilderChars06/StringBuilderChars06.class differ diff --git a/regression/strings/StringBuilderChars06/StringBuilderChars06.java b/regression/strings/StringBuilderChars06/StringBuilderChars06.java new file mode 100644 index 00000000000..f3b3b6bc8d8 --- /dev/null +++ b/regression/strings/StringBuilderChars06/StringBuilderChars06.java @@ -0,0 +1,9 @@ +public class StringBuilderChars06 +{ + public static void main(String[] args) + { + StringBuilder buffer = new StringBuilder("DiffBlue Limited"); + buffer.reverse(); + assert buffer.toString().equals("detimiL eTlBffiiH"); + } +} diff --git a/regression/strings/StringBuilderChars06/test.desc b/regression/strings/StringBuilderChars06/test.desc new file mode 100644 index 00000000000..4a711edf496 --- /dev/null +++ b/regression/strings/StringBuilderChars06/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderChars06.class +--string-refine --unwind 100 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderConstructors01/StringBuilderConstructors01.class b/regression/strings/StringBuilderConstructors01/StringBuilderConstructors01.class new file mode 100644 index 00000000000..c7052b38c1f Binary files /dev/null and b/regression/strings/StringBuilderConstructors01/StringBuilderConstructors01.class differ diff --git a/regression/strings/StringBuilderConstructors01/StringBuilderConstructors01.java b/regression/strings/StringBuilderConstructors01/StringBuilderConstructors01.java new file mode 100644 index 00000000000..efb5524c2b8 --- /dev/null +++ b/regression/strings/StringBuilderConstructors01/StringBuilderConstructors01.java @@ -0,0 +1,13 @@ +public class StringBuilderConstructors01 +{ + public static void main(String[] args) + { + StringBuilder buffer1 = new StringBuilder(); + StringBuilder buffer2 = new StringBuilder(10); + StringBuilder buffer3 = new StringBuilder("diffblue"); + + assert buffer1.length()==0; + assert buffer2.length()==0; + assert buffer3.length()>0; + } +} diff --git a/regression/strings/StringBuilderConstructors01/test.desc b/regression/strings/StringBuilderConstructors01/test.desc new file mode 100644 index 00000000000..2c60f9bbbda --- /dev/null +++ b/regression/strings/StringBuilderConstructors01/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StringBuilderConstructors01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderConstructors02/StringBuilderConstructors02.class b/regression/strings/StringBuilderConstructors02/StringBuilderConstructors02.class new file mode 100644 index 00000000000..2bfe2e70d3b Binary files /dev/null and b/regression/strings/StringBuilderConstructors02/StringBuilderConstructors02.class differ diff --git a/regression/strings/StringBuilderConstructors02/StringBuilderConstructors02.java b/regression/strings/StringBuilderConstructors02/StringBuilderConstructors02.java new file mode 100644 index 00000000000..34df0144e82 --- /dev/null +++ b/regression/strings/StringBuilderConstructors02/StringBuilderConstructors02.java @@ -0,0 +1,8 @@ +public class StringBuilderConstructors02 +{ + public static void main(String[] args) + { + StringBuilder buffer3 = new StringBuilder("diffblue"); + assert buffer3.equals("diffblue"); + } +} diff --git a/regression/strings/StringBuilderConstructors02/test.desc b/regression/strings/StringBuilderConstructors02/test.desc new file mode 100644 index 00000000000..8cbad8cfe16 --- /dev/null +++ b/regression/strings/StringBuilderConstructors02/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StringBuilderConstructors02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.class b/regression/strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.class new file mode 100644 index 00000000000..7858a392c3f Binary files /dev/null and b/regression/strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.class differ diff --git a/regression/strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.java b/regression/strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.java new file mode 100644 index 00000000000..e864b796249 --- /dev/null +++ b/regression/strings/StringBuilderInsertDelete01/StringBuilderInsertDelete01.java @@ -0,0 +1,46 @@ +public class StringBuilderInsertDelete01 +{ + public static void main(String[] args) + { + Object objectRef = "diffblue"; + String string = "test"; + char[] charArray = {'v', 'e', 'r', 'i', 'f', 'i', 'c', 'a', 't', 'i', 'o', 'n'}; + boolean booleanValue = true; + char characterValue = 'K'; + int integerValue = 7; + long longValue = 10000000; + float floatValue = 2.5f; + double doubleValue = 33.333; + + StringBuilder buffer = new StringBuilder(); + + buffer.insert(0, objectRef) + .insert(0, "-") + .insert(0, string) + .insert(0, "-") + .insert(0, charArray) + .insert(0, "-") + .insert(0, charArray, 3, 3) + .insert(0, "-") + .insert(0, booleanValue) + .insert(0, "-") + .insert(0, characterValue) + .insert(0, "-") + .insert(0, integerValue) + .insert(0, "-") + .insert(0, longValue) + .insert(0, "-") + .insert(0, floatValue) + .insert(0, "-") + .insert(0, doubleValue); + + String tmp=buffer.toString(); + assert tmp.equals("33.333-2.5-10000000-7-K-true-ifi-verification-test-diffblue"); + + buffer.deleteCharAt(10); + buffer.delete(2, 6); + + tmp=buffer.toString(); + assert tmp.equals("33-2.510000000-7-K-true-ifi-verification-test-diffblue"); + } +} diff --git a/regression/strings/StringBuilderInsertDelete01/test.desc b/regression/strings/StringBuilderInsertDelete01/test.desc new file mode 100644 index 00000000000..4c3000d6a97 --- /dev/null +++ b/regression/strings/StringBuilderInsertDelete01/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderInsertDelete01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.class b/regression/strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.class new file mode 100644 index 00000000000..e5a8ff2cd05 Binary files /dev/null and b/regression/strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.class differ diff --git a/regression/strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.java b/regression/strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.java new file mode 100644 index 00000000000..d0e4923ad3c --- /dev/null +++ b/regression/strings/StringBuilderInsertDelete02/StringBuilderInsertDelete02.java @@ -0,0 +1,40 @@ +public class StringBuilderInsertDelete02 +{ + public static void main(String[] args) + { + Object objectRef = "diffblue"; + String string = "test"; + char[] charArray = {'v', 'e', 'r', 'i', 'f', 'i', 'c', 'a', 't', 'i', 'o', 'n'}; + boolean booleanValue = true; + char characterValue = 'K'; + int integerValue = 7; + long longValue = 10000000; + float floatValue = 2.5f; + double doubleValue = 33.333; + + StringBuilder buffer = new StringBuilder(); + + buffer.insert(0, objectRef) + .insert(0, "-") + .insert(0, string) + .insert(0, "-") + .insert(0, charArray) + .insert(0, "-") + .insert(0, charArray, 3, 3) + .insert(0, "-") + .insert(0, booleanValue) + .insert(0, "-") + .insert(0, characterValue) + .insert(0, "-") + .insert(0, integerValue) + .insert(0, "-") + .insert(0, longValue) + .insert(0, "-") + .insert(0, floatValue) + .insert(0, "-") + .insert(0, doubleValue); + + String tmp=buffer.toString(); + assert tmp.equals("33.333-2.5-10000000-7-K-true-ifi-verification-test--diffblue"); + } +} diff --git a/regression/strings/StringBuilderInsertDelete02/test.desc b/regression/strings/StringBuilderInsertDelete02/test.desc new file mode 100644 index 00000000000..f78bf3f983a --- /dev/null +++ b/regression/strings/StringBuilderInsertDelete02/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderInsertDelete02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.class b/regression/strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.class new file mode 100644 index 00000000000..6e238d7caea Binary files /dev/null and b/regression/strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.class differ diff --git a/regression/strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.java b/regression/strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.java new file mode 100644 index 00000000000..bad25b201a3 --- /dev/null +++ b/regression/strings/StringBuilderInsertDelete03/StringBuilderInsertDelete03.java @@ -0,0 +1,43 @@ +public class StringBuilderInsertDelete03 +{ + public static void main(String[] args) + { + Object objectRef = "diffblue"; + String string = "test"; + char[] charArray = {'v', 'e', 'r', 'i', 'f', 'i', 'c', 'a', 't', 'i', 'o', 'n'}; + boolean booleanValue = true; + char characterValue = 'K'; + int integerValue = 7; + long longValue = 10000000; + float floatValue = 2.5f; + double doubleValue = 33.333; + + StringBuilder buffer = new StringBuilder(); + + buffer.insert(0, objectRef) + .insert(0, "-") + .insert(0, string) + .insert(0, "-") + .insert(0, charArray) + .insert(0, "-") + .insert(0, charArray, 3, 3) + .insert(0, "-") + .insert(0, booleanValue) + .insert(0, "-") + .insert(0, characterValue) + .insert(0, "-") + .insert(0, integerValue) + .insert(0, "-") + .insert(0, longValue) + .insert(0, "-") + .insert(0, floatValue) + .insert(0, "-") + .insert(0, doubleValue); + + buffer.deleteCharAt(10); + buffer.delete(2, 6); + + String tmp=buffer.toString(); + assert tmp.equals("33-2.510000000-7-K-true-iai-verification-test-diffblue"); + } +} diff --git a/regression/strings/StringBuilderInsertDelete03/test.desc b/regression/strings/StringBuilderInsertDelete03/test.desc new file mode 100644 index 00000000000..b3882f41f7e --- /dev/null +++ b/regression/strings/StringBuilderInsertDelete03/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringBuilderInsertDelete03.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringCompare01/StringCompare01.class b/regression/strings/StringCompare01/StringCompare01.class new file mode 100644 index 00000000000..38f0d216e1c Binary files /dev/null and b/regression/strings/StringCompare01/StringCompare01.class differ diff --git a/regression/strings/StringCompare01/StringCompare01.java b/regression/strings/StringCompare01/StringCompare01.java new file mode 100644 index 00000000000..5a669d5c409 --- /dev/null +++ b/regression/strings/StringCompare01/StringCompare01.java @@ -0,0 +1,47 @@ +public class StringCompare01 +{ + public static void main(String[] args) + { + String s1 = new String("test"); + String s2 = "goodbye"; + String s3 = "Automatic Test Generation"; + String s4 = "automatic test generation"; + + if (s1.equals("test")) // true + assert true; + else + assert false; + + if (s1 != "test") // true; they are not the same object + assert true; + else + assert false; + + if (s3.equalsIgnoreCase(s4)) // true + assert true; + else + assert false; + + assert s1.compareTo(s2)==13; //true + + assert s2.compareTo(s1)==-13; //true + + assert s1.compareTo(s1)==0; //true + + assert s3.compareTo(s4)==-32; //true + + assert s4.compareTo(s3)==32; //true + + // test regionMatches (case sensitive) + if (!s3.regionMatches(0, s4, 0, 5)) //true + assert true; + else + assert false; + + // test regionMatches (ignore case) + if (s3.regionMatches(true, 0, s4, 0, 5)) //true + assert true; + else + assert false; + } +} diff --git a/regression/strings/StringCompare01/test.desc b/regression/strings/StringCompare01/test.desc new file mode 100644 index 00000000000..52b1d6d084c --- /dev/null +++ b/regression/strings/StringCompare01/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringCompare01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringCompare02/StringCompare02.class b/regression/strings/StringCompare02/StringCompare02.class new file mode 100644 index 00000000000..4e8b7d2ad9f Binary files /dev/null and b/regression/strings/StringCompare02/StringCompare02.class differ diff --git a/regression/strings/StringCompare02/StringCompare02.java b/regression/strings/StringCompare02/StringCompare02.java new file mode 100644 index 00000000000..29978a7bd30 --- /dev/null +++ b/regression/strings/StringCompare02/StringCompare02.java @@ -0,0 +1,14 @@ +public class StringCompare02 +{ + public static void main(String[] args) + { + String s3 = "Automatic Test Generation"; + String s4 = "automatic test generation"; + + // test regionMatches (case sensitive) + if (s3.regionMatches(0, s4, 0, 5)) //false + assert true; + else + assert false; + } +} diff --git a/regression/strings/StringCompare02/test.desc b/regression/strings/StringCompare02/test.desc new file mode 100644 index 00000000000..abc986be65d --- /dev/null +++ b/regression/strings/StringCompare02/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringCompare02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringCompare03/StringCompare03.class b/regression/strings/StringCompare03/StringCompare03.class new file mode 100644 index 00000000000..1fcdba9a862 Binary files /dev/null and b/regression/strings/StringCompare03/StringCompare03.class differ diff --git a/regression/strings/StringCompare03/StringCompare03.java b/regression/strings/StringCompare03/StringCompare03.java new file mode 100644 index 00000000000..fbd881efd48 --- /dev/null +++ b/regression/strings/StringCompare03/StringCompare03.java @@ -0,0 +1,14 @@ +public class StringCompare03 +{ + public static void main(String[] args) + { + String s3 = "Automatic Test Generation"; + String s4 = "automatic test generation"; + + // test regionMatches (ignore case) + if (!s3.regionMatches(true, 0, s4, 0, 5)) //false + assert true; + else + assert false; + } +} diff --git a/regression/strings/StringCompare03/test.desc b/regression/strings/StringCompare03/test.desc new file mode 100644 index 00000000000..fa518907143 --- /dev/null +++ b/regression/strings/StringCompare03/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringCompare03.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringCompare04/StringCompare04.class b/regression/strings/StringCompare04/StringCompare04.class new file mode 100644 index 00000000000..cb288719581 Binary files /dev/null and b/regression/strings/StringCompare04/StringCompare04.class differ diff --git a/regression/strings/StringCompare04/StringCompare04.java b/regression/strings/StringCompare04/StringCompare04.java new file mode 100644 index 00000000000..c602594930f --- /dev/null +++ b/regression/strings/StringCompare04/StringCompare04.java @@ -0,0 +1,9 @@ +public class StringCompare04 +{ + public static void main(String[] args) + { + String s1 = new String("test"); + String s2 = "goodbye"; + assert s2.compareTo(s1)==13; //false + } +} diff --git a/regression/strings/StringCompare04/test.desc b/regression/strings/StringCompare04/test.desc new file mode 100644 index 00000000000..f1b2a9790cc --- /dev/null +++ b/regression/strings/StringCompare04/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringCompare04.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringCompare05/StringCompare05.class b/regression/strings/StringCompare05/StringCompare05.class new file mode 100644 index 00000000000..70bbad48ef6 Binary files /dev/null and b/regression/strings/StringCompare05/StringCompare05.class differ diff --git a/regression/strings/StringCompare05/StringCompare05.java b/regression/strings/StringCompare05/StringCompare05.java new file mode 100644 index 00000000000..8764cb5c99a --- /dev/null +++ b/regression/strings/StringCompare05/StringCompare05.java @@ -0,0 +1,11 @@ +public class StringCompare05 +{ + public static void main(String[] args) + { + String s1 = new String("test"); + if (s1 == "test") // false; they are not the same object + assert true; + else + assert false; + } +} diff --git a/regression/strings/StringCompare05/test.desc b/regression/strings/StringCompare05/test.desc new file mode 100644 index 00000000000..159809fac0f --- /dev/null +++ b/regression/strings/StringCompare05/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringCompare05.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringConcatenation01/StringConcatenation01.class b/regression/strings/StringConcatenation01/StringConcatenation01.class new file mode 100644 index 00000000000..8a2ee685b44 Binary files /dev/null and b/regression/strings/StringConcatenation01/StringConcatenation01.class differ diff --git a/regression/strings/StringConcatenation01/StringConcatenation01.java b/regression/strings/StringConcatenation01/StringConcatenation01.java new file mode 100644 index 00000000000..be516610e94 --- /dev/null +++ b/regression/strings/StringConcatenation01/StringConcatenation01.java @@ -0,0 +1,17 @@ +public class StringConcatenation01 +{ + public static void main(String[] args) + { + String s1 = "Happy at"; + String s2 = " DiffBlue"; + + assert s1.equals("Happy at"); + assert s2.equals(" DiffBlue"); + + String tmp=s1.concat(s2); + assert tmp.equals("Happy at DiffBlue"); + + tmp=s1; + assert tmp.equals("Happy at"); + } +} diff --git a/regression/strings/StringConcatenation01/test.desc b/regression/strings/StringConcatenation01/test.desc new file mode 100644 index 00000000000..a229b504571 --- /dev/null +++ b/regression/strings/StringConcatenation01/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StringConcatenation01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringConcatenation02/StringConcatenation02.class b/regression/strings/StringConcatenation02/StringConcatenation02.class new file mode 100644 index 00000000000..b8272c61412 Binary files /dev/null and b/regression/strings/StringConcatenation02/StringConcatenation02.class differ diff --git a/regression/strings/StringConcatenation02/StringConcatenation02.java b/regression/strings/StringConcatenation02/StringConcatenation02.java new file mode 100644 index 00000000000..84f1c72e60c --- /dev/null +++ b/regression/strings/StringConcatenation02/StringConcatenation02.java @@ -0,0 +1,10 @@ +public class StringConcatenation02 +{ + public static void main(String[] args) + { + String s1 = "Happy at"; + String s2 = " DiffBlue"; + assert s1.equals("Happy at "); + assert s2.equals(" DiffBlue"); + } +} diff --git a/regression/strings/StringConcatenation02/test.desc b/regression/strings/StringConcatenation02/test.desc new file mode 100644 index 00000000000..937caa3295e --- /dev/null +++ b/regression/strings/StringConcatenation02/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StringConcatenation02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringConcatenation03/StringConcatenation03.class b/regression/strings/StringConcatenation03/StringConcatenation03.class new file mode 100644 index 00000000000..49d03b9c937 Binary files /dev/null and b/regression/strings/StringConcatenation03/StringConcatenation03.class differ diff --git a/regression/strings/StringConcatenation03/StringConcatenation03.java b/regression/strings/StringConcatenation03/StringConcatenation03.java new file mode 100644 index 00000000000..56d397b96dc --- /dev/null +++ b/regression/strings/StringConcatenation03/StringConcatenation03.java @@ -0,0 +1,17 @@ +public class StringConcatenation03 +{ + public static void main(String[] args) + { + String s1 = "Happy at"; + String s2 = " DiffBlue"; + + System.out.printf( + "Result of s1.concat(s2) = %s\n", s1.concat(s2)); + String tmp=s1.concat(s2); + assert tmp.equals("Happy at DiffBllue"); + + tmp=s1; + System.out.printf("s1 after concatenation = %s\n", s1); + assert tmp.equals("Happy at"); + } +} diff --git a/regression/strings/StringConcatenation03/test.desc b/regression/strings/StringConcatenation03/test.desc new file mode 100644 index 00000000000..26ccc899a87 --- /dev/null +++ b/regression/strings/StringConcatenation03/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringConcatenation03.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringConcatenation04/StringConcatenation04.class b/regression/strings/StringConcatenation04/StringConcatenation04.class new file mode 100644 index 00000000000..047d2b908ab Binary files /dev/null and b/regression/strings/StringConcatenation04/StringConcatenation04.class differ diff --git a/regression/strings/StringConcatenation04/StringConcatenation04.java b/regression/strings/StringConcatenation04/StringConcatenation04.java new file mode 100644 index 00000000000..5ffc9086517 --- /dev/null +++ b/regression/strings/StringConcatenation04/StringConcatenation04.java @@ -0,0 +1,10 @@ +public class StringConcatenation04 +{ + public static void main(String[] args) + { + String s1 = "Happy at"; + String tmp=s1; + System.out.printf("s1 after concatenation = %s\n", s1); + assert tmp.equals("Happy at"); + } +} diff --git a/regression/strings/StringConcatenation04/test.desc b/regression/strings/StringConcatenation04/test.desc new file mode 100644 index 00000000000..ea980c45d54 --- /dev/null +++ b/regression/strings/StringConcatenation04/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringConcatenation04.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringConstructors01/StringConstructors01.class b/regression/strings/StringConstructors01/StringConstructors01.class new file mode 100644 index 00000000000..c4e2ce34c83 Binary files /dev/null and b/regression/strings/StringConstructors01/StringConstructors01.class differ diff --git a/regression/strings/StringConstructors01/StringConstructors01.java b/regression/strings/StringConstructors01/StringConstructors01.java new file mode 100644 index 00000000000..406653de694 --- /dev/null +++ b/regression/strings/StringConstructors01/StringConstructors01.java @@ -0,0 +1,19 @@ +public class StringConstructors01 +{ + public static void main(String[] args) + { + char[] charArray = {'d', 'i', 'f', 'f', 'b', 'l', 'u', 'e'}; + String s = new String("test"); + + String s1 = new String(); + String s2 = new String(s); + String s3 = new String(charArray); + String s4 = new String(charArray, 4, 4); + + assert s1.equals(""); + assert s2.equals("test"); + assert s3.equals("diffblue"); + assert s4.equals("blue"); + } +} + diff --git a/regression/strings/StringConstructors01/test.desc b/regression/strings/StringConstructors01/test.desc new file mode 100644 index 00000000000..ed57bdfdde5 --- /dev/null +++ b/regression/strings/StringConstructors01/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringConstructors01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringConstructors02/StringConstructors02.class b/regression/strings/StringConstructors02/StringConstructors02.class new file mode 100644 index 00000000000..0cca7f99377 Binary files /dev/null and b/regression/strings/StringConstructors02/StringConstructors02.class differ diff --git a/regression/strings/StringConstructors02/StringConstructors02.java b/regression/strings/StringConstructors02/StringConstructors02.java new file mode 100644 index 00000000000..b20877b8106 --- /dev/null +++ b/regression/strings/StringConstructors02/StringConstructors02.java @@ -0,0 +1,9 @@ +public class StringConstructors02 +{ + public static void main(String[] args) + { + String s1 = new String(); + assert s1.equals(" "); + } +} + diff --git a/regression/strings/StringConstructors02/test.desc b/regression/strings/StringConstructors02/test.desc new file mode 100644 index 00000000000..c2a30b3534c --- /dev/null +++ b/regression/strings/StringConstructors02/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringConstructors02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringConstructors03/StringConstructors03.class b/regression/strings/StringConstructors03/StringConstructors03.class new file mode 100644 index 00000000000..fba6b043267 Binary files /dev/null and b/regression/strings/StringConstructors03/StringConstructors03.class differ diff --git a/regression/strings/StringConstructors03/StringConstructors03.java b/regression/strings/StringConstructors03/StringConstructors03.java new file mode 100644 index 00000000000..a2f6ced182a --- /dev/null +++ b/regression/strings/StringConstructors03/StringConstructors03.java @@ -0,0 +1,10 @@ +public class StringConstructors03 +{ + public static void main(String[] args) + { + String s = new String("test"); + String s2 = new String(s); + assert s2.equals("tesst"); + } +} + diff --git a/regression/strings/StringConstructors03/test.desc b/regression/strings/StringConstructors03/test.desc new file mode 100644 index 00000000000..5419e5ae48e --- /dev/null +++ b/regression/strings/StringConstructors03/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringConstructors03.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringConstructors04/StringConstructors04.class b/regression/strings/StringConstructors04/StringConstructors04.class new file mode 100644 index 00000000000..d7705f364f3 Binary files /dev/null and b/regression/strings/StringConstructors04/StringConstructors04.class differ diff --git a/regression/strings/StringConstructors04/StringConstructors04.java b/regression/strings/StringConstructors04/StringConstructors04.java new file mode 100644 index 00000000000..bd9828e6a5f --- /dev/null +++ b/regression/strings/StringConstructors04/StringConstructors04.java @@ -0,0 +1,10 @@ +public class StringConstructors04 +{ + public static void main(String[] args) + { + char[] charArray = {'d', 'i', 'f', 'f', 'b', 'l', 'u', 'e'}; + String s4 = new String(charArray, 4, 4); + assert s4.equals("bllue"); + } +} + diff --git a/regression/strings/StringConstructors04/test.desc b/regression/strings/StringConstructors04/test.desc new file mode 100644 index 00000000000..21394f70327 --- /dev/null +++ b/regression/strings/StringConstructors04/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringConstructors04.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringConstructors05/StringConstructors05.class b/regression/strings/StringConstructors05/StringConstructors05.class new file mode 100644 index 00000000000..8339e1ddab3 Binary files /dev/null and b/regression/strings/StringConstructors05/StringConstructors05.class differ diff --git a/regression/strings/StringConstructors05/StringConstructors05.java b/regression/strings/StringConstructors05/StringConstructors05.java new file mode 100644 index 00000000000..49cc43f4269 --- /dev/null +++ b/regression/strings/StringConstructors05/StringConstructors05.java @@ -0,0 +1,10 @@ +public class StringConstructors05 +{ + public static void main(String[] args) + { + char[] charArray = {'d', 'i', 'f', 'f', 'b', 'l', 'u', 'e'}; + String s3 = new String(charArray); + assert s3.equals("diffkblue"); + } +} + diff --git a/regression/strings/StringConstructors05/test.desc b/regression/strings/StringConstructors05/test.desc new file mode 100644 index 00000000000..9804850d77e --- /dev/null +++ b/regression/strings/StringConstructors05/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringConstructors05.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringIndexMethods01/StringIndexMethods01.class b/regression/strings/StringIndexMethods01/StringIndexMethods01.class new file mode 100644 index 00000000000..f8086f133e6 Binary files /dev/null and b/regression/strings/StringIndexMethods01/StringIndexMethods01.class differ diff --git a/regression/strings/StringIndexMethods01/StringIndexMethods01.java b/regression/strings/StringIndexMethods01/StringIndexMethods01.java new file mode 100644 index 00000000000..da000057993 --- /dev/null +++ b/regression/strings/StringIndexMethods01/StringIndexMethods01.java @@ -0,0 +1,20 @@ +public class StringIndexMethods01 +{ + public static void main(String[] args) + { + String letters = "automatictestcasegenerationatdiffblue"; + + assert letters.indexOf('c')==8; + assert letters.indexOf('a', 1)==5; + assert letters.indexOf('$')==-1; + assert letters.lastIndexOf('c')==13; + assert letters.lastIndexOf('a', 25)==22; + assert letters.lastIndexOf('$')==-1; + assert letters.indexOf("diffblue")==29; + assert letters.indexOf("diffblue", 7)==29; + assert letters.indexOf("generation")==17; + assert letters.lastIndexOf("diffblue")==29; + assert letters.lastIndexOf("diffblue", 25)==-1; + assert letters.lastIndexOf("automatic")==0; + } +} diff --git a/regression/strings/StringIndexMethods01/test.desc b/regression/strings/StringIndexMethods01/test.desc new file mode 100644 index 00000000000..005d4459f12 --- /dev/null +++ b/regression/strings/StringIndexMethods01/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringIndexMethods01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringIndexMethods02/StringIndexMethods02.class b/regression/strings/StringIndexMethods02/StringIndexMethods02.class new file mode 100644 index 00000000000..fe322fde894 Binary files /dev/null and b/regression/strings/StringIndexMethods02/StringIndexMethods02.class differ diff --git a/regression/strings/StringIndexMethods02/StringIndexMethods02.java b/regression/strings/StringIndexMethods02/StringIndexMethods02.java new file mode 100644 index 00000000000..5c2ea999dd0 --- /dev/null +++ b/regression/strings/StringIndexMethods02/StringIndexMethods02.java @@ -0,0 +1,8 @@ +public class StringIndexMethods02 +{ + public static void main(String[] args) + { + String letters = "automatictestcasegenerationatdiffblue"; + assert letters.indexOf('a', 1)==6; + } +} diff --git a/regression/strings/StringIndexMethods02/test.desc b/regression/strings/StringIndexMethods02/test.desc new file mode 100644 index 00000000000..cad6c487fae --- /dev/null +++ b/regression/strings/StringIndexMethods02/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringIndexMethods02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringIndexMethods03/StringIndexMethods03.class b/regression/strings/StringIndexMethods03/StringIndexMethods03.class new file mode 100644 index 00000000000..e8733f57168 Binary files /dev/null and b/regression/strings/StringIndexMethods03/StringIndexMethods03.class differ diff --git a/regression/strings/StringIndexMethods03/StringIndexMethods03.java b/regression/strings/StringIndexMethods03/StringIndexMethods03.java new file mode 100644 index 00000000000..83b710073b5 --- /dev/null +++ b/regression/strings/StringIndexMethods03/StringIndexMethods03.java @@ -0,0 +1,8 @@ +public class StringIndexMethods03 +{ + public static void main(String[] args) + { + String letters = "automatictestcasegenerationatdiffblue"; + assert letters.lastIndexOf('$')==1; + } +} diff --git a/regression/strings/StringIndexMethods03/test.desc b/regression/strings/StringIndexMethods03/test.desc new file mode 100644 index 00000000000..3dff0b27714 --- /dev/null +++ b/regression/strings/StringIndexMethods03/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringIndexMethods03.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringIndexMethods04/StringIndexMethods04.class b/regression/strings/StringIndexMethods04/StringIndexMethods04.class new file mode 100644 index 00000000000..69a8fe4d628 Binary files /dev/null and b/regression/strings/StringIndexMethods04/StringIndexMethods04.class differ diff --git a/regression/strings/StringIndexMethods04/StringIndexMethods04.java b/regression/strings/StringIndexMethods04/StringIndexMethods04.java new file mode 100644 index 00000000000..1271bcaf36b --- /dev/null +++ b/regression/strings/StringIndexMethods04/StringIndexMethods04.java @@ -0,0 +1,8 @@ +public class StringIndexMethods04 +{ + public static void main(String[] args) + { + String letters = "automatictestcasegenerationatdiffblue"; + assert letters.indexOf("diffblue")==28; + } +} diff --git a/regression/strings/StringIndexMethods04/test.desc b/regression/strings/StringIndexMethods04/test.desc new file mode 100644 index 00000000000..758f22d2bf4 --- /dev/null +++ b/regression/strings/StringIndexMethods04/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringIndexMethods04.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringIndexMethods05/StringIndexMethods05.class b/regression/strings/StringIndexMethods05/StringIndexMethods05.class new file mode 100644 index 00000000000..a4f4f767495 Binary files /dev/null and b/regression/strings/StringIndexMethods05/StringIndexMethods05.class differ diff --git a/regression/strings/StringIndexMethods05/StringIndexMethods05.java b/regression/strings/StringIndexMethods05/StringIndexMethods05.java new file mode 100644 index 00000000000..f6de4ce541b --- /dev/null +++ b/regression/strings/StringIndexMethods05/StringIndexMethods05.java @@ -0,0 +1,8 @@ +public class StringIndexMethods05 +{ + public static void main(String[] args) + { + String letters = "automatictestcasegenerationatdiffblue"; + assert letters.lastIndexOf("diffblue", 25)==1; + } +} diff --git a/regression/strings/StringIndexMethods05/test.desc b/regression/strings/StringIndexMethods05/test.desc new file mode 100644 index 00000000000..d415ef1381e --- /dev/null +++ b/regression/strings/StringIndexMethods05/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringIndexMethods05.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringMiscellaneous01/StringMiscellaneous01.class b/regression/strings/StringMiscellaneous01/StringMiscellaneous01.class new file mode 100644 index 00000000000..4f63b35324b Binary files /dev/null and b/regression/strings/StringMiscellaneous01/StringMiscellaneous01.class differ diff --git a/regression/strings/StringMiscellaneous01/StringMiscellaneous01.java b/regression/strings/StringMiscellaneous01/StringMiscellaneous01.java new file mode 100644 index 00000000000..26fc7442f7f --- /dev/null +++ b/regression/strings/StringMiscellaneous01/StringMiscellaneous01.java @@ -0,0 +1,32 @@ +public class StringMiscellaneous01 +{ + public static void main(String[] args) + { + String s1 = "Automatic Test Generation"; + String s2 = "noitareneG tseT citamotuA"; + String s3 = "Autom"; + char[] charArray = new char[5]; + + assert s1.length()==25; + + int i=0; + for (int count = s1.length() - 1; count >= 0; count--) + { + System.out.printf("%c ", s1.charAt(count)); + assert s1.charAt(count) == s2.charAt(i); + ++i; + } + + // copy characters from string into charArray + s1.getChars(0, 5, charArray, 0); + i=0; + for (char character : charArray) + { + System.out.print(character); + assert s3.charAt(i) == character; + ++i; + } + + System.out.println(); + } +} diff --git a/regression/strings/StringMiscellaneous01/test.desc b/regression/strings/StringMiscellaneous01/test.desc new file mode 100644 index 00000000000..050c3e99e90 --- /dev/null +++ b/regression/strings/StringMiscellaneous01/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringMiscellaneous01.class +--string-refine --unwind 30 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringMiscellaneous02/StringMiscellaneous02.class b/regression/strings/StringMiscellaneous02/StringMiscellaneous02.class new file mode 100644 index 00000000000..f1d880c012a Binary files /dev/null and b/regression/strings/StringMiscellaneous02/StringMiscellaneous02.class differ diff --git a/regression/strings/StringMiscellaneous02/StringMiscellaneous02.java b/regression/strings/StringMiscellaneous02/StringMiscellaneous02.java new file mode 100644 index 00000000000..d2351fb79d6 --- /dev/null +++ b/regression/strings/StringMiscellaneous02/StringMiscellaneous02.java @@ -0,0 +1,8 @@ +public class StringMiscellaneous02 +{ + public static void main(String[] args) + { + String s1 = "Automatic Test Generation"; + assert s1.length()==24; + } +} diff --git a/regression/strings/StringMiscellaneous02/test.desc b/regression/strings/StringMiscellaneous02/test.desc new file mode 100644 index 00000000000..53c46cf1a7f --- /dev/null +++ b/regression/strings/StringMiscellaneous02/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringMiscellaneous02.class +--string-refine --unwind 30 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringMiscellaneous03/StringMiscellaneous03.class b/regression/strings/StringMiscellaneous03/StringMiscellaneous03.class new file mode 100644 index 00000000000..210c05ddf32 Binary files /dev/null and b/regression/strings/StringMiscellaneous03/StringMiscellaneous03.class differ diff --git a/regression/strings/StringMiscellaneous03/StringMiscellaneous03.java b/regression/strings/StringMiscellaneous03/StringMiscellaneous03.java new file mode 100644 index 00000000000..2adfe30f5d0 --- /dev/null +++ b/regression/strings/StringMiscellaneous03/StringMiscellaneous03.java @@ -0,0 +1,15 @@ +public class StringMiscellaneous03 +{ + public static void main(String[] args) + { + String s1 = "Automatic Test Generation"; + String s2 = "noitareneG tseT citamotuA"; + char[] charArray = new char[5]; + int i=0; + for (int count = s1.length() - 1; count >= 0; count--) + { + assert s1.charAt(count) != s2.charAt(i); + ++i; + } + } +} diff --git a/regression/strings/StringMiscellaneous03/test.desc b/regression/strings/StringMiscellaneous03/test.desc new file mode 100644 index 00000000000..f255272ed5b --- /dev/null +++ b/regression/strings/StringMiscellaneous03/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringMiscellaneous03.class +--string-refine --unwind 30 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringMiscellaneous04/StringMiscellaneous04.class b/regression/strings/StringMiscellaneous04/StringMiscellaneous04.class new file mode 100644 index 00000000000..c7f02bedbb2 Binary files /dev/null and b/regression/strings/StringMiscellaneous04/StringMiscellaneous04.class differ diff --git a/regression/strings/StringMiscellaneous04/StringMiscellaneous04.java b/regression/strings/StringMiscellaneous04/StringMiscellaneous04.java new file mode 100644 index 00000000000..e9fe0292317 --- /dev/null +++ b/regression/strings/StringMiscellaneous04/StringMiscellaneous04.java @@ -0,0 +1,40 @@ +public class StringMiscellaneous04 +{ + public static void main(String[] args) + { + String s1 = "diffblue"; + String s2 = "TESTGENERATION"; + String s3 = " automated "; + + assert s1.equals("diffblue"); + assert s2.equals("TESTGENERATION"); + assert s3.equals(" automated "); + + System.out.printf( + "Replace 'f' with 'F' in s1: %s\n\n", s1.replace('f', 'F')); + String tmp=s1.replace('f', 'F'); + assert tmp.equals("diFFblue"); + + tmp=s1.toUpperCase(); + assert tmp.equals("DIFFBLUE"); + + tmp=s2.toLowerCase(); + assert tmp.equals("testgeneration"); + + tmp=s3.trim(); + assert tmp.equals("automated"); + + // test toCharArray method + char[] charArray = s1.toCharArray(); + System.out.print("s1 as a character array = "); + + int i=0; + for (char character : charArray) + { + assert character=="diffblue".charAt(i); + ++i; + } + + System.out.println(); + } +} diff --git a/regression/strings/StringMiscellaneous04/test.desc b/regression/strings/StringMiscellaneous04/test.desc new file mode 100644 index 00000000000..737ab3b0f8c --- /dev/null +++ b/regression/strings/StringMiscellaneous04/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringMiscellaneous04.class +--string-refine --unwind 30 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringStartEnd01/StringStartEnd01.class b/regression/strings/StringStartEnd01/StringStartEnd01.class new file mode 100644 index 00000000000..37d2596a6c1 Binary files /dev/null and b/regression/strings/StringStartEnd01/StringStartEnd01.class differ diff --git a/regression/strings/StringStartEnd01/StringStartEnd01.java b/regression/strings/StringStartEnd01/StringStartEnd01.java new file mode 100644 index 00000000000..c1bc4bac328 --- /dev/null +++ b/regression/strings/StringStartEnd01/StringStartEnd01.java @@ -0,0 +1,31 @@ +public class StringStartEnd01 +{ + public static void main(String[] args) + { + String[] strings = {"tested", "testing", "passed", "passing"}; + + int i=0; + for (String string : strings) + { + if (string.startsWith("te")) + ++i; + } + assert i==2; + + i=0; + for (String string : strings) + { + if (string.startsWith("ste", 2)) + ++i; + } + assert i==1; + + i=0; + for (String string : strings) + { + if (string.endsWith("ed")) + ++i; + } + assert i==2; + } +} diff --git a/regression/strings/StringStartEnd01/test.desc b/regression/strings/StringStartEnd01/test.desc new file mode 100644 index 00000000000..a5463d5b5ea --- /dev/null +++ b/regression/strings/StringStartEnd01/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StringStartEnd01.class +--string-refine --unwind 30 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringStartEnd02/StringStartEnd02.class b/regression/strings/StringStartEnd02/StringStartEnd02.class new file mode 100644 index 00000000000..f7b535e4848 Binary files /dev/null and b/regression/strings/StringStartEnd02/StringStartEnd02.class differ diff --git a/regression/strings/StringStartEnd02/StringStartEnd02.java b/regression/strings/StringStartEnd02/StringStartEnd02.java new file mode 100644 index 00000000000..8920026e8fb --- /dev/null +++ b/regression/strings/StringStartEnd02/StringStartEnd02.java @@ -0,0 +1,15 @@ +public class StringStartEnd02 +{ + public static void main(String[] args) + { + String[] strings = {"tested", "testing", "passed", "passing"}; + + int i=0; + for (String string : strings) + { + if (string.startsWith("te")) + ++i; + } + assert i==1; + } +} diff --git a/regression/strings/StringStartEnd02/test.desc b/regression/strings/StringStartEnd02/test.desc new file mode 100644 index 00000000000..16f696efa01 --- /dev/null +++ b/regression/strings/StringStartEnd02/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StringStartEnd02.class +--string-refine --unwind 30 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringStartEnd03/StringStartEnd03.class b/regression/strings/StringStartEnd03/StringStartEnd03.class new file mode 100644 index 00000000000..a353c5e3a30 Binary files /dev/null and b/regression/strings/StringStartEnd03/StringStartEnd03.class differ diff --git a/regression/strings/StringStartEnd03/StringStartEnd03.java b/regression/strings/StringStartEnd03/StringStartEnd03.java new file mode 100644 index 00000000000..79479f9535b --- /dev/null +++ b/regression/strings/StringStartEnd03/StringStartEnd03.java @@ -0,0 +1,15 @@ +public class StringStartEnd03 +{ + public static void main(String[] args) + { + String[] strings = {"tested", "testing", "passed", "passing"}; + + int i=0; + for (String string : strings) + { + if (string.endsWith("ed")) + ++i; + } + assert i==3; + } +} diff --git a/regression/strings/StringStartEnd03/test.desc b/regression/strings/StringStartEnd03/test.desc new file mode 100644 index 00000000000..e6d8c460709 --- /dev/null +++ b/regression/strings/StringStartEnd03/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StringStartEnd03.class +--string-refine --unwind 15 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringValueOf01/StringValueOf01.class b/regression/strings/StringValueOf01/StringValueOf01.class new file mode 100644 index 00000000000..8103d7fb901 Binary files /dev/null and b/regression/strings/StringValueOf01/StringValueOf01.class differ diff --git a/regression/strings/StringValueOf01/StringValueOf01.java b/regression/strings/StringValueOf01/StringValueOf01.java new file mode 100644 index 00000000000..4a1bdc14273 --- /dev/null +++ b/regression/strings/StringValueOf01/StringValueOf01.java @@ -0,0 +1,41 @@ +public class StringValueOf01 +{ + public static void main(String[] args) + { + char[] charArray = {'d', 'i', 'f', 'f', 'b', 'l', 'u', 'e'}; + boolean booleanValue = false; + char characterValue = 'T'; + int integerValue = 7; + long longValue = 10000000000L; // L suffix indicates long + float floatValue = 2.5f; // f indicates that 2.5 is a float + double doubleValue = 33.333; // no suffix, double is default + Object objectRef = "test"; // assign string to an Object reference + + String tmp=String.valueOf(charArray); + assert tmp.equals("diffblue"); + + tmp=String.valueOf(charArray, 3, 3); + assert tmp.equals("fbl"); + + tmp=String.valueOf(booleanValue); + assert tmp.equals("false"); + + tmp=String.valueOf(characterValue); + assert tmp.equals("T"); + + tmp=String.valueOf(integerValue); + assert tmp.equals("7"); + + tmp=String.valueOf(longValue); + assert tmp.equals("10000000000"); + + tmp=String.valueOf(floatValue); + assert tmp.equals("2.5"); + + tmp=String.valueOf(doubleValue); + assert tmp.equals("33.333"); + + tmp=String.valueOf(objectRef); + assert tmp.equals("test"); + } +} diff --git a/regression/strings/StringValueOf01/test.desc b/regression/strings/StringValueOf01/test.desc new file mode 100644 index 00000000000..341f5e98975 --- /dev/null +++ b/regression/strings/StringValueOf01/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringValueOf01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/StringValueOf02/StringValueOf02.class b/regression/strings/StringValueOf02/StringValueOf02.class new file mode 100644 index 00000000000..daf17d33300 Binary files /dev/null and b/regression/strings/StringValueOf02/StringValueOf02.class differ diff --git a/regression/strings/StringValueOf02/StringValueOf02.java b/regression/strings/StringValueOf02/StringValueOf02.java new file mode 100644 index 00000000000..a730af26c02 --- /dev/null +++ b/regression/strings/StringValueOf02/StringValueOf02.java @@ -0,0 +1,9 @@ +public class StringValueOf02 +{ + public static void main(String[] args) + { + char[] charArray = {'d', 'i', 'f', 'f', 'b', 'l', 'u', 'e'}; + String tmp=String.valueOf(charArray); + assert tmp.equals("difffblue"); + } +} diff --git a/regression/strings/StringValueOf02/test.desc b/regression/strings/StringValueOf02/test.desc new file mode 100644 index 00000000000..00835385bc8 --- /dev/null +++ b/regression/strings/StringValueOf02/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringValueOf02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringValueOf03/StringValueOf03.class b/regression/strings/StringValueOf03/StringValueOf03.class new file mode 100644 index 00000000000..886aedc6b1d Binary files /dev/null and b/regression/strings/StringValueOf03/StringValueOf03.class differ diff --git a/regression/strings/StringValueOf03/StringValueOf03.java b/regression/strings/StringValueOf03/StringValueOf03.java new file mode 100644 index 00000000000..0c51518b300 --- /dev/null +++ b/regression/strings/StringValueOf03/StringValueOf03.java @@ -0,0 +1,9 @@ +public class StringValueOf03 +{ + public static void main(String[] args) + { + char[] charArray = {'d', 'i', 'f', 'f', 'b', 'l', 'u', 'e'}; + String tmp=String.valueOf(charArray, 3, 3); + assert tmp.equals("fbbl"); + } +} diff --git a/regression/strings/StringValueOf03/test.desc b/regression/strings/StringValueOf03/test.desc new file mode 100644 index 00000000000..19921a8e98f --- /dev/null +++ b/regression/strings/StringValueOf03/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringValueOf03.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringValueOf04/StringValueOf04.class b/regression/strings/StringValueOf04/StringValueOf04.class new file mode 100644 index 00000000000..5a0d670146c Binary files /dev/null and b/regression/strings/StringValueOf04/StringValueOf04.class differ diff --git a/regression/strings/StringValueOf04/StringValueOf04.java b/regression/strings/StringValueOf04/StringValueOf04.java new file mode 100644 index 00000000000..91ea3e67c30 --- /dev/null +++ b/regression/strings/StringValueOf04/StringValueOf04.java @@ -0,0 +1,9 @@ +public class StringValueOf04 +{ + public static void main(String[] args) + { + boolean booleanValue = false; + String tmp=String.valueOf(booleanValue); + assert tmp.equals("true"); + } +} diff --git a/regression/strings/StringValueOf04/test.desc b/regression/strings/StringValueOf04/test.desc new file mode 100644 index 00000000000..1312d27676d --- /dev/null +++ b/regression/strings/StringValueOf04/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StringValueOf04.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringValueOf05/StringValueOf05.class b/regression/strings/StringValueOf05/StringValueOf05.class new file mode 100644 index 00000000000..08abc79c499 Binary files /dev/null and b/regression/strings/StringValueOf05/StringValueOf05.class differ diff --git a/regression/strings/StringValueOf05/StringValueOf05.java b/regression/strings/StringValueOf05/StringValueOf05.java new file mode 100644 index 00000000000..03854f575b0 --- /dev/null +++ b/regression/strings/StringValueOf05/StringValueOf05.java @@ -0,0 +1,9 @@ +public class StringValueOf05 +{ + public static void main(String[] args) + { + char characterValue = 'T'; + String tmp=String.valueOf(characterValue); + assert tmp.equals("A"); + } +} diff --git a/regression/strings/StringValueOf05/test.desc b/regression/strings/StringValueOf05/test.desc new file mode 100644 index 00000000000..ccb5b3dc440 --- /dev/null +++ b/regression/strings/StringValueOf05/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StringValueOf05.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringValueOf06/StringValueOf06.class b/regression/strings/StringValueOf06/StringValueOf06.class new file mode 100644 index 00000000000..e9a8065210a Binary files /dev/null and b/regression/strings/StringValueOf06/StringValueOf06.class differ diff --git a/regression/strings/StringValueOf06/StringValueOf06.java b/regression/strings/StringValueOf06/StringValueOf06.java new file mode 100644 index 00000000000..b13a3899f0f --- /dev/null +++ b/regression/strings/StringValueOf06/StringValueOf06.java @@ -0,0 +1,9 @@ +public class StringValueOf06 +{ + public static void main(String[] args) + { + int integerValue = 7; + String tmp=String.valueOf(integerValue); + assert tmp.equals("77"); + } +} diff --git a/regression/strings/StringValueOf06/test.desc b/regression/strings/StringValueOf06/test.desc new file mode 100644 index 00000000000..c78afa98f2f --- /dev/null +++ b/regression/strings/StringValueOf06/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StringValueOf06.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringValueOf07/StringValueOf07.class b/regression/strings/StringValueOf07/StringValueOf07.class new file mode 100644 index 00000000000..36e9401884c Binary files /dev/null and b/regression/strings/StringValueOf07/StringValueOf07.class differ diff --git a/regression/strings/StringValueOf07/StringValueOf07.java b/regression/strings/StringValueOf07/StringValueOf07.java new file mode 100644 index 00000000000..c4c44435d22 --- /dev/null +++ b/regression/strings/StringValueOf07/StringValueOf07.java @@ -0,0 +1,10 @@ +public class StringValueOf07 +{ + public static void main(String[] args) + { + long longValue = 10000000000L; + System.out.printf("long = %s\n", String.valueOf(longValue)); + String tmp=String.valueOf(longValue); + assert tmp.equals("100000000000"); + } +} diff --git a/regression/strings/StringValueOf07/test.desc b/regression/strings/StringValueOf07/test.desc new file mode 100644 index 00000000000..7b19c4ff67b --- /dev/null +++ b/regression/strings/StringValueOf07/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +StringValueOf07.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringValueOf08/StringValueOf08.class b/regression/strings/StringValueOf08/StringValueOf08.class new file mode 100644 index 00000000000..356ddbbb9d4 Binary files /dev/null and b/regression/strings/StringValueOf08/StringValueOf08.class differ diff --git a/regression/strings/StringValueOf08/StringValueOf08.java b/regression/strings/StringValueOf08/StringValueOf08.java new file mode 100644 index 00000000000..539c60e5a9f --- /dev/null +++ b/regression/strings/StringValueOf08/StringValueOf08.java @@ -0,0 +1,9 @@ +public class StringValueOf08 +{ + public static void main(String[] args) + { + float floatValue = 2.5f; + String tmp=String.valueOf(floatValue); + assert tmp.equals("2.50"); + } +} diff --git a/regression/strings/StringValueOf08/test.desc b/regression/strings/StringValueOf08/test.desc new file mode 100644 index 00000000000..a7d90b1b9ef --- /dev/null +++ b/regression/strings/StringValueOf08/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringValueOf08.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringValueOf09/StringValueOf09.class b/regression/strings/StringValueOf09/StringValueOf09.class new file mode 100644 index 00000000000..e852bce13a4 Binary files /dev/null and b/regression/strings/StringValueOf09/StringValueOf09.class differ diff --git a/regression/strings/StringValueOf09/StringValueOf09.java b/regression/strings/StringValueOf09/StringValueOf09.java new file mode 100644 index 00000000000..cc35ddb0733 --- /dev/null +++ b/regression/strings/StringValueOf09/StringValueOf09.java @@ -0,0 +1,9 @@ +public class StringValueOf09 +{ + public static void main(String[] args) + { + double doubleValue = 33.333; // no suffix, double is default + String tmp=String.valueOf(doubleValue); + assert tmp.equals("33.3333"); + } +} diff --git a/regression/strings/StringValueOf09/test.desc b/regression/strings/StringValueOf09/test.desc new file mode 100644 index 00000000000..10f6b102a67 --- /dev/null +++ b/regression/strings/StringValueOf09/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringValueOf09.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/StringValueOf10/StringValueOf10.class b/regression/strings/StringValueOf10/StringValueOf10.class new file mode 100644 index 00000000000..da330143f4d Binary files /dev/null and b/regression/strings/StringValueOf10/StringValueOf10.class differ diff --git a/regression/strings/StringValueOf10/StringValueOf10.java b/regression/strings/StringValueOf10/StringValueOf10.java new file mode 100644 index 00000000000..044586124a7 --- /dev/null +++ b/regression/strings/StringValueOf10/StringValueOf10.java @@ -0,0 +1,9 @@ +public class StringValueOf10 +{ + public static void main(String[] args) + { + Object objectRef = "test"; // assign string to an Object reference + String tmp=String.valueOf(objectRef); + assert tmp.equals("tesst"); + } +} diff --git a/regression/strings/StringValueOf10/test.desc b/regression/strings/StringValueOf10/test.desc new file mode 100644 index 00000000000..5de3d5aade7 --- /dev/null +++ b/regression/strings/StringValueOf10/test.desc @@ -0,0 +1,8 @@ +FUTURE +StringValueOf10.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/SubString01/SubString01.class b/regression/strings/SubString01/SubString01.class new file mode 100644 index 00000000000..861bf6905d3 Binary files /dev/null and b/regression/strings/SubString01/SubString01.class differ diff --git a/regression/strings/SubString01/SubString01.java b/regression/strings/SubString01/SubString01.java new file mode 100644 index 00000000000..c99db9b7308 --- /dev/null +++ b/regression/strings/SubString01/SubString01.java @@ -0,0 +1,13 @@ +public class SubString01 +{ + public static void main(String[] args) + { + String letters = "automatictestcasegenerationatdiffblue"; + + String tmp=letters.substring(20); + assert tmp.equals("erationatdiffblue"); + + tmp=letters.substring(9, 13); + assert tmp.equals("test"); + } +} diff --git a/regression/strings/SubString01/test.desc b/regression/strings/SubString01/test.desc new file mode 100644 index 00000000000..8eea70cf458 --- /dev/null +++ b/regression/strings/SubString01/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +SubString01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/SubString02/SubString02.class b/regression/strings/SubString02/SubString02.class new file mode 100644 index 00000000000..d758b7baf0b Binary files /dev/null and b/regression/strings/SubString02/SubString02.class differ diff --git a/regression/strings/SubString02/SubString02.java b/regression/strings/SubString02/SubString02.java new file mode 100644 index 00000000000..36961dcca75 --- /dev/null +++ b/regression/strings/SubString02/SubString02.java @@ -0,0 +1,9 @@ +public class SubString02 +{ + public static void main(String[] args) + { + String letters = "automatictestcasegenerationatdiffblue"; + String tmp=letters.substring(20); + assert tmp.equals("erationatdifffblue"); + } +} diff --git a/regression/strings/SubString02/test.desc b/regression/strings/SubString02/test.desc new file mode 100644 index 00000000000..e7b21cdd678 --- /dev/null +++ b/regression/strings/SubString02/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +SubString02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/SubString03/SubString03.class b/regression/strings/SubString03/SubString03.class new file mode 100644 index 00000000000..27241061d32 Binary files /dev/null and b/regression/strings/SubString03/SubString03.class differ diff --git a/regression/strings/SubString03/SubString03.java b/regression/strings/SubString03/SubString03.java new file mode 100644 index 00000000000..33fe0f25d11 --- /dev/null +++ b/regression/strings/SubString03/SubString03.java @@ -0,0 +1,9 @@ +public class SubString03 +{ + public static void main(String[] args) + { + String letters = "automatictestcasegenerationatdiffblue"; + String tmp=letters.substring(9, 13); + assert tmp.equals("teest"); + } +} diff --git a/regression/strings/SubString03/test.desc b/regression/strings/SubString03/test.desc new file mode 100644 index 00000000000..2b8db21a829 --- /dev/null +++ b/regression/strings/SubString03/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +SubString03.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/TokenTest01/TokenTest01.class b/regression/strings/TokenTest01/TokenTest01.class new file mode 100644 index 00000000000..70e112fbafb Binary files /dev/null and b/regression/strings/TokenTest01/TokenTest01.class differ diff --git a/regression/strings/TokenTest01/TokenTest01.java b/regression/strings/TokenTest01/TokenTest01.java new file mode 100644 index 00000000000..2180bc94c1d --- /dev/null +++ b/regression/strings/TokenTest01/TokenTest01.java @@ -0,0 +1,24 @@ +import java.util.StringTokenizer; + +public class TokenTest01 +{ + public static void main(String[] args) + { + String sentence = "automatic test case generation"; + String[] tokens = sentence.split(" "); + System.out.printf("Number of elements: %d\nThe tokens are:\n", + tokens.length); + assert tokens.length==4; + + int i=0; + for (String token : tokens) + { + System.out.println(token); + if (i==0) assert token.equals("automatic"); + else if (i==1) assert token.equals("test"); + else if (i==2) assert token.equals("case"); + else if (i==3) assert token.equals("generation"); + ++i; + } + } +} diff --git a/regression/strings/TokenTest01/test.desc b/regression/strings/TokenTest01/test.desc new file mode 100644 index 00000000000..02a11e8e392 --- /dev/null +++ b/regression/strings/TokenTest01/test.desc @@ -0,0 +1,8 @@ +FUTURE +TokenTest01.class +--string-refine --unwind 30 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/TokenTest02/TokenTest02.class b/regression/strings/TokenTest02/TokenTest02.class new file mode 100644 index 00000000000..09f38782aa1 Binary files /dev/null and b/regression/strings/TokenTest02/TokenTest02.class differ diff --git a/regression/strings/TokenTest02/TokenTest02.java b/regression/strings/TokenTest02/TokenTest02.java new file mode 100644 index 00000000000..944d0a169a0 --- /dev/null +++ b/regression/strings/TokenTest02/TokenTest02.java @@ -0,0 +1,17 @@ +import java.util.StringTokenizer; + +public class TokenTest02 +{ + public static void main(String[] args) + { + String sentence = "automatic test case generation"; + String[] tokens = sentence.split(" "); + + int i=0; + for (String token : tokens) + { + if (i==3) assert token.equals("genneration"); + ++i; + } + } +} diff --git a/regression/strings/TokenTest02/test.desc b/regression/strings/TokenTest02/test.desc new file mode 100644 index 00000000000..3bcf7505e25 --- /dev/null +++ b/regression/strings/TokenTest02/test.desc @@ -0,0 +1,8 @@ +FUTURE +TokenTest02.class +--string-refine --unwind 15 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/strings/Validate01/Validate01.class b/regression/strings/Validate01/Validate01.class new file mode 100644 index 00000000000..a5a99f5efc1 Binary files /dev/null and b/regression/strings/Validate01/Validate01.class differ diff --git a/regression/strings/Validate01/Validate01.java b/regression/strings/Validate01/Validate01.java new file mode 100644 index 00000000000..3443cd30588 --- /dev/null +++ b/regression/strings/Validate01/Validate01.java @@ -0,0 +1,30 @@ +public class Validate01 +{ + public static void main(String[] args) + { + String firstName = "XXX"; + String lastName = "YYY"; + String address = "ZZZ IIII AAAA 5689"; + String city = "Oxford"; + String state = "Oxfordshire"; + String zip = "OX37AF"; + String phone = "+4477777"; + + if (!ValidateInput01.validateFirstName(firstName)) + assert false; + else if (!ValidateInput01.validateLastName(lastName)) + assert false; + else if (!ValidateInput01.validateAddress(address)) + System.out.println("Invalid address"); + else if (!ValidateInput01.validateCity(city)) + assert false; + else if (!ValidateInput01.validateState(state)) + assert false; + else if (!ValidateInput01.validateZip(zip)) + System.out.println("Invalid zip code"); + else if (!ValidateInput01.validatePhone(phone)) + System.out.println("Invalid phone number"); + else + System.out.println("Valid input. Thank you."); + } +} diff --git a/regression/strings/Validate01/ValidateInput01.class b/regression/strings/Validate01/ValidateInput01.class new file mode 100644 index 00000000000..5efab9300fc Binary files /dev/null and b/regression/strings/Validate01/ValidateInput01.class differ diff --git a/regression/strings/Validate01/ValidateInput01.java b/regression/strings/Validate01/ValidateInput01.java new file mode 100644 index 00000000000..961b02f2d30 --- /dev/null +++ b/regression/strings/Validate01/ValidateInput01.java @@ -0,0 +1,38 @@ +public class ValidateInput01 +{ + public static boolean validateFirstName(String firstName) + { + return firstName.matches("[A-Z][a-zA-Z]*"); + } + + public static boolean validateLastName(String lastName) + { + return lastName.matches("[a-zA-z]+(['-][a-zA-Z]+)*"); + } + + public static boolean validateAddress(String address) + { + return address.matches( + "\\d+\\s+([a-zA-Z]+|[a-zA-Z]+\\s[a-zA-Z]+)"); + } + + public static boolean validateCity(String city) + { + return city.matches("([a-zA-Z]+|[a-zA-Z]+\\s[a-zA-Z]+)"); + } + + public static boolean validateState(String state) + { + return state.matches("([a-zA-Z]+|[a-zA-Z]+\\s[a-zA-Z]+)") ; + } + + public static boolean validateZip(String zip) + { + return zip.matches("\\d{5}"); + } + + public static boolean validatePhone(String phone) + { + return phone.matches("[1-9]\\d{2}-[1-9]\\d{2}-\\d{4}"); + } +} diff --git a/regression/strings/Validate01/test.desc b/regression/strings/Validate01/test.desc new file mode 100644 index 00000000000..e797b2735aa --- /dev/null +++ b/regression/strings/Validate01/test.desc @@ -0,0 +1,8 @@ +FUTURE +Validate01.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/strings/Validate02/Validate02.class b/regression/strings/Validate02/Validate02.class new file mode 100644 index 00000000000..1d9ddd04737 Binary files /dev/null and b/regression/strings/Validate02/Validate02.class differ diff --git a/regression/strings/Validate02/Validate02.java b/regression/strings/Validate02/Validate02.java new file mode 100644 index 00000000000..7f59d706e8c --- /dev/null +++ b/regression/strings/Validate02/Validate02.java @@ -0,0 +1,22 @@ +public class Validate02 +{ + public static void main(String[] args) + { + String address = "ZZZ IIII AAAA 5689"; + String city = "Oxford"; + String state = "Oxfordshire"; + String zip = "OX37AF"; + String phone = "+4477777"; + + if (!ValidateInput02.validateAddress(address)) + assert false; + else if (!ValidateInput02.validateCity(city)) + System.out.println("Invalid city"); + else if (!ValidateInput02.validateState(state)) + System.out.println("Invalid state"); + else if (!ValidateInput02.validateZip(zip)) + System.out.println("Invalid zip code"); + else + System.out.println("Valid input. Thank you."); + } +} diff --git a/regression/strings/Validate02/ValidateInput02.class b/regression/strings/Validate02/ValidateInput02.class new file mode 100644 index 00000000000..8aabb3aea58 Binary files /dev/null and b/regression/strings/Validate02/ValidateInput02.class differ diff --git a/regression/strings/Validate02/ValidateInput02.java b/regression/strings/Validate02/ValidateInput02.java new file mode 100644 index 00000000000..ac21ba620ba --- /dev/null +++ b/regression/strings/Validate02/ValidateInput02.java @@ -0,0 +1,38 @@ +public class ValidateInput02 +{ + public static boolean validateFirstName(String firstName) + { + return firstName.matches("[A-Z][a-zA-Z]*"); + } + + public static boolean validateLastName(String lastName) + { + return lastName.matches("[a-zA-z]+(['-][a-zA-Z]+)*"); + } + + public static boolean validateAddress(String address) + { + return address.matches( + "\\d+\\s+([a-zA-Z]+|[a-zA-Z]+\\s[a-zA-Z]+)"); + } + + public static boolean validateCity(String city) + { + return city.matches("([a-zA-Z]+|[a-zA-Z]+\\s[a-zA-Z]+)"); + } + + public static boolean validateState(String state) + { + return state.matches("([a-zA-Z]+|[a-zA-Z]+\\s[a-zA-Z]+)") ; + } + + public static boolean validateZip(String zip) + { + return zip.matches("\\d{5}"); + } + + public static boolean validatePhone(String phone) + { + return phone.matches("[1-9]\\d{2}-[1-9]\\d{2}-\\d{4}"); + } +} diff --git a/regression/strings/Validate02/test.desc b/regression/strings/Validate02/test.desc new file mode 100644 index 00000000000..b30016bf880 --- /dev/null +++ b/regression/strings/Validate02/test.desc @@ -0,0 +1,8 @@ +FUTURE +Validate02.class +--string-refine +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/scripts/bash-autocomplete/.gitignore b/scripts/bash-autocomplete/.gitignore new file mode 100644 index 00000000000..1e0acedc4f2 --- /dev/null +++ b/scripts/bash-autocomplete/.gitignore @@ -0,0 +1 @@ +cbmc.sh diff --git a/scripts/bash-autocomplete/Readme.md b/scripts/bash-autocomplete/Readme.md new file mode 100644 index 00000000000..00101d99159 --- /dev/null +++ b/scripts/bash-autocomplete/Readme.md @@ -0,0 +1,31 @@ +# CBMC Autocomplete Scripts for Bash +This directory contains an autocomplete script for bash. +## Installation +1. Compile cbmc and + +2. `cd scripts/bash-autocomplete` + +3. `./extract-switches.sh` + +4. Put the following at the end of you in your `~/.bashrc`, with the directories adapted to your directory structure: + ```bash + cbmcautocomplete=~/diffblue/cbmc/scripts/bash-autocomplete/cbmc.sh + if [ -f $cbmcautocomplete ]; then + . $cbmcautocomplete + fi + ``` +## Usage +As with the usual autocomplete in bash, start typing a switch to complete it, for example: +``` +cbmc --clas +``` +will complete to +``` +cbmc --classpath +``` + +## Features implemented + +* Completing all switches +* Completing values for `--cover`, `--mm` and `--arch` +* When completing a name of a file to analyze, only files with supported extensions are shown. diff --git a/scripts/bash-autocomplete/cbmc.sh.template b/scripts/bash-autocomplete/cbmc.sh.template new file mode 100644 index 00000000000..cbd64762b2d --- /dev/null +++ b/scripts/bash-autocomplete/cbmc.sh.template @@ -0,0 +1,43 @@ +#!/bin/bash +_cbmc_autocomplete() +{ + #list of all switches cbmc has. IMPORTANT: in the template file, this variable must be defined on line 5. + local switches="" + #word on which the cursor is + local cur=${COMP_WORDS[COMP_CWORD]} + #previous word (in case it is a switch with a parameter) + local prev=${COMP_WORDS[COMP_CWORD-1]} + + #check if the command before cursor is a switch that takes parameters, if yes, + #offer a choice of parameters + case "$prev" in + --cover) #for coverage we list the options explicitly + COMPREPLY=( $( compgen -W "assertion path branch location decision condition mcdc cover" -- $cur ) ) + return 0 + ;; + --mm) #for memory models we list the options explicitly + COMPREPLY=( $( compgen -W "sc tso pso" -- $cur ) ) + return 0 + ;; + --arch) #for architecture we list the options explicitly + COMPREPLY=( $( compgen -W "i386 x86_64" -- $cur ) ) + return 0 + ;; + -I|--classpath|-cp|--outfile|--existing-coverage|--graphml-cex) + #a switch that takes a file parameter of which we don't know an extension + #TODO probably we can do more for -I, --classpath, -cp + _filedir + return 0 + ;; + esac + + #complete a switch from a standard list, if the parameter under cursor starts with a hyphen + if [[ "$cur" == -* ]]; then + COMPREPLY=( $( compgen -W "$switches" -- $cur ) ) + return 0 + fi + + #if none of the above applies, offer directories and files that we can analyze + _filedir "@(class|jar|cpp|cc|c\+\+|ii|cxx|c|i|gb)" +} +complete -F _cbmc_autocomplete cbmc diff --git a/scripts/bash-autocomplete/extract_switches.sh b/scripts/bash-autocomplete/extract_switches.sh new file mode 100755 index 00000000000..e000b469bea --- /dev/null +++ b/scripts/bash-autocomplete/extract_switches.sh @@ -0,0 +1,48 @@ +#!/bin/bash +echo "Compiling the helper file to extract the raw list of parameters from cbmc" +g++ -c -MMD -MP -std=c++11 -Wall -I ../../src/ -ftrack-macro-expansion=0 -fno-diagnostics-show-caret switch_extractor_helper.c -o tmp.o 2> pragma.txt + +retval=$? + +#clean up compiled files, we don't need them. +rm tmp.o 2> /dev/null +rm tmp.d 2> /dev/null + +#check if compilation went fine +if [ $retval -ne 0 ]; then + echo "Problem compiling the helper file, parameter list not extracted." + exit 1; +fi + +echo "Converting the raw parameter list to the format required by autocomplete scripts" +rawstring=`sed "s/^.*pragma message: \(.*\)/\1/" pragma.txt` +#delete pragma file, we won't need it +rm pragma.txt 2> /dev/null + +#now the main bit, convert from raw format to a proper list of switches +cleanstring=`( + #extract 2-hyphen switches, such as --foo + #grep for '(foo)' expressions, and then use sed to remove parantheses and put '--' at the start + (echo $rawstring | grep -o "([^)]*)" | sed "s/^.\(.*\).$/--\1/") ; + #extract 1-hyphen switches, such as -F + #use sed to remove all (foo) expressions, then you're left with switches and ':', so grep the colons out and then use sed to include the '-' + (echo $rawstring | sed "s/([^)]*)//g" | grep -o "[a-zA-Z0-9]" | sed "s/\(.*\)/-\1/") + ) | tr '\n' ' '` + +#sanity check that there is only one line of output +if [ `echo $cleanstring | wc -l | awk '{print $1}'` -ne 1 ]; then + echo "Problem converting the parameter list to the correct format, I was expecting one line but either got 0 or >2. This is likely to be an error in this conversion script." + exit 1; +fi + +#sanity check that there are no dangerous characters +echo $cleanstring | grep -q "[^a-zA-Z0-9 -]" +if [ $? -eq 0 ]; then + echo "Problem converting the parameter list to the correct format, illegal characters detected. This is likely to be an error in this conversion script." + exit 1; +fi + +echo "Injecting the parameter list to the autocomplete file." +sed "5 s/.*/ local switches=\"$cleanstring\"/" cbmc.sh.template > cbmc.sh + +rm pragma.txt 2> /dev/null diff --git a/scripts/bash-autocomplete/switch_extractor_helper.c b/scripts/bash-autocomplete/switch_extractor_helper.c new file mode 100644 index 00000000000..4d9cc2e56fe --- /dev/null +++ b/scripts/bash-autocomplete/switch_extractor_helper.c @@ -0,0 +1,3 @@ +#include "cbmc/cbmc_parse_options.h" + +#pragma message CBMC_OPTIONS diff --git a/src/Makefile b/src/Makefile index 7b9e3a1d446..e4c62f33eed 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,7 +1,7 @@ DIRS = ansi-c big-int cbmc cpp goto-cc goto-instrument goto-programs \ goto-symex langapi pointer-analysis solvers util linking xmllang \ - assembler analyses java_bytecode aa-path-symex path-symex musketeer \ - json cegis goto-analyzer jsil symex goto-diff aa-symex clobber \ + assembler analyses java_bytecode path-symex musketeer \ + json cegis goto-analyzer jsil symex goto-diff clobber \ memory-models all: cbmc.dir goto-cc.dir goto-instrument.dir symex.dir goto-analyzer.dir goto-diff.dir @@ -44,8 +44,6 @@ symex.dir: languages goto-programs.dir pointer-analysis.dir \ goto-symex.dir linking.dir analyses.dir solvers.dir \ path-symex.dir goto-instrument.dir -aa-symex.dir: symex.dir aa-path-symex.dir - # building for a particular directory $(patsubst %, %.dir, $(DIRS)): @@ -110,4 +108,12 @@ libzip-build: @echo "Building libzip" @(cd ../libzip; BASE=`pwd`; ./configure --with-zlib=$(BASE)/zlib ; make) -.PHONY: minisat2-download glucose-download zlib-download libzip-download libzip-build +cprover-jar-build: + @echo "Building org.cprover.jar" + @(cd java_bytecode/library/; \ + mkdir -p target; \ + javac -d target/ `find src/ -name "*.java"`; \ + cd target; jar cf org.cprover.jar `find . -name "*.class"`; \ + mv org.cprover.jar ../../../) + +.PHONY: minisat2-download glucose-download zlib-download libzip-download libzip-build cprover-jar-build diff --git a/src/aa-path-symex/Makefile b/src/aa-path-symex/Makefile deleted file mode 100644 index 9d3c4d96074..00000000000 --- a/src/aa-path-symex/Makefile +++ /dev/null @@ -1,15 +0,0 @@ -SRC = path_symex_state.cpp path_symex.cpp build_goto_trace.cpp - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = aa-path-symex$(LIBEXT) - -all: aa-path-symex$(LIBEXT) - -############################################################################### - -aa-path-symex$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/aa-path-symex/build_goto_trace.cpp b/src/aa-path-symex/build_goto_trace.cpp deleted file mode 120000 index a8d26f1b4bd..00000000000 --- a/src/aa-path-symex/build_goto_trace.cpp +++ /dev/null @@ -1 +0,0 @@ -../path-symex/build_goto_trace.cpp \ No newline at end of file diff --git a/src/aa-path-symex/build_goto_trace.h b/src/aa-path-symex/build_goto_trace.h deleted file mode 120000 index 3183a6b0910..00000000000 --- a/src/aa-path-symex/build_goto_trace.h +++ /dev/null @@ -1 +0,0 @@ -../path-symex/build_goto_trace.h \ No newline at end of file diff --git a/src/aa-path-symex/path_symex.cpp b/src/aa-path-symex/path_symex.cpp deleted file mode 100644 index f503f25c6e1..00000000000 --- a/src/aa-path-symex/path_symex.cpp +++ /dev/null @@ -1,1257 +0,0 @@ -/*******************************************************************\ - -Module: Concrete Symbolic Transformer - -Author: Daniel Kroening, kroening@kroening.com - Alex Horn, alex.horn@cs.ox.ac.uk - -\*******************************************************************/ - -#include -#include -#include -#include -#include - -#include - -#include - -#include "path_symex.h" - -// #define DEBUG - -#ifdef DEBUG -#include -#endif - -class path_symext -{ -public: - inline path_symext() - { - } - - void operator()( - path_symex_statet &state, - std::list &furter_states); - - void operator()(path_symex_statet &state); - - void do_goto( - path_symex_statet &state, - bool taken); - - void do_assert_fail(path_symex_statet &state) - { - const goto_programt::instructiont &instruction= - *state.get_instruction(); - - state.record_step(); - state.next_pc(); - exprt guard=state.read(not_exprt(instruction.guard)); - state.history->guard=guard; - } - -protected: - void do_goto( - path_symex_statet &state, - std::list &further_states); - - void function_call( - path_symex_statet &state, - const code_function_callt &call, - std::list &further_states) - { - exprt f=state.read(call.function()); - function_call_rec(state, call, f, further_states); - } - - void function_call_rec( - path_symex_statet &state, - const code_function_callt &function_call, - const exprt &function, - std::list &further_states); - - void return_from_function( - path_symex_statet &state, - const exprt &return_value); - - void symex_malloc( - path_symex_statet &state, - const exprt &lhs, - const side_effect_exprt &code); - - void assign( - path_symex_statet &state, - const exprt &lhs, - const exprt &rhs); - - inline void assign( - path_symex_statet &state, - const code_assignt &assignment) - { - assign(state, assignment.lhs(), assignment.rhs()); - } - - void assign_rec( - path_symex_statet &state, - exprt::operandst &guard, // instantiated - const exprt &ssa_lhs, // instantiated, recursion here - const exprt &ssa_rhs); // instantiated - - static bool propagate(const exprt &src); -}; - -/*******************************************************************\ - -Function: path_symext::propagate - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bool path_symext::propagate(const exprt &src) -{ - // propagate things that are 'simple enough' - if(src.is_constant()) - return true; - else if(src.id()==ID_member) - return propagate(to_member_expr(src).struct_op()); - else if(src.id()==ID_index) - return false; - else if(src.id()==ID_typecast) - return propagate(to_typecast_expr(src).op()); - else if(src.id()==ID_symbol) - return true; - else if(src.id()==ID_address_of) - return true; - else if(src.id()==ID_plus) - { - forall_operands(it, src) - if(!propagate(*it)) - return false; - return true; - } - else if(src.id()==ID_array) - { - forall_operands(it, src) - if(!propagate(*it)) - return false; - return true; - } - else if(src.id()==ID_vector) - { - forall_operands(it, src) - if(!propagate(*it)) - return false; - return true; - } - else if(src.id()==ID_if) - { - const if_exprt &if_expr=to_if_expr(src); - if(!propagate(if_expr.true_case()) || - !propagate(if_expr.false_case())) - return false; - - return true; - } - else if(src.id()==ID_array_of) - { - return propagate(to_array_of_expr(src).what()); - } - else if(src.id()==ID_union) - { - return propagate(to_union_expr(src).op()); - } - else - { - return false; - } -} - -/*******************************************************************\ - -Function: path_symext::assign - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_symext::assign( - path_symex_statet &state, - const exprt &lhs, - const exprt &rhs) -{ - if(rhs.id()==ID_side_effect) // catch side effects on rhs - { - const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs); - const irep_idt &statement=side_effect_expr.get_statement(); - - if(statement==ID_malloc) - { - symex_malloc(state, lhs, side_effect_expr); - return; - } - else if(statement==ID_nondet) - { - // done in statet:instantiate_rec - } - else - throw "unexpected side-effect on rhs: "+id2string(statement); - } - - // read the address of the lhs, with propagation - exprt lhs_address=state.read(address_of_exprt(lhs)); - - // now SSA the lhs, no propagation - exprt ssa_lhs= - state.read_no_propagate(dereference_exprt(lhs_address)); - - // read the rhs - exprt ssa_rhs=state.read(rhs); - - // start recursion on lhs - exprt::operandst _guard; // start with empty guard - assign_rec(state, _guard, ssa_lhs, ssa_rhs); -} - -/*******************************************************************\ - -Function: path_symext::symex_malloc - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -inline static typet c_sizeof_type_rec(const exprt &expr) -{ - const irept &sizeof_type=expr.find(ID_C_c_sizeof_type); - - if(!sizeof_type.is_nil()) - { - return static_cast(sizeof_type); - } - else if(expr.id()==ID_mult) - { - forall_operands(it, expr) - { - typet t=c_sizeof_type_rec(*it); - if(t.is_not_nil()) - return t; - } - } - - return nil_typet(); -} - -void path_symext::symex_malloc( - path_symex_statet &state, - const exprt &lhs, - const side_effect_exprt &code) -{ - if(code.operands().size()!=1) - throw "malloc expected to have one operand"; - - // increment dynamic object counter - unsigned dynamic_count=++state.var_map.dynamic_count; - - exprt size=code.op0(); - typet object_type=nil_typet(); - - { - exprt tmp_size=state.read(size); // to allow constant propagation - - // special treatment for sizeof(T)*x - if(tmp_size.id()==ID_mult && - tmp_size.operands().size()==2 && - tmp_size.op0().find(ID_C_c_sizeof_type).is_not_nil()) - { - object_type=array_typet( - c_sizeof_type_rec(tmp_size.op0()), - tmp_size.op1()); - } - else - { - typet tmp_type=c_sizeof_type_rec(tmp_size); - - if(tmp_type.is_not_nil()) - { - // Did the size get multiplied? - mp_integer elem_size=pointer_offset_size(tmp_type, state.var_map.ns); - mp_integer alloc_size; - if(elem_size<0 || to_integer(tmp_size, alloc_size)) - { - } - else - { - if(alloc_size==elem_size) - object_type=tmp_type; - else - { - mp_integer elements=alloc_size/elem_size; - - if(elements*elem_size==alloc_size) - object_type= - array_typet(tmp_type, from_integer(elements, tmp_size.type())); - } - } - } - } - - if(object_type.is_nil()) - object_type=array_typet(unsigned_char_type(), tmp_size); - - // we introduce a fresh symbol for the size - // to prevent any issues of the size getting ever changed - - if(object_type.id()==ID_array && - !to_array_type(object_type).size().is_constant()) - { - exprt &size=to_array_type(object_type).size(); - - symbolt size_symbol; - - size_symbol.base_name="dynamic_object_size"+std::to_string(dynamic_count); - size_symbol.name="symex::"+id2string(size_symbol.base_name); - size_symbol.is_lvalue=true; - size_symbol.type=tmp_size.type(); - size_symbol.mode=ID_C; - - assign(state, - size_symbol.symbol_expr(), - size); - - size=size_symbol.symbol_expr(); - } - } - - // value - symbolt value_symbol; - - value_symbol.base_name= - "dynamic_object"+std::to_string(state.var_map.dynamic_count); - value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name); - value_symbol.is_lvalue=true; - value_symbol.type=object_type; - value_symbol.type.set("#dynamic", true); - value_symbol.mode=ID_C; - - address_of_exprt rhs; - - if(object_type.id()==ID_array) - { - rhs.type()=pointer_typet(value_symbol.type.subtype()); - index_exprt index_expr(value_symbol.type.subtype()); - index_expr.array()=value_symbol.symbol_expr(); - index_expr.index()=from_integer(0, index_type()); - rhs.op0()=index_expr; - } - else - { - rhs.op0()=value_symbol.symbol_expr(); - rhs.type()=pointer_typet(value_symbol.type); - } - - if(rhs.type()!=lhs.type()) - rhs.make_typecast(lhs.type()); - - assign(state, lhs, rhs); -} - -/*******************************************************************\ - -Function: path_symext::assign_rec - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_symext::assign_rec( - path_symex_statet &state, - exprt::operandst &guard, - const exprt &ssa_lhs, - const exprt &ssa_rhs) -{ - // const typet &ssa_lhs_type=state.var_map.ns.follow(ssa_lhs.type()); - - #ifdef DEBUG - std::cout << "assign_rec: " << ssa_lhs.pretty() << std::endl; - // std::cout << "ssa_lhs_type: " << ssa_lhs_type.id() << std::endl; - #endif - - if(ssa_lhs.id()==ID_symbol) - { - // These are expected to be SSA symbols - assert(ssa_lhs.get_bool(ID_C_SSA_symbol)); - - const symbol_exprt &symbol_expr=to_symbol_expr(ssa_lhs); - const irep_idt &full_identifier=symbol_expr.get(ID_C_full_identifier); - - #ifdef DEBUG - const irep_idt &ssa_identifier=symbol_expr.get_identifier(); - std::cout << "SSA symbol identifier: " << ssa_identifier << std::endl; - std::cout << "full identifier: " << full_identifier << std::endl; - #endif - - var_mapt::var_infot &var_info=state.var_map[full_identifier]; - assert(var_info.full_identifier==full_identifier); - - // increase the SSA counter and produce new SSA symbol expression - var_info.increment_ssa_counter(); - symbol_exprt new_lhs=var_info.ssa_symbol(); - - #ifdef DEBUG - std::cout << "new_lhs: " << new_lhs.get_identifier() << std::endl; - #endif - - // record new state of lhs - { - // reference is not stable - path_symex_statet::var_statet &var_state=state.get_var_state(var_info); - var_state.ssa_symbol=new_lhs; - } - - // rhs nil means non-det assignment - if(ssa_rhs.is_nil()) - { - path_symex_statet::var_statet &var_state=state.get_var_state(var_info); - var_state.value=nil_exprt(); - } - else - { - // consistency check - if(!base_type_eq(ssa_rhs.type(), new_lhs.type(), state.var_map.ns)) - { - #ifdef DEBUG - std::cout << "ssa_rhs: " << ssa_rhs.pretty() << std::endl; - std::cout << "new_lhs: " << new_lhs.pretty() << std::endl; - #endif - throw "assign_rec got different types"; - } - - // record the step - state.record_step(); - path_symex_stept &step=*state.history; - - if(!guard.empty()) - step.guard=conjunction(guard); - step.full_lhs=ssa_lhs; - step.ssa_lhs=new_lhs; - step.ssa_rhs=ssa_rhs; - - // propagate the rhs? - path_symex_statet::var_statet &var_state=state.get_var_state(var_info); - var_state.value=propagate(ssa_rhs)?ssa_rhs:nil_exprt(); - } - } - else if(ssa_lhs.id()==ID_member) - { - #ifdef DEBUG - std::cout << "assign_rec ID_member" << std::endl; - #endif - - const member_exprt &ssa_lhs_member_expr=to_member_expr(ssa_lhs); - const exprt &struct_op=ssa_lhs_member_expr.struct_op(); - - const typet &compound_type= - state.var_map.ns.follow(struct_op.type()); - - if(compound_type.id()==ID_struct) - { - // We flatten the top-level structs, so this one is inside an - // array or a union. - - exprt member_name(ID_member_name); - member_name.set( - ID_component_name, - ssa_lhs_member_expr.get_component_name()); - - with_exprt new_rhs(struct_op, member_name, ssa_rhs); - - assign_rec(state, guard, struct_op, new_rhs); - } - else if(compound_type.id()==ID_union) - { - // rewrite into byte_extract, and do again - exprt offset=from_integer(0, index_type()); - - byte_extract_exprt - new_lhs(byte_update_id(), struct_op, offset, ssa_rhs.type()); - - assign_rec(state, guard, new_lhs, ssa_rhs); - } - else - throw "assign_rec: member expects struct or union type"; - } - else if(ssa_lhs.id()==ID_index) - { - #ifdef DEBUG - std::cout << "assign_rec ID_index" << std::endl; - #endif - - throw "unexpected array index on lhs"; - } - else if(ssa_lhs.id()==ID_dereference) - { - #ifdef DEBUG - std::cout << "assign_rec ID_dereference" << std::endl; - #endif - - throw "unexpected dereference on lhs"; - } - else if(ssa_lhs.id()==ID_if) - { - #ifdef DEBUG - std::cout << "assign_rec ID_if" << std::endl; - #endif - - const if_exprt &lhs_if_expr=to_if_expr(ssa_lhs); - exprt cond=lhs_if_expr.cond(); - - // true - guard.push_back(cond); - assign_rec(state, guard, lhs_if_expr.true_case(), ssa_rhs); - guard.pop_back(); - - // false - guard.push_back(not_exprt(cond)); - assign_rec(state, guard, lhs_if_expr.false_case(), ssa_rhs); - guard.pop_back(); - } - else if(ssa_lhs.id()==ID_byte_extract_little_endian || - ssa_lhs.id()==ID_byte_extract_big_endian) - { - #ifdef DEBUG - std::cout << "assign_rec ID_byte_extract" << std::endl; - #endif - - const byte_extract_exprt &byte_extract_expr= - to_byte_extract_expr(ssa_lhs); - - // assignment to byte_extract operators: - // turn into byte_update operator - - irep_idt new_id; - - if(ssa_lhs.id()==ID_byte_extract_little_endian) - new_id=ID_byte_update_little_endian; - else if(ssa_lhs.id()==ID_byte_extract_big_endian) - new_id=ID_byte_update_big_endian; - else - assert(false); - - byte_update_exprt new_rhs(new_id); - - new_rhs.type()=byte_extract_expr.op().type(); - new_rhs.op()=byte_extract_expr.op(); - new_rhs.offset()=byte_extract_expr.offset(); - new_rhs.value()=ssa_rhs; - - const exprt new_lhs=byte_extract_expr.op(); - - assign_rec(state, guard, new_lhs, new_rhs); - } - else if(ssa_lhs.id()==ID_struct) - { - const struct_typet &struct_type= - to_struct_type(state.var_map.ns.follow(ssa_lhs.type())); - const struct_typet::componentst &components= - struct_type.components(); - - // split up into components - const exprt::operandst &operands=ssa_lhs.operands(); - - assert(operands.size()==components.size()); - - for(std::size_t i=0; i &further_states) -{ - #ifdef DEBUG - std::cout << "function_call_rec: " << function.pretty() << std::endl; - #endif - - if(function.id()==ID_symbol) - { - const irep_idt &function_identifier= - to_symbol_expr(function).get_identifier(); - - // find the function - locst::function_mapt::const_iterator f_it= - state.locs.function_map.find(function_identifier); - - if(f_it==state.locs.function_map.end()) - throw - "failed to find `"+id2string(function_identifier)+ - "' in function_map"; - - const locst::function_entryt &function_entry=f_it->second; - - loc_reft function_entry_point=function_entry.first_loc; - - // do we have a body? - if(function_entry_point==loc_reft()) - { - // no body - - // this is a skip - if(call.lhs().is_not_nil()) - assign(state, call.lhs(), nil_exprt()); - - state.next_pc(); - return; - } - - // push a frame on the call stack - path_symex_statet::threadt &thread= - state.threads[state.get_current_thread()]; - thread.call_stack.push_back(path_symex_statet::framet()); - thread.call_stack.back().current_function=function_identifier; - thread.call_stack.back().return_location=thread.pc.next_loc(); - thread.call_stack.back().return_lhs=call.lhs(); - thread.call_stack.back().saved_local_vars=thread.local_vars; - - - const code_typet &code_type=function_entry.type; - - const code_typet::parameterst &function_parameters=code_type.parameters(); - - const exprt::operandst &call_arguments=call.arguments(); - - // now assign the argument values to parameters - for(std::size_t i=0; iguard=not_exprt(guard); - function_call_rec( - further_states.back(), call, if_expr.false_case(), further_states); - } - - // do the true-case in 'state' - { - state.record_branch_step(true); - state.history->guard=guard; - function_call_rec(state, call, if_expr.true_case(), further_states); - } - } - } - else - // NOLINTNEXTLINE(readability/throw) as message is correctly uppercase - throw "TODO: function_call "+function.id_string(); -} - -/*******************************************************************\ - -Function: path_symext::return_from_function - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_symext::return_from_function( - path_symex_statet &state, - const exprt &return_value) -{ - path_symex_statet::threadt &thread=state.threads[state.get_current_thread()]; - - // returning from very last function? - if(thread.call_stack.empty()) - { - state.disable_current_thread(); - } - else - { - // update statistics - state.recursion_map[thread.call_stack.back().current_function]--; - - // set PC to return location - thread.pc=thread.call_stack.back().return_location; - - // assign the return value - if(return_value.is_not_nil() && - thread.call_stack.back().return_lhs.is_not_nil()) - assign(state, thread.call_stack.back().return_lhs, return_value); - - thread.call_stack.pop_back(); - } -} - -/*******************************************************************\ - -Function: path_symext::do_goto - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_symext::do_goto( - path_symex_statet &state, - std::list &further_states) -{ - const goto_programt::instructiont &instruction= - *state.get_instruction(); - - if(instruction.is_backwards_goto()) - { - // we keep a statistic on how many times we execute backwards gotos - state.unwinding_map[state.pc()]++; - } - - const loct &loc=state.locs[state.pc()]; - assert(!loc.branch_target.is_nil()); - - exprt guard=state.read(instruction.guard); - - if(guard.is_true()) // branch taken always - { - state.record_branch_step(true); - state.set_pc(loc.branch_target); - return; // we are done - } - -#ifdef PATH_SYMEX_FORK - pid_t pid=-1; -#endif - - if(!guard.is_false()) - { - // branch taken case - -#ifdef PATH_SYMEX_FORK - pid=fork(); - if(pid==0) - { - // "state" is stored in "further_states" - assert(!further_states.empty()); - - // child process explores paths starting from the - // new state thereby partitioning the search space - std::list::iterator - s_it=further_states.begin(), s_end=further_states.end(); - while(s_it!=s_end) - { - if(&(*s_it)!=&state) - // iterators in std::list are stable - s_it=further_states.erase(s_it); - else - ++s_it; - } - - assert(further_states.size()==1); - - // branch not taken case - state.record_branch_step(false); - state.set_pc(loc.branch_target); - state.history->guard=guard; - } -#endif - -#ifdef PATH_SYMEX_FORK - // forking failed so continue as if PATH_SYMEX_FORK were undefined - if(pid==-1) // NOLINT(readability/braces) -#endif - { -#ifdef PATH_SYMEX_LAZY_STATE - // lazily copy the state into 'further_states' - further_states.push_back(path_symex_statet::lazy_copy(state)); - further_states.back().record_true_branch(); -#else - // eagerly copy the state into 'further_states' - further_states.push_back(state); - further_states.back().record_branch_step(true); - further_states.back().set_pc(loc.branch_target); - further_states.back().history->guard=guard; -#endif - } - } - -#ifdef PATH_SYMEX_FORK - // parent process (regardless of any possible fork errors) - // should finish to explore all current 'further_states' - if(pid!=0) // NOLINT(readability/braces) -#endif - { - // branch not taken case - exprt negated_guard=not_exprt(guard); - state.record_branch_step(false); - state.next_pc(); - state.history->guard=negated_guard; - } -} - -/*******************************************************************\ - -Function: path_symext::do_goto - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_symext::do_goto( - path_symex_statet &state, - bool taken) -{ - state.record_step(); - - const goto_programt::instructiont &instruction= - *state.get_instruction(); - - if(instruction.is_backwards_goto()) - { - // we keep a statistic on how many times we execute backwards gotos - state.unwinding_map[state.pc()]++; - } - - exprt guard=state.read(instruction.guard); - - if(taken) - { - // branch taken case - const loct &loc=state.locs[state.pc()]; - assert(!loc.branch_target.is_nil()); - state.set_pc(loc.branch_target); - state.history->guard=guard; - } - else - { - // branch not taken case - exprt negated_guard=not_exprt(guard); - state.next_pc(); - state.history->guard=negated_guard; - } -} - -/*******************************************************************\ - -Function: path_symext::operator() - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_symext::operator()( - path_symex_statet &state, - std::list &further_states) -{ - const goto_programt::instructiont &instruction= - *state.get_instruction(); - - #ifdef DEBUG - std::cout << "path_symext::operator(): " << instruction.type - << std::endl; - #endif - - switch(instruction.type) - { - case END_FUNCTION: - // pop the call stack - state.record_step(); - return_from_function(state, nil_exprt()); - break; - - case RETURN: - // pop the call stack - { - state.record_step(); - exprt return_val=instruction.code.operands().size()==1? - instruction.code.op0():nil_exprt(); - return_from_function(state, return_val); - } - break; - - case START_THREAD: - { - const loct &loc=state.locs[state.pc()]; - assert(!loc.branch_target.is_nil()); - - state.record_step(); - state.next_pc(); - - // ordering of the following matters due to vector instability - path_symex_statet::threadt &new_thread=state.add_thread(); - path_symex_statet::threadt &old_thread= - state.threads[state.get_current_thread()]; - new_thread.pc=loc.branch_target; - new_thread.local_vars=old_thread.local_vars; - } - break; - - case END_THREAD: - state.record_step(); - state.disable_current_thread(); - break; - - case GOTO: - if(state.is_lazy()) - do_goto(state, state.restore_branch()); - else - do_goto(state, further_states); - break; - - case CATCH: - // ignore for now - state.record_step(); - state.next_pc(); - break; - - case THROW: - state.record_step(); - throw "THROW not yet implemented"; // NOLINT(readability/throw) - - case ASSUME: - state.record_step(); - state.next_pc(); - if(instruction.guard.is_false()) - state.disable_current_thread(); - else - { - exprt guard=state.read(instruction.guard); - state.history->guard=guard; - } - break; - - case ASSERT: - case SKIP: - case LOCATION: - case DEAD: - state.record_step(); - state.next_pc(); - break; - - case DECL: - // assigning an RHS of NIL means 'nondet' - assign(state, to_code_decl(instruction.code).symbol(), nil_exprt()); - state.next_pc(); - break; - - case ATOMIC_BEGIN: - if(state.inside_atomic_section) - throw "nested ATOMIC_BEGIN"; - - state.record_step(); - state.next_pc(); - state.inside_atomic_section=true; - break; - - case ATOMIC_END: - if(!state.inside_atomic_section) - throw "ATOMIC_END unmatched"; // NOLINT(readability/throw) - - state.record_step(); - state.next_pc(); - state.inside_atomic_section=false; - break; - - case ASSIGN: - assign(state, to_code_assign(instruction.code)); - state.next_pc(); - break; - - case FUNCTION_CALL: - state.record_step(); - function_call( - state, to_code_function_call(instruction.code), further_states); - break; - - case OTHER: - state.record_step(); - - { - const codet &code=instruction.code; - const irep_idt &statement=code.get_statement(); - - if(statement==ID_expression) - { - // like SKIP - } - else if(statement==ID_printf) - { - // ignore for now (should record stuff printed) - } - else if(statement==ID_asm) - { - // ignore for now - } - else if(statement==ID_fence) - { - // ignore for SC - } - else if(statement==ID_input) - { - // just needs to be recorded - } - else - throw "unexpected OTHER statement: "+id2string(statement); - } - - state.next_pc(); - break; - - default: - throw "path_symext: unexpected instruction"; - } -} - -/*******************************************************************\ - -Function: path_symext::operator() - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_symext::operator()(path_symex_statet &state) -{ - std::list further_states; - operator()(state, further_states); - if(!further_states.empty()) - throw "path_symext got unexpected further states"; -} - -/*******************************************************************\ - -Function: path_symex - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_symex( - path_symex_statet &state, - std::list &further_states) -{ - // "state" is stored in "further_states" - assert(!further_states.empty()); - - path_symext path_symex; - path_symex(state, further_states); -} - -/*******************************************************************\ - -Function: path_symex - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_symex(path_symex_statet &state) -{ - path_symext path_symex; - path_symex(state); -} - -/*******************************************************************\ - -Function: path_symex_goto - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_symex_goto( - path_symex_statet &state, - bool taken) -{ - path_symext path_symex; - path_symex.do_goto(state, taken); -} - -/*******************************************************************\ - -Function: path_symex_assert_fail - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_symex_assert_fail(path_symex_statet &state) -{ - path_symext path_symex; - path_symex.do_assert_fail(state); -} diff --git a/src/aa-path-symex/path_symex.h b/src/aa-path-symex/path_symex.h deleted file mode 120000 index 538d30846d4..00000000000 --- a/src/aa-path-symex/path_symex.h +++ /dev/null @@ -1 +0,0 @@ -../path-symex/path_symex.h \ No newline at end of file diff --git a/src/aa-path-symex/path_symex_state.cpp b/src/aa-path-symex/path_symex_state.cpp deleted file mode 100644 index b0c502f639d..00000000000 --- a/src/aa-path-symex/path_symex_state.cpp +++ /dev/null @@ -1,799 +0,0 @@ -/*******************************************************************\ - -Module: State of path-based symbolic simulator - -Author: Daniel Kroening, kroening@kroening.com - Alex Horn, alex.horn@cs.ox.ac.uk - -\*******************************************************************/ - -#include -#include -#include - -#include - -#include - -#include -#include - -#include "path_symex_state.h" - -// #define DEBUG - -#ifdef DEBUG -#include -#include -#endif - -/*******************************************************************\ - -Function: initial_state - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -path_symex_statet initial_state( - var_mapt &var_map, - const locst &locs, - path_symex_historyt &path_symex_history) -{ - return path_symex_statet( - var_map, - locs, - path_symex_step_reft(path_symex_history), - path_symex_statet::branchest()); -} - -/*******************************************************************\ - -Function: path_symex_statet::output - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -goto_programt::const_targett path_symex_statet::get_instruction() const -{ - assert(current_thread " << tmp.pretty() << std::endl; - #endif - - return tmp5; -} - -/*******************************************************************\ - -Function: path_symex_statet::instantiate_rec - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -exprt path_symex_statet::instantiate_rec( - const exprt &src, - bool propagate) -{ - #ifdef DEBUG - std::cout << "instantiate_rec: " - << from_expr(var_map.ns, "", src) << std::endl; - #endif - - const typet &src_type=var_map.ns.follow(src.type()); - - if(src_type.id()==ID_struct) // src is a struct - { - const struct_typet &struct_type=to_struct_type(src_type); - const struct_typet::componentst &components=struct_type.components(); - - struct_exprt result(src.type()); - result.operands().resize(components.size()); - - // split it up into components - for(unsigned i=0; ithread_nr!=current_thread) - no_thread_interleavings++; - - // update our statistics - depth++; - - // add the step - history.generate_successor(); - path_symex_stept &step=*history; - - // copy PC - assert(current_threadis_goto()); - -#ifdef PATH_SYMEX_LAZY_BRANCH - if(!branches.empty() || history.is_nil()) -#endif - { - // get_branches() relies on branch decisions - branches.push_back(taken); - - if(get_instruction()->is_goto()) - { - branches_restore++; - } - else - { - assert(pc()==locs.entry_loc); - assert(history.is_nil()); - } - } - - record_step(); -} - -/*******************************************************************\ - -Function: path_symex_statet::is_feasible - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bool path_symex_statet::is_feasible( - decision_proceduret &decision_procedure) const -{ - // feed path constraint to decision procedure - decision_procedure << history; - - // check whether SAT - switch(decision_procedure()) - { - case decision_proceduret::D_SATISFIABLE: return true; - - case decision_proceduret::D_UNSATISFIABLE: return false; - - case decision_proceduret::D_ERROR: throw "error from decision procedure"; - } - - return true; // not really reachable -} - -/*******************************************************************\ - -Function: path_symex_statet::check_assertion - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bool path_symex_statet::check_assertion( - decision_proceduret &decision_procedure) -{ - const goto_programt::instructiont &instruction=*get_instruction(); - - // assert that this is an assertion - assert(instruction.is_assert()); - - // the assertion in SSA - exprt assertion=read(instruction.guard); - - // trivial? - if(assertion.is_true()) - return true; // no error - - // the path constraint - decision_procedure << history; - - // negate the assertion - decision_procedure.set_to(assertion, false); - - // check whether SAT - switch(decision_procedure.dec_solve()) - { - case decision_proceduret::D_SATISFIABLE: - return false; // error - - case decision_proceduret::D_UNSATISFIABLE: - return true; // no error - - default: - throw "error from decision procedure"; - } - - return true; // not really reachable -} diff --git a/src/aa-path-symex/path_symex_state.h b/src/aa-path-symex/path_symex_state.h deleted file mode 100644 index dd10e43d8da..00000000000 --- a/src/aa-path-symex/path_symex_state.h +++ /dev/null @@ -1,350 +0,0 @@ -/*******************************************************************\ - -Module: State of path-based symbolic simulator - -Author: Daniel Kroening, kroening@kroening.com - Alex Horn, alex.horn@cs.ox.ac.uk - -\*******************************************************************/ - -#ifndef CPROVER_AA_PATH_SYMEX_PATH_SYMEX_STATE_H -#define CPROVER_AA_PATH_SYMEX_PATH_SYMEX_STATE_H - -#include - -#include -#include -#include - -// These variables may be defined in this header file only because -// it is (transitively) included by many essential path-symex files. -// In addition, since these variables determine how states are -// handled, it makes sense to define them in this header file. -#define PATH_SYMEX_LAZY_STATE -#define PATH_SYMEX_FORK - -// This flag is particularly useful for regression testing purposes. -// -// If PATH_SYMEX_LAZY_BRANCH is undefined, then branches are always -// recorded and the control logic in get_branches() is bypassed. But -// the output of path_search() should be identical in this setting; -// otherwise, the assumptions about GOTO programs or the history -// data structure should be revisited. -#define PATH_SYMEX_LAZY_BRANCH - -// check POSIX-compliance -#ifdef PATH_SYMEX_FORK -#if defined(__linux__) || \ - defined(__FreeBSD_kernel__) || \ - defined(__GNU__) || \ - defined(__unix__) || \ - defined(__CYGWIN__) || \ - defined(__MACH__) -#include -#include -#else -#error Cannot define PATH_SYMEX_FORK on non-POSIX systems -#endif -#endif - -class path_symex_statet -{ -public: - // use symbolic execution to repopulate composite fields - - // TODO: consider std::bitset or chaining to shrink state size - typedef std::vector branchest; - - // if _branches.empty(), then initial state; otherwise, lazy state - - // \post: pc() is the entry point to the program under scrutiny - path_symex_statet( - var_mapt &_var_map, - const locst &_locs, - path_symex_step_reft _history, - const branchest &_branches): - var_map(_var_map), - locs(_locs), - shared_vars(), - threads(), - inside_atomic_section(), - history(_history), - unwinding_map(), - recursion_map(), - branches(_branches), - branches_restore(0), - current_thread(0), - no_thread_interleavings(0), - depth(0) - { - path_symex_statet::threadt &thread=add_thread(); - thread.pc=locs.entry_loc; // reset its PC - } - - // like initial state except that branches are copied from "other" - // and history will be 'nil' - static path_symex_statet lazy_copy(path_symex_statet &other) - { - // allow compiler to use RVO - return path_symex_statet( - other.var_map, - other.locs, - path_symex_step_reft(), - other.get_branches()); - } - - // These are tied to a particular var_map - // and a particular program. - var_mapt &var_map; - const locst &locs; - - // the value of a variable - struct var_statet - { - // it's a given explicit value or a symbol with given identifier - exprt value; - symbol_exprt ssa_symbol; - - // for uninterpreted functions or arrays we maintain an index set - typedef std::set index_sett; - index_sett index_set; - - var_statet(): - value(nil_exprt()), - ssa_symbol(irep_idt()) - { - } - }; - - // the values of the shared variables - typedef std::vector var_valt; - var_valt shared_vars; - - // procedure frame - struct framet - { - irep_idt current_function; - loc_reft return_location; - exprt return_lhs; - var_valt saved_local_vars; - }; - - // call stack - typedef std::vector call_stackt; - - // the state of a thread - struct threadt - { - public: - loc_reft pc; - call_stackt call_stack; // the call stack - var_valt local_vars; // thread-local variables - bool active; - - threadt():active(true) - { - } - }; - - typedef std::vector threadst; - threadst threads; - - // warning: reference is not stable - var_statet &get_var_state(const var_mapt::var_infot &var_info); - - bool inside_atomic_section; - - unsigned get_current_thread() const - { - return current_thread; - } - - void set_current_thread(unsigned _thread) - { - current_thread=_thread; - } - - goto_programt::const_targett get_instruction() const; - - // branch taken case - void record_true_branch() - { - branches.push_back(true); - } - - // branch not taken case - void record_false_branch() - { - branches.push_back(false); - } - - bool is_lazy() const - { - return branches_restore < branches.size(); - } - - // returns branch direction that should be taken - bool restore_branch() - { - assert(is_lazy()); - return branches[branches_restore++]; - } - - bool is_executable() const - { - return !threads.empty() && - threads[current_thread].active; - } - - // execution history - path_symex_step_reft history; - - // adds an entry to the history - void record_step(); - - // like record_step() except that branch decision is also recorded - void record_branch_step(bool taken); - - // various state transformers - - threadt &add_thread() - { - threads.resize(threads.size()+1); - return threads.back(); - } - - void disable_current_thread() - { - threads[current_thread].active=false; - } - - loc_reft pc() const - { - return threads[current_thread].pc; - } - - void next_pc() - { - threads[current_thread].pc.increase(); - } - - void set_pc(loc_reft new_pc) - { - threads[current_thread].pc=new_pc; - } - - // output - void output(std::ostream &out) const; - void output(const threadt &thread, std::ostream &out) const; - - // instantiate expressions with propagation - exprt read(const exprt &src) - { - return read(src, true); - } - - // instantiate without constant propagation - exprt read_no_propagate(const exprt &src) - { - return read(src, false); - } - - exprt dereference_rec(const exprt &src, bool propagate); - - std::string array_index_as_string(const exprt &) const; - - unsigned get_no_thread_interleavings() const - { - return no_thread_interleavings; - } - - unsigned get_depth() const - { - return depth; - } - - bool is_feasible(class decision_proceduret &) const; - - bool check_assertion(class decision_proceduret &); - - // counts how many times we have executed backwards edges - typedef std::map unwinding_mapt; - unwinding_mapt unwinding_map; - - // similar for recursive function calls - typedef std::map recursion_mapt; - recursion_mapt recursion_map; - -protected: - branchest branches; - branchest::size_type branches_restore; - - // On first call, O(N) where N is the length of the execution path - // leading to this state. Subsequent calls run in constant time. - const branchest &get_branches() - { - if(!branches.empty() || history.is_nil()) - return branches; - - // Contrarily, suppose this state is lazy. Since we did not - // return above, branches.empty(). By definition of is_lazy(), - // branches_restore must have been a negative number. Since - // its type is unsigned, however, this is impossible. - assert(!is_lazy()); - - path_symex_step_reft step_ref=history; - assert(!step_ref.is_nil()); - loc_reft next_loc_ref=pc(); - for(;;) - { - if(step_ref.is_nil()) - break; - - const loct &loc=locs[step_ref->pc]; - if(loc.target->is_goto()) - { - branches.push_back(loc.branch_target==next_loc_ref); - assert(branches.back() || step_ref->pc.next_loc()==next_loc_ref); - } - - next_loc_ref=step_ref->pc; - step_ref=step_ref->predecessor; - } - - // preserve non-laziness of this state (see first assertion) - branches_restore=branches.size(); - - // TODO: add "path_symex_step::branch_depth" field so we can - // reserve() the right capacity of vector and avoid reverse(). - std::reverse(branches.begin(), branches.end()); - - return branches; - } - - unsigned current_thread; - unsigned no_thread_interleavings; - unsigned depth; - - exprt read( - const exprt &src, - bool propagate); - - exprt instantiate_rec( - const exprt &src, - bool propagate); - - exprt instantiate_rec_address( - const exprt &src, - bool propagate); - - exprt read_symbol_member_index( - const exprt &src, - bool propagate); -}; - -path_symex_statet initial_state( - var_mapt &var_map, - const locst &locs, - path_symex_historyt &); - -#endif // CPROVER_AA_PATH_SYMEX_PATH_SYMEX_STATE_H diff --git a/src/aa-symex/Makefile b/src/aa-symex/Makefile deleted file mode 100644 index a5e2b0ad5d8..00000000000 --- a/src/aa-symex/Makefile +++ /dev/null @@ -1,68 +0,0 @@ -SRC = path_search.cpp - -OBJ += ../ansi-c/ansi-c$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ - ../big-int/big-int$(LIBEXT) \ - ../goto-programs/goto-programs$(LIBEXT) \ - ../analyses/analyses$(LIBEXT) \ - ../langapi/langapi$(LIBEXT) \ - ../xmllang/xmllang$(LIBEXT) \ - ../assembler/assembler$(LIBEXT) \ - ../solvers/solvers$(LIBEXT) \ - ../util/util$(LIBEXT) \ - ../goto-symex/adjust_float_expressions$(OBJEXT) \ - ../goto-symex/rewrite_union$(OBJEXT) \ - ../pointer-analysis/dereference$(OBJEXT) \ - ../goto-instrument/cover$(OBJEXT) \ - ../aa-path-symex/aa-path-symex$(LIBEXT) \ - ../symex/symex_main$(OBJEXT) \ - ../symex/symex_parse_options$(OBJEXT) \ - ../symex/symex_cover$(OBJEXT) \ - ../path-symex/locs$(OBJEXT) ../path-symex/var_map$(OBJEXT) \ - ../path-symex/path_symex_history$(OBJEXT) - -INCLUDES= -I .. - -LIBS = - -include ../config.inc -include ../common - -CLEANFILES = symex$(EXEEXT) - -all: symex$(EXEEXT) - -ifneq ($(wildcard ../bv_refinement/Makefile),) - OBJ += ../bv_refinement/bv_refinement$(LIBEXT) - CP_CXXFLAGS += -DHAVE_BV_REFINEMENT -endif - -ifneq ($(wildcard ../cpp/Makefile),) - OBJ += ../cpp/cpp$(LIBEXT) - CP_CXXFLAGS += -DHAVE_CPP -endif - -ifneq ($(wildcard ../java_bytecode/Makefile),) - OBJ += ../java_bytecode/java_bytecode$(LIBEXT) - CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE -endif - -ifneq ($(wildcard ../specc/Makefile),) - OBJ += ../specc/specc$(LIBEXT) - CP_CXXFLAGS += -DHAVE_SPECC -endif - -ifneq ($(wildcard ../php/Makefile),) - OBJ += ../php/php$(LIBEXT) - CP_CXXFLAGS += -DHAVE_PHP -endif - -############################################################################### - -symex$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: symex-mac-signed - -symex-mac-signed: cbmc$(EXEEXT) - strip symex$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) symex$(EXEEXT) diff --git a/src/aa-symex/path_search.cpp b/src/aa-symex/path_search.cpp deleted file mode 100644 index 5bfa680177f..00000000000 --- a/src/aa-symex/path_search.cpp +++ /dev/null @@ -1,517 +0,0 @@ -/*******************************************************************\ - -Module: Path-based Symbolic Execution - -Author: Daniel Kroening, kroening@kroening.com - Alex Horn, alex.horn@cs.ox.ac.uk - -\*******************************************************************/ - -#include -#include - -#include -#include - -#include -#include - -#include "path_search.h" - -#ifdef PATH_SYMEX_FORK -// we've already check that the platform is (mostly) POSIX-compliant -#include -#endif - -/*******************************************************************\ - -Function: path_searcht::operator() - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -path_searcht::resultt path_searcht::operator()( - const goto_functionst &goto_functions) -{ -#ifdef PATH_SYMEX_FORK - // Disable output because there is no meaningful way - // to write text when multiple path_search processes - // run concurrently. This could be remedied by piping - // to individual files or inter-process communication, - // a performance bottleneck, however. - null_message_handlert null_message; - set_message_handler(null_message); -#endif - - locst locs(ns); - var_mapt var_map(ns); - - locs.build(goto_functions); - - // this is the container for the history-forest - path_symex_historyt history; - - queue.push_back(initial_state(var_map, locs, history)); - - // set up the statistics - number_of_instructions=0; - number_of_dropped_states=0; - number_of_paths=0; - number_of_VCCs=0; - number_of_VCCs_after_simplification=0; - number_of_failed_properties=0; - number_of_fast_forward_steps=0; - - // stop the time - start_time=current_time(); - - initialize_property_map(goto_functions); - - while(!queue.empty()) - { - // Pick a state from the queue, - // according to some heuristic. - queuet::iterator state=pick_state(); - - // fast forwarding required? - if(state->is_lazy()) - { - assert(state->is_executable()); - assert(state->history.is_nil()); - - // keep allocated memory, this is faster than - // instantiating a new empty vector and map - history.clear(); - var_map.clear(); - state->history=path_symex_step_reft(history); - - // restore all fields of a lazy state by symbolic - // execution along previously recorded branches - const queuet::size_type queue_size=queue.size(); - do - { - number_of_fast_forward_steps++; - - path_symex(*state, queue); -#ifdef PATH_SYMEX_OUTPUT - status() << "Fast forward thread " << state->get_current_thread() - << "/" << state->threads.size() - << " PC " << state->pc() << messaget::eom; -#endif - } - while(state->is_lazy() && state->is_executable()); - assert(queue.size() == queue_size); - } - - // TODO: check lazy states before fast forwarding, or perhaps it - // is better to even check before inserting into queue - if(drop_state(*state)) - { - number_of_dropped_states++; - queue.erase(state); - continue; - } - - if(!state->is_executable()) - { - queue.erase(state); - continue; - } - - // count only executable instructions - number_of_instructions++; - -#ifdef PATH_SYMEX_OUTPUT - status() << "Queue " << queue.size() - << " thread " << state->get_current_thread() - << "/" << state->threads.size() - << " PC " << state->pc() << messaget::eom; -#endif - - // an error, possibly? - if(state->get_instruction()->is_assert()) - { - if(show_vcc) - do_show_vcc(*state); - else - { - check_assertion(*state); - - // all assertions failed? - if(number_of_failed_properties==property_map.size()) - break; - } - } - -#ifdef PATH_SYMEX_FORK - if(try_await()) - { - debug() << "Child process has terminated " - "so exit parent" << messaget::eom; - break; - } -#endif - - // execute and record whether a "branch" occurred - const queuet::size_type queue_size = queue.size(); - path_symex(*state, queue); - - assert(queue_size <= queue.size()); - number_of_paths += (queue.size() - queue_size); - } - -#ifdef PATH_SYMEX_FORK - int exit_status=await(); - if(exit_status==0 && number_of_failed_properties!=0) - { - // the eldest child process (if any) reports found bugs - report_statistics(); - return UNSAFE; - } - else - { - // either a child found and reported a bug or - // the parent's search partition is safe - switch(exit_status) - { - case 0: return SAFE; - case 10: return UNSAFE; - default: return ERROR; - } - } -#else - report_statistics(); - - return number_of_failed_properties==0?SAFE:UNSAFE; -#endif -} - -#ifdef PATH_SYMEX_FORK -/*******************************************************************\ - -Function: path_searcht::await() - - Inputs: - - Outputs: returns zero if and only if every child process succeeds; - otherwise, the error of exactly one child is returned - - Purpose: POSIX-compliant (possibly blocking) wait on child - processes, writes to error() if anything goes wrong; - any earlier calls to try_await() do not affect await() - -\*******************************************************************/ - -int path_searcht::await() -{ - int status; - for(;;) - { - // a process' entries for its child processes are deleted after - // the first call to waitpid(). When waitpid() is called again - // it returns -1 and errno is set to ECHILD. - pid_t pid=wait(&status); - if(pid==-1) - { - if(errno==ECHILD) - break; // no more child processes - } - else - { - if(!WIFEXITED(status) || WEXITSTATUS(status)!=0) - { - debug() << "PID " << pid << " failed, return code " - << WEXITSTATUS(status) << messaget::eom; - - return WEXITSTATUS(status); - } - } - } - - return 0; -} - -/*******************************************************************\ - -Function: path_searcht::try_await() - - Inputs: - - Outputs: returns true if and only if at least one child process - has terminated - - Purpose: POSIX-compliant nonblocking wait on child processes, - child's status is preserved for await() function - -\*******************************************************************/ - -bool path_searcht::try_await() -{ - int status; - pid_t pid=waitpid(-1, &status, WNOHANG | WNOWAIT); - return pid!=-1; -} -#endif - -/*******************************************************************\ - -Function: path_searcht::report_statistics - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_searcht::report_statistics() -{ - // report a bit - - status() << "Number of instructions: " - << number_of_instructions << messaget::eom; - - status() << "Number of dropped states: " - << number_of_dropped_states << messaget::eom; - - status() << "Number of paths: " - << number_of_paths << messaget::eom; - - status() << "Number of fast forward steps: " - << number_of_fast_forward_steps << messaget::eom; - - status() << "Generated " << number_of_VCCs << " VCC(s), " - << number_of_VCCs_after_simplification - << " remaining after simplification" - << messaget::eom; - - time_periodt total_time=current_time()-start_time; - status() << "Runtime: " << total_time << "s total, " - << sat_time << "s SAT" << messaget::eom; -} - -/*******************************************************************\ - -Function: path_searcht::pick_state - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -path_searcht::queuet::iterator path_searcht::pick_state() -{ - // Picking the first one is a DFS. - return queue.begin(); -} - -/*******************************************************************\ - -Function: path_searcht::do_show_vcc - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_searcht::do_show_vcc(statet &state) -{ - // keep statistics - number_of_VCCs++; - - const goto_programt::instructiont &instruction= - *state.get_instruction(); - - mstreamt &out=result(); - - if(instruction.source_location.is_not_nil()) - out << instruction.source_location << '\n'; - - if(instruction.source_location.get_comment()!="") - out << instruction.source_location.get_comment() << '\n'; - - unsigned count=1; - - std::vector steps; - state.history.build_history(steps); - - for(const auto &step_ref : steps) - { - if(step_ref->guard.is_not_nil()) - { - std::string string_value=from_expr(ns, "", step_ref->guard); - out << "{-" << count << "} " << string_value << '\n'; - count++; - } - - if(step_ref->ssa_rhs.is_not_nil()) - { - equal_exprt equality(step_ref->ssa_lhs, step_ref->ssa_rhs); - std::string string_value=from_expr(ns, "", equality); - out << "{-" << count << "} " << string_value << '\n'; - count++; - } - } - - out << "|--------------------------" << '\n'; - - exprt assertion=state.read(instruction.guard); - - out << "{" << 1 << "} " - << from_expr(ns, "", assertion) << '\n'; - - if(!assertion.is_true()) - number_of_VCCs_after_simplification++; - - out << eom; -} - -/*******************************************************************\ - -Function: path_searcht::drop_state - - Inputs: - - Outputs: - - Purpose: decide whether to drop a state - -\*******************************************************************/ - -bool path_searcht::drop_state(const statet &state) const -{ - // depth limit - if(depth_limit_set && state.get_depth()>depth_limit) - return true; - - // context bound - if(context_bound_set && state.get_no_thread_interleavings()>context_bound) - return true; - - - // unwinding limit -- loops - if(unwind_limit_set && state.get_instruction()->is_backwards_goto()) - { - for(const auto &loop_info : state.unwinding_map) - if(loop_info.second>unwind_limit) - return true; - } - - // unwinding limit -- recursion - if(unwind_limit_set && state.get_instruction()->is_function_call()) - { - for(const auto &rec_info : state.recursion_map) - if(rec_info.second>unwind_limit) - return true; - } - - return false; -} - -/*******************************************************************\ - -Function: path_searcht::check_assertion - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_searcht::check_assertion(statet &state) -{ - // keep statistics - number_of_VCCs++; - - const goto_programt::instructiont &instruction= - *state.get_instruction(); - - irep_idt property_name=instruction.source_location.get_property_id(); - property_entryt &property_entry=property_map[property_name]; - - if(property_entry.status==FAILURE) - return; // already failed - else if(property_entry.status==NOT_REACHED) - property_entry.status=SUCCESS; // well, for now! - - // the assertion in SSA - exprt assertion= - state.read(instruction.guard); - - if(assertion.is_true()) - return; // no error, trivially - - // keep statistics - number_of_VCCs_after_simplification++; - - status() << "Checking property " << property_name << eom; - - // take the time - absolute_timet sat_start_time=current_time(); - - satcheckt satcheck; - bv_pointerst bv_pointers(ns, satcheck); - - satcheck.set_message_handler(get_message_handler()); - bv_pointers.set_message_handler(get_message_handler()); - - if(!state.check_assertion(bv_pointers)) - { - build_goto_trace(state, bv_pointers, property_entry.error_trace); - property_entry.status=FAILURE; - number_of_failed_properties++; - } - - sat_time+=current_time()-sat_start_time; -} - -/*******************************************************************\ - -Function: path_searcht::initialize_property_map - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void path_searcht::initialize_property_map( - const goto_functionst &goto_functions) -{ - forall_goto_functions(it, goto_functions) - if(!it->second.is_inlined()) - { - const goto_programt &goto_program=it->second.body; - - forall_goto_program_instructions(i_it, goto_program) - { - if(!i_it->is_assert()) - continue; - - const source_locationt &source_location=i_it->source_location; - - irep_idt property_name=source_location.get_property_id(); - - property_entryt &property_entry=property_map[property_name]; - property_entry.status=NOT_REACHED; - property_entry.description=source_location.get_comment(); - property_entry.source_location=source_location; - } - } -} diff --git a/src/aa-symex/path_search.h b/src/aa-symex/path_search.h deleted file mode 100644 index 51c67ac93f0..00000000000 --- a/src/aa-symex/path_search.h +++ /dev/null @@ -1,119 +0,0 @@ -/*******************************************************************\ - -Module: Path-based Symbolic Execution - -Author: Daniel Kroening, kroening@kroening.com - Alex Horn, alex.horn@cs.ox.ac.uk - -\*******************************************************************/ - -#ifndef CPROVER_AA_SYMEX_PATH_SEARCH_H -#define CPROVER_AA_SYMEX_PATH_SEARCH_H - -#include - -#include - -#include - -class path_searcht:public safety_checkert -{ -public: - explicit path_searcht(const namespacet &_ns): - safety_checkert(_ns), - show_vcc(false), - depth_limit_set(false), // no limit - context_bound_set(false), - unwind_limit_set(false) - { - } - - virtual resultt operator()( - const goto_functionst &goto_functions); - - void set_depth_limit(unsigned limit) - { - depth_limit_set=true; - depth_limit=limit; - } - - void set_context_bound(unsigned limit) - { - context_bound_set=true; - context_bound=limit; - } - - void set_unwind_limit(unsigned limit) - { - unwind_limit_set=true; - unwind_limit=limit; - } - - bool show_vcc; - - // statistics - unsigned number_of_instructions; - unsigned number_of_dropped_states; - unsigned number_of_paths; - unsigned number_of_VCCs; - unsigned number_of_VCCs_after_simplification; - unsigned number_of_failed_properties; - unsigned number_of_fast_forward_steps; - absolute_timet start_time; - time_periodt sat_time; - - enum statust { NOT_REACHED, SUCCESS, FAILURE }; - - struct property_entryt - { - statust status; - irep_idt description; - goto_tracet error_trace; - source_locationt source_location; - - bool is_success() const { return status==SUCCESS; } - bool is_failure() const { return status==FAILURE; } - bool is_not_reached() const { return status==NOT_REACHED; } - }; - - typedef std::map property_mapt; - property_mapt property_map; - -protected: -#ifdef PATH_SYMEX_FORK - // blocks until child processes have terminated - int await(); - - // returns whether at least one child process has terminated - bool try_await(); -#endif - - typedef path_symex_statet statet; - - // State queue. Iterators are stable. - // The states most recently executed are at the head. - typedef std::list queuet; - queuet queue; - - // search heuristic - queuet::iterator pick_state(); - - bool execute(queuet::iterator state, const namespacet &); - - void check_assertion(statet &state); - void do_show_vcc(statet &state); - - bool drop_state(const statet &state) const; - - void report_statistics(); - - void initialize_property_map( - const goto_functionst &goto_functions); - - unsigned depth_limit; - unsigned context_bound; - unsigned unwind_limit; - bool depth_limit_set, context_bound_set, unwind_limit_set; -}; - -#endif // CPROVER_AA_SYMEX_PATH_SEARCH_H diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 87e9beb45d2..adc6e2ee517 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -56,6 +56,7 @@ class optionst; "(graphml-witness):" \ "(java-max-vla-length):(java-unwind-enum-static)" \ "(localize-faults)(localize-faults-method):" \ + "(lazy-methods)" \ "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) class cbmc_parse_optionst: diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index f900b9824a7..04d50e76f82 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -544,8 +544,8 @@ bool compilet::parse(const std::string &file_name) language_filet language_file; - std::pair - res=language_files.filemap.insert( + std::pair + res=language_files.file_map.insert( std::pair(file_name, language_file)); language_filet &lf=res.first->second; @@ -736,7 +736,7 @@ bool compilet::parse_source(const std::string &file_name) return true; // so we remove it from the list afterwards - language_files.filemap.erase(file_name); + language_files.file_map.erase(file_name); return false; } diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index fa92bc27cc7..9f1aa347679 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -10,8 +10,11 @@ Date: May 2016 #include #include +#include +#include #include +#include #include "cover.h" @@ -28,6 +31,11 @@ class basic_blockst if(next_is_target || it->is_target()) block_count++; + const irep_idt &line=it->source_location.get_line(); + if(!line.empty()) + block_line_cover_map[block_count] + .insert(unsafe_string2unsigned(id2string(line))); + block_map[it]=block_count; if(!it->source_location.is_nil() && @@ -35,7 +43,26 @@ class basic_blockst source_location_map[block_count]=it->source_location; next_is_target= +#if 0 + // Disabled for being too messy it->is_goto() || it->is_function_call() || it->is_assume(); +#else + it->is_goto() || it->is_function_call(); +#endif + } + + // create list of covered lines as CSV string and set as property of source + // location of basic block, compress to ranges if applicable + format_number_ranget format_lines; + for(const auto &cover_set : block_line_cover_map) + { + assert(!cover_set.second.empty()); + std::vector + line_list{cover_set.second.begin(), cover_set.second.end()}; + + std::string covered_lines=format_lines(line_list); + source_location_map[cover_set.first] + .set_basic_block_covered_lines(covered_lines); } } @@ -47,6 +74,11 @@ class basic_blockst typedef std::map source_location_mapt; source_location_mapt source_location_map; + // map block numbers to set of line numbers + typedef std::map > + block_line_cover_mapt; + block_line_cover_mapt block_line_cover_map; + inline unsigned operator[](goto_programt::const_targett t) { return block_map[t]; @@ -414,7 +446,7 @@ std::set collect_mcdc_controlling_nested( const std::set &decisions) { // To obtain the 1st-level controlling conditions - std::set controlling = collect_mcdc_controlling(decisions); + std::set controlling=collect_mcdc_controlling(decisions); std::set result; // For each controlling condition, to check if it contains @@ -627,7 +659,7 @@ void remove_repetition(std::set &exprs) **/ for(auto &y : new_exprs) { - bool iden = true; + bool iden=true; for(auto &c : conditions) { std::set signs1=sign_of_expr(c, x); @@ -669,7 +701,7 @@ void remove_repetition(std::set &exprs) } // update the original ''exprs'' - exprs = new_exprs; + exprs=new_exprs; } /*******************************************************************\ @@ -838,7 +870,8 @@ bool is_mcdc_pair( if(diff_count==1) return true; - else return false; + else + return false; } /*******************************************************************\ @@ -963,7 +996,8 @@ void minimize_mcdc_controlling( { controlling=new_controlling; } - else break; + else + break; } } @@ -1297,9 +1331,12 @@ void instrument_cover_goals( const std::set decisions=collect_decisions(i_it); std::set both; - std::set_union(conditions.begin(), conditions.end(), - decisions.begin(), decisions.end(), - inserter(both, both.end())); + std::set_union( + conditions.begin(), + conditions.end(), + decisions.begin(), + decisions.end(), + inserter(both, both.end())); const source_locationt source_location=i_it->source_location; @@ -1397,6 +1434,9 @@ void instrument_cover_goals( f_it->first=="__CPROVER_initialize") continue; - instrument_cover_goals(symbol_table, f_it->second.body, criterion); + instrument_cover_goals( + symbol_table, + f_it->second.body, + criterion); } } diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index d06a79e01d8..24005138109 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -163,7 +163,8 @@ void dump_ct::operator()(std::ostream &os) } // we don't want to dump in full all definitions - if(!tag_added && ignore(symbol)) + if(!tag_added && + system_symbols.is_symbol_internal_symbol(symbol, system_headers)) continue; if(!symbols_sorted.insert(name_str).second) @@ -344,7 +345,7 @@ void dump_ct::convert_compound( ns.lookup(to_symbol_type(type).get_identifier()); assert(symbol.is_type); - if(!ignore(symbol)) + if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers)) convert_compound(symbol.type, unresolved, recursive, os); } else if(type.id()==ID_c_enum_tag) @@ -353,7 +354,7 @@ void dump_ct::convert_compound( ns.lookup(to_c_enum_tag_type(type).get_identifier()); assert(symbol.is_type); - if(!ignore(symbol)) + if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers)) convert_compound(symbol.type, unresolved, recursive, os); } else if(type.id()==ID_array || type.id()==ID_pointer) @@ -610,259 +611,6 @@ void dump_ct::convert_compound_enum( /*******************************************************************\ -Function: dump_ct::init_system_library_map - -Inputs: - -Outputs: - -Purpose: - -\*******************************************************************/ - -#define ADD_TO_SYSTEM_LIBRARY(v, header) \ - for(size_t i=0; isecond); - return true; - } - - return false; -} - -/*******************************************************************\ - Function: dump_ct::cleanup_decl Inputs: diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h index 6bb7b79638e..c8c77da5102 100644 --- a/src/goto-instrument/dump_c_class.h +++ b/src/goto-instrument/dump_c_class.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include class dump_ct { @@ -30,7 +31,7 @@ class dump_ct language(factory()) { if(use_system_headers) - init_system_library_map(); + system_symbols=system_library_symbolst(); } virtual ~dump_ct() @@ -51,21 +52,15 @@ class dump_ct std::set system_headers; - typedef std::unordered_map - system_library_mapt; - system_library_mapt system_library_map; + system_library_symbolst system_symbols; typedef std::unordered_map declared_enum_constants_mapt; declared_enum_constants_mapt declared_enum_constants; - void init_system_library_map(); - std::string type_to_string(const typet &type); std::string expr_to_string(const exprt &expr); - bool ignore(const symbolt &symbol); - static std::string indent(const unsigned n) { return std::string(2*n, ' '); diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index d8cb835e4a8..8b69282c381 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -20,7 +20,11 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \ slice_global_inits.cpp goto_inline_class.cpp class_identifier.cpp \ show_goto_functions_json.cpp \ show_goto_functions_xml.cpp \ - remove_static_init_loops.cpp remove_instanceof.cpp + remove_static_init_loops.cpp \ + remove_instanceof.cpp \ + class_identifier.cpp \ + system_library_symbols.cpp \ + INCLUDES= -I .. diff --git a/src/goto-programs/get_goto_model.cpp b/src/goto-programs/get_goto_model.cpp index 5afef435596..02aae876030 100644 --- a/src/goto-programs/get_goto_model.cpp +++ b/src/goto-programs/get_goto_model.cpp @@ -75,8 +75,8 @@ bool get_goto_modelt::operator()(const std::vector &files) return true; } - std::pair - result=language_files.filemap.insert( + std::pair + result=language_files.file_map.insert( std::pair(filename, language_filet())); language_filet &lf=result.first->second; diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp index 830798c289e..c8c97f8d4a5 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -213,7 +213,12 @@ void goto_partial_inline( // called function const goto_functiont &goto_function=f_it->second; - if(!goto_function.body_available()) + // We can't take functions without bodies to find functions + // inside them to be inlined. + // We also don't allow for the _start function to have any of its + // function calls to be inlined + if(!goto_function.body_available() || + f_it->first==ID__start) continue; const goto_programt &goto_program=goto_function.body; diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index ad8bdcdfdd9..4179afb5395 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -65,6 +65,7 @@ void goto_trace_stept::output( case goto_trace_stept::ASSIGNMENT: out << "ASSIGNMENT"; break; case goto_trace_stept::GOTO: out << "GOTO"; break; case goto_trace_stept::DECL: out << "DECL"; break; + case goto_trace_stept::DEAD: out << "DEAD"; break; case goto_trace_stept::OUTPUT: out << "OUTPUT"; break; case goto_trace_stept::INPUT: out << "INPUT"; break; case goto_trace_stept::ATOMIC_BEGIN: out << "ATOMC_BEGIN"; break; @@ -73,7 +74,9 @@ void goto_trace_stept::output( case goto_trace_stept::SHARED_WRITE: out << "SHARED WRITE"; break; case goto_trace_stept::FUNCTION_CALL: out << "FUNCTION CALL"; break; case goto_trace_stept::FUNCTION_RETURN: out << "FUNCTION RETURN"; break; - default: assert(false); + default: + out << "unknown type: " << type << std::endl; + assert(false); } if(type==ASSERT || type==ASSUME || type==GOTO) diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 507d538ada0..a669fac5e6b 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -154,6 +154,13 @@ class goto_tracet steps.push_back(step); } + // retrieves the final step in the trace for manipulation + // (used to fill a trace from code, hence non-const) + inline goto_trace_stept &get_last_step() + { + return steps.back(); + } + // delete all steps after (not including) s void trim_after(stepst::iterator s) { diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 4b950593aed..c93b50a2500 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -339,7 +339,8 @@ void remove_virtual_functionst::get_functions( component_name, functions); - functions.push_back(root_function); + if(root_function.symbol_expr!=symbol_exprt()) + functions.push_back(root_function); } /*******************************************************************\ diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index c7a6bdedf3f..cbbb00225c7 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -130,6 +130,10 @@ void show_properties_json( json_properties.push_back(jsont()).make_object(); json_property["name"]=json_stringt(id2string(property_id)); json_property["class"]=json_stringt(id2string(property_class)); + if(!source_location.get_basic_block_covered_lines().empty()) + json_property["coveredLines"]= + json_stringt( + id2string(source_location.get_basic_block_covered_lines())); json_property["sourceLocation"]=json(source_location); json_property["description"]=json_stringt(id2string(description)); json_property["expression"]= diff --git a/src/goto-programs/system_library_symbols.cpp b/src/goto-programs/system_library_symbols.cpp new file mode 100644 index 00000000000..250eb3b1cdb --- /dev/null +++ b/src/goto-programs/system_library_symbols.cpp @@ -0,0 +1,353 @@ +/*******************************************************************\ + +Module: Goto Programs + +Author: Thomas Kiley + +\*******************************************************************/ + +#include "system_library_symbols.h" +#include +#include +#include +#include + +system_library_symbolst::system_library_symbolst() +{ + init_system_library_map(); +} + +/*******************************************************************\ + +Function: system_library_symbolst::init_system_library_map + +Inputs: + +Outputs: + +Purpose: To generate a map of header file names -> list of symbols + The symbol names are reserved as the header and source files + will be compiled in to the goto program. + +\*******************************************************************/ + +void system_library_symbolst::init_system_library_map() +{ + // ctype.h + std::list ctype_syms= + { + "isalnum", "isalpha", "isblank", "iscntrl", "isdigit", "isgraph", + "islower", "isprint", "ispunct", "isspace", "isupper", "isxdigit", + "tolower", "toupper" + }; + add_to_system_library("ctype.h", ctype_syms); + + // fcntl.h + std::list fcntl_syms= + { + "creat", "fcntl", "open" + }; + add_to_system_library("fcntl.h", fcntl_syms); + + // locale.h + std::list locale_syms= + { + "setlocale" + }; + add_to_system_library("locale.h", locale_syms); + + // math.h + std::list math_syms= + { + "acos", "acosh", "asin", "asinh", "atan", "atan2", "atanh", + "cbrt", "ceil", "copysign", "cos", "cosh", "erf", "erfc", "exp", + "exp2", "expm1", "fabs", "fdim", "floor", "fma", "fmax", "fmin", + "fmod", "fpclassify", "fpclassifyl", "fpclassifyf", "frexp", + "hypot", "ilogb", "isfinite", "isinf", "isnan", "isnormal", + "j0", "j1", "jn", "ldexp", "lgamma", "llrint", "llround", "log", + "log10", "log1p", "log2", "logb", "lrint", "lround", "modf", "nan", + "nearbyint", "nextafter", "pow", "remainder", "remquo", "rint", + "round", "scalbln", "scalbn", "signbit", "sin", "sinh", "sqrt", + "tan", "tanh", "tgamma", "trunc", "y0", "y1", "yn", "isinff", + "isinfl", "isnanf", "isnanl" + }; + add_to_system_library("math.h", math_syms); + + // for some reason the math functions can sometimes be prefixed with + // a double underscore + std::list underscore_math_syms; + for(const irep_idt &math_sym : math_syms) + { + std::ostringstream underscore_id; + underscore_id << "__" << math_sym; + underscore_math_syms.push_back(irep_idt(underscore_id.str())); + } + add_to_system_library("math.h", underscore_math_syms); + + // pthread.h + std::list pthread_syms= + { + "pthread_cleanup_pop", "pthread_cleanup_push", + "pthread_cond_broadcast", "pthread_cond_destroy", + "pthread_cond_init", "pthread_cond_signal", + "pthread_cond_timedwait", "pthread_cond_wait", "pthread_create", + "pthread_detach", "pthread_equal", "pthread_exit", + "pthread_getspecific", "pthread_join", "pthread_key_delete", + "pthread_mutex_destroy", "pthread_mutex_init", + "pthread_mutex_lock", "pthread_mutex_trylock", + "pthread_mutex_unlock", "pthread_once", "pthread_rwlock_destroy", + "pthread_rwlock_init", "pthread_rwlock_rdlock", + "pthread_rwlock_unlock", "pthread_rwlock_wrlock", + "pthread_rwlockattr_destroy", "pthread_rwlockattr_getpshared", + "pthread_rwlockattr_init", "pthread_rwlockattr_setpshared", + "pthread_self", "pthread_setspecific" + }; + add_to_system_library("pthread.h", pthread_syms); + + // setjmp.h + std::list setjmp_syms= + { + "_longjmp", "_setjmp", "longjmp", "longjmperror", "setjmp", + "siglongjmp", "sigsetjmp" + }; + add_to_system_library("setjmp.h", setjmp_syms); + + // stdio.h + std::list stdio_syms= + { + "asprintf", "clearerr", "fclose", "fdopen", "feof", "ferror", + "fflush", "fgetc", "fgetln", "fgetpos", "fgets", "fgetwc", + "fgetws", "fileno", "fopen", "fprintf", "fpurge", "fputc", + "fputs", "fputwc", "fputws", "fread", "freopen", "fropen", + "fscanf", "fseek", "fsetpos", "ftell", "funopen", "fwide", + "fwopen", "fwprintf", "fwrite", "getc", "getchar", "getdelim", + "getline", "gets", "getw", "getwc", "getwchar", "mkdtemp", + "mkstemp", "mktemp", "perror", "printf", "putc", "putchar", + "puts", "putw", "putwc", "putwchar", "remove", "rewind", "scanf", + "setbuf", "setbuffer", "setlinebuf", "setvbuf", "snprintf", + "sprintf", "sscanf", "strerror", "swprintf", "sys_errlist", + "sys_nerr", "tempnam", "tmpfile", "tmpnam", "ungetc", "ungetwc", + "vasprintf", "vfprintf", "vfscanf", "vfwprintf", "vprintf", + "vscanf", "vsnprintf", "vsprintf", "vsscanf", "vswprintf", + "vwprintf", "wprintf", + /* non-public struct types */ + "tag-__sFILE", "tag-__sbuf", // OS X + "tag-_IO_FILE", "tag-_IO_marker", // Linux + }; + add_to_system_library("stdio.h", stdio_syms); + + // stdlib.h + std::list stdlib_syms= + { + "abort", "abs", "atexit", "atof", "atoi", "atol", "atoll", + "bsearch", "calloc", "div", "exit", "free", "getenv", "labs", + "ldiv", "llabs", "lldiv", "malloc", "mblen", "mbstowcs", "mbtowc", + "qsort", "rand", "realloc", "srand", "strtod", "strtof", "strtol", + "strtold", "strtoll", "strtoul", "strtoull", "system", "wcstombs", + "wctomb" + }; + add_to_system_library("stdlib.h", stdlib_syms); + + // string.h + std::list string_syms= + { + "strcat", "strncat", "strchr", "strrchr", "strcmp", "strncmp", + "strcpy", "strncpy", "strerror", "strlen", "strpbrk", "strspn", + "strcspn", "strstr", "strtok", "strcasecmp", "strncasecmp", "strdup", + "memset" + }; + add_to_system_library("string.h", string_syms); + + // time.h + std::list time_syms= + { + "asctime", "asctime_r", "ctime", "ctime_r", "difftime", "gmtime", + "gmtime_r", "localtime", "localtime_r", "mktime", + /* non-public struct types */ + "tag-timespec", "tag-timeval" + }; + add_to_system_library("time.h", time_syms); + + // unistd.h + std::list unistd_syms= + { + "_exit", "access", "alarm", "chdir", "chown", "close", "dup", + "dup2", "execl", "execle", "execlp", "execv", "execve", "execvp", + "fork", "fpathconf", "getcwd", "getegid", "geteuid", "getgid", + "getgroups", "getlogin", "getpgrp", "getpid", "getppid", "getuid", + "isatty", "link", "lseek", "pathconf", "pause", "pipe", "read", + "rmdir", "setgid", "setpgid", "setsid", "setuid", "sleep", + "sysconf", "tcgetpgrp", "tcsetpgrp", "ttyname", "ttyname_r", + "unlink", "write" + }; + add_to_system_library("unistd.h", unistd_syms); + + // sys/select.h + std::list sys_select_syms= + { + "select" + }; + add_to_system_library("sys/select.h", sys_select_syms); + + // sys/socket.h + std::list sys_socket_syms= + { + "accept", "bind", "connect" + }; + add_to_system_library("sys/socket.h", sys_socket_syms); + + // sys/stat.h + std::list sys_stat_syms= + { + "fstat", "lstat", "stat" + }; + add_to_system_library("sys/stat.h", sys_stat_syms); + + std::list fenv_syms= + { + "fenv_t", "fexcept_t", "feclearexcept", "fegetexceptflag", + "feraiseexcept", "fesetexceptflag", "fetestexcept", + "fegetround", "fesetround", "fegetenv", "feholdexcept", + "fesetenv", "feupdateenv" + }; + add_to_system_library("fenv.h", fenv_syms); + + std::list errno_syms= + { + "__error", "__errno_location", "__errno" + }; + add_to_system_library("errno.c", errno_syms); + + std::list noop_syms= + { + "__noop" + }; + add_to_system_library("noop.c", noop_syms); + +#if 0 + // sys/types.h + std::list sys_types_syms= + { + }; + add_to_system_library("sys/types.h", sys_types_syms); +#endif + + // sys/wait.h + std::list sys_wait_syms= + { + "wait", "waitpid" + }; + add_to_system_library("sys/wait.h", sys_wait_syms); +} + +/*******************************************************************\ + +Function: system_library_symbolst::add_to_system_library + +Inputs: + header_file - the name of the header file the symbol came from + symbols - a list of the names of the symbols in the header file + +Outputs: + +Purpose: To add the symbols from a specific header file to the + system library map. The symbol is used as the key so that + we can easily look up symbols. + +\*******************************************************************/ + +void system_library_symbolst::add_to_system_library( + irep_idt header_file, + std::list symbols) +{ + for(const irep_idt &symbol : symbols) + { + system_library_map[symbol]=header_file; + } +} + + +/*******************************************************************\ + +Function: system_library_symbolst::is_symbol_internal_symbol + +Inputs: + symbol - the symbol to check + +Outputs: True if the symbol is an internal symbol. If specific system + headers need to be included, the out_system_headers will contain + the headers. + +Purpose: To find out if a symbol is an internal symbol. + +\*******************************************************************/ + +bool system_library_symbolst::is_symbol_internal_symbol( + const symbolt &symbol, + std::set &out_system_headers) const +{ + const std::string &name_str=id2string(symbol.name); + + if(has_prefix(name_str, CPROVER_PREFIX) || + name_str=="__func__" || + name_str=="__FUNCTION__" || + name_str=="__PRETTY_FUNCTION__" || + name_str=="argc'" || + name_str=="argv'" || + name_str=="envp'" || + name_str=="envp_size'") + return true; + + // exclude nondet instructions + if(has_prefix(name_str, "nondet_")) + { + return true; + } + + if(has_prefix(name_str, "__VERIFIER")) + { + return true; + } + + const std::string &file_str=id2string(symbol.location.get_file()); + + // don't dump internal GCC builtins + if((file_str=="gcc_builtin_headers_alpha.h" || + file_str=="gcc_builtin_headers_arm.h" || + file_str=="gcc_builtin_headers_ia32.h" || + file_str=="gcc_builtin_headers_mips.h" || + file_str=="gcc_builtin_headers_power.h" || + file_str=="gcc_builtin_headers_generic.h") && + has_prefix(name_str, "__builtin_")) + return true; + + if(name_str=="__builtin_va_start" || + name_str=="__builtin_va_end" || + symbol.name==ID_gcc_builtin_va_arg) + { + out_system_headers.insert("stdarg.h"); + return true; + } + + // don't dump asserts + else if(name_str=="__assert_fail" || + name_str=="_assert" || + name_str=="__assert_c99" || + name_str=="_wassert") + { + return true; + } + + if(name_str.find("$link")!=std::string::npos) + return false; + + const auto &it=system_library_map.find(symbol.name); + + if(it!=system_library_map.end()) + { + out_system_headers.insert(id2string(it->second)); + return true; + } + + return false; +} diff --git a/src/goto-programs/system_library_symbols.h b/src/goto-programs/system_library_symbols.h new file mode 100644 index 00000000000..9438e052a76 --- /dev/null +++ b/src/goto-programs/system_library_symbols.h @@ -0,0 +1,38 @@ +/*******************************************************************\ + +Module: Goto Programs + +Author: Thomas Kiley + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_SYSTEM_LIBRARY_SYMBOLS_H +#define CPROVER_GOTO_PROGRAMS_SYSTEM_LIBRARY_SYMBOLS_H + +#include +#include +#include +#include + +class symbolt; + +class system_library_symbolst +{ +public: + system_library_symbolst(); + + bool is_symbol_internal_symbol( + const symbolt &symbol, + std::set &out_system_headers) const; + +private: + void init_system_library_map(); + + void add_to_system_library( + irep_idt header_file, + std::list symbols); + + std::map system_library_map; +}; + +#endif // CPROVER_GOTO_PROGRAMS_SYSTEM_LIBRARY_SYMBOLS_H diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 8d42611bfe0..440b0ce32cf 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_root_class.h" #include "java_types.h" #include "java_bytecode_convert_method.h" +#include "java_bytecode_language.h" #include #include @@ -27,11 +28,15 @@ class java_bytecode_convert_classt:public messaget symbol_tablet &_symbol_table, message_handlert &_message_handler, bool _disable_runtime_checks, - size_t _max_array_length): + size_t _max_array_length, + lazy_methodst& _lazy_methods, + lazy_methods_modet _lazy_methods_mode): messaget(_message_handler), symbol_table(_symbol_table), disable_runtime_checks(_disable_runtime_checks), - max_array_length(_max_array_length) + max_array_length(_max_array_length), + lazy_methods(_lazy_methods), + lazy_methods_mode(_lazy_methods_mode) { } @@ -52,6 +57,8 @@ class java_bytecode_convert_classt:public messaget symbol_tablet &symbol_table; const bool disable_runtime_checks; const size_t max_array_length; + lazy_methodst &lazy_methods; + lazy_methods_modet lazy_methods_mode; // conversion void convert(const classt &c); @@ -75,6 +82,13 @@ Function: java_bytecode_convert_classt::convert void java_bytecode_convert_classt::convert(const classt &c) { + std::string qualified_classname="java::"+id2string(c.name); + if(symbol_table.has_symbol(qualified_classname)) + { + debug() << "Skip class " << c.name << " (already loaded)" << eom; + return; + } + class_typet class_type; class_type.set_tag(c.name); @@ -107,7 +121,7 @@ void java_bytecode_convert_classt::convert(const classt &c) symbolt new_symbol; new_symbol.base_name=c.name; new_symbol.pretty_name=c.name; - new_symbol.name="java::"+id2string(c.name); + new_symbol.name=qualified_classname; class_type.set(ID_name, new_symbol.name); new_symbol.type=class_type; new_symbol.mode=ID_java; @@ -128,13 +142,35 @@ void java_bytecode_convert_classt::convert(const classt &c) // now do methods for(const auto &method : c.methods) - java_bytecode_convert_method( + { + const irep_idt method_identifier= + id2string(qualified_classname)+ + "."+id2string(method.name)+ + ":"+method.signature; + // Always run the lazy pre-stage, as it symbol-table + // registers the function. + java_bytecode_convert_method_lazy( *class_symbol, + method_identifier, method, - symbol_table, - get_message_handler(), - disable_runtime_checks, - max_array_length); + symbol_table); + if(lazy_methods_mode==LAZY_METHODS_MODE_EAGER) + { + // Upgrade to a fully-realized symbol now: + java_bytecode_convert_method( + *class_symbol, + method, + symbol_table, + get_message_handler(), + disable_runtime_checks, + max_array_length); + } + else + { + // Wait for our caller to decide what needs elaborating. + lazy_methods[method_identifier]=std::make_pair(class_symbol, &method); + } + } // is this a root class? if(c.extends.empty()) @@ -322,13 +358,17 @@ bool java_bytecode_convert_class( symbol_tablet &symbol_table, message_handlert &message_handler, bool disable_runtime_checks, - size_t max_array_length) + size_t max_array_length, + lazy_methodst &lazy_methods, + lazy_methods_modet lazy_methods_mode) { java_bytecode_convert_classt java_bytecode_convert_class( symbol_table, message_handler, disable_runtime_checks, - max_array_length); + max_array_length, + lazy_methods, + lazy_methods_mode); try { diff --git a/src/java_bytecode/java_bytecode_convert_class.h b/src/java_bytecode/java_bytecode_convert_class.h index ffaaf6e34da..5cc1526a125 100644 --- a/src/java_bytecode/java_bytecode_convert_class.h +++ b/src/java_bytecode/java_bytecode_convert_class.h @@ -13,12 +13,15 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "java_bytecode_parse_tree.h" +#include "java_bytecode_language.h" bool java_bytecode_convert_class( const java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table, message_handlert &message_handler, bool disable_runtime_checks, - size_t max_array_length); + size_t max_array_length, + lazy_methodst &, + lazy_methods_modet); #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 54412747708..447b5dacb80 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -5,7 +5,6 @@ Module: JAVA Bytecode Language Conversion Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - #ifdef DEBUG #include #endif @@ -183,43 +182,93 @@ const exprt java_bytecode_convert_methodt::variable( /*******************************************************************\ -Function: java_bytecode_convert_methodt::convert +Function: java_bytecode_convert_method_lazy - Inputs: + Inputs: `class_symbol`: class this method belongs to + `method_identifier`: fully qualified method name, including + type signature (e.g. "x.y.z.f:(I)") + `m`: parsed method object to convert + `symbol_table`: global symbol table (will be modified) Outputs: - Purpose: + Purpose: This creates a method symbol in the symtab, but doesn't + actually perform method conversion just yet. The caller + should call java_bytecode_convert_method later to give the + symbol/method a body. \*******************************************************************/ -void java_bytecode_convert_methodt::convert( +void java_bytecode_convert_method_lazy( const symbolt &class_symbol, - const methodt &m) + const irep_idt &method_identifier, + const java_bytecode_parse_treet::methodt &m, + symbol_tablet &symbol_table) { + symbolt method_symbol; typet member_type=java_type_from_string(m.signature); - assert(member_type.id()==ID_code); - - const irep_idt method_identifier= - id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.signature; - method_id=method_identifier; + method_symbol.name=method_identifier; + method_symbol.base_name=m.base_name; + method_symbol.mode=ID_java; + method_symbol.location=m.source_location; + method_symbol.location.set_function(method_identifier); - code_typet &code_type=to_code_type(member_type); - method_return_type=code_type.return_type(); - code_typet::parameterst ¶meters=code_type.parameters(); + if(method_symbol.base_name=="") + { + method_symbol.pretty_name= + id2string(class_symbol.pretty_name)+"."+ + id2string(class_symbol.base_name)+"()"; + member_type.set(ID_constructor, true); + } + else + method_symbol.pretty_name= + id2string(class_symbol.pretty_name)+"."+ + id2string(m.base_name)+"()"; // do we need to add 'this' as a parameter? if(!m.is_static) { + code_typet &code_type=to_code_type(member_type); + code_typet::parameterst ¶meters=code_type.parameters(); code_typet::parametert this_p; - const reference_typet object_ref_type( - symbol_typet(class_symbol.name)); + const reference_typet object_ref_type(symbol_typet(class_symbol.name)); this_p.type()=object_ref_type; this_p.set_this(); parameters.insert(parameters.begin(), this_p); } + method_symbol.type=member_type; + symbol_table.add(method_symbol); +} + +/*******************************************************************\ + +Function: java_bytecode_convert_methodt::convert + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void java_bytecode_convert_methodt::convert( + const symbolt &class_symbol, + const methodt &m) +{ + const irep_idt method_identifier= + id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.signature; + method_id=method_identifier; + + const auto &old_sym=symbol_table.lookup(method_identifier); + + typet member_type=old_sym.type; + code_typet &code_type=to_code_type(member_type); + method_return_type=code_type.return_type(); + code_typet::parameterst ¶meters=code_type.parameters(); + variables.clear(); // find parameter names in the local variable table: @@ -347,10 +396,10 @@ void java_bytecode_convert_methodt::convert( if((!m.is_abstract) && (!m.is_native)) method_symbol.value=convert_instructions(m, code_type); - // do we have the method symbol already? + // Replace the existing stub symbol with the real deal: const auto s_it=symbol_table.symbols.find(method.get_name()); - if(s_it!=symbol_table.symbols.end()) - symbol_table.symbols.erase(s_it); // erase, we stubbed it + assert(s_it!=symbol_table.symbols.end()); + symbol_table.symbols.erase(s_it); symbol_table.add(method_symbol); } @@ -754,6 +803,43 @@ static void gather_symbol_live_ranges( /*******************************************************************\ +Function: java_bytecode_convert_methodt::check_static_field_stub + + Inputs: `se`: Symbol expression referring to a static field + `basename`: The static field's basename + + Outputs: Creates a symbol table entry for the static field if one + doesn't exist already. + + Purpose: See above + +\*******************************************************************/ + +void java_bytecode_convert_methodt::check_static_field_stub( + const symbol_exprt &symbol_expr, + const irep_idt &basename) +{ + const auto &id=symbol_expr.get_identifier(); + if(symbol_table.symbols.find(id)==symbol_table.symbols.end()) + { + // Create a stub, to be overwritten if/when the real class is loaded. + symbolt new_symbol; + new_symbol.is_static_lifetime=true; + new_symbol.is_lvalue=true; + new_symbol.is_state_var=true; + new_symbol.name=id; + new_symbol.base_name=basename; + new_symbol.type=symbol_expr.type(); + new_symbol.pretty_name=new_symbol.name; + new_symbol.mode=ID_java; + new_symbol.is_type=false; + new_symbol.value.make_nil(); + symbol_table.add(new_symbol); + } +} + +/*******************************************************************\ + Function: java_bytecode_convert_methodt::convert_instructions Inputs: @@ -1006,6 +1092,25 @@ codet java_bytecode_convert_methodt::convert_instructions( get_message_handler()); } } + // replace calls to CProver.assume + else if(statement=="invokestatic" && + id2string(arg0.get(ID_identifier))== + "java::org.cprover.CProver.assume:(Z)V") + { + const code_typet &code_type=to_code_type(arg0.type()); + // sanity check: function has the right number of args + assert(code_type.parameters().size()==1); + + exprt operand = pop(1)[0]; + // we may need to adjust the type of the argument + if(operand.type()!=bool_typet()) + operand.make_typecast(bool_typet()); + + c=code_assumet(operand); + source_locationt loc=i_it->source_location; + loc.set_function(method_id); + c.add_source_location()=loc; + } else if(statement=="invokeinterface" || statement=="invokespecial" || statement=="invokevirtual" || @@ -1037,7 +1142,11 @@ codet java_bytecode_convert_methodt::convert_instructions( { if(as_string(arg0.get(ID_identifier)) .find("")!=std::string::npos) + { + if(needed_classes) + needed_classes->insert(classname); code_type.set(ID_constructor, true); + } else code_type.set(ID_java_super_method_call, true); } @@ -1119,11 +1228,15 @@ codet java_bytecode_convert_methodt::convert_instructions( assert(use_this); assert(!call.arguments().empty()); call.function()=arg0; + // Populate needed methods later, + // once we know what object types can exist. } else { // static binding call.function()=symbol_exprt(arg0.get(ID_identifier), arg0.type()); + if(needed_methods) + needed_methods->push_back(arg0.get(ID_identifier)); } call.function().add_source_location()=loc; @@ -1665,6 +1778,11 @@ codet java_bytecode_convert_methodt::convert_instructions( symbol_exprt symbol_expr(arg0.type()); const auto &field_name=arg0.get_string(ID_component_name); symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name); + if(needed_classes && arg0.type().id()==ID_symbol) + { + needed_classes->insert( + to_symbol_type(arg0.type()).get_identifier()); + } results[0]=java_bytecode_promotion(symbol_expr); // set $assertionDisabled to false @@ -1682,6 +1800,11 @@ codet java_bytecode_convert_methodt::convert_instructions( symbol_exprt symbol_expr(arg0.type()); const auto &field_name=arg0.get_string(ID_component_name); symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name); + if(needed_classes && arg0.type().id()==ID_symbol) + { + needed_classes->insert( + to_symbol_type(arg0.type()).get_identifier()); + } c=code_assignt(symbol_expr, op[0]); } else if(statement==patternt("?2?")) // i2c etc. @@ -2144,13 +2267,17 @@ void java_bytecode_convert_method( symbol_tablet &symbol_table, message_handlert &message_handler, bool disable_runtime_checks, - size_t max_array_length) + size_t max_array_length, + safe_pointer > needed_methods, + safe_pointer > needed_classes) { java_bytecode_convert_methodt java_bytecode_convert_method( symbol_table, message_handler, disable_runtime_checks, - max_array_length); + max_array_length, + needed_methods, + needed_classes); java_bytecode_convert_method(class_symbol, method); } diff --git a/src/java_bytecode/java_bytecode_convert_method.h b/src/java_bytecode/java_bytecode_convert_method.h index 8945af95bd1..e81881f44e1 100644 --- a/src/java_bytecode/java_bytecode_convert_method.h +++ b/src/java_bytecode/java_bytecode_convert_method.h @@ -11,15 +11,46 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include "java_bytecode_parse_tree.h" +class class_hierarchyt; + void java_bytecode_convert_method( const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &, symbol_tablet &symbol_table, message_handlert &message_handler, bool disable_runtime_checks, - size_t max_array_length); + size_t max_array_length, + safe_pointer > needed_methods, + safe_pointer > needed_classes); + +// Must provide both the optional parameters or neither. +inline void java_bytecode_convert_method( + const symbolt &class_symbol, + const java_bytecode_parse_treet::methodt &method, + symbol_tablet &symbol_table, + message_handlert &message_handler, + bool disable_runtime_checks, + size_t max_array_length) +{ + java_bytecode_convert_method( + class_symbol, + method, + symbol_table, + message_handler, + disable_runtime_checks, + max_array_length, + safe_pointer >::create_null(), + safe_pointer >::create_null()); +} + +void java_bytecode_convert_method_lazy( + const symbolt &class_symbol, + const irep_idt &method_identifier, + const java_bytecode_parse_treet::methodt &, + symbol_tablet &symbol_table); #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index 8c0e708a530..6844e337f22 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -13,8 +13,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include "java_bytecode_parse_tree.h" +#include "java_bytecode_convert_class.h" #include #include @@ -29,11 +31,15 @@ class java_bytecode_convert_methodt:public messaget symbol_tablet &_symbol_table, message_handlert &_message_handler, bool _disable_runtime_checks, - size_t _max_array_length): + size_t _max_array_length, + safe_pointer > _needed_methods, + safe_pointer > _needed_classes): messaget(_message_handler), symbol_table(_symbol_table), disable_runtime_checks(_disable_runtime_checks), - max_array_length(_max_array_length) + max_array_length(_max_array_length), + needed_methods(_needed_methods), + needed_classes(_needed_classes) { } @@ -52,6 +58,8 @@ class java_bytecode_convert_methodt:public messaget symbol_tablet &symbol_table; const bool disable_runtime_checks; const size_t max_array_length; + safe_pointer > needed_methods; + safe_pointer > needed_classes; irep_idt method_id; irep_idt current_method; @@ -211,6 +219,10 @@ class java_bytecode_convert_methodt:public messaget const code_typet &); const bytecode_infot &get_bytecode_info(const irep_idt &statement); + + void check_static_field_stub( + const symbol_exprt &se, + const irep_idt &basename); }; #endif diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 1d9d9f57b41..e9d5a87186b 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -14,8 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "java_bytecode_language.h" #include "java_bytecode_convert_class.h" +#include "java_bytecode_convert_method.h" #include "java_bytecode_internal_additions.h" #include "java_bytecode_typecheck.h" #include "java_entry_point.h" @@ -45,6 +48,12 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) std::stoi(cmd.get_value("java-max-input-array-length")); if(cmd.isset("java-max-vla-length")) max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length")); + if(cmd.isset("lazy-methods-context-sensitive")) + lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_SENSITIVE; + else if(cmd.isset("lazy-methods")) + lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE; + else + lazy_methods_mode=LAZY_METHODS_MODE_EAGER; } /*******************************************************************\ @@ -147,6 +156,8 @@ bool java_bytecode_languaget::parse( { status() << "JAR file without entry point: loading it all" << eom; java_class_loader.load_entire_jar(path); + for(const auto &kv : java_class_loader.jar_map.at(path).entries) + main_jar_classes.push_back(kv.first); } else java_class_loader.add_jar_file(path); @@ -170,6 +181,287 @@ bool java_bytecode_languaget::parse( /*******************************************************************\ +Function: get_virtual_method_target + + Inputs: `needed_classes`: set of classes that can be instantiated. + Any potential callee not in this set will be ignored. + `call_basename`: unqualified function name with type + signature (e.g. "f:(I)") + `classname`: class name that may define or override a + function named `call_basename`. + `symbol_table`: global symtab + + Outputs: Returns the fully qualified name of `classname`'s definition + of `call_basename` if found and `classname` is present in + `needed_classes`, or irep_idt() otherwise. + + Purpose: Find a virtual callee, if one is defined and the callee type + is known to exist. + +\*******************************************************************/ + +static irep_idt get_virtual_method_target( + const std::set &needed_classes, + const irep_idt &call_basename, + const irep_idt &classname, + const symbol_tablet &symbol_table) +{ + // Program-wide, is this class ever instantiated? + if(!needed_classes.count(classname)) + return irep_idt(); + auto methodid=id2string(classname)+"."+id2string(call_basename); + if(symbol_table.has_symbol(methodid)) + return methodid; + else + return irep_idt(); +} + +/*******************************************************************\ + +Function: get_virtual_method_target + + Inputs: `c`: function call whose potential target functions should + be determined. + `needed_classes`: set of classes that can be instantiated. + Any potential callee not in this set will be ignored. + `symbol_table`: global symtab + `class_hierarchy`: global class hierarchy + + Outputs: Populates `needed_methods` with all possible `c` callees, + taking `needed_classes` into account (virtual function + overrides defined on classes that are not 'needed' are + ignored) + + Purpose: Find possible callees, excluding types that are not known + to be instantiated. + +\*******************************************************************/ + +static void get_virtual_method_targets( + const code_function_callt &c, + const std::set &needed_classes, + std::vector &needed_methods, + symbol_tablet &symbol_table, + const class_hierarchyt &class_hierarchy) +{ + const auto &called_function=c.function(); + assert(called_function.id()==ID_virtual_function); + + const auto &call_class=called_function.get(ID_C_class); + assert(call_class!=irep_idt()); + const auto &call_basename=called_function.get(ID_component_name); + assert(call_basename!=irep_idt()); + + auto old_size=needed_methods.size(); + + auto child_classes=class_hierarchy.get_children_trans(call_class); + for(const auto &child_class : child_classes) + { + auto child_method= + get_virtual_method_target( + needed_classes, + call_basename, + child_class, + symbol_table); + if(child_method!=irep_idt()) + needed_methods.push_back(child_method); + } + + irep_idt parent_class_id=call_class; + while(1) + { + auto parent_method= + get_virtual_method_target( + needed_classes, + call_basename, + parent_class_id, + symbol_table); + if(parent_method!=irep_idt()) + { + needed_methods.push_back(parent_method); + break; + } + else + { + auto findit=class_hierarchy.class_map.find(parent_class_id); + if(findit==class_hierarchy.class_map.end()) + break; + else + { + const auto &entry=findit->second; + if(entry.parents.empty()) + break; + else + parent_class_id=entry.parents[0]; + } + } + } + + if(needed_methods.size()==old_size) + { + // Didn't find any candidate callee. Generate a stub. + std::string stubname=id2string(call_class)+"."+id2string(call_basename); + symbolt symbol; + symbol.name=stubname; + symbol.base_name=call_basename; + symbol.type=c.function().type(); + symbol.value.make_nil(); + symbol.mode=ID_java; + symbol_table.add(symbol); + } +} + +/*******************************************************************\ + +Function: gather_virtual_callsites + + Inputs: `e`: expression tree to search + + Outputs: Populates `result` with pointers to each function call + within e that calls a virtual function. + + Purpose: See output + +\*******************************************************************/ + +static void gather_virtual_callsites( + const exprt &e, + std::vector &result) +{ + if(e.id()!=ID_code) + return; + const codet &c=to_code(e); + if(c.get_statement()==ID_function_call && + to_code_function_call(c).function().id()==ID_virtual_function) + result.push_back(&to_code_function_call(c)); + else + forall_operands(it, e) + gather_virtual_callsites(*it, result); +} + +/*******************************************************************\ + +Function: gather_needed_globals + + Inputs: `e`: expression tree to search + `symbol_table`: global symtab + + Outputs: Populates `needed` with global variable symbols referenced + from `e` or its children. + + Purpose: See output + +\*******************************************************************/ + +static void gather_needed_globals( + const exprt &e, + const symbol_tablet &symbol_table, + symbol_tablet &needed) +{ + if(e.id()==ID_symbol) + { + const auto &sym=symbol_table.lookup(to_symbol_expr(e).get_identifier()); + if(sym.is_static_lifetime) + needed.add(sym); + } + else + forall_operands(opit, e) + gather_needed_globals(*opit, symbol_table, needed); +} + +/*******************************************************************\ + +Function: gather_field_types + + Inputs: `class_type`: root of class tree to search + `ns`: global namespace + + Outputs: Populates `needed_classes` with all Java reference types + reachable starting at `class_type`. For example if + `class_type` is `symbol_typet("java::A")` and A has a B + field, then `B` (but not `A`) will be added to + `needed_classes`. + + Purpose: See output + +\*******************************************************************/ + +static void gather_field_types( + const typet &class_type, + const namespacet &ns, + std::set &needed_classes) +{ + const auto &underlying_type=to_struct_type(ns.follow(class_type)); + for(const auto &field : underlying_type.components()) + { + if(field.type().id()==ID_struct || field.type().id()==ID_symbol) + gather_field_types(field.type(), ns, needed_classes); + else if(field.type().id()==ID_pointer) + { + // Skip array primitive pointers, for example: + if(field.type().subtype().id()!=ID_symbol) + continue; + const auto &field_classid= + to_symbol_type(field.type().subtype()).get_identifier(); + if(needed_classes.insert(field_classid).second) + gather_field_types(field.type().subtype(), ns, needed_classes); + } + } +} + +/*******************************************************************\ + +Function: initialize_needed_classes + + Inputs: `entry_points`: list of fully-qualified function names that + we should assume are reachable + `ns`: global namespace + `ch`: global class hierarchy + + Outputs: Populates `needed_classes` with all Java reference types + whose references may be passed, directly or indirectly, + to any of the functions in `entry_points`. + + Purpose: See output + +\*******************************************************************/ + +static void initialize_needed_classes( + const std::vector &entry_points, + const namespacet &ns, + const class_hierarchyt &ch, + std::set &needed_classes) +{ + for(const auto &mname : entry_points) + { + const auto &symbol=ns.lookup(mname); + const auto &mtype=to_code_type(symbol.type); + for(const auto ¶m : mtype.parameters()) + { + if(param.type().id()==ID_pointer) + { + const auto ¶m_classid= + to_symbol_type(param.type().subtype()).get_identifier(); + std::vector class_and_parents= + ch.get_parents_trans(param_classid); + class_and_parents.push_back(param_classid); + for(const auto &classid : class_and_parents) + needed_classes.insert(classid); + gather_field_types(param.type().subtype(), ns, needed_classes); + } + } + } + + // Also add classes whose instances are magically + // created by the JVM and so won't be spotted by + // looking for constructors and calls as usual: + needed_classes.insert("java::java.lang.String"); + needed_classes.insert("java::java.lang.Class"); + needed_classes.insert("java::java.lang.Object"); +} + +/*******************************************************************\ + Function: java_bytecode_languaget::typecheck Inputs: @@ -200,7 +492,18 @@ bool java_bytecode_languaget::typecheck( symbol_table, get_message_handler(), disable_runtime_checks, - max_user_array_length)) + max_user_array_length, + lazy_methods, + lazy_methods_mode)) + return true; + } + + // Now incrementally elaborate methods + // that are reachable from this entry point. + if(lazy_methods_mode==LAZY_METHODS_MODE_CONTEXT_INSENSITIVE) + { + // ci: context-insensitive. + if(do_ci_lazy_method_conversion(symbol_table, lazy_methods)) return true; } @@ -214,6 +517,221 @@ bool java_bytecode_languaget::typecheck( /*******************************************************************\ +Function: java_bytecode_languaget::do_ci_lazy_method_conversion + + Inputs: `symbol_table`: global symbol table + `lazy_methods`: map from method names to relevant symbol + and parsed-method objects. + + Outputs: Elaborates lazily-converted methods that may be reachable + starting from the main entry point (usually provided with + the --function command-line option) (side-effect on the + symbol_table). Returns false on success. + + Purpose: Uses a simple context-insensitive ('ci') analysis to + determine which methods may be reachable from the main + entry point. In brief, static methods are reachable if we + find a callsite in another reachable site, while virtual + methods are reachable if we find a virtual callsite + targeting a compatible type *and* a constructor callsite + indicating an object of that type may be instantiated (or + evidence that an object of that type exists before the + main function is entered, such as being passed as a + parameter). + +\*******************************************************************/ + +bool java_bytecode_languaget::do_ci_lazy_method_conversion( + symbol_tablet &symbol_table, + lazy_methodst &lazy_methods) +{ + class_hierarchyt ch; + ch(symbol_table); + + std::vector method_worklist1; + std::vector method_worklist2; + + auto main_function= + get_main_symbol(symbol_table, main_class, get_message_handler(), true); + if(main_function.stop_convert) + { + // Failed, mark all functions in the given main class(es) reachable. + std::vector reachable_classes; + if(!main_class.empty()) + reachable_classes.push_back(main_class); + else + reachable_classes=main_jar_classes; + for(const auto &classname : reachable_classes) + { + const auto &methods= + java_class_loader.class_map.at(classname).parsed_class.methods; + for(const auto &method : methods) + { + const irep_idt methodid="java::"+id2string(classname)+"."+ + id2string(method.name)+":"+ + id2string(method.signature); + method_worklist2.push_back(methodid); + } + } + } + else + method_worklist2.push_back(main_function.main_function.name); + + std::set needed_classes; + initialize_needed_classes( + method_worklist2, + namespacet(symbol_table), + ch, + needed_classes); + + std::set methods_already_populated; + std::vector virtual_callsites; + + bool any_new_methods; + do + { + any_new_methods=false; + while(method_worklist2.size()!=0) + { + std::swap(method_worklist1, method_worklist2); + for(const auto &mname : method_worklist1) + { + if(!methods_already_populated.insert(mname).second) + continue; + auto findit=lazy_methods.find(mname); + if(findit==lazy_methods.end()) + { + debug() << "Skip " << mname << eom; + continue; + } + debug() << "CI lazy methods: elaborate " << mname << eom; + const auto &parsed_method=findit->second; + java_bytecode_convert_method( + *parsed_method.first, + *parsed_method.second, + symbol_table, + get_message_handler(), + disable_runtime_checks, + max_user_array_length, + safe_pointer >::create_non_null( + &method_worklist2), + safe_pointer >::create_non_null( + &needed_classes)); + gather_virtual_callsites( + symbol_table.lookup(mname).value, + virtual_callsites); + any_new_methods=true; + } + method_worklist1.clear(); + } + + // Given the object types we now know may be created, populate more + // possible virtual function call targets: + + debug() << "CI lazy methods: add virtual method targets (" + << virtual_callsites.size() + << " callsites)" + << eom; + + for(const auto &callsite : virtual_callsites) + { + // This will also create a stub if a virtual callsite has no targets. + get_virtual_method_targets( + *callsite, + needed_classes, + method_worklist2, + symbol_table, + ch); + } + } + while(any_new_methods); + + // Remove symbols for methods that were declared but never used: + symbol_tablet keep_symbols; + + for(const auto &sym : symbol_table.symbols) + { + if(sym.second.is_static_lifetime) + continue; + if(lazy_methods.count(sym.first) && + !methods_already_populated.count(sym.first)) + { + continue; + } + if(sym.second.type.id()==ID_code) + gather_needed_globals(sym.second.value, symbol_table, keep_symbols); + keep_symbols.add(sym.second); + } + + debug() << "CI lazy methods: removed " + << symbol_table.symbols.size() - keep_symbols.symbols.size() + << " unreachable methods and globals" + << eom; + + symbol_table.swap(keep_symbols); + + return false; +} + +/*******************************************************************\ + +Function: java_bytecode_languaget::lazy_methods_provided + + Inputs: None + + Outputs: Populates `methods` with the complete list of lazy methods + that are available to convert (those which are valid + parameters for `convert_lazy_method`) + + Purpose: Provide feedback to `language_filest` so that when asked + for a lazy method, it can delegate to this instance of + java_bytecode_languaget. + +\*******************************************************************/ + +void java_bytecode_languaget::lazy_methods_provided( + std::set &methods) const +{ + for(const auto &kv : lazy_methods) + methods.insert(kv.first); +} + +/*******************************************************************\ + +Function: java_bytecode_languaget::convert_lazy_method + + Inputs: `id`: method ID to convert + `symtab`: global symbol table + + Outputs: Amends the symbol table entry for function `id`, which + should be a lazy method provided by this instance of + `java_bytecode_languaget`. It should initially have a nil + value. After this method completes, it will have a value + representing the method body, identical to that produced + using eager method conversion. + + Purpose: Promote a lazy-converted method (one whose type is known + but whose body hasn't been converted) into a fully- + elaborated one. + +\*******************************************************************/ + +void java_bytecode_languaget::convert_lazy_method( + const irep_idt &id, + symbol_tablet &symtab) +{ + const auto &lazy_method_entry=lazy_methods.at(id); + java_bytecode_convert_method( + *lazy_method_entry.first, + *lazy_method_entry.second, + symtab, + get_message_handler(), + disable_runtime_checks, + max_user_array_length); +} + +/*******************************************************************\ + Function: java_bytecode_languaget::final Inputs: diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index 5937f6f4fd4..ea177e0226a 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -16,6 +16,20 @@ Author: Daniel Kroening, kroening@kroening.com #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5 +enum lazy_methods_modet +{ + LAZY_METHODS_MODE_EAGER, + LAZY_METHODS_MODE_CONTEXT_INSENSITIVE, + LAZY_METHODS_MODE_CONTEXT_SENSITIVE +}; + +typedef std::pair< + const symbolt *, + const java_bytecode_parse_treet::methodt *> + lazy_method_valuet; +typedef std::map + lazy_methodst; + class java_bytecode_languaget:public languaget { public: @@ -69,9 +83,15 @@ class java_bytecode_languaget:public languaget std::set extensions() const override; void modules_provided(std::set &modules) override; + virtual void lazy_methods_provided(std::set &) const override; + virtual void convert_lazy_method( + const irep_idt &id, symbol_tablet &) override; protected: + bool do_ci_lazy_method_conversion(symbol_tablet &, lazy_methodst &); + irep_idt main_class; + std::vector main_jar_classes; java_class_loadert java_class_loader; bool assume_inputs_non_null; // assume inputs variables to be non-null @@ -82,6 +102,8 @@ class java_bytecode_languaget:public languaget // - array size for newarray size_t max_nondet_array_length; // maximal length for non-det array creation size_t max_user_array_length; // max size for user code created arrays + lazy_methodst lazy_methods; + lazy_methods_modet lazy_methods_mode; }; languaget *new_java_bytecode_language(); diff --git a/src/java_bytecode/java_class_loader.h b/src/java_bytecode/java_class_loader.h index 4d67b3e7164..b2a4953445a 100644 --- a/src/java_bytecode/java_class_loader.h +++ b/src/java_bytecode/java_class_loader.h @@ -37,7 +37,6 @@ class java_class_loadert:public messaget jar_poolt jar_pool; -protected: class jar_map_entryt { public: diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index dcc3dead0a8..44a59091ba2 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -327,11 +327,11 @@ void java_record_outputs( } } - main_function_resultt get_main_symbol( symbol_tablet &symbol_table, const irep_idt &main_class, - message_handlert &message_handler) + message_handlert &message_handler, + bool allow_no_body) { symbolt symbol; main_function_resultt res; @@ -415,7 +415,7 @@ main_function_resultt get_main_symbol( } // check if it has a body - if(symbol.value.is_nil()) + if(symbol.value.is_nil() && !allow_no_body) { message.error() << "main method `" << main_class << "' has no body" << messaget::eom; @@ -480,7 +480,7 @@ main_function_resultt get_main_symbol( symbol=symbol_table.symbols.find(*matches.begin())->second; // check if it has a body - if(symbol.value.is_nil()) + if(symbol.value.is_nil() && !allow_no_body) { message.error() << "main method `" << main_class << "' has no body" << messaget::eom; diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h index 7fa562de89a..e6575734d80 100644 --- a/src/java_bytecode/java_entry_point.h +++ b/src/java_bytecode/java_entry_point.h @@ -28,6 +28,7 @@ typedef struct main_function_resultt get_main_symbol( symbol_tablet &symbol_table, const irep_idt &main_class, - message_handlert &); + message_handlert &, + bool allow_no_body=false); #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H diff --git a/src/java_bytecode/library/src/org/cprover/CProver.java b/src/java_bytecode/library/src/org/cprover/CProver.java new file mode 100644 index 00000000000..72c3eeb1d70 --- /dev/null +++ b/src/java_bytecode/library/src/org/cprover/CProver.java @@ -0,0 +1,11 @@ +package org.cprover; + +public final class CProver +{ + public static boolean enableAssume=true; + public static void assume(boolean condition) + { + if(enableAssume) + throw new RuntimeException("Cannot execute program with CProver.assume()"); + } +} diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 8640d735631..95b5d104a4f 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -104,8 +104,8 @@ bool language_uit::parse(const std::string &filename) return true; } - std::pair - result=language_files.filemap.insert( + std::pair + result=language_files.file_map.insert( std::pair(filename, language_filet())); language_filet &lf=result.first->second; diff --git a/src/util/Makefile b/src/util/Makefile index 6cc42a18fb8..c605d26c747 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -22,7 +22,7 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \ irep_ids.cpp byte_operators.cpp string2int.cpp file_util.cpp \ memory_info.cpp pipe_stream.cpp irep_hash.cpp endianness_map.cpp \ ssa_expr.cpp json_irep.cpp json_expr.cpp \ - string_utils.cpp + format_number_range.cpp string_utils.cpp INCLUDES= -I .. diff --git a/src/util/format_number_range.cpp b/src/util/format_number_range.cpp new file mode 100644 index 00000000000..cca3bbf154c --- /dev/null +++ b/src/util/format_number_range.cpp @@ -0,0 +1,122 @@ +/*******************************************************************\ + +Module: Format vector of numbers into a compressed range + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include +#include +#include + +#include "format_number_range.h" + +/*******************************************************************\ + +Function: format_number_range::operator() + + Inputs: vector of numbers + + Outputs: string of compressed number range representation + + Purpose: create shorter representation for output + +\*******************************************************************/ + +std::string format_number_ranget::operator()(std::vector &numbers) +{ + std::string number_range; + std::sort(numbers.begin(), numbers.end()); + unsigned end_number=numbers.back(); + if(numbers.front()==end_number) + number_range=std::to_string(end_number); // only single number + else + { + bool next=true; + bool first=true; + bool range=false; + unsigned start_number=numbers.front(); + unsigned last_number=start_number; + + for(const auto &number : numbers) + { + if(next) + { + next=false; + start_number=number; + last_number=number; + } + // advance one forward + else + { + if(number==last_number+1 && !(number==end_number)) + { + last_number++; + if(last_number>start_number+1) + range=true; + } + // end this block range + else + { + if(first) + first=false; + else + number_range+=","; + if(last_number>start_number) + { + if(range) + { + if(number==end_number && number==last_number+1) + number_range+= + std::to_string(start_number)+"-"+std::to_string(end_number); + else if(number==end_number) + number_range+= + std::to_string(start_number)+"-"+std::to_string(last_number)+ + ","+std::to_string(end_number); + else + number_range+= + std::to_string(start_number)+"-"+std::to_string(last_number); + } + else + { + if(number!=end_number) + number_range+= + std::to_string(start_number)+","+std::to_string(last_number); + else + { + if(start_number+1==last_number && last_number+1==number) + number_range+= + std::to_string(start_number)+"-"+std::to_string(end_number); + else + number_range+= + std::to_string(start_number)+ + ","+std::to_string(last_number)+ + ","+std::to_string(end_number); + } + } + start_number=number; + last_number=number; + range=false; + continue; + } + else + { + if(number!=end_number) + number_range+=std::to_string(start_number); + else + number_range+=std::to_string(start_number)+","+ + std::to_string(end_number); + start_number=number; + last_number=number; + range=false; + continue; // already set next start number + } + next=true; + } + } + } + } + assert(!number_range.empty()); + return number_range; +} diff --git a/src/util/format_number_range.h b/src/util/format_number_range.h new file mode 100644 index 00000000000..7ff016e9c4d --- /dev/null +++ b/src/util/format_number_range.h @@ -0,0 +1,21 @@ +/*******************************************************************\ + +Module: Format vector of numbers into a compressed range + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_FORMAT_NUMBER_RANGE_H +#define CPROVER_UTIL_FORMAT_NUMBER_RANGE_H + +#include +#include + +class format_number_ranget +{ +public: + std::string operator()(std::vector &); +}; + +#endif // CPROVER_UTIL_FORMAT_NUMBER_RANGE_H diff --git a/src/util/irep_ids.txt b/src/util/irep_ids.txt index 9bcb7807671..29907f11040 100644 --- a/src/util/irep_ids.txt +++ b/src/util/irep_ids.txt @@ -737,6 +737,7 @@ bswap java_bytecode_index java_instanceof java_super_method_call +skip_initialize java_enum_static_unwind string_constraint string_not_contains_constraint @@ -800,4 +801,5 @@ cprover_string_to_char_array_func cprover_string_to_lower_case_func cprover_string_to_upper_case_func cprover_string_trim_func -cprover_string_value_of_func \ No newline at end of file +cprover_string_value_of_func +basic_block_covered_lines \ No newline at end of file diff --git a/src/util/language.h b/src/util/language.h index edd83471cd5..b19615496ec 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -49,6 +49,15 @@ class languaget:public messaget virtual void modules_provided(std::set &modules) { } + // add lazy functions provided to set + + virtual void lazy_methods_provided(std::set &methods) const + { } + + // populate a lazy method + virtual void convert_lazy_method(const irep_idt &id, symbol_tablet &) + { } + // final adjustments, e.g., initialization and call to main() virtual bool final( diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp index dffad975c45..46f51564b54 100644 --- a/src/util/language_file.cpp +++ b/src/util/language_file.cpp @@ -65,6 +65,13 @@ void language_filet::get_modules() language->modules_provided(modules); } +void language_filet::convert_lazy_method( + const irep_idt &id, + symbol_tablet &symbol_table) +{ + language->convert_lazy_method(id, symbol_table); +} + /*******************************************************************\ Function: language_filest::show_parse @@ -79,8 +86,8 @@ Function: language_filest::show_parse void language_filest::show_parse(std::ostream &out) { - for(filemapt::iterator it=filemap.begin(); - it!=filemap.end(); it++) + for(file_mapt::iterator it=file_map.begin(); + it!=file_map.end(); it++) it->second.language->show_parse(out); } @@ -98,8 +105,8 @@ Function: language_filest::parse bool language_filest::parse() { - for(filemapt::iterator it=filemap.begin(); - it!=filemap.end(); it++) + for(file_mapt::iterator it=file_map.begin(); + it!=file_map.end(); it++) { // open file @@ -145,8 +152,8 @@ bool language_filest::typecheck(symbol_tablet &symbol_table) { // typecheck interfaces - for(filemapt::iterator it=filemap.begin(); - it!=filemap.end(); it++) + for(file_mapt::iterator it=file_map.begin(); + it!=file_map.end(); it++) { if(it->second.language->interfaces(symbol_table)) return true; @@ -156,8 +163,8 @@ bool language_filest::typecheck(symbol_tablet &symbol_table) unsigned collision_counter=0; - for(filemapt::iterator fm_it=filemap.begin(); - fm_it!=filemap.end(); fm_it++) + for(file_mapt::iterator fm_it=file_map.begin(); + fm_it!=file_map.end(); fm_it++) { const language_filet::modulest &modules= fm_it->second.modules; @@ -170,7 +177,7 @@ bool language_filest::typecheck(symbol_tablet &symbol_table) // these may collide, and then get renamed std::string module_name=*mo_it; - while(modulemap.find(module_name)!=modulemap.end()) + while(module_map.find(module_name)!=module_map.end()) { module_name=*mo_it+"#"+std::to_string(collision_counter); collision_counter++; @@ -179,25 +186,34 @@ bool language_filest::typecheck(symbol_tablet &symbol_table) language_modulet module; module.file=&fm_it->second; module.name=module_name; - modulemap.insert( + module_map.insert( std::pair(module.name, module)); } } // typecheck files - for(filemapt::iterator it=filemap.begin(); - it!=filemap.end(); it++) + for(file_mapt::iterator it=file_map.begin(); + it!=file_map.end(); it++) { if(it->second.modules.empty()) + { if(it->second.language->typecheck(symbol_table, "")) return true; + // register lazy methods. + // TODO: learn about modules and generalise this + // to module-providing languages if required. + std::set lazy_method_ids; + it->second.language->lazy_methods_provided(lazy_method_ids); + for(const auto &id : lazy_method_ids) + lazy_method_map[id]=&it->second; + } } // typecheck modules - for(modulemapt::iterator it=modulemap.begin(); - it!=modulemap.end(); it++) + for(module_mapt::iterator it=module_map.begin(); + it!=module_map.end(); it++) { if(typecheck_module(symbol_table, it->second)) return true; @@ -223,8 +239,8 @@ bool language_filest::final( { std::set languages; - for(filemapt::iterator it=filemap.begin(); - it!=filemap.end(); it++) + for(file_mapt::iterator it=file_map.begin(); + it!=file_map.end(); it++) { if(languages.insert(it->second.language->id()).second) if(it->second.language->final(symbol_table)) @@ -249,8 +265,8 @@ Function: language_filest::interfaces bool language_filest::interfaces( symbol_tablet &symbol_table) { - for(filemapt::iterator it=filemap.begin(); - it!=filemap.end(); it++) + for(file_mapt::iterator it=file_map.begin(); + it!=file_map.end(); it++) { if(it->second.language->interfaces(symbol_table)) return true; @@ -277,9 +293,9 @@ bool language_filest::typecheck_module( { // check module map - modulemapt::iterator it=modulemap.find(module); + module_mapt::iterator it=module_map.find(module); - if(it==modulemap.end()) + if(it==module_map.end()) { error() << "found no file that provides module " << module << eom; return true; diff --git a/src/util/language_file.h b/src/util/language_file.h index 533e8d5240e..d3184d48697 100644 --- a/src/util/language_file.h +++ b/src/util/language_file.h @@ -42,6 +42,10 @@ class language_filet void get_modules(); + void convert_lazy_method( + const irep_idt &id, + symbol_tablet &symbol_table); + language_filet(const language_filet &rhs); language_filet():language(NULL) @@ -54,15 +58,21 @@ class language_filet class language_filest:public messaget { public: - typedef std::map filemapt; - filemapt filemap; + typedef std::map file_mapt; + file_mapt file_map; + + // Contains pointers into file_mapt! + typedef std::map module_mapt; + module_mapt module_map; - typedef std::map modulemapt; - modulemapt modulemap; + // Contains pointers into filemapt! + // This is safe-ish as long as this is std::map. + typedef std::map lazy_method_mapt; + lazy_method_mapt lazy_method_map; void clear_files() { - filemap.clear(); + file_map.clear(); } bool parse(); @@ -75,10 +85,26 @@ class language_filest:public messaget bool interfaces(symbol_tablet &symbol_table); + bool has_lazy_method(const irep_idt &id) + { + return lazy_method_map.count(id); + } + + // The method must have been added to the symbol table and registered + // in lazy_method_map (currently always in language_filest::typecheck) + // for this to be legal. + void convert_lazy_method( + const irep_idt &id, + symbol_tablet &symbol_table) + { + return lazy_method_map.at(id)->convert_lazy_method(id, symbol_table); + } + void clear() { - filemap.clear(); - modulemap.clear(); + file_map.clear(); + module_map.clear(); + lazy_method_map.clear(); } protected: diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp index 338a6103e40..6a9082b6823 100644 --- a/src/util/mp_arith.cpp +++ b/src/util/mp_arith.cpp @@ -17,6 +17,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "mp_arith.h" #include "arith_tools.h" + +typedef BigInt::ullong_t ullong_t; // NOLINT(readability/identifiers) +typedef BigInt::llong_t llong_t; // NOLINT(readability/identifiers) + /*******************************************************************\ Function: >> @@ -320,3 +324,277 @@ unsigned integer2unsigned(const mp_integer &n) assert(ull <= std::numeric_limits::max()); return (unsigned)ull; } + +/*******************************************************************\ + +Function: bitwise_or + + Inputs: + + Outputs: + + Purpose: bitwise or + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer bitwise_or(const mp_integer &a, const mp_integer &b) +{ + ullong_t result=a.to_ulong()|b.to_ulong(); + return result; +} + +/*******************************************************************\ + +Function: bitwise_and + + Inputs: + + Outputs: + + Purpose: bitwise and + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer bitwise_and(const mp_integer &a, const mp_integer &b) +{ + ullong_t result=a.to_ulong()&b.to_ulong(); + return result; +} + +/*******************************************************************\ + +Function: bitwise_xor + + Inputs: + + Outputs: + + Purpose: bitwise xor + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b) +{ + ullong_t result=a.to_ulong()^b.to_ulong(); + return result; +} + +/*******************************************************************\ + +Function: bitwise_neg + + Inputs: + + Outputs: + + Purpose: bitwise negation + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer bitwise_neg(const mp_integer &a) +{ + ullong_t result=~a.to_ulong(); + return result; +} + +/*******************************************************************\ + +Function: arith_left_shift + + Inputs: + + Outputs: + + Purpose: arithmetic left shift + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer arith_left_shift( + const mp_integer &a, + const mp_integer &b, + std::size_t true_size) +{ + ullong_t shift=b.to_ulong(); + if(shift>true_size && a!=mp_integer(0)) + throw "shift value out of range"; + + llong_t result=a.to_long()<true_size) + throw "shift value out of range"; + + llong_t sign=(1<<(true_size-1))&number; + llong_t pad=(sign==0) ? 0 : ~((1<<(true_size-shift))-1); + llong_t result=(number >> shift)|pad; + return result; +} + +/*******************************************************************\ + +Function: logic_left_shift + + Inputs: + + Outputs: + + Purpose: logic left shift + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer logic_left_shift( + const mp_integer &a, + const mp_integer &b, + std::size_t true_size) +{ + ullong_t shift=b.to_ulong(); + if(shift>true_size && a!=mp_integer(0)) + throw "shift value out of range"; + llong_t result=a.to_long()<true_size) + throw "shift value out of range"; + + ullong_t result=((ullong_t)a.to_long()) >> shift; + return result; +} + +/*******************************************************************\ + +Function: rotate_right + + Inputs: + + Outputs: + + Purpose: rotates right (MSB=LSB) + bitwise operations only make sense on native objects, hence the + largest object size should be the largest available c++ integer + size (currently long long) + +\*******************************************************************/ + +mp_integer rotate_right( + const mp_integer &a, + const mp_integer &b, + std::size_t true_size) +{ + ullong_t number=a.to_ulong(); + ullong_t shift=b.to_ulong(); + if(shift>true_size) + throw "shift value out of range"; + + ullong_t revShift=true_size-shift; + ullong_t filter=1<<(true_size-1); + ullong_t result=(number >> shift)|((number<true_size) + throw "shift value out of range"; + + ullong_t revShift=true_size-shift; + ullong_t filter=1<<(true_size-1); + ullong_t result=((number<> revShift); + return result; +} diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h index 030a292bb74..046b1bff788 100644 --- a/src/util/mp_arith.h +++ b/src/util/mp_arith.h @@ -20,6 +20,28 @@ typedef BigInt mp_integer; std::ostream &operator<<(std::ostream &, const mp_integer &); mp_integer operator>>(const mp_integer &, const mp_integer &); mp_integer operator<<(const mp_integer &, const mp_integer &); +mp_integer bitwise_or(const mp_integer &, const mp_integer &); +mp_integer bitwise_and(const mp_integer &, const mp_integer &); +mp_integer bitwise_xor(const mp_integer &, const mp_integer &); +mp_integer bitwise_neg(const mp_integer &); + +mp_integer arith_left_shift( + const mp_integer &, const mp_integer &, std::size_t true_size); + +mp_integer arith_right_shift( + const mp_integer &, const mp_integer &, std::size_t true_size); + +mp_integer logic_left_shift( + const mp_integer &, const mp_integer &, std::size_t true_size); + +mp_integer logic_right_shift( + const mp_integer &, const mp_integer &, std::size_t true_size); + +mp_integer rotate_right( + const mp_integer &, const mp_integer &, std::size_t true_size); + +mp_integer rotate_left( + const mp_integer &, const mp_integer &, std::size_t true_size); const std::string integer2string(const mp_integer &, unsigned base=10); const mp_integer string2integer(const std::string &, unsigned base=10); @@ -28,5 +50,6 @@ const mp_integer binary2integer(const std::string &, bool is_signed); mp_integer::ullong_t integer2ulong(const mp_integer &); std::size_t integer2size_t(const mp_integer &); unsigned integer2unsigned(const mp_integer &); +const mp_integer mp_zero=string2integer("0"); #endif // CPROVER_UTIL_MP_ARITH_H diff --git a/src/util/safe_pointer.h b/src/util/safe_pointer.h new file mode 100644 index 00000000000..47e52ac13fe --- /dev/null +++ b/src/util/safe_pointer.h @@ -0,0 +1,64 @@ +/*******************************************************************\ + +Module: Simple checked pointers + +Author: Chris Smowton, chris@smowton.net + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_SAFE_POINTER_H +#define CPROVER_UTIL_SAFE_POINTER_H + +template class safe_pointer +{ + public: + operator bool() const + { + return !!ptr; + } + + T *get() const + { + assert(ptr && "dereferenced a null safe pointer"); + return ptr; + } + + T &operator*() const + { + return *get(); + } + + T *operator->() const + { + return get(); + } + + static safe_pointer create_null() + { + return safe_pointer(); + } + + static safe_pointer create_non_null( + T *target) + { + assert(target && "initialized safe pointer with null"); + return safe_pointer(target); + } + + static safe_pointer create_maybe_null( + T *target) + { + return safe_pointer(target); + } + + protected: + T *ptr; + + explicit safe_pointer(T *target) : ptr(target) + {} + + safe_pointer() : ptr(nullptr) + {} +}; + +#endif diff --git a/src/util/source_location.h b/src/util/source_location.h index b24befcb8c4..9d905c775cb 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -73,6 +73,11 @@ class source_locationt:public irept return get(ID_java_bytecode_index); } + const irep_idt &get_basic_block_covered_lines() const + { + return get(ID_basic_block_covered_lines); + } + void set_file(const irep_idt &file) { set(ID_file, file); @@ -128,6 +133,11 @@ class source_locationt:public irept set(ID_java_bytecode_index, index); } + void set_basic_block_covered_lines(const irep_idt &covered_lines) + { + return set(ID_basic_block_covered_lines, covered_lines); + } + void set_hide() { set(ID_hide, true); diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index c75d7d2ed92..affd2907eb5 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -78,6 +78,19 @@ static void build_ssa_identifier_rec( assert(false); } +/* Used to determine whether or not an identifier can be built + * before trying and getting an exception */ +bool ssa_exprt::can_build_identifier(const exprt &expr) +{ + if(expr.id()==ID_symbol) + return true; + else if(expr.id()==ID_member || + expr.id()==ID_index) + return can_build_identifier(expr.op0()); + else + return false; +} + /*******************************************************************\ Function: ssa_exprt::build_identifier diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index 446e82169d6..e18862fa9f9 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -64,7 +64,7 @@ class ssa_exprt:public symbol_exprt const irep_idt get_l1_object_identifier() const { - #if 0 + #if 1 return get_l1_object().get_identifier(); #else // the above is the clean version, this is the fast one, using @@ -134,6 +134,10 @@ class ssa_exprt:public symbol_exprt const irep_idt &l0, const irep_idt &l1, const irep_idt &l2); + + /* Used to determine whether or not an identifier can be built + * before trying and getting an exception */ + static bool can_build_identifier(const exprt &src); }; /*! \brief Cast a generic exprt to an \ref ssa_exprt diff --git a/src/util/std_expr.h b/src/util/std_expr.h index a2f78ab25e8..30296525585 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2979,6 +2979,17 @@ class member_exprt:public exprt { return op0(); } + + // Retrieves the object(symbol) this member corresponds to + inline const symbol_exprt &symbol() const + { + const exprt &op=op0(); + if(op.id()==ID_member) + { + return static_cast(op).symbol(); + } + return to_symbol_expr(op); + } }; /*! \brief Cast a generic exprt to a \ref member_exprt