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

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

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

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

Modified Files:
	ListenerAdapter.java 
Log Message:
grammar fix in comment :)

Index: ListenerAdapter.java
===================================================================
RCS file: /cvsroot/javapathfinder//javapathfinder/src/gov/nasa/jpf/ListenerAdapter.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- ListenerAdapter.java	10 May 2005 06:46:54 -0000	1.1
+++ ListenerAdapter.java	6 Sep 2005 21:21:08 -0000	1.2
@@ -21,7 +21,7 @@
 
 /**
  * Adapter class that dummy implements both VMListener and SearchListener interfaces
- * Used to ease implementation of listeners that only process few notifications
+ * Used to ease implementation of listeners that only process a few notifications
  */
 public class ListenerAdapter implements VMListener, SearchListener {
 

[Javapathfinder-devel] update and JPF and Java 1.5

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

I think I got most of the Java 1.5 problems sorted out - can you  
please start to use JPF (from CVS) on Java 1.5, so that I get a bit  
more testing before we make a new release?

-- Peter

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

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

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

Modified Files:
	JPF_java_lang_StringBuffer.java 
Log Message:
Java 1.5 apparently has changed the java.lang.StringBuffer implementation
(the 'shared' hack is gone), so we have to do some evil version branching
in our native peer class


Index: JPF_java_lang_StringBuffer.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_StringBuffer.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- JPF_java_lang_StringBuffer.java	26 Apr 2005 19:43:27 -0000	1.1.1.1
+++ JPF_java_lang_StringBuffer.java	26 Aug 2005 21:30:28 -0000	1.2
@@ -23,8 +23,25 @@
 /**
  * MJI NativePeer class for java.lang.StringBuffer library abstraction
  */
-public class JPF_java_lang_StringBuffer
-{
+public class JPF_java_lang_StringBuffer {
+  
+  static boolean hasSharedField = false; // Java 1.4 has, 1.5 doesn't
+  
+  public static void $clinit (MJIEnv env, int clsObjRef) {
+    // apparently, Java 1.5 has changed the implementation of class
+    // StringBuffer so that it doesn't use the 'shared' state anymore
+    // (which was a performance hack to avoid copying the char array
+    // data when creating String objects from subsequently unmodified
+    // StringBuffers
+    // adding this little extra logic here also serves the purpose of
+    // avoiding a native ObjectStreamClass method which is called during
+    // the static StringBuffer init
+    ClassInfo ci = env.getClassInfo();
+    if (ci.getInstanceField("shared") != null) {
+      hasSharedField = true;
+    }
+  }
+  
   static int appendString (MJIEnv env, int objref, String s) {
     int slen = s.length();
     int aref = env.getReferenceField(objref, "value");
@@ -52,7 +69,9 @@
       env.setReferenceField(objref, "value", arefNew);
     }
     
-    env.setBooleanField(objref, "shared", false);
+    if (hasSharedField) {
+      env.setBooleanField(objref, "shared", false);
+    }
     env.setIntField(objref, "count", n);
     
     return objref;
@@ -128,7 +147,9 @@
       env.setReferenceField(objref, "value", arefNew);
     }
     
-    env.setBooleanField(objref, "shared", false);
+    if (hasSharedField) {
+      env.setBooleanField(objref, "shared", false);
+    }
     env.setIntField(objref, "count", n);
     
     return objref;

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

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

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

Modified Files:
	RaceDetector.java 
Log Message:
Ok, since I claimed it would be easy to check for cycles, I've just added this. It's still a bit over-simplified, since we don't check for identical call stacks in each access thread, but again I claim that's easy enough (hashing ThreadInfo call stacks could probably be quite handy for other things too, so I will add it there). In fact, RaceDetector changes would be minor (the FieldAccess ctor and equal()), and it now can deal with sync by signals 

Index: RaceDetector.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/RaceDetector.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- RaceDetector.java	25 Aug 2005 17:02:16 -0000	1.1
+++ RaceDetector.java	25 Aug 2005 18:22:57 -0000	1.2
@@ -62,6 +62,8 @@
       this.ti = ti;
       this.finsn = finsn;
       this.locksHeld = ti.getLockedObjects().toArray();
+      
+      // <2do> we should also hash the threads callstack here
     }
   
     Object[] intersect (Object[] a, Object[] b) {
@@ -104,11 +106,23 @@
       return null; // no potential conflict found
     }
     
+    public boolean equals (Object other) {
+      if (other instanceof FieldAccess) {
+        FieldAccess fa = (FieldAccess)other;
+        if (ti != fa.ti) return false;
+        if (finsn != fa.finsn) return false;
+        // <2do> we should also check for same callstack, but that's a detail we leave out for now
+        
+        return true;
+      }
+      return false;
+    }
+    
     String describe () {
       String s = isWriteAccess() ? "write" : "read"; 
       s += " from thread: \"";
       s += ti.getName();
-      s += "\", locking {";
+      s += "\", holding locks {";
       for (int i=0; i<locksHeld.length; i++) {
         if (i>0) s += ',';
         s += locksHeld[i];
@@ -145,11 +159,18 @@
   
   Stack transitions = new Stack();   // the stack of FieldStateChanges
   ArrayList pendingChanges;          // changed FieldStates during the last transition
+  FieldAccess access1, access2;      // our race candidates (race if encountered in reverse order)
   FieldAccessSequence raceField;     // if this becomes non-null, we have a race and terminate
+  
   String[] watchFields;              // list of regular expressions to match class/field names
+  boolean terminate;                 // terminate search when we found a (potential) race
+  boolean verifyCycle;               // don't report potentials, go on until encountering
+                                     // the suspicious insns in both orders
   
   public RaceDetector (Config config) {
     watchFields = config.getStringArray("race.fields");
+    terminate = config.getBoolean("race.terminate", true);
+    verifyCycle = config.getBoolean("race.verify_cycle", false);
   }
     
   boolean isWatchedField (FieldInstruction finsn) {
@@ -239,11 +260,29 @@
           if (!fa.hasLockCandidates()) {
             FieldAccess conflict = fa.getConflict();            
             if (conflict != null) {
-              raceField = fs;
               
-              System.err.println("potential race detected: " + fs.id);
-              System.err.println("\t" + fa.describe());
-              System.err.println("\t" + conflict.describe());
+              if (verifyCycle) {
+                if (access1 != null) {
+                  if (fa.equals(access2) && conflict.equals(access1)) {
+                    if (terminate) {
+                      raceField = fs;
+                    }
+                    System.err.println("race detected (access occurred in both orders): " + fs.id);
+                    System.err.println("\t" + fa.describe());
+                    System.err.println("\t" + conflict.describe());                    
+                  }
+                } else {
+                  access1 = fa;
+                  access2 = conflict;
+                }
+              } else {
+                if (terminate) {
+                  raceField = fs;
+                }
+                System.err.println("potential race detected: " + fs.id);
+                System.err.println("\t" + fa.describe());
+                System.err.println("\t" + conflict.describe());
+              }              
             }
           }
         }

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm StaticElementInfo.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-serv9016/src/gov/nasa/jpf/jvm

Modified Files:
	StaticElementInfo.java 
Log Message:
omit @<index> postfix in toString(), as it is misleading (not distinguishable from DynamicElementInfos, and quite pointless for statics)

Index: StaticElementInfo.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/StaticElementInfo.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- StaticElementInfo.java	26 Apr 2005 19:44:05 -0000	1.1.1.1
+++ StaticElementInfo.java	25 Aug 2005 17:19:49 -0000	1.2
@@ -122,6 +122,10 @@
     return classObjectRef;
   }
 
+  public String toString() {
+    return getClassInfo().getName(); // don't append index (useless and misleading for statics)
+  }
+  
   private void blowup () {
     throw new JPFException("cannot access StaticElementInfo by index");
   }

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

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

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

Modified Files:
	InstanceFieldInstruction.java 
Log Message:
field varId was shadowing a super class field

Index: InstanceFieldInstruction.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode/InstanceFieldInstruction.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- InstanceFieldInstruction.java	26 Apr 2005 19:44:12 -0000	1.1.1.1
+++ InstanceFieldInstruction.java	25 Aug 2005 17:12:46 -0000	1.2
@@ -31,7 +31,6 @@
 public abstract class InstanceFieldInstruction extends FieldInstruction
 {
   int lastThis = -1;
-  String varId;
   
   public FieldInfo getFieldInfo () {
     if (fi == null) {
@@ -56,7 +55,8 @@
     
     return true;
   }
-   
+
+  
   public int getLastThis() {
     return lastThis;
   }

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

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

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

Modified Files:
	Instruction.java 
Log Message:
added a convenience method getSourceLocation() returning a String with file:line info

Index: Instruction.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode/Instruction.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- Instruction.java	7 May 2005 00:10:56 -0000	1.2
+++ Instruction.java	25 Aug 2005 17:11:11 -0000	1.3
@@ -19,6 +19,7 @@
 package gov.nasa.jpf.jvm.bytecode;
 
 import gov.nasa.jpf.JPFException;
+import gov.nasa.jpf.jvm.ClassInfo;
 import gov.nasa.jpf.jvm.JVM;
 import gov.nasa.jpf.jvm.KernelState;
 import gov.nasa.jpf.jvm.MethodInfo;
@@ -188,6 +189,25 @@
     return s.substring(26);  // gov.nasa.jpf.jvm.bytecode package
   }
   
+  public String getSourceLocation () {
+    ClassInfo ci = mi.getClassInfo();
+    int line = mi.getLineNumber(this);
+    String file = ci.getSourceFileName();
+    
+    String s = ci.getName() + '.' + mi.getFullName() + " at ";
+    
+    if (file != null) {
+      s +=  file;
+      s += ':'; 
+      s += line;
+    } else {
+      s += "pc ";
+      s += position;
+    }
+    
+    return s;
+  }
+  
   //SUNYSB
   protected abstract void setPeer (org.apache.bcel.generic.Instruction i,
                                    ConstantPool cp);

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

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

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

Modified Files:
	HeapTracker.java 
Log Message:
updated HeapTracker to use properties instead of command line args for its parameters, and derived it from PropertyListenerAdapter

Index: HeapTracker.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/HeapTracker.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- HeapTracker.java	26 Apr 2005 19:44:21 -0000	1.1.1.1
+++ HeapTracker.java	25 Aug 2005 17:06:00 -0000	1.2
@@ -19,9 +19,7 @@
 
 package gov.nasa.jpf.tools;
 
-import gov.nasa.jpf.GenericProperty;
-import gov.nasa.jpf.VMListener;
-import gov.nasa.jpf.SearchListener;
+import gov.nasa.jpf.PropertyListenerAdapter;
 import gov.nasa.jpf.VM;
 
 import gov.nasa.jpf.jvm.ElementInfo;
@@ -41,14 +39,10 @@
 import java.util.regex.Pattern;
 
 /**
- * HeapTracker - listener class to check heap utilization along all
- * execution paths (e.g. to verify heap bounds). HeapTracker is a drop-in
- * replacement for JPF (which is called by it).
- *.
- * This listener also shows how to terminate JPF in case of a property violation
- * by registering itself as a JPF Property instance
+ * HeapTracker - property-listener class to check heap utilization along all
+ * execution paths (e.g. to verify heap bounds)
  */
-public class HeapTracker extends GenericProperty implements VMListener, SearchListener {
+public class HeapTracker extends PropertyListenerAdapter {
   
   class PathStat implements Cloneable {
     int nNew = 0;
@@ -63,8 +57,7 @@
       }
     }
   }
-  
-    
+      
   PathStat stat = new PathStat();
   Stack pathStats = new Stack();
   
@@ -108,8 +101,8 @@
   int initAlive = 0;
 
   // used as a property check
-  int maxHeapSizeLimit = -1;
-  int maxLiveLimit = -1;
+  int maxHeapSizeLimit;
+  int maxLiveLimit;
   boolean throwOutOfMemory = false;
   Pattern classPattern = null;
   
@@ -132,15 +125,26 @@
       }
   }
 
+  public HeapTracker (Config config) {
+    maxHeapSizeLimit = config.getInt("heap.size_limit", -1);
+    maxLiveLimit = config.getInt("heap.live_limit", -1);
+    throwOutOfMemory = config.getBoolean("heap.throw_exception");
+    
+    String regEx = config.getString("heap.classes");
+    if (regEx != null) {
+      classPattern = Pattern.compile(regEx);
+    }
+  }
+  
   /******************************************* abstract Property *****/
 
   /**
-   * return 'true' if property is violated
+   * return 'false' if property is violated
    */
   public boolean check (VM vm, Object arg) {
     if (throwOutOfMemory) {
       // in this case we don't want to stop the program, but see if it
-      // behaves gracefully
+      // behaves gracefully - don't report a property violation
       return true;
     } else {
       if ((maxHeapSizeLimit >= 0) && (stat.heapSize > maxHeapSizeLimit)) {
@@ -160,6 +164,8 @@
   
   /******************************************* SearchListener interface *****/
   public void searchStarted(Search search) {
+    super.searchStarted(search);
+    
     updateMaxPathValues();
     pathStats.push(stat);
     
@@ -186,10 +192,6 @@
     }
   }
   
-  public void stateProcessed (Search search) {
-    // nothing to do
-  }
-  
   public void stateBacktracked(Search search) {
     nBacktrack++;
     
@@ -233,35 +235,8 @@
     System.out.println(" / " + (maxPathReleased - initReleased));
   }
   
-  public void searchConstraintHit(Search search) {
-    // TODO
-  }
-  
-  public void stateRestored(Search search) {
-    // TODO
-  }
-    
-  public void propertyViolated(Search search) {
-    // TODO
-  }
-  
   
   /******************************************* VMListener interface *********/
-  public void exceptionThrown(VM vm) {
-    // not interested
-  }
-  public void threadStarted(VM vm) {
-  }
-  public void threadTerminated(VM vm) {
-  }
-  
-  public void classLoaded(VM vm) {
-    // not interested
-  }
-  public void instructionExecuted(VM vm) {
-  }
-  
-  /***** the processed notifications ****************/
   public void gcBegin(VM vm) {
     JVM jvm = (JVM)vm;
     /**
@@ -407,42 +382,13 @@
   }
   
   
-  void filterArgs (String[] args) {
-    for (int i=0; i<args.length; i++) {
-      if (args[i].equals("-heapSizeLimit")) {
-        args[i++] = null;
-        if (i < args.length) {
-          maxHeapSizeLimit = Integer.parseInt(args[i]);
-          args[i] = null;
-        }
-      } else if (args[i].equals("-liveLimit")) {
-        args[i++] = null;
-        if (i < args.length) {
-          maxLiveLimit = Integer.parseInt(args[i]);
-          args[i] = null;
-        }
-      } else if (args[i].equals("-classPattern")) {
-        args[i++] = null;
-        if (i < args.length) {
-          String regEx = args[i];
-          args[i] = null;
-          
-          classPattern = Pattern.compile(regEx);
-        }
-      }else if (args[i].equals("-throwOutOfMemory")) {
-        args[i] = null;
-        throwOutOfMemory = true;
-      }
-    }
-  }
-  
   static void printUsage () {
     System.out.println("HeapTracker - a JPF listener tool to report and check heap utilization");
     System.out.println("usage: java gov.nasa.jpf.tools.HeapTracker <jpf-options> <heapTracker-options> <class>");
-    System.out.println("       -heapSizeLimit <num> : report property violation if heap exceeds <num> bytes");
-    System.out.println("       -liveLimit <num> : report property violation if more than <num> live objects");
-    System.out.println("       -classPattern <regEx> : only report instances of classes matching <regEx>");
-    System.out.println("       -throwOutOfMemory: throw a OutOfMemoryError instead of reporting property violation");
+    System.out.println("       +heap.size_limit=<num> : report property violation if heap exceeds <num> bytes");
+    System.out.println("       +heap.live_limit=<num> : report property violation if more than <num> live objects");
+    System.out.println("       +heap.classes=<regEx> : only report instances of classes matching <regEx>");
+    System.out.println("       +heap.throw_exception=<bool>: throw a OutOfMemoryError instead of reporting property violation");
   }
 
   
@@ -451,13 +397,11 @@
       printUsage();
       return;
     }
-    
-    HeapTracker listener = new HeapTracker();
-    listener.filterArgs(args);
-    
     Config conf = JPF.createConfig(args);
     // set own options here..
     
+    HeapTracker listener = new HeapTracker(conf);    
+    
     JPF jpf = new JPF(conf);
     jpf.addSearchListener(listener);
     jpf.addVMListener(listener);

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/tools RaceDetector.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-serv2066/src/gov/nasa/jpf/tools

Added Files:
	RaceDetector.java 
Log Message:
simple lockset based race detector listener. We don't check for cycles yet (i.e. if the potentially conflicting operations really could occur in reverse order), but that should be easy to add 

--- NEW FILE: RaceDetector.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 java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Stack;

import gov.nasa.jpf.PropertyListenerAdapter;
import gov.nasa.jpf.Search;
import gov.nasa.jpf.VM;
import gov.nasa.jpf.Config;
import gov.nasa.jpf.jvm.ElementInfo;
import gov.nasa.jpf.jvm.JVM;
import gov.nasa.jpf.jvm.ThreadInfo;
import gov.nasa.jpf.jvm.bytecode.FieldInstruction;
import gov.nasa.jpf.jvm.bytecode.InstanceFieldInstruction;
import gov.nasa.jpf.jvm.bytecode.Instruction;
import gov.nasa.jpf.jvm.bytecode.PUTFIELD;
import gov.nasa.jpf.jvm.bytecode.PUTSTATIC;
import gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction;

/**
 * Simple field access race detector example
 * 
 * This implemenation so far doesn't deal with synchronization via signals, it
 * only checks if the lockset intersections of reads and writes from different
 * threads get empty. A more sophisticated version would check if the two
 * suspicious access operations (one read, one write) will also happen in reverse
 * order (that's the beauty of using this inside a model checker)
 */
public class RaceDetector extends PropertyListenerAdapter {
  
  /*** helper classes ***************************************************************/
  static class FieldAccess {
    ThreadInfo ti;
    Object[] locksHeld;          // the ones we have during this operation (not really required)
    Object[] lockCandidates;     // the intersection for all prev operations
    FieldInstruction finsn;
    
    FieldAccess prev;
    
    FieldAccess (ThreadInfo ti, FieldInstruction finsn) {
      this.ti = ti;
      this.finsn = finsn;
      this.locksHeld = ti.getLockedObjects().toArray();
    }
  
    Object[] intersect (Object[] a, Object[] b) {
      ArrayList list = new ArrayList(a.length);
      for (int i=0; i<a.length; i++) {
        for (int j=0; j<b.length; j++) {
          if (a[i].equals(b[j])) {
            list.add(a[i]);
            break;
          }
        }
      }
      return (list.size() == a.length) ? a : list.toArray();
    }
    
    void updateLockCandidates () {
      if (prev == null) {
        lockCandidates = locksHeld;
      } else {
        lockCandidates = intersect(locksHeld, prev.lockCandidates);
      }
    }
    
    boolean hasLockCandidates () {
      return (lockCandidates.length > 0);
    }
    
    boolean isWriteAccess () {
      return ((finsn instanceof PUTFIELD) || (finsn instanceof PUTSTATIC));
    }
    
    FieldAccess getConflict () {
      boolean isWrite = isWriteAccess();
      
      for (FieldAccess c = prev; c != null; c = c.prev) {
        if ((c.ti != ti) && (isWrite != c.isWriteAccess())) {
          return c;
        }
      }
      return null; // no potential conflict found
    }
    
    String describe () {
      String s = isWriteAccess() ? "write" : "read"; 
      s += " from thread: \"";
      s += ti.getName();
      s += "\", locking {";
      for (int i=0; i<locksHeld.length; i++) {
        if (i>0) s += ',';
        s += locksHeld[i];
      }
      s += "} in ";
      s += finsn.getSourceLocation();
      return s;
    }
  }
  
  static class FieldAccessSequence {
    String id;
    FieldAccess lastAccess;
    
    FieldAccessSequence (String id) {
      this.id = id;
    }
      
    void addAccess (FieldAccess fa) {
      fa.prev = lastAccess;
      lastAccess = fa;
      fa.updateLockCandidates();
    }
    
    void purgeLastAccess () {
      lastAccess = lastAccess.prev;
    }
    
  }
    

  /*** private fields and methods ****************************************/
  HashMap fields = new HashMap();
  
  Stack transitions = new Stack();   // the stack of FieldStateChanges
  ArrayList pendingChanges;          // changed FieldStates during the last transition
  FieldAccessSequence raceField;     // if this becomes non-null, we have a race and terminate
  String[] watchFields;              // list of regular expressions to match class/field names
  
  public RaceDetector (Config config) {
    watchFields = config.getStringArray("race.fields");
  }
    
  boolean isWatchedField (FieldInstruction finsn) {
    if (watchFields == null) {
      return true;
    }
    
    String fname = finsn.getVariableId();
    
    for (int i = 0; i<watchFields.length; i++) {
      if (fname.matches(watchFields[i])){
        return true;
      }
    }
    
    return false;
  }
    
  
  /*** GenericProperty **************************************************/
  
  public boolean check(VM vm, Object arg) {
    return (raceField == null);
  }
  
  public String getErrorMessage () {
    return ("potential field race: " + raceField.id);
  }
  
  /*** SearchListener ****************************************************/
  
  public void stateAdvanced(Search search) {
    transitions.push(pendingChanges);
    pendingChanges = null;
  }

  public void stateBacktracked(Search search) {
    ArrayList fops = (ArrayList) transitions.pop();
    if (fops != null) {
      for (Iterator it=fops.iterator(); it.hasNext(); ) {
        FieldAccessSequence fs = (FieldAccessSequence) it.next();
        fs.purgeLastAccess();
      }      
    }
  }
  
  /*** VMListener *******************************************************/
  
  public void instructionExecuted(VM vm) {
    JVM jvm = (JVM)vm;
    Instruction insn = jvm.getLastInstruction();
    
    if (insn instanceof FieldInstruction) {
      ThreadInfo ti = jvm.getLastThreadInfo();
      FieldInstruction finsn = (FieldInstruction)insn;
      String id = null;

      if (raceField != null) { // we only report the first one
        return;
      }
      
      if (ti.hasOtherRunnables() && isWatchedField(finsn)) {
        if (insn instanceof StaticFieldInstruction) { // that's shared per se
          id = finsn.getVariableId();
        } else { // instance field, check if the object is shared
          ElementInfo ei = ((InstanceFieldInstruction)insn).getLastElementInfo();
          if (ei.isShared()) {
            id = finsn.getId(ei); 
          }
        }
        
        if (id != null) {
          FieldAccessSequence fs = (FieldAccessSequence) fields.get(id);
          if (fs == null) { // first time
            fs = new FieldAccessSequence(id);
            fields.put(id, fs);
          }
          
          FieldAccess fa = new FieldAccess(ti, finsn);
          fs.addAccess(fa);
     
          if (pendingChanges == null) {
            pendingChanges = new ArrayList(5);
          }
          pendingChanges.add(fs);
          
          if (!fa.hasLockCandidates()) {
            FieldAccess conflict = fa.getConflict();            
            if (conflict != null) {
              raceField = fs;
              
              System.err.println("potential race detected: " + fs.id);
              System.err.println("\t" + fa.describe());
              System.err.println("\t" + conflict.describe());
            }
          }
        }
      }
    }
  }  
}

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

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

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

Modified Files:
	Config.java 
Log Message:
trim property value strings. At least Java 1.4.2 on OS X didn't do this, resulting in
NumberFormatExceptions that caused default values to be used when '-show' pretended to have the right property values (hard to see a blank at the end of the line)

Index: Config.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/Config.java,v
retrieving revision 1.5
retrieving revision 1.6
diff -u -d -r1.5 -r1.6
--- Config.java	8 Jun 2005 23:47:02 -0000	1.5
+++ Config.java	25 Aug 2005 16:55:37 -0000	1.6
@@ -338,6 +338,14 @@
     for (Enumeration keys = keys(); keys.hasMoreElements();) {
       String k = (String) keys.nextElement();
       String v = getProperty(k);
+      
+      // trim heading and trailing blanks (at least Java 1.4.2 does not take care of trailing blanks)
+      String v0 = v;
+      v = v.trim();
+      if (v != v0) {
+        put(k, v);
+      }
+      
       if ("true".equalsIgnoreCase(v) || "t".equalsIgnoreCase(v)
           || "yes".equalsIgnoreCase(v) || "y".equalsIgnoreCase(v)) {
         put(k, "true");

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

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

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

Modified Files:
	IdleFilter.java 
Log Message:
* removed maxStrikes and strikes in idleFilter
* now if we loop too much we call it as suspicious straight away rather
* than let it go maxStrikes times

Index: IdleFilter.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/IdleFilter.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- IdleFilter.java	16 Aug 2005 06:50:21 -0000	1.2
+++ IdleFilter.java	16 Aug 2005 22:27:33 -0000	1.3
@@ -52,128 +52,124 @@
  * 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 class ThreadStat {
-    String tname;
-    int strikes;
-    int backJumps;
-    boolean isCleared = false;
-    
-    int loopStartPc;
-    int loopEndPc;
-    int loopStackDepth;
-    
-    ThreadStat (String tname) {
-      this.tname = tname;
-    }
-  }
-  
-  DynamicObjectArray threadStats = new DynamicObjectArray(16);  
-  ThreadStat ts;
-  
-  int maxStrikes;
-  int maxBackJumps;
-  boolean jumpPast;
-  
-  //----------------------------------------------------- SearchListener interface
 
-  public IdleFilter (Config config) {
-    maxBackJumps = config.getInt("idle.max_backjumps", 500);
-    maxStrikes = config.getInt("idle.max_strikes", 1);
-    jumpPast = config.getBoolean("idle.jump", false);
-  }
-  
-  public void stateAdvanced(Search search) {
-    ts.backJumps = 0;
-    ts.isCleared = false;
-    ts.loopStackDepth = 0;
-    ts.loopStartPc = ts.loopEndPc = 0;
-  }
+	static Logger log = JPF.getLogger("gov.nasa.jpf.tools.IdleFilter");
 
-  public void stateBacktracked(Search search) {
-    ts.strikes = 0;
-    ts.backJumps = 0;
-    ts.isCleared = false;
-    ts.loopStackDepth = 0;
-    ts.loopStartPc = ts.loopEndPc = 0;
-  }
-  
-  //----------------------------------------------------- VMListener interface
-  public void instructionExecuted(VM vm) {
-    JVM jvm = (JVM)vm;
-    Instruction insn = jvm.getLastInstruction();
-    ThreadInfo ti = jvm.getLastThreadInfo();
+	static class ThreadStat {
+		String tname;
+		int backJumps;
+		boolean isCleared = false;
+		int loopStartPc;
+		int loopEndPc;
+		int loopStackDepth;
 
-    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
-            ts.strikes++;
-            
-            if (ts.strikes > maxStrikes) {
+		ThreadStat(String tname) {
+			this.tname = tname;
+		}
+	}
 
-              MethodInfo mi = insn.getMethod();
-              ClassInfo ci = mi.getClassInfo();
-              int line = mi.getLineNumber(insn);
-              String file = ci.getSourceFileName();
+	DynamicObjectArray threadStats = new DynamicObjectArray(16);
+	ThreadStat ts;
+	int maxBackJumps;
+	boolean jumpPast;
 
-              if (jumpPast) {
-                Instruction next = insn.getNext();
-                ti.setPC(next);
+	//----------------------------------------------------- SearchListener interface
 
-                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 + ")");
-              }
-            }
-          }          
-        }
-      }
-      
-    } 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();
+	public IdleFilter(Config config) {
+		maxBackJumps = config.getInt("idle.max_backjumps", 500);
+		jumpPast = config.getBoolean("idle.jump", false);
+	}
+
+	public void stateAdvanced(Search search) {
+		ts.backJumps = 0;
+		ts.isCleared = false;
+		ts.loopStackDepth = 0;
+		ts.loopStartPc = ts.loopEndPc = 0;
+	}
+
+	public void stateBacktracked(Search search) {
+		ts.backJumps = 0;
+		ts.isCleared = false;
+		ts.loopStackDepth = 0;
+		ts.loopStartPc = ts.loopEndPc = 0;
+	}
+
+	//----------------------------------------------------- VMListener interface
+	public void instructionExecuted(VM vm) {
+		JVM jvm = (JVM) vm;
+		Instruction insn = jvm.getLastInstruction();
+		ThreadInfo ti = jvm.getLastThreadInfo();
+
+		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) {
+							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 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 + ")");
+						}
+					}
+				}
+			}
+
+		} 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;
+					}
+				}
+			}
+		}
+	}
 
