[Javapathfinder-svn] SF.net SVN: javapathfinder:[1480] branches/mango/MangoJPF

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

Revision: 1480
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1480&view=rev
Author:   frankrimlinger
Date:     2009-05-03 16:57:47 +0000 (Sun, 03 May 2009)

Log Message:
-----------
Exceptions have been grocked.

First, the mango catch mechanism cannot be dropped.  The point is that a method doesn't "know" where it returns to, so an exception cannot "know" where it will be thrown.  All we can do is model the local structure of the throw, and stitch these together when evaluating a nested calling sequence within the target method.  Therefore, during the scanning phase, it is meaningless to trace the path of a thrown exception.  This is totally spurious information, just an artifact of the scanning process.  Therefore, there is no point throwing exceptions in the first place: mango already knows which instructions throw, and why they throw, and there is nothing more to be learned.

So, all the information about exceptions meticulously supplied to the scanner bytecodes must be stripped back out again.

Now here is where things get weird.  We still need to simulate all the handler code within the supplied methods and build the corresponding control flow graph segments.  Otherwise the mango catchers will have nowhere to send the caught exceptions.  So, just like in the case of clinits, we must rely on the target launcher to use MJI to get at these entrypoints.  Fortunately, they can be recovered from the MethodInfo class.  Its a little trickier than the case of invocations, because there could be multiple handlers in a given method, so you need to arrange to traverse all of them.  Also, you must manually push a ScannerStackFrame so that the handler will have something to digest.  (Since we are going into scanner mode, we don't have to bother with setting up the heap or the operand stack.)

Now what happens when the handler "returns". There is no problem here, because it will either happen because of a return or an athrow. Either way, we will pop the ScannerStackFrame and detect the jpf StackFrame, and this will trigger a phase change to jpf.  Execution will then proceed in the MangoTargetLauncher just after the native call to fire the handler.


Start by writing the launcher code and native methods to scan the handlers.  This is a brain-burner.

NB: If you are in scanning phase and you have already visited an instruction, then you should return null, meaning that this path need not be explored.

We need a master counter of ALL outstanding choices within a target method simulation.  A return to jpf should just return null if there are outstanding choices.  The transition to jpf should only occur when no choices remain.  This prevents jpf from backtracking back into a target once it has left it, potentially creating an exponential growth in the number of paths to traverse.

Modified Paths:
--------------
    branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
    branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.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/ALOAD.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ASTORE.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DRETURN.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FRETURN.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IRETURN.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LRETURN.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java

Added Paths:
-----------
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java

Removed Paths:
-------------
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScanChoiceGenerator.java


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