2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.vm;
20 import gov.nasa.jpf.JPF;
22 import java.util.logging.Logger;
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.
32 * FieldLockInfos are only used if vm.por.sync_detection is set
34 * NOTE this might involve assumptions that can be violated in subsequent
35 * paths, and might cause potential races to go undetected
37 public abstract class FieldLockInfo implements Cloneable {
39 static Logger log = JPF.getLogger("gov.nasa.jpf.vm.FieldLockInfo");
41 static protected final FieldLockInfo empty = new EmptyFieldLockInfo();
43 protected ThreadInfo tiLastCheck; // the thread this FieldLockInfo was last checked for
45 public static FieldLockInfo getEmptyFieldLockInfo(){
49 public abstract FieldLockInfo checkProtection (ThreadInfo ti, ElementInfo ei, FieldInfo fi);
50 public abstract boolean isProtected ();
52 public abstract FieldLockInfo cleanUp (Heap heap);
53 protected abstract int[] getCandidateLockSet();
55 public boolean isFinal() {
59 public boolean needsPindown (ElementInfo ei) {
65 * we need this for faster instantiation. Make sure it gets overridden in
66 * case there is a need for per-instance parameterization
69 public Object clone () throws CloneNotSupportedException {
73 void lockAssumptionFailed (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
74 String src = ti.getTopFrameMethodInfo().getClassInfo().getSourceFileName();
75 int line = ti.getLine();
77 StringBuilder sb = new StringBuilder( "unprotected field access of: ");
80 sb.append(fi.getName());
81 sb.append( " in thread: ");
82 sb.append( ti.getName());
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);
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");
97 log.severe(sb.toString());
100 void appendLockSet (StringBuilder sb, int[] lockSet) {
101 Heap heap = VM.getVM().getHeap();
103 if ((lockSet == null) || (lockSet.length == 0)) {
107 for (int i=0; i<lockSet.length;) {
108 int ref = lockSet[i];
109 if (ref != MJIEnv.NULL) {
110 ElementInfo ei = heap.get(ref);
115 sb.append(lockSet[i]);
119 if (i<lockSet.length) sb.append(',');
128 * FieldLockSet implementation for fields that are terminally considered to be unprotected
130 class EmptyFieldLockInfo extends FieldLockInfo {
133 public FieldLockInfo checkProtection (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
138 public FieldLockInfo cleanUp (Heap heap) {
143 public boolean isProtected () {
148 public boolean isFinal() {
153 protected int[] getCandidateLockSet() {
158 public String toString() {
159 return "EmptyFieldLockInfo";