Skip to content
This repository has been archived by the owner on Aug 10, 2024. It is now read-only.

Commit

Permalink
Remove Checker Framework
Browse files Browse the repository at this point in the history
No timeline for JDK9 support: see
typetools/checker-framework#1224
  • Loading branch information
Pr0methean committed Oct 10, 2017
1 parent 941bfdc commit d288781
Show file tree
Hide file tree
Showing 21 changed files with 305 additions and 367 deletions.
399 changes: 213 additions & 186 deletions .idea/workspace.xml

Large diffs are not rendered by default.

39 changes: 9 additions & 30 deletions betterrandom/pom.xml
Original file line number Diff line number Diff line change
@@ -1,14 +1,15 @@
<?xml version="1.0" encoding="UTF-8"?>
<!--suppress XmlHighlighting -->
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<project xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xmlns="http://maven.apache.org/POM/4.0.0"
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
<modelVersion>4.0.0</modelVersion>
<packaging>jar</packaging>
<properties>
<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
<prefix />
<prefix/>
<maven.compiler.source>1.8</maven.compiler.source>
<maven.compiler.target>1.8</maven.compiler.target>
<annotatedJdk>${org.checkerframework:jdk8:jar}</annotatedJdk>
<github.global.server>github</github.global.server>
</properties>
<groupId>io.github.pr0methean.betterrandom</groupId>
Expand Down Expand Up @@ -49,6 +50,11 @@
</distributionManagement>

<dependencies>
<dependency>
<groupId>com.google.code.findbugs</groupId>
<artifactId>jsr305</artifactId>
<version>3.0.2</version>
</dependency>
<dependency>
<!-- https://mvnrepository.com/artifact/org.apache.maven.plugins/maven-deploy-plugin -->
<groupId>org.apache.maven.plugins</groupId>
Expand All @@ -75,21 +81,6 @@
<version>3.6.1</version>
<scope>test</scope>
</dependency>
<dependency>
<groupId>org.checkerframework</groupId>
<artifactId>checker-qual</artifactId>
<version>2.2.1</version>
</dependency>
<dependency>
<groupId>org.checkerframework</groupId>
<artifactId>checker</artifactId>
<version>2.2.1</version>
</dependency>
<dependency>
<groupId>org.checkerframework</groupId>
<artifactId>jdk8</artifactId>
<version>2.2.1</version>
</dependency>
<dependency>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-deploy-plugin</artifactId>
Expand Down Expand Up @@ -121,7 +112,6 @@
<subpackages>io.github.pr0methean</subpackages>
<show>protected</show>
<links>
<link>https://checkerframework.org/api</link>
<link>https://docs.oracle.com/javase/8/docs/api</link>
<link>https://google.github.io/guava/releases/19.0/api/docs</link>
</links>
Expand Down Expand Up @@ -243,12 +233,6 @@
<Xmaxerrs>10000</Xmaxerrs>
<Xmaxwarns>10000</Xmaxwarns>
</compilerArguments>
<!-- FIXME: Enable once all issues are fixed
<annotationProcessors>
<annotationProcessor>org.checkerframework.checker.nullness.NullnessChecker
</annotationProcessor>
</annotationProcessors>
-->
<compilerArgs>
<arg>-Xbootclasspath/p:${annotatedJdk}</arg>
</compilerArgs>
Expand Down Expand Up @@ -350,11 +334,6 @@
readResolve(); !static !transient &lt;fields&gt;; }
</option>

<!-- Allow deletion of castNonNull -->
<option>-assumenosideeffects public class
org.checkerframework.checker.nullness.NullnessUtil
</option>

<!-- Work around a MethodHandle.invokeExact signature-check issue -->
<option>-dontwarn java.lang.invoke**</option>

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,6 @@
// ============================================================================
package io.github.pr0methean.betterrandom.prng;

import static org.checkerframework.checker.nullness.NullnessUtil.castNonNull;

import com.google.common.base.MoreObjects.ToStringHelper;
import io.github.pr0methean.betterrandom.seed.DefaultSeedGenerator;
import io.github.pr0methean.betterrandom.seed.SeedException;
Expand All @@ -34,8 +32,6 @@
import javax.crypto.Cipher;
import javax.crypto.NoSuchPaddingException;
import javax.crypto.spec.SecretKeySpec;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;

