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

[Javapathfinder-devel] javapathfinder/bin jpf,1.5,1.6 jpf-dot,1.3,1.4 jpf-dot.bat,1.1.1.1,1.2 jpf.bat,1.1.1.1,1.2

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

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

Modified Files:
	jpf jpf-dot jpf-dot.bat jpf.bat 
Log Message:
* some more script fixes (*.bat) NOT tested yet

* improvised check for unknown '-' options prior to starting the VM. NOTE - this
requires all known options to be consumed (nullified) before this is done, so the
check should be the very last thing before the Search is set off



Index: jpf-dot.bat
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/bin/jpf-dot.bat,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- jpf-dot.bat	26 Apr 2005 19:43:03 -0000	1.1.1.1
+++ jpf-dot.bat	11 May 2005 18:05:34 -0000	1.2
@@ -1,3 +1,7 @@
+REM
+REM overly simplified batch file to start JPF from a command prompt
+REM
+
 @echo off
 
 REM Set the JPF_HOME directory
@@ -14,15 +18,16 @@
 set CP=%CP%;%JPF_HOME%\build\test
 
 REM Otherwise, we look for the jar (binary distributions)
-set CP=%CP%;%JPF_HOME%\lib\jpf.jar
+set %CP%;%JPF_HOME%\lib\jpf.jar
 
 REM And these are the external libs we use at runtime
-set CP=%CP%;%JPF_HOME%\lib\xercesImpl.jar
-set CP=%CP%;%JPF_HOME%\lib\xmlParserAPIs.jar
+REM (include the CLASSPATH first, in case somebody wants to use specific versions)
+set CP=%CP%;%CLASSPATH%
+
 set CP=%CP%;%JPF_HOME%\lib\bcel.jar
-set CP=%CP%;%JPF_HOME%\lib\md5-twmacinta.jar
-set CP=%CP%;%JPF_HOME%\lib\edu.jar
-set CP=%CP%;%JPF_HOME%\lib\scale.jar
+set CP=%CP%;%JPF_HOME%\lib\fast-MD5.jar
+set CP=%CP%;%JPF_HOME%\lib\xercesImpl.jar
+set CP=%CP%;%JPF_HOME%\lib\xml-apis.jar
 
 REM our standard native peer environment
 REM * For our source distribution.
@@ -35,13 +40,10 @@
 set CP=%CP%;%JPF_HOME%\examples
 set CP=%CP%;%JPF_HOME%\build\examples
 
-REM JPF boot class path
-set BCP=%JPF_HOME%\build\env\jpf;%JPF_HOME%\lib\env_jpf.jar
-
-REM JVM flags
 set JVM_FLAGS=-Xmx1536m
 
+
 REM StateSpaceDot tool options
 set SSDO=-show-source -transition-numbers
 
-java %JVM_FLAGS% -classpath "%CP%" gov.nasa.jpf.tools.StateSpaceDot %SSDO% -jpf-bootclasspath "%BCP%" %1 %2 %3 %4 %5 %6 %7 %8 %9
+java %JVM_FLAGS% -classpath "%CP%" gov.nasa.jpf.tools.StateSpaceDot %SSDO% %1 %2 %3 %4 %5 %6 %7 %8 %9

Index: jpf.bat
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/bin/jpf.bat,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- jpf.bat	26 Apr 2005 19:43:03 -0000	1.1.1.1
+++ jpf.bat	11 May 2005 18:05:34 -0000	1.2
@@ -1,3 +1,7 @@
+REM
+REM overly simplified batch file to start JPF from a command prompt
+REM
+
 @echo off
 
 REM Set the JPF_HOME directory
@@ -14,15 +18,16 @@
 set CP=%CP%;%JPF_HOME%\build\test
 
 REM Otherwise, we look for the jar (binary distributions)
-set CP=%CP%;%JPF_HOME%\lib\jpf.jar
+set %CP%;%JPF_HOME%\lib\jpf.jar
 
 REM And these are the external libs we use at runtime
-set CP=%CP%;%JPF_HOME%\lib\xercesImpl.jar
-set CP=%CP%;%JPF_HOME%\lib\xmlParserAPIs.jar
+REM (include the CLASSPATH first, in case somebody wants to use specific versions)
+set CP=%CP%;%CLASSPATH%
+
 set CP=%CP%;%JPF_HOME%\lib\bcel.jar
-set CP=%CP%;%JPF_HOME%\lib\md5-twmacinta.jar
-set CP=%CP%;%JPF_HOME%\lib\edu.jar
-set CP=%CP%;%JPF_HOME%\lib\scale.jar
+set CP=%CP%;%JPF_HOME%\lib\fast-MD5.jar
+set CP=%CP%;%JPF_HOME%\lib\xercesImpl.jar
+set CP=%CP%;%JPF_HOME%\lib\xml-apis.jar
 
 REM our standard native peer environment
 REM * For our source distribution.
@@ -35,8 +40,6 @@
 set CP=%CP%;%JPF_HOME%\examples
 set CP=%CP%;%JPF_HOME%\build\examples
 
-set BCP=%JPF_HOME%\build\env\jpf;%JPF_HOME%\lib\env_jpf.jar
-
 set JVM_FLAGS=-Xmx1536m
 
-java %JVM_FLAGS% -classpath "%CP%" gov.nasa.jpf.JPF -jpf-bootclasspath "%BCP%" %1 %2 %3 %4 %5 %6 %7 %8 %9
+java %JVM_FLAGS% -classpath "%CP%" gov.nasa.jpf.JPF %1 %2 %3 %4 %5 %6 %7 %8 %9

Index: jpf-dot
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/bin/jpf-dot,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- jpf-dot	11 May 2005 01:18:06 -0000	1.3
+++ jpf-dot	11 May 2005 18:05:34 -0000	1.4
@@ -63,4 +63,4 @@
   SSDOT_FLAGS="-show-source -transition-numbers"
 fi
 
-java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.tools.StateSpaceDot "$SSDOT_FLAGS" $@
+java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.tools.StateSpaceDot $SSDOT_FLAGS $@

Index: jpf
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/bin/jpf,v
retrieving revision 1.5
retrieving revision 1.6
diff -u -d -r1.5 -r1.6
--- jpf	11 May 2005 01:18:06 -0000	1.5
+++ jpf	11 May 2005 18:05:34 -0000	1.6
@@ -55,5 +55,4 @@
   JVM_FLAGS="-Xmx1024m"
 fi
 
-java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.JPF  "$@"
-
+java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.JPF $@

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf JPF.java,1.1.1.1,1.2

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

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

Modified Files:
	JPF.java 
Log Message:
* some more script fixes (*.bat) NOT tested yet

* improvised check for unknown '-' options prior to starting the VM. NOTE - this
requires all known options to be consumed (nullified) before this is done, so the
check should be the very last thing before the Search is set off



Index: JPF.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/JPF.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- JPF.java	26 Apr 2005 19:43:55 -0000	1.1.1.1
+++ JPF.java	11 May 2005 18:05:34 -0000	1.2
@@ -170,10 +170,30 @@
     return false;
   }
     
