Refactor

build.gradle

@@ -4,9 +4,9 @@ plugins {
     id 'java-library'
     id 'maven-publish'
     id 'signing'
-    id 'com.diffplug.spotless' version '6.25.0'
-    id 'org.checkerframework' version '0.6.49'
-    id("net.ltgt.errorprone") version "4.1.0"
+    id 'com.diffplug.spotless' version '7.1.0'
+    id 'org.checkerframework' version '0.6.56'
+    id 'net.ltgt.errorprone' version '4.3.0'
     id 'com.adarshr.test-logger' version '4.0.0'
 }
 
@@ -22,26 +22,26 @@ application {
 
 dependencies {
 
-    implementation 'com.github.javaparser:javaparser-symbol-solver-core:3.26.1'
+    implementation 'com.github.javaparser:javaparser-symbol-solver-core:3.27.0'
 
     implementation 'net.sf.jopt-simple:jopt-simple:5.0.4'
 
-    implementation "org.vineflower:vineflower:1.11.0"
+    implementation "org.vineflower:vineflower:1.11.1"
 
-    implementation 'commons-io:commons-io:2.18.0'
+    implementation 'commons-io:commons-io:2.19.0'
 
     // Use JUnit test framework.
     testImplementation 'junit:junit:4.13.2'
 
-    errorprone("com.google.errorprone:error_prone_core:2.35.1")
+    errorprone("com.google.errorprone:error_prone_core:2.40.0")
 }
 
 // Use require-javadoc. From https://github.com/plume-lib/require-javadoc.
 configurations {
     requireJavadoc
 }
 dependencies {
-    requireJavadoc "org.plumelib:require-javadoc:1.0.9"
+    requireJavadoc "org.plumelib:require-javadoc:2.0.0"
 }
 task requireJavadoc(type: JavaExec) {
     group = 'Documentation'

src/main/java/org/checkerframework/specimin/AmbiguityResolutionPolicy.java

@@ -0,0 +1,18 @@
+package org.checkerframework.specimin;
+
+import com.google.common.base.Ascii;
+
+public enum AmbiguityResolutionPolicy {
+  All,
+  BestEffort,
+  InputCondition;
+
+  public static AmbiguityResolutionPolicy parse(String input) {
+    return switch (Ascii.toLowerCase(input)) {
+      case "all" -> AmbiguityResolutionPolicy.All;
+      case "best-effort" -> AmbiguityResolutionPolicy.BestEffort;
+      case "input-condition" -> AmbiguityResolutionPolicy.InputCondition;
+      default -> throw new IllegalArgumentException();
+    };
+  }
+}

src/main/java/org/checkerframework/specimin/JavaLangUtils.java

@@ -273,46 +273,34 @@ private JavaLangUtils() {
    * @return the set of compatible types, such as ["boolean", "Boolean"]
    */
   public static String[] getTypesForOp(String binOp) {
-    switch (binOp) {
-      case "*":
-      case "/":
-      case "%":
-        // JLS 15.17
-        return NUMERIC_PRIMITIVES;
-      case "-":
-        // JLS 15.18
-        return NUMERIC_PRIMITIVES;
-      case "+":
-        // JLS 15.18 (see note about "+", which can also mean string concatenation!)
-        return NUMERIC_PRIMITIVES_AND_STRING;
-      case ">>":
-      case ">>>":
-      case "<<":
-        // JSL 15.19
-        return INTEGRAL_PRIMITIVES;
-      case "<":
-      case "<=":
-      case ">":
-      case ">=":
-        // JLS 15.20.1
-        return NUMERIC_PRIMITIVES;
-      case "==":
-      case "!=":
-        // JLS 15.21 says that it's an error if one of the sides of an == or != is a boolean or
-        // numeric type, but the other is not. This return value is based on that error condition.
-        return NUMERIC_PRIMITIVES_AND_BOOLEANS;
-      case "^":
-      case "&":
-      case "|":
-        // JLS 15.22
-        return NUMERIC_PRIMITIVES_AND_BOOLEANS;
-      case "||":
-      case "&&":
-        // JLS 15.23 and 15.24
-        return BOOLEANS;
-      default:
-        throw new IllegalArgumentException("unexpected binary operator: " + binOp);
-    }
+    return switch (binOp) {
+      // JLS 15.17
+      case "*", "/", "%" -> NUMERIC_PRIMITIVES;
+
+      // JLS 15.18
+      case "-" -> NUMERIC_PRIMITIVES;
+
+      // JLS 15.18 (see note about "+", which can also mean string concatenation!)
+      case "+" -> NUMERIC_PRIMITIVES_AND_STRING;
+
+      // JSL 15.19
+      case ">>", ">>>", "<<" -> INTEGRAL_PRIMITIVES;
+
+      // JLS 15.20.1
+      case "<", "<=", ">", ">=" -> NUMERIC_PRIMITIVES;
+
+      // JLS 15.21 says that it's an error if one of the sides of an == or != is a boolean or
+      // numeric type, but the other is not. This return value is based on that error condition.
+      case "==", "!=" -> NUMERIC_PRIMITIVES_AND_BOOLEANS;
+
+      // JLS 15.22
+      case "^", "&", "|" -> NUMERIC_PRIMITIVES_AND_BOOLEANS;
+
+      // JLS 15.23 and 15.24
+      case "||", "&&" -> BOOLEANS;
+
+      default -> throw new IllegalArgumentException("unexpected binary operator: " + binOp);
+    };
   }
 
   /**

src/main/java/org/checkerframework/specimin/JavaParserUtil.java

@@ -25,6 +25,8 @@
 import java.util.List;
 import java.util.Optional;
 import java.util.stream.Collectors;
+
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.signature.qual.FullyQualifiedName;
 
 /**
@@ -196,21 +198,7 @@ public static String getValueTypeFromAnnotationExpression(Expression value) {
    */
   @SuppressWarnings("signature") // result is a fully-qualified name or else this throws
   public static @FullyQualifiedName String getEnclosingClassName(Node node) {
-    Node parent = getEnclosingClassLike(node);
-
-    if (parent instanceof ClassOrInterfaceDeclaration) {
-      return ((ClassOrInterfaceDeclaration) parent).getFullyQualifiedName().orElseThrow();
-    }
-
-    if (parent instanceof EnumDeclaration) {
-      return ((EnumDeclaration) parent).getFullyQualifiedName().orElseThrow();
-    }
-
-    if (parent instanceof AnnotationDeclaration) {
-      return ((AnnotationDeclaration) parent).getFullyQualifiedName().orElseThrow();
-    }
-
-    throw new RuntimeException("unexpected kind of node: " + parent.getClass());
+    return getEnclosingClassLike(node).getFullyQualifiedName().orElseThrow();
   }
 
   /**
@@ -222,14 +210,31 @@ public static String getValueTypeFromAnnotationExpression(Expression value) {
    * @param node a node that is contained in a class-like structure
    * @return the nearest enclosing class-like node
    */
-  public static Node getEnclosingClassLike(Node node) {
+  public static TypeDeclaration<?> getEnclosingClassLike(Node node) {
     Node parent = node.getParentNode().orElseThrow();
-    while (!(parent instanceof ClassOrInterfaceDeclaration
-        || parent instanceof EnumDeclaration
-        || parent instanceof AnnotationDeclaration)) {
+    while (!(parent instanceof TypeDeclaration<?>)) {
       parent = parent.getParentNode().orElseThrow();
     }
-    return parent;
+    return (TypeDeclaration<?>) parent;
+  }
+
+  /**
+   * See {@code getEnclosingClassLike(Node)} for more details. This does not throw if a parent is
+   * not found; instead, it returns null.
+   *
+   * @param node a node that is contained in a class-like structure
+   * @return the nearest enclosing class-like node
+   */
+  public static @Nullable TypeDeclaration<?> getEnclosingClassLikeOptional(Node node) {
+    Optional<Node> parent = node.getParentNode();
+    while (parent.isPresent() && !(parent.get() instanceof TypeDeclaration<?>)) {
+      parent = parent.get().getParentNode();
+    }
+
+    if (parent.isPresent()) {
+      return (TypeDeclaration<?>) parent.get();
+    }
+    return null;
   }
 
   /**

src/main/java/org/checkerframework/specimin/Slicer.java

@@ -0,0 +1,137 @@
+package org.checkerframework.specimin;
+
+import com.github.javaparser.StaticJavaParser;
+import com.github.javaparser.ast.CompilationUnit;
+import com.github.javaparser.ast.ImportDeclaration;
+import com.github.javaparser.ast.Node;
+import com.github.javaparser.ast.PackageDeclaration;
+import com.github.javaparser.resolution.Resolvable;
+import com.github.javaparser.resolution.UnsolvedSymbolException;
+import com.github.javaparser.resolution.declarations.ResolvedReferenceTypeDeclaration;
+import java.io.IOException;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.ArrayDeque;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Queue;
+import java.util.Set;
+import org.checkerframework.specimin.unsolved.UnsolvedSymbolAlternates;
+import org.checkerframework.specimin.unsolved.UnsolvedSymbolGenerator;
+
+public class Slicer {
+  /** The slice of nodes. */
+  private final Set<Node> slice = new HashSet<>();
+
+  /**
+   * The slice of unsolved symbol definitions. These values need not be unique; the map is provided
+   * for simple lookups when adding new symbols.
+   */
+  private final Map<String, UnsolvedSymbolAlternates<?>> unsolvedSlice = new HashMap<>();
+
+  /** The Nodes that need to be processed in the main algorithm. */
+  private final Queue<Node> worklist = new ArrayDeque<>();
+
+  private final Map<String, Path> existingClassesToFilePath;
+  private final String rootDirectory;
+  private final Map<String, CompilationUnit> toSlice;
+
+  public Slicer(
+      Map<String, Path> existingClassesToFilePath,
+      String rootDirectory,
+      Map<String, CompilationUnit> toSlice) {
+    this.existingClassesToFilePath = existingClassesToFilePath;
+    this.rootDirectory = rootDirectory;
+    this.toSlice = toSlice;
+  }
+
+  public void slice() throws IOException {
+    Set<String> usedTypes = new HashSet<>();
+
+    // Step 1: build the slice; see which nodes to keep
+    while (!worklist.isEmpty()) {
+      Node element = worklist.remove();
+      handleElement(element, usedTypes);
+    }
+
+    // Step 2: add all used types
+    for (String used : usedTypes) {
+      toSlice.put(
+          used, StaticJavaParser.parse(Path.of(rootDirectory, qualifiedNameToFilePath(used))));
+    }
+
+    // Step 3: remove all nodes except the ones marked for keeping OR package/import declarations
+    for (CompilationUnit cu : toSlice.values()) {
+      sliceNode(cu);
+    }
+  }
+
+  public void addToWorklist(Node node) {
+    worklist.add(node);
+  }
+
+  private void handleElement(Node node, Set<String> usedTypes) {
+    if (slice.contains(node)) {
+      return;
+    }
+
+    if (node instanceof Resolvable<?>) {
+      Resolvable<?> asResolvable = (Resolvable<?>) node;
+
+      try {
+        Object resolved = asResolvable.resolve();
+
+        worklist.addAll(TypeRuleDependencyMap.getRelevantElements(resolved));
+        if (resolved instanceof ResolvedReferenceTypeDeclaration) {
+          String qualifiedName = ((ResolvedReferenceTypeDeclaration) resolved).getQualifiedName();
+          usedTypes.add(qualifiedName);
+        }
+
+        slice.add(node);
+      } catch (UnsolvedSymbolException ex) {
+        // Generate a synthetic type
+      }
+    } else {
+      // If it's not a resolvable node, it's going to be:
+      // 1) a non-resolvable expression (like a try {} block)
+      // 2) a type parameter
+
+      // It's guaranteed that these are relevant to the slice due to the algorithm.
+
+      // We need to add this to the slice (or we potentially face missing
+      // declarations or broken code). We also need to ask the type rule
+      // dependency map if we can break this node down further.
+
+      slice.add(node);
+    }
+
+    worklist.addAll(TypeRuleDependencyMap.getRelevantElements(node));
+  }
+
+  /**
+   * Recursively removes all nodes not in the slice.
+   *
+   * @param node The node to slice
+   */
+  private void sliceNode(Node node) {
+    if (slice.contains(node)) {
+      for (Node child : node.getChildNodes()) {
+        sliceNode(child);
+      }
+    } else if (!(node instanceof PackageDeclaration || node instanceof ImportDeclaration)) {
+      node.remove();
+    }
+  }
+
+  private String qualifiedNameToFilePath(String qualifiedName) {
+    if (!existingClassesToFilePath.containsKey(qualifiedName)) {
+      throw new RuntimeException(
+          "qualifiedNameToFilePath only works for classes in the original directory");
+    }
+    Path absoluteFilePath = existingClassesToFilePath.get(qualifiedName);
+    // theoretically rootDirectory should already be absolute as stated in README.
+    Path absoluteRootDirectory = Paths.get(rootDirectory).toAbsolutePath();
+    return absoluteRootDirectory.relativize(absoluteFilePath).toString();
+  }
+}