Skip to content
Draft
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
39 commits
Select commit Hold shift + click to select a range
f4ad227
upgrade to latest versions
theron-wang Jul 11, 2025
924f0ee
Refactor without unsolved symbol generation
theron-wang Jul 15, 2025
7a4adf5
make SpeciminRunner runnable
theron-wang Jul 15, 2025
637200c
unsolved symbol generation part 1
theron-wang Jul 18, 2025
9d56bff
forgot to include changes to `Slicer`
theron-wang Jul 18, 2025
cd3e6f4
add type parameter support
theron-wang Jul 18, 2025
4d5caf0
add handling for conditionals + operator in type guessing
theron-wang Jul 21, 2025
26f11f7
some fixes + best effort output
theron-wang Jul 24, 2025
224e427
add deleted files
theron-wang Jul 24, 2025
706f4a4
make it build
theron-wang Jul 24, 2025
702e4e3
fix some bugs
theron-wang Jul 25, 2025
e5e905d
more bug fixes + test case updates
theron-wang Jul 28, 2025
c6b6da1
make requested changes + add docs
theron-wang Jul 29, 2025
14e0c4c
handle array types
theron-wang Jul 29, 2025
3518456
some more bug fixes
theron-wang Jul 30, 2025
78523a7
add ambiguity case for unsolved method calls in solvable method/const…
theron-wang Jul 30, 2025
354dd2b
make some changes
theron-wang Jul 31, 2025
d4472fa
make some more changes
theron-wang Jul 31, 2025
8ead882
make comment changes from yesterday's review
theron-wang Jul 31, 2025
ead3cd4
make some fixes
theron-wang Jul 31, 2025
4c837f6
make fixes
theron-wang Jul 31, 2025
81648d5
bug fixes + short review changes
theron-wang Aug 1, 2025
6e928e0
add support for type arguments
theron-wang Aug 4, 2025
c369d72
must implement methods and other fixes
theron-wang Aug 6, 2025
14871d9
pr review changes
theron-wang Aug 6, 2025
f26bd72
fix some bugs
theron-wang Aug 8, 2025
7a6fc1c
fix anonymous classes, override in synthetic types, pr changes, lambd…
theron-wang Aug 8, 2025
02a8153
stop crashing for cases with solvable lambda constraint types
theron-wang Aug 11, 2025
093e895
small fixes and add additional test cases based on #423
theron-wang Aug 13, 2025
e60e057
super type relationships + bug fixes
theron-wang Aug 14, 2025
07bc8ea
allow inheritance for bounded wildcards and other type arguments + ja…
theron-wang Aug 15, 2025
ece78bb
fix a few bugs
theron-wang Aug 15, 2025
ebd54b3
address pr comments and start adding method reference support
theron-wang Aug 19, 2025
379da54
method references
theron-wang Aug 22, 2025
af5fa76
bug fixes + javadoc
theron-wang Aug 22, 2025
7a50937
fix must implement methods
theron-wang Sep 1, 2025
20ee324
must implement methods should generate in unsolved class + private ou…
theron-wang Sep 23, 2025
10a36ee
Merge branch 'main' of https://github.com/njit-jerse/specimin into re…
theron-wang Nov 6, 2025
03ee823
include methods that are implemented but referenced by an abstract su…
theron-wang Nov 7, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
147 changes: 144 additions & 3 deletions src/main/java/org/checkerframework/specimin/JavaParserUtil.java
Original file line number Diff line number Diff line change
Expand Up @@ -50,13 +50,16 @@
import com.github.javaparser.utils.Pair;
import com.google.common.base.Splitter;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Optional;
import java.util.Set;
import java.util.stream.Collectors;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.signature.qual.FullyQualifiedName;

