2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
19 package gov.nasa.jpf.vm;
21 import gov.nasa.jpf.Config;
22 import gov.nasa.jpf.JPF;
23 import gov.nasa.jpf.SystemAttribute;
24 import gov.nasa.jpf.util.FieldSpecMatcher;
25 import gov.nasa.jpf.util.JPFLogger;
26 import gov.nasa.jpf.util.MethodSpecMatcher;
27 import gov.nasa.jpf.util.TypeSpecMatcher;
28 import gov.nasa.jpf.vm.choice.ThreadChoiceFromSet;
31 * an abstract SharednessPolicy implementation that makes use of both
32 * shared field access CGs and exposure CGs.
34 * This class is highly configurable, both in terms of using exposure CGs and filters.
35 * The *never_break filters should be used with care to avoid missing defects, especially
36 * the (transitive) method filters.
37 * NOTE - the default settings from jpf-core/jpf.properties include several
38 * java.util.concurrent* and java.lang.* fields/methods that can in fact contribute to
39 * concurrency defects, esp. in SUTs that explicitly use Thread/ThreadGroup objects, in
40 * which case they should be removed.
42 * The *always_break field filter should only be used for white box SUT analysis if JPF
43 * fails to detect sharedness (e.g. because no exposure is used). This should only
44 * go into application property files
46 public abstract class GenericSharednessPolicy implements SharednessPolicy, Attributor {
48 //--- auxiliary types to configure filters
49 static class NeverBreakIn implements SystemAttribute {
50 static NeverBreakIn singleton = new NeverBreakIn();
52 static class NeverBreakOn implements SystemAttribute {
53 static NeverBreakOn singleton = new NeverBreakOn();
55 static class AlwaysBreakOn implements SystemAttribute {
56 static AlwaysBreakOn singleton = new AlwaysBreakOn();
59 protected static JPFLogger logger = JPF.getLogger("shared");
62 //--- options used for concurrent field access detection
64 protected TypeSpecMatcher neverBreakOnTypes;
66 protected TypeSpecMatcher alwaysBreakOnTypes;
69 * never break or expose if a matching method is on the stack
71 protected MethodSpecMatcher neverBreakInMethods;
74 * never break on matching fields
76 protected FieldSpecMatcher neverBreakOnFields;
79 * always break matching fields, no matter if object is already shared or not
81 protected FieldSpecMatcher alwaysBreakOnFields;
85 * do we break on final field access
87 protected boolean skipFinals;
88 protected boolean skipConstructedFinals;
89 protected boolean skipStaticFinals;
92 * do we break inside of constructors
93 * (note that 'this' references could leak from ctors, but
94 * this is rather unusual)
96 protected boolean skipInits;
99 * do we add CGs for objects that could become shared, e.g. when storing
100 * a reference to a non-shared object in a shared object field.
101 * NOTE: this is a conservative measure since we don't know yet at the
102 * point of exposure if the object will ever be shared, which means it
103 * can cause state explosion.
105 protected boolean breakOnExposure;
108 * options to filter out lock protected field access, which is not
109 * supposed to cause shared CGs
110 * (this has no effect on exposure though)
112 protected boolean useSyncDetection;
113 protected int lockThreshold;
118 protected GenericSharednessPolicy (Config config){
119 neverBreakInMethods = MethodSpecMatcher.create( config.getStringArray("vm.shared.never_break_methods"));
121 neverBreakOnTypes = TypeSpecMatcher.create(config.getStringArray("vm.shared.never_break_types"));
122 alwaysBreakOnTypes = TypeSpecMatcher.create(config.getStringArray("vm.shared.always_break_types"));
124 neverBreakOnFields = FieldSpecMatcher.create( config.getStringArray("vm.shared.never_break_fields"));
125 alwaysBreakOnFields = FieldSpecMatcher.create( config.getStringArray("vm.shared.always_break_fields"));
127 skipFinals = config.getBoolean("vm.shared.skip_finals", true);
128 skipConstructedFinals = config.getBoolean("vm.shared.skip_constructed_finals", false);
129 skipStaticFinals = config.getBoolean("vm.shared.skip_static_finals", true);
130 skipInits = config.getBoolean("vm.shared.skip_inits", true);
132 breakOnExposure = config.getBoolean("vm.shared.break_on_exposure", true);
134 useSyncDetection = config.getBoolean("vm.shared.sync_detection", true);
135 lockThreshold = config.getInt("vm.shared.lockthreshold", 5);
138 //--- internal methods (potentially overridden by subclass)
141 //--- attribute management
143 protected void setTypeAttributes (TypeSpecMatcher neverMatcher, TypeSpecMatcher alwaysMatcher, ClassInfo ciLoaded){
144 // we flatten this for performance reasons
145 for (ClassInfo ci = ciLoaded; ci!= null; ci = ci.getSuperClass()){
146 if (alwaysMatcher != null && alwaysMatcher.matches(ci)){
147 ciLoaded.addAttr(AlwaysBreakOn.singleton);
150 if (neverMatcher != null && neverMatcher.matches(ci)){
151 ciLoaded.addAttr( NeverBreakOn.singleton);
157 protected void setFieldAttributes (FieldSpecMatcher neverMatcher, FieldSpecMatcher alwaysMatcher, ClassInfo ci){
158 for (FieldInfo fi : ci.getDeclaredInstanceFields()) {
159 // invisible fields (created by compiler)
160 if (fi.getName().startsWith("this$")) {
161 fi.addAttr( NeverBreakOn.singleton);
166 if (neverMatcher != null && neverMatcher.matches(fi)) {
167 fi.addAttr( NeverBreakOn.singleton);
169 if (alwaysMatcher != null && alwaysMatcher.matches(fi)) {
170 fi.addAttr( AlwaysBreakOn.singleton);
174 if (fi.hasAnnotation("gov.nasa.jpf.annotation.NeverBreak")){
175 fi.addAttr( NeverBreakOn.singleton);
179 for (FieldInfo fi : ci.getDeclaredStaticFields()) {
180 // invisible fields (created by compiler)
181 if ("$assertionsDisabled".equals(fi.getName())) {
182 fi.addAttr( NeverBreakOn.singleton);
187 if (neverMatcher != null && neverMatcher.matches(fi)) {
188 fi.addAttr( NeverBreakOn.singleton);
190 if (alwaysMatcher != null && alwaysMatcher.matches(fi)) {
191 fi.addAttr( AlwaysBreakOn.singleton);
195 if (fi.hasAnnotation("gov.nasa.jpf.annotation.NeverBreak")){
196 fi.addAttr( NeverBreakOn.singleton);
201 protected boolean isInNeverBreakMethod (ThreadInfo ti){
202 for (StackFrame frame = ti.getTopFrame(); frame != null; frame=frame.getPrevious()){
203 MethodInfo mi = frame.getMethodInfo();
204 if (mi.hasAttr( NeverBreakIn.class)){
212 protected abstract boolean checkOtherRunnables (ThreadInfo ti);
214 // this needs a three-way return value, hence Boolean
215 protected Boolean canHaveSharednessCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
217 if (ti.isFirstStepInsn()){ // no empty transitions
218 return Boolean.FALSE;
221 if (!checkOtherRunnables(ti)){ // nothing to reschedule
222 return Boolean.FALSE;
225 if (ti.hasAttr( NeverBreakIn.class)){
226 return Boolean.FALSE;
230 if (isInNeverBreakMethod(ti)){
235 ClassInfo ciFieldOwner = eiFieldOwner.getClassInfo();
236 if (ciFieldOwner.hasAttr(NeverBreakOn.class)){
237 return Boolean.FALSE;
239 if (ciFieldOwner.hasAttr(AlwaysBreakOn.class)){
245 if (fi.hasAttr(AlwaysBreakOn.class)) {
248 if (fi.hasAttr(NeverBreakOn.class)) {
249 return Boolean.FALSE;
256 //--- FieldLockInfo management
259 * static attribute filters that determine if the check..Access() and check..Exposure() methods should be called.
260 * This is only called once per instruction execution since it filters all cases that would set a CG.
261 * Filter conditions have to apply to both field access and object exposure.
263 protected abstract FieldLockInfo createFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi);
267 * generic version of FieldLockInfo update, which relies on FieldLockInfo implementation to determine
268 * if ElementInfo needs to be cloned
270 protected ElementInfo updateFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
271 FieldLockInfo fli = ei.getFieldLockInfo(fi);
273 fli = createFieldLockInfo(ti, ei, fi);
274 ei = ei.getModifiableInstance();
275 ei.setFieldLockInfo(fi, fli);
278 FieldLockInfo newFli = fli.checkProtection(ti, ei, fi);
280 ei = ei.getModifiableInstance();
281 ei.setFieldLockInfo(fi,newFli);
289 //--- runnable computation & CG creation
291 // NOTE - we don't schedule threads outside this process since field access if process local
293 protected ThreadInfo[] getRunnables (ApplicationContext appCtx){
294 return vm.getThreadList().getProcessTimeoutRunnables(appCtx);
297 protected ChoiceGenerator<ThreadInfo> getRunnableCG (String id, ThreadInfo tiCurrent){
298 if (vm.getSystemState().isAtomic()){ // no CG if we are in a atomic section
302 ThreadInfo[] choices = getRunnables(tiCurrent.getApplicationContext());
303 if (choices.length <= 1){ // field access doesn't block, i.e. the current thread is always runnable
307 return new ThreadChoiceFromSet( id, choices, true);
310 protected boolean setNextChoiceGenerator (ChoiceGenerator<ThreadInfo> cg){
312 return vm.getSystemState().setNextChoiceGenerator(cg); // listeners could still remove CGs
319 //--- internal policy methods that can be overridden by subclasses
321 protected ElementInfo updateSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
322 ThreadInfoSet tis = ei.getReferencingThreads();
323 ThreadInfoSet newTis = tis.add(ti);
326 ei = ei.getModifiableInstance();
327 ei.setReferencingThreads(newTis);
330 // we only change from non-shared to shared
331 if (newTis.isShared(ti, ei) && !ei.isShared() && !ei.isSharednessFrozen()) {
332 ei = ei.getModifiableInstance();
333 ei.setShared(ti, true);
336 if (ei.isShared() && fi != null){
337 ei = updateFieldLockInfo(ti,ei,fi);
343 protected boolean setsExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){
344 if (breakOnExposure){
345 ClassInfo ciExposed = eiExposed.getClassInfo();
348 if (ciExposed.hasAttr(NeverBreakOn.class)){
351 if (ciExposed.hasAttr(AlwaysBreakOn.class)){
352 logger.info("type exposure CG setting field ", fi, " to ", eiExposed);
353 return setNextChoiceGenerator(getRunnableCG("EXPOSE", ti));
356 // we can't filter on immutability since the race subject could be a reference
357 // that is exposed through the exposed object
359 if (isInNeverBreakMethod(ti)){
363 if (eiFieldOwner.isExposedOrShared() && isFirstExposure(eiFieldOwner, eiExposed)){
364 // don't check against the 'old' field value because this might get called after the field was already updated
365 // we should solely depend on different object sharedness
366 eiExposed = eiExposed.getExposedInstance(ti, eiFieldOwner);
367 logger.info("exposure CG setting field ", fi, " to ", eiExposed);
368 return setNextChoiceGenerator(getRunnableCG("EXPOSE", ti));
375 protected boolean isFirstExposure (ElementInfo eiFieldOwner, ElementInfo eiExposed){
376 if (!eiExposed.isImmutable()){
377 if (!eiExposed.isExposedOrShared()) {
378 return (eiFieldOwner.isExposedOrShared());
386 //------------------------------------------------ Attributor interface
389 * this can be used to initializeSharednessPolicy per-application mechanisms such as ClassInfo attribution
392 public void initializeSharednessPolicy (VM vm, ApplicationContext appCtx){
395 SystemClassLoaderInfo sysCl = appCtx.getSystemClassLoader();
396 sysCl.addAttributor(this);
401 public void setAttributes (ClassInfo ci){
402 setTypeAttributes( neverBreakOnTypes, alwaysBreakOnTypes, ci);
404 setFieldAttributes( neverBreakOnFields, alwaysBreakOnFields, ci);
406 // this one is more expensive to iterate over and should be avoided
407 if (neverBreakInMethods != null){
408 for (MethodInfo mi : ci.getDeclaredMethods().values()){
409 if (neverBreakInMethods.matches(mi)){
410 mi.setAttr( NeverBreakIn.singleton);
417 //------------------------------------------------ SharednessPolicy interface
420 public ElementInfo updateObjectSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
421 return updateSharedness(ti, ei, fi);
424 public ElementInfo updateClassSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
425 return updateSharedness(ti, ei, fi);
428 public ElementInfo updateArraySharedness (ThreadInfo ti, ElementInfo ei, int idx){
429 // NOTE - we don't support per-element FieldLockInfos (yet)
430 return updateSharedness(ti, ei, null);
435 * check to determine if call site, object/class attributes and thread execution state
436 * could cause CGs. This is called before sharedness is updated, i.e. can be used to
437 * filter objects/classes that should not be sharedness tracked
440 public boolean canHaveSharedObjectCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
441 Boolean ret = canHaveSharednessCG( ti, insn, eiFieldOwner, fi);
446 if (eiFieldOwner.isImmutable()){
450 if (skipFinals && fi.isFinal()){
454 //--- mixed (dynamic) attributes
455 if (skipConstructedFinals && fi.isFinal() && eiFieldOwner.isConstructed()){
459 if (skipInits && insn.getMethodInfo().isInit()){
467 public boolean canHaveSharedClassCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
468 Boolean ret = canHaveSharednessCG( ti, insn, eiFieldOwner, fi);
473 if (eiFieldOwner.isImmutable()){
477 if (skipStaticFinals && fi.isFinal()){
481 // call site. This could be transitive, in which case it has to be dynamic and can't be moved to isRelevant..()
482 MethodInfo mi = insn.getMethodInfo();
483 if (mi.isClinit() && (fi.getClassInfo() == mi.getClassInfo())) {
484 // clinits are all synchronized, so they are lock protected per se
492 public boolean canHaveSharedArrayCG (ThreadInfo ti, Instruction insn, ElementInfo eiArray, int idx){
493 Boolean ret = canHaveSharednessCG( ti, insn, eiArray, null);
498 // more array specific checks here
505 * <2do> explain why not transitive
507 * these are the public interfaces towards FieldInstructions. Callers have to be aware this will
508 * change the /referenced/ ElementInfo in case the respective object becomes exposed
511 public boolean setsSharedObjectCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
512 if (eiFieldOwner.getClassInfo().hasAttr(AlwaysBreakOn.class) ||
513 (eiFieldOwner.isShared() && !eiFieldOwner.isLockProtected(fi))) {
514 logger.info("CG accessing shared instance field ", fi);
515 return setNextChoiceGenerator( getRunnableCG("SHARED_OBJECT", ti));
522 public boolean setsSharedClassCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi){
523 if (eiFieldOwner.getClassInfo().hasAttr(AlwaysBreakOn.class) ||
524 (eiFieldOwner.isShared() && !eiFieldOwner.isLockProtected(fi))) {
525 logger.info("CG accessing shared static field ", fi);
526 return setNextChoiceGenerator( getRunnableCG("SHARED_CLASS", ti));
533 public boolean setsSharedArrayCG (ThreadInfo ti, Instruction insn, ElementInfo eiArray, int index){
534 if (eiArray.isShared()){
535 // <2do> we should check lock protection for the whole array here
536 logger.info("CG accessing shared array ", eiArray);
537 return setNextChoiceGenerator( getRunnableCG("SHARED_ARRAY", ti));
544 //--- internal policy methods that can be overridden by subclasses
546 protected boolean isRelevantStaticFieldAccess (ThreadInfo ti, Instruction insn, ElementInfo ei, FieldInfo fi){
551 if (ei.isImmutable()){
555 if (skipStaticFinals && fi.isFinal()){
559 if (!ti.hasOtherRunnables()){ // nothing to break for
563 // call site. This could be transitive, in which case it has to be dynamic and can't be moved to isRelevant..()
564 MethodInfo mi = insn.getMethodInfo();
565 if (mi.isClinit() && (fi.getClassInfo() == mi.getClassInfo())) {
566 // clinits are all synchronized, so they are lock protected per se
574 protected boolean isRelevantArrayAccess (ThreadInfo ti, Instruction insn, ElementInfo ei, int index){
575 // <2do> this is too simplistic, we should support filters for array objects
577 if (!ti.hasOtherRunnables()){
585 if (ti.isFirstStepInsn()){ // we already did break
592 //--- object exposure
594 // <2do> explain why not transitive
597 public boolean setsSharedObjectExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){
598 return setsExposureCG(ti,insn,eiFieldOwner,fi,eiExposed);
602 public boolean setsSharedClassExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed){
603 return setsExposureCG(ti,insn,eiFieldOwner,fi,eiExposed);
606 // since exposure is about the object being exposed (the element), there is no separate setsSharedArrayExposureCG
610 public void cleanupThreadTermination(ThreadInfo ti) {
611 // default action is to do nothing