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

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Revision: 1764
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1764&view=rev
Author:   frankrimlinger
Date:     2009-07-16 17:37:29 +0000 (Thu, 16 Jul 2009)

Log Message:
-----------
More array rehab.  It is not necessary to create intermediate subarray objects just so they can be retrieved.  The retrieval mechanism has all the information necessary to manufacture such objects as required.  So "pushRefH" has been retired.  This impacts

AALOAD
AASTORE
ARRAYLENGTH

The new scheme also impacts valueH semantics, and works like so.  Suppose X is a class and we create x=new X[][][] and then access x[1][2][3].  This should be the default value null. First, multinewarray updates the heap:

H1 = (pusH (refH 'nH ^className ) "X[][][]" 'H)

There is also info about sublengths which we suppress.   Now we have aaload 1, which updates the opstack like so

(push (valueH (refH 'nH 1) H1) opStack )

The point is that valueH can inspect H1, discover that 'nH is a multiarray and that x[1] is not initialized, so it can just manufacture the object (array 'nH 1), so the opstack rewrites to

(push (array 'nH 1) opStack)

Now we have aaload 2, so

(push (valueH (refH (array 'nH 1) 2) H1) opStack)

Once again, valueH can dig down to 'nH, inspect H1, so we get

(push (array 'nH 1 2) opStack)

because we have the normalization (array (array obj i_1 ... i_n) i_n+1) = (array obj i_1 ... i_n+1)

Finally aaload 3 gives

(push (valueH (refH (array 'nH 1 2) 3) H1) opStack)

but this time, valueH realizes that H1 is three dimensional, and so (array 'nH 1 2 3) is uninitialized, hence we punch in the default to get

(push ^null opStack) as desired.

Observe that by putting more smarts in valueH, we make the formal semantics much more uniform, which helps out both the rewriter and ACL2 theorem prover.  Any entry in a multi-array gets a canonical home if it wants it.  

NB: the old "ptr" rulekey is now the more descriptive "array".  The old usage for "array" is obsolete and has already been retired.  valueH will get its smarts when we hit the multiarray class in mangoModelTest.  For now, we just rehab the formal semantics of the affected instructions.

Modified Paths:
--------------
    branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/Checkcast.java
    branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/Instanceof.java
    branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentPtr.java
    branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEngine.java
    branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashMangoModel.java
    branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java
    branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashRewriter.java
    branches/mango/Mango/Mango/src/mango/worker/mangoModel/agent/CheckCast_getValueAgent.java
    branches/mango/Mango/Mango/src/mango/worker/mangoModel/agent/InstanceOfAgent.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapModel.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapObjectModel.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/executable/HeapSym.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/model/TranslationManager.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/sym/TranslationSym.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/Invocation.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC_W.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java
    branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/sym/JclassSym.java

Removed Paths:
-------------
    branches/mango/Mango/Mango/src/mango/ruleAction/form/binder/PushRefH.java

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