Menu
▾
▴
[Javapathfinder-svn] SF.net SVN: javapathfinder:[1884] branches/mango/Mango
|
From: <fra...@us...> - 2009-09-02 04:15:45
|
Revision: 1884
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1884&view=rev
Author: frankrimlinger
Date: 2009-09-02 04:15:34 +0000 (Wed, 02 Sep 2009)
Log Message:
-----------
Introduced JPFrewriter and its Launcher and InstructionFactory in the new package mango.rewriter in the javapathfinder-mango-bridge. Moved classes Edge and Vertex, which extend Graphic, from mango.worker.mangoModel to mango.rewriter.synthetic. The base class Graphic now extends Instruction, so JPFrewriter can now execute Vertex and Edge objects. So far so good, but how is this execution to take place?
Here is a theory of operation, which is somewhat speculative at this point. JPF has the notion of a Step, which is an executed instruction, and a Transition, which is a sequence of Steps from the last branch point. The current trail is stored in the SystemState and so is available to the execute() method of an instruction. The point is that an Instruction that is executing can obtain the "last step" of the trail, which presumably is the instruction that just executed, if any.
Here is the punchline: a Step can store an "annotation", which can be any Object. Its pretty clear that JPF regards this as user register, since the only reference to setAnnotation() is in an MJI method called addComment(), which probably enables the source code annotation concept. As this only exists in JPF extensions, we presumably are free to knock ourselves out. So annotate a Step by storing MangoState
class MangoState{
Hitem totalState;
Hitem partialState;
}
Now we are good-to-go. TotalState is the accumulated state from the module entry point to the current instruction, and partialState is the accumulated state from the last branch point. Its up to the choice generators to carry the total state from one Transition to the next. TotalState will enable specification, and partialState will enable invariant factorization.
This feels right, but here is a question. How can an Instruction that is executing get a hold of its Step, which doesn't exist yet? This must be listener thing.
Well, at the outset have to call ss.recordSteps(true), where ss is the SystemState singleton. Then, assuming nobody has altered the logInstruction field of the ThreadInfo, the step will be recorded just AFTER execution of the instruction. But then, as expected, there is vm.notifyInstructionExecuted, passing this ThreadInfo and the instruction.
So, we install a listener that responds to "instruction executed" by
1) Creating the formal expressions for the new MangoState.
2) posting a rewrite message to a higher priority queue and blocking the JPFrewriter thread. There will have to be some work done in the ThreadSupport project to allow execution of higher priority messages while a message is in the "blocked" state. Currently there is no such state, but it's time to face the music. There is no other way, short of abandoning jpf. Since we are in a listener when the block occurs, JPFrewriter should be in a pretty consistent state.
Now this rewriter message is going to be firing up Module instantiations, which will affect data in ChoiceGenerators, and invariant detection, which will cause tracebacks. The tracebacks are read-only as far as JPFrewriter is concerned, so relatively safe. But the fact is that we will be messing with ChoiceGenerator data while blocked inside a listener, but this seems safe enough. When the JPFrewriter wakes up, it exits the listener and continues the Transition. When the transition is done and a new choice is made, well, it may not be a choice we could have predicted in advance, but that's life.
So, JPFrewriter will be the main driver of automation. It will take frequent naps, but each time it wakes up it will be a little bit smarter. What is nice about dynamically wiring the choice generators is that the game can be made to play itself until all cases are exhausted, at which point the JPFcmd finally finishes and the higher level automation kicks in to clean up, restart, select the next target, and fire up a new JPFrewriter.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/deprecatedPackage/DeprecatedMethods.java
branches/mango/Mango/Mango/src/mango/graph/data/supervertex/SuperEntryData.java
branches/mango/Mango/Mango/src/mango/graph/data/ucon/UconData.java
branches/mango/Mango/Mango/src/mango/gumboModel/factory/EmbeddedJVMFactory.java
branches/mango/Mango/Mango/src/mango/gumboModel/factory/GraphModelFactory.java
branches/mango/Mango/Mango/src/mango/gumboModel/factory/MultiGraphModelFactory.java
branches/mango/Mango/Mango/src/mango/gumboModel/factory/SourceModelFactory.java
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/AssignNotObjectValue.java
branches/mango/Mango/Mango/src/mango/tree/model/Cell.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/AlphaDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/BackupDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/CodeDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/EdgeDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/GraphDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/OmegaDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/UconDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/BackupEdge.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/EdgeIterator.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/InstallResult.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/Path.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/PathCollection.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/SimpleLoopPath.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/AcyclicGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/CpnGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/Graph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/SuperCpnGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/GraphicSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/LoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/PackageSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/SuperVertexClassSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/return_terminator/ReturnTerminatorSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/sink_terminator/SinkTerminatorSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperBlowUpSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperEntrySym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperLoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/InvocationUconSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/UconOSTerminatorSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/UconSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/AcyclicVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/BackupVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/CallVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/LoopVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/MethodVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/SuperVertex.java
branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInterface.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
Added Paths:
-----------
branches/mango/Mango/javapathfinder-mango-bridge/gov/nasa/jpf/JPFrewriter.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/InstructionFactory.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/Launcher.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Edge.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Graphic.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/Edge.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graphic/Graphic.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/Vertex.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
