From 7d8db370a7dd1db0548c12d2ec19d1915efe3f60 Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 8 Jun 2021 23:03:49 -0400 Subject: [PATCH 1/6] make it compile --- src/backend/z3smt/Z3SmtFormatTranslator.java | 15 +++++------ src/backend/z3smt/Z3SmtSolver.java | 2 +- .../UnitsInferenceAnnotatedTypeFactory.java | 25 ++++++++++--------- src/units/UnitsInferenceViewpointAdapter.java | 2 +- src/units/UnitsVisitor.java | 4 +-- .../backend/gje/UnitsGJEFormatTranslator.java | 5 ++-- .../z3smt/UnitsZ3SmtFormatTranslator.java | 24 +++--------------- .../UnitsZ3SmtCombineConstraintEncoder.java | 9 ++++--- 8 files changed, 36 insertions(+), 50 deletions(-) diff --git a/src/backend/z3smt/Z3SmtFormatTranslator.java b/src/backend/z3smt/Z3SmtFormatTranslator.java index eee0eee..204076b 100644 --- a/src/backend/z3smt/Z3SmtFormatTranslator.java +++ b/src/backend/z3smt/Z3SmtFormatTranslator.java @@ -6,6 +6,7 @@ import checkers.inference.model.LubVariableSlot; import checkers.inference.model.RefinementVariableSlot; import checkers.inference.model.Slot; +import checkers.inference.model.SourceVariableSlot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.AbstractFormatTranslator; import checkers.inference.solver.frontend.Lattice; @@ -37,13 +38,13 @@ public final void init(Context ctx) { finishInitializingEncoders(); } - protected abstract SlotEncodingT serializeVarSlot(VariableSlot slot); + protected abstract SlotEncodingT serializeVariableSlot(VariableSlot slot); protected abstract SlotEncodingT serializeConstantSlot(ConstantSlot slot); @Override - public SlotEncodingT serialize(VariableSlot slot) { - return serializeVarSlot(slot); + public SlotEncodingT serialize(SourceVariableSlot slot) { + return serializeVariableSlot(slot); } @Override @@ -53,22 +54,22 @@ public SlotEncodingT serialize(ConstantSlot slot) { @Override public SlotEncodingT serialize(ExistentialVariableSlot slot) { - return serializeVarSlot(slot); + return serializeVariableSlot(slot); } @Override public SlotEncodingT serialize(RefinementVariableSlot slot) { - return serializeVarSlot(slot); + return serializeVariableSlot(slot); } @Override public SlotEncodingT serialize(CombVariableSlot slot) { - return serializeVarSlot(slot); + return serializeVariableSlot(slot); } @Override public SlotEncodingT serialize(LubVariableSlot slot) { - return serializeVarSlot(slot); + return serializeVariableSlot(slot); } /** diff --git a/src/backend/z3smt/Z3SmtSolver.java b/src/backend/z3smt/Z3SmtSolver.java index 6484bd1..95d2bb7 100644 --- a/src/backend/z3smt/Z3SmtSolver.java +++ b/src/backend/z3smt/Z3SmtSolver.java @@ -341,7 +341,7 @@ protected void encodeAllSlots() { // generate slot constraints for (Slot slot : slots) { - if (slot.isVariable()) { + if (slot instanceof VariableSlot) { VariableSlot varSlot = (VariableSlot) slot; BoolExpr wfConstraint = formatTranslator.encodeSlotWellformnessConstraint(varSlot); diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index a750426..7c5839f 100644 --- a/src/units/UnitsInferenceAnnotatedTypeFactory.java +++ b/src/units/UnitsInferenceAnnotatedTypeFactory.java @@ -12,6 +12,7 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.ConstraintManager; import checkers.inference.model.Slot; +import checkers.inference.model.SourceVariableSlot; import checkers.inference.model.VariableSlot; import checkers.inference.qual.VarAnnot; import checkers.inference.util.InferenceViewpointAdapter; @@ -283,12 +284,12 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { inferenceTypeFactory.getAnnotatedType(binaryTree.getLeftOperand()); AnnotatedTypeMirror rhsATM = inferenceTypeFactory.getAnnotatedType(binaryTree.getRightOperand()); - VariableSlot lhs = slotManager.getVariableSlot(lhsATM); - VariableSlot rhs = slotManager.getVariableSlot(rhsATM); + Slot lhs = slotManager.getSlot(lhsATM); + Slot rhs = slotManager.getSlot(rhsATM); // create varslot for the result of the binary tree computation // note: constraints for binary ops are added in UnitsVisitor - VariableSlot result; + Slot result; switch (binaryTree.getKind()) { case PLUS: // if it is a string concatenation, result is dimensionless @@ -329,8 +330,8 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { // add to cache Set resultSet = AnnotationUtils.createAnnotationSet(); resultSet.add(resultAM); - final Pair> varATMPair = - Pair.of(slotManager.getVariableSlot(atm), resultSet); + final Pair> varATMPair = + Pair.of(slotManager.getSlot(atm), resultSet); treeToVarAnnoPair.put(binaryTree, varATMPair); } } @@ -410,16 +411,16 @@ private void generateVarSlotForStaticFinalConstants( // if member is from source code, it must be unannotated // if member is from byte code, it must not be annotated with a // non-dimensionless unit - if ((!fromByteCode && slot.isVariable()) + if ((!fromByteCode && slot instanceof VariableSlot) || (fromByteCode - && slot.isConstant() + && slot instanceof ConstantSlot && AnnotationUtils.areSame( ((ConstantSlot) slot).getValue(), unitsRepUtils.DIMENSIONLESS))) { // Generate a fresh variable for inference AnnotationLocation loc = VariableAnnotator.treeToLocation(atypeFactory, tree); - VariableSlot varSlot = slotManager.createVariableSlot(loc); + SourceVariableSlot varSlot = slotManager.createSourceVariableSlot(loc, TreeUtils.typeOf(tree)); atm.replaceAnnotation(slotManager.getAnnotation(varSlot)); } } @@ -432,7 +433,7 @@ private void generateVarSlotForStaticFinalConstants( // @PolyAll private boolean isPolyAnnotation(AnnotationMirror annot) { Slot slot = slotManager.getSlot(annot); - if (slot.isConstant()) { + if (slot instanceof ConstantSlot) { AnnotationMirror constant = ((ConstantSlot) slot).getValue(); return InferenceQualifierHierarchy.isPolymorphic(constant); } @@ -530,13 +531,13 @@ public Void visitNewClass(NewClassTree newClassTree, AnnotatedTypeMirror atm) { // "@Poly Clazz(@Poly param)" we have the following annotations: // 1) the variable slot generated for the polymorphic declared return type - VariableSlot varSlotForPolyReturn = + SourceVariableSlot varSlotForPolyReturn = variableAnnotator.getOrCreatePolyVar(newClassTree); // disable insertion of polymorphic return variable slot varSlotForPolyReturn.setInsertable(false); // 2) the call site return type: "@m" in "new @m Clazz(...)" - VariableSlot callSiteReturnVarSlot = slotManager.getVariableSlot(atm); + Slot callSiteReturnVarSlot = slotManager.getSlot(atm); // Create a subtype constraint: callSiteReturnVarSlot <: varSlotForPolyReturn // since after annotation insertion, the varSlotForPolyReturn is conceptually a @@ -558,7 +559,7 @@ public Void visitMethodInvocation( super.visitMethodInvocation(methodInvocationTree, atm); if (isMethodDeclaredWithPolymorphicReturn(methodInvocationTree)) { - VariableSlot varSlotForPolyReturn = + SourceVariableSlot varSlotForPolyReturn = variableAnnotator.getOrCreatePolyVar(methodInvocationTree); // disable insertion of polymorphic return variable slot varSlotForPolyReturn.setInsertable(false); diff --git a/src/units/UnitsInferenceViewpointAdapter.java b/src/units/UnitsInferenceViewpointAdapter.java index fb1934f..3ac37f3 100644 --- a/src/units/UnitsInferenceViewpointAdapter.java +++ b/src/units/UnitsInferenceViewpointAdapter.java @@ -33,7 +33,7 @@ protected AnnotationMirror combineAnnotationWithAnnotation( return unitsRepUtils.BOTTOM; } Slot declSlot = InferenceMain.getInstance().getSlotManager().getSlot(declaredAnnotation); - if (declSlot.isConstant()) { + if (declSlot instanceof ConstantSlot) { ConstantSlot cs = (ConstantSlot) declSlot; if (AnnotationUtils.areSame(cs.getValue(), unitsRepUtils.RECEIVER_DEPENDANT_UNIT)) { return super.combineAnnotationWithAnnotation( diff --git a/src/units/UnitsVisitor.java b/src/units/UnitsVisitor.java index 4448536..1c6c0a3 100644 --- a/src/units/UnitsVisitor.java +++ b/src/units/UnitsVisitor.java @@ -174,8 +174,8 @@ public Void visitBinary(BinaryTree binaryTree, Void p) { break; default: // TODO: replace with LUBSlot pending mier's PR - VariableSlot lubSlot = - slotManager.getVariableSlot(atypeFactory.getAnnotatedType(binaryTree)); + Slot lubSlot = + slotManager.getSlot(atypeFactory.getAnnotatedType(binaryTree)); // Create LUB constraint by default constraintManager.addSubtypeConstraint(lhs, lubSlot); constraintManager.addSubtypeConstraint(rhs, lubSlot); diff --git a/src/units/solvers/backend/gje/UnitsGJEFormatTranslator.java b/src/units/solvers/backend/gje/UnitsGJEFormatTranslator.java index 27ce4a6..1a84af8 100644 --- a/src/units/solvers/backend/gje/UnitsGJEFormatTranslator.java +++ b/src/units/solvers/backend/gje/UnitsGJEFormatTranslator.java @@ -7,6 +7,7 @@ import checkers.inference.model.LubVariableSlot; import checkers.inference.model.RefinementVariableSlot; import checkers.inference.model.Slot; +import checkers.inference.model.SourceVariableSlot; import checkers.inference.model.VariableSlot; import checkers.inference.model.serialization.ToStringSerializer; import checkers.inference.solver.backend.AbstractFormatTranslator; @@ -63,7 +64,7 @@ protected int assignGJEVarIDs(Collection constraints) { constraint.serialize(slotsCollector); } - for (VariableSlot slot : slotsCollector.getSlots()) { + for (Slot slot : slotsCollector.getSlots()) { slotGJEtoCFIMap.put(gjeID, slot); slotCFItoGJEMap.put(slot, gjeID); System.err.println("ID: " + gjeID + " --> slot " + slot.serialize(toStringSerializer)); @@ -134,7 +135,7 @@ protected GJEInferenceUnit serializeConstantSlot(ConstantSlot slot) { } @Override - public GJEInferenceUnit serialize(VariableSlot slot) { + public GJEInferenceUnit serialize(SourceVariableSlot slot) { // System.err.println("Serializing vs " + slot); return serializeVarSlot(slot); } diff --git a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java index 8ea5f92..fd0501d 100644 --- a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java +++ b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java @@ -54,7 +54,7 @@ protected ConstraintEncoderFactory createConstraintEncoderFactory() { @Override public String generateZ3SlotDeclaration(VariableSlot slot) { - Z3InferenceUnit encodedSlot = serializeVarSlot(slot); + Z3InferenceUnit encodedSlot = serializeVariableSlot(slot); List slotDeclaration = new ArrayList<>(); @@ -90,7 +90,7 @@ private String addZ3IntDefinition(IntExpr z3IntVariable) { } @Override - protected Z3InferenceUnit serializeVarSlot(VariableSlot slot) { + protected Z3InferenceUnit serializeVariableSlot(VariableSlot slot) { int slotID = slot.getId(); if (serializedSlots.containsKey(slotID)) { @@ -153,7 +153,7 @@ protected Z3InferenceUnit serializeConstantSlot(ConstantSlot slot) { public void preAnalyzeSlots(Collection slots) { Set constantSlots = new HashSet<>(); for (Slot slot : slots) { - if (slot.isConstant()) { + if (slot instanceof ConstantSlot) { constantSlots.add((ConstantSlot) slot); } } @@ -166,30 +166,12 @@ public void preAnalyzeSlots(Collection slots) { @Override public BoolExpr encodeSlotWellformnessConstraint(VariableSlot slot) { - if (slot instanceof ConstantSlot) { - ConstantSlot cs = (ConstantSlot) slot; - AnnotationMirror anno = cs.getValue(); - // encode PolyUnit as constant trues - if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT)) { - return ctx.mkTrue(); - } - } - Z3InferenceUnit serializedSlot = slot.serialize(this); return UnitsZ3SmtEncoderUtils.slotWellformedness(ctx, serializedSlot); } @Override public BoolExpr encodeSlotPreferenceConstraint(VariableSlot slot) { - if (slot instanceof ConstantSlot) { - ConstantSlot cs = (ConstantSlot) slot; - AnnotationMirror anno = cs.getValue(); - // encode PolyUnit as constant trues - if (AnnotationUtils.areSame(anno, unitsRepUtils.POLYUNIT)) { - return ctx.mkTrue(); - } - } - Z3InferenceUnit serializedSlot = slot.serialize(this); return UnitsZ3SmtEncoderUtils.slotPreference(ctx, serializedSlot); } diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java index 7c81da5..f4d31c4 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java @@ -2,6 +2,7 @@ import backend.z3smt.Z3SmtFormatTranslator; import backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; +import checkers.inference.model.CombVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; @@ -29,7 +30,7 @@ public UnitsZ3SmtCombineConstraintEncoder( @Override public BoolExpr encodeVariable_Variable( - VariableSlot target, VariableSlot declared, VariableSlot result) { + VariableSlot target, VariableSlot declared, CombVariableSlot result) { Z3InferenceUnit decl = declared.serialize(z3SmtFormatTranslator); Z3InferenceUnit res = result.serialize(z3SmtFormatTranslator); return UnitsZ3SmtEncoderUtils.equality(ctx, decl, res); @@ -37,7 +38,7 @@ public BoolExpr encodeVariable_Variable( @Override public BoolExpr encodeVariable_Constant( - VariableSlot target, ConstantSlot declared, VariableSlot result) { + VariableSlot target, ConstantSlot declared, CombVariableSlot result) { Z3InferenceUnit tar = target.serialize(z3SmtFormatTranslator); Z3InferenceUnit decl = declared.serialize(z3SmtFormatTranslator); Z3InferenceUnit res = result.serialize(z3SmtFormatTranslator); @@ -49,7 +50,7 @@ public BoolExpr encodeVariable_Constant( @Override public BoolExpr encodeConstant_Variable( - ConstantSlot target, VariableSlot declared, VariableSlot result) { + ConstantSlot target, VariableSlot declared, CombVariableSlot result) { Z3InferenceUnit decl = declared.serialize(z3SmtFormatTranslator); Z3InferenceUnit res = result.serialize(z3SmtFormatTranslator); return UnitsZ3SmtEncoderUtils.equality(ctx, decl, res); @@ -57,7 +58,7 @@ public BoolExpr encodeConstant_Variable( @Override public BoolExpr encodeConstant_Constant( - ConstantSlot target, ConstantSlot declared, VariableSlot result) { + ConstantSlot target, ConstantSlot declared, CombVariableSlot result) { Z3InferenceUnit tar = target.serialize(z3SmtFormatTranslator); Z3InferenceUnit decl = declared.serialize(z3SmtFormatTranslator); Z3InferenceUnit res = result.serialize(z3SmtFormatTranslator); From 8342b39ab09c53dcdd02946fce8f2517a5b5e01b Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 10 Jun 2021 07:18:06 -0400 Subject: [PATCH 2/6] bug-fix; switch to python3; code reformat --- .travis.yml | 1 + build.gradle | 17 +++-- gradle/wrapper/gradle-wrapper.properties | 2 +- src/backend/z3smt/Z3SmtFormatTranslator.java | 3 + src/backend/z3smt/Z3SmtSolver.java | 6 +- src/backend/z3smt/Z3SmtSolverFactory.java | 1 + .../Z3SmtAbstractConstraintEncoder.java | 2 + .../Z3SmtConstraintEncoderFactory.java | 2 + src/units/UnitsAnnotatedTypeFactory.java | 38 ++++++----- src/units/UnitsAnnotationClassLoader.java | 7 ++- src/units/UnitsAnnotationFormatter.java | 9 ++- src/units/UnitsChecker.java | 7 ++- .../UnitsInferenceAnnotatedTypeFactory.java | 63 ++++++++++--------- src/units/UnitsInferenceViewpointAdapter.java | 7 ++- src/units/UnitsViewpointAdapter.java | 6 +- src/units/UnitsVisitor.java | 17 ++--- src/units/notusedquals/A.java | 3 +- src/units/notusedquals/N.java | 5 +- src/units/notusedquals/cd.java | 3 +- src/units/notusedquals/kPa.java | 5 +- src/units/notusedquals/kmol.java | 5 +- src/units/qual/PolyUnit.java | 3 +- src/units/qual/RDU.java | 3 +- src/units/qual/UnitsBottom.java | 3 +- src/units/qual/UnitsRep.java | 5 +- src/units/representation/TypecheckUnit.java | 3 +- .../UnitsRepresentationUtils.java | 48 +++++++------- .../solvers/backend/UnitsSolverEngine.java | 2 + .../backend/gje/UnitsGJEFormatTranslator.java | 16 +++-- .../solvers/backend/gje/UnitsGJESolver.java | 8 ++- .../backend/gje/UnitsGJESolverFactory.java | 1 + .../UnitsGJEAbstractConstraintEncoder.java | 1 + .../UnitsGJEArithmeticConstraintEncoder.java | 2 + .../UnitsGJEComparableConstraintEncoder.java | 1 + .../UnitsGJEConstraintEncoderFactory.java | 7 +++ .../gje/encoder/UnitsGJEEncoderUtils.java | 1 + .../UnitsGJEEqualityConstraintEncoder.java | 1 + .../UnitsGJESubtypeConstraintEncoder.java | 1 + .../gje/representation/GJEEquationSet.java | 6 +- .../gje/representation/GJEInferenceUnit.java | 3 +- .../z3smt/UnitsZ3SmtFormatTranslator.java | 20 +++--- .../z3smt/UnitsZ3SmtSolverFactory.java | 2 + ...UnitsZ3SmtArithmeticConstraintEncoder.java | 4 ++ .../UnitsZ3SmtCombineConstraintEncoder.java | 4 ++ ...UnitsZ3SmtComparableConstraintEncoder.java | 3 + .../UnitsZ3SmtConstraintEncoderFactory.java | 9 +++ .../z3smt/encoder/UnitsZ3SmtEncoderUtils.java | 2 + .../UnitsZ3SmtEqualityConstraintEncoder.java | 3 + .../UnitsZ3SmtSubtypeConstraintEncoder.java | 3 + .../z3smt/representation/Z3InferenceUnit.java | 4 +- src/units/util/UnitsTypecheckUtils.java | 3 +- testing/inference/GenericIterator.java | 3 +- testing/inference/JavaCollections.java | 3 +- .../inference/JavaUtilConcurrentTimeUnit.java | 3 +- testing/inference/JavaUtilDataStructures.java | 3 +- testing/inference/StaticFinalConstants.java | 3 +- testing/inference/TryWithResources.java | 3 +- .../typecheck/JavaUtilConcurrentTimeUnit.java | 3 +- testing/unsat/WhileLoopIterator.java | 3 +- tests/units/UnitsInferenceTest.java | 9 ++- tests/units/UnitsTypecheckTest.java | 7 ++- 61 files changed, 279 insertions(+), 142 deletions(-) diff --git a/.travis.yml b/.travis.yml index deadc40..81fe7eb 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,4 +1,5 @@ language: java +python: 3.8 dist: trusty jdk: - oraclejdk8 diff --git a/build.gradle b/build.gradle index 27cae70..71149c0 100644 --- a/build.gradle +++ b/build.gradle @@ -91,12 +91,17 @@ afterEvaluate { group 'Verification' systemProperties 'path.afu.scripts': "${afu}/scripts", - 'path.inference.script': "${cfi}/scripts/inference", - JDK_JAR: "${cf}/checker/dist/jdk8.jar" + 'path.inference.script': "${cfi}/scripts/inference" + + if (JavaVersion.current() == JavaVersion.VERSION_1_8) { + systemProperties +=[JDK_JAR: "${cf}/checker/dist/jdk8.jar"] + } environment "external_checker_classpath", "${units}/build/classes/java/main:${units}/build/resources/main" - jvmArgs "-Xbootclasspath/p:${cfi}/dist/javac.jar" + if (JavaVersion.current() == JavaVersion.VERSION_1_8) { + jvmArgs "-Xbootclasspath/p:${cfi}/dist/javac.jar" + } testLogging { // Always run the tests @@ -180,7 +185,7 @@ task getCodeFormatScripts() { task pythonIsInstalled(type: Exec) { description "Check that the python executable is installed." - executable = "python" + executable = "python3" args "--version" } @@ -222,7 +227,7 @@ List getJavaFilesToFormat() { task checkFormat(type: Exec, dependsOn: [getCodeFormatScripts, pythonIsInstalled], group: 'Format') { description 'Check whether the source code is properly formatted' - executable 'python' + executable 'python3' doFirst { args += "${formatScripts}/check-google-java-format.py" args += "--aosp" // 4 space indentation @@ -239,7 +244,7 @@ task checkFormat(type: Exec, dependsOn: [getCodeFormatScripts, pythonIsInstalled task reformat(type: Exec, dependsOn: [getCodeFormatScripts, pythonIsInstalled], group: 'Format') { description 'Format the Java source code' // jdk8 and checker-qual have no source, so skip - executable 'python' + executable 'python3' doFirst { args += "${formatScripts}/run-google-java-format.py" args += "--aosp" // 4 space indentation diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index 838e6bc..4e1cc9d 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,5 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-5.3-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-6.1.1-all.zip zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists diff --git a/src/backend/z3smt/Z3SmtFormatTranslator.java b/src/backend/z3smt/Z3SmtFormatTranslator.java index 204076b..7dab264 100644 --- a/src/backend/z3smt/Z3SmtFormatTranslator.java +++ b/src/backend/z3smt/Z3SmtFormatTranslator.java @@ -10,12 +10,15 @@ import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.AbstractFormatTranslator; import checkers.inference.solver.frontend.Lattice; + import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; + import java.util.Collection; import java.util.HashMap; import java.util.List; import java.util.Map; + import javax.annotation.processing.ProcessingEnvironment; import javax.lang.model.element.AnnotationMirror; diff --git a/src/backend/z3smt/Z3SmtSolver.java b/src/backend/z3smt/Z3SmtSolver.java index 95d2bb7..f26fec0 100644 --- a/src/backend/z3smt/Z3SmtSolver.java +++ b/src/backend/z3smt/Z3SmtSolver.java @@ -16,9 +16,13 @@ import checkers.inference.solver.util.SolverArg; import checkers.inference.solver.util.SolverEnvironment; import checkers.inference.solver.util.Statistics; + import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; import com.microsoft.z3.Expr; + +import org.checkerframework.javacutil.BugInCF; + import java.io.BufferedReader; import java.io.File; import java.io.IOException; @@ -27,8 +31,8 @@ import java.util.HashMap; import java.util.List; import java.util.Map; + import javax.lang.model.element.AnnotationMirror; -import org.checkerframework.javacutil.BugInCF; // TODO: make this an abstract class with common features public class Z3SmtSolver diff --git a/src/backend/z3smt/Z3SmtSolverFactory.java b/src/backend/z3smt/Z3SmtSolverFactory.java index f280f5b..830bd59 100644 --- a/src/backend/z3smt/Z3SmtSolverFactory.java +++ b/src/backend/z3smt/Z3SmtSolverFactory.java @@ -6,6 +6,7 @@ import checkers.inference.solver.backend.Solver; import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.SolverEnvironment; + import java.util.Collection; public abstract class Z3SmtSolverFactory diff --git a/src/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java b/src/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java index badc64b..a6644dc 100644 --- a/src/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java +++ b/src/backend/z3smt/encoder/Z3SmtAbstractConstraintEncoder.java @@ -1,8 +1,10 @@ package backend.z3smt.encoder; import backend.z3smt.Z3SmtFormatTranslator; + import checkers.inference.solver.backend.encoder.AbstractConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; diff --git a/src/backend/z3smt/encoder/Z3SmtConstraintEncoderFactory.java b/src/backend/z3smt/encoder/Z3SmtConstraintEncoderFactory.java index 6e79ba6..08844df 100644 --- a/src/backend/z3smt/encoder/Z3SmtConstraintEncoderFactory.java +++ b/src/backend/z3smt/encoder/Z3SmtConstraintEncoderFactory.java @@ -1,8 +1,10 @@ package backend.z3smt.encoder; import backend.z3smt.Z3SmtFormatTranslator; + import checkers.inference.solver.backend.encoder.AbstractConstraintEncoderFactory; import checkers.inference.solver.frontend.Lattice; + import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; diff --git a/src/units/UnitsAnnotatedTypeFactory.java b/src/units/UnitsAnnotatedTypeFactory.java index 30dc995..943c1a0 100644 --- a/src/units/UnitsAnnotatedTypeFactory.java +++ b/src/units/UnitsAnnotatedTypeFactory.java @@ -2,15 +2,7 @@ import com.sun.source.tree.BinaryTree; import com.sun.source.tree.Tree.Kind; -import java.lang.annotation.Annotation; -import java.util.Collections; -import java.util.HashMap; -import java.util.HashSet; -import java.util.LinkedHashSet; -import java.util.Map; -import java.util.Map.Entry; -import java.util.Set; -import javax.lang.model.element.AnnotationMirror; + import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.qual.LiteralKind; @@ -34,9 +26,9 @@ import org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory; import org.checkerframework.framework.util.defaults.QualifierDefaults; import org.checkerframework.javacutil.AnnotationUtils; -import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.UserError; + import units.qual.BaseUnit; import units.qual.PolyUnit; import units.qual.RDU; @@ -45,6 +37,17 @@ import units.representation.UnitsRepresentationUtils; import units.util.UnitsTypecheckUtils; +import java.lang.annotation.Annotation; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.LinkedHashSet; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Set; + +import javax.lang.model.element.AnnotationMirror; + public class UnitsAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { // static reference to the singleton instance protected static UnitsRepresentationUtils unitsRepUtils; @@ -90,7 +93,7 @@ public AnnotationMirror canonicalAnnotation(AnnotationMirror anno) { // check to see if it is an internal units annotation if (AnnotationUtils.areSameByClass(anno, UnitsRep.class)) { // fill in missing base units - return anno; //unitsRepUtils.fillMissingBaseUnits(anno); + return anno; // unitsRepUtils.fillMissingBaseUnits(anno); } // check to see if it's a surface annotation such as @m or @UnknownUnits @@ -125,7 +128,7 @@ public boolean isSupportedQualifier(AnnotationMirror anno) { return false; } if (AnnotationUtils.areSameByClass(anno, UnitsRep.class)) { - return true; + return true; } if (AnnotationUtils.areSameByClass(anno, PolyUnit.class)) { return true; @@ -202,7 +205,8 @@ protected Set findBottoms( } /** - * Programmatically set {@link UnitsRepresentationUtils#POLYUNIT} as the polymorphic qualifiers + * Programmatically set {@link UnitsRepresentationUtils#POLYUNIT} as the polymorphic + * qualifiers */ @Override protected void addPolyRelations( @@ -272,8 +276,8 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { if (AnnotationUtils.areSameByClass(subAnno, UnitsRep.class) && AnnotationUtils.areSameByClass(superAnno, UnitsRep.class)) { - return AnnotationUtils.areSame(subAnno, superAnno); - //return UnitsTypecheckUtils.unitsEqual(subAnno, superAnno); + return AnnotationUtils.areSame(subAnno, superAnno); + // return UnitsTypecheckUtils.unitsEqual(subAnno, superAnno); // if (AnnotationUtils.areSame(superAnno, unitsRepUtils.METER)) { // System.err.println(" === checking SUBTYPE \n " @@ -282,9 +286,9 @@ public boolean isSubtype(AnnotationMirror subAnno, AnnotationMirror superAnno) { // + " result: " + result); // } - //return result; + // return result; } - + return true; } } diff --git a/src/units/UnitsAnnotationClassLoader.java b/src/units/UnitsAnnotationClassLoader.java index b28421c..76b68ff 100644 --- a/src/units/UnitsAnnotationClassLoader.java +++ b/src/units/UnitsAnnotationClassLoader.java @@ -1,13 +1,16 @@ package units; -import java.lang.annotation.Annotation; -import javax.lang.model.element.AnnotationMirror; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.type.AnnotationClassLoader; + import units.qual.BaseUnit; import units.qual.UnitsAlias; import units.representation.UnitsRepresentationUtils; +import java.lang.annotation.Annotation; + +import javax.lang.model.element.AnnotationMirror; + public class UnitsAnnotationClassLoader extends AnnotationClassLoader { public UnitsAnnotationClassLoader(BaseTypeChecker checker) { diff --git a/src/units/UnitsAnnotationFormatter.java b/src/units/UnitsAnnotationFormatter.java index acd67fb..1763f9a 100644 --- a/src/units/UnitsAnnotationFormatter.java +++ b/src/units/UnitsAnnotationFormatter.java @@ -1,12 +1,15 @@ package units; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.util.DefaultAnnotationFormatter; + +import units.representation.UnitsRepresentationUtils; + import java.util.List; + import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.AnnotationValue; import javax.lang.model.element.VariableElement; -import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.framework.util.DefaultAnnotationFormatter; -import units.representation.UnitsRepresentationUtils; public class UnitsAnnotationFormatter extends DefaultAnnotationFormatter { diff --git a/src/units/UnitsChecker.java b/src/units/UnitsChecker.java index 45f3215..705528e 100644 --- a/src/units/UnitsChecker.java +++ b/src/units/UnitsChecker.java @@ -5,13 +5,16 @@ import checkers.inference.InferrableChecker; import checkers.inference.SlotManager; import checkers.inference.model.ConstraintManager; -import java.lang.annotation.Annotation; -import java.util.Set; + import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.framework.qual.StubFiles; import org.checkerframework.framework.source.SupportedOptions; + import units.representation.UnitsRepresentationUtils; +import java.lang.annotation.Annotation; +import java.util.Set; + @StubFiles({ "JavaBoxedPrimitives.astub", "JavaIOPrintstream.astub", diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index 7c5839f..0ca58ee 100644 --- a/src/units/UnitsInferenceAnnotatedTypeFactory.java +++ b/src/units/UnitsInferenceAnnotatedTypeFactory.java @@ -16,6 +16,7 @@ import checkers.inference.model.VariableSlot; import checkers.inference.qual.VarAnnot; import checkers.inference.util.InferenceViewpointAdapter; + import com.sun.source.tree.BinaryTree; import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.IdentifierTree; @@ -24,15 +25,7 @@ import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.NewClassTree; import com.sun.source.tree.Tree; -import java.lang.annotation.Annotation; -import java.util.Collection; -import java.util.HashSet; -import java.util.Map; -import java.util.Set; -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.Element; -import javax.lang.model.element.ExecutableElement; -import javax.lang.model.element.Name; + import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeFormatter; @@ -52,8 +45,19 @@ import org.checkerframework.javacutil.Pair; import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.UserError; + import units.representation.UnitsRepresentationUtils; +import java.util.Collection; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Name; + public class UnitsInferenceAnnotatedTypeFactory extends InferenceAnnotatedTypeFactory { // static reference to the singleton instance protected static UnitsRepresentationUtils unitsRepUtils; @@ -96,25 +100,25 @@ protected AnnotationClassLoader createAnnotationClassLoader() { return new UnitsAnnotationClassLoader(checker); } -// // In Inference ATF, this returns the set of real qualifiers -// @Override -// protected Set> createSupportedTypeQualifiers() { -// // get all the loaded annotations -// Set> qualSet = new HashSet>(); -// // Super grabs all supported qualifiers from the real qualifier hierarchy -// // and also puts in VarAnnot -// qualSet.addAll(super.createSupportedTypeQualifiers()); -// -// // System.err.println( " --- quals = " + qualSet ); -// -// // // load all the external units -// // loadAllExternalUnits(); -// // -// // // copy all loaded external Units to qual set -// // qualSet.addAll(externalQualsMap.values()); -// -// return qualSet; -// } + // // In Inference ATF, this returns the set of real qualifiers + // @Override + // protected Set> createSupportedTypeQualifiers() { + // // get all the loaded annotations + // Set> qualSet = new HashSet>(); + // // Super grabs all supported qualifiers from the real qualifier hierarchy + // // and also puts in VarAnnot + // qualSet.addAll(super.createSupportedTypeQualifiers()); + // + // // System.err.println( " --- quals = " + qualSet ); + // + // // // load all the external units + // // loadAllExternalUnits(); + // // + // // // copy all loaded external Units to qual set + // // qualSet.addAll(externalQualsMap.values()); + // + // return qualSet; + // } // In Inference ATF, this returns the alias for a given real qualifier @Override @@ -420,7 +424,8 @@ private void generateVarSlotForStaticFinalConstants( // Generate a fresh variable for inference AnnotationLocation loc = VariableAnnotator.treeToLocation(atypeFactory, tree); - SourceVariableSlot varSlot = slotManager.createSourceVariableSlot(loc, TreeUtils.typeOf(tree)); + SourceVariableSlot varSlot = + slotManager.createSourceVariableSlot(loc, TreeUtils.typeOf(tree)); atm.replaceAnnotation(slotManager.getAnnotation(varSlot)); } } diff --git a/src/units/UnitsInferenceViewpointAdapter.java b/src/units/UnitsInferenceViewpointAdapter.java index 3ac37f3..13b12ad 100644 --- a/src/units/UnitsInferenceViewpointAdapter.java +++ b/src/units/UnitsInferenceViewpointAdapter.java @@ -4,13 +4,16 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; import checkers.inference.util.InferenceViewpointAdapter; -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.Element; + import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.javacutil.AnnotationUtils; + import units.representation.UnitsRepresentationUtils; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; + public class UnitsInferenceViewpointAdapter extends InferenceViewpointAdapter { // static reference to the singleton instance diff --git a/src/units/UnitsViewpointAdapter.java b/src/units/UnitsViewpointAdapter.java index dc9076b..b347fdd 100644 --- a/src/units/UnitsViewpointAdapter.java +++ b/src/units/UnitsViewpointAdapter.java @@ -1,13 +1,15 @@ package units; -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.Element; import org.checkerframework.framework.type.AbstractViewpointAdapter; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.javacutil.AnnotationUtils; + import units.representation.UnitsRepresentationUtils; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; + public class UnitsViewpointAdapter extends AbstractViewpointAdapter { // static reference to the singleton instance diff --git a/src/units/UnitsVisitor.java b/src/units/UnitsVisitor.java index 1c6c0a3..cd639a0 100644 --- a/src/units/UnitsVisitor.java +++ b/src/units/UnitsVisitor.java @@ -11,19 +11,22 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.ConstraintManager; import checkers.inference.model.Slot; -import checkers.inference.model.VariableSlot; + import com.sun.source.tree.BinaryTree; import com.sun.source.tree.Tree.Kind; import com.sun.source.tree.TypeCastTree; import com.sun.source.tree.UnaryTree; -import java.util.Set; -import javax.lang.model.element.AnnotationMirror; + import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.TreeUtils; + import units.representation.UnitsRepresentationUtils; -import units.util.UnitsTypecheckUtils; + +import java.util.Set; + +import javax.lang.model.element.AnnotationMirror; public class UnitsVisitor extends InferenceVisitor { @@ -174,8 +177,7 @@ public Void visitBinary(BinaryTree binaryTree, Void p) { break; default: // TODO: replace with LUBSlot pending mier's PR - Slot lubSlot = - slotManager.getSlot(atypeFactory.getAnnotatedType(binaryTree)); + Slot lubSlot = slotManager.getSlot(atypeFactory.getAnnotatedType(binaryTree)); // Create LUB constraint by default constraintManager.addSubtypeConstraint(lhs, lubSlot); constraintManager.addSubtypeConstraint(rhs, lubSlot); @@ -264,7 +266,8 @@ public Void visitTypeCast(TypeCastTree node, Void p) { UnitsRepresentationUtils.getInstance().TOP); // If expression type is dimensionless, permit it to be casted to anything - if (AnnotationUtils.areSame(exprType, UnitsRepresentationUtils.getInstance().DIMENSIONLESS)) { + if (AnnotationUtils.areSame( + exprType, UnitsRepresentationUtils.getInstance().DIMENSIONLESS)) { if (atypeFactory.getDependentTypesHelper() != null) { AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node); atypeFactory.getDependentTypesHelper().checkType(type, node.getType()); diff --git a/src/units/notusedquals/A.java b/src/units/notusedquals/A.java index f0a023f..8fac524 100644 --- a/src/units/notusedquals/A.java +++ b/src/units/notusedquals/A.java @@ -1,11 +1,12 @@ package units.notusedquals; +import units.qual.BaseUnit; + import java.lang.annotation.Documented; import java.lang.annotation.ElementType; import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; -import units.qual.BaseUnit; /** * Ampere. diff --git a/src/units/notusedquals/N.java b/src/units/notusedquals/N.java index dcebaec..b94e6fe 100644 --- a/src/units/notusedquals/N.java +++ b/src/units/notusedquals/N.java @@ -1,12 +1,13 @@ package units.notusedquals; +import units.qual.BUC; +import units.qual.UnitsAlias; + import java.lang.annotation.Documented; import java.lang.annotation.ElementType; import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; -import units.qual.BUC; -import units.qual.UnitsAlias; /** * Newton. diff --git a/src/units/notusedquals/cd.java b/src/units/notusedquals/cd.java index 85b730e..20a8877 100644 --- a/src/units/notusedquals/cd.java +++ b/src/units/notusedquals/cd.java @@ -1,11 +1,12 @@ package units.notusedquals; +import units.qual.BaseUnit; + import java.lang.annotation.Documented; import java.lang.annotation.ElementType; import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; -import units.qual.BaseUnit; /** * candela. diff --git a/src/units/notusedquals/kPa.java b/src/units/notusedquals/kPa.java index 45c8ddc..b0a7e86 100644 --- a/src/units/notusedquals/kPa.java +++ b/src/units/notusedquals/kPa.java @@ -1,12 +1,13 @@ package units.notusedquals; +import units.qual.BUC; +import units.qual.UnitsAlias; + import java.lang.annotation.Documented; import java.lang.annotation.ElementType; import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; -import units.qual.BUC; -import units.qual.UnitsAlias; /** * A kilopascal. diff --git a/src/units/notusedquals/kmol.java b/src/units/notusedquals/kmol.java index c2b58db..25bbd47 100644 --- a/src/units/notusedquals/kmol.java +++ b/src/units/notusedquals/kmol.java @@ -1,12 +1,13 @@ package units.notusedquals; +import units.qual.BUC; +import units.qual.UnitsAlias; + import java.lang.annotation.Documented; import java.lang.annotation.ElementType; import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; -import units.qual.BUC; -import units.qual.UnitsAlias; /** * kili mol. diff --git a/src/units/qual/PolyUnit.java b/src/units/qual/PolyUnit.java index 9223083..a65f9ce 100644 --- a/src/units/qual/PolyUnit.java +++ b/src/units/qual/PolyUnit.java @@ -1,11 +1,12 @@ package units.qual; +import org.checkerframework.framework.qual.PolymorphicQualifier; + import java.lang.annotation.Documented; import java.lang.annotation.ElementType; import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; -import org.checkerframework.framework.qual.PolymorphicQualifier; /** * A polymorphic qualifier for the units-of-measure type system implemented by the Units Checker. diff --git a/src/units/qual/RDU.java b/src/units/qual/RDU.java index 6be2671..098b32d 100644 --- a/src/units/qual/RDU.java +++ b/src/units/qual/RDU.java @@ -1,11 +1,12 @@ package units.qual; +import org.checkerframework.framework.qual.SubtypeOf; + import java.lang.annotation.Documented; import java.lang.annotation.ElementType; import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; -import org.checkerframework.framework.qual.SubtypeOf; /** * UnitReceiverDependant is the top type of the type hierarchy. diff --git a/src/units/qual/UnitsBottom.java b/src/units/qual/UnitsBottom.java index baa0d63..14ebe75 100644 --- a/src/units/qual/UnitsBottom.java +++ b/src/units/qual/UnitsBottom.java @@ -3,12 +3,13 @@ import static org.checkerframework.framework.qual.TypeUseLocation.EXPLICIT_LOWER_BOUND; import static org.checkerframework.framework.qual.TypeUseLocation.EXPLICIT_UPPER_BOUND; +import org.checkerframework.framework.qual.TargetLocations; + import java.lang.annotation.Documented; import java.lang.annotation.ElementType; import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; -import org.checkerframework.framework.qual.TargetLocations; /** * The bottom type in the Units type system. Programmers should rarely write this type. diff --git a/src/units/qual/UnitsRep.java b/src/units/qual/UnitsRep.java index 16ca5be..2f4c249 100644 --- a/src/units/qual/UnitsRep.java +++ b/src/units/qual/UnitsRep.java @@ -1,12 +1,13 @@ package units.qual; +import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.SubtypeOf; + import java.lang.annotation.Documented; import java.lang.annotation.ElementType; import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; -import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; -import org.checkerframework.framework.qual.SubtypeOf; /** * Internal representation of a Unit, used as the core annotation mirror diff --git a/src/units/representation/TypecheckUnit.java b/src/units/representation/TypecheckUnit.java index db35df7..3101407 100644 --- a/src/units/representation/TypecheckUnit.java +++ b/src/units/representation/TypecheckUnit.java @@ -1,8 +1,9 @@ package units.representation; +import org.checkerframework.javacutil.BugInCF; + import java.util.Map; import java.util.Objects; -import org.checkerframework.javacutil.BugInCF; /** * A data structure class to encapsulate a set of java variables representing a unit for type diff --git a/src/units/representation/UnitsRepresentationUtils.java b/src/units/representation/UnitsRepresentationUtils.java index 8836e82..4a5b73f 100644 --- a/src/units/representation/UnitsRepresentationUtils.java +++ b/src/units/representation/UnitsRepresentationUtils.java @@ -2,6 +2,22 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.solver.util.Statistics; + +import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; +import org.checkerframework.javacutil.AnnotationBuilder; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.BugInCF; + +import units.UnitsAnnotatedTypeFactory; +import units.qual.BUC; +import units.qual.Dimensionless; +import units.qual.PolyUnit; +import units.qual.RDU; +import units.qual.UnitsAlias; +import units.qual.UnitsBottom; +import units.qual.UnitsRep; +import units.qual.UnknownUnits; + import java.lang.annotation.Annotation; import java.util.ArrayList; import java.util.Collections; @@ -15,22 +31,10 @@ import java.util.TreeMap; import java.util.TreeSet; import java.util.stream.Collectors; + import javax.annotation.processing.ProcessingEnvironment; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.util.Elements; -import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; -import org.checkerframework.javacutil.AnnotationBuilder; -import org.checkerframework.javacutil.AnnotationUtils; -import org.checkerframework.javacutil.BugInCF; -import units.UnitsAnnotatedTypeFactory; -import units.qual.BUC; -import units.qual.Dimensionless; -import units.qual.PolyUnit; -import units.qual.RDU; -import units.qual.UnitsAlias; -import units.qual.UnitsBottom; -import units.qual.UnitsRep; -import units.qual.UnknownUnits; /** * Utility class containing logic for creating and converting internal representations of units @@ -76,7 +80,7 @@ public class UnitsRepresentationUtils { * Instances of time units for use with various time APIs, used by {@link * UnitsAnnotatedTypeFactory#UnitsImplicitsTreeAnnotator} */ -// public AnnotationMirror SECOND, MILLISECOND, MICROSECOND, NANOSECOND; + // public AnnotationMirror SECOND, MILLISECOND, MICROSECOND, NANOSECOND; // Comparator used to sort annotation classes by their simple class name private static Comparator> annoClassComparator = @@ -249,13 +253,13 @@ public void postInit() { SURFACE_TOP = AnnotationBuilder.fromClass(elements, UnknownUnits.class); SURFACE_BOTTOM = AnnotationBuilder.fromClass(elements, UnitsBottom.class); -// -// Map secondBaseMap = createZeroFilledBaseUnitsMap(); -// secondBaseMap.put("s", 1); -// SECOND = createInternalUnit(false, false, 0, secondBaseMap); -// MILLISECOND = createInternalUnit(false, false, -3, secondBaseMap); -// MICROSECOND = createInternalUnit(false, false, -6, secondBaseMap); -// NANOSECOND = createInternalUnit(false, false, -9, secondBaseMap); + // + // Map secondBaseMap = createZeroFilledBaseUnitsMap(); + // secondBaseMap.put("s", 1); + // SECOND = createInternalUnit(false, false, 0, secondBaseMap); + // MILLISECOND = createInternalUnit(false, false, -3, secondBaseMap); + // MICROSECOND = createInternalUnit(false, false, -6, secondBaseMap); + // NANOSECOND = createInternalUnit(false, false, -9, secondBaseMap); // for (Entry entry : unitsAnnotationMirrorMap // .entrySet()) { @@ -493,7 +497,7 @@ public TypecheckUnit createTypecheckUnit(AnnotationMirror anno) { if (typecheckUnitCache.containsKey(anno)) { return typecheckUnitCache.get(anno); } - + TypecheckUnit unit = new TypecheckUnit(); // if it is a polyunit or rdu annotation, generate top diff --git a/src/units/solvers/backend/UnitsSolverEngine.java b/src/units/solvers/backend/UnitsSolverEngine.java index 3b9fd1d..33287d7 100644 --- a/src/units/solvers/backend/UnitsSolverEngine.java +++ b/src/units/solvers/backend/UnitsSolverEngine.java @@ -2,7 +2,9 @@ import checkers.inference.solver.SolverEngine; import checkers.inference.solver.backend.SolverFactory; + import org.checkerframework.javacutil.BugInCF; + import units.solvers.backend.gje.UnitsGJESolverFactory; import units.solvers.backend.z3smt.UnitsZ3SmtSolverFactory; diff --git a/src/units/solvers/backend/gje/UnitsGJEFormatTranslator.java b/src/units/solvers/backend/gje/UnitsGJEFormatTranslator.java index 1a84af8..6805f1c 100644 --- a/src/units/solvers/backend/gje/UnitsGJEFormatTranslator.java +++ b/src/units/solvers/backend/gje/UnitsGJEFormatTranslator.java @@ -14,19 +14,23 @@ import checkers.inference.solver.backend.encoder.ConstraintEncoderFactory; import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.PrintUtils.UniqueSlotCollector; -import java.util.Collection; -import java.util.HashMap; -import java.util.List; -import java.util.Map; -import javax.annotation.processing.ProcessingEnvironment; -import javax.lang.model.element.AnnotationMirror; + import org.checkerframework.javacutil.AnnotationUtils; + import units.representation.TypecheckUnit; import units.representation.UnitsRepresentationUtils; import units.solvers.backend.gje.encoder.UnitsGJEConstraintEncoderFactory; import units.solvers.backend.gje.representation.GJEEquationSet; import units.solvers.backend.gje.representation.GJEInferenceUnit; +import java.util.Collection; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +import javax.annotation.processing.ProcessingEnvironment; +import javax.lang.model.element.AnnotationMirror; + // AbstractFormatTranslator public class UnitsGJEFormatTranslator extends AbstractFormatTranslator { diff --git a/src/units/solvers/backend/gje/UnitsGJESolver.java b/src/units/solvers/backend/gje/UnitsGJESolver.java index 49b4f30..02ec1c1 100644 --- a/src/units/solvers/backend/gje/UnitsGJESolver.java +++ b/src/units/solvers/backend/gje/UnitsGJESolver.java @@ -8,6 +8,11 @@ import checkers.inference.solver.util.FileUtils; import checkers.inference.solver.util.SolverEnvironment; import checkers.inference.solver.util.Statistics; + +import org.checkerframework.javacutil.BugInCF; + +import units.solvers.backend.gje.representation.GJEEquationSet; + import java.io.BufferedReader; import java.io.File; import java.io.IOException; @@ -21,9 +26,8 @@ import java.util.Set; import java.util.TreeSet; import java.util.logging.Logger; + import javax.lang.model.element.AnnotationMirror; -import org.checkerframework.javacutil.BugInCF; -import units.solvers.backend.gje.representation.GJEEquationSet; // GaussJordanElimination solver public class UnitsGJESolver extends Solver { diff --git a/src/units/solvers/backend/gje/UnitsGJESolverFactory.java b/src/units/solvers/backend/gje/UnitsGJESolverFactory.java index 1f255a2..26ce21e 100644 --- a/src/units/solvers/backend/gje/UnitsGJESolverFactory.java +++ b/src/units/solvers/backend/gje/UnitsGJESolverFactory.java @@ -6,6 +6,7 @@ import checkers.inference.solver.backend.Solver; import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.SolverEnvironment; + import java.util.Collection; public class UnitsGJESolverFactory extends AbstractSolverFactory { diff --git a/src/units/solvers/backend/gje/encoder/UnitsGJEAbstractConstraintEncoder.java b/src/units/solvers/backend/gje/encoder/UnitsGJEAbstractConstraintEncoder.java index c16066f..ffb30ae 100644 --- a/src/units/solvers/backend/gje/encoder/UnitsGJEAbstractConstraintEncoder.java +++ b/src/units/solvers/backend/gje/encoder/UnitsGJEAbstractConstraintEncoder.java @@ -2,6 +2,7 @@ import checkers.inference.solver.backend.encoder.AbstractConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import units.solvers.backend.gje.UnitsGJEFormatTranslator; import units.solvers.backend.gje.representation.GJEEquationSet; diff --git a/src/units/solvers/backend/gje/encoder/UnitsGJEArithmeticConstraintEncoder.java b/src/units/solvers/backend/gje/encoder/UnitsGJEArithmeticConstraintEncoder.java index be0205d..aa9e02d 100644 --- a/src/units/solvers/backend/gje/encoder/UnitsGJEArithmeticConstraintEncoder.java +++ b/src/units/solvers/backend/gje/encoder/UnitsGJEArithmeticConstraintEncoder.java @@ -7,7 +7,9 @@ import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import org.checkerframework.javacutil.BugInCF; + import units.solvers.backend.gje.UnitsGJEFormatTranslator; import units.solvers.backend.gje.representation.GJEEquationSet; import units.util.UnitsTypecheckUtils; diff --git a/src/units/solvers/backend/gje/encoder/UnitsGJEComparableConstraintEncoder.java b/src/units/solvers/backend/gje/encoder/UnitsGJEComparableConstraintEncoder.java index 2705b76..986da12 100644 --- a/src/units/solvers/backend/gje/encoder/UnitsGJEComparableConstraintEncoder.java +++ b/src/units/solvers/backend/gje/encoder/UnitsGJEComparableConstraintEncoder.java @@ -5,6 +5,7 @@ import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import units.solvers.backend.gje.UnitsGJEFormatTranslator; import units.solvers.backend.gje.representation.GJEEquationSet; diff --git a/src/units/solvers/backend/gje/encoder/UnitsGJEConstraintEncoderFactory.java b/src/units/solvers/backend/gje/encoder/UnitsGJEConstraintEncoderFactory.java index b195f13..88c83ae 100644 --- a/src/units/solvers/backend/gje/encoder/UnitsGJEConstraintEncoderFactory.java +++ b/src/units/solvers/backend/gje/encoder/UnitsGJEConstraintEncoderFactory.java @@ -2,6 +2,7 @@ import checkers.inference.solver.backend.encoder.AbstractConstraintEncoderFactory; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; +import checkers.inference.solver.backend.encoder.ComparisonConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; @@ -11,6 +12,7 @@ import checkers.inference.solver.backend.encoder.implication.ImplicationConstraintEncoder; import checkers.inference.solver.backend.encoder.preference.PreferenceConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import units.solvers.backend.gje.UnitsGJEFormatTranslator; import units.solvers.backend.gje.representation.GJEEquationSet; @@ -72,4 +74,9 @@ public ImplicationConstraintEncoder createImplicationConstraintE public ArithmeticConstraintEncoder createArithmeticConstraintEncoder() { return new UnitsGJEArithmeticConstraintEncoder(lattice, formatTranslator); } + + @Override + public ComparisonConstraintEncoder createComparisonConstraintEncoder() { + return null; + } } diff --git a/src/units/solvers/backend/gje/encoder/UnitsGJEEncoderUtils.java b/src/units/solvers/backend/gje/encoder/UnitsGJEEncoderUtils.java index 34cb7ae..f7b0538 100644 --- a/src/units/solvers/backend/gje/encoder/UnitsGJEEncoderUtils.java +++ b/src/units/solvers/backend/gje/encoder/UnitsGJEEncoderUtils.java @@ -1,6 +1,7 @@ package units.solvers.backend.gje.encoder; import org.checkerframework.javacutil.BugInCF; + import units.representation.UnitsRepresentationUtils; import units.solvers.backend.gje.representation.GJEEquationSet; import units.solvers.backend.gje.representation.GJEInferenceUnit; diff --git a/src/units/solvers/backend/gje/encoder/UnitsGJEEqualityConstraintEncoder.java b/src/units/solvers/backend/gje/encoder/UnitsGJEEqualityConstraintEncoder.java index daabd51..40710ac 100644 --- a/src/units/solvers/backend/gje/encoder/UnitsGJEEqualityConstraintEncoder.java +++ b/src/units/solvers/backend/gje/encoder/UnitsGJEEqualityConstraintEncoder.java @@ -5,6 +5,7 @@ import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import units.solvers.backend.gje.UnitsGJEFormatTranslator; import units.solvers.backend.gje.representation.GJEEquationSet; diff --git a/src/units/solvers/backend/gje/encoder/UnitsGJESubtypeConstraintEncoder.java b/src/units/solvers/backend/gje/encoder/UnitsGJESubtypeConstraintEncoder.java index 2a61d85..3682606 100644 --- a/src/units/solvers/backend/gje/encoder/UnitsGJESubtypeConstraintEncoder.java +++ b/src/units/solvers/backend/gje/encoder/UnitsGJESubtypeConstraintEncoder.java @@ -5,6 +5,7 @@ import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import units.solvers.backend.gje.UnitsGJEFormatTranslator; import units.solvers.backend.gje.representation.GJEEquationSet; diff --git a/src/units/solvers/backend/gje/representation/GJEEquationSet.java b/src/units/solvers/backend/gje/representation/GJEEquationSet.java index 77567ea..0342331 100644 --- a/src/units/solvers/backend/gje/representation/GJEEquationSet.java +++ b/src/units/solvers/backend/gje/representation/GJEEquationSet.java @@ -1,13 +1,15 @@ package units.solvers.backend.gje.representation; +import org.checkerframework.javacutil.BugInCF; + +import units.representation.UnitsRepresentationUtils; + import java.util.HashMap; import java.util.HashSet; import java.util.Map; import java.util.Map.Entry; import java.util.Objects; import java.util.Set; -import org.checkerframework.javacutil.BugInCF; -import units.representation.UnitsRepresentationUtils; public class GJEEquationSet { diff --git a/src/units/solvers/backend/gje/representation/GJEInferenceUnit.java b/src/units/solvers/backend/gje/representation/GJEInferenceUnit.java index e0923a2..b5e8a63 100644 --- a/src/units/solvers/backend/gje/representation/GJEInferenceUnit.java +++ b/src/units/solvers/backend/gje/representation/GJEInferenceUnit.java @@ -1,8 +1,9 @@ package units.solvers.backend.gje.representation; +import units.representation.UnitsRepresentationUtils; + import java.util.Map; import java.util.Objects; -import units.representation.UnitsRepresentationUtils; /** * A data structure class to encapsulate a set of variables representing a unit for inference diff --git a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java index fd0501d..6b6d39a 100644 --- a/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java +++ b/src/units/solvers/backend/z3smt/UnitsZ3SmtFormatTranslator.java @@ -1,13 +1,25 @@ package units.solvers.backend.z3smt; import backend.z3smt.Z3SmtFormatTranslator; + import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.ConstraintEncoderFactory; import checkers.inference.solver.frontend.Lattice; + import com.microsoft.z3.BoolExpr; import com.microsoft.z3.IntExpr; + +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.Pair; + +import units.representation.TypecheckUnit; +import units.representation.UnitsRepresentationUtils; +import units.solvers.backend.z3smt.encoder.UnitsZ3SmtConstraintEncoderFactory; +import units.solvers.backend.z3smt.encoder.UnitsZ3SmtEncoderUtils; +import units.solvers.backend.z3smt.representation.Z3InferenceUnit; + import java.util.ArrayList; import java.util.Collection; import java.util.HashMap; @@ -15,15 +27,9 @@ import java.util.List; import java.util.Map; import java.util.Set; + import javax.annotation.processing.ProcessingEnvironment; import javax.lang.model.element.AnnotationMirror; -import org.checkerframework.javacutil.AnnotationUtils; -import org.checkerframework.javacutil.Pair; -import units.representation.TypecheckUnit; -import units.representation.UnitsRepresentationUtils; -import units.solvers.backend.z3smt.encoder.UnitsZ3SmtConstraintEncoderFactory; -import units.solvers.backend.z3smt.encoder.UnitsZ3SmtEncoderUtils; -import units.solvers.backend.z3smt.representation.Z3InferenceUnit; public class UnitsZ3SmtFormatTranslator extends Z3SmtFormatTranslator { diff --git a/src/units/solvers/backend/z3smt/UnitsZ3SmtSolverFactory.java b/src/units/solvers/backend/z3smt/UnitsZ3SmtSolverFactory.java index 6da9a60..a750abb 100644 --- a/src/units/solvers/backend/z3smt/UnitsZ3SmtSolverFactory.java +++ b/src/units/solvers/backend/z3smt/UnitsZ3SmtSolverFactory.java @@ -2,7 +2,9 @@ import backend.z3smt.Z3SmtFormatTranslator; import backend.z3smt.Z3SmtSolverFactory; + import checkers.inference.solver.frontend.Lattice; + import units.representation.TypecheckUnit; import units.solvers.backend.z3smt.representation.Z3InferenceUnit; diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtArithmeticConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtArithmeticConstraintEncoder.java index d18e681..45540f0 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtArithmeticConstraintEncoder.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtArithmeticConstraintEncoder.java @@ -2,6 +2,7 @@ import backend.z3smt.Z3SmtFormatTranslator; import backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; + import checkers.inference.model.ArithmeticConstraint.ArithmeticOperationKind; import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.ConstantSlot; @@ -9,9 +10,12 @@ import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; + import org.checkerframework.javacutil.BugInCF; + import units.representation.TypecheckUnit; import units.solvers.backend.z3smt.representation.Z3InferenceUnit; import units.util.UnitsTypecheckUtils; diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java index f4d31c4..7473626 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtCombineConstraintEncoder.java @@ -2,14 +2,18 @@ import backend.z3smt.Z3SmtFormatTranslator; import backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; + import checkers.inference.model.CombVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; + import org.checkerframework.javacutil.AnnotationUtils; + import units.representation.TypecheckUnit; import units.representation.UnitsRepresentationUtils; import units.solvers.backend.z3smt.representation.Z3InferenceUnit; diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtComparableConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtComparableConstraintEncoder.java index 541dcbb..209f6d1 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtComparableConstraintEncoder.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtComparableConstraintEncoder.java @@ -2,13 +2,16 @@ import backend.z3smt.Z3SmtFormatTranslator; import backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; + import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; + import units.representation.TypecheckUnit; import units.solvers.backend.z3smt.representation.Z3InferenceUnit; diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java index 2056456..5c14b0c 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtConstraintEncoderFactory.java @@ -2,7 +2,9 @@ import backend.z3smt.Z3SmtFormatTranslator; import backend.z3smt.encoder.Z3SmtConstraintEncoderFactory; + import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; +import checkers.inference.solver.backend.encoder.ComparisonConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; @@ -11,8 +13,10 @@ import checkers.inference.solver.backend.encoder.implication.ImplicationConstraintEncoder; import checkers.inference.solver.backend.encoder.preference.PreferenceConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; + import units.representation.TypecheckUnit; import units.solvers.backend.z3smt.representation.Z3InferenceUnit; @@ -75,4 +79,9 @@ public ImplicationConstraintEncoder createImplicationConstraintEncoder public ArithmeticConstraintEncoder createArithmeticConstraintEncoder() { return new UnitsZ3SmtArithmeticConstraintEncoder(lattice, ctx, formatTranslator); } + + @Override + public ComparisonConstraintEncoder createComparisonConstraintEncoder() { + return null; + } } diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java index 7465a71..2345504 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEncoderUtils.java @@ -3,7 +3,9 @@ import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; import com.microsoft.z3.IntNum; + import org.checkerframework.javacutil.Pair; + import units.representation.UnitsRepresentationUtils; import units.solvers.backend.z3smt.representation.Z3InferenceUnit; diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEqualityConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEqualityConstraintEncoder.java index 8d1be07..9391fd5 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEqualityConstraintEncoder.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtEqualityConstraintEncoder.java @@ -2,13 +2,16 @@ import backend.z3smt.Z3SmtFormatTranslator; import backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; + import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; + import units.representation.TypecheckUnit; import units.solvers.backend.z3smt.representation.Z3InferenceUnit; diff --git a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtSubtypeConstraintEncoder.java b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtSubtypeConstraintEncoder.java index a4ba018..3c2efa5 100644 --- a/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtSubtypeConstraintEncoder.java +++ b/src/units/solvers/backend/z3smt/encoder/UnitsZ3SmtSubtypeConstraintEncoder.java @@ -2,13 +2,16 @@ import backend.z3smt.Z3SmtFormatTranslator; import backend.z3smt.encoder.Z3SmtAbstractConstraintEncoder; + import checkers.inference.model.ConstantSlot; import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; import checkers.inference.solver.frontend.Lattice; + import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; + import units.representation.TypecheckUnit; import units.solvers.backend.z3smt.representation.Z3InferenceUnit; diff --git a/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java b/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java index c5890d0..b176251 100644 --- a/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java +++ b/src/units/solvers/backend/z3smt/representation/Z3InferenceUnit.java @@ -4,10 +4,12 @@ import com.microsoft.z3.Context; import com.microsoft.z3.IntExpr; import com.microsoft.z3.IntNum; -import java.util.Map; + import units.representation.UnitsRepresentationUtils; import units.solvers.backend.z3smt.encoder.UnitsZ3SmtEncoderUtils; +import java.util.Map; + /** * A data structure class to encapsulate a set of Z3 variables representing a unit for inference. */ diff --git a/src/units/util/UnitsTypecheckUtils.java b/src/units/util/UnitsTypecheckUtils.java index 0b2a102..d622a83 100644 --- a/src/units/util/UnitsTypecheckUtils.java +++ b/src/units/util/UnitsTypecheckUtils.java @@ -1,9 +1,10 @@ package units.util; -import javax.lang.model.element.AnnotationMirror; import units.representation.TypecheckUnit; import units.representation.UnitsRepresentationUtils; +import javax.lang.model.element.AnnotationMirror; + /** Utility class with methods for computing the result unit of various arithmetic operations. */ public class UnitsTypecheckUtils { diff --git a/testing/inference/GenericIterator.java b/testing/inference/GenericIterator.java index 63e7327..872a604 100644 --- a/testing/inference/GenericIterator.java +++ b/testing/inference/GenericIterator.java @@ -1,7 +1,8 @@ /** @skip-test */ -import java.util.Iterator; import units.qual.*; +import java.util.Iterator; + // from ode4j // class MyList implements Iterable { diff --git a/testing/inference/JavaCollections.java b/testing/inference/JavaCollections.java index 2770c8b..0e8678c 100644 --- a/testing/inference/JavaCollections.java +++ b/testing/inference/JavaCollections.java @@ -1,7 +1,8 @@ -import java.util.*; import units.UnitsTools; import units.qual.*; +import java.util.*; + class JavaCollections { void collections() { diff --git a/testing/inference/JavaUtilConcurrentTimeUnit.java b/testing/inference/JavaUtilConcurrentTimeUnit.java index 0bfbc06..c7d486d 100644 --- a/testing/inference/JavaUtilConcurrentTimeUnit.java +++ b/testing/inference/JavaUtilConcurrentTimeUnit.java @@ -1,8 +1,9 @@ import static java.util.concurrent.TimeUnit.*; -import java.util.concurrent.TimeUnit; import units.qual.*; +import java.util.concurrent.TimeUnit; + class JavaUtilConcurrentTimeUnit { void test(long time, TimeUnit unit) throws Exception { diff --git a/testing/inference/JavaUtilDataStructures.java b/testing/inference/JavaUtilDataStructures.java index 7e48954..a97cfaf 100644 --- a/testing/inference/JavaUtilDataStructures.java +++ b/testing/inference/JavaUtilDataStructures.java @@ -1,6 +1,7 @@ -import java.util.*; import units.qual.*; +import java.util.*; + class JavaUtilDataStructures { void rawMapTest() { diff --git a/testing/inference/StaticFinalConstants.java b/testing/inference/StaticFinalConstants.java index dcfa473..50c4aff 100644 --- a/testing/inference/StaticFinalConstants.java +++ b/testing/inference/StaticFinalConstants.java @@ -25,7 +25,8 @@ static class MyConstants { public static final @rad int HASUNIT = 20 * UnitsTools.rad; - public MyConstants() {}; + public MyConstants() {} + ; } void inferRadians2() { diff --git a/testing/inference/TryWithResources.java b/testing/inference/TryWithResources.java index 916fbc2..a81f48d 100644 --- a/testing/inference/TryWithResources.java +++ b/testing/inference/TryWithResources.java @@ -1,7 +1,8 @@ +import units.qual.*; + import java.io.BufferedReader; import java.io.FileReader; import java.io.IOException; -import units.qual.*; // @skip-test // unable to insert inferred annotations for resource variables in try blocks diff --git a/testing/typecheck/JavaUtilConcurrentTimeUnit.java b/testing/typecheck/JavaUtilConcurrentTimeUnit.java index ff62699..fdefd0a 100644 --- a/testing/typecheck/JavaUtilConcurrentTimeUnit.java +++ b/testing/typecheck/JavaUtilConcurrentTimeUnit.java @@ -1,8 +1,9 @@ import static java.util.concurrent.TimeUnit.*; -import java.util.concurrent.TimeUnit; import units.qual.*; +import java.util.concurrent.TimeUnit; + class JavaUtilConcurrentTimeUnit { @SuppressWarnings("units") diff --git a/testing/unsat/WhileLoopIterator.java b/testing/unsat/WhileLoopIterator.java index 05c7393..a60944d 100644 --- a/testing/unsat/WhileLoopIterator.java +++ b/testing/unsat/WhileLoopIterator.java @@ -1,6 +1,7 @@ -import java.util.*; import units.qual.*; +import java.util.*; + class WhileLoopIterator { List list; diff --git a/tests/units/UnitsInferenceTest.java b/tests/units/UnitsInferenceTest.java index dcb6e86..763293d 100644 --- a/tests/units/UnitsInferenceTest.java +++ b/tests/units/UnitsInferenceTest.java @@ -1,14 +1,17 @@ package units; import checkers.inference.test.CFInferenceTest; -import java.io.File; -import java.util.ArrayList; -import java.util.List; + import org.checkerframework.framework.test.TestUtilities; import org.checkerframework.javacutil.Pair; import org.junit.runners.Parameterized.Parameters; + import units.solvers.backend.UnitsSolverEngine; +import java.io.File; +import java.util.ArrayList; +import java.util.List; + public class UnitsInferenceTest extends CFInferenceTest { public UnitsInferenceTest(File testFile) { diff --git a/tests/units/UnitsTypecheckTest.java b/tests/units/UnitsTypecheckTest.java index f3affd8..d4048f6 100644 --- a/tests/units/UnitsTypecheckTest.java +++ b/tests/units/UnitsTypecheckTest.java @@ -1,12 +1,13 @@ package units; -import java.io.File; -import java.util.ArrayList; -import java.util.List; import org.checkerframework.framework.test.CheckerFrameworkPerFileTest; import org.checkerframework.framework.test.TestUtilities; import org.junit.runners.Parameterized.Parameters; +import java.io.File; +import java.util.ArrayList; +import java.util.List; + public class UnitsTypecheckTest extends CheckerFrameworkPerFileTest { public UnitsTypecheckTest(File testFile) { From 85b7224d299d49580d15a53769081ee4df434984 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 10 Jun 2021 12:03:41 -0400 Subject: [PATCH 3/6] update .travis.yml --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 81fe7eb..49abd5d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -5,6 +5,6 @@ jdk: - oraclejdk8 install: - - pip install --user -r ./.travis-requirements.txt + - pip3 install --user -r ./.travis-requirements.txt script: ./.travis-build.sh From 42a372888f2e4d679f2b0f9f5c549c2253460762 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 10 Jun 2021 13:59:16 -0400 Subject: [PATCH 4/6] update .travis.yml --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 49abd5d..4758ec3 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,5 +1,5 @@ language: java -python: 3.8 +python: 3.6 dist: trusty jdk: - oraclejdk8 From 8d38f4a8917d79d51ce74df0e369928f9f671733 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 2 Sep 2021 11:55:54 -0400 Subject: [PATCH 5/6] support eisop update --- gradle/wrapper/gradle-wrapper.properties | 2 +- src/units/UnitsAnnotatedTypeFactory.java | 3 +- src/units/UnitsChecker.java | 3 +- .../UnitsInferenceAnnotatedTypeFactory.java | 128 +----------------- src/units/UnitsVisitor.java | 2 +- 5 files changed, 10 insertions(+), 128 deletions(-) diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index 4e1cc9d..1b16c34 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,5 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-6.1.1-all.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-6.1.1-bin.zip zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists diff --git a/src/units/UnitsAnnotatedTypeFactory.java b/src/units/UnitsAnnotatedTypeFactory.java index 943c1a0..c9dd47b 100644 --- a/src/units/UnitsAnnotatedTypeFactory.java +++ b/src/units/UnitsAnnotatedTypeFactory.java @@ -1,5 +1,6 @@ package units; +import checkers.inference.BaseInferenceRealTypeFactory; import com.sun.source.tree.BinaryTree; import com.sun.source.tree.Tree.Kind; @@ -48,7 +49,7 @@ import javax.lang.model.element.AnnotationMirror; -public class UnitsAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { +public class UnitsAnnotatedTypeFactory extends BaseInferenceRealTypeFactory { // static reference to the singleton instance protected static UnitsRepresentationUtils unitsRepUtils; diff --git a/src/units/UnitsChecker.java b/src/units/UnitsChecker.java index 705528e..a76427c 100644 --- a/src/units/UnitsChecker.java +++ b/src/units/UnitsChecker.java @@ -1,5 +1,6 @@ package units; +import checkers.inference.BaseInferenceRealTypeFactory; import checkers.inference.BaseInferrableChecker; import checkers.inference.InferenceChecker; import checkers.inference.InferrableChecker; @@ -52,7 +53,7 @@ public UnitsVisitor createVisitor( } @Override - public UnitsAnnotatedTypeFactory createRealTypeFactory() { + public BaseInferenceRealTypeFactory createRealTypeFactory(boolean infer) { return new UnitsAnnotatedTypeFactory(this); } diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index 0ca58ee..2d4e900 100644 --- a/src/units/UnitsInferenceAnnotatedTypeFactory.java +++ b/src/units/UnitsInferenceAnnotatedTypeFactory.java @@ -133,126 +133,6 @@ public AnnotationMirror canonicalAnnotation(AnnotationMirror anno) { return result; } - @Override - public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) { - return new UnitsInferenceQualifierHierarchy(factory); - } - - private final class UnitsInferenceQualifierHierarchy extends InferenceQualifierHierarchy { - public UnitsInferenceQualifierHierarchy(MultiGraphFactory multiGraphFactory) { - super(multiGraphFactory); - } - - // In inference mode, the only bottom is VarAnnot - @Override - protected Set findBottoms( - Map> supertypes) { - Set newBottoms = super.findBottoms(supertypes); - newBottoms.remove(unitsRepUtils.RAWUNITSREP); - return newBottoms; - } - - // In inference mode, the only qualifier is VarAnnot. The poly qualifiers are - // PolyAll and any poly qual from the type system. - @Override - protected void finish( - QualifierHierarchy qualHierarchy, - Map> supertypesMap, - Map polyQualifiers, - Set tops, - Set bottoms, - Object... args) { - super.finish(qualHierarchy, supertypesMap, polyQualifiers, tops, bottoms, args); - - // TODO: this update, which is sensible to keep the inference qual hierarchy clean, - // causes crashes in creating constant slots for @PolyUnit - // disabling for now - - /* - * Map before update: - supertypesMap - @checkers.inference.qual.VarAnnot -> [@org.checkerframework.framework.qual.PolyAll] - @org.checkerframework.framework.qual.PolyAll -> [@checkers.inference.qual.VarAnnot, @units.qual.UnitsRep] - @units.qual.PolyUnit -> [@org.checkerframework.framework.qual.PolyAll, @units.qual.UnitsRep] - @units.qual.UnitsRep -> [] - polyQualifiers {null=@org.checkerframework.framework.qual.PolyAll, @units.qual.UnitsRep=@units.qual.PolyUnit} - tops [@checkers.inference.qual.VarAnnot] - bottoms [@checkers.inference.qual.VarAnnot] - */ - // - // // Remove @UnitsRep from super of PolyAll - // assert supertypesMap.containsKey(unitsRepUtils.POLYALL); - // Set polyAllSupers = AnnotationUtils.createAnnotationSet(); - // polyAllSupers.addAll(supertypesMap.get(unitsRepUtils.POLYALL)); - // polyAllSupers.remove(unitsRepUtils.RAWUNITSINTERNAL); - // supertypesMap.put(unitsRepUtils.POLYALL, - // Collections.unmodifiableSet(polyAllSupers)); - // - // // Remove @UnitsRep from super of PolyUnit - // assert supertypesMap.containsKey(unitsRepUtils.POLYUNIT); - // Set polyUnitSupers = AnnotationUtils.createAnnotationSet(); - // polyUnitSupers.addAll(supertypesMap.get(unitsRepUtils.POLYUNIT)); - // polyUnitSupers.remove(unitsRepUtils.RAWUNITSINTERNAL); - // supertypesMap.put(unitsRepUtils.POLYUNIT, - // Collections.unmodifiableSet(polyUnitSupers)); - // - // // Remove @UnitsRep from map - // supertypesMap.remove(unitsRepUtils.RAWUNITSINTERNAL); - // - // // Remove @UnitsRep from polyQualifiers - // assert polyQualifiers.containsKey(unitsRepUtils.RAWUNITSINTERNAL); - // polyQualifiers.remove(unitsRepUtils.RAWUNITSINTERNAL); - // - // System.err.println(" === Inference ATF "); - // System.err.println(" supertypesMap "); - // for (Entry e : supertypesMap.entrySet()) { - // System.err.println(" " + e.getKey() + " -> " + e.getValue()); - // } - // System.err.println(" polyQualifiers " + polyQualifiers); - // System.err.println(" tops " + tops); - // System.err.println(" bottoms " + bottoms); - - /* - * Map after update: - supertypesMap - @checkers.inference.qual.VarAnnot -> [@org.checkerframework.framework.qual.PolyAll] - @org.checkerframework.framework.qual.PolyAll -> [@checkers.inference.qual.VarAnnot] - @units.qual.PolyUnit -> [@org.checkerframework.framework.qual.PolyAll] - polyQualifiers {null=@org.checkerframework.framework.qual.PolyAll} - tops [@checkers.inference.qual.VarAnnot] - bottoms [@checkers.inference.qual.VarAnnot] - */ - } - - @Override - public Set leastUpperBounds( - Collection annos1, - Collection annos2) { - if (InferenceMain.isHackMode(annos1.size() != annos2.size())) { - Set result = AnnotationUtils.createAnnotationSet(); - for (AnnotationMirror a1 : annos1) { - for (AnnotationMirror a2 : annos2) { - AnnotationMirror lub = leastUpperBound(a1, a2); - if (lub != null) { - result.add(lub); - } - } - } - - return result; - } - - return super.leastUpperBounds(annos1, annos2); - } - } - - @Override - protected Set getDefaultTypeDeclarationBounds() { - Set top = new HashSet<>(); - top.add(unitsRepUtils.TOP); - return top; - } - @Override protected InferenceViewpointAdapter createViewpointAdapter() { return new UnitsInferenceViewpointAdapter(this); @@ -322,13 +202,13 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { result = slotManager.createConstantSlot(unitsRepUtils.DIMENSIONLESS); break; default: - result = slotManager.createLubVariableSlot(lhs, rhs); + result = slotManager.createLubMergeVariableSlot(lhs, rhs); break; } // insert varAnnot of the slot into the ATM AnnotationMirror resultAM = slotManager.getAnnotation(result); - atm.clearAnnotations(); + atm.clearPrimaryAnnotations(); atm.replaceAnnotation(resultAM); // add to cache @@ -440,7 +320,7 @@ private boolean isPolyAnnotation(AnnotationMirror annot) { Slot slot = slotManager.getSlot(annot); if (slot instanceof ConstantSlot) { AnnotationMirror constant = ((ConstantSlot) slot).getValue(); - return InferenceQualifierHierarchy.isPolymorphic(constant); + return getQualifierHierarchy().isPolymorphicQualifier(constant); } return false; } @@ -598,7 +478,7 @@ private void replaceATM(AnnotatedTypeMirror atm, AnnotationMirror am) { AnnotationBuilder ab = new AnnotationBuilder(realTypeFactory.getProcessingEnv(), VarAnnot.class); ab.setValue("value", cs.getId()); - atm.clearAnnotations(); + atm.clearPrimaryAnnotations(); atm.replaceAnnotation(ab.build()); } } diff --git a/src/units/UnitsVisitor.java b/src/units/UnitsVisitor.java index 2439ff1..d2ee833 100644 --- a/src/units/UnitsVisitor.java +++ b/src/units/UnitsVisitor.java @@ -272,7 +272,7 @@ public Void visitTypeCast(TypeCastTree node, Void p) { exprType, UnitsRepresentationUtils.getInstance().DIMENSIONLESS)) { if (atypeFactory.getDependentTypesHelper() != null) { AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node); - atypeFactory.getDependentTypesHelper().checkType(type, node.getType()); + atypeFactory.getDependentTypesHelper().checkTypeForErrorExpressions(type, node.getType()); } // perform scan and reduce as per super.super.visitTypeCast() From 6ba70ffc10bc8796cb491eff59a109db3df47185 Mon Sep 17 00:00:00 2001 From: d367wang Date: Thu, 2 Sep 2021 12:11:43 -0400 Subject: [PATCH 6/6] fix compile error --- src/units/UnitsAnnotatedTypeFactory.java | 13 +++++++++++-- src/units/UnitsInferenceAnnotatedTypeFactory.java | 7 ------- src/units/UnitsVisitor.java | 8 ++++---- 3 files changed, 15 insertions(+), 13 deletions(-) diff --git a/src/units/UnitsAnnotatedTypeFactory.java b/src/units/UnitsAnnotatedTypeFactory.java index c9dd47b..94cc852 100644 --- a/src/units/UnitsAnnotatedTypeFactory.java +++ b/src/units/UnitsAnnotatedTypeFactory.java @@ -1,10 +1,10 @@ package units; import checkers.inference.BaseInferenceRealTypeFactory; + import com.sun.source.tree.BinaryTree; import com.sun.source.tree.Tree.Kind; -import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.qual.LiteralKind; import org.checkerframework.framework.qual.TypeUseLocation; @@ -24,6 +24,7 @@ import org.checkerframework.framework.type.typeannotator.TypeAnnotator; import org.checkerframework.framework.util.AnnotationFormatter; import org.checkerframework.framework.util.GraphQualifierHierarchy; +import org.checkerframework.framework.util.MultiGraphQualifierHierarchy; import org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory; import org.checkerframework.framework.util.defaults.QualifierDefaults; import org.checkerframework.javacutil.AnnotationUtils; @@ -161,8 +162,16 @@ protected void addCheckedCodeDefaults(QualifierDefaults defs) { defs.addCheckedCodeDefault(unitsRepUtils.TOP, TypeUseLocation.LOCAL_VARIABLE); } + @SuppressWarnings("deprecation") + @Override + public QualifierHierarchy createQualifierHierarchy() { + return MultiGraphQualifierHierarchy.createMultiGraphQualifierHierarchy(this); + } + + @SuppressWarnings("deprecation") @Override - public QualifierHierarchy createQualifierHierarchy(MultiGraphFactory factory) { + public QualifierHierarchy createQualifierHierarchyWithMultiGraphFactory( + MultiGraphFactory factory) { return new UnitsQualifierHierarchy(factory); } diff --git a/src/units/UnitsInferenceAnnotatedTypeFactory.java b/src/units/UnitsInferenceAnnotatedTypeFactory.java index 2d4e900..0bd9e09 100644 --- a/src/units/UnitsInferenceAnnotatedTypeFactory.java +++ b/src/units/UnitsInferenceAnnotatedTypeFactory.java @@ -2,8 +2,6 @@ import checkers.inference.InferenceAnnotatedTypeFactory; import checkers.inference.InferenceChecker; -import checkers.inference.InferenceMain; -import checkers.inference.InferenceQualifierHierarchy; import checkers.inference.InferenceTreeAnnotator; import checkers.inference.InferrableChecker; import checkers.inference.SlotManager; @@ -33,12 +31,10 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType; import org.checkerframework.framework.type.AnnotationClassLoader; import org.checkerframework.framework.type.DefaultAnnotatedTypeFormatter; -import org.checkerframework.framework.type.QualifierHierarchy; import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; import org.checkerframework.framework.type.treeannotator.TreeAnnotator; import org.checkerframework.framework.util.AnnotatedTypes; import org.checkerframework.framework.util.AnnotationFormatter; -import org.checkerframework.framework.util.MultiGraphQualifierHierarchy.MultiGraphFactory; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; @@ -48,9 +44,6 @@ import units.representation.UnitsRepresentationUtils; -import java.util.Collection; -import java.util.HashSet; -import java.util.Map; import java.util.Set; import javax.lang.model.element.AnnotationMirror; diff --git a/src/units/UnitsVisitor.java b/src/units/UnitsVisitor.java index d2ee833..6253525 100644 --- a/src/units/UnitsVisitor.java +++ b/src/units/UnitsVisitor.java @@ -11,7 +11,6 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.ConstraintManager; import checkers.inference.model.Slot; -import checkers.inference.model.VariableSlot; import com.sun.source.tree.BinaryTree; import com.sun.source.tree.Tree.Kind; @@ -178,8 +177,7 @@ public Void visitBinary(BinaryTree binaryTree, Void p) { break; default: // TODO: replace with LUBSlot pending mier's PR - VariableSlot lubSlot = - slotManager.getVariableSlot(atypeFactory.getAnnotatedType(binaryTree)); + Slot lubSlot = slotManager.getSlot(atypeFactory.getAnnotatedType(binaryTree)); // Create LUB constraint by default constraintManager.addSubtypeConstraint(lhs, lubSlot); constraintManager.addSubtypeConstraint(rhs, lubSlot); @@ -272,7 +270,9 @@ public Void visitTypeCast(TypeCastTree node, Void p) { exprType, UnitsRepresentationUtils.getInstance().DIMENSIONLESS)) { if (atypeFactory.getDependentTypesHelper() != null) { AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(node); - atypeFactory.getDependentTypesHelper().checkTypeForErrorExpressions(type, node.getType()); + atypeFactory + .getDependentTypesHelper() + .checkTypeForErrorExpressions(type, node.getType()); } // perform scan and reduce as per super.super.visitTypeCast()