Menu
▾
▴
javapathfinder-svn — source repository related messages (SVN)
You can subscribe to this list here.
| 2008 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(16) |
Jun
(42) |
Jul
(46) |
Aug
(48) |
Sep
(33) |
Oct
(26) |
Nov
(28) |
Dec
(38) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2009 |
Jan
(35) |
Feb
(80) |
Mar
(112) |
Apr
(108) |
May
(102) |
Jun
(126) |
Jul
(89) |
Aug
(82) |
Sep
(36) |
Oct
(7) |
Nov
(1) |
Dec
(4) |
| 2010 |
Jan
(87) |
Feb
|
Mar
(2) |
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: <wat...@us...> - 2009-10-02 05:16:26
|
Revision: 1919
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1919&view=rev
Author: watcharin
Date: 2009-10-02 05:16:19 +0000 (Fri, 02 Oct 2009)
Log Message:
-----------
Separate logging code from CacheNotifier to the new class, CacheLogger.
Use JPF logging interface instead of "System.out.print". State numbers are displayed on "fine" log level. Operations on trees and cache are displayed on "info" log level.
Modified Paths:
--------------
trunk/extensions/net-iocache/bin/env.sh
trunk/extensions/net-iocache/env/jpf/gov/nasa/jpf/network/cache/CacheLayerInputStream.java
trunk/extensions/net-iocache/env/jpf/java/net/ServerSocket.java
trunk/extensions/net-iocache/env/jpf/java/net/Socket.java
trunk/extensions/net-iocache/env/jvm/gov/nasa/jpf/jvm/JPF_java_net_ServerSocket.java
trunk/extensions/net-iocache/src/gov/nasa/jpf/network/cache/CacheLayer.java
trunk/extensions/net-iocache/src/gov/nasa/jpf/network/cache/PhysicalConnection.java
trunk/extensions/net-iocache/src/gov/nasa/jpf/network/cache/RRTree.java
trunk/extensions/net-iocache/src/gov/nasa/jpf/network/listener/CacheNotifier.java
trunk/extensions/net-iocache/src/gov/nasa/jpf/network/listener/SearchTreeMonitor.java
Added Paths:
-----------
trunk/extensions/net-iocache/src/gov/nasa/jpf/network/listener/CacheLogger.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ada...@us...> - 2009-10-01 17:44:04
|
Revision: 1918
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1918&view=rev
Author: adam_kiezun
Date: 2009-10-01 17:43:52 +0000 (Thu, 01 Oct 2009)
Log Message:
-----------
jFuzz: delete unused test, update documentation, add example
Modified Paths:
--------------
trunk/extensions/concolic/doc/userdoc.html
Added Paths:
-----------
trunk/extensions/concolic/simpleTest.sh
Removed Paths:
-------------
trunk/extensions/concolic/test/jfuzz/tests/StringTest.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ada...@us...> - 2009-09-30 19:22:44
|
Revision: 1917
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1917&view=rev
Author: adam_kiezun
Date: 2009-09-30 19:22:32 +0000 (Wed, 30 Sep 2009)
Log Message:
-----------
contributed by David Harvison: jFuzz caching strategies, next-file selection strategies, coverage metrics
Modified Paths:
--------------
trunk/.classpath
trunk/extensions/concolic/src/gov/nasa/jpf/util/Files.java
trunk/extensions/concolic/src/jfuzz/ConcolicListener.java
trunk/extensions/concolic/src/jfuzz/JFuzz.java
trunk/extensions/concolic/src/jfuzz/JFuzzConfig.java
trunk/extensions/concolic/src/jfuzz/JPF_jfuzz_DebugFuzz.java
trunk/extensions/concolic/src/jfuzz/termination/NeverTerminate.java
trunk/extensions/concolic/src/jfuzz/termination/TerminationStrategy.java
trunk/extensions/concolic/src/jfuzz/termination/TimedTermination.java
trunk/extensions/concolic/src/jfuzz/termination/UpToFixedNumber.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/CharMultiArrayPC.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/CharPC.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/JPF_gov_nasa_jpf_concolic_tests_TestUtils.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/MultiArgsPC.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/MultiPC.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/SimpleCharArrayPC.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/SimplePC.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/tests/TestUtils.java
trunk/extensions/concolic/test/gov/nasa/jpf/concolic/unitTests/AllTests.java
trunk/extensions/concolic/test/jfuzz/unitTests/AbstractJFuzzTest.java
trunk/extensions/concolic/test/jfuzz/unitTests/AllTests.java
trunk/extensions/concolic/test/jfuzz/unitTests/ReadTest.java
trunk/extensions/concolic/test/jfuzz/unitTests/SimpleTest.java
trunk/extensions/concolic/test/jfuzz/unitTests/SimplifyPCTest.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/BinaryLinearIntegerExpression.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/SymbolicInteger.java
Added Paths:
-----------
trunk/extensions/concolic/doc/index.css
trunk/extensions/concolic/doc/jfuzz.png
trunk/extensions/concolic/doc/userdoc.html
trunk/extensions/concolic/doc/userdoc.pdf
trunk/extensions/concolic/lib/emma.jar
trunk/extensions/concolic/src/jfuzz/cache/
trunk/extensions/concolic/src/jfuzz/cache/CacheStrategy.java
trunk/extensions/concolic/src/jfuzz/cache/NameIndependentCache.java
trunk/extensions/concolic/src/jfuzz/cache/NoCache.java
trunk/extensions/concolic/src/jfuzz/cache/OneToOneMap.java
trunk/extensions/concolic/src/jfuzz/nextfile/
trunk/extensions/concolic/src/jfuzz/nextfile/Coverage.java
trunk/extensions/concolic/src/jfuzz/nextfile/Newest.java
trunk/extensions/concolic/src/jfuzz/nextfile/NextFileStrategy.java
trunk/extensions/concolic/src/jfuzz/nextfile/Oldest.java
trunk/extensions/concolic/src/jfuzz/nextfile/Random.java
trunk/extensions/concolic/src/jfuzz/util/
trunk/extensions/concolic/src/jfuzz/util/Constraints.java
trunk/extensions/concolic/src/jfuzz/util/MeasureCoverage.java
trunk/extensions/concolic/src/jfuzz/util/MeasureTiming.java
trunk/extensions/concolic/src/jfuzz/util/SimplifyPC.java
Removed Paths:
-------------
trunk/extensions/concolic/ReadMe.html
trunk/extensions/concolic/src/jfuzz/PathCache.java
trunk/extensions/concolic/src/jfuzz/SimplifyPC.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <tel...@us...> - 2009-09-28 02:21:58
|
Revision: 1916
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1916&view=rev
Author: telcontar
Date: 2009-09-28 02:21:46 +0000 (Mon, 28 Sep 2009)
Log Message:
-----------
* Statistics.java: instructions counter "insns" wraps around for large runs when limited to 31+sign bits; changed to long.
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/report/Statistics.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ppa...@us...> - 2009-09-25 13:46:53
|
Revision: 1915
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1915&view=rev
Author: pparizek
Date: 2009-09-25 13:46:46 +0000 (Fri, 25 Sep 2009)
Log Message:
-----------
PriorityParameters are now reflected by RealtimeThread and NoHeapRealtimeThread
Modified Paths:
--------------
trunk/extensions/rtembed/env/jpf/javax/realtime/NoHeapRealtimeThread.java
trunk/extensions/rtembed/env/jpf/javax/realtime/PriorityParameters.java
trunk/extensions/rtembed/env/jpf/javax/realtime/RealtimeThread.java
trunk/extensions/rtembed/env/jpf/javax/realtime/SchedulingParameters.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ne...@us...> - 2009-09-22 20:34:37
|
Revision: 1914
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1914&view=rev
Author: nehas
Date: 2009-09-22 20:34:30 +0000 (Tue, 22 Sep 2009)
Log Message:
-----------
* Added some getter functions to the MetaHeuristic and GuidedDFSearch classes
* Added a stateGenListener class inorder to get access to the abstract traces and concrete state to visualize the guided search
* Minor modifications to the RunGuidedTest and TraceOutputListener
Modified Paths:
--------------
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/jpf/TraceOutputListener.java
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/heuristic/GuidedDFSearch.java
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/heuristic/MetaHeuristic.java
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/setup/RunGuidedTest.java
Added Paths:
-----------
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/visualize/
trunk/extensions/guidedsymbolic/src/edu/byu/cs/guided/search/visualize/StateGenListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-22 17:17:02
|
Revision: 1913
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1913&view=rev
Author: frankrimlinger
Date: 2009-09-22 17:16:54 +0000 (Tue, 22 Sep 2009)
Log Message:
-----------
This is the final update to the jpf source-forge respository for the Mango project. The new home for Mango is the Mercurial (as opposed to SVN) repository at
http://babelfish.arc.nasa.gov/hg/jpf/jpf-mango
The new java pathfinder wiki is at
http://babelfish.arc.nasa.gov/trac/jpf/
and the Mango wiki may be accessed from this page, or at
http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-mango
Modified Paths:
--------------
branches/mango/Mango/.classpath
branches/mango/Mango/.project
branches/mango/Mango/META-INF/MANIFEST.MF
branches/mango/Mango/jpf-mango-bridge/gov/nasa/jpf/JPFrewriter.java
branches/mango/Mango/jpf-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/Mango/jpf-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/FieldInstruction.java
Added Paths:
-----------
branches/mango/Mango/jpf-mango-bridge/
branches/mango/Mango/plugins/bcel_plugin_1.0.0.jar
Removed Paths:
-------------
branches/mango/Mango/default.properties
branches/mango/Mango/javapathfinder-mango-bridge/
branches/mango/Mango/plugins/jpf_trunk_build_tools_lib_1.0.0.jar
branches/mango/Mango/plugins/jpf_trunk_lib_1.0.0.jar
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ppa...@us...> - 2009-09-22 14:17:06
|
Revision: 1912
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1912&view=rev
Author: pparizek
Date: 2009-09-22 14:03:35 +0000 (Tue, 22 Sep 2009)
Log Message:
-----------
more precise capture of visibility of scoped memory areas among threads
Modified Paths:
--------------
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/memory/MemoryAreasChecker.java
Added Paths:
-----------
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/memory/ScopedMemoryAwareSchedulerFactory.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-21 04:20:02
|
Revision: 1911
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1911&view=rev
Author: frankrimlinger
Date: 2009-09-21 04:19:56 +0000 (Mon, 21 Sep 2009)
Log Message:
-----------
Completed testing of TrailManager. Removed the logic from the Graphic.execution() jig which caused an instruction to visited only once. This was sufficient for the code subdivision algorithm but case enumeration requires the potentially exponential enumeration of all paths. Fixed bug involving MethodEntrySym. The MethodEntrySym should walk the LoopGraph with blowup level 0, NOT the CpnGraph, starting at the corresponding entrypoint. (The CpnGraph is generally not even acyclic, so the walk doesn't terminate.) Fixed bugs in Vertex.getDestinations(). Tested exhaustive walk logic (excluding omea-alpha jump). Added weak attractor logic to BlowupChoiceGenerator and tested.
To complete the global traversal logic, need to write MethodChoiceGenerator.getDestination(). This is complicated by the need to maintain the TrailState. Then on to "unravelling predicate transformers.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/graph/data/ucon/UconData.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/Sym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/EdgeSym.java
branches/mango/Mango/Mango/src/mango/worker/msg/OpenDefinitionMsg.java
branches/mango/Mango/Mango/src/mango/worker/msg/SelectTargetMsg.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/BlowupChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/LoopChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MangoAnnotation.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/TrailManager.java
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/MethodEntrySym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-18 20:41:28
|
Revision: 1910
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1910&view=rev
Author: frankrimlinger
Date: 2009-09-18 20:41:21 +0000 (Fri, 18 Sep 2009)
Log Message:
-----------
Completed coding of TrailManager to construct the strong and weak maps. Need to test.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graphic/GraphicConnection.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/ComponentChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Edge.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
Added Paths:
-----------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/TrailManager.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-16 20:51:04
|
Revision: 1909
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1909&view=rev
Author: frankrimlinger
Date: 2009-09-16 20:50:57 +0000 (Wed, 16 Sep 2009)
Log Message:
-----------
To write the choice logic for methods and blowups, first need the notion of the *strong attractor* and the *weak attractor* of a vertex. The strong attractor S(v) of v is the maximal subgraph of G with unique sink v. Clearly the strong attractor is unique, and for vertices v and w, either S(v) and S(w) are disjoint, or one of these graphs is included in the other. The weak attractor W(v) of v is the union of all paths which terminate at v. Clearly W(v) contains S(v). The attraction is weak because when you are in W(v)-S(v) you still have the chance to escape v altogether.
Let G be the graph of all components together with superCpnConnection and subCpnConnection connections. We are interested in S(omega) and W(omega) for omega vertices of G.
Computation for S(v):
0) v is in S(v)
1) if w is a vertex of S(v), then every inbound edge to w is in S(v).
2) a vertex w is in S(v) if and only if every outbound edge of w is in S(v).
Computation for W(v)
0) S(V) is in W(v)
1) if w is a vertex of W(v), then every inbound edge to w is in W(v).
2) a vertex w is in W(v) if and only if there exists an outbound edge of w in S(V).
MethodChoiceGenerator trail logic: Let Omega be the set of all omega vertices. The the trail state set is {open,attracted,repelled} x Omega. The trail starts out in the open state for each omega. If it enters S(omega) for some omega, the state transitions to attracted for that omega. The trail must now hit omega, when it does, it jumps to the corresponding alpha, and changes its state to repelled with respect to omega. The trail must now remain in the repelled state with respect to omega, which means either stopping at alpha (i.e. stuck in infinite loop) or traveling along a path in G-V(omega) to a sink of G. Notice that by infinite loop we mean a *structurally* infinite loop, i.e., no exit branch, like while(true){}. This doesn't happen very often, but a driver could have this structure.
Strictly speaking the attracted state is unnecessary, but good feedback.
BlowupChoiceGenerator trail logic: Start at alpha and remain in W(omega). End at omega.
Observe that there is ample opportunity for exponential growth in the number of trails. But for now, we punt on case filtering and case consolidation. The point here is that the computation of S(v) and W(v) is linear in the size of G, so there is no problem computing the branching logic as such.
To implement, after you get the choice vector, you can enumerate the relevant omega vertices, then use computation logic above to radiate away from each omega, updating
HashMap<Object,HashSet<Vertex>> strongMap
HashMap<Object, HashSet <Vertex>> weakMap
Given any edge, relevant GraphicConnection, or vertex x, strongMap.get(x) contains omega for x in S(omega). Mutatis mutandis for weak map.
The following gets added to the MangoAnnotation to manage the trail state:
enum TrailState {ATTRACTED,REPELLED}
HashMap<Vertex,TrailState> trailState
The trail state is assumed to be open for each omega, unless otherwise indicated. Now just update trailState everytime there is a state change as described above.
Introduce TrailManager object to compute strongMap and weakMap. The ComponentChoiceGenerator constructor instantiates and initializes the TrailManager.
Modified Paths:
--------------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
branches/mango/Mango/src/mango/intro/LoginDialog.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-16 03:38:33
|
Revision: 1908
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1908&view=rev
Author: frankrimlinger
Date: 2009-09-16 03:38:26 +0000 (Wed, 16 Sep 2009)
Log Message:
-----------
Hotwired RewriteListener.instructionExecuted() and Graphic.execute() for test of global traverse logic. Traversal of simple loops and blowups appears to be functional, using default logic to traverse a graph. Test with nested_blowup.
FIX bug traversing MethodEntrySym graph with default logic. Then punch in the external getDestinations() logic in the RewriteChoiceGenerator extensions and test. Then restore RewriteListener and Graphic logic and start working on the internal logic.
Modified Paths:
--------------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/BlowupChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/LoopChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MethodChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteListener.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Graphic.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/LoopSym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/MethodEntrySym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/SuperLoopSym.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-15 20:23:52
|
Revision: 1907
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1907&view=rev
Author: frankrimlinger
Date: 2009-09-15 20:23:44 +0000 (Tue, 15 Sep 2009)
Log Message:
-----------
Moved MethodEntrySym, SuperLoopSym, and LoopSym into the rewriter.synthetic package. Extended these class from Instruction and implementing the new ComponentInstruction interface. Added superCpnSym field to MethodEntrySym so it can retrieve the component graph with the corresponding entrypoint.
With this in place, ComponentChoiceGenerator now simply executes each ComponentInstruction, working backwards from the end of the component vector generated by the BackupAlg instance.
Each component instruction executes by installing the corresponding choice generator.
MethodEntrySym: MethodChoiceGenerator
walks CpnGraph, starting at entrypoint corresponding to MethodEntrySym. Follows connectors, passing through a given omega no more than once per case. To "pass through" omega means that you automatically jump to the corresponding alpha and keep going.
SuperLoopSym: BlowupChoiceGenerator
walks LoopGraph starting at alpha. Follows connectors which remain in this graph. case must end at omega
LoopSym: LoopChoiceGenerator
walks linear path, starting at supplied entrypoint.
The details to set all this up are quite idiosyncratic, which is why the Syms were all broken out as separate instructions.
Completed coding of ComponentChoiceGenerator. Tested against baseline package code. The components are executed in the correct order.
Completed coding of the ComponentInstruction execute() methods, so that the proper RewriteChoiceGenerator created with an Outbound choice corresponding entrypoint and loaded as the new choice generator. Previous testing of RewriteChoiceGenerator loaded the entrypoint from the current DefinitionManger. But now we just proceed with no DefinitionManger. Whatever gui monitoring is required will start more or less from scratch as requirements change dramatically.
There are now two kinds of traversal logic on a collision course. The first is the logic of "unravelling predicate transformers", 1892-1896, and the logic of component choice generators, discussed in 1898 and summarized above. This can be thought of as local and global traversal logic, respectively. The global logic may be viewed as constraining the local choices to the admissible outbound edges. This constraint is introduced programmatically by creating RewriteChoiceGenerator.getDestinations(). For the test jig, this method just returned *all* the outgoing edges. But now the problem is bounced to the current choice generator, one of the above. The choice generator then must probe the graph in question to determine which edges and/or vertex connector destinations are appropriate, and return them.
Incidentally, this functionality now obviates the need for the ucon and gstack formalism. For now this formalism will be left intact in the loop algorithm, because it was very hard to get right in the first place and it may once again be needed someday. It will be the job of the choice generator deliver the proper "glue" across connectors.
TODO: before tuning the state logic, get the global traversal logic working. Specifically, this means implementing getDestinations() within the RewriteChoiceGenerator extensions.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/graph/data/graphic/LoopData.java
branches/mango/Mango/Mango/src/mango/graph/data/supervertex/SuperLoopData.java
branches/mango/Mango/Mango/src/mango/graph/data/ucon/MethodEntryData.java
branches/mango/Mango/Mango/src/mango/graph/msg/Graph2DViewCreateRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/loop/msg/LoopDefinitionLocatorMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/loop/msg/LoopDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/method/MethodDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/method/msg/CreateMethodStubMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionLocatorMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/instance/loop/agent/LoopInstanceAgent.java
branches/mango/Mango/Mango/src/mango/module/instance/loop/model/LoopInstanceManager.java
branches/mango/Mango/Mango/src/mango/module/instance/loop/msg/CloseLoopInstanceMsg.java
branches/mango/Mango/Mango/src/mango/module/instance/loop/sym/LoopInstanceSym.java
branches/mango/Mango/Mango/src/mango/ruleAction/module/instance/BuildLoopInstanceManager.java
branches/mango/Mango/Mango/src/mango/ruleAction/module/instance/InstantiateLoopERROR.java
branches/mango/Mango/Mango/src/mango/ruleAction/module/instance/IsLoopDefinitionClosed.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/LoopSymReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/MethodEntrySymReq.java
branches/mango/Mango/Mango/src/mango/worker/Mango.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hitem.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/InterpretableSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/Path.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperBlowUpSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/AlphaSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/BackupVertex.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/msg/SelectTargetMsg.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/HitemUtil.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/BlowupChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/ComponentChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/LoopChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MethodChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteListener.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Graphic.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/InvokeRewriter.java
Added Paths:
-----------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/ComponentInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/LoopSym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/MethodEntrySym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/SuperLoopSym.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/LoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperLoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-14 20:55:31
|
Revision: 1906
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1906&view=rev
Author: frankrimlinger
Date: 2009-09-14 20:55:20 +0000 (Mon, 14 Sep 2009)
Log Message:
-----------
Target selection is now wired up to the target preference and fully implemented and tested against MutualRecursion, ecap2, nested_blowup, and ItsAWrap. The target selection algorithm will always produce a component choice vector for JPFrewriter, unless there truly is nothing at all to specify. In the event a component choice vector is produced, SelectTaretMsg will kick off JPFrewriter.
Proceed with 1899, except that the "ComponentSurvey" is no longer necessary. The vector of components for the ComponentChoiceGenerator, in order of increasing independence, is already created. just call BackupAlg.getInstance().getComponentChoiceVector and walk it backwards.
TODO: write component choice generator and path choice generator. This is enough to get started with ItsAWrap.clear target. Work through all the issues involved with semi-automation of the loop specification.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/graph/msg/ForwardFlowRequestMsg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/msg/SelectTargetMsg.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-14 05:08:09
|
Revision: 1905
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1905&view=rev
Author: frankrimlinger
Date: 2009-09-14 05:08:00 +0000 (Mon, 14 Sep 2009)
Log Message:
-----------
A SuperCpnSym represents a Graph whose entrypoints are MethodEntrySym's. Each such MethodEntrySym must, at least for the time being, fire up a DefinitionManager. A MethodEntrySym is a GraphicSym, and so has an outgoingConnections field, which is a set of GraphicConnection's. There are many kinds of GraphicConnection, but the relevant one for walking the forward flow are the superCpnConnection and subCpnConnection
>From the point of view of walking forward flow, the only wrinkle introduced by a system with mutual co-recursion is that not all entrypoints of a SuperCpnSym are associated with the same method. In fact, there will be one such entrypoint for each method of the system. This is not a problem because each entrypoint gets its own DefinitionManager anyway.
Introduced GraphIterator class, and migrated graph walking functionality so nested walks can take place. This ancient bug is finally put to rest. Compared modelling of "frank" configuration in Mango versus MangoBaseline, precisely 28 seconds in both cases, so that there is zero performance hit using the GraphIterator class.
Generated the flat list of terminal SuperCpnSym's. However, what we really want is the corresponding flat list of MethodEntrySym's. Not necessarily one-to-one because of mutual corecursion. Also on the fly create maps
MethodInfo--> Vector<Integer>
ClassInfo --> Vector<Integer>
Which map each associated method and class to the corresponding indices of the flat vector. Now give a target that maps to a MethodInfo or ClassInfo, you can map to an index and hence a MethodEntrySym. But not done yet. We really need to find the least dependent module associated with MethodEntrySym. In order to do this, need to back off to the SuperCpnSym, and flatten its forward flow, picking up all SuperLoopSym's which are destinations of a SuperBlowUpSym's, and all LoopSym's. You don't need to bother with initial SuperLoopSym's as these do not contain an alpha-omega pair.
So, to summarize, once you deduce the "closest" MethodEntrySym, you flatten its *relevant* forward flow. This give you the order of component execution for the ComponentChoiceGenerator, modulo duplicate entries.
TODO: finish the target selection algorithm by acquiring the nearest MethodEntrySym and preparing the required ordering for the ComponentChoiceGenerator.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/AcyclicGraph.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/sym/graphic/GraphicSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/SuperVertexClassSym.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/UconSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/AcyclicVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/SuperCpnVertex.java
branches/mango/Mango/Mango/src/mango/worker/msg/OpenDefinitionMsg.java
branches/mango/Mango/Mango/src/mango/worker/msg/SelectTargetMsg.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/GraphIterator.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-11 18:44:12
|
Revision: 1904
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1904&view=rev
Author: frankrimlinger
Date: 2009-09-11 18:44:06 +0000 (Fri, 11 Sep 2009)
Log Message:
-----------
Debated whether or not to improve graph class names. Decided against doing so because they make good sense in the context of the original loop algorithm, which is still completely intact and must be maintained. The mapping of 1803 will suffice.
Changed target class preference to target preference. The user just enters any string. Mango first tries to match a class, and if that doesn't work, a method, and if that doesn't work, the chosen target is the first available terminal SuperCpnSym, and if none, then done.
TODO Encapsulate this logic in the new TargetSelectionMsg. The "closest" SuperCpnSym is determined by just doing a depth first search and linearly ordering all vertices of the entire entrypoint/SuperCpnSym complex, locating the target within this linear order, and then picking the nearest terminal SuperCpnSym within this linear order.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/Mango/Mango/src/mango/worker/msg/OpenDefinitionMsg.java
branches/mango/Mango/src/mango/intro/ConfigurationDetails.java
branches/mango/Mango/src/mango/intro/LoginDialog.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/worker/msg/SelectTargetMsg.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-11 04:30:39
|
Revision: 1903
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1903&view=rev
Author: frankrimlinger
Date: 2009-09-11 04:30:32 +0000 (Fri, 11 Sep 2009)
Log Message:
-----------
Generalized SuperCpnGraphCreateRequestMsg to FowardFlowRequestMsg, which can generate the forward flow from any SuperVertex. This is very handy for visualization of subgraphs. To find the targetable methods, walk the forward flow of the entrypoints graph. The structure of this graph is like so:
PackageSym ...
SuperVertexClassSym
MethodSym
Now for each individual MethodSym, walk its foward flow, structure like so
SuperCpnSym ....
SuperLoopSym
SuperBlowUpSym LoopSym...LoopSym
....
Walk until you get to SuperCpnSym with no outgoing edge to a SuperCpnSym. This is a *terminal* SuperCpnSym. The job of the target selection algorithm is to pick the SuperCpnSym *closest* to some prescribed class or method. Exactly what this means is TBD, but assuming you have picked the target SuperCpnSym, you now do the component survey for jpf like so:
Let F denote the forward flow of the target SuperCpnSym. The correspondence with 1899 is like so
ComponentChoiceGenerator performs breadth-first backward flow on F, from leaves to the target SuperCpnSym, skipping the intermediary SuperBlowUpSym.
PathChoiceGenerator applied to LoopSym graphs
BlowUpChoiceGeneragor applied to SuperLoopSym graphs
MethodChoiceGenerator applied to SuperCpnSym graph.
The terminology leaves much to be desired, but for now not going to change it. Now that the facts on the ground are understood, its time to write the target selection algorithm and the component survey/ComponentChoiceGenerator. Then test this mechanism to make sure you can traverse tricky examples correctly. Then punch in the other choice generators. Finally, you can start working on the internal structure of vertex execution, this is 1892 and companion document.
Wrote the class loopTests.MutualCorecursion to clarify what happens in the case of mutual corecursion. In this case, there is still a single SuperCpnSym, but the most dependent SuperLoopSym has multiple entry points, one for each method of the system. The fact that the SuperCpnSym professes allegiance to a particular one of the two methods is just an artifact. Just don't make unnecessary assumptions about graphs and everything will be fine.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/graph/agent/GraphViewAgent.java
branches/mango/Mango/Mango/src/mango/gumboModel/action/MangoActionManager.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/PackageSym.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/graph/msg/ForwardFlowRequestMsg.java
branches/mango/Mango/mangoUserHome/frank/loopTests/src/loopTests/MutualCorecursion.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/graph/msg/SuperCpnGraphCreateRequestMsg.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-10 21:22:35
|
Revision: 1902
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1902&view=rev
Author: frankrimlinger
Date: 2009-09-10 21:22:13 +0000 (Thu, 10 Sep 2009)
Log Message:
-----------
It turns out there was a EZ bug in MangoInvokeInstruction.getResolvedMethod(). But the TABLESWITCH formal peer was OK. Mango was a little worried about whether or not a single instruction could generate multiple branch conditions for the same destination. This is in fact exactly what TABLESWITCH does in certain cases. So problem was "fixed" by deleting the warning.
However, the LoopGraph (not well named because actually acyclic) generated from a blow up may contain innermost loops, and the problem is that these loops for some reason are not appearing in the loop hierarchy.
OK, what happens here is a little complex. During phase2, the innermost loops are collapsed, then each remaining non-trivial cluster is blown up. Then the flow from each alpha to omega is excised, and the process repeats on each excision. Needless, to say, a fair amount of graph cloning takes place, and the trouble is that the cloned vertices were not inheriting the innermost loop dependency vectors set up by the initial innermost loop collapse.
Fixing this problem is complicated by the fact that the graph cloner uses reflection to create the new vertices, which are not required to be of the same class as those of the input graph. To safely pass the dependency vector when it is appropriate to do so, chose to put a little hack in the bottleneck routine Graph.associatedOutputVertex(). TRICKY: some loops now appear more than once in the dependency graph structure, for example in loopTests.fibonocci. Rather than fight city hall, just be sure to eliminate duplicates from the final dependency vector.
Incidentally, fibonocci is a fine example of mutual co-recursion, so keep testing it as automation proceeds.
YIKES. Inspection of A!_B!_A!_Component_loopTests.nested_blowup.main(I)V reveals that the acyclic graph of a blowup need not be connected. This means in some cases you do cross over connectors when seeking omega. But its ok, because you only cross over to connector entrypoints that are entrypoints of the SAME graph, and this is easily checked.
CORRECTION: the branching logic in 1899 for blowups should read
Do not go down any edge which only leads to a component sink other than omega, unless you are going to connect to an entrypoint of the same component. (All such entrypoints will ultimately lead to omega).
NEXT: Clean up the dependency tree of all entrypoints, starting at the root "Java Code Entrypoints" in order to develop the dependency tree of modules required for target selection.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/graph/msg/Graph2DViewCreateRequestMsg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/SimpleLoopPath.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/vertex/LoopVertex.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-10 16:55:44
|
Revision: 1901
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1901&view=rev
Author: frankrimlinger
Date: 2009-09-10 16:55:36 +0000 (Thu, 10 Sep 2009)
Log Message:
-----------
Wrote code for properly recording the dependency sequence of nested loops. Tests agains rkrug baseline were fine, but testing agains frank/loopTests/nested_blowup uncovered a bug in the TABLESWITCH formal peer. This bug is inherited from MangoBaseline, but only fixing in Mango.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/graph/msg/Graph2DViewCreateRequestMsg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/LoopVertex.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-10 04:19:02
|
Revision: 1900
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1900&view=rev
Author: frankrimlinger
Date: 2009-09-10 04:18:52 +0000 (Thu, 10 Sep 2009)
Log Message:
-----------
BackupAlg and LoopGraph has been marked for alterations needed to construct dependence hierarchy for inner loops. Just write the code. Then address the larger question of module dependence.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-09 17:52:41
|
Revision: 1899
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1899&view=rev
Author: frankrimlinger
Date: 2009-09-09 17:52:35 +0000 (Wed, 09 Sep 2009)
Log Message:
-----------
Throughout this discussion, "method" always means "co-recursive system of methods", which most of the time is just an ordinary method component. In order to implement the logic of 1898, introduced ComponentChoiceGenerator, analogous to TargetChoiceGenerator for the SCANNER. The InvokeRewrite instruction now loads the ComponentChoiceGenerator, which initializes by creating the ComponentSurvey, analogous to the SCANNER CodeSurvey. Also, three different extensions of RewriteChoiceGenerator are introduced: MethodChoiceGenerator, BlowupChoiceGenerator, and LoopChoiceGenerator. A RewriteChoiceGenerator is subordinate to the ComponentChoiceGenerator, just as the BranchChoiceGenerator is subordinate to the TargetChoiceGenerator in the SCANNER.
A crucial design point is that the Vertex and Edge instructions are unaware of the context in which they are executing, be it method, blowup, or loop. So any logic specific to an individual context must be in the corresponding choice generator, NOT the instruction. But this begs the question, how is an instruction to know what kind of ChoiceGenerator to load? Well, since branching logic is quite different depending on the context, this question now has to be reflected back to the current choice generator.
Now the game plays itself. The ComponentSurvey will create a list of components, which are all extensions of Graphic, in order of increasing dependence. To execute a component is simply to install the correct choice generator extension. The LoopChoiceGenerator is for innermost loops modelled by the SimpleLoopPath class. The rest of the components are all LoopGraphs, which may be distinguished by whether or not the alphaSym field is defined. The BlowUpChoiceGenerator is for all LoopGraphs with defined alphaSym, and the balance are for MethodChoiceGenerator. The set of most dependent components corresponds exactly to this balance, and consist of a single LoopGraph except possible in the case of mutually co-recursive methods.
With the seed ChoiceGenerator in place, execution of instructions commences, and subsequent choice generators will be of the same type.
The branching logic for the choice generators is like so:
PathChoiceGenerator: trivial, just execute the path and specify the loop when you get to the end.
BlowUpChoiceGenerator: Execute starting at the alpha vertex. Do not go down any edge which only leads to a component sink other than omega. Each time you get to omega, specify a case of the loop. When all paths to the loop are specified, complete the loop specification.
MethodChoiceGenerator: Execute starting at each entrance. Do not go down any path that leads only to an alpha vertex. (Its ok to cross an omega vertex, you just pick up the loop transformer as part of your predicate transformation.) When you get to a component sink, follow all connectors. If you get to a sink with no connectors, specify the case. When you specify the last case, complete the method specification.
NB: the "unravelling predicate transformers" document is still in force, as it deals mostly with events that take place during instruction execution. This note deals what takes place before and after execution. Some of the responsibilities in this note may actually be performed by listeners, this is mostly a matter of convenience.
TODO: finish the target selection algorithm, and then implement this note and unravelling pred transformers. Then lots of testing.
Modified Paths:
--------------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/InvokeRewriter.java
Added Paths:
-----------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/BlowupChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/ComponentChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/LoopChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MethodChoiceGenerator.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-09 04:52:52
|
Revision: 1898
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1898&view=rev
Author: frankrimlinger
Date: 2009-09-09 04:52:43 +0000 (Wed, 09 Sep 2009)
Log Message:
-----------
Blowups introduce an interesting complication. A blowup component has two special vertices, alpha and omega. Every path from alpha to omega is a case of the blown up loop. What stratification buys you in MangoBasline is a means of detecting and bundling all these cases into a single predicate transformer, which the rewriter must then disentangle. But in Mango, jpf is supposed to be in charge.
Mathematically, the "methods" and "loops" dichotomy is unnatural. The natural object is the component graph, and the issue is to compute universal connector predicate transformers at component sources in terms of the place-holders at component sinks. This is the function that stratification performed at a high level of abstraction, without actually interpreting the individual instructions. The rewriter then had to struggle heroically to open up interpretations in a sensible order in order to give the user some hope of understanding and moderating the process.
The rewriter is now relieved of this responsibility, but now it falls to jpf to execute the paths in an order that makes sense to the user. The really nice thing about this is that jpf is on the outside looking in, and gets to see the whole graph at once, whereas the rewriter is unable to see the forest for the trees.
So what exactly is the "looking from the outside in" algorithm. First, component sources are categorized as
method entrypoint
component entrypoint
alpha
Component sinks are categorized as
method exit
component exit
omega
In this context, innermost loop graphs are just linear graphs beginning with alpha and ending with omega. The loop subdivision algorithm makes the following guarantees:
1. A component either has exactly one alpha and one omega vertex, or it has no alpha or omega vertex.
2. No edge enters alpha, no edge leaves omega.
3. A "connector" entering a component entrypoint has its source in a more dependent component. Likewise, an connector exiting a component exit has a destination is a less dependent graph. In otherwise, the "total graph" of subgraphs and connectors is acyclic.
4. The paths from an alpha to an omega within the total graph are actually contained within the component containing alpha and omega, and constitute the case of the corresponding loop.
5. Now consider the quotient of the total graph obtained by identifying alpha and omega pairs. The paths in this graph from method entrypoint to method exit points which contain no loop case are the cases for the method. Such a path will contain an alpha-omega vertex exactly once or not at all (i.e. because the loop is inside another loop). Likewise, the paths from alpha-omega to itself which comprise the loop cases will meet other alpha-omega vertices exactly once or not at all. The predicate transformer for the alpha-omega vertex is the recursive function corresponding to the loop, which must be punched in when executing a path through alpha-omega for some less dependent loop or method.
Having stated these facts, the algorithm for jpf is now clear.
1. get a most dependent component containing an alpha omega pair, if none, go to 4
2. execute the paths from alpha to omega, and specify the loop.
3. go to 1
4. execute the paths from method entrypoint to method exit points, crossing over connectors as needed. At this point, jpf no longer needs to respect the component boundaries. When all paths are specified, on to the next method.
One final point, in full generality, method must be replaced by "co-recursive system of methods" and in this context there could be multiple entry points.
OK, need to sleep on this and do some engineering to get jpf up to speed on the search strategy and the various activities that must occur at the special times.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/graph/data/supervertex/SuperLoopData.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperLoopSym.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-08 20:28:15
|
Revision: 1897
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1897&view=rev
Author: frankrimlinger
Date: 2009-09-08 20:28:07 +0000 (Tue, 08 Sep 2009)
Log Message:
-----------
Before continuing with the predicate unravelling business, decided to take the hit and get target selection working. This involves walking the dependency diagram of modules, which is a subject that hasn't been visited in years. Wrote a new command to display the relevant graph, and discovered that loops formed inside of blowups were not appearing. Traced the problem to AlphaSym call to HitemUtil.seekLoopSym, which somehow relies on stratification to perform its function. Since stratification is no long available, need to rework this.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/graph/agent/GraphViewAgent.java
branches/mango/Mango/Mango/src/mango/gumboModel/ColorDataBinding.java
branches/mango/Mango/Mango/src/mango/gumboModel/action/MangoActionManager.java
branches/mango/Mango/Mango/src/mango/gumboModel/factory/GraphModelFactory.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hitem.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/Graph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/GraphicSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/MethodSym.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/graphic/VertexSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperBlowUpSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperCpnSym.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/AlphaSym.java
branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/Mango/Mango/src/mango/worker/msg/OpenDefinitionMsg.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/graph/data/supervertex/PackageData.java
branches/mango/Mango/Mango/src/mango/graph/data/supervertex/SuperClassData.java
branches/mango/Mango/Mango/src/mango/graph/msg/SuperCpnGraphCreateRequestMsg.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/worker/msg/GenerateSpecificationMsg.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-08 03:54:46
|
Revision: 1896
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1896&view=rev
Author: frankrimlinger
Date: 2009-09-08 03:54:39 +0000 (Tue, 08 Sep 2009)
Log Message:
-----------
Debugged some wiring, and now the JPFREWRITER thread will go to sleep and let the SESSION thread kick in with HarvestChoiceCommand, for the first Vertex instruction. Now need some rules so the harvest can do its thing.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/module/definition/loop/msg/LoopDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MangoAnnotation.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteListener.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/msg/HarvestChoiceCmd.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Graphic.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/trap/HarvestChoiceTrap.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-07 04:09:07
|
Revision: 1895
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1895&view=rev
Author: frankrimlinger
Date: 2009-09-07 04:08:57 +0000 (Mon, 07 Sep 2009)
Log Message:
-----------
Refined the design for unravelling predicate transformers, and completed all the high-level wiring for jpf interface. It remains to write HarvestChoiceCmd, InstantiateFreeChoiceCmd, and SpecifyCaseCmd, and associated traps and rules.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/loop/msg/LoopDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/method/MethodDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashRewriter.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/TrapCommand.java
branches/mango/Mango/doc/unravelling predicate transfomers.rtf
branches/mango/Mango/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_rewriter_RewriterMJI.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MangoAnnotation.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteListener.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/sym/HarvestChoiceSym.java
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/RewriteInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
Added Paths:
-----------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/FreeAssumption.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/InplaceChoice.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/OutboundChoice.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/msg/
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/msg/HarvestChoiceCmd.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/msg/InstantiateFreeChoiceCmd.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/msg/SpecifyCaseCmd.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/trap/
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/trap/HarvestChoiceTrap.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/PriorityScheduleRequestMsg.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteChoice.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