+  /**
+   * this assumes that we have checked and 'consumed' (nullified) all known
+   * options, so we just have to check for any '-' option prior to the
+   * target class name
+   */
+  static void checkUnknownArgs (String[] args) {
+    for ( int i=0; i<args.length; i++) {
+      if (args[i] != null) {
+        if (args[i].charAt(0) == '-') {
+          Debug.println(Debug.ERROR, "! Warning - unknown command line option: " + args[i]);
+        } 
+        else {
+          // this is supposed to be the target class name - everything that follows
+          // is supposed to be processed by the program under test
+          break;
+        }
+      }
+    }
+  }
+  
   public static void printBanner (Config config) {
     System.out.print("Java Pathfinder Model Checker v");
     System.out.print(config.getString("jpf.version", "3.1x"));
-    System.out.println(" - (C) 1999-2004 RIACS/NASA Ames Research Center");
+    System.out.println(" - (C) 1999-2005 RIACS/NASA Ames Research Center");
   }
   
   public static void main(String[] args) {
@@ -194,6 +214,8 @@
     }
     
     if (conf.getTargetArg() != null) {
+      checkUnknownArgs(args);
+      
       JPF jpf =  new JPF(conf);
       jpf.run();
     }
@@ -273,26 +295,6 @@
     return null;
   }
   
-  /**
-   * Do whatever has to be done with the options before we create the JPF
-   * object, esp. banner or usage printing. Return 'false' if there is no need
-   * for further processing
-   */
-  boolean processOptions() {
-  	
-    if (config.hasArg("-d(ump(-config)?)?")) {
-      config.printContents(new PrintWriter(System.out));
-    }
-
-    if ((config.getArgs() == null) || config.hasArg("-h(elp)?")) {
-    		showUsage();
-    		return false;
-    }
-    
-    // do we have an application or path file specifier
-    return config.hasArg("[~-][a-zA-Z0-9_]*");
-  }
-
   static void showUsage() {
     System.out
         .println("Usage: \"java [<vm-option>..] gov.nasa.jpf.JPF [<jpf-option>..] [<app> [<app-arg>..]]");

[Javapathfinder-devel] CVSROOT commitlog,1.3,1.4

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

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

Added Files:
	commitlog 
Log Message:
again, added commitlog

--- NEW FILE: commitlog ---
------------------ start commit log 05/12/2005 -------------------

[Javapathfinder-devel] javapathfinder/bin jpf,1.4,1.5 jpf-dot,1.2,1.3

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

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

Modified Files:
	jpf jpf-dot 
Log Message:
double checked for dos or Mac line-endings

[Javapathfinder-devel] javapathfinder/bin jpf-dot,1.1.1.1,1.2

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

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

Modified Files:
	jpf-dot 
Log Message:
updated jpf-dot script

Index: jpf-dot
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/bin/jpf-dot,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- jpf-dot	26 Apr 2005 19:43:03 -0000	1.1.1.1
+++ jpf-dot	11 May 2005 01:10:42 -0000	1.2
@@ -13,52 +13,54 @@
 #if we have class files, we probably want to use those first
 CP=$JPF_HOME/build/jpf
 CP=$CP:$JPF_HOME/build/test
-#otherwise, we look for the jar (binary distributions)
-CP=$CP:$JPF_HOME/lib/jpf.jar
-
-#those are the external libs we use at runtime
-CP=$CP:$JPF_HOME/lib/bcel.jar
-CP=$CP:$JPF_HOME/lib/md5-twmacinta.jar
-CP=$CP:$JPF_HOME/lib/edu.jar
-CP=$CP:$JPF_HOME/lib/scale.jar
-CP=$CP:$JPF_HOME/lib/xercesImpl.jar:$JPF_HOME/lib/xmlParserAPIs.jar
-
-#our standard native peer environment
-# * For our source distribution.
-CP=$CP:$JPF_HOME/build/env/jvm
 
-# * For our binary dirtribution
-CP=$CP:$JPF_HOME/lib/env_jvm.jar
+#add (recursively) any *.jar or *.zip that's under $JPF_HOME/lib
+#note that those take precedence over what already is in the classpath
+if test -d "$JPF_HOME/lib"; then
+  CP=$CP:`find "$JPF_HOME"/lib \( -name "*.jar" -or -name "*.zip" \) -exec echo -n {}":" \;`
+fi
 
-# * For C runtime environment (source distribution)
-CP=$CP:$JPF_HOME/build/env/c-runtime
+if test -d "$JPF_HOME/extensions"; then
+  CP=$CP:`find "$JPF_HOME"/extensions \( -name "*.jar" -or -name "*.zip" \) -exec echo -n {}":" \;`
+fi
 
-# * For c_runtime environment
-CP=$CP:$JPF_HOME/build/lib/env_c_runtime.jar
+#our standard native peer environment (just the peer, NOT the model classes)
+CP=$CP:$JPF_HOME/build/env/jvm
 
 #Examples
-CP=$CP:$JPF_HOME/examples
 CP=$CP:$JPF_HOME/build/examples
 
-#add the global CLASSPATH
-
+#append the global CLASSPATH
 if $_cygwin; then
   CP=`cygpath --path --windows "$CP"`
+  JAVA_HOME=`cygpath --path --windows "$JAVA_HOME"`
   CLASSPATH=`cygpath --path --windows "$CLASSPATH"`
   CP="$CP;$CLASSPATH"
-  JAVA_HOME=`cygpath --path --windows "$JAVA_HOME"`
 else
   CP="$CP:$CLASSPATH"
 fi
 
-BCP=$JPF_HOME/build/env/jpf:$JPF_HOME/lib/env_jpf.jar
-if $_cygwin; then
-  BCP=`cygpath --path --windows "$BCP"`
+#now check if we find our mandatory jars
+if test ! `expr "$CP" : ".*\(bcel[^\.]*\.jar\).*"`; then
+  echo "*** you don't seem to have bcel.jar in your CLASSPATH, please fix ***"
+  exit
+fi
+if test ! `expr "$CP" : ".*\(xercesImpl\.jar\).*"`; then
+  echo "*** you don't seem to have the Xerces libs in your CLASSPATH, please fix ***"
+  exit
 fi
+#no good way to check for the MD5 since it could be a zip, a jar, or just a path
 
-# StateSpaceDot tool options
-SSDO="-show-source -transition-numbers"
+if test -z $JVM_FLAGS; then
+  JVM_FLAGS="-Xmx1024m"
+fi
 
-JVM_FLAGS="-Xmx1024m"
+java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.JPF  "$@"
 
-java $JVM_FLAGS -classpath "$CP" $JPF_JVM_FLAGS gov.nasa.jpf.tools.StateSpaceDot $SSDO -jpf-bootclasspath "$BCP" $@
+
+# StateSpaceDot tool options
+if test -z $SSDOT_FLAGS; then
+  SSDOT_FLAGS="-show-source -transition-numbers"
+fi
+
+java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.tools.StateSpaceDot "$SSDOT_FLAGS" $@

[Javapathfinder-devel] CVSROOT commitlog,1.2,NONE

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

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

Removed Files:
	commitlog 
Log Message:
fixing commitlog permissions

--- commitlog DELETED ---

[Javapathfinder-devel] CVSROOT commitlog,1.1,1.2

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

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

Modified Files:
	commitlog 
Log Message:
commitlog permissions

[Javapathfinder-devel] javapathfinder/bin jpf,1.3,1.4

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

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

Modified Files:
	jpf 
Log Message:
Masouds cygwin script fixes

Index: jpf
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/bin/jpf,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- jpf	1 May 2005 04:09:21 -0000	1.3
+++ jpf	10 May 2005 23:20:37 -0000	1.4
@@ -16,12 +16,12 @@
 
 #add (recursively) any *.jar or *.zip that's under $JPF_HOME/lib
 #note that those take precedence over what already is in the classpath
-if test -d $JPF_HOME/lib; then
-  CP=$CP:`find $JPF_HOME/lib \( -name "*.jar" -or -name "*.zip" \) -exec echo -n {}":" \;`
+if test -d "$JPF_HOME/lib"; then
+  CP=$CP:`find "$JPF_HOME"/lib \( -name "*.jar" -or -name "*.zip" \) -exec echo -n {}":" \;`
 fi
 
-if test -d $JPF_HOME/extensions; then
-  CP=$CP:`find $JPF_HOME/extensions \( -name "*.jar" -or -name "*.zip" \) -exec echo -n {}":" \;`
+if test -d "$JPF_HOME/extensions"; then
+  CP=$CP:`find "$JPF_HOME"/extensions \( -name "*.jar" -or -name "*.zip" \) -exec echo -n {}":" \;`
 fi
 
 #our standard native peer environment (just the peer, NOT the model classes)
@@ -41,19 +41,19 @@
 fi
 
 #now check if we find our mandatory jars
-if test ! `expr $CP : ".*\(bcel.*\.jar\).*"`; then
+if test ! `expr "$CP" : ".*\(bcel[^\.]*\.jar\).*"`; then
   echo "*** you don't seem to have bcel.jar in your CLASSPATH, please fix ***"
   exit
 fi
-if test ! `expr $CP : ".*\(xercesImpl\.jar\).*"`; then
+if test ! `expr "$CP" : ".*\(xercesImpl\.jar\).*"`; then
   echo "*** you don't seem to have the Xerces libs in your CLASSPATH, please fix ***"
   exit
 fi
 #no good way to check for the MD5 since it could be a zip, a jar, or just a path
 
-
 if test -z $JVM_FLAGS; then
   JVM_FLAGS="-Xmx1024m"
 fi
 
 java $JVM_FLAGS -classpath "$CP" gov.nasa.jpf.JPF  "$@"
+

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

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

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

Modified Files:
	ThreadInfo.java 
Log Message:
moved the idle loop detection out of the core and into gov.nasa.jpf.tools.IdleFilter listener, which
is also a bit more sophisticated. It checks not just for back jump threshold, but abandons the test if it
detects ArrayStoreInstructions or InvokeInstructions, assuming both are doing stuff that shouldn't be
ignored. The thing can be made vastly more sophisticated, but it nicely shows what can be done
with listeners. It passes the

  int[] a = new int[500]; // init loop  -> pass
  for (int i=0; i<a.length; i++) a[i] = i; 

   for (long l=0; l<1000000; l++); // bad idle loop  -> filter

test. To ease creation of listeners like this, I've also added a ListenerAdapter, which dummy implements
both VMListener and SearchListener, so that tools only have to override their relevant notificatiion
methods

Index: ThreadInfo.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ThreadInfo.java,v
retrieving revision 1.8
retrieving revision 1.9
diff -u -d -r1.8 -r1.9
--- ThreadInfo.java	7 May 2005 00:40:01 -0000	1.8
+++ ThreadInfo.java	10 May 2005 06:46:55 -0000	1.9
@@ -152,9 +152,6 @@
    */
   LinkedList lockedObjects = new LinkedList();
   
-  /** number of consecutive POR breaks this thread had since the last backtrack
-   */
-  int forcedPorBreaks;
   
   // the following parameters are configurable. Would be nice if we could keep
   // them on a per-instance basis, but there are a few locations
@@ -180,12 +177,7 @@
    * we don't treat access of the corresponding field as a boundary step 
    */
   static boolean porSyncDetection;
-  
-  /** after how many back jumps (potential loop closing GOTOs) do we get suspicious
-   * that we are in an endless loop that would never return from executePorStep
-   */
-  static int porMaxBackJumps;
-  
+    
   static boolean init (Config config) {
     threadDataPool = new HashPool();
     stackFramePool = new HashPool();
@@ -195,7 +187,6 @@
     porInEffect = config.getBoolean("vm.por");
     porFieldBoundaries = config.getBoolean("vm.por.field_boundaries");
     porSyncDetection = config.getBoolean("vm.por.sync_detection");
-    porMaxBackJumps = config.getInt("vm.por.max_backjumps", 50);
     
     return true;
   }
@@ -1222,8 +1213,6 @@
     hasChanged = new BitSet();
     lowestChanged = -1;
     
-    forcedPorBreaks = 0;
-    
     this.data = data;
   }
   
