Menu
▾
▴
javapathfinder-svn
|
From: <fra...@us...> - 2009-04-14 17:33:26
|
Revision: 1400
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1400&view=rev
Author: frankrimlinger
Date: 2009-04-14 17:33:10 +0000 (Tue, 14 Apr 2009)
Log Message:
-----------
Removing dependence on JPF from Mango. This was just some proof-of-concept code that resulted in the new MangoJPF project. The Mango project will be used to complete testing of the original port from C++, and the results will be incorporated in MangoJPF. Mango should go away in a few months, but MangoJPF will eventually become an Eclipse Workbench plugin.
Modified Paths:
--------------
branches/mango/Mango/.classpath
branches/mango/Mango/META-INF/MANIFEST.MF
branches/mango/Mango/Mango/src/mango/control/msg/StartRequestMsg.java
branches/mango/Mango/Mango.product
branches/mango/Mango/content/proofArtifacts.xhtml
branches/mango/Mango/plugins/Mango_Jars_1.0.0.jar
Removed Paths:
-------------
branches/mango/Mango/plugins/JPF_jar_1.0.0.jar
branches/mango/Mango/repository/plugins/JPF_jar_1.0.0.jar
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-14 21:29:35
|
Revision: 1402
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1402&view=rev
Author: frankrimlinger
Date: 2009-04-14 21:29:16 +0000 (Tue, 14 Apr 2009)
Log Message:
-----------
Finally figured out how to get help working. This is actually a case of a more general technique, "plugin poker". When documentation goes stale, it is likely that the technique still works, but just uses different plugins. So, just start adding them. You have to know when to hold, and when to fold...
Modified Paths:
--------------
branches/mango/Mango/plugin.xml
branches/mango/MangoJPF/MangoJPF.product
branches/mango/MangoJPF/jpf jar command.rtf
branches/mango/MangoJPF/plugin.xml
Added Paths:
-----------
branches/mango/Mango/help.bmp
branches/mango/Mango/html/
branches/mango/Mango/html/concepts/
branches/mango/Mango/html/concepts/maintopic.html
branches/mango/Mango/html/concepts/subtopic.html
branches/mango/Mango/html/concepts/subtopic2.html
branches/mango/Mango/html/gettingstarted/
branches/mango/Mango/html/gettingstarted/maintopic.html
branches/mango/Mango/html/gettingstarted/subtopic.html
branches/mango/Mango/html/gettingstarted/subtopic2.html
branches/mango/Mango/html/help_home.html
branches/mango/Mango/html/reference/
branches/mango/Mango/html/reference/maintopic.html
branches/mango/Mango/html/reference/subtopic.html
branches/mango/Mango/html/reference/subtopic2.html
branches/mango/Mango/html/samples/
branches/mango/Mango/html/samples/maintopic.html
branches/mango/Mango/html/samples/subtopic.html
branches/mango/Mango/html/samples/subtopic2.html
branches/mango/Mango/html/tasks/
branches/mango/Mango/html/tasks/maintopic.html
branches/mango/Mango/html/tasks/subtopic.html
branches/mango/Mango/html/tasks/subtopic2.html
branches/mango/Mango/html/toc.html
branches/mango/Mango/preferences.ini
branches/mango/Mango/toc/
branches/mango/Mango/toc/tocconcepts.xml
branches/mango/Mango/toc/tocgettingstarted.xml
branches/mango/Mango/toc/tocreference.xml
branches/mango/Mango/toc/tocsamples.xml
branches/mango/Mango/toc/toctasks.xml
branches/mango/Mango/toc.xml
branches/mango/Mango Jars/jpf jar command.rtf
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/
branches/mango/MangoJPF/toc/tocconcepts.xml
branches/mango/MangoJPF/toc/tocgettingstarted.xml
branches/mango/MangoJPF/toc/tocreference.xml
branches/mango/MangoJPF/toc/tocsamples.xml
branches/mango/MangoJPF/toc/toctasks.xml
branches/mango/MangoJPF/toc.xml
Removed Paths:
-------------
branches/mango/Mango/jpf jar command.rtf
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-15 05:36:26
|
Revision: 1404
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1404&view=rev
Author: frankrimlinger
Date: 2009-04-15 05:36:08 +0000 (Wed, 15 Apr 2009)
Log Message:
-----------
Added a help button to the login dialog pointing the new user to the help. Added some advice about configuration to the Welcome window. Finally figured out how layout works in SWT. Rather cold and efficient compared to the wonderful weirdness of Swing boxes. But anyway, have a sensible initial layout burned into the code now.
Modified Paths:
--------------
branches/mango/Mango/content/mango.xhtml
branches/mango/Mango/introContent.xml
branches/mango/Mango/src/mango/intro/ApplicationWorkbenchWindowAdvisor.java
branches/mango/Mango/src/mango/intro/LoginDialog.java
branches/mango/Mango/src/mango/intro/Perspective.java
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/.settings/org.eclipse.jdt.core.prefs
branches/mango/MangoJPF/META-INF/MANIFEST.MF
Added Paths:
-----------
branches/mango/Mango/content/aboutHelp.xhtml
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-16 16:53:53
|
Revision: 1409
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1409&view=rev
Author: frankrimlinger
Date: 2009-04-16 16:53:47 +0000 (Thu, 16 Apr 2009)
Log Message:
-----------
beginning to understand the how the plugin manifest, the product manifest, the project build path preferences, the plug-in dependencies virtual folder view, the repository, the launch configuration, the .metadata, and the runtime.product all work together to make it happen. You must achieve a higher state of consciousness, transcending documentation, to truly understand the rich client platform.
Modified Paths:
--------------
branches/mango/Mango/.classpath
Removed Paths:
-------------
branches/mango/Mango/plugins/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-17 04:11:10
|
Revision: 1413
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1413&view=rev
Author: frankrimlinger
Date: 2009-04-17 04:11:08 +0000 (Fri, 17 Apr 2009)
Log Message:
-----------
Have realized that jpf really does override java.lang.Class and other fun classes in ways that are significantly incompatible with the rest of the universe. But even loading the jpf versions of these classes, I still crash very early on in the class loader. This could be an incompatibility with the jar plugins?? Perhaps I must convince the jar plugin builder to accept the rogue java.lang code??? Must sleep on this.
Modified Paths:
--------------
branches/mango/Mango/.classpath
branches/mango/Mango/META-INF/MANIFEST.MF
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/.project
branches/mango/MangoJPF/META-INF/MANIFEST.MF
branches/mango/MangoJPF/META-INF/MangoJPF.product
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-17 17:48:33
|
Revision: 1415
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1415&view=rev
Author: frankrimlinger
Date: 2009-04-17 17:48:21 +0000 (Fri, 17 Apr 2009)
Log Message:
-----------
The first step to getting jpf code to run is to reproduce the exact environment that it likes. Just bundling the jars that jpf uses into plugins should not affect runtime, so that is still in place. However, instead of attempting to jar the source code that jpf-trunk loads, I just link to this source from MangoJPF. Having done so, all the jpf code compiles inside of MangoJPF, except the java5/6 "compatibility code". Probably breaks as I am running under J2SE6. I filtered out the sun compatibility classes, but now there is a broken calls in env/jpf/jaf.lang.Class and System. Hopefully not a problem, but in any event should go away when the switch to J2SE6 is "official".
But, lots of MangoJPF code is breaking. Certain things can probably be safely thrown overboard. In particular, extensions/ui/env/jpf/java.awt and java.swing are probably stubs for jpf users. Doing this, the rest of the jpf code still compiles, hooray, and the only remaining issues with MangoJPF involve some unsupported methods in env/jpf/java/lang, especially Class and ClassLoader. I rewrite the MangoJPF code to conform. Not a problem since JPF will be taking over this particular MangoJPF functionality anyway.
So, with all of this in place, I get past my initial crash to
[SEVERE] error during VM runtime initialization: wrong model classes (check vm.[boot]classpath)
This looks hopeful, so syncing to lock in current progress. Of course, the link to the jpf-trunk source code is a very temporary expedient. It is not a deployable solution, and it is far too tempting to alter jpf-trunk code this way. Once things settle down I will find a way to jar most if not all of the trunk code.
Modified Paths:
--------------
branches/mango/Mango/content/proofArtifacts.xhtml
branches/mango/Mango/content/specification.xhtml
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/.project
branches/mango/MangoJPF/META-INF/MANIFEST.MF
branches/mango/MangoJPF/META-INF/MangoJPF.product
branches/mango/MangoJPF/Mango/src/mango/control/input/JarLoader.java
branches/mango/MangoJPF/Mango/src/mango/control/msg/StartRequestMsg.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/Hash.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/backupDelegate/BackupDelegate.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/graph/Graph.java
branches/mango/MangoJPF/Mango/src/mango/workstation/RuleResourceManager.java
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.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 04:31:54
|
Revision: 1420
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1420&view=rev
Author: frankrimlinger
Date: 2009-04-20 04:31:51 +0000 (Mon, 20 Apr 2009)
Log Message:
-----------
Switcheroo of symbolic execution to produce control flow diagram (as well as building byte code models) in progress. Made a copy of SymbolicInstructionFactory, called MangoInstructionFactory. For sanity test, created a copy of symbc/examples/MyClass1, which I put in the FrankInput project as symbolicExecution/SimpleTest. Discovered that jpf has a little trouble finding classes in remote projects, but there is a trick for this: the last line of the properties just needs to be the fully qualified class name, then all of a sudden jpf is ok with it. From within MangoJPF, fired up symbolic execution of SimpleTest against MangoInstructionFactory, producing the expected output (same as for MyClass1). So, all the plumbing is in place, it is time to bend MangoInstructionFactory to my will, and make it create the control flow diagram.
There is one slighly weird thing. JPF is ever so careful to get static initialization right, and so must be aware of the beginning of time from the get go. Whereas mango just assumes the beginning of time was at some unknown point in the past, and doesn't get stressed about it. The upshot is that I must manufacture a driver to call the targeted method before unleashing jpf. It is theoretically possible to do this, but maybe jpf can allow entrypoints other than main(). Must investigate. Either way, the nominal jpf execution is bogus, since the static initialization is "wrong". So there will always be a problematic element in switching between mango and "real" jpf.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/input/.classpath
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ClassParsingAlg.java
branches/mango/MangoJPF/html/toc.html
branches/mango/MangoJPF/plugin.xml
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/input/SymbolicExecutionTest/
branches/mango/Mango/mangoUserHome/frank/input/SymbolicExecutionTest/symbolicExecution/
branches/mango/Mango/mangoUserHome/frank/input/SymbolicExecutionTest/symbolicExecution/SimpleTest.java
branches/mango/Mango/mangoUserHome/frank/input/default.properties
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/D2I.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/D2L.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DADD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DCMPG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DCMPL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DDIV.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DMUL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DNEG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DREM.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/DSUB.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/F2D.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/F2I.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/F2L.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FADD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FCMPG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FCMPL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FDIV.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FMUL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FNEG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FREM.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/FSUB.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/GETSTATIC.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2B.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2C.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2D.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2F.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2L.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/I2S.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IADD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IAND.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFEQ.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFGE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFGT.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFLE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFLT.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFNE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IFNULL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPEQ.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPGE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPGT.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPLE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPLT.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IF_ICMPNE.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IINC.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IMUL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/INEG.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
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IOR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/ISUB.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/IXOR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/L2D.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/L2F.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/L2I.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LADD.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LAND.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LCMP.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LMUL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LNEG.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LOOKUPSWITCH.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LOR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LSHL.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LSHR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LSUB.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LUSHR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/LXOR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/NEW.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/SwitchInstruction.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/SymbolicStringHandler.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/mango/symbc/bytecode/TABLESWITCH.java
branches/mango/MangoJPF/toc/
branches/mango/MangoJPF/toc/tocconcepts.xml
branches/mango/MangoJPF/toc/tocgettingstarted.xml
branches/mango/MangoJPF/toc/tocreference.xml
branches/mango/MangoJPF/toc/tocsamples.xml
branches/mango/MangoJPF/toc/toctasks.xml
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/JPF_MIRROR.java
branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/symbc/
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-05-15 18:54:50
|
Revision: 1524
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1524&view=rev
Author: frankrimlinger
Date: 2009-05-15 18:54:42 +0000 (Fri, 15 May 2009)
Log Message:
-----------
Detailed work on bridge port of exception handling in progress. But first, need to figure out exactly how the contruction of the total graph is to proceed. The first point is that the intermediate Branch class is to be completely eliminated. There will be a 1-1 binding between Instructions and total graph vertices. Instead of creating branches, just immediately punch in the corresponding edge between vertices. This amounts to wiring in the correct phase1 code at the moment branches are currently created, and creating total vertex peers for the instructions on demand. To avoid calling buildFormalPeer more than once, define an Hitem formalPeer member which represents the state transition. That way we can grab it when necessary and also know when it has already been created.
Start by defining exactly what happens when jpf calls the mango hooks.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/javaModel/jvmSyntax/attributes/Code_attribute.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWCREATOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/ATHROWHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecodeSynthetic/INVOKETARGET.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-03 03:02:16
|
Revision: 1586
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1586&view=rev
Author: frankrimlinger
Date: 2009-06-03 03:02:12 +0000 (Wed, 03 Jun 2009)
Log Message:
-----------
Minor repairs to Mango project to it running again after changes to location of jar plugins. Discovered that the missing super vertices were created when Mango build the source code graphs, as a side effect. Since MangoJPF isn't going to create these graphs at all, it must create these vertices another way. Already a fix is in place to create the SuperVertexSyms, so just need to create and bind the vertices at this time.
Modified Paths:
--------------
branches/mango/Mango/.classpath
branches/mango/Mango/META-INF/MANIFEST.MF
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graphic/Graphic.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/SuperVertexClassSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/SuperVertex.java
branches/mango/Mango/Mango.product
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-03 15:24:06
|
Revision: 1589
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1589&view=rev
Author: frankrimlinger
Date: 2009-06-03 15:23:56 +0000 (Wed, 03 Jun 2009)
Log Message:
-----------
MangoJPF now survives phase1. Supervertices are posting to the entrypoints window, but not the method graphs. Need to take a look at these before unleashing phase2.
HACK in MethodSym revealChildren in order to look at method graphs.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/SuperVertex.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/WorkerControl.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/graphic/MethodSym.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/AbstractUconMethod.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BadMethod.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/OSmethod.java
branches/mango/MangoJPF/src/mango/views/GlobalViewWindow.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-03 23:46:53
|
Revision: 1591
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1591&view=rev
Author: frankrimlinger
Date: 2009-06-03 23:46:51 +0000 (Wed, 03 Jun 2009)
Log Message:
-----------
MangoJPF survives the loop subdivision algorithm of phase2, and the components for itsAWrap.clear and the itsAWrap.clear loop both graph properly, as compared against the same graphs from Mango.
Next bug is in the stratification alg. Eventually stratification will be dropped, but I have to fix it now to finish all the baseline tests. Cannot move on before this.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/graph/Graph.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-06 07:17:48
|
Revision: 1602
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1602&view=rev
Author: frankrimlinger
Date: 2009-06-06 07:17:40 +0000 (Sat, 06 Jun 2009)
Log Message:
-----------
2D graphs now working for both Mango and MangoJPF. Controlled by static flag in Mango, which is so Stone Age, and by prefernece in MangoJPF, which is nice because it is "hot" in that preference change is reflected if containing folder is closed and reopened.
Modified Paths:
--------------
branches/mango/Mango/META-INF/MANIFEST.MF
branches/mango/Mango/Mango/src/mango/worker/Mango.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperBlowUpSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperEntrySym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperLoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperStrataSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperBlowUpSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperEntrySym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperLoopSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperStrataSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java
branches/mango/MangoJPF/src/mango/preferences/GeneralPreferencePage.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-11 20:50:49
|
Revision: 1613
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1613&view=rev
Author: frankrimlinger
Date: 2009-06-11 20:50:47 +0000 (Thu, 11 Jun 2009)
Log Message:
-----------
Still working on wonderfully subtle rewriting bug in MangoJPF. Fortunately, a comparison with Mango yields a unification failure very early on. Detailed analysis of exactly what the unifier does in the two different programs is in progress. To reproduce, open the itsAWrap.main predicate transformer in a separate window, then
1. opening up to the first codeSym
2. unconditionally rewrite codeSym
3. turn on hits
4. unconditionally rewrite (o codeSym pathSym)
The trouble is that when pathSym is interpreted, it is supposed to be typed as state. This typing never kicks in MangoJPF, so composition doesn't fire, and the day is lost.
Why?
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/engine/events/RewriteEvent.java
branches/mango/Mango/Mango/src/mango/worker/engine/unifier/ActionCallBack.java
branches/mango/Mango/Mango/src/mango/worker/engine/unifier/UnifyEvent.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/MangoJPF/Mango/src/mango/worker/engine/events/RewriteEvent.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/unifier/ActionCallBack.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/unifier/UnifyEvent.java
Added Paths:
-----------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/baseline/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-12 03:27:07
|
Revision: 1615
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1615&view=rev
Author: frankrimlinger
Date: 2009-06-12 03:27:03 +0000 (Fri, 12 Jun 2009)
Log Message:
-----------
Solved the MangoJPF rewriter bug. The trouble was I decided that "manual block mode" had not been used in years and so could be dropped from support in the MangoJPF gui. Since this broke some code, I just happily deleted all code that referred to the corresponding boolean flag. But the devil came knocking at my door. Because UnifyEvent calls isManuallyBlocked, which calls manualBlockMode(), which in Mango always returns false. This causes isManuallyBlocked to return false. Trouble is, pulling this code out of MangoJPF just caused control flow to go on to the rest of the routine. The idea is that when manual block mode is on, UconSym and PathSym won't interpret. This was helpful long ago when debugging certain composition issues. But now it just stops the rewriter dead in its tracks.
How it could possibly be that this failure mode did not occur while rewriting the ItsAWrap loop is a tremendous mystery that will never be investigated.
To solve the problem, just reinstated manualBlockMode(), so that it always returns false, and restored calls to this routine. This way, if I ever *want* this feature again, the hook is in place.
Anticipating other damage caused by the initial reckless act, also reinstated semiAutoBlockMode() and autoBlockMode. In Mango, all three of these routines always return false, because the actual flag is an unblockStateCode_t that is always null, as it was never hooked up to the vestigial gui.
There were no calls to semiAutoBlockMode() in Mango, so no harm no foul. The calls to autoBlockMode() have been reinstated.
In the legacy code, semiAutoBlockMode is the default, so even though it is never called, it returns true in MangoJPF. manualBlockMode and autoBlockMode return false.
Lesson learned: A firm grasp of what is view and what is model is essential to success. Happily, with these repairs in place, the initial rewritten predicate transformer for ItsAWrap.clear looks good. So, onward.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/engine/unifier/UnifyEvent.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/simpleSubstitution/SUBRautomatic.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/sym/InterpretableSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/unifier/UnifyEvent.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-12 18:06:25
|
Revision: 1616
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1616&view=rev
Author: frankrimlinger
Date: 2009-06-12 18:06:21 +0000 (Fri, 12 Jun 2009)
Log Message:
-----------
Reinstated clear on reset for Entrypoints window and Session window.
Generated MangoJPF session for ItsAWrap. clear.
Fixed a rewriting bug in ItsAWrap.main. The bizarre pop2 instruction can only resolve whether it is supposed to pop one or two values during rewriting. For this purpose, the pop2 rulekey was introduced. Unfortunately, many instructions use a local variable pop2 when building the formal peer, and the distinction got confused in MangoJPF. To fix this problem,
1. refactored pop2 to pop2Wide in both Mango and MangoJPF
2. revised rulebase accordingly, in both Mango and MangoJPF
3. fixed the broken rules in MangoJPF. This were easy to find because pop2Wide only occurs in the POP2 formal peer. All the other instances changed to the local variable pop2.
I do remember deleting those pop2 locals now in MangoJPF because they were "not being used". The whole issue came about because when porting to the javapathfinder-mango-bridge, the inheritance structure changed so that references to rulekeys had to be made more explicit. TRICKY!
As an afterthought, this experience shows that making expressions with empty argument lists a syntax error is a good idea after all. Otherwise this error could have taken a long time to diagnose. Checking the syntax of formal peer expresssions with the new MangoInstructionFactory.sanityTest() creates no discernible overhead, and so this feature will be left on.
Next bug: callThisClinit fails to resolve during call to clear() in ItsAWrap.main. No surprise here, as the clinit plumbing has been completely reworked for MangoJPF.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java
branches/mango/Mango/Mango/src/mango/worker/javaModel/byteCodeModel/PopDupSwap.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/META-INF/MangoJPF.product
branches/mango/MangoJPF/Mango/src/mango/worker/GlobalViewModel.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/Cons.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java
branches/mango/MangoJPF/ThreadSupport/src/threadModel/SystemBuilder.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoFormalInterface.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/length of the Array 'x' is greater than or equal to 10.zip
branches/mango/MangoJPF/src/mango/views/GlobalViewWindow.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-13 16:10:55
|
Revision: 1623
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1623&view=rev
Author: frankrimlinger
Date: 2009-06-13 16:10:53 +0000 (Sat, 13 Jun 2009)
Log Message:
-----------
Fixed minor bug in INVOKECLINIT.
Working on itsAWrap.main bug. The problem is basic, in that the clear routine is never invoked. The stratification differs from that of Mango, so this is the place to start.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-14 19:28:34
|
Revision: 1626
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1626&view=rev
Author: frankrimlinger
Date: 2009-06-14 19:28:28 +0000 (Sun, 14 Jun 2009)
Log Message:
-----------
Investigation of the itsAWrap.main invariant bug continues. Have verified that the context free input state for the invocation of itsAWrap.clear is the same in Mango and MangoJPF. However, the input state for MangoJPF is slightly confused. If in fact this is causing the problem, then there is a very unhealthy dependence on context in the invariant mechanism that needs to be fixed. Currently comparing invariant detection success in Mango versus MangoJPF to try and discover exactly when the invariant mechanism gets confused.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/module/msg/DebugInvariantsMsg.java
branches/mango/Mango/Mango/src/mango/worker/Mango.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/Sym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupAlg/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/ConditionalMethodAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/InvariantAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/InvariantHypoAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/LocalVarConditionalEquivalenceAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/MethodInvariantAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/model/InvariantModel.java
branches/mango/MangoJPF/Mango/src/mango/module/msg/DebugInvariantsMsg.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/form/binder/LocalVarBind.java
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/sym/Sym.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/form/sym/binder/executable/LocalVarSym.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/ConditionalMethodAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/InvariantAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/InvariantHypoAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/LocalVarConditionalEquivalenceAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/MethodInvariantAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/model/InvariantModel.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AbstractUconPlace.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-15 19:15:48
|
Revision: 1630
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1630&view=rev
Author: frankrimlinger
Date: 2009-06-15 18:04:38 +0000 (Mon, 15 Jun 2009)
Log Message:
-----------
Finally traced the invariant bug in the case of incorrect context. This was a pretty terrifying bug. It actually occurs in JavaType.getJavaTypeName(), which was incorrectly translated from C++. Specifically, the local variable name "LocalVar_at_offset_1_lineNumber_0", indicating unknown context, was interpreted incorrectly as a class name X, in the Lx; syntax, because we forgot to check for the ";". The bogus type returned was "LocalVar_at_offset_1_lineNumber_0", and then InequivalentRef.inequivalentJavaType() made a "risky" comparison which decide that InequivalentRef.inequivalentJavaType() and "int" were in-equivalent types. This erroneous result in turn allowed HeapModel.totalVacuumService() to garbage collect the heap, which in turn allowed InvariantAgentTest to return a positive result for invariant detection. YIKES!
FWIW, the risky comparison was reported in the log window and the console, and I have been systematically ignoring it for about a week now. So now the warning is much more angry sounding, in the hopes that it will get my attention in the future.
Fixed getJavaTypeName() to check for the ";" before returning a class name, in both Mango and MangoJPF.
With this fix in place, invariant detection operates correctly, so that the conjecture x[5]==x[6] is produced with respect to the itsAWrap loop output heap.
However, can't finish rewriting itsAWrap.main() because get non-deterministic result as the ArrayIndexOutOfBoundsException and NullPointerException don't vanish as they should. This is a known bug that I will get to soon.
FIRST, really need to fix the incorrect context bug, as it leads to unsatisfactory output in the specification window. This is a thankless task as the code will go away with jpf integration, but must establish a baseline.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/module/msg/DebugInvariantsMsg.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentRef.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/JavaType.java
branches/mango/MangoJPF/Mango/src/mango/module/msg/DebugInvariantsMsg.java
branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentRef.java
branches/mango/MangoJPF/Mango/src/mango/worker/engine/events/RewriteEvent.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/ValueHAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/BaseInvariantAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/InvariantTestAgent.java
branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/model/JavaType.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-16 16:08:36
|
Revision: 1634
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1634&view=rev
Author: frankrimlinger
Date: 2009-06-16 16:08:34 +0000 (Tue, 16 Jun 2009)
Log Message:
-----------
Added ACL2 folder for development of strategies for Mango proof artifacts.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
Added Paths:
-----------
branches/mango/MangoJPF/ACL2/
branches/mango/MangoJPF/ACL2/itsAWrap-construct.lisp
branches/mango/MangoJPF/ACL2/itsAWrap-construct.lisp.a2s
branches/mango/MangoJPF/ACL2/mango-model.lisp
branches/mango/MangoJPF/ACL2/mango-model.lisp.a2s
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-17 02:15:57
|
Revision: 1636
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1636&view=rev
Author: frankrimlinger
Date: 2009-06-17 01:48:16 +0000 (Wed, 17 Jun 2009)
Log Message:
-----------
Fixed context problem in itsAWrap.main. The problem was the very ugly issue of "context transition" that will go away when the jpf rewriter kicks in. Specifically the rule "abstract info resolution" has hardcoded literal embedded in subclause ( info "AbstractUconClass.AbstractUconMethod()V" -1 lineage ) which in MangoJPF needs to be (info "AbstractUconMethod()V" -1 lineage ) to account for minor differences in how certain names are generated. No other instances of this literal occur in the rulebase, so hopefully this issue is put to rest. This is a fine example of what a treacherous miserable business context is, even though it is essential for success.
As for the non-deterministic control flow bug, this was diagnosed instantly upon inspection of the 2D control flow diagrams. Sometimes a picture is really worth 1k words. In particular, the exceptional outgoing edges of an instruction that throws exceptions should bind to the branch condition for the exception. This binding was present in Mango but not MangoJPF, as discovered by right clicking on the edges in question. In the old days attempts were sometimes made to label the edges with their branch conditions, but this always made the graph too busy.
It turns out the fix for this bug was sort of there already, just needed a little tune up. Most of the problem stems from really different terminology between Mango and MangoJPF for Instructions:
Mango MangoJPF
lineNumber offset
instructionIndex position
The earlier fix introduction "syntheticPosition" was wrong. What we really need is "syntheticOffset". Also, all the places where you call getLineNumber() in mango have to be translated to getOffset() in MangoJPF, *NOT* getPosition().
Further confusing the matter, jpf uses "lineNumber" to refere to source code lines. Also, the jpf ExceptionHandler class returns positions for ranges, NOT offsets as one might expect when literally translating from JVM2ed. So a conversion has to be made for this.
The offset/position confusion is probably not all sorted out yet.
With all this in place, we still need to force loading of the exception handler tables. JPF is pretty lazy about this. This work is in progress.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/ACL2/itsAWrap-construct.lisp
branches/mango/MangoJPF/ACL2/itsAWrap-construct.lisp.a2s
branches/mango/MangoJPF/ACL2/mango-model.lisp.a2s
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/AbstractUconMethod.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BadMethod.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInterface.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/OSmethod.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AbstractUconPlace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BadPlace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BeginningOfTime.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKETARGET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/OSplace.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SyntheticInstruction.java
branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip
branches/mango/MangoJPF/mangoUserHome/frank/sessions/a.zip
Added Paths:
-----------
branches/mango/MangoJPF/mangoUserHome/frank/sessions/baseline/itsAWrap/main([I)Z/a.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-17 17:03:40
|
Revision: 1641
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1641&view=rev
Author: frankrimlinger
Date: 2009-06-17 17:03:37 +0000 (Wed, 17 Jun 2009)
Log Message:
-----------
There is a bug involving the default package. MangoJPF doesn't seem to find the corresponding .class files, event when one is specified as the target class. For now working around this by moving Marc's exception handler test code to the "extest" package.
The invocation formal peers are not failing gracefully when there are link errors. This needs to be figured out. We may have to punch in the rest of the clinit design sooner rather than later so that popular java.io methods can be sensibly modelled.
Have verified there there is in fact an issue with jpf lazy loading of method exception handlers. This loading is now forced by calling MethodUtil.getExceptions().
In extest.lptry1, Mango is generating exception handler branch conditions as will as well as gracefully handling an invocation of java.ioPrintStream.println(I)V. So this is a good place to start once ItsAWrap.main is working.
Something is causing branch conditions for exceptions to be dropped very early on. This problem has nothing to do with existence of exception handlers or lack thereof.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/sessions/lptry1.zip
branches/mango/MangoJPF/mangoUserHome/marc/arrayCopyShell/src/extest/
branches/mango/MangoJPF/mangoUserHome/marc/arrayCopyShell/src/extest/arrayCopyShell.java
branches/mango/MangoJPF/mangoUserHome/marc/hypo2/src/extest/
branches/mango/MangoJPF/mangoUserHome/marc/hypo2/src/extest/hypo2.java
branches/mango/MangoJPF/mangoUserHome/marc/jar/
branches/mango/MangoJPF/mangoUserHome/marc/jar/extest.jar
branches/mango/MangoJPF/mangoUserHome/marc/jarBuild
branches/mango/MangoJPF/mangoUserHome/marc/lptry1/extest/
branches/mango/MangoJPF/mangoUserHome/marc/lptry1/extest/lptry1.java
branches/mango/MangoJPF/mangoUserHome/marc/lptry2/src/extest/
branches/mango/MangoJPF/mangoUserHome/marc/lptry2/src/extest/lptry2.java
branches/mango/MangoJPF/mangoUserHome/marc/try1/extest/
branches/mango/MangoJPF/mangoUserHome/marc/try1/extest/try1.java
branches/mango/MangoJPF/mangoUserHome/marc/try2/extest/
branches/mango/MangoJPF/mangoUserHome/marc/try2/extest/try2.java
branches/mango/MangoJPF/mangoUserHome/marc/try3/extest/
branches/mango/MangoJPF/mangoUserHome/marc/try3/extest/try3.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk1/extest/
branches/mango/MangoJPF/mangoUserHome/marc/trychk1/extest/trychk1.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk2/extest/
branches/mango/MangoJPF/mangoUserHome/marc/trychk2/extest/trychk2.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk3/extest/
branches/mango/MangoJPF/mangoUserHome/marc/trychk3/extest/trychk3.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk6/extest/
branches/mango/MangoJPF/mangoUserHome/marc/trychk6/extest/trychk6.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk7/extest/
branches/mango/MangoJPF/mangoUserHome/marc/trychk7/extest/trychk7.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk8/extest/
branches/mango/MangoJPF/mangoUserHome/marc/trychk8/extest/trychk8.java
Removed Paths:
-------------
branches/mango/MangoJPF/mangoUserHome/marc/arrayCopyShell/src/arrayCopyShell.java
branches/mango/MangoJPF/mangoUserHome/marc/hypo2/src/hypo2.java
branches/mango/MangoJPF/mangoUserHome/marc/lptry1/lptry1.java
branches/mango/MangoJPF/mangoUserHome/marc/lptry2/src/lptry2.java
branches/mango/MangoJPF/mangoUserHome/marc/try1/try1.java
branches/mango/MangoJPF/mangoUserHome/marc/try2/try2.java
branches/mango/MangoJPF/mangoUserHome/marc/try3/try3.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk1/trychk1.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk2/trychk2.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk3/trychk3.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk6/trychk6.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk7/trychk7.java
branches/mango/MangoJPF/mangoUserHome/marc/trychk8/trychk8.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-18 02:26:57
|
Revision: 1651
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1651&view=rev
Author: frankrimlinger
Date: 2009-06-18 02:26:56 +0000 (Thu, 18 Jun 2009)
Log Message:
-----------
Endowed all test code with java project structures, for both Mango and MangoJPF.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/input/SymbolicExecutionTest/symbolicExecution/SimpleTest.java
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/.classpath
branches/mango/Mango/mangoUserHome/frank/.project
branches/mango/Mango/mangoUserHome/frank/jar/mangoTest.jar
branches/mango/MangoJPF/mangoUserHome/frank/.classpath
branches/mango/MangoJPF/mangoUserHome/frank/.project
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/frank/input/build
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-18 02:50:19
|
Revision: 1650
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1650&view=rev
Author: frankrimlinger
Date: 2009-06-18 01:49:20 +0000 (Thu, 18 Jun 2009)
Log Message:
-----------
Cleanup in preparation for testing of MangoJPF. Mango currently does not depend on any jpf extensions, so the extension plugins have been removed. Cleanup of mangoUserHome.
Modified Paths:
--------------
branches/mango/Mango/META-INF/MANIFEST.MF
branches/mango/Mango/Mango.product
branches/mango/MangoJPF/META-INF/MANIFEST.MF
branches/mango/MangoJPF/META-INF/MangoJPF.product
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/jar/
branches/mango/Mango/mangoUserHome/frank/jarBuild
branches/mango/Mango/mangoUserHome/frank/sessions/marc.zip
branches/mango/Mango/mangoUserHome/frank/sessions/rkrug.zip
branches/mango/Mango/mangoUserHome/marc/
branches/mango/Mango/mangoUserHome/marc/.classpath
branches/mango/Mango/mangoUserHome/marc/.project
branches/mango/Mango/mangoUserHome/marc/arrayCopyShell/
branches/mango/Mango/mangoUserHome/marc/arrayCopyShell/src/
branches/mango/Mango/mangoUserHome/marc/arrayCopyShell/src/extest/
branches/mango/Mango/mangoUserHome/marc/arrayCopyShell/src/extest/arrayCopyShell.java
branches/mango/Mango/mangoUserHome/marc/hypo2/
branches/mango/Mango/mangoUserHome/marc/hypo2/src/
branches/mango/Mango/mangoUserHome/marc/hypo2/src/extest/
branches/mango/Mango/mangoUserHome/marc/hypo2/src/extest/hypo2.java
branches/mango/Mango/mangoUserHome/marc/jar/
branches/mango/Mango/mangoUserHome/marc/jar/extest.jar
branches/mango/Mango/mangoUserHome/marc/jarBuild
branches/mango/Mango/mangoUserHome/marc/lptry1/
branches/mango/Mango/mangoUserHome/marc/lptry1/extest/
branches/mango/Mango/mangoUserHome/marc/lptry1/extest/lptry1.java
branches/mango/Mango/mangoUserHome/marc/lptry2/
branches/mango/Mango/mangoUserHome/marc/lptry2/src/
branches/mango/Mango/mangoUserHome/marc/lptry2/src/extest/
branches/mango/Mango/mangoUserHome/marc/lptry2/src/extest/lptry2.java
branches/mango/Mango/mangoUserHome/marc/try1/
branches/mango/Mango/mangoUserHome/marc/try1/extest/
branches/mango/Mango/mangoUserHome/marc/try1/extest/try1.java
branches/mango/Mango/mangoUserHome/marc/try2/
branches/mango/Mango/mangoUserHome/marc/try2/extest/
branches/mango/Mango/mangoUserHome/marc/try2/extest/try2.java
branches/mango/Mango/mangoUserHome/marc/try3/
branches/mango/Mango/mangoUserHome/marc/try3/extest/
branches/mango/Mango/mangoUserHome/marc/try3/extest/try3.java
branches/mango/Mango/mangoUserHome/marc/trychk1/
branches/mango/Mango/mangoUserHome/marc/trychk1/extest/
branches/mango/Mango/mangoUserHome/marc/trychk1/extest/trychk1.java
branches/mango/Mango/mangoUserHome/marc/trychk2/
branches/mango/Mango/mangoUserHome/marc/trychk2/extest/
branches/mango/Mango/mangoUserHome/marc/trychk2/extest/trychk2.java
branches/mango/Mango/mangoUserHome/marc/trychk3/
branches/mango/Mango/mangoUserHome/marc/trychk3/extest/
branches/mango/Mango/mangoUserHome/marc/trychk3/extest/trychk3.java
branches/mango/Mango/mangoUserHome/marc/trychk6/
branches/mango/Mango/mangoUserHome/marc/trychk6/extest/
branches/mango/Mango/mangoUserHome/marc/trychk6/extest/trychk6.java
branches/mango/Mango/mangoUserHome/marc/trychk7/
branches/mango/Mango/mangoUserHome/marc/trychk7/extest/
branches/mango/Mango/mangoUserHome/marc/trychk7/extest/trychk7.java
branches/mango/Mango/mangoUserHome/marc/trychk8/
branches/mango/Mango/mangoUserHome/marc/trychk8/extest/
branches/mango/Mango/mangoUserHome/marc/trychk8/extest/trychk8.java
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/frank/input/default.properties
branches/mango/Mango/repository/
branches/mango/MangoJPF/mangoUserHome/frank/input/build
branches/mango/MangoJPF/mangoUserHome/marc/jar/
branches/mango/MangoJPF/mangoUserHome/marc/jarBuild
branches/mango/MangoJPF/mangoUserHome/rkrug/input/jar/
branches/mango/MangoJPF/mangoUserHome/rkrug/input/jarBuild
branches/mango/MangoJPF/mangoUserHome/rkrug/rules/
branches/mango/MangoJPF/mangoUserHome/rkrug/sessions/
branches/mango/MangoJPF/mangoUserHome/system/input/jar/
branches/mango/MangoJPF/mangoUserHome/system/input/jarBuild
branches/mango/MangoJPF/mangoUserHome/system/rules/
branches/mango/MangoJPF/mangoUserHome/system/sessions/
branches/mango/MangoJPF/plugins/javapathfinder_trunk_extensions_symbc_lib_update1_1.0.0.jar
branches/mango/MangoJPF/plugins/jpf_trunk_extensions_concolic_1.0.0.jar
branches/mango/MangoJPF/plugins/jpf_trunk_extensions_symbc_1.0.0.jar
branches/mango/MangoJPF/plugins/jpf_trunk_extensions_symbolic_1.0.0.jar
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-19 02:15:50
|
Revision: 1663
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1663&view=rev
Author: frankrimlinger
Date: 2009-06-19 01:04:19 +0000 (Fri, 19 Jun 2009)
Log Message:
-----------
Quickly realized that the formal requirement of Mango and the operational requirements of JPF just will not blend, so abandoning attempts to create a hybrid environment. The new plan is to introduce
ClassInfo ClassUtil.getFormalPeer(ClassInfo clazz)
MethodInfo MethodUtil. getFormalPeer(MethodInfo method)
These routines prepend "MangoFormal." to the name of the class of the passed object if not already present. So, for example, java.lang.Boolean.toString becomes java.lang.MangoFormalBoolean.toString. If the Class or Method with the revised name is found, then the corresponding ClassInfo or MethodInfo is returned. Otherwise the input value is returned. This allows classes designed to support formal analysis to mask previously existing classes.
The point is that mango knows when it wants the formal version and can ask for it, just like jpf "knows" when it wants MethodInfo instead of Method. The new strategy is completely transparent to jpf, unlike the misguided attempt to blend. However, in the MangoJPF code base, except for some code which actually controls the jpf operation, all access to MethodInfo and ClassInfo objects must be routed through the above methods. ?\194?\160?\194?\160This is going to be a fair amount of work to get right, but the payoff will be complete flexibility to mask or not mask the jpf environment without ever interfering with jpf internals.
Deleted existing mangoUserHome/system code to get a fresh start for conversion to MangoFormal names.
Modified Paths:
--------------
branches/mango/MangoJPF/mangoUserHome/system/.classpath
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/sessions/system.zip
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/Mango/mangoUserHome/frank/sessions/lptry1.zip
branches/mango/MangoJPF/mangoUserHome/system/System/
branches/mango/MangoJPF/mangoUserHome/system/SystemTests/src/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-01 04:40:01
|
Revision: 1708
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1708&view=rev
Author: frankrimlinger
Date: 2009-07-01 04:39:26 +0000 (Wed, 01 Jul 2009)
Log Message:
-----------
Bug #1 was that the branch from an invocation instruction to the ACATCHHANDLER was not fed to the choice generated, so the SCANNER never had a chance to scan the exception handler code. There is a subtle point here. If you feed a branch to the choice generator, then updateMangoModel will be called automatically for that branch, so DO NOT call it directly. On the other hand, the branch from an invocation to the (potentially) called routine(s) are NOT passed to the choice generator since method entrypoints are handled separately by the TargetChoiceGenerator. So for these branches, you MUST call updateMangoModel directly.
Bug #2 was that the ACATCHHANDLER execute routine was just returning null. What it is supposed to do is feed the branches to the choice generated that were created by the invocation instruction buildFormalPeer call to createACatchHandlerBranching(). Ditto for ATHROWCREATOR
The fix for bug#2 is in place. Bug#1 is harder because it involves some tricky chicken-and-egg issues. This fix is in progress.
Some parts of the returnPointLink mechanism appear to be obsolete in the C++ code. Some parts of the returnPointLink mechanism are definitely still functional. Eventually this murky issue must be unravelled.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/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.
|
Thanks for helping keep SourceForge clean.
X