[Prev][Next][Index][Thread]

Re: Type soundness issues in Java

"Sophia Drossopoulou(Osp. Dezani)" wrote:

> I would like first to (probably needlessly) clarify that the example
> has nothing to do with binary compatibility, since removal of an
> interface is not listed as a binary compatible change in the spec. The
> example only has to to with the loader and verifier.

Here is my understanding:

(1) In Martin's example, it is not necessary to load "interface I" to
detect that the assignment i=a (PC 42 and 43 in the bytecode provided
by Ole) is ill-typed. The information that "class A" does not
implement "interface I" is already available within the declaration of
A and thus nothing else needs to be loaded.  However, the loaders need
to be called in the type inference if "class A" indirectly implements
"interface I" (say "class A" implements "interface J", and "interface
J" extends "interface I"). In this case, a BC verifier may need to
load "interface J", in order to check whether "class A" implements
"interface I".

(2) As Phillip pointed out, the observed behavior in Martin's example
is because interface types are not checked in verifier but at run time
in the current Sun's implementation. However, this implementation has
not been explicitly required by Sun's specs. Another implementation
may choose to do the verification in a less lazy way.  Actually, the
VM Spec explicitly says that verifier may cause addtional interfaces
to be loaded (think the above case of indirection implementation.)

> Secondly, this example raised (in discussion with Mariangiola
> Dezani-Ciancaglini) the following question:
>
> Obviously, and because of the laziness allowed in verification and
> loading, different Java implementations may behave differently, and
> some will throw exceptions where others might not. So, what about the
> claim that Java will have the same behaviour across all platforms?

(3) Java and JVM Specs seem to have tried hard to ensure that although
different strategies may be used in different implementations,
"Throwable" objects can only thrown at the time as though one standard
strategy is used, or different strategies throw the same type of
"Throwable" objects. (Of course the question remains open whether the
specs have really succeeded in doing so.)

> Could we replace the above claim by the following, weaker one?
>
>    Let us consider an eager implementation EI (eager loading and verification).
>    Then,  every program that executes on EI without throwing an unchecked
>    exception should have the same behaviour on every other implementation.
>    On the other hand, a program that throws an unchecked exception on some
>    implementation will also throw an unchecked exception (although not
>    necessarily the same one) on EI.

> (Of course I am ignoring here the issue of different package
> implementations across platforms).
>
> The applicability of the above claim would be severy reduced by the
> fact that we can handle exceptions in Java. Therefore, the behaviour
> of a program that throws an unchecked exception AND handles it cannot
> be compared to the behaviour of the same program on EI. The two
> implementations could even return different values, or one could
> terminate abnormaly and the other could handle the exception and
> terminate abnormally.

(4) Java and JVM Specs seem to require that all "Throwable" objects
that may be thrown by JVM, BC verifier and class loaders are "Error"
objects, not "Exception" objects ("Error" and "Exception" are
subclasses of "Throwable"). Even if loaders may be user-defined Java
programs and may throw "Exception" objects, the JVM will translate
these "Exception" objects into "Error" objects. "Error" objects need
not be cought by Java programs. (Of course, this does not prevent the
user from writing Java programs to catch "Error" objects.)

Cheers,

Zhenyu