01: //
02: // Copyright (C) 2005 United States Government as represented by the
03: // Administrator of the National Aeronautics and Space Administration
04: // (NASA). All Rights Reserved.
05: //
06: // This software is distributed under the NASA Open Source Agreement
07: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
08: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
09: // directory tree for the complete NOSA document.
10: //
11: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18: //
19: package gov.nasa.jpf.jvm;
20:
21: /**
22: * class encapsulating the lock protection detection for field access
23: * instructions. Used by on-the-fly partial order reduction in FieldInstruction
24: * to determine if a GET/PUT_FIELD/STATIC insn has to be treated as a
25: * boundary step (terminates a transition). If the field access is always
26: * protected by a lock, only the corresponding sync (INVOKExx or MONITORENTER)
27: * are boundary steps, thus the number of states can be significantly reduced
28: */
29: public abstract class FieldLockInfo implements Cloneable {
30: static protected FieldLockInfo empty = new EmptyFieldLockInfo();
31:
32: public abstract FieldLockInfo checkProtection(ElementInfo ei,
33: FieldInfo fi, ThreadInfo ti);
34:
35: public abstract boolean isProtected();
36:
37: /*
38: * we need this for faster instantiation. Make sure it gets overridden in
39: * case there is a need for per-instance parameterization
40: */
41: public Object clone() throws CloneNotSupportedException {
42: return super .clone();
43: }
44: }
45:
46: /**
47: * FieldLockSet implementation for fields that are terminally considered to be unprotected
48: */
49: class EmptyFieldLockInfo extends FieldLockInfo {
50: public FieldLockInfo checkProtection(ElementInfo ei, FieldInfo fi,
51: ThreadInfo ti) {
52: return this ;
53: }
54:
55: public boolean isProtected() {
56: return false;
57: }
58: }
|