RE: Type soundness issues in Java

I thought about this a little more, and while I think the principles I
described are more or less right, I'm not sure about the details.  For
example, verification should have loaded I.class to verify the field access
"i.c".  Similarly, it looks like it's the loading of class I that causes the
final failure, but you would have thought the binary compatibility checks
would have failed when class A was loaded in line 1 of main().  If not, it
may be that the assumption tracking in the loader/verifier a messy business
indeed, which may leave plenty of room for implementation bugs...  

So perhaps the story could be cleaner, and a formalization or model
implementation might help with this!


-----Original Message-----
From: Don Syme 
Sent: 17 May 1999 20:47
To: 'Kim Bruce'; types@cis.upenn.edu; Martin.Buechi@abo.fi
Subject: RE: Type soundness issues in Java

Exactly when a IncompatibleClassChange error should be raised is not
explicitly defined in the Java language defn, just as it's not defined when
VerificationFailure exceptions should be raised.  There's a minimum, of
course: they should be raised before anything evil happens, e.g. before any
functionality is accessed in a non-compatible class or before a method's
code (or basic block) is executed.  Generally Java implementations will
delay the loading of a class or interface until the very last minute: in
your example I believe I.class has not even been loaded until the last line.

This means such errors may be detected much later than you might think, and
so the definition of type soundness is indeed much looser than a theorist
may like, precisely because the type environment is only "partially filled
in".  Even when I have a class such as A, the hierarchy above A may not have
been loaded, if there was no reason to do so!  Similarly, verification
happens very lazily, e,g, a method is verified just before it is called.

You could certainly formalize all this, e.g. start with an operational
description of verification and execution that involves only partly
constructed type environments.  You kind of need this for dynamic linking
anyway.  It's not enormously interesting, because in a sense the implementor
is just doing the natural thing and made all binding resolutions happen as
late as possible.

You might have also wondered why verification does not fail on the second
attempt to run Main, since the assignment no longer appears valid
(verification succeeds, at least using Microsoft's jvc and jview with the /v
flag).  I believe this is because operationally the verifier has also never
needed to load I.class, i.e. verification succeeds with respect to any
_valid_ I.class.  In a sense the requirement to check this assumption (that
I is valid, i.e. binary compatible) is propogated forward and ultimately
checked when a real I.class is loaded, and an error is raised.  

Ultimately, after the assignment we have the rather strange situation of
having a value of type "I", but without knowing what "I" means (i.e. never
of having actually loaded the .class file that defines interface "I"), and
indeed not knowing yet if type I makes any sense at all!  I guess you could
call it faith....

Finally, it may even be that the compilers are optimizing "i" away
completely, so you really should look at the .class files as well.

At the lab:                                     At home:
Microsoft Research Cambridge                    11 John St
St George House                                 CB1 1DT
Cambridge, CB2 3NH, UK
Ph: +44 (0) 1223 744797                         Ph: +44 (0) 1223 722244
email: dsyme@microsoft.com
   "Knowledge, the beginning of it is bitter to taste, 
       but the end is sweeter than honey." 
                                           --  11C Samarkand proverb