-        if (stackDepth == ts.loopStackDepth) {
-          if ((pc >= ts.loopStartPc) && (pc < ts.loopEndPc)) {
-            ts.isCleared = true;
-          }
-        }
-      }
-    }      
-  }
-  
 }

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

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

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

Modified Files:
	IdleFilter.java 
Log Message:
tried to refine the IdleFilter heuristics a bit:

(1) we now store the loop bounds/stackdepth, and only shortcut the test if we
have array or invoke insns inside the last loop. This should take care of the
case where we have such insns BEFORE we enter the critical loop, thus cutting it off before it really starts to do it's magic

(2) we now even have an option to jump past the end of the loop, and continue
from there. Sounds dangerous, but hey - we give a warning

(3) added log warnings for both search pruning and jump around

(4) changed the ThreadStat store from a slow HashMap to a thread index based
DynamicObjectArray. Should make things a bit faster

(5) using the ts.IsCleared shortcut in the non-GOTO branch (which is the 
vast majority) should also accelerate things a bit

Index: IdleFilter.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/IdleFilter.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- IdleFilter.java	10 May 2005 06:46:54 -0000	1.1
+++ IdleFilter.java	16 Aug 2005 06:50:21 -0000	1.2
@@ -19,16 +19,21 @@
 package gov.nasa.jpf.tools;
 
 import gov.nasa.jpf.Config;
