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

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

Revision: 1704
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1704&view=rev
Author:   frankrimlinger
Date:     2009-06-30 20:50:37 +0000 (Tue, 30 Jun 2009)

Log Message:
-----------
ATHROWHANDLER is not branching correctly, so that instructions (like ASTORE) that handlers normally flow into are unreachable.  The problem is that the ReturnPointLinkSym mechanism is not implemented.  Probably need to go back to the original C++ to figure out what is going on here.  The place to start is ClassParsingAlg::linkAthrowHandler.  Working with marc's hypo2 test code.

Looking ahead, some details of the jpf rewriter are becoming clear.  Phase2 will terminate prior to stratification, just emitting a set of components.  The component selection algorithm will pick the "best" independent component, meaning a component "near" the target method which does not depend on any non-abstracted module.  A synthetic MethodInfo will be created whose "instructions" are just proxies for the vertices of this component.  A new extension of JPF, called REWRITER, will be instantiated.  REWRITER will just act directly on the instructions of the synthetic MethodInfo, bypassing the class loading phase altogether.  The different types of component vertices will give rise to different instructions, so that component connectors can be properly interpreted and loop vertices can orchestrate the "look-behind" strategy for invariant computation.  Since this strategy only involves looking backward along a single execution path, it doesn't really need the full weight of the backtracking mechanism.  But the backtracking mechanism will still have its traditional role of exhausting all paths, or at least all "interesting" paths, so that targeted module will be specified in a single REWRITER pass.  This will make the process much more efficient as common initial paths no longer require re-tracing for each case.  An "ordinary" instruction will just handle composition with the forward predicate transformer B* ^ I*.  For non-trivial non-loop-dependent branch predicates B=b1 v .. V bn, the branch condition bi can just be automatically translated and assumed, displaying automatically in the specification window.  The updated state can also be translated to check for a "translation halt".  Whenever there is a translation halt, the user will intervene with appropriate definitions and translation rules.  Once the situation is rectified, then REWRITER will fire back up and continue generating the specification.  For loop-dependent branches B, REWRITER will first try invariant look-behind to eliminate the loops.  If this fails, there will be an "invariance halt".  In the case of loop termination, B will consist of a set of alternative ways to exit a loop, and the user then must choose the nominal exit condition as the "termination conjecture".  (In the uncommon case of more than one nominal exit, the user can declare a backtracking point to get the opportunity to explore it later.)  In any case, the user must formulate a conjecture that ensures deterministic forward execution, so that mango knows what branch to take.  The user must also volunteer hypotheses on the module input parameters that make the conjecture true.  This is on a best-effort basis, proof of conjectures is sub-contracted to a theorem prover.  Since at all times REWRITER "knows where we are", context can be zippered on as needed for computations which require context.  In particular, context does not need to be present during state composition, so the whole "context resolution" issue goes away.  There will also be the existing halt for module instantiation.  Note that the strategies which require halting should be handled by listeners so that the instructions can concentrate on the basic issue of state transition.

Modified Paths:
--------------
    branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java


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