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

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

Revision: 1710
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1710&view=rev
Author:   frankrimlinger
Date:     2009-07-01 21:03:05 +0000 (Wed, 01 Jul 2009)

Log Message:
-----------
Each invocation is followed by an ACATCHHANDLER which handles exceptions thrown by callee but not caught in callee.   Each instruction which potentially throws and exception directly is followed by an ATHROWCREATOR.  The purpose of these synthetic instructions is to route the exception to the correct handler instuctions embedded in the code block, or to the synthetic ATHROWHANDLER instruction to handle the finally clause and/or uncaught exceptions.

Fix in progress so that the ACATCHHANLDER and ATHROWCREATORs are 
a) created before referenced
b) passed to the choice generator of the instruction which invokes, in the case of ACATCHHANDLER, or throws, in the case of ATHROWCREATOR, and,
c) endowed with their branches prior to scanner execution, so that scanner flow through all the handlers is accomplished.

INVOKEINTERFACE conforms to the new scheme, remains to rewire the rest of the invocations and then all the other methods throwing exceptions.

Some comments to clear up the vast cloud of confusion that has accompanied this issue.

The theory of return points is thus: each invocation in the modeled code determines which methods it potentially calls.  So we get a map invocation --> {potentially_called_method}.  Inverting this map gives method --> {potential_invocation_point}.  By considering the next instruction after the point of invocation, we get method-->{potential_return_point}.

There are two tricky observations to make:
1) The universal connector (ucon) for a return instruction has the form OR_i (and invocation_i return_point_i).  In a flat calling space, this ucon is never actually applied, because the state transition of the invoked method is already known, and so it is just applied along the branch from invocation to next instruction.  However, in the case of mutual co-recursion, the return branch condition is in play.  To resolve this condition the invocation point became part of the "context" of the callee frame.  This context was then dragged along ball-and-chain style as the state transitions of the callee were composed, vastly increasing the complexity of the rewrite rules.  But in the brave new jpf world, we have look-behind, so we can go *get* the invocation point in the rare event we need to resolve a return condition.  Otherwise, we don't trouble ourselves about it at all.

2) The logic of the return point system implements (1).  The reason some of this logic is commented out is historical.  ATHROWCREATOR creates the branch conditions required to route an exception thrown by a non-invocation instruction.  Ditto ACATCHHANDLER for invoke instructions.  Originally, ATHROWCREATOR and ACATCHHANDLER folded in the return branch condition of (1) in the case of an uncaught exception.  But then Marc thought, "we need to implement finally".  So the return logic was commented out and replaced by a branch to the unique ATHROWHANDLER for the method.

Modified Paths:
--------------
    branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.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/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/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/INVOKEVIRTUAL.java


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