src/main/gov/nasa/jpf/listener/NonSharedChecker.java

   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