From 38e9801a44e9c348e6c87ba159d2e5be1a482a16 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 21 Aug 2018 16:43:54 +0100 Subject: [PATCH 1/2] Add an overview of what lowerings are done --- jbmc/src/java_bytecode/README.md | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/jbmc/src/java_bytecode/README.md b/jbmc/src/java_bytecode/README.md index 0537bf3f185..7deecee31b9 100644 --- a/jbmc/src/java_bytecode/README.md +++ b/jbmc/src/java_bytecode/README.md @@ -6,6 +6,27 @@ 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. These need to be rewritten in terms of +other, more fundamental operations in order to analyse the Java program. This +operation is referred to as "lowering". + +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" +- \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) + +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 handled by \ref goto-symex. \section java-bytecode-array-representation How are Java arrays represented in GOTO From 31963a349d11ed3d5bb976319271a0f274b9affc Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 30 Aug 2018 11:50:57 +0100 Subject: [PATCH 2/2] Add tempoary reference to background concepts To be replaced by diffblue/cbmc#2806 --- jbmc/src/java_bytecode/README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/README.md b/jbmc/src/java_bytecode/README.md index 7deecee31b9..314aac0c256 100644 --- a/jbmc/src/java_bytecode/README.md +++ b/jbmc/src/java_bytecode/README.md @@ -11,7 +11,8 @@ To be documented. The Java language contains high-level programming concepts like virtual functions and throw/catch semantics. These need to be rewritten in terms of other, more fundamental operations in order to analyse the Java program. This -operation is referred to as "lowering". +operation is referred to as "lowering". See Background Concepts for more +information. The following lowering operations are done on Java bytecode after converting into a basic `codet` representation.