@@ -2088,8 +2077,6 @@
    */
   protected boolean executePorStep () throws JPFException {
         
-    int backJumps =0;
-    
     while (true) {      
       Instruction pc = executeInstruction();
             
@@ -2137,16 +2124,7 @@
       if ( yield || pc.isSchedulingRelevant(list.ks.ss, list.ks, this)) {
         yield = false;
         break;
-      }
-      
-      if (pc.isBackJump()) {
-        if (backJumps++ > porMaxBackJumps) {
-          if (forcedPorBreaks++ > 1) {
-            vm.setIgnoreState(true);
-          }
-          break; // we break before the jump backwards
-        }
-      }
+      }      
     }
     
     return true;

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

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

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

Added Files:
	IdleFilter.java 
Log Message:
moved the idle loop detection out of the core and into gov.nasa.jpf.tools.IdleFilter listener, which
is also a bit more sophisticated. It checks not just for back jump threshold, but abandons the test if it
detects ArrayStoreInstructions or InvokeInstructions, assuming both are doing stuff that shouldn't be
ignored. The thing can be made vastly more sophisticated, but it nicely shows what can be done
with listeners. It passes the

  int[] a = new int[500]; // init loop  -> pass
  for (int i=0; i<a.length; i++) a[i] = i; 

   for (long l=0; l<1000000; l++); // bad idle loop  -> filter

test. To ease creation of listeners like this, I've also added a ListenerAdapter, which dummy implements
both VMListener and SearchListener, so that tools only have to override their relevant notificatiion
methods

--- NEW FILE: IdleFilter.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.tools;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.Search;
import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.VM;
import gov.nasa.jpf.jvm.JVM;
import gov.nasa.jpf.jvm.ThreadInfo;
import gov.nasa.jpf.jvm.bytecode.ArrayStoreInstruction;
import gov.nasa.jpf.jvm.bytecode.Instruction;
import gov.nasa.jpf.jvm.bytecode.InvokeInstruction;

import java.util.HashMap;

/**
 * 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++);
 * 
 * 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
 */
public class IdleFilter extends ListenerAdapter {
    
  static class ThreadStat {
    String tname;
    int strikes;
    int backJumps;
    boolean isCleared = false;
    
    ThreadStat (String tname) {
      this.tname = tname;
    }
  }
  
  HashMap threadStats = new HashMap();
  
  ThreadStat ts;
  
  int maxStrikes;
  int maxBackJumps;
  
  //----------------------------------------------------- SearchListener interface

  public IdleFilter (Config config) {
    maxBackJumps = config.getInt("idle.max_backjumps", 500);
    maxStrikes = config.getInt("idle.max_strikes", 1);
  }
  
  public void stateAdvanced(Search search) {
    ts.backJumps = 0;
    ts.isCleared = false;
  }

  public void stateBacktracked(Search search) {
    ts.strikes = 0;
    ts.backJumps = 0;
    ts.isCleared = false;
  }
  
