Add an overview of what lowerings are done [DOC-25] #2792
Conversation
thk123
requested review from
cesaro,
cristina-david,
mgudemann,
NathanJPhillips,
peterschrammel,
pkesseli and
smowton
as code owners
jbmc/src/java_bytecode/README.md
Outdated
| @@ -6,6 +6,21 @@ This module provides a front end for Java. | |||
| \section java-bytecode-conversion-section Overview of conversion from bytecode to codet | |||
|
|
|||
| To be documented. | |||
| \subsection java-bytecode-lowering-to-goto Lowering to GOTO | |||
|
|
|||
| The Java language contains high level programming concepts like virtual functions and throw/catch semantics. We need to rewrite these in terms of other, more fundamental operations in order to analyse it. This operation is referred to as "lowering". | |||
jbmc/src/java_bytecode/README.md
Outdated
|
|
||
| The Java language contains high level programming concepts like virtual functions and throw/catch semantics. We need to rewrite these in terms of other, more fundamental operations in order to analyse it. This operation is referred to as "lowering". | ||
|
|
||
| The following lowering operations are done on java bytecode after converting into a basic codet representation. |
jbmc/src/java_bytecode/README.md
Outdated
|
|
||
| The following lowering operations are done on java bytecode after converting into a basic codet representation. | ||
|
|
||
| - \ref java-bytecode-runtime-exceptions "Add runtime exceptions" |
There was a problem hiding this comment.
This is not a lowering in the strict sense. It is adding part of the JVM's execution algorithm into the analysed program.
There was a problem hiding this comment.
We should also mention remove_nondet then.
There was a problem hiding this comment.
Hmm - I consider it in the same bucket since the JVM detects null pointer access and throws an exception - we lower that "high level feature" of the JVM into a fundamental operation of if(a == null), what would you call it?
Remove_nondet is kind of a weird one since it doesn't exist in Java bytecode or the JVM - it is a CPROVER construct right?
There was a problem hiding this comment.
I think we should carefully distinguish between lowering and instrumentation. The former is a rewrite of the code (supposedly semantics-preserving), while the latter will add or modify behaviour.
jbmc/src/java_bytecode/README.md
Outdated
| - \ref java-bytecode-runtime-exceptions "Add runtime exceptions" | ||
| - \ref java-bytecode-remove-java-new "Remove new calls" | ||
| - \ref java-bytecode-remove-exceptions "Remove thrown exceptions" | ||
| - As well as other non-java specific transformations (see \ref goto-programs for details on these) |
There was a problem hiding this comment.
There is remove_instanceof and remove_virtual_methods
There was a problem hiding this comment.
remove-virtual-methods is not Java specific (covered by the link to goto-programs). The section for remove_instanceof is missing so will add after #2775 is merged.
jbmc/src/java_bytecode/README.md
Outdated
| These are performed in `process_goto_function` for example | ||
| \ref jbmc_parse_optionst::process_goto_function | ||
|
|
||
| Once these lowerings have been completed, you have a GOTO model that can be analysed. |
There was a problem hiding this comment.
analysed: maybe be more specific 'handled by \ref goto-symex'. Also the lowering passes do some kind of 'analysis'.
|
@peterschrammel some comments addressed - I have questions about the others. |
|
@cesaro Hi - sorry is there an action you want me to take from your comment? Perhaps a link to this section: https://github.com/diffblue/cbmc/pull/2806/files#diff-6988ca396abc0c4e424da9d8494e2f1fR814 from the word lowering. If I do that, would you be happy to approve? |
jbmc/src/java_bytecode/README.md
Outdated
| The following lowering operations are done on Java bytecode after converting into a basic `codet` representation. | ||
|
|
||
| - \ref java-bytecode-runtime-exceptions "Add runtime exceptions" | ||
| - \ref java-bytecode-remove-java-new "Remove new calls" |
jbmc/src/java_bytecode/README.md
Outdated
| - \ref java-bytecode-remove-java-new "Remove new calls" | ||
| - \ref java-bytecode-remove-exceptions "Remove thrown exceptions" | ||
| - \ref java-bytecode-remove-instance-of | ||
| - As well as other non-java specific transformations (see \ref goto-programs for details on these) |
|
Done, will wait until I've merged the other (colliding) doc change to avoid spamming Travis #2773 |
|
@thk123 Yes, good to merge with just a reference to the background concepts. Since this will probably be merged before #2806 you can just a reference to the section Background Concepts in plain English when you explain what a lowering are and we will create the link from here in #2806 to the specific term in the Glossary subsection. |
thk123
force-pushed
the
thk/lowerings-overview
branch
from
58b41bf to
31963a3
Compare
As expressed on #2775 we should have one place that explains what is meant by lowering in a holistic sense, with links to the new sections.