javapathfinder-devel — development related topics (your place if you work with the sources)

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/tools RaceDetector.java,1.3,1.4

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv3832

Modified Files:
	RaceDetector.java 
Log Message:
forgot to clone the lockSet elements, which causes subsequent comparisons to
fail after a backtrack (ElementInfo indices are reset to -1)

using toString() to store the lock ElementInfos is lame (slow), but safe
and convenient. I'm lazy today 


Index: RaceDetector.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/RaceDetector.java,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- RaceDetector.java	25 Aug 2005 18:55:44 -0000	1.3
+++ RaceDetector.java	5 Oct 2005 06:17:07 -0000	1.4
@@ -22,6 +22,7 @@
 import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.Iterator;
+import java.util.LinkedList;
 import java.util.Stack;
 
 import gov.nasa.jpf.PropertyListenerAdapter;
@@ -49,7 +50,9 @@
  */
 public class RaceDetector extends PropertyListenerAdapter {
   
+  
   /*** helper classes ***************************************************************/
+  
   static class FieldAccess {
     ThreadInfo ti;
     Object[] locksHeld;          // the ones we have during this operation (not really required)
@@ -61,8 +64,18 @@
     FieldAccess (ThreadInfo ti, FieldInstruction finsn) {
       this.ti = ti;
       this.finsn = finsn;
-      this.locksHeld = ti.getLockedObjects().toArray();
       
+      // we have to do some sort of cloning, since the lockSet and the 
+      // ElementInfos in it are going to be changed by JPF
+      LinkedList lockSet = ti.getLockedObjects();
+      locksHeld = new Object[lockSet.size()];
+      if (locksHeld.length > 0) {
+        Iterator it = lockSet.iterator();
+        for (int i=0; it.hasNext(); i++) {
+          locksHeld[i] = ((ElementInfo)it.next()).toString(); // <2do> - that's lame, but convenient
+        }
+      }
+            
       // <2do> we should also hash the threads callstack here
     }
   

[Javapathfinder-devel] javapathfinder/env/jpf/java/lang Class.java,1.3,1.4

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/env/jpf/java/lang
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv1242/jpf/java/lang

Modified Files:
	Class.java 
Log Message:
nce it is easy enough and we needed a quick solution, today's 5min hack is to add Class.getSuperclass()


Index: Class.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/env/jpf/java/lang/Class.java,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- Class.java	18 May 2005 06:41:46 -0000	1.3
+++ Class.java	23 Sep 2005 17:12:45 -0000	1.4
@@ -126,15 +126,7 @@
     return isPrimitive;
   }
 
-  /* the following methods are not (yet) supported, but are required by some
-   * braindead IDEs who cannot compile classes w/o putting them into the
-   * build classpath - which means they will use THIS java.lang.Class to
-   * compile the rest of JPF. Don't ask what I think of this
-   */
-  public Class getSuperclass () {
-    // <2do>
-    throw new JPFException("Class.getSuperClass() not yet supported");
-  }
+  public native Class getSuperclass ();
 
   public native Object newInstance () throws InstantiationException,
                                       IllegalAccessException;

[Javapathfinder-devel] javapathfinder/env/jvm/gov/nasa/jpf/jvm JPF_java_lang_Class.java,1.2,1.3

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/env/jvm/gov/nasa/jpf/jvm
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv1242/jvm/gov/nasa/jpf/jvm

Modified Files:
	JPF_java_lang_Class.java 
Log Message:
nce it is easy enough and we needed a quick solution, today's 5min hack is to add Class.getSuperclass()


Index: JPF_java_lang_Class.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- JPF_java_lang_Class.java	5 May 2005 01:03:54 -0000	1.2
+++ JPF_java_lang_Class.java	23 Sep 2005 17:12:45 -0000	1.3
@@ -121,6 +121,16 @@
     return ref;
   }
   
