Menu
▾
▴
[Javapathfinder-svn] SF.net SVN: javapathfinder:[1551] branches/mango/MangoJPF
|
From: <fra...@us...> - 2009-05-25 18:47:25
|
Revision: 1551
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1551&view=rev
Author: frankrimlinger
Date: 2009-05-25 18:47:13 +0000 (Mon, 25 May 2009)
Log Message:
-----------
javapathfinder-mango-bridge port is now complete. The plan is now to get phase1 working on itsAWrap, and then hot-wire the target method to itsAWrap.clear() and abstract this method. Once this is working, punch in the target select algorithm and port the rest of the baseline tests to MangoJPF. At this point, throw out the Mango project, and rename MangoJPF to Mango. Then copy to MangoBaseline and forge ahead into terra incognita.
The goals for the project are
1. Eliminate stratification from phase2.
2. Add a REWRITER phase to the scanner bytecodes, so that they can be used for rewriting. To greatly reduce load and complexity on the rewriter, DO NOT bind context prior to rewriting. Since the results will be deployed as jpf state-along-a-path, context can be bound after composition occurs. Note this will not completely eliminate rewriting with context, as certain things, in particular garbage collection, require context to perform address comparisons. But the horrible issue of "context resolution" which occurs during composition can be eliminated.
3. Drive the rewriter automatically along the paths, stopping only when translation fails and the user must add new definitions. Store traversed path for each case in the rulebase so jpf can restart cold.
4. And finally, with all this in place, it will be possible to use the backtracking mechanism to produce factorizations for invariant detection. These factorizations should be baked into the cake from step two onward and stored persistently, even as they are now in a very limited and clumsy way.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHash.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ReturnPointLink.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ICONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOOKUPSWITCH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITORENTER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITOREXIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NOP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RUNSTART.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SWAP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/TABLESWITCH.java
Removed Paths:
-------------
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Branching.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Getandput.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Invoking.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Linker.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Loading.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/LogicAndIntegerInc.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Newandmisc.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/PopDupSwap.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Pushing.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Return.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/Storing.java
branches/mango/MangoJPF/Mango/src/mango/worker/byteCodeModel/TypeCasting.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeNames.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