  //----------------------------------------------------- VMListener interface
  public void instructionExecuted(VM vm) {
    JVM jvm = (JVM)vm;
    Instruction insn = jvm.getLastInstruction();
    ThreadInfo ti = jvm.getLastThreadInfo();

    String tid = ti.getName(); // not ideal, but still better than boxing int's
    ts = (ThreadStat)threadStats.get(tid);
    if (ts == null) {
      ts = new ThreadStat(tid);
      threadStats.put(tid, ts);
    }
    
    if (insn.isBackJump() && !ts.isCleared ) {
      ts.backJumps++;
      
      if (ts.backJumps > maxBackJumps) {
        ti.yield();
        ts.strikes++;
        
        if (ts.strikes > maxStrikes) {
          // cut this sucker of - we declare this a visited state
          // <2do> - we should probably issue a warning message here
          jvm.setIgnoreState(true);
        }
      }
    } else if (insn instanceof InvokeInstruction) {
      ts.isCleared=true; // shut it off for this forward
    } else if (insn instanceof ArrayStoreInstruction) {
      ts.isCleared=true;
    }
  }
  
}

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

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

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

Added Files:
	ListenerAdapter.java 
Log Message:
moved the idle loop detection out of the core and into gov.nasa.jpf.tools.IdleFilter listener, which
is also a bit more sophisticated. It checks not just for back jump threshold, but abandons the test if it
detects ArrayStoreInstructions or InvokeInstructions, assuming both are doing stuff that shouldn't be
ignored. The thing can be made vastly more sophisticated, but it nicely shows what can be done
with listeners. It passes the

  int[] a = new int[500]; // init loop  -> pass
  for (int i=0; i<a.length; i++) a[i] = i; 

   for (long l=0; l<1000000; l++); // bad idle loop  -> filter

test. To ease creation of listeners like this, I've also added a ListenerAdapter, which dummy implements
both VMListener and SearchListener, so that tools only have to override their relevant notificatiion
methods

--- NEW FILE: ListenerAdapter.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;


/**
 * Adapter class that dummy implements both VMListener and SearchListener interfaces
 * Used to ease implementation of listeners that only process few notifications
 */
public class ListenerAdapter implements VMListener, SearchListener {

  /* (non-Javadoc)
   * @see gov.nasa.jpf.VMListener#instructionExecuted(gov.nasa.jpf.VM)
   */
  public void instructionExecuted(VM vm) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.VMListener#threadStarted(gov.nasa.jpf.VM)
   */
  public void threadStarted(VM vm) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.VMListener#threadTerminated(gov.nasa.jpf.VM)
   */
  public void threadTerminated(VM vm) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.VMListener#classLoaded(gov.nasa.jpf.VM)
   */
  public void classLoaded(VM vm) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.VMListener#objectCreated(gov.nasa.jpf.VM)
   */
  public void objectCreated(VM vm) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.VMListener#objectReleased(gov.nasa.jpf.VM)
   */
  public void objectReleased(VM vm) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.VMListener#gcBegin(gov.nasa.jpf.VM)
   */
  public void gcBegin(VM vm) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.VMListener#gcEnd(gov.nasa.jpf.VM)
   */
  public void gcEnd(VM vm) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.VMListener#exceptionThrown(gov.nasa.jpf.VM)
   */
  public void exceptionThrown(VM vm) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.SearchListener#stateAdvanced(gov.nasa.jpf.Search)
   */
  public void stateAdvanced(Search search) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.SearchListener#stateProcessed(gov.nasa.jpf.Search)
   */
  public void stateProcessed(Search search) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.SearchListener#stateBacktracked(gov.nasa.jpf.Search)
   */
  public void stateBacktracked(Search search) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.SearchListener#stateRestored(gov.nasa.jpf.Search)
   */
  public void stateRestored(Search search) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.SearchListener#propertyViolated(gov.nasa.jpf.Search)
   */
  public void propertyViolated(Search search) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.SearchListener#searchStarted(gov.nasa.jpf.Search)
   */
  public void searchStarted(Search search) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.SearchListener#searchConstraintHit(gov.nasa.jpf.Search)
   */
  public void searchConstraintHit(Search search) {
  }

  /* (non-Javadoc)
   * @see gov.nasa.jpf.SearchListener#searchFinished(gov.nasa.jpf.Search)
   */
  public void searchFinished(Search search) {
  }

}

[Javapathfinder-devel] CVSROOT checkoutlist,1.2,1.3

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

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

Modified Files:
	checkoutlist 
Log Message:
and while we are at it, the commitlog, too

Index: checkoutlist
===================================================================
RCS file: /cvsroot/javapathfinder/CVSROOT/checkoutlist,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- checkoutlist	7 May 2005 01:09:37 -0000	1.2
+++ checkoutlist	7 May 2005 01:12:35 -0000	1.3
@@ -12,3 +12,4 @@
 #
 # comment lines begin with '#'
 syncmail
+commitlog

[Javapathfinder-devel] CVSROOT syncmail,1.2,1.3

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

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

Modified Files:
	syncmail 
Log Message:
syncmail, again

Index: syncmail
===================================================================
RCS file: /cvsroot/javapathfinder/CVSROOT/syncmail,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- syncmail	7 May 2005 00:25:25 -0000	1.2
+++ syncmail	7 May 2005 01:10:22 -0000	1.3
@@ -1,5 +1,4 @@
 #! /usr/bin/python
-#  -*- Python -*-
 
 # Copyright (c) 2002, 2003, 2004 Barry Warsaw, Fred Drake, and contributors
 # All rights reserved.

Re: [Javapathfinder-devel] Re: infinite POR loop

[Peter C. M. <pcm...@em...>]

> But after one step it will see it has been in the state before and
> backtrack and try the other threads???

why? It will only match if the stacks are the same, but they aren't 
(locals are changing, pc is different). We could work around the pc by 
only breaking on, say GOTOs, but I don't see a solution for the locals 
issue

-- Peter

RE: [Javapathfinder-devel] Re: infinite POR loop

[Willem V. <wv...@em...>]

> That was my original thinking too, but no. The forward succeeds (it
> executed something), the state is new (changed the stack), so DFSearch
> happily goes one step down and restarts to search with thread 0. It's
> almost like we want to switch to BFS for one depth. So there's three
> solutions I could see:

But after one step it will see it has been in the state before and
backtrack and try the other threads???

--
Willem C. Visser                 Automated Software Engineering Group
RIACS/NASA Ames Research Center            wv...@em...
M/S 269-2                                     http://ase.arc.nasa.gov
Moffett Field, CA 94035                (650)604-3515 fax 4036  rm 235


