opprop · wmdietl · Aug 2, 2023 · Aug 2, 2023
diff --git a/build.gradle b/build.gradle
@@ -7,7 +7,7 @@ buildscript {
             // Code formatting; defines targets "spotlessApply" and "spotlessCheck".
             // https://github.com/diffplug/spotless/tags ; see tags starting "gradle/"
             // Only works on JDK 11+.
-            classpath 'com.diffplug.spotless:spotless-plugin-gradle:6.18.0'
+            classpath 'com.diffplug.spotless:spotless-plugin-gradle:6.20.0'
         }
     }
 }

diff --git a/src/ontology/OntologyAnnotatedTypeFactory.java b/src/ontology/OntologyAnnotatedTypeFactory.java
@@ -1,14 +1,15 @@
 package ontology;
 
 import checkers.inference.BaseInferenceRealTypeFactory;
-
 import com.google.common.collect.ImmutableMap;
 import com.sun.source.tree.NewArrayTree;
 import com.sun.source.tree.NewClassTree;
-
+import java.util.EnumSet;
+import java.util.Map;
+import java.util.Set;
+import javax.lang.model.element.AnnotationMirror;
 import ontology.qual.OntologyValue;
 import ontology.util.OntologyUtils;
-
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.framework.qual.TypeUseLocation;
@@ -21,12 +22,6 @@
 import org.checkerframework.framework.util.defaults.QualifierDefaults;
 import org.checkerframework.javacutil.BugInCF;
 
