diff --git a/regression/cbmc-java/NullPointer3/NullPointer3.class b/regression/cbmc-java/NullPointer3/NullPointer3.class index 8ad089310c3..b79f5adef44 100644 Binary files a/regression/cbmc-java/NullPointer3/NullPointer3.class and b/regression/cbmc-java/NullPointer3/NullPointer3.class differ diff --git a/regression/cbmc-java/NullPointer3/NullPointer3.java b/regression/cbmc-java/NullPointer3/NullPointer3.java index 00004f14467..fa8b227dd94 100644 --- a/regression/cbmc-java/NullPointer3/NullPointer3.java +++ b/regression/cbmc-java/NullPointer3/NullPointer3.java @@ -4,5 +4,4 @@ public static void main(String[] args) { throw null; // NULL pointer dereference } - } diff --git a/regression/cbmc-java/NullPointer3/test.desc b/regression/cbmc-java/NullPointer3/test.desc index cc33c21738b..5dd14d8dfb9 100644 --- a/regression/cbmc-java/NullPointer3/test.desc +++ b/regression/cbmc-java/NullPointer3/test.desc @@ -1,9 +1,9 @@ CORE NullPointer3.class ---pointer-check --stop-on-fail +--pointer-check ^EXIT=10$ ^SIGNAL=0$ -^ file NullPointer3.java line 5 function java::NullPointer3.main:\(\[Ljava/lang/String;\)V bytecode_index 1$ +^.*Throw null: FAILURE$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-java/exceptions1/A.class b/regression/cbmc-java/exceptions1/A.class new file mode 100644 index 00000000000..eb19ef6be2b Binary files /dev/null and b/regression/cbmc-java/exceptions1/A.class differ diff --git a/regression/cbmc-java/exceptions1/B.class b/regression/cbmc-java/exceptions1/B.class new file mode 100644 index 00000000000..47ae8f218e4 Binary files /dev/null and b/regression/cbmc-java/exceptions1/B.class differ diff --git a/regression/cbmc-java/exceptions1/C.class b/regression/cbmc-java/exceptions1/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions1/C.class differ diff --git a/regression/cbmc-java/exceptions1/D.class b/regression/cbmc-java/exceptions1/D.class new file mode 100644 index 00000000000..12179e84294 Binary files /dev/null and b/regression/cbmc-java/exceptions1/D.class differ diff --git a/regression/cbmc-java/exceptions1/test.class b/regression/cbmc-java/exceptions1/test.class new file mode 100644 index 00000000000..c76687b1bc7 Binary files /dev/null and b/regression/cbmc-java/exceptions1/test.class differ diff --git a/regression/cbmc-java/exceptions1/test.desc b/regression/cbmc-java/exceptions1/test.desc new file mode 100644 index 00000000000..638351f4397 --- /dev/null +++ b/regression/cbmc-java/exceptions1/test.desc @@ -0,0 +1,10 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 26 function.*: FAILURE$ +\*\* 1 of 9 failed \(2 iterations\)$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions1/test.java b/regression/cbmc-java/exceptions1/test.java new file mode 100644 index 00000000000..bc925b32d65 --- /dev/null +++ b/regression/cbmc-java/exceptions1/test.java @@ -0,0 +1,30 @@ +class A extends Throwable {} +class B extends A {} +class C extends B {} +class D extends C {} + +public class test { + public static void main (String arg[]) { + try { + D d = new D(); + C c = new C(); + B b = new B(); + A a = new A(); + A e = a; + throw e; + } + catch(D exc) { + assert false; + } + catch(C exc) { + assert false; + } + catch(B exc) { + assert false; + } + catch(A exc) { + assert false; + } + } +} + diff --git a/regression/cbmc-java/exceptions10/A.class b/regression/cbmc-java/exceptions10/A.class new file mode 100644 index 00000000000..963ae156be0 Binary files /dev/null and b/regression/cbmc-java/exceptions10/A.class differ diff --git a/regression/cbmc-java/exceptions10/B.class b/regression/cbmc-java/exceptions10/B.class new file mode 100644 index 00000000000..47ae8f218e4 Binary files /dev/null and b/regression/cbmc-java/exceptions10/B.class differ diff --git a/regression/cbmc-java/exceptions10/C.class b/regression/cbmc-java/exceptions10/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions10/C.class differ diff --git a/regression/cbmc-java/exceptions10/test.class b/regression/cbmc-java/exceptions10/test.class new file mode 100644 index 00000000000..2ff5d07c9a9 Binary files /dev/null and b/regression/cbmc-java/exceptions10/test.class differ diff --git a/regression/cbmc-java/exceptions10/test.desc b/regression/cbmc-java/exceptions10/test.desc new file mode 100644 index 00000000000..4654e88cbb6 --- /dev/null +++ b/regression/cbmc-java/exceptions10/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 12 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions10/test.java b/regression/cbmc-java/exceptions10/test.java new file mode 100644 index 00000000000..14feb2f9b1d --- /dev/null +++ b/regression/cbmc-java/exceptions10/test.java @@ -0,0 +1,25 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +public class test { + static void foo() { + try { + A b = new A(); + throw b; + } + catch(A exc) { + assert false; + } + } + + public static void main (String args[]) { + try { + A a = new A(); + foo(); + } + catch(B exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/exceptions11/A.class b/regression/cbmc-java/exceptions11/A.class new file mode 100644 index 00000000000..ad46eafd1d9 Binary files /dev/null and b/regression/cbmc-java/exceptions11/A.class differ diff --git a/regression/cbmc-java/exceptions11/B.class b/regression/cbmc-java/exceptions11/B.class new file mode 100644 index 00000000000..3af09687e1a Binary files /dev/null and b/regression/cbmc-java/exceptions11/B.class differ diff --git a/regression/cbmc-java/exceptions11/test.class b/regression/cbmc-java/exceptions11/test.class new file mode 100644 index 00000000000..0bba6142244 Binary files /dev/null and b/regression/cbmc-java/exceptions11/test.class differ diff --git a/regression/cbmc-java/exceptions11/test.desc b/regression/cbmc-java/exceptions11/test.desc new file mode 100644 index 00000000000..cb92a091217 --- /dev/null +++ b/regression/cbmc-java/exceptions11/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 36 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions11/test.java b/regression/cbmc-java/exceptions11/test.java new file mode 100644 index 00000000000..032af621fc3 --- /dev/null +++ b/regression/cbmc-java/exceptions11/test.java @@ -0,0 +1,39 @@ +class A extends RuntimeException { + int i=1; +}; + +class B extends A { +}; + +public class test { + static int foo(int k) { + try { + if(k==0) + { + A a = new A(); + throw a; + } + else + { + A b = new A(); + throw b; + } + + } + catch(B exc) { + assert exc.i==1; + } + return 1; + } + + + public static void main (String args[]) { + try { + A a = new A(); + foo(6); + } + catch(A exc) { + assert exc.i==2; + } + } +} diff --git a/regression/cbmc-java/exceptions12/A.class b/regression/cbmc-java/exceptions12/A.class new file mode 100644 index 00000000000..963ae156be0 Binary files /dev/null and b/regression/cbmc-java/exceptions12/A.class differ diff --git a/regression/cbmc-java/exceptions12/B.class b/regression/cbmc-java/exceptions12/B.class new file mode 100644 index 00000000000..47ae8f218e4 Binary files /dev/null and b/regression/cbmc-java/exceptions12/B.class differ diff --git a/regression/cbmc-java/exceptions12/C.class b/regression/cbmc-java/exceptions12/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions12/C.class differ diff --git a/regression/cbmc-java/exceptions12/F.class b/regression/cbmc-java/exceptions12/F.class new file mode 100644 index 00000000000..fa452c17721 Binary files /dev/null and b/regression/cbmc-java/exceptions12/F.class differ diff --git a/regression/cbmc-java/exceptions12/test.class b/regression/cbmc-java/exceptions12/test.class new file mode 100644 index 00000000000..a4350fcd81d Binary files /dev/null and b/regression/cbmc-java/exceptions12/test.class differ diff --git a/regression/cbmc-java/exceptions12/test.desc b/regression/cbmc-java/exceptions12/test.desc new file mode 100644 index 00000000000..4654e88cbb6 --- /dev/null +++ b/regression/cbmc-java/exceptions12/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 12 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions12/test.java b/regression/cbmc-java/exceptions12/test.java new file mode 100644 index 00000000000..5828419fac6 --- /dev/null +++ b/regression/cbmc-java/exceptions12/test.java @@ -0,0 +1,27 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +class F { + void foo() { + try { + B b = new B(); + throw b; + } + catch(B exc) { + assert false; + } + } +} + +public class test { + public static void main (String args[]) { + try { + F f = new F(); + f.foo(); + } + catch(B exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/exceptions13/A.class b/regression/cbmc-java/exceptions13/A.class new file mode 100644 index 00000000000..963ae156be0 Binary files /dev/null and b/regression/cbmc-java/exceptions13/A.class differ diff --git a/regression/cbmc-java/exceptions13/B.class b/regression/cbmc-java/exceptions13/B.class new file mode 100644 index 00000000000..47ae8f218e4 Binary files /dev/null and b/regression/cbmc-java/exceptions13/B.class differ diff --git a/regression/cbmc-java/exceptions13/C.class b/regression/cbmc-java/exceptions13/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions13/C.class differ diff --git a/regression/cbmc-java/exceptions13/F.class b/regression/cbmc-java/exceptions13/F.class new file mode 100644 index 00000000000..85408ad5f8a Binary files /dev/null and b/regression/cbmc-java/exceptions13/F.class differ diff --git a/regression/cbmc-java/exceptions13/test.class b/regression/cbmc-java/exceptions13/test.class new file mode 100644 index 00000000000..a4350fcd81d Binary files /dev/null and b/regression/cbmc-java/exceptions13/test.class differ diff --git a/regression/cbmc-java/exceptions13/test.desc b/regression/cbmc-java/exceptions13/test.desc new file mode 100644 index 00000000000..cb7c1b81341 --- /dev/null +++ b/regression/cbmc-java/exceptions13/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 25 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions13/test.java b/regression/cbmc-java/exceptions13/test.java new file mode 100644 index 00000000000..56d763f68d3 --- /dev/null +++ b/regression/cbmc-java/exceptions13/test.java @@ -0,0 +1,28 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +class F { + void foo() { + try { + B b = new B(); + throw b; + } + catch(B exc) { + throw exc; + } + } +} + +public class test { + + public static void main (String args[]) { + try { + F f = new F(); + f.foo(); + } + catch(B exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/exceptions14/A.class b/regression/cbmc-java/exceptions14/A.class new file mode 100644 index 00000000000..963ae156be0 Binary files /dev/null and b/regression/cbmc-java/exceptions14/A.class differ diff --git a/regression/cbmc-java/exceptions14/B.class b/regression/cbmc-java/exceptions14/B.class new file mode 100644 index 00000000000..47ae8f218e4 Binary files /dev/null and b/regression/cbmc-java/exceptions14/B.class differ diff --git a/regression/cbmc-java/exceptions14/C.class b/regression/cbmc-java/exceptions14/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions14/C.class differ diff --git a/regression/cbmc-java/exceptions14/test.class b/regression/cbmc-java/exceptions14/test.class new file mode 100644 index 00000000000..1737cbde0b5 Binary files /dev/null and b/regression/cbmc-java/exceptions14/test.class differ diff --git a/regression/cbmc-java/exceptions14/test.desc b/regression/cbmc-java/exceptions14/test.desc new file mode 100644 index 00000000000..dc5ca4fa5cb --- /dev/null +++ b/regression/cbmc-java/exceptions14/test.desc @@ -0,0 +1,8 @@ +CORE +test.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions14/test.java b/regression/cbmc-java/exceptions14/test.java new file mode 100644 index 00000000000..24f44a5d3d9 --- /dev/null +++ b/regression/cbmc-java/exceptions14/test.java @@ -0,0 +1,24 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +public class test { + public static void main (String args[]) { + try { + try { + C c = new C(); + A a = new A(); + } + catch(C exc) { + assert false; + } + catch(B exc) { + assert false; + } + } + catch(A exc) { + assert false; + } + + } +} diff --git a/regression/cbmc-java/exceptions15/InetAddress.class b/regression/cbmc-java/exceptions15/InetAddress.class new file mode 100644 index 00000000000..3229324e624 Binary files /dev/null and b/regression/cbmc-java/exceptions15/InetAddress.class differ diff --git a/regression/cbmc-java/exceptions15/InetSocketAddress.class b/regression/cbmc-java/exceptions15/InetSocketAddress.class new file mode 100644 index 00000000000..1303bb9a0a9 Binary files /dev/null and b/regression/cbmc-java/exceptions15/InetSocketAddress.class differ diff --git a/regression/cbmc-java/exceptions15/test.class b/regression/cbmc-java/exceptions15/test.class new file mode 100644 index 00000000000..b3f0d2daa47 Binary files /dev/null and b/regression/cbmc-java/exceptions15/test.class differ diff --git a/regression/cbmc-java/exceptions15/test.desc b/regression/cbmc-java/exceptions15/test.desc new file mode 100644 index 00000000000..f2414f96a67 --- /dev/null +++ b/regression/cbmc-java/exceptions15/test.desc @@ -0,0 +1,8 @@ +CORE +test.class +--function test.translate +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions15/test.java b/regression/cbmc-java/exceptions15/test.java new file mode 100644 index 00000000000..057d3223a63 --- /dev/null +++ b/regression/cbmc-java/exceptions15/test.java @@ -0,0 +1,20 @@ +class InetAddress {} +class InetSocketAddress {} + +public class test { + public String lookupPtrRecord(InetAddress address) { + return "Foo"; + } + + public InetAddress reverse(InetAddress address) { + return address; + } + + public void translate(InetAddress address, int i) { + try { + String domainName = lookupPtrRecord(reverse(address)); + } catch (Exception e) { + assert false; + } + } +} diff --git a/regression/cbmc-java/exceptions16/A.class b/regression/cbmc-java/exceptions16/A.class new file mode 100644 index 00000000000..963ae156be0 Binary files /dev/null and b/regression/cbmc-java/exceptions16/A.class differ diff --git a/regression/cbmc-java/exceptions16/B.class b/regression/cbmc-java/exceptions16/B.class new file mode 100644 index 00000000000..47ae8f218e4 Binary files /dev/null and b/regression/cbmc-java/exceptions16/B.class differ diff --git a/regression/cbmc-java/exceptions16/C.class b/regression/cbmc-java/exceptions16/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions16/C.class differ diff --git a/regression/cbmc-java/exceptions16/test.class b/regression/cbmc-java/exceptions16/test.class new file mode 100644 index 00000000000..189317658ce Binary files /dev/null and b/regression/cbmc-java/exceptions16/test.class differ diff --git a/regression/cbmc-java/exceptions16/test.desc b/regression/cbmc-java/exceptions16/test.desc new file mode 100644 index 00000000000..960b995f7d3 --- /dev/null +++ b/regression/cbmc-java/exceptions16/test.desc @@ -0,0 +1,9 @@ +CORE +test.class +--function test.foo +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 18 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions16/test.java b/regression/cbmc-java/exceptions16/test.java new file mode 100644 index 00000000000..9d1c2729516 --- /dev/null +++ b/regression/cbmc-java/exceptions16/test.java @@ -0,0 +1,21 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +public class test { + static void foo (int x) { + try { + x++; + } + catch(A exc) { + assert false; + } + + try { + throw new B(); + } + catch(B exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/exceptions18/A.class b/regression/cbmc-java/exceptions18/A.class new file mode 100644 index 00000000000..eb37079f4ed Binary files /dev/null and b/regression/cbmc-java/exceptions18/A.class differ diff --git a/regression/cbmc-java/exceptions18/Test.class b/regression/cbmc-java/exceptions18/Test.class new file mode 100644 index 00000000000..1c2f3dba008 Binary files /dev/null and b/regression/cbmc-java/exceptions18/Test.class differ diff --git a/regression/cbmc-java/exceptions18/Test.java b/regression/cbmc-java/exceptions18/Test.java new file mode 100644 index 00000000000..92ecf88c98b --- /dev/null +++ b/regression/cbmc-java/exceptions18/Test.java @@ -0,0 +1,23 @@ +class A extends RuntimeException {} +class B extends A {} + +public class Test { + void foo() + { + A a=new A(); + throw a; + } + void goo() + { + try + { + foo(); + assert false; + } + catch(B e) + { + assert false; + } + } + +} diff --git a/regression/cbmc-java/exceptions18/test.desc b/regression/cbmc-java/exceptions18/test.desc new file mode 100644 index 00000000000..eff4927d2da --- /dev/null +++ b/regression/cbmc-java/exceptions18/test.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--function Test.goo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions2/A.class b/regression/cbmc-java/exceptions2/A.class new file mode 100644 index 00000000000..eb19ef6be2b Binary files /dev/null and b/regression/cbmc-java/exceptions2/A.class differ diff --git a/regression/cbmc-java/exceptions2/B.class b/regression/cbmc-java/exceptions2/B.class new file mode 100644 index 00000000000..47ae8f218e4 Binary files /dev/null and b/regression/cbmc-java/exceptions2/B.class differ diff --git a/regression/cbmc-java/exceptions2/C.class b/regression/cbmc-java/exceptions2/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions2/C.class differ diff --git a/regression/cbmc-java/exceptions2/test.class b/regression/cbmc-java/exceptions2/test.class new file mode 100644 index 00000000000..a6aed72e3b3 Binary files /dev/null and b/regression/cbmc-java/exceptions2/test.class differ diff --git a/regression/cbmc-java/exceptions2/test.desc b/regression/cbmc-java/exceptions2/test.desc new file mode 100644 index 00000000000..8645e5ea074 --- /dev/null +++ b/regression/cbmc-java/exceptions2/test.desc @@ -0,0 +1,10 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 15 function.*: FAILURE$ +^\*\* 1 of 5 failed \(2 iterations\)$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions2/test.java b/regression/cbmc-java/exceptions2/test.java new file mode 100644 index 00000000000..420b50219c1 --- /dev/null +++ b/regression/cbmc-java/exceptions2/test.java @@ -0,0 +1,18 @@ +class A extends Throwable {} +class B extends A {} +class C extends B {} + +public class test { + public static void main (String args[]) { + try { + B b = new B(); + throw b; + } + catch(C exc) { + assert false; + } + catch(B exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/exceptions3/A.class b/regression/cbmc-java/exceptions3/A.class new file mode 100644 index 00000000000..eb19ef6be2b Binary files /dev/null and b/regression/cbmc-java/exceptions3/A.class differ diff --git a/regression/cbmc-java/exceptions3/B.class b/regression/cbmc-java/exceptions3/B.class new file mode 100644 index 00000000000..47ae8f218e4 Binary files /dev/null and b/regression/cbmc-java/exceptions3/B.class differ diff --git a/regression/cbmc-java/exceptions3/C.class b/regression/cbmc-java/exceptions3/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions3/C.class differ diff --git a/regression/cbmc-java/exceptions3/test.class b/regression/cbmc-java/exceptions3/test.class new file mode 100644 index 00000000000..2e669adea88 Binary files /dev/null and b/regression/cbmc-java/exceptions3/test.class differ diff --git a/regression/cbmc-java/exceptions3/test.desc b/regression/cbmc-java/exceptions3/test.desc new file mode 100644 index 00000000000..8b917c506ae --- /dev/null +++ b/regression/cbmc-java/exceptions3/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 14 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions3/test.java b/regression/cbmc-java/exceptions3/test.java new file mode 100644 index 00000000000..9f6a55e11b4 --- /dev/null +++ b/regression/cbmc-java/exceptions3/test.java @@ -0,0 +1,17 @@ +class A extends Throwable {} +class B extends A {} +class C extends B {} + +public class test { + public static void main (String args[]) { + try { + throw new B(); + } + catch(C exc) { + assert false; + } + catch(B exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/exceptions4/A.class b/regression/cbmc-java/exceptions4/A.class new file mode 100644 index 00000000000..eb19ef6be2b Binary files /dev/null and b/regression/cbmc-java/exceptions4/A.class differ diff --git a/regression/cbmc-java/exceptions4/B.class b/regression/cbmc-java/exceptions4/B.class new file mode 100644 index 00000000000..47ae8f218e4 Binary files /dev/null and b/regression/cbmc-java/exceptions4/B.class differ diff --git a/regression/cbmc-java/exceptions4/C.class b/regression/cbmc-java/exceptions4/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions4/C.class differ diff --git a/regression/cbmc-java/exceptions4/test.class b/regression/cbmc-java/exceptions4/test.class new file mode 100644 index 00000000000..0718c0cd81c Binary files /dev/null and b/regression/cbmc-java/exceptions4/test.class differ diff --git a/regression/cbmc-java/exceptions4/test.desc b/regression/cbmc-java/exceptions4/test.desc new file mode 100644 index 00000000000..dc5ca4fa5cb --- /dev/null +++ b/regression/cbmc-java/exceptions4/test.desc @@ -0,0 +1,8 @@ +CORE +test.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions4/test.java b/regression/cbmc-java/exceptions4/test.java new file mode 100644 index 00000000000..8a144925f9f --- /dev/null +++ b/regression/cbmc-java/exceptions4/test.java @@ -0,0 +1,21 @@ +class A extends Throwable {} +class B extends A {} +class C extends B {} + +public class test { + public static void main (String args[]) { + try { + B b = new B(); + throw b; + } + catch(C exc) { + System.out.println("C"); + assert false; + } + catch(B exc) { + System.out.println("B"); + } + } +} + + diff --git a/regression/cbmc-java/exceptions5/A.class b/regression/cbmc-java/exceptions5/A.class new file mode 100644 index 00000000000..eb19ef6be2b Binary files /dev/null and b/regression/cbmc-java/exceptions5/A.class differ diff --git a/regression/cbmc-java/exceptions5/B.class b/regression/cbmc-java/exceptions5/B.class new file mode 100644 index 00000000000..47ae8f218e4 Binary files /dev/null and b/regression/cbmc-java/exceptions5/B.class differ diff --git a/regression/cbmc-java/exceptions5/C.class b/regression/cbmc-java/exceptions5/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions5/C.class differ diff --git a/regression/cbmc-java/exceptions5/D.class b/regression/cbmc-java/exceptions5/D.class new file mode 100644 index 00000000000..12179e84294 Binary files /dev/null and b/regression/cbmc-java/exceptions5/D.class differ diff --git a/regression/cbmc-java/exceptions5/test.class b/regression/cbmc-java/exceptions5/test.class new file mode 100644 index 00000000000..7873fdd3ad4 Binary files /dev/null and b/regression/cbmc-java/exceptions5/test.class differ diff --git a/regression/cbmc-java/exceptions5/test.desc b/regression/cbmc-java/exceptions5/test.desc new file mode 100644 index 00000000000..dc5ca4fa5cb --- /dev/null +++ b/regression/cbmc-java/exceptions5/test.desc @@ -0,0 +1,8 @@ +CORE +test.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions5/test.java b/regression/cbmc-java/exceptions5/test.java new file mode 100644 index 00000000000..6ba7b653b89 --- /dev/null +++ b/regression/cbmc-java/exceptions5/test.java @@ -0,0 +1,30 @@ +class A extends Throwable {} +class B extends A {} +class C extends B {} +class D extends C {}public class test { + public static void main (String arg[]) { + try { + D d = new D(); + C c = new C(); + B b = new B(); + A a = new A(); + A e = a; + throw e; + } + catch(D exc) { + System.out.println("D"); + assert false; + } + catch(C exc) { + System.out.println("C"); + assert false; + } + catch(B exc) { + System.out.println("B"); + assert false; + } + catch(A exc) { + System.out.println("A"); + } + } +} diff --git a/regression/cbmc-java/exceptions6/A.class b/regression/cbmc-java/exceptions6/A.class new file mode 100644 index 00000000000..fbaaf105dba Binary files /dev/null and b/regression/cbmc-java/exceptions6/A.class differ diff --git a/regression/cbmc-java/exceptions6/B.class b/regression/cbmc-java/exceptions6/B.class new file mode 100644 index 00000000000..ec8971aad2e Binary files /dev/null and b/regression/cbmc-java/exceptions6/B.class differ diff --git a/regression/cbmc-java/exceptions6/C.class b/regression/cbmc-java/exceptions6/C.class new file mode 100644 index 00000000000..aeeb2cef5bf Binary files /dev/null and b/regression/cbmc-java/exceptions6/C.class differ diff --git a/regression/cbmc-java/exceptions6/D.class b/regression/cbmc-java/exceptions6/D.class new file mode 100644 index 00000000000..12179e84294 Binary files /dev/null and b/regression/cbmc-java/exceptions6/D.class differ diff --git a/regression/cbmc-java/exceptions6/test.class b/regression/cbmc-java/exceptions6/test.class new file mode 100644 index 00000000000..e0c57f3e318 Binary files /dev/null and b/regression/cbmc-java/exceptions6/test.class differ diff --git a/regression/cbmc-java/exceptions6/test.desc b/regression/cbmc-java/exceptions6/test.desc new file mode 100644 index 00000000000..79549d80731 --- /dev/null +++ b/regression/cbmc-java/exceptions6/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 18 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions6/test.java b/regression/cbmc-java/exceptions6/test.java new file mode 100644 index 00000000000..fd9a7fd5326 --- /dev/null +++ b/regression/cbmc-java/exceptions6/test.java @@ -0,0 +1,26 @@ +class A extends RuntimeException { + int i; + A() { + i = 1; + } +} +class B extends A {} +class C extends B {} + +public class test { + public static void main (String args[]) { + try { + try { + int i = 0; + throw new A(); + } + catch(A exc) { + assert exc.i==2; + } + } + catch(B exc) { + assert exc.i==2; + } + + } +} diff --git a/regression/cbmc-java/exceptions7/A.class b/regression/cbmc-java/exceptions7/A.class new file mode 100644 index 00000000000..963ae156be0 Binary files /dev/null and b/regression/cbmc-java/exceptions7/A.class differ diff --git a/regression/cbmc-java/exceptions7/B.class b/regression/cbmc-java/exceptions7/B.class new file mode 100644 index 00000000000..47ae8f218e4 Binary files /dev/null and b/regression/cbmc-java/exceptions7/B.class differ diff --git a/regression/cbmc-java/exceptions7/C.class b/regression/cbmc-java/exceptions7/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions7/C.class differ diff --git a/regression/cbmc-java/exceptions7/test.class b/regression/cbmc-java/exceptions7/test.class new file mode 100644 index 00000000000..f9e3cf244d9 Binary files /dev/null and b/regression/cbmc-java/exceptions7/test.class differ diff --git a/regression/cbmc-java/exceptions7/test.desc b/regression/cbmc-java/exceptions7/test.desc new file mode 100644 index 00000000000..e138e4349ec --- /dev/null +++ b/regression/cbmc-java/exceptions7/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 21 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions7/test.java b/regression/cbmc-java/exceptions7/test.java new file mode 100644 index 00000000000..e03be8a56fb --- /dev/null +++ b/regression/cbmc-java/exceptions7/test.java @@ -0,0 +1,25 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +public class test { + public static void main (String args[]) { + try { + try { + C c = new C(); + A a = new A(); + throw a; + } + catch(C exc) { + assert false; + } + catch(B exc) { + assert false; + } + } + catch(A exc) { + assert false; + } + + } +} diff --git a/regression/cbmc-java/exceptions8/A.class b/regression/cbmc-java/exceptions8/A.class new file mode 100644 index 00000000000..963ae156be0 Binary files /dev/null and b/regression/cbmc-java/exceptions8/A.class differ diff --git a/regression/cbmc-java/exceptions8/B.class b/regression/cbmc-java/exceptions8/B.class new file mode 100644 index 00000000000..47ae8f218e4 Binary files /dev/null and b/regression/cbmc-java/exceptions8/B.class differ diff --git a/regression/cbmc-java/exceptions8/C.class b/regression/cbmc-java/exceptions8/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions8/C.class differ diff --git a/regression/cbmc-java/exceptions8/test.class b/regression/cbmc-java/exceptions8/test.class new file mode 100644 index 00000000000..c5420fc89b8 Binary files /dev/null and b/regression/cbmc-java/exceptions8/test.class differ diff --git a/regression/cbmc-java/exceptions8/test.desc b/regression/cbmc-java/exceptions8/test.desc new file mode 100644 index 00000000000..a400cbb8d02 --- /dev/null +++ b/regression/cbmc-java/exceptions8/test.desc @@ -0,0 +1,9 @@ +CORE +test.class + +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file test.java line 23 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions8/test.java b/regression/cbmc-java/exceptions8/test.java new file mode 100644 index 00000000000..7d6af5324b7 --- /dev/null +++ b/regression/cbmc-java/exceptions8/test.java @@ -0,0 +1,29 @@ +class A extends RuntimeException {} +class B extends A {} +class C extends B {} + +public class test { + static void foo() { + try { + B b = new B(); + throw b; + } + catch(C exc) { + int i=0; + } + } + + public static void main (String args[]) { + try { + A a = new A(); + foo(); + throw a; + } + catch(B exc) { + assert false; + } + catch(A exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/exceptions9/A.class b/regression/cbmc-java/exceptions9/A.class new file mode 100644 index 00000000000..ad46eafd1d9 Binary files /dev/null and b/regression/cbmc-java/exceptions9/A.class differ diff --git a/regression/cbmc-java/exceptions9/B.class b/regression/cbmc-java/exceptions9/B.class new file mode 100644 index 00000000000..3af09687e1a Binary files /dev/null and b/regression/cbmc-java/exceptions9/B.class differ diff --git a/regression/cbmc-java/exceptions9/C.class b/regression/cbmc-java/exceptions9/C.class new file mode 100644 index 00000000000..0c9779a4c2b Binary files /dev/null and b/regression/cbmc-java/exceptions9/C.class differ diff --git a/regression/cbmc-java/exceptions9/test.class b/regression/cbmc-java/exceptions9/test.class new file mode 100644 index 00000000000..ee137ed9bf6 Binary files /dev/null and b/regression/cbmc-java/exceptions9/test.class differ diff --git a/regression/cbmc-java/exceptions9/test.desc b/regression/cbmc-java/exceptions9/test.desc new file mode 100644 index 00000000000..dc5ca4fa5cb --- /dev/null +++ b/regression/cbmc-java/exceptions9/test.desc @@ -0,0 +1,8 @@ +CORE +test.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/exceptions9/test.java b/regression/cbmc-java/exceptions9/test.java new file mode 100644 index 00000000000..53f7838fd03 --- /dev/null +++ b/regression/cbmc-java/exceptions9/test.java @@ -0,0 +1,39 @@ +class A extends RuntimeException { + int i=1; +}; + +class B extends A { +}; + +public class test { + static int foo(int k) { + try { + if(k==0) + { + A a = new A(); + throw a; + } + else + { + A b = new A(); + throw b; + } + + } + catch(B exc) { + assert exc.i==1; + } + return 1; + } + + + public static void main (String args[]) { + try { + A a = new A(); + foo(6); + } + catch(A exc) { + assert exc.i==1; + } + } +} diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc index b2b26ecb9ce..2e196d82e8c 100644 --- a/regression/cbmc-java/virtual7/test.desc +++ b/regression/cbmc-java/virtual7/test.desc @@ -3,10 +3,9 @@ test.class --show-goto-functions ^EXIT=0$ ^SIGNAL=0$ -IF "java::E".*THEN GOTO [12] -IF "java::B".*THEN GOTO [12] -IF "java::D".*THEN GOTO [12] -IF "java::C".*THEN GOTO [12] +IF "java::E".*THEN GOTO [67] +IF "java::B".*THEN GOTO [67] +IF "java::D".*THEN GOTO [67] +IF "java::C".*THEN GOTO [67] -- IF "java::A".*THEN GOTO -GOTO 4 diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 7364752d093..6eb044257c6 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -894,7 +895,9 @@ bool cbmc_parse_optionst::process_goto_program( cmdline.isset("pointer-check")); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(symbol_table, goto_functions); - // Java instanceof -> clsid comparison: + // remove catch and throw + remove_exceptions(symbol_table, goto_functions); + // Similar removal of RTTI inspection: remove_instanceof(symbol_table, goto_functions); // full slice? diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 68e28755041..e462740c1cc 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -387,7 +388,9 @@ bool goto_analyzer_parse_optionst::process_goto_program( remove_function_pointers(goto_model, cmdline.isset("pointer-check")); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); - // Java instanceof -> clsid comparison: + // remove Java throw and catch + remove_exceptions(goto_model); + // remove rtti remove_instanceof(goto_model); // do partial inlining diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 3cbbac3a55b..209a5daeed1 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -810,6 +811,8 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal( cmdline.isset("pointer-check")); status() << "Virtual function removal" << eom; remove_virtual_functions(symbol_table, goto_functions); + status() << "Catch and throw removal" << eom; + remove_exceptions(symbol_table, goto_functions); status() << "Java instanceof removal" << eom; remove_instanceof(symbol_table, goto_functions); } diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index d8cb835e4a8..d5cc5ea25eb 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -13,8 +13,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \ remove_unused_functions.cpp remove_vector.cpp \ wp.cpp goto_clean_expr.cpp safety_checker.cpp parameter_assignments.cpp \ compute_called_functions.cpp link_to_library.cpp \ - remove_returns.cpp osx_fat_reader.cpp remove_complex.cpp \ - goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \ + remove_returns.cpp remove_exceptions.cpp osx_fat_reader.cpp \ + remove_complex.cpp goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \ graphml_witness.cpp remove_virtual_functions.cpp \ class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp \ slice_global_inits.cpp goto_inline_class.cpp class_identifier.cpp \ diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index a3124f3b898..58cf6666897 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -47,6 +47,85 @@ static bool is_empty(const goto_programt &goto_program) /*******************************************************************\ +Function: finish_catch_push_targets + + Inputs: + + Outputs: + + Purpose: Populate the CATCH instructions with the targets + corresponding to their associated labels + +\*******************************************************************/ + +static void finish_catch_push_targets(goto_programt &dest) +{ + std::map label_targets; + + // in the first pass collect the labels and the corresponding targets + Forall_goto_program_instructions(it, dest) + { + if(!it->labels.empty()) + { + for(auto label : it->labels) + // record the label and the corresponding target + label_targets.insert(std::make_pair(label, it)); + } + } + + // in the second pass set the targets + Forall_goto_program_instructions(it, dest) + { + if(it->is_catch()) + { + bool handler_added=true; + irept exceptions=it->code.find(ID_exception_list); + + if(exceptions.is_nil() && + it->code.has_operands()) + exceptions=it->code.op0().find(ID_exception_list); + + const irept::subt &exception_list=exceptions.get_sub(); + + if(!exception_list.empty()) + { + // in this case we have a CATCH_PUSH + irept handlers=it->code.find(ID_label); + if(handlers.is_nil() && + it->code.has_operands()) + handlers=it->code.op0().find(ID_label); + const irept::subt &handler_list=handlers.get_sub(); + + // some handlers may not have been converted (if there was no + // exception to be caught); in such a situation we abort + for(const auto &handler : handler_list) + { + if(label_targets.find(handler.id())==label_targets.end()) + { + handler_added=false; + break; + } + } + + if(!handler_added) + continue; + + for(const auto &handler : handler_list) + { + std::map::const_iterator handler_it= + label_targets.find(handler.id()); + assert(handler_it!=label_targets.end()); + // set the target + it->targets.push_back(handler_it->second); + } + } + } + } +} + +/******************************************************************* \ + Function: goto_convertt::finish_gotos Inputs: @@ -302,6 +381,7 @@ void goto_convertt::goto_convert_rec( finish_gotos(dest); finish_computed_gotos(dest); finish_guarded_gotos(dest); + finish_catch_push_targets(dest); } /*******************************************************************\ diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index feab8197046..05c35efa3c0 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -94,6 +94,9 @@ class goto_convertt:public messaget side_effect_exprt &expr, goto_programt &dest, bool result_is_used); + void remove_push_catch( + side_effect_exprt &expr, + goto_programt &dest); void remove_assignment( side_effect_exprt &expr, goto_programt &dest, @@ -237,6 +240,7 @@ class goto_convertt:public messaget void convert_msc_try_except(const codet &code, goto_programt &dest); void convert_msc_leave(const codet &code, goto_programt &dest); void convert_try_catch(const codet &code, goto_programt &dest); + void convert_java_try_catch(const codet &code, goto_programt &dest); void convert_CPROVER_try_catch(const codet &code, goto_programt &dest); void convert_CPROVER_try_finally(const codet &code, goto_programt &dest); void convert_CPROVER_throw(const codet &code, goto_programt &dest); diff --git a/src/goto-programs/goto_convert_exceptions.cpp b/src/goto-programs/goto_convert_exceptions.cpp index 8d04f3cca16..63f503e8a0b 100644 --- a/src/goto-programs/goto_convert_exceptions.cpp +++ b/src/goto-programs/goto_convert_exceptions.cpp @@ -128,6 +128,73 @@ void goto_convertt::convert_msc_leave( /*******************************************************************\ +Function: goto_convertt::convert_java_try_catch + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_convertt::convert_java_try_catch( + const codet &code, + goto_programt &dest) +{ + assert(!code.operands().empty()); + + // add the CATCH instruction to 'dest' + goto_programt::targett catch_instruction=dest.add_instruction(); + catch_instruction->make_catch(); + catch_instruction->code.set_statement(ID_catch); + catch_instruction->source_location=code.source_location(); + catch_instruction->function=code.source_location().get_function(); + + // the CATCH instruction is annotated with a list of exception IDs + const irept exceptions=code.op0().find(ID_exception_list); + if(exceptions.is_not_nil()) + { + irept::subt exceptions_sub=exceptions.get_sub(); + irept::subt &exception_list= + catch_instruction->code.add(ID_exception_list).get_sub(); + exception_list.resize(exceptions_sub.size()); + for(size_t i=0; icode.add(ID_label).get_sub(); + handlers_list.resize(handlers_sub.size()); + for(size_t i=0; icode.get_sub().resize(1); + catch_instruction->code.get_sub()[0]=code.op0().op0(); + } + + // add a SKIP target for the end of everything + goto_programt end; + goto_programt::targett end_target=end.add_instruction(); + end_target->make_skip(); + end_target->source_location=code.source_location(); + end_target->function=code.source_location().get_function(); + + // add the end-target + dest.destructive_append(end); +} + +/*******************************************************************\ + Function: goto_convertt::convert_try_catch Inputs: diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index f34ee9d03a0..dbebb856ec1 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -767,6 +767,29 @@ void goto_convertt::remove_statement_expression( /*******************************************************************\ +Function: goto_convertt::remove_push_catch + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_convertt::remove_push_catch( + side_effect_exprt &expr, + goto_programt &dest) +{ + // we only get here for ID_push_catch, which is only used for Java + convert_java_try_catch(code_expressiont(expr), dest); + + // the result can't be used, these are void + expr.make_nil(); +} + +/*******************************************************************\ + Function: goto_convertt::remove_side_effect Inputs: @@ -837,6 +860,8 @@ void goto_convertt::remove_side_effect( // the result can't be used, these are void expr.make_nil(); } + else if(statement==ID_push_catch) + remove_push_catch(expr, dest); else { error().source_location=expr.find_source_location(); diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 77161fcb4d8..bd9cb39c73e 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -474,6 +474,14 @@ class goto_program_templatet instructions.clear(); } + targett get_end_function() + { + assert(!instructions.empty()); + targett end_function=--instructions.end(); + assert(end_function->is_end_function()); + return end_function; + } + //! Copy a full goto program, preserving targets void copy_from(const goto_program_templatet &src); diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp new file mode 100644 index 00000000000..e73eba8d2ec --- /dev/null +++ b/src/goto-programs/remove_exceptions.cpp @@ -0,0 +1,543 @@ +/*******************************************************************\ + +Module: Remove exception handling + +Author: Cristina David + +Date: December 2016 + +\*******************************************************************/ + +#ifdef DEBUG +#include +#endif + +#include +#include + +#include +#include + +#include "remove_exceptions.h" + +class remove_exceptionst +{ + typedef std::vector> catch_handlerst; + typedef std::vector stack_catcht; + +public: + explicit remove_exceptionst(symbol_tablet &_symbol_table): + symbol_table(_symbol_table) + { + } + + void operator()( + goto_functionst &goto_functions); + +protected: + symbol_tablet &symbol_table; + + void add_exceptional_returns( + const goto_functionst::function_mapt::iterator &); + + void instrument_exception_handler( + const goto_functionst::function_mapt::iterator &, + const goto_programt::instructionst::iterator &); + + void instrument_throw( + const goto_functionst::function_mapt::iterator &, + const goto_programt::instructionst::iterator &, + const stack_catcht &, + std::vector &); + + void instrument_function_call( + const goto_functionst::function_mapt::iterator &, + const goto_programt::instructionst::iterator &, + const stack_catcht &, + std::vector &); + + void instrument_exceptions( + const goto_functionst::function_mapt::iterator &); +}; + +/*******************************************************************\ + +Function: remove_exceptionst::add_exceptional_returns + +Inputs: + +Outputs: + +Purpose: adds exceptional return variables for every function that + may escape exceptions + +\*******************************************************************/ + +void remove_exceptionst::add_exceptional_returns( + const goto_functionst::function_mapt::iterator &func_it) +{ + const irep_idt &function_id=func_it->first; + goto_programt &goto_program=func_it->second.body; + + assert(symbol_table.has_symbol(function_id)); + const symbolt &function_symbol=symbol_table.lookup(function_id); + + // for now only add exceptional returns for Java + if(function_symbol.mode!=ID_java) + return; + + if(goto_program.empty()) + return; + + // We generate an exceptional return value for any function that has + // a throw or a function call. This can be improved by only considering + // function calls that may escape exceptions. However, this will + // require multiple passes. + bool add_exceptional_var=false; + forall_goto_program_instructions(instr_it, goto_program) + if(instr_it->is_throw() || instr_it->is_function_call()) + { + add_exceptional_var=true; + break; + } + + if(add_exceptional_var) + { + // look up the function symbol + symbol_tablet::symbolst::iterator s_it= + symbol_table.symbols.find(function_id); + + assert(s_it!=symbol_table.symbols.end()); + + auxiliary_symbolt new_symbol; + new_symbol.is_static_lifetime=true; + new_symbol.module=function_symbol.module; + new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX; + new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX; + new_symbol.mode=function_symbol.mode; + new_symbol.type=typet(ID_pointer, empty_typet()); + symbol_table.add(new_symbol); + + // initialize the exceptional return with NULL + symbol_exprt lhs_expr_null=new_symbol.symbol_expr(); + null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet()))); + goto_programt::targett t_null= + goto_program.insert_before(goto_program.instructions.begin()); + t_null->make_assignment(); + t_null->source_location= + goto_program.instructions.begin()->source_location; + t_null->code=code_assignt( + lhs_expr_null, + rhs_expr_null); + t_null->function=function_id; + } +} + +/*******************************************************************\ + +Function: remove_exceptionst::instrument_exception_handler + +Inputs: + +Outputs: + +Purpose: at the beginning of each handler in function f + adds exc=f#exception_value; f#exception_value=NULL; + +\*******************************************************************/ + +void remove_exceptionst::instrument_exception_handler( + const goto_functionst::function_mapt::iterator &func_it, + const goto_programt::instructionst::iterator &instr_it) +{ + const irep_idt &function_id=func_it->first; + goto_programt &goto_program=func_it->second.body; + + assert(instr_it->type==CATCH && instr_it->code.has_operands()); + + // retrieve the exception variable + const exprt &exception=instr_it->code.op0(); + + if(symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX)) + { + const symbolt &function_symbol= + symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + // next we reset the exceptional return to NULL + symbol_exprt lhs_expr_null=function_symbol.symbol_expr(); + null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet()))); + + // add the assignment + goto_programt::targett t_null=goto_program.insert_after(instr_it); + t_null->make_assignment(); + t_null->source_location=instr_it->source_location; + t_null->code=code_assignt( + lhs_expr_null, + rhs_expr_null); + t_null->function=instr_it->function; + + // add the assignment exc=f#exception_value + symbol_exprt rhs_expr_exc=function_symbol.symbol_expr(); + + goto_programt::targett t_exc=goto_program.insert_after(instr_it); + t_exc->make_assignment(); + t_exc->source_location=instr_it->source_location; + t_exc->code=code_assignt( + typecast_exprt(exception, rhs_expr_exc.type()), + rhs_expr_exc); + t_exc->function=instr_it->function; + } + instr_it->make_skip(); +} + +/*******************************************************************\ + +Function: remove_exceptionst::instrument_throw + +Inputs: + +Outputs: + +Purpose: instruments each throw with conditional GOTOS to the + corresponding exception handlers + +\*******************************************************************/ + +void remove_exceptionst::instrument_throw( + const goto_functionst::function_mapt::iterator &func_it, + const goto_programt::instructionst::iterator &instr_it, + const remove_exceptionst::stack_catcht &stack_catch, + std::vector &locals) +{ + assert(instr_it->type==THROW); + + goto_programt &goto_program=func_it->second.body; + const irep_idt &function_id=func_it->first; + + assert(instr_it->code.operands().size()==1); + + // find the end of the function + goto_programt::targett end_function=goto_program.get_end_function(); + if(end_function!=instr_it) + { + // jump to the end of the function + // this will appear after the GOTO-based dynamic dispatch below + goto_programt::targett t_end=goto_program.insert_after(instr_it); + t_end->make_goto(end_function); + t_end->source_location=instr_it->source_location; + t_end->function=instr_it->function; + } + + + // find the symbol corresponding to the caught exceptions + const symbolt &exc_symbol= + symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + symbol_exprt exc_thrown=exc_symbol.symbol_expr(); + + // add GOTOs implementing the dynamic dispatch of the + // exception handlers + for(std::size_t i=stack_catch.size(); i-->0;) + { + for(std::size_t j=stack_catch[i].size(); j-->0;) + { + goto_programt::targett new_state_pc= + stack_catch[i][j].second; + + // find handler + goto_programt::targett t_exc=goto_program.insert_after(instr_it); + t_exc->make_goto(new_state_pc); + t_exc->source_location=instr_it->source_location; + t_exc->function=instr_it->function; + + // use instanceof to check that this is the correct handler + symbol_typet type(stack_catch[i][j].first); + type_exprt expr(type); + + binary_predicate_exprt check(exc_thrown, ID_java_instanceof, expr); + t_exc->guard=check; + } + } + + // add dead instructions + for(const auto &local : locals) + { + goto_programt::targett t_dead=goto_program.insert_after(instr_it); + t_dead->make_dead(); + t_dead->code=code_deadt(local); + t_dead->source_location=instr_it->source_location; + t_dead->function=instr_it->function; + } + + // replace "throw x;" by "f#exception_value=x;" + exprt exc_expr=instr_it->code; + while(exc_expr.id()!=ID_symbol && exc_expr.has_operands()) + exc_expr=exc_expr.op0(); + + // add the assignment with the appropriate cast + code_assignt assignment(typecast_exprt(exc_thrown, exc_expr.type()), + exc_expr); + // now turn the `throw' into `assignment' + instr_it->type=ASSIGN; + instr_it->code=assignment; +} + +/*******************************************************************\ + +Function: remove_exceptionst::instrument_function_call + +Inputs: + +Outputs: + +Purpose: instruments each function call that may escape exceptions + with conditional GOTOS to the corresponding exception handlers + +\*******************************************************************/ + +void remove_exceptionst::instrument_function_call( + const goto_functionst::function_mapt::iterator &func_it, + const goto_programt::instructionst::iterator &instr_it, + const stack_catcht &stack_catch, + std::vector &locals) +{ + assert(instr_it->type==FUNCTION_CALL); + + goto_programt &goto_program=func_it->second.body; + const irep_idt &function_id=func_it->first; + + // save the address of the next instruction + goto_programt::instructionst::iterator next_it=instr_it; + next_it++; + + code_function_callt &function_call=to_code_function_call(instr_it->code); + assert(function_call.function().id()==ID_symbol); + const irep_idt &callee_id= + to_symbol_expr(function_call.function()).get_identifier(); + + if(symbol_table.has_symbol(id2string(callee_id)+EXC_SUFFIX)) + { + // we may have an escaping exception + const symbolt &callee_exc_symbol= + symbol_table.lookup(id2string(callee_id)+EXC_SUFFIX); + symbol_exprt callee_exc=callee_exc_symbol.symbol_expr(); + + // find the end of the function + goto_programt::targett end_function=goto_program.get_end_function(); + if(end_function!=instr_it) + { + // jump to the end of the function + // this will appear after the GOTO-based dynamic dispatch below + goto_programt::targett t_end=goto_program.insert_after(instr_it); + t_end->make_goto(end_function); + t_end->source_location=instr_it->source_location; + t_end->function=instr_it->function; + } + + for(std::size_t i=stack_catch.size(); i-->0;) + { + for(std::size_t j=stack_catch[i].size(); j-->0;) + { + goto_programt::targett new_state_pc; + new_state_pc=stack_catch[i][j].second; + goto_programt::targett t_exc=goto_program.insert_after(instr_it); + t_exc->make_goto(new_state_pc); + t_exc->source_location=instr_it->source_location; + t_exc->function=instr_it->function; + // use instanceof to check that this is the correct handler + symbol_typet type(stack_catch[i][j].first); + type_exprt expr(type); + binary_predicate_exprt check_instanceof( + callee_exc, + ID_java_instanceof, + expr); + t_exc->guard=check_instanceof; + } + } + + // add dead instructions + for(const auto &local : locals) + { + goto_programt::targett t_dead=goto_program.insert_after(instr_it); + t_dead->make_dead(); + t_dead->code=code_deadt(local); + t_dead->source_location=instr_it->source_location; + t_dead->function=instr_it->function; + } + + // add a null check (so that instanceof can be applied) + equal_exprt eq_null( + callee_exc, + null_pointer_exprt(pointer_typet(empty_typet()))); + goto_programt::targett t_null=goto_program.insert_after(instr_it); + t_null->make_goto(next_it); + t_null->source_location=instr_it->source_location; + t_null->function=instr_it->function; + t_null->guard=eq_null; + + // after each function call g() in function f + // adds f#exception_value=g#exception_value; + const symbolt &caller= + symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + const symbol_exprt &lhs_expr=caller.symbol_expr(); + + goto_programt::targett t=goto_program.insert_after(instr_it); + t->make_assignment(); + t->source_location=instr_it->source_location; + t->code=code_assignt(lhs_expr, callee_exc); + t->function=instr_it->function; + } +} + +/*******************************************************************\ + +Function: remove_exceptionst::instrument_exceptions + +Inputs: + +Outputs: + +Purpose: instruments throws, function calls that may escape exceptions + and exception handlers. Additionally, it re-computes + the live-range of local variables in order to add DEAD instructions. + +\*******************************************************************/ + +void remove_exceptionst::instrument_exceptions( + const goto_functionst::function_mapt::iterator &func_it) +{ + stack_catcht stack_catch; // stack of try-catch blocks + std::vector> stack_locals; // stack of local vars + std::vector locals; + goto_programt &goto_program=func_it->second.body; + + if(goto_program.empty()) + return; + Forall_goto_program_instructions(instr_it, goto_program) + { + if(instr_it->is_decl()) + { + code_declt decl=to_code_decl(instr_it->code); + locals.push_back(decl.symbol()); + } + // it's a CATCH but not a handler (as it has no operands) + else if(instr_it->type==CATCH && !instr_it->code.has_operands()) + { + if(instr_it->targets.empty()) // pop + { + // pop the local vars stack + if(!stack_locals.empty()) + { + locals=stack_locals.back(); + stack_locals.pop_back(); + } + // pop from the stack if possible + if(!stack_catch.empty()) + { + stack_catch.pop_back(); + } + else + { +#ifdef DEBUG + std::cout << "Remove exceptions: empty stack" << std::endl; +#endif + } + } + else // push + { + stack_locals.push_back(locals); + locals.clear(); + + remove_exceptionst::catch_handlerst exception; + stack_catch.push_back(exception); + remove_exceptionst::catch_handlerst &last_exception= + stack_catch.back(); + + // copy targets + const irept::subt &exception_list= + instr_it->code.find(ID_exception_list).get_sub(); + assert(exception_list.size()==instr_it->targets.size()); + + // Fill the map with the catch type and the target + unsigned i=0; + for(auto target : instr_it->targets) + { + last_exception.push_back( + std::make_pair(exception_list[i].id(), target)); + i++; + } + } + instr_it->make_skip(); + } + // CATCH handler + else if(instr_it->type==CATCH && instr_it->code.has_operands()) + { + instrument_exception_handler(func_it, instr_it); + } + else if(instr_it->type==THROW) + { + instrument_throw(func_it, instr_it, stack_catch, locals); + } + else if(instr_it->type==FUNCTION_CALL) + { + instrument_function_call(func_it, instr_it, stack_catch, locals); + } + } +} + +/*******************************************************************\ + +Function: remove_exceptionst::operator() + +Inputs: + +Outputs: + +Purpose: + +\*******************************************************************/ + +void remove_exceptionst::operator()(goto_functionst &goto_functions) +{ + Forall_goto_functions(it, goto_functions) + add_exceptional_returns(it); + Forall_goto_functions(it, goto_functions) + instrument_exceptions(it); +} + +/*******************************************************************\ + +Function: remove_exceptions + +Inputs: + +Outputs: + +Purpose: removes throws/CATCH-POP/CATCH-PUSH + +\*******************************************************************/ + +void remove_exceptions( + symbol_tablet &symbol_table, + goto_functionst &goto_functions) +{ + remove_exceptionst remove_exceptions(symbol_table); + remove_exceptions(goto_functions); +} + +/*******************************************************************\ + +Function: remove_exceptions + +Inputs: + +Outputs: + +Purpose: removes throws/CATCH-POP/CATCH-PUSH + +\*******************************************************************/ + +void remove_exceptions(goto_modelt &goto_model) +{ + remove_exceptionst remove_exceptions(goto_model.symbol_table); + remove_exceptions(goto_model.goto_functions); +} diff --git a/src/goto-programs/remove_exceptions.h b/src/goto-programs/remove_exceptions.h new file mode 100644 index 00000000000..89162b5833d --- /dev/null +++ b/src/goto-programs/remove_exceptions.h @@ -0,0 +1,24 @@ +/*******************************************************************\ + +Module: Remove function exceptional returns + +Author: Cristina David + +Date: December 2016 + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_EXCEPTIONS_H +#define CPROVER_GOTO_PROGRAMS_REMOVE_EXCEPTIONS_H + +#include + +#define EXC_SUFFIX "#exception_value" + +// Removes 'throw x' and CATCH-PUSH/CATCH-POP +// and adds the required instrumentation (GOTOs and assignments) + +void remove_exceptions(symbol_tablet &, goto_functionst &); +void remove_exceptions(goto_modelt &); + +#endif diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index f101d19c824..3e9cebc116a 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -108,6 +108,25 @@ exprt::operandst java_bytecode_convert_methodt::pop(std::size_t n) return operands; } +/*******************************************************************\ + +Function: java_bytecode_convert_methodt::pop_residue + +Inputs: + +Outputs: + +Purpose: removes minimum(n, stack.size()) elements from the stack + +\*******************************************************************/ + +void java_bytecode_convert_methodt::pop_residue(std::size_t n) +{ + std::size_t residue_size=std::min(n, stack.size()); + + stack.resize(stack.size()-residue_size); +} + void java_bytecode_convert_methodt::push(const exprt::operandst &o) { stack.resize(stack.size()+o.size()); @@ -169,7 +188,6 @@ const exprt java_bytecode_convert_methodt::variable( symbol_exprt result(identifier, t); result.set(ID_C_base_name, base_name); used_local_names.insert(result); - return result; } else @@ -798,8 +816,10 @@ static void gather_symbol_live_ranges( } } else + { forall_operands(it, e) gather_symbol_live_ranges(pc, *it, result); + } } /*******************************************************************\ @@ -866,6 +886,26 @@ codet java_bytecode_convert_methodt::convert_instructions( a_entry.first->second.successors.push_back(next->address); } + if(i_it->statement=="athrow" || + i_it->statement=="invokestatic" || + i_it->statement=="invokevirtual" || + i_it->statement=="invokespecial" || + i_it->statement=="invokeinterface") + { + // find the corresponding try-catch blocks and add the handlers + // to the targets + for(const auto &exception_row : method.exception_table) + { + if(i_it->address>=exception_row.start_pc && + i_it->addresssecond.successors.push_back( + exception_row.handler_pc); + targets.insert(exception_row.handler_pc); + } + } + } + if(i_it->statement=="goto" || i_it->statement==patternt("if_?cmp??") || i_it->statement==patternt("if??") || @@ -943,7 +983,6 @@ codet java_bytecode_convert_methodt::convert_instructions( setup_local_variables(method, address_map); std::set working_set; - bool assertion_failure=false; if(!instructions.empty()) working_set.insert(instructions.front().address); @@ -953,6 +992,7 @@ codet java_bytecode_convert_methodt::convert_instructions( std::set::iterator cur=working_set.begin(); address_mapt::iterator a_it=address_map.find(*cur); assert(a_it!=address_map.end()); + unsigned cur_pc=*cur; working_set.erase(cur); if(a_it->second.done) @@ -989,6 +1029,48 @@ codet java_bytecode_convert_methodt::convert_instructions( statement=std::string(id2string(statement), 0, statement.size()-2); } + // we throw away the first statement in an exception handler + // as we don't know if a function call had a normal or exceptional return + auto it=method.exception_table.begin(); + for(; it!=method.exception_table.end(); ++it) + { + if(cur_pc==it->handler_pc) + { + exprt exc_var=variable( + arg0, statement[0], + i_it->address, + NO_CAST); + + // throw away the operands + pop_residue(bytecode_info.pop); + + // add a CATCH-PUSH signaling a handler + side_effect_expr_catcht catch_handler_expr; + // pack the exception variable so that it can be used + // later for instrumentation + catch_handler_expr.get_sub().resize(1); + catch_handler_expr.get_sub()[0]=exc_var; + + code_expressiont catch_handler(catch_handler_expr); + code_labelt newlabel(label(std::to_string(cur_pc)), + code_blockt()); + + code_blockt label_block=to_code_block(newlabel.code()); + code_blockt handler_block; + handler_block.move_to_operands(c); + handler_block.move_to_operands(catch_handler); + handler_block.move_to_operands(label_block); + c=handler_block; + break; + } + } + + if(it!=method.exception_table.end()) + { + // go straight to the next statement + continue; + } + exprt::operandst op=pop(bytecode_info.pop); exprt::operandst results; results.resize(bytecode_info.push, nil_exprt()); @@ -1001,21 +1083,30 @@ codet java_bytecode_convert_methodt::convert_instructions( else if(statement=="athrow") { assert(op.size()==1 && results.size()==1); - if(!assertion_failure) - { - side_effect_expr_throwt throw_expr; - throw_expr.add_source_location()=i_it->source_location; - throw_expr.copy_to_operands(op[0]); - c=code_expressiont(throw_expr); - results[0]=op[0]; - } - else + code_blockt block; + if(!disable_runtime_checks) { - // TODO: this can be removed once we properly handle throw - // if this athrow is generated by an assertion, then skip it - c=code_skipt(); - assertion_failure=false; + // TODO throw NullPointerException instead + const typecast_exprt lhs(op[0], pointer_typet(empty_typet())); + const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type()))); + const exprt not_equal_null( + binary_relation_exprt(lhs, ID_notequal, rhs)); + code_assertt check(not_equal_null); + check.add_source_location() + .set_comment("Throw null"); + check.add_source_location() + .set_property_class("null-pointer-exception"); + block.move_to_operands(check); } + + side_effect_expr_throwt throw_expr; + throw_expr.add_source_location()=i_it->source_location; + throw_expr.copy_to_operands(op[0]); + c=code_expressiont(throw_expr); + results[0]=op[0]; + + block.move_to_operands(c); + c=block; } else if(statement=="checkcast") { @@ -1061,13 +1152,6 @@ codet java_bytecode_convert_methodt::convert_instructions( statement=="invokevirtual" || statement=="invokestatic") { - // Remember that this is triggered by an assertion - if(statement=="invokespecial" && - id2string(arg0.get(ID_identifier)) - .find("AssertionError")!=std::string::npos) - { - assertion_failure=true; - } const bool use_this(statement!="invokestatic"); const bool is_virtual( statement=="invokevirtual" || statement=="invokeinterface"); @@ -1992,6 +2076,115 @@ codet java_bytecode_convert_methodt::convert_instructions( c.operands()=op; } + // next we do the exception handling + std::vector exception_ids; + std::vector handler_labels; + + // for each try-catch add a CATCH-PUSH instruction + // each CATCH-PUSH records a list of all the handler labels + // together with a list of all the exception ids + + // be aware of different try-catch blocks with the same starting pc + std::size_t pos=0; + std::size_t end_pc=0; + while(possource_location.get_line().empty()) c.add_source_location()=i_it->source_location; @@ -2003,6 +2196,18 @@ codet java_bytecode_convert_methodt::convert_instructions( address_mapt::iterator a_it2=address_map.find(address); assert(a_it2!=address_map.end()); + // we don't worry about exception handlers as we don't load the + // operands from the stack anyway -- we keep explicit global + // exception variables + for(const auto &exception_row : method.exception_table) + { + if(address==exception_row.handler_pc) + { + stack.clear(); + break; + } + } + if(!stack.empty() && a_it2->second.predecessors.size()>1) { // copy into temporaries @@ -2067,8 +2272,6 @@ codet java_bytecode_convert_methodt::convert_instructions( } } - // TODO: add exception handlers from exception table - // review successor computation of athrow! code_blockt code; // Add anonymous locals to the symtab: @@ -2097,6 +2300,7 @@ codet java_bytecode_convert_methodt::convert_instructions( // First create a simple flat list of basic blocks. We'll add lexical nesting // constructs as variable live-ranges require next. bool start_new_block=true; + int previous_address=-1; for(const auto &address_pair : address_map) { const unsigned address=address_pair.first; @@ -2110,6 +2314,16 @@ codet java_bytecode_convert_methodt::convert_instructions( // (e.g. due to exceptional control flow) if(!start_new_block) start_new_block=address_pair.second.predecessors.size()>1; + // Start a new lexical block if we've just entered a try block + if(!start_new_block && previous_address!=-1) + { + for(const auto &exception_row : method.exception_table) + if(exception_row.start_pc==previous_address) + { + start_new_block=true; + break; + } + } if(start_new_block) { @@ -2129,6 +2343,8 @@ codet java_bytecode_convert_methodt::convert_instructions( add_to_block.add(c); } start_new_block=address_pair.second.successors.size()>1; + + previous_address=address; } // Find out where temporaries are used: diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index ae4ba711640..4fb24c47b84 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -141,6 +141,7 @@ class java_bytecode_convert_methodt:public messaget exprt::operandst pop(std::size_t n); + void pop_residue(std::size_t n); void push(const exprt::operandst &o); bool is_constructor(const class_typet::methodt &method); diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 518e64a2ecd..54aa9382759 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -32,6 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -369,6 +370,8 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) remove_vector(goto_model); // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(goto_model); + // Java throw and catch -> explicit exceptional return variables: + remove_exceptions(goto_model); // Java instanceof -> clsid comparison: remove_instanceof(goto_model); rewrite_union(goto_model); diff --git a/src/util/irep_ids.txt b/src/util/irep_ids.txt index 9bcb7807671..066a5f831cc 100644 --- a/src/util/irep_ids.txt +++ b/src/util/irep_ids.txt @@ -738,6 +738,7 @@ java_bytecode_index java_instanceof java_super_method_call java_enum_static_unwind +push_catch string_constraint string_not_contains_constraint cprover_char_literal_func @@ -800,4 +801,4 @@ 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 diff --git a/src/util/std_code.h b/src/util/std_code.h index 08aec694e9e..17d038274a3 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -1122,6 +1122,35 @@ inline const side_effect_expr_throwt &to_side_effect_expr_throw( assert(expr.get(ID_statement)==ID_throw); return static_cast(expr); } +/*! \brief A side effect that pushes/pops a catch handler +*/ +class side_effect_expr_catcht:public side_effect_exprt +{ +public: + side_effect_expr_catcht():side_effect_exprt(ID_push_catch) + { + } + explicit side_effect_expr_catcht(const irept &exception_list): + side_effect_exprt(ID_push_catch) + { + set(ID_exception_list, exception_list); + } +}; + +static inline side_effect_expr_catcht &to_side_effect_expr_catch(exprt &expr) +{ + assert(expr.id()==ID_side_effect); + assert(expr.get(ID_statement)==ID_push_catch); + return static_cast(expr); +} + +static inline const side_effect_expr_catcht &to_side_effect_expr_catch( + const exprt &expr) +{ + assert(expr.id()==ID_side_effect); + assert(expr.get(ID_statement)==ID_push_catch); + return static_cast(expr); +} /*! \brief A try/catch block */