import java.util.Random;
import java.util.concurrent.locks.ReentrantLock;
import org.checkerframework.checker.lock.qual.*;
import org.checkerframework.dataflow.qual.SideEffectFree;

public class TestTreeKinds {
  class MyClass {
    Object field = new Object();

    @LockingFree
    Object method(@GuardSatisfied MyClass this) {
      return new Object();
    }

    void method2(@GuardSatisfied MyClass this) {}
  }

  @GuardedBy("lock") MyClass m;

  {
    // In constructor/initializer, it's OK not to hold the lock on 'this', but other locks must
    // be respected.
    // :: error: (lock.not.held)
    m.field = new Object();
  }

  final ReentrantLock lock = new ReentrantLock();
  final ReentrantLock lock2 = new ReentrantLock();

  @GuardedBy("lock") MyClass foo = new MyClass();

  MyClass unguardedFoo = new MyClass();

  @EnsuresLockHeld("lock")
  void lockTheLock() {
    lock.lock();
  }

  @EnsuresLockHeld("lock2")
  void lockTheLock2() {
    lock2.lock();
  }

  @EnsuresLockHeldIf(expression = "lock", result = true)
  boolean tryToLockTheLock() {
    return lock.tryLock();
  }

  // This @MayReleaseLocks annotation causes dataflow analysis to assume 'lock' is released after
  // unlockTheLock() is called.
  @MayReleaseLocks
  void unlockTheLock() {}

  @SideEffectFree
  void sideEffectFreeMethod() {}

  @LockingFree
  void lockingFreeMethod() {}

  @MayReleaseLocks
  void nonSideEffectFreeMethod() {}

  @Holding("lock")
  void requiresLockHeldMethod() {}

  MyClass fooArray @GuardedBy("lock") [] = new MyClass[3];

  @GuardedBy("lock") MyClass fooArray2[] = new MyClass[3];

  @GuardedBy("lock") MyClass fooArray3[][] = new MyClass[3][3];

  MyClass fooArray4 @GuardedBy("lock") [][] = new MyClass[3][3];

  MyClass fooArray5[] @GuardedBy("lock") [] = new MyClass[3][3];

  class myClass {
    int i = 0;
  }

  @GuardedBy("lock") myClass myClassInstance = new myClass();

  @GuardedBy("lock") Exception exception = new Exception();

  class MyParametrizedType<T> {
    T foo;
    int l;
  }

  @GuardedBy("lock") MyParametrizedType<MyClass> myParametrizedType = new MyParametrizedType<>();

  MyClass getFooWithWrongReturnType() {
    // :: error: (return)
    return foo; // return of guarded object
  }

  @GuardedBy("lock") MyClass getFoo() {
    return foo;
  }

  MyClass @GuardedBy("lock") [] getFooArray() {
    return fooArray;
  }

  @GuardedBy("lock") MyClass[] getFooArray2() {
    return fooArray2;
  }

  @GuardedBy("lock") MyClass[][] getFooArray3() {
    return fooArray3;
  }

  MyClass @GuardedBy("lock") [][] getFooArray4() {
    return fooArray4;
  }

  MyClass[] @GuardedBy("lock") [] getFooArray5() {
    return fooArray5;
  }

  enum myEnumType {
    ABC,
    DEF
  }

  @GuardedBy("lock") myEnumType myEnum;

  void testEnumType() {
    // TODO: assignment is technically correct, but we could
    // make it friendlier for the user if constant enum values on the RHS
    // automatically cast to the @GuardedBy annotation of the LHS.
    // :: error: (assignment)
    myEnum = myEnumType.ABC;
  }

  final Object intrinsicLock = new Object();

  void testThreadHoldsLock(@GuardedBy("intrinsicLock") MyClass m) {
    if (Thread.holdsLock(intrinsicLock)) {
      m.field.toString();
    } else {
      // :: error: (lock.not.held)
      m.field.toString();
    }
  }

