Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/listener/NonSharedChecker.java @ 26:4eb191cbb68c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Mon, 04 May 2015 22:10:33 -0700
parents
children
comparison
equal deleted inserted replaced
25:3517702bd768 26:4eb191cbb68c
1 /*
2 * Copyright (C) 2015, 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.listener;
19
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;
36
37 /**
38 *
39 */
40 public class NonSharedChecker extends ListenerAdapter {
41
42 boolean throwOnCycle = false;
43
44 static class Access {
45 ThreadInfo ti;
46 Access prev;
47
48 Access(ThreadInfo ti, Access prev){
49 this.ti = ti;
50 this.prev = prev;
51 }
52
53 // <2do> get a better hashCode for state hashing
54 public int hashCode() {
55 int h = ti.getId();
56 for (Access p = prev; p!= null; p = p.prev){
57 h = 31*h + p.ti.getId();
58 }
59 return h;
60 }
61 // but we don't care for equals()
62 }
63
64 public NonSharedChecker (Config conf){
65 throwOnCycle = conf.getBoolean("nonshared.throw_on_cycle");
66 }
67
68 boolean isNonShared(ElementInfo ei){
69 ClassInfo ci = ei.getClassInfo();
70 return (ci.getAnnotation("gov.nasa.jpf.annotation.NonShared") != null);
71 }
72
73 boolean checkLiveCycles (ElementInfo ei, ThreadInfo ti, Access ac){
74 if (ti == ac.ti){
75 return true; // Ok, fine - no need to record
76
77 } else {
78 boolean foundLiveOne = false;
79 for (Access a = ac; a != null; a = a.prev){
80 ThreadInfo t = a.ti;
81 if (t == ti){ // cycle detected
82 return !foundLiveOne;
83 }
84 foundLiveOne = (foundLiveOne || t.isAlive()); // <2do> maybe we should check for non-blocked threads
85 }
86
87 // new one, record it in the access history of the object
88 ac = new Access(ti, ac);
89 ei = ei.getModifiableInstance();
90 ei.setObjectAttr(ac);
91 }
92
93 return true;
94 }
95
96
97 @Override
98 public void executeInstruction (VM vm, ThreadInfo ti, Instruction insn){
99
100 ElementInfo ei = null;
101
102 if (ti.isFirstStepInsn()) {
103 return;
104 }
105
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();
117 if (ref != -1){
118 ei = ti.getElementInfo(ref);
119 }
120 } else if (insn instanceof ALOAD){
121 StackFrame frame = ti.getTopFrame();
122 int ref = frame.getLocalVariable(((ALOAD)insn).getLocalVariableIndex());
123 if (ref != -1){
124 ei = ti.getElementInfo(ref);
125 }
126 }
127
128 if (ei != null){
129 Access ac = ei.getObjectAttr(Access.class);
130 if (ac != null){
131 if (!checkLiveCycles(ei,ti,ac)){
132 StringBuilder sb = new StringBuilder("NonShared object: ");
133 sb.append( ei);
134 sb.append(" accessed in live thread cycle: ");
135 sb.append( ti.getName());
136 for (Access a = ac; a != null; a = a.prev ){
137 sb.append(',');
138 sb.append(a.ti.getName());
139 }
140 String msg = sb.toString();
141
142 if (throwOnCycle){
143 ti.setNextPC( ti.createAndThrowException("java.lang.AssertionError", msg));
144 } else {
145 System.err.println("WARNING: " + msg);
146 System.err.println("\tat " + insn.getSourceLocation());
147 }
148 return;
149 }
150 }
151 }
152 }
153
154 @Override
155 public void objectCreated (VM vm, ThreadInfo ti, ElementInfo ei){
156 if (isNonShared(ei)){
157 ei.setObjectAttrNoClone(new Access(ti, null));
158 }
159 }
160 }
161