From: bdemsky <bdemsky@uci.edu>
Date: Fri, 2 Aug 2019 21:40:08 +0000 (-0700)
Subject: SmartThings specific support to reduce state space
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=bb450df1325bfc34342bc55c1cb0a7110326ad39

SmartThings specific support to reduce state space
---

diff --git a/main.jpf b/main.jpf
index 7b9a3ad..2034df4 100644
--- a/main.jpf
+++ b/main.jpf
@@ -26,6 +26,6 @@ apps=App1,App2
 #track_location_var_conflict=true
 
 # Timeout in minutes (default is 0 which means no timeout)
-timeout=3
+timeout=0
 
 #search.class = gov.nasa.jpf.search.heuristic.UserHeuristic
diff --git a/src/main/gov/nasa/jpf/vm/serialize/AmmendableFilterConfiguration.java b/src/main/gov/nasa/jpf/vm/serialize/AmmendableFilterConfiguration.java
index 1f7befd..b7d4d2e 100644
--- a/src/main/gov/nasa/jpf/vm/serialize/AmmendableFilterConfiguration.java
+++ b/src/main/gov/nasa/jpf/vm/serialize/AmmendableFilterConfiguration.java
@@ -159,6 +159,7 @@ public class AmmendableFilterConfiguration implements FilterConfiguration {
       }
       if (include) {
         v.add(field);
+        //        System.out.println("Including "+field);
       }
     }
     Iterable<FieldInfo> ret = v;
@@ -182,6 +183,7 @@ public class AmmendableFilterConfiguration implements FilterConfiguration {
       }
       if (include) {
         v.add(field);
+        //        System.out.println("Including "+field);
       }
     }
     return v;
diff --git a/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java b/src/main/gov/nasa/jpf/vm/serialize/CFSerializer.java
index 895b94a..bdd6355 100644
--- 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]);
+        }
       }
     }
   }
diff --git a/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java b/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
index dcfa11c..70d8589 100644
--- a/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
+++ b/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
@@ -32,15 +32,79 @@ public class SmartThingsConfig
   implements FieldAmmendment, FrameAmmendment {
 
   boolean ignoreClass(ClassInfo ci) {
-    String pName = ci.getPackageName();
-    if (pName.startsWith("org.codehaus.groovy")) {
-      //      System.out.println("Ignoring "+pName);
+    String pName = ci.getName();
+    if (pName.startsWith("org")) {
+      if (pName.startsWith("org.codehaus.groovy")) {
+        //      System.out.println("Ignoring "+pName);
+        return true;
+      }
+      if (pName.startsWith("org.apache.groovy")) {
+        //      System.out.println("Ignoring "+pName);
+        return true;
+      }
+    } else if (pName.startsWith("java")) {
+      if (pName.startsWith("java.lang")) {
+        if (pName.startsWith("java.lang.reflect")) {
+          return true;
+        }
+        if (pName.startsWith("java.lang.ref")) {
+          return true;
+        }
+        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.Package"))
+          return true;
+      } else {
+      if (pName.startsWith("java.util.concurrent")) {
+        //      System.out.println("Ignoring "+pName);
+        return true;
+      }
+      if (pName.startsWith("java.util.logging")) {
+        //      System.out.println("Ignoring "+pName);
+        return true;
+      }
+      if (pName.startsWith("java.beans")) {
+        return true;
+      }
+      if (pName.startsWith("java.io.OutputStreamWriter"))
+        return true;
+      if (pName.startsWith("java.io.PrintStream"))
+        return true;
+      if (pName.startsWith("java.io.BufferedWriter"))
+        return true;
+      }
+      if (pName.startsWith("java.nio.charset"))
+        return true;
+      
+    } else if (pName.startsWith("groovy")) {
+      if (pName.startsWith("groovy.lang")) {
+        //      System.out.println("Ignoring "+pName);
+        return true;
+      }
+      if (pName.startsWith("groovyjarjarasm.asm")) {
+        //      System.out.println("Ignoring "+pName);
+        return true;
+      }
+    }
+    if (pName.startsWith("com.sun.beans")) {
       return true;
     }
-    if (pName.startsWith("groovy.lang")) {
-      //      System.out.println("Ignoring "+pName);
+    if (pName.startsWith("sun.reflect")) {
       return true;
     }
+    if (pName.startsWith("sun.misc.SharedSecrets"))
+      return true;
+    if (pName.startsWith("sun.util.logging"))
+      return true;
+    if (pName.startsWith("sun.net.www"))
+      return true;
+    
     return false;
   }
   
@@ -49,7 +113,9 @@ public class SmartThingsConfig
     ClassInfo ci = fi.getClassInfo();
     if (ignoreClass(ci))
       return POLICY_IGNORE;
-    
+    ClassInfo civ = fi.getTypeClassInfo();
+    if (ignoreClass(civ))
+      return POLICY_IGNORE;      
     return sofar;
   }
 
@@ -60,6 +126,8 @@ public class SmartThingsConfig
       sofar.includeLocals = false;
       sofar.includeOps = false;
       sofar.includePC = false;
+    } else {
+      //      System.out.println("Including M: " +mi);
     }
 
     return sofar;