[Javapathfinder-svn] SF.net SVN: javapathfinder:[1843] branches/mango/Mango

[<fra...@us...>]

Revision: 1843
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1843&view=rev
Author:   frankrimlinger
Date:     2009-08-20 22:49:31 +0000 (Thu, 20 Aug 2009)

Log Message:
-----------
checkcast rehab in progress.  Requires the "mango theory of types".

jpf likes to deliver "canonical type" in instructions like checkcast.  The issue for mango is, does canonical type contain all the information required to translate to "source code level format".  And the answer is yes.   The algorithm is simple.  Say x is in canonical type.

If x does not contain "[", then x is source code level.  If x does contain "[", then Types.getTypeName(x) will be source code level.  End of story.

Examples:

int  --> int
I     --> I
[I   --> int[]
[LI; --> I[]

At the source code level, the names of types, classes, and arrays all blur together in a uniform syntax  

identifier[] ...[]

where the bracket(s) are optional. Strings satisfying this syntax are referred by mango as "class names". We stretch the identifier concept to allow for <xxx>.    This allows <init>, <clinit>, and the mango formal types to join the club.  So questions like, given a class name x, is x primitive?, is x an array?, is x a non-array class?, is x mango formal? are all meaningful and can be answered deterministically by parsing the name.  This unravels the mystery connection between "int" and "java.lang.Integer.TYPE".  These are different class names, one representing a primitive java type, and one representing a non-array class.

We definitely DO NOT use mango class names to directly represent field descriptors (JVM2ed 4.3.2).  The reason is that field descriptors for Object type and Array type do not even satisfy the syntax of mango class name.  Worse, the field descriptor "I" has the semantics of the class name "int", NOT the class name "I".  And most horribly, field descriptors use "internal form", i.e., "/" instead of "."  Ditto for method descriptors.  Nevertheless, all descriptors have a natural translation

I --> int
LI; --> I
V --> void


and so on.

So, canonical type is a good thing, but we stick with source code level "class names", because they faithfully represent all the semantics, and are pleasing to the eye.  Moreover, the mango theory of types may be admitted to ACL2, and allows us to distinguish all the exotica placed in the heap, using class names in the subaddress  of a location.  This is critical for garbage collection.

Modified Paths:
--------------
    branches/mango/Mango/Mango/src/mango/worker/Worker.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.