Java Bytecode - Revision history

C-Otto at 11:21, 31 January 2013

2013-01-31T11:21:18Z

2013-01-28T09:43:09Z

Considered Types

2011-03-28T12:28:28Z

(forbidden native method) Undo revision 1138 by C-Otto (talk)

2011-03-28T12:27:20Z

2009-12-22T10:01:58Z

2009-12-21T14:52:45Z

2009-12-21T14:51:30Z

Participants

2009-12-21T14:50:10Z

2009-12-21T14:48:32Z

2009-12-21T14:40:37Z

@@ Line 46: / Line 46: @@
 == Details ==
 === Errors and Exceptions ===
 In most cases, an instance of '''java.lang.Error''' thrown by the JVM is undesired behaviour.
@@ Line 158: / Line 161: @@
 * The opcodes '''LDC (0x12)''' and '''LDC_W (0x13)''' are not allowed in the variants that return a '''String''' or '''Class''' instance. These variants are problematic, because they may return some already known instance.
-* The opcode '''INVOKEDYNAMIC (0xBA)''' is not part of the instruction set, yet, so it is not allowed.
+* The opcode '''INVOKEDYNAMIC (0xBA)''' is not part of the instruction set of Java 6, so it is not allowed.
 * The opcodes '''MONITORENTER (0xC2)''' and '''MONITOREXIT (0xC3)''' only make sense when using multithreading. Furthermore, correct handling of '''MONITOREXIT''' is more involved. As a result, these two opcodes are not allowed.
 * The reserved opcodes '''BREAKPOINT (0xCA)''', '''IMPDEP1 (0xFE)''', '''IMPDEP2 (0xFF)''' are not allowed.

@@ Line 55: / Line 55: @@
 The list of considered classes can be extended in the future to allow for more advanced examples, e.g. involving '''System.out.println(...)''' and other "library" code.
-All additional class files are taken from the current Debian version of
+All additional class files are taken from a Debian version of
 OpenJDK [1].

@@ Line 29: / Line 29: @@
 Analysis starts with '''public static void main(String[] args)'''. This method is specified in the .jar file by adding a file '''META-INF/MANIFEST.MF''' including a line '''Main-Class: some/package/SomeClass'''. Note that it is unclear whether the standard is slashed or dotted notation, so it may be a good idea to accept both.
-Using constructs like '''(new Object()).hashCode()''' or '''args.length''' or '''args[i].length()''' one gets unknown (for the last two options: non-negative) '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.
+Using constructs like '''args.length''' or '''args[i].length()''' one gets unknown non-negative '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.
   public static void main(String[] args) {

@@ Line 29: / Line 29: @@
 Analysis starts with '''public static void main(String[] args)'''. This method is specified in the .jar file by adding a file '''META-INF/MANIFEST.MF''' including a line '''Main-Class: some/package/SomeClass'''. Note that it is unclear whether the standard is slashed or dotted notation, so it may be a good idea to accept both.
-Using constructs like '''args.length''' or '''args[i].length()''' one gets unknown non-negative '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.
+Using constructs like '''(new Object()).hashCode()''' or '''args.length''' or '''args[i].length()''' one gets unknown (for the last two options: non-negative) '''int''' values and can use these to create a large number of problem instances. As an example, the following code can be used to construct problems where termination of some algorithm working on lists of arbitrary length should be proved.
   public static void main(String[] args) {

@@ Line 41: / Line 41: @@
 == Participants ==
 In the 2009 competition the tools
-[http://julia.scienze.univr.it:8080/julia/ Julia],
+[[Tools:Julia|Julia]],
 [http://costa.ls.fi.upm.es/costa/costa.php COSTA] and
 [[Tools:AProVE|AProVE]] took part in the JBC categories.

@@ Line 173: / Line 173: @@
 === Categories ===
-We propose to have two categories of Java Bytecode problems. One category
+The JBC problems are divided into two categories.
-contains programs with recursion and one only contains programs without
+One category contains all examples that make use of recursion, whereas all examples in the other category do not use recursion at all.
 recursion. The reason is that recursion poses a special problem for the
 analysis since one has to handle the call stack properly. We think that
 it is interesting to evaluate the performance of termination analyzers

@@ Line 11: / Line 11: @@
 As discussed in the steering committee, the compilation of a JBC problem based on given Java code is done manually, so the existing tools do not have to implement or use a Java compiler.
-There are languages different from Java that compile to JBC (e.g. Python/Jython, Ruby/JRuby, Scala, ...). The JBC category can be filled with corresponding problems.
+There are languages different from Java that compile to JBC (e.g. Python/Jython, Ruby/JRuby, Scala, ...).
 == Problem definition ==
 A JBC problem is defined by up to three parts.
 * byte code
-* Java source
+* source
 * start method
@@ Line 22: / Line 24: @@
 Providing the code is straightforward and is accomplished using a [http://en.wikipedia.org/wiki/JAR_(file_format) .jar file] that contains all .class files needed for the analysis.
 === Java Source ===
-This part is optional. If the Java source for the compiled program is available, the corresponding source files are packed into a file '''source.zip''' which is then stored in the .jar file.
+This part is optional. If the source for the compiled program is available, the corresponding source files are packed into a file '''source.zip''' which is then stored in the .jar file.
 === Start Method ===

← Older revision		Revision as of 14:40, 21 December 2009
Line 178:		Line 178:
	All input problems must pass the bytecode verification process. Therefore,		All input problems must pass the bytecode verification process. Therefore,
	the analyzers do not need to verify the given bytecode.		the analyzers do not need to verify the given bytecode.
		+
		+	[[Category:Categories]]