From: bdemsky <bdemsky@uci.edu>
Date: Sat, 3 Aug 2019 07:05:28 +0000 (-0700)
Subject: edits
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=b0001bdd35423a649b78ecfff0d82b8d476a2c98

edits
---

diff --git a/jpf.properties b/jpf.properties
index 57b7670..0dd4cae 100644
--- a/jpf.properties
+++ b/jpf.properties
@@ -253,7 +253,7 @@ vm.finalize = false
 
 # this is a preemption boundary specifying the max number of instructions after which we
 # break the current transition if there are other runnable threads
-vm.max_transition_length = 50000
+vm.max_transition_length = 2000000000
 
 # are thread ids of terminated threads with recycled thread objects reused when creating new
 # threads. This is required for programs that sequentially create many short living threads
diff --git a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
index bdd6355..da14d02 100644
--- a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
+++ b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
@@ -21,6 +21,10 @@ package gov.nasa.jpf.vm.serialize;
 import java.util.Iterator;
 
 import gov.nasa.jpf.vm.ElementInfo;
+import gov.nasa.jpf.vm.StaticElementInfo;
+import gov.nasa.jpf.vm.Fields;
+import gov.nasa.jpf.util.FinalBitSet;
+import gov.nasa.jpf.vm.ClassInfo;
 import gov.nasa.jpf.vm.Instruction;
 import gov.nasa.jpf.vm.MJIEnv;
 import gov.nasa.jpf.vm.StackFrame;
@@ -79,6 +83,14 @@ public class CFSerializer extends FilteringSerializer {
       buf.add(MJIEnv.NULL);
     } else {
       ElementInfo ei = heap.get(objref);
+      ClassInfo ci = ei.getClassInfo();
+
+      if (SmartThingsConfig.instance.ignoreClass(ci)) {
+        ei.setSid(0);
+        buf.add(0);
+        return;
+      }
+      
       int sid = ei.getSid();
 
       if (positiveSid){ // count sid upwards from 1
@@ -102,29 +114,54 @@ public class CFSerializer extends FilteringSerializer {
   }
 
 
-  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;
     }
   }
+
+  //Don't think we actually have static fields...so this should be safe
+  @Override
+  protected void serializeClassLoaders(){
+  }
+
+  protected void serializeClass (StaticElementInfo sei){
+    // buf.add(sei.getStatus());
+    
+    Fields fields = sei.getFields();
+    ClassInfo ci = sei.getClassInfo();
+    FinalBitSet filtered = getStaticFilterMask(ci);
+    FinalBitSet refs = getStaticRefMask(ci);
+    int max = ci.getStaticDataSize();
+    if (SmartThingsConfig.instance.staticClass(ci))
+      return;
+    for (int i = 0; i < max; i++) {
+      if (!filtered.get(i)) {
+        int v = fields.getIntValue(i);
+        if (refs.get(i)) {
+          processReference(v);
+        } else {
+          buf.add(v);
+        }
+      }
+    }
+  }
+
   
   @Override
   protected void serializeFrame(StackFrame frame){
     FramePolicy fp = getFramePolicy(frame.getMethodInfo());
     Instruction pc = frame.getPC();
     int len = frame.getTopPos()+1;
-    
-    if (fp == null || fp.includePC || istop) {
+
+    if (fp == null || fp.includePC) {
       buf.add(frame.getMethodInfo().getGlobalId());
       buf.add( pc != null ? pc.getInstructionIndex() : -1);
     }
 
-    if (fp == null || fp.includeLocals || istop) {
+    if (fp == null || fp.includeLocals) {
       buf.add(len);
       
       // unfortunately we can't do this as a block operation because that
diff --git a/src/main/gov/nasa/jpf/vm/serialize/FilteringSerializer.java b/src/main/gov/nasa/jpf/vm/serialize/FilteringSerializer.java
index 2a90765..236a9b0 100644
--- a/src/main/gov/nasa/jpf/vm/serialize/FilteringSerializer.java
+++ b/src/main/gov/nasa/jpf/vm/serialize/FilteringSerializer.java
@@ -448,7 +448,7 @@ public class FilteringSerializer extends AbstractSerializer implements Reference
 
   @Override
   protected int[] computeStoringData() {
-
+    
     buf.clear();
     heap = ks.getHeap();
     initReferenceQueue();
@@ -481,4 +481,4 @@ public class FilteringSerializer extends AbstractSerializer implements Reference
     }
     System.out.println(']');
   }
-}
\ No newline at end of file
+}
diff --git a/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java b/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
index 70d8589..94fc0f3 100644
--- a/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
+++ b/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
@@ -31,7 +31,35 @@ import gov.nasa.jpf.vm.serialize.AmmendableFilterConfiguration.FrameAmmendment;
 public class SmartThingsConfig
   implements FieldAmmendment, FrameAmmendment {
 
-  boolean ignoreClass(ClassInfo ci) {
+  public boolean staticClass(ClassInfo ci) {
+    String pName = ci.getName();
+    if (pName.startsWith("java."))
+      return true;
+
+    if (pName.startsWith("sun."))
+      return true;
+
+    if (pName.startsWith("com.sun"))
+      return true;
+
+    if (pName.startsWith("org."))
+      return true;
+
+    if (pName.startsWith("groovy."))
+      return true;
+
+    if (pName.startsWith("groovyjarjarasm."))
+      return true;
+
+    if (pName.startsWith("gov."))
+      return true;
+
+    if (pName.startsWith("["))
+      return true;
+
+    return false;
+  }
+  public boolean ignoreClass(ClassInfo ci) {
     String pName = ci.getName();
     if (pName.startsWith("org")) {
       if (pName.startsWith("org.codehaus.groovy")) {
@@ -53,11 +81,10 @@ public class SmartThingsConfig
         if (pName.startsWith("java.lang.ClassLoader")) {
           return true;
         }
-        if (pName.startsWith("java.lang.Thread$State")) {
-          return true;
-        }
         if (pName.startsWith("java.lang.Class"))
           return true;
+        if (pName.startsWith("java.lang.Thread"))
+          return true;
         if (pName.startsWith("java.lang.Package"))
           return true;
       } else {
@@ -104,7 +131,8 @@ public class SmartThingsConfig
       return true;
     if (pName.startsWith("sun.net.www"))
       return true;
-    
+    if (pName.startsWith("gov.nasa"))
+      return true;
     return false;
   }