|
|
|
/*
|
|
|
|
* Copyright (c) 2016 - present Facebook, Inc.
|
|
|
|
* All rights reserved.
|
|
|
|
*
|
|
|
|
* This source code is licensed under the BSD style license found in the
|
|
|
|
* LICENSE file in the root directory of this source tree. An additional grant
|
|
|
|
* of patent rights can be found in the PATENTS file in the same directory.
|
|
|
|
*/
|
|
|
|
|
|
|
|
package codetoanalyze.java.checkers;
|
|
|
|
|
|
|
|
import javax.annotation.concurrent.ThreadSafe;
|
|
|
|
|
|
|
|
import java.util.concurrent.locks.Lock;
|
|
|
|
import java.util.concurrent.locks.ReadWriteLock;
|
|
|
|
import java.util.concurrent.locks.ReentrantLock;
|
|
|
|
import java.util.concurrent.locks.ReentrantReadWriteLock;
|
|
|
|
|
|
|
|
@ThreadSafe
|
|
|
|
public class Locks {
|
|
|
|
|
|
|
|
Integer f;
|
|
|
|
|
|
|
|
Lock mLock;
|
|
|
|
ReadWriteLock mReadWriteLock;
|
|
|
|
ReentrantLock mReentrantLock;
|
|
|
|
ReentrantReadWriteLock mReentrantReadWriteLock;
|
|
|
|
|
|
|
|
public void lockInOneBranchBad(boolean b) {
|
|
|
|
if (b) {
|
|
|
|
mLock.lock();
|
|
|
|
}
|
|
|
|
f = 24;
|
|
|
|
if (b) {
|
|
|
|
mLock.unlock();
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
public void afterUnlockBad() {
|
|
|
|
mLock.lock();
|
|
|
|
mLock.unlock();
|
|
|
|
f = 42;
|
|
|
|
}
|
|
|
|
|
|
|
|
public void afterReentrantLockUnlockBad() {
|
|
|
|
mReentrantLock.lock();
|
|
|
|
mReentrantLock.unlock();
|
|
|
|
f = 42;
|
|
|
|
}
|
|
|
|
|
|
|
|
public void afterWriteLockUnlockBad() {
|
|
|
|
mReentrantReadWriteLock.writeLock().lock();
|
|
|
|
mReentrantReadWriteLock.writeLock().unlock();
|
|
|
|
f = 42;
|
|
|
|
}
|
|
|
|
|
|
|
|
public void lockOk() {
|
|
|
|
mLock.lock();
|
|
|
|
f = 42;
|
|
|
|
mLock.unlock();
|
|
|
|
}
|
|
|
|
|
|
|
|
public void lockBothBranchesOk(boolean b) {
|
|
|
|
if (b) {
|
|
|
|
mLock.lock();
|
|
|
|
} else {
|
|
|
|
mLock.lock();
|
|
|
|
}
|
|
|
|
f = 42;
|
|
|
|
mLock.unlock();
|
|
|
|
}
|
|
|
|
|
|
|
|
public void reentrantLockOk() {
|
|
|
|
mReentrantLock.lock();
|
|
|
|
f = 42;
|
|
|
|
mReentrantLock.unlock();
|
|
|
|
}
|
|
|
|
|
|
|
|
public void rReentrantLockTryLockOk() {
|
|
|
|
if (mReentrantLock.tryLock()) {
|
|
|
|
f = 42;
|
|
|
|
mReentrantLock.unlock();
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
public void reentrantLockInterruptiblyOk() throws InterruptedException {
|
|
|
|
mReentrantLock.lockInterruptibly();
|
|
|
|
f = 42;
|
|
|
|
mReentrantLock.unlock();
|
|
|
|
}
|
|
|
|
|
|
|
|
private void acquireLock() {
|
|
|
|
mLock.lock();
|
|
|
|
}
|
|
|
|
|
|
|
|
public void acquireLockInCalleeOk() {
|
|
|
|
acquireLock();
|
|
|
|
f = 42;
|
|
|
|
mLock.unlock();
|
|
|
|
}
|
|
|
|
|
|
|
|
public void writeLockOk() {
|
|
|
|
mReadWriteLock.writeLock().lock();
|
|
|
|
f = 42;
|
|
|
|
mReadWriteLock.writeLock().unlock();
|
|
|
|
}
|
|
|
|
|
|
|
|
public void reentrantWriteLockOk() {
|
|
|
|
mReentrantReadWriteLock.writeLock().lock();
|
|
|
|
f = 42;
|
|
|
|
mReentrantReadWriteLock.writeLock().unlock();
|
|
|
|
}
|
|
|
|
|
|
|
|
private void releaseLock() {
|
|
|
|
mLock.unlock();
|
|
|
|
}
|
|
|
|
|
|
|
|
// our "squish all locks into one" abstraction is not ideal here...
|
|
|
|
public void FP_unlockOneLock() {
|
|
|
|
mLock.lock();
|
|
|
|
mReentrantLock.lock();
|
|
|
|
mReentrantLock.unlock();
|
|
|
|
f = 42;
|
|
|
|
mLock.unlock();
|
|
|
|
}
|
|
|
|
|
|
|
|
// ... or here
|
|
|
|
public void FN_releaseLockInCalleeBad() {
|
|
|
|
mLock.lock();
|
|
|
|
releaseLock();
|
|
|
|
f = 42;
|
|
|
|
}
|
|
|
|
|
|
|
|
// we don't model the case where `tryLock` fails
|
|
|
|
public void FN_withReentrantLockTryLockBad() {
|
|
|
|
if (!mReentrantLock.tryLock()) {
|
|
|
|
f = 42;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
// we shouldn't be able to write when holding a readLock
|
|
|
|
public void FN_readLockOk() {
|
|
|
|
mReentrantReadWriteLock.readLock().lock();
|
|
|
|
f = 42;
|
|
|
|
mReentrantReadWriteLock.readLock().unlock();
|
|
|
|
}
|
|
|
|
|
|
|
|
}
|