-import java.util.EnumSet;
-import java.util.Map;
-import java.util.Set;
-
-import javax.lang.model.element.AnnotationMirror;
-
 public class OntologyAnnotatedTypeFactory extends BaseInferenceRealTypeFactory {
 
     public OntologyAnnotatedTypeFactory(BaseTypeChecker checker, boolean isInfer) {

diff --git a/src/ontology/OntologyChecker.java b/src/ontology/OntologyChecker.java
@@ -7,7 +7,6 @@
 import checkers.inference.dataflow.InferenceAnalysis;
 import checkers.inference.dataflow.InferenceTransfer;
 import checkers.inference.model.ConstraintManager;
-
 import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 import org.checkerframework.framework.flow.CFTransfer;
 

diff --git a/src/ontology/OntologyInferenceAnnotatedTypeFactory.java b/src/ontology/OntologyInferenceAnnotatedTypeFactory.java
@@ -8,25 +8,21 @@
 import checkers.inference.VariableAnnotator;
 import checkers.inference.model.ConstantSlot;
 import checkers.inference.model.ConstraintManager;
-
 import com.sun.source.tree.NewArrayTree;
 import com.sun.source.tree.NewClassTree;
 import com.sun.source.tree.ParameterizedTypeTree;
 import com.sun.source.tree.Tree.Kind;
 import com.sun.source.util.TreePath;
-
+import javax.lang.model.element.AnnotationMirror;
 import ontology.qual.OntologyValue;
 import ontology.util.OntologyUtils;
-
 import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.LiteralTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
 
-import javax.lang.model.element.AnnotationMirror;
-
 public class OntologyInferenceAnnotatedTypeFactory extends InferenceAnnotatedTypeFactory {
 
     public OntologyInferenceAnnotatedTypeFactory(

diff --git a/src/ontology/OntologyTypeValidator.java b/src/ontology/OntologyTypeValidator.java
@@ -2,24 +2,20 @@
 
 import checkers.inference.InferenceValidator;
 import checkers.inference.InferenceVisitor;
-
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Set;
+import javax.lang.model.element.AnnotationMirror;
+import javax.tools.Diagnostic;
 import ontology.qual.Ontology;
 import ontology.qual.OntologyValue;
 import ontology.util.OntologyUtils;
-
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.framework.source.DiagMessage;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.QualifierHierarchy;
 
-import java.util.ArrayList;
-import java.util.List;
-import java.util.Set;
-
-import javax.lang.model.element.AnnotationMirror;
-import javax.tools.Diagnostic;
-
 /**
  * This class checks the well-formedness of ontology values used inside an {@link Ontology}
  * annotation. The current rules include: 1. If the type is TOP, BOTTOM, or POLY, the annotation

diff --git a/src/ontology/OntologyVisitor.java b/src/ontology/OntologyVisitor.java
@@ -3,7 +3,6 @@
 import checkers.inference.InferenceChecker;
 import checkers.inference.InferenceValidator;
 import checkers.inference.InferenceVisitor;
-
 import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 
 public class OntologyVisitor extends InferenceVisitor<OntologyChecker, BaseAnnotatedTypeFactory> {

diff --git a/src/ontology/qual/Ontology.java b/src/ontology/qual/Ontology.java
@@ -1,10 +1,9 @@
 package ontology.qual;
 
-import org.checkerframework.framework.qual.SubtypeOf;
-
 import java.lang.annotation.Documented;
 import java.lang.annotation.ElementType;
 import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
 
 @Documented
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})

diff --git a/src/ontology/solvers/backend/OntologyGraphSolvingStrategy.java b/src/ontology/solvers/backend/OntologyGraphSolvingStrategy.java
@@ -18,15 +18,7 @@
 import checkers.inference.solver.frontend.TwoQualifiersLattice;
 import checkers.inference.solver.strategy.GraphSolvingStrategy;
 import checkers.inference.solver.util.SolverEnvironment;
-
 import com.sun.tools.javac.util.Pair;
-
-import ontology.qual.OntologyValue;
-import ontology.util.OntologyUtils;
-
-import org.checkerframework.javacutil.AnnotationUtils;
-import org.checkerframework.javacutil.BugInCF;
-
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.Collection;
@@ -37,9 +29,12 @@
 import java.util.Map;
 import java.util.Map.Entry;
 import java.util.Set;
-
 import javax.annotation.processing.ProcessingEnvironment;
 import javax.lang.model.element.AnnotationMirror;
+import ontology.qual.OntologyValue;
+import ontology.util.OntologyUtils;
+import org.checkerframework.javacutil.AnnotationUtils;
+import org.checkerframework.javacutil.BugInCF;
 
 public class OntologyGraphSolvingStrategy extends GraphSolvingStrategy {
 

diff --git a/src/ontology/solvers/backend/OntologySolverEngine.java b/src/ontology/solvers/backend/OntologySolverEngine.java
@@ -6,7 +6,6 @@
 import checkers.inference.solver.strategy.GraphSolvingStrategy;
 import checkers.inference.solver.strategy.SolvingStrategy;
 import checkers.inference.solver.util.NameUtils;
-
 import ontology.solvers.backend.z3.OntologyZ3SolverFactory;
 
 public class OntologySolverEngine extends SolverEngine {

diff --git a/src/ontology/solvers/backend/z3/OntologyZ3BitVectorCodec.java b/src/ontology/solvers/backend/z3/OntologyZ3BitVectorCodec.java
@@ -1,23 +1,19 @@
 package ontology.solvers.backend.z3;
 
 import checkers.inference.solver.backend.z3.Z3BitVectorCodec;
-
-import ontology.qual.OntologyValue;
-import ontology.util.OntologyUtils;
-
-import org.checkerframework.javacutil.AnnotationUtils;
-import org.checkerframework.javacutil.BugInCF;
-
 import java.math.BigInteger;
 import java.util.Collections;
 import java.util.EnumMap;
 import java.util.EnumSet;
 import java.util.Map;
 import java.util.Map.Entry;
 import java.util.Set;
-
 import javax.annotation.processing.ProcessingEnvironment;
 import javax.lang.model.element.AnnotationMirror;
+import ontology.qual.OntologyValue;
+import ontology.util.OntologyUtils;
+import org.checkerframework.javacutil.AnnotationUtils;
+import org.checkerframework.javacutil.BugInCF;
 
 public class OntologyZ3BitVectorCodec implements Z3BitVectorCodec {
 

diff --git a/src/ontology/solvers/backend/z3/OntologyZ3FormatTranslator.java b/src/ontology/solvers/backend/z3/OntologyZ3FormatTranslator.java
@@ -10,13 +10,10 @@
 import checkers.inference.solver.backend.z3.Z3BitVectorCodec;
 import checkers.inference.solver.backend.z3.Z3BitVectorFormatTranslator;
 import checkers.inference.solver.frontend.Lattice;
-
 import com.microsoft.z3.BitVecExpr;
 import com.microsoft.z3.BoolExpr;
-
 import ontology.solvers.backend.z3.encoder.OntologyZ3BitVectorConstraintEncoderFactory;
 import ontology.util.OntologyUtils;
-
 import org.checkerframework.javacutil.AnnotationUtils;
 
 public class OntologyZ3FormatTranslator extends Z3BitVectorFormatTranslator {

diff --git a/src/ontology/solvers/backend/z3/encoder/OntologyZ3BitVectorConstraintEncoderFactory.java b/src/ontology/solvers/backend/z3/encoder/OntologyZ3BitVectorConstraintEncoderFactory.java
@@ -4,7 +4,6 @@
 import checkers.inference.solver.backend.z3.encoder.Z3BitVectorConstraintEncoderFactory;
 import checkers.inference.solver.backend.z3.encoder.Z3BitVectorSubtypeConstraintEncoder;
 import checkers.inference.solver.frontend.Lattice;
-
 import com.microsoft.z3.Context;
 
 public class OntologyZ3BitVectorConstraintEncoderFactory

diff --git a/src/ontology/solvers/backend/z3/encoder/OntologyZ3BitVectorSubtypeConstraintEncoder.java b/src/ontology/solvers/backend/z3/encoder/OntologyZ3BitVectorSubtypeConstraintEncoder.java
@@ -3,7 +3,6 @@
 import checkers.inference.solver.backend.z3.Z3BitVectorFormatTranslator;
 import checkers.inference.solver.backend.z3.encoder.Z3BitVectorSubtypeConstraintEncoder;
 import checkers.inference.solver.frontend.Lattice;
-
 import com.microsoft.z3.Context;
 
 public class OntologyZ3BitVectorSubtypeConstraintEncoder

diff --git a/src/ontology/util/OntologyStatisticUtil.java b/src/ontology/util/OntologyStatisticUtil.java
@@ -7,13 +7,6 @@
 import checkers.inference.model.Slot;
 import checkers.inference.model.SubtypeConstraint;
 import checkers.inference.model.VariableSlot;
-
-import ontology.qual.OntologyValue;
-
-import org.checkerframework.framework.type.QualifierHierarchy;
-import org.checkerframework.javacutil.AnnotationUtils;
-import org.checkerframework.javacutil.BugInCF;
-
 import java.io.File;
 import java.io.PrintWriter;
 import java.nio.charset.StandardCharsets;
@@ -26,8 +19,11 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
-
 import javax.lang.model.element.AnnotationMirror;
+import ontology.qual.OntologyValue;
+import org.checkerframework.framework.type.QualifierHierarchy;
+import org.checkerframework.javacutil.AnnotationUtils;
+import org.checkerframework.javacutil.BugInCF;
 
 public class OntologyStatisticUtil {
 
@@ -297,6 +293,7 @@ private static void recordKeyValue(StringBuilder sb, String key, String value) {
     public static class PostVerificationStatisticRecorder {
         private Set<Constraint> missingSolutionCons;
         private Set<ViolatedConsDiagnostic> violatedConsDiags;
+
         /**
          * whether store verbose informations. currently this parameter doesn't exposed to outside
          * setting, which means one may need hard reset value here if trigger verbose. Modify it if

diff --git a/src/ontology/util/OntologyUtils.java b/src/ontology/util/OntologyUtils.java
@@ -1,24 +1,21 @@
 package ontology.util;
 
-import ontology.qual.Ontology;
-import ontology.qual.OntologyValue;
-
-import org.checkerframework.javacutil.AnnotationBuilder;
-import org.checkerframework.javacutil.AnnotationUtils;
-import org.checkerframework.javacutil.BugInCF;
-import org.checkerframework.javacutil.TreeUtils;
-import org.checkerframework.javacutil.TypesUtils;
-
 import java.util.Arrays;
 import java.util.EnumSet;
-
 import javax.annotation.processing.ProcessingEnvironment;
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.ExecutableElement;
 import javax.lang.model.type.TypeKind;
 import javax.lang.model.type.TypeMirror;
 import javax.lang.model.util.Elements;
 import javax.lang.model.util.Types;
+import ontology.qual.Ontology;
+import ontology.qual.OntologyValue;
+import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.AnnotationUtils;
+import org.checkerframework.javacutil.BugInCF;
+import org.checkerframework.javacutil.TreeUtils;
+import org.checkerframework.javacutil.TypesUtils;
 
 public class OntologyUtils {
 

diff --git a/src/ontology/util/ViolatedConsDiagnostic.java b/src/ontology/util/ViolatedConsDiagnostic.java
@@ -1,10 +1,8 @@
 package ontology.util;
 
 import checkers.inference.model.SubtypeConstraint;
-
 import java.util.Collections;
 import java.util.List;
-
 import javax.lang.model.element.AnnotationMirror;
 
 public class ViolatedConsDiagnostic {

diff --git a/testing/WellFormednessTest.java b/testing/WellFormednessTest.java
@@ -4,8 +4,10 @@
 public class WellFormednessTest {
     // :: error: (type.invalid.conflicting.elements)
     @Ontology(values = {OntologyValue.POLY, OntologyValue.FORCE_3D}) String invalidPoly;
+
     // :: error: (type.invalid.conflicting.elements)
     @Ontology(values = {OntologyValue.TOP, OntologyValue.FORCE_3D}) String invalidTop;
+
     // :: error: (type.invalid.conflicting.elements)
     @Ontology(values = {OntologyValue.BOTTOM, OntologyValue.FORCE_3D}) String invalidBottom;
 }
diff --git a/tests/ontology/OntologyTest.java b/tests/ontology/OntologyTest.java
@@ -1,17 +1,14 @@
 package ontology;
 
 import checkers.inference.test.CFInferenceTest;
-
+import java.io.File;
+import java.util.ArrayList;
+import java.util.List;
 import ontology.solvers.backend.OntologySolverEngine;
-
 import org.checkerframework.framework.test.TestUtilities;
 import org.checkerframework.javacutil.Pair;
 import org.junit.runners.Parameterized.Parameters;
 
-import java.io.File;
-import java.util.ArrayList;
-import java.util.List;
-
 public class OntologyTest extends CFInferenceTest {
 
     public OntologyTest(File testFile) {