import org.checkerframework.checker.lock.qual.GuardSatisfied;
import org.checkerframework.checker.lock.qual.GuardedBy;
import org.checkerframework.checker.lock.qual.GuardedByUnknown;
import org.checkerframework.checker.lock.qual.MayReleaseLocks;

public class GuardSatisfiedTest {
    void testGuardSatisfiedIndexMatching(
            @GuardSatisfied GuardSatisfiedTest this,
            @GuardSatisfied(1) Object o,
            @GuardSatisfied(2) Object p,
            @GuardSatisfied Object q) {
        methodToCall1(o, o);
        methodToCall1(p, p);
        // :: error: (guardsatisfied.parameters.must.match)
        methodToCall1(o, p);
        // :: error: (guardsatisfied.parameters.must.match)
        methodToCall1(p, o);
    }

    // Test defaulting of parameters - they must default to @GuardedBy({}), not @GuardSatisfied
    void testDefaulting(Object mustDefaultToGuardedByNothing, @GuardSatisfied Object p) {
        // Must assign in this direction to test the defaulting because assigning a RHS of
        // @GuardedBy({}) to a LHS @GuardSatisfied is legal.
        // :: error: (assignment.type.incompatible)
        mustDefaultToGuardedByNothing = p;
        @GuardedBy({}) Object q = mustDefaultToGuardedByNothing;
    }

    void testMethodCall(
            @GuardSatisfied GuardSatisfiedTest this,
            @GuardedBy("lock1") Object o,
            @GuardedBy("lock2") Object p,
            @GuardSatisfied Object q) {
        // Test matching parameters

        // :: error: (lock.not.held)
        methodToCall1(o, o);
        // :: error: (lock.not.held) :: error: (guardsatisfied.parameters.must.match)
        methodToCall1(o, p);
        // :: error: (lock.not.held)
        methodToCall1(p, p);
        synchronized (lock2) {
            // :: error: (lock.not.held)
            methodToCall1(o, o);
            // :: error: (guardsatisfied.parameters.must.match) :: error: (lock.not.held)
            methodToCall1(o, p);
            methodToCall1(p, p);
            synchronized (lock1) {
                methodToCall1(o, o);
                // :: error: (guardsatisfied.parameters.must.match)
                methodToCall1(o, p);
                methodToCall1(p, p);
            }
        }

        // Test a return type matching a parameter.

        // :: error: (lock.not.held)
        o = methodToCall2(o);
        // :: error: (lock.not.held) :: error: (assignment.type.incompatible)
        p = methodToCall2(o);
        // :: error: (lock.not.held)
        methodToCall2(o);
        // :: error: (lock.not.held)
        methodToCall2(p);
        synchronized (lock2) {
            // :: error: (lock.not.held)
            o = methodToCall2(o);
            // :: error: (lock.not.held) :: error: (assignment.type.incompatible)
            p = methodToCall2(o);
            // :: error: (lock.not.held)
            methodToCall2(o);
            methodToCall2(p);
        }
        synchronized (lock1) {
            o = methodToCall2(o);
            // :: error: (assignment.type.incompatible)
            p = methodToCall2(o);
            methodToCall2(o);
            // :: error: (lock.not.held)
            methodToCall2(p);
        }

        // Test the receiver type matching a parameter

        // Two @GS parameters with no index are incomparable (as is the case for 'this' and 'q')
        // :: error: (guardsatisfied.parameters.must.match)
        methodToCall3(q);

        // :: error: (guardsatisfied.parameters.must.match) :: error: (lock.not.held)
        methodToCall3(p);
        synchronized (lock1) {
            // Two @GS parameters with no index are incomparable (as is the case for 'this' and 'q')
            // :: error: (guardsatisfied.parameters.must.match)
            methodToCall3(q);
            // :: error: (guardsatisfied.parameters.must.match) :: error: (lock.not.held)
            methodToCall3(p);
            synchronized (lock2) {
                // Two @GS parameters with no index are incomparable (as is the case for 'this' and
                // 'q')
                // :: error: (guardsatisfied.parameters.must.match)
                methodToCall3(q);
                // :: error: (guardsatisfied.parameters.must.match)
                methodToCall3(p);
            }
        }

        // Test the return type matching the receiver type

        methodToCall4();
    }

    // Test the return type NOT matching the receiver type
    void testMethodCall(@GuardedBy("lock1") GuardSatisfiedTest this) {
        @GuardedBy("lock2") Object g;
        // :: error: (lock.not.held)
        methodToCall4();
        // TODO: lock.not.held is getting swallowed below
        //  error (assignment.type.incompatible) error (lock.not.held)
        // g = methodToCall4();

        // Separate the above test case into two for now
        // :: error: (lock.not.held)
        methodToCall4();

        // The following error is due to the fact that you cannot access "this.lock1" without first
        // having acquired "lock1".  The right fix in a user scenario would be to not guard "this"
        // with "this.lock1". The current object could instead be guarded by "<self>" or by some
        // other lock expression that is not one of its fields. We are keeping this test case here
        // to make sure this scenario issues a warning.
        // :: error: (lock.not.held)
        synchronized (lock1) {
            // :: error: (assignment.type.incompatible)
            g = methodToCall4();
        }
    }

    // :: error: (guardsatisfied.return.must.have.index)
    @GuardSatisfied Object testReturnTypesMustMatchAndMustHaveAnIndex1(@GuardSatisfied Object o) {
        // If the two @GuardSatisfied had an index, this error would not be issued:
        // :: error: (guardsatisfied.assignment.disallowed)
        return o;
    }

    @GuardSatisfied(1) Object testReturnTypesMustMatchAndMustHaveAnIndex2(@GuardSatisfied(1) Object o) {
        return o;
    }

