[Javapathfinder-svn] SF.net SVN: javapathfinder:[1823] branches/mango/Mango

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Revision: 1823
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1823&view=rev
Author:   frankrimlinger
Date:     2009-08-12 22:19:46 +0000 (Wed, 12 Aug 2009)

Log Message:
-----------

In progress: brining sanity to state translation.  Translation begins with a match of the targeted state, in particular, the heap, stack, and staticArea components are translated.   Some terminology: if the stack has the form (push frame (pop (pop stack))), then frame is referred to as the "caller frame".  If it has the form (push frame (pop stack)), then "called frame".  These two cases correspond to method and loop specification, respectively.  The "ambient method" is the method of the caller frame or the method containing the loop.  A "parameter of the ambient method" refers the source-code level notion of parameter.  (It is not meaningful to translate local variables which are not parameters when forming a specification, because the meaning of the variable has already be abstracted away.)

We start by determining the maps localVar and localType.

1.  for each heap item pair of the form ((loc ref ^className), value), add ref->value to localType.

2.  add x->getType(x) to localType for each parameter x of the ambient method, such that x has formal type <object>.  Recall that getType() is the "java type" of x, determined by the ambient method info.

3. for each defined offset in the local variable array of the called frame, say local variable x with value obj, if x is a parameter of the ambient method, if x has formal type <object>, then add obj->x to localRef.

4. If the caller frame has a "return value", that is, a defined value obj for op0 (top operand on opStack) and obj has formal type <object>, then add obj -> method-return-type to localType, again as determined by the ambient method info.

5. To translate a HeapItemModel (ref,sa,value), first apply the localVar map, and then set up the translation for each mapped item, say x=(tr ref), y=(tr sa), z= (tr value).  

a) if (refType(ref) is defined and is an array type, emit x[y]=z.
b) otherwise, if minimal type of sa is java_int, emit x[y]=z.
c) otherwise, if (refType(ref)) is defined and is not an array type, emit x.y=z
d) otherwise, emit x?y =z

Case b is based on the fact (?) that only an array could have a subaddress that was a concrete number.  Case d hopefully will not happen but if it does, then hopefully the fix can be accomplished with the new improved typing system.

6.  To translate a LocalItemModel or OpItemModel associated with the called frame, just apply localVar to the value in quesion, emitting  local-var-name=(tr value) or op<i>=tr(value) as the case may be.  If there is more than one frame, we are in a mutually recursive loop body, fun fun.  This really hasn't been examined much, but for now, preface each frame with "Top Frame" or "Recursive Frame" as the case may be before emitting item translations.

7. To translate the return value of the caller frame, use existing logic for thrown exceptions, otherwise,  let type=refType(value), emit Returns type: (tr value).  Observe in this case there is no point applying localRef because it is empty.  This is as it should be, as parameter assignments in the called method DO NOT feed back to the caller.  The unhappy "call by reference" idiom of c++ does not exist in java.

8. To translate a StatItemModel (sa,value), apply localVar to value, and emit sa=(tr value).  This makes sense since sa is always a concrete symbol representing a fully qualified field name.  (Well, there is some hack involving setting sa to a number, but we will take that as it comes.  Marc may have done this to represent static arrays?)

So, the complete translation is just the list of item translations, with the return value last, if it exists.  If we are in the called frame case, and there is no return value, then append "No return value." to the list.  That's all there is to it.  Notice all the jvm model artifacts like heap and stack have vanished, as they should.  Well, in the case of mutual recursion, there are still frames, not exactly sure how to proceed yet here.  Anyways, what has appeared are all the translations for utility functions and more importantly, user introduced functions.  These function translations hopefully impart meaning to the specification.  If there is any point to this project, it is to allow the user to inject this meaning as painlessly as possible.

Modified Paths:
--------------
    branches/mango/Mango/Mango/src/mango/control/msg/OpenEncapsulationTemplateRequestMsg.java
    branches/mango/Mango/Mango/src/mango/control/msg/OpenInterpretationRequestMsg.java
    branches/mango/Mango/Mango/src/mango/control/msg/OpenMFLEditorRequestMsg.java
    branches/mango/Mango/Mango/src/mango/debugger/msg/ClearBreakPointMsg.java
    branches/mango/Mango/Mango/src/mango/debugger/msg/SetBreakPointMsg.java
    branches/mango/Mango/Mango/src/mango/graph/msg/Graph2DViewCreateRequestMsg.java
    branches/mango/Mango/Mango/src/mango/graph/msg/Graph3DViewCreateRequestMsg.java
    branches/mango/Mango/Mango/src/mango/graph/msg/MultiGraph3DViewCreateRequestMsg.java
    branches/mango/Mango/Mango/src/mango/gumboModel/interaction/PopUpMenuEnabler.java
    branches/mango/Mango/Mango/src/mango/module/definition/loop/msg/LoopDefinitionLocatorMsg.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/msg/AddConjectureTranslateMsg.java
    branches/mango/Mango/Mango/src/mango/module/definition/msg/AddEquivalenceConjectureLocatorMsg.java
    branches/mango/Mango/Mango/src/mango/module/definition/msg/AddEquivalenceLocatorMsg.java
    branches/mango/Mango/Mango/src/mango/module/definition/msg/AddHypothesisTranslateMsg.java
    branches/mango/Mango/Mango/src/mango/module/definition/msg/EliminateHypothesisLocatorMsg.java
    branches/mango/Mango/Mango/src/mango/module/msg/ApplyLinearLocatorMsg.java
    branches/mango/Mango/Mango/src/mango/module/msg/ContainsTestMsg.java
    branches/mango/Mango/Mango/src/mango/module/msg/GarbageCollectLocatorMsg.java
    branches/mango/Mango/Mango/src/mango/module/msg/GeneralizeLocatorMsg.java
    branches/mango/Mango/Mango/src/mango/module/msg/MapToScopeLocatorMsg.java
    branches/mango/Mango/Mango/src/mango/module/msg/MatchMakerLocatorMsg.java
    branches/mango/Mango/Mango/src/mango/module/msg/ShowModuleMsg.java
    branches/mango/Mango/Mango/src/mango/module/msg/TranslateMsg.java
    branches/mango/Mango/Mango/src/mango/source/agent/msg/SourceViewCreateRequestMsg.java
    branches/mango/Mango/Mango/src/mango/tree/msg/TreeNodeOpenRequestMsg.java
    branches/mango/Mango/Mango/src/mango/tree/msg/TreeRuleViewCreateRequestMsg.java
    branches/mango/Mango/Mango/src/mango/tree/msg/TreeViewCreateRequestMsg.java
    branches/mango/Mango/Mango/src/mango/tree/msg/UndoFormattingOpenRequestMsg.java
    branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/msg/RewriteLocatorMsg.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/trap/RewriteTrap.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/model/EventLoopTrap.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/PopUpMsg.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/PostCoreRequestMsg.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/RedoLocatorMsg.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ReplaceRewriteLocatorMsg.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ShowTypeRequestMsg.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/UndoLocatorMsg.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/WorkerCommand.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/model/TranslateModuleManager.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/trap/ScriptedTranslateTrap.java
    branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.