src/main/gov/nasa/jpf/vm/FieldLockInfo.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.vm;
  19
  20 import gov.nasa.jpf.JPF;
  21
  22 import java.util.logging.Logger;
  23
  24 /**
  25  * class encapsulating the lock protection status for field access
  26  * instructions. Used by on-the-fly partial order reduction in FieldInstruction
  27  * to determine if a GET/PUT_FIELD/STATIC insn has to be treated as a
  28  * boundary step (terminates a transition). If the field access is always
  29  * protected by a lock, only the corresponding sync (INVOKExx or MONITORENTER)
  30  * are boundary steps, thus the number of states can be significantly reduced.
  31  *
  32  * FieldLockInfos are only used if vm.por.sync_detection is set
  33  *
  34  * NOTE this might involve assumptions that can be violated in subsequent
  35  * paths, and might cause potential races to go undetected
  36  */
  37 public abstract class FieldLockInfo implements Cloneable  {
  38
  39   static Logger log = JPF.getLogger("gov.nasa.jpf.vm.FieldLockInfo");
  40
  41   static protected final FieldLockInfo empty = new EmptyFieldLockInfo();
  42
  43   protected ThreadInfo tiLastCheck; // the thread this FieldLockInfo was last checked for
  44
  45   public static FieldLockInfo getEmptyFieldLockInfo(){
  46     return empty;
  47   }
  48
  49   public abstract FieldLockInfo checkProtection (ThreadInfo ti, ElementInfo ei, FieldInfo fi);
  50   public abstract boolean isProtected ();
  51
  52   public abstract FieldLockInfo cleanUp (Heap heap);
  53   protected abstract int[] getCandidateLockSet();
  54
  55   public boolean isFinal() {
  56     return isProtected();
  57   }
  58
  59   public boolean needsPindown (ElementInfo ei) {
  60     return false;
  61   }
  62
  63
  64   /*
  65    * we need this for faster instantiation. Make sure it gets overridden in
  66    * case there is a need for per-instance parameterization
  67    */
  68   @Override
  69   public Object clone () throws CloneNotSupportedException {
  70     return super.clone();
  71   }
  72
  73   void lockAssumptionFailed (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
  74     String src = ti.getTopFrameMethodInfo().getClassInfo().getSourceFileName();
  75     int line = ti.getLine();
  76
  77     StringBuilder sb = new StringBuilder( "unprotected field access of: ");
  78     sb.append(ei);
  79     sb.append('.');
  80     sb.append(fi.getName());
  81     sb.append( " in thread: ");
  82     sb.append( ti.getName());
  83     sb.append( " (");
  84     sb.append( src);
  85     sb.append(':');
  86     sb.append(line);
  87     sb.append(")\n[SEVERE].. last lock candidates: ");
  88     appendLockSet(sb, getCandidateLockSet());
  89     if (tiLastCheck != null) {
  90       sb.append(" set by ");
  91       sb.append(tiLastCheck);
  92     }
  93     sb.append( "\n[SEVERE].. current locks: ");
  94     appendLockSet(sb, ti.getLockedObjectReferences());
  95     sb.append("\n[SEVERE].. if this is not a race, re-run with 'vm.shared.sync_detection=false' or exclude field from checks");
  96
  97     log.severe(sb.toString());
  98   }
  99
 100   void appendLockSet (StringBuilder sb, int[] lockSet) {
 101     Heap heap = VM.getVM().getHeap();
 102
 103     if ((lockSet == null) || (lockSet.length == 0)) {
 104       sb.append( "{}");
 105     } else {
 106       sb.append('{');
 107       for (int i=0; i<lockSet.length;) {
 108         int ref = lockSet[i];
 109         if (ref != MJIEnv.NULL) {
 110           ElementInfo ei = heap.get(ref);
 111           if (ei != null) {
 112             sb.append(ei);
 113           } else {
 114             sb.append("?@");
 115             sb.append(lockSet[i]);
 116           }
 117         }
 118         i++;
 119         if (i<lockSet.length) sb.append(',');
 120       }
 121       sb.append('}');
 122     }
 123   }
 124
 125 }
 126
 127 /**
 128  * FieldLockSet implementation for fields that are terminally considered to be unprotected
 129  */
 130 class EmptyFieldLockInfo extends FieldLockInfo {
 131
 132   @Override
 133   public FieldLockInfo checkProtection (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
 134     return this;
 135   }
 136
 137   @Override
 138   public FieldLockInfo cleanUp (Heap heap) {
 139     return this;
 140   }
 141
 142   @Override
 143   public boolean isProtected () {
 144     return false;
 145   }
 146
 147   @Override
 148   public boolean isFinal() {
 149     return true;
 150   }
 151
 152   @Override
 153   protected int[] getCandidateLockSet() {
 154     return new int[0];
 155   }
 156
 157   @Override
 158   public String toString() {
 159     return "EmptyFieldLockInfo";
 160   }
 161 }
 162