changeset 22:cd7880ab73c7

fixed JPF_.._Verify.registerChoiceGenerator() to not break and ignore the transition if there are no choices, but to just return the provided default value. Thanks to Pascal Kessell for reporting added a .include_null option for the TypedObjectChoice CG. If it is set (default) 'null' is included in the choice set added a dedicated reg test for TypedObjectChoice, removed the one in DataChoiceTest
author Peter Mehlitz <pcmehlitz@gmail.com>
date Tue, 14 Apr 2015 15:01:25 -0700
parents caa0924e093d
children db918c531e6d
files src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java src/main/gov/nasa/jpf/vm/choice/TypedObjectChoice.java src/tests/gov/nasa/jpf/test/mc/data/DataChoiceTest.java src/tests/gov/nasa/jpf/test/mc/data/TypedObjectChoiceTest.java
diffstat 4 files changed, 121 insertions(+), 43 deletions(-) [+]
line wrap: on
line diff
--- a/src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java	Fri Apr 10 20:53:11 2015 -0700
+++ b/src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java	Tue Apr 14 15:01:25 2015 -0700
@@ -345,16 +345,14 @@
 
     String key = id + ".class";
     gen = config.getEssentialInstance(key, cgClass, cgArgTypes, cgArgs);
-
     return gen;
   }
 
   static <T> T registerChoiceGenerator (MJIEnv env, SystemState ss, ThreadInfo ti, ChoiceGenerator<T> cg, T dummyVal){
 
     int n = cg.getTotalNumberOfChoices();
-    if (n == 0) { // we need a CG
-      ss.setIgnored(true);
-      ti.breakTransition( cg.getId());
+    if (n == 0) {
+      // nothing, just return the default value
 
     } else if (n == 1 && !breakSingleChoice) {
       // no choice -> no CG optimization
@@ -497,7 +495,7 @@
     if (!ti.isFirstStepInsn()) { // first time around
       String id = env.getStringObject(idRef);
       ReferenceChoiceGenerator cg = createChoiceGenerator( ReferenceChoiceGenerator.class, ss, id);
-      return registerChoiceGenerator(env,ss,ti,cg, 0);
+      return registerChoiceGenerator(env,ss,ti,cg, MJIEnv.NULL);
 
     } else {
       String id = env.getStringObject(idRef);
--- a/src/main/gov/nasa/jpf/vm/choice/TypedObjectChoice.java	Fri Apr 10 20:53:11 2015 -0700
+++ b/src/main/gov/nasa/jpf/vm/choice/TypedObjectChoice.java	Tue Apr 14 15:01:25 2015 -0700
@@ -19,12 +19,7 @@
 package gov.nasa.jpf.vm.choice;
 
 import gov.nasa.jpf.Config;
-import gov.nasa.jpf.vm.ChoiceGeneratorBase;
-import gov.nasa.jpf.vm.ClassInfo;
-import gov.nasa.jpf.vm.ElementInfo;
-import gov.nasa.jpf.vm.Heap;
-import gov.nasa.jpf.vm.VM;
-import gov.nasa.jpf.vm.ReferenceChoiceGenerator;
+import gov.nasa.jpf.vm.*;
 
 import java.util.ArrayList;
 
@@ -33,7 +28,7 @@
  * is a replacement for the old 'Verify.randomObject'
  */
 public class TypedObjectChoice extends ChoiceGeneratorBase<Integer> implements ReferenceChoiceGenerator {
-  
+
   // the requested object type
   protected String type;
   
@@ -53,7 +48,7 @@
     if (type == null) {
       throw conf.exception("missing 'type' property for TypedObjectChoice " + id);
     }
-    
+
     ArrayList<ElementInfo> list = new ArrayList<ElementInfo>();
     
     for ( ElementInfo ei : heap.liveObjects()) {
@@ -62,11 +57,19 @@
         list.add(ei);
       }
     }
-    
+
+    if (conf.getBoolean(id + ".include_null", true)){
+      list.add(null);
+    }
+
     values = new int[list.size()];
     int i = 0;
     for ( ElementInfo ei : list) {
-      values[i++] = ei.getObjectRef();
+      if (ei != null) {
+        values[i++] = ei.getObjectRef();
+      } else {
+        values[i++] = MJIEnv.NULL;
+      }
     }
     
     count = -1;
--- a/src/tests/gov/nasa/jpf/test/mc/data/DataChoiceTest.java	Fri Apr 10 20:53:11 2015 -0700
+++ b/src/tests/gov/nasa/jpf/test/mc/data/DataChoiceTest.java	Tue Apr 14 15:01:25 2015 -0700
@@ -137,32 +137,4 @@
       }
     }
   }
-
-
-
-  @Test
-  public void testTypedObjectChoice() {
-
-    if (!isJPFRun()) {
-      Verify.resetCounter(0);
-    }
-
-    if (verifyNoPropertyViolation("+my_typed_object.class=gov.nasa.jpf.vm.choice.TypedObjectChoice",
-            "+my_typed_object.type=" + MyType.class.getName())) {
-
-      MyType o1 = new MyType("one");
-      MyType o2 = new MyType("two");
-
-      Object o = Verify.getObject("my_typed_object");
-      Verify.incrementCounter(0);
-      System.out.println(o);
-    }
-
-    if (!isJPFRun()) { // this is only executed outside JPF
-      if (Verify.getCounter(0) != 2) {
-        fail("wrong number of backtracks");
-      }
-    }
-
-  }
 }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/tests/gov/nasa/jpf/test/mc/data/TypedObjectChoiceTest.java	Tue Apr 14 15:01:25 2015 -0700