> Date: Sun, 16 May 1999 14:02:03 +0300
> To: types@cis.upenn.edu
> From: Martin Buechi <Martin.Buechi@abo.fi>
> Subject: Type soundness issues in Java
> 1.Failure of type soundness in combination with binary compatibility
> --------------------------------------------------------------------
> I have stumbled over what I consider to be a failure of type soundness in
> Java. The problem is exposed in combination with binary compatibility.
> However, since Java even defines an exception for this case, I am
> how type soundness is really defined in Java. Or is this just an
> implementation error, that is present in all JVM's that I have tested?
> Here goes the example:
> -- I.java
> interface I {
> 	int c=4;
> 	void m();
> }
> -- A.java
> public class A implements I { // "implements I" commented out for 
> 	public void m() {
> 		System.out.println("m");
> 	}
> }
> -- Main.java
> public class Main {
> 	public static void main(String args[]) {
> 		A a = new A();
> 		I i;
> 		System.out.println("I've been started");
> 		if(a instanceof I)
> 			System.out.println("a is instance of I!");
> 		else
> 			System.out.println("a Is NOT instance of I");
> 		i=a;
> 		System.out.println("Cast succeeded!");
> 		System.out.println(java.lang.Integer.toString(i.c,10));
> 		i.m();
> 	}
> }
> --
> I have tested this under JDK 1.2 on Solaris 2.6 (as well as JDK 1.1.7 on
> Solaris and under Netscape 4.07 and on the Mac MRJ 2.0):
> First we compile everything:
> % /opt/jdk_1.2/bin/javac Main.java
> Then we comment out "implements I" in A.java, save it, and recompile only
> A.java.
> % /opt/jdk_1.2/bin/javac A.java
> Then we run it.
> % /opt/jdk_1.2/bin/java Main
> I've been started
> a Is NOT instance of I
> Cast succeeded!
> 4
> Exception in thread "main" java.lang.IncompatibleClassChangeError: class A

> not implement interface I
>         at Main.main(Compiled Code)
> --

> 2. Practical undermining of type soundness by "bad" programming practice
> ------------------------------------------------------------------------
> The second issue concerns the advocated programming style of the Java
> Collections Framework  (JCF)
> "All of the modification methods in the collection interfaces are labeled
> optional. Some implementations may not perform one or more of these
> operations, throwing a runtime exception (UnsupportedOperationException)
> they are attempted. Implementations must specify in their documentation
> which optional operations they support. Several terms are introduced to
> in this specification."
> What is the difference from the client's perspective between an object
> explicitly throwing a UnsupportedOperationException as advocated in JCF
> an automatically generated "no such method" in an untyped/not type sound
> language?
> (UnsupportedOperationException being a subclass of
> java.lang.RuntimeException, methods are not even required to declare in
> their throws clause that this type of exceptions might be thrown during
> execution of the methods but not caught. Anyhow, I am not sure if it would
> make a big practical difference if UnsupportedOperationException would
> to be listed in the throws clause.)
> I don't believe too much in the "Implementations must specify in their
> documentation which optional operations they support" either because the
> documentation is not fed to the compiler and, therefore, easily ignored.
> In a strongly type language with by-name equivalence for types, I would
> like to use types to stand for explicit external specifications
> typing). If we introduce UnsupportedOperationException's we have to reduce
> the specifications to "does the desired thing or throws an exception",
> where the "or" stands for a demonic choice. Hence, no meaningful
> can be proved anymore. Therefore, I personally believe that the much
> acclaimed JCF sets a bad example by promoting the practical undermining of
> type soundness.
> I think that the solution to the JCF design problem would be to introduce
> many smaller interfaces (e.g. CollectionWithoutModification,
> CollectionRemove) grouping related methods, that are likely to be fully or
> not at all implemented,that are then combined. Of course, I would advocate
> compound types (Martin Büchi and Wolfgang Weck. Compound Types for Java.
> Proceedings of OOPSLA'98. Pages 362-373. ACM Press, 1998 [End of own paper
> ad :)]) or a similar mechanism to avoid cluttering the name space with all
> the combinations required because of strict by-name type equivalence.
> Yours,
> Martin
> ====================================================================
> Abo Akademi University          | mailto:Martin.Buechi@abo.fi
> Department of Computer Science  | phone: +358 (0)2 215-4034
> Lemminkaisenkatu 14a            | fax:   +358 (0)2 215-4732
> 20520  Turku                    | www:   http://www.abo.fi/~mbuechi/
> FINLAND                         | time:  UTC +0300
> --------------------------------------------------------------------
> Make something idiot proof, and someone will build a better idiot.
> ====================================================================