From a72c2918352d91d3977dffa479007873e5da1a96 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Fri, 2 Aug 2019 12:33:03 -0700
Subject: [PATCH 1/1] SmartThings support

---
 jpf.properties                                |  1 +
 .../jpf/vm/serialize/SmartThingsConfig.java   | 69 +++++++++++++++++++
 .../SmartThingsFilterConfiguration.java       | 50 ++++++++++++++
 3 files changed, 120 insertions(+)
 create mode 100644 src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
 create mode 100644 src/main/gov/nasa/jpf/vm/serialize/SmartThingsFilterConfiguration.java

diff --git a/jpf.properties b/jpf.properties
index 8c0270d..57b7670 100644
--- a/jpf.properties
+++ b/jpf.properties
@@ -131,6 +131,7 @@ vm.backtracker.class = gov.nasa.jpf.vm.DefaultBacktracker
 vm.serializer.class = gov.nasa.jpf.vm.serialize.CFSerializer
 #vm.serializer.class = gov.nasa.jpf.vm.serialize.AdaptiveSerializer
 #vm.serializer.class = gov.nasa.jpf.vm.serialize.FilteringSerializer
+filter.class = gov.nasa.jpf.vm.serialize.SmartThingsFilterConfiguration
 
 # the class that models static fields and classes
 vm.statics.class = gov.nasa.jpf.vm.OVStatics
diff --git a/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java b/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
new file mode 100644
index 0000000..dcfa11c
--- /dev/null
+++ b/src/main/gov/nasa/jpf/vm/serialize/SmartThingsConfig.java
@@ -0,0 +1,69 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+
+package gov.nasa.jpf.vm.serialize;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.annotation.FilterField;
+import gov.nasa.jpf.annotation.FilterFrame;
+import gov.nasa.jpf.vm.AnnotationInfo;
+import gov.nasa.jpf.vm.FieldInfo;
+import gov.nasa.jpf.vm.ClassInfo;
+import gov.nasa.jpf.vm.MethodInfo;
+import gov.nasa.jpf.vm.serialize.AmmendableFilterConfiguration.FieldAmmendment;
+import gov.nasa.jpf.vm.serialize.AmmendableFilterConfiguration.FrameAmmendment;
+
+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);
+      return true;
+    }
+    if (pName.startsWith("groovy.lang")) {
+      //      System.out.println("Ignoring "+pName);
+      return true;
+    }
+    return false;
+  }
+  
+  @Override
+  public boolean ammendFieldInclusion(FieldInfo fi, boolean sofar) {
+    ClassInfo ci = fi.getClassInfo();
+    if (ignoreClass(ci))
+      return POLICY_IGNORE;
+    
+    return sofar;
+  }
+
+  @Override
+  public FramePolicy ammendFramePolicy(MethodInfo mi, FramePolicy sofar) {
+    ClassInfo ci = mi.getClassInfo();
+    if (ignoreClass(ci)) {
+      sofar.includeLocals = false;
+      sofar.includeOps = false;
+      sofar.includePC = false;
+    }
+
+    return sofar;
+  }
+
+  public static final SmartThingsConfig instance = new SmartThingsConfig();
+}
diff --git a/src/main/gov/nasa/jpf/vm/serialize/SmartThingsFilterConfiguration.java b/src/main/gov/nasa/jpf/vm/serialize/SmartThingsFilterConfiguration.java
new file mode 100644
index 0000000..f51b39d
--- /dev/null
+++ b/src/main/gov/nasa/jpf/vm/serialize/SmartThingsFilterConfiguration.java
@@ -0,0 +1,50 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+
+package gov.nasa.jpf.vm.serialize;
+
+import gov.nasa.jpf.Config;
+
+
+public class SmartThingsFilterConfiguration extends AmmendableFilterConfiguration {
+  @Override
+  public void init(Config config) {
+    // these built-in come first
+    appendStaticAmmendment(IgnoreConstants.instance);
+    appendInstanceAmmendment(IgnoreReflectiveNames.instance);
+    appendFieldAmmendment(IgnoreThreadNastiness.instance);
+    appendFieldAmmendment(IgnoreUtilSilliness.instance);
+
+    appendFrameAmmendment(SmartThingsConfig.instance);
+    appendStaticAmmendment(SmartThingsConfig.instance);
+    appendFieldAmmendment(SmartThingsConfig.instance);
+    
+    // ignores (e.g. NoMatch) from annotations
+    IgnoresFromAnnotations ignores = new IgnoresFromAnnotations(config); 
+    appendFieldAmmendment(ignores);
+    appendFrameAmmendment(ignores);
+    
+    // configured via properties
+    super.init(config);
+    
+    // includes (e.g. ForceMatch) from annotations
+    IncludesFromAnnotations includes = new IncludesFromAnnotations(config); 
+    appendFieldAmmendment(includes);
+    //appendFrameAmmendment(includes);
+  }
+}
-- 
2.34.1