Checkerframework Implementation

build.gradle

@@ -3,8 +3,11 @@ plugins {
 	id 'application'
 	id("com.diffplug.spotless") version "7.0.4"
 	id 'jacoco'
+	id("org.checkerframework").version("0.6.61")
 }
 
+apply plugin: "org.checkerframework"
+
 group = 'com.example'
 version = '1.0'
 
@@ -27,6 +30,11 @@ dependencies {
 	implementation 'org.checkerframework:checker:3.21.0'
 	annotationProcessor 'org.checkerframework:checker:3.21.0'
 
+	// Specify Checker Framework v3.52.0
+	compileOnly("org.checkerframework:checker-qual:3.52.0")
+	testCompileOnly("org.checkerframework:checker-qual:3.52.0")
+	checkerFramework("org.checkerframework:checker:3.52.0")
+
 	// Apache Commons
 	implementation 'commons-io:commons-io:2.16.1'
 
@@ -49,6 +57,15 @@ dependencies {
 	runtimeOnly 'org.apache.logging.log4j:log4j-layout-template-json'
 }
 
+checkerFramework {
+// Define which checkers to run
+checkers = [
+	"org.checkerframework.checker.nullness.NullnessChecker",
+]
+extraJavacArgs = [
+"-Astubs=$projectDir/src/main/stubs"
+]
+}
 
 spotless {
 

src/main/java/AddNullCheckBeforeDereferenceRefactoring.java

@@ -173,10 +173,17 @@ public void apply(ASTNode node, ASTRewrite rewriter) {
 			}
 
 			Expression ternary = validRefactors.get(varName.resolveBinding());
+			if (ternary == null) {
+				continue;
+			}
 
 			AST ast = node.getAST();
 			ParenthesizedExpression pExpression = ast.newParenthesizedExpression();
-			pExpression.setExpression((Expression) ASTNode.copySubtree(ast, ternary));
+			Expression expr = (Expression) ASTNode.copySubtree(ast, ternary);
+			if (expr == null) {
+				continue;
+			}
+			pExpression.setExpression(expr);
 
 			LOGGER.debug("[DEBUG] Replacing Variable: " + varName);
 			LOGGER.debug("[DEBUG] New Value: " + pExpression);

src/main/java/BooleanFlagRefactoring.java

@@ -2,6 +2,7 @@
 import java.util.List;
 import java.util.Map;
 
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.eclipse.jdt.core.dom.AST;
 import org.eclipse.jdt.core.dom.ASTNode;
 import org.eclipse.jdt.core.dom.Assignment;
@@ -66,7 +67,13 @@ private boolean isApplicable(VariableDeclarationStatement stmt) {
 		AST ast = stmt.getAST();
 
 		// Search through all declared variables in declaration node for a booleanflag
-		for (VariableDeclarationFragment frag : (List<VariableDeclarationFragment>) stmt.fragments()) {
+		// Eclipse JDT API guarantees fragments() returns a live
+		// List<VariableDeclarationFragment>
+		// See
+		// https://help.eclipse.org/latest/topic/org.eclipse.jdt.doc.isv/reference/api/org/eclipse/jdt/core/dom/VariableDeclarationStatement.html#fragments()
+		@SuppressWarnings("unchecked")
+		List<VariableDeclarationFragment> fragments = (List<VariableDeclarationFragment>) stmt.fragments();
+		for (VariableDeclarationFragment frag : fragments) {
 			Expression varInitializer = frag.getInitializer();
 			if (varInitializer == null) {
 				continue;
@@ -119,7 +126,7 @@ private boolean isEqualityOperator(Operator op) {
 		return (op == Operator.NOT_EQUALS || op == Operator.EQUALS);
 	}
 
-	private SimpleName getNullComparisonVariable(InfixExpression infix) {
+	private @Nullable SimpleName getNullComparisonVariable(InfixExpression infix) {
 		Expression leftOperand = infix.getLeftOperand();
 		Expression rightOperand = infix.getRightOperand();
 		if (leftOperand instanceof SimpleName varName && rightOperand instanceof NullLiteral) {
@@ -148,7 +155,7 @@ public void apply(ASTNode node, ASTRewrite rewriter) {
 		}
 	}
 
-	private void apply(ASTRewrite rewriter, SimpleName flagName) {
+	private void apply(ASTRewrite rewriter, @Nullable SimpleName flagName) {
 		if (flagName == null || !isFlag(flagName)) {
 			return;
 		}

src/main/java/NestedNullRefactoring.java

@@ -2,7 +2,6 @@
 import java.util.Dictionary;
 import java.util.Hashtable;
 import java.util.List;
-
 import org.eclipse.jdt.core.dom.AST;
 import org.eclipse.jdt.core.dom.ASTNode;
 import org.eclipse.jdt.core.dom.Block;
@@ -90,7 +89,16 @@ private boolean isApplicableImpl(MethodDeclaration declaration) {
 		}
 
 		Block body = declaration.getBody();
-		List<Statement> stmts = body.statements();
+		if (body == null) {
+			return false;
+		}
+
+		// Eclipse JDT API guarantees statements() returns a live
+		// List<Statement>
+		// See
+		// https://help.eclipse.org/latest/topic/org.eclipse.jdt.doc.isv/reference/api/org/eclipse/jdt/core/dom/Block.html#statements()
+		@SuppressWarnings("unchecked")
+		List<Statement> stmts = (List<Statement>) body.statements();
 
 		boolean isOneLine = stmts.size() == 1;
 		if (!isOneLine) {
@@ -104,7 +112,7 @@ private boolean isApplicableImpl(MethodDeclaration declaration) {
 
 		// Checks that the return statement is of a single equality check
 		Expression retExpr = ((ReturnStatement) stmt).getExpression();
-		if (!(retExpr instanceof InfixExpression)) {
+		if (retExpr == null || !(retExpr instanceof InfixExpression)) {
 			return false;
 		}
 
@@ -118,7 +126,11 @@ private boolean isApplicableImpl(MethodDeclaration declaration) {
 			if ((isValidOperand(leftOperand) && rightOperand instanceof NullLiteral)
 					|| (isValidOperand(rightOperand) && leftOperand instanceof NullLiteral)) {
 				System.out.println("[DEBUG] Found one line null check method: " + declaration.getName());
-				applicableMethods.put((declaration.resolveBinding()), retExpr);
+				IMethodBinding binding = declaration.resolveBinding();
+				if (binding == null) {
+					return false;
+				}
+				applicableMethods.put((binding), retExpr);
 			}
 		}
 		return false;
@@ -144,7 +156,12 @@ public void apply(ASTNode node, ASTRewrite rewriter) {
 	}
 
 	private void replace(ASTNode node, ASTRewrite rewriter, MethodInvocation invocation) {
-		Expression expr = (applicableMethods.get((invocation.resolveMethodBinding())));
+		IMethodBinding binding = invocation.resolveMethodBinding();
+		if (binding == null) {
+			return;
+		}
+
+		Expression expr = (applicableMethods.get(binding));
 		if (expr == null) {
 			System.err.println("Cannot find applicable method for refactoring. ");
 			return;

src/main/java/RefactoringEngine.java

@@ -2,6 +2,7 @@
 import java.util.List;
 
 import org.apache.logging.log4j.Logger;
+import org.checkerframework.checker.nullness.qual.NonNull;
 import org.apache.logging.log4j.LogManager;
 import org.eclipse.jdt.core.dom.AST;
 import org.eclipse.jdt.core.dom.ASTNode;
@@ -51,7 +52,7 @@ public RefactoringEngine(List<String> refactoringNames) {
 	 * @param sourceCode
 	 *            A string representing the filepath of the source code to refactor
 	 */
-	public String applyRefactorings(CompilationUnit cu, String sourceCode) {
+	public @NonNull String applyRefactorings(CompilationUnit cu, String sourceCode) {
 		AST ast = cu.getAST();
 		ASTRewrite rewriter = ASTRewrite.create(ast);
 
@@ -70,6 +71,7 @@ public void preVisit(ASTNode node) {
 		}
 
 		Document document = new Document(sourceCode);
+
 		TextEdit edits = rewriter.rewriteAST(document, null);
 		try {
 			edits.apply(document);

src/main/java/SentinelRefactoring.java

@@ -26,6 +26,8 @@
 
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
+import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
 
 /**
  * This class represents a refactoring in which integer variables whose values
@@ -57,19 +59,24 @@ public class SentinelRefactoring extends Refactoring {
 	 */
 	private class Sentinel {
 		/**
-		 * The original assignment statement setting the sentinel's value.
+		 * The original assignment statement setting the sentinel's value. A null value
+		 * indicates the sentinel has not yet been assigned a value
 		 */
-		public Assignment sentinel_assignment;
+		public @Nullable Assignment sentinel_assignment;
 		/**
-		 * The conditional expression used to decide the value of the sentinel.
+		 * The conditional expression used to decide the value of the sentinel. A null
+		 * value indicates a variable which could become a sentinel, but has not yet had
+		 * a conditional assignemnt.
 		 */
-		public InfixExpression null_check;
+		public @Nullable InfixExpression null_check;
 		/**
-		 * The last value assigned to the sentinel; Used for validity tracking.
+		 * The last value assigned to the sentinel; Used for validity tracking. A null
+		 * value represents an unknown previous value.
 		 */
-		public Object lastValue;
+		public @Nullable Object lastValue;
 
-		public Sentinel(Assignment sentinel_assignment, InfixExpression null_check, Object lastValue) {
+		public Sentinel(@Nullable Assignment sentinel_assignment, @Nullable InfixExpression null_check,
+				@Nullable Object lastValue) {
 			this.sentinel_assignment = sentinel_assignment;
 			this.null_check = null_check;
 			this.lastValue = lastValue;
@@ -110,8 +117,11 @@ private void detectReassignment(Assignment assignmentNode) {
 	 * Detects sentinels which are shadowed by new local variables and removes them.
 	 */
 	private void detectShadowing(VariableDeclarationStatement declaration) {
-		@SuppressWarnings("unchecked") // Silence type warnings; fragments() documentation guarantees type is
-		// valid.
+		// Eclipse JDT API guarantees fragments() returns a live
+		// List<VariableDeclarationFragment>
+		// See
+		// https://help.eclipse.org/latest/topic/org.eclipse.jdt.doc.isv/reference/api/org/eclipse/jdt/core/dom/VariableDeclarationStatement.html#fragments()
+		@SuppressWarnings("unchecked")
 		List<VariableDeclarationFragment> fragments = declaration.fragments();
 		for (VariableDeclarationFragment fragment : fragments) {
 			SimpleName varName = fragment.getName();
@@ -180,7 +190,9 @@ private void updateSentinel(ASTNode node) {
 			for (Map.Entry<IBinding, Sentinel> entry : sentinelCandidates.entrySet()) {
 				IBinding key = entry.getKey();
 				Sentinel sentinel = sentinelCandidates.get(key);
-				sentinel.lastValue = null;
+				if (sentinel != null) {
+					sentinel.lastValue = null;
+				}
 			}
 		}
 	}
@@ -265,7 +277,7 @@ public boolean isApplicable(InfixExpression infix) {
 	 * @param expr
 	 *            the Expression to parse
 	 */
-	private boolean isEqualityCheck(InfixExpression.Operator operator) {
+	private boolean isEqualityCheck(@Nullable Operator operator) {
 		return ((operator == InfixExpression.Operator.NOT_EQUALS || operator == InfixExpression.Operator.EQUALS));
 	}
 
@@ -300,8 +312,11 @@ public void detectSentinels(IfStatement ifStmt) {
 			return;
 		}
 
-		@SuppressWarnings("unchecked") // Silence type warnings; statements() documentation guarantees type is
-		// valid.
+		// Eclipse JDT API guarantees statements() returns a live
+		// List<Statement>
+		// See
+		// https://help.eclipse.org/latest/topic/org.eclipse.jdt.doc.isv/reference/api/org/eclipse/jdt/core/dom/Block.html#statements()
+		@SuppressWarnings("unchecked")
 		List<Statement> stmts = thenStmt.statements();
 
 		// Checks that there is only one line in the ifStatement.
@@ -378,6 +393,9 @@ public void apply(ASTNode node, ASTRewrite rewriter) {
 			Expression sent_val = sentinel_assignment.getRightHandSide();
 
 			InfixExpression null_check = sentinel.null_check;
+			if (null_check == null) {
+				continue;
+			}
 			InfixExpression.Operator null_check_op = null_check.getOperator();
 
 			AST ast = node.getAST();
@@ -393,19 +411,19 @@ public void apply(ASTNode node, ASTRewrite rewriter) {
 	/**
 	 * Returns the opposite of the given InfixExpression equality operator.
 	 */
-	private InfixExpression.Operator reverseOperator(InfixExpression.Operator op) {
+	private @NonNull Operator reverseOperator(Operator op) {
 		if (op == InfixExpression.Operator.EQUALS) {
 			return InfixExpression.Operator.NOT_EQUALS;
 		} else if (op == InfixExpression.Operator.NOT_EQUALS) {
 			return InfixExpression.Operator.EQUALS;
 		}
-		return null;
+		return op;
 	}
 
 	/**
 	 * Returns the conditonal operator to use in a refactored null check.
 	 */
-	public InfixExpression.Operator getRefactoredOperator(Operator null_check_op, Operator sentinel_check_op,
+	public @NonNull Operator getRefactoredOperator(Operator null_check_op, Operator sentinel_check_op,
 			boolean originalValueMatch) {
 		Operator refactoredOperator = originalValueMatch ? null_check_op : reverseOperator(null_check_op);
 
@@ -420,7 +438,7 @@ public InfixExpression.Operator getRefactoredOperator(Operator null_check_op, Op
 	 * @param exprs
 	 *            A list of expressions to parse
 	 */
-	public InfixExpression parseNullCheck(List<Expression> exprs) {
+	public @Nullable InfixExpression parseNullCheck(List<Expression> exprs) {
 		for (Expression expr : exprs) {
 			if (expr instanceof InfixExpression null_check_candidate) {
 				Expression leftOperand = null_check_candidate.getLeftOperand();

src/main/java/VGRTool.java

@@ -18,6 +18,7 @@
 import org.eclipse.jdt.core.dom.MethodInvocation;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
+import org.checkerframework.checker.nullness.qual.NonNull;
 
 /**
  * Program entrypoint class; Runs the refactoring engine on given source code
@@ -72,7 +73,7 @@ public static void main(String[] args) {
 	 * @param directory
 	 *            Filepath of directory to search through (non-recursive)
 	 */
-	private static List<File> getJavaFiles(String directory) throws IOException {
+	private static @NonNull List<File> getJavaFiles(String directory) throws IOException {
 		List<File> javaFiles = new ArrayList<>();
 
 		Files.walk(Paths.get(directory)).filter(path -> path.toString().endsWith(".java"))

src/main/stubs/parser.astub

@@ -0,0 +1,11 @@
+package org.eclipse.jdt.core.dom;
+
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.initialization.qual.UnknownInitialization;
+import org.eclipse.jdt.core.dom.ASTParser;
+
+public class ASTParser extends Object {
+        public void setEnvironment(String[] classpathEntries, String @Nullable [] sourcepathEntries, String @Nullable [] encodings, boolean includeRunningVMBootclasspath);
+        public ASTNode createAST(@Nullable org.eclipse.core.runtime.IProgressMonitor monitor);
+
+}

src/main/stubs/rewrite.astub

@@ -0,0 +1,9 @@
+package org.eclipse.jdt.core.dom.rewrite;
+
+import org.eclipse.jdt.core.dom.rewrite.ASTRewrite;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class ASTRewrite extends Object {
+        public org.eclipse.text.edits.TextEdit rewriteAST(org.eclipse.jface.text.IDocument document, @Nullable Map options) throws JavaModelException, IllegalArgumentException;
+        public final void replace(ASTNode node, ASTNode replacement, @Nullable org.eclipse.text.edits.TextEditGroup editGroup);
+}