+import gov.nasa.jpf.JPF;
 import gov.nasa.jpf.Search;
 import gov.nasa.jpf.ListenerAdapter;
 import gov.nasa.jpf.VM;
+import gov.nasa.jpf.jvm.ClassInfo;
 import gov.nasa.jpf.jvm.JVM;
+import gov.nasa.jpf.jvm.MethodInfo;
 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 gov.nasa.jpf.util.DynamicObjectArray;
 
 import java.util.HashMap;
+import java.util.logging.Logger;
 
 /**
  * simple combined listener that checks if a thread seems to do idle loops that might starve
@@ -48,40 +53,51 @@
  */
 public class IdleFilter extends ListenerAdapter {
     
+  static Logger log = JPF.getLogger("gov.nasa.jpf.tools.IdleFilter");
+  
   static class ThreadStat {
     String tname;
     int strikes;
     int backJumps;
     boolean isCleared = false;
     
+    int loopStartPc;
+    int loopEndPc;
+    int loopStackDepth;
+    
     ThreadStat (String tname) {
       this.tname = tname;
     }
   }
   
-  HashMap threadStats = new HashMap();
-  
+  DynamicObjectArray threadStats = new DynamicObjectArray(16);  
   ThreadStat ts;
   
   int maxStrikes;
   int maxBackJumps;
+  boolean jumpPast;
   
   //----------------------------------------------------- SearchListener interface
 
   public IdleFilter (Config config) {
     maxBackJumps = config.getInt("idle.max_backjumps", 500);
     maxStrikes = config.getInt("idle.max_strikes", 1);
+    jumpPast = config.getBoolean("idle.jump", false);
   }
   
   public void stateAdvanced(Search search) {
     ts.backJumps = 0;
     ts.isCleared = false;
+    ts.loopStackDepth = 0;
+    ts.loopStartPc = ts.loopEndPc = 0;
   }
 
   public void stateBacktracked(Search search) {
     ts.strikes = 0;
     ts.backJumps = 0;
     ts.isCleared = false;
+    ts.loopStackDepth = 0;
+    ts.loopStartPc = ts.loopEndPc = 0;
   }
   
   //----------------------------------------------------- VMListener interface
@@ -90,31 +106,74 @@
     Instruction insn = jvm.getLastInstruction();
     ThreadInfo ti = jvm.getLastThreadInfo();
 
-    String tid = ti.getName(); // not ideal, but still better than boxing int's
+    int tid = ti.getIndex();
     ts = (ThreadStat)threadStats.get(tid);
     if (ts == null) {
-      ts = new ThreadStat(tid);
-      threadStats.put(tid, ts);
+      ts = new ThreadStat(ti.getName());
+      threadStats.set(tid,ts);
     }
     
-    if (insn.isBackJump() && !ts.isCleared ) {
+    if (insn.isBackJump()) {
       ts.backJumps++;
+    
+      int loopStackDepth = ti.countStackFrames();
+      int loopPc = jvm.getNextInstruction().getPosition();
       
-      if (ts.backJumps > maxBackJumps) {
-        ti.yield();
-        ts.strikes++;
+      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) {
         
-        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);
+            ti.yield();  // this breaks the executePorStep loop
+            ts.strikes++;
+            
+            if (ts.strikes > maxStrikes) {
+
+              MethodInfo mi = insn.getMethod();
+              ClassInfo ci = mi.getClassInfo();
+              int line = mi.getLineNumber(insn);
+              String file = ci.getSourceFileName();
+
+              if (jumpPast) {
+                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 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 + ")");
+              }
+            }
+          }          
         }
       }
