Mercurial > hg > Members > kono > jpf-core

annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
26
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
1 /*
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
2 * Copyright (C) 2015, United States Government, as represented by the
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
3 * Administrator of the National Aeronautics and Space Administration.
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
4 * All rights reserved.
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
5 *
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
8 * in compliance with the License. You may obtain a copy of the License at
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
9 *
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
10 * http://www.apache.org/licenses/LICENSE-2.0.
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
11 *
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
12 * Unless required by applicable law or agreed to in writing, software
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
13 * distributed under the License is distributed on an "AS IS" BASIS,
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
15 * See the License for the specific language governing permissions and
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
16 * limitations under the License.
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
17 */
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
18 package gov.nasa.jpf.listener;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
19
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
20 import gov.nasa.jpf.Config;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
21 import gov.nasa.jpf.ListenerAdapter;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
22 import gov.nasa.jpf.vm.ClassInfo;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
23 import gov.nasa.jpf.vm.ElementInfo;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
24 import gov.nasa.jpf.vm.VM;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
25 import gov.nasa.jpf.vm.ThreadInfo;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
26 import gov.nasa.jpf.jvm.bytecode.ALOAD;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
27 import gov.nasa.jpf.jvm.bytecode.ARETURN;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
28 import gov.nasa.jpf.jvm.bytecode.ASTORE;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
29 import gov.nasa.jpf.jvm.bytecode.IFNONNULL;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
30 import gov.nasa.jpf.jvm.bytecode.IFNULL;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
31 import gov.nasa.jpf.vm.bytecode.InstanceFieldInstruction;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
32 import gov.nasa.jpf.vm.Instruction;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
33 import gov.nasa.jpf.jvm.bytecode.MONITORENTER;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
34 import gov.nasa.jpf.jvm.bytecode.VirtualInvocation;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
35 import gov.nasa.jpf.vm.StackFrame;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
36
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
37 /**
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
38 *
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
39 */
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
40 public class NonSharedChecker extends ListenerAdapter {
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
41
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
42 boolean throwOnCycle = false;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
43
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
44 static class Access {
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
45 ThreadInfo ti;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
46 Access prev;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
47
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
48 Access(ThreadInfo ti, Access prev){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
49 this.ti = ti;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
50 this.prev = prev;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
51 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
52
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
53 // <2do> get a better hashCode for state hashing
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
54 public int hashCode() {
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
55 int h = ti.getId();
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
56 for (Access p = prev; p!= null; p = p.prev){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
57 h = 31*h + p.ti.getId();
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
58 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
59 return h;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
60 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
61 // but we don't care for equals()
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
62 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
63
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
64 public NonSharedChecker (Config conf){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
65 throwOnCycle = conf.getBoolean("nonshared.throw_on_cycle");
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
66 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
67
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
68 boolean isNonShared(ElementInfo ei){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
69 ClassInfo ci = ei.getClassInfo();
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
70 return (ci.getAnnotation("gov.nasa.jpf.annotation.NonShared") != null);
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
71 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
72
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
73 boolean checkLiveCycles (ElementInfo ei, ThreadInfo ti, Access ac){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
74 if (ti == ac.ti){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
75 return true; // Ok, fine - no need to record
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
76
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
77 } else {
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
78 boolean foundLiveOne = false;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
79 for (Access a = ac; a != null; a = a.prev){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
80 ThreadInfo t = a.ti;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
81 if (t == ti){ // cycle detected
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
82 return !foundLiveOne;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
83 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
84 foundLiveOne = (foundLiveOne || t.isAlive()); // <2do> maybe we should check for non-blocked threads
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
85 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
86
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
87 // new one, record it in the access history of the object
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
88 ac = new Access(ti, ac);
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
89 ei = ei.getModifiableInstance();
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
90 ei.setObjectAttr(ac);
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
91 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
92
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
93 return true;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
94 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
95
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
96
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
97 @Override
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
98 public void executeInstruction (VM vm, ThreadInfo ti, Instruction insn){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
99
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
100 ElementInfo ei = null;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
101
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
102 if (ti.isFirstStepInsn()) {
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
103 return;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
104 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
105
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
106 if (insn instanceof InstanceFieldInstruction){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
107 ei = ((InstanceFieldInstruction)insn).peekElementInfo(ti);
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
108 } else if (insn instanceof VirtualInvocation){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
109 ei = ((VirtualInvocation)insn).getThisElementInfo(ti); // Outch - that's expensive
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
110 } else if (insn instanceof MONITORENTER ||
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
111 insn instanceof ASTORE ||
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
112 insn instanceof ARETURN ||
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
113 insn instanceof IFNONNULL ||
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
114 insn instanceof IFNULL) {
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
115 StackFrame frame = ti.getTopFrame();
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
116 int ref = frame.peek();
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
117 if (ref != -1){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
118 ei = ti.getElementInfo(ref);
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
119 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
120 } else if (insn instanceof ALOAD){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
121 StackFrame frame = ti.getTopFrame();
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
122 int ref = frame.getLocalVariable(((ALOAD)insn).getLocalVariableIndex());
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
123 if (ref != -1){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
124 ei = ti.getElementInfo(ref);
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
125 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
126 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
127
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
128 if (ei != null){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
129 Access ac = ei.getObjectAttr(Access.class);
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
130 if (ac != null){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
131 if (!checkLiveCycles(ei,ti,ac)){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
132 StringBuilder sb = new StringBuilder("NonShared object: ");
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
133 sb.append( ei);
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
134 sb.append(" accessed in live thread cycle: ");
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
135 sb.append( ti.getName());
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
136 for (Access a = ac; a != null; a = a.prev ){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
137 sb.append(',');
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
138 sb.append(a.ti.getName());
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
139 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
140 String msg = sb.toString();
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
141
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
142 if (throwOnCycle){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
143 ti.setNextPC( ti.createAndThrowException("java.lang.AssertionError", msg));
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
144 } else {
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
145 System.err.println("WARNING: " + msg);
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
146 System.err.println("\tat " + insn.getSourceLocation());
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
147 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
148 return;
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
149 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
150 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
151 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
152 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
153
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
154 @Override
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
155 public void objectCreated (VM vm, ThreadInfo ti, ElementInfo ei){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
156 if (isNonShared(ei)){
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
157 ei.setObjectAttrNoClone(new Access(ti, null));
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
158 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
159 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
160 }
4eb191cbb68c moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic
Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
parents:
diff changeset
161