import java.util.concurrent.locks.*;
import org.checkerframework.checker.lock.qual.*;
import org.checkerframework.framework.qual.AnnotatedFor;

public class BasicLockTest {
  class MyClass {
    public Object field;
  }

  MyClass myUnannotatedMethod(MyClass param) {
    return param;
  }

  void myUnannotatedMethod2() {}

  @AnnotatedFor("lock")
  MyClass myAnnotatedMethod(MyClass param) {
    return param;
  }

  @AnnotatedFor("lock")
  void myAnnotatedMethod2() {}

  final @GuardedBy({}) ReentrantLock lockField = new ReentrantLock();

  @GuardedBy("lockField") MyClass m;

  @GuardedBy({}) MyClass o1 = new MyClass(), p1;

  @AnnotatedFor("lock")
  @MayReleaseLocks
  void testFields() {
    // Test in two ways that return values are @GuardedByUnknown.
    // The first way is more durable as cannot.dereference is tied specifically to
    // @GuardedByUnknown (and @GuardedByBottom, but it is unlikely to become the default for
    // return values on unannotated methods).
    // :: error: (lock.not.held) :: error: (argument)
    myUnannotatedMethod(o1).field = new Object();
    // The second way is less durable because the default for fields is currently @GuardedBy({})
    // but could be changed to @GuardedByUnknown.
    // :: error: (assignment) :: error: (argument)
    p1 = myUnannotatedMethod(o1);

    // Now test that an unannotated method behaves as if it's annotated with @MayReleaseLocks
    lockField.lock();
    myAnnotatedMethod2();
    m.field = new Object();
    myUnannotatedMethod2();
    // :: error: (lock.not.held)
    m.field = new Object();
  }

  void unannotatedReleaseLock(ReentrantLock lock) {
    lock.unlock();
  }

  @AnnotatedFor("lock")
  @MayReleaseLocks
  void testLocalVariables() {
    MyClass o2 = new MyClass(), p2;
    // :: error: (argument)
    p2 = myUnannotatedMethod(o2);
    MyClass o3 = new MyClass();
    myAnnotatedMethod(o3);

    // Now test that an unannotated method behaves as if it's annotated with @MayReleaseLocks
    final @GuardedBy({}) ReentrantLock lock = new ReentrantLock();
    @GuardedBy("lock") MyClass q = new MyClass();
    lock.lock();
    myAnnotatedMethod2();
    q.field = new Object();
    // Should behave as @MayReleaseLocks, and *should* reset @LockHeld assumption about local
    // variable lock.
    myUnannotatedMethod2();
    // :: error: (lock.not.held)
    q.field = new Object();
    lock.lock();
    // Should behave as @MayReleaseLocks, and *should* reset @LockHeld assumption about local
    // variable lock.
    // :: error: (argument)
    unannotatedReleaseLock(lock);
    // :: error: (lock.not.held)
    q.field = new Object();
  }
}