  void testTreeTypes() {
    int i, l;

    MyClass o = new MyClass();
    MyClass f = new MyClass();

    // The following test cases were inspired from annotator.find.ASTPathCriterion.isSatisfiedBy
    // in the Annotation File Utilities

    // TODO: File a bug for the dataflow issue mentioned in the line below.
    // TODO: uncomment: Hits a bug in dataflow:
    // do {
    //     break;
    // } while (foo.field != null); // access to guarded object in condition of do/while loop
    // :: error: (lock.not.held)
    for (foo = new MyClass(); foo.field != null; foo = new MyClass()) {
      break;
    } // access to guarded object in condition of for loop
    // assignment to guarded object (OK) --- foo is still refined to @GuardedBy("lock") after
    // this point, though.
    foo = new MyClass();
    // A simple method call to a guarded object is not considered a dereference (only field
    // accesses are considered dereferences).
    unguardedFoo.method2();
    // Same as above, but the guard must be satisfied if the receiver is @GuardSatisfied.
    // :: error: (lock.not.held)
    foo.method2();
    // attempt to use guarded object in a switch statement
    // :: error: (lock.not.held)
    switch (foo.field.hashCode()) {
    }
    // attempt to use guarded object inside a try with resources
    // try(foo = new MyClass()) { foo.field.toString(); }

    // Retrieving an element from a guarded array is a dereference
    // :: error: (lock.not.held)
    MyClass m = fooArray[0];

    // method call on dereference of unguarded element of *guarded* array
    // :: error: (lock.not.held)
    fooArray[0].field.toString();
    // :: error: (lock.not.held)
    l = fooArray.length; // dereference of guarded array itself

    // method call on dereference of guarded array element
    // :: error: (lock.not.held)
    fooArray2[0].field.toString();
    // method call on dereference of unguarded array - TODO: currently preconditions are not
    // retrieved correctly from array types. This is not unique to the Lock Checker.
    // fooArray2.field.toString();

    // method call on dereference of guarded array element of multidimensional array
    // :: error: (lock.not.held)
    fooArray3[0][0].field.toString();
    // method call on dereference of unguarded single-dimensional array element of unguarded
    // multidimensional array - TODO: currently preconditions are not retrieved correctly from
    // array types. This is not unique to the Lock Checker.
    // fooArray3[0].field.toString();
    // method call on dereference of unguarded multidimensional array - TODO: currently
    // preconditions are not retrieved correctly from array types. This is not unique to the
    // Lock Checker.
    // fooArray3.field.toString();

    // method call on dereference of unguarded array element of *guarded* multidimensional array
    // :: error: (lock.not.held)
    fooArray4[0][0].field.toString();
    // dereference of unguarded single-dimensional array element of *guarded* multidimensional
    // array
    // :: error: (lock.not.held)
    l = fooArray4[0].length;
    // dereference of guarded multidimensional array
    // :: error: (lock.not.held)
    l = fooArray4.length;

    // method call on dereference of unguarded array element of *guarded subarray* of
    // multidimensional array
    // :: error: (lock.not.held)
    fooArray5[0][0].field.toString();
    // dereference of guarded single-dimensional array element of multidimensional array
    // :: error: (lock.not.held)
    l = fooArray5[0].length;
    // dereference of unguarded multidimensional array
    l = fooArray5.length;

    // :: error: (lock.not.held)
    l = getFooArray().length; // dereference of guarded array returned by a method

    // method call on dereference of guarded array element returned by a method
    // :: error: (lock.not.held)
    getFooArray2()[0].field.toString();
    // dereference of unguarded array returned by a method
    l = getFooArray2().length;

    // method call on dereference of guarded array element of multidimensional array returned by
    // a method
    // :: error: (lock.not.held)
    getFooArray3()[0][0].field.toString();
    // dereference of unguarded single-dimensional array element of multidimensional array
    // returned by a method
    l = getFooArray3()[0].length;
    // dereference of unguarded multidimensional array returned by a method
    l = getFooArray3().length;

    // method call on dereference of unguarded array element of *guarded* multidimensional array
    // returned by a method
    // :: error: (lock.not.held)
    getFooArray4()[0][0].field.toString();
    // dereference of unguarded single-dimensional array element of *guarded* multidimensional
    // array returned by a method
    // :: error: (lock.not.held)
    l = getFooArray4()[0].length;
    // dereference of guarded multidimensional array returned by a method
    // :: error: (lock.not.held)
    l = getFooArray4().length;

    // method call on dereference of unguarded array element of *guarded subarray* of
    // multidimensional array returned by a method
    // :: error: (lock.not.held)
    getFooArray5()[0][0].field.toString();
    // dereference of guarded single-dimensional array element of multidimensional array
    // returned by a method
    // :: error: (lock.not.held)
    l = getFooArray5()[0].length;
    // dereference of unguarded multidimensional array returned by a method
    l = getFooArray5().length;

    // Test different @GuardedBy(...) present on the element and array locations.
    @GuardedBy("lock") MyClass @GuardedBy("lock2") [] array = new MyClass[3];
    // :: error: (lock.not.held)
    array[0].field = new Object();
    if (lock.isHeldByCurrentThread()) {
      // :: error: (lock.not.held)
      array[0].field = new Object();
      if (lock2.isHeldByCurrentThread()) {
        array[0].field = new Object();
      }
    }

    // method call on guarded object within parenthesized expression
    // :: error: (lock.not.held)
    String s = (foo.field.toString());
    // :: error: (lock.not.held)
    foo.field.toString(); // method call on guarded object
    // :: error: (lock.not.held)
    getFoo().field.toString(); // method call on guarded object returned by a method
    // :: error: (lock.not.held)
    this.foo.field.toString(); // method call on guarded object using 'this' literal
    // dereference of guarded object in labeled statement
    label:
    // :: error: (lock.not.held)
    foo.field.toString();
    // access to guarded object in instanceof expression (OK)
    if (foo instanceof MyClass) {}
    // access to guarded object in while condition of while loop (OK)
    while (foo != null) {
      break;
    }
    // binary operator on guarded object in else if condition (OK)
    if (false) {
    } else if (foo == o) {
    }
    // access to guarded object in a lambda expression
    Runnable rn =
        () -> {
          // :: error: (lock.not.held)
          foo.field.toString();
        };
    // :: error: (lock.not.held)
    i = myClassInstance.i; // access to member field of guarded object
    // MemberReferenceTrees? how do they work
    fooArray = new MyClass[3]; // second allocation of guarded array (OK)
    // dereference of guarded object in conditional expression tree
    // :: error: (lock.not.held)
    s = i == 5 ? foo.field.toString() : f.field.toString();
    // dereference of guarded object in conditional expression tree
    // :: error: (lock.not.held)
    s = i == 5 ? f.field.toString() : foo.field.toString();
    // Testing of 'return' is done in getFooWithWrongReturnType()
    // throwing a guarded object - when throwing an exception, it must be @GuardedBy({}). Even
    // @GuardedByUnknown is not allowed.
    try {
      // :: error: (throw)
      throw exception;
    } catch (Exception e) {
    }
    // casting of a guarded object to an unguarded object
    // :: error: (assignment)
    @GuardedBy({}) Object e1 = (Object) exception;
    // OK, since the local variable's type gets refined to @GuardedBy("lock")
    Object e2 = (Object) exception;
    // :: error: (lock.not.held)
    l = myParametrizedType.l; // dereference of guarded object having a parameterized type

    // We need to support locking on local variables and protecting local variables because
    // these locals may contain references to fields. Somehow we need to pass along the
    // information of which field it was.

    if (foo == o) { // binary operator on guarded object (OK)
      o.field.toString();
    }

    if (foo == null) {
      // With -AconcurrentSemantics turned off, a cannot.dereference error would be expected,
      // since there is an attempt to dereference an expression whose type has been refined to
      // @GuardedByBottom (due to the comparison to null). However, with -AconcurrentSemantics
      // turned on, foo may no longer be null by now, the refinement to @GuardedByBottom is
      // lost and the refined type of foo is now the declared type ( @GuardedBy("lock") ),
      // resulting in the lock.not.held error.
      // :: error: (lock.not.held)
      foo.field.toString();
    }

    // TODO: Reenable:
    // @PolyGuardedBy should not be written here, but it is not explicitly forbidden by the
    // framework.
    // @PolyGuardedBy MyClass m2 = new MyClass();
    // (cannot.dereference)
    // m2.field.toString();
  }