-    } else if (insn instanceof InvokeInstruction) {
-      ts.isCleared=true; // shut it off for this forward
-    } else if (insn instanceof ArrayStoreInstruction) {
-      ts.isCleared=true;
-    }
+      
+    } 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/tools StateSpaceDot.java,1.5,1.6

[Masoud Mansouri-S. <mas...@us...>]

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

Modified Files:
	StateSpaceDot.java 
Log Message:
* Now last output is only added to the second portion of a transition.
   For 2 states s1 and s2 and a transition t1 between them (s1->t1->s2),
   the last output is only added to t1->s2 portion.

Index: StateSpaceDot.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v
retrieving revision 1.5
retrieving revision 1.6
diff -u -d -r1.5 -r1.6
--- StateSpaceDot.java	27 Jun 2005 21:42:09 -0000	1.5
+++ StateSpaceDot.java	12 Aug 2005 22:12:51 -0000	1.6
@@ -196,7 +196,7 @@
   private void endGraph() throws IOException {
     addNode(prev_state);
     if (format==GDF_FORMAT) {
-      graph.write("edgedef>node1,node2,label,labelvisible,directed,thread INT,lastoutput VARCHAR(32)");
+      graph.write("edgedef>node1,node2,label,labelvisible,directed,thread INT");
       graph.newLine();
 
       // Output all the edges that we have accumulated so far
@@ -391,8 +391,7 @@
   private String makeGdfEdgeString(String from_id,
   		                           String to_id,
 								   String label,
-								   int thread,
-								   String lastOutput) {
+								   int thread) {
   	StringBuffer sb=new StringBuffer();
   	sb.append(from_id).append(',').append(to_id).append(',').
 	  append('\"');
@@ -403,10 +402,6 @@
   	}
   	sb.append('\"').append(',').append(labelvisible).append(',').append(true).
 	append(',').append(thread);
-  	lastOutput=replaceString(lastOutput, "\"", "\'\'");
-  	if ((lastOutput!=null) && (!"".equals(lastOutput))) {
-  		sb.append(',').append('\"').append(lastOutput).append('\"');
-  	}
   	replaceString(sb, "\n", "");
   	return sb.toString();
   }
@@ -443,24 +438,25 @@
     if (format==GDF_FORMAT) {
       Transition trans=state.getTransition();
       int thread = trans.getThread();
-      String lastoutput=convertGdfSpecial(trans.getOutput());
       
       // edgedef>node1,node2,label,labelvisible,directed,thread INT
 
-      // Old State -> Transition - labeled with the last output if any.
+      // Old State -> Transition - labeled with the source info if any.
       gdfEdges.add(
       		makeGdfEdgeString("st"+old_id, "tr"+my_id,
       				          makeGdfLabel(state, my_id),
-      				          thread, lastoutput));
+      				          thread));
 
       // Transition node: name,label,style,color
       graph.write("tr" + my_id + ",\"" +my_id+"\","+transition_node_style);
       
       graph.newLine();