/**
* <p>Non-linear random number generator based on the AES block cipher in counter mode. Uses the
Expand Down Expand Up @@ -177,9 +173,8 @@ private void readObject(final ObjectInputStream in) throws IOException, ClassNot
}

@Override
@EnsuresNonNull({"counter", "counterInput", "cipher", "lock"})
protected void initTransientFields(
@UnknownInitialization AesCounterRandom this) {
AesCounterRandom this) {
super.initTransientFields();
if (counter == null) {
counter = new byte[COUNTER_SIZE_BYTES];
Expand Down Expand Up @@ -290,24 +285,22 @@ public void setSeed(final byte[] seed) {
} catch (final NoSuchAlgorithmException e) {
throw new RuntimeException(e);
}
this.seed = castNonNull(this.seed);
}

/**
* Combines the given seed with the existing seed using SHA-256.
*/
@Override
@SuppressWarnings("contracts.postcondition.not.satisfied")
public synchronized void setSeed(@UnknownInitialization(Random.class)AesCounterRandom this,
public synchronized void setSeed(AesCounterRandom this,
final long seed) {
if (superConstructorFinished) {
super.setSeed(seed);
}
}

@EnsuresNonNull({"counter", "this.seed", "entropyBits"})
@Override
protected void setSeedInternal(@UnknownInitialization(Random.class)AesCounterRandom this,
protected void setSeedInternal(AesCounterRandom this,
final byte[] seed) {
final int seedLength = seed.length;
if ((seedLength < 16) || (seedLength > MAX_TOTAL_SEED_LENGTH_BYTES)) {
Expand All @@ -322,7 +315,7 @@ protected void setSeedInternal(@UnknownInitialization(Random.class)AesCounterRan
counter = new byte[COUNTER_SIZE_BYTES];
System.arraycopy(seed, keyLength, counter, 0, seedLength - keyLength);
try {
castNonNull(cipher).init(Cipher.ENCRYPT_MODE, new SecretKeySpec(key, ALGORITHM));
cipher.init(Cipher.ENCRYPT_MODE, new SecretKeySpec(key, ALGORITHM));
} catch (final InvalidKeyException e) {
throw new RuntimeException("Invalid key: " + Arrays.toString(key), e);
}
Expand All @@ -331,7 +324,7 @@ protected void setSeedInternal(@UnknownInitialization(Random.class)AesCounterRan

/** Returns the longest supported seed length. */
@Override
public int getNewSeedLength(@UnknownInitialization AesCounterRandom this) {
public int getNewSeedLength(AesCounterRandom this) {
return MAX_TOTAL_SEED_LENGTH_BYTES;
}
}
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
package io.github.pr0methean.betterrandom.prng;

import static java.lang.Integer.toUnsignedLong;
import static org.checkerframework.checker.nullness.NullnessUtil.castNonNull;

import com.google.common.base.MoreObjects;
import com.google.common.base.MoreObjects.ToStringHelper;
Expand Down Expand Up @@ -33,10 +32,7 @@
import java.util.stream.IntStream;
import java.util.stream.LongStream;
import java.util.stream.StreamSupport;
import org.checkerframework.checker.initialization.qual.UnderInitialization;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import javax.annotation.Nullable;

/**
* Abstract {@link Random} with a seed field and an implementation of entropy counting.
Expand Down Expand Up @@ -104,7 +100,8 @@ protected BaseRandom(final int seedSizeBytes) throws SeedException {
* @param seedLength The seed length in bytes.
* @throws SeedException If there is a problem generating a seed.
*/
protected BaseRandom(final SeedGenerator seedGenerator, final int seedLength) throws SeedException {
protected BaseRandom(final SeedGenerator seedGenerator, final int seedLength)
throws SeedException {
this(seedGenerator.generateSeed(seedLength));
entropyBits = new AtomicLong(0);
}
Expand All @@ -114,7 +111,6 @@ protected BaseRandom(final SeedGenerator seedGenerator, final int seedLength) th
*
* @param seed the seed.
*/
@EnsuresNonNull("this.seed")
protected BaseRandom(final byte[] seed) {
superConstructorFinished = true;
if (seed == null) {
Expand Down Expand Up @@ -631,7 +627,6 @@ public byte[] getSeed() {
}
}

@EnsuresNonNull({"this.seed", "entropyBits"})
@Override
public void setSeed(final byte[] seed) {
lock.lock();
Expand All @@ -650,9 +645,8 @@ public void setSeed(final byte[] seed) {
* input with the existing seed as {@link java.security.SecureRandom#setSeed(long)} does.
*/
@SuppressWarnings("method.invocation.invalid")
@EnsuresNonNull({"this.seed", "entropyBits"})
@Override
public synchronized void setSeed(@UnknownInitialization(Random.class)BaseRandom this,
public synchronized void setSeed(BaseRandom this,
final long seed) {
final byte[] seedBytes = BinaryUtils.convertLongToBytes(seed);
if (superConstructorFinished) {
Expand Down Expand Up @@ -703,8 +697,7 @@ public boolean preferSeedWithLong() {
*
* @param seed The new seed.
*/
@EnsuresNonNull({"this.seed", "entropyBits"})
protected void setSeedInternal(@UnknownInitialization(Random.class)BaseRandom this,
protected void setSeedInternal(BaseRandom this,
final byte[] seed) {
if (this.seed == null || this.seed.length != seed.length) {
this.seed = seed.clone();
Expand All @@ -721,20 +714,18 @@ protected void setSeedInternal(@UnknownInitialization(Random.class)BaseRandom th
/**
* Called in constructor and readObject to initialize transient fields.
*/
@EnsuresNonNull("lock")
protected void initTransientFields(@UnknownInitialization BaseRandom this) {
protected void initTransientFields(BaseRandom this) {
if (lock == null) {
lock = new ReentrantLock();
}
superConstructorFinished = true;
}

@EnsuresNonNull({"lock", "seed", "entropyBits"})
private void readObject(@UnderInitialization(BaseRandom.class)BaseRandom this,
private void readObject(BaseRandom this,
final ObjectInputStream in) throws IOException, ClassNotFoundException {
in.defaultReadObject();
initTransientFields();
setSeedInternal(castNonNull(seed));
setSeedInternal(seed);
}

@Override
Expand Down Expand Up @@ -768,7 +759,6 @@ private void asyncReseedIfPossible() {
*
* @throws InvalidObjectException if the {@link DefaultSeedGenerator} fails.
*/
@EnsuresNonNull({"lock", "seed", "entropyBits"})
@SuppressWarnings("OverriddenMethodCallDuringObjectConstruction")
private void readObjectNoData() throws InvalidObjectException {
LOG.warn("BaseRandom.readObjectNoData() invoked; using DefaultSeedGenerator");
Expand All @@ -789,8 +779,7 @@ private void readObjectNoData() throws InvalidObjectException {
* subclasses that can't actually use an 8-byte seed. Also used in {@link #readObjectNoData()}.
*/
@SuppressWarnings("LockAcquiredButNotSafelyReleased")
@EnsuresNonNull({"seed", "entropyBits"})
protected void fallbackSetSeed(@UnknownInitialization BaseRandom this) {
protected void fallbackSetSeed(BaseRandom this) {
boolean locked = false;
if (lock != null) {
lock.lock();
Expand All @@ -815,5 +804,5 @@ protected void fallbackSetSeed(@UnknownInitialization BaseRandom this) {
}

@Override
public abstract int getNewSeedLength(@UnknownInitialization BaseRandom this);
public abstract int getNewSeedLength(BaseRandom this);
}
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,6 @@
import io.github.pr0methean.betterrandom.seed.SeedGenerator;
import io.github.pr0methean.betterrandom.util.BinaryUtils;
import java.util.Arrays;
import java.util.Random;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;

/**
* Java port of the <a href="http://home.southernct.edu/~pasqualonia1/ca/report.html"
Expand Down Expand Up @@ -133,9 +129,7 @@ protected ToStringHelper addSubclassFields(final ToStringHelper original) {
.add("currentCellIndex", currentCellIndex);
}

@EnsuresNonNull("cells")
@RequiresNonNull("seed")
private void copySeedToCellsAndPreEvolve(@UnknownInitialization CellularAutomatonRandom this) {
private void copySeedToCellsAndPreEvolve(CellularAutomatonRandom this) {
cells = new int[AUTOMATON_LENGTH];
// Set initial cell states using seed.
cells[AUTOMATON_LENGTH - 1] = seed[0] + 128;
Expand All @@ -158,8 +152,7 @@ private void copySeedToCellsAndPreEvolve(@UnknownInitialization CellularAutomato
}
}

@RequiresNonNull("cells")
private int internalNext(@UnknownInitialization CellularAutomatonRandom this, final int bits) {
private int internalNext(CellularAutomatonRandom this, final int bits) {
// Set cell addresses using address of current cell.
final int cellC = currentCellIndex - 1;

Expand Down Expand Up @@ -193,7 +186,7 @@ public int next(final int bits) {
}

@Override
public synchronized void setSeed(@UnknownInitialization(Random.class)CellularAutomatonRandom this,
public synchronized void setSeed(CellularAutomatonRandom this,
final long seed) {
final byte[] shortenedSeed = convertIntToBytes(((Long) seed).hashCode());
if (superConstructorFinished) {
Expand All @@ -204,7 +197,7 @@ public synchronized void setSeed(@UnknownInitialization(Random.class)CellularAut
}

@Override
protected void setSeedInternal(@UnknownInitialization(Random.class)CellularAutomatonRandom this,
protected void setSeedInternal(CellularAutomatonRandom this,
final byte[] seed) {
if (seed.length != SEED_SIZE_BYTES) {
throw new IllegalArgumentException("Cellular Automaton RNG requires a 32-bit (4-byte) seed.");
Expand All @@ -216,7 +209,7 @@ protected void setSeedInternal(@UnknownInitialization(Random.class)CellularAutom

/** Returns the only supported seed length. */
@Override
public int getNewSeedLength(@UnknownInitialization CellularAutomatonRandom this) {
public int getNewSeedLength(CellularAutomatonRandom this) {
return SEED_SIZE_BYTES;
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,6 @@
// ============================================================================
package io.github.pr0methean.betterrandom.prng;

import static org.checkerframework.checker.nullness.NullnessUtil.castNonNull;

import com.google.common.base.MoreObjects.ToStringHelper;
import io.github.pr0methean.betterrandom.seed.DefaultSeedGenerator;
import io.github.pr0methean.betterrandom.seed.SeedException;
Expand All @@ -25,8 +23,6 @@
import io.github.pr0methean.betterrandom.util.EntryPoint;
import java.util.Arrays;
import java.util.Random;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;

/**
* <p>A Java version of George Marsaglia's <a href="http://school.anhb.uwa.edu.au/personalpages/kwessen/shared/Marsaglia03.html">Complementary
Expand Down Expand Up @@ -82,7 +78,6 @@ public Cmwc4096Random(final SeedGenerator seedGenerator) throws SeedException {
*/
public Cmwc4096Random(final byte[] seed) {
super(seed);
state = castNonNull(state);
}

@Override
Expand All @@ -102,14 +97,13 @@ public byte[] getSeed() {
* @param seed ignored
*/
@Override
public synchronized void setSeed(@UnknownInitialization(Random.class)Cmwc4096Random this,
public synchronized void setSeed(Cmwc4096Random this,
final long seed) {
fallbackSetSeed();
}

@EnsuresNonNull({"this.seed", "state", "entropyBits"})
@Override
protected void setSeedInternal(@UnknownInitialization(Random.class)Cmwc4096Random this,
protected void setSeedInternal(Cmwc4096Random this,
final byte[] seed) {
if ((seed == null) || (seed.length != SEED_SIZE_BYTES)) {
throw new IllegalArgumentException("CMWC RNG requires 16kb of seed data.");
Expand Down Expand Up @@ -142,7 +136,7 @@ protected int next(final int bits) {

/** Returns the only supported seed length. */
@Override
public int getNewSeedLength(@UnknownInitialization Cmwc4096Random this) {
public int getNewSeedLength(Cmwc4096Random this) {
return SEED_SIZE_BYTES;
}
}
Loading

0 comments on commit d288781

Please sign in to comment.