  @MayReleaseLocks
  public void testLocals() {
    final ReentrantLock localLock = new ReentrantLock();

    @GuardedBy("localLock") MyClass guardedByLocalLock = new MyClass();

    // :: error: (lock.not.held)
    guardedByLocalLock.field.toString();

    @GuardedBy("lock") MyClass local = new MyClass();

    // :: error: (lock.not.held)
    local.field.toString();

    lockTheLock();

    local.field.toString(); // No warning output

    unlockTheLock();
  }

  @MayReleaseLocks
  public void testMethodAnnotations() {
    Random r = new Random();

    if (r.nextBoolean()) {
      lockTheLock();
      requiresLockHeldMethod();
    } else {
      // :: error: (contracts.precondition)
      requiresLockHeldMethod();
    }

    if (r.nextBoolean()) {
      lockTheLock();
      foo.field.toString();

      unlockTheLock();

      // :: error: (lock.not.held)
      foo.field.toString();
    } else {
      // :: error: (lock.not.held)
      foo.field.toString();
    }

    if (tryToLockTheLock()) {
      foo.field.toString();
    } else {
      // :: error: (lock.not.held)
      foo.field.toString();
    }

    if (r.nextBoolean()) {
      lockTheLock();
      sideEffectFreeMethod();
      foo.field.toString();
    } else {
      lockTheLock();
      nonSideEffectFreeMethod();
      // :: error: (lock.not.held)
      foo.field.toString();
    }

    if (r.nextBoolean()) {
      lockTheLock();
      lockingFreeMethod();
      foo.field.toString();
    } else {
      lockTheLock();
      nonSideEffectFreeMethod();
      // :: error: (lock.not.held)
      foo.field.toString();
    }
  }

