Add documentation on `remove-instanceof` [DOC-25] #2775

thomasspriggs · 2018-08-21T13:18:51Z

Add documentation on remove-instanceof.

krobelus · 2018-08-21T13:35:16Z

jbmc/src/java_bytecode/README.md

+```java
+Object c = new C();
+Object d = new D();
+boolean b1 = a instanceof A; // true


mixed up variables here

thk123 · 2018-08-21T13:36:40Z

jbmc/src/java_bytecode/README.md

+
+For a simple example where class `A` is derived from `Object` and no classes derrive from `A`, the expression `e instanceof A` needs to be lowered to an expression equivalent to `e == null ? false : e->@class_identifier == "A"`. The null case needs to be taken into account first, as we can't lookup the value of a `@class_identifier` field in a null pointer. Note that according to the Java specification, `null` is not an instance of any type.
+
+For an example with inheritance where class `D` is derrived from `C` and `C` is derrived from `Object`, then `e instanceof C` needs to be lowered to an expression equivalent to `e == null ? false : (e->@class_identifier == "C" || e->@class_identifier == "D")`. To lower `e instanceof C` correctly, we need to take into account each of the classes derrived from `C`. Working out what classes derive from a given class type is performed using an instance of the `class_hierarchyt` class.


Irritatingly doxygen is warning about the use of @class_identifier dunno if it is better to just use class_identifier to prevent the warning or just ignore - or see if you can fix in the doxygen settings

jeannielynnmoulton · 2018-08-21T13:42:38Z

jbmc/src/java_bytecode/README.md

+```
+Then, `x` will be set to `true` and `y` will be set to `false`.
+
+`instanceof` also works with inheritance. Given classes `C` and `D`, where `C` derrives from `Object` and `D` derives from `C`. If the following example java code is executed -


Throughout for variations, the correct spelling is "derive"

jeannielynnmoulton · 2018-08-21T13:49:05Z

jbmc/src/java_bytecode/README.md

+
+`instanceof` has its own instruction type in the java bytecode. We need to rewrite it in terms of other, more fundamental operations in order to analyse it. This operation is referred to as "lowering" or in this specific case - `remove_instanceof`.
+
+For a simple example where class `A` is derived from `Object` and no classes derrive from `A`, the expression `e instanceof A` needs to be lowered to an expression equivalent to `e == null ? false : e->@class_identifier == "A"`. The null case needs to be taken into account first, as we can't lookup the value of a `@class_identifier` field in a null pointer. Note that according to the Java specification, `null` is not an instance of any type.


In java speak, "extends" is probably preferred to "derives"

thk123 · 2018-08-21T13:44:35Z

jbmc/src/java_bytecode/README.md

@@ -43,6 +43,45 @@ To be documented.

 To be documented.

+\section java-bytecode-remove-instanceof Remove instanceof
+
+Java has an operator called `instanceof`, which is used to check if an instance of a class is of a particular type. For example given that `A` and `B` are the identifiers of classes, which derive directly from Object. If the following example java code is executed -


I think a summary of the operator is useful - but I'd probably stop short of the full inheritance example (you could exapnd your initial example to include a instanceof Object. You can instead link to this:https://docs.oracle.com/javase/tutorial/java/nutsandbolts/op2.html (irritatingly you can't link to the instanceof section)

thk123 · 2018-08-21T13:47:01Z

jbmc/src/java_bytecode/README.md

