2 * Copyright (C) 2015, 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.listener;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.ListenerAdapter;
22 import gov.nasa.jpf.vm.ClassInfo;
23 import gov.nasa.jpf.vm.ElementInfo;
24 import gov.nasa.jpf.vm.VM;
25 import gov.nasa.jpf.vm.ThreadInfo;
26 import gov.nasa.jpf.jvm.bytecode.ALOAD;
27 import gov.nasa.jpf.jvm.bytecode.ARETURN;
28 import gov.nasa.jpf.jvm.bytecode.ASTORE;
29 import gov.nasa.jpf.jvm.bytecode.IFNONNULL;
30 import gov.nasa.jpf.jvm.bytecode.IFNULL;
31 import gov.nasa.jpf.vm.bytecode.InstanceFieldInstruction;
32 import gov.nasa.jpf.vm.Instruction;
33 import gov.nasa.jpf.jvm.bytecode.MONITORENTER;
34 import gov.nasa.jpf.jvm.bytecode.VirtualInvocation;
35 import gov.nasa.jpf.vm.StackFrame;
40 public class NonSharedChecker extends ListenerAdapter {
42 boolean throwOnCycle = false;
48 Access(ThreadInfo ti, Access prev){
53 // <2do> get a better hashCode for state hashing
54 public int hashCode() {
56 for (Access p = prev; p!= null; p = p.prev){
57 h = 31*h + p.ti.getId();
61 // but we don't care for equals()
64 public NonSharedChecker (Config conf){
65 throwOnCycle = conf.getBoolean("nonshared.throw_on_cycle");
68 boolean isNonShared(ElementInfo ei){
69 ClassInfo ci = ei.getClassInfo();
70 return (ci.getAnnotation("gov.nasa.jpf.annotation.NonShared") != null);
73 boolean checkLiveCycles (ElementInfo ei, ThreadInfo ti, Access ac){
75 return true; // Ok, fine - no need to record
78 boolean foundLiveOne = false;
79 for (Access a = ac; a != null; a = a.prev){
81 if (t == ti){ // cycle detected
84 foundLiveOne = (foundLiveOne || t.isAlive()); // <2do> maybe we should check for non-blocked threads
87 // new one, record it in the access history of the object
88 ac = new Access(ti, ac);
89 ei = ei.getModifiableInstance();
98 public void executeInstruction (VM vm, ThreadInfo ti, Instruction insn){
100 ElementInfo ei = null;
102 if (ti.isFirstStepInsn()) {
106 if (insn instanceof InstanceFieldInstruction){
107 ei = ((InstanceFieldInstruction)insn).peekElementInfo(ti);
108 } else if (insn instanceof VirtualInvocation){
109 ei = ((VirtualInvocation)insn).getThisElementInfo(ti); // Outch - that's expensive
110 } else if (insn instanceof MONITORENTER ||
111 insn instanceof ASTORE ||
112 insn instanceof ARETURN ||
113 insn instanceof IFNONNULL ||
114 insn instanceof IFNULL) {
115 StackFrame frame = ti.getTopFrame();
116 int ref = frame.peek();
118 ei = ti.getElementInfo(ref);
120 } else if (insn instanceof ALOAD){
121 StackFrame frame = ti.getTopFrame();
122 int ref = frame.getLocalVariable(((ALOAD)insn).getLocalVariableIndex());
124 ei = ti.getElementInfo(ref);
129 Access ac = ei.getObjectAttr(Access.class);
131 if (!checkLiveCycles(ei,ti,ac)){
132 StringBuilder sb = new StringBuilder("NonShared object: ");
134 sb.append(" accessed in live thread cycle: ");
135 sb.append( ti.getName());
136 for (Access a = ac; a != null; a = a.prev ){
138 sb.append(a.ti.getName());
140 String msg = sb.toString();
143 ti.setNextPC( ti.createAndThrowException("java.lang.AssertionError", msg));
145 System.err.println("WARNING: " + msg);
146 System.err.println("\tat " + insn.getSourceLocation());
155 public void objectCreated (VM vm, ThreadInfo ti, ElementInfo ei){
156 if (isNonShared(ei)){
157 ei.setObjectAttrNoClone(new Access(ti, null));