Menu
▾
▴
javapathfinder-svn
|
From: <fra...@us...> - 2009-04-16 14:15:54
|
Revision: 1408
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1408&view=rev
Author: frankrimlinger
Date: 2009-04-16 14:15:46 +0000 (Thu, 16 Apr 2009)
Log Message:
-----------
Cleaning out the MangoRPF plugin repository for a fresh start. This repository is supposed to contain plugins, but somehow has been filled up with unjarred classes. This is goofy. Discovered there is no problem loading jpf classes as such, but realized that the jpf classes won't load without the jars they depend on. These are listed in the java build path for the trunk. (There is also a Xerces zip file which I repackaged as a jar.) The MangoRPF product needs to have these jars bundled into a plugin and deposited in its plugin repository. But, I suspect that the "jar plugin project" tries to resolve inconsistencies as it creates the bundled jar. This causes trouble when there are a lot of jars. In any case, I am unable to bundle all the required jars in a single plugin using jar plugin project. So, attempting to just bundle a few at a time. Also, need to create a new configuration item for the location of the jpf .properties file.
Modified Paths:
--------------
branches/mango/MangoJPF/META-INF/MANIFEST.MF
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
Removed Paths:
-------------
branches/mango/MangoJPF/repository/plugins/Array1$A.class
branches/mango/MangoJPF/repository/plugins/Array1$B.class
branches/mango/MangoJPF/repository/plugins/Array1.class
branches/mango/MangoJPF/repository/plugins/Array1.es
branches/mango/MangoJPF/repository/plugins/Completion1$A.class
branches/mango/MangoJPF/repository/plugins/Completion1$B.class
branches/mango/MangoJPF/repository/plugins/Completion1.class
branches/mango/MangoJPF/repository/plugins/Completion1.es
branches/mango/MangoJPF/repository/plugins/CompletionSend$A.class
branches/mango/MangoJPF/repository/plugins/CompletionSend$B.class
branches/mango/MangoJPF/repository/plugins/CompletionSend$C.class
branches/mango/MangoJPF/repository/plugins/CompletionSend.class
branches/mango/MangoJPF/repository/plugins/CompletionSend.es
branches/mango/MangoJPF/repository/plugins/ExampleAbort$Failure.class
branches/mango/MangoJPF/repository/plugins/ExampleAbort.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active$Busy.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active$Connecting.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active$DialTone.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active$Dialing$Receive.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active$Dialing$Send.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active$Dialing$Wait.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active$Dialing.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active$Invalid.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active$Pinned.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active$Ringing.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active$Talking.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active$Timeout.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Active.class
branches/mango/MangoJPF/repository/plugins/FixedPhone$Idle.class
branches/mango/MangoJPF/repository/plugins/FixedPhone.class
branches/mango/MangoJPF/repository/plugins/FixedPhone.es
branches/mango/MangoJPF/repository/plugins/FixedPhone.graffle
branches/mango/MangoJPF/repository/plugins/FixedPhone.pdf
branches/mango/MangoJPF/repository/plugins/FixedPhone.png
branches/mango/MangoJPF/repository/plugins/KeepAlive$A.class
branches/mango/MangoJPF/repository/plugins/KeepAlive$B.class
branches/mango/MangoJPF/repository/plugins/KeepAlive.class
branches/mango/MangoJPF/repository/plugins/Logger.class
branches/mango/MangoJPF/repository/plugins/META-INF/
branches/mango/MangoJPF/repository/plugins/MultipleToplevels.class
branches/mango/MangoJPF/repository/plugins/MyClass1.class
branches/mango/MangoJPF/repository/plugins/MyClass2.class
branches/mango/MangoJPF/repository/plugins/MyClassFP.class
branches/mango/MangoJPF/repository/plugins/MyClassWithFields.class
branches/mango/MangoJPF/repository/plugins/MyDriver1.class
branches/mango/MangoJPF/repository/plugins/MyDriverForFields.class
branches/mango/MangoJPF/repository/plugins/OSGI-INF/
branches/mango/MangoJPF/repository/plugins/Option.class
branches/mango/MangoJPF/repository/plugins/Ortho1$S1.class
branches/mango/MangoJPF/repository/plugins/Ortho1$S2$A1.class
branches/mango/MangoJPF/repository/plugins/Ortho1$S2$A2.class
branches/mango/MangoJPF/repository/plugins/Ortho1$S2$B1.class
branches/mango/MangoJPF/repository/plugins/Ortho1$S2$B2.class
branches/mango/MangoJPF/repository/plugins/Ortho1$S2.class
branches/mango/MangoJPF/repository/plugins/Ortho1$S3.class
branches/mango/MangoJPF/repository/plugins/Ortho1.class
branches/mango/MangoJPF/repository/plugins/Ortho1.es
branches/mango/MangoJPF/repository/plugins/Ortho1.graffle
branches/mango/MangoJPF/repository/plugins/Ortho1.pdf
branches/mango/MangoJPF/repository/plugins/POGO.class
branches/mango/MangoJPF/repository/plugins/PrioritySend$A$B.class
branches/mango/MangoJPF/repository/plugins/PrioritySend$A.class
branches/mango/MangoJPF/repository/plugins/PrioritySend.class
branches/mango/MangoJPF/repository/plugins/PrioritySend.es
branches/mango/MangoJPF/repository/plugins/PrioritySendRegions$R1.class
branches/mango/MangoJPF/repository/plugins/PrioritySendRegions$R2.class
branches/mango/MangoJPF/repository/plugins/PrioritySendRegions.class
branches/mango/MangoJPF/repository/plugins/PropertyTEST1.class
branches/mango/MangoJPF/repository/plugins/RATS.class
branches/mango/MangoJPF/repository/plugins/RCAT.class
branches/mango/MangoJPF/repository/plugins/ReceiverConstraints$A.class
branches/mango/MangoJPF/repository/plugins/ReceiverConstraints$B.class
branches/mango/MangoJPF/repository/plugins/ReceiverConstraints.class
branches/mango/MangoJPF/repository/plugins/ReceiverConstraints.es
branches/mango/MangoJPF/repository/plugins/Repeat.es
branches/mango/MangoJPF/repository/plugins/Repeater$A.class
branches/mango/MangoJPF/repository/plugins/Repeater.class
branches/mango/MangoJPF/repository/plugins/Robot.class
branches/mango/MangoJPF/repository/plugins/RobotManager$ListModel.class
branches/mango/MangoJPF/repository/plugins/RobotManager-nothread-console.jpf
branches/mango/MangoJPF/repository/plugins/RobotManager-nothread.es
branches/mango/MangoJPF/repository/plugins/RobotManager-nothread.jpf
branches/mango/MangoJPF/repository/plugins/RobotManager-thread-console.jpf
branches/mango/MangoJPF/repository/plugins/RobotManager-thread.es
branches/mango/MangoJPF/repository/plugins/RobotManager-thread1.jpf
branches/mango/MangoJPF/repository/plugins/RobotManager-thread2.jpf
branches/mango/MangoJPF/repository/plugins/RobotManager-thread3.jpf
branches/mango/MangoJPF/repository/plugins/RobotManager-thread4.jpf
branches/mango/MangoJPF/repository/plugins/RobotManager.class
branches/mango/MangoJPF/repository/plugins/RobotManagerView$1.class
branches/mango/MangoJPF/repository/plugins/RobotManagerView$2.class
branches/mango/MangoJPF/repository/plugins/RobotManagerView$3.class
branches/mango/MangoJPF/repository/plugins/RobotManagerView$4.class
branches/mango/MangoJPF/repository/plugins/RobotManagerView$5.class
branches/mango/MangoJPF/repository/plugins/RobotManagerView$6.class
branches/mango/MangoJPF/repository/plugins/RobotManagerView$RobotCellRenderer.class
branches/mango/MangoJPF/repository/plugins/RobotManagerView.class
branches/mango/MangoJPF/repository/plugins/RobotStatusAcquisitionThread.class
branches/mango/MangoJPF/repository/plugins/RunAnt.class
branches/mango/MangoJPF/repository/plugins/RunJPF.class
branches/mango/MangoJPF/repository/plugins/RunTool.class
branches/mango/MangoJPF/repository/plugins/SecondToplevel$A.class
branches/mango/MangoJPF/repository/plugins/SecondToplevel$B.class
branches/mango/MangoJPF/repository/plugins/SecondToplevel.class
branches/mango/MangoJPF/repository/plugins/SendEvents1$A.class
branches/mango/MangoJPF/repository/plugins/SendEvents1$B.class
branches/mango/MangoJPF/repository/plugins/SendEvents1$C.class
branches/mango/MangoJPF/repository/plugins/SendEvents1.class
branches/mango/MangoJPF/repository/plugins/SendEvents1.es
branches/mango/MangoJPF/repository/plugins/SendEvents2$A$A1.class
branches/mango/MangoJPF/repository/plugins/SendEvents2$A$A2.class
branches/mango/MangoJPF/repository/plugins/SendEvents2$A.class
branches/mango/MangoJPF/repository/plugins/SendEvents2$B$B1.class
branches/mango/MangoJPF/repository/plugins/SendEvents2$B$B2.class
branches/mango/MangoJPF/repository/plugins/SendEvents2$B.class
branches/mango/MangoJPF/repository/plugins/SendEvents2.class
branches/mango/MangoJPF/repository/plugins/SendEvents2.es
branches/mango/MangoJPF/repository/plugins/StringTest.class
branches/mango/MangoJPF/repository/plugins/SyncEvents$A1.class
branches/mango/MangoJPF/repository/plugins/SyncEvents$A2.class
branches/mango/MangoJPF/repository/plugins/SyncEvents$B1.class
branches/mango/MangoJPF/repository/plugins/SyncEvents.class
branches/mango/MangoJPF/repository/plugins/TestInput.class
branches/mango/MangoJPF/repository/plugins/TestOutput.class
branches/mango/MangoJPF/repository/plugins/TestOutputFailing.class
branches/mango/MangoJPF/repository/plugins/TestSafetyAutomaton.class
branches/mango/MangoJPF/repository/plugins/Wildcards$A.class
branches/mango/MangoJPF/repository/plugins/Wildcards$B.class
branches/mango/MangoJPF/repository/plugins/Wildcards.class
branches/mango/MangoJPF/repository/plugins/Wildcards.es
branches/mango/MangoJPF/repository/plugins/coverage/
branches/mango/MangoJPF/repository/plugins/gov/
branches/mango/MangoJPF/repository/plugins/jfuzz/
branches/mango/MangoJPF/repository/plugins/ltl2buchi.properties
branches/mango/MangoJPF/repository/plugins/samplevisualizeconfigs/
branches/mango/MangoJPF/repository/plugins/sequences/
branches/mango/MangoJPF/repository/plugins/symbolicheap/
branches/mango/MangoJPF/repository/plugins/txtfiles/
branches/mango/MangoJPF/repository/plugins/visualize/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-16 17:24:41
|
Revision: 1410
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1410&view=rev
Author: frankrimlinger
Date: 2009-04-16 17:24:30 +0000 (Thu, 16 Apr 2009)
Log Message:
-----------
cleanup of MangoJPF in preparation for product rebuild.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/META-INF/MANIFEST.MF
Removed Paths:
-------------
branches/mango/MangoJPF/MangoJPF.product
branches/mango/MangoJPF/repository/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-16 19:34:15
|
Revision: 1411
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1411&view=rev
Author: frankrimlinger
Date: 2009-04-16 19:34:09 +0000 (Thu, 16 Apr 2009)
Log Message:
-----------
The MangoJPF help mechanism somehow got broken. Clearing it out for a fresh start.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/META-INF/MANIFEST.MF
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
branches/mango/MangoJPF/content/mangoJPF.xhtml
branches/mango/MangoJPF/content/proofArtifacts.xhtml
branches/mango/MangoJPF/introContent.xml
branches/mango/MangoJPF/plugin.xml
branches/mango/MangoJPF/src/mango/intro/ApplicationWorkbenchWindowAdvisor.java
branches/mango/MangoJPF/src/mango/intro/LoginDialog.java
branches/mango/MangoJPF/src/mango/intro/Perspective.java
Added Paths:
-----------
branches/mango/MangoJPF/META-INF/MangoJPF.product
branches/mango/MangoJPF/content/aboutHelp.xhtml
branches/mango/MangoJPF/help.bmp
Removed Paths:
-------------
branches/mango/MangoJPF/html/
branches/mango/MangoJPF/toc/
branches/mango/MangoJPF/toc.xml
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-16 19:59:41
|
Revision: 1412
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1412&view=rev
Author: frankrimlinger
Date: 2009-04-16 19:59:37 +0000 (Thu, 16 Apr 2009)
Log Message:
-----------
OK, there probably was nothing wrong with the MangoJPF help mechanism as such. The problem was that the "class path settings" needed to be updated. This is a good one to try whenever plugins don't seem to be kicking in. However, it was just as well to throw out the old hand written table of contents html. The proper thing to do is to use the suppled table of contents html editor to build up the help files. The workings of this editor revealed in detail when you click on its help icon.
To summarize, Mango and MangoJPF are both healthy again. MangoJPF still needs its plugin jars bundling the jars required by jpf. These are now stored in the toplevel directory javapathfinder-mango/"target jars". This is a good place for manufactured plugins to hang out, as they must be loaded into the "target" at the Eclipse preference level. Once so loaded, they easily feed into the MangoJPF plugin. The "repository" concept isn't working for me and so I have abandoned it.
So, plugins should flow from the Eclipse preference target, to the project preference build path, to the plugin manifest, to the produce configuration editor. Don't try to work them upstream, and it's a piece of cake.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/META-INF/MangoJPF.product
branches/mango/MangoJPF/plugin.xml
Added Paths:
-----------
branches/mango/MangoJPF/html/
branches/mango/MangoJPF/html/concepts/
branches/mango/MangoJPF/html/concepts/maintopic.html
branches/mango/MangoJPF/html/concepts/subtopic.html
branches/mango/MangoJPF/html/concepts/subtopic2.html
branches/mango/MangoJPF/html/gettingstarted/
branches/mango/MangoJPF/html/gettingstarted/maintopic.html
branches/mango/MangoJPF/html/gettingstarted/subtopic.html
branches/mango/MangoJPF/html/gettingstarted/subtopic2.html
branches/mango/MangoJPF/html/reference/
branches/mango/MangoJPF/html/reference/maintopic.html
branches/mango/MangoJPF/html/reference/subtopic.html
branches/mango/MangoJPF/html/reference/subtopic2.html
branches/mango/MangoJPF/html/samples/
branches/mango/MangoJPF/html/samples/maintopic.html
branches/mango/MangoJPF/html/samples/subtopic.html
branches/mango/MangoJPF/html/samples/subtopic2.html
branches/mango/MangoJPF/html/tasks/
branches/mango/MangoJPF/html/tasks/maintopic.html
branches/mango/MangoJPF/html/tasks/subtopic.html
branches/mango/MangoJPF/html/tasks/subtopic2.html
branches/mango/MangoJPF/html/toc.html
branches/mango/MangoJPF/toc.xml
branches/mango/MangoJPF/tocconcepts.xml
branches/mango/MangoJPF/tocgettingstarted.xml
branches/mango/MangoJPF/tocreference.xml
branches/mango/MangoJPF/tocsamples.xml
branches/mango/MangoJPF/toctasks.xml
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-18 03:51:00
|
Revision: 1418
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1418&view=rev
Author: frankrimlinger
Date: 2009-04-18 03:50:58 +0000 (Sat, 18 Apr 2009)
Log Message:
-----------
Created extension of JPF, called JPF_MIRROR, whose main routine creates the vm but does not fire up a thread and run. Now comes an interesting issue. Mango needs to do an analysis of the "entire" code body in order to convert loops to recursive functions. But jpf pulls in classes on-the-fly, starting out with just enough grist for the mill. This is certainly more elegant, but jpf doesn't necessarily "care" about complete coverage of all paths. It seems quite likely there is an option for such a preference, and I will investigate. In any case, the idea is to give jpf the method to be analyzed as the "main" routine and let it run through though all edges of the forward control flow graph at least once. This will cause all the invovled classes to get pulled in. Once I have all the relevant class models then mango can do its thing, creating "advice" for future jpf runs.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/.project
branches/mango/MangoJPF/Mango/src/mango/control/msg/StartRequestMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ClassParsingAlg.java
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/JPF_MIRROR.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-20 16:57:24
|
Revision: 1421
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1421&view=rev
Author: frankrimlinger
Date: 2009-04-20 16:57:17 +0000 (Mon, 20 Apr 2009)
Log Message:
-----------
Brilliant idea to reflect the target method inside target launcher main() for jpf symbolic execution has ended in abject failure:
java.lang.ClassNotFoundException
at java.lang.Class.forName(Native Method)
at mango.symbc.MangoTargetLauncher.getTargetMethod(MangoTargetLauncher.java:37)
at mango.symbc.MangoTargetLauncher.main(MangoTargetLauncher.java:13)
Evidently jpf draws the line at diving into reflection, and who can blame it for that?
Also, any hanky panky with the entrypoint is ruled out: on page 158, section5.2 of JVM2nd Ed., we have
"The Java virtual machine then links the initial class, initializes it, and invokes its public class method void main(String[]).
So it is written, so it must be. This is one of those exquisitely rare occasions when direct alteration of the .class file is required. Therefore, prior to any class loading, I will use my home-grown parser to read in MangoTargetLauncher.class, burn in the call to the targeted method, and write it back out. The trick is just to make sure that no other ClassLoader can find MangoTargetLauncher, and then call the "midnight special" ClassLoader to load it in when it is ready to go.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ClassParsingAlg.java
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/MangoTargetLauncher.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-21 14:21:19
|
Revision: 1424
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1424&view=rev
Author: frankrimlinger
Date: 2009-04-21 14:21:15 +0000 (Tue, 21 Apr 2009)
Log Message:
-----------
Successful test of MangoTargetLauncher, which uses reflection to invoke the target method for symbolic simulation, eliminating the need to manually create a main() driver. Under this scenario, successfully duplicate the entire run for the MyClass1 example. The trick was to debug the launcher using the vm BEFORE attempting vm^2, because unfortunately cannot step through vm^2 with debugger (maybe you can with VJP?).
In any event, learned about listeners and the model java interface. There is a lot of subtle stuff going on here, and the fact that the launcher works out-of-the-box gives me enormous confidence to proceed.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/MangoTargetLauncher.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-21 17:04:42
|
Revision: 1425
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1425&view=rev
Author: frankrimlinger
Date: 2009-04-21 17:04:29 +0000 (Tue, 21 Apr 2009)
Log Message:
-----------
Test of itsAWrap under symbolic vm^2 execution. Fixed some imported package bugs in my version of the bytecode package. There could be a few more of these bugs still outstanding. With this in place, vm^2 got as far as vm, to a NullPointerException in clear(), as expected. But simulated method invocation appears to be working, so now will proceed to clear out all the simulation functionality other than class loading and invocation. Of course, you will need to add logic for the next pc in the case of branch instructions, and this will get you into choices and backtracking. Not sure how this will play out yet. But goal is to get jpf to traverse the forward control flow as efficiently as possible. Once this happens, the can think about punching in functionality to build control flow graph.
Confirmed that vm^2 does not required a project level dependence on the target project in order to executed the target project code. All this is taken care of through properties, as expected. However, vm obviously DOES require this link, everything else being equal.
Thinking down the road, ideally, the user should just point to a class, then simulation kicks in and travels down all methods in the class to build up the total control flow diagram and the call diagram. Then call diagram can be analyzed with respect to the rulebase to determine plausible next candidates for specification, which can then be presented to the user in a chooser window. This should all happen fast enough for the user to not think anything has happened. This will eliminate a lot of annoying file navigation and start up latency in current mango version.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mainArgFile
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INVOKEVIRTUAL.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/BytecodeUtils.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-22 00:14:16
|
Revision: 1432
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1432&view=rev
Author: frankrimlinger
Date: 2009-04-22 00:13:59 +0000 (Wed, 22 Apr 2009)
Log Message:
-----------
Successful simulation of itsAWrap using package mango.symbc.bytecode, which models all the bytecodes. This involved a few very minor changes to gov.nasa.jpf.jvm in order to avoid a runtime ClassCastException. I have submitted these changes to Peter for approval.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ReturnInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-22 21:40:21
|
Revision: 1440
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1440&view=rev
Author: frankrimlinger
Date: 2009-04-22 21:40:08 +0000 (Wed, 22 Apr 2009)
Log Message:
-----------
MangoJPF now has a design! This should carry through 2010, and will be revised/fleshed out as coding requirements and testing dictate.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/INVOKECG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/RETURN.java
Added Paths:
-----------
branches/mango/MangoJPF/doc/
branches/mango/MangoJPF/doc/design.rtf
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-23 12:28:04
|
Revision: 1444
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1444&view=rev
Author: frankrimlinger
Date: 2009-04-23 12:28:00 +0000 (Thu, 23 Apr 2009)
Log Message:
-----------
Updating preferences to account for needs of jpf in progress. Much of this will go away in the final product. As a workbench plugin, you should just get everything you need to know from the current project and you own stash of plugins. This is still down the road.
Modified Paths:
--------------
branches/mango/MangoJPF/doc/design.rtf
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/MangoTargetLauncher.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/bytecode/ALOAD.java
branches/mango/MangoJPF/src/mango/intro/ConfigurationDetails.java
branches/mango/MangoJPF/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-04-23 22:28:25
|
Revision: 1446
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1446&view=rev
Author: frankrimlinger
Date: 2009-04-23 22:28:22 +0000 (Thu, 23 Apr 2009)
Log Message:
-----------
Almost done rewiring preference mechanism for jpf integration. Just a few more bugs downstream from the gui stuff.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/control/action/input/LibraryJarsAction.java
branches/mango/MangoJPF/Mango/src/mango/control/action/input/SourceDirsAction.java
branches/mango/MangoJPF/Mango/src/mango/control/action/input/TargetJarsAction.java
branches/mango/MangoJPF/Mango/src/mango/control/msg/LoadClassFileDataRequestMsg.java
branches/mango/MangoJPF/Mango/src/mango/control/msg/SetSourceDirectoryRequestMsg.java
branches/mango/MangoJPF/Mango/src/mango/core/gui/action/PrintAbstractionsAction.java
branches/mango/MangoJPF/Mango/src/mango/rmi/file/MangoFilePacket.java
branches/mango/MangoJPF/Mango/src/mango/script/MangoScriptResource.java
branches/mango/MangoJPF/Mango/src/mango/script/MangoScriptSourceDirectory.java
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ClassModel.java
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/MangoTargetLauncher.java
branches/mango/MangoJPF/src/mango/intro/ConfigurationDetails.java
branches/mango/MangoJPF/src/mango/intro/LoginDialog.java
branches/mango/MangoJPF/src/mango/views/LogWindow.java
branches/mango/MangoJPF/src/mango/views/WorkstationWindow.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-24 18:50:34
|
Revision: 1449
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1449&view=rev
Author: frankrimlinger
Date: 2009-04-24 18:50:23 +0000 (Fri, 24 Apr 2009)
Log Message:
-----------
Removed all jpf extensions from MangoJPF classpath. Changed JPF extension to SCANNER, because SCANNER will be fired to perform the initial scan of the designated class. For this purpose, SCANNER fires MangoTargetLauncher.main(), which reflectively calls all the methods in the designated class to make sure all code gets traversed. Moved ported bytecodes to package mango.scanner.bytecode since these bytecodes must be specifically designed to scan. Because gov.nasa.jpf.symbc is no longer with us, a lot of these bytecodes are no longer compiling, but this is expected and they need to be stripped anyway to implement scanner functionality. The first step is just to make sure every possible branch choice at the bytecode level is identified. This includes all possible condition values for branch instructions, and all runtime exceptions for ALL bytecodes. And there are other weirdo exceptions, they all impact control flow so they all get modelled. OK, not modelling IlletaMonitorStateException, as analysis is single threaded.
Start with ASTORE, you have a long row to hoe.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/.project
branches/mango/MangoJPF/Mango/src/mango/control/msg/StartRequestMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ArrayInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ArrayLoadInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ArrayStoreInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2B.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2C.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2S.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ICONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IINC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ILOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INSTANCEOF.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IfInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCMP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC2_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOOKUPSWITCH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LocalVariableInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LockInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LongArrayLoadInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LongArrayStoreInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITORENTER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITOREXIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NOP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RUNSTART.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SWAP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SwitchInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/TABLESWITCH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/VirtualInvocation.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoTargetLauncher.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BytecodeUtils.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ReturnInstruction.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BytecodeUtils.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ReturnInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/MangoTargetLauncher.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-25 18:33:04
|
Revision: 1451
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1451&view=rev
Author: frankrimlinger
Date: 2009-04-25 18:32:54 +0000 (Sat, 25 Apr 2009)
Log Message:
-----------
Fixed wiring bug that prevented scanner bytecodes from loading. Verified that scanner bytecodes are now now loading, at least the ones that compile. Back to bytecode rehab.
Modified Paths:
--------------
branches/mango/MangoJPF/META-INF/MANIFEST.MF
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BytecodeUtils.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/SymbolicListener.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/symbc/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-28 22:38:18
|
Revision: 1459
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1459&view=rev
Author: frankrimlinger
Date: 2009-04-28 22:38:08 +0000 (Tue, 28 Apr 2009)
Log Message:
-----------
Finally grocked MJIEnv. When you want to push an object for JPF to JVM, well, you can't expect an object to show up on the other side, all you get is a state and some references (heap addresses). It's up to you to dive into the heap using the MJIEnv accessors and recover any data you want. So probably will end up with a greatly expanded set of accessors that "know" the structure of important objects (like Instruction). But the point is, it can be done.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_scanner_ScannerMJI.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-29 02:33:56
|
Revision: 1460
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1460&view=rev
Author: frankrimlinger
Date: 2009-04-29 02:33:37 +0000 (Wed, 29 Apr 2009)
Log Message:
-----------
Earlier comment was somewhat confused. It is indeed true that you need MJIEnv to parse state object, however, I will never need to do this. I do need to get the structure of the Instruction objects, but these are already at the JVM level, so good to go.
Refined the phase change strategy. We define the extension ScannerStackFrame of StackFrame.
When an invocation instruction executes, if SCANNER.scannerPhase is BEGIN or SCAN, then it sets up an InvocationChoiceGenerator if one is not present already. SCANNER.scannerPhase is set to SCAN.
InvocationChoiceGenerator is trivial for all but virtual invocation. But it is easier just to cover all cases with the same procedure.
The choices of which methods could possibly be virtually invoked are determined by existing mango strategies. However, as classes are now loaded just-in-time, we need to enforce a pro-active class loading up front to make sure the entire targeted code base is surveyed for candidates. No big deal, just a recursive walk though classpath space and a hashed inventory of fully qualified method names and signatures. There is just no other way to do this.
The generated choice instructions will be INVOKExxxSCAN, corresponding to the original INVOKExxx instruction. These synthetic instructions will push a ScannerStackFrame.
A return instruction examines the class of the caller frame. If this class is NOT a ScannerStackFrame, then SCANNER.scannerPhase is set to JPF.
Note that END phase is not needed and has been discarded.
Both the invocation and return instruction families must implement the Transition interface. This just emphasizes the fact that, even when in BEGIN or SCAN phase, these instructions act on JPF state, by adding or removing frames as appropriate. Also, when a return instruction does transition to JPF, it must push some sort of dummy value onto the caller opstack if required, or there will be tears.
The BEGIN transition is probably unnecessary, since the transition from JPF to BEGIN occurs in the native code scan(), just before we box and return the invocation instruction. So it seems likely that the invocation is the next thing to happen anyway. If this proves to be so, then BEGIN can be eliminated.
Note that all this depends very much on the single threaded assumption. A multi-threaded version would, at a minimum, require scannerPhase maintained on a per thread basis. But since multithreading would bring formal analysis to its knees anyway, there is no point to adding this layer of complexity.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_scanner_ScannerMJI.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoTargetLauncher.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScanChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScannerMJI.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/ScannerStackFrame.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/TargetMethodRegistrar.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINITSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACESCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIALSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATICSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUALSCAN.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/MethodInfoAdapter.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/ReturnInstructionAdapter.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/StackFrameAdapter.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-29 18:19:15
|
Revision: 1461
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1461&view=rev
Author: frankrimlinger
Date: 2009-04-29 18:19:00 +0000 (Wed, 29 Apr 2009)
Log Message:
-----------
Ran into an unpleasant snag while writing VirtualMethodRegistrar extension of ClassLoader to inventory all modelled methods. Recall this inventory is required by InvocationChoiceGenerator. I decided I would use the jpf model of the java package for mango, since it is remarkably full of goodies. But when I tried to read it in with ClassLoader.defineClass(), well, thats a security violation of the root ClassLoader. And rightfully so. No problem, I say, because I can just run virtually under JPF. Unfortunately, defineClass is "not supported yet" in JPF world. Oh well, the fall back plan is just to change "java" to "javaShadow" and refactor the classes. Then I can perform my inventory, just changing "javaShadow" back to "java" wherever I see it. This is ugly, but I have to get on with it.
Hopefully defineClass() will be properly modelled some day in JPF, as the comment seems to suggest. Actually, mango currently parses .class files by hand, but I don't want to go there. This is exactly the code I want to eliminate.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/.project
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/File.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/FileDescriptor.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/FileInputStream.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/FileOutputStream.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/InputStreamReader.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/OutputStreamWriter.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/RandomAccessFile.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/Class.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/ClassLoader.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/StackTraceElement.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/System.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/Thread.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/Throwable.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/annotation/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/annotation/Inherited.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/annotation/Retention.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/ref/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/ref/Reference.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/ref/ReferenceQueue.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/ref/WeakReference.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/AccessibleObject.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/Constructor.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/Field.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/InvocationTargetException.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/Method.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/security/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/security/AccessController.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/security/MessageDigest.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/text/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/text/DecimalFormat.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/text/Format.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/text/NumberFormat.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/text/SimpleDateFormat.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/BrokenBarrierException.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/CyclicBarrier.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/atomic/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/atomic/AtomicIntegerFieldUpdater.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/atomic/AtomicLongFieldUpdater.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/atomic/AtomicReferenceFieldUpdater.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/regex/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/regex/Matcher.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/regex/Pattern.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/VirtualMethodRegistrar.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/TargetMethodRegistrar.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-01 03:13:22
|
Revision: 1473
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1473&view=rev
Author: frankrimlinger
Date: 2009-05-01 03:12:58 +0000 (Fri, 01 May 2009)
Log Message:
-----------
With the conceptual issues regarding invocation, return, and scanner mode transition under control, resumed bytecode rehab. Several templates have been created for this purpose. Bytecodes which do manipulate the stack, eg, invocations and returns, or offer multiple branches other than for thrown exceptions, throw IllegalStateException("NEED CODE HERE"). (That is, throw at the vm level, NOT the vm^2 level!) Once the rehab is complete, jpf level execution will be functional. The rest of the bytecode functionality can the be written and tested on a pay-as-you-go basis as the missing code exceptions are encountered.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/.project
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X2.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InstructionTemplates.txt
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-01 18:07:17
|
Revision: 1475
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1475&view=rev
Author: frankrimlinger
Date: 2009-05-01 18:07:15 +0000 (Fri, 01 May 2009)
Log Message:
-----------
Completed rough-out of mango.scanner.bytecode. Tested JPF execution phase by successfully running MangoTargetLauncher. With the test-bed in place, we can switch on scanner phase as planned and code and debug the scanner bytecode functionality one bytecode at a time. Actually, there are only about twenty bytecodes that require special consideration, so this is manageable. There is also the unexplored listener issue. How exactly do clinits fire? What else is going on? Still much to learn.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2B.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2C.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2S.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ICONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IINC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ILOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INSTANCEOF.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINITSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACESCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIALSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATICSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUALSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCMP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC2_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOOKUPSWITCH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITORENTER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITOREXIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NOP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RUNSTART.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SWAP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/TABLESWITCH.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode/
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/VirtualInvocationScan.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SIPUSH.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-02 20:23:03
|
Revision: 1479
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1479&view=rev
Author: frankrimlinger
Date: 2009-05-02 20:22:52 +0000 (Sat, 02 May 2009)
Log Message:
-----------
Working through details of jpf/scanner invocation phase transition.
Notes: 1) invokevirtual and invokeinterface are almost the same, except invokeinterface does not require access control. 2) mango currently simulates a thrown exception by "returning" an exception object to caller, and then "catching" return values and branching to the handlers or rethrowing as appropriate. The question then becomes, since jpf is now in the driver's seat as far as control flow goes, can we scrap the old "exception catchers" and just model the observed jpf behavior. This really is the way to go, because if the map from jpf simulation to the mango control flow graph is not invertable, there will be problems down the road.
Modified Paths:
--------------
branches/mango/MangoJPF/.settings/org.eclipse.jdt.core.prefs
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScanChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-03 16:57:56
|
Revision: 1480
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1480&view=rev
Author: frankrimlinger
Date: 2009-05-03 16:57:47 +0000 (Sun, 03 May 2009)
Log Message:
-----------
Exceptions have been grocked.
First, the mango catch mechanism cannot be dropped. The point is that a method doesn't "know" where it returns to, so an exception cannot "know" where it will be thrown. All we can do is model the local structure of the throw, and stitch these together when evaluating a nested calling sequence within the target method. Therefore, during the scanning phase, it is meaningless to trace the path of a thrown exception. This is totally spurious information, just an artifact of the scanning process. Therefore, there is no point throwing exceptions in the first place: mango already knows which instructions throw, and why they throw, and there is nothing more to be learned.
So, all the information about exceptions meticulously supplied to the scanner bytecodes must be stripped back out again.
Now here is where things get weird. We still need to simulate all the handler code within the supplied methods and build the corresponding control flow graph segments. Otherwise the mango catchers will have nowhere to send the caught exceptions. So, just like in the case of clinits, we must rely on the target launcher to use MJI to get at these entrypoints. Fortunately, they can be recovered from the MethodInfo class. Its a little trickier than the case of invocations, because there could be multiple handlers in a given method, so you need to arrange to traverse all of them. Also, you must manually push a ScannerStackFrame so that the handler will have something to digest. (Since we are going into scanner mode, we don't have to bother with setting up the heap or the operand stack.)
Now what happens when the handler "returns". There is no problem here, because it will either happen because of a return or an athrow. Either way, we will pop the ScannerStackFrame and detect the jpf StackFrame, and this will trigger a phase change to jpf. Execution will then proceed in the MangoTargetLauncher just after the native call to fire the handler.
Start by writing the launcher code and native methods to scan the handlers. This is a brain-burner.
NB: If you are in scanning phase and you have already visited an instruction, then you should return null, meaning that this path need not be explored.
We need a master counter of ALL outstanding choices within a target method simulation. A return to jpf should just return null if there are outstanding choices. The transition to jpf should only occur when no choices remain. This prevents jpf from backtracking back into a target once it has left it, potentially creating an exponential growth in the number of paths to traverse.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScanChoiceGenerator.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-05 18:19:59
|
Revision: 1486
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1486&view=rev
Author: frankrimlinger
Date: 2009-05-05 18:19:45 +0000 (Tue, 05 May 2009)
Log Message:
-----------
Prep work for final scanner bytecode rehab in place. The code is a lot cleaner and meaner. Replacing the target launcher with a choice generator for the synthetic INVOKETARGET instruction turned out to really simplify matters. In particular, the "phase transition" is now trivial. Once the scanner turns on, it stays until vm^2 exits upon exhausting all choices.
Hopefully it will all work as expected, but not possible to test until bytecodes are ready.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchListener.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/TargetChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/ScannerStackFrame.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScanChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/VirtualInvocationScan.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-05 21:40:25
|
Revision: 1487
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1487&view=rev
Author: frankrimlinger
Date: 2009-05-05 21:40:16 +0000 (Tue, 05 May 2009)
Log Message:
-----------
Scanner bytecodes are squeaky clean now, and most branch and all invocation bytecodes have been written. The only tricky thing is jsr and ret. Actually, jsr is easy because you can get the destination from the bcel peer. But ret is harder because the ret destination is in a local variable, and the frame is of course not available to us. So we resort to the mango method, just walk through the method, looking for a jsr which branches to the ret. Once we find it, our dest is just the instruction after the jsr. EZ
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2B.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2C.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2S.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ICONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IINC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ILOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INSTANCEOF.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-06 21:27:56
|
Revision: 1489
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1489&view=rev
Author: frankrimlinger
Date: 2009-05-06 21:27:41 +0000 (Wed, 06 May 2009)
Log Message:
-----------
Finished final bytecode rehab and started testing code scanner. Late binding of the choice generated PC via VMListeners turns out to be a huge win. This works exactly as expected, and jpf is spinning out beautiful graph data for Mango to absorb. All the data is offered on a silver platter, without having to painfully wrestle down the bits in the .class files.
Have starting working on well understood control flow issues, rulebase look up for missing code, etc. Once this settles down I will bind the formal state transition logic to the instructions, and adapt the mango code subdivision algorithm to the new setting. All that is required is to maintain the binding to jpf instructions, so that eventually the rewriter can be driven by jpf simulation. This will be very cool.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_scanner_ScannerMJI.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/INVOKETARGET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCMP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC2_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOOKUPSWITCH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITORENTER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITOREXIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NOP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SWAP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/TABLESWITCH.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/TargetListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-07 02:26:48
|
Revision: 1490
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1490&view=rev
Author: frankrimlinger
Date: 2009-05-07 02:26:40 +0000 (Thu, 07 May 2009)
Log Message:
-----------
Fixed various invocation related bugs. There is a problem when a choice terminates at an instruction that has already been visited. For some reason, pc becomes null because no listener is listening? Must investigate.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchListener.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
×
Want the latest updates on software, tech news, and AI?
Get latest updates about software, tech news, and AI from SourceForge directly in your inbox once a month.
Thanks for helping keep SourceForge clean.
X