where can I get the "typechecking verifier" specification?

[iulian dragos]

Hello all,

The title says it all: I am trying to download the specification of the new verification algorithm found in JVM 1.6. I remember I could download it as pdf some time ago, but I cannot get it anymore. Here's what I tried:

Proposed changes to the JVM - outdated. Says JSR 202 but in fact links to JSR 924, which has no downloadable content. I manually tried

JSR 202 - the download link doesn't work because 'Your download transaction cannot be approved. Contact Customer Service.'. This was the place I downloaded it last time, before Sun was bought by Oracle.

Searched all over the Oracle Java website, no success. 

Anybody can help me?

thanks,

iulian

PS. More concretely, I would like to know how the verifier checks interface calls. IIRC, the data-flow verifier allowed all interface calls to go through, even though the static type of the receiver may not implement that interface. Is it still the case?

--
« Je déteste la montagne, ça cache le paysage »
Alphonse Allais

[Rémi Forax]

A draft of version 3 of jvms was published here:
http://blogs.sun.com/abuckley/entry/draft_of_the_java_vm

see section 4.10.

Rémi

--
You received this message because you are subscribed to the Google Groups "JVM Languages" group.
To post to this group, send email to jvm-la...@googlegroups.com.
To unsubscribe from this group, send email to jvm-language...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/jvm-languages?hl=en.

[John Rose]

On Aug 30, 2010, at 3:03 AM, iulian dragos wrote:

> IIRC, the data-flow verifier allowed all interface calls to go through, even though the static type of the receiver may not implement that interface. Is it still the case?

Absolutely. It would be a major breaking change to reject receivers which do not appear to implement the interface.

In the inferencing verifier, non-implementation of a receiver cannot be proven in general, since any non-final static receiver can be extended by a subclass that implements. Only for final classes can non-implementation be proven, and this is not worth verifier complexity. The new verifier follows suit. One reason for this (Alex would know) is probably to allow old bytecodes to be retroactively provided with new verifier proofs.f

Bytecode compilers naturally produce union types at join points (SSA phi nodes) which both old and new verifiers approximate as LCA classes. This approximation discards interface information. Here's an example (based on a bug I remember we had to fix in the JVM long ago):

interface Foo { Object foo(); }
class LCA {}
class C1 extends LCA implements Foo { ... }
class C2 extends LCA implements Foo { ... }
... static Object callEither(boolean z, C1 c1, C2 c2) {
Foo foo = z ? c1 : c2; // verifier type is LCA, not Foo
return foo.foo(); // ~~ ((Foo)LCA).foo()
}

In the most common form of this code shape, the role of LCA is played by Object.

Note the ambiguity in the bytecodes between whether the variable "foo" (probably local #3) is a Foo or an LCA.

In principle, a type checking verifier could require explicitly declared interface types on locals, to capture the compiler's "intention" that the variable "foo" above is a Foo interface instead of LCA. Then invokeinterface could obtain a proof of implementation from the type checking verifier. So why not require the declaration, since the Java language does? (Iulian, your careful study of the new verifier probably raised this question for you.)

But since old bytecodes rely on the old ambiguity between Foo and LCA, there would be no way to retrofit old bytecodes to the new verifier. This is what I mean by a major breaking change. It (perhaps) would not affect bytecodes generated from Java source codes (exercise for the reader) but it would break bytecodes spun by backends which rely on the free conversion between interfaces and Object.

Note that the new JVM spec (posted by Alex) includes this comment: "For assignments, interfaces are treated like Object." The comment is borne out by the Prolog code. This is a point of compatibility with the inferencing verifier.

(At the bytecode level, interface types can for some uses double as nominal aliases for Object. E.g., the hypothetical interface Dynamic might appear in type signatures where the intentional use of the Object is as a dynamically typed reference. The JVM wouldn't care, unless you attempted to actually invoke a method on the interface.)

Bottom line: Interface call receivers in the JVM are checked at each point of call, and not by the verifier.

-- John

[iulian dragos]

Thanks a lot for the detailed explanations! 

What puzzles me is how difficult it is to get the spec of this feature. :)

iulian

--
You received this message because you are subscribed to the Google Groups "JVM Languages" group.
To post to this group, send email to jvm-la...@googlegroups.com.
To unsubscribe from this group, send email to jvm-language...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/jvm-languages?hl=en.