Expand All @@ -81,13 +84,14 @@ private JavaParserUtil() {
* through reflection in JavaParserSymbolSolver. This field is initialized once in SpeciminRunner.
* Note that by the time you evaluate the value of this field, it should already be non-null.
*/
private static @Nullable TypeSolver typeSolver = null;
private static @MonotonicNonNull TypeSolver typeSolver = null;

/**
* Set the TypeSolver instance to be used by the JavaParserFacade.
*
* @param typeSolver the TypeSolver instance to set
*/
@EnsuresNonNull("JavaParserUtil.typeSolver")
public static void setTypeSolver(TypeSolver typeSolver) {
JavaParserUtil.typeSolver = typeSolver;
}
Expand Down Expand Up @@ -1521,8 +1525,7 @@ public static String getInitializerRHS(String variableType) {

// Don't use a map here: in case a ResolvedType is the same for different parameters, we could
// have different pieces of information (i.e., two parameters are both resolved type T, but
// the args
// could be different in the method call)
// the args could be different in the method call)
List<Pair<ResolvedType, ResolvedType>> resolvedTypeToPotentialASTTypes = new ArrayList<>();

if (methodCallParent.getParentNode().orElse(null) instanceof ReturnStmt returnStmt
Expand Down Expand Up @@ -1671,4 +1674,142 @@ public static String getInitializerRHS(String variableType) {

return null;
}

/**
* Given a list, return all subsets.
*
* @param original The original list
* @return A list of all subsets
*/
public static <T> List<List<T>> generateSubsets(List<T> original) {
List<List<T>> subsets = new ArrayList<>();
// There are 2^n - 1 subsets; each bit will determine if an element is included
int totalSubsets = 1 << original.size();

for (int i = 0; i < totalSubsets; i++) {
List<T> subset = new ArrayList<>();
for (int j = 0; j < original.size(); j++) {
if ((i & (1 << j)) != 0) {
subset.add(original.get(j));
}
}
subsets.add(subset);
}

return subsets;
}

/**
* Given a list of collections, return all combinations of elements where one element is picked
* from each collection. For example, if you input a list [[1, 2], [3]], then output [[1, 3], [2,
* 3]].
*
* @param collections The list of collections to combine
* @return A list of all combinations of elements
*/
public static <T> List<List<T>> generateAllCombinations(
List<? extends Collection<T>> collections) {
List<List<T>> combos = new ArrayList<>();
combos.add(new ArrayList<>());

for (Collection<T> set : collections) {
int stop = combos.size();
for (int i = 0; i < stop; i++) {
List<T> combination = combos.get(i);
for (T element : set) {
List<T> newCombination = new ArrayList<>(combination);
newCombination.add(element);
combos.add(newCombination);
}
}
}

// The first element will always be an empty list, so we'll remove it
combos.remove(0);

return combos;
}

/**
* Finds the closest method or lambda ancestor of a return statement. Will throw if neither is
* found, since a return statement is always located in one of these contexts.
*
* @param returnStmt The return statement
* @return The closest method or lambda ancestor (either of type MethodDeclaration or LambdaExpr)
*/
public static Node findClosestMethodOrLambdaAncestor(ReturnStmt returnStmt) {
@SuppressWarnings("unchecked")
Node ancestor =
returnStmt
.<Node>findAncestor(
n -> {
return n instanceof MethodDeclaration || n instanceof LambdaExpr;
},
Node.class)
.get();
return ancestor;
}

/**
* This method handles a very specific case: if an unsolved method call has a scope whose type is
* a supertype of the type this method is being called in, then it will try to find a method with
* the same signature in the current type or a solvable supertype.
*
* @param methodCall The method call, unsolved
* @param fqnToCompilationUnit The map of FQNs to compilation units
* @return A method declaration if found, or null if not
*/
public static @Nullable MethodDeclaration tryFindMethodDeclarationWithSameSignatureFromThisType(
MethodCallExpr methodCall, Map<String, CompilationUnit> fqnToCompilationUnit) {
if (!methodCall.hasScope()) {
return null;
}

Expression scope = methodCall.getScope().get();

Type scopeType = tryGetTypeFromExpression(scope, fqnToCompilationUnit);

if (scopeType == null) {
return null;
}

TypeDeclaration<?> enclosingClass = getEnclosingClassLike(methodCall);

List<TypeDeclaration<?>> solvableAncestors =
getAllSolvableAncestors(enclosingClass, fqnToCompilationUnit);

solvableAncestors.add(enclosingClass);

boolean isScopeTypeAnAncestor = false;
for (TypeDeclaration<?> thisOrAncestor : solvableAncestors) {
if (thisOrAncestor instanceof NodeWithExtends<?> withExtends
&& withExtends.getExtendedTypes().contains(scopeType)) {
isScopeTypeAnAncestor = true;
break;
} else if (thisOrAncestor instanceof NodeWithImplements<?> withImplements
&& withImplements.getImplementedTypes().contains(scopeType)) {
isScopeTypeAnAncestor = true;
break;
}
}

if (!isScopeTypeAnAncestor) {
return null;
}

MethodCallExpr clone = methodCall.clone();
clone.removeScope();
clone.setParentNode(methodCall.getParentNode().get());

List<MethodDeclaration> methods =
tryResolveMethodCallWithUnresolvableArguments(clone, fqnToCompilationUnit);

clone.remove();

if (methods.size() == 1) {
return methods.get(0);
}

return null;
}
}
70 changes: 69 additions & 1 deletion src/main/java/org/checkerframework/specimin/Slicer.java
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@
import com.github.javaparser.ast.body.MethodDeclaration;
import com.github.javaparser.ast.body.TypeDeclaration;
import com.github.javaparser.ast.body.VariableDeclarator;
import com.github.javaparser.ast.expr.AssignExpr;
import com.github.javaparser.ast.expr.Expression;
import com.github.javaparser.ast.expr.FieldAccessExpr;
import com.github.javaparser.ast.expr.MethodCallExpr;
Expand All @@ -24,7 +25,10 @@
import com.github.javaparser.ast.type.UnknownType;
import com.github.javaparser.resolution.Resolvable;
import com.github.javaparser.resolution.UnsolvedSymbolException;
import com.github.javaparser.resolution.declarations.ResolvedFieldDeclaration;
import com.github.javaparser.resolution.declarations.ResolvedValueDeclaration;
import com.github.javaparser.resolution.types.ResolvedType;
import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Deque;
Expand Down Expand Up @@ -69,7 +73,7 @@ public class Slicer {
* are guaranteed to be generated. Contains only select Nodes, determined by {@link
* UnsolvedSymbolGenerator#needToPostProcess(Node)}.
*/
private final Set<Node> postProcessingWorklist = new LinkedHashSet<>();
private final Deque<Node> postProcessingWorklist = new ArrayDeque<>();

/** The result of the slice, not including generated symbols. */
private final Set<CompilationUnit> resultCompilationUnits = new HashSet<>();
Expand Down Expand Up @@ -129,6 +133,8 @@ public static SliceResult slice(
}
}

unsolvedSymbolGenerator.generateAllAlternatesBasedOnSuperTypeRelationships();

slicer.prune();

return new SliceResult(
Expand All @@ -146,6 +152,8 @@ private void buildSlice() {
handleElement(element);
}

generatedSymbolSlice.addAll(unsolvedSymbolGenerator.clearMethodsWithNull());

if (!generatedSymbolSlice.isEmpty()) {
// Step 2: Add more information to generated symbols based on context
Iterator<Node> ppwIterator = postProcessingWorklist.iterator();
Expand Down Expand Up @@ -451,6 +459,66 @@ private void removeNonSliceNodes(Node node) {
for (Node child : copy) {
removeNonSliceNodes(child);
}

// If we encounter an empty final field, try to see if we've included an assignment expression
// that sets it in the slice. If not, then we need to add a default initializer.
if (node instanceof VariableDeclarator fieldDeclarator
&& fieldDeclarator.getInitializer().isEmpty()
&& fieldDeclarator.getParentNode().get() instanceof FieldDeclaration fieldDecl
&& fieldDecl.isFinal()) {
ResolvedFieldDeclaration resolved = (ResolvedFieldDeclaration) fieldDeclarator.resolve();

boolean isSet =
slice.stream()
.filter(n -> n instanceof AssignExpr)
.map(n -> (AssignExpr) n)
.filter(
assignExpr -> {
if (assignExpr.getTarget().isFieldAccessExpr()) {
try {
ResolvedValueDeclaration target =
assignExpr.getTarget().asFieldAccessExpr().resolve();

if (target.isField()) {
return target
.asField()
.declaringType()
.getQualifiedName()
.equals(resolved.declaringType().getQualifiedName())
&& target.getName().equals(resolved.getName());
}
} catch (UnsolvedSymbolException e) {
return false;
}
} else if (assignExpr.getTarget().isNameExpr()) {
try {
ResolvedValueDeclaration target =
assignExpr.getTarget().asNameExpr().resolve();

if (target.isField()) {
return target
.asField()
.declaringType()
.getQualifiedName()
.equals(resolved.declaringType().getQualifiedName())
&& target.getName().equals(resolved.getName());
}
return target.equals(resolved);
} catch (UnsolvedSymbolException e) {
return false;
}
}

return false;
})
.findFirst()
.isPresent();

if (!isSet) {
fieldDeclarator.setInitializer(
JavaParserUtil.getInitializerRHS(fieldDeclarator.getType().toString()));
}
}
}
// If a BlockStmt is being removed, it's a method/constructor to be trimmed
else if (node instanceof BlockStmt blockStmt
Expand Down
Loading
Loading