import org.checkerframework.checker.lock.qual.*;
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.dataflow.qual.*;

public class ItselfExpressionCases {
  final Object somelock = new Object();

  private final @GuardedBy({"<self>"}) MyClass m = new MyClass();

  @Pure
  private @GuardedBy({"<self>"}) MyClass getm() {
    return m;
  }

  @Pure
  private @GuardedBy({"<self>"}) MyClass getm2(@GuardedBy("<self>") ItselfExpressionCases this) {
    // The following error is due to the precondition of the this.m field dereference not being
    // satisfied.
    // :: error: (lock.not.held)
    return m;
  }

  @Pure
  private Object getmfield() {
    // :: error: (lock.not.held)
    return getm().field;
  }

  public void arrayTest(final Object @GuardedBy("<self>") [] a1) {
    // :: error: (lock.not.held)
    Object a = a1[0];
    synchronized (a1) {
      a = a1[0];
    }
  }

  Object @GuardedBy("<self>") [] a2;

  @Pure
  public Object @GuardedBy("<self>") [] geta2() {
    return a2;
  }

  public void arrayTest() {
    // :: error: (lock.not.held)
    Object a = geta2()[0];
    synchronized (geta2()) {
      a = geta2()[0];
    }
  }

  public void testCheckPreconditions(
      final @GuardedBy("<self>") MyClass o,
      @GuardSatisfied Object gs,
      @GuardSatisfied MyClass gsMyClass) {
    // :: error: (lock.not.held)
    getm().field = new Object();
    synchronized (getm()) {
      getm().field = new Object();
    }

    // :: error: (lock.not.held)
    m.field = new Object();
    synchronized (m) {
      m.field = new Object();
    }

    // :: error: (lock.not.held)
    gs = m.field;
    synchronized (m) {
      gs = m.field;
    }

    // :: error: (lock.not.held)
    gs = getm().field;
    synchronized (getm()) {
      gs = getm().field;
    }

    // :: error: (lock.not.held)
    gsMyClass = getm();
    synchronized (getm()) {
      gsMyClass = getm();
    }

    // :: error: (lock.not.held) :: error: (contracts.precondition)
    o.foo();
    synchronized (o) {
      // :: error: (contracts.precondition)
      o.foo();
      synchronized (somelock) {
        // o.foo() requires o.somelock is held, not this.somelock.
        // :: error: (contracts.precondition)
        o.foo();
      }
    }

    // :: error: (lock.not.held)
    o.foo2();
    synchronized (o) {
      o.foo2();
    }
  }

  class MyClass {
    Object field = new Object();

    @Holding("somelock")
    void foo(@GuardSatisfied MyClass this) {}

    void foo2(@GuardSatisfied MyClass this) {}

    void method(@GuardedBy("<self>") MyClass this) {
      // :: error: (lock.not.held) :: error: (contracts.precondition)
      this.foo();
      // :: error: (lock.not.held):: error: (contracts.precondition)
      foo();
      // :: error: (lock.not.held)
      synchronized (somelock) {
        // :: error: (lock.not.held)
        this.foo();
        // :: error: (lock.not.held)
        foo();
        synchronized (this) {
          this.foo();
          foo();
        }
      }

      // :: error: (lock.not.held)
      this.foo2();
      // :: error: (lock.not.held)
      foo2();
      synchronized (this) {
        this.foo2();
        foo2();
      }
    }
  }
}