From ea8d0a5028364f3b6fd58198ed0da9fb99f8da13 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Fri, 1 Nov 2019 11:59:51 -0400 Subject: [PATCH 01/10] added underlying type to Variable Slot --- .../inference/DefaultSlotManager.java | 7 ++-- .../inference/ImpliedTypeAnnotator.java | 4 +-- src/checkers/inference/SlotManager.java | 3 +- src/checkers/inference/VariableAnnotator.java | 21 +++++++----- .../inference/model/VariableSlot.java | 33 +++++++++++++++++++ 5 files changed, 54 insertions(+), 14 deletions(-) diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index ad01eef4c..03220e63e 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -17,6 +17,7 @@ import javax.annotation.processing.ProcessingEnvironment; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.AnnotationValue; +import javax.lang.model.type.TypeMirror; import checkers.inference.model.LubVariableSlot; @@ -300,17 +301,17 @@ public int getNumberOfSlots() { } @Override - public VariableSlot createVariableSlot(AnnotationLocation location) { + public VariableSlot createVariableSlot(AnnotationLocation location, TypeMirror type) { VariableSlot variableSlot; if (location.getKind() == AnnotationLocation.Kind.MISSING) { //Don't cache slot for MISSING LOCATION. Just create a new one and return. - variableSlot = new VariableSlot(location, nextId()); + variableSlot = new VariableSlot(location, nextId(), type); addToVariables(variableSlot); } else if (locationCache.containsKey(location)) { int id = locationCache.get(location); variableSlot = getVariable(id); } else { - variableSlot = new VariableSlot(location, nextId()); + variableSlot = new VariableSlot(location, nextId(), type); addToVariables(variableSlot); locationCache.put(location, variableSlot.getId()); } diff --git a/src/checkers/inference/ImpliedTypeAnnotator.java b/src/checkers/inference/ImpliedTypeAnnotator.java index 55913aeaa..ca20cd8eb 100644 --- a/src/checkers/inference/ImpliedTypeAnnotator.java +++ b/src/checkers/inference/ImpliedTypeAnnotator.java @@ -78,7 +78,7 @@ protected void insertExistentialVariable(AnnotatedTypeVariable typeVariableUse, typeFactory.getAnnotatedType(typeVariableUse.getUnderlyingType().asElement()); AnnotationLocation location = getLocation(typeVariableUse, astRecords); - VariableSlot potentialVar = slotManager.createVariableSlot(location); + VariableSlot potentialVar = slotManager.createVariableSlot(location, typeVariableUse.getUnderlyingType()); existentialVariableInserter.insert(potentialVar, typeVariableUse, declaration); } @@ -120,7 +120,7 @@ protected Void scan(AnnotatedTypeMirror type, Map astRecords) { AnnotationLocation location = getLocation(type, astRecords); - VariableSlot slot = slotManager.createVariableSlot(location); + VariableSlot slot = slotManager.createVariableSlot(location, type.getUnderlyingType()); type.addAnnotation(slotManager.getAnnotation(slot)); } diff --git a/src/checkers/inference/SlotManager.java b/src/checkers/inference/SlotManager.java index 8a10e81ab..5f07d1bfc 100644 --- a/src/checkers/inference/SlotManager.java +++ b/src/checkers/inference/SlotManager.java @@ -6,6 +6,7 @@ import java.util.List; import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.type.TypeMirror; import checkers.inference.model.AnnotationLocation; import checkers.inference.model.ArithmeticVariableSlot; @@ -40,7 +41,7 @@ public interface SlotManager { * used to locate this variable in code * @return VariableSlot that corresponds to this location */ - VariableSlot createVariableSlot(AnnotationLocation location); + VariableSlot createVariableSlot(AnnotationLocation location, TypeMirror type); /** * Create new RefinementVariableSlot and return the reference to it if no diff --git a/src/checkers/inference/VariableAnnotator.java b/src/checkers/inference/VariableAnnotator.java index 693086513..0b9625243 100644 --- a/src/checkers/inference/VariableAnnotator.java +++ b/src/checkers/inference/VariableAnnotator.java @@ -37,6 +37,7 @@ import javax.lang.model.element.TypeElement; import javax.lang.model.element.TypeParameterElement; import javax.lang.model.type.TypeKind; +import javax.lang.model.type.TypeMirror; import com.sun.source.tree.AnnotatedTypeTree; import com.sun.source.tree.ArrayTypeTree; @@ -195,6 +196,10 @@ protected AnnotationLocation treeToLocation(Tree tree) { return treeToLocation(inferenceTypeFactory, tree); } + protected TypeMirror treeToType(Tree tree) { + return InferenceMain.getInstance().getRealTypeFactory().getAnnotatedType(tree).getUnderlyingType(); + } + /** * For each method call that uses a method with a polymorphic qualifier, we replace all uses of that polymorphic * qualifier with a Variable. Sometimes we might have to later retrieve that qualifier for a given invocation @@ -205,7 +210,7 @@ protected AnnotationLocation treeToLocation(Tree tree) { public VariableSlot getOrCreatePolyVar(Tree tree) { VariableSlot polyVar = treeToPolyVar.get(tree); if (polyVar == null) { - polyVar = slotManager.createVariableSlot(treeToLocation(tree)); + polyVar = slotManager.createVariableSlot(treeToLocation(tree), treeToType(tree)); treeToPolyVar.put(tree, polyVar); } @@ -224,7 +229,7 @@ public VariableSlot getOrCreatePolyVar(Tree tree) { * @return A new VariableSlot corresponding to tree */ private VariableSlot createVariable(final Tree tree) { - final VariableSlot varSlot = createVariable(treeToLocation(tree)); + final VariableSlot varSlot = createVariable(treeToLocation(tree), treeToType(tree)); // if (path != null) { // Element element = inferenceTypeFactory.getTreeUtils().getElement(path); @@ -251,9 +256,9 @@ private VariableSlot createVariable(final Tree tree) { * actual implied tree appended to it. * @return A new VariableSlot corresponding to tree */ - private VariableSlot createVariable(final AnnotationLocation location) { + private VariableSlot createVariable(final AnnotationLocation location, TypeMirror type) { final VariableSlot variableSlot = slotManager - .createVariableSlot(location); + .createVariableSlot(location, type); return variableSlot; } @@ -528,7 +533,7 @@ private VariableSlot addPrimaryVariable(AnnotatedTypeMirror atm, final Tree tree * the type. */ public VariableSlot addImpliedPrimaryVariable(AnnotatedTypeMirror atm, final AnnotationLocation location) { - VariableSlot variable = slotManager.createVariableSlot(location); + VariableSlot variable = slotManager.createVariableSlot(location, atm.getUnderlyingType()); atm.addAnnotation(slotManager.getAnnotation(variable)); AnnotationMirror realAnno = atm.getAnnotationInHierarchy(realTop); @@ -564,7 +569,7 @@ private VariableSlot replaceOrCreateEquivalentVarAnno(AnnotatedTypeMirror atm, T realQualifier = realTypeFactory.getAnnotatedType(tree).getAnnotationInHierarchy(realTop); varSlot = slotManager.createConstantSlot(realQualifier); } else { - varSlot = createVariable(location); + varSlot = createVariable(location, atm.getUnderlyingType()); } atm.replaceAnnotation(slotManager.getAnnotation(varSlot)); @@ -757,7 +762,7 @@ private void handleClassDeclaration(AnnotatedDeclaredType classType, ClassTree c if (!extendsMissingTrees.containsKey(classElement)) { // TODO: SEE COMMENT ON createImpliedExtendsLocation AnnotationLocation location = createImpliedExtendsLocation(classTree); - extendsSlot = createVariable(location); + extendsSlot = createVariable(location, classType.getUnderlyingType()); extendsMissingTrees.put(classElement, extendsSlot); logger.fine("Created variable for implicit extends on class:\n" + extendsSlot.getId() + " => " + classElement + " (extends Object)"); @@ -1211,7 +1216,7 @@ public Void visitTypeVariable(AnnotatedTypeVariable typeVar, Tree tree) { final VariableSlot extendsSlot; if (!extendsMissingTrees.containsKey(typeVarElement)) { AnnotationLocation location = createImpliedExtendsLocation(typeParameterTree); - extendsSlot = createVariable(location); + extendsSlot = createVariable(location, typeVar.getUnderlyingType()); extendsMissingTrees.put(typeVarElement, extendsSlot); logger.fine("Created variable for implicit extends on type parameter:\n" + extendsSlot.getId() + " => " + typeVarElement + " (extends Object)"); diff --git a/src/checkers/inference/model/VariableSlot.java b/src/checkers/inference/model/VariableSlot.java index 1285c1ba8..06e1033f7 100644 --- a/src/checkers/inference/model/VariableSlot.java +++ b/src/checkers/inference/model/VariableSlot.java @@ -4,6 +4,8 @@ import java.util.HashSet; import java.util.Set; +import javax.lang.model.type.TypeMirror; + /** * VariableSlot is a Slot representing an undetermined value (i.e. a variable we are solving for). * After the Solver is run, each VariableSlot should have an assigned value which is then written @@ -36,6 +38,9 @@ public class VariableSlot extends Slot implements Comparable{ */ private boolean insertable = true; + /** Actual type wrapped with this TypeMirror. */ + protected final TypeMirror actualType; + /** * @param location Used to locate this variable in code, see @AnnotationLocation * @param id Unique identifier for this variable @@ -43,8 +48,21 @@ public class VariableSlot extends Slot implements Comparable{ public VariableSlot(AnnotationLocation location, int id) { super(location); this.id = id; + this.actualType = null; + } + + /** + * @param location Used to locate this variable in code, see @AnnotationLocation + * @param id Unique identifier for this variable + * @param type the underlying type + */ + public VariableSlot(AnnotationLocation location, int id, TypeMirror type) { + super(location); + this.id = id; + this.actualType = type; } + // Slots this variable has been merged to. private final Set mergedToSlots = new HashSet<>(); @@ -74,12 +92,27 @@ public boolean isMergedTo(VariableSlot other) { return false; } + /** + * Returns the underlying unannotated Java type, which this wraps. + * + * @return the underlying type + */ + public TypeMirror getUnderlyingType() { + return actualType; + } + public int getId() { return id; } public VariableSlot(int id) { this.id = id; + this.actualType = null; + } + + public VariableSlot(int id, TypeMirror type) { + this.id = id; + this.actualType = type; } public Set getMergedToSlots() { From c1f65d15ad1e3a64037d01bb0c68064aed112d07 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Fri, 8 Nov 2019 19:04:54 -0500 Subject: [PATCH 02/10] Slot refactor. Make all slots that extends varaibleslot to extends slots instead --- .../inference/DefaultSlotManager.java | 14 +-- .../ExistentialVariableInserter.java | 8 +- .../InferenceQualifierPolymorphism.java | 3 +- .../InferenceTypeVariableSubstitutor.java | 2 +- src/checkers/inference/SlotManager.java | 4 +- src/checkers/inference/VariableAnnotator.java | 51 ++++---- .../inference/VariableSlotReplacer.java | 21 ++-- .../inference/dataflow/InferenceValue.java | 4 +- .../model/ArithmeticVariableSlot.java | 4 +- .../inference/model/CombVariableSlot.java | 4 +- .../inference/model/ConstantSlot.java | 4 +- .../model/ExistentialVariableSlot.java | 12 +- .../inference/model/LubVariableSlot.java | 4 +- .../model/RefinementVariableSlot.java | 4 +- src/checkers/inference/model/Serializer.java | 3 +- src/checkers/inference/model/Slot.java | 116 +++++++++++++++-- .../inference/model/VariableSlot.java | 117 +++--------------- .../serialization/CnfVecIntSerializer.java | 6 + .../model/serialization/JsonSerializer.java | 13 +- .../serialization/ToStringSerializer.java | 14 ++- .../backend/AbstractFormatTranslator.java | 6 + .../z3/Z3BitVectorFormatTranslator.java | 3 +- .../inference/solver/util/PrintUtils.java | 15 ++- .../InferenceTypeArgumentInference.java | 16 +-- 24 files changed, 252 insertions(+), 196 deletions(-) diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index 03220e63e..12a12e1f0 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -54,7 +54,7 @@ public class DefaultSlotManager implements SlotManager { * ConstantSlots are also stored in this map, since ConstantSlot is subclass * of VariableSlot. */ - private final Map variables; + private final Map variables; /** * A map of {@link AnnotationMirror} to {@link Integer} for caching @@ -77,7 +77,7 @@ public class DefaultSlotManager implements SlotManager { * uniquely identified by its potential and alternative VariablesSlots. * {@link Integer} is the id of the corresponding ExistentialVariableSlot */ - private final Map, Integer> existentialSlotPairCache; + private final Map, Integer> existentialSlotPairCache; /** * A map of {@link Pair} of {@link Slot} to {@link Integer} for caching @@ -157,7 +157,7 @@ private int nextId() { return nextId++; } - private void addToVariables(final VariableSlot slot) { + private void addToVariables(final Slot slot) { variables.put(slot.getId(), slot); } @@ -165,7 +165,7 @@ private void addToVariables(final VariableSlot slot) { * @inheritDoc */ @Override - public VariableSlot getVariable( int id ) { + public Slot getVariable( int id ) { return variables.get(id); } @@ -309,7 +309,7 @@ public VariableSlot createVariableSlot(AnnotationLocation location, TypeMirror t addToVariables(variableSlot); } else if (locationCache.containsKey(location)) { int id = locationCache.get(location); - variableSlot = getVariable(id); + variableSlot = (VariableSlot) getVariable(id); } else { variableSlot = new VariableSlot(location, nextId(), type); addToVariables(variableSlot); @@ -383,9 +383,9 @@ public LubVariableSlot createLubVariableSlot(Slot left, Slot right) { } @Override - public ExistentialVariableSlot createExistentialVariableSlot(VariableSlot potentialSlot, VariableSlot alternativeSlot) { + public ExistentialVariableSlot createExistentialVariableSlot(Slot potentialSlot, Slot alternativeSlot) { ExistentialVariableSlot existentialVariableSlot; - Pair pair = new Pair<>(potentialSlot, alternativeSlot); + Pair pair = new Pair<>(potentialSlot, alternativeSlot); if (existentialSlotPairCache.containsKey(pair)) { int id = existentialSlotPairCache.get(pair); existentialVariableSlot = (ExistentialVariableSlot) getVariable(id); diff --git a/src/checkers/inference/ExistentialVariableInserter.java b/src/checkers/inference/ExistentialVariableInserter.java index fa9f6e731..992da9b62 100644 --- a/src/checkers/inference/ExistentialVariableInserter.java +++ b/src/checkers/inference/ExistentialVariableInserter.java @@ -94,7 +94,7 @@ public ExistentialVariableInserter(final SlotManager slotManager, final Constrai /** * See class comments for information on insert */ - public void insert(final VariableSlot potentialVariable, final AnnotatedTypeMirror typeUse, + public void insert(final Slot potentialVariable, final AnnotatedTypeMirror typeUse, final AnnotatedTypeMirror declaration) { insert(potentialVariable, typeUse, declaration, false); } @@ -102,7 +102,7 @@ public void insert(final VariableSlot potentialVariable, final AnnotatedTypeMirr /** * See class comments for information on insert */ - public void insert(final VariableSlot potentialVariable, final AnnotatedTypeMirror typeUse, + public void insert(final Slot potentialVariable, final AnnotatedTypeMirror typeUse, final AnnotatedTypeMirror declaration, boolean mustExist) { if (potentialVariable == null || !(potentialVariable instanceof VariableSlot)) { throw new BugInCF("Bad type variable slot: slot=" + potentialVariable); @@ -121,10 +121,10 @@ public void insert(final VariableSlot potentialVariable, final AnnotatedTypeMirr } private class InsertionVisitor extends EquivalentAtmComboScanner { - private VariableSlot potentialVariable; + private Slot potentialVariable; private AnnotationMirror potentialVarAnno; - public InsertionVisitor(final VariableSlot potentialVariable, + public InsertionVisitor(final Slot potentialVariable, final AnnotationMirror potentialVarAnno, final boolean mustExist) { this.potentialVariable = potentialVariable; diff --git a/src/checkers/inference/InferenceQualifierPolymorphism.java b/src/checkers/inference/InferenceQualifierPolymorphism.java index 86144688b..cbd666363 100644 --- a/src/checkers/inference/InferenceQualifierPolymorphism.java +++ b/src/checkers/inference/InferenceQualifierPolymorphism.java @@ -9,6 +9,7 @@ import com.sun.source.tree.Tree; import checkers.inference.model.ConstantSlot; +import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; /** @@ -71,7 +72,7 @@ public Void scan(AnnotatedTypeMirror type, Void v) { if (type != null) { AnnotationMirror varSlot = type.getAnnotationInHierarchy(varAnnot); if (varSlot != null) { - VariableSlot var = (VariableSlot) slotManager.getSlot(varSlot); + Slot var = slotManager.getSlot(varSlot); if (InferenceMain.isHackMode(var == null)) { } else if (var.isConstant()) { AnnotationMirror constant = ((ConstantSlot)var).getValue(); diff --git a/src/checkers/inference/InferenceTypeVariableSubstitutor.java b/src/checkers/inference/InferenceTypeVariableSubstitutor.java index 1ee42967d..c59762880 100644 --- a/src/checkers/inference/InferenceTypeVariableSubstitutor.java +++ b/src/checkers/inference/InferenceTypeVariableSubstitutor.java @@ -66,7 +66,7 @@ protected AnnotatedTypeMirror substituteTypeVariable(AnnotatedTypeMirror argumen // we remove it (because it's between the potential variable and the bounds) and replace it // with one that is between the SAME potential variable but the argumenht instead - final VariableSlot potentialSlot = ((ExistentialVariableSlot) upperBoundSlot).getPotentialSlot(); + final Slot potentialSlot = ((ExistentialVariableSlot) upperBoundSlot).getPotentialSlot(); if (argument.getKind() != TypeKind.TYPEVAR) { final Slot altSlot = slotManager.getVariableSlot(argument); diff --git a/src/checkers/inference/SlotManager.java b/src/checkers/inference/SlotManager.java index 5f07d1bfc..e4073f576 100644 --- a/src/checkers/inference/SlotManager.java +++ b/src/checkers/inference/SlotManager.java @@ -118,7 +118,7 @@ public interface SlotManager { * @return the ExistentialVariableSlot that wraps this potentialSlot and * alternativeSlot */ - ExistentialVariableSlot createExistentialVariableSlot(VariableSlot potentialSlot, VariableSlot alternativeSlot); + ExistentialVariableSlot createExistentialVariableSlot(Slot potentialSlot, Slot alternativeSlot); /** * Create new ArithmeticVariableSlot at the given location and return a reference to it if no @@ -152,7 +152,7 @@ public interface SlotManager { AnnotationMirror createEquivalentVarAnno(final AnnotationMirror realQualifier); /** Return the variable identified by the given id or null if no such variable has been added */ - VariableSlot getVariable( int id ); + Slot getVariable( int id ); /** * Given a slot return an annotation that represents the slot when added to an AnnotatedTypeMirror. diff --git a/src/checkers/inference/VariableAnnotator.java b/src/checkers/inference/VariableAnnotator.java index 0b9625243..c14c6c80f 100644 --- a/src/checkers/inference/VariableAnnotator.java +++ b/src/checkers/inference/VariableAnnotator.java @@ -70,6 +70,7 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.ConstraintManager; import checkers.inference.model.ExistentialVariableSlot; +import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.model.tree.ArtificialExtendsBoundTree; import checkers.inference.qual.VarAnnot; @@ -104,7 +105,7 @@ public class VariableAnnotator extends AnnotatedTypeScanner { * annotation mirror for a tree is calculated (i.e least upper bound for * binary tree), and the calculated result is cached in the set. **/ - protected final Map>> treeToVarAnnoPair; + protected final Map>> treeToVarAnnoPair; /** Store elements that have already been annotated **/ private final Map elementToAtm; @@ -238,8 +239,8 @@ private VariableSlot createVariable(final Tree tree) { // } // } - final Pair> varATMPair = Pair - .> of(varSlot, + final Pair> varATMPair = Pair + .> of(varSlot, AnnotationUtils.createAnnotationSet()); treeToVarAnnoPair.put(tree, varATMPair); logger.fine("Created variable for tree:\n" + varSlot.getId() + " => " + tree); @@ -273,8 +274,8 @@ public ConstantSlot createConstant(final AnnotationMirror value, final Tree tree // } Set annotations = AnnotationUtils.createAnnotationSet(); annotations.add(constantSlot.getValue()); - final Pair> varATMPair = Pair - .> of((VariableSlot) constantSlot, + final Pair> varATMPair = Pair + .> of(constantSlot, annotations); treeToVarAnnoPair.put(tree, varATMPair); logger.fine("Created variable for tree:\n" + constantSlot.getId() + " => " + tree); @@ -293,7 +294,7 @@ public ConstantSlot createConstant(final AnnotationMirror value, final Tree tree * This method then applies the existential variable as a primary annotation on atm */ ExistentialVariableSlot getOrCreateExistentialVariable(final AnnotatedTypeMirror atm, - final VariableSlot potentialVariable, + final Slot potentialVariable, final VariableSlot alternativeSlot) { ExistentialVariableSlot existentialVariable = getOrCreateExistentialVariable(potentialVariable, alternativeSlot); atm.replaceAnnotation(slotManager.getAnnotation(existentialVariable)); @@ -309,8 +310,8 @@ ExistentialVariableSlot getOrCreateExistentialVariable(final AnnotatedTypeMirror * potentialVariable and alternative and stores it. * Otherwise, it returns the previously stored ExistentialVariableSlot */ - ExistentialVariableSlot getOrCreateExistentialVariable(final VariableSlot potentialVariable, - final VariableSlot alternativeSlot) { + ExistentialVariableSlot getOrCreateExistentialVariable(final Slot potentialVariable, + final Slot alternativeSlot) { final Pair idPair = Pair.of(potentialVariable.getId(), alternativeSlot.getId()); ExistentialVariableSlot existentialVariable = idsToExistentialSlots.get(idPair); @@ -363,7 +364,7 @@ private void addExistentialVariable(final AnnotatedTypeVariable typeVar, final T // } // } - final VariableSlot potentialVariable; + final Slot potentialVariable; final Element varElem; final Tree typeTree; @@ -435,8 +436,8 @@ private void addExistentialVariable(final AnnotatedTypeVariable typeVar, final T } potentialVariable = createVariable(typeTree); - final Pair> varATMPair = Pair - .> of( + final Pair> varATMPair = Pair + .> of( potentialVariable, typeVar.getAnnotations()); treeToVarAnnoPair.put(typeTree, varATMPair); @@ -494,9 +495,9 @@ private boolean isInUpperBound(TreePath path) { * after this method completes * @param tree Tree for which we want to create variables */ - private VariableSlot addPrimaryVariable(AnnotatedTypeMirror atm, final Tree tree) { + private Slot addPrimaryVariable(AnnotatedTypeMirror atm, final Tree tree) { - final VariableSlot variable; + final Slot variable; if (treeToVarAnnoPair.containsKey(tree)) { variable = treeToVarAnnoPair.get(tree).first; @@ -508,7 +509,7 @@ private VariableSlot addPrimaryVariable(AnnotatedTypeMirror atm, final Tree tree } else { AnnotationLocation location = treeToLocation(tree); variable = replaceOrCreateEquivalentVarAnno(atm, tree, location); - final Pair> varATMPair = Pair + final Pair> varATMPair = Pair .of(variable, AnnotationUtils.createAnnotationSet()); @@ -550,8 +551,8 @@ public VariableSlot addImpliedPrimaryVariable(AnnotatedTypeMirror atm, final Ann * Given an atm, replace its real annotation from pre-annotated code and implicit from the underlying type system * by the equivalent varAnnotation, or creating a new VarAnnotation for it if doesn't have any existing annotations. */ - private VariableSlot replaceOrCreateEquivalentVarAnno(AnnotatedTypeMirror atm, Tree tree, final AnnotationLocation location) { - VariableSlot varSlot = null; + private Slot replaceOrCreateEquivalentVarAnno(AnnotatedTypeMirror atm, Tree tree, final AnnotationLocation location) { + Slot varSlot = null; AnnotationMirror realQualifier = null; AnnotationMirror existinVar = atm.getAnnotationInHierarchy(varAnnot); @@ -576,7 +577,7 @@ private VariableSlot replaceOrCreateEquivalentVarAnno(AnnotatedTypeMirror atm, T return varSlot; } - public VariableSlot getTopConstant() { + public ConstantSlot getTopConstant() { return slotManager.createConstantSlot(realTop); } @@ -624,7 +625,7 @@ public Void visitDeclared(final AnnotatedDeclaredType adt, final Tree tree) { // already annotated. case STRING_LITERAL: case IDENTIFIER: - VariableSlot primary = addPrimaryVariable(adt, tree); + Slot primary = addPrimaryVariable(adt, tree); handleWasRawDeclaredTypes(adt); addDeclarationConstraints(getOrCreateDeclBound(adt), primary); break; @@ -796,7 +797,7 @@ private void handleClassDeclaration(AnnotatedDeclaredType classType, ClassTree c visitTogether(classType.getTypeArguments(), classTree.getTypeParameters()); - VariableSlot varSlot = getOrCreateDeclBound(classType); + Slot varSlot = getOrCreateDeclBound(classType); classType.addAnnotation(slotManager.getAnnotation(varSlot)); // before we were relying on trees but the ClassTree has it's type args erased @@ -1050,7 +1051,7 @@ private void annotateArrayLiteral(AnnotatedArrayType type, NewArrayTree tree) { // add an actual variable // Add a variable to the outer type. - VariableSlot slot = addPrimaryVariable(type, tree); + Slot slot = addPrimaryVariable(type, tree); TreePath pathToTree = inferenceTypeFactory.getPath(tree); ASTRecord astRecord = ASTPathUtil.getASTRecordForPath(inferenceTypeFactory, pathToTree); @@ -1524,7 +1525,7 @@ public void handleBinaryTree(AnnotatedTypeMirror atm, BinaryTree binaryTree) { atm.clearAnnotations(); atm.addAnnotations(lubs); if (slotManager.getVariableSlot(atm).isVariable()) { - final Pair> varATMPair = Pair.>of( + final Pair> varATMPair = Pair.>of( slotManager.getVariableSlot(atm), lubs); treeToVarAnnoPair.put(binaryTree, varATMPair); } else { @@ -1616,12 +1617,12 @@ protected Boolean scan(AnnotatedTypeMirror type, Void aVoid) { * This method returns the annotation that may or may not be placed on the class declaration for type. * If it does not already exist, this method creates the annotation and stores it in classDeclAnnos. */ - private VariableSlot getOrCreateDeclBound(AnnotatedDeclaredType type) { + private Slot getOrCreateDeclBound(AnnotatedDeclaredType type) { TypeElement classDecl = (TypeElement) type.getUnderlyingType().asElement(); - VariableSlot topConstant = getTopConstant(); - VariableSlot declSlot = classDeclAnnos.get(classDecl); + Slot topConstant = getTopConstant(); + Slot declSlot = classDeclAnnos.get(classDecl); if (declSlot == null) { Tree decl = inferenceTypeFactory.declarationFromElement(classDecl); if (decl != null) { @@ -1637,7 +1638,7 @@ private VariableSlot getOrCreateDeclBound(AnnotatedDeclaredType type) { return declSlot; } - private void addDeclarationConstraints(VariableSlot declSlot, VariableSlot instanceSlot) { + private void addDeclarationConstraints(Slot declSlot, Slot instanceSlot) { constraintManager.addSubtypeConstraint(instanceSlot, declSlot); } diff --git a/src/checkers/inference/VariableSlotReplacer.java b/src/checkers/inference/VariableSlotReplacer.java index a6a110dfa..455186a39 100644 --- a/src/checkers/inference/VariableSlotReplacer.java +++ b/src/checkers/inference/VariableSlotReplacer.java @@ -11,6 +11,7 @@ import javax.lang.model.element.AnnotationMirror; import checkers.inference.model.ExistentialVariableSlot; +import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; /** @@ -55,7 +56,7 @@ public VariableSlotReplacer(final Collection initialReplacements, f replacements.addAll(initialReplacements); } - public VariableSlotReplacer addReplacement(final VariableSlot oldSlot, final VariableSlot newSlot) { + public VariableSlotReplacer addReplacement(final Slot oldSlot, final Slot newSlot) { this.replacements.add(new Replacement(oldSlot, newSlot)); return this; } @@ -101,7 +102,7 @@ protected Void scan(AnnotatedTypeMirror type, Set replacements) { protected void testAndReplace(Replacement replacement, AnnotatedTypeMirror type) { AnnotationMirror anno = type.getAnnotationInHierarchy(varAnnot); if (anno != null) { - VariableSlot variable = (VariableSlot) slotManager.getSlot(anno); + Slot variable = slotManager.getSlot(anno); if (slotManager.getVariableSlot(type).equals(replacement.oldSlot)) { final AnnotationMirror newAnnotation = slotManager.getAnnotation(replacement.newSlot); @@ -109,7 +110,7 @@ protected void testAndReplace(Replacement replacement, AnnotatedTypeMirror type) } else if (replaceInExistentials && variable instanceof ExistentialVariableSlot) { - VariableSlot existentialReplacement = + Slot existentialReplacement = constructExistentialReplacement(replacement, (ExistentialVariableSlot) variable); if (existentialReplacement != null) { final AnnotationMirror newAnnotation = slotManager.getAnnotation(existentialReplacement); @@ -120,13 +121,13 @@ protected void testAndReplace(Replacement replacement, AnnotatedTypeMirror type) } - protected VariableSlot constructExistentialReplacement(Replacement replacement, + protected Slot constructExistentialReplacement(Replacement replacement, ExistentialVariableSlot variable) { - VariableSlot potential = variable.getPotentialSlot(); + Slot potential = variable.getPotentialSlot(); AnnotationMirror potentialAnno = null; // alternative may itself be another existential - VariableSlot alternative = variable.getAlternativeSlot(); + Slot alternative = variable.getAlternativeSlot(); boolean replace = false; @@ -140,7 +141,7 @@ protected VariableSlot constructExistentialReplacement(Replacement replacement, replace = true; } else if (alternative instanceof ExistentialVariableSlot) { - VariableSlot existentialAlternative = + Slot existentialAlternative = constructExistentialReplacement(replacement, (ExistentialVariableSlot) alternative); if (existentialAlternative != null) { @@ -158,10 +159,10 @@ protected VariableSlot constructExistentialReplacement(Replacement replacement, } public static class Replacement { - public final VariableSlot oldSlot; - public final VariableSlot newSlot; + public final Slot oldSlot; + public final Slot newSlot; - public Replacement(final VariableSlot oldSlot, final VariableSlot newSlot) { + public Replacement(final Slot oldSlot, final Slot newSlot) { this.oldSlot = oldSlot; this.newSlot = newSlot; diff --git a/src/checkers/inference/dataflow/InferenceValue.java b/src/checkers/inference/dataflow/InferenceValue.java index 514539a01..749860486 100644 --- a/src/checkers/inference/dataflow/InferenceValue.java +++ b/src/checkers/inference/dataflow/InferenceValue.java @@ -119,8 +119,8 @@ public CFValue mostSpecific(CFValue other, CFValue backup) { */ public CFValue mostSpecificFromSlot(final Slot thisSlot, final Slot otherSlot, final CFValue other, final CFValue backup) { if (thisSlot.isVariable() && otherSlot.isVariable()) { - VariableSlot thisVarSlot = (VariableSlot) thisSlot; - VariableSlot otherVarSlot = (VariableSlot) otherSlot; + Slot thisVarSlot = thisSlot; + Slot otherVarSlot = otherSlot; if (thisVarSlot.isMergedTo(otherVarSlot)) { return other; } else if (otherVarSlot.isMergedTo(thisVarSlot)) { diff --git a/src/checkers/inference/model/ArithmeticVariableSlot.java b/src/checkers/inference/model/ArithmeticVariableSlot.java index a0d8c87f7..a2406c9ce 100644 --- a/src/checkers/inference/model/ArithmeticVariableSlot.java +++ b/src/checkers/inference/model/ArithmeticVariableSlot.java @@ -4,10 +4,10 @@ * ArithmeticVariableSlot represent the result of an arithmetic operation between two other * {@link VariableSlot}s. Note that this slot is serialized identically to a {@link VariableSlot}. */ -public class ArithmeticVariableSlot extends VariableSlot { +public class ArithmeticVariableSlot extends Slot { public ArithmeticVariableSlot(AnnotationLocation location, int id) { - super(location, id); + super(id, location); } @Override diff --git a/src/checkers/inference/model/CombVariableSlot.java b/src/checkers/inference/model/CombVariableSlot.java index 18dd35a01..4578f8815 100644 --- a/src/checkers/inference/model/CombVariableSlot.java +++ b/src/checkers/inference/model/CombVariableSlot.java @@ -11,13 +11,13 @@ * TODO: One thing to note, is the viewpoint adaptation locations I believe should be * TODO: accompanied with a CombineConstraint where as the LUBs only use the subtype constraints */ -public class CombVariableSlot extends VariableSlot { +public class CombVariableSlot extends Slot { private final Slot first; private final Slot second; public CombVariableSlot(AnnotationLocation location, int id, Slot first, Slot second) { - super(location, id); + super(id, location); this.first = first; this.second = second; } diff --git a/src/checkers/inference/model/ConstantSlot.java b/src/checkers/inference/model/ConstantSlot.java index 97ea515f7..e20058679 100644 --- a/src/checkers/inference/model/ConstantSlot.java +++ b/src/checkers/inference/model/ConstantSlot.java @@ -15,7 +15,7 @@ * will be represented by a ConstantSlot( @NonNull ) * */ -public class ConstantSlot extends VariableSlot { +public class ConstantSlot extends Slot { /** * The annotation in the real type system that this slot is equivalent to @@ -41,7 +41,7 @@ public class ConstantSlot extends VariableSlot { * program */ public ConstantSlot(AnnotationMirror value, AnnotationLocation location, int id) { - super(location, id); + super(id, location); checkAndSetValue(value); } diff --git a/src/checkers/inference/model/ExistentialVariableSlot.java b/src/checkers/inference/model/ExistentialVariableSlot.java index 3df615e39..7fd47b415 100644 --- a/src/checkers/inference/model/ExistentialVariableSlot.java +++ b/src/checkers/inference/model/ExistentialVariableSlot.java @@ -48,15 +48,15 @@ * } * } */ -public class ExistentialVariableSlot extends VariableSlot { +public class ExistentialVariableSlot extends Slot { // a variable whose annotation may or may not exist in source code - private final VariableSlot potentialSlot; + private final Slot potentialSlot; // the variable which would take part in a constraint if potentialSlot does not exist - private final VariableSlot alternativeSlot; + private final Slot alternativeSlot; - public ExistentialVariableSlot(int id, VariableSlot potentialSlot, VariableSlot alternativeSlot) { + public ExistentialVariableSlot(int id, Slot potentialSlot, Slot alternativeSlot) { super(id); setInsertable(false); @@ -86,11 +86,11 @@ public Kind getKind() { return Kind.EXISTENTIAL_VARIABLE; } - public VariableSlot getPotentialSlot() { + public Slot getPotentialSlot() { return potentialSlot; } - public VariableSlot getAlternativeSlot() { + public Slot getAlternativeSlot() { return alternativeSlot; } diff --git a/src/checkers/inference/model/LubVariableSlot.java b/src/checkers/inference/model/LubVariableSlot.java index eece91e62..0c52dea21 100644 --- a/src/checkers/inference/model/LubVariableSlot.java +++ b/src/checkers/inference/model/LubVariableSlot.java @@ -3,13 +3,13 @@ /** * LubVariableSlot models the least-upper-bounds of two other slots. */ -public class LubVariableSlot extends VariableSlot { +public class LubVariableSlot extends Slot { private final Slot left; private final Slot right; public LubVariableSlot(AnnotationLocation location, int id, Slot left, Slot right) { - super(location, id); + super(id, location); this.left = left; this.right = right; } diff --git a/src/checkers/inference/model/RefinementVariableSlot.java b/src/checkers/inference/model/RefinementVariableSlot.java index 39b11e906..b12c1b994 100644 --- a/src/checkers/inference/model/RefinementVariableSlot.java +++ b/src/checkers/inference/model/RefinementVariableSlot.java @@ -58,12 +58,12 @@ * Essentially, RefinementVariableSlots allow us to generate constraints as if the code were written in * SSA form ( http://en.wikipedia.org/wiki/Static_single_assignment_form ). */ -public class RefinementVariableSlot extends VariableSlot { +public class RefinementVariableSlot extends Slot { private final Slot refined; public RefinementVariableSlot(AnnotationLocation location, int id, Slot refined) { - super(location, id); + super(id, location); this.refined = refined; } diff --git a/src/checkers/inference/model/Serializer.java b/src/checkers/inference/model/Serializer.java index 8fd10b6c2..3cb4d2379 100644 --- a/src/checkers/inference/model/Serializer.java +++ b/src/checkers/inference/model/Serializer.java @@ -26,6 +26,8 @@ public interface Serializer { T serialize(InequalityConstraint constraint); + S serialize(Slot slot); + S serialize(VariableSlot slot); S serialize(ConstantSlot slot); @@ -47,5 +49,4 @@ public interface Serializer { T serialize(ImplicationConstraint implicationConstraint); T serialize(ArithmeticConstraint arithmeticConstraint); - } diff --git a/src/checkers/inference/model/Slot.java b/src/checkers/inference/model/Slot.java index 9a368ddae..552ecfd50 100644 --- a/src/checkers/inference/model/Slot.java +++ b/src/checkers/inference/model/Slot.java @@ -1,5 +1,9 @@ package checkers.inference.model; +import java.util.Collections; +import java.util.HashSet; +import java.util.Set; + /** * Slots represent logical variables over which Constraints are generated. * @@ -7,7 +11,7 @@ * within type-systems. E.g: an int literal is always NonNull but can't hold an annotation, * nonetheless, we generate a ConstantSlot representing the literal. */ -public abstract class Slot { +public abstract class Slot implements Comparable { /** * Used to locate this Slot in source code. ASTRecords are written to Jaif files along with the @@ -16,23 +20,54 @@ public abstract class Slot { private AnnotationLocation location; /** - * Create a slot with a default location of {@link AnnotationLocation#MISSING_LOCATION}. + * Uniquely identifies this Slot. id's are monotonically increasing in value by the order they + * are generated */ - public Slot() { - location = AnnotationLocation.MISSING_LOCATION; - } + private final int id; + + /** + * Should this VariableSlot be inserted back into the source code. + * This should be false for types have have an implicit annotation + * and slots for pre-annotated code. + */ + private boolean insertable; /** * Create a Slot with the given annotation location. * + * @param id Unique identifier for this variable + * @param insertable whether this variable is insertable into source code or not * @param location an AnnotationLocation for which the slot is attached to */ - public Slot(AnnotationLocation location) { + public Slot(int id, AnnotationLocation location) { + this.id = id; + this.insertable = false; this.location = location; } + /** + * Create a slot with a default location of + * {@link AnnotationLocation#MISSING_LOCATION}. + * + * @param id Unique identifier for this variable + * @param insertable whether this variable is insertable into source code or not + */ + public Slot(int id) { + this(id, AnnotationLocation.MISSING_LOCATION); + } + + // Slots this variable has been merged to. + private final Set mergedToSlots = new HashSet<>(); + + // Refinement variables that refine this slot. + private final Set refinedToSlots = new HashSet<>(); + public abstract S serialize(Serializer serializer); + public int getId() { + return id; + } + public AnnotationLocation getLocation() { return location; } @@ -41,6 +76,19 @@ public void setLocation(AnnotationLocation location) { this.location = location; } + /** + * Should this VariableSlot be inserted back into the source code. + * This should be false for types have have an implicit annotation + * and slots for pre-annotated code. + */ + public boolean isInsertable() { + return insertable; + } + + public void setInsertable(boolean insertable) { + this.insertable = insertable; + } + public abstract Kind getKind(); public enum Kind { @@ -58,6 +106,60 @@ public boolean isVariable() { } public boolean isConstant() { - return getKind() == Kind.CONSTANT; + return this instanceof ConstantSlot; } + + public boolean isMergedTo(Slot other) { + for (Slot mergedTo: mergedToSlots) { + if (mergedTo.equals(other)) { + return true; + } else { + if (mergedTo.isMergedTo(other)) { + return true; + } + } + } + return false; + } + + public Set getMergedToSlots() { + return Collections.unmodifiableSet(mergedToSlots); + } + + public void addMergedToSlot(LubVariableSlot mergedSlot) { + this.mergedToSlots.add(mergedSlot); + } + + public Set getRefinedToSlots() { + return refinedToSlots; + } + + @Override + public String toString() { + return this.getClass().getSimpleName() + "(" + id + ")"; + } + + @Override + public int hashCode() { + return id; + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + Slot other = (Slot) obj; + if (id != other.id) + return false; + return true; + } + + @Override + public int compareTo(Slot other) { + return Integer.compare(id, other.id); + } } diff --git a/src/checkers/inference/model/VariableSlot.java b/src/checkers/inference/model/VariableSlot.java index 06e1033f7..7f13818aa 100644 --- a/src/checkers/inference/model/VariableSlot.java +++ b/src/checkers/inference/model/VariableSlot.java @@ -1,11 +1,9 @@ package checkers.inference.model; -import java.util.Collections; -import java.util.HashSet; -import java.util.Set; - import javax.lang.model.type.TypeMirror; +import org.checkerframework.javacutil.AnnotationUtils; + /** * VariableSlot is a Slot representing an undetermined value (i.e. a variable we are solving for). * After the Solver is run, each VariableSlot should have an assigned value which is then written @@ -23,20 +21,7 @@ * Variable slot hold references to slots it is refined by, and slots it is merged to. * */ -public class VariableSlot extends Slot implements Comparable{ - - /** - * Uniquely identifies this Slot. id's are monotonically increasing in value by the order they - * are generated - */ - private final int id; - - /** - * Should this VariableSlot be inserted back into the source code. - * This should be false for types have have an implicit annotation - * and slots for pre-annotated code. - */ - private boolean insertable = true; +public class VariableSlot extends Slot { /** Actual type wrapped with this TypeMirror. */ protected final TypeMirror actualType; @@ -46,8 +31,7 @@ public class VariableSlot extends Slot implements Comparable{ * @param id Unique identifier for this variable */ public VariableSlot(AnnotationLocation location, int id) { - super(location); - this.id = id; + super(id, location); this.actualType = null; } @@ -57,17 +41,18 @@ public VariableSlot(AnnotationLocation location, int id) { * @param type the underlying type */ public VariableSlot(AnnotationLocation location, int id, TypeMirror type) { - super(location); - this.id = id; + super(id, location); this.actualType = type; } - - // Slots this variable has been merged to. - private final Set mergedToSlots = new HashSet<>(); - - // Refinement variables that refine this slot. - private final Set refinedToSlots = new HashSet<>(); + /** + * @param location Used to locate this variable in code, see @AnnotationLocation + * @param id Unique identifier for this variable + */ + public VariableSlot(int id) { + super(id); + this.actualType = null; + } @Override public S serialize(Serializer serializer) { @@ -79,19 +64,6 @@ public Kind getKind() { return Kind.VARIABLE; } - public boolean isMergedTo(VariableSlot other) { - for (VariableSlot mergedTo: mergedToSlots) { - if (mergedTo.equals(other)) { - return true; - } else { - if (mergedTo.isMergedTo(other)) { - return true; - } - } - } - return false; - } - /** * Returns the underlying unannotated Java type, which this wraps. * @@ -101,66 +73,11 @@ public TypeMirror getUnderlyingType() { return actualType; } - public int getId() { - return id; - } - - public VariableSlot(int id) { - this.id = id; - this.actualType = null; - } - - public VariableSlot(int id, TypeMirror type) { - this.id = id; - this.actualType = type; - } - - public Set getMergedToSlots() { - return Collections.unmodifiableSet(mergedToSlots); - } - - public void addMergedToSlot(LubVariableSlot mergedSlot) { - this.mergedToSlots.add(mergedSlot); - } - - public Set getRefinedToSlots() { - return refinedToSlots; - } - + /** + * Should this VariableSlot be inserted back into the source code. + */ @Override - public String toString() { - return this.getClass().getSimpleName() + "(" + id + ")"; - } - public boolean isInsertable() { - return insertable; - } - - public void setInsertable(boolean insertable) { - this.insertable = insertable; - } - - @Override - public int hashCode() { - return id; - } - - @Override - public boolean equals(Object obj) { - if (this == obj) - return true; - if (obj == null) - return false; - if (getClass() != obj.getClass()) - return false; - VariableSlot other = (VariableSlot) obj; - if (id != other.id) - return false; - return true; - } - - @Override - public int compareTo(VariableSlot other) { - return Integer.compare(id, other.id); + return false; } } diff --git a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java index 0d4297f17..43d95358a 100644 --- a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java +++ b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java @@ -215,6 +215,12 @@ public boolean emptyClause(VecInt ... clauses) { return false; } + @Override + public VecInt[] serialize(Slot slot) { + // doesn't really mean anything + return null; + } + @Override public VecInt[] serialize(VariableSlot slot) { // doesn't really mean anything diff --git a/src/checkers/inference/model/serialization/JsonSerializer.java b/src/checkers/inference/model/serialization/JsonSerializer.java index 485059545..ef6faa2c4 100644 --- a/src/checkers/inference/model/serialization/JsonSerializer.java +++ b/src/checkers/inference/model/serialization/JsonSerializer.java @@ -213,13 +213,18 @@ protected String getConstantString(AnnotationMirror value) { } @Override - public String serialize(VariableSlot slot) { + public String serialize(Slot slot) { return VAR_PREFIX + slot.getId(); } + @Override + public String serialize(VariableSlot slot) { + return serialize((Slot) slot); + } + @Override public String serialize(RefinementVariableSlot slot) { - return serialize((VariableSlot) slot); + return serialize((Slot) slot); } @Override @@ -235,12 +240,12 @@ public String serialize(ConstantSlot slot) { @Override public String serialize(CombVariableSlot slot) { - return serialize((VariableSlot) slot); + return serialize((Slot) slot); } @Override public String serialize(LubVariableSlot slot) { - return serialize((VariableSlot) slot); + return serialize((Slot) slot); } @SuppressWarnings("unchecked") diff --git a/src/checkers/inference/model/serialization/ToStringSerializer.java b/src/checkers/inference/model/serialization/ToStringSerializer.java index 660800fa2..129d71582 100644 --- a/src/checkers/inference/model/serialization/ToStringSerializer.java +++ b/src/checkers/inference/model/serialization/ToStringSerializer.java @@ -302,6 +302,14 @@ private String getAssumptionsString(ImplicationConstraint implicationConstraint) } // variables + @Override + public String serialize(Slot slot) { + final StringBuilder sb = new StringBuilder(); + sb.append(slot.getId()); + optionallyShowVerbose(slot, sb); + return sb.toString(); + } + @Override public String serialize(VariableSlot slot) { final StringBuilder sb = new StringBuilder(); @@ -368,21 +376,21 @@ public String getCurrentIndentString() { return indentStrings.get(indentationLevel); } - private void formatMerges(final VariableSlot slot, final StringBuilder sb) { + private void formatMerges(final Slot slot, final StringBuilder sb) { if (!slot.getMergedToSlots().isEmpty()) { sb.append(": merged to -> ") .append(slot.getMergedToSlots()); } } - private void optionallyShowVerbose(final VariableSlot varSlot, final StringBuilder sb) { + private void optionallyShowVerbose(final Slot varSlot, final StringBuilder sb) { if (showVerboseVars) { formatMerges(varSlot, sb); optionallyFormatAstPath(varSlot, sb); } } - private void optionallyFormatAstPath(final VariableSlot varSlot, final StringBuilder sb) { + private void optionallyFormatAstPath(final Slot varSlot, final StringBuilder sb) { if (showAstPaths && (varSlot.isInsertable() || (varSlot.getLocation() != null))) { sb.append("\n") .append(getCurrentIndentString()) diff --git a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java index b84f82c7f..186e639a1 100644 --- a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java +++ b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java @@ -13,6 +13,7 @@ import checkers.inference.model.LubVariableSlot; import checkers.inference.model.PreferenceConstraint; import checkers.inference.model.RefinementVariableSlot; +import checkers.inference.model.Slot; import checkers.inference.model.SubtypeConstraint; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.ArithmeticConstraintEncoder; @@ -207,6 +208,11 @@ public ConstraintEncodingT serialize(ArithmeticConstraint constraint) { ConstraintEncoderCoordinator.dispatch(constraint, arithmeticConstraintEncoder); } + @Override + public SlotEncodingT serialize(Slot slot) { + return null; + } + @Override public SlotEncodingT serialize(VariableSlot slot) { return null; diff --git a/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java b/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java index 36540ced8..e3e5a8a72 100644 --- a/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java +++ b/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java @@ -23,6 +23,7 @@ import checkers.inference.model.ExistentialVariableSlot; import checkers.inference.model.LubVariableSlot; import checkers.inference.model.RefinementVariableSlot; +import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.frontend.Lattice; @@ -82,7 +83,7 @@ protected final void addSoftConstraint(BoolExpr constraint, int weight, String g solver.AssertSoft(constraint, weight, group); } - public BitVecExpr serializeVarSlot(VariableSlot slot) { + public BitVecExpr serializeVarSlot(Slot slot) { if (slot instanceof ConstantSlot) { throw new BugInCF("Attempt to serializing ConstantSlot by serializeVarSlot() method. Should use serializeConstantSlot() instead!"); } diff --git a/src/checkers/inference/solver/util/PrintUtils.java b/src/checkers/inference/solver/util/PrintUtils.java index b977b2519..3c38c13e4 100644 --- a/src/checkers/inference/solver/util/PrintUtils.java +++ b/src/checkers/inference/solver/util/PrintUtils.java @@ -27,6 +27,7 @@ import checkers.inference.model.PreferenceConstraint; import checkers.inference.model.RefinementVariableSlot; import checkers.inference.model.Serializer; +import checkers.inference.model.Slot; import checkers.inference.model.SubtypeConstraint; import checkers.inference.model.VariableSlot; import checkers.inference.model.serialization.ToStringSerializer; @@ -154,7 +155,7 @@ private static void outputUnsatConstraints(PrintStream stream, Collection unsatConstraints public static final class UniqueSlotCollector implements Serializer { /** Stores a set of uniquely visited slots, sorted based on slot ID. */ - private final Set uniqueRelatedSlots; + private final Set uniqueRelatedSlots; public UniqueSlotCollector() { uniqueRelatedSlots = new TreeSet<>(); } - public Set getSlots() { + public Set getSlots() { return uniqueRelatedSlots; } - private void addSlotIfNotAdded(VariableSlot slot) { + private void addSlotIfNotAdded(Slot slot) { if (!(slot instanceof ConstantSlot)) { uniqueRelatedSlots.add(slot); } @@ -287,6 +288,12 @@ public Void serialize(ConstantSlot slot) { return null; } + @Override + public Void serialize(Slot slot) { + addSlotIfNotAdded(slot); + return null; + } + @Override public Void serialize(VariableSlot slot) { addSlotIfNotAdded(slot); diff --git a/src/checkers/inference/typearginference/InferenceTypeArgumentInference.java b/src/checkers/inference/typearginference/InferenceTypeArgumentInference.java index 2d3ddfa85..eab851259 100644 --- a/src/checkers/inference/typearginference/InferenceTypeArgumentInference.java +++ b/src/checkers/inference/typearginference/InferenceTypeArgumentInference.java @@ -41,6 +41,7 @@ import checkers.inference.VariableSlotReplacer; import checkers.inference.model.ConstraintManager; import checkers.inference.model.ExistentialVariableSlot; +import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.util.CrossFactoryAtmCopier; import checkers.inference.util.InferenceUtil; @@ -109,7 +110,7 @@ public Map inferTypeArgs(AnnotatedTypeFactory final Set targets = TypeArgInferenceUtil.methodTypeToTargets(methodType); Map targetToType = InferenceUtil.makeOrderedMap(targets, targetTypes); - Map targetToPrimary = findTargetVariableSlots(targetToType); + Map targetToPrimary = findTargetVariableSlots(targetToType); final List argTypes = TypeArgInferenceUtil.getArgumentTypes(expressionTree, typeFactory); @@ -182,7 +183,7 @@ private Set createBoundAndAssignmentAFs(AnnotatedTypeMirror assign // TODO: Figure out if we need to make copies of the types private void replaceExistentialVariables(AnnotatedExecutableType methodType, AnnotatedTypeFactory typeFactory, - Map targetToPrimary) { + Map targetToPrimary) { VariableSlotReplacer variableSlotReplacer = new VariableSlotReplacer(slotManager, variableAnnotator, varAnnot, true); @@ -194,7 +195,7 @@ private void replaceExistentialVariables(AnnotatedExecutableType methodType, Ann AnnotationMirror upperBoundAnno = AnnotatedTypes.findEffectiveAnnotationInHierarchy(inferenceTypeFactory.getQualifierHierarchy(), upperBound, varAnnot); - VariableSlot upperBoundVariable = (VariableSlot) slotManager.getSlot(upperBoundAnno); + Slot upperBoundVariable = slotManager.getSlot(upperBoundAnno); // handles the cases like , the upper bound anno on E will appear as a potential // annotation on T @@ -204,7 +205,7 @@ private void replaceExistentialVariables(AnnotatedExecutableType methodType, Ann VariableSlot lowerBoundVariable = slotManager.getVariableSlot(lowerBound); - VariableSlot newSlot = targetToPrimary.get(target); + Slot newSlot = targetToPrimary.get(target); variableSlotReplacer.addReplacement(upperBoundVariable, newSlot); variableSlotReplacer.addReplacement(lowerBoundVariable, newSlot); } @@ -220,9 +221,9 @@ private void replaceExistentialVariables(AnnotatedExecutableType methodType, Ann } - private Map findTargetVariableSlots(Map targetToType) { + private Map findTargetVariableSlots(Map targetToType) { - Map targetToVar = new LinkedHashMap<>(); + Map targetToVar = new LinkedHashMap<>(); for (TypeVariable target : targetToType.keySet()) { final AnnotatedTypeMirror type = targetToType.get(target); @@ -239,7 +240,7 @@ private Map findTargetVariableSlots(Map findTargetVariableSlots(Map Date: Mon, 11 Nov 2019 18:50:34 -0500 Subject: [PATCH 03/10] slot refactoring. Remove all cast to VariableSlot and uses Slot instead --- .../inference/ConstraintNormalizer.java | 8 +- .../inference/DefaultInferenceResult.java | 2 +- .../inference/DefaultSlotManager.java | 32 +- .../ExistentialVariableInserter.java | 9 +- .../InferenceAnnotatedTypeFactory.java | 6 +- src/checkers/inference/InferenceMain.java | 5 +- .../InferenceQualifierHierarchy.java | 4 +- src/checkers/inference/InferenceResult.java | 6 +- .../InferenceTypeVariableSubstitutor.java | 2 +- src/checkers/inference/InferenceVisitor.java | 2 +- src/checkers/inference/SlotManager.java | 4 +- src/checkers/inference/VariableAnnotator.java | 2 +- .../inference/dataflow/InferenceTransfer.java | 2 +- .../model/ArithmeticVariableSlot.java | 2 +- .../inference/model/ConstraintManager.java | 6 +- .../model/ExistentialConstraint.java | 8 +- .../inference/model/PreferenceConstraint.java | 8 +- src/checkers/inference/model/Slot.java | 2 + .../inference/model/VariableSlot.java | 13 +- .../serialization/CnfVecIntSerializer.java | 30 +- .../model/serialization/JsonDeserializer.java | 6 +- .../serialization/ToStringSerializer.java | 12 +- .../inference/solver/PropagationSolver.java | 66 ++- .../inference/solver/backend/Solver.java | 2 +- .../encoder/ArithmeticConstraintEncoder.java | 7 +- .../encoder/ConstraintEncoderCoordinator.java | 33 +- .../solver/backend/encoder/SlotSlotCombo.java | 4 +- .../binary/BinaryConstraintEncoder.java | 8 +- .../combine/CombineConstraintEncoder.java | 14 +- .../LogiQLComparableConstraintEncoder.java | 8 +- .../LogiQLEqualityConstraintEncoder.java | 8 +- .../LogiQLInequalityConstraintEncoder.java | 8 +- .../LogiQLSubtypeConstraintEncoder.java | 8 +- .../MaxSATComparableConstraintEncoder.java | 8 +- .../MaxSATEqualityConstraintEncoder.java | 8 +- .../MaxSATInequalityConstraintEncoder.java | 8 +- .../MaxSATPreferenceConstraintEncoder.java | 3 +- .../MaxSATSubtypeConstraintEncoder.java | 12 +- .../z3/Z3BitVectorFormatTranslator.java | 7 +- .../Z3BitVectorEqualityConstraintEncoder.java | 7 +- ...3BitVectorPreferenceConstraintEncoder.java | 3 +- .../Z3BitVectorSubtypeConstraintEncoder.java | 7 +- .../backend/z3smt/Z3SmtFormatTranslator.java | 91 ++++ .../solver/backend/z3smt/Z3SmtSolver.java | 493 ++++++++++++++++++ .../constraintgraph/ConstraintGraph.java | 5 +- .../solver/constraintgraph/Vertex.java | 15 +- .../inference/solver/util/Statistics.java | 4 +- .../InferenceTypeArgumentInference.java | 2 +- .../util/InferenceViewpointAdapter.java | 2 +- .../checkers/propagation/IFlowSolver.java | 2 +- 50 files changed, 789 insertions(+), 225 deletions(-) create mode 100644 src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java create mode 100644 src/checkers/inference/solver/backend/z3smt/Z3SmtSolver.java diff --git a/src/checkers/inference/ConstraintNormalizer.java b/src/checkers/inference/ConstraintNormalizer.java index 4bc883f67..dfee5aa92 100644 --- a/src/checkers/inference/ConstraintNormalizer.java +++ b/src/checkers/inference/ConstraintNormalizer.java @@ -255,7 +255,7 @@ public Set toConstraints() { ret.add(InferenceMain .getInstance() .getConstraintManager() - .createExistentialConstraint((VariableSlot) slot, ifExistsConstraints, + .createExistentialConstraint(slot, ifExistsConstraints, ifNotExistsConstraints)); return ret; } @@ -298,14 +298,14 @@ public String toString() { if (alwaysExists) { sb.append("["); sb.append( - slot.isVariable() ? ((VariableSlot) slot).getId() + slot.isVariable() ? (slot).getId() : ((ConstantSlot) slot).getValue()); sb.append("]"); } else { if (!exists) { sb.append("!"); } - sb.append(((VariableSlot) slot).getId()); + sb.append((slot).getId()); } return sb.toString(); } @@ -333,7 +333,7 @@ public int compare(Slot o1, Slot o2) { } } - return ((VariableSlot) o1).getId() - ((VariableSlot) o2).getId(); + return (o1).getId() - (o2).getId(); } } diff --git a/src/checkers/inference/DefaultInferenceResult.java b/src/checkers/inference/DefaultInferenceResult.java index a674497e9..6c13037da 100644 --- a/src/checkers/inference/DefaultInferenceResult.java +++ b/src/checkers/inference/DefaultInferenceResult.java @@ -20,7 +20,7 @@ public class DefaultInferenceResult implements InferenceResult { /** - * A map from variable Id of {@link checkers.inference.model.VariableSlot VariableSlot} + * A map from variable Id of {@link checkers.inference.model.Slot Slot} * to {@link AnnotationMirror}. * * No solution should set this field to null. Otherwise, if the map is empty, it means diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index 12a12e1f0..2f50456e8 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -50,9 +50,9 @@ public class DefaultSlotManager implements SlotManager { /** * A map for storing all the slots encountered by this slot manager. Key is * an {@link Integer}, representing a slot id. Value is a - * {@link VariableSlot} that corresponds to this slot id. Note that + * {@link Slot} that corresponds to this slot id. Note that * ConstantSlots are also stored in this map, since ConstantSlot is subclass - * of VariableSlot. + * of Slot. */ private final Map variables; @@ -72,7 +72,7 @@ public class DefaultSlotManager implements SlotManager { private final Map locationCache; /** - * A map of {@link Pair} of {@link VariableSlot} to {@link Integer} for + * A map of {@link Pair} of {@link Slot} to {@link Integer} for * caching ExistentialVariableSlot. Each ExistentialVariableSlot can be * uniquely identified by its potential and alternative VariablesSlots. * {@link Integer} is the id of the corresponding ExistentialVariableSlot @@ -174,16 +174,10 @@ public Slot getVariable( int id ) { */ @Override public AnnotationMirror getAnnotation(final Slot slot) { - // if slot is a VariableSlot or one of its subclasses - if (slot instanceof VariableSlot) { - // We need to build the AnnotationBuilder each time because AnnotationBuilders are only - // allowed to build their annotations once - return convertVariable((VariableSlot) slot, - new AnnotationBuilder(processingEnvironment, VarAnnot.class)); - } - - throw new IllegalArgumentException( - "Slot type unrecognized( " + slot.getClass() + ") Slot=" + slot.toString()); + // We need to build the AnnotationBuilder each time because AnnotationBuilders are only + // allowed to build their annotations once + return convertVariable(slot, + new AnnotationBuilder(processingEnvironment, VarAnnot.class)); } /** @@ -194,7 +188,7 @@ public AnnotationMirror getAnnotation(final Slot slot) { * build @CombVarAnnots * @return An annotation representing variable */ - private AnnotationMirror convertVariable( final VariableSlot variable, final AnnotationBuilder annotationBuilder) { + private AnnotationMirror convertVariable( final Slot variable, final AnnotationBuilder annotationBuilder) { annotationBuilder.setValue("value", variable.getId() ); return annotationBuilder.build(); } @@ -204,7 +198,7 @@ private AnnotationMirror convertVariable( final VariableSlot variable, final Ann * @inheritDoc */ @Override - public VariableSlot getVariableSlot( final AnnotatedTypeMirror atm ) { + public Slot getVariableSlot( final AnnotatedTypeMirror atm ) { AnnotationMirror annot = atm.getAnnotationInHierarchy(this.varAnnot); if (annot == null) { @@ -215,7 +209,7 @@ public VariableSlot getVariableSlot( final AnnotatedTypeMirror atm ) { throw new BugInCF("Missing VarAnnot annotation: " + atm); } - return (VariableSlot) getSlot(annot); + return getSlot(annot); } /** @@ -271,11 +265,11 @@ public List getSlots() { * @inheritDoc */ @Override - public List getVariableSlots() { - List varSlots = new ArrayList<>(); + public List getVariableSlots() { + List varSlots = new ArrayList<>(); for (Slot slot : variables.values()) { if (slot.isVariable()) { - varSlots.add((VariableSlot) slot); + varSlots.add(slot); } } return varSlots; diff --git a/src/checkers/inference/ExistentialVariableInserter.java b/src/checkers/inference/ExistentialVariableInserter.java index 992da9b62..5ce6ccdcc 100644 --- a/src/checkers/inference/ExistentialVariableInserter.java +++ b/src/checkers/inference/ExistentialVariableInserter.java @@ -104,7 +104,7 @@ public void insert(final Slot potentialVariable, final AnnotatedTypeMirror typeU */ public void insert(final Slot potentialVariable, final AnnotatedTypeMirror typeUse, final AnnotatedTypeMirror declaration, boolean mustExist) { - if (potentialVariable == null || !(potentialVariable instanceof VariableSlot)) { + if (potentialVariable == null) { throw new BugInCF("Bad type variable slot: slot=" + potentialVariable); } @@ -151,10 +151,9 @@ public void matchAndReplacePrimary(final AnnotatedTypeMirror typeUse, final Anno } } - if (declSlot instanceof VariableSlot) { - final VariableSlot varSlot = slotManager.getVariableSlot(declaration); + if (declSlot.isVariable()) { final ExistentialVariableSlot existVar = - varAnnotator.getOrCreateExistentialVariable(typeUse, potentialVariable, varSlot); + varAnnotator.getOrCreateExistentialVariable(typeUse, potentialVariable, declSlot); } else if (!InferenceMain.isHackMode()) { throw new BugInCF("Unexpected constant slot in:" + declaration); @@ -277,7 +276,7 @@ private boolean matchesSlot(final AnnotatedTypeMirror type) { return false; } - VariableSlot varSlot = slotManager.getVariableSlot(type); + Slot varSlot = slotManager.getVariableSlot(type); if (varSlot == null) { return false; } diff --git a/src/checkers/inference/InferenceAnnotatedTypeFactory.java b/src/checkers/inference/InferenceAnnotatedTypeFactory.java index 5c9873d4c..755cdc43e 100644 --- a/src/checkers/inference/InferenceAnnotatedTypeFactory.java +++ b/src/checkers/inference/InferenceAnnotatedTypeFactory.java @@ -48,7 +48,9 @@ import javax.lang.model.type.TypeVariable; import checkers.inference.dataflow.InferenceAnalysis; +import checkers.inference.model.ConstantSlot; import checkers.inference.model.ConstraintManager; +import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.qual.VarAnnot; import checkers.inference.util.ConstantToVariableAnnotator; @@ -122,7 +124,7 @@ public class InferenceAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { // though we know the value of that variable. In this case, rather than creating a new variable // for every one of these locations and increase the number of variables we solve for, use // the same variable slot for all of these locations. This map contains those variables. - private Map, VariableSlot> constantToVarAnnot = new HashMap<>(); + private Map, ConstantSlot> constantToVarAnnot = new HashMap<>(); public InferenceAnnotatedTypeFactory( InferenceChecker inferenceChecker, @@ -263,7 +265,7 @@ protected DependentTypesHelper createDependentTypesHelper() { return null; } - protected Map, VariableSlot> getConstantVars() { + protected Map, ConstantSlot> getConstantVars() { return Collections.unmodifiableMap(constantToVarAnnot); } diff --git a/src/checkers/inference/InferenceMain.java b/src/checkers/inference/InferenceMain.java index ea05b0715..90d1a5764 100644 --- a/src/checkers/inference/InferenceMain.java +++ b/src/checkers/inference/InferenceMain.java @@ -22,6 +22,7 @@ import checkers.inference.model.AnnotationLocation; import checkers.inference.model.Constraint; import checkers.inference.model.ConstraintManager; +import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.qual.VarAnnot; import checkers.inference.util.InferenceUtil; @@ -215,7 +216,7 @@ private void writeJaif() { try (PrintWriter writer = new PrintWriter(new FileOutputStream(InferenceOptions.jaifFile))) { - List varSlots = slotManager.getVariableSlots(); + List varSlots = slotManager.getVariableSlots(); Map values = new HashMap<>(); Set> annotationClasses = new HashSet<>(); @@ -230,7 +231,7 @@ private void writeJaif() { annotationClasses.add(annotation); } } - for (VariableSlot slot : varSlots) { + for (Slot slot : varSlots) { if (slot.getLocation() != null && slot.isInsertable() && (solverResult == null || solverResult.containsSolutionForVariable(slot.getId()))) { // TODO: String serialization of annotations. diff --git a/src/checkers/inference/InferenceQualifierHierarchy.java b/src/checkers/inference/InferenceQualifierHierarchy.java index 52103bb7e..d6d9c0c08 100644 --- a/src/checkers/inference/InferenceQualifierHierarchy.java +++ b/src/checkers/inference/InferenceQualifierHierarchy.java @@ -264,8 +264,8 @@ public AnnotationMirror leastUpperBound(final AnnotationMirror a1, final Annotat Slot constantSlot = slotMgr.createConstantSlot(realLub); return slotMgr.getAnnotation(constantSlot); } else { - VariableSlot var1 = (VariableSlot) slot1; - VariableSlot var2 = (VariableSlot) slot2; + Slot var1 = slot1; + Slot var2 = slot2; if (var1 == var2) { // They are the same slot. diff --git a/src/checkers/inference/InferenceResult.java b/src/checkers/inference/InferenceResult.java index d64a6d93d..37f9fd443 100644 --- a/src/checkers/inference/InferenceResult.java +++ b/src/checkers/inference/InferenceResult.java @@ -36,7 +36,7 @@ public interface InferenceResult { /** * A method to check if there is solution for a particular variable ID or not. * - * @param varId id of a {@link checkers.inference.model.VariableSlot VariableSlot} + * @param varId id of a {@link checkers.inference.model.Slot Slot} * @return true iff {@link #hasSolution()} returns true and internal inferred * result(implementation detail) contains solution for {@code varId} * @@ -46,9 +46,9 @@ public interface InferenceResult { boolean containsSolutionForVariable(int varId); /** - * A method to get the inferred solution for the given variable ID. + * A method to get the inferred solution for the given slot ID. * - * @param varId id of a {@link checkers.inference.model.VariableSlot VariableSlot} + * @param varId id of a {@link checkers.inference.model.Slot Slot} * @return non-null solution iff {@link #hasSolution()} returns true and internal * inferred result(implementation detail) contains solution for {@code varId} * diff --git a/src/checkers/inference/InferenceTypeVariableSubstitutor.java b/src/checkers/inference/InferenceTypeVariableSubstitutor.java index c59762880..ed2af3b75 100644 --- a/src/checkers/inference/InferenceTypeVariableSubstitutor.java +++ b/src/checkers/inference/InferenceTypeVariableSubstitutor.java @@ -71,7 +71,7 @@ protected AnnotatedTypeMirror substituteTypeVariable(AnnotatedTypeMirror argumen if (argument.getKind() != TypeKind.TYPEVAR) { final Slot altSlot = slotManager.getVariableSlot(argument); - final VariableSlot alternative = (VariableSlot) altSlot; + final Slot alternative = altSlot; if (alternative != null) { final ExistentialVariableSlot slot = slotManager.createExistentialVariableSlot(potentialSlot, alternative); argument.replaceAnnotation(slotManager.getAnnotation(slot)); diff --git a/src/checkers/inference/InferenceVisitor.java b/src/checkers/inference/InferenceVisitor.java index e76cd9468..d10f69651 100644 --- a/src/checkers/inference/InferenceVisitor.java +++ b/src/checkers/inference/InferenceVisitor.java @@ -255,7 +255,7 @@ public void addPreference(AnnotatedTypeMirror type, AnnotationMirror anno, int w if (infer) { ConstraintManager cManager = InferenceMain.getInstance().getConstraintManager(); SlotManager sManager = InferenceMain.getInstance().getSlotManager(); - VariableSlot vSlot = sManager.getVariableSlot(type); + Slot vSlot = sManager.getVariableSlot(type); ConstantSlot cSlot = InferenceMain.getInstance().getSlotManager().createConstantSlot(anno); cManager.addPreferenceConstraint(vSlot, cSlot, weight); } diff --git a/src/checkers/inference/SlotManager.java b/src/checkers/inference/SlotManager.java index e4073f576..bced6a806 100644 --- a/src/checkers/inference/SlotManager.java +++ b/src/checkers/inference/SlotManager.java @@ -179,7 +179,7 @@ public interface SlotManager { * there is no VariableSlot this method throws an exception * @param atm An annotated type mirror with a VarAnnot in its primary annotations list */ - VariableSlot getVariableSlot(AnnotatedTypeMirror atm); + Slot getVariableSlot(AnnotatedTypeMirror atm); /** * Return all slots collected by this SlotManager @@ -191,7 +191,7 @@ public interface SlotManager { * Return all VariableSlots collected by this SlotManager * @return a lit of VariableSlots */ - List getVariableSlots(); + List getVariableSlots(); List getConstantSlots(); } diff --git a/src/checkers/inference/VariableAnnotator.java b/src/checkers/inference/VariableAnnotator.java index c14c6c80f..2b0ccfd2a 100644 --- a/src/checkers/inference/VariableAnnotator.java +++ b/src/checkers/inference/VariableAnnotator.java @@ -295,7 +295,7 @@ public ConstantSlot createConstant(final AnnotationMirror value, final Tree tree */ ExistentialVariableSlot getOrCreateExistentialVariable(final AnnotatedTypeMirror atm, final Slot potentialVariable, - final VariableSlot alternativeSlot) { + final Slot alternativeSlot) { ExistentialVariableSlot existentialVariable = getOrCreateExistentialVariable(potentialVariable, alternativeSlot); atm.replaceAnnotation(slotManager.getAnnotation(existentialVariable)); return existentialVariable; diff --git a/src/checkers/inference/dataflow/InferenceTransfer.java b/src/checkers/inference/dataflow/InferenceTransfer.java index 268420c35..d855b7504 100644 --- a/src/checkers/inference/dataflow/InferenceTransfer.java +++ b/src/checkers/inference/dataflow/InferenceTransfer.java @@ -217,7 +217,7 @@ private TransferResult createRefinementVar(Node lhs, // Fields from library methods can be refined, but the slotToRefine is a ConstantSlot // which does not have a refined slots field. if (slotToRefine.isVariable()) { - ((VariableSlot) slotToRefine).getRefinedToSlots().add(refVar); + slotToRefine.getRefinedToSlots().add(refVar); } createdRefinementVariables.put(assignmentTree, refVar); diff --git a/src/checkers/inference/model/ArithmeticVariableSlot.java b/src/checkers/inference/model/ArithmeticVariableSlot.java index a2406c9ce..a38c5ec10 100644 --- a/src/checkers/inference/model/ArithmeticVariableSlot.java +++ b/src/checkers/inference/model/ArithmeticVariableSlot.java @@ -2,7 +2,7 @@ /** * ArithmeticVariableSlot represent the result of an arithmetic operation between two other - * {@link VariableSlot}s. Note that this slot is serialized identically to a {@link VariableSlot}. + * {@link Slot}s. Note that this slot is serialized identically to a {@link Slot}. */ public class ArithmeticVariableSlot extends Slot { diff --git a/src/checkers/inference/model/ConstraintManager.java b/src/checkers/inference/model/ConstraintManager.java index aa54a2257..2ddb3e20c 100644 --- a/src/checkers/inference/model/ConstraintManager.java +++ b/src/checkers/inference/model/ConstraintManager.java @@ -129,7 +129,7 @@ public CombineConstraint createCombineConstraint(Slot target, Slot decl, Slot re /** * Creates a {@link PreferenceConstraint} for the given slots with the given weight. */ - public PreferenceConstraint createPreferenceConstraint(VariableSlot variable, ConstantSlot goal, + public PreferenceConstraint createPreferenceConstraint(Slot variable, ConstantSlot goal, int weight) { return PreferenceConstraint.create(variable, goal, weight, getCurrentLocation()); } @@ -139,7 +139,7 @@ public PreferenceConstraint createPreferenceConstraint(VariableSlot variable, Co */ public ExistentialConstraint createExistentialConstraint(Slot slot, List ifExistsConstraints, List ifNotExistsConstraints) { - return ExistentialConstraint.create((VariableSlot) slot, ifExistsConstraints, + return ExistentialConstraint.create(slot, ifExistsConstraints, ifNotExistsConstraints, getCurrentLocation()); } @@ -260,7 +260,7 @@ public void addCombineConstraint(Slot target, Slot decl, Slot result) { /** * Creates and adds a {@link PreferenceConstraint} to the constraint set. */ - public void addPreferenceConstraint(VariableSlot variable, ConstantSlot goal, int weight) { + public void addPreferenceConstraint(Slot variable, ConstantSlot goal, int weight) { add(createPreferenceConstraint(variable, goal, weight)); } diff --git a/src/checkers/inference/model/ExistentialConstraint.java b/src/checkers/inference/model/ExistentialConstraint.java index 94f6807f0..2255d9287 100644 --- a/src/checkers/inference/model/ExistentialConstraint.java +++ b/src/checkers/inference/model/ExistentialConstraint.java @@ -24,7 +24,7 @@ public class ExistentialConstraint extends Constraint { // A variable whose annotation may or may not exist - private final VariableSlot potentialVariable; + private final Slot potentialVariable; // The constraints to enforce if potentialVariable exists private final List potentialConstraints; @@ -32,7 +32,7 @@ public class ExistentialConstraint extends Constraint { // the constraints to enforce if potentialVariable DOES NOT exist private final List alternateConstraints; - private ExistentialConstraint(VariableSlot potentialVariable, + private ExistentialConstraint(Slot potentialVariable, List potentialConstraints, List alternateConstraints, AnnotationLocation location) { super(combineSlots(potentialVariable, potentialConstraints, alternateConstraints), location); @@ -41,7 +41,7 @@ private ExistentialConstraint(VariableSlot potentialVariable, this.alternateConstraints = Collections.unmodifiableList(alternateConstraints); } - protected static ExistentialConstraint create(VariableSlot potentialVariable, + protected static ExistentialConstraint create(Slot potentialVariable, List potentialConstraints, List alternateConstraints, AnnotationLocation location) { if (potentialVariable == null || potentialConstraints == null @@ -68,7 +68,7 @@ private static List combineSlots(Slot potential, final List .. return Collections.unmodifiableList(slots); } - public VariableSlot getPotentialVariable() { + public Slot getPotentialVariable() { return potentialVariable; } diff --git a/src/checkers/inference/model/PreferenceConstraint.java b/src/checkers/inference/model/PreferenceConstraint.java index feb89caf5..f2e1cb8b5 100644 --- a/src/checkers/inference/model/PreferenceConstraint.java +++ b/src/checkers/inference/model/PreferenceConstraint.java @@ -8,11 +8,11 @@ */ public class PreferenceConstraint extends Constraint { - private final VariableSlot variable; + private final Slot variable; private final ConstantSlot goal; private final int weight; - private PreferenceConstraint(VariableSlot variable, ConstantSlot goal, int weight, + private PreferenceConstraint(Slot variable, ConstantSlot goal, int weight, AnnotationLocation location) { super(Arrays. asList(variable, goal), location); this.variable = variable; @@ -20,7 +20,7 @@ private PreferenceConstraint(VariableSlot variable, ConstantSlot goal, int weigh this.weight = weight; } - protected static PreferenceConstraint create(VariableSlot variable, ConstantSlot goal, + protected static PreferenceConstraint create(Slot variable, ConstantSlot goal, int weight, AnnotationLocation location) { if (variable == null || goal == null) { throw new BugInCF("Create preference constraint with null argument. Variable: " @@ -35,7 +35,7 @@ public T serialize(Serializer serializer) { return serializer.serialize(this); } - public VariableSlot getVariable() { + public Slot getVariable() { return variable; } diff --git a/src/checkers/inference/model/Slot.java b/src/checkers/inference/model/Slot.java index 552ecfd50..d73e68e4a 100644 --- a/src/checkers/inference/model/Slot.java +++ b/src/checkers/inference/model/Slot.java @@ -4,6 +4,8 @@ import java.util.HashSet; import java.util.Set; +import javax.lang.model.type.TypeMirror; + /** * Slots represent logical variables over which Constraints are generated. * diff --git a/src/checkers/inference/model/VariableSlot.java b/src/checkers/inference/model/VariableSlot.java index 7f13818aa..4c82f2fc6 100644 --- a/src/checkers/inference/model/VariableSlot.java +++ b/src/checkers/inference/model/VariableSlot.java @@ -26,15 +26,6 @@ public class VariableSlot extends Slot { /** Actual type wrapped with this TypeMirror. */ protected final TypeMirror actualType; - /** - * @param location Used to locate this variable in code, see @AnnotationLocation - * @param id Unique identifier for this variable - */ - public VariableSlot(AnnotationLocation location, int id) { - super(id, location); - this.actualType = null; - } - /** * @param location Used to locate this variable in code, see @AnnotationLocation * @param id Unique identifier for this variable @@ -49,9 +40,9 @@ public VariableSlot(AnnotationLocation location, int id, TypeMirror type) { * @param location Used to locate this variable in code, see @AnnotationLocation * @param id Unique identifier for this variable */ - public VariableSlot(int id) { + public VariableSlot(int id, TypeMirror type) { super(id); - this.actualType = null; + this.actualType = type; } @Override diff --git a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java index 43d95358a..d2848c741 100644 --- a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java +++ b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java @@ -49,7 +49,7 @@ public VecInt[] serialize(SubtypeConstraint constraint) { return new VariableCombos() { @Override - protected VecInt[] constant_variable(ConstantSlot subtype, VariableSlot supertype, SubtypeConstraint constraint) { + protected VecInt[] constant_variable(ConstantSlot subtype, Slot supertype, SubtypeConstraint constraint) { if (isTop(subtype)) { return asVecArray(-supertype.getId()); @@ -59,7 +59,7 @@ protected VecInt[] constant_variable(ConstantSlot subtype, VariableSlot supertyp } @Override - protected VecInt[] variable_constant(VariableSlot subtype, ConstantSlot supertype, SubtypeConstraint constraint) { + protected VecInt[] variable_constant(Slot subtype, ConstantSlot supertype, SubtypeConstraint constraint) { if (!isTop(supertype)) { return asVecArray(subtype.getId()); } @@ -68,7 +68,7 @@ protected VecInt[] variable_constant(VariableSlot subtype, ConstantSlot supertyp } @Override - protected VecInt[] variable_variable(VariableSlot subtype, VariableSlot supertype, SubtypeConstraint constraint) { + protected VecInt[] variable_variable(Slot subtype, Slot supertype, SubtypeConstraint constraint) { // this is supertype => subtype which is the equivalent of (!supertype v subtype) return asVecArray(-supertype.getId(), subtype.getId()); @@ -83,7 +83,7 @@ public VecInt[] serialize(EqualityConstraint constraint) { return new VariableCombos() { @Override - protected VecInt[] constant_variable(ConstantSlot slot1, VariableSlot slot2, EqualityConstraint constraint) { + protected VecInt[] constant_variable(ConstantSlot slot1, Slot slot2, EqualityConstraint constraint) { if (isTop(slot1)) { return asVecArray(-slot2.getId()); @@ -93,12 +93,12 @@ protected VecInt[] constant_variable(ConstantSlot slot1, VariableSlot slot2, Equ } @Override - protected VecInt[] variable_constant(VariableSlot slot1, ConstantSlot slot2, EqualityConstraint constraint) { + protected VecInt[] variable_constant(Slot slot1, ConstantSlot slot2, EqualityConstraint constraint) { return constant_variable(slot2, slot1, constraint); } @Override - protected VecInt[] variable_variable(VariableSlot slot1, VariableSlot slot2, EqualityConstraint constraint) { + protected VecInt[] variable_variable(Slot slot1, Slot slot2, EqualityConstraint constraint) { // a <=> b which is the same as (!a v b) & (!b v a) return new VecInt[]{ @@ -116,7 +116,7 @@ public VecInt[] serialize(InequalityConstraint constraint) { return new VariableCombos() { @Override - protected VecInt[] constant_variable(ConstantSlot slot1, VariableSlot slot2, InequalityConstraint constraint) { + protected VecInt[] constant_variable(ConstantSlot slot1, Slot slot2, InequalityConstraint constraint) { if (isTop(slot1)) { return asVecArray(slot2.getId()); @@ -126,12 +126,12 @@ protected VecInt[] constant_variable(ConstantSlot slot1, VariableSlot slot2, Ine } @Override - protected VecInt[] variable_constant(VariableSlot slot1, ConstantSlot slot2, InequalityConstraint constraint) { + protected VecInt[] variable_constant(Slot slot1, ConstantSlot slot2, InequalityConstraint constraint) { return constant_variable(slot2, slot1, constraint); } @Override - protected VecInt[] variable_variable(VariableSlot slot1, VariableSlot slot2, InequalityConstraint constraint) { + protected VecInt[] variable_variable(Slot slot1, Slot slot2, InequalityConstraint constraint) { // a <=> !b which is the same as (!a v !b) & (b v a) return new VecInt[]{ @@ -323,15 +323,15 @@ VecInt[] asVecArray(int ... vars) { */ class VariableCombos { - protected VecInt[] variable_variable(VariableSlot slot1, VariableSlot slot2, T constraint) { + protected VecInt[] variable_variable(Slot slot1, Slot slot2, T constraint) { return defaultAction(slot1, slot2, constraint); } - protected VecInt[] constant_variable(ConstantSlot slot1, VariableSlot slot2, T constraint) { + protected VecInt[] constant_variable(ConstantSlot slot1, Slot slot2, T constraint) { return defaultAction(slot1, slot2, constraint); } - protected VecInt[] variable_constant(VariableSlot slot1, ConstantSlot slot2, T constraint) { + protected VecInt[] variable_constant(Slot slot1, ConstantSlot slot2, T constraint) { return defaultAction(slot1, slot2, constraint); } @@ -349,12 +349,12 @@ public VecInt[] accept(Slot slot1, Slot slot2, T constraint) { if (slot2 instanceof ConstantSlot) { result = constant_constant((ConstantSlot) slot1, (ConstantSlot) slot2, constraint); } else { - result = constant_variable((ConstantSlot) slot1, (VariableSlot) slot2, constraint); + result = constant_variable((ConstantSlot) slot1, slot2, constraint); } } else if (slot2 instanceof ConstantSlot) { - result = variable_constant((VariableSlot) slot1, (ConstantSlot) slot2, constraint); + result = variable_constant(slot1, (ConstantSlot) slot2, constraint); } else { - result = variable_variable((VariableSlot) slot1, (VariableSlot) slot2, constraint); + result = variable_variable(slot1, slot2, constraint); } return result; diff --git a/src/checkers/inference/model/serialization/JsonDeserializer.java b/src/checkers/inference/model/serialization/JsonDeserializer.java index 639a3aad2..7fafb8110 100644 --- a/src/checkers/inference/model/serialization/JsonDeserializer.java +++ b/src/checkers/inference/model/serialization/JsonDeserializer.java @@ -115,7 +115,7 @@ public List jsonArrayToConstraints(final JSONArray jsonConstraints) jsonArrayToConstraints((JSONArray) constraint.get(EXISTENTIAL_THEN)); List elseConstraints = jsonArrayToConstraints((JSONArray) constraint.get(EXISTENTIAL_ELSE)); - results.add(constraintManager.createExistentialConstraint((VariableSlot) potential, + results.add(constraintManager.createExistentialConstraint(potential, thenConstraints, elseConstraints)); } else { throw new IllegalArgumentException("Parse error: unknown constraint type: " + obj); @@ -142,7 +142,7 @@ private Set findPotentialVars(JSONArray constraints, Set potenti String constraintType = (String) constraint.get(CONSTRAINT_KEY); if (constraintType.equals(EXISTENTIAL_CONSTRAINT_KEY)) { - VariableSlot potential = (VariableSlot) parseSlot((String) constraint.get(EXISTENTIAL_ID)); + Slot potential = parseSlot((String) constraint.get(EXISTENTIAL_ID)); potentialVariableIds.add(String.valueOf(potential.getId())); Object thenConstraints = constraint.get(EXISTENTIAL_THEN); @@ -204,7 +204,7 @@ public Map getAnnotationValues() { private Slot parseSlot(String slot) { if (slot.startsWith(VAR_PREFIX)) { int id = new Integer(slot.split(":")[1]); - return new VariableSlot(id); + return new VariableSlot(id, null); } else { // TODO: THIS NEEDS FIXING AnnotationMirror value = annotationSerializer.deserialize(slot); diff --git a/src/checkers/inference/model/serialization/ToStringSerializer.java b/src/checkers/inference/model/serialization/ToStringSerializer.java index 129d71582..0f2d5b649 100644 --- a/src/checkers/inference/model/serialization/ToStringSerializer.java +++ b/src/checkers/inference/model/serialization/ToStringSerializer.java @@ -93,15 +93,9 @@ public String serializeSlots(Iterable slots, String delimiter) { Set serializedOtherSlots = new TreeSet<>(); for (Slot slot : slots) { - if (slot instanceof VariableSlot) { - // sort the varSlots by ID through insertion to TreeMap - VariableSlot varSlot = (VariableSlot) slot; - serializedVarSlots.put(varSlot.getId(), - getCurrentIndentString() + varSlot.serialize(this)); - } else { - // sort all other slots by serialized string content through insertion to TreeSet - serializedOtherSlots.add(getCurrentIndentString() + slot.serialize(this)); - } + // sort the varSlots by ID through insertion to TreeMap + serializedVarSlots.put(slot.getId(), + getCurrentIndentString() + slot.serialize(this)); } List serializedSlots = new ArrayList<>(); diff --git a/src/checkers/inference/solver/PropagationSolver.java b/src/checkers/inference/solver/PropagationSolver.java index 4f3d124cd..6b8711444 100644 --- a/src/checkers/inference/solver/PropagationSolver.java +++ b/src/checkers/inference/solver/PropagationSolver.java @@ -24,7 +24,6 @@ import checkers.inference.model.ExistentialConstraint; import checkers.inference.model.Slot; import checkers.inference.model.SubtypeConstraint; -import checkers.inference.model.VariableSlot; /** * InferenceSolver FloodSolver implementation @@ -91,18 +90,18 @@ public InferenceResult solve( */ public InferenceResult solve() { - Set fixedBottom = new HashSet(); - Set fixedTop = new HashSet(); - Map> superTypePropagation = new HashMap<>(); - Map> subTypePropagation = new HashMap<>(); + Set fixedBottom = new HashSet(); + Set fixedTop = new HashSet(); + Map> superTypePropagation = new HashMap<>(); + Map> subTypePropagation = new HashMap<>(); preprocessConstraints(fixedBottom, fixedTop, superTypePropagation, subTypePropagation); // Propagate supertype - Set inferredTop = propagateValues(fixedTop, superTypePropagation); + Set inferredTop = propagateValues(fixedTop, superTypePropagation); // Propagate subtype - Set inferredBottom = propagateValues(fixedBottom, subTypePropagation); + Set inferredBottom = propagateValues(fixedBottom, subTypePropagation); return mergeToResult(fixedBottom, fixedTop, inferredTop, inferredBottom); } @@ -121,10 +120,10 @@ public InferenceResult solve() { * @param superTypePropagation Map, where if a key is a supertyp, all variables in the value must also be supertype * @param subTypePropagation Map, where if a key is a subtype, all variables in the value must also be subtypes */ - private void preprocessConstraints(Set fixedBottom, - Set fixedTop, - Map> superTypePropagation, - Map> subTypePropagation) { + private void preprocessConstraints(Set fixedBottom, + Set fixedTop, + Map> superTypePropagation, + Map> subTypePropagation) { for (Constraint constraint: constraints) { // Skip constraints that are just constants @@ -137,7 +136,7 @@ private void preprocessConstraints(Set fixedBottom, if (equality.getFirst() instanceof ConstantSlot) { // Equal to a constant forces a constant AnnotationMirror value = ((ConstantSlot) equality.getFirst()).getValue(); - VariableSlot variable = (VariableSlot) equality.getSecond(); + Slot variable = equality.getSecond(); if (AnnotationUtils.areSame(value, top)) { fixedTop.add(variable); } else { @@ -146,7 +145,7 @@ private void preprocessConstraints(Set fixedBottom, } else if (equality.getSecond() instanceof ConstantSlot) { // Equal to a constant forces a constant AnnotationMirror value = ((ConstantSlot) equality.getSecond()).getValue(); - VariableSlot variable = (VariableSlot) equality.getFirst(); + Slot variable = equality.getFirst(); if (AnnotationUtils.areSame(value, top)) { fixedTop.add(variable); } else { @@ -154,32 +153,32 @@ private void preprocessConstraints(Set fixedBottom, } } else { // Variable equality means values of one propagates to values of the other, for both subtype and supertype - addEntryToMap(superTypePropagation, (VariableSlot) equality.getFirst(), (VariableSlot) equality.getSecond(), constraint); - addEntryToMap(superTypePropagation, (VariableSlot) equality.getSecond(), (VariableSlot) equality.getFirst(), constraint); - addEntryToMap(subTypePropagation, (VariableSlot) equality.getFirst(), (VariableSlot) equality.getSecond(), constraint); - addEntryToMap(subTypePropagation, (VariableSlot) equality.getSecond(), (VariableSlot) equality.getFirst(), constraint); + addEntryToMap(superTypePropagation, equality.getFirst(), equality.getSecond(), constraint); + addEntryToMap(superTypePropagation, equality.getSecond(), equality.getFirst(), constraint); + addEntryToMap(subTypePropagation, equality.getFirst(), equality.getSecond(), constraint); + addEntryToMap(subTypePropagation, equality.getSecond(), equality.getFirst(), constraint); } } else if (constraint instanceof SubtypeConstraint) { SubtypeConstraint subtype = (SubtypeConstraint) constraint; if (subtype.getSubtype() instanceof ConstantSlot) { // If top is a subtype of a variable, that variable is top AnnotationMirror value = ((ConstantSlot) subtype.getSubtype()).getValue(); - VariableSlot variable = (VariableSlot) subtype.getSupertype(); + Slot variable = subtype.getSupertype(); if (AnnotationUtils.areSame(value, top)) { fixedTop.add(variable); } } else if (subtype.getSupertype() instanceof ConstantSlot) { // If a variable is a subtype of bottom, that variable is bottom AnnotationMirror value = ((ConstantSlot) subtype.getSupertype()).getValue(); - VariableSlot variable = (VariableSlot) subtype.getSubtype(); + Slot variable = subtype.getSubtype(); if (AnnotationUtils.areSame(value, bottom)) { fixedBottom.add(variable); } } else { // If the RHS is top, the LHS must be top - addEntryToMap(superTypePropagation, (VariableSlot) subtype.getSubtype(), (VariableSlot) subtype.getSupertype(), constraint); + addEntryToMap(superTypePropagation, subtype.getSubtype(), subtype.getSupertype(), constraint); // If the LHS is bottom, the RHS must be bottom - addEntryToMap(subTypePropagation, (VariableSlot) subtype.getSupertype(), (VariableSlot) subtype.getSubtype(), constraint); + addEntryToMap(subTypePropagation, subtype.getSupertype(), subtype.getSubtype(), constraint); } } else if (constraint instanceof ExistentialConstraint) { InferenceMain.getInstance().logger.warning("PropagationSolver: Existential constraint found. Inferred annotations may not type check "); @@ -197,13 +196,12 @@ private void preprocessConstraints(Set fixedBottom, * @return */ private InferenceResult mergeToResult( - Set fixedBottom, Set fixedTop, - Set inferredTop, Set inferredBottom) { + Set fixedBottom, Set fixedTop, + Set inferredTop, Set inferredBottom) { Map solutions = new HashMap(); for (Slot slot : slots) { if (slot.isVariable()) { - VariableSlot vslot = (VariableSlot) slot; AnnotationMirror result; if (fixedBottom.contains(slot)) { result = bottom; @@ -217,7 +215,7 @@ private InferenceResult mergeToResult( result = defaultValue; } if (result != defaultValue) { - solutions.put(vslot.getId(), result); + solutions.put(slot.getId(), result); } } } @@ -234,18 +232,18 @@ private InferenceResult mergeToResult( * * @return All values that were fixed flooded/propagated to. */ - private Set propagateValues(Set fixed, - Map> typePropagation) { + private Set propagateValues(Set fixed, + Map> typePropagation) { - Set results = new HashSet(); + Set results = new HashSet(); - Set worklist = new HashSet(fixed); + Set worklist = new HashSet(fixed); while (!worklist.isEmpty()) { - VariableSlot variable = worklist.iterator().next(); + Slot variable = worklist.iterator().next(); worklist.remove(variable); if (typePropagation.containsKey(variable)) { - List inferred = typePropagation.get(variable); - List inferredVars = new ArrayList(); + List inferred = typePropagation.get(variable); + List inferredVars = new ArrayList(); inferredVars.addAll(inferred); inferredVars.removeAll(results); results.addAll(inferredVars); @@ -265,8 +263,8 @@ private boolean checkContainsVariable(Constraint constraint) { return containsVariable; } - void addEntryToMap(Map> entries, VariableSlot key, VariableSlot value, Constraint constraint) { - List valueList; + void addEntryToMap(Map> entries, Slot key, Slot value, Constraint constraint) { + List valueList; if (entries.get(key) == null) { valueList = new ArrayList<>(); entries.put(key, valueList); diff --git a/src/checkers/inference/solver/backend/Solver.java b/src/checkers/inference/solver/backend/Solver.java index 39c538d5e..3eb317f38 100644 --- a/src/checkers/inference/solver/backend/Solver.java +++ b/src/checkers/inference/solver/backend/Solver.java @@ -113,7 +113,7 @@ public Solver(SolverEnvironment solverEnvironment, Collection slots, protected void collectVarSlots(Constraint constraint) { for (Slot slot : constraint.getSlots()) { if (!(slot instanceof ConstantSlot)) { - this.varSlotIds.add(((VariableSlot) slot).getId()); + this.varSlotIds.add(slot.getId()); } } } diff --git a/src/checkers/inference/solver/backend/encoder/ArithmeticConstraintEncoder.java b/src/checkers/inference/solver/backend/encoder/ArithmeticConstraintEncoder.java index f4307d395..3e4474643 100644 --- a/src/checkers/inference/solver/backend/encoder/ArithmeticConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/encoder/ArithmeticConstraintEncoder.java @@ -3,6 +3,7 @@ import checkers.inference.model.ArithmeticConstraint.ArithmeticOperationKind; import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.ConstantSlot; +import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; /** @@ -15,13 +16,13 @@ */ public interface ArithmeticConstraintEncoder { ConstraintEncodingT encodeVariable_Variable(ArithmeticOperationKind operation, - VariableSlot leftOperand, VariableSlot rightOperand, ArithmeticVariableSlot result); + Slot leftOperand, Slot rightOperand, ArithmeticVariableSlot result); ConstraintEncodingT encodeVariable_Constant(ArithmeticOperationKind operation, - VariableSlot leftOperand, ConstantSlot rightOperand, ArithmeticVariableSlot result); + Slot leftOperand, ConstantSlot rightOperand, ArithmeticVariableSlot result); ConstraintEncodingT encodeConstant_Variable(ArithmeticOperationKind operation, - ConstantSlot leftOperand, VariableSlot rightOperand, ArithmeticVariableSlot result); + ConstantSlot leftOperand, Slot rightOperand, ArithmeticVariableSlot result); ConstraintEncodingT encodeConstant_Constant(ArithmeticOperationKind operation, ConstantSlot leftOperand, ConstantSlot rightOperand, ArithmeticVariableSlot result); diff --git a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java index 5cb031b97..3d697a593 100644 --- a/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java +++ b/src/checkers/inference/solver/backend/encoder/ConstraintEncoderCoordinator.java @@ -8,7 +8,6 @@ import checkers.inference.model.ExistentialConstraint; import checkers.inference.model.ImplicationConstraint; import checkers.inference.model.PreferenceConstraint; -import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.binary.BinaryConstraintEncoder; import checkers.inference.solver.backend.encoder.combine.CombineConstraintEncoder; import checkers.inference.solver.backend.encoder.existential.ExistentialConstraintEncoder; @@ -38,14 +37,14 @@ public static ConstraintEncodingT dispatch(BinaryConstrain BinaryConstraintEncoder encoder) { switch (SlotSlotCombo.valueOf(constraint.getFirst(), constraint.getSecond())) { case VARIABLE_VARIABLE: - return encoder.encodeVariable_Variable((VariableSlot) constraint.getFirst(), - (VariableSlot) constraint.getSecond()); + return encoder.encodeVariable_Variable(constraint.getFirst(), + constraint.getSecond()); case VARIABLE_CONSTANT: - return encoder.encodeVariable_Constant((VariableSlot) constraint.getFirst(), + return encoder.encodeVariable_Constant(constraint.getFirst(), (ConstantSlot) constraint.getSecond()); case CONSTANT_VARIABLE: return encoder.encodeConstant_Variable((ConstantSlot) constraint.getFirst(), - (VariableSlot) constraint.getSecond()); + constraint.getSecond()); case CONSTANT_CONSTANT: throw new BugInCF("Attempting to encode a constant-constant combination " + "for a binary constraint. This should be normalized to " @@ -59,21 +58,21 @@ public static ConstraintEncodingT dispatch(CombineConstrai CombineConstraintEncoder encoder) { switch (SlotSlotCombo.valueOf(constraint.getTarget(), constraint.getDeclared())) { case VARIABLE_VARIABLE: - return encoder.encodeVariable_Variable((VariableSlot) constraint.getTarget(), - (VariableSlot) constraint.getDeclared(), - (VariableSlot) constraint.getResult()); + return encoder.encodeVariable_Variable(constraint.getTarget(), + constraint.getDeclared(), + constraint.getResult()); case VARIABLE_CONSTANT: - return encoder.encodeVariable_Constant((VariableSlot) constraint.getTarget(), + return encoder.encodeVariable_Constant(constraint.getTarget(), (ConstantSlot) constraint.getDeclared(), - (VariableSlot) constraint.getResult()); + constraint.getResult()); case CONSTANT_VARIABLE: return encoder.encodeConstant_Variable((ConstantSlot) constraint.getTarget(), - (VariableSlot) constraint.getDeclared(), - (VariableSlot) constraint.getResult()); + constraint.getDeclared(), + constraint.getResult()); case CONSTANT_CONSTANT: return encoder.encodeConstant_Constant((ConstantSlot) constraint.getTarget(), (ConstantSlot) constraint.getDeclared(), - (VariableSlot) constraint.getResult()); + constraint.getResult()); default: throw new BugInCF("Unsupported SlotSlotCombo enum."); } @@ -85,16 +84,16 @@ public static ConstraintEncodingT dispatch( switch (SlotSlotCombo.valueOf(constraint.getLeftOperand(), constraint.getRightOperand())) { case VARIABLE_VARIABLE: return encoder.encodeVariable_Variable(constraint.getOperation(), - (VariableSlot) constraint.getLeftOperand(), - (VariableSlot) constraint.getRightOperand(), constraint.getResult()); + constraint.getLeftOperand(), + constraint.getRightOperand(), constraint.getResult()); case VARIABLE_CONSTANT: return encoder.encodeVariable_Constant(constraint.getOperation(), - (VariableSlot) constraint.getLeftOperand(), + constraint.getLeftOperand(), (ConstantSlot) constraint.getRightOperand(), constraint.getResult()); case CONSTANT_VARIABLE: return encoder.encodeConstant_Variable(constraint.getOperation(), (ConstantSlot) constraint.getLeftOperand(), - (VariableSlot) constraint.getRightOperand(), constraint.getResult()); + constraint.getRightOperand(), constraint.getResult()); case CONSTANT_CONSTANT: return encoder.encodeConstant_Constant(constraint.getOperation(), (ConstantSlot) constraint.getLeftOperand(), diff --git a/src/checkers/inference/solver/backend/encoder/SlotSlotCombo.java b/src/checkers/inference/solver/backend/encoder/SlotSlotCombo.java index 87688a192..c69aa169e 100644 --- a/src/checkers/inference/solver/backend/encoder/SlotSlotCombo.java +++ b/src/checkers/inference/solver/backend/encoder/SlotSlotCombo.java @@ -16,8 +16,8 @@ *

* But the {@link Slot.Kind} that's needed here is coarser-grained than its original definition: * Only knowing if a {@code Slot} is variable or constant is enough in solver encoding. Because solver - * treats every {@link checkers.inference.model.VariableSlot} and its subclasses essentially as having - * unknown value that is to be inferred and only the {@link checkers.inference.model.VariableSlot#id} is + * treats every {@link checkers.inference.model.Slot} and its subclasses essentially as having + * unknown value that is to be inferred and only the {@link checkers.inference.model.Slot#id} is * interesting; Solver treats {@link checkers.inference.model.ConstantSlot} as having a real qualifier * that no inference is needed. * diff --git a/src/checkers/inference/solver/backend/encoder/binary/BinaryConstraintEncoder.java b/src/checkers/inference/solver/backend/encoder/binary/BinaryConstraintEncoder.java index e339893c7..2e2371738 100644 --- a/src/checkers/inference/solver/backend/encoder/binary/BinaryConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/encoder/binary/BinaryConstraintEncoder.java @@ -1,7 +1,7 @@ package checkers.inference.solver.backend.encoder.binary; import checkers.inference.model.ConstantSlot; -import checkers.inference.model.VariableSlot; +import checkers.inference.model.Slot; /** * Interface that defines operations to encode a {@link checkers.inference.model.BinaryConstraint}. @@ -15,9 +15,9 @@ */ public interface BinaryConstraintEncoder { - ConstraintEncodingT encodeVariable_Variable(VariableSlot fst, VariableSlot snd); + ConstraintEncodingT encodeVariable_Variable(Slot fst, Slot snd); - ConstraintEncodingT encodeVariable_Constant(VariableSlot fst, ConstantSlot snd); + ConstraintEncodingT encodeVariable_Constant(Slot fst, ConstantSlot snd); - ConstraintEncodingT encodeConstant_Variable(ConstantSlot fst, VariableSlot snd); + ConstraintEncodingT encodeConstant_Variable(ConstantSlot fst, Slot snd); } diff --git a/src/checkers/inference/solver/backend/encoder/combine/CombineConstraintEncoder.java b/src/checkers/inference/solver/backend/encoder/combine/CombineConstraintEncoder.java index cbbe8cc56..6f6b3030f 100644 --- a/src/checkers/inference/solver/backend/encoder/combine/CombineConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/encoder/combine/CombineConstraintEncoder.java @@ -1,7 +1,7 @@ package checkers.inference.solver.backend.encoder.combine; import checkers.inference.model.ConstantSlot; -import checkers.inference.model.VariableSlot; +import checkers.inference.model.Slot; /** * Interface that defines operations to encode a {@link checkers.inference.model.CombineConstraint}. It has four methods @@ -9,8 +9,8 @@ * declared} slots. * *

- * {@code result} is always {@link checkers.inference.model.CombVariableSlot}, which is essentially {@link VariableSlot}, - * whose {@link VariableSlot#id} is the only interesting knowledge in encoding phase. Therefore there don't exist + * {@code result} is always {@link checkers.inference.model.CombVariableSlot}, which is essentially {@link Slot}, + * whose {@link Slot#id} is the only interesting knowledge in encoding phase. Therefore there don't exist * methods in which {@code result} is {@link ConstantSlot}. * * @see checkers.inference.model.CombineConstraint @@ -18,11 +18,11 @@ */ public interface CombineConstraintEncoder { - ConstraintEncodingT encodeVariable_Variable(VariableSlot target, VariableSlot declared, VariableSlot result); + ConstraintEncodingT encodeVariable_Variable(Slot target, Slot declared, Slot result); - ConstraintEncodingT encodeVariable_Constant(VariableSlot target, ConstantSlot declared, VariableSlot result); + ConstraintEncodingT encodeVariable_Constant(Slot target, ConstantSlot declared, Slot result); - ConstraintEncodingT encodeConstant_Variable(ConstantSlot target, VariableSlot declared, VariableSlot result); + ConstraintEncodingT encodeConstant_Variable(ConstantSlot target, Slot declared, Slot result); - ConstraintEncodingT encodeConstant_Constant(ConstantSlot target, ConstantSlot declared, VariableSlot result); + ConstraintEncodingT encodeConstant_Constant(ConstantSlot target, ConstantSlot declared, Slot result); } diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java index 68a127f22..24b8c1859 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLComparableConstraintEncoder.java @@ -1,7 +1,7 @@ package checkers.inference.solver.backend.logiql.encoder; import checkers.inference.model.ConstantSlot; -import checkers.inference.model.VariableSlot; +import checkers.inference.model.Slot; import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.NameUtils; @@ -13,19 +13,19 @@ public LogiQLComparableConstraintEncoder(Lattice lattice) { } @Override - public String encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { + public String encodeVariable_Variable(Slot fst, Slot snd) { String logiQLData = "+comparableConstraint(v1, v2), +variable(v1), +hasvariableName[v1] = " + fst.getId() + ", +variable(v2), +hasvariableName[v2] = " + snd.getId() + ".\n"; return logiQLData; } @Override - public String encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { + public String encodeVariable_Constant(Slot fst, ConstantSlot snd) { return encodeConstant_Variable(snd, fst); } @Override - public String encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { + public String encodeConstant_Variable(ConstantSlot fst, Slot snd) { String constantName = NameUtils.getSimpleName(fst.getValue()); int variableId = snd.getId(); String logiQLData = "+equalityConstraintContainsConstant(c, v), +constant(c), +hasconstantName[c] = \"" diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLEqualityConstraintEncoder.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLEqualityConstraintEncoder.java index ba4a9653f..d683adc97 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLEqualityConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLEqualityConstraintEncoder.java @@ -1,7 +1,7 @@ package checkers.inference.solver.backend.logiql.encoder; import checkers.inference.model.ConstantSlot; -import checkers.inference.model.VariableSlot; +import checkers.inference.model.Slot; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.NameUtils; @@ -13,19 +13,19 @@ public LogiQLEqualityConstraintEncoder(Lattice lattice) { } @Override - public String encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { + public String encodeVariable_Variable(Slot fst, Slot snd) { String logiQLData = "+equalityConstraint(v1, v2), +variable(v1), +hasvariableName[v1] = " + fst.getId() + ", +variable(v2), +hasvariableName[v2] = " + snd.getId() + ".\n"; return logiQLData; } @Override - public String encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { + public String encodeVariable_Constant(Slot fst, ConstantSlot snd) { return encodeConstant_Variable(snd, fst); } @Override - public String encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { + public String encodeConstant_Variable(ConstantSlot fst, Slot snd) { String constantName = NameUtils.getSimpleName(fst.getValue()); int variableId = snd.getId(); String logiQLData = "+equalityConstraintContainsConstant(c, v), +constant(c), +hasconstantName[c] = \"" diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLInequalityConstraintEncoder.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLInequalityConstraintEncoder.java index 412539fa7..31463893f 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLInequalityConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLInequalityConstraintEncoder.java @@ -1,7 +1,7 @@ package checkers.inference.solver.backend.logiql.encoder; import checkers.inference.model.ConstantSlot; -import checkers.inference.model.VariableSlot; +import checkers.inference.model.Slot; import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.NameUtils; @@ -13,19 +13,19 @@ public LogiQLInequalityConstraintEncoder(Lattice lattice) { } @Override - public String encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { + public String encodeVariable_Variable(Slot fst, Slot snd) { String logiQLData = "+inequalityConstraint(v1, v2), +variable(v1), +hasvariableName[v1] = " + fst.getId() + ", +variable(v2), +hasvariableName[v2] = " + snd.getId() + ".\n"; return logiQLData; } @Override - public String encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { + public String encodeVariable_Constant(Slot fst, ConstantSlot snd) { return encodeConstant_Variable(snd, fst); } @Override - public String encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { + public String encodeConstant_Variable(ConstantSlot fst, Slot snd) { String constantName = NameUtils.getSimpleName(fst.getValue()); int variableId = snd.getId(); String logiQLData = "+inequalityConstraintContainsConstant(c, v), +constant(c), +hasconstantName[c] = \"" diff --git a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLSubtypeConstraintEncoder.java b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLSubtypeConstraintEncoder.java index 5ebd3b4b2..48d2db5c7 100644 --- a/src/checkers/inference/solver/backend/logiql/encoder/LogiQLSubtypeConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/logiql/encoder/LogiQLSubtypeConstraintEncoder.java @@ -1,7 +1,7 @@ package checkers.inference.solver.backend.logiql.encoder; import checkers.inference.model.ConstantSlot; -import checkers.inference.model.VariableSlot; +import checkers.inference.model.Slot; import checkers.inference.solver.backend.encoder.binary.SubtypeConstraintEncoder; import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.NameUtils; @@ -13,7 +13,7 @@ public LogiQLSubtypeConstraintEncoder(Lattice lattice) { } @Override - public String encodeVariable_Variable(VariableSlot subtype, VariableSlot supertype) { + public String encodeVariable_Variable(Slot subtype, Slot supertype) { String logiQLData = "+subtypeConstraint(v1, v2), +variable(v1), +hasvariableName[v1] = " + subtype.getId() + ", +variable(v2), +hasvariableName[v2] = " + supertype.getId() + ".\n"; @@ -21,7 +21,7 @@ public String encodeVariable_Variable(VariableSlot subtype, VariableSlot superty } @Override - public String encodeVariable_Constant(VariableSlot subtype, ConstantSlot supertype) { + public String encodeVariable_Constant(Slot subtype, ConstantSlot supertype) { String supertypeName = NameUtils.getSimpleName(supertype.getValue()); int subtypeId = subtype.getId(); String logiQLData = "+subtypeConstraintRightConstant(v, c), +variable(v), +hasvariableName[v] = " @@ -30,7 +30,7 @@ public String encodeVariable_Constant(VariableSlot subtype, ConstantSlot superty } @Override - public String encodeConstant_Variable(ConstantSlot subtype, VariableSlot supertype) { + public String encodeConstant_Variable(ConstantSlot subtype, Slot supertype) { String subtypeName = NameUtils.getSimpleName(subtype.getValue()); int supertypeId = supertype.getId(); String logiQLData = "+subtypeConstraintLeftConstant(c, v), +constant(c), +hasconstantName[c] = \"" diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java index a9cb02d9a..801cfc95a 100644 --- a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATComparableConstraintEncoder.java @@ -1,7 +1,7 @@ package checkers.inference.solver.backend.maxsat.encoder; import checkers.inference.model.ConstantSlot; -import checkers.inference.model.VariableSlot; +import checkers.inference.model.Slot; import checkers.inference.solver.backend.encoder.binary.ComparableConstraintEncoder; import checkers.inference.solver.backend.maxsat.MathUtils; import checkers.inference.solver.backend.maxsat.VectorUtils; @@ -20,7 +20,7 @@ public MaxSATComparableConstraintEncoder(Lattice lattice, Map !b which is the same as (!a v !b) & (b v a) List list = new ArrayList(); for (AnnotationMirror type : lattice.allTypes) { @@ -39,7 +39,7 @@ public VecInt[] encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { } @Override - public VecInt[] encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { + public VecInt[] encodeVariable_Constant(Slot fst, ConstantSlot snd) { if (lattice.incomparableType.keySet().contains(snd.getValue())) { List resultList = new ArrayList<>(); for (AnnotationMirror incomparable : lattice.incomparableType.get(snd.getValue())) { @@ -56,7 +56,7 @@ public VecInt[] encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { } @Override - public VecInt[] encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { + public VecInt[] encodeConstant_Variable(ConstantSlot fst, Slot snd) { return encodeVariable_Constant(snd, fst); } } diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATEqualityConstraintEncoder.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATEqualityConstraintEncoder.java index d42c2a188..55f958460 100644 --- a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATEqualityConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATEqualityConstraintEncoder.java @@ -1,7 +1,7 @@ package checkers.inference.solver.backend.maxsat.encoder; import checkers.inference.model.ConstantSlot; -import checkers.inference.model.VariableSlot; +import checkers.inference.model.Slot; import checkers.inference.solver.backend.encoder.binary.EqualityConstraintEncoder; import checkers.inference.solver.backend.maxsat.MathUtils; import checkers.inference.solver.backend.maxsat.VectorUtils; @@ -18,7 +18,7 @@ public MaxSATEqualityConstraintEncoder(Lattice lattice, Map b which is the same as (!a v b) & (!b v a) VecInt[] result = new VecInt[lattice.numTypes * 2]; int i = 0; @@ -36,12 +36,12 @@ public VecInt[] encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { } @Override - public VecInt[] encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { + public VecInt[] encodeVariable_Constant(Slot fst, ConstantSlot snd) { return encodeConstant_Variable(snd, fst); } @Override - public VecInt[] encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { + public VecInt[] encodeConstant_Variable(ConstantSlot fst, Slot snd) { if (lattice.allTypes.contains(fst.getValue())) { return VectorUtils.asVecArray( MathUtils.mapIdToMatrixEntry(snd.getId(), typeToInt.get(fst.getValue()), lattice)); diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATInequalityConstraintEncoder.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATInequalityConstraintEncoder.java index fb850d54c..275ad4ad4 100644 --- a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATInequalityConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATInequalityConstraintEncoder.java @@ -1,7 +1,7 @@ package checkers.inference.solver.backend.maxsat.encoder; import checkers.inference.model.ConstantSlot; -import checkers.inference.model.VariableSlot; +import checkers.inference.model.Slot; import checkers.inference.solver.backend.encoder.binary.InequalityConstraintEncoder; import checkers.inference.solver.backend.maxsat.MathUtils; import checkers.inference.solver.backend.maxsat.VectorUtils; @@ -18,7 +18,7 @@ public MaxSATInequalityConstraintEncoder(Lattice lattice, Map !b which is the same as (!a v !b) & (b v a) VecInt[] result = new VecInt[lattice.numTypes * 2]; int i = 0; @@ -36,12 +36,12 @@ public VecInt[] encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { } @Override - public VecInt[] encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { + public VecInt[] encodeVariable_Constant(Slot fst, ConstantSlot snd) { return encodeConstant_Variable(snd, fst); } @Override - public VecInt[] encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { + public VecInt[] encodeConstant_Variable(ConstantSlot fst, Slot snd) { if (lattice.allTypes.contains(fst.getValue())) { return VectorUtils.asVecArray( -MathUtils.mapIdToMatrixEntry(snd.getId(), typeToInt.get(fst.getValue()), lattice)); diff --git a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATPreferenceConstraintEncoder.java b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATPreferenceConstraintEncoder.java index 7eb065957..a573e2aba 100644 --- a/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATPreferenceConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/maxsat/encoder/MaxSATPreferenceConstraintEncoder.java @@ -2,6 +2,7 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.PreferenceConstraint; +import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.preference.PreferenceConstraintEncoder; import checkers.inference.solver.backend.maxsat.MathUtils; @@ -22,7 +23,7 @@ public MaxSATPreferenceConstraintEncoder(Lattice lattice, Map mustNotBe, VariableSlot vSlot, ConstantSlot cSlot) { + protected VecInt[] getMustNotBe(Set mustNotBe, Slot vSlot, ConstantSlot cSlot) { List resultList = new ArrayList(); @@ -49,7 +49,7 @@ protected VecInt[] getMustNotBe(Set mustNotBe, VariableSlot vS return emptyValue; } - protected int[] getMaybe(AnnotationMirror type, VariableSlot knownType, VariableSlot unknownType, + protected int[] getMaybe(AnnotationMirror type, Slot knownType, Slot unknownType, Collection maybeSet) { int[] maybeArray = new int[maybeSet.size() + 1]; int i = 1; @@ -62,7 +62,7 @@ protected int[] getMaybe(AnnotationMirror type, VariableSlot knownType, Variable } @Override - public VecInt[] encodeVariable_Variable(VariableSlot subtype, VariableSlot supertype) { + public VecInt[] encodeVariable_Variable(Slot subtype, Slot supertype) { // if subtype is top, then supertype is top. // if supertype is bottom, then subtype is bottom. VecInt supertypeOfTop = VectorUtils.asVec( @@ -93,7 +93,7 @@ public VecInt[] encodeVariable_Variable(VariableSlot subtype, VariableSlot super } @Override - public VecInt[] encodeVariable_Constant(VariableSlot subtype, ConstantSlot supertype) { + public VecInt[] encodeVariable_Constant(Slot subtype, ConstantSlot supertype) { final Set mustNotBe = new HashSet<>(); if (AnnotationUtils.areSame(supertype.getValue(), lattice.bottom)) { return VectorUtils.asVecArray( @@ -110,7 +110,7 @@ public VecInt[] encodeVariable_Constant(VariableSlot subtype, ConstantSlot super } @Override - public VecInt[] encodeConstant_Variable(ConstantSlot subtype, VariableSlot supertype) { + public VecInt[] encodeConstant_Variable(ConstantSlot subtype, Slot supertype) { final Set mustNotBe = new HashSet<>(); if (AnnotationUtils.areSame(subtype.getValue(), lattice.top)) { return VectorUtils.asVecArray( diff --git a/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java b/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java index e3e5a8a72..fe3e25df6 100644 --- a/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java +++ b/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java @@ -120,7 +120,12 @@ public BitVecExpr serializeConstantSlot(ConstantSlot slot) { protected ConstraintEncoderFactory createConstraintEncoderFactory() { return new Z3BitVectorConstraintEncoderFactory(lattice, context, this); } - + + @Override + public BitVecExpr serialize(Slot slot) { + return serializeVarSlot(slot); + } + @Override public BitVecExpr serialize(VariableSlot slot) { return serializeVarSlot(slot); diff --git a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorEqualityConstraintEncoder.java b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorEqualityConstraintEncoder.java index 6be615ccd..1af849483 100644 --- a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorEqualityConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorEqualityConstraintEncoder.java @@ -2,7 +2,6 @@ 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.backend.z3.Z3BitVectorFormatTranslator; import checkers.inference.solver.frontend.Lattice; @@ -24,17 +23,17 @@ protected BoolExpr encode(Slot fst, Slot snd) { } @Override - public BoolExpr encodeVariable_Variable(VariableSlot fst, VariableSlot snd) { + public BoolExpr encodeVariable_Variable(Slot fst, Slot snd) { return encode(fst, snd); } @Override - public BoolExpr encodeVariable_Constant(VariableSlot fst, ConstantSlot snd) { + public BoolExpr encodeVariable_Constant(Slot fst, ConstantSlot snd) { return encode(fst, snd); } @Override - public BoolExpr encodeConstant_Variable(ConstantSlot fst, VariableSlot snd) { + public BoolExpr encodeConstant_Variable(ConstantSlot fst, Slot snd) { return encode(fst, snd); } } diff --git a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorPreferenceConstraintEncoder.java b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorPreferenceConstraintEncoder.java index b2ed3245c..9ff929897 100644 --- a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorPreferenceConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorPreferenceConstraintEncoder.java @@ -2,6 +2,7 @@ import checkers.inference.model.ConstantSlot; import checkers.inference.model.PreferenceConstraint; +import checkers.inference.model.Slot; import checkers.inference.model.VariableSlot; import checkers.inference.solver.backend.encoder.preference.PreferenceConstraintEncoder; import checkers.inference.solver.backend.z3.Z3BitVectorFormatTranslator; @@ -23,7 +24,7 @@ public Z3BitVectorPreferenceConstraintEncoder(Lattice lattice, Context context, */ @Override public BoolExpr encode(PreferenceConstraint constraint) { - VariableSlot variableSlot = constraint.getVariable(); + Slot variableSlot = constraint.getVariable(); ConstantSlot constantSlot = constraint.getGoal(); BitVecExpr varBV = z3BitVectorFormatTranslator.serializeVarSlot(variableSlot); diff --git a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorSubtypeConstraintEncoder.java b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorSubtypeConstraintEncoder.java index 53e605a7d..bb1c4e3a0 100644 --- a/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorSubtypeConstraintEncoder.java +++ b/src/checkers/inference/solver/backend/z3/encoder/Z3BitVectorSubtypeConstraintEncoder.java @@ -2,7 +2,6 @@ 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.backend.z3.Z3BitVectorFormatTranslator; import checkers.inference.solver.frontend.Lattice; @@ -42,17 +41,17 @@ protected BoolExpr encode(Slot subtype, Slot supertype) { } @Override - public BoolExpr encodeVariable_Variable(VariableSlot subtype, VariableSlot supertype) { + public BoolExpr encodeVariable_Variable(Slot subtype, Slot supertype) { return encode(subtype, supertype); } @Override - public BoolExpr encodeVariable_Constant(VariableSlot subtype, ConstantSlot supertype) { + public BoolExpr encodeVariable_Constant(Slot subtype, ConstantSlot supertype) { return encode(subtype, supertype); } @Override - public BoolExpr encodeConstant_Variable(ConstantSlot subtype, VariableSlot supertype) { + public BoolExpr encodeConstant_Variable(ConstantSlot subtype, Slot supertype) { return encode(subtype, supertype); } } diff --git a/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java b/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java new file mode 100644 index 000000000..676aa8564 --- /dev/null +++ b/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java @@ -0,0 +1,91 @@ +package checkers.inference.solver.backend.z3smt; + +import checkers.inference.model.CombVariableSlot; +import checkers.inference.model.ConstantSlot; +import checkers.inference.model.ExistentialVariableSlot; +import checkers.inference.model.LubVariableSlot; +import checkers.inference.model.RefinementVariableSlot; +import checkers.inference.model.Slot; +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; + +// AbstractFormatTranslator +public abstract class Z3SmtFormatTranslator + extends AbstractFormatTranslator { + + protected Context ctx; + + /** Cache of all serialized slots, keyed on slot ID. */ + protected final Map serializedSlots; + + public Z3SmtFormatTranslator(Lattice lattice) { + super(lattice); + serializedSlots = new HashMap<>(); + } + + public final void init(Context ctx) { + this.ctx = ctx; + finishInitializingEncoders(); + } + + protected abstract SlotEncodingT serializeVarSlot(Slot slot); + + protected abstract SlotEncodingT serializeConstantSlot(ConstantSlot slot); + + @Override + public SlotEncodingT serialize(Slot slot) { + return serializeVarSlot(slot); + } + + @Override + public SlotEncodingT serialize(VariableSlot slot) { + return serializeVarSlot(slot); + } + + @Override + public SlotEncodingT serialize(ConstantSlot slot) { + return serializeConstantSlot(slot); + } + + @Override + public SlotEncodingT serialize(ExistentialVariableSlot slot) { + return serializeVarSlot(slot); + } + + @Override + public SlotEncodingT serialize(RefinementVariableSlot slot) { + return serializeVarSlot(slot); + } + + @Override + public SlotEncodingT serialize(CombVariableSlot slot) { + return serializeVarSlot(slot); + } + + @Override + public SlotEncodingT serialize(LubVariableSlot slot) { + return serializeVarSlot(slot); + } + + /** + * Subclasses can override this method to perform pre-analysis of slots for encoding + * optimization + */ + public void preAnalyzeSlots(Collection slots) {} + + public abstract BoolExpr encodeSlotWellformnessConstraint(Slot slot); + + public abstract BoolExpr encodeSlotPreferenceConstraint(Slot slot); + + public abstract Map decodeSolution( + List model, ProcessingEnvironment processingEnv); +} diff --git a/src/checkers/inference/solver/backend/z3smt/Z3SmtSolver.java b/src/checkers/inference/solver/backend/z3smt/Z3SmtSolver.java new file mode 100644 index 000000000..e897dfb54 --- /dev/null +++ b/src/checkers/inference/solver/backend/z3smt/Z3SmtSolver.java @@ -0,0 +1,493 @@ +package checkers.inference.solver.backend.z3smt; + +import checkers.inference.model.ArithmeticConstraint; +import checkers.inference.model.ArithmeticConstraint.ArithmeticOperationKind; +import checkers.inference.model.CombineConstraint; +import checkers.inference.model.ComparableConstraint; +import checkers.inference.model.Constraint; +import checkers.inference.model.EqualityConstraint; +import checkers.inference.model.ExistentialConstraint; +import checkers.inference.model.ImplicationConstraint; +import checkers.inference.model.InequalityConstraint; +import checkers.inference.model.PreferenceConstraint; +import checkers.inference.model.Slot; +import checkers.inference.model.SubtypeConstraint; +import checkers.inference.model.VariableSlot; +import checkers.inference.model.serialization.ToStringSerializer; +import checkers.inference.solver.backend.Solver; +import checkers.inference.solver.backend.z3smt.Z3SmtFormatTranslator; +import checkers.inference.solver.frontend.Lattice; +import checkers.inference.solver.util.ExternalSolverUtils; +import checkers.inference.solver.util.FileUtils; +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 java.io.BufferedReader; +import java.io.File; +import java.io.IOException; +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import javax.lang.model.element.AnnotationMirror; +import org.checkerframework.javacutil.BugInCF; + +public class Z3SmtSolver + extends Solver> { + + public enum Z3SolverEngineArg implements SolverArg { + /** option to use optimizing mode or not */ + optimizingMode + } + + protected final Context ctx; + protected com.microsoft.z3.Optimize solver; + protected StringBuffer smtFileContents; + + protected static final String z3Program = "z3"; + protected boolean optimizingMode; + protected boolean getUnsatCore; + + // used in non-optimizing mode to find unsat constraints + protected final Map serializedConstraints = new HashMap<>(); + protected final List unsatConstraintIDs = new ArrayList<>(); + + // file is written at projectRootFolder/constraints.smt + protected static final String pathToProject = + new File(new File("").getAbsolutePath()).toString(); + protected static final String constraintsFile = pathToProject + "/z3Constraints.smt"; + protected static final String constraintsUnsatCoreFile = + pathToProject + "/z3ConstraintsUnsatCore.smt"; + protected static final String constraintsStatsFile = pathToProject + "/z3ConstraintsGlob.smt"; + + // timing statistics variables + protected long serializationStart; + protected long serializationEnd; + protected long solvingStart; + protected long solvingEnd; + + public Z3SmtSolver( + SolverEnvironment solverEnvironment, + Collection slots, + Collection constraints, + Z3SmtFormatTranslator z3SmtFormatTranslator, + Lattice lattice) { + super(solverEnvironment, slots, constraints, z3SmtFormatTranslator, lattice); + + Map z3Args = new HashMap<>(); + + // add timeout arg + if (withTimeout()) { + z3Args.put("timeout", Integer.toString(timeout())); + } + // creating solver + ctx = new Context(z3Args); + + z3SmtFormatTranslator.init(ctx); + } + + protected boolean withTimeout() { + return false; + } + + protected int timeout() { + return 2 * 60 * 1000; // timeout of 2 mins by default + } + + // Main entry point + @Override + public Map solve() { + // serialize based on user choice of running in optimizing or non-optimizing mode + optimizingMode = solverEnvironment.getBoolArg(Z3SolverEngineArg.optimizingMode); + getUnsatCore = false; + + if (optimizingMode) { + System.err.println("Encoding for optimizing mode"); + } else { + System.err.println("Encoding for non-optimizing mode"); + } + + serializeSMTFileContents(); + + solvingStart = System.currentTimeMillis(); + // in Units, if the status is SAT then there must be output in the model + List results = runZ3Solver(); + solvingEnd = System.currentTimeMillis(); + + Statistics.addOrIncrementEntry( + "smt_serialization_time(millisec)", serializationEnd - serializationStart); + Statistics.addOrIncrementEntry("smt_solving_time(millisec)", solvingEnd - solvingStart); + + System.err.println("=== Arithmetic Constraints Printout ==="); + Map arithmeticConstraintCounters = new HashMap<>(); + for (ArithmeticOperationKind kind : ArithmeticOperationKind.values()) { + arithmeticConstraintCounters.put(kind, 0); + } + for (Constraint constraint : constraints) { + if (constraint instanceof ArithmeticConstraint) { + ArithmeticConstraint arithmeticConstraint = (ArithmeticConstraint) constraint; + ArithmeticOperationKind kind = arithmeticConstraint.getOperation(); + arithmeticConstraintCounters.put(kind, arithmeticConstraintCounters.get(kind) + 1); + } + } + for (ArithmeticOperationKind kind : ArithmeticOperationKind.values()) { + System.err.println( + " Made arithmetic " + + kind.getSymbol() + + " constraint: " + + arithmeticConstraintCounters.get(kind)); + } + + if (results == null) { + System.err.println("\n\n!!! The set of constraints is unsatisfiable! !!!"); + return null; + } + + return formatTranslator.decodeSolution( + results, solverEnvironment.processingEnvironment); + } + + @Override + public Collection explainUnsatisfiable() { + optimizingMode = false; + getUnsatCore = true; + + System.err.println("Now encoding for unsat core dump."); + serializeSMTFileContents(); + + solvingStart = System.currentTimeMillis(); + runZ3Solver(); + solvingEnd = System.currentTimeMillis(); + + Statistics.addOrIncrementEntry( + "smt_unsat_serialization_time(millisec)", serializationEnd - serializationStart); + Statistics.addOrIncrementEntry( + "smt_unsat_solving_time(millisec)", solvingEnd - solvingStart); + + List unsatConstraints = new ArrayList<>(); + + for (String constraintID : unsatConstraintIDs) { + Constraint c = serializedConstraints.get(constraintID); + unsatConstraints.add(c); + } + + return unsatConstraints; + } + + private void serializeSMTFileContents() { + // make a fresh solver to contain encodings of the slots + solver = ctx.mkOptimize(); + // make a new buffer to store the serialized smt file contents + smtFileContents = new StringBuffer(); + + // only enable in non-optimizing mode + if (!optimizingMode && getUnsatCore) { + smtFileContents.append("(set-option :produce-unsat-cores true)\n"); + } + + serializationStart = System.currentTimeMillis(); + encodeAllSlots(); + encodeAllConstraints(); + if (optimizingMode) { + encodeAllSoftConstraints(); + } + serializationEnd = System.currentTimeMillis(); + + System.err.println("Encoding constraints done!"); + + smtFileContents.append("(check-sat)\n"); + if (!optimizingMode && getUnsatCore) { + smtFileContents.append("(get-unsat-core)\n"); + } else { + smtFileContents.append("(get-model)\n"); + } + + System.err.println("Writing constraints to file: " + constraintsFile); + + writeConstraintsToSMTFile(); + } + + private void writeConstraintsToSMTFile() { + String fileContents = smtFileContents.toString(); + + if (!getUnsatCore) { + // write the constraints to the file for external solver use + FileUtils.writeFile(new File(constraintsFile), fileContents); + } else { + // write the constraints to the file for external solver use + FileUtils.writeFile(new File(constraintsUnsatCoreFile), fileContents); + } + // write a copy in append mode to stats file for later bulk analysis + FileUtils.appendFile(new File(constraintsStatsFile), fileContents); + } + + protected void encodeAllSlots() { + // preprocess slots + formatTranslator.preAnalyzeSlots(slots); + + // generate slot constraints + for (Slot slot : slots) { + if (slot.isVariable()) { + Slot varSlot = slot; + + BoolExpr wfConstraint = formatTranslator.encodeSlotWellformnessConstraint(varSlot); + + if (!wfConstraint.simplify().isTrue()) { + solver.Assert(wfConstraint); + } + if (optimizingMode) { + encodeSlotPreferenceConstraint(varSlot); + } + } + } + + // solver.toString() also includes "(check-sat)" as the last line, + // remove it + String slotDefinitionsAndConstraints = solver.toString(); + int truncateIndex = slotDefinitionsAndConstraints.lastIndexOf("(check-sat)"); + assert truncateIndex != -1; + + // append slot definitions to overall smt file + smtFileContents.append(slotDefinitionsAndConstraints.substring(0, truncateIndex)); + } + + @Override + protected void encodeAllConstraints() { + int current = 1; + + StringBuffer constraintSmtFileContents = new StringBuffer(); + + for (Constraint constraint : constraints) { + BoolExpr serializedConstraint = constraint.serialize(formatTranslator); + + if (serializedConstraint == null) { + // TODO: Should error abort if unsupported constraint detected. + // Currently warning is a workaround for making ontology + // working, as in some cases existential constraints generated. + // Should investigate on this, and change this to ErrorAbort + // when eliminated unsupported constraints. + System.err.println( + "Unsupported constraint detected! Constraint type: " + + constraint.getClass().getSimpleName()); + continue; + } + + Expr simplifiedConstraint = serializedConstraint.simplify(); + + if (simplifiedConstraint.isTrue()) { + // This only works if the BoolExpr is directly the value Z3True. + // Still a good filter, but doesn't filter enough. + // EG: (and (= false false) (= false false) (= 0 0) (= 0 0) (= 0 0)) + // Skip tautology. + current++; + continue; + } + + if (simplifiedConstraint.isFalse()) { + final ToStringSerializer toStringSerializer = new ToStringSerializer(false); + throw new BugInCF( + "impossible constraint: " + + constraint.serialize(toStringSerializer) + + "\nSerialized:\n" + + serializedConstraint); + } + + String clause = simplifiedConstraint.toString(); + + if (!optimizingMode && getUnsatCore) { + // add assertions with names, for unsat core dump + String constraintName = constraint.getClass().getSimpleName() + current; + + constraintSmtFileContents.append("(assert (! "); + constraintSmtFileContents.append(clause); + constraintSmtFileContents.append(" :named " + constraintName + "))\n"); + + // add constraint to serialized constraints map, so that we can + // retrieve later using the constraint name when outputting the unsat core + serializedConstraints.put(constraintName, constraint); + } else { + constraintSmtFileContents.append("(assert "); + constraintSmtFileContents.append(clause); + constraintSmtFileContents.append(")\n"); + } + + current++; + } + + String constraintSmt = constraintSmtFileContents.toString(); + + smtFileContents.append(constraintSmt); + } + + private void encodeAllSoftConstraints() { + for (Constraint constraint : constraints) { + // Generate a soft constraint for subtype constraint + if (constraint instanceof SubtypeConstraint) { + encodeSoftSubtypeConstraint((SubtypeConstraint) constraint); + } + // Generate soft constraint for comparison constraint + if (constraint instanceof ComparableConstraint) { + encodeSoftComparableConstraint((ComparableConstraint) constraint); + } + // Generate soft constraint for arithmetic constraint + if (constraint instanceof ArithmeticConstraint) { + encodeSoftArithmeticConstraint((ArithmeticConstraint) constraint); + } + // Generate soft constraint for equality constraint + if (constraint instanceof EqualityConstraint) { + encodeSoftEqualityConstraint((EqualityConstraint) constraint); + } + // Generate soft constraint for inequality constraint + if (constraint instanceof InequalityConstraint) { + encodeSoftInequalityConstraint((InequalityConstraint) constraint); + } + // Generate soft constraint for implication constraint + if (constraint instanceof ImplicationConstraint) { + encodeSoftImplicationConstraint((ImplicationConstraint) constraint); + } + // Generate soft constraint for existential constraint + if (constraint instanceof ExistentialConstraint) { + encodeSoftExistentialConstraint((ExistentialConstraint) constraint); + } + // Generate soft constraint for combine constraint + if (constraint instanceof CombineConstraint) { + encodeSoftCombineConstraint((CombineConstraint) constraint); + } + // Generate soft constraint for preference constraint + if (constraint instanceof PreferenceConstraint) { + encodeSoftPreferenceConstraint((PreferenceConstraint) constraint); + } + } + } + + protected void encodeSoftSubtypeConstraint(SubtypeConstraint constraint) {} + + protected void encodeSoftComparableConstraint(ComparableConstraint constraint) {} + + protected void encodeSoftArithmeticConstraint(ArithmeticConstraint constraint) {} + + protected void encodeSoftEqualityConstraint(EqualityConstraint constraint) {} + + protected void encodeSoftInequalityConstraint(InequalityConstraint constraint) {} + + protected void encodeSoftImplicationConstraint(ImplicationConstraint constraint) {} + + protected void encodeSoftExistentialConstraint(ExistentialConstraint constraint) {} + + protected void encodeSoftCombineConstraint(CombineConstraint constraint) {} + + protected void encodeSoftPreferenceConstraint(PreferenceConstraint constraint) {} + + protected void encodeSlotPreferenceConstraint(Slot varSlot) { + // empty string means no optimization group + solver.AssertSoft( + formatTranslator.encodeSlotPreferenceConstraint(varSlot), 1, ""); + } + + protected void addSoftConstraint(Expr serializedConstraint, int weight) { + smtFileContents.append("(assert-soft " + serializedConstraint + " :weight " + weight + ")\n"); + } + + private List runZ3Solver() { + // TODO: add z3 stats? + String[] command; + if (!getUnsatCore) { + command = new String[] {z3Program, constraintsFile}; + } else { + command = new String[] {z3Program, constraintsUnsatCoreFile}; + } + + // stores results from z3 program output + final List results = new ArrayList<>(); + + // Run command + // TODO: check that stdErr has no errors + int exitStatus = + ExternalSolverUtils.runExternalSolver( + command, + stdOut -> parseStdOut(stdOut, results), + stdErr -> ExternalSolverUtils.printStdStream(System.err, stdErr)); + // if exit status from z3 is not 0, then it is unsat + return exitStatus == 0 ? results : null; + } + + // parses the STD output from the z3 process and handles SAT and UNSAT outputs + private void parseStdOut(BufferedReader stdOut, List results) { + String line = ""; + + boolean declarationLine = true; + // each result line is "varName value" + String resultsLine = ""; + + boolean unsat = false; + + try { + while ((line = stdOut.readLine()) != null) { + line = line.trim(); + + if (getUnsatCore) { + // UNSAT Cases ==================== + if (line.contentEquals("unsat")) { + unsat = true; + continue; + } + if (unsat) { + if (line.startsWith("(")) { + line = line.substring(1); // remove open bracket + } + if (line.endsWith(")")) { + line = line.substring(0, line.length() - 1); + } + + for (String constraintID : line.split(" ")) { + unsatConstraintIDs.add(constraintID); + } + continue; + } + } else { + // SAT Cases ======================= + // processing define-fun lines + if (declarationLine && line.startsWith("(define-fun")) { + declarationLine = false; + + int firstBar = line.indexOf('|'); + int lastBar = line.lastIndexOf('|'); + + assert firstBar != -1; + assert lastBar != -1; + assert firstBar < lastBar; + assert line.contains("Bool") || line.contains("Int"); + + // copy z3 variable name into results line + resultsLine += line.substring(firstBar + 1, lastBar); + continue; + } + // processing lines immediately following define-fun lines + if (!declarationLine) { + declarationLine = true; + String value = line.substring(0, line.lastIndexOf(')')); + + if (value.contains("-")) { // negative number + // remove brackets surrounding negative numbers + value = value.substring(1, value.length() - 1); + // remove space between - and the number itself + value = String.join("", value.split(" ")); + } + + resultsLine += " " + value; + results.add(resultsLine); + resultsLine = ""; + continue; + } + } + } + } catch (IOException e) { + e.printStackTrace(); + } + } +} diff --git a/src/checkers/inference/solver/constraintgraph/ConstraintGraph.java b/src/checkers/inference/solver/constraintgraph/ConstraintGraph.java index ab70af534..f171f6011 100644 --- a/src/checkers/inference/solver/constraintgraph/ConstraintGraph.java +++ b/src/checkers/inference/solver/constraintgraph/ConstraintGraph.java @@ -12,7 +12,6 @@ import checkers.inference.model.Constraint; import checkers.inference.model.Slot; import checkers.inference.model.SubtypeConstraint; -import checkers.inference.model.VariableSlot; /** * ConstraintGraph represents constraints in a graph form. Each constraint is an @@ -89,8 +88,8 @@ protected void addConstant(Vertex vertex) { } protected void createEdge(Slot slot1, Slot slot2, Constraint constraint) { - Integer slot1Id = ((VariableSlot) slot1).getId(); - Integer slot2Id = ((VariableSlot) slot2).getId(); + Integer slot1Id = slot1.getId(); + Integer slot2Id = slot2.getId(); Vertex vertex1; Vertex vertex2; diff --git a/src/checkers/inference/solver/constraintgraph/Vertex.java b/src/checkers/inference/solver/constraintgraph/Vertex.java index 0d8bab650..c19b19267 100644 --- a/src/checkers/inference/solver/constraintgraph/Vertex.java +++ b/src/checkers/inference/solver/constraintgraph/Vertex.java @@ -26,15 +26,12 @@ protected Vertex(Slot slot) { this.edges = new HashSet(); this.slot = slot; - if (slot instanceof VariableSlot) { - VariableSlot vs = (VariableSlot) slot; - this.id = vs.getId(); - if (slot instanceof ConstantSlot) { - ConstantSlot cs = (ConstantSlot) slot; - this.value = cs.getValue(); - } else { - this.value = null; - } + this.id = slot.getId(); + if (slot instanceof ConstantSlot) { + ConstantSlot cs = (ConstantSlot) slot; + this.value = cs.getValue(); + } else { + this.value = null; } } diff --git a/src/checkers/inference/solver/util/Statistics.java b/src/checkers/inference/solver/util/Statistics.java index 7d0366c0b..4c609bfe5 100644 --- a/src/checkers/inference/solver/util/Statistics.java +++ b/src/checkers/inference/solver/util/Statistics.java @@ -6,10 +6,8 @@ import java.util.Map; import java.util.Map.Entry; -import checkers.inference.model.ConstantSlot; import checkers.inference.model.Constraint; import checkers.inference.model.Slot; -import checkers.inference.model.VariableSlot; /** * Recorder for statistics. @@ -55,7 +53,7 @@ public static void recordSlotsStatistics(final Collection slots) { long totalVariableSlots = 0; for (Slot slot : slots) { - if (slot instanceof VariableSlot && !(slot instanceof ConstantSlot)) { + if (slot.isVariable()) { totalVariableSlots++; } diff --git a/src/checkers/inference/typearginference/InferenceTypeArgumentInference.java b/src/checkers/inference/typearginference/InferenceTypeArgumentInference.java index eab851259..71e5974e1 100644 --- a/src/checkers/inference/typearginference/InferenceTypeArgumentInference.java +++ b/src/checkers/inference/typearginference/InferenceTypeArgumentInference.java @@ -203,7 +203,7 @@ private void replaceExistentialVariables(AnnotatedExecutableType methodType, Ann upperBoundVariable = ((ExistentialVariableSlot) upperBoundVariable).getPotentialSlot(); } - VariableSlot lowerBoundVariable = slotManager.getVariableSlot(lowerBound); + Slot lowerBoundVariable = slotManager.getVariableSlot(lowerBound); Slot newSlot = targetToPrimary.get(target); variableSlotReplacer.addReplacement(upperBoundVariable, newSlot); diff --git a/src/checkers/inference/util/InferenceViewpointAdapter.java b/src/checkers/inference/util/InferenceViewpointAdapter.java index 86c2f9cc4..08fbe8234 100644 --- a/src/checkers/inference/util/InferenceViewpointAdapter.java +++ b/src/checkers/inference/util/InferenceViewpointAdapter.java @@ -23,7 +23,7 @@ public InferenceViewpointAdapter(AnnotatedTypeFactory atypeFactory) { @Override protected AnnotationMirror extractAnnotationMirror(AnnotatedTypeMirror atm) { - final VariableSlot varSlot = slotManager.getVariableSlot(atm); + final Slot varSlot = slotManager.getVariableSlot(atm); if (varSlot == null && !InferenceMain.isHackMode()) { throw new BugInCF(atm + " doesn't contain a slot"); } diff --git a/src/sparta/checkers/propagation/IFlowSolver.java b/src/sparta/checkers/propagation/IFlowSolver.java index 55e58e62a..03cbb8b3b 100644 --- a/src/sparta/checkers/propagation/IFlowSolver.java +++ b/src/sparta/checkers/propagation/IFlowSolver.java @@ -174,7 +174,7 @@ private Set getInferredSlotPermissions(Slot slot) { if (slot.getKind() == Kind.EXISTENTIAL_VARIABLE) { throw new IllegalArgumentException("Unexpected variable type:" + slot); } - return getFlowSet(((VariableSlot) slot).getId()); + return getFlowSet(slot.getId()); } else if (slot.isConstant()) { Set constantSet = new HashSet<>(); From 9af2d3452d35e06f565d6902882c3c246bc24612 Mon Sep 17 00:00:00 2001 From: txiang61 Date: Thu, 14 Nov 2019 03:49:10 -0500 Subject: [PATCH 04/10] add ArithmeticVariableSlot serialization and clean up some code --- .../inference/DefaultSlotManager.java | 56 +++++++++---------- .../InferenceAnnotatedTypeFactory.java | 4 +- .../InferenceQualifierHierarchy.java | 29 +++++----- .../InferenceTypeVariableSubstitutor.java | 5 +- src/checkers/inference/SlotManager.java | 2 +- .../inference/dataflow/InferenceValue.java | 22 ++++---- src/checkers/inference/model/Serializer.java | 4 +- .../serialization/CnfVecIntSerializer.java | 13 +++-- .../model/serialization/JsonSerializer.java | 17 ++++-- .../serialization/ToStringSerializer.java | 18 +++--- .../backend/AbstractFormatTranslator.java | 11 ++-- .../z3/Z3BitVectorFormatTranslator.java | 13 +++-- .../backend/z3smt/Z3SmtFormatTranslator.java | 11 ++-- .../inference/solver/util/PrintUtils.java | 13 +++-- .../solvers/classic/DataflowSerializer.java | 1 + 15 files changed, 112 insertions(+), 107 deletions(-) diff --git a/src/checkers/inference/DefaultSlotManager.java b/src/checkers/inference/DefaultSlotManager.java index 2f50456e8..b4d650a5e 100644 --- a/src/checkers/inference/DefaultSlotManager.java +++ b/src/checkers/inference/DefaultSlotManager.java @@ -54,7 +54,7 @@ public class DefaultSlotManager implements SlotManager { * ConstantSlots are also stored in this map, since ConstantSlot is subclass * of Slot. */ - private final Map variables; + private final Map slots; /** * A map of {@link AnnotationMirror} to {@link Integer} for caching @@ -105,7 +105,7 @@ public DefaultSlotManager( final ProcessingEnvironment processingEnvironment, this.processingEnvironment = processingEnvironment; // sort the qualifiers so that they are always assigned the same varId this.realQualifiers = sortAnnotationClasses(realQualifiers); - variables = new LinkedHashMap<>(); + slots = new LinkedHashMap<>(); AnnotationBuilder builder = new AnnotationBuilder(processingEnvironment, VarAnnot.class); builder.setValue("value", -1 ); @@ -123,7 +123,7 @@ public DefaultSlotManager( final ProcessingEnvironment processingEnvironment, Set mirrors = InferenceMain.getInstance().getRealTypeFactory().getQualifierHierarchy().getTypeQualifiers(); for (AnnotationMirror am : mirrors) { ConstantSlot constantSlot = new ConstantSlot(am, nextId()); - addToVariables(constantSlot); + addToSlots(constantSlot); constantCache.put(am, constantSlot.getId()); } } @@ -157,16 +157,16 @@ private int nextId() { return nextId++; } - private void addToVariables(final Slot slot) { - variables.put(slot.getId(), slot); + private void addToSlots(final Slot slot) { + slots.put(slot.getId(), slot); } /** * @inheritDoc */ @Override - public Slot getVariable( int id ) { - return variables.get(id); + public Slot getSlot( int id ) { + return slots.get(id); } /** @@ -227,12 +227,12 @@ public Slot getSlot( final AnnotationMirror annotationMirror ) { id = Integer.valueOf( annoValue.toString() ); } - return getVariable( id ); + return getSlot( id ); } else { if (constantCache.containsKey(annotationMirror)) { - ConstantSlot constantSlot = (ConstantSlot) getVariable( + ConstantSlot constantSlot = (ConstantSlot) getSlot( constantCache.get(annotationMirror)); return constantSlot; @@ -257,7 +257,7 @@ public Slot getSlot( final AnnotationMirror annotationMirror ) { */ @Override public List getSlots() { - return new ArrayList(this.variables.values()); + return new ArrayList(this.slots.values()); } // Sometimes, I miss scala. @@ -267,7 +267,7 @@ public List getSlots() { @Override public List getVariableSlots() { List varSlots = new ArrayList<>(); - for (Slot slot : variables.values()) { + for (Slot slot : slots.values()) { if (slot.isVariable()) { varSlots.add(slot); } @@ -281,7 +281,7 @@ public List getVariableSlots() { @Override public List getConstantSlots() { List constants = new ArrayList<>(); - for (Slot slot : variables.values()) { + for (Slot slot : slots.values()) { if (slot.isConstant()) { constants.add((ConstantSlot) slot); } @@ -300,13 +300,13 @@ public VariableSlot createVariableSlot(AnnotationLocation location, TypeMirror t if (location.getKind() == AnnotationLocation.Kind.MISSING) { //Don't cache slot for MISSING LOCATION. Just create a new one and return. variableSlot = new VariableSlot(location, nextId(), type); - addToVariables(variableSlot); + addToSlots(variableSlot); } else if (locationCache.containsKey(location)) { int id = locationCache.get(location); - variableSlot = (VariableSlot) getVariable(id); + variableSlot = (VariableSlot) getSlot(id); } else { variableSlot = new VariableSlot(location, nextId(), type); - addToVariables(variableSlot); + addToSlots(variableSlot); locationCache.put(location, variableSlot.getId()); } return variableSlot; @@ -318,13 +318,13 @@ public RefinementVariableSlot createRefinementVariableSlot(AnnotationLocation lo if (location.getKind() == AnnotationLocation.Kind.MISSING) { //Don't cache slot for MISSING LOCATION. Just create a new one and return. refinementVariableSlot = new RefinementVariableSlot(location, nextId(), refined); - addToVariables(refinementVariableSlot); + addToSlots(refinementVariableSlot); } else if (locationCache.containsKey(location)) { int id = locationCache.get(location); - refinementVariableSlot = (RefinementVariableSlot) getVariable(id); + refinementVariableSlot = (RefinementVariableSlot) getSlot(id); } else { refinementVariableSlot = new RefinementVariableSlot(location, nextId(), refined); - addToVariables(refinementVariableSlot); + addToSlots(refinementVariableSlot); locationCache.put(location, refinementVariableSlot.getId()); } return refinementVariableSlot; @@ -335,10 +335,10 @@ public ConstantSlot createConstantSlot(AnnotationMirror value) { ConstantSlot constantSlot; if (constantCache.containsKey(value)) { int id = constantCache.get(value); - constantSlot = (ConstantSlot) getVariable(id); + constantSlot = (ConstantSlot) getSlot(id); } else { constantSlot = new ConstantSlot(value, nextId()); - addToVariables(constantSlot); + addToSlots(constantSlot); constantCache.put(value, constantSlot.getId()); } return constantSlot; @@ -350,10 +350,10 @@ public CombVariableSlot createCombVariableSlot(Slot receiver, Slot declared) { Pair pair = new Pair<>(receiver, declared); if (combSlotPairCache.containsKey(pair)) { int id = combSlotPairCache.get(pair); - combVariableSlot = (CombVariableSlot) getVariable(id); + combVariableSlot = (CombVariableSlot) getSlot(id); } else { combVariableSlot = new CombVariableSlot(null, nextId(), receiver, declared); - addToVariables(combVariableSlot); + addToSlots(combVariableSlot); combSlotPairCache.put(pair, combVariableSlot.getId()); } return combVariableSlot; @@ -366,11 +366,11 @@ public LubVariableSlot createLubVariableSlot(Slot left, Slot right) { Pair pair = new Pair<>(left, right); if (lubSlotPairCache.containsKey(pair)) { int id = lubSlotPairCache.get(pair); - lubVariableSlot = (LubVariableSlot) getVariable(id); + lubVariableSlot = (LubVariableSlot) getSlot(id); } else { // We need a non-null location in the future for better debugging outputs lubVariableSlot = new LubVariableSlot(null, nextId(), left, right); - addToVariables(lubVariableSlot); + addToSlots(lubVariableSlot); lubSlotPairCache.put(pair, lubVariableSlot.getId()); } return lubVariableSlot; @@ -382,10 +382,10 @@ public ExistentialVariableSlot createExistentialVariableSlot(Slot potentialSlot, Pair pair = new Pair<>(potentialSlot, alternativeSlot); if (existentialSlotPairCache.containsKey(pair)) { int id = existentialSlotPairCache.get(pair); - existentialVariableSlot = (ExistentialVariableSlot) getVariable(id); + existentialVariableSlot = (ExistentialVariableSlot) getSlot(id); } else { existentialVariableSlot = new ExistentialVariableSlot(nextId(), potentialSlot, alternativeSlot); - addToVariables(existentialVariableSlot); + addToSlots(existentialVariableSlot); existentialSlotPairCache.put(pair, existentialVariableSlot.getId()); } return existentialVariableSlot; @@ -401,7 +401,7 @@ public ArithmeticVariableSlot createArithmeticVariableSlot(AnnotationLocation lo // create the arithmetic var slot if it doesn't exist for the given location if (!arithmeticSlotCache.containsKey(location)) { ArithmeticVariableSlot slot = new ArithmeticVariableSlot(location, nextId()); - addToVariables(slot); + addToSlots(slot); arithmeticSlotCache.put(location, slot.getId()); return slot; } @@ -418,7 +418,7 @@ public ArithmeticVariableSlot getArithmeticVariableSlot(AnnotationLocation locat if (!arithmeticSlotCache.containsKey(location)) { return null; } else { - return (ArithmeticVariableSlot) getVariable(arithmeticSlotCache.get(location)); + return (ArithmeticVariableSlot) getSlot(arithmeticSlotCache.get(location)); } } diff --git a/src/checkers/inference/InferenceAnnotatedTypeFactory.java b/src/checkers/inference/InferenceAnnotatedTypeFactory.java index 755cdc43e..168656a1c 100644 --- a/src/checkers/inference/InferenceAnnotatedTypeFactory.java +++ b/src/checkers/inference/InferenceAnnotatedTypeFactory.java @@ -124,7 +124,7 @@ public class InferenceAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { // though we know the value of that variable. In this case, rather than creating a new variable // for every one of these locations and increase the number of variables we solve for, use // the same variable slot for all of these locations. This map contains those variables. - private Map, ConstantSlot> constantToVarAnnot = new HashMap<>(); + private Map, VariableSlot> constantToVarAnnot = new HashMap<>(); public InferenceAnnotatedTypeFactory( InferenceChecker inferenceChecker, @@ -265,7 +265,7 @@ protected DependentTypesHelper createDependentTypesHelper() { return null; } - protected Map, ConstantSlot> getConstantVars() { + protected Map, VariableSlot> getConstantVars() { return Collections.unmodifiableMap(constantToVarAnnot); } diff --git a/src/checkers/inference/InferenceQualifierHierarchy.java b/src/checkers/inference/InferenceQualifierHierarchy.java index d6d9c0c08..ef57a7040 100644 --- a/src/checkers/inference/InferenceQualifierHierarchy.java +++ b/src/checkers/inference/InferenceQualifierHierarchy.java @@ -264,32 +264,29 @@ public AnnotationMirror leastUpperBound(final AnnotationMirror a1, final Annotat Slot constantSlot = slotMgr.createConstantSlot(realLub); return slotMgr.getAnnotation(constantSlot); } else { - Slot var1 = slot1; - Slot var2 = slot2; - - if (var1 == var2) { + if (slot1 == slot2) { // They are the same slot. - return slotMgr.getAnnotation(var1); + return slotMgr.getAnnotation(slot1); - } else if (!Collections.disjoint(var1.getMergedToSlots(), var2.getMergedToSlots())) { + } else if (!Collections.disjoint(slot1.getMergedToSlots(), slot2.getMergedToSlots())) { // They have common merge variables, return the annotations on one of the common merged variables. - Slot commonMergedSlot = getOneIntersected(var1.getMergedToSlots(), var2.getMergedToSlots()); + Slot commonMergedSlot = getOneIntersected(slot1.getMergedToSlots(), slot2.getMergedToSlots()); return slotMgr.getAnnotation(commonMergedSlot); - } else if (var1.isMergedTo(var2)) { + } else if (slot1.isMergedTo(slot2)) { // var2 is a merge variable that var1 has been merged to. So just return annotation on var2. - return slotMgr.getAnnotation(var2); - } else if (var2.isMergedTo(var1)) { + return slotMgr.getAnnotation(slot2); + } else if (slot2.isMergedTo(slot1)) { // Vice versa. - return slotMgr.getAnnotation(var1); + return slotMgr.getAnnotation(slot1); } else { // Create a new LubVariable for var1 and var2. - final LubVariableSlot mergeVariableSlot = slotMgr.createLubVariableSlot(var1, var2); - constraintMgr.addSubtypeConstraint(var1, mergeVariableSlot); - constraintMgr.addSubtypeConstraint(var2, mergeVariableSlot); + final LubVariableSlot mergeVariableSlot = slotMgr.createLubVariableSlot(slot1, slot2); + constraintMgr.addSubtypeConstraint(slot1, mergeVariableSlot); + constraintMgr.addSubtypeConstraint(slot2, mergeVariableSlot); - var1.addMergedToSlot(mergeVariableSlot); - var2.addMergedToSlot(mergeVariableSlot); + slot1.addMergedToSlot(mergeVariableSlot); + slot2.addMergedToSlot(mergeVariableSlot); return slotMgr.getAnnotation(mergeVariableSlot); } diff --git a/src/checkers/inference/InferenceTypeVariableSubstitutor.java b/src/checkers/inference/InferenceTypeVariableSubstitutor.java index ed2af3b75..59005050e 100644 --- a/src/checkers/inference/InferenceTypeVariableSubstitutor.java +++ b/src/checkers/inference/InferenceTypeVariableSubstitutor.java @@ -71,9 +71,8 @@ protected AnnotatedTypeMirror substituteTypeVariable(AnnotatedTypeMirror argumen if (argument.getKind() != TypeKind.TYPEVAR) { final Slot altSlot = slotManager.getVariableSlot(argument); - final Slot alternative = altSlot; - if (alternative != null) { - final ExistentialVariableSlot slot = slotManager.createExistentialVariableSlot(potentialSlot, alternative); + if (altSlot != null) { + final ExistentialVariableSlot slot = slotManager.createExistentialVariableSlot(potentialSlot, altSlot); argument.replaceAnnotation(slotManager.getAnnotation(slot)); } else { if (!InferenceMain.isHackMode()) { diff --git a/src/checkers/inference/SlotManager.java b/src/checkers/inference/SlotManager.java index bced6a806..208cfb41b 100644 --- a/src/checkers/inference/SlotManager.java +++ b/src/checkers/inference/SlotManager.java @@ -152,7 +152,7 @@ public interface SlotManager { AnnotationMirror createEquivalentVarAnno(final AnnotationMirror realQualifier); /** Return the variable identified by the given id or null if no such variable has been added */ - Slot getVariable( int id ); + Slot getSlot( int id ); /** * Given a slot return an annotation that represents the slot when added to an AnnotatedTypeMirror. diff --git a/src/checkers/inference/dataflow/InferenceValue.java b/src/checkers/inference/dataflow/InferenceValue.java index 749860486..0f4d90171 100644 --- a/src/checkers/inference/dataflow/InferenceValue.java +++ b/src/checkers/inference/dataflow/InferenceValue.java @@ -119,29 +119,27 @@ public CFValue mostSpecific(CFValue other, CFValue backup) { */ public CFValue mostSpecificFromSlot(final Slot thisSlot, final Slot otherSlot, final CFValue other, final CFValue backup) { if (thisSlot.isVariable() && otherSlot.isVariable()) { - Slot thisVarSlot = thisSlot; - Slot otherVarSlot = otherSlot; - if (thisVarSlot.isMergedTo(otherVarSlot)) { + if (thisSlot.isMergedTo(otherSlot)) { return other; - } else if (otherVarSlot.isMergedTo(thisVarSlot)) { + } else if (otherSlot.isMergedTo(thisSlot)) { return this; - } else if (thisVarSlot instanceof RefinementVariableSlot - && ((RefinementVariableSlot) thisVarSlot).getRefined().equals(otherVarSlot)) { + } else if (thisSlot instanceof RefinementVariableSlot + && ((RefinementVariableSlot) thisSlot).getRefined().equals(otherSlot)) { return this; - } else if (otherVarSlot instanceof RefinementVariableSlot - && ((RefinementVariableSlot) otherVarSlot).getRefined().equals(thisVarSlot)) { + } else if (otherSlot instanceof RefinementVariableSlot + && ((RefinementVariableSlot) otherSlot).getRefined().equals(thisSlot)) { return other; } else { // Check if one of these has refinement variables that were merged to the other. - for (RefinementVariableSlot slot : thisVarSlot.getRefinedToSlots()) { - if (slot.isMergedTo(otherVarSlot)) { + for (RefinementVariableSlot slot : thisSlot.getRefinedToSlots()) { + if (slot.isMergedTo(otherSlot)) { return other; } } - for (RefinementVariableSlot slot : otherVarSlot.getRefinedToSlots()) { - if (slot.isMergedTo(thisVarSlot)) { + for (RefinementVariableSlot slot : otherSlot.getRefinedToSlots()) { + if (slot.isMergedTo(thisSlot)) { return this; } } diff --git a/src/checkers/inference/model/Serializer.java b/src/checkers/inference/model/Serializer.java index 3cb4d2379..41944a754 100644 --- a/src/checkers/inference/model/Serializer.java +++ b/src/checkers/inference/model/Serializer.java @@ -26,8 +26,6 @@ public interface Serializer { T serialize(InequalityConstraint constraint); - S serialize(Slot slot); - S serialize(VariableSlot slot); S serialize(ConstantSlot slot); @@ -40,6 +38,8 @@ public interface Serializer { S serialize(LubVariableSlot slot); + S serialize(ArithmeticVariableSlot slot); + T serialize(ComparableConstraint comparableConstraint); T serialize(CombineConstraint combineConstraint); diff --git a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java index d2848c741..bf6ebe526 100644 --- a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java +++ b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java @@ -11,6 +11,7 @@ import checkers.inference.SlotManager; import checkers.inference.model.ArithmeticConstraint; +import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; @@ -215,12 +216,6 @@ public boolean emptyClause(VecInt ... clauses) { return false; } - @Override - public VecInt[] serialize(Slot slot) { - // doesn't really mean anything - return null; - } - @Override public VecInt[] serialize(VariableSlot slot) { // doesn't really mean anything @@ -249,6 +244,12 @@ public VecInt[] serialize(CombVariableSlot slot) { public VecInt[] serialize(LubVariableSlot slot) { return null; } + + @Override + public VecInt[] serialize(ArithmeticVariableSlot slot) { + // doesn't really mean anything + return null; + } @Override public VecInt[] serialize(ExistentialVariableSlot slot) { diff --git a/src/checkers/inference/model/serialization/JsonSerializer.java b/src/checkers/inference/model/serialization/JsonSerializer.java index ef6faa2c4..120f5bed4 100644 --- a/src/checkers/inference/model/serialization/JsonSerializer.java +++ b/src/checkers/inference/model/serialization/JsonSerializer.java @@ -12,6 +12,7 @@ import org.json.simple.JSONArray; import org.json.simple.JSONObject; import checkers.inference.model.ArithmeticConstraint; +import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; @@ -212,19 +213,18 @@ protected String getConstantString(AnnotationMirror value) { return annotationSerializer.serialize(value); } - @Override - public String serialize(Slot slot) { + private String serializeSlot(Slot slot) { return VAR_PREFIX + slot.getId(); } @Override public String serialize(VariableSlot slot) { - return serialize((Slot) slot); + return serializeSlot(slot); } @Override public String serialize(RefinementVariableSlot slot) { - return serialize((Slot) slot); + return serializeSlot(slot); } @Override @@ -240,12 +240,17 @@ public String serialize(ConstantSlot slot) { @Override public String serialize(CombVariableSlot slot) { - return serialize((Slot) slot); + return serializeSlot(slot); } @Override public String serialize(LubVariableSlot slot) { - return serialize((Slot) slot); + return serializeSlot(slot); + } + + @Override + public String serialize(ArithmeticVariableSlot slot) { + return serializeSlot(slot); } @SuppressWarnings("unchecked") diff --git a/src/checkers/inference/model/serialization/ToStringSerializer.java b/src/checkers/inference/model/serialization/ToStringSerializer.java index 0f2d5b649..7b3ca7c0d 100644 --- a/src/checkers/inference/model/serialization/ToStringSerializer.java +++ b/src/checkers/inference/model/serialization/ToStringSerializer.java @@ -12,6 +12,7 @@ import org.checkerframework.javacutil.PluginUtil; import checkers.inference.InferenceMain; import checkers.inference.model.ArithmeticConstraint; +import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; @@ -295,15 +296,6 @@ private String getAssumptionsString(ImplicationConstraint implicationConstraint) return String.join(" & ", serializedAssumptions); } - // variables - @Override - public String serialize(Slot slot) { - final StringBuilder sb = new StringBuilder(); - sb.append(slot.getId()); - optionallyShowVerbose(slot, sb); - return sb.toString(); - } - @Override public String serialize(VariableSlot slot) { final StringBuilder sb = new StringBuilder(); @@ -362,6 +354,14 @@ public String serialize(LubVariableSlot slot) { return sb.toString(); } + @Override + public String serialize(ArithmeticVariableSlot slot) { + final StringBuilder sb = new StringBuilder(); + sb.append(slot.getId()); + optionallyShowVerbose(slot, sb); + return sb.toString(); + } + /** * @return the indent string for the current indentation level as stored in * {@link #indentationLevel}. diff --git a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java index 186e639a1..7f2485cb3 100644 --- a/src/checkers/inference/solver/backend/AbstractFormatTranslator.java +++ b/src/checkers/inference/solver/backend/AbstractFormatTranslator.java @@ -1,6 +1,7 @@ package checkers.inference.solver.backend; import checkers.inference.model.ArithmeticConstraint; +import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; @@ -208,11 +209,6 @@ public ConstraintEncodingT serialize(ArithmeticConstraint constraint) { ConstraintEncoderCoordinator.dispatch(constraint, arithmeticConstraintEncoder); } - @Override - public SlotEncodingT serialize(Slot slot) { - return null; - } - @Override public SlotEncodingT serialize(VariableSlot slot) { return null; @@ -242,4 +238,9 @@ public SlotEncodingT serialize(CombVariableSlot slot) { public SlotEncodingT serialize(LubVariableSlot slot) { return null; } + + @Override + public SlotEncodingT serialize(ArithmeticVariableSlot slot) { + return null; + } } diff --git a/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java b/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java index fe3e25df6..30d09dde1 100644 --- a/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java +++ b/src/checkers/inference/solver/backend/z3/Z3BitVectorFormatTranslator.java @@ -18,6 +18,7 @@ import com.microsoft.z3.Context; import com.microsoft.z3.Optimize; +import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ExistentialVariableSlot; @@ -120,12 +121,7 @@ public BitVecExpr serializeConstantSlot(ConstantSlot slot) { protected ConstraintEncoderFactory createConstraintEncoderFactory() { return new Z3BitVectorConstraintEncoderFactory(lattice, context, this); } - - @Override - public BitVecExpr serialize(Slot slot) { - return serializeVarSlot(slot); - } - + @Override public BitVecExpr serialize(VariableSlot slot) { return serializeVarSlot(slot); @@ -155,6 +151,11 @@ public BitVecExpr serialize(CombVariableSlot slot) { public BitVecExpr serialize(LubVariableSlot slot) { return serializeVarSlot(slot); } + + @Override + public BitVecExpr serialize(ArithmeticVariableSlot slot) { + return serializeVarSlot(slot); + } @Override public AnnotationMirror decodeSolution(BitVecNum solution, ProcessingEnvironment processingEnvironment) { diff --git a/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java b/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java index 676aa8564..dca3176c6 100644 --- a/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java +++ b/src/checkers/inference/solver/backend/z3smt/Z3SmtFormatTranslator.java @@ -1,5 +1,6 @@ package checkers.inference.solver.backend.z3smt; +import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; import checkers.inference.model.ConstantSlot; import checkers.inference.model.ExistentialVariableSlot; @@ -41,11 +42,6 @@ public final void init(Context ctx) { protected abstract SlotEncodingT serializeConstantSlot(ConstantSlot slot); - @Override - public SlotEncodingT serialize(Slot slot) { - return serializeVarSlot(slot); - } - @Override public SlotEncodingT serialize(VariableSlot slot) { return serializeVarSlot(slot); @@ -75,6 +71,11 @@ public SlotEncodingT serialize(CombVariableSlot slot) { public SlotEncodingT serialize(LubVariableSlot slot) { return serializeVarSlot(slot); } + + @Override + public SlotEncodingT serialize(ArithmeticVariableSlot slot) { + return serializeVarSlot(slot); + } /** * Subclasses can override this method to perform pre-analysis of slots for encoding diff --git a/src/checkers/inference/solver/util/PrintUtils.java b/src/checkers/inference/solver/util/PrintUtils.java index 3c38c13e4..ca869cf03 100644 --- a/src/checkers/inference/solver/util/PrintUtils.java +++ b/src/checkers/inference/solver/util/PrintUtils.java @@ -13,6 +13,7 @@ import checkers.inference.InferenceMain; import checkers.inference.model.ArithmeticConstraint; +import checkers.inference.model.ArithmeticVariableSlot; import checkers.inference.model.CombVariableSlot; import checkers.inference.model.CombineConstraint; import checkers.inference.model.ComparableConstraint; @@ -288,12 +289,6 @@ public Void serialize(ConstantSlot slot) { return null; } - @Override - public Void serialize(Slot slot) { - addSlotIfNotAdded(slot); - return null; - } - @Override public Void serialize(VariableSlot slot) { addSlotIfNotAdded(slot); @@ -330,5 +325,11 @@ public Void serialize(LubVariableSlot slot) { addSlotIfNotAdded(slot); return null; } + + @Override + public Void serialize(ArithmeticVariableSlot slot) { + addSlotIfNotAdded(slot); + return null; + } } } diff --git a/src/dataflow/solvers/classic/DataflowSerializer.java b/src/dataflow/solvers/classic/DataflowSerializer.java index 2c7817e51..4e404572a 100644 --- a/src/dataflow/solvers/classic/DataflowSerializer.java +++ b/src/dataflow/solvers/classic/DataflowSerializer.java @@ -14,6 +14,7 @@ import checkers.inference.InferenceMain; import checkers.inference.model.ConstantSlot; import checkers.inference.model.Constraint; +import checkers.inference.model.VariableSlot; import checkers.inference.model.serialization.CnfVecIntSerializer; import dataflow.qual.DataFlowTop; import dataflow.util.DataflowUtils; From 8bccb7d7f1fa11de4e11663180fe9aaf8d35660d Mon Sep 17 00:00:00 2001 From: txiang61 Date: Fri, 15 Nov 2019 18:24:10 -0500 Subject: [PATCH 05/10] update test files and correct variableslot insertion and utilize variable annotator --- src/checkers/inference/VariableAnnotator.java | 2 +- src/checkers/inference/model/VariableSlot.java | 2 +- .../checkers/system/StatisticsMultithreadTest.java | 14 +++++++++++--- 3 files changed, 13 insertions(+), 5 deletions(-) diff --git a/src/checkers/inference/VariableAnnotator.java b/src/checkers/inference/VariableAnnotator.java index 2b0ccfd2a..5df66c20c 100644 --- a/src/checkers/inference/VariableAnnotator.java +++ b/src/checkers/inference/VariableAnnotator.java @@ -198,7 +198,7 @@ protected AnnotationLocation treeToLocation(Tree tree) { } protected TypeMirror treeToType(Tree tree) { - return InferenceMain.getInstance().getRealTypeFactory().getAnnotatedType(tree).getUnderlyingType(); + return TreeUtils.typeOf(tree); } /** diff --git a/src/checkers/inference/model/VariableSlot.java b/src/checkers/inference/model/VariableSlot.java index 4c82f2fc6..6b98d0405 100644 --- a/src/checkers/inference/model/VariableSlot.java +++ b/src/checkers/inference/model/VariableSlot.java @@ -69,6 +69,6 @@ public TypeMirror getUnderlyingType() { */ @Override public boolean isInsertable() { - return false; + return true; } } diff --git a/tests/checkers/system/StatisticsMultithreadTest.java b/tests/checkers/system/StatisticsMultithreadTest.java index 66b07dd02..1a401e368 100644 --- a/tests/checkers/system/StatisticsMultithreadTest.java +++ b/tests/checkers/system/StatisticsMultithreadTest.java @@ -125,9 +125,9 @@ private String classStatsKeyName(Class clazz) { public void testRecordSlotsStatistics() { slots = new ArrayList<>(); - slots.add(new DummyOneSlot()); - slots.add(new DummyTwoSlot()); - slots.add(new DummyTwoSlot()); + slots.add(new DummyOneSlot(0)); + slots.add(new DummyTwoSlot(1)); + slots.add(new DummyTwoSlot(2)); runThreads(threadID -> new RecordSlotsTestThread()); @@ -145,6 +145,10 @@ public void run() { // dummy slots used in this test private class DummyOneSlot extends Slot { + public DummyOneSlot(int id) { + super(id); + } + @Override public S serialize(Serializer serializer) { return null; @@ -157,6 +161,10 @@ public Kind getKind() { } private class DummyTwoSlot extends Slot { + public DummyTwoSlot(int id) { + super(id); + } + @Override public S serialize(Serializer serializer) { return null; From 5908ead2b6ce5942a9e48ee08790d0a5f29b5fb3 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Tue, 19 Nov 2019 19:57:42 -0500 Subject: [PATCH 06/10] Update Serializer.java --- src/checkers/inference/model/Serializer.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/checkers/inference/model/Serializer.java b/src/checkers/inference/model/Serializer.java index bfba88dad..41944a754 100644 --- a/src/checkers/inference/model/Serializer.java +++ b/src/checkers/inference/model/Serializer.java @@ -26,8 +26,6 @@ public interface Serializer { T serialize(InequalityConstraint constraint); - S serialize(Slot slot); - S serialize(VariableSlot slot); S serialize(ConstantSlot slot); From 23def4052cd173b35c74d956e6b7c07ad0e3eb94 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Tue, 19 Nov 2019 19:58:09 -0500 Subject: [PATCH 07/10] Update CnfVecIntSerializer.java --- .../inference/model/serialization/CnfVecIntSerializer.java | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java index 522102e4c..bf6ebe526 100644 --- a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java +++ b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java @@ -216,12 +216,6 @@ public boolean emptyClause(VecInt ... clauses) { return false; } - @Override - public VecInt[] serialize(Slot slot) { - // doesn't really mean anything - return null; - } - @Override public VecInt[] serialize(VariableSlot slot) { // doesn't really mean anything From a6574c0e3555b50d091c023fdf9a82ccdfcc6dc2 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Tue, 19 Nov 2019 20:00:53 -0500 Subject: [PATCH 08/10] Update JsonSerializer.java --- src/checkers/inference/model/serialization/JsonSerializer.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/checkers/inference/model/serialization/JsonSerializer.java b/src/checkers/inference/model/serialization/JsonSerializer.java index c764eb0eb..2528c85bd 100644 --- a/src/checkers/inference/model/serialization/JsonSerializer.java +++ b/src/checkers/inference/model/serialization/JsonSerializer.java @@ -218,6 +218,7 @@ private String serializeSlot(Slot slot) { } @Override + public String serialize(VariableSlot slot) { return serializeSlot(slot); } From e1a18504525870a0536afe5de4e8f2e2dfeb33b9 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Tue, 19 Nov 2019 20:02:59 -0500 Subject: [PATCH 09/10] Update ToStringSerializer.java --- .../inference/model/serialization/ToStringSerializer.java | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/checkers/inference/model/serialization/ToStringSerializer.java b/src/checkers/inference/model/serialization/ToStringSerializer.java index 80fdd8f90..7b3ca7c0d 100644 --- a/src/checkers/inference/model/serialization/ToStringSerializer.java +++ b/src/checkers/inference/model/serialization/ToStringSerializer.java @@ -296,14 +296,6 @@ private String getAssumptionsString(ImplicationConstraint implicationConstraint) return String.join(" & ", serializedAssumptions); } - @Override - public String serialize(Slot slot) { - final StringBuilder sb = new StringBuilder(); - sb.append(slot.getId()); - optionallyShowVerbose(slot, sb); - return sb.toString(); - } - @Override public String serialize(VariableSlot slot) { final StringBuilder sb = new StringBuilder(); From cd33d90143245b18e09fd30b58f64d28769df452 Mon Sep 17 00:00:00 2001 From: Jenny Xiang Date: Tue, 19 Nov 2019 20:03:54 -0500 Subject: [PATCH 10/10] Update PrintUtils.java --- src/checkers/inference/solver/util/PrintUtils.java | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/checkers/inference/solver/util/PrintUtils.java b/src/checkers/inference/solver/util/PrintUtils.java index 075318a6e..ca869cf03 100644 --- a/src/checkers/inference/solver/util/PrintUtils.java +++ b/src/checkers/inference/solver/util/PrintUtils.java @@ -289,12 +289,6 @@ public Void serialize(ConstantSlot slot) { return null; } - @Override - public Void serialize(Slot slot) { - addSlotIfNotAdded(slot); - return null; - } - @Override public Void serialize(VariableSlot slot) { addSlotIfNotAdded(slot);