Mercurial > hg > Members > kono > jpf-core
view src/main/gov/nasa/jpf/vm/GenericSharednessPolicy.java @ 34:49be04cc6389 default tip java9-try
cyclic dependency ...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 19 Dec 2017 11:21:23 +0900 |
parents | 61d41facf527 |
children |
line wrap: on
line source
/* * Copyright (C) 2014, 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.vm; import gov.nasa.jpf.Config; import gov.nasa.jpf.JPF; import gov.nasa.jpf.SystemAttribute; import gov.nasa.jpf.util.FieldSpecMatcher; import gov.nasa.jpf.util.JPFLogger; import gov.nasa.jpf.util.MethodSpecMatcher; import gov.nasa.jpf.util.TypeSpecMatcher; import gov.nasa.jpf.vm.choice.ThreadChoiceFromSet; /** * an abstract SharednessPolicy implementation that makes use of both * shared field access CGs and exposure CGs. * * This class is highly configurable, both in terms of using exposure CGs and filters. * The *never_break filters should be used with care to avoid missing defects, especially * the (transitive) method filters. * NOTE - the default settings from jpf-core/jpf.properties include several * java.util.concurrent* and java.lang.* fields/methods that can in fact contribute to * concurrency defects, esp. in SUTs that explicitly use Thread/ThreadGroup objects, in * which case they should be removed. * * The *always_break field filter should only be used for white box SUT analysis if JPF * fails to detect sharedness (e.g. because no exposure is used). This should only * go into application property files */ public abstract class GenericSharednessPolicy implements SharednessPolicy, Attributor { //--- auxiliary types to configure filters static class NeverBreakIn implements SystemAttribute { static NeverBreakIn singleton = new NeverBreakIn(); } static class NeverBreakOn implements SystemAttribute { static NeverBreakOn singleton = new NeverBreakOn(); } static class AlwaysBreakOn implements SystemAttribute { static AlwaysBreakOn singleton = new AlwaysBreakOn(); } protected static JPFLogger logger = JPF.getLogger("shared"); //--- options used for concurrent field access detection protected TypeSpecMatcher neverBreakOnTypes; protected TypeSpecMatcher alwaysBreakOnTypes; /** * never break or expose if a matching method is on the stack */ protected MethodSpecMatcher neverBreakInMethods; /** * never break on matching fields */ protected FieldSpecMatcher neverBreakOnFields; /** * always break matching fields, no matter if object is already shared or not */ protected FieldSpecMatcher alwaysBreakOnFields; /** * do we break on final field access */ protected boolean skipFinals; protected boolean skipConstructedFinals; protected boolean skipStaticFinals; /** * do we break inside of constructors * (note that 'this' references could leak from ctors, but * this is rather unusual) */ protected boolean skipInits; /** * do we add CGs for objects that could become shared, e.g. when storing * a reference to a non-shared object in a shared object field. * NOTE: this is a conservative measure since we don't know yet at the * point of exposure if the object will ever be shared, which means it * can cause state explosion. */ protected boolean breakOnExposure; /** * options to filter out lock protected field access, which is not * supposed to cause shared CGs * (this has no effect on exposure though) */ protected boolean useSyncDetection; protected int lockThreshold; protected VM vm; protected GenericSharednessPolicy (Config config){ neverBreakInMethods = MethodSpecMatcher.create( config.getStringArray("vm.shared.never_break_methods")); neverBreakOnTypes = TypeSpecMatcher.create(config.getStringArray("vm.shared.never_break_types")); alwaysBreakOnTypes = TypeSpecMatcher.create(config.getStringArray("vm.shared.always_break_types")); neverBreakOnFields = FieldSpecMatcher.create( config.getStringArray("vm.shared.never_break_fields")); alwaysBreakOnFields = FieldSpecMatcher.create( config.getStringArray("vm.shared.always_break_fields")); skipFinals = config.getBoolean("vm.shared.skip_finals", true); skipConstructedFinals = config.getBoolean("vm.shared.skip_constructed_finals", false); skipStaticFinals = config.getBoolean("vm.shared.skip_static_finals", true); skipInits = config.getBoolean("vm.shared.skip_inits", true); breakOnExposure = config.getBoolean("vm.shared.break_on_exposure", true); useSyncDetection = config.getBoolean("vm.shared.sync_detection", true); lockThreshold = config.getInt("vm.shared.lockthreshold", 5); } //--- internal methods (potentially overridden by subclass) //--- attribute management protected void setTypeAttributes (TypeSpecMatcher neverMatcher, TypeSpecMatcher alwaysMatcher, ClassInfo ciLoaded){ // we flatten this for performance reasons for (ClassInfo ci = ciLoaded; ci!= null; ci = ci.getSuperClass()){ if (alwaysMatcher != null && alwaysMatcher.matches(ci)){ ciLoaded.addAttr(AlwaysBreakOn.singleton); return; } if (neverMatcher != null && neverMatcher.matches(ci)){ ciLoaded.addAttr( NeverBreakOn.singleton); return; } } } protected void setFieldAttributes (FieldSpecMatcher neverMatcher, FieldSpecMatcher alwaysMatcher, ClassInfo ci){ for (FieldInfo fi : ci.getDeclaredInstanceFields()) { // invisible fields (created by compiler) if (fi.getName().startsWith("this$")) { fi.addAttr( NeverBreakOn.singleton); continue; } // configuration if (neverMatcher != null && neverMatcher.matches(fi)) { fi.addAttr( NeverBreakOn.singleton); } if (alwaysMatcher != null && alwaysMatcher.matches(fi)) { fi.addAttr( AlwaysBreakOn.singleton); } // annotation if (fi.hasAnnotation("gov.nasa.jpf.annotation.NeverBreak")){ fi.addAttr( NeverBreakOn.singleton); } } for (FieldInfo fi : ci.getDeclaredStaticFields()) { // invisible fields (created by compiler) if ("$assertionsDisabled".equals(fi.getName())) { fi.addAttr( NeverBreakOn.singleton); continue; } // configuration if (neverMatcher != null && neverMatcher.matches(fi)) { fi.addAttr( NeverBreakOn.singleton); } if (alwaysMatcher != null && alwaysMatcher.matches(fi)) { fi.addAttr( AlwaysBreakOn.singleton); } // annotation if (fi.hasAnnotation("gov.nasa.jpf.annotation.NeverBreak")){ fi.addAttr( NeverBreakOn.singleton); } } } protected boolean isInNeverBreakMethod (ThreadInfo ti){ for (StackFrame frame = ti.getTopFrame(); frame != null; frame=frame.getPrevious()){ MethodInfo mi = frame.getMethodInfo(); if (mi.hasAttr( NeverBreakIn.class)){ return true; } } return false; } protected abstract boolean checkOtherRunnables (ThreadInfo ti); // this needs a three-way return value, hence Boolean protected Boolean canHaveSharednessCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){ //--- thread if (ti.isFirstStepInsn()){ // no empty transitions return Boolean.FALSE; } if (!checkOtherRunnables(ti)){ // nothing to reschedule return Boolean.FALSE; } if (ti.hasAttr( NeverBreakIn.class)){ return Boolean.FALSE; } //--- method if (isInNeverBreakMethod(ti)){ return false; } //--- type ClassInfo ciFieldOwner = eiFieldOwner.getClassInfo(); if (ciFieldOwner.hasAttr(NeverBreakOn.class)){ return Boolean.FALSE; } if (ciFieldOwner.hasAttr(AlwaysBreakOn.class)){ return Boolean.TRUE; } //--- field if (fi != null){ if (fi.hasAttr(AlwaysBreakOn.class)) { return Boolean.TRUE; } if (fi.hasAttr(NeverBreakOn.class)) { return Boolean.FALSE; } } return null; } //--- FieldLockInfo management /** * static attribute filters that determine if the check..Access() and check..Exposure() methods should be called. * This is only called once per instruction execution since it filters all cases that would set a CG. * Filter conditions have to apply to both field access and object exposure. */ protected abstract FieldLockInfo createFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi); /** * generic version of FieldLockInfo update, which relies on FieldLockInfo implementation to determine * if ElementInfo needs to be cloned */ protected ElementInfo updateFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi){ FieldLockInfo fli = ei.getFieldLockInfo(fi); if (fli == null){ fli = createFieldLockInfo(ti, ei, fi); ei = ei.getModifiableInstance(); ei.setFieldLockInfo(fi, fli); } else { FieldLockInfo newFli = fli.checkProtection(ti, ei, fi); if (newFli != fli) { ei = ei.getModifiableInstance(); ei.setFieldLockInfo(fi,newFli); } } return ei; } //--- runnable computation & CG creation // NOTE - we don't schedule threads outside this process since field access if process local protected ThreadInfo[] getRunnables (ApplicationContext appCtx){ return vm.getThreadList().getProcessTimeoutRunnables(appCtx); } protected ChoiceGenerator<ThreadInfo> getRunnableCG (String id, ThreadInfo tiCurrent){ if (vm.getSystemState().isAtomic()){ // no CG if we are in a atomic section return null; } ThreadInfo[] choices = getRunnables(tiCurrent.getApplicationContext()); if (choices.length <= 1){ // field access doesn't block, i.e. the current thread is always runnable return null; } return new ThreadChoiceFromSet( id, choices, true); } protected boolean setNextChoiceGenerator (ChoiceGenerator<ThreadInfo> cg){ if (cg != null){ return vm.getSystemState().setNextChoiceGenerator(cg); // listeners could still remove CGs } return false; } //--- internal policy methods that can be overridden by subclasses protected ElementInfo updateSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){ ThreadInfoSet tis = ei.getReferencingThreads(); ThreadInfoSet newTis = tis.add(ti); if (tis != newTis){ ei = ei.getModifiableInstance(); ei.setReferencingThreads(newTis); } // we only change from non-shared to shared if (newTis.isShared(ti, ei) && !ei.isShared() && !ei.isSharednessFrozen()) { ei = ei.getModifiableInstance(); ei.setShared(ti, true); } if (ei.isShared() && fi != null){ ei = updateFieldLockInfo(ti,ei,fi); } return ei; } protected boolean setsExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){ if (breakOnExposure){ ClassInfo ciExposed = eiExposed.getClassInfo(); //--- exposed type if (ciExposed.hasAttr(NeverBreakOn.class)){ return false; } if (ciExposed.hasAttr(AlwaysBreakOn.class)){ logger.info("type exposure CG setting field ", fi, " to ", eiExposed); return setNextChoiceGenerator(getRunnableCG("EXPOSE", ti)); } // we can't filter on immutability since the race subject could be a reference // that is exposed through the exposed object if (isInNeverBreakMethod(ti)){ return false; } if (eiFieldOwner.isExposedOrShared() && isFirstExposure(eiFieldOwner, eiExposed)){ // don't check against the 'old' field value because this might get called after the field was already updated // we should solely depend on different object sharedness eiExposed = eiExposed.getExposedInstance(ti, eiFieldOwner); logger.info("exposure CG setting field ", fi, " to ", eiExposed); return setNextChoiceGenerator(getRunnableCG("EXPOSE", ti)); } } return false; } protected boolean isFirstExposure (ElementInfo eiFieldOwner, ElementInfo eiExposed){ if (!eiExposed.isImmutable()){ if (!eiExposed.isExposedOrShared()) { return (eiFieldOwner.isExposedOrShared()); } } return false; } //------------------------------------------------ Attributor interface /** * this can be used to initializeSharednessPolicy per-application mechanisms such as ClassInfo attribution */ @Override public void initializeSharednessPolicy (VM vm, ApplicationContext appCtx){ this.vm = vm; SystemClassLoaderInfo sysCl = appCtx.getSystemClassLoader(); sysCl.addAttributor(this); } @Override public void setAttributes (ClassInfo ci){ setTypeAttributes( neverBreakOnTypes, alwaysBreakOnTypes, ci); setFieldAttributes( neverBreakOnFields, alwaysBreakOnFields, ci); // this one is more expensive to iterate over and should be avoided if (neverBreakInMethods != null){ for (MethodInfo mi : ci.getDeclaredMethods().values()){ if (neverBreakInMethods.matches(mi)){ mi.setAttr( NeverBreakIn.singleton); } } } } //------------------------------------------------ SharednessPolicy interface @Override public ElementInfo updateObjectSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){ return updateSharedness(ti, ei, fi); } @Override public ElementInfo updateClassSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){ return updateSharedness(ti, ei, fi); } @Override public ElementInfo updateArraySharedness (ThreadInfo ti, ElementInfo ei, int idx){ // NOTE - we don't support per-element FieldLockInfos (yet) return updateSharedness(ti, ei, null); } /** * check to determine if call site, object/class attributes and thread execution state * could cause CGs. This is called before sharedness is updated, i.e. can be used to * filter objects/classes that should not be sharedness tracked */ @Override public boolean canHaveSharedObjectCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){ Boolean ret = canHaveSharednessCG( ti, insn, eiFieldOwner, fi); if (ret != null){ return ret; } if (eiFieldOwner.isImmutable()){ return false; } if (skipFinals && fi.isFinal()){ return false; } //--- mixed (dynamic) attributes if (skipConstructedFinals && fi.isFinal() && eiFieldOwner.isConstructed()){ return false; } if (skipInits && insn.getMethodInfo().isInit()){ return false; } return true; } @Override public boolean canHaveSharedClassCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){ Boolean ret = canHaveSharednessCG( ti, insn, eiFieldOwner, fi); if (ret != null){ return ret; } if (eiFieldOwner.isImmutable()){ return false; } if (skipStaticFinals && fi.isFinal()){ return false; } // call site. This could be transitive, in which case it has to be dynamic and can't be moved to isRelevant..() MethodInfo mi = insn.getMethodInfo(); if (mi.isClinit() && (fi.getClassInfo() == mi.getClassInfo())) { // clinits are all synchronized, so they are lock protected per se return false; } return true; } @Override public boolean canHaveSharedArrayCG (ThreadInfo ti, Instruction insn, ElementInfo eiArray, int idx){ Boolean ret = canHaveSharednessCG( ti, insn, eiArray, null); if (ret != null){ return ret; } // more array specific checks here return true; } /** * <2do> explain why not transitive * * these are the public interfaces towards FieldInstructions. Callers have to be aware this will * change the /referenced/ ElementInfo in case the respective object becomes exposed */ @Override public boolean setsSharedObjectCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){ if (eiFieldOwner.getClassInfo().hasAttr(AlwaysBreakOn.class) || (eiFieldOwner.isShared() && !eiFieldOwner.isLockProtected(fi))) { logger.info("CG accessing shared instance field ", fi); return setNextChoiceGenerator( getRunnableCG("SHARED_OBJECT", ti)); } return false; } @Override public boolean setsSharedClassCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){ if (eiFieldOwner.getClassInfo().hasAttr(AlwaysBreakOn.class) || (eiFieldOwner.isShared() && !eiFieldOwner.isLockProtected(fi))) { logger.info("CG accessing shared static field ", fi); return setNextChoiceGenerator( getRunnableCG("SHARED_CLASS", ti)); } return false; } @Override public boolean setsSharedArrayCG (ThreadInfo ti, Instruction insn, ElementInfo eiArray, int index){ if (eiArray.isShared()){ // <2do> we should check lock protection for the whole array here logger.info("CG accessing shared array ", eiArray); return setNextChoiceGenerator( getRunnableCG("SHARED_ARRAY", ti)); } return false; } //--- internal policy methods that can be overridden by subclasses protected boolean isRelevantStaticFieldAccess (ThreadInfo ti, Instruction insn, ElementInfo ei, FieldInfo fi){ if (!ei.isShared()){ return false; } if (ei.isImmutable()){ return false; } if (skipStaticFinals && fi.isFinal()){ return false; } if (!ti.hasOtherRunnables()){ // nothing to break for return false; } // call site. This could be transitive, in which case it has to be dynamic and can't be moved to isRelevant..() MethodInfo mi = insn.getMethodInfo(); if (mi.isClinit() && (fi.getClassInfo() == mi.getClassInfo())) { // clinits are all synchronized, so they are lock protected per se return false; } return true; } protected boolean isRelevantArrayAccess (ThreadInfo ti, Instruction insn, ElementInfo ei, int index){ // <2do> this is too simplistic, we should support filters for array objects if (!ti.hasOtherRunnables()){ return false; } if (!ei.isShared()){ return false; } if (ti.isFirstStepInsn()){ // we already did break return false; } return true; } //--- object exposure // <2do> explain why not transitive @Override public boolean setsSharedObjectExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){ return setsExposureCG(ti,insn,eiFieldOwner,fi,eiExposed); } @Override public boolean setsSharedClassExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){ return setsExposureCG(ti,insn,eiFieldOwner,fi,eiExposed); } // since exposure is about the object being exposed (the element), there is no separate setsSharedArrayExposureCG @Override public void cleanupThreadTermination(ThreadInfo ti) { // default action is to do nothing } }