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

SourceForge Headquarters 225 Broadway Suite 1600 San Diego, CA 92101 +1 (858) 422-6466

Revision: 1864
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1864&view=rev
Author:   frankrimlinger
Date:     2009-08-28 19:59:39 +0000 (Fri, 28 Aug 2009)

Log Message:
-----------
Realized that most of the MangoFormal aliasing the system source code is very harmful and very unnecessary.  At some point, lost sight of the design goal of aliasing, which is simply to allow the class loader to admit both the real and the aliased system classes.  The burden on Mango is then to ensure that all formal analysis is done using the aliased class methods, not the real ones.

Therefore, the only thing that needs to be aliased within the source code are
1) the actual name of the class within the class declaration, and to the extent there are package visibility issues,  the names of the extended classes
2) final methods that cannot be overloaded, 
3) constructor method names, which of course must be the same as the aliased class name,
4) anything else I can't think of right now.

TODO eliminating all method name, field name, and signature aliasing in the system source code.  The only final method that gets the treatment is getClass_MangoFormal().  START WITH Double_MangoFormal.

TODO:  Simplify MangoMethodPeer, which is supposed to produced the aliased methods.  Signature aliasing is no longer necessary.  It is only necessary to alias getClass to getClass_MangoFormal.  Since the JVM patches in the constructors, they are not an issue.  End of story.

Completed native implementation of Object_MangoFormal.  Created new class mango.lang.reflect.Mango_Array for native array accessors.  Created mango.io.Mango_PrintStream to provide native buffer support.

Complete rewrite of Array_MangoFormal to use new native accessors.

Another issue has to do with "this".  If you are going to pass "this" to another method, you might have to wrap with a native method like so

XXX formal2nominal(XXX_MangoFormal obj){}

The native implementation just returns obj, but the declaration at the source code level is enough to fake out the compiler.  Probably this issue is what started the signature aliasing business, but clearly the new solution is bfc.

Put all the required formal2nominal methods in the native support class mango.lang.Mango_Object

NB: Of course it is ok for native support to have _MangoFormal in signatures if this helps avoid formal2nominal wrappers.  

Final thought: you could always write your own class loader, but it would have to be integrated into jpf core and it really does not belong there.

Modified Paths:
--------------
    branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/MakeClass.java
    branches/mango/Mango/Mango/src/mango/worker/Worker.java
    branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hash.java
    branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/CompositionImplication.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/StableImplication.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/TemplateImplication.java
    branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
    branches/mango/Mango/mangoUserHome/system/System/java/io/FileOutputStream_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/io/FilterOutputStream_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/io/InputStream_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/io/ObjectStreamClass_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/io/OutputStream_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/io/PrintStream_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/lang/Boolean_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/lang/Byte_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/lang/CharSequence_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/lang/Character_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/lang/ClassCastException_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/lang/Class_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/lang/Double_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/lang/Object_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/java/lang/reflect/Array_MangoFormal.java
    branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Byte.java
    branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Class.java

Added Paths:
-----------
    branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/HashCode.java
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal()Ljava.lang.Class_MangoFormal;/
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal()Ljava.lang.Class_MangoFormal;/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal([Ljava.lang.Object_MangoFormal;)Ljava.lang.Class_MangoFormal;/
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal([Ljava.lang.Object_MangoFormal;)Ljava.lang.Class_MangoFormal;/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/mango/
    branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/
    branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/
    branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/
    branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/<init>()V/
    branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/<init>()V/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getLength(Ljava.lang.Object_MangoFormal;)I/
    branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getLength(Ljava.lang.Object_MangoFormal;)I/Final case.zip
    branches/mango/Mango/mangoUserHome/system/System/mango/io/
    branches/mango/Mango/mangoUserHome/system/System/mango/io/Mango_PrintStream.java
    branches/mango/Mango/mangoUserHome/system/System/mango/lang/reflect/
    branches/mango/Mango/mangoUserHome/system/System/mango/lang/reflect/Mango_Array.java

Removed Paths:
-------------
    branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Boolean.java
    branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Object.java

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