# HG changeset patch # User Peter Mehlitz # Date 1430802633 25200 # Node ID 4eb191cbb68c2546b289d07f9eee12aa9976922d # Parent 3517702bd76802e09e747ca0469f9dca27a925cc moved NonShared + checker listener over from old jpf-aprop. Note this is still a JVM specific listener but it could be VM agnostic diff -r 3517702bd768 -r 4eb191cbb68c src/annotations/gov/nasa/jpf/annotation/NonShared.java --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/annotations/gov/nasa/jpf/annotation/NonShared.java Mon May 04 22:10:33 2015 -0700 @@ -0,0 +1,30 @@ +/* + * Copyright (C) 2015, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package gov.nasa.jpf.annotation; + +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; + +/** + * instances of @NonShared classes are not allowed to be referenced from + * more than one thread (but do allow hand-over) + */ +@Retention(RetentionPolicy.RUNTIME) +public @interface NonShared { + +} diff -r 3517702bd768 -r 4eb191cbb68c src/main/gov/nasa/jpf/listener/NonSharedChecker.java --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/main/gov/nasa/jpf/listener/NonSharedChecker.java Mon May 04 22:10:33 2015 -0700 @@ -0,0 +1,161 @@ +/* + * Copyright (C) 2015, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package gov.nasa.jpf.listener; + +import gov.nasa.jpf.Config; +import gov.nasa.jpf.ListenerAdapter; +import gov.nasa.jpf.vm.ClassInfo; +import gov.nasa.jpf.vm.ElementInfo; +import gov.nasa.jpf.vm.VM; +import gov.nasa.jpf.vm.ThreadInfo; +import gov.nasa.jpf.jvm.bytecode.ALOAD; +import gov.nasa.jpf.jvm.bytecode.ARETURN; +import gov.nasa.jpf.jvm.bytecode.ASTORE; +import gov.nasa.jpf.jvm.bytecode.IFNONNULL; +import gov.nasa.jpf.jvm.bytecode.IFNULL; +import gov.nasa.jpf.vm.bytecode.InstanceFieldInstruction; +import gov.nasa.jpf.vm.Instruction; +import gov.nasa.jpf.jvm.bytecode.MONITORENTER; +import gov.nasa.jpf.jvm.bytecode.VirtualInvocation; +import gov.nasa.jpf.vm.StackFrame; + +/** + * + */ +public class NonSharedChecker extends ListenerAdapter { + + boolean throwOnCycle = false; + + static class Access { + ThreadInfo ti; + Access prev; + + Access(ThreadInfo ti, Access prev){ + this.ti = ti; + this.prev = prev; + } + + // <2do> get a better hashCode for state hashing + public int hashCode() { + int h = ti.getId(); + for (Access p = prev; p!= null; p = p.prev){ + h = 31*h + p.ti.getId(); + } + return h; + } + // but we don't care for equals() + } + + public NonSharedChecker (Config conf){ + throwOnCycle = conf.getBoolean("nonshared.throw_on_cycle"); + } + + boolean isNonShared(ElementInfo ei){ + ClassInfo ci = ei.getClassInfo(); + return (ci.getAnnotation("gov.nasa.jpf.annotation.NonShared") != null); + } + + boolean checkLiveCycles (ElementInfo ei, ThreadInfo ti, Access ac){ + if (ti == ac.ti){ + return true; // Ok, fine - no need to record + + } else { + boolean foundLiveOne = false; + for (Access a = ac; a != null; a = a.prev){ + ThreadInfo t = a.ti; + if (t == ti){ // cycle detected + return !foundLiveOne; + } + foundLiveOne = (foundLiveOne || t.isAlive()); // <2do> maybe we should check for non-blocked threads + } + + // new one, record it in the access history of the object + ac = new Access(ti, ac); + ei = ei.getModifiableInstance(); + ei.setObjectAttr(ac); + } + + return true; + } + + + @Override + public void executeInstruction (VM vm, ThreadInfo ti, Instruction insn){ + + ElementInfo ei = null; + + if (ti.isFirstStepInsn()) { + return; + } + + if (insn instanceof InstanceFieldInstruction){ + ei = ((InstanceFieldInstruction)insn).peekElementInfo(ti); + } else if (insn instanceof VirtualInvocation){ + ei = ((VirtualInvocation)insn).getThisElementInfo(ti); // Outch - that's expensive + } else if (insn instanceof MONITORENTER || + insn instanceof ASTORE || + insn instanceof ARETURN || + insn instanceof IFNONNULL || + insn instanceof IFNULL) { + StackFrame frame = ti.getTopFrame(); + int ref = frame.peek(); + if (ref != -1){ + ei = ti.getElementInfo(ref); + } + } else if (insn instanceof ALOAD){ + StackFrame frame = ti.getTopFrame(); + int ref = frame.getLocalVariable(((ALOAD)insn).getLocalVariableIndex()); + if (ref != -1){ + ei = ti.getElementInfo(ref); + } + } + + if (ei != null){ + Access ac = ei.getObjectAttr(Access.class); + if (ac != null){ + if (!checkLiveCycles(ei,ti,ac)){ + StringBuilder sb = new StringBuilder("NonShared object: "); + sb.append( ei); + sb.append(" accessed in live thread cycle: "); + sb.append( ti.getName()); + for (Access a = ac; a != null; a = a.prev ){ + sb.append(','); + sb.append(a.ti.getName()); + } + String msg = sb.toString(); + + if (throwOnCycle){ + ti.setNextPC( ti.createAndThrowException("java.lang.AssertionError", msg)); + } else { + System.err.println("WARNING: " + msg); + System.err.println("\tat " + insn.getSourceLocation()); + } + return; + } + } + } + } + + @Override + public void objectCreated (VM vm, ThreadInfo ti, ElementInfo ei){ + if (isNonShared(ei)){ + ei.setObjectAttrNoClone(new Access(ti, null)); + } + } +} +