  void methodThatTakesAnInteger(Integer i) {}

  void testBoxedPrimitiveType() {
    Integer i = null;
    if (i == null) {}

    methodThatTakesAnInteger(i);
  }

  void testReceiverGuardedByItself(@GuardedBy("<self>") TestTreeKinds this) {
    // :: error: (lock.not.held)
    method();
    synchronized (this) {
      method();
    }
  }

  void method(@GuardSatisfied TestTreeKinds this) {}

  void testOtherClassReceiverGuardedByItself(final @GuardedBy("<self>") OtherClass o) {
    // :: error: (lock.not.held)
    o.foo();
    synchronized (o) {
      o.foo();
    }
  }

  class OtherClass {
    void foo(@GuardSatisfied OtherClass this) {}
  }

  void testExplicitLockSynchronized() {
    final ReentrantLock lock = new ReentrantLock();
    // :: error: (explicit.lock.synchronized)
    synchronized (lock) {
    }
  }

  void testPrimitiveTypeGuardedby() {
    // :: error: (immutable.type.guardedby)
    @GuardedBy("lock") int a = 0;
    // :: error: (immutable.type.guardedby)
    @GuardedBy int b = 0;
    // :: error: (immutable.type.guardedby) :: error: (guardsatisfied.location.disallowed)
    @GuardSatisfied int c = 0;
    // :: error: (immutable.type.guardedby) :: error: (guardsatisfied.location.disallowed)
    @GuardSatisfied(1) int d = 0;
    int e = 0;
    // :: error: (immutable.type.guardedby)
    @GuardedByUnknown int f = 0;
    // :: error: (immutable.type.guardedby) :: error: (assignment)
    @GuardedByBottom int g = 0;
  }

  void testBinaryOperatorBooleanResultIsAlwaysGuardedByNothing() {
    @GuardedBy("lock") Object o1 = new Object();
    Object o2 = new Object();
    // boolean variables are implicitly @GuardedBy({}).
    boolean b1 = o1 == o2;
    boolean b2 = o2 == o1;
    boolean b3 = o1 != o2;
    boolean b4 = o2 != o1;
    boolean b5 = o1 instanceof Object;
    boolean b6 = o2 instanceof Object;
    boolean b7 = o1 instanceof @GuardedBy("lock") Object;
    boolean b8 = o2 instanceof @GuardedBy("lock") Object;
  }
}