+```
+Then, `b1` will be `true`, `b2` will be `false`, `b3` will be `true` and `b4` will be `true`.
+
+`instanceof` has its own instruction type in the java bytecode. We need to rewrite it in terms of other, more fundamental operations in order to analyse it. This operation is referred to as "lowering" or in this specific case - `remove_instanceof`.


One think that I think is useful is specific Java -> Java bytecode that would be translated by this step. I'd also avoid redefining "lowering" and why it is needed since imagine you are reading about all these different transformations, you don't want to keep reading why lowering is necessary.

I also don't know, but apart from the instanceof operator, does any other Java code get translated into an instanceof (e.g. do casts? catch blocks?)

DOC-25 should also create a description of the pipeline of lowering stages.

OK I will add that overview sentence.

I have taken this overview sentence and made it into this PR: #2792

thk123 · 2018-08-21T13:48:30Z

jbmc/src/java_bytecode/README.md

+
+`instanceof` has its own instruction type in the java bytecode. We need to rewrite it in terms of other, more fundamental operations in order to analyse it. This operation is referred to as "lowering" or in this specific case - `remove_instanceof`.
+
+For a simple example where class `A` is derived from `Object` and no classes derrive from `A`, the expression `e instanceof A` needs to be lowered to an expression equivalent to `e == null ? false : e->@class_identifier == "A"`. The null case needs to be taken into account first, as we can't lookup the value of a `@class_identifier` field in a null pointer. Note that according to the Java specification, `null` is not an instance of any type.


I think docs are better when they are less wordy as quicker to get the info out (i.e. pull the Java code out into a block rather than embedding inside a sentence).

thk123 · 2018-08-21T13:48:58Z

jbmc/src/java_bytecode/README.md

+
+For a simple example where class `A` is derived from `Object` and no classes derrive from `A`, the expression `e instanceof A` needs to be lowered to an expression equivalent to `e == null ? false : e->@class_identifier == "A"`. The null case needs to be taken into account first, as we can't lookup the value of a `@class_identifier` field in a null pointer. Note that according to the Java specification, `null` is not an instance of any type.
+
+For an example with inheritance where class `D` is derrived from `C` and `C` is derrived from `Object`, then `e instanceof C` needs to be lowered to an expression equivalent to `e == null ? false : (e->@class_identifier == "C" || e->@class_identifier == "D")`. To lower `e instanceof C` correctly, we need to take into account each of the classes derrived from `C`. Working out what classes derive from a given class type is performed using an instance of the `class_hierarchyt` class.


I would do one example (the slightly more complex one) and work through that since the info in the first one is entirely contained in the second and it isn't super complex IMO.

thk123 · 2018-08-21T13:49:51Z

jbmc/src/java_bytecode/README.md

+
+For an example with inheritance where class `D` is derrived from `C` and `C` is derrived from `Object`, then `e instanceof C` needs to be lowered to an expression equivalent to `e == null ? false : (e->@class_identifier == "C" || e->@class_identifier == "D")`. To lower `e instanceof C` correctly, we need to take into account each of the classes derrived from `C`. Working out what classes derive from a given class type is performed using an instance of the `class_hierarchyt` class.
+
+In terms of the goto program, the `instanceof` operator is identified in the expression tree, based on the `exprt.id()` being `ID_java_instance_of`. The left hand side of the operator must be a pointer and the right hand side must be a type.


Too much detail here I think - try and get the fact of the java_instance_of as part of the previous worked example.

Refer to the class docs for these details.

thk123 · 2018-08-21T13:50:46Z

jbmc/src/java_bytecode/README.md

+
+In terms of the goto program, the `instanceof` operator is identified in the expression tree, based on the `exprt.id()` being `ID_java_instance_of`. The left hand side of the operator must be a pointer and the right hand side must be a type.
+
+The lowered form has a refinement to help with null pointer analysis later on. Instead of dereferencing the pointer to get @class_identifier in each comparision, it is dereferenced a single time and the result is reused. This is easier to analyse for null pointers, because there is only a single dereference to consider. So the constructed program takes the form -


This is useful but probably too in depth for an overview on the pass - I suggest pulling out of this PR and putting on the remove_instanceof doc itself.

thk123 · 2018-08-21T13:52:22Z

jbmc/src/java_bytecode/README.md

@@ -43,6 +43,45 @@ To be documented.

 To be documented.

+\section java-bytecode-remove-instanceof Remove instanceof
+
+Java has an operator called `instanceof`, which is used to check if an instance of a class is of a particular type. For example given that `A` and `B` are the identifiers of classes, which derive directly from Object. If the following example java code is executed -


Lead with a one sentence summary of the whole thing before going into detail about the instanceof operator. I.e.

\ref remove_instanceof.h removes the bytecode instruction `instanceof ` and replaces it with two instructions: - check whether the pointer is null - if not null, does the class identifier match the type of any of its subtypes

peterschrammel · 2018-08-21T14:17:52Z

jbmc/src/java_bytecode/README.md

@@ -43,6 +43,45 @@ To be documented.

 To be documented.

+\section java-bytecode-remove-instanceof Remove instanceof
+
+Java has an operator called `instanceof`, which is used to check if an instance of a class is of a particular type. For example given that `A` and `B` are the identifiers of classes, which derive directly from Object. If the following example java code is executed -


Link the source file resp. class at the beginning

peterschrammel · 2018-08-21T14:19:46Z

jbmc/src/java_bytecode/README.md

+```
+Then, `b1` will be `true`, `b2` will be `false`, `b3` will be `true` and `b4` will be `true`.
+
+`instanceof` has its own instruction type in the java bytecode. We need to rewrite it in terms of other, more fundamental operations in order to analyse it. This operation is referred to as "lowering" or in this specific case - `remove_instanceof`.


DOC-25 should also create a description of the pipeline of lowering stages.

peterschrammel · 2018-08-21T14:20:33Z

jbmc/src/java_bytecode/README.md

+
+For an example with inheritance where class `D` is derrived from `C` and `C` is derrived from `Object`, then `e instanceof C` needs to be lowered to an expression equivalent to `e == null ? false : (e->@class_identifier == "C" || e->@class_identifier == "D")`. To lower `e instanceof C` correctly, we need to take into account each of the classes derrived from `C`. Working out what classes derive from a given class type is performed using an instance of the `class_hierarchyt` class.
+
+In terms of the goto program, the `instanceof` operator is identified in the expression tree, based on the `exprt.id()` being `ID_java_instance_of`. The left hand side of the operator must be a pointer and the right hand side must be a type.


Refer to the class docs for these details.

thk123 · 2018-09-27T10:54:47Z

jbmc/src/java_bytecode/remove_instanceof.h

