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

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

Revision: 1460
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1460&view=rev
Author:   frankrimlinger
Date:     2009-04-29 02:33:37 +0000 (Wed, 29 Apr 2009)

Log Message:
-----------
Earlier comment was somewhat confused.  It is indeed true that you need MJIEnv to parse state object, however, I will never need to do this.  I do need to get the structure of the Instruction objects, but these are already at the JVM level, so good to go.


Refined the phase change strategy.  We define the extension ScannerStackFrame of StackFrame. 

When an invocation instruction executes, if SCANNER.scannerPhase is BEGIN or SCAN, then it sets up an InvocationChoiceGenerator if one is not present already.  SCANNER.scannerPhase is set to SCAN.

InvocationChoiceGenerator is trivial for all but virtual invocation.  But it is easier just to cover all cases with the same procedure.

The choices of which methods could possibly be virtually invoked are determined by existing mango strategies.  However, as classes are now loaded just-in-time, we need to enforce a pro-active class loading up front to make sure the entire targeted code base is surveyed for candidates.  No big deal, just a recursive walk though classpath space and a hashed inventory of fully qualified method names and signatures.  There is just no other way to do this.

The generated choice instructions will be INVOKExxxSCAN, corresponding to the original INVOKExxx instruction.  These synthetic instructions will push a ScannerStackFrame.

A return instruction examines the class of the caller frame.  If this class is NOT a ScannerStackFrame, then SCANNER.scannerPhase is set to JPF.

Note that END phase is not needed and has been discarded.

Both the invocation and return instruction families must implement the Transition interface.  This just emphasizes the fact that, even when in BEGIN or SCAN phase, these instructions act on JPF state, by adding or removing frames as appropriate.  Also, when a return instruction does transition to JPF, it must push some sort of dummy value onto the caller opstack if required, or there will be tears.

The BEGIN transition is probably unnecessary, since the transition from JPF to BEGIN occurs in the native code scan(), just before we box and return the invocation instruction.  So it seems likely that the invocation is the next thing to happen anyway.  If this proves to be so, then BEGIN can be eliminated.

Note that all this depends very much on the single threaded assumption.  A multi-threaded version would, at a minimum, require scannerPhase maintained on a per thread basis.  But since multithreading would bring formal analysis to its knees anyway, there is no point to adding this layer of complexity.

Modified Paths:
--------------
    branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_scanner_ScannerMJI.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoTargetLauncher.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScanChoiceGenerator.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScannerMJI.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

Added Paths:
-----------
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/ScannerStackFrame.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/TargetMethodRegistrar.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINITSCAN.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACESCAN.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIALSCAN.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATICSCAN.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUALSCAN.java

Removed Paths:
-------------
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/MethodInfoAdapter.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/ReturnInstructionAdapter.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/StackFrameAdapter.java


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