    @GuardSatisfied(0) Object testReturnTypesMustMatchAndMustHaveAnIndex3(@GuardSatisfied(0) Object o) {
        return o;
    }

    // @GuardSatisfied is equivalent to @GuardSatisfied(-1).
    // :: error: (guardsatisfied.return.must.have.index)
    @GuardSatisfied Object testReturnTypesMustMatchAndMustHaveAnIndex4(@GuardSatisfied(-1) Object o) {
        // If the two @GuardSatisfied had an index, this error would not be issued:
        // :: error: (guardsatisfied.assignment.disallowed)
        return o;
    }

    @GuardSatisfied(1) Object testReturnTypesMustMatchAndMustHaveAnIndex5(@GuardSatisfied(2) Object o) {
        // :: error: (return.type.incompatible)
        return o;
    }

    // :: error: (guardsatisfied.return.must.have.index)
    @GuardSatisfied Object testReturnTypesMustMatchAndMustHaveAnIndex6(@GuardSatisfied(2) Object o) {
        // :: error: (return.type.incompatible)
        return o;
    }

    void testParamsMustMatch(@GuardSatisfied(1) Object o, @GuardSatisfied(2) Object p) {
        // :: error: (assignment.type.incompatible)
        o = p;
    }

    void methodToCall1(
            @GuardSatisfied GuardSatisfiedTest this,
            @GuardSatisfied(1) Object o,
            @GuardSatisfied(1) Object p) {}

    @GuardSatisfied(1) Object methodToCall2(@GuardSatisfied GuardSatisfiedTest this, @GuardSatisfied(1) Object o) {
        return o;
    }

    void methodToCall3(@GuardSatisfied(1) GuardSatisfiedTest this, @GuardSatisfied(1) Object o) {}

    @GuardSatisfied(1) Object methodToCall4(@GuardSatisfied(1) GuardSatisfiedTest this) {
        return this;
    }

    final Object lock1 = new Object(), lock2 = new Object();

    void testAssignment(@GuardSatisfied Object o) {
        @GuardedBy({"lock1", "lock2"}) Object p = new Object();
        // :: error: (lock.not.held)
        o = p;
        synchronized (lock1) {
            // :: error: (lock.not.held)
            o = p;
            synchronized (lock2) {
                o = p;
            }
        }
    }

    // Test disallowed @GuardSatisfied locations.
    // Whenever a disallowed location can be located within a method return type,
    // receiver or parameter, test it there, because it's important to check
    // that those are not mistakenly allowed, since annotations
    // on method return types, receivers and parameters are allowed.
    // By definition, fields and non-parameter local variables cannot be
    // in one of these locations on a method declaration, but other
    // locations can be.

    // :: error: (guardsatisfied.location.disallowed)
    @GuardSatisfied Object field;
    // :: error: (guardsatisfied.location.disallowed)
    void testGuardSatisfiedOnArrayElementAndLocalVariable(@GuardSatisfied Object[] array) {
        // :: error: (guardsatisfied.location.disallowed)
        @GuardSatisfied Object local;
    }

    // :: error: (guardsatisfied.location.disallowed)
    <T extends @GuardSatisfied Object> T testGuardSatisfiedOnBound(T t) {
        return t;
    }

    class MyParameterizedClass1<T extends @GuardedByUnknown Object> {
        void testGuardSatisfiedOnReceiverOfParameterizedClass(
                @GuardSatisfied MyParameterizedClass1<T> this) {}

        void testGuardSatisfiedOnArrayOfParameterizedType(
                MyParameterizedClass1<T> @GuardSatisfied [] array) {}

        void testGuardSatisfiedOnArrayComponentOfParameterizedType(
                // :: error: (guardsatisfied.location.disallowed)
                @GuardSatisfied MyParameterizedClass1<T>[] array) {}
    };

    void testGuardSatisfiedOnWildCardExtendsBound(
            // :: error: (guardsatisfied.location.disallowed)
            MyParameterizedClass1<? extends @GuardSatisfied Object> l) {}

    void testGuardSatisfiedOnWildCardSuperBound(
            // :: error: (guardsatisfied.location.disallowed)
            MyParameterizedClass1<? super @GuardSatisfied Object> l) {}

    @GuardSatisfied(1) Object testGuardSatisfiedOnParameters(
            @GuardSatisfied GuardSatisfiedTest this,
            Object @GuardSatisfied [] array,
            @GuardSatisfied Object param,
            @GuardSatisfied(1) Object param2) {
        return param2;
    }

    void testGuardSatisfiedOnArray1(Object @GuardSatisfied [][][] array) {}
    // :: error: (guardsatisfied.location.disallowed)
    void testGuardSatisfiedOnArray2(@GuardSatisfied Object[][][] array) {}
    // :: error: (guardsatisfied.location.disallowed)
    void testGuardSatisfiedOnArray3(Object[] @GuardSatisfied [][] array) {}
    // :: error: (guardsatisfied.location.disallowed)
    void testGuardSatisfiedOnArray4(Object[][] @GuardSatisfied [] array) {}
}

class Foo {
    @MayReleaseLocks
    void m1() {}

    @MayReleaseLocks
    // :: error: (guardsatisfied.with.mayreleaselocks)
    void m2(@GuardSatisfied Foo f) {
        // :: error: (method.invocation.invalid)
        f.m1();
    }

    @MayReleaseLocks
    void m2_2(Foo f) {
        f.m1();
    }

    void m3(@GuardSatisfied Foo f) {
        // :: error: (method.guarantee.violated) :: error: (method.invocation.invalid)
        f.m1();
    }

    @MayReleaseLocks
    void m4(Foo f) {
        f.m1();
    }

    @MayReleaseLocks
    void m5(Foo f) {
        m3(f);
    }
}