+  public static int getSuperclass (MJIEnv env, int robj) {
+    ClassInfo ci = getReferringClassInfo(env, robj);
+    ClassInfo sci = ci.getSuperClass();
+    if (sci != null) {
+      return sci.getClassObjectRef();
+    } else {
+      return MJIEnv.NULL;
+    }
+  }
+  
   static ClassInfo getReferringClassInfo (MJIEnv env, int robj) {
     // this is only the ElementInfo for the java.lang.Class object
     ElementInfo ei = env.getElementInfo(robj);

[Javapathfinder-devel] /javapathfinder/examples testchoices.IntChoiceFromStaticVarSet.properties,1.1,1.2

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder//javapathfinder/examples
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv28076/examples

Modified Files:
	testchoices.IntChoiceFromStaticVarSet.properties 
Log Message:
* missing uppercase at beginning of class name - partially worked but jpf failed strangely

Index: testchoices.IntChoiceFromStaticVarSet.properties
===================================================================
RCS file: /cvsroot/javapathfinder//javapathfinder/examples/testchoices.IntChoiceFromStaticVarSet.properties,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- testchoices.IntChoiceFromStaticVarSet.properties	12 Sep 2005 16:25:09 -0000	1.1
+++ testchoices.IntChoiceFromStaticVarSet.properties	12 Sep 2005 18:01:30 -0000	1.2
@@ -12,7 +12,7 @@
 
 yTest.class = gov.nasa.jpf.jvm.choice.IntChoiceFromStaticVarSet
 
-yTest.values = intChoices.FIFTY, IntChoices.ONE
+yTest.values = IntChoices.FIFTY, IntChoices.ONE
 
 # expected output: (assuming values match names in IntChoices class)
 	

[Javapathfinder-devel] javapathfinder/examples testchoices.IntChoiceFromStaticVarSet.properties,NONE,1.1

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/examples
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv6226/examples

Added Files:
	testchoices.IntChoiceFromStaticVarSet.properties 
Log Message:
* another example


--- NEW FILE: testchoices.IntChoiceFromStaticVarSet.properties ---

#
# Choice configuration
#

# this is to use -show to confirm 
testchoice.properties = IntChoiceFromStaticVarSet

xTest.class = gov.nasa.jpf.jvm.choice.IntChoiceFromStaticVarSet

xTest.values = IntChoices.ONE, IntChoices.TWO, IntChoices.THREE

yTest.class = gov.nasa.jpf.jvm.choice.IntChoiceFromStaticVarSet

yTest.values = intChoices.FIFTY, IntChoices.ONE

# expected output: (assuming values match names in IntChoices class)
	
#	x is 1
#	y is 50
#	program end
#	y is 1
#	program end
#	x is 2
#	y is 50
#	program end
# 	y is 1
#	program end
#	x is 3
#	y is 50
#	program end
# 	y is 1
#	program end
	
	

[Javapathfinder-devel] javapathfinder/examples IntChoices.java,1.1,1.2

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/examples
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv6115/examples

Modified Files:
	IntChoices.java 
Log Message:
* added some static constants for examples
	
		

Index: IntChoices.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/examples/IntChoices.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- IntChoices.java	11 Sep 2005 16:17:29 -0000	1.1
+++ IntChoices.java	12 Sep 2005 16:24:31 -0000	1.2
@@ -30,6 +30,13 @@
 
 public class IntChoices {
 
+	
+	static final int ONE = 1;
+	static final int TWO = 2;
+	static int THREE = 3;
+	static int FIFTY = 50;
+	
+	
 	static int x = 5;
 	static int y = 55;
 	

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm/choice IntChoiceFromSet.java,1.3,1.4

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv5731/src/gov/nasa/jpf/jvm/choice

Modified Files:
	IntChoiceFromSet.java 
Log Message:
* added some static constants for examples
	
		

Index: IntChoiceFromSet.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/IntChoiceFromSet.java,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- IntChoiceFromSet.java	11 Sep 2005 16:16:14 -0000	1.3
+++ IntChoiceFromSet.java	12 Sep 2005 16:23:20 -0000	1.4
@@ -1,4 +1,4 @@
-//
+ //
 //Copyright (C) 2005 United States Government as represented by the
 //Administrator of the National Aeronautics and Space Administration
 //(NASA).  All Rights Reserved.

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm/choice IntChoiceFromStaticVarSet.java,NONE,1.1

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv5606/src/gov/nasa/jpf/jvm/choice

Added Files:
	IntChoiceFromStaticVarSet.java 
Log Message:
* choic generator under construction - not passing tests yet

--- NEW FILE: IntChoiceFromStaticVarSet.java ---
//
//Copyright (C) 2005 United States Government as represented by the
//Administrator of the National Aeronautics and Space Administration
//(NASA).  All Rights Reserved.
//
//This software is distributed under the NASA Open Source Agreement
//(NOSA), version 1.3.  The NOSA has been approved by the Open Source
//Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
//directory tree for the complete NOSA document.
//
//THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
//KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
//LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
//SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
//A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
//THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
//DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
//

/*
 * Created on Sep 8, 2005
 *
 * TODO To change the template for this generated file go to
 * Window - Preferences - Java - Code Style - Code Templates
 */
package gov.nasa.jpf.jvm.choice;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.jvm.IntChoiceGenerator;
import gov.nasa.jpf.jvm.JVM;
import gov.nasa.jpf.jvm.StaticElementInfo;
import gov.nasa.jpf.jvm.ClassInfo;
/**
 * @author jpenix
 *
 * choose from a set of static variables (auch as an enumeration)
 * specified in a configuration as
 * bob.class = IntChoiceFromStaticVarSet
 * bob.values = {MyClass.ONE, MyClass.TWO, MyOtherClass.OTHER}
 * where "bob" is the choice id.
 * 
 * choices can then made using: getInt("bob");
 */
/**
 * @author jpenix
 *
 * TODO To change the template for this generated type comment go to
 * Window - Preferences - Java - Code Style - Code Templates
 */
public class IntChoiceFromStaticVarSet extends IntChoiceGenerator {

	String[] values;
	int count = -1;
	
	/**
	 * @param conf - JPF configuration object
	 * @param id - String identifier for the choice instance. this should be unique.
	 */
	public IntChoiceFromStaticVarSet(Config conf, String id) {
		super(id);
		values = conf.getStringArray(id + ".values");
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.IntChoiceGenerator#getNextChoice()
	 */
	public int getNextChoice(JVM vm) {
		
		//split out class name and variable name
		String[] varId = values[count].split("[.]+");

	    ClassInfo ci = ClassInfo.getClassInfo(varId[0]);
	    StaticElementInfo ei = vm.getKernelState().sa.get(ci.getName());
	    int ret = ei.getIntField(varId[1], null);

		// print "Choice: bob = MyClass.ONE(1)"
		vm.println("Choice: "+id + " = " + values[count] + "("+ret+")");
	    return ret;
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#hasMoreChoices()
	 */
	public boolean hasMoreChoices(JVM vm) {
		if (count < values.length-1)
			return true;
		else
			return false;
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#advance(gov.nasa.jpf.jvm.JVM)
	 */
	public void advance(JVM vm) {
		count++;
	}

}

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm/choice TwoIntChoice.java,1.2,1.3 IntChoiceFromSet.java,1.2,1.3

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv26770/src/gov/nasa/jpf/jvm/choice

Modified Files:
	TwoIntChoice.java IntChoiceFromSet.java 
Log Message:
* two new choice generators for integers

Index: IntChoiceFromSet.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/IntChoiceFromSet.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- IntChoiceFromSet.java	9 Sep 2005 23:31:42 -0000	1.2
+++ IntChoiceFromSet.java	11 Sep 2005 16:16:14 -0000	1.3
@@ -1,3 +1,22 @@
+//
+//Copyright (C) 2005 United States Government as represented by the
+//Administrator of the National Aeronautics and Space Administration
+//(NASA).  All Rights Reserved.
+//
+//This software is distributed under the NASA Open Source Agreement
+//(NOSA), version 1.3.  The NOSA has been approved by the Open Source
+//Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
+//directory tree for the complete NOSA document.
+//
+//THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
+//KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
+//LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
+//SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
+//A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
+//THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
+//DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
+//
+
 /*
  * Created on Sep 8, 2005
  *
@@ -9,7 +28,7 @@
 import gov.nasa.jpf.Config;
 import gov.nasa.jpf.jvm.IntChoiceGenerator;
 import gov.nasa.jpf.jvm.JVM;
-
+import gov.nasa.jpf.JPFException;
 /**
  * @author jpenix
  *
@@ -22,34 +41,42 @@
  */
 public class IntChoiceFromSet extends IntChoiceGenerator {
 
+	// int values to choose from stored as strings
 	String[] values;
-	int count = 0;
+	
+	int count = -1;
 	
 	/**
 	 * @param id
 	 */
 	public IntChoiceFromSet(Config conf, String id) {
 		super(id);
-		values = conf.getStringArray("values");
+		values = conf.getStringArray(id + ".values");
+		if (values == null) {
+			throw new JPFException("value set for <" + id + "> choice did not load");
+		}
 	}
 
 	/* (non-Javadoc)
 	 * @see gov.nasa.jpf.jvm.IntChoiceGenerator#getNextChoice()
 	 */
 	public int getNextChoice(JVM vm) {
-//		try {
-			int ret = Integer.parseInt(values[count]);
-			System.out.println(id + ": " + ret);
+		
+		try {
+		// watch out this returns 0 if it parses wrong
+		int ret = Integer.parseInt(values[count]); 
+			vm.println(id + ": " + ret);
 	        return ret;
-//	      } catch (NumberFormatException nfx) {
-//	        return 0;
+	      } catch (NumberFormatException nfx) {
+	        throw new JPFException("Number format error for <" + id +">: parsing \"" + values[count] +"\"");
+	      }
 	}
 
 	/* (non-Javadoc)
 	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#hasMoreChoices()
 	 */
 	public boolean hasMoreChoices(JVM vm) {
-		if (count < values.length)
+		if (count < values.length-1)  
 			return true;
 		else
 			return false;

Index: TwoIntChoice.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/TwoIntChoice.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- TwoIntChoice.java	9 Sep 2005 23:31:42 -0000	1.2
+++ TwoIntChoice.java	11 Sep 2005 16:16:14 -0000	1.3
@@ -1,3 +1,22 @@
+//
+//Copyright (C) 2005 United States Government as represented by the
+//Administrator of the National Aeronautics and Space Administration
+//(NASA).  All Rights Reserved.
+//
+//This software is distributed under the NASA Open Source Agreement
+//(NOSA), version 1.3.  The NOSA has been approved by the Open Source
+//Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
+//directory tree for the complete NOSA document.
+//
+//THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
+//KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
+//LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
+//SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
+//A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
+//THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
+//DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
+//
+
 /*
  * Created on Sep 7, 2005
  *
@@ -17,8 +36,8 @@
  */
 public class TwoIntChoice extends IntChoiceGenerator {
 
-	int firstValue = 1;
-	int secondValue = 0;
+	int firstValue = 100;
+	int secondValue = 200;
 
 	String firstMsg = "pass";
 	String secondMsg = "fail";
@@ -41,12 +60,13 @@
 		switch (state){
 			case 0: {
 				ret = firstValue;
-				System.out.println(firstMsg);
+				vm.println(firstMsg);
 				break;
 			}
 			case 1: {
 				ret = secondValue;
-				System.out.println(secondMsg);
+				vm.println(secondMsg);
+				break;
 			}
 			default: { 
 				ret = 99;
@@ -67,6 +87,7 @@
 	 */
 	public void advance(JVM vm) {
 		state++;
+		//vm.println("advancing to state "+state);
 	}
 
 }

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm ChoiceGenerator.java,1.2,1.3 DoubleChoiceGenerator.java,1.1,1.2 SystemState.java,1.3,1.4 BooleanChoiceGenerator.java,1.1,1.2 JPF_gov_nasa_jpf_jvm_Verify.java,1.3,1.4 IntChoiceGenerator.java,1.1,1.2

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv3727/src/gov/nasa/jpf/jvm

Modified Files:
	ChoiceGenerator.java DoubleChoiceGenerator.java 
	SystemState.java BooleanChoiceGenerator.java 
	JPF_gov_nasa_jpf_jvm_Verify.java IntChoiceGenerator.java 
Log Message:
slightly changed the ChoiceGenerator API so that advance(), hasMoreChoices() and getNextChoice() all get the VM passed in as a parameter. So that ChoiceGenerators can do real fancy stuff at any time.

Still the preferred way should be to somehow compute the choice set the first time advance() is called - for performance, traceability and esp. coverage reasons. That way, we can JPF ask at any time "how many open upstream choices do you still have?"

Index: JPF_gov_nasa_jpf_jvm_Verify.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- JPF_gov_nasa_jpf_jvm_Verify.java	8 Sep 2005 23:24:31 -0000	1.3
+++ JPF_gov_nasa_jpf_jvm_Verify.java	9 Sep 2005 23:31:43 -0000	1.4
@@ -155,7 +155,7 @@
       gen = vm.createBooleanChoiceGenerator();
     }
     if (gen instanceof BooleanChoiceGenerator) {
-      return ((BooleanChoiceGenerator)gen).getNextChoice(); 
+      return ((BooleanChoiceGenerator)gen).getNextChoice(vm); 
     } else {
       // we are in trouble
       throw new JPFException("wrong ChoiceGenerator type: " + gen + " not boolean");
@@ -170,7 +170,7 @@
       gen = vm.createIntChoiceGenerator(min, max);
     }
     if (gen instanceof IntChoiceGenerator) {
-      return ((IntChoiceGenerator)gen).getNextChoice(); 
+      return ((IntChoiceGenerator)gen).getNextChoice(vm); 
     } else {
       // we are in trouble
       throw new JPFException("wrong ChoiceGenerator type: " + gen + " not boolean");
@@ -194,7 +194,7 @@
     }
     
     if (gen instanceof IntChoiceGenerator) {
-      return ((IntChoiceGenerator)gen).getNextChoice(); 
+      return ((IntChoiceGenerator)gen).getNextChoice(vm); 
     } else {
       // we are in trouble
       if (id == null) {
@@ -221,7 +221,7 @@
     }
     
     if (gen instanceof DoubleChoiceGenerator) {
-      return ((DoubleChoiceGenerator)gen).getNextChoice(); 
+      return ((DoubleChoiceGenerator)gen).getNextChoice(vm); 
     } else {
       // we are in trouble
       if (id == null) {

Index: BooleanChoiceGenerator.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/BooleanChoiceGenerator.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- BooleanChoiceGenerator.java	7 Sep 2005 22:08:20 -0000	1.1
+++ BooleanChoiceGenerator.java	9 Sep 2005 23:31:43 -0000	1.2
@@ -38,11 +38,11 @@
   super(id);
 }
 
-public boolean hasMoreChoices() {
+public boolean hasMoreChoices(JVM vm) {
   return (state < 1);
 }
 
-public boolean getNextChoice () {
+public boolean getNextChoice (JVM vm) {
   return (state < 1);
 }
 

Index: DoubleChoiceGenerator.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/DoubleChoiceGenerator.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- DoubleChoiceGenerator.java	7 Sep 2005 22:08:20 -0000	1.1
+++ DoubleChoiceGenerator.java	9 Sep 2005 23:31:43 -0000	1.2
@@ -28,5 +28,5 @@
   super(id);
 }
 
-public abstract double getNextChoice ();
+public abstract double getNextChoice (JVM vm);
 }

Index: SystemState.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/SystemState.java,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- SystemState.java	9 Sep 2005 04:55:38 -0000	1.3
+++ SystemState.java	9 Sep 2005 23:31:43 -0000	1.4
@@ -308,7 +308,7 @@
   void scheduleNext (JVM jvm) {
     // <2do> this is a hack for now to avoid having to change "nextSuccessor"
     // but it should go away as soon as the Scheduler becomes a Choice Generator too
-    if ((gen != null) && (gen.hasMoreChoices())) return;
+    if ((gen != null) && (gen.hasMoreChoices(jvm))) return;
 
     sch.next();
   }

Index: ChoiceGenerator.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ChoiceGenerator.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- ChoiceGenerator.java	8 Sep 2005 23:25:15 -0000	1.2
+++ ChoiceGenerator.java	9 Sep 2005 23:31:43 -0000	1.3
@@ -43,7 +43,7 @@
   this.idRef = idRef;
 }
 
-public abstract boolean hasMoreChoices ();
+public abstract boolean hasMoreChoices (JVM vm);
 
 public abstract void advance (JVM vm);
 }

Index: IntChoiceGenerator.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/IntChoiceGenerator.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- IntChoiceGenerator.java	7 Sep 2005 22:08:20 -0000	1.1
+++ IntChoiceGenerator.java	9 Sep 2005 23:31:43 -0000	1.2
@@ -27,5 +27,5 @@
   super(id);
 }
 
-public abstract int getNextChoice ();
+public abstract int getNextChoice (JVM vm);
 }

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm/choice TwoIntChoice.java,1.1,1.2 DoubleThresholdGenerator.java,1.1,1.2 IntChoiceFromSet.java,1.1,1.2 IntIntervalGenerator.java,1.2,1.3

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv3727/src/gov/nasa/jpf/jvm/choice

Modified Files:
	TwoIntChoice.java DoubleThresholdGenerator.java 
	IntChoiceFromSet.java IntIntervalGenerator.java 
Log Message:
slightly changed the ChoiceGenerator API so that advance(), hasMoreChoices() and getNextChoice() all get the VM passed in as a parameter. So that ChoiceGenerators can do real fancy stuff at any time.

Still the preferred way should be to somehow compute the choice set the first time advance() is called - for performance, traceability and esp. coverage reasons. That way, we can JPF ask at any time "how many open upstream choices do you still have?"

Index: DoubleThresholdGenerator.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/DoubleThresholdGenerator.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- DoubleThresholdGenerator.java	8 Sep 2005 23:21:04 -0000	1.1
+++ DoubleThresholdGenerator.java	9 Sep 2005 23:31:42 -0000	1.2
@@ -41,11 +41,11 @@
   state = -1;
 }
 
-public boolean hasMoreChoices () {
+public boolean hasMoreChoices (JVM vm) {
   return (state < 2);
 }
 
-public double getNextChoice () {
+public double getNextChoice (JVM vm) {
   switch (state) {
   case -1:
   case 0: return low;

Index: IntChoiceFromSet.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/IntChoiceFromSet.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- IntChoiceFromSet.java	8 Sep 2005 23:21:04 -0000	1.1
+++ IntChoiceFromSet.java	9 Sep 2005 23:31:42 -0000	1.2
@@ -36,7 +36,7 @@
 	/* (non-Javadoc)
 	 * @see gov.nasa.jpf.jvm.IntChoiceGenerator#getNextChoice()
 	 */
-	public int getNextChoice() {
+	public int getNextChoice(JVM vm) {
 //		try {
 			int ret = Integer.parseInt(values[count]);
 			System.out.println(id + ": " + ret);
@@ -48,7 +48,7 @@
 	/* (non-Javadoc)
 	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#hasMoreChoices()
 	 */
-	public boolean hasMoreChoices() {
+	public boolean hasMoreChoices(JVM vm) {
 		if (count < values.length)
 			return true;
 		else

Index: IntIntervalGenerator.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/IntIntervalGenerator.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- IntIntervalGenerator.java	9 Sep 2005 04:55:39 -0000	1.2
+++ IntIntervalGenerator.java	9 Sep 2005 23:31:42 -0000	1.3
@@ -76,11 +76,11 @@
   init();
 }
 
-public int getNextChoice () {
+public int getNextChoice (JVM vm) {
   return next;
 }
 
-public boolean hasMoreChoices () {
+public boolean hasMoreChoices (JVM vm) {
   if (delta > 0) {
     return (next < max);
   } else {

Index: TwoIntChoice.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/TwoIntChoice.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- TwoIntChoice.java	8 Sep 2005 23:21:04 -0000	1.1
+++ TwoIntChoice.java	9 Sep 2005 23:31:42 -0000	1.2
@@ -36,7 +36,7 @@
 	/* (non-Javadoc)
 	 * @see gov.nasa.jpf.jvm.IntChoiceGenerator#getNextChoice()
 	 */
-	public int getNextChoice() {
+	public int getNextChoice(JVM vm) {
 		int ret;
 		switch (state){
 			case 0: {
@@ -58,7 +58,7 @@
 	/* (non-Javadoc)
 	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#hasMoreChoices()
 	 */
-	public boolean hasMoreChoices() {
+	public boolean hasMoreChoices(JVM vm) {
 		return state < 1;
 	}
 

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/tools IdleFilter.java,1.3,1.4

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv12883/src/gov/nasa/jpf/tools

Modified Files:
	IdleFilter.java 
Log Message:
bad, bad back porter! half of the ChoiceGenerator interfacing was missing, the other half was wrong. Added some convenience array getters to Config, but those are not terribly efficient 

Index: IdleFilter.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/IdleFilter.java,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- IdleFilter.java	16 Aug 2005 22:27:33 -0000	1.3
+++ IdleFilter.java	9 Sep 2005 04:55:39 -0000	1.4
@@ -36,140 +36,147 @@
 import java.util.logging.Logger;
 
 /**
- * simple combined listener that checks if a thread seems to do idle loops that might starve
- * other threads. The most classical case is a "busy wait" loop like
+ * simple combined listener that checks if a thread seems to do idle loops that
+ * might starve other threads. The most classical case is a "busy wait" loop
+ * like
  * 
- *   for (long l=0; l<1000000; l++);
+ * for (long l=0; l<1000000; l++);
  * 
  * which would give us a pretty long path. Even worse, things like
- *   
- *   while (true);
  * 
- * would never return if we don't break the partial order execution loop.
- * Once IdleFilter determines a thread is not doing anything useful (no field access, no array
- * element access, no method calls, huge number of back jumps), it breaks the POR loop and
- * increases a counter. If it encounters the same thread doing this again consecutively, it
- * marks the state as seen, which prunes the whole search tree underneath it
+ * while (true);
+ * 
+ * would never return if we don't break the partial order execution loop. Once
+ * IdleFilter determines a thread is not doing anything useful (no field access,
+ * no array element access, no method calls, huge number of back jumps), it
+ * breaks the POR loop and increases a counter. If it encounters the same thread
+ * doing this again consecutively, it marks the state as seen, which prunes the
+ * whole search tree underneath it
  */
 public class IdleFilter extends ListenerAdapter {
 
-	static Logger log = JPF.getLogger("gov.nasa.jpf.tools.IdleFilter");
+  static Logger log = JPF.getLogger("gov.nasa.jpf.tools.IdleFilter");
 
-	static class ThreadStat {
-		String tname;
-		int backJumps;
-		boolean isCleared = false;
-		int loopStartPc;
-		int loopEndPc;
-		int loopStackDepth;
+  static class ThreadStat {
+    String tname;
 
-		ThreadStat(String tname) {
-			this.tname = tname;
-		}
-	}
+    int backJumps;
 
-	DynamicObjectArray threadStats = new DynamicObjectArray(16);
-	ThreadStat ts;
-	int maxBackJumps;
-	boolean jumpPast;
+    boolean isCleared = false;
 
-	//----------------------------------------------------- SearchListener interface
+    int loopStartPc;
 
-	public IdleFilter(Config config) {
-		maxBackJumps = config.getInt("idle.max_backjumps", 500);
-		jumpPast = config.getBoolean("idle.jump", false);
-	}
+    int loopEndPc;
 
-	public void stateAdvanced(Search search) {
-		ts.backJumps = 0;
-		ts.isCleared = false;
-		ts.loopStackDepth = 0;
-		ts.loopStartPc = ts.loopEndPc = 0;
-	}
+    int loopStackDepth;
 
-	public void stateBacktracked(Search search) {
-		ts.backJumps = 0;
-		ts.isCleared = false;
-		ts.loopStackDepth = 0;
-		ts.loopStartPc = ts.loopEndPc = 0;
-	}
+    ThreadStat(String tname) {
+      this.tname = tname;
+    }
+  }
 
-	//----------------------------------------------------- VMListener interface
-	public void instructionExecuted(VM vm) {
-		JVM jvm = (JVM) vm;
-		Instruction insn = jvm.getLastInstruction();
-		ThreadInfo ti = jvm.getLastThreadInfo();
+  DynamicObjectArray threadStats = new DynamicObjectArray(16);
 
-		int tid = ti.getIndex();
-		ts = (ThreadStat) threadStats.get(tid);
-		if (ts == null) {
-			ts = new ThreadStat(ti.getName());
-			threadStats.set(tid, ts);
-		}
+  ThreadStat ts;
 
-		if (insn.isBackJump()) {
-			ts.backJumps++;
+  int maxBackJumps;
 
-			int loopStackDepth = ti.countStackFrames();
-			int loopPc = jvm.getNextInstruction().getPosition();
+  boolean jumpPast;
 
-			if ((loopStackDepth != ts.loopStackDepth)
-					|| (loopPc != ts.loopStartPc)) {
-				// new loop, reset
-				ts.isCleared = false;
-				ts.loopStackDepth = loopStackDepth;
-				ts.loopStartPc = loopPc;
-				ts.loopEndPc = insn.getPosition();
-				ts.backJumps = 0;
-			} else {
-				if (!ts.isCleared) {
-					if (ts.backJumps > maxBackJumps) {
+  // ----------------------------------------------------- SearchListener
+  // interface
 
-						ti.yield(); // this breaks the executePorStep loop
-						MethodInfo mi = insn.getMethod();
-						ClassInfo ci = mi.getClassInfo();
-						int line = mi.getLineNumber(insn);
-						String file = ci.getSourceFileName();
+  public IdleFilter(Config config) {
+    maxBackJumps = config.getInt("idle.max_backjumps", 500);
+    jumpPast = config.getBoolean("idle.jump", false);
+  }
 
-						if (jumpPast) {
-							Instruction next = insn.getNext();
-							ti.setPC(next);
+  public void stateAdvanced(Search search) {
+    ts.backJumps = 0;
+    ts.isCleared = false;
+    ts.loopStackDepth = 0;
+    ts.loopStartPc = ts.loopEndPc = 0;
+  }
 
-							log
-									.warning("WARNING: IdleFilter jumped past loop in: "
-											+ ti.getName()
-											+ "\n\tat "
-											+ ci.getName()
-											+ "."
-											+ mi.getName()
-											+ "(" + file + ":" + line + ")");
-						} else {
-							// cut this sucker of - we declare this a visited state
-							jvm.setIgnoreState(true);
-							log.warning("WARNING: IdleFilter pruned thread: "
-									+ ti.getName() + "\n\tat " + ci.getName()
-									+ "." + mi.getName() + "(" + file + ":"
-									+ line + ")");
-						}
-					}
-				}
-			}
+  public void stateBacktracked(Search search) {
+    ts.backJumps = 0;
+    ts.isCleared = false;
+    ts.loopStackDepth = 0;
+    ts.loopStartPc = ts.loopEndPc = 0;
+  }
 
-		} else if (!ts.isCleared) {
-			// if we call methods or set array elements inside the loop in question, we
-			// assume this is not an idle loop and terminate the checks
-			if ((insn instanceof InvokeInstruction)
-					|| (insn instanceof ArrayStoreInstruction)) {
-				int stackDepth = ti.countStackFrames();
-				int pc = insn.getPosition();
+  // ----------------------------------------------------- VMListener interface
+  public void instructionExecuted(VM vm) {
+    JVM jvm = (JVM) vm;
+    Instruction insn = jvm.getLastInstruction();
+    ThreadInfo ti = jvm.getLastThreadInfo();
 
-				if (stackDepth == ts.loopStackDepth) {
-					if ((pc >= ts.loopStartPc) && (pc < ts.loopEndPc)) {
-						ts.isCleared = true;
-					}
-				}
-			}
-		}
-	}
+    int tid = ti.getIndex();
+    ts = (ThreadStat) threadStats.get(tid);
+    if (ts == null) {
+      ts = new ThreadStat(ti.getName());
+      threadStats.set(tid, ts);
+    }
+
+    if (insn.isBackJump()) {
+      ts.backJumps++;
+
+      int loopStackDepth = ti.countStackFrames();
+      int loopPc = jvm.getNextInstruction().getPosition();
+
+      if ((loopStackDepth != ts.loopStackDepth) || (loopPc != ts.loopStartPc)) {
+        // new loop, reset
+        ts.isCleared = false;
+        ts.loopStackDepth = loopStackDepth;
+        ts.loopStartPc = loopPc;
+        ts.loopEndPc = insn.getPosition();
+        ts.backJumps = 0;
+      } else {
+        if (!ts.isCleared) {
+          if (ts.backJumps > maxBackJumps) {
+
+            ti.yield(); // this breaks the executePorStep loop
+            MethodInfo mi = insn.getMethod();
+            ClassInfo ci = mi.getClassInfo();
+            int line = mi.getLineNumber(insn);
+            String file = ci.getSourceFileName();
+
+            if (jumpPast) {
+              // pretty bold, we jump past the loop end and go on from there
+              
+              Instruction next = insn.getNext();
+              ti.setPC(next);
+
+              log.warning("WARNING: IdleFilter jumped past loop in: "
+                  + ti.getName() + "\n\tat " + ci.getName() + "."
+                  + mi.getName() + "(" + file + ":" + line + ")");
+            } else {
+              // cut this sucker off - we declare this a visited state
+              jvm.setIgnoreState(true);
+              
+              log.warning("WARNING: IdleFilter pruned thread: " + ti.getName()
+                  + "\n\tat " + ci.getName() + "." + mi.getName() + "(" + file
+                  + ":" + line + ")");
+            }
+          }
+        }
+      }
+
+    } else if (!ts.isCleared) {
+      // if we call methods or set array elements inside the loop in question,
+      // we assume this is not an idle loop and terminate the checks
+      if ((insn instanceof InvokeInstruction)
+          || (insn instanceof ArrayStoreInstruction)) {
+        int stackDepth = ti.countStackFrames();
+        int pc = insn.getPosition();
+
+        if (stackDepth == ts.loopStackDepth) {
+          if ((pc >= ts.loopStartPc) && (pc < ts.loopEndPc)) {
+            ts.isCleared = true;
+          }
+        }
+      }
+    }
+  }
 
 }

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm/choice IntIntervalGenerator.java,1.1,1.2

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv12883/src/gov/nasa/jpf/jvm/choice

Modified Files:
	IntIntervalGenerator.java 
Log Message:
bad, bad back porter! half of the ChoiceGenerator interfacing was missing, the other half was wrong. Added some convenience array getters to Config, but those are not terribly efficient 

Index: IntIntervalGenerator.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/IntIntervalGenerator.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- IntIntervalGenerator.java	8 Sep 2005 23:21:04 -0000	1.1
+++ IntIntervalGenerator.java	9 Sep 2005 04:55:39 -0000	1.2
@@ -40,6 +40,12 @@
     throw new JPFException ("IntIntervalGenerator delta value is 0");
   }
   
+  if (min > max) {
+    int t = max;
+    max = min;
+    min = t;
+  }
+  
   if (delta > 0) {
     next = min - delta;
   } else {
@@ -76,9 +82,9 @@
 
 public boolean hasMoreChoices () {
   if (delta > 0) {
-    return (next <= max);
+    return (next < max);
   } else {
-    return (next >= min);
+    return (next > min);
   }
 }
 

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm SystemState.java,1.2,1.3 JVM.java,1.9,1.10 IntIntervalGenerator.java,1.1,NONE DoubleThresholdGenerator.java,1.1,NONE

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv12883/src/gov/nasa/jpf/jvm

Modified Files:
	SystemState.java JVM.java 
Removed Files:
	IntIntervalGenerator.java DoubleThresholdGenerator.java 
Log Message:
bad, bad back porter! half of the ChoiceGenerator interfacing was missing, the other half was wrong. Added some convenience array getters to Config, but those are not terribly efficient 

Index: JVM.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/JVM.java,v
retrieving revision 1.9
retrieving revision 1.10
diff -u -d -r1.9 -r1.10
--- JVM.java	8 Sep 2005 23:27:59 -0000	1.9
+++ JVM.java	9 Sep 2005 04:55:38 -0000	1.10
@@ -916,7 +916,6 @@
    */
   public boolean backtrack () {
     if (!backtrackStack.isEmpty()) {
-//System.out.println("@@@ HUHH??");
       // restore the KernelState
       backtrackKernelState();
       
@@ -995,7 +994,7 @@
       
       // execute the instruction(s) to get to the next state
       // this changes the SystemState (e.g. finds the next thread to run)
-      if (ss.nextSuccessor()) {
+      if (ss.nextSuccessor(this)) {
         // runs the garbage collector (if necessary), which might change the
         // KernelState (DynamicArea)
         // we need to do this before we hash the state to find out if it is
@@ -1024,7 +1023,6 @@
         
       } else { // state was completely explored, no transition ocurred
         popKernelState();
-//System.out.println("@@@ VM.forward bailed");
         return false;
       }
       

Index: SystemState.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/SystemState.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- SystemState.java	7 Sep 2005 22:08:20 -0000	1.2
+++ SystemState.java	9 Sep 2005 04:55:38 -0000	1.3
@@ -232,7 +232,7 @@
    * return 'true' if we actually executed instructions, 'false' if this
    * state was already completely processed
    */
-  public boolean nextSuccessor () throws JPFException {
+  public boolean nextSuccessor (JVM vm) throws JPFException {
     ThreadInfo th; // Thread that is going to be executed
     
     violatedAssertion = false;
@@ -241,6 +241,10 @@
     boring = false;
     th = (ThreadInfo) sch.locateThread(this);
 
+    if (gen != null) {
+      gen.advance(vm); // <2do> will replace the scheduler
+    }
+    
     if (ks.isIntermediate()) {
       int intermediateThread = ks.getIntermediateThread();
 
@@ -297,9 +301,7 @@
   }
 
   void prepareNext (JVM jvm) {
-    if (gen != null) {
-      gen.advance(jvm); // <2do> will replace the scheduler
-    }
+    gen = null;
     sch.initialize();
   }
 

--- DoubleThresholdGenerator.java DELETED ---

--- IntIntervalGenerator.java DELETED ---

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf Config.java,1.7,1.8

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv12883/src/gov/nasa/jpf

Modified Files:
	Config.java 
Log Message:
bad, bad back porter! half of the ChoiceGenerator interfacing was missing, the other half was wrong. Added some convenience array getters to Config, but those are not terribly efficient 

Index: Config.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/Config.java,v
retrieving revision 1.7
retrieving revision 1.8
diff -u -d -r1.7 -r1.8
--- Config.java	7 Sep 2005 22:08:20 -0000	1.7
+++ Config.java	9 Sep 2005 04:55:38 -0000	1.8
@@ -120,7 +120,9 @@
     this.fileName = fileName;
     gotProperties = loadFile(fileName, alternatePath, codeBase);
 
-    processArgs(args);
+    if (args != null){
+      processArgs(args);
+    }
     normalizeValues();
   }
 
@@ -370,6 +372,26 @@
     }
   }
 
+  public int[] getIntArray (String key) throws Exception {
+    String v = getProperty(key);
+    
+    if (v != null) {
+      String[] sa = v.split("[:;, ]+");
+      int[] a = new int[sa.length];
+      int i = 0;
+      try {
+        for (; i<sa.length; i++) {
+          a[i] = Integer.parseInt(sa[i]);
+        }
+        return a;
+      } catch (NumberFormatException nfx) {
+        throw new Exception("illegal int[] element in '" + key + "' = \"" + sa[i] + '"');
+      }
+    } else {
+      return null;
+    }
+  }
+
   public int getInt(String key) {
     return getInt(key, 0);
   }
@@ -404,6 +426,27 @@
     return defValue;
   }
 
+  public long[] getLongArray (String key) throws Exception {
+    String v = getProperty(key);
+    
+    if (v != null) {
+      String[] sa = v.split("[:;, ]+");
+      long[] a = new long[sa.length];
+      int i = 0;
+      try {
+        for (; i<sa.length; i++) {
+          a[i] = Long.parseLong(sa[i]);
+        }
+        return a;
+      } catch (NumberFormatException nfx) {
+        throw new Exception("illegal long[] element in " + key + " = " + sa[i]);
+      }
+    } else {
+      return null;
+    }
+  }
+
+  
   public double getDouble (String key) {
     return getDouble(key, 0.0);
   }
@@ -421,6 +464,26 @@
     return defValue;    
   }
 
+  public double[] getDoubleArray (String key) throws Exception {
+    String v = getProperty(key);
+    
+    if (v != null) {
+      String[] sa = v.split("[:;, ]+");
+      double[] a = new double[sa.length];
+      int i = 0;
+      try {
+        for (; i<sa.length; i++) {
+          a[i] = Double.parseDouble(sa[i]);
+        }
+        return a;
+      } catch (NumberFormatException nfx) {
+        throw new Exception("illegal double[] element in " + key + " = " + sa[i]);
+      }
+    } else {
+      return null;
+    }
+  }
+
   
   public String getString(String key) {
     return getProperty(key);

[Javapathfinder-devel] /javapathfinder/src/gov/nasa/jpf/jvm JVM.java,1.8,1.9

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv17227/src/gov/nasa/jpf/jvm

Modified Files:
	JVM.java 
Log Message:
* uncomment the stupid import


Index: JVM.java
===================================================================
RCS file: /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm/JVM.java,v
retrieving revision 1.8
retrieving revision 1.9
diff -u -d -r1.8 -r1.9
--- JVM.java	8 Sep 2005 23:27:16 -0000	1.8
+++ JVM.java	8 Sep 2005 23:27:59 -0000	1.9
@@ -48,7 +48,7 @@
 
 import gov.nasa.jpf.jvm.bytecode.FieldInstruction;
 import gov.nasa.jpf.jvm.bytecode.Instruction;
-//import gov.nasa.jpf.jvm.choice.IntIntervalGenerator;
+import gov.nasa.jpf.jvm.choice.IntIntervalGenerator;
 
 
 /**

[Javapathfinder-devel] /javapathfinder/src/gov/nasa/jpf/jvm JVM.java,1.7,1.8

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv17081/src/gov/nasa/jpf/jvm

Modified Files:
	JVM.java 
Log Message:
* added import with class move to jvm.choice

Index: JVM.java
===================================================================
RCS file: /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm/JVM.java,v
retrieving revision 1.7
retrieving revision 1.8
diff -u -d -r1.7 -r1.8
--- JVM.java	7 Sep 2005 22:08:20 -0000	1.7
+++ JVM.java	8 Sep 2005 23:27:16 -0000	1.8
@@ -48,6 +48,7 @@
 
 import gov.nasa.jpf.jvm.bytecode.FieldInstruction;
 import gov.nasa.jpf.jvm.bytecode.Instruction;
+//import gov.nasa.jpf.jvm.choice.IntIntervalGenerator;
 
 
 /**

[Javapathfinder-devel] /javapathfinder/src/gov/nasa/jpf/jvm ChoiceGenerator.java,1.1,1.2

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv16745/src/gov/nasa/jpf/jvm

Modified Files:
	ChoiceGenerator.java 
Log Message:
* make id visible to out of package subclasses (public)

Index: ChoiceGenerator.java
===================================================================
RCS file: /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm/ChoiceGenerator.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- ChoiceGenerator.java	7 Sep 2005 22:08:20 -0000	1.1
+++ ChoiceGenerator.java	8 Sep 2005 23:25:15 -0000	1.2
@@ -23,7 +23,8 @@
 */
 public abstract class ChoiceGenerator {
 
-String id;
+	// want the id to be visible to subclasses outside package
+public String id;
 int idRef;
 
 protected ChoiceGenerator (String id) {

[Javapathfinder-devel] /javapathfinder/src/gov/nasa/jpf/jvm JPF_gov_nasa_jpf_jvm_Verify.java,1.2,1.3

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv16625/src/gov/nasa/jpf/jvm

Modified Files:
	JPF_gov_nasa_jpf_jvm_Verify.java 
Log Message:
* need to qualify overloaded getInt calls (Peter's brain, John's fingers)

Index: JPF_gov_nasa_jpf_jvm_Verify.java
===================================================================
RCS file: /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- JPF_gov_nasa_jpf_jvm_Verify.java	7 Sep 2005 22:08:20 -0000	1.2
+++ JPF_gov_nasa_jpf_jvm_Verify.java	8 Sep 2005 23:24:31 -0000	1.3
@@ -162,7 +162,7 @@
     }    
   }
   
-  public static final int getInt (MJIEnv env, int clsObjRef, int min, int max) {
+  public static final int getInt__II (MJIEnv env, int clsObjRef, int min, int max) {
     JVM vm = env.getVM();
     
     ChoiceGenerator gen = vm.getChoiceGenerator();
@@ -177,7 +177,7 @@
     }    
   }
   
-  public static final double getInt (MJIEnv env, int clsObjRef, int idRef) {
+  public static final int getInt__Ljava_lang_String_2 (MJIEnv env, int clsObjRef, int idRef) {
     JVM vm = env.getVM();
     
     // there is only one per state, so if we have been here before, we don't

[Javapathfinder-devel] /javapathfinder/src/gov/nasa/jpf/jvm/choice TwoIntChoice.java,NONE,1.1 DoubleThresholdGenerator.java,NONE,1.1 IntIntervalGenerator.java,NONE,1.1 IntChoiceFromSet.java,NONE,1.1

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/jvm/choice
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv16022/src/gov/nasa/jpf/jvm/choice

Added Files:
	TwoIntChoice.java DoubleThresholdGenerator.java 
	IntIntervalGenerator.java IntChoiceFromSet.java 
Log Message:
* new package for choice generators
* moved in 2 classes from jvm
* 2 new choice generators hot off the press

--- NEW FILE: DoubleThresholdGenerator.java ---
//
//Copyright (C) 2005 United States Government as represented by the
//Administrator of the National Aeronautics and Space Administration
//(NASA).  All Rights Reserved.
//
//This software is distributed under the NASA Open Source Agreement
//(NOSA), version 1.3.  The NOSA has been approved by the Open Source
//Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
//directory tree for the complete NOSA document.
//
//THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
//KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
//LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
//SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
//A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
//THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
//DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
//

package gov.nasa.jpf.jvm.choice;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.jvm.DoubleChoiceGenerator;
import gov.nasa.jpf.jvm.JVM;

/**
* ChoiceGenerator instance that produces a simple 3 value enumeration
* 
*/
public class DoubleThresholdGenerator extends DoubleChoiceGenerator {

double low, threshold, high;
int state;

public DoubleThresholdGenerator (Config conf, String id) {
  super(id);
  
  low = conf.getDouble (id + ".low");
  threshold = conf.getDouble(id + ".threshold");
  high = conf.getDouble(id + ".high");
  state = -1;
}

public boolean hasMoreChoices () {
  return (state < 2);
}

public double getNextChoice () {
  switch (state) {
  case -1:
  case 0: return low;
  case 1: return threshold;
  default: return high;
  }
}

public void advance (JVM vm) {
  state++;
}
}

--- NEW FILE: IntChoiceFromSet.java ---
/*
 * Created on Sep 8, 2005
 *
 * TODO To change the template for this generated file go to
 * Window - Preferences - Java - Code Style - Code Templates
 */
package gov.nasa.jpf.jvm.choice;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.jvm.IntChoiceGenerator;
import gov.nasa.jpf.jvm.JVM;

/**
 * @author jpenix
 *
 * choose from a set of values provided in configuration as
 * xxx.class = IntChoiceFromSet
 * xxx.values = {1, 2, 3, 400}
 * where "xxx" is the choice id.
 * 
 * choices can then made using: getInt("xxx");
 */
public class IntChoiceFromSet extends IntChoiceGenerator {

	String[] values;
	int count = 0;
	
	/**
	 * @param id
	 */
	public IntChoiceFromSet(Config conf, String id) {
		super(id);
		values = conf.getStringArray("values");
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.IntChoiceGenerator#getNextChoice()
	 */
	public int getNextChoice() {
//		try {
			int ret = Integer.parseInt(values[count]);
			System.out.println(id + ": " + ret);
	        return ret;
//	      } catch (NumberFormatException nfx) {
//	        return 0;
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#hasMoreChoices()
	 */
	public boolean hasMoreChoices() {
		if (count < values.length)
			return true;
		else
			return false;
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#advance(gov.nasa.jpf.jvm.JVM)
	 */
	public void advance(JVM vm) {
		count++;
	}

}

--- NEW FILE: IntIntervalGenerator.java ---
//
//Copyright (C) 2005 United States Government as represented by the
//Administrator of the National Aeronautics and Space Administration
//(NASA).  All Rights Reserved.
//
//This software is distributed under the NASA Open Source Agreement
//(NOSA), version 1.3.  The NOSA has been approved by the Open Source
//Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
//directory tree for the complete NOSA document.
//
//THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
//KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
//LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
//SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
//A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
//THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
//DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
//package gov.nasa.jpf.jvm;
//
package gov.nasa.jpf.jvm.choice;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.JPFException;
import gov.nasa.jpf.jvm.IntChoiceGenerator;
import gov.nasa.jpf.jvm.JVM;


/**
* Choice Generator that enumerates an interval of int values
* Pretty simplistic implementation for now, but at least it can count up and down
*/
public class IntIntervalGenerator extends IntChoiceGenerator {

int min, max;
int next;
int delta;

private void init () {
  if (delta == 0) {
    throw new JPFException ("IntIntervalGenerator delta value is 0");
  }
  
  if (delta > 0) {
    next = min - delta;
  } else {
    next = max + delta;
  }
}

public IntIntervalGenerator (int min, int max, int delta) {
  super("int");
  
  this.min = min;
  this.max = max;
  this.delta = delta;
  
  init();    
}

public IntIntervalGenerator (int min, int max) {
  this(min, max, 1);
}
  
public IntIntervalGenerator (Config conf, String id) {
  super(id);
  min = conf.getInt( id + ".min");
  max = conf.getInt( id + ".max");
  delta = conf.getInt( id + ".delta", 1);

  init();
}

public int getNextChoice () {
  return next;
}

public boolean hasMoreChoices () {
  if (delta > 0) {
    return (next <= max);
  } else {
    return (next >= min);
  }
}

public void advance (JVM vm) {
  next += delta;
}
}

--- NEW FILE: TwoIntChoice.java ---
/*
 * Created on Sep 7, 2005
 *
 * TODO To change the template for this generated file go to
 * Window - Preferences - Java - Code Style - Code Templates
 */
package gov.nasa.jpf.jvm.choice;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.jvm.IntChoiceGenerator;
import gov.nasa.jpf.jvm.JVM;

/**
 * @author jpenix
 *
 * designed to choose return values from a function calls
 */
public class TwoIntChoice extends IntChoiceGenerator {

	int firstValue = 1;
	int secondValue = 0;

	String firstMsg = "pass";
	String secondMsg = "fail";
	
	int state = -1;
	
	public TwoIntChoice(Config conf, String id) {
		  super(id);
		  firstValue = conf.getInt( id + ".firstValue");
		  firstMsg = conf.getString( id + ".firstMessage");
		  secondValue = conf.getInt( id + ".secondValue");
		  secondMsg = conf.getString( id + ".secondMessage");
	}
	
	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.IntChoiceGenerator#getNextChoice()
	 */
	public int getNextChoice() {
		int ret;
		switch (state){
			case 0: {
				ret = firstValue;
				System.out.println(firstMsg);
				break;
			}
			case 1: {
				ret = secondValue;
				System.out.println(secondMsg);
			}
			default: { 
				ret = 99;
			}		
		}
		return ret;
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#hasMoreChoices()
	 */
	public boolean hasMoreChoices() {
		return state < 1;
	}

	/* (non-Javadoc)
	 * @see gov.nasa.jpf.jvm.ChoiceGenerator#advance(gov.nasa.jpf.jvm.JVM)
	 */
	public void advance(JVM vm) {
		state++;
	}

}

[Javapathfinder-devel] /javapathfinder/src/gov/nasa/jpf/tools StateSpaceDot.java,1.7,1.8

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/tools
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv2061/src/gov/nasa/jpf/tools

Modified Files:
	StateSpaceDot.java 
Log Message:
* i swear that compiled before...

Index: StateSpaceDot.java
===================================================================
RCS file: /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v
retrieving revision 1.7
retrieving revision 1.8
diff -u -d -r1.7 -r1.8
--- StateSpaceDot.java	6 Sep 2005 21:29:46 -0000	1.7
+++ StateSpaceDot.java	8 Sep 2005 18:28:12 -0000	1.8
@@ -515,7 +515,7 @@
     System.out.println("JPF State Space dot Graph Generator");
     listener.filterArgs(args);
 
-    System.out.println("...graph output to " + GRAPH_FILENAME + "...");
+    System.out.println("...graph output to " + listener.out_filename + "...");
 
     if (helpRequested==true) {
     	return;

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm BooleanChoiceGenerator.java,NONE,1.1 ChoiceGenerator.java,NONE,1.1 DoubleChoiceGenerator.java,NONE,1.1 DoubleThresholdGenerator.java,NONE,1.1 IntChoiceGenerator.java,NONE,1.1 IntIntervalGenerator.java,NONE,1.1 JPF_gov_nasa_jpf_jvm_Verify.java,1.1.1.1,1.2 JVM.java,1.6,1.7 SystemState.java,1.1.1.1,1.2 Verify.java,1.1.1.1,1.2

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv1579/src/gov/nasa/jpf/jvm

Modified Files:
	JPF_gov_nasa_jpf_jvm_Verify.java JVM.java SystemState.java 
	Verify.java 
Added Files:
	BooleanChoiceGenerator.java ChoiceGenerator.java 
	DoubleChoiceGenerator.java DoubleThresholdGenerator.java 
	IntChoiceGenerator.java IntIntervalGenerator.java 
Log Message:
this is NOT YET the big ChoceGenerator merge! But since we presented it at Spin, and we already use
it, this adds some data CGs (i.e. ThreadChoiceGenerators are not yet supported in this version).

Some things will get refactored (mostly the CG creation), but the CG interface itself will be
compatible, i.e. you can start to write some of them




--- NEW FILE: IntIntervalGenerator.java ---

--- NEW FILE: BooleanChoiceGenerator.java ---


--- NEW FILE: DoubleThresholdGenerator.java ---

--- NEW FILE: DoubleChoiceGenerator.java ---


--- NEW FILE: ChoiceGenerator.java ---

--- NEW FILE: IntChoiceGenerator.java ---

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf Config.java,1.6,1.7

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv1579/src/gov/nasa/jpf

Modified Files:
	Config.java 
Log Message:
this is NOT YET the big ChoceGenerator merge! But since we presented it at Spin, and we already use
it, this adds some data CGs (i.e. ThreadChoiceGenerators are not yet supported in this version).

Some things will get refactored (mostly the CG creation), but the CG interface itself will be
compatible, i.e. you can start to write some of them

[Javapathfinder-devel] javapathfinder jpf.properties,1.2,1.3

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv1579

Modified Files:
	jpf.properties 
Log Message:
this is NOT YET the big ChoceGenerator merge! But since we presented it at Spin, and we already use
it, this adds some data CGs (i.e. ThreadChoiceGenerators are not yet supported in this version).

Some things will get refactored (mostly the CG creation), but the CG interface itself will be
compatible, i.e. you can start to write some of them

[Javapathfinder-devel] /javapathfinder/src/gov/nasa/jpf/tools StateSpaceDot.java,1.6,1.7

[John P. <joh...@us...>]

Update of /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/tools
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv16432/src/gov/nasa/jpf/tools

Modified Files:
	StateSpaceDot.java 
Log Message:
* a few prints to let you know what is happening

Index: StateSpaceDot.java
===================================================================
RCS file: /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v
retrieving revision 1.6
retrieving revision 1.7
diff -u -d -r1.6 -r1.7
--- StateSpaceDot.java	12 Aug 2005 22:12:51 -0000	1.6
+++ StateSpaceDot.java	6 Sep 2005 21:29:46 -0000	1.7
@@ -511,7 +511,12 @@
   
   public static void main(String [] args) {
     StateSpaceDot listener = new StateSpaceDot();
+
+    System.out.println("JPF State Space dot Graph Generator");
     listener.filterArgs(args);
+
+    System.out.println("...graph output to " + GRAPH_FILENAME + "...");
+
     if (helpRequested==true) {
     	return;
     }
@@ -522,6 +527,7 @@
     JPF jpf = new JPF(conf);
     jpf.addSearchListener(listener);
 
+    System.out.println("...running JPF...");
     jpf.run();
   }
 }