Menu
▾
▴
javapathfinder-svn
|
From: <fra...@us...> - 2009-08-27 02:47:50
|
Revision: 1859
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1859&view=rev
Author: frankrimlinger
Date: 2009-08-27 02:47:43 +0000 (Thu, 27 Aug 2009)
Log Message:
-----------
Fixed bug in ATRHOWCREATOR that cause a thrown exception to be placed on the called frame instead of the caller frame.
Fixed "special" subaddress translation bug.
Completed testing of Class_MangoFormal.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/control/action/input/RuleBaseAction.java
branches/mango/Mango/Mango/src/mango/core/CoreMangoActiveObject.java
branches/mango/Mango/Mango/src/mango/core/CoreRule.java
branches/mango/Mango/Mango/src/mango/core/CoreRuleBase.java
branches/mango/Mango/Mango/src/mango/core/gui/action/NewCoreRuleAction.java
branches/mango/Mango/Mango/src/mango/module/model/ModuleManager.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateValueH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEnterpriseAndTranslation.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/Sym.java
branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/Mango/Mango/src/mango/worker/msg/RulebaseMsg.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/sym/TranslationSym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/clazz is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/clazz is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsFalse()Z/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsFalse()Z/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsTrue()Z/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsTrue()Z/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class_MangoFormal;)Z/clazz is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class_MangoFormal;)Z/clazz is undefined.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-08-27 03:52:02
|
Revision: 1860
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1860&view=rev
Author: frankrimlinger
Date: 2009-08-27 03:51:56 +0000 (Thu, 27 Aug 2009)
Log Message:
-----------
As usual, "_MangoFormal" suprressed. Preliminary to rehab of Object class, devised a tricky test of Class.getComponent:
public String intComponentTest(){
Class<?> clazz=int[].class.getComponentType();
boolean test=(clazz.equals(Integer.TYPE));
if(test){
return clazz.getName();
}
return "failed";
}
In order to specify this, assuming that Class.equals() just delegates to Object.equals(). BUG: the zen question, is equals(Ljava/lang/Object)Z accessible to the class int, is causing some trouble.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/AssignNotObjectValue.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/Mango/mangoUserHome/system/System/java/lang/Object_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/reflect/Array_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/SystemTests/src/systemTests/ClassTests.java
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/byteValue()B/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/byteValue()B/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/obj is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/obj may not be cast to java.lang.Byte_MangoFormal.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/this._value does not equal obj._value.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Byte_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/this._value equals obj._value.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-08-27 22:46:36
|
Revision: 1861
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1861&view=rev
Author: frankrimlinger
Date: 2009-08-27 22:46:22 +0000 (Thu, 27 Aug 2009)
Log Message:
-----------
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/control/action/input/RuleBaseAction.java
branches/mango/Mango/Mango/src/mango/core/CoreRule.java
branches/mango/Mango/Mango/src/mango/module/definition/action/CloseBothAction.java
branches/mango/Mango/Mango/src/mango/module/definition/action/CloseCaseAction.java
branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/msg/CloseCaseMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/msg/CloseCaseTranslateMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/msg/DeleteUnusedParametersMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/trap/CloseCaseConnector.java
branches/mango/Mango/Mango/src/mango/module/definition/trap/HarvestParametersTrap.java
branches/mango/Mango/Mango/src/mango/module/definition/trap/ScriptedCloseCaseConnector.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeMethod.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/MakeComponentClass.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/string/GetCanonicalTypeName.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/Quotes.java
branches/mango/Mango/Mango/src/mango/script/gui/action/ScriptOpenAction.java
branches/mango/Mango/Mango/src/mango/script/gui/action/ScriptSaveAction.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/Mango/Mango/src/mango/worker/msg/RulebaseMsg.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/trap/BuildInvariantNamesConnector.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/trap/BuildInvariantNamesTrap.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/agent/TranslateModuleAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/sym/TranslationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/trap/ScriptedTranslateTrap.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/trap/TranslateTrap.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/className is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class_MangoFormal;)Z/cls is defined.zip
branches/mango/Mango/mangoUserHome/system/SystemTests/src/systemTests/ClassTests.java
branches/mango/Mango/src/mango/views/GenSpecWindow.java
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/booleanValue()Z/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/booleanValue()Z/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/obj is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/obj may not be cast to java.lang.Boolean_MangoFormal.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/this._value does not equal obj._value.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Boolean_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/this._value equals obj._value.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/Final case. className is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/Final case. this is not an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/this is an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class_MangoFormal;)Z/Final case. cls is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/obj is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/obj may not be cast to java.lang.Integer_MangoFormal.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/this._value does not equal obj._value.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/this._value equals obj._value.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/intValue()I/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Integer_MangoFormal/intValue()I/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse()Z/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse(Ljava.lang.Class_MangoFormal;Ljava.lang.Class_MangoFormal;)Z/Final case. x is defined, y is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleTrue()Z/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class_MangoFormal;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/Final case. clazz is an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/clazz is not an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/clazz is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class_MangoFormal;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String_MangoFormal;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest()Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest()Ljava.lang.String_MangoFormal;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest2()Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest2()Ljava.lang.String_MangoFormal;/Final case.zip
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/className is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/Class name of this is an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/Class name of this is not a loadable class.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class_MangoFormal;)Z/cls is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse()Z/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse(Ljava.lang.Class_MangoFormal;Ljava.lang.Class_MangoFormal;)Z/x is defined, y is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleTrue()Z/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/Class name of clazz is an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/clazz is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/clazz is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsFalse()Z/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsTrue()Z/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveFalse()Z/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/a.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/case.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-08-28 03:26:45
|
Revision: 1863
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1863&view=rev
Author: frankrimlinger
Date: 2009-08-28 03:26:37 +0000 (Fri, 28 Aug 2009)
Log Message:
-----------
Another tweak to ATHROWCREATOR. The issue is whether or not the originating instruction of the throw is an invocation or not. If it is an invocation, then a frame has already been set up for the called method, and we need to pop that frame *before* setting up the exception. But if the originating instruction is NOT an invocation, then ATHROWCREATE just puts the exception on the current frame.
NB: this has nothing to do with an exception thrown but not caught within the called method. These are handled by a different mechanism.
This issue has been bouncing around all summer. I finally get it.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/objI is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/Final case. className is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/className is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/Final case. clazz is an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/clazz is not an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class_MangoFormal;)Ljava.lang.Class_MangoFormal;/clazz is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String_MangoFormal;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest2()Ljava.lang.String_MangoFormal;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class_MangoFormal;)Z/clazz is defined.zip
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Final case. objI may be cast to I.zip
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/objI may not be cast to I.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/Final case. clazz is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class_MangoFormal;)Z/clazz is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsFalse()Z/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsTrue()Z/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class_MangoFormal;)Z/Final case. clazz is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveFalse()Z/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/Final case.zip
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/<init>()V/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Class name of objI may be cast to I.zip
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Class name of objI may not be cast to I.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(LI;)I/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may be cast to I.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may not be cast to I.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/compareTo_LocalVar_at_offset_1_lineNumber_1 is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens()Ljava.lang.Class_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens1()Ljava.lang.Class_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens2()Ljava.lang.Class_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens3()Ljava.lang.Class_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class_MangoFormal;)Z/clazz is undefined.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-08-28 19:59:47
|
Revision: 1864
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1864&view=rev
Author: frankrimlinger
Date: 2009-08-28 19:59:39 +0000 (Fri, 28 Aug 2009)
Log Message:
-----------
Realized that most of the MangoFormal aliasing the system source code is very harmful and very unnecessary. At some point, lost sight of the design goal of aliasing, which is simply to allow the class loader to admit both the real and the aliased system classes. The burden on Mango is then to ensure that all formal analysis is done using the aliased class methods, not the real ones.
Therefore, the only thing that needs to be aliased within the source code are
1) the actual name of the class within the class declaration, and to the extent there are package visibility issues, the names of the extended classes
2) final methods that cannot be overloaded,
3) constructor method names, which of course must be the same as the aliased class name,
4) anything else I can't think of right now.
TODO eliminating all method name, field name, and signature aliasing in the system source code. The only final method that gets the treatment is getClass_MangoFormal(). START WITH Double_MangoFormal.
TODO: Simplify MangoMethodPeer, which is supposed to produced the aliased methods. Signature aliasing is no longer necessary. It is only necessary to alias getClass to getClass_MangoFormal. Since the JVM patches in the constructors, they are not an issue. End of story.
Completed native implementation of Object_MangoFormal. Created new class mango.lang.reflect.Mango_Array for native array accessors. Created mango.io.Mango_PrintStream to provide native buffer support.
Complete rewrite of Array_MangoFormal to use new native accessors.
Another issue has to do with "this". If you are going to pass "this" to another method, you might have to wrap with a native method like so
XXX formal2nominal(XXX_MangoFormal obj){}
The native implementation just returns obj, but the declaration at the source code level is enough to fake out the compiler. Probably this issue is what started the signature aliasing business, but clearly the new solution is bfc.
Put all the required formal2nominal methods in the native support class mango.lang.Mango_Object
NB: Of course it is ok for native support to have _MangoFormal in signatures if this helps avoid formal2nominal wrappers.
Final thought: you could always write your own class loader, but it would have to be integrated into jpf core and it really does not belong there.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/MakeClass.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hash.java
branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/CompositionImplication.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/StableImplication.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/TemplateImplication.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/system/System/java/io/FileOutputStream_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/io/FilterOutputStream_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/io/InputStream_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/io/ObjectStreamClass_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/io/OutputStream_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/io/PrintStream_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Boolean_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Byte_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/CharSequence_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Character_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/ClassCastException_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Class_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Double_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Object_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/reflect/Array_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Byte.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Class.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/HashCode.java
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal()Ljava.lang.Class_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal()Ljava.lang.Class_MangoFormal;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal([Ljava.lang.Object_MangoFormal;)Ljava.lang.Class_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal([Ljava.lang.Object_MangoFormal;)Ljava.lang.Class_MangoFormal;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getLength(Ljava.lang.Object_MangoFormal;)I/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getLength(Ljava.lang.Object_MangoFormal;)I/Final case.zip
branches/mango/Mango/mangoUserHome/system/System/mango/io/
branches/mango/Mango/mangoUserHome/system/System/mango/io/Mango_PrintStream.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/reflect/
branches/mango/Mango/mangoUserHome/system/System/mango/lang/reflect/Mango_Array.java
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Boolean.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Object.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-08-29 18:48:36
|
Revision: 1866
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1866&view=rev
Author: frankrimlinger
Date: 2009-08-29 18:48:30 +0000 (Sat, 29 Aug 2009)
Log Message:
-----------
More _MangoFormal cleanup.
Defeated the generation of formal signatures by altering MangoMethodPeer.toFormalSignature(). Also changed methodName2FormalMethodName() so that toString() is no longer altered. Tweaked a few methods in the mango system package that DO require _MangoFormal on some signatures.
Cleared out obsolete sessions.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/engine/rule/TemplateRule.java
branches/mango/Mango/Mango/src/mango/worker/engine/rule/Tier.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/MethodSym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/Array length of x is greater than or equal to 10.zip
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8- dload_i_Code_01/op0 is less than 10.zip
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/main([I)Z/Final case. x[5] equals x[6].zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String;)Ljava.lang.Class;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String;)Ljava.lang.Class;/Final case. className is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String;)Ljava.lang.Class;/className is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getName()Ljava.lang.String;/
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.xml
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/
branches/mango/Mango/mangoUserHome/frank/sessions/I/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getName()Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class_MangoFormal;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal()Ljava.lang.Class_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/getClass_MangoFormal([Ljava.lang.Object_MangoFormal;)Ljava.lang.Class_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-08-29 22:01:48
|
Revision: 1867
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1867&view=rev
Author: frankrimlinger
Date: 2009-08-29 22:01:41 +0000 (Sat, 29 Aug 2009)
Log Message:
-----------
Added logic to use the declared type of a local variable when resolving possible methods for getVirtualRunTimeMethod. This is just a patch, don't really intend to settle this issue in MangoBaseline. Once jpf simulation is driving specification, it will be possible just to specify all the plausible choices without a lot of user interaction.
Rebuilt all sessions. System methods and signatures are no longer burdened with the _MangoFormal notation, so now the system specification should grow rapidly.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/engine/rule/AssumeEquivRule.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/agent/AutoAssumeEquivalenceAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/agent/TranslateModuleAgent.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Final case. objI may be cast to I.zip
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/objI is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/objI may not be cast to I.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/
branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(LI;)I/
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(LI;)I/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object;)I/
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object;)I/Final case. compareTo_LocalVar_at_offset_1_lineNumber_1 may not be cast to I.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object;)I/compareTo_LocalVar_at_offset_1_lineNumber_1 is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object;)I/compareTo_LocalVar_at_offset_1_lineNumber_1 may be cast to I.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens()Ljava.lang.Class;/
branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens()Ljava.lang.Class;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens1()Ljava.lang.Class;/
branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens1()Ljava.lang.Class;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens2()Ljava.lang.Class;/
branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens2()Ljava.lang.Class;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens3()Ljava.lang.Class;/
branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens3()Ljava.lang.Class;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class;/Final case. this is not an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class;/this is an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class;)Z/Final case. cls is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class;)Z/cls is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/equals(Ljava.lang.Object;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/equals(Ljava.lang.Object;)Z/Final case. this does not equal obj.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/equals(Ljava.lang.Object;)Z/this equals obj.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse()Z/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse()Z/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse(Ljava.lang.Class;Ljava.lang.Class;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse(Ljava.lang.Class;Ljava.lang.Class;)Z/Final case. x is defined, y is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleTrue()Z/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleTrue()Z/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class;/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class;)Ljava.lang.Class;/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class;)Ljava.lang.Class;/Final case. clazz is not an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class;)Ljava.lang.Class;/clazz is an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class;)Ljava.lang.Class;/clazz is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class;/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String;/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest()Ljava.lang.String;/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest()Ljava.lang.String;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest2()Ljava.lang.String;/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest2()Ljava.lang.String;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class;)Z/Final case. clazz is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class;)Z/clazz is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsFalse()Z/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsFalse()Z/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsTrue()Z/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsTrue()Z/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class;)Z/Final case. clazz is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class;)Z/clazz is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveFalse()Z/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveFalse()Z/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/
branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/Final case.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-08-30 03:57:22
|
Revision: 1868
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1868&view=rev
Author: frankrimlinger
Date: 2009-08-30 03:57:14 +0000 (Sun, 30 Aug 2009)
Log Message:
-----------
Its always nice when Mango "does something". Here is an example of how errors can be caught. I wrote the following utility to check for the usual array errors:
static public void check(Object array, int index){
if(!array.getClass().getComponentType().isArray()){
throw new IllegalArgumentException();
}
if(index<0 || index>=getLength(array)){
throw new ArrayIndexOutOfBoundsException();
}
}
Here is what mango had to say
Hypothesis: Class-object array is an array
Hypothesis: component class of Class-object array is an array
This is as far as I got, because I just wanted "array" to be an array. Just seeing the same thing written a different way is often enough to break the spell.
Fixed bug where rewriter would fail silently because expected method definition not found in rule base. Now it fails with some noise. This happens for example when an exception is thrown that has not been modelled in the rulebase.
Modelled requisite exception constructors and completed spec for utility method mango.lang.reflect.Mango_Array.check()
Just for the record, including the spec summary here. It is more to read than the original code, true, but the information is organized differently and maybe this is worth something. But even if the final dump of information is worthless, the act of generating it is valuable. So FULL automation is not the goal, the goal is to feed the information at a rate the mind can easily assimilate. (automatic assumptions suppressed, these are too dull to read)
check(Ljava/lang/Object;I)V
cases
Final case. index is less than Array length of array
hypotheses
index is less than Array length of array
index is greater than or equal to 0
Class-object array is an array
array is defined
No return value.
index is greater than or equal to Array length of array
hypotheses
index is greater than or equal to Array length of array
index is greater than or equal to 0
Class-object array is an array
array is defined
Throws: java.lang.ArrayIndexOutOfBoundsException.
Class-object array is not an array
hypotheses
Class-object array is not an array
array is defined
Throws: java.lang.IllegalArgumentException.
index is less than 0
hypotheses
index is less than 0
Class-object array is an array
array is defined
Throws: java.lang.ArrayIndexOutOfBoundsException.
array is undefined
hypotheses
array is undefined
Throws: java.lang.NullPointerException.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/ruleAction/translate/automatic/MethodCallAssumption.java
branches/mango/Mango/Mango/src/mango/worker/engine/rule/AssumeEquivRule.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/WorkFlowUtil.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/system/System/java/lang/IllegalStateException_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/reflect/Mango_Array.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/ruleAction/translate/automatic/MethodCallAssumptionClassObject.java
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/Assign_formal_classObject.java
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/ArrayIndexOutOfBoundsException_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/ArrayIndexOutOfBoundsException_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/ArrayIndexOutOfBoundsException_MangoFormal/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IllegalArgumentException_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IllegalArgumentException_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IllegalArgumentException_MangoFormal/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IndexOutOfBoundsException_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IndexOutOfBoundsException_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IndexOutOfBoundsException_MangoFormal/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/Mango_String/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/Mango_String/formal2nominal(Ljava.lang.String_MangoFormal;)Ljava.lang.String;/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/Mango_String/formal2nominal(Ljava.lang.String_MangoFormal;)Ljava.lang.String;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/check(Ljava.lang.Object;I)V/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/check(Ljava.lang.Object;I)V/Class-object array is not an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/check(Ljava.lang.Object;I)V/Final case. index is less than Array length of array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/check(Ljava.lang.Object;I)V/array is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/check(Ljava.lang.Object;I)V/index is greater than or equal to Array length of array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/check(Ljava.lang.Object;I)V/index is less than 0.zip
branches/mango/Mango/mangoUserHome/spec
branches/mango/Mango/mangoUserHome/system/System/java/lang/ArrayIndexOutOfBoundsException_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/IllegalArgumentException_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/IndexOutOfBoundsException_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/RuntimeException_MangoFormal.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-08-31 03:21:29
|
Revision: 1869
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1869&view=rev
Author: frankrimlinger
Date: 2009-08-31 03:21:21 +0000 (Mon, 31 Aug 2009)
Log Message:
-----------
Cleanup of system code to make sure all methods targeted for native implementation throw IllegalStateException. There are dozens if not hundreds of these, but just a few at a time go a long way.
Completed spec of Mango_Array.isType(). Wrote native implementation for Mango_Array.getShort(). Fixed a mispelled rulekey name that was interfering with garbage collection. Nasty. Fixed Checkcast action to return 't or 'f, NOT 1 or 0.
Next bug: Rewriter compression problem, a.zip.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/Checkcast.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeException.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetInterfaceRunTimeMethod.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeException.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeMethod.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/Equals.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashStable.java
branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/Mango/mangoUserHome/system/System/java/io/FileOutputStream_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/io/FilterOutputStream_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/io/InputStream_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/io/ObjectStreamClass_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/io/OutputStream_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/io/PrintStream_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Boolean_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Byte_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Character_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Double_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Float_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Integer_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Long_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Math_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Short_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/StringBuffer_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/StringBuilder_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/String_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/System_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/math/BigInteger_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/net/URI_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/util/ArrayList_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/mango/io/Mango_PrintStream.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Integer.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Short.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_StringBuffer.java
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/rules/rulebase (original) 2.zip
branches/mango/Mango/mangoUserHome/frank/rules/rulebase (original).zip
branches/mango/Mango/mangoUserHome/frank/sessions/a
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/reflect/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/reflect/Array_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/reflect/Array_MangoFormal/getShort(Ljava.lang.Object;I)S/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/io/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/io/Mango_PrintStream/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/io/Mango_PrintStream/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/io/Mango_PrintStream/<init>()V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/io/Mango_PrintStream/append(Ljava.io.PrintStream_MangoFormal;Ljava.lang.String;)V/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/io/Mango_PrintStream/append(Ljava.io.PrintStream_MangoFormal;Ljava.lang.String;)V/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/get(Ljava.lang.Object;I)Ljava.lang.Object;/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/get(Ljava.lang.Object;I)Ljava.lang.Object;/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/get(Ljava.lang.Object;I)Ljava.lang.Object;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getBoolean(Ljava.lang.Object;I)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getBoolean(Ljava.lang.Object;I)Z/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getByte(Ljava.lang.Object;I)B/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getByte(Ljava.lang.Object;I)B/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getChar(Ljava.lang.Object;I)C/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getChar(Ljava.lang.Object;I)C/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getDouble(Ljava.lang.Object;I)D/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getDouble(Ljava.lang.Object;I)D/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getFloat(Ljava.lang.Object;I)F/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getFloat(Ljava.lang.Object;I)F/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getInt(Ljava.lang.Object;I)I/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getInt(Ljava.lang.Object;I)I/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getLong(Ljava.lang.Object;I)J/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getLong(Ljava.lang.Object;I)J/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getShort(Ljava.lang.Object;I)S/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/getShort(Ljava.lang.Object;I)S/Final case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/isType(Ljava.lang.Object;Ljava.lang.String;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/isType(Ljava.lang.Object;Ljava.lang.String;)Z/Class-object array is not an array.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/isType(Ljava.lang.Object;Ljava.lang.String;)Z/Final case. component class of Class-object array does not equal type.value.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/isType(Ljava.lang.Object;Ljava.lang.String;)Z/array is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/isType(Ljava.lang.Object;Ljava.lang.String;)Z/component class of Class-object array equals type.value.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/isType(Ljava.lang.Object;Ljava.lang.String;)Z/type is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/lang/reflect/Mango_Array/isType(Ljava.lang.Object;Ljava.lang.String;)Z/type may not be cast to java.lang.String.zip
branches/mango/Mango/mangoUserHome/frank/sessions/mango/util/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/util/Mango_ArrayList/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/util/Mango_ArrayList/add(Ljava.lang.Object;Ljava.lang.Object;)V/
branches/mango/Mango/mangoUserHome/frank/sessions/mango/util/Mango_ArrayList/add(Ljava.lang.Object;Ljava.lang.Object;)V/Final case.zip
branches/mango/Mango/mangoUserHome/system/cheatsheet.txt
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/spec
branches/mango/Mango/mangoUserHome/system/System/java/lang/CharSequence_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/mango/cheat_sheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Class.forName worksheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.append(str1,str2) worksheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.arraySyntax worksheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.charAt worksheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.setValueFromStringBuffer worksheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_StringBuffer.append worksheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_StringBuffer.length worksheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/lang/toCharArray Worksheet (Autosaved)
branches/mango/Mango/mangoUserHome/system/System/mango/lang/toCharArray Worksheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/util/Mango_ArrayList.add worksheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/util/Mango_ArrayList.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-01 20:35:24
|
Revision: 1883
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1883&view=rev
Author: frankrimlinger
Date: 2009-09-01 20:35:17 +0000 (Tue, 01 Sep 2009)
Log Message:
-----------
Trip down memory lane. Back in 2002, if I had realized that the graphs I was building could be acted on by jpf, a lot of trouble could have been saved, but oh well. The first order of business is to reconstruct the graph of an innermost loop. Innermost loops are trivially embedded in the control flow, in the sense that they can be collapsed without creating new loops. The sequences of edges representing an innermost loop still exists as the Path.cass graphic of the corresponding LoopSym, but the Graph adapter code is missing. Probably was too funky to survive translation from C++.
Reintroduced the corresponding SuperPathSym, which may now be accessed by opening the LoopSym of the innermost loop. The edge sequence generated by an innermost loop is now a SimpleLoopPath extending Path, which is now abstract. The reason Path is made abstract is so it can have the abstract method getEntryPoint(), which returns the first vertex and by indirection the content of the path. SimpleLoopPath does some munging of the path sequence before delivering the entryPoint, so that the GateSym's are all falsified along the edges. We no longer have to deny that we are leaving the loop, since there is no place else to go. Also, the entrypoint represents the underlying CodeSym, which is the "first instruction" of the loop, NOT the loop as a whole. Finally, the last vertex of a SimpleLoopPath interprets to the trivial state transformation. All of the these modifications are made so that when jpf traverses the Graph with entrypointSet {simpleLoopPath.getEntryPoint()}, it will specify the state transition of the loop body, which is the desired outcome.
NB: A SuperPathSym is not to be confused with the existing SuperLoopSym. A SuperLoopSym is an intermediary created by "blowing up". In the case of ItsAWrap, we have an innermost loop, so there is nothing to blow up, so the graph corresponding SuperLoopSym coincides with that of the ambient MethodSym. The terminology is not great.
Next: create and wire LoopDefinitionRequestMsg and MethodDefintionRequestMsg to create a JPFrewriter and fire it up.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/Resources/IconIndex.java
branches/mango/Mango/Mango/src/mango/graph/data/graphic/CodeData.java
branches/mango/Mango/Mango/src/mango/graph/data/graphic/VertexData.java
branches/mango/Mango/Mango/src/mango/graph/data/ucon/UconData.java
branches/mango/Mango/Mango/src/mango/graph/msg/MultiGraph3DViewCreateRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionLocatorMsg.java
branches/mango/Mango/Mango/src/mango/worker/Mango.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/BackupEdge.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/Edge.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/InstallResult.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/Path.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/LoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/MethodSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/SourceLineSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/VertexSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/AlphaSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/BackupVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/LoopVertex.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/HitemUtil.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/SimpleLoopPath.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperPathSym.java
branches/mango/Mango/mangoUserHome/rkrug/itsAWrap/src/baseline/ItsAWrap.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/graph/data/supervertex/SuperStrataData.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/StrataGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperStrataSym.java
branches/mango/Mango/mangoUserHome/rkrug/itsAWrap/src/baseline/itsAWrap.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-02 04:15:45
|
Revision: 1884
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1884&view=rev
Author: frankrimlinger
Date: 2009-09-02 04:15:34 +0000 (Wed, 02 Sep 2009)
Log Message:
-----------
Introduced JPFrewriter and its Launcher and InstructionFactory in the new package mango.rewriter in the javapathfinder-mango-bridge. Moved classes Edge and Vertex, which extend Graphic, from mango.worker.mangoModel to mango.rewriter.synthetic. The base class Graphic now extends Instruction, so JPFrewriter can now execute Vertex and Edge objects. So far so good, but how is this execution to take place?
Here is a theory of operation, which is somewhat speculative at this point. JPF has the notion of a Step, which is an executed instruction, and a Transition, which is a sequence of Steps from the last branch point. The current trail is stored in the SystemState and so is available to the execute() method of an instruction. The point is that an Instruction that is executing can obtain the "last step" of the trail, which presumably is the instruction that just executed, if any.
Here is the punchline: a Step can store an "annotation", which can be any Object. Its pretty clear that JPF regards this as user register, since the only reference to setAnnotation() is in an MJI method called addComment(), which probably enables the source code annotation concept. As this only exists in JPF extensions, we presumably are free to knock ourselves out. So annotate a Step by storing MangoState
class MangoState{
Hitem totalState;
Hitem partialState;
}
Now we are good-to-go. TotalState is the accumulated state from the module entry point to the current instruction, and partialState is the accumulated state from the last branch point. Its up to the choice generators to carry the total state from one Transition to the next. TotalState will enable specification, and partialState will enable invariant factorization.
This feels right, but here is a question. How can an Instruction that is executing get a hold of its Step, which doesn't exist yet? This must be listener thing.
Well, at the outset have to call ss.recordSteps(true), where ss is the SystemState singleton. Then, assuming nobody has altered the logInstruction field of the ThreadInfo, the step will be recorded just AFTER execution of the instruction. But then, as expected, there is vm.notifyInstructionExecuted, passing this ThreadInfo and the instruction.
So, we install a listener that responds to "instruction executed" by
1) Creating the formal expressions for the new MangoState.
2) posting a rewrite message to a higher priority queue and blocking the JPFrewriter thread. There will have to be some work done in the ThreadSupport project to allow execution of higher priority messages while a message is in the "blocked" state. Currently there is no such state, but it's time to face the music. There is no other way, short of abandoning jpf. Since we are in a listener when the block occurs, JPFrewriter should be in a pretty consistent state.
Now this rewriter message is going to be firing up Module instantiations, which will affect data in ChoiceGenerators, and invariant detection, which will cause tracebacks. The tracebacks are read-only as far as JPFrewriter is concerned, so relatively safe. But the fact is that we will be messing with ChoiceGenerator data while blocked inside a listener, but this seems safe enough. When the JPFrewriter wakes up, it exits the listener and continues the Transition. When the transition is done and a new choice is made, well, it may not be a choice we could have predicted in advance, but that's life.
So, JPFrewriter will be the main driver of automation. It will take frequent naps, but each time it wakes up it will be a little bit smarter. What is nice about dynamically wiring the choice generators is that the game can be made to play itself until all cases are exhausted, at which point the JPFcmd finally finishes and the higher level automation kicks in to clean up, restart, select the next target, and fire up a new JPFrewriter.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/deprecatedPackage/DeprecatedMethods.java
branches/mango/Mango/Mango/src/mango/graph/data/supervertex/SuperEntryData.java
branches/mango/Mango/Mango/src/mango/graph/data/ucon/UconData.java
branches/mango/Mango/Mango/src/mango/gumboModel/factory/EmbeddedJVMFactory.java
branches/mango/Mango/Mango/src/mango/gumboModel/factory/GraphModelFactory.java
branches/mango/Mango/Mango/src/mango/gumboModel/factory/MultiGraphModelFactory.java
branches/mango/Mango/Mango/src/mango/gumboModel/factory/SourceModelFactory.java
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/AssignNotObjectValue.java
branches/mango/Mango/Mango/src/mango/tree/model/Cell.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/AlphaDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/BackupDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/CodeDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/EdgeDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/GraphDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/OmegaDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/backupDelegate/UconDelegate.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/BackupEdge.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/EdgeIterator.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/InstallResult.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/Path.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/PathCollection.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/SimpleLoopPath.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/AcyclicGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/CpnGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/Graph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/SuperCpnGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/GraphicSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/LoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/PackageSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/SuperVertexClassSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/return_terminator/ReturnTerminatorSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/sink_terminator/SinkTerminatorSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperBlowUpSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperEntrySym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperLoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/InvocationUconSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/UconOSTerminatorSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/UconSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/AcyclicVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/BackupVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/CallVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/LoopVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/MethodVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/SuperVertex.java
branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInterface.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
Added Paths:
-----------
branches/mango/Mango/javapathfinder-mango-bridge/gov/nasa/jpf/JPFrewriter.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/InstructionFactory.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/Launcher.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Edge.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Graphic.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/Edge.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graphic/Graphic.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/Vertex.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-02 15:11:55
|
Revision: 1885
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1885&view=rev
Author: frankrimlinger
Date: 2009-09-02 15:11:47 +0000 (Wed, 02 Sep 2009)
Log Message:
-----------
Happily, no fundamental modification of the ThreadSupport project is necessary to support "user" blocking of a Commander thread. The point is that a ReentrantLock has already been established in the SystemBuilder, called "executionLock". The command that holds the lock is the only one that gets to execute. This lock was established to *prevent* higher priority commands from swapping in randomly while a lower priority command was running. So if a lower priority command wants to block, it does the following:
create a new Semaphore sem.
create the higher priority message, passing sem
post the higher priority message
unlock the executionLock
acquire sem
lock the executionLock
All the higher priority message has to do is release sem when it is done. The lower priority message will then unblock and continue execution.
BUT, what happens if the lower priority message is so unlucky that it swaps out just after unlocking. Then the higher priority message kicks in, does its thing, and attempts to release the semaphore before it was ever acquired? Well, the higher priority thread can accommodate this situation like so:
while(true){
if(!sem.hasQueuedThreads()){
Thread.sleep(1);
}
else{
sem.release();
break;
}
}
It's a piece of cake! The InterruptCode interface declares two methods, getSemaphore() and transit(). ScheduleRequestMsg implements this interface, so extensions can now run as interrupt code. All they have to do is accept a Semaphore and pass it to super(), and call transit() instead of transit(Command.E.FINISH) The base class implementation of transit() handles the cleanup at FINISH time.
For any Command that needs to block, there is the incantation:
wait( new XXXmsg(<usual arguments>, new Semaphore()))
The method wait() accepts any Command implementing InterruptCode, and calls its getSemphore() method to implement the blocking logic for this command.
Modified ScheduleRequestMsg and Command to accomodate the InterruptCode interface. Created the new lowest priority for the session threads, JPFREWRITER. With JPFrewriter running the show, its not clear that that the "session" concept has any meaning, but we just let sessions continue to exist until it is clear they are no longer needed.
The whole idea of having a static set of threads tied to pre-defined priorities is feeling a little 20th century, but oh well, good enough for now.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/control/msg/ReplayedMsg.java
branches/mango/Mango/Mango/src/mango/worker/msg/ScheduleAutoCommand.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/EventLoopTrap.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ScheduleRequestMsg.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/TrapCommand.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/WorkerCommand.java
branches/mango/Mango/ThreadSupport/src/threadModel/Command.java
branches/mango/Mango/ThreadSupport/src/threadModel/Priority.java
branches/mango/Mango/ThreadSupport/src/threadModel/SystemBuilder.java
Added Paths:
-----------
branches/mango/Mango/ThreadSupport/src/threadModel/InterruptCode.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-02 19:14:12
|
Revision: 1886
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1886&view=rev
Author: frankrimlinger
Date: 2009-09-02 19:13:57 +0000 (Wed, 02 Sep 2009)
Log Message:
-----------
Wired up the JPFrewriter according to 1884. It remains to implement the functionality of RewriteChoiceGenerator, RewriteListener, and the getEntryPoint() method for classes LoopDefinitionManager and MethodDefinitionManager.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/loop/msg/LoopDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/method/MethodDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/Mango/ThreadSupport/src/threadModel/Command.java
branches/mango/Mango/javapathfinder-mango-bridge/gov/nasa/jpf/JPFrewriter.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/Launcher.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoTargetLauncher.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
Added Paths:
-----------
branches/mango/Mango/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_rewriter_RewriterMJI.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/JPFrewriterCmd.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteListener.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriterMJI.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/InvokeRewriter.java
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8- dload_i_Code_01/Final case. op0 is less than 10.zip
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/Array length of x is greater than or equal to 10.zip
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8- dload_i_Code_01/a.zip
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8- dload_i_Code_01/op0 is less than 10.zip
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/main([I)Z/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-03 03:44:19
|
Revision: 1887
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1887&view=rev
Author: frankrimlinger
Date: 2009-09-03 03:44:12 +0000 (Thu, 03 Sep 2009)
Log Message:
-----------
Most of the wiring for JPFrewriter is now in place. Need to punch in the branching logic for Vertex and Edge instructions. In RewriteListener.instructionExecuted(), you need to acquire the last Step, generate its MangoState, and wait on a command to rewrite the MangoState components. Then the game starts to play itself.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/method/MethodDefinitionManager.java
branches/mango/Mango/javapathfinder-mango-bridge/gov/nasa/jpf/JPFrewriter.java
branches/mango/Mango/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_rewriter_RewriterMJI.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/InstructionFactory.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteListener.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Edge.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java
Added Paths:
-----------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MangoState.java
branches/mango/Mango/mangoUserHome/rkrug/itsAWrap/src/baseline/ItsAWrap.java.tmp
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-03 18:11:09
|
Revision: 1888
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1888&view=rev
Author: frankrimlinger
Date: 2009-09-03 18:11:02 +0000 (Thu, 03 Sep 2009)
Log Message:
-----------
It turns out that the annotation object exists at the transition level, not the step level as indicated in 1884. But thats ok, just store a MangoAnnotation. Inside the MangoAnnotation, there is a HashMap that maps each step to its MangoState.
Wired in branching logic for Vertex and Edge. Decided there was no need for separate listener for branching, so this is in the RewriteListener.
TODO: Vertex.firstExecuted() in particular, the issue splicing of totalState with the previous transition needs to be figured out.
Vertex.instructionExecuted() needs to compose with state of the previous edge. Also, if there is no outgoing edge, then needs to wait on message to complete the specification for this case. NB: NOT to be confused with no "next pc", which just means we are at the end of a transition.
Edge.instructionExecuted() needs to do a lot of stuff. Assumption of branch conditions, module instantiation, and setting up its mango state, which is previous composed with trivial or the instantiated module state. (The whole point of assuming the branch condition is to make it go away). Also buried in here will be the user stuff to help out with translation issues, so there will have to be a "Go" button after all so the user can indicate when ready to continue.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/utilities/Set.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MangoState.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteListener.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Edge.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Graphic.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/InvokeRewriter.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Boolean_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Character_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Class_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Double_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Integer_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Math_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Short_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/System_MangoFormal.java
Added Paths:
-----------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MangoAnnotation.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/RewriterInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-03 22:08:52
|
Revision: 1889
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1889&view=rev
Author: frankrimlinger
Date: 2009-09-03 22:08:44 +0000 (Thu, 03 Sep 2009)
Log Message:
-----------
Various tweaks to better understand exactly how JPFrewriter, RewriteChoiceGenerator, and RewriteListener play together. Simulations show all the paths through a loop body or acyclic module graph are covered exactly once. Ready for the tricky business of state splicing across transitions. Also made sure persistent names were manufactured in order to support "transition replay", which will eventually be an issue.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/engine/sym/InterpretableSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/SimpleLoopPath.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteListener.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Edge.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/RewriterInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-06 03:54:28
|
Revision: 1893
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1893&view=rev
Author: frankrimlinger
Date: 2009-09-06 03:54:21 +0000 (Sun, 06 Sep 2009)
Log Message:
-----------
Completed design for unravelling predicate transformers. Implementation in progress.
Modified Paths:
--------------
branches/mango/Mango/doc/unravelling predicate transfomers.rtf
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MangoAnnotation.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MangoState.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteListener.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Edge.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
Added Paths:
-----------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteChoice.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/sym/
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/sym/HarvestChoiceSym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/RewriteInstruction.java
Removed Paths:
-------------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/RewriterInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-07 04:09:07
|
Revision: 1895
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1895&view=rev
Author: frankrimlinger
Date: 2009-09-07 04:08:57 +0000 (Mon, 07 Sep 2009)
Log Message:
-----------
Refined the design for unravelling predicate transformers, and completed all the high-level wiring for jpf interface. It remains to write HarvestChoiceCmd, InstantiateFreeChoiceCmd, and SpecifyCaseCmd, and associated traps and rules.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/loop/msg/LoopDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/method/MethodDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashRewriter.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/TrapCommand.java
branches/mango/Mango/doc/unravelling predicate transfomers.rtf
branches/mango/Mango/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_rewriter_RewriterMJI.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MangoAnnotation.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteListener.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/sym/HarvestChoiceSym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Edge.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Graphic.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/RewriteInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
Added Paths:
-----------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/FreeAssumption.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/InplaceChoice.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/OutboundChoice.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/msg/
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/msg/HarvestChoiceCmd.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/msg/InstantiateFreeChoiceCmd.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/msg/SpecifyCaseCmd.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/trap/
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/trap/HarvestChoiceTrap.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/PriorityScheduleRequestMsg.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteChoice.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-08 03:54:46
|
Revision: 1896
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1896&view=rev
Author: frankrimlinger
Date: 2009-09-08 03:54:39 +0000 (Tue, 08 Sep 2009)
Log Message:
-----------
Debugged some wiring, and now the JPFREWRITER thread will go to sleep and let the SESSION thread kick in with HarvestChoiceCommand, for the first Vertex instruction. Now need some rules so the harvest can do its thing.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/module/definition/loop/msg/LoopDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MangoAnnotation.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteListener.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/msg/HarvestChoiceCmd.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Graphic.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/trap/HarvestChoiceTrap.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-10 21:22:35
|
Revision: 1902
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1902&view=rev
Author: frankrimlinger
Date: 2009-09-10 21:22:13 +0000 (Thu, 10 Sep 2009)
Log Message:
-----------
It turns out there was a EZ bug in MangoInvokeInstruction.getResolvedMethod(). But the TABLESWITCH formal peer was OK. Mango was a little worried about whether or not a single instruction could generate multiple branch conditions for the same destination. This is in fact exactly what TABLESWITCH does in certain cases. So problem was "fixed" by deleting the warning.
However, the LoopGraph (not well named because actually acyclic) generated from a blow up may contain innermost loops, and the problem is that these loops for some reason are not appearing in the loop hierarchy.
OK, what happens here is a little complex. During phase2, the innermost loops are collapsed, then each remaining non-trivial cluster is blown up. Then the flow from each alpha to omega is excised, and the process repeats on each excision. Needless, to say, a fair amount of graph cloning takes place, and the trouble is that the cloned vertices were not inheriting the innermost loop dependency vectors set up by the initial innermost loop collapse.
Fixing this problem is complicated by the fact that the graph cloner uses reflection to create the new vertices, which are not required to be of the same class as those of the input graph. To safely pass the dependency vector when it is appropriate to do so, chose to put a little hack in the bottleneck routine Graph.associatedOutputVertex(). TRICKY: some loops now appear more than once in the dependency graph structure, for example in loopTests.fibonocci. Rather than fight city hall, just be sure to eliminate duplicates from the final dependency vector.
Incidentally, fibonocci is a fine example of mutual co-recursion, so keep testing it as automation proceeds.
YIKES. Inspection of A!_B!_A!_Component_loopTests.nested_blowup.main(I)V reveals that the acyclic graph of a blowup need not be connected. This means in some cases you do cross over connectors when seeking omega. But its ok, because you only cross over to connector entrypoints that are entrypoints of the SAME graph, and this is easily checked.
CORRECTION: the branching logic in 1899 for blowups should read
Do not go down any edge which only leads to a component sink other than omega, unless you are going to connect to an entrypoint of the same component. (All such entrypoints will ultimately lead to omega).
NEXT: Clean up the dependency tree of all entrypoints, starting at the root "Java Code Entrypoints" in order to develop the dependency tree of modules required for target selection.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/graph/msg/Graph2DViewCreateRequestMsg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/SimpleLoopPath.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/Graph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/LoopVertex.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-11 04:30:39
|
Revision: 1903
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1903&view=rev
Author: frankrimlinger
Date: 2009-09-11 04:30:32 +0000 (Fri, 11 Sep 2009)
Log Message:
-----------
Generalized SuperCpnGraphCreateRequestMsg to FowardFlowRequestMsg, which can generate the forward flow from any SuperVertex. This is very handy for visualization of subgraphs. To find the targetable methods, walk the forward flow of the entrypoints graph. The structure of this graph is like so:
PackageSym ...
SuperVertexClassSym
MethodSym
Now for each individual MethodSym, walk its foward flow, structure like so
SuperCpnSym ....
SuperLoopSym
SuperBlowUpSym LoopSym...LoopSym
....
Walk until you get to SuperCpnSym with no outgoing edge to a SuperCpnSym. This is a *terminal* SuperCpnSym. The job of the target selection algorithm is to pick the SuperCpnSym *closest* to some prescribed class or method. Exactly what this means is TBD, but assuming you have picked the target SuperCpnSym, you now do the component survey for jpf like so:
Let F denote the forward flow of the target SuperCpnSym. The correspondence with 1899 is like so
ComponentChoiceGenerator performs breadth-first backward flow on F, from leaves to the target SuperCpnSym, skipping the intermediary SuperBlowUpSym.
PathChoiceGenerator applied to LoopSym graphs
BlowUpChoiceGeneragor applied to SuperLoopSym graphs
MethodChoiceGenerator applied to SuperCpnSym graph.
The terminology leaves much to be desired, but for now not going to change it. Now that the facts on the ground are understood, its time to write the target selection algorithm and the component survey/ComponentChoiceGenerator. Then test this mechanism to make sure you can traverse tricky examples correctly. Then punch in the other choice generators. Finally, you can start working on the internal structure of vertex execution, this is 1892 and companion document.
Wrote the class loopTests.MutualCorecursion to clarify what happens in the case of mutual corecursion. In this case, there is still a single SuperCpnSym, but the most dependent SuperLoopSym has multiple entry points, one for each method of the system. The fact that the SuperCpnSym professes allegiance to a particular one of the two methods is just an artifact. Just don't make unnecessary assumptions about graphs and everything will be fine.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/graph/agent/GraphViewAgent.java
branches/mango/Mango/Mango/src/mango/gumboModel/action/MangoActionManager.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/PackageSym.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/graph/msg/ForwardFlowRequestMsg.java
branches/mango/Mango/mangoUserHome/frank/loopTests/src/loopTests/MutualCorecursion.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/graph/msg/SuperCpnGraphCreateRequestMsg.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-11 18:44:12
|
Revision: 1904
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1904&view=rev
Author: frankrimlinger
Date: 2009-09-11 18:44:06 +0000 (Fri, 11 Sep 2009)
Log Message:
-----------
Debated whether or not to improve graph class names. Decided against doing so because they make good sense in the context of the original loop algorithm, which is still completely intact and must be maintained. The mapping of 1803 will suffice.
Changed target class preference to target preference. The user just enters any string. Mango first tries to match a class, and if that doesn't work, a method, and if that doesn't work, the chosen target is the first available terminal SuperCpnSym, and if none, then done.
TODO Encapsulate this logic in the new TargetSelectionMsg. The "closest" SuperCpnSym is determined by just doing a depth first search and linearly ordering all vertices of the entire entrypoint/SuperCpnSym complex, locating the target within this linear order, and then picking the nearest terminal SuperCpnSym within this linear order.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/msg/NewWorkerMsg.java
branches/mango/Mango/Mango/src/mango/worker/msg/OpenDefinitionMsg.java
branches/mango/Mango/src/mango/intro/ConfigurationDetails.java
branches/mango/Mango/src/mango/intro/LoginDialog.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/worker/msg/SelectTargetMsg.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-14 05:08:09
|
Revision: 1905
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1905&view=rev
Author: frankrimlinger
Date: 2009-09-14 05:08:00 +0000 (Mon, 14 Sep 2009)
Log Message:
-----------
A SuperCpnSym represents a Graph whose entrypoints are MethodEntrySym's. Each such MethodEntrySym must, at least for the time being, fire up a DefinitionManager. A MethodEntrySym is a GraphicSym, and so has an outgoingConnections field, which is a set of GraphicConnection's. There are many kinds of GraphicConnection, but the relevant one for walking the forward flow are the superCpnConnection and subCpnConnection
>From the point of view of walking forward flow, the only wrinkle introduced by a system with mutual co-recursion is that not all entrypoints of a SuperCpnSym are associated with the same method. In fact, there will be one such entrypoint for each method of the system. This is not a problem because each entrypoint gets its own DefinitionManager anyway.
Introduced GraphIterator class, and migrated graph walking functionality so nested walks can take place. This ancient bug is finally put to rest. Compared modelling of "frank" configuration in Mango versus MangoBaseline, precisely 28 seconds in both cases, so that there is zero performance hit using the GraphIterator class.
Generated the flat list of terminal SuperCpnSym's. However, what we really want is the corresponding flat list of MethodEntrySym's. Not necessarily one-to-one because of mutual corecursion. Also on the fly create maps
MethodInfo--> Vector<Integer>
ClassInfo --> Vector<Integer>
Which map each associated method and class to the corresponding indices of the flat vector. Now give a target that maps to a MethodInfo or ClassInfo, you can map to an index and hence a MethodEntrySym. But not done yet. We really need to find the least dependent module associated with MethodEntrySym. In order to do this, need to back off to the SuperCpnSym, and flatten its forward flow, picking up all SuperLoopSym's which are destinations of a SuperBlowUpSym's, and all LoopSym's. You don't need to bother with initial SuperLoopSym's as these do not contain an alpha-omega pair.
So, to summarize, once you deduce the "closest" MethodEntrySym, you flatten its *relevant* forward flow. This give you the order of component execution for the ComponentChoiceGenerator, modulo duplicate entries.
TODO: finish the target selection algorithm by acquiring the nearest MethodEntrySym and preparing the required ordering for the ComponentChoiceGenerator.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/AcyclicGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/Graph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/GraphicSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/SuperVertexClassSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperBlowUpSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperEntrySym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperLoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/UconSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/AcyclicVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/SuperCpnVertex.java
branches/mango/Mango/Mango/src/mango/worker/msg/OpenDefinitionMsg.java
branches/mango/Mango/Mango/src/mango/worker/msg/SelectTargetMsg.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/GraphIterator.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-15 20:23:52
|
Revision: 1907
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1907&view=rev
Author: frankrimlinger
Date: 2009-09-15 20:23:44 +0000 (Tue, 15 Sep 2009)
Log Message:
-----------
Moved MethodEntrySym, SuperLoopSym, and LoopSym into the rewriter.synthetic package. Extended these class from Instruction and implementing the new ComponentInstruction interface. Added superCpnSym field to MethodEntrySym so it can retrieve the component graph with the corresponding entrypoint.
With this in place, ComponentChoiceGenerator now simply executes each ComponentInstruction, working backwards from the end of the component vector generated by the BackupAlg instance.
Each component instruction executes by installing the corresponding choice generator.
MethodEntrySym: MethodChoiceGenerator
walks CpnGraph, starting at entrypoint corresponding to MethodEntrySym. Follows connectors, passing through a given omega no more than once per case. To "pass through" omega means that you automatically jump to the corresponding alpha and keep going.
SuperLoopSym: BlowupChoiceGenerator
walks LoopGraph starting at alpha. Follows connectors which remain in this graph. case must end at omega
LoopSym: LoopChoiceGenerator
walks linear path, starting at supplied entrypoint.
The details to set all this up are quite idiosyncratic, which is why the Syms were all broken out as separate instructions.
Completed coding of ComponentChoiceGenerator. Tested against baseline package code. The components are executed in the correct order.
Completed coding of the ComponentInstruction execute() methods, so that the proper RewriteChoiceGenerator created with an Outbound choice corresponding entrypoint and loaded as the new choice generator. Previous testing of RewriteChoiceGenerator loaded the entrypoint from the current DefinitionManger. But now we just proceed with no DefinitionManger. Whatever gui monitoring is required will start more or less from scratch as requirements change dramatically.
There are now two kinds of traversal logic on a collision course. The first is the logic of "unravelling predicate transformers", 1892-1896, and the logic of component choice generators, discussed in 1898 and summarized above. This can be thought of as local and global traversal logic, respectively. The global logic may be viewed as constraining the local choices to the admissible outbound edges. This constraint is introduced programmatically by creating RewriteChoiceGenerator.getDestinations(). For the test jig, this method just returned *all* the outgoing edges. But now the problem is bounced to the current choice generator, one of the above. The choice generator then must probe the graph in question to determine which edges and/or vertex connector destinations are appropriate, and return them.
Incidentally, this functionality now obviates the need for the ucon and gstack formalism. For now this formalism will be left intact in the loop algorithm, because it was very hard to get right in the first place and it may once again be needed someday. It will be the job of the choice generator deliver the proper "glue" across connectors.
TODO: before tuning the state logic, get the global traversal logic working. Specifically, this means implementing getDestinations() within the RewriteChoiceGenerator extensions.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/graph/data/graphic/LoopData.java
branches/mango/Mango/Mango/src/mango/graph/data/supervertex/SuperLoopData.java
branches/mango/Mango/Mango/src/mango/graph/data/ucon/MethodEntryData.java
branches/mango/Mango/Mango/src/mango/graph/msg/Graph2DViewCreateRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/loop/msg/LoopDefinitionLocatorMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/loop/msg/LoopDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/method/MethodDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/method/msg/CreateMethodStubMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionLocatorMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/method/msg/MethodDefinitionRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/instance/loop/agent/LoopInstanceAgent.java
branches/mango/Mango/Mango/src/mango/module/instance/loop/model/LoopInstanceManager.java
branches/mango/Mango/Mango/src/mango/module/instance/loop/msg/CloseLoopInstanceMsg.java
branches/mango/Mango/Mango/src/mango/module/instance/loop/sym/LoopInstanceSym.java
branches/mango/Mango/Mango/src/mango/ruleAction/module/instance/BuildLoopInstanceManager.java
branches/mango/Mango/Mango/src/mango/ruleAction/module/instance/InstantiateLoopERROR.java
branches/mango/Mango/Mango/src/mango/ruleAction/module/instance/IsLoopDefinitionClosed.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/LoopSymReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/MethodEntrySymReq.java
branches/mango/Mango/Mango/src/mango/worker/Mango.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hitem.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/InterpretableSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/edge/Path.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/graph/LoopGraph.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperBlowUpSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperVertexSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/AlphaSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/BackupVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/CpnVertex.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/vertex/LoopVertex.java
branches/mango/Mango/Mango/src/mango/worker/msg/SelectTargetMsg.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/HitemUtil.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/BlowupChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/ComponentChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/LoopChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/MethodChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteChoiceGenerator.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/RewriteListener.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Graphic.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/InvokeRewriter.java
Added Paths:
-----------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/ComponentInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/LoopSym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/MethodEntrySym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/SuperLoopSym.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/LoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/superVertex/SuperLoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-09-16 20:51:04
|
Revision: 1909
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1909&view=rev
Author: frankrimlinger
Date: 2009-09-16 20:50:57 +0000 (Wed, 16 Sep 2009)
Log Message:
-----------
To write the choice logic for methods and blowups, first need the notion of the *strong attractor* and the *weak attractor* of a vertex. The strong attractor S(v) of v is the maximal subgraph of G with unique sink v. Clearly the strong attractor is unique, and for vertices v and w, either S(v) and S(w) are disjoint, or one of these graphs is included in the other. The weak attractor W(v) of v is the union of all paths which terminate at v. Clearly W(v) contains S(v). The attraction is weak because when you are in W(v)-S(v) you still have the chance to escape v altogether.
Let G be the graph of all components together with superCpnConnection and subCpnConnection connections. We are interested in S(omega) and W(omega) for omega vertices of G.
Computation for S(v):
0) v is in S(v)
1) if w is a vertex of S(v), then every inbound edge to w is in S(v).
2) a vertex w is in S(v) if and only if every outbound edge of w is in S(v).
Computation for W(v)
0) S(V) is in W(v)
1) if w is a vertex of W(v), then every inbound edge to w is in W(v).
2) a vertex w is in W(v) if and only if there exists an outbound edge of w in S(V).
MethodChoiceGenerator trail logic: Let Omega be the set of all omega vertices. The the trail state set is {open,attracted,repelled} x Omega. The trail starts out in the open state for each omega. If it enters S(omega) for some omega, the state transitions to attracted for that omega. The trail must now hit omega, when it does, it jumps to the corresponding alpha, and changes its state to repelled with respect to omega. The trail must now remain in the repelled state with respect to omega, which means either stopping at alpha (i.e. stuck in infinite loop) or traveling along a path in G-V(omega) to a sink of G. Notice that by infinite loop we mean a *structurally* infinite loop, i.e., no exit branch, like while(true){}. This doesn't happen very often, but a driver could have this structure.
Strictly speaking the attracted state is unnecessary, but good feedback.
BlowupChoiceGenerator trail logic: Start at alpha and remain in W(omega). End at omega.
Observe that there is ample opportunity for exponential growth in the number of trails. But for now, we punt on case filtering and case consolidation. The point here is that the computation of S(v) and W(v) is linear in the size of G, so there is no problem computing the branching logic as such.
To implement, after you get the choice vector, you can enumerate the relevant omega vertices, then use computation logic above to radiate away from each omega, updating
HashMap<Object,HashSet<Vertex>> strongMap
HashMap<Object, HashSet <Vertex>> weakMap
Given any edge, relevant GraphicConnection, or vertex x, strongMap.get(x) contains omega for x in S(omega). Mutatis mutandis for weak map.
The following gets added to the MangoAnnotation to manage the trail state:
enum TrailState {ATTRACTED,REPELLED}
HashMap<Vertex,TrailState> trailState
The trail state is assumed to be open for each omega, unless otherwise indicated. Now just update trailState everytime there is a state change as described above.
Introduce TrailManager object to compute strongMap and weakMap. The ComponentChoiceGenerator constructor instantiates and initializes the TrailManager.
Modified Paths:
--------------
branches/mango/Mango/javapathfinder-mango-bridge/mango/rewriter/synthetic/Vertex.java
branches/mango/Mango/src/mango/intro/LoginDialog.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
Thanks for helping keep SourceForge clean.
X