Menu
▾
▴
[Javapathfinder-svn] SF.net SVN: javapathfinder:[1793] branches/mango/Mango
|
From: <fra...@us...> - 2009-07-30 23:54:35
|
Revision: 1793
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1793&view=rev
Author: frankrimlinger
Date: 2009-07-30 23:54:19 +0000 (Thu, 30 Jul 2009)
Log Message:
-----------
Completed and tested code for minimum type of an object. Harvest parameters now uses minimum type. Tweaked the minimum type data to optimize parametrization choices. Very nice. Teased apart the types <className> and <classNameSymbol>. The point here is that both of these are recognized as <className> for the purpose of garbage collection, but a <classNameSymbol> implies <defeatParametrization> so we don't paint the rose. Updated the rulebase accordingly.
All Markers were initialized with type <notObject>. Unfortunately, ^null *is* an <object>, because we have blurred the distinction between and object and its reference. The null object has no business being a Marker in the first place, since its semantics are so very different from every other marker. So, like EmptyString, it has been split off into its own singleton class NullObject extending Sym directly. Altered the MFL encoder/decoder to retain the syntax ^null but back it with NullObject instead of Marker.
An attempt to create a Marker with name "null" or a NullObject with any name other than "null" will throw IllegalStateException.
Changed name of the RuleKey "refH" to "loc", consistenty with the type <location> introduced for ref expressions. Every object,subaddress pair has a location in the heap, and every object IS its reference, which is why null can be an object. This is not compatible with java terminology, but so be it. The null object never occurs in a location pair, which is why the heap counter state variable never can take the value null. We assume infinite storage, finite resources is SEP.
BUG: local variable parametrization is broken.
TODO: In Worker.staticReset(), use reflection to examine ALL the mango code and call ALL the staticReset methods (except Worker.staticReset). Its time to do this. This is EZ code.
TODO: You MUST add code NOW to compute the transitive closure of the submitted linear orders. It is just impossibly difficult to do this by hand. Also, you can detect circularity this way and this is a valuable debugging feature.
TODO: Eliminate the HeapPointer class, folding all its functionality into the typing system. This class originally arose to compensate for the inadequacy of earlier versions of typing, but now it is just a swamp area that will hold back evolution of garbage collection. The plan is just to create all the required types for temporal logic and object taxonomy, and then build up the rules for heap pointer comparison on an as needed basis.
Modified Paths:
--------------
branches/mango/Mango/ACL2/itsAWrap-construct.lisp
branches/mango/Mango/Mango/src/mango/core/CoreSym.java
branches/mango/Mango/Mango/src/mango/core/CoreVariable.java
branches/mango/Mango/Mango/src/mango/core/mfl/CoreMFLBuilder.java
branches/mango/Mango/Mango/src/mango/core/mfl/CoreMFLCreator.java
branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/sym/ParamSym.java
branches/mango/Mango/Mango/src/mango/module/model/RuleModel.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/conditional/WithDiveCommutes.java
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/classModel/Instanceof.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsAssignmentCompatible.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/Equals.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentRef.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/string/ToCharArray.java
branches/mango/Mango/Mango/src/mango/ruleAction/form/binder/BindBoot.java
branches/mango/Mango/Mango/src/mango/ruleAction/form/binder/ValueH.java
branches/mango/Mango/Mango/src/mango/ruleAction/function/theory/ModelHeapVacuum.java
branches/mango/Mango/Mango/src/mango/ruleAction/function/theory/ModelHeapVacuum012.java
branches/mango/Mango/Mango/src/mango/ruleAction/function/theory/ModelHeapVacuum02.java
branches/mango/Mango/Mango/src/mango/ruleAction/function/theory/ModelHeapVacuumA.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/automatic/MethodCallAssumption.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateLocation.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateValueH.java
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/AssignNotObjectValue.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashLogicAndArithmetic.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashMangoModel.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashTyping.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/ClassNameSym.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/InvocationNameSym.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/Marker.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/agent/CheckCast_getValueAgent.java
branches/mango/Mango/Mango/src/mango/worker/utilities/Util.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/agent/SimplifyAndAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapPointer.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/EquationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/FoundationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapObjectModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/executable/FrameSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/model/FactorizationModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/model/InvariantModel.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ACONST_NULL.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNONNULL.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNULL.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC_W.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.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/system/System/java/lang/Worksheet for String._MangoFormal<init>(C)V.txt
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/bin/mango/lang/Mango_String.charAt worksheet.rtf
branches/mango/Mango/mangoUserHome/system/bin/mango/lang/Mango_String.length worksheet.rtf
branches/mango/Mango/mangoUserHome/system/bin/mango/lang/Mango_String.setValueFromStringBuffer worksheet.rtf
branches/mango/Mango/mangoUserHome/system/bin/mango/lang/Mango_StringBuffer.append worksheet.rtf
branches/mango/Mango/mangoUserHome/system/bin/mango/util/Mango_ArrayList.add worksheet.rtf
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/ruleAction/typeAssignment/Assign_formal_className.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/ClassNameReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/ClassNameSymbolReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/EnabledParameterReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/InvocationNameSymbolReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/rewriter/DefeatParametrizationReq.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/NullObject.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/ClassNameSymReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/InvocationNameSymReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/ParameterReq.java
branches/mango/Mango/bytecode cheat.txt
branches/mango/Mango/intermediate transformers
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
