SmartThings specific support to reduce state space

[jpf-core.git] / src / main / gov / nasa / jpf / vm / serialize / CFSerializer.java

diff --git a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
index 895b94a3f1d2d59c9c8c6cbc007f98d8726ca88d..bdd63554cba8f675ada4bf645298072f5622900d 100644 (file)
--- a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
+++ b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
@@ -77,7 +77,6 @@ public class CFSerializer extends FilteringSerializer {
   public void processReference(int objref) {
     if (objref == MJIEnv.NULL) {
       buf.add(MJIEnv.NULL);
-
     } else {
       ElementInfo ei = heap.get(objref);
       int sid = ei.getSid();
@@ -101,34 +100,42 @@ public class CFSerializer extends FilteringSerializer {
       buf.add(sid);
     }
   }
-  
+
+
+  boolean istop;
   @Override
   protected void serializeStackFrames() {
     ThreadList tl = ks.getThreadList();
-
+    istop = true;
     for (Iterator<ThreadInfo> it = tl.canonicalLiveIterator(); it.hasNext(); ) {
       serializeStackFrames(it.next());
+      istop = false;
     }
   }
   
   @Override
   protected void serializeFrame(StackFrame frame){
-    buf.add(frame.getMethodInfo().getGlobalId());
-
+    FramePolicy fp = getFramePolicy(frame.getMethodInfo());
     Instruction pc = frame.getPC();
-    buf.add( pc != null ? pc.getInstructionIndex() : -1);
-
     int len = frame.getTopPos()+1;
-    buf.add(len);
-
-    // unfortunately we can't do this as a block operation because that
-    // would use concrete reference values as hash data, i.e. break heap symmetry
-    int[] slots = frame.getSlots();
-    for (int i = 0; i < len; i++) {
-      if (frame.isReferenceSlot(i)) {
-        processReference(slots[i]);
-      } else {
-        buf.add(slots[i]);
+    
+    if (fp == null || fp.includePC || istop) {
+      buf.add(frame.getMethodInfo().getGlobalId());
+      buf.add( pc != null ? pc.getInstructionIndex() : -1);
+    }
+
+    if (fp == null || fp.includeLocals || istop) {
+      buf.add(len);
+      
+      // unfortunately we can't do this as a block operation because that
+      // would use concrete reference values as hash data, i.e. break heap symmetry
+      int[] slots = frame.getSlots();
+      for (int i = 0; i < len; i++) {
+        if (frame.isReferenceSlot(i)) {
+          processReference(slots[i]);
+        } else {
+          buf.add(slots[i]);
+        }
       }
     }
   }