> -----Original Message-----
> From: jav...@li...
> [mailto:jav...@li...] On Behalf Of
> Peter C.Mehlitz
> Sent: Friday, May 06, 2005 10:14 AM
> To: Jav...@li...
> Subject: [Javapathfinder-devel] Re: infinite POR loop
> 
> [..we should move all these discussions to the mailing list..]
> 
> That was my original thinking too, but no. The forward succeeds (it
> executed something), the state is new (changed the stack), so DFSearch
> happily goes one step down and restarts to search with thread 0. It's
> almost like we want to switch to BFS for one depth. So there's three
> solutions I could see:
> 
> (1) request a backtrack after breaking the por loop, to force the
> scheduler to advance past the suspicious thread at the same search
> level
> 
> (2) just 'blank out' the suspicious thread from the next forward
> scheduling sequence (i.e. skip it for the next search depth)
> 
> (3) re-order threads
> 
> While (1) seems to be less disruptive, there is of course a pretty
> hefty 'optimization' issue. If the thread doesn't recover (which is
> very likely), it will henceforth always cause one additional backtrack
> per search depth. I think it basically kills DFSearch at this point.
> Wonder what effects re-ordering would have on
> state-storage/backtracking, though. Don't know about (2) yet, either
> 
> the case is pretty easy to get:
> 
> public class Starve implements Runnable {
>       public void run () {
>            throw new RuntimeException("blow it up");
>       }
> 
>       public static void main (String[] args) {
>            Starve o = new Starve();
>            Thread t = new Thread(o);
>            t.start();
> 
>            int sum=0;
>            while (true) { // starve t
>                 sum++;
>            }
>       }
> }
> 
> -- Peter
> 
> On May 5, 2005, at 9:18 PM, Willem Visser wrote:
> 
> > Changing the thread order does seem extreme, but I'll think if there
> > is a
> > reason not to do that.
> >
> > Of course you could also just break the loop and forget about it, if
> > there
> > is something interesting in the rest of the system it will come out
-
> > pushing the "dead-thread" to the end would be an optimization.
> >
> > The thing here is that this issue should seldom come up, in fact if
it
> > comes
> > up in a "real" program then frankly it is a bug - you obviously
didn't
> > want
> > a non-progressing, non-interacting cycle in your code. The only
> > scenario
> > this could legitimately happen is when you abstract a program - but
we
> > don't
> > do these kind of abstractions (we do the abstract state storing
> > variety).
> >
> > Others that have dealt with this kind of issue either punt by
stating
> > these
> > idle-loops are not allowed, or they use some clever loop breaking
via
> > back-edges etc.
> >
> > ----- Original Message -----
> > From: "Peter C. Mehlitz" <pcm...@em...>
> > To: "Willem Visser" <wv...@em...>; "John Penix"
> > <Joh...@na...>
> > Sent: Thursday, May 05, 2005 8:10 PM
> > Subject: infinite POR loop
> >
> >
> >> that's of course a bit more interesting - what we need in addition
to
> >> a
> >> trivial loop breaker is some sort of a Thread.yield, i.e. if we
have a
> >> suspicious thread that seems to bore us to death with idling, we
have
> >> to make sure we change the scheduling order, so that this sucker
> >> henceforth always gets explored last. Should be simple enough by
> >> pushing it to the end of the ThreadList when resetting the
scheduler
> >> (which is effectively an index re-order in
SystemState.prepareNext()),
> >> but I'm a bit uncertain what re-ordering does to us. I think, so
far
> >> thread indexes were invariant.
> >>
> >> Any insights, thoughts, suggestions?
> >>
> >> -- Peter
> >>
> >
> 
> 
> 
> -------------------------------------------------------
> This SF.Net email is sponsored by: NEC IT Guy Games.
> Get your fingers limbered up and give it your best shot. 4 great
events, 4
> opportunities to win big! Highest score wins.NEC IT Guy Games. Play to
> win an NEC 61 plasma display. Visit http://www.necitguy.com/?r=20
> _______________________________________________
> Javapathfinder-devel mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel

[Javapathfinder-devel] Re: infinite POR loop

[Peter C. M. <pcm...@em...>]

[..we should move all these discussions to the mailing list..]

That was my original thinking too, but no. The forward succeeds (it 
executed something), the state is new (changed the stack), so DFSearch 
happily goes one step down and restarts to search with thread 0. It's 
almost like we want to switch to BFS for one depth. So there's three 
solutions I could see:

(1) request a backtrack after breaking the por loop, to force the 
scheduler to advance past the suspicious thread at the same search 
level

(2) just 'blank out' the suspicious thread from the next forward 
scheduling sequence (i.e. skip it for the next search depth)

(3) re-order threads

While (1) seems to be less disruptive, there is of course a pretty 
hefty 'optimization' issue. If the thread doesn't recover (which is 
very likely), it will henceforth always cause one additional backtrack 
per search depth. I think it basically kills DFSearch at this point. 
Wonder what effects re-ordering would have on 
state-storage/backtracking, though. Don't know about (2) yet, either

the case is pretty easy to get:

public class Starve implements Runnable {
      public void run () {
           throw new RuntimeException("blow it up");
      }

      public static void main (String[] args) {
           Starve o = new Starve();
           Thread t = new Thread(o);
           t.start();

           int sum=0;
           while (true) { // starve t
                sum++;
           }
      }
}

-- Peter

On May 5, 2005, at 9:18 PM, Willem Visser wrote:

> Changing the thread order does seem extreme, but I'll think if there 
> is a
> reason not to do that.
>
> Of course you could also just break the loop and forget about it, if 
> there
> is something interesting in the rest of the system it will come out -
> pushing the "dead-thread" to the end would be an optimization.
>
> The thing here is that this issue should seldom come up, in fact if it 
> comes
> up in a "real" program then frankly it is a bug - you obviously didn't 
> want
> a non-progressing, non-interacting cycle in your code. The only 
> scenario
> this could legitimately happen is when you abstract a program - but we 
> don't
> do these kind of abstractions (we do the abstract state storing 
> variety).
>
> Others that have dealt with this kind of issue either punt by stating 
> these
> idle-loops are not allowed, or they use some clever loop breaking via
> back-edges etc.
>
> ----- Original Message -----
> From: "Peter C. Mehlitz" <pcm...@em...>
> To: "Willem Visser" <wv...@em...>; "John Penix"
> <Joh...@na...>
> Sent: Thursday, May 05, 2005 8:10 PM
> Subject: infinite POR loop
>
>
>> that's of course a bit more interesting - what we need in addition to 
>> a
>> trivial loop breaker is some sort of a Thread.yield, i.e. if we have a
>> suspicious thread that seems to bore us to death with idling, we have
>> to make sure we change the scheduling order, so that this sucker
>> henceforth always gets explored last. Should be simple enough by
>> pushing it to the end of the ThreadList when resetting the scheduler
>> (which is effectively an index re-order in SystemState.prepareNext()),
>> but I'm a bit uncertain what re-ordering does to us. I think, so far
>> thread indexes were invariant.
>>
>> Any insights, thoughts, suggestions?
>>
>> -- Peter
>>
>

[Javapathfinder-devel] CVS commit digest and policy

[Peter C. M. <pcm...@em...>]

I've added an entry to the CVSROOT/loginfo, to henceforth post commit 
messages to this list (so that people can see what's going on before 
the stuff eventually shows up in the anonymous repository).

When we commit, we should append a line "related bugs" that refers to 
corresponding entries in the bug tracking system.

Since there was no prior notification, I append a short digest of my 
major commits during the last days

-- Peter


------------------------------------------------ 05/04
superficially, this is a simplistic java.lang.Class.newInstance() 
implementation (we don't treat
exceptions yet).

But in reality it is the ability to call back into JPF executed code 
from native methods. This is not a full
circle yet, since the called JPF method will be executed atomically 
(i.e. is not allowed to block). This
can be worked around at some point by adding a sythetic frame to call 
the desired method (something
we already do for static inits during VM initialization), but that's 
not supported yet. But the main
infrastructure for this  (mostly the different return value and next pc 
handling by means of a call type
StackFrame attribute) is now in place.

