Menu
▾
▴
[Javapathfinder-svn] SF.net SVN: javapathfinder:[1756] branches/mango/Mango
|
From: <fra...@us...> - 2009-07-13 21:52:04
|
Revision: 1756
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1756&view=rev
Author: frankrimlinger
Date: 2009-07-13 21:51:58 +0000 (Mon, 13 Jul 2009)
Log Message:
-----------
Only the "valueOf" methods of String_MangoFormal still lack native abstraction. But before doing this, a much more significant issue needs attention. The overhaul of the type system, long overdue, is finally underway. Historically, several competing systems grew up, all represented in the code base in various stages of decay. The goal is a single typing system with flat primitive name space. Several comments are in order.
The type of an object was stored in the rulebase like so
(pushH (refH ref ^Type) stripped-object-syntax heap)
so that the type of a string becomes java.lang.String, as opposed to
Ljava.langString; or java/lang/String or even Ljava/lang/String;
This choice was made long ago, when the what-you-see-is-what-you-should-store idea was very much in vogue.
Give this, what is the type of an integer field x? The choice was "I", as opposed to "int". This was the wrong choice, because now there is no way to distinguish the class named "I" from an integer. So now is the time to fix this problem. For primitive types, we switch to java language level syntax: byte, short, int, etc for B,S,I etc. Fortunately, jpf FieldInfo.getType() is returning java language level anyway, so this is good.
As for the type of an array of integers, it is now
int[]
as opposed to "[I" or "L[I;" because this is what is specified at the java language level. This means that the syntactic test for array type, given a type name, is now endsWith(typeName,"]"), as opposed to startsWith(typeName,"["). This change must be propagated through the rulebase and the code base.
NB: for arrays, FieldInfo.getType() does the right thing, because this traces all the way back to gov.nasa.jpf.jvm.Types.getTypeName(String type), which contains the desired conversion.
if (c == '[') {
return getTypeName(type.substring(1)) + "[]";
}
if (type.charAt(len - 1) == ';') {
return type.substring(1, type.indexOf(';')).replace('/', '.');
}
This is clearly doing what we want. In other words, "type" and "java type" have now converged to the same thing, so the horrible JavaType class has been retired. This functionality is now in the mango.FormalTypes in the javapathfinder-mango-bridge, which extends gov.nasa.jpf.jvm.Types. The FormalTypes class completely rationalizes the computation of type inequivalence by reference to so-called "instance equivalence classes" of types.
Needless to say, the "formal types" like heap, stack, string, and so on, now have names that collide with the java class names in the brave new flattened name space. All of these have been converted to from X to <X>, which is the jvm strategy for avoiding namespace collision.
Consistent with the strategy of flattening the type space, the LogicaKey extension of RuleKey has been abandoned. A RuleKey now represents a type if and only if its typeFlag is set. All of the defX rulekeys in the rulebase have been replaced by the Y or <Y> rulekey counterpart, where the binding from X to Y was determined by the now obsolete buildLogicalKey method.
NB: This discussion only applies to the type as stored in formal heap. Method signatures are *always* stored and displayed in internal formal. A rose by any other name would small as sweet.
It will probably take some time for typing to settle down, but at least now the path is clear and the foundations are firm.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/Resources/IconIndex.java
branches/mango/Mango/Mango/src/mango/core/sym/RuleKey.java
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/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/ruleAction/conditionalTechniques/conditional/Free.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefArithmeticValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefCoefficientValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefConjunctionValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefDouble.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefEquationValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefFloat.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefGstack.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefInequationValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefInt.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefIntegralValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefLong.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefStringValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/InheritTypeFromThirdArg.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeException.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentRef.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/function/FunctionSpaceTypeName.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/linearArithmetic/CoefficientValue.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/ArithmeticValue.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/DoubleH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/FloatH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hitem.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/IntegerH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Kons.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/LongH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Number.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/csym/Csym.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashInitialize.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashLogicAndArithmetic.java
branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java
branches/mango/Mango/Mango/src/mango/worker/engine/rule/RuleAction.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/Sym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/GateSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/EdgeSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/LoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/PathSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/UconSym.java
branches/mango/Mango/Mango/src/mango/worker/utilities/Util.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/ConjunctionSym.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/coreTechniques/sym/FreeVariableSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/InequationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapItemModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/LocalVarModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/executable/LocalVarSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/agent/StabilizeParameterAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/FunctionSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleHypothesisSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleInvocationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/HitemUtil.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ShowTypeRequestMsg.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/sym/JclassSym.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/rules/substring param.zip
branches/mango/Mango/mangoUserHome/system/System/mango/cheat_sheet.txt
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefObject.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefPredicate.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefPredicateTransformer.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefState.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefUcon.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/TypeAssignmentRule.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/csym/TypeAssignmentCsym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java
branches/mango/Mango/mangoUserHome/frank/rules/hypothese for bounds.zip
branches/mango/Mango/mangoUserHome/frank/rules/substring hypo.zip
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/core/sym/LogicalKey.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefAbstractSym.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefHP.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefP.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefPT.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefPushHvalue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefS.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefU.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/LogicalKeyRule.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/csym/LogicalKeyCsym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/JavaType.java
branches/mango/Mango/mangoUserHome/frank/rules/backupString.zip
branches/mango/Mango/mangoUserHome/frank/rules/concatParam.zip
branches/mango/Mango/mangoUserHome/frank/rules/parameters.zip
branches/mango/Mango/mangoUserHome/frank/rules/tier.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
