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

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

Revision: 1636
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1636&view=rev
Author:   frankrimlinger
Date:     2009-06-17 01:48:16 +0000 (Wed, 17 Jun 2009)

Log Message:
-----------
Fixed context problem in itsAWrap.main.  The problem was the very ugly issue of "context transition" that will go away when the jpf rewriter kicks in.  Specifically the rule "abstract info resolution" has hardcoded literal embedded in subclause ( info "AbstractUconClass.AbstractUconMethod()V" -1 lineage ) which in MangoJPF needs to be (info "AbstractUconMethod()V" -1 lineage ) to account for minor differences in how certain names are generated.  No other instances of this literal occur in the rulebase, so hopefully this issue is put to rest.  This is a fine example of what a treacherous miserable business context is, even though it is essential for success.

As for the non-deterministic control flow bug, this was diagnosed instantly upon inspection of the 2D control flow diagrams.  Sometimes a picture is really worth 1k words.  In particular, the exceptional outgoing edges of an instruction that throws exceptions should bind to the branch condition for the exception.  This binding was present in Mango but not MangoJPF, as discovered by right clicking on the edges in question.  In the old days attempts were sometimes made to label the edges with their branch conditions, but this always made the graph too busy.

It turns out the fix for this bug was sort of there already, just needed a little tune up.  Most of the problem stems from really different terminology between Mango and MangoJPF for Instructions:

Mango			MangoJPF
lineNumber			offset
instructionIndex		position

The earlier fix introduction "syntheticPosition" was wrong.  What we really need is "syntheticOffset".  Also, all the places where you call getLineNumber() in mango have to be translated to getOffset() in MangoJPF, *NOT* getPosition().  

Further confusing the matter, jpf uses "lineNumber" to refere to source code lines.  Also, the jpf ExceptionHandler class returns positions for ranges, NOT offsets as one might expect when literally translating from JVM2ed.  So a conversion has to be made for this.

The offset/position confusion is probably not all sorted out yet.

With all this in place, we still need to force loading of the exception handler tables.  JPF is pretty lazy about this.  This work is in progress.

Modified Paths:
--------------
    branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
    branches/mango/MangoJPF/ACL2/itsAWrap-construct.lisp
    branches/mango/MangoJPF/ACL2/itsAWrap-construct.lisp.a2s
    branches/mango/MangoJPF/ACL2/mango-model.lisp.a2s
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/AbstractUconMethod.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BadMethod.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInterface.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/OSmethod.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AbstractUconPlace.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BadPlace.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BeginningOfTime.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKETARGET.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/OSplace.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SyntheticInstruction.java
    branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
    branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip

Added Paths:
-----------
    branches/mango/MangoJPF/mangoUserHome/frank/sessions/baseline/itsAWrap/main([I)Z/a.zip


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