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: <fra...@us...> - 2009-06-17 14:45:59
|
Revision: 1638
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1638&view=rev
Author: frankrimlinger
Date: 2009-06-17 14:45:41 +0000 (Wed, 17 Jun 2009)
Log Message:
-----------
Fixing SVN mistake, have to create the java project for marc first and then "share" it.
Removed Paths:
-------------
branches/mango/MangoJPF/mangoUserHome/marc/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-17 14:35:04
|
Revision: 1637
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1637&view=rev
Author: frankrimlinger
Date: 2009-06-17 14:35:02 +0000 (Wed, 17 Jun 2009)
Log Message:
-----------
The idea that jpf was not loading exception tables is wrong. These tables only apply to checked exceptions thrown by a method, which is not the situation I am in. So the immediate problem of dropped exception branch conditions lies elsewhere. To address this whole issue more systematically, have reinstanted Marc's exception handler tests, which for the most part are taken from the old IBM jikes test suite.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
Added Paths:
-----------
branches/mango/MangoJPF/mangoUserHome/marc/
branches/mango/MangoJPF/mangoUserHome/marc/arrayCopyShell/
branches/mango/MangoJPF/mangoUserHome/marc/arrayCopyShell/src/
branches/mango/MangoJPF/mangoUserHome/marc/arrayCopyShell/src/arrayCopyShell.java
branches/mango/MangoJPF/mangoUserHome/marc/hypo2/
branches/mango/MangoJPF/mangoUserHome/marc/hypo2/src/
branches/mango/MangoJPF/mangoUserHome/marc/hypo2/src/hypo2.java
branches/mango/MangoJPF/mangoUserHome/marc/lptry1/
branches/mango/MangoJPF/mangoUserHome/marc/lptry1/lptry1.java
branches/mango/MangoJPF/mangoUserHome/marc/lptry2/
branches/mango/MangoJPF/mangoUserHome/marc/lptry2/src/
branches/mango/MangoJPF/mangoUserHome/marc/lptry2/src/lptry2.java
branches/mango/MangoJPF/mangoUserHome/marc/try1/
branches/mango/MangoJPF/mangoUserHome/marc/try1/try1.java
branches/mango/MangoJPF/mangoUserHome/marc/try2/
branches/mango/MangoJPF/mangoUserHome/marc/try2/try2.java
branches/mango/MangoJPF/mangoUserHome/marc/try3/
branches/mango/MangoJPF/mangoUserHome/marc/try3/try3.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk1/
branches/mango/MangoJPF/mangoUserHome/marc/trychk1/trychk1.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk2/
branches/mango/MangoJPF/mangoUserHome/marc/trychk2/trychk2.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk3/
branches/mango/MangoJPF/mangoUserHome/marc/trychk3/trychk3.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk6/
branches/mango/MangoJPF/mangoUserHome/marc/trychk6/trychk6.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk7/
branches/mango/MangoJPF/mangoUserHome/marc/trychk7/trychk7.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk8/
branches/mango/MangoJPF/mangoUserHome/marc/trychk8/trychk8.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-17 02:15:57
|
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.
|
|
From: <pcm...@us...> - 2009-06-16 19:56:53
|
Revision: 1635
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1635&view=rev
Author: pcmehlitz
Date: 2009-06-16 19:56:46 +0000 (Tue, 16 Jun 2009)
Log Message:
-----------
* leftover 'defaults' ref in the - now flattened - Config
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/Config.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-16 16:08:36
|
Revision: 1634
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1634&view=rev
Author: frankrimlinger
Date: 2009-06-16 16:08:34 +0000 (Tue, 16 Jun 2009)
Log Message:
-----------
Added ACL2 folder for development of strategies for Mango proof artifacts.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
Added Paths:
-----------
branches/mango/MangoJPF/ACL2/
branches/mango/MangoJPF/ACL2/itsAWrap-construct.lisp
branches/mango/MangoJPF/ACL2/itsAWrap-construct.lisp.a2s
branches/mango/MangoJPF/ACL2/mango-model.lisp
branches/mango/MangoJPF/ACL2/mango-model.lisp.a2s
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-16 05:12:08
|
Revision: 1633
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1633&view=rev
Author: frankrimlinger
Date: 2009-06-16 05:12:07 +0000 (Tue, 16 Jun 2009)
Log Message:
-----------
Got rid of the lineNumber==-1 hack for synthetic instructions. This was useful to get up and running but now need a genuine implementation.
SyntheticInstructions now must implement getSyntheticPosition(), and should throw IllegalStateException if getPosition() or getOffset() is called. This is so we can hunt down all the places that a synthetic position is used and make sure the supplied implementations make sense.
BadPlace, OSplace, and AbstractUconPlace all return 0 for the synthetic position.
ATHROWCREATOR and ACATCHHANDLER getSyntheticPosition() returns the position of the parent instruction. This is necessary for correct propagation of context. In the case of ATHROWCREATOR, the parent is an ATHROW. In the case of ACATCHHANDLER, on of INVOKEINTERFACE, INVOKESPECIAL, INVOKESTATIC, or INVOKEVIRTUAL.
ATHROWHANDLER returns a synthetic position of 0. We take the point of view that only parameters have context in a handler.
Punched in various patches to call getSyntheticPosition as appropriate.
With all this in place, no effect on the itsAWrap.main context bug. But certainly I am on the right track.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalInterface.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/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
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-06-16 05:11:46
|
Revision: 1632
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1632&view=rev
Author: staats
Date: 2009-06-16 05:11:45 +0000 (Tue, 16 Jun 2009)
Log Message:
-----------
Added Paths:
-----------
trunk/extensions/complexcoverage/bin/jpf-parallel-client
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-06-16 01:24:48
|
Revision: 1631
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1631&view=rev
Author: staats
Date: 2009-06-16 00:17:15 +0000 (Tue, 16 Jun 2009)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/JPFManager.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/JPFManagerInterface.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/RemoteJPF.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/StartJPFManager.java
Added Paths:
-----------
trunk/extensions/complexcoverage/launch/CompCov BinTree Symbolic.launch
trunk/extensions/complexcoverage/launch/CompCov BinomialHeap Symbolic.launch
trunk/extensions/complexcoverage/launch/CompCov DoubleTest Normal.launch
trunk/extensions/complexcoverage/launch/CompCov FibHeap Symbolic.launch
trunk/extensions/complexcoverage/launch/CompCov MultiProcess JPF.launch
trunk/extensions/complexcoverage/launch/CompCov Parallel Client.launch
trunk/extensions/complexcoverage/launch/CompCov Parallel Manager Testfile.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun Measure Reduced.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun Normal.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun Reduce.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun Run Reduced Test #0.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun SimpleCoverage.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun Symbolic.launch
trunk/extensions/complexcoverage/launch/CompCov TreeMap Symbolic.launch
Removed Paths:
-------------
trunk/extensions/complexcoverage/launch/ComplexCoverage BinTree Symbolic.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage BinomialHeap Symbolic.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage DoubleTest Normal.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage FibHeap Symbolic.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage MultiProcess JPF.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TestFun Measure Reduced.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TestFun Normal.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TestFun Reduce.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TestFun Run Reduced Test #0.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TestFun SimpleCoverage.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TestFun Symbolic.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TreeMap Symbolic.launch
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-15 19:15:48
|
Revision: 1630
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1630&view=rev
Author: frankrimlinger
Date: 2009-06-15 18:04:38 +0000 (Mon, 15 Jun 2009)
Log Message:
-----------
Finally traced the invariant bug in the case of incorrect context. This was a pretty terrifying bug. It actually occurs in JavaType.getJavaTypeName(), which was incorrectly translated from C++. Specifically, the local variable name "LocalVar_at_offset_1_lineNumber_0", indicating unknown context, was interpreted incorrectly as a class name X, in the Lx; syntax, because we forgot to check for the ";". The bogus type returned was "LocalVar_at_offset_1_lineNumber_0", and then InequivalentRef.inequivalentJavaType() made a "risky" comparison which decide that InequivalentRef.inequivalentJavaType() and "int" were in-equivalent types. This erroneous result in turn allowed HeapModel.totalVacuumService() to garbage collect the heap, which in turn allowed InvariantAgentTest to return a positive result for invariant detection. YIKES!
FWIW, the risky comparison was reported in the log window and the console, and I have been systematically ignoring it for about a week now. So now the warning is much more angry sounding, in the hopes that it will get my attention in the future.
Fixed getJavaTypeName() to check for the ";" before returning a class name, in both Mango and MangoJPF.
With this fix in place, invariant detection operates correctly, so that the conjecture x[5]==x[6] is produced with respect to the itsAWrap loop output heap.
However, can't finish rewriting itsAWrap.main() because get non-deterministic result as the ArrayIndexOutOfBoundsException and NullPointerException don't vanish as they should. This is a known bug that I will get to soon.
FIRST, really need to fix the incorrect context bug, as it leads to unsatisfactory output in the specification window. This is a thankless task as the code will go away with jpf integration, but must establish a baseline.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/module/msg/DebugInvariantsMsg.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentRef.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/JavaType.java
branches/mango/MangoJPF/Mango/src/mango/module/msg/DebugInvariantsMsg.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentRef.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/events/RewriteEvent.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/ValueHAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/BaseInvariantAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/InvariantTestAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/model/JavaType.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-15 16:22:40
|
Revision: 1629
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1629&view=rev
Author: frankrimlinger
Date: 2009-06-15 16:19:48 +0000 (Mon, 15 Jun 2009)
Log Message:
-----------
Verified that the incorrectly detect invariant in the InvariantTestAgent is "caused" by the wrong context supplied for the computation. The corresponding context free computation does not yield an invariant. Several observations need to be made here:
1. This mechanism will be entirely redesigned with jpf backtracking supplying context, so at this point we just need to hack out a temporary solution.
2. If we don't supply context, then certain issues, like heap reference temporal logic, can't do their thing. So we need to figure out why the context is wrong in the first place and at least get parity between Mango and MangoJPF.
3. But more than that, we need to find out exactly why the wrong context is leading to the incorrect result. More than likely this is a rewriter bug in its own right that needs to be fixed even for the version which is to come.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/InvariantTestAgent.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <sb...@us...> - 2009-06-15 13:24:37
|
Revision: 1628
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1628&view=rev
Author: sbadame
Date: 2009-06-15 13:24:31 +0000 (Mon, 15 Jun 2009)
Log Message:
-----------
Double quotes no longer surround the paths in execution.
Modified Paths:
--------------
trunk/ide/netbeans/RunJPF/src/gov/nasa/runjpf/RunJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-15 12:03:01
|
Revision: 1627
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1627&view=rev
Author: frankrimlinger
Date: 2009-06-15 12:01:59 +0000 (Mon, 15 Jun 2009)
Log Message:
-----------
still working on invariant bug
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleInvocationSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/BaseInvariantAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/InvariantTestAgent.java
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-14 19:28:34
|
Revision: 1626
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1626&view=rev
Author: frankrimlinger
Date: 2009-06-14 19:28:28 +0000 (Sun, 14 Jun 2009)
Log Message:
-----------
Investigation of the itsAWrap.main invariant bug continues. Have verified that the context free input state for the invocation of itsAWrap.clear is the same in Mango and MangoJPF. However, the input state for MangoJPF is slightly confused. If in fact this is causing the problem, then there is a very unhealthy dependence on context in the invariant mechanism that needs to be fixed. Currently comparing invariant detection success in Mango versus MangoJPF to try and discover exactly when the invariant mechanism gets confused.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/module/msg/DebugInvariantsMsg.java
branches/mango/Mango/Mango/src/mango/worker/Mango.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/Sym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/ConditionalMethodAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/InvariantAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/InvariantHypoAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/LocalVarConditionalEquivalenceAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/MethodInvariantAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/model/InvariantModel.java
branches/mango/MangoJPF/Mango/src/mango/module/msg/DebugInvariantsMsg.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/form/binder/LocalVarBind.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/sym/Sym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/binder/executable/LocalVarSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/ConditionalMethodAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/InvariantAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/InvariantHypoAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/LocalVarConditionalEquivalenceAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/MethodInvariantAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/model/InvariantModel.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AbstractUconPlace.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-14 03:43:43
|
Revision: 1625
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1625&view=rev
Author: frankrimlinger
Date: 2009-06-14 03:43:42 +0000 (Sun, 14 Jun 2009)
Log Message:
-----------
the acatchhandlers are somehow goofed up, don't seem to be getting the branch conditions. Getting a non-deterministic predicate transformer. This bug is an old friend, probably not hard to fix.
But something much more troubling is happening.
Setting up the expression (valueH (refH x 5) heap), where heap is the output loop heap, we observe that the rule "valueH invariance" fires in MangoJPF, reducing the expression to
(valueH (refH x 5) inputHeap)
In Mango, no invariant rule fires, and the expression is unchanged.
It seems very unlikely that there really is an issue in the invariant mechanism. Some initial condition must be getting garbled. Still, this is the place to start. Find out why the "valueh invariance" rule is getting confused.
Modified Paths:
--------------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-13 22:16:32
|
Revision: 1624
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1624&view=rev
Author: frankrimlinger
Date: 2009-06-13 22:15:54 +0000 (Sat, 13 Jun 2009)
Log Message:
-----------
Fixed two bugs: The "fake methods" bad method, abstraction ucon method, and OSmethod were not being modelled, and the routine hasMangoModel was returning false when passed these methods. This set in motion a sequence of events with the unhappy result that clear() never gets invoked by main(). The cause was again just the result of code that got shifted around during the port to MangoJPF.
With this fix, observed the correct stratification and component graph for itsAWrap.main.
Unfortunately, itsAWrap.main is still exhibiting the original problem, that is x[5] and x[6] are not functions of loop output heap. However, the loop output heap does appear as the itsAWrap.main output heap.
So, something else is going on here.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/edge/Edge.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-13 16:10:55
|
Revision: 1623
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1623&view=rev
Author: frankrimlinger
Date: 2009-06-13 16:10:53 +0000 (Sat, 13 Jun 2009)
Log Message:
-----------
Fixed minor bug in INVOKECLINIT.
Working on itsAWrap.main bug. The problem is basic, in that the clear routine is never invoked. The stratification differs from that of Mango, so this is the place to start.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
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/bytecode/INVOKECLINIT.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-06-12 21:21:12
|
Revision: 1622
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1622&view=rev
Author: staats
Date: 2009-06-12 21:19:42 +0000 (Fri, 12 Jun 2009)
Log Message:
-----------
Added Paths:
-----------
trunk/extensions/complexcoverage/bin/
trunk/extensions/complexcoverage/bin/jpf-parallel-server
trunk/extensions/complexcoverage/bin/wideopen.policy
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-06-12 20:52:31
|
Revision: 1621
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1621&view=rev
Author: staats
Date: 2009-06-12 20:51:35 +0000 (Fri, 12 Jun 2009)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/StartJPFManager.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-06-12 20:50:00
|
Revision: 1620
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1620&view=rev
Author: staats
Date: 2009-06-12 20:48:40 +0000 (Fri, 12 Jun 2009)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/StartJPFManager.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-06-12 20:18:35
|
Revision: 1619
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1619&view=rev
Author: staats
Date: 2009-06-12 20:18:32 +0000 (Fri, 12 Jun 2009)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/JPFManager.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/JPFManagerInterface.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/RemoteJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-12 19:20:26
|
Revision: 1618
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1618&view=rev
Author: frankrimlinger
Date: 2009-06-12 19:19:55 +0000 (Fri, 12 Jun 2009)
Log Message:
-----------
Added dirty session save to quit handler.
Wired in the new HasCommutingClinit rule to the corresponding action to fix rewriting problem in ItsAWrap.main(). But this only works because ItsAWrap does not trigger any clinit invocation. To handle the problem more generally, introduced preference to suppress clinit invocation. This in itself does not cause unsoundness. What is unsound is to introduce rules to resolve references to non-final static fields in an ad-hoc manner. When this issue comes up, we can turn off the preference and implement the rest of the new clinit mechanism.
Specifically, the rule HasCommutingClinit just returns (dualp 'f) if the "Suppress clinit invocation" preference is on. For now, we leave this turned off.
Next bug, ItsAWrap.main thinks x[5] and x[6] are loop invariant. Technically, this is true, but shouldn't be able to know this. YIKES!
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/clinit/HasCommutingClinit.java
branches/mango/MangoJPF/Mango/src/mango/script/model/MangoScriptModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/src/mango/preferences/GeneralPreferencePage.java
Added Paths:
-----------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
Removed Paths:
-------------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/baseline/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-06-12 18:44:55
|
Revision: 1617
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1617&view=rev
Author: staats
Date: 2009-06-12 18:44:32 +0000 (Fri, 12 Jun 2009)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TestFile.java
Added Paths:
-----------
trunk/extensions/complexcoverage/launch/
trunk/extensions/complexcoverage/launch/ComplexCoverage BinTree Symbolic.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage BinomialHeap Symbolic.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage DoubleTest Normal.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage FibHeap Symbolic.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage MultiProcess JPF.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TestFun Measure Reduced.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TestFun Normal.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TestFun Reduce.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TestFun Run Reduced Test #0.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TestFun SimpleCoverage.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TestFun Symbolic.launch
trunk/extensions/complexcoverage/launch/ComplexCoverage TreeMap Symbolic.launch
Removed Paths:
-------------
trunk/extensions/complexcoverage/test/ComplexCoverage BinTree Symbolic.launch
trunk/extensions/complexcoverage/test/ComplexCoverage BinomialHeap Symbolic.launch
trunk/extensions/complexcoverage/test/ComplexCoverage DoubleTest Normal.launch
trunk/extensions/complexcoverage/test/ComplexCoverage FibHeap Symbolic.launch
trunk/extensions/complexcoverage/test/ComplexCoverage MultiProcess JPF.launch
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun Measure Reduced.launch
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun Normal.launch
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun Reduce.launch
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun Run Reduced Test #0.launch
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun SimpleCoverage.launch
trunk/extensions/complexcoverage/test/ComplexCoverage TestFun Symbolic.launch
trunk/extensions/complexcoverage/test/ComplexCoverage TreeMap Symbolic.launch
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-12 18:06:25
|
Revision: 1616
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1616&view=rev
Author: frankrimlinger
Date: 2009-06-12 18:06:21 +0000 (Fri, 12 Jun 2009)
Log Message:
-----------
Reinstated clear on reset for Entrypoints window and Session window.
Generated MangoJPF session for ItsAWrap. clear.
Fixed a rewriting bug in ItsAWrap.main. The bizarre pop2 instruction can only resolve whether it is supposed to pop one or two values during rewriting. For this purpose, the pop2 rulekey was introduced. Unfortunately, many instructions use a local variable pop2 when building the formal peer, and the distinction got confused in MangoJPF. To fix this problem,
1. refactored pop2 to pop2Wide in both Mango and MangoJPF
2. revised rulebase accordingly, in both Mango and MangoJPF
3. fixed the broken rules in MangoJPF. This were easy to find because pop2Wide only occurs in the POP2 formal peer. All the other instances changed to the local variable pop2.
I do remember deleting those pop2 locals now in MangoJPF because they were "not being used". The whole issue came about because when porting to the javapathfinder-mango-bridge, the inheritance structure changed so that references to rulekeys had to be made more explicit. TRICKY!
As an afterthought, this experience shows that making expressions with empty argument lists a syntax error is a good idea after all. Otherwise this error could have taken a long time to diagnose. Checking the syntax of formal peer expresssions with the new MangoInstructionFactory.sanityTest() creates no discernible overhead, and so this feature will be left on.
Next bug: callThisClinit fails to resolve during call to clear() in ItsAWrap.main. No surprise here, as the clinit plumbing has been completely reworked for MangoJPF.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java
branches/mango/Mango/Mango/src/mango/worker/javaModel/byteCodeModel/PopDupSwap.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/META-INF/MangoJPF.product
branches/mango/MangoJPF/Mango/src/mango/worker/GlobalViewModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/Cons.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java
branches/mango/MangoJPF/ThreadSupport/src/threadModel/SystemBuilder.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalInterface.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/length of the Array 'x' is greater than or equal to 10.zip
branches/mango/MangoJPF/src/mango/views/GlobalViewWindow.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-12 03:27:07
|
Revision: 1615
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1615&view=rev
Author: frankrimlinger
Date: 2009-06-12 03:27:03 +0000 (Fri, 12 Jun 2009)
Log Message:
-----------
Solved the MangoJPF rewriter bug. The trouble was I decided that "manual block mode" had not been used in years and so could be dropped from support in the MangoJPF gui. Since this broke some code, I just happily deleted all code that referred to the corresponding boolean flag. But the devil came knocking at my door. Because UnifyEvent calls isManuallyBlocked, which calls manualBlockMode(), which in Mango always returns false. This causes isManuallyBlocked to return false. Trouble is, pulling this code out of MangoJPF just caused control flow to go on to the rest of the routine. The idea is that when manual block mode is on, UconSym and PathSym won't interpret. This was helpful long ago when debugging certain composition issues. But now it just stops the rewriter dead in its tracks.
How it could possibly be that this failure mode did not occur while rewriting the ItsAWrap loop is a tremendous mystery that will never be investigated.
To solve the problem, just reinstated manualBlockMode(), so that it always returns false, and restored calls to this routine. This way, if I ever *want* this feature again, the hook is in place.
Anticipating other damage caused by the initial reckless act, also reinstated semiAutoBlockMode() and autoBlockMode. In Mango, all three of these routines always return false, because the actual flag is an unblockStateCode_t that is always null, as it was never hooked up to the vestigial gui.
There were no calls to semiAutoBlockMode() in Mango, so no harm no foul. The calls to autoBlockMode() have been reinstated.
In the legacy code, semiAutoBlockMode is the default, so even though it is never called, it returns true in MangoJPF. manualBlockMode and autoBlockMode return false.
Lesson learned: A firm grasp of what is view and what is model is essential to success. Happily, with these repairs in place, the initial rewritten predicate transformer for ItsAWrap.clear looks good. So, onward.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/engine/unifier/UnifyEvent.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/simpleSubstitution/SUBRautomatic.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/sym/InterpretableSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/unifier/UnifyEvent.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-06-11 23:52:19
|
Revision: 1614
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1614&view=rev
Author: staats
Date: 2009-06-11 23:52:17 +0000 (Thu, 11 Jun 2009)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/JPFManager.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/JPFManagerInterface.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/MultiJPFListener.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/RemoteJPF.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/StartJPFManager.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/multicore/JPFProcess.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/multicore/MultiProcessJPF.java
trunk/extensions/complexcoverage/test/ComplexCoverage MultiProcess JPF.launch
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TestFile.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