The main motivation for this is to ease on-the-fly instrumentation in 
the future

related bugs: 1195640

------------------------------------------------ 05/02
* fixed problem with recursive class init (StaticArea.newClass), which 
also answered
the long standing question why there ever were life object overwrites 
accepted
(indeed that was a hack enabling recursive class init - sort of). Now 
the innermost
recursion proceeds with static class init, while the outer ones 
re-check before they
ever create/init a class object

* re-introduced UncaughtException usage. Indeed we need this to handle 
the
notorious 'ArrayIndexOutOfBounds' problem that was nothing but an 
unhandled
exception in a clinit (i.e. automatically executed code with an 
'artificial'
stackframe) that just didn't have the right provisions to check for 
failure
(no central place to check for null pc's - could be called from 
anywhere). This
also required slight changes to DFSearch, since we have to check for 
failed
properties no matter what when we return from forward (not just for new 
states)
The other searches already did this anyway.

maybe we should also do this for backtracks

related bugs: 1191665 (closing)

------------------------------------------------- 04/30
Java 1.5 LDC_W workaround

With Java 1.5, Sun silently introduced a classfile change - LDC_W can
now directly reference CLASS constpool entries. Unfortunately, BCEL 5.1 
chokes on it with a
hard exception. It's fixed in BCELs Subversion repository since Aug 
2004, but they don't
have a new release out yet. The mods I did (close to a hack) should 
compile with both BCELs,
but of course only run - when encountering a Java 1.5 classfile - with 
BCEL > 5.1 (e.g. from
their source repository). Good thing I built the runtime library 
snapshot from BCELs source
repository, so that should work.

Don't know yet if this fixes all Java 1.5 problems

The fix needs to be updated when a new BCEL version comes out 
(Types.CLASS)

related bugs: 1191462 (part)

--------------------------------------------------  04/29
fixed problem with extra-native method use of MJIEnv, mostly
by pulling heap and static area out of the MJIEnv call environment
(it's invariant).

Still the use of MJIEnv outside native methods is dangerous, since
you have to make sure you don't rely on the call environment, but
as long as we don't have MJIEnv refactored (which doesn't make much
sense otherwise), this seems to be the lesser of evils

related bugs: 1191644 (closing)

[Javapathfinder-devel] Re: Endless loops and POR?

[Peter C. M. <pcm...@em...>]

Yes, but before I do, I just want to think a few minutes about the 
livelock detection - it seems awfully close

-- Peter

On May 2, 2005, at 11:01 AM, Willem Visser wrote:
> I meant in POR transitions, but the same will happen in atomic steps.
>
> This is a pathological case I admit, but it is a problem - if someone
> writes a program with a meaningless endless loop, then even under a
> normal VM this will be bad. However if someone writes a meaningless
> endless loop in one thread and a bug in another thread then we'll never
> find the bug if the meaningless thread gets scheduled first.
>
> I think the counter would be good - it will fix this problem. But set 
> it
> real high so that we don't unnecessarily break por-steps.
>
>> -----Original Message-----
>> From: Peter C. Mehlitz [mailto:pcm...@em...]
>> Sent: Monday, May 02, 2005 10:49 AM
>> To: wv...@em...
>> Cc: jp...@em...
>> Subject: Re: Endless loops and POR?
>>
>> You mean POR transitions or atomic sections? You're right that we
>> currently have no "progress" check, but why wouldn't a normal VM loop
>> endlessly in this case? Or do you mean starvation, where another
> thread
>> would exit, but a daemon does endless loops w/o boundary steps so the
>> first one doesn't get scheduled? Right, that would be a problem
>>
>> should be easy to implement though, a simple counter should do. Can
>> actually be requested from outside (ThreadInfo.yield())
>>
>>> Do you know whether there is a flag/option to break loops in atomic
>>> steps? If not then we still have the bug that you could cycle
> forever
>>> in
>>> a loop that accesses no external variables and doesn't change state
> -
>>> no
>>> this is rare, but someone found it :-)
>

Re: [Javapathfinder-devel] Junit test failures?

[Peter C. M. <pcm...@em...>]

Ok, the LDC_W Java 1.5 issue should be resolved, here's my comment

    /*
      * Java 1.5 silently introduced a class file change - LDCs can now 
directly reference class
      * constpool entries. To make it more interesting, BCEL 5.1 chokes 
on this with a hard exception.
      * As of Aug 2004, this was fixed in the BCEL Subversion 
repository, but there is no new
      * release out yet. In order to compile this code with BCEL 5.1, we 
can't even use Type.CLASS.
      * The current hack should compile with both BCEL 5.1 and svn, but 
only runs - when encountering
      * a Java 1.5 class file - if the BCEL svn jar is used
      */

good thing I used the BCEL Subversion repository for our jpf-lib.zip 
snapshot.

But there are remaining Java 1.5 runtime issues: (1) TestAssert still 
hangs (interesting, it doesn't do much else than just raising an 
AssertionError - I guess that also has to do with class const 
handling), (2) some of the threading tests fail for apparently the same 
cause, which I assume is a change in one of the system classes (Thread, 
ThreadGroup etc.) we are depending on. Both need direct access to a box 
running Java 1.5, so it has to wait until next week.

-- Peter



On Apr 28, 2005, at 12:35 PM, Jean-Francois Halleux wrote:
> BCEL 5.1, "standard" binary distribution.
>
> JF
> -----Original Message-----
> From: Peter C. Mehlitz [mailto:pcm...@em...]
> Sent: jeudi 28 avril 2005 21:09
> To: <jav...@li...>
> Cc: hal...@sk...
> Subject: Re: [Javapathfinder-devel] Junit test failures?
>
>
> Thanks. Yes, it's a known BCEL / Java 1.5 problem caused by a changed
> LDC_W bytecode spec (LDCs can now directly reference class constants):
>
> java.lang.RuntimeException: Unknown or invalid constant type at 99
> 	at org.apache.bcel.generic.LDC.getType(LDC.java:148)
> 	at gov.nasa.jpf.jvm.bytecode.LDC_W.setPeer(LDC_W.java:47)
> ...
>
> strange thing is that it should be fixed in the current BCEL version.
> Which one do you use?
>
> -- Peter
>
>

RE: [Javapathfinder-devel] Junit test failures?

[Jean-Francois H. <hal...@sk...>]

BCEL 5.1, "standard" binary distribution.

JF
-----Original Message-----
From: Peter C. Mehlitz [mailto:pcm...@em...]
Sent: jeudi 28 avril 2005 21:09
To: <jav...@li...>
Cc: hal...@sk...
Subject: Re: [Javapathfinder-devel] Junit test failures?


Thanks. Yes, it's a known BCEL / Java 1.5 problem caused by a changed 
LDC_W bytecode spec (LDCs can now directly reference class constants):

java.lang.RuntimeException: Unknown or invalid constant type at 99
	at org.apache.bcel.generic.LDC.getType(LDC.java:148)
	at gov.nasa.jpf.jvm.bytecode.LDC_W.setPeer(LDC_W.java:47)
...

strange thing is that it should be fixed in the current BCEL version. 
Which one do you use?

-- Peter

Re: [Javapathfinder-devel] Junit test failures?

[Peter C. M. <pcm...@em...>]

Thanks. Yes, it's a known BCEL / Java 1.5 problem caused by a changed 
LDC_W bytecode spec (LDCs can now directly reference class constants):