+/// must be a type.
+///
+/// The lowered form has a refinement to help with null pointer analysis later
+/// on. Instead of dereferencing the pointer to get @class_identifier in each


doxygen is complaining about the @ here looks like you can use \@

allredj

Passed Diffblue compatibility checks (cbmc commit: b2b7dc3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86282968

thomasspriggs · 2018-09-28T16:04:43Z

@jeannielynnmoulton Re-review?

thomasspriggs requested review from cesaro, cristina-david, mgudemann, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners August 21, 2018 13:18

krobelus reviewed Aug 21, 2018

View reviewed changes

thk123 reviewed Aug 21, 2018

View reviewed changes

jeannielynnmoulton reviewed Aug 21, 2018

View reviewed changes

thk123 reviewed Aug 21, 2018

View reviewed changes

peterschrammel added the documentation label Aug 21, 2018

peterschrammel reviewed Aug 21, 2018

View reviewed changes

peterschrammel assigned NathanJPhillips and thomasspriggs Aug 21, 2018

thk123 mentioned this pull request Aug 21, 2018

Add an overview of what lowerings are done [DOC-25] #2792

Merged

thk123 changed the title ~~Add documentation on remove-instanceof~~ Add documentation on remove-instanceof [DOC-25] Sep 6, 2018

thomasspriggs force-pushed the tas/doc_remove_instanceof branch 2 times, most recently from ddb2086 to b68f550 Compare September 26, 2018 14:54

thk123 approved these changes Sep 27, 2018

View reviewed changes

thk123 reviewed Sep 27, 2018

View reviewed changes

tautschnig unassigned NathanJPhillips Sep 27, 2018

Add documentation on remove-instanceof

b2b7dc3

thomasspriggs force-pushed the tas/doc_remove_instanceof branch from b68f550 to b2b7dc3 Compare September 28, 2018 11:11

allredj reviewed Sep 28, 2018

View reviewed changes

tautschnig assigned jeannielynnmoulton and unassigned thomasspriggs Sep 28, 2018

jeannielynnmoulton approved these changes Oct 2, 2018

View reviewed changes

thk123 merged commit 5c62ca9 into diffblue:develop Oct 2, 2018

thk123 deleted the tas/doc_remove_instanceof branch October 2, 2018 10:02


		For a simple example where class `A` is derived from `Object` and no classes derrive from `A`, the expression `e instanceof A` needs to be lowered to an expression equivalent to `e == null ? false : e->@class_identifier == "A"`. The null case needs to be taken into account first, as we can't lookup the value of a `@class_identifier` field in a null pointer. Note that according to the Java specification, `null` is not an instance of any type.

		For an example with inheritance where class `D` is derrived from `C` and `C` is derrived from `Object`, then `e instanceof C` needs to be lowered to an expression equivalent to `e == null ? false : (e->@class_identifier == "C" \|\| e->@class_identifier == "D")`. To lower `e instanceof C` correctly, we need to take into account each of the classes derrived from `C`. Working out what classes derive from a given class type is performed using an instance of the `class_hierarchyt` class.


		`instanceof` has its own instruction type in the java bytecode. We need to rewrite it in terms of other, more fundamental operations in order to analyse it. This operation is referred to as "lowering" or in this specific case - `remove_instanceof`.

		For a simple example where class `A` is derived from `Object` and no classes derrive from `A`, the expression `e instanceof A` needs to be lowered to an expression equivalent to `e == null ? false : e->@class_identifier == "A"`. The null case needs to be taken into account first, as we can't lookup the value of a `@class_identifier` field in a null pointer. Note that according to the Java specification, `null` is not an instance of any type.


		For an example with inheritance where class `D` is derrived from `C` and `C` is derrived from `Object`, then `e instanceof C` needs to be lowered to an expression equivalent to `e == null ? false : (e->@class_identifier == "C" \|\| e->@class_identifier == "D")`. To lower `e instanceof C` correctly, we need to take into account each of the classes derrived from `C`. Working out what classes derive from a given class type is performed using an instance of the `class_hierarchyt` class.

		In terms of the goto program, the `instanceof` operator is identified in the expression tree, based on the `exprt.id()` being `ID_java_instance_of`. The left hand side of the operator must be a pointer and the right hand side must be a type.


		In terms of the goto program, the `instanceof` operator is identified in the expression tree, based on the `exprt.id()` being `ID_java_instance_of`. The left hand side of the operator must be a pointer and the right hand side must be a type.

		The lowered form has a refinement to help with null pointer analysis later on. Instead of dereferencing the pointer to get @class_identifier in each comparision, it is dereferenced a single time and the result is reused. This is easier to analyse for null pointers, because there is only a single dereference to consider. So the constructed program takes the form -

Add documentation on remove-instanceof [DOC-25] #2775

Add documentation on remove-instanceof [DOC-25] #2775

Uh oh!

Conversation

thomasspriggs commented Aug 21, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

thomasspriggs commented Sep 28, 2018

Uh oh!

Uh oh!

Add documentation on `remove-instanceof` [DOC-25] #2775

Add documentation on `remove-instanceof` [DOC-25] #2775