@@ -0,0 +1,105 @@
+/*
+ * Copyright (C) 2015, 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.test.mc.data;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import gov.nasa.jpf.vm.Verify;
+import org.junit.Test;
+
+/**
+ * regression test for TypedObjectChoice CGs
+ */
+public class TypedObjectChoiceTest extends TestJPF {
+
+  static class A {
+    int id;
+    A (int i){
+      id = i;
+    }
+    public String toString(){ return String.format("A(%d)", id); }
+  }
+
+  @Test
+  public void testNoCG (){
+    if (verifyNoPropertyViolation("+mycg.class=gov.nasa.jpf.vm.choice.TypedObjectChoice",
+            "+mycg.include_null=false",
+            "+mycg.type=" + getClass().getName() + "$A")){
+      Object o = Verify.getObject("mycg");
+      System.out.print("got object: ");
+      System.out.println(o);
+
+      assertTrue( o == null);
+    }
+  }
+
+  @Test
+  public void testNoObject (){
+    if (verifyNoPropertyViolation("+mycg.class=gov.nasa.jpf.vm.choice.TypedObjectChoice",
+                                  "+mycg.include_null=true",
+                                  "+mycg.type=" + getClass().getName() + "$A")){
+      Object o = Verify.getObject("mycg");
+      System.out.print("got object: ");
+      System.out.println(o);
+
+      assertTrue( o == null);
+    }
+  }
+
+  @Test
+  public void testObject (){
+    if (verifyNoPropertyViolation("+mycg.class=gov.nasa.jpf.vm.choice.TypedObjectChoice",
+            "+mycg.include_null=false",
+            "+mycg.type=" + getClass().getName() + "$A")) {
+      A a = new A(42);
+
+      Object o = Verify.getObject("mycg");
+      System.out.print("got object: ");
+      System.out.println(o);
+
+      assertTrue(o instanceof A);
+      a = (A) o;
+      assertTrue(a.id == 42);
+    }
+  }
+
+  @Test
+  public void testMultipleObjects(){
+    if (verifyNoPropertyViolation("+mycg.class=gov.nasa.jpf.vm.choice.TypedObjectChoice",
+            "+mycg.include_null=false",
+            "+mycg.type=" + getClass().getName() + "$A")) {
+      A a1 = new A(1);
+      A a2 = new A(2);
+
+      Object o = Verify.getObject("mycg");
+      System.out.print("got object: ");
+      System.out.println(o);
+
+      assertTrue(o instanceof A);
+      A a = (A) o;
+      Verify.setBitInBitSet(0, a.id, true);
+      Verify.incrementCounter(0);
+    }
+
+    if (!isJPFRun()){
+      assertTrue( Verify.getCounter(0) == 2);
+      assertTrue( Verify.getBitInBitSet(0, 1));
+      assertTrue( Verify.getBitInBitSet(0, 2));
+    }
+  }
+
+}