[Javapathfinder-svn] SF.net SVN: javapathfinder:[1491] branches/mango/MangoJPF/ javapathfinder-mango-bridge/mango/scanner

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

Revision: 1491
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1491&view=rev
Author:   frankrimlinger
Date:     2009-05-07 16:14:04 +0000 (Thu, 07 May 2009)

Log Message:
-----------
Fixed a few more scanning bugs.  Successful scan of all methods system code (i.e. in javapathfinder-trunk/env/jpf/java) and user code (in MangoJPF/mangoUserHome/rkrug/input). Identification of clinit, native, and abstract methods.  Identification of all unmodelled invocation destinations.  Verified tableswitch is working correctly, which is a good sign that BranchChoiceGenerator is ok.

It remains only to punch in the exception handler entrypoints to the TargetChoiceGenerator, and the scanner is complete. 

NB: OK, you need to position the scan AFTER the rulebase is read in.  The reason is that we must have the manifest of abstraction methods ready-to-go before the scan starts.

Now for some fun stuff.  Several things must happen on-the-fly as control flow edges are reported to mango: 

1. build a map from unmodelled-and-abstracted to rulebase abstractions.  Report link errors for unmodelled-and-not-abstracted

2. build a map from modelled-and-abstracted invocations to rulebase abstractions.

3. build a dependency graph of modelled-but-not-abstracted.  The leaves of this graph will be the candidates for the next abstraction target.

4. and of course, build the total control diagram whose vertices are bound to jpf Instructions and mango formal logic.  This is the critical binding that will allow context-free expressions to bind to context and tap into jpf world.

NOTE: in 1-3, vertices are bound to jpf MethodInfos.  

So, by the end of the scan, the stage is set for mango component analysis. We just jump right in at BackupAlg.phaseII() and deal with the culture shock.

Modified Paths:
--------------
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchListener.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/TargetChoiceGenerator.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOOKUPSWITCH.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/TABLESWITCH.java


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