java.lang.RuntimeException: Unknown or invalid constant type at 99
	at org.apache.bcel.generic.LDC.getType(LDC.java:148)
	at gov.nasa.jpf.jvm.bytecode.LDC_W.setPeer(LDC_W.java:47)
...

strange thing is that it should be fixed in the current BCEL version. 
Which one do you use?

-- Peter

Re: [Javapathfinder-devel] Junit test failures?

[Peter C. M. <pcm...@em...>]

Yes, that looks like a JDK 1.5 issue. Unfortunately I can't test this 
right now, but can you send me a tarball of the build/test/TestXX.txt 
files you get when you run the regression tests? That should give me a 
better idea of what's going on.

Thx
-- Peter

[Javapathfinder-devel] the ;missing lib' problem

[Peter C. M. <pcm...@em...>]

this is a failing Ant javac task, or more specifically the fileset 
construct that is used to collect jars and zips from the 'lib' dir. I 
modified the build.xml so that it starts at the toplevel dir, and uses 
${lib.dir} only as a pattern component. That should fix it for now, 
whether you have the jars under 'lib' or externally

-- Peter

RE: [Javapathfinder-devel] Junit test failures?

[Willem V. <wv...@em...>]

Hi,

Just checkout and ran from here and all tests pass. However I'm pretty
sure the problem is JDK 1.5, I'm using 1.4. Unfortunately we didn't test
with 1.5, and there are small VM changes in 1.5 (not to mention changes
in the libraries) that some of our tests must be running into.

Thanks for pointing this problem out to us - we'll fix it soon. I
suggest using 1.4 for use with JPF in the interim.

Bye,
Willem=20

--
Willem C. Visser                 Automated Software Engineering Group
RIACS/NASA Ames Research Center            wv...@em...
M/S 269-2                                     http://ase.arc.nasa.gov
Moffett Field, CA 94035                (650)604-3515 fax 4036  rm 235


> -----Original Message-----
> From: jav...@li...
> [mailto:jav...@li...] On Behalf Of
> Jean-Francois Halleux
> Sent: Wednesday, April 27, 2005 1:36 PM
> To: jav...@li...
> Subject: [Javapathfinder-devel] Junit test failures?
>=20
> Hello,
>=20
> 	thanks for making this project open source.
>=20
> a) The run-tests target appears to return failures for some tests (see
> details hereunder).
> b) I had to skip "TestAssertJPF" because it would not return its
results
> after 15 minutes.
>=20
> OS is Windows NT 2000 SP4, JVM is SUN JDK 1.5.0.2, src is latest from
HEAD
>=20
> Is this expected or should all the unit tests pass ?
>=20
> Regards,
>=20
> Jean-Fran=E7ois Halleux
>=20
>=20
> run-tests:
>      [echo] --- running Junit tests from build/test..
>     [junit] Running gov.nasa.jpf.jvm.TestArrayJPF
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestArray
> test2DArray
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestArray
> test2DStringArra
> y
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestArray
testAoBX
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestArray
> testCharArray
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestArray
> testIntArray
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestArray
> testStringArray
>     [junit] Tests run: 6, Failures: 0, Errors: 0, Time elapsed: 4,126
sec
>=20
>=20
>     [junit] Running gov.nasa.jpf.jvm.TestCastJPF
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestCast
testCast
> testCast
> Fail
>     [junit] Tests run: 1, Failures: 0, Errors: 0, Time elapsed: 1,802
sec
>=20
>=20
>     [junit] Running gov.nasa.jpf.jvm.TestExceptionJPF
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestException
> testNPE
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestException
> testNPECall
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestException
> testArrayInd
> exOutOfBoundsLow
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestException
> testArrayInd
> exOutOfBoundsHigh
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestException
> testLocalHan
> dler
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestException
> testCallerHa
> ndler
>     [junit] Tests run: 6, Failures: 0, Errors: 0, Time elapsed: 4,106
sec
>=20
>=20
>     [junit] Running gov.nasa.jpf.jvm.TestFieldJPF
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestField
> testReadInstance
>=20
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestField
> testReadStatic
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestField
> testWriteInstanc
> e
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestField
> testWriteStatic
>     [junit] Tests run: 4, Failures: 0, Errors: 0, Time elapsed: 3,105
sec
>=20
>=20
>     [junit] Running gov.nasa.jpf.jvm.TestJavaLangClassJPF
>     [junit]   running jpf with args:
gov.nasa.jpf.jvm.TestJavaLangClass
> testClas
> sField
>     [junit]   running jpf with args:
gov.nasa.jpf.jvm.TestJavaLangClass
> testClas
> sForName
>     [junit]   running jpf with args:
gov.nasa.jpf.jvm.TestJavaLangClass
> testGetC
> lass
>     [junit]   running jpf with args:
gov.nasa.jpf.jvm.TestJavaLangClass
> testIden
> tity
>     [junit] Tests run: 4, Failures: 0, Errors: 0, Time elapsed: 2,995
sec
>=20
>=20
>     [junit] Running gov.nasa.jpf.jvm.TestMethodJPF
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestMethod
testCtor
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestMethod
testCall
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestMethod
> testInheritedCa
> ll
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestMethod
> testVirtualCall
>=20
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestMethod
> testSpecialCall
>=20
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestMethod
> testStaticCall
>     [junit] Tests run: 6, Failures: 0, Errors: 0, Time elapsed: 4,136
sec
>=20
>=20
>     [junit] Running gov.nasa.jpf.jvm.TestNativePeerJPF
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
> testClInit
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
> testNativeC
> reate2DimIntArray
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
> testNativeC
> reateIntArray
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
> testNativeC
> reateStringArray
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
> testNativeE
> xception
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
> testNativeC
> rash
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
> testInit
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
> testNativeI
> nstanceMethod
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
> testNativeS
> taticMethod
>     [junit] Tests run: 9, Failures: 0, Errors: 0, Time elapsed: 4,967
sec
>=20
>=20
>     [junit] Running gov.nasa.jpf.jvm.TestThreadJPF
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestThread
> testDaemon
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestThread
testMain
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestThread
testName
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestThread
> testPriority
>     [junit] Tests run: 4, Failures: 0, Errors: 0, Time elapsed: 3,304
sec
>=20
>=20
>     [junit] Running gov.nasa.jpf.jvm.TestWaitJPF
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestWait
> testSimpleWait
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestWait
> testLoopedWait
>     [junit]   running jpf with args: gov.nasa.jpf.jvm.TestWait
> testInterruptedWa
> it
>     [junit] Tests run: 3, Failures: 0, Errors: 0, Time elapsed: 2,964
sec
>=20
>=20
>     [junit] Running gov.nasa.jpf.mc.TestCrossingJPF
>     [junit]   running jpf with args: gov.nasa.jpf.mc.Crossing
>     [junit]   running jpf with args:
> +search.class=3Dgov.nasa.jpf.search.heuristic
> .HeuristicSearch
> +search.heuristic.class=3Dgov.nasa.jpf.search.heuristic.BFSHeuris
> tic gov.nasa.jpf.mc.Crossing
>     [junit] Tests run: 2, Failures: 1, Errors: 1, Time elapsed: 3,875
sec
>=20
>=20
>     [junit] TEST gov.nasa.jpf.mc.TestCrossingJPF FAILED
>     [junit] Running gov.nasa.jpf.mc.TestRandomJPF
>     [junit]   running jpf with args: gov.nasa.jpf.mc.TestRandom
testRandom
> 3
>     [junit]   running jpf with args:
> +search.class=3Dgov.nasa.jpf.search.heuristic
> .HeuristicSearch
> +search.heuristic.class=3Dgov.nasa.jpf.search.heuristic.BFSHeuris
> tic gov.nasa.jpf.mc.TestRandom
>     [junit] Tests run: 2, Failures: 0, Errors: 0, Time elapsed: 2,213
sec
>=20
>=20
>     [junit] Running gov.nasa.jpf.mc.TestVMDeadlockJPF
>     [junit]   running jpf with args: gov.nasa.jpf.mc.TestVMDeadlock
> testSyncMthD
> eadlock
>     [junit]   running jpf with args: gov.nasa.jpf.mc.TestVMDeadlock
> testSyncBloc
> kDeadlock
>     [junit]   running jpf with args: gov.nasa.jpf.mc.TestVMDeadlock
> testMixedDea
> dlock
>     [junit]   running jpf with args: gov.nasa.jpf.mc.TestVMDeadlock
> testMissedSi
> gnalDeadlock
>     [junit] Tests run: 4, Failures: 4, Errors: 0, Time elapsed: 3,485
sec
>=20
>=20
>     [junit] TEST gov.nasa.jpf.mc.TestVMDeadlockJPF FAILED
>=20
>=20
>=20
> -------------------------------------------------------
> SF.Net email is sponsored by: Tell us your software development plans!
> Take this survey and enter to win a one-year sub to SourceForge.net
> Plus IDC's 2005 look-ahead and a copy of this survey
> Click here to start!  http://www.idcswdc.com/cgi-bin/survey?id=105hix
> _______________________________________________
> Javapathfinder-devel mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel

[Javapathfinder-devel] Junit test failures?

[Jean-Francois H. <hal...@sk...>]

Hello,

	thanks for making this project open source.

a) The run-tests target appears to return failures for some tests (see
details hereunder).
b) I had to skip "TestAssertJPF" because it would not return its results
after 15 minutes.

OS is Windows NT 2000 SP4, JVM is SUN JDK 1.5.0.2, src is latest from HEA=
D

Is this expected or should all the unit tests pass ?

Regards,

Jean-Fran=E7ois Halleux


run-tests:
     [echo] --- running Junit tests from build/test..
    [junit] Running gov.nasa.jpf.jvm.TestArrayJPF
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestArray test2DArr=
ay
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestArray
test2DStringArra
y
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestArray testAoBX
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestArray
testCharArray
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestArray testIntAr=
ray
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestArray
testStringArray
    [junit] Tests run: 6, Failures: 0, Errors: 0, Time elapsed: 4,126 sec


    [junit] Running gov.nasa.jpf.jvm.TestCastJPF
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestCast testCast
testCast
Fail
    [junit] Tests run: 1, Failures: 0, Errors: 0, Time elapsed: 1,802 sec


    [junit] Running gov.nasa.jpf.jvm.TestExceptionJPF
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestException testN=
PE
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestException
testNPECall
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestException
testArrayInd
exOutOfBoundsLow
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestException
testArrayInd
exOutOfBoundsHigh
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestException
testLocalHan
dler
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestException
testCallerHa
ndler
    [junit] Tests run: 6, Failures: 0, Errors: 0, Time elapsed: 4,106 sec


    [junit] Running gov.nasa.jpf.jvm.TestFieldJPF
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestField
testReadInstance

    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestField
testReadStatic
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestField
testWriteInstanc
e
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestField
testWriteStatic
    [junit] Tests run: 4, Failures: 0, Errors: 0, Time elapsed: 3,105 sec


    [junit] Running gov.nasa.jpf.jvm.TestJavaLangClassJPF
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestJavaLangClass
testClas
sField
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestJavaLangClass
testClas
sForName
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestJavaLangClass
testGetC
lass
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestJavaLangClass
testIden
tity
    [junit] Tests run: 4, Failures: 0, Errors: 0, Time elapsed: 2,995 sec


    [junit] Running gov.nasa.jpf.jvm.TestMethodJPF
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestMethod testCtor
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestMethod testCall
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestMethod
testInheritedCa
ll
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestMethod
testVirtualCall

    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestMethod
testSpecialCall

    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestMethod
testStaticCall
    [junit] Tests run: 6, Failures: 0, Errors: 0, Time elapsed: 4,136 sec


    [junit] Running gov.nasa.jpf.jvm.TestNativePeerJPF
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
testClInit
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
testNativeC
reate2DimIntArray
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
testNativeC
reateIntArray
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
testNativeC
reateStringArray
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
testNativeE
xception
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
testNativeC
rash
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
testInit
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
testNativeI
nstanceMethod
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestNativePeer
testNativeS
taticMethod
    [junit] Tests run: 9, Failures: 0, Errors: 0, Time elapsed: 4,967 sec


    [junit] Running gov.nasa.jpf.jvm.TestThreadJPF
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestThread testDaem=
on
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestThread testMain
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestThread testName
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestThread
testPriority
    [junit] Tests run: 4, Failures: 0, Errors: 0, Time elapsed: 3,304 sec


    [junit] Running gov.nasa.jpf.jvm.TestWaitJPF
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestWait
testSimpleWait
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestWait
testLoopedWait
    [junit]   running jpf with args: gov.nasa.jpf.jvm.TestWait
testInterruptedWa
it
    [junit] Tests run: 3, Failures: 0, Errors: 0, Time elapsed: 2,964 sec


    [junit] Running gov.nasa.jpf.mc.TestCrossingJPF
    [junit]   running jpf with args: gov.nasa.jpf.mc.Crossing
    [junit]   running jpf with args:
+search.class=3Dgov.nasa.jpf.search.heuristic
.HeuristicSearch
+search.heuristic.class=3Dgov.nasa.jpf.search.heuristic.BFSHeuris
tic gov.nasa.jpf.mc.Crossing
    [junit] Tests run: 2, Failures: 1, Errors: 1, Time elapsed: 3,875 sec


    [junit] TEST gov.nasa.jpf.mc.TestCrossingJPF FAILED
    [junit] Running gov.nasa.jpf.mc.TestRandomJPF
    [junit]   running jpf with args: gov.nasa.jpf.mc.TestRandom testRando=
m 3
    [junit]   running jpf with args:
+search.class=3Dgov.nasa.jpf.search.heuristic
.HeuristicSearch
+search.heuristic.class=3Dgov.nasa.jpf.search.heuristic.BFSHeuris
tic gov.nasa.jpf.mc.TestRandom
    [junit] Tests run: 2, Failures: 0, Errors: 0, Time elapsed: 2,213 sec


    [junit] Running gov.nasa.jpf.mc.TestVMDeadlockJPF
    [junit]   running jpf with args: gov.nasa.jpf.mc.TestVMDeadlock
testSyncMthD
eadlock
    [junit]   running jpf with args: gov.nasa.jpf.mc.TestVMDeadlock
testSyncBloc
kDeadlock
    [junit]   running jpf with args: gov.nasa.jpf.mc.TestVMDeadlock
testMixedDea
dlock
    [junit]   running jpf with args: gov.nasa.jpf.mc.TestVMDeadlock
testMissedSi
gnalDeadlock
    [junit] Tests run: 4, Failures: 4, Errors: 0, Time elapsed: 3,485 sec


    [junit] TEST gov.nasa.jpf.mc.TestVMDeadlockJPF FAILED