Skip to content

Commit 3bd5e1a

Browse files
jeannielynnmoultonjeannielynnmoulton
committed
Adds summary for remove_exceptions.
1 parent dbd6988 commit 3bd5e1a

File tree

1 file changed

+153
-2
lines changed

1 file changed

+153
-2
lines changed

‎jbmc/src/java_bytecode/README.md

Lines changed: 153 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,9 +39,160 @@ To be documented.
3939

4040
To be documented.
4141

42-
\section java-bytecode-remove-exceptions remove_exceptions
42+
\section java-bytecode-remove-exceptions Remove exceptions
4343

44-
To be documented.
44+
When `remove_exceptions` is called on the goto model, the goto model contains
45+
complex instructions such as CATCH-POP, CATCH-PUSH and THROW. In order to
46+
analyze the goto model, the instructions must be simplified to use more basic
47+
instructions - this is called "lowering". This class lowers CATCH and
48+
THROW instructions.
49+
50+
Exceptions that have been thrown, but not yet caught are stored the global
51+
`@inflight_exception`. When they have been caught, the global
52+
`@inflight_exception` is set back to null and ready for the next exception.
53+
54+
\subsection Throw
55+
56+
Consider a simple method `testException(I)V`:
57+
58+
```java
59+
public void testException(int i) throws Exception {
60+
if (i < 0) {
61+
throw new Exception();
62+
}
63+
field = i;
64+
}
65+
```
66+
67+
The goto for `testException(I)V` before `remove_exceptions` (removing comments
68+
and replacing irrelevant parts with `...`) is:
69+
70+
```
71+
com.diffblue.regression.TestExceptions.testException(int) /* java::com.diffblue.regression.TestExceptions.testException:(I)V */
72+
IF i >= 0 THEN GOTO 3
73+
struct java.lang.Exception *new_tmp0;
74+
new_tmp0 = new struct java.lang.Exception;
75+
IF !(new_tmp0 == null) THEN GOTO 1
76+
77+
...
78+
79+
1: SKIP
80+
new_tmp0 . java.lang.Exception.<init>:()V();
81+
82+
...
83+
84+
2: SKIP
85+
THROW: throw(new_tmp0)
86+
dead new_tmp0;
87+
88+
...
89+
90+
```
91+
where there is a `THROW` instruction to be replaced.
92+
93+
After passing the goto model through `remove_exceptions`, it is:
94+
95+
```
96+
com.diffblue.regression.TestExceptions.testException(int) /* java::com.diffblue.regression.TestExceptions.testException:(I)V */
97+
IF i >= 0 THEN GOTO 4
98+
struct java.lang.Exception *new_tmp0;
99+
new_tmp0 = new struct java.lang.Exception;
100+
IF !(new_tmp0 == null) THEN GOTO 1
101+
102+
...
103+
104+
1: new_tmp0 . java.lang.Exception.<init>:()V();
105+
IF @inflight_exception == null THEN GOTO 2 // it is because we've not used it yet
106+
107+
...
108+
109+
2: IF !(new_tmp0 == null) THEN GOTO 3
110+
111+
...
112+
113+
3: @inflight_exception = (void *)new_tmp0;
114+
dead new_tmp0;
115+
116+
...
117+
118+
```
119+
where now instead of the instruction `THROW`, the global variable
120+
`@inflight_exception` holds the thrown exception in ia separate goto statement.
121+
122+
\subsection Catch
123+
124+
Consider the method `catchSomething(I)V` that tries the above method `testException(I)V` and catches the exception:
125+
126+
```java
127+
public void catchSomething(int i) {
128+
try {
129+
testException(i);
130+
} catch (Exception e) {
131+
}
132+
}
133+
```
134+
135+
The goto model before `remove_exceptions` is:
136+
```
137+
com.diffblue.regression.TestExceptions.catchSomething(int) /* java::com.diffblue.regression.TestExceptions.catchSomething:(I)V */
138+
139+
...
140+
141+
CATCH-PUSH ->2
142+
143+
...
144+
145+
1: SKIP
146+
this . com.diffblue.regression.TestExceptions.testException:(I)V(i);
147+
CATCH-POP
148+
GOTO 3
149+
2: void *anonlocal::2a;
150+
struct java.lang.Exception *caught_exception_tmp0;
151+
EXCEPTION LANDING PAD (struct java.lang.Exception * caught_exception_tmp0)
152+
anonlocal::2a = (void *)caught_exception_tmp0;
153+
dead caught_exception_tmp0;
154+
dead anonlocal::2a;
155+
156+
...
157+
158+
```
159+
which contains `CATCH` instructions that are intended to be replaced.
160+
161+
After `remove_exceptions` the goto model is:
162+
163+
```
164+
com.diffblue.regression.TestExceptions.catchSomething(int) /* java::com.diffblue.regression.TestExceptions.catchSomething:(I)V */
165+
166+
...
167+
168+
this . com.diffblue.regression.TestExceptions.testException:(I)V(i);
169+
IF @inflight_exception == null THEN GOTO 3 // true if testException does not throw, method terminates normally
170+
IF !(@inflight_exception == null) THEN GOTO 1 // true if testException throws, enters catch block
171+
172+
...
173+
174+
1: __CPROVER_string class_identifier_tmp;
175+
class_identifier_tmp = ((struct java.lang.Object *)@inflight_exception)->@class_identifier;
176+
instanceof_result_tmp = class_identifier_tmp == "java::java.lang.Exception" || ... ; // TRUE
177+
dead class_identifier_tmp;
178+
2: IF instanceof_result_tmp THEN GOTO 4
179+
180+
...
181+
182+
3: ASSERT false // block 3
183+
GOTO 5
184+
4: void *anonlocal::2a; // The catch block
185+
struct java.lang.Exception *caught_exception_tmp0;
186+
ASSERT false // block 4
187+
caught_exception_tmp0 = (struct java.lang.Exception *)@inflight_exception;
188+
@inflight_exception = null;
189+
anonlocal::2a = (void *)caught_exception_tmp0;
190+
dead caught_exception_tmp0;
191+
dead anonlocal::2a;
192+
5: ASSERT false // block 5
193+
6: END_FUNCTION
194+
```
195+
where the `CATCH` instructions have been replaced with new goto statements.
45196

46197
\section java-bytecode-method-stubbing Method stubbing
47198

0 commit comments

Comments
 (0)