-      // Transition -> New State - labeled with the source info if any.
+      // Transition -> New State - labeled with the last output if any.
+      
+      String lastOutputLabel=
+      	replaceString(convertGdfSpecial(trans.getOutput()), "\"", "\'\'");
       gdfEdges.add(
-      		makeGdfEdgeString("tr"+my_id, "st"+new_id, lastoutput, thread,
-      				           lastoutput));
+      	makeGdfEdgeString("tr"+my_id, "st"+new_id, lastOutputLabel, thread));
     } else { // DOT
       graph.write("  st" + old_id + " -> tr" + my_id + ";");
       graph.newLine();

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/search/heuristic ChooseFree.java,1.1.1.1,1.2 DFSHeuristic.java,1.1.1.1,1.2 MostBlocked.java,1.1.1.1,1.2 PreferThreads.java,1.1.1.1,1.2

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

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

Modified Files:
	ChooseFree.java DFSHeuristic.java MostBlocked.java 
	PreferThreads.java 
Log Message:
some more forgotten public modifiers for Heuristic ctors


Index: DFSHeuristic.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/heuristic/DFSHeuristic.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- DFSHeuristic.java	26 Apr 2005 19:44:19 -0000	1.1.1.1
+++ DFSHeuristic.java	10 Aug 2005 16:34:01 -0000	1.2
@@ -28,7 +28,7 @@
   VM vm;
   HeuristicSearch hSearch;
 
-  DFSHeuristic (HeuristicSearch hs) {
+  public DFSHeuristic (HeuristicSearch hs) {
     hSearch = hs;
     vm = hSearch.getVM();
   }

Index: MostBlocked.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/heuristic/MostBlocked.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- MostBlocked.java	26 Apr 2005 19:44:20 -0000	1.1.1.1
+++ MostBlocked.java	10 Aug 2005 16:34:01 -0000	1.2
@@ -29,7 +29,7 @@
 public class MostBlocked implements Heuristic {
   VM vm;
 
-  MostBlocked (HeuristicSearch hSearch) {
+  public MostBlocked (HeuristicSearch hSearch) {
     vm = hSearch.getVM();
   }
 

Index: ChooseFree.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/heuristic/ChooseFree.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- ChooseFree.java	26 Apr 2005 19:44:19 -0000	1.1.1.1
+++ ChooseFree.java	10 Aug 2005 16:34:01 -0000	1.2
@@ -30,7 +30,7 @@
 public class ChooseFree implements Heuristic {
   VM vm;
 
-  ChooseFree (HeuristicSearch hSearch) {
+  public ChooseFree (HeuristicSearch hSearch) {
     vm = hSearch.getVM();
   }
 

Index: PreferThreads.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/heuristic/PreferThreads.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- PreferThreads.java	26 Apr 2005 19:44:20 -0000	1.1.1.1
+++ PreferThreads.java	10 Aug 2005 16:34:01 -0000	1.2
@@ -34,7 +34,7 @@
   VM vm;
   String[] preferredThreads;
 
-  PreferThreads (Config config, HeuristicSearch hSearch) {
+  public PreferThreads (Config config, HeuristicSearch hSearch) {
     vm = hSearch.getVM();
     preferredThreads = config.getStringArray("search.heuristic.preferredThreads");
   }

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

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

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

Modified Files:
	Interleaving.java 
Log Message:
ctor must be public so that we can instantiate via Config


Index: Interleaving.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/heuristic/Interleaving.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- Interleaving.java	26 Apr 2005 19:44:20 -0000	1.1.1.1
+++ Interleaving.java	10 Aug 2005 16:31:39 -0000	1.2
@@ -35,7 +35,7 @@
   VM              vm;
   int             threadHistoryLimit;
 
-  Interleaving (Config config, HeuristicSearch hSearch) {
+  public Interleaving (Config config, HeuristicSearch hSearch) {
     vm = hSearch.getVM();
     search = hSearch;
     

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

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

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

Modified Files:
	Fields.java 
Log Message:
disregard - there's always one debug leftover left..


Index: Fields.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/Fields.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- Fields.java	29 Jul 2005 21:02:26 -0000	1.2
+++ Fields.java	29 Jul 2005 21:09:43 -0000	1.3
@@ -129,7 +129,6 @@
   }
   
   public void setLongValue (int index, long newValue) {
-		int i = index;
 		values[index++] = Types.hiLong(newValue);
     values[index] = Types.loLong(newValue);
   }

[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/jvm ElementInfo.java,1.1.1.1,1.2 Fields.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-serv29252/src/gov/nasa/jpf/jvm

Modified Files:
	ElementInfo.java Fields.java 
Log Message:
fixes rather embarrasing index screwup in ElementInfo when accesing Long/Double array
elements (the index in Fields is int[] based, so it has to be adjusted *2)


Index: Fields.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/Fields.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- Fields.java	26 Apr 2005 19:44:00 -0000	1.1.1.1
+++ Fields.java	29 Jul 2005 21:02:26 -0000	1.2
@@ -129,7 +129,8 @@
   }
   
   public void setLongValue (int index, long newValue) {
-    values[index++] = Types.hiLong(newValue);
+		int i = index;
+		values[index++] = Types.hiLong(newValue);
     values[index] = Types.loLong(newValue);
   }
   

Index: ElementInfo.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ElementInfo.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- ElementInfo.java	26 Apr 2005 19:44:00 -0000	1.1.1.1
+++ ElementInfo.java	29 Jul 2005 21:02:26 -0000	1.2
@@ -518,7 +518,7 @@
 
   public void setLongElement(int index, long value) {
     checkArray(index);
-    cloneFields().setLongValue(index, value);
+    cloneFields().setLongValue(index*2, value);
   }
 
   public int getElement(int index) {
@@ -528,7 +528,7 @@
 
   public long getLongElement(int index) {
     checkArray(index);
-    return fields.getLongValue(index);
+    return fields.getLongValue(index*2);
   }
 
   public void setIndex(int newIndex) {

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

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

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

Modified Files:
	jpf.properties 
Log Message:
fixes rather embarrasing index screwup in ElementInfo when accesing Long/Double array
elements (the index in Fields is int[] based, so it has to be adjusted *2)


Index: jpf.properties
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/jpf.properties,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- jpf.properties	26 Apr 2005 19:43:02 -0000	1.1.1.1
+++ jpf.properties	29 Jul 2005 21:02:25 -0000	1.2
@@ -4,7 +4,7 @@
 
 
 
-# search.class = gov.nasa.jpf.search.heuristic.BFSHeuristic
+# search.class = gov.nasa.jpf.search.heuristic.HeuristicSearch
 # search.heuristic.class = gov.nasa.jpf.search.heuristic.BFSHeuristic
 # search.heuristic.comparator.class = gov.nasa.jpf.search.heuristic.DefaultComparator
 # search.min_free = 1M

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

[Masoud Mansouri-S. <mas...@us...>]

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

Modified Files:
	StateSpaceDot.java 
Log Message:
* Added the program output at the transitions to the edges (only for the
   gdf format). For an edge of the form st1->tr1->st2, the source line is
   included in the label of the first segment (st1->tr1) and the application
   output is added as the label of the second segment (tr1->st2).
* Added a -help option.
* Refactored the code slightly to make it more maintainable.
* Changed the type of the thread number field of edges to be INTs and
   not VARCHAR(32)s.

Index: StateSpaceDot.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v
retrieving revision 1.4
retrieving revision 1.5
diff -u -d -r1.4 -r1.5
--- StateSpaceDot.java	23 Jun 2005 01:10:06 -0000	1.4
+++ StateSpaceDot.java	27 Jun 2005 21:42:09 -0000	1.5
@@ -43,10 +43,11 @@
  * 
  * Options:
  *   -gdf:                Generate the graph in GDF format. The default is DOT.
- *   -transition-numbers: Generate transition numbers
- *   -show-source:        Show source lines.
- *   -labelvisible:       Indicates if the label on the transitions is visible
- *                        (used only with the -gdf option)
+ *   -transition-numbers: Include transition numbers in transition labels.
+ *   -show-source:        Include source lines in transition labels.
+ *   -labelvisible:       Indicates if the label on the transitions is visible (used only with the -gdf option)
+ *   -help:               Prints this help information and stops.
+ * 
  * @date 9/12/03
  * @author Owen O'Malley (Initial version generating the DOT graph)
  * 
@@ -81,6 +82,8 @@
   private static int format=DOT_FORMAT;
   private String out_filename = OUT_FILENAME_NO_EXT+"."+DOT_EXT;
   private static boolean labelvisible=false;
+  private static boolean helpRequested=false;
+
   
   /* In gdf format all the edges must come after all the nodes of the graph
    * are generated. So we first output the nodes as we come across them but
@@ -193,7 +196,7 @@
   private void endGraph() throws IOException {
     addNode(prev_state);
     if (format==GDF_FORMAT) {
-      graph.write("edgedef>node1,node2,label,labelvisible,directed,thread VARCHAR(32)");
+      graph.write("edgedef>node1,node2,label,labelvisible,directed,thread INT,lastoutput VARCHAR(32)");
       graph.newLine();
 
       // Output all the edges that we have accumulated so far
@@ -244,35 +247,11 @@
      
         // We need to precede the dot-specific special characters which appear
         // in the Java source line, such as ']' and '"', with the '\' escape
-        // characters and also to remove any new lines. There seems to be a bug
-        // in Java String's replaceAll() method which does not allow us to use
-        // it to replace the special chars in the source_line string, so here
-        // I am using StringBuffer's replace method to do this - masoud
-     
-        int indexOfNewLine=0;
-        while (indexOfNewLine!=-1) {
-          indexOfNewLine=sb.indexOf("\\n");
-          if (indexOfNewLine!=-1)
-            sb.replace(indexOfNewLine, indexOfNewLine+2, "");
-        }
-     
-        int indexOfBracket=0, lastIndex=0;
-        while (indexOfBracket!=-1) {
-          indexOfBracket=sb.indexOf("]", lastIndex);
-          if (indexOfBracket!=-1) {
-            sb.replace(indexOfBracket, indexOfBracket+1, "\\]");
-            lastIndex=indexOfBracket+2;
-          }
-        }
+        // characters and also to remove any new lines.
      
-        int indexOfQuote=0, lastIndexOfQueote=0;
-        while (indexOfQuote!=-1) {
-          indexOfQuote=sb.indexOf("\"",lastIndexOfQueote);
-          if (indexOfQuote!=-1) {
-            sb.replace(indexOfQuote, indexOfQuote+1, "\\\"");
-            lastIndexOfQueote=indexOfQuote+2;
-          }
-        }
+        replaceString(sb, "\n", "");
+        replaceString(sb, "]", "\\]");
+        replaceString(sb, "\"", "\\\"");
         result.append(sb.toString());
       }
     }
@@ -303,27 +282,59 @@
   	  String source_line=last_trans_step.getSourceRef().getLineString();
   	  if ((source_line != null) && !source_line.equals("")) {
 
-        StringBuffer sb=new StringBuffer(source_line);
-  	     
-  	    // We need to deal with gdf-specific special characters which appear
+  	    // We need to deal with gdf-specific special characters which couls appear
   	    // in the Java source line, such as '"'.
-  	     
-  	    int indexOfQuote=0, lastIndexOfQueote=0;
-  	    while (indexOfQuote!=-1) {
-  	      indexOfQuote=sb.indexOf("\"",lastIndexOfQueote);
- 	      if (indexOfQuote!=-1) {
-  	        sb.replace(indexOfQuote, indexOfQuote+1, "\'\'");
-  	        lastIndexOfQueote=indexOfQuote+2;
-  	      }
-  	    }
-  	     
-  	    result.append(sb.toString());
+  	    result.append(source_line);
+  	  	convertGdfSpecial(result);
   	  }
     }
   	return result.toString();
   }
 
   /**
+   * Locates and replaces all occurrences of a given string with another given
+   * string in an original string buffer. There seems to be a bug in Java
+   * String's replaceAll() method which does not allow us to use it to replace
+   * some special chars so here we use StringBuffer's replace method to do
+   * this.
+   * @param original The original string buffer.
+   * @param from The replaced string.
+   * @param to The replacing string.
+   * @return The original string buffer with the sub-string replaced
+   *         throughout.
+   */
+  private StringBuffer replaceString(StringBuffer original,
+  		                             String from,
+									 String to) {
+    int indexOfReplaced=0, lastIndexOfReplaced=0;
+    while (indexOfReplaced!=-1) {
+      indexOfReplaced=original.indexOf(from,lastIndexOfReplaced);
+      if (indexOfReplaced!=-1) {
+      	original.replace(indexOfReplaced, indexOfReplaced+1, to);
+        lastIndexOfReplaced=indexOfReplaced+to.length();
+      }
+    }
+    return original;
+  }
+  
+  /**
+   * Locates and replaces all occurrences of a given string with another given
+   * string in an original string buffer.
+   * @param original The original string buffer.
+   * @param from The replaced string.
+   * @param to The replacing string.
+   * @return The original string buffer with the sub-string replaced
+   *         throughout.
+   */
+  private String replaceString(String original, String from, String to) {
+  	if ((original!=null) && (from!=null) && (to!=null)) {
+      return replaceString(new StringBuffer(original), from, to).toString();
+  	} else {
+      return original;
+  	}
+  }
+
+  /**
    * Add a new node to the graph with the relevant properties.
    */
   private void addNode(StateInformation state) throws IOException {
@@ -375,25 +386,81 @@
   }
 
   /**
+   * Creates an GDF edge string.
+   */
+  private String makeGdfEdgeString(String from_id,
+  		                           String to_id,
+								   String label,
+								   int thread,
+								   String lastOutput) {
+  	StringBuffer sb=new StringBuffer();
+  	sb.append(from_id).append(',').append(to_id).append(',').
+	  append('\"');
+  	if ((label!=null) && (!"".equals(label))) {
+  		sb.append(label);
+  	} else {
+  		sb.append('-');
+  	}
+  	sb.append('\"').append(',').append(labelvisible).append(',').append(true).
+	append(',').append(thread);
+  	lastOutput=replaceString(lastOutput, "\"", "\'\'");
+  	if ((lastOutput!=null) && (!"".equals(lastOutput))) {
+  		sb.append(',').append('\"').append(lastOutput).append('\"');
+  	}
+  	replaceString(sb, "\n", "");
+  	return sb.toString();
+  }
+
+  /**
+   * GUESS cannot deal with '\n' chars, so remove them. Also convert all '"'
+   * characters to "''".
+   * @param str The string to perform the conversion on.
+   * @return The converted string.
+   */
+  private String convertGdfSpecial(String str) {
+  	if ((str==null) || "".equals(str)) return "";
+  	
+  	StringBuffer sb=new StringBuffer(str);
+  	convertGdfSpecial(sb);
+  	return sb.toString();
+  }
+  
+  /**
+   * GUESS cannot deal with '\n' chars, so replace them with a space. Also
+   * convert all '"' characters to "''".
+   * @param sb The string buffer to perform the conversion on.
+   */
+  private void convertGdfSpecial(StringBuffer sb) {
+  	replaceString(sb, "\"", "\'\'");
+  	replaceString(sb, "\n", " ");
+  }
+
+  /**
    * Create an edge in the graph file from old_id to new_id.
    */
   private void addEdge(int old_id, int new_id, Search state) throws IOException {
     int my_id = edge_id++;
     if (format==GDF_FORMAT) {
-      int thread = state.getTransition().getThread();
-      // edgedef>node1,node2,label,labelvisible,directed,thread VARCHAR(32)
+      Transition trans=state.getTransition();
+      int thread = trans.getThread();
+      String lastoutput=convertGdfSpecial(trans.getOutput());
+      
+      // edgedef>node1,node2,label,labelvisible,directed,thread INT
+
+      // Old State -> Transition - labeled with the last output if any.
+      gdfEdges.add(
+      		makeGdfEdgeString("st"+old_id, "tr"+my_id,
+      				          makeGdfLabel(state, my_id),
+      				          thread, lastoutput));
 
-      // Old State -> Transition. Only this segment is labeled with the source
-      // information.
-      gdfEdges.add("st" + old_id + ",tr" + my_id+",\""+
-      		       makeGdfLabel(state, my_id) +"\","+
-				   labelvisible+",true,"+thread);
       // Transition node: name,label,style,color
       graph.write("tr" + my_id + ",\"" +my_id+"\","+transition_node_style);
+      
       graph.newLine();
-      // Transition -> New State
-      gdfEdges.add("tr" + my_id + ",st" + new_id+",\"" +my_id+
-      		       "\","+labelvisible+",true,"+thread);
+      // Transition -> New State - labeled with the source info if any.
+      gdfEdges.add(
+      		makeGdfEdgeString("tr"+my_id, "st"+new_id, lastoutput, thread,
+      				           lastoutput));
     } else { // DOT
       graph.write("  st" + old_id + " -> tr" + my_id + ";");
       graph.newLine();
@@ -404,6 +471,25 @@
     }
   }
 
+  /**
+   * Show the usage message.
+   */
+  static void showUsage() {
+    System.out
+        .println("Usage: \"java [<vm-options>] gov.nasa.jpf.tools.StateSpaceDot [<graph-options>] [<jpf-options-and-args>]");
+    System.out.println("  <graph-options> : ");
+    System.out.println("    -gdf:                Generate the graph in GDF format. The default is DOT.");
+    System.out.println("    -transition-numbers: Include transition numbers in transition labels.");
+    System.out.println("    -show-source:        Include source lines in transition labels.");
+    System.out.println("    -labelvisible:       Indicates if the label on the transitions is visible (used only with the -gdf option)");
+    System.out.println("    -help:               Prints this help information and stops.");
+    System.out.println("  <jpf-options-and-args>:");
+    System.out.println("    Options and command line arguments passed directly to JPF.");
+    System.out.println("  Note: With -gdf option transition edges could also include program output ");
+    System.out.println("  but in order to enable this JPF's vm.path_output option must be set to ");
+    System.out.println("  true.");
+  }
+
   void filterArgs (String[] args) {
     for (int i=0; i<args.length; i++) {
       String arg = args[i];
@@ -420,14 +506,20 @@
       } else if ("-labelvisible".equals(arg)) {
        	labelvisible=true;
         args[i] = null;      	
+      } else if  ("-help".equals(args[i])) {
+      	showUsage();
+      	helpRequested=true;
       }
     }    
   }
-
+  
   public static void main(String [] args) {
     StateSpaceDot listener = new StateSpaceDot();
     listener.filterArgs(args);
-
+    if (helpRequested==true) {
+    	return;
+    }
+    
     Config conf = JPF.createConfig(args);
     // do own settings here
 

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

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

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

Modified Files:
	JPF_java_io_RandomAccessFile.java 
Log Message:
* fixed problem with RandomAccessFile not working for multiple 
* accesses to the same file

Index: JPF_java_io_RandomAccessFile.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/env/jvm/gov/nasa/jpf/jvm/JPF_java_io_RandomAccessFile.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- JPF_java_io_RandomAccessFile.java	26 Apr 2005 19:43:26 -0000	1.1.1.1
+++ JPF_java_io_RandomAccessFile.java	23 Jun 2005 20:50:06 -0000	1.2
@@ -19,6 +19,8 @@
 
 package gov.nasa.jpf.jvm;
 
+import java.util.HashMap;
+
 /**
  * MJI NativePeer class for java.io.RandomAccessFile library abstraction
  *
@@ -26,6 +28,28 @@
  */
 public class JPF_java_io_RandomAccessFile {
 
+	// need to see whether the file is already in use
+	// if so, then we'll update the file data and length in the original file
+	// we do update the length in the local object, but not the data
+		
+	static HashMap File2DataMap = new HashMap();
+	
+	// get the mapped object if one exists
+	private static int getMapping(MJIEnv env, int this_ptr) {
+		int fn_ptr = env.getReferenceField(this_ptr,"filename");
+		Object o = File2DataMap.get(new Integer(fn_ptr));
+		if (o == null)
+			return this_ptr;
+		return ((Integer)o).intValue();
+	}
+	
+	// set the mapping during the constructor call
+	public static void setDataMap(MJIEnv env, int this_ptr) {
+		int fn_ptr = env.getReferenceField(this_ptr,"filename");
+		if (!File2DataMap.containsKey(new Integer(fn_ptr))) 
+			File2DataMap.put(new Integer(fn_ptr),new Integer(this_ptr));
+	}
+	
   public static void writeByte(MJIEnv env, int this_ptr, int data) {
     long current_posn = env.getLongField(this_ptr, current_position);
     long current_len = env.getLongField(this_ptr, current_length);
@@ -37,6 +61,8 @@
     env.setLongField(this_ptr, current_position, current_posn);
     if (current_posn >= current_len) {
       env.setLongField(this_ptr, current_length, current_posn + 1);
+      // update length in the mapped object if it exists
+      env.setLongField(getMapping(env,this_ptr), current_length, current_posn + 1);
     }
   }
 
@@ -58,6 +84,8 @@
       env.setLongField(this_ptr, current_position, len);
     }
     env.setLongField(this_ptr, current_length, len);
+    // update length in the mapped object if it exists
+    env.setLongField(getMapping(env,this_ptr), current_length, current_posn + 1);
   }
 
   public static int read(MJIEnv env, int this_ptr, int data_array,
@@ -105,6 +133,9 @@
 
   private static int findDataChunk(MJIEnv env, int this_ptr, long position,
                                    int chunk_size) {
+  	
+  	//check if the file data is mapped, use mapped this_ptr if it exists
+  	this_ptr = getMapping(env,this_ptr);  	
     int prev_obj = MJIEnv.NULL;
     int cur_obj = env.getReferenceField(this_ptr, data_root);
     long chunk_idx = position/chunk_size;

[Javapathfinder-devel] javapathfinder/env/jpf/java/io RandomAccessFile.java,1.1.1.1,1.2

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

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

Modified Files:
	RandomAccessFile.java 
Log Message:
* fixed problem with RandomAccessFile not working for multiple 
* accesses to the same file

Index: RandomAccessFile.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/env/jpf/java/io/RandomAccessFile.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- RandomAccessFile.java	26 Apr 2005 19:43:25 -0000	1.1.1.1
+++ RandomAccessFile.java	23 Jun 2005 20:49:05 -0000	1.2
@@ -30,6 +30,7 @@
     filename = name;
     isOpen = true;
     isReadOnly = "r".equals(permissions);
+    setDataMap();
   }
 
   public void seek(long posn) throws IOException {
@@ -40,6 +41,8 @@
     return currentLength;
   }
 
+  public native void setDataMap();
+  
   public native void writeByte(int data) throws IOException;
 
   public native void write(byte[] data, int start, int len

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

[Masoud Mansouri-S. <mas...@us...>]

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

Modified Files:
	StateSpaceDot.java 
Log Message:
- Added transition nodes rather than using just edges for transitions.
   We need multiple transitions between two states which GUESS/GDF
   cannot handle at the moment so rather than st0->st1, we now have
   st0->tr0->st1. The source line information is on the label of the first segment (st0->tr0). The (tr0->st1) is labeled with the transition number only. By default labels are set to be invisible. Must use -labelvisible option to generate the graph with visible transition labels otherwise when GUESS is run you can use "g.edges.labelvisible=true" from the GUESS Jython command line.
- stateRestored() method was modified to solve a bug that I discovered
  which caused wrong edges to be drawn when BFS HeuristicSearch was
  used. Willem found and suggested the fix.


Index: StateSpaceDot.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v
retrieving revision 1.3
retrieving revision 1.4
diff -u -d -r1.3 -r1.4
--- StateSpaceDot.java	21 Jun 2005 00:07:19 -0000	1.3
+++ StateSpaceDot.java	23 Jun 2005 01:10:06 -0000	1.4
@@ -58,20 +58,34 @@
   private static final String GDF_EXT = "gdf";
   private static final String OUT_FILENAME_NO_EXT = "jpf-state-space";
 
+  // NODE styles constants
+  private static final int RECTABGLE = 1;
+  private static final int ELLIPSE   = 2;
+  private static final int ROUND_RECTABGLE = 3;
+  private static final int RECTABGLE_WITH_TEXT = 4;
+  private static final int ELLIPSE_WITH_TEXT = 5;
+  private static final int ROUND_RECTABGLE_WITH_TEXT = 6;
+
+  // State and transition node styles used
+  private static final int state_node_style=ELLIPSE_WITH_TEXT;
+  private static final int transition_node_style=RECTABGLE_WITH_TEXT;
+
+  // File formats supported
+  private static final int DOT_FORMAT=0;
+  private static final int GDF_FORMAT=1;
+
   private BufferedWriter graph = null;
   private int edge_id = 0;
   private static boolean transition_numbers=false;
   private static boolean show_source=false;
-  private static int DOT_FORMAT=0;
-  private static int GDF_FORMAT=1;
-  private int format=DOT_FORMAT;
+  private static int format=DOT_FORMAT;
   private String out_filename = OUT_FILENAME_NO_EXT+"."+DOT_EXT;
-  private boolean labelvisible=false;
-
-  /* In gdf format all the edges must come after all the nodes of the graph are
-   * generated. So we first output the nodes as come across them but we store
-   * the strings for edges in the gdfEdges list and output them when the
-   * search ends.
+  private static boolean labelvisible=false;
+  
+  /* In gdf format all the edges must come after all the nodes of the graph
+   * are generated. So we first output the nodes as we come across them but
+   * we store the strings for edges in the gdfEdges list and output them when
+   * the search ends.
    */
   ArrayList gdfEdges=new ArrayList();
 
@@ -112,7 +126,7 @@
   }
 
   public void stateRestored (Search search) {
-   // N/A
+    prev_state.reset(search.getStateNumber(), false, false);
   }
 
   public void stateProcessed (Search search) {
@@ -172,22 +186,26 @@
   }
 
   /**
-   * Put the footer for the graph into the file.
+   * In the case of the DOT graph it is just adding the final "}" at the end.
+   * In the case of GPF format we must output edge definition and all the
+   * edges that we have found.
    */
   private void endGraph() throws IOException {
     addNode(prev_state);
     if (format==GDF_FORMAT) {
       graph.write("edgedef>node1,node2,label,labelvisible,directed,thread VARCHAR(32)");
+      graph.newLine();
+
+      // Output all the edges that we have accumulated so far
+      int size=gdfEdges.size();
+  	  for (int i=0; i<size; i++) {
+  		graph.write((String) gdfEdges.get(i));
+  	    graph.newLine();
+  	  }
     } else {
       graph.write("}");
+      graph.newLine();
     }
-    graph.newLine();
-	// Output all the edges that we have accumulated so far
-	int size=gdfEdges.size();
-	for (int i=0; i<size; i++) {
-		graph.write((String) gdfEdges.get(i));
-	    graph.newLine();
-	}
     graph.close();
   }
 
@@ -270,7 +288,7 @@
     if (trans == null) {
   	  return "-init-";
   	}
-
+    
   	StringBuffer result = new StringBuffer();
 
   	if (transition_numbers) {
@@ -315,7 +333,7 @@
         if (state.error != null) {
           graph.write(":" + state.error);
         }
-        graph.write("\",5");
+        graph.write("\","+state_node_style);
         if (state.error != null) {
             graph.write(",red");
           } else if (state.has_next) {
@@ -364,9 +382,18 @@
     if (format==GDF_FORMAT) {
       int thread = state.getTransition().getThread();
       // edgedef>node1,node2,label,labelvisible,directed,thread VARCHAR(32)
-      gdfEdges.add("st" + old_id + ",st" + new_id+
-                   ",\"" + makeGdfLabel(state, my_id)+"\","+
-                   labelvisible+",true,"+thread);
+
+      // Old State -> Transition. Only this segment is labeled with the source
+      // information.
+      gdfEdges.add("st" + old_id + ",tr" + my_id+",\""+
+      		       makeGdfLabel(state, my_id) +"\","+
+				   labelvisible+",true,"+thread);
+      // Transition node: name,label,style,color
+      graph.write("tr" + my_id + ",\"" +my_id+"\","+transition_node_style);
+      graph.newLine();
+      // Transition -> New State
+      gdfEdges.add("tr" + my_id + ",st" + new_id+",\"" +my_id+
+      		       "\","+labelvisible+",true,"+thread);
     } else { // DOT
       graph.write("  st" + old_id + " -> tr" + my_id + ";");
       graph.newLine();

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

[Masoud Mansouri-S. <mas...@us...>]

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

Modified Files:
	StateSpaceDot.java 
Log Message:
* Extended this to also support gdf format used by GUESS from HP
   - http://www.hpl.hp.com/research/idl/projects/graphs/.
   This tool can handle graphs of much larger size than GraphViz could
    handle. You can zoom in and out and interact with the graph using
    a Python like notation. E.g., coloring edges based on thread numbers,
    finding and making visible only the path between 2 specific states, etc.
   The graph is stored in a file called "jpf-state-space.<extension>"
    where is ".dot" or ".gdf". By default it generates a DOT graph as
    before. Options added:
       -gdf:     Generate the graph in GDF format. The default is DOT.
       -labelvisible:       Indicates if the label on the transitions is visible
                                 (used only with the -gdf option)

Index: StateSpaceDot.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -d -r1.2 -r1.3
--- StateSpaceDot.java	14 Jun 2005 19:43:08 -0000	1.2
+++ StateSpaceDot.java	21 Jun 2005 00:07:19 -0000	1.3
@@ -30,23 +30,50 @@
 import java.io.FileWriter;
 import java.io.IOException;
 import java.util.Iterator;
-
+import java.util.ArrayList;
 
 /*
- * Add an state space observer to JPF and build a DOT graph of the state space
- * that is explored by JPF. The graph is stored in "./jpf-state-space.dot".
- *
+ * Add a state space observer to JPF and build a graph of the state space
+ * that is explored by JPF. The graph can be generated in different formats.
+ * The current formats that are supported are DOT (visualized by a tool
+ * like GraphViz from ATT - http://www.graphviz.org/) and gdf (used by GUESS
+ * from HP - http://www.hpl.hp.com/research/idl/projects/graphs/).
+ * The graph is stored in a file called "jpf-state-space.<extension>" where
+ * extension is ".dot" or ".gdf". By default it generates a DOT graph.
+ * 
+ * Options:
+ *   -gdf:                Generate the graph in GDF format. The default is DOT.
+ *   -transition-numbers: Generate transition numbers
+ *   -show-source:        Show source lines.
+ *   -labelvisible:       Indicates if the label on the transitions is visible
+ *                        (used only with the -gdf option)
  * @date 9/12/03
- *
- * @author Owen O'Malley
+ * @author Owen O'Malley (Initial version generating the DOT graph)
+ * 
+ * @date 7/17/05
+ * @author Masoud Mansouri-Samani (Extended to also generate the gdf graph)
  */
-
 public class StateSpaceDot implements SearchListener {
-  private static final String GRAPH_FILENAME = "jpf-state-space.dot";
+  private static final String DOT_EXT = "dot";
+  private static final String GDF_EXT = "gdf";
+  private static final String OUT_FILENAME_NO_EXT = "jpf-state-space";
+
   private BufferedWriter graph = null;
   private int edge_id = 0;
   private static boolean transition_numbers=false;
   private static boolean show_source=false;
+  private static int DOT_FORMAT=0;
+  private static int GDF_FORMAT=1;
+  private int format=DOT_FORMAT;
+  private String out_filename = OUT_FILENAME_NO_EXT+"."+DOT_EXT;
+  private boolean labelvisible=false;
+
+  /* In gdf format all the edges must come after all the nodes of the graph are
+   * generated. So we first output the nodes as come across them but we store
+   * the strings for edges in the gdfEdges list and output them when the
+   * search ends.
+   */
+  ArrayList gdfEdges=new ArrayList();
 
   private StateInformation prev_state = null;
 
@@ -69,9 +96,11 @@
     boolean has_next =search.hasNextState();
     boolean is_new = search.isNewState();
     try {
-      graph.write("/* searchAdvanced(" + id + ", " + makeLabel(search, id) +
+      if (format==DOT_FORMAT) {
+        graph.write("/* searchAdvanced(" + id + ", " + makeDotLabel(search, id) +
                     ", " + has_next + ") */");
-      graph.newLine();
+        graph.newLine();
+      }
       if (prev_state != null) {
         addEdge(prev_state.id, id, search);
       } else {
@@ -83,26 +112,30 @@
   }
 
   public void stateRestored (Search search) {
-    // N/A
+   // N/A
   }
-  
+
   public void stateProcessed (Search search) {
-    // nothing to do
+   // nothing to do
   }
-  
+
   public void stateBacktracked(Search search) {
     try {
       addNode(prev_state);
       prev_state.reset(search.getStateNumber(), false, false);
-      graph.write("/* searchBacktracked(" + prev_state + ") */");
-      graph.newLine();
+      if (format==DOT_FORMAT) {
+        graph.write("/* searchBacktracked(" + prev_state + ") */");
+        graph.newLine();
+      }
     } catch (IOException e) {}
   }
 
   public void searchConstraintHit(Search search) {
     try {
-      graph.write("/* searchConstraintHit(" + search.getStateNumber() + ") */");
-      graph.newLine();
+      if (format==DOT_FORMAT) {
+        graph.write("/* searchConstraintHit(" + search.getStateNumber() + ") */");
+        graph.newLine();
+      }
     } catch (IOException e) {}
   }
   
@@ -116,20 +149,26 @@
   }
 
   public void propertyViolated(Search search) {
-    try {
-      prev_state.error = getErrorMsg(search);
-      graph.write("/* propertyViolated(" + search.getStateNumber() + ") */");
-      graph.newLine();
-    } catch (IOException e) {}
+	try {
+	  prev_state.error = getErrorMsg(search);
+	  if (format==DOT_FORMAT) {
+	    graph.write("/* propertyViolated(" + search.getStateNumber() + ") */");
+	    graph.newLine();
+	  }
+	} catch (IOException e) {}
   }
 
   /**
    * Put the header for the graph into the file.
    */
   private void beginGraph() throws IOException {
-    graph = new BufferedWriter(new FileWriter(GRAPH_FILENAME));
-    graph.write("digraph jpf_state_space {");
-    graph.newLine();
+	graph = new BufferedWriter(new FileWriter(out_filename));
+	if (format==GDF_FORMAT) {
+	  graph.write("nodedef>name,label,style,color");
+	} else { // dot
+	  graph.write("digraph jpf_state_space {");
+	}
+	graph.newLine();
   }
 
   /**
@@ -137,15 +176,25 @@
    */
   private void endGraph() throws IOException {
     addNode(prev_state);
-    graph.write("}");
+    if (format==GDF_FORMAT) {
+      graph.write("edgedef>node1,node2,label,labelvisible,directed,thread VARCHAR(32)");
+    } else {
+      graph.write("}");
+    }
     graph.newLine();
+	// Output all the edges that we have accumulated so far
+	int size=gdfEdges.size();
+	for (int i=0; i<size; i++) {
+		graph.write((String) gdfEdges.get(i));
+	    graph.newLine();
+	}
     graph.close();
   }
 
   /**
    * Return the string that will be used to label this state for the user.
    */
-  private String makeLabel(Search state, int my_id) {
+  private String makeDotLabel(Search state, int my_id) {
     Transition trans = state.getTransition();
     if (trans == null) {
       return "-init-";
@@ -174,21 +223,21 @@
         result.append("\\n");
 
         StringBuffer sb=new StringBuffer(source_line);
-        
+     
         // We need to precede the dot-specific special characters which appear
         // in the Java source line, such as ']' and '"', with the '\' escape
         // characters and also to remove any new lines. There seems to be a bug
         // in Java String's replaceAll() method which does not allow us to use
         // it to replace the special chars in the source_line string, so here
         // I am using StringBuffer's replace method to do this - masoud
-        
+     
         int indexOfNewLine=0;
         while (indexOfNewLine!=-1) {
           indexOfNewLine=sb.indexOf("\\n");
           if (indexOfNewLine!=-1)
-        	  sb.replace(indexOfNewLine, indexOfNewLine+2, "");
+            sb.replace(indexOfNewLine, indexOfNewLine+2, "");
         }
-        
+     
         int indexOfBracket=0, lastIndex=0;
         while (indexOfBracket!=-1) {
           indexOfBracket=sb.indexOf("]", lastIndex);
@@ -197,7 +246,7 @@
             lastIndex=indexOfBracket+2;
           }
         }
-        
+     
         int indexOfQuote=0, lastIndexOfQueote=0;
         while (indexOfQuote!=-1) {
           indexOfQuote=sb.indexOf("\"",lastIndexOfQueote);
@@ -206,7 +255,6 @@
             lastIndexOfQueote=indexOfQuote+2;
           }
         }
-        
         result.append(sb.toString());
       }
     }
@@ -215,23 +263,81 @@
   }
 
   /**
+   * Return the string that will be used to label this state in the GDF graph.
+   */
+  private String makeGdfLabel(Search state, int my_id) {
+    Transition trans = state.getTransition();
+    if (trans == null) {
+  	  return "-init-";
+  	}
+
+  	StringBuffer result = new StringBuffer();
+
+  	if (transition_numbers) {
+  	  result.append(my_id);
+  	  result.append(":");
+  	}
+
+  	TransitionStep last_trans_step = trans.getLastTransitionStep();
+  	result.append(last_trans_step.getSourceRef().toString());
+
+  	if (show_source) {
+  	  String source_line=last_trans_step.getSourceRef().getLineString();
+  	  if ((source_line != null) && !source_line.equals("")) {
+
+        StringBuffer sb=new StringBuffer(source_line);
+  	     
+  	    // We need to deal with gdf-specific special characters which appear
+  	    // in the Java source line, such as '"'.
+  	     
+  	    int indexOfQuote=0, lastIndexOfQueote=0;
+  	    while (indexOfQuote!=-1) {
+  	      indexOfQuote=sb.indexOf("\"",lastIndexOfQueote);
+ 	      if (indexOfQuote!=-1) {
+  	        sb.replace(indexOfQuote, indexOfQuote+1, "\'\'");
+  	        lastIndexOfQueote=indexOfQuote+2;
+  	      }
+  	    }
+  	     
+  	    result.append(sb.toString());
+  	  }
+    }
+  	return result.toString();
+  }
+
+  /**
    * Add a new node to the graph with the relevant properties.
    */
   private void addNode(StateInformation state) throws IOException {
     if (state.is_new) {
-      graph.write("  st" + state.id + " [label=\"" + state.id);
-      if (state.error != null) {
-        graph.write(":" + state.error);
-      }
-      graph.write("\",shape=");
-      if (state.error != null) {
-        graph.write("diamond,color=red");
-      } else if (state.has_next) {
-        graph.write("circle,color=black");
-      } else {
-        graph.write("egg,color=green");
+      if (format==GDF_FORMAT) {
+        graph.write("st" + state.id + ",\"" + state.id);
+        if (state.error != null) {
+          graph.write(":" + state.error);
+        }
+        graph.write("\",5");
+        if (state.error != null) {
+            graph.write(",red");
+          } else if (state.has_next) {
+            graph.write(",black");
+          } else {
+            graph.write(",green");
+          }
+      } else { // The dot version
+        graph.write("  st" + state.id + " [label=\"" + state.id);
+        if (state.error != null) {
+          graph.write(":" + state.error);
+        }
+        graph.write("\",shape=");
+        if (state.error != null) {
+          graph.write("diamond,color=red");
+        } else if (state.has_next) {
+          graph.write("circle,color=black");
+        } else {
+          graph.write("egg,color=green");
+        }
+        graph.write("];");
       }
-      graph.write("];");
       graph.newLine();
     }
   }
@@ -255,14 +361,20 @@
    */
   private void addEdge(int old_id, int new_id, Search state) throws IOException {
     int my_id = edge_id++;
-    graph.write("  st" + old_id + " -> tr" + my_id + ";");
-    graph.newLine();
-    graph.write("  tr" + my_id +
-                  " [label=\"" + makeLabel(state, my_id) +
+    if (format==GDF_FORMAT) {
+      int thread = state.getTransition().getThread();
+      // edgedef>node1,node2,label,labelvisible,directed,thread VARCHAR(32)
+      gdfEdges.add("st" + old_id + ",st" + new_id+
+                   ",\"" + makeGdfLabel(state, my_id)+"\","+
+                   labelvisible+",true,"+thread);
+    } else { // DOT
+      graph.write("  st" + old_id + " -> tr" + my_id + ";");
+      graph.newLine();
+      graph.write("  tr" + my_id + " [label=\"" + makeDotLabel(state, my_id) +
                   "\",shape=box]");
-    graph.newLine();
-    graph.write("  tr" + my_id + " -> st" + new_id + ";");
-    graph.newLine();
+      graph.newLine();
+      graph.write("  tr" + my_id + " -> st" + new_id + ";");
+    }
   }
 
   void filterArgs (String[] args) {
@@ -274,23 +386,27 @@
       } else if ("-show-source".equals(arg)) {
         show_source = true;
         args[i] = null;
+      } else if ("-gdf".equals(arg)) {
+        format=GDF_FORMAT;
+        out_filename=OUT_FILENAME_NO_EXT+"."+GDF_EXT;
+        args[i] = null;
+      } else if ("-labelvisible".equals(arg)) {
+       	labelvisible=true;
+        args[i] = null;      	
       }
     }    
   }
-  
+
   public static void main(String [] args) {
     StateSpaceDot listener = new StateSpaceDot();
     listener.filterArgs(args);
-    
+
     Config conf = JPF.createConfig(args);
     // do own settings here
-    
+
     JPF jpf = new JPF(conf);
     jpf.addSearchListener(listener);
 
     jpf.run();
   }
 }
-
-
-

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

[Masoud Mansouri-S. <mas...@us...>]

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

Modified Files:
	StateSpaceDot.java 
Log Message:
* Fixed a bug which appears when the show_source option is used. The
  Java source line may contain dot-specific special characters. We need
  to precede those (e.g., ']' and '"') with the '\' escape character. There
  seems to be a bug in Java String's replaceAll() method which does not
  allow us to use it so I used the more combersome StringBuffer's replace
  method to do this.


Index: StateSpaceDot.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- StateSpaceDot.java	26 Apr 2005 19:44:22 -0000	1.1.1.1
+++ StateSpaceDot.java	14 Jun 2005 19:43:08 -0000	1.2
@@ -172,7 +172,42 @@
       String source_line=last_trans_step.getSourceRef().getLineString();
       if ((source_line != null) && !source_line.equals("")) {
         result.append("\\n");
-        result.append(source_line.replaceAll("\\n", ""));
+
+        StringBuffer sb=new StringBuffer(source_line);
+        
+        // We need to precede the dot-specific special characters which appear
+        // in the Java source line, such as ']' and '"', with the '\' escape
+        // characters and also to remove any new lines. There seems to be a bug
+        // in Java String's replaceAll() method which does not allow us to use
+        // it to replace the special chars in the source_line string, so here
+        // I am using StringBuffer's replace method to do this - masoud
+        
+        int indexOfNewLine=0;
+        while (indexOfNewLine!=-1) {
+          indexOfNewLine=sb.indexOf("\\n");
+          if (indexOfNewLine!=-1)
+        	  sb.replace(indexOfNewLine, indexOfNewLine+2, "");
+        }
+        
+        int indexOfBracket=0, lastIndex=0;
+        while (indexOfBracket!=-1) {
+          indexOfBracket=sb.indexOf("]", lastIndex);
+          if (indexOfBracket!=-1) {
+            sb.replace(indexOfBracket, indexOfBracket+1, "\\]");
+            lastIndex=indexOfBracket+2;
+          }
+        }
+        
+        int indexOfQuote=0, lastIndexOfQueote=0;
+        while (indexOfQuote!=-1) {
+          indexOfQuote=sb.indexOf("\"",lastIndexOfQueote);
+          if (indexOfQuote!=-1) {
+            sb.replace(indexOfQuote, indexOfQuote+1, "\\\"");
+            lastIndexOfQueote=indexOfQuote+2;
+          }
+        }
+        
+        result.append(sb.toString());
       }
     }
 

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

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

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

Modified Files:
	SourceRef.java 
Log Message:
trying a bit harder in case we don't have sources. It now prints out at least what sources are missing. Note that there is still the vm.report.show_missing_lines, which goes beyond that by printing executed insns (too many options, <sigh>)

Index: SourceRef.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/util/SourceRef.java,v
retrieving revision 1.1.1.1
retrieving revision 1.2
diff -u -d -r1.1.1.1 -r1.2
--- SourceRef.java	26 Apr 2005 19:44:24 -0000	1.1.1.1
+++ SourceRef.java	9 Jun 2005 19:54:54 -0000	1.2
@@ -91,6 +91,10 @@
     return true;
   }
 
+  public String getFileName () {
+    return fileName;
+  }
+    
   public void set (SourceRef sr) {
     fileName = sr.fileName;
     line = sr.line;