Skip to content

Commit

Permalink
Merge pull request #66 from LoiNguyenCS/fix-cf-issue
Browse files Browse the repository at this point in the history
Fix a crash in Checker Framework issue
  • Loading branch information
LoiNguyenCS authored Dec 7, 2023
2 parents 7e27bf2 + b4ea9c5 commit eb1b1bc
Show file tree
Hide file tree
Showing 23 changed files with 362 additions and 13 deletions.
29 changes: 29 additions & 0 deletions src/main/java/org/checkerframework/specimin/PrunerVisitor.java
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@
import com.github.javaparser.ast.type.Type;
import com.github.javaparser.ast.visitor.ModifierVisitor;
import com.github.javaparser.ast.visitor.Visitable;
import com.github.javaparser.resolution.UnsolvedSymbolException;
import com.github.javaparser.resolution.declarations.ResolvedConstructorDeclaration;
import com.github.javaparser.resolution.declarations.ResolvedMethodDeclaration;
import java.util.Iterator;
Expand Down Expand Up @@ -91,6 +92,16 @@ public Node visit(ImportDeclaration decl, Void p) {

@Override
public Visitable visit(MethodDeclaration methodDecl, Void p) {
try {
// resolved() will only check if the return type is solvable
// getQualifiedSignature() will also check if the parameters are solvable
methodDecl.resolve().getQualifiedSignature();
} catch (UnsolvedSymbolException e) {
// The current class is employed by the target methods, although not all of its members are
// utilized. It's not surprising for unused members to remain unresolved.
methodDecl.remove();
return methodDecl;
}
ResolvedMethodDeclaration resolved = methodDecl.resolve();
if (methodsToLeaveUnchanged.contains(resolved.getQualifiedSignature())) {
insideTargetMethod = true;
Expand All @@ -112,6 +123,16 @@ public Visitable visit(MethodDeclaration methodDecl, Void p) {

@Override
public Visitable visit(ConstructorDeclaration constructorDecl, Void p) {
try {
// resolved() will only check if the return type is solvable
// getQualifiedSignature() will also check if the parameters are solvable
constructorDecl.resolve().getQualifiedSignature();
} catch (UnsolvedSymbolException e) {
// The current class is employed by the target methods, although not all of its members are
// utilized. It's not surprising for unused members to remain unresolved.
constructorDecl.remove();
return constructorDecl;
}
ResolvedConstructorDeclaration resolved = constructorDecl.resolve();
if (methodsToLeaveUnchanged.contains(resolved.getQualifiedSignature())) {
return super.visit(constructorDecl, p);
Expand All @@ -126,6 +147,14 @@ public Visitable visit(ConstructorDeclaration constructorDecl, Void p) {

@Override
public Visitable visit(FieldDeclaration fieldDecl, Void p) {
try {
fieldDecl.resolve();
} catch (UnsolvedSymbolException e) {
// The current class is employed by the target methods, although not all of its members are
// utilized. It's not surprising for unused members to remain unresolved.
fieldDecl.remove();
return fieldDecl;
}
String classFullName = fieldDecl.resolve().declaringType().getQualifiedName();
boolean isFinal = fieldDecl.isFinal();
Iterator<VariableDeclarator> iterator = fieldDecl.getVariables().iterator();
Expand Down
11 changes: 9 additions & 2 deletions src/main/java/org/checkerframework/specimin/SpeciminRunner.java
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@
import com.github.javaparser.symbolsolver.resolution.typesolvers.JarTypeSolver;
import com.github.javaparser.symbolsolver.resolution.typesolvers.JavaParserTypeSolver;
import com.github.javaparser.symbolsolver.resolution.typesolvers.ReflectionTypeSolver;
import com.github.javaparser.utils.SourceRoot;
import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;
Expand Down Expand Up @@ -104,7 +105,14 @@ public static void performMinimization(
parsedTargetFiles.put(targetFile, parseJavaFile(root, targetFile));
}

UnsolvedSymbolVisitor addMissingClass = new UnsolvedSymbolVisitor(root);
// the set of Java files already exist in the input codebase
Set<Path> existingFiles = new HashSet<>();
SourceRoot sourceRoot = new SourceRoot(Path.of(root));
sourceRoot.tryToParse();
for (CompilationUnit compilationUnit : sourceRoot.getCompilationUnits()) {
existingFiles.add(compilationUnit.getStorage().get().getPath().toAbsolutePath().normalize());
}
UnsolvedSymbolVisitor addMissingClass = new UnsolvedSymbolVisitor(root, existingFiles);
addMissingClass.setClassesFromJar(jarPaths);
/**
* The set of path of files that have been created by addMissingClass. We will delete all those
Expand Down Expand Up @@ -153,7 +161,6 @@ public static void performMinimization(
}

Set<String> relatedClass = new HashSet<>(parsedTargetFiles.keySet());

// add all files related to the targeted methods
for (String classFullName : finder.getUsedClass()) {
String directoryOfFile = classFullName.replace(".", "/") + ".java";
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@
import com.github.javaparser.ast.expr.SuperExpr;
import com.github.javaparser.ast.stmt.CatchClause;
import com.github.javaparser.ast.stmt.ExplicitConstructorInvocationStmt;
import com.github.javaparser.ast.type.ClassOrInterfaceType;
import com.github.javaparser.ast.type.ReferenceType;
import com.github.javaparser.ast.type.Type;
import com.github.javaparser.ast.type.UnionType;
Expand All @@ -25,6 +26,7 @@
import com.github.javaparser.resolution.declarations.ResolvedValueDeclaration;
import com.github.javaparser.resolution.types.ResolvedReferenceType;
import com.github.javaparser.resolution.types.ResolvedType;
import com.google.common.base.Splitter;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
Expand Down Expand Up @@ -182,10 +184,8 @@ public Visitable visit(VariableDeclarator node, Void arg) {
@Override
public Visitable visit(MethodDeclaration method, Void p) {
String methodDeclAsString = method.getDeclarationAsString(false, false, false);
// The substring here is to remove the method's return type. Return types cannot contain spaces.
// TODO: test this with annotations
String methodName =
this.classFQName + "#" + methodDeclAsString.substring(methodDeclAsString.indexOf(' ') + 1);
String methodName = this.classFQName + "#" + removeMethodReturnType(methodDeclAsString);
// this method belongs to an anonymous class inside the target method
if (insideTargetMethod) {
ObjectCreationExpr parentExpression = (ObjectCreationExpr) method.getParentNode().get();
Expand Down Expand Up @@ -278,6 +278,24 @@ public Visitable visit(MethodCallExpr call, Void p) {
return super.visit(call, p);
}

@Override
public Visitable visit(ClassOrInterfaceType type, Void p) {
if (!insideTargetMethod) {
return super.visit(type, p);
}
try {
usedClass.add(type.resolve().getQualifiedName());
}
// if the type has a fully-qualified form, JavaParser also consider other components rather than
// the class name as ClassOrInterfaceType. For example, if the type is org.A.B, then JavaParser
// will also consider org and org.A as ClassOrInterfaceType.
// if type is a type variable, we will get an UnsupportedOperation Exception.
catch (UnsolvedSymbolException | UnsupportedOperationException e) {
return super.visit(type, p);
}
return super.visit(type, p);
}

@Override
public Visitable visit(ObjectCreationExpr newExpr, Void p) {
if (insideTargetMethod) {
Expand Down Expand Up @@ -307,7 +325,9 @@ public Visitable visit(FieldAccessExpr expr, Void p) {
usedMembers.add(fullNameOfClass + "#" + expr.getName().asString());
usedClass.add(fullNameOfClass);
usedClass.add(expr.resolve().getType().describe());
} catch (UnsolvedSymbolException e) {
}
// when the type is a primitive array, we will have an UnsupportedOperationException
catch (UnsolvedSymbolException | UnsupportedOperationException e) {
// if the a field is accessed in the form of a fully-qualified path, such as
// org.example.A.b, then other components in the path apart from the class name and field
// name, such as org and org.example, will also be considered as FieldAccessExpr.
Expand All @@ -333,6 +353,22 @@ public Visitable visit(NameExpr expr, Void p) {
return super.visit(expr, p);
}

/**
* Given a method declaration, this method return the declaration of that method without the
* return type.
*
* @param methodDeclaration the method declaration to be used as input
* @return methodDeclaration without the return type
*/
public static String removeMethodReturnType(String methodDeclaration) {
String methodDeclarationWithoutParen =
methodDeclaration.substring(0, methodDeclaration.indexOf("("));
List<String> methodParts = Splitter.onPattern(" ").splitToList(methodDeclarationWithoutParen);
String methodName = methodParts.get(methodParts.size() - 1);
String methodReturnType = methodDeclaration.substring(0, methodDeclaration.indexOf(methodName));
return methodDeclaration.replace(methodReturnType, "");
}

/**
* Resolves unionType parameters one by one and adds them in the usedClass set.
*
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -164,14 +164,19 @@ public class UnsolvedSymbolVisitor extends ModifierVisitor<Void> {
*/
private Map<String, @ClassGetSimpleName String> fieldNameToClassNameMap = new HashMap<>();

/** The list of existing files in the input codebase. */
private Set<Path> setOfExistingFiles;

/**
* Create a new UnsolvedSymbolVisitor instance
*
* @param rootDirectory the root directory of the input files
* @param setOfExistingFiles the set of existing files in the input codebase
*/
public UnsolvedSymbolVisitor(String rootDirectory) {
public UnsolvedSymbolVisitor(String rootDirectory, Set<Path> setOfExistingFiles) {
this.rootDirectory = rootDirectory;
this.gotException = true;
this.setOfExistingFiles = setOfExistingFiles;
}

/**
Expand Down Expand Up @@ -271,6 +276,15 @@ public void setExceptionToFalse() {
gotException = false;
}

@Override
public Node visit(ImportDeclaration decl, Void arg) {
if (decl.isAsterisk()) {
throw new RuntimeException(
"A wildcard import statement found. Please use explicit import" + " statements.");
}
return super.visit(decl, arg);
}

@Override
public Visitable visit(PackageDeclaration node, Void arg) {
this.currentPackage = node.getNameAsString();
Expand Down Expand Up @@ -400,6 +414,7 @@ public Visitable visit(TryStmt node, Void p) {
@Override
public Visitable visit(CatchClause node, Void p) {
HashSet<String> currentLocalVariables = new HashSet<>();
currentLocalVariables.add(node.getParameter().getNameAsString());
localVariables.addFirst(currentLocalVariables);
Visitable result = super.visit(node, p);
localVariables.removeFirst();
Expand Down Expand Up @@ -428,6 +443,10 @@ public Visitable visit(VariableDeclarator decl, Void p) {

// This part is to create synthetic class for the type of decl if needed.
Type declType = decl.getType();
if (declType.isVarType()) {
// nothing to do here. A var type could never be solved.
return super.visit(decl, p);
}
try {
declType.resolve();
} catch (UnsolvedSymbolException | UnsupportedOperationException e) {
Expand Down Expand Up @@ -577,9 +596,8 @@ public Visitable visit(FieldAccessExpr node, Void p) {
classAndPackageMap.getOrDefault(simpleClassName, currentPackage) + "." + node;
updateClassSetWithQualifiedFieldSignature(fullyQualifiedCall, true);
}
// if the symbol that called this field is solvable yet this field is unsolved, then the type of
// the calling symbol is a synthetic class that needs to have a synthetic field updated
else if (canBeSolved(node.getScope())) {
// check if this unsolved field belongs to a synthetic class.
else if (canBeSolved(node.getScope()) && !belongsToARealClassFile(node)) {
updateSyntheticClassWithNonStaticFields(node);
}

Expand Down Expand Up @@ -738,6 +756,20 @@ public Visitable visit(ObjectCreationExpr newExpr, Void p) {
return newExpr;
}

/**
* Given a field access expression, this method determines whether the field is declared in one of
* the original class file in the codebase (instead of a synthetic class).
*
* @param node a FieldAccessExpr instance
* @return true if the field is inside an original class file
*/
public boolean belongsToARealClassFile(FieldAccessExpr node) {
Expression nodeScope = node.getScope();
String filePath =
rootDirectory + nodeScope.calculateResolvedType().describe().replace(".", "/") + ".java";
return setOfExistingFiles.contains(Path.of(filePath).toAbsolutePath().normalize());
}

/**
* @param parameter parameter from visitor method which is unsolvable.
*/
Expand Down Expand Up @@ -769,11 +801,14 @@ private void handleParameterResolveFailure(@NonNull Parameter parameter) {
* @param parameter unionType parameter from visitor class
*/
private void resolveUnionType(@NonNull Parameter parameter) {
for (var param : parameter.getType().asUnionType().getElements()) {
for (ReferenceType param : parameter.getType().asUnionType().getElements()) {
try {
param.resolve();
} catch (UnsolvedSymbolException | UnsupportedOperationException e) {
handleParameterResolveFailure(parameter);
// since this type is unsolved, it could not be a primitive type
@ClassGetSimpleName String typeName = param.getElementType().asClassOrInterfaceType().getName().asString();
UnsolvedClass newClass = updateUnsolvedClassWithClassName(typeName, true);
updateMissingClass(newClass);
}
}
}
Expand Down Expand Up @@ -1418,7 +1453,6 @@ public void createMissingClass(UnsolvedClass missedClass) {
String filePathStr =
this.rootDirectory + classDirectory + "/" + missedClass.getClassName() + ".java";
Path filePath = Paths.get(filePathStr);

createdClass.add(filePath);
try {
Path parentPath = filePath.getParent();
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
package org.checkerframework.specimin;

import java.io.IOException;
import org.junit.Test;

/**
* This test checks if Specimin can work when the parameter of the catch clause is used in the
* associating block statement.
*/
public class LocalVarInExceptionTest {
@Test
public void runTest() throws IOException {
SpeciminTestExecutor.runTestWithoutJarPaths(
"localvarinexception",
new String[] {"com/example/Simple.java"},
new String[] {"com.example.Simple#bar()"});
}
}
15 changes: 15 additions & 0 deletions src/test/java/org/checkerframework/specimin/UnionTypeTest.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
package org.checkerframework.specimin;

import java.io.IOException;
import org.junit.Test;

/** This test checks if Specimin can work when there is an unsolved union type. */
public class UnionTypeTest {
@Test
public void runTest() throws IOException {
SpeciminTestExecutor.runTestWithoutJarPaths(
"uniontype",
new String[] {"com/example/Simple.java"},
new String[] {"com.example.Simple#bar()"});
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
package org.checkerframework.specimin;

import java.io.IOException;
import org.junit.Test;

/**
* This test checks if Specimin will not create a synthetic file for a class that already exist in
* the input codebase.
*/
public class UnsolvedFieldInExistingFile {
@Test
public void runTest() throws IOException {
SpeciminTestExecutor.runTestWithoutJarPaths(
"unsolvedFieldInExistingFile",
new String[] {"com/example/Simple.java"},
new String[] {"com.example.Simple#bar()"});
}
}
15 changes: 15 additions & 0 deletions src/test/java/org/checkerframework/specimin/VarTypeTest.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
package org.checkerframework.specimin;

import java.io.IOException;
import org.junit.Test;

/** This test checks if Specimin can work when there is the var keyword in the input test. */
public class VarTypeTest {
@Test
public void runTest() throws IOException {
SpeciminTestExecutor.runTestWithoutJarPaths(
"vartype",
new String[] {"com/example/Simple.java"},
new String[] {"com.example.Simple#bar()"});
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
package com.example;

import javalanguage.Method;

class Simple {

void bar() {
String x = "";
Method method = new Method();
try {
method.solve();
} catch (UnsupportedOperationException e) {
x = e.toString();
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
package javalanguage;

public class Method {

public Method() {
throw new Error();
}

public SolveReturnType solve() {
throw new Error();
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
package javalanguage;

public class SolveReturnType {
}
Loading

0 comments on commit eb1b1bc

Please sign in to comment.