--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/vm/GenericSharednessPolicy.java	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,614 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+
+package gov.nasa.jpf.vm;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.JPF;
+import gov.nasa.jpf.SystemAttribute;
+import gov.nasa.jpf.util.FieldSpecMatcher;
+import gov.nasa.jpf.util.JPFLogger;
+import gov.nasa.jpf.util.MethodSpecMatcher;
+import gov.nasa.jpf.util.TypeSpecMatcher;
+import gov.nasa.jpf.vm.choice.ThreadChoiceFromSet;
+
+/**
+ * an abstract SharednessPolicy implementation that makes use of both
+ * shared field access CGs and exposure CGs.
+ * 
+ * This class is highly configurable, both in terms of using exposure CGs and filters.
+ * The *never_break filters should be used with care to avoid missing defects, especially
+ * the (transitive) method filters.
+ * NOTE - the default settings from jpf-core/jpf.properties include several
+ * java.util.concurrent* and java.lang.* fields/methods that can in fact contribute to
+ * concurrency defects, esp. in SUTs that explicitly use Thread/ThreadGroup objects, in
+ * which case they should be removed.
+ * 
+ * The *always_break field filter should only be used for white box SUT analysis if JPF
+ * fails to detect sharedness (e.g. because no exposure is used). This should only
+ * go into application property files
+ */
+public abstract class GenericSharednessPolicy implements SharednessPolicy, Attributor {
+  
+  //--- auxiliary types to configure filters
+  static class NeverBreakIn implements SystemAttribute {
+    static NeverBreakIn singleton = new NeverBreakIn();
+  } 
+  static class NeverBreakOn implements SystemAttribute {
+    static NeverBreakOn singleton = new NeverBreakOn();
+  } 
+  static class AlwaysBreakOn implements SystemAttribute {
+    static AlwaysBreakOn singleton = new AlwaysBreakOn();
+  } 
+  
+  protected static JPFLogger logger = JPF.getLogger("shared");
+  
+  
+  //--- options used for concurrent field access detection
+  
+  protected TypeSpecMatcher neverBreakOnTypes;
+  
+  protected TypeSpecMatcher alwaysBreakOnTypes;
+  
+  /**
+   * never break or expose if a matching method is on the stack
+   */
+  protected MethodSpecMatcher neverBreakInMethods;
+  
+  /**
+   * never break on matching fields 
+   */  
+  protected FieldSpecMatcher neverBreakOnFields;
+    
+  /**
+   * always break matching fields, no matter if object is already shared or not
+   */  
+  protected FieldSpecMatcher alwaysBreakOnFields;
+  
+
+  /**
+   * do we break on final field access 
+   */
+  protected boolean skipFinals;
+  protected boolean skipConstructedFinals;
+  protected boolean skipStaticFinals;
+  
+  /**
+   * do we break inside of constructors
+   * (note that 'this' references could leak from ctors, but
+   * this is rather unusual)
+   */
+  protected boolean skipInits;
+
+  /**
+   * do we add CGs for objects that could become shared, e.g. when storing
+   * a reference to a non-shared object in a shared object field.
+   * NOTE: this is a conservative measure since we don't know yet at the
+   * point of exposure if the object will ever be shared, which means it
+   * can cause state explosion.
+   */
+  protected boolean breakOnExposure;
+  
+  /**
+   * options to filter out lock protected field access, which is not
+   * supposed to cause shared CGs
+   * (this has no effect on exposure though)
+   */
+  protected boolean useSyncDetection;
+  protected int lockThreshold;  
+  
+  protected VM vm;
+  
+  
+  protected GenericSharednessPolicy (Config config){
+    neverBreakInMethods = MethodSpecMatcher.create( config.getStringArray("vm.shared.never_break_methods"));
+    
+    neverBreakOnTypes = TypeSpecMatcher.create(config.getStringArray("vm.shared.never_break_types"));
+    alwaysBreakOnTypes = TypeSpecMatcher.create(config.getStringArray("vm.shared.always_break_types"));
+    
+    neverBreakOnFields = FieldSpecMatcher.create( config.getStringArray("vm.shared.never_break_fields"));
+    alwaysBreakOnFields = FieldSpecMatcher.create( config.getStringArray("vm.shared.always_break_fields"));
+    
+    skipFinals = config.getBoolean("vm.shared.skip_finals", true);
+    skipConstructedFinals = config.getBoolean("vm.shared.skip_constructed_finals", false);
+    skipStaticFinals = config.getBoolean("vm.shared.skip_static_finals", true);
+    skipInits = config.getBoolean("vm.shared.skip_inits", true);
+    
+    breakOnExposure = config.getBoolean("vm.shared.break_on_exposure", true);
+    
+    useSyncDetection = config.getBoolean("vm.shared.sync_detection", true);
+    lockThreshold = config.getInt("vm.shared.lockthreshold", 5);  
+  }
+  
+  //--- internal methods (potentially overridden by subclass)
+  
+  
+  //--- attribute management
+
+  protected void setTypeAttributes (TypeSpecMatcher neverMatcher, TypeSpecMatcher alwaysMatcher, ClassInfo ciLoaded){
+    // we flatten this for performance reasons
+    for (ClassInfo ci = ciLoaded; ci!= null; ci = ci.getSuperClass()){
+      if (alwaysMatcher != null && alwaysMatcher.matches(ci)){
+        ciLoaded.addAttr(AlwaysBreakOn.singleton);
+        return;
+      }
+      if (neverMatcher != null && neverMatcher.matches(ci)){
+        ciLoaded.addAttr( NeverBreakOn.singleton);
+        return;
+      }
+    }
+  }
+  
+  protected void setFieldAttributes (FieldSpecMatcher neverMatcher, FieldSpecMatcher alwaysMatcher, ClassInfo ci){
+    for (FieldInfo fi : ci.getDeclaredInstanceFields()) {
+      // invisible fields (created by compiler)
+      if (fi.getName().startsWith("this$")) {
+        fi.addAttr( NeverBreakOn.singleton);
+        continue;
+      }        
+
+      // configuration
+      if (neverMatcher != null && neverMatcher.matches(fi)) {
+        fi.addAttr( NeverBreakOn.singleton);
+      }
+      if (alwaysMatcher != null && alwaysMatcher.matches(fi)) {
+        fi.addAttr( AlwaysBreakOn.singleton);
+      }
+      
+      // annotation
+      if (fi.hasAnnotation("gov.nasa.jpf.annotation.NeverBreak")){
+        fi.addAttr( NeverBreakOn.singleton);        
+      }
+    }
+
+    for (FieldInfo fi : ci.getDeclaredStaticFields()) {
+      // invisible fields (created by compiler)
+      if ("$assertionsDisabled".equals(fi.getName())) {
+        fi.addAttr( NeverBreakOn.singleton);
+        continue;
+      }
+
+      // configuration
+      if (neverMatcher != null && neverMatcher.matches(fi)) {
+        fi.addAttr( NeverBreakOn.singleton);
+      }
+      if (alwaysMatcher != null && alwaysMatcher.matches(fi)) {
+        fi.addAttr( AlwaysBreakOn.singleton);
+      }
+      
+      // annotation
+      if (fi.hasAnnotation("gov.nasa.jpf.annotation.NeverBreak")){
+        fi.addAttr( NeverBreakOn.singleton);        
+      }
+    }
+  }
+  
+  protected boolean isInNeverBreakMethod (ThreadInfo ti){
+    for (StackFrame frame = ti.getTopFrame(); frame != null; frame=frame.getPrevious()){
+      MethodInfo mi = frame.getMethodInfo();
+      if (mi.hasAttr( NeverBreakIn.class)){
+        return true;
+      }
+    }
+
+    return false;
+  }
+  
+  protected abstract boolean checkOtherRunnables (ThreadInfo ti);
+  
+  // this needs a three-way return value, hence Boolean
+  protected Boolean canHaveSharednessCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
+    //--- thread
+    if (ti.isFirstStepInsn()){ // no empty transitions
+      return Boolean.FALSE;
+    }
+    
+    if (!checkOtherRunnables(ti)){ // nothing to reschedule
+      return Boolean.FALSE;
+    }
+    
+    if (ti.hasAttr( NeverBreakIn.class)){
+      return Boolean.FALSE;
+    }
+    
+    //--- method
+    if (isInNeverBreakMethod(ti)){
+      return false;
+    }
+    
+    //--- type
+    ClassInfo ciFieldOwner = eiFieldOwner.getClassInfo();
+    if (ciFieldOwner.hasAttr(NeverBreakOn.class)){
+      return Boolean.FALSE;
+    }
+    if (ciFieldOwner.hasAttr(AlwaysBreakOn.class)){
+      return Boolean.TRUE;
+    }
+    
+    //--- field
+    if (fi != null){
+      if (fi.hasAttr(AlwaysBreakOn.class)) {
+        return Boolean.TRUE;
+      }
+      if (fi.hasAttr(NeverBreakOn.class)) {
+        return Boolean.FALSE;
+      }
+    }
+    
+    return null;    
+  }
+
+  //--- FieldLockInfo management
+  
+  /**
+   * static attribute filters that determine if the check..Access() and check..Exposure() methods should be called.
+   * This is only called once per instruction execution since it filters all cases that would set a CG.
+   * Filter conditions have to apply to both field access and object exposure.
+   */
+  protected abstract FieldLockInfo createFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi);
+
+  
+  /**
+   * generic version of FieldLockInfo update, which relies on FieldLockInfo implementation to determine
+   * if ElementInfo needs to be cloned
+   */  
+  protected ElementInfo updateFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
+    FieldLockInfo fli = ei.getFieldLockInfo(fi);
+    if (fli == null){
+      fli = createFieldLockInfo(ti, ei, fi);
+      ei = ei.getModifiableInstance();
+      ei.setFieldLockInfo(fi, fli);
+      
+    } else {
+      FieldLockInfo newFli = fli.checkProtection(ti, ei, fi);
+      if (newFli != fli) {
+        ei = ei.getModifiableInstance();
+        ei.setFieldLockInfo(fi,newFli);
+      }
+    }
+    
+    return ei;
+  }
+  
+  
+  //--- runnable computation & CG creation
+
+  // NOTE - we don't schedule threads outside this process since field access if process local
+  
+  protected ThreadInfo[] getRunnables (ApplicationContext appCtx){
+    return vm.getThreadList().getProcessTimeoutRunnables(appCtx);
+  }
+  
+  protected ChoiceGenerator<ThreadInfo> getRunnableCG (String id, ThreadInfo tiCurrent){
+    if (vm.getSystemState().isAtomic()){ // no CG if we are in a atomic section
+      return null;
+    }
+    
+    ThreadInfo[] choices = getRunnables(tiCurrent.getApplicationContext());
+    if (choices.length <= 1){ // field access doesn't block, i.e. the current thread is always runnable
+      return null;
+    }
+    
+    return new ThreadChoiceFromSet( id, choices, true);
+  }
+  
+  protected boolean setNextChoiceGenerator (ChoiceGenerator<ThreadInfo> cg){
+    if (cg != null){
+      return vm.getSystemState().setNextChoiceGenerator(cg); // listeners could still remove CGs
+    }
+    
+    return false;
+  }
+  
+  
+  //--- internal policy methods that can be overridden by subclasses
+  
+  protected ElementInfo updateSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
+    ThreadInfoSet tis = ei.getReferencingThreads();
+    ThreadInfoSet newTis = tis.add(ti);
+    
+    if (tis != newTis){
+      ei = ei.getModifiableInstance();
+      ei.setReferencingThreads(newTis);
+    }
+      
+    // we only change from non-shared to shared
+    if (newTis.isShared(ti, ei) && !ei.isShared() && !ei.isSharednessFrozen()) {
+      ei = ei.getModifiableInstance();
+      ei.setShared(ti, true);
+    }
+
+    if (ei.isShared() && fi != null){
+      ei = updateFieldLockInfo(ti,ei,fi);
+    }
+    
+    return ei;
+  }
+
+  protected boolean setsExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){
+    if (breakOnExposure){
+      ClassInfo ciExposed = eiExposed.getClassInfo();
+      
+      //--- exposed type
+      if (ciExposed.hasAttr(NeverBreakOn.class)){
+        return false;
+      }      
+      if (ciExposed.hasAttr(AlwaysBreakOn.class)){
+        logger.info("type exposure CG setting field ", fi, " to ", eiExposed);
+        return setNextChoiceGenerator(getRunnableCG("EXPOSE", ti));
+      }        
+        
+      // we can't filter on immutability since the race subject could be a reference
+      // that is exposed through the exposed object
+      
+      if (isInNeverBreakMethod(ti)){
+        return false;
+      }
+      
+      if (eiFieldOwner.isExposedOrShared() && isFirstExposure(eiFieldOwner, eiExposed)){        
+        // don't check against the 'old' field value because this might get called after the field was already updated
+        // we should solely depend on different object sharedness
+        eiExposed = eiExposed.getExposedInstance(ti, eiFieldOwner);
+        logger.info("exposure CG setting field ", fi, " to ", eiExposed);
+        return setNextChoiceGenerator(getRunnableCG("EXPOSE", ti));
+      }
+    }
+
+    return false;
+  }
+
+  protected boolean isFirstExposure (ElementInfo eiFieldOwner, ElementInfo eiExposed){
+    if (!eiExposed.isImmutable()){
+      if (!eiExposed.isExposedOrShared()) {
+         return (eiFieldOwner.isExposedOrShared());
+      }
+    }
+        
+    return false;
+  }
+
+  
+  //------------------------------------------------ Attributor interface
+    
+  /**
+   * this can be used to initializeSharednessPolicy per-application mechanisms such as ClassInfo attribution
+   */
+  @Override
+  public void initializeSharednessPolicy (VM vm, ApplicationContext appCtx){
+    this.vm = vm;
+    
+    SystemClassLoaderInfo sysCl = appCtx.getSystemClassLoader();
+    sysCl.addAttributor(this);
+  }
+  
+  
+  @Override
+  public void setAttributes (ClassInfo ci){
+    setTypeAttributes( neverBreakOnTypes, alwaysBreakOnTypes, ci);
+    
+    setFieldAttributes( neverBreakOnFields, alwaysBreakOnFields, ci);
+    
+    // this one is more expensive to iterate over and should be avoided
+    if (neverBreakInMethods != null){
+      for (MethodInfo mi : ci.getDeclaredMethods().values()){
+        if (neverBreakInMethods.matches(mi)){
+          mi.setAttr( NeverBreakIn.singleton);
+        }
+      }
+    }
+    
+  }
+    
+  //------------------------------------------------ SharednessPolicy interface
+  
+  @Override
+  public ElementInfo updateObjectSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
+    return updateSharedness(ti, ei, fi);
+  }
+  @Override
+  public ElementInfo updateClassSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
+    return updateSharedness(ti, ei, fi);
+  }
+  @Override
+  public ElementInfo updateArraySharedness (ThreadInfo ti, ElementInfo ei, int idx){
+    // NOTE - we don't support per-element FieldLockInfos (yet)
+    return updateSharedness(ti, ei, null);
+  }
+
+  
+  /**
+   * check to determine if call site, object/class attributes and thread execution state
+   * could cause CGs. This is called before sharedness is updated, i.e. can be used to
+   * filter objects/classes that should not be sharedness tracked
+   */
+  @Override
+  public boolean canHaveSharedObjectCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
+    Boolean ret = canHaveSharednessCG( ti, insn, eiFieldOwner, fi);
+    if (ret != null){
+      return ret;
+    }
+    
+    if  (eiFieldOwner.isImmutable()){
+      return false;
+    }
+    
+    if (skipFinals && fi.isFinal()){
+      return false;
+    }
+        
+    //--- mixed (dynamic) attributes
+    if (skipConstructedFinals && fi.isFinal() && eiFieldOwner.isConstructed()){
+      return false;
+    }
+    
+    if (skipInits && insn.getMethodInfo().isInit()){
+      return false;
+    }
+    
+    return true;
+  }
+  
+  @Override
+  public boolean canHaveSharedClassCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
+    Boolean ret = canHaveSharednessCG( ti, insn, eiFieldOwner, fi);
+    if (ret != null){
+      return ret;
+    }
+
+    if  (eiFieldOwner.isImmutable()){
+      return false;
+    }
+    
+    if (skipStaticFinals && fi.isFinal()){
+      return false;
+    }
+
+    // call site. This could be transitive, in which case it has to be dynamic and can't be moved to isRelevant..()
+    MethodInfo mi = insn.getMethodInfo();
+    if (mi.isClinit() && (fi.getClassInfo() == mi.getClassInfo())) {
+      // clinits are all synchronized, so they are lock protected per se
+      return false;
+    }
+    
+    return true;
+  }
+  
+  @Override
+  public boolean canHaveSharedArrayCG (ThreadInfo ti, Instruction insn, ElementInfo eiArray, int idx){
+    Boolean ret = canHaveSharednessCG( ti, insn, eiArray, null);
+    if (ret != null){
+      return ret;
+    }
+
+    // more array specific checks here
+    
+    return true;
+  }
+  
+  
+  /**
+   * <2do> explain why not transitive
+   * 
+   * these are the public interfaces towards FieldInstructions. Callers have to be aware this will 
+   * change the /referenced/ ElementInfo in case the respective object becomes exposed
+   */
+  @Override
+  public boolean setsSharedObjectCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
+    if (eiFieldOwner.getClassInfo().hasAttr(AlwaysBreakOn.class) ||
+            (eiFieldOwner.isShared() && !eiFieldOwner.isLockProtected(fi))) {
+      logger.info("CG accessing shared instance field ", fi);
+      return setNextChoiceGenerator( getRunnableCG("SHARED_OBJECT", ti));
+    }
+    
+    return false;
+  }
+
+  @Override
+  public boolean setsSharedClassCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
+    if (eiFieldOwner.getClassInfo().hasAttr(AlwaysBreakOn.class) ||
+            (eiFieldOwner.isShared() && !eiFieldOwner.isLockProtected(fi))) {
+      logger.info("CG accessing shared static field ", fi);
+      return setNextChoiceGenerator( getRunnableCG("SHARED_CLASS", ti));
+    }
+    
+    return false;
+  }
+  
+  @Override
+  public boolean setsSharedArrayCG (ThreadInfo ti, Instruction insn, ElementInfo eiArray, int index){
+    if (eiArray.isShared()){
+      // <2do> we should check lock protection for the whole array here
+      logger.info("CG accessing shared array ", eiArray);
+      return setNextChoiceGenerator( getRunnableCG("SHARED_ARRAY", ti));
+    }
+    
+    return false;
+  }
+
+  
+  //--- internal policy methods that can be overridden by subclasses
+    
+  protected boolean isRelevantStaticFieldAccess (ThreadInfo ti, Instruction insn, ElementInfo ei, FieldInfo fi){
+    if (!ei.isShared()){
+      return false;
+    }
+    
+    if  (ei.isImmutable()){
+      return false;
+    }
+    
+    if (skipStaticFinals && fi.isFinal()){
+      return false;
+    }    
+    
+    if (!ti.hasOtherRunnables()){ // nothing to break for
+      return false;
+    }
+
+    // call site. This could be transitive, in which case it has to be dynamic and can't be moved to isRelevant..()
+    MethodInfo mi = insn.getMethodInfo();
+    if (mi.isClinit() && (fi.getClassInfo() == mi.getClassInfo())) {
+      // clinits are all synchronized, so they are lock protected per se
+      return false;
+    }
+    
+    return true;
+  }
+
+  
+  protected boolean isRelevantArrayAccess (ThreadInfo ti, Instruction insn, ElementInfo ei, int index){
+    // <2do> this is too simplistic, we should support filters for array objects
+    
+    if (!ti.hasOtherRunnables()){
+      return false;
+    }
+    
+    if (!ei.isShared()){
+      return false;
+    }
+    
+    if (ti.isFirstStepInsn()){ // we already did break
+      return false;
+    }
+
+    return true;
+  }
+  
+  //--- object exposure 
+
+  // <2do> explain why not transitive
+  
+  @Override
+  public boolean setsSharedObjectExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){
+    return setsExposureCG(ti,insn,eiFieldOwner,fi,eiExposed);
+  }
+
+  @Override
+  public boolean setsSharedClassExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){
+    return setsExposureCG(ti,insn,eiFieldOwner,fi,eiExposed);
+  }  
+
+  // since exposure is about the object being exposed (the element), there is no separate setsSharedArrayExposureCG
+  
+  
+  @Override
+  public void cleanupThreadTermination(ThreadInfo ti) {
+    // default action is